diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 8f3f164ba5..6ca25098f7 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -781,7 +781,12 @@ records but does not formally prove: - The external `usize::unchecked_mul` and `usize::unchecked_add` models return the exact product and sum on non-overflowing inputs. Their Lean definitions use checked arithmetic, and every use proves both results fit. - They claim no Rust behavior outside that domain. + They claim no Rust behavior outside that domain. The cast composition + harness derives these bounds from successful plan selection and a + representable source size, and compares complete source/destination sizes + using the independent remainder-based reference. Pointer provenance, + reference validity, and `KnownLayout` implementations remain outside this + numerical proof. - Lean's kernel, its standard logic axioms, and the imported proof artifacts check the encoded propositions correctly. Release checksums establish artifact identity, not a proof of compiler or model correctness. @@ -849,3 +854,14 @@ checking its signature; no formatting proposition or behavior is assumed. A change to a proposition or a function fails the audit. The PhantomData model likewise records its zero runtime fields, with a Lean shape theorem that fails if extraction adds fields; it makes no ownership or provenance claim. + +## Numerical cast composition + +The inline checks in `layout/cast_from.rs` cover numerical cast composition. +They select a production `CastPlan`, require the checked metadata calculation +to succeed, compare it with the actual unchecked conversion, and compare +complete sizes using the independent remainder-based reference. Metadata +representability follows from a representable complete source size; it is not +an assumed harness precondition. The proof covers all three accepted plan +variants. Rejected plans carry no completeness promise, and the typed pointer +adapter's provenance and `KnownLayout` obligations remain outside this proof. diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md index cbfcd427de..9ebdc845bc 100644 --- a/verification/aeneas/SEMANTICS.md +++ b/verification/aeneas/SEMANTICS.md @@ -114,7 +114,12 @@ checked multiplication and addition. The correspondence premise is restricted to non-overflowing inputs: each call returns the exact natural-number result. No correspondence is claimed for overflowing inputs, where Rust's unchecked operations have undefined behavior. The arithmetic contracts prove both -intermediate results fit. +intermediate results fit; `cast_from::checks::assert_cast_preserves_size` +derives those bounds from an accepted plan and a representable complete source +size, rather than accepting them as harness preconditions. The root also checks +size preservation against the independent remainder-based reference. It +covers the numerical composition, not pointer provenance, reference validity, +or the `KnownLayout` implementation obligations at the pointer boundary. The remaining trusted boundary is the pinned Rust-to-LLBC-to-Lean translation, its builtin arithmetic and control-flow models, the external primitive diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index daeba92e69..42060c202d 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -1185,6 +1185,179 @@ def layout.cast_from.CastPlan.cast_metadata | layout.cast_from.CastPlan.SizedToUnsized dst_meta => ok dst_meta | layout.cast_from.CastPlan.SizedToSized => ok 0#usize +/-- [zerocopy::layout::tail_checks::same_optional_usize]: + Source: 'src/layout/tail_checks.rs', lines 29:0-35:1 -/ +def layout.tail_checks.same_optional_usize + (left : Option Std.Usize) (right : Option Std.Usize) : Result Bool := do + match left with + | none => match right with + | none => ok true + | some _ => ok false + | some left1 => + match right with + | none => ok false + | some right1 => ok (left1 = right1) + +/-- [zerocopy::layout::tail_transform_checks::witness_matches]: + Source: 'src/layout/tail_transform_checks.rs', lines 30:0-41: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::cast_from::checks::witness_matches]: + Source: 'src/layout/cast_from.rs', lines 369:4-374:5 -/ +def layout.cast_from.checks.witness_matches + (runtime_layout : layout.DstLayout) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : + Result Bool + := do + match runtime_layout.size_info with + | layout.SizeInfo.Sized _ => ok true + | layout.SizeInfo.SliceDst tail => + layout.tail_transform_checks.witness_matches tail align phase + +/-- [zerocopy::layout::tail_checks::reference_round_up]: + Source: 'src/layout/tail_checks.rs', lines 38:0-42:1 -/ +def layout.tail_checks.reference_round_up + (bytes : Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) : + Result (Option Std.Usize) + := do + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let remainder ← bytes % i + let padding ← if remainder = 0#usize + then ok 0#usize + else i - remainder + ok (Usize.checked_add bytes padding) + +/-- [zerocopy::layout::tail_checks::reference_size]: + Source: 'src/layout/tail_checks.rs', lines 44:0-60:1 -/ +def layout.tail_checks.reference_size + (tail : layout.TrailingSliceLayout Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (elems : Std.Usize) : + Result (Option Std.Usize) + := do + let o ← lift (Usize.checked_mul elems tail.elem_size) + match o with + | none => ok none + | some bytes => + let o1 ← lift (Usize.checked_add phase bytes) + match o1 with + | none => ok none + | some input => + let o2 ← layout.tail_checks.reference_round_up input align + match o2 with + | none => ok none + | some rounded => ok (Usize.checked_add tail.size_base rounded) + +/-- [zerocopy::layout::cast_from::checks::reference_size]: + Source: 'src/layout/cast_from.rs', lines 378:4-388:5 -/ +def layout.cast_from.checks.reference_size + (runtime_layout : layout.DstLayout) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (elems : Std.Usize) : + Result (Option Std.Usize) + := do + match runtime_layout.size_info with + | layout.SizeInfo.Sized size => ok (some size) + | layout.SizeInfo.SliceDst tail => + layout.tail_checks.reference_size tail align phase elems + +/-- [zerocopy::layout::cast_from::checks::checked_metadata]: + Source: 'src/layout/cast_from.rs', lines 390:4-401:5 -/ +def layout.cast_from.checks.checked_metadata + (plan : layout.cast_from.CastPlan) (src_meta : Std.Usize) : + Result (Option Std.Usize) + := do + match plan with + | layout.cast_from.CastPlan.UnsizedToUnsized offset_delta_elems elem_multiple + => + let o ← lift (Usize.checked_mul src_meta elem_multiple) + match o with + | none => ok none + | some scaled => ok (Usize.checked_add offset_delta_elems scaled) + | layout.cast_from.CastPlan.SizedToUnsized dst_meta => ok (some dst_meta) + | layout.cast_from.CastPlan.SizedToSized => ok (some 0#usize) + +/-- [zerocopy::layout::cast_from::checks::assert_cast_preserves_size]: + Source: 'src/layout/cast_from.rs', lines 423:4-458:5 -/ +def layout.cast_from.checks.assert_cast_preserves_size + (src : layout.DstLayout) (dst : layout.DstLayout) + (src_rounding_align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (src_phase : Std.Usize) + (dst_rounding_align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (dst_phase : Std.Usize) + (src_meta : Std.Usize) : + Result Unit + := do + let b ← + layout.cast_from.checks.witness_matches src src_rounding_align src_phase + if b + then + let b1 ← + layout.cast_from.checks.witness_matches dst dst_rounding_align dst_phase + if b1 + then + let o ← layout.cast_from.CastPlan.try_compute src dst + match o with + | none => ok () + | some plan => + let o1 ← + layout.cast_from.checks.reference_size src src_rounding_align + src_phase src_meta + match o1 with + | none => ok () + | some _ => + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + src.align + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + dst.align + massert (i >= i1) + let o2 ← layout.cast_from.checks.checked_metadata plan src_meta + match o2 with + | none => fail panic + | some «meta» => + let dst_meta ← + layout.cast_from.CastPlan.cast_metadata plan src_meta + massert (dst_meta = «meta») + let o3 ← + layout.cast_from.checks.reference_size dst dst_rounding_align + dst_phase dst_meta + let b2 ← layout.tail_checks.same_optional_usize o3 o1 + massert b2 + else ok () + else ok () + /-- [zerocopy::layout::composition_checks::matches_reference]: Source: 'src/layout/composition_checks.rs', lines 57:0-75:1 -/ def layout.composition_checks.matches_reference @@ -2123,58 +2296,6 @@ def layout.primitive_checks.check_empty_layout massert empty.statically_shallow_unpadded else ok () -/-- [zerocopy::layout::tail_checks::same_optional_usize]: - Source: 'src/layout/tail_checks.rs', lines 29:0-35:1 -/ -def layout.tail_checks.same_optional_usize - (left : Option Std.Usize) (right : Option Std.Usize) : Result Bool := do - match left with - | none => match right with - | none => ok true - | some _ => ok false - | some left1 => - match right with - | none => ok false - | some right1 => ok (left1 = right1) - -/-- [zerocopy::layout::tail_checks::reference_round_up]: - Source: 'src/layout/tail_checks.rs', lines 38:0-42:1 -/ -def layout.tail_checks.reference_round_up - (bytes : Std.Usize) - (align : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) : - Result (Option Std.Usize) - := do - let i ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align - let remainder ← bytes % i - let padding ← if remainder = 0#usize - then ok 0#usize - else i - remainder - ok (Usize.checked_add bytes padding) - -/-- [zerocopy::layout::tail_checks::reference_size]: - Source: 'src/layout/tail_checks.rs', lines 44:0-60:1 -/ -def layout.tail_checks.reference_size - (tail : layout.TrailingSliceLayout Std.Usize) - (align : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) - (elems : Std.Usize) : - Result (Option Std.Usize) - := do - let o ← lift (Usize.checked_mul elems tail.elem_size) - match o with - | none => ok none - | some bytes => - let o1 ← lift (Usize.checked_add phase bytes) - match o1 with - | none => ok none - | some input => - let o2 ← layout.tail_checks.reference_round_up input align - match o2 with - | none => ok none - | some rounded => ok (Usize.checked_add tail.size_base rounded) - /-- [zerocopy::layout::tail_checks::reference_capacity]: Source: 'src/layout/tail_checks.rs', lines 63:0-76:1 -/ def layout.tail_checks.reference_capacity @@ -2397,33 +2518,8 @@ def layout.tail_checks.layout_observations_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 -/ + Source: 'src/layout/tail_transform_checks.rs', lines 44:0-70:1 -/ def layout.tail_transform_checks.reference_advance (tail : layout.TrailingSliceLayout Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -2452,7 +2548,7 @@ def layout.tail_transform_checks.reference_advance | 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 -/ + Source: 'src/layout/tail_transform_checks.rs', lines 73:0-90:1 -/ def layout.tail_transform_checks.reference_wrapping_padding (tail : layout.TrailingSliceLayout Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -2478,7 +2574,7 @@ def layout.tail_transform_checks.reference_wrapping_padding 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 -/ + Source: 'src/layout/tail_transform_checks.rs', lines 105:0-138:1 -/ def layout.tail_transform_checks.tail_transformations_check (tail : layout.TrailingSliceLayout Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -2547,7 +2643,7 @@ def layout.tail_transform_checks.tail_transformations_check else ok () /-- [zerocopy::layout::tail_transform_checks::tail_size_sequence_check]: - Source: 'src/layout/tail_transform_checks.rs', lines 145:0-163:1 -/ + Source: 'src/layout/tail_transform_checks.rs', lines 149:0-167:1 -/ def layout.tail_transform_checks.tail_size_sequence_check (left : layout.TrailingSliceLayout Std.Usize) (right : layout.TrailingSliceLayout Std.Usize) @@ -2582,7 +2678,7 @@ def layout.tail_transform_checks.tail_size_sequence_check else ok () /-- [zerocopy::layout::tail_transform_checks::tail_dynamic_padding_check]: - Source: 'src/layout/tail_transform_checks.rs', lines 174:0-188:1 -/ + Source: 'src/layout/tail_transform_checks.rs', lines 178:0-192:1 -/ def layout.tail_transform_checks.tail_dynamic_padding_check (runtime_layout : layout.DstLayout) (align : core.num.nonzero.NonZero Std.Usize diff --git a/verification/aeneas/lean/CastMath.lean b/verification/aeneas/lean/CastMath.lean index cacc659a7c..b17e6b1805 100644 --- a/verification/aeneas/lean/CastMath.lean +++ b/verification/aeneas/lean/CastMath.lean @@ -41,4 +41,37 @@ theorem affine_size_of_advance (src dst : Formula) (offset multiple : Nat) (n : Nat) : src.size n = dst.size (offset + n * multiple) := by rw [hseq n, advance_affine_size src dst offset multiple n he] +/- A destination element occupies at least one byte. Hence its element count +cannot exceed its complete numerical size, regardless of rounding plateaus. +-/ +theorem Formula.metadata_le_size (f : Formula) (n : Nat) (he : 0 < f.elem) : + n ≤ f.size n := by + have hmul : n ≤ n * f.elem := by + simpa only [Nat.mul_one] using Nat.mul_le_mul_left n (show 1 ≤ f.elem by omega) + have hsize := f.size_lower_bound n + omega + +/- Size preservation bounds both unchecked metadata operations. The product +and sum are separately bounded so the result directly supplies their two +no-overflow preconditions. Source formula validity is unnecessary here. +-/ +theorem affine_metadata_bounds (src dst : Formula) (offset multiple n : Nat) + (hdst : 0 < dst.elem) + (hsize : src.size n = dst.size (offset + n * multiple)) : + n * multiple ≤ src.size n ∧ offset + n * multiple ≤ src.size n := by + have h := dst.metadata_le_size (offset + n * multiple) hdst + rw [← hsize] at h + omega + +/- A caller's object-size bound now bounds both arithmetic operations. The +limit is abstract so the lemma applies to isize::MAX or usize::MAX. +-/ +theorem affine_metadata_fits (src dst : Formula) (offset multiple n limit : Nat) + (hdst : 0 < dst.elem) + (hsize : src.size n = dst.size (offset + n * multiple)) + (hfit : src.size n ≤ limit) : + n * multiple ≤ limit ∧ offset + n * multiple ≤ limit := by + obtain ⟨hproduct, hsum⟩ := affine_metadata_bounds src dst offset multiple n hdst hsize + exact ⟨Nat.le_trans hproduct hfit, Nat.le_trans hsum hfit⟩ + end Zerocopy.LayoutMath diff --git a/verification/aeneas/lean/Obligations/CastComposition.lean b/verification/aeneas/lean/Obligations/CastComposition.lean new file mode 100644 index 0000000000..171c95f1a7 --- /dev/null +++ b/verification/aeneas/lean/Obligations/CastComposition.lean @@ -0,0 +1,36 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import LayoutModel +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations +open Zerocopy.Proofs +set_option linter.unusedVariables false + +/- This arbitrary-outcome expectation requires every harness assertion to +terminate throughout the automatic decoder domain. It includes no size-fit, +metadata-fit, witness-match, phase-range, or size-equality premise: the harness +itself guards the independent witnesses and derives metadata representability. +-/ +def cast_composition_check_spec_contract + (src dst : layout.DstLayout) (src_align : NonZeroUsize) (src_phase : Usize) + (dst_align : NonZeroUsize) (dst_phase src_meta : Usize) (run : Result Unit) : Prop := + 0 < src.align.val.val → 0 < dst.align.val.val → + canonicalLayout src → canonicalLayout dst → + 0 < src_align.val.val → 0 < dst_align.val.val → run ⦃ _ => True ⦄ + +def cast_composition_check_spec : Prop := + ∀ src dst src_align src_phase dst_align dst_phase src_meta, + cast_composition_check_spec_contract src dst src_align src_phase dst_align dst_phase src_meta + (layout.cast_from.checks.assert_cast_preserves_size + src dst src_align src_phase dst_align dst_phase src_meta) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/CastComposition.lean b/verification/aeneas/lean/Proofs/CastComposition.lean new file mode 100644 index 0000000000..4d0bc3d6b9 --- /dev/null +++ b/verification/aeneas/lean/Proofs/CastComposition.lean @@ -0,0 +1,171 @@ +/- 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.CastSelection +public import Proofs.CastArithmetic +public import Proofs.CastSafety +public import Proofs.TailTransformReference +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw.CastComposition +open TailChecks + +/- The layout guard is total and exposes the witness only when it succeeds. +Sized layouts intentionally ignore both witness values. +-/ +theorem witness_matches (self : layout.DstLayout) (align : NonZeroUsize) (phase : Usize) : + layout.cast_from.checks.witness_matches self align phase + ⦃ b => b = true → witnessMatches self align phase ⦄ := by + unfold layout.cast_from.checks.witness_matches + cases hs : self.size_info with + | Sized size => simp [witnessMatches, hs, WP.spec_ok] + | SliceDst tail => + simpa only [witnessMatches, hs] using TailTransforms.witness_matches tail align phase + +/- The independent remainder-based reference computes the mathematical +complete size, including overflow. Guarded witnesses identify its formula. +-/ +theorem reference_size (self : layout.DstLayout) (align : NonZeroUsize) + (phase elems : Usize) (positive : 0 < align.val.val) + (witness : witnessMatches self align phase) : + layout.cast_from.checks.reference_size self align phase elems + ⦃ result => result.map UScalar.val = checkedNat (completeLayoutSize self elems.val) ⦄ := by + unfold layout.cast_from.checks.reference_size + cases hs : self.size_info with + | Sized size => + have fits : size.val ≤ Usize.max := by scalar_tac + simp only [WP.spec_ok, Option.map_some, completeLayoutSize, hs, checkedNat, fits, if_true] + | SliceDst tail => + simp only [witnessMatches, hs] at witness + have view := witness_view tail align phase witness.1 witness.2.1 witness.2.2 + apply WP.spec_mono (TailChecks.reference_size tail align phase elems positive) + intro result facts + simpa only [completeLayoutSize, hs, view, LayoutMath.Formula.checkedSize, checkedNat] + using facts + +/- This independent checked implementation returns precisely the natural +metadata map when it fits, and none otherwise. Its intermediate product +cannot overflow while its nonnegative final sum fits. +-/ +theorem checked_metadata (plan : layout.cast_from.CastPlan) (src_meta : Usize) : + layout.cast_from.checks.checked_metadata plan src_meta + ⦃ result => result.map UScalar.val = checkedNat (castPlanMetadata plan src_meta.val) ⦄ := by + unfold layout.cast_from.checks.checked_metadata + cases plan with + | UnsizedToUnsized base multiple => + step as ⟨product, product_facts⟩ + cases product with + | none => + simp only [] at product_facts + have overflow : ¬base.val + src_meta.val * multiple.val ≤ Usize.max := by omega + simp [castPlanMetadata, checkedNat, overflow, WP.spec_ok] + | some product => + simp only [] at product_facts + have product_value : product.val = src_meta.val * multiple.val := by omega + simp only [WP.spec_ok, checked_add_value, castPlanMetadata, product_value] + | SizedToUnsized metadata => + have fits : metadata.val ≤ Usize.max := by scalar_tac + simp only [WP.spec_ok, Option.map_some, castPlanMetadata, checkedNat, fits, if_true] + | SizedToSized => + simp only [WP.spec_ok, Option.map_some, castPlanMetadata, checkedNat, Nat.zero_le, if_true] + rfl + +/- The root accepts arbitrary metadata and witness phases. Witness failures, +rejected plans and source-size overflow return normally. Once selection and +source sizing succeed, the certificate itself supplies the metadata bound; +metadata overflow is then impossible, and both final assertions follow. +-/ +theorem assert_cast_preserves_size (src dst : layout.DstLayout) + (src_align : NonZeroUsize) (src_phase : Usize) + (dst_align : NonZeroUsize) (dst_phase src_meta : Usize) + (hsa : 0 < src.align.val.val) (hda : 0 < dst.align.val.val) + (hsc : canonicalLayout src) (hdc : canonicalLayout dst) + (hsrc_align : 0 < src_align.val.val) (hdst_align : 0 < dst_align.val.val) : + layout.cast_from.checks.assert_cast_preserves_size + src dst src_align src_phase dst_align dst_phase src_meta ⦃ _ => True ⦄ := by + unfold layout.cast_from.checks.assert_cast_preserves_size + step with witness_matches src src_align src_phase as ⟨src_matches, src_witness⟩ + split + · rename_i src_matches_true + have src_witness := src_witness src_matches_true + step with witness_matches dst dst_align dst_phase as ⟨dst_matches, dst_witness⟩ + split + · rename_i dst_matches_true + have dst_witness := dst_witness dst_matches_true + step with Raw.cast_plan_spec src dst hsa hda hsc hdc as ⟨selected, selected_facts⟩ + cases selected with + | none => simp only [WP.spec_ok] + | some plan => + step with reference_size src src_align src_phase src_meta hsrc_align src_witness + as ⟨src_size, src_size_facts⟩ + cases src_size with + | none => simp only [WP.spec_ok] + | some src_size => + simp only [Option.map_some] at src_size_facts + have source := (checkedNat_some _ _).mp src_size_facts.symm + have fits := castPlanSpec_metadata_fits src dst plan selected_facts src_meta.val source.1 + have alignment := castPlanSpec_alignment src dst plan selected_facts + have alignment_raw : src.align.val ≥ dst.align.val := by scalar_tac + simp only [core.num.nonzero.NonZero.get, bind_ok, alignment_raw, + massert, if_true] + step with checked_metadata plan src_meta as ⟨expected, expected_facts⟩ + cases expected with + | none => + simp only [Option.map_none] at expected_facts + have overflow := (checkedNat_none _).mp expected_facts.symm + unfold castMetadataFits at fits + omega + | some expected => + simp only [Option.map_some] at expected_facts + have expected_value := (checkedNat_some _ _).mp expected_facts.symm + step with Raw.cast_metadata_spec plan src_meta fits as ⟨dst_meta, dst_meta_value⟩ + have metadata_same : dst_meta = expected := + UScalar.eq_of_val_eq (dst_meta_value.trans expected_value.2) + simp only [metadata_same, if_true, bind_ok] + step with reference_size dst dst_align dst_phase expected hdst_align dst_witness + as ⟨dst_size, dst_size_facts⟩ + have same_size := castPlanSpec_size src dst plan selected_facts src_meta.val + rw [expected_value.2] at same_size + have same : dst_size = some src_size := by + apply optional_value_injective + rw [dst_size_facts, ← same_size] + exact src_size_facts.symm + step with same_optional_usize dst_size (some src_size) as ⟨same_result, same_iff⟩ + simp [same_iff.mpr same, WP.spec_ok] + · simp only [WP.spec_ok] + · simp only [WP.spec_ok] + +end Zerocopy.Proofs.Raw.CastComposition + +namespace Zerocopy.Proofs +open AeneasSpecs + +/- The canonical contract exposes exactly the automatic decoder domain. It +adds no source-size, metadata-fit, phase-range, or size-equality requirement. +-/ +theorem cast_composition_check_spec : Specs.cast_composition_check_spec := by + unfold Specs.cast_composition_check_spec + representation_simps + intro src dst src_align src_phase dst_align dst_phase src_meta hsrc hdst hsrc_align hdst_align + have hcsrc : canonicalLayout src := by + cases hs : src.size_info with + | Sized _ => simp only [canonicalLayout, hs] + | SliceDst _ => simpa only [canonicalLayout, hs] using hsrc.2 + have hcdst : canonicalLayout dst := by + cases hs : dst.size_info with + | Sized _ => simp only [canonicalLayout, hs] + | SliceDst _ => simpa only [canonicalLayout, hs] using hdst.2 + apply WP.spec_mono (Raw.CastComposition.assert_cast_preserves_size src dst src_align src_phase + dst_align dst_phase src_meta hsrc.1 hdst.1 hcsrc hcdst hsrc_align hdst_align) + intro result _facts + exact ⟨(), rfl⟩ +register_spec_step cast_composition_check_spec + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/CastSafety.lean b/verification/aeneas/lean/Proofs/CastSafety.lean new file mode 100644 index 0000000000..3fe8db89e2 --- /dev/null +++ b/verification/aeneas/lean/Proofs/CastSafety.lean @@ -0,0 +1,62 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import LayoutModel +public import CastMath +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs + +/- A successful selector certificate retains the alignment ordering directly. +No additional layout validity premise is needed to project that fact. +-/ +theorem castPlanSpec_alignment (src dst : layout.DstLayout) + (plan : layout.cast_from.CastPlan) + (hplan : castPlanSpec src dst (some plan)) : + dst.align.val.val ≤ src.align.val.val := hplan.1 + +/- Variant compatibility in the certificate rules out the nine unsupported +combinations. Each supported variant preserves complete size for every natural +source count; this is independent of machine representability. +-/ +theorem castPlanSpec_size (src dst : layout.DstLayout) + (plan : layout.cast_from.CastPlan) + (hplan : castPlanSpec src dst (some plan)) (count : Nat) : + completeLayoutSize src count = + completeLayoutSize dst (castPlanMetadata plan count) := by + cases hs : src.size_info <;> cases hd : dst.size_info <;> cases plan <;> + simp only [castPlanSpec, hs, hd, and_false] at hplan <;> try contradiction + all_goals simp only [completeLayoutSize, hs, hd, castPlanMetadata] + · rw [hplan.2] + · exact hplan.2.2.symm + · exact hplan.2.2.2 count + +/- A fitting complete source size bounds the numerical metadata map. For an +affine plan, affine_metadata_fits supplies both its product and sum bounds; +the sum is precisely castMetadataFits. Destination-stride positivity is +already retained by the certificate, rather than assumed by this theorem. +-/ +theorem castPlanSpec_metadata_fits (src dst : layout.DstLayout) + (plan : layout.cast_from.CastPlan) + (hplan : castPlanSpec src dst (some plan)) (count : Nat) + (hfit : completeLayoutSize src count ≤ Usize.max) : + castMetadataFits plan count := by + cases hs : src.size_info <;> cases hd : dst.size_info <;> cases plan <;> + simp only [castPlanSpec, hs, hd, and_false] at hplan <;> try contradiction + all_goals simp only [completeLayoutSize, hs] at hfit + all_goals simp only [castMetadataFits, castPlanMetadata] + · exact Nat.zero_le _ + · apply Nat.le_trans ((trailingFormula _).metadata_le_size _ hplan.2.1) + rw [hplan.2.2] + exact hfit + · exact (LayoutMath.affine_metadata_fits _ _ _ _ count Usize.max + hplan.2.1 (hplan.2.2.2 count) hfit).2 + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/CastComposition.lean b/verification/aeneas/lean/RequiredModelContracts/CastComposition.lean new file mode 100644 index 0000000000..5f8e128059 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/CastComposition.lean @@ -0,0 +1,41 @@ +/- 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 Obligations.CastComposition +public import RequiredModelContracts.CastPlan +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +/- Recover all decoder witnesses from the independently stated raw domain, +then consume the supplied contract for the same arbitrary execution outcome. +This adapter does not use the implementation proof or execute the harness. +-/ +@[contract_simps] theorem required_cast_composition_check + (src dst : layout.DstLayout) (src_align : NonZeroUsize) (src_phase : Usize) + (dst_align : NonZeroUsize) (dst_phase src_meta : Usize) (run : Result Unit) + (provided : Specs.cast_composition_check_spec_contract + src dst src_align src_phase dst_align dst_phase src_meta run) : + Obligations.cast_composition_check_spec_contract + src dst src_align src_phase dst_align dst_phase src_meta run := by + intro src_positive dst_positive src_canonical dst_canonical src_align_positive dst_align_positive + obtain ⟨src_value, src_decoded⟩ := layout_admitted_of_canonical src src_positive src_canonical + obtain ⟨dst_value, dst_decoded⟩ := layout_admitted_of_canonical dst dst_positive dst_canonical + let src_align_value : NonZeroUsizeValue := ⟨unsignedWord src_align.val, src_align_positive⟩ + let dst_align_value : NonZeroUsizeValue := ⟨unsignedWord dst_align.val, dst_align_positive⟩ + have src_align_decoded := (decodeNonZeroUScalar_iff src_align src_align_value).mpr rfl + have dst_align_decoded := (decodeNonZeroUScalar_iff dst_align dst_align_value).mpr rfl + apply WP.spec_mono (provided src_value src_decoded dst_value dst_decoded + src_align_value src_align_decoded (unsignedWord src_phase) rfl + dst_align_value dst_align_decoded (unsignedWord dst_phase) rfl (unsignedWord src_meta) rfl) + rintro result ⟨_value, _decoded, _facts⟩ + trivial + +end Zerocopy.Proofs diff --git a/zerocopy/src/layout/cast_from.rs b/zerocopy/src/layout/cast_from.rs index 11f9ea2cd7..5d9daf8f1f 100644 --- a/zerocopy/src/layout/cast_from.rs +++ b/zerocopy/src/layout/cast_from.rs @@ -291,56 +291,14 @@ impl CastParams }; // SAFETY: The sized variants perform no unchecked arithmetic. - // For `UnsizedToUnsized`, `self.plan` was selected for the layouts and - // witnesses that this affine map makes `Src` and `Dst`'s complete - // rounded size formulas equal for every source metadata value. - // Interpret the arithmetic in this proof over the - // mathematical nonnegative integers. Since the - // caller promises that `src_meta` is valid `Src` - // metadata, the source object size `src_size` it - // describes is at most `isize::MAX`. Let - // `src_elem_size` and `dst_elem_size` be the - // respective trailing-slice element sizes. Then: - // - // src_meta * src_elem_size - // <= src_size <= isize::MAX. - // - // Since `elem_multiple` is the exact ratio - // `src_elem_size / dst_elem_size` and - // `dst_elem_size >= 1`, - // - // src_meta * elem_multiple - // <= src_meta * src_elem_size - // <= isize::MAX <= usize::MAX. - // - // Thus `scaled_elems = src_meta * elem_multiple` - // is representable, and its byte contribution is - // `scaled_elems * dst_elem_size = src_meta * - // src_elem_size`. Let `base_bytes = - // offset_delta_elems * dst_elem_size`. - // `size_sequences_match` compares the source - // formula with the destination formula advanced by - // `base_bytes`. The latter's unrounded term - // contains `base_bytes + src_meta * src_elem_size`, - // and its complete size is at least that large - // (formally checked by Kani in - // `prove_size_formula_bounds_size_offset`). - // Sequence equality therefore gives, over the - // mathematical nonnegative integers, - // - // base_bytes + src_meta * src_elem_size - // = (offset_delta_elems + scaled_elems) - // * dst_elem_size - // <= src_size. - // - // Since `dst_elem_size >= 1`, the metadata sum - // `offset_delta_elems + scaled_elems` is also at - // most `src_size`, and thus at most `isize::MAX <= - // usize::MAX`. The sum is therefore representable, - // and the returned metadata describes a `Dst` of - // the same size. - // SAFETY: The bounds above establish the helper's - // complete no-overflow precondition. + // For the affine variant, the selected plan makes the complete source + // and destination sizes equal and has a positive destination stride. + // Destination size is at least metadata * stride, so the complete + // metadata sum is at most source size. The multiplication's result is + // no larger than that sum. Both therefore fit usize, since the caller + // bounds source size by isize::MAX. The assertions in + // checks::assert_cast_preserves_size prove this numerical composition + // against the independent remainder-based size calculation. let dst_meta = unsafe { self.plan.cast_metadata(src_meta) }; Dst::PointerMetadata::from_elem_count(dst_meta) } @@ -398,3 +356,152 @@ where ::raw_from_ptr_len(src.as_non_null().cast(), dst_meta).as_ptr() } } + +// Keep the numerical proof harness next to the pointer adapter it justifies. +// The harness uses no pointers. Its assertion safety proves the size and +// arithmetic part of the adapter's safety argument; pointer construction, +// provenance, and the KnownLayout contract remain separate obligations. +#[allow(dead_code, clippy::manual_map, clippy::needless_nonzero_get)] +mod checks { + use super::{CastPlan, DstLayout, NonZeroUsize, SizeInfo}; + use crate::layout::{tail_checks, tail_transform_checks}; + + fn witness_matches(runtime_layout: DstLayout, align: NonZeroUsize, phase: usize) -> bool { + match runtime_layout.size_info { + SizeInfo::Sized { .. } => true, + SizeInfo::SliceDst(tail) => tail_transform_checks::witness_matches(tail, align, phase), + } + } + + // This calculation uses explicit alignment/phase witnesses and the simple + // remainder-based reference. It does not call the production size formula. + fn reference_size( + runtime_layout: DstLayout, + align: NonZeroUsize, + phase: usize, + elems: usize, + ) -> Option { + match runtime_layout.size_info { + SizeInfo::Sized { size } => Some(size), + SizeInfo::SliceDst(tail) => tail_checks::reference_size(tail, align, phase, elems), + } + } + + fn checked_metadata(plan: CastPlan, src_meta: usize) -> Option { + match plan { + CastPlan::UnsizedToUnsized { offset_delta_elems, elem_multiple } => { + match src_meta.checked_mul(elem_multiple) { + Some(scaled) => offset_delta_elems.checked_add(scaled), + None => None, + } + } + CastPlan::SizedToUnsized { dst_meta } => Some(dst_meta), + CastPlan::SizedToSized => Some(0), + } + } + + /// Every selected plan preserves the complete object size and alignment + /// requirement. For a representable source size, its metadata arithmetic + /// must fit, and its unchecked implementation must agree with checked + /// arithmetic. Both source and destination sizes use the independent + /// remainder-based reference calculation. + /// + /// The witness guards identify the compressed alignment/phase encoding; + /// every valid encoding has witnesses. Rejected plans and unrepresentable + /// source sizes impose no claim. In particular, overflow of *metadata* + /// after an accepted plan and representable source size is an assertion + /// failure, rather than an input exclusion. + /// + /// Rust objects have the stronger size bound of isize::MAX. Proving this + /// for every size fitting usize therefore covers that numerical domain. + /// The harness does not model pointer provenance or construct references. + /// + /// ```aeneas + /// spec cast_composition_check_spec + /// ensures(raw) _ => True + /// ``` + fn assert_cast_preserves_size( + src: DstLayout, + dst: DstLayout, + src_rounding_align: NonZeroUsize, + src_phase: usize, + dst_rounding_align: NonZeroUsize, + dst_phase: usize, + src_meta: usize, + ) { + if !witness_matches(src, src_rounding_align, src_phase) + || !witness_matches(dst, dst_rounding_align, dst_phase) + { + return; + } + let plan = match CastPlan::try_compute(&src, &dst) { + Some(plan) => plan, + None => return, + }; + let src_size = match reference_size(src, src_rounding_align, src_phase, src_meta) { + Some(size) => size, + None => return, + }; + assert!(src.align.get() >= dst.align.get()); + let expected_meta = match checked_metadata(plan, src_meta) { + Some(meta) => meta, + None => panic!("selected cast metadata overflowed"), + }; + // SAFETY: The preceding checked calculation establishes that both + // the multiplication and addition required by cast_metadata fit. + let dst_meta = unsafe { plan.cast_metadata(src_meta) }; + assert!(dst_meta == expected_meta); + assert!(tail_checks::same_optional_usize( + reference_size(dst, dst_rounding_align, dst_phase, dst_meta), + Some(src_size), + )); + } + + #[cfg(test)] + mod tests { + use super::*; + use crate::layout::{RoundingAlignAndPhase, TrailingSliceLayout}; + + #[test] + fn selected_cast_composition() { + let one = NonZeroUsize::new(1).unwrap(); + let four = NonZeroUsize::new(4).unwrap(); + let sized = DstLayout { + align: four, + size_info: SizeInfo::Sized { size: 12 }, + statically_shallow_unpadded: false, + }; + let dst = DstLayout { + align: four, + statically_shallow_unpadded: false, + size_info: SizeInfo::SliceDst(TrailingSliceLayout { + offset: 0, + elem_size: 4, + size_base: 0, + size_rounding_align_and_phase: RoundingAlignAndPhase::new(four, 2), + }), + }; + let src = DstLayout { + align: four, + statically_shallow_unpadded: false, + size_info: SizeInfo::SliceDst(TrailingSliceLayout { + // Physical offsets deliberately differ from size bases. + // Cast planning must compare complete rounded sizes. + offset: 3, + elem_size: 8, + size_base: 8, + size_rounding_align_and_phase: RoundingAlignAndPhase::new(four, 2), + }), + }; + assert!(CastPlan::try_compute(&sized, &sized).is_some()); + assert!(CastPlan::try_compute(&sized, &dst).is_some()); + assert!(CastPlan::try_compute(&src, &dst).is_some()); + for count in [0, 1, 7, usize::MAX / 16, usize::MAX].iter().copied() { + // Sized witnesses are ignored, including their phase. + assert_cast_preserves_size(sized, sized, one, 0, one, 0, count); + assert_cast_preserves_size(sized, dst, one, 0, four, 2, count); + assert_cast_preserves_size(src, dst, four, 2, four, 2, count); + } + } + } +} diff --git a/zerocopy/src/layout/tail_transform_checks.rs b/zerocopy/src/layout/tail_transform_checks.rs index 9d7a1f9885..0985417dae 100644 --- a/zerocopy/src/layout/tail_transform_checks.rs +++ b/zerocopy/src/layout/tail_transform_checks.rs @@ -27,7 +27,11 @@ use super::{ DstLayout, SizeInfo, TrailingSliceLayout, }; -pub(crate) 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(