From 171931818a24b7f97e76fb33d55ad4320e89bc16 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 14 Oct 2026 20:25:50 -0400 Subject: [PATCH] Prove concrete owned standard transmutation Verify the native standard transmute calls for u32 -> [u8; 4], [u8; 4] -> u32, and u8 -> bool. Retain the original ordered Rust endpoint types, require their canonical closed providers, and audit whole primitive and provider definitions plus every reached call, including calls inside unannotated helpers. Scope the numeric interpretation to the original little-endian 64-bit compiler target. The fixed unsigned scalars and initialized byte arrays have no padding or pointers. Boolean decoding accepts exactly zero and one and returns undef before constructing a Boolean for any invalid byte. Prove the Rust round-trip assertion root and independent arbitrary-outcome contracts for both integer conversions and the guarded Boolean conversion. The production transmute macro, pointer semantics, and generic FromBytes support remain deferred. gherrit-pr-id: Gwz22aqvb6z6qe2dmsgncsa6phc6jlxbf Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/admission.py | 42 ++++- verification/aeneas/control_runner.py | 4 +- verification/aeneas/external.json | 3 +- verification/aeneas/golden/Funs.lean | 43 ++++- .../aeneas/golden/FunsExternal_Template.lean | 11 +- verification/aeneas/lean/Check.lean | 127 +++++++++++++ .../lean/Obligations/OwnedTransmute.lean | 40 ++++ .../aeneas/lean/Proofs/OwnedTransmute.lean | 108 +++++++++++ .../OwnedTransmute.lean | 42 +++++ .../aeneas/lean/Zerocopy/FunsExternal.lean | 28 +++ .../aeneas/negative-control-family.sh | 20 +- verification/aeneas/projections/Specs.lean | 36 ++++ .../aeneas/tests/std_transmute_controls.py | 173 ++++++++++++++++++ verification/aeneas/tests/test_admission.py | 12 ++ zerocopy/src/util/mod.rs | 3 + zerocopy/src/util/owned_transmute.rs | 104 +++++++++++ 16 files changed, 778 insertions(+), 18 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/OwnedTransmute.lean create mode 100644 verification/aeneas/lean/Proofs/OwnedTransmute.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/OwnedTransmute.lean create mode 100644 verification/aeneas/tests/std_transmute_controls.py create mode 100644 zerocopy/src/util/owned_transmute.rs diff --git a/verification/aeneas/admission.py b/verification/aeneas/admission.py index d450560b26..8189e05d4a 100644 --- a/verification/aeneas/admission.py +++ b/verification/aeneas/admission.py @@ -117,7 +117,7 @@ def __init__(self, data, registry, law_traits=()): if options[key] != expected: raise ValueError(f'Unreviewed extraction option {key}: {options[key]!r}') stages = {variant(f['body'])[0] for f in self.functions.values() - if f['body'] != 'Opaque'} + if f['body'] != 'Opaque' and variant(f['body'])[0] != 'Intrinsic'} if len(stages) != 1 or not stages <= {'Unstructured', 'Structured'}: raise ValueError('Missing or mixed admission body stages') self.before = stages == {'Unstructured'} @@ -263,6 +263,10 @@ def visit(self, index): continue if kind == 'Builtin': tag, _ = variant(detail) + if tag == 'RustcIntrinsic' and name == 'core::intrinsics::transmute': + if function['body'] != {'Intrinsic': {'name': 'transmute', 'arg_names': ['src']}}: + raise ValueError('Standard transmute intrinsic body changed') + continue if tag in {'Inline', 'TrackCaller'}: continue elif kind == 'Unknown': @@ -279,6 +283,17 @@ def visit(self, index): if matches: if len(matches) != 1: raise ValueError(f'External interpretation signature changed: {name}') + if name == 'core::intrinsics::transmute': + expected_providers = { + 'u32->[u8;4]': 'Zerocopy.stdTransmuteU32ToBytes', + '[u8;4]->u32': 'Zerocopy.stdTransmuteBytesToU32', + 'u8->bool': 'Zerocopy.stdTransmuteU8ToBool', + } + if (matches[0].get('interpretation_extension') != 'closed-implicit-owned-provider-v1' + or matches[0].get('providers') != expected_providers + or meta['is_local'] or function['body'] != { + 'Intrinsic': {'name': 'transmute', 'arg_names': ['src']}}): + raise ValueError('Standard transmute reviewed boundary extension changed') # A builtin may replace a visible Rust body. Always select the # interpretation first, rather than approving the unused body. self.visited[index] = {'rust': name, 'origin': 'interpretation', @@ -721,7 +736,22 @@ def block(self, block, unwind=False): 'usize', 'core::num::niche_types::NonZeroUsizeInner'] if actual != expected: raise ValueError(f'Unsupported NonZero::new_unchecked instantiation {actual}') - self.calls.append({'caller': self.current, 'callee': name}) + call_evidence = {'caller': self.current, 'callee': name} + if name == 'core::intrinsics::transmute': + actual = [self.ty_name(ty) for ty in fn['generics']['types']] + providers = { + ('u32', '[u8;4]'): 'Zerocopy.stdTransmuteU32ToBytes', + ('[u8;4]', 'u32'): 'Zerocopy.stdTransmuteBytesToU32', + ('u8', 'bool'): 'Zerocopy.stdTransmuteU8ToBool', + } + if tuple(actual) not in providers: + raise ValueError(f'Unsupported standard transmute instantiation {actual}') + if fn['generics']['regions'] or fn['generics']['const_generics'] or fn['generics']['trait_refs']: + raise ValueError('Standard transmute acquired additional generic arguments') + call_evidence.update(type_arguments=actual, + provider=providers[tuple(actual)], + caller_def_id=self.current_function['def_id']) + self.calls.append(call_evidence) self.visit(callee) self.block(body['on_unwind'], True) elif tag == 'Assert': @@ -837,7 +867,7 @@ def input_identity(root): for name, value in os.environ.items(): if value and (name in {'RUSTFLAGS', 'CARGO_ENCODED_RUSTFLAGS', 'CARGO_BUILD_RUSTFLAGS', 'RUSTC', 'RUSTC_WRAPPER', - 'RUSTC_WORKSPACE_WRAPPER', 'CHARON_ARGS'} or + 'RUSTC_WORKSPACE_WRAPPER', 'CHARON_ARGS', 'CARGO_BUILD_TARGET'} or re.fullmatch(r'CARGO_TARGET_.*_RUSTFLAGS', name)): raise ValueError(f'Unreviewed compiler override {name}') configs = [] @@ -856,7 +886,7 @@ def input_identity(root): # Conservative lexical check avoids implementing Cargo's precedence # rules. Even a dormant override is rejected, rather than guessed safe. text = '\n'.join(line.split('#', 1)[0] for line in path.read_text().splitlines()) - if re.search(r'\b(rustflags|rustc|rustc-wrapper|rustc-workspace-wrapper)\b', text): + if re.search(r'\b(rustflags|rustc|rustc-wrapper|rustc-workspace-wrapper)\b|\b(?:build\.)?target\s*=', text): raise ValueError(f'Unreviewed Cargo compiler configuration: {path}') # Discovery and freshness use the same unconditional source inventory. # Cache-like names under src cannot hide newly added Rust specifications. @@ -909,7 +939,7 @@ def inspect(root, work, roots, sources, body_digests=None, law_traits=()): guarded = {row['rust'] for row in registry if row.get('opaque') or row['signature']['unsafe']} def guarded_calls(stage): - return Counter((call['caller'], call['callee']) for call in stage['calls'] + return Counter((call['caller'], call['callee'], tuple(call.get('type_arguments', []))) for call in stage['calls'] if call.get('callee') in guarded) missing = guarded_calls(reports['before']) - guarded_calls(reports['llbc']) if missing: @@ -932,6 +962,8 @@ def guarded_calls(stage): def check_translation(work, evidence): text = (work / 'Zerocopy/FunsExternal_Template.lean').read_text() signatures = { + 'core.intrinsics.transmute': + 'axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst', 'util.transmute_unchecked': 'axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst', 'util.copy_unchecked': diff --git a/verification/aeneas/control_runner.py b/verification/aeneas/control_runner.py index e5f67ee322..a4efbe3b3a 100644 --- a/verification/aeneas/control_runner.py +++ b/verification/aeneas/control_runner.py @@ -27,9 +27,9 @@ import time FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi', - 'contracts', 'dependencies', 'admission', 'semantics') + 'contracts', 'dependencies', 'admission', 'semantics', 'owned-std') MODELS = ('golden-verification', 'verification') -FIXTURES = ('NegativeControl.lean', 'WeakOutcome.lean', +FIXTURES = ('StdTransmuteAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean', 'RoundingConstructorControl.lean', 'RoundingDomainControl.lean', 'Zerocopy/ScopeControl.lean', 'Zerocopy/ShapeControl.lean', 'Zerocopy/ModelControl.lean', 'Proofs/WitnessOwnerControl.lean', diff --git a/verification/aeneas/external.json b/verification/aeneas/external.json index 2ce379ce23..d3c0e0f1ce 100644 --- a/verification/aeneas/external.json +++ b/verification/aeneas/external.json @@ -33,5 +33,6 @@ {"rust": "core::num::{u32}::to_le_bytes", "signature": {"unsafe": false, "inputs": ["u32"], "output": "[u8;4]", "types": 0, "consts": 0}, "lean": "core.num.U32.to_le_bytes"}, {"rust": "core::num::{usize}::MAX", "signature": {"unsafe": false, "inputs": [], "output": "usize", "types": 0, "consts": 0}, "lean": "Usize.MAX"}, {"rust": "core::clone::impls::{core::clone::Clone}::clone", "signature": {"unsafe": false, "inputs": ["&usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "core.clone.CloneUsize"}, - {"rust": "core::num::niche_types::{core::clone::Clone}::clone", "signature": {"unsafe": false, "inputs": ["&core::num::niche_types::NonZeroUsizeInner"], "output": "core::num::niche_types::NonZeroUsizeInner", "types": 0, "consts": 0}, "lean": "core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone"} + {"rust": "core::num::niche_types::{core::clone::Clone}::clone", "signature": {"unsafe": false, "inputs": ["&core::num::niche_types::NonZeroUsizeInner"], "output": "core::num::niche_types::NonZeroUsizeInner", "types": 0, "consts": 0}, "lean": "core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone"}, + {"rust": "core::intrinsics::transmute", "signature": {"unsafe": true, "inputs": ["T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "core.intrinsics.transmute", "interpretation_extension": "closed-implicit-owned-provider-v1", "providers": {"u32->[u8;4]": "Zerocopy.stdTransmuteU32ToBytes", "[u8;4]->u32": "Zerocopy.stdTransmuteBytesToU32", "u8->bool": "Zerocopy.stdTransmuteU8ToBool"}} ] diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 6b3f6d2cfc..e9976c0c69 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -792,7 +792,7 @@ def trait_checks.check_array_into_bytes : Result Unit := do (Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes)) /-- [zerocopy::util::padding_needed_for]: - Source: 'src/util/mod.rs', lines 163:0-223:1 -/ + Source: 'src/util/mod.rs', lines 166:0-226:1 -/ def util.padding_needed_for (len : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -808,7 +808,7 @@ def util.padding_needed_for ok (i2 &&& mask) /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: - Source: 'src/util/mod.rs', lines 250:0-268:1 -/ + Source: 'src/util/mod.rs', lines 253:0-271:1 -/ def util.round_down_to_next_multiple_of_alignment (n : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -825,7 +825,7 @@ def util.round_down_to_next_multiple_of_alignment ok (n &&& mask) /-- [zerocopy::util::max]: - Source: 'src/util/mod.rs', lines 277:0-283:1 -/ + Source: 'src/util/mod.rs', lines 280:0-286:1 -/ def util.max (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) @@ -845,7 +845,7 @@ def util.max else ok a /-- [zerocopy::util::min]: - Source: 'src/util/mod.rs', lines 292:0-298:1 -/ + Source: 'src/util/mod.rs', lines 295:0-301:1 -/ def util.min (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) @@ -864,6 +864,41 @@ def util.min then ok b else ok a +/-- [zerocopy::util::owned_transmute::to_bytes_native]: + Source: 'src/util/owned_transmute.rs', lines 29:0-33:1 -/ +def util.owned_transmute.to_bytes_native + (value : Std.U32) : Result (Array Std.U8 4#usize) := do + core.intrinsics.transmute (Array Std.U8 4#usize) value + +/-- [zerocopy::util::owned_transmute::to_bytes]: + Source: 'src/util/owned_transmute.rs', lines 22:0-24:1 -/ +def util.owned_transmute.to_bytes + (value : Std.U32) : Result (Array Std.U8 4#usize) := do + util.owned_transmute.to_bytes_native value + +/-- [zerocopy::util::owned_transmute::from_bytes]: + Source: 'src/util/owned_transmute.rs', lines 44:0-48:1 -/ +def util.owned_transmute.from_bytes + (bytes : Array Std.U8 4#usize) : Result Std.U32 := do + core.intrinsics.transmute Std.U32 bytes + +/-- [zerocopy::util::owned_transmute::checked_bool]: + Source: 'src/util/owned_transmute.rs', lines 59:0-67:1 -/ +def util.owned_transmute.checked_bool + (byte : Std.U8) : Result (Option Bool) := do + if byte < 2#u8 + then let b ← core.intrinsics.transmute Bool byte + ok (some b) + else ok none + +/-- [zerocopy::util::owned_transmute::round_trip_checks]: + Source: 'src/util/owned_transmute.rs', lines 75:0-79:1 -/ +def util.owned_transmute.round_trip_checks + (value : Std.U32) : Result Unit := do + let bytes ← util.owned_transmute.to_bytes value + let restored ← util.owned_transmute.from_bytes bytes + massert (restored = value) + /-- [zerocopy::util::safety_checks::checked_bool]: Source: 'src/util/safety_checks/mod.rs', lines 28:0-38:1 -/ def util.safety_checks.checked_bool diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index fd2ceb84e7..2a05df9bda 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -28,6 +28,13 @@ set_option maxHeartbeats 1000000 set_option maxRecDepth 2048 open Zerocopy +/-- [core::intrinsics::transmute]: + Source: '/rustc/library/core/src/intrinsics/mod.rs', lines 898:0-898:57 + Name pattern: [core::intrinsics::transmute] + Visibility: public -/ +@[rust_fun "core::intrinsics::transmute"] +axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst + /-- [core::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}::clone]: Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22 Name pattern: [core::num::niche_types::{core::clone::Clone}::clone] @@ -51,11 +58,11 @@ axiom core.num.nonzero.NonZero.get core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T /-- [zerocopy::util::copy_unchecked]: - Source: 'src/util/mod.rs', lines 310:0-325:1 -/ + Source: 'src/util/mod.rs', lines 313:0-328:1 -/ axiom util.copy_unchecked : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8) /-- [zerocopy::util::transmute_unchecked]: - Source: 'src/util/mod.rs', lines 337:0-366:1 -/ + Source: 'src/util/mod.rs', lines 340:0-369:1 -/ axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean index d40e9c042a..29ef24344a 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -72,6 +72,132 @@ private def checkUnemittedNativeType (env : Environment) (row : Json) : TermElab unless (generics.getObjValAs? (Array Json) field).toOption == some #[] do throwError "Unemitted native type has unsupported generic obligations: {rust}" +-- This closed boundary adds an interpretation-only provider to the std +-- primitive. Compare whole definitions independently of the functional proofs, +-- then bind each reached native call (including unannotated helpers) to its +-- original Rust endpoints and exact canonical provider. +private partial def stdTransmuteCalls (expression : Expr) : Array Expr := + if expression.getAppFn.isConstOf `core.intrinsics.transmute then + #[expression] ++ expression.getAppArgs.foldl + (fun found arg => found ++ stdTransmuteCalls arg) #[] + else + match expression with + | .app fn arg => stdTransmuteCalls fn ++ stdTransmuteCalls arg + | .lam _ ty body _ | .forallE _ ty body _ => stdTransmuteCalls ty ++ stdTransmuteCalls body + | .letE _ ty value body _ => stdTransmuteCalls ty ++ stdTransmuteCalls value ++ stdTransmuteCalls body + | .mdata _ body | .proj _ _ body => stdTransmuteCalls body + | _ => #[] + +private def auditStdTransmute (bindings : Json) : TermElabM Unit := do + let env ← getEnv + unless env.contains `core.intrinsics.transmute do return + let ctor ← Term.elabType (← `(∀ (Src Dst : Type), + (Src → Aeneas.Std.Result Dst) → Zerocopy.StdOwnedTransmute Src Dst)) + let some (.ctorInfo classCtor) := env.find? `Zerocopy.StdOwnedTransmute.mk + | throwError "Standard transmute provider must retain its reviewed one-field carrier" + unless ← Meta.isDefEq classCtor.type ctor do + throwError "Standard transmute provider carrier changed" + let expectedType ← Term.elabType (← `(∀ {Src : Type} (Dst : Type) + [Zerocopy.StdOwnedTransmute Src Dst], Src → Aeneas.Std.Result Dst)) + let expectedBody ← Term.elabTerm (← `(fun {Src : Type} (Dst : Type) + [provider : Zerocopy.StdOwnedTransmute Src Dst] (src : Src) => provider.run src)) none + Term.synthesizeSyntheticMVarsNoPostponing + let some (.defnInfo primitive) := env.find? `core.intrinsics.transmute + | throwError "Standard transmute interpretation must be a definition" + unless (← Meta.isDefEq primitive.type expectedType) && + (← Meta.isDefEq primitive.value (← instantiateMVars expectedBody)) do + throwError "Standard transmute extended signature or whole interpretation changed" + let forward ← Term.elabTerm (← `( + ({ run := fun value => Aeneas.Std.Result.ok (Aeneas.Std.core.num.U32.to_le_bytes value) } : + Zerocopy.StdOwnedTransmute Aeneas.Std.U32 (Aeneas.Std.Array Aeneas.Std.U8 4#usize)))) none + let backward ← Term.elabTerm (← `( + ({ run := fun bytes => Aeneas.Std.Result.ok (Aeneas.Std.core.num.U32.from_le_bytes bytes) } : + Zerocopy.StdOwnedTransmute (Aeneas.Std.Array Aeneas.Std.U8 4#usize) Aeneas.Std.U32))) none + let boolean ← Term.elabTerm (← `( + ({ run := fun byte => if byte.val < 2 then Aeneas.Std.Result.ok (decide (byte.val = 1)) + else Aeneas.Std.Result.fail Aeneas.Std.Error.undef } : + Zerocopy.StdOwnedTransmute Aeneas.Std.U8 Bool))) none + Term.synthesizeSyntheticMVarsNoPostponing + for (providerName, providerValue) in #[(`Zerocopy.stdTransmuteU32ToBytes, forward), + (`Zerocopy.stdTransmuteBytesToU32, backward), (`Zerocopy.stdTransmuteU8ToBool, boolean)] do + let some (.defnInfo provider) := env.find? providerName + | throwError "Standard transmute provider {providerName} must be a definition" + unless ← Meta.isDefEq provider.value (← instantiateMVars providerValue) do + throwError "Standard transmute provider {providerName} changed its whole interpretation" + let .ok admission := bindings.getObjVal? "admission" + | throwError "Standard transmute requires original compiler admission" + let .ok stages := admission.getObjVal? "stages" + | throwError "Standard transmute requires both compiler admission stages" + let .ok original := stages.getObjVal? "before" + | throwError "Standard transmute lacks original admission" + let .ok lowered := stages.getObjVal? "llbc" + | throwError "Standard transmute lacks lowered admission" + let .ok originalCalls := original.getObjValAs? (Array Json) "calls" + | throwError "Standard transmute lacks original call evidence" + let .ok loweredCalls := lowered.getObjValAs? (Array Json) "calls" + | throwError "Standard transmute lacks lowered call evidence" + let originalStd := originalCalls.filter fun row => row.getObjValAs? String "callee" == .ok "core::intrinsics::transmute" + let loweredStd := loweredCalls.filter fun row => row.getObjValAs? String "callee" == .ok "core::intrinsics::transmute" + -- Ordered type arguments identify source and destination independently; + -- preserve each call, its owner, and its multiplicity through lowering. + unless originalStd == loweredStd do + throwError "Standard transmute changed original ordered Rust endpoints or call ownership" + let .ok executions := lowered.getObjValAs? (Array Json) "executions" + | throwError "Standard transmute lacks the complete execution closure" + let nativeText ← IO.FS.readFile "Zerocopy/translation.json" + let .ok native := Json.parse nativeText | throwError "Invalid native primitive call map" + let .ok functions := native.getObjValAs? (Array Json) "functions" + | throwError "Missing native primitive function map" + for execution in executions do + if execution.getObjValAs? String "origin" != .ok "body" then continue + let .ok rust := execution.getObjValAs? String "rust" | throwError "Missing primitive call owner" + let expected := loweredStd.filter fun row => row.getObjValAs? String "caller" == .ok rust + let selected := functions.filter fun row => row.getObjValAs? String "rust_name" == .ok rust + -- General dictionary owners can have a different native spelling. Owners + -- with this boundary must have an exact producer identity from their call. + if expected.isEmpty && selected.isEmpty then continue + let candidates := if expected.isEmpty then selected else functions.filter fun row => + expected.any (fun call => call.getObjValAs? Nat "caller_def_id" == row.getObjValAs? Nat "def_id") + unless !candidates.isEmpty do throwError "Missing compiled standard transmute owner {rust}" + -- Native loop splitting can emit several bodies for one Rust owner. Audit + -- their aggregate inventory rather than silently omitting the loop helper. + let mut actual : Array Expr := #[] + let mut names : Array Name := #[] + for candidate in candidates do + let .ok raw := candidate.getObjValAs? String "lean_name" | throwError "Missing native owner name" + unless !names.contains raw.toName do throwError "Repeated native primitive owner {raw}" + names := names.push raw.toName + let some (.defnInfo owner) := env.find? raw.toName + | throwError "Reached primitive owner {rust} must retain its compiled body" + actual := actual ++ stdTransmuteCalls owner.value + unless actual.size == expected.size do + throwError "Compiled standard transmute call inventory differs for {rust}" + -- Consume one original witness per compiled call. Repeated calls with the + -- same endpoints are legal, but neither omission nor duplication is legal. + let mut remaining := expected + for call in actual do + let args := call.getAppArgs + unless args.size == 4 do throwError "Standard transmute acquired unsupported compiled arguments" + let matching ← remaining.filterM fun row => do + let .ok types := row.getObjValAs? (Array String) "type_arguments" | throwError "Missing Rust endpoints" + let (source, target, canonical) ← match types.toList with + | ["u32", "[u8;4]"] => pure ((← Term.elabType (← `(Aeneas.Std.U32))), + (← Term.elabType (← `(Aeneas.Std.Array Aeneas.Std.U8 4#usize))), `Zerocopy.stdTransmuteU32ToBytes) + | ["[u8;4]", "u32"] => pure ((← Term.elabType (← `(Aeneas.Std.Array Aeneas.Std.U8 4#usize))), + (← Term.elabType (← `(Aeneas.Std.U32))), `Zerocopy.stdTransmuteBytesToU32) + | ["u8", "bool"] => pure ((← Term.elabType (← `(Aeneas.Std.U8))), + (← Term.elabType (← `(Bool))), `Zerocopy.stdTransmuteU8ToBool) + | _ => throwError "Unsupported original Rust standard transmute endpoints" + unless row.getObjValAs? String "provider" == .ok canonical.toString do + throwError "Original Rust endpoint provider binding changed" + return (← Meta.isDefEq args[0]! source) && (← Meta.isDefEq args[1]! target) && + args[2]! == mkConst canonical + unless !matching.isEmpty do + throwError "Compiled standard transmute did not retain its canonical endpoint provider in {rust}" + let some selectedIndex := remaining.findIdx? (· == matching[0]!) + | throwError "Missing matched standard transmute call" + remaining := remaining.extract 0 selectedIndex ++ remaining.extract (selectedIndex + 1) remaining.size + run_elab do let env ← getEnv let layoutInputs := #[`Zerocopy.RustLayout.size, `Zerocopy.RustLayout.alignInput] @@ -301,6 +427,7 @@ run_elab do | throwError "Invalid {stage} execution admission roots" unless roots.size == rootNames.size && rootNames.all roots.contains do throwError "Execution admission roots disagree with the function binding table" + auditStdTransmute bindings let some typesModule := env.getModuleIdx? `Zerocopy.Types | throwError "Raw extracted types must be imported" let some shapesModule := env.getModuleIdx? `ModelShapes diff --git a/verification/aeneas/lean/Obligations/OwnedTransmute.lean b/verification/aeneas/lean/Obligations/OwnedTransmute.lean new file mode 100644 index 0000000000..242eaa11a4 --- /dev/null +++ b/verification/aeneas/lean/Obligations/OwnedTransmute.lean @@ -0,0 +1,40 @@ +/- Copyright 2026 The Fuchsia Authors +SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT -/ + +module +public import Obligations.Byteorder +@[expose] public section +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations + +-- Retain the independent positional digit expectations used for numerical +-- byteorder. These expectations inspect arbitrary outcomes, not executions. +def owned_transmute_to_bytes_spec_contract (value : U32) + (run : Result (Aeneas.Std.Array U8 4#usize)) : Prop := + write_u32_le_spec_contract value run + +def owned_transmute_to_bytes_spec : Prop := + ∀ value, owned_transmute_to_bytes_spec_contract value (util.owned_transmute.to_bytes value) + +def owned_transmute_from_bytes_spec_contract (bytes : Aeneas.Std.Array U8 4#usize) + (run : Result U32) : Prop := read_u32_le_spec_contract bytes run + +def owned_transmute_from_bytes_spec : Prop := + ∀ bytes, owned_transmute_from_bytes_spec_contract bytes (util.owned_transmute.from_bytes bytes) + +def owned_transmute_bool_spec_contract (byte : U8) (run : Result (Option Bool)) : Prop := + run ⦃ output => match output with + | none => 2 ≤ byte.val + | some value => byte.val < 2 ∧ value = decide (byte.val = 1) ⦄ + +def owned_transmute_bool_spec : Prop := + ∀ byte, owned_transmute_bool_spec_contract byte (util.owned_transmute.checked_bool byte) + +def owned_transmute_round_trip_checks_spec_contract (_value : U32) (run : Result Unit) : Prop := + run ⦃ _ => True ⦄ + +def owned_transmute_round_trip_checks_spec : Prop := + ∀ value, owned_transmute_round_trip_checks_spec_contract value + (util.owned_transmute.round_trip_checks value) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/OwnedTransmute.lean b/verification/aeneas/lean/Proofs/OwnedTransmute.lean new file mode 100644 index 0000000000..50cd71ebf5 --- /dev/null +++ b/verification/aeneas/lean/Proofs/OwnedTransmute.lean @@ -0,0 +1,108 @@ +/- Copyright 2026 The Fuchsia Authors +SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT -/ + +module +public import Specs +public import BytesAdapter +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs.Raw + +theorem owned_transmute_to_bytes (value : U32) : + util.owned_transmute.to_bytes value ⦃ bytes => + bytes.val.map U8.bv = Rust.Bytes.encodeLE 4 value.val ⦄ := by + have actual : util.owned_transmute.to_bytes value = + .ok (core.num.U32.to_le_bytes value) := rfl + rw [actual] + simp only [WP.spec_ok] + have digits : (core.num.U32.to_le_bytes value).val.map U8.bv = value.bv.toLEBytes := by + simp only [core.num.U32.to_le_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + rw [digits] + exact Rust.Bytes.AeneasAdapter.toLEBytes_eq_encodeLE (by decide) value.bv + +theorem owned_transmute_from_bytes (bytes : Aeneas.Std.Array U8 4#usize) : + util.owned_transmute.from_bytes bytes ⦃ value => + value.val = Rust.Bytes.decodeLE (bytes.val.map U8.bv) ⦄ := by + have actual : util.owned_transmute.from_bytes bytes = + .ok (core.num.U32.from_le_bytes bytes) := rfl + rw [actual] + simp only [WP.spec_ok, core.num.U32.from_le_bytes, UScalar.val, BitVec.toNat_cast] + exact Rust.Bytes.AeneasAdapter.fromLEBytes_toNat _ + +theorem owned_transmute_bool (byte : U8) : + util.owned_transmute.checked_bool byte ⦃ output => match output with + | none => 2 ≤ byte.val + | some value => byte.val < 2 ∧ value = decide (byte.val = 1) ⦄ := by + have actual : core.intrinsics.transmute Bool byte = + if byte.val < 2 then .ok (decide (byte.val = 1)) else forbiddenExecution := rfl + unfold util.owned_transmute.checked_bool + simp only [UScalar.lt_equiv, UScalar.ofNatCore_val_eq] + by_cases below : byte.val < 2 + · simp only [if_pos below] + rw [actual] + simp only [if_pos below, bind_ok, WP.spec_ok] + exact ⟨below, trivial⟩ + · simp only [if_neg below, WP.spec_ok] + omega + +theorem owned_transmute_round_trip_checks (value : U32) : + util.owned_transmute.round_trip_checks value ⦃ _ => True ⦄ := by + have digits : (core.num.U32.to_le_bytes value).val.map U8.bv = value.bv.toLEBytes := by + simp only [core.num.U32.to_le_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + have identical : core.num.U32.from_le_bytes (core.num.U32.to_le_bytes value) = value := by + apply UScalar.eq_of_val_eq + change (BitVec.fromLEBytes ((core.num.U32.to_le_bytes value).val.map U8.bv)).toNat = value.bv.toNat + rw [digits, Rust.Bytes.AeneasAdapter.fromLEBytes_toNat] + exact Rust.Bytes.AeneasAdapter.decodeLE_toLEBytes (by decide) value.bv + have actualTo : util.owned_transmute.to_bytes value = + .ok (core.num.U32.to_le_bytes value) := rfl + have actualFrom : util.owned_transmute.from_bytes (core.num.U32.to_le_bytes value) = + .ok (core.num.U32.from_le_bytes (core.num.U32.to_le_bytes value)) := rfl + simp [util.owned_transmute.round_trip_checks, actualTo, actualFrom, identical, bind_ok] + +end Zerocopy.Proofs.Raw +namespace Zerocopy.Proofs + +theorem owned_transmute_to_bytes_spec : Specs.owned_transmute_to_bytes_spec := by + intro value mathValue decoded + have same := (decodeUScalar_iff value mathValue).mp decoded + apply WP.spec_mono (Raw.owned_transmute_to_bytes value) + intro bytes facts + refine ⟨unsignedArray bytes, decodeArray_unsigned bytes, ?_⟩ + change _ = Rust.Bytes.encodeLE 4 mathValue.value + rw [decodedArray_bytes_eq bytes (unsignedArray bytes) (decodeArray_unsigned bytes), ← same] + exact facts + +theorem owned_transmute_from_bytes_spec : Specs.owned_transmute_from_bytes_spec := by + intro bytes mathBytes decoded + apply WP.spec_mono (Raw.owned_transmute_from_bytes bytes) + intro value facts + refine ⟨unsignedWord value, rfl, ?_⟩ + change value.val = _ + rw [decodedArray_bytes_eq bytes mathBytes decoded] + exact facts + +theorem owned_transmute_bool_spec : Specs.owned_transmute_bool_spec := by + intro byte mathByte decoded + have same := (decodeUScalar_iff byte mathByte).mp decoded + apply WP.spec_mono (Raw.owned_transmute_bool byte) + intro output facts + refine ⟨output, ?_, ?_⟩ + · cases output <;> rfl + · cases output <;> simpa only [← same] using facts + +theorem owned_transmute_round_trip_checks_spec : Specs.owned_transmute_round_trip_checks_spec := by + intro value _ _ + apply WP.spec_mono (Raw.owned_transmute_round_trip_checks value) + intro _ _ + exact ⟨(), rfl, trivial⟩ + +-- Invalid representations must fail before constructing a Boolean, even for +-- a True postcondition. Discarding the result cannot erase forbidden execution. +example : ¬ (core.intrinsics.transmute Bool 2#u8 ⦃ _ => True ⦄) := by + change ¬ (Result.fail Error.undef : Result Bool) ⦃ _ => True ⦄ + simp + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/OwnedTransmute.lean b/verification/aeneas/lean/RequiredModelContracts/OwnedTransmute.lean new file mode 100644 index 0000000000..c2bc1ec339 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/OwnedTransmute.lean @@ -0,0 +1,42 @@ +/- Copyright 2026 The Fuchsia Authors +SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT -/ + +module +public import RequiredModelContracts.Byteorder +public import Obligations.OwnedTransmute +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +-- These bridges reuse positional digit expectations, not implementation +-- correctness. Every provided hypothesis is about the same arbitrary run. +@[contract_simps] theorem required_owned_transmute_to_bytes (value : U32) + (run : Result (Aeneas.Std.Array U8 4#usize)) + (provided : Specs.owned_transmute_to_bytes_spec_contract value run) : + Obligations.owned_transmute_to_bytes_spec_contract value run := by + exact required_write_u32_le value run provided + +@[contract_simps] theorem required_owned_transmute_from_bytes (bytes : Aeneas.Std.Array U8 4#usize) + (run : Result U32) (provided : Specs.owned_transmute_from_bytes_spec_contract bytes run) : + Obligations.owned_transmute_from_bytes_spec_contract bytes run := by + exact required_read_u32_le bytes run provided + +@[contract_simps] theorem required_owned_transmute_bool (byte : U8) + (run : Result (Option Bool)) (provided : Specs.owned_transmute_bool_spec_contract byte run) : + Obligations.owned_transmute_bool_spec_contract byte run := by + apply WP.spec_mono (provided (unsignedWord byte) rfl) + rintro output ⟨value, decoded, facts⟩ + have identityDecode : RustModel.decode output = some output := by + cases output <;> rfl + have same : value = output := Option.some.inj (decoded.symm.trans identityDecode) + subst value + cases output <;> exact facts + +@[contract_simps] theorem required_owned_transmute_round_trip_checks (value : U32) + (run : Result Unit) (provided : Specs.owned_transmute_round_trip_checks_spec_contract value run) : + Obligations.owned_transmute_round_trip_checks_spec_contract value run := by + apply WP.spec_mono (provided (unsignedWord value) rfl) + rintro _ ⟨_, _, _⟩ + trivial + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index 23aed8ce7f..68313fb2df 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -54,6 +54,34 @@ noncomputable def util.transmute_unchecked {Src : Type} (Dst : Type) else forbiddenExecution else forbiddenExecution +-- The standard primitive uses a closed, interpretation-only provider. Original +-- Rust endpoint admission and compiled call auditing bind every reached use to +-- one of these fixed providers; no arbitrary dictionary enters a Rust root. +-- This preserves endpoint identity without testing equality of erased Types. +class Zerocopy.StdOwnedTransmute (Src Dst : Type) where + run : Src → Result Dst + +instance Zerocopy.stdTransmuteU32ToBytes : + Zerocopy.StdOwnedTransmute U32 (Array U8 4#usize) where + run value := .ok (core.num.U32.to_le_bytes value) + +instance Zerocopy.stdTransmuteBytesToU32 : + Zerocopy.StdOwnedTransmute (Array U8 4#usize) U32 where + run bytes := .ok (core.num.U32.from_le_bytes bytes) + +instance Zerocopy.stdTransmuteU8ToBool : Zerocopy.StdOwnedTransmute U8 Bool where + run byte := if byte.val < 2 then .ok (decide (byte.val = 1)) else forbiddenExecution + +-- The additional implicit parameter is explicitly part of the reviewed std +-- boundary, not a translated Rust trait argument. Other endpoints are rejected +-- by admission and have no registered provider. The numeric cases require the +-- independently checked little-endian compiler profile; Boolean validity does +-- not depend on byte order. +def core.intrinsics.transmute {Src : Type} (Dst : Type) + [provider : Zerocopy.StdOwnedTransmute Src Dst] (src : Src) : Result Dst := + provider.run src + + @[simp] def core.num.nonzero.NonZero.get {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) (x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val diff --git a/verification/aeneas/negative-control-family.sh b/verification/aeneas/negative-control-family.sh index 77cc4aa6d2..3db0053065 100644 --- a/verification/aeneas/negative-control-family.sh +++ b/verification/aeneas/negative-control-family.sh @@ -24,7 +24,7 @@ echo "Testing failure controls in $1" # suite starts and is removed on exit. Use the same roster for both decisions # so cleanup cannot delete a source that belonged to an earlier editor session. control_files=( - NegativeControl.lean WeakOutcome.lean + StdTransmuteAuditProbe.lean NegativeControl.lean WeakOutcome.lean RoundingConstructorControl.lean RoundingDomainControl.lean Zerocopy/ScopeControl.lean Zerocopy/ShapeControl.lean Zerocopy/ModelControl.lean Proofs/WitnessOwnerControl.lean Proofs/PaddingDependencyControl.lean @@ -822,13 +822,16 @@ if grep -Fq 'def core.mem.align_of' Zerocopy/FunsExternal.lean; then python3 - <<'PYCONTROL' from pathlib import Path s = Path("Check.lean").read_text() -begin = ' let env ← getEnv\n' +# Select the top-level audit command. The standalone probe consumes the carrier +# set because its normal consumer follows this prefix in the full audit. +begin = 'run_elab do\n let env ← getEnv\n' end = ' let mut proofModules : Array ModuleIdx := #[]' if s.count(begin) != 1 or s.count(end) != 1: raise SystemExit("External-input audit control boundaries no longer match") -body = s[s.index(begin):s.index(end)] +body = s[s.index(begin) + len('run_elab do\n'):s.index(end)] Path("NegativeControl.lean").write_text( - 'import Lean\nimport Zerocopy.FunsExternal\nopen Lean Elab Command\nrun_elab do\n' + body) + 'import Lean\nimport Zerocopy.FunsExternal\nopen Lean Elab Command\nrun_elab do\n' + body + + ' let _ := opaqueCarriers\n pure ()\n') PYCONTROL aeneas_lake env lean -DwarningAsError=true NegativeControl.lean \ > "$backup/abi-baseline.log" 2>&1 || { @@ -1572,6 +1575,15 @@ expect_failure "a min implementation with its comparison reversed" min-build.log restore_build audit fi # semantics +if [[ $AENEAS_CONTROL_FAMILY == owned-std ]] && has_model util.owned_transmute.to_bytes; then + # This family has its own frozen project and preserves exact command logs. + # Standard-boundary controls inspect original endpoints in both compiler + # stages, then challenge whole definitions and canonical native providers. + python3 -B "$repo/verification/aeneas/control_runner.py" command \ + "$AENEAS_CONTROL_LOG_DIR/commands" -- python3 -B \ + "$repo/verification/aeneas/tests/std_transmute_controls.py" \ + --work "$PWD" --runtime "$tools_dir" --evidence "$backup/owned-std-evidence" +fi control_complete=yes ) check_workspace "$AENEAS_CONTROL_MODEL" diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 5911ea7f12..8992e2fb55 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -184,6 +184,42 @@ spec min_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.min_spec for Zerocopy.util.min with 2 +check_model_inputs Zerocopy.util.owned_transmute.to_bytes with 0 type parameters +aeneas_spec_begin +spec owned_transmute_to_bytes_spec + for @Zerocopy.util.owned_transmute.to_bytes with 0 type parameters + ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + Rust.Bytes.encodeLE 4 (value : Nat) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.owned_transmute_to_bytes_spec for Zerocopy.util.owned_transmute.to_bytes with 1 + +check_model_inputs Zerocopy.util.owned_transmute.from_bytes with 0 type parameters +aeneas_spec_begin +spec owned_transmute_from_bytes_spec + for @Zerocopy.util.owned_transmute.from_bytes with 0 type parameters + ensures value => (value : Nat) = Rust.Bytes.decodeLE + (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.owned_transmute_from_bytes_spec for Zerocopy.util.owned_transmute.from_bytes with 1 + +check_model_inputs Zerocopy.util.owned_transmute.checked_bool with 0 type parameters +aeneas_spec_begin +spec owned_transmute_bool_spec + for @Zerocopy.util.owned_transmute.checked_bool with 0 type parameters + ensures output => match output with + | none => 2 ≤ (byte : Nat) + | some value => (byte : Nat) < 2 ∧ value = decide ((byte : Nat) = 1) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.owned_transmute_bool_spec for Zerocopy.util.owned_transmute.checked_bool with 1 + +check_model_inputs Zerocopy.util.owned_transmute.round_trip_checks with 0 type parameters +aeneas_spec_begin +spec owned_transmute_round_trip_checks_spec + for @Zerocopy.util.owned_transmute.round_trip_checks with 0 type parameters + ensures _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.owned_transmute_round_trip_checks_spec for Zerocopy.util.owned_transmute.round_trip_checks with 1 + check_model_inputs Zerocopy.util.safety_checks.checked_bool with 0 type parameters aeneas_spec_begin spec checked_bool_spec diff --git a/verification/aeneas/tests/std_transmute_controls.py b/verification/aeneas/tests/std_transmute_controls.py new file mode 100644 index 0000000000..3b32c4eef9 --- /dev/null +++ b/verification/aeneas/tests/std_transmute_controls.py @@ -0,0 +1,173 @@ +# Copyright 2026 The Fuchsia Authors +# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT + +"""Challenge standard-transmute endpoint admission and compiled providers. + +Compiler mutations stay in memory. Lean mutations affect only a disposable +project and are restored and rebuilt. No invalid Rust execution is performed. +""" + +import argparse +import copy +import json +import os +from pathlib import Path +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[3] +sys.path.insert(0, str(ROOT / 'verification/aeneas')) +import admission +import toolchain + + +def nodes(value): + if isinstance(value, dict): + yield value + for child in value.values(): + yield from nodes(child) + elif isinstance(value, list): + for child in value: + yield from nodes(child) + + +def admission_controls(work, evidence): + registry = json.loads((ROOT / 'verification/aeneas/external.json').read_text()) + manifest = json.loads((work / 'bindings.json').read_text()) + laws = [row['rust'] for row in manifest['trait_laws']] + owner = 'zerocopy::util::owned_transmute::to_bytes' + for stage, filename in [('before', 'zerocopy.before.ullbc'), ('llbc', 'zerocopy.llbc')]: + data = json.loads((work / filename).read_text()) + baseline = admission.Admission(data, registry, laws) + baseline.audit([owner]) + helper = next(f for f in baseline.functions.values() + if baseline.name(f['item_meta']['name']) == owner + '_native') + intrinsic = next(i for i, f in baseline.functions.items() + if baseline.name(f['item_meta']['name']) == 'core::intrinsics::transmute') + calls = [node['Regular'] for node in nodes(helper['body']) + if node.get('Regular', {}).get('kind', {}).get('Fun') == intrinsic] + if len(calls) != 1: + raise ValueError('Expected one standard call in the actual unannotated helper') + original = copy.deepcopy(calls[0]['generics']['types']) + calls[0]['generics']['types'][0] = {'Untagged': {'Scalar': { + 'Integer': {'Unsigned': 'U16'}}}} + try: + admission.Admission(data, registry, laws).audit([owner]) + except ValueError as error: + if 'Unsupported standard transmute instantiation' not in str(error): + raise ValueError('Endpoint mutation failed outside its intended guard') from error + evidence.append({'case': stage + '-unsupported-endpoint', 'rejection': str(error)}) + else: + raise ValueError('Accepted an unsupported original Rust endpoint') + finally: + calls[0]['generics']['types'] = original + for key, bad in [('is_little_endian', False), ('target_pointer_size', 4)]: + target = data['translated']['target_information'][0]['value'] + old = target[key] + target[key] = bad + try: + admission.Admission(data, registry, laws) + except ValueError as error: + if 'little-endian 64-bit target' not in str(error): + raise + evidence.append({'case': stage + '-' + key, 'rejection': str(error)}) + else: + raise ValueError('Accepted an unsupported original target profile') + finally: + target[key] = old + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--work', type=Path, required=True) + parser.add_argument('--runtime', type=Path, required=True) + parser.add_argument('--evidence', type=Path, required=True) + args = parser.parse_args() + work, runtime, output = args.work.resolve(), args.runtime.resolve(), args.evidence.resolve() + standard = work in [ROOT / 'target/aeneas/verification', ROOT / 'target/aeneas/golden-verification'] + private = (work.name == 'project' and work.parent.parent.name.startswith('control-sandboxes-') + and work.parent.parent.parent == ROOT / 'target/aeneas' + and os.environ.get('AENEAS_CONTROL_PROJECT') == str(work) + and os.environ.get('AENEAS_CONTROL_REPO') == str(ROOT)) + if not (standard or private): + raise ValueError('Controls require a disposable verification project') + toolchain.validate(ROOT, runtime) + output.mkdir(parents=True, exist_ok=False) + environment = toolchain.runtime_env(runtime) + environment['LEAN_NUM_THREADS'] = '2' + results = [] + admission_controls(work, results) + source = (ROOT / 'verification/aeneas/lean/Check.lean').read_text() + begin = source.index('-- This closed boundary') + end = source.index('run_elab do\n') + probe = work / 'StdTransmuteAuditProbe.lean' + if probe.exists() or probe.is_symlink(): + raise ValueError('Control probe already belongs to an earlier session') + probe.write_text('import Lean\nimport Zerocopy.Funs\nopen Lean Elab Command\n' + source[begin:end] + + 'run_elab do\n let contents ← IO.FS.readFile "bindings.json"\n' + ' let .ok bindings := Json.parse contents | throwError "Invalid control bindings"\n' + ' auditStdTransmute bindings\n') + external, native = work / 'Zerocopy/FunsExternal.lean', work / 'Zerocopy/Funs.lean' + originals = {external: external.read_text(), native: native.read_text()} + start = originals[external].index('instance Zerocopy.stdTransmuteU8ToBool :') + end = originals[external].index('\n-- The additional implicit parameter', start) + boolean = originals[external][start:end] + if boolean.count('else forbiddenExecution') != 1: + raise ValueError('Boolean provider control boundary changed') + + def run(label, command, expected=''): + log = output / (label + '.log') + with log.open('w') as stream: + result = subprocess.run(command, cwd=work, env=environment, + stdout=stream, stderr=subprocess.STDOUT) + contents = log.read_text() + results.append({'case': label, 'command': command, 'exit_code': result.returncode, + 'log': str(log), 'expected_rejection': expected}) + if expected: + if result.returncode == 0 or expected not in contents: + raise ValueError(f'{label} did not fail at its intended audit: {log}') + elif result.returncode: + raise ValueError(f'{label} failed: {log}') + + build = ['lake', '--old', 'build', '+Zerocopy.Funs:olean'] + audit = ['lake', '--old', 'env', 'lean', '-DwarningAsError=true', probe.name] + try: + run('positive-audit', audit) + for case in ['failure-erasure', 'opaque-provider', 'shadow-provider']: + for path, text in originals.items(): + path.write_text(text) + if case == 'failure-erasure': + external.write_text(originals[external][:start] + + boolean.replace('else forbiddenExecution', 'else .ok false') + originals[external][end:]) + rejection = 'changed its whole interpretation' + elif case == 'opaque-provider': + external.write_text(originals[external][:start] + + 'axiom Zerocopy.stdTransmuteU8ToBool : Zerocopy.StdOwnedTransmute U8 Bool\n' + 'attribute [instance] Zerocopy.stdTransmuteU8ToBool\n' + originals[external][end:]) + rejection = 'must be a definition' + else: + external.write_text(originals[external] + + '\n@[reducible] def Zerocopy.shadowStdProvider :\n' + ' Zerocopy.StdOwnedTransmute U32 (Array U8 4#usize) :=\n' + ' Zerocopy.stdTransmuteU32ToBytes\n') + needle = 'core.intrinsics.transmute (Array Std.U8 4#usize) value' + if originals[native].count(needle) != 1: + raise ValueError('Expected one native primitive call in the unannotated helper') + native.write_text(originals[native].replace(needle, + 'core.intrinsics.transmute (Array Std.U8 4#usize) (provider := Zerocopy.shadowStdProvider) value')) + rejection = 'did not retain its canonical endpoint provider' + run(case + '-elaboration', build) + run(case + '-rejection', audit, rejection) + finally: + for path, text in originals.items(): + path.write_text(text) + try: + run('restored-native-elaboration', build) + run('restored-positive-audit', audit) + finally: + probe.unlink(missing_ok=True) + (output / 'evidence.json').write_text(json.dumps({'restored': True, 'results': results}, indent=2) + '\n') + + +if __name__ == '__main__': + main() diff --git a/verification/aeneas/tests/test_admission.py b/verification/aeneas/tests/test_admission.py index eaef9e4f31..de8ef8409f 100644 --- a/verification/aeneas/tests/test_admission.py +++ b/verification/aeneas/tests/test_admission.py @@ -240,6 +240,18 @@ def test_compiler_override_is_rejected_before_compilation(self): with self.assertRaisesRegex(ValueError, 'compiler override RUSTFLAGS'): admission.input_identity(ROOT) + def test_target_override_is_rejected_before_compilation(self): + with mock.patch.dict(os.environ, {'CARGO_BUILD_TARGET': 'aarch64-apple-darwin'}, clear=True): + with self.assertRaisesRegex(ValueError, 'compiler override CARGO_BUILD_TARGET'): + admission.input_identity(ROOT) + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + (root / '.cargo').mkdir() + (root / '.cargo/config.toml').write_text('[build]\ntarget = "powerpc64-unknown-linux-gnu"\n') + with mock.patch.dict(os.environ, {'CARGO_HOME': str(root / 'cargo')}, clear=True): + with self.assertRaisesRegex(ValueError, 'Cargo compiler configuration'): + admission.input_identity(root) + def test_nonzero_constructor_template_preserves_guarded_result_and_dictionary(self): leaf = 'core.num.nonzero.NonZero.new_unchecked' evidence = {'stages': {'llbc': {'executions': [{'rust': 'std constructor', 'lean': leaf}]}}} diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index 8235c0f3d1..e9167686c1 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -14,6 +14,9 @@ pub(crate) mod macros; #[doc(hidden)] pub mod macro_util; +#[cfg(target_endian = "little")] +#[allow(dead_code)] +mod owned_transmute; mod safety_checks; use core::{ diff --git a/zerocopy/src/util/owned_transmute.rs b/zerocopy/src/util/owned_transmute.rs new file mode 100644 index 0000000000..1f5eb2d5f2 --- /dev/null +++ b/zerocopy/src/util/owned_transmute.rs @@ -0,0 +1,104 @@ +// Copyright 2026 The Fuchsia Authors +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// Licensed under a BSD-style license , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +//! Concrete owned conversions through the standard transmute primitive. +//! +//! This private verification module is selected only on little-endian targets. +//! Verification separately checks the original compiler target and rejects +//! unsupported target overrides. These types have no padding or pointer fields. + +/// Preserves all four bytes of the original integer. +/// +/// ```aeneas +/// spec owned_transmute_to_bytes_spec +/// ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = +/// Rust.Bytes.encodeLE 4 (value : Nat) +/// ``` +fn to_bytes(value: u32) -> [u8; 4] { + to_bytes_native(value) +} + +// This unannotated helper remains in the checked execution closure. +#[allow(unknown_lints)] // unnecessary_transmutes is newer than the MSRV. +#[allow(unnecessary_transmutes)] +fn to_bytes_native(value: u32) -> [u8; 4] { + // SAFETY: Both types have size four, contain no padding, and accept every + // bit pattern. Transmute moves the representation into the owned result. + unsafe { core::mem::transmute::(value) } +} + +/// Interprets every initialized four-byte representation as an integer. +/// +/// ```aeneas +/// spec owned_transmute_from_bytes_spec +/// ensures value => (value : Nat) = Rust.Bytes.decodeLE +/// (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) +/// ``` +#[allow(unknown_lints)] // unnecessary_transmutes is newer than the MSRV. +#[allow(unnecessary_transmutes)] +fn from_bytes(bytes: [u8; 4]) -> u32 { + // SAFETY: Both types have size four, contain no padding, and accept every + // bit pattern. No pointer, borrow, or destructor crosses this conversion. + unsafe { core::mem::transmute::<[u8; 4], u32>(bytes) } +} + +/// Checks Boolean validity before invoking the standard primitive. +/// +/// ```aeneas +/// spec owned_transmute_bool_spec +/// ensures output => match output with +/// | none => 2 ≤ (byte : Nat) +/// | some value => (byte : Nat) < 2 ∧ value = decide ((byte : Nat) = 1) +/// ``` +#[allow(clippy::transmute_int_to_bool)] // Exercise the standard primitive itself. +fn checked_bool(byte: u8) -> Option { + if byte < 2 { + // SAFETY: u8 and bool have size one and no padding. The guard admits + // exactly Boolean representations zero and one before construction. + Some(unsafe { core::mem::transmute::(byte) }) + } else { + None + } +} + +/// Checks the complete owned integer round trip. +/// +/// ```aeneas +/// spec owned_transmute_round_trip_checks_spec +/// ensures _ => True +/// ``` +fn round_trip_checks(value: u32) { + let bytes = to_bytes(value); + let restored = from_bytes(bytes); + assert!(restored == value); +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn concrete_examples() { + for value in [0, 1, 0x1234_5678, u32::MAX] { + assert_eq!(to_bytes(value), value.to_le_bytes()); + assert_eq!(from_bytes(value.to_le_bytes()), value); + round_trip_checks(value); + } + for byte in 0..=u8::MAX { + assert_eq!( + checked_bool(byte), + match byte { + 0 => Some(false), + 1 => Some(true), + _ => None, + } + ); + } + } +}