Retain indexed storage in Rust model providers

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.

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.

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]`;

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

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,38 +52,38 @@ 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
 -- 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)
+  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