diff --git a/verification/aeneas/DESIGN.md b/verification/aeneas/DESIGN.md index b1b28560ae..e990b8aa8c 100644 --- a/verification/aeneas/DESIGN.md +++ b/verification/aeneas/DESIGN.md @@ -414,11 +414,12 @@ parallel coverage registry or automatic Rust ABI assumptions. - **Broader carriers and effects.** Recursive nominal groups, general indexed carriers, const generics, associated-type trait laws, higher-ranked bounds, bounded nominal models, and escaping borrow reconstruction remain unsupported with - explicit errors. The first trait-law bridge supports `Self`-only traits and - simple generic bounds, with `Unaligned` and a total byte codec as checked - examples. Add semantics and admission checks before accepting - them. Stateful or nondeterministic APIs may need observable traces and - effects, rather than only result contracts. + explicit errors. The trait-law bridge supports type-parameterized traits + and type-only bounds, preserving every original argument and native + dictionary. `TransmuteFrom` exercises four ordered type arguments and + generic state-model providers. Add semantics and admission checks before + accepting the remaining carriers. Stateful or nondeterministic APIs may need + observable traces and effects, rather than only result contracts. - **Abstract storage and bit validity.** Check byte-to-value production before entering Aeneas's typed value domain; rejection must remain a forbidden execution, independently of ordinary library-model admission. A storage model @@ -471,3 +472,22 @@ The generic-field staging problem and copy-back gap are resolved. Model proof completion is scoped to decoder construction rather than defaults attached to the model declaration. Encoders, losslessness, and representation certificates remain optional properties justified by particular operation proofs. + +## Referent contents: implemented scope + +The shared `Rust.Referent` algebra covers uninitialized, initialized, and safe +byte domains, including empty safe domains. The zerocopy adapter uses the +retained physical and mathematical decoders. Validity markers carry optional +type-level codes, checked against their actual `Validity::KIND` dictionaries. +This uses the existing model-provider binding and audit; it adds no separate +state-dictionary inference mechanism. + +Marked `TransmuteFrom` blanket impls, ordinary wrapper pairs, and the two +`Cell`/`UnsafeCell` chains have checked native law proofs. `CastableFrom` retains +its exact two identity pairs. Generic clients consume those laws, while +independent outcome families state the actual byte implications. Execution +success remains outside any conditional interpretation of a validity state. + +`AsInitialized` contents and opaque `MaybeUninit` storage remain deferred. +Pointer casts and projections will additionally need explicit byte-range, +metadata, access, and resource arguments. These content laws do not grant them. diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 91f3ef3550..0e3be3be3c 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -533,10 +533,12 @@ admitted implementation method body in the original and final ASTs, even when only the law refers to the method. Excluded provided methods cannot execute; interface-only validators retain their required signatures but cannot be called. -This initial bridge accepts traits with only their `Self` parameter and simple -generic bounds. It compares compiler-resolved original and final type -applications, rather than matching clause ordinals. Associated types, higher -ranked bounds, transformed carrier identities, and bounds on nominal model +The bridge accepts type-parameterized traits and type-only bounds, including +`?Sized`. It preserves the complete ordered application: `Self` and every other +Rust type argument. Source syntax records bound arity; compiler identities +resolve the arguments. Original and final applications must agree, including +repeated arguments, rather than merely matching clause ordinals. Associated +types, higher ranked bounds, transformed carrier identities, and bounds on nominal model definitions fail closed. The compiled audit independently enumerates implementation dictionaries and requires the same complete set of proof obligations. Omitting or swapping a @@ -1325,3 +1327,42 @@ size guard, providers, trait premises, and destination admission. The exact [semantic scope and Rust premises](SEMANTICS.md#generic-owned-conversion-through-transmute_copy) exclude pointer provenance, resource ownership, meaningful destructor execution, and general storage-copy effects. The production `transmute!` macro is unchanged. + +## Referent validity implications + +`Rust.Referent` in `anneal/lean` describes three byte-content promises at an +explicit width: `Uninit` permits any contents, `Initialized` requires initialized +bytes, and `Safe` requires successful physical and mathematical decoding. An +uninhabited type can have an empty safe domain. No default value, inhabitedness, +unique representation, or canonical encoding is required. + +The `TransmuteFrom` annotation in `pointer/transmute.rs` checks directional +inclusion of these domains when widths agree. Four blanket impls use the +existing `IntoBytes` and `FromBytes` laws or weaken the content promise. Twelve +wrapper directions compare the actual mapped physical decoder and its retained +mathematical decoder. The two `Cell`/`UnsafeCell` chains use those same domain +equivalences. `CastableFrom` has a separate, exact invariant: both states are +`Uninit`, or both are `Initialized`. + +The four empty validity-marker types retain their empty extracted carriers. +Their generated model providers carry an optional type-level code; the +`Validity` law checks that code against the actual `KIND` constant. Missing code +metadata rejects the law. The code identifies `AsInitialized` but supplies no +interpretation of its contents. Forgetting any state to `Uninit` remains valid +without that interpretation. + +`pointer/referent_checks.rs` consumes the actual Rust bounds, including unused +bounds, and selects concrete blanket and wrapper dictionaries. Its generic +composition test requires equal source and intermediate widths. Without that +premise, two transfers could hold only because their individual width guards +are false. Independent required contracts restate the byte implications and +require successful execution even when no modeled state matches a marker. +Both golden and live builds check every marked impl and discovered spec. + +These are conditional facts about contents. Applying them to Rust requires the +installed physical decoder and mathematical model to describe that referent. +A missing physical decoder supplies no view from which to reason; it is not an +empty safe domain. Pointer access, provenance, aliasing, mutation permissions, +and external resources remain separate obligations. The pinned extractor gives +`MaybeUninit` an opaque carrier without a byte-storage interpretation, so +its transitive wrapper impls remain unmarked and deferred. diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md index 6dc550492e..14cad8b966 100644 --- a/verification/aeneas/SEMANTICS.md +++ b/verification/aeneas/SEMANTICS.md @@ -322,3 +322,23 @@ and [`transmute_copy` documentation](https://doc.rust-lang.org/1.74.0/core/mem/f The numeric, resource-free representation profiles remain the supported domain; this proof does not admit arbitrary downstream representations merely because a trait dictionary can be extracted. + +## Referent-content boundary + +`Rust.Referent.Allowed` combines an explicit byte width with a content promise. +`Safe` requires a raw value from physical decoding and a mathematical value +from that same retained model's decoder. An empty safe domain makes a +safe-source implication vacuous without constructing an impossible value. +Completeness in the other direction still requires an actual decoded result. + +`TransmuteFrom` is conditional on equal widths. Its composition theorem also +requires the intermediate width to agree; outer equality alone is insufficient. +Transparent-wrapper proofs compare both decoding stages, so equal layout alone +cannot erase a library invariant. `CastableFrom` states its two permitted type +identity pairs directly, rather than accepting coincidentally equal safe domains. + +The type-level validity codes identify the four empty Rust markers and agree +with their actual associated constants. They do not inhabit the marker types +or interpret `AsInitialized`. The resource-free numeric representation premise +still governs application to Rust; these laws provide no permission to access +or mutate memory. Opaque `MaybeUninit` has no admitted storage model here. diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index c36ccf7fde..ffb883540c 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -3238,8 +3238,127 @@ def pointer_metadata_usize_size_for_metadata native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do core.mem.zeroed Self +/-- Trait implementation: [zerocopy::pointer::invariant::sealed::{impl zerocopy::pointer::invariant::sealed::Sealed for zerocopy::pointer::invariant::Uninit}] + Source: 'src/pointer/invariant.rs', lines 333:4-333:29 -/ +@[reducible] +def pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantSealedSealed : + pointer.invariant.sealed.Sealed pointer.invariant.Uninit := { +} + +/-- [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::Validity for zerocopy::pointer::invariant::Uninit}::KIND] + Source: 'src/pointer/invariant.rs', lines 198:4-198:52 + Visibility: public -/ +@[global_simps, irreducible] +def pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantValidity.KIND + : pointer.invariant.ValidityKind := + pointer.invariant.ValidityKind.Uninit + +/-- Trait implementation: [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::Validity for zerocopy::pointer::invariant::Uninit}] + Source: 'src/pointer/invariant.rs', lines 197:0-199:1 -/ +@[reducible] +def pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantValidity : + pointer.invariant.Validity pointer.invariant.Uninit := { + KIND := ok + pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantValidity.KIND + sealedSealedInst := + pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantSealedSealed +} + +/-- Trait implementation: [zerocopy::pointer::invariant::sealed::{impl zerocopy::pointer::invariant::sealed::Sealed for zerocopy::pointer::invariant::AsInitialized}] + Source: 'src/pointer/invariant.rs', lines 334:4-334:36 -/ +@[reducible] +def pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantSealedSealed + : pointer.invariant.sealed.Sealed pointer.invariant.AsInitialized := { +} + +/-- [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::Validity for zerocopy::pointer::invariant::AsInitialized}::KIND] + Source: 'src/pointer/invariant.rs', lines 235:4-235:59 + Visibility: public -/ +@[global_simps, irreducible] +def pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantValidity.KIND + : pointer.invariant.ValidityKind := + pointer.invariant.ValidityKind.AsInitialized + +/-- Trait implementation: [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::Validity for zerocopy::pointer::invariant::AsInitialized}] + Source: 'src/pointer/invariant.rs', lines 234:0-236:1 -/ +@[reducible] +def pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantValidity : + pointer.invariant.Validity pointer.invariant.AsInitialized := { + KIND := ok + pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantValidity.KIND + sealedSealedInst := + pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantSealedSealed +} + +/-- Trait implementation: [zerocopy::pointer::invariant::sealed::{impl zerocopy::pointer::invariant::sealed::Sealed for zerocopy::pointer::invariant::Initialized}] + Source: 'src/pointer/invariant.rs', lines 335:4-335:34 -/ +@[reducible] +def pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantSealedSealed : + pointer.invariant.sealed.Sealed pointer.invariant.Initialized := { +} + +/-- [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::Validity for zerocopy::pointer::invariant::Initialized}::KIND] + Source: 'src/pointer/invariant.rs', lines 249:4-249:57 + Visibility: public -/ +@[global_simps, irreducible] +def pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity.KIND + : pointer.invariant.ValidityKind := + pointer.invariant.ValidityKind.Initialized + +/-- Trait implementation: [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::Validity for zerocopy::pointer::invariant::Initialized}] + Source: 'src/pointer/invariant.rs', lines 248:0-250:1 -/ +@[reducible] +def pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity : + pointer.invariant.Validity pointer.invariant.Initialized := { + KIND := ok + pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity.KIND + sealedSealedInst := + pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantSealedSealed +} + +/-- Trait implementation: [zerocopy::pointer::invariant::sealed::{impl zerocopy::pointer::invariant::sealed::Sealed for zerocopy::pointer::invariant::Safe}] + Source: 'src/pointer/invariant.rs', lines 336:4-336:27 -/ +@[reducible] +def pointer.invariant.Safe.Insts.ZerocopyPointerInvariantSealedSealed : + pointer.invariant.sealed.Sealed pointer.invariant.Safe := { +} + +/-- [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::Validity for zerocopy::pointer::invariant::Safe}::KIND] + Source: 'src/pointer/invariant.rs', lines 261:4-261:50 + Visibility: public -/ +@[global_simps, irreducible] +def pointer.invariant.Safe.Insts.ZerocopyPointerInvariantValidity.KIND + : pointer.invariant.ValidityKind := + pointer.invariant.ValidityKind.Safe + +/-- Trait implementation: [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::Validity for zerocopy::pointer::invariant::Safe}] + Source: 'src/pointer/invariant.rs', lines 260:0-262:1 -/ +@[reducible] +def pointer.invariant.Safe.Insts.ZerocopyPointerInvariantValidity : + pointer.invariant.Validity pointer.invariant.Safe := { + KIND := ok pointer.invariant.Safe.Insts.ZerocopyPointerInvariantValidity.KIND + sealedSealedInst := + pointer.invariant.Safe.Insts.ZerocopyPointerInvariantSealedSealed +} + +/-- Trait implementation: [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::CastableFrom for DT}] + Source: 'src/pointer/invariant.rs', lines 285:0-285:78 -/ +@[reducible] +def pointer.invariant.CastableFromDTSTUninitUninit.Blanket (ST : Type) (DT : + Type) : pointer.invariant.CastableFrom DT ST pointer.invariant.Uninit + pointer.invariant.Uninit := { +} + +/-- Trait implementation: [zerocopy::pointer::invariant::{impl zerocopy::pointer::invariant::CastableFrom for DT}] + Source: 'src/pointer/invariant.rs', lines 290:0-290:88 -/ +@[reducible] +def pointer.invariant.CastableFromDTSTInitializedInitialized.Blanket (ST : + Type) (DT : Type) : pointer.invariant.CastableFrom DT ST + pointer.invariant.Initialized pointer.invariant.Initialized := { +} + /-- [zerocopy::pointer::cast::cast_unsized_layouts_match]: - Source: 'src/pointer/mod.rs', lines 195:4-207:5 -/ + Source: 'src/pointer/mod.rs', lines 196:4-208:5 -/ def pointer.cast.cast_unsized_layouts_match (src : layout.DstLayout) (dst : layout.DstLayout) : Result Bool := do match src.size_info with @@ -3269,7 +3388,7 @@ def pointer.cast.cast_unsized_layouts_match else ok false /-- [zerocopy::pointer::cast::checks::witness_matches]: - Source: 'src/pointer/mod.rs', lines 218:8-225:9 -/ + Source: 'src/pointer/mod.rs', lines 219:8-226:9 -/ def pointer.cast.checks.witness_matches (runtime_layout : layout.DstLayout) (align : core.num.nonzero.NonZero Std.Usize @@ -3282,7 +3401,7 @@ def pointer.cast.checks.witness_matches layout.tail_transform_checks.witness_matches tail align phase /-- [zerocopy::pointer::cast::checks::reference_size]: - Source: 'src/pointer/mod.rs', lines 227:8-239:9 -/ + Source: 'src/pointer/mod.rs', lines 228:8-240:9 -/ def pointer.cast.checks.reference_size (runtime_layout : layout.DstLayout) (align : core.num.nonzero.NonZero Std.Usize @@ -3296,7 +3415,7 @@ def pointer.cast.checks.reference_size layout.tail_checks.reference_size tail align phase metadata /-- [zerocopy::pointer::cast::checks::assert_cast_unsized]: - Source: 'src/pointer/mod.rs', lines 251:8-276:9 -/ + Source: 'src/pointer/mod.rs', lines 252:8-277:9 -/ def pointer.cast.checks.assert_cast_unsized (src : layout.DstLayout) (dst : layout.DstLayout) (src_align : core.num.nonzero.NonZero Std.Usize @@ -3341,6 +3460,267 @@ def pointer.cast.checks.assert_cast_unsized else ok () else ok () +/-- [zerocopy::pointer::referent_checks::require_transfer]: + Source: 'src/pointer/referent_checks.rs', lines 27:0-31:1 -/ +def pointer.referent_checks.require_transfer + {Src : Type} {Dst : Type} {SV : Type} {DV : Type} (transmuteTransmuteFromInst + : pointer.transmute.TransmuteFrom Dst Src SV DV) : + Result Unit + := do + ok () + +/-- [zerocopy::pointer::referent_checks::require_type_independent]: + Source: 'src/pointer/referent_checks.rs', lines 37:0-41:1 -/ +def pointer.referent_checks.require_type_independent + {Src : Type} {Dst : Type} {SV : Type} {DV : Type} (invariantCastableFromInst + : pointer.invariant.CastableFrom Dst Src SV DV) : + Result Unit + := do + ok () + +/-- [zerocopy::pointer::referent_checks::compose_safe_transfers]: + Source: 'src/pointer/referent_checks.rs', lines 52:0-57:1 -/ +def pointer.referent_checks.compose_safe_transfers + {Src : Type} {Mid : Type} {Dst : Type} + (transmuteTransmuteFromMidSrcSafeSafeInst : pointer.transmute.TransmuteFrom + Mid Src pointer.invariant.Safe pointer.invariant.Safe) + (transmuteTransmuteFromDstMidSafeSafeInst : pointer.transmute.TransmuteFrom + Dst Mid pointer.invariant.Safe pointer.invariant.Safe) : + Result Unit + := do + ok () + +/-- [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 Bool.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#2::{impl zerocopy::IntoBytes for bool}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Bool.Insts.ZerocopyIntoBytes : IntoBytes Bool := { + only_derive_is_allowed_to_implement_this_trait := + Bool.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::FromBytes 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.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- [zerocopy::impls::_#1::{impl zerocopy::FromZeros 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.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 153:8-153:62 + Visibility: public -/ +def + U32.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U32.Insts.ZerocopyTryFromBytes : TryFromBytes Std.U32 := { + only_derive_is_allowed_to_implement_this_trait := + U32.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + is_safe := fun {A : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment A) => U32.Insts.ZerocopyTryFromBytes.is_safe + pointerinvariantAlignmentInst +} + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::FromZeros for u32}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U32.Insts.ZerocopyFromZeros : FromZeros Std.U32 := { + TryFromBytesInst := U32.Insts.ZerocopyTryFromBytes + only_derive_is_allowed_to_implement_this_trait := + U32.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + new_zeroed := FromZeros.new_zeroed.default Std.U32 +} + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::FromBytes for u32}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U32.Insts.ZerocopyFromBytes : FromBytes Std.U32 := { + FromZerosInst := U32.Insts.ZerocopyFromZeros + only_derive_is_allowed_to_implement_this_trait := + U32.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom, zerocopy::pointer::invariant::Safe, zerocopy::pointer::invariant::Safe> for T}] + Source: 'src/pointer/transmute.rs', lines 449:0-449:74 -/ +@[reducible] +def pointer.transmute.TransmuteFromTManuallyDropSafeSafe.Blanket (T : Type) : + pointer.transmute.TransmuteFrom T (core.mem.manually_drop.ManuallyDrop T) + pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for Dst}] + Source: 'src/pointer/transmute.rs', lines 423:0-429:1 -/ +@[reducible] +def pointer.transmute.TransmuteFromDstSrcVUninit.Blanket (Src : Type) (Dst : + Type) {V : Type} (invariantValidityInst : pointer.invariant.Validity V) : + pointer.transmute.TransmuteFrom Dst Src V pointer.invariant.Uninit := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for Dst}] + Source: 'src/pointer/transmute.rs', lines 389:0-394:1 -/ +@[reducible] +def pointer.transmute.TransmuteFromDstSrcInitializedSafe.Blanket (Src : Type) + {Dst : Type} (FromBytesInst : FromBytes Dst) : + pointer.transmute.TransmuteFrom Dst Src pointer.invariant.Initialized + pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for Dst}] + Source: 'src/pointer/transmute.rs', lines 376:0-381:1 -/ +@[reducible] +def pointer.transmute.TransmuteFromDstSrcSafeInitialized.Blanket {Src : Type} + (Dst : Type) (IntoBytesInst : IntoBytes Src) : + pointer.transmute.TransmuteFrom Dst Src pointer.invariant.Safe + pointer.invariant.Initialized := { +} + +/-- [zerocopy::pointer::referent_checks::concrete_transfers]: + Source: 'src/pointer/referent_checks.rs', lines 72:0-79:1 -/ +def pointer.referent_checks.concrete_transfers : Result Unit := do + pointer.referent_checks.require_transfer + (pointer.transmute.TransmuteFromDstSrcSafeInitialized.Blanket Std.U8 + Bool.Insts.ZerocopyIntoBytes) + pointer.referent_checks.require_transfer + (pointer.transmute.TransmuteFromDstSrcInitializedSafe.Blanket (Array Std.U8 + 4#usize) U32.Insts.ZerocopyFromBytes) + pointer.referent_checks.require_transfer + (pointer.transmute.TransmuteFromDstSrcVUninit.Blanket Std.U8 Bool + pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity) + pointer.referent_checks.require_transfer + (pointer.transmute.TransmuteFromTManuallyDropSafeSafe.Blanket Std.U8) + pointer.referent_checks.require_type_independent + (pointer.invariant.CastableFromDTSTInitializedInitialized.Blanket Std.U8 + Bool) + pointer.referent_checks.require_type_independent + (pointer.invariant.CastableFromDTSTUninitUninit.Blanket Bool Std.U32) + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for Dst}] + Source: 'src/pointer/transmute.rs', lines 406:0-411:1 -/ +@[reducible] +def pointer.transmute.TransmuteFromDstSrcInitializedInitialized.Blanket (Src : + Type) (Dst : Type) : pointer.transmute.TransmuteFrom Dst Src + pointer.invariant.Initialized pointer.invariant.Initialized := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for core::mem::manually_drop::ManuallyDrop}] + Source: 'src/pointer/transmute.rs', lines 442:0-442:74 -/ +@[reducible] +def + core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe + (T : Type) : pointer.transmute.TransmuteFrom + (core.mem.manually_drop.ManuallyDrop T) T pointer.invariant.Safe + pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for zerocopy::wrappers::Unalign}] + Source: 'src/pointer/transmute.rs', lines 463:0-463:61 -/ +@[reducible] +def wrappers.Unalign.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe (T : + Type) : pointer.transmute.TransmuteFrom (wrappers.Unalign T) T + pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom, zerocopy::pointer::invariant::Safe, zerocopy::pointer::invariant::Safe> for T}] + Source: 'src/pointer/transmute.rs', lines 470:0-470:61 -/ +@[reducible] +def pointer.transmute.TransmuteFromTUnalignSafeSafe.Blanket (T : Type) : + pointer.transmute.TransmuteFrom T (wrappers.Unalign T) pointer.invariant.Safe + pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for core::num::wrapping::Wrapping}] + Source: 'src/pointer/transmute.rs', lines 510:0-510:62 -/ +@[reducible] +def + core.num.wrapping.Wrapping.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe + (T : Type) : pointer.transmute.TransmuteFrom (core.num.wrapping.Wrapping T) T + pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom, zerocopy::pointer::invariant::Safe, zerocopy::pointer::invariant::Safe> for T}] + Source: 'src/pointer/transmute.rs', lines 517:0-517:62 -/ +@[reducible] +def pointer.transmute.TransmuteFromTWrappingSafeSafe.Blanket (T : Type) : + pointer.transmute.TransmuteFrom T (core.num.wrapping.Wrapping T) + pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for core::cell::UnsafeCell}] + Source: 'src/pointer/transmute.rs', lines 546:0-546:72 -/ +@[reducible] +def core.cell.UnsafeCell.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe + (T : Type) : pointer.transmute.TransmuteFrom (core.cell.UnsafeCell T) T + pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom, zerocopy::pointer::invariant::Safe, zerocopy::pointer::invariant::Safe> for T}] + Source: 'src/pointer/transmute.rs', lines 553:0-553:72 -/ +@[reducible] +def pointer.transmute.TransmuteFromTUnsafeCellSafeSafe.Blanket (T : Type) : + pointer.transmute.TransmuteFrom T (core.cell.UnsafeCell T) + pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom for core::cell::Cell}] + Source: 'src/pointer/transmute.rs', lines 583:0-583:66 -/ +@[reducible] +def core.cell.Cell.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe (T : + Type) : pointer.transmute.TransmuteFrom (core.cell.Cell T) T + pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom, zerocopy::pointer::invariant::Safe, zerocopy::pointer::invariant::Safe> for T}] + Source: 'src/pointer/transmute.rs', lines 590:0-590:66 -/ +@[reducible] +def pointer.transmute.TransmuteFromTCellSafeSafe.Blanket (T : Type) : + pointer.transmute.TransmuteFrom T (core.cell.Cell T) pointer.invariant.Safe + pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom, zerocopy::pointer::invariant::Safe, zerocopy::pointer::invariant::Safe> for core::cell::UnsafeCell}] + Source: 'src/pointer/transmute.rs', lines 607:0-612:1 -/ +@[reducible] +def + core.cell.UnsafeCell.Insts.ZerocopyPointerTransmuteTransmuteFromCellSafeSafe + {T : Type} (TransmuteFromTCellSafeSafeInst : pointer.transmute.TransmuteFrom + T (core.cell.Cell T) pointer.invariant.Safe pointer.invariant.Safe) + (TransmuteFromUnsafeCellTSafeSafeInst : pointer.transmute.TransmuteFrom + (core.cell.UnsafeCell T) T pointer.invariant.Safe pointer.invariant.Safe) : + pointer.transmute.TransmuteFrom (core.cell.UnsafeCell T) (core.cell.Cell T) + pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::pointer::transmute::{impl zerocopy::pointer::transmute::TransmuteFrom, zerocopy::pointer::invariant::Safe, zerocopy::pointer::invariant::Safe> for core::cell::Cell}] + Source: 'src/pointer/transmute.rs', lines 623:0-628:1 -/ +@[reducible] +def + core.cell.Cell.Insts.ZerocopyPointerTransmuteTransmuteFromUnsafeCellSafeSafe + {T : Type} (TransmuteFromTUnsafeCellSafeSafeInst : + pointer.transmute.TransmuteFrom T (core.cell.UnsafeCell T) + pointer.invariant.Safe pointer.invariant.Safe) + (TransmuteFromCellTSafeSafeInst : pointer.transmute.TransmuteFrom + (core.cell.Cell T) T pointer.invariant.Safe pointer.invariant.Safe) : + pointer.transmute.TransmuteFrom (core.cell.Cell T) (core.cell.UnsafeCell T) + pointer.invariant.Safe pointer.invariant.Safe := { +} + /-- [zerocopy::split_at::split_right_len]: Source: 'src/split_at.rs', lines 27:0-29:1 -/ def split_at.split_right_len @@ -3584,21 +3964,6 @@ def Array.Insts.ZerocopyIntoBytes {T : Type} (N : Std.Usize) (IntoBytesInst : N IntoBytesInst } -/-- [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 Bool.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait - : Result Unit := do - ok () - -/-- Trait implementation: [zerocopy::impls::_#2::{impl zerocopy::IntoBytes for bool}] - Source: 'src/util/macros.rs', lines 30:8-32:9 -/ -@[reducible] -def Bool.Insts.ZerocopyIntoBytes : IntoBytes Bool := { - 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]: Source: 'src/util/macros.rs', lines 165:8-165:62 Visibility: public -/ @@ -4005,58 +4370,6 @@ def I16.Insts.ZerocopyIntoBytes : IntoBytes Std.I16 := { I16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait } -/-- [zerocopy::impls::_#1::{impl zerocopy::FromZeros 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.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait - : Result Unit := do - ok () - -/-- [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}::only_derive_is_allowed_to_implement_this_trait]: - Source: 'src/util/macros.rs', lines 153:8-153:62 - Visibility: public -/ -def - U32.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait - : Result Unit := do - ok () - -/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}] - Source: 'src/util/macros.rs', lines 30:8-32:9 -/ -@[reducible] -def U32.Insts.ZerocopyTryFromBytes : TryFromBytes Std.U32 := { - only_derive_is_allowed_to_implement_this_trait := - U32.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait - is_safe := fun {A : Type} (pointerinvariantAlignmentInst : - pointer.invariant.Alignment A) => U32.Insts.ZerocopyTryFromBytes.is_safe - pointerinvariantAlignmentInst -} - -/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::FromZeros for u32}] - Source: 'src/util/macros.rs', lines 30:8-32:9 -/ -@[reducible] -def U32.Insts.ZerocopyFromZeros : FromZeros Std.U32 := { - TryFromBytesInst := U32.Insts.ZerocopyTryFromBytes - only_derive_is_allowed_to_implement_this_trait := - U32.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait - new_zeroed := FromZeros.new_zeroed.default Std.U32 -} - -/-- [zerocopy::impls::_#1::{impl zerocopy::FromBytes 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.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait - : Result Unit := do - ok () - -/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::FromBytes for u32}] - Source: 'src/util/macros.rs', lines 30:8-32:9 -/ -@[reducible] -def U32.Insts.ZerocopyFromBytes : FromBytes Std.U32 := { - FromZerosInst := U32.Insts.ZerocopyFromZeros - only_derive_is_allowed_to_implement_this_trait := - U32.Insts.ZerocopyFromBytes.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 -/ @@ -5224,4 +5537,21 @@ def util.safety_checks.bool_slice_valid (bytes : Slice Std.U8) : Result Bool := do util.safety_checks.bool_slice_valid_loop bytes 0#usize +/-- Trait implementation: [zerocopy::wrappers::{impl zerocopy::pointer::transmute::TransmuteFrom for zerocopy::wrappers::read_only_def::ReadOnly}] + Source: 'src/wrappers.rs', lines 732:0-732:70 -/ +@[reducible] +def + wrappers.read_only_def.ReadOnly.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe + (T : Type) : pointer.transmute.TransmuteFrom (wrappers.read_only_def.ReadOnly + T) T pointer.invariant.Safe pointer.invariant.Safe := { +} + +/-- Trait implementation: [zerocopy::wrappers::{impl zerocopy::pointer::transmute::TransmuteFrom, zerocopy::pointer::invariant::Safe, zerocopy::pointer::invariant::Safe> for T}] + Source: 'src/wrappers.rs', lines 739:0-739:70 -/ +@[reducible] +def pointer.transmute.TransmuteFromTReadOnlySafeSafe.Blanket (T : Type) : + pointer.transmute.TransmuteFrom T (wrappers.read_only_def.ReadOnly T) + pointer.invariant.Safe pointer.invariant.Safe := { +} + end Zerocopy diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index bcb41c4a7f..8f6cc85aad 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -131,6 +131,17 @@ axiom core.num.Usize.unchecked_add axiom core.num.Usize.unchecked_mul : Std.Usize → Std.Usize → Result Std.Usize +/-- [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}::is_safe]: + Source: 'src/util/macros.rs', lines 155:8-160:9 + Visibility: public -/ +axiom U32.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment Alignment) : + pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly Std.U32) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result + Bool + /-- [zerocopy::util::copy_unchecked]: Source: 'src/util/mod.rs', lines 334:0-349:1 -/ axiom util.copy_unchecked @@ -163,17 +174,6 @@ axiom U8.Insts.ZerocopyTryFromBytes.is_safe pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result Bool -/-- [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}::is_safe]: - Source: 'src/util/macros.rs', lines 155:8-160:9 - Visibility: public -/ -axiom U32.Insts.ZerocopyTryFromBytes.is_safe - {Alignment : Type} (pointerinvariantAlignmentInst : - pointer.invariant.Alignment Alignment) : - pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly Std.U32) - (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) - pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result - Bool - /-- [zerocopy::impls::_#3::{impl zerocopy::TryFromBytes for bool}::is_safe]: Source: 'src/util/macros.rs', lines 143:8-148:9 Visibility: public -/ diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 90bb560955..eac066d6ec 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -269,17 +269,17 @@ structure wrappers.read_only_def.ReadOnly (T : Type) where inner : T /-- [zerocopy::pointer::invariant::Initialized] - Source: 'src/pointer/invariant.rs', lines 227:0-227:23 + Source: 'src/pointer/invariant.rs', lines 240:0-240:23 Visibility: public -/ inductive pointer.invariant.Initialized where /-- [zerocopy::pointer::invariant::Shared] - Source: 'src/pointer/invariant.rs', lines 133:0-133:18 + Source: 'src/pointer/invariant.rs', lines 140:0-140:18 Visibility: public -/ inductive pointer.invariant.Shared where /-- Trait declaration: [zerocopy::pointer::invariant::sealed::Sealed] - Source: 'src/pointer/invariant.rs', lines 296:4-296:23 + Source: 'src/pointer/invariant.rs', lines 325:4-325:23 Visibility: public -/ structure pointer.invariant.sealed.Sealed (Self : Type) where @@ -291,18 +291,18 @@ structure pointer.invariant.Aliasing (Self : Type) where sealedSealedInst : pointer.invariant.sealed.Sealed Self /-- Trait declaration: [zerocopy::pointer::invariant::Read] - Source: 'src/pointer/invariant.rs', lines 277:0-277:33 + Source: 'src/pointer/invariant.rs', lines 306:0-306:33 Visibility: public -/ structure pointer.invariant.Read (Self : Type) (A : Type) (R : Type) where AliasingInst : pointer.invariant.Aliasing A /-- [zerocopy::pointer::invariant::Safe] - Source: 'src/pointer/invariant.rs', lines 238:0-238:16 + Source: 'src/pointer/invariant.rs', lines 254:0-254:16 Visibility: public -/ inductive pointer.invariant.Safe where /-- Trait declaration: [zerocopy::pointer::invariant::Reference] - Source: 'src/pointer/invariant.rs', lines 121:0-121:41 + Source: 'src/pointer/invariant.rs', lines 128:0-128:41 Visibility: public -/ structure pointer.invariant.Reference (Self : Type) where AliasingInst : pointer.invariant.Aliasing Self @@ -357,6 +357,51 @@ structure IntoBytes (Self : Type) where structure Unaligned (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit +/-- [zerocopy::pointer::invariant::ValidityKind] + Source: 'src/pointer/invariant.rs', lines 115:0-120:1 + Visibility: public -/ +@[discriminant isize] +inductive pointer.invariant.ValidityKind where +| Uninit : pointer.invariant.ValidityKind +| AsInitialized : pointer.invariant.ValidityKind +| Initialized : pointer.invariant.ValidityKind +| Safe : pointer.invariant.ValidityKind + +/-- Trait declaration: [zerocopy::pointer::invariant::Validity] + Source: 'src/pointer/invariant.rs', lines 111:0-113:1 + Visibility: public -/ +structure pointer.invariant.Validity (Self : Type) where + KIND : Result pointer.invariant.ValidityKind + sealedSealedInst : pointer.invariant.sealed.Sealed Self + +/-- [zerocopy::pointer::invariant::Uninit] + Source: 'src/pointer/invariant.rs', lines 189:0-189:18 + Visibility: public -/ +inductive pointer.invariant.Uninit where + +/-- [zerocopy::pointer::invariant::AsInitialized] + Source: 'src/pointer/invariant.rs', lines 228:0-228:25 + Visibility: public -/ +inductive pointer.invariant.AsInitialized where + +/-- Trait declaration: [zerocopy::pointer::invariant::CastableFrom] + Source: 'src/pointer/invariant.rs', lines 279:0-279:52 + Visibility: public -/ +structure pointer.invariant.CastableFrom (Self : Type) (ST : Type) (SV : Type) + (DV : Type) where + +/-- Trait declaration: [zerocopy::pointer::transmute::TransmuteFrom] + Source: 'src/pointer/transmute.rs', lines 345:0-345:54 + Visibility: public -/ +structure pointer.transmute.TransmuteFrom (Self : Type) (Src : Type) (SV : + Type) (DV : Type) where + +/-- [zerocopy::wrappers::Unalign] + Source: 'src/wrappers.rs', lines 118:0-118:25 + Visibility: public -/ +structure wrappers.Unalign (T : Type) where + _0 : T + /-- Trait declaration: [zerocopy::trait_checks::ByteCodec] Source: 'src/trait_checks.rs', lines 97:0-100:1 -/ structure trait_checks.ByteCodec (Self : Type) where @@ -372,12 +417,6 @@ structure trait_checks.XorCodec where structure trait_checks.Forward (C : Type) where _0 : core.marker.PhantomData C -/-- [zerocopy::wrappers::Unalign] - Source: 'src/wrappers.rs', lines 118:0-118:25 - Visibility: public -/ -structure wrappers.Unalign (T : Type) where - _0 : T - /-- Trait declaration: [zerocopy::util::macro_util::transmute_copy::StaticAssert] Source: 'src/util/macros.rs', lines 679:8-681:9 -/ structure util.macro_util.transmute_copy.StaticAssert (Self : Type) where diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py index ba6b2cef7c..56e62e8606 100644 --- a/verification/aeneas/inline.py +++ b/verification/aeneas/inline.py @@ -1163,6 +1163,7 @@ def assemble(root, annotations, work, development=False): imports.append('public import TraitLaws') law_lines = GeneratedLines([*golden.HEADER.rstrip().splitlines(), '', 'module', 'public import Zerocopy.Funs', 'public import TraitLawsSupport', + *(['public import ReferentValidity'] if (root / 'verification/aeneas/lean/ReferentValidity.lean').exists() else []), *[line for line in imports if line in {'public import LayoutModel', 'public import Arithmetic'}], '@[expose] public section', 'open Aeneas Aeneas.Std', 'namespace Zerocopy.TraitLaws', '']) diff --git a/verification/aeneas/lean/DeriveModels.lean b/verification/aeneas/lean/DeriveModels.lean index f5bf63be97..7b332a32ef 100644 --- a/verification/aeneas/lean/DeriveModels.lean +++ b/verification/aeneas/lean/DeriveModels.lean @@ -514,8 +514,24 @@ private meta def deriveProvider (raw : Name) (count : Nat) -- contain no unresolved choice metavariable. let choice := mkLambda `_raw .default rawTy (mkApp (mkConst ``List.nil [.zero]) (mkConst ``Rust.Storage.AMByte)) + -- Marker types have no values from which to recover their type-level + -- meaning. Attach the code to their ordinary generated provider. Every + -- other type lacks this metadata; absence never means a weak state. + let marker ← match raw with + | ``Zerocopy.pointer.invariant.Uninit => pure (some ``ValidityMarker.uninit) + | ``Zerocopy.pointer.invariant.AsInitialized => pure (some ``ValidityMarker.asInitialized) + | ``Zerocopy.pointer.invariant.Initialized => pure (some ``ValidityMarker.initialized) + | ``Zerocopy.pointer.invariant.Safe => pure (some ``ValidityMarker.safe) + | _ => pure none + if marker.isSome && (!info.ctors.isEmpty || count != 0) then + throwError "Validity markers must retain their empty nominal carriers: {raw}" + let markerValue ← match marker with + | none => mkAppOptM ``Option.none #[some (mkConst ``ValidityMarker)] + | some constructor => mkAppOptM ``Option.some #[some (mkConst ``ValidityMarker), + some (mkConst constructor)] let provider ← mkAppOptM ``RustModel.mk #[some rawTy, some modelTy, - some (mkAppN (mkConst b.decoder levels) all), some representation, some choice] + some (mkAppN (mkConst b.decoder levels) all), some representation, some choice, + some markerValue] addDefinition b.provider info.levelParams (← mkLambdaFVars all provider) setReducibilityStatus b.provider .reducible addInstance b.provider .global 1000 diff --git a/verification/aeneas/lean/Obligations/ReferentValidity.lean b/verification/aeneas/lean/Obligations/ReferentValidity.lean new file mode 100644 index 0000000000..9c142d63e3 --- /dev/null +++ b/verification/aeneas/lean/Obligations/ReferentValidity.lean @@ -0,0 +1,110 @@ +/- 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 Zerocopy.Funs +public import TraitLaws +public import Rust.Referent +@[expose] public section + +/-! +The expectations below state the byte-content implication directly. Each safe +representation must pass the installed physical decoder and the retained +mathematical decoder. The same byte list and its width survive the transfer; +the width comparison remains a guard. These expectations concern contents only. +-/ +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace Zerocopy.Obligations + +def stateCode : Rust.Referent.State → ValidityMarker + | .uninit => .uninit + | .initialized => .initialized + | .safe => .safe + +def contents {Raw : Type} (meaning : RustModel Raw) (physical : BitDecoder Raw) + (state : Rust.Referent.State) (bytes : List AMByte) : Prop := + match state with + | .uninit => True + | .initialized => Rust.Storage.Initialized bytes + | .safe => ∃ raw mathematical, + physical.run bytes = some raw ∧ meaning.decode raw = some mathematical + +def contentTransfer {Src Dst : Type} (source : RustModel Src) + (sourcePhysical : BitDecoder Src) (destination : RustModel Dst) + (destinationPhysical : BitDecoder Dst) + (sourceState destinationState : Rust.Referent.State) : Prop := + sourcePhysical.byteSize = destinationPhysical.byteSize → ∀ bytes, + bytes.length = sourcePhysical.byteSize → contents source sourcePhysical sourceState bytes → + bytes.length = destinationPhysical.byteSize ∧ + contents destination destinationPhysical destinationState bytes + +def installedContentTransfer {Src Dst : Type} (source : RustModel Src) + (destination : RustModel Dst) (sourceState destinationState : Rust.Referent.State) : Prop := + ∀ sourcePhysical destinationPhysical, + source.representation = some sourcePhysical → + destination.representation = some destinationPhysical → + contentTransfer source sourcePhysical destination destinationPhysical sourceState destinationState + +def require_transfer_spec_contract (Src Dst SV DV : Type) + (dictionary : pointer.transmute.TransmuteFrom Dst Src SV DV) (run : Result Unit) : Prop := + ∀ [source : RustModel Src] [destination : RustModel Dst] + [sourceMeaning : RustModel SV] [destinationMeaning : RustModel DV], + TraitLaws.transmute_from Dst Src SV DV dictionary → + run ⦃ _ => ∀ sourceState destinationState, + sourceMeaning.validityMarker = some (stateCode sourceState) → + destinationMeaning.validityMarker = some (stateCode destinationState) → + installedContentTransfer source destination sourceState destinationState ⦄ + +def require_transfer_spec : Prop := + ∀ (Src Dst SV DV : Type) (dictionary : pointer.transmute.TransmuteFrom Dst Src SV DV), + require_transfer_spec_contract Src Dst SV DV dictionary + (pointer.referent_checks.require_transfer dictionary) + +def require_type_independent_spec_contract (Src Dst SV DV : Type) + (dictionary : pointer.invariant.CastableFrom Dst Src SV DV) (run : Result Unit) : Prop := + ∀ [RustModel Src] [RustModel Dst] [RustModel SV] [RustModel DV], + TraitLaws.castable_from Dst Src SV DV dictionary → + run ⦃ _ => + (SV = pointer.invariant.Uninit ∧ DV = pointer.invariant.Uninit) ∨ + (SV = pointer.invariant.Initialized ∧ DV = pointer.invariant.Initialized) ⦄ + +def require_type_independent_spec : Prop := + ∀ (Src Dst SV DV : Type) (dictionary : pointer.invariant.CastableFrom Dst Src SV DV), + require_type_independent_spec_contract Src Dst SV DV dictionary + (pointer.referent_checks.require_type_independent dictionary) + +def compose_safe_transfers_spec_contract (Src Mid Dst : Type) + (first : pointer.transmute.TransmuteFrom Mid Src pointer.invariant.Safe pointer.invariant.Safe) + (second : pointer.transmute.TransmuteFrom Dst Mid pointer.invariant.Safe pointer.invariant.Safe) + (run : Result Unit) : Prop := + ∀ [source : RustModel Src] [_middle : RustModel Mid] [destination : RustModel Dst], + TraitLaws.transmute_from Mid Src pointer.invariant.Safe pointer.invariant.Safe first → + TraitLaws.transmute_from Dst Mid pointer.invariant.Safe pointer.invariant.Safe second → + RustModel.sameSize Src Mid → + run ⦃ _ => installedContentTransfer source destination .safe .safe ⦄ + +def compose_safe_transfers_spec : Prop := + ∀ (Src Mid Dst : Type) + (first : pointer.transmute.TransmuteFrom Mid Src pointer.invariant.Safe pointer.invariant.Safe) + (second : pointer.transmute.TransmuteFrom Dst Mid pointer.invariant.Safe pointer.invariant.Safe), + compose_safe_transfers_spec_contract Src Mid Dst first second + (pointer.referent_checks.compose_safe_transfers first second) + +def concrete_transfers_spec_contract (run : Result Unit) : Prop := + run ⦃ _ => + contentTransfer modelBool boolDecoder (modelUScalar .U8) u8BitDecoder .safe .initialized ∧ + contentTransfer (modelUScalar .U8) u8BitDecoder modelBool boolDecoder .initialized .uninit ∧ + ((pointer.invariant.Initialized = pointer.invariant.Uninit ∧ + pointer.invariant.Initialized = pointer.invariant.Uninit) ∨ + (pointer.invariant.Initialized = pointer.invariant.Initialized ∧ + pointer.invariant.Initialized = pointer.invariant.Initialized)) ⦄ + +def concrete_transfers_spec : Prop := + concrete_transfers_spec_contract pointer.referent_checks.concrete_transfers + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/ReferentValidity.lean b/verification/aeneas/lean/Proofs/ReferentValidity.lean new file mode 100644 index 0000000000..3629845a28 --- /dev/null +++ b/verification/aeneas/lean/Proofs/ReferentValidity.lean @@ -0,0 +1,264 @@ +/- 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 ReferentWrappers +public import Proofs.FromBytes +public import Proofs.IntoBytes +@[expose] public section + +/-! +Each implementation theorem keeps the native function's complete input prefix, +then adds exactly the providers and input laws required by the proof audit. +The conclusion names the actual extracted dictionary. Wrapper implications use +both decoder stages of the canonical providers; they do not choose encodings. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +@[instance] theorem pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantValidity_law : + TraitLaws.validity_kind pointer.invariant.Uninit + Zerocopy.pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantValidity := + ⟨⟨.uninit, rfl, by + simp [Zerocopy.pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantValidity.KIND, + Referent.nativeKind]⟩⟩ + +@[instance] theorem pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantValidity_law : + TraitLaws.validity_kind pointer.invariant.AsInitialized + Zerocopy.pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantValidity := + ⟨⟨.asInitialized, rfl, by + simp [Zerocopy.pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantValidity.KIND, + Referent.nativeKind]⟩⟩ + +@[instance] theorem pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity_law : + TraitLaws.validity_kind pointer.invariant.Initialized + Zerocopy.pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity := + ⟨⟨.initialized, rfl, by + simp [Zerocopy.pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity.KIND, + Referent.nativeKind]⟩⟩ + +@[instance] theorem pointer.invariant.Safe.Insts.ZerocopyPointerInvariantValidity_law : + TraitLaws.validity_kind pointer.invariant.Safe + Zerocopy.pointer.invariant.Safe.Insts.ZerocopyPointerInvariantValidity := + ⟨⟨.safe, rfl, by + simp [Zerocopy.pointer.invariant.Safe.Insts.ZerocopyPointerInvariantValidity.KIND, + Referent.nativeKind]⟩⟩ + +@[instance] theorem pointer.transmute.TransmuteFromDstSrcSafeInitialized.Blanket_law + {Src : Type} (Dst : Type) (dictionary : IntoBytes Src) + [source : RustModel Src] [destination : RustModel Dst] + [law : TraitLaws.into_bytes_initialized Src dictionary] : + TraitLaws.transmute_from Dst Src pointer.invariant.Safe pointer.invariant.Initialized + (Zerocopy.pointer.transmute.TransmuteFromDstSrcSafeInitialized.Blanket Dst dictionary) := + ⟨Referent.safe_to_initialized Src Dst + (@TraitLaws.into_bytes_initialized.holds Src dictionary source law).1⟩ + +@[instance] theorem pointer.transmute.TransmuteFromDstSrcInitializedSafe.Blanket_law + (Src : Type) {Dst : Type} (dictionary : FromBytes Dst) + [source : RustModel Src] [destination : RustModel Dst] + [law : TraitLaws.from_bytes_valid Dst dictionary] + [_parentLaw : TraitLaws.from_zeros_valid Dst dictionary.FromZerosInst] : + TraitLaws.transmute_from Dst Src pointer.invariant.Initialized pointer.invariant.Safe + (Zerocopy.pointer.transmute.TransmuteFromDstSrcInitializedSafe.Blanket Src dictionary) := + ⟨Referent.initialized_to_safe Src Dst + (@TraitLaws.from_bytes_valid.holds Dst dictionary destination law)⟩ + +@[instance] theorem pointer.transmute.TransmuteFromDstSrcInitializedInitialized.Blanket_law + (Src Dst : Type) [source : RustModel Src] [destination : RustModel Dst] : + TraitLaws.transmute_from Dst Src pointer.invariant.Initialized pointer.invariant.Initialized + (Zerocopy.pointer.transmute.TransmuteFromDstSrcInitializedInitialized.Blanket Src Dst) := + ⟨Referent.initialized_identity Src Dst⟩ + +@[instance] theorem pointer.transmute.TransmuteFromDstSrcVUninit.Blanket_law + (Src Dst : Type) {V : Type} (dictionary : pointer.invariant.Validity V) + [source : RustModel Src] [destination : RustModel Dst] [meaning : RustModel V] + [law : TraitLaws.validity_kind V dictionary] : + TraitLaws.transmute_from Dst Src V pointer.invariant.Uninit + (Zerocopy.pointer.transmute.TransmuteFromDstSrcVUninit.Blanket Src Dst dictionary) := by + obtain ⟨marker, identified, _⟩ := @TraitLaws.validity_kind.holds V dictionary meaning law + exact ⟨Referent.forget Src Dst V ⟨marker, identified⟩⟩ + +-- Each direction uses the same proved safe-domain equivalence. The theorem +-- inputs preserve the native implementation prefix before the payload provider. + +@[instance] theorem core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from (_root_.core.mem.manually_drop.ManuallyDrop T) T pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe T) := + ⟨Referent.safe_transfer_of_implication T (_root_.core.mem.manually_drop.ManuallyDrop T) + (fun bytes => (Referent.safeBytes_manuallyDrop_iff T bytes).mpr)⟩ + +@[instance] theorem pointer.transmute.TransmuteFromTManuallyDropSafeSafe.Blanket_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from T (_root_.core.mem.manually_drop.ManuallyDrop T) pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.pointer.transmute.TransmuteFromTManuallyDropSafeSafe.Blanket T) := + ⟨Referent.safe_transfer_of_implication (_root_.core.mem.manually_drop.ManuallyDrop T) T + (fun bytes => (Referent.safeBytes_manuallyDrop_iff T bytes).mp)⟩ + +@[instance] theorem wrappers.Unalign.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from (Zerocopy.wrappers.Unalign T) T pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.wrappers.Unalign.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe T) := + ⟨Referent.safe_transfer_of_implication T (Zerocopy.wrappers.Unalign T) + (fun bytes => (Referent.safeBytes_unalign_iff T bytes).mpr)⟩ + +@[instance] theorem pointer.transmute.TransmuteFromTUnalignSafeSafe.Blanket_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from T (Zerocopy.wrappers.Unalign T) pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.pointer.transmute.TransmuteFromTUnalignSafeSafe.Blanket T) := + ⟨Referent.safe_transfer_of_implication (Zerocopy.wrappers.Unalign T) T + (fun bytes => (Referent.safeBytes_unalign_iff T bytes).mp)⟩ + +@[instance] theorem core.num.wrapping.Wrapping.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from (Zerocopy.core.num.wrapping.Wrapping T) T pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.core.num.wrapping.Wrapping.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe T) := + ⟨Referent.safe_transfer_of_implication T (Zerocopy.core.num.wrapping.Wrapping T) + (fun bytes => (Referent.safeBytes_wrapping_iff T bytes).mpr)⟩ + +@[instance] theorem pointer.transmute.TransmuteFromTWrappingSafeSafe.Blanket_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from T (Zerocopy.core.num.wrapping.Wrapping T) pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.pointer.transmute.TransmuteFromTWrappingSafeSafe.Blanket T) := + ⟨Referent.safe_transfer_of_implication (Zerocopy.core.num.wrapping.Wrapping T) T + (fun bytes => (Referent.safeBytes_wrapping_iff T bytes).mp)⟩ + +@[instance] theorem core.cell.UnsafeCell.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from (_root_.core.cell.UnsafeCell T) T pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.core.cell.UnsafeCell.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe T) := + ⟨Referent.safe_transfer_of_implication T (_root_.core.cell.UnsafeCell T) + (fun bytes => (Referent.safeBytes_unsafeCell_iff T bytes).mpr)⟩ + +@[instance] theorem pointer.transmute.TransmuteFromTUnsafeCellSafeSafe.Blanket_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from T (_root_.core.cell.UnsafeCell T) pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.pointer.transmute.TransmuteFromTUnsafeCellSafeSafe.Blanket T) := + ⟨Referent.safe_transfer_of_implication (_root_.core.cell.UnsafeCell T) T + (fun bytes => (Referent.safeBytes_unsafeCell_iff T bytes).mp)⟩ + +@[instance] theorem core.cell.Cell.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from (_root_.core.cell.Cell T) T pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.core.cell.Cell.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe T) := + ⟨Referent.safe_transfer_of_implication T (_root_.core.cell.Cell T) + (fun bytes => (Referent.safeBytes_cell_iff T bytes).mpr)⟩ + +@[instance] theorem pointer.transmute.TransmuteFromTCellSafeSafe.Blanket_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from T (_root_.core.cell.Cell T) pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.pointer.transmute.TransmuteFromTCellSafeSafe.Blanket T) := + ⟨Referent.safe_transfer_of_implication (_root_.core.cell.Cell T) T + (fun bytes => (Referent.safeBytes_cell_iff T bytes).mp)⟩ + +@[instance] theorem wrappers.read_only_def.ReadOnly.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from (Zerocopy.wrappers.read_only_def.ReadOnly T) T pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.wrappers.read_only_def.ReadOnly.Insts.ZerocopyPointerTransmuteTransmuteFromTSafeSafe T) := + ⟨Referent.safe_transfer_of_implication T (Zerocopy.wrappers.read_only_def.ReadOnly T) + (fun bytes => (Referent.safeBytes_readOnly_iff T bytes).mpr)⟩ + +@[instance] theorem pointer.transmute.TransmuteFromTReadOnlySafeSafe.Blanket_law + (T : Type) [meaning : RustModel T] : + TraitLaws.transmute_from T (Zerocopy.wrappers.read_only_def.ReadOnly T) pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.pointer.transmute.TransmuteFromTReadOnlySafeSafe.Blanket T) := + ⟨Referent.safe_transfer_of_implication (Zerocopy.wrappers.read_only_def.ReadOnly T) T + (fun bytes => (Referent.safeBytes_readOnly_iff T bytes).mp)⟩ + +-- Retain both dictionaries and their laws, as the Rust where-clauses require. +-- The canonical wrapper domains also prove the implication directly, including +-- the case where no payload decoder is installed. No size premise is added. + +@[instance] theorem core.cell.UnsafeCell.Insts.ZerocopyPointerTransmuteTransmuteFromCellSafeSafe_law + {T : Type} + (first : pointer.transmute.TransmuteFrom T (_root_.core.cell.Cell T) + pointer.invariant.Safe pointer.invariant.Safe) + (second : pointer.transmute.TransmuteFrom (_root_.core.cell.UnsafeCell T) T + pointer.invariant.Safe pointer.invariant.Safe) + [meaning : RustModel T] + [_firstLaw : TraitLaws.transmute_from T (_root_.core.cell.Cell T) + pointer.invariant.Safe pointer.invariant.Safe first] + [_secondLaw : TraitLaws.transmute_from (_root_.core.cell.UnsafeCell T) T + pointer.invariant.Safe pointer.invariant.Safe second] : + TraitLaws.transmute_from (_root_.core.cell.UnsafeCell T) (_root_.core.cell.Cell T) + pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.core.cell.UnsafeCell.Insts.ZerocopyPointerTransmuteTransmuteFromCellSafeSafe + first second) := + ⟨Referent.safe_transfer_of_implication (_root_.core.cell.Cell T) (_root_.core.cell.UnsafeCell T) + (fun bytes admitted => (Referent.safeBytes_unsafeCell_iff T bytes).mpr + ((Referent.safeBytes_cell_iff T bytes).mp admitted))⟩ + +@[instance] theorem core.cell.Cell.Insts.ZerocopyPointerTransmuteTransmuteFromUnsafeCellSafeSafe_law + {T : Type} + (first : pointer.transmute.TransmuteFrom T (_root_.core.cell.UnsafeCell T) + pointer.invariant.Safe pointer.invariant.Safe) + (second : pointer.transmute.TransmuteFrom (_root_.core.cell.Cell T) T + pointer.invariant.Safe pointer.invariant.Safe) + [meaning : RustModel T] + [_firstLaw : TraitLaws.transmute_from T (_root_.core.cell.UnsafeCell T) + pointer.invariant.Safe pointer.invariant.Safe first] + [_secondLaw : TraitLaws.transmute_from (_root_.core.cell.Cell T) T + pointer.invariant.Safe pointer.invariant.Safe second] : + TraitLaws.transmute_from (_root_.core.cell.Cell T) (_root_.core.cell.UnsafeCell T) + pointer.invariant.Safe pointer.invariant.Safe + (Zerocopy.core.cell.Cell.Insts.ZerocopyPointerTransmuteTransmuteFromUnsafeCellSafeSafe + first second) := + ⟨Referent.safe_transfer_of_implication (_root_.core.cell.UnsafeCell T) (_root_.core.cell.Cell T) + (fun bytes admitted => (Referent.safeBytes_cell_iff T bytes).mpr + ((Referent.safeBytes_unsafeCell_iff T bytes).mp admitted))⟩ + +@[instance] theorem pointer.invariant.CastableFromDTSTUninitUninit.Blanket_law (ST DT : Type) : + TraitLaws.castable_from DT ST pointer.invariant.Uninit pointer.invariant.Uninit + (Zerocopy.pointer.invariant.CastableFromDTSTUninitUninit.Blanket ST DT) := + ⟨Or.inl ⟨rfl, rfl⟩⟩ + +@[instance] theorem pointer.invariant.CastableFromDTSTInitializedInitialized.Blanket_law + (ST DT : Type) : + TraitLaws.castable_from DT ST pointer.invariant.Initialized pointer.invariant.Initialized + (Zerocopy.pointer.invariant.CastableFromDTSTInitializedInitialized.Blanket ST DT) := + ⟨Or.inr ⟨rfl, rfl⟩⟩ + +-- These empty Rust bodies still receive their exact dictionary laws. The +-- specification also checks admission of the successful Unit result. + +theorem require_transfer_spec : Specs.require_transfer_spec := by + intro Src Dst SV DV dictionary + intros + simp only [pointer.referent_checks.require_transfer, WP.spec_ok] + exact ⟨(), rfl, + @TraitLaws.transmute_from.holds Dst Src SV DV dictionary _ _ _ _ inferInstance⟩ + +theorem require_type_independent_spec : Specs.require_type_independent_spec := by + intro Src Dst SV DV dictionary + intros + simp only [pointer.referent_checks.require_type_independent, WP.spec_ok] + exact ⟨(), rfl, @TraitLaws.castable_from.holds Dst Src SV DV dictionary inferInstance⟩ + +theorem compose_safe_transfers_spec : Specs.compose_safe_transfers_spec := by + intro Src Mid Dst first second + intros + simp only [pointer.referent_checks.compose_safe_transfers, WP.spec_ok] + refine ⟨(), rfl, Referent.safe_trans Src Mid Dst ?_ ?_ (by assumption)⟩ + · exact @TraitLaws.transmute_from.holds Mid Src pointer.invariant.Safe pointer.invariant.Safe + first _ _ _ _ inferInstance + · exact @TraitLaws.transmute_from.holds Dst Mid pointer.invariant.Safe pointer.invariant.Safe + second _ _ _ _ inferInstance + +theorem concrete_transfers_spec : Specs.concrete_transfers_spec := by + simp only [Specs.concrete_transfers_spec, pointer.referent_checks.concrete_transfers, + pointer.referent_checks.require_transfer, pointer.referent_checks.require_type_independent, + bind_ok, WP.spec_ok] + refine ⟨(), rfl, ?_, ?_, ?_⟩ + · exact Referent.safe_to_initialized Bool U8 Rust.Storage.boolDecoder_initialized + · exact Referent.forget U8 Bool pointer.invariant.Initialized ⟨.initialized, rfl⟩ + · exact Or.inr ⟨rfl, rfl⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/ReferentContractTests.lean b/verification/aeneas/lean/ReferentContractTests.lean new file mode 100644 index 0000000000..e6c2f4f766 --- /dev/null +++ b/verification/aeneas/lean/ReferentContractTests.lean @@ -0,0 +1,157 @@ +/- 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 +import all Proofs.ReferentValidity +import RequiredContracts +import RequiredModelContracts.ReferentValidity +import all ModelPrelude + +/-! +These checks protect the meanings behind the inline invariants. A validity +marker is an empty Rust type with a type-level code, not a value constructor. +Its actual associated constant must agree with that code. Unknown metadata +and missing physical decoding remain separate failures. +-/ + +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace Zerocopy.ReferentTests + +-- Pin constants directly, independently of the code-to-KIND conversion helper. +example : pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantValidity.KIND = + pointer.invariant.ValidityKind.Uninit := by + simp [pointer.invariant.Uninit.Insts.ZerocopyPointerInvariantValidity.KIND] + +example : pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantValidity.KIND = + pointer.invariant.ValidityKind.AsInitialized := by + simp [pointer.invariant.AsInitialized.Insts.ZerocopyPointerInvariantValidity.KIND] + +example : pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity.KIND = + pointer.invariant.ValidityKind.Initialized := by + simp [pointer.invariant.Initialized.Insts.ZerocopyPointerInvariantValidity.KIND] + +example : pointer.invariant.Safe.Insts.ZerocopyPointerInvariantValidity.KIND = + pointer.invariant.ValidityKind.Safe := by + simp [pointer.invariant.Safe.Insts.ZerocopyPointerInvariantValidity.KIND] + +example : (inferInstance : RustModel pointer.invariant.Uninit).validityMarker = + some .uninit := rfl +example : (inferInstance : RustModel pointer.invariant.AsInitialized).validityMarker = + some .asInitialized := rfl +example : (inferInstance : RustModel pointer.invariant.Initialized).validityMarker = + some .initialized := rfl +example : (inferInstance : RustModel pointer.invariant.Safe).validityMarker = + some .safe := rfl + +-- These providers have not created values of the empty marker carriers. +example (raw : pointer.invariant.Uninit) : False := nomatch raw +example (raw : pointer.invariant.AsInitialized) : False := nomatch raw +example (raw : pointer.invariant.Initialized) : False := nomatch raw +example (raw : pointer.invariant.Safe) : False := nomatch raw + +@[reducible] def unknownMeaning : RustModel Nat := { Model := Nat, «decode» := some } + +example (kind : Result pointer.invariant.ValidityKind) : + ¬@Referent.kindMatches Nat unknownMeaning kind := by + rintro ⟨marker, impossible, _⟩ + cases impossible + +example (V : Type) [RustModel V] : + ¬Referent.kindMatches V (.fail .undef) := by + rintro ⟨_, _, impossible⟩ + exact fail_not_ok impossible + +example : ¬Nonempty (Referent.View unknownMeaning) := by + rintro ⟨⟨decoder, impossible⟩⟩ + cases impossible + +theorem two_not_safe_bool : + ¬Referent.safeBytes (inferInstance : RustModel Bool) [AMByte.init 2] := by + rintro ⟨decoder, installed, raw, _, accepted, _⟩ + have same : decoder = boolDecoder := Option.some.inj installed.symm + subst decoder + rw [boolDecoder_run_two] at accepted + contradiction + +/-- Initialization alone cannot justify reinterpreting byte 2 as a boolean. -/ +example : ¬Referent.transmuteFrom U8 Bool pointer.invariant.Initialized + pointer.invariant.Safe := by + intro proof + have transfers := Referent.transmute_sound U8 Bool pointer.invariant.Initialized + pointer.invariant.Safe .initialized .safe rfl rfl proof + have bad := transfers ⟨u8BitDecoder, rfl⟩ ⟨boolDecoder, rfl⟩ rfl + [AMByte.init 2] ⟨rfl, by simp [Initialized]⟩ + exact two_not_safe_bool bad.2 + +/-- Unsupported AsInitialized reasoning has no evidence constructor. The +separate forgetting constructor still permits every source to become Uninit. -/ +example (Src Dst : Type) [source : RustModel Src] [destination : RustModel Dst] : + ¬Referent.Supports source destination .asInitialized .safe := by + have excluded : ∀ first second, Referent.Supports source destination first second → + first = .asInitialized → second = .safe → False := by + intro first second supported + cases supported with + | forget kind => intro _ impossible; cases impossible + | modeled first second proof => + intro impossible _ + cases first <;> cases impossible + intro supported + exact excluded _ _ supported rfl rfl + +example (SV DV : Type) : Referent.typeIndependentPair SV DV ↔ + (SV = pointer.invariant.Uninit ∧ DV = pointer.invariant.Uninit) ∨ + (SV = pointer.invariant.Initialized ∧ DV = pointer.invariant.Initialized) := Iff.rfl + +-- Execution safety cannot become conditional on finding a modeled state. Even +-- an AsInitialized marker must not let a forbidden result satisfy this family. +example (Src Dst SV DV : Type) [source : RustModel Src] [destination : RustModel Dst] + [sourceMeaning : RustModel SV] [destinationMeaning : RustModel DV] + (dictionary : pointer.transmute.TransmuteFrom Dst Src SV DV) + (law : TraitLaws.transmute_from Dst Src SV DV dictionary) : + ¬Obligations.require_transfer_spec_contract Src Dst SV DV dictionary (.fail .undef) := by + intro promised + have forbidden := @promised source destination sourceMeaning destinationMeaning law + simp at forbidden + +-- These are valid Lean proofs of weaker statements. The native proof audit +-- must reject them even though the kernel accepts their bodies. +private theorem extraPremise (Src Dst : Type) [RustModel Src] [RustModel Dst] (_extra : True) : + TraitLaws.transmute_from Dst Src pointer.invariant.Initialized pointer.invariant.Initialized + (pointer.transmute.TransmuteFromDstSrcInitializedInitialized.Blanket Src Dst) := + ⟨Referent.initialized_identity Src Dst⟩ + +/-- error: Trait implementation proof omitted required inputs or added premises -/ +#guard_msgs in +run_elab do + AeneasSpecs.auditTraitImplementationProof + ``TraitLaws.transmute_from + ``pointer.transmute.TransmuteFromDstSrcInitializedInitialized.Blanket + ``extraPremise + +@[reducible] private def replacementMeaning (T : Type) : RustModel T := + { Model := T, «decode» := some } + +private theorem replacedProviders (Src Dst : Type) [_source : RustModel Src] + [_destination : RustModel Dst] : + @TraitLaws.transmute_from Dst Src pointer.invariant.Initialized pointer.invariant.Initialized + (pointer.transmute.TransmuteFromDstSrcInitializedInitialized.Blanket Src Dst) + (replacementMeaning Dst) (replacementMeaning Src) _ _ := +by + letI : RustModel Src := replacementMeaning Src + letI : RustModel Dst := replacementMeaning Dst + exact ⟨Referent.initialized_identity Src Dst⟩ + +/-- error: Trait implementation proof changed its dictionary or canonical provider -/ +#guard_msgs in +run_elab do + AeneasSpecs.auditTraitImplementationProof + ``TraitLaws.transmute_from + ``pointer.transmute.TransmuteFromDstSrcInitializedInitialized.Blanket + ``replacedProviders + +end Zerocopy.ReferentTests diff --git a/verification/aeneas/lean/ReferentValidity.lean b/verification/aeneas/lean/ReferentValidity.lean new file mode 100644 index 0000000000..408de92d5f --- /dev/null +++ b/verification/aeneas/lean/ReferentValidity.lean @@ -0,0 +1,224 @@ +/- 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 Models +public import Zerocopy.Funs +public import Rust.Referent +@[expose] public section + +/-! +The Rust validity markers describe permitted referent contents, not pointer +permissions. This adapter connects their exact extracted identities to the +shared byte-domain algebra. Physical and mathematical decoding must both +succeed for `Safe`; initialization alone does not construct a typed value. + +A `View` names an available decoder from the retained model. Missing support +cannot supply a view, while an explicitly empty decoder can: an uninhabited +type has no safe representations, even when its width is zero. Laws quantify +over views and remain conditional on the documented Rust correspondence of +those decoders. They introduce no layout or inhabitedness axiom. + +`AsInitialized` is not interpreted. The `forget` constructor +proves the state-independent weakening to `Uninit`. Every other supported +transfer needs one of the three modeled states and an ordinary checked proof. +-/ + +open Aeneas.Std AeneasSpecs Rust.Storage +namespace Zerocopy.Referent + +abbrev Kind := ValidityMarker +abbrev SafeState := pointer.invariant.Safe +abbrev InitializedState := pointer.invariant.Initialized +abbrev UninitState := pointer.invariant.Uninit + +def nativeKind : Kind → pointer.invariant.ValidityKind + | .uninit => .Uninit + | .asInitialized => .AsInitialized + | .initialized => .Initialized + | .safe => .Safe + +/-- The retained type model supplies the marker's meaning. Check that the +actual Rust dictionary evaluates to that code; missing metadata is rejected. -/ +def kindMatches (V : Type) [meaning : RustModel V] + (kind : Result pointer.invariant.ValidityKind) : Prop := + ∃ marker, meaning.validityMarker = some marker ∧ kind = .ok (nativeKind marker) + +def nativeState : Rust.Referent.State → Kind + | .uninit => .uninit + | .initialized => .initialized + | .safe => .safe + +/-- The decoder is not an independently selectable replacement for the model. -/ +structure View {Raw : Type} (meaning : RustModel Raw) where + decoder : BitDecoder Raw + installed : meaning.representation = some decoder + +/-- All representations accepted by both stages, without choosing an encoding. -/ +def safeBytes {Raw : Type} (meaning : RustModel Raw) (bytes : List AMByte) : Prop := + ∃ decoder, meaning.representation = some decoder ∧ + ∃ raw value, decoder.run bytes = some raw ∧ meaning.decode raw = some value + +theorem safeBytes_view {Raw : Type} (meaning : RustModel Raw) (view : View meaning) + (bytes : List AMByte) : + safeBytes meaning bytes ↔ + Rust.Referent.Safe view.decoder.asStorageDecoder meaning.decode () bytes := by + constructor + · rintro ⟨decoder, installed, raw, value, physical, mathematical⟩ + have same : decoder = view.decoder := Option.some.inj (installed.symm.trans view.installed) + subst decoder + exact ⟨raw, value, by simpa only [BitDecoder.run_asStorageDecoder] using physical, + mathematical⟩ + · rintro ⟨raw, value, physical, mathematical⟩ + exact ⟨view.decoder, view.installed, raw, value, + by simpa only [BitDecoder.run_asStorageDecoder] using physical, mathematical⟩ + +def transfer {Src Dst : Type} (source : RustModel Src) (destination : RustModel Dst) + (sourceState destinationState : Rust.Referent.State) : Prop := + ∀ (sourceView : View source) (destinationView : View destination), + Rust.Referent.Transfer sourceView.decoder.byteSize (safeBytes source) sourceState + destinationView.decoder.byteSize (safeBytes destination) destinationState + +/-- This is evidence of supported reasoning, not a false interpretation of an +unsupported state's byte domain. Forgetting a promise needs no such domain. -/ +inductive Supports {Src Dst : Type} (source : RustModel Src) (destination : RustModel Dst) : + Kind → Kind → Prop where + | forget (kind : Kind) : Supports source destination kind .uninit + | modeled (sourceState destinationState : Rust.Referent.State) + (proof : transfer source destination sourceState destinationState) : + Supports source destination (nativeState sourceState) (nativeState destinationState) + +/-- All four original Rust type arguments retain their meanings. State +metadata is separate from the referent's physical and mathematical decoders. -/ +def transmuteFrom (Src Dst SV DV : Type) [source : RustModel Src] + [destination : RustModel Dst] [sourceState : RustModel SV] + [destinationState : RustModel DV] : Prop := + ∃ first second, sourceState.validityMarker = some first ∧ + destinationState.validityMarker = some second ∧ + Supports source destination first second + +/-- The source contract names exactly these two pairs. Even an accidental +equality of safe domains must not authorize `Safe` here. -/ +def typeIndependentPair (SV DV : Type) : Prop := + (SV = pointer.invariant.Uninit ∧ DV = pointer.invariant.Uninit) ∨ + (SV = pointer.invariant.Initialized ∧ DV = pointer.invariant.Initialized) + +theorem safe_to_initialized (Src Dst : Type) [source : RustModel Src] + [destination : RustModel Dst] (initialized : RustModel.initializedRepresentation Src) : + transmuteFrom Src Dst SafeState InitializedState := by + refine ⟨_, _, rfl, rfl, ?_⟩ + apply Supports.modeled .safe .initialized + intro sv dv same bytes admitted + refine ⟨admitted.1.trans same, ?_⟩ + obtain ⟨decoder, installed, raw, _, physical, _⟩ := admitted.2 + have initializes : decoder.Initialized := by + simpa only [RustModel.initializedRepresentation, installed] using initialized + exact initializes bytes raw physical + +theorem initialized_to_safe (Src Dst : Type) [source : RustModel Src] + [destination : RustModel Dst] (complete : RustModel.completeRepresentation Dst) : + transmuteFrom Src Dst InitializedState SafeState := by + refine ⟨_, _, rfl, rfl, ?_⟩ + apply Supports.modeled .initialized .safe + intro sv dv same bytes admitted + refine ⟨admitted.1.trans same, dv.decoder, dv.installed, ?_⟩ + have completes := complete + simp only [RustModel.completeRepresentation, dv.installed] at completes + exact completes bytes (admitted.1.trans same) admitted.2 + +theorem initialized_identity (Src Dst : Type) [RustModel Src] [RustModel Dst] : + transmuteFrom Src Dst InitializedState InitializedState := by + refine ⟨_, _, rfl, rfl, ?_⟩ + exact Supports.modeled .initialized .initialized + (fun sv dv => Rust.Referent.initialized_identity _ _ _ _) + +theorem forget (Src Dst V : Type) [RustModel Src] [RustModel Dst] + [meaning : RustModel V] (known : ∃ marker, meaning.validityMarker = some marker) : + transmuteFrom Src Dst V UninitState := by + obtain ⟨marker, identified⟩ := known + exact ⟨marker, .uninit, identified, rfl, Supports.forget marker⟩ + +/-- Wrapper proofs reduce to their two actual decoder domains. The theorem +does not assume a reversible mathematical model or a canonical byte encoding. -/ +theorem safe_transfer_of_implication (Src Dst : Type) [source : RustModel Src] + [destination : RustModel Dst] + (preserves : ∀ bytes, safeBytes source bytes → safeBytes destination bytes) : + transmuteFrom Src Dst SafeState SafeState := by + refine ⟨_, _, rfl, rfl, ?_⟩ + exact Supports.modeled .safe .safe (fun sv dv => + Rust.Referent.safe_transfer_of_implication _ _ _ _ (fun bytes _ => preserves bytes)) + +theorem nativeState_injective : Function.Injective nativeState := by + intro left right same + cases left <;> cases right <;> simp_all [nativeState] + +/-- Eliminate supported reasoning into a real byte-domain implication. This +also justifies forgetting any modeled source state without an interpretation +of the unsupported states. -/ +theorem Supports.sound {Src Dst : Type} {source : RustModel Src} + {destination : RustModel Dst} {first second : Kind} + (supported : Supports source destination first second) : + ∀ sourceState destinationState, + first = nativeState sourceState → second = nativeState destinationState → + transfer source destination sourceState destinationState := by + cases supported with + | forget kind => + intro sourceState destinationState _ destinationIs + cases destinationState <;> simp only [nativeState] at destinationIs + · intro sv dv + exact Rust.Referent.to_uninit _ _ _ _ sourceState + · contradiction + · contradiction + | modeled first second proof => + intro sourceState destinationState sourceIs destinationIs + cases nativeState_injective sourceIs + cases nativeState_injective destinationIs + exact proof + +/-- Expose the actual content implication, independently of its evidence +constructors. The required-contract checks consume this theorem. -/ +theorem transmute_sound (Src Dst SV DV : Type) [source : RustModel Src] + [destination : RustModel Dst] [sourceMeaning : RustModel SV] + [destinationMeaning : RustModel DV] (sourceState destinationState : Rust.Referent.State) + (sourceCode : sourceMeaning.validityMarker = some (nativeState sourceState)) + (destinationCode : destinationMeaning.validityMarker = some (nativeState destinationState)) + (proof : transmuteFrom Src Dst SV DV) : + transfer source destination sourceState destinationState := by + obtain ⟨first, second, sourceIs, destinationIs, supported⟩ := proof + exact supported.sound sourceState destinationState + (Option.some.inj (sourceIs.symm.trans sourceCode)) + (Option.some.inj (destinationIs.symm.trans destinationCode)) + +theorem safe_transfer_iff (Src Dst : Type) [source : RustModel Src] + [destination : RustModel Dst] : + transmuteFrom Src Dst SafeState SafeState ↔ transfer source destination .safe .safe := + ⟨transmute_sound Src Dst SafeState SafeState .safe .safe rfl rfl, + fun proof => ⟨.safe, .safe, rfl, rfl, Supports.modeled .safe .safe proof⟩⟩ + +/-- Equal source and intermediate widths make conditional transfers compose. +The final width remains guarded by the result's own implication. -/ +theorem safe_trans (Src Mid Dst : Type) [source : RustModel Src] + [middle : RustModel Mid] [destination : RustModel Dst] + (first : transmuteFrom Src Mid SafeState SafeState) + (second : transmuteFrom Mid Dst SafeState SafeState) + (same : RustModel.sameSize Src Mid) : + transmuteFrom Src Dst SafeState SafeState := by + apply (safe_transfer_iff Src Dst).mpr + intro sourceView destinationView + obtain ⟨width, _, _, sourceSize, middleSize⟩ := same + cases available : middle.representation with + | none => simp [available] at middleSize + | some decoder => + simp only [sourceView.installed, Option.map_some, Option.some.injEq] at sourceSize + simp only [available, Option.map_some, Option.some.injEq] at middleSize + exact Rust.Referent.transfer_trans _ _ _ _ _ _ .safe .safe .safe + ((safe_transfer_iff Src Mid).mp first sourceView ⟨decoder, available⟩) + ((safe_transfer_iff Mid Dst).mp second ⟨decoder, available⟩ destinationView) + (sourceSize.trans middleSize.symm) + +end Zerocopy.Referent diff --git a/verification/aeneas/lean/ReferentWrappers.lean b/verification/aeneas/lean/ReferentWrappers.lean new file mode 100644 index 0000000000..28c275efb9 --- /dev/null +++ b/verification/aeneas/lean/ReferentWrappers.lean @@ -0,0 +1,102 @@ +/- 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 ReferentValidity +import all RustModel +import all ModelPrelude +@[expose] public section + +/-! +A transparent wrapper has its payload's safe byte domain when its physical +decoder maps payload values and its mathematical decoder admits exactly those +mapped values that the payload admits. These two premises refer to the actual +providers. They require neither a preferred encoding nor an inhabited payload. + +The equivalences below concern stored bytes only. In particular, the Cell and +UnsafeCell results do not supply aliasing or mutation permissions. +-/ + +open Aeneas.Std AeneasSpecs Rust.Storage +namespace Zerocopy.Referent + +/-- Every successful mapped physical result comes from a payload. It therefore +suffices to compare mathematical admission on those mapped values; no inverse +function or model-value equality is needed. A missing payload decoder leaves +both safe domains empty. -/ +theorem safeBytes_wrapper_iff {A B : Type} [ma : RustModel A] [mb : RustModel B] + (wrap : A → B) + (representation : mb.representation = wrapperRepresentation wrap) + (admission : ∀ raw, (∃ value, mb.decode (wrap raw) = some value) ↔ + ∃ value, ma.decode raw = some value) + (bytes : List AMByte) : safeBytes mb bytes ↔ safeBytes ma bytes := by + cases available : ma.representation with + | none => simp [safeBytes, representation, wrapperRepresentation, available] + | some decoder => + constructor + · rintro ⟨outer, installed, wrapped, value, physical, mathematical⟩ + have sameDecoder : outer = decoder.map wrap := by + apply Option.some.inj + rw [← installed, representation, wrapperRepresentation, available] + rfl + subst outer + rw [BitDecoder.run_map] at physical + cases language : decoder.run bytes with + | none => simp [language] at physical + | some raw => + have sameValue : wrap raw = wrapped := by simpa [language] using physical + subst wrapped + obtain ⟨mathematical, mathematicalChild⟩ := (admission raw).mp ⟨value, mathematical⟩ + exact ⟨decoder, available, raw, mathematical, language, mathematicalChild⟩ + · rintro ⟨actual, installed, raw, value, physical, mathematical⟩ + have sameDecoder : actual = decoder := Option.some.inj (installed.symm.trans available) + subst actual + obtain ⟨mathematical, mathematicalWrapper⟩ := (admission raw).mpr ⟨value, mathematical⟩ + refine ⟨decoder.map wrap, ?_, wrap raw, mathematical, ?_, mathematicalWrapper⟩ + · simp only [representation, wrapperRepresentation, available, Option.map_some] + · rw [BitDecoder.run_map, physical] + rfl + +theorem safeBytes_manuallyDrop_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) : + safeBytes (inferInstance : RustModel (core.mem.manually_drop.ManuallyDrop T)) bytes ↔ + safeBytes ma bytes := + safeBytes_wrapper_iff core.mem.manually_drop.ManuallyDrop.mk rfl (fun _ => Iff.rfl) bytes + +theorem safeBytes_cell_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) : + safeBytes (inferInstance : RustModel (core.cell.Cell T)) bytes ↔ safeBytes ma bytes := + safeBytes_wrapper_iff core.cell.Cell.mk rfl (fun _ => Iff.rfl) bytes + +theorem safeBytes_unsafeCell_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) : + safeBytes (inferInstance : RustModel (core.cell.UnsafeCell T)) bytes ↔ safeBytes ma bytes := + safeBytes_wrapper_iff core.cell.UnsafeCell.mk rfl (fun _ => Iff.rfl) bytes + +theorem safeBytes_wrapping_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) : + safeBytes (inferInstance : RustModel (Zerocopy.core.num.wrapping.Wrapping T)) bytes ↔ + safeBytes ma bytes := + safeBytes_wrapper_iff Zerocopy.core.num.wrapping.Wrapping.mk rfl (fun _ => Iff.rfl) bytes + +/-- The generated model decodes its child before constructing a wrapper model. +Its actual definition, rather than its physical layout alone, proves admission. -/ +theorem safeBytes_unalign_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) : + safeBytes (inferInstance : RustModel (Zerocopy.wrappers.Unalign T)) bytes ↔ + safeBytes ma bytes := by + apply safeBytes_wrapper_iff Zerocopy.wrappers.Unalign.mk rfl ?_ bytes + intro raw + cases decoded : ma.decode raw <;> + simp [RustModel.decode, Zerocopy.wrappers.Unalign.decode, Zerocopy.wrappers.Unalign.decodeFields, decoded] + +theorem safeBytes_readOnly_iff (T : Type) [ma : RustModel T] (bytes : List AMByte) : + safeBytes (inferInstance : RustModel (Zerocopy.wrappers.read_only_def.ReadOnly T)) bytes ↔ + safeBytes ma bytes := by + apply safeBytes_wrapper_iff Zerocopy.wrappers.read_only_def.ReadOnly.mk rfl ?_ bytes + intro raw + cases decoded : ma.decode raw <;> + simp [RustModel.decode, Zerocopy.wrappers.read_only_def.ReadOnly.decode, + Zerocopy.wrappers.read_only_def.ReadOnly.decodeFields, decoded] + +end Zerocopy.Referent diff --git a/verification/aeneas/lean/RequiredModelContracts/ReferentValidity.lean b/verification/aeneas/lean/RequiredModelContracts/ReferentValidity.lean new file mode 100644 index 0000000000..eed80ef6a6 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/ReferentValidity.lean @@ -0,0 +1,108 @@ +/- 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 Obligations.ReferentValidity +public import ReferentValidity +@[expose] public section + +/-! +These adapters consume a supplied contract for an arbitrary outcome. They keep +the original dictionaries and all retained providers, then recover the direct +byte-content expectation. No adapter executes an extracted function. +-/ +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace Zerocopy.Proofs + +private theorem safeBytes_contents {Raw : Type} (meaning : RustModel Raw) + (physical : BitDecoder Raw) (installed : meaning.representation = some physical) + (bytes : List AMByte) : + Referent.safeBytes meaning bytes ↔ Obligations.contents meaning physical .safe bytes := by + constructor + · rintro ⟨decoder, available, raw, mathematical, language, decoded⟩ + have same : decoder = physical := Option.some.inj (available.symm.trans installed) + subst decoder + exact ⟨raw, mathematical, language, decoded⟩ + · rintro ⟨raw, mathematical, language, decoded⟩ + exact ⟨physical, installed, raw, mathematical, language, decoded⟩ + +private theorem allowed_contents {Raw : Type} (meaning : RustModel Raw) + (physical : BitDecoder Raw) (installed : meaning.representation = some physical) + (state : Rust.Referent.State) (bytes : List AMByte) : + Rust.Referent.Allowed physical.byteSize (Referent.safeBytes meaning) state bytes ↔ + bytes.length = physical.byteSize ∧ Obligations.contents meaning physical state bytes := by + cases state with + | uninit => rfl + | initialized => rfl + | safe => exact and_congr_right (fun _ => safeBytes_contents meaning physical installed bytes) + +private theorem contentTransfer_of_adapter {Src Dst : Type} + (source : RustModel Src) (destination : RustModel Dst) + (sourceState destinationState : Rust.Referent.State) + (transfer : Referent.transfer source destination sourceState destinationState) : + Obligations.installedContentTransfer source destination sourceState destinationState := by + intro sourcePhysical destinationPhysical sourceInstalled destinationInstalled same bytes width content + have result := transfer ⟨sourcePhysical, sourceInstalled⟩ + ⟨destinationPhysical, destinationInstalled⟩ same bytes + ((allowed_contents source sourcePhysical sourceInstalled sourceState bytes).mpr ⟨width, content⟩) + exact (allowed_contents destination destinationPhysical destinationInstalled destinationState bytes).mp result + +@[contract_simps] theorem required_require_transfer (Src Dst SV DV : Type) + (dictionary : pointer.transmute.TransmuteFrom Dst Src SV DV) (run : Result Unit) + (provided : Specs.require_transfer_spec_contract Src Dst SV DV dictionary run) : + Obligations.require_transfer_spec_contract Src Dst SV DV dictionary run := by + intro source destination sourceMeaning destinationMeaning law + letI := law + apply WP.spec_mono provided + rintro _ ⟨_, _, transfer⟩ sourceState destinationState sourceCode destinationCode + apply contentTransfer_of_adapter source destination sourceState destinationState + apply Referent.transmute_sound Src Dst SV DV sourceState destinationState + · cases sourceState <;> exact sourceCode + · cases destinationState <;> exact destinationCode + · exact transfer + +@[contract_simps] theorem required_require_type_independent (Src Dst SV DV : Type) + (dictionary : pointer.invariant.CastableFrom Dst Src SV DV) (run : Result Unit) + (provided : Specs.require_type_independent_spec_contract Src Dst SV DV dictionary run) : + Obligations.require_type_independent_spec_contract Src Dst SV DV dictionary run := by + intro source destination sourceMeaning destinationMeaning law + letI := law + apply WP.spec_mono provided + rintro _ ⟨_, _, pair⟩ + exact pair + +@[contract_simps] theorem required_compose_safe_transfers (Src Mid Dst : Type) + (first : pointer.transmute.TransmuteFrom Mid Src pointer.invariant.Safe pointer.invariant.Safe) + (second : pointer.transmute.TransmuteFrom Dst Mid pointer.invariant.Safe pointer.invariant.Safe) + (run : Result Unit) + (provided : Specs.compose_safe_transfers_spec_contract Src Mid Dst first second run) : + Obligations.compose_safe_transfers_spec_contract Src Mid Dst first second run := by + intro source middle destination firstLaw secondLaw same + letI := firstLaw + letI := secondLaw + apply WP.spec_mono (provided same) + rintro _ ⟨_, _, transfer⟩ + apply contentTransfer_of_adapter source destination .safe .safe + exact Referent.transmute_sound Src Dst pointer.invariant.Safe pointer.invariant.Safe + .safe .safe rfl rfl transfer + +@[contract_simps] theorem required_concrete_transfers (run : Result Unit) + (provided : Specs.concrete_transfers_spec_contract run) : + Obligations.concrete_transfers_spec_contract run := by + apply WP.spec_mono provided + rintro _ ⟨_, _, first, second, pair⟩ + refine ⟨?_, ?_, pair⟩ + · exact contentTransfer_of_adapter modelBool (modelUScalar .U8) .safe .initialized + (Referent.transmute_sound Bool U8 pointer.invariant.Safe pointer.invariant.Initialized + .safe .initialized rfl rfl first) boolDecoder u8BitDecoder rfl rfl + · exact contentTransfer_of_adapter (modelUScalar .U8) modelBool .initialized .uninit + (Referent.transmute_sound U8 Bool pointer.invariant.Initialized pointer.invariant.Uninit + .initialized .uninit rfl rfl second) u8BitDecoder boolDecoder rfl rfl + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RustModel.lean b/verification/aeneas/lean/RustModel.lean index 57f3eb1129..2ee3eae4bd 100644 --- a/verification/aeneas/lean/RustModel.lean +++ b/verification/aeneas/lean/RustModel.lean @@ -28,6 +28,16 @@ transferred from the raw representation without a second runtime check. open Lean Lean.Meta Aeneas.Std namespace AeneasSpecs +/-- A validity marker describes a referent promise, even though its Rust +carrier is uninhabited and has no value to decode. AsInitialized is identified +here without supplying an interpretation of its permitted byte contents. -/ +inductive ValidityMarker where + | uninit + | asInitialized + | initialized + | safe + deriving DecidableEq, Repr + /-- The provider fixes both the mathematical type and the decoder. Two providers may share a Model type while assigning different meanings or admission domains to the same raw value, so contracts retain the actual provider explicitly. -/ @@ -41,6 +51,10 @@ class RustModel (Raw : Type u) where /-- A preferred physical representation. Operations check it before use. Universally varying this field retains every accepted representation. -/ representationChoice : Raw → List Rust.Storage.AMByte := fun _ => [] + /-- Optional type-level meaning for pointer validity markers. Ordinary + value types leave this absent. A Validity law requires an explicit code and + checks it against the actual associated constant; absence never means Uninit. -/ + validityMarker : Option ValidityMarker := none -- The associated type is transparent so ordinary rewriting and coercions can -- identify a retained provider's Model with its named mathematical carrier. diff --git a/verification/aeneas/projections/ModelShapes.lean b/verification/aeneas/projections/ModelShapes.lean index 980cfca212..6c6427b2b9 100644 --- a/verification/aeneas/projections/ModelShapes.lean +++ b/verification/aeneas/projections/ModelShapes.lean @@ -81,9 +81,15 @@ derive_model_shape Zerocopy.pointer.invariant.Shared with 0 type parameters derive_model_shape Zerocopy.pointer.invariant.Safe with 0 type parameters -derive_model_shape Zerocopy.trait_checks.XorCodec with 0 type parameters +derive_model_shape Zerocopy.pointer.invariant.ValidityKind with 0 type parameters -derive_model_shape Zerocopy.trait_checks.Forward with 1 type parameters +derive_model_shape Zerocopy.pointer.invariant.Uninit with 0 type parameters + +derive_model_shape Zerocopy.pointer.invariant.AsInitialized with 0 type parameters derive_model_shape Zerocopy.wrappers.Unalign with 1 type parameters +derive_model_shape Zerocopy.trait_checks.XorCodec with 0 type parameters + +derive_model_shape Zerocopy.trait_checks.Forward with 1 type parameters + diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean index 2989e63686..cbaa064b2e 100644 --- a/verification/aeneas/projections/Models.lean +++ b/verification/aeneas/projections/Models.lean @@ -107,12 +107,21 @@ check_model_binding Zerocopy.pointer.invariant.Shared with 0 type parameters derive_rust_model Zerocopy.pointer.invariant.Safe with 0 type parameters check_model_binding Zerocopy.pointer.invariant.Safe with 0 type parameters +derive_rust_model Zerocopy.pointer.invariant.ValidityKind with 0 type parameters +check_model_binding Zerocopy.pointer.invariant.ValidityKind with 0 type parameters + +derive_rust_model Zerocopy.pointer.invariant.Uninit with 0 type parameters +check_model_binding Zerocopy.pointer.invariant.Uninit with 0 type parameters + +derive_rust_model Zerocopy.pointer.invariant.AsInitialized with 0 type parameters +check_model_binding Zerocopy.pointer.invariant.AsInitialized with 0 type parameters + +derive_rust_model Zerocopy.wrappers.Unalign with 1 type parameters with_physical 0 +check_model_binding Zerocopy.wrappers.Unalign with 1 type parameters + derive_rust_model Zerocopy.trait_checks.XorCodec with 0 type parameters check_model_binding Zerocopy.trait_checks.XorCodec with 0 type parameters derive_rust_model Zerocopy.trait_checks.Forward with 1 type parameters check_model_binding Zerocopy.trait_checks.Forward with 1 type parameters -derive_rust_model Zerocopy.wrappers.Unalign with 1 type parameters with_physical 0 -check_model_binding Zerocopy.wrappers.Unalign with 1 type parameters - diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index abc9142065..955c877fac 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -609,6 +609,46 @@ spec cast_unsized_check_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.cast_unsized_check_spec for Zerocopy.pointer.cast.checks.assert_cast_unsized with 7 +check_model_inputs Zerocopy.pointer.referent_checks.require_transfer with 4 type parameters +aeneas_spec_begin +spec require_transfer_spec + for @Zerocopy.pointer.referent_checks.require_transfer with 4 type parameters + ensures(raw) _ => Referent.transmuteFrom Src Dst SV DV +aeneas_spec_end +check_spec_binding Zerocopy.Specs.require_transfer_spec for Zerocopy.pointer.referent_checks.require_transfer with 5 + +check_model_inputs Zerocopy.pointer.referent_checks.require_type_independent with 4 type parameters +aeneas_spec_begin +spec require_type_independent_spec + for @Zerocopy.pointer.referent_checks.require_type_independent with 4 type parameters + ensures(raw) _ => Referent.typeIndependentPair SV DV +aeneas_spec_end +check_spec_binding Zerocopy.Specs.require_type_independent_spec for Zerocopy.pointer.referent_checks.require_type_independent with 5 + +check_model_inputs Zerocopy.pointer.referent_checks.compose_safe_transfers with 3 type parameters +aeneas_spec_begin +spec compose_safe_transfers_spec + for @Zerocopy.pointer.referent_checks.compose_safe_transfers with 3 type parameters + requires(raw) first_size : AeneasSpecs.RustModel.sameSize Src Mid + ensures(raw) _ => Referent.transmuteFrom Src Dst + Zerocopy.pointer.invariant.Safe Zerocopy.pointer.invariant.Safe +aeneas_spec_end +check_spec_binding Zerocopy.Specs.compose_safe_transfers_spec for Zerocopy.pointer.referent_checks.compose_safe_transfers with 5 + +check_model_inputs Zerocopy.pointer.referent_checks.concrete_transfers with 0 type parameters +aeneas_spec_begin +spec concrete_transfers_spec + for @Zerocopy.pointer.referent_checks.concrete_transfers with 0 type parameters + ensures(raw) _ => + Referent.transmuteFrom Bool U8 + Zerocopy.pointer.invariant.Safe Zerocopy.pointer.invariant.Initialized ∧ + Referent.transmuteFrom U8 Bool + Zerocopy.pointer.invariant.Initialized Zerocopy.pointer.invariant.Uninit ∧ + Referent.typeIndependentPair Zerocopy.pointer.invariant.Initialized + Zerocopy.pointer.invariant.Initialized +aeneas_spec_end +check_spec_binding Zerocopy.Specs.concrete_transfers_spec for Zerocopy.pointer.referent_checks.concrete_transfers with 0 + check_model_inputs Zerocopy.split_at.split_right_len with 0 type parameters aeneas_spec_begin spec split_right_len_spec diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean index 16820cd214..64f15c57b8 100644 --- a/verification/aeneas/projections/TraitLaws.lean +++ b/verification/aeneas/projections/TraitLaws.lean @@ -9,6 +9,7 @@ those terms. -/ module public import Zerocopy.Funs public import TraitLawsSupport +public import ReferentValidity public import LayoutModel @[expose] public section open Aeneas Aeneas.Std @@ -27,17 +28,19 @@ trait_dictionary @Zerocopy.FromZeros trait_dictionary @Zerocopy.FromBytes trait_dictionary @Zerocopy.IntoBytes trait_dictionary @Zerocopy.Unaligned +trait_dictionary @Zerocopy.pointer.invariant.Validity +trait_dictionary @Zerocopy.pointer.invariant.CastableFrom +trait_dictionary @Zerocopy.pointer.transmute.TransmuteFrom trait_dictionary @Zerocopy.trait_checks.ByteCodec trait_dictionary @Zerocopy.util.macro_util.transmute_copy.StaticAssert trait_invariant from_zeros_valid for @Zerocopy.FromZeros with 1 type parameters where self => AeneasSpecs.RustModel.zeroRepresentation Self -trait_invariant unaligned for @Zerocopy.Unaligned with 1 type parameters where self => - Zerocopy.RustLayout.align Self = 1#usize +trait_invariant transmute_from for @Zerocopy.pointer.transmute.TransmuteFrom with 4 type parameters where self => + Referent.transmuteFrom Src Self SV DV -trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type parameters where self => - ∀ byte, (do let encoded ← self.encode byte; self.decode encoded) - ⦃ result => result = byte ⦄ +trait_invariant castable_from for @Zerocopy.pointer.invariant.CastableFrom with 4 type parameters where self => + Referent.typeIndependentPair SV DV trait_invariant into_bytes_initialized for @Zerocopy.IntoBytes with 1 type parameters where self => AeneasSpecs.RustModel.initializedRepresentation Self ∧ @@ -46,4 +49,14 @@ trait_invariant into_bytes_initialized for @Zerocopy.IntoBytes with 1 type param trait_invariant from_bytes_valid for @Zerocopy.FromBytes with 1 type parameters where self => AeneasSpecs.RustModel.completeRepresentation Self +trait_invariant validity_kind for @Zerocopy.pointer.invariant.Validity with 1 type parameters where self => + Referent.kindMatches Self self.KIND + +trait_invariant unaligned for @Zerocopy.Unaligned with 1 type parameters where self => + Zerocopy.RustLayout.align Self = 1#usize + +trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type parameters where self => + ∀ byte, (do let encoded ← self.encode byte; self.decode encoded) + ⦃ result => result = byte ⦄ + end Zerocopy.TraitLaws diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py index d3807a4e63..314a0d99a4 100644 --- a/verification/aeneas/tests/test_inline.py +++ b/verification/aeneas/tests/test_inline.py @@ -95,6 +95,26 @@ def setUp(self): def parse(self, source): return inline.parse_file(source, syntax(source)) + def test_parameterized_referent_sites_pass_the_source_census(self): + source = (ROOT / 'zerocopy/src/pointer/transmute.rs').read_text() + annotations = self.parse(source) + law = next(row for row in annotations if row['kind'] == 'trait') + self.assertEqual(law['syntax'], 'TransmuteFrom') + self.assertEqual(law['generics'], ['Self', 'Src', 'SV', 'DV']) + markers = [row for row in annotations if row['kind'] == 'trait-impl'] + self.assertEqual(len(markers), 16) + self.assertTrue(all(row['theorem'] is None for row in markers)) + conditional = [row for row in markers + if any(bound['subject'] is None for bound in row['trait_bounds'])] + self.assertEqual(len(conditional), 2) + self.assertTrue(all(bound['argument_count'] == 3 + for row in conditional for bound in row['trait_bounds'])) + invariant_source = (ROOT / 'zerocopy/src/pointer/invariant.rs').read_text() + invariant_annotations = self.parse(invariant_source) + castable = next(row for row in invariant_annotations + if row['kind'] == 'trait' and row['syntax'] == 'CastableFrom') + self.assertEqual(castable['generics'], ['Self', 'ST', 'SV', 'DV']) + def test_parameterized_trait_declaration_retains_marker_bound_census(self): source = ('/// ```aeneas\n/// invariant law for self => True\n/// ```\n' 'pub unsafe trait TransmuteFrom {}') diff --git a/zerocopy/src/pointer/invariant.rs b/zerocopy/src/pointer/invariant.rs index ca07f01cbc..fe7fc8b7f0 100644 --- a/zerocopy/src/pointer/invariant.rs +++ b/zerocopy/src/pointer/invariant.rs @@ -101,6 +101,13 @@ pub trait Alignment: Sealed { /// These conditions describe only exact reinterpretations. Shrinking /// projections may have validity that depends on the relationship between the /// projected region and bytes outside it, and require additional reasoning. +/// +/// The checked invariant below identifies the state using `KIND` and the +/// retained type model. It does not yet interpret `AsInitialized` contents. +/// +/// ```aeneas +/// invariant validity_kind for self => Referent.kindMatches Self self.KIND +/// ``` pub unsafe trait Validity: Sealed { const KIND: ValidityKind; } @@ -184,6 +191,9 @@ pub enum Uninit {} // function of any property of `T` other than its bit validity (in fact, it's // not even a property of `T`'s bit validity, but this is more than we are // required to uphold). +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl Validity for Uninit { const KIND: ValidityKind = ValidityKind::Uninit; } @@ -218,6 +228,9 @@ unsafe impl Validity for Uninit { pub enum AsInitialized {} // SAFETY: `AsInitialized`'s validity is well-defined for all `T: ?Sized`, and // is not a function of any property of `T` other than its bit validity. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl Validity for AsInitialized { const KIND: ValidityKind = ValidityKind::AsInitialized; } @@ -229,6 +242,9 @@ pub enum Initialized {} // not a function of any property of `T` other than its bit validity (in fact, // it's not even a property of `T`'s bit validity, but this is more than we are // required to uphold). +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl Validity for Initialized { const KIND: ValidityKind = ValidityKind::Initialized; } @@ -238,6 +254,9 @@ unsafe impl Validity for Initialized { pub enum Safe {} // SAFETY: `Safe`'s validity is well-defined for all `T: ?Sized`, and is not a // function of any property of `T` other than its bit validity. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl Validity for Safe { const KIND: ValidityKind = ValidityKind::Safe; } @@ -253,11 +272,21 @@ unsafe impl Validity for Safe { /// /// `DT: CastableFrom` is sound if `SV = DV = Uninit` or `SV = DV = /// Initialized`. +/// +/// ```aeneas +/// invariant castable_from for self => Referent.typeIndependentPair SV DV +/// ``` pub unsafe trait CastableFrom {} // SAFETY: `SV = DV = Uninit`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl CastableFrom for DT {} // SAFETY: `SV = DV = Initialized`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl CastableFrom for DT {} /// [`Ptr`](crate::Ptr) referents that permit unsynchronized read operations. diff --git a/zerocopy/src/pointer/mod.rs b/zerocopy/src/pointer/mod.rs index 910a91c19b..4759396748 100644 --- a/zerocopy/src/pointer/mod.rs +++ b/zerocopy/src/pointer/mod.rs @@ -15,6 +15,7 @@ mod inner; pub mod invariant; mod ptr; +mod referent_checks; pub mod transmute; pub use inner::PtrInner; diff --git a/zerocopy/src/pointer/referent_checks.rs b/zerocopy/src/pointer/referent_checks.rs new file mode 100644 index 0000000000..396fcfd53c --- /dev/null +++ b/zerocopy/src/pointer/referent_checks.rs @@ -0,0 +1,80 @@ +// Copyright 2026 The Fuchsia Authors +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// 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. + +//! Verification clients for the actual Rust validity dictionaries. +//! +//! The bodies need no memory access. Their postconditions demonstrate that a +//! Rust bound supplies the exact law checked at its implementation, including +//! when execution does not use the dictionary. These are content implications, +//! not proofs that a pointer cast or simultaneous access is permitted. + +#![allow(dead_code)] + +use super::{ + invariant::{CastableFrom, Initialized, Safe, Uninit}, + TransmuteFrom, +}; + +/// ```aeneas +/// spec require_transfer_spec +/// ensures(raw) _ => Referent.transmuteFrom Src Dst SV DV +/// ``` +fn require_transfer() +where + Dst: TransmuteFrom + ?Sized, +{ +} + +/// ```aeneas +/// spec require_type_independent_spec +/// ensures(raw) _ => Referent.typeIndependentPair SV DV +/// ``` +fn require_type_independent() +where + Dst: CastableFrom + ?Sized, +{ +} + +/// Intermediate width equality is a real premise: each individual transfer +/// promises nothing when its own endpoint sizes differ. +/// +/// ```aeneas +/// spec compose_safe_transfers_spec +/// requires(raw) first_size : AeneasSpecs.RustModel.sameSize Src Mid +/// ensures(raw) _ => Referent.transmuteFrom Src Dst +/// Zerocopy.pointer.invariant.Safe Zerocopy.pointer.invariant.Safe +/// ``` +fn compose_safe_transfers() +where + Mid: TransmuteFrom, + Dst: TransmuteFrom, +{ +} + +/// Select real blanket and wrapper implementations, rather than supplying +/// standalone Lean dictionaries that merely resemble them. +/// +/// ```aeneas +/// spec concrete_transfers_spec +/// ensures(raw) _ => +/// Referent.transmuteFrom Bool U8 +/// Zerocopy.pointer.invariant.Safe Zerocopy.pointer.invariant.Initialized ∧ +/// Referent.transmuteFrom U8 Bool +/// Zerocopy.pointer.invariant.Initialized Zerocopy.pointer.invariant.Uninit ∧ +/// Referent.typeIndependentPair Zerocopy.pointer.invariant.Initialized +/// Zerocopy.pointer.invariant.Initialized +/// ``` +fn concrete_transfers() { + require_transfer::(); + require_transfer::<[u8; 4], u32, Initialized, Safe>(); + require_transfer::(); + require_transfer::, u8, Safe, Safe>(); + require_type_independent::(); + require_type_independent::(); +} diff --git a/zerocopy/src/pointer/transmute.rs b/zerocopy/src/pointer/transmute.rs index 114e5bf0f3..42da793246 100644 --- a/zerocopy/src/pointer/transmute.rs +++ b/zerocopy/src/pointer/transmute.rs @@ -338,6 +338,10 @@ where /// /// If the referents are not the same size, then `Dst: TransmuteFrom` conveys no safety guarantee. +/// +/// ```aeneas +/// invariant transmute_from for self => Referent.transmuteFrom Src Self SV DV +/// ``` pub unsafe trait TransmuteFrom {} /// Carries the ability to perform a size-preserving cast or conversion from a @@ -366,6 +370,9 @@ impl SizeEq for T { // SAFETY: `Src: IntoBytes` guarantees that every valid representation of // `Src` is entirely initialized. If the referent widths agree, those same // bytes satisfy `Initialized` for `Dst`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for Dst where Src: IntoBytes + ?Sized, @@ -376,6 +383,9 @@ where // SAFETY: Since `Dst: FromBytes`, any initialized bit pattern may appear in the // referent of a `Ptr`. If the referent widths agree, // `Initialized` source bytes therefore satisfy `Safe` for `Dst`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for Dst where Src: ?Sized, @@ -390,6 +400,9 @@ where // SAFETY: The set of allowed bit patterns in the referent of any `Initialized` // `Ptr` is the same regardless of referent type. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for Dst where Src: ?Sized, @@ -404,6 +417,9 @@ where // SAFETY: A `Dst` with validity `Uninit` permits any byte sequence, and // therefore can be transmuted from any value. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for Dst where Src: ?Sized, @@ -420,10 +436,16 @@ where // // `ManuallyDrop` is guaranteed to have the same layout and bit validity as // `T` +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for ManuallyDrop {} // SAFETY: By the preceding safety proof, `ManuallyDrop` and `T` have the // same bit validity. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom, Safe, Safe> for T {} // SAFETY: By the preceding safety proof, `ManuallyDrop` and `T` have the @@ -435,10 +457,16 @@ const _: () = // SAFETY: // - `Unalign` promises to have the same size as `T`. // - `Unalign` promises to have the same validity as `T`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for Unalign {} // SAFETY: By the preceding safety proof, `Unalign` and `T` have the // same bit validity. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom, Safe, Safe> for T {} // SAFETY: By the preceding safety proof, `Unalign` and `T` have the @@ -476,10 +504,16 @@ const _: () = unsafe { unsafe_impl_shared_compatible!(T => T, Unalign) }; // #[repr(transparent)] // pub struct Wrapping(pub T); // ``` +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for Wrapping {} // SAFETY: By the preceding safety proof, `Wrapping` and `T` have the // same bit validity. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom, Safe, Safe> for T {} // SAFETY: By the preceding safety proof, `Wrapping` and `T` have the @@ -506,10 +540,16 @@ const _: () = unsafe { unsafe_impl_shared_compatible!(T => T, Wrapping) }; // `UnsafeCell` has the same in-memory representation as its inner type // `T`. A consequence of this guarantee is that it is possible to convert // between `T` and `UnsafeCell`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for UnsafeCell {} // SAFETY: By the preceding safety proof, `UnsafeCell` and `T` have the // same bit validity. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom, Safe, Safe> for T {} // SAFETY: By the preceding safety proof, `UnsafeCell` and `T` have the @@ -537,10 +577,16 @@ const _: () = // `UnsafeCell` has the same in-memory representation as its inner type // `T`. A consequence of this guarantee is that it is possible to convert // between `T` and `UnsafeCell`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for Cell {} // SAFETY: By the preceding safety proof, `Cell` and `T` have the // same bit validity. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom, Safe, Safe> for T {} // SAFETY: By the preceding safety proof, `Cell` and `T` have the @@ -555,6 +601,9 @@ impl_transitive_size_eq!(T: ?Sized => Cell => T => UnsafeCell); // above. Thus both conditional bounds apply: `T: TransmuteFrom, Safe, // Safe>` preserves bit validity, and `UnsafeCell: TransmuteFrom` preserves it again. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom, Safe, Safe> for UnsafeCell where T: TransmuteFrom, Safe, Safe>, @@ -568,6 +617,9 @@ impl_transitive_size_eq!(T: ?Sized => UnsafeCell => T => Cell); // conditional bounds apply: `T: TransmuteFrom, Safe, Safe>` // preserves bit validity, and `Cell: TransmuteFrom` preserves // it again. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom, Safe, Safe> for Cell where T: TransmuteFrom, Safe, Safe>, diff --git a/zerocopy/src/wrappers.rs b/zerocopy/src/wrappers.rs index ea3e97f116..5fe929b8b2 100644 --- a/zerocopy/src/wrappers.rs +++ b/zerocopy/src/wrappers.rs @@ -726,10 +726,16 @@ const _: () = { // SAFETY: `ReadOnly` is a `#[repr(transparent)]` wrapper around `T`, and so // it has the same bit validity as `T`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom for ReadOnly {} // SAFETY: `ReadOnly` is a `#[repr(transparent)]` wrapper around `T`, and so // it has the same bit validity as `T`. +/// ```aeneas +/// invariant_proof +/// ``` unsafe impl TransmuteFrom, Safe, Safe> for T {} impl Default for ReadOnly {