From 227b724e632b62a53850bb26b826759a168fc27b Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 10:41:04 -0400 Subject: [PATCH] Prove primitive DstLayout constructors Connect the primitive, unpadded, slice and empty constructors to the recursive mathematical models. Prove capacity and nonzero-element conversion contracts while retaining useful broader raw statements. Add total Rust assertion harnesses that compare every constructor field with size_of and align_of observations. Keep the alignment guards and modeled ABI inputs explicit, and document the premise connecting those inputs to Rust's actual layouts. Decoding an arbitrary layout does not establish that it describes a realizable Rust type. gherrit-pr-id: Gi4f4vhkj7z3stqqcu5unrzfoqwqp3tuc Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 8 +- verification/aeneas/SEMANTICS.md | 203 ++++++++++++++ verification/aeneas/golden/Funs.lean | 247 +++++++++++++++++- .../aeneas/golden/FunsExternal_Template.lean | 7 + verification/aeneas/golden/Types.lean | 26 +- verification/aeneas/lean/LayoutModel.lean | 119 ++++++++- verification/aeneas/lean/MathViews.lean | 95 ++++++- .../aeneas/lean/ModelProjectionLaws.lean | 74 ++++++ verification/aeneas/lean/Obligations.lean | 112 +++++++- .../aeneas/lean/Proofs/Contracts.lean | 130 ++++++++- .../aeneas/lean/Proofs/PrimitiveChecks.lean | 85 ++++++ .../aeneas/lean/Proofs/Raw/Encoding.lean | 1 + .../aeneas/lean/Proofs/Raw/Layout.lean | 134 ++++++++++ .../aeneas/lean/Proofs/Raw/Trailing.lean | 48 ++++ .../aeneas/lean/RequiredModelContracts.lean | 16 +- .../PrimitiveChecks.lean | 56 ++++ .../aeneas/lean/Zerocopy/FunsExternal.lean | 31 ++- .../aeneas/projections/ModelShapes.lean | 6 + verification/aeneas/projections/Models.lean | 9 + verification/aeneas/projections/Specs.lean | 104 ++++++++ zerocopy/src/layout/mod.rs | 67 +++++ zerocopy/src/layout/primitive_checks.rs | 99 +++++++ 22 files changed, 1651 insertions(+), 26 deletions(-) create mode 100644 verification/aeneas/SEMANTICS.md create mode 100644 verification/aeneas/lean/ModelProjectionLaws.lean create mode 100644 verification/aeneas/lean/Proofs/PrimitiveChecks.lean create mode 100644 verification/aeneas/lean/Proofs/Raw/Layout.lean create mode 100644 verification/aeneas/lean/Proofs/Raw/Trailing.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/PrimitiveChecks.lean create mode 100644 zerocopy/src/layout/primitive_checks.rs diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index f6c6049488..2c1b4e0564 100644 --- a/verification/aeneas/README.md +++ b/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 diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md new file mode 100644 index 0000000000..b831de5c9d --- /dev/null +++ b/verification/aeneas/SEMANTICS.md @@ -0,0 +1,203 @@ + + +# 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. + + + +## 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. diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index c1fadd4f6a..8ebf01c851 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -651,14 +651,14 @@ def byteorder.verification.set_u32_be byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 /-- [zerocopy::layout::POINTER_WIDTH_BITS] - Source: 'src/layout/mod.rs', lines 20:0-20:62 -/ + Source: 'src/layout/mod.rs', lines 23:0-23:62 -/ @[global_simps, irreducible] def layout.POINTER_WIDTH_BITS : Result Std.Usize := do let i ← core.mem.size_of Std.Usize i * 8#usize /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::new]: - Source: 'src/layout/mod.rs', lines 100:4-119:5 -/ + Source: 'src/layout/mod.rs', lines 103:4-122:5 -/ def layout.RoundingAlignAndPhase.new (align : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : @@ -679,7 +679,7 @@ def layout.RoundingAlignAndPhase.new | some encoded1 => ok { _0 := encoded1 } /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]: - Source: 'src/layout/mod.rs', lines 133:4-160:5 -/ + Source: 'src/layout/mod.rs', lines 136:4-163:5 -/ def layout.RoundingAlignAndPhase.components (self : layout.RoundingAlignAndPhase) : Result ((core.num.nonzero.NonZero Std.Usize @@ -707,7 +707,7 @@ def layout.RoundingAlignAndPhase.components ok (align1, phase) /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]: - Source: 'src/layout/mod.rs', lines 173:4-182:5 -/ + Source: 'src/layout/mod.rs', lines 176:4-185:5 -/ def layout.RoundingAlignAndPhase.align (self : layout.RoundingAlignAndPhase) : Result (core.num.nonzero.NonZero Std.Usize @@ -716,6 +716,153 @@ def layout.RoundingAlignAndPhase.align let (nz, _) ← layout.RoundingAlignAndPhase.components self ok nz +/-- [zerocopy::layout::{zerocopy::layout::SizeInfo}::try_to_nonzero_elem_size]: + Source: 'src/layout/mod.rs', lines 791:4-819:5 -/ +def layout.SizeInfoUsize.try_to_nonzero_elem_size + (self : layout.SizeInfo Std.Usize) : + Result (Option (layout.SizeInfo (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner))) + := do + match self with + | layout.SizeInfo.Sized size => ok (some (layout.SizeInfo.Sized size)) + | layout.SizeInfo.SliceDst tsl => + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + tsl.elem_size + match o with + | none => ok none + | some elem_size => + ok (some (layout.SizeInfo.SliceDst + { + offset := tsl.offset, + elem_size, + size_base := tsl.size_base, + size_rounding_align_and_phase := tsl.size_rounding_align_and_phase + })) + +/-- [zerocopy::layout::max_elems_for_bytes]: + Source: 'src/layout/mod.rs', lines 847:0-862:1 -/ +def layout.max_elems_for_bytes + (bytes : Std.Usize) + (elem_size : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) : + Result (Std.Usize × Std.Usize) + := do + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner elem_size + let elems ← bytes / i + let o ← lift (Usize.checked_mul elems i) + match o with + | none => fail panic + | some used => ok (elems, used) + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::MIN_ALIGN] + Source: 'src/layout/mod.rs', lines 882:4-885:6 -/ +@[global_simps, irreducible] +def layout.DstLayout.MIN_ALIGN + : + Result (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) + := do + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner 1#usize + match o with + | none => fail panic + | some min_align => ok min_align + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::assume_shallow_unpadded]: + Source: 'src/layout/mod.rs', lines 951:4-960:5 -/ +def layout.DstLayout.assume_shallow_unpadded + (self : layout.DstLayout) : Result layout.DstLayout := do + ok { self with statically_shallow_unpadded := true } + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::new_zst]: + Source: 'src/layout/mod.rs', lines 989:4-1009:5 + Visibility: public -/ +def layout.DstLayout.new_zst + (repr_align : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) : + Result layout.DstLayout + := do + let align ← + match repr_align with + | none => layout.DstLayout.MIN_ALIGN + | some align1 => ok align1 + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let b ← core.num.Usize.is_power_of_two i + massert b + ok + { + align, + size_info := (layout.SizeInfo.Sized 0#usize), + statically_shallow_unpadded := true + } + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_type]: + Source: 'src/layout/mod.rs', lines 1033:4-1058:5 + Visibility: public -/ +def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do + let i ← core.mem.align_of T + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner i + match o with + | none => fail panic + | some align => + let i1 ← core.mem.size_of T + ok + { + align, + size_info := (layout.SizeInfo.Sized i1), + statically_shallow_unpadded := false + } + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_unpadded_type]: + Source: 'src/layout/mod.rs', lines 1088:4-1102:5 + Visibility: public -/ +def layout.DstLayout.for_unpadded_type + (T : Type) : Result layout.DstLayout := do + let dl ← layout.DstLayout.for_type T + layout.DstLayout.assume_shallow_unpadded dl + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_slice]: + Source: 'src/layout/mod.rs', lines 1127:4-1163:5 -/ +def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do + let i ← core.mem.align_of T + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner i + match o with + | none => fail panic + | some align => + let i1 ← core.mem.size_of T + let raap ← layout.RoundingAlignAndPhase.new align 0#usize + ok + { + align, + size_info := + (layout.SizeInfo.SliceDst + { + offset := 0#usize, + elem_size := i1, + size_base := 0#usize, + size_rounding_align_and_phase := raap + }), + statically_shallow_unpadded := true + } + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::requires_static_padding]: + Source: 'src/layout/mod.rs', lines 1554:4-1563:5 + Visibility: public -/ +def layout.DstLayout.requires_static_padding + (self : layout.DstLayout) : Result Bool := do + ok (¬ self.statically_shallow_unpadded) + /-- [zerocopy::layout::nested_reference::round_up]: Source: 'src/layout/nested_reference.rs', lines 48:0-58:1 -/ def layout.nested_reference.round_up @@ -831,6 +978,98 @@ def layout.nested_reference.size_for_metadata ok (some size) else ok none +/-- [zerocopy::layout::primitive_checks::check_primitive_layouts]: + Source: 'src/layout/primitive_checks.rs', lines 31:0-61:1 -/ +def layout.primitive_checks.check_primitive_layouts + (T : Type) : Result Unit := do + let size ← core.mem.size_of T + let align ← core.mem.align_of T + let b ← core.num.Usize.is_power_of_two align + if b + then + let fixed ← layout.DstLayout.for_type T + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + fixed.align + massert (i = align) + let b1 ← + match fixed.size_info with + | layout.SizeInfo.Sized actual => + if actual = size + then ok true + else ok false + | layout.SizeInfo.SliceDst _ => ok false + massert b1 + massert (¬ fixed.statically_shallow_unpadded) + let unpadded ← layout.DstLayout.for_unpadded_type T + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + unpadded.align + massert (i1 = align) + let b2 ← + match unpadded.size_info with + | layout.SizeInfo.Sized actual => + if actual = size + then ok true + else ok false + | layout.SizeInfo.SliceDst _ => ok false + massert b2 + massert unpadded.statically_shallow_unpadded + let slice ← layout.DstLayout.for_slice T + let i2 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + slice.align + massert (i2 = align) + massert slice.statically_shallow_unpadded + match slice.size_info with + | layout.SizeInfo.Sized _ => fail panic + | layout.SizeInfo.SliceDst tail => + massert (tail.offset = 0#usize) + massert (tail.elem_size = size) + massert (tail.size_base = 0#usize) + let i3 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + tail.size_rounding_align_and_phase._0 + massert (i3 = align) + else ok () + +/-- [zerocopy::layout::primitive_checks::check_empty_layout]: + Source: 'src/layout/primitive_checks.rs', lines 69:0-81:1 -/ +def layout.primitive_checks.check_empty_layout + (repr_align : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) : + Result Unit + := do + let expected_align ← + match repr_align with + | none => ok 1#usize + | some align => + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let b ← core.num.Usize.is_power_of_two expected_align + if b + then + let empty ← layout.DstLayout.new_zst repr_align + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + empty.align + massert (i = expected_align) + let b1 ← + match empty.size_info with + | layout.SizeInfo.Sized i1 => + match i1.val with + | 0 => ok true + | _ => ok false + | layout.SizeInfo.SliceDst _ => ok false + massert b1 + massert empty.statically_shallow_unpadded + else ok () + /-- [zerocopy::FromZeros::new_zeroed]: Source: 'src/lib.rs', lines 3827:4-3833:5 Visibility: public -/ diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index ec8aee01f2..76ecc41466 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -42,6 +42,13 @@ axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst @[rust_fun "core::mem::size_of"] axiom core.mem.size_of (T : Type) : Result Std.Usize +/-- [core::mem::align_of]: + Source: '/rustc/library/core/src/mem/mod.rs', lines 543:0-543:35 + Name pattern: [core::mem::align_of] + Visibility: public -/ +@[rust_fun "core::mem::align_of"] +axiom core.mem.align_of (T : Type) : Result Std.Usize + /-- [core::mem::zeroed]: Source: '/rustc/library/core/src/mem/mod.rs', lines 755:0-755:36 Name pattern: [core::mem::zeroed] diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 0c9a04890f..a702da6d51 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -178,11 +178,35 @@ structure byteorder.F64 (O : Type) where _1 : core.marker.PhantomData O /-- [zerocopy::layout::RoundingAlignAndPhase] - Source: 'src/layout/mod.rs', lines 81:0-81:54 -/ + Source: 'src/layout/mod.rs', lines 84:0-84:54 -/ structure layout.RoundingAlignAndPhase where _0 : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner +/-- [zerocopy::layout::TrailingSliceLayout] + Source: 'src/layout/mod.rs', lines 191:0-245:1 -/ +structure layout.TrailingSliceLayout (E : Type) where + offset : Std.Usize + elem_size : E + size_base : Std.Usize + size_rounding_align_and_phase : layout.RoundingAlignAndPhase + +/-- [zerocopy::layout::SizeInfo] + Source: 'src/layout/mod.rs', lines 53:0-56:1 -/ +@[discriminant isize] +inductive layout.SizeInfo (E : Type) where +| Sized : Std.Usize → layout.SizeInfo E +| SliceDst : layout.TrailingSliceLayout E → layout.SizeInfo E + +/-- [zerocopy::layout::DstLayout] + Source: 'src/layout/mod.rs', lines 40:0-48:1 + Visibility: public -/ +structure layout.DstLayout where + align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner + size_info : layout.SizeInfo Std.Usize + statically_shallow_unpadded : Bool + /-- [zerocopy::layout::nested_reference::NestedLayer] Source: 'src/layout/nested_reference.rs', lines 29:0-33:1 -/ structure layout.nested_reference.NestedLayer where diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean index adc6a518f7..1e6e647a76 100644 --- a/verification/aeneas/lean/LayoutModel.lean +++ b/verification/aeneas/lean/LayoutModel.lean @@ -9,25 +9,128 @@ those terms. -/ module public import Zerocopy.Funs public import SpecPrelude +public import MathViews public import LayoutMath @[expose] public section /-! -Extracted trailing records contain machine words and compressed rounding -encodings. This module interprets those records as an unbounded complete-size -formula and a separately observed physical slice offset. Its definitions do -not call an extracted operation or assume that an operation is correct. - -Keeping physical offset separate from normalized base and phase is essential: -inner padding can make them differ. Operation proofs use these observations -to connect extracted arithmetic with the independent layout mathematics. +Extracted records contain machine words and compressed rounding encodings. +This module gives those records ordinary mathematical observations: a size +formula, a physical slice offset, and field placement. The definitions do not +call an extracted operation or assume that it is correct. + +Proofs uses the raw observations to state implementation lemmas and +independent expectations. ModelViews exposes corresponding observations of +recursively decoded mathematical records for inline clauses. +ModelProjectionLaws proves the connection when decoding succeeds. Keeping +physical offset separate from normalized base and phase is essential: inner +padding can make them differ. -/ open Aeneas Aeneas.Std namespace Zerocopy.Proofs +/- Read the raw trailing record as a complete-size formula over byte counts. The +compressed word determines alignment and phase; physical offset is retained. +-/ +def byteFormula {E : Type} (self : layout.TrailingSliceLayout E) : LayoutMath.Formula := + let code := self.size_rounding_align_and_phase._0.val.val + let align := 2 ^ Nat.log2 code + ⟨self.size_base.val, code - align, align, 0, self.offset.val⟩ + +/- Specialize the byte formula to the raw element stride used by usize metadata. +-/ +def trailingFormula (self : layout.TrailingSliceLayout Usize) : LayoutMath.Formula := + { byteFormula self with elem := self.elem_size.val } + +/- An absent packing bound acts as the largest representable power of two. The +alignment domain bounds ensure that taking the minimum leaves an admitted +field alignment unchanged in that case. +-/ +def packingValue (packed : Option NonZeroUsize) : Nat := + (packed.map (fun a => a.val.val)).getD (2 ^ (System.Platform.numBits - 1)) + +def fieldAlignment (field : layout.DstLayout) (packed : Option NonZeroUsize) : Nat := + min field.align.val.val (packingValue packed) + +/- Round the current fixed size to the field's effective placement alignment. +-/ +def placement (size : Usize) (field : layout.DstLayout) (packed : Option NonZeroUsize) := + LayoutMath.roundUp size.val (fieldAlignment field packed) + +/- Project the raw record to the fragment vocabulary used by layout operations. +This preserves alignment, payload, physical offset, stride, and unpadded +flag. +-/ +def layoutValue (self : layout.DstLayout) : LayoutMath.LayoutValue := + { align := self.align.val.val, + payload := match self.size_info with + | .Sized size => .fixed size.val + | .SliceDst tail => .trailing (trailingFormula tail), + unpadded := self.statically_shallow_unpadded } + +/- Require the nonzero compressed rounding word in a trailing payload. Sized +fragments have no rounding encoding to validate. +-/ +def canonicalLayout (self : layout.DstLayout) : Prop := + match self.size_info with + | .Sized _ => True + | .SliceDst t => 0 < t.size_rounding_align_and_phase._0.val.val + +/- The selected Rust layout premise bounds power-of-two alignments at 2^29. This +is an explicit operation domain, not a consequence of NonZeroUsize alone. +-/ +def alignmentDomain (a : Nat) : Prop := a.isPowerOfTwo ∧ a ≤ 2 ^ 29 end Zerocopy.Proofs +-- Mathematical projections consume the one recursively decoded record. The +-- raw projections above remain for independently stated representation claims. +namespace Zerocopy.ModelViews +open AeneasSpecs + +/- Read the decoded mathematical trailing record as a complete-size formula over +byte counts. Alignment and phase have already been decoded; physical offset +remains a separate observation. +-/ +def byteFormula {EModel : Type} + (self : layout.TrailingSliceLayout.Fields EModel) : LayoutMath.Formula := + let rounding := self.size_rounding_align_and_phase + ⟨self.size_base.value, rounding.phase, rounding.align, 0, self.offset.value⟩ + +/- Specialize the byte formula to the decoded bounded element stride used by +usize metadata. +-/ +def trailingFormula (self : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize)) : LayoutMath.Formula := + { byteFormula self with elem := self.elem_size.value } + +/- An absent packing bound acts as the largest representable power of two. The +alignment domain bounds ensure that taking the minimum leaves an admitted +field alignment unchanged in that case. +-/ +def packingValue (packed : Option NonZeroUsizeValue) : Nat := + (packed.map (fun a => a.value)).getD (2 ^ (System.Platform.numBits - 1)) + +def fieldAlignment (field : layout.DstLayout.Fields) (packed : Option NonZeroUsizeValue) : Nat := + min field.align.value (packingValue packed) + +/- Round the current fixed size to the field's effective placement alignment. +-/ +def placement (size : UnsignedWord .Usize) (field : layout.DstLayout.Fields) + (packed : Option NonZeroUsizeValue) : Nat := + LayoutMath.roundUp size.value (fieldAlignment field packed) + +/- Project the decoded record to the fragment vocabulary used by layout +operations, preserving alignment, payload, physical offset, stride and flag. +-/ +def layoutValue (self : layout.DstLayout.Fields) : LayoutMath.LayoutValue := + { align := self.align.value, + payload := match self.size_info with + | .Sized size => .fixed size.value + | .SliceDst tail => .trailing (trailingFormula tail), + unpadded := self.statically_shallow_unpadded } + +end Zerocopy.ModelViews + namespace Zerocopy.Proofs.NestedReference /- The independent recursive rule uses unbounded arithmetic and complete diff --git a/verification/aeneas/lean/MathViews.lean b/verification/aeneas/lean/MathViews.lean index 81ad558122..ff28890d68 100644 --- a/verification/aeneas/lean/MathViews.lean +++ b/verification/aeneas/lean/MathViews.lean @@ -37,6 +37,17 @@ set_option linter.unusedSimpArgs false def encodingValid (code : layout.RoundingAlignAndPhase) : Prop := 0 < code._0.val.val +def trailingValid {E : Type} [RustModel E] (tail : layout.TrailingSliceLayout E) : Prop := + isValid tail.elem_size ∧ encodingValid tail.size_rounding_align_and_phase + +def sizeInfoValid {E : Type} [RustModel E] (info : layout.SizeInfo E) : Prop := + match info with + | .Sized _ => True + | .SliceDst tail => trailingValid tail + +def layoutValid (self : layout.DstLayout) : Prop := + 0 < self.align.val.val ∧ sizeInfoValid self.size_info + @[contract_simps] theorem admission_eq {Raw : Type u} (provider : RustModel Raw) (raw : Raw) : (∃ value, provider.decode raw = some value) = @isValid Raw provider raw := rfl @@ -78,6 +89,37 @@ def encodingValid (code : layout.RoundingAlignAndPhase) : Prop := layout.RoundingAlignAndPhase.decode, layout.RoundingAlignAndPhase.decodeFields, modelNonZeroUScalar, hp, encodingValid] +@[simp, contract_simps] theorem trailing_valid_iff {E : Type} [RustModel E] + (tail : layout.TrailingSliceLayout E) : isValid tail ↔ trailingValid tail := by + change (∃ value, layout.TrailingSliceLayout.decode E tail = some value) ↔ _ + unfold trailingValid + simp only [layout.TrailingSliceLayout.decode, layout.TrailingSliceLayout.decodeFields, + decodeUScalar, admitted_bind, admitted_some, + and_true, true_and, option_decoded_post_iff, admission_eq, encoding_valid_iff] + change (isValid tail.elem_size ∧ isValid tail.size_rounding_align_and_phase) ↔ _ + rw [encoding_valid_iff] + +@[simp, contract_simps] theorem size_info_valid_iff {E : Type} [RustModel E] + (info : layout.SizeInfo E) : isValid info ↔ sizeInfoValid info := by + change (∃ value, layout.SizeInfo.decode E info = some value) ↔ _ + cases info <;> + simp only [layout.SizeInfo.decode, layout.SizeInfo.decodeFields, + decodeUScalar, admitted_bind, admitted_some, + and_true, true_and, admission_eq, sizeInfoValid, trailing_valid_iff] + change isValid _ ↔ _ + exact trailing_valid_iff _ + +@[simp, contract_simps] theorem layout_valid_iff (self : layout.DstLayout) : + isValid self ↔ layoutValid self := by + change (∃ value, layout.DstLayout.decode self = some value) ↔ _ + unfold layoutValid + simp only [layout.DstLayout.decode, layout.DstLayout.decodeFields, + admitted_bind, admitted_some, and_true, + option_decoded_post_iff, admission_eq, nonzero_valid_iff, size_info_valid_iff, + bool_valid_iff] + change (isValid self.align ∧ isValid self.size_info ∧ isValid self.statically_shallow_unpadded) ↔ _ + simp only [nonzero_valid_iff, size_info_valid_iff, bool_valid_iff, and_true] + @[contract_simps] theorem scalar_admitted_iff (x : UScalar ty) : (∃ value, RustModel.decode x = some value) ↔ True := scalar_valid_iff x @@ -87,6 +129,15 @@ def encodingValid (code : layout.RoundingAlignAndPhase) : Prop := @[contract_simps] theorem encoding_admitted_iff (x : layout.RoundingAlignAndPhase) : (∃ value, RustModel.decode x = some value) ↔ encodingValid x := encoding_valid_iff x +@[contract_simps] theorem trailing_admitted_iff {E : Type} [RustModel E] (x : layout.TrailingSliceLayout E) : + (∃ value, RustModel.decode x = some value) ↔ trailingValid x := trailing_valid_iff x + +@[contract_simps] theorem size_info_admitted_iff {E : Type} [RustModel E] (x : layout.SizeInfo E) : + (∃ value, RustModel.decode x = some value) ↔ sizeInfoValid x := size_info_valid_iff x + +@[contract_simps] theorem layout_admitted_iff (x : layout.DstLayout) : + (∃ value, RustModel.decode x = some value) ↔ layoutValid x := layout_valid_iff x + @[contract_simps] theorem bool_admitted_iff (x : Bool) : (∃ value, RustModel.decode x = some value) ↔ True := bool_valid_iff x @@ -103,16 +154,58 @@ def encodingValid (code : layout.RoundingAlignAndPhase) : Prop := (∃ value, layout.RoundingAlignAndPhase.decode raw = some value) ↔ encodingValid raw := encoding_valid_iff raw +@[contract_simps] theorem trailing_decoder_admitted_iff {E : Type} [RustModel E] + (raw : layout.TrailingSliceLayout E) : + (∃ value, layout.TrailingSliceLayout.decode E raw = some value) ↔ + trailingValid raw := trailing_valid_iff raw + +@[contract_simps] theorem size_info_decoder_admitted_iff {E : Type} [RustModel E] (raw : layout.SizeInfo E) : + (∃ value, layout.SizeInfo.decode E raw = some value) ↔ + sizeInfoValid raw := size_info_valid_iff raw + +@[contract_simps] theorem layout_decoder_admitted_iff (raw : layout.DstLayout) : + (∃ value, layout.DstLayout.decode raw = some value) ↔ + layoutValid raw := layout_valid_iff raw + @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) : Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff attribute [contract_simps] option_valid_iff prod_valid_iff result_valid_iff attribute [contract_simps] and_true true_and and_self true_implies forall_true_iff -attribute [contract_simps] encodingValid +attribute [contract_simps] encodingValid trailingValid sizeInfoValid layoutValid @[simp, contract_simps] theorem rounding_model_decode_eq (raw : layout.RoundingAlignAndPhase) : RustModel.decode raw = layout.RoundingAlignAndPhase.decode raw := rfl +@[simp, contract_simps] theorem trailing_model_decode_eq {E : Type} [RustModel E] + (raw : layout.TrailingSliceLayout E) : + RustModel.decode raw = layout.TrailingSliceLayout.decode E raw := rfl + +@[simp, contract_simps] theorem size_info_model_decode_eq {E : Type} [RustModel E] + (raw : layout.SizeInfo E) : + RustModel.decode raw = layout.SizeInfo.decode E raw := rfl + +@[simp, contract_simps] theorem layout_model_decode_eq (raw : layout.DstLayout) : + RustModel.decode raw = layout.DstLayout.decode raw := rfl + +-- A named decoder can also occur after a surrounding structural traversal +-- exposes the retained dictionary. These are the same admission equivalences. +@[contract_simps] theorem trailing_usize_admitted_iff + (raw : layout.TrailingSliceLayout Usize) : + (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize), + RustModel.decode raw = some value) ↔ + 0 < raw.size_rounding_align_and_phase._0.val.val := by + simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using + trailing_admitted_iff raw + +-- Optional traversal exposes the same fixed provider's named decoder directly. +@[contract_simps] theorem trailing_usize_decoder_admitted_iff + (raw : layout.TrailingSliceLayout Usize) : + (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize), + layout.TrailingSliceLayout.decode Usize raw = some value) ↔ + 0 < raw.size_rounding_align_and_phase._0.val.val := + trailing_usize_admitted_iff raw + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/ModelProjectionLaws.lean b/verification/aeneas/lean/ModelProjectionLaws.lean new file mode 100644 index 0000000000..2e6cfb0b1f --- /dev/null +++ b/verification/aeneas/lean/ModelProjectionLaws.lean @@ -0,0 +1,74 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import LayoutModel +public import RepresentationLaws +@[expose] public section + +/-! +Inline layout specifications use decoded mathematical records. Existing raw +proofs and independently written expectations use extracted records. These +lemmas connect their observations when the chosen provider decodes +successfully. They preserve physical offsets, stride, flags, and the inner +rounding encoding; an equality of total sizes alone would not retain those +promises. + +The lemmas are tools for particular operation proofs and adequacy checks. +They are not universal assumptions that arbitrary decoders preserve all raw +data. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +theorem byteFormula_decode {E : Type} [RustModel E] + (raw : layout.TrailingSliceLayout E) (value : layout.TrailingSliceLayout.Fields (ModelOf E)) + (h : layout.TrailingSliceLayout.decode E raw = some value) : + ModelViews.byteFormula value = byteFormula raw := by + have fields := (layout.TrailingSliceLayout.decode_decompose E raw value).mp h + simp only [layout.TrailingSliceLayout.decodeFields, decodeUScalar, + Option.some.injEq] at fields + rcases fields with ⟨offset, rfl, elem, _, base, rfl, rounding, hr, rfl⟩ + obtain ⟨ha, hp⟩ := rounding_decode_components raw.size_rounding_align_and_phase rounding hr + simp only [ModelViews.byteFormula, byteFormula, unsignedWord_value, ha, hp] + +theorem trailingFormula_decode (raw : layout.TrailingSliceLayout Usize) + (value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize)) + (h : layout.TrailingSliceLayout.decode Usize raw = some value) : + ModelViews.trailingFormula value = trailingFormula raw := by + have hb := byteFormula_decode raw value h + have fields := (layout.TrailingSliceLayout.decode_decompose Usize raw value).mp h + simp only [layout.TrailingSliceLayout.decodeFields, decodeUScalar, + Option.some.injEq] at fields + rcases fields with ⟨offset, rfl, elem, rfl, base, rfl, rounding, _, rfl⟩ + simp only [ModelViews.trailingFormula, trailingFormula, hb, unsignedWord_value] + +theorem layoutValue_decode (raw : layout.DstLayout) (value : layout.DstLayout.Fields) + (h : layout.DstLayout.decode raw = some value) : + ModelViews.layoutValue value = layoutValue raw := by + have fields := (layout.DstLayout.decode_decompose raw value).mp h + simp only [layout.DstLayout.decodeFields, Option.some.injEq] at fields + rcases fields with ⟨align, ha, info, hi, flag, hf, rfl⟩ + have hva := (decodeNonZeroUScalar_iff raw.align align).mp ha + change some raw.statically_shallow_unpadded = some flag at hf + cases Option.some.inj hf + have infoFields := (layout.SizeInfo.decode_decompose Usize raw.size_info info).mp hi + cases hs : raw.size_info with + | Sized size => + simp only [hs, layout.SizeInfo.decodeFields, decodeUScalar, + Option.some.injEq] at infoFields + rcases infoFields with ⟨size, rfl, rfl⟩ + simp only [ModelViews.layoutValue, layoutValue, hs, unsignedWord_value, hva] + | SliceDst tail => + simp only [hs, layout.SizeInfo.decodeFields, decodeUScalar, + Option.some.injEq] at infoFields + rcases infoFields with ⟨tailValue, ht, rfl⟩ + simp only [ModelViews.layoutValue, layoutValue, hs, hva, + trailingFormula_decode tail tailValue ht] + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index e2b5a5aa10..c64720befa 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -7,10 +7,6 @@ This file may not be copied, modified, or distributed except according to those terms. -/ module -public import Zerocopy.Funs -public import SpecPrelude -public import MathViews -public import Arithmetic public import LayoutModel @[expose] public section @@ -130,6 +126,95 @@ def encoding_align_spec : Prop := ∀ (code : layout.RoundingAlignAndPhase), encoding_align_spec_contract code (layout.RoundingAlignAndPhase.align code) +def try_nonzero_spec_contract (si : layout.SizeInfo Usize) + (run : Result (Option (layout.SizeInfo NonZeroUsize))) : Prop := + sizeInfoValid si → run ⦃ r => (∀ next ∈ r, sizeInfoValid next) ∧ + match si with + | .Sized bytes => r = some (.Sized bytes) + | .SliceDst t => if t.elem_size = 0#usize then r = none else + ∃ next, r = some (.SliceDst next) ∧ next.offset = t.offset ∧ next.size_base = t.size_base ∧ + next.size_rounding_align_and_phase = t.size_rounding_align_and_phase ∧ + next.elem_size.val = t.elem_size ⦄ + +def try_nonzero_spec : Prop := + ∀ (si : layout.SizeInfo Usize), + try_nonzero_spec_contract si (layout.SizeInfoUsize.try_to_nonzero_elem_size si) + +def max_elems_for_bytes_spec_contract (budget : Usize) (stride : NonZeroUsize) + (run : Result (Usize × Usize)) : Prop := + 0 < stride.val.val → + run ⦃ (n, bytes) => + n.val = budget.val / stride.val.val ∧ bytes.val = n.val * stride.val.val ∧ + bytes.val ≤ budget.val ∧ budget.val < (n.val + 1) * stride.val.val ∧ + (∀ k : Nat, k * stride.val.val ≤ budget.val ↔ k ≤ n.val) ⦄ + +def max_elems_for_bytes_spec : Prop := + ∀ (budget : Usize) (stride : NonZeroUsize), + max_elems_for_bytes_spec_contract budget stride (layout.max_elems_for_bytes budget stride) + +def assume_shallow_unpadded_spec_contract (self : layout.DstLayout) + (run : Result layout.DstLayout) : Prop := + layoutValid self → ∃ r, run = .ok r ∧ layoutValid r ∧ + r.align = self.align ∧ r.size_info = self.size_info ∧ r.statically_shallow_unpadded = true + +def assume_shallow_unpadded_spec : Prop := + ∀ (self : layout.DstLayout), + assume_shallow_unpadded_spec_contract self (layout.DstLayout.assume_shallow_unpadded self) + +def new_zst_spec_contract (a : Option NonZeroUsize) + (run : Result layout.DstLayout) : Prop := + (∀ x ∈ a, 0 < x.val.val) → (∀ x ∈ a, x.val.val.isPowerOfTwo) → + ∃ r, run = .ok r ∧ layoutValid r ∧ r.align = a.getD ⟨1#usize⟩ ∧ + r.size_info = .Sized 0#usize ∧ r.statically_shallow_unpadded = true + +def new_zst_spec : Prop := + ∀ (a : Option NonZeroUsize), + new_zst_spec_contract a (layout.DstLayout.new_zst a) + +def for_type_spec_contract (T : Type) + (run : Result layout.DstLayout) : Prop := + ∀ [RustModel T] (size align : Usize), core.mem.size_of T = .ok size → + core.mem.align_of T = .ok align → 0 < align.val → + ∃ r, run = .ok r ∧ layoutValid r ∧ r.align.val = align ∧ + r.size_info = .Sized size ∧ r.statically_shallow_unpadded = false + +def for_type_spec : Prop := + ∀ (T : Type), + for_type_spec_contract T (layout.DstLayout.for_type T) + +def for_unpadded_type_spec_contract (T : Type) + (run : Result layout.DstLayout) : Prop := + ∀ [RustModel T] (size align : Usize), core.mem.size_of T = .ok size → + core.mem.align_of T = .ok align → 0 < align.val → + ∃ r, run = .ok r ∧ layoutValid r ∧ r.align.val = align ∧ + r.size_info = .Sized size ∧ r.statically_shallow_unpadded = true + +def for_unpadded_type_spec : Prop := + ∀ (T : Type), + for_unpadded_type_spec_contract T (layout.DstLayout.for_unpadded_type T) + +def for_slice_spec_contract (T : Type) + (run : Result layout.DstLayout) : Prop := + ∀ [RustModel T] (size align : Usize), core.mem.size_of T = .ok size → + core.mem.align_of T = .ok align → align.val.isPowerOfTwo → + ∃ r, run = .ok r ∧ layoutValid r ∧ r.align.val = align ∧ + r.statically_shallow_unpadded = true ∧ ∃ t, r.size_info = .SliceDst t ∧ + t.offset = 0#usize ∧ t.elem_size = size ∧ t.size_base = 0#usize ∧ + t.size_rounding_align_and_phase._0.val.val = align.val + +def for_slice_spec : Prop := + ∀ (T : Type), + for_slice_spec_contract T (layout.DstLayout.for_slice T) + +def requires_static_padding_spec_contract (self : layout.DstLayout) + (run : Result Bool) : Prop := + layoutValid self → ∃ r, run = .ok r ∧ + r = !self.statically_shallow_unpadded + +def requires_static_padding_spec : Prop := + ∀ (self : layout.DstLayout), + requires_static_padding_spec_contract self (layout.DstLayout.requires_static_padding self) + end Zerocopy.Obligations @@ -147,3 +232,22 @@ def arithmetic_checks_spec : Prop := arithmetic_checks_spec_contract len align (util.checks.check_arithmetic len align) end Zerocopy.Obligations + +namespace Zerocopy.Obligations + +def primitive_layout_checks_spec_contract (T : Type) (run : Result Unit) : Prop := + ∀ [RustModel T], run ⦃ _ => True ⦄ + +def primitive_layout_checks_spec : Prop := + ∀ (T : Type), primitive_layout_checks_spec_contract T + (layout.primitive_checks.check_primitive_layouts T) + +def empty_layout_checks_spec_contract (repr_align : Option NonZeroUsize) + (run : Result Unit) : Prop := + (∀ align ∈ repr_align, 0 < align.val.val) → run ⦃ _ => True ⦄ + +def empty_layout_checks_spec : Prop := + ∀ repr_align, empty_layout_checks_spec_contract repr_align + (layout.primitive_checks.check_empty_layout repr_align) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/Contracts.lean b/verification/aeneas/lean/Proofs/Contracts.lean index 05c6b9e850..88e0a46854 100644 --- a/verification/aeneas/lean/Proofs/Contracts.lean +++ b/verification/aeneas/lean/Proofs/Contracts.lean @@ -7,7 +7,8 @@ This file may not be copied, modified, or distributed except according to those terms. -/ module -public import Proofs.Raw.Encoding +public import Proofs.Raw.Trailing +public import Proofs.Raw.Layout @[expose] public section open Aeneas Aeneas.Std @@ -76,9 +77,136 @@ theorem encoding_align_spec : Zerocopy.Specs.encoding_align_spec := by exact ⟨av, (decodeNonZeroUScalar_iff align av).mpr rfl, he.trans hvalue.1.symm⟩ register_spec_step encoding_align_spec +theorem max_elems_for_bytes_spec : Zerocopy.Specs.max_elems_for_bytes_spec := by + unfold Zerocopy.Specs.max_elems_for_bytes_spec + representation_simps + intro bytes elem hn + apply WP.spec_mono (Raw.max_elems_for_bytes_spec bytes elem hn) + intro result facts + refine ⟨?_, facts⟩ + change isValid result + simp +register_spec_step max_elems_for_bytes_spec + +theorem assume_shallow_unpadded_spec : Zerocopy.Specs.assume_shallow_unpadded_spec := by + unfold Zerocopy.Specs.assume_shallow_unpadded_spec + representation_simps + intro self hv + apply WP.spec_mono (Raw.assume_shallow_unpadded_spec self) + intro r facts + refine ⟨?_, facts⟩ + simpa only [facts.1, facts.2.1] using hv +register_spec_step assume_shallow_unpadded_spec + +/- Construct a fixed layout from explicit modeled size and alignment reads. +Those reads are data premises supplied by the external ABI bridge, not axioms +asserting that an arbitrary modeled size is the layout of a Rust type. +-/ +theorem for_type_spec : Zerocopy.Specs.for_type_spec := by + unfold Zerocopy.Specs.for_type_spec + representation_simps + intro T validity size align hs ha hn + apply WP.spec_mono (Raw.for_type_spec T size align hs ha hn) + intro r facts + refine ⟨?_, facts⟩ + simp only [facts.1, facts.2.1, hn, and_self] +register_spec_step for_type_spec + +/- Construct the same fixed layout with its asserted unpadded flag. The caller's +separate padding justification is outside this numerical contract. +-/ +theorem for_unpadded_type_spec : Zerocopy.Specs.for_unpadded_type_spec := by + unfold Zerocopy.Specs.for_unpadded_type_spec + representation_simps + intro T validity size align hs ha hn + apply WP.spec_mono (Raw.for_unpadded_type_spec T size align hs ha hn) + intro r facts + refine ⟨?_, facts⟩ + simp only [facts.1, facts.2.1, hn, and_self] +register_spec_step for_unpadded_type_spec + +/- Construct a trailing layout with element size as stride and the modeled ABI +alignment as its rounding alignment. The primitive read premises stay +explicit. +-/ +theorem for_slice_spec : Zerocopy.Specs.for_slice_spec := by + unfold Zerocopy.Specs.for_slice_spec + representation_simps + intro T validity size align hs ha hp + apply WP.spec_mono (Raw.for_slice_spec T size align hs ha hp) + intro r facts + refine ⟨?_, facts⟩ + rcases facts with ⟨halign, _, tail, hsi, _, _, _, hcode⟩ + simp only [halign, hsi] + have := Nat.pos_of_isPowerOfTwo hp + simpa only [hcode, and_self] using this +register_spec_step for_slice_spec + +theorem requires_static_padding_spec : Zerocopy.Specs.requires_static_padding_spec := by + unfold Zerocopy.Specs.requires_static_padding_spec + representation_simps + intro self _ + exact Raw.requires_static_padding_spec self +register_spec_step requires_static_padding_spec + end Zerocopy.Proofs namespace Zerocopy.Proofs open AeneasSpecs +/- Explain both zero-stride rejection and successful conversion. The raw lemma +retains broad representation coverage; the canonical spec adds recursive +admission rather than silently changing that useful raw theorem. +-/ +theorem try_nonzero_spec : Zerocopy.Specs.try_nonzero_spec := by + unfold Zerocopy.Specs.try_nonzero_spec + representation_simps + intro self value decoded + have hv := (size_info_valid_iff self).mp ⟨value, decoded⟩ + apply WP.spec_mono (Raw.try_nonzero_spec self) + intro r facts + constructor + swap + · cases self <;> simpa using facts + change isValid r + rw [option_valid_iff] + cases self with + | Sized size => + simp only [] at facts + rw [facts] + simp [sizeInfoValid] + | SliceDst tail => + simp only [sizeInfoValid, trailingValid, scalar_valid_iff, true_and] at hv + simp only [] at facts + by_cases hz : tail.elem_size = 0#usize + · simp only [hz, if_true] at facts + rw [facts] + simp + · simp only [hz, if_false] at facts + rcases facts with ⟨next, hr, _, _, hcode, helem⟩ + rw [hr] + simp only [Option.mem_some_iff, forall_eq'] + rw [size_info_valid_iff] + change trailingValid next + simp only [trailingValid, nonzero_valid_iff, encodingValid, hcode] + have hnz : tail.elem_size.val ≠ 0 := by + intro h + apply hz + exact UScalar.eq_of_val_eq (by simpa using h) + exact ⟨by simpa only [helem] using Nat.pos_of_ne_zero hnz, hv⟩ +register_spec_step try_nonzero_spec + +theorem new_zst_spec : Zerocopy.Specs.new_zst_spec := by + unfold Zerocopy.Specs.new_zst_spec + representation_simps + intro repr_align hv hp + apply WP.spec_mono (Raw.new_zst_spec repr_align hp) + intro r facts + refine ⟨?_, facts⟩ + simp only [facts.1, facts.2.1] + cases repr_align with + | none => simp + | some a => simpa only [Option.getD_some, and_true] using Nat.pos_of_isPowerOfTwo (hp a rfl) +register_spec_step new_zst_spec + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/PrimitiveChecks.lean b/verification/aeneas/lean/Proofs/PrimitiveChecks.lean new file mode 100644 index 0000000000..9413da9e7f --- /dev/null +++ b/verification/aeneas/lean/Proofs/PrimitiveChecks.lean @@ -0,0 +1,85 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Proofs +@[expose] public section + +/-! +These proofs compose the constructor contracts to check the Rust assertions. +The size and alignment inputs retain the audited ABI-read interpretations; +the harness itself supplies the visible power-of-two admission condition. +-/ +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw + +theorem primitive_layout_checks (T : Type) : + layout.primitive_checks.check_primitive_layouts T ⦃ _ => True ⦄ := by + classical + let size : Usize := if T = Usize then + { bv := BitVec.ofNat _ (System.Platform.numBits / 8) } else RustLayout.size T + let align : Usize := RustLayout.align T + have hs : core.mem.size_of T = .ok size := rfl + have ha : core.mem.align_of T = .ok align := rfl + unfold layout.primitive_checks.check_primitive_layouts + rw [hs, ha] + simp only [bind_ok] + step as ⟨enabled, he⟩ + split + · rename_i yes + have power : align.val.isPowerOfTwo := Eq.mp he yes + have positive := Nat.pos_of_isPowerOfTwo power + step with for_type_spec T size align hs ha positive as ⟨fixed, hf, hfs, hfp⟩ + simp [core.num.nonzero.NonZero.get, hf, hfs, hfp, align, size, massert] + step with for_unpadded_type_spec T size align hs ha positive as ⟨unpadded, hu, hus, hup⟩ + simp [hu, hus, hup, align] + step with for_slice_spec T size align hs ha power as ⟨slice, hsa, hsp, tail, hsi, ho, hel, hb, hc⟩ + simp [hsa, hsp, hsi, ho, hel, hb, align] + have same : tail.size_rounding_align_and_phase._0.val = align := + UScalar.eq_of_val_eq hc + simp [same, align] + · simp only [WP.spec_ok] + +theorem empty_layout_checks (repr_align : Option NonZeroUsize) : + layout.primitive_checks.check_empty_layout repr_align ⦃ _ => True ⦄ := by + unfold layout.primitive_checks.check_empty_layout + cases repr_align with + | none => + simp only [core.num.nonzero.NonZero.get, bind_ok] + step as ⟨enabled, he⟩ + split + · step with new_zst_spec none (by simp) as ⟨empty, ha, hs, hp⟩ + simp [ha, hs, hp, massert, UScalar.val] + · simp only [WP.spec_ok] + | some align => + simp only [core.num.nonzero.NonZero.get, bind_ok] + step as ⟨enabled, he⟩ + split + · rename_i yes + have power : align.val.val.isPowerOfTwo := Eq.mp he yes + step with new_zst_spec (some align) (by simpa using power) as ⟨empty, ha, hs, hp⟩ + simp [ha, hs, hp, massert, UScalar.val] + · simp only [WP.spec_ok] + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs + +theorem primitive_layout_checks_spec : Specs.primitive_layout_checks_spec := by + intro T _ + apply WP.spec_mono (Raw.primitive_layout_checks T) + intro _ _ + exact ⟨(), rfl, trivial⟩ + +theorem empty_layout_checks_spec : Specs.empty_layout_checks_spec := by + intro repr_align _ _ + apply WP.spec_mono (Raw.empty_layout_checks repr_align) + intro _ _ + exact ⟨(), rfl, trivial⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/Raw/Encoding.lean b/verification/aeneas/lean/Proofs/Raw/Encoding.lean index eb0718d347..45fb48c3eb 100644 --- a/verification/aeneas/lean/Proofs/Raw/Encoding.lean +++ b/verification/aeneas/lean/Proofs/Raw/Encoding.lean @@ -11,6 +11,7 @@ public import Specs public import Proofs.Util public import Aeneas public import Loops +public import LayoutModel public import RepresentationLaws public import LayoutMath import all Mathlib.Data.Nat.Log diff --git a/verification/aeneas/lean/Proofs/Raw/Layout.lean b/verification/aeneas/lean/Proofs/Raw/Layout.lean new file mode 100644 index 0000000000..eaceac2fca --- /dev/null +++ b/verification/aeneas/lean/Proofs/Raw/Layout.lean @@ -0,0 +1,134 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Proofs.Raw.Encoding +import all Mathlib.Data.Nat.Log +import all Init.Data.Nat.Power2.Basic +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw + +set_option linter.unusedVariables false +theorem assume_shallow_unpadded_spec : + ∀ (self : layout.DstLayout), + @Zerocopy.layout.DstLayout.assume_shallow_unpadded self ⦃ r => r.align = self.align ∧ r.size_info = self.size_info ∧ r.statically_shallow_unpadded = true ⦄ := by + intro self + simp only [layout.DstLayout.assume_shallow_unpadded, WP.spec_ok, and_self] + +/- Construct a fixed layout from explicit modeled size and alignment reads. +Those reads are data premises supplied by the external ABI bridge, not axioms +asserting that an arbitrary modeled size is the layout of a Rust type. +-/ +theorem for_type_spec : + ∀ (T : Type) (size align : Usize), ∀ (hs : (core.mem.size_of T = .ok size : Prop)), ∀ (ha : (core.mem.align_of T = .ok align : Prop)), ∀ (hn : (0 < align.val : Prop)), + @Zerocopy.layout.DstLayout.for_type T ⦃ r => r.align.val = align ∧ r.size_info = layout.SizeInfo.Sized size ∧ r.statically_shallow_unpadded = false ⦄ := by + intro T size align hs ha hn + have haz : align ≠ 0#usize := by + intro h + have hv := congrArg UScalar.val h + change align.val = 0 at hv + omega + unfold layout.DstLayout.for_type + rw [ha] + simp only [bind_ok, core.num.nonzero.NonZero.new, cast_eq, haz, + ↓reduceDIte, ↓reduceIte, hs, WP.spec_ok, and_self] + +/- Construct the same fixed layout with its asserted unpadded flag. The caller's +separate padding justification is outside this numerical contract. +-/ +theorem for_unpadded_type_spec : + ∀ (T : Type) (size align : Usize), ∀ (hs : (core.mem.size_of T = .ok size : Prop)), ∀ (ha : (core.mem.align_of T = .ok align : Prop)), ∀ (hn : (0 < align.val : Prop)), + @Zerocopy.layout.DstLayout.for_unpadded_type T ⦃ r => r.align.val = align ∧ r.size_info = layout.SizeInfo.Sized size ∧ r.statically_shallow_unpadded = true ⦄ := by + intro T size align hs ha hn + unfold layout.DstLayout.for_unpadded_type + step with for_type_spec T size align hs ha hn as ⟨dl, halign, hsize, _⟩ + step with assume_shallow_unpadded_spec dl as ⟨r, hr, hsi, hp⟩ + exact ⟨hr ▸ halign, hsi ▸ hsize, hp⟩ + +/- Construct a trailing layout with element size as stride and the modeled ABI +alignment as its rounding alignment. The primitive read premises stay +explicit. +-/ +theorem for_slice_spec : + ∀ (T : Type) (size align : Usize), ∀ (hs : (core.mem.size_of T = .ok size : Prop)), ∀ (ha : (core.mem.align_of T = .ok align : Prop)), ∀ (hp : (align.val.isPowerOfTwo : Prop)), + @Zerocopy.layout.DstLayout.for_slice T ⦃ r => r.align.val = align ∧ r.statically_shallow_unpadded = true ∧ + ∃ tail, r.size_info = layout.SizeInfo.SliceDst tail ∧ + tail.offset = 0#usize ∧ tail.elem_size = size ∧ tail.size_base = 0#usize ∧ + tail.size_rounding_align_and_phase._0.val.val = align.val ⦄ := by + intro T size align hs ha hp + have hpos := Nat.pos_of_isPowerOfTwo hp + have haz : align ≠ 0#usize := by + intro h + have hv := congrArg UScalar.val h + change align.val = 0 at hv + omega + unfold layout.DstLayout.for_slice + rw [ha] + simp only [bind_ok, core.num.nonzero.NonZero.new, cast_eq, haz, + ↓reduceDIte, ↓reduceIte, hs] + step with encoding_new_spec ⟨align⟩ 0#usize hp (by simpa using hpos) as ⟨encoded, he⟩ + refine ⟨_, rfl, rfl, rfl, rfl, ?_⟩ + simpa using he + +theorem requires_static_padding_spec : + ∀ (self : layout.DstLayout), + @Zerocopy.layout.DstLayout.requires_static_padding self ⦃ r => r = !self.statically_shallow_unpadded ⦄ := by + intro self + simp only [layout.DstLayout.requires_static_padding, WP.spec_ok] + cases self.statically_shallow_unpadded <;> rfl + +/- Explain both zero-stride rejection and successful conversion. The raw lemma +retains broad representation coverage; the canonical spec adds recursive +admission rather than silently changing that useful raw theorem. +-/ +theorem try_nonzero_spec : + ∀ (self : layout.SizeInfo Usize), + @Zerocopy.layout.SizeInfoUsize.try_to_nonzero_elem_size self ⦃ r => match self with + | .Sized size => r = some (.Sized size) + | .SliceDst tail => + if tail.elem_size = 0#usize then r = none else + ∃ t, r = some (.SliceDst t) ∧ t.offset = tail.offset ∧ + t.size_base = tail.size_base ∧ + t.size_rounding_align_and_phase = tail.size_rounding_align_and_phase ∧ + t.elem_size.val = tail.elem_size ⦄ := by + intro self + cases self with + | Sized size => simp [layout.SizeInfoUsize.try_to_nonzero_elem_size] + | SliceDst tail => + unfold layout.SizeInfoUsize.try_to_nonzero_elem_size core.num.nonzero.NonZero.new + by_cases hz : tail.elem_size = 0#usize + · simp only [cast_eq, hz, ↓reduceDIte, ↓reduceIte, bind_ok, WP.spec_ok] + · simp only [cast_eq, hz, ↓reduceDIte, ↓reduceIte, bind_ok, WP.spec_ok] + exact ⟨_, rfl, rfl, rfl, rfl, rfl⟩ + +theorem min_align_eq : layout.DstLayout.MIN_ALIGN = .ok ⟨1#usize⟩ := by + simp [layout.DstLayout.MIN_ALIGN, core.num.nonzero.NonZero.new] + +theorem new_zst_spec : + ∀ (repr_align : Option NonZeroUsize), ∀ (hp : (∀ a ∈ repr_align, a.val.val.isPowerOfTwo : Prop)), + @Zerocopy.layout.DstLayout.new_zst repr_align ⦃ r => r.align = repr_align.getD ⟨1#usize⟩ ∧ + r.size_info = .Sized 0#usize ∧ r.statically_shallow_unpadded = true ⦄ := by + intro repr_align hp + unfold layout.DstLayout.new_zst + have ha : (repr_align.getD ⟨1#usize⟩).val.val.isPowerOfTwo := by + cases repr_align with + | none => exact ⟨0, by simp⟩ + | some a => exact hp a rfl + cases repr_align + all_goals + simp only [min_align_eq, Option.getD_none, Option.getD_some, + core.num.nonzero.NonZero.get, bind_ok] at ha ⊢ + step as ⟨b, hb⟩ + have hbt : b = true := by + have hb' : (b = true) = True := by simpa only [ha, Nat.isPowerOfTwo_one] using hb + exact Eq.mpr hb' trivial + simp [massert, hbt, bind_ok, WP.spec_ok] + +end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/Proofs/Raw/Trailing.lean b/verification/aeneas/lean/Proofs/Raw/Trailing.lean new file mode 100644 index 0000000000..740777817f --- /dev/null +++ b/verification/aeneas/lean/Proofs/Raw/Trailing.lean @@ -0,0 +1,48 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Proofs.Raw.Encoding +import all Mathlib.Data.Nat.Log +import all Init.Data.Nat.Power2.Basic +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw + +set_option linter.unusedVariables false +theorem max_elems_for_bytes_spec : + ∀ (bytes : Usize) (elem_size : NonZeroUsize), ∀ (hn : (0 < elem_size.val.val : Prop)), + @Zerocopy.layout.max_elems_for_bytes bytes elem_size ⦃ (elems, used) => + elems.val = bytes.val / elem_size.val.val ∧ used.val = elems.val * elem_size.val.val ∧ + used ≤ bytes ∧ bytes.val < (elems.val + 1) * elem_size.val.val ∧ + (∀ n : Nat, n * elem_size.val.val ≤ bytes.val ↔ n ≤ elems.val) ⦄ := by + intro bytes elem hn + unfold layout.max_elems_for_bytes + simp only [core.num.nonzero.NonZero.get, bind_ok] + step with Usize.div_spec bytes (y := elem.val) (by omega) as ⟨elems, he⟩ + have hfit : elems.val * elem.val.val ≤ bytes.val := by + rw [he, Nat.mul_comm] + exact Nat.mul_div_le _ _ + have hav : bytes.val ≤ Usize.max := by scalar_tac + step as ⟨product, hmul⟩ + cases product with + | none => + simp only [] at hmul + omega + | some used => + simp only [] at hmul + simp only [WP.spec_ok] + refine ⟨he, hmul.2.1, (UScalar.le_equiv _ _).mpr (by omega), ?_, ?_⟩ + · rw [he, Nat.mul_comm] + exact Nat.lt_mul_div_succ _ hn + · intro n + rw [he] + exact (Nat.le_div_iff_mul_le hn).symm + +end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/RequiredModelContracts.lean b/verification/aeneas/lean/RequiredModelContracts.lean index a3051dee3c..c6fd3536fd 100644 --- a/verification/aeneas/lean/RequiredModelContracts.lean +++ b/verification/aeneas/lean/RequiredModelContracts.lean @@ -26,7 +26,8 @@ proved implications available to check_contract's bounded normalization. open Aeneas Aeneas.Std AeneasSpecs namespace Zerocopy.Proofs -attribute [contract_simps] encoding_decoder_admitted_iff +attribute [contract_simps] encoding_decoder_admitted_iff trailing_decoder_admitted_iff + size_info_decoder_admitted_iff layout_decoder_admitted_iff @[contract_simps] theorem required_encoding_new (align : NonZeroUsize) (phase : Usize) (run : Result layout.RoundingAlignAndPhase) @@ -81,4 +82,17 @@ attribute [contract_simps] encoding_decoder_admitted_iff exact ⟨Nat.pos_of_isPowerOfTwo value.align_pow2, value.align_pow2, value.phase_lt, hraw.symm, hcanonical.1, hcanonical.2⟩ +@[contract_simps] theorem required_try_nonzero (self : layout.SizeInfo Usize) + (run : Result (Option (layout.SizeInfo NonZeroUsize))) + (provided : Specs.try_nonzero_spec_contract self run) : + Obligations.try_nonzero_spec_contract self run := by + intro accepted + obtain ⟨value, decoded⟩ := (size_info_valid_iff self).mpr accepted + apply WP.spec_mono (provided value decoded) + rintro result ⟨resultValue, resultDecoded, facts⟩ + refine ⟨?_, ?_⟩ + · have valid : isValid result := ⟨resultValue, resultDecoded⟩ + simpa only [option_valid_iff, size_info_valid_iff] using valid + · cases self <;> simpa only using facts + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/PrimitiveChecks.lean b/verification/aeneas/lean/RequiredModelContracts/PrimitiveChecks.lean new file mode 100644 index 0000000000..49bde2fd73 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/PrimitiveChecks.lean @@ -0,0 +1,56 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import RequiredModelContracts +@[expose] public section + +/-! +The independent expectations require successful execution on the original +Rust input domains. These implications check that the generated unit-returning +specifications retain that promise for an arbitrary execution outcome. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +/- Canonical raw layouts satisfy the input decoder's requirements. Share this +bridge with later allocation and cast checks so their broad raw domains do not +need to assume successful decoding separately. -/ +theorem layout_admitted_of_canonical (self : layout.DstLayout) + (positive : 0 < self.align.val.val) (canonical : canonicalLayout self) : + ∃ value, RustModel.decode self = some value := by + apply (layout_admitted_iff self).mpr + refine ⟨positive, ?_⟩ + cases info : self.size_info with + | Sized size => simp only [sizeInfoValid] + | SliceDst tail => + simpa only [sizeInfoValid, trailingValid, scalar_valid_iff, true_and, + encodingValid, canonicalLayout, info] using canonical + +@[contract_simps] theorem required_primitive_layout_checks (T : Type) + (run : Result Unit) (provided : Specs.primitive_layout_checks_spec_contract T run) : + Obligations.primitive_layout_checks_spec_contract T run := by + intro validity + apply WP.spec_mono (provided) + intro _ _ + trivial + +@[contract_simps] theorem required_empty_layout_checks (repr_align : Option NonZeroUsize) + (run : Result Unit) (provided : Specs.empty_layout_checks_spec_contract repr_align run) : + Obligations.empty_layout_checks_spec_contract repr_align run := by + intro positive + have admitted : isValid repr_align := by + rw [option_nonzero_unsigned_valid_iff] + intro align member + exact (nonzero_valid_iff align).mpr (positive align member) + obtain ⟨value, decoded⟩ := admitted + apply WP.spec_mono (provided value decoded) + intro _ _ + trivial + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index 559024360d..d0de054abe 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -159,13 +159,34 @@ def core.intrinsics.transmute {Src : Type} (Dst : Type) {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) (x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val --- Extraction uses size_of only for usize to calculate its bit width. Other --- types remain unsupported rather than receiving arbitrary layout values. +-- Aeneas erases Rust's ABI information from a generic Type parameter. These +-- two data parameters supply that information. They assert no propositions; +-- every consumer must prove its contract under explicit size/alignment inputs. +-- The axiom audit admits exactly these signatures, never arbitrary axioms. +axiom Zerocopy.RustLayout.size (T : Type) : Usize +axiom Zerocopy.RustLayout.alignInput (T : Type) : Usize + +-- The byte primitive has compiler alignment one. Its native compile-time +-- assertion lives beside the Rust layout fixtures. This is a concrete external +-- interpretation, not a proof of an arbitrary ABI fact; generic types retain +-- the original unconstrained data input. Keep this one case explicit rather +-- than inferring physical layout from a Lean type's mathematical meaning. +noncomputable def Zerocopy.RustLayout.align (T : Type) : Usize := by + classical + exact if T = U8 then 1#usize else Zerocopy.RustLayout.alignInput T + +@[simp] theorem Zerocopy.RustLayout.align_u8 : + Zerocopy.RustLayout.align U8 = 1#usize := by + simp [Zerocopy.RustLayout.align] + @[simp] noncomputable def core.mem.size_of (T : Type) : Result Usize := by classical - exact if T = Usize then - .ok { bv := BitVec.ofNat _ (System.Platform.numBits / 8) } - else .fail .panic + exact .ok (if T = Usize then + { bv := BitVec.ofNat _ (System.Platform.numBits / 8) } + else Zerocopy.RustLayout.size T) + +@[simp] noncomputable def core.mem.align_of (T : Type) : Result Usize := + .ok (Zerocopy.RustLayout.align T) -- The extracted call sites instantiate this primitive only at Usize. Other -- types are unsupported, so the model cannot promise a recoverable panic. diff --git a/verification/aeneas/projections/ModelShapes.lean b/verification/aeneas/projections/ModelShapes.lean index 842835771e..987bf9d0ba 100644 --- a/verification/aeneas/projections/ModelShapes.lean +++ b/verification/aeneas/projections/ModelShapes.lean @@ -53,6 +53,12 @@ model RoundingValue where fits : align + phase ≤ Usize.max end +derive_model_shape Zerocopy.layout.TrailingSliceLayout with 1 type parameters + +derive_model_shape Zerocopy.layout.SizeInfo with 1 type parameters + +derive_model_shape Zerocopy.layout.DstLayout with 0 type parameters + derive_model_shape Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters derive_model_shape Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean index bb3b96f74a..3c408a9a59 100644 --- a/verification/aeneas/projections/Models.lean +++ b/verification/aeneas/projections/Models.lean @@ -65,6 +65,15 @@ derive_rust_model Zerocopy.layout.RoundingAlignAndPhase with 0 type parameters d { align := align, phase := word - align, .. } check_model_binding Zerocopy.layout.RoundingAlignAndPhase with 0 type parameters +derive_rust_model Zerocopy.layout.TrailingSliceLayout with 1 type parameters +check_model_binding Zerocopy.layout.TrailingSliceLayout with 1 type parameters + +derive_rust_model Zerocopy.layout.SizeInfo with 1 type parameters +check_model_binding Zerocopy.layout.SizeInfo with 1 type parameters + +derive_rust_model Zerocopy.layout.DstLayout with 0 type parameters +check_model_binding Zerocopy.layout.DstLayout with 0 type parameters + derive_rust_model Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters check_model_binding Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 0f2b54b2eb..ac4f3295d1 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -150,6 +150,94 @@ spec encoding_align_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.encoding_align_spec for Zerocopy.layout.RoundingAlignAndPhase.align with 1 +check_model_inputs Zerocopy.layout.SizeInfoUsize.try_to_nonzero_elem_size with 0 type parameters +aeneas_spec_begin +spec try_nonzero_spec + for @Zerocopy.layout.SizeInfoUsize.try_to_nonzero_elem_size with 0 type parameters + ensures(raw) r => match self with + | .Sized size => r = some (.Sized size) + | .SliceDst tail => + if tail.elem_size = 0#usize then r = none else + ∃ t, r = some (.SliceDst t) ∧ t.offset = tail.offset ∧ + t.size_base = tail.size_base ∧ + t.size_rounding_align_and_phase = tail.size_rounding_align_and_phase ∧ + t.elem_size.val = tail.elem_size +aeneas_spec_end +check_spec_binding Zerocopy.Specs.try_nonzero_spec for Zerocopy.layout.SizeInfoUsize.try_to_nonzero_elem_size with 1 + +check_model_inputs Zerocopy.layout.max_elems_for_bytes with 0 type parameters +aeneas_spec_begin +spec max_elems_for_bytes_spec + for @Zerocopy.layout.max_elems_for_bytes with 0 type parameters + ensures(raw) (elems, used) => + elems.val = bytes.val / elem_size.val.val ∧ used.val = elems.val * elem_size.val.val ∧ + used ≤ bytes ∧ bytes.val < (elems.val + 1) * elem_size.val.val ∧ + (∀ n : Nat, n * elem_size.val.val ≤ bytes.val ↔ n ≤ elems.val) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.max_elems_for_bytes_spec for Zerocopy.layout.max_elems_for_bytes with 2 + +check_model_inputs Zerocopy.layout.DstLayout.assume_shallow_unpadded with 0 type parameters +aeneas_spec_begin +spec assume_shallow_unpadded_spec + for @Zerocopy.layout.DstLayout.assume_shallow_unpadded with 0 type parameters + ensures(raw) r => r.align = self.align ∧ r.size_info = self.size_info ∧ r.statically_shallow_unpadded = true +aeneas_spec_end +check_spec_binding Zerocopy.Specs.assume_shallow_unpadded_spec for Zerocopy.layout.DstLayout.assume_shallow_unpadded with 1 + +check_model_inputs Zerocopy.layout.DstLayout.new_zst with 0 type parameters +aeneas_spec_begin +spec new_zst_spec + for @Zerocopy.layout.DstLayout.new_zst with 0 type parameters + requires(raw) hp : ∀ a ∈ repr_align, a.val.val.isPowerOfTwo + ensures(raw) r => r.align = repr_align.getD ⟨1#usize⟩ ∧ + r.size_info = .Sized 0#usize ∧ r.statically_shallow_unpadded = true +aeneas_spec_end +check_spec_binding Zerocopy.Specs.new_zst_spec for Zerocopy.layout.DstLayout.new_zst with 1 + +check_model_inputs Zerocopy.layout.DstLayout.for_type with 1 type parameters +aeneas_spec_begin +spec for_type_spec (size align : Usize) + for @Zerocopy.layout.DstLayout.for_type with 1 type parameters + requires(raw) hs : core.mem.size_of T = .ok size + requires(raw) ha : core.mem.align_of T = .ok align + requires(raw) hn : 0 < align.val + ensures(raw) r => r.align.val = align ∧ r.size_info = layout.SizeInfo.Sized size ∧ r.statically_shallow_unpadded = false +aeneas_spec_end +check_spec_binding Zerocopy.Specs.for_type_spec for Zerocopy.layout.DstLayout.for_type with 1 + +check_model_inputs Zerocopy.layout.DstLayout.for_unpadded_type with 1 type parameters +aeneas_spec_begin +spec for_unpadded_type_spec (size align : Usize) + for @Zerocopy.layout.DstLayout.for_unpadded_type with 1 type parameters + requires(raw) hs : core.mem.size_of T = .ok size + requires(raw) ha : core.mem.align_of T = .ok align + requires(raw) hn : 0 < align.val + ensures(raw) r => r.align.val = align ∧ r.size_info = layout.SizeInfo.Sized size ∧ r.statically_shallow_unpadded = true +aeneas_spec_end +check_spec_binding Zerocopy.Specs.for_unpadded_type_spec for Zerocopy.layout.DstLayout.for_unpadded_type with 1 + +check_model_inputs Zerocopy.layout.DstLayout.for_slice with 1 type parameters +aeneas_spec_begin +spec for_slice_spec (size align : Usize) + for @Zerocopy.layout.DstLayout.for_slice with 1 type parameters + requires(raw) hs : core.mem.size_of T = .ok size + requires(raw) ha : core.mem.align_of T = .ok align + requires(raw) hp : align.val.isPowerOfTwo + ensures(raw) r => r.align.val = align ∧ r.statically_shallow_unpadded = true ∧ + ∃ tail, r.size_info = layout.SizeInfo.SliceDst tail ∧ + tail.offset = 0#usize ∧ tail.elem_size = size ∧ tail.size_base = 0#usize ∧ + tail.size_rounding_align_and_phase._0.val.val = align.val +aeneas_spec_end +check_spec_binding Zerocopy.Specs.for_slice_spec for Zerocopy.layout.DstLayout.for_slice with 1 + +check_model_inputs Zerocopy.layout.DstLayout.requires_static_padding with 0 type parameters +aeneas_spec_begin +spec requires_static_padding_spec + for @Zerocopy.layout.DstLayout.requires_static_padding with 0 type parameters + ensures(raw) r => r = !self.statically_shallow_unpadded +aeneas_spec_end +check_spec_binding Zerocopy.Specs.requires_static_padding_spec for Zerocopy.layout.DstLayout.requires_static_padding with 1 + check_model_inputs Zerocopy.layout.nested_reference.round_up with 0 type parameters aeneas_spec_begin spec nested_round_up_spec @@ -170,6 +258,22 @@ spec nested_reference_size_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.nested_reference_size_spec for Zerocopy.layout.nested_reference.size_for_metadata with 4 +check_model_inputs Zerocopy.layout.primitive_checks.check_primitive_layouts with 1 type parameters +aeneas_spec_begin +spec primitive_layout_checks_spec + for @Zerocopy.layout.primitive_checks.check_primitive_layouts with 1 type parameters + ensures _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.primitive_layout_checks_spec for Zerocopy.layout.primitive_checks.check_primitive_layouts with 1 + +check_model_inputs Zerocopy.layout.primitive_checks.check_empty_layout with 0 type parameters +aeneas_spec_begin +spec empty_layout_checks_spec + for @Zerocopy.layout.primitive_checks.check_empty_layout with 0 type parameters + ensures _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.empty_layout_checks_spec for Zerocopy.layout.primitive_checks.check_empty_layout with 1 + default_trait_body Zerocopy.FromZeros.new_zeroed.default for Zerocopy.FromZeros with 1 type parameters check_model_inputs Zerocopy.FromZeros.new_zeroed.default with 1 type parameters aeneas_spec_begin diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index dd6003f86c..0a28cfe2cb 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -12,6 +12,9 @@ #[allow(dead_code)] mod nested_reference; +#[allow(dead_code)] +mod primitive_checks; + use core::{mem, num::NonZeroUsize}; use crate::util; @@ -773,6 +776,18 @@ impl SizeInfo { (SizeInfo::SliceDst(original), None) => original.elem_size == 0, _ => false, }))] + /// + /// ```aeneas + /// spec try_nonzero_spec + /// ensures(raw) r => match self with + /// | .Sized size => r = some (.Sized size) + /// | .SliceDst tail => + /// if tail.elem_size = 0#usize then r = none else + /// ∃ t, r = some (.SliceDst t) ∧ t.offset = tail.offset ∧ + /// t.size_base = tail.size_base ∧ + /// t.size_rounding_align_and_phase = tail.size_rounding_align_and_phase ∧ + /// t.elem_size.val = tail.elem_size + /// ``` const fn try_to_nonzero_elem_size(&self) -> Option> { #[cfg(kani)] #[kani::proof_for_contract(SizeInfo::try_to_nonzero_elem_size)] @@ -821,6 +836,14 @@ impl SizeInfo { }) )] #[inline(always)] +/// +/// ```aeneas +/// spec max_elems_for_bytes_spec +/// ensures(raw) (elems, used) => +/// elems.val = bytes.val / elem_size.val.val ∧ used.val = elems.val * elem_size.val.val ∧ +/// used ≤ bytes ∧ bytes.val < (elems.val + 1) * elem_size.val.val ∧ +/// (∀ n : Nat, n * elem_size.val.val ≤ bytes.val ↔ n ≤ elems.val) +/// ``` const fn max_elems_for_bytes(bytes: usize, elem_size: NonZeroUsize) -> (usize, usize) { #[cfg(kani)] #[kani::proof_for_contract(max_elems_for_bytes)] @@ -920,6 +943,11 @@ impl DstLayout { result.align == self.align && result.size_info == self.size_info && result.statically_shallow_unpadded }))] + /// + /// ```aeneas + /// spec assume_shallow_unpadded_spec + /// ensures(raw) r => r.align = self.align ∧ r.size_info = self.size_info ∧ r.statically_shallow_unpadded = true + /// ``` const fn assume_shallow_unpadded(self) -> Self { #[cfg(kani)] #[kani::proof_for_contract(DstLayout::assume_shallow_unpadded)] @@ -951,6 +979,13 @@ impl DstLayout { && result.size_info == SizeInfo::Sized { size: 0 } && result.statically_shallow_unpadded }))] + /// + /// ```aeneas + /// spec new_zst_spec + /// requires(raw) hp : ∀ a ∈ repr_align, a.val.val.isPowerOfTwo + /// ensures(raw) r => r.align = repr_align.getD ⟨1#usize⟩ ∧ + /// r.size_info = .Sized 0#usize ∧ r.statically_shallow_unpadded = true + /// ``` pub const fn new_zst(repr_align: Option) -> DstLayout { #[cfg(kani)] #[kani::proof_for_contract(DstLayout::new_zst)] @@ -987,6 +1022,14 @@ impl DstLayout { && result.size_info == SizeInfo::Sized { size: mem::size_of::() } && result.statically_shallow_unpadded == false }))] + /// + /// ```aeneas + /// spec for_type_spec (size align : Usize) + /// requires(raw) hs : core.mem.size_of T = .ok size + /// requires(raw) ha : core.mem.align_of T = .ok align + /// requires(raw) hn : 0 < align.val + /// ensures(raw) r => r.align.val = align ∧ r.size_info = layout.SizeInfo.Sized size ∧ r.statically_shallow_unpadded = false + /// ``` pub const fn for_type() -> DstLayout { #[cfg(kani)] #[kani::proof_for_contract(DstLayout::for_type::<()>)] @@ -1034,6 +1077,14 @@ impl DstLayout { && result.size_info == SizeInfo::Sized { size: mem::size_of::() } && result.statically_shallow_unpadded == true }))] + /// + /// ```aeneas + /// spec for_unpadded_type_spec (size align : Usize) + /// requires(raw) hs : core.mem.size_of T = .ok size + /// requires(raw) ha : core.mem.align_of T = .ok align + /// requires(raw) hn : 0 < align.val + /// ensures(raw) r => r.align.val = align ∧ r.size_info = layout.SizeInfo.Sized size ∧ r.statically_shallow_unpadded = true + /// ``` pub const fn for_unpadded_type() -> DstLayout { #[cfg(kani)] #[kani::proof_for_contract(DstLayout::for_unpadded_type::<()>)] @@ -1062,6 +1113,17 @@ impl DstLayout { && trailing.elem_size == mem::size_of::() && trailing.size_rounding_align_and_phase.components() == (result.align, 0)) }))] + /// + /// ```aeneas + /// spec for_slice_spec (size align : Usize) + /// requires(raw) hs : core.mem.size_of T = .ok size + /// requires(raw) ha : core.mem.align_of T = .ok align + /// requires(raw) hp : align.val.isPowerOfTwo + /// ensures(raw) r => r.align.val = align ∧ r.statically_shallow_unpadded = true ∧ + /// ∃ tail, r.size_info = layout.SizeInfo.SliceDst tail ∧ + /// tail.offset = 0#usize ∧ tail.elem_size = size ∧ tail.size_base = 0#usize ∧ + /// tail.size_rounding_align_and_phase._0.val.val = align.val + /// ``` pub(crate) const fn for_slice() -> DstLayout { #[cfg(kani)] #[kani::proof_for_contract(DstLayout::for_slice::<()>)] @@ -1484,6 +1546,11 @@ impl DstLayout { #[must_use] #[inline(always)] #[cfg_attr(kani, kani::ensures(|&padding| padding == !self.statically_shallow_unpadded))] + /// + /// ```aeneas + /// spec requires_static_padding_spec + /// ensures(raw) r => r = !self.statically_shallow_unpadded + /// ``` pub const fn requires_static_padding(self) -> bool { #[cfg(kani)] #[kani::proof_for_contract(DstLayout::requires_static_padding)] diff --git a/zerocopy/src/layout/primitive_checks.rs b/zerocopy/src/layout/primitive_checks.rs new file mode 100644 index 0000000000..b1b0b2041f --- /dev/null +++ b/zerocopy/src/layout/primitive_checks.rs @@ -0,0 +1,99 @@ +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// Copyright 2026 The Fuchsia Authors +// +// Licensed under the 2-Clause BSD License , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +//! These assertions make the primitive constructor promises readable in Rust. +//! +//! Aeneas proves successful execution, including the assertions, for arbitrary +//! inputs to each harness. The standard-library size and alignment reads are +//! the reference observations; the explicit Rust layout premise explains how +//! their extracted inputs correspond to the compiler's actual ABI. + +use super::{mem, DstLayout, NonZeroUsize, SizeInfo}; + +/// Compares the three primitive constructors with Rust's size and alignment. +/// +/// Rust type alignments are nonzero powers of two. The explicit guard also +/// makes the admitted ABI inputs visible when those reads are modeled as +/// unconstrained data during extraction. +/// +/// ```aeneas +/// spec primitive_layout_checks_spec +/// ensures _ => True +/// ``` +fn check_primitive_layouts() { + let size = mem::size_of::(); + let align = mem::align_of::(); + if !align.is_power_of_two() { + return; + } + + let fixed = DstLayout::for_type::(); + assert!(fixed.align.get() == align); + assert!(matches!(fixed.size_info, SizeInfo::Sized { size: actual } if actual == size)); + assert!(!fixed.statically_shallow_unpadded); + + let unpadded = DstLayout::for_unpadded_type::(); + assert!(unpadded.align.get() == align); + assert!(matches!(unpadded.size_info, SizeInfo::Sized { size: actual } if actual == size)); + assert!(unpadded.statically_shallow_unpadded); + + let slice = DstLayout::for_slice::(); + assert!(slice.align.get() == align); + assert!(slice.statically_shallow_unpadded); + match slice.size_info { + SizeInfo::SliceDst(tail) => { + assert!(tail.offset == 0); + assert!(tail.elem_size == size); + assert!(tail.size_base == 0); + // Alignment plus a zero phase has exactly this encoding. + assert!(tail.size_rounding_align_and_phase.0.get() == align); + } + SizeInfo::Sized { .. } => panic!("slice constructor returned a sized layout"), + } +} + +/// Checks the empty layout constructor, including its optional alignment. +/// +/// ```aeneas +/// spec empty_layout_checks_spec +/// ensures _ => True +/// ``` +fn check_empty_layout(repr_align: Option) { + let expected_align = match repr_align { + Some(align) => align.get(), + None => 1, + }; + if !expected_align.is_power_of_two() { + return; + } + let empty = DstLayout::new_zst(repr_align); + assert!(empty.align.get() == expected_align); + assert!(matches!(empty.size_info, SizeInfo::Sized { size: 0 })); + assert!(empty.statically_shallow_unpadded); +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn primitive_examples() { + check_primitive_layouts::<()>(); + check_primitive_layouts::(); + check_primitive_layouts::(); + check_primitive_layouts::<(u8, u64)>(); + check_primitive_layouts::<[u64; 3]>(); + check_empty_layout(None); + for align in [1, 2, 8, 3] { + check_empty_layout(NonZeroUsize::new(align)); + } + } +}