Prove the native slice IntoBytes implementation

verification/aeneas/DESIGN.md

@@ -500,6 +500,9 @@ 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.
+The native slice `IntoBytes` impl carries the same mandatory proof marker as
+its fixed-layout counterparts; the client harness exercises native slice and
+unsized-wrapper dictionary selection.
 
 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

verification/aeneas/LOWERING_AUDIT.md

@@ -143,7 +143,7 @@ translation premises already recorded in [SEMANTICS.md](SEMANTICS.md).
 
 ### Exact authored implementation scope
 
-The default-feature library extraction has 59 nameless `invariant_proof`
+The default-feature library extraction has 60 nameless `invariant_proof`
 markers, each attached through invocation arguments to one native positive
 `IntoBytes` impl. This count inventories authored claims; the native binding
 manifest and checked implementation-law witnesses establish which compiled
@@ -157,6 +157,7 @@ owners fulfill them.
 | Niche option | `Option<N>` for each of the preceding 12 nonzero carriers | 12 |
 | Empty marker | `PhantomData<T>` for `T: ?Sized`, without `T: IntoBytes` | 1 |
 | Array | `[T; N]` for `T: IntoBytes`, every `const N: usize` | 1 |
+| Slice | `[T]` for `T: IntoBytes`, every explicit `usize` element count | 1 |
 | Sized wrapper | `Wrapping<T>`, `Unalign<T>` for `T: IntoBytes` | 2 |
 | Possibly unsized wrapper | `ManuallyDrop<T>`, `Cell<T>`, `UnsafeCell<T>`, `ReadOnly<T>` for `T: ?Sized + IntoBytes` | 4 |
 | Byteorder | `U16<O>`, `U32<O>`, `U64<O>`, `U128<O>`, `Usize<O>`, `I16<O>`, `I32<O>`, `I64<O>`, `I128<O>`, `Isize<O>`, `F32<O>`, `F64<O>` for every `O`, without `O: ByteOrder` | 12 |
@@ -176,15 +177,15 @@ Byteorder markers are concrete invocation arguments, not a fence duplicated by
 `define_type!`. `F32` and `F64` store `[u8; 4]` and `[u8; 8]`; their laws depend
 on those byte arrays, not native floating-point bit semantics.
 
-Deferred implementations are `[T]`, `str`, native `f32`/`f64` and feature-gated
+Deferred implementations are `str`, native `f32`/`f64` and feature-gated
 `f16`/`f128`, atomics under their target/version cfgs, SIMD under its
 feature/target/version cfgs, procedural derives, and the generated struct/union
 impls of `cryptocorrosion_derive_traits!`. These remain ordinary Rust impls;
 this inventory makes no initialization-law certification for them. Neither
 core nor zerocopy `MaybeUninit`, non-unit tuples, raw pointers, references,
 `NonNull`, nor arbitrary `Option<T>` has an `IntoBytes` impl in this snapshot.
 Incoming downstream dictionaries still require their own conditional law
-premises; these 59 local markers do not certify future external implementations.
+premises; these 60 local markers do not certify future external implementations.
 
 ### Decoder correspondence premises
 

verification/aeneas/README.md

@@ -56,6 +56,18 @@ allocator admission additionally needs the outer alignment and the signed
 metadata-size bound. Allocator behavior, zeroing, and `Box` validity remain
 separate Rust obligations.
 
+The native `[T]: IntoBytes` implementation has an `invariant_proof` marker.
+Its proof consumes the element's actual trait dictionary and retained model,
+then establishes initialization and realizability at explicit slice counts.
+`trait_checks::check_slice_into_bytes` also exercises concrete slice and
+`ManuallyDrop<[u8]>` dictionary selection. Zero-sized elements keep their count;
+an empty slice of an uninhabited type does not manufacture an element.
+
+The shared `Rust.Pointer.Geometry` library proves bounded projections and cast
+composition, including empty destinations and slice splitting. These are
+mathematical foundations. Native pointer operations remain rejected by admission
+because the unchanged Aeneas pointer carrier cannot preserve their geometry.
+
 These harnesses use the same annotation and proof rules as every other function.
 There is no root marker or separately maintained list of required functions.
 Every present specification must have its corresponding proof in both CI builds.
