diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md
index 130b078e75..db9c129733 100644
--- a/verification/aeneas/LOWERING_AUDIT.md
+++ b/verification/aeneas/LOWERING_AUDIT.md
@@ -8,7 +8,9 @@ the translation preserves the observations needed by that claim.
 
 The current integration proves conditional functional contracts under the
 correspondence premises in [SEMANTICS.md](SEMANTICS.md). It does not yet implement
-an abstract storage model or establish general Rust UB-freedom.
+a runtime storage semantics or establish general Rust UB-freedom.
+The pure byte representation model described below supplies initialization laws;
+it does not add storage events to extracted executions.
 [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) describes the implemented admission
 checks on the preserved pre-transformation snapshot and final LLBC, as well as
 the additional requirements for future storage and handler models. Those checks
@@ -117,6 +119,48 @@ numerical propositions are false. Conversely, they apply inside annotated
 functions too: finding every annotation does not establish that every relevant
 operation in its dependency closure was faithfully modeled.
 
+## Pure byte representations and the array law
+
+[`Rust.Storage`](../../anneal/lean/Rust/Storage.lean) now 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 this law when a
+physical decoder is available and is `False` otherwise. It does not use the
+library's mathematical decoder to restrict the byte lists under consideration.
+
+The array theorem partitions an accepted representation into contiguous element
+chunks and proves initialization from the element law. Its proof consumes the
+whole byte list, including an empty final remainder, for every count. Counting
+elements rather than advancing by a positive byte width also covers empty
+arrays and zero-sized elements.
+
+The Rust interpretation remains an explicit correspondence premise: each
+physical decoder's width and admission domain must cover the language-valid
+representations of its Rust type. `BitDecoder` does not encode or prove that
+premise. A decoder which rejects everything satisfies the initialization law
+vacuously, so that law alone cannot justify its use as a Rust representation
+model. The current primitive decoders and their array composition must be
+reviewed against the [Rust Reference layout](https://doc.rust-lang.org/reference/type-layout.html#array-layout)
+and [validity rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#invalid-values),
+as explained in [README.md](README.md#array-intobytes-initialization-law).
+Array size and element offsets exclude padding outside complete element chunks;
+padding inside a chunk is covered only by the element's law.
+
+A nameless `invariant_proof` fence on the ordinary array impl selects that
+exact compiler owner, independently of any caller harness. Both AST stages must
+retain its original type, usize length, and element dictionary parameters.
+The checked ordinary Lean theorem covers that complete native dictionary
+application under the element's law and model correspondence premises; the
+kernel witness and independent telescope audit reject specialization or added
+assumptions. This still relies on the reviewed correspondence from the Rust
+impl header to its native dictionary, not merely on a proof name.
+
+These definitions do not make the existing lowering retain byte storage events,
+initialization changes, or pointer provenance. They prove the modeled array
+`IntoBytes` trait law under the representation premises, not the runtime
+`as_bytes` implementation or general Rust UB-freedom. The typed-transfer and
+value-production boundaries above still apply.
+
 ## Complete LLBC operation inventory
 
 “Logical” below means the value-and-borrow interpretation. It does not mean
diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index a6901bc147..7974ad2e32 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -597,6 +597,50 @@ fence is the reserved CI-checked convention. Near-miss guard detection and the
 independent policy protect that convention without treating all mathematical
 prose as annotations.
 
+## Array `IntoBytes` initialization law
+
+The `IntoBytes` fence in [`lib.rs`](../../zerocopy/src/lib.rs) requires every
+accepted physical representation byte to be initialized. A byte in
+[`Rust.Storage`](../../anneal/lean/Rust/Storage.lean) is either initialized with
+an eight-bit value or uninitialized. Each physical decoder has a fixed width;
+a successful run must consume exactly that width. The law covers the entire
+accepted byte list, including any padding within an element representation.
+
+This physical decoder is separate from `RustModel.decode`, which interprets a
+typed value for library contracts. `RustModel.initializedRepresentation`
+quantifies over every successful physical decoding, even when the library
+model rejects that value. A missing physical decoder makes the law `False`.
+The current physical models cover `bool`, `u8`, `()`, and arrays recursively
+built from them; other mathematical models do not acquire a byte law by default.
+
+`arrayDecoder_initialized` proves that arrays inherit this law from their
+element decoder for every element count. The decoder splits the representation
+into consecutive chunks of the element width and requires an empty final
+remainder. An empty array accepts only an empty byte list. Zero-sized elements
+use empty chunks, so positive counts of `()` also have no representation bytes.
+The concrete checks in
+[`trait_checks.rs`](../../zerocopy/src/trait_checks.rs) exercise primitive,
+empty, zero-sized, and nested arrays; the extracted generic implementation law
+supplies the result for arbitrary counts under the element's law.
+
+Applying the theorem to Rust requires a correspondence premise for the physical
+decoder. Its width must equal Rust's size, and it must admit every language-valid
+representation. The [Rust Reference array layout rules](https://doc.rust-lang.org/reference/type-layout.html#array-layout)
+give size `N * size_of::<T>()`, alignment equal to `T`'s alignment, and element
+`k` at byte offset `k * size_of::<T>()`. These rules leave no padding between
+complete element representations; padding already included in `size_of::<T>()`
+still needs the element's initialization law. The [validity rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#invalid-values)
+require valid array elements, restrict `bool` to zero and one, and require
+initialized integers. The primitive layouts give `bool` and `u8` one byte and
+`()` zero bytes. These language facts justify the current decoder choices;
+Lean checks the initialization and array composition laws within that model.
+
+This proof establishes the array trait law under those correspondence premises.
+The pure representation model does not track runtime storage, typed transfers,
+or pointer provenance. `IntoBytes::as_bytes` retains its Rust safety argument;
+its pointer implementation is not proved by this array law. See
+[LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the remaining lowering boundaries.
+
 ## Native Lean proofs and independent checks
 
 `Specs.lean` is generated from the Rust comments in a fixed context containing
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index 7b5101b074..6b3f6d2cfc 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -707,6 +707,90 @@ def trait_checks.forwarded_byte_codec (byte : Std.U8) : Result Std.U8 := do
     (trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec
     trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec) byte
 
+/-- [zerocopy::trait_checks::require_into_bytes]:
+    Source: 'src/trait_checks.rs', lines 77:0-77:47 -/
+def trait_checks.require_into_bytes
+  {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do
+  ok ()
+
+/-- [zerocopy::impls::_#23::{impl zerocopy::IntoBytes for [T; N]}::only_derive_is_allowed_to_implement_this_trait]:
+    Source: 'src/util/macros.rs', lines 165:8-165:62
+    Visibility: public -/
+def
+  Array.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+  {T : Type} (N : Std.Usize) (IntoBytesInst : IntoBytes T) : Result Unit := do
+  ok ()
+
+/-- Trait implementation: [zerocopy::impls::_#23::{impl zerocopy::IntoBytes for [T; N]}]
+    Source: 'src/util/macros.rs', lines 132:8-134:9 -/
+@[reducible]
+def Array.Insts.ZerocopyIntoBytes {T : Type} (N : Std.Usize) (IntoBytesInst :
+  IntoBytes T) : IntoBytes (Array T N) := {
+  only_derive_is_allowed_to_implement_this_trait :=
+    Array.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+    N IntoBytesInst
+}
+
+/-- [zerocopy::impls::_::{impl zerocopy::IntoBytes for ()}::only_derive_is_allowed_to_implement_this_trait]:
+    Source: 'src/util/macros.rs', lines 165:8-165:62
+    Visibility: public -/
+def
+  Tuple.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+  : Result Unit := do
+  ok ()
+
+/-- Trait implementation: [zerocopy::impls::_::{impl zerocopy::IntoBytes for ()}]
+    Source: 'src/util/macros.rs', lines 30:8-32:9 -/
+@[reducible]
+def Tuple.Insts.ZerocopyIntoBytes : IntoBytes Unit := {
+  only_derive_is_allowed_to_implement_this_trait :=
+    Tuple.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+}
+
+/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u8}::only_derive_is_allowed_to_implement_this_trait]:
+    Source: 'src/util/macros.rs', lines 165:8-165:62
+    Visibility: public -/
+def U8.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+  : Result Unit := do
+  ok ()
+
+/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u8}]
+    Source: 'src/util/macros.rs', lines 30:8-32:9 -/
+@[reducible]
+def U8.Insts.ZerocopyIntoBytes : IntoBytes Std.U8 := {
+  only_derive_is_allowed_to_implement_this_trait :=
+    U8.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+}
+
+/-- [zerocopy::impls::_#2::{impl zerocopy::IntoBytes for bool}::only_derive_is_allowed_to_implement_this_trait]:
+    Source: 'src/util/macros.rs', lines 165:8-165:62
+    Visibility: public -/
+def Bool.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+  : Result Unit := do
+  ok ()
+
+/-- Trait implementation: [zerocopy::impls::_#2::{impl zerocopy::IntoBytes for bool}]
+    Source: 'src/util/macros.rs', lines 30:8-32:9 -/
+@[reducible]
+def Bool.Insts.ZerocopyIntoBytes : IntoBytes Bool := {
+  only_derive_is_allowed_to_implement_this_trait :=
+    Bool.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+}
+
+/-- [zerocopy::trait_checks::check_array_into_bytes]:
+    Source: 'src/trait_checks.rs', lines 92:0-98:1 -/
+def trait_checks.check_array_into_bytes : Result Unit := do
+  trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize
+    Bool.Insts.ZerocopyIntoBytes)
+  trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize
+    U8.Insts.ZerocopyIntoBytes)
+  trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 4#usize
+    Tuple.Insts.ZerocopyIntoBytes)
+  trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 0#usize
+    Bool.Insts.ZerocopyIntoBytes)
+  trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize
+    (Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes))
+
 /-- [zerocopy::util::padding_needed_for]:
     Source: 'src/util/mod.rs', lines 163:0-223:1 -/
 def util.padding_needed_for
diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean
index ea487bd212..464a829fb8 100644
--- a/verification/aeneas/golden/Types.lean
+++ b/verification/aeneas/golden/Types.lean
@@ -99,6 +99,12 @@ structure byteorder.U32 (O : Type) where
   _0 : Array Std.U8 4#usize
   _1 : core.marker.PhantomData O
 
+/-- Trait declaration: [zerocopy::IntoBytes]
+    Source: 'src/lib.rs', lines 5941:0-6446:1
+    Visibility: public -/
+structure IntoBytes (Self : Type) where
+  only_derive_is_allowed_to_implement_this_trait : Result Unit
+
 /-- Trait declaration: [zerocopy::trait_checks::ByteCodec]
     Source: 'src/trait_checks.rs', lines 26:0-29:1 -/
 structure trait_checks.ByteCodec (Self : Type) where
diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py
index c335d9c140..06776f48bd 100644
--- a/verification/aeneas/inline.py
+++ b/verification/aeneas/inline.py
@@ -1025,6 +1025,15 @@ def save_bindings(root, annotations, work, development=False):
                           'file': source['file'], 'syntax': source['syntax'],
                           'open_line': source['open_line'], 'end_line': source['end_line'], 'end_col': source['end_col']}
     physical_plans = {}
