From d3f61ab4c00990ff84d06c0b0fe5fa0e32763866 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 8 Oct 2026 19:38:44 -0400 Subject: [PATCH] Prove guarded Boolean conversion and byte copying Exercise the registered unsafe boundaries with small extracted Rust callers. Check the raw byte before producing a Bool, accepting exactly 0 and 1. Check destination capacity before copying a prefix, and prove the complete updated slice, preserved suffix and unchanged rejection. Interpret invalid Boolean production and oversized copying as forbidden execution using Aeneas's undef tag. Both total and partial contracts must reject it, including when a caller discards the value or later diverges. Check complete primitive definitions and mutation controls, rather than only their successful branches. The union and pointer implementations remain reviewed, source-bound interpretations. The proofs establish the callers' guards and value behavior under those interpretations and valid-reference premises. Agent-authored-by: AI agent acting on joshlf's behalf gherrit-pr-id: Gsfnevxtkkrjpqabfdz42n6ncfeyaul7y --- tools/aeneas-inline/src/main.rs | 14 ++- verification/aeneas/README.md | 25 +++++ verification/aeneas/control_runner.py | 2 +- verification/aeneas/golden/Funs.lean | 30 ++++- .../aeneas/golden/FunsExternal_Template.lean | 9 ++ verification/aeneas/lean/Check.lean | 25 +++++ .../aeneas/lean/Obligations/SafetyChecks.lean | 32 ++++++ .../aeneas/lean/Proofs/SafetyChecks.lean | 80 +++++++++++++ .../RequiredModelContracts/SafetyChecks.lean | 37 ++++++ verification/aeneas/lean/SafetyTests.lean | 58 ++++++++++ .../aeneas/lean/Zerocopy/FunsExternal.lean | 35 ++++++ .../aeneas/negative-control-extraction.sh | 4 + .../aeneas/negative-control-family.sh | 42 +++++++ verification/aeneas/projections/Specs.lean | 18 +++ .../aeneas/tests/producer-controls.sh | 106 ++++++++++++++++++ .../aeneas/tests/producer-controls/Cargo.lock | 7 ++ .../aeneas/tests/producer-controls/Cargo.toml | 7 ++ .../aeneas/tests/producer-controls/Check.lean | 29 +++++ .../aeneas/tests/producer-controls/src/lib.rs | 60 ++++++++++ .../aeneas/tests/test_control_runner.py | 48 ++++++++ verification/aeneas/tests/test_inline.py | 9 ++ zerocopy/src/util/mod.rs | 2 + zerocopy/src/util/safety_checks/mod.rs | 96 ++++++++++++++++ 23 files changed, 769 insertions(+), 6 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/SafetyChecks.lean create mode 100644 verification/aeneas/lean/Proofs/SafetyChecks.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/SafetyChecks.lean create mode 100644 verification/aeneas/lean/SafetyTests.lean create mode 100755 verification/aeneas/tests/producer-controls.sh create mode 100644 verification/aeneas/tests/producer-controls/Cargo.lock create mode 100644 verification/aeneas/tests/producer-controls/Cargo.toml create mode 100644 verification/aeneas/tests/producer-controls/Check.lean create mode 100644 verification/aeneas/tests/producer-controls/src/lib.rs create mode 100644 zerocopy/src/util/safety_checks/mod.rs diff --git a/tools/aeneas-inline/src/main.rs b/tools/aeneas-inline/src/main.rs index f54fa089d4..8a64b35a82 100644 --- a/tools/aeneas-inline/src/main.rs +++ b/tools/aeneas-inline/src/main.rs @@ -129,7 +129,8 @@ impl Functions<'_> { supported &= receiver.reference.is_none() || receiver.mutability.is_none(); } syn::FnArg::Typed(input) => { - supported &= !unsupported_borrow(&input.ty, true); + supported &= + !unsupported_borrow(&input.ty, true) || mutable_byte_slice(&input.ty); match input.pat.as_ref() { syn::Pat::Ident(pattern) if pattern.by_ref.is_none() && pattern.subpat.is_none() => @@ -298,6 +299,17 @@ fn unsupported_borrow(ty: &syn::Type, allow_shared: bool) -> bool { visitor.found } +// Aeneas returns this mutable input as ordinary updated byte-slice state. +// This narrow shape has no nested loans, stored references, or escaping borrow +// transformer. Other mutable inputs remain unsupported until their returned +// state and reconstruction semantics have an explicit audit. +fn mutable_byte_slice(ty: &syn::Type) -> bool { + let syn::Type::Reference(reference) = ty else { return false }; + let syn::Type::Slice(slice) = reference.elem.as_ref() else { return false }; + let syn::Type::Path(element) = slice.elem.as_ref() else { return false }; + reference.mutability.is_some() && element.qself.is_none() && element.path.is_ident("u8") +} + fn has_borrowed_fields(fields: &Value) -> bool { // Struct fields and enum variants share the report's recursive container // shape. A borrowed field in any variant makes the nominal owner unsupported. diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 20ca4da81b..5319434f5a 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -168,6 +168,31 @@ builtin correspondence also remains part of the pinned translator's trust boundary. See [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) for the implemented fragment and [LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the erasure inventory. +The first storage examples are in +[`util/safety_checks/mod.rs`](../../zerocopy/src/util/safety_checks/mod.rs): + +- `checked_bool` accepts exactly byte encodings 0 and 1 and rejects all others. +- `checked_copy` copies a fitting prefix, preserves the suffix, and leaves the + entire destination unchanged when the source is too long. Its model returns + the updated mutable slice explicitly. + +The existing production `add_scaled_metadata` exercises guarded unchecked +addition and multiplication. Each of these four primitive definitions has an +independent complete-definition check, including its forbidden branch. Kernel +controls prove rejection even if an invalid result is discarded or followed by +divergence. Extraction controls check actual generated callers that discard an +invalid Boolean or reach it before a loop. Mutation controls also challenge the +failure tag and helper guards. + +Incoming references must already denote valid Rust allocations with the +necessary exclusivity and initializedness. Logical byte lists do not establish +provenance, allocation lifetime, or reference validity. Both storage examples +use padding-free `u8`/`bool`; general padding and typed-copy effects remain +unsupported. No panic-catching, thread, callback, or failure-recovery model is +admitted. Both today's total and partial contracts reject *every* execution +failure, including source UB aborts whose tag the pinned importer merges with +panic. Supporting a recovery handler would require preserving that distinction. + The binding manifest records both inspected snapshots, their dependency closures, exact registry identity, sources, compiler configuration, and patched runtime. Inputs are captured before compilation and checked again during binding diff --git a/verification/aeneas/control_runner.py b/verification/aeneas/control_runner.py index d42318c462..e5f67ee322 100644 --- a/verification/aeneas/control_runner.py +++ b/verification/aeneas/control_runner.py @@ -26,7 +26,7 @@ import tempfile import time -FAMILIES = ('authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi', +FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi', 'contracts', 'dependencies', 'admission', 'semantics') MODELS = ('golden-verification', 'verification') FIXTURES = ('NegativeControl.lean', 'WeakOutcome.lean', diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index f63b0dc3e7..a5dfa5edf3 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -65,7 +65,7 @@ def Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner : } /-- [zerocopy::util::padding_needed_for]: - Source: 'src/util/mod.rs', lines 161:0-221:1 -/ + Source: 'src/util/mod.rs', lines 163:0-223:1 -/ def util.padding_needed_for (len : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -81,7 +81,7 @@ def util.padding_needed_for ok (i2 &&& mask) /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: - Source: 'src/util/mod.rs', lines 248:0-266:1 -/ + Source: 'src/util/mod.rs', lines 250:0-268:1 -/ def util.round_down_to_next_multiple_of_alignment (n : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -98,7 +98,7 @@ def util.round_down_to_next_multiple_of_alignment ok (n &&& mask) /-- [zerocopy::util::max]: - Source: 'src/util/mod.rs', lines 275:0-281:1 -/ + Source: 'src/util/mod.rs', lines 277:0-283:1 -/ def util.max (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) @@ -118,7 +118,7 @@ def util.max else ok a /-- [zerocopy::util::min]: - Source: 'src/util/mod.rs', lines 290:0-296:1 -/ + Source: 'src/util/mod.rs', lines 292:0-298:1 -/ def util.min (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) @@ -137,4 +137,26 @@ def util.min then ok b else ok a +/-- [zerocopy::util::safety_checks::checked_bool]: + Source: 'src/util/safety_checks/mod.rs', lines 28:0-38:1 -/ +def util.safety_checks.checked_bool + (byte : Std.U8) : Result (Option Bool) := do + if byte < 2#u8 + then let b ← util.transmute_unchecked Bool byte + ok (some b) + else ok none + +/-- [zerocopy::util::safety_checks::checked_copy]: + Source: 'src/util/safety_checks/mod.rs', lines 51:0-61:1 -/ +def util.safety_checks.checked_copy + (src : Slice Std.U8) (dst : Slice Std.U8) : + Result (Bool × (Slice Std.U8)) + := do + let i := Slice.len src + let i1 := Slice.len dst + if i <= i1 + then let dst1 ← util.copy_unchecked src dst + ok (true, dst1) + else ok (false, dst) + end Zerocopy diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index ccb87a43d6..fd2ceb84e7 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -50,3 +50,12 @@ axiom core.num.nonzero.NonZero.get core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) : core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T +/-- [zerocopy::util::copy_unchecked]: + Source: 'src/util/mod.rs', lines 310:0-325: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 -/ +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 8a7e3d6b0a..084929939d 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -63,6 +63,31 @@ run_elab do throwError "Missing external size read" unless ← Meta.isDefEq (mkConst `core.mem.size_of) sizeRead do throwError "External size read changed its data-input interpretation" + if env.contains `util.transmute_unchecked then + let expected ← Term.elabTerm (← `(fun {Src : Type} (Dst : Type) (src : Src) => by + classical + exact if hs : Src = Aeneas.Std.U8 then + if hd : Dst = Bool then + let byte := cast hs src + if byte.val < 2 then Aeneas.Std.Result.ok (cast hd.symm (decide (byte.val = 1))) + else Aeneas.Std.Result.fail Aeneas.Std.Error.undef + else Aeneas.Std.Result.fail Aeneas.Std.Error.undef + else Aeneas.Std.Result.fail Aeneas.Std.Error.undef)) none + Term.synthesizeSyntheticMVarsNoPostponing + unless ← Meta.isDefEq (mkConst `util.transmute_unchecked) (← instantiateMVars expected) do + throwError "External Boolean conversion changed its complete interpretation" + if env.contains `util.copy_unchecked then + let expected ← Term.elabTerm (← `(fun (src dst : Aeneas.Std.Slice Aeneas.Std.U8) => + if h : src.val.length ≤ dst.val.length then + Aeneas.Std.Result.ok (Aeneas.Std.Slice.from + (src.val ++ dst.val.drop src.val.length) (by + have := dst.property + simp only [List.length_append, List.length_drop] + omega)) + else Aeneas.Std.Result.fail Aeneas.Std.Error.undef)) none + Term.synthesizeSyntheticMVarsNoPostponing + unless ← Meta.isDefEq (mkConst `util.copy_unchecked) (← instantiateMVars expected) do + throwError "External byte copy changed its complete interpretation" -- Module indices identify declarations by compiled ownership. A matching -- namespace is insufficient: a generated or unrelated module could otherwise -- install a theorem under a handwritten proof's expected name. diff --git a/verification/aeneas/lean/Obligations/SafetyChecks.lean b/verification/aeneas/lean/Obligations/SafetyChecks.lean new file mode 100644 index 0000000000..13e489adef --- /dev/null +++ b/verification/aeneas/lean/Obligations/SafetyChecks.lean @@ -0,0 +1,32 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Zerocopy +@[expose] public section +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations + +-- The independent expectations describe all inputs, including rejected bytes +-- and insufficient destinations. They are propositions, not trusted axioms. +def checked_bool_spec_contract (byte : U8) (run : Result (Option Bool)) : Prop := + run ⦃ out => out = if byte.val < 2 then some (decide (byte.val = 1)) else none ⦄ + +def checked_bool_spec : Prop := + ∀ byte, checked_bool_spec_contract byte (util.safety_checks.checked_bool byte) + +def checked_copy_spec_contract (src dst : Slice U8) + (run : Result (Bool × Slice U8)) : Prop := + run ⦃ out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then src.val ++ dst.val.drop src.val.length else dst.val ⦄ + +def checked_copy_spec : Prop := + ∀ src dst, checked_copy_spec_contract src dst (util.safety_checks.checked_copy src dst) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/SafetyChecks.lean b/verification/aeneas/lean/Proofs/SafetyChecks.lean new file mode 100644 index 0000000000..ae2b1edcaa --- /dev/null +++ b/verification/aeneas/lean/Proofs/SafetyChecks.lean @@ -0,0 +1,80 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Specs +public import ModelLemmas +@[expose] public section + +/-! +The callers establish the guards of the trusted conversion and copying helpers. +These are proofs of composition, not proofs of the opaque Rust helper bodies. +The result witnesses additionally check that the actual returned representation, +including the updated mutable slice, decodes successfully. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +private theorem decode_bool_option (value : Option Bool) : + (inferInstance : RustModel (Option Bool)).decode value = some value := by + cases value <;> rfl + +private theorem decode_unsigned_list (values : List U8) : + decodeList (modelUScalar .U8).decode values = some (values.map unsignedWord) := by + induction values with + | nil => rfl + | cons head tail ih => simp [decodeList, ih] + +def byteSlice (raw : Slice U8) : SliceValue (UnsignedWord .U8) := + ⟨raw.val.map unsignedWord, by simpa only [List.length_map] using raw.property⟩ + +theorem decode_byte_slice (raw : Slice U8) : + (modelSlice (α := U8)).decode raw = some (byteSlice raw) := by + apply (decodeSlice_iff (modelUScalar .U8) raw (byteSlice raw)).mpr + exact decode_unsigned_list raw.val + +private theorem decode_copy_result (out : Bool × Slice U8) : + (inferInstance : RustModel (Bool × Slice U8)).decode out = + some (out.1, byteSlice out.2) := by + have decoded := decode_byte_slice out.2 + simp only [RustModel.decode] at decoded ⊢ + rw [decoded] + +theorem checked_bool_raw (byte : U8) : + util.safety_checks.checked_bool byte ⦃ out => + out = if byte.val < 2 then some (decide (byte.val = 1)) else none ⦄ := by + by_cases valid : byte.val < 2 + · simp [util.safety_checks.checked_bool, UScalar.lt_equiv, + UScalar.ofNatCore_val_eq, util.transmute_unchecked, valid, bind_ok] + · simp [util.safety_checks.checked_bool, UScalar.lt_equiv, + UScalar.ofNatCore_val_eq, valid] + +theorem checked_bool_spec : Specs.checked_bool_spec := by + intro byte _ _ + apply WP.spec_mono (checked_bool_raw byte) + intro result same + exact ⟨result, decode_bool_option result, same⟩ + +theorem checked_copy_raw (src dst : Slice U8) : + util.safety_checks.checked_copy src dst ⦃ out => + out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then src.val ++ dst.val.drop src.val.length else dst.val ⦄ := by + by_cases fits : src.val.length ≤ dst.val.length + · simp [util.safety_checks.checked_copy, Slice.len, UScalar.le_equiv, + util.copy_unchecked, fits, bind_ok] + · simp [util.safety_checks.checked_copy, Slice.len, UScalar.le_equiv, + fits] + +theorem checked_copy_spec : Specs.checked_copy_spec := by + intro src dst _ _ _ _ + apply WP.spec_mono (checked_copy_raw src dst) + intro result facts + exact ⟨(result.1, byteSlice result.2), decode_copy_result result, facts⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/SafetyChecks.lean b/verification/aeneas/lean/RequiredModelContracts/SafetyChecks.lean new file mode 100644 index 0000000000..e43962075b --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/SafetyChecks.lean @@ -0,0 +1,37 @@ +/- 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 RequiredContracts +public import Specs +public import Proofs.SafetyChecks +public import Obligations.SafetyChecks +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +-- These implications quantify over an arbitrary execution. They do not use +-- the successful behavior of the extracted caller to strengthen its contract. +@[contract_simps] theorem required_checked_bool (byte : U8) + (run : Result (Option Bool)) + (provided : Specs.checked_bool_spec_contract byte run) : + Obligations.checked_bool_spec_contract byte run := by + apply WP.spec_mono (provided (unsignedWord byte) rfl) + rintro output ⟨_, _, facts⟩ + exact facts + +@[contract_simps] theorem required_checked_copy (src dst : Slice U8) + (run : Result (Bool × Slice U8)) + (provided : Specs.checked_copy_spec_contract src dst run) : + Obligations.checked_copy_spec_contract src dst run := by + apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src) + (byteSlice dst) (decode_byte_slice dst)) + rintro output ⟨_, _, facts⟩ + exact facts + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/SafetyTests.lean b/verification/aeneas/lean/SafetyTests.lean new file mode 100644 index 0000000000..ec86c7c89e --- /dev/null +++ b/verification/aeneas/lean/SafetyTests.lean @@ -0,0 +1,58 @@ +/- 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 SpecsSyntax +public import Zerocopy.Funs +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace SafetyTests + +-- Sequencing cannot convert forbidden execution into either a value or +-- divergence. In particular, discarding a callee's result is still sequencing. +theorem forbidden_bind {α β : Type} (next : α → Result β) : + (Result.fail .undef >>= next) = Result.fail .undef := bind_fail .undef next + +theorem total_rejects_forbidden {α : Type} (post : α → Prop) : + ¬ WP.spec (.fail .undef) post := by simp + +theorem partial_rejects_forbidden {α : Type} (post : α → Prop) : + ¬ WP.dspec (.fail .undef) post := by simp + +-- Every oversized copy is forbidden, rather than success with truncated +-- output or a recoverable None. The caller proves this branch unreachable. +theorem copy_rejects_oversize (src dst : Slice U8) + (oversize : dst.val.length < src.val.length) : + util.copy_unchecked src dst = .fail .undef := by + simp [util.copy_unchecked, Zerocopy.forbiddenExecution, Nat.not_le.mpr oversize] + +-- This is the model of an unsafe producer with an invalid bit pattern. These +-- examples execute no Rust UB: they examine its forbidden abstract outcome. +noncomputable def badBool : Result Bool := util.transmute_unchecked Bool (2#u8) + +theorem bad_bool_forbidden : badBool = .fail .undef := by + simp [badBool, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val] + +noncomputable def discardCall : Result Unit := do let _ ← badBool; Result.ok () +noncomputable def failThenDiverge : Result Unit := do let _ ← badBool; Result.div +def diverge : Result Unit := .div +spec discarded for discardCall with 0 type parameters + ensures _ => True +partial spec beforeDivergence for failThenDiverge with 0 type parameters + ensures _ => True + +example : ¬discarded := by simp [discarded, discardCall, bad_bool_forbidden] +example : ¬beforeDivergence := by simp [beforeDivergence, failThenDiverge, bad_bool_forbidden] + +-- Even a contract that says nothing about the output must prove its execution +-- judgment. Partial contracts permit divergence, but never preceding UB. +partial spec diverges for diverge with 0 type parameters + ensures _ => True +example : diverges := WP.dspec.div _ + +end SafetyTests diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index c820466380..23aed8ce7f 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -19,6 +19,41 @@ def core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone (x : core.num.niche_types.NonZeroUsizeInner) : Result core.num.niche_types.NonZeroUsizeInner := .ok x +-- A forbidden execution cannot be accepted as an ordinary Rust panic. The +-- backend's existing undef tag also marks unsupported models, so it means +-- "no permitted execution claim", not necessarily that the Rust code has UB. +-- Total and partial contracts both reject it. Future recovery models must +-- propagate it rather than turn it into a successful return or divergence. +def Zerocopy.forbiddenExecution {α : Type} : Result α := .fail .undef + +-- This is an interpretation of the whole Rust helper, whose raw-pointer body +-- is deliberately opaque to extraction. Valid input references supply separate +-- readable source and exclusive destination regions. The additional length +-- guard belongs to execution: violating it must fail even if the caller ignores +-- the result. Payload bytes have no padding or invalid bit patterns. +def util.copy_unchecked (src dst : Slice U8) : Result (Slice U8) := + if h : src.val.length ≤ dst.val.length then + .ok (Slice.from (src.val ++ dst.val.drop src.val.length) (by + have := dst.property + simp only [List.length_append, List.length_drop] + omega)) + else forbiddenExecution + +-- Only the u8-to-bool instantiation is supported. The admission checker also +-- checks the original Rust type arguments, before Aeneas can erase them. This +-- guard checks bit validity BEFORE creating a Bool, whose Lean carrier cannot +-- represent an invalid boolean. All other instantiations fail closed. +noncomputable def util.transmute_unchecked {Src : Type} (Dst : Type) + (src : Src) : Result Dst := by + classical + exact if hs : Src = U8 then + if hd : Dst = Bool then + let byte := cast hs src + if byte.val < 2 then .ok (cast hd.symm (decide (byte.val = 1))) + else forbiddenExecution + else forbiddenExecution + else forbiddenExecution + @[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-extraction.sh b/verification/aeneas/negative-control-extraction.sh index a8d9f8a4d3..4bac330a67 100644 --- a/verification/aeneas/negative-control-extraction.sh +++ b/verification/aeneas/negative-control-extraction.sh @@ -31,5 +31,9 @@ manifest = json.loads(Path(sys.argv[1]).read_text()) if manifest.get('version') != 3 or manifest.get('mode') != 'verified-live': raise SystemExit('Invalid verified bindings for extraction controls') functions = {row['raw'] for row in manifest['bindings'].values() if row['kind'] == 'function'} +print('storage' if 'Zerocopy.util.safety_checks.checked_bool' in functions else '') PY ) +if [[ $capabilities == *storage* ]]; then + run bash verification/aeneas/tests/producer-controls.sh generate "$AENEAS_CONTROL_PRODUCER_DIR" +fi diff --git a/verification/aeneas/negative-control-family.sh b/verification/aeneas/negative-control-family.sh index 56f2eca8de..8db08cddac 100644 --- a/verification/aeneas/negative-control-family.sh +++ b/verification/aeneas/negative-control-family.sh @@ -175,6 +175,13 @@ PYCONTROL has_model() { has_binding function "Zerocopy.$1" } +if [[ $AENEAS_CONTROL_FAMILY == producers ]] && has_model util.safety_checks.checked_bool; then + python3 -B "$repo/verification/aeneas/control_runner.py" command \ + "$AENEAS_CONTROL_LOG_DIR/commands" -- bash \ + "$repo/verification/aeneas/tests/producer-controls.sh" check \ + "$PWD" "$AENEAS_CONTROL_PRODUCER_DIR" +fi + if [[ $AENEAS_CONTROL_FAMILY == trait-rounding ]]; then # A constrained mathematical value can still break an operation promise or its # required raw input domain. Probe the unchanged constructor source fence in an @@ -254,6 +261,41 @@ if ! grep -Fq 'unsupported failure erasure' "$backup/unsafe-erasure-audit.log"; fi restore_build +# Each storage interpretation must reject its bad inputs even when safe callers +# never take that branch. First establish that the mutation still compiles, then +# require the independent complete-definition audit to reject it. +if has_model util.safety_checks.checked_bool; then + for mutation in boolean copy; do + python3 - "$mutation" <<'PYCONTROL' +from pathlib import Path +import sys +p = Path("Zerocopy/FunsExternal.lean") +s = p.read_text() +if sys.argv[1] == 'boolean': + start = s.index('noncomputable def util.transmute_unchecked') + end = s.index('\n\n', start) + before = s[start:end] + after = before.replace('else forbiddenExecution', 'else .ok (cast hd.symm false)', 1) +else: + start = s.index('def util.copy_unchecked') + end = s.index('-- Only the u8-to-bool', start) + before = s[start:end] + after = before.replace('else forbiddenExecution', 'else .ok dst', 1) +if before == after: + raise SystemExit('Storage boundary control no longer matches') +p.write_text(s[:start] + after + s[end:]) +PYCONTROL + check_model_mutant "permitted bad $mutation input" Zerocopy.FunsExternal + expect_failure "permitted bad $mutation input" storage-guard-audit.log audit + if ! grep -Eq 'Boolean conversion changed|byte copy changed' "$backup/storage-guard-audit.log"; then + cat "$backup/storage-guard-audit.log" >&2; exit 1 + fi + expect_failure "permitted bad $mutation input" storage-guard-proof.log \ + aeneas_lake env lean -DwarningAsError=true SafetyTests.lean + restore_build + done +fi + fi # unsafe if [[ $AENEAS_CONTROL_FAMILY == coverage ]]; then diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index f21d391a3a..0651aba92d 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -50,4 +50,22 @@ spec min_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.min_spec for Zerocopy.util.min with 2 +check_model_inputs Zerocopy.util.safety_checks.checked_bool with 0 type parameters +aeneas_spec_begin +spec checked_bool_spec + for @Zerocopy.util.safety_checks.checked_bool with 0 type parameters + ensures(raw) r => r = if byte.val < 2 then some (decide (byte.val = 1)) else none +aeneas_spec_end +check_spec_binding Zerocopy.Specs.checked_bool_spec for Zerocopy.util.safety_checks.checked_bool with 1 + +check_model_inputs Zerocopy.util.safety_checks.checked_copy with 0 type parameters +aeneas_spec_begin +spec checked_copy_spec + for @Zerocopy.util.safety_checks.checked_copy with 0 type parameters + ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then src.val ++ dst.val.drop src.val.length else dst.val +aeneas_spec_end +check_spec_binding Zerocopy.Specs.checked_copy_spec for Zerocopy.util.safety_checks.checked_copy with 2 + end Zerocopy.Specs diff --git a/verification/aeneas/tests/producer-controls.sh b/verification/aeneas/tests/producer-controls.sh new file mode 100755 index 0000000000..c1729890b6 --- /dev/null +++ b/verification/aeneas/tests/producer-controls.sh @@ -0,0 +1,106 @@ +#!/usr/bin/env bash +# 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. + +# Compile deliberately invalid producers; never execute their Rust code. +set -euo pipefail +case "${1:-}" in + generate) + [[ $# == 2 ]] || { echo "Usage: $0 generate FIXTURES" >&2; exit 1; } + mode=generate + mkdir -p "$2" + work=$(cd "$2" && pwd) + ;; + check) + [[ $# == 3 && -f "$2/bindings.json" && -d "$3/Controls" ]] || { + echo "Usage: $0 check VERIFIED_PROJECT FIXTURES" >&2; exit 1; + } + mode=check + project=$(cd "$2" && pwd) + work=$(cd "$3" && pwd) + ;; + *) + # Preserve the original standalone interface and its complete coverage. + [[ $# == 1 && -f "$1/bindings.json" ]] || { echo "Usage: $0 VERIFIED_PROJECT" >&2; exit 1; } + mode=both + project=$(cd "$1" && pwd) + work="$project/producer-controls" + ;; +esac +cd "$(dirname "$0")/../../.." +repo=$PWD +source verification/aeneas/toolchain.sh +tools_dir=${AENEAS_TOOLCHAIN_DIR:-"$repo/target/aeneas/toolchain"} +fixture="$repo/verification/aeneas/tests/producer-controls" +if [[ $mode != check ]]; then +mkdir -p "$work/Controls" +roots=aeneas_admission_controls::valid,aeneas_admission_controls::ignored,aeneas_admission_controls::before_divergence +boundary=aeneas_admission_controls::util::transmute_unchecked +# These are the same reviewed exclusions as the production extraction. The +# toy crate defines none of those methods, but admission checks the full profile. +excluded_args=() +while IFS= read -r method; do + [[ -z "$method" ]] || excluded_args+=(--exclude "$method") +done < <(python3 -B verification/aeneas/admission.py exclude) +( + cd "$fixture" + CHARON_ADMISSION_SNAPSHOT="$work/controls.before.ullbc" \ + CARGO_TARGET_DIR="$work/rust" \ + "$tools_dir/charon" cargo --preset=aeneas --sysroot default \ + --mir promoted --no-dedup-serialized-ast --opaque "$boundary" \ + "${excluded_args[@]}" \ + --start-from "$roots" --dest-file "$work/controls.llbc" \ + --abort-on-error --error-on-warnings -- --lib --locked --offline +) +# Exercise the same admission traversal, with the fixture's exact callable +# identity. This does not mint a production binding manifest or certify the +# toy helper body: its opaque interpretation is deliberately a test premise. +python3 - "$repo" "$work" "$roots" "$boundary" <<'PY' +import json, sys +from pathlib import Path +repo, work = map(Path, sys.argv[1:3]) +sys.path.insert(0, str(repo / 'verification/aeneas')) +import admission +registry = json.loads((repo / 'verification/aeneas/external.json').read_text()) +entry = next(row.copy() for row in registry if row['rust'] == 'zerocopy::util::transmute_unchecked') +entry['rust'] = sys.argv[4] +for filename, before in [('controls.before.ullbc', True), ('controls.llbc', False)]: + checker = admission.Admission(json.loads((work / filename).read_text()), [entry]) + if checker.before != before: + raise SystemExit('Producer control has the wrong inspection stage') + checker.audit(sys.argv[3].split(',')) +PY +"$tools_dir/aeneas" -backend lean -namespace Controls \ + -dest "$work/Controls" -split-files -abort-on-error \ + -warnings-as-errors -no-progress-bar -use-tuple-structs false "$work/controls.llbc" +cat > "$work/Controls/TypesExternal.lean" <<'LEAN' +module +public import Aeneas +LEAN +cat > "$work/Controls/FunsExternal.lean" <<'LEAN' +module +public import Controls.Types +public import Zerocopy.FunsExternal +LEAN +fi +if [[ $mode != generate ]]; then +mkdir -p "$project/.lake/build/lib/lean/Controls" +( + cd "$project" + # Compile every fixture module freshly. A cached caller from another model + # cannot make a missing or erased unsafe call look forbidden. + for name in TypesExternal Types FunsExternal Funs; do + aeneas_lake env lean --root="$work" -DwarningAsError=true \ + "$work/Controls/$name.lean" \ + -o "$project/.lake/build/lib/lean/Controls/$name.olean" + done + aeneas_lake env lean -DwarningAsError=true "$fixture/Check.lean" +) +echo 'Confirmed: generated callers retain forbidden production before discard and divergence' + +fi diff --git a/verification/aeneas/tests/producer-controls/Cargo.lock b/verification/aeneas/tests/producer-controls/Cargo.lock new file mode 100644 index 0000000000..3b37b58e9c --- /dev/null +++ b/verification/aeneas/tests/producer-controls/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "aeneas_admission_controls" +version = "0.0.0" diff --git a/verification/aeneas/tests/producer-controls/Cargo.toml b/verification/aeneas/tests/producer-controls/Cargo.toml new file mode 100644 index 0000000000..2d2a38298e --- /dev/null +++ b/verification/aeneas/tests/producer-controls/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "aeneas_admission_controls" +version = "0.0.0" +edition = "2021" +publish = false + +[workspace] diff --git a/verification/aeneas/tests/producer-controls/Check.lean b/verification/aeneas/tests/producer-controls/Check.lean new file mode 100644 index 0000000000..3e8a1fd7bc --- /dev/null +++ b/verification/aeneas/tests/producer-controls/Check.lean @@ -0,0 +1,29 @@ +/- 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. -/ + +import Controls.Funs +open Aeneas Aeneas.Std Controls + +-- Start with a successful generated call: a missing module, wrong namespace, +-- or broken interpretation cannot count as rejecting an invalid execution. +example : valid (1#u8) ⦃ out => out = some true ⦄ := by + simp [valid, util.transmute_unchecked, UScalar.val] + +-- These are real Aeneas-generated callers, not handwritten monadic witnesses. +-- The invalid call must survive filtering even when its result is unused. +example : ignored = Result.fail .undef := by + simp [ignored, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val] + +example : before_divergence false = Result.fail .undef := by + simp [before_divergence, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val] + +example : ¬ WP.spec ignored (fun _ => True) := by + simp [ignored, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val] + +example : ¬ WP.dspec (before_divergence false) (fun _ => True) := by + simp [before_divergence, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val] diff --git a/verification/aeneas/tests/producer-controls/src/lib.rs b/verification/aeneas/tests/producer-controls/src/lib.rs new file mode 100644 index 0000000000..2206dc748c --- /dev/null +++ b/verification/aeneas/tests/producer-controls/src/lib.rs @@ -0,0 +1,60 @@ +// 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. + +//! Extraction controls, never executed as Rust. +//! +//! The invalid producers intentionally violate Boolean bit validity. We prove +//! that their extracted executions are forbidden, rather than running Rust UB. +//! The helper is opaque, with the same u8-to-bool interpretation as production. +//! This fixture tests translation of calls, not certification of its union body. +#![allow(dead_code)] + +pub mod util { + use core::mem::ManuallyDrop; + + /// The caller must supply a bit-valid representation of `Dst` with equal + /// size. Only `u8` to `bool` is selected in these extraction controls. + pub const unsafe fn transmute_unchecked(src: Src) -> Dst { + union Bits { + src: ManuallyDrop, + dst: ManuallyDrop, + } + // SAFETY: This requires the documented caller obligations. The bad + // fixtures below deliberately violate them and must never be executed. + ManuallyDrop::into_inner(unsafe { Bits { src: ManuallyDrop::new(src) }.dst }) + } +} + +pub fn valid(byte: u8) -> Option { + if byte < 2 { + // SAFETY: Both one-byte types have equal size; 0 and 1 are valid bools. + Some(unsafe { util::transmute_unchecked(byte) }) + } else { + None + } +} + +/// No call to this extraction fixture is permitted. +pub unsafe fn ignored() { + // Deliberate UB for a negative control. Do not execute this Rust function. + let _ = unsafe { util::transmute_unchecked::(2u8) }; +} + +/// No call to this extraction fixture is permitted, including when its caller +/// would accept divergence. UB happens before the loop begins. +pub unsafe fn before_divergence(escape: bool) { + // Deliberate UB for a negative control. Do not execute this Rust function. + let _ = unsafe { util::transmute_unchecked::(2u8) }; + // Keep a syntactic exit: the pinned extractor rejects loops with no break. + // The Lean control chooses false, so an accepted execution could not exit. + loop { + if escape { + break; + } + } +} diff --git a/verification/aeneas/tests/test_control_runner.py b/verification/aeneas/tests/test_control_runner.py index 13e9b360ea..b1b8e92be8 100644 --- a/verification/aeneas/tests/test_control_runner.py +++ b/verification/aeneas/tests/test_control_runner.py @@ -268,6 +268,54 @@ def test_suite_interruption_during_baseline_stops_descendants_and_keeps_roster(s process.kill() process.wait() + def test_shared_producer_fixtures_are_recompiled_against_each_model(self): + lake = shutil.which('lake') + if lake is None: + self.skipTest('Requires the pinned Lean installation') + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + scripts = root / 'verification/aeneas/tests' + scripts.mkdir(parents=True) + shutil.copyfile(AENEAS / 'tests/producer-controls.sh', scripts / 'producer-controls.sh') + (scripts / 'producer-controls').mkdir() + (scripts / 'producer-controls/Check.lean').write_text( + 'import Controls.Funs\nexample : translated = 0 := rfl\n') + (root / 'verification/aeneas/toolchain.sh').write_text( + 'AENEAS_TOOLCHAIN_DIR=/unused-for-replay\naeneas_lake() ( unset CI; command lake --old "$@"; )\n') + shared = root / 'shared' + (shared / 'Controls').mkdir(parents=True) + for name, text in { + 'TypesExternal': 'module\n', + 'Types': 'module\npublic import Controls.TypesExternal\n', + 'FunsExternal': 'module\npublic import Controls.Types\npublic import Zerocopy.FunsExternal\n', + 'Funs': 'module\npublic import Controls.FunsExternal\n@[expose] public section\ndef translated : Nat := modelValue\n', + }.items(): + (shared / 'Controls' / (name + '.lean')).write_text(text) + original = {p.name: p.read_bytes() for p in (shared / 'Controls').iterdir()} + env = dict(os.environ) + env.pop('CI', None) + for model, value in [('golden', 0), ('live', 0), ('changed-live', 1)]: + project = root / model + (project / 'Zerocopy').mkdir(parents=True) + (project / 'lean-toolchain').write_bytes((AENEAS.parents[1] / 'anneal/lean/lean-toolchain').read_bytes()) + (project / 'bindings.json').write_text('{}') + (project / 'lakefile.lean').write_text( + 'import Lake\nopen Lake DSL\npackage producerReplay\nlean_lib Zerocopy\n') + (project / 'Zerocopy/FunsExternal.lean').write_text(f'module\n@[expose] public section\ndef modelValue : Nat := {value}\n') + built = subprocess.run([lake, '--old', 'build', '+Zerocopy.FunsExternal'], + cwd=project, env=env, capture_output=True) + self.assertEqual(built.returncode, 0, built.stdout + built.stderr) + replay = subprocess.run(['bash', str(scripts / 'producer-controls.sh'), + 'check', str(project), str(shared)], env=env, capture_output=True) + if value == 0: + self.assertEqual(replay.returncode, 0, replay.stdout + replay.stderr) + for module in ('TypesExternal', 'Types', 'FunsExternal', 'Funs'): + self.assertTrue((project / '.lake/build/lib/lean/Controls' / (module + '.olean')).exists()) + else: + self.assertNotEqual(replay.returncode, 0) + self.assertIn(b'Check.lean', replay.stdout + replay.stderr) + self.assertEqual({p.name: p.read_bytes() for p in (shared / 'Controls').iterdir()}, original) + def test_ci_preflight_accepts_native_trait_laws_and_rejects_projection_edits(self): sys.path.insert(0, str(AENEAS)) with tempfile.TemporaryDirectory() as temporary: diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py index 927b1ef31e..8390f37afd 100644 --- a/verification/aeneas/tests/test_inline.py +++ b/verification/aeneas/tests/test_inline.py @@ -194,6 +194,15 @@ def test_inherent_and_generic_ownership_automatically_introduces_rust_names(self with self.assertRaises(ValueError): self.parse('impl S { ' + BLOCK + 'fn f(&mut self, x: usize) {} }') + def test_only_explicit_mutable_byte_slice_inputs_are_supported(self): + found = self.parse(BLOCK + 'fn f(x: &mut [u8]) {}')[0] + self.assertEqual(found['inputs'], ['x']) + for signature in ('fn f(x: &mut [u16]) {}', 'fn f(x: &mut bool) {}', + 'fn f(x: Option<&mut [u8]>) {}', + 'fn f(x: &mut [u8]) -> &mut [u8] { x }'): + with self.subTest(signature=signature), self.assertRaises(ValueError): + self.parse(BLOCK + signature) + def test_ghosts_and_requirements_cannot_shadow_original_parameters(self): for header in ('(x : Nat)', '(T : Type)', '(ghost ghost : Nat)'): block = BLOCK.replace('spec f_spec', 'spec f_spec ' + header) diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index a09045dccd..8235c0f3d1 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -14,6 +14,8 @@ pub(crate) mod macros; #[doc(hidden)] pub mod macro_util; +mod safety_checks; + use core::{ marker::PhantomData, mem::{self, ManuallyDrop}, diff --git a/zerocopy/src/util/safety_checks/mod.rs b/zerocopy/src/util/safety_checks/mod.rs new file mode 100644 index 0000000000..29bde56082 --- /dev/null +++ b/zerocopy/src/util/safety_checks/mod.rs @@ -0,0 +1,96 @@ +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// Copyright 2026 The Fuchsia Authors +// +// Licensed under the 2-Clause BSD 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. + +//! Small callers of the trusted storage boundaries. +//! +//! The proofs check the callers' guards and results. The interpretations of +//! `transmute_unchecked::` and `copy_unchecked` remain explicit trusted +//! premises; these harnesses do not prove the union or raw-pointer operations +//! inside those helpers. Both boundaries reject forbidden execution before +//! producing a typed value, even when that value is subsequently discarded. + +#![allow(dead_code)] + +/// Converts precisely the two valid boolean encodings. +/// +/// ```aeneas +/// spec checked_bool_spec +/// ensures(raw) r => r = if byte.val < 2 then some (decide (byte.val = 1)) else none +/// ``` +fn checked_bool(byte: u8) -> Option { + if byte < 2 { + // SAFETY: The branch restricts `byte` to 0 or 1, the two boolean bit + // patterns. Both types have size one, satisfying the helper's size + // assertion. The trusted interpretation checks this same condition + // before producing a bool; it cannot silently accept another byte. + Some(unsafe { super::transmute_unchecked(byte) }) + } else { + None + } +} + +/// Copies a fitting prefix; failure leaves the destination unchanged. +/// +/// The returned state in the extracted model includes the updated destination. +/// Its suffix must be preserved, including when the source is empty. +/// +/// ```aeneas +/// spec checked_copy_spec +/// ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ +/// out.2.val = if src.val.length ≤ dst.val.length +/// then src.val ++ dst.val.drop src.val.length else dst.val +/// ``` +fn checked_copy(src: &[u8], dst: &mut [u8]) -> bool { + if src.len() <= dst.len() { + // SAFETY: This branch establishes the helper's sole additional + // requirement, `src.len() <= dst.len()`. The valid input references + // supply initialized source bytes and an exclusive destination. + unsafe { super::copy_unchecked(src, dst) }; + true + } else { + false + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn all_boolean_bytes() { + for byte in 0..=u8::MAX { + assert_eq!( + checked_bool(byte), + match byte { + 0 => Some(false), + 1 => Some(true), + _ => None, + } + ); + } + } + + #[test] + fn copy_boundaries() { + for len in 0..=4 { + let mut dst = [9; 3]; + let src = &[1, 2, 3, 4][..len]; + let fits = checked_copy(src, &mut dst); + assert_eq!(fits, len <= dst.len()); + if fits { + assert_eq!(&dst[..len], src); + assert!(dst[len..].iter().all(|byte| *byte == 9)); + } else { + assert_eq!(dst, [9; 3]); + } + } + } +}