diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index e4fdc3048b..59c094fcce 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -805,6 +805,14 @@ law. Negative Lean examples distinguish Boolean zero validity from Boolean validity for every byte, and reject zero construction of nonzero integers or a value rejected by its library decoder. +The specification on the existing `FromZeros::new_zeroed` default method proves +its actual body under the exact enclosing trait's law. Its stdlib boundary, +`core::mem::zeroed`, decodes zero storage before returning a typed value; +rejection is forbidden execution, even for a `True` postcondition. The compiled +audit checks this complete definition, not just successful examples. An +independent required contract states the physical and mathematical decoding +facts without using the primitive's implementation. + Aeneas normally has no model dictionary in the computation. The downstream `native_models` elaborator retains a provider only in generic definitions whose bodies need this boundary. Original Rust arguments remain in their exact @@ -826,8 +834,8 @@ As with `IntoBytes`, applying these proofs to Rust assumes the physical decoder has the correct Rust width and language meaning. The primitive and array interpretations have explicit Reference premises; compiler assertions challenge the concrete widths. A generic provider is a supplied interpretation, not a -proof of an arbitrary downstream type's representation. These construction laws -cover the selected impls; they do not certify pointer access, external-state +proof of an arbitrary downstream type's representation. This example covers +resource-free owned zero construction, not pointer access, external-state invariants, destructors, or every `FromBytes`/`FromZeros` impl. ## Native Lean proofs and independent checks diff --git a/verification/aeneas/control_runner.py b/verification/aeneas/control_runner.py index a4efbe3b3a..cda73c5405 100644 --- a/verification/aeneas/control_runner.py +++ b/verification/aeneas/control_runner.py @@ -29,7 +29,7 @@ FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi', 'contracts', 'dependencies', 'admission', 'semantics', 'owned-std') MODELS = ('golden-verification', 'verification') -FIXTURES = ('StdTransmuteAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean', +FIXTURES = ('StdTransmuteAuditProbe.lean', 'ZeroedAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean', 'RoundingConstructorControl.lean', 'RoundingDomainControl.lean', 'Zerocopy/ScopeControl.lean', 'Zerocopy/ShapeControl.lean', 'Zerocopy/ModelControl.lean', 'Proofs/WitnessOwnerControl.lean', diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index bf8af4c75f..c55c1bd583 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -644,7 +644,7 @@ def byteorder.verification.set_u32_be byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 /-- [zerocopy::FromZeros::new_zeroed]: - Source: 'src/lib.rs', lines 3823:4-3829:5 + Source: 'src/lib.rs', lines 3827:4-3833:5 Visibility: public -/ @[trait_default] native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index d54dc0e86d..64ea9516f1 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -246,7 +246,7 @@ structure TryFromBytes (Self : Type) where pointer.invariant.Initialized → Result Bool /-- Trait declaration: [zerocopy::FromZeros] - Source: 'src/lib.rs', lines 3708:0-4070:1 + Source: 'src/lib.rs', lines 3708:0-4074:1 Visibility: public -/ structure FromZeros (Self : Type) where TryFromBytesInst : TryFromBytes Self @@ -254,14 +254,14 @@ structure FromZeros (Self : Type) where new_zeroed : Result Self /-- Trait declaration: [zerocopy::FromBytes] - Source: 'src/lib.rs', lines 4298:0-5710:1 + Source: 'src/lib.rs', lines 4302:0-5714:1 Visibility: public -/ structure FromBytes (Self : Type) where FromZerosInst : FromZeros Self only_derive_is_allowed_to_implement_this_trait : Result Unit /-- Trait declaration: [zerocopy::IntoBytes] - Source: 'src/lib.rs', lines 5949:0-6454:1 + Source: 'src/lib.rs', lines 5953:0-6458:1 Visibility: public -/ structure IntoBytes (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit diff --git a/verification/aeneas/lean/Obligations/Zeroed.lean b/verification/aeneas/lean/Obligations/Zeroed.lean new file mode 100644 index 0000000000..b25fbc1583 --- /dev/null +++ b/verification/aeneas/lean/Obligations/Zeroed.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 TraitLaws +public import RustRepresentation +@[expose] public section + +/-! +The independent outcome family requires successful execution, an available +physical decoder accepting the initialized all-zero representation, and an +accepted mathematical value through the retained provider. It does not define +the expected outcome in terms of the extracted default method or its guarded +implementation. The concrete proposition specializes the same family to that +method only after the arbitrary-outcome expectation has been stated. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Obligations + +def new_zeroed_spec_contract (Self : Type) (meaning : RustModel Self) + (run : Result Self) : Prop := + ∀ (dictionary : FromZeros Self) [_law : @TraitLaws.from_zeros_valid Self dictionary meaning], + ∃ raw value decoder, run = .ok raw ∧ meaning.representation = some decoder ∧ + decoder.run (List.replicate decoder.byteSize (Rust.Storage.AMByte.init 0)) = some raw ∧ + meaning.decode raw = some value + +def new_zeroed_spec : Prop := + ∀ (Self : Type) [_meaning : RustModel Self], + new_zeroed_spec_contract Self _meaning (FromZeros.new_zeroed.default Self) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/Zeroed.lean b/verification/aeneas/lean/Proofs/Zeroed.lean new file mode 100644 index 0000000000..b62622c4f7 --- /dev/null +++ b/verification/aeneas/lean/Proofs/Zeroed.lean @@ -0,0 +1,33 @@ +/- 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 RustRepresentation +@[expose] public section + +/-! +The production default method calls the guarded zero constructor with its +retained semantic provider. Its enclosing FromZeros dictionary supplies zero +admission; the returned raw value must also decode through that same provider. +This proof does not infer that a moved raw value retains initialized padding. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +theorem new_zeroed_spec : Specs.new_zeroed_spec := by + intro Self meaning dictionary law + obtain ⟨raw, value, constructed, decoded⟩ := meaning.zeroedResult_admitted + (@TraitLaws.from_zeros_valid.holds Self dictionary meaning law) + change meaning.zeroedResult ⦃ output => + ∃ mathematical, meaning.decode output = some mathematical ∧ meaning.zeroedResult = .ok output ⦄ + rw [constructed] + exact ⟨value, decoded, rfl⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/Zeroed.lean b/verification/aeneas/lean/RequiredModelContracts/Zeroed.lean new file mode 100644 index 0000000000..560bd3dae4 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/Zeroed.lean @@ -0,0 +1,30 @@ +/- 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 Obligations.Zeroed +public import RequiredContracts +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +-- Compare arbitrary outcomes without assuming the function's own correctness. +-- The expectation states each decoding stage instead of repeating zeroedValue. +@[contract_simps] theorem required_new_zeroed (Self : Type) [meaning : RustModel Self] + (run : Result Self) (provided : Specs.new_zeroed_spec_contract Self run) : + Obligations.new_zeroed_spec_contract Self meaning run := by + intro dictionary law + obtain ⟨raw, executed, mathematical, decoded, zeroed⟩ := + (WP.spec_equiv_exists run _).mp (provided dictionary) + obtain ⟨decoder, available, physical, _⟩ := + (meaning.zeroedResult_eq_ok_iff raw).mp zeroed + exact ⟨raw, mathematical, decoder, executed, available, physical, decoded⟩ + + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/ZeroedContractTests.lean b/verification/aeneas/lean/ZeroedContractTests.lean new file mode 100644 index 0000000000..07a104cfd7 --- /dev/null +++ b/verification/aeneas/lean/ZeroedContractTests.lean @@ -0,0 +1,45 @@ +/- 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 Proofs.Zeroed +public import Proofs.FromBytes +public import RequiredModelContracts.Zeroed +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +-- The independent expectation rejects failure, divergence, and a valid Boolean +-- with the wrong value. These are model tests, not executions of invalid Rust. +example : Obligations.new_zeroed_spec := by + intro Self meaning + exact required_new_zeroed Self (FromZeros.new_zeroed.default Self) + (new_zeroed_spec Self) + +example : ¬ @Obligations.new_zeroed_spec_contract Bool modelBool (.fail .undef) := by + intro expected + obtain ⟨raw, _, _, executed, _⟩ := expected Bool.Insts.ZerocopyFromZeros + simp at executed + +example : ¬ @Obligations.new_zeroed_spec_contract Bool modelBool .div := by + intro expected + obtain ⟨raw, _, _, executed, _⟩ := expected Bool.Insts.ZerocopyFromZeros + simp at executed + +example : ¬ @Obligations.new_zeroed_spec_contract Bool modelBool (.ok true) := by + intro expected + obtain ⟨raw, _, decoder, executed, available, physical, _⟩ := + expected Bool.Insts.ZerocopyFromZeros + have same : raw = true := by simpa using executed.symm + subst raw + change some Rust.Storage.boolDecoder = some decoder at available + cases Option.some.inj available + change some false = some true at physical + contradiction + +end Zerocopy.Proofs diff --git a/verification/aeneas/negative-control-family.sh b/verification/aeneas/negative-control-family.sh index 3db0053065..b08bbc0e9f 100644 --- a/verification/aeneas/negative-control-family.sh +++ b/verification/aeneas/negative-control-family.sh @@ -24,7 +24,7 @@ echo "Testing failure controls in $1" # suite starts and is removed on exit. Use the same roster for both decisions # so cleanup cannot delete a source that belonged to an earlier editor session. control_files=( - StdTransmuteAuditProbe.lean NegativeControl.lean WeakOutcome.lean + StdTransmuteAuditProbe.lean ZeroedAuditProbe.lean NegativeControl.lean WeakOutcome.lean RoundingConstructorControl.lean RoundingDomainControl.lean Zerocopy/ScopeControl.lean Zerocopy/ShapeControl.lean Zerocopy/ModelControl.lean Proofs/WitnessOwnerControl.lean Proofs/PaddingDependencyControl.lean @@ -310,6 +310,12 @@ restore_build() { } if [[ $AENEAS_CONTROL_FAMILY == unsafe ]]; then +# Exercise the new constructor's execution guard and exact retained decoder, +# separately from its proof on valid inputs and its enclosing trait premise. +if has_model FromZeros.new_zeroed.default; then + python3 -B "$repo/verification/aeneas/tests/zeroed_audit_controls.py" \ + --work "$PWD" --runtime "$tools_dir" --evidence "$backup/zeroed" +fi # Successful-input proofs cannot detect changing UB into an ordinary panic. # Check the independent primitive interpretation, then directly compile the # rejection examples so --old cannot replay a test from the unchanged model. diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 8992e2fb55..e789f38735 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -122,6 +122,15 @@ spec set_u32_be_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.set_u32_be_spec for Zerocopy.byteorder.verification.set_u32_be with 2 +default_trait_body Zerocopy.FromZeros.new_zeroed.default for Zerocopy.FromZeros with 1 type parameters +check_model_inputs Zerocopy.FromZeros.new_zeroed.default with 1 type parameters +aeneas_spec_begin +spec new_zeroed_spec + for @Zerocopy.FromZeros.new_zeroed.default with 1 type parameters + ensures(raw) r => AeneasSpecs.RustModel.zeroedValue r +aeneas_spec_end +check_spec_binding Zerocopy.Specs.new_zeroed_spec for Zerocopy.FromZeros.new_zeroed.default with 1 + check_model_inputs Zerocopy.trait_checks.byte_codec_roundtrip with 1 type parameters aeneas_spec_begin spec byte_codec_roundtrip_spec diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean index a78de272b0..c47a29cc66 100644 --- a/verification/aeneas/projections/TraitLaws.lean +++ b/verification/aeneas/projections/TraitLaws.lean @@ -26,6 +26,9 @@ trait_dictionary @Zerocopy.FromZeros trait_dictionary @Zerocopy.FromBytes trait_dictionary @Zerocopy.IntoBytes trait_dictionary @Zerocopy.trait_checks.ByteCodec +trait_invariant from_zeros_valid for @Zerocopy.FromZeros with 1 type parameters where self => + AeneasSpecs.RustModel.zeroRepresentation Self + trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type parameters where self => ∀ byte, (do let encoded ← self.encode byte; self.decode encoded) ⦃ result => result = byte ⦄ @@ -33,9 +36,6 @@ trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type trait_invariant into_bytes_initialized for @Zerocopy.IntoBytes with 1 type parameters where self => AeneasSpecs.RustModel.initializedRepresentation Self -trait_invariant from_zeros_valid for @Zerocopy.FromZeros with 1 type parameters where self => - AeneasSpecs.RustModel.zeroRepresentation Self - trait_invariant from_bytes_valid for @Zerocopy.FromBytes with 1 type parameters where self => AeneasSpecs.RustModel.completeRepresentation Self diff --git a/verification/aeneas/tests/zeroed_audit_controls.py b/verification/aeneas/tests/zeroed_audit_controls.py new file mode 100644 index 0000000000..f0d1c9ab9b --- /dev/null +++ b/verification/aeneas/tests/zeroed_audit_controls.py @@ -0,0 +1,195 @@ +# 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. + +"""Challenge zeroed's compiled interpretation, provider, and source premises. + +Only a disposable generated project is mutated. Every native mutant must first +compile; rejection must then come from its intended audit diagnostic. Compiler +snapshots remain unchanged, and no invalid Rust execution is performed. +""" + +import argparse +import copy +import json +import os +from pathlib import Path +import re +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[3] +sys.path.insert(0, str(ROOT / 'verification/aeneas')) +import toolchain + + +PROBE = '''import ZeroedAudit +open Lean Elab +run_elab do + let contents ← IO.FS.readFile "bindings.json" + let .ok bindings := Json.parse contents | throwError "Invalid control bindings" + auditZeroed bindings +''' + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--work', type=Path, required=True) + parser.add_argument('--runtime', type=Path, required=True) + parser.add_argument('--evidence', type=Path, required=True) + args = parser.parse_args() + work = args.work.resolve() + runtime = args.runtime.resolve() + output = args.evidence.resolve() + standard = work in [ROOT / 'target/aeneas/verification', + ROOT / 'target/aeneas/golden-verification'] + private = (work.name == 'project' + and work.parent.parent.name.startswith('control-sandboxes-') + and work.parent.parent.parent == ROOT / 'target/aeneas' + and os.environ.get('AENEAS_CONTROL_PROJECT') == str(work) + and os.environ.get('AENEAS_CONTROL_REPO') == str(ROOT)) + if not (standard or private): + raise ValueError('Controls require a disposable verification project') + toolchain.validate(ROOT, runtime) + environment = toolchain.runtime_env(runtime) + environment['LEAN_NUM_THREADS'] = '2' + output.mkdir(parents=True, exist_ok=False) + probe = work / 'ZeroedAuditProbe.lean' + if probe.exists() or probe.is_symlink(): + raise ValueError('Zeroed audit probe already belongs to an earlier session') + external = work / 'Zerocopy/FunsExternal.lean' + native = work / 'Zerocopy/Funs.lean' + bindings = work / 'bindings.json' + originals = {path: path.read_bytes() for path in (external, native, bindings)} + manifest = json.loads(originals[bindings]) + owner = 'zerocopy::FromZeros::new_zeroed' + entry = manifest['bindings'][owner] + if (entry['raw'] != 'Zerocopy.FromZeros.new_zeroed.default' + or entry['erased_self_bound']['rust'] != 'zerocopy::FromZeros'): + raise ValueError('Zeroed controls require the actual default and erased Self owner') + stages = manifest['admission']['stages'] + for stage in ('before', 'llbc'): + calls = [row for row in stages[stage]['calls'] + if row.get('callee') == 'core::mem::zeroed'] + if (len(calls) != 1 or calls[0]['caller'] != owner + or calls[0]['type_arguments'] != ['T0'] + or not isinstance(calls[0]['caller_def_id'], int)): + raise ValueError('Zeroed controls require the actual original generic call') + results = [] + restored = False + + def run(label, argv, expected='', *, fresh=False): + log = output / (label + '.log') + command = [sys.executable, '-B', str(ROOT / 'verification/aeneas/control_runner.py'), + 'command'] + if fresh: + command.append('--fresh') + command.extend([str(output / 'commands'), '--', *argv]) + with log.open('wb') as stream: + result = subprocess.run(command, cwd=work, env=environment, + stdout=stream, stderr=subprocess.STDOUT) + diagnostic = log.read_text(errors='replace') + results.append({'case': label, 'command': command, + 'exit_code': result.returncode, 'log': str(log), + 'expected_rejection': expected}) + if expected: + if (result.returncode != 1 or expected not in diagnostic + or re.search(r'error(?:\([^)]*\))?:', diagnostic) is None): + raise ValueError(f'{label} did not fail at its intended audit: {log}') + elif result.returncode != 0: + raise ValueError(f'{label} failed: {log}') + + build = ['lake', '--old', 'build', '+Zerocopy.FunsExternal', + '+Zerocopy.Funs', '+ZeroedAudit'] + audit = ['lake', '--old', 'env', 'lean', '-DwarningAsError=true', probe.name] + required = ['lake', '--old', 'build', '+Required'] + full_audit = ['lake', '--old', 'env', 'lean', '-DwarningAsError=true', 'Check.lean'] + + def restore_sources(): + for path, original in originals.items(): + if path.read_bytes() != original: + path.write_bytes(original) + + def restore_build(label): + restore_sources() + run(label + '-elaboration', build, fresh=True) + run(label + '-audit', audit) + + try: + with probe.open('x') as stream: + stream.write(PROBE) + run('positive-native-elaboration', build, fresh=True) + run('positive-audit', audit) + run('positive-required-elaboration', required, fresh=True) + run('positive-enclosing-premise-audit', full_audit) + + text = originals[external].decode() + signature = ('noncomputable def core.mem.zeroed (T : Type) ' + '[model : AeneasSpecs.RustModel T] : Result T :=\n') + before = signature + ' model.zeroedResult\n' + after = signature + ''' match model.representation with + | none => .fail .undef + | some decoder => Result.ofOption + (decoder.run (List.replicate decoder.byteSize (Rust.Storage.AMByte.init 0))) .undef +''' + if text.count(before) != 1: + raise ValueError('Zeroed interpretation control boundary changed') + external.write_text(text.replace(before, after)) + run('missing-model-guard-elaboration', build, fresh=True) + run('missing-model-guard-rejection', audit, + 'core.mem.zeroed changed its full signature or body') + restore_build('restored-model-guard') + + text = originals[native].decode() + before = ' core.mem.zeroed Self\n' + after = ''' core.mem.zeroed Self (model := { + Model := AeneasSpecs.ModelOf Self, + decode := fun _ => none, + representation := (inferInstance : AeneasSpecs.RustModel Self).representation }) +''' + if text.count(before) != 1: + raise ValueError('Zeroed native default control boundary changed') + native.write_text(text.replace(before, after)) + run('replaced-provider-elaboration', build, fresh=True) + run('replaced-provider-rejection', audit, + 'changed its original type or retained provider') + restore_build('restored-provider') + run('restored-provider-required-elaboration', required, fresh=True) + + mutant = copy.deepcopy(manifest) + calls = mutant['admission']['stages']['llbc']['calls'] + next(row for row in calls if row.get('callee') == 'core::mem::zeroed')[ + 'type_arguments'] = ['T1'] + bindings.write_text(json.dumps(mutant, indent=2) + '\n') + run('lowered-endpoint-rejection', audit, + 'Zeroed changed original Rust type arguments, ownership, or multiplicity') + restore_sources() + run('restored-endpoint-audit', audit) + + mutant = copy.deepcopy(manifest) + mutant['bindings'][owner]['erased_self_bound'] = None + bindings.write_text(json.dumps(mutant, indent=2) + '\n') + run('vanished-enclosing-premise-rejection', full_audit, + 'Unexpected enclosing trait premise on Zerocopy.FromZeros.new_zeroed.default') + restore_sources() + run('restored-enclosing-premise-audit', full_audit) + finally: + restore_sources() + try: + run('restored-native-elaboration', build, fresh=True) + run('restored-positive-audit', audit) + run('restored-required-elaboration', required, fresh=True) + run('restored-positive-full-audit', full_audit) + restored = True + finally: + probe.unlink(missing_ok=True) + (output / 'evidence.json').write_text(json.dumps( + {'restored': restored, 'results': results}, indent=2) + '\n') + + +if __name__ == '__main__': + main() diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index 1497cae629..595b0c449d 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -3820,6 +3820,10 @@ pub unsafe trait FromZeros: TryFromBytes { )] #[must_use = "has no side effects"] #[inline(always)] + /// ```aeneas + /// spec new_zeroed_spec + /// ensures(raw) r => AeneasSpecs.RustModel.zeroedValue r + /// ``` fn new_zeroed() -> Self where Self: Sized,