Prove CastUnsized's production layout acceptance gate

verification/aeneas/README.md

@@ -69,6 +69,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.

verification/aeneas/golden/Funs.lean

@@ -2308,6 +2308,109 @@ def pointer_metadata_usize_size_for_metadata
 native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do
   core.mem.zeroed Self
 
+/-- [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

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.

verification/aeneas/lean/Obligations/CastUnsized.lean

@@ -0,0 +1,44 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, 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

verification/aeneas/lean/Proofs/CastUnsized.lean

@@ -0,0 +1,180 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, 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