From 653bb35dcad39811d13ab64ca6192436892737a5 Mon Sep 17 00:00:00 2001
From: Josh Liebow-Feeser <hello@joshlf.com>
Date: Fri, 2 Oct 2026 11:05:49 -0400
Subject: [PATCH] Prove cast validation and exact metadata inference

Establish independent error priority, greatest-fitting metadata and exact
prefix/suffix outcomes. Keep outcome examples distinct from contract expansion,
including unattainable sizes and intentional zero-stride panic.

Compare exact-size metadata and complete cast results with independent Rust
calculations, including error precedence, greatest fitting counts, and both
prefix/suffix splits. State address overflow and zero-stride exclusions in Rust.

Validation: fresh pinned extraction and complete-model golden comparison;
independent golden/live Lean builds, required-contract checks, and the
transitive axiom audit.

gherrit-pr-id: Gurqevo3e4xhhk2x275sikrq6qmdyzyqb
Agent-authored-by: AI agent acting on joshlf's behalf
---
 verification/aeneas/README.md                 |  10 +
 verification/aeneas/golden/Funs.lean          | 260 ++++++++++++++-
 verification/aeneas/golden/Types.lean         |  15 +
 verification/aeneas/lean/Corollaries.lean     |  11 +
 verification/aeneas/lean/LayoutModel.lean     |  49 ++-
 verification/aeneas/lean/MathViews.lean       |  26 +-
 verification/aeneas/lean/Obligations.lean     |  55 ++++
 .../aeneas/lean/Obligations/TailChecks.lean   |  11 +
 verification/aeneas/lean/OutcomeTests.lean    | 124 +++++++
 verification/aeneas/lean/Proofs.lean          | 307 ++++++++++++++++++
 .../aeneas/lean/Proofs/TailChecks.lean        | 156 +++++++++
 .../aeneas/lean/Proofs/TailReference.lean     | 248 ++++++++++++++
 .../aeneas/lean/RequiredModelContracts.lean   |  44 +++
 .../RequiredModelContracts/TailChecks.lean    |  18 +
 zerocopy/src/layout/mod.rs                    |  14 +
 zerocopy/src/layout/tail_checks.rs            | 287 +++++++++++++++-
 16 files changed, 1629 insertions(+), 6 deletions(-)
 create mode 100644 verification/aeneas/lean/OutcomeTests.lean

diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index ca0a49648b..7494d3f4cc 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -170,6 +170,7 @@ added without extending the specification set.
 | `DstLayout::{extend,pad_to_align}` | Exact field placement, alignment, padding flags, and normalized size formulas; outer padding preserves each field's complete inner size. |
 | Trailing advancement and size-sequence comparison | Exact byte advancement; a positive comparison establishes equal sizes for every natural metadata value. |
 | `DstLayout::requires_dynamic_padding` | Exact flag result and a mathematical condition sufficient to eliminate dynamic padding for all metadata values. |
+| Cast validation and exact-size metadata | Alignment/size error priority, greatest fitting metadata, exact prefix/suffix split, and rejection of unattainable sizes. |
 
 Every registered function uses total `spec`: accepted raw representations,
 supplied mathematical ghosts, and explicit requirements imply successful
@@ -207,6 +208,10 @@ padding inside packed fields.
 A positive size-sequence comparison establishes equal sizes for every natural
 metadata value; a negative result does not assert that the sequences differ.
 
+Cast validation and exact metadata inference establish error priority, exact
+splits and rejection of unattainable sizes. Intentional zero-stride panic is
+checked separately.
+
 Plain arithmetic clauses use mathematical word values carrying machine bounds
 and NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw
 clauses preserve the extracted representation vocabulary while retaining
@@ -506,6 +511,11 @@ audit checks those identities and their generated-module ownership in both
 directions, independently scans raw nominal types, and rejects missing or extra
 provider registrations. This reuses one verified table without another coverage roster.
 
