Prove selected cast plans preserve size without metadata overflow

verification/aeneas/README.md

@@ -1344,3 +1344,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.

verification/aeneas/SEMANTICS.md

@@ -122,7 +122,12 @@ on overflow. 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 downstream `forbiddenExecution` marker uses Aeneas's existing `.undef`
 failure tag. The backend also uses that tag for unsupported modeling, so it

verification/aeneas/golden/Funs.lean

@@ -1193,6 +1193,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
@@ -2139,19 +2312,6 @@ def Slice.Insts.ZerocopyKnownLayout.LAYOUT (T : Type)
   : Result layout.DstLayout :=
   layout.DstLayout.for_slice T
 
-/-- [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::primitive_checks::check_u32_slice_known_layout]:
     Source: 'src/layout/primitive_checks.rs', lines 95:0-120:1 -/
 def layout.primitive_checks.check_u32_slice_known_layout
@@ -2190,45 +2350,6 @@ def layout.primitive_checks.check_u32_slice_known_layout
         massert b1
   else ok ()
 
-/-- [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
@@ -2451,31 +2572,6 @@ 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-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::tail_transform_checks::reference_advance]:
     Source: 'src/layout/tail_transform_checks.rs', lines 44:0-70:1 -/
 def layout.tail_transform_checks.reference_advance

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

verification/aeneas/lean/Obligations/CastComposition.lean

@@ -0,0 +1,36 @@
+/- 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
+
+/- 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