From 8142b6126a2769a194f06abc8ec098d8e990b9d4 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 11:00:09 -0400 Subject: [PATCH] Prove advancement and padding-sequence decisions Specify trailing-layout advancement, size offsets, wrapping padding and dynamic-padding classification against the mathematical formulas. Prove that a positive size-sequence comparison implies equal complete sizes for every natural metadata count. Rejection remains conservative and does not imply inequality. Add total Rust harnesses checking exact advancement outcomes and the corresponding checked-size comparisons, preserving the stronger unbounded theorem. gherrit-pr-id: Gpvecn2gjh2spv5hy32nqxdlgiqp5jus7 Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 5 +- verification/aeneas/golden/Funs.lean | 356 ++++++++++++++++-- verification/aeneas/golden/Types.lean | 8 +- verification/aeneas/lean/MathViews.lean | 15 +- verification/aeneas/lean/Obligations.lean | 39 ++ .../lean/Obligations/TailTransforms.lean | 58 +++ .../aeneas/lean/Proofs/Contracts.lean | 38 ++ .../aeneas/lean/Proofs/Raw/Layout.lean | 97 +++++ .../aeneas/lean/Proofs/Raw/Trailing.lean | 143 +++++++ .../lean/Proofs/TailTransformChecks.lean | 323 ++++++++++++++++ .../lean/Proofs/TailTransformReference.lean | 209 ++++++++++ .../TailTransforms.lean | 72 ++++ verification/aeneas/projections/Specs.lean | 54 +++ zerocopy/src/layout/mod.rs | 24 ++ zerocopy/src/layout/tail_transform_checks.rs | 188 +++++++++ 15 files changed, 1596 insertions(+), 33 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/TailTransforms.lean create mode 100644 verification/aeneas/lean/Proofs/TailTransformChecks.lean create mode 100644 verification/aeneas/lean/Proofs/TailTransformReference.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/TailTransforms.lean create mode 100644 zerocopy/src/layout/tail_transform_checks.rs diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index b09e07e5b0..b553993fa0 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -268,7 +268,7 @@ whole-program unsafe-code certification. ## Scope and proofs -Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs), [tail assertions](../../zerocopy/src/layout/tail_checks.rs), [composition assertions](../../zerocopy/src/layout/composition_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), [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 @@ -364,6 +364,9 @@ 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. + Plain arithmetic clauses use mathematical word values carrying machine bounds and, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index bb2d15bdca..daffcaa35b 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -952,7 +952,7 @@ def util.padding_needed_for ok (i2 &&& mask) /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::CURRENT_MAX_ALIGN] - Source: 'src/layout/mod.rs', lines 935:4-938:6 -/ + Source: 'src/layout/mod.rs', lines 951:4-954:6 -/ @[global_simps, irreducible] def layout.DstLayout.CURRENT_MAX_ALIGN : @@ -968,14 +968,14 @@ def layout.DstLayout.CURRENT_MAX_ALIGN | some max_align => ok max_align /-- [zerocopy::layout::POINTER_WIDTH_BITS] - Source: 'src/layout/mod.rs', lines 29:0-29:62 -/ + Source: 'src/layout/mod.rs', lines 32:0-32: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::DstLayout}::THEORETICAL_MAX_ALIGN] - Source: 'src/layout/mod.rs', lines 921:4-925:10 -/ + Source: 'src/layout/mod.rs', lines 937:4-941:10 -/ @[global_simps, irreducible] def layout.DstLayout.THEORETICAL_MAX_ALIGN : @@ -993,7 +993,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 1314:4-1460:5 + Source: 'src/layout/mod.rs', lines 1330:4-1476:5 Visibility: public -/ def layout.DstLayout.extend (self : layout.DstLayout) (field : layout.DstLayout) @@ -1167,7 +1167,7 @@ def util.round_down_to_next_multiple_of_alignment ok (n &&& mask) /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]: - Source: 'src/layout/mod.rs', lines 142:4-169:5 -/ + Source: 'src/layout/mod.rs', lines 145:4-172:5 -/ def layout.RoundingAlignAndPhase.components (self : layout.RoundingAlignAndPhase) : Result ((core.num.nonzero.NonZero Std.Usize @@ -1195,7 +1195,7 @@ def layout.RoundingAlignAndPhase.components ok (align1, phase) /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::new]: - Source: 'src/layout/mod.rs', lines 109:4-128:5 -/ + Source: 'src/layout/mod.rs', lines 112:4-131:5 -/ def layout.RoundingAlignAndPhase.new (align : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : @@ -1216,7 +1216,7 @@ def layout.RoundingAlignAndPhase.new | some encoded1 => ok { _0 := encoded1 } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::pad_to_align]: - Source: 'src/layout/mod.rs', lines 1496:4-1586:5 + Source: 'src/layout/mod.rs', lines 1512:4-1602:5 Visibility: public -/ def layout.DstLayout.pad_to_align (self : layout.DstLayout) : Result layout.DstLayout := do @@ -1341,7 +1341,7 @@ def layout.composition_checks.check_pad else ok () /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]: - Source: 'src/layout/mod.rs', lines 182:4-191:5 -/ + Source: 'src/layout/mod.rs', lines 185:4-194:5 -/ def layout.RoundingAlignAndPhase.align (self : layout.RoundingAlignAndPhase) : Result (core.num.nonzero.NonZero Std.Usize @@ -1351,7 +1351,7 @@ def layout.RoundingAlignAndPhase.align ok nz /-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_offset]: - Source: 'src/layout/mod.rs', lines 271:4-284:5 -/ + Source: 'src/layout/mod.rs', lines 274:4-287:5 -/ def layout.TrailingSliceLayout.size_offset {E : Type} (self : layout.TrailingSliceLayout E) : Result Std.Usize := do let (size_align, size_phase) ← @@ -1361,7 +1361,7 @@ def layout.TrailingSliceLayout.size_offset ok (aligned_base ||| size_phase) /-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::max_trailing_bytes]: - Source: 'src/layout/mod.rs', lines 307:4-396:5 -/ + Source: 'src/layout/mod.rs', lines 310:4-399:5 -/ def layout.TrailingSliceLayout.max_trailing_bytes {E : Type} (self : layout.TrailingSliceLayout E) (available_bytes : Std.Usize) : @@ -1390,7 +1390,7 @@ def layout.TrailingSliceLayout.max_trailing_bytes ok (some trailing_bytes) /-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::padding_for_elems]: - Source: 'src/layout/mod.rs', lines 421:4-476:5 -/ + Source: 'src/layout/mod.rs', lines 424:4-479:5 -/ def layout.TrailingSliceLayoutUsize.padding_for_elems (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : Result Std.Usize @@ -1412,7 +1412,7 @@ def layout.TrailingSliceLayoutUsize.padding_for_elems ok (core.num.Usize.wrapping_add i3 rounding_padding) /-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_for_elems]: - Source: 'src/layout/mod.rs', lines 494:4-558:5 -/ + Source: 'src/layout/mod.rs', lines 497:4-561:5 -/ def layout.TrailingSliceLayoutUsize.size_for_elems (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : Result (Option Std.Usize) @@ -1435,8 +1435,83 @@ def layout.TrailingSliceLayoutUsize.size_for_elems let size ← lift (core.num.Usize.wrapping_add trailing_end i) ok (some size) +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::has_same_size_sequence]: + Source: 'src/layout/mod.rs', lines 585:4-662:5 -/ +def layout.TrailingSliceLayoutUsize.has_same_size_sequence + (self : layout.TrailingSliceLayout Std.Usize) + (other : layout.TrailingSliceLayout Std.Usize) : + Result Bool + := do + if self.elem_size != other.elem_size + then ok false + else + let o ← layout.TrailingSliceLayoutUsize.size_for_elems self 0#usize + let o1 ← layout.TrailingSliceLayoutUsize.size_for_elems other 0#usize + match o with + | none => ok false + | some self_size => + match o1 with + | none => ok false + | some other_size => + if self_size = other_size + then + let (self_align, self_phase) ← + layout.RoundingAlignAndPhase.components + self.size_rounding_align_and_phase + let (other_align, other_phase) ← + layout.RoundingAlignAndPhase.components + other.size_rounding_align_and_phase + let self_align1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + self_align + let other_align1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + other_align + let max_align ← + if self_align1 > other_align1 + then ok self_align1 + else ok other_align1 + let i ← self.elem_size % max_align + if i = 0#usize + then ok true + else + if self_align1 != other_align1 + then ok false + else ok (self_phase = other_phase) + else ok false + +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::advance]: + Source: 'src/layout/mod.rs', lines 706:4-802:5 -/ +def layout.TrailingSliceLayoutUsize.advance + (self : layout.TrailingSliceLayout Std.Usize) (bytes : Std.Usize) + (elem_size : Std.Usize) : + Result (Option (layout.TrailingSliceLayout 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 align_mask ← i - 1#usize + let i1 ← core.num.Usize.MAX - self.size_base + let phase_capacity ← lift (i1 ||| align_mask) + let max_advance ← phase_capacity - size_phase + if bytes > max_advance + then ok none + else + let advanced_phase ← size_phase + bytes + let normalized_phase ← lift (advanced_phase &&& align_mask) + let whole_bytes ← + util.round_down_to_next_multiple_of_alignment advanced_phase size_align + let size_base ← self.size_base + whole_bytes + let raap ← layout.RoundingAlignAndPhase.new size_align normalized_phase + ok (some + { self with elem_size, size_base, size_rounding_align_and_phase := raap }) + /-- [zerocopy::layout::{zerocopy::layout::SizeInfo}::try_to_nonzero_elem_size]: - Source: 'src/layout/mod.rs', lines 820:4-848:5 -/ + Source: 'src/layout/mod.rs', lines 836:4-864:5 -/ def layout.SizeInfoUsize.try_to_nonzero_elem_size (self : layout.SizeInfo Std.Usize) : Result (Option (layout.SizeInfo (core.num.nonzero.NonZero Std.Usize @@ -1461,7 +1536,7 @@ def layout.SizeInfoUsize.try_to_nonzero_elem_size })) /-- [zerocopy::layout::max_elems_for_bytes]: - Source: 'src/layout/mod.rs', lines 876:0-891:1 -/ + Source: 'src/layout/mod.rs', lines 892:0-907:1 -/ def layout.max_elems_for_bytes (bytes : Std.Usize) (elem_size : core.num.nonzero.NonZero Std.Usize @@ -1478,7 +1553,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 911:4-914:6 -/ + Source: 'src/layout/mod.rs', lines 927:4-930:6 -/ @[global_simps, irreducible] def layout.DstLayout.MIN_ALIGN : @@ -1493,13 +1568,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 980:4-989:5 -/ + 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 1018:4-1038:5 + Source: 'src/layout/mod.rs', lines 1034:4-1054:5 Visibility: public -/ def layout.DstLayout.new_zst (repr_align : Option (core.num.nonzero.NonZero Std.Usize @@ -1523,7 +1598,7 @@ def layout.DstLayout.new_zst } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_type]: - Source: 'src/layout/mod.rs', lines 1062:4-1087:5 + Source: 'src/layout/mod.rs', lines 1078:4-1103:5 Visibility: public -/ def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do let i ← core.mem.align_of T @@ -1542,7 +1617,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 1117:4-1131:5 + Source: 'src/layout/mod.rs', lines 1133:4-1147:5 Visibility: public -/ def layout.DstLayout.for_unpadded_type (T : Type) : Result layout.DstLayout := do @@ -1550,7 +1625,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 1156:4-1192:5 -/ + Source: 'src/layout/mod.rs', lines 1172:4-1208:5 -/ def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do let i ← core.mem.align_of T let o ← @@ -1576,12 +1651,37 @@ 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 1603:4-1612:5 + Source: 'src/layout/mod.rs', lines 1619:4-1628: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 + Visibility: public -/ +def layout.DstLayout.requires_dynamic_padding + (self : layout.DstLayout) : Result Bool := do + match self.size_info with + | layout.SizeInfo.Sized _ => ok false + | layout.SizeInfo.SliceDst trailing_slice_layout => + let o ← + layout.TrailingSliceLayoutUsize.size_for_elems trailing_slice_layout + 0#usize + match o with + | none => ok true + | some initial_size => + let nz ← + layout.RoundingAlignAndPhase.align + trailing_slice_layout.size_rounding_align_and_phase + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz + let i1 ← trailing_slice_layout.elem_size % i + if initial_size != trailing_slice_layout.offset + then ok true + else ok (¬ (i1 = 0#usize)) + /-- [zerocopy::layout::nested_reference::round_up]: Source: 'src/layout/nested_reference.rs', lines 48:0-58:1 -/ def layout.nested_reference.round_up @@ -1899,6 +1999,220 @@ def layout.tail_checks.trailing_arithmetic_check else ok () else ok () +/-- [zerocopy::layout::tail_transform_checks::witness_matches]: + Source: 'src/layout/tail_transform_checks.rs', lines 30:0-37:1 -/ +def layout.tail_transform_checks.witness_matches + (tail : layout.TrailingSliceLayout Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : + Result Bool + := do + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + 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 + layout.tail_checks.same_optional_usize o (some i1) + else ok false + else ok false + +/-- [zerocopy::layout::tail_transform_checks::reference_advance]: + Source: 'src/layout/tail_transform_checks.rs', lines 40:0-66:1 -/ +def layout.tail_transform_checks.reference_advance + (tail : layout.TrailingSliceLayout Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (bytes : Std.Usize) : + Result (Option (Std.Usize × Std.Usize)) + := do + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let remainder ← bytes % i + let whole_bytes ← bytes - remainder + let o ← lift (Usize.checked_add phase remainder) + match o with + | none => ok none + | some shifted => + let new_phase ← shifted % i + let carry ← shifted - new_phase + let o1 ← lift (Usize.checked_add tail.size_base whole_bytes) + match o1 with + | none => ok none + | some base => + let o2 ← lift (Usize.checked_add base carry) + match o2 with + | none => ok none + | some base1 => ok (some (base1, new_phase)) + +/-- [zerocopy::layout::tail_transform_checks::reference_wrapping_padding]: + Source: 'src/layout/tail_transform_checks.rs', lines 69:0-86:1 -/ +def layout.tail_transform_checks.reference_wrapping_padding + (tail : layout.TrailingSliceLayout Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (elems : Std.Usize) : + Result Std.Usize + := do + let trailing_bytes ← + lift (core.num.Usize.wrapping_mul elems tail.elem_size) + let rounding_input ← + lift (core.num.Usize.wrapping_add phase trailing_bytes) + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let remainder ← rounding_input % i + let padding ← if remainder = 0#usize + then ok 0#usize + else i - remainder + let rounded ← lift (core.num.Usize.wrapping_add rounding_input padding) + let complete ← lift (core.num.Usize.wrapping_add tail.size_base rounded) + let slice_end ← + lift (core.num.Usize.wrapping_add tail.offset trailing_bytes) + ok (core.num.Usize.wrapping_sub complete slice_end) + +/-- [zerocopy::layout::tail_transform_checks::tail_transformations_check]: + Source: 'src/layout/tail_transform_checks.rs', lines 101:0-134:1 -/ +def layout.tail_transform_checks.tail_transformations_check + (tail : layout.TrailingSliceLayout Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (bytes : Std.Usize) (replacement_stride : Std.Usize) (elems : Std.Usize) : + Result Unit + := do + let b ← layout.tail_transform_checks.witness_matches tail align phase + if b + then + let actual ← + layout.TrailingSliceLayoutUsize.advance tail bytes replacement_stride + let expected ← + layout.tail_transform_checks.reference_advance tail align phase bytes + let (tail1, same) ← + match actual with + | none => + do + let b1 ← match expected with + | none => ok true + | some _ => ok false + ok (tail, b1) + | some actual1 => + match expected with + | none => ok (tail, false) + | some p => + do + let (base, new_phase) := p + let b1 ← + if actual1.offset = tail.offset + then + if actual1.elem_size = replacement_stride + then + if actual1.size_base = base + then + do + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + align + let o ← lift (Usize.checked_add i new_phase) + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + actual1.size_rounding_align_and_phase._0 + layout.tail_checks.same_optional_usize o (some i1) + else ok false + else ok false + else ok false + ok (tail, b1) + massert same + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let i1 ← tail1.size_base % i + let floor_base ← tail1.size_base - i1 + let i2 ← layout.TrailingSliceLayout.size_offset tail1 + let o ← lift (Usize.checked_add floor_base phase) + let b1 ← layout.tail_checks.same_optional_usize (some i2) o + massert b1 + let i3 ← layout.TrailingSliceLayoutUsize.padding_for_elems tail1 elems + let i4 ← + layout.tail_transform_checks.reference_wrapping_padding tail1 align phase + elems + massert (i3 = i4) + else ok () + +/-- [zerocopy::layout::tail_transform_checks::tail_size_sequence_check]: + Source: 'src/layout/tail_transform_checks.rs', lines 145:0-163:1 -/ +def layout.tail_transform_checks.tail_size_sequence_check + (left : layout.TrailingSliceLayout Std.Usize) + (right : layout.TrailingSliceLayout Std.Usize) + (left_align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (left_phase : Std.Usize) + (right_align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (right_phase : Std.Usize) + (elems : Std.Usize) : + Result Unit + := do + let b ← + layout.tail_transform_checks.witness_matches left left_align left_phase + if b + then + let b1 ← + layout.tail_transform_checks.witness_matches right right_align + right_phase + if b1 + then + let b2 ← + layout.TrailingSliceLayoutUsize.has_same_size_sequence left right + if b2 + then + let o ← + layout.tail_checks.reference_size left left_align left_phase elems + let o1 ← + layout.tail_checks.reference_size right right_align right_phase elems + let b3 ← layout.tail_checks.same_optional_usize o o1 + massert b3 + else ok () + else ok () + else ok () + +/-- [zerocopy::layout::tail_transform_checks::tail_dynamic_padding_check]: + Source: 'src/layout/tail_transform_checks.rs', lines 174:0-188:1 -/ +def layout.tail_transform_checks.tail_dynamic_padding_check + (runtime_layout : layout.DstLayout) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : + Result Unit + := do + match runtime_layout.size_info with + | layout.SizeInfo.Sized _ => + let b ← layout.DstLayout.requires_dynamic_padding runtime_layout + massert (¬ b) + | layout.SizeInfo.SliceDst tail => + let b ← layout.tail_transform_checks.witness_matches tail align phase + if b + then + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let stride_remainder ← tail.elem_size % i + let o ← layout.tail_checks.reference_size tail align phase 0#usize + let b1 ← layout.tail_checks.same_optional_usize o (some tail.offset) + let no_dynamic_padding ← + if b1 + then ok (stride_remainder = 0#usize) + else ok false + let b2 ← layout.DstLayout.requires_dynamic_padding runtime_layout + massert (b2 = (¬ no_dynamic_padding)) + else ok () + /-- [zerocopy::{impl zerocopy::PointerMetadata for ()}::from_elem_count]: Source: 'src/lib.rs', lines 975:4-975:46 Visibility: public -/ diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index cd19cd1994..0e63ebd96e 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -203,13 +203,13 @@ structure layout.composition_checks.ReferenceLayout where unpadded : Bool /-- [zerocopy::layout::RoundingAlignAndPhase] - Source: 'src/layout/mod.rs', lines 90:0-90:54 -/ + Source: 'src/layout/mod.rs', lines 93:0-93: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 197:0-251:1 -/ + Source: 'src/layout/mod.rs', lines 200:0-254:1 -/ structure layout.TrailingSliceLayout (E : Type) where offset : Std.Usize elem_size : E @@ -217,14 +217,14 @@ structure layout.TrailingSliceLayout (E : Type) where size_rounding_align_and_phase : layout.RoundingAlignAndPhase /-- [zerocopy::layout::SizeInfo] - Source: 'src/layout/mod.rs', lines 59:0-62:1 -/ + Source: 'src/layout/mod.rs', lines 62:0-65: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 46:0-54:1 + Source: 'src/layout/mod.rs', lines 49:0-57:1 Visibility: public -/ structure layout.DstLayout where align : core.num.nonzero.NonZero Std.Usize diff --git a/verification/aeneas/lean/MathViews.lean b/verification/aeneas/lean/MathViews.lean index 99f754dc03..bfb06410d0 100644 --- a/verification/aeneas/lean/MathViews.lean +++ b/verification/aeneas/lean/MathViews.lean @@ -178,6 +178,14 @@ def layoutValid (self : layout.DstLayout) : Prop := simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using trailing_admitted_iff raw +-- Optional traversal exposes the same fixed provider's named decoder directly. +@[contract_simps] theorem trailing_usize_decoder_admitted_iff + (raw : layout.TrailingSliceLayout Usize) : + (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize), + layout.TrailingSliceLayout.decode Usize raw = some value) ↔ + 0 < raw.size_rounding_align_and_phase._0.val.val := + trailing_usize_admitted_iff raw + @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) : Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff @@ -203,11 +211,4 @@ 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_decoder_admitted_iff - (raw : layout.TrailingSliceLayout Usize) : - (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize), - layout.TrailingSliceLayout.decode Usize raw = some value) ↔ - 0 < raw.size_rounding_align_and_phase._0.val.val := - trailing_usize_admitted_iff raw - end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index 62ce35cca4..3002b1cad9 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -170,6 +170,31 @@ 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 same_size_sequence_spec_contract (a b : layout.TrailingSliceLayout Usize) + (run : Result Bool) : Prop := + 0 < a.size_rounding_align_and_phase._0.val.val → 0 < b.size_rounding_align_and_phase._0.val.val → + ∃ same, run = .ok same ∧ + (same = true → ∀ n : Nat, (trailingFormula a).size n = (trailingFormula b).size n) + +def same_size_sequence_spec : Prop := + ∀ (a b : layout.TrailingSliceLayout Usize), + same_size_sequence_spec_contract a b + (layout.TrailingSliceLayoutUsize.has_same_size_sequence a b) + +def advance_spec_contract (t : layout.TrailingSliceLayout Usize) (bytes stride : Usize) + (run : Result (Option (layout.TrailingSliceLayout Usize))) : Prop := + 0 < t.size_rounding_align_and_phase._0.val.val → + run ⦃ r => (∀ next ∈ r, encodingValid next.size_rounding_align_and_phase) ∧ + match r with + | none => Usize.max < ((trailingFormula t).advance bytes.val stride.val).base + | some next => trailingFormula next = (trailingFormula t).advance bytes.val stride.val ∧ + ((trailingFormula t).advance bytes.val stride.val).base ≤ Usize.max ⦄ + +def advance_spec : Prop := + ∀ (t : layout.TrailingSliceLayout Usize) (bytes stride : Usize), + advance_spec_contract t bytes stride + (layout.TrailingSliceLayoutUsize.advance t bytes stride) + def try_nonzero_spec_contract (si : layout.SizeInfo Usize) (run : Result (Option (layout.SizeInfo NonZeroUsize))) : Prop := sizeInfoValid si → run ⦃ r => (∀ next ∈ r, sizeInfoValid next) ∧ @@ -309,6 +334,20 @@ def requires_static_padding_spec : Prop := ∀ (self : layout.DstLayout), requires_static_padding_spec_contract self (layout.DstLayout.requires_static_padding self) +def requires_dynamic_padding_spec_contract (self : layout.DstLayout) + (run : Result Bool) : Prop := + layoutValid self → + ∃ r, run = .ok r ∧ + (r = false ↔ match self.size_info with + | .Sized _ => True + | .SliceDst t => (trailingFormula t).size 0 = t.offset.val ∧ + t.elem_size.val % (trailingFormula t).align = 0) + +def requires_dynamic_padding_spec : Prop := + ∀ (self : layout.DstLayout), + requires_dynamic_padding_spec_contract self + (layout.DstLayout.requires_dynamic_padding self) + end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Obligations/TailTransforms.lean b/verification/aeneas/lean/Obligations/TailTransforms.lean new file mode 100644 index 0000000000..154c0df387 --- /dev/null +++ b/verification/aeneas/lean/Obligations/TailTransforms.lean @@ -0,0 +1,58 @@ +/- 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 arbitrary-run contracts retain the full decoded machine-word domain. +Their total True conclusions discharge the numerical assertions visible in +Rust; the original natural-number method obligations remain independent. +-/ +def tail_transformations_check_spec_contract + (tail : layout.TrailingSliceLayout Usize) (align : NonZeroUsize) + (phase bytes replacement_stride elems : Usize) (run : Result Unit) : Prop := + 0 < tail.size_rounding_align_and_phase._0.val.val → 0 < align.val.val → + run ⦃ _ => True ⦄ + +def tail_transformations_check_spec : Prop := + ∀ tail align phase bytes replacement_stride elems, + tail_transformations_check_spec_contract tail align phase bytes replacement_stride elems + (layout.tail_transform_checks.tail_transformations_check + tail align phase bytes replacement_stride elems) + +def tail_size_sequence_check_spec_contract + (left right : layout.TrailingSliceLayout Usize) + (left_align : NonZeroUsize) (left_phase : Usize) + (right_align : NonZeroUsize) (right_phase elems : Usize) (run : Result Unit) : Prop := + 0 < left.size_rounding_align_and_phase._0.val.val → + 0 < right.size_rounding_align_and_phase._0.val.val → + 0 < left_align.val.val → 0 < right_align.val.val → run ⦃ _ => True ⦄ + +def tail_size_sequence_check_spec : Prop := + ∀ left right left_align left_phase right_align right_phase elems, + tail_size_sequence_check_spec_contract left right left_align left_phase right_align right_phase elems + (layout.tail_transform_checks.tail_size_sequence_check + left right left_align left_phase right_align right_phase elems) + +def tail_dynamic_padding_check_spec_contract + (runtime_layout : layout.DstLayout) (align : NonZeroUsize) (phase : Usize) + (run : Result Unit) : Prop := + layoutValid runtime_layout → 0 < align.val.val → run ⦃ _ => True ⦄ + +def tail_dynamic_padding_check_spec : Prop := + ∀ runtime_layout align phase, + tail_dynamic_padding_check_spec_contract runtime_layout align phase + (layout.tail_transform_checks.tail_dynamic_padding_check runtime_layout align phase) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/Contracts.lean b/verification/aeneas/lean/Proofs/Contracts.lean index 1e39b28417..49a14110e0 100644 --- a/verification/aeneas/lean/Proofs/Contracts.lean +++ b/verification/aeneas/lean/Proofs/Contracts.lean @@ -131,6 +131,16 @@ theorem size_for_elems_spec : Zerocopy.Specs.size_for_elems_spec := by exact facts register_spec_step size_for_elems_spec +/- Prove that a positive comparison implies equal sizes for all metadata. The +negative branch deliberately promises no inequality between the sequences. +-/ +theorem same_size_sequence_spec : Zerocopy.Specs.same_size_sequence_spec := by + unfold Zerocopy.Specs.same_size_sequence_spec + representation_simps + intro self other hs ho + exact Raw.same_size_sequence_spec self other hs ho +register_spec_step same_size_sequence_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 @@ -203,11 +213,39 @@ theorem requires_static_padding_spec : Zerocopy.Specs.requires_static_padding_sp exact Raw.requires_static_padding_spec self register_spec_step requires_static_padding_spec +theorem requires_dynamic_padding_spec : Zerocopy.Specs.requires_dynamic_padding_spec := by + unfold Zerocopy.Specs.requires_dynamic_padding_spec + representation_simps + intro self hv + apply Raw.requires_dynamic_padding_spec self + cases hs : self.size_info with + | Sized _ => trivial + | SliceDst _ => simpa only [hs] using hv.2 +register_spec_step requires_dynamic_padding_spec + end Zerocopy.Proofs namespace Zerocopy.Proofs open AeneasSpecs +/- Changing the byte origin must preserve the complete-size formula. Carry +aligned bytes into base and keep the residual phase without losing physical +offset. +-/ +theorem advance_spec : Zerocopy.Specs.advance_spec := by + unfold Zerocopy.Specs.advance_spec + representation_simps + intro self bytes elem hv + apply WP.spec_mono (Raw.advance_spec self bytes elem hv) + rintro result ⟨accepted, facts⟩ + refine ⟨?_, facts⟩ + change isValid result + rw [option_valid_iff] + intro next member + rw [trailing_valid_iff] + exact ⟨by simp, accepted next member⟩ +register_spec_step advance_spec + /- 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. diff --git a/verification/aeneas/lean/Proofs/Raw/Layout.lean b/verification/aeneas/lean/Proofs/Raw/Layout.lean index 1567d1ae96..26d49b1f6c 100644 --- a/verification/aeneas/lean/Proofs/Raw/Layout.lean +++ b/verification/aeneas/lean/Proofs/Raw/Layout.lean @@ -309,4 +309,101 @@ theorem theoretical_max_align_spec : ↓reduceDIte, ↓reduceIte, bind_ok, WP.spec_ok] exact hv +theorem fill_low_bits (n k : Nat) : n ||| (2 ^ k - 1) = n - n % 2 ^ k + (2 ^ k - 1) := by + have h : (n - n % 2 ^ k) % 2 ^ k = 0 := by + rw [← Nat.div_mul_self_eq_mod_sub_self, Nat.mul_mod_left] + rw [← LayoutMath.aligned_or _ _ _ ⟨k, rfl⟩ h (by have := Nat.two_pow_pos k; omega)] + apply Nat.eq_of_testBit_eq + intro i + rw [Nat.testBit_or, Nat.testBit_or, Nat.testBit_two_pow_sub_one] + by_cases hi : i < k + · simp only [hi, decide_true, Bool.or_true] + · simp only [hi, decide_false, Bool.or_false] + rw [← Nat.div_mul_self_eq_mod_sub_self, ← Nat.shiftLeft_eq] + rw [Nat.testBit_shiftLeft] + rw [Nat.testBit_div_two_pow] + simp only [show k ≤ i by omega, decide_true, Bool.true_and, + show i - k + k = i by omega] + +/- Changing the byte origin must preserve the complete-size formula. Carry +aligned bytes into base and keep the residual phase without losing physical +offset. +-/ +theorem advance_spec : + ∀ (self : layout.TrailingSliceLayout Usize) (bytes elem_size : Usize), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)), + @Zerocopy.layout.TrailingSliceLayoutUsize.advance self bytes elem_size ⦃ result => (∀ t ∈ result, encodingValid t.size_rounding_align_and_phase) ∧ match result with + | none => Usize.max < ((trailingFormula self).advance bytes.val elem_size.val).base + | some t => trailingFormula t = (trailingFormula self).advance bytes.val elem_size.val ∧ + ((trailingFormula self).advance bytes.val elem_size.val).base ≤ Usize.max ⦄ := by + intro self bytes elem hn + unfold layout.TrailingSliceLayoutUsize.advance + step with encoding_components_spec _ hn as ⟨a, p, ha, hp, hsum, halign, hphase⟩ + have hv := trailing_view self a.val.val p.val ha hp hsum.symm + have apos := Nat.pos_of_isPowerOfTwo ha + simp only [core.num.nonzero.NonZero.get, bind_ok] + 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, _⟩ + step with Usize.sub_spec (show self.size_base.val ≤ core.num.Usize.MAX.val by scalar_tac) as ⟨available, hav, _⟩ + let pc := available ||| mask + have hpc : pc.val = (Usize.max - self.size_base.val) - + (Usize.max - self.size_base.val) % a.val.val + (a.val.val - 1) := by + obtain ⟨k, hk⟩ := ha + rw [UScalar.val_or, hm, hav] + rw [hk, fill_low_bits] + have hpbound : p.val ≤ pc.val := by + have hor : mask.val ≤ pc.val := by + rw [UScalar.val_or] + exact Nat.right_le_or + omega + simp only [lift, bind_ok] + step with Usize.sub_spec hpbound as ⟨advance, hadv, _⟩ + dsimp only [pc] at * + simp only [UScalar.lt_equiv] + split + · rename_i hlarge + simp only [WP.spec_ok, hv, LayoutMath.Formula.advance] + constructor + · simp + · have hcap := LayoutMath.floor_capacity (p.val + bytes.val) + (Usize.max - self.size_base.val) a.val.val apos + have hbase : self.size_base.val ≤ Usize.max := by scalar_tac + have hrem := Nat.mod_le (p.val + bytes.val) a.val.val + omega + · rename_i hsmall + have hshift : p.val + bytes.val ≤ (available ||| mask).val := by omega + have hword : (available ||| mask).val ≤ Usize.max := by + have h := UScalar.hSize (available ||| mask) + simp only [UScalar.size, Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq] at h ⊢ + have := Nat.two_pow_pos System.Platform.numBits + omega + step with Usize.add_spec (x := p) (y := bytes) (by omega) as ⟨shifted, hshifted⟩ + have hlow : (shifted &&& mask).val = shifted.val % a.val.val := by + obtain ⟨k, hk⟩ := ha + rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod] + step with round_down_spec shifted a ha as ⟨whole, _, hwhole, _, _, _⟩ + have hbase : self.size_base.val + whole.val ≤ Usize.max := by + have hcap := (LayoutMath.floor_capacity (p.val + bytes.val) + (Usize.max - self.size_base.val) a.val.val apos).mpr (by omega) + rw [hwhole, hshifted] + have hb : self.size_base.val ≤ Usize.max := by scalar_tac + omega + step with Usize.add_spec (x := self.size_base) (y := whole) hbase as ⟨base, hb⟩ + step with encoding_new_spec a (shifted &&& mask) ha (by rw [hlow]; exact Nat.mod_lt _ apos) as ⟨encoded, he⟩ + have hnew := trailing_view + ({ self with elem_size := elem, size_base := base, size_rounding_align_and_phase := encoded }) + a.val.val (shifted.val % a.val.val) ha (Nat.mod_lt _ apos) (by rw [he, hlow]) + have hencoded : encodingValid encoded := by + unfold encodingValid + rw [he] + omega + simp only [hnew, hv, LayoutMath.Formula.advance] + refine ⟨?_, ?_, ?_⟩ + · simpa using hencoded + · rw [hshifted, hb, hwhole, hshifted] + congr 1 + have := Nat.mod_le (p.val + bytes.val) a.val.val + omega + · rw [hwhole, hshifted] at hbase + have := Nat.mod_le (p.val + bytes.val) a.val.val + omega + end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/Proofs/Raw/Trailing.lean b/verification/aeneas/lean/Proofs/Raw/Trailing.lean index b325790be0..b7735cce7d 100644 --- a/verification/aeneas/lean/Proofs/Raw/Trailing.lean +++ b/verification/aeneas/lean/Proofs/Raw/Trailing.lean @@ -276,6 +276,67 @@ theorem size_for_elems_spec : p.val + self.offset.val + elems.val * self.elem_size.val by omega, hp, word_mod_of_le _ hfit] +theorem checked_some_size (f : LayoutMath.Formula) (n : Nat) (size : Usize) + (h : some size.val = f.checkedSize Usize.max n) : + size.val = f.size n ∧ f.size n ≤ Usize.max := by + unfold LayoutMath.Formula.checkedSize at h + split at h <;> simp_all + +theorem checked_none_size (f : LayoutMath.Formula) (n : Nat) + (h : none = f.checkedSize Usize.max n) : Usize.max < f.size n := by + unfold LayoutMath.Formula.checkedSize at h + split at h <;> simp_all + +theorem requires_dynamic_padding_spec : + ∀ (self : layout.DstLayout), ∀ (hn : (match self.size_info with + | .Sized _ => True + | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val : Prop)), + @Zerocopy.layout.DstLayout.requires_dynamic_padding self ⦃ r => (r = false ↔ match self.size_info with + | .Sized _ => True + | .SliceDst tail => (trailingFormula tail).size 0 = tail.offset.val ∧ + tail.elem_size.val % (trailingFormula tail).align = 0) ⦄ := by + intro self hn + unfold layout.DstLayout.requires_dynamic_padding + cases hs : self.size_info with + | Sized size => simp [WP.spec_ok] + | SliceDst tail => + simp only [hs] at hn + step with size_for_elems_spec tail 0#usize hn as ⟨initial, hi⟩ + cases initial with + | none => + dsimp only + have hmiss := checked_none_size _ _ hi + have hoff : tail.offset.val ≤ Usize.max := by scalar_tac + apply WP.spec.ret + simp only [Bool.true_eq_false, false_iff] + intro h + omega + | some initial => + dsimp only + have hv := checked_some_size _ _ initial hi + step with encoding_align_spec _ hn as ⟨a, ha⟩ + simp only [core.num.nonzero.NonZero.get, bind_ok] + have hap : 0 < a.val.val := by rw [ha]; exact Nat.two_pow_pos _ + step with Usize.rem_spec tail.elem_size (y := a.val) (by omega) as ⟨remainder, hr⟩ + simp only [bne_iff_ne] + split + · rename_i hne + apply WP.spec.ret + simp only [Bool.true_eq_false, false_iff] + intro h + apply hne + apply UScalar.eq_of_val_eq + omega + · rename_i heq + have heq' : initial.val = tail.offset.val := by + have h : initial = tail.offset := not_ne_iff.mp heq + exact congrArg UScalar.val h + apply WP.spec.ret + simp only [decide_eq_false_iff_not, not_not, UScalar.eq_equiv, + show (0#usize).val = 0 by simp, hr, ← heq', ← hv.1, true_and] + rw [ha] + rfl + theorem power_dvd_of_le (a b : Nat) (ha : a.isPowerOfTwo) (hb : b.isPowerOfTwo) (hle : a ≤ b) : a ∣ b := by obtain ⟨i, hi⟩ := ha @@ -283,4 +344,86 @@ theorem power_dvd_of_le (a b : Nat) (ha : a.isPowerOfTwo) (hb : b.isPowerOfTwo) rw [hi, hj] at hle ⊢ exact Nat.pow_dvd_pow 2 ((Nat.pow_le_pow_iff_right (by decide : 1 < 2)).mp hle) +/- Prove that a positive comparison implies equal sizes for all metadata. The +negative branch deliberately promises no inequality between the sequences. +-/ +theorem same_size_sequence_spec : + ∀ (self other : layout.TrailingSliceLayout Usize), ∀ (hs : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)), ∀ (ho : (0 < other.size_rounding_align_and_phase._0.val.val : Prop)), + @Zerocopy.layout.TrailingSliceLayoutUsize.has_same_size_sequence self other ⦃ b => b = true → ∀ n : Nat, (trailingFormula self).size n = (trailingFormula other).size n ⦄ := by + intro self other hs ho + unfold layout.TrailingSliceLayoutUsize.has_same_size_sequence + simp only [bne_iff_ne] + split + · simp [WP.spec_ok] + · rename_i he + have helem : self.elem_size = other.elem_size := not_ne_iff.mp he + step with size_for_elems_spec self 0#usize hs as ⟨s, hsize⟩ + step with size_for_elems_spec other 0#usize ho as ⟨o, hother⟩ + cases s with + | none => simp [WP.spec_ok] + | some s => + cases o with + | none => simp [WP.spec_ok] + | some o => + dsimp only + split + · rename_i hsame + have hz : (trailingFormula self).size 0 = (trailingFormula other).size 0 := by + have h1 := (checked_some_size _ _ s hsize).1 + have h2 := (checked_some_size _ _ o hother).1 + have hh := congrArg UScalar.val hsame + omega + step with encoding_components_spec _ hs as ⟨a, p, ha, hp, _, hav, hpv⟩ + step with encoding_components_spec _ ho as ⟨b, q, hb, hq, _, hbv, hqv⟩ + simp only [core.num.nonzero.NonZero.get, bind_ok] + have hmax : (if a.val > b.val then Result.ok a.val else Result.ok b.val) = + Result.ok (max a.val b.val) := by + by_cases h : a.val > b.val + · simp only [h, if_true, max_eq_left (le_of_lt h)] + · simp only [h, if_false, max_eq_right (le_of_not_gt h)] + rw [hmax] + simp only [bind_ok] + have hmaxp : 0 < (max a.val b.val).val := by + rw [Arithmetic.coe_max] + exact Nat.lt_of_lt_of_le (Nat.pos_of_isPowerOfTwo ha) (Nat.le_max_left _ _) + step with Usize.rem_spec self.elem_size (y := max a.val b.val) (by omega) as ⟨rem, hr⟩ + split + · rename_i hrem + apply WP.spec.ret + intro _ n + have hm : self.elem_size.val % (max a.val b.val).val = 0 := by + have := congrArg UScalar.val hrem + simpa only [show (0#usize).val = 0 by simp, hr] using this + have hmaxpow : (max a.val b.val).val.isPowerOfTwo := by + rw [Arithmetic.coe_max] + by_cases h : a.val.val ≤ b.val.val + · simpa only [Nat.max_eq_right h] using hb + · simpa only [Nat.max_eq_left (by omega : b.val.val ≤ a.val.val)] using ha + have hda := power_dvd_of_le _ _ ha hmaxpow (by rw [Arithmetic.coe_max]; exact Nat.le_max_left _ _) + have hdb := power_dvd_of_le _ _ hb hmaxpow (by rw [Arithmetic.coe_max]; exact Nat.le_max_right _ _) + have hma : self.elem_size.val % a.val.val = 0 := by + rw [← Nat.mod_mod_of_dvd _ hda, hm, Nat.zero_mod] + have hmb : other.elem_size.val % b.val.val = 0 := by + rw [← helem, ← Nat.mod_mod_of_dvd _ hdb, hm, Nat.zero_mod] + apply LayoutMath.same_sequence_sound _ _ _ n + refine ⟨congrArg UScalar.val helem, hz, Or.inl ?_⟩ + simp only [trailingFormula, byteFormula] + rw [← hav, ← hbv] + exact ⟨hma, hmb⟩ + · split + · simp [WP.spec_ok] + · rename_i heqa + apply WP.spec.ret + simp only [decide_eq_true_eq] + intro heqp n + apply LayoutMath.same_sequence_sound _ _ _ n + refine ⟨congrArg UScalar.val helem, hz, Or.inr ?_⟩ + have haeq : a.val = b.val := not_ne_iff.mp heqa + have haveq := congrArg UScalar.val haeq + have hpveq := congrArg UScalar.val heqp + simp only [trailingFormula, byteFormula] + rw [← hpv, ← hqv, ← hav, ← hbv] + exact ⟨haveq, hpveq⟩ + · simp [WP.spec_ok] + end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/Proofs/TailTransformChecks.lean b/verification/aeneas/lean/Proofs/TailTransformChecks.lean new file mode 100644 index 0000000000..f59d5031ba --- /dev/null +++ b/verification/aeneas/lean/Proofs/TailTransformChecks.lean @@ -0,0 +1,323 @@ +/- 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.TailTransformReference +public import RequiredModelContracts.TailTransforms +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw.TailTransforms +open TailChecks +set_option linter.unusedVariables false +set_option linter.unusedSimpArgs false + +/- A literal view of the extracted comparison block keeps its matcher stable +while proving all stored fields and both Option outcomes. It does not replace +or bypass either the production transformation or the independent reference. +-/ +theorem word_bound (word : Usize) : word.val ≤ Usize.max := by + simpa only [UScalar.rMax_eq_pow_numBits, Usize.max, Usize.numBits] using word.hrBounds + +def advanceComparison (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (elem : Usize) + (actual : Option (layout.TrailingSliceLayout Usize)) (expected : Option (Usize × Usize)) : + Result (layout.TrailingSliceLayout Usize × Bool) := + match (generalizing := false) actual with + | none => do + let same ← match (generalizing := false) expected with + | none => Result.ok true + | some _ => Result.ok false + Result.ok (tail, same) + | some actual => + match (generalizing := false) expected with + | none => Result.ok (tail, false) + | some pair => + do + let (base, new_phase) := pair + let same ← + if actual.offset = tail.offset then + if actual.elem_size = elem then + if actual.size_base = base then do + let encoded ← lift (Usize.checked_add align.val new_phase) + layout.tail_checks.same_optional_usize encoded + (some actual.size_rounding_align_and_phase._0.val) + else Result.ok false + else Result.ok false + else Result.ok false + Result.ok (tail, same) + +theorem advance_comparison (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase bytes elem : Usize) + (actual : Option (layout.TrailingSliceLayout Usize)) (expected : Option (Usize × Usize)) + (actual_facts : (∀ t ∈ actual, encodingValid t.size_rounding_align_and_phase) ∧ + match actual with + | none => Usize.max < ((witnessFormula tail align phase).advance bytes.val elem.val).base + | some t => trailingFormula t = (witnessFormula tail align phase).advance bytes.val elem.val ∧ + ((witnessFormula tail align phase).advance bytes.val elem.val).base ≤ Usize.max) + (expected_facts : match expected with + | none => Usize.max < ((witnessFormula tail align phase).advance bytes.val elem.val).base + | some (base, new_phase) => + base.val = ((witnessFormula tail align phase).advance bytes.val elem.val).base ∧ + new_phase.val = ((witnessFormula tail align phase).advance bytes.val elem.val).phase ∧ + ((witnessFormula tail align phase).advance bytes.val elem.val).base ≤ Usize.max) : + advanceComparison tail align elem actual expected ⦃ pair => pair.1 = tail ∧ pair.2 = true ⦄ := by + cases actual with + | none => + cases expected with + | none => simp [advanceComparison, WP.spec_ok] + | some pair => simp only [] at actual_facts expected_facts; omega + | some actual => + cases expected with + | none => simp only [] at actual_facts expected_facts; omega + | some pair => + rcases pair with ⟨base, new_phase⟩ + simp only [] at actual_facts expected_facts + have formula_eq := actual_facts.2.1 + have offset_eq : actual.offset = tail.offset := UScalar.eq_of_val_eq + (congrArg LayoutMath.Formula.offset formula_eq) + have elem_eq : actual.elem_size = elem := UScalar.eq_of_val_eq + (congrArg LayoutMath.Formula.elem formula_eq) + have base_eq : actual.size_base = base := UScalar.eq_of_val_eq + ((congrArg LayoutMath.Formula.base formula_eq).trans expected_facts.1.symm) + have actual_positive : 0 < actual.size_rounding_align_and_phase._0.val.val := + actual_facts.1 actual (by simp) + obtain ⟨value, decoded⟩ := rounding_decode_positive actual.size_rounding_align_and_phase actual_positive + have encoded_value := (rounding_decode_iff actual.size_rounding_align_and_phase value).mp decoded + have components := rounding_decode_components actual.size_rounding_align_and_phase value decoded + have align_value : value.align = align.val.val := by + rw [components.1] + exact congrArg LayoutMath.Formula.align formula_eq + have phase_value : value.phase = new_phase.val := by + rw [components.2] + exact (congrArg LayoutMath.Formula.phase formula_eq).trans expected_facts.2.1.symm + have encoding : actual.size_rounding_align_and_phase._0.val.val = align.val.val + new_phase.val := by + change actual.size_rounding_align_and_phase._0.val.val = value.align + value.phase at encoded_value + simpa only [align_value, phase_value] using encoded_value + have encoded : Usize.checked_add align.val new_phase = + some actual.size_rounding_align_and_phase._0.val := by + apply optional_value_injective + rw [checked_add_value] + exact (checkedNat_some _ _).mpr ⟨by rw [← encoding]; exact word_bound _, encoding.symm⟩ + simp only [advanceComparison, uncurry_apply_pair, offset_eq, elem_eq, base_eq, eq_self_iff_true, if_true, encoded, lift, bind_ok] + step with same_optional_usize (some actual.size_rounding_align_and_phase._0.val) + (some actual.size_rounding_align_and_phase._0.val) as ⟨same, same_iff⟩ + simp [same_iff, WP.spec_ok] + +/- Same wrapped complete-size observations imply the same machine word: the +physical slice end cancels modulo the word size, then both residues are below +that modulus. This establishes exact output equality, not just a congruence. +-/ +theorem padding_unique (tail : layout.TrailingSliceLayout Usize) (elems left right : Usize) + (same : (left.val + tail.offset.val + elems.val * tail.elem_size.val) % UScalar.size .Usize = + (right.val + tail.offset.val + elems.val * tail.elem_size.val) % UScalar.size .Usize) : left = right := by + have modular : Nat.ModEq (UScalar.size .Usize) + (left.val + (tail.offset.val + elems.val * tail.elem_size.val)) + (right.val + (tail.offset.val + elems.val * tail.elem_size.val)) := by + change (_ % _ = _ % _) + simpa only [Nat.add_assoc] using same + have cancelled := Nat.ModEq.add_right_cancel' + (tail.offset.val + elems.val * tail.elem_size.val) modular + change left.val % UScalar.size .Usize = right.val % UScalar.size .Usize at cancelled + rw [Nat.mod_eq_of_lt (UScalar.hSize left), Nat.mod_eq_of_lt (UScalar.hSize right)] at cancelled + exact UScalar.eq_of_val_eq cancelled + +theorem offset_and_padding_check (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase elems : 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) : + (do + let remainder ← tail.size_base % align.val + let floor_base ← tail.size_base - remainder + let offset ← layout.TrailingSliceLayout.size_offset tail + let expected ← lift (Usize.checked_add floor_base phase) + let same ← layout.tail_checks.same_optional_usize (some offset) expected + massert same + let actual ← layout.TrailingSliceLayoutUsize.padding_for_elems tail elems + let expected ← layout.tail_transform_checks.reference_wrapping_padding tail align phase elems + massert (actual = expected)) ⦃ _ => True ⦄ := by + have positive := Nat.pos_of_isPowerOfTwo power + have code_positive : 0 < tail.size_rounding_align_and_phase._0.val.val := by omega + have view := witness_view tail align phase power phase_lt encoding + step with Usize.rem_spec tail.size_base (y := align.val) (by omega) as ⟨remainder, remainder_value⟩ + have remainder_bound := Nat.mod_le tail.size_base.val align.val.val + step with Usize.sub_spec (x := tail.size_base) (y := remainder) (by omega) as ⟨floor, floor_value⟩ + step with Zerocopy.Proofs.Raw.size_offset_spec tail code_positive as ⟨offset, offset_value⟩ + change offset.val = tail.size_base.val - tail.size_base.val % (trailingFormula tail).align + + (trailingFormula tail).phase at offset_value + rw [view] at offset_value + simp only [witnessFormula] at offset_value + have addition : Usize.checked_add floor phase = some offset := by + apply optional_value_injective + rw [checked_add_value] + exact (checkedNat_some _ _).mpr ⟨by have := word_bound offset; omega, by omega⟩ + simp only [addition, lift, bind_ok] + step with same_optional_usize (some offset) (some offset) as ⟨same, same_iff⟩ + simp only [massert, same_iff.mpr trivial, if_true, bind_ok] + step with Zerocopy.Proofs.Raw.padding_for_elems_spec tail elems code_positive as ⟨actual, actual_facts⟩ + step with reference_wrapping_padding tail align phase elems power as ⟨expected, expected_facts⟩ + rw [view] at actual_facts + have same := padding_unique tail elems actual expected (by + simpa only [Usize.size, Usize.numBits, UScalar.size, UScalarTy.Usize_numBits_eq] + using actual_facts.trans expected_facts.symm) + simp [massert, same, WP.spec_ok] + +theorem tail_transformations_check (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase bytes elem elems : Usize) : + layout.tail_transform_checks.tail_transformations_check tail align phase bytes elem elems ⦃ _ => True ⦄ := by + unfold layout.tail_transform_checks.tail_transformations_check + step with witness_matches tail align phase as ⟨guard_result, matches_facts⟩ + split + · rename_i matches_true + obtain ⟨power, phase_lt, encoding⟩ := matches_facts matches_true + have positive := Nat.pos_of_isPowerOfTwo power + have code_positive : 0 < tail.size_rounding_align_and_phase._0.val.val := by omega + have view := witness_view tail align phase power phase_lt encoding + step with Zerocopy.Proofs.Raw.advance_spec tail bytes elem code_positive as ⟨actual, actual_valid, actual_facts⟩ + step with reference_advance tail align phase bytes elem power phase_lt as ⟨expected, expected_facts⟩ + rw [view] at actual_facts + simp only [core.num.nonzero.NonZero.get, bind_ok] + change (Aeneas.Std.bind (advanceComparison tail align elem actual expected) _) ⦃ _ ⦄ + step with advance_comparison tail align phase bytes elem actual expected ⟨actual_valid, actual_facts⟩ expected_facts + as ⟨tail_copy, same, copy_eq, same_true⟩ + subst tail_copy + simp only [massert, same_true, if_true, bind_ok] + exact offset_and_padding_check tail align phase elems power phase_lt encoding + · simp only [WP.spec_ok] + +/- The original method theorem supplies equality for every natural-number +count. Here that stronger fact discharges a different executable observation: +independent checked Option sizes agree at the supplied machine-word count. +-/ +theorem tail_size_sequence_check (left right : layout.TrailingSliceLayout Usize) + (left_align : NonZeroUsize) (left_phase : Usize) + (right_align : NonZeroUsize) (right_phase elems : Usize) : + layout.tail_transform_checks.tail_size_sequence_check + left right left_align left_phase right_align right_phase elems ⦃ _ => True ⦄ := by + unfold layout.tail_transform_checks.tail_size_sequence_check + step with witness_matches left left_align left_phase as ⟨left_matches, left_facts⟩ + split + · rename_i left_true + obtain ⟨left_power, left_phase_lt, left_encoding⟩ := left_facts left_true + have left_positive := Nat.pos_of_isPowerOfTwo left_power + have left_code_positive : 0 < left.size_rounding_align_and_phase._0.val.val := by omega + have left_view := witness_view left left_align left_phase left_power left_phase_lt left_encoding + step with witness_matches right right_align right_phase as ⟨right_matches, right_facts⟩ + split + · rename_i right_true + obtain ⟨right_power, right_phase_lt, right_encoding⟩ := right_facts right_true + have right_positive := Nat.pos_of_isPowerOfTwo right_power + have right_code_positive : 0 < right.size_rounding_align_and_phase._0.val.val := by omega + have right_view := witness_view right right_align right_phase right_power right_phase_lt right_encoding + step with Zerocopy.Proofs.Raw.same_size_sequence_spec left right left_code_positive right_code_positive + as ⟨same_sequence, same_sequence_facts⟩ + split + · rename_i sequence_true + have sizes_equal := same_sequence_facts sequence_true elems.val + rw [left_view, right_view] at sizes_equal + step with reference_size left left_align left_phase elems left_positive as ⟨left_size, left_size_facts⟩ + step with reference_size right right_align right_phase elems right_positive as ⟨right_size, right_size_facts⟩ + have checked_equal : (witnessFormula left left_align left_phase).checkedSize Usize.max elems.val = + (witnessFormula right right_align right_phase).checkedSize Usize.max elems.val := by + simp only [LayoutMath.Formula.checkedSize, sizes_equal] + have sizes_same := optional_value_injective + (left_size_facts.trans (checked_equal.trans right_size_facts.symm)) + step with same_optional_usize left_size right_size as ⟨same, same_iff⟩ + simp [massert, same_iff.mpr sizes_same, WP.spec_ok] + · simp only [WP.spec_ok] + · simp only [WP.spec_ok] + · simp only [WP.spec_ok] + +/- The independent checked zero-size observation includes its None branch. +Overflow cannot be mistaken for no padding because a stored offset fits. +-/ +theorem tail_dynamic_padding_check (runtime_layout : layout.DstLayout) + (align : NonZeroUsize) (phase : Usize) : + layout.tail_transform_checks.tail_dynamic_padding_check runtime_layout align phase ⦃ _ => True ⦄ := by + unfold layout.tail_transform_checks.tail_dynamic_padding_check + cases info_eq : runtime_layout.size_info with + | Sized size => + step with Zerocopy.Proofs.Raw.requires_dynamic_padding_spec runtime_layout + (by simp only [info_eq]) as ⟨actual, actual_facts⟩ + simp only [info_eq] at actual_facts + have actual_false := actual_facts.mpr trivial + simp [actual_false, massert, WP.spec_ok] + | SliceDst tail => + step with witness_matches tail align phase as ⟨guard_result, guard_facts⟩ + split + · rename_i guard_true + obtain ⟨power, phase_lt, encoding⟩ := guard_facts guard_true + have positive := Nat.pos_of_isPowerOfTwo power + have code_positive : 0 < tail.size_rounding_align_and_phase._0.val.val := by omega + have view := witness_view tail align phase power phase_lt encoding + simp only [core.num.nonzero.NonZero.get, bind_ok] + step with Usize.rem_spec tail.elem_size (y := align.val) (by omega) + as ⟨stride_remainder, stride_value⟩ + step with reference_size tail align phase 0#usize positive as ⟨initial, initial_facts⟩ + step with same_optional_usize initial (some tail.offset) as ⟨zero_matches, zero_facts⟩ + have initial_iff : initial = some tail.offset ↔ + (witnessFormula tail align phase).size 0 = tail.offset.val := by + constructor + · intro equal + rw [equal] at initial_facts + exact (Zerocopy.Proofs.Raw.checked_some_size _ _ _ initial_facts).1.symm + · intro equal + apply optional_value_injective + rw [initial_facts] + simp only [LayoutMath.Formula.checkedSize, equal, word_bound tail.offset, if_true, + Option.map_some] + have no_dynamic_spec : + (if zero_matches then Result.ok (decide (stride_remainder = 0#usize)) else Result.ok false) ⦃ (b : Bool) => + b = true ↔ (witnessFormula tail align phase).size 0 = tail.offset.val ∧ + tail.elem_size.val % align.val.val = 0 ⦄ := by + cases zero_case : zero_matches with + | false => + have not_equal : ¬(witnessFormula tail align phase).size 0 = tail.offset.val := by + intro equal + have is_true := zero_facts.mpr (initial_iff.mpr equal) + rw [zero_case] at is_true + contradiction + simp [WP.spec_ok, not_equal] + | true => + have equal := initial_iff.mp (zero_facts.mp zero_case) + simp [WP.spec_ok, equal, UScalar.eq_equiv, stride_value] + step with no_dynamic_spec as ⟨no_dynamic, no_dynamic_facts⟩ + step with Zerocopy.Proofs.Raw.requires_dynamic_padding_spec runtime_layout + (by simpa only [info_eq] using code_positive) as ⟨actual, actual_facts⟩ + simp only [info_eq, view, witnessFormula] at actual_facts + cases actual <;> cases no_dynamic <;> simp_all [witnessFormula, massert, WP.spec_ok] + · simp only [WP.spec_ok] + +end Zerocopy.Proofs.Raw.TailTransforms + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem tail_transformations_check_spec : Specs.tail_transformations_check_spec := by + unfold Specs.tail_transformations_check_spec + intros + apply WP.spec_mono (Raw.TailTransforms.tail_transformations_check _ _ _ _ _ _) + intro result facts + exact ⟨(), rfl, trivial⟩ + +theorem tail_size_sequence_check_spec : Specs.tail_size_sequence_check_spec := by + unfold Specs.tail_size_sequence_check_spec + intros + apply WP.spec_mono (Raw.TailTransforms.tail_size_sequence_check _ _ _ _ _ _ _) + intro result facts + exact ⟨(), rfl, trivial⟩ + +theorem tail_dynamic_padding_check_spec : Specs.tail_dynamic_padding_check_spec := by + unfold Specs.tail_dynamic_padding_check_spec + intros + apply WP.spec_mono (Raw.TailTransforms.tail_dynamic_padding_check _ _ _) + intro result facts + exact ⟨(), rfl, trivial⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/TailTransformReference.lean b/verification/aeneas/lean/Proofs/TailTransformReference.lean new file mode 100644 index 0000000000..1246b0ce73 --- /dev/null +++ b/verification/aeneas/lean/Proofs/TailTransformReference.lean @@ -0,0 +1,209 @@ +/- 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 +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw.TailTransforms +open TailChecks +set_option linter.unusedVariables false +set_option linter.unusedSimpArgs false + +/- This guard exposes the exact stored alignment/phase witness. It adds no +physical-layout restriction and has coverage from encoding_witness_coverage. +-/ +theorem witness_matches (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase : Usize) : + layout.tail_transform_checks.witness_matches tail align phase ⦃ b => + b = true → align.val.val.isPowerOfTwo ∧ phase.val < align.val.val ∧ + tail.size_rounding_align_and_phase._0.val.val = align.val.val + phase.val ⦄ := by + unfold layout.tail_transform_checks.witness_matches + 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 + 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⟩ + rename_i matches_true + have same_code := matches_iff.mp matches_true + rw [same_code] at encoded_facts + exact ⟨power_fact, phase_lt, encoded_facts.2.1⟩ + · simp [WP.spec_ok] + · simp [WP.spec_ok] + +/- A representable power of two is at most half the word modulus. Thus two +alignment remainders can be added without overflow, even at the largest +compressed alignment. This is a derived machine-width fact, not a new guard. +-/ +theorem remainder_pair_fits (align : NonZeroUsize) (phase bytes : Usize) + (power : align.val.val.isPowerOfTwo) (phase_lt : phase.val < align.val.val) : + phase.val + bytes.val % align.val.val ≤ Usize.max := by + have positive := Nat.pos_of_isPowerOfTwo power + have remainder_lt := Nat.mod_lt bytes.val positive + have alignment_lt := UScalar.hSize align.val + obtain ⟨factor, modulus_eq⟩ := Arithmetic.alignment_dvd_size align.val power + have factor_ge : 2 ≤ factor := by + by_contra small + have cases : factor = 0 ∨ factor = 1 := by omega + rcases cases with zero | one + · simp only [zero, Nat.mul_zero] at modulus_eq + omega + · simp only [one, Nat.mul_one] at modulus_eq + omega + have half := Nat.mul_le_mul_left align.val.val factor_ge + rw [← modulus_eq] at half + have max_eq : Usize.max + 1 = UScalar.size .Usize := by + simp only [Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq, UScalar.size] + have positive := Nat.two_pow_pos System.Platform.numBits + omega + omega + +/- The reference splits bytes before adding phase, but preserves exactly the +natural-number normalized base and phase. Each None branch means that base, +and only that base, exceeds the machine-word maximum. +-/ +theorem reference_advance (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase bytes elem : Usize) + (power : align.val.val.isPowerOfTwo) (phase_lt : phase.val < align.val.val) : + layout.tail_transform_checks.reference_advance tail align phase bytes ⦃ result => + let next := (witnessFormula tail align phase).advance bytes.val elem.val + match result with + | none => Usize.max < next.base + | some (base, new_phase) => base.val = next.base ∧ + new_phase.val = next.phase ∧ next.base ≤ Usize.max ⦄ := by + have positive := Nat.pos_of_isPowerOfTwo power + have remainder_bound := Nat.mod_le bytes.val align.val.val + have sum_fits := remainder_pair_fits align phase bytes power phase_lt + have phase_mod : (phase.val + bytes.val % align.val.val) % align.val.val = + (phase.val + bytes.val) % align.val.val := by + rw [Nat.add_mod phase.val bytes.val, Nat.add_mod phase.val (bytes.val % align.val.val), + Nat.mod_mod] + have shifted_mod_le := Nat.mod_le (phase.val + bytes.val % align.val.val) align.val.val + have full_mod_le := Nat.mod_le (phase.val + bytes.val) align.val.val + unfold layout.tail_transform_checks.reference_advance + simp only [core.num.nonzero.NonZero.get, bind_ok] + step with Usize.rem_spec bytes (y := align.val) (by omega) as ⟨remainder, remainder_value⟩ + step with Usize.sub_spec (x := bytes) (y := remainder) (by omega) as ⟨whole, whole_value⟩ + step as ⟨shifted, shifted_facts⟩ + cases shifted with + | none => + simp only [] at shifted_facts + omega + | some shifted => + simp only [] at shifted_facts + step with Usize.rem_spec shifted (y := align.val) (by omega) as ⟨new_phase, new_phase_value⟩ + have phase_value : new_phase.val = (phase.val + bytes.val) % align.val.val := by + rw [new_phase_value, shifted_facts.2.1, remainder_value, phase_mod] + have carry_bound := Nat.mod_le shifted.val align.val.val + step with Usize.sub_spec (x := shifted) (y := new_phase) (by omega) as ⟨carry, carry_value⟩ + have normalized : tail.size_base.val + whole.val + carry.val = + ((witnessFormula tail align phase).advance bytes.val elem.val).base := by + simp only [witnessFormula, LayoutMath.Formula.advance] + omega + step as ⟨base, base_facts⟩ + cases base with + | none => + simp only [] at base_facts + simp only [WP.spec_ok] + omega + | some base => + simp only [] at base_facts + step as ⟨result, result_facts⟩ + cases result with + | none => + simp only [] at result_facts + simp only [WP.spec_ok] + omega + | some result => + simp only [] at result_facts + simp only [WP.spec_ok, witnessFormula, LayoutMath.Formula.advance] + exact ⟨by omega, phase_value, by omega⟩ + +/- Establish the same modular observation as the production padding method, +using full wrapped multiplication and quotient/remainder rounding instead of +its masked optimization. Modular cancellation later gives exact word equality. +-/ +theorem reference_wrapping_padding (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase elems : Usize) (power : align.val.val.isPowerOfTwo) : + layout.tail_transform_checks.reference_wrapping_padding tail align phase elems ⦃ result => + (result.val + tail.offset.val + elems.val * tail.elem_size.val) % UScalar.size .Usize = + (witnessFormula tail align phase).size elems.val % UScalar.size .Usize ⦄ := by + have positive := Nat.pos_of_isPowerOfTwo power + let trailing := core.num.Usize.wrapping_mul elems tail.elem_size + let input := core.num.Usize.wrapping_add phase trailing + have input_mod : input.val % align.val.val = + (phase.val + elems.val * tail.elem_size.val) % align.val.val := by + simp only [input, trailing, core.num.Usize.wrapping_add_val_eq, + core.num.Usize.wrapping_mul_val_eq] + rw [Nat.mod_mod_of_dvd _ (Arithmetic.alignment_dvd_size align.val power)] + rw [Nat.add_mod, Nat.mod_mod_of_dvd _ (Arithmetic.alignment_dvd_size align.val power), + ← Nat.add_mod] + have result_facts (padding : Usize) + (padding_value : padding.val = + (align.val.val - (phase.val + elems.val * tail.elem_size.val) % align.val.val) % align.val.val) : + let rounded := core.num.Usize.wrapping_add input padding + let complete := core.num.Usize.wrapping_add tail.size_base rounded + let slice_end := core.num.Usize.wrapping_add tail.offset trailing + ((core.num.Usize.wrapping_sub complete slice_end).val + tail.offset.val + + elems.val * tail.elem_size.val) % UScalar.size .Usize = + (witnessFormula tail align phase).size elems.val % UScalar.size .Usize := by + dsimp only + let complete := core.num.Usize.wrapping_add tail.size_base + (core.num.Usize.wrapping_add input padding) + let slice_end := core.num.Usize.wrapping_add tail.offset trailing + change ((core.num.Usize.wrapping_sub complete slice_end).val + tail.offset.val + + elems.val * tail.elem_size.val) % _ = _ + rw [Nat.add_assoc, Nat.add_mod, Nat.add_mod tail.offset.val, + ← core.num.Usize.wrapping_mul_val_eq] + change (((core.num.Usize.wrapping_sub complete slice_end).val) % _ + + ((tail.offset.val % _ + trailing.val) % _)) % _ = _ + have slice_value : (tail.offset.val % UScalar.size .Usize + trailing.val) % + UScalar.size .Usize = slice_end.val := by + simp only [slice_end, core.num.Usize.wrapping_add_val_eq, Nat.mod_add_mod] + rw [slice_value] + change (((core.num.Usize.wrapping_sub complete slice_end).val) % _ + slice_end.val) % _ = _ + rw [Nat.mod_eq_of_lt (UScalar.hSize (core.num.Usize.wrapping_sub complete slice_end)), + wrapping_sub_cancel] + simp only [complete, core.num.Usize.wrapping_add_val_eq, Nat.mod_add_mod, + input, trailing, core.num.Usize.wrapping_mul_val_eq, Nat.add_mod_mod, + witnessFormula, LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp, + padding_value] + unfold layout.tail_transform_checks.reference_wrapping_padding + simp only [lift, bind_ok, core.num.nonzero.NonZero.get] + change (do + let remainder ← input % align.val + let padding ← if remainder = 0#usize then Result.ok 0#usize else align.val - remainder + Result.ok (core.num.Usize.wrapping_sub + (core.num.Usize.wrapping_add tail.size_base (core.num.Usize.wrapping_add input padding)) + (core.num.Usize.wrapping_add tail.offset trailing))) ⦃ _ ⦄ + step with Usize.rem_spec input (y := align.val) (by omega) as ⟨remainder, remainder_value⟩ + change remainder.val = input.val % align.val.val at remainder_value + have remainder_lt := Nat.mod_lt input.val positive + simp only [UScalar.eq_equiv, UScalar.ofNatCore_val_eq] + split + · rename_i zero + simp only [bind_ok, WP.spec_ok] + apply result_facts + simp only [UScalar.ofNatCore_val_eq] + rw [← input_mod, ← remainder_value, zero, Nat.sub_zero, Nat.mod_self] + · rename_i nonzero + step with Usize.sub_spec (x := align.val) (y := remainder) (by omega) as ⟨padding, padding_value⟩ + apply result_facts + rw [← input_mod] + rw [Nat.mod_eq_of_lt (show align.val.val - input.val % align.val.val < align.val.val by omega)] + omega + +end Zerocopy.Proofs.Raw.TailTransforms diff --git a/verification/aeneas/lean/RequiredModelContracts/TailTransforms.lean b/verification/aeneas/lean/RequiredModelContracts/TailTransforms.lean new file mode 100644 index 0000000000..1b3aad2e73 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/TailTransforms.lean @@ -0,0 +1,72 @@ +/- 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.TailTransforms +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs +set_option linter.unusedVariables false + +@[contract_simps] theorem required_tail_transformations_check + (tail : layout.TrailingSliceLayout Usize) (align : NonZeroUsize) + (phase bytes replacement_stride elems : Usize) (run : Result Unit) + (provided : Specs.tail_transformations_check_spec_contract + tail align phase bytes replacement_stride elems run) : + Obligations.tail_transformations_check_spec_contract + tail align phase bytes replacement_stride elems run := by + intro positive align_positive + obtain ⟨tail_value, decoded_tail⟩ := + (trailing_valid_iff tail).mpr ⟨by simp, positive⟩ + 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 bytes) rfl + (unsignedWord replacement_stride) rfl (unsignedWord elems) rfl) + rintro result ⟨value, decoded, facts⟩ + trivial + +@[contract_simps] theorem required_tail_size_sequence_check + (left right : layout.TrailingSliceLayout Usize) + (left_align : NonZeroUsize) (left_phase : Usize) + (right_align : NonZeroUsize) (right_phase elems : Usize) (run : Result Unit) + (provided : Specs.tail_size_sequence_check_spec_contract + left right left_align left_phase right_align right_phase elems run) : + Obligations.tail_size_sequence_check_spec_contract + left right left_align left_phase right_align right_phase elems run := by + intro left_positive right_positive left_align_positive right_align_positive + obtain ⟨left_value, decoded_left⟩ := + (trailing_valid_iff left).mpr ⟨by simp, left_positive⟩ + obtain ⟨right_value, decoded_right⟩ := + (trailing_valid_iff right).mpr ⟨by simp, right_positive⟩ + let av : NonZeroUsizeValue := ⟨unsignedWord left_align.val, left_align_positive⟩ + let bv : NonZeroUsizeValue := ⟨unsignedWord right_align.val, right_align_positive⟩ + have decoded_a := (decodeNonZeroUScalar_iff left_align av).mpr rfl + have decoded_b := (decodeNonZeroUScalar_iff right_align bv).mpr rfl + apply WP.spec_mono (provided left_value decoded_left right_value decoded_right + av decoded_a (unsignedWord left_phase) rfl bv decoded_b + (unsignedWord right_phase) rfl (unsignedWord elems) rfl) + rintro result ⟨value, decoded, facts⟩ + trivial + +@[contract_simps] theorem required_tail_dynamic_padding_check + (runtime_layout : layout.DstLayout) (align : NonZeroUsize) (phase : Usize) + (run : Result Unit) + (provided : Specs.tail_dynamic_padding_check_spec_contract runtime_layout align phase run) : + Obligations.tail_dynamic_padding_check_spec_contract runtime_layout align phase run := by + intro valid_runtime align_positive + obtain ⟨layout_value, decoded_layout⟩ := (layout_valid_iff runtime_layout).mpr valid_runtime + let av : NonZeroUsizeValue := ⟨unsignedWord align.val, align_positive⟩ + have decoded_align := (decodeNonZeroUScalar_iff align av).mpr rfl + apply WP.spec_mono (provided layout_value decoded_layout av decoded_align (unsignedWord phase) rfl) + rintro result ⟨value, decoded, facts⟩ + trivial + +end Zerocopy.Proofs diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 9a35ca9bf9..ccdba15e57 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -201,6 +201,25 @@ spec size_for_elems_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.size_for_elems_spec for Zerocopy.layout.TrailingSliceLayoutUsize.size_for_elems with 2 +check_model_inputs Zerocopy.layout.TrailingSliceLayoutUsize.has_same_size_sequence with 0 type parameters +aeneas_spec_begin +spec same_size_sequence_spec + for @Zerocopy.layout.TrailingSliceLayoutUsize.has_same_size_sequence with 0 type parameters + ensures(raw) b => b = true → ∀ n : Nat, (trailingFormula self).size n = (trailingFormula other).size n +aeneas_spec_end +check_spec_binding Zerocopy.Specs.same_size_sequence_spec for Zerocopy.layout.TrailingSliceLayoutUsize.has_same_size_sequence with 2 + +check_model_inputs Zerocopy.layout.TrailingSliceLayoutUsize.advance with 0 type parameters +aeneas_spec_begin +spec advance_spec + for @Zerocopy.layout.TrailingSliceLayoutUsize.advance with 0 type parameters + ensures(raw) result => match result with + | none => Usize.max < ((trailingFormula self).advance bytes.val elem_size.val).base + | some t => trailingFormula t = (trailingFormula self).advance bytes.val elem_size.val ∧ + ((trailingFormula self).advance bytes.val elem_size.val).base ≤ Usize.max +aeneas_spec_end +check_spec_binding Zerocopy.Specs.advance_spec for Zerocopy.layout.TrailingSliceLayoutUsize.advance with 3 + check_model_inputs Zerocopy.layout.SizeInfoUsize.try_to_nonzero_elem_size with 0 type parameters aeneas_spec_begin spec try_nonzero_spec @@ -315,6 +334,17 @@ spec requires_static_padding_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.requires_static_padding_spec for Zerocopy.layout.DstLayout.requires_static_padding with 1 +check_model_inputs Zerocopy.layout.DstLayout.requires_dynamic_padding with 0 type parameters +aeneas_spec_begin +spec requires_dynamic_padding_spec + for @Zerocopy.layout.DstLayout.requires_dynamic_padding with 0 type parameters + ensures(raw) r => (r = false ↔ match self.size_info with + | .Sized _ => True + | .SliceDst tail => (trailingFormula tail).size 0 = tail.offset.val ∧ + tail.elem_size.val % (trailingFormula tail).align = 0) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.requires_dynamic_padding_spec for Zerocopy.layout.DstLayout.requires_dynamic_padding with 1 + check_model_inputs Zerocopy.layout.nested_reference.round_up with 0 type parameters aeneas_spec_begin spec nested_round_up_spec @@ -359,6 +389,30 @@ spec trailing_arithmetic_check_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.trailing_arithmetic_check_spec for Zerocopy.layout.tail_checks.trailing_arithmetic_check with 5 +check_model_inputs Zerocopy.layout.tail_transform_checks.tail_transformations_check with 0 type parameters +aeneas_spec_begin +spec tail_transformations_check_spec + for @Zerocopy.layout.tail_transform_checks.tail_transformations_check with 0 type parameters + ensures(raw) _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.tail_transformations_check_spec for Zerocopy.layout.tail_transform_checks.tail_transformations_check with 6 + +check_model_inputs Zerocopy.layout.tail_transform_checks.tail_size_sequence_check with 0 type parameters +aeneas_spec_begin +spec tail_size_sequence_check_spec + for @Zerocopy.layout.tail_transform_checks.tail_size_sequence_check with 0 type parameters + ensures(raw) _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.tail_size_sequence_check_spec for Zerocopy.layout.tail_transform_checks.tail_size_sequence_check with 7 + +check_model_inputs Zerocopy.layout.tail_transform_checks.tail_dynamic_padding_check with 0 type parameters +aeneas_spec_begin +spec tail_dynamic_padding_check_spec + for @Zerocopy.layout.tail_transform_checks.tail_dynamic_padding_check with 0 type parameters + ensures(raw) _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.tail_dynamic_padding_check_spec for Zerocopy.layout.tail_transform_checks.tail_dynamic_padding_check with 3 + check_model_inputs Zerocopy.pointer_metadata_unit_from_elem_count with 0 type parameters aeneas_spec_begin spec pointer_metadata_unit_from_elem_count_spec diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index dd46318db2..0f9eb5460a 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -21,6 +21,9 @@ mod tail_checks; #[allow(dead_code)] mod composition_checks; +#[allow(dead_code)] +mod tail_transform_checks; + use core::{mem, num::NonZeroUsize}; use crate::util; @@ -574,6 +577,11 @@ impl TrailingSliceLayout { && self.elem_size % other_align.get() == 0) || (self_align == other_align && self_phase == other_phase))) }))] + /// + /// ```aeneas + /// spec same_size_sequence_spec + /// ensures(raw) b => b = true → ∀ n : Nat, (trailingFormula self).size n = (trailingFormula other).size n + /// ``` pub(crate) const fn has_same_size_sequence(self, other: Self) -> bool { #[cfg(all(kani, kani_slow))] #[kani::proof_for_contract(TrailingSliceLayout::has_same_size_sequence)] @@ -687,6 +695,14 @@ impl TrailingSliceLayout { None => expected_offset.is_none(), } }))] + /// + /// ```aeneas + /// spec advance_spec + /// ensures(raw) result => match result with + /// | none => Usize.max < ((trailingFormula self).advance bytes.val elem_size.val).base + /// | some t => trailingFormula t = (trailingFormula self).advance bytes.val elem_size.val ∧ + /// ((trailingFormula self).advance bytes.val elem_size.val).base ≤ Usize.max + /// ``` const fn advance(self, bytes: usize, elem_size: usize) -> Option { #[cfg(all(kani, kani_slow))] #[kani::proof_for_contract(TrailingSliceLayout::advance)] @@ -1625,6 +1641,14 @@ impl DstLayout { || trailing.elem_size % trailing.size_rounding_align_and_phase.align().get() != 0 ), }))] + /// + /// ```aeneas + /// spec requires_dynamic_padding_spec + /// ensures(raw) r => (r = false ↔ match self.size_info with + /// | .Sized _ => True + /// | .SliceDst tail => (trailingFormula tail).size 0 = tail.offset.val ∧ + /// tail.elem_size.val % (trailingFormula tail).align = 0) + /// ``` pub const fn requires_dynamic_padding(self) -> bool { #[cfg(all(kani, kani_slow))] #[kani::proof_for_contract(DstLayout::requires_dynamic_padding)] diff --git a/zerocopy/src/layout/tail_transform_checks.rs b/zerocopy/src/layout/tail_transform_checks.rs new file mode 100644 index 0000000000..db7daed12e --- /dev/null +++ b/zerocopy/src/layout/tail_transform_checks.rs @@ -0,0 +1,188 @@ +// 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 layout transformations. +//! +//! Explicit alignment and phase witnesses bind the independent calculations +//! to the stored word. Every nonzero word has such witnesses. The references +//! use remainders and checked or wrapping arithmetic; they do not decode the +//! production representation or call its transformation helpers. + +// Explicit scalar reads and Option matches keep these arithmetic branches +// visible to reviewers and supported by the pinned Aeneas extraction. +#![allow(clippy::manual_map, clippy::needless_nonzero_get)] + +use core::num::NonZeroUsize; + +use super::{ + tail_checks::{reference_size, same_optional_usize}, + DstLayout, SizeInfo, TrailingSliceLayout, +}; + +fn witness_matches(tail: TrailingSliceLayout, align: NonZeroUsize, phase: usize) -> bool { + 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()), + ) +} + +#[allow(clippy::arithmetic_side_effects)] +fn reference_advance( + tail: TrailingSliceLayout, + align: NonZeroUsize, + phase: usize, + bytes: usize, +) -> Option<(usize, usize)> { + // Splitting first avoids overflowing phase + bytes when the normalized + // result still needs to be classified. Under the witness guard, adding + // the two remainders always fits. The checked base additions decide + // exactly whether the new normalized base fits in a machine word. + let remainder = bytes % align.get(); + let whole_bytes = bytes - remainder; + match phase.checked_add(remainder) { + None => None, + Some(shifted) => { + let new_phase = shifted % align.get(); + let carry = shifted - new_phase; + match tail.size_base.checked_add(whole_bytes) { + None => None, + Some(base) => match base.checked_add(carry) { + None => None, + Some(base) => Some((base, new_phase)), + }, + } + } + } +} + +#[allow(clippy::arithmetic_side_effects)] +fn reference_wrapping_padding( + tail: TrailingSliceLayout, + align: NonZeroUsize, + phase: usize, + elems: usize, +) -> usize { + // The complete padded size and physical slice end are both computed + // modulo the word size. Their wrapping difference remains meaningful + // even for overflowing sizes and offsets outside the complete object. + let trailing_bytes = elems.wrapping_mul(tail.elem_size); + let rounding_input = phase.wrapping_add(trailing_bytes); + let remainder = rounding_input % align.get(); + let padding = if remainder == 0 { 0 } else { align.get() - remainder }; + let rounded = rounding_input.wrapping_add(padding); + let complete = tail.size_base.wrapping_add(rounded); + let slice_end = tail.offset.wrapping_add(trailing_bytes); + complete.wrapping_sub(slice_end) +} + +/// Compare advance success/failure and every stored output field with an +/// independent normalized base and phase. Advancing preserves the physical +/// offset, installs the requested stride, and stores alignment + new phase. +/// Overflow must agree exactly, including near usize::MAX. +/// +/// Also compare the size offset with floor(base / alignment) * alignment + +/// phase, and compare wrapping padding with rounded size minus slice end. +/// No physical-layout, maximum-type-alignment, or signed-size bound is imposed. +/// +/// ```aeneas +/// spec tail_transformations_check_spec +/// ensures(raw) _ => True +/// ``` +fn tail_transformations_check( + tail: TrailingSliceLayout, + align: NonZeroUsize, + phase: usize, + bytes: usize, + replacement_stride: usize, + elems: usize, +) { + if witness_matches(tail, align, phase) { + let actual = tail.advance(bytes, replacement_stride); + let expected = reference_advance(tail, align, phase, bytes); + let same = match (actual, expected) { + (None, None) => true, + (Some(actual), Some((base, new_phase))) => { + actual.offset == tail.offset + && actual.elem_size == replacement_stride + && actual.size_base == base + && same_optional_usize( + align.get().checked_add(new_phase), + Some(actual.size_rounding_align_and_phase.0.get()), + ) + } + _ => false, + }; + assert!(same); + + #[allow(clippy::arithmetic_side_effects)] + let floor_base = tail.size_base - tail.size_base % align.get(); + assert!(same_optional_usize(Some(tail.size_offset()), floor_base.checked_add(phase))); + assert!( + tail.padding_for_elems(elems) == reference_wrapping_padding(tail, align, phase, elems) + ); + } +} + +/// A positive size-sequence comparison must imply equal independently +/// calculated Option sizes for any runtime element count. This checks the +/// complete result: equality of successful sizes and agreement on overflow. +/// The method's negative result makes no assertion about the sequences. +/// +/// ```aeneas +/// spec tail_size_sequence_check_spec +/// ensures(raw) _ => True +/// ``` +fn tail_size_sequence_check( + left: TrailingSliceLayout, + right: TrailingSliceLayout, + left_align: NonZeroUsize, + left_phase: usize, + right_align: NonZeroUsize, + right_phase: usize, + elems: usize, +) { + if witness_matches(left, left_align, left_phase) + && witness_matches(right, right_align, right_phase) + && left.has_same_size_sequence(right) + { + assert!(same_optional_usize( + reference_size(left, left_align, left_phase, elems), + reference_size(right, right_align, right_phase, elems), + )); + } +} + +/// Dynamic padding is absent exactly when the independent zero-element size +/// is the physical slice offset and the stride is alignment-divisible. A +/// zero-element size overflow therefore reports dynamic padding. Fixed-size +/// layouts never require dynamic padding. +/// +/// ```aeneas +/// spec tail_dynamic_padding_check_spec +/// ensures(raw) _ => True +/// ``` +fn tail_dynamic_padding_check(runtime_layout: DstLayout, align: NonZeroUsize, phase: usize) { + match runtime_layout.size_info { + SizeInfo::Sized { .. } => assert!(!runtime_layout.requires_dynamic_padding()), + SizeInfo::SliceDst(tail) => { + if witness_matches(tail, align, phase) { + #[allow(clippy::arithmetic_side_effects)] + let stride_remainder = tail.elem_size % align.get(); + let no_dynamic_padding = + same_optional_usize(reference_size(tail, align, phase, 0), Some(tail.offset)) + && stride_remainder == 0; + assert!(runtime_layout.requires_dynamic_padding() == !no_dynamic_padding); + } + } + } +}