From 1bf2c3f21353a613d2520a766c2a548c11edb198 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 14 Oct 2026 13:46:22 -0400 Subject: [PATCH] Prove scalar and PhantomData IntoBytes implementations IntoBytes promises that every language-valid representation is fully initialized. Attach nameless invariant_proof markers to the existing integer, character, nonzero, niche-option and PhantomData impl sites, then prove each exact extracted dictionary using the shared decoder laws. Together with the existing unit, bool and array proofs, this covers 41 local impls without assuming a library decoder accepts their values. Nonzero decoding rejects zero. Option> instead maps the full integer domain, making zero a valid None while keeping uninitialized storage a decoding failure. PhantomData supplies its own empty constructor and requires neither a value nor a model of its generic parameter. The complete generic dictionary audit and both independent model builds require these ordinary Lean witnesses. Their interpretation remains conditional on the documented Rust representation correspondence. gherrit-pr-id: Gfvteq5ybeueoxbb3izeqov7vsweunep Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/golden/Funs.lean | 654 +++++++++++++++++- .../aeneas/golden/TypesExternal_Template.lean | 77 +++ .../aeneas/lean/Proofs/IntoBytes.lean | 209 ++++++ zerocopy/src/impls.rs | 323 +++++++-- .../ui/transmute-ptr-to-usize.nightly.stderr | 20 +- .../ui/transmute-ptr-to-usize.stable.stderr | 58 +- 6 files changed, 1257 insertions(+), 84 deletions(-) create mode 100644 verification/aeneas/lean/Proofs/IntoBytes.lean 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