From f60aa3f791015b3bbc8681fe6c35c9fb91fe8787 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 14 Oct 2026 23:45:34 -0400 Subject: [PATCH] Prove FromZeros::new_zeroed through its enclosing trait law Annotate the production default method and prove that its returned value comes from zero storage and satisfies the retained mathematical decoder. The enclosing FromZeros law supplies the constructor's admission premise, including when Charon removes its unused computational Self dictionary. Keep an independently authored outcome contract which states physical and mathematical decoding directly. Check that the inline specification implies it for any outcome, then apply it to the proved default body. Tests reject failure, divergence and a valid Boolean with the wrong value. Add compiled negative controls for a missing decoder guard, a substituted provider, changed compiler endpoints and a vanished enclosing trait premise. Each mutant must elaborate before the intended audit rejects it. gherrit-pr-id: Gxtqzofwtbtv4xz242wckf27ztdvftifl Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 12 +- verification/aeneas/control_runner.py | 2 +- verification/aeneas/golden/Funs.lean | 2 +- verification/aeneas/golden/Types.lean | 6 +- .../aeneas/lean/Obligations/Zeroed.lean | 37 ++++ verification/aeneas/lean/Proofs/Zeroed.lean | 33 +++ .../lean/RequiredModelContracts/Zeroed.lean | 30 +++ .../aeneas/lean/ZeroedContractTests.lean | 45 ++++ .../aeneas/negative-control-family.sh | 8 +- verification/aeneas/projections/Specs.lean | 9 + .../aeneas/projections/TraitLaws.lean | 6 +- .../aeneas/tests/zeroed_audit_controls.py | 195 ++++++++++++++++++ zerocopy/src/lib.rs | 4 + 13 files changed, 378 insertions(+), 11 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/Zeroed.lean create mode 100644 verification/aeneas/lean/Proofs/Zeroed.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/Zeroed.lean create mode 100644 verification/aeneas/lean/ZeroedContractTests.lean create mode 100644 verification/aeneas/tests/zeroed_audit_controls.py 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,