From eda1edf292ea04e9a838b4fdac863a0ecb161714 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-size metadata inference

Specify metadata_for_exact_size and validate_cast_and_convert_metadata
against independent layout calculations. Prove exact representability,
greatest-fitting metadata, alignment-before-size error priority and the
complete prefix or suffix result.

Add Rust assertion harnesses comparing the full optional metadata and cast
outcomes with remainder-based checked arithmetic. Keep address-addition
bounds and the zero-stride panic exclusion visible in their domains.
Outcome examples cover unattainable sizes and intentional panic separately
from checks of the specification's meaning.

Prove the concrete u32 slice KnownLayout initializer and every checked
size_for_elems result through a Rust assertion harness. Admission traverses
the actual local constant body, rather than assuming its descriptor. An
initializer mutation challenges that connection.

Retain reproducible native capability fixtures for generic KnownLayout,
the production transmute macro, and raw pointers. Unsupported equalities,
recursive declaration dependencies, and incomplete pointer carriers remain
explicit blockers; no bounds or declarations are removed to admit them.

gherrit-pr-id: Grerckvocdnwpdtef665ubpieo6wlwfdj
Agent-authored-by: AI agent acting on joshlf's behalf
---
 verification/aeneas/DESIGN.md                 |  99 +++++-
 verification/aeneas/README.md                 |   4 +
 verification/aeneas/golden/Funs.lean          | 306 +++++++++++++++++-
 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     |  63 ++++
 .../aeneas/lean/Obligations/TailChecks.lean   |  11 +
 verification/aeneas/lean/OutcomeTests.lean    | 124 +++++++
 .../aeneas/lean/Proofs/Contracts.lean         |  45 +++
 .../aeneas/lean/Proofs/PrimitiveChecks.lean   |  72 +++++
 verification/aeneas/lean/Proofs/Raw/Cast.lean | 283 ++++++++++++++++
 .../aeneas/lean/Proofs/TailChecks.lean        | 156 +++++++++
 .../aeneas/lean/Proofs/TailReference.lean     | 248 ++++++++++++++
 .../aeneas/lean/RequiredModelContracts.lean   |  44 +++
 .../RequiredModelContracts/TailChecks.lean    |  18 ++
 .../aeneas/projections/ModelShapes.lean       |   4 +
 verification/aeneas/projections/Models.lean   |   6 +
 verification/aeneas/projections/Specs.lean    |  36 +++
 .../aeneas/tests/capabilities/README.md       | 107 ++++++
 .../capabilities/invalid-transmute/Cargo.lock |  61 ++++
 .../capabilities/invalid-transmute/Cargo.toml |  12 +
 .../capabilities/invalid-transmute/src/lib.rs |  11 +
 .../capabilities/known-layout/Cargo.lock      |  61 ++++
 .../capabilities/known-layout/Cargo.toml      |  12 +
 .../capabilities/known-layout/src/lib.rs      |  25 ++
 .../capabilities/owned-transmute/Cargo.lock   |  61 ++++
 .../capabilities/owned-transmute/Cargo.toml   |  12 +
 .../capabilities/owned-transmute/src/lib.rs   |  15 +
 .../aeneas/tests/capabilities/probe.py        |  97 ++++++
 .../capabilities/raw-pointers/Cargo.lock      |  61 ++++
 .../capabilities/raw-pointers/Cargo.toml      |  12 +
 .../capabilities/raw-pointers/src/lib.rs      |  21 ++
 .../capabilities/std-transmute/Cargo.lock     |   7 +
 .../capabilities/std-transmute/Cargo.toml     |   9 +
 .../capabilities/std-transmute/src/lib.rs     |  20 ++
 zerocopy/src/layout/mod.rs                    |  14 +
 zerocopy/src/layout/primitive_checks.rs       |  42 +++
 zerocopy/src/layout/tail_checks.rs            | 287 +++++++++++++++-
 40 files changed, 2555 insertions(+), 12 deletions(-)
 create mode 100644 verification/aeneas/lean/OutcomeTests.lean
 create mode 100644 verification/aeneas/lean/Proofs/Raw/Cast.lean
 create mode 100644 verification/aeneas/tests/capabilities/README.md
 create mode 100644 verification/aeneas/tests/capabilities/invalid-transmute/Cargo.lock
 create mode 100644 verification/aeneas/tests/capabilities/invalid-transmute/Cargo.toml
 create mode 100644 verification/aeneas/tests/capabilities/invalid-transmute/src/lib.rs
 create mode 100644 verification/aeneas/tests/capabilities/known-layout/Cargo.lock
 create mode 100644 verification/aeneas/tests/capabilities/known-layout/Cargo.toml
 create mode 100644 verification/aeneas/tests/capabilities/known-layout/src/lib.rs
 create mode 100644 verification/aeneas/tests/capabilities/owned-transmute/Cargo.lock
 create mode 100644 verification/aeneas/tests/capabilities/owned-transmute/Cargo.toml
 create mode 100644 verification/aeneas/tests/capabilities/owned-transmute/src/lib.rs
 create mode 100644 verification/aeneas/tests/capabilities/probe.py
 create mode 100644 verification/aeneas/tests/capabilities/raw-pointers/Cargo.lock
 create mode 100644 verification/aeneas/tests/capabilities/raw-pointers/Cargo.toml
 create mode 100644 verification/aeneas/tests/capabilities/raw-pointers/src/lib.rs
 create mode 100644 verification/aeneas/tests/capabilities/std-transmute/Cargo.lock
 create mode 100644 verification/aeneas/tests/capabilities/std-transmute/Cargo.toml
 create mode 100644 verification/aeneas/tests/capabilities/std-transmute/src/lib.rs

diff --git a/verification/aeneas/DESIGN.md b/verification/aeneas/DESIGN.md
index b9aa5b58cf..b1b28560ae 100644
--- a/verification/aeneas/DESIGN.md
+++ b/verification/aeneas/DESIGN.md
@@ -304,6 +304,92 @@ the library already models every part of Rust's abstract machine.
 
 ## Deferred decisions and reopening evidence
 
