From dec2c0063973f7a9814350418747cfd92beb686f Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 15 Oct 2026 11:53:50 -0400 Subject: [PATCH] Require realizable source representations for IntoBytes An initialized physical decoder can reject every byte string. Its initialization law then holds without supplying any bytes for an admitted source value, so that law alone cannot justify a conversion out of the value. Require each mathematically admitted source value to have a physical representation. Prove this stronger IntoBytes invariant for the existing primitive, array, and wrapper implementations. Keep initialization over the full physical decoding domain, independently of library admission. The existence requirement permits multiple representations of one value and remains vacuous for uninhabited sources. Regression examples cover both cases, empty arrays, and an initialized decoder that cannot represent one of its admitted values. gherrit-pr-id: Gdtlvwakxpzsmcwa7vhtmv7d5h63sbw3l Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 8 + verification/aeneas/golden/Types.lean | 4 +- .../aeneas/lean/Proofs/IntoBytes.lean | 156 ++++---- .../aeneas/lean/Proofs/TraitChecks.lean | 22 +- verification/aeneas/lean/RustModel.lean | 8 + .../aeneas/lean/RustRealizability.lean | 334 ++++++++++++++++++ .../aeneas/lean/RustRealizabilityModels.lean | 139 ++++++++ .../aeneas/lean/RustRealizabilityTests.lean | 94 +++++ .../aeneas/projections/TraitLaws.lean | 3 +- zerocopy/src/lib.rs | 3 +- 10 files changed, 684 insertions(+), 87 deletions(-) create mode 100644 verification/aeneas/lean/RustRealizability.lean create mode 100644 verification/aeneas/lean/RustRealizabilityModels.lean create mode 100644 verification/aeneas/lean/RustRealizabilityTests.lean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index adae7cf864..f61ff87f51 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -728,6 +728,14 @@ requires an available physical decoder and initialization over its entire accepted domain. Absence is `False`; rejection by the library's mathematical `RustModel.decode` cannot reduce this domain. +The law also requires **source realizability**: each raw value admitted by the +mathematical decoder has at least one physical byte representation. Initialization +alone cannot provide those bytes; an always-rejecting physical decoder would +satisfy it vacuously. The reusable proofs in +[`RustRealizability.lean`](lean/RustRealizability.lean) cover the same primitive, +array, and wrapper families. No default source value, unique encoder, or +inhabitedness assumption is introduced. + There are 59 authored implementation markers: `()`, `bool`, `char`; all twelve signed/unsigned integer carriers; all twelve corresponding `NonZero` carriers and their `Option` forms; `PhantomData`; arrays; `Wrapping`, `ManuallyDrop`, diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index e5c868118c..2b8e48c0a6 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -346,13 +346,13 @@ structure FromBytes (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit /-- Trait declaration: [zerocopy::IntoBytes] - Source: 'src/lib.rs', lines 6017:0-6490:1 + Source: 'src/lib.rs', lines 6018:0-6491:1 Visibility: public -/ structure IntoBytes (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit /-- Trait declaration: [zerocopy::Unaligned] - Source: 'src/lib.rs', lines 6628:0-6635:1 + Source: 'src/lib.rs', lines 6629:0-6636:1 Visibility: public -/ structure Unaligned (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit diff --git a/verification/aeneas/lean/Proofs/IntoBytes.lean b/verification/aeneas/lean/Proofs/IntoBytes.lean index 7cc9f8408f..e8542c972c 100644 --- a/verification/aeneas/lean/Proofs/IntoBytes.lean +++ b/verification/aeneas/lean/Proofs/IntoBytes.lean @@ -10,6 +10,8 @@ those terms. -/ module public import Specs public import TraitLaws +public import RustRealizability +public import RustRealizabilityModels public import Proofs.TraitChecks @[expose] public section @@ -26,52 +28,52 @@ namespace Zerocopy.Proofs @[instance] theorem I8.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized I8 Zerocopy.I8.Insts.ZerocopyIntoBytes := - ⟨initializedIScalar .I8⟩ + ⟨⟨initializedIScalar .I8, realizableIScalar .I8⟩⟩ @[instance] theorem U16.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized U16 Zerocopy.U16.Insts.ZerocopyIntoBytes := - ⟨initializedUScalar .U16⟩ + ⟨⟨initializedUScalar .U16, realizableUScalar .U16⟩⟩ @[instance] theorem I16.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized I16 Zerocopy.I16.Insts.ZerocopyIntoBytes := - ⟨initializedIScalar .I16⟩ + ⟨⟨initializedIScalar .I16, realizableIScalar .I16⟩⟩ @[instance] theorem U32.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized U32 Zerocopy.U32.Insts.ZerocopyIntoBytes := - ⟨initializedUScalar .U32⟩ + ⟨⟨initializedUScalar .U32, realizableUScalar .U32⟩⟩ @[instance] theorem I32.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized I32 Zerocopy.I32.Insts.ZerocopyIntoBytes := - ⟨initializedIScalar .I32⟩ + ⟨⟨initializedIScalar .I32, realizableIScalar .I32⟩⟩ @[instance] theorem U64.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized U64 Zerocopy.U64.Insts.ZerocopyIntoBytes := - ⟨initializedUScalar .U64⟩ + ⟨⟨initializedUScalar .U64, realizableUScalar .U64⟩⟩ @[instance] theorem I64.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized I64 Zerocopy.I64.Insts.ZerocopyIntoBytes := - ⟨initializedIScalar .I64⟩ + ⟨⟨initializedIScalar .I64, realizableIScalar .I64⟩⟩ @[instance] theorem U128.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized U128 Zerocopy.U128.Insts.ZerocopyIntoBytes := - ⟨initializedUScalar .U128⟩ + ⟨⟨initializedUScalar .U128, realizableUScalar .U128⟩⟩ @[instance] theorem I128.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized I128 Zerocopy.I128.Insts.ZerocopyIntoBytes := - ⟨initializedIScalar .I128⟩ + ⟨⟨initializedIScalar .I128, realizableIScalar .I128⟩⟩ @[instance] theorem Usize.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized Usize Zerocopy.Usize.Insts.ZerocopyIntoBytes := - ⟨initializedUScalar .Usize⟩ + ⟨⟨initializedUScalar .Usize, realizableUScalar .Usize⟩⟩ @[instance] theorem Isize.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized Isize Zerocopy.Isize.Insts.ZerocopyIntoBytes := - ⟨initializedIScalar .Isize⟩ + ⟨⟨initializedIScalar .Isize, realizableIScalar .Isize⟩⟩ @[instance] theorem Char.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized Char Zerocopy.Char.Insts.ZerocopyIntoBytes := - ⟨Rust.Storage.BitDecoder.filterMap_initialized _ _ - (Rust.Storage.integerDecoder_initialized 4 .little)⟩ + ⟨⟨Rust.Storage.BitDecoder.filterMap_initialized _ _ + (Rust.Storage.integerDecoder_initialized 4 .little), realizableChar⟩⟩ -- Zero rejects NonZero construction; for Option it denotes a successfully -- decoded None. Initialization follows the same full integer carrier. @@ -79,62 +81,62 @@ namespace Zerocopy.Proofs @[instance] theorem core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U8 core.num.niche_types.NonZeroU8Inner) Zerocopy.core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩ + ⟨⟨initializedNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner, realizableNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I8 core.num.niche_types.NonZeroI8Inner) Zerocopy.core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩ + ⟨⟨initializedNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner, realizableNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U16 core.num.niche_types.NonZeroU16Inner) Zerocopy.core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩ + ⟨⟨initializedNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner, realizableNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I16 core.num.niche_types.NonZeroI16Inner) Zerocopy.core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩ + ⟨⟨initializedNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner, realizableNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U32 core.num.niche_types.NonZeroU32Inner) Zerocopy.core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩ + ⟨⟨initializedNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner, realizableNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I32 core.num.niche_types.NonZeroI32Inner) Zerocopy.core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩ + ⟨⟨initializedNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner, realizableNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U64 core.num.niche_types.NonZeroU64Inner) Zerocopy.core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩ + ⟨⟨initializedNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner, realizableNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I64 core.num.niche_types.NonZeroI64Inner) Zerocopy.core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩ + ⟨⟨initializedNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner, realizableNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U128 core.num.niche_types.NonZeroU128Inner) Zerocopy.core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩ + ⟨⟨initializedNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner, realizableNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I128 core.num.niche_types.NonZeroI128Inner) Zerocopy.core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩ + ⟨⟨initializedNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner, realizableNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner) Zerocopy.core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩ + ⟨⟨initializedNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner, realizableNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩⟩ @[instance] theorem core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero Isize core.num.niche_types.NonZeroIsizeInner) Zerocopy.core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes := - ⟨initializedNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩ + ⟨⟨initializedNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner, realizableNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩⟩ -- Zero rejects NonZero construction; for Option it denotes a successfully -- decoded None. Initialization follows the same full integer carrier. @@ -142,69 +144,69 @@ namespace Zerocopy.Proofs @[instance] theorem core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U8 core.num.niche_types.NonZeroU8Inner)) Zerocopy.core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩ + ⟨⟨initializedOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner, realizableOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I8 core.num.niche_types.NonZeroI8Inner)) Zerocopy.core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩ + ⟨⟨initializedOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner, realizableOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U16 core.num.niche_types.NonZeroU16Inner)) Zerocopy.core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩ + ⟨⟨initializedOptionNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner, realizableOptionNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I16 core.num.niche_types.NonZeroI16Inner)) Zerocopy.core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩ + ⟨⟨initializedOptionNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner, realizableOptionNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U32 core.num.niche_types.NonZeroU32Inner)) Zerocopy.core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩ + ⟨⟨initializedOptionNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner, realizableOptionNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I32 core.num.niche_types.NonZeroI32Inner)) Zerocopy.core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩ + ⟨⟨initializedOptionNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner, realizableOptionNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U64 core.num.niche_types.NonZeroU64Inner)) Zerocopy.core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩ + ⟨⟨initializedOptionNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner, realizableOptionNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I64 core.num.niche_types.NonZeroI64Inner)) Zerocopy.core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩ + ⟨⟨initializedOptionNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner, realizableOptionNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U128 core.num.niche_types.NonZeroU128Inner)) Zerocopy.core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩ + ⟨⟨initializedOptionNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner, realizableOptionNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I128 core.num.niche_types.NonZeroI128Inner)) Zerocopy.core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩ + ⟨⟨initializedOptionNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner, realizableOptionNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩⟩ @[instance] theorem core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner)) Zerocopy.core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩ + ⟨⟨initializedOptionNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner, realizableOptionNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩⟩ @[instance] theorem core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero Isize core.num.niche_types.NonZeroIsizeInner)) Zerocopy.core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes := - ⟨initializedOptionNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩ + ⟨⟨initializedOptionNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner, realizableOptionNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩⟩ -- No value of T is stored in PhantomData, so this law needs no model or -- trait promise for T, including when T is uninhabited. @[instance] theorem core.marker.PhantomData.Insts.ZerocopyIntoBytes_law (T : Type) : TraitLaws.into_bytes_initialized (Zerocopy.core.marker.PhantomData T) (Zerocopy.core.marker.PhantomData.Insts.ZerocopyIntoBytes T) := - ⟨Rust.Storage.emptyDecoder_initialized _⟩ + ⟨⟨Rust.Storage.emptyDecoder_initialized _, realizablePhantomData T⟩⟩ -- Transparent wrappers inherit the exact incoming dictionary promise. @@ -215,48 +217,54 @@ namespace Zerocopy.Proofs [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : TraitLaws.into_bytes_initialized (Zerocopy.core.num.wrapping.Wrapping T) (Zerocopy.core.num.wrapping.Wrapping.Insts.ZerocopyIntoBytes dictionary) := - ⟨initializedWrapping T - (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + ⟨⟨initializedWrapping T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableWrapping T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩ @[instance] theorem core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes_law {T : Type} (dictionary : IntoBytes T) [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : TraitLaws.into_bytes_initialized (core.mem.manually_drop.ManuallyDrop T) (Zerocopy.core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes dictionary) := - ⟨initializedManuallyDrop T - (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + ⟨⟨initializedManuallyDrop T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableManuallyDrop T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩ @[instance] theorem core.cell.Cell.Insts.ZerocopyIntoBytes_law {T : Type} (dictionary : IntoBytes T) [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : TraitLaws.into_bytes_initialized (core.cell.Cell T) (Zerocopy.core.cell.Cell.Insts.ZerocopyIntoBytes dictionary) := - ⟨initializedCell T - (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + ⟨⟨initializedCell T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableCell T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩ @[instance] theorem core.cell.UnsafeCell.Insts.ZerocopyIntoBytes_law {T : Type} (dictionary : IntoBytes T) [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : TraitLaws.into_bytes_initialized (core.cell.UnsafeCell T) (Zerocopy.core.cell.UnsafeCell.Insts.ZerocopyIntoBytes dictionary) := - ⟨initializedUnsafeCell T - (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + ⟨⟨initializedUnsafeCell T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableUnsafeCell T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩ @[instance] theorem wrappers.Unalign.Insts.ZerocopyIntoBytes_law {T : Type} (dictionary : IntoBytes T) [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : TraitLaws.into_bytes_initialized (Zerocopy.wrappers.Unalign T) (Zerocopy.wrappers.Unalign.Insts.ZerocopyIntoBytes dictionary) := - ⟨initializedWrapperRepresentation Zerocopy.wrappers.Unalign.mk - (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + ⟨⟨initializedWrapperRepresentation Zerocopy.wrappers.Unalign.mk + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableUnalign T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩ @[instance] theorem wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes_law {T : Type} (dictionary : IntoBytes T) [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : TraitLaws.into_bytes_initialized (Zerocopy.wrappers.read_only_def.ReadOnly T) (Zerocopy.wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes dictionary) := - ⟨initializedWrapperRepresentation Zerocopy.wrappers.read_only_def.ReadOnly.mk - (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + ⟨⟨initializedWrapperRepresentation Zerocopy.wrappers.read_only_def.ReadOnly.mk + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableReadOnly T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩ -- The byte-order parameter is phantom. Only the byte array contributes -- storage, and its elements inherit the u8 initialization theorem. @@ -265,96 +273,96 @@ namespace Zerocopy.Proofs (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U16 O) (Zerocopy.byteorder.U16.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.U16.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8)), realizableByteorderU16 O⟩⟩ @[instance] theorem byteorder.U32.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U32 O) (Zerocopy.byteorder.U32.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.U32.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderU32 O⟩⟩ @[instance] theorem byteorder.U64.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U64 O) (Zerocopy.byteorder.U64.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.U64.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderU64 O⟩⟩ @[instance] theorem byteorder.U128.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U128 O) (Zerocopy.byteorder.U128.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.U128.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8)), realizableByteorderU128 O⟩⟩ @[instance] theorem byteorder.Usize.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.Usize O) (Zerocopy.byteorder.Usize.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.Usize.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderUsize O⟩⟩ @[instance] theorem byteorder.I16.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I16 O) (Zerocopy.byteorder.I16.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.I16.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8)), realizableByteorderI16 O⟩⟩ @[instance] theorem byteorder.I32.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I32 O) (Zerocopy.byteorder.I32.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.I32.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderI32 O⟩⟩ @[instance] theorem byteorder.I64.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I64 O) (Zerocopy.byteorder.I64.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.I64.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderI64 O⟩⟩ @[instance] theorem byteorder.I128.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I128 O) (Zerocopy.byteorder.I128.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.I128.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8)), realizableByteorderI128 O⟩⟩ @[instance] theorem byteorder.Isize.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.Isize O) (Zerocopy.byteorder.Isize.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.Isize.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderIsize O⟩⟩ @[instance] theorem byteorder.F32.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.F32 O) (Zerocopy.byteorder.F32.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.F32.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderF32 O⟩⟩ @[instance] theorem byteorder.F64.Insts.ZerocopyIntoBytes_law (O : Type) [meaning : RustModel O] : TraitLaws.into_bytes_initialized (Zerocopy.byteorder.F64 O) (Zerocopy.byteorder.F64.Insts.ZerocopyIntoBytes O) := - ⟨initializedWrapperRepresentation + ⟨⟨initializedWrapperRepresentation (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk) - (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderF64 O⟩⟩ end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/TraitChecks.lean b/verification/aeneas/lean/Proofs/TraitChecks.lean index e70eca529f..22b03b51ff 100644 --- a/verification/aeneas/lean/Proofs/TraitChecks.lean +++ b/verification/aeneas/lean/Proofs/TraitChecks.lean @@ -9,6 +9,7 @@ those terms. -/ module public import Specs public import TraitLaws +public import RustRealizability @[expose] public section /-! @@ -50,15 +51,15 @@ namespace Zerocopy.Proofs -- library decoder's (possibly smaller) admission domain. @[instance] theorem Bool.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized Bool Zerocopy.Bool.Insts.ZerocopyIntoBytes := - ⟨Rust.Storage.boolDecoder_initialized⟩ + ⟨⟨Rust.Storage.boolDecoder_initialized, realizableBool⟩⟩ @[instance] theorem U8.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized U8 Zerocopy.U8.Insts.ZerocopyIntoBytes := - ⟨initializedUScalar .U8⟩ + ⟨⟨initializedUScalar .U8, realizableUScalar .U8⟩⟩ @[instance] theorem Tuple.Insts.ZerocopyIntoBytes_law : TraitLaws.into_bytes_initialized Unit Zerocopy.Tuple.Insts.ZerocopyIntoBytes := - ⟨Rust.Storage.unitDecoder_initialized⟩ + ⟨⟨Rust.Storage.unitDecoder_initialized, realizableUnit⟩⟩ -- The original type, const length, and computational dictionary remain the -- native implementation's prefix. Only the element's provider and law are @@ -68,7 +69,10 @@ namespace Zerocopy.Proofs [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : TraitLaws.into_bytes_initialized (Aeneas.Std.Array T N) (Zerocopy.Array.Insts.ZerocopyIntoBytes N dictionary) := - ⟨RustModel.initialized_array T N (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + ⟨⟨RustModel.initialized_array T N + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, + RustModel.realizable_array T N + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩ -- Calling the real Rust helper selects the existing unsafe impls in Charon. -- The generic impl law proves all lengths; these concrete cases additionally @@ -79,20 +83,20 @@ theorem array_into_bytes_spec : Specs.array_into_bytes_spec := by refine ⟨(), rfl, ?_, ?_, ?_, ?_, ?_⟩ · exact (@TraitLaws.into_bytes_initialized.holds _ (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes) - _ inferInstance) + _ inferInstance).1 · exact (@TraitLaws.into_bytes_initialized.holds _ (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.U8.Insts.ZerocopyIntoBytes) - _ inferInstance) + _ inferInstance).1 · exact (@TraitLaws.into_bytes_initialized.holds _ (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Tuple.Insts.ZerocopyIntoBytes) - _ inferInstance) + _ inferInstance).1 · exact (@TraitLaws.into_bytes_initialized.holds _ (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes) - _ inferInstance) + _ inferInstance).1 · exact (@TraitLaws.into_bytes_initialized.holds _ (Zerocopy.Array.Insts.ZerocopyIntoBytes _ (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)) - _ inferInstance) + _ inferInstance).1 theorem unaligned_alignment_spec : Specs.unaligned_alignment_spec := by intro T dictionary _ law diff --git a/verification/aeneas/lean/RustModel.lean b/verification/aeneas/lean/RustModel.lean index 45c33f0d89..4a54d75ef5 100644 --- a/verification/aeneas/lean/RustModel.lean +++ b/verification/aeneas/lean/RustModel.lean @@ -63,6 +63,14 @@ def RustModel.initializedRepresentation (Raw : Type u) [m : RustModel Raw] : Pro | none => False | some decoder => decoder.Initialized +/-- Every admitted source has some physical representation. This is vacuous +for uninhabited sources and does not require a canonical encoding. -/ +def RustModel.realizableRepresentation (Raw : Type u) [m : RustModel Raw] : Prop := + match m.representation with + | none => False + | some decoder => ∀ raw, @isValid Raw m raw → + ∃ bytes, decoder.run bytes = some raw + /-- Every initialized representation of the physical width admits a language value and a mathematical value through this same provider. Missing physical semantics fail closed. This law does not establish Rust layout correspondence, diff --git a/verification/aeneas/lean/RustRealizability.lean b/verification/aeneas/lean/RustRealizability.lean new file mode 100644 index 0000000000..bb64337299 --- /dev/null +++ b/verification/aeneas/lean/RustRealizability.lean @@ -0,0 +1,334 @@ +/- 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 RustRepresentation +import all RustModel +import all ModelPrelude +import all Rust.Storage +import all RustAeneas.Storage +@[expose] public section + +/-! +Source realizability is conditional on mathematical admission. It supplies a +physical representation of that particular raw value, without imposing a +default value or a unique representation. An uninhabited raw carrier therefore +needs no invented source value. These existence laws leave initialization and +Rust layout correspondence as separate obligations. +-/ + +namespace Rust.Storage + +/-- Integer encoding supplies a representation for every fixed-width word. -/ +theorem integerDecoder_realizable (byteSize : Nat) (endian : Rust.Bytes.Endian) + (word : BitVec (8 * byteSize)) : + ∃ bytes, (integerDecoder byteSize endian).run bytes = some word := by + have bound : word.toNat < 256 ^ byteSize := by + rw [Rust.Bytes.radix_pow_eq_two_pow] + exact word.isLt + cases endian with + | little => + refine ⟨(Rust.Bytes.encodeLE byteSize word.toNat).map AMByte.init, ?_⟩ + rw [integerDecoder_run_map _ _ _ (Rust.Bytes.length_encodeLE _ _)] + simp only [Rust.Bytes.decode, Rust.Bytes.decodeLE_encodeLE_of_lt _ _ bound] + congr 1 + simp + | big => + refine ⟨(Rust.Bytes.encodeBE byteSize word.toNat).map AMByte.init, ?_⟩ + rw [integerDecoder_run_map _ _ _ (Rust.Bytes.length_encodeBE _ _)] + simp only [Rust.Bytes.decode, Rust.Bytes.decodeBE_encodeBE_of_lt _ _ bound] + congr 1 + simp + +namespace BitDecoder + +/-- A mapped decoder realizes an output whenever one realized input maps to it. -/ +theorem map_realizable (decoder : BitDecoder Raw) (f : Raw → Other) + (raw : Raw) (h : ∃ bytes, decoder.run bytes = some raw) : + ∃ bytes, (decoder.map f).run bytes = some (f raw) := by + obtain ⟨bytes, accepted⟩ := h + exact ⟨bytes, by rw [run_map, accepted]; rfl⟩ + +/-- Filtering preserves an existing representation when the value passes. -/ +theorem filterMap_realizable (decoder : BitDecoder Raw) (f : Raw → Option Other) + (raw : Raw) (other : Other) (h : ∃ bytes, decoder.run bytes = some raw) + (passes : f raw = some other) : + ∃ bytes, (decoder.filterMap f).run bytes = some other := by + obtain ⟨bytes, accepted⟩ := h + exact ⟨bytes, by rw [run_filterMap, accepted]; exact passes⟩ + +end BitDecoder + +/-- Concatenate one witness per admitted element. Recursion follows the value +list, so empty arrays and zero-sized elements require no inhabited carrier. -/ +theorem arrayDecode_realizable (element : BitDecoder Raw) (admitted : Raw → Prop) + (realizable : ∀ raw, admitted raw → ∃ bytes, element.run bytes = some raw) + (raws : List Raw) (valid : ∀ raw ∈ raws, admitted raw) : + ∃ bytes, bytes.length = raws.length * element.byteSize ∧ + arrayDecode element raws.length bytes = some ⟨raws, rfl⟩ := by + induction raws with + | nil => exact ⟨[], by simp, rfl⟩ + | cons raw raws ih => + obtain ⟨head, headAccepted⟩ := realizable raw (valid raw (by simp)) + have headWidth := BitDecoder.run_length element head raw headAccepted + obtain ⟨tail, tailWidth, tailAccepted⟩ := ih + (fun raw member => valid raw (by simp [member])) + refine ⟨head ++ tail, ?_, ?_⟩ + · simp only [List.length_append, List.length_cons, headWidth, tailWidth, Nat.succ_mul] + omega + · simp only [List.length_cons, arrayDecode, ← headWidth, List.take_left, List.drop_left, + headAccepted, tailAccepted] + rfl + +end Rust.Storage + +open Aeneas.Std Rust.Storage +namespace AeneasSpecs + +theorem RustModel.realizableRepresentation_exists {Raw : Type u} [m : RustModel Raw] + (realizable : RustModel.realizableRepresentation Raw) + (decoder : BitDecoder Raw) (available : m.representation = some decoder) + (raw : Raw) (valid : isValid raw) : ∃ bytes, decoder.run bytes = some raw := by + simp only [RustModel.realizableRepresentation, available] at realizable + exact realizable raw valid + +theorem realizableUScalar (ty : UScalarTy) : + RustModel.realizableRepresentation (UScalar ty) := by + intro raw _ + obtain ⟨bytes, accepted⟩ := integerDecoder_realizable (ty.numBits / 8) .little + (raw.bv.cast (AeneasAdapter.unsigned_byte_width ty).symm) + refine ⟨bytes, ?_⟩ + change ((integerDecoder _ _).map _).run bytes = _ + rw [BitDecoder.run_map, accepted] + simp + +theorem realizableIScalar (ty : IScalarTy) : + RustModel.realizableRepresentation (IScalar ty) := by + intro raw _ + obtain ⟨bytes, accepted⟩ := integerDecoder_realizable (ty.numBits / 8) .little + (raw.bv.cast (AeneasAdapter.signed_byte_width ty).symm) + refine ⟨bytes, ?_⟩ + change ((integerDecoder _ _).map _).run bytes = _ + rw [BitDecoder.run_map, accepted] + simp + +theorem realizableBool : RustModel.realizableRepresentation Bool := by + intro raw _ + cases raw + · exact ⟨[AMByte.init 0], boolDecoder_run_zero⟩ + · exact ⟨[AMByte.init 1], boolDecoder_run_one⟩ + +theorem realizableUnit : RustModel.realizableRepresentation Unit := by + intro raw _ + cases raw + exact ⟨[], unitDecoder_run_nil⟩ + +theorem realizablePhantomData (T : Type) : + RustModel.realizableRepresentation (Zerocopy.core.marker.PhantomData T) := by + intro raw _ + rw [phantomData_eq_mk T raw] + exact ⟨[], emptyDecoder_run_nil _⟩ + +theorem realizableChar : RustModel.realizableRepresentation Char := by + intro raw _ + obtain ⟨bytes, accepted⟩ := integerDecoder_realizable 4 .little + (BitVec.ofNat 32 raw.val.toNat) + refine ⟨bytes, ?_⟩ + change ((integerDecoder 4 .little).filterMap _).run bytes = _ + rw [BitDecoder.run_filterMap, accepted] + have word : UInt32.ofNat (BitVec.ofNat 32 raw.val.toNat).toNat = raw.val := by + rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (UInt32.toNat_lt raw.val)] + exact UInt32.ofNat_toNat + have valid : _root_.isValidChar raw.val := by + simpa only [_root_.isValidChar, UInt32.lt_iff_toNat_lt, UInt32.reduceToNat, + UInt32.isValidChar, Nat.isValidChar] using raw.valid + simp only [Option.bind_some, word, dif_pos valid] + +theorem realizableOptionNonZeroUScalar (ty : UScalarTy) (Inner : Type) : + RustModel.realizableRepresentation (Option (core.num.nonzero.NonZero (UScalar ty) Inner)) := by + intro raw valid + cases raw with + | none => + obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists + (realizableUScalar ty) (uScalarBitDecoder ty) rfl ⟨0⟩ ⟨_, rfl⟩ + exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; rfl⟩ + | some raw => + have nonzero : raw.val.val ≠ 0 := by + obtain ⟨value, accepted⟩ := valid + by_cases positive : 0 < raw.val.val + · omega + · simp [RustModel.decode, positive] at accepted + obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists + (realizableUScalar ty) (uScalarBitDecoder ty) rfl raw.val ⟨_, rfl⟩ + exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp [nonzero]⟩ + +theorem realizableOptionNonZeroIScalar (ty : IScalarTy) (Inner : Type) : + RustModel.realizableRepresentation (Option (core.num.nonzero.NonZero (IScalar ty) Inner)) := by + intro raw valid + cases raw with + | none => + obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists + (realizableIScalar ty) (iScalarBitDecoder ty) rfl ⟨0⟩ ⟨_, rfl⟩ + exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp only [Option.map_some, IScalar.val, BitVec.toInt_ofNat, Int.natCast_zero, Int.zero_bmod, ite_true]⟩ + | some raw => + have nonzero : raw.val.val ≠ 0 := by + obtain ⟨value, accepted⟩ := valid + by_contra zero + simp [RustModel.decode, zero] at accepted + obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists + (realizableIScalar ty) (iScalarBitDecoder ty) rfl raw.val ⟨_, rfl⟩ + exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp [nonzero]⟩ + +theorem realizableNonZeroUScalar (ty : UScalarTy) (Inner : Type) : + RustModel.realizableRepresentation (core.num.nonzero.NonZero (UScalar ty) Inner) := by + intro raw valid + have nonzero : raw.val.val ≠ 0 := by + obtain ⟨value, accepted⟩ := valid + by_cases positive : 0 < raw.val.val + · omega + · simp [RustModel.decode, positive] at accepted + obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists + (realizableUScalar ty) (uScalarBitDecoder ty) rfl raw.val ⟨_, rfl⟩ + refine ⟨bytes, ?_⟩ + change ((uScalarBitDecoder ty).filterMap _).run bytes = _ + rw [BitDecoder.run_filterMap, accepted] + simp only [Option.bind_some, nonzero, ↓reduceIte] + +theorem realizableNonZeroIScalar (ty : IScalarTy) (Inner : Type) : + RustModel.realizableRepresentation (core.num.nonzero.NonZero (IScalar ty) Inner) := by + intro raw valid + have nonzero : raw.val.val ≠ 0 := by + obtain ⟨value, accepted⟩ := valid + by_contra zero + simp [RustModel.decode, zero] at accepted + obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists + (realizableIScalar ty) (iScalarBitDecoder ty) rfl raw.val ⟨_, rfl⟩ + refine ⟨bytes, ?_⟩ + change ((iScalarBitDecoder ty).filterMap _).run bytes = _ + rw [BitDecoder.run_filterMap, accepted] + simp only [Option.bind_some, nonzero, ↓reduceIte] + +/-- A transparent wrapper reuses its payload's bytes. The inverse and validity +premises also cover generated wrapper providers with their retained decoder. -/ +theorem RustModel.realizable_of_wrapper {A B : Type} [ma : RustModel A] [mb : RustModel B] + (wrap : A → B) (unwrap : B → A) (inverse : ∀ raw, wrap (unwrap raw) = raw) + (representation : mb.representation = wrapperRepresentation wrap) + (validChild : ∀ raw, isValid raw → isValid (unwrap raw)) + (child : RustModel.realizableRepresentation A) : + RustModel.realizableRepresentation B := by + cases available : ma.representation with + | none => simp [RustModel.realizableRepresentation, available] at child + | some decoder => + simp only [RustModel.realizableRepresentation, available] at child + simp only [RustModel.realizableRepresentation, representation, + wrapperRepresentation, available, Option.map_some] + intro raw valid + obtain ⟨bytes, accepted⟩ := child (unwrap raw) (validChild raw valid) + exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp [inverse]⟩ + +theorem realizableManuallyDrop (T : Type) [ma : RustModel T] + (child : RustModel.realizableRepresentation T) : + RustModel.realizableRepresentation (core.mem.manually_drop.ManuallyDrop T) := + RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl + (fun _ valid => valid) child + +theorem realizableCell (T : Type) [ma : RustModel T] + (child : RustModel.realizableRepresentation T) : + RustModel.realizableRepresentation (core.cell.Cell T) := + RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl + (fun _ valid => valid) child + +theorem realizableUnsafeCell (T : Type) [ma : RustModel T] + (child : RustModel.realizableRepresentation T) : + RustModel.realizableRepresentation (core.cell.UnsafeCell T) := + RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl + (fun _ valid => valid) child + +theorem realizableWrapping (T : Type) [ma : RustModel T] + (child : RustModel.realizableRepresentation T) : + RustModel.realizableRepresentation (Zerocopy.core.num.wrapping.Wrapping T) := + RustModel.realizable_of_wrapper _ (·._0) (by rintro ⟨raw⟩; rfl) rfl + (fun _ valid => valid) child + +/-- Successful list decoding admits every stored element with the same provider. -/ +theorem decodeList_valid {α : Type u} [ma : RustModel α] + (raws : List α) (values : List ma.Model) (accepted : decodeList ma.decode raws = some values) : + ∀ raw ∈ raws, isValid raw := by + induction raws generalizing values with + | nil => simp + | cons head tail ih => + cases decodedHead : ma.decode head with + | none => simp [decodeList, decodedHead] at accepted + | some value => + cases decodedTail : decodeList ma.decode tail with + | none => simp [decodeList, decodedHead, decodedTail] at accepted + | some values => + intro raw member + rcases List.mem_cons.mp member with same | member + · subst raw; exact ⟨value, decodedHead⟩ + · exact ih _ decodedTail raw member + +/-- Element admission constructs list admission without choosing a default. -/ +theorem decodeList_exists {α : Type u} [ma : RustModel α] + (raws : List α) (valid : ∀ raw ∈ raws, isValid raw) : + ∃ values, decodeList ma.decode raws = some values := by + induction raws with + | nil => exact ⟨[], rfl⟩ + | cons raw raws ih => + obtain ⟨value, head⟩ := valid raw (by simp) + obtain ⟨values, tail⟩ := ih (fun raw member => valid raw (by simp [member])) + exact ⟨value :: values, by simp [decodeList, head, tail]⟩ + +theorem RustModel.valid_array {α : Type u} [ma : RustModel α] {n : Usize} + (raw : Aeneas.Std.Array α n) (valid : ∀ item ∈ raw.val, isValid item) : isValid raw := by + obtain ⟨values, decoded⟩ := decodeList_exists raw.val valid + unfold isValid + dsimp only [RustModel.decode] + split + · rename_i rejected + rw [decoded] at rejected + contradiction + · exact ⟨_, rfl⟩ + +theorem RustModel.realizable_array (α : Type u) [ma : RustModel α] (n : Usize) + (element : RustModel.realizableRepresentation α) : + @RustModel.realizableRepresentation (Aeneas.Std.Array α n) (@modelArray α n ma) := by + cases available : ma.representation with + | none => simp [RustModel.realizableRepresentation, available] at element + | some decoder => + simp only [RustModel.realizableRepresentation, available] at element + unfold RustModel.realizableRepresentation + rw [show (@modelArray α n ma).representation = ma.representation.map (fun element => + (arrayDecoder element n.val).map + (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl] + rw [available] + simp only [Option.map_some] + intro raw valid + obtain ⟨model, accepted⟩ := valid + have all : ∀ item ∈ raw.val, isValid item := by + dsimp only [RustModel.decode] at accepted + split at accepted + · contradiction + · rename_i values decoded + exact decodeList_valid raw.val values decoded + obtain ⟨bytes, width, physical⟩ := arrayDecode_realizable decoder isValid element raw.val all + refine ⟨bytes, ?_⟩ + rw [BitDecoder.run_map] + have rawLength : raw.val.length = n.val := raw.property + have decoded : arrayDecode decoder n.val bytes = some ⟨raw.val, rawLength⟩ := by + have transport (count : Nat) (h : raw.val.length = count) : + arrayDecode decoder count bytes = some ⟨raw.val, h⟩ := by + cases h + exact physical + exact transport n.val rawLength + have fromRaw : Aeneas.Std.Array.from raw.val rawLength = raw := + Aeneas.Std.Array.ext _ _ (Aeneas.Std.Array.from_val _ _) + simp only [rawLength] at width + simp [BitDecoder.run, arrayDecoder, width, decoded, fromRaw] + +end AeneasSpecs diff --git a/verification/aeneas/lean/RustRealizabilityModels.lean b/verification/aeneas/lean/RustRealizabilityModels.lean new file mode 100644 index 0000000000..7294a926ad --- /dev/null +++ b/verification/aeneas/lean/RustRealizabilityModels.lean @@ -0,0 +1,139 @@ +/- 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 RustRealizability +public import Models +import all RustModel +import all ModelPrelude +@[expose] public section + +open Aeneas.Std Rust.Storage +namespace AeneasSpecs + +/-- Generated providers retain their mathematical admission checks. A wrapper +may restrict admission further, but must still admit its stored child. -/ +theorem realizableUnalign (T : Type) [ma : RustModel T] + (child : RustModel.realizableRepresentation T) : + RustModel.realizableRepresentation (Zerocopy.wrappers.Unalign T) := by + apply RustModel.realizable_of_wrapper Zerocopy.wrappers.Unalign.mk (·._0) + (by rintro ⟨raw⟩; rfl) rfl ?_ child + intro raw valid + obtain ⟨value, accepted⟩ := valid + cases decoded : ma.decode raw._0 with + | none => simp [RustModel.decode, Zerocopy.wrappers.Unalign.decode, decoded] at accepted + | some value => exact ⟨value, decoded⟩ + +theorem realizableReadOnly (T : Type) [ma : RustModel T] + (child : RustModel.realizableRepresentation T) : + RustModel.realizableRepresentation (Zerocopy.wrappers.read_only_def.ReadOnly T) := by + apply RustModel.realizable_of_wrapper Zerocopy.wrappers.read_only_def.ReadOnly.mk (·.inner) + (by rintro ⟨raw⟩; rfl) rfl ?_ child + intro raw valid + obtain ⟨value, accepted⟩ := valid + cases decoded : ma.decode raw.inner with + | none => simp [RustModel.decode, Zerocopy.wrappers.read_only_def.ReadOnly.decode, decoded] at accepted + | some value => exact ⟨value, decoded⟩ + +theorem realizableByteorderU16 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.U16 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.U16.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (2#usize) (realizableUScalar .U8)) + +theorem realizableByteorderU32 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.U32 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.U32.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8)) + +theorem realizableByteorderU64 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.U64 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.U64.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8)) + +theorem realizableByteorderU128 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.U128 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.U128.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (16#usize) (realizableUScalar .U8)) + +theorem realizableByteorderUsize (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.Usize O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.Usize.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8)) + +theorem realizableByteorderI16 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.I16 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.I16.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (2#usize) (realizableUScalar .U8)) + +theorem realizableByteorderI32 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.I32 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.I32.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8)) + +theorem realizableByteorderI64 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.I64 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.I64.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8)) + +theorem realizableByteorderI128 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.I128 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.I128.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (16#usize) (realizableUScalar .U8)) + +theorem realizableByteorderIsize (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.Isize O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.Isize.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8)) + +theorem realizableByteorderF32 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.F32 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.F32.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8)) + +theorem realizableByteorderF64 (O : Type) [RustModel O] : + RustModel.realizableRepresentation (Zerocopy.byteorder.F64 O) := by + apply RustModel.realizable_of_wrapper + (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk) + (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl + (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩)) + (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8)) + +end AeneasSpecs diff --git a/verification/aeneas/lean/RustRealizabilityTests.lean b/verification/aeneas/lean/RustRealizabilityTests.lean new file mode 100644 index 0000000000..cf7028d4f6 --- /dev/null +++ b/verification/aeneas/lean/RustRealizabilityTests.lean @@ -0,0 +1,94 @@ +/- 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 RustRealizabilityModels +import all RustModel +import all ModelPrelude +import all Rust.Storage +@[expose] public section + +open Aeneas.Std AeneasSpecs Rust.Storage +namespace RustRealizabilityTests + +example (ty : UScalarTy) : RustModel.realizableRepresentation (UScalar ty) := realizableUScalar ty +example (ty : IScalarTy) : RustModel.realizableRepresentation (IScalar ty) := realizableIScalar ty +example : RustModel.realizableRepresentation Char := realizableChar +example : RustModel.realizableRepresentation Bool := realizableBool +example (ty : UScalarTy) (Inner : Type) : + RustModel.realizableRepresentation (core.num.nonzero.NonZero (UScalar ty) Inner) := + realizableNonZeroUScalar ty Inner +example (ty : IScalarTy) (Inner : Type) : + RustModel.realizableRepresentation (Option (core.num.nonzero.NonZero (IScalar ty) Inner)) := + realizableOptionNonZeroIScalar ty Inner +example : RustModel.realizableRepresentation + (Aeneas.Std.Array (Aeneas.Std.Array Bool (2#usize)) (3#usize)) := + RustModel.realizable_array _ _ (RustModel.realizable_array _ _ realizableBool) +example : RustModel.realizableRepresentation (Aeneas.Std.Array Unit (4#usize)) := + RustModel.realizable_array _ _ realizableUnit +example (T : Type) : RustModel.realizableRepresentation + (Aeneas.Std.Array (Zerocopy.core.marker.PhantomData T) (3#usize)) := + RustModel.realizable_array _ _ (realizablePhantomData T) + +-- Source existence cannot be inferred from initialization alone: this +-- initialized decoder realizes false, while the provider also admits true. +@[reducible] def missingTrue : RustModel Bool where + Model := Bool + «decode» := some + representation := some (emptyDecoder false) + +example : @RustModel.initializedRepresentation Bool missingTrue := emptyDecoder_initialized false +example : ¬ @RustModel.realizableRepresentation Bool missingTrue := by + intro realizable + obtain ⟨bytes, accepted⟩ := realizable true ⟨true, rfl⟩ + have empty : bytes = [] := List.length_eq_zero_iff.mp + (BitDecoder.run_length (emptyDecoder false) bytes true accepted) + subst bytes + contradiction + +-- Missing physical semantics remain unavailable even when no raw values exist. +@[reducible] def noPhysical : RustModel Empty where + Model := Empty + «decode» := some +example : ¬ @RustModel.realizableRepresentation Empty noPhysical := by + change ¬ False + exact not_false + +-- With an explicit decoder, an uninhabited raw carrier is vacuous and needs +-- no Inhabited instance. Empty arrays of this element carrier are realizable. +@[reducible] def emptyPhysical : RustModel Empty where + Model := Empty + «decode» := some + representation := some { byteSize := 0, «decode» := fun _ => none } + +theorem emptyRealizable : @RustModel.realizableRepresentation Empty emptyPhysical := by + intro raw + cases raw + +example : @RustModel.realizableRepresentation (Aeneas.Std.Array Empty (0#usize)) + (@modelArray Empty (0#usize) emptyPhysical) := + @RustModel.realizable_array Empty emptyPhysical (0#usize) emptyRealizable + +-- Distinct bytes may represent the same raw value; realizability supplies +-- existence and does not impose uniqueness or a canonical inverse. +@[reducible] def ambiguous : RustModel Bool where + Model := Unit + «decode» raw := if raw then none else some () + representation := some ((uScalarBitDecoder .U8).map fun _ => false) + +theorem ambiguousRealizable : @RustModel.realizableRepresentation Bool ambiguous := by + intro raw valid + cases raw with + | false => exact ⟨[AMByte.init 0], rfl⟩ + | true => obtain ⟨value, accepted⟩ := valid; contradiction + +example : ((uScalarBitDecoder .U8).map fun _ => false).run [AMByte.init 0] = some false := rfl +example : ((uScalarBitDecoder .U8).map fun _ => false).run [AMByte.init 1] = some false := rfl +example : [AMByte.init 0] ≠ [AMByte.init 1] := by decide + +end RustRealizabilityTests diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean index 152ded5181..4c7b510126 100644 --- a/verification/aeneas/projections/TraitLaws.lean +++ b/verification/aeneas/projections/TraitLaws.lean @@ -39,7 +39,8 @@ trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type ⦃ result => result = byte ⦄ trait_invariant into_bytes_initialized for @Zerocopy.IntoBytes with 1 type parameters where self => - AeneasSpecs.RustModel.initializedRepresentation Self + AeneasSpecs.RustModel.initializedRepresentation Self ∧ + AeneasSpecs.RustModel.realizableRepresentation Self trait_invariant from_bytes_valid for @Zerocopy.FromBytes with 1 type parameters where self => AeneasSpecs.RustModel.completeRepresentation Self diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index 147d350695..58adfe171c 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -6012,7 +6012,8 @@ pub use zerocopy_derive::IntoBytes; )] /// ```aeneas /// invariant into_bytes_initialized for self => -/// AeneasSpecs.RustModel.initializedRepresentation Self +/// AeneasSpecs.RustModel.initializedRepresentation Self ∧ +/// AeneasSpecs.RustModel.realizableRepresentation Self /// ``` pub unsafe trait IntoBytes { // The `Self: Sized` bound makes it so that this function doesn't prevent