From 777bc8236f7c6c691159058438e378185adeede2 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 10:46:24 -0400 Subject: [PATCH] Prove exact trailing sizes, padding and capacity Connect conditional trailing-layout contracts to independent unbounded formulas for size, capacity, wrapping padding and checked overflow. Preserve the broad Raw arithmetic lemmas used by composition proofs. Express trailing-size specifications through the existing mathematical formula and optional decoded size. Prove that the compact contract still implies the independently authored exact representation obligations. Compare complete optional trailing sizes and capacities with independent checked Rust arithmetic. Visible alignment/phase witnesses cover every nonzero encoding without restricting physical offsets or imposing extra size bounds. Validation: fresh pinned extraction and complete-model golden comparison; independent golden/live Lean builds, required-contract checks, and the transitive axiom audit. gherrit-pr-id: Gsnkt6couze5saom2wzruz5yjl6gkrcsg Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 6 +- verification/aeneas/golden/Funs.lean | 263 +++++++++++++-- verification/aeneas/golden/Types.lean | 8 +- verification/aeneas/lean/Corollaries.lean | 61 +++- verification/aeneas/lean/MathViews.lean | 20 +- .../aeneas/lean/ModelProjectionLaws.lean | 9 + verification/aeneas/lean/Obligations.lean | 44 +++ .../aeneas/lean/Obligations/TailChecks.lean | 33 ++ verification/aeneas/lean/Proofs.lean | 308 +++++++++++++++++- .../aeneas/lean/Proofs/TailChecks.lean | 83 +++++ .../aeneas/lean/Proofs/TailReference.lean | 237 ++++++++++++++ .../RequiredModelContracts/TailChecks.lean | 36 ++ zerocopy/src/layout/mod.rs | 26 ++ zerocopy/src/layout/tail_checks.rs | 111 +++++++ 14 files changed, 1189 insertions(+), 56 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/TailChecks.lean create mode 100644 verification/aeneas/lean/Proofs/TailChecks.lean create mode 100644 verification/aeneas/lean/Proofs/TailReference.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/TailChecks.lean create mode 100644 zerocopy/src/layout/tail_checks.rs diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 66ae4ec727..213ba54302 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -121,7 +121,7 @@ zerocopy's unsafe pointer operations are sound. ## Scope and proofs -Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs). +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). Extraction starts from the function and nominal-type owners of every present `aeneas` fence in `zerocopy/src`, including their dependencies. Every present @@ -137,6 +137,7 @@ added without extending the specification set. | `DstLayout::{assume_shallow_unpadded,new_zst,for_type,for_unpadded_type,for_slice}` | Exact alignment, size-information fields, and recorded shallow-padding flags under explicit input premises. | | `SizeInfo::try_to_nonzero_elem_size`, `max_elems_for_bytes` | Exact zero handling, preserved representation fields, and greatest fitting element count. | | `DstLayout::requires_static_padding` | Exact negation of the recorded shallow-unpadded flag. | +| Trailing size, padding, and capacity | Exact size-offset and capacity formulas, checked-size overflow, and wrapping padding; successful sizes and physical padding refine the independent recursive semantics. | Every registered function uses total `spec`: accepted raw representations, supplied mathematical ghosts, and explicit requirements imply successful @@ -165,6 +166,9 @@ 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. + Plain arithmetic clauses use mathematical word values carrying machine bounds and NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw clauses preserve the extracted representation vocabulary while retaining diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index d6426bef15..68124969b4 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -643,14 +643,14 @@ def byteorder.verification.set_u32_be byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 /-- [zerocopy::layout::POINTER_WIDTH_BITS] - Source: 'src/layout/mod.rs', lines 23:0-23:62 -/ + Source: 'src/layout/mod.rs', lines 26:0-26:62 -/ @[global_simps, irreducible] def layout.POINTER_WIDTH_BITS : Result Std.Usize := do let i ← core.mem.size_of Std.Usize i * 8#usize /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::new]: - Source: 'src/layout/mod.rs', lines 103:4-122:5 -/ + Source: 'src/layout/mod.rs', lines 106:4-125:5 -/ def layout.RoundingAlignAndPhase.new (align : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : @@ -671,7 +671,7 @@ def layout.RoundingAlignAndPhase.new | some encoded1 => ok { _0 := encoded1 } /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]: - Source: 'src/layout/mod.rs', lines 136:4-163:5 -/ + Source: 'src/layout/mod.rs', lines 139:4-166:5 -/ def layout.RoundingAlignAndPhase.components (self : layout.RoundingAlignAndPhase) : Result ((core.num.nonzero.NonZero Std.Usize @@ -699,7 +699,7 @@ def layout.RoundingAlignAndPhase.components ok (align1, phase) /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]: - Source: 'src/layout/mod.rs', lines 176:4-185:5 -/ + Source: 'src/layout/mod.rs', lines 179:4-188:5 -/ def layout.RoundingAlignAndPhase.align (self : layout.RoundingAlignAndPhase) : Result (core.num.nonzero.NonZero Std.Usize @@ -708,8 +708,126 @@ def layout.RoundingAlignAndPhase.align let (nz, _) ← layout.RoundingAlignAndPhase.components self ok nz +/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: + Source: 'src/util/mod.rs', lines 261:0-279:1 -/ +def util.round_down_to_next_multiple_of_alignment + (n : Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) : + Result Std.Usize + := do + let align1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let b ← core.num.Usize.is_power_of_two align1 + massert b + let i ← align1 - 1#usize + let mask ← lift (~~~ i) + ok (n &&& mask) + +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_offset]: + Source: 'src/layout/mod.rs', lines 268:4-281:5 -/ +def layout.TrailingSliceLayout.size_offset + {E : Type} (self : layout.TrailingSliceLayout E) : Result Std.Usize := do + let (size_align, size_phase) ← + layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase + let aligned_base ← + util.round_down_to_next_multiple_of_alignment self.size_base size_align + ok (aligned_base ||| size_phase) + +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::max_trailing_bytes]: + Source: 'src/layout/mod.rs', lines 304:4-393:5 -/ +def layout.TrailingSliceLayout.max_trailing_bytes + {E : Type} (self : layout.TrailingSliceLayout E) + (available_bytes : Std.Usize) : + Result (Option Std.Usize) + := do + let (size_align, size_phase) ← + layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase + let rounded_phase ← + if size_phase = 0#usize + then ok 0#usize + else + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align + let o ← lift (Usize.checked_add self.size_base rounded_phase) + match o with + | none => ok none + | some size => + let o1 ← lift (Usize.checked_sub available_bytes size) + match o1 with + | none => ok none + | some bytes => + let aligned_bytes ← + util.round_down_to_next_multiple_of_alignment bytes size_align + let initial_padding ← rounded_phase - size_phase + let trailing_bytes ← lift (aligned_bytes ||| initial_padding) + ok (some trailing_bytes) + +/-- [zerocopy::util::padding_needed_for]: + Source: 'src/util/mod.rs', lines 169:0-229:1 -/ +def util.padding_needed_for + (len : Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) : + Result Std.Usize + := do + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let mask ← i - 1#usize + let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize) + let i2 ← lift (~~~ i1) + ok (i2 &&& mask) + +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::padding_for_elems]: + Source: 'src/layout/mod.rs', lines 418:4-473:5 -/ +def layout.TrailingSliceLayoutUsize.padding_for_elems + (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : + Result Std.Usize + := do + let (size_align, size_phase) ← + layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align + let size_mask ← i - 1#usize + let elem_remainder ← lift (self.elem_size &&& size_mask) + let i1 ← lift (core.num.Usize.wrapping_mul elems elem_remainder) + let trailing_remainder ← lift (i1 &&& size_mask) + let rounding_input ← + lift (core.num.Usize.wrapping_add size_phase trailing_remainder) + let rounding_padding ← util.padding_needed_for rounding_input size_align + let i2 ← lift (core.num.Usize.wrapping_add self.size_base size_phase) + let i3 ← lift (core.num.Usize.wrapping_sub i2 self.offset) + ok (core.num.Usize.wrapping_add i3 rounding_padding) + +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_for_elems]: + Source: 'src/layout/mod.rs', lines 491:4-555:5 -/ +def layout.TrailingSliceLayoutUsize.size_for_elems + (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : + Result (Option Std.Usize) + := do + let o ← + layout.TrailingSliceLayout.max_trailing_bytes self core.num.Usize.MAX + match o with + | none => ok none + | some bytes => + let o1 ← lift (Usize.checked_mul self.elem_size elems) + match o1 with + | none => ok none + | some bytes1 => + if bytes1 > bytes + then ok none + else + let trailing_end ← + lift (core.num.Usize.wrapping_add self.offset bytes1) + let i ← layout.TrailingSliceLayoutUsize.padding_for_elems self elems + let size ← lift (core.num.Usize.wrapping_add trailing_end i) + ok (some size) + /-- [zerocopy::layout::{zerocopy::layout::SizeInfo}::try_to_nonzero_elem_size]: - Source: 'src/layout/mod.rs', lines 791:4-819:5 -/ + Source: 'src/layout/mod.rs', lines 817:4-845:5 -/ def layout.SizeInfoUsize.try_to_nonzero_elem_size (self : layout.SizeInfo Std.Usize) : Result (Option (layout.SizeInfo (core.num.nonzero.NonZero Std.Usize @@ -734,7 +852,7 @@ def layout.SizeInfoUsize.try_to_nonzero_elem_size })) /-- [zerocopy::layout::max_elems_for_bytes]: - Source: 'src/layout/mod.rs', lines 847:0-862:1 -/ + Source: 'src/layout/mod.rs', lines 873:0-888:1 -/ def layout.max_elems_for_bytes (bytes : Std.Usize) (elem_size : core.num.nonzero.NonZero Std.Usize @@ -751,7 +869,7 @@ def layout.max_elems_for_bytes | some used => ok (elems, used) /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::MIN_ALIGN] - Source: 'src/layout/mod.rs', lines 882:4-885:6 -/ + Source: 'src/layout/mod.rs', lines 908:4-911:6 -/ @[global_simps, irreducible] def layout.DstLayout.MIN_ALIGN : @@ -766,13 +884,13 @@ def layout.DstLayout.MIN_ALIGN | some min_align => ok min_align /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::assume_shallow_unpadded]: - Source: 'src/layout/mod.rs', lines 951:4-960:5 -/ + Source: 'src/layout/mod.rs', lines 977:4-986:5 -/ def layout.DstLayout.assume_shallow_unpadded (self : layout.DstLayout) : Result layout.DstLayout := do ok { self with statically_shallow_unpadded := true } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::new_zst]: - Source: 'src/layout/mod.rs', lines 989:4-1009:5 + Source: 'src/layout/mod.rs', lines 1015:4-1035:5 Visibility: public -/ def layout.DstLayout.new_zst (repr_align : Option (core.num.nonzero.NonZero Std.Usize @@ -796,7 +914,7 @@ def layout.DstLayout.new_zst } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_type]: - Source: 'src/layout/mod.rs', lines 1033:4-1058:5 + Source: 'src/layout/mod.rs', lines 1059:4-1084:5 Visibility: public -/ def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do let i ← core.mem.align_of T @@ -815,7 +933,7 @@ def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_unpadded_type]: - Source: 'src/layout/mod.rs', lines 1088:4-1102:5 + Source: 'src/layout/mod.rs', lines 1114:4-1128:5 Visibility: public -/ def layout.DstLayout.for_unpadded_type (T : Type) : Result layout.DstLayout := do @@ -823,7 +941,7 @@ def layout.DstLayout.for_unpadded_type layout.DstLayout.assume_shallow_unpadded dl /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_slice]: - Source: 'src/layout/mod.rs', lines 1127:4-1163:5 -/ + Source: 'src/layout/mod.rs', lines 1153:4-1189:5 -/ def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do let i ← core.mem.align_of T let o ← @@ -849,7 +967,7 @@ 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 1554:4-1563:5 + Source: 'src/layout/mod.rs', lines 1580:4-1589:5 Visibility: public -/ def layout.DstLayout.requires_static_padding (self : layout.DstLayout) : Result Bool := do @@ -1062,38 +1180,115 @@ def layout.primitive_checks.check_empty_layout massert empty.statically_shallow_unpadded else ok () -/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: - Source: 'src/util/mod.rs', lines 261:0-279:1 -/ -def util.round_down_to_next_multiple_of_alignment - (n : Std.Usize) +/-- [zerocopy::layout::tail_checks::same_optional_usize]: + Source: 'src/layout/tail_checks.rs', lines 29:0-35:1 -/ +def layout.tail_checks.same_optional_usize + (left : Option Std.Usize) (right : Option Std.Usize) : Result Bool := do + match left with + | none => match right with + | none => ok true + | some _ => ok false + | some left1 => + match right with + | none => ok false + | some right1 => ok (left1 = right1) + +/-- [zerocopy::layout::tail_checks::reference_round_up]: + Source: 'src/layout/tail_checks.rs', lines 38:0-42:1 -/ +def layout.tail_checks.reference_round_up + (bytes : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) : - Result Std.Usize + Result (Option Std.Usize) := do - let align1 ← + let i ← core.num.nonzero.NonZero.get Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align - let b ← core.num.Usize.is_power_of_two align1 - massert b - let i ← align1 - 1#usize - let mask ← lift (~~~ i) - ok (n &&& mask) + let remainder ← bytes % i + let padding ← if remainder = 0#usize + then ok 0#usize + else i - remainder + ok (Usize.checked_add bytes padding) + +/-- [zerocopy::layout::tail_checks::reference_size]: + Source: 'src/layout/tail_checks.rs', lines 44:0-60:1 -/ +def layout.tail_checks.reference_size + (tail : layout.TrailingSliceLayout Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (elems : Std.Usize) : + Result (Option Std.Usize) + := do + let o ← lift (Usize.checked_mul elems tail.elem_size) + match o with + | none => ok none + | some bytes => + let o1 ← lift (Usize.checked_add phase bytes) + match o1 with + | none => ok none + | some input => + let o2 ← layout.tail_checks.reference_round_up input align + match o2 with + | none => ok none + | some rounded => ok (Usize.checked_add tail.size_base rounded) -/-- [zerocopy::util::padding_needed_for]: - Source: 'src/util/mod.rs', lines 169:0-229:1 -/ -def util.padding_needed_for - (len : Std.Usize) +/-- [zerocopy::layout::tail_checks::reference_capacity]: + Source: 'src/layout/tail_checks.rs', lines 63:0-76:1 -/ +def layout.tail_checks.reference_capacity + (tail : layout.TrailingSliceLayout Std.Usize) (align : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) : - Result Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (budget : Std.Usize) : + Result (Option Std.Usize) + := do + let o ← lift (Usize.checked_sub budget tail.size_base) + match o with + | none => ok none + | some after_base => + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let i1 ← after_base % i + let rounded_budget ← after_base - i1 + ok (Usize.checked_sub rounded_budget phase) + +/-- [zerocopy::layout::tail_checks::trailing_arithmetic_check]: + Source: 'src/layout/tail_checks.rs', lines 88:0-111:1 -/ +def layout.tail_checks.trailing_arithmetic_check + (tail : layout.TrailingSliceLayout Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (elems : Std.Usize) (budget : Std.Usize) : + Result Unit := do let i ← core.num.nonzero.NonZero.get Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align - let mask ← i - 1#usize - let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize) - let i2 ← lift (~~~ i1) - ok (i2 &&& mask) + let b ← core.num.Usize.is_power_of_two i + if b + then + if phase < i + then + let o ← lift (Usize.checked_add i phase) + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + tail.size_rounding_align_and_phase._0 + let b1 ← layout.tail_checks.same_optional_usize o (some i1) + if b1 + then + let o1 ← layout.TrailingSliceLayoutUsize.size_for_elems tail elems + let o2 ← layout.tail_checks.reference_size tail align phase elems + let b2 ← layout.tail_checks.same_optional_usize o1 o2 + massert b2 + let o3 ← layout.TrailingSliceLayout.max_trailing_bytes tail budget + let o4 ← + layout.tail_checks.reference_capacity tail align phase budget + let b3 ← layout.tail_checks.same_optional_usize o3 o4 + massert b3 + else ok () + else ok () + else ok () /-- [zerocopy::util::checks::check_arithmetic]: Source: 'src/util/checks.rs', lines 38:0-46:1 -/ diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 267aabb722..565f2aaf74 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -100,13 +100,13 @@ structure byteorder.U32 (O : Type) where _1 : core.marker.PhantomData O /-- [zerocopy::layout::RoundingAlignAndPhase] - Source: 'src/layout/mod.rs', lines 84:0-84:54 -/ + Source: 'src/layout/mod.rs', lines 87:0-87:54 -/ structure layout.RoundingAlignAndPhase where _0 : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner /-- [zerocopy::layout::TrailingSliceLayout] - Source: 'src/layout/mod.rs', lines 191:0-245:1 -/ + Source: 'src/layout/mod.rs', lines 194:0-248:1 -/ structure layout.TrailingSliceLayout (E : Type) where offset : Std.Usize elem_size : E @@ -114,14 +114,14 @@ structure layout.TrailingSliceLayout (E : Type) where size_rounding_align_and_phase : layout.RoundingAlignAndPhase /-- [zerocopy::layout::SizeInfo] - Source: 'src/layout/mod.rs', lines 53:0-56:1 -/ + Source: 'src/layout/mod.rs', lines 56:0-59:1 -/ @[discriminant isize] inductive layout.SizeInfo (E : Type) where | Sized : Std.Usize → layout.SizeInfo E | SliceDst : layout.TrailingSliceLayout E → layout.SizeInfo E /-- [zerocopy::layout::DstLayout] - Source: 'src/layout/mod.rs', lines 40:0-48:1 + Source: 'src/layout/mod.rs', lines 43:0-51:1 Visibility: public -/ structure layout.DstLayout where align : core.num.nonzero.NonZero Std.Usize diff --git a/verification/aeneas/lean/Corollaries.lean b/verification/aeneas/lean/Corollaries.lean index edab313551..8adb0db7fd 100644 --- a/verification/aeneas/lean/Corollaries.lean +++ b/verification/aeneas/lean/Corollaries.lean @@ -14,14 +14,15 @@ import all Init.Data.Nat.Power2.Basic /-! A function contract is most useful when other proofs can consume it. These -corollaries compose the checked arithmetic operation lemmas into further -numeric consequences. They reuse the proved computation and discharge its -stated requirements, rather than proving a different calculation in its -place. +corollaries compose the checked operation lemmas into arithmetic consequences +and layout equivalence results. In particular, the recursive-size and direct +record-placement results connect runtime normalization to independent layout +mathematics for every metadata value in their stated domains. -The results remain conditional functional guarantees. They do not establish -pointer safety or prove that every Rust caller meets the contract's -requirements. +The bridge to an actual Rust type remains the explicit premise documented in +SEMANTICS.md. A proof about extracted numerical operations does not itself +prove pointer safety, nor does it prove that every Rust caller meets a +contract's requirements. -/ open Aeneas Aeneas.Std Aeneas.Std.Result namespace Zerocopy.Corollaries @@ -82,4 +83,50 @@ 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 +theorem size_matches_recursive (tail : layout.TrailingSliceLayout Usize) + (description : LayoutMath.Description) (n : Usize) + (hn : 0 < tail.size_rounding_align_and_phase._0.val.val) + (hd : description.valid) + (hr : trailingFormula tail = description.compile) : + layout.TrailingSliceLayoutUsize.size_for_elems tail n + ⦃ r => r.map UScalar.val = + if description.size n.val ≤ Usize.max then some (description.size n.val) else none ⦄ := by + step with Proofs.Raw.size_for_elems_spec tail n hn as ⟨r, hsize⟩ + rw [hr, LayoutMath.Formula.checkedSize, LayoutMath.compile_size description hd] at hsize + exact hsize + +theorem padding_matches_recursive (tail : layout.TrailingSliceLayout Usize) + (description : LayoutMath.Description) (n : Usize) + (hn : 0 < tail.size_rounding_align_and_phase._0.val.val) + (hd : description.valid) + (hr : trailingFormula tail = description.compile) + (hfit : description.size n.val ≤ Usize.max) : + layout.TrailingSliceLayoutUsize.padding_for_elems tail n + ⦃ p => p.val + description.offset + n.val * description.elem = description.size n.val ⦄ := by + step with Proofs.Raw.padding_for_elems_spec tail n hn as ⟨p, hp⟩ + have ho : tail.offset.val = description.offset := by + have h := congrArg LayoutMath.Formula.offset hr + simpa only [trailingFormula, byteFormula, LayoutMath.compile_offset] using h + have he : tail.elem_size.val = description.elem := by + have h := congrArg LayoutMath.Formula.elem hr + simpa only [trailingFormula, LayoutMath.compile_elem] using h + rw [ho, he, hr, LayoutMath.compile_size description hd] at hp + have hcontains := LayoutMath.description_contains_tail description n.val + let physical := description.offset + n.val * description.elem + let remaining := description.size n.val - physical + have hsum : remaining + physical = description.size n.val := by + dsimp only [remaining, physical] + omega + have hmod : Nat.ModEq (UScalar.size .Usize) (p.val + physical) (remaining + physical) := by + change (p.val + physical) % UScalar.size .Usize = + (remaining + physical) % UScalar.size .Usize + rw [hsum] + simpa only [physical, Nat.add_assoc, UScalar.size_UScalarTyUsize] using hp + have hcancel := Nat.ModEq.add_right_cancel' physical hmod + have hremaining : remaining ≤ Usize.max := by dsimp only [remaining]; omega + change p.val % UScalar.size .Usize = remaining % UScalar.size .Usize at hcancel + rw [Nat.mod_eq_of_lt (UScalar.hSize p), word_mod_of_le remaining hremaining] at hcancel + dsimp only [remaining, physical] at hcancel + omega + end Zerocopy.Corollaries diff --git a/verification/aeneas/lean/MathViews.lean b/verification/aeneas/lean/MathViews.lean index ff28890d68..99f754dc03 100644 --- a/verification/aeneas/lean/MathViews.lean +++ b/verification/aeneas/lean/MathViews.lean @@ -167,6 +167,17 @@ def layoutValid (self : layout.DstLayout) : Prop := (∃ value, layout.DstLayout.decode raw = some value) ↔ layoutValid raw := layout_valid_iff raw +-- Concrete contracts retain the automatic machine-word provider. Making its +-- carrier explicit avoids recovering a raw dictionary from the type-only Fields +-- family while preserving the generic admission theorem above. +@[contract_simps] theorem trailing_usize_admitted_iff + (raw : layout.TrailingSliceLayout Usize) : + (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize), + RustModel.decode raw = some value) ↔ + 0 < raw.size_rounding_align_and_phase._0.val.val := by + simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using + trailing_admitted_iff raw + @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) : Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff @@ -192,15 +203,6 @@ attribute [contract_simps] encodingValid trailingValid sizeInfoValid layoutValid -- A named decoder can also occur after a surrounding structural traversal -- exposes the retained dictionary. These are the same admission equivalences. -@[contract_simps] theorem trailing_usize_admitted_iff - (raw : layout.TrailingSliceLayout Usize) : - (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize), - RustModel.decode raw = some value) ↔ - 0 < raw.size_rounding_align_and_phase._0.val.val := by - simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using - trailing_admitted_iff raw - --- Optional traversal exposes the same fixed provider's named decoder directly. @[contract_simps] theorem trailing_usize_decoder_admitted_iff (raw : layout.TrailingSliceLayout Usize) : (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize), diff --git a/verification/aeneas/lean/ModelProjectionLaws.lean b/verification/aeneas/lean/ModelProjectionLaws.lean index 2e6cfb0b1f..0c97fd6b6d 100644 --- a/verification/aeneas/lean/ModelProjectionLaws.lean +++ b/verification/aeneas/lean/ModelProjectionLaws.lean @@ -71,4 +71,13 @@ 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 + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index c64720befa..a645741c05 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -126,6 +126,50 @@ def encoding_align_spec : Prop := ∀ (code : layout.RoundingAlignAndPhase), encoding_align_spec_contract code (layout.RoundingAlignAndPhase.align code) +def size_offset_spec_contract (E : Type) (t : layout.TrailingSliceLayout E) + (run : Result Usize) : Prop := + ∀ [RustModel E], trailingValid t → + ∃ offset, run = .ok offset ∧ + offset.val = t.size_base.val - t.size_base.val % (byteFormula t).align + (byteFormula t).phase + +def size_offset_spec : Prop := + ∀ (E : Type) (t : layout.TrailingSliceLayout E), + size_offset_spec_contract E t (layout.TrailingSliceLayout.size_offset t) + +def max_trailing_bytes_spec_contract + (E : Type) (t : layout.TrailingSliceLayout E) (budget : Usize) + (run : Result (Option Usize)) : Prop := + ∀ [RustModel E], + trailingValid t → + ∃ cap, run = .ok cap ∧ + cap.map UScalar.val = (byteFormula t).capacity budget.val + +def max_trailing_bytes_spec : Prop := + ∀ (E : Type) (t : layout.TrailingSliceLayout E) (budget : Usize), + max_trailing_bytes_spec_contract E t budget + (layout.TrailingSliceLayout.max_trailing_bytes t budget) + +def padding_for_elems_spec_contract (t : layout.TrailingSliceLayout Usize) (n : Usize) + (run : Result Usize) : Prop := + 0 < t.size_rounding_align_and_phase._0.val.val → + ∃ p, run = .ok p ∧ + (p.val + t.offset.val + n.val * t.elem_size.val) % UScalar.size .Usize = + (trailingFormula t).size n.val % UScalar.size .Usize + +def padding_for_elems_spec : Prop := + ∀ (t : layout.TrailingSliceLayout Usize) (n : Usize), + padding_for_elems_spec_contract t n (layout.TrailingSliceLayoutUsize.padding_for_elems t n) + +def size_for_elems_spec_contract (t : layout.TrailingSliceLayout Usize) (n : Usize) + (run : Result (Option Usize)) : Prop := + 0 < t.size_rounding_align_and_phase._0.val.val → + ∃ size, run = .ok size ∧ + size.map UScalar.val = (trailingFormula t).checkedSize Usize.max n.val + +def size_for_elems_spec : Prop := + ∀ (t : layout.TrailingSliceLayout Usize) (n : Usize), + size_for_elems_spec_contract t n (layout.TrailingSliceLayoutUsize.size_for_elems t n) + def try_nonzero_spec_contract (si : layout.SizeInfo Usize) (run : Result (Option (layout.SizeInfo NonZeroUsize))) : Prop := sizeInfoValid si → run ⦃ r => (∀ next ∈ r, sizeInfoValid next) ∧ diff --git a/verification/aeneas/lean/Obligations/TailChecks.lean b/verification/aeneas/lean/Obligations/TailChecks.lean new file mode 100644 index 0000000000..4fb4d750e6 --- /dev/null +++ b/verification/aeneas/lean/Obligations/TailChecks.lean @@ -0,0 +1,33 @@ +/- 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 +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations +open Zerocopy.Proofs +set_option linter.unusedVariables false + +/- These roots promise that every assertion terminates on the full admitted +Rust domain. Their observations are the executable assertions in tail_checks; +the original method obligations retain their separate mathematical promises. +-/ +def trailing_arithmetic_check_spec_contract + (tail : layout.TrailingSliceLayout Usize) (align : NonZeroUsize) + (phase elems budget : Usize) (run : Result Unit) : Prop := + 0 < tail.size_rounding_align_and_phase._0.val.val → 0 < align.val.val → + run ⦃ _ => True ⦄ + +def trailing_arithmetic_check_spec : Prop := + ∀ tail align phase elems budget, + trailing_arithmetic_check_spec_contract tail align phase elems budget + (layout.tail_checks.trailing_arithmetic_check tail align phase elems budget) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean index 0119cc2995..79cb66444e 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -14,6 +14,8 @@ public import Aeneas public import Loops public import LayoutModel public import RepresentationLaws +public import ModelProjectionLaws +public import Obligations public import LayoutMath import all Mathlib.Data.Nat.Log import all Init.Data.Nat.Power2.Basic @@ -36,7 +38,8 @@ implementation each time. Aeneas Result describes execution success, panic, or divergence. Rust Option and Rust Result values may themselves be successful payloads. The proof must -keep these cases distinct. +keep these cases distinct. Corollaries connects the operation results to the +independent recursive layout semantics under the explicit Rust premise. -/ open Aeneas Aeneas.Std namespace Zerocopy.Proofs.Raw @@ -205,6 +208,105 @@ theorem encoding_align_spec : step with encoding_components_spec self hn as ⟨a, p, _, _, _, ha, _⟩ simpa only [WP.spec_ok] using ha +/- Reading physical offset must preserve the raw word even though the element +carrier can be generic. No size normalization is needed for this observation. +-/ +theorem size_offset_spec : + ∀ {E : Type} (self : layout.TrailingSliceLayout E), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)), + @Zerocopy.layout.TrailingSliceLayout.size_offset E self ⦃ offset => + offset.val = self.size_base.val - self.size_base.val % (byteFormula self).align + (byteFormula self).phase ⦄ := by + intro E self hn + unfold layout.TrailingSliceLayout.size_offset + step with encoding_components_spec _ hn as ⟨a, p, ha, hp, hsum, halign, hphase⟩ + step with round_down_spec self.size_base a ha as ⟨base, _, hb, hmod, _, _⟩ + simp only [UScalar.val_or] + rw [LayoutMath.aligned_or _ _ _ ha hmod hp, hb] + simp only [byteFormula] + rw [← halign] + omega + +/- Solve the rounded complete-size inequality for the greatest byte budget. The +proof must preserve rounding plateaus and the case where even zero bytes do +not fit; dividing by element stride belongs to a later operation. +-/ +theorem max_trailing_bytes_spec : + ∀ {E : Type} (self : layout.TrailingSliceLayout E) (available_bytes : Usize), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)), + @Zerocopy.layout.TrailingSliceLayout.max_trailing_bytes E self available_bytes ⦃ r => r.map UScalar.val = (byteFormula self).capacity available_bytes.val ⦄ := by + intro E self available hn + unfold layout.TrailingSliceLayout.max_trailing_bytes + step with encoding_components_spec _ hn as ⟨a, p, ha, hp, hsum, halign, hphase⟩ + have apos := Nat.pos_of_isPowerOfTwo ha + have hview : byteFormula self = ⟨self.size_base.val, p.val, a.val.val, 0, self.offset.val⟩ := by + unfold byteFormula + dsimp only + rw [← hphase, ← halign] + let rp : Usize := if p = 0#usize then 0#usize else a.val + have hrp : rp.val = LayoutMath.roundUp p.val a.val.val := by + rw [LayoutMath.roundUp_phase _ _ apos hp] + by_cases hz : p = 0#usize + · simp only [rp, hz, if_true] + rfl + · have hzero : p.val ≠ 0 := by + intro h + exact hz (UScalar.eq_of_val_eq (by simpa using h)) + simp only [rp, hz, hzero, if_false] + have hrmod : rp.val % a.val.val = 0 := by rw [hrp]; exact (LayoutMath.roundUp_properties _ _ apos).2.2 + have hrge : p.val ≤ rp.val := by rw [hrp]; exact (LayoutMath.roundUp_properties _ _ apos).1 + have hrlt : rp.val - p.val < a.val.val := by + have := (LayoutMath.roundUp_properties p.val a.val.val apos).2.1 + omega + have hbranch : (if p = 0#usize then Result.ok 0#usize else + core.num.nonzero.NonZero.get Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a) = Result.ok rp := by + simp only [core.num.nonzero.NonZero.get] + by_cases h : p = 0#usize <;> simp only [h, if_true, if_false, rp] + rw [hbranch] + simp only [bind_ok] + step as ⟨checked, hadd⟩ + cases checked with + | none => + simp only [] at hadd + have hav : available.val ≤ Usize.max := by scalar_tac + have hmiss : ¬(byteFormula self).bytes 0 ≤ available.val := by + rw [hview] + simp only [LayoutMath.Formula.bytes, Nat.add_zero, ← hrp] + omega + simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.capacity, hmiss, if_false] + | some minimum => + simp only [] at hadd + step as ⟨checked, hsub⟩ + cases checked with + | none => + simp only [] at hsub + simp only [] + have hmiss : ¬(byteFormula self).bytes 0 ≤ available.val := by + rw [hview] + simp only [LayoutMath.Formula.bytes, Nat.add_zero, ← hrp] + omega + simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.capacity, hmiss, if_false] + | some extra => + simp only [] at hsub + simp only [] + step with round_down_spec extra a ha as ⟨aligned, hle, hal, hmod, _, _⟩ + step with Usize.sub_spec hrge as ⟨padding, hpadding, _⟩ + have hfit : (byteFormula self).bytes 0 ≤ available.val := by + rw [hview] + simp only [LayoutMath.Formula.bytes, Nat.add_zero, ← hrp] + omega + simp only [lift, bind_ok, WP.spec_ok, Option.map_some, + LayoutMath.Formula.capacity, hfit, if_true] + have hpl : padding.val < a.val.val := by + dsimp only [rp] at hrlt + omega + rw [UScalar.val_or, LayoutMath.aligned_or _ _ _ ha hmod hpl] + rw [hview] + dsimp only + have hbudget : available.val - self.size_base.val = rp.val + extra.val := by omega + rw [hbudget, LayoutMath.floor_shift _ _ _ hrmod] + congr 1 + have hrem := Nat.mod_le extra.val a.val.val + dsimp only [rp] at * + omega + theorem assume_shallow_unpadded_spec : ∀ (self : layout.DstLayout), @Zerocopy.layout.DstLayout.assume_shallow_unpadded self ⦃ r => r.align = self.align ∧ r.size_info = self.size_info ∧ r.statically_shallow_unpadded = true ⦄ := by @@ -302,6 +404,138 @@ theorem requires_static_padding_spec : simp only [layout.DstLayout.requires_static_padding, WP.spec_ok] cases self.statically_shallow_unpadded <;> rfl +theorem wrapping_sub_cancel (x y : Usize) : + ((core.num.Usize.wrapping_sub x y).val + y.val) % UScalar.size .Usize = x.val := by + rw [core.num.Usize.wrapping_sub_val_eq, Nat.mod_add_mod] + have hy := UScalar.hSize y + rw [show x.val + (UScalar.size .Usize - y.val) + y.val = + x.val + UScalar.size .Usize by omega, Nat.add_mod_right] + exact Nat.mod_eq_of_lt (UScalar.hSize x) + +/- Compute padding with wrapping machine arithmetic. The raw theorem records the +modular result; physical padding follows only when the complete size fits. +-/ +theorem padding_for_elems_spec : + ∀ (self : layout.TrailingSliceLayout Usize) (elems : Usize), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)), + @Zerocopy.layout.TrailingSliceLayoutUsize.padding_for_elems self elems ⦃ p => (p.val + self.offset.val + elems.val * self.elem_size.val) % UScalar.size .Usize = + (trailingFormula self).size elems.val % UScalar.size .Usize ⦄ := by + intro self elems hn + unfold layout.TrailingSliceLayoutUsize.padding_for_elems + step with encoding_components_spec _ hn as ⟨a, r, ha, hr, hsum, halign, hphase⟩ + simp only [core.num.nonzero.NonZero.get, bind_ok] + have apos := Nat.pos_of_isPowerOfTwo ha + step with Usize.sub_spec (show (1#usize).val ≤ a.val.val by simpa using (show 1 ≤ a.val.val by omega)) as ⟨mask, hm, _⟩ + simp only [lift, bind_ok] + have low (x : Usize) : (x &&& mask).val = x.val % a.val.val := by + obtain ⟨k, hk⟩ := ha + rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod] + let t := core.num.Usize.wrapping_mul elems (self.elem_size &&& mask) &&& mask + have ht : t.val = (elems.val * self.elem_size.val) % a.val.val := by + rw [low, core.num.Usize.wrapping_mul_val_eq, low, + Nat.mod_mod_of_dvd _ (Arithmetic.alignment_dvd_size a.val ha)] + rw [Nat.mul_mod, Nat.mod_mod, ← Nat.mul_mod] + let input := core.num.Usize.wrapping_add r t + have hi : input.val % a.val.val = + (r.val + elems.val * self.elem_size.val) % a.val.val := by + rw [core.num.Usize.wrapping_add_val_eq, + Nat.mod_mod_of_dvd _ (Arithmetic.alignment_dvd_size a.val ha), ht, Nat.add_mod_mod] + step with Zerocopy.Proofs.Raw.padding_lt_alignment input a ha as ⟨rp, _, hp, _, _, _⟩ + have hp' : rp.val = (a.val.val - (r.val + elems.val * self.elem_size.val) % a.val.val) % a.val.val := by + rw [hi] at hp + exact hp + simp only [core.num.Usize.wrapping_add_val_eq, Nat.add_assoc, Nat.mod_add_mod] + rw [show + (core.num.Usize.wrapping_sub (core.num.Usize.wrapping_add self.size_base r) self.offset).val + + (rp.val + (self.offset.val + elems.val * self.elem_size.val)) = + ((core.num.Usize.wrapping_sub (core.num.Usize.wrapping_add self.size_base r) self.offset).val + + self.offset.val) + (elems.val * self.elem_size.val + rp.val) by omega, + ← Nat.mod_add_mod, wrapping_sub_cancel, core.num.Usize.wrapping_add_val_eq, Nat.mod_add_mod] + simp only [trailingFormula, byteFormula, LayoutMath.Formula.size, LayoutMath.Formula.bytes, + LayoutMath.roundUp] + rw [← hphase, ← halign, hp'] + congr 1 + omega + +theorem trailing_align_pos (self : layout.TrailingSliceLayout Usize) : + 0 < (trailingFormula self).align := Nat.two_pow_pos _ + +theorem trailing_product_le_size (self : layout.TrailingSliceLayout Usize) (n : Nat) : + n * self.elem_size.val ≤ (trailingFormula self).size n := by + have h := (LayoutMath.roundUp_properties + ((trailingFormula self).phase + n * self.elem_size.val) + (trailingFormula self).align (trailing_align_pos self)).1 + unfold trailingFormula byteFormula LayoutMath.Formula.size LayoutMath.Formula.bytes at * + dsimp only at * + omega + +theorem word_mod_of_le (n : Nat) (h : n ≤ Usize.max) : n % UScalar.size .Usize = n := by + apply Nat.mod_eq_of_lt + have hp := Nat.two_pow_pos System.Platform.numBits + simp only [Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq, UScalar.size] at h ⊢ + omega + +/- Distinguish a successful checked size from overflow using the unbounded +complete-size formula. Rust None is a successful payload, not a panic. +-/ +theorem size_for_elems_spec : + ∀ (self : layout.TrailingSliceLayout Usize) (elems : Usize), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)), + @Zerocopy.layout.TrailingSliceLayoutUsize.size_for_elems self elems ⦃ r => r.map UScalar.val = (trailingFormula self).checkedSize Usize.max elems.val ⦄ := by + intro self elems hn + unfold layout.TrailingSliceLayoutUsize.size_for_elems + step with max_trailing_bytes_spec self core.num.Usize.MAX hn as ⟨cap, hc⟩ + have hc' := LayoutMath.capacity_spec (byteFormula self) core.num.Usize.MAX.val + (show 0 < (byteFormula self).align from Nat.two_pow_pos _) + simp only [core.num.Usize.MAX, UScalar.ofNatCore_val_eq] at hc' + have hprod := trailing_product_le_size self elems.val + cases cap with + | none => + simp only [Option.map_none] at hc + rw [← hc] at hc' + have hmiss := hc' (elems.val * self.elem_size.val) + change Usize.max < (trailingFormula self).size elems.val at hmiss + simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.checkedSize, + show ¬(trailingFormula self).size elems.val ≤ Usize.max by omega, if_false] + | some cap => + simp only [Option.map_some] at hc + rw [← hc] at hc' + have hiff := hc' (elems.val * self.elem_size.val) + change (trailingFormula self).size elems.val ≤ Usize.max ↔ + elems.val * self.elem_size.val ≤ cap.val at hiff + step as ⟨product, hm⟩ + cases product with + | none => + simp only [] at hm + have hmiss : ¬(trailingFormula self).size elems.val ≤ Usize.max := by + rw [Nat.mul_comm] at hm + omega + simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.checkedSize, hmiss, if_false] + | some bytes => + simp only [] at hm + simp only [UScalar.lt_equiv] + split + · rename_i hbig + have hmiss : ¬(trailingFormula self).size elems.val ≤ Usize.max := by + rw [Nat.mul_comm] at hm + omega + simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.checkedSize, hmiss, if_false] + · rename_i hsmall + have hfit : (trailingFormula self).size elems.val ≤ Usize.max := by + apply hiff.mpr + rw [hm.2.1, Nat.mul_comm] at hsmall + omega + simp only [lift, bind_ok] + step with padding_for_elems_spec self elems hn as ⟨p, hp⟩ + have hsz : Usize.size = UScalar.size .Usize := by + simp only [Usize.size, Usize.numBits, UScalarTy.Usize_numBits_eq, UScalar.size] + rw [hsz] at hp + simp only [Option.map_some, + LayoutMath.Formula.checkedSize, hfit, if_true, + core.num.Usize.wrapping_add_val_eq, Nat.mod_add_mod] + rw [hm.2.1, Nat.mul_comm] + rw [show self.offset.val + elems.val * self.elem_size.val + p.val = + p.val + self.offset.val + elems.val * self.elem_size.val by omega, + hp, word_mod_of_le _ hfit] + /- Explain both zero-stride rejection and successful conversion. The raw lemma retains broad representation coverage; the canonical spec adds recursive admission rather than silently changing that useful raw theorem. @@ -415,6 +649,60 @@ theorem encoding_align_spec : Zerocopy.Specs.encoding_align_spec := by exact ⟨av, (decodeNonZeroUScalar_iff align av).mpr rfl, he.trans hvalue.1.symm⟩ register_spec_step encoding_align_spec +/- Reading physical offset must preserve the raw word even though the element +carrier can be generic. No size normalization is needed for this observation. +-/ +theorem size_offset_spec : Zerocopy.Specs.size_offset_spec := by + unfold Zerocopy.Specs.size_offset_spec + representation_simps + intro E self validity hv + exact Raw.size_offset_spec self hv.2 +register_spec_step size_offset_spec + +/- Solve the rounded complete-size inequality for the greatest byte budget. The +proof must preserve rounding plateaus and the case where even zero bytes do +not fit; dividing by element stride belongs to a later operation. +-/ +theorem max_trailing_bytes_spec : Zerocopy.Specs.max_trailing_bytes_spec := by + unfold Zerocopy.Specs.max_trailing_bytes_spec + representation_simps + intro E self available validity hv + apply WP.spec_mono (Raw.max_trailing_bytes_spec self available hv.2) + intro result facts + refine ⟨?_, facts⟩ + change isValid result + simp +register_spec_step max_trailing_bytes_spec + +/- Compute padding with wrapping machine arithmetic. The raw theorem records the +modular result; physical padding follows only when the complete size fits. +-/ +theorem padding_for_elems_spec : Zerocopy.Specs.padding_for_elems_spec := by + unfold Zerocopy.Specs.padding_for_elems_spec + representation_simps + intro self elems hv + exact Raw.padding_for_elems_spec self elems hv +register_spec_step padding_for_elems_spec + +/- Distinguish a successful checked size from overflow using the unbounded +complete-size formula. Rust None is a successful payload, not a panic. +-/ +theorem size_for_elems_spec : Zerocopy.Specs.size_for_elems_spec := by + intro self elems value hvalue count hcount + have hv : 0 < self.size_rounding_align_and_phase._0.val.val := + by simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using + (trailing_decoder_admitted_iff self).mp ⟨value, hvalue⟩ + have hformula := trailingFormula_decode self value hvalue + have hn := (decodeUScalar_iff elems count).mp hcount + apply WP.spec_mono (Raw.size_for_elems_spec self elems hv) + intro result facts + obtain ⟨decoded, hd⟩ := (option_valid_iff result).mpr (by simp) + refine ⟨decoded, hd, ?_⟩ + change decoded.map (fun size => (size : Nat)) = _ + rw [optionalSize_decode result decoded hd, hformula, ← hn] + exact facts +register_spec_step size_for_elems_spec + theorem max_elems_for_bytes_spec : Zerocopy.Specs.max_elems_for_bytes_spec := by unfold Zerocopy.Specs.max_elems_for_bytes_spec representation_simps @@ -547,4 +835,22 @@ theorem new_zst_spec : Zerocopy.Specs.new_zst_spec := by | some a => simpa only [Option.getD_some, and_true] using Nat.pos_of_isPowerOfTwo (hp a rfl) register_spec_step new_zst_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 + (self : layout.TrailingSliceLayout Usize) (elems : Usize) (run : Result (Option Usize)) + (provided : Zerocopy.Specs.size_for_elems_spec_contract self elems run) : + Zerocopy.Obligations.size_for_elems_spec_contract self elems run := by + intro positive + have valid : trailingValid self := ⟨by simp, positive⟩ + obtain ⟨value, hvalue⟩ := (trailing_decoder_admitted_iff self).mpr valid + have hformula := trailingFormula_decode self value hvalue + have execution := provided value hvalue (unsignedWord elems) rfl + simp only [WP.spec_equiv_exists] at execution + obtain ⟨result, hexec, decoded, hd, hsize⟩ := execution + refine ⟨result, hexec, ?_⟩ + change decoded.map (fun size => (size : Nat)) = _ at hsize + rw [optionalSize_decode result decoded hd, hformula, unsignedWord_value] at hsize + exact hsize + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/TailChecks.lean b/verification/aeneas/lean/Proofs/TailChecks.lean new file mode 100644 index 0000000000..2323571ddc --- /dev/null +++ b/verification/aeneas/lean/Proofs/TailChecks.lean @@ -0,0 +1,83 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Proofs +public import Proofs.TailReference +public import RequiredModelContracts.TailChecks +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw.TailChecks +set_option linter.unusedVariables false +set_option linter.unusedSimpArgs false + +/- The roots execute the production operation and the separate reference, +then prove the actual Rust assertion. The reference lemmas retain their own +arithmetic derivations; neither side is substituted for an extracted body. +-/ +theorem trailing_arithmetic_check (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase elems budget : Usize) : + layout.tail_checks.trailing_arithmetic_check tail align phase elems budget ⦃ _ => True ⦄ := by + unfold layout.tail_checks.trailing_arithmetic_check + simp only [core.num.nonzero.NonZero.get, bind_ok] + step as ⟨power, power_iff⟩ + split + · rename_i power_true + have power_fact : align.val.val.isPowerOfTwo := Eq.mp power_iff power_true + have align_positive := Nat.pos_of_isPowerOfTwo power_fact + simp only [UScalar.lt_equiv] + split + · rename_i phase_lt + step as ⟨encoded, encoded_facts⟩ + step with same_optional_usize encoded (some tail.size_rounding_align_and_phase._0.val) + as ⟨code_matches, matches_iff⟩ + split + · rename_i matches_true + have encoded_eq := matches_iff.mp matches_true + rw [encoded_eq] at encoded_facts + simp only [] at encoded_facts + have encoding : tail.size_rounding_align_and_phase._0.val.val = align.val.val + phase.val := + encoded_facts.2.1 + have positive : 0 < tail.size_rounding_align_and_phase._0.val.val := by omega + have formula_eq := witness_view tail align phase power_fact phase_lt encoding + step with Zerocopy.Proofs.Raw.size_for_elems_spec tail elems positive as ⟨actual_size, actual_size_value⟩ + step with reference_size tail align phase elems align_positive as ⟨expected_size, expected_size_value⟩ + rw [formula_eq] at actual_size_value + have size_same : actual_size = expected_size := optional_value_injective + (actual_size_value.trans expected_size_value.symm) + step with same_optional_usize actual_size expected_size as ⟨same_size, same_size_iff⟩ + have size_true := same_size_iff.mpr size_same + simp only [massert, size_true, if_true, bind_ok] + step with Zerocopy.Proofs.Raw.max_trailing_bytes_spec tail budget positive as ⟨actual_capacity, actual_capacity_value⟩ + step with reference_capacity tail align phase budget align_positive as ⟨expected_capacity, expected_capacity_value⟩ + have byte_capacity : (byteFormula tail).capacity budget.val = + (trailingFormula tail).capacity budget.val := rfl + rw [byte_capacity, formula_eq] at actual_capacity_value + have capacity_same : actual_capacity = expected_capacity := optional_value_injective + (actual_capacity_value.trans expected_capacity_value.symm) + step with same_optional_usize actual_capacity expected_capacity as ⟨same_capacity, same_capacity_iff⟩ + have capacity_true := same_capacity_iff.mpr capacity_same + simp [massert, capacity_true, WP.spec_ok] + · simp only [WP.spec_ok] + · simp only [WP.spec_ok] + · simp only [WP.spec_ok] + +end Zerocopy.Proofs.Raw.TailChecks + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem trailing_arithmetic_check_spec : Specs.trailing_arithmetic_check_spec := by + unfold Specs.trailing_arithmetic_check_spec + intros + apply WP.spec_mono (Raw.TailChecks.trailing_arithmetic_check _ _ _ _ _) + intro result facts + exact ⟨(), rfl, trivial⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/TailReference.lean b/verification/aeneas/lean/Proofs/TailReference.lean new file mode 100644 index 0000000000..6357054a1c --- /dev/null +++ b/verification/aeneas/lean/Proofs/TailReference.lean @@ -0,0 +1,237 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import LayoutModel +public import RepresentationLaws +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw.TailChecks +set_option linter.unusedVariables false +set_option linter.unusedSimpArgs false + +def witnessFormula (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase : Usize) : LayoutMath.Formula := + ⟨tail.size_base.val, phase.val, align.val.val, tail.elem_size.val, tail.offset.val⟩ + +def checkedNat (n : Nat) : Option Nat := if n ≤ Usize.max then some n else none + +@[simp] theorem checkedNat_none (n : Nat) : checkedNat n = none ↔ Usize.max < n := by + simp [checkedNat] + +@[simp] theorem checkedNat_some (n value : Nat) : + checkedNat n = some value ↔ n ≤ Usize.max ∧ n = value := by + unfold checkedNat + split <;> simp_all + +theorem checked_add_value (x y : Usize) : + (Usize.checked_add x y).map UScalar.val = checkedNat (x.val + y.val) := by + have h := Usize.checked_add_bv_spec x y + cases output_eq : Usize.checked_add x y with + | none => + simp only [output_eq] at h ⊢ + simp [checkedNat, show ¬x.val + y.val ≤ Usize.max by omega] + | some result => + simp only [output_eq] at h ⊢ + simp [checkedNat, h.1, h.2.1] + +theorem checked_mul_value (x y : Usize) : + (Usize.checked_mul x y).map UScalar.val = checkedNat (x.val * y.val) := by + have h := Usize.checked_mul_bv_spec x y + cases output_eq : Usize.checked_mul x y with + | none => + simp only [output_eq] at h ⊢ + simp [checkedNat, show ¬x.val * y.val ≤ Usize.max by omega] + | some result => + simp only [output_eq] at h ⊢ + simp [checkedNat, h.1, h.2.1] + +theorem same_optional_usize (left right : Option Usize) : + layout.tail_checks.same_optional_usize left right ⦃ b => (b = true ↔ left = right) ⦄ := by + cases left <;> cases right <;> + simp [layout.tail_checks.same_optional_usize, WP.spec_ok] + +theorem optional_value_injective {left right : Option Usize} + (same : left.map UScalar.val = right.map UScalar.val) : left = right := by + cases left with + | none => + cases right with + | none => rfl + | some right => cases same + | some left => + cases right with + | none => cases same + | some right => + congr 1 + exact UScalar.eq_of_val_eq (Option.some.inj same) + +/- This is coverage of the Rust witness guard, rather than an additional +restriction on the compressed representation. Every positive stored word +decodes to a power of two and a phase below it. +-/ +theorem encoding_witness_coverage (tail : layout.TrailingSliceLayout Usize) + (positive : 0 < tail.size_rounding_align_and_phase._0.val.val) : + ∃ a p : Nat, a.isPowerOfTwo ∧ p < a ∧ + a + p = tail.size_rounding_align_and_phase._0.val.val := by + obtain ⟨value, decoded⟩ := rounding_decode_positive tail.size_rounding_align_and_phase positive + have h := (rounding_decode_iff tail.size_rounding_align_and_phase value).mp decoded + exact ⟨value.align, value.phase, value.align_pow2, value.phase_lt, h.symm⟩ + +theorem witness_view (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase : Usize) (power : align.val.val.isPowerOfTwo) + (phase_lt : phase.val < align.val.val) + (encoding : tail.size_rounding_align_and_phase._0.val.val = align.val.val + phase.val) : + trailingFormula tail = witnessFormula tail align phase := by + let value : layout.RoundingAlignAndPhase.RoundingValue := + { align := align.val.val, phase := phase.val, align_pow2 := power, + phase_lt := phase_lt, fits := by rw [← encoding]; scalar_tac } + have decoded := (rounding_decode_iff tail.size_rounding_align_and_phase value).mpr encoding + have components := rounding_decode_components tail.size_rounding_align_and_phase value decoded + simp only [value] at components + rw [encoding] at components + simp only [trailingFormula, byteFormula, witnessFormula, ← components.1, + encoding, Nat.add_sub_cancel_left] + +def witnessMatches (runtime_layout : layout.DstLayout) + (align : NonZeroUsize) (phase : Usize) : Prop := + match runtime_layout.size_info with + | .Sized _ => True + | .SliceDst tail => align.val.val.isPowerOfTwo ∧ phase.val < align.val.val ∧ + tail.size_rounding_align_and_phase._0.val.val = align.val.val + phase.val + +theorem reference_round_up (bytes : Usize) (align : NonZeroUsize) + (positive : 0 < align.val.val) : + layout.tail_checks.reference_round_up bytes align ⦃ result => + result.map UScalar.val = checkedNat (LayoutMath.roundUp bytes.val align.val.val) ⦄ := by + unfold layout.tail_checks.reference_round_up + simp only [core.num.nonzero.NonZero.get, bind_ok] + step with Usize.rem_spec bytes (y := align.val) (by omega) as ⟨remainder, remainder_value⟩ + have remainder_lt := Nat.mod_lt bytes.val positive + simp only [UScalar.eq_equiv, UScalar.ofNatCore_val_eq] + split + · rename_i zero + have rounded : LayoutMath.roundUp bytes.val align.val.val = bytes.val := by + apply LayoutMath.roundUp_eq + omega + simp only [bind_ok, WP.spec_ok] + rw [checked_add_value, rounded, UScalar.ofNatCore_val_eq, Nat.add_zero] + · rename_i nonzero + step with Usize.sub_spec (x := align.val) (y := remainder) (by omega) as ⟨padding, padding_value⟩ + rw [checked_add_value] + congr 1 + unfold LayoutMath.roundUp + have padding_lt : align.val.val - bytes.val % align.val.val < align.val.val := by omega + rw [Nat.mod_eq_of_lt padding_lt] + omega + +theorem reference_size (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase elems : Usize) (positive : 0 < align.val.val) : + layout.tail_checks.reference_size tail align phase elems ⦃ result => + result.map UScalar.val = (witnessFormula tail align phase).checkedSize Usize.max elems.val ⦄ := by + let f := witnessFormula tail align phase + have lower := (LayoutMath.roundUp_properties + (phase.val + elems.val * tail.elem_size.val) align.val.val positive).1 + have size_eq : f.size elems.val = tail.size_base.val + + LayoutMath.roundUp (phase.val + elems.val * tail.elem_size.val) align.val.val := rfl + unfold layout.tail_checks.reference_size + step as ⟨product, product_facts⟩ + cases product with + | none => + simp only [] at product_facts + have overflow : Usize.max < f.size elems.val := by omega + simp [LayoutMath.Formula.checkedSize, ← size_eq, f, overflow, Nat.not_le.mpr overflow] + | some bytes => + simp only [] at product_facts + step as ⟨input, input_facts⟩ + cases input with + | none => + simp only [] at input_facts + have overflow : Usize.max < f.size elems.val := by omega + simp [LayoutMath.Formula.checkedSize, ← size_eq, f, overflow, Nat.not_le.mpr overflow] + | some input => + simp only [] at input_facts + step with reference_round_up input align positive as ⟨rounded, rounded_facts⟩ + have input_value : input.val = phase.val + elems.val * tail.elem_size.val := by omega + rw [input_value] at rounded_facts + cases rounded with + | none => + simp only [Option.map_none] at rounded_facts + have overflow_round := (checkedNat_none _).mp rounded_facts.symm + have overflow : Usize.max < f.size elems.val := by omega + simp [LayoutMath.Formula.checkedSize, ← size_eq, f, Nat.not_le.mpr overflow] + | some rounded => + simp only [Option.map_some] at rounded_facts + have rounded_value := (checkedNat_some _ _).mp rounded_facts.symm + simp only [WP.spec_ok] + rw [checked_add_value] + change checkedNat _ = _ + rw [← rounded_value.2] + rfl + +theorem capacity_condition (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase budget : Usize) (positive : 0 < align.val.val) : + (witnessFormula tail align phase).bytes 0 ≤ budget.val ↔ + tail.size_base.val ≤ budget.val ∧ + phase.val ≤ (budget.val - tail.size_base.val) - + (budget.val - tail.size_base.val) % align.val.val := by + have nonnegative := (LayoutMath.roundUp_properties phase.val align.val.val positive).1 + have round_condition := LayoutMath.roundUp_le_budget phase.val align.val.val + (budget.val - tail.size_base.val) positive + change tail.size_base.val + LayoutMath.roundUp (phase.val + 0) align.val.val ≤ _ ↔ _ + rw [Nat.add_zero] + constructor + · intro fit + exact ⟨by omega, round_condition.mp (by omega)⟩ + · rintro ⟨base_fits, phase_fits⟩ + have := round_condition.mpr phase_fits + omega + +theorem reference_capacity (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase budget : Usize) (positive : 0 < align.val.val) : + layout.tail_checks.reference_capacity tail align phase budget ⦃ result => + result.map UScalar.val = (witnessFormula tail align phase).capacity budget.val ⦄ := by + have condition := capacity_condition tail align phase budget positive + unfold layout.tail_checks.reference_capacity + step as ⟨after_base, base_facts⟩ + cases after_base with + | none => + simp only [] at base_facts + have miss : ¬(witnessFormula tail align phase).bytes 0 ≤ budget.val := by + intro fit + have := condition.mp fit + omega + simp [LayoutMath.Formula.capacity, miss] + | some after_base => + simp only [] at base_facts + simp only [core.num.nonzero.NonZero.get, bind_ok] + step with Usize.rem_spec after_base (y := align.val) (by omega) as ⟨remainder, remainder_value⟩ + have remainder_bound := Nat.mod_le after_base.val align.val.val + step with Usize.sub_spec (x := after_base) (y := remainder) (by omega) as ⟨rounded, rounded_value⟩ + have rounded_budget : rounded.val = (budget.val - tail.size_base.val) - + (budget.val - tail.size_base.val) % align.val.val := by + rw [rounded_value, remainder_value, base_facts.2.1] + have phase_facts := Usize.checked_sub_bv_spec rounded phase + cases result_eq : Usize.checked_sub rounded phase with + | none => + simp only [result_eq] at phase_facts + have miss : ¬(witnessFormula tail align phase).bytes 0 ≤ budget.val := by + intro fit + have := condition.mp fit + omega + simp [result_eq, LayoutMath.Formula.capacity, miss] + | some result => + simp only [result_eq] at phase_facts + have fit : (witnessFormula tail align phase).bytes 0 ≤ budget.val := + condition.mpr ⟨base_facts.1, by omega⟩ + simp only [result_eq, WP.spec_ok, Option.map_some, LayoutMath.Formula.capacity, fit, if_true] + dsimp only [witnessFormula] + congr 1 + omega + +end Zerocopy.Proofs.Raw.TailChecks diff --git a/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean b/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean new file mode 100644 index 0000000000..bbe3d294a6 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean @@ -0,0 +1,36 @@ +/- 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 Specs +public import Obligations.TailChecks +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs +set_option linter.unusedVariables false + +/- Recover the full raw domain from the actual decoders before consuming the +supplied arbitrary-outcome contract. These adapters do not run either check. +-/ +@[contract_simps] theorem required_trailing_arithmetic_check + (tail : layout.TrailingSliceLayout Usize) (align : NonZeroUsize) + (phase elems budget : Usize) (run : Result Unit) + (provided : Specs.trailing_arithmetic_check_spec_contract tail align phase elems budget run) : + Obligations.trailing_arithmetic_check_spec_contract tail align phase elems budget run := by + intro positive align_positive + have valid_tail : isValid tail := (trailing_valid_iff tail).mpr ⟨by simp, positive⟩ + obtain ⟨tail_value, decoded_tail⟩ := valid_tail + let av : NonZeroUsizeValue := ⟨unsignedWord align.val, align_positive⟩ + have decoded_align := (decodeNonZeroUScalar_iff align av).mpr rfl + apply WP.spec_mono (provided tail_value decoded_tail av decoded_align + (unsignedWord phase) rfl (unsignedWord elems) rfl (unsignedWord budget) rfl) + rintro result ⟨value, decoded, facts⟩ + trivial + +end Zerocopy.Proofs diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index 7da300d273..ce7a76ce7c 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -15,6 +15,9 @@ mod nested_reference; #[allow(dead_code)] mod primitive_checks; +#[allow(dead_code)] +mod tail_checks; + use core::{mem, num::NonZeroUsize}; use crate::util; @@ -256,6 +259,12 @@ impl TrailingSliceLayout { let (align, phase) = self.size_rounding_align_and_phase.components(); offset == util::round_down_to_next_multiple_of_alignment(self.size_base, align) + phase }))] + /// + /// ```aeneas + /// spec size_offset_spec + /// ensures(raw) offset => + /// offset.val = self.size_base.val - self.size_base.val % (byteFormula self).align + (byteFormula self).phase + /// ``` const fn size_offset(&self) -> usize { #[cfg(kani)] #[kani::proof_for_contract(TrailingSliceLayout::::size_offset)] @@ -287,6 +296,11 @@ impl TrailingSliceLayout { .map(|bytes| util::round_down_to_next_multiple_of_alignment(bytes, align)) .and_then(|rounded| rounded.checked_sub(phase)) }))] + /// + /// ```aeneas + /// spec max_trailing_bytes_spec + /// ensures(raw) r => r.map UScalar.val = (byteFormula self).capacity available_bytes.val + /// ``` const fn max_trailing_bytes(&self, available_bytes: usize) -> Option { #[cfg(kani)] #[kani::proof_for_contract(TrailingSliceLayout::::max_trailing_bytes)] @@ -395,6 +409,12 @@ impl TrailingSliceLayout { let object_size = self.size_base.wrapping_add(rounded); padding == object_size.wrapping_sub(self.offset.wrapping_add(trailing_bytes)) }))] + /// + /// ```aeneas + /// spec padding_for_elems_spec + /// ensures(raw) p => (p.val + self.offset.val + elems.val * self.elem_size.val) % UScalar.size .Usize = + /// (trailingFormula self).size elems.val % UScalar.size .Usize + /// ``` pub(crate) const fn padding_for_elems(self, elems: usize) -> usize { #[cfg(kani)] #[kani::proof_for_contract(TrailingSliceLayout::padding_for_elems)] @@ -462,6 +482,12 @@ impl TrailingSliceLayout { size == elems.checked_mul(self.elem_size) .and_then(|bytes| proofs::slice_dst_size_for_trailing_bytes(self, bytes)) }))] + /// + /// ```aeneas + /// spec size_for_elems_spec + /// ensures result => result.map (fun size => (size : Nat)) = + /// (ModelViews.trailingFormula self).checkedSize Usize.max (elems : Nat) + /// ``` pub(crate) const fn size_for_elems(self, elems: usize) -> Option { #[cfg(kani)] #[kani::proof_for_contract(TrailingSliceLayout::size_for_elems)] diff --git a/zerocopy/src/layout/tail_checks.rs b/zerocopy/src/layout/tail_checks.rs new file mode 100644 index 0000000000..9706950641 --- /dev/null +++ b/zerocopy/src/layout/tail_checks.rs @@ -0,0 +1,111 @@ +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// Copyright 2026 The Fuchsia Authors +// +// Licensed under the 2-Clause BSD License , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +//! Executable assertions for trailing sizes, capacities, and cast metadata. +//! +//! The reference calculations receive an explicit alignment and phase. They +//! use division remainders and checked arithmetic, and never decode the +//! production rounding representation or call production size helpers. The +//! checks bind these independent witnesses to the stored word before comparing +//! results. Every nonzero stored word has such witnesses: its highest set bit +//! is the alignment, and the lower bits are the phase. + +// Explicit scalar reads and matches keep the reference independent of extra +// trait dictionaries and higher-order library models in the pinned extraction. +#![allow(clippy::needless_nonzero_get, clippy::manual_map)] + +use core::num::NonZeroUsize; + +use super::TrailingSliceLayout; + +pub(super) fn same_optional_usize(left: Option, right: Option) -> bool { + match (left, right) { + (Some(left), Some(right)) => left == right, + (None, None) => true, + _ => false, + } +} + +#[allow(clippy::arithmetic_side_effects)] +fn reference_round_up(bytes: usize, align: NonZeroUsize) -> Option { + let remainder = bytes % align.get(); + let padding = if remainder == 0 { 0 } else { align.get() - remainder }; + bytes.checked_add(padding) +} + +pub(super) fn reference_size( + tail: TrailingSliceLayout, + align: NonZeroUsize, + phase: usize, + elems: usize, +) -> Option { + match elems.checked_mul(tail.elem_size) { + None => None, + Some(bytes) => match phase.checked_add(bytes) { + None => None, + Some(input) => match reference_round_up(input, align) { + None => None, + Some(rounded) => tail.size_base.checked_add(rounded), + }, + }, + } +} + +#[allow(clippy::arithmetic_side_effects)] +fn reference_capacity( + tail: TrailingSliceLayout, + align: NonZeroUsize, + phase: usize, + budget: usize, +) -> Option { + match budget.checked_sub(tail.size_base) { + None => None, + Some(after_base) => { + let rounded_budget = after_base - after_base % align.get(); + rounded_budget.checked_sub(phase) + } + } +} + +/// Check the entire optional size and capacity results, including overflow. +/// +/// Physical slice offset does not constrain this claim: a raw layout can have +/// its slice outside the complete object. Nor is rounding alignment restricted +/// to Rust's maximum type alignment; every nonzero encoding is covered. +/// +/// ```aeneas +/// spec trailing_arithmetic_check_spec +/// ensures(raw) _ => True +/// ``` +fn trailing_arithmetic_check( + tail: TrailingSliceLayout, + align: NonZeroUsize, + phase: usize, + elems: usize, + budget: usize, +) { + if align.get().is_power_of_two() + && phase < align.get() + && same_optional_usize( + align.get().checked_add(phase), + Some(tail.size_rounding_align_and_phase.0.get()), + ) + { + assert!(same_optional_usize( + tail.size_for_elems(elems), + reference_size(tail, align, phase, elems), + )); + assert!(same_optional_usize( + tail.max_trailing_bytes(budget), + reference_capacity(tail, align, phase, budget), + )); + } +}