diff --git a/verification/aeneas/DESIGN.md b/verification/aeneas/DESIGN.md
index e990b8aa8c..5bcfc3c73a 100644
--- a/verification/aeneas/DESIGN.md
+++ b/verification/aeneas/DESIGN.md
@@ -491,3 +491,40 @@ success remains outside any conditional interpretation of a validity state.
 `AsInitialized` contents and opaque `MaybeUninit` storage remain deferred.
 Pointer casts and projections will additionally need explicit byte-range,
 metadata, access, and resource arguments. These content laws do not grant them.
+
+## Indexed storage and geometric projections
+
+There is one physical profile per retained `RustModel`. A fixed profile uses
+`BitDecoder`; an indexed profile uses `StorageDecoder` and retains its metadata
+type and equality. Ordinary slices use `usize` element counts. Transparent
+wrappers retain those counts. `IntoBytes` initialization covers every accepted
+language representation, and realizability supplies bytes at each admitted raw
+value's actual metadata. Neither law reconstructs metadata from byte length.
+
+Generic Lean providers are more general than Rust's `Sized` parameters. To keep
+array and wrapper laws valid for every supplied provider, indexed children also
+compose as mathematical sequences with an explicit list of child metadata.
+Array sequences check the declared count; slice sequences check the usize
+length bound. This total mathematical extension supplies no Rust ABI for an
+array of unsized elements. A native layout or pointer operation still needs its
+own admitted semantics and correspondence premises.
+
+The fixed-width `representation` API is derived from this profile. Owned zero
+initialization and transmutation require that projection to exist. The current
+native `FromBytes` and `FromZeros` laws retain their fixed-layout scope; indexed
+completeness remains an explicit `StorageDecoder.CompleteWith` proof. Extending
+those native laws requires carrying the `Sized`-related premises needed by
+owned-value methods, rather than silently guessing metadata for them.
+
+Geometric projection requires a bounded forward offset and unchanged opaque
+provenance. `Cast` additionally retains the start; `CastExact` retains the size.
+The shared library proves identity, composition, slice splitting, byte-count
+views, empty-destination bounds, and no-wrap consequences under explicit bounds.
+These numeric theorems grant no access permission or reference validity.
+
+Native pointer execution remains rejected: the unchanged Aeneas pin erases the
+observations these proofs need. Supporting native `Project`, `Cast`, or
+`CastExact` proofs will require a faithful pointer carrier and primitive
+translation. Associated-type equalities and recursive declaration limitations
+also continue to block the richer `KnownLayout` path. No backend overlay or
+assumed model of a local target bypasses those limits.
diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md
index c6d425327c..e9af0cdb16 100644
--- a/verification/aeneas/LOWERING_AUDIT.md
+++ b/verification/aeneas/LOWERING_AUDIT.md
@@ -124,8 +124,11 @@ operation in its dependency closure was faithfully modeled.
 [`Rust.Storage`](../../anneal/lean/Rust/Storage.lean) represents initialized and
 uninitialized bytes and fixed-width physical decoders as pure values.
 `BitDecoder.Initialized` says that every byte list accepted by a decoder is
-initialized. `RustModel.initializedRepresentation` requires an available
-physical decoder and this law; absence is `False`. The library's mathematical
+initialized. `RustModel.initializedRepresentation` requires an available physical profile
+and this law at every metadata value; absence is `False`. The single profile
+in `RustModel.storage` is either fixed or indexed. Its fixed `representation`
+accessor is a projection used by owned-value primitives, not a second physical
+interpretation. Slice storage takes its count explicitly. The library's mathematical
 `decode` cannot restrict that quantification. A decoder rejecting every byte
 list satisfies initialization vacuously, so its law alone does not establish
 correspondence with Rust.
diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index 0e3be3be3c..3bbb0bbfc0 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -735,7 +735,7 @@ mathematical decoder has at least one physical byte representation. Initializati
 alone cannot provide those bytes; an always-rejecting physical decoder would
 satisfy it vacuously. The reusable proofs in
 [`RustRealizability.lean`](lean/RustRealizability.lean) cover the same primitive,
-array, and wrapper families. No default source value, unique encoder, or
+array, slice, and wrapper families. No default source value, unique encoder, or
 inhabitedness assumption is introduced.
 
 There are 59 authored implementation markers: `()`, `bool`, `char`; all twelve
@@ -765,9 +765,9 @@ elements, so the same rule covers empty arrays, positive counts of zero-byte
 elements, and nested arrays. Padding within an element remains the element
 law's obligation. Wrapper decoders preserve the actual child's failures and
 initialization law. Generic `?Sized` impl bounds are retained; a supplied
-physical provider for an unsized value must also carry its applicable metadata
-and representation width. These conditional laws supply no universal DST
-representation model.
+physical profile for an unsized value retains its applicable metadata and
+representation width. Canonical slice profiles use usize element counts;
+other DST families still need explicit physical semantics.
 
 The byteorder structs have transparent byte-array storage plus an empty
 `PhantomData` field. In particular, `F32` and `F64` use `[u8; 4]` and `[u8; 8]`;