+### Resource-free layout and storage work
+
+The shared library supplies two independent foundations for layout and owned
+byte-cast proofs:
+
+- `Rust.Pointer.Value` retains an address, opaque optional provenance, and
+  metadata. Its casts and metadata operations preserve the exact provenance
+  value. Pointer equality observes address and metadata; it does not compare
+  provenance. Non-nullness supplies no alignment, liveness, or access permission.
+- `Rust.Storage.StorageDecoder` takes metadata explicitly, checks the requested
+  byte width, and checks that a successful raw result carries that metadata.
+  Fixed-width decoders adapt through unit metadata. Slice counts are inputs,
+  including for zero-sized elements; byte length cannot recover those counts.
+
+These are mathematical definitions and checked laws, not newly admitted Rust
+operations. The storage carrier still contains only initialized numeric bytes
+and uninitialized bytes. It does not encode pointers or decide where provenance
+lives in a pointer's representation. Pointer-bearing byte operations remain
+unsupported. Typed copies still require the treatment described in
+[the lowering audit](LOWERING_AUDIT.md), including
+[Aeneas issue #1405](https://github.com/AeneasVerif/aeneas/issues/1405).
+
+Byte-cast reasoning uses the existing distinction between language validity and
+optional mathematical admission. The source's `IntoBytes` law ranges over all
+accepted language representations, regardless of mathematical admission. The
+destination's intended `FromBytes` law must accept every initialized storage of
+the correct width at both stages. The shared cast lemma composes these laws for
+arbitrary represented bytes. It supplies no encoder and does not claim that a
+particular Rust transmutation follows this interpretation.
+
+The concrete `check_u32_slice_known_layout` Rust harness checks the actual
+`<[u32] as KnownLayout>::LAYOUT` initializer, its descriptor fields, and sizing
+for every element count, including checked-multiplication overflow. Admission
+visits the local constant's initializer body; no axiom supplies the descriptor.
+The visible guards expose the power-of-two and size-divisibility premises of
+the ABI reads. This checks that concrete numerical behavior, not the complete
+generic trait invariant. The proof also rejects an initializer changed from
+`for_slice` to `for_type`.
+
+The native capability fixtures under `tests/capabilities/` preserve the next
+translation boundaries. With the current pins, the generic `KnownLayout`
+fixture retains an associated-type equality that Aeneas rejects. A second
+fixture without an explicit caller-side equality fails on the trait's own
+`MaybeUninit` metadata equality. The production
+`transmute!` fixture retains its compile-time trait-check helper and a loop that
+Aeneas rejects. The required `FromBytes` declaration dependencies additionally
+reach the unsupported recursive `Invariants`/`Alignment` group. These failures
+are not successful extraction or completed Rust proofs. Do not delete bounds,
+equalities, or required declarations to make those targets extract. Required
+recursive declaration support is deferred; dependent work must wait for tools
+that support it.
+
+Native raw-pointer emission has a separate limitation. The pinned backend's
+carrier stores only `v : T`, and its scalar pointer cast returns `undef`.
+Emitted slice construction and `NonNull` operations remain external templates.
+The mathematical pointer model does not repair that carrier or grant admission
+to those operations. The existing checker continues to reject them. A faithful
+carrier and checked primitive interpretations are prerequisites for proving
+their address, metadata, or provenance behavior.
+
+When those boundaries are supported, bind `KnownLayout::LAYOUT` to the original
+Rust type and its metadata-indexed geometry. Reuse the complete recursive
+layout semantics, which preserves an inner field's padding before outer
+rounding. Preserve physical tail offset, stride, alignment, and conservative
+padding flags. Keep mathematical extent, `usize` representability, and the
+`isize` object-size restriction separate. The `MaybeUninit` obligation also
+requires identical metadata and layout and acceptance of uninitialized storage
+in every position; a layout-only theorem must not be presented as the full
+trait invariant.
+
+Concrete owned conversions use the actual standard transmute primitive for
+`u32` and four-byte arrays, plus a guarded `u8`-to-`bool` conversion. These types
+have no pointers, resources, destruction, or external-state invariants. Original
+Rust endpoint checks and a compiled canonical-provider audit restrict that
+interpretation to those cases; it does not admit the production macro or an
+arbitrary generic transmute. Invalid Boolean encodings take the forbidden path,
+even with postcondition `True`. Reference creation remains a later target because
+numerical geometry and provenance presence alone do not supply permissions or
+lifetimes. Derive
+proof requests are also deferred. Existing annotation discovery, native binding
+records, independent golden/live proofs, and dependency audits remain the sole
+route to reporting a Rust specification as checked; these foundations add no
+parallel coverage registry or automatic Rust ABI assumptions.
+
+### Other deferred decisions
+
 - **Canonical layout abstraction.** Retain structural `DstLayout` and existing
   `ModelViews` initially. Padding and trailing-size pilots already use those
   views. Use `extend`, sequence queries, and capacity contracts to compare total
@@ -325,8 +411,8 @@ the library already models every part of Rust's abstract machine.
   tactics, and the existing loop adapter. Introduce a larger lifting DSL,
   per-model tactics, or new loop abstraction only after concrete repeated
   failures show a net benefit over ordinary lemmas and a thin tactic.
-- **Broader carriers and effects.** Recursive nominal groups, indexed carriers,
-  const generics, associated-type trait laws, higher-ranked bounds, bounded
+- **Broader carriers and effects.** Recursive nominal groups, general indexed
+  carriers, const generics, associated-type trait laws, higher-ranked bounds, bounded
   nominal models, and escaping borrow reconstruction remain unsupported with
   explicit errors. The first trait-law bridge supports `Self`-only traits and
   simple generic bounds, with `Unaligned` and a total byte codec as checked
@@ -338,11 +424,12 @@ the library already models every part of Rust's abstract machine.
   execution, independently of ordinary library-model admission. A storage model
   must account for the translation's omissions as well as its primitives. The
   [pinned lowering audit](LOWERING_AUDIT.md) records known omissions and the
-  additional admission checks needed before making memory-safety claims.
-  [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) specifies the proposed closed
+  admission checks needed before making memory-safety claims.
+  [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) specifies the closed
   dependency traversal, controlled build origins using Charon's existing MIR
-  preservation setup, primitive rules, and mandatory CI path. These additional
-  checks are not implemented yet.
+  preservation setup, primitive rules, and mandatory CI path. CI enforces
+  these checks for the admitted fragment; extending that fragment requires
+  corresponding operation semantics and coverage checks.
   <!-- FIXME: Typed transfers lose storage events; track support at
   https://github.com/AeneasVerif/aeneas/issues/1405. Until then, a typed storage
   abstraction must forget all padding contents and initialization facts. It
diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index 174d79af6e..f54c86163f 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -390,6 +390,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, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping
 raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index 0c426e3c83..5d756948c4 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -1682,6 +1682,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 48:0-58:1 -/
 def layout.nested_reference.round_up
@@ -1889,6 +1983,14 @@ def layout.primitive_checks.check_empty_layout
     massert empty.statically_shallow_unpadded
   else ok ()
 
+/-- [zerocopy::{impl zerocopy::KnownLayout for [T]}::LAYOUT]
+    Source: 'src/lib.rs', lines 1123:4-1123:58
+    Visibility: public -/
+@[global_simps, irreducible]
+def Slice.Insts.ZerocopyKnownLayout.LAYOUT (T : Type)
+  : Result layout.DstLayout :=
+  layout.DstLayout.for_slice T
+
 /-- [zerocopy::layout::tail_checks::same_optional_usize]:
     Source: 'src/layout/tail_checks.rs', lines 29:0-35:1 -/
 def layout.tail_checks.same_optional_usize
@@ -1902,6 +2004,44 @@ def layout.tail_checks.same_optional_usize
     | none => ok false
     | some right1 => ok (left1 = right1)
 
+/-- [zerocopy::layout::primitive_checks::check_u32_slice_known_layout]:
+    Source: 'src/layout/primitive_checks.rs', lines 95:0-120:1 -/
+def layout.primitive_checks.check_u32_slice_known_layout
+  (elems : Std.Usize) : Result Unit := do
+  let size ← core.mem.size_of Std.U32
+  let align ← core.mem.align_of Std.U32
+  let b ← core.num.Usize.is_power_of_two align
+  if b
+  then
+    let i ← size % align
+    if i != 0#usize
+    then ok ()
+    else
+      let slice ← Slice.Insts.ZerocopyKnownLayout.LAYOUT Std.U32
+      let i1 ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+          slice.align
+      massert (i1 = align)
+      massert slice.statically_shallow_unpadded
+      match slice.size_info with
+      | layout.SizeInfo.Sized _ => fail panic
+      | layout.SizeInfo.SliceDst tail =>
+        massert (tail.offset = 0#usize)
+        massert (tail.elem_size = size)
+        massert (tail.size_base = 0#usize)
+        let i2 ←
+          core.num.nonzero.NonZero.get
+            Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+            tail.size_rounding_align_and_phase._0
+        massert (i2 = align)
+        let actual ←
+          layout.TrailingSliceLayoutUsize.size_for_elems tail elems
+        let expected ← lift (Usize.checked_mul elems size)
+        let b1 ← layout.tail_checks.same_optional_usize actual expected
+        massert b1
+  else ok ()
+
 /-- [zerocopy::layout::tail_checks::reference_round_up]:
     Source: 'src/layout/tail_checks.rs', lines 38:0-42:1 -/
 def layout.tail_checks.reference_round_up
@@ -1961,8 +2101,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
@@ -1999,6 +2213,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-41:1 -/
 def layout.tail_transform_checks.witness_matches
diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean
index 0e63ebd96e..714facef25 100644
--- a/verification/aeneas/golden/Types.lean
+++ b/verification/aeneas/golden/Types.lean
@@ -232,6 +232,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 29:0-33: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..01ffe7113a 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
 
@@ -383,4 +438,12 @@ def empty_layout_checks_spec : Prop :=
   ∀ repr_align, empty_layout_checks_spec_contract repr_align
     (layout.primitive_checks.check_empty_layout repr_align)
 
+def u32_slice_known_layout_checks_spec_contract (_elems : Usize)
+    (run : Result Unit) : Prop :=
+  run ⦃ _ => True ⦄
+
+def u32_slice_known_layout_checks_spec : Prop :=
+  ∀ elems, u32_slice_known_layout_checks_spec_contract elems
+    (layout.primitive_checks.check_u32_slice_known_layout elems)
+
 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/Contracts.lean b/verification/aeneas/lean/Proofs/Contracts.lean
index 49a14110e0..fead244b30 100644
--- a/verification/aeneas/lean/Proofs/Contracts.lean
+++ b/verification/aeneas/lean/Proofs/Contracts.lean
@@ -8,6 +8,7 @@ those terms. -/
 
 module
 public import Proofs.Raw.Trailing
+public import Proofs.Raw.Cast
 public import Proofs.Raw.Construction
 @[expose] public section
 
@@ -223,6 +224,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/PrimitiveChecks.lean b/verification/aeneas/lean/Proofs/PrimitiveChecks.lean
index 9413da9e7f..8196553cec 100644
--- a/verification/aeneas/lean/Proofs/PrimitiveChecks.lean
+++ b/verification/aeneas/lean/Proofs/PrimitiveChecks.lean
@@ -8,6 +8,7 @@ those terms. -/
 
 module
 public import Proofs
+public import Proofs.TailReference
 @[expose] public section
 
 /-!
@@ -66,6 +67,71 @@ theorem empty_layout_checks (repr_align : Option NonZeroUsize) :
       simp [ha, hs, hp, massert, UScalar.val]
     · simp only [WP.spec_ok]
 
+/- Follow the actual built-in associated-constant initializer. This proves
+the concrete numerical assertions without assuming a KnownLayout trait law.
+-/
+theorem u32_slice_known_layout_checks (elems : Usize) :
+    layout.primitive_checks.check_u32_slice_known_layout elems ⦃ _ => True ⦄ := by
+  classical
+  let size : Usize := if U32 = Usize then
+    { bv := BitVec.ofNat _ (System.Platform.numBits / 8) } else RustLayout.size U32
+  let align := RustLayout.align U32
+  have hs : core.mem.size_of U32 = .ok size := rfl
+  have ha : core.mem.align_of U32 = .ok align := rfl
+  unfold layout.primitive_checks.check_u32_slice_known_layout
+  rw [hs, ha]
+  simp only [bind_ok]
+  step as ⟨enabled, he⟩
+  split
+  · rename_i yes
+    have power : align.val.isPowerOfTwo := Eq.mp he yes
+    have positive := Nat.pos_of_isPowerOfTwo power
+    step with Usize.rem_spec size (y := align) (by omega) as ⟨remainder, hr⟩
+    simp only [UScalar.eq_equiv, UScalar.ofNatCore_val_eq]
+    split
+    · simp only [WP.spec_ok]
+    · rename_i divisible
+      have remainder_zero : remainder = 0#usize := by
+        simpa only [bne_iff_ne, not_not] using divisible
+      have multiple : size.val % align.val = 0 := by
+        change remainder.val = size.val % align.val at hr
+        rw [remainder_zero] at hr
+        simpa only [UScalar.ofNatCore_val_eq] using hr.symm
+      unfold Slice.Insts.ZerocopyKnownLayout.LAYOUT
+      step with for_slice_spec U32 size align hs ha power as
+        ⟨slice, hsa, hsp, tail, hsi, ho, hel, hb, hc⟩
+      simp [core.num.nonzero.NonZero.get, hsa, hsp, hsi, ho, hel, hb,
+        align, size, massert]
+      have same : tail.size_rounding_align_and_phase._0.val = align :=
+        UScalar.eq_of_val_eq hc
+      simp [same, align]
+      have encoded_positive : 0 < tail.size_rounding_align_and_phase._0.val.val := by
+        rw [same]
+        exact positive
+      have formula := TailChecks.witness_view tail ⟨align⟩ 0#usize power
+        (by simpa using positive) (by simpa using hc)
+      step with size_for_elems_spec tail elems encoded_positive as ⟨actual, actual_value⟩
+      have product_aligned : (elems.val * size.val) % align.val = 0 := by
+        simp [Nat.mul_mod, multiple]
+      have size_formula : (trailingFormula tail).size elems.val = elems.val * size.val := by
+        rw [formula]
+        simp only [TailChecks.witnessFormula, LayoutMath.Formula.size,
+          LayoutMath.Formula.bytes, hb, hel, UScalar.ofNatCore_val_eq,
+          Nat.zero_add]
+        change LayoutMath.roundUp (elems.val * size.val) align.val = elems.val * size.val
+        exact LayoutMath.roundUp_eq _ _ product_aligned
+      have actual_expected : actual = Usize.checked_mul elems size :=
+        TailChecks.optional_value_injective (by
+          simp only [LayoutMath.Formula.checkedSize, size_formula] at actual_value
+          simpa only [TailChecks.checkedNat] using
+            actual_value.trans (TailChecks.checked_mul_value elems size).symm)
+      simp only [lift, bind_ok]
+      step with TailChecks.same_optional_usize actual (Usize.checked_mul elems size) as
+        ⟨same_result, result_iff⟩
+      have same_true := result_iff.mpr actual_expected
+      simp only [same_true, if_true, WP.spec_ok]
+  · simp only [WP.spec_ok]
+
 end Zerocopy.Proofs.Raw
 
 namespace Zerocopy.Proofs
@@ -82,4 +148,10 @@ theorem empty_layout_checks_spec : Specs.empty_layout_checks_spec := by
   intro _ _
   exact ⟨(), rfl, trivial⟩
 
+theorem u32_slice_known_layout_checks_spec : Specs.u32_slice_known_layout_checks_spec := by
+  intro elems _ _
+  apply WP.spec_mono (Raw.u32_slice_known_layout_checks elems)
+  intro _ _
+  exact ⟨(), rfl, trivial⟩
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/Raw/Cast.lean b/verification/aeneas/lean/Proofs/Raw/Cast.lean
new file mode 100644
index 0000000000..9dcb4b0427
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/Raw/Cast.lean
@@ -0,0 +1,283 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import Proofs.Raw.Trailing
+public import Proofs.Raw.Layout
+import all Mathlib.Data.Nat.Log
+import all Init.Data.Nat.Power2.Basic
+@[expose] public section
+
+open Aeneas Aeneas.Std
+namespace Zerocopy.Proofs.Raw
+
+set_option linter.unusedVariables false
+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
+
+end Zerocopy.Proofs.Raw
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/verification/aeneas/projections/ModelShapes.lean b/verification/aeneas/projections/ModelShapes.lean
index a350e0329e..551bc8819a 100644
--- a/verification/aeneas/projections/ModelShapes.lean
+++ b/verification/aeneas/projections/ModelShapes.lean
@@ -65,6 +65,10 @@ derive_model_shape Zerocopy.layout.SizeInfo with 1 type parameters
 
 derive_model_shape Zerocopy.layout.DstLayout with 0 type parameters
 
+derive_model_shape Zerocopy.layout.CastType with 0 type parameters
+
+derive_model_shape Zerocopy.layout.MetadataCastError with 0 type parameters
+
 derive_model_shape Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters
 
 derive_model_shape Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters
diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean
index e1982fca2c..66fe244db2 100644
--- a/verification/aeneas/projections/Models.lean
+++ b/verification/aeneas/projections/Models.lean
@@ -83,6 +83,12 @@ check_model_binding Zerocopy.layout.SizeInfo with 1 type parameters
 derive_rust_model Zerocopy.layout.DstLayout with 0 type parameters
 check_model_binding Zerocopy.layout.DstLayout with 0 type parameters
 
+derive_rust_model Zerocopy.layout.CastType with 0 type parameters
+check_model_binding Zerocopy.layout.CastType with 0 type parameters
+
+derive_rust_model Zerocopy.layout.MetadataCastError with 0 type parameters
+check_model_binding Zerocopy.layout.MetadataCastError with 0 type parameters
+
 derive_rust_model Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters
 check_model_binding Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters
 
diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean
index 6c6a9f1d20..6634cd6c3f 100644
--- a/verification/aeneas/projections/Specs.lean
+++ b/verification/aeneas/projections/Specs.lean
@@ -345,6 +345,26 @@ spec requires_dynamic_padding_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.requires_dynamic_padding_spec for Zerocopy.layout.DstLayout.requires_dynamic_padding with 1
 
+check_model_inputs Zerocopy.layout.DstLayout.metadata_for_exact_size with 0 type parameters
+aeneas_spec_begin
+spec metadata_exact_spec
+  for @Zerocopy.layout.DstLayout.metadata_for_exact_size with 0 type parameters
+  ensures(raw) r => metadataSpec self size.val r
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.metadata_exact_spec for Zerocopy.layout.DstLayout.metadata_for_exact_size with 2
+
+check_model_inputs Zerocopy.layout.DstLayout.validate_cast_and_convert_metadata with 0 type parameters
+aeneas_spec_begin
+spec validate_cast_spec
+  for @Zerocopy.layout.DstLayout.validate_cast_and_convert_metadata with 0 type parameters
+  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
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.validate_cast_spec for Zerocopy.layout.DstLayout.validate_cast_and_convert_metadata with 4
+
 check_model_inputs Zerocopy.layout.nested_reference.round_up with 0 type parameters
 aeneas_spec_begin
 spec nested_round_up_spec
@@ -381,6 +401,14 @@ spec empty_layout_checks_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.empty_layout_checks_spec for Zerocopy.layout.primitive_checks.check_empty_layout with 1
 
+check_model_inputs Zerocopy.layout.primitive_checks.check_u32_slice_known_layout with 0 type parameters
+aeneas_spec_begin
+spec u32_slice_known_layout_checks_spec
+  for @Zerocopy.layout.primitive_checks.check_u32_slice_known_layout with 0 type parameters
+  ensures _ => True
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.u32_slice_known_layout_checks_spec for Zerocopy.layout.primitive_checks.check_u32_slice_known_layout with 1
+
 check_model_inputs Zerocopy.layout.tail_checks.trailing_arithmetic_check with 0 type parameters
 aeneas_spec_begin
 spec trailing_arithmetic_check_spec
@@ -389,6 +417,14 @@ spec trailing_arithmetic_check_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.trailing_arithmetic_check_spec for Zerocopy.layout.tail_checks.trailing_arithmetic_check with 5
 
+check_model_inputs Zerocopy.layout.tail_checks.layout_observations_check with 0 type parameters
+aeneas_spec_begin
+spec layout_observations_check_spec
+  for @Zerocopy.layout.tail_checks.layout_observations_check with 0 type parameters
+  ensures(raw) _ => True
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.layout_observations_check_spec for Zerocopy.layout.tail_checks.layout_observations_check with 7
+
 check_model_inputs Zerocopy.layout.tail_transform_checks.tail_transformations_check with 0 type parameters
 aeneas_spec_begin
 spec tail_transformations_check_spec
diff --git a/verification/aeneas/tests/capabilities/README.md b/verification/aeneas/tests/capabilities/README.md
new file mode 100644
index 0000000000..446f60e5cb
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/README.md
@@ -0,0 +1,107 @@
+<!-- Copyright 2026 The Fuchsia Authors
+SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT -->
+
+# Native capability fixtures
+
+These small, independent crates challenge the pinned native extraction without
+editing compiler output, deleting associated equalities, or replacing local
+helpers with axioms. They are capability probes, not admitted Rust soundness
+proofs. Each new observation records the repository's actual HEAD, dirty status,
+source digests, and validated runtime metadata.
+
+Run from the repository root with the existing `AENEAS_TOOLCHAIN_DIR` and
+`CARGO_HOME` from the verification setup, using a fresh evidence directory:
+
+```bash
+python3 -B verification/aeneas/tests/capabilities/probe.py known-layout \
+  --runtime "$AENEAS_TOOLCHAIN_DIR" \
+  --cargo-home "$CARGO_HOME" \
+  --work target/capabilities/known-layout-new \
+  --cargo-target target/owned-transmute-capability/cargo-target
+```
+
+Replace the case and work directory with `owned-transmute`, `invalid-transmute`,
+`raw-pointers`, `std-transmute`, `known-layout-unconstrained`, or
+`known-layout-concrete`.
+The last two select only their own root from the `known-layout` fixture.
+Each run records commands, exit codes, source digest, and
+logs in `evidence.json`. Charon also records the pre-transformation ULLBC and
+final LLBC. The driver refuses an existing evidence directory and returns the
+first failing stage's status. Inspect the recorded stage results to distinguish
+the expected negative fixture from an unexpected failure.
+The tracked Cargo lockfiles are used with `--locked`; the probe does not
+regenerate them. Compilation occurs through the native Charon driver, as in the
+verification pipeline.
+
+Observed with the preserved patched runtime on October 14, 2026:
+
+| Case | Charon | Aeneas | Result |
+| --- | --- | --- | --- |
+| `known-layout` | 0 | 2 | The original `KnownLayout<PointerMetadata = usize>` constraint survives lifting. `SymbolicToPureTypes.ml:1000` requires an empty associated-type constraint list and rejects the generic root signature. |
+| `known-layout-unconstrained` | 0 | 2 | The generic root has no associated-type constraints. The original trait's `MaybeUninit` metadata equality survives lifting and triggers the same check while Aeneas translates the trait's method signatures. |
+| `known-layout-concrete` | 0 | 0 | The concrete slice root emits, but calls an external associated-constant axiom template; its descriptor value or initializer is not translated or proved. |
+| `owned-transmute` | 0 | 2 | The actual production `transmute!` expansion retains its compile-time trait-check helper. `InterpLoops.ml:411` rejects that helper's infinite loop. No conversion theorem is established. |
+| `invalid-transmute` | 101 | Not run | Rust rejects `u8 -> bool` because `bool` does not implement `FromBytes` (E0277). This confirms a compilation gate, not a runtime byte-decoder proof. |
+| `raw-pointers` | 0 | 0 | Native emission succeeds, but does not establish useful raw-pointer semantics or an admitted proof. |
+
+The raw-pointer result needs particular care. The pinned backend's
+`Aeneas/Std/RawPtr.lean` represents a raw pointer by `v : T`; it carries no
+address or provenance. Its `RawPtr.cast_scalar` always returns `.fail .undef`.
+The emitted slice-pointer constructor and `NonNull::new` are external function
+axiom templates, and `NonNull` is an external type axiom template. None of those
+templates is an accepted interpretation in this experiment. The existing
+admission checker also rejects raw-pointer types. Successful emission therefore
+does not provide a pointer-preservation or memory-safety theorem.
+
+The exact `KnownLayout` experiment fails before recursive trait extraction.
+Its error must not be relabeled as a recursive-declaration diagnostic. The
+trait's recursive `MaybeUninit: KnownLayout` bound and metadata equality remain
+in the preserved original compiler evidence; no translation patch or weakened
+trait was introduced.
+
+The unconstrained follow-up isolates that retained trait equality from the
+explicit equality in the first root. Its final trait constraint identifies
+`<Self::MaybeUninit as KnownLayout>::PointerMetadata = Self::PointerMetadata`.
+The concrete follow-up emits a call to
+`Slice.Insts.ZerocopyKnownLayout.LAYOUT Std.U32`, with the implementation's
+associated constant left in `FunsExternal_Template.lean` as an axiom because
+zerocopy is a dependency of the independent fixture. This emission cannot stand
+in for a proof of the constant's body or of a generic `KnownLayout` dictionary.
+
+## Checked local initializer
+
+The production harness `check_u32_slice_known_layout` in
+`zerocopy/src/layout/primitive_checks.rs` compiles inside zerocopy's own crate.
+Unlike the independent dependency fixture, it reaches the local slice
+implementation's actual associated-constant initializer. The preserved and
+final compiler evidence retains that body; admission traverses its execution.
+Native output defines `Slice.Insts.ZerocopyKnownLayout.LAYOUT T` by calling
+`layout.DstLayout.for_slice T`. No external axiom supplies the descriptor.
+
+The harness checks the actual `[u32]` descriptor fields and its size for every
+count against independent checked multiplication. Its Lean proof uses that
+retained initializer under the visible ABI-read guards. A development negative
+control changes the initializer from `for_slice` to `for_type`: the native module
+still elaborates, but the proof fails. The associated constant is thus part of
+the checked behavior, rather than an assumed trait promise.
+
+This remains a concrete numerical assertion proof under the existing primitive
+interpretations and Rust correspondence premise. It does not supply a generic
+`KnownLayout` law, its `MaybeUninit` obligations, or pointer/reference safety.
+
+## Direct standard transmute
+
+`std-transmute` calls the standard primitive directly for `u32 -> [u8; 4]`,
+the reverse conversion, and `u8 -> bool` after checking Boolean validity. It
+rejects non-little-endian targets at compilation. Native emission succeeds and
+retains all local wrapper bodies, with one external `core::intrinsics::transmute`
+template. This observation isolates the standard primitive from the production
+macro's unsupported compile-time helper loop; it does not prove the macro.
+
+The separate owned-operation proof adds an explicit interpretation-only provider
+to that standard boundary. Admission checks each original Rust endpoint pair;
+compiled auditing binds every reached call to its canonical provider and checks
+the whole provider definitions. Numerical cases use the verified 64-bit
+little-endian profile. The Boolean provider checks validity before construction
+and returns forbidden execution outside its domain. Neither this boundary nor
+its providers cover padding, pointers, resources, or arbitrary Rust types.
diff --git a/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.lock b/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.lock
new file mode 100644
index 0000000000..6b3392da3b
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.lock
@@ -0,0 +1,61 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "owned-transmute-negative"
+version = "0.0.0"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.63"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.63"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.toml b/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.toml
new file mode 100644
index 0000000000..99178873ae
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.toml
@@ -0,0 +1,12 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "owned-transmute-negative"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+zerocopy = { path = "../../../../../zerocopy", default-features = false }
diff --git a/verification/aeneas/tests/capabilities/invalid-transmute/src/lib.rs b/verification/aeneas/tests/capabilities/invalid-transmute/src/lib.rs
new file mode 100644
index 0000000000..2d6c73cb4d
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/invalid-transmute/src/lib.rs
@@ -0,0 +1,11 @@
+// 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.
+
+pub fn to_bool(value: u8) -> bool {
+    zerocopy::transmute!(value)
+}
diff --git a/verification/aeneas/tests/capabilities/known-layout/Cargo.lock b/verification/aeneas/tests/capabilities/known-layout/Cargo.lock
new file mode 100644
index 0000000000..9499ba46fc
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/known-layout/Cargo.lock
@@ -0,0 +1,61 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "known-layout-probe"
+version = "0.0.0"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.63"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.63"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/verification/aeneas/tests/capabilities/known-layout/Cargo.toml b/verification/aeneas/tests/capabilities/known-layout/Cargo.toml
new file mode 100644
index 0000000000..05ad38ca5b
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/known-layout/Cargo.toml
@@ -0,0 +1,12 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "known-layout-probe"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+zerocopy = { path = "../../../../../zerocopy", default-features = false }
diff --git a/verification/aeneas/tests/capabilities/known-layout/src/lib.rs b/verification/aeneas/tests/capabilities/known-layout/src/lib.rs
new file mode 100644
index 0000000000..1661dab3bf
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/known-layout/src/lib.rs
@@ -0,0 +1,25 @@
+// 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.
+
+use zerocopy::{DstLayout, KnownLayout};
+
+pub fn layout<T: ?Sized + KnownLayout<PointerMetadata = usize>>() -> DstLayout {
+    T::LAYOUT
+}
+
+pub fn slice_u32_layout() -> DstLayout {
+    layout::<[u32]>()
+}
+
+pub fn layout_unconstrained<T: KnownLayout>() -> DstLayout {
+    T::LAYOUT
+}
+
+pub fn slice_u32_layout_direct() -> DstLayout {
+    <[u32] as KnownLayout>::LAYOUT
+}
diff --git a/verification/aeneas/tests/capabilities/owned-transmute/Cargo.lock b/verification/aeneas/tests/capabilities/owned-transmute/Cargo.lock
new file mode 100644
index 0000000000..00b1b8beec
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/owned-transmute/Cargo.lock
@@ -0,0 +1,61 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "owned-transmute-probe"
+version = "0.0.0"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.63"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.63"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/verification/aeneas/tests/capabilities/owned-transmute/Cargo.toml b/verification/aeneas/tests/capabilities/owned-transmute/Cargo.toml
new file mode 100644
index 0000000000..1a3d13ac7d
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/owned-transmute/Cargo.toml
@@ -0,0 +1,12 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "owned-transmute-probe"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+zerocopy = { path = "../../../../../zerocopy", default-features = false }
diff --git a/verification/aeneas/tests/capabilities/owned-transmute/src/lib.rs b/verification/aeneas/tests/capabilities/owned-transmute/src/lib.rs
new file mode 100644
index 0000000000..6962e4eeda
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/owned-transmute/src/lib.rs
@@ -0,0 +1,15 @@
+// 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.
+
+pub fn to_bytes(value: u32) -> [u8; 4] {
+    zerocopy::transmute!(value)
+}
+
+pub fn from_bytes(value: [u8; 4]) -> u32 {
+    zerocopy::transmute!(value)
+}
diff --git a/verification/aeneas/tests/capabilities/probe.py b/verification/aeneas/tests/capabilities/probe.py
new file mode 100644
index 0000000000..6a997a5419
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/probe.py
@@ -0,0 +1,97 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+"""Record exact native capability failures without modifying extracted ASTs."""
+
+import argparse
+import hashlib
+import json
+from pathlib import Path
+import subprocess
+import sys
+import time
+
+
+CASES = {
+    'known-layout': 'known_layout_probe::layout,known_layout_probe::slice_u32_layout',
+    'known-layout-unconstrained': 'known_layout_probe::layout_unconstrained',
+    'known-layout-concrete': 'known_layout_probe::slice_u32_layout_direct',
+    'owned-transmute': 'owned_transmute_probe::to_bytes,owned_transmute_probe::from_bytes',
+    'invalid-transmute': 'owned_transmute_negative::to_bool',
+    'std-transmute': 'std_transmute_probe::to_bytes,std_transmute_probe::from_bytes,std_transmute_probe::guarded_bool',
+    'raw-pointers': 'raw_pointer_probe::cast,raw_pointer_probe::with_len,raw_pointer_probe::nonnull',
+}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('case', choices=CASES)
+    parser.add_argument('--runtime', type=Path, required=True)
+    parser.add_argument('--cargo-home', type=Path, required=True)
+    parser.add_argument('--work', type=Path, required=True)
+    parser.add_argument('--cargo-target', type=Path, required=True)
+    args = parser.parse_args()
+    runtime, work = args.runtime.resolve(), args.work.resolve()
+    root = Path(__file__).resolve().parents[4]
+    sys.path.insert(0, str(root / 'verification/aeneas'))
+    import toolchain
+    metadata, charon_version = toolchain.validate(root, runtime)
+    fixture_case = ('known-layout' if args.case.startswith('known-layout')
+                    else args.case)
+    fixture = Path(__file__).resolve().parent / fixture_case
+    work.mkdir(parents=True, exist_ok=False)
+    (work / 'native').mkdir(exist_ok=True)
+    environment = toolchain.runtime_env(runtime)
+    environment.update({
+        'RUSTUP_TOOLCHAIN': metadata['rust-toolchain-version'],
+        'CARGO_HOME': str(args.cargo_home.resolve()),
+        'CARGO_TARGET_DIR': str(args.cargo_target.resolve()),
+        'CARGO_BUILD_JOBS': '2', 'CARGO_NET_OFFLINE': 'true',
+        'CHARON_ADMISSION_SNAPSHOT': str(work / 'probe.before.ullbc'),
+    })
+    commands = [
+        ('charon', [str(runtime / 'charon'), 'cargo', '--preset=aeneas',
+                    '--sysroot', 'default', '--start-from', CASES[args.case],
+                    '--mir', 'promoted', '--no-dedup-serialized-ast',
+                    '--dest-file', str(work / 'probe.llbc'), '--abort-on-error',
+                    '--error-on-warnings', '--', '--lib', '--locked', '--offline']),
+        ('aeneas', [str(runtime / 'aeneas'), '-backend', 'lean', '-namespace',
+                    'Probe', '-dest', str(work / 'native'), '-split-files',
+                    '-emit-json', '-abort-on-error', '-warnings-as-errors',
+                    '-no-progress-bar', '-use-tuple-structs', 'false',
+                    str(work / 'probe.llbc')]),
+    ]
+    sources = sorted((root / 'zerocopy/src').rglob('*.rs')) + [
+        root / 'zerocopy/build.rs', root / 'zerocopy/Cargo.toml',
+        root / 'zerocopy/Cargo.lock', fixture / 'src/lib.rs',
+        fixture / 'Cargo.toml', fixture / 'Cargo.lock', Path(__file__).resolve(),
+    ]
+    evidence = {'case': args.case, 'fixture': str(fixture),
+                'runtime': str(runtime), 'runtime_metadata': metadata,
+                'charon_version': charon_version,
+                'repository_head': subprocess.check_output(
+                    ['git', 'rev-parse', 'HEAD'], cwd=root, text=True).strip(),
+                'repository_status': subprocess.check_output(
+                    ['git', 'status', '--porcelain'], cwd=root, text=True),
+                'source_sha256': {str(path.relative_to(root)):
+                    hashlib.sha256(path.read_bytes()).hexdigest()
+                    for path in sources}, 'steps': []}
+    for name, command in commands:
+        log_path = work / (name + '.log')
+        started = time.monotonic()
+        with log_path.open('w') as log:
+            result = subprocess.run(command, cwd=fixture, env=environment,
+                                    stdout=log, stderr=subprocess.STDOUT)
+        evidence['steps'].append({'name': name, 'command': command,
+                                  'exit_code': result.returncode,
+                                  'seconds': round(time.monotonic() - started, 2),
+                                  'log': str(log_path)})
+        (work / 'evidence.json').write_text(json.dumps(evidence, indent=2) + '\n')
+        print(name, result.returncode, log_path, flush=True)
+        if result.returncode:
+            return result.returncode
+    return 0
+
+
+if __name__ == '__main__':
+    raise SystemExit(main())
diff --git a/verification/aeneas/tests/capabilities/raw-pointers/Cargo.lock b/verification/aeneas/tests/capabilities/raw-pointers/Cargo.lock
new file mode 100644
index 0000000000..a4c65c14e6
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/raw-pointers/Cargo.lock
@@ -0,0 +1,61 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "raw-pointer-probe"
+version = "0.0.0"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.63"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.63"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/verification/aeneas/tests/capabilities/raw-pointers/Cargo.toml b/verification/aeneas/tests/capabilities/raw-pointers/Cargo.toml
new file mode 100644
index 0000000000..630530baec
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/raw-pointers/Cargo.toml
@@ -0,0 +1,12 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "raw-pointer-probe"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+zerocopy = { path = "../../../../../zerocopy", default-features = false }
diff --git a/verification/aeneas/tests/capabilities/raw-pointers/src/lib.rs b/verification/aeneas/tests/capabilities/raw-pointers/src/lib.rs
new file mode 100644
index 0000000000..8244c2fff0
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/raw-pointers/src/lib.rs
@@ -0,0 +1,21 @@
+// 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.
+
+use core::ptr::NonNull;
+
+pub fn cast(pointer: *const u32) -> *const u8 {
+    pointer as *const u8
+}
+
+pub fn with_len(pointer: *const u8, count: usize) -> *const [u8] {
+    core::ptr::slice_from_raw_parts(pointer, count)
+}
+
+pub fn nonnull(pointer: *mut u8) -> Option<NonNull<u8>> {
+    NonNull::new(pointer)
+}
diff --git a/verification/aeneas/tests/capabilities/std-transmute/Cargo.lock b/verification/aeneas/tests/capabilities/std-transmute/Cargo.lock
new file mode 100644
index 0000000000..81c95e1f23
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/std-transmute/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "std-transmute-probe"
+version = "0.0.0"
diff --git a/verification/aeneas/tests/capabilities/std-transmute/Cargo.toml b/verification/aeneas/tests/capabilities/std-transmute/Cargo.toml
new file mode 100644
index 0000000000..5dfbe5f385
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/std-transmute/Cargo.toml
@@ -0,0 +1,9 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "std-transmute-probe"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
diff --git a/verification/aeneas/tests/capabilities/std-transmute/src/lib.rs b/verification/aeneas/tests/capabilities/std-transmute/src/lib.rs
new file mode 100644
index 0000000000..73ca76f63e
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/std-transmute/src/lib.rs
@@ -0,0 +1,20 @@
+// Copyright 2026 The Fuchsia Authors
+// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+#[cfg(not(target_endian = "little"))]
+compile_error!("this concrete byte-conversion probe supports little-endian targets only");
+
+#[allow(unnecessary_transmutes)]
+pub fn to_bytes(value: u32) -> [u8; 4] {
+    unsafe { core::mem::transmute::<u32, [u8; 4]>(value) }
+}
+
+#[allow(unnecessary_transmutes)]
+pub fn from_bytes(value: [u8; 4]) -> u32 {
+    unsafe { core::mem::transmute::<[u8; 4], u32>(value) }
+}
+
+pub fn guarded_bool(value: u8) -> bool {
+    assert!(value < 2);
+    unsafe { core::mem::transmute::<u8, bool>(value) }
+}
diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs
index 1a5c8cb965..f2ded8d82e 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(all(kani, kani_slow))]
         #[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/primitive_checks.rs b/zerocopy/src/layout/primitive_checks.rs
index b1b0b2041f..bd34705c33 100644
--- a/zerocopy/src/layout/primitive_checks.rs
+++ b/zerocopy/src/layout/primitive_checks.rs
@@ -80,6 +80,45 @@ fn check_empty_layout(repr_align: Option<NonZeroUsize>) {
     assert!(empty.statically_shallow_unpadded);
 }
 
+/// Checks the actual built-in `[u32]` descriptor and every element count.
+///
+/// The ABI guard makes the primitive-read premises visible in the extracted
+/// model. The comparison retains overflow: both computations must return
+/// `None` when the mathematical byte length does not fit in `usize`.
+/// This checks one associated constant, not the complete `KnownLayout` trait.
+///
+/// ```aeneas
+/// spec u32_slice_known_layout_checks_spec
+///   ensures _ => True
+/// ```
+#[allow(clippy::arithmetic_side_effects)]
+fn check_u32_slice_known_layout(elems: usize) {
+    let size = mem::size_of::<u32>();
+    let align = mem::align_of::<u32>();
+    if !align.is_power_of_two() {
+        return;
+    }
+    if size % align != 0 {
+        return;
+    }
+
+    let slice = <[u32] as crate::KnownLayout>::LAYOUT;
+    assert!(slice.align.get() == align);
+    assert!(slice.statically_shallow_unpadded);
+    match slice.size_info {
+        SizeInfo::SliceDst(tail) => {
+            assert!(tail.offset == 0);
+            assert!(tail.elem_size == size);
+            assert!(tail.size_base == 0);
+            assert!(tail.size_rounding_align_and_phase.0.get() == align);
+            let actual = tail.size_for_elems(elems);
+            let expected = elems.checked_mul(size);
+            assert!(super::tail_checks::same_optional_usize(actual, expected));
+        }
+        SizeInfo::Sized { .. } => panic!("slice descriptor returned a sized layout"),
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -92,6 +131,9 @@ mod tests {
         check_primitive_layouts::<(u8, u64)>();
         check_primitive_layouts::<[u64; 3]>();
         check_empty_layout(None);
+        for elems in [0, 1, usize::MAX / 4, usize::MAX / 4 + 1, usize::MAX] {
+            check_u32_slice_known_layout(elems);
+        }
         for align in [1, 2, 8, 3] {
             check_empty_layout(NonZeroUsize::new(align));
         }
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,
+                    },
+                )),
+            );
+        }
+    }
+}