Prove primitive DstLayout constructors

verification/aeneas/README.md

@@ -262,7 +262,7 @@ whole-program unsafe-code certification.
 
 ## Scope and proofs
 
-Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs).
+Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs).
 
 Extraction starts from the function and nominal-type owners of every present
 `aeneas` fence in `zerocopy/src`, including their dependencies. The current
@@ -346,6 +346,12 @@ alignment and bounded phase with machine-fit proofs. Ordinary representation
 laws establish acceptance of every positive stored word and exact reconstruction
 from that pair. Zero is rejected by the native NonZero child decoder.
 
+`LayoutModel.lean` supplies raw observations and projections of the recursively
+decoded records without function proofs. Layout models retain each field and
+the unpadded flag; realizability, alignment and fit conditions remain explicit.
+Generic size/alignment reads are external data inputs, not correctness axioms.
+See [SEMANTICS.md](SEMANTICS.md) for the Rust correspondence premise.
+
 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

verification/aeneas/SEMANTICS.md

@@ -0,0 +1,203 @@
+<!-- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -->
+
+# Layout semantics and the Rust boundary
+
+`lean/LayoutMath.lean` defines layout independently of the Rust implementation.
+Its recursive `Description.size` places a complete inner field at an aligned
+offset, then rounds the enclosing record's size. Every level retains the
+inner field's own padding. `Description.offset` tracks the physical slice
+offset separately from the size calculation.
+
+The compilation theorem is parametric in nesting depth and slice metadata.
+For a leaf whose element size is divisible by its alignment,
+`compile_size` proves that normalization into a `Formula` preserves size for
+every metadata value. `compile_offset` and `compile_elem` preserve physical
+offset and element stride; `compiled_contains_tail` proves that the full size
+contains those physical bytes. These statements use unbounded `Nat`
+arithmetic and do not assume that the result fits a machine integer.
+
+The normalization target describes size as
+`base + roundUp (phase + metadata * elem) align`. Neither `base + phase` nor
+the method called `size_offset` is generally the physical slice offset.
+`pad_size` proves the two alignment-order cases of rounding a normalized
+formula, and `advance_size` proves byte advancement independently of the
+physical offset. `capacity_spec` and `maximal_metadata` account for plateaus:
+several different metadata values can have the same complete padded size.
+
+`recordState` separately evaluates declaration-order field placement for each
+metadata value. It uses each field's complete size, without manipulating the
+normalization's base, phase, or size alignment. `recordState_refinement` proves
+that the normalized prefix fold agrees with this direct rule for arbitrary
+field lists in the construction domain. These are mathematical theorems. The contracts at this stage do not
+establish conformance of an extracted record constructor to this rule.
+
+## Explicit Rust premise
+
+The mathematical statements do not certify a compiler implementation. Their
+application to Rust assumes the following bridge for the exact compiler,
+target, features, and type instantiation used for extraction or a regression
+test:
+
+1. Element size and alignment inputs equal Rust's `size_of` and `align_of`
+   results; alignment is a positive power of two, and element size is a
+   multiple of it. Slice metadata counts elements with this stride.
+2. A `repr(C)` record places fields in declaration order, aligning the next
+   field's offset and adding its complete size. The record is finally rounded
+   to its own alignment. Packing caps field placement alignment; explicit
+   alignment raises the record's alignment. Neither changes an inner field's
+   complete size or internal padding.
+3. An accepted type instantiation with generic indirection around a packed
+   field follows the same recursive rule, including when an inner type has an
+   explicit alignment. Continued acceptance of this otherwise prohibited
+   transitive combination is a compatibility premise, not a Reference theorem.
+4. The descriptor inputs correspond to the actual fields and representation
+   modifiers. Bounds required by each extracted contract hold, including
+   machine overflow checks and the compiler's allowed alignment range. Object
+   creation and pointer operations additionally require their own Rust safety
+   contracts; a numerical layout theorem does not establish these contracts.
+
+The versioned [Rust 1.93 layout Reference](https://doc.rust-lang.org/1.93.0/reference/type-layout.html)
+provides the source of the ordinary layout rules. In particular,
+`layout.repr.inter-field` says that an outer representation
+"does not change the layout of the fields themselves". The sections
+`layout.properties.align`, `layout.properties.size`, `layout.array`,
+`layout.slice`, `layout.repr.c.struct.size-field-offset`, and
+`layout.repr.alignment` supply the other rules. Applying these rules to the
+pinned extraction compiler and other tested compilers is an explicit
+compatibility premise. Sparse compiler tests do not prove compatibility for
+an interval of compiler versions or for an untested target.
+
+The packed regression has complete size 10 at metadata zero, whereas the old
+flattened calculation yields 8. `packed_regression` checks this witness in
+Lean. Compiler regression tests independently compare actual Rust layouts
+with the candidate recursive rule; their role is to challenge the bridge,
+not to replace the universal algebra proof.
+
+## External inputs and trust
+
+Aeneas erases ABI layout information from generic Rust type parameters.
+`Zerocopy.RustLayout.size` and `Zerocopy.RustLayout.align` are therefore
+uninterpreted **data inputs**, each of type `Type → Usize`. No proposition
+about their values is an axiom. The constructors' contracts explicitly
+require the relevant primitive reads and alignment properties. The audit
+admits exactly these two names and verifies their signatures. Changing an
+input to a proposition, or adding another axiom, fails the audit.
+
+The primitive correspondence applies to the selected Rust type instantiation;
+Lean's erased type alone is not an ABI descriptor. If distinct Rust types erase
+to the same Lean type, each constructor theorem still needs its own primitive
+read premise. Combining incompatible ABI interpretations into a single
+instantiation is not justified by the data-input model.
+
+The `usize` size used to calculate pointer width is modeled separately as
+the selected word width divided by eight. The extracted scalar model
+supports 32- and 64-bit words. `NonZero::new` is modeled for the `Usize`
+instantiations actually extracted: zero returns `None`, and a nonzero input
+returns that input without changing its bits. `NonZero::get` returns those
+bits. Lean's representation permits zero in the external wrapper, so contracts
+using mathematical models reject that zero representation through the native
+NonZero decoder. Its mathematical output carries positivity and machine bounds.
+The rounding decoder accepts every positive representable word and decomposes
+it into a power-of-two alignment and bounded phase; structural layout models
+reuse that shared pair. This admission law has an ordinary Lean proof and does
+not change the extracted raw implementation.
+
+The remaining trusted boundary is the pinned Rust-to-LLBC-to-Lean translation,
+its builtin arithmetic and control-flow models, the external primitive
+correspondences above, the Lean kernel, and specification adequacy. Both
+golden and live extraction must independently satisfy the required theorem
+types, axiom audit, and proof dependency checks. Fuzzy textual equivalence
+alone establishes none of these semantic claims.
+
+## Admitted execution and remaining storage limits
+
+The [pinned lowering audit](LOWERING_AUDIT.md) records operations that translation
+ignores or abstracts, including destruction, allocation and physical value
+transfers. A forbidden tag rejects an operation represented in the model; it
+cannot reveal an operation erased before that model was produced.
+
+[ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) describes the implemented restricted
+value-and-borrow fragment. CI checks a preserved promoted-MIR import before
+Charon's transformations, final LLBC, and the complete executable dependency
+closure. Unsupported operations and unregistered opaque calls reject the run.
+Admission is tied to the compiler inputs and the patched runtime; it is not a
+formal certificate of rustc or Aeneas correctness. Valid incoming references,
+reviewed builtin lowering, and registered external interpretations remain
+explicit premises. Boolean production and byte copying exercise two such
+boundaries; they do not establish general storage or provenance semantics.
+
+<!-- FIXME: Exact abstract bytes for general typed values require accounting for
+typed copies: https://github.com/AeneasVerif/aeneas/issues/1405. A restricted
+model can instead forget padding contents and initializedness at all times,
+while retaining access obligations. The current numerical byte-order model
+does not supply this storage semantics. -->
+
+## Mathematical model and ghost domain
+
+`RustModel` associates a raw carrier with a mathematical type and an optional
+decoder. The complete decoder recursively decodes every field before applying
+the inline local decoder. Its accepted domain and retained observations are
+part of the specification. It does not require injectivity, an encoder, or a
+canonical raw representative. Constraints stored as model proof fields must be
+established by safe Lean construction under the same axiom audit as the proofs.
+
+Function contracts execute the original extracted function on the original raw
+arguments. Plain clauses refer to decoded values; `(raw)` clauses refer to the
+corresponding raw inputs and successful payload. Both require accepted inputs
+and successful output decoding. Named requirements are successive premises;
+multiple postconditions are conjunctive. Ordinary ghosts are universally
+quantified in mathematical input context, before requirements and execution.
+Their types may impose premises or be empty. Conditional correctness does not
+establish unconditional caller admission or panic-freedom for such domains.
+
+Automatic providers are fixed from the single verified source/extraction table,
+explicit generic dictionaries, and recursive container combinators. Authored
+instances cannot redirect these retained choices. Model shapes precede support helpers and full decoders; ordinary Lean imports
+must remain acyclic. Raw representations and temporary internal states remain
+unchanged by these mathematical interpretations.
+
+Independent required contracts compare the inline contract with an authored
+expectation for every possible execution outcome, including panic and divergence.
+The comparison preserves input admission, requirements, and postconditions; only
+its execution argument is abstracted. After proving the implication, the checker
+specializes it to the original extracted call and canonical proof. Model proof
+fields establish that successfully constructed mathematical values satisfy their
+constraints. Operation expectations establish what those values mean for the
+verified methods. A separate representation relation is optional proof machinery,
+not a universal requirement. See [DESIGN.md](DESIGN.md) for the full design and
+explicitly deferred decisions.
+
+## Concrete owned standard transmute
+
+The private `util/owned_transmute.rs` entry points call the actual standard
+`core::mem::transmute` operation. Native extraction lowers it to
+`core::intrinsics::transmute`; its external interpretation has an explicit,
+closed implicit provider parameter. The reviewed endpoints are `u32 -> [u8; 4]`,
+`[u8; 4] -> u32`, and `u8 -> bool`. Original compiler evidence retains those
+ordered Rust type arguments. Admission rejects every other instantiation, and
+compiled auditing checks each reached call's canonical provider, including calls
+inside unannotated helpers. It also independently checks the whole primitive
+and provider definitions and the extended primitive signature.
+
+The integer providers encode and decode little-endian bytes. Verification admits
+only the original 64-bit little-endian compiler target and rejects target
+overrides before compilation; the private integer harness module is gated by
+Rust's target-endian configuration. Ordinary nonproof builds remain portable.
+The Boolean provider accepts exactly bytes zero and one and returns `.fail
+.undef` otherwise, before constructing a Boolean. Its validity rule is independent
+of endianness. Discarding an invalid result cannot make a True postcondition hold.
+
+This interpretation relies on the standard transmute contract: both values must
+be valid at their types, equal sizes are checked by Rust, and the operation moves
+the representation. These fixed unsigned scalars and byte arrays accept every
+bit pattern, contain no padding or pointers, and have no destructor. The
+[standard contract](https://doc.rust-lang.org/std/mem/fn.transmute.html) does not
+promise preservation of padding for general by-value types. The interpretation
+supplies no general pointer, provenance, allocation, borrowing, or generic trait
+law, and proves no production `transmute!` macro expansion.