diff --git a/verification/aeneas/DESIGN.md b/verification/aeneas/DESIGN.md index 5bcfc3c73a..ebd0bc2064 100644 --- a/verification/aeneas/DESIGN.md +++ b/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 diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md index e9af0cdb16..a585dc23a7 100644 --- a/verification/aeneas/LOWERING_AUDIT.md +++ b/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` for each of the preceding 12 nonzero carriers | 12 | | Empty marker | `PhantomData` 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`, `Unalign` for `T: IntoBytes` | 2 | | Possibly unsized wrapper | `ManuallyDrop`, `Cell`, `UnsafeCell`, `ReadOnly` for `T: ?Sized + IntoBytes` | 4 | | Byteorder | `U16`, `U32`, `U64`, `U128`, `Usize`, `I16`, `I32`, `I64`, `I128`, `Isize`, `F32`, `F64` for every `O`, without `O: ByteOrder` | 12 | @@ -176,7 +177,7 @@ 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; @@ -184,7 +185,7 @@ this inventory makes no initialization-law certification for them. Neither core nor zerocopy `MaybeUninit`, non-unit tuples, raw pointers, references, `NonNull`, nor arbitrary `Option` 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 diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 3bbb0bbfc0..8f3f9b1a31 100644 --- a/verification/aeneas/README.md +++ b/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 diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index ffb883540c..2f82d89664 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/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}::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}] + 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}::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}] - 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}::only_derive_is_allowed_to_implement_this_trait]: Source: 'src/util/macros.rs', lines 204:16-221:17 Visibility: public -/ diff --git a/verification/aeneas/lean/Obligations/TraitChecks.lean b/verification/aeneas/lean/Obligations/TraitChecks.lean index 78612aaab1..4fe9eb411c 100644 --- a/verification/aeneas/lean/Obligations/TraitChecks.lean +++ b/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 diff --git a/verification/aeneas/lean/Proofs/IntoBytes.lean b/verification/aeneas/lean/Proofs/IntoBytes.lean index ca868e7d2f..e54242d0d4 100644 --- a/verification/aeneas/lean/Proofs/IntoBytes.lean +++ b/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 diff --git a/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean b/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean index 3dc1ee91bf..826f7647ea 100644 --- a/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean +++ b/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) : diff --git a/verification/aeneas/native_types.py b/verification/aeneas/native_types.py index adb05c7010..c5c94641f0 100644 --- a/verification/aeneas/native_types.py +++ b/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']) diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 955c877fac..28d2b8e45d 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/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 diff --git a/verification/aeneas/tests/test_native_types.py b/verification/aeneas/tests/test_native_types.py index 2b2a78ee3a..3c80416474 100644 --- a/verification/aeneas/tests/test_native_types.py +++ b/verification/aeneas/tests/test_native_types.py @@ -71,7 +71,7 @@ def test_all_twelve_concrete_dictionaries_preserve_nominal_inner(self): self.assertEqual(source, untouched) self.assertEqual(traits.simple_type(lifted, before)[2][1][0], 'nominal') - def test_option_and_array_recurse_without_erasing_the_carrier(self): + def test_option_array_and_slice_recurse_without_erasing_the_carrier(self): before, final, source, expected = fixture() option = {'def_id': 4, 'item_meta': meta('core::option::Option'), 'generics': params(['T'])} before['type_decls'].append(option) @@ -82,6 +82,9 @@ def test_option_and_array_recurse_without_erasing_the_carrier(self): lifted = native.lift_original_type(array, before, final) self.assertEqual(lifted['Array'][0], expected) self.assertEqual(lifted['Array'][1:], array['Array'][1:]) + sliced = {'Slice': [source, None]} + self.assertEqual(native.lift_original_type(sliced, before, final), + {'Slice': [expected, None]}) def test_rejects_changed_native_evidence(self): mutations = { diff --git a/verification/aeneas/tests/test_trait_invariants.py b/verification/aeneas/tests/test_trait_invariants.py index cd46983448..675ea24a72 100644 --- a/verification/aeneas/tests/test_trait_invariants.py +++ b/verification/aeneas/tests/test_trait_invariants.py @@ -85,6 +85,51 @@ def test_only_empty_rust_tuple_has_unit_identity(self): with self.assertRaisesRegex(ValueError, 'carrier erasure'): traits.simple_type(unit, self.final) + def test_slice_retains_element_identity_and_rejects_unknown_metadata(self): + element = {'TypeVar': {'Free': 0}} + self.assertEqual(traits.simple_type({'Slice': [element, None]}, self.final), + ['slice', ['parameter', 0]]) + for ty in ({'Slice': [element]}, {'Slice': [element, {'unknown': 0}]}, + {'Slice': [{'RawPtr': [element, 'Shared']}, None]}, + {'Ref': [None, {'Slice': [element, None]}, 'Mut']}): + with self.assertRaisesRegex(ValueError, 'carrier erasure'): + traits.simple_type(ty, self.final) + + def test_slice_impl_rejects_changed_element_and_reference_carrier(self): + annotations = inline.Annotations() + annotations['zerocopy::Marker'] = {'kind': 'trait', 'rust': 'zerocopy::Marker', + 'generics': ['Self'], 'theorem': 'marker', 'predicate': 'Self = Self'} + sliced = {'Untagged': {'Slice': [{'TypeVar': {'Free': 0}}, None]}} + implementation = {'def_id': 2, 'item_meta': meta('zerocopy::SliceMarkerImpl'), + 'impl_trait': {'id': 0, 'generics': args([sliced])}, + 'generics': generics()} + self.final['trait_impls'] = [implementation] + self.before['trait_impls'] = [copy.deepcopy(implementation)] + original = self.before['trait_impls'][0] + original['impl_trait']['generics']['types'][0]['Untagged']['Slice'][0] = { + 'TypeVar': {'Bound': [0, 0]}} + location = {'file': 'src/lib.rs', 'begin_line': 1, 'end_line': 4} + native = {'crate': 'zerocopy', 'charon_version': '0.1.276', + 'aeneas_version': 'nightly-2026.10.01-ca282ec+nominal-tuple-structs.1', + 'trait_decls': [{'def_id': 0, 'lean_name': 'Zerocopy.Marker', + 'rust_name': 'zerocopy::Marker', 'is_local': True, 'source': location}], + 'trait_impls': [{'def_id': 2, 'lean_name': 'Zerocopy.Slice.Insts.Marker', + 'impl_trait_def_id': 0, 'impl_trait_rust_name': 'zerocopy::Marker', + 'is_local': True, 'source': location}]} + with tempfile.TemporaryDirectory() as tmp: + work = Path(tmp); (work / 'Zerocopy').mkdir() + (work / 'Zerocopy/translation.json').write_text(json.dumps(native)) + def bind(): + return traits.bind_laws(annotations, work, self.final, self.before) + self.assertEqual(bind()[1][0]['rust_type'], [['slice', ['parameter', 0]]]) + for changed in ( + {'Untagged': {'Slice': [{'Scalar': 'Bool'}, None]}}, + {'Untagged': {'Ref': [None, sliced, 'Mut']}}): + with self.subTest(carrier=changed): + implementation['impl_trait']['generics']['types'] = [changed] + with self.assertRaises(ValueError): + bind() + def test_native_mapping_requires_complete_exact_dictionary_identity(self): annotations = inline.Annotations() annotations['zerocopy::Marker'] = {'kind': 'trait', 'rust': 'zerocopy::Marker', diff --git a/verification/aeneas/trait_invariants.py b/verification/aeneas/trait_invariants.py index 8f1d0d7d75..5b90f8e2b0 100644 --- a/verification/aeneas/trait_invariants.py +++ b/verification/aeneas/trait_invariants.py @@ -128,6 +128,8 @@ def simple_type(value, crate, bound_depth=0): elif tag == 'Array' and isinstance(body, list) and len(body) == 3 and body[2] is None: return ['array', simple_type(body[0], crate, bound_depth), simple_const(body[1], bound_depth)] + elif tag == 'Slice' and isinstance(body, list) and len(body) == 2 and body[1] is None: + return ['slice', simple_type(body[0], crate, bound_depth)] elif tag == 'Adt' and body.get('builtin') == 'Tuple': if body.get('generics') == {'regions': [], 'types': [], 'const_generics': [], 'trait_refs': []}: diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index 87965aa194..92fb4cc8f7 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -1255,7 +1255,12 @@ const _: () = unsafe { }); unsafe_impl!(T: FromZeros => FromZeros for [T]); unsafe_impl!(T: FromBytes => FromBytes for [T]); - unsafe_impl!(T: IntoBytes => IntoBytes for [T]); + unsafe_impl!( + /// ```aeneas + /// invariant_proof + /// ``` + T: IntoBytes => IntoBytes for [T] + ); unsafe_impl!(T: Unaligned => Unaligned for [T]); }; diff --git a/zerocopy/src/trait_checks.rs b/zerocopy/src/trait_checks.rs index c44519b254..e63be32610 100644 --- a/zerocopy/src/trait_checks.rs +++ b/zerocopy/src/trait_checks.rs @@ -145,7 +145,7 @@ fn forwarded_byte_codec(byte: u8) -> u8 { byte_codec_roundtrip::>(byte) } -fn require_into_bytes() {} +fn require_into_bytes() {} /// Forces extraction of the existing array IntoBytes implementation and its /// primitive and nested dependencies. CI checks the generic implementation law @@ -168,6 +168,24 @@ fn check_array_into_bytes() { require_into_bytes::<[[bool; 2]; 3]>(); } +/// Exercise native slice and unsized-wrapper trait selection. The promise +/// ranges over explicit element counts, including zero-sized elements; it does +/// not grant permission to access a pointer or assert a Rust ABI identity. +/// +/// ```aeneas +/// spec slice_into_bytes_spec +/// 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)) +/// ``` +fn check_slice_into_bytes() { + require_into_bytes::<[bool]>(); + require_into_bytes::<[()]>(); + require_into_bytes::>(); +} + #[cfg(test)] mod tests { use super::*; @@ -185,5 +203,6 @@ mod tests { assert_eq!(forwarded_byte_codec(byte), byte); } check_array_into_bytes(); + check_slice_into_bytes(); } }