+    if (not development and (work / 'zerocopy.llbc').is_file()
+            and (work / 'zerocopy.before.ullbc').is_file()):
+        import physical_models
+        final = json.loads((work / 'zerocopy.llbc').read_text())['translated']
+        before = json.loads((work / 'zerocopy.before.ullbc').read_text())['translated']
+        physical_plans = physical_models.validate_physical_wrapper_plans(final, before)
+        for rust, entry in bindings.items():
+            if rust in physical_plans:
+                entry['physical_model'] = physical_plans[rust]
     type_image = list(native_omissions)
     classes = getattr(annotations, 'type_classes', None) if not development else None
     if not development and types.exists() and classes is None:
diff --git a/verification/aeneas/lean/DeriveModels.lean b/verification/aeneas/lean/DeriveModels.lean
index 1008dca069..d245ad4202 100644
--- a/verification/aeneas/lean/DeriveModels.lean
+++ b/verification/aeneas/lean/DeriveModels.lean
@@ -105,10 +105,17 @@ meta partial def boundModelProvider (raw : Expr) (params dicts : Array Expr) : M
     mkAppOptM n (xs.map some)
   if head.isConstOf ``UScalar then return ← app ``modelUScalar args
   if head.isConstOf ``IScalar then return ← app ``modelIScalar args
+  if head.isConstOf ``Char then return mkConst ``modelChar
   -- PhantomData has no stored child value: select its fixed empty provider
   -- without demanding a model for the type named by its phantom parameter.
   if head.isConstOf ``Zerocopy.core.marker.PhantomData then
     return ← app ``modelPhantomData args
+  for (carrier, provider) in #[
+      (``core.mem.manually_drop.ManuallyDrop, ``modelManuallyDrop),
+      (``core.cell.Cell, ``modelCell), (``core.cell.UnsafeCell, ``modelUnsafeCell)] do
+    if head.isConstOf carrier then
+      let child ← boundModelProvider args[0]! params dicts
+      return ← app provider (args ++ #[child])
   if head.isConstOf ``Bool then return mkConst ``modelBool
   if head.isConstOf ``Nat then return mkConst ``modelNat
   if head.isConstOf ``Int then return mkConst ``modelInt
@@ -121,6 +128,15 @@ meta partial def boundModelProvider (raw : Expr) (params dicts : Array Expr) : M
     return ← app (if head.isConstOf ``Prod then ``modelProd else ``modelRustResult)
       (args ++ #[ma, mb])
   if head.isConstOf ``Option || head.isConstOf ``List || head.isConstOf ``Slice then
+    if head.isConstOf ``Option then
+      let child ← whnf args[0]!
+      if child.getAppFn.isConstOf ``core.num.nonzero.NonZero then
+        let fields := child.getAppArgs
+        let word ← whnf fields[0]!
+        if word.getAppFn.isConstOf ``UScalar then
+          return ← app ``modelOptionNonZeroUScalar #[word.appArg!, fields[1]!]
+        if word.getAppFn.isConstOf ``IScalar then
+          return ← app ``modelOptionNonZeroIScalar #[word.appArg!, fields[1]!]
     let ma ← boundModelProvider args[0]! params dicts
     let provider := if head.isConstOf ``Option then ``modelOption
       else if head.isConstOf ``List then ``modelList else ``modelSlice
@@ -361,7 +377,8 @@ that wrapper's decomposition, and finally register the complete RustModel.
 An absent local decoder is structural identity. An infallible authored decoder
 returns a model; a fallible one returns Option model and can restrict admission. -/
 private meta def deriveProvider (raw : Name) (count : Nat)
-    (localDecoder : Option (Name × Syntax × Bool)) : TermElabM Unit := do
+    (localDecoder : Option (Name × Syntax × Bool))
+    (physicalPayload : Option Nat := none) : TermElabM Unit := do
   let info ← nominal raw count
   let some b := (modelExtension.getState (← getEnv)).find? raw
     | throwError "Missing Fields/model shape for {raw}"
@@ -448,8 +465,41 @@ 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]
+      | some payload => do
+        -- LLBC validation authorizes only named builtin storage wrappers. Lean
+        -- independently checks that reconstruction uses the actual raw fields.
+        let some structureInfo := getStructureInfo? (← getEnv) raw
+          | throwError "Physical wrappers must be structures: {raw}"
+        let supported := #[`Zerocopy.wrappers.Unalign,
+          `Zerocopy.wrappers.read_only_def.ReadOnly]
+        let byteorder := raw.getPrefix == `Zerocopy.byteorder &&
+          #[`U16, `U32, `U64, `U128, `Usize, `I16, `I32, `I64, `I128,
+            `Isize, `F32, `F64].contains (Name.mkSimple raw.getString!)
+        unless supported.contains raw || byteorder do
+          throwError "Unsupported physical wrapper owner: {raw}"
+        unless payload == 0 && structureInfo.fieldNames.size == (if byteorder then 2 else 1) do
+          throwError "Physical wrapper field shape changed: {raw}"
+        let ctor := mkAppN (mkConst info.ctors.head! levels) params
+        forallTelescope (← inferType ctor) fun fields _ => do
+          let fieldTy ← inferType fields[payload]!
+          let child ← boundModelProvider fieldTy params dicts
+          let wrap ← withLocalDeclD `payload fieldTy fun value => do
+            let mut values := #[]
+            for i in [:fields.size] do
+              if i == payload then values := values.push value
+              else
+                let ty ← whnf (← inferType fields[i]!)
+                unless ty.getAppFn.isConstOf ``Zerocopy.core.marker.PhantomData do
+                  throwError "Only PhantomData may accompany a physical payload: {raw}"
+                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]
     let provider ← mkAppOptM ``RustModel.mk #[some rawTy, some modelTy,
