From ef5452c56793d17f89b0db3794afadbf8203690f Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 14 Oct 2026 13:39:24 -0400 Subject: [PATCH] Prove array IntoBytes initialization from element laws The existing unsafe array impl relies on every element representation being initialized and Rust arrays adding no padding between complete elements. Give IntoBytes an inline initialization law over abstract bytes, then prove the actual extracted generic array dictionary from its element's law. Place invariant_proof on the existing unsafe_impl! invocation so the generic proof is required independently of concrete callers. Check primitive, empty, zero-sized, and nested array uses in Rust. Keep physical decoding independent of optional library admission. Missing byte semantics cannot establish the law. Provide explicit inhabited empty decoders and width-indexed integer, character and nonzero/niche decoders, with checked initialization laws and mathematical-admission bridges. Uninhabited and external-state token controls prevent zero-byte storage from fabricating construction permission. Invalid byte-to-value decoding produces the forbidden outcome rejected by total and partial contracts. The Rust Reference bridge remains an explicit premise; this does not prove the pointer implementation of as_bytes. Native const-identity mutations, independent required contracts, and proofs against both model builds check the generic implementation. Adapt metadata-indexed storage to the existing retained model providers. Compose language decoding with mathematical admission while preserving forbidden failure. Explicit Usize slice counts distinguish zero-sized representations; kernel counterexamples reject wrong metadata and invalid Boolean bytes even with a True postcondition. gherrit-pr-id: G4s3r4gpuxvvnoxoizjjgoy3b2rwmgi7g Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/LOWERING_AUDIT.md | 46 +++++- verification/aeneas/README.md | 44 +++++ verification/aeneas/golden/Funs.lean | 84 ++++++++++ verification/aeneas/golden/Types.lean | 6 + verification/aeneas/inline.py | 9 ++ verification/aeneas/lean/DeriveModels.lean | 71 ++++++++- .../aeneas/lean/EmptyConstructionTests.lean | 104 ++++++++++++ .../aeneas/lean/IndexedStorageTests.lean | 114 +++++++++++++ verification/aeneas/lean/ModelLemmas.lean | 22 +++ verification/aeneas/lean/ModelPrelude.lean | 147 ++++++++++++++++- .../aeneas/lean/Obligations/TraitChecks.lean | 22 +++ .../aeneas/lean/PhysicalModelTests.lean | 113 +++++++++++++ .../aeneas/lean/Proofs/TraitChecks.lean | 50 ++++++ .../RequiredModelContracts/TraitChecks.lean | 8 + verification/aeneas/lean/RustModel.lean | 150 +++++++++++++++++- .../aeneas/lean/Zerocopy/TypesExternal.lean | 30 +++- verification/aeneas/projections/Models.lean | 4 +- verification/aeneas/projections/Specs.lean | 13 ++ .../aeneas/projections/TraitLaws.lean | 4 + zerocopy/src/impls.rs | 12 +- zerocopy/src/lib.rs | 4 + zerocopy/src/trait_checks.rs | 24 +++ 22 files changed, 1065 insertions(+), 16 deletions(-) create mode 100644 verification/aeneas/lean/EmptyConstructionTests.lean create mode 100644 verification/aeneas/lean/IndexedStorageTests.lean create mode 100644 verification/aeneas/lean/PhysicalModelTests.lean diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md index 130b078e75..db9c129733 100644 --- a/verification/aeneas/LOWERING_AUDIT.md +++ b/verification/aeneas/LOWERING_AUDIT.md @@ -8,7 +8,9 @@ the translation preserves the observations needed by that claim. The current integration proves conditional functional contracts under the correspondence premises in [SEMANTICS.md](SEMANTICS.md). It does not yet implement -an abstract storage model or establish general Rust UB-freedom. +a runtime storage semantics or establish general Rust UB-freedom. +The pure byte representation model described below supplies initialization laws; +it does not add storage events to extracted executions. [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) describes the implemented admission checks on the preserved pre-transformation snapshot and final LLBC, as well as the additional requirements for future storage and handler models. Those checks @@ -117,6 +119,48 @@ numerical propositions are false. Conversely, they apply inside annotated functions too: finding every annotation does not establish that every relevant operation in its dependency closure was faithfully modeled. +## Pure byte representations and the array law + +[`Rust.Storage`](../../anneal/lean/Rust/Storage.lean) now represents initialized +and uninitialized bytes and fixed-width physical decoders as pure values. +`BitDecoder.Initialized` says that every byte list accepted by a decoder is +initialized. `RustModel.initializedRepresentation` requires this law when a +physical decoder is available and is `False` otherwise. It does not use the +library's mathematical decoder to restrict the byte lists under consideration. + +The array theorem partitions an accepted representation into contiguous element +chunks and proves initialization from the element law. Its proof consumes the +whole byte list, including an empty final remainder, for every count. Counting +elements rather than advancing by a positive byte width also covers empty +arrays and zero-sized elements. + +The Rust interpretation remains an explicit correspondence premise: each +physical decoder's width and admission domain must cover the language-valid +representations of its Rust type. `BitDecoder` does not encode or prove that +premise. A decoder which rejects everything satisfies the initialization law +vacuously, so that law alone cannot justify its use as a Rust representation +model. The current primitive decoders and their array composition must be +reviewed against the [Rust Reference layout](https://doc.rust-lang.org/reference/type-layout.html#array-layout) +and [validity rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#invalid-values), +as explained in [README.md](README.md#array-intobytes-initialization-law). +Array size and element offsets exclude padding outside complete element chunks; +padding inside a chunk is covered only by the element's law. + +A nameless `invariant_proof` fence on the ordinary array impl selects that +exact compiler owner, independently of any caller harness. Both AST stages must +retain its original type, usize length, and element dictionary parameters. +The checked ordinary Lean theorem covers that complete native dictionary +application under the element's law and model correspondence premises; the +kernel witness and independent telescope audit reject specialization or added +assumptions. This still relies on the reviewed correspondence from the Rust +impl header to its native dictionary, not merely on a proof name. + +These definitions do not make the existing lowering retain byte storage events, +initialization changes, or pointer provenance. They prove the modeled array +`IntoBytes` trait law under the representation premises, not the runtime +`as_bytes` implementation or general Rust UB-freedom. The typed-transfer and +value-production boundaries above still apply. + ## Complete LLBC operation inventory “Logical” below means the value-and-borrow interpretation. It does not mean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index a6901bc147..7974ad2e32 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -597,6 +597,50 @@ fence is the reserved CI-checked convention. Near-miss guard detection and the independent policy protect that convention without treating all mathematical prose as annotations. +## Array `IntoBytes` initialization law + +The `IntoBytes` fence in [`lib.rs`](../../zerocopy/src/lib.rs) requires every +accepted physical representation byte to be initialized. A byte in +[`Rust.Storage`](../../anneal/lean/Rust/Storage.lean) is either initialized with +an eight-bit value or uninitialized. Each physical decoder has a fixed width; +a successful run must consume exactly that width. The law covers the entire +accepted byte list, including any padding within an element representation. + +This physical decoder is separate from `RustModel.decode`, which interprets a +typed value for library contracts. `RustModel.initializedRepresentation` +quantifies over every successful physical decoding, even when the library +model rejects that value. A missing physical decoder makes the law `False`. +The current physical models cover `bool`, `u8`, `()`, and arrays recursively +built from them; other mathematical models do not acquire a byte law by default. + +`arrayDecoder_initialized` proves that arrays inherit this law from their +element decoder for every element count. The decoder splits the representation +into consecutive chunks of the element width and requires an empty final +remainder. An empty array accepts only an empty byte list. Zero-sized elements +use empty chunks, so positive counts of `()` also have no representation bytes. +The concrete checks in +[`trait_checks.rs`](../../zerocopy/src/trait_checks.rs) exercise primitive, +empty, zero-sized, and nested arrays; the extracted generic implementation law +supplies the result for arbitrary counts under the element's law. + +Applying the theorem to Rust requires a correspondence premise for the physical +decoder. Its width must equal Rust's size, and it must admit every language-valid +representation. The [Rust Reference array layout rules](https://doc.rust-lang.org/reference/type-layout.html#array-layout) +give size `N * size_of::()`, alignment equal to `T`'s alignment, and element +`k` at byte offset `k * size_of::()`. These rules leave no padding between +complete element representations; padding already included in `size_of::()` +still needs the element's initialization law. The [validity rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#invalid-values) +require valid array elements, restrict `bool` to zero and one, and require +initialized integers. The primitive layouts give `bool` and `u8` one byte and +`()` zero bytes. These language facts justify the current decoder choices; +Lean checks the initialization and array composition laws within that model. + +This proof establishes the array trait law under those correspondence premises. +The pure representation model does not track runtime storage, typed transfers, +or pointer provenance. `IntoBytes::as_bytes` retains its Rust safety argument; +its pointer implementation is not proved by this array law. See +[LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the remaining lowering boundaries. + ## Native Lean proofs and independent checks `Specs.lean` is generated from the Rust comments in a fixed context containing diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 7b5101b074..6b3f6d2cfc 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -707,6 +707,90 @@ def trait_checks.forwarded_byte_codec (byte : Std.U8) : Result Std.U8 := do (trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec) byte +/-- [zerocopy::trait_checks::require_into_bytes]: + Source: 'src/trait_checks.rs', lines 77:0-77:47 -/ +def trait_checks.require_into_bytes + {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do + ok () + +/-- [zerocopy::impls::_#23::{impl zerocopy::IntoBytes for [T; N]}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + Array.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (N : Std.Usize) (IntoBytesInst : IntoBytes T) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#23::{impl zerocopy::IntoBytes for [T; N]}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def Array.Insts.ZerocopyIntoBytes {T : Type} (N : Std.Usize) (IntoBytesInst : + IntoBytes T) : IntoBytes (Array T N) := { + only_derive_is_allowed_to_implement_this_trait := + Array.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + N IntoBytesInst +} + +/-- [zerocopy::impls::_::{impl zerocopy::IntoBytes for ()}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + Tuple.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_::{impl zerocopy::IntoBytes for ()}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Tuple.Insts.ZerocopyIntoBytes : IntoBytes Unit := { + only_derive_is_allowed_to_implement_this_trait := + Tuple.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 -/ +def U8.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u8}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U8.Insts.ZerocopyIntoBytes : IntoBytes Std.U8 := { + only_derive_is_allowed_to_implement_this_trait := + U8.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#2::{impl zerocopy::IntoBytes for bool}::only_derive_is_allowed_to_implement_this_trait]: + 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::trait_checks::check_array_into_bytes]: + Source: 'src/trait_checks.rs', lines 92:0-98:1 -/ +def trait_checks.check_array_into_bytes : Result Unit := do + trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize + Bool.Insts.ZerocopyIntoBytes) + trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize + U8.Insts.ZerocopyIntoBytes) + trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 4#usize + Tuple.Insts.ZerocopyIntoBytes) + trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 0#usize + Bool.Insts.ZerocopyIntoBytes) + trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize + (Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes)) + /-- [zerocopy::util::padding_needed_for]: Source: 'src/util/mod.rs', lines 163:0-223:1 -/ def util.padding_needed_for diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index ea487bd212..464a829fb8 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -99,6 +99,12 @@ structure byteorder.U32 (O : Type) where _0 : Array Std.U8 4#usize _1 : core.marker.PhantomData O +/-- Trait declaration: [zerocopy::IntoBytes] + Source: 'src/lib.rs', lines 5941:0-6446:1 + Visibility: public -/ +structure IntoBytes (Self : Type) where + only_derive_is_allowed_to_implement_this_trait : Result Unit + /-- Trait declaration: [zerocopy::trait_checks::ByteCodec] Source: 'src/trait_checks.rs', lines 26:0-29:1 -/ structure trait_checks.ByteCodec (Self : Type) where diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py index c335d9c140..06776f48bd 100644 --- a/verification/aeneas/inline.py +++ b/verification/aeneas/inline.py @@ -1025,6 +1025,15 @@ def save_bindings(root, annotations, work, development=False): 'file': source['file'], 'syntax': source['syntax'], 'open_line': source['open_line'], 'end_line': source['end_line'], 'end_col': source['end_col']} physical_plans = {} + if (not development and (work / 'zerocopy.llbc').is_file() + and (work / 'zerocopy.before.ullbc').is_file()): + import physical_models + final = json.loads((work / 'zerocopy.llbc').read_text())['translated'] + before = json.loads((work / 'zerocopy.before.ullbc').read_text())['translated'] + physical_plans = physical_models.validate_physical_wrapper_plans(final, before) + for rust, entry in bindings.items(): + if rust in physical_plans: + entry['physical_model'] = physical_plans[rust] type_image = list(native_omissions) classes = getattr(annotations, 'type_classes', None) if not development else None if not development and types.exists() and classes is None: diff --git a/verification/aeneas/lean/DeriveModels.lean b/verification/aeneas/lean/DeriveModels.lean index 1008dca069..d245ad4202 100644 --- a/verification/aeneas/lean/DeriveModels.lean +++ b/verification/aeneas/lean/DeriveModels.lean @@ -105,10 +105,17 @@ meta partial def boundModelProvider (raw : Expr) (params dicts : Array Expr) : M mkAppOptM n (xs.map some) if head.isConstOf ``UScalar then return ← app ``modelUScalar args if head.isConstOf ``IScalar then return ← app ``modelIScalar args + if head.isConstOf ``Char then return mkConst ``modelChar -- PhantomData has no stored child value: select its fixed empty provider -- without demanding a model for the type named by its phantom parameter. if head.isConstOf ``Zerocopy.core.marker.PhantomData then return ← app ``modelPhantomData args + for (carrier, provider) in #[ + (``core.mem.manually_drop.ManuallyDrop, ``modelManuallyDrop), + (``core.cell.Cell, ``modelCell), (``core.cell.UnsafeCell, ``modelUnsafeCell)] do + if head.isConstOf carrier then + let child ← boundModelProvider args[0]! params dicts + return ← app provider (args ++ #[child]) if head.isConstOf ``Bool then return mkConst ``modelBool if head.isConstOf ``Nat then return mkConst ``modelNat if head.isConstOf ``Int then return mkConst ``modelInt @@ -121,6 +128,15 @@ meta partial def boundModelProvider (raw : Expr) (params dicts : Array Expr) : M return ← app (if head.isConstOf ``Prod then ``modelProd else ``modelRustResult) (args ++ #[ma, mb]) if head.isConstOf ``Option || head.isConstOf ``List || head.isConstOf ``Slice then + if head.isConstOf ``Option then + let child ← whnf args[0]! + if child.getAppFn.isConstOf ``core.num.nonzero.NonZero then + let fields := child.getAppArgs + let word ← whnf fields[0]! + if word.getAppFn.isConstOf ``UScalar then + return ← app ``modelOptionNonZeroUScalar #[word.appArg!, fields[1]!] + if word.getAppFn.isConstOf ``IScalar then + return ← app ``modelOptionNonZeroIScalar #[word.appArg!, fields[1]!] let ma ← boundModelProvider args[0]! params dicts let provider := if head.isConstOf ``Option then ``modelOption else if head.isConstOf ``List then ``modelList else ``modelSlice @@ -361,7 +377,8 @@ that wrapper's decomposition, and finally register the complete RustModel. An absent local decoder is structural identity. An infallible authored decoder returns a model; a fallible one returns Option model and can restrict admission. -/ private meta def deriveProvider (raw : Name) (count : Nat) - (localDecoder : Option (Name × Syntax × Bool)) : TermElabM Unit := do + (localDecoder : Option (Name × Syntax × Bool)) + (physicalPayload : Option Nat := none) : TermElabM Unit := do let info ← nominal raw count let some b := (modelExtension.getState (← getEnv)).find? raw | throwError "Missing Fields/model shape for {raw}" @@ -448,8 +465,41 @@ private meta def deriveProvider (raw : Name) (count : Nat) addDecl (.thmDecl { «name» := raw ++ `decode_decompose, levelParams := info.levelParams, «type» := (← inferType decomposition), value := decomposition }) (forceExpose := true) + let bitDecoderTy ← mkAppM ``Rust.Storage.BitDecoder #[rawTy] + let representation ← match physicalPayload with + | none => mkAppOptM ``Option.none #[some bitDecoderTy] + | some payload => do + -- LLBC validation authorizes only named builtin storage wrappers. Lean + -- independently checks that reconstruction uses the actual raw fields. + let some structureInfo := getStructureInfo? (← getEnv) raw + | throwError "Physical wrappers must be structures: {raw}" + let supported := #[`Zerocopy.wrappers.Unalign, + `Zerocopy.wrappers.read_only_def.ReadOnly] + let byteorder := raw.getPrefix == `Zerocopy.byteorder && + #[`U16, `U32, `U64, `U128, `Usize, `I16, `I32, `I64, `I128, + `Isize, `F32, `F64].contains (Name.mkSimple raw.getString!) + unless supported.contains raw || byteorder do + throwError "Unsupported physical wrapper owner: {raw}" + unless payload == 0 && structureInfo.fieldNames.size == (if byteorder then 2 else 1) do + throwError "Physical wrapper field shape changed: {raw}" + let ctor := mkAppN (mkConst info.ctors.head! levels) params + forallTelescope (← inferType ctor) fun fields _ => do + let fieldTy ← inferType fields[payload]! + let child ← boundModelProvider fieldTy params dicts + let wrap ← withLocalDeclD `payload fieldTy fun value => do + let mut values := #[] + for i in [:fields.size] do + if i == payload then values := values.push value + else + let ty ← whnf (← inferType fields[i]!) + unless ty.getAppFn.isConstOf ``Zerocopy.core.marker.PhantomData do + throwError "Only PhantomData may accompany a physical payload: {raw}" + values := values.push (← mkAppOptM ``Zerocopy.core.marker.PhantomData.mk + (ty.getAppArgs.map some)) + mkLambdaFVars #[value] (mkAppN ctor values) + mkAppOptM ``wrapperRepresentation #[some fieldTy, some rawTy, some child, some wrap] let provider ← mkAppOptM ``RustModel.mk #[some rawTy, some modelTy, - some (mkAppN (mkConst b.decoder levels) all)] + some (mkAppN (mkConst b.decoder levels) all), some representation] addDefinition b.provider info.levelParams (← mkLambdaFVars all provider) setReducibilityStatus b.provider .reducible addInstance b.provider .global 1000 @@ -468,6 +518,23 @@ elab "derive_rust_model " rawId:ident " with " count:num " type " "parameters" deriveProvider (← realizeGlobalConstNoOverloadWithInfo rawId) count.getNat (some (self.getId, body, true)) +elab "derive_rust_model " rawId:ident " with " count:num " type " "parameters" + " with_physical " payloadIndex:num : command => Command.liftTermElabM do + deriveProvider (← realizeGlobalConstNoOverloadWithInfo rawId) count.getNat none + (some payloadIndex.getNat) + +elab "derive_rust_model " rawId:ident " with " count:num " type " "parameters" + " with_physical " payloadIndex:num " decode " self:ident " => " body:term : command => + Command.liftTermElabM do + deriveProvider (← realizeGlobalConstNoOverloadWithInfo rawId) count.getNat + (some (self.getId, body, false)) (some payloadIndex.getNat) + +elab "derive_rust_model " rawId:ident " with " count:num " type " "parameters" + " with_physical " payloadIndex:num " decode? " self:ident " => " body:term : command => + Command.liftTermElabM do + deriveProvider (← realizeGlobalConstNoOverloadWithInfo rawId) count.getNat + (some (self.getId, body, true)) (some payloadIndex.getNat) + /-- Audit the elaborated provider against its registered raw owner, mathematical type, full decoder, and generic count. Definitional equality unfolds actual expressions, so matching names alone cannot attach a provider to a wrong type. -/ diff --git a/verification/aeneas/lean/EmptyConstructionTests.lean b/verification/aeneas/lean/EmptyConstructionTests.lean new file mode 100644 index 0000000000..763c9fed3c --- /dev/null +++ b/verification/aeneas/lean/EmptyConstructionTests.lean @@ -0,0 +1,104 @@ +/- 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 ModelPrelude +import all RustModel +import all ModelPrelude +@[expose] public section + +/-! +Empty storage supplies no constructor permission or library invariant. These +model controls distinguish a supplied Lean inhabitant, an explicit physical +representation decoder, and admission by the retained mathematical provider. +They execute no invalid Rust construction. +-/ +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace EmptyConstructionTests + +-- An uninhabited raw carrier needs no fabricated inhabitant to fail closed. +@[reducible] def modelEmpty : RustModel Empty where + Model := Unit + decode raw := nomatch raw + +example : ¬ @RustModel.initializedRepresentation Empty modelEmpty := by + simp [RustModel.initializedRepresentation, RustModel.representation] + +example : modelEmpty.decodeBitsResult [] = .fail .undef := rfl +example : modelEmpty.decodeBytesResult [] = .fail .undef := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode] +example : ¬ WP.spec (modelEmpty.decodeBytesResult []) (fun _ => True) := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation] +example : ¬ WP.dspec (modelEmpty.decodeBytesResult []) (fun _ => True) := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation] + +inductive StateToken where + | mk + deriving Inhabited + +-- Lean's Inhabited instance alone does not install physical semantics. This +-- provider even accepts its raw value mathematically, but byte construction +-- still has no physical representation decoder. +@[reducible] def inhabitedOnly : RustModel StateToken where + Model := Unit + decode _ := some () + +example : ¬ @RustModel.initializedRepresentation StateToken inhabitedOnly := by + simp [RustModel.initializedRepresentation, RustModel.representation] + +example : (default : StateToken) = .mk := rfl +example : inhabitedOnly.decode .mk = some () := rfl +example : inhabitedOnly.decodeBytesResult [] = .fail .undef := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode] + +-- Model an external admission condition explicitly. The physical decoder may +-- supply the unit-like raw constructor while the full provider still rejects +-- that value when the required external state is absent. +@[reducible] def stateModel (masked : Bool) : RustModel StateToken where + Model := Unit + decode _ := if masked then some () else none + representation := some (emptyDecoder StateToken.mk) + +example : (stateModel false).decodeBitsResult [] = .ok StateToken.mk := rfl +example : (stateModel true).decodeBytesResult [] = .ok () := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, + emptyDecoder, BitDecoder.run] +example : (stateModel false).decodeBytesResult [] = .fail .undef := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, + emptyDecoder, BitDecoder.run] +example : ¬ WP.spec ((stateModel false).decodeBytesResult []) (fun _ => True) := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, + emptyDecoder, BitDecoder.run] +example : ¬ WP.dspec ((stateModel false).decodeBytesResult []) (fun _ => True) := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, + emptyDecoder, BitDecoder.run] + +-- Both states satisfy the physical initialization law. That law cannot prove +-- admission by the library provider, let alone a Rust constructor precondition. +example (masked : Bool) : + @RustModel.initializedRepresentation StateToken (stateModel masked) := + emptyDecoder_initialized StateToken.mk + +-- PhantomData stores no T. Its explicit raw constructor and empty decoder +-- therefore need neither a T value nor a RustModel T, even for uninhabited T. +example : (modelPhantomData Empty).decodeBitsResult [] = + .ok (Zerocopy.core.marker.PhantomData.mk : Zerocopy.core.marker.PhantomData Empty) := rfl +example : (modelPhantomData Empty).decodeBytesResult [] = .ok () := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, + emptyDecoder, BitDecoder.run] + +end EmptyConstructionTests diff --git a/verification/aeneas/lean/IndexedStorageTests.lean b/verification/aeneas/lean/IndexedStorageTests.lean new file mode 100644 index 0000000000..7f9009f723 --- /dev/null +++ b/verification/aeneas/lean/IndexedStorageTests.lean @@ -0,0 +1,114 @@ +/- 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 RustModel + +/-! +These model tests use explicit metadata and numeric byte representations. +They prove decoder behavior, not a Rust ABI identity, pointer reconstruction, +or the full contract of any unsafe trait or byte-cast implementation. +-/ +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace IndexedStorageTests + +example : (modelBool).decodeStorageResult boolDecoder.asStorageDecoder () [AMByte.init 1] = .ok true := by + rw [RustModel.decodeStorageResult_as_runWith] + rfl +example : (modelBool).decodeStorageResult boolDecoder.asStorageDecoder () [AMByte.init 2] = .fail .undef := by + rw [RustModel.decodeStorageResult_as_runWith] + rfl +example : (modelBool).decodeStorageResult boolDecoder.asStorageDecoder () [AMByte.uninit] = .fail .undef := by + rw [RustModel.decodeStorageResult_as_runWith] + rfl +example : (modelBool).decodeStorageResult boolDecoder.asStorageDecoder () [] = .fail .undef := by + rw [RustModel.decodeStorageResult_as_runWith] + rfl + +-- The native slice adapter preserves every explicit count and the array domain. +example (count : Usize) (bytes : List AMByte) + (values : { values : List Bool // values.length = count.val }) + (accepted : (arrayDecoder boolDecoder count.val).run bytes = some values) : + RustModel.decodeStorageBitsResult (RustModel.sliceStorageDecoder boolDecoder) count bytes = + .ok (Slice.from values.val (by rw [values.property]; scalar_tac)) := by + rw [RustModel.decodeStorageBitsResult, RustModel.sliceStorageDecoder_run, accepted] + rfl +example : (RustModel.sliceStorageDecoder boolDecoder).Initialized := + RustModel.sliceStorageDecoder_initialized _ boolDecoder_initialized + +-- Equal zero-byte widths support every usize count without guessing that count. +example (count : Usize) : ∃ raw, + RustModel.decodeStorageBitsResult (RustModel.sliceStorageDecoder unitDecoder) count [] = .ok raw := by + obtain ⟨values, accepted⟩ := arrayDecoder_complete unitDecoder + (fun bytes width _ => ⟨(), emptyDecoder_complete () bytes width⟩) count.val [] + (by simp [unitDecoder, emptyDecoder]) initialized_nil + rw [RustModel.decodeStorageBitsResult, RustModel.sliceStorageDecoder_run, accepted] + exact ⟨_, rfl⟩ +example (count : Usize) (bytes : List AMByte) (raw : Slice Unit) + (accepted : (RustModel.sliceStorageDecoder unitDecoder).run count bytes = some raw) : + raw.len = count := StorageDecoder.run_metadata _ _ _ _ accepted + +-- A mathematical decoder cannot conceal an invalid language representation. +@[reducible] def rejectsAll : RustModel Unit where + Model := Unit + decode _ := none + +example : rejectsAll.decodeStorageResult unitDecoder.asStorageDecoder () [] = .fail .undef := by + rw [RustModel.decodeStorageResult_as_runWith] + rfl +example : RustModel.decodeStorageBitsResult unitDecoder.asStorageDecoder () [] = .ok () := rfl +example : unitDecoder.asStorageDecoder.Initialized := + BitDecoder.asStorageDecoder_initialized _ unitDecoder_initialized +example : ¬ unitDecoder.asStorageDecoder.CompleteWith rejectsAll.decode := by + intro complete + obtain ⟨value, accepted⟩ := complete () [] rfl initialized_nil + simp [StorageDecoder.runWith] at accepted + +-- An uninitialized representation remains forbidden for the initialization law, +-- even if the mathematical decoder rejects every returned raw value. +def acceptsUninit : StorageDecoder Unit Unit where + byteSize _ := 1 + metadata _ := () + decode _ _ := some () + +example : rejectsAll.decodeStorageResult acceptsUninit () [AMByte.uninit] = .fail .undef := by + rw [RustModel.decodeStorageResult_as_runWith] + rfl +example : ¬ acceptsUninit.Initialized := by + intro initialized + have impossible := initialized () [AMByte.uninit] () rfl + simp [Initialized] at impossible + +-- The checked metadata observation applies even to zero-width representations. +def wrongCount : StorageDecoder Nat Nat where + byteSize _ := 0 + metadata := id + decode _ _ := some 0 + +example : RustModel.decodeStorageBitsResult wrongCount 3 [] = .fail .undef := rfl +example : modelNat.decodeStorageResult wrongCount 3 [] = .fail .undef := by + rw [RustModel.decodeStorageResult_as_runWith] + rfl + +-- A vacuous postcondition cannot admit language-invalid byte construction. +example : ¬ WP.spec + (modelBool.decodeStorageResult boolDecoder.asStorageDecoder () [AMByte.init 2]) + (fun _ => True) := by + rw [RustModel.decodeStorageResult_as_runWith] + change ¬ WP.spec (.fail .undef : Result Bool) (fun _ => True) + simp +example : ¬ WP.dspec (modelNat.decodeStorageResult wrongCount 3 []) (fun _ => True) := by + rw [RustModel.decodeStorageResult_as_runWith] + change ¬ WP.dspec (.fail .undef : Result Nat) (fun _ => True) + simp + +#print axioms RustModel.decodeStorageResult_as_runWith +#print axioms RustModel.decodeStorageResult_eq_ok_iff +#print axioms RustModel.sliceStorageDecoder_initialized + +end IndexedStorageTests diff --git a/verification/aeneas/lean/ModelLemmas.lean b/verification/aeneas/lean/ModelLemmas.lean index e65075c91b..4797183db4 100644 --- a/verification/aeneas/lean/ModelLemmas.lean +++ b/verification/aeneas/lean/ModelLemmas.lean @@ -8,6 +8,7 @@ those terms. -/ module public import ModelPrelude +public import ContractSimps @[expose] public section /-! @@ -48,6 +49,27 @@ theorem admitted_dite {α : Type} (P : Prop) [Decidable P] (value : P → α) : isValid raw ↔ ∀ x ∈ raw, isValid x := by cases raw <;> simp [isValid, RustModel.decode, modelOption, Option.map_eq_some_iff] +-- Niche-aware providers change physical storage, while retaining ordinary +-- Option admission. State that observation explicitly so proofs need not +-- unfold the physical decoder to recover their mathematical input domain. +@[simp, contract_simps] theorem option_nonzero_unsigned_decode_eq (ty : UScalarTy) (Inner : Type) + (raw : Option (core.num.nonzero.NonZero (UScalar ty) Inner)) : + RustModel.decode raw = (modelOption (ma := modelNonZeroUScalar ty Inner)).decode raw := rfl + +@[simp, contract_simps] theorem option_nonzero_signed_decode_eq (ty : IScalarTy) (Inner : Type) + (raw : Option (core.num.nonzero.NonZero (IScalar ty) Inner)) : + RustModel.decode raw = (modelOption (ma := modelNonZeroIScalar ty Inner)).decode raw := rfl + +@[simp, contract_simps] theorem option_nonzero_unsigned_valid_iff (ty : UScalarTy) (Inner : Type) + (raw : Option (core.num.nonzero.NonZero (UScalar ty) Inner)) : + isValid raw ↔ ∀ x ∈ raw, isValid x := by + exact @option_valid_iff _ (modelNonZeroUScalar ty Inner) raw + +@[simp, contract_simps] theorem option_nonzero_signed_valid_iff (ty : IScalarTy) (Inner : Type) + (raw : Option (core.num.nonzero.NonZero (IScalar ty) Inner)) : + isValid raw ↔ ∀ x ∈ raw, isValid x := by + exact @option_valid_iff _ (modelNonZeroIScalar ty Inner) raw + @[simp] theorem prod_valid_iff {α β : Type} [RustModel α] [RustModel β] (raw : α × β) : isValid raw ↔ isValid raw.1 ∧ isValid raw.2 := by rcases raw with ⟨a, b⟩ diff --git a/verification/aeneas/lean/ModelPrelude.lean b/verification/aeneas/lean/ModelPrelude.lean index 7d2f64655c..b8c02429de 100644 --- a/verification/aeneas/lean/ModelPrelude.lean +++ b/verification/aeneas/lean/ModelPrelude.lean @@ -8,6 +8,7 @@ those terms. -/ module public import RustModel +public import RustAeneas.Storage public import Zerocopy.Types @[expose] public section @@ -30,7 +31,8 @@ namespace AeneasSpecs -- variance, drop checking, or pointer provenance. @[reducible] instance modelPhantomData (T : Type) : RustModel (Zerocopy.core.marker.PhantomData T) := - { Model := Unit, «decode» := fun _ => some () } + { Model := Unit, «decode» := fun _ => some (), + representation := some (Rust.Storage.emptyDecoder Zerocopy.core.marker.PhantomData.mk) } /-- This check fails if the pinned extracted carrier gains runtime fields. -/ theorem phantomData_eq_mk (T : Type) (raw : Zerocopy.core.marker.PhantomData T) : @@ -39,6 +41,58 @@ theorem phantomData_eq_mk (T : Type) (raw : Zerocopy.core.marker.PhantomData T) rfl +-- A wrapper has exactly its payload's accepted bytes. Missing child storage +-- semantics stay missing; a mathematical decoder never supplies those bytes. +def wrapperRepresentation {A B : Type} [ma : RustModel A] (wrap : A → B) : + Option (Rust.Storage.BitDecoder B) := ma.representation.map (·.map wrap) + +theorem initializedWrapperRepresentation {A B : Type} [ma : RustModel A] + (wrap : A → B) (child : RustModel.initializedRepresentation A) : + match wrapperRepresentation wrap with + | none => False + | some decoder => decoder.Initialized := by + cases h : ma.representation with + | none => simp [RustModel.initializedRepresentation, h] at child + | some decoder => + simp only [RustModel.initializedRepresentation, h] at child + simp only [wrapperRepresentation, h, Option.map_some] + exact Rust.Storage.BitDecoder.map_initialized decoder wrap child + +-- These providers interpret stored values only. They do not model mutation, +-- aliasing, synchronization, or destruction of the standard-library wrappers. +@[reducible] instance modelManuallyDrop (T : Type) [ma : RustModel T] : + RustModel (core.mem.manually_drop.ManuallyDrop T) where + Model := ma.Model + decode raw := ma.decode raw.value + representation := wrapperRepresentation core.mem.manually_drop.ManuallyDrop.mk + +@[reducible] instance modelCell (T : Type) [ma : RustModel T] : + RustModel (core.cell.Cell T) where + Model := ma.Model + decode raw := ma.decode raw.value + representation := wrapperRepresentation core.cell.Cell.mk + +@[reducible] instance modelUnsafeCell (T : Type) [ma : RustModel T] : + RustModel (core.cell.UnsafeCell T) where + Model := ma.Model + decode raw := ma.decode raw.value + representation := wrapperRepresentation core.cell.UnsafeCell.mk + +theorem initializedManuallyDrop (T : Type) [ma : RustModel T] + (child : RustModel.initializedRepresentation T) : + RustModel.initializedRepresentation (core.mem.manually_drop.ManuallyDrop T) := + initializedWrapperRepresentation core.mem.manually_drop.ManuallyDrop.mk child + +theorem initializedCell (T : Type) [ma : RustModel T] + (child : RustModel.initializedRepresentation T) : + RustModel.initializedRepresentation (core.cell.Cell T) := + initializedWrapperRepresentation core.cell.Cell.mk child + +theorem initializedUnsafeCell (T : Type) [ma : RustModel T] + (child : RustModel.initializedRepresentation T) : + RustModel.initializedRepresentation (core.cell.UnsafeCell T) := + initializedWrapperRepresentation core.cell.UnsafeCell.mk child + -- The bounds are proofs stored beside the value. They contribute constraints -- to the mathematical type without another runtime field or admission test. structure UnsignedWord (ty : UScalarTy) where @@ -82,20 +136,103 @@ def signedWord (x : IScalar ty) : SignedWord ty := ⟨x.val, by simpa only [IScalar.min] using x.hmin, by have := x.hmax; simp only [IScalar.max]; omega⟩ -@[reducible] instance modelUScalar (ty : UScalarTy) : RustModel (UScalar ty) := - ⟨UnsignedWord ty, fun x => some (unsignedWord x)⟩ -@[reducible] instance modelIScalar (ty : IScalarTy) : RustModel (IScalar ty) := - { Model := SignedWord ty, «decode» := fun x => some (signedWord x) } +/-- Admission currently checks a little-endian 64-bit extraction target. +The shared initialization theorems are independent of this byte order. -/ +def uScalarBitDecoder (ty : UScalarTy) : Rust.Storage.BitDecoder (UScalar ty) := + Rust.Storage.AeneasAdapter.unsignedDecoder ty .little + +def iScalarBitDecoder (ty : IScalarTy) : Rust.Storage.BitDecoder (IScalar ty) := + Rust.Storage.AeneasAdapter.signedDecoder ty .little + +abbrev u8BitDecoder := uScalarBitDecoder .U8 + +@[reducible] instance modelUScalar (ty : UScalarTy) : RustModel (UScalar ty) where + Model := UnsignedWord ty + decode x := some (unsignedWord x) + representation := some (uScalarBitDecoder ty) +@[reducible] instance modelIScalar (ty : IScalarTy) : RustModel (IScalar ty) where + Model := SignedWord ty + decode x := some (signedWord x) + representation := some (iScalarBitDecoder ty) + +/-- Char stores a Unicode scalar value in four bytes. Filtering the complete +integer decoder rejects surrogates and out-of-range code points without ever +turning an uninitialized representation into a character. -/ +def charBitDecoder : Rust.Storage.BitDecoder Char := + (Rust.Storage.integerDecoder 4 .little).filterMap fun word => + let value := UInt32.ofNat word.toNat + if h : isValidChar value then some ⟨value, h⟩ else none + +@[reducible] instance modelChar : RustModel Char where + Model := Char + decode x := some x + representation := some charBitDecoder + +def nonzeroUScalarBitDecoder (ty : UScalarTy) (Inner : Type) : + Rust.Storage.BitDecoder (core.num.nonzero.NonZero (UScalar ty) Inner) := + (uScalarBitDecoder ty).filterMap fun word => + if word.val = 0 then none else some ⟨word⟩ + +def nonzeroIScalarBitDecoder (ty : IScalarTy) (Inner : Type) : + Rust.Storage.BitDecoder (core.num.nonzero.NonZero (IScalar ty) Inner) := + (iScalarBitDecoder ty).filterMap fun word => + if word.val = 0 then none else some ⟨word⟩ @[reducible] instance modelNonZeroUScalar (ty : UScalarTy) (Inner : Type) : RustModel (core.num.nonzero.NonZero (UScalar ty) Inner) where Model := NonZeroUnsignedWord ty decode raw := if h : 0 < raw.val.val then some ⟨unsignedWord raw.val, h⟩ else none + representation := some (nonzeroUScalarBitDecoder ty Inner) @[reducible] instance modelNonZeroIScalar (ty : IScalarTy) (Inner : Type) : RustModel (core.num.nonzero.NonZero (IScalar ty) Inner) where Model := NonZeroSignedWord ty decode raw := if h : raw.val.val ≠ 0 then some ⟨signedWord raw.val, h⟩ else none + representation := some (nonzeroIScalarBitDecoder ty Inner) + +-- Rust guarantees the zero niche for these particular standard-library +-- wrappers. Map the full integer decoder: a zero is a successfully decoded +-- Rust None, whereas an earlier byte failure remains a decoding failure. +-- A generic Option has no physical decoder inferred from its payload. +@[reducible] instance (priority := 1001) modelOptionNonZeroUScalar + (ty : UScalarTy) (Inner : Type) : + RustModel (Option (core.num.nonzero.NonZero (UScalar ty) Inner)) where + Model := Option (NonZeroUnsignedWord ty) + decode := (modelOption (ma := modelNonZeroUScalar ty Inner)).decode + representation := some ((uScalarBitDecoder ty).map fun word => + if word.val = 0 then none else some ⟨word⟩) + +@[reducible] instance (priority := 1001) modelOptionNonZeroIScalar + (ty : IScalarTy) (Inner : Type) : + RustModel (Option (core.num.nonzero.NonZero (IScalar ty) Inner)) where + Model := Option (NonZeroSignedWord ty) + decode := (modelOption (ma := modelNonZeroIScalar ty Inner)).decode + representation := some ((iScalarBitDecoder ty).map fun word => + if word.val = 0 then none else some ⟨word⟩) + +theorem initializedUScalar (ty : UScalarTy) : + RustModel.initializedRepresentation (UScalar ty) := + Rust.Storage.AeneasAdapter.unsignedDecoder_initialized ty .little + +theorem initializedIScalar (ty : IScalarTy) : + RustModel.initializedRepresentation (IScalar ty) := + Rust.Storage.AeneasAdapter.signedDecoder_initialized ty .little + +theorem initializedNonZeroUScalar (ty : UScalarTy) (Inner : Type) : + RustModel.initializedRepresentation (core.num.nonzero.NonZero (UScalar ty) Inner) := + Rust.Storage.BitDecoder.filterMap_initialized _ _ (initializedUScalar ty) + +theorem initializedNonZeroIScalar (ty : IScalarTy) (Inner : Type) : + RustModel.initializedRepresentation (core.num.nonzero.NonZero (IScalar ty) Inner) := + Rust.Storage.BitDecoder.filterMap_initialized _ _ (initializedIScalar ty) + +theorem initializedOptionNonZeroUScalar (ty : UScalarTy) (Inner : Type) : + RustModel.initializedRepresentation (Option (core.num.nonzero.NonZero (UScalar ty) Inner)) := + Rust.Storage.BitDecoder.map_initialized _ _ (initializedUScalar ty) + +theorem initializedOptionNonZeroIScalar (ty : IScalarTy) (Inner : Type) : + RustModel.initializedRepresentation (Option (core.num.nonzero.NonZero (IScalar ty) Inner)) := + Rust.Storage.BitDecoder.map_initialized _ _ (initializedIScalar ty) abbrev NonZeroUsizeValue := NonZeroUnsignedWord .Usize abbrev modelNonZeroUsize := modelNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner diff --git a/verification/aeneas/lean/Obligations/TraitChecks.lean b/verification/aeneas/lean/Obligations/TraitChecks.lean index 94deb09304..0261867c00 100644 --- a/verification/aeneas/lean/Obligations/TraitChecks.lean +++ b/verification/aeneas/lean/Obligations/TraitChecks.lean @@ -21,6 +21,28 @@ The contract families quantify an arbitrary outcome independently of any body. open Aeneas Aeneas.Std namespace Zerocopy.Obligations +-- State initialization directly on accepted byte lists. This expectation +-- independently fixes the physical decoder used by each concrete root case, +-- rather than referring to the generated RustModel representation selection. +def arrayBytesInitialized (element : Rust.Storage.BitDecoder Raw) (count : Usize) : Prop := + ∀ bytes values, + ((Rust.Storage.arrayDecoder element count.val).map + (fun values => Aeneas.Std.Array.from values.val values.property)).run bytes = some values → + Rust.Storage.Initialized bytes + +def array_into_bytes_spec_contract (run : Result Unit) : Prop := + run ⦃ _ => + arrayBytesInitialized Rust.Storage.boolDecoder (3#usize) ∧ + arrayBytesInitialized AeneasSpecs.u8BitDecoder (3#usize) ∧ + arrayBytesInitialized Rust.Storage.unitDecoder (4#usize) ∧ + arrayBytesInitialized Rust.Storage.boolDecoder (0#usize) ∧ + arrayBytesInitialized ((Rust.Storage.arrayDecoder Rust.Storage.boolDecoder 2).map + (fun values => Aeneas.Std.Array.from (n := 2#usize) values.val values.property)) (3#usize) ⦄ + +def array_into_bytes_spec : Prop := + array_into_bytes_spec_contract trait_checks.check_array_into_bytes + + def byte_codec_roundtrip_spec_contract (C : Type) (dictionary : trait_checks.ByteCodec C) (byte : U8) (run : Result U8) : Prop := TraitLaws.byte_roundtrip C dictionary → run ⦃ result => result = byte ⦄ diff --git a/verification/aeneas/lean/PhysicalModelTests.lean b/verification/aeneas/lean/PhysicalModelTests.lean new file mode 100644 index 0000000000..8eae1607d5 --- /dev/null +++ b/verification/aeneas/lean/PhysicalModelTests.lean @@ -0,0 +1,113 @@ +/- 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 ModelPrelude +import all RustModel +import all ModelPrelude +@[expose] public section + +/-! +A physical decoder describes which abstract bytes can produce a Rust value. +The library decoder may impose additional restrictions on that value, but those +restrictions must not weaken IntoBytes: every language-valid representation +must be initialized. These examples pin that separation and the forbidden +outcome of an invalid byte-to-value construction. + +These are model tests, not executions of invalid Rust. In particular, they do +not construct an invalid boolean or read uninitialized memory in Rust. +-/ +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace PhysicalModelTests + +example : RustModel.initializedRepresentation Bool := boolDecoder_initialized +example : RustModel.initializedRepresentation Unit := unitDecoder_initialized +example : RustModel.initializedRepresentation U8 := + initializedUScalar .U8 + +-- One proof covers every supported width and signedness. It does not assume +-- that an integer's alignment equals its byte size. +example (ty : UScalarTy) : RustModel.initializedRepresentation (UScalar ty) := + initializedUScalar ty +example (ty : IScalarTy) : RustModel.initializedRepresentation (IScalar ty) := + initializedIScalar ty + +example : (modelUScalar .U16).decodeBitsResult [AMByte.init 0x34, AMByte.init 0x12] = + .ok (0x1234#u16) := rfl +example : (modelIScalar .I16).decodeBitsResult [AMByte.init 255, AMByte.init 255] = + .ok ((-1)#i16) := rfl +example : (modelChar).decodeBitsResult [AMByte.init 65, AMByte.init 0, + AMByte.init 0, AMByte.init 0] = .ok 'A' := rfl +example : (modelChar).decodeBitsResult [AMByte.init 0, AMByte.init 0xd8, + AMByte.init 0, AMByte.init 0] = .fail .undef := rfl + +-- Zero is not a NonZero value, but it is the valid None representation of +-- Option. Failure to collect initialized bytes never becomes None. +example : (modelNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).decodeBitsResult + [AMByte.init 0] = .fail .undef := rfl +example : (modelOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).decodeBitsResult + [AMByte.init 0] = .ok none := rfl +example : (modelOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).decodeBitsResult + [AMByte.uninit] = .fail .undef := rfl +example : (modelOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner).decodeBitsResult + [AMByte.init 255] = .ok (some ⟨(-1)#i8⟩) := rfl + +-- Missing physical semantics cannot establish a trait law by vacuity. +example : ¬ RustModel.initializedRepresentation Nat := by + simp [RustModel.initializedRepresentation, RustModel.representation] + +-- This intentionally bad physical decoder accepts an uninitialized byte. +-- Rejecting all library values cannot turn it into an IntoBytes interpretation. +def acceptsUninit : BitDecoder Nat where + byteSize := 1 + decode _ := some 0 + +@[reducible] def rejectsEverything : RustModel Nat where + Model := Unit + decode _ := none + representation := some acceptsUninit + +example : ¬ @RustModel.initializedRepresentation Nat rejectsEverything := by + intro law + have forbidden := law [AMByte.uninit] 0 rfl + simp [Initialized] at forbidden + +example : (modelBool).decodeBitsResult [AMByte.uninit] = .fail .undef := rfl +example : (modelBool).decodeBitsResult [AMByte.init 2] = .fail .undef := rfl +example : (modelBool).decodeBitsResult [] = .fail .undef := rfl +example : (modelBool).decodeBytesResult [AMByte.init 1] = .ok true := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, BitDecoder.run, boolDecoder] +example : (modelUScalar .U8).decodeBytesResult [AMByte.init 255] = + .ok (unsignedWord (255#u8)) := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, + uScalarBitDecoder, Rust.Storage.AeneasAdapter.unsignedDecoder, + BitDecoder.map, BitDecoder.run, integerDecoder, collectInitialized, + Rust.Bytes.decode, Rust.Bytes.decodeLE, UScalar.ofNatCore] + +-- Both correctness judgments reject forbidden construction, even when the +-- written postcondition makes no promise about the returned value. +example : ¬ WP.spec (modelBool.decodeBytesResult [AMByte.init 2]) (fun _ => True) := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, BitDecoder.run, boolDecoder] +example : ¬ WP.dspec (modelBool.decodeBytesResult [AMByte.uninit]) (fun _ => True) := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, + RustModel.decodeResult, RustModel.representation, RustModel.decode, BitDecoder.run, boolDecoder] + +-- An element-count recursion, rather than division by byte width, handles +-- empty arrays, zero-sized elements, and nested arrays with the same rule. +example : RustModel.initializedRepresentation (Aeneas.Std.Array Bool (0#usize)) := + RustModel.initialized_array _ _ boolDecoder_initialized +example : RustModel.initializedRepresentation (Aeneas.Std.Array Unit (4#usize)) := + RustModel.initialized_array _ _ unitDecoder_initialized +example : RustModel.initializedRepresentation + (Aeneas.Std.Array (Aeneas.Std.Array Bool (2#usize)) (3#usize)) := + RustModel.initialized_array _ _ (RustModel.initialized_array _ _ boolDecoder_initialized) + +end PhysicalModelTests diff --git a/verification/aeneas/lean/Proofs/TraitChecks.lean b/verification/aeneas/lean/Proofs/TraitChecks.lean index 76439dafd3..f2f2bb9085 100644 --- a/verification/aeneas/lean/Proofs/TraitChecks.lean +++ b/verification/aeneas/lean/Proofs/TraitChecks.lean @@ -19,6 +19,56 @@ proves a total codec, and forwarding preserves only the supplied codec's law. open Aeneas Aeneas.Std AeneasSpecs namespace Zerocopy.Proofs +-- These primitive byte interpretations follow Rust's validity and layout +-- rules. The array law below uses those interpretations, not the optional +-- 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⟩ + +@[instance] theorem U8.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized U8 Zerocopy.U8.Insts.ZerocopyIntoBytes := + ⟨initializedUScalar .U8⟩ + +@[instance] theorem Tuple.Insts.ZerocopyIntoBytes_law : + TraitLaws.into_bytes_initialized Unit Zerocopy.Tuple.Insts.ZerocopyIntoBytes := + ⟨Rust.Storage.unitDecoder_initialized⟩ + +-- The original type, const length, and computational dictionary remain the +-- native implementation's prefix. Only the element's provider and law are +-- added. There is no assumption of the array's own law. +@[instance] theorem Array.Insts.ZerocopyIntoBytes_law + {T : Type} (N : Usize) (dictionary : IntoBytes T) + [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)⟩ + +-- Calling the real Rust helper selects the existing unsafe impls in Charon. +-- The generic impl law proves all lengths; these concrete cases additionally +-- check that the actual extraction and canonical model bindings compose. +theorem array_into_bytes_spec : Specs.array_into_bytes_spec := by + simp only [Specs.array_into_bytes_spec, Zerocopy.trait_checks.check_array_into_bytes, + Zerocopy.trait_checks.require_into_bytes, bind_ok, WP.spec_ok] + refine ⟨(), rfl, ?_, ?_, ?_, ?_, ?_⟩ + · exact (@TraitLaws.into_bytes_initialized.holds _ + (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes) + _ inferInstance) + · exact (@TraitLaws.into_bytes_initialized.holds _ + (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.U8.Insts.ZerocopyIntoBytes) + _ inferInstance) + · exact (@TraitLaws.into_bytes_initialized.holds _ + (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Tuple.Insts.ZerocopyIntoBytes) + _ inferInstance) + · exact (@TraitLaws.into_bytes_initialized.holds _ + (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes) + _ inferInstance) + · exact (@TraitLaws.into_bytes_initialized.holds _ + (Zerocopy.Array.Insts.ZerocopyIntoBytes _ + (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)) + _ inferInstance) + + @[instance] theorem trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec_law : TraitLaws.byte_roundtrip Zerocopy.trait_checks.XorCodec Zerocopy.trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec := by diff --git a/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean b/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean index 2c39ccd5c8..2bd4230751 100644 --- a/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean +++ b/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean @@ -22,6 +22,14 @@ substitute implementation. None of these adapters executes the function. open Aeneas Aeneas.Std AeneasSpecs namespace Zerocopy.Proofs +@[contract_simps] theorem required_array_into_bytes (run : Result Unit) + (provided : Specs.array_into_bytes_spec_contract run) : + Obligations.array_into_bytes_spec_contract run := by + apply WP.spec_mono provided + rintro _ ⟨_, _, boolean, byte, unit, empty, nested⟩ + exact ⟨boolean, byte, unit, empty, nested⟩ + + @[contract_simps] theorem required_byte_codec_roundtrip (C : Type) (dictionary : trait_checks.ByteCodec C) (byte : U8) (run : Result U8) (provided : Specs.byte_codec_roundtrip_spec_contract C dictionary byte run) : diff --git a/verification/aeneas/lean/RustModel.lean b/verification/aeneas/lean/RustModel.lean index 28d35e942c..1aed812ae2 100644 --- a/verification/aeneas/lean/RustModel.lean +++ b/verification/aeneas/lean/RustModel.lean @@ -8,6 +8,7 @@ those terms. -/ module public import Aeneas +public import Rust.Storage public meta import Lean @[expose] public section @@ -33,6 +34,10 @@ to the same raw value, so contracts retain the actual provider explicitly. -/ class RustModel (Raw : Type u) where Model : Type u decode : Raw → Option Model + /-- Optional language-level byte interpretation. Absence means that this + provider cannot establish byte-validity laws. + This decoder operates independently of the optional library invariant. -/ + representation : Option (Rust.Storage.BitDecoder Raw) := none -- The associated type is transparent so ordinary rewriting and coercions can -- identify a retained provider's Model with its named mathematical carrier. @@ -49,6 +54,23 @@ def isValid {Raw : Type u} [m : RustModel Raw] (raw : Raw) : Prop := def decoded {Raw : Type u} (m : RustModel Raw) (raw : Raw) (value : m.Model) : Prop := m.decode raw = some value +/-- IntoBytes needs an available physical decoder whose entire language-valid +representation domain is initialized. A library decoder cannot shrink this +quantification: even a provider which rejects every mathematical value must +establish initialization for all bytes accepted by its physical decoder. -/ +def RustModel.initializedRepresentation (Raw : Type u) [m : RustModel Raw] : Prop := + match m.representation with + | none => False + | some decoder => decoder.Initialized + +/-- Constructing a typed value from bytes requires language-level decoding. +The unsupported-model case also fails closed. No invalid Raw is produced. -/ +def RustModel.decodeBitsResult {Raw : Type u} (m : RustModel Raw) + (bytes : List Rust.Storage.AMByte) : Result Raw := + match m.representation with + | none => .fail .undef + | some decoder => Result.ofOption (decoder.asStorageDecoder.run () bytes) .undef + /-- Compose execution with the retained provider's mathematical decoder. An earlier execution failure or divergence is preserved. A rejected returned value becomes `undef`, marking an unadmitted value of this modeled computation; @@ -59,6 +81,49 @@ def RustModel.decodeResult {Raw : Type u} (m : RustModel Raw) let raw ← run Result.ofOption (m.decode raw) .undef +/-- Language-level decoding followed by the retained mathematical decoder. +Failure at either stage is preserved, rather than supplying a default value. -/ +def RustModel.decodeBytesResult {Raw : Type u} (m : RustModel Raw) + (bytes : List Rust.Storage.AMByte) : Result m.Model := + m.decodeResult (m.decodeBitsResult bytes) + +/-- Explicit metadata-indexed language decoding. No metadata is guessed from +byte length, and every rejected width, representation, or metadata returns undef. -/ +def RustModel.decodeStorageBitsResult {Raw : Type u} {Metadata : Type v} + [DecidableEq Metadata] (physical : Rust.Storage.StorageDecoder Metadata Raw) + (metadata : Metadata) (bytes : List Rust.Storage.AMByte) : Result Raw := + Result.ofOption (physical.run metadata bytes) .undef + +/-- Apply the retained mathematical provider after checked physical decoding. +An explicit decoder supplies the layout and language domain; it does not +supply a Rust ABI or provenance correspondence by virtue of its type. -/ +def RustModel.decodeStorageResult {Raw : Type u} {Metadata : Type v} + [DecidableEq Metadata] (m : RustModel Raw) + (physical : Rust.Storage.StorageDecoder Metadata Raw) + (metadata : Metadata) (bytes : List Rust.Storage.AMByte) : Result m.Model := + m.decodeResult (RustModel.decodeStorageBitsResult physical metadata bytes) + +/-- One guarded composition underlies both Option admission and Aeneas failure. -/ +theorem RustModel.decodeStorageResult_as_runWith {Raw : Type u} {Metadata : Type v} + [DecidableEq Metadata] (m : RustModel Raw) + (physical : Rust.Storage.StorageDecoder Metadata Raw) + (metadata : Metadata) (bytes : List Rust.Storage.AMByte) : + m.decodeStorageResult physical metadata bytes = + Result.ofOption (physical.runWith m.decode metadata bytes) .undef := by + cases language : physical.run metadata bytes with + | none => simp [RustModel.decodeStorageResult, RustModel.decodeStorageBitsResult, + RustModel.decodeResult, Rust.Storage.StorageDecoder.runWith, language] + | some raw => simp [RustModel.decodeStorageResult, RustModel.decodeStorageBitsResult, + RustModel.decodeResult, Rust.Storage.StorageDecoder.runWith, language] + +/-- The fixed representation API is the Unit-metadata specialization. -/ +theorem RustModel.decodeBytesResult_eq_decodeStorageResult {Raw : Type u} (m : RustModel Raw) + (physical : Rust.Storage.BitDecoder Raw) (available : m.representation = some physical) + (bytes : List Rust.Storage.AMByte) : + m.decodeBytesResult bytes = m.decodeStorageResult physical.asStorageDecoder () bytes := by + simp [RustModel.decodeBytesResult, RustModel.decodeBitsResult, available, + RustModel.decodeStorageResult, RustModel.decodeStorageBitsResult] + @[simp] theorem RustModel.decodeResult_ok {Raw : Type u} (m : RustModel Raw) (raw : Raw) : m.decodeResult (.ok raw) = Result.ofOption (m.decode raw) .undef := by simp [RustModel.decodeResult] @@ -82,6 +147,18 @@ theorem RustModel.decodeResult_eq_ok_iff {Raw : Type u} (m : RustModel Raw) | vis effect continuation => simp [RustModel.decodeResult] | div => simp +/-- A composed storage success retains the same physical and mathematical +providers, with neither admission stage hidden by the other. -/ +theorem RustModel.decodeStorageResult_eq_ok_iff {Raw : Type u} {Metadata : Type v} + [DecidableEq Metadata] (m : RustModel Raw) + (physical : Rust.Storage.StorageDecoder Metadata Raw) + (metadata : Metadata) (bytes : List Rust.Storage.AMByte) (value : m.Model) : + m.decodeStorageResult physical metadata bytes = .ok value ↔ + ∃ raw, physical.run metadata bytes = some raw ∧ m.decode raw = some value := by + rw [RustModel.decodeStorageResult_as_runWith, + ← Rust.Storage.StorageDecoder.runWith_eq_some_iff] + cases physical.runWith m.decode metadata bytes <;> simp + /-- Total correctness for the composition is the existing decoded-result post on the original execution, with the provider and postcondition unchanged. -/ theorem RustModel.spec_decodeResult_iff {Raw : Type u} (m : RustModel Raw) @@ -106,10 +183,16 @@ theorem RustModel.dspec_decodeResult_iff {Raw : Type u} (m : RustModel Raw) simp only [RustModel.decodeResult_div] constructor <;> intro _ <;> exact WP.dspec.div _ -@[reducible] instance modelBool : RustModel Bool := { Model := Bool, «decode» := some } +@[reducible] instance modelBool : RustModel Bool where + Model := Bool + decode := some + representation := some Rust.Storage.boolDecoder @[reducible] instance modelNat : RustModel Nat := { Model := Nat, «decode» := some } @[reducible] instance modelInt : RustModel Int := { Model := Int, «decode» := some } -@[reducible] instance modelUnit : RustModel Unit := { Model := Unit, «decode» := some } +@[reducible] instance modelUnit : RustModel Unit where + Model := Unit + decode := some + representation := some Rust.Storage.unitDecoder @[reducible] instance modelProd {α : Type u} {β : Type v} [ma : RustModel α] [mb : RustModel β] : RustModel (α × β) where @@ -161,12 +244,75 @@ abbrev ArrayValue (Element : Type u) (n : Usize) := | none => none | some values => some ⟨values, (decodeList_length ma.decode h) ▸ raw.property⟩ +/-- Explicit physical slice adapter. The caller supplies a usize element count, +including for zero-sized elements. Its value-level bound is carried by metadata, +so no count is inferred from byte length and no extra Nat admission guard is needed. -/ +def RustModel.sliceStorageDecoder {α : Type u} (element : Rust.Storage.BitDecoder α) : + Rust.Storage.StorageDecoder Usize (Slice α) where + byteSize count := count.val * element.byteSize + metadata := Slice.len + decode count bytes := (Rust.Storage.arrayDecode element count.val bytes).map (fun values => + Slice.from values.val (by rw [values.property]; scalar_tac)) + +/-- The native slice adapter has exactly the fixed-count array admission domain; +only its carrier and explicit usize metadata differ. -/ +theorem RustModel.sliceStorageDecoder_run {α : Type u} (element : Rust.Storage.BitDecoder α) + (count : Usize) (bytes : List Rust.Storage.AMByte) : + (RustModel.sliceStorageDecoder element).run count bytes = + ((Rust.Storage.arrayDecoder element count.val).run bytes).map + (fun values => Slice.from values.val (by rw [values.property]; scalar_tac)) := by + by_cases width : bytes.length = count.val * element.byteSize + · simp only [Rust.Storage.StorageDecoder.run, RustModel.sliceStorageDecoder, + Rust.Storage.BitDecoder.run, Rust.Storage.arrayDecoder, width, ↓reduceIte] + cases language : Rust.Storage.arrayDecode element count.val bytes with + | none => rfl + | some values => + have agrees : (Slice.from values.val (by rw [values.property]; scalar_tac)).len = count := by + apply UScalar.eq_of_val_eq + simp only [Slice.len_val, Slice.length, Slice.from_val, values.property] + simp [agrees] + · simp [Rust.Storage.StorageDecoder.run, RustModel.sliceStorageDecoder, + Rust.Storage.BitDecoder.run, Rust.Storage.arrayDecoder, width] + +/-- The slice adapter preserves the element initialization law. -/ +theorem RustModel.sliceStorageDecoder_initialized {α : Type u} + (element : Rust.Storage.BitDecoder α) (initialized : element.Initialized) : + (RustModel.sliceStorageDecoder element).Initialized := by + intro count bytes raw accepted + have language := ((Rust.Storage.StorageDecoder.run_eq_some_iff _ _ _ _).mp accepted).2.1 + simp only [RustModel.sliceStorageDecoder] at language + cases decoded : Rust.Storage.arrayDecode element count.val bytes with + | none => simp [decoded] at language + | some values => exact Rust.Storage.arrayDecode_initialized element initialized count.val bytes values decoded + @[reducible] instance modelArray {α : Type u} (n : Usize) [ma : RustModel α] : RustModel (Aeneas.Std.Array α n) where Model := ArrayValue ma.Model n decode raw := match h : decodeList ma.decode raw.val with | none => none | some values => some ⟨values, (decodeList_length ma.decode h) ▸ raw.property⟩ + representation := ma.representation.map (fun element => + (Rust.Storage.arrayDecoder element n.val).map + (fun values => Aeneas.Std.Array.from values.val values.property)) + +/-- The language-level array representation concatenates element storage. +This theorem concerns every accepted representation, including padding bytes; +it never asks whether the optional library decoder accepts the decoded value. -/ +theorem RustModel.initialized_array (α : Type u) [ma : RustModel α] (n : Usize) + (element : RustModel.initializedRepresentation α) : + @RustModel.initializedRepresentation (Aeneas.Std.Array α n) (@modelArray α n ma) := by + cases representation : ma.representation with + | none => simp [RustModel.initializedRepresentation, representation] at element + | some decoder => + simp only [RustModel.initializedRepresentation, representation] at element + unfold RustModel.initializedRepresentation + rw [show (@modelArray α n ma).representation = ma.representation.map (fun element => + (Rust.Storage.arrayDecoder element n.val).map + (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl] + rw [representation] + simp only [Option.map_some] + exact Rust.Storage.BitDecoder.map_initialized _ _ + (Rust.Storage.arrayDecoder_initialized decoder element n.val) -- This is Rust's Ok/Err payload type. Either constructor is admitted exactly -- when its selected child decodes, independently of Aeneas execution Result. diff --git a/verification/aeneas/lean/Zerocopy/TypesExternal.lean b/verification/aeneas/lean/Zerocopy/TypesExternal.lean index 10c6e45a5b..41ca7b502f 100644 --- a/verification/aeneas/lean/Zerocopy/TypesExternal.lean +++ b/verification/aeneas/lean/Zerocopy/TypesExternal.lean @@ -11,10 +11,34 @@ public import Aeneas @[expose] public section open Aeneas.Std --- These types model stored values, not Rust's niche encoding or memory layout. --- The generic wrapper admits zero; the alignment theorems explicitly require --- positivity. This over-approximation includes every valid NonZeroUsize. +-- The extracted NonZero carrier deliberately admits a zero field. The +-- physical and mathematical decoders in ModelPrelude perform the nonzero +-- check; merely building this Lean record grants no Rust construction rights. +abbrev core.num.niche_types.NonZeroU8Inner := U8 +abbrev core.num.niche_types.NonZeroI8Inner := I8 +abbrev core.num.niche_types.NonZeroU16Inner := U16 +abbrev core.num.niche_types.NonZeroI16Inner := I16 +abbrev core.num.niche_types.NonZeroU32Inner := U32 +abbrev core.num.niche_types.NonZeroI32Inner := I32 +abbrev core.num.niche_types.NonZeroU64Inner := U64 +abbrev core.num.niche_types.NonZeroI64Inner := I64 +abbrev core.num.niche_types.NonZeroU128Inner := U128 +abbrev core.num.niche_types.NonZeroI128Inner := I128 abbrev core.num.niche_types.NonZeroUsizeInner := Usize +abbrev core.num.niche_types.NonZeroIsizeInner := Isize structure core.num.nonzero.NonZero (T : Type) (_Inner : Type) where val : T + +-- These standard-library types are opaque at this extraction boundary. Their +-- documented byte representation is that of T. Retain nominal wrappers: +-- identical stored bytes do not make their APIs or invariants interchangeable. +-- This models only stored values, not Cell's access protocol or destruction. +structure core.mem.manually_drop.ManuallyDrop (T : Type) where + value : T + +structure core.cell.Cell (T : Type) where + value : T + +structure core.cell.UnsafeCell (T : Type) where + value : T diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean index a196c69439..67cf095612 100644 --- a/verification/aeneas/projections/Models.lean +++ b/verification/aeneas/projections/Models.lean @@ -22,10 +22,10 @@ check_model_binding Zerocopy.byteorder.BigEndian with 0 type parameters derive_rust_model Zerocopy.byteorder.LittleEndian with 0 type parameters check_model_binding Zerocopy.byteorder.LittleEndian with 0 type parameters -derive_rust_model Zerocopy.byteorder.U16 with 1 type parameters +derive_rust_model Zerocopy.byteorder.U16 with 1 type parameters with_physical 0 check_model_binding Zerocopy.byteorder.U16 with 1 type parameters -derive_rust_model Zerocopy.byteorder.U32 with 1 type parameters +derive_rust_model Zerocopy.byteorder.U32 with 1 type parameters with_physical 0 check_model_binding Zerocopy.byteorder.U32 with 1 type parameters derive_rust_model Zerocopy.trait_checks.XorCodec with 0 type parameters diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 9c2fb98603..5911ea7f12 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -138,6 +138,19 @@ spec forwarded_byte_codec_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.forwarded_byte_codec_spec for Zerocopy.trait_checks.forwarded_byte_codec with 1 +check_model_inputs Zerocopy.trait_checks.check_array_into_bytes with 0 type parameters +aeneas_spec_begin +spec array_into_bytes_spec + for @Zerocopy.trait_checks.check_array_into_bytes with 0 type parameters + ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Bool 3#usize) + ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array U8 3#usize) + ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Unit 4#usize) + ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Bool 0#usize) + ensures _ => AeneasSpecs.RustModel.initializedRepresentation + (Aeneas.Std.Array (Aeneas.Std.Array Bool 2#usize) 3#usize) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.array_into_bytes_spec for Zerocopy.trait_checks.check_array_into_bytes with 0 + check_model_inputs Zerocopy.util.padding_needed_for with 0 type parameters aeneas_spec_begin spec padding_lt_alignment diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean index 2d539fc6c2..166c642ed6 100644 --- a/verification/aeneas/projections/TraitLaws.lean +++ b/verification/aeneas/projections/TraitLaws.lean @@ -16,9 +16,13 @@ namespace Zerocopy.TraitLaws trait_dictionary @Zerocopy.core.num.nonzero.ZeroablePrimitive trait_dictionary @Zerocopy.byteorder.private.Sealed trait_dictionary @Zerocopy.byteorder.ByteOrder +trait_dictionary @Zerocopy.IntoBytes trait_dictionary @Zerocopy.trait_checks.ByteCodec 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 into_bytes_initialized for @Zerocopy.IntoBytes with 1 type parameters where self => + AeneasSpecs.RustModel.initializedRepresentation Self + end Zerocopy.TraitLaws diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index 4df786fd21..5912f1835f 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -904,7 +904,17 @@ const _: () = unsafe { }); unsafe_impl!(const N: usize, T: FromZeros => FromZeros for [T; N]); unsafe_impl!(const N: usize, T: FromBytes => FromBytes for [T; N]); - unsafe_impl!(const N: usize, T: IntoBytes => IntoBytes for [T; N]); + // SAFETY: As shown above, arrays concatenate their elements without extra + // padding. `T: IntoBytes` guarantees that each element's entire storage is + // initialized, so every byte of the array is initialized too, including for + // zero-length arrays and zero-sized elements. The invariant proof checks + // this implication for every `T` and `N`, under the Rust array-layout model. + unsafe_impl!( + /// ```aeneas + /// invariant_proof + /// ``` + const N: usize, T: IntoBytes => IntoBytes for [T; N] + ); unsafe_impl!(const N: usize, T: Unaligned => Unaligned for [T; N]); assert_unaligned!([(); 0], [(); 1], [u8; 0], [u8; 1]); unsafe_impl!(T: Immutable => Immutable for [T]); diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index 2f7d78f7cd..ea6b1cbb28 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -5934,6 +5934,10 @@ pub use zerocopy_derive::IntoBytes; not(no_zerocopy_diagnostic_on_unimplemented_1_78_0), diagnostic::on_unimplemented(note = "Consider adding `#[derive(IntoBytes)]` to `{Self}`") )] +/// ```aeneas +/// invariant into_bytes_initialized for self => +/// AeneasSpecs.RustModel.initializedRepresentation Self +/// ``` pub unsafe trait IntoBytes { // The `Self: Sized` bound makes it so that this function doesn't prevent // `IntoBytes` from being object safe. Note that other `IntoBytes` methods diff --git a/zerocopy/src/trait_checks.rs b/zerocopy/src/trait_checks.rs index 637a3f65d2..ed16535077 100644 --- a/zerocopy/src/trait_checks.rs +++ b/zerocopy/src/trait_checks.rs @@ -74,6 +74,29 @@ fn forwarded_byte_codec(byte: u8) -> u8 { byte_codec_roundtrip::>(byte) } +fn require_into_bytes() {} + +/// Forces extraction of the existing array IntoBytes implementation and its +/// primitive and nested dependencies. CI checks the generic implementation law +/// for every count; these concrete uses also exercise Rust's trait selection. +/// +/// ```aeneas +/// spec array_into_bytes_spec +/// ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Bool 3#usize) +/// ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array U8 3#usize) +/// ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Unit 4#usize) +/// ensures _ => AeneasSpecs.RustModel.initializedRepresentation (Aeneas.Std.Array Bool 0#usize) +/// ensures _ => AeneasSpecs.RustModel.initializedRepresentation +/// (Aeneas.Std.Array (Aeneas.Std.Array Bool 2#usize) 3#usize) +/// ``` +fn check_array_into_bytes() { + require_into_bytes::<[bool; 3]>(); + require_into_bytes::<[u8; 3]>(); + require_into_bytes::<[(); 4]>(); + require_into_bytes::<[bool; 0]>(); + require_into_bytes::<[[bool; 2]; 3]>(); +} + #[cfg(test)] mod tests { use super::*; @@ -83,5 +106,6 @@ mod tests { for byte in 0..=u8::MAX { assert_eq!(forwarded_byte_codec(byte), byte); } + check_array_into_bytes(); } }