From 22d62861e2ffa9be82ea424a221fc2fe3ee01f47 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Mon, 5 Oct 2026 18:35:46 -0400 Subject: [PATCH] Prove the concrete CastUnsized layout gate Move the actual CastUnsized layout decision into a pure helper consumed by the associated constant. Prove sized equality and accepted DST alignment, physical offset, and complete size sequences. Check an independent Rust sizing harness, including overflow and zero-sized tails. These are conditional numerical guarantees, not pointer-validity proofs. Validation: pinned extraction; independent golden/live proofs, required-contract checks and axiom audits; targeted Rust tests. gherrit-pr-id: G2cbw3wr4c5plt3vf5yzd54trtag3zhkh Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 7 + verification/aeneas/golden/Funs.lean | 103 ++++++++++ verification/aeneas/lean/LayoutModel.lean | 8 + .../aeneas/lean/Obligations/CastUnsized.lean | 44 +++++ .../aeneas/lean/Proofs/CastUnsized.lean | 180 ++++++++++++++++++ .../RequiredModelContracts/CastUnsized.lean | 59 ++++++ zerocopy/src/pointer/mod.rs | 165 ++++++++++++++-- 7 files changed, 554 insertions(+), 12 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/CastUnsized.lean create mode 100644 verification/aeneas/lean/Proofs/CastUnsized.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/CastUnsized.lean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index bce4986756..1ec9bc8ee8 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -33,6 +33,13 @@ 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. +The checks in [`pointer/mod.rs`](../../zerocopy/src/pointer/mod.rs) follow the +actual `CastUnsized` layout gate. Accepted DST pairs retain alignment, physical +tail offset, and complete sizes for every metadata count. Sized pairs need only +equal sizes, including zero-sized layouts with different alignments. Rejection +does not claim that a cast would be impossible. The proof covers the numerical +decision and sizing comparison, not the resulting pointer's validity. + 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 8ede2e2e44..59244f85cf 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -2293,6 +2293,109 @@ def pointer_metadata_usize_size_for_metadata := do Usize.Insts.ZerocopyPointerMetadata.size_for_metadata metadata runtime_layout +/-- [zerocopy::pointer::cast::cast_unsized_layouts_match]: + Source: 'src/pointer/mod.rs', lines 195:4-207:5 -/ +def pointer.cast.cast_unsized_layouts_match + (src : layout.DstLayout) (dst : layout.DstLayout) : Result Bool := do + match src.size_info with + | layout.SizeInfo.Sized src_size => + match dst.size_info with + | layout.SizeInfo.Sized dst_size => ok (src_size = dst_size) + | layout.SizeInfo.SliceDst _ => ok false + | layout.SizeInfo.SliceDst src_trailing => + match dst.size_info with + | layout.SizeInfo.Sized _ => ok false + | layout.SizeInfo.SliceDst dst_trailing => + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + src.align + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + dst.align + if i = i1 + then + if src_trailing.offset = dst_trailing.offset + then + layout.TrailingSliceLayoutUsize.has_same_size_sequence src_trailing + dst_trailing + else ok false + else ok false + +/-- [zerocopy::pointer::cast::checks::witness_matches]: + Source: 'src/pointer/mod.rs', lines 218:8-225:9 -/ +def pointer.cast.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::pointer::cast::checks::reference_size]: + Source: 'src/pointer/mod.rs', lines 227:8-239:9 -/ +def pointer.cast.checks.reference_size + (runtime_layout : layout.DstLayout) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) + (metadata : 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 metadata + +/-- [zerocopy::pointer::cast::checks::assert_cast_unsized]: + Source: 'src/pointer/mod.rs', lines 251:8-276:9 -/ +def pointer.cast.checks.assert_cast_unsized + (src : layout.DstLayout) (dst : layout.DstLayout) + (src_align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (src_phase : Std.Usize) + (dst_align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (dst_phase : Std.Usize) + (metadata : Std.Usize) : + Result Unit + := do + let b ← pointer.cast.checks.witness_matches src src_align src_phase + if b + then + let b1 ← pointer.cast.checks.witness_matches dst dst_align dst_phase + if b1 + then + let b2 ← pointer.cast.cast_unsized_layouts_match src dst + if b2 + then + let o ← + pointer.cast.checks.reference_size src src_align src_phase metadata + let o1 ← + pointer.cast.checks.reference_size dst dst_align dst_phase metadata + let b3 ← layout.tail_checks.same_optional_usize o o1 + massert b3 + match src.size_info with + | layout.SizeInfo.Sized _ => ok () + | layout.SizeInfo.SliceDst src_tail => + match dst.size_info with + | layout.SizeInfo.Sized _ => ok () + | layout.SizeInfo.SliceDst dst_tail => + 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) + massert (src_tail.offset = dst_tail.offset) + else ok () + else ok () + else ok () + /-- [zerocopy::split_at::split_right_len]: Source: 'src/split_at.rs', lines 27:0-29:1 -/ def split_at.split_right_len diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean index 1e6e647a76..bbcb36f971 100644 --- a/verification/aeneas/lean/LayoutModel.lean +++ b/verification/aeneas/lean/LayoutModel.lean @@ -42,6 +42,14 @@ def byteFormula {E : Type} (self : layout.TrailingSliceLayout E) : LayoutMath.Fo def trailingFormula (self : layout.TrailingSliceLayout Usize) : LayoutMath.Formula := { byteFormula self with elem := self.elem_size.val } +/- Complete sizes use exactly the same layout observations as the independent +record semantics. This is distinct from the physical trailing-field offset. +-/ +def completeLayoutSize (self : layout.DstLayout) (count : Nat) : Nat := + match self.size_info with + | .Sized size => size.val + | .SliceDst tail => (trailingFormula tail).size count + /- An absent packing bound acts as the largest representable power of two. The alignment domain bounds ensure that taking the minimum leaves an admitted field alignment unchanged in that case. diff --git a/verification/aeneas/lean/Obligations/CastUnsized.lean b/verification/aeneas/lean/Obligations/CastUnsized.lean new file mode 100644 index 0000000000..7be0b777ec --- /dev/null +++ b/verification/aeneas/lean/Obligations/CastUnsized.lean @@ -0,0 +1,44 @@ +/- 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 + +def cast_unsized_layouts_match_spec_contract (src dst : layout.DstLayout) + (run : Result Bool) : Prop := + layoutValid src → layoutValid dst → run ⦃ accepted => + match src.size_info, dst.size_info with + | .Sized src_size, .Sized dst_size => + accepted = decide (src_size.val = dst_size.val) + | .SliceDst src_tail, .SliceDst dst_tail => accepted = true → + src.align.val.val = dst.align.val.val ∧ src_tail.offset.val = dst_tail.offset.val ∧ + ∀ count : Nat, + completeLayoutSize src count = completeLayoutSize dst count ∧ + (completeLayoutSize src count ≤ Usize.max ↔ completeLayoutSize dst count ≤ Usize.max) + | _, _ => accepted = false ⦄ +def cast_unsized_layouts_match_spec : Prop := ∀ src dst, + cast_unsized_layouts_match_spec_contract src dst + (pointer.cast.cast_unsized_layouts_match src dst) + +def cast_unsized_check_spec_contract (src dst : layout.DstLayout) + (src_align : NonZeroUsize) (src_phase : Usize) (dst_align : NonZeroUsize) + (dst_phase metadata : Usize) (run : Result Unit) : Prop := + layoutValid src → layoutValid dst → + 0 < src_align.val.val → 0 < dst_align.val.val → run ⦃ _ => True ⦄ +def cast_unsized_check_spec : Prop := ∀ src dst src_align src_phase dst_align dst_phase metadata, + cast_unsized_check_spec_contract src dst src_align src_phase dst_align dst_phase metadata + (pointer.cast.checks.assert_cast_unsized src dst src_align src_phase dst_align dst_phase metadata) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/CastUnsized.lean b/verification/aeneas/lean/Proofs/CastUnsized.lean new file mode 100644 index 0000000000..abc1e1fc3f --- /dev/null +++ b/verification/aeneas/lean/Proofs/CastUnsized.lean @@ -0,0 +1,180 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + + +module +public import Proofs +public import Proofs.TailTransformReference +public import RequiredModelContracts.CastUnsized +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw.CastUnsized +open TailChecks + +theorem cast_unsized_layouts_match_spec (src dst : layout.DstLayout) + (src_valid : layoutValid src) (dst_valid : layoutValid dst) : + pointer.cast.cast_unsized_layouts_match src dst ⦃ accepted => + match src.size_info, dst.size_info with + | .Sized src_size, .Sized dst_size => accepted = decide (src_size = dst_size) + | .SliceDst src_tail, .SliceDst dst_tail => accepted = true → + src.align = dst.align ∧ src_tail.offset = dst_tail.offset ∧ + ∀ count : Nat, completeLayoutSize src count = completeLayoutSize dst count + | _, _ => accepted = false ⦄ := by + unfold pointer.cast.cast_unsized_layouts_match + cases src_info : src.size_info with + | Sized src_size => cases dst.size_info <;> simp [WP.spec_ok] + | SliceDst src_tail => + cases dst_info : dst.size_info with + | Sized dst_size => simp [WP.spec_ok] + | SliceDst dst_tail => + have src_positive : 0 < src_tail.size_rounding_align_and_phase._0.val.val := by + simpa only [sizeInfoValid, src_info, trailingValid, + scalar_valid_iff, true_and, encodingValid] using src_valid.2 + have dst_positive : 0 < dst_tail.size_rounding_align_and_phase._0.val.val := by + simpa only [sizeInfoValid, dst_info, trailingValid, + scalar_valid_iff, true_and, encodingValid] using dst_valid.2 + simp only [core.num.nonzero.NonZero.get, bind_ok] + split + · rename_i align_same + split + · rename_i offset_same + step with Zerocopy.Proofs.Raw.same_size_sequence_spec + src_tail dst_tail src_positive dst_positive as ⟨accepted, sizes⟩ + rename_i yes + refine ⟨?_, offset_same, ?_⟩ + · apply nonzero_raw_eq_of_value_eq + exact congrArg UScalar.val align_same + · intro count + simpa only [completeLayoutSize, src_info, dst_info] using sizes yes count + · simp [WP.spec_ok] + · simp [WP.spec_ok] + +/- Every accepted gate preserves size. The sized branch needs no alignment +premise and includes zero-sized layouts with different alignments. -/ +theorem accepted_sizes (src dst : layout.DstLayout) (accepted : Bool) + (yes : accepted = true) + (facts : match src.size_info, dst.size_info with + | .Sized src_size, .Sized dst_size => accepted = decide (src_size = dst_size) + | .SliceDst src_tail, .SliceDst dst_tail => accepted = true → + src.align = dst.align ∧ src_tail.offset = dst_tail.offset ∧ + ∀ count : Nat, completeLayoutSize src count = completeLayoutSize dst count + | _, _ => accepted = false) : + ∀ count : Nat, completeLayoutSize src count = completeLayoutSize dst count := by + cases src_info : src.size_info <;> cases dst_info : dst.size_info + · simp only [src_info, dst_info, yes] at facts + have same : _ := of_decide_eq_true facts.symm + simp only [completeLayoutSize, src_info, dst_info, same, implies_true] + · simp_all + · simp_all + · simp only [src_info, dst_info] at facts + exact (facts yes).2.2 + +theorem witness_matches (self : layout.DstLayout) (align : NonZeroUsize) (phase : Usize) : + pointer.cast.checks.witness_matches self align phase + ⦃ accepted => accepted = true → witnessMatches self align phase ⦄ := by + unfold pointer.cast.checks.witness_matches + cases info : self.size_info with + | Sized size => simp [witnessMatches, info, WP.spec_ok] + | SliceDst tail => + simpa only [witnessMatches, info] using TailTransforms.witness_matches tail align phase + +theorem reference_size (self : layout.DstLayout) (align : NonZeroUsize) + (phase metadata : Usize) (positive : 0 < align.val.val) + (witness : witnessMatches self align phase) : + pointer.cast.checks.reference_size self align phase metadata + ⦃ result => result.map UScalar.val = checkedNat (completeLayoutSize self metadata.val) ⦄ := by + unfold pointer.cast.checks.reference_size + cases info : self.size_info with + | Sized size => + have fits : size.val ≤ Usize.max := by scalar_tac + simp only [WP.spec_ok, Option.map_some, completeLayoutSize, info, checkedNat, fits, if_true] + | SliceDst tail => + simp only [witnessMatches, info] 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 metadata positive) + intro result facts + simpa only [completeLayoutSize, info, view, LayoutMath.Formula.checkedSize, checkedNat] using facts + +theorem cast_unsized_check (src dst : layout.DstLayout) + (src_align : NonZeroUsize) (src_phase : Usize) (dst_align : NonZeroUsize) + (dst_phase metadata : Usize) (src_valid : layoutValid src) (dst_valid : layoutValid dst) + (src_positive : 0 < src_align.val.val) (dst_positive : 0 < dst_align.val.val) : + pointer.cast.checks.assert_cast_unsized src dst src_align src_phase dst_align dst_phase metadata + ⦃ _ => True ⦄ := by + unfold pointer.cast.checks.assert_cast_unsized + step with witness_matches src src_align src_phase as ⟨src_matches, src_witness⟩ + split + · rename_i src_yes + step with witness_matches dst dst_align dst_phase as ⟨dst_matches, dst_witness⟩ + split + · rename_i dst_yes + step with cast_unsized_layouts_match_spec src dst src_valid dst_valid as ⟨accepted, gate_facts⟩ + split + · rename_i yes + have sizes := accepted_sizes src dst accepted yes gate_facts + step with reference_size src src_align src_phase metadata src_positive (src_witness src_yes) + as ⟨src_size, src_size_facts⟩ + step with reference_size dst dst_align dst_phase metadata dst_positive (dst_witness dst_yes) + as ⟨dst_size, dst_size_facts⟩ + have size_same := optional_value_injective + (src_size_facts.trans ((congrArg checkedNat (sizes metadata.val)).trans dst_size_facts.symm)) + step with same_optional_usize src_size dst_size as ⟨same, same_iff⟩ + have same_yes := same_iff.mpr size_same + simp only [massert, same_yes, if_true, bind_ok] + cases src_info : src.size_info with + | Sized bytes => simp [WP.spec_ok] + | SliceDst src_tail => + cases dst_info : dst.size_info with + | Sized bytes => simp [WP.spec_ok] + | SliceDst dst_tail => + simp only [src_info, dst_info] at gate_facts + obtain ⟨align_same, offset_same, _⟩ := gate_facts yes + simp [core.num.nonzero.NonZero.get, align_same, offset_same, WP.spec_ok] + · simp [WP.spec_ok] + · simp [WP.spec_ok] + · simp [WP.spec_ok] + +end Zerocopy.Proofs.Raw.CastUnsized + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem cast_unsized_layouts_match_spec : Specs.cast_unsized_layouts_match_spec := by + unfold Specs.cast_unsized_layouts_match_spec + representation_simps + intro src dst src_valid dst_valid + have src_admitted : layoutValid src := by + simpa only [layoutValid, sizeInfoValid, trailingValid, scalar_valid_iff, + true_and, encodingValid] using src_valid + have dst_admitted : layoutValid dst := by + simpa only [layoutValid, sizeInfoValid, trailingValid, scalar_valid_iff, + true_and, encodingValid] using dst_valid + apply WP.spec_mono (Raw.CastUnsized.cast_unsized_layouts_match_spec + src dst src_admitted dst_admitted) + intro accepted facts + cases src_info : src.size_info <;> cases dst_info : dst.size_info <;> + simpa only [src_info, dst_info, UScalar.eq_equiv] using facts +register_spec_step cast_unsized_layouts_match_spec + +theorem cast_unsized_check_spec : Specs.cast_unsized_check_spec := by + unfold Specs.cast_unsized_check_spec + intro src dst src_align src_phase dst_align dst_phase metadata + src_value src_decoded dst_value dst_decoded src_align_value src_align_decoded + src_phase_value src_phase_decoded dst_align_value dst_align_decoded + dst_phase_value dst_phase_decoded metadata_value metadata_decoded + have src_valid := (layout_valid_iff src).mp ⟨src_value, src_decoded⟩ + have dst_valid := (layout_valid_iff dst).mp ⟨dst_value, dst_decoded⟩ + have src_positive := (nonzero_valid_iff src_align).mp ⟨src_align_value, src_align_decoded⟩ + have dst_positive := (nonzero_valid_iff dst_align).mp ⟨dst_align_value, dst_align_decoded⟩ + apply WP.spec_mono (Raw.CastUnsized.cast_unsized_check src dst src_align src_phase + dst_align dst_phase metadata src_valid dst_valid src_positive dst_positive) + intro result _facts + exact ⟨(), rfl, trivial⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/CastUnsized.lean b/verification/aeneas/lean/RequiredModelContracts/CastUnsized.lean new file mode 100644 index 0000000000..663050341c --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/CastUnsized.lean @@ -0,0 +1,59 @@ +/- 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.CastUnsized +public import RequiredModelContracts +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +@[contract_simps] theorem required_cast_unsized_layouts_match (src dst : layout.DstLayout) + (run : Result Bool) + (provided : Specs.cast_unsized_layouts_match_spec_contract src dst run) : + Obligations.cast_unsized_layouts_match_spec_contract src dst run := by + intro src_valid dst_valid + obtain ⟨src_value, src_decoded⟩ := (layout_valid_iff src).mpr src_valid + obtain ⟨dst_value, dst_decoded⟩ := (layout_valid_iff dst).mpr dst_valid + apply WP.spec_mono (provided src_value src_decoded dst_value dst_decoded) + rintro accepted ⟨_value, _decoded, facts⟩ + cases src_info : src.size_info <;> cases dst_info : dst.size_info + · simpa only [src_info, dst_info, UScalar.eq_equiv] using facts + · simpa only [src_info, dst_info] using facts + · simpa only [src_info, dst_info] using facts + · simp only [src_info, dst_info] at facts ⊢ + intro yes + obtain ⟨align_same, offset_same, size_same⟩ := facts yes + refine ⟨congrArg (fun (a : NonZeroUsize) => a.val.val) align_same, + congrArg UScalar.val offset_same, ?_⟩ + intro count + exact ⟨size_same count, by rw [size_same count]⟩ + +@[contract_simps] theorem required_cast_unsized_check (src dst : layout.DstLayout) + (src_align : NonZeroUsize) (src_phase : Usize) (dst_align : NonZeroUsize) + (dst_phase metadata : Usize) (run : Result Unit) + (provided : Specs.cast_unsized_check_spec_contract + src dst src_align src_phase dst_align dst_phase metadata run) : + Obligations.cast_unsized_check_spec_contract + src dst src_align src_phase dst_align dst_phase metadata run := by + intro src_valid dst_valid src_positive dst_positive + obtain ⟨src_value, src_decoded⟩ := (layout_valid_iff src).mpr src_valid + obtain ⟨dst_value, dst_decoded⟩ := (layout_valid_iff dst).mpr dst_valid + let src_align_value : NonZeroUsizeValue := ⟨unsignedWord src_align.val, src_positive⟩ + let dst_align_value : NonZeroUsizeValue := ⟨unsignedWord dst_align.val, dst_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 metadata) rfl) + rintro result ⟨_value, _decoded, _facts⟩ + trivial + +end Zerocopy.Proofs diff --git a/zerocopy/src/pointer/mod.rs b/zerocopy/src/pointer/mod.rs index 52ba00fd95..910a91c19b 100644 --- a/zerocopy/src/pointer/mod.rs +++ b/zerocopy/src/pointer/mod.rs @@ -47,7 +47,7 @@ where pub mod cast { use core::{marker::PhantomData, mem}; - use crate::{layout::SizeInfo, HasField, KnownLayout, PtrInner}; + use crate::{layout::SizeInfo, DstLayout, HasField, KnownLayout, PtrInner}; /// A pointer cast or projection. /// @@ -177,6 +177,157 @@ pub mod cast { #[allow(missing_debug_implementations, missing_copy_implementations)] pub enum CastUnsized {} + /// The numerical acceptance gate used by `CastUnsized`. + /// + /// Sized layouts compare only their sizes. Slice DSTs also compare their + /// alignment and physical trailing-slice offset. The size-sequence check + /// recognizes sufficient conditions; rejection need not prove inequality. + /// + /// ```aeneas + /// spec cast_unsized_layouts_match_spec + /// ensures(raw) accepted => match src.size_info, dst.size_info with + /// | .Sized src_size, .Sized dst_size => accepted = decide (src_size = dst_size) + /// | .SliceDst src_tail, .SliceDst dst_tail => accepted = true → + /// src.align = dst.align ∧ src_tail.offset = dst_tail.offset ∧ + /// ∀ count : Nat, completeLayoutSize src count = completeLayoutSize dst count + /// | _, _ => accepted = false + /// ``` + pub(crate) const fn cast_unsized_layouts_match(src: DstLayout, dst: DstLayout) -> bool { + match (src.size_info, dst.size_info) { + (SizeInfo::Sized { size: src_size }, SizeInfo::Sized { size: dst_size }) => { + src_size == dst_size + } + (SizeInfo::SliceDst(src_trailing), SizeInfo::SliceDst(dst_trailing)) => { + src.align.get() == dst.align.get() + && src_trailing.offset == dst_trailing.offset + && src_trailing.has_same_size_sequence(dst_trailing) + } + _ => false, + } + } + + // The numerical gate is exercised without pointer construction. Independent + // remainder-based sizes retain their complete Option, including overflow. + #[allow(dead_code, clippy::needless_nonzero_get)] + mod checks { + use core::num::NonZeroUsize; + + use super::{cast_unsized_layouts_match, DstLayout, 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) + } + } + } + + fn reference_size( + runtime_layout: DstLayout, + align: NonZeroUsize, + phase: usize, + metadata: usize, + ) -> Option { + match runtime_layout.size_info { + SizeInfo::Sized { size } => Some(size), + SizeInfo::SliceDst(tail) => { + tail_checks::reference_size(tail, align, phase, metadata) + } + } + } + + /// Acceptance preserves complete sizes for every metadata value, even + /// when those sizes overflow. Slice DSTs also preserve the physical + /// trailing-slice offset and alignment. Sized casts deliberately do + /// not constrain alignment. Witness guards only identify each stored + /// rounding encoding; every positive encoding admits witnesses. + /// + /// ```aeneas + /// spec cast_unsized_check_spec + /// ensures(raw) _ => True + /// ``` + fn assert_cast_unsized( + src: DstLayout, + dst: DstLayout, + src_align: NonZeroUsize, + src_phase: usize, + dst_align: NonZeroUsize, + dst_phase: usize, + metadata: usize, + ) { + if !witness_matches(src, src_align, src_phase) + || !witness_matches(dst, dst_align, dst_phase) + || !cast_unsized_layouts_match(src, dst) + { + return; + } + assert!(tail_checks::same_optional_usize( + reference_size(src, src_align, src_phase, metadata), + reference_size(dst, dst_align, dst_phase, metadata), + )); + if let (SizeInfo::SliceDst(src_tail), SizeInfo::SliceDst(dst_tail)) = + (src.size_info, dst.size_info) + { + assert!(src.align.get() == dst.align.get()); + assert!(src_tail.offset == dst_tail.offset); + } + } + + #[cfg(test)] + mod tests { + use super::*; + use crate::layout::{RoundingAlignAndPhase, TrailingSliceLayout}; + + #[test] + fn sized_gate_preserves_alignment_independence() { + let one = NonZeroUsize::new(1).unwrap(); + let eight = NonZeroUsize::new(8).unwrap(); + for size in [0, 8] { + let src = DstLayout { + align: one, + size_info: SizeInfo::Sized { size }, + statically_shallow_unpadded: true, + }; + let dst = DstLayout { align: eight, ..src }; + assert!(cast_unsized_layouts_match(src, dst)); + assert_cast_unsized(src, dst, one, 0, one, 0, usize::MAX); + let different = DstLayout { size_info: SizeInfo::Sized { size: 16 }, ..dst }; + assert!(!cast_unsized_layouts_match(src, different)); + } + } + + #[test] + fn dst_gate_preserves_complete_overflow_and_physical_offset() { + let four = NonZeroUsize::new(4).unwrap(); + let tail = TrailingSliceLayout { + offset: 7, + elem_size: 4, + size_base: 0, + size_rounding_align_and_phase: RoundingAlignAndPhase::new(four, 0), + }; + let src = DstLayout { + align: four, + size_info: SizeInfo::SliceDst(tail), + statically_shallow_unpadded: false, + }; + assert!(cast_unsized_layouts_match(src, src)); + for metadata in [0, 1, usize::MAX / 4, usize::MAX] { + assert_cast_unsized(src, src, four, 0, four, 0, metadata); + } + let dst = DstLayout { + size_info: SizeInfo::SliceDst(TrailingSliceLayout { offset: 8, ..tail }), + ..src + }; + assert!(!cast_unsized_layouts_match(src, dst)); + let sized = DstLayout { size_info: SizeInfo::Sized { size: 0 }, ..src }; + assert!(!cast_unsized_layouts_match(src, sized)); + assert!(!cast_unsized_layouts_match(sized, src)); + } + } + } + // SAFETY: By the `static_assert!`, `Src` and `Dst` are either: // - Both sized and equal in size // - Both slice DSTs with the same trailing-slice offset, the same object @@ -192,17 +343,7 @@ pub mod cast { // FIXME: Do we want this to support shrinking casts as well? If so, // we'll need to remove the `CastExact` impl. static_assert!(Src: ?Sized + KnownLayout, Dst: ?Sized + KnownLayout => { - let src = ::LAYOUT; - let dst = ::LAYOUT; - match (src.size_info, dst.size_info) { - (SizeInfo::Sized { size: src_size }, SizeInfo::Sized { size: dst_size }) => src_size == dst_size, - (SizeInfo::SliceDst(src_trailing), SizeInfo::SliceDst(dst_trailing)) => { - src.align.get() == dst.align.get() - && src_trailing.offset == dst_trailing.offset - && src_trailing.has_same_size_sequence(dst_trailing) - }, - _ => false, - } + cast_unsized_layouts_match(::LAYOUT, ::LAYOUT) }); let metadata = Src::pointer_to_metadata(src.as_ptr());