Prove cast validation and exact-size metadata inference

Specify metadata_for_exact_size and validate_cast_and_convert_metadata
against independent layout calculations. Prove exact representability,
greatest-fitting metadata, alignment-before-size error priority and the
complete prefix or suffix result.

Add Rust assertion harnesses comparing the full optional metadata and cast
outcomes with remainder-based checked arithmetic. Keep address-addition
bounds and the zero-stride panic exclusion visible in their domains.
Outcome examples cover unattainable sizes and intentional panic separately
from checks of the specification's meaning.

Prove the concrete u32 slice KnownLayout initializer and every checked
size_for_elems result through a Rust assertion harness. Admission traverses
the actual local constant body, rather than assuming its descriptor. An
initializer mutation challenges that connection.

Retain reproducible native capability fixtures for generic KnownLayout,
the production transmute macro, and raw pointers. Unsupported equalities,
recursive declaration dependencies, and incomplete pointer carriers remain
explicit blockers; no bounds or declarations are removed to admit them.

gherrit-pr-id: Grerckvocdnwpdtef665ubpieo6wlwfdj
Agent-authored-by: AI agent acting on joshlf's behalf

Author: joshlf

verification/aeneas/DESIGN.md

@@ -304,6 +304,92 @@ the library already models every part of Rust's abstract machine.
 
 ## Deferred decisions and reopening evidence
 
