Prove primitive layout constructors with recursive mathematical models

verification/aeneas/README.md

@@ -114,28 +114,29 @@ postconditions could promise less. Passing proofs establish the written claims;
 they do not establish that those claims capture the intended behavior.
 
 The comments in these modules explain their inputs, outputs, and non-obvious
-checks. This integration proves conditional functional
+checks. [SEMANTICS.md](SEMANTICS.md) states the premise connecting the independent
+layout mathematics to Rust. This integration proves conditional functional
 behavior; it does not prove that every caller meets the requirements or that
 zerocopy's unsafe pointer operations are sound.
 
 ## 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. Every present
 fence must have a supported Rust owner, exact extraction binding, and the
 corresponding checked Lean declarations. Unannotated functions and impls can be
 added without extending the specification set.
 
-| Rust function | Checked property |
+| Functions | Checked property |
 | --- | --- |
 | Byteorder U16/U32 read, write, and set (both endiannesses) | Exact integer value, every encoded byte, and setter/getter equality for every typed input. |
-| `max` | Returns the mathematical maximum, selects an input, and bounds both inputs from above. |
-| `min` | Returns the mathematical minimum, selects an input, and bounds both inputs from below. |
-| `padding_needed_for` | For power-of-two alignment, returns padding below it and exactly `(align - len % align) % align`, the least padding making the sum aligned, with zero padding exactly when the input is aligned. |
-| `round_down_to_next_multiple_of_alignment` | For power-of-two alignment, returns exactly `n - n % align`, the greatest aligned value at most `n`; the next multiple exceeds `n`. |
+| `max`, `min`, padding, round-down | Exact extrema, least padding, greatest aligned predecessor, and bounds. |
 | Alignment/phase encoder and decoders | Power-of-two alignment, bounded phase, and exact encoding round-trip. |
+| `DstLayout::{assume_shallow_unpadded,new_zst,for_type,for_unpadded_type,for_slice}` | Exact alignment, size-information fields, and recorded shallow-padding flags under explicit input premises. |
+| `SizeInfo::try_to_nonzero_elem_size`, `max_elems_for_bytes` | Exact zero handling, preserved representation fields, and greatest fitting element count. |
+| `DstLayout::requires_static_padding` | Exact negation of the recorded shallow-unpadded flag. |
 
 Every registered function uses total `spec`: accepted raw representations,
 supplied mathematical ghosts, and explicit requirements imply successful
@@ -158,6 +159,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 NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw
 clauses preserve the extracted representation vocabulary while retaining
@@ -362,8 +369,10 @@ These are conditional contracts over accepted representations, supplied ghosts,
 and satisfied requirements. A decoder may intentionally forget observations or
 reject raw values. A ghost with type `False`, or a dependent ghost with an empty
 domain, makes the relevant contract vacuous. Neither the pipeline nor a decoder
-proves that every Rust caller meets the domain. Operation-specific
-alignment and fit conditions remain explicit. The independently written operation expectations check both intended input
+proves that every Rust caller meets the domain. `DstLayout` initially keeps a
+structural mathematical model, including its unpadded flag and decoded rounding
+pair, without imposing a global realizable-layout requirement. Operation-specific
+alignment, fit, and construction conditions remain explicit. The independently written operation expectations check both intended input
 admission and promised behavior. Representation laws can be useful proof helpers;
 they are not an additional universal model-certification requirement.
 
@@ -462,6 +471,12 @@ declarations from every handwritten Lean module, including unused auxiliary
 modules, together with the model, vocabulary, obligations, and generated
 specifications. Only `propext`, `Classical.choice`, and `Quot.sound` are
 permitted.
+The explicit data-only Rust layout inputs documented in `SEMANTICS.md`
+are also permitted. Models with generic alignment reads must provide both
+data inputs with their exact signatures; the audit also checks that generic
+size/alignment reads use those inputs and that `Usize` size uses the pointer
+width. These checks pin the declared external interpretation; correspondence
+to the actual Rust ABI remains an explicit premise.
 New axioms, `sorryAx`, and native evaluator proof axioms fail.
 
 Callers reuse ordinary exported theorems, either explicitly with `step with` or

verification/aeneas/SEMANTICS.md

@@ -0,0 +1,151 @@
+<!-- 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.
+
+## 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.