Prove array IntoBytes initialization from element laws

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

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

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

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

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:

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. -/