From 5b3579b22f95da0b1f866f5e7aa3af094875d8ee Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 11:26:30 -0400 Subject: [PATCH] Prove record construction against independent Rust references Prove record construction under the independent prefix construction domain and connect results to recursive field placement. Retain concrete admitted-domain witnesses; decoding does not assert that arbitrary raw records describe realizable Rust layouts. Prove the ordinary Rust assertion harness equating production sizing with the independent nested reference for arbitrary depth and every machine metadata count, including overflow and zero-size tails. Compare arbitrary field-list construction against independent Rust extension/padding and every stored field. Keep the explicit compiler premise and regression tests as the Rust boundary. Validation: fresh pinned extraction and complete-model golden comparison; independent golden/live Lean builds, required-contract checks, and the transitive axiom audit. Closes #3617 gherrit-pr-id: Gnng6cftnqanivvm3mjiwcif6hovmkymt Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 211 ++++--- verification/aeneas/SEMANTICS.md | 21 +- verification/aeneas/golden/Funs.lean | 422 ++++++++++++- verification/aeneas/golden/Types.lean | 2 +- .../aeneas/lean/CompositionConstructor.lean | 352 +++++++++++ verification/aeneas/lean/Corollaries.lean | 59 +- verification/aeneas/lean/LayoutMath.lean | 27 + verification/aeneas/lean/LayoutModel.lean | 30 + .../aeneas/lean/LayoutModelDomainTests.lean | 183 ++++++ verification/aeneas/lean/MathViews.lean | 35 +- .../aeneas/lean/ModelProjectionLaws.lean | 138 ++--- verification/aeneas/lean/Obligations.lean | 38 +- .../lean/Obligations/CompositionChecks.lean | 11 + verification/aeneas/lean/Proofs.lean | 111 +++- .../aeneas/lean/Proofs/CompositionChecks.lean | 73 ++- .../lean/Proofs/NestedConstruction.lean | 576 ++++++++++++++++++ .../aeneas/lean/Proofs/NestedReference.lean | 11 + .../CompositionChecks.lean | 22 + zerocopy/src/layout/composition_checks.rs | 59 ++ zerocopy/src/layout/mod.rs | 41 +- zerocopy/src/layout/nested_reference.rs | 101 +++ 21 files changed, 2303 insertions(+), 220 deletions(-) create mode 100644 verification/aeneas/lean/CompositionConstructor.lean create mode 100644 verification/aeneas/lean/LayoutModelDomainTests.lean create mode 100644 verification/aeneas/lean/Proofs/NestedConstruction.lean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 6ca25098f7..d52c4e50c8 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -14,11 +14,18 @@ the inline Rust specifications against both the checked-in and live models. The required `All checks succeeded (ci.yml)` job depends on it. The settled design and deferred work are recorded in [DESIGN.md](DESIGN.md). -Application claims can use ordinary Rust assertion harnesses with total -`ensures _ => True` specifications. Successful termination requires every -assertion to pass. Review the independent calculation, complete comparisons, -and early returns together: returning early excludes that input from the -comparison. +For application review, start with the ordinary Rust reference calculations and +assertion harnesses in [`layout/nested_reference.rs`](../../zerocopy/src/layout/nested_reference.rs), +[`layout/tail_checks.rs`](../../zerocopy/src/layout/tail_checks.rs), +[`layout/composition_checks.rs`](../../zerocopy/src/layout/composition_checks.rs), +[`layout/tail_transform_checks.rs`](../../zerocopy/src/layout/tail_transform_checks.rs), +[`layout/primitive_checks.rs`](../../zerocopy/src/layout/primitive_checks.rs), and +[`util/checks.rs`](../../zerocopy/src/util/checks.rs). A total `ensures _ => True` +specification on a harness proves that it terminates without failing any of its +assertions for every admitted input. The assertions, comparisons, and early +returns are ordinary Rust, so the reviewer can assess the intended behavior and +its domain together. In particular, a guard that returns early excludes that +case from the comparison even though the harness itself still succeeds. Six concrete wrappers in [`lib.rs`](../../zerocopy/src/lib.rs) call the actual `PointerMetadata` implementations for `()` and `usize`. Their contracts check @@ -150,77 +157,93 @@ 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), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs), [tail assertions](../../zerocopy/src/layout/tail_checks.rs), [composition assertions](../../zerocopy/src/layout/composition_checks.rs), [tail transformations](../../zerocopy/src/layout/tail_transform_checks.rs). - Extraction starts from the function and nominal-type owners of every present -`aeneas` fence in `zerocopy/src`, including their dependencies. Every present -fence must have a supported Rust owner, exact extraction binding, and the -corresponding checked Lean declarations. Unannotated functions and impls can be -added without extending the specification set. +`aeneas` fence in `zerocopy/src`, including their dependencies. The current +function specifications cover the layout and arithmetic methods and their Rust +reference harnesses. Unannotated functions and impls can be added without +extending the specification set. Every present fence must have a supported Rust +owner, exact extraction binding, and the corresponding checked Lean declarations. | 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`, `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. | -| Trailing size, padding, and capacity | Exact size-offset and capacity formulas, checked-size overflow, and wrapping padding; successful sizes and physical padding refine the independent recursive semantics. | -| `DstLayout::{extend,pad_to_align}` | Exact field placement, alignment, padding flags, and normalized size formulas; outer padding preserves each field's complete inner size. | -| Trailing advancement and size-sequence comparison | Exact byte advancement; a positive comparison establishes equal sizes for every natural metadata value. | -| `DstLayout::requires_dynamic_padding` | Exact flag result and a mathematical condition sufficient to eliminate dynamic padding for all metadata values. | +| Trailing size, padding, capacity, and advancement | Independent unbounded size formulas, exact checked-size overflow, wrapping padding, and byte advancement. | +| Size-sequence comparison | A positive answer establishes equal sizes for every natural metadata value. | +| Zero-stride conversion and element capacity | Exact zero handling, preserved representation fields, and greatest fitting element count. | +| `DstLayout` constructors, extension, and padding | Exact fields, field placement, alignment, flags, and normalized size formulas. The record constructor terminates for arbitrary field lists satisfying the independent construction domain. | +| Static and dynamic padding queries | Exact flag result and the mathematical condition sufficient to eliminate dynamic padding for all metadata values. | | Cast validation and exact-size metadata | Alignment/size error priority, greatest fitting metadata, exact prefix/suffix split, and rejection of unattainable sizes. | -Every registered function uses total `spec`: accepted raw representations, -supplied mathematical ghosts, and explicit requirements imply successful -termination, successful output decoding, and the postconditions. These are -quantified conditional contracts, not finite test inputs. Broader ordinary Raw -lemmas retain useful representation-level domains. - -`Corollaries.lean` composes the arithmetic proofs: extrema preserve a shared -predicate, and round-down is monotone, aligned and idempotent under its stated -conditions. - -`LayoutMath.lean` supplies independent unbounded size and capacity formulas. - -The mathematical layout semantics proves normalization across arbitrary -nesting and metadata values. These algebraic laws do not themselves verify -a Rust layout method. - -The nominal rounding wrapper decodes to `RoundingValue`, a power-of-two -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. - -The checked trailing-size and padding contracts connect machine arithmetic -to the independent recursive semantics. - -Extension and normalized padding preserve complete inner sizes, including -padding inside packed fields. +All registered specifications use total `spec`: accepted input representations +and their stated requirements imply successful termination, a valid returned +value, and their postconditions. Intentional panic for +casting a zero-stride DST is checked separately. The size-sequence comparison +is conservative: a negative result does not claim that the sequences differ. + +`LayoutMath.lean` defines an independent recursive layout semantics and proves +normalization correct for every nesting depth and metadata value. The extracted +contracts connect machine arithmetic and control flow to that mathematics. +`LayoutModel.lean` supplies shared interpretation predicates, without using +any function proof. `Corollaries.lean` connects checked sizes and physical +padding to the recursive semantics, proves that outer padding preserves +complete inner sizes, and connects the record constructor to direct +per-metadata field placement. +See [SEMANTICS.md](SEMANTICS.md) for the exact Rust premise and trust boundary. + +The nested Rust reference starts with `metadata * element_size`, then places +each complete inner record at a remainder-based aligned offset and rounds the +containing size. Its equivalence harness constructs the production layout and +compares the complete `Option` result, including overflow. It handles +arbitrary nesting, zero-size tails, and every machine-word metadata count. +The construction guards are visible in Rust: invalid descriptors, excessive +alignment, and static layouts that do not fit return before construction. +The tail harnesses additionally compare capacity, exact-size metadata, and both +successful cast splits and alignment/size errors. Their explicit witnesses let +reviewers read alignment and phase directly instead of decoding a stored word. +The original mathematical helper theorems retain their broader natural-number +domains; these Rust harnesses quantify the machine-word arguments Rust receives. +The composition harnesses compare extension, padding, and arbitrary field-list +construction, including every stored field and the shallow-padding flag. The +transformation harnesses compare byte advancement, wrapping padding, dynamic +padding queries, and checked sizes after a positive size-sequence answer. The +existing sequence theorem additionally preserves its unbounded size equality; +equality of checked optional sizes alone would lose differences after overflow. -A positive size-sequence comparison establishes equal sizes for every natural -metadata value; a negative result does not assert that the sequences differ. +The inline checks in `layout/cast_from.rs` cover numerical cast composition. +They select a production `CastPlan`, require the checked metadata calculation +to succeed, compare it with the actual unchecked conversion, and compare +complete sizes using the independent remainder-based reference. Metadata +representability follows from a representable complete source size; it is not +an assumed harness precondition. The proof covers all three accepted plan +variants. Rejected plans carry no completeness promise, and the typed pointer +adapter's provenance and `KnownLayout` obligations remain outside this proof. -Cast validation and exact metadata inference establish error priority, exact -splits and rejection of unattainable sizes. Intentional zero-stride panic is -checked separately. +The constructor's requirements check field alignment, the independent prefix +layout's overflow bounds, canonical encodings, and final padding bounds. These +are predicates over the mathematical construction, not assumptions that the +Rust constructor returned a correct result. Fragment operations have explicit +fit requirements; arbitrary malformed internal layout records need not succeed. +Generic size/alignment reads are explicit external data inputs, never axioms +asserting layout correctness. 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 -automatic input and output decoding. - -CI uses the default features, debug assertions and the runner's native target. -Local replay also supports macOS arm64. These conditional contracts do not -certify other extraction configurations, rustc, zerocopy's pointer safety or -whole-crate unsafe behavior. +and, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping +raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary +unbounded mathematics. Explicit `(raw)` clauses retain the extracted scalar +operations, whose checked arithmetic returns execution `Result` values. +Operation-specific power-of-two alignment and overflow bounds remain explicit +requirements. + +CI uses the default features, debug assertions, and the runner's native +`x86_64-unknown-linux-gnu` target. Local replay also supports macOS arm64. The +proofs cover all registered layout methods under their stated domains; +they do not certify other extraction configurations, a rustc implementation, +or zerocopy's pointer safety. The explicit Rust premise connects the recursive +semantics to an actual type's layout. Compiler regression tests challenge that +premise independently of the Lean algebra. Aeneas currently targets a safe Rust +subset; whole-crate unsafe verification is a separate task. ## Shared mathematical library @@ -428,7 +451,7 @@ Rust. Charon's root identity, exact source body, source path, and signature must match the annotation, including inherent Self types and inactive `cfg` alternatives. Discovery retains exact inspected source snapshots; later digest, binding, and assembly steps reject changes to any inspected input. The source -digest includes unannotated dependency files. Every +digest includes all inspected crate Rust sources and reserved-fence candidates. Every contents-bearing Charon-local file must agree with its inspected snapshot, so an unchanged caller cannot hide a changed dependency. Pinned external `/rustc` files without source contents remain within the translation premise. @@ -437,24 +460,26 @@ variables, with no swapping, coercion, or substitution. Introduced signatures ar inspectable in the generated Lean propositions and native editor. The source annotations determine the extraction roots. Removing an annotation -and its associated proof intentionally removes that claim from the checked set; +and its associated proofs intentionally removes that claim from the checked set; the source and generated golden changes make the reduced coverage reviewable. There is no separately maintained function or type coverage roster. Nominal -types are still registered and audited independently from their specifications. - -Every present function annotation must match its exact extracted function. -Called functions and constants remain part of the complete dependency model. -Model -names, theorem identities, filenames, and dependency edges are derived rather -than stored as additional synchronized inventory fields. Discovery scans all -repository Rust sources except generated and vendored directories. A Rust -lexer distinguishes comments from strings and `syn` establishes ownership -before conditional compilation. +types used by extracted functions retain their exact source mapping and +structural model checks, including unannotated dependency types. + +Model names, theorem identities, filenames, and dependency edges are derived +from the present annotations and verified extraction. Discovery inspects all +`zerocopy/src` Rust sources and reserved-fence candidates elsewhere in the +repository, except generated and vendored directories. A Rust lexer distinguishes +comments from strings and `syn` establishes ownership before conditional +compilation. A present fence on an unsupported owner, including one hidden in a +macro, fails discovery; unannotated macros and impls keep their ordinary Rust +meaning. Every function extraction root must match a present function annotation. No parser can recognize every informal prose claim as a proof. The `aeneas` -fence is the reserved CI-checked convention. Near-miss guard detection and the -independent policy protect that convention without treating all mathematical -prose as annotations. +fence is the reserved CI-checked convention. Near-miss guard detection protects +that convention without treating all mathematical prose as annotations. CI +checks every present specification on both the golden and live models so an +owned fence cannot escape proof checking or the compiled binding and axiom audits. ## Native Lean proofs and independent checks @@ -516,6 +541,11 @@ exact-size metadata, the required outcomes spell out error priority, split positions, exact size, and greatest-fitting metadata independently of the predicates used by the inline specs. `OutcomeTests.lean` pins distinguishing fixed-size, suffix-alignment, and padded-size plateau examples. +`LayoutModelDomainTests.lean` also establishes concrete admitted constructor +inputs and exact views for an ordinary record and a nested packed DST. These +bounded examples guard against vacuous preconditions; they do not establish +that every Rust type meets the construction domain. + `Check.lean` derives dependencies from elaborated theorem types and terms, following helpers across handwritten modules, including private helpers, and writes `proof-dependencies.json` in each proof workspace. It imports and audits all @@ -665,7 +695,8 @@ regenerates specifications and builds both models in fresh isolated projects. Checked addition, subtraction, and multiplication already have upstream `step_pure` specifications. Use `step as ⟨result, facts⟩` and split the `Option` result to obtain both the exact successful value and the overflow condition. -`SupportTests.lean` exercises all inputs, including overflow. +`SupportTests.lean` exercises all inputs, including overflow. Layout proofs use +these registrations directly, without naming bitvector specification lemmas. A contract may express equality through a pure mathematical view: @@ -687,9 +718,12 @@ registry then lets callers use `step` without specifying the theorem manually. `AeneasContracts.indexed_loop_spec` specializes Aeneas's `loop.spec_decr_nat` to a state and `Usize` index. Supply a view, the mathematical value of each prefix, and a representation invariant. Each continuing body step must advance -the index by exactly one and establish the next prefix; a completed step must -be at the length. The adapter supplies bounds and the decreasing `length - index` -termination measure. `SupportTests.lean` contains an independent example. +the index by +exactly one and establish the next prefix; a completed step must be at the +length. The adapter supplies bounds and the decreasing `length - index` +termination measure. The record constructor instantiates this rule; its body +proof still establishes the arithmetic bounds needed to avoid Rust overflow. +`SupportTests.lean` contains a smaller independent example. The specification syntax, examples, and required-contract proof terms participate in the axiom audit. Failure controls challenge an incorrect view, @@ -729,7 +763,7 @@ additional generated files, changes to external-template signatures, and code changes fail with a normalized diff and require regeneration. CI compiles the checked-in model and the unmodified live model in separate fresh -Lake workspaces. Both must prove all inline specifications and any checked-in composition +Lake workspaces. Both must prove all inline specifications and composition corollaries and pass required checks and the complete axiom audit. The normalized text is used only for comparison, never compilation. This independently checks that accepted differences preserve the proved properties; it does not by itself @@ -854,14 +888,3 @@ checking its signature; no formatting proposition or behavior is assumed. A change to a proposition or a function fails the audit. The PhantomData model likewise records its zero runtime fields, with a Lean shape theorem that fails if extraction adds fields; it makes no ownership or provenance claim. - -## Numerical cast composition - -The inline checks in `layout/cast_from.rs` cover numerical cast composition. -They select a production `CastPlan`, require the checked metadata calculation -to succeed, compare it with the actual unchecked conversion, and compare -complete sizes using the independent remainder-based reference. Metadata -representability follows from a representable complete source size; it is not -an assumed harness precondition. The proof covers all three accepted plan -variants. Rejected plans carry no completeness promise, and the typed pointer -adapter's provenance and `KnownLayout` obligations remain outside this proof. diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md index 9ebdc845bc..76ae48953e 100644 --- a/verification/aeneas/SEMANTICS.md +++ b/verification/aeneas/SEMANTICS.md @@ -34,11 +34,21 @@ several different metadata values can have the same complete padded size. 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. +field lists in the construction domain. `constructor_matches_record` connects +the extracted, terminating record constructor to this rule and final rounding. ## Explicit Rust premise +The Rust reference in `zerocopy/src/layout/nested_reference.rs` follows the same +recursive rule using checked machine arithmetic and remainder-based rounding. +`assert_matches_dst_layout` compares its complete optional size with the +production layout for arbitrary nesting and metadata. A total unit contract +checks the assertions themselves, including equality when both computations +overflow. Its early returns describe the construction domain in Rust. Other +Rust harnesses compare primitive fields, trailing sizes, capacity, metadata, +and cast results. They make these application claims readable without inspecting +the out-of-line Lean proofs that establish them. + 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 @@ -104,9 +114,9 @@ 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. +it into a power-of-two alignment and a bounded phase; structural layout models +reuse that shared pair. This admission law requires its ordinary Lean proof and +does not change the extracted raw implementation. The extracted cast metadata helper uses Rust's unsafe `usize::unchecked_mul` and `usize::unchecked_add`. Their handwritten external models use Aeneas's @@ -128,6 +138,7 @@ 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 diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 42060c202d..07befed82d 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -951,7 +951,7 @@ def layout.RoundingAlignAndPhase.align ok nz /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::validate_cast_and_convert_metadata]: - Source: 'src/layout/mod.rs', lines 1839:4-1986:5 -/ + Source: 'src/layout/mod.rs', lines 1854:4-2001:5 -/ def layout.DstLayout.validate_cast_and_convert_metadata (self : layout.DstLayout) (addr : Std.Usize) (bytes_len : Std.Usize) (cast_type : layout.CastType) : @@ -1022,7 +1022,7 @@ def layout.DstLayout.validate_cast_and_convert_metadata ok (core.result.Result.Ok (elems, split_at)) /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::metadata_for_exact_size]: - Source: 'src/layout/mod.rs', lines 1701:4-1724:5 -/ + Source: 'src/layout/mod.rs', lines 1716:4-1739:5 -/ def layout.DstLayout.metadata_for_exact_size (self : layout.DstLayout) (size : Std.Usize) : Result (Option Std.Usize) @@ -1164,7 +1164,7 @@ def layout.cast_from.CastPlan.try_compute else ok none /-- [zerocopy::layout::add_scaled_metadata]: - Source: 'src/layout/mod.rs', lines 2008:0-2082:1 -/ + Source: 'src/layout/mod.rs', lines 2023:0-2097:1 -/ def layout.add_scaled_metadata (base : Std.Usize) (metadata : Std.Usize) (multiple : Std.Usize) : Result Std.Usize @@ -1603,6 +1603,78 @@ def layout.composition_checks.reference_pad else ok none else ok none +/-- [zerocopy::layout::composition_checks::reference_constructor]: loop body 0: + Source: 'src/layout/composition_checks.rs', lines 213:4-219:5 -/ +@[rust_loop_body] +def layout.composition_checks.reference_constructor_loop.body + (packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) + (fields : Slice layout.composition_checks.ReferenceLayout) + (state : Option layout.composition_checks.ReferenceLayout) (i : Std.Usize) : + Result (ControlFlow ((Option layout.composition_checks.ReferenceLayout) × + Std.Usize) (Option layout.composition_checks.ReferenceLayout)) + := do + let i1 := Slice.len fields + if i < i1 + then + let state1 ← + match state with + | none => ok none + | some preceding => + do + let rl ← Slice.index_usize fields i + layout.composition_checks.reference_extend preceding rl packed + let i2 ← i + 1#usize + ok (cont (state1, i2)) + else ok (done state) + +/-- [zerocopy::layout::composition_checks::reference_constructor]: loop 0: + Source: 'src/layout/composition_checks.rs', lines 213:4-219:5 -/ +@[rust_loop] +def layout.composition_checks.reference_constructor_loop + (packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) + (fields : Slice layout.composition_checks.ReferenceLayout) + (state : Option layout.composition_checks.ReferenceLayout) (i : Std.Usize) : + Result (Option layout.composition_checks.ReferenceLayout) + := do + loop + (fun (state1, i1) => + layout.composition_checks.reference_constructor_loop.body packed fields + state1 i1) + (state, i) + +/-- [zerocopy::layout::composition_checks::reference_constructor]: + Source: 'src/layout/composition_checks.rs', lines 199:0-224:1 -/ +def layout.composition_checks.reference_constructor + (repr_align : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) + (packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) + (fields : Slice layout.composition_checks.ReferenceLayout) : + Result (Option layout.composition_checks.ReferenceLayout) + := do + let align ← + match repr_align with + | none => ok 1#usize + | some align1 => + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align1 + let b ← layout.composition_checks.extension_alignment align + if b + then + let state ← + layout.composition_checks.reference_constructor_loop packed fields (some + { + align, + size := (layout.composition_checks.ReferenceSize.Fixed 0#usize), + unpadded := true + }) 0#usize + match state with + | none => ok none + | some reference => layout.composition_checks.reference_pad reference + else ok none + /-- [zerocopy::util::min]: Source: 'src/util/mod.rs', lines 306:0-312:1 -/ def util.min @@ -1678,7 +1750,7 @@ def layout.DstLayout.THEORETICAL_MAX_ALIGN | some max_align => ok max_align /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::extend]: - Source: 'src/layout/mod.rs', lines 1330:4-1476:5 + Source: 'src/layout/mod.rs', lines 1345:4-1491:5 Visibility: public -/ def layout.DstLayout.extend (self : layout.DstLayout) (field : layout.DstLayout) @@ -1805,7 +1877,7 @@ def layout.DstLayout.extend | layout.SizeInfo.SliceDst _ => fail panic /-- [zerocopy::layout::composition_checks::check_extend]: - Source: 'src/layout/composition_checks.rs', lines 203:0-218:1 -/ + Source: 'src/layout/composition_checks.rs', lines 233:0-248:1 -/ def layout.composition_checks.check_extend (preceding : layout.DstLayout) (field : layout.DstLayout) (packed : Option (core.num.nonzero.NonZero Std.Usize @@ -1835,7 +1907,7 @@ def layout.composition_checks.check_extend else ok () /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::pad_to_align]: - Source: 'src/layout/mod.rs', lines 1512:4-1602:5 + Source: 'src/layout/mod.rs', lines 1527:4-1617:5 Visibility: public -/ def layout.DstLayout.pad_to_align (self : layout.DstLayout) : Result layout.DstLayout := do @@ -1940,7 +2012,7 @@ def layout.DstLayout.pad_to_align } /-- [zerocopy::layout::composition_checks::check_pad]: - Source: 'src/layout/composition_checks.rs', lines 226:0-233:1 -/ + Source: 'src/layout/composition_checks.rs', lines 256:0-263:1 -/ def layout.composition_checks.check_pad (runtime_layout : layout.DstLayout) (reference : layout.composition_checks.ReferenceLayout) : @@ -1974,12 +2046,6 @@ def layout.DstLayout.MIN_ALIGN | none => fail panic | some min_align => ok min_align -/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::assume_shallow_unpadded]: - Source: 'src/layout/mod.rs', lines 996:4-1005: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 1034:4-1054:5 Visibility: public -/ @@ -2004,6 +2070,132 @@ def layout.DstLayout.new_zst statically_shallow_unpadded := true } +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_repr_c_struct]: loop body 0: + Source: 'src/layout/mod.rs', lines 1277:8-1282:9 + Visibility: public -/ +@[rust_loop_body] +def layout.DstLayout.for_repr_c_struct_loop.body + (repr_packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) (fields : Slice layout.DstLayout) + (result : layout.DstLayout) (i : Std.Usize) : + Result (ControlFlow (layout.DstLayout × Std.Usize) layout.DstLayout) + := do + let i1 := Slice.len fields + if i < i1 + then + let field ← Slice.index_usize fields i + let result1 ← layout.DstLayout.extend result field repr_packed + let i2 ← i + 1#usize + ok (cont (result1, i2)) + else ok (done result) + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_repr_c_struct]: loop 0: + Source: 'src/layout/mod.rs', lines 1277:8-1282:9 + Visibility: public -/ +@[rust_loop] +def layout.DstLayout.for_repr_c_struct_loop + (repr_packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) (fields : Slice layout.DstLayout) + (result : layout.DstLayout) (i : Std.Usize) : + Result layout.DstLayout + := do + loop + (fun (result1, i1) => layout.DstLayout.for_repr_c_struct_loop.body + repr_packed fields result1 i1) + (result, i) + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_repr_c_struct]: + Source: 'src/layout/mod.rs', lines 1253:4-1299:5 + Visibility: public -/ +def layout.DstLayout.for_repr_c_struct + (repr_align : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) + (repr_packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) (fields : Slice layout.DstLayout) : + Result layout.DstLayout + := do + let result ← layout.DstLayout.new_zst repr_align + let result1 ← + layout.DstLayout.for_repr_c_struct_loop repr_packed fields result 0#usize + layout.DstLayout.pad_to_align result1 + +/-- [zerocopy::layout::composition_checks::check_constructor]: loop body 0: + Source: 'src/layout/composition_checks.rs', lines 282:4-285:5 -/ +@[rust_loop_body] +def layout.composition_checks.check_constructor_loop.body + (fields : Slice layout.DstLayout) + (references : Slice layout.composition_checks.ReferenceLayout) + (matching : Bool) (i : Std.Usize) : + Result (ControlFlow (Bool × Std.Usize) Bool) + := do + let i1 := Slice.len fields + if i < i1 + then + let matching1 ← + if matching + then + do + let dl ← Slice.index_usize fields i + let rl ← Slice.index_usize references i + layout.composition_checks.matches_reference dl rl + else ok false + let i2 ← i + 1#usize + ok (cont (matching1, i2)) + else ok (done matching) + +/-- [zerocopy::layout::composition_checks::check_constructor]: loop 0: + Source: 'src/layout/composition_checks.rs', lines 282:4-285:5 -/ +@[rust_loop] +def layout.composition_checks.check_constructor_loop + (fields : Slice layout.DstLayout) + (references : Slice layout.composition_checks.ReferenceLayout) + (matching : Bool) (i : Std.Usize) : + Result Bool + := do + loop + (fun (matching1, i1) => + layout.composition_checks.check_constructor_loop.body fields references + matching1 i1) + (matching, i) + +/-- [zerocopy::layout::composition_checks::check_constructor]: + Source: 'src/layout/composition_checks.rs', lines 271:0-292:1 -/ +def layout.composition_checks.check_constructor + (repr_align : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) + (packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) (fields : Slice layout.DstLayout) + (references : Slice layout.composition_checks.ReferenceLayout) : + Result Unit + := do + let i := Slice.len fields + let i1 := Slice.len references + if i != i1 + then ok () + else + let matching ← + layout.composition_checks.check_constructor_loop fields references true + 0#usize + if matching + then + let o ← + layout.composition_checks.reference_constructor repr_align packed + references + match o with + | none => ok () + | some expected => + let actual ← + layout.DstLayout.for_repr_c_struct repr_align packed fields + let b ← layout.composition_checks.matches_reference actual expected + massert b + else ok () + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::assume_shallow_unpadded]: + Source: 'src/layout/mod.rs', lines 996:4-1005: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}::for_type]: Source: 'src/layout/mod.rs', lines 1078:4-1103:5 Visibility: public -/ @@ -2058,14 +2250,14 @@ def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::requires_static_padding]: - Source: 'src/layout/mod.rs', lines 1619:4-1628:5 + Source: 'src/layout/mod.rs', lines 1634:4-1643:5 Visibility: public -/ def layout.DstLayout.requires_static_padding (self : layout.DstLayout) : Result Bool := do ok (¬ self.statically_shallow_unpadded) /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::requires_dynamic_padding]: - Source: 'src/layout/mod.rs', lines 1652:4-1678:5 + Source: 'src/layout/mod.rs', lines 1667:4-1693:5 Visibility: public -/ def layout.DstLayout.requires_dynamic_padding (self : layout.DstLayout) : Result Bool := do @@ -2090,7 +2282,7 @@ def layout.DstLayout.requires_dynamic_padding else ok (¬ (i1 = 0#usize)) /-- [zerocopy::layout::nested_reference::round_up]: - Source: 'src/layout/nested_reference.rs', lines 46:0-56:1 -/ + Source: 'src/layout/nested_reference.rs', lines 52:0-62:1 -/ def layout.nested_reference.round_up (size : Std.Usize) (align : Std.Usize) : Result (Option Std.Usize) := do if align = 0#usize @@ -2103,7 +2295,7 @@ def layout.nested_reference.round_up ok (Usize.checked_add size i) /-- [zerocopy::layout::nested_reference::apply_layer]: - Source: 'src/layout/nested_reference.rs', lines 58:0-80:1 -/ + Source: 'src/layout/nested_reference.rs', lines 64:0-86:1 -/ def layout.nested_reference.apply_layer (layer : layout.nested_reference.NestedLayer) (size : Std.Usize) (alignment : Std.Usize) : @@ -2143,7 +2335,7 @@ def layout.nested_reference.apply_layer else ok none /-- [zerocopy::layout::nested_reference::size_for_metadata]: loop body 0: - Source: 'src/layout/nested_reference.rs', lines 108:4-115:5 -/ + Source: 'src/layout/nested_reference.rs', lines 114:4-121:5 -/ @[rust_loop_body] def layout.nested_reference.size_for_metadata_loop.body (leading : Slice layout.nested_reference.NestedLayer) @@ -2164,7 +2356,7 @@ def layout.nested_reference.size_for_metadata_loop.body else ok (done state) /-- [zerocopy::layout::nested_reference::size_for_metadata]: loop 0: - Source: 'src/layout/nested_reference.rs', lines 108:4-115:5 -/ + Source: 'src/layout/nested_reference.rs', lines 114:4-121:5 -/ @[rust_loop] def layout.nested_reference.size_for_metadata_loop (leading : Slice layout.nested_reference.NestedLayer) @@ -2177,7 +2369,7 @@ def layout.nested_reference.size_for_metadata_loop (state, i) /-- [zerocopy::layout::nested_reference::size_for_metadata]: - Source: 'src/layout/nested_reference.rs', lines 94:0-120:1 -/ + Source: 'src/layout/nested_reference.rs', lines 100:0-126:1 -/ def layout.nested_reference.size_for_metadata (leading : Slice layout.nested_reference.NestedLayer) (elem_size : Std.Usize) (leaf_align : Std.Usize) (elems : Std.Usize) : @@ -2204,6 +2396,196 @@ def layout.nested_reference.size_for_metadata ok (some size) else ok none +/-- [zerocopy::layout::nested_reference::assert_matches_dst_layout]: loop body 0: + Source: 'src/layout/nested_reference.rs', lines 158:4-168:5 -/ +@[rust_loop_body] +def layout.nested_reference.assert_matches_dst_layout_loop0.body + (nz : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) + (leading : Slice layout.nested_reference.NestedLayer) (i : Std.Usize) + (valid : Bool) : + Result (ControlFlow (Std.Usize × Bool) Bool) + := do + let i1 := Slice.len leading + if i < i1 + then + let layer ← Slice.index_usize leading i + let b ← core.num.Usize.is_power_of_two layer.packed + let valid1 ← + if b + then + do + let b1 ← core.num.Usize.is_power_of_two layer.min_align + if b1 + then + if layer.min_align > layer.packed + then ok false + else + let i2 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz + if layer.packed > i2 + then ok false + else ok valid + else ok false + else ok false + let i2 ← i + 1#usize + ok (cont (i2, valid1)) + else ok (done valid) + +/-- [zerocopy::layout::nested_reference::assert_matches_dst_layout]: loop 0: + Source: 'src/layout/nested_reference.rs', lines 158:4-168:5 -/ +@[rust_loop] +def layout.nested_reference.assert_matches_dst_layout_loop0 + (nz : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) + (leading : Slice layout.nested_reference.NestedLayer) (i : Std.Usize) + (valid : Bool) : + Result Bool + := do + loop + (fun (i1, valid1) => + layout.nested_reference.assert_matches_dst_layout_loop0.body nz leading + i1 valid1) + (i, valid) + +/-- [zerocopy::layout::nested_reference::assert_matches_dst_layout]: loop body 1: + Source: 'src/layout/nested_reference.rs', lines 190:4-208:5 -/ +@[rust_loop_body] +def layout.nested_reference.assert_matches_dst_layout_loop1.body + (leading : Slice layout.nested_reference.NestedLayer) + (runtime_layout : layout.DstLayout) (i : Std.Usize) : + Result (ControlFlow (layout.DstLayout × Std.Usize) layout.DstLayout) + := do + if i != 0#usize + then + let i1 ← i - 1#usize + let layer ← Slice.index_usize leading i1 + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + layer.packed + let packed ← + match o with + | none => layout.DstLayout.MIN_ALIGN + | some a => ok a + let o1 ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + layer.min_align + let min_align ← + match o1 with + | none => layout.DstLayout.MIN_ALIGN + | some a => ok a + let nz ← layout.DstLayout.MIN_ALIGN + let s ← + lift (Array.to_slice + (Array.make 2#usize [ + ({ + align := nz, + size_info := (layout.SizeInfo.Sized layer.prefix_bytes), + statically_shallow_unpadded := true + } : layout.DstLayout), runtime_layout + ])) + let runtime_layout1 ← + layout.DstLayout.for_repr_c_struct (some min_align) (some packed) s + ok (cont (runtime_layout1, i1)) + else ok (done runtime_layout) + +/-- [zerocopy::layout::nested_reference::assert_matches_dst_layout]: loop 1: + Source: 'src/layout/nested_reference.rs', lines 190:4-208:5 -/ +@[rust_loop] +def layout.nested_reference.assert_matches_dst_layout_loop1 + (leading : Slice layout.nested_reference.NestedLayer) + (runtime_layout : layout.DstLayout) (i : Std.Usize) : + Result layout.DstLayout + := do + loop + (fun (runtime_layout1, i1) => + layout.nested_reference.assert_matches_dst_layout_loop1.body leading + runtime_layout1 i1) + (runtime_layout, i) + +/-- [zerocopy::layout::nested_reference::assert_matches_dst_layout]: + Source: 'src/layout/nested_reference.rs', lines 144:0-221:1 -/ +def layout.nested_reference.assert_matches_dst_layout + (leading : Slice layout.nested_reference.NestedLayer) (elem_size : Std.Usize) + (leaf_align : Std.Usize) (elems : Std.Usize) : + Result Unit + := do + let b ← core.num.Usize.is_power_of_two leaf_align + if b + then + let nz ← layout.DstLayout.CURRENT_MAX_ALIGN + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz + if leaf_align > i + then ok () + else + let i1 ← elem_size % leaf_align + if i1 != 0#usize + then ok () + else + let valid ← + layout.nested_reference.assert_matches_dst_layout_loop0 nz leading + 0#usize true + if valid + then + let o ← + layout.nested_reference.size_for_metadata leading elem_size + leaf_align 0#usize + let b1 := core.option.Option.is_none o + if b1 + then ok () + else + let o1 ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + leaf_align + match o1 with + | none => ok () + | some a => + let raap ← layout.RoundingAlignAndPhase.new a 0#usize + let i2 := Slice.len leading + let runtime_layout ← + layout.nested_reference.assert_matches_dst_layout_loop1 leading + { + align := a, + size_info := + (layout.SizeInfo.SliceDst + { + offset := 0#usize, + elem_size, + size_base := 0#usize, + size_rounding_align_and_phase := raap + }), + statically_shallow_unpadded := true + } i2 + let actual ← + match runtime_layout.size_info with + | layout.SizeInfo.Sized size => ok (some size) + | layout.SizeInfo.SliceDst tail => + layout.TrailingSliceLayoutUsize.size_for_elems tail elems + let i3 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + a + let expected ← + layout.nested_reference.size_for_metadata leading elem_size i3 + elems + match actual with + | none => + match expected with + | none => ok () + | some _ => fail panic + | some actual1 => + match expected with + | none => fail panic + | some expected1 => massert (actual1 = expected1) + else ok () + else ok () + /-- [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 diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 3d04b8065c..58f0c71473 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -178,7 +178,7 @@ structure layout.composition_checks.ReferenceLayout where unpadded : Bool /-- [zerocopy::layout::nested_reference::NestedLayer] - Source: 'src/layout/nested_reference.rs', lines 27:0-31:1 -/ + Source: 'src/layout/nested_reference.rs', lines 33:0-37:1 -/ structure layout.nested_reference.NestedLayer where packed : Std.Usize min_align : Std.Usize diff --git a/verification/aeneas/lean/CompositionConstructor.lean b/verification/aeneas/lean/CompositionConstructor.lean new file mode 100644 index 0000000000..25fc02b3a8 --- /dev/null +++ b/verification/aeneas/lean/CompositionConstructor.lean @@ -0,0 +1,352 @@ +/- 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 CompositionReference +@[expose] public section + +/-! +The constructor has two ordinary Rust loops: one checks every supplied witness, +then the independent constructor folds Option-valued checked field placement. +The invariants below retain all completed append domains, including failure +propagation, so final success cannot silently skip an overflowing field. +-/ +open Aeneas Aeneas.Std +namespace Zerocopy.CompositionReference +open Zerocopy.Proofs +set_option linter.unusedSimpArgs false + +def fieldsMatchThrough (fields : Slice layout.DstLayout) (references : Slice ReferenceLayout) + (count : Nat) : Prop := + ∀ j (hf : j < fields.val.length) (hr : j < references.val.length), j < count → + Matches fields.val[j] references.val[j] + +theorem fieldsMatchThrough_succ (fields : Slice layout.DstLayout) (references : Slice ReferenceLayout) + (i : Nat) (hf : i < fields.val.length) (hr : i < references.val.length) : + fieldsMatchThrough fields references (i + 1) ↔ + fieldsMatchThrough fields references i ∧ Matches fields.val[i] references.val[i] := by + constructor + · intro all + exact ⟨fun j hj hrj before => all j hj hrj (by omega), all i hf hr (by omega)⟩ + · rintro ⟨before, current⟩ j hj hrj next + by_cases old : j < i + · exact before j hj hrj old + · have same : j = i := by omega + subst j + exact current + +def referencePrefix (fields : Slice ReferenceLayout) (minimum : Nat) + (packed : Option NonZeroUsize) (i : Nat) : LayoutMath.LayoutValue := + LayoutMath.LayoutValue.prefixValue (fields.val.map value) (LayoutMath.LayoutValue.initial minimum) + (packingValue packed) i + +def referenceHistory (fields : Slice ReferenceLayout) (minimum : Nat) + (packed : Option NonZeroUsize) (count : Nat) : Prop := + ∀ j (hj : j < fields.val.length), j < count → + alignmentDomain (referencePrefix fields minimum packed j).align ∧ + alignmentDomain fields.val[j].align.val ∧ valid fields.val[j] ∧ + (referencePrefix fields minimum packed j).extendFits (value fields.val[j]) + (packingValue packed) Usize.max + +def referenceState (fields : Slice ReferenceLayout) (minimum : Nat) + (packed : Option NonZeroUsize) (state : Option ReferenceLayout) (i : Nat) : Prop := + ∀ current, state = some current → + value current = referencePrefix fields minimum packed i ∧ valid current ∧ + alignmentDomain current.align.val ∧ + (0 < i → ∀ a ∈ packed, alignmentDomain a.val.val) ∧ + referenceHistory fields minimum packed i + +theorem referencePrefix_step (fields : Slice ReferenceLayout) (minimum : Nat) + (packed : Option NonZeroUsize) (i : Nat) (hi : i < fields.val.length) : + referencePrefix fields minimum packed (i + 1) = + (referencePrefix fields minimum packed i).extend (value fields.val[i]) (packingValue packed) := by + unfold referencePrefix + rw [LayoutMath.LayoutValue.prefixValue_step (fields.val.map value) + (LayoutMath.LayoutValue.initial minimum) (packingValue packed) i (by simpa using hi)] + simp only [List.getElem_map] + +theorem max_domain (a b : Nat) (ha : alignmentDomain a) (hb : alignmentDomain b) : + alignmentDomain (max a b) := by + rcases le_total a b with h | h + · simpa only [max_eq_right h] using hb + · simpa only [max_eq_left h] using ha + +theorem packed_domain (field : Nat) (packed : Option NonZeroUsize) + (hf : alignmentDomain field) (hp : ∀ a ∈ packed, alignmentDomain a.val.val) : + alignmentDomain (min field (packingValue packed)) := by + cases packed with + | none => + have limit : 2 ^ 29 ≤ packingValue none := by + rcases System.Platform.numBits_eq with h | h <;> simp [packingValue, h] + have bound := hf.2 + simpa only [min_eq_left (show field ≤ packingValue none by omega)] using hf + | some cap => + have hc := hp cap rfl + rcases le_total field cap.val.val with h | h + · simpa only [packingValue, Option.map_some, Option.getD_some, min_eq_left h] using hf + · simpa only [packingValue, Option.map_some, Option.getD_some, min_eq_right h] using hc + +theorem extended_domain (preceding field : LayoutMath.LayoutValue) (packed : Option NonZeroUsize) + (ha : alignmentDomain preceding.align) (hf : alignmentDomain field.align) + (hp : ∀ a ∈ packed, alignmentDomain a.val.val) + (fit : preceding.extendFits field (packingValue packed) Usize.max) : + alignmentDomain (preceding.extend field (packingValue packed)).align := by + cases hs : preceding.payload with + | trailing _ => simp [LayoutMath.LayoutValue.extendFits, hs] at fit + | fixed _ => + simpa only [LayoutMath.LayoutValue.extend, hs] using max_domain _ _ ha (packed_domain _ _ hf hp) + +end Zerocopy.CompositionReference + +namespace Zerocopy.Proofs.Raw +open Zerocopy.CompositionReference +set_option linter.unusedSimpArgs false + +theorem composition_matching_loop_spec (fields : Slice layout.DstLayout) + (references : Slice ReferenceLayout) (lengths : fields.val.length = references.val.length) + (matching : Bool) (i : Usize) (hi : i.val ≤ fields.val.length) + (hv : (matching = true) = fieldsMatchThrough fields references i.val) : + layout.composition_checks.check_constructor_loop fields references matching i + ⦃ out => (out = true) = fieldsMatchThrough fields references fields.val.length ⦄ := by + unfold layout.composition_checks.check_constructor_loop + apply WP.spec_mono (AeneasContracts.indexed_loop_spec fields.val.length + (fun b : Bool => b = true) (fieldsMatchThrough fields references) (fun _ => True) _ + ?_ matching i hi hv trivial) + · intro out facts + exact facts.1 + · intro matching idx hi hv _ + unfold layout.composition_checks.check_constructor_loop.body + simp only [UScalar.lt_equiv, Slice.len_val, Slice.length, and_true] + split + · rename_i hlt + have hrl : idx.val < references.val.length := by omega + have hroom : idx.val + (1#usize).val ≤ Usize.max := by + have := fields.property + change idx.val + 1 ≤ Usize.max + omega + split + · rename_i yes + have previous : fieldsMatchThrough fields references idx.val := Eq.mp hv yes + step with Slice.index_usize_spec fields idx hlt as ⟨field, hf⟩ + step with Slice.index_usize_spec references idx hrl as ⟨reference, hr⟩ + step with composition_matches_spec field reference as ⟨checked, hc⟩ + have next_view : (checked = true) = fieldsMatchThrough fields references (idx.val + 1) := by + apply propext + rw [fieldsMatchThrough_succ fields references idx.val hlt hrl] + simpa only [previous, true_and, hf, hr] using hc + step with Usize.add_spec (x := idx) (y := 1#usize) hroom as ⟨j, hj⟩ + change j.val = idx.val + 1 at hj + simpa only [hlt, hj, true_and] using next_view + · rename_i no + simp only [bind_ok] + have next_view : (false = true) = fieldsMatchThrough fields references (idx.val + 1) := by + apply propext + rw [fieldsMatchThrough_succ fields references idx.val hlt hrl] + have np : ¬fieldsMatchThrough fields references idx.val := by + intro hp + exact no (Eq.mpr hv hp) + simp [np] + step with Usize.add_spec (x := idx) (y := 1#usize) hroom as ⟨j, hj⟩ + change j.val = idx.val + 1 at hj + simpa only [hlt, hj, true_and] using next_view + · have same : idx.val = fields.val.length := by omega + exact WP.spec.ret ⟨same, hv⟩ + +theorem composition_reference_loop_spec (packed : Option NonZeroUsize) + (fields : Slice ReferenceLayout) (minimum : Nat) (state : Option ReferenceLayout) (i : Usize) + (fields_valid : ∀ j (hj : j < fields.val.length), valid fields.val[j]) + (hi : i.val ≤ fields.val.length) (hv : referenceState fields minimum packed state i.val) : + layout.composition_checks.reference_constructor_loop packed fields state i + ⦃ out => referenceState fields minimum packed out fields.val.length ⦄ := by + unfold layout.composition_checks.reference_constructor_loop + apply loop.spec_decr_nat + (fun s : Option ReferenceLayout × Usize => fields.val.length - s.2.val) + (fun s => s.2.val ≤ fields.val.length ∧ referenceState fields minimum packed s.1 s.2.val) + · rintro ⟨state, idx⟩ ⟨hi, hv⟩ + dsimp only at hi hv + unfold layout.composition_checks.reference_constructor_loop.body + simp only [UScalar.lt_equiv, Slice.len_val, Slice.length] + split + · rename_i hlt + have hroom : idx.val + (1#usize).val ≤ Usize.max := by + have := fields.property + change idx.val + 1 ≤ Usize.max + omega + cases state with + | none => + simp only [bind_ok] + step with Usize.add_spec (x := idx) (y := 1#usize) hroom as ⟨j, hj⟩ + change j.val = idx.val + 1 at hj + refine ⟨by omega, ?_, by omega⟩ + intro expected same + cases same + | some preceding => + step with Slice.index_usize_spec fields idx hlt as ⟨field, hf⟩ + step with composition_reference_extend_spec preceding field packed as ⟨next, hn⟩ + cases next with + | none => + step with Usize.add_spec (x := idx) (y := 1#usize) hroom as ⟨j, hj⟩ + change j.val = idx.val + 1 at hj + refine ⟨by omega, ?_, by omega⟩ + intro expected same + cases same + | some next => + obtain ⟨preceding_domain, field_domain, packed_domain, fits, output, validity⟩ := hn next rfl + obtain ⟨preceding_view, _, _, _, history⟩ := hv preceding rfl + have valid_next : valid next := validity (by rw [hf]; exact fields_valid idx.val hlt) + have domain_next : alignmentDomain next.align.val := by + have domain := extended_domain (value preceding) (value field) packed preceding_domain + field_domain packed_domain fits + have alignment := congrArg LayoutMath.LayoutValue.align output + change next.align.val = _ at alignment + rw [← alignment] at domain + exact domain + have next_view : value next = referencePrefix fields minimum packed (idx.val + 1) := by + rw [referencePrefix_step fields minimum packed idx.val hlt, ← preceding_view, ← hf] + exact output + step with Usize.add_spec (x := idx) (y := 1#usize) hroom as ⟨jnext, hjnext⟩ + change jnext.val = idx.val + 1 at hjnext + refine ⟨by omega, ?_, by omega⟩ + rw [hjnext] + intro expected same + cases same + refine ⟨next_view, valid_next, domain_next, fun _ => packed_domain, ?_⟩ + intro j hj before + by_cases old : j < idx.val + · exact history j hj old + · have same : j = idx.val := by omega + subst j + refine ⟨?_, ?_, fields_valid idx.val hlt, ?_⟩ + · have alignment := congrArg LayoutMath.LayoutValue.align preceding_view + change preceding.align.val = _ at alignment + simpa only [← alignment] using preceding_domain + · simpa only [← hf] using field_domain + · simpa only [preceding_view, hf] using fits + · have same : idx.val = fields.val.length := by omega + exact WP.spec.ret (same ▸ hv) + · exact ⟨hi, hv⟩ + +theorem composition_reference_constructor_spec (repr_align packed : Option NonZeroUsize) + (fields : Slice ReferenceLayout) + (fields_valid : ∀ j (hj : j < fields.val.length), valid fields.val[j]) : + layout.composition_checks.reference_constructor repr_align packed fields + ⦃ result => ∀ expected, result = some expected → + (∀ a ∈ repr_align, alignmentDomain a.val.val) ∧ + (0 < fields.val.length → ∀ a ∈ packed, alignmentDomain a.val.val) ∧ + referenceHistory fields (initialAlignment repr_align) packed fields.val.length ∧ + alignmentDomain (referencePrefix fields (initialAlignment repr_align) packed fields.val.length).align ∧ + (referencePrefix fields (initialAlignment repr_align) packed fields.val.length).padFits Usize.max ∧ + value expected = (referencePrefix fields (initialAlignment repr_align) packed fields.val.length).pad ∧ + valid expected ⦄ := by + unfold layout.composition_checks.reference_constructor + let align : Usize := match repr_align with | none => 1#usize | some a => a.val + have alignment_read : (match (generalizing := false) repr_align with + | none => Result.ok 1#usize + | some a => core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a) = Result.ok align := by + cases repr_align <;> rfl + change (Aeneas.Std.bind (match (generalizing := false) repr_align with + | none => Result.ok 1#usize + | some a => core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a) _) ⦃ _ ⦄ + rw [alignment_read] + simp only [bind_ok] + have ha : align.val = initialAlignment repr_align := by + cases repr_align <;> simp only [align, initialAlignment, Option.map_some, + Option.getD_some, Option.map_none, Option.getD_none] + simp + step with composition_alignment_spec align as ⟨enabled, he⟩ + split + · rename_i yes + have domain := he.mp yes + have initial_domain : alignmentDomain (initialAlignment repr_align) := by rw [← ha]; exact domain + have admitted : ∀ a ∈ repr_align, alignmentDomain a.val.val := by + cases repr_align with + | none => simp + | some a => + intro b member + have same : b = a := by simpa [eq_comm] using member + subst b + simpa only [initialAlignment, Option.map_some, Option.getD_some] using initial_domain + have start : referenceState fields (initialAlignment repr_align) packed + (some ⟨align, .Fixed 0#usize, true⟩) (0#usize).val := by + intro current same + cases same + refine ⟨?_, trivial, domain, ?_, ?_⟩ + · simp only [value, referencePrefix, LayoutMath.LayoutValue.prefixValue, + LayoutMath.LayoutValue.initial, ha, show (0#usize).val = 0 by simp, + List.take_zero, List.foldl_nil] + · intro impossible + simp at impossible + · intro j hj impossible + simp at impossible + step with composition_reference_loop_spec packed fields (initialAlignment repr_align) + (some ⟨align, .Fixed 0#usize, true⟩) 0#usize fields_valid (by simp) start + as ⟨complete, completed⟩ + cases complete with + | none => simp + | some complete => + obtain ⟨view, _, final_domain, packed_domain, history⟩ := completed complete rfl + apply WP.spec_mono (composition_reference_pad_spec complete) + intro result facts expected same + obtain ⟨_, fits, output, validity⟩ := facts expected same + refine ⟨admitted, packed_domain, history, ?_, ?_, ?_, validity⟩ + · have alignment := congrArg LayoutMath.LayoutValue.align view + change complete.align.val = _ at alignment + simpa only [← alignment] using final_domain + · simpa only [view] using fits + · simpa only [view] using output + · simp + +/- Packing is read only while appending a field. The empty constructor also +terminates when its unused packing word is not an admitted power of two. -/ +theorem composition_empty_production_loop (packed : Option NonZeroUsize) + (fields : Slice layout.DstLayout) (start : layout.DstLayout) (empty : fields.val.length = 0) : + layout.DstLayout.for_repr_c_struct_loop packed fields start 0#usize ⦃ out => out = start ⦄ := by + unfold layout.DstLayout.for_repr_c_struct_loop + apply loop.spec_decr_nat (fun _ => 0) (fun s => s = (start, 0#usize)) + · intro state same + cases same + unfold layout.DstLayout.for_repr_c_struct_loop.body + simp [UScalar.lt_equiv, Slice.len_val, Slice.length, empty] + · rfl + +theorem composition_production_constructor_spec (repr_align packed : Option NonZeroUsize) + (fields : Slice layout.DstLayout) + (ha : ∀ a ∈ repr_align, alignmentDomain a.val.val) + (hp : 0 < fields.val.length → ∀ a ∈ packed, alignmentDomain a.val.val) + (hd : constructionDomain fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed) + (hlast : alignmentDomain + (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed fields.val.length).align) + (hfit : (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) + packed fields.val.length).padFits Usize.max) : + layout.DstLayout.for_repr_c_struct repr_align packed fields ⦃ r => + layoutValue r = (constructionPrefix fields (LayoutMath.LayoutValue.initial + (initialAlignment repr_align)) packed fields.val.length).pad ∧ canonicalLayout r ⦄ := by + by_cases nonempty : 0 < fields.val.length + · exact for_repr_c_struct_spec repr_align packed fields ha (hp nonempty) hd hlast hfit + · have empty : fields.val.length = 0 := by omega + unfold layout.DstLayout.for_repr_c_struct + step with new_zst_spec repr_align (fun a h => (ha a h).1) as ⟨start, halign, hsize, hunpadded⟩ + have view : layoutValue start = constructionPrefix fields + (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed fields.val.length := by + simp only [constructionPrefix, LayoutMath.LayoutValue.prefixValue, empty, + List.take_zero, List.foldl_nil, layoutValue, hsize, hunpadded, halign, + initialAlignment, LayoutMath.LayoutValue.initial] + cases repr_align <;> rfl + have canonical : canonicalLayout start := by simp only [canonicalLayout, hsize] + step with composition_empty_production_loop packed fields start empty as ⟨complete, same⟩ + subst complete + step with pad_value_spec start (by + have alignment := congrArg LayoutMath.LayoutValue.align view + change start.align.val.val = _ at alignment + rw [alignment] + exact hlast.1) canonical (by rw [view]; exact hfit) as ⟨result, output, canonical⟩ + exact ⟨by rw [output, view], canonical⟩ + +end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/Corollaries.lean b/verification/aeneas/lean/Corollaries.lean index 3c74904bff..f6a05ae8c3 100644 --- a/verification/aeneas/lean/Corollaries.lean +++ b/verification/aeneas/lean/Corollaries.lean @@ -28,7 +28,7 @@ open Aeneas Aeneas.Std Aeneas.Std.Result namespace Zerocopy.Corollaries open Proofs Proofs.Raw - +/- Selecting either input preserves any predicate shared by both inputs. -/ theorem max_preserves (a b : NonZeroUsize) (P : NonZeroUsize → Prop) (ha : P a) (hb : P b) : @@ -49,6 +49,7 @@ theorem min_preserves (a b : NonZeroUsize) (P : NonZeroUsize → Prop) · simpa only [h] using ha · simpa only [h] using hb +/-- Aligned inputs are fixed points of round-down. -/ theorem round_down_aligned (n : Usize) (align : NonZeroUsize) (hpow : (align.val : Nat).isPowerOfTwo) (haligned : (n : Nat) % (align.val : Nat) = 0) : @@ -83,6 +84,7 @@ theorem round_down_monotone (a b : Usize) (align : NonZeroUsize) apply (UScalar.le_equiv _ _).mpr exact hgreatest m.val ((UScalar.le_equiv _ _).mp (le_trans hbound hab)) haligned +/-- The original conservative headroom bound implies the exact fit bound. -/ theorem pad_to_align_sized_headroom (self : layout.DstLayout) (size : Usize) (hs : self.size_info = .Sized size) (hpow : self.align.val.val.isPowerOfTwo) @@ -96,6 +98,7 @@ theorem pad_to_align_sized_headroom (self : layout.DstLayout) (size : Usize) obtain ⟨r, hr, _⟩ := WP.spec_imp_exists hp exact ⟨r, hr⟩ +-- Padding preserves the complete inner size, including its own padding. theorem pad_to_align_size (self : layout.DstLayout) (ha : self.align.val.val.isPowerOfTwo) (hc : canonicalLayout self) @@ -120,6 +123,7 @@ theorem pad_to_align_size (self : layout.DstLayout) · rename_i h exact power_dvd_of_le _ _ ha hinner (by omega) +-- The independent recursive rule determines checked sizes for every metadata. theorem size_matches_recursive (tail : layout.TrailingSliceLayout Usize) (description : LayoutMath.Description) (n : Usize) (hn : 0 < tail.size_rounding_align_and_phase._0.val.val) @@ -132,6 +136,7 @@ theorem size_matches_recursive (tail : layout.TrailingSliceLayout Usize) rw [hr, LayoutMath.Formula.checkedSize, LayoutMath.compile_size description hd] at hsize exact hsize +-- Within the machine size bound, wrapping padding is ordinary physical padding. theorem padding_matches_recursive (tail : layout.TrailingSliceLayout Usize) (description : LayoutMath.Description) (n : Usize) (hn : 0 < tail.size_rounding_align_and_phase._0.val.val) @@ -166,6 +171,7 @@ theorem padding_matches_recursive (tail : layout.TrailingSliceLayout Usize) dsimp only [remaining, physical] at hcancel omega +/-- A zero element stride intentionally panics before inspecting the address. -/ theorem validate_zero_stride (self : layout.DstLayout) (tail : layout.TrailingSliceLayout Usize) (hs : self.size_info = .SliceDst tail) (he : tail.elem_size = 0#usize) (addr length : Usize) (side : layout.CastType) : @@ -177,4 +183,55 @@ theorem validate_zero_stride (self : layout.DstLayout) (tail : layout.TrailingSl rw [hconverted, hv] simp only [bind_ok] +-- The constructor agrees with direct per-metadata field placement for any +-- number of fields. The direct rule retains each field's complete inner size. +theorem constructor_matches_record (repr_align packed : Option NonZeroUsize) + (fields : Slice layout.DstLayout) + (ha : ∀ a ∈ repr_align, alignmentDomain a.val.val) + (hp : ∀ a ∈ packed, alignmentDomain a.val.val) + (hd : constructionDomain fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed) + (hlast : alignmentDomain + (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed fields.val.length).align) + (hfit : (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) + packed fields.val.length).padFits Usize.max) : + layout.DstLayout.for_repr_c_struct repr_align packed fields + ⦃ r => ∀ n : Nat, + let direct := LayoutMath.recordState (fields.val.map layoutValue) + (initialAlignment repr_align) (packingValue packed) n fields.val.length + (layoutValue r).size n = LayoutMath.roundUp direct.2 direct.1 ⦄ := by + obtain ⟨start, hstart, halign, hsize, hunpadded⟩ := + WP.spec_imp_exists (Proofs.Raw.new_zst_spec repr_align (fun a h => (ha a h).1)) + have hv : layoutValue start = constructionPrefix fields + (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed (0#usize).val := by + simp only [constructionPrefix, LayoutMath.LayoutValue.prefixValue, show (0#usize).val = 0 by simp, + List.take_zero, List.foldl_nil, layoutValue, hsize, hunpadded, halign, + initialAlignment, LayoutMath.LayoutValue.initial] + cases repr_align <;> rfl + have hc : canonicalLayout start := by simp only [canonicalLayout, hsize] + obtain ⟨complete, hloop, hv, hc⟩ := WP.spec_imp_exists + (Proofs.Raw.constructor_loop_spec packed fields _ start 0#usize hp hd (by simp) hv hc) + have hca : complete.align.val.val = + (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed fields.val.length).align := + congrArg LayoutMath.LayoutValue.align hv + obtain ⟨r, hpad, hnumeric⟩ := WP.spec_imp_exists (pad_to_align_size complete + (by rw [hca]; exact hlast.1) hc (by rw [hv]; exact hfit)) + unfold layout.DstLayout.for_repr_c_struct + rw [hstart, bind_ok, hloop, bind_ok, hpad] + apply WP.spec.ret + intro n + dsimp only + rw [hnumeric n, hca, hv] + have hdomain : ∀ i (hi : i < (fields.val.map layoutValue).length), + (LayoutMath.LayoutValue.prefixValue (fields.val.map layoutValue) + (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) (packingValue packed) i).extendFits + (fields.val.map layoutValue)[i] (packingValue packed) Usize.max := by + intro i hi + have hil : i < fields.val.length := by simpa only [List.length_map] using hi + simpa only [constructionPrefix, List.getElem_map] using (hd i hil).2.2.2 + have hstate := LayoutMath.recordState_refinement (fields.val.map layoutValue) + (initialAlignment repr_align) (packingValue packed) n Usize.max hdomain + fields.val.length (by simp only [List.length_map, le_refl]) + rw [hstate] + rfl + end Zerocopy.Corollaries diff --git a/verification/aeneas/lean/LayoutMath.lean b/verification/aeneas/lean/LayoutMath.lean index 88714149da..3125c8f913 100644 --- a/verification/aeneas/lean/LayoutMath.lean +++ b/verification/aeneas/lean/LayoutMath.lean @@ -645,6 +645,33 @@ def LayoutValue.padFits (v : LayoutValue) (limit : Nat) : Prop := if f.align < v.align then roundUp f.base f.align + f.phase ≤ limit else roundUp f.base v.align ≤ limit +/- A completed zero-metadata size bound supplies every stored-field bound +needed by padding. This is stronger than guessing conservative headroom: it +uses the same exact fit domain as the independent recursive sizing rule. +-/ +theorem LayoutValue.padFits_of_zero_size (v : LayoutValue) (f : Formula) (limit : Nat) + (hv : v.payload = .trailing f) (ha : 0 < f.align) (ho : 0 < v.align) + (hd : if f.align < v.align then f.align ∣ v.align else v.align ∣ f.align) + (hfit : roundUp (v.size 0) v.align ≤ limit) : v.padFits limit := by + simp only [LayoutValue.size, hv] at hfit + simp only [LayoutValue.padFits, hv] + split + · rename_i hlarge + let fixed := roundUp f.base f.align + f.phase + have hsize : (f.pad v.align).size 0 = roundUp fixed v.align := by + simp only [Formula.pad, hlarge, if_true, Formula.size, Formula.bytes, + Nat.zero_mul, Nat.add_zero] + simpa only [fixed, Nat.add_zero] using normalize_phase fixed 0 v.align + have hpad := pad_size f 0 v.align ha ho hd + rw [hsize] at hpad + have hfixed := (roundUp_properties fixed v.align ho).1 + change fixed ≤ limit + omega + · have hbase : f.base ≤ f.size 0 := by + simp only [Formula.size, Formula.bytes, roundUp] + omega + exact le_trans (roundUp_mono ho hbase) hfit + theorem LayoutValue.extend_size (v field : LayoutValue) (packing bytes n : Nat) (h : v.payload = .fixed bytes) : (v.extend field packing).size n = diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean index bfb79671e5..59eac81d30 100644 --- a/verification/aeneas/lean/LayoutModel.lean +++ b/verification/aeneas/lean/LayoutModel.lean @@ -166,6 +166,26 @@ is an explicit operation domain, not a consequence of NonZeroUsize alone. -/ def alignmentDomain (a : Nat) : Prop := a.isPowerOfTwo ∧ a ≤ 2 ^ 29 +/- Compute the independent prefix state for a constructor loop iteration. +-/ +def constructionPrefix (fields : Slice layout.DstLayout) (initial : LayoutMath.LayoutValue) + (packed : Option NonZeroUsize) (i : Nat) : LayoutMath.LayoutValue := + LayoutMath.LayoutValue.prefixValue (fields.val.map layoutValue) initial (packingValue packed) i + +/- Require every intermediate append to fit before promising that the entire +record constructor terminates. Its final padding bound is stated separately. +-/ +def constructionDomain (fields : Slice layout.DstLayout) (initial : LayoutMath.LayoutValue) + (packed : Option NonZeroUsize) : Prop := + ∀ i (hi : i < fields.val.length), + alignmentDomain (constructionPrefix fields initial packed i).align ∧ + alignmentDomain fields.val[i].align.val.val ∧ canonicalLayout fields.val[i] ∧ + (constructionPrefix fields initial packed i).extendFits + (layoutValue fields.val[i]) (packingValue packed) Usize.max + +def initialAlignment (repr_align : Option NonZeroUsize) : Nat := + (repr_align.map (fun a => a.val.val)).getD 1 + attribute [contract_simps] castSide castSplit castSpec metadataSpec end Zerocopy.Proofs @@ -216,6 +236,16 @@ def layoutValue (self : layout.DstLayout.Fields) : LayoutMath.LayoutValue := | .SliceDst tail => .trailing (trailingFormula tail), unpadded := self.statically_shallow_unpadded } +/- Compute a constructor prefix from decoded mathematical field records. +-/ +def constructionPrefix (fields : List layout.DstLayout.Fields) + (initial : LayoutMath.LayoutValue) (packed : Option NonZeroUsizeValue) + (i : Nat) : LayoutMath.LayoutValue := + LayoutMath.LayoutValue.prefixValue (fields.map layoutValue) initial (packingValue packed) i + +def initialAlignment (repr_align : Option NonZeroUsizeValue) : Nat := + (repr_align.map (fun a => a.value)).getD 1 + end Zerocopy.ModelViews namespace Zerocopy.Proofs.NestedReference diff --git a/verification/aeneas/lean/LayoutModelDomainTests.lean b/verification/aeneas/lean/LayoutModelDomainTests.lean new file mode 100644 index 0000000000..587f7d5a69 --- /dev/null +++ b/verification/aeneas/lean/LayoutModelDomainTests.lean @@ -0,0 +1,183 @@ +/- 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 Mathlib.Tactic.NormNum +@[expose] public section + +/-! +A constructor's preconditions must admit the inputs for which it promises +behavior. These concrete examples test the independently stated construction +domain, including ordinary fields, nested packed layouts, invalid alignments, +and overflow. Checking the domain separately prevents an accidentally empty +precondition from making a constructor theorem appear useful. +-/ +open Aeneas Aeneas.Std Zerocopy Zerocopy.Proofs + +namespace Zerocopy.LayoutModelDomainTests + +private theorem two_fields_fit : 2 ≤ Usize.max := by + rcases System.Platform.numBits_eq with h | h <;> + simp only [Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq, h] <;> decide + +private theorem one_alignment : alignmentDomain 1 := ⟨Nat.isPowerOfTwo_one, by decide⟩ +private theorem two_alignment : alignmentDomain 2 := ⟨by simpa using Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo Nat.isPowerOfTwo_one, by decide⟩ +private theorem four_alignment : alignmentDomain 4 := ⟨by simpa using Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo two_alignment.1, by decide⟩ + +def byteField : layout.DstLayout := + { align := ⟨1#usize⟩, size_info := .Sized 1#usize, + statically_shallow_unpadded := true } + +def wordField : layout.DstLayout := + { align := ⟨4#usize⟩, size_info := .Sized 4#usize, + statically_shallow_unpadded := true } + +def ordinaryFields : Slice layout.DstLayout := + Slice.from [byteField, wordField] (by simpa only [List.length_cons, List.length_nil] using two_fields_fit) + +-- The inner aligned DST has physical offset5 but normalized base4/phase1. +def innerAlignedTail : layout.TrailingSliceLayout Usize := + { offset := 5#usize, elem_size := 1#usize, size_base := 4#usize, + size_rounding_align_and_phase := ⟨⟨5#usize⟩⟩ } + +def innerAlignedField : layout.DstLayout := + { align := ⟨4#usize⟩, size_info := .SliceDst innerAlignedTail, + statically_shallow_unpadded := true } + +def twoBytePrefix : layout.DstLayout := + { align := ⟨1#usize⟩, size_info := .Sized 2#usize, + statically_shallow_unpadded := true } + +def packedFields : Slice layout.DstLayout := + Slice.from [twoBytePrefix, innerAlignedField] + (by simpa only [List.length_cons, List.length_nil] using two_fields_fit) + +def packedTwo : Option NonZeroUsize := some ⟨2#usize⟩ + +def nestedDescription : LayoutMath.Description := + .record 2 0 (some 1) (.record 5 2 none (.slice 1 0)) + +-- These explicitly positive examples make False-strengthened domains fail. +theorem ordinary_record_admitted : + constructionDomain ordinaryFields (LayoutMath.LayoutValue.initial 1) none ∧ + alignmentDomain (constructionPrefix ordinaryFields (LayoutMath.LayoutValue.initial 1) none 2).align ∧ + (constructionPrefix ordinaryFields (LayoutMath.LayoutValue.initial 1) none 2).padFits Usize.max := by + constructor + · intro i hi + have hicases : i = 0 ∨ i = 1 := by + simp only [ordinaryFields, Slice.from_val, List.length_cons, List.length_nil] at hi + omega + rcases hicases with rfl | rfl + all_goals + rcases System.Platform.numBits_eq with h | h <;> + norm_num [constructionPrefix, ordinaryFields, Slice.from_val, + LayoutMath.LayoutValue.prefixValue, LayoutMath.LayoutValue.initial, + LayoutMath.LayoutValue.extend, LayoutMath.LayoutValue.extendFits, + LayoutMath.roundUp, layoutValue, byteField, wordField, canonicalLayout, + packingValue, one_alignment, four_alignment, h, + Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq] + · constructor + · rcases System.Platform.numBits_eq with h | h <;> + norm_num [constructionPrefix, ordinaryFields, Slice.from_val, + LayoutMath.LayoutValue.prefixValue, LayoutMath.LayoutValue.initial, + LayoutMath.LayoutValue.extend, LayoutMath.roundUp, layoutValue, + byteField, wordField, packingValue, four_alignment, h] + · rcases System.Platform.numBits_eq with h | h <;> + norm_num [constructionPrefix, ordinaryFields, Slice.from_val, + LayoutMath.LayoutValue.prefixValue, LayoutMath.LayoutValue.initial, + LayoutMath.LayoutValue.extend, LayoutMath.LayoutValue.padFits, + LayoutMath.roundUp, layoutValue, byteField, wordField, packingValue, + Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq, h] + +theorem nested_packed_record_admitted : + (∀ a ∈ packedTwo, alignmentDomain a.val.val) ∧ + constructionDomain packedFields (LayoutMath.LayoutValue.initial 1) packedTwo ∧ + alignmentDomain (constructionPrefix packedFields (LayoutMath.LayoutValue.initial 1) packedTwo 2).align ∧ + (constructionPrefix packedFields (LayoutMath.LayoutValue.initial 1) packedTwo 2).padFits Usize.max := by + refine ⟨?_, ?_, ?_, ?_⟩ + · simp [packedTwo, two_alignment] + · intro i hi + have hicases : i = 0 ∨ i = 1 := by + simp only [packedFields, Slice.from_val, List.length_cons, List.length_nil] at hi + omega + rcases hicases with rfl | rfl + all_goals + rcases System.Platform.numBits_eq with h | h <;> + norm_num [constructionPrefix, packedFields, Slice.from_val, + LayoutMath.LayoutValue.prefixValue, LayoutMath.LayoutValue.initial, + LayoutMath.LayoutValue.extend, LayoutMath.LayoutValue.extendFits, + LayoutMath.roundUp, layoutValue, twoBytePrefix, innerAlignedField, + innerAlignedTail, trailingFormula, byteFormula, canonicalLayout, + packedTwo, packingValue, one_alignment, four_alignment, h, + Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq, + show Nat.log2 5 = 2 by decide] + · norm_num [constructionPrefix, packedFields, Slice.from_val, + LayoutMath.LayoutValue.prefixValue, LayoutMath.LayoutValue.initial, + LayoutMath.LayoutValue.extend, LayoutMath.roundUp, layoutValue, + twoBytePrefix, innerAlignedField, innerAlignedTail, packedTwo, packingValue, + trailingFormula, byteFormula, two_alignment, show Nat.log2 5 = 2 by decide] + · rcases System.Platform.numBits_eq with h | h <;> + norm_num [constructionPrefix, packedFields, Slice.from_val, + LayoutMath.LayoutValue.prefixValue, LayoutMath.LayoutValue.initial, + LayoutMath.LayoutValue.extend, LayoutMath.LayoutValue.padFits, + LayoutMath.roundUp, layoutValue, twoBytePrefix, innerAlignedField, + innerAlignedTail, packedTwo, packingValue, trailingFormula, byteFormula, + Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq, h, + show Nat.log2 5 = 2 by decide] + +-- Exact values distinguish this view from a constant or flattened interpretation. +theorem input_views_are_exact : + layoutValue byteField = ⟨1, .fixed 1, true⟩ ∧ + layoutValue wordField = ⟨4, .fixed 4, true⟩ ∧ + layoutValue innerAlignedField = ⟨4, .trailing ⟨4, 1, 4, 1, 5⟩, true⟩ := by + norm_num [layoutValue, byteField, wordField, innerAlignedField, innerAlignedTail, + trailingFormula, byteFormula, show Nat.log2 5 = 2 by decide] + +theorem ordinary_prefix_is_exact : + (constructionPrefix ordinaryFields (LayoutMath.LayoutValue.initial 1) none 2).pad = + ⟨4, .fixed 8, false⟩ := by + rcases System.Platform.numBits_eq with h | h <;> + norm_num [constructionPrefix, ordinaryFields, Slice.from_val, + LayoutMath.LayoutValue.prefixValue, LayoutMath.LayoutValue.initial, + LayoutMath.LayoutValue.extend, LayoutMath.LayoutValue.pad, LayoutMath.roundUp, + layoutValue, byteField, wordField, packingValue, h] + +theorem nested_description_is_valid : nestedDescription.valid := by + simp [nestedDescription, LayoutMath.Description.valid] + +theorem nested_packed_prefix_is_exact : + (constructionPrefix packedFields (LayoutMath.LayoutValue.initial 1) packedTwo 2).pad = + ⟨2, .trailing ⟨6, 1, 4, 1, 7⟩, true⟩ := by + norm_num [constructionPrefix, packedFields, Slice.from_val, + LayoutMath.LayoutValue.prefixValue, LayoutMath.LayoutValue.initial, + LayoutMath.LayoutValue.extend, LayoutMath.LayoutValue.pad, + LayoutMath.Formula.pad, LayoutMath.roundUp, layoutValue, twoBytePrefix, + innerAlignedField, innerAlignedTail, packedTwo, packingValue, trailingFormula, + byteFormula, show Nat.log2 5 = 2 by decide] + +theorem nested_packed_zero_retains_inner_padding : + (constructionPrefix packedFields (LayoutMath.LayoutValue.initial 1) packedTwo 2).pad.size 0 = 10 ∧ + nestedDescription.size 0 = 10 ∧ LayoutMath.roundUp 7 2 = 8 := by + rw [nested_packed_prefix_is_exact] + norm_num [LayoutMath.LayoutValue.size, LayoutMath.Formula.size, + LayoutMath.Formula.bytes, LayoutMath.roundUp, nestedDescription, + LayoutMath.Description.size, LayoutMath.Description.alignExponent, + LayoutMath.Description.fieldAlignExponent] + +-- Representation domains are checked independently of the mathematical view. +theorem nominal_domains_are_admitted : + layoutValid byteField ∧ layoutValid wordField ∧ layoutValid innerAlignedField := by + norm_num [layoutValid, sizeInfoValid, trailingValid, encodingValid, + scalar_valid_iff, byteField, wordField, innerAlignedField, innerAlignedTail] + +theorem zero_encoding_is_excluded : + ¬ encodingValid ⟨⟨0#usize⟩⟩ := by + norm_num [encodingValid] + +end Zerocopy.LayoutModelDomainTests diff --git a/verification/aeneas/lean/MathViews.lean b/verification/aeneas/lean/MathViews.lean index 5700db3e06..3d02f70bcf 100644 --- a/verification/aeneas/lean/MathViews.lean +++ b/verification/aeneas/lean/MathViews.lean @@ -172,6 +172,24 @@ attribute [contract_simps] option_valid_iff prod_valid_iff result_valid_iff @[contract_simps] theorem slice_admitted_iff {α : Type} [RustModel α] (x : Slice α) : (∃ value, RustModel.decode x = some value) ↔ ∀ v ∈ x.val, isValid v := slice_valid_iff x +-- Normalize projections of the retained nominal providers to their named +-- decoders before admission or decomposition. These equations fix the actual +-- provider; they do not infer a provider from its mathematical carrier. +@[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 encoding_decoder_admitted_iff (raw : layout.RoundingAlignAndPhase) : @@ -216,21 +234,4 @@ 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 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. end Zerocopy.Proofs diff --git a/verification/aeneas/lean/ModelProjectionLaws.lean b/verification/aeneas/lean/ModelProjectionLaws.lean index ee370fdc45..57eefcecac 100644 --- a/verification/aeneas/lean/ModelProjectionLaws.lean +++ b/verification/aeneas/lean/ModelProjectionLaws.lean @@ -71,75 +71,6 @@ theorem layoutValue_decode (raw : layout.DstLayout) (value : layout.DstLayout.Fi simp only [ModelViews.layoutValue, layoutValue, hs, hva, trailingFormula_decode tail tailValue ht] -/-- Optional machine sizes retain both absence and the exact numeric payload. -/ -theorem optionalSize_decode (raw : Option Usize) (value : Option (UnsignedWord .Usize)) - (h : RustModel.decode raw = some value) : - value.map (fun size => (size : Nat)) = raw.map UScalar.val := by - cases raw <;> - simp only [RustModel.decode, Option.map_some, - Option.some.injEq] at h <;> - cases h <;> rfl - -/-- Padding's existing view retains every exact field observation required by -its raw contract, including the size variant and the unpadded flag. -/ -theorem layout_pad_iff (self result : layout.DstLayout) : - layoutValue result = (layoutValue self).pad ↔ - result.align = self.align ∧ match self.size_info with - | .Sized bytes => ∃ padded, result.size_info = .Sized padded ∧ - padded.val = LayoutMath.roundUp bytes.val self.align.val.val ∧ - result.statically_shallow_unpadded = - (self.statically_shallow_unpadded && decide (bytes.val % self.align.val.val = 0)) - | .SliceDst tail => ∃ next, result.size_info = .SliceDst next ∧ - trailingFormula next = (trailingFormula tail).pad self.align.val.val ∧ - result.statically_shallow_unpadded = self.statically_shallow_unpadded := by - constructor - · intro h - have ha := congrArg LayoutMath.LayoutValue.align h - have hp := congrArg LayoutMath.LayoutValue.payload h - have hu := congrArg LayoutMath.LayoutValue.unpadded h - have align : result.align = self.align := by - have hv : result.align.val = self.align.val := UScalar.eq_of_val_eq ha - have ext : ∀ a b : NonZeroUsize, a.val = b.val → a = b := by - rintro ⟨a⟩ ⟨b⟩ h - cases h - rfl - exact ext result.align self.align hv - refine ⟨align, ?_⟩ - cases hs : self.size_info <;> cases hr : result.size_info <;> - simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, - LayoutMath.Payload.fixed.injEq, LayoutMath.Payload.trailing.injEq, - reduceCtorEq] at hp hu ⊢ - all_goals exact ⟨_, rfl, hp, hu⟩ - · rintro ⟨ha, h⟩ - cases hs : self.size_info with - | Sized bytes => - simp only [hs] at h - rcases h with ⟨padded, hr, hp, hu⟩ - simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, ha, hp, hu] - | SliceDst tail => - simp only [hs] at h - rcases h with ⟨next, hr, hp, hu⟩ - simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, ha, hp, hu] - -/-- Exact physical offset and stride remain observable through the padding view; -equality of bounded words follows from equality of their numeric projections. -/ -theorem layout_pad_trailing_fields (self result : layout.DstLayout) - (tail : layout.TrailingSliceLayout Usize) - (hs : self.size_info = .SliceDst tail) - (h : layoutValue result = (layoutValue self).pad) : - ∃ next, result.size_info = .SliceDst next ∧ - next.offset = tail.offset ∧ next.elem_size = tail.elem_size := by - have facts := (layout_pad_iff self result).mp h - simp only [hs] at facts - obtain ⟨next, hn, hf, _⟩ := facts.2 - refine ⟨next, hn, UScalar.eq_of_val_eq ?_, UScalar.eq_of_val_eq ?_⟩ - · have ho := congrArg LayoutMath.Formula.offset hf - dsimp only [LayoutMath.Formula.pad] at ho - split at ho <;> exact ho - · have he := congrArg LayoutMath.Formula.elem hf - dsimp only [LayoutMath.Formula.pad] at he - split at he <;> exact he - theorem packingValue_decode (raw : Option NonZeroUsize) (value : Option NonZeroUsizeValue) (h : RustModel.decode raw = some value) : @@ -164,6 +95,15 @@ theorem packing_alignment_decode (raw : Option NonZeroUsize) have ha := (decodeNonZeroUScalar_iff align decoded).mp hd simp only [Option.mem_some_iff, forall_eq', ha] +/-- Optional machine sizes retain both absence and the exact numeric payload. -/ +theorem optionalSize_decode (raw : Option Usize) (value : Option (UnsignedWord .Usize)) + (h : RustModel.decode raw = some value) : + value.map (fun size => (size : Nat)) = raw.map UScalar.val := by + cases raw <;> + simp only [RustModel.decode, Option.map_some, + Option.some.injEq] at h <;> + cases h <;> rfl + /-- Positive rounding encodings are recovered from both observed components. -/ theorem rounding_eq_of_components (left right : layout.RoundingAlignAndPhase) (hl : 0 < left._0.val.val) (hr : 0 < right._0.val.val) @@ -247,4 +187,64 @@ theorem layout_extend_iff (self field result : layout.DstLayout) placement, fieldAlignment, trailingFormula, byteFormula, ha, hu, ho, hb, he, hc] rfl +/-- Padding's existing view retains every exact field observation required by +its raw contract, including the size variant and the unpadded flag. -/ +theorem layout_pad_iff (self result : layout.DstLayout) : + layoutValue result = (layoutValue self).pad ↔ + result.align = self.align ∧ match self.size_info with + | .Sized bytes => ∃ padded, result.size_info = .Sized padded ∧ + padded.val = LayoutMath.roundUp bytes.val self.align.val.val ∧ + result.statically_shallow_unpadded = + (self.statically_shallow_unpadded && decide (bytes.val % self.align.val.val = 0)) + | .SliceDst tail => ∃ next, result.size_info = .SliceDst next ∧ + trailingFormula next = (trailingFormula tail).pad self.align.val.val ∧ + result.statically_shallow_unpadded = self.statically_shallow_unpadded := by + constructor + · intro h + have ha := congrArg LayoutMath.LayoutValue.align h + have hp := congrArg LayoutMath.LayoutValue.payload h + have hu := congrArg LayoutMath.LayoutValue.unpadded h + have align : result.align = self.align := by + have hv : result.align.val = self.align.val := UScalar.eq_of_val_eq ha + have ext : ∀ a b : NonZeroUsize, a.val = b.val → a = b := by + rintro ⟨a⟩ ⟨b⟩ h + cases h + rfl + exact ext result.align self.align hv + refine ⟨align, ?_⟩ + cases hs : self.size_info <;> cases hr : result.size_info <;> + simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, + LayoutMath.Payload.fixed.injEq, LayoutMath.Payload.trailing.injEq, + reduceCtorEq] at hp hu ⊢ + all_goals exact ⟨_, rfl, hp, hu⟩ + · rintro ⟨ha, h⟩ + cases hs : self.size_info with + | Sized bytes => + simp only [hs] at h + rcases h with ⟨padded, hr, hp, hu⟩ + simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, ha, hp, hu] + | SliceDst tail => + simp only [hs] at h + rcases h with ⟨next, hr, hp, hu⟩ + simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, ha, hp, hu] + +/-- Exact physical offset and stride remain observable through the padding view; +equality of bounded words follows from equality of their numeric projections. -/ +theorem layout_pad_trailing_fields (self result : layout.DstLayout) + (tail : layout.TrailingSliceLayout Usize) + (hs : self.size_info = .SliceDst tail) + (h : layoutValue result = (layoutValue self).pad) : + ∃ next, result.size_info = .SliceDst next ∧ + next.offset = tail.offset ∧ next.elem_size = tail.elem_size := by + have facts := (layout_pad_iff self result).mp h + simp only [hs] at facts + obtain ⟨next, hn, hf, _⟩ := facts.2 + refine ⟨next, hn, UScalar.eq_of_val_eq ?_, UScalar.eq_of_val_eq ?_⟩ + · have ho := congrArg LayoutMath.Formula.offset hf + dsimp only [LayoutMath.Formula.pad] at ho + split at ho <;> exact ho + · have he := congrArg LayoutMath.Formula.elem hf + dsimp only [LayoutMath.Formula.pad] at he + split at he <;> exact he + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index 912743afb0..c5b99a38e8 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -49,9 +49,23 @@ def nested_reference_size_spec : Prop := nested_reference_size_spec_contract leading elem_size leaf_align elems (layout.nested_reference.size_for_metadata leading elem_size leaf_align elems) +-- An arbitrary successful unit outcome characterizes total assertion safety. +-- Panic and divergence cannot satisfy this independent expectation. +def nested_reference_matches_spec_contract + (_leading : Slice layout.nested_reference.NestedLayer) (_elem_size _leaf_align _elems : Usize) + (run : Result Unit) : Prop := + ∃ output, run = .ok output + +def nested_reference_matches_spec : Prop := + ∀ leading elem_size leaf_align elems, + nested_reference_matches_spec_contract leading elem_size leaf_align elems + (layout.nested_reference.assert_matches_dst_layout leading elem_size leaf_align elems) abbrev NonZeroUsize := core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner +-- Written independently of the specification expansions, using mathematical +-- values. Each family describes an arbitrary outcome; its transparent alias +-- applies the family to the extracted operation. def max_spec_contract (a b : NonZeroUsize) (run : Result NonZeroUsize) : Prop := 0 < a.val.val → 0 < b.val.val → ∃ r, run = .ok r ∧ 0 < r.val.val ∧ @@ -97,6 +111,8 @@ def round_down_spec : Prop := ∀ (n : Usize) (align : NonZeroUsize), round_down_spec_contract n align (util.round_down_to_next_multiple_of_alignment n align) +-- These propositions are maintained separately from the specification macro and +-- native proof modules. They fix successful termination and mathematical results. def encoding_new_spec_contract (a : NonZeroUsize) (p : Usize) (run : Result layout.RoundingAlignAndPhase) : Prop := 0 < a.val.val → a.val.val.isPowerOfTwo → p.val < a.val.val → @@ -403,6 +419,24 @@ def metadata_exact_spec : Prop := ∀ (self : layout.DstLayout) (size : Usize), metadata_exact_spec_contract self size (layout.DstLayout.metadata_for_exact_size self size) +def for_repr_c_struct_spec_contract + (a packed : Option NonZeroUsize) (fields : Slice layout.DstLayout) + (run : Result layout.DstLayout) : Prop := + (∀ x ∈ a, 0 < x.val.val) → (∀ x ∈ packed, 0 < x.val.val) → + (∀ field ∈ fields.val, layoutValid field) → + (∀ x ∈ a, alignmentDomain x.val.val) → (∀ x ∈ packed, alignmentDomain x.val.val) → + constructionDomain fields (LayoutMath.LayoutValue.initial (initialAlignment a)) packed → + alignmentDomain (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment a)) + packed fields.val.length).align → + (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment a)) + packed fields.val.length).padFits Usize.max → + ∃ r, run = .ok r ∧ layoutValid r ∧ layoutValue r = + (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment a)) packed fields.val.length).pad + +def for_repr_c_struct_spec : Prop := + ∀ (a packed : Option NonZeroUsize) (fields : Slice layout.DstLayout), + for_repr_c_struct_spec_contract a packed fields + (layout.DstLayout.for_repr_c_struct a packed fields) end Zerocopy.Obligations @@ -419,10 +453,6 @@ def arithmetic_checks_spec : Prop := ∀ (len : Usize) (align : NonZeroUsize), 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 ⦄ diff --git a/verification/aeneas/lean/Obligations/CompositionChecks.lean b/verification/aeneas/lean/Obligations/CompositionChecks.lean index 758492ba82..8c59ff67bd 100644 --- a/verification/aeneas/lean/Obligations/CompositionChecks.lean +++ b/verification/aeneas/lean/Obligations/CompositionChecks.lean @@ -39,4 +39,15 @@ def composition_pad_checks_spec : Prop := ∀ runtime_layout reference, composition_pad_checks_spec_contract runtime_layout reference (layout.composition_checks.check_pad runtime_layout reference) +def composition_constructor_checks_spec_contract (repr_align packed : Option NonZeroUsize) + (fields : Slice layout.DstLayout) (_references : Slice CompositionReferenceLayout) + (run : Result Unit) : Prop := + (∀ a ∈ repr_align, 0 < a.val.val) → (∀ a ∈ packed, 0 < a.val.val) → + (∀ field ∈ fields.val, layoutValid field) → run ⦃ _ => True ⦄ + +def composition_constructor_checks_spec : Prop := + ∀ repr_align packed fields references, + composition_constructor_checks_spec_contract repr_align packed fields references + (layout.composition_checks.check_constructor repr_align packed fields references) + end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean index a15e1bdd5e..9ea2143f55 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -44,8 +44,8 @@ independent recursive layout semantics under the explicit Rust premise. open Aeneas Aeneas.Std namespace Zerocopy.Proofs.Raw +-- Raw contract requirements intentionally retain their descriptive proof names. set_option linter.unusedVariables false - /- Read the pinned platform's pointer width through its modeled primitive. This establishes the runtime constant used by encoding and packing arithmetic. -/ @@ -114,6 +114,7 @@ theorem highest_bit_xor (k p : Nat) (hp : p < 2 ^ k) : (2 ^ k + p) ^^^ 2 ^ k = p · rw [Nat.testBit_two_pow_of_ne (Ne.symm hi)] simp + /- Prove the implementation's bit scan recovers the alignment and phase of every positive stored word, not only words built by the constructor. -/ @@ -934,7 +935,6 @@ theorem packing_limit_spec (packed : Option NonZeroUsize) -- Aeneas shares a generated matcher with the alignment encoder. The model -- comparison checks that matcher; this proof deliberately names it. set_option linter.auxLemma false in - /- Append a field at its effective packed alignment, retaining the field's complete inner layout. The canonical theorem then proves the concise mathematical extension equation and successful decoding of the returned @@ -1487,6 +1487,92 @@ theorem pad_value_spec (self : layout.DstLayout) attribute [step] pad_value_spec +theorem construction_prefix_step (fields : Slice layout.DstLayout) (initial : LayoutMath.LayoutValue) + (packed : Option NonZeroUsize) (i : Nat) (hi : i < fields.val.length) : + constructionPrefix fields initial packed (i + 1) = + (constructionPrefix fields initial packed i).extend (layoutValue fields.val[i]) (packingValue packed) := by + unfold constructionPrefix + rw [LayoutMath.LayoutValue.prefixValue_step _ _ _ _ (by simpa only [List.length_map] using hi)] + simp only [List.getElem_map] + +/- Relate each extracted loop state to the independently computed field prefix. +The shared indexed-loop adapter proves termination from the remaining field +count; each body step preserves the representation facts needed for the next. +-/ +theorem constructor_loop_spec (packed : Option NonZeroUsize) (fields : Slice layout.DstLayout) + (initial : LayoutMath.LayoutValue) (self : layout.DstLayout) (i : Usize) + (hp : ∀ a ∈ packed, alignmentDomain a.val.val) + (hd : constructionDomain fields initial packed) + (hi : i.val ≤ fields.val.length) + (hv : layoutValue self = constructionPrefix fields initial packed i.val) + (hc : canonicalLayout self) : + layout.DstLayout.for_repr_c_struct_loop packed fields self i + ⦃ r => layoutValue r = constructionPrefix fields initial packed fields.val.length ∧ canonicalLayout r ⦄ := by + unfold layout.DstLayout.for_repr_c_struct_loop + apply AeneasContracts.indexed_loop_spec fields.val.length layoutValue + (constructionPrefix fields initial packed) canonicalLayout + · intro value idx hi hv hc + unfold layout.DstLayout.for_repr_c_struct_loop.body + simp only [UScalar.lt_equiv, Slice.len_val, Slice.length] + split + · rename_i hlt + have hlt' : idx.val < fields.val.length := hlt + step with Slice.index_usize_spec fields idx hlt' as ⟨field, hf⟩ + obtain ⟨hself, hfield, hcanon, hfits⟩ := hd idx.val hlt' + have hsa : alignmentDomain value.align.val.val := by + have hh := congrArg LayoutMath.LayoutValue.align hv + change value.align.val.val = _ at hh + rw [hh] + exact hself + have hfa : alignmentDomain field.align.val.val := by rw [hf]; exact hfield + have hca : canonicalLayout field := by rw [hf]; exact hcanon + have hfit : (layoutValue value).extendFits (layoutValue field) (packingValue packed) Usize.max := by + rw [hv, hf] + exact hfits + step as ⟨next, hnext, hcn⟩ + have hroom : idx.val + (1#usize).val ≤ Usize.max := by + have := fields.property + change idx.val + 1 ≤ Usize.max + omega + step with Usize.add_spec (x := idx) (y := 1#usize) hroom as ⟨j, hj⟩ + change j.val = idx.val + 1 at hj + refine ⟨hlt', hj, ?_, hcn⟩ + rw [hj, construction_prefix_step fields initial packed idx.val hlt', hnext, hv, hf] + · rename_i hdone + have heq : idx.val = fields.val.length := by omega + exact WP.spec.ret ⟨heq, hv, hc⟩ + · exact hi + · exact hv + · exact hc + +/- Stitch together initialization, every field append, and final padding. The +requirements cover arbitrary field lists in the independent construction +domain, rather than assuming that the constructor already returned correctly. +-/ +theorem for_repr_c_struct_spec : + ∀ (repr_align repr_packed : Option NonZeroUsize) (fields : Slice layout.DstLayout), ∀ (ha : (∀ a ∈ repr_align, alignmentDomain a.val.val : Prop)), ∀ (hp : (∀ a ∈ repr_packed, alignmentDomain a.val.val : Prop)), ∀ (hd : (constructionDomain fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) repr_packed : Prop)), ∀ (hlast : (alignmentDomain + (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) repr_packed fields.val.length).align : Prop)), ∀ (hfit : ((constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) + repr_packed fields.val.length).padFits Usize.max : Prop)), + @Zerocopy.layout.DstLayout.for_repr_c_struct repr_align repr_packed fields ⦃ r => layoutValue r = + (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) repr_packed fields.val.length).pad ∧ canonicalLayout r ⦄ := by + intro repr_align packed fields ha hp hd hlast hfit + unfold layout.DstLayout.for_repr_c_struct + step with new_zst_spec repr_align (fun a h => (ha a h).1) as ⟨start, halign, hsize, hunpadded⟩ + have hv : layoutValue start = constructionPrefix fields + (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed (0#usize).val := by + simp only [constructionPrefix, LayoutMath.LayoutValue.prefixValue, show (0#usize).val = 0 by simp, + List.take_zero, List.foldl_nil, layoutValue, hsize, hunpadded, halign, + initialAlignment, LayoutMath.LayoutValue.initial] + cases repr_align <;> rfl + have hc : canonicalLayout start := by simp only [canonicalLayout, hsize] + step with constructor_loop_spec packed fields _ start 0#usize hp hd (by simp) hv hc as ⟨complete, hv, hc⟩ + step with pad_value_spec complete (by + have hh := congrArg LayoutMath.LayoutValue.align hv + change complete.align.val.val = _ at hh + rw [hh] + exact hlast.1) hc (by rw [hv]; exact hfit) as ⟨result, hr, hcanonical⟩ + exact ⟨by rw [hr, hv], hcanonical⟩ + end Zerocopy.Proofs.Raw namespace Zerocopy.Proofs @@ -1918,6 +2004,27 @@ theorem pad_to_align_spec : Zerocopy.Specs.pad_to_align_spec := by exact (layout_pad_iff self result).mpr facts register_spec_step pad_to_align_spec +/- Stitch together initialization, every field append, and final padding. The +requirements cover arbitrary field lists in the independent construction +domain, rather than assuming that the constructor already returned correctly. +-/ +theorem for_repr_c_struct_spec : Zerocopy.Specs.for_repr_c_struct_spec := by + unfold Zerocopy.Specs.for_repr_c_struct_spec + representation_simps + intro repr_align packed fields _ _ _ ha hp hd hlast hfit + apply WP.spec_mono (Raw.for_repr_c_struct_spec repr_align packed fields ha hp hd hlast hfit) + rintro r ⟨hr, hc⟩ + refine ⟨?_, hr⟩ + refine ⟨?_, ?_⟩ + · have halign := congrArg LayoutMath.LayoutValue.align hr + change r.align.val.val = _ at halign + rw [halign] + exact Nat.pos_of_isPowerOfTwo hlast.1 + · cases hs : r.size_info with + | Sized _ => trivial + | SliceDst _ => simpa only [canonicalLayout, hs] using hc +register_spec_step for_repr_c_struct_spec + /-- An arbitrary proof of the compact mathematical clause implies the separately maintained exact optional-size and overflow obligation. -/ @[contract_simps] theorem size_for_elems_spec_implies_required diff --git a/verification/aeneas/lean/Proofs/CompositionChecks.lean b/verification/aeneas/lean/Proofs/CompositionChecks.lean index c1a3d6a4fa..6bcb34da30 100644 --- a/verification/aeneas/lean/Proofs/CompositionChecks.lean +++ b/verification/aeneas/lean/Proofs/CompositionChecks.lean @@ -7,7 +7,7 @@ This file may not be copied, modified, or distributed except according to those terms. -/ module -public import CompositionReference +public import CompositionConstructor @[expose] public section /-! @@ -83,6 +83,70 @@ theorem composition_extend_checks (preceding field : layout.DstLayout) · simp · simp +theorem composition_constructor_checks (repr_align packed : Option NonZeroUsize) + (fields : Slice layout.DstLayout) (references : Slice ReferenceLayout) : + layout.composition_checks.check_constructor repr_align packed fields references ⦃ _ => True ⦄ := by + unfold layout.composition_checks.check_constructor + simp only [bne_iff_ne, ne_eq, UScalar.eq_equiv, Slice.len_val, Slice.length] + split + · simp + · rename_i equal_length + have lengths : fields.val.length = references.val.length := by omega + have initial_matching : (true = true) = fieldsMatchThrough fields references (0#usize).val := by + apply propext + simp [fieldsMatchThrough] + step with composition_matching_loop_spec fields references lengths true 0#usize + (by simp) initial_matching as ⟨matching, hm⟩ + split + · rename_i yes + have all_matching := Eq.mp hm yes + have matched (j : Nat) (hj : j < fields.val.length) (hr : j < references.val.length) : + Matches fields.val[j] references.val[j] := all_matching j hj hr hj + have fields_valid : ∀ j (hr : j < references.val.length), valid references.val[j] := by + intro j hr + have hj : j < fields.val.length := by omega + exact (matches_value _ _ (matched j hj hr)).1 + have field_views : fields.val.map layoutValue = references.val.map value := by + apply List.ext_getElem + · simpa only [List.length_map] using lengths + · intro j hj hr + have hj' : j < fields.val.length := by simpa only [List.length_map] using hj + have hr' : j < references.val.length := by simpa only [List.length_map] using hr + simpa only [List.getElem_map] using (matches_value _ _ (matched j hj' hr')).2.2 + have prefixes (j : Nat) : constructionPrefix fields + (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed j = + referencePrefix references (initialAlignment repr_align) packed j := by + simp only [constructionPrefix, referencePrefix, field_views] + step with composition_reference_constructor_spec repr_align packed references fields_valid as ⟨expected, he⟩ + cases expected with + | none => simp + | some expected => + obtain ⟨initial_domain, packed_domain, history, final_domain, fits, expected_view, expected_validity⟩ := he expected rfl + have construction : constructionDomain fields + (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) packed := by + intro j hj + have hr : j < references.val.length := by omega + obtain ⟨previous_domain, field_domain, _, field_fit⟩ := history j hr hr + obtain ⟨_, field_canonical, view⟩ := matches_value _ _ (matched j hj hr) + have alignment := congrArg LayoutMath.LayoutValue.align view + change fields.val[j].align.val.val = references.val[j].align.val at alignment + refine ⟨?_, ?_, field_canonical, ?_⟩ + · simpa only [prefixes] using previous_domain + · simpa only [alignment] using field_domain + · simpa only [prefixes, view] using field_fit + step with composition_production_constructor_spec repr_align packed fields initial_domain + (by simpa only [lengths] using packed_domain) construction + (by simpa only [prefixes, lengths] using final_domain) + (by simpa only [prefixes, lengths] using fits) + as ⟨actual, actual_view, actual_canonical⟩ + have same : layoutValue actual = value expected := by + rw [actual_view, prefixes, lengths, expected_view] + have matched_result := matches_of_value actual expected actual_canonical expected_validity same + step with composition_matches_spec actual expected as ⟨checked, hc⟩ + have yes : checked = true := hc.mpr matched_result + simp [yes, massert] + · simp + end Zerocopy.Proofs.Raw namespace Zerocopy.Proofs @@ -101,4 +165,11 @@ theorem composition_extend_checks_spec : Specs.composition_extend_checks_spec := intro _ _ exact ⟨(), rfl, trivial⟩ +theorem composition_constructor_checks_spec : Specs.composition_constructor_checks_spec := by + intro repr_align packed fields references + repeat intro + apply WP.spec_mono (Raw.composition_constructor_checks repr_align packed fields references) + intro _ _ + exact ⟨(), rfl, trivial⟩ + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/NestedConstruction.lean b/verification/aeneas/lean/Proofs/NestedConstruction.lean new file mode 100644 index 0000000000..3f1771f9bc --- /dev/null +++ b/verification/aeneas/lean/Proofs/NestedConstruction.lean @@ -0,0 +1,576 @@ +/- 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 Corollaries +import all Init.Data.Nat.Power2.Basic +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.NestedReference +open LayoutMath + +def prefixValue (bytes : Nat) : LayoutValue := ⟨1, .fixed bytes, true⟩ + +def layerFragment (inner : LayoutValue) (minimum packing bytes : Nat) : LayoutValue := + ((LayoutValue.initial minimum).extend (prefixValue bytes) packing).extend inner packing + +theorem prefixValue_extend (minimum packing bytes : Nat) + (hm : 0 < minimum) (hp : 0 < packing) : + (LayoutValue.initial minimum).extend (prefixValue bytes) packing = + ⟨minimum, .fixed bytes, true⟩ := by + have hmin : min 1 packing = 1 := Nat.min_eq_left (by omega) + have hmax : max minimum 1 = minimum := Nat.max_eq_left (by omega) + simp [LayoutValue.initial, LayoutValue.extend, prefixValue, hmin, hmax, roundUp] + +theorem layerFragment_align (inner : LayoutValue) (minimum packing bytes : Nat) + (hm : 0 < minimum) (hp : 0 < packing) : + (layerFragment inner minimum packing bytes).align = max minimum (min inner.align packing) := by + rw [layerFragment, prefixValue_extend minimum packing bytes hm hp] + rfl + +theorem layerFragment_size (inner : LayoutValue) (minimum packing bytes n : Nat) + (hm : 0 < minimum) (hp : 0 < packing) : + (layerFragment inner minimum packing bytes).size n = + roundUp bytes (min inner.align packing) + inner.size n := by + rw [layerFragment, prefixValue_extend minimum packing bytes hm hp] + exact LayoutValue.extend_size _ _ _ _ _ rfl + +theorem layerFragment_payload (inner : LayoutValue) (f : Formula) + (minimum packing bytes : Nat) (hf : inner.payload = .trailing f) + (hm : 0 < minimum) (hp : 0 < packing) : + (layerFragment inner minimum packing bytes).payload = + .trailing { f with base := roundUp bytes (min inner.align packing) + f.base, offset := roundUp bytes (min inner.align packing) + f.offset } := by + rw [layerFragment, prefixValue_extend minimum packing bytes hm hp] + simp only [LayoutValue.extend, hf] + +theorem layerFragment_bounds (inner : LayoutValue) (f : Formula) + (minimum packing bytes limit : Nat) (hf : inner.payload = .trailing f) + (hm : 0 < minimum) (hp : 0 < packing) (hi : 0 < inner.align) + (ho : f.offset ≤ inner.size 0) + (hfit : roundUp (roundUp bytes (min inner.align packing) + inner.size 0) + (max minimum (min inner.align packing)) ≤ limit) : + bytes ≤ limit ∧ roundUp bytes (min inner.align packing) + f.offset ≤ limit ∧ + roundUp bytes (min inner.align packing) + f.base ≤ limit := by + have hplace := (roundUp_properties bytes (min inner.align packing) (by omega)).1 + have houter := (roundUp_properties + (roundUp bytes (min inner.align packing) + inner.size 0) + (max minimum (min inner.align packing)) (by omega)).1 + have hbase : f.base ≤ inner.size 0 := by + simp only [LayoutValue.size, hf, Formula.size, Formula.bytes, roundUp] + omega + omega + +theorem layerFragment_padFits (inner : LayoutValue) (f : Formula) + (minimum packing bytes limit : Nat) (hf : inner.payload = .trailing f) + (hm : 0 < minimum) (hp : 0 < packing) + (ha : f.align.isPowerOfTwo) + (hout : (max minimum (min inner.align packing)).isPowerOfTwo) + (hfit : roundUp (roundUp bytes (min inner.align packing) + inner.size 0) + (max minimum (min inner.align packing)) ≤ limit) : + (layerFragment inner minimum packing bytes).padFits limit := by + let g : Formula := { f with base := roundUp bytes (min inner.align packing) + f.base, offset := roundUp bytes (min inner.align packing) + f.offset } + have hv := layerFragment_payload inner f minimum packing bytes hf hm hp + change (layerFragment inner minimum packing bytes).payload = .trailing g at hv + apply LayoutValue.padFits_of_zero_size _ g limit hv + · exact Nat.pos_of_isPowerOfTwo ha + · rw [layerFragment_align inner minimum packing bytes hm hp] + exact Nat.pos_of_isPowerOfTwo hout + · rw [layerFragment_align inner minimum packing bytes hm hp] + change if f.align < max minimum (min inner.align packing) then + f.align ∣ max minimum (min inner.align packing) else + max minimum (min inner.align packing) ∣ f.align + split + · exact Raw.power_dvd_of_le _ _ ha hout (by omega) + · exact Raw.power_dvd_of_le _ _ hout ha (by omega) + · rw [layerFragment_size inner minimum packing bytes 0 hm hp, + layerFragment_align inner minimum packing bytes hm hp] + exact hfit + +theorem layerFragment_pad_size (inner : LayoutValue) (f : Formula) + (minimum packing bytes n : Nat) (hf : inner.payload = .trailing f) + (hm : 0 < minimum) (hp : 0 < packing) + (ha : f.align.isPowerOfTwo) + (hout : (max minimum (min inner.align packing)).isPowerOfTwo) : + ((layerFragment inner minimum packing bytes).pad).size n = + roundUp (roundUp bytes (min inner.align packing) + inner.size n) + (max minimum (min inner.align packing)) := by + let g : Formula := { f with base := roundUp bytes (min inner.align packing) + f.base, offset := roundUp bytes (min inner.align packing) + f.offset } + have hv := layerFragment_payload inner f minimum packing bytes hf hm hp + change (layerFragment inner minimum packing bytes).payload = .trailing g at hv + have hd : if g.align < (layerFragment inner minimum packing bytes).align then + g.align ∣ (layerFragment inner minimum packing bytes).align else + (layerFragment inner minimum packing bytes).align ∣ g.align := by + rw [layerFragment_align inner minimum packing bytes hm hp] + change if f.align < max minimum (min inner.align packing) then + f.align ∣ max minimum (min inner.align packing) else + max minimum (min inner.align packing) ∣ f.align + split + · exact Raw.power_dvd_of_le _ _ ha hout (by omega) + · exact Raw.power_dvd_of_le _ _ hout ha (by omega) + have hpad := pad_size g n (layerFragment inner minimum packing bytes).align + (Nat.pos_of_isPowerOfTwo ha) + (by rw [layerFragment_align inner minimum packing bytes hm hp]; + exact Nat.pos_of_isPowerOfTwo hout) hd + have hs : (layerFragment inner minimum packing bytes).size n = g.size n := by + simp only [LayoutValue.size, hv] + rw [← hs, layerFragment_size inner minimum packing bytes n hm hp, + layerFragment_align inner minimum packing bytes hm hp] at hpad + simpa only [LayoutValue.pad, hv, LayoutValue.size, + layerFragment_align inner minimum packing bytes hm hp] using hpad + +end Zerocopy.Proofs.NestedReference + +namespace Zerocopy.Proofs.Raw +open LayoutMath NestedReference + +def nestedPrefix (bytes : Usize) : layout.DstLayout := + { align := ⟨1#usize⟩, size_info := .Sized bytes, statically_shallow_unpadded := true } + +theorem nested_prefix_value (bytes : Usize) : + layoutValue (nestedPrefix bytes) = NestedReference.prefixValue bytes.val := rfl + +/-- One recursive layer has the same exact static fit domain as the direct +reference. Its inner fragment retains the complete inner size for every count. -/ +theorem nested_layer_constructor_spec (minimum packed : NonZeroUsize) (bytes : Usize) + (inner : layout.DstLayout) (tail : layout.TrailingSliceLayout Usize) + (fields : Slice layout.DstLayout) (hfields : fields.val = [nestedPrefix bytes, inner]) + (hm : alignmentDomain minimum.val.val) (hp : alignmentDomain packed.val.val) + (hi : alignmentDomain inner.align.val.val) (hc : canonicalLayout inner) + (hs : inner.size_info = .SliceDst tail) + (ho : tail.offset.val ≤ (layoutValue inner).size 0) + (hfit : roundUp (roundUp bytes.val (min inner.align.val.val packed.val.val) + + (layoutValue inner).size 0) (max minimum.val.val (min inner.align.val.val packed.val.val)) ≤ Usize.max) : + layout.DstLayout.for_repr_c_struct (some minimum) (some packed) fields + ⦃ r => canonicalLayout r ∧ + r.align.val.val = max minimum.val.val (min inner.align.val.val packed.val.val) ∧ + (∀ n : Nat, (layoutValue r).size n = + roundUp (roundUp bytes.val (min inner.align.val.val packed.val.val) + + (layoutValue inner).size n) + (max minimum.val.val (min inner.align.val.val packed.val.val))) ∧ + ∃ out, r.size_info = .SliceDst out ∧ out.offset.val ≤ (layoutValue r).size 0 ⦄ := by + have hmpos := Nat.pos_of_isPowerOfTwo hm.1 + have hppos := Nat.pos_of_isPowerOfTwo hp.1 + have hipos := Nat.pos_of_isPowerOfTwo hi.1 + have hplacePow : (min inner.align.val.val packed.val.val).isPowerOfTwo := by + by_cases h : inner.align.val.val ≤ packed.val.val + · simpa only [Nat.min_eq_left h] using hi.1 + · simpa only [Nat.min_eq_right (by omega : packed.val.val ≤ inner.align.val.val)] using hp.1 + have houtPow : (max minimum.val.val (min inner.align.val.val packed.val.val)).isPowerOfTwo := by + by_cases h : minimum.val.val ≤ min inner.align.val.val packed.val.val + · simpa only [Nat.max_eq_right h] using hplacePow + · simpa only [Nat.max_eq_left (by omega : min inner.align.val.val packed.val.val ≤ minimum.val.val)] using hm.1 + have hout : alignmentDomain (max minimum.val.val (min inner.align.val.val packed.val.val)) := + ⟨houtPow, max_le hm.2 (le_trans (Nat.min_le_left _ _) hi.2)⟩ + have hf : (layoutValue inner).payload = .trailing (trailingFormula tail) := by + simp only [layoutValue, hs] + have hformulaPow : (trailingFormula tail).align.isPowerOfTwo := by + exact ⟨_, rfl⟩ + have bounds := layerFragment_bounds (layoutValue inner) (trailingFormula tail) + minimum.val.val packed.val.val bytes.val Usize.max hf hmpos hppos hipos ho hfit + have hprefix : constructionPrefix fields (LayoutValue.initial (initialAlignment (some minimum))) + (some packed) 1 = ⟨minimum.val.val, .fixed bytes.val, true⟩ := by + simp only [constructionPrefix, hfields, List.map_cons, List.map_nil, + LayoutValue.prefixValue, List.take_succ_cons, List.take_zero, List.foldl_cons, + List.foldl_nil, nested_prefix_value, initialAlignment, packingValue, + Option.map_some, Option.getD_some] + exact prefixValue_extend _ _ _ hmpos hppos + have hcomplete : constructionPrefix fields (LayoutValue.initial (initialAlignment (some minimum))) + (some packed) fields.val.length = + layerFragment (layoutValue inner) minimum.val.val packed.val.val bytes.val := by + simp only [constructionPrefix, hfields, List.length_cons, List.length_nil, + List.map_cons, List.map_nil, LayoutValue.prefixValue, List.take_succ_cons, + List.take_zero, List.foldl_cons, List.foldl_nil, nested_prefix_value, + initialAlignment, packingValue, Option.map_some, Option.getD_some] + rfl + have hd : constructionDomain fields (LayoutValue.initial (initialAlignment (some minimum))) + (some packed) := by + intro i hil + have hil' : i < 2 := by simpa only [hfields, List.length_cons, List.length_nil] using hil + have heither : i = 0 ∨ i = 1 := by omega + rcases heither with rfl | rfl + · simp only [constructionPrefix, LayoutValue.prefixValue, List.take_zero, List.foldl_nil, + initialAlignment, Option.map_some, Option.getD_some, LayoutValue.initial, + hfields, List.getElem_cons_zero, nestedPrefix, canonicalLayout, layoutValue, + LayoutValue.extendFits, packingValue, show (1#usize).val = 1 by simp] + have hmin : min 1 packed.val.val = 1 := Nat.min_eq_left (by omega) + simpa only [hmin, roundUp, Nat.zero_mod, Nat.mod_self, Nat.zero_add] using + (show alignmentDomain minimum.val.val ∧ alignmentDomain 1 ∧ True ∧ bytes.val ≤ Usize.max from + ⟨hm, ⟨⟨0, rfl⟩, by decide⟩, trivial, bounds.1⟩) + · rw [hprefix] + simp only [hfields, List.getElem_cons_succ, List.getElem_cons_zero] + refine ⟨hm, hi, hc, ?_⟩ + simp only [LayoutValue.extendFits, hf, packingValue, Option.map_some, Option.getD_some] + exact bounds.2 + have hlast : alignmentDomain (constructionPrefix fields + (LayoutValue.initial (initialAlignment (some minimum))) (some packed) fields.val.length).align := by + rw [hcomplete, layerFragment_align _ _ _ _ hmpos hppos] + exact hout + have hpad : (constructionPrefix fields (LayoutValue.initial (initialAlignment (some minimum))) + (some packed) fields.val.length).padFits Usize.max := by + rw [hcomplete] + exact layerFragment_padFits _ _ _ _ _ _ hf hmpos hppos hformulaPow houtPow hfit + step with for_repr_c_struct_spec (some minimum) (some packed) fields + (by intro a ha; cases ha; exact hm) (by intro a ha; cases ha; exact hp) + hd hlast hpad as ⟨result, hr, hcanonical⟩ + rw [hcomplete] at hr + have halign : result.align.val.val = max minimum.val.val (min inner.align.val.val packed.val.val) := by + have h := congrArg LayoutValue.align hr + simpa only [layoutValue, LayoutValue.pad, layerFragment_align _ _ _ _ hmpos hppos] using h + have hsize : ∀ n : Nat, (layoutValue result).size n = + roundUp (roundUp bytes.val (min inner.align.val.val packed.val.val) + + (layoutValue inner).size n) (max minimum.val.val (min inner.align.val.val packed.val.val)) := by + intro n + rw [hr] + exact layerFragment_pad_size _ _ _ _ _ _ hf hmpos hppos hformulaPow houtPow + have hpayload := congrArg LayoutValue.payload hr + have hfragment := layerFragment_payload (layoutValue inner) (trailingFormula tail) + minimum.val.val packed.val.val bytes.val hf hmpos hppos + simp only [LayoutValue.pad, hfragment] at hpayload + cases hresult : result.size_info with + | Sized size => simp only [layoutValue, hresult] at hpayload; contradiction + | SliceDst out => + have hformula : trailingFormula out = + ({ trailingFormula tail with base := roundUp bytes.val (min inner.align.val.val packed.val.val) + (trailingFormula tail).base, offset := roundUp bytes.val (min inner.align.val.val packed.val.val) + (trailingFormula tail).offset }).pad + (layerFragment (layoutValue inner) minimum.val.val packed.val.val bytes.val).align := by + simpa only [layoutValue, hresult, Payload.trailing.injEq] using hpayload + have hoffset := congrArg Formula.offset hformula + simp only [trailingFormula, byteFormula, Formula.pad] at hoffset + split at hoffset <;> simp only at hoffset + all_goals + refine ⟨hcanonical, halign, hsize, out, rfl, ?_⟩ + rw [hsize 0, hoffset] + have houter := (roundUp_properties + (roundUp bytes.val (min inner.align.val.val packed.val.val) + (layoutValue inner).size 0) + (max minimum.val.val (min inner.align.val.val packed.val.val)) + (Nat.pos_of_isPowerOfTwo houtPow)).1 + omega + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs.NestedReference + +def runtime (layers : List layout.nested_reference.NestedLayer) (elem alignment : Nat) + (inner : layout.DstLayout) : Prop := + canonicalLayout inner ∧ + (∀ n : Nat, ((layoutValue inner).size n, inner.align.val.val) = state layers elem alignment n) ∧ + ∃ tail, inner.size_info = .SliceDst tail ∧ tail.offset.val ≤ (layoutValue inner).size 0 + +def layerDomain (layer : layout.nested_reference.NestedLayer) : Prop := + layerValid layer ∧ layer.packed.val ≤ 2 ^ 29 + +end Zerocopy.Proofs.NestedReference + +namespace Zerocopy.Proofs.Raw +open LayoutMath NestedReference + +/-- Reverse construction terminates for any admitted descriptor length. Its +invariant keeps the physical tail offset and the complete per-metadata size. -/ +theorem nested_construction_loop_spec + (leading : Slice layout.nested_reference.NestedLayer) (elem alignment : Nat) + (inner : layout.DstLayout) (i : Usize) + (hvalid : NestedReference.valid leading.val elem alignment) + (ha : alignment ≤ 2 ^ 29) + (hb : ∀ layer ∈ leading.val, layer.packed.val ≤ 2 ^ 29) + (hfit : (NestedReference.state leading.val elem alignment 0).1 ≤ Usize.max) + (hi : i.val ≤ leading.val.length) + (hv : NestedReference.runtime (leading.val.drop i.val) elem alignment inner) : + layout.nested_reference.assert_matches_dst_layout_loop1 leading inner i + ⦃ out => NestedReference.runtime leading.val elem alignment out ⦄ := by + unfold layout.nested_reference.assert_matches_dst_layout_loop1 + apply loop.spec_decr_nat + (fun s : layout.DstLayout × Usize => s.2.val) + (fun s => s.2.val ≤ leading.val.length ∧ + NestedReference.runtime (leading.val.drop s.2.val) elem alignment s.1) + · rintro ⟨inner, idx⟩ ⟨hi, hv⟩ + dsimp only at hi hv ⊢ + unfold layout.nested_reference.assert_matches_dst_layout_loop1.body + simp only [bne_iff_ne] + split + · rename_i hn + have hpos : 0 < idx.val := by + have hz : idx.val ≠ 0 := by + intro h + apply hn + exact UScalar.eq_of_val_eq (by simpa using h) + omega + step with Usize.sub_spec (x := idx) (y := 1#usize) (by simp; omega) + as ⟨j, hj, _⟩ + have hj' : j.val + 1 = idx.val := by + change j.val = idx.val - 1 at hj + omega + have hjlt : j.val < leading.val.length := by omega + step with Slice.index_usize_spec leading j hjlt as ⟨layer, hlayer⟩ + have hlmem : layer ∈ leading.val := by rw [hlayer]; exact List.getElem_mem hjlt + have hl := hvalid.2.2 layer hlmem + have hpacknz : layer.packed ≠ 0#usize := by + intro h + have hp := Nat.pos_of_isPowerOfTwo hl.1 + have hz := congrArg UScalar.val h + simp only [show (0#usize).val = 0 by simp] at hz + omega + have hminnz : layer.min_align ≠ 0#usize := by + intro h + have hp := Nat.pos_of_isPowerOfTwo hl.2.1 + have hz := congrArg UScalar.val h + simp only [show (0#usize).val = 0 by simp] at hz + omega + simp only [core.num.nonzero.NonZero.new, cast_eq, hpacknz, hminnz, + ↓reduceDIte, ↓reduceIte, bind_ok, min_align_eq, lift] + let fields := Array.to_slice (Array.make 2#usize [nestedPrefix layer.prefix_bytes, inner]) + have hfields : fields.val = [nestedPrefix layer.prefix_bytes, inner] := rfl + have hinnerValid : NestedReference.valid (leading.val.drop idx.val) elem alignment := + ⟨hvalid.1, hvalid.2.1, fun layer hl => hvalid.2.2 layer (List.mem_of_mem_drop hl)⟩ + have halign : inner.align.val.val = + (NestedReference.state (leading.val.drop idx.val) elem alignment 0).2 := + congrArg Prod.snd (hv.2.1 0) + have hinnerDomain : alignmentDomain inner.align.val.val := by + rw [halign] + refine ⟨NestedReference.state_alignment_power _ _ _ _ hinnerValid, ?_⟩ + apply NestedReference.state_alignment_bound _ _ _ _ _ ha + intro layer hlmem + have hm := hvalid.2.2 layer (List.mem_of_mem_drop hlmem) + exact le_trans hm.2.2 (hb layer (List.mem_of_mem_drop hlmem)) + have hminimum : alignmentDomain layer.min_align.val := + ⟨hl.2.1, le_trans hl.2.2 (hb layer hlmem)⟩ + have hpacking : alignmentDomain layer.packed.val := ⟨hl.1, hb layer hlmem⟩ + have hmath : ∀ n : Nat, NestedReference.state (leading.val.drop j.val) elem alignment n = + NestedReference.step layer (NestedReference.state (leading.val.drop idx.val) elem alignment n) := by + intro n + rw [List.drop_eq_getElem_cons hjlt, NestedReference.state_cons, hj', ← hlayer] + obtain ⟨tail, htail, hoffset⟩ := hv.2.2 + have houterFit : roundUp (roundUp layer.prefix_bytes.val + (min inner.align.val.val layer.packed.val) + (layoutValue inner).size 0) + (max layer.min_align.val (min inner.align.val.val layer.packed.val)) ≤ Usize.max := by + have h := NestedReference.suffix_zero_size_fits leading.val elem alignment Usize.max j.val hfit + rw [hmath 0, ← hv.2.1 0] at h + exact h + change layout.DstLayout.for_repr_c_struct (some ⟨layer.min_align⟩) + (some ⟨layer.packed⟩) fields >>= _ ⦃ _ ⦄ + step with nested_layer_constructor_spec ⟨layer.min_align⟩ ⟨layer.packed⟩ + layer.prefix_bytes inner tail fields hfields hminimum hpacking hinnerDomain + hv.1 htail hoffset houterFit as ⟨out, hc, houtalign, houtsize, outtail, hoout, hoffout⟩ + refine ⟨by omega, ⟨hc, ?_, outtail, hoout, hoffout⟩, by omega⟩ + intro n + rw [hmath n, ← hv.2.1 n] + simp only [NestedReference.step, houtalign, houtsize] + · rename_i hz + have heq : idx.val = 0 := by + have h : idx = 0#usize := not_ne_iff.mp hz + simpa using congrArg UScalar.val h + simpa only [heq, List.drop_zero, WP.spec_ok] using hv + · exact ⟨hi, hv⟩ + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs.Raw +open NestedReference + +theorem nested_guard_loop_spec (maximum : NonZeroUsize) + (leading : Slice layout.nested_reference.NestedLayer) (i : Usize) (valid : Bool) + (hmaximum : maximum.val.val = 2 ^ 29) (hi : i.val ≤ leading.val.length) + (hv : valid = true → ∀ layer ∈ leading.val.take i.val, NestedReference.layerDomain layer) : + layout.nested_reference.assert_matches_dst_layout_loop0 maximum leading i valid + ⦃ out => out = true → ∀ layer ∈ leading.val, NestedReference.layerDomain layer ⦄ := by + unfold layout.nested_reference.assert_matches_dst_layout_loop0 + apply loop.spec_decr_nat + (fun s : Usize × Bool => leading.val.length - s.1.val) + (fun s => s.1.val ≤ leading.val.length ∧ + (s.2 = true → ∀ layer ∈ leading.val.take s.1.val, NestedReference.layerDomain layer)) + · rintro ⟨idx, valid⟩ ⟨hi, hv⟩ + dsimp only at hi hv ⊢ + unfold layout.nested_reference.assert_matches_dst_layout_loop0.body + simp only [Slice.len_val, Slice.length, UScalar.lt_equiv] + split + · rename_i hlt + step with Slice.index_usize_spec leading idx hlt as ⟨layer, hlayer⟩ + step as ⟨packedPow, hpow⟩ + have hcheck : (if packedPow then do + let b ← core.num.Usize.is_power_of_two layer.min_align + if b then + if layer.min_align > layer.packed then Result.ok false + else do + let bound ← core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner maximum + if layer.packed > bound then Result.ok false else Result.ok valid + else Result.ok false + else Result.ok false) + ⦃ next => next = true → valid = true ∧ NestedReference.layerDomain layer ⦄ := by + cases packedPow with + | false => simp + | true => + have hp : layer.packed.val.isPowerOfTwo := (Iff.of_eq hpow).mp rfl + simp only [if_true] + step as ⟨minimumPow, hminimum⟩ + cases minimumPow with + | false => simp + | true => + have hm : layer.min_align.val.isPowerOfTwo := (Iff.of_eq hminimum).mp rfl + simp only [if_true, core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv] + split + · simp + · rename_i hmin + split + · simp + · rename_i hpack + apply WP.spec.ret + intro hvalid + exact ⟨hvalid, ⟨hp, hm, by omega⟩, by omega⟩ + step with hcheck as ⟨next, hnext⟩ + have hlen := Slice.property leading + step with Usize.add_spec (x := idx) (y := 1#usize) (by simp; omega) as ⟨j, hj⟩ + change j.val = idx.val + 1 at hj + refine ⟨by omega, ?_, by omega⟩ + intro htrue item hitem + obtain ⟨hprevious, hl⟩ := hnext htrue + rw [hj, List.take_succ_eq_append_getElem hlt] at hitem + rcases List.mem_append.mp hitem with hleft | hright + · exact hv hprevious item hleft + · have heq : item = leading.val[idx.val] := List.mem_singleton.mp hright + rw [heq, ← hlayer] + exact hl + · rename_i hdone + have hend : idx.val = leading.val.length := by omega + simpa only [hend, List.take_length, WP.spec_ok] using hv + · exact ⟨hi, hv⟩ + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs.Raw +open LayoutMath NestedReference + +theorem nested_word_option_injective (a b : Option Usize) + (h : a.map UScalar.val = b.map UScalar.val) : a = b := by + cases a with + | none => cases b <;> simp_all + | some x => + cases b with + | none => simp_all + | some y => + have heq : x.val = y.val := by simpa only [Option.map_some, Option.some.injEq] using h + exact congrArg some (UScalar.eq_of_val_eq heq) + +/-- This ordinary assertion harness has no semantic precondition. Every invalid +descriptor returns successfully through a Rust guard, and every admitted +descriptor agrees with production sizing for every machine metadata count. -/ +theorem nested_reference_matches_spec + (leading : Slice layout.nested_reference.NestedLayer) (elem_size leaf_align elems : Usize) : + layout.nested_reference.assert_matches_dst_layout leading elem_size leaf_align elems + ⦃ _ => True ⦄ := by + classical + unfold layout.nested_reference.assert_matches_dst_layout + step as ⟨leafPow, hleafPow⟩ + cases leafPow with + | false => simp + | true => + have hpow : leaf_align.val.isPowerOfTwo := (Iff.of_eq hleafPow).mp rfl + have hpos := Nat.pos_of_isPowerOfTwo hpow + simp only [if_true] + step with current_max_align_spec as ⟨maximum, hmaximum⟩ + simp only [core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv] + split + · simp + · rename_i hleafBound + have hbound : leaf_align.val ≤ 2 ^ 29 := by omega + step with Usize.rem_spec elem_size (y := leaf_align) (by omega) as ⟨remainder, hr⟩ + simp only [bne_iff_ne] + split + · simp + · rename_i hremzero + have hstride : elem_size.val % leaf_align.val = 0 := by + have hz : remainder = 0#usize := not_ne_iff.mp hremzero + simpa only [hr, show (0#usize).val = 0 by simp] using congrArg UScalar.val hz + step with nested_guard_loop_spec maximum leading 0#usize true hmaximum + (by simp) (by simp) as ⟨valid, hvalid⟩ + cases valid with + | false => simp + | true => + have domains := hvalid rfl + have hv : NestedReference.valid leading.val elem_size.val leaf_align.val := + ⟨hpow, hstride, fun layer hl => (domains layer hl).1⟩ + have hb : ∀ layer ∈ leading.val, layer.packed.val ≤ 2 ^ 29 := + fun layer hl => (domains layer hl).2 + simp only [if_true] + step with nested_reference_size_spec leading elem_size leaf_align 0#usize + as ⟨initialSize, hsize0⟩ + cases initialSize with + | none => simp + | some zeroSize => + have hfit : (NestedReference.state leading.val elem_size.val leaf_align.val 0).1 ≤ Usize.max := by + simp only [Option.map_some, NestedReference.checkedSize, hv, if_true] at hsize0 + split at hsize0 + · assumption + · contradiction + have hnz : leaf_align ≠ 0#usize := by + intro h + have hz := congrArg UScalar.val h + simp only [show (0#usize).val = 0 by simp] at hz + omega + simp only [Option.isNone_some, Bool.false_eq_true, + core.num.nonzero.NonZero.new, cast_eq, hnz, ↓reduceDIte, ↓reduceIte, bind_ok] + step with encoding_new_spec ⟨leaf_align⟩ 0#usize hpow + (by simpa only [show (0#usize).val = 0 by simp] using hpos) as ⟨encoding, hencoding⟩ + let tail : layout.TrailingSliceLayout Usize := + { offset := 0#usize, elem_size, size_base := 0#usize, + size_rounding_align_and_phase := encoding } + let leaf : layout.DstLayout := + { align := ⟨leaf_align⟩, size_info := .SliceDst tail, statically_shallow_unpadded := true } + have hformula : trailingFormula tail = ⟨0, 0, leaf_align.val, elem_size.val, 0⟩ := by + have h := trailing_view tail leaf_align.val 0 hpow hpos hencoding + simpa only [tail, show (0#usize).val = 0 by simp] using h + have hstart : NestedReference.runtime (leading.val.drop (Slice.len leading).val) + elem_size.val leaf_align.val leaf := by + simp only [Slice.len_val, Slice.length, List.drop_length, NestedReference.runtime] + refine ⟨?_, ?_, tail, rfl, ?_⟩ + · simp only [canonicalLayout, leaf, tail] + simp only [Nat.add_zero] at hencoding + omega + · intro n + have haligned : n * elem_size.val % leaf_align.val = 0 := by + simp only [Nat.mul_mod, hstride, Nat.mul_zero, Nat.zero_mod] + simp only [layoutValue, leaf, LayoutValue.size, hformula, + Formula.size, Formula.bytes, Nat.zero_add, NestedReference.state, + List.foldr_nil, roundUp_eq _ _ haligned] + · simp only [tail, show (0#usize).val = 0 by simp] + omega + change layout.nested_reference.assert_matches_dst_layout_loop1 leading leaf + (Slice.len leading) >>= _ ⦃ _ ⦄ + step with nested_construction_loop_spec leading elem_size.val leaf_align.val + leaf (Slice.len leading) hv hbound hb hfit + (by simp only [Slice.len_val, Slice.length, le_refl]) hstart + as ⟨result, hruntime⟩ + obtain ⟨hcanonical, hsizes, resultTail, htail, hoffset⟩ := hruntime + rw [htail] + have htailPositive : 0 < resultTail.size_rounding_align_and_phase._0.val.val := by + simpa only [canonicalLayout, htail] using hcanonical + step with size_for_elems_spec resultTail elems htailPositive as ⟨actual, hactual⟩ + step with nested_reference_size_spec leading elem_size leaf_align elems as ⟨expected, hexpected⟩ + have hsize := congrArg Prod.fst (hsizes elems.val) + simp only [layoutValue, htail, LayoutValue.size] at hsize + have heq : actual = expected := by + apply nested_word_option_injective + rw [hactual, hexpected] + simp only [Formula.checkedSize, NestedReference.checkedSize, hv, if_true, hsize] + rw [← heq] + cases actual <;> simp [massert] + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem nested_reference_matches_spec : Zerocopy.Specs.nested_reference_matches_spec := by + intro leading elem_size leaf_align elems layers hl elemValue he alignmentValue ha metadataValue hn + apply WP.spec_mono (Raw.nested_reference_matches_spec leading elem_size leaf_align elems) + intro result _ + cases result + exact ⟨(), rfl, trivial⟩ +register_spec_step nested_reference_matches_spec + +end Zerocopy.Proofs + diff --git a/verification/aeneas/lean/Proofs/NestedReference.lean b/verification/aeneas/lean/Proofs/NestedReference.lean index 071f791689..8597927b8d 100644 --- a/verification/aeneas/lean/Proofs/NestedReference.lean +++ b/verification/aeneas/lean/Proofs/NestedReference.lean @@ -407,6 +407,17 @@ theorem nested_layers_decoder_total (raw : Slice layout.nested_reference.NestedL rintro result ⟨decoded, hdecoded, hr⟩ exact hr +@[contract_simps] theorem nested_reference_matches_spec_implies_required + (leading : Slice layout.nested_reference.NestedLayer) (elem_size leaf_align elems : Usize) + (run : Result Unit) + (provided : Zerocopy.Specs.nested_reference_matches_spec_contract leading elem_size leaf_align elems run) : + Zerocopy.Obligations.nested_reference_matches_spec_contract leading elem_size leaf_align elems run := by + obtain ⟨layers, hlayers⟩ := nested_layers_decoder_total leading + have execution := provided layers hlayers (unsignedWord elem_size) rfl + (unsignedWord leaf_align) rfl (unsignedWord elems) rfl + obtain ⟨output, hexec, _⟩ := WP.spec_imp_exists execution + exact ⟨output, hexec⟩ + @[contract_simps] theorem nested_round_up_spec_implies_required (size align : Usize) (run : Result (Option Usize)) (provided : Zerocopy.Specs.nested_round_up_spec_contract size align run) : diff --git a/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean b/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean index 922c105830..8fb5a6d648 100644 --- a/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean +++ b/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean @@ -67,4 +67,26 @@ theorem composition_options_admitted (words : Option NonZeroUsize) intro _ _ trivial +@[contract_simps] theorem required_composition_constructor_checks (repr_align packed : Option NonZeroUsize) + (fields : Slice layout.DstLayout) (references : Slice layout.composition_checks.ReferenceLayout) + (run : Result Unit) (provided : Specs.composition_constructor_checks_spec_contract repr_align packed fields references run) : + Obligations.composition_constructor_checks_spec_contract repr_align packed fields references run := by + intro align_positive packed_positive fields_valid + obtain ⟨align_value, align_decode⟩ := composition_options_admitted repr_align align_positive + obtain ⟨packed_value, packed_decode⟩ := composition_options_admitted packed packed_positive + have fields_admitted : isValid fields := by + rw [slice_valid_iff] + intro field member + exact (layout_decoder_admitted_iff field).mpr (fields_valid field member) + have references_admitted : isValid references := by + rw [slice_valid_iff] + intro reference _ + exact composition_reference_admitted reference + obtain ⟨fields_value, fields_decode⟩ := fields_admitted + obtain ⟨references_value, references_decode⟩ := references_admitted + apply WP.spec_mono (provided align_value align_decode packed_value packed_decode fields_value fields_decode + references_value references_decode) + intro _ _ + trivial + end Zerocopy.Proofs diff --git a/zerocopy/src/layout/composition_checks.rs b/zerocopy/src/layout/composition_checks.rs index be7f3184ab..1c41ad2920 100644 --- a/zerocopy/src/layout/composition_checks.rs +++ b/zerocopy/src/layout/composition_checks.rs @@ -193,6 +193,36 @@ fn reference_pad(reference: ReferenceLayout) -> Option { Some(ReferenceLayout { size, unpadded: reference.unpadded & no_static_padding, ..reference }) } +/// Compose an arbitrary field slice, then add the final record's padding. +/// Each field contributes its entire size, so packing this record preserves +/// padding that belongs to an inner record. +fn reference_constructor( + repr_align: Option, + packed: Option, + fields: &[ReferenceLayout], +) -> Option { + let align = match repr_align { + Some(align) => align.get(), + None => 1, + }; + if !extension_alignment(align) { + return None; + } + let mut state = Some(ReferenceLayout { align, size: ReferenceSize::Fixed(0), unpadded: true }); + let mut i = 0; + while i < fields.len() { + state = match state { + Some(preceding) => reference_extend(preceding, fields[i], packed), + None => None, + }; + i += 1; + } + match state { + Some(reference) => reference_pad(reference), + None => None, + } +} + /// Check extension against every stored reference observation on the exact /// checked-arithmetic domain where the production operation can succeed. /// @@ -231,3 +261,32 @@ fn check_pad(runtime_layout: DstLayout, reference: ReferenceLayout) { } } } + +/// Check arbitrary-length construction against independent field composition. +/// +/// ```aeneas +/// spec composition_constructor_checks_spec +/// ensures _ => True +/// ``` +fn check_constructor( + repr_align: Option, + packed: Option, + fields: &[DstLayout], + references: &[ReferenceLayout], +) { + if fields.len() != references.len() { + return; + } + let mut matching = true; + let mut i = 0; + while i < fields.len() { + matching = matching && matches_reference(fields[i], references[i]); + i += 1; + } + if matching { + if let Some(expected) = reference_constructor(repr_align, packed, references) { + let actual = DstLayout::for_repr_c_struct(repr_align, packed, fields); + assert!(matches_reference(actual, expected)); + } + } +} diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index 31e59e5091..f2a5849ba2 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -1237,6 +1237,19 @@ impl DstLayout { #[cfg_attr(kani, kani::ensures(|&result| { Some(result) == proofs::repr_c_layout(repr_align, repr_packed, fields) }))] + /// + /// ```aeneas + /// spec for_repr_c_struct_spec + /// requires(raw) ha : ∀ a ∈ repr_align, alignmentDomain a.val.val + /// requires(raw) hp : ∀ a ∈ repr_packed, alignmentDomain a.val.val + /// requires(raw) hd : constructionDomain fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) repr_packed + /// requires(raw) hlast : alignmentDomain + /// (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) repr_packed fields.val.length).align + /// requires(raw) hfit : (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) + /// repr_packed fields.val.length).padFits Usize.max + /// ensures(raw) r => layoutValue r = + /// (constructionPrefix fields (LayoutMath.LayoutValue.initial (initialAlignment repr_align)) repr_packed fields.val.length).pad + /// ``` pub const fn for_repr_c_struct( repr_align: Option, repr_packed: Option, @@ -1255,22 +1268,24 @@ impl DstLayout { let _ = DstLayout::for_repr_c_struct(kani::any(), kani::any(), &fields[..len]); } - let mut layout = DstLayout::new_zst(repr_align); + // A local named `layout` shadows Aeneas's generated Lean namespace. + // Keep this name distinct so the extracted calls resolve correctly. + let mut result = DstLayout::new_zst(repr_align); let mut i = 0; #[allow(clippy::arithmetic_side_effects)] while i < fields.len() { #[allow(clippy::indexing_slicing)] let field = fields[i]; - layout = layout.extend(field, repr_packed); + result = result.extend(field, repr_packed); i += 1; } - layout = layout.pad_to_align(); + result = result.pad_to_align(); - // SAFETY: `layout` accurately describes the layout of a `repr(C)` + // SAFETY: `result` accurately describes the result of a `repr(C)` // struct with `repr_align` or `repr_packed` alignment modifications and - // the given `fields`. The `layout` is constructed using a sequence of + // the given `fields`. The `result` is constructed using a sequence of // invocations of `DstLayout::{new_zst,extend,pad_to_align}`. The // documentation of these items vows that invocations in this manner // will accurately describe a type, so long as: @@ -1280,7 +1295,7 @@ impl DstLayout { // - the presence of `repr_align` and `repr_packed` are correctly accounted for. // // We respect all three of these preconditions above. - layout + result } /// Like `Layout::extend`, this creates a layout that describes a record @@ -2279,6 +2294,14 @@ mod tests { &[(nz(1), nz(1), 1), (nz(2), nz(2), 3), (nz(8), nz(8), 5)], ]; for &leading in cases { + let reference_layers: Vec<_> = leading + .iter() + .map(|&(packed, align, prefix)| nested_reference::NestedLayer { + packed: packed.get(), + min_align: align.get(), + prefix_bytes: prefix, + }) + .collect(); for &(elem_size, alignment) in &[(0, 1), (0, 8), (1, 1), (2, 2), (3, 1), (8, 8)] { let alignment = nz(alignment); let expected = size_for_metadata_model(leading, elem_size, alignment); @@ -2290,6 +2313,12 @@ mod tests { max_elems.saturating_add(1), usize::MAX, ]) { + nested_reference::assert_matches_dst_layout( + &reference_layers, + elem_size, + alignment.get(), + elems, + ); assert_eq!( actual(elems), expected(elems), diff --git a/zerocopy/src/layout/nested_reference.rs b/zerocopy/src/layout/nested_reference.rs index f13b4e0e10..d65400e2db 100644 --- a/zerocopy/src/layout/nested_reference.rs +++ b/zerocopy/src/layout/nested_reference.rs @@ -18,6 +18,12 @@ // also leave the overflow paths visible in this independent reference. #![allow(clippy::question_mark, clippy::manual_map)] +#[cfg(not(kani))] +use core::num::NonZeroUsize; + +#[cfg(not(kani))] +use super::{DstLayout, RoundingAlignAndPhase, SizeInfo, TrailingSliceLayout}; + /// One containing record, before placing its final field. /// /// Plain words make the descriptor's mathematical decoding total. The Rust @@ -118,3 +124,98 @@ pub(super) fn size_for_metadata( None => None, } } + +/// Checks the production layout against the independent size calculation. +/// +/// The guards expose the construction domain as ordinary Rust. Invalid +/// descriptors, alignments above the production constructor's documented +/// bound, and unrepresentable static layouts return immediately. Every +/// element count is compared, including dynamic overflow and zero-size tails. +/// +/// A total `_ => True` specification proves that these ordinary assertions +/// cannot fail; the comparison itself is part of the extracted computation. +/// +/// ```aeneas +/// spec nested_reference_matches_spec +/// ensures(raw) _ => True +/// ``` +#[cfg(not(kani))] +#[allow(clippy::arithmetic_side_effects, clippy::indexing_slicing)] +pub(super) fn assert_matches_dst_layout( + leading: &[NestedLayer], + elem_size: usize, + leaf_align: usize, + elems: usize, +) { + if !leaf_align.is_power_of_two() + || leaf_align > DstLayout::CURRENT_MAX_ALIGN.get() + || elem_size % leaf_align != 0 + { + return; + } + let mut i = 0; + let mut valid = true; + while i < leading.len() { + let layer = leading[i]; + if !layer.packed.is_power_of_two() + || !layer.min_align.is_power_of_two() + || layer.min_align > layer.packed + || layer.packed > DstLayout::CURRENT_MAX_ALIGN.get() + { + valid = false; + } + i += 1; + } + if !valid { + return; + } + if size_for_metadata(leading, elem_size, leaf_align, 0).is_none() { + return; + } + let leaf_align = match NonZeroUsize::new(leaf_align) { + Some(a) => a, + None => return, + }; + let mut runtime_layout = DstLayout { + align: leaf_align, + size_info: SizeInfo::SliceDst(TrailingSliceLayout { + offset: 0, + elem_size, + size_base: 0, + size_rounding_align_and_phase: RoundingAlignAndPhase::new(leaf_align, 0), + }), + statically_shallow_unpadded: true, + }; + let mut i = leading.len(); + while i != 0 { + i -= 1; + let layer = leading[i]; + let packed = match NonZeroUsize::new(layer.packed) { + Some(a) => a, + None => DstLayout::MIN_ALIGN, + }; + let min_align = match NonZeroUsize::new(layer.min_align) { + Some(a) => a, + None => DstLayout::MIN_ALIGN, + }; + let prefix = DstLayout { + align: DstLayout::MIN_ALIGN, + size_info: SizeInfo::Sized { size: layer.prefix_bytes }, + statically_shallow_unpadded: true, + }; + runtime_layout = + DstLayout::for_repr_c_struct(Some(min_align), Some(packed), &[prefix, runtime_layout]); + } + let actual = match runtime_layout.size_info { + SizeInfo::Sized { size } => Some(size), + SizeInfo::SliceDst(tail) => tail.size_for_elems(elems), + }; + let expected = size_for_metadata(leading, elem_size, leaf_align.get(), elems); + // Primitive comparisons keep the assertion visible without bringing + // formatting or Option's trait dictionary into the extraction. + match (actual, expected) { + (Some(actual), Some(expected)) => assert!(actual == expected), + (None, None) => (), + _ => panic!("nested layout size differs from the independent reference"), + } +}