@@ -738,15 +750,15 @@ satisfy it vacuously. The reusable proofs in
 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
+There are 60 authored implementation markers: `()`, `bool`, `char`; all twelve
 signed/unsigned integer carriers; all twelve corresponding `NonZero` carriers
-and their `Option` forms; `PhantomData`; arrays; `Wrapping`, `ManuallyDrop`,
+and their `Option` forms; `PhantomData`; arrays and slices; `Wrapping`, `ManuallyDrop`,
 `Cell`, `UnsafeCell`, `ReadOnly`, `Unalign`; and all twelve byteorder wrappers.
 [The scope inventory](LOWERING_AUDIT.md#exact-authored-implementation-scope)
 retains their exact generic bounds, configuration branches, and deferred impls.
 The default library build selects the handwritten `Unalign` and byteorder
 implementations; their derive/test alternatives remain deferred. Native floats,
-slices, `str`, atomics, SIMD, and other derive-generated impls remain outside
+`str`, atomics, SIMD, and other derive-generated impls remain outside
 this implementation-law scope.
 
 Integer physical decoders assemble initialized bytes in the extraction target's

verification/aeneas/golden/Funs.lean

@@ -3358,7 +3358,7 @@ def pointer.invariant.CastableFromDTSTInitializedInitialized.Blanket (ST :
 }
 
 /-- [zerocopy::pointer::cast::cast_unsized_layouts_match]:
-    Source: 'src/pointer/mod.rs', lines 196:4-208:5 -/
+    Source: 'src/pointer/mod.rs', lines 205:4-217:5 -/
 def pointer.cast.cast_unsized_layouts_match
   (src : layout.DstLayout) (dst : layout.DstLayout) : Result Bool := do
   match src.size_info with
@@ -3388,7 +3388,7 @@ def pointer.cast.cast_unsized_layouts_match
       else ok false
 
 /-- [zerocopy::pointer::cast::checks::witness_matches]:
-    Source: 'src/pointer/mod.rs', lines 219:8-226:9 -/
+    Source: 'src/pointer/mod.rs', lines 228:8-235:9 -/
 def pointer.cast.checks.witness_matches
   (runtime_layout : layout.DstLayout)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -3401,7 +3401,7 @@ def pointer.cast.checks.witness_matches
     layout.tail_transform_checks.witness_matches tail align phase
 
 /-- [zerocopy::pointer::cast::checks::reference_size]:
-    Source: 'src/pointer/mod.rs', lines 228:8-240:9 -/
+    Source: 'src/pointer/mod.rs', lines 237:8-249:9 -/
 def pointer.cast.checks.reference_size
   (runtime_layout : layout.DstLayout)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -3415,7 +3415,7 @@ def pointer.cast.checks.reference_size
     layout.tail_checks.reference_size tail align phase metadata
 
 /-- [zerocopy::pointer::cast::checks::assert_cast_unsized]:
-    Source: 'src/pointer/mod.rs', lines 252:8-277:9 -/
+    Source: 'src/pointer/mod.rs', lines 261:8-286:9 -/
 def pointer.cast.checks.assert_cast_unsized
   (src : layout.DstLayout) (dst : layout.DstLayout)
   (src_align : core.num.nonzero.NonZero Std.Usize
@@ -3461,7 +3461,7 @@ def pointer.cast.checks.assert_cast_unsized
   else ok ()
 
 /-- [zerocopy::pointer::referent_checks::require_transfer]:
-    Source: 'src/pointer/referent_checks.rs', lines 27:0-31:1 -/
+    Source: 'src/pointer/referent_checks.rs', lines 28:0-32:1 -/
 def pointer.referent_checks.require_transfer
   {Src : Type} {Dst : Type} {SV : Type} {DV : Type} (transmuteTransmuteFromInst
   : pointer.transmute.TransmuteFrom Dst Src SV DV) :
@@ -3470,7 +3470,7 @@ def pointer.referent_checks.require_transfer
   ok ()
 
 /-- [zerocopy::pointer::referent_checks::require_type_independent]:
-    Source: 'src/pointer/referent_checks.rs', lines 37:0-41:1 -/
+    Source: 'src/pointer/referent_checks.rs', lines 38:0-42:1 -/
 def pointer.referent_checks.require_type_independent
   {Src : Type} {Dst : Type} {SV : Type} {DV : Type} (invariantCastableFromInst
   : pointer.invariant.CastableFrom Dst Src SV DV) :
@@ -3479,7 +3479,7 @@ def pointer.referent_checks.require_type_independent
   ok ()
 
 /-- [zerocopy::pointer::referent_checks::compose_safe_transfers]:
-    Source: 'src/pointer/referent_checks.rs', lines 52:0-57:1 -/
+    Source: 'src/pointer/referent_checks.rs', lines 53:0-58:1 -/
 def pointer.referent_checks.compose_safe_transfers
   {Src : Type} {Mid : Type} {Dst : Type}
   (transmuteTransmuteFromMidSrcSafeSafeInst : pointer.transmute.TransmuteFrom
@@ -3592,7 +3592,7 @@ def pointer.transmute.TransmuteFromDstSrcSafeInitialized.Blanket {Src : Type}
 }
 
 /-- [zerocopy::pointer::referent_checks::concrete_transfers]:
-    Source: 'src/pointer/referent_checks.rs', lines 72:0-79:1 -/
+    Source: 'src/pointer/referent_checks.rs', lines 73:0-80:1 -/
 def pointer.referent_checks.concrete_transfers : Result Unit := do
   pointer.referent_checks.require_transfer
     (pointer.transmute.TransmuteFromDstSrcSafeInitialized.Blanket Std.U8
@@ -3941,7 +3941,7 @@ def trait_checks.forwarded_byte_codec (byte : Std.U8) : Result Std.U8 := do
     trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec) byte
 
 /-- [zerocopy::trait_checks::require_into_bytes]:
-    Source: 'src/trait_checks.rs', lines 148:0-148:47 -/
+    Source: 'src/trait_checks.rs', lines 148:0-148:56 -/
 def trait_checks.require_into_bytes
   {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do
   ok ()
@@ -4009,6 +4009,54 @@ def trait_checks.check_array_into_bytes : Result Unit := do
   trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize
     (Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes))
 
+/-- [zerocopy::impls::_#35::{impl zerocopy::IntoBytes for core::mem::manually_drop::ManuallyDrop<T>}::only_derive_is_allowed_to_implement_this_trait]:
+    Source: 'src/util/macros.rs', lines 204:16-221:17
+    Visibility: public -/
+def
+  core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+  {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do
+  ok ()
+
+/-- Trait implementation: [zerocopy::impls::_#35::{impl zerocopy::IntoBytes for core::mem::manually_drop::ManuallyDrop<T>}]
+    Source: 'src/util/macros.rs', lines 201:12-228:13 -/
+@[reducible]
+def core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes {T : Type}
+  (IntoBytesInst : IntoBytes T) : IntoBytes
+  (core.mem.manually_drop.ManuallyDrop T) := {
+  only_derive_is_allowed_to_implement_this_trait :=
+    core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+    IntoBytesInst
+}
+
+/-- [zerocopy::impls::_#23::{impl zerocopy::IntoBytes for [T]}::only_derive_is_allowed_to_implement_this_trait]:
+    Source: 'src/util/macros.rs', lines 165:8-165:62
+    Visibility: public -/
+def
+  Slice.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+  {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do
+  ok ()
+
+/-- Trait implementation: [zerocopy::impls::_#23::{impl zerocopy::IntoBytes for [T]}]
+    Source: 'src/util/macros.rs', lines 132:8-134:9 -/
+@[reducible]
+def Slice.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst : IntoBytes T) :
+  IntoBytes (Slice T) := {
+  only_derive_is_allowed_to_implement_this_trait :=
+    Slice.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
+    IntoBytesInst
+}
+
+/-- [zerocopy::trait_checks::check_slice_into_bytes]:
+    Source: 'src/trait_checks.rs', lines 183:0-187:1 -/
+def trait_checks.check_slice_into_bytes : Result Unit := do
+  trait_checks.require_into_bytes (Slice.Insts.ZerocopyIntoBytes
+    Bool.Insts.ZerocopyIntoBytes)
+  trait_checks.require_into_bytes (Slice.Insts.ZerocopyIntoBytes
+    Tuple.Insts.ZerocopyIntoBytes)
+  trait_checks.require_into_bytes
+    (core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes
+    (Slice.Insts.ZerocopyIntoBytes U8.Insts.ZerocopyIntoBytes))
+
 /-- [zerocopy::util::allocation::prepare]:
     Source: 'src/util/allocation.rs', lines 33:0-38:1 -/
 def util.allocation.prepare
@@ -5327,25 +5375,6 @@ def core.num.wrapping.Wrapping.Insts.ZerocopyIntoBytes {T : Type}
     IntoBytesInst
 }
 
-/-- [zerocopy::impls::_#35::{impl zerocopy::IntoBytes for core::mem::manually_drop::ManuallyDrop<T>}::only_derive_is_allowed_to_implement_this_trait]:
-    Source: 'src/util/macros.rs', lines 204:16-221:17
-    Visibility: public -/
-def
-  core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
-  {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do
-  ok ()
-
-/-- Trait implementation: [zerocopy::impls::_#35::{impl zerocopy::IntoBytes for core::mem::manually_drop::ManuallyDrop<T>}]
-    Source: 'src/util/macros.rs', lines 201:12-228:13 -/
-@[reducible]
-def core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes {T : Type}
-  (IntoBytesInst : IntoBytes T) : IntoBytes
-  (core.mem.manually_drop.ManuallyDrop T) := {
-  only_derive_is_allowed_to_implement_this_trait :=
-    core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait
-    IntoBytesInst
-}
-
 /-- [zerocopy::impls::_#39::{impl zerocopy::IntoBytes for core::cell::Cell<T>}::only_derive_is_allowed_to_implement_this_trait]:
     Source: 'src/util/macros.rs', lines 204:16-221:17
     Visibility: public -/

verification/aeneas/lean/Obligations/TraitChecks.lean

@@ -104,4 +104,25 @@ def forwarded_byte_codec_spec_contract (byte : U8) (run : Result U8) : Prop :=
 def forwarded_byte_codec_spec : Prop :=
   ∀ (byte : U8), forwarded_byte_codec_spec_contract byte (trait_checks.forwarded_byte_codec byte)
 
+/-- Explicit count-indexed expectation, independent of provider selection. -/
+def sliceBytesInitialized (element : Rust.Storage.BitDecoder Raw) : Prop :=
+  ∀ (count : Usize) bytes raw,
+    (AeneasSpecs.RustModel.sliceStorageDecoder element).run count bytes = some raw →
+      Rust.Storage.Initialized bytes
+
+def slice_into_bytes_spec_contract (run : Result Unit) : Prop :=
+  run ⦃ _ =>
+    sliceBytesInitialized Rust.Storage.boolDecoder ∧
+    (∀ raw : Aeneas.Std.Slice Bool, ∃ bytes,
+      (AeneasSpecs.RustModel.sliceStorageDecoder Rust.Storage.boolDecoder).run raw.len bytes = some raw) ∧
+    sliceBytesInitialized Rust.Storage.unitDecoder ∧
+    (∀ (count : Usize) bytes raw,
+      ((AeneasSpecs.RustModel.sliceStorageDecoder AeneasSpecs.u8BitDecoder).map
+        core.mem.manually_drop.ManuallyDrop.mk
+        (fun wrapped => wrapped.value.len) (fun _ => rfl)).run count bytes = some raw →
+      Rust.Storage.Initialized bytes) ⦄
+
+def slice_into_bytes_spec : Prop :=
+  slice_into_bytes_spec_contract trait_checks.check_slice_into_bytes
+
 end Zerocopy.Obligations

verification/aeneas/lean/Proofs/IntoBytes.lean

@@ -365,4 +365,34 @@ namespace Zerocopy.Proofs
     (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk) (·._0) (fun _ => rfl)
     (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderF64 O⟩⟩
 
+-- The native slice dictionary retains the element's exact provider and law.
+-- Its result uses explicit count metadata; it never recovers a count from bytes.
+@[instance] theorem Slice.Insts.ZerocopyIntoBytes_law
+    {T : Type} (dictionary : IntoBytes T)
+    [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
+    TraitLaws.into_bytes_initialized (Aeneas.Std.Slice T)
+      (Zerocopy.Slice.Insts.ZerocopyIntoBytes dictionary) :=
+  ⟨⟨RustModel.initialized_slice T
+      (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1,
+    RustModel.realizable_slice T
+      (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
+
+theorem slice_into_bytes_spec : Specs.slice_into_bytes_spec := by
+  simp only [Specs.slice_into_bytes_spec, Zerocopy.trait_checks.check_slice_into_bytes,
+    Zerocopy.trait_checks.require_into_bytes, bind_ok, WP.spec_ok]
+  refine ⟨(), rfl, ?_, ?_, ?_, ?_⟩
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.Slice.Insts.ZerocopyIntoBytes Zerocopy.Bool.Insts.ZerocopyIntoBytes)
+      _ inferInstance).1
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.Slice.Insts.ZerocopyIntoBytes Zerocopy.Bool.Insts.ZerocopyIntoBytes)
+      _ inferInstance).2
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.Slice.Insts.ZerocopyIntoBytes Zerocopy.Tuple.Insts.ZerocopyIntoBytes)
+      _ inferInstance).1
+  · exact (@TraitLaws.into_bytes_initialized.holds _
+      (Zerocopy.core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes
+        (Zerocopy.Slice.Insts.ZerocopyIntoBytes Zerocopy.U8.Insts.ZerocopyIntoBytes))
+      _ inferInstance).1
+
 end Zerocopy.Proofs

verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean

@@ -10,6 +10,7 @@ module
 public import Specs
 public import Obligations.TraitChecks
 public import MathViews
+public import RustRealizability
 @[expose] public section
 
 /-!
@@ -29,6 +30,15 @@ namespace Zerocopy.Proofs
   rintro _ ⟨_, _, boolean, byte, unit, empty, nested⟩
   exact ⟨boolean, byte, unit, empty, nested⟩
 
+@[contract_simps] theorem required_slice_into_bytes (run : Result Unit)
+    (provided : Specs.slice_into_bytes_spec_contract run) :
+    Obligations.slice_into_bytes_spec_contract run := by
+  apply WP.spec_mono provided
+  rintro _ ⟨_, _, boolean, realizable, unit, wrapped⟩
+  refine ⟨boolean, ?_, unit, wrapped⟩
+  intro raw
+  exact realizable raw (RustModel.valid_slice raw (fun item _ => ⟨item, rfl⟩))
+
 @[contract_simps] theorem required_unaligned_alignment (T : Type) (dictionary : Unaligned T)
     (run : Result Usize)
     (provided : Specs.unaligned_alignment_spec_contract T dictionary run) :

verification/aeneas/native_types.py

@@ -88,10 +88,11 @@ def lift(current):
         current = _plain(current)
         if not isinstance(current, dict) or len(current) != 1:
             return current
-        if 'Array' in current:
-            array = deepcopy(current['Array'])
-            array[0] = lift(array[0])
-            return {'Array': array}
+        if 'Array' in current or 'Slice' in current:
+            kind = 'Array' if 'Array' in current else 'Slice'
+            sequence = deepcopy(current[kind])
+            sequence[0] = lift(sequence[0])
+            return {kind: sequence}
         if 'Adt' not in current:
             return current
         body = deepcopy(current['Adt'])

verification/aeneas/projections/Specs.lean

@@ -752,6 +752,18 @@ spec array_into_bytes_spec
 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.trait_checks.check_slice_into_bytes with 0 type parameters
+aeneas_spec_begin
+spec slice_into_bytes_spec
+  for @Zerocopy.trait_checks.check_slice_into_bytes with 0 type parameters
+  ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Slice Bool)
+  ensures _ => AeneasSpecs.RustModel.realizableRepresentation (Aeneas.Std.Slice Bool)
+  ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Slice Unit)
+  ensures _ => AeneasSpecs.RustModel.initializedRepresentation
+    (core.mem.manually_drop.ManuallyDrop (Aeneas.Std.Slice U8))
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.slice_into_bytes_spec for Zerocopy.trait_checks.check_slice_into_bytes with 0
+
 check_model_inputs Zerocopy.util.allocation.prepare with 0 type parameters
 aeneas_spec_begin
 spec allocation_prepare_spec