diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 80773da371..5f167b5cb6 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -26,6 +26,13 @@ element-count conversion, layout-variant handling, and checked metadata sizing. Using these results for an arbitrary `KnownLayout` implementation requires separate layout correspondence. +The numerical harness in [`split_at.rs`](../../zerocopy/src/split_at.rs) compares +split sizes with the independent remainder-based reference. It checks physical +tail containment and the zero-padding gate. The shared length helper also runs +in the production pointer path. These proofs establish bounds and disjoint byte +intervals, including empty and zero-sized tails; pointer validity and provenance +remain separate Rust obligations. + These harnesses use the same annotation and proof rules as every other function. There is no root marker or separately maintained list of required functions. Every present specification must have its corresponding proof in both CI builds. diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index bce9f0475f..ba3b580415 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -2300,6 +2300,97 @@ def pointer_metadata_usize_size_for_metadata := do Usize.Insts.ZerocopyPointerMetadata.size_for_metadata metadata runtime_layout +/-- [zerocopy::split_at::split_right_len]: + Source: 'src/split_at.rs', lines 27:0-29:1 -/ +def split_at.split_right_len + (total : Std.Usize) (left : Std.Usize) : Result Std.Usize := do + total - left + +/-- [zerocopy::split_at::split_zero_padding]: + Source: 'src/split_at.rs', lines 39:0-41:1 -/ +def split_at.split_zero_padding (padding : Std.Usize) : Result Bool := do + ok (padding = 0#usize) + +/-- [zerocopy::split_at::numerical_checks::check_split_geometry]: + Source: 'src/split_at.rs', lines 68:4-126:5 -/ +def split_at.numerical_checks.check_split_geometry + (tail : layout.TrailingSliceLayout Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (total : Std.Usize) (left : Std.Usize) : + Result Unit + := do + let b ← layout.tail_transform_checks.witness_matches tail align phase + if b + then + if left > total + then ok () + else + let o ← layout.tail_checks.reference_size tail align phase total + match o with + | none => ok () + | some size => + let o1 ← lift (Usize.checked_mul total tail.elem_size) + match o1 with + | none => ok () + | some bytes => + let o2 ← lift (Usize.checked_add tail.offset bytes) + match o2 with + | none => ok () + | some «end» => + if «end» > size + then ok () + else + let o3 ← + layout.TrailingSliceLayoutUsize.size_for_elems tail total + let b1 ← layout.tail_checks.same_optional_usize o3 o + massert b1 + let o4 ← + layout.TrailingSliceLayoutUsize.size_for_elems tail left + let left_size ← core.option.Option.unwrap o4 + let o5 ← + layout.tail_checks.reference_size tail align phase left + let b2 ← + layout.tail_checks.same_optional_usize o5 (some left_size) + massert b2 + massert (left_size <= size) + let right ← split_at.split_right_len total left + let i ← right + left + massert (i = total) + let o6 ← lift (Usize.checked_mul left tail.elem_size) + let left_bytes ← core.option.Option.unwrap o6 + let o7 ← lift (Usize.checked_mul right tail.elem_size) + let right_bytes ← core.option.Option.unwrap o7 + let o8 ← lift (Usize.checked_add tail.offset left_bytes) + let right_start ← core.option.Option.unwrap o8 + let o9 ← lift (Usize.checked_add right_start right_bytes) + let right_end ← core.option.Option.unwrap o9 + massert (right_end = «end») + massert (right_end <= size) + let i1 ← + layout.TrailingSliceLayoutUsize.padding_for_elems tail left + let b3 ← split_at.split_zero_padding i1 + if b3 + then massert (left_size = right_start) + else ok () + let b4 ← + layout.DstLayout.requires_dynamic_padding + { + align, + size_info := (layout.SizeInfo.SliceDst tail), + statically_shallow_unpadded := false + } + if b4 + then ok () + else massert (left_size = right_start) + if left = total + then massert (right_bytes = 0#usize) + else ok () + if tail.elem_size = 0#usize + then massert (right_bytes = 0#usize) + else ok () + else ok () + /-- [zerocopy::util::bytewrite::exact]: Source: 'src/util/bytewrite/mod.rs', lines 27:0-37:1 -/ def util.bytewrite.exact diff --git a/verification/aeneas/lean/Obligations/Split.lean b/verification/aeneas/lean/Obligations/Split.lean new file mode 100644 index 0000000000..b3ccb6034f --- /dev/null +++ b/verification/aeneas/lean/Obligations/Split.lean @@ -0,0 +1,47 @@ +/- 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 + +-- Expected domains and observations are independent of inline specs. The +-- successful count subtraction has exactly the source's valid-index domain. +def split_right_len_spec_contract (total left : Usize) (run : Result Usize) : Prop := + left.val ≤ total.val → run ⦃ right => + right.val = total.val - left.val ∧ right.val + left.val = total.val ∧ + right.val ≤ total.val ⦄ + +def split_right_len_spec : Prop := ∀ total left, + split_right_len_spec_contract total left (split_at.split_right_len total left) + +-- Every machine padding value is admitted. Acceptance retains its exact gate. +def split_zero_padding_spec_contract (padding : Usize) (run : Result Bool) : Prop := + run ⦃ accepted => (accepted = true ↔ padding.val = 0) ⦄ + +def split_zero_padding_spec : Prop := ∀ padding, + split_zero_padding_spec_contract padding (split_at.split_zero_padding padding) + +-- Every positive stored layout word and positive witness alignment is admitted, +-- with arbitrary other fields and indices. The source guards reject mismatched +-- witnesses and nonrealizable/overflowing geometry before assertion sites. +def split_geometry_check_spec_contract (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase total left : Usize) (run : Result Unit) : Prop := + 0 < tail.size_rounding_align_and_phase._0.val.val → 0 < align.val.val → + run ⦃ _ => True ⦄ + +def split_geometry_check_spec : Prop := ∀ tail align phase total left, + split_geometry_check_spec_contract tail align phase total left + (split_at.numerical_checks.check_split_geometry tail align phase total left) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/Split.lean b/verification/aeneas/lean/Proofs/Split.lean new file mode 100644 index 0000000000..36ee1ea87f --- /dev/null +++ b/verification/aeneas/lean/Proofs/Split.lean @@ -0,0 +1,305 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Proofs +public import Proofs.TailReference +public import Proofs.TailTransformReference +public import SplitMath +public import RequiredModelContracts.Split +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw.Split +open Zerocopy.Proofs.Raw +open Zerocopy.Proofs.Raw.TailChecks +set_option linter.unusedVariables false +set_option linter.unusedSimpArgs false + +theorem right_len (total left : Usize) (index : left.val ≤ total.val) : + split_at.split_right_len total left ⦃ right => + right.val = total.val - left.val ∧ right.val + left.val = total.val ∧ + right.val ≤ total.val ⦄ := by + unfold split_at.split_right_len + step with Usize.sub_spec index as ⟨right, value, _⟩ + exact ⟨value, by omega, by omega⟩ + +theorem zero_padding (padding : Usize) : + split_at.split_zero_padding padding ⦃ accepted => (accepted = true ↔ padding.val = 0) ⦄ := by + simp [split_at.split_zero_padding, WP.spec_ok, UScalar.eq_equiv] + +/-- The actual modular padding computation supplies a sufficient boundary. +Both physical bytes and complete size are bounded, so congruence cannot hide +an overflow. No assumption about pointers enters this lemma. -/ +theorem padding_boundary (tail : layout.TrailingSliceLayout Usize) (left : Usize) + (positive : 0 < tail.size_rounding_align_and_phase._0.val.val) + (physical : tail.offset.val + left.val * tail.elem_size.val ≤ Usize.max) + (fits : (trailingFormula tail).size left.val ≤ Usize.max) : + layout.TrailingSliceLayoutUsize.padding_for_elems tail left ⦃ padding => + padding.val = 0 → (trailingFormula tail).size left.val = + tail.offset.val + left.val * tail.elem_size.val ⦄ := by + apply WP.spec_mono (padding_for_elems_spec tail left positive) + intro padding congruence zero + rw [zero, Nat.zero_add, word_mod_of_le _ physical, word_mod_of_le _ fits] at congruence + exact congruence.symm + + +/-- Execute the ordinary Rust root. Guards admit mismatched witnesses and +unrealizable descriptions without making assertions; fitting physical layouts +and valid indices reach all assertions, including zero strides and end splits. -/ +theorem geometry_check (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase total left : Usize) : + split_at.numerical_checks.check_split_geometry tail align phase total left ⦃ _ => True ⦄ := by + unfold split_at.numerical_checks.check_split_geometry + step with TailTransforms.witness_matches tail align phase as ⟨matched_gate, witness⟩ + split + · rename_i matched + obtain ⟨power, phase_lt, encoding⟩ := witness matched + have align_positive := Nat.pos_of_isPowerOfTwo power + have 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 [UScalar.lt_equiv] + split + · simp only [WP.spec_ok] + · rename_i not_out_of_bounds + have index : left.val ≤ total.val := by omega + step with reference_size tail align phase total align_positive as ⟨source, source_value⟩ + cases source with + | none => simp only [WP.spec_ok] + | some source => + simp only [Option.map_some] at source_value + rw [← view] at source_value + have source_facts := checked_some_size _ _ source source_value + step as ⟨tail_bytes, tail_bytes_facts⟩ + cases tail_bytes with + | none => simp only [WP.spec_ok] + | some tail_bytes => + simp only [] at tail_bytes_facts + step as ⟨tail_end, tail_end_facts⟩ + cases tail_end with + | none => simp only [WP.spec_ok] + | some tail_end => + simp only [] at tail_end_facts + simp only [UScalar.lt_equiv] + split + · simp only [WP.spec_ok] + · rename_i contained + have physical : tail.offset.val + total.val * tail.elem_size.val ≤ + (trailingFormula tail).size total.val := by omega + obtain ⟨count_total, right_count_bound, left_mono, left_fit, left_bytes_fit, + right_bytes_fit, left_physical, byte_sum_raw, end_contained⟩ := + SplitMath.split_bounds (trailingFormula tail) total.val left.val Usize.max + (trailing_align_pos tail) index physical source_facts.2 + change left.val * tail.elem_size.val ≤ Usize.max at left_bytes_fit + change (total.val - left.val) * tail.elem_size.val ≤ Usize.max at right_bytes_fit + change tail.offset.val + left.val * tail.elem_size.val ≤ Usize.max at left_physical + change tail.offset.val + left.val * tail.elem_size.val + + (total.val - left.val) * tail.elem_size.val = + tail.offset.val + total.val * tail.elem_size.val at byte_sum_raw + have byte_sum : tail.offset.val + left.val * tail.elem_size.val + + (total.val - left.val) * tail.elem_size.val = tail_end.val := by omega + step with size_for_elems_spec tail total positive as ⟨actual_source, actual_source_value⟩ + have source_same : actual_source = some source := optional_value_injective + (actual_source_value.trans source_value.symm) + step with same_optional_usize actual_source (some source) as ⟨same_source, same_source_iff⟩ + simp only [massert, same_source_iff.mpr source_same, if_true, bind_ok] + step with size_for_elems_spec tail left positive as ⟨left_option, left_value⟩ + cases left_option with + | none => + have overflow := checked_none_size _ _ left_value + omega + | some left_size => + simp only [Option.map_some] at left_value + have left_facts := checked_some_size _ _ left_size left_value + simp only [core.option.Option.unwrap, Result.ofOption, bind_ok] + step with reference_size tail align phase left align_positive as ⟨reference_left, reference_left_value⟩ + rw [← view] at reference_left_value + have left_same : reference_left = some left_size := optional_value_injective + (reference_left_value.trans left_value.symm) + step with same_optional_usize reference_left (some left_size) as ⟨same_left, same_left_iff⟩ + simp only [massert, same_left_iff.mpr left_same, if_true, bind_ok] + have left_below : left_size ≤ source := (UScalar.le_equiv _ _).mpr (by + omega) + simp only [massert, left_below, if_true, bind_ok] + step with right_len total left index as ⟨right, right_value, count_sum, right_below⟩ + step with Usize.add_spec (x := right) (y := left) + (by + have bound : total.val ≤ Usize.max := by scalar_tac + omega) as ⟨sum, sum_value⟩ + have sum_eq : sum = total := UScalar.eq_of_val_eq (by omega) + simp only [massert, sum_eq, if_true, bind_ok] + step as ⟨left_bytes, left_bytes_value⟩ + cases left_bytes with + | none => simp only [] at left_bytes_value; omega + | some left_bytes => + simp only [] at left_bytes_value + simp only [core.option.Option.unwrap, Result.ofOption, bind_ok] + step as ⟨right_bytes, right_bytes_value⟩ + cases right_bytes with + | none => + simp only [] at right_bytes_value + rw [right_value] at right_bytes_value + omega + | some right_bytes => + simp only [] at right_bytes_value + rw [right_value] at right_bytes_value + simp only [core.option.Option.unwrap, Result.ofOption, bind_ok] + step as ⟨right_start, right_start_value⟩ + cases right_start with + | none => simp only [] at right_start_value; omega + | some right_start => + simp only [] at right_start_value + simp only [core.option.Option.unwrap, Result.ofOption, bind_ok] + step as ⟨right_end, right_end_value⟩ + cases right_end with + | none => simp only [] at right_end_value; omega + | some right_end => + simp only [] at right_end_value + simp only [core.option.Option.unwrap, Result.ofOption, bind_ok] + have end_eq : right_end = tail_end := UScalar.eq_of_val_eq (by omega) + have end_below : tail_end ≤ source := (UScalar.le_equiv _ _).mpr (by omega) + simp only [massert, end_eq, end_below, if_true, bind_ok] + step with padding_boundary tail left positive left_physical left_fit + as ⟨padding, padding_zero⟩ + step with zero_padding padding as ⟨accepted, acceptance⟩ + have runtime_check : + (if accepted then massert (left_size = right_start) else Result.ok ()) + ⦃ _ => True ⦄ := by + split + · rename_i accepted_true + have boundary := padding_zero (acceptance.mp accepted_true) + have same : left_size = right_start := UScalar.eq_of_val_eq (by omega) + simp [massert, same, WP.spec_ok] + · simp [WP.spec_ok] + simp only [massert] at runtime_check + step with runtime_check + step with requires_dynamic_padding_spec + (⟨align, .SliceDst tail, false⟩ : layout.DstLayout) positive + as ⟨dynamic, dynamic_iff⟩ + have static_check : + (if dynamic then Result.ok () else massert (left_size = right_start)) + ⦃ _ => True ⦄ := by + cases dynamic with + | true => simp [WP.spec_ok] + | false => + have absent := dynamic_iff.mp rfl + have boundary := LayoutMath.no_dynamic_padding + (trailingFormula tail) absent.1 absent.2 left.val + change (trailingFormula tail).size left.val = + tail.offset.val + left.val * tail.elem_size.val at boundary + have same : left_size = right_start := UScalar.eq_of_val_eq (by omega) + simp [massert, same, WP.spec_ok] + simp only [massert] at static_check + step with static_check + have end_check : + (if left = total then massert (right_bytes = 0#usize) else Result.ok ()) + ⦃ _ => True ⦄ := by + split + · rename_i at_end + have same : right_bytes = 0#usize := UScalar.eq_of_val_eq (by + have values := congrArg UScalar.val at_end + simp only [values, Nat.sub_self, Nat.zero_mul] at right_bytes_value + simp only [UScalar.ofNatCore_val_eq] + omega) + simp [massert, same, WP.spec_ok] + · simp [WP.spec_ok] + simp only [massert] at end_check + step with end_check + split + · rename_i zst + have same : right_bytes = 0#usize := UScalar.eq_of_val_eq (by + have zero : tail.elem_size.val = 0 := by + simpa only [UScalar.eq_equiv, UScalar.ofNatCore_val_eq] using zst + simp only [zero, Nat.mul_zero] at right_bytes_value + simp only [UScalar.ofNatCore_val_eq] + omega) + simp [massert, same, WP.spec_ok] + · simp [WP.spec_ok] + · simp only [WP.spec_ok] + +/-- Apply the production runtime gate to the numerical split geometry. +No successful gate is replaced by a mathematical algorithm. -/ +theorem runtime_gate_disjoint (tail : layout.TrailingSliceLayout Usize) + (total left : Usize) (positive : 0 < tail.size_rounding_align_and_phase._0.val.val) + (index : left.val ≤ total.val) + (physical : tail.offset.val + total.val * tail.elem_size.val ≤ + (trailingFormula tail).size total.val) + (fits : (trailingFormula tail).size total.val ≤ Usize.max) : + (do + let padding ← layout.TrailingSliceLayoutUsize.padding_for_elems tail left + split_at.split_zero_padding padding) ⦃ accepted => accepted = true → + SplitMath.Disjoint ((trailingFormula tail).size left.val) + (tail.offset.val + left.val * tail.elem_size.val) + ((total.val - left.val) * tail.elem_size.val) ⦄ := by + obtain ⟨_, _, _, left_fit, _, _, start_fit, _, _⟩ := + SplitMath.split_bounds (trailingFormula tail) total.val left.val Usize.max + (trailing_align_pos tail) index physical fits + step with padding_boundary tail left positive start_fit left_fit + as ⟨padding, boundary⟩ + apply WP.spec_mono (zero_padding padding) + intro accepted gate accepted_true + exact SplitMath.runtime_disjoint (trailingFormula tail) total.val left.val + (boundary (gate.mp accepted_true)) + +/-- The actual layout decision proves disjointness at every split index. +This theorem is stronger numerically than just the fitting machine indices; +containment and arithmetic-fit follow separately from split_bounds. -/ +theorem static_gate_disjoint (runtime_layout : layout.DstLayout) + (tail : layout.TrailingSliceLayout Usize) + (tail_eq : runtime_layout.size_info = .SliceDst tail) + (positive : 0 < tail.size_rounding_align_and_phase._0.val.val) : + layout.DstLayout.requires_dynamic_padding runtime_layout + ⦃ dynamic => dynamic = false → ∀ total left : Nat, + SplitMath.Disjoint ((trailingFormula tail).size left) + (tail.offset.val + left * tail.elem_size.val) ((total - left) * tail.elem_size.val) ⦄ := by + have domain : match runtime_layout.size_info with + | .Sized _ => True + | .SliceDst t => 0 < t.size_rounding_align_and_phase._0.val.val := by + simpa only [tail_eq] using positive + apply WP.spec_mono (requires_dynamic_padding_spec runtime_layout domain) + intro dynamic gate absent total left + have properties := gate.mp absent + simp only [tail_eq] at properties + exact SplitMath.static_disjoint (trailingFormula tail) total left properties.1 properties.2 + +end Zerocopy.Proofs.Raw.Split + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem split_right_len_spec : Specs.split_right_len_spec := by + intro total left totalValue totalDecoded leftValue leftDecoded index + have totalSame := (decodeUScalar_iff total totalValue).mp totalDecoded + have leftSame := (decodeUScalar_iff left leftValue).mp leftDecoded + apply WP.spec_mono (Raw.Split.right_len total left (by + simpa only [← totalSame, ← leftSame] using index)) + intro right facts + refine ⟨unsignedWord right, rfl, ?_⟩ + dsimp only + rw [← totalSame, ← leftSame] + exact ⟨facts.2.1, facts.2.2⟩ +register_spec_step split_right_len_spec + +theorem split_zero_padding_spec : Specs.split_zero_padding_spec := by + intro padding paddingValue paddingDecoded + have same := (decodeUScalar_iff padding paddingValue).mp paddingDecoded + apply WP.spec_mono (Raw.Split.zero_padding padding) + intro accepted facts + refine ⟨accepted, rfl, ?_⟩ + simpa only [← same] using facts +register_spec_step split_zero_padding_spec + +theorem split_geometry_check_spec : Specs.split_geometry_check_spec := by + unfold Specs.split_geometry_check_spec + intros + apply WP.spec_mono (Raw.Split.geometry_check _ _ _ _ _) + intro result facts + exact ⟨(), rfl, trivial⟩ +register_spec_step split_geometry_check_spec + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/Split.lean b/verification/aeneas/lean/RequiredModelContracts/Split.lean new file mode 100644 index 0000000000..aeb9d5efe3 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/Split.lean @@ -0,0 +1,52 @@ +/- 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.Split +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +@[contract_simps] theorem required_split_right_len (total left : Usize) (run : Result Usize) + (provided : Specs.split_right_len_spec_contract total left run) : + Obligations.split_right_len_spec_contract total left run := by + intro index + apply WP.spec_mono (provided (unsignedWord total) rfl (unsignedWord left) rfl index) + rintro right ⟨value, decoded, count, bound⟩ + have same := (decodeUScalar_iff right value).mp decoded + change value.value + left.val = total.val at count + change value.value ≤ total.val at bound + rw [← same] at count bound + exact ⟨by omega, count, bound⟩ + +@[contract_simps] theorem required_split_zero_padding (padding : Usize) (run : Result Bool) + (provided : Specs.split_zero_padding_spec_contract padding run) : + Obligations.split_zero_padding_spec_contract padding run := by + apply WP.spec_mono (provided (unsignedWord padding) rfl) + rintro accepted ⟨value, decoded, fact⟩ + have same : value = accepted := by + symm + simpa only [RustModel.decode, modelBool, Option.some.injEq] using decoded + simpa only [same, unsignedWord] using fact + +@[contract_simps] theorem required_split_geometry_check (tail : layout.TrailingSliceLayout Usize) + (align : NonZeroUsize) (phase total left : Usize) (run : Result Unit) + (provided : Specs.split_geometry_check_spec_contract tail align phase total left run) : + Obligations.split_geometry_check_spec_contract tail align phase total left run := by + intro positive alignPositive + obtain ⟨tailValue, tailDecoded⟩ := (trailing_valid_iff tail).mpr ⟨by simp, positive⟩ + let av : NonZeroUsizeValue := ⟨unsignedWord align.val, alignPositive⟩ + have alignDecoded := (decodeNonZeroUScalar_iff align av).mpr rfl + apply WP.spec_mono (provided tailValue tailDecoded av alignDecoded + (unsignedWord phase) rfl (unsignedWord total) rfl (unsignedWord left) rfl) + intro result facts + trivial + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/SplitMath.lean b/verification/aeneas/lean/SplitMath.lean new file mode 100644 index 0000000000..68fecfa4fe --- /dev/null +++ b/verification/aeneas/lean/SplitMath.lean @@ -0,0 +1,97 @@ +/- 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 LayoutMath +@[expose] public section + +namespace Zerocopy.SplitMath +open LayoutMath + +/-- Half-open byte ranges [0, leftSize) and [rightStart, rightStart + rightBytes). +This definition includes empty ranges and contains no pointer assumptions. -/ +def Disjoint (leftSize rightStart rightBytes : Nat) : Prop := + ∀ byte, ¬ (byte < leftSize ∧ rightStart ≤ byte ∧ byte < rightStart + rightBytes) + +theorem disjoint_of_boundary (leftSize rightStart rightBytes : Nat) + (boundary : leftSize ≤ rightStart) : Disjoint leftSize rightStart rightBytes := by + intro byte overlap + omega + +theorem empty_right_disjoint (leftSize rightStart : Nat) : + Disjoint leftSize rightStart 0 := by + intro byte overlap + omega + +/-- Every count, product, sum and output length fits in the original byte +budget. The physical-tail premise is explicit because arbitrary Formula +records need not describe a realizable Rust layout. -/ +theorem split_bounds (f : Formula) (total left limit : Nat) + (positive : 0 < f.align) (index : left ≤ total) + (contains : f.offset + total * f.elem ≤ f.size total) + (fits : f.size total ≤ limit) : + (total - left) + left = total ∧ total - left ≤ total ∧ + f.size left ≤ f.size total ∧ f.size left ≤ limit ∧ + left * f.elem ≤ limit ∧ (total - left) * f.elem ≤ limit ∧ + f.offset + left * f.elem ≤ limit ∧ + f.offset + left * f.elem + (total - left) * f.elem = + f.offset + total * f.elem ∧ + f.offset + left * f.elem + (total - left) * f.elem ≤ f.size total := by + have counts : (total - left) + left = total := by omega + have mono := f.size_mono positive index + have leftBytes := Nat.mul_le_mul_right f.elem index + have rightBytes := Nat.mul_le_mul_right f.elem (show total - left ≤ total by omega) + have sumBytes : left * f.elem + (total - left) * f.elem = total * f.elem := by + rw [← Nat.add_mul, Nat.add_comm left, counts] + exact ⟨counts, by omega, mono, by omega, by omega, by omega, + by omega, by omega, by omega⟩ + +/-- Zero padding yields the shared boundary and therefore disjointness. +This is a sufficient condition, never asserted to be necessary. -/ +theorem runtime_disjoint (f : Formula) (total left : Nat) + (zero : f.size left = f.offset + left * f.elem) : + Disjoint (f.size left) (f.offset + left * f.elem) ((total - left) * f.elem) := by + apply disjoint_of_boundary + omega + +theorem static_disjoint (f : Formula) (total left : Nat) + (initial : f.size 0 = f.offset) (stride : f.elem % f.align = 0) : + Disjoint (f.size left) (f.offset + left * f.elem) ((total - left) * f.elem) := + runtime_disjoint f total left (no_dynamic_padding f initial stride left) + +/-- The exact recursive layout domain discharges physical containment for all +indices, including arbitrary nested packing and zero-sized elements. -/ +theorem compiled_split_bounds (d : Description) (valid : d.valid) + (total left limit : Nat) (index : left ≤ total) + (fits : d.compile.size total ≤ limit) : + (total - left) + left = total ∧ total - left ≤ total ∧ + d.compile.size left ≤ d.compile.size total ∧ d.compile.size left ≤ limit ∧ + left * d.compile.elem ≤ limit ∧ (total - left) * d.compile.elem ≤ limit ∧ + d.compile.offset + left * d.compile.elem ≤ limit ∧ + d.compile.offset + left * d.compile.elem + (total - left) * d.compile.elem = + d.compile.offset + total * d.compile.elem ∧ + d.compile.offset + left * d.compile.elem + (total - left) * d.compile.elem ≤ + d.compile.size total := + split_bounds d.compile total left limit (compile_valid d).1 index + (compiled_contains_tail d valid total) fits + +theorem zst_right_disjoint (f : Formula) (total left : Nat) (zst : f.elem = 0) : + Disjoint (f.size left) (f.offset + left * f.elem) ((total - left) * f.elem) := by + rw [zst, Nat.mul_zero] + exact empty_right_disjoint _ _ + +theorem end_split_disjoint (f : Formula) (total : Nat) : + Disjoint (f.size total) (f.offset + total * f.elem) ((total - total) * f.elem) := by + rw [Nat.sub_self, Nat.zero_mul] + exact empty_right_disjoint _ _ + +/-- Explicitly exhibit why zero padding must not be claimed necessary. -/ +theorem padded_empty_example : Disjoint 4 1 0 ∧ 4 ≠ 1 := + ⟨empty_right_disjoint 4 1, by decide⟩ + +end Zerocopy.SplitMath diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index 74427ad193..37a492aafd 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -16,13 +16,13 @@ mod nested_reference; mod primitive_checks; #[allow(dead_code)] -mod tail_checks; +pub(crate) mod tail_checks; #[allow(dead_code)] mod composition_checks; #[allow(dead_code)] -mod tail_transform_checks; +pub(crate) mod tail_transform_checks; use core::{mem, num::NonZeroUsize}; diff --git a/zerocopy/src/layout/tail_checks.rs b/zerocopy/src/layout/tail_checks.rs index 9706950641..2a0e616841 100644 --- a/zerocopy/src/layout/tail_checks.rs +++ b/zerocopy/src/layout/tail_checks.rs @@ -26,7 +26,7 @@ use core::num::NonZeroUsize; use super::TrailingSliceLayout; -pub(super) fn same_optional_usize(left: Option, right: Option) -> bool { +pub(crate) fn same_optional_usize(left: Option, right: Option) -> bool { match (left, right) { (Some(left), Some(right)) => left == right, (None, None) => true, @@ -41,7 +41,7 @@ fn reference_round_up(bytes: usize, align: NonZeroUsize) -> Option { bytes.checked_add(padding) } -pub(super) fn reference_size( +pub(crate) fn reference_size( tail: TrailingSliceLayout, align: NonZeroUsize, phase: usize, diff --git a/zerocopy/src/layout/tail_transform_checks.rs b/zerocopy/src/layout/tail_transform_checks.rs index db7daed12e..9d7a1f9885 100644 --- a/zerocopy/src/layout/tail_transform_checks.rs +++ b/zerocopy/src/layout/tail_transform_checks.rs @@ -27,7 +27,7 @@ use super::{ DstLayout, SizeInfo, TrailingSliceLayout, }; -fn witness_matches(tail: TrailingSliceLayout, align: NonZeroUsize, phase: usize) -> bool { +pub(crate) fn witness_matches(tail: TrailingSliceLayout, align: NonZeroUsize, phase: usize) -> bool { align.get().is_power_of_two() && phase < align.get() && same_optional_usize( diff --git a/zerocopy/src/pointer/inner.rs b/zerocopy/src/pointer/inner.rs index d926e1e520..eeef49f948 100644 --- a/zerocopy/src/pointer/inner.rs +++ b/zerocopy/src/pointer/inner.rs @@ -402,10 +402,9 @@ impl<'a, T> PtrInner<'a, [T]> { // trivially satisfied. let base = unsafe { base.add(range.start) }; - // SAFETY: The caller promises that `start <= end`, and so this will not - // underflow. - #[allow(unstable_name_collisions)] - let len = unsafe { range.end.unchecked_sub(range.start) }; + // The caller promises `start <= end`, which establishes the numerical + // precondition of `split_right_len` and prevents subtraction underflow. + let len = crate::split_at::split_right_len(range.end, range.start); let ptr = core::ptr::slice_from_raw_parts_mut(base, len); diff --git a/zerocopy/src/split_at.rs b/zerocopy/src/split_at.rs index 0a98c130d0..7f15e4f585 100644 --- a/zerocopy/src/split_at.rs +++ b/zerocopy/src/split_at.rs @@ -12,6 +12,164 @@ use super::*; use crate::pointer::invariant::{Aligned, Exclusive, Invariants, Safe, Shared}; +// These pure decisions are shared by the pointer operations and the executable +// numerical checks below. Their proofs concern counts and byte ranges only. +/// The number of elements remaining after a valid split index. +/// +/// ```aeneas +/// spec split_right_len_spec +/// requires hindex : (left : Nat) ≤ (total : Nat) +/// ensures right => (right : Nat) + (left : Nat) = (total : Nat) ∧ +/// (right : Nat) ≤ (total : Nat) +/// ``` +#[inline(always)] +#[allow(clippy::arithmetic_side_effects)] +pub(crate) fn split_right_len(total: usize, left: usize) -> usize { + total - left +} + +/// The runtime gate is sufficient for disjointness; an empty right range can +/// also be disjoint when the left part has padding. +/// +/// ```aeneas +/// spec split_zero_padding_spec +/// ensures accepted => (accepted = true ↔ (padding : Nat) = 0) +/// ``` +#[inline(always)] +pub(crate) fn split_zero_padding(padding: usize) -> bool { + padding == 0 +} + +// This is ordinary Rust, visible to extraction without entering pointer code. +// Numeric witnesses and checked reference sizes guard every assertion. The +// remainder-based reference lives with the existing trailing-layout checks. +#[allow(dead_code, clippy::needless_nonzero_get, clippy::arithmetic_side_effects)] +mod numerical_checks { + use core::num::NonZeroUsize; + + use crate::layout::{ + tail_checks::{reference_size, same_optional_usize}, + tail_transform_checks::witness_matches, + DstLayout, SizeInfo, TrailingSliceLayout, + }; + + /// Check valid split geometry against an independent remainder-based size + /// calculation. Nonmatching witnesses, overflow, and layouts whose complete + /// size does not contain their physical tail leave before the assertions. + /// Zero-sized elements and an empty right slice follow the same arithmetic. + /// The unwraps are assertions too: the proof must show that every guarded + /// arithmetic operation succeeds, rather than discard a failing case. + /// + /// ```aeneas + /// spec split_geometry_check_spec + /// ensures _ => True + /// ``` + #[allow(clippy::unwrap_used)] + fn check_split_geometry( + tail: TrailingSliceLayout, + align: NonZeroUsize, + phase: usize, + total: usize, + left: usize, + ) { + if !witness_matches(tail, align, phase) { + return; + } + if left > total { + return; + } + let source_size = match reference_size(tail, align, phase, total) { + Some(size) => size, + None => return, + }; + let tail_bytes = match total.checked_mul(tail.elem_size) { + Some(bytes) => bytes, + None => return, + }; + let tail_end = match tail.offset.checked_add(tail_bytes) { + Some(end) => end, + None => return, + }; + if tail_end > source_size { + return; + } + assert!(same_optional_usize(tail.size_for_elems(total), Some(source_size))); + let left_size = tail.size_for_elems(left).unwrap(); + assert!(same_optional_usize(reference_size(tail, align, phase, left), Some(left_size))); + assert!(left_size <= source_size); + let right = super::split_right_len(total, left); + assert!(right + left == total); + let left_bytes = left.checked_mul(tail.elem_size).unwrap(); + let right_bytes = right.checked_mul(tail.elem_size).unwrap(); + let right_start = tail.offset.checked_add(left_bytes).unwrap(); + let right_end = right_start.checked_add(right_bytes).unwrap(); + assert!(right_end == tail_end); + assert!(right_end <= source_size); + if super::split_zero_padding(tail.padding_for_elems(left)) { + assert!(left_size == right_start); + } + let layout = DstLayout { + align, + size_info: SizeInfo::SliceDst(tail), + statically_shallow_unpadded: false, + }; + if !layout.requires_dynamic_padding() { + assert!(left_size == right_start); + } + // An empty right byte range is disjoint regardless of left padding. + if left == total { + assert!(right_bytes == 0); + } + if tail.elem_size == 0 { + assert!(right_bytes == 0); + } + } + + #[cfg(test)] + mod tests { + use super::*; + use crate::layout::RoundingAlignAndPhase; + + #[test] + fn split_geometry_boundaries() { + for alignment in [1, 2, 8] { + let align = NonZeroUsize::new(alignment).unwrap(); + for phase in 0..alignment { + for stride in [0, 1, 2, 8] { + for offset in [0, phase, 5] { + let tail = TrailingSliceLayout { + offset, + elem_size: stride, + size_base: 5, + size_rounding_align_and_phase: RoundingAlignAndPhase::new( + align, phase, + ), + }; + for total in 0..16 { + for left in 0..17 { + check_split_geometry(tail, align, phase, total, left); + } + } + } + } + } + } + let align = NonZeroUsize::new(8).unwrap(); + let tail = TrailingSliceLayout { + offset: 1, + elem_size: 0, + size_base: 0, + size_rounding_align_and_phase: RoundingAlignAndPhase::new(align, 1), + }; + for left in [0, 1, usize::MAX] { + check_split_geometry(tail, align, 1, usize::MAX, left); + } + let overflowing = TrailingSliceLayout { elem_size: usize::MAX, ..tail }; + check_split_geometry(overflowing, align, 1, 2, 1); + } + } +} + /// Types that can be split in two. /// /// This trait generalizes Rust's existing support for splitting slices to @@ -1031,7 +1189,7 @@ where // FIXME(#1290): Once we require `KnownLayout` on all fields, add an // `IS_IMMUTABLE` associated const, and add `T::IS_IMMUTABLE ||` to the // below check. - if trailing_padding == 0 { + if split_zero_padding(trailing_padding) { // SAFETY: As established above, `trailing_padding` is the exact // padding after the left part's trailing slice. If it is zero, // the left and right parts are strictly non-overlapping. diff --git a/zerocopy/zerocopy-derive/tests/ui/struct.msrv.stderr b/zerocopy/zerocopy-derive/tests/ui/struct.msrv.stderr index ad2db50c39..b36b403d34 100644 --- a/zerocopy/zerocopy-derive/tests/ui/struct.msrv.stderr +++ b/zerocopy/zerocopy-derive/tests/ui/struct.msrv.stderr @@ -317,9 +317,9 @@ error[E0277]: the trait bound `SplitAtNotKnownLayout: zerocopy_renamed::KnownLay | ^^^^^^^ the trait `zerocopy_renamed::KnownLayout` is not implemented for `SplitAtNotKnownLayout` | note: required by a bound in `SplitAt` - --> $WORKSPACE/src/split_at.rs:97:27 + --> $WORKSPACE/src/split_at.rs:255:27 | -97 | pub unsafe trait SplitAt: KnownLayout { +255 | pub unsafe trait SplitAt: KnownLayout { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ required by this bound in `SplitAt` = note: this error originates in the derive macro `SplitAt` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/zerocopy/zerocopy-derive/tests/ui/struct.nightly.stderr b/zerocopy/zerocopy-derive/tests/ui/struct.nightly.stderr index 07e443a31b..f1d8e5dadf 100644 --- a/zerocopy/zerocopy-derive/tests/ui/struct.nightly.stderr +++ b/zerocopy/zerocopy-derive/tests/ui/struct.nightly.stderr @@ -484,7 +484,7 @@ help: the trait `zerocopy_renamed::KnownLayout` is not implemented for `SplitAtN $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `SplitAt` - --> src/split_at.rs:97:0 + --> src/split_at.rs:255:0 = note: this error originates in the derive macro `SplitAt` (in Nightly builds, run with -Z macro-backtrace for more info) error[E0277]: the trait bound `u8: SplitAt` is not satisfied @@ -502,10 +502,10 @@ help: the following other types implement trait `SplitAt` ... 363 | #[derive(SplitAt, KnownLayout)] | ^^^^^^^ `SplitAtSized` - --> src/split_at.rs:289:0 + --> src/split_at.rs:447:0 | = note: `[T]` - ::: src/split_at.rs:312:0 + ::: src/split_at.rs:470:0 | = note: `ManuallyDrop` = note: this error originates in the derive macro `SplitAt` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/zerocopy/zerocopy-derive/tests/ui/struct.stable.stderr b/zerocopy/zerocopy-derive/tests/ui/struct.stable.stderr index 1ae10d808c..fc6dd5ebee 100644 --- a/zerocopy/zerocopy-derive/tests/ui/struct.stable.stderr +++ b/zerocopy/zerocopy-derive/tests/ui/struct.stable.stderr @@ -428,7 +428,7 @@ help: the trait `zerocopy_renamed::KnownLayout` is not implemented for `SplitAtN $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `SplitAt` - --> src/split_at.rs:97:0 + --> src/split_at.rs:255:0 = note: this error originates in the derive macro `SplitAt` (in Nightly builds, run with -Z macro-backtrace for more info) error[E0277]: the trait bound `u8: SplitAt` is not satisfied @@ -446,10 +446,10 @@ help: the following other types implement trait `SplitAt` ... 363 | #[derive(SplitAt, KnownLayout)] | ^^^^^^^ `SplitAtSized` - --> src/split_at.rs:289:0 + --> src/split_at.rs:447:0 | = note: `[T]` - ::: src/split_at.rs:312:0 + ::: src/split_at.rs:470:0 | = note: `ManuallyDrop` = note: this error originates in the derive macro `SplitAt` (in Nightly builds, run with -Z macro-backtrace for more info)