+### Resource-free layout and storage work
+
+The shared library supplies two independent foundations for layout and owned
+byte-cast proofs:
+
+- `Rust.Pointer.Value` retains an address, opaque optional provenance, and
+  metadata. Its casts and metadata operations preserve the exact provenance
+  value. Pointer equality observes address and metadata; it does not compare
+  provenance. Non-nullness supplies no alignment, liveness, or access permission.
+- `Rust.Storage.StorageDecoder` takes metadata explicitly, checks the requested
+  byte width, and checks that a successful raw result carries that metadata.
+  Fixed-width decoders adapt through unit metadata. Slice counts are inputs,
+  including for zero-sized elements; byte length cannot recover those counts.
+
+These are mathematical definitions and checked laws, not newly admitted Rust
+operations. The storage carrier still contains only initialized numeric bytes
+and uninitialized bytes. It does not encode pointers or decide where provenance
+lives in a pointer's representation. Pointer-bearing byte operations remain
+unsupported. Typed copies still require the treatment described in
+[the lowering audit](LOWERING_AUDIT.md), including
+[Aeneas issue #1405](https://github.com/AeneasVerif/aeneas/issues/1405).
+
+Byte-cast reasoning uses the existing distinction between language validity and
+optional mathematical admission. The source's `IntoBytes` law ranges over all
+accepted language representations, regardless of mathematical admission. The
+destination's intended `FromBytes` law must accept every initialized storage of
+the correct width at both stages. The shared cast lemma composes these laws for
+arbitrary represented bytes. It supplies no encoder and does not claim that a
+particular Rust transmutation follows this interpretation.
+
+The concrete `check_u32_slice_known_layout` Rust harness checks the actual
+`<[u32] as KnownLayout>::LAYOUT` initializer, its descriptor fields, and sizing
+for every element count, including checked-multiplication overflow. Admission
+visits the local constant's initializer body; no axiom supplies the descriptor.
+The visible guards expose the power-of-two and size-divisibility premises of
+the ABI reads. This checks that concrete numerical behavior, not the complete
+generic trait invariant. The proof also rejects an initializer changed from
+`for_slice` to `for_type`.
+
+The native capability fixtures under `tests/capabilities/` preserve the next
+translation boundaries. With the current pins, the generic `KnownLayout`
+fixture retains an associated-type equality that Aeneas rejects. A second
+fixture without an explicit caller-side equality fails on the trait's own
+`MaybeUninit` metadata equality. The production
+`transmute!` fixture retains its compile-time trait-check helper and a loop that
+Aeneas rejects. The required `FromBytes` declaration dependencies additionally
+reach the unsupported recursive `Invariants`/`Alignment` group. These failures
+are not successful extraction or completed Rust proofs. Do not delete bounds,
+equalities, or required declarations to make those targets extract. Required
+recursive declaration support is deferred; dependent work must wait for tools
+that support it.
+
+Native raw-pointer emission has a separate limitation. The pinned backend's
+carrier stores only `v : T`, and its scalar pointer cast returns `undef`.
+Emitted slice construction and `NonNull` operations remain external templates.
+The mathematical pointer model does not repair that carrier or grant admission
+to those operations. The existing checker continues to reject them. A faithful
+carrier and checked primitive interpretations are prerequisites for proving
+their address, metadata, or provenance behavior.
+
+When those boundaries are supported, bind `KnownLayout::LAYOUT` to the original
+Rust type and its metadata-indexed geometry. Reuse the complete recursive
+layout semantics, which preserves an inner field's padding before outer
+rounding. Preserve physical tail offset, stride, alignment, and conservative
+padding flags. Keep mathematical extent, `usize` representability, and the
+`isize` object-size restriction separate. The `MaybeUninit` obligation also
+requires identical metadata and layout and acceptance of uninitialized storage
+in every position; a layout-only theorem must not be presented as the full
+trait invariant.
+
+Concrete owned conversions use the actual standard transmute primitive for
+`u32` and four-byte arrays, plus a guarded `u8`-to-`bool` conversion. These types
+have no pointers, resources, destruction, or external-state invariants. Original
+Rust endpoint checks and a compiled canonical-provider audit restrict that
+interpretation to those cases; it does not admit the production macro or an
+arbitrary generic transmute. Invalid Boolean encodings take the forbidden path,
+even with postcondition `True`. Reference creation remains a later target because
+numerical geometry and provenance presence alone do not supply permissions or
+lifetimes. Derive
+proof requests are also deferred. Existing annotation discovery, native binding
+records, independent golden/live proofs, and dependency audits remain the sole
+route to reporting a Rust specification as checked; these foundations add no
+parallel coverage registry or automatic Rust ABI assumptions.
+
+### Other deferred decisions
+
 - **Canonical layout abstraction.** Retain structural `DstLayout` and existing
   `ModelViews` initially. Padding and trailing-size pilots already use those
   views. Use `extend`, sequence queries, and capacity contracts to compare total
@@ -325,8 +411,8 @@ the library already models every part of Rust's abstract machine.
   tactics, and the existing loop adapter. Introduce a larger lifting DSL,
   per-model tactics, or new loop abstraction only after concrete repeated
   failures show a net benefit over ordinary lemmas and a thin tactic.
-- **Broader carriers and effects.** Recursive nominal groups, indexed carriers,
-  const generics, associated-type trait laws, higher-ranked bounds, bounded
+- **Broader carriers and effects.** Recursive nominal groups, general indexed
+  carriers, const generics, associated-type trait laws, higher-ranked bounds, bounded
   nominal models, and escaping borrow reconstruction remain unsupported with
   explicit errors. The first trait-law bridge supports `Self`-only traits and
   simple generic bounds, with `Unaligned` and a total byte codec as checked
@@ -338,11 +424,12 @@ the library already models every part of Rust's abstract machine.
   execution, independently of ordinary library-model admission. A storage model
   must account for the translation's omissions as well as its primitives. The
   [pinned lowering audit](LOWERING_AUDIT.md) records known omissions and the
-  additional admission checks needed before making memory-safety claims.
-  [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) specifies the proposed closed
+  admission checks needed before making memory-safety claims.
+  [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) specifies the closed
   dependency traversal, controlled build origins using Charon's existing MIR
-  preservation setup, primitive rules, and mandatory CI path. These additional
-  checks are not implemented yet.
+  preservation setup, primitive rules, and mandatory CI path. CI enforces
+  these checks for the admitted fragment; extending that fragment requires
+  corresponding operation semantics and coverage checks.
   <!-- FIXME: Typed transfers lose storage events; track support at
   https://github.com/AeneasVerif/aeneas/issues/1405. Until then, a typed storage
   abstraction must forget all padding contents and initialization facts. It

verification/aeneas/README.md

@@ -390,6 +390,10 @@ padding inside packed fields.
 A positive size-sequence comparison establishes equal sizes for every natural
 metadata value; a negative result does not assert that the sequences differ.
 
+Cast validation and exact metadata inference establish error priority, exact
+splits and rejection of unattainable sizes. Intentional zero-stride panic is
+checked separately.
+
 Plain arithmetic clauses use mathematical word values carrying machine bounds
 and, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping
 raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary