diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index e9976c0c69..ba39e32eb6 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -731,20 +731,19 @@ def Array.Insts.ZerocopyIntoBytes {T : Type} (N : Std.Usize) (IntoBytesInst : N IntoBytesInst } -/-- [zerocopy::impls::_::{impl zerocopy::IntoBytes for ()}::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 - Tuple.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +def Bool.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait : Result Unit := do ok () -/-- Trait implementation: [zerocopy::impls::_::{impl zerocopy::IntoBytes for ()}] +/-- Trait implementation: [zerocopy::impls::_#2::{impl zerocopy::IntoBytes for bool}] Source: 'src/util/macros.rs', lines 30:8-32:9 -/ @[reducible] -def Tuple.Insts.ZerocopyIntoBytes : IntoBytes Unit := { +def Bool.Insts.ZerocopyIntoBytes : IntoBytes Bool := { only_derive_is_allowed_to_implement_this_trait := - Tuple.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + Bool.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]: @@ -762,19 +761,20 @@ def U8.Insts.ZerocopyIntoBytes : IntoBytes Std.U8 := { 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]: +/-- [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 Bool.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +def + Tuple.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait : Result Unit := do ok () -/-- Trait implementation: [zerocopy::impls::_#2::{impl zerocopy::IntoBytes for bool}] +/-- Trait implementation: [zerocopy::impls::_::{impl zerocopy::IntoBytes for ()}] Source: 'src/util/macros.rs', lines 30:8-32:9 -/ @[reducible] -def Bool.Insts.ZerocopyIntoBytes : IntoBytes Bool := { +def Tuple.Insts.ZerocopyIntoBytes : IntoBytes Unit := { only_derive_is_allowed_to_implement_this_trait := - Bool.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + Tuple.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait } /-- [zerocopy::trait_checks::check_array_into_bytes]: @@ -791,6 +791,638 @@ 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::_#1::{impl zerocopy::IntoBytes for i8}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def I8.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i8}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def I8.Insts.ZerocopyIntoBytes : IntoBytes Std.I8 := { + only_derive_is_allowed_to_implement_this_trait := + I8.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u16}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u16}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U16.Insts.ZerocopyIntoBytes : IntoBytes Std.U16 := { + only_derive_is_allowed_to_implement_this_trait := + U16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i16}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def I16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i16}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def I16.Insts.ZerocopyIntoBytes : IntoBytes Std.I16 := { + only_derive_is_allowed_to_implement_this_trait := + I16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u32}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U32.Insts.ZerocopyIntoBytes : IntoBytes Std.U32 := { + only_derive_is_allowed_to_implement_this_trait := + U32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def I32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i32}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def I32.Insts.ZerocopyIntoBytes : IntoBytes Std.I32 := { + only_derive_is_allowed_to_implement_this_trait := + I32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u64}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u64}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U64.Insts.ZerocopyIntoBytes : IntoBytes Std.U64 := { + only_derive_is_allowed_to_implement_this_trait := + U64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i64}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def I64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i64}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def I64.Insts.ZerocopyIntoBytes : IntoBytes Std.I64 := { + only_derive_is_allowed_to_implement_this_trait := + I64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u128}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U128.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u128}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U128.Insts.ZerocopyIntoBytes : IntoBytes Std.U128 := { + only_derive_is_allowed_to_implement_this_trait := + U128.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i128}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def I128.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i128}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def I128.Insts.ZerocopyIntoBytes : IntoBytes Std.I128 := { + only_derive_is_allowed_to_implement_this_trait := + I128.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for usize}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + Usize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for usize}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Usize.Insts.ZerocopyIntoBytes : IntoBytes Std.Usize := { + only_derive_is_allowed_to_implement_this_trait := + Usize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for isize}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + Isize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for isize}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Isize.Insts.ZerocopyIntoBytes : IntoBytes Std.Isize := { + only_derive_is_allowed_to_implement_this_trait := + Isize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#4::{impl zerocopy::IntoBytes for char}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def Char.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#4::{impl zerocopy::IntoBytes for char}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Char.Insts.ZerocopyIntoBytes : IntoBytes Char := { + only_derive_is_allowed_to_implement_this_trait := + Char.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.U8 + core.num.niche_types.NonZeroU8Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.I8 + core.num.niche_types.NonZeroI8Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.U16 + core.num.niche_types.NonZeroU16Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.I16 + core.num.niche_types.NonZeroI16Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.U32 + core.num.niche_types.NonZeroU32Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.I32 + core.num.niche_types.NonZeroI32Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.U64 + core.num.niche_types.NonZeroU64Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.I64 + core.num.niche_types.NonZeroI64Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.U128 + core.num.niche_types.NonZeroU128Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.I128 + core.num.niche_types.NonZeroI128Inner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#8::{impl zerocopy::IntoBytes for core::num::nonzero::NonZero}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes : + IntoBytes (core.num.nonzero.NonZero Std.Isize + core.num.niche_types.NonZeroIsizeInner) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.U8 + core.num.niche_types.NonZeroU8Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.I8 + core.num.niche_types.NonZeroI8Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.U16 + core.num.niche_types.NonZeroU16Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.I16 + core.num.niche_types.NonZeroI16Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.U32 + core.num.niche_types.NonZeroU32Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.I32 + core.num.niche_types.NonZeroI32Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.U64 + core.num.niche_types.NonZeroU64Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.I64 + core.num.niche_types.NonZeroI64Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.U128 + core.num.niche_types.NonZeroU128Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.I128 + core.num.niche_types.NonZeroI128Inner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#9::{impl zerocopy::IntoBytes for core::option::Option>}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes : + IntoBytes (Option (core.num.nonzero.NonZero Std.Isize + core.num.niche_types.NonZeroIsizeInner)) := { + only_derive_is_allowed_to_implement_this_trait := + core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#12::{impl zerocopy::IntoBytes for core::marker::PhantomData}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + core.marker.PhantomData.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (T : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#12::{impl zerocopy::IntoBytes for core::marker::PhantomData}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def core.marker.PhantomData.Insts.ZerocopyIntoBytes (T : Type) : IntoBytes + (core.marker.PhantomData T) := { + only_derive_is_allowed_to_implement_this_trait := + core.marker.PhantomData.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + T +} + /-- [zerocopy::util::padding_needed_for]: Source: 'src/util/mod.rs', lines 166:0-226:1 -/ def util.padding_needed_for diff --git a/verification/aeneas/golden/TypesExternal_Template.lean b/verification/aeneas/golden/TypesExternal_Template.lean index eb785fcd09..7e0a757dc9 100644 --- a/verification/aeneas/golden/TypesExternal_Template.lean +++ b/verification/aeneas/golden/TypesExternal_Template.lean @@ -33,6 +33,83 @@ set_option maxRecDepth 2048 @[rust_type "core::num::niche_types::NonZeroUsizeInner"] axiom core.num.niche_types.NonZeroUsizeInner : Type +/-- [core::num::niche_types::NonZeroU8Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroU8Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroU8Inner"] +axiom core.num.niche_types.NonZeroU8Inner : Type + +/-- [core::num::niche_types::NonZeroI8Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroI8Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroI8Inner"] +axiom core.num.niche_types.NonZeroI8Inner : Type + +/-- [core::num::niche_types::NonZeroU16Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroU16Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroU16Inner"] +axiom core.num.niche_types.NonZeroU16Inner : Type + +/-- [core::num::niche_types::NonZeroI16Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroI16Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroI16Inner"] +axiom core.num.niche_types.NonZeroI16Inner : Type + +/-- [core::num::niche_types::NonZeroU32Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroU32Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroU32Inner"] +axiom core.num.niche_types.NonZeroU32Inner : Type + +/-- [core::num::niche_types::NonZeroI32Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroI32Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroI32Inner"] +axiom core.num.niche_types.NonZeroI32Inner : Type + +/-- [core::num::niche_types::NonZeroU64Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroU64Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroU64Inner"] +axiom core.num.niche_types.NonZeroU64Inner : Type + +/-- [core::num::niche_types::NonZeroI64Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroI64Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroI64Inner"] +axiom core.num.niche_types.NonZeroI64Inner : Type + +/-- [core::num::niche_types::NonZeroU128Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroU128Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroU128Inner"] +axiom core.num.niche_types.NonZeroU128Inner : Type + +/-- [core::num::niche_types::NonZeroI128Inner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroI128Inner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroI128Inner"] +axiom core.num.niche_types.NonZeroI128Inner : Type + +/-- [core::num::niche_types::NonZeroIsizeInner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroIsizeInner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroIsizeInner"] +axiom core.num.niche_types.NonZeroIsizeInner : Type + /-- [core::num::nonzero::NonZero] Source: '/rustc/library/core/src/num/nonzero.rs', lines 112:0-112:40 Name pattern: [core::num::nonzero::NonZero] diff --git a/verification/aeneas/lean/Proofs/IntoBytes.lean b/verification/aeneas/lean/Proofs/IntoBytes.lean new file mode 100644 index 0000000000..393b327069 --- /dev/null +++ b/verification/aeneas/lean/Proofs/IntoBytes.lean @@ -0,0 +1,209 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + + +module +public import Specs +public import TraitLaws +public import Proofs.TraitChecks +@[expose] public section + +/-! +Each theorem names the actual extracted implementation dictionary. The final +audit checks its complete generic inputs and rejects additional assumptions. +The shared decoder lemmas supply the representation facts; these declarations +attach those facts to the unsafe impls visible in Rust. They do not assert that +every IntoBytes method body or every compilation configuration is verified. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +@[instance] theorem I8.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized I8 Zerocopy.I8.Insts.ZerocopyIntoBytes := + ⟨initializedIScalar .I8⟩ + +@[instance] theorem U16.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized U16 Zerocopy.U16.Insts.ZerocopyIntoBytes := + ⟨initializedUScalar .U16⟩ + +@[instance] theorem I16.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized I16 Zerocopy.I16.Insts.ZerocopyIntoBytes := + ⟨initializedIScalar .I16⟩ + +@[instance] theorem U32.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized U32 Zerocopy.U32.Insts.ZerocopyIntoBytes := + ⟨initializedUScalar .U32⟩ + +@[instance] theorem I32.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized I32 Zerocopy.I32.Insts.ZerocopyIntoBytes := + ⟨initializedIScalar .I32⟩ + +@[instance] theorem U64.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized U64 Zerocopy.U64.Insts.ZerocopyIntoBytes := + ⟨initializedUScalar .U64⟩ + +@[instance] theorem I64.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized I64 Zerocopy.I64.Insts.ZerocopyIntoBytes := + ⟨initializedIScalar .I64⟩ + +@[instance] theorem U128.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized U128 Zerocopy.U128.Insts.ZerocopyIntoBytes := + ⟨initializedUScalar .U128⟩ + +@[instance] theorem I128.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized I128 Zerocopy.I128.Insts.ZerocopyIntoBytes := + ⟨initializedIScalar .I128⟩ + +@[instance] theorem Usize.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized Usize Zerocopy.Usize.Insts.ZerocopyIntoBytes := + ⟨initializedUScalar .Usize⟩ + +@[instance] theorem Isize.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized Isize Zerocopy.Isize.Insts.ZerocopyIntoBytes := + ⟨initializedIScalar .Isize⟩ + +@[instance] theorem Char.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized Char Zerocopy.Char.Insts.ZerocopyIntoBytes := + ⟨Rust.Storage.BitDecoder.filterMap_initialized _ _ + (Rust.Storage.integerDecoder_initialized 4 .little)⟩ + +-- Zero rejects NonZero construction; for Option it denotes a successfully +-- decoded None. Initialization follows the same full integer carrier. + +@[instance] theorem core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U8 core.num.niche_types.NonZeroU8Inner) + Zerocopy.core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I8 core.num.niche_types.NonZeroI8Inner) + Zerocopy.core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U16 core.num.niche_types.NonZeroU16Inner) + Zerocopy.core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I16 core.num.niche_types.NonZeroI16Inner) + Zerocopy.core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U32 core.num.niche_types.NonZeroU32Inner) + Zerocopy.core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I32 core.num.niche_types.NonZeroI32Inner) + Zerocopy.core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U64 core.num.niche_types.NonZeroU64Inner) + Zerocopy.core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I64 core.num.niche_types.NonZeroI64Inner) + Zerocopy.core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U128 core.num.niche_types.NonZeroU128Inner) + Zerocopy.core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I128 core.num.niche_types.NonZeroI128Inner) + Zerocopy.core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩ + +@[instance] theorem core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner) + Zerocopy.core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩ + +@[instance] theorem core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero Isize core.num.niche_types.NonZeroIsizeInner) + Zerocopy.core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes := + ⟨initializedNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩ + +-- Zero rejects NonZero construction; for Option it denotes a successfully +-- decoded None. Initialization follows the same full integer carrier. + +@[instance] theorem core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U8 core.num.niche_types.NonZeroU8Inner)) + Zerocopy.core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩ + +@[instance] theorem core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I8 core.num.niche_types.NonZeroI8Inner)) + Zerocopy.core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩ + +@[instance] theorem core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U16 core.num.niche_types.NonZeroU16Inner)) + Zerocopy.core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩ + +@[instance] theorem core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I16 core.num.niche_types.NonZeroI16Inner)) + Zerocopy.core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩ + +@[instance] theorem core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U32 core.num.niche_types.NonZeroU32Inner)) + Zerocopy.core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩ + +@[instance] theorem core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I32 core.num.niche_types.NonZeroI32Inner)) + Zerocopy.core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩ + +@[instance] theorem core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U64 core.num.niche_types.NonZeroU64Inner)) + Zerocopy.core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩ + +@[instance] theorem core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I64 core.num.niche_types.NonZeroI64Inner)) + Zerocopy.core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩ + +@[instance] theorem core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U128 core.num.niche_types.NonZeroU128Inner)) + Zerocopy.core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩ + +@[instance] theorem core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I128 core.num.niche_types.NonZeroI128Inner)) + Zerocopy.core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩ + +@[instance] theorem core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner)) + Zerocopy.core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩ + +@[instance] theorem core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero Isize core.num.niche_types.NonZeroIsizeInner)) + Zerocopy.core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes := + ⟨initializedOptionNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩ + +-- No value of T is stored in PhantomData, so this law needs no model or +-- trait promise for T, including when T is uninhabited. +@[instance] theorem core.marker.PhantomData.Insts.ZerocopyIntoBytes_law (T : Type) : + TraitLaws.into_bytes_initialized (Zerocopy.core.marker.PhantomData T) + (Zerocopy.core.marker.PhantomData.Insts.ZerocopyIntoBytes T) := + ⟨Rust.Storage.emptyDecoder_initialized _⟩ + +end Zerocopy.Proofs diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index 5912f1835f..3f6c672b24 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -29,7 +29,13 @@ use crate::pointer::cast::{CastSizedExact, CastUnsized}; // [1] https://doc.rust-lang.org/1.81.0/reference/type-layout.html#tuple-layout #[allow(clippy::multiple_unsafe_ops_per_block)] const _: () = unsafe { - unsafe_impl!((): Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes, Unaligned); + unsafe_impl!( + (): Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, Unaligned, + ); assert_unaligned!(()); }; @@ -65,19 +71,91 @@ const _: () = unsafe { // bits or bytes, update this comment, especially the reference to [1]. #[allow(clippy::multiple_unsafe_ops_per_block)] const _: () = unsafe { - unsafe_impl!(u8: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes, Unaligned); - unsafe_impl!(i8: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes, Unaligned); + unsafe_impl!( + u8: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, Unaligned, + ); + unsafe_impl!( + i8: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, Unaligned, + ); assert_unaligned!(u8, i8); - unsafe_impl!(u16: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(i16: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(u32: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(i32: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(u64: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(i64: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(u128: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(i128: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(usize: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(isize: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); + unsafe_impl!( + u16: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + i16: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + u32: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + i32: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + u64: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + i64: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + u128: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + i128: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + usize: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + isize: Immutable, TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); unsafe_impl!(f32: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); unsafe_impl!(f64: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); #[cfg(feature = "float-nightly")] @@ -98,7 +176,15 @@ const _: () = unsafe { // // [1] https://doc.rust-lang.org/1.81.0/reference/types/boolean.html #[allow(clippy::multiple_unsafe_ops_per_block)] -const _: () = unsafe { unsafe_impl!(bool: Immutable, FromZeros, IntoBytes, Unaligned) }; +const _: () = unsafe { + unsafe_impl!( + bool: Immutable, FromZeros, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, Unaligned, + ); +}; assert_unaligned!(bool); // SAFETY: The impl must only return `true` for its argument if the original @@ -128,7 +214,15 @@ const _: () = unsafe { // // [1] https://doc.rust-lang.org/1.81.0/reference/types/textual.html #[allow(clippy::multiple_unsafe_ops_per_block)] -const _: () = unsafe { unsafe_impl!(char: Immutable, FromZeros, IntoBytes) }; +const _: () = unsafe { + unsafe_impl!( + char: Immutable, FromZeros, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); +}; // SAFETY: The impl must only return `true` for its argument if the original // `Maybe` refers to a valid `char`. `char::from_u32` guarantees that it @@ -224,19 +318,91 @@ macro_rules! unsafe_impl_try_from_bytes_for_nonzero { // the exception that 0 is not a valid instance. #[allow(clippy::multiple_unsafe_ops_per_block)] const _: () = unsafe { - unsafe_impl!(NonZeroU8: Immutable, IntoBytes, Unaligned); - unsafe_impl!(NonZeroI8: Immutable, IntoBytes, Unaligned); + unsafe_impl!( + NonZeroU8: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, Unaligned, + ); + unsafe_impl!( + NonZeroI8: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, Unaligned, + ); assert_unaligned!(NonZeroU8, NonZeroI8); - unsafe_impl!(NonZeroU16: Immutable, IntoBytes); - unsafe_impl!(NonZeroI16: Immutable, IntoBytes); - unsafe_impl!(NonZeroU32: Immutable, IntoBytes); - unsafe_impl!(NonZeroI32: Immutable, IntoBytes); - unsafe_impl!(NonZeroU64: Immutable, IntoBytes); - unsafe_impl!(NonZeroI64: Immutable, IntoBytes); - unsafe_impl!(NonZeroU128: Immutable, IntoBytes); - unsafe_impl!(NonZeroI128: Immutable, IntoBytes); - unsafe_impl!(NonZeroUsize: Immutable, IntoBytes); - unsafe_impl!(NonZeroIsize: Immutable, IntoBytes); + unsafe_impl!( + NonZeroU16: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroI16: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroU32: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroI32: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroU64: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroI64: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroU128: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroI128: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroUsize: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + NonZeroIsize: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); unsafe_impl_try_from_bytes_for_nonzero!( NonZeroU8[u8], NonZeroI8[i8], @@ -279,19 +445,91 @@ const _: () = unsafe { // are guaranteed to have the same size and alignment: #[allow(clippy::multiple_unsafe_ops_per_block)] const _: () = unsafe { - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes, Unaligned); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes, Unaligned); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, Unaligned, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, Unaligned, + ); assert_unaligned!(Option, Option); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); - unsafe_impl!(Option: TryFromBytes, FromZeros, FromBytes, IntoBytes); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); + unsafe_impl!( + Option: TryFromBytes, FromZeros, FromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + IntoBytes, + ); }; // SAFETY: While it's not fully documented, the consensus is that `Box` does @@ -655,7 +893,12 @@ const _: () = unsafe { unsafe_impl!(T: ?Sized => TryFromBytes for PhantomData); unsafe_impl!(T: ?Sized => FromZeros for PhantomData); unsafe_impl!(T: ?Sized => FromBytes for PhantomData); - unsafe_impl!(T: ?Sized => IntoBytes for PhantomData); + unsafe_impl!( + /// ```aeneas + /// invariant_proof + /// ``` + T: ?Sized => IntoBytes for PhantomData + ); unsafe_impl!(T: ?Sized => Unaligned for PhantomData); assert_unaligned!(PhantomData<()>, PhantomData, PhantomData); }; diff --git a/zerocopy/tests/ui/transmute-ptr-to-usize.nightly.stderr b/zerocopy/tests/ui/transmute-ptr-to-usize.nightly.stderr index 4cb3c7aeaa..a9012843bf 100644 --- a/zerocopy/tests/ui/transmute-ptr-to-usize.nightly.stderr +++ b/zerocopy/tests/ui/transmute-ptr-to-usize.nightly.stderr @@ -11,13 +11,19 @@ error[E0277]: the trait bound `*const usize: IntoBytes` is not satisfied help: the trait `IntoBytes` is implemented for `usize` --> src/util/macros.rs:30:9 | - 30 | unsafe impl $trait for $ty { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^ - | - ::: src/impls.rs:79:5 - | - 79 | unsafe_impl!(usize: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - | ----------------------------------------------------------------------------- in this macro invocation + 30 | unsafe impl $trait for $ty { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + | + ::: src/impls.rs:145:5 + | +145 | / unsafe_impl!( +146 | | usize: Immutable, TryFromBytes, FromZeros, FromBytes, +147 | | /// ```aeneas +148 | | /// invariant_proof +149 | | /// ``` +150 | | IntoBytes, +151 | | ); + | |_____- in this macro invocation note: required by a bound in `POINTER_VALUE::transmute` --> $DIR/transmute-ptr-to-usize.rs:21:30 | diff --git a/zerocopy/tests/ui/transmute-ptr-to-usize.stable.stderr b/zerocopy/tests/ui/transmute-ptr-to-usize.stable.stderr index 7cf3cfa8be..716d42e339 100644 --- a/zerocopy/tests/ui/transmute-ptr-to-usize.stable.stderr +++ b/zerocopy/tests/ui/transmute-ptr-to-usize.stable.stderr @@ -1,32 +1,38 @@ error[E0277]: the trait bound `*const usize: IntoBytes` is not satisfied - --> $DIR/transmute-ptr-to-usize.rs:21:30 - | -21 | const POINTER_VALUE: usize = transmute!(&0usize as *const usize); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | | - | the trait `IntoBytes` is not implemented for `*const usize` - | required by a bound introduced by this call - | - = note: Consider adding `#[derive(IntoBytes)]` to `*const usize` + --> $DIR/transmute-ptr-to-usize.rs:21:30 + | + 21 | const POINTER_VALUE: usize = transmute!(&0usize as *const usize); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | | + | the trait `IntoBytes` is not implemented for `*const usize` + | required by a bound introduced by this call + | + = note: Consider adding `#[derive(IntoBytes)]` to `*const usize` help: the trait `IntoBytes` is implemented for `usize` - --> src/util/macros.rs:30:9 - | -30 | unsafe impl $trait for $ty { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^ - | - ::: src/impls.rs:79:5 - | -79 | unsafe_impl!(usize: Immutable, TryFromBytes, FromZeros, FromBytes, IntoBytes); - | ----------------------------------------------------------------------------- in this macro invocation + --> src/util/macros.rs:30:9 + | + 30 | unsafe impl $trait for $ty { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + | + ::: src/impls.rs:145:5 + | +145 | / unsafe_impl!( +146 | | usize: Immutable, TryFromBytes, FromZeros, FromBytes, +147 | | /// ```aeneas +148 | | /// invariant_proof +149 | | /// ``` +150 | | IntoBytes, +151 | | ); + | |_____- in this macro invocation note: required by a bound in `POINTER_VALUE::transmute` - --> $DIR/transmute-ptr-to-usize.rs:21:30 - | -21 | const POINTER_VALUE: usize = transmute!(&0usize as *const usize); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | | - | required by a bound in this function - | required by this bound in `transmute` - = note: this error originates in the macro `transmute` (in Nightly builds, run with -Z macro-backtrace for more info) + --> $DIR/transmute-ptr-to-usize.rs:21:30 + | + 21 | const POINTER_VALUE: usize = transmute!(&0usize as *const usize); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | | + | required by a bound in this function + | required by this bound in `transmute` + = note: this error originates in the macro `transmute` (in Nightly builds, run with -Z macro-backtrace for more info) error: aborting due to 1 previous error