diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 04ed772e40..80773da371 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -194,7 +194,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. Every present @@ -212,6 +212,8 @@ added without extending the specification set. | `DstLayout::requires_static_padding` | Exact negation of the recorded shallow-unpadded flag. | | Trailing size, padding, and capacity | Exact size-offset and capacity formulas, checked-size overflow, and wrapping padding; successful sizes and physical padding refine the independent recursive semantics. | | `DstLayout::{extend,pad_to_align}` | Exact field placement, alignment, padding flags, and normalized size formulas; outer padding preserves each field's complete inner size. | +| Trailing advancement and size-sequence comparison | Exact byte advancement; a positive comparison establishes equal sizes for every natural metadata value. | +| `DstLayout::requires_dynamic_padding` | Exact flag result and a mathematical condition sufficient to eliminate dynamic padding for all metadata values. | Every registered function uses total `spec`: accepted raw representations, supplied mathematical ghosts, and explicit requirements imply successful @@ -246,6 +248,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 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 4b4dc968db..bce9f0475f 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -951,7 +951,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 : @@ -967,14 +967,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 : @@ -992,7 +992,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) @@ -1166,7 +1166,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 @@ -1194,7 +1194,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) : @@ -1215,7 +1215,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 @@ -1340,7 +1340,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 @@ -1350,7 +1350,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) ← @@ -1360,7 +1360,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) : @@ -1389,7 +1389,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 @@ -1411,7 +1411,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) @@ -1434,8 +1434,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 @@ -1460,7 +1535,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 @@ -1477,7 +1552,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 : @@ -1492,13 +1567,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 @@ -1522,7 +1597,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 @@ -1541,7 +1616,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 @@ -1549,7 +1624,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 ← @@ -1575,12 +1650,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 46:0-56:1 -/ def layout.nested_reference.round_up @@ -1898,6 +1998,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 973:4-973:46 Visibility: public -/ diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 995d8e49aa..465d9bd59c 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -125,13 +125,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 @@ -139,14 +139,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.lean b/verification/aeneas/lean/Proofs.lean index 026aec8d1a..ca2345c17f 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -761,6 +761,164 @@ 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 + +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 packing_limit_spec (packed : Option NonZeroUsize) (hp : ∀ a ∈ packed, a.val.val.isPowerOfTwo) : (match packed with | none => layout.DstLayout.THEORETICAL_MAX_ALIGN | some a => Result.ok a) @@ -904,6 +1062,88 @@ 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] + /- Lift detailed raw extension facts to the independent fragment operation. This supplies the constructor loop's mathematical state transition. -/ @@ -1104,6 +1344,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 @@ -1176,11 +1426,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/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/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index e1366f7725..74427ad193 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); + } + } + } +}