From f6cb425673a2d78c19fe6b1c843dc013cce9a6b5 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Mon, 5 Oct 2026 13:12:33 -0400 Subject: [PATCH] Prove cast metadata composition against reference sizes Add an inline Rust assertion harness that selects the production cast plan, requires checked metadata arithmetic to succeed, invokes the actual unchecked conversion, and compares complete sizes using the independent remainder-based reference. Cover sized-to-sized, sized-to-DST and affine DST-to-DST plans. Prove metadata representability from the accepted plan and a complete source size fitting usize, covering the stronger isize-bound caller domain. Retain independent contract checks and explicit witness guards. Pointer provenance, reference validity and KnownLayout implementations remain separate obligations. Validation: fresh required proofs and axiom audit, all170 library tests, and MSRV/stable/nightly and workspace Clippy checks. Both complete final models reject an incorrect arithmetic model and a failing root assertion. Agent-authored-by: AI agent acting on joshlf's behalf gherrit-pr-id: G3ae3zf3etbretqebdewalwfyjb4kmdpo --- verification/aeneas/README.md | 18 +- verification/aeneas/SEMANTICS.md | 7 +- verification/aeneas/golden/Funs.lean | 260 ++++++++++++------ verification/aeneas/lean/CastMath.lean | 33 +++ .../lean/Obligations/CastComposition.lean | 36 +++ .../aeneas/lean/Proofs/CastComposition.lean | 171 ++++++++++++ .../aeneas/lean/Proofs/CastSafety.lean | 62 +++++ .../CastComposition.lean | 41 +++ zerocopy/src/layout/cast_from.rs | 207 ++++++++++---- zerocopy/src/layout/tail_transform_checks.rs | 6 +- 10 files changed, 706 insertions(+), 135 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/CastComposition.lean create mode 100644 verification/aeneas/lean/Proofs/CastComposition.lean create mode 100644 verification/aeneas/lean/Proofs/CastSafety.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/CastComposition.lean 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(