diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index f222d889e4..59c094fcce 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -56,35 +56,6 @@ allocator admission additionally needs the outer alignment and the signed metadata-size bound. Allocator behavior, zeroing, and `Box` validity remain separate Rust obligations. -Six concrete wrappers in [`lib.rs`](../../zerocopy/src/lib.rs) call the actual -`PointerMetadata` implementations for `()` and `usize`. Their contracts check -element-count conversion, layout-variant handling, and checked metadata sizing. -Using these results for an arbitrary `KnownLayout` implementation requires -separate layout correspondence. - -The numerical harness in [`split_at.rs`](../../zerocopy/src/split_at.rs) compares -split sizes with the independent remainder-based reference. It checks physical -tail containment and the zero-padding gate. The shared length helper also runs -in the production pointer path. These proofs establish bounds and disjoint byte -intervals, including empty and zero-sized tails; pointer validity and provenance -remain separate Rust obligations. - -The checks in [`pointer/mod.rs`](../../zerocopy/src/pointer/mod.rs) follow the -actual `CastUnsized` layout gate. Accepted DST pairs retain alignment, physical -tail offset, and complete sizes for every metadata count. Sized pairs need only -equal sizes, including zero-sized layouts with different alignments. Rejection -does not claim that a cast would be impossible. The proof covers the numerical -decision and sizing comparison, not the resulting pointer's validity. - -The checks in [`util/allocation.rs`](../../zerocopy/src/util/allocation.rs) cover -actual metadata sizing and exact preparation of allocator arguments. Preparation -preserves every optional size and the supplied alignment, without adding a -runtime validity filter. Under explicit correspondence to a valid recursive -layout, separate lemmas establish complete size and tail containment. Numerical -allocator admission additionally needs the outer alignment and the signed -metadata-size bound. Allocator behavior, zeroing, and `Box` validity remain -separate Rust obligations. - These harnesses use the same annotation and proof rules as every other function. There is no root marker or separately maintained list of required functions. Every present specification must have its corresponding proof in both CI builds. @@ -291,8 +262,6 @@ whole-program unsafe-code certification. ## Scope and proofs -Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [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. The current function specifications cover the layout and arithmetic methods and their Rust @@ -364,36 +333,6 @@ fit requirements; arbitrary malformed internal layout records need not succeed. Generic size/alignment reads are explicit external data inputs, never axioms asserting layout correctness. -`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. - -A positive size-sequence comparison establishes equal sizes for every natural -metadata value; a negative result does not assert that the sequences differ. - -Cast validation and exact metadata inference establish error priority, exact -splits and rejection of unattainable sizes. Intentional zero-stride panic is -checked separately. - Plain arithmetic clauses use mathematical word values carrying machine bounds and, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary @@ -1344,14 +1283,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 57ff6eb8d3..98dafb6fef 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 @@ -111,9 +121,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 diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index fd8a4e8996..f24c23bc95 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -959,7 +959,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) : @@ -1030,7 +1030,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) @@ -1172,7 +1172,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 @@ -1611,6 +1611,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 312:0-318:1 -/ def util.min @@ -1686,7 +1758,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) @@ -1813,7 +1885,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 @@ -1843,7 +1915,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 @@ -1948,7 +2020,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) : @@ -1982,12 +2054,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 -/ @@ -2012,6 +2078,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 -/ @@ -2066,14 +2258,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 @@ -2098,7 +2290,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 48:0-58:1 -/ + Source: 'src/layout/nested_reference.rs', lines 54:0-64:1 -/ def layout.nested_reference.round_up (size : Std.Usize) (align : Std.Usize) : Result (Option Std.Usize) := do if align = 0#usize @@ -2111,7 +2303,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 60:0-82:1 -/ + Source: 'src/layout/nested_reference.rs', lines 66:0-88:1 -/ def layout.nested_reference.apply_layer (layer : layout.nested_reference.NestedLayer) (size : Std.Usize) (alignment : Std.Usize) : @@ -2151,7 +2343,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 110:4-117:5 -/ + Source: 'src/layout/nested_reference.rs', lines 116:4-123:5 -/ @[rust_loop_body] def layout.nested_reference.size_for_metadata_loop.body (leading : Slice layout.nested_reference.NestedLayer) @@ -2172,7 +2364,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 110:4-117:5 -/ + Source: 'src/layout/nested_reference.rs', lines 116:4-123:5 -/ @[rust_loop] def layout.nested_reference.size_for_metadata_loop (leading : Slice layout.nested_reference.NestedLayer) @@ -2185,7 +2377,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 96:0-122:1 -/ + Source: 'src/layout/nested_reference.rs', lines 102:0-128: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) : @@ -2212,6 +2404,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 160:4-170: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 160:4-170: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 192:4-210: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 192:4-210: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 146:0-223: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 41e7bcb68e..e5c868118c 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -256,7 +256,7 @@ structure layout.composition_checks.ReferenceLayout where unpadded : Bool /-- [zerocopy::layout::nested_reference::NestedLayer] - Source: 'src/layout/nested_reference.rs', lines 29:0-33:1 -/ + Source: 'src/layout/nested_reference.rs', lines 35:0-39: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 01ffe7113a..019f7b397f 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/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/Contracts.lean b/verification/aeneas/lean/Proofs/Contracts.lean index fead244b30..5e3bab8bad 100644 --- a/verification/aeneas/lean/Proofs/Contracts.lean +++ b/verification/aeneas/lean/Proofs/Contracts.lean @@ -443,6 +443,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/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/Proofs/Raw/Composition.lean b/verification/aeneas/lean/Proofs/Raw/Composition.lean index c82c2964da..d77e6e81d1 100644 --- a/verification/aeneas/lean/Proofs/Raw/Composition.lean +++ b/verification/aeneas/lean/Proofs/Raw/Composition.lean @@ -31,7 +31,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 diff --git a/verification/aeneas/lean/Proofs/Raw/Construction.lean b/verification/aeneas/lean/Proofs/Raw/Construction.lean index c84832cfae..2f6d7fa5d0 100644 --- a/verification/aeneas/lean/Proofs/Raw/Construction.lean +++ b/verification/aeneas/lean/Proofs/Raw/Construction.lean @@ -96,4 +96,90 @@ 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 diff --git a/verification/aeneas/lean/Proofs/Raw/Encoding.lean b/verification/aeneas/lean/Proofs/Raw/Encoding.lean index cdc423f303..10fa47cc51 100644 --- a/verification/aeneas/lean/Proofs/Raw/Encoding.lean +++ b/verification/aeneas/lean/Proofs/Raw/Encoding.lean @@ -23,6 +23,7 @@ import all Init.Data.Nat.Power2.Basic 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. @@ -92,6 +93,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. -/ diff --git a/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean b/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean index e38dabb013..5f61929e04 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/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 2ff692e2a9..132bea595f 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -176,6 +176,14 @@ spec composition_pad_checks_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.composition_pad_checks_spec for Zerocopy.layout.composition_checks.check_pad with 2 +check_model_inputs Zerocopy.layout.composition_checks.check_constructor with 0 type parameters +aeneas_spec_begin +spec composition_constructor_checks_spec + for @Zerocopy.layout.composition_checks.check_constructor with 0 type parameters + ensures _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.composition_constructor_checks_spec for Zerocopy.layout.composition_checks.check_constructor with 4 + check_model_inputs Zerocopy.layout.RoundingAlignAndPhase.new with 0 type parameters aeneas_spec_begin spec encoding_new_spec @@ -337,6 +345,22 @@ spec for_slice_spec (size align : Usize) aeneas_spec_end check_spec_binding Zerocopy.Specs.for_slice_spec for Zerocopy.layout.DstLayout.for_slice with 1 +check_model_inputs Zerocopy.layout.DstLayout.for_repr_c_struct with 0 type parameters +aeneas_spec_begin +spec for_repr_c_struct_spec + for @Zerocopy.layout.DstLayout.for_repr_c_struct with 0 type parameters + 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 +aeneas_spec_end +check_spec_binding Zerocopy.Specs.for_repr_c_struct_spec for Zerocopy.layout.DstLayout.for_repr_c_struct with 3 + check_model_inputs Zerocopy.layout.DstLayout.extend with 0 type parameters aeneas_spec_begin spec extend_spec @@ -431,6 +455,14 @@ spec nested_reference_size_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.nested_reference_size_spec for Zerocopy.layout.nested_reference.size_for_metadata with 4 +check_model_inputs Zerocopy.layout.nested_reference.assert_matches_dst_layout with 0 type parameters +aeneas_spec_begin +spec nested_reference_matches_spec + for @Zerocopy.layout.nested_reference.assert_matches_dst_layout with 0 type parameters + ensures(raw) _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.nested_reference_matches_spec for Zerocopy.layout.nested_reference.assert_matches_dst_layout with 4 + check_model_inputs Zerocopy.layout.primitive_checks.check_primitive_layouts with 1 type parameters aeneas_spec_begin spec primitive_layout_checks_spec 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 acba2289bb..76c7b3cc4e 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 @@ -2393,6 +2408,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); @@ -2404,6 +2427,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 c43d91e93c..5b0d9ba691 100644 --- a/zerocopy/src/layout/nested_reference.rs +++ b/zerocopy/src/layout/nested_reference.rs @@ -20,6 +20,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 @@ -120,3 +126,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"), + } +}