+For cast validation and
+exact-size metadata, the required outcomes spell out error priority, split
+positions, exact size, and greatest-fitting metadata independently of the
+predicates used by the inline specs. `OutcomeTests.lean` pins distinguishing
+fixed-size, suffix-alignment, and padded-size plateau examples.
 `Check.lean` derives dependencies from elaborated theorem types and terms,
 following helpers across handwritten modules, including private helpers, and
 writes `proof-dependencies.json` in each proof workspace. It imports and audits all
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index d788bed9fe..9bb9209aa1 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -1674,6 +1674,100 @@ def layout.DstLayout.requires_dynamic_padding
       then ok true
       else ok (¬ (i1 = 0#usize))
 
+/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::validate_cast_and_convert_metadata]:
+    Source: 'src/layout/mod.rs', lines 1839:4-1986:5 -/
+def layout.DstLayout.validate_cast_and_convert_metadata
+  (self : layout.DstLayout) (addr : Std.Usize) (bytes_len : Std.Usize)
+  (cast_type : layout.CastType) :
+  Result (core.result.Result (Std.Usize × Std.Usize) layout.MetadataCastError)
+  := do
+  let o ← layout.SizeInfoUsize.try_to_nonzero_elem_size self.size_info
+  match o with
+  | none => fail panic
+  | some size_info =>
+    let o1 ← lift (Usize.checked_add addr bytes_len)
+    let e := core.option.Option.is_some o1
+    massert e
+    let offset ←
+      match cast_type with
+      | layout.CastType.Prefix => ok 0#usize
+      | layout.CastType.Suffix => ok bytes_len
+    let i ← addr + offset
+    let i1 ←
+      core.num.nonzero.NonZero.get
+        Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner 
+        self.align
+    let i2 ← i % i1
+    if i2 != 0#usize
+    then ok (core.result.Result.Err layout.MetadataCastError.Alignment)
+    else
+      match size_info with
+      | layout.SizeInfo.Sized size =>
+        massert ((size > bytes_len) || (size <= bytes_len))
+        if size > bytes_len
+        then ok (core.result.Result.Err layout.MetadataCastError.Size)
+        else
+          match cast_type with
+          | layout.CastType.Prefix =>
+            ok (core.result.Result.Ok (0#usize, size))
+          | layout.CastType.Suffix =>
+            let split_at ← bytes_len - size
+            ok (core.result.Result.Ok (0#usize, split_at))
+      | layout.SizeInfo.SliceDst trailing =>
+        let o2 ←
+          layout.TrailingSliceLayout.max_trailing_bytes trailing bytes_len
+        match o2 with
+        | none => ok (core.result.Result.Err layout.MetadataCastError.Size)
+        | some bytes =>
+          let (elems, _) ←
+            layout.max_elems_for_bytes bytes trailing.elem_size
+          let size_align ←
+            layout.RoundingAlignAndPhase.align
+              trailing.size_rounding_align_and_phase
+          let i3 ←
+            core.num.nonzero.NonZero.get
+              Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+              trailing.elem_size
+          let unused_bytes ← bytes % i3
+          let unused_aligned_bytes ←
+            util.round_down_to_next_multiple_of_alignment unused_bytes
+              size_align
+          let i4 ← bytes_len - trailing.size_base
+          let max_rounded_bytes ←
+            util.round_down_to_next_multiple_of_alignment i4 size_align
+          let i5 ← max_rounded_bytes - unused_aligned_bytes
+          let self_bytes ← trailing.size_base + i5
+          massert (self_bytes <= bytes_len)
+          match cast_type with
+          | layout.CastType.Prefix =>
+            ok (core.result.Result.Ok (elems, self_bytes))
+          | layout.CastType.Suffix =>
+            let split_at ← bytes_len - self_bytes
+            ok (core.result.Result.Ok (elems, split_at))
+
+/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::metadata_for_exact_size]:
+    Source: 'src/layout/mod.rs', lines 1701:4-1724:5 -/
+def layout.DstLayout.metadata_for_exact_size
+  (self : layout.DstLayout) (size : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  match self.size_info with
+  | layout.SizeInfo.Sized _ => ok none
+  | layout.SizeInfo.SliceDst tsl =>
+    match tsl.elem_size.val with
+    | 0 => ok none
+    | _ =>
+      let r ←
+        layout.DstLayout.validate_cast_and_convert_metadata self 0#usize size
+          layout.CastType.Prefix
+      match r with
+      | core.result.Result.Ok p =>
+        let (elems, object_size) := p
+        if object_size = size
+        then ok (some elems)
+        else ok none
+      | core.result.Result.Err _ => ok none
+
 /-- [zerocopy::layout::nested_reference::round_up]:
     Source: 'src/layout/nested_reference.rs', lines 46:0-56:1 -/
 def layout.nested_reference.round_up
@@ -1953,8 +2047,82 @@ def layout.tail_checks.reference_capacity
     let rounded_budget ← after_base - i1
     ok (Usize.checked_sub rounded_budget phase)
 
+/-- [zerocopy::layout::tail_checks::reference_metadata]:
+    Source: 'src/layout/tail_checks.rs', lines 78:0-104:1 -/
+def layout.tail_checks.reference_metadata
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (size : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  match runtime_layout.size_info with
+  | layout.SizeInfo.Sized _ => ok none
+  | layout.SizeInfo.SliceDst tail =>
+    if tail.elem_size = 0#usize
+    then ok none
+    else
+      let o ← layout.tail_checks.reference_capacity tail align phase size
+      match o with
+      | none => ok none
+      | some bytes =>
+        let elems ← bytes / tail.elem_size
+        let o1 ← layout.tail_checks.reference_size tail align phase elems
+        let b ← layout.tail_checks.same_optional_usize o1 (some size)
+        if b
+        then ok (some elems)
+        else ok none
+
+/-- [zerocopy::layout::tail_checks::reference_cast]:
+    Source: 'src/layout/tail_checks.rs', lines 107:0-154:1 -/
+def layout.tail_checks.reference_cast
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (addr : Std.Usize) (length : Std.Usize) (side : layout.CastType) :
+  Result (core.result.Result (Std.Usize × Std.Usize) layout.MetadataCastError)
+  := do
+  let anchor ←
+    match side with
+    | layout.CastType.Prefix => ok addr
+    | layout.CastType.Suffix => addr + length
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+      runtime_layout.align
+  let i1 ← anchor % i
+  if i1 != 0#usize
+  then ok (core.result.Result.Err layout.MetadataCastError.Alignment)
+  else
+    let candidate ←
+      match runtime_layout.size_info with
+      | layout.SizeInfo.Sized size =>
+        if size <= length
+        then ok (some (0#usize, size))
+        else ok none
+      | layout.SizeInfo.SliceDst tail =>
+        do
+        let o ← layout.tail_checks.reference_capacity tail align phase length
+        match o with
+        | none => ok none
+        | some bytes =>
+          let elems ← bytes / tail.elem_size
+          let o1 ← layout.tail_checks.reference_size tail align phase elems
+          match o1 with
+          | none => ok none
+          | some size => ok (some (elems, size))
+    match candidate with
+    | none => ok (core.result.Result.Err layout.MetadataCastError.Size)
+    | some p =>
+      let (elems, size) := p
+      match side with
+      | layout.CastType.Prefix => ok (core.result.Result.Ok p)
+      | layout.CastType.Suffix =>
+        let split ← length - size
+        ok (core.result.Result.Ok (elems, split))
+
 /-- [zerocopy::layout::tail_checks::trailing_arithmetic_check]:
-    Source: 'src/layout/tail_checks.rs', lines 88:0-111:1 -/
+    Source: 'src/layout/tail_checks.rs', lines 166:0-189:1 -/
 def layout.tail_checks.trailing_arithmetic_check
   (tail : layout.TrailingSliceLayout Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -1991,6 +2159,96 @@ def layout.tail_checks.trailing_arithmetic_check
     else ok ()
   else ok ()
 
+/-- [zerocopy::layout::tail_checks::layout_observations_check]:
+    Source: 'src/layout/tail_checks.rs', lines 204:0-247:1 -/
+def layout.tail_checks.layout_observations_check
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (size : Std.Usize) (addr : Std.Usize) (length : Std.Usize)
+  (side : layout.CastType) :
+  Result Unit
+  := do
+  let (si, encoding_matches) ←
+    match runtime_layout.size_info with
+    | layout.SizeInfo.Sized _ => ok (runtime_layout.size_info, true)
+    | layout.SizeInfo.SliceDst tail =>
+      do
+      let i ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+      let b ← core.num.Usize.is_power_of_two i
+      let b1 ←
+        if b
+        then
+          if phase < i
+          then
+            do
+            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
+      ok (runtime_layout.size_info, b1)
+  if encoding_matches
+  then
+    let o ←
+      layout.DstLayout.metadata_for_exact_size
+        { runtime_layout with size_info := si } size
+    let o1 ←
+      layout.tail_checks.reference_metadata
+        { runtime_layout with size_info := si } align phase size
+    let b ← layout.tail_checks.same_optional_usize o o1
+    massert b
+    let nonzero_stride ←
+      match si with
+      | layout.SizeInfo.Sized _ => ok true
+      | layout.SizeInfo.SliceDst tail => ok (tail.elem_size != 0#usize)
+    let o2 ← lift (Usize.checked_add addr length)
+    let b1 := core.option.Option.is_some o2
+    if b1
+    then
+      if nonzero_stride
+      then
+        let actual ←
+          layout.DstLayout.validate_cast_and_convert_metadata
+            { runtime_layout with size_info := si } addr length side
+        let expected ←
+          layout.tail_checks.reference_cast
+            { runtime_layout with size_info := si } align phase addr length
+            side
+        let same ←
+          match actual with
+          | core.result.Result.Ok p =>
+            match expected with
+            | core.result.Result.Ok p1 =>
+              let (elems, split) := p
+              let (expected_elems, expected_split) := p1
+              if elems = expected_elems
+              then ok (split = expected_split)
+              else ok false
+            | core.result.Result.Err _ => ok false
+          | core.result.Result.Err mce =>
+            match expected with
+            | core.result.Result.Ok _ => ok false
+            | core.result.Result.Err mce1 =>
+              match mce with
+              | layout.MetadataCastError.Alignment =>
+                match mce1 with
+                | layout.MetadataCastError.Alignment => ok true
+                | layout.MetadataCastError.Size => ok false
+              | layout.MetadataCastError.Size =>
+                match mce1 with
+                | layout.MetadataCastError.Alignment => ok false
+                | layout.MetadataCastError.Size => ok true
+        massert same
+      else ok ()
+    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
diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean
index 465d9bd59c..a4c2f9fae7 100644
--- a/verification/aeneas/golden/Types.lean
+++ b/verification/aeneas/golden/Types.lean
@@ -154,6 +154,21 @@ structure layout.DstLayout where
   size_info : layout.SizeInfo Std.Usize
   statically_shallow_unpadded : Bool
 
+/-- [zerocopy::layout::CastType]
+    Source: 'src/layout/mod.rs', lines 913:0-916:1
+    Visibility: public -/
+@[discriminant isize]
+inductive layout.CastType where
+| Prefix : layout.CastType
+| Suffix : layout.CastType
+
+/-- [zerocopy::layout::MetadataCastError]
+    Source: 'src/layout/mod.rs', lines 920:0-923:1 -/
+@[discriminant isize]
+inductive layout.MetadataCastError where
+| Alignment : layout.MetadataCastError
+| Size : layout.MetadataCastError
+
 /-- [zerocopy::layout::nested_reference::NestedLayer]
     Source: 'src/layout/nested_reference.rs', lines 27:0-31:1 -/
 structure layout.nested_reference.NestedLayer where
diff --git a/verification/aeneas/lean/Corollaries.lean b/verification/aeneas/lean/Corollaries.lean
index f5ccc84d61..3c74904bff 100644
--- a/verification/aeneas/lean/Corollaries.lean
+++ b/verification/aeneas/lean/Corollaries.lean
@@ -166,4 +166,15 @@ theorem padding_matches_recursive (tail : layout.TrailingSliceLayout Usize)
   dsimp only [remaining, physical] at hcancel
   omega
 
+theorem validate_zero_stride (self : layout.DstLayout) (tail : layout.TrailingSliceLayout Usize)
+    (hs : self.size_info = .SliceDst tail) (he : tail.elem_size = 0#usize)
+    (addr length : Usize) (side : layout.CastType) :
+    layout.DstLayout.validate_cast_and_convert_metadata self addr length side = .fail .panic := by
+  have hp := Proofs.Raw.try_nonzero_spec self.size_info
+  obtain ⟨converted, hconverted, hv⟩ := WP.spec_imp_exists hp
+  simp only [hs, he, if_true] at hv
+  unfold layout.DstLayout.validate_cast_and_convert_metadata
+  rw [hconverted, hv]
+  simp only [bind_ok]
+
 end Zerocopy.Corollaries
diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean
index bbcb36f971..87586631af 100644
--- a/verification/aeneas/lean/LayoutModel.lean
+++ b/verification/aeneas/lean/LayoutModel.lean
@@ -16,8 +16,9 @@ public import LayoutMath
 /-!
 Extracted records contain machine words and compressed rounding encodings.
 This module gives those records ordinary mathematical observations: a size
-formula, a physical slice offset, and field placement. The definitions do not
-call an extracted operation or assume that it is correct.
+formula, a physical slice offset, field placement, and cast or metadata
+outcomes. The definitions do not call an extracted operation or assume that
+it is correct.
 
 Proofs uses the raw observations to state implementation lemmas and
 independent expectations. ModelViews exposes corresponding observations of
@@ -65,6 +66,48 @@ def fieldAlignment (field : layout.DstLayout) (packed : Option NonZeroUsize) : N
 def placement (size : Usize) (field : layout.DstLayout) (packed : Option NonZeroUsize) :=
   LayoutMath.roundUp size.val (fieldAlignment field packed)
 
+def castSide (cast : layout.CastType) (length : Nat) : Nat :=
+  match cast with | .Prefix => 0 | .Suffix => length
+
+def castSplit (cast : layout.CastType) (length size : Nat) : Nat :=
+  match cast with | .Prefix => size | .Suffix => length - size
+
+/- Describe exact cast outcomes independently of the implementation. Alignment
+errors have priority; a suffix checks the end address; successful trailing
+casts return the greatest fitting metadata and the corresponding physical
+split.
+-/
+def castSpec (self : layout.DstLayout) (addr length : Nat) (cast : layout.CastType)
+    (result : core.result.Result (Usize × Usize) layout.MetadataCastError) : Prop :=
+  let anchor := addr + castSide cast length
+  match result with
+  | .Err .Alignment => anchor % self.align.val.val ≠ 0
+  | .Err .Size => anchor % self.align.val.val = 0 ∧
+    match self.size_info with
+    | .Sized size => length < size.val
+    | .SliceDst tail => ∀ n : Nat, length < (trailingFormula tail).size n
+  | .Ok (elems, split) => anchor % self.align.val.val = 0 ∧
+    match self.size_info with
+    | .Sized size => elems.val = 0 ∧ size.val ≤ length ∧
+      split.val = castSplit cast length size.val
+    | .SliceDst tail => (trailingFormula tail).size elems.val ≤ length ∧
+      (∀ n : Nat, (trailingFormula tail).size n ≤ length ↔ n ≤ elems.val) ∧
+      split.val = castSplit cast length ((trailingFormula tail).size elems.val)
+
+/- Describe exact-size metadata, including failure when no count has that
+complete size. On a rounding plateau, success must select the greatest count;
+fixed layouts and zero element strides have no inferred trailing metadata.
+-/
+def metadataSpec (self : layout.DstLayout) (size : Nat) (r : Option Usize) : Prop :=
+  match self.size_info with
+  | .Sized _ => r = none
+  | .SliceDst tail =>
+    if tail.elem_size.val = 0 then r = none else
+    match r with
+    | none => ∀ n : Nat, (trailingFormula tail).size n ≠ size
+    | some elems => (trailingFormula tail).size elems.val = size ∧
+      (∀ n : Nat, (trailingFormula tail).size n ≤ size ↔ n ≤ elems.val)
+
 /- Project the raw record to the fragment vocabulary used by layout operations.
 This preserves alignment, payload, physical offset, stride, and unpadded
 flag.
@@ -89,6 +132,8 @@ is an explicit operation domain, not a consequence of NonZeroUsize alone.
 -/
 def alignmentDomain (a : Nat) : Prop := a.isPowerOfTwo ∧ a ≤ 2 ^ 29
 
+attribute [contract_simps] castSide castSplit castSpec metadataSpec
+
 end Zerocopy.Proofs
 
 -- Mathematical projections consume the one recursively decoded record. The
diff --git a/verification/aeneas/lean/MathViews.lean b/verification/aeneas/lean/MathViews.lean
index bfb06410d0..5700db3e06 100644
--- a/verification/aeneas/lean/MathViews.lean
+++ b/verification/aeneas/lean/MathViews.lean
@@ -120,6 +120,24 @@ def layoutValid (self : layout.DstLayout) : Prop :=
   change (isValid self.align ∧ isValid self.size_info ∧ isValid self.statically_shallow_unpadded) ↔ _
   simp only [nonzero_valid_iff, size_info_valid_iff, bool_valid_iff, and_true]
 
+@[simp, contract_simps] theorem cast_type_valid_iff (side : layout.CastType) : isValid side ↔ True := by
+  cases side <;>
+    simp [isValid, RustModel.decode, layout.CastType.aeneasModel,
+      layout.CastType.decode, layout.CastType.decodeFields]
+
+@[simp, contract_simps] theorem metadata_error_valid_iff (error : layout.MetadataCastError) :
+    isValid error ↔ True := by
+  cases error <;>
+    simp [isValid, RustModel.decode, layout.MetadataCastError.aeneasModel,
+      layout.MetadataCastError.decode, layout.MetadataCastError.decodeFields]
+
+@[simp, contract_simps] theorem cast_result_valid_iff
+    (r : core.result.Result (Usize × Usize) layout.MetadataCastError) : isValid r ↔ True := by
+  cases r <;> simp [result_valid_iff]
+
+attribute [contract_simps] option_valid_iff prod_valid_iff result_valid_iff
+  list_valid_iff slice_valid_iff
+
 @[contract_simps] theorem scalar_admitted_iff (x : UScalar ty) :
     (∃ value, RustModel.decode x = some value) ↔ True := scalar_valid_iff x
 
@@ -141,6 +159,12 @@ def layoutValid (self : layout.DstLayout) : Prop :=
 @[contract_simps] theorem bool_admitted_iff (x : Bool) :
     (∃ value, RustModel.decode x = some value) ↔ True := bool_valid_iff x
 
+@[contract_simps] theorem cast_type_admitted_iff (x : layout.CastType) :
+    (∃ value, RustModel.decode x = some value) ↔ True := cast_type_valid_iff x
+
+@[contract_simps] theorem cast_result_admitted_iff (x : core.result.Result (Usize × Usize) layout.MetadataCastError) :
+    (∃ value, RustModel.decode x = some value) ↔ True := cast_result_valid_iff x
+
 @[contract_simps] theorem option_admitted_iff {α : Type} [RustModel α] (x : Option α) :
     (∃ value : Option (ModelOf α), RustModel.decode x = some value) ↔
       ∀ v ∈ x, isValid v := option_valid_iff x
@@ -189,8 +213,6 @@ def layoutValid (self : layout.DstLayout) : Prop :=
 @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) :
     Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff
 
-attribute [contract_simps] option_valid_iff prod_valid_iff result_valid_iff
-
 attribute [contract_simps] and_true true_and and_self true_implies forall_true_iff
 attribute [contract_simps] encodingValid trailingValid sizeInfoValid layoutValid
 
diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean
index 3002b1cad9..912743afb0 100644
--- a/verification/aeneas/lean/Obligations.lean
+++ b/verification/aeneas/lean/Obligations.lean
@@ -348,6 +348,61 @@ def requires_dynamic_padding_spec : Prop :=
     requires_dynamic_padding_spec_contract self
       (layout.DstLayout.requires_dynamic_padding self)
 
+def validate_cast_spec_contract
+    (self : layout.DstLayout) (addr length : Usize) (side : layout.CastType)
+    (run : Result (core.result.Result (Usize × Usize) layout.MetadataCastError)) : Prop :=
+  layoutValid self →
+    0 < self.align.val.val → addr.val + length.val ≤ Usize.max →
+    (match self.size_info with
+      | .Sized _ => True
+      | .SliceDst t => 0 < t.size_rounding_align_and_phase._0.val.val ∧ 0 < t.elem_size.val) →
+    ∃ r, run = .ok r ∧
+      -- State the expected cases independently of the inline outcome helper.
+      let anchor := addr.val + (match side with | .Prefix => 0 | .Suffix => length.val)
+      match r with
+      | .Err .Alignment => anchor % self.align.val.val ≠ 0
+      | .Err .Size => anchor % self.align.val.val = 0 ∧
+        match self.size_info with
+        | .Sized bytes => length.val < bytes.val
+        | .SliceDst tail => ∀ n : Nat, length.val < (trailingFormula tail).size n
+      | .Ok (elems, split) => anchor % self.align.val.val = 0 ∧
+        match self.size_info with
+        | .Sized bytes => elems.val = 0 ∧ bytes.val ≤ length.val ∧
+          split.val = (match side with
+            | .Prefix => bytes.val
+            | .Suffix => length.val - bytes.val)
+        | .SliceDst tail => (trailingFormula tail).size elems.val ≤ length.val ∧
+          (∀ n : Nat, (trailingFormula tail).size n ≤ length.val ↔ n ≤ elems.val) ∧
+          split.val = (match side with
+            | .Prefix => (trailingFormula tail).size elems.val
+            | .Suffix => length.val - (trailingFormula tail).size elems.val)
+
+def validate_cast_spec : Prop :=
+  ∀ (self : layout.DstLayout) (addr length : Usize) (side : layout.CastType),
+    validate_cast_spec_contract self addr length side
+      (layout.DstLayout.validate_cast_and_convert_metadata self addr length side)
+
+def metadata_exact_spec_contract (self : layout.DstLayout) (size : Usize)
+    (run : Result (Option Usize)) : Prop :=
+  layoutValid self → 0 < self.align.val.val →
+    (match self.size_info with
+      | .Sized _ => True
+      | .SliceDst t => t.elem_size.val ≠ 0 → 0 < t.size_rounding_align_and_phase._0.val.val) →
+    ∃ r, run = .ok r ∧
+      -- Pin exact size and maximal metadata without sharing the inline predicate.
+      match self.size_info with
+      | .Sized _ => r = none
+      | .SliceDst tail =>
+        if tail.elem_size.val = 0 then r = none else
+        match r with
+        | none => ∀ n : Nat, (trailingFormula tail).size n ≠ size.val
+        | some elems => (trailingFormula tail).size elems.val = size.val ∧
+          (∀ n : Nat, (trailingFormula tail).size n ≤ size.val ↔ n ≤ elems.val)
+
+def metadata_exact_spec : Prop :=
+  ∀ (self : layout.DstLayout) (size : Usize),
+    metadata_exact_spec_contract self size (layout.DstLayout.metadata_for_exact_size self size)
+
 
 end Zerocopy.Obligations
 
diff --git a/verification/aeneas/lean/Obligations/TailChecks.lean b/verification/aeneas/lean/Obligations/TailChecks.lean
index 4fb4d750e6..8e271fb901 100644
--- a/verification/aeneas/lean/Obligations/TailChecks.lean
+++ b/verification/aeneas/lean/Obligations/TailChecks.lean
@@ -30,4 +30,15 @@ def trailing_arithmetic_check_spec : Prop :=
     trailing_arithmetic_check_spec_contract tail align phase elems budget
       (layout.tail_checks.trailing_arithmetic_check tail align phase elems budget)
 
+def layout_observations_check_spec_contract
+    (runtime_layout : layout.DstLayout) (align : NonZeroUsize)
+    (phase size addr length : Usize) (side : layout.CastType)
+    (run : Result Unit) : Prop :=
+  layoutValid runtime_layout → 0 < align.val.val → run ⦃ _ => True ⦄
+
+def layout_observations_check_spec : Prop :=
+  ∀ runtime_layout align phase size addr length side,
+    layout_observations_check_spec_contract runtime_layout align phase size addr length side
+      (layout.tail_checks.layout_observations_check runtime_layout align phase size addr length side)
+
 end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/OutcomeTests.lean b/verification/aeneas/lean/OutcomeTests.lean
new file mode 100644
index 0000000000..b3cf7db109
--- /dev/null
+++ b/verification/aeneas/lean/OutcomeTests.lean
@@ -0,0 +1,124 @@
+/- 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
+public import Mathlib.Tactic.NormNum
+@[expose] public section
+
+/-!
+Proof verification is only useful if the supplied outcome predicate rejects
+wrong answers. These numerical examples challenge the independent cast and
+metadata predicates directly: error priority, prefix versus suffix anchors,
+maximum metadata on padded-size plateaus, and zero-stride behavior. They do
+not run the extracted functions; they check what the predicates mean.
+-/
+open Aeneas Aeneas.Std Zerocopy Zerocopy.Proofs
+
+namespace Zerocopy.OutcomeTests
+
+-- Numerical boundary cases independently pin the inline outcome predicates.
+def fixedEight : layout.DstLayout :=
+  { align := ⟨4#usize⟩, size_info := .Sized 8#usize,
+    statically_shallow_unpadded := false }
+
+def plateauTail : layout.TrailingSliceLayout Usize :=
+  { offset := 0#usize, elem_size := 1#usize, size_base := 0#usize,
+    size_rounding_align_and_phase := ⟨⟨4#usize⟩⟩ }
+
+def plateauFour : layout.DstLayout :=
+  { align := ⟨4#usize⟩, size_info := .SliceDst plateauTail,
+    statically_shallow_unpadded := true }
+
+def zeroStride : layout.DstLayout :=
+  { plateauFour with size_info := .SliceDst { plateauTail with elem_size := 0#usize } }
+
+-- Incorrect Sized metadata is excluded even when the size and split fit.
+theorem rejects_wrong_sized_elems :
+    ¬ castSpec fixedEight 0 20 .Prefix (.Ok (1#usize, 8#usize)) := by
+  norm_num [castSpec, fixedEight, castSide, castSplit]
+
+-- Prefix and suffix splits differ when length is larger than twice the size.
+theorem rejects_wrong_prefix_split :
+    ¬ castSpec fixedEight 0 20 .Prefix (.Ok (0#usize, 12#usize)) := by
+  norm_num [castSpec, fixedEight, castSide, castSplit]
+
+theorem rejects_wrong_suffix_split :
+    ¬ castSpec fixedEight 0 20 .Suffix (.Ok (0#usize, 8#usize)) := by
+  norm_num [castSpec, fixedEight, castSide, castSplit]
+
+theorem admits_correct_suffix_split :
+    castSpec fixedEight 0 20 .Suffix (.Ok (0#usize, 12#usize)) := by
+  norm_num [castSpec, fixedEight, castSide, castSplit]
+
+-- Misalignment has priority over insufficient size.
+theorem rejects_wrong_error_priority :
+    ¬ castSpec fixedEight 1 0 .Prefix (.Err .Size) := by
+  norm_num [castSpec, fixedEight, castSide]
+
+theorem admits_alignment_before_size :
+    castSpec fixedEight 1 0 .Prefix (.Err .Alignment) := by
+  norm_num [castSpec, fixedEight, castSide]
+
+-- A suffix uses the end address: 1+3 is aligned even though 1 is not.
+theorem rejects_wrong_suffix_anchor :
+    ¬ castSpec fixedEight 1 3 .Suffix (.Err .Alignment) := by
+  norm_num [castSpec, fixedEight, castSide]
+
+theorem admits_suffix_size_error :
+    castSpec fixedEight 1 3 .Suffix (.Err .Size) := by
+  norm_num [castSpec, fixedEight, castSide]
+
+-- One element fits at length 4, but metadata must be the greatest fitting 4.
+theorem rejects_nonmaximal_cast_metadata :
+    ¬ castSpec plateauFour 0 4 .Prefix (.Ok (1#usize, 4#usize)) := by
+  intro h
+  have hmaximum := h.2.2.1 4
+  norm_num [trailingFormula, byteFormula, plateauFour, plateauTail,
+    LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp,
+    show Nat.log2 4 = 2 by decide] at hmaximum
+
+
+theorem rejects_fixed_metadata :
+    ¬ metadataSpec fixedEight 8 (some 1#usize) := by
+  simp [metadataSpec, fixedEight]
+
+theorem admits_no_fixed_metadata : metadataSpec fixedEight 8 none := by
+  simp [metadataSpec, fixedEight]
+
+theorem rejects_zero_stride_metadata :
+    ¬ metadataSpec zeroStride 4 (some 1#usize) := by
+  simp [metadataSpec, zeroStride, plateauFour, plateauTail]
+
+-- Returning none is incorrect when n=4 has exact complete size 4.
+theorem rejects_absent_exact_metadata :
+    ¬ metadataSpec plateauFour 4 none := by
+  intro h
+  have hmissing := h 4
+  norm_num [trailingFormula, byteFormula, plateauFour, plateauTail,
+    LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp,
+    show Nat.log2 4 = 2 by decide] at hmissing
+
+-- Exact complete size alone does not suffice on a padded-size plateau.
+theorem rejects_nonmaximal_exact_metadata :
+    ¬ metadataSpec plateauFour 4 (some 1#usize) := by
+  intro h
+  have hmaximum := h.2 4
+  norm_num [trailingFormula, byteFormula, plateauFour, plateauTail,
+    LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp,
+    show Nat.log2 4 = 2 by decide] at hmaximum
+
+theorem rejects_inexact_metadata :
+    ¬ metadataSpec plateauFour 3 (some 3#usize) := by
+  intro h
+  have hexact := h.1
+  norm_num [trailingFormula, byteFormula, plateauFour, plateauTail,
+    LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp,
+    show Nat.log2 4 = 2 by decide] at hexact
+
+end Zerocopy.OutcomeTests
diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean
index ca2345c17f..a15e1bdd5e 100644
--- a/verification/aeneas/lean/Proofs.lean
+++ b/verification/aeneas/lean/Proofs.lean
@@ -1144,6 +1144,269 @@ theorem same_size_sequence_spec :
               exact ⟨haveq, hpveq⟩
         · simp [WP.spec_ok]
 
+theorem cast_offset_spec (cast : layout.CastType) (length : Usize) :
+    (match cast with | .Prefix => Result.ok 0#usize | .Suffix => Result.ok length)
+      ⦃ offset => offset.val = castSide cast length.val ∧ offset ≤ length ⦄ := by
+  cases cast <;> simp [castSide, WP.spec_ok]
+
+theorem cast_split_spec (cast : layout.CastType) (length size elems : Usize)
+    (h : size.val ≤ length.val) :
+    (match cast with
+      | .Prefix => Result.ok (core.result.Result.Ok (elems, size))
+      | .Suffix => do
+        let split ← length - size
+        Result.ok (core.result.Result.Ok (elems, split)) :
+      Result (core.result.Result (Usize × Usize) layout.MetadataCastError))
+      ⦃ r => ∃ split, r = .Ok (elems, split) ∧
+        split.val = castSplit cast length.val size.val ⦄ := by
+  cases cast with
+  | Prefix => exact WP.spec.ret ⟨size, rfl, rfl⟩
+  | Suffix =>
+    step with Usize.sub_spec h as ⟨split, hs, _⟩
+    exact ⟨split, rfl, hs⟩
+
+/- Track alignment-error priority, complete-size capacity, and prefix/suffix
+splitting through the actual branches. A zero trailing stride intentionally
+panics and therefore lies outside this total contract's required domain.
+-/
+theorem validate_cast_spec :
+  ∀ (self : layout.DstLayout) (addr bytes_len : Usize) (cast_type : layout.CastType), ∀ (ha : (0 < self.align.val.val : Prop)), ∀ (hroom : (addr.val + bytes_len.val ≤ Usize.max : Prop)), ∀ (ht : (match self.size_info with
+    | .Sized _ => True
+    | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val ∧ 0 < tail.elem_size.val : Prop)),
+    @Zerocopy.layout.DstLayout.validate_cast_and_convert_metadata self addr bytes_len cast_type ⦃ r => castSpec self addr.val bytes_len.val cast_type r ⦄ := by
+  intro self addr length cast ha hroom ht
+  unfold layout.DstLayout.validate_cast_and_convert_metadata
+  cases hs : self.size_info with
+  | Sized size =>
+    step with try_nonzero_spec (.Sized size) as ⟨converted, hconverted⟩
+    rw [hconverted]
+    step as ⟨checked, haddr⟩
+    cases checked with
+    | none => simp only [] at haddr; omega
+    | some ending =>
+      simp only [] at haddr
+      simp only [Option.isSome_some, massert, if_true, bind_ok]
+      step with cast_offset_spec cast length as ⟨offset, ho, hle⟩
+      have hlen := (UScalar.le_equiv _ _).mp hle
+      step with Usize.add_spec (x := addr) (y := offset) (by omega) as ⟨aligned, haligned⟩
+      simp only [core.num.nonzero.NonZero.get, bind_ok]
+      step with Usize.rem_spec aligned (y := self.align.val) (by omega) as ⟨rem, hr⟩
+      simp only [bne_iff_ne]
+      split
+      · rename_i hne
+        apply WP.spec.ret
+        unfold castSpec
+        have hv : rem.val ≠ 0 := by
+          intro h
+          apply hne
+          exact (UScalar.eq_equiv _ _).mpr h
+        rw [hr, haligned, ho] at hv
+        exact hv
+      · rename_i heq
+        have hzero : (addr.val + castSide cast length.val) % self.align.val.val = 0 := by
+          have h : rem = 0#usize := not_ne_iff.mp heq
+          have hv := congrArg UScalar.val h
+          rw [hr, haligned, ho] at hv
+          exact hv
+        have htotal : (decide (size > length) || decide (size ≤ length)) = true := by
+          simp only [Bool.or_eq_true, decide_eq_true_eq]
+          exact lt_or_ge length size
+        simp only [UScalar.lt_equiv, UScalar.le_equiv] at htotal ⊢
+        simp only [htotal, if_true, bind_ok]
+        split
+        · rename_i hbig
+          apply WP.spec.ret
+          simp only [castSpec, hs]
+          exact ⟨hzero, hbig⟩
+        · rename_i hsmall
+          step with cast_split_spec cast length size 0#usize (by omega) as ⟨r, split, hr, hv⟩
+          rw [hr]
+          simp only [castSpec, hs, show (0#usize).val = 0 by simp]
+          exact ⟨hzero, trivial, by omega, hv⟩
+  | SliceDst tail =>
+    simp only [hs] at ht
+    step with try_nonzero_spec (.SliceDst tail) as ⟨converted, hconverted⟩
+    have hne : tail.elem_size ≠ 0#usize := by
+      intro h
+      have hv := congrArg UScalar.val h
+      change tail.elem_size.val = 0 at hv
+      omega
+    simp only [hne, if_false] at hconverted
+    obtain ⟨t, hconverted, hoffset, hbase, hcode, helem⟩ := hconverted
+    rw [hconverted]
+    step as ⟨checked, haddr⟩
+    cases checked with
+    | none => simp only [] at haddr; omega
+    | some ending =>
+      simp only [] at haddr
+      simp only [Option.isSome_some, massert, if_true, bind_ok]
+      step with cast_offset_spec cast length as ⟨offset, ho, hle⟩
+      have hlen := (UScalar.le_equiv _ _).mp hle
+      step with Usize.add_spec (x := addr) (y := offset) (by omega) as ⟨aligned, haligned⟩
+      simp only [core.num.nonzero.NonZero.get, bind_ok]
+      step with Usize.rem_spec aligned (y := self.align.val) (by omega) as ⟨rem, hr⟩
+      simp only [bne_iff_ne]
+      split
+      · rename_i hne
+        apply WP.spec.ret
+        unfold castSpec
+        have hv : rem.val ≠ 0 := by
+          intro h
+          apply hne
+          exact (UScalar.eq_equiv _ _).mpr h
+        rw [hr, haligned, ho] at hv
+        exact hv
+      · rename_i heq
+        have hzero : (addr.val + castSide cast length.val) % self.align.val.val = 0 := by
+          have h : rem = 0#usize := not_ne_iff.mp heq
+          have hv := congrArg UScalar.val h
+          rw [hr, haligned, ho] at hv
+          exact hv
+        have htn : 0 < t.size_rounding_align_and_phase._0.val.val := by rw [hcode]; exact ht.1
+        have hte : 0 < t.elem_size.val.val := by rw [helem]; exact ht.2
+        have hview : byteFormula t = byteFormula tail := by simp only [byteFormula, hbase, hcode, hoffset]
+        step with max_trailing_bytes_spec t length htn as ⟨capacity, hc⟩
+        rw [hview] at hc
+        cases capacity with
+        | none =>
+          have hmiss := LayoutMath.capacity_spec (byteFormula tail) length.val (Nat.two_pow_pos _)
+          rw [← hc] at hmiss
+          apply WP.spec.ret
+          refine ⟨hzero, ?_⟩
+          simp only [hs]
+          intro n
+          exact hmiss (n * tail.elem_size.val)
+        | some capacity =>
+          dsimp only
+          step with max_elems_for_bytes_spec capacity t.elem_size hte as ⟨elems, used, hen, _, _, _, _⟩
+          step with encoding_align_spec t.size_rounding_align_and_phase htn as ⟨a, ha⟩
+          have hav : a.val.val = (trailingFormula tail).align := by
+            simpa only [trailingFormula, byteFormula, hcode] using ha
+          step with Usize.rem_spec capacity (y := t.elem_size.val) (by omega) as ⟨unused, hu⟩
+          have hap : a.val.val.isPowerOfTwo := ⟨_, by simpa only [hcode] using ha⟩
+          step with round_down_spec unused a hap as ⟨unused_aligned, _, huf, _, _, _⟩
+          have hcap : (trailingFormula tail).capacity length.val = some capacity.val := hc.symm
+          have hmax := LayoutMath.maximal_metadata _ _ _ ht.2 hcap (trailing_align_pos tail)
+          have hfit : (trailingFormula tail).size elems.val ≤ length.val := by
+            apply (hmax elems.val).mpr
+            rw [hen, helem]
+            exact le_rfl
+          have hmin := (LayoutMath.capacity_spec (trailingFormula tail) length.val (trailing_align_pos tail))
+          rw [hcap] at hmin
+          have hminfit := (hmin 0).mpr (by omega)
+          have hbfit : t.size_base.val ≤ length.val := by
+            rw [hbase]
+            simp only [trailingFormula, byteFormula, LayoutMath.Formula.bytes] at hminfit
+            omega
+          step with Usize.sub_spec hbfit as ⟨available, hb, _⟩
+          step with round_down_spec available a hap as ⟨budget, _, hbudget, _, _, _⟩
+          have hused := LayoutMath.capacity_object_size (trailingFormula tail) length.val capacity.val
+            (trailing_align_pos tail) hcap
+          change (trailingFormula tail).size (capacity.val / tail.elem_size.val) =
+            tail.size_base.val + (length.val - tail.size_base.val -
+              (length.val - tail.size_base.val) % (trailingFormula tail).align) -
+              (capacity.val % tail.elem_size.val -
+                capacity.val % tail.elem_size.val % (trailingFormula tail).align) at hused
+          rw [← hav, ← hbase] at hused
+          have hunused : unused.val = capacity.val % tail.elem_size.val := by rw [hu, helem]
+          have hbval : budget.val = length.val - t.size_base.val -
+              (length.val - t.size_base.val) % a.val.val := by rw [hbudget, hb]
+          have hus : unused_aligned.val ≤ budget.val := by
+            have hmod := Nat.mod_le capacity.val tail.elem_size.val
+            have hcapval : capacity.val = length.val - t.size_base.val -
+                (length.val - t.size_base.val) % a.val.val - (trailingFormula tail).phase := by
+              unfold LayoutMath.Formula.capacity at hcap
+              simp only [hminfit, if_true, Option.some.injEq] at hcap
+              have hav' : a.val.val = 2 ^ tail.size_rounding_align_and_phase._0.val.val.log2 := hav
+              simpa only [trailingFormula, byteFormula, ← hav', ← hbase] using hcap.symm
+            rw [huf, hbval, hunused]
+            omega
+          step with Usize.sub_spec hus as ⟨remaining, hremaining, _⟩
+          have hsum : t.size_base.val + remaining.val ≤ Usize.max := by
+            have hlenfit : length.val ≤ Usize.max := by scalar_tac
+            rw [hremaining]
+            have hbudget_bound : budget.val ≤ length.val - t.size_base.val := by rw [hbval]; omega
+            omega
+          step with Usize.add_spec (x := t.size_base) (y := remaining) hsum as ⟨size, hsize⟩
+          have hexact : size.val = (trailingFormula tail).size elems.val := by
+            rw [hen, helem]
+            rw [hused]
+            rw [hsize, hremaining, huf, hunused, hbval]
+            rw [huf, hunused, hbval] at hus
+            omega
+          have hsizefit : size ≤ length := (UScalar.le_equiv _ _).mpr (by rw [hexact]; exact hfit)
+          simp only [hsizefit, if_true, bind_ok]
+          step with cast_split_spec cast length size elems (by rw [hexact]; exact hfit) as ⟨r, split, hr, hv⟩
+          rw [hr]
+          simp only [castSpec, hs]
+          refine ⟨hzero, hfit, ?_, ?_⟩
+          · intro n
+            rw [hmax n, hen, helem]
+            rfl
+          · simpa only [hexact] using hv
+
+/- Prove exact metadata inference, including rejection of unattainable sizes and
+greatest-count selection when several counts share the same padded size.
+-/
+theorem metadata_exact_spec :
+  ∀ (self : layout.DstLayout) (size : Usize), ∀ (ha : (0 < self.align.val.val : Prop)), ∀ (ht : (match self.size_info with
+    | .Sized _ => True
+    | .SliceDst tail => tail.elem_size.val ≠ 0 →
+      0 < tail.size_rounding_align_and_phase._0.val.val : Prop)),
+    @Zerocopy.layout.DstLayout.metadata_for_exact_size self size ⦃ r => metadataSpec self size.val r ⦄ := by
+  intro self size ha ht
+  unfold layout.DstLayout.metadata_for_exact_size
+  cases hs : self.size_info with
+  | Sized s => simp only [WP.spec_ok, metadataSpec, hs]
+  | SliceDst tail =>
+    simp only [hs] at ht ⊢
+    cases hz : tail.elem_size.val with
+    | zero =>
+      simp only [WP.spec_ok, metadataSpec, hs, hz, if_true]
+    | succ k =>
+      simp only []
+      have he : 0 < tail.elem_size.val := by omega
+      have hn : tail.elem_size.val ≠ 0 := by omega
+      step with validate_cast_spec self 0#usize size .Prefix ha (by scalar_tac)
+        (by simp only [hs]; exact ⟨ht hn, he⟩) as ⟨cast, hc⟩
+      cases cast with
+      | Err err =>
+        cases err with
+        | Alignment =>
+          simp only [castSpec, castSide, Nat.zero_add, Nat.zero_mod,
+            ] at hc
+          exact False.elim (hc rfl)
+        | Size =>
+          simp only [castSpec, castSide, hs,
+            Nat.zero_add, Nat.zero_mod, true_and] at hc
+          apply WP.spec.ret
+          simp only [metadataSpec, hs, hn, if_false]
+          intro n h
+          have := hc n
+          omega
+      | Ok pair =>
+        rcases pair with ⟨elems, bytes⟩
+        change (if bytes = size then Result.ok (some elems) else Result.ok none)
+          ⦃ r => metadataSpec self size.val r ⦄
+        simp only [castSpec, castSide, castSplit, hs,
+          Nat.zero_add, Nat.zero_mod, true_and] at hc
+        split
+        · rename_i hsame
+          apply WP.spec.ret
+          simp only [metadataSpec, hs, hn, if_false]
+          have hbytes := congrArg UScalar.val hsame
+          exact ⟨by omega, hc.2.1⟩
+        · rename_i hdiff
+          apply WP.spec.ret
+          simp only [metadataSpec, hs, hn, if_false]
+          intro n h
+          have hle : n ≤ elems.val := (hc.2.1 n).mp (by omega)
+          have hmono := LayoutMath.Formula.size_mono (trailingFormula tail)
+            (trailing_align_pos tail) hle
+          apply hdiff
+          apply (UScalar.eq_equiv _ _).mpr
+          omega
+
 /- Lift detailed raw extension facts to the independent fragment operation. This
 supplies the constructor loop's mathematical state transition.
 -/
@@ -1436,6 +1699,50 @@ theorem requires_dynamic_padding_spec : Zerocopy.Specs.requires_dynamic_padding_
   | SliceDst _ => simpa only [hs] using hv.2
 register_spec_step requires_dynamic_padding_spec
 
+/- Prove exact metadata inference, including rejection of unattainable sizes and
+greatest-count selection when several counts share the same padded size.
+-/
+theorem metadata_exact_spec : Zerocopy.Specs.metadata_exact_spec := by
+  unfold Zerocopy.Specs.metadata_exact_spec
+  representation_simps
+  intro self size hv
+  have ht : match self.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => tail.elem_size.val ≠ 0 →
+        0 < tail.size_rounding_align_and_phase._0.val.val := by
+    cases hs : self.size_info with
+    | Sized _ => trivial
+    | SliceDst tail =>
+      simp only [hs] at hv
+      intro _
+      exact hv.2
+  apply WP.spec_mono (Raw.metadata_exact_spec self size hv.1 ht)
+  intro result facts
+  refine ⟨?_, facts⟩
+  change isValid result
+  simp
+register_spec_step metadata_exact_spec
+
+/- Track alignment-error priority, complete-size capacity, and prefix/suffix
+splitting through the actual branches. A zero trailing stride intentionally
+panics and therefore lies outside this total contract's required domain.
+-/
+theorem validate_cast_spec : Zerocopy.Specs.validate_cast_spec := by
+  unfold Zerocopy.Specs.validate_cast_spec
+  representation_simps
+  intro self addr length side hv hroom helem
+  have ht : match self.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val ∧
+        0 < tail.elem_size.val := by
+    cases hs : self.size_info with
+    | Sized _ => trivial
+    | SliceDst tail =>
+      simp only [hs] at hv helem
+      exact ⟨hv.2, helem⟩
+  exact Raw.validate_cast_spec self addr length side hv.1 hroom ht
+register_spec_step validate_cast_spec
+
 end Zerocopy.Proofs
 
 namespace Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/TailChecks.lean b/verification/aeneas/lean/Proofs/TailChecks.lean
index 2323571ddc..c4d9d6657a 100644
--- a/verification/aeneas/lean/Proofs/TailChecks.lean
+++ b/verification/aeneas/lean/Proofs/TailChecks.lean
@@ -68,6 +68,150 @@ theorem trailing_arithmetic_check (tail : layout.TrailingSliceLayout Usize)
     · simp only [WP.spec_ok]
   · simp only [WP.spec_ok]
 
+theorem encoding_guard_spec (runtime_layout : layout.DstLayout)
+    (align : NonZeroUsize) (phase : Usize) :
+    (match (generalizing := false) runtime_layout.size_info with
+      | .Sized _ => Result.ok (runtime_layout.size_info, true)
+      | .SliceDst tail => do
+        let power ← core.num.Usize.is_power_of_two align.val
+        let code_matches ←
+          if power then
+            if phase < align.val then
+              do
+              let encoded ← lift (Usize.checked_add align.val phase)
+              layout.tail_checks.same_optional_usize encoded (some tail.size_rounding_align_and_phase._0.val)
+            else Result.ok false
+          else Result.ok false
+        Result.ok (runtime_layout.size_info, code_matches)) ⦃ pair =>
+      pair.1 = runtime_layout.size_info ∧
+        (pair.2 = true → witnessMatches runtime_layout align phase) ⦄ := by
+  cases info_eq : runtime_layout.size_info with
+  | Sized bytes => simp [WP.spec_ok, witnessMatches, info_eq]
+  | SliceDst tail =>
+    step as ⟨power, power_iff⟩
+    split
+    · rename_i power_true
+      have power_fact : align.val.val.isPowerOfTwo := Eq.mp power_iff power_true
+      simp only [UScalar.lt_equiv]
+      split
+      · rename_i phase_lt
+        step as ⟨encoded, encoded_facts⟩
+        step with same_optional_usize encoded
+          (some tail.size_rounding_align_and_phase._0.val) as ⟨code_matches, matches_iff⟩
+        simp only [WP.spec_ok, Prod.fst, Prod.snd, witnessMatches, info_eq]
+        intro matches_true
+        have same_code := matches_iff.mp matches_true
+        rw [same_code] at encoded_facts
+        exact ⟨power_fact, phase_lt, encoded_facts.2.1⟩
+      · simp [bind_ok, WP.spec_ok]
+    · simp [bind_ok, WP.spec_ok]
+
+theorem witness_positive (runtime_layout : layout.DstLayout)
+    (align : NonZeroUsize) (phase : Usize)
+    (witness : witnessMatches runtime_layout align phase) :
+    match runtime_layout.size_info with
+    | .Sized _ => True
+    | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val := by
+  cases info_eq : runtime_layout.size_info with
+  | Sized bytes => trivial
+  | SliceDst tail =>
+    simp only [witnessMatches, info_eq] at witness
+    have positive := Nat.pos_of_isPowerOfTwo witness.1
+    omega
+
+theorem layout_observations_check (runtime_layout : layout.DstLayout)
+    (align : NonZeroUsize) (phase size addr length : Usize) (side : layout.CastType)
+    (layout_positive : 0 < runtime_layout.align.val.val) (align_positive : 0 < align.val.val) :
+    layout.tail_checks.layout_observations_check runtime_layout align phase size addr length side ⦃ _ => True ⦄ := by
+  unfold layout.tail_checks.layout_observations_check
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  change (Aeneas.Std.bind (match (generalizing := false) runtime_layout.size_info with
+      | .Sized _ => Result.ok (runtime_layout.size_info, true)
+      | .SliceDst tail => do
+        let power ← core.num.Usize.is_power_of_two align.val
+        let code_matches ←
+          if power then
+            if phase < align.val then
+              do
+              let encoded ← lift (Usize.checked_add align.val phase)
+              layout.tail_checks.same_optional_usize encoded (some tail.size_rounding_align_and_phase._0.val)
+            else Result.ok false
+          else Result.ok false
+        Result.ok (runtime_layout.size_info, code_matches)) _) ⦃ _ ⦄
+  step with encoding_guard_spec runtime_layout align phase as ⟨info, code_matches, same_info, when_matches⟩
+  subst info
+  split
+  · rename_i matches_true
+    have witness := when_matches matches_true
+    have positive := witness_positive runtime_layout align phase witness
+    have meta_domain : match runtime_layout.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => tail.elem_size.val ≠ 0 → 0 < tail.size_rounding_align_and_phase._0.val.val := by
+      cases info_eq : runtime_layout.size_info with
+      | Sized bytes => trivial
+      | SliceDst tail =>
+        simp only [info_eq] at positive ⊢
+        intro nonzero
+        exact positive
+    step with Zerocopy.Proofs.Raw.metadata_exact_spec runtime_layout size layout_positive meta_domain
+      as ⟨actual_metadata, actual_metadata_spec⟩
+    step with reference_metadata runtime_layout align phase size align_positive witness
+      as ⟨expected_metadata, expected_metadata_spec⟩
+    have metadata_same := metadata_unique runtime_layout size.val actual_metadata expected_metadata
+      actual_metadata_spec expected_metadata_spec
+    step with same_optional_usize actual_metadata expected_metadata as ⟨same_metadata, same_metadata_iff⟩
+    have metadata_true := same_metadata_iff.mpr metadata_same
+    simp only [massert, metadata_true, if_true, bind_ok]
+    cases info_eq : runtime_layout.size_info with
+    | Sized bytes =>
+      simp only [info_eq, bind_ok]
+      have updated_eq : { runtime_layout with size_info := .Sized bytes } = runtime_layout := by
+        rw [← info_eq]
+      rw [updated_eq]
+      step as ⟨ending, ending_facts⟩
+      cases ending with
+      | none => simp [Option.isSome, WP.spec_ok]
+      | some ending =>
+        simp only [] at ending_facts
+        simp only [Option.isSome, if_true]
+        have room : addr.val + length.val ≤ Usize.max := ending_facts.1
+        step with Zerocopy.Proofs.Raw.validate_cast_spec runtime_layout addr length side layout_positive room
+          (by simp only [info_eq]) as ⟨actual, actual_spec⟩
+        step with reference_cast runtime_layout align phase addr length side layout_positive align_positive room witness
+          (by simp only [info_eq]) as ⟨expected, expected_spec⟩
+        have same := cast_unique runtime_layout addr.val length.val side actual expected actual_spec expected_spec
+        subst expected
+        cases actual with
+        | Ok pair => rcases pair with ⟨elems, split⟩; simp [massert, WP.spec_ok]
+        | Err error => cases error <;> simp [massert, WP.spec_ok]
+    | SliceDst tail =>
+      simp only [info_eq, bind_ok]
+      simp only [info_eq] at positive
+      have updated_eq : { runtime_layout with size_info := .SliceDst tail } = runtime_layout := by
+        rw [← info_eq]
+      rw [updated_eq]
+      step as ⟨ending, ending_facts⟩
+      cases ending with
+      | none => simp [Option.isSome, WP.spec_ok]
+      | some ending =>
+        simp only [] at ending_facts
+        simp only [Option.isSome, if_true, bne_iff_ne]
+        split
+        · rename_i stride_nonzero
+          have stride : 0 < tail.elem_size.val := by scalar_tac
+          have room : addr.val + length.val ≤ Usize.max := ending_facts.1
+          step with Zerocopy.Proofs.Raw.validate_cast_spec runtime_layout addr length side layout_positive room
+            (by simpa only [info_eq] using And.intro positive stride) as ⟨actual, actual_spec⟩
+          step with reference_cast runtime_layout align phase addr length side layout_positive align_positive room witness
+            (by simpa only [info_eq] using stride) as ⟨expected, expected_spec⟩
+          have same := cast_unique runtime_layout addr.val length.val side actual expected actual_spec expected_spec
+          subst expected
+          cases actual with
+          | Ok pair => rcases pair with ⟨elems, split⟩; simp [massert, WP.spec_ok]
+          | Err error => cases error <;> simp [massert, WP.spec_ok]
+        · simp only [WP.spec_ok]
+  · simp only [WP.spec_ok]
+
 end Zerocopy.Proofs.Raw.TailChecks
 
 namespace Zerocopy.Proofs
@@ -80,4 +224,16 @@ theorem trailing_arithmetic_check_spec : Specs.trailing_arithmetic_check_spec :=
   intro result facts
   exact ⟨(), rfl, trivial⟩
 
+theorem layout_observations_check_spec : Specs.layout_observations_check_spec := by
+  unfold Specs.layout_observations_check_spec
+  intro runtime_layout align phase size addr length side runtime_value runtime_decoded
+    align_value align_decoded phase_value phase_decoded size_value size_decoded
+    addr_value addr_decoded length_value length_decoded side_value side_decoded
+  have runtime_valid := (layout_valid_iff runtime_layout).mp ⟨runtime_value, runtime_decoded⟩
+  have align_valid := (nonzero_valid_iff align).mp ⟨align_value, align_decoded⟩
+  apply WP.spec_mono (Raw.TailChecks.layout_observations_check runtime_layout align phase size addr length side
+    runtime_valid.1 align_valid)
+  intro result facts
+  exact ⟨(), rfl, trivial⟩
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/TailReference.lean b/verification/aeneas/lean/Proofs/TailReference.lean
index 6357054a1c..0bd38440a5 100644
--- a/verification/aeneas/lean/Proofs/TailReference.lean
+++ b/verification/aeneas/lean/Proofs/TailReference.lean
@@ -234,4 +234,252 @@ theorem reference_capacity (tail : layout.TrailingSliceLayout Usize)
       congr 1
       omega
 
+theorem metadata_unique (runtime_layout : layout.DstLayout) (size : Nat)
+    (left right : Option Usize)
+    (left_spec : metadataSpec runtime_layout size left)
+    (right_spec : metadataSpec runtime_layout size right) : left = right := by
+  cases info_eq : runtime_layout.size_info with
+  | Sized bytes =>
+    simp only [metadataSpec, info_eq] at left_spec right_spec
+    rw [left_spec, right_spec]
+  | SliceDst tail =>
+    by_cases zero : tail.elem_size.val = 0
+    · simp only [metadataSpec, info_eq, zero, if_true] at left_spec right_spec
+      rw [left_spec, right_spec]
+    · simp only [metadataSpec, info_eq, zero, if_false] at left_spec right_spec
+      cases left with
+      | none =>
+        cases right with
+        | none => rfl
+        | some right => exact False.elim (left_spec right.val right_spec.1)
+      | some left =>
+        cases right with
+        | none => exact False.elim (right_spec left.val left_spec.1)
+        | some right =>
+          have le_right := (right_spec.2 left.val).mp (by omega)
+          have le_left := (left_spec.2 right.val).mp (by omega)
+          congr 1
+          exact UScalar.eq_of_val_eq (by omega)
+
+theorem cast_unique (runtime_layout : layout.DstLayout) (addr length : Nat)
+    (side : layout.CastType)
+    (left right : core.result.Result (Usize × Usize) layout.MetadataCastError)
+    (left_spec : castSpec runtime_layout addr length side left)
+    (right_spec : castSpec runtime_layout addr length side right) : left = right := by
+  cases left with
+  | Ok left =>
+    rcases left with ⟨left_elems, left_split⟩
+    cases right with
+    | Err error =>
+      cases error with
+      | Alignment => exact False.elim (right_spec left_spec.1)
+      | Size =>
+        cases info_eq : runtime_layout.size_info with
+        | Sized bytes => simp only [castSpec, info_eq] at left_spec right_spec; omega
+        | SliceDst tail =>
+          simp only [castSpec, info_eq] at left_spec right_spec
+          have miss := right_spec.2 left_elems.val
+          omega
+    | Ok right =>
+      rcases right with ⟨right_elems, right_split⟩
+      cases info_eq : runtime_layout.size_info with
+      | Sized bytes =>
+        simp only [castSpec, info_eq] at left_spec right_spec
+        have elems_eq : left_elems = right_elems := UScalar.eq_of_val_eq (by omega)
+        have split_eq : left_split = right_split := UScalar.eq_of_val_eq (by omega)
+        rw [elems_eq, split_eq]
+      | SliceDst tail =>
+        simp only [castSpec, info_eq] at left_spec right_spec
+        have le_right := (right_spec.2.2.1 left_elems.val).mp left_spec.2.1
+        have le_left := (left_spec.2.2.1 right_elems.val).mp right_spec.2.1
+        have elems_eq : left_elems = right_elems := UScalar.eq_of_val_eq (by omega)
+        have split_eq : left_split = right_split := UScalar.eq_of_val_eq (by
+          rw [elems_eq] at left_spec
+          omega)
+        rw [elems_eq, split_eq]
+  | Err left_error =>
+    cases right with
+    | Ok right =>
+      rcases right with ⟨right_elems, right_split⟩
+      cases left_error with
+      | Alignment => exact False.elim (left_spec right_spec.1)
+      | Size =>
+        cases info_eq : runtime_layout.size_info with
+        | Sized bytes => simp only [castSpec, info_eq] at left_spec right_spec; omega
+        | SliceDst tail =>
+          simp only [castSpec, info_eq] at left_spec right_spec
+          have miss := left_spec.2 right_elems.val
+          omega
+    | Err right_error =>
+      cases left_error <;> cases right_error <;> simp_all [castSpec]
+
+theorem reference_cast (runtime_layout : layout.DstLayout) (align : NonZeroUsize)
+    (phase addr length : Usize) (side : layout.CastType)
+    (layout_positive : 0 < runtime_layout.align.val.val)
+    (align_positive : 0 < align.val.val)
+    (room : addr.val + length.val ≤ Usize.max)
+    (witness : witnessMatches runtime_layout align phase)
+    (stride : match runtime_layout.size_info with | .Sized _ => True | .SliceDst t => 0 < t.elem_size.val) :
+    layout.tail_checks.reference_cast runtime_layout align phase addr length side ⦃ result =>
+      castSpec runtime_layout addr.val length.val side result ⦄ := by
+  have anchor_spec : (match side with
+      | .Prefix => Result.ok addr
+      | .Suffix => addr + length) ⦃ anchor => anchor.val = addr.val + castSide side length.val ⦄ := by
+    cases side with
+    | Prefix => simp [WP.spec_ok, castSide]
+    | Suffix =>
+      apply WP.spec_mono (Usize.add_spec (x := addr) (y := length) room)
+      intro result facts
+      simpa only [castSide] using facts
+  unfold layout.tail_checks.reference_cast
+  change ((match side with
+    | .Prefix => Result.ok addr
+    | .Suffix => addr + length) >>= _) ⦃ result => castSpec runtime_layout addr.val length.val side result ⦄
+  step with anchor_spec as ⟨anchor, anchor_value⟩
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  step with Usize.rem_spec anchor (y := runtime_layout.align.val) (by omega) as ⟨remainder, remainder_value⟩
+  rw [anchor_value] at remainder_value
+  simp only [bne_iff_ne, UScalar.eq_equiv, UScalar.ofNatCore_val_eq]
+  split
+  · rename_i not_aligned
+    simp only [ne_eq, UScalar.eq_equiv, UScalar.ofNatCore_val_eq] at not_aligned
+    apply WP.spec.ret
+    change (addr.val + castSide side length.val) % runtime_layout.align.val.val ≠ 0
+    rwa [← remainder_value]
+  · rename_i aligned
+    simp only [ne_eq, not_not, UScalar.eq_equiv, UScalar.ofNatCore_val_eq] at aligned
+    have anchor_aligned : (addr.val + castSide side length.val) % runtime_layout.align.val.val = 0 := by omega
+    cases info_eq : runtime_layout.size_info with
+    | Sized size =>
+      simp only [info_eq, bind_ok]
+      split
+      · rename_i size_fits
+        have fits : size.val ≤ length.val := (UScalar.le_equiv _ _).mp size_fits
+        cases side with
+        | Prefix =>
+          simp only [bind_ok, WP.spec_ok, castSpec, info_eq, castSplit, UScalar.ofNatCore_val_eq]
+          exact ⟨anchor_aligned, rfl, fits, rfl⟩
+        | Suffix =>
+          step with Usize.sub_spec (x := length) (y := size) fits as ⟨split, split_value⟩
+          simp only [castSpec, info_eq, castSplit, UScalar.ofNatCore_val_eq]
+          exact ⟨anchor_aligned, trivial, fits, split_value⟩
+      · rename_i size_misses
+        simp only [bind_ok, WP.spec_ok, castSpec, info_eq]
+        exact ⟨anchor_aligned, by scalar_tac⟩
+    | SliceDst tail =>
+      simp only [witnessMatches, info_eq] at witness
+      simp only [info_eq] at stride ⊢
+      have formula_eq := witness_view tail align phase witness.1 witness.2.1 witness.2.2
+      let f := witnessFormula tail align phase
+      step with reference_capacity tail align phase length align_positive as ⟨capacity, capacity_value⟩
+      have capacity_spec := LayoutMath.capacity_spec f length.val align_positive
+      cases capacity with
+      | none =>
+        simp only [Option.map_none] at capacity_value
+        rw [← capacity_value] at capacity_spec
+        simp only [bind_ok, WP.spec_ok, castSpec, info_eq]
+        refine ⟨anchor_aligned, ?_⟩
+        intro n
+        rw [formula_eq]
+        exact capacity_spec (n * tail.elem_size.val)
+      | some capacity =>
+        simp only [Option.map_some] at capacity_value
+        step with Usize.div_spec capacity (y := tail.elem_size) (by omega) as ⟨elems, elems_value⟩
+        have greatest : ∀ n, f.size n ≤ length.val ↔ n ≤ elems.val := by
+          have maximal := LayoutMath.maximal_metadata f length.val capacity.val stride
+            capacity_value.symm align_positive
+          simpa only [f, witnessFormula, elems_value] using maximal
+        have selected_fits := (greatest elems.val).mpr (by rfl)
+        have checked_fits : f.size elems.val ≤ Usize.max := by scalar_tac
+        step with reference_size tail align phase elems align_positive as ⟨selected_size, selected_value⟩
+        have selected_exact : selected_size.map UScalar.val = some (f.size elems.val) := by
+          change selected_size.map UScalar.val = f.checkedSize Usize.max elems.val at selected_value
+          simpa only [LayoutMath.Formula.checkedSize, checked_fits, if_true] using selected_value
+        cases selected_size with
+        | none => cases selected_exact
+        | some selected_size =>
+          have size_value : selected_size.val = f.size elems.val := Option.some.inj selected_exact
+          have fits : selected_size.val ≤ length.val := by rw [size_value]; exact selected_fits
+          change selected_size.val = (witnessFormula tail align phase).size elems.val at size_value
+          cases side with
+          | Prefix =>
+            simp only [bind_ok, WP.spec_ok, castSpec, info_eq, castSplit]
+            rw [formula_eq]
+            exact ⟨anchor_aligned, selected_fits, greatest, size_value⟩
+          | Suffix =>
+            simp only [bind_ok]
+            step with Usize.sub_spec (x := length) (y := selected_size) fits as ⟨split, split_value⟩
+            simp only [castSpec, info_eq, castSplit]
+            rw [formula_eq]
+            exact ⟨anchor_aligned, selected_fits, greatest, by omega⟩
+
+theorem reference_metadata (runtime_layout : layout.DstLayout) (align : NonZeroUsize)
+    (phase size : Usize) (align_positive : 0 < align.val.val)
+    (witness : witnessMatches runtime_layout align phase) :
+    layout.tail_checks.reference_metadata runtime_layout align phase size ⦃ result =>
+      metadataSpec runtime_layout size.val result ⦄ := by
+  unfold layout.tail_checks.reference_metadata
+  cases info_eq : runtime_layout.size_info with
+  | Sized bytes => simp only [WP.spec_ok, metadataSpec, info_eq]
+  | SliceDst tail =>
+    simp only [witnessMatches, info_eq] at witness
+    have formula_eq := witness_view tail align phase witness.1 witness.2.1 witness.2.2
+    let f := witnessFormula tail align phase
+    simp only [info_eq, UScalar.eq_equiv, UScalar.ofNatCore_val_eq]
+    split
+    · rename_i zero
+      simp only [WP.spec_ok, metadataSpec, info_eq, zero, if_true]
+    · rename_i nonzero
+      have stride : 0 < tail.elem_size.val := by omega
+      step with reference_capacity tail align phase size align_positive as ⟨capacity, capacity_value⟩
+      have capacity_spec := LayoutMath.capacity_spec f size.val align_positive
+      cases capacity with
+      | none =>
+        simp only [Option.map_none] at capacity_value
+        rw [← capacity_value] at capacity_spec
+        simp only [WP.spec_ok, metadataSpec, info_eq, nonzero, if_false]
+        intro n exact_size
+        have misses := capacity_spec (n * tail.elem_size.val)
+        rw [formula_eq] at exact_size
+        change size.val < f.size n at misses
+        change f.size n = size.val at exact_size
+        omega
+      | some capacity =>
+        simp only [Option.map_some] at capacity_value
+        step with Usize.div_spec capacity (y := tail.elem_size) (by omega) as ⟨elems, elems_value⟩
+        have greatest : ∀ n, f.size n ≤ size.val ↔ n ≤ elems.val := by
+          have maximal := LayoutMath.maximal_metadata f size.val capacity.val stride
+            capacity_value.symm align_positive
+          simpa only [f, witnessFormula, elems_value] using maximal
+        have selected_fits := (greatest elems.val).mpr (by rfl)
+        have checked_fits : f.size elems.val ≤ Usize.max := by scalar_tac
+        step with reference_size tail align phase elems align_positive as ⟨selected_size, selected_value⟩
+        have selected_exact : selected_size.map UScalar.val = some (f.size elems.val) := by
+          change selected_size.map UScalar.val = f.checkedSize Usize.max elems.val at selected_value
+          simpa only [LayoutMath.Formula.checkedSize, checked_fits, if_true] using selected_value
+        cases selected_size with
+        | none => cases selected_exact
+        | some selected_size =>
+          have size_value : selected_size.val = f.size elems.val := Option.some.inj selected_exact
+          step with same_optional_usize (some selected_size) (some size) as ⟨same, same_iff⟩
+          split
+          · rename_i same_true
+            have same_size := Option.some.inj (same_iff.mp same_true)
+            simp only [WP.spec_ok, metadataSpec, info_eq, nonzero, if_false]
+            rw [formula_eq]
+            exact ⟨by rw [← size_value, same_size], greatest⟩
+          · rename_i different
+            have different_size : selected_size ≠ size := by
+              intro same_size
+              exact different (same_iff.mpr (by rw [same_size]))
+            simp only [WP.spec_ok, metadataSpec, info_eq, nonzero, if_false]
+            intro n exact_size
+            rw [formula_eq] at exact_size
+            change f.size n = size.val at exact_size
+            have count_le := (greatest n).mp (by omega)
+            have monotone := LayoutMath.Formula.size_mono f align_positive count_le
+            apply different_size
+            apply UScalar.eq_of_val_eq
+            omega
+
 end Zerocopy.Proofs.Raw.TailChecks
diff --git a/verification/aeneas/lean/RequiredModelContracts.lean b/verification/aeneas/lean/RequiredModelContracts.lean
index efb0a1c6e8..96ff2be744 100644
--- a/verification/aeneas/lean/RequiredModelContracts.lean
+++ b/verification/aeneas/lean/RequiredModelContracts.lean
@@ -143,4 +143,48 @@ attribute [contract_simps] encoding_decoder_admitted_iff trailing_decoder_admitt
     simpa only [option_valid_iff, size_info_valid_iff] using valid
   · cases self <;> simpa only using facts
 
+@[contract_simps] theorem required_metadata_exact (self : layout.DstLayout) (size : Usize)
+    (run : Result (Option Usize)) (provided : Specs.metadata_exact_spec_contract self size run) :
+    Obligations.metadata_exact_spec_contract self size run := by
+  intro valid _align _rounding
+  obtain ⟨value, decoded⟩ := (layout_decoder_admitted_iff self).mpr valid
+  have result := provided value decoded (unsignedWord size) rfl
+  simp only [WP.spec_equiv_exists] at result
+  obtain ⟨output, call, math, admitted, facts⟩ := result
+  refine ⟨output, call, ?_⟩
+  cases info : self.size_info <;> cases output <;>
+    simp only [metadataSpec, info] at facts ⊢
+  all_goals exact facts
+
+@[contract_simps] theorem required_validate_cast (self : layout.DstLayout)
+    (addr length : Usize) (side : layout.CastType)
+    (run : Result (core.result.Result (Usize × Usize) layout.MetadataCastError))
+    (provided : Specs.validate_cast_spec_contract self addr length side run) :
+    Obligations.validate_cast_spec_contract self addr length side run := by
+  intro valid _align room trailing
+  obtain ⟨value, decoded⟩ := (layout_decoder_admitted_iff self).mpr valid
+  obtain ⟨sideValue, sideDecoded⟩ := (cast_type_valid_iff side).mpr trivial
+  have elems : match self.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => 0 < tail.elem_size.val := by
+    cases info : self.size_info with
+    | Sized _ => trivial
+    | SliceDst _ =>
+      simp only [info] at trailing
+      exact trailing.2
+  have result := provided value decoded (unsignedWord addr) rfl
+    (unsignedWord length) rfl sideValue sideDecoded room elems
+  simp only [WP.spec_equiv_exists] at result
+  obtain ⟨output, call, math, admitted, facts⟩ := result
+  refine ⟨output, call, ?_⟩
+  cases output with
+  | Err error =>
+    cases error <;> cases side <;> cases info : self.size_info <;>
+      simpa only [castSpec, castSide, castSplit, info] using facts
+  | Ok pair =>
+    rcases pair with ⟨count, split⟩
+    cases side <;> cases info : self.size_info <;>
+      simpa only [castSpec, castSide, castSplit, info] using facts
+
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean b/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean
index bbe3d294a6..418b8197c6 100644
--- a/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean
+++ b/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean
@@ -33,4 +33,22 @@ supplied arbitrary-outcome contract. These adapters do not run either check.
   rintro result ⟨value, decoded, facts⟩
   trivial
 
+@[contract_simps] theorem required_layout_observations_check
+    (runtime_layout : layout.DstLayout) (align : NonZeroUsize)
+    (phase size addr length : Usize) (side : layout.CastType) (run : Result Unit)
+    (provided : Specs.layout_observations_check_spec_contract
+      runtime_layout align phase size addr length side run) :
+    Obligations.layout_observations_check_spec_contract
+      runtime_layout align phase size addr length side run := by
+  intro valid_runtime align_positive
+  obtain ⟨layout_value, decoded_layout⟩ := (layout_valid_iff runtime_layout).mpr valid_runtime
+  let av : NonZeroUsizeValue := ⟨unsignedWord align.val, align_positive⟩
+  have decoded_align := (decodeNonZeroUScalar_iff align av).mpr rfl
+  obtain ⟨side_value, decoded_side⟩ := (cast_type_valid_iff side).mpr trivial
+  apply WP.spec_mono (provided layout_value decoded_layout av decoded_align
+    (unsignedWord phase) rfl (unsignedWord size) rfl (unsignedWord addr) rfl
+    (unsignedWord length) rfl side_value decoded_side)
+  rintro result ⟨value, decoded, facts⟩
+  trivial
+
 end Zerocopy.Proofs
diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs
index 97d37f8543..d2d0ccf852 100644
--- a/zerocopy/src/layout/mod.rs
+++ b/zerocopy/src/layout/mod.rs
@@ -1693,6 +1693,11 @@ impl DstLayout {
             _ => None,
         }
     }))]
+    ///
+    /// ```aeneas
+    /// spec metadata_exact_spec
+    ///   ensures(raw) r => metadataSpec self size.val r
+    /// ```
     const fn metadata_for_exact_size(&self, size: usize) -> Option<usize> {
         #[cfg(kani)]
         #[kani::proof_for_contract(DstLayout::metadata_for_exact_size)]
@@ -1822,6 +1827,15 @@ impl DstLayout {
             _ => false,
         }
     }))]
+    ///
+    /// ```aeneas
+    /// spec validate_cast_spec
+    ///   requires(raw) hroom : addr.val + bytes_len.val ≤ Usize.max
+    ///   requires(raw) ht : match self.size_info with
+    ///     | .Sized _ => True
+    ///     | .SliceDst tail => 0 < tail.elem_size.val
+    ///   ensures(raw) r => castSpec self addr.val bytes_len.val cast_type r
+    /// ```
     pub(crate) const fn validate_cast_and_convert_metadata(
         &self,
         addr: usize,
diff --git a/zerocopy/src/layout/tail_checks.rs b/zerocopy/src/layout/tail_checks.rs
index 2a0e616841..bd31bbfcf8 100644
--- a/zerocopy/src/layout/tail_checks.rs
+++ b/zerocopy/src/layout/tail_checks.rs
@@ -24,7 +24,7 @@
 
 use core::num::NonZeroUsize;
 
-use super::TrailingSliceLayout;
+use super::{CastType, DstLayout, MetadataCastError, SizeInfo, TrailingSliceLayout};
 
 pub(crate) fn same_optional_usize(left: Option<usize>, right: Option<usize>) -> bool {
     match (left, right) {
@@ -75,6 +75,84 @@ fn reference_capacity(
     }
 }
 
+fn reference_metadata(
+    runtime_layout: DstLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    size: usize,
+) -> Option<usize> {
+    match runtime_layout.size_info {
+        SizeInfo::Sized { .. } => None,
+        SizeInfo::SliceDst(tail) => {
+            if tail.elem_size == 0 {
+                return None;
+            }
+            match reference_capacity(tail, align, phase, size) {
+                None => None,
+                Some(bytes) => {
+                    #[allow(clippy::arithmetic_side_effects)]
+                    let elems = bytes / tail.elem_size;
+                    if same_optional_usize(reference_size(tail, align, phase, elems), Some(size)) {
+                        Some(elems)
+                    } else {
+                        None
+                    }
+                }
+            }
+        }
+    }
+}
+
+#[allow(clippy::arithmetic_side_effects)]
+fn reference_cast(
+    runtime_layout: DstLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    addr: usize,
+    length: usize,
+    side: CastType,
+) -> Result<(usize, usize), MetadataCastError> {
+    // The caller checks address addition and excludes the zero-stride panic
+    // before either the production or reference cast is evaluated.
+    let anchor = match side {
+        CastType::Prefix => addr,
+        CastType::Suffix => addr + length,
+    };
+    // Alignment failure has priority over insufficient size.
+    if anchor % runtime_layout.align.get() != 0 {
+        return Err(MetadataCastError::Alignment);
+    }
+    let candidate = match runtime_layout.size_info {
+        SizeInfo::Sized { size } => {
+            if size <= length {
+                Some((0, size))
+            } else {
+                None
+            }
+        }
+        SizeInfo::SliceDst(tail) => match reference_capacity(tail, align, phase, length) {
+            None => None,
+            Some(bytes) => {
+                let elems = bytes / tail.elem_size;
+                match reference_size(tail, align, phase, elems) {
+                    Some(size) => Some((elems, size)),
+                    None => None,
+                }
+            }
+        },
+    };
+    match candidate {
+        None => Err(MetadataCastError::Size),
+        Some((elems, size)) => {
+            let split = match side {
+                CastType::Prefix => size,
+                CastType::Suffix => length - size,
+            };
+            Ok((elems, split))
+        }
+    }
+}
+
 /// Check the entire optional size and capacity results, including overflow.
 ///
 /// Physical slice offset does not constrain this claim: a raw layout can have
@@ -109,3 +187,210 @@ fn trailing_arithmetic_check(
         ));
     }
 }
+
+/// Check exact-size metadata and complete cast results against independent
+/// calculations. A successful cast must select the greatest fitting element
+/// count and its padded prefix/suffix split; errors must have the same kind.
+///
+/// The address guard is the production method's no-overflow premise. The
+/// explicit zero-stride guard excludes its documented panic, even when an
+/// alignment error would otherwise be returned. Exact-size inference itself
+/// is also checked for zero-stride tails, for which it must return `None`.
+///
+/// ```aeneas
+/// spec layout_observations_check_spec
+///   ensures(raw) _ => True
+/// ```
+fn layout_observations_check(
+    runtime_layout: DstLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    size: usize,
+    addr: usize,
+    length: usize,
+    side: CastType,
+) {
+    let encoding_matches = match runtime_layout.size_info {
+        SizeInfo::Sized { .. } => true,
+        SizeInfo::SliceDst(tail) => {
+            align.get().is_power_of_two()
+                && phase < align.get()
+                && same_optional_usize(
+                    align.get().checked_add(phase),
+                    Some(tail.size_rounding_align_and_phase.0.get()),
+                )
+        }
+    };
+    if encoding_matches {
+        assert!(same_optional_usize(
+            runtime_layout.metadata_for_exact_size(size),
+            reference_metadata(runtime_layout, align, phase, size),
+        ));
+        let nonzero_stride = match runtime_layout.size_info {
+            SizeInfo::Sized { .. } => true,
+            SizeInfo::SliceDst(tail) => tail.elem_size != 0,
+        };
+        if addr.checked_add(length).is_some() && nonzero_stride {
+            let actual = runtime_layout.validate_cast_and_convert_metadata(addr, length, side);
+            let expected = reference_cast(runtime_layout, align, phase, addr, length, side);
+            let same = match (actual, expected) {
+                (Ok((elems, split)), Ok((expected_elems, expected_split))) => {
+                    elems == expected_elems && split == expected_split
+                }
+                (Err(MetadataCastError::Alignment), Err(MetadataCastError::Alignment))
+                | (Err(MetadataCastError::Size), Err(MetadataCastError::Size)) => true,
+                _ => false,
+            };
+            assert!(same);
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::layout::RoundingAlignAndPhase;
+
+    fn tail_layout(
+        outer_align: usize,
+        size_align: usize,
+        elem_size: usize,
+        size_base: usize,
+        phase: usize,
+        offset: usize,
+    ) -> DstLayout {
+        DstLayout {
+            align: NonZeroUsize::new(outer_align).unwrap(),
+            size_info: SizeInfo::SliceDst(TrailingSliceLayout {
+                offset,
+                elem_size,
+                size_base,
+                size_rounding_align_and_phase: RoundingAlignAndPhase::new(
+                    NonZeroUsize::new(size_align).unwrap(),
+                    phase,
+                ),
+            }),
+            statically_shallow_unpadded: false,
+        }
+    }
+
+    fn check_cast(
+        layout: DstLayout,
+        size_align: usize,
+        phase: usize,
+        addr: usize,
+        length: usize,
+        side: CastType,
+        expected: Result<(usize, usize), MetadataCastError>,
+    ) {
+        let size_align = NonZeroUsize::new(size_align).unwrap();
+        // The proved root compares complete results, including both error
+        // kinds. Pin the reference result too, so each case documents its path.
+        layout_observations_check(layout, size_align, phase, length, addr, length, side);
+        assert!(match (reference_cast(layout, size_align, phase, addr, length, side), expected) {
+            (Ok(actual), Ok(expected)) => actual == expected,
+            (Err(MetadataCastError::Alignment), Err(MetadataCastError::Alignment))
+            | (Err(MetadataCastError::Size), Err(MetadataCastError::Size)) => true,
+            _ => false,
+        });
+    }
+
+    fn check_both(
+        layout: DstLayout,
+        size_align: usize,
+        phase: usize,
+        length: usize,
+        elems: usize,
+        size: usize,
+    ) {
+        check_cast(layout, size_align, phase, 0, length, CastType::Prefix, Ok((elems, size)));
+        check_cast(
+            layout,
+            size_align,
+            phase,
+            0,
+            length,
+            CastType::Suffix,
+            Ok((elems, length.checked_sub(size).unwrap())),
+        );
+    }
+
+    #[test]
+    fn cast_rounded_size_branches() {
+        // An input below the rounding alignment can select an empty object.
+        check_both(tail_layout(1, 8, 1, 0, 0, 4), 8, 0, 7, 0, 0);
+
+        // Strides below, equal to, and above the size alignment all use the
+        // complete size. Nonzero base and phase differ from physical offset.
+        // For stride 10, the unused remainders are 2, 4, and 6: below, equal
+        // to, and above alignment 4. Only the last two discard a rounded unit.
+        for &(align, stride, length, elems, size) in &[
+            (8, 3, 29, 7, 29),
+            (4, 4, 29, 5, 29),
+            (4, 10, 29, 2, 29),
+            (4, 10, 21, 1, 17),
+            (4, 10, 33, 2, 29),
+        ] {
+            check_both(tail_layout(1, align, stride, 5, 2, 63), align, 2, length, elems, size);
+        }
+
+        // This raw layout need not describe a completed Rust type. Comparing
+        // stride 6 to outer alignment 8 would incorrectly retain all 16 bytes;
+        // size alignment 4 requires discarding the aligned remainder of 4.
+        check_both(tail_layout(8, 4, 6, 0, 0, 3), 4, 0, 16, 2, 12);
+    }
+
+    #[test]
+    fn cast_errors_keep_alignment_priority() {
+        let sized = DstLayout {
+            align: NonZeroUsize::new(8).unwrap(),
+            size_info: SizeInfo::Sized { size: 24 },
+            statically_shallow_unpadded: false,
+        };
+        check_both(sized, 4, 2, 32, 0, 24);
+        for &layout in &[sized, tail_layout(8, 4, 6, 16, 2, 3)] {
+            for &side in &[CastType::Prefix, CastType::Suffix] {
+                check_cast(layout, 4, 2, 1, 4, side, Err(MetadataCastError::Alignment));
+                let addr = match side {
+                    CastType::Prefix => 0,
+                    CastType::Suffix => 4,
+                };
+                check_cast(layout, 4, 2, addr, 4, side, Err(MetadataCastError::Size));
+            }
+        }
+    }
+
+    #[test]
+    fn cast_sizes_near_word_limit() {
+        let max = usize::MAX;
+        let rounded = max.checked_sub(7).unwrap();
+        check_both(tail_layout(1, 8, 1, 0, 0, max), 8, 0, max, rounded, rounded);
+        check_both(tail_layout(1, 4, 8, 0, 0, max), 4, 0, max, rounded / 8, rounded);
+        check_both(tail_layout(1, 4, 1, rounded, 3, 0), 4, 3, max, 1, max.checked_sub(3).unwrap());
+        let sized = DstLayout {
+            align: NonZeroUsize::new(1).unwrap(),
+            size_info: SizeInfo::Sized { size: max },
+            statically_shallow_unpadded: false,
+        };
+        check_both(sized, 4, 2, max, 0, max);
+        let overflowing = tail_layout(1, 4, 1, max.checked_sub(3).unwrap(), 1, 0);
+        for &side in &[CastType::Prefix, CastType::Suffix] {
+            check_cast(overflowing, 4, 1, 0, max, side, Err(MetadataCastError::Size));
+            check_cast(
+                tail_layout(1, 4, 6, 0, 0, 3),
+                4,
+                0,
+                max.checked_sub(16).unwrap(),
+                16,
+                side,
+                Ok((
+                    2,
+                    match side {
+                        CastType::Prefix => 12,
+                        CastType::Suffix => 4,
+                    },
+                )),
+            );
+        }
+    }
+}