diff --git a/verification/aeneas/ADMISSION_DESIGN.md b/verification/aeneas/ADMISSION_DESIGN.md index bb01b1d5df..1d5a4d6f05 100644 --- a/verification/aeneas/ADMISSION_DESIGN.md +++ b/verification/aeneas/ADMISSION_DESIGN.md @@ -21,8 +21,8 @@ patch saves its imported unstructured AST *before any Charon transformations*. `admission.py` inspects that snapshot and final LLBC. It follows every function binding and executable dependency, including original unwind and dead blocks. A stock driver cannot silently skip the check: the missing snapshot rejects the -run. Drop terminators are rejected before drop elaboration or cleanup can erase -them. During admission, the driver refuses to fall back to optimized MIR for +run. Before drop elaboration or cleanup can erase a drop, admission either +proves that it cannot execute a destructor or rejects it. During admission, the driver refuses to fall back to optimized MIR for local bodies if their requested MIR was stolen. We deliberately use promoted MIR rather than drop-elaborated MIR; no supported execution relies on a destructor's effects. @@ -30,8 +30,8 @@ effects. The allowed operations are logical integers, booleans, field records, ordinary arrays/slices, supported borrows, checked indexing/arithmetic, branching, and loops. Unknown AST constructors and extraction options reject the run. Escaping -borrows, callbacks, raw pointers, foreign ABIs, statics, assembly, drops, union -storage, and general memory observations remain unsupported. Valid incoming +borrows, callbacks, raw pointers, foreign ABIs, statics, assembly, executable +destruction, union storage, and general memory observations remain unsupported. Valid incoming references and Aeneas's reviewed borrow translation are explicit premises. `external.json` supplies exact reviewed leaves, including standard-library @@ -419,6 +419,61 @@ The mathematical `RustModel` dictionaries are interpretations of values. They are not contracts for arbitrary Rust trait methods and do not establish that a Rust type has no destructor. Keep these two uses of dictionaries distinct. +## Conditional drops of empty whole locals + +A move transfers a destruction obligation; it does not promise that the old +storage has been cleared. Early MIR can therefore retain a conditional drop of +a local after its value has moved elsewhere. Ignoring that drop is justified +only if the local cannot still carry a destruction obligation. This rule makes +no assumption about whether the local's type implements `Drop`. + +`DropOwnership.lean` checks a finite control-flow graph. Every entry, including +entries of disconnected components, starts with every local possibly owning an +obligation. A whole-local move removes that local's obligation. A definition, +assignment destination, call destination, or storage marker restores uncertainty. +Right-hand-side effects precede the destination definition. A call defines its +destination on both normal and unwind successors, conservatively. Joins take +the union of incoming possibilities. A conditional drop is accepted only when +its local is absent from that union. The theorem `accepted_drop_empty` proves +this property for every concrete ownership execution covered by the graph. +`accepted_drop_noop` then states the explicit semantic bridge: if dropping an +obligation-free slot is silent, the admitted drop is a no-op. + +`DropJson.lean` reads the complete tagged compiler body, including its local +inventory, all blocks, unwind edges, and disconnected code. It constructs the +graph in Lean, with strict checks on executable JSON fields and constructors. +It rejects a candidate slot if it is borrowed, projected, or exposed indirectly. +Only whole-local conditional drops are candidates. Topological ordering must +cover every node; any cycle rejects this exemption. This restriction applies +only to bodies requesting a drop exemption: existing drop-free loops retain +their existing admission rules. Structured switches and escaping aliases also +remain outside this first decoder. + +`DropAudit.lean` quotes the actual body from a frozen compiler snapshot and +asks Lean's kernel to establish `DropJson.acceptBody body = true` by reduction. +Python does not supply an event list or an ownership verdict. Both the original +ULLBC and final LLBC must obtain their own proofs; local numbers need not agree +between stages. A hash binds each proof record to the inspected body and exact +snapshot bytes. The final verification command repeats the entire admission +traversal and obtains fresh kernel proofs before compiling either the golden +or live model. Missing, additional, duplicated, or stale records reject the run. +A previously successful compiled witness never authorizes a later check. + +The formal theorem concerns ownership graphs. Relating the strict JSON decoder +to Charon's documented execution order and relating empty conditional drops to +Rust remain reviewed compiler correspondence premises. This work does not +prove rustc, Charon, general drop glue, partial initialization, destructor +execution, or arbitrary typed-storage semantics. Unknown operations still +reject admission independently of the ownership proof. + +`DropOwnershipTests.lean` checks ownership boundary cases; +`DropJsonTests.lean` checks raw compiler-schema mutations. Python tests exercise +the actual snapshot-to-kernel command and reject a move changed to a copy, +forged identities, unknown executable fields, and missing evidence. The Rust +`util::move_checks` fixture moves an unrestricted generic value through a call. +Its value contract is checked against both models, while a native test confirms +that a destructor stays attached to the returned value. + ## Operation rules for the first supported subset Start with deterministic integer and initialized-byte computations, ordinary @@ -431,7 +486,7 @@ rules are release conditions, not exemptions that are already implemented. | Copy, move, assignment, arguments, and returns | Interpret logical values only when the state relation justifies erasing physical transfer effects. Exact general typed storage is excluded. | | Creation of values from storage or unchecked construction | Require a guarded producer interpretation before the typed carrier is entered. Invalid production remains forbidden even if its value is unused. | | `PlaceMention` and projected place formation | Reject unless a reviewed rule proves the projections valid in related states. A count of reference/field projections or absence of raw pointers is insufficient. | -| Residual `Drop`, including conditional and unwind drops | Reject initially. `-eval-drops` does not execute the destructor. Enabling it is not admission. | +| Residual `Drop`, including conditional and unwind drops | Require the whole-body empty-slot proof below for conditional drops; reject every other drop. `-eval-drops` does not execute the destructor. | | `#[target_feature]`, dispatch variants, unsupported ABIs | Reject initially. Later support must require the real platform/ABI conditions at the call boundary. | | Raw pointers, unions, raw-memory constants, transmutation, FFI, assembly | Reject unless a specifically admitted primitive completely interprets the operation; no generic successful placeholder. | | Allocation, allocator parameters, interior mutation, atomics, concurrency | Exclude initially; logical return values alone do not describe their effects. | @@ -448,7 +503,8 @@ Charon removes some proven-trivial drops. That removal is part of the reviewed normalization premise. Do not infer that every generic or opaque type has a trivial destructor just because no destructor body was imported. A future drop implementation must extract precise drop glue, inspect its callees and unwind -paths, and preserve conditional/uninitialized/packed-place semantics. +paths, and preserve conditional/uninitialized/packed-place semantics. The +empty-slot rule below does not implement destruction. The source state relation must justify ordinary reference dereferences, reborrows, retagging, and field projections. For the restricted safe-borrow @@ -476,7 +532,8 @@ admit a simple exceptional suffix only when it is entered exclusively after an already-modeled failure, cannot reenter normal execution, and contains no unclassified effects. Existing proofs exclude that failure on admitted inputs. `UnwindResume` in such a suffix is not the same as permitting it on a normal -execution path. Residual destruction remains rejected there as elsewhere. +execution path. Destruction remains rejected there as elsewhere; only proven +empty conditional drops may be ignored. If the rule cannot establish the connection to modeled failure, reject it. An external interpretation cannot return `.div` as a placeholder for unsupported diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 59c094fcce..adae7cf864 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -90,8 +90,11 @@ each tool answers a different question: Before Aeneas runs, `admission.py` follows every executable dependency from every discovered specification in two snapshots: original promoted MIR as imported by Charon, and final LLBC. Annotation status never exempts a callee. - Unsupported drops, raw pointers, arbitrary indirect calls, foreign code, - and unknown effects reject extraction. Calls through original trait + Conditional drops require a kernel-checked empty-slot proof in each + snapshot; other drops reject extraction. The narrow rule and its compiler + premises are documented in [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md#conditional-drops-of-empty-whole-locals). + Raw pointers, arbitrary indirect calls, foreign code, and unknown effects + also reject extraction. Calls through original trait dictionaries are admitted only through the checked trait-law boundary described below. This prevents an operation from being accepted simply because a later lowering forgets it. The small Charon snapshot patch diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md index 98dafb6fef..3f0b3863de 100644 --- a/verification/aeneas/SEMANTICS.md +++ b/verification/aeneas/SEMANTICS.md @@ -176,7 +176,11 @@ cannot reveal an operation erased before that model was produced. [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) describes the implemented restricted value-and-borrow fragment. CI checks a preserved promoted-MIR import before Charon's transformations, final LLBC, and the complete executable dependency -closure. Unsupported operations and unregistered opaque calls reject the run. +closure. A retained conditional drop requires a kernel-checked proof that its +whole local has no destruction obligation, independently for both compiler +snapshots. Other drops, unsupported operations, and unregistered opaque calls +reject the run. The ownership proof does not certify compiler translation or +execute destructor bodies. Admission is tied to the compiler inputs and the patched runtime; it is not a formal certificate of rustc or Aeneas correctness. Valid incoming references, reviewed builtin lowering, and registered external interpretations remain diff --git a/verification/aeneas/admission.py b/verification/aeneas/admission.py index 3f2ca10517..46f104e8a9 100644 --- a/verification/aeneas/admission.py +++ b/verification/aeneas/admission.py @@ -16,8 +16,9 @@ are exact registered leaves with guards, rather than unchecked carrier casts. The traversal starts at every bound specification. Annotation status never -exempts a callee. Unknown constructors, indirect calls, drops, and raw storage -observations fail closed. The report identifies the inspected LLBC and selected +exempts a callee. Unknown constructors, indirect calls, executable destruction, +and raw storage observations fail closed. Only a kernel-checked empty-slot +proof permits ignoring a conditional drop. The report identifies the inspected LLBC and selected interpretations; it is evidence of this inspection, not a proof of rustc. """ @@ -29,6 +30,7 @@ from pathlib import Path import source_inventory +import drop_ownership # These provided methods require memory or I/O semantics outside our admitted @@ -118,7 +120,7 @@ def fields(value, expected): class Admission: - def __init__(self, data, registry, law_traits=()): + def __init__(self, data, registry, law_traits=(), *, certify_drops=None): if data.get('has_errors') is not False or data.get('charon_version') != '0.1.276': raise ValueError('Admission requires successful LLBC from the reviewed Charon schema') self.crate = data['translated'] @@ -133,6 +135,8 @@ def __init__(self, data, registry, law_traits=()): self.law_traits = set(law_traits) self.locals = {} self.checked_types = set() + self.certify_drops = certify_drops + self.empty_drops = {} options = self.crate['options'] targets = self.crate['target_information'] if (len(targets) != 1 or targets[0]['value']['target_pointer_size'] != 8 or @@ -373,6 +377,17 @@ def visit(self, index): if local['drop_flag_for'] is not None: raise ValueError(f'Conditional drop flag in {name}') try: + if drop_ownership.contains_drop(function['body']): + # A failed or absent kernel check must leave the old rejection + # intact. This checks the complete body, including cleanup and + # disconnected blocks, before any Drop receives an exemption. + if self.certify_drops is None: + raise ValueError('Drop requires a kernel-checked compiler body') + proof = self.certify_drops(function) + if (proof.get('function_def_id') != index or + proof.get('body_sha256') != drop_ownership.body_digest(function['body'])): + raise ValueError('Drop proof does not identify this exact compiler body') + self.empty_drops[index] = proof if stage == 'Structured': self.block(body['body']) else: @@ -429,10 +444,13 @@ def assertion(self, assertion): def abort(self, abort): tag, _ = variant(abort) - # The pinned interpreter collapses source UB aborts into panic. Both - # remain rejected by every admitted contract. No recovery or failure + # The pinned interpreter maps every Abort (including UB and unwind + # termination) to panic: InterpStatements.ml's `Abort _` case. All + # remain rejected by every admitted contract, even on a normal path. + # ContractTests checks total/partial rejection with postcondition True. + # No recovery or failure # handler is admitted; adding one requires preserving this distinction. - if tag not in {'Panic', 'UndefinedBehavior'}: + if tag not in {'Panic', 'UndefinedBehavior', 'UnwindTerminate'}: raise ValueError(f'Unreviewed abort {tag}') def place(self, place, indexed=False): @@ -807,7 +825,10 @@ def block(self, block, unwind=False): for statement in block['statements']: fields(statement, 'span id kind comments_before') tag, body = variant(statement['kind']) - if unwind and tag not in {'StorageDead', 'UnwindResume', 'Abort', 'Nop'}: + certified = (self.current_function is not None and + self.current_function.get('def_id') in self.empty_drops) + if unwind and tag not in {'StorageDead', 'UnwindResume', 'Abort', 'Nop'} and not ( + tag == 'Drop' and certified): raise ValueError(f'Unclassified unwind effect {tag}') if tag in {'StorageLive', 'StorageDead', 'Nop', 'Return', 'Break', 'Continue'}: continue @@ -818,6 +839,16 @@ def block(self, block, unwind=False): self.place(body[0]); self.rvalue(body[1]) elif tag == 'PlaceMention': self.place(body) + elif tag == 'Drop': + fields(body, 'place fn_ptr kind on_unwind') + if (not certified or body['kind'] != 'Conditional' or + variant(body['place']['kind'])[0] != 'Local'): + raise ValueError('Only kernel-checked empty conditional Drop is supported') + self.place(body['place']) + # The proof makes this glue call unreachable. Its cleanup is + # still structurally audited; it is not an execution exemption + # for other unsupported operations hidden in an unwind block. + self.block(body['on_unwind'], True) elif tag == 'Borrowck': kind, place = variant(body) if kind != 'FakeRead': @@ -939,6 +970,10 @@ def cfg(self, blocks): fields(body, 'call target on_unwind') body = {'call': body['call'], 'on_unwind': {'span': term['span'], 'id': 0, 'statements': []}} + elif tag == 'Drop': + fields(body, 'kind place fn_ptr target on_unwind') + body = {key: body[key] for key in ('kind', 'place', 'fn_ptr')} + body['on_unwind'] = {'span': term['span'], 'id': 0, 'statements': []} elif tag == 'Assert': fields(body, 'assert target on_unwind') self.assertion(body['assert']) @@ -985,7 +1020,7 @@ def audit(self, roots): continue self.audit_implementation(implementation, trait) return {'roots': sorted(roots), 'executions': list(self.visited.values()), - 'calls': self.calls} + 'calls': self.calls, 'empty_drops': list(self.empty_drops.values())} def input_identity(root): @@ -1045,19 +1080,71 @@ def input_identity(root): 'runtime': digest(tools / 'aeneas-build.json')} -def inspect(root, work, roots, sources, body_digests=None, law_traits=()): +def inspect_stages(root, work, roots, law_traits): + """Audit both complete snapshots, obtaining new drop proofs each time.""" + roots = sorted(roots) registry_path = root / 'verification/aeneas/external.json' registry = json.loads(registry_path.read_text()) reports = {} + drops = drop_ownership.KernelDrops(root, work) for stage, filename in [('before', 'zerocopy.before.ullbc'), ('llbc', 'zerocopy.llbc')]: path = work / filename if not path.is_file(): raise ValueError(f'Missing mandatory {stage} admission snapshot: {path}') - checked = Admission(json.loads(path.read_text()), registry, law_traits) + contents = path.read_bytes() + drops.freeze(stage, contents) + checked = Admission(json.loads(contents), registry, law_traits, + certify_drops=lambda function, stage=stage: drops.certify(stage, function)) if checked.before != (stage == 'before'): raise ValueError(f'Wrong AST stage for mandatory {stage} snapshot') reports[stage] = checked.audit(roots) - reports[stage]['sha256'] = digest(path) + reports[stage]['sha256'] = hashlib.sha256(contents).hexdigest() + if digest(path) != reports[stage]['sha256']: + raise ValueError('Compiler snapshot changed during execution admission') + return reports + + +def recheck(root, work, manifest): + """Replay admission before checking either model's final proofs. + + The saved report describes what must be checked; it cannot authorize an + erased effect by itself. In particular, rerun the kernel on the snapshots + even when an earlier phase recorded a successful empty-drop proof. Proof + artifacts may have different hashes in a fresh build, so compare their + source identities rather than treating an old compiled witness as authority. + """ + roots = sorted(name for name, binding in manifest['bindings'].items() + if binding['kind'] == 'function') + saved = manifest['admission']['stages'] + for stage, filename in [('before', 'zerocopy.before.ullbc'), ('llbc', 'zerocopy.llbc')]: + if digest(work / filename) != saved[stage].get('sha256'): + raise ValueError(f'Stale {stage} admission snapshot; run fresh extraction') + actual = inspect_stages(root, work, roots, + [law['rust'] for law in manifest.get('trait_laws', [])]) + + def source_records(report): + # Deliberately require the key even when there are no candidates. A + # missing list is not an alternative spelling of successful admission. + try: + records = report['empty_drops'] + if not isinstance(records, list): + raise ValueError('Invalid empty-drop proof records') + normalized = [{key: row[key] for key in + ('function_def_id', 'body_sha256', 'snapshot_sha256')} + for row in records] + return dict(report, empty_drops=normalized) + except (KeyError, TypeError) as error: + raise ValueError('Missing or invalid empty-drop proof records') from error + + for stage in actual: + if source_records(saved[stage]) != source_records(actual[stage]): + raise ValueError(f'Stale or incomplete {stage} admission evidence; run fresh extraction') + + +def inspect(root, work, roots, sources, body_digests=None, law_traits=()): + registry_path = root / 'verification/aeneas/external.json' + registry = json.loads(registry_path.read_text()) + reports = inspect_stages(root, work, roots, law_traits) for entry in registry: if entry.get('opaque') and any(row['rust'] == entry['rust'] for row in reports['llbc']['executions']): diff --git a/verification/aeneas/drop_ownership.py b/verification/aeneas/drop_ownership.py new file mode 100644 index 0000000000..e2df08d725 --- /dev/null +++ b/verification/aeneas/drop_ownership.py @@ -0,0 +1,125 @@ +# 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. + +"""Require a fresh kernel proof before ignoring an empty conditional drop. + +This driver never calculates ownership events. Lean reads the complete frozen +compiler snapshot and checks its own strict projection and ownership analysis. +The driver binds that proof to the exact body the admission traversal visits. +""" + +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import tempfile + +import toolchain + + +def body_digest(body): + return hashlib.sha256(json.dumps(body, sort_keys=True).encode()).hexdigest() + + +def contains_drop(value): + """Find candidates, without using this search to decide their safety. + + Searching every nested node includes unwind paths. The existing syntax + audit still rejects unknown executable constructs independently of Lean. + """ + if isinstance(value, dict): + return 'Drop' in value or any(contains_drop(v) for v in value.values()) + if isinstance(value, list): + return any(contains_drop(v) for v in value) + return False + + +class KernelDrops: + """One fresh checker build, shared by this inspection's two snapshots.""" + + MODULES = ('DropOwnership', 'DropJson', 'DropAudit') + + def __init__(self, root, work): + self.root = root.resolve() + self.parent = work.resolve() + self.work = None + self.snapshots = {} + self.proofs = {} + + def freeze(self, stage, contents): + # This is the exact buffer parsed by Admission, not a second file read. + self.snapshots[stage] = contents + + def initialize(self): + if self.work is not None: + return + tools = Path(os.environ.get('AENEAS_TOOLCHAIN_DIR', + self.root / 'target/aeneas/toolchain')).resolve() + metadata, _ = toolchain.validate(self.root, tools) + self.work = Path(tempfile.mkdtemp(prefix='empty-drops-', dir=self.parent)) + self.lean = tools / 'lean/bin/lean' + self.env = toolchain.runtime_env(tools) + # Do not inherit another project's modules or accept stale witnesses. + self.env['LEAN_PATH'] = str(self.work) + self.metadata = metadata + for module in self.MODULES: + shutil.copyfile(self.root / 'verification/aeneas/lean' / (module + '.lean'), + self.work / (module + '.lean')) + self.run(module) + + def run(self, module, env=None): + command = [str(self.lean), '-o', module + '.olean', module + '.lean'] + log = self.work / (module + '.log') + with log.open('w') as output: + result = subprocess.run(command, cwd=self.work, env=env or self.env, + stdout=output, stderr=subprocess.STDOUT) + if result.returncode: + raise ValueError(f'Kernel rejected empty-drop admission; see {log}:\n' + + log.read_text()[-6000:]) + + def certify(self, stage, function): + self.initialize() + index = function['def_id'] + if type(index) is not int or index < 0: + raise ValueError('Drop admission requires a native function index') + contents = self.snapshots[stage] + data = json.loads(contents) + matches = [f for f in data['translated']['fun_decls'] + if f and f.get('def_id') == index] + if len(matches) != 1 or matches[0]['body'] != function['body']: + raise ValueError('Drop proof input differs from the inspected compiler body') + snapshot = self.work / (stage + '.json') + if snapshot.exists(): + if snapshot.read_bytes() != contents: + raise ValueError('Frozen drop-admission snapshot changed') + else: + snapshot.write_bytes(contents) + module = f'DropWitness_{stage}_{index}' + witness = self.work / (module + '.lean') + source = ( + 'import DropAudit\n' + 'set_option maxRecDepth 100000\n' + 'set_option maxHeartbeats 20000000\n' + f'certify_empty_drops {index}\n') + witness.write_text(source) + env = dict(self.env, AENEAS_DROP_SNAPSHOT=str(snapshot)) + self.run(module, env) + # An editor must not repair a temporary proof input while Lean runs + # and leave a certificate attributed to the original compiler body. + if snapshot.read_bytes() != contents or witness.read_text() != source: + raise ValueError('Drop proof inputs changed during kernel checking') + record = {'function_def_id': index, + 'body_sha256': body_digest(function['body']), + 'snapshot_sha256': hashlib.sha256(contents).hexdigest(), + 'proof_module': module, + 'proof_sha256': hashlib.sha256( + (self.work / (module + '.olean')).read_bytes()).hexdigest()} + self.proofs[stage, index] = record + return record diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index f24c23bc95..221b1ee780 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -651,7 +651,7 @@ def byteorder.verification.set_u32_be byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: - Source: 'src/util/mod.rs', lines 268:0-286:1 -/ + Source: 'src/util/mod.rs', lines 269:0-287:1 -/ def util.round_down_to_next_multiple_of_alignment (n : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -752,7 +752,7 @@ def layout.TrailingSliceLayoutUsize.advance { self with elem_size, size_base, size_rounding_align_and_phase := raap }) /-- [zerocopy::util::padding_needed_for]: - Source: 'src/util/mod.rs', lines 176:0-236:1 -/ + Source: 'src/util/mod.rs', lines 177:0-237:1 -/ def util.padding_needed_for (len : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -1684,7 +1684,7 @@ def layout.composition_checks.reference_constructor else ok none /-- [zerocopy::util::min]: - Source: 'src/util/mod.rs', lines 312:0-318:1 -/ + Source: 'src/util/mod.rs', lines 313:0-319:1 -/ def util.min (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) @@ -1704,7 +1704,7 @@ def util.min else ok a /-- [zerocopy::util::max]: - Source: 'src/util/mod.rs', lines 296:0-302:1 -/ + Source: 'src/util/mod.rs', lines 297:0-303:1 -/ def util.max (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) @@ -5033,6 +5033,16 @@ def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst : IntoBytesInst } +/-- [zerocopy::util::move_checks::forward]: + Source: 'src/util/move_checks/mod.rs', lines 28:0-30:1 -/ +def util.move_checks.forward {T : Type} (value : T) : Result T := do + ok value + +/-- [zerocopy::util::move_checks::move_through_call]: + Source: 'src/util/move_checks/mod.rs', lines 24:0-26:1 -/ +def util.move_checks.move_through_call {T : Type} (value : T) : Result T := do + util.move_checks.forward value + /-- [zerocopy::util::owned_transmute::to_bytes_native]: Source: 'src/util/owned_transmute.rs', lines 30:0-34:1 -/ def util.owned_transmute.to_bytes_native diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index 44e138f28f..4dd18d1124 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -116,12 +116,12 @@ axiom core.num.Usize.unchecked_mul : Std.Usize → Std.Usize → Result Std.Usize /-- [zerocopy::util::copy_unchecked]: - Source: 'src/util/mod.rs', lines 330:0-345:1 -/ + Source: 'src/util/mod.rs', lines 331:0-346:1 -/ axiom util.copy_unchecked : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8) /-- [zerocopy::util::copy_unchecked_at]: - Source: 'src/util/mod.rs', lines 359:0-370:1 -/ + Source: 'src/util/mod.rs', lines 360:0-371:1 -/ axiom util.copy_unchecked_at : Slice Std.U8 → Slice Std.U8 → Std.Usize → Result (Slice Std.U8) @@ -182,7 +182,7 @@ axiom Array.Insts.ZerocopyTryFromBytes.is_safe Bool /-- [zerocopy::util::transmute_unchecked]: - Source: 'src/util/mod.rs', lines 382:0-411:1 -/ + Source: 'src/util/mod.rs', lines 383:0-412:1 -/ axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst /-- [zerocopy::util::validity::read_byte]: diff --git a/verification/aeneas/lean/DropAudit.lean b/verification/aeneas/lean/DropAudit.lean new file mode 100644 index 0000000000..c06faefa61 --- /dev/null +++ b/verification/aeneas/lean/DropAudit.lean @@ -0,0 +1,79 @@ +/- 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 DropJson +public meta import Lean +public section + +/-! +Read the compiler's complete snapshot, rather than a caller-supplied list of +ownership events. The command selects exactly one native function, quotes its +entire body as data, and asks the kernel to check that the pure decoder and +ownership checker accept it. The metaprogram supplies only data and reflexivity; +it cannot substitute a successful native computation for a proof. + +The Python driver freezes the bytes it inspected into a fresh proof directory. +Its report binds that snapshot to the original compiler input. This command +does not claim that JSON import proves the correctness of rustc or Charon. +-/ + +open Lean Meta Elab Command + +namespace AeneasSpecs.DropAudit + +private meta partial def quoteJson (value : Json) : MetaM Expr := do + match value with + | .null => return mkConst ``Json.null + | .bool value => return mkApp (mkConst ``Json.bool) (toExpr value) + | .num value => + let number := mkApp2 (mkConst ``JsonNumber.mk) + (toExpr value.mantissa) (toExpr value.exponent) + return mkApp (mkConst ``Json.num) number + | .str value => return mkApp (mkConst ``Json.str) (toExpr value) + | .arr values => + return mkApp (mkConst ``Json.arr) + (← mkArrayLit (mkConst ``Json) (← values.mapM quoteJson).toList) + | .obj fields => + let pairs ← fields.toArray.mapM fun (key, value) => do + mkAppM ``Prod.mk #[toExpr key, ← quoteJson value] + let pairType := mkApp2 (mkConst ``Prod [.zero, .zero]) + (mkConst ``String) (mkConst ``Json) + return mkApp (mkConst ``Json.mkObj) (← mkListLit pairType pairs.toList) + +/-- Emit a kernel-checked acceptance theorem for one exact compiler body. -/ +elab "certify_empty_drops " index:num : command => do + let some source ← IO.getEnv "AENEAS_DROP_SNAPSHOT" + | throwError "Missing frozen compiler snapshot for drop admission" + let .ok snapshot := Json.parse (← IO.FS.readFile source) + | throwError "Malformed compiler snapshot for drop admission" + unless (snapshot.getObjValAs? Bool "has_errors").toOption == some false do + throwError "Drop admission requires a successful compiler snapshot" + let .ok translated := snapshot.getObjVal? "translated" + | throwError "Missing translated compiler crate" + let .ok functions := translated.getObjValAs? (Array Json) "fun_decls" + | throwError "Missing native function inventory" + let functionId := index.getNat + let selected := functions.filter fun function => + (function.getObjValAs? Nat "def_id").toOption == some functionId + unless selected.size == 1 do + throwError "Missing or ambiguous native function {functionId}" + let .ok body := selected[0]!.getObjVal? "body" + | throwError "Native function {functionId} has no body" + let bodyExpr ← liftTermElabM <| quoteJson body + let proposition ← liftTermElabM <| mkEq + (mkApp (mkConst ``DropJson.acceptBody) bodyExpr) (toExpr true) + -- The kernel must reduce acceptBody on the actual quoted body to true. + -- No native_decide, axiom, or computed Boolean is used as a proof premise. + let proof ← liftTermElabM <| mkEqRefl (toExpr true) + let theoremName := Name.mkSimple s!"empty_drop_body_{functionId}" + liftCoreM <| addDecl <| .thmDecl { + name := theoremName, levelParams := [], type := proposition, value := proof } + logInfo m!"Kernel checked empty drops in native function {functionId}" + +end AeneasSpecs.DropAudit diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index 019f7b397f..87a8818042 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -86,6 +86,20 @@ def min_spec : Prop := ∀ (a b : NonZeroUsize), min_spec_contract a b (util.min a b) +-- The generic fixture must return its original value successfully and retain +-- that value's accepted decoding. The ownership audit is independent of this +-- value-level expectation; neither the model provider nor this precondition +-- promises that the Rust type has no destructor. +def move_through_call_spec_contract (T : Type) (value : T) (run : Result T) : Prop := + ∀ [provider : RustModel T] (mathematical : provider.Model), + provider.decode value = some mathematical → + ∃ result, run = .ok result ∧ + ∃ decoded, provider.decode result = some decoded ∧ result = value + +def move_through_call_spec : Prop := + ∀ (T : Type) (value : T), move_through_call_spec_contract T value + (util.move_checks.move_through_call value) + def padding_lt_alignment_contract (len : Usize) (align : NonZeroUsize) (run : Result Usize) : Prop := ∀ (_valid : 0 < align.val.val) (_h : align.val.val.isPowerOfTwo), diff --git a/verification/aeneas/lean/Proofs/MoveChecks.lean b/verification/aeneas/lean/Proofs/MoveChecks.lean new file mode 100644 index 0000000000..54a9566635 --- /dev/null +++ b/verification/aeneas/lean/Proofs/MoveChecks.lean @@ -0,0 +1,28 @@ +/- 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 +@[expose] public section + +/-! +The admission proof, checked before extraction, establishes that the retained +conditional drops cannot execute a destructor. This theorem then checks the +ordinary value behavior against both golden and live function definitions. +The same decoded witness passes through the call; no inhabitedness assumption +or restriction on the generic type's destructor is introduced. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +theorem move_through_call_spec : Specs.move_through_call_spec := by + intro T value provider mathematical decoded + exact WP.spec.ret ⟨mathematical, decoded, rfl⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 132bea595f..c59ecbfd1f 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -832,6 +832,14 @@ spec min_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.min_spec for Zerocopy.util.min with 2 +check_model_inputs Zerocopy.util.move_checks.move_through_call with 1 type parameters +aeneas_spec_begin +spec move_through_call_spec + for @Zerocopy.util.move_checks.move_through_call with 1 type parameters + ensures(raw) result => result = value +aeneas_spec_end +check_spec_binding Zerocopy.Specs.move_through_call_spec for Zerocopy.util.move_checks.move_through_call with 2 + check_model_inputs Zerocopy.util.owned_transmute.to_bytes with 0 type parameters aeneas_spec_begin spec owned_transmute_to_bytes_spec diff --git a/verification/aeneas/run.sh b/verification/aeneas/run.sh index c62aa89b27..78f570bb36 100755 --- a/verification/aeneas/run.sh +++ b/verification/aeneas/run.sh @@ -94,8 +94,9 @@ export CHARON_ANNOTATION_ORIGINS="$work/annotation-origins.json" # FIXME: Typed copies erase storage events (upstream issue #1405): # https://github.com/AeneasVerif/aeneas/issues/1405. Neither strict extraction # errors nor the downstream forbidden tag can detect an already erased effect. -# Promoted MIR precedes drop elaboration: residual Drop terminators reject the -# body rather than relying on destructor desugaring or Aeneas's drop erasure. +# Promoted MIR precedes drop elaboration. Each retained conditional drop needs +# a kernel proof that its whole local is empty; all other drops reject the body. +# Aeneas's erasure cannot establish that a destructor has no effects. python3 verification/aeneas/prepare.py llbc "$work/zerocopy.llbc" "${inline_cmd[@]}" bindings "${inline_args[@]}" --work "$work" "$tools_dir/aeneas" -backend lean -namespace Zerocopy -dest "$work/Zerocopy" \ diff --git a/verification/aeneas/tests/test_admission.py b/verification/aeneas/tests/test_admission.py index 37716030e6..07a9d680a3 100644 --- a/verification/aeneas/tests/test_admission.py +++ b/verification/aeneas/tests/test_admission.py @@ -179,7 +179,7 @@ def test_drop_before_cleanup_and_on_unwind_is_rejected(self): with self.subTest(block=index): previous = self.body()[index]['terminator']['kind'] self.body()[index]['terminator']['kind'] = {'Drop': {}} - with self.assertRaisesRegex(ValueError, 'original terminator Drop'): + with self.assertRaisesRegex(ValueError, 'Drop requires a kernel-checked compiler body'): self.check() self.body()[index]['terminator']['kind'] = previous @@ -217,9 +217,14 @@ def test_bit_invalid_production_cannot_be_an_infallible_cast(self): with self.assertRaisesRegex(ValueError, 'Unreviewed cast Transmute'): self.check() - def test_ub_abort_must_not_become_unwind_termination(self): + def test_known_termination_abort_retains_a_failure_obligation(self): + # Pinned Aeneas lowers every Abort to panic, which both contracts + # reject even for True. Admission is not a proof that execution avoids + # this terminator. Unknown failure forms remain unreviewed. self.body()[0]['terminator']['kind'] = {'Abort': 'UnwindTerminate'} - with self.assertRaisesRegex(ValueError, 'Unreviewed abort UnwindTerminate'): + self.assertEqual(self.check()['roots'], [self.root]) + self.body()[0]['terminator']['kind'] = {'Abort': 'UnreviewedTermination'} + with self.assertRaisesRegex(ValueError, 'Unreviewed abort UnreviewedTermination'): self.check() def test_guarded_translation_must_remain_failure_capable(self): diff --git a/verification/aeneas/tests/test_drop_ownership.py b/verification/aeneas/tests/test_drop_ownership.py new file mode 100644 index 0000000000..8cb948658f --- /dev/null +++ b/verification/aeneas/tests/test_drop_ownership.py @@ -0,0 +1,425 @@ +# 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. + +"""Check the complete-snapshot boundary for empty conditional-drop proofs. + +Small, self-contained compiler-schema bodies exercise both extraction stages. +Installed-runtime tests build the actual Lean checker and witness command; +Python-only controls keep binding and missing-proof rejection covered without +an installed runtime. These fixtures do not execute Rust or establish the +compiler correspondence premise of the ownership model. +""" + +import copy +import hashlib +import json +import os +from pathlib import Path +import sys +import tempfile +import unittest +from unittest import mock + +ROOT = Path(__file__).resolve().parents[3] +sys.path.insert(0, str(ROOT / 'verification/aeneas')) +import admission +import drop_ownership + +TOOLS = Path(os.environ.get('AENEAS_TOOLCHAIN_DIR', + str(ROOT / 'target/aeneas/toolchain'))).resolve() +LEAN = TOOLS / 'lean/bin/lean' +ROOT_NAME = 'zerocopy::empty_drop_test' +FUNCTION_ID = 7 + + +def body_fixture(stage='Unstructured', move='Move'): + """Move the argument into the return slot, then conditionally drop it.""" + boolean = {'Untagged': {'Scalar': 'Bool'}} + span = {'Untagged': {'data': {'file_id': 0, + 'beg': {'line': 1, 'col': 0}, 'end': {'line': 1, 'col': 1}}, + 'generated_from_span': None}} + generics = {'regions': [], 'types': [], 'const_generics': [], 'trait_refs': []} + + def place(index): + return {'kind': {'Local': index}, 'ty': copy.deepcopy(boolean)} + + def statement(kind, index=0): + result = {'span': span, 'kind': kind, 'comments_before': []} + if stage == 'Structured': + result['id'] = index + return result + + assignment = {'Assign': [place(0), {'Use': [{move: place(1)}, 'Yes']}]} + dropped = {'kind': 'Conditional', 'place': place(1), + 'fn_ptr': {'kind': {'Fun': 99}, 'generics': generics}} + if stage == 'Unstructured': + dropped.update(target=1, on_unwind=2) + contents = [ + {'statements': [statement(assignment)], + 'terminator': statement({'Drop': dropped})}, + {'statements': [], 'terminator': statement('Return')}, + {'statements': [], 'terminator': statement('UnwindResume')}, + ] + elif stage == 'Structured': + dropped['on_unwind'] = {'span': span, 'id': 1, + 'statements': [statement('UnwindResume', 2)]} + contents = {'span': span, 'id': 0, 'statements': [ + statement(assignment), statement({'Drop': dropped}, 1), + statement('Return', 3)]} + else: + raise ValueError(stage) + return {stage: {'span': span, 'bound_body_regions': 0, + 'locals': {'arg_count': 1, 'locals': [ + {'index': index, 'name': None, 'span': span, + 'ty': copy.deepcopy(boolean), 'drop_flag_for': None} + for index in range(2)]}, + 'body': contents, 'comments': []}} + + +def function_fixture(stage='Unstructured', move='Move'): + return {'def_id': FUNCTION_ID, 'body': body_fixture(stage, move)} + + +def snapshot_bytes(function, **extra): + return json.dumps({'has_errors': False, + 'translated': {'fun_decls': [function]}, **extra}, sort_keys=True).encode() + + +def admission_fixture(stage='Unstructured', move='Move'): + # Reuse only the checked-in compiler option and declaration scaffolding. + # This leaf root needs no external interpretations or executable callees. + fixture = Path(__file__).with_name('admission') / 'boolean.before.ullbc' + data = json.loads(fixture.read_text()) + function = next(f for f in data['translated']['fun_decls'] if f) + function['def_id'] = FUNCTION_ID + function['item_meta']['name'] = [{'Ident': [part, 0]} + for part in ROOT_NAME.split('::')] + function['item_meta']['attr_info']['attributes'] = [] + function['signature'] = {'is_unsafe': False, 'abi': 'Rust', + 'is_variadic': False, 'inputs': [{'Untagged': {'Scalar': 'Bool'}}], + 'output': {'Untagged': {'Scalar': 'Bool'}}} + function['body'] = body_fixture(stage, move) + crate = data['translated'] + crate['fun_decls'] = [function] + crate['trait_impls'] = [] + crate['options']['exclude'] = list(admission.EXCLUDED_PROVIDED_METHODS) + crate['options']['opaque'] = [admission.INTERFACE_ONLY_VALIDATORS, + *admission.INTERFACE_ONLY_TYPES] + return data, function + + +def recheck_fixture(work): + """Write both stage inputs and their saved source-identity records.""" + registry = json.loads((ROOT / 'verification/aeneas/external.json').read_text()) + reports = {} + for stage, tag, filename in ( + ('before', 'Unstructured', 'zerocopy.before.ullbc'), + ('llbc', 'Structured', 'zerocopy.llbc')): + data, function = admission_fixture(tag) + # inspect_stages uses the production registry. This leaf fixture does + # not call any of its boundaries, but must preserve its option profile. + data['translated']['options']['opaque'] += [row['rust'] for row in registry + if row.get('opaque')] + contents = json.dumps(data).encode() + (work / filename).write_bytes(contents) + snapshot = hashlib.sha256(contents).hexdigest() + reports[stage] = {'roots': [ROOT_NAME], 'calls': [], + 'executions': [{'rust': ROOT_NAME, 'origin': 'body'}], + 'sha256': snapshot, 'empty_drops': [{ + 'function_def_id': FUNCTION_ID, + 'body_sha256': drop_ownership.body_digest(function['body']), + 'snapshot_sha256': snapshot, + 'proof_module': 'old_witness_' + stage, 'proof_sha256': 'old-artifact'}]} + return {'bindings': {ROOT_NAME: {'kind': 'function'}, + 'unused::Type': {'kind': 'type'}}, + 'trait_laws': [], 'admission': {'stages': reports}} + + +class DropBindingTests(unittest.TestCase): + def setUp(self): + self.scratch = tempfile.TemporaryDirectory(prefix='aeneas-drop-binding-') + self.addCleanup(self.scratch.cleanup) + self.driver = drop_ownership.KernelDrops(ROOT, Path(self.scratch.name)) + + def test_body_substitution_with_same_native_id_is_rejected_before_lean(self): + original = function_fixture() + self.driver.freeze('before', snapshot_bytes(original)) + for replacement in (function_fixture(move='Copy'), + {'def_id': FUNCTION_ID, 'body': {'fabricated': []}}): + with self.subTest(body=replacement['body']): + with mock.patch.object(self.driver, 'initialize'), \ + mock.patch.object(self.driver, 'run') as run: + with self.assertRaisesRegex(ValueError, 'differs from the inspected'): + self.driver.certify('before', replacement) + run.assert_not_called() + + def test_duplicate_native_ids_are_rejected_before_lean(self): + function = function_fixture() + contents = json.dumps({'has_errors': False, 'translated': { + 'fun_decls': [function, copy.deepcopy(function)]}}).encode() + self.driver.freeze('before', contents) + with mock.patch.object(self.driver, 'initialize'), \ + mock.patch.object(self.driver, 'run') as run: + with self.assertRaisesRegex(ValueError, 'differs from the inspected'): + self.driver.certify('before', function) + run.assert_not_called() + + def test_admission_requires_a_certificate_callback(self): + for stage in ('Unstructured', 'Structured'): + data, _ = admission_fixture(stage) + with self.subTest(stage=stage): + with self.assertRaisesRegex(ValueError, 'requires a kernel-checked compiler body'): + admission.Admission(data, []).audit([ROOT_NAME]) + + def test_admission_rejects_a_certificate_for_another_body(self): + data, function = admission_fixture(move='Copy') + stale = {'function_def_id': FUNCTION_ID, + 'body_sha256': drop_ownership.body_digest(body_fixture())} + self.assertNotEqual(stale['body_sha256'], + drop_ownership.body_digest(function['body'])) + with self.assertRaisesRegex(ValueError, 'does not identify this exact compiler body'): + admission.Admission(data, [], certify_drops=lambda _: stale).audit([ROOT_NAME]) + + def test_admission_propagates_certificate_failure(self): + data, _ = admission_fixture() + + def rejected(_): + raise ValueError('kernel proof failed') + + with self.assertRaisesRegex(ValueError, 'kernel proof failed'): + admission.Admission(data, [], certify_drops=rejected).audit([ROOT_NAME]) + + +class DropRecheckTests(unittest.TestCase): + def setUp(self): + self.scratch = tempfile.TemporaryDirectory(prefix='aeneas-drop-recheck-') + self.addCleanup(self.scratch.cleanup) + self.work = Path(self.scratch.name) + self.manifest = recheck_fixture(self.work) + self.fresh = copy.deepcopy(self.manifest['admission']['stages']) + + def test_missing_empty_or_duplicate_proof_records_are_rejected(self): + for stage in ('before', 'llbc'): + for mutation in ('missing', 'empty', 'duplicate', 'not-list'): + saved = copy.deepcopy(self.manifest) + report = saved['admission']['stages'][stage] + if mutation == 'missing': + del report['empty_drops'] + elif mutation == 'empty': + report['empty_drops'] = [] + elif mutation == 'duplicate': + report['empty_drops'] *= 2 + else: + report['empty_drops'] = None + with self.subTest(stage=stage, mutation=mutation): + with mock.patch.object(admission, 'inspect_stages', return_value=self.fresh): + with self.assertRaisesRegex(ValueError, 'proof records|admission evidence'): + admission.recheck(ROOT, self.work, saved) + + def test_missing_or_stale_body_and_snapshot_identities_are_rejected(self): + for stage in ('before', 'llbc'): + for key in ('function_def_id', 'body_sha256', 'snapshot_sha256'): + for mutation in ('missing', 'stale'): + saved = copy.deepcopy(self.manifest) + row = saved['admission']['stages'][stage]['empty_drops'][0] + if mutation == 'missing': + del row[key] + else: + row[key] = 'different-source' + with self.subTest(stage=stage, key=key, mutation=mutation): + with mock.patch.object(admission, 'inspect_stages', return_value=self.fresh): + with self.assertRaisesRegex(ValueError, 'proof records|admission evidence'): + admission.recheck(ROOT, self.work, saved) + + def test_changed_snapshot_is_rejected_before_inspection(self): + for stage, filename in (('before', 'zerocopy.before.ullbc'), ('llbc', 'zerocopy.llbc')): + path = self.work / filename + original = path.read_bytes() + path.write_bytes(original + b'\n') + with self.subTest(stage=stage): + with mock.patch.object(admission, 'inspect_stages') as inspect: + with self.assertRaisesRegex(ValueError, f'Stale {stage} admission snapshot'): + admission.recheck(ROOT, self.work, self.manifest) + inspect.assert_not_called() + path.write_bytes(original) + + def test_missing_snapshot_hash_is_rejected_before_inspection(self): + for stage in ('before', 'llbc'): + saved = copy.deepcopy(self.manifest) + del saved['admission']['stages'][stage]['sha256'] + with self.subTest(stage=stage): + with mock.patch.object(admission, 'inspect_stages') as inspect: + with self.assertRaisesRegex(ValueError, f'Stale {stage} admission snapshot'): + admission.recheck(ROOT, self.work, saved) + inspect.assert_not_called() + + def test_recheck_compares_source_records_and_requests_bound_roots(self): + # Fresh compilation can produce different artifact names or hashes. + # Acceptance still requires equal body and snapshot source identities. + for report in self.fresh.values(): + report['empty_drops'][0].update(proof_module='new_witness', proof_sha256='new-artifact') + self.manifest['trait_laws'] = [{'rust': 'zerocopy::TestLaw'}] + with mock.patch.object(admission, 'inspect_stages', return_value=self.fresh) as inspect: + admission.recheck(ROOT, self.work, self.manifest) + inspect.assert_called_once_with(ROOT, self.work, [ROOT_NAME], ['zerocopy::TestLaw']) + + +@unittest.skipUnless(LEAN.is_file(), 'requires installed pinned Lean') +class CompiledDropAdmissionTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.scratch = tempfile.TemporaryDirectory(prefix='aeneas-drop-kernel-') + cls.addClassCleanup(cls.scratch.cleanup) + cls.driver = drop_ownership.KernelDrops(ROOT, Path(cls.scratch.name)) + # Build once, but use a distinct frozen stage for each independent case. + # A present installation must pass production provenance validation. + cls.driver.initialize() + + def certify(self, stage, function, contents=None): + contents = snapshot_bytes(function) if contents is None else contents + self.driver.freeze(stage, contents) + return self.driver.certify(stage, function) + + def test_both_complete_body_stages_receive_fresh_kernel_proofs(self): + for tag, stage in (('Unstructured', 'before'), ('Structured', 'final')): + with self.subTest(stage=stage): + function = function_fixture(tag) + # An unused snapshot field still contributes to the identity. + contents = snapshot_bytes(function, compiler_identity='test-fixture') + record = self.certify(stage, function, contents) + self.assertEqual(record['function_def_id'], FUNCTION_ID) + self.assertEqual(record['body_sha256'], + drop_ownership.body_digest(function['body'])) + self.assertEqual(record['snapshot_sha256'], hashlib.sha256(contents).hexdigest()) + self.assertEqual((self.driver.work / (stage + '.json')).read_bytes(), contents) + proof = self.driver.work / (record['proof_module'] + '.olean') + self.assertEqual(record['proof_sha256'], hashlib.sha256(proof.read_bytes()).hexdigest()) + + def test_move_to_copy_mutation_fails_in_the_kernel(self): + for tag in ('Unstructured', 'Structured'): + stage = 'copy_' + tag.lower() + with self.subTest(stage=tag): + with self.assertRaisesRegex(ValueError, 'Kernel rejected empty-drop admission'): + self.certify(stage, function_fixture(tag, move='Copy')) + self.assertNotIn((stage, FUNCTION_ID), self.driver.proofs) + log = self.driver.work / f'DropWitness_{stage}_{FUNCTION_ID}.log' + self.assertIn('(kernel) declaration type mismatch', log.read_text()) + + def test_repaired_temporary_body_cannot_certify_the_original(self): + # Lean can prove the repaired Move body. That proof must never be + # recorded against the unsafe Copy body selected by Admission. + stage = 'repaired_temporary_body' + original = function_fixture(move='Copy') + repaired = snapshot_bytes(function_fixture()) + run = self.driver.run + + def repair_then_check(module, env=None): + (self.driver.work / (stage + '.json')).write_bytes(repaired) + return run(module, env) + + with mock.patch.object(self.driver, 'run', side_effect=repair_then_check): + with self.assertRaisesRegex(ValueError, 'inputs changed during kernel checking'): + self.certify(stage, original) + self.assertNotIn((stage, FUNCTION_ID), self.driver.proofs) + + def test_edited_witness_cannot_omit_the_kernel_command(self): + stage = 'edited_witness' + run = self.driver.run + + def erase_then_check(module, env=None): + (self.driver.work / (module + '.lean')).write_text('import DropAudit\n') + return run(module, env) + + with mock.patch.object(self.driver, 'run', side_effect=erase_then_check): + with self.assertRaisesRegex(ValueError, 'inputs changed during kernel checking'): + self.certify(stage, function_fixture(move='Copy')) + self.assertNotIn((stage, FUNCTION_ID), self.driver.proofs) + + def test_unknown_executable_field_cannot_receive_a_proof(self): + function = function_fixture() + function['body']['Unstructured']['body'][0]['statements'][0]['hidden_move'] = 1 + with self.assertRaisesRegex(ValueError, 'Kernel rejected empty-drop admission'): + self.certify('unknown_field', function) + self.assertNotIn(('unknown_field', FUNCTION_ID), self.driver.proofs) + + def test_changing_frozen_snapshot_bytes_cannot_reuse_a_proof(self): + function = function_fixture() + original = snapshot_bytes(function) + first = self.certify('changed_buffer', function, original) + changed = original + b'\n' + self.assertEqual(json.loads(original), json.loads(changed)) + self.driver.freeze('changed_buffer', changed) + with self.assertRaisesRegex(ValueError, 'Frozen drop-admission snapshot changed'): + self.driver.certify('changed_buffer', function) + self.assertEqual((self.driver.work / 'changed_buffer.json').read_bytes(), original) + self.assertNotEqual(first['snapshot_sha256'], hashlib.sha256(changed).hexdigest()) + + def test_tampered_snapshot_file_is_rejected(self): + function = function_fixture() + original = snapshot_bytes(function) + self.certify('changed_file', function, original) + (self.driver.work / 'changed_file.json').write_bytes(original + b'\n') + with self.assertRaisesRegex(ValueError, 'Frozen drop-admission snapshot changed'): + self.driver.certify('changed_file', function) + + def test_lean_command_independently_rejects_duplicate_native_ids(self): + function = function_fixture() + snapshot = self.driver.work / 'duplicate_command.json' + snapshot.write_text(json.dumps({'has_errors': False, 'translated': { + 'fun_decls': [function, copy.deepcopy(function)]}})) + module = 'DuplicateNativeDropControl' + (self.driver.work / (module + '.lean')).write_text( + f'import DropAudit\ncertify_empty_drops {FUNCTION_ID}\n') + env = dict(self.driver.env, AENEAS_DROP_SNAPSHOT=str(snapshot)) + with self.assertRaisesRegex(ValueError, 'Missing or ambiguous native function'): + self.driver.run(module, env) + + def test_admission_uses_kernel_certificates_for_both_stages(self): + for tag in ('Unstructured', 'Structured'): + data, function = admission_fixture(tag) + stage = 'audit_' + tag.lower() + self.driver.freeze(stage, json.dumps(data).encode()) + with self.subTest(stage=tag): + report = admission.Admission(data, [], certify_drops= + lambda current, stage=stage: self.driver.certify(stage, current)).audit([ROOT_NAME]) + self.assertEqual(report['roots'], [ROOT_NAME]) + self.assertEqual(report['empty_drops'], [self.driver.proofs[stage, FUNCTION_ID]]) + self.assertEqual(report['executions'], [{'rust': ROOT_NAME, 'origin': 'body'}]) + self.assertEqual(report['empty_drops'][0]['body_sha256'], + drop_ownership.body_digest(function['body'])) + + def test_recheck_rebuilds_checker_and_kernel_witnesses_for_both_stages(self): + with tempfile.TemporaryDirectory(prefix='aeneas-fresh-drop-recheck-') as directory: + work = Path(directory) + manifest = recheck_fixture(work) + saved = admission.inspect_stages(ROOT, work, [ROOT_NAME], []) + manifest['admission']['stages'] = copy.deepcopy(saved) + previous_builds = set(work.glob('empty-drops-*')) + self.assertEqual(len(previous_builds), 1) + # Saved compiled-witness fields are deliberately unusable. A fresh + # proof must establish the same complete-body source identities. + for report in manifest['admission']['stages'].values(): + report['empty_drops'][0].update(proof_module='absent_saved_witness', + proof_sha256='untrusted-saved-artifact') + real_run = drop_ownership.KernelDrops.run + runs = [] + + def record_run(driver, module, env=None): + runs.append((driver.work, module)) + return real_run(driver, module, env) + + with mock.patch.object(drop_ownership.KernelDrops, 'run', new=record_run): + admission.recheck(ROOT, work, manifest) + self.assertEqual([module for _, module in runs], [ + 'DropOwnership', 'DropJson', 'DropAudit', + f'DropWitness_before_{FUNCTION_ID}', f'DropWitness_llbc_{FUNCTION_ID}']) + self.assertTrue(all(directory not in previous_builds for directory, _ in runs)) + + +if __name__ == '__main__': + unittest.main() diff --git a/verification/aeneas/tests/test_toolchain.py b/verification/aeneas/tests/test_toolchain.py index cccaf96c3a..002d6163e0 100644 --- a/verification/aeneas/tests/test_toolchain.py +++ b/verification/aeneas/tests/test_toolchain.py @@ -373,6 +373,7 @@ def test_shell_exports_validated_runtime_for_admission_with_and_without_override for name in ['anneal/flake.lock', 'verification/aeneas/toolchain.sh', 'verification/aeneas/toolchain.py', 'verification/aeneas/admission.py', 'verification/aeneas/source_inventory.py', + 'verification/aeneas/drop_ownership.py', 'verification/aeneas/patches/use-tuple-structs.patch', 'verification/aeneas/patches/admission-snapshot.patch']: target = root / name diff --git a/verification/aeneas/tests/test_workspace.py b/verification/aeneas/tests/test_workspace.py index 9e65e3a02e..b0351ff671 100644 --- a/verification/aeneas/tests/test_workspace.py +++ b/verification/aeneas/tests/test_workspace.py @@ -160,15 +160,18 @@ def test_verified_check_requires_both_admission_stages_and_fresh_inputs(self): mutants.append(mutant) with mock.patch.object(admission, 'input_identity', return_value={'project': 'current'}), \ mock.patch.object(admission, 'digest', return_value='registry'), \ + mock.patch.object(admission, 'recheck') as recheck, \ mock.patch.object(workspace, 'run_checked') as run: for mutant in mutants: (work / 'bindings.json').write_text(json.dumps(mutant)) with self.subTest(mutant=mutant), self.assertRaisesRegex(ValueError, 'admission evidence'): workspace.check(root, work) run.assert_not_called() + recheck.assert_not_called() (work / 'bindings.json').write_text(json.dumps(manifest)) workspace.check(root, work) self.assertEqual(run.call_count, 3) + recheck.assert_called_once_with(root, work, manifest) run.reset_mock() # An editor changing Rust during a successful proof build must # prevent that build from certifying the edited source. diff --git a/verification/aeneas/workspace.py b/verification/aeneas/workspace.py index d702326d09..1ef7a61eaf 100644 --- a/verification/aeneas/workspace.py +++ b/verification/aeneas/workspace.py @@ -247,6 +247,7 @@ def check(root, work, *, require_admission=False): set(evidence.get('stages', {})) != {'before', 'llbc'} or any(stage.get('roots') != roots for stage in evidence['stages'].values())): raise ValueError('Missing or stale mandatory admission evidence; run fresh extraction') + admission.recheck(root, work, manifest) # --old preserves the archive's read-only dependency caches, but ignores # changed imports. A persistent editor project could therefore reuse a proof # checked against an earlier model. Even the direct axiom audit would accept diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index ad07629e88..795cec98ce 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -17,6 +17,7 @@ pub mod macro_util; mod allocation; pub(crate) mod bytewrite; mod checks; +mod move_checks; #[cfg(target_endian = "little")] #[allow(dead_code)] mod owned_transmute; diff --git a/zerocopy/src/util/move_checks/mod.rs b/zerocopy/src/util/move_checks/mod.rs new file mode 100644 index 0000000000..2b3096b085 --- /dev/null +++ b/zerocopy/src/util/move_checks/mod.rs @@ -0,0 +1,52 @@ +// 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. + +//! Exercise ownership transfer without assuming that `T` has no destructor. +//! +//! Early MIR retains conditional drops of the argument and its temporary even +//! after both have moved. CI must prove those slots empty before ignoring the +//! drops. Neither the generic caller nor its callee may execute a destructor. + +#![allow(dead_code)] + +/// Returns the original value through an ordinary generic call. +/// +/// ```aeneas +/// spec move_through_call_spec +/// ensures(raw) result => result = value +/// ``` +fn move_through_call(value: T) -> T { + forward(value) +} + +fn forward(value: T) -> T { + value +} + +#[cfg(test)] +mod tests { + use core::cell::Cell; + + use super::move_through_call; + + #[test] + fn destructor_stays_with_returned_value() { + struct CountDrop<'a>(&'a Cell); + impl Drop for CountDrop<'_> { + fn drop(&mut self) { + self.0.set(self.0.get().saturating_add(1)); + } + } + let drops = Cell::new(0); + let returned = move_through_call(CountDrop(&drops)); + assert_eq!(drops.get(), 0); + drop(returned); + assert_eq!(drops.get(), 1); + } +}