diff --git a/verification/aeneas/lean/DeriveModels.lean b/verification/aeneas/lean/DeriveModels.lean
index 7b332a32ef..dd1776b5ce 100644
--- a/verification/aeneas/lean/DeriveModels.lean
+++ b/verification/aeneas/lean/DeriveModels.lean
@@ -476,9 +476,9 @@ private meta def deriveProvider (raw : Name) (count : Nat)
     addDecl (.thmDecl {
       «name» := raw ++ `decode_decompose, levelParams := info.levelParams,
       «type» := (← inferType decomposition), value := decomposition }) (forceExpose := true)
-    let bitDecoderTy ← mkAppM ``Rust.Storage.BitDecoder #[rawTy]
-    let representation ← match physicalPayload with
-      | none => mkAppOptM ``Option.none #[some bitDecoderTy]
+    let storageTy ← mkAppM ``PhysicalStorage #[rawTy]
+    let storage ← match physicalPayload with
+      | none => mkAppOptM ``Option.none #[some storageTy]
       | some payload => do
         -- LLBC validation authorizes only named builtin storage wrappers. Lean
         -- independently checks that reconstruction uses the actual raw fields.
@@ -508,7 +508,15 @@ private meta def deriveProvider (raw : Name) (count : Nat)
                 values := values.push (← mkAppOptM ``Zerocopy.core.marker.PhantomData.mk
                   (ty.getAppArgs.map some))
             mkLambdaFVars #[value] (mkAppN ctor values)
-          mkAppOptM ``wrapperRepresentation #[some fieldTy, some rawTy, some child, some wrap]
+          -- The raw structure's actual payload projection preserves metadata.
+          -- Projecting it from the constructor reduces to the original payload,
+          -- so the kernel checks the inverse without an external wrapper axiom.
+          let unwrap ← withLocalDeclD `raw rawTy fun value =>
+            mkLambdaFVars #[value] (mkProj raw payload value)
+          let inverse ← withLocalDeclD `payload fieldTy fun value => do
+            mkLambdaFVars #[value] (← mkEqRefl value)
+          mkAppOptM ``wrapperStorage #[some fieldTy, some rawTy, some child, some wrap,
+            some unwrap, some inverse]
     -- Constructor application does not insert the defaults used by structure
     -- syntax. Supply the empty preference explicitly so generated providers
     -- contain no unresolved choice metavariable.
@@ -530,7 +538,7 @@ private meta def deriveProvider (raw : Name) (count : Nat)
       | some constructor => mkAppOptM ``Option.some #[some (mkConst ``ValidityMarker),
           some (mkConst constructor)]
     let provider ← mkAppOptM ``RustModel.mk #[some rawTy, some modelTy,
-      some (mkAppN (mkConst b.decoder levels) all), some representation, some choice,
+      some (mkAppN (mkConst b.decoder levels) all), some storage, some choice,
       some markerValue]
     addDefinition b.provider info.levelParams (← mkLambdaFVars all provider)
   setReducibilityStatus b.provider .reducible
diff --git a/verification/aeneas/lean/EmptyConstructionTests.lean b/verification/aeneas/lean/EmptyConstructionTests.lean
index 763c9fed3c..84726b795b 100644
--- a/verification/aeneas/lean/EmptyConstructionTests.lean
+++ b/verification/aeneas/lean/EmptyConstructionTests.lean
@@ -27,18 +27,18 @@ namespace EmptyConstructionTests
   decode raw := nomatch raw
 
 example : ¬ @RustModel.initializedRepresentation Empty modelEmpty := by
-  simp [RustModel.initializedRepresentation, RustModel.representation]
+  simp [RustModel.initializedRepresentation, RustModel.storage]
 
 example : modelEmpty.decodeBitsResult [] = .fail .undef := rfl
 example : modelEmpty.decodeBytesResult [] = .fail .undef := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode]
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, RustModel.decode]
 example : ¬ WP.spec (modelEmpty.decodeBytesResult []) (fun _ => True) := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation]
+    RustModel.decodeResult, RustModel.representation, RustModel.storage]
 example : ¬ WP.dspec (modelEmpty.decodeBytesResult []) (fun _ => True) := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation]
+    RustModel.decodeResult, RustModel.representation, RustModel.storage]
 
 inductive StateToken where
   | mk
@@ -52,13 +52,13 @@ inductive StateToken where
   decode _ := some ()
 
 example : ¬ @RustModel.initializedRepresentation StateToken inhabitedOnly := by
-  simp [RustModel.initializedRepresentation, RustModel.representation]
+  simp [RustModel.initializedRepresentation, RustModel.storage]
 
 example : (default : StateToken) = .mk := rfl
 example : inhabitedOnly.decode .mk = some () := rfl
 example : inhabitedOnly.decodeBytesResult [] = .fail .undef := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode]
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, RustModel.decode]
 
 -- Model an external admission condition explicitly. The physical decoder may
 -- supply the unit-like raw constructor while the full provider still rejects
@@ -66,24 +66,24 @@ example : inhabitedOnly.decodeBytesResult [] = .fail .undef := by
 @[reducible] def stateModel (masked : Bool) : RustModel StateToken where
   Model := Unit
   decode _ := if masked then some () else none
-  representation := some (emptyDecoder StateToken.mk)
+  storage := some (.fixed (emptyDecoder StateToken.mk))
 
 example : (stateModel false).decodeBitsResult [] = .ok StateToken.mk := rfl
 example : (stateModel true).decodeBytesResult [] = .ok () := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode,
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode,
     emptyDecoder, BitDecoder.run]
 example : (stateModel false).decodeBytesResult [] = .fail .undef := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode,
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode,
     emptyDecoder, BitDecoder.run]
 example : ¬ WP.spec ((stateModel false).decodeBytesResult []) (fun _ => True) := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode,
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode,
     emptyDecoder, BitDecoder.run]
 example : ¬ WP.dspec ((stateModel false).decodeBytesResult []) (fun _ => True) := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode,
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode,
     emptyDecoder, BitDecoder.run]
 
 -- Both states satisfy the physical initialization law. That law cannot prove
@@ -98,7 +98,7 @@ example : (modelPhantomData Empty).decodeBitsResult [] =
     .ok (Zerocopy.core.marker.PhantomData.mk : Zerocopy.core.marker.PhantomData Empty) := rfl
 example : (modelPhantomData Empty).decodeBytesResult [] = .ok () := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode,
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode,
     emptyDecoder, BitDecoder.run]
 
 end EmptyConstructionTests
diff --git a/verification/aeneas/lean/ModelPrelude.lean b/verification/aeneas/lean/ModelPrelude.lean
index 60239e648f..7f5d9df041 100644
--- a/verification/aeneas/lean/ModelPrelude.lean
+++ b/verification/aeneas/lean/ModelPrelude.lean
@@ -32,7 +32,7 @@ namespace AeneasSpecs
 @[reducible] instance modelPhantomData (T : Type) :
     RustModel (Zerocopy.core.marker.PhantomData T) :=
   { Model := Unit, «decode» := fun _ => some (),
-    representation := some (Rust.Storage.emptyDecoder Zerocopy.core.marker.PhantomData.mk) }
+    storage := some (.fixed (Rust.Storage.emptyDecoder Zerocopy.core.marker.PhantomData.mk)) }
 
 /-- This check fails if the pinned extracted carrier gains runtime fields. -/
 theorem phantomData_eq_mk (T : Type) (raw : Zerocopy.core.marker.PhantomData T) :
@@ -41,22 +41,37 @@ theorem phantomData_eq_mk (T : Type) (raw : Zerocopy.core.marker.PhantomData T)
   rfl
 
 
--- A wrapper has exactly its payload's accepted bytes. Missing child storage
--- semantics stay missing; a mathematical decoder never supplies those bytes.
+-- A wrapper has exactly its payload's accepted bytes and retains its metadata.
+-- Missing physical semantics stay missing; a mathematical decoder cannot supply them.
+def wrapperStorage {A B : Type} [ma : RustModel A] (wrap : A → B) (unwrap : B → A)
+    (inverse : ∀ raw, unwrap (wrap raw) = raw) : Option (PhysicalStorage B) :=
+  ma.storage.map (·.map wrap unwrap inverse)
+
+-- Fixed-layout consumers keep a projection of the same child's physical profile.
 def wrapperRepresentation {A B : Type} [ma : RustModel A] (wrap : A → B) :
     Option (Rust.Storage.BitDecoder B) := ma.representation.map (·.map wrap)
 
-theorem initializedWrapperRepresentation {A B : Type} [ma : RustModel A]
-    (wrap : A → B) (child : RustModel.initializedRepresentation A) :
-    match wrapperRepresentation wrap with
+@[simp] theorem wrapperStorage_fixed? {A B : Type} [ma : RustModel A]
+    (wrap : A → B) (unwrap : B → A) (inverse : ∀ raw, unwrap (wrap raw) = raw) :
+    (wrapperStorage wrap unwrap inverse).bind PhysicalStorage.fixed? =
+      wrapperRepresentation wrap := by
+  cases stored : ma.storage with
+  | none => simp [wrapperStorage, wrapperRepresentation, RustModel.representation, stored]
+  | some physical =>
+    simp [wrapperStorage, wrapperRepresentation, RustModel.representation, stored]
+
+theorem initializedWrapperStorage {A B : Type} [ma : RustModel A]
+    (wrap : A → B) (unwrap : B → A) (inverse : ∀ raw, unwrap (wrap raw) = raw)
+    (child : RustModel.initializedRepresentation A) :
+    match wrapperStorage wrap unwrap inverse with
     | none => False
-    | some decoder => decoder.Initialized := by
-  cases h : ma.representation with
-  | none => simp [RustModel.initializedRepresentation, h] at child
-  | some decoder =>
-    simp only [RustModel.initializedRepresentation, h] at child
-    simp only [wrapperRepresentation, h, Option.map_some]
-    exact Rust.Storage.BitDecoder.map_initialized decoder wrap child
+    | some physical => physical.Initialized := by
+  cases stored : ma.storage with
+  | none => simp [RustModel.initializedRepresentation, stored] at child
+  | some physical =>
+    simp only [wrapperStorage, stored, Option.map_some]
+    exact physical.map_initialized wrap unwrap inverse
+      (by simpa [RustModel.initializedRepresentation, stored] using child)
 
 -- These providers interpret stored values only. They do not model mutation,
 -- aliasing, synchronization, or destruction of the standard-library wrappers.
@@ -64,46 +79,46 @@ theorem initializedWrapperRepresentation {A B : Type} [ma : RustModel A]
     RustModel (core.mem.manually_drop.ManuallyDrop T) where
   Model := ma.Model
   decode raw := ma.decode raw.value
-  representation := wrapperRepresentation core.mem.manually_drop.ManuallyDrop.mk
+  storage := wrapperStorage core.mem.manually_drop.ManuallyDrop.mk (fun raw => raw.value) (fun _ => rfl)
   representationChoice raw := ma.representationChoice raw.value
 
 @[reducible] instance modelCell (T : Type) [ma : RustModel T] :
     RustModel (core.cell.Cell T) where
   Model := ma.Model
   decode raw := ma.decode raw.value
-  representation := wrapperRepresentation core.cell.Cell.mk
+  storage := wrapperStorage core.cell.Cell.mk (fun raw => raw.value) (fun _ => rfl)
 
 @[reducible] instance modelUnsafeCell (T : Type) [ma : RustModel T] :
     RustModel (core.cell.UnsafeCell T) where
   Model := ma.Model
   decode raw := ma.decode raw.value
-  representation := wrapperRepresentation core.cell.UnsafeCell.mk
+  storage := wrapperStorage core.cell.UnsafeCell.mk (fun raw => raw.value) (fun _ => rfl)
 
 @[reducible] instance modelWrapping (T : Type) [ma : RustModel T] :
     RustModel (Zerocopy.core.num.wrapping.Wrapping T) where
   Model := ma.Model
   decode raw := ma.decode raw._0
-  representation := wrapperRepresentation Zerocopy.core.num.wrapping.Wrapping.mk
+  storage := wrapperStorage Zerocopy.core.num.wrapping.Wrapping.mk (fun raw => raw._0) (fun _ => rfl)
 
 theorem initializedManuallyDrop (T : Type) [ma : RustModel T]
     (child : RustModel.initializedRepresentation T) :
     RustModel.initializedRepresentation (core.mem.manually_drop.ManuallyDrop T) :=
-  initializedWrapperRepresentation core.mem.manually_drop.ManuallyDrop.mk child
+  initializedWrapperStorage core.mem.manually_drop.ManuallyDrop.mk (fun raw => raw.value) (fun _ => rfl) child
 
 theorem initializedCell (T : Type) [ma : RustModel T]
     (child : RustModel.initializedRepresentation T) :
     RustModel.initializedRepresentation (core.cell.Cell T) :=
-  initializedWrapperRepresentation core.cell.Cell.mk child
+  initializedWrapperStorage core.cell.Cell.mk (fun raw => raw.value) (fun _ => rfl) child
 
 theorem initializedUnsafeCell (T : Type) [ma : RustModel T]
     (child : RustModel.initializedRepresentation T) :
     RustModel.initializedRepresentation (core.cell.UnsafeCell T) :=
-  initializedWrapperRepresentation core.cell.UnsafeCell.mk child
+  initializedWrapperStorage core.cell.UnsafeCell.mk (fun raw => raw.value) (fun _ => rfl) child
 
 theorem initializedWrapping (T : Type) [ma : RustModel T]
     (child : RustModel.initializedRepresentation T) :
     RustModel.initializedRepresentation (Zerocopy.core.num.wrapping.Wrapping T) :=
-  initializedWrapperRepresentation Zerocopy.core.num.wrapping.Wrapping.mk child
+  initializedWrapperStorage Zerocopy.core.num.wrapping.Wrapping.mk (fun raw => raw._0) (fun _ => rfl) child
 
 -- The bounds are proofs stored beside the value. They contribute constraints
 -- to the mathematical type without another runtime field or admission test.
@@ -161,11 +176,11 @@ abbrev u8BitDecoder := uScalarBitDecoder .U8
 @[reducible] instance modelUScalar (ty : UScalarTy) : RustModel (UScalar ty) where
   Model := UnsignedWord ty
   decode x := some (unsignedWord x)
-  representation := some (uScalarBitDecoder ty)
+  storage := some (.fixed (uScalarBitDecoder ty))
 @[reducible] instance modelIScalar (ty : IScalarTy) : RustModel (IScalar ty) where
   Model := SignedWord ty
   decode x := some (signedWord x)
-  representation := some (iScalarBitDecoder ty)
+  storage := some (.fixed (iScalarBitDecoder ty))
 
 /-- Char stores a Unicode scalar value in four bytes. Filtering the complete
 integer decoder rejects surrogates and out-of-range code points without ever
@@ -178,7 +193,7 @@ def charBitDecoder : Rust.Storage.BitDecoder Char :=
 @[reducible] instance modelChar : RustModel Char where
   Model := Char
   decode x := some x
-  representation := some charBitDecoder
+  storage := some (.fixed charBitDecoder)
 
 def nonzeroUScalarBitDecoder (ty : UScalarTy) (Inner : Type) :
     Rust.Storage.BitDecoder (core.num.nonzero.NonZero (UScalar ty) Inner) :=
@@ -194,13 +209,13 @@ def nonzeroIScalarBitDecoder (ty : IScalarTy) (Inner : Type) :
     RustModel (core.num.nonzero.NonZero (UScalar ty) Inner) where
   Model := NonZeroUnsignedWord ty
   decode raw := if h : 0 < raw.val.val then some ⟨unsignedWord raw.val, h⟩ else none
-  representation := some (nonzeroUScalarBitDecoder ty Inner)
+  storage := some (.fixed (nonzeroUScalarBitDecoder ty Inner))
 
 @[reducible] instance modelNonZeroIScalar (ty : IScalarTy) (Inner : Type) :
     RustModel (core.num.nonzero.NonZero (IScalar ty) Inner) where
   Model := NonZeroSignedWord ty
   decode raw := if h : raw.val.val ≠ 0 then some ⟨signedWord raw.val, h⟩ else none
-  representation := some (nonzeroIScalarBitDecoder ty Inner)
+  storage := some (.fixed (nonzeroIScalarBitDecoder ty Inner))
 
 -- Rust guarantees the zero niche for these particular standard-library
 -- wrappers. Map the full integer decoder: a zero is a successfully decoded
@@ -211,16 +226,16 @@ def nonzeroIScalarBitDecoder (ty : IScalarTy) (Inner : Type) :
     RustModel (Option (core.num.nonzero.NonZero (UScalar ty) Inner)) where
   Model := Option (NonZeroUnsignedWord ty)
   decode := (modelOption (ma := modelNonZeroUScalar ty Inner)).decode
-  representation := some ((uScalarBitDecoder ty).map fun word =>
-    if word.val = 0 then none else some ⟨word⟩)
+  storage := some (.fixed ((uScalarBitDecoder ty).map fun word =>
+    if word.val = 0 then none else some ⟨word⟩))
 
 @[reducible] instance (priority := 1001) modelOptionNonZeroIScalar
     (ty : IScalarTy) (Inner : Type) :
     RustModel (Option (core.num.nonzero.NonZero (IScalar ty) Inner)) where
   Model := Option (NonZeroSignedWord ty)
   decode := (modelOption (ma := modelNonZeroIScalar ty Inner)).decode
-  representation := some ((iScalarBitDecoder ty).map fun word =>
-    if word.val = 0 then none else some ⟨word⟩)
+  storage := some (.fixed ((iScalarBitDecoder ty).map fun word =>
+    if word.val = 0 then none else some ⟨word⟩))
 
 theorem initializedUScalar (ty : UScalarTy) :
     RustModel.initializedRepresentation (UScalar ty) :=
diff --git a/verification/aeneas/lean/NativeProviderAudit.lean b/verification/aeneas/lean/NativeProviderAudit.lean
index 118eb95221..b875271442 100644
--- a/verification/aeneas/lean/NativeProviderAudit.lean
+++ b/verification/aeneas/lean/NativeProviderAudit.lean
@@ -110,8 +110,8 @@ meta def auditNativeProviders (bindings : Json) : TermElabM Unit := do
   boundaryDefinition `AeneasSpecs.modelManuallyDrop
     (← `(fun (T : Type) [child : AeneasSpecs.RustModel T] =>
       ({ Model := child.Model, «decode» := fun raw => child.decode raw.value,
-         representation := child.representation.map
-           (fun decoder => decoder.map core.mem.manually_drop.ManuallyDrop.mk),
+         storage := child.storage.map (fun physical => physical.map
+           core.mem.manually_drop.ManuallyDrop.mk (fun raw => raw.value) (fun _ => rfl)),
          representationChoice := fun raw => child.representationChoice raw.value } :
         AeneasSpecs.RustModel (core.mem.manually_drop.ManuallyDrop T))))
     #[.default, .instImplicit]
diff --git a/verification/aeneas/lean/PhysicalModelTests.lean b/verification/aeneas/lean/PhysicalModelTests.lean
index 8eae1607d5..1e6dfa64ed 100644
--- a/verification/aeneas/lean/PhysicalModelTests.lean
+++ b/verification/aeneas/lean/PhysicalModelTests.lean
@@ -59,7 +59,7 @@ example : (modelOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner).de
 
 -- Missing physical semantics cannot establish a trait law by vacuity.
 example : ¬ RustModel.initializedRepresentation Nat := by
-  simp [RustModel.initializedRepresentation, RustModel.representation]
+  simp [RustModel.initializedRepresentation, RustModel.storage]
 
 -- This intentionally bad physical decoder accepts an uninitialized byte.
 -- Rejecting all library values cannot turn it into an IntoBytes interpretation.
@@ -70,7 +70,7 @@ def acceptsUninit : BitDecoder Nat where
 @[reducible] def rejectsEverything : RustModel Nat where
   Model := Unit
   decode _ := none
-  representation := some acceptsUninit
+  storage := some (.fixed acceptsUninit)
 
 example : ¬ @RustModel.initializedRepresentation Nat rejectsEverything := by
   intro law
@@ -82,11 +82,11 @@ example : (modelBool).decodeBitsResult [AMByte.init 2] = .fail .undef := rfl
 example : (modelBool).decodeBitsResult [] = .fail .undef := rfl
 example : (modelBool).decodeBytesResult [AMByte.init 1] = .ok true := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode, BitDecoder.run, boolDecoder]
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode, BitDecoder.run, boolDecoder]
 example : (modelUScalar .U8).decodeBytesResult [AMByte.init 255] =
     .ok (unsignedWord (255#u8)) := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode,
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode,
     uScalarBitDecoder, Rust.Storage.AeneasAdapter.unsignedDecoder,
     BitDecoder.map, BitDecoder.run, integerDecoder, collectInitialized,
     Rust.Bytes.decode, Rust.Bytes.decodeLE, UScalar.ofNatCore]
@@ -95,10 +95,10 @@ example : (modelUScalar .U8).decodeBytesResult [AMByte.init 255] =
 -- written postcondition makes no promise about the returned value.
 example : ¬ WP.spec (modelBool.decodeBytesResult [AMByte.init 2]) (fun _ => True) := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode, BitDecoder.run, boolDecoder]
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode, BitDecoder.run, boolDecoder]
 example : ¬ WP.dspec (modelBool.decodeBytesResult [AMByte.uninit]) (fun _ => True) := by
   simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
-    RustModel.decodeResult, RustModel.representation, RustModel.decode, BitDecoder.run, boolDecoder]
+    RustModel.decodeResult, RustModel.representation, RustModel.storage, PhysicalStorage.fixed?, RustModel.decode, BitDecoder.run, boolDecoder]
 
 -- An element-count recursion, rather than division by byte width, handles
 -- empty arrays, zero-sized elements, and nested arrays with the same rule.
diff --git a/verification/aeneas/lean/PhysicalStorage.lean b/verification/aeneas/lean/PhysicalStorage.lean
new file mode 100644
index 0000000000..2a488349e3
--- /dev/null
+++ b/verification/aeneas/lean/PhysicalStorage.lean
@@ -0,0 +1,116 @@
+/- 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 Rust.Storage
+@[expose] public section
+
+/-!
+A provider has one physical interpretation. Fixed storage is the Unit-metadata
+case; indexed storage retains its own metadata and equality test. The fixed
+accessor is deliberately partial: an owned-value primitive must not guess a
+slice count, even when several counts have the same byte width.
+
+Initialization and realizability range over the whole interpretation. The
+fixed accessor supports existing owned-value primitives and fixed-layout laws;
+it is a projection of this interpretation, never a second decoder to maintain.
+-/
+
+namespace AeneasSpecs
+open Rust.Storage
+
+inductive PhysicalStorage (Raw : Type u) where
+  | fixed (decoder : BitDecoder Raw)
+  | indexed (Metadata : Type) (equality : DecidableEq Metadata)
+      (decoder : StorageDecoder Metadata Raw)
+
+namespace PhysicalStorage
+
+def fixed? : PhysicalStorage Raw → Option (BitDecoder Raw)
+  | .fixed decoder => some decoder
+  | .indexed .. => none
+
+def Initialized : PhysicalStorage Raw → Prop
+  | .fixed decoder => decoder.Initialized
+  | .indexed _ equality decoder => @StorageDecoder.Initialized _ _ equality decoder
+
+/-- Realizability uses the raw value's actual metadata, not a guessed count. -/
+def Realizable (valid : Raw → Prop) : PhysicalStorage Raw → Prop
+  | .fixed decoder => ∀ raw, valid raw → ∃ bytes, decoder.run bytes = some raw
+  | .indexed _ equality decoder => ∀ raw, valid raw →
+      ∃ bytes, @StorageDecoder.run _ _ equality decoder (decoder.metadata raw) bytes = some raw
+
+/-- A storage wrapper keeps the child's metadata and byte interpretation.
+The inverse law concerns only wrapping a child, not a mathematical encoder. -/
+def map (physical : PhysicalStorage A) (wrap : A → B) (unwrap : B → A)
+    (inverse : ∀ raw, unwrap (wrap raw) = raw) : PhysicalStorage B :=
+  match physical with
+  | .fixed decoder => .fixed (decoder.map wrap)
+  | .indexed metadata equality decoder =>
+    .indexed metadata equality (decoder.map wrap (fun raw => decoder.metadata (unwrap raw))
+      (fun raw => congrArg decoder.metadata (inverse raw)))
+
+@[simp] theorem fixed?_map (physical : PhysicalStorage A) (wrap : A → B) (unwrap : B → A)
+    (inverse : ∀ raw, unwrap (wrap raw) = raw) :
+    (physical.map wrap unwrap inverse).fixed? = physical.fixed?.map (·.map wrap) := by
+  cases physical <;> rfl
+
+theorem map_initialized (physical : PhysicalStorage A) (wrap : A → B) (unwrap : B → A)
+    (inverse : ∀ raw, unwrap (wrap raw) = raw) (initialized : physical.Initialized) :
+    (physical.map wrap unwrap inverse).Initialized := by
+  cases physical with
+  | fixed decoder => exact BitDecoder.map_initialized decoder wrap initialized
+  | indexed metadata equality decoder =>
+    letI := equality
+    exact StorageDecoder.map_initialized decoder wrap (fun raw => decoder.metadata (unwrap raw))
+      (fun raw => congrArg decoder.metadata (inverse raw)) initialized
+
+theorem initialized_fixed {physical : PhysicalStorage Raw} {decoder : BitDecoder Raw}
+    (available : physical.fixed? = some decoder) (initialized : physical.Initialized) :
+    decoder.Initialized := by
+  cases physical with
+  | fixed selected => cases Option.some.inj available; exact initialized
+  | indexed => contradiction
+
+end PhysicalStorage
+end AeneasSpecs
+
+namespace Rust.Storage.StorageDecoder
+
+/-- A sequence carrier may restrict its length (fixed arrays or bounded slices).
+The original metadata and bytes are retained before checking that shape. -/
+def restrict [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw)
+    (valid : Raw → Prop) [DecidablePred valid] : StorageDecoder Metadata {raw // valid raw} where
+  byteSize := decoder.byteSize
+  metadata raw := decoder.metadata raw.val
+  decode metadata bytes := (decoder.run metadata bytes).bind fun raw =>
+    if h : valid raw then some ⟨raw, h⟩ else none
+
+@[simp] theorem run_restrict [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw)
+    (valid : Raw → Prop) [DecidablePred valid] (metadata : Metadata) (bytes : List AMByte) :
+    (decoder.restrict valid).run metadata bytes =
+      (decoder.run metadata bytes).bind (fun raw => if h : valid raw then some ⟨raw, h⟩ else none) := by
+  by_cases width : bytes.length = decoder.byteSize metadata
+  · cases language : decoder.decode metadata bytes with
+    | none => simp [run, restrict, width, language]
+    | some raw =>
+      by_cases agrees : decoder.metadata raw = metadata
+      · by_cases admitted : valid raw <;> simp [run, restrict, width, language, agrees, admitted]
+      · simp [run, restrict, width, language, agrees]
+  · simp [run, restrict, width]
+
+theorem restrict_initialized [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw)
+    (valid : Raw → Prop) [DecidablePred valid] (initialized : decoder.Initialized) :
+    (decoder.restrict valid).Initialized := by
+  intro metadata bytes raw accepted
+  rw [run_restrict] at accepted
+  cases language : decoder.run metadata bytes with
+  | none => simp [language] at accepted
+  | some output => exact initialized metadata bytes output language
+
+end Rust.Storage.StorageDecoder
diff --git a/verification/aeneas/lean/Proofs/IntoBytes.lean b/verification/aeneas/lean/Proofs/IntoBytes.lean
index e8542c972c..ca868e7d2f 100644
--- a/verification/aeneas/lean/Proofs/IntoBytes.lean
+++ b/verification/aeneas/lean/Proofs/IntoBytes.lean
@@ -253,7 +253,7 @@ namespace Zerocopy.Proofs
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (Zerocopy.wrappers.Unalign T)
       (Zerocopy.wrappers.Unalign.Insts.ZerocopyIntoBytes dictionary) :=
-  ⟨⟨initializedWrapperRepresentation Zerocopy.wrappers.Unalign.mk
+  ⟨⟨initializedWrapperStorage Zerocopy.wrappers.Unalign.mk (·._0) (fun _ => rfl)
     (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableUnalign T
     (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
@@ -262,7 +262,7 @@ namespace Zerocopy.Proofs
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (Zerocopy.wrappers.read_only_def.ReadOnly T)
       (Zerocopy.wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes dictionary) :=
-  ⟨⟨initializedWrapperRepresentation Zerocopy.wrappers.read_only_def.ReadOnly.mk
+  ⟨⟨initializedWrapperStorage Zerocopy.wrappers.read_only_def.ReadOnly.mk (·.inner) (fun _ => rfl)
     (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableReadOnly T
     (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
@@ -273,96 +273,96 @@ namespace Zerocopy.Proofs
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U16 O)
       (Zerocopy.byteorder.U16.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.U16.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.U16.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8)), realizableByteorderU16 O⟩⟩
 
 @[instance] theorem byteorder.U32.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U32 O)
       (Zerocopy.byteorder.U32.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.U32.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.U32.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderU32 O⟩⟩
 
 @[instance] theorem byteorder.U64.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U64 O)
       (Zerocopy.byteorder.U64.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.U64.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.U64.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderU64 O⟩⟩
 
 @[instance] theorem byteorder.U128.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U128 O)
       (Zerocopy.byteorder.U128.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.U128.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.U128.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8)), realizableByteorderU128 O⟩⟩
 
 @[instance] theorem byteorder.Usize.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.Usize O)
       (Zerocopy.byteorder.Usize.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.Usize.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.Usize.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderUsize O⟩⟩
 
 @[instance] theorem byteorder.I16.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I16 O)
       (Zerocopy.byteorder.I16.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.I16.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.I16.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8)), realizableByteorderI16 O⟩⟩
 
 @[instance] theorem byteorder.I32.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I32 O)
       (Zerocopy.byteorder.I32.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.I32.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.I32.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderI32 O⟩⟩
 
 @[instance] theorem byteorder.I64.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I64 O)
       (Zerocopy.byteorder.I64.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.I64.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.I64.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderI64 O⟩⟩
 
 @[instance] theorem byteorder.I128.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I128 O)
       (Zerocopy.byteorder.I128.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.I128.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.I128.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8)), realizableByteorderI128 O⟩⟩
 
 @[instance] theorem byteorder.Isize.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.Isize O)
       (Zerocopy.byteorder.Isize.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.Isize.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.Isize.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderIsize O⟩⟩
 
 @[instance] theorem byteorder.F32.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.F32 O)
       (Zerocopy.byteorder.F32.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.F32.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.F32.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderF32 O⟩⟩
 
 @[instance] theorem byteorder.F64.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.F64 O)
       (Zerocopy.byteorder.F64.Insts.ZerocopyIntoBytes O) :=
-  ⟨⟨initializedWrapperRepresentation
-    (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk)
+  ⟨⟨initializedWrapperStorage
+    (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderF64 O⟩⟩
 
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/ReferentValidity.lean b/verification/aeneas/lean/ReferentValidity.lean
index 408de92d5f..5586f7eea1 100644
--- a/verification/aeneas/lean/ReferentValidity.lean
+++ b/verification/aeneas/lean/ReferentValidity.lean
@@ -117,7 +117,7 @@ theorem safe_to_initialized (Src Dst : Type) [source : RustModel Src]
   refine ⟨admitted.1.trans same, ?_⟩
   obtain ⟨decoder, installed, raw, _, physical, _⟩ := admitted.2
   have initializes : decoder.Initialized := by
-    simpa only [RustModel.initializedRepresentation, installed] using initialized
+    exact source.initialized_fixed decoder installed initialized
   exact initializes bytes raw physical
 
 theorem initialized_to_safe (Src Dst : Type) [source : RustModel Src]
diff --git a/verification/aeneas/lean/ReferentWrappers.lean b/verification/aeneas/lean/ReferentWrappers.lean
index 28c275efb9..bbb548584b 100644
--- a/verification/aeneas/lean/ReferentWrappers.lean
+++ b/verification/aeneas/lean/ReferentWrappers.lean
@@ -65,27 +65,27 @@ theorem safeBytes_wrapper_iff {A B : Type} [ma : RustModel A] [mb : RustModel B]
 theorem safeBytes_manuallyDrop_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) :
     safeBytes (inferInstance : RustModel (core.mem.manually_drop.ManuallyDrop T)) bytes ↔
       safeBytes ma bytes :=
-  safeBytes_wrapper_iff core.mem.manually_drop.ManuallyDrop.mk rfl (fun _ => Iff.rfl) bytes
+  safeBytes_wrapper_iff core.mem.manually_drop.ManuallyDrop.mk (by simp only [RustModel.representation, RustModel.storage, wrapperStorage_fixed?]) (fun _ => Iff.rfl) bytes
 
 theorem safeBytes_cell_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) :
     safeBytes (inferInstance : RustModel (core.cell.Cell T)) bytes ↔ safeBytes ma bytes :=
-  safeBytes_wrapper_iff core.cell.Cell.mk rfl (fun _ => Iff.rfl) bytes
+  safeBytes_wrapper_iff core.cell.Cell.mk (by simp only [RustModel.representation, RustModel.storage, wrapperStorage_fixed?]) (fun _ => Iff.rfl) bytes
 
 theorem safeBytes_unsafeCell_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) :
     safeBytes (inferInstance : RustModel (core.cell.UnsafeCell T)) bytes ↔ safeBytes ma bytes :=
-  safeBytes_wrapper_iff core.cell.UnsafeCell.mk rfl (fun _ => Iff.rfl) bytes
+  safeBytes_wrapper_iff core.cell.UnsafeCell.mk (by simp only [RustModel.representation, RustModel.storage, wrapperStorage_fixed?]) (fun _ => Iff.rfl) bytes
 
 theorem safeBytes_wrapping_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) :
     safeBytes (inferInstance : RustModel (Zerocopy.core.num.wrapping.Wrapping T)) bytes ↔
       safeBytes ma bytes :=
-  safeBytes_wrapper_iff Zerocopy.core.num.wrapping.Wrapping.mk rfl (fun _ => Iff.rfl) bytes
+  safeBytes_wrapper_iff Zerocopy.core.num.wrapping.Wrapping.mk (by simp only [RustModel.representation, RustModel.storage, wrapperStorage_fixed?]) (fun _ => Iff.rfl) bytes
 
 /-- The generated model decodes its child before constructing a wrapper model.
 Its actual definition, rather than its physical layout alone, proves admission. -/
 theorem safeBytes_unalign_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) :
     safeBytes (inferInstance : RustModel (Zerocopy.wrappers.Unalign T)) bytes ↔
       safeBytes ma bytes := by
-  apply safeBytes_wrapper_iff Zerocopy.wrappers.Unalign.mk rfl ?_ bytes
+  apply safeBytes_wrapper_iff Zerocopy.wrappers.Unalign.mk (by simp only [RustModel.representation, RustModel.storage, wrapperStorage_fixed?]) ?_ bytes
   intro raw
   cases decoded : ma.decode raw <;>
     simp [RustModel.decode, Zerocopy.wrappers.Unalign.decode, Zerocopy.wrappers.Unalign.decodeFields, decoded]
@@ -93,7 +93,7 @@ theorem safeBytes_unalign_iff (T : Type) [ma : RustModel T] (bytes : List AMByte
 theorem safeBytes_readOnly_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) :
     safeBytes (inferInstance : RustModel (Zerocopy.wrappers.read_only_def.ReadOnly T)) bytes ↔
       safeBytes ma bytes := by
-  apply safeBytes_wrapper_iff Zerocopy.wrappers.read_only_def.ReadOnly.mk rfl ?_ bytes
+  apply safeBytes_wrapper_iff Zerocopy.wrappers.read_only_def.ReadOnly.mk (by simp only [RustModel.representation, RustModel.storage, wrapperStorage_fixed?]) ?_ bytes
   intro raw
   cases decoded : ma.decode raw <;>
     simp [RustModel.decode, Zerocopy.wrappers.read_only_def.ReadOnly.decode,
diff --git a/verification/aeneas/lean/RustModel.lean b/verification/aeneas/lean/RustModel.lean
index 2ee3eae4bd..b81dda2379 100644
--- a/verification/aeneas/lean/RustModel.lean
+++ b/verification/aeneas/lean/RustModel.lean
@@ -8,7 +8,7 @@ those terms. -/
 
 module
 public import Aeneas
-public import Rust.Storage
+public import PhysicalStorage
 public meta import Lean
 @[expose] public section
 
@@ -47,7 +47,7 @@ class RustModel (Raw : Type u) where
   /-- Optional language-level byte interpretation. Absence means that this
   provider cannot establish byte-validity laws.
   This decoder operates independently of the optional library invariant. -/
-  representation : Option (Rust.Storage.BitDecoder Raw) := none
+  storage : Option (PhysicalStorage Raw) := none
   /-- A preferred physical representation. Operations check it before use.
   Universally varying this field retains every accepted representation. -/
   representationChoice : Raw → List Rust.Storage.AMByte := fun _ => []
@@ -71,31 +71,61 @@ def isValid {Raw : Type u} [m : RustModel Raw] (raw : Raw) : Prop :=
 def decoded {Raw : Type u} (m : RustModel Raw) (raw : Raw) (value : m.Model) : Prop :=
   m.decode raw = some value
 
-/-- IntoBytes needs an available physical decoder whose entire language-valid
-representation domain is initialized. A library decoder cannot shrink this
-quantification: even a provider which rejects every mathematical value must
-establish initialization for all bytes accepted by its physical decoder. -/
+/-- The fixed-width compatibility API is derived from the sole physical profile.
+Indexed storage never acquires an invented fixed metadata value. -/
+def RustModel.representation {Raw : Type u} (m : RustModel Raw) :
+    Option (Rust.Storage.BitDecoder Raw) := m.storage.bind PhysicalStorage.fixed?
+
+/-- IntoBytes covers every accepted language representation at every metadata,
+independently of the optional library decoder. Missing storage fails closed. -/
 def RustModel.initializedRepresentation (Raw : Type u) [m : RustModel Raw] : Prop :=
-  match m.representation with
+  match m.storage with
   | none => False
-  | some decoder => decoder.Initialized
+  | some physical => physical.Initialized
 
-/-- Every admitted source has some physical representation. This is vacuous
-for uninhabited sources and does not require a canonical encoding. -/
+/-- Every admitted source has bytes at its actual metadata. This is vacuous
+for an uninhabited source and never constructs a default value. -/
 def RustModel.realizableRepresentation (Raw : Type u) [m : RustModel Raw] : Prop :=
-  match m.representation with
+  match m.storage with
   | none => False
-  | some decoder => ∀ raw, @isValid Raw m raw →
-      ∃ bytes, decoder.run bytes = some raw
+  | some physical => physical.Realizable (@isValid Raw m)
+
+/-- An owned operation may use the fixed projection only after this check. -/
+theorem RustModel.initialized_fixed {Raw : Type u} (m : RustModel Raw)
+    (decoder : Rust.Storage.BitDecoder Raw) (available : m.representation = some decoder)
+    (initialized : @RustModel.initializedRepresentation Raw m) : decoder.Initialized := by
+  cases stored : m.storage with
+  | none => simp [RustModel.representation, stored] at available
+  | some physical =>
+    simp only [RustModel.representation, stored, Option.bind_some] at available
+    exact physical.initialized_fixed available (by simpa [RustModel.initializedRepresentation, stored] using initialized)
+
+/-- Recover realizability for the fixed decoder selected by an owned operation. -/
+theorem RustModel.realizable_fixed {Raw : Type u} (m : RustModel Raw)
+    (decoder : Rust.Storage.BitDecoder Raw) (available : m.representation = some decoder)
+    (realizable : @RustModel.realizableRepresentation Raw m) :
+    ∀ raw, @isValid Raw m raw → ∃ bytes, decoder.run bytes = some raw := by
+  cases stored : m.storage with
+  | none => simp [RustModel.representation, stored] at available
+  | some physical =>
+    cases physical with
+    | fixed selected =>
+      have same : selected = decoder := by simpa [RustModel.representation, stored,
+        PhysicalStorage.fixed?] using available
+      subst selected
+      simpa [RustModel.realizableRepresentation, stored, PhysicalStorage.Realizable] using realizable
+    | indexed metadata equality selected =>
+      simp [RustModel.representation, stored, PhysicalStorage.fixed?] at available
 
 /-- Change the operational preference without changing either decoder. -/
 @[reducible] def RustModel.withChoice {Raw : Type u} (m : RustModel Raw)
     (choose : Raw → List Rust.Storage.AMByte) : RustModel Raw :=
   { m with representationChoice := choose }
 
-/-- Every initialized representation of the physical width admits a language
+/-- Fixed-layout FromBytes law. Every initialized representation admits a language
 value and a mathematical value through this same provider. Missing physical
-semantics fail closed. This law does not establish Rust layout correspondence,
+semantics fail closed. Indexed completeness is `StorageDecoder.CompleteWith`;
+this owned-value law requires the fixed projection. Neither establishes Rust layout correspondence,
 resource ownership, or the other obligations of a FromBytes implementation. -/
 def RustModel.completeRepresentation (Raw : Type u) [m : RustModel Raw] : Prop :=
   match m.representation with
@@ -312,13 +342,13 @@ theorem RustModel.dspec_decodeResult_iff {Raw : Type u} (m : RustModel Raw)
 @[reducible] instance modelBool : RustModel Bool where
   Model := Bool
   decode := some
-  representation := some Rust.Storage.boolDecoder
+  storage := some (.fixed Rust.Storage.boolDecoder)
 @[reducible] instance modelNat : RustModel Nat := { Model := Nat, «decode» := some }
 @[reducible] instance modelInt : RustModel Int := { Model := Int, «decode» := some }
 @[reducible] instance modelUnit : RustModel Unit where
   Model := Unit
   decode := some
-  representation := some Rust.Storage.unitDecoder
+  storage := some (.fixed Rust.Storage.unitDecoder)
 
 @[reducible] instance modelProd {α : Type u} {β : Type v} [ma : RustModel α] [mb : RustModel β] :
     RustModel (α × β) where
@@ -364,12 +394,6 @@ abbrev SliceValue (Element : Type u) :=
 abbrev ArrayValue (Element : Type u) (n : Usize) :=
   { values : List Element // values.length = n.val }
 
-@[reducible] instance modelSlice {α : Type u} [ma : RustModel α] : RustModel (Slice α) where
-  Model := SliceValue ma.Model
-  decode raw := match h : decodeList ma.decode raw.val with
-    | none => none
-    | some values => some ⟨values, (decodeList_length ma.decode h) ▸ raw.property⟩
-
 /-- Explicit physical slice adapter. The caller supplies a usize element count,
 including for zero-sized elements. Its value-level bound is carried by metadata,
 so no count is inferred from byte length and no extra Nat admission guard is needed. -/
@@ -411,34 +435,98 @@ theorem RustModel.sliceStorageDecoder_initialized {α : Type u}
   | none => simp [decoded] at language
   | some values => exact Rust.Storage.arrayDecode_initialized element initialized count.val bytes values decoded
 
+/-- Fixed arrays preserve fixed storage. Indexed children also compose as a
+pure sequence of explicitly supplied metadata; no Rust ABI is inferred for
+otherwise impossible instantiations such as an array of unsized elements. -/
+def PhysicalStorage.array (physical : PhysicalStorage α) (n : Usize) :
+    PhysicalStorage (Aeneas.Std.Array α n) :=
+  match physical with
+  | .fixed element => .fixed ((Rust.Storage.arrayDecoder element n.val).map
+      (fun values => Aeneas.Std.Array.from values.val values.property))
+  | .indexed metadata equality element =>
+    .indexed (List metadata) inferInstance
+      ((element.sequence.restrict (fun values => values.length = n.val)).map
+        (fun values => Aeneas.Std.Array.from values.val values.property)
+        (fun raw => raw.val.map element.metadata)
+        (fun values => by simp only [Aeneas.Std.Array.from_val]; rfl))
+
+/-- Ordinary Rust slices have usize element-count metadata. Composing already
+indexed mathematical children retains each child's metadata explicitly. This
+second case makes generic model laws total; it asserts no nested-DST Rust ABI. -/
+def PhysicalStorage.slice (physical : PhysicalStorage α) : PhysicalStorage (Slice α) :=
+  match physical with
+  | .fixed element => .indexed Usize inferInstance (RustModel.sliceStorageDecoder element)
+  | .indexed metadata equality element =>
+    .indexed (List metadata) inferInstance
+      ((element.sequence.restrict (fun values => values.length ≤ Usize.max)).map
+        (fun values => Slice.from values.val values.property)
+        (fun raw => raw.val.map element.metadata)
+        (fun values => by simp only [Slice.from_val]; rfl))
+
+@[reducible] instance modelSlice {α : Type u} [ma : RustModel α] : RustModel (Slice α) where
+  Model := SliceValue ma.Model
+  decode raw := match h : decodeList ma.decode raw.val with
+    | none => none
+    | some values => some ⟨values, (decodeList_length ma.decode h) ▸ raw.property⟩
+  storage := ma.storage.map PhysicalStorage.slice
+
 @[reducible] instance modelArray {α : Type u} (n : Usize) [ma : RustModel α] :
     RustModel (Aeneas.Std.Array α n) where
   Model := ArrayValue ma.Model n
   decode raw := match h : decodeList ma.decode raw.val with
     | none => none
     | some values => some ⟨values, (decodeList_length ma.decode h) ▸ raw.property⟩
-  representation := ma.representation.map (fun element =>
-    (Rust.Storage.arrayDecoder element n.val).map
-      (fun values => Aeneas.Std.Array.from values.val values.property))
+  storage := ma.storage.map (·.array n)
 
-/-- The language-level array representation concatenates element storage.
-This theorem concerns every accepted representation, including padding bytes;
-it never asks whether the optional library decoder accepts the decoded value. -/
+@[simp] theorem modelArray_representation {α : Type u} [ma : RustModel α] (n : Usize) :
+    (@modelArray α n ma).representation = ma.representation.map (fun element =>
+      (Rust.Storage.arrayDecoder element n.val).map
+        (fun values => Aeneas.Std.Array.from values.val values.property)) := by
+  change (ma.storage.map (·.array n)).bind PhysicalStorage.fixed? = _
+  cases stored : ma.storage with
+  | none => simp [RustModel.representation, stored]
+  | some physical => cases physical <;> simp [RustModel.representation,
+      PhysicalStorage.array, PhysicalStorage.fixed?, stored]
+
+theorem PhysicalStorage.initialized_array (physical : PhysicalStorage α) (n : Usize)
+    (initialized : physical.Initialized) : (physical.array n).Initialized := by
+  cases physical with
+  | fixed element =>
+    exact Rust.Storage.BitDecoder.map_initialized _ _
+      (Rust.Storage.arrayDecoder_initialized element initialized n.val)
+  | indexed metadata equality element =>
+    apply Rust.Storage.StorageDecoder.map_initialized
+    exact element.sequence.restrict_initialized _ (element.sequence_initialized initialized)
+
+theorem PhysicalStorage.initialized_slice (physical : PhysicalStorage α)
+    (initialized : physical.Initialized) : physical.slice.Initialized := by
+  cases physical with
+  | fixed element => exact RustModel.sliceStorageDecoder_initialized element initialized
+  | indexed metadata equality element =>
+    apply Rust.Storage.StorageDecoder.map_initialized
+    exact element.sequence.restrict_initialized _ (element.sequence_initialized initialized)
+
+/-- Initialization includes every language representation, independently of
+whether the mathematical decoder accepts the resulting raw value. -/
 theorem RustModel.initialized_array (α : Type u) [ma : RustModel α] (n : Usize)
     (element : RustModel.initializedRepresentation α) :
     @RustModel.initializedRepresentation (Aeneas.Std.Array α n) (@modelArray α n ma) := by
-  cases representation : ma.representation with
-  | none => simp [RustModel.initializedRepresentation, representation] at element
-  | some decoder =>
-    simp only [RustModel.initializedRepresentation, representation] at element
-    unfold RustModel.initializedRepresentation
-    rw [show (@modelArray α n ma).representation = ma.representation.map (fun element =>
-      (Rust.Storage.arrayDecoder element n.val).map
-        (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl]
-    rw [representation]
-    simp only [Option.map_some]
-    exact Rust.Storage.BitDecoder.map_initialized _ _
-      (Rust.Storage.arrayDecoder_initialized decoder element n.val)
+  cases stored : ma.storage with
+  | none => simp [RustModel.initializedRepresentation, stored] at element
+  | some physical =>
+    simp only [RustModel.initializedRepresentation, RustModel.storage, stored, Option.map_some]
+    exact physical.initialized_array n
+      (by simpa [RustModel.initializedRepresentation, stored] using element)
+
+theorem RustModel.initialized_slice (α : Type u) [ma : RustModel α]
+    (element : RustModel.initializedRepresentation α) :
+    @RustModel.initializedRepresentation (Slice α) (@modelSlice α ma) := by
+  cases stored : ma.storage with
+  | none => simp [RustModel.initializedRepresentation, stored] at element
+  | some physical =>
+    simp only [RustModel.initializedRepresentation, RustModel.storage, stored, Option.map_some]
+    exact physical.initialized_slice
+      (by simpa [RustModel.initializedRepresentation, stored] using element)
 
 -- This is Rust's Ok/Err payload type. Either constructor is admitted exactly
 -- when its selected child decodes, independently of Aeneas execution Result.
diff --git a/verification/aeneas/lean/RustRealizability.lean b/verification/aeneas/lean/RustRealizability.lean
index bb64337299..93e58a2eea 100644
--- a/verification/aeneas/lean/RustRealizability.lean
+++ b/verification/aeneas/lean/RustRealizability.lean
@@ -94,8 +94,7 @@ theorem RustModel.realizableRepresentation_exists {Raw : Type u} [m : RustModel
     (realizable : RustModel.realizableRepresentation Raw)
     (decoder : BitDecoder Raw) (available : m.representation = some decoder)
     (raw : Raw) (valid : isValid raw) : ∃ bytes, decoder.run bytes = some raw := by
-  simp only [RustModel.realizableRepresentation, available] at realizable
-  exact realizable raw valid
+  exact m.realizable_fixed decoder available realizable raw valid
 
 theorem realizableUScalar (ty : UScalarTy) :
     RustModel.realizableRepresentation (UScalar ty) := by
@@ -213,46 +212,57 @@ theorem realizableNonZeroIScalar (ty : IScalarTy) (Inner : Type) :
   rw [BitDecoder.run_filterMap, accepted]
   simp only [Option.bind_some, nonzero, ↓reduceIte]
 
-/-- A transparent wrapper reuses its payload's bytes. The inverse and validity
-premises also cover generated wrapper providers with their retained decoder. -/
+/-- A transparent wrapper reuses its payload's bytes at the same metadata.
+Both inverse laws ensure that every admitted wrapper is in the image of wrapping. -/
 theorem RustModel.realizable_of_wrapper {A B : Type} [ma : RustModel A] [mb : RustModel B]
-    (wrap : A → B) (unwrap : B → A) (inverse : ∀ raw, wrap (unwrap raw) = raw)
-    (representation : mb.representation = wrapperRepresentation wrap)
+    (wrap : A → B) (unwrap : B → A)
+    (leftInverse : ∀ raw, unwrap (wrap raw) = raw)
+    (rightInverse : ∀ raw, wrap (unwrap raw) = raw)
+    (storage : mb.storage = wrapperStorage wrap unwrap leftInverse)
     (validChild : ∀ raw, isValid raw → isValid (unwrap raw))
     (child : RustModel.realizableRepresentation A) :
     RustModel.realizableRepresentation B := by
-  cases available : ma.representation with
-  | none => simp [RustModel.realizableRepresentation, available] at child
-  | some decoder =>
-    simp only [RustModel.realizableRepresentation, available] at child
-    simp only [RustModel.realizableRepresentation, representation,
-      wrapperRepresentation, available, Option.map_some]
-    intro raw valid
-    obtain ⟨bytes, accepted⟩ := child (unwrap raw) (validChild raw valid)
-    exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp [inverse]⟩
+  cases stored : ma.storage with
+  | none => simp [RustModel.realizableRepresentation, stored] at child
+  | some physical =>
+    simp only [RustModel.realizableRepresentation, stored] at child
+    simp only [RustModel.realizableRepresentation, storage, wrapperStorage, stored, Option.map_some]
+    cases physical with
+    | fixed decoder =>
+      intro raw valid
+      obtain ⟨bytes, accepted⟩ := child (unwrap raw) (validChild raw valid)
+      exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp [rightInverse]⟩
+    | indexed metadata equality decoder =>
+      intro raw valid
+      obtain ⟨bytes, accepted⟩ := child (unwrap raw) (validChild raw valid)
+      refine ⟨bytes, ?_⟩
+      rw [StorageDecoder.run_map]
+      simp only [StorageDecoder.map]
+      rw [accepted]
+      simp [rightInverse]
 
 theorem realizableManuallyDrop (T : Type) [ma : RustModel T]
     (child : RustModel.realizableRepresentation T) :
     RustModel.realizableRepresentation (core.mem.manually_drop.ManuallyDrop T) :=
-  RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl
+  RustModel.realizable_of_wrapper _ (·.value) (by intro raw; rfl) (by rintro ⟨raw⟩; rfl) rfl
     (fun _ valid => valid) child
 
 theorem realizableCell (T : Type) [ma : RustModel T]
     (child : RustModel.realizableRepresentation T) :
     RustModel.realizableRepresentation (core.cell.Cell T) :=
-  RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl
+  RustModel.realizable_of_wrapper _ (·.value) (by intro raw; rfl) (by rintro ⟨raw⟩; rfl) rfl
     (fun _ valid => valid) child
 
 theorem realizableUnsafeCell (T : Type) [ma : RustModel T]
     (child : RustModel.realizableRepresentation T) :
     RustModel.realizableRepresentation (core.cell.UnsafeCell T) :=
-  RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl
+  RustModel.realizable_of_wrapper _ (·.value) (by intro raw; rfl) (by rintro ⟨raw⟩; rfl) rfl
     (fun _ valid => valid) child
 
 theorem realizableWrapping (T : Type) [ma : RustModel T]
     (child : RustModel.realizableRepresentation T) :
     RustModel.realizableRepresentation (Zerocopy.core.num.wrapping.Wrapping T) :=
-  RustModel.realizable_of_wrapper _ (·._0) (by rintro ⟨raw⟩; rfl) rfl
+  RustModel.realizable_of_wrapper _ (·._0) (by intro raw; rfl) (by rintro ⟨raw⟩; rfl) rfl
     (fun _ valid => valid) child
 
 /-- Successful list decoding admits every stored element with the same provider. -/
@@ -295,28 +305,21 @@ theorem RustModel.valid_array {α : Type u} [ma : RustModel α] {n : Usize}
     contradiction
   · exact ⟨_, rfl⟩
 
-theorem RustModel.realizable_array (α : Type u) [ma : RustModel α] (n : Usize)
-    (element : RustModel.realizableRepresentation α) :
-    @RustModel.realizableRepresentation (Aeneas.Std.Array α n) (@modelArray α n ma) := by
-  cases available : ma.representation with
-  | none => simp [RustModel.realizableRepresentation, available] at element
-  | some decoder =>
-    simp only [RustModel.realizableRepresentation, available] at element
-    unfold RustModel.realizableRepresentation
-    rw [show (@modelArray α n ma).representation = ma.representation.map (fun element =>
-      (arrayDecoder element n.val).map
-        (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl]
-    rw [available]
-    simp only [Option.map_some]
-    intro raw valid
-    obtain ⟨model, accepted⟩ := valid
-    have all : ∀ item ∈ raw.val, isValid item := by
-      dsimp only [RustModel.decode] at accepted
-      split at accepted
-      · contradiction
-      · rename_i values decoded
-        exact decodeList_valid raw.val values decoded
-    obtain ⟨bytes, width, physical⟩ := arrayDecode_realizable decoder isValid element raw.val all
+/-- Restricting mathematical admission preserves existing physical witnesses. -/
+theorem PhysicalStorage.realizable_mono (physical : PhysicalStorage Raw)
+    (source destination : Raw → Prop) (realizable : physical.Realizable source)
+    (preserves : ∀ raw, destination raw → source raw) : physical.Realizable destination := by
+  cases physical <;> exact fun raw valid => realizable raw (preserves raw valid)
+
+/-- Arrays compose representations of admitted children. Indexed children use
+an explicit metadata list, retaining every element boundary even at size zero. -/
+theorem PhysicalStorage.realizable_array (physical : PhysicalStorage α) (n : Usize)
+    (valid : α → Prop) (realizable : physical.Realizable valid) :
+    (physical.array n).Realizable (fun raw => ∀ item ∈ raw.val, valid item) := by
+  cases physical with
+  | fixed decoder =>
+    intro raw all
+    obtain ⟨bytes, width, physical⟩ := arrayDecode_realizable decoder valid realizable raw.val all
     refine ⟨bytes, ?_⟩
     rw [BitDecoder.run_map]
     have rawLength : raw.val.length = n.val := raw.property
@@ -330,5 +333,95 @@ theorem RustModel.realizable_array (α : Type u) [ma : RustModel α] (n : Usize)
       Aeneas.Std.Array.ext _ _ (Aeneas.Std.Array.from_val _ _)
     simp only [rawLength] at width
     simp [BitDecoder.run, arrayDecoder, width, decoded, fromRaw]
+  | indexed metadata equality decoder =>
+    intro raw all
+    obtain ⟨bytes, accepted⟩ := decoder.sequence_realizable valid realizable
+      (raw.val.map decoder.metadata) raw.val rfl all
+    refine ⟨bytes, ?_⟩
+    rw [StorageDecoder.run_map, StorageDecoder.run_restrict]
+    simp only [StorageDecoder.map]
+    rw [accepted]
+    simp only [raw.property, ↓reduceDIte, Option.bind_some, Option.map_some]
+    congr 1
+    exact Aeneas.Std.Array.ext _ _ (Aeneas.Std.Array.from_val _ _)
+
+/-- Slice realizability retains the raw slice's actual count. Indexed children
+compose their own metadata without claiming a nested-DST Rust layout. -/
+theorem PhysicalStorage.realizable_slice (physical : PhysicalStorage α)
+    (valid : α → Prop) (realizable : physical.Realizable valid) :
+    physical.slice.Realizable (fun raw => ∀ item ∈ raw.val, valid item) := by
+  cases physical with
+  | fixed decoder =>
+    intro raw all
+    obtain ⟨bytes, accepted⟩ := arrayDecoder_realizable decoder valid realizable raw.val all
+    refine ⟨bytes, ?_⟩
+    rw [RustModel.sliceStorageDecoder_run]
+    dsimp only [RustModel.sliceStorageDecoder]
+    have rawCount : raw.val.length = raw.len.val := by simp
+    have transport (count : Nat) (h : raw.val.length = count) :
+        (arrayDecoder decoder count).run bytes = some ⟨raw.val, h⟩ := by
+      cases h
+      exact accepted
+    rw [transport raw.len.val rawCount]
+    simp only [Option.map_some]
+    congr 1
+    exact Slice.ext _ _ (Slice.from_val _ _)
+  | indexed metadata equality decoder =>
+    intro raw all
+    obtain ⟨bytes, accepted⟩ := decoder.sequence_realizable valid realizable
+      (raw.val.map decoder.metadata) raw.val rfl all
+    refine ⟨bytes, ?_⟩
+    rw [StorageDecoder.run_map, StorageDecoder.run_restrict]
+    simp only [StorageDecoder.map]
+    rw [accepted]
+    simp only [raw.property, ↓reduceDIte, Option.bind_some, Option.map_some]
+    congr 1
+    exact Slice.ext _ _ (Slice.from_val _ _)
+
+theorem RustModel.realizable_array (α : Type u) [ma : RustModel α] (n : Usize)
+    (element : RustModel.realizableRepresentation α) :
+    @RustModel.realizableRepresentation (Aeneas.Std.Array α n) (@modelArray α n ma) := by
+  cases stored : ma.storage with
+  | none => simp [RustModel.realizableRepresentation, stored] at element
+  | some physical =>
+    simp only [RustModel.realizableRepresentation, RustModel.storage, stored, Option.map_some]
+    apply (physical.array n).realizable_mono _ _ (physical.realizable_array n isValid
+      (by simpa [RustModel.realizableRepresentation, stored] using element))
+    intro raw valid
+    obtain ⟨value, accepted⟩ := valid
+    dsimp only [RustModel.decode] at accepted
+    split at accepted
+    · contradiction
+    · rename_i values decoded
+      exact decodeList_valid raw.val values decoded
+
+/-- Slice admission follows from admission of every stored element. -/
+theorem RustModel.valid_slice {α : Type u} [ma : RustModel α]
+    (raw : Slice α) (valid : ∀ item ∈ raw.val, isValid item) : isValid raw := by
+  obtain ⟨values, decoded⟩ := decodeList_exists raw.val valid
+  unfold isValid
+  dsimp only [RustModel.decode]
+  split
+  · rename_i rejected
+    rw [decoded] at rejected
+    contradiction
+  · exact ⟨_, rfl⟩
+
+theorem RustModel.realizable_slice (α : Type u) [ma : RustModel α]
+    (element : RustModel.realizableRepresentation α) :
+    @RustModel.realizableRepresentation (Slice α) (@modelSlice α ma) := by
+  cases stored : ma.storage with
+  | none => simp [RustModel.realizableRepresentation, stored] at element
+  | some physical =>
+    simp only [RustModel.realizableRepresentation, RustModel.storage, stored, Option.map_some]
+    apply physical.slice.realizable_mono _ _ (physical.realizable_slice isValid
+      (by simpa [RustModel.realizableRepresentation, stored] using element))
+    intro raw valid
+    obtain ⟨value, accepted⟩ := valid
+    dsimp only [RustModel.decode] at accepted
+    split at accepted
+    · contradiction
+    · rename_i values decoded
+      exact decodeList_valid raw.val values decoded
 
 end AeneasSpecs
diff --git a/verification/aeneas/lean/RustRealizabilityModels.lean b/verification/aeneas/lean/RustRealizabilityModels.lean
index 7294a926ad..0b7b302768 100644
--- a/verification/aeneas/lean/RustRealizabilityModels.lean
+++ b/verification/aeneas/lean/RustRealizabilityModels.lean
@@ -22,7 +22,7 @@ theorem realizableUnalign (T : Type) [ma : RustModel T]
     (child : RustModel.realizableRepresentation T) :
     RustModel.realizableRepresentation (Zerocopy.wrappers.Unalign T) := by
   apply RustModel.realizable_of_wrapper Zerocopy.wrappers.Unalign.mk (·._0)
-    (by rintro ⟨raw⟩; rfl) rfl ?_ child
+    (by intro raw; rfl) (by rintro ⟨raw⟩; rfl) rfl ?_ child
   intro raw valid
   obtain ⟨value, accepted⟩ := valid
   cases decoded : ma.decode raw._0 with
@@ -33,7 +33,7 @@ theorem realizableReadOnly (T : Type) [ma : RustModel T]
     (child : RustModel.realizableRepresentation T) :
     RustModel.realizableRepresentation (Zerocopy.wrappers.read_only_def.ReadOnly T) := by
   apply RustModel.realizable_of_wrapper Zerocopy.wrappers.read_only_def.ReadOnly.mk (·.inner)
-    (by rintro ⟨raw⟩; rfl) rfl ?_ child
+    (by intro raw; rfl) (by rintro ⟨raw⟩; rfl) rfl ?_ child
   intro raw valid
   obtain ⟨value, accepted⟩ := valid
   cases decoded : ma.decode raw.inner with
@@ -44,7 +44,7 @@ theorem realizableByteorderU16 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.U16 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.U16.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (2#usize) (realizableUScalar .U8))
 
@@ -52,7 +52,7 @@ theorem realizableByteorderU32 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.U32 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.U32.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8))
 
@@ -60,7 +60,7 @@ theorem realizableByteorderU64 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.U64 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.U64.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
 
@@ -68,7 +68,7 @@ theorem realizableByteorderU128 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.U128 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.U128.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (16#usize) (realizableUScalar .U8))
 
@@ -76,7 +76,7 @@ theorem realizableByteorderUsize (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.Usize O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.Usize.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
 
@@ -84,7 +84,7 @@ theorem realizableByteorderI16 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.I16 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.I16.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (2#usize) (realizableUScalar .U8))
 
@@ -92,7 +92,7 @@ theorem realizableByteorderI32 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.I32 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.I32.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8))
 
@@ -100,7 +100,7 @@ theorem realizableByteorderI64 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.I64 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.I64.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
 
@@ -108,7 +108,7 @@ theorem realizableByteorderI128 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.I128 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.I128.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (16#usize) (realizableUScalar .U8))
 
@@ -116,7 +116,7 @@ theorem realizableByteorderIsize (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.Isize O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.Isize.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
 
@@ -124,7 +124,7 @@ theorem realizableByteorderF32 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.F32 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.F32.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8))
 
@@ -132,7 +132,7 @@ theorem realizableByteorderF64 (O : Type) [RustModel O] :
     RustModel.realizableRepresentation (Zerocopy.byteorder.F64 O) := by
   apply RustModel.realizable_of_wrapper
     (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (·._0) (by intro raw; rfl) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
     (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
     (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
 
diff --git a/verification/aeneas/lean/RustRealizabilityTests.lean b/verification/aeneas/lean/RustRealizabilityTests.lean
index cf7028d4f6..a2f52cdc57 100644
--- a/verification/aeneas/lean/RustRealizabilityTests.lean
+++ b/verification/aeneas/lean/RustRealizabilityTests.lean
@@ -40,7 +40,7 @@ example (T : Type) : RustModel.realizableRepresentation
 @[reducible] def missingTrue : RustModel Bool where
   Model := Bool
   «decode» := some
-  representation := some (emptyDecoder false)
+  storage := some (.fixed (emptyDecoder false))
 
 example : @RustModel.initializedRepresentation Bool missingTrue := emptyDecoder_initialized false
 example : ¬ @RustModel.realizableRepresentation Bool missingTrue := by
@@ -64,7 +64,7 @@ example : ¬ @RustModel.realizableRepresentation Empty noPhysical := by
 @[reducible] def emptyPhysical : RustModel Empty where
   Model := Empty
   «decode» := some
-  representation := some { byteSize := 0, «decode» := fun _ => none }
+  storage := some (.fixed { byteSize := 0, «decode» := fun _ => none })
 
 theorem emptyRealizable : @RustModel.realizableRepresentation Empty emptyPhysical := by
   intro raw
@@ -79,7 +79,7 @@ example : @RustModel.realizableRepresentation (Aeneas.Std.Array Empty (0#usize))
 @[reducible] def ambiguous : RustModel Bool where
   Model := Unit
   «decode» raw := if raw then none else some ()
-  representation := some ((uScalarBitDecoder .U8).map fun _ => false)
+  storage := some (.fixed ((uScalarBitDecoder .U8).map fun _ => false))
 
 theorem ambiguousRealizable : @RustModel.realizableRepresentation Bool ambiguous := by
   intro raw valid
diff --git a/verification/aeneas/lean/RustRepresentation.lean b/verification/aeneas/lean/RustRepresentation.lean
index f32519c520..547df69c3c 100644
--- a/verification/aeneas/lean/RustRepresentation.lean
+++ b/verification/aeneas/lean/RustRepresentation.lean
@@ -107,7 +107,7 @@ theorem RustModel.complete_array (α : Type u) [ma : RustModel α] (n : Usize)
     unfold RustModel.completeRepresentation
     rw [show (@modelArray α n ma).representation = ma.representation.map (fun element =>
       (arrayDecoder element n.val).map
-        (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl]
+        (fun values => Aeneas.Std.Array.from values.val values.property)) from modelArray_representation n]
     rw [available]
     simp only [Option.map_some]
     change ∀ bytes, bytes.length = n.val * decoder.byteSize → Initialized bytes → _
@@ -164,7 +164,7 @@ theorem RustModel.zero_array (α : Type u) [ma : RustModel α] (n : Usize)
     unfold RustModel.zeroRepresentation
     rw [show (@modelArray α n ma).representation = ma.representation.map (fun element =>
       (arrayDecoder element n.val).map
-        (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl]
+        (fun values => Aeneas.Std.Array.from values.val values.property)) from modelArray_representation n]
     rw [available]
     simp only [Option.map_some]
     refine ⟨Aeneas.Std.Array.from raw.val raw.property,
diff --git a/verification/aeneas/lean/RustRepresentationTests.lean b/verification/aeneas/lean/RustRepresentationTests.lean
index f3b391717f..934fa7bd37 100644
--- a/verification/aeneas/lean/RustRepresentationTests.lean
+++ b/verification/aeneas/lean/RustRepresentationTests.lean
@@ -67,9 +67,9 @@ example : (modelNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).zeroedRe
 
 -- Missing physical semantics fail closed even for an inhabited raw carrier.
 example : ¬ RustModel.completeRepresentation Nat := by
-  simp [RustModel.completeRepresentation, RustModel.representation]
+  simp [RustModel.completeRepresentation, RustModel.representation, RustModel.storage]
 example : ¬ RustModel.zeroRepresentation Nat := by
-  simp [RustModel.zeroRepresentation, RustModel.representation]
+  simp [RustModel.zeroRepresentation, RustModel.representation, RustModel.storage]
 example : modelNat.zeroedResult = .fail .undef := rfl
 
 -- The same physical domain with a provider rejecting zero must reject the
@@ -77,7 +77,7 @@ example : modelNat.zeroedResult = .fail .undef := rfl
 @[reducible] def rejectsZero : RustModel U8 where
   Model := Unit
   decode raw := if raw.val = 0 then none else some ()
-  representation := some (uScalarBitDecoder .U8)
+  storage := some (.fixed (uScalarBitDecoder .U8))
 
 theorem rejectsZero_not_zero : ¬ @RustModel.zeroRepresentation U8 rejectsZero := by
   intro zero
diff --git a/verification/aeneas/lean/TransmuteModel.lean b/verification/aeneas/lean/TransmuteModel.lean
index 5d90131c6e..b376c5d7dd 100644
--- a/verification/aeneas/lean/TransmuteModel.lean
+++ b/verification/aeneas/lean/TransmuteModel.lean
@@ -7,7 +7,7 @@ This file may not be copied, modified, or distributed except according to
 those terms. -/
 
 module
-public import ModelPrelude
+public import RustRealizability
 @[expose] public section
 
 /-!
@@ -187,13 +187,16 @@ theorem transmuteCopyResult_admitted {Src : Type u} {Dst : Type v}
     ∃ dst value, source.transmuteCopyResult destination src = .ok dst ∧
       destination.decode dst = some value ∧ source.byteCastWith destination src dst := by
   cases hs : source.representation with
-  | none => simp [initializedRepresentation, hs] at initialized
+  | none =>
+    cases hd : destination.representation with
+    | none => simp [completeRepresentation, hd] at complete
+    | some decoder => simp [hs, hd] at sameWidth
   | some sd =>
     cases hd : destination.representation with
     | none => simp [completeRepresentation, hd] at complete
     | some dd =>
-      simp only [initializedRepresentation, hs] at initialized
-      simp only [realizableRepresentation, hs] at realizable
+      have initialized := source.initialized_fixed sd hs initialized
+      have realizable := source.realizable_fixed sd hs realizable
       simp only [completeRepresentation, hd] at complete
       have width : sd.byteSize = dd.byteSize := by simpa [hs, hd] using sameWidth
       obtain ⟨initial, initialAccepted⟩ := realizable src valid
@@ -254,7 +257,9 @@ end RustModel
 
 @[simp] theorem manuallyDrop_representation {T : Type} (m : RustModel T) :
     (modelManuallyDrop T (ma := m)).representation =
-      m.representation.map (·.map core.mem.manually_drop.ManuallyDrop.mk) := rfl
+      m.representation.map (·.map core.mem.manually_drop.ManuallyDrop.mk) := by
+  change (wrapperStorage _ _ _).bind PhysicalStorage.fixed? = _
+  exact wrapperStorage_fixed? _ _ _
 
 theorem manuallyDrop_represented {T : Type} (m : RustModel T) (raw : T) (bytes : List AMByte) :
     (modelManuallyDrop T (ma := m)).represented ⟨raw⟩ bytes ↔ m.represented raw bytes := by
@@ -281,21 +286,13 @@ theorem manuallyDrop_withChoice {T : Type} (m : RustModel T)
 @[simp] theorem manuallyDrop_width {T : Type} (m : RustModel T) :
     (modelManuallyDrop T (ma := m)).representation.map (·.byteSize) =
       m.representation.map (·.byteSize) := by
-  change (m.representation.map (·.map core.mem.manually_drop.ManuallyDrop.mk)).map (·.byteSize) = _
+  rw [manuallyDrop_representation]
   cases h : m.representation <;> simp [BitDecoder.map]
 
 theorem manuallyDrop_realizable {T : Type} (m : RustModel T)
     (realizable : @RustModel.realizableRepresentation T m) :
     @RustModel.realizableRepresentation (core.mem.manually_drop.ManuallyDrop T)
       (modelManuallyDrop T (ma := m)) := by
-  cases h : m.representation with
-  | none => simp [RustModel.realizableRepresentation, h] at realizable
-  | some decoder =>
-    simp only [RustModel.realizableRepresentation, h] at realizable
-    unfold RustModel.realizableRepresentation
-    rw [manuallyDrop_representation, h]
-    intro raw valid
-    obtain ⟨bytes, accepted⟩ := realizable raw.value valid
-    exact ⟨bytes, by simp [BitDecoder.run_map, accepted]⟩
+  exact realizableManuallyDrop T realizable
 
 end AeneasSpecs
diff --git a/verification/aeneas/lean/TransmuteModelTests.lean b/verification/aeneas/lean/TransmuteModelTests.lean
index 6c63e9f27d..bbe1ef74ba 100644
--- a/verification/aeneas/lean/TransmuteModelTests.lean
+++ b/verification/aeneas/lean/TransmuteModelTests.lean
@@ -17,12 +17,12 @@ namespace TransmuteModelTests
 @[reducible] def ambiguousSource : RustModel Unit where
   Model := Unit
   decode := some
-  representation := some (byteDecoder.map fun _ => ())
+  storage := some (.fixed (byteDecoder.map fun _ => ()))
 
 @[reducible] def byteDestination : RustModel Rust.Bytes.Byte where
   Model := Rust.Bytes.Byte
   decode := some
-  representation := some byteDecoder
+  storage := some (.fixed byteDecoder)
 
 theorem ambiguous_source_initialized : @RustModel.initializedRepresentation Unit ambiguousSource :=
   BitDecoder.map_initialized _ _ byteDecoder_initialized
@@ -66,7 +66,7 @@ example (choose : Unit → List AMByte) :
 @[reducible] def rejectsAllSource : RustModel Unit where
   Model := Unit
   decode := some
-  representation := some { byteSize := 1, decode := fun _ => none }
+  storage := some (.fixed { byteSize := 1, decode := fun _ => none })
 
 example : @RustModel.initializedRepresentation Unit rejectsAllSource := by
   intro bytes raw accepted
@@ -90,7 +90,7 @@ example : rejectsAllSource.transmuteCopyResult byteDestination () = .fail .undef
 @[reducible] def emptySource : RustModel Empty where
   Model := Empty
   decode raw := nomatch raw
-  representation := some { byteSize := 0, decode := fun _ => none }
+  storage := some (.fixed { byteSize := 0, decode := fun _ => none })
 
 example : @RustModel.realizableRepresentation Empty emptySource := by
   intro raw
@@ -109,7 +109,7 @@ example : ¬ @RustModel.completeRepresentation Empty emptySource := by
 @[reducible] def boolDestination : RustModel Bool where
   Model := Bool
   decode := some
-  representation := some boolDecoder
+  storage := some (.fixed boolDecoder)
 
 theorem rejects_invalid_bool :
     (ambiguousSource.withChoice (fun _ => [.init 2])).transmuteCopyResult boolDestination () =
@@ -129,7 +129,7 @@ example : ¬ WP.spec
 @[reducible] def rejectsModelDestination : RustModel Rust.Bytes.Byte where
   Model := Unit
   decode := fun _ => none
-  representation := some byteDecoder
+  storage := some (.fixed byteDecoder)
 
 example :
     (ambiguousSource.withChoice (fun _ => [.init 0])).transmuteCopyResult rejectsModelDestination () =
diff --git a/verification/aeneas/tests/zeroed_audit_controls.py b/verification/aeneas/tests/zeroed_audit_controls.py
index f0d1c9ab9b..be4c4004fe 100644
--- a/verification/aeneas/tests/zeroed_audit_controls.py
+++ b/verification/aeneas/tests/zeroed_audit_controls.py
@@ -149,7 +149,7 @@ def restore_build(label):
         after = '''  core.mem.zeroed Self (model := {
     Model := AeneasSpecs.ModelOf Self,
     decode := fun _ => none,
-    representation := (inferInstance : AeneasSpecs.RustModel Self).representation })
+    storage := (inferInstance : AeneasSpecs.RustModel Self).storage })
 '''
         if text.count(before) != 1:
             raise ValueError('Zeroed native default control boundary changed')