Prove cast metadata composition against reference sizes

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.

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

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

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