From 7be8c70932afc5fc3a650286cbe6f3872fa86230 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 10:41:04 -0400 Subject: [PATCH] Prove primitive layout constructors with recursive mathematical models Prove primitive constructor, zero-stride and capacity contracts over recursively valid fields while preserving useful broader Raw statements. Keep operation-specific alignment, fit and ABI interpretation premises explicit; independent expectations check the generated contracts. Add total Rust assertion harnesses for primitive, unpadded, slice, and empty layout constructors. Compare every stored field with Rust size/alignment reads and retain the broader original mathematical constructor contracts. Validation: fresh pinned extraction and complete-model golden comparison; independent golden/live Lean builds, required-contract checks, and the transitive axiom audit. gherrit-pr-id: Glbefkopwxutlxlg5qgtbtb3p6a5o73ow Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 33 ++- verification/aeneas/SEMANTICS.md | 151 ++++++++++ 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 +++++++- verification/aeneas/lean/Proofs.lean | 272 ++++++++++++++++++ .../aeneas/lean/Proofs/PrimitiveChecks.lean | 85 ++++++ .../aeneas/lean/RequiredModelContracts.lean | 16 +- .../PrimitiveChecks.lean | 56 ++++ .../aeneas/lean/Zerocopy/FunsExternal.lean | 18 +- zerocopy/src/layout/mod.rs | 67 +++++ zerocopy/src/layout/primitive_checks.rs | 99 +++++++ 16 files changed, 1444 insertions(+), 33 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/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 1d8ee8b4b8..66ae4ec727 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -114,13 +114,14 @@ 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 @@ -128,14 +129,14 @@ 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 diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md new file mode 100644 index 0000000000..2a89db4cd0 --- /dev/null +++ b/verification/aeneas/SEMANTICS.md @@ -0,0 +1,151 @@ + + +# 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. diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 051c3f642f..d6426bef15 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -643,14 +643,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) : @@ -671,7 +671,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 @@ -699,7 +699,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 @@ -708,6 +708,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 46:0-56:1 -/ def layout.nested_reference.round_up @@ -823,6 +970,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::util::round_down_to_next_multiple_of_alignment]: Source: 'src/util/mod.rs', lines 261:0-279:1 -/ def util.round_down_to_next_multiple_of_alignment diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index 03f8eb3085..7a0028e10c 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -35,6 +35,13 @@ open Zerocopy @[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::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}::clone]: Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22 Name pattern: [core::num::niche_types::{core::clone::Clone}::clone] diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 1d882da79b..267aabb722 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -100,11 +100,35 @@ structure byteorder.U32 (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 27:0-31: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.lean b/verification/aeneas/lean/Proofs.lean index bee36adb80..0119cc2995 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -12,6 +12,7 @@ public import Proofs.Util public import Proofs.NestedReference public import Aeneas public import Loops +public import LayoutModel public import RepresentationLaws public import LayoutMath import all Mathlib.Data.Nat.Log @@ -204,6 +205,150 @@ theorem encoding_align_spec : step with encoding_components_spec self hn as ⟨a, p, _, _, _, ha, _⟩ simpa only [WP.spec_ok] using ha +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 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 + +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 namespace Zerocopy.Proofs @@ -270,9 +415,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/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..35eacbaf55 --- /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_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 52612ebaa5..5d1706a7f2 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -23,13 +23,21 @@ def core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone {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.align (T : Type) : Usize + @[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. @[simp] noncomputable def core.num.nonzero.NonZero.new diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index 9ad84757f8..7da300d273 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)); + } + } +}