Require realizable source representations for IntoBytes

verification/aeneas/README.md

@@ -728,6 +728,14 @@ requires an available physical decoder and initialization over its entire
 accepted domain. Absence is `False`; rejection by the library's mathematical
 `RustModel.decode` cannot reduce this domain.
 
+The law also requires **source realizability**: each raw value admitted by the
+mathematical decoder has at least one physical byte representation. Initialization
+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
+inhabitedness assumption is introduced.
+
 There are 59 authored implementation markers: `()`, `bool`, `char`; all twelve
 signed/unsigned integer carriers; all twelve corresponding `NonZero` carriers
 and their `Option` forms; `PhantomData`; arrays; `Wrapping`, `ManuallyDrop`,

verification/aeneas/golden/Types.lean

@@ -346,13 +346,13 @@ structure FromBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
 /-- Trait declaration: [zerocopy::IntoBytes]
-    Source: 'src/lib.rs', lines 6017:0-6490:1
+    Source: 'src/lib.rs', lines 6018:0-6491:1
     Visibility: public -/
 structure IntoBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
 /-- Trait declaration: [zerocopy::Unaligned]
-    Source: 'src/lib.rs', lines 6628:0-6635:1
+    Source: 'src/lib.rs', lines 6629:0-6636:1
     Visibility: public -/
 structure Unaligned (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit

verification/aeneas/lean/Proofs/TraitChecks.lean

@@ -9,6 +9,7 @@ those terms. -/
 module
 public import Specs
 public import TraitLaws
+public import RustRealizability
 @[expose] public section
 
 /-!
@@ -50,15 +51,15 @@ namespace Zerocopy.Proofs
 -- 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⟩
+  ⟨⟨Rust.Storage.boolDecoder_initialized, realizableBool⟩⟩
 
 @[instance] theorem U8.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized U8 Zerocopy.U8.Insts.ZerocopyIntoBytes :=
-  ⟨initializedUScalar .U8⟩
+  ⟨⟨initializedUScalar .U8, realizableUScalar .U8⟩⟩
 
 @[instance] theorem Tuple.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized Unit Zerocopy.Tuple.Insts.ZerocopyIntoBytes :=
-  ⟨Rust.Storage.unitDecoder_initialized⟩
+  ⟨⟨Rust.Storage.unitDecoder_initialized, realizableUnit⟩⟩
 
 -- The original type, const length, and computational dictionary remain the
 -- native implementation's prefix. Only the element's provider and law are
@@ -68,7 +69,10 @@ namespace Zerocopy.Proofs
     [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)⟩
+  ⟨⟨RustModel.initialized_array T N
+      (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1,
+    RustModel.realizable_array T N
+      (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
 -- Calling the real Rust helper selects the existing unsafe impls in Charon.
 -- The generic impl law proves all lengths; these concrete cases additionally
@@ -79,20 +83,20 @@ theorem array_into_bytes_spec : Specs.array_into_bytes_spec := by
   refine ⟨(), rfl, ?_, ?_, ?_, ?_, ?_⟩
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)
-      _ inferInstance)
+      _ inferInstance).1
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.U8.Insts.ZerocopyIntoBytes)
-      _ inferInstance)
+      _ inferInstance).1
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Tuple.Insts.ZerocopyIntoBytes)
-      _ inferInstance)
+      _ inferInstance).1
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)
-      _ inferInstance)
+      _ inferInstance).1
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _
         (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes))
-      _ inferInstance)
+      _ inferInstance).1
 
 theorem unaligned_alignment_spec : Specs.unaligned_alignment_spec := by
   intro T dictionary _ law

verification/aeneas/lean/RustModel.lean

@@ -63,6 +63,14 @@ def RustModel.initializedRepresentation (Raw : Type u) [m : RustModel Raw] : Pro
   | none => False
   | some decoder => decoder.Initialized
 
+/-- Every admitted source has some physical representation. This is vacuous
+for uninhabited sources and does not require a canonical encoding. -/
+def RustModel.realizableRepresentation (Raw : Type u) [m : RustModel Raw] : Prop :=
+  match m.representation with
+  | none => False
+  | some decoder => ∀ raw, @isValid Raw m raw →
+      ∃ bytes, decoder.run bytes = some raw
+
 /-- Every initialized representation of the physical width admits a language
 value and a mathematical value through this same provider. Missing physical
 semantics fail closed. This law does not establish Rust layout correspondence,