-      some (mkAppN (mkConst b.decoder levels) all)]
+      some (mkAppN (mkConst b.decoder levels) all), some representation]
     addDefinition b.provider info.levelParams (← mkLambdaFVars all provider)
   setReducibilityStatus b.provider .reducible
   addInstance b.provider .global 1000
@@ -468,6 +518,23 @@ elab "derive_rust_model " rawId:ident " with " count:num " type " "parameters"
   deriveProvider (← realizeGlobalConstNoOverloadWithInfo rawId) count.getNat
     (some (self.getId, body, true))
 
+elab "derive_rust_model " rawId:ident " with " count:num " type " "parameters"
+    " with_physical " payloadIndex:num : command => Command.liftTermElabM do
+  deriveProvider (← realizeGlobalConstNoOverloadWithInfo rawId) count.getNat none
+    (some payloadIndex.getNat)
+
+elab "derive_rust_model " rawId:ident " with " count:num " type " "parameters"
+    " with_physical " payloadIndex:num " decode " self:ident " => " body:term : command =>
+  Command.liftTermElabM do
+    deriveProvider (← realizeGlobalConstNoOverloadWithInfo rawId) count.getNat
+      (some (self.getId, body, false)) (some payloadIndex.getNat)
+
+elab "derive_rust_model " rawId:ident " with " count:num " type " "parameters"
+    " with_physical " payloadIndex:num " decode? " self:ident " => " body:term : command =>
+  Command.liftTermElabM do
+    deriveProvider (← realizeGlobalConstNoOverloadWithInfo rawId) count.getNat
+      (some (self.getId, body, true)) (some payloadIndex.getNat)
+
 /-- Audit the elaborated provider against its registered raw owner, mathematical
 type, full decoder, and generic count. Definitional equality unfolds actual
 expressions, so matching names alone cannot attach a provider to a wrong type. -/
diff --git a/verification/aeneas/lean/EmptyConstructionTests.lean b/verification/aeneas/lean/EmptyConstructionTests.lean
new file mode 100644
index 0000000000..763c9fed3c
--- /dev/null
+++ b/verification/aeneas/lean/EmptyConstructionTests.lean
@@ -0,0 +1,104 @@
+/- 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 ModelPrelude
+import all RustModel
+import all ModelPrelude
+@[expose] public section
+
+/-!
+Empty storage supplies no constructor permission or library invariant. These
+model controls distinguish a supplied Lean inhabitant, an explicit physical
+representation decoder, and admission by the retained mathematical provider.
+They execute no invalid Rust construction.
+-/
+open Aeneas Aeneas.Std AeneasSpecs Rust.Storage
+namespace EmptyConstructionTests
+
+-- An uninhabited raw carrier needs no fabricated inhabitant to fail closed.
+@[reducible] def modelEmpty : RustModel Empty where
+  Model := Unit
+  decode raw := nomatch raw
+
+example : ¬ @RustModel.initializedRepresentation Empty modelEmpty := by
+  simp [RustModel.initializedRepresentation, RustModel.representation]
+
+example : modelEmpty.decodeBitsResult [] = .fail .undef := rfl
+example : modelEmpty.decodeBytesResult [] = .fail .undef := by
+  simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
+    RustModel.decodeResult, RustModel.representation, RustModel.decode]
+example : ¬ WP.spec (modelEmpty.decodeBytesResult []) (fun _ => True) := by
+  simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
+    RustModel.decodeResult, RustModel.representation]
+example : ¬ WP.dspec (modelEmpty.decodeBytesResult []) (fun _ => True) := by
+  simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
+    RustModel.decodeResult, RustModel.representation]
+
+inductive StateToken where
+  | mk
+  deriving Inhabited
+
+-- Lean's Inhabited instance alone does not install physical semantics. This
+-- provider even accepts its raw value mathematically, but byte construction
+-- still has no physical representation decoder.
+@[reducible] def inhabitedOnly : RustModel StateToken where
+  Model := Unit
+  decode _ := some ()
+
+example : ¬ @RustModel.initializedRepresentation StateToken inhabitedOnly := by
+  simp [RustModel.initializedRepresentation, RustModel.representation]
+
+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]
+
+-- Model an external admission condition explicitly. The physical decoder may
+-- supply the unit-like raw constructor while the full provider still rejects
+-- that value when the required external state is absent.
+@[reducible] def stateModel (masked : Bool) : RustModel StateToken where
+  Model := Unit
+  decode _ := if masked then some () else none
+  representation := some (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,
+    emptyDecoder, BitDecoder.run]
+example : (stateModel false).decodeBytesResult [] = .fail .undef := by
+  simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
+    RustModel.decodeResult, RustModel.representation, 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,
+    emptyDecoder, BitDecoder.run]
+example : ¬ WP.dspec ((stateModel false).decodeBytesResult []) (fun _ => True) := by
+  simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
+    RustModel.decodeResult, RustModel.representation, RustModel.decode,
+    emptyDecoder, BitDecoder.run]
+
+-- Both states satisfy the physical initialization law. That law cannot prove
+-- admission by the library provider, let alone a Rust constructor precondition.
+example (masked : Bool) :
+    @RustModel.initializedRepresentation StateToken (stateModel masked) :=
+  emptyDecoder_initialized StateToken.mk
+
+-- PhantomData stores no T. Its explicit raw constructor and empty decoder
+-- therefore need neither a T value nor a RustModel T, even for uninhabited T.
+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,
+    emptyDecoder, BitDecoder.run]
+
+end EmptyConstructionTests
diff --git a/verification/aeneas/lean/IndexedStorageTests.lean b/verification/aeneas/lean/IndexedStorageTests.lean
new file mode 100644
index 0000000000..7f9009f723
--- /dev/null
+++ b/verification/aeneas/lean/IndexedStorageTests.lean
@@ -0,0 +1,114 @@
+/- 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
+import all RustModel
+
+/-!
+These model tests use explicit metadata and numeric byte representations.
+They prove decoder behavior, not a Rust ABI identity, pointer reconstruction,
+or the full contract of any unsafe trait or byte-cast implementation.
+-/
+open Aeneas Aeneas.Std AeneasSpecs Rust.Storage
+namespace IndexedStorageTests
+
+example : (modelBool).decodeStorageResult boolDecoder.asStorageDecoder () [AMByte.init 1] = .ok true := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  rfl
+example : (modelBool).decodeStorageResult boolDecoder.asStorageDecoder () [AMByte.init 2] = .fail .undef := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  rfl
+example : (modelBool).decodeStorageResult boolDecoder.asStorageDecoder () [AMByte.uninit] = .fail .undef := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  rfl
+example : (modelBool).decodeStorageResult boolDecoder.asStorageDecoder () [] = .fail .undef := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  rfl
+
+-- The native slice adapter preserves every explicit count and the array domain.
+example (count : Usize) (bytes : List AMByte)
+    (values : { values : List Bool // values.length = count.val })
+    (accepted : (arrayDecoder boolDecoder count.val).run bytes = some values) :
+    RustModel.decodeStorageBitsResult (RustModel.sliceStorageDecoder boolDecoder) count bytes =
+      .ok (Slice.from values.val (by rw [values.property]; scalar_tac)) := by
+  rw [RustModel.decodeStorageBitsResult, RustModel.sliceStorageDecoder_run, accepted]
+  rfl
+example : (RustModel.sliceStorageDecoder boolDecoder).Initialized :=
+  RustModel.sliceStorageDecoder_initialized _ boolDecoder_initialized
+
+-- Equal zero-byte widths support every usize count without guessing that count.
+example (count : Usize) : ∃ raw,
+    RustModel.decodeStorageBitsResult (RustModel.sliceStorageDecoder unitDecoder) count [] = .ok raw := by
+  obtain ⟨values, accepted⟩ := arrayDecoder_complete unitDecoder
+    (fun bytes width _ => ⟨(), emptyDecoder_complete () bytes width⟩) count.val []
+    (by simp [unitDecoder, emptyDecoder]) initialized_nil
+  rw [RustModel.decodeStorageBitsResult, RustModel.sliceStorageDecoder_run, accepted]
+  exact ⟨_, rfl⟩
+example (count : Usize) (bytes : List AMByte) (raw : Slice Unit)
+    (accepted : (RustModel.sliceStorageDecoder unitDecoder).run count bytes = some raw) :
+    raw.len = count := StorageDecoder.run_metadata _ _ _ _ accepted
+
+-- A mathematical decoder cannot conceal an invalid language representation.
+@[reducible] def rejectsAll : RustModel Unit where
+  Model := Unit
+  decode _ := none
+
+example : rejectsAll.decodeStorageResult unitDecoder.asStorageDecoder () [] = .fail .undef := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  rfl
+example : RustModel.decodeStorageBitsResult unitDecoder.asStorageDecoder () [] = .ok () := rfl
+example : unitDecoder.asStorageDecoder.Initialized :=
+  BitDecoder.asStorageDecoder_initialized _ unitDecoder_initialized
+example : ¬ unitDecoder.asStorageDecoder.CompleteWith rejectsAll.decode := by
+  intro complete
+  obtain ⟨value, accepted⟩ := complete () [] rfl initialized_nil
+  simp [StorageDecoder.runWith] at accepted
+
+-- An uninitialized representation remains forbidden for the initialization law,
+-- even if the mathematical decoder rejects every returned raw value.
+def acceptsUninit : StorageDecoder Unit Unit where
+  byteSize _ := 1
+  metadata _ := ()
+  decode _ _ := some ()
+
+example : rejectsAll.decodeStorageResult acceptsUninit () [AMByte.uninit] = .fail .undef := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  rfl
+example : ¬ acceptsUninit.Initialized := by
+  intro initialized
+  have impossible := initialized () [AMByte.uninit] () rfl
+  simp [Initialized] at impossible
+
+-- The checked metadata observation applies even to zero-width representations.
+def wrongCount : StorageDecoder Nat Nat where
+  byteSize _ := 0
+  metadata := id
+  decode _ _ := some 0
+
+example : RustModel.decodeStorageBitsResult wrongCount 3 [] = .fail .undef := rfl
+example : modelNat.decodeStorageResult wrongCount 3 [] = .fail .undef := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  rfl
+
+-- A vacuous postcondition cannot admit language-invalid byte construction.
+example : ¬ WP.spec
+    (modelBool.decodeStorageResult boolDecoder.asStorageDecoder () [AMByte.init 2])
+    (fun _ => True) := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  change ¬ WP.spec (.fail .undef : Result Bool) (fun _ => True)
+  simp
+example : ¬ WP.dspec (modelNat.decodeStorageResult wrongCount 3 []) (fun _ => True) := by
+  rw [RustModel.decodeStorageResult_as_runWith]
+  change ¬ WP.dspec (.fail .undef : Result Nat) (fun _ => True)
+  simp
+
+#print axioms RustModel.decodeStorageResult_as_runWith
+#print axioms RustModel.decodeStorageResult_eq_ok_iff
+#print axioms RustModel.sliceStorageDecoder_initialized
+
+end IndexedStorageTests
diff --git a/verification/aeneas/lean/ModelLemmas.lean b/verification/aeneas/lean/ModelLemmas.lean
index e65075c91b..4797183db4 100644
--- a/verification/aeneas/lean/ModelLemmas.lean
+++ b/verification/aeneas/lean/ModelLemmas.lean
@@ -8,6 +8,7 @@ those terms. -/
 
 module
 public import ModelPrelude
+public import ContractSimps
 @[expose] public section
 
 /-!
@@ -48,6 +49,27 @@ theorem admitted_dite {α : Type} (P : Prop) [Decidable P] (value : P → α) :
     isValid raw ↔ ∀ x ∈ raw, isValid x := by
   cases raw <;> simp [isValid, RustModel.decode, modelOption, Option.map_eq_some_iff]
 
+-- Niche-aware providers change physical storage, while retaining ordinary
+-- Option admission. State that observation explicitly so proofs need not
+-- unfold the physical decoder to recover their mathematical input domain.
+@[simp, contract_simps] theorem option_nonzero_unsigned_decode_eq (ty : UScalarTy) (Inner : Type)
+    (raw : Option (core.num.nonzero.NonZero (UScalar ty) Inner)) :
+    RustModel.decode raw = (modelOption (ma := modelNonZeroUScalar ty Inner)).decode raw := rfl
+
+@[simp, contract_simps] theorem option_nonzero_signed_decode_eq (ty : IScalarTy) (Inner : Type)
+    (raw : Option (core.num.nonzero.NonZero (IScalar ty) Inner)) :
+    RustModel.decode raw = (modelOption (ma := modelNonZeroIScalar ty Inner)).decode raw := rfl
+
+@[simp, contract_simps] theorem option_nonzero_unsigned_valid_iff (ty : UScalarTy) (Inner : Type)
+    (raw : Option (core.num.nonzero.NonZero (UScalar ty) Inner)) :
+    isValid raw ↔ ∀ x ∈ raw, isValid x := by
+  exact @option_valid_iff _ (modelNonZeroUScalar ty Inner) raw
+
+@[simp, contract_simps] theorem option_nonzero_signed_valid_iff (ty : IScalarTy) (Inner : Type)
+    (raw : Option (core.num.nonzero.NonZero (IScalar ty) Inner)) :
+    isValid raw ↔ ∀ x ∈ raw, isValid x := by
+  exact @option_valid_iff _ (modelNonZeroIScalar ty Inner) raw
+
 @[simp] theorem prod_valid_iff {α β : Type} [RustModel α] [RustModel β]
     (raw : α × β) : isValid raw ↔ isValid raw.1 ∧ isValid raw.2 := by
   rcases raw with ⟨a, b⟩
diff --git a/verification/aeneas/lean/ModelPrelude.lean b/verification/aeneas/lean/ModelPrelude.lean
index 7d2f64655c..b8c02429de 100644
--- a/verification/aeneas/lean/ModelPrelude.lean
+++ b/verification/aeneas/lean/ModelPrelude.lean
@@ -8,6 +8,7 @@ those terms. -/
 
 module
 public import RustModel
+public import RustAeneas.Storage
 public import Zerocopy.Types
 @[expose] public section
 
@@ -30,7 +31,8 @@ namespace AeneasSpecs
 -- variance, drop checking, or pointer provenance.
 @[reducible] instance modelPhantomData (T : Type) :
     RustModel (Zerocopy.core.marker.PhantomData T) :=
-  { Model := Unit, «decode» := fun _ => some () }
+  { Model := Unit, «decode» := fun _ => some (),
+    representation := some (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) :
@@ -39,6 +41,58 @@ 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.
+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
+    | 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
+
+-- These providers interpret stored values only. They do not model mutation,
+-- aliasing, synchronization, or destruction of the standard-library wrappers.
+@[reducible] instance modelManuallyDrop (T : Type) [ma : RustModel T] :
+    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
+
+@[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
+
+@[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
+
+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
+
+theorem initializedCell (T : Type) [ma : RustModel T]
+    (child : RustModel.initializedRepresentation T) :
+    RustModel.initializedRepresentation (core.cell.Cell T) :=
+  initializedWrapperRepresentation core.cell.Cell.mk child
+
+theorem initializedUnsafeCell (T : Type) [ma : RustModel T]
+    (child : RustModel.initializedRepresentation T) :
+    RustModel.initializedRepresentation (core.cell.UnsafeCell T) :=
+  initializedWrapperRepresentation core.cell.UnsafeCell.mk child
+
 -- The bounds are proofs stored beside the value. They contribute constraints
 -- to the mathematical type without another runtime field or admission test.
 structure UnsignedWord (ty : UScalarTy) where
@@ -82,20 +136,103 @@ def signedWord (x : IScalar ty) : SignedWord ty :=
   ⟨x.val, by simpa only [IScalar.min] using x.hmin,
     by have := x.hmax; simp only [IScalar.max]; omega⟩
 
-@[reducible] instance modelUScalar (ty : UScalarTy) : RustModel (UScalar ty) :=
-  ⟨UnsignedWord ty, fun x => some (unsignedWord x)⟩
-@[reducible] instance modelIScalar (ty : IScalarTy) : RustModel (IScalar ty) :=
-  { Model := SignedWord ty, «decode» := fun x => some (signedWord x) }
+/-- Admission currently checks a little-endian 64-bit extraction target.
+The shared initialization theorems are independent of this byte order. -/
+def uScalarBitDecoder (ty : UScalarTy) : Rust.Storage.BitDecoder (UScalar ty) :=
+  Rust.Storage.AeneasAdapter.unsignedDecoder ty .little
+
+def iScalarBitDecoder (ty : IScalarTy) : Rust.Storage.BitDecoder (IScalar ty) :=
+  Rust.Storage.AeneasAdapter.signedDecoder ty .little
+
+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)
+@[reducible] instance modelIScalar (ty : IScalarTy) : RustModel (IScalar ty) where
+  Model := SignedWord ty
+  decode x := some (signedWord x)
+  representation := some (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
+turning an uninitialized representation into a character. -/
+def charBitDecoder : Rust.Storage.BitDecoder Char :=
+  (Rust.Storage.integerDecoder 4 .little).filterMap fun word =>
+    let value := UInt32.ofNat word.toNat
+    if h : isValidChar value then some ⟨value, h⟩ else none
+
+@[reducible] instance modelChar : RustModel Char where
+  Model := Char
+  decode x := some x
+  representation := some charBitDecoder
+
+def nonzeroUScalarBitDecoder (ty : UScalarTy) (Inner : Type) :
+    Rust.Storage.BitDecoder (core.num.nonzero.NonZero (UScalar ty) Inner) :=
+  (uScalarBitDecoder ty).filterMap fun word =>
+    if word.val = 0 then none else some ⟨word⟩
+
+def nonzeroIScalarBitDecoder (ty : IScalarTy) (Inner : Type) :
+    Rust.Storage.BitDecoder (core.num.nonzero.NonZero (IScalar ty) Inner) :=
+  (iScalarBitDecoder ty).filterMap fun word =>
+    if word.val = 0 then none else some ⟨word⟩
 
 @[reducible] instance modelNonZeroUScalar (ty : UScalarTy) (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)
 
 @[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)
+
+-- Rust guarantees the zero niche for these particular standard-library
+-- wrappers. Map the full integer decoder: a zero is a successfully decoded
+-- Rust None, whereas an earlier byte failure remains a decoding failure.
+-- A generic Option<T> has no physical decoder inferred from its payload.
+@[reducible] instance (priority := 1001) modelOptionNonZeroUScalar
+    (ty : UScalarTy) (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⟩)
+
+@[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⟩)
+
+theorem initializedUScalar (ty : UScalarTy) :
+    RustModel.initializedRepresentation (UScalar ty) :=
+  Rust.Storage.AeneasAdapter.unsignedDecoder_initialized ty .little
+
+theorem initializedIScalar (ty : IScalarTy) :
+    RustModel.initializedRepresentation (IScalar ty) :=
+  Rust.Storage.AeneasAdapter.signedDecoder_initialized ty .little
+
+theorem initializedNonZeroUScalar (ty : UScalarTy) (Inner : Type) :
+    RustModel.initializedRepresentation (core.num.nonzero.NonZero (UScalar ty) Inner) :=
+  Rust.Storage.BitDecoder.filterMap_initialized _ _ (initializedUScalar ty)
+
+theorem initializedNonZeroIScalar (ty : IScalarTy) (Inner : Type) :
+    RustModel.initializedRepresentation (core.num.nonzero.NonZero (IScalar ty) Inner) :=
+  Rust.Storage.BitDecoder.filterMap_initialized _ _ (initializedIScalar ty)
+
+theorem initializedOptionNonZeroUScalar (ty : UScalarTy) (Inner : Type) :
+    RustModel.initializedRepresentation (Option (core.num.nonzero.NonZero (UScalar ty) Inner)) :=
+  Rust.Storage.BitDecoder.map_initialized _ _ (initializedUScalar ty)
+
+theorem initializedOptionNonZeroIScalar (ty : IScalarTy) (Inner : Type) :
+    RustModel.initializedRepresentation (Option (core.num.nonzero.NonZero (IScalar ty) Inner)) :=
+  Rust.Storage.BitDecoder.map_initialized _ _ (initializedIScalar ty)
 
 abbrev NonZeroUsizeValue := NonZeroUnsignedWord .Usize
 abbrev modelNonZeroUsize := modelNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner
diff --git a/verification/aeneas/lean/Obligations/TraitChecks.lean b/verification/aeneas/lean/Obligations/TraitChecks.lean
index 94deb09304..0261867c00 100644
--- a/verification/aeneas/lean/Obligations/TraitChecks.lean
+++ b/verification/aeneas/lean/Obligations/TraitChecks.lean
@@ -21,6 +21,28 @@ The contract families quantify an arbitrary outcome independently of any body.
 open Aeneas Aeneas.Std
 namespace Zerocopy.Obligations
 
+-- State initialization directly on accepted byte lists. This expectation
+-- independently fixes the physical decoder used by each concrete root case,
+-- rather than referring to the generated RustModel representation selection.
+def arrayBytesInitialized (element : Rust.Storage.BitDecoder Raw) (count : Usize) : Prop :=
+  ∀ bytes values,
+    ((Rust.Storage.arrayDecoder element count.val).map
+      (fun values => Aeneas.Std.Array.from values.val values.property)).run bytes = some values →
+      Rust.Storage.Initialized bytes
+
+def array_into_bytes_spec_contract (run : Result Unit) : Prop :=
+  run ⦃ _ =>
+    arrayBytesInitialized Rust.Storage.boolDecoder (3#usize) ∧
+    arrayBytesInitialized AeneasSpecs.u8BitDecoder (3#usize) ∧
+    arrayBytesInitialized Rust.Storage.unitDecoder (4#usize) ∧
+    arrayBytesInitialized Rust.Storage.boolDecoder (0#usize) ∧
+    arrayBytesInitialized ((Rust.Storage.arrayDecoder Rust.Storage.boolDecoder 2).map
+      (fun values => Aeneas.Std.Array.from (n := 2#usize) values.val values.property)) (3#usize) ⦄
+
+def array_into_bytes_spec : Prop :=
+  array_into_bytes_spec_contract trait_checks.check_array_into_bytes
+
+
 def byte_codec_roundtrip_spec_contract (C : Type) (dictionary : trait_checks.ByteCodec C)
     (byte : U8) (run : Result U8) : Prop :=
   TraitLaws.byte_roundtrip C dictionary → run ⦃ result => result = byte ⦄
diff --git a/verification/aeneas/lean/PhysicalModelTests.lean b/verification/aeneas/lean/PhysicalModelTests.lean
new file mode 100644
index 0000000000..8eae1607d5
--- /dev/null
+++ b/verification/aeneas/lean/PhysicalModelTests.lean
@@ -0,0 +1,113 @@
+/- 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 ModelPrelude
+import all RustModel
+import all ModelPrelude
+@[expose] public section
+
+/-!
+A physical decoder describes which abstract bytes can produce a Rust value.
+The library decoder may impose additional restrictions on that value, but those
+restrictions must not weaken IntoBytes: every language-valid representation
+must be initialized. These examples pin that separation and the forbidden
+outcome of an invalid byte-to-value construction.
+
+These are model tests, not executions of invalid Rust. In particular, they do
+not construct an invalid boolean or read uninitialized memory in Rust.
+-/
+open Aeneas Aeneas.Std AeneasSpecs Rust.Storage
+namespace PhysicalModelTests
+
+example : RustModel.initializedRepresentation Bool := boolDecoder_initialized
+example : RustModel.initializedRepresentation Unit := unitDecoder_initialized
+example : RustModel.initializedRepresentation U8 :=
+  initializedUScalar .U8
+
+-- One proof covers every supported width and signedness. It does not assume
+-- that an integer's alignment equals its byte size.
+example (ty : UScalarTy) : RustModel.initializedRepresentation (UScalar ty) :=
+  initializedUScalar ty
+example (ty : IScalarTy) : RustModel.initializedRepresentation (IScalar ty) :=
+  initializedIScalar ty
+
+example : (modelUScalar .U16).decodeBitsResult [AMByte.init 0x34, AMByte.init 0x12] =
+    .ok (0x1234#u16) := rfl
+example : (modelIScalar .I16).decodeBitsResult [AMByte.init 255, AMByte.init 255] =
+    .ok ((-1)#i16) := rfl
+example : (modelChar).decodeBitsResult [AMByte.init 65, AMByte.init 0,
+    AMByte.init 0, AMByte.init 0] = .ok 'A' := rfl
+example : (modelChar).decodeBitsResult [AMByte.init 0, AMByte.init 0xd8,
+    AMByte.init 0, AMByte.init 0] = .fail .undef := rfl
+
+-- Zero is not a NonZero value, but it is the valid None representation of
+-- Option<NonZero>. Failure to collect initialized bytes never becomes None.
+example : (modelNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).decodeBitsResult
+    [AMByte.init 0] = .fail .undef := rfl
+example : (modelOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).decodeBitsResult
+    [AMByte.init 0] = .ok none := rfl
+example : (modelOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).decodeBitsResult
+    [AMByte.uninit] = .fail .undef := rfl
+example : (modelOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner).decodeBitsResult
+    [AMByte.init 255] = .ok (some ⟨(-1)#i8⟩) := rfl
+
+-- Missing physical semantics cannot establish a trait law by vacuity.
+example : ¬ RustModel.initializedRepresentation Nat := by
+  simp [RustModel.initializedRepresentation, RustModel.representation]
+
+-- This intentionally bad physical decoder accepts an uninitialized byte.
+-- Rejecting all library values cannot turn it into an IntoBytes interpretation.
+def acceptsUninit : BitDecoder Nat where
+  byteSize := 1
+  decode _ := some 0
+
+@[reducible] def rejectsEverything : RustModel Nat where
+  Model := Unit
+  decode _ := none
+  representation := some acceptsUninit
+
+example : ¬ @RustModel.initializedRepresentation Nat rejectsEverything := by
+  intro law
+  have forbidden := law [AMByte.uninit] 0 rfl
+  simp [Initialized] at forbidden
+
+example : (modelBool).decodeBitsResult [AMByte.uninit] = .fail .undef := rfl
+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]
+example : (modelUScalar .U8).decodeBytesResult [AMByte.init 255] =
+    .ok (unsignedWord (255#u8)) := by
+  simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
+    RustModel.decodeResult, RustModel.representation, RustModel.decode,
+    uScalarBitDecoder, Rust.Storage.AeneasAdapter.unsignedDecoder,
+    BitDecoder.map, BitDecoder.run, integerDecoder, collectInitialized,
+    Rust.Bytes.decode, Rust.Bytes.decodeLE, UScalar.ofNatCore]
+
+-- Both correctness judgments reject forbidden construction, even when the
+-- 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]
+example : ¬ WP.dspec (modelBool.decodeBytesResult [AMByte.uninit]) (fun _ => True) := by
+  simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult,
+    RustModel.decodeResult, RustModel.representation, 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.
+example : RustModel.initializedRepresentation (Aeneas.Std.Array Bool (0#usize)) :=
+  RustModel.initialized_array _ _ boolDecoder_initialized
+example : RustModel.initializedRepresentation (Aeneas.Std.Array Unit (4#usize)) :=
+  RustModel.initialized_array _ _ unitDecoder_initialized
+example : RustModel.initializedRepresentation
+    (Aeneas.Std.Array (Aeneas.Std.Array Bool (2#usize)) (3#usize)) :=
+  RustModel.initialized_array _ _ (RustModel.initialized_array _ _ boolDecoder_initialized)
+
+end PhysicalModelTests
diff --git a/verification/aeneas/lean/Proofs/TraitChecks.lean b/verification/aeneas/lean/Proofs/TraitChecks.lean
index 76439dafd3..f2f2bb9085 100644
--- a/verification/aeneas/lean/Proofs/TraitChecks.lean
+++ b/verification/aeneas/lean/Proofs/TraitChecks.lean
@@ -19,6 +19,56 @@ proves a total codec, and forwarding preserves only the supplied codec's law.
 open Aeneas Aeneas.Std AeneasSpecs
 namespace Zerocopy.Proofs
 
+-- These primitive byte interpretations follow Rust's validity and layout
+-- rules. The array law below uses those interpretations, not the optional
+-- library decoder's (possibly smaller) admission domain.
+@[instance] theorem Bool.Insts.ZerocopyIntoBytes_law :
+    TraitLaws.into_bytes_initialized Bool Zerocopy.Bool.Insts.ZerocopyIntoBytes :=
+  ⟨Rust.Storage.boolDecoder_initialized⟩
+
+@[instance] theorem U8.Insts.ZerocopyIntoBytes_law :
+    TraitLaws.into_bytes_initialized U8 Zerocopy.U8.Insts.ZerocopyIntoBytes :=
+  ⟨initializedUScalar .U8⟩
+
+@[instance] theorem Tuple.Insts.ZerocopyIntoBytes_law :
+    TraitLaws.into_bytes_initialized Unit Zerocopy.Tuple.Insts.ZerocopyIntoBytes :=
+  ⟨Rust.Storage.unitDecoder_initialized⟩
+
+-- The original type, const length, and computational dictionary remain the
+-- native implementation's prefix. Only the element's provider and law are
+-- added. There is no assumption of the array's own law.
+@[instance] theorem Array.Insts.ZerocopyIntoBytes_law
+    {T : Type} (N : Usize) (dictionary : IntoBytes T)
+    [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
+    TraitLaws.into_bytes_initialized (Aeneas.Std.Array T N)
+      (Zerocopy.Array.Insts.ZerocopyIntoBytes N dictionary) :=
+  ⟨RustModel.initialized_array T N (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩
+
+-- Calling the real Rust helper selects the existing unsafe impls in Charon.
+-- The generic impl law proves all lengths; these concrete cases additionally
+-- check that the actual extraction and canonical model bindings compose.
+theorem array_into_bytes_spec : Specs.array_into_bytes_spec := by
+  simp only [Specs.array_into_bytes_spec, Zerocopy.trait_checks.check_array_into_bytes,
+    Zerocopy.trait_checks.require_into_bytes, bind_ok, WP.spec_ok]
+  refine ⟨(), rfl, ?_, ?_, ?_, ?_, ?_⟩
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)
+      _ inferInstance)
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.U8.Insts.ZerocopyIntoBytes)
+      _ inferInstance)
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Tuple.Insts.ZerocopyIntoBytes)
+      _ inferInstance)
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)
+      _ inferInstance)
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.Array.Insts.ZerocopyIntoBytes _
+        (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes))
+      _ inferInstance)
+
+
 @[instance] theorem trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec_law :
     TraitLaws.byte_roundtrip Zerocopy.trait_checks.XorCodec
       Zerocopy.trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec := by
diff --git a/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean b/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean
index 2c39ccd5c8..2bd4230751 100644
--- a/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean
+++ b/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean
@@ -22,6 +22,14 @@ substitute implementation. None of these adapters executes the function.
 open Aeneas Aeneas.Std AeneasSpecs
 namespace Zerocopy.Proofs
 
+@[contract_simps] theorem required_array_into_bytes (run : Result Unit)
+    (provided : Specs.array_into_bytes_spec_contract run) :
+    Obligations.array_into_bytes_spec_contract run := by
+  apply WP.spec_mono provided
+  rintro _ ⟨_, _, boolean, byte, unit, empty, nested⟩
+  exact ⟨boolean, byte, unit, empty, nested⟩
+
+
 @[contract_simps] theorem required_byte_codec_roundtrip (C : Type)
     (dictionary : trait_checks.ByteCodec C) (byte : U8) (run : Result U8)
     (provided : Specs.byte_codec_roundtrip_spec_contract C dictionary byte run) :
diff --git a/verification/aeneas/lean/RustModel.lean b/verification/aeneas/lean/RustModel.lean
index 28d35e942c..1aed812ae2 100644
--- a/verification/aeneas/lean/RustModel.lean
+++ b/verification/aeneas/lean/RustModel.lean
@@ -8,6 +8,7 @@ those terms. -/
 
 module
 public import Aeneas
+public import Rust.Storage
 public meta import Lean
 @[expose] public section
 
@@ -33,6 +34,10 @@ to the same raw value, so contracts retain the actual provider explicitly. -/
 class RustModel (Raw : Type u) where
   Model : Type u
   decode : Raw → Option Model
+  /-- 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
 
 -- The associated type is transparent so ordinary rewriting and coercions can
 -- identify a retained provider's Model with its named mathematical carrier.
@@ -49,6 +54,23 @@ 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. -/
+def RustModel.initializedRepresentation (Raw : Type u) [m : RustModel Raw] : Prop :=
+  match m.representation with
+  | none => False
+  | some decoder => decoder.Initialized
+
+/-- Constructing a typed value from bytes requires language-level decoding.
+The unsupported-model case also fails closed. No invalid Raw is produced. -/
+def RustModel.decodeBitsResult {Raw : Type u} (m : RustModel Raw)
+    (bytes : List Rust.Storage.AMByte) : Result Raw :=
+  match m.representation with
+  | none => .fail .undef
+  | some decoder => Result.ofOption (decoder.asStorageDecoder.run () bytes) .undef
+
 /-- Compose execution with the retained provider's mathematical decoder.
 An earlier execution failure or divergence is preserved. A rejected returned
 value becomes `undef`, marking an unadmitted value of this modeled computation;
@@ -59,6 +81,49 @@ def RustModel.decodeResult {Raw : Type u} (m : RustModel Raw)
   let raw ← run
   Result.ofOption (m.decode raw) .undef
 
+/-- Language-level decoding followed by the retained mathematical decoder.
+Failure at either stage is preserved, rather than supplying a default value. -/
+def RustModel.decodeBytesResult {Raw : Type u} (m : RustModel Raw)
+    (bytes : List Rust.Storage.AMByte) : Result m.Model :=
+  m.decodeResult (m.decodeBitsResult bytes)
+
+/-- Explicit metadata-indexed language decoding. No metadata is guessed from
+byte length, and every rejected width, representation, or metadata returns undef. -/
+def RustModel.decodeStorageBitsResult {Raw : Type u} {Metadata : Type v}
+    [DecidableEq Metadata] (physical : Rust.Storage.StorageDecoder Metadata Raw)
+    (metadata : Metadata) (bytes : List Rust.Storage.AMByte) : Result Raw :=
+  Result.ofOption (physical.run metadata bytes) .undef
+
+/-- Apply the retained mathematical provider after checked physical decoding.
+An explicit decoder supplies the layout and language domain; it does not
+supply a Rust ABI or provenance correspondence by virtue of its type. -/
+def RustModel.decodeStorageResult {Raw : Type u} {Metadata : Type v}
+    [DecidableEq Metadata] (m : RustModel Raw)
+    (physical : Rust.Storage.StorageDecoder Metadata Raw)
+    (metadata : Metadata) (bytes : List Rust.Storage.AMByte) : Result m.Model :=
+  m.decodeResult (RustModel.decodeStorageBitsResult physical metadata bytes)
+
+/-- One guarded composition underlies both Option admission and Aeneas failure. -/
+theorem RustModel.decodeStorageResult_as_runWith {Raw : Type u} {Metadata : Type v}
+    [DecidableEq Metadata] (m : RustModel Raw)
+    (physical : Rust.Storage.StorageDecoder Metadata Raw)
+    (metadata : Metadata) (bytes : List Rust.Storage.AMByte) :
+    m.decodeStorageResult physical metadata bytes =
+      Result.ofOption (physical.runWith m.decode metadata bytes) .undef := by
+  cases language : physical.run metadata bytes with
+  | none => simp [RustModel.decodeStorageResult, RustModel.decodeStorageBitsResult,
+      RustModel.decodeResult, Rust.Storage.StorageDecoder.runWith, language]
+  | some raw => simp [RustModel.decodeStorageResult, RustModel.decodeStorageBitsResult,
+      RustModel.decodeResult, Rust.Storage.StorageDecoder.runWith, language]
+
+/-- The fixed representation API is the Unit-metadata specialization. -/
+theorem RustModel.decodeBytesResult_eq_decodeStorageResult {Raw : Type u} (m : RustModel Raw)
+    (physical : Rust.Storage.BitDecoder Raw) (available : m.representation = some physical)
+    (bytes : List Rust.Storage.AMByte) :
+    m.decodeBytesResult bytes = m.decodeStorageResult physical.asStorageDecoder () bytes := by
+  simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, available,
+    RustModel.decodeStorageResult, RustModel.decodeStorageBitsResult]
+
 @[simp] theorem RustModel.decodeResult_ok {Raw : Type u} (m : RustModel Raw) (raw : Raw) :
     m.decodeResult (.ok raw) = Result.ofOption (m.decode raw) .undef := by
   simp [RustModel.decodeResult]
@@ -82,6 +147,18 @@ theorem RustModel.decodeResult_eq_ok_iff {Raw : Type u} (m : RustModel Raw)
   | vis effect continuation => simp [RustModel.decodeResult]
   | div => simp
 
+/-- A composed storage success retains the same physical and mathematical
+providers, with neither admission stage hidden by the other. -/
+theorem RustModel.decodeStorageResult_eq_ok_iff {Raw : Type u} {Metadata : Type v}
+    [DecidableEq Metadata] (m : RustModel Raw)
+    (physical : Rust.Storage.StorageDecoder Metadata Raw)
+    (metadata : Metadata) (bytes : List Rust.Storage.AMByte) (value : m.Model) :
+    m.decodeStorageResult physical metadata bytes = .ok value ↔
+      ∃ raw, physical.run metadata bytes = some raw ∧ m.decode raw = some value := by
+  rw [RustModel.decodeStorageResult_as_runWith,
+    ← Rust.Storage.StorageDecoder.runWith_eq_some_iff]
+  cases physical.runWith m.decode metadata bytes <;> simp
+
 /-- Total correctness for the composition is the existing decoded-result post
 on the original execution, with the provider and postcondition unchanged. -/
 theorem RustModel.spec_decodeResult_iff {Raw : Type u} (m : RustModel Raw)
@@ -106,10 +183,16 @@ theorem RustModel.dspec_decodeResult_iff {Raw : Type u} (m : RustModel Raw)
     simp only [RustModel.decodeResult_div]
     constructor <;> intro _ <;> exact WP.dspec.div _
 
-@[reducible] instance modelBool : RustModel Bool := { Model := Bool, «decode» := some }
+@[reducible] instance modelBool : RustModel Bool where
+  Model := Bool
+  decode := some
+  representation := some 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 := { Model := Unit, «decode» := some }
+@[reducible] instance modelUnit : RustModel Unit where
+  Model := Unit
+  decode := some
+  representation := some Rust.Storage.unitDecoder
 
 @[reducible] instance modelProd {α : Type u} {β : Type v} [ma : RustModel α] [mb : RustModel β] :
     RustModel (α × β) where
@@ -161,12 +244,75 @@ abbrev ArrayValue (Element : Type u) (n : Usize) :=
     | 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. -/
+def RustModel.sliceStorageDecoder {α : Type u} (element : Rust.Storage.BitDecoder α) :
+    Rust.Storage.StorageDecoder Usize (Slice α) where
+  byteSize count := count.val * element.byteSize
+  metadata := Slice.len
+  decode count bytes := (Rust.Storage.arrayDecode element count.val bytes).map (fun values =>
+    Slice.from values.val (by rw [values.property]; scalar_tac))
+
+/-- The native slice adapter has exactly the fixed-count array admission domain;
+only its carrier and explicit usize metadata differ. -/
+theorem RustModel.sliceStorageDecoder_run {α : Type u} (element : Rust.Storage.BitDecoder α)
+    (count : Usize) (bytes : List Rust.Storage.AMByte) :
+    (RustModel.sliceStorageDecoder element).run count bytes =
+      ((Rust.Storage.arrayDecoder element count.val).run bytes).map
+        (fun values => Slice.from values.val (by rw [values.property]; scalar_tac)) := by
+  by_cases width : bytes.length = count.val * element.byteSize
+  · simp only [Rust.Storage.StorageDecoder.run, RustModel.sliceStorageDecoder,
+      Rust.Storage.BitDecoder.run, Rust.Storage.arrayDecoder, width, ↓reduceIte]
+    cases language : Rust.Storage.arrayDecode element count.val bytes with
+    | none => rfl
+    | some values =>
+      have agrees : (Slice.from values.val (by rw [values.property]; scalar_tac)).len = count := by
+        apply UScalar.eq_of_val_eq
+        simp only [Slice.len_val, Slice.length, Slice.from_val, values.property]
+      simp [agrees]
+  · simp [Rust.Storage.StorageDecoder.run, RustModel.sliceStorageDecoder,
+      Rust.Storage.BitDecoder.run, Rust.Storage.arrayDecoder, width]
+
+/-- The slice adapter preserves the element initialization law. -/
+theorem RustModel.sliceStorageDecoder_initialized {α : Type u}
+    (element : Rust.Storage.BitDecoder α) (initialized : element.Initialized) :
+    (RustModel.sliceStorageDecoder element).Initialized := by
+  intro count bytes raw accepted
+  have language := ((Rust.Storage.StorageDecoder.run_eq_some_iff _ _ _ _).mp accepted).2.1
+  simp only [RustModel.sliceStorageDecoder] at language
+  cases decoded : Rust.Storage.arrayDecode element count.val bytes with
+  | none => simp [decoded] at language
+  | some values => exact Rust.Storage.arrayDecode_initialized element initialized count.val bytes values decoded
+
 @[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))
+
+/-- 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. -/
+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)
 
 -- 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/Zerocopy/TypesExternal.lean b/verification/aeneas/lean/Zerocopy/TypesExternal.lean
index 10c6e45a5b..41ca7b502f 100644
--- a/verification/aeneas/lean/Zerocopy/TypesExternal.lean
+++ b/verification/aeneas/lean/Zerocopy/TypesExternal.lean
@@ -11,10 +11,34 @@ public import Aeneas
 @[expose] public section
 open Aeneas.Std
 
--- These types model stored values, not Rust's niche encoding or memory layout.
--- The generic wrapper admits zero; the alignment theorems explicitly require
--- positivity. This over-approximation includes every valid NonZeroUsize.
+-- The extracted NonZero carrier deliberately admits a zero field. The
+-- physical and mathematical decoders in ModelPrelude perform the nonzero
+-- check; merely building this Lean record grants no Rust construction rights.
+abbrev core.num.niche_types.NonZeroU8Inner := U8
+abbrev core.num.niche_types.NonZeroI8Inner := I8
+abbrev core.num.niche_types.NonZeroU16Inner := U16
+abbrev core.num.niche_types.NonZeroI16Inner := I16
+abbrev core.num.niche_types.NonZeroU32Inner := U32
+abbrev core.num.niche_types.NonZeroI32Inner := I32
+abbrev core.num.niche_types.NonZeroU64Inner := U64
+abbrev core.num.niche_types.NonZeroI64Inner := I64
+abbrev core.num.niche_types.NonZeroU128Inner := U128
+abbrev core.num.niche_types.NonZeroI128Inner := I128
 abbrev core.num.niche_types.NonZeroUsizeInner := Usize
+abbrev core.num.niche_types.NonZeroIsizeInner := Isize
 
 structure core.num.nonzero.NonZero (T : Type) (_Inner : Type) where
   val : T
+
+-- These standard-library types are opaque at this extraction boundary. Their
+-- documented byte representation is that of T. Retain nominal wrappers:
+-- identical stored bytes do not make their APIs or invariants interchangeable.
+-- This models only stored values, not Cell's access protocol or destruction.
+structure core.mem.manually_drop.ManuallyDrop (T : Type) where
+  value : T
+
+structure core.cell.Cell (T : Type) where
+  value : T
+
+structure core.cell.UnsafeCell (T : Type) where
+  value : T
diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean
index a196c69439..67cf095612 100644
--- a/verification/aeneas/projections/Models.lean
+++ b/verification/aeneas/projections/Models.lean
@@ -22,10 +22,10 @@ check_model_binding Zerocopy.byteorder.BigEndian with 0 type parameters
 derive_rust_model Zerocopy.byteorder.LittleEndian with 0 type parameters
 check_model_binding Zerocopy.byteorder.LittleEndian with 0 type parameters
 
-derive_rust_model Zerocopy.byteorder.U16 with 1 type parameters
+derive_rust_model Zerocopy.byteorder.U16 with 1 type parameters with_physical 0
 check_model_binding Zerocopy.byteorder.U16 with 1 type parameters
 
-derive_rust_model Zerocopy.byteorder.U32 with 1 type parameters
+derive_rust_model Zerocopy.byteorder.U32 with 1 type parameters with_physical 0
 check_model_binding Zerocopy.byteorder.U32 with 1 type parameters
 
 derive_rust_model Zerocopy.trait_checks.XorCodec with 0 type parameters
diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean
index 9c2fb98603..5911ea7f12 100644
--- a/verification/aeneas/projections/Specs.lean
+++ b/verification/aeneas/projections/Specs.lean
@@ -138,6 +138,19 @@ spec forwarded_byte_codec_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.forwarded_byte_codec_spec for Zerocopy.trait_checks.forwarded_byte_codec with 1
 
+check_model_inputs Zerocopy.trait_checks.check_array_into_bytes with 0 type parameters
+aeneas_spec_begin
+spec array_into_bytes_spec
+  for @Zerocopy.trait_checks.check_array_into_bytes with 0 type parameters
+  ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Bool 3#usize)
+  ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array U8 3#usize)
+  ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Unit 4#usize)
+  ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Bool 0#usize)
+  ensures _ => AeneasSpecs.RustModel.initializedRepresentation
+    (Aeneas.Std.Array (Aeneas.Std.Array Bool 2#usize) 3#usize)
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.array_into_bytes_spec for Zerocopy.trait_checks.check_array_into_bytes with 0
+
 check_model_inputs Zerocopy.util.padding_needed_for with 0 type parameters
 aeneas_spec_begin
 spec padding_lt_alignment
diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean
index 2d539fc6c2..166c642ed6 100644
--- a/verification/aeneas/projections/TraitLaws.lean
+++ b/verification/aeneas/projections/TraitLaws.lean
@@ -16,9 +16,13 @@ namespace Zerocopy.TraitLaws
 trait_dictionary @Zerocopy.core.num.nonzero.ZeroablePrimitive
 trait_dictionary @Zerocopy.byteorder.private.Sealed
 trait_dictionary @Zerocopy.byteorder.ByteOrder
+trait_dictionary @Zerocopy.IntoBytes
 trait_dictionary @Zerocopy.trait_checks.ByteCodec
 trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type parameters where self =>
   ∀ byte, (do let encoded ← self.encode byte; self.decode encoded)
       ⦃ result => result = byte ⦄
 
+trait_invariant into_bytes_initialized for @Zerocopy.IntoBytes with 1 type parameters where self =>
+  AeneasSpecs.RustModel.initializedRepresentation Self
+
 end Zerocopy.TraitLaws
diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs
index 4df786fd21..5912f1835f 100644
--- a/zerocopy/src/impls.rs
+++ b/zerocopy/src/impls.rs
@@ -904,7 +904,17 @@ const _: () = unsafe {
     });
     unsafe_impl!(const N: usize, T: FromZeros => FromZeros for [T; N]);
     unsafe_impl!(const N: usize, T: FromBytes => FromBytes for [T; N]);
-    unsafe_impl!(const N: usize, T: IntoBytes => IntoBytes for [T; N]);
+    // SAFETY: As shown above, arrays concatenate their elements without extra
+    // padding. `T: IntoBytes` guarantees that each element's entire storage is
+    // initialized, so every byte of the array is initialized too, including for
+    // zero-length arrays and zero-sized elements. The invariant proof checks
+    // this implication for every `T` and `N`, under the Rust array-layout model.
+    unsafe_impl!(
+        /// ```aeneas
+        /// invariant_proof
+        /// ```
+        const N: usize, T: IntoBytes => IntoBytes for [T; N]
+    );
     unsafe_impl!(const N: usize, T: Unaligned => Unaligned for [T; N]);
     assert_unaligned!([(); 0], [(); 1], [u8; 0], [u8; 1]);
     unsafe_impl!(T: Immutable => Immutable for [T]);
diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs
index 2f7d78f7cd..ea6b1cbb28 100644
--- a/zerocopy/src/lib.rs
+++ b/zerocopy/src/lib.rs
@@ -5934,6 +5934,10 @@ pub use zerocopy_derive::IntoBytes;
     not(no_zerocopy_diagnostic_on_unimplemented_1_78_0),
     diagnostic::on_unimplemented(note = "Consider adding `#[derive(IntoBytes)]` to `{Self}`")
 )]
+/// ```aeneas
+/// invariant into_bytes_initialized for self =>
+///   AeneasSpecs.RustModel.initializedRepresentation Self
+/// ```
 pub unsafe trait IntoBytes {
     // The `Self: Sized` bound makes it so that this function doesn't prevent
     // `IntoBytes` from being object safe. Note that other `IntoBytes` methods
diff --git a/zerocopy/src/trait_checks.rs b/zerocopy/src/trait_checks.rs
index 637a3f65d2..ed16535077 100644
--- a/zerocopy/src/trait_checks.rs
+++ b/zerocopy/src/trait_checks.rs
@@ -74,6 +74,29 @@ fn forwarded_byte_codec(byte: u8) -> u8 {
     byte_codec_roundtrip::<Forward<XorCodec>>(byte)
 }
 
+fn require_into_bytes<T: crate::IntoBytes>() {}
+
+/// Forces extraction of the existing array IntoBytes implementation and its
+/// primitive and nested dependencies. CI checks the generic implementation law
+/// for every count; these concrete uses also exercise Rust's trait selection.
+///
+/// ```aeneas
+/// spec array_into_bytes_spec
+///   ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Bool 3#usize)
+///   ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array U8 3#usize)
+///   ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Unit 4#usize)
+///   ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Bool 0#usize)
+///   ensures _ => AeneasSpecs.RustModel.initializedRepresentation
+///     (Aeneas.Std.Array (Aeneas.Std.Array Bool 2#usize) 3#usize)
+/// ```
+fn check_array_into_bytes() {
+    require_into_bytes::<[bool; 3]>();
+    require_into_bytes::<[u8; 3]>();
+    require_into_bytes::<[(); 4]>();
+    require_into_bytes::<[bool; 0]>();
+    require_into_bytes::<[[bool; 2]; 3]>();
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -83,5 +106,6 @@ mod tests {
         for byte in 0..=u8::MAX {
             assert_eq!(forwarded_byte_codec(byte), byte);
         }
+        check_array_into_bytes();
     }
 }