From 394b6d63ae68bd7f8313647edac7e0d82eb17199 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 15 Oct 2026 12:23:41 -0400 Subject: [PATCH] Prove a generic owned conversion against byte models Add a trait-bounded const helper that consumes Src: IntoBytes and returns Dst: FromBytes after an equal-size post-monomorphization assertion. Use ManuallyDrop and the standard transmute_copy operation. Their Lean interpretations retain the original extracted arguments before adding semantic providers. The helper requires Rust 1.83 to borrow a generic source that may have interior mutability in const evaluation. The production transmute macro remains unchanged. Interpret the copy through both physical decoders and destination model admission. Quantify generic proofs over a checked representation preference, then prove coverage of every represented output while fixing the decoders. This preserves ambiguous source encodings. Admission limits the fragment to one conversion with polymorphic forwarding; independent choices across repeated operations require a richer effect model. Audit original compiler endpoints, constant initializers, exact retained providers, and complete primitive interpretations. Preserve the ordinary ABI size queries and state physical-width correspondence explicitly. The existing ownership checker proves the erased conditional drops empty. Prove the actual helper and a caller that reuses its theorem. Add independent contract expectations and compiled mutation controls for substituted providers, altered primitive models, missing call witnesses, and the size guard. Physical profiles and standard-library semantics remain explicit Rust correspondence premises; this adds no general pointer/resource model. Regenerate UI snapshots on all three pinned compilers for the shifted source line numbers. Their diagnostic text is unchanged. gherrit-pr-id: Gmhd5pbk4jan7lwabm442fdhchwui6nnr Agent-authored-by: AI agent acting on joshlf's behalf --- .github/workflows/ci.yml | 5 + verification/aeneas/README.md | 31 ++ verification/aeneas/SEMANTICS.md | 66 ++++ verification/aeneas/admission.py | 209 +++++++++++- verification/aeneas/control_runner.py | 3 +- verification/aeneas/external.json | 4 +- verification/aeneas/golden/Funs.lean | 56 +++- .../aeneas/golden/FunsExternal_Template.lean | 22 +- verification/aeneas/golden/Types.lean | 5 + verification/aeneas/lean/Check.lean | 2 + verification/aeneas/lean/DeriveModels.lean | 7 +- .../lean/GenericTransmuteContractTests.lean | 61 ++++ verification/aeneas/lean/ModelPrelude.lean | 1 + .../aeneas/lean/NativeProviderAudit.lean | 261 +++++++++++++++ .../lean/Obligations/GenericTransmute.lean | 53 +++ .../aeneas/lean/Proofs/GenericTransmute.lean | 166 ++++++++++ .../GenericTransmute.lean | 46 +++ verification/aeneas/lean/RustModel.lean | 8 + verification/aeneas/lean/TransmuteModel.lean | 301 ++++++++++++++++++ .../aeneas/lean/TransmuteModelTests.lean | 155 +++++++++ .../aeneas/lean/Zerocopy/FunsExternal.lean | 26 ++ .../aeneas/negative-control-family.sh | 7 +- verification/aeneas/prepare.py | 2 +- verification/aeneas/projections/Specs.lean | 18 ++ .../aeneas/projections/TraitLaws.lean | 1 + .../aeneas/tests/test_trait_invariants.py | 62 ++++ .../tests/test_transmute_copy_admission.py | 250 +++++++++++++++ .../tests/transmute_copy_audit_controls.py | 264 +++++++++++++++ verification/aeneas/trait_invariants.py | 10 +- zerocopy/Cargo.toml | 7 + zerocopy/src/util/generic_transmute.rs | 67 ++++ zerocopy/src/util/macro_util.rs | 65 ++++ zerocopy/src/util/mod.rs | 3 + zerocopy/tests/ui/transmute_mut.msrv.stderr | 4 +- .../tests/ui/transmute_mut.nightly.stderr | 40 +-- zerocopy/tests/ui/transmute_mut.stable.stderr | 32 +- zerocopy/tests/ui/transmute_ref.msrv.stderr | 4 +- .../tests/ui/transmute_ref.nightly.stderr | 4 +- zerocopy/tests/ui/transmute_ref.stable.stderr | 4 +- zerocopy/tests/ui/try_transmute.msrv.stderr | 8 +- .../tests/ui/try_transmute.nightly.stderr | 14 +- zerocopy/tests/ui/try_transmute.stable.stderr | 14 +- .../tests/ui/try_transmute_mut.nightly.stderr | 52 +-- .../tests/ui/try_transmute_mut.stable.stderr | 40 +-- .../tests/ui/try_transmute_ref.nightly.stderr | 36 +-- .../tests/ui/try_transmute_ref.stable.stderr | 28 +- 46 files changed, 2362 insertions(+), 162 deletions(-) create mode 100644 verification/aeneas/lean/GenericTransmuteContractTests.lean create mode 100644 verification/aeneas/lean/NativeProviderAudit.lean create mode 100644 verification/aeneas/lean/Obligations/GenericTransmute.lean create mode 100644 verification/aeneas/lean/Proofs/GenericTransmute.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/GenericTransmute.lean create mode 100644 verification/aeneas/lean/TransmuteModel.lean create mode 100644 verification/aeneas/lean/TransmuteModelTests.lean create mode 100644 verification/aeneas/tests/test_transmute_copy_admission.py create mode 100644 verification/aeneas/tests/transmute_copy_audit_controls.py create mode 100644 zerocopy/src/util/generic_transmute.rs diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4365f6e7ea..b7cb33a086 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -85,6 +85,7 @@ jobs: # `build.rs`. Each of these represents the minimum Rust version for # which a particular feature is supported. "no-zerocopy-simd-x86-avx12-1-89-0", + "no-zerocopy-const-refs-to-cell-1-83-0", "no-zerocopy-core-error-1-81-0", "no-zerocopy-slice-ptr-len-1-79-0", "no-zerocopy-diagnostic-on-unimplemented-1-78-0", @@ -119,6 +120,8 @@ jobs: feature_profile: "all" - toolchain: "no-zerocopy-simd-x86-avx12-1-89-0" feature_profile: "all" + - toolchain: "no-zerocopy-const-refs-to-cell-1-83-0" + feature_profile: "all" - toolchain: "no-zerocopy-core-error-1-81-0" feature_profile: "all" - toolchain: "no-zerocopy-slice-ptr-len-1-79-0" @@ -147,6 +150,8 @@ jobs: # zerocopy-derive doesn't behave differently on these toolchains. - crate: "zerocopy-derive" toolchain: "no-zerocopy-simd-x86-avx12-1-89-0" + - crate: "zerocopy-derive" + toolchain: "no-zerocopy-const-refs-to-cell-1-83-0" - crate: "zerocopy-derive" toolchain: "no-zerocopy-core-error-1-81-0" - crate: "zerocopy-derive" diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index f61ff87f51..91f3ef3550 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -1294,3 +1294,34 @@ checking its signature; no formatting proposition or behavior is assumed. A change to a proposition or a function fails the audit. The PhantomData model likewise records its zero runtime fields, with a Lean shape theorem that fails if extraction adds fields; it makes no ownership or provenance claim. + +## Generic owned transmute proof + +The inline specification on [`util::macro_util::transmute_copy`](../../zerocopy/src/util/macro_util.rs) +requires `RustModel.sameSize Src Dst` and guarantees `RustModel.byteCast src result`. +`sameSize` links both ordinary ABI size queries to the physical decoder widths. +`byteCast` says one byte string represents both endpoints; it does not select a +canonical string. Accepted input decoding, termination, non-panicking execution, +and output decoding remain automatic contract obligations. + +[`Proofs/GenericTransmute.lean`](lean/Proofs/GenericTransmute.lean) proves the actual +helper, an independent generic caller, guard retention, and coverage of every +represented outcome. The caller reuses the helper's theorem. The byte proof +combines source initialization and realizability with destination completeness. +An uninhabited source is vacuous, and zero-sized types need no special case. + +Aeneas's ordinary `Result` is deterministic. To cover ambiguous representations, +`RustModel` retains a checked representation preference and generic specifications +quantify over that provider. The coverage theorem varies only the preference, +while fixing both decoders. Tests show that the same raw source can yield two +different byte-observing outputs. Admission permits only one conversion per +execution and generic forwarding that retains that choice. Repetition, loops, +recursion, concrete forwarding, and unreviewed endpoint shapes fail closed. + +CI also audits the compiler call identities, ordered endpoints, exact providers, +constant initializer, and complete external interpretations. The ownership checker +proves the ignored normal and unwind drops empty. Failure controls challenge the +size guard, providers, trait premises, and destination admission. The exact +[semantic scope and Rust premises](SEMANTICS.md#generic-owned-conversion-through-transmute_copy) +exclude pointer provenance, resource ownership, meaningful destructor execution, +and general storage-copy effects. The production `transmute!` macro is unchanged. diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md index 3f0b3863de..6dc550492e 100644 --- a/verification/aeneas/SEMANTICS.md +++ b/verification/aeneas/SEMANTICS.md @@ -256,3 +256,69 @@ bit pattern, contain no padding or pointers, and have no destructor. The promise preservation of padding for general by-value types. The interpretation supplies no general pointer, provenance, allocation, borrowing, or generic trait law, and proves no production `transmute!` macro expansion. + +## Generic owned conversion through `transmute_copy` + +The const helper in `util/macro_util.rs` consumes `Src: IntoBytes`, checks equal +sizes with the real post-monomorphization assertion, wraps the source in +`ManuallyDrop`, and calls the standard `transmute_copy`. Its independent generic +caller in `util/generic_transmute.rs` consumes the helper's contract. Both roots +are extracted and proved in the golden and live builds. The production +`transmute!` macro does not use this helper yet. Rust versions before 1.83 omit +the helper. Although the standard operation has been const since 1.74, borrowing +its generic source requires `const_refs_to_cell`, stabilized in 1.83. `IntoBytes` +guarantees initialized representations but does not require `Immutable`, so the +source may have interior mutability. See the +[Rust stabilization PR](https://github.com/rust-lang/rust/pull/129195). + +Three different facts support the byte proof. `IntoBytes` establishes that all +accepted physical representations are initialized. It also establishes source +realizability: each mathematically admitted source value has some physical +representation. `FromBytes` establishes that every initialized representation of +the destination width admits both a language value and a mathematical value. +Realizability is conditional on a source value, so an uninhabited source remains +vacuous; it does not acquire an arbitrary value or an `Inhabited` requirement. + +`RustModel.sameSize` makes the layout bridge explicit. The ordinary total ABI +queries must return the same `usize`, and both physical decoder widths must +equal that observed size. This is the correspondence premise of the Lean model, +not an additional safety rule imposed on safe Rust callers. The Rust assertion +checks actual sizes; the byte models still need their documented correspondence +to Rust. Existing layout proofs retain their original ABI query interpretation. + +Physical decoding is a relation from a raw value to its accepted byte strings; +it need not provide a unique string. A model's `representationChoice` selects a +preferred string, which is checked before use. Generic contracts universally +quantify that provider. Coverage theorems then vary its preference while fixing +its decoders, proving that every permitted representation and decoded outcome +occurs in the verified family. The public postcondition `byteCast` observes a +common byte string, independently of the preference. Tests exhibit two distinct +destination values for the same raw source. This covers ambiguous source +representations, not nondeterministic decoding of one fixed string. + +The admitted fragment permits at most one conversion per execution, including +unannotated callees and constant initializers. Repeated calls, recursion, loops, +and concrete forwarding that would fix the source preference are rejected. +Supporting them requires an explicit extension of the choice semantics. The +compiled audit checks original type arguments and exact retained providers on +both direct and forwarded calls. Equal Lean carrier types cannot justify +substituting another provider. Identical pure size queries may be shared by +Aeneas; their endpoint bindings remain mandatory, while copy calls retain their +original multiplicity. + +The standard-library boundary supplies `ManuallyDrop`'s layout and bit-validity +identity, destructor suppression, and the equal-width `transmute_copy` behavior +on a valid readable reference. It permits different source and destination +alignments. The ownership checker independently proves all ignored conditional +drops empty, including unwind paths. No meaningful destructor execution, +pointer provenance, allocation ownership, or external resource invariant is +modeled. Destination padding may be forgotten after construction; it is not +promised to retain its input bytes. General typed-copy storage effects remain +deferred: [Aeneas issue #1405](https://github.com/AeneasVerif/aeneas/issues/1405). + +The underlying contracts are recorded in the pinned standard library and the +[versioned `ManuallyDrop` documentation](https://doc.rust-lang.org/1.74.0/core/mem/struct.ManuallyDrop.html) +and [`transmute_copy` documentation](https://doc.rust-lang.org/1.74.0/core/mem/fn.transmute_copy.html). +The numeric, resource-free representation profiles remain the supported domain; +this proof does not admit arbitrary downstream representations merely because a +trait dictionary can be extracted. diff --git a/verification/aeneas/admission.py b/verification/aeneas/admission.py index 46f104e8a9..ffe4936fd7 100644 --- a/verification/aeneas/admission.py +++ b/verification/aeneas/admission.py @@ -91,6 +91,9 @@ # Calls to them are rejected; the generated interface definitions return undef. INTERFACE_ONLY_VALIDATORS = '{impl zerocopy::TryFromBytes for _}::is_safe' INTERFACE_ONLY_TYPES = ('zerocopy::pointer::ptr::def::Ptr',) +MANUALLY_DROP = 'core::mem::manually_drop::ManuallyDrop' +MANUALLY_DROP_NEW = 'core::mem::manually_drop::{' + MANUALLY_DROP + '}::new' +TRANSMUTE_COPY = 'core::mem::transmute_copy' def digest(path): @@ -240,6 +243,11 @@ def ty_name(self, ty, *, check_carrier=True): if tag == 'Adt': base = self.name(self.types[body['id']]['item_meta']['name']) args = body['generics']['types'] + if check_carrier and base == MANUALLY_DROP: + arguments = body['generics'] + if (len(args) != 1 or any(arguments.get(key) for key in + ('regions', 'const_generics', 'trait_refs'))): + raise ValueError('Unreviewed opaque value carrier ManuallyDrop type arguments') if body['generics']['const_generics']: raise ValueError('Nominal const-generic value carriers are unsupported') if check_carrier: @@ -273,6 +281,20 @@ def check_type(self, index): declaration = self.types[index] kind, body = variant(declaration['kind']) name = self.name(declaration['item_meta']['name']) + if name == MANUALLY_DROP: + meta = declaration['item_meta'] + generics = declaration.get('generics', {}) + if (kind != 'Opaque' or meta.get('is_local') is not False + or meta.get('is_extern') is not False + or meta.get('has_errors') is not False + or meta.get('lang_item') != 'ManuallyDrop' + or len(generics.get('types', [])) != 1 + or generics['types'][0]['index'] != 0 + or any(generics.get(key) for key in ('regions', + 'const_generics', 'trait_clauses', 'regions_outlive', + 'types_outlive', 'trait_type_constraints'))): + raise ValueError('Unreviewed opaque value carrier ManuallyDrop shape') + return if kind == 'Opaque': if name not in {'tuple0', 'str', 'core::fmt::Arguments', 'core::fmt::Formatter', 'core::marker::PhantomData', @@ -354,6 +376,30 @@ def visit(self, index): matches[0].get('interpretation_extension') != 'retained-model-provider-v1' or meta['is_local']): raise ValueError('Zeroed construction changed its reviewed model-provider boundary') + if name == 'core::mem::size_of' and (meta['is_local'] or function['body'] != 'Opaque'): + raise ValueError('Size read changed its reviewed ABI boundary') + if name in {MANUALLY_DROP_NEW, TRANSMUTE_COPY}: + extension = ('nominal-wrapper-constructor-v1' if name == MANUALLY_DROP_NEW + else 'retained-model-byte-copy-v1') + generics = function['generics'] + regions = generics['regions'] + expected = ({'unsafe': False, 'inputs': ['T0'], + 'output': MANUALLY_DROP + '', 'types': 1, 'consts': 0} + if name == MANUALLY_DROP_NEW else + {'unsafe': True, 'inputs': ['&T0'], 'output': 'T1', + 'types': 2, 'consts': 0}) + expected_lean = ('core.mem.manually_drop.ManuallyDrop.new' + if name == MANUALLY_DROP_NEW else 'core.mem.transmute_copy') + if (prototype != expected or matches[0]['lean'] != expected_lean + or matches[0].get('interpretation_extension') != extension + or meta['is_local'] or function['body'] != 'Opaque' + or len(regions) != (1 if name == TRANSMUTE_COPY else 0) + or [ty['index'] for ty in generics['types']] != + list(range(prototype['types'])) + or (regions and regions[0]['index'] != 0) + or any(generics[key] for key in ('const_generics', + 'trait_clauses', 'regions_outlive', 'trait_type_constraints'))): + raise ValueError('Transmute-copy reviewed external boundary changed') # A builtin may replace a visible Rust body. Always select the # interpretation first, rather than approving the unused body. self.visited[index] = {'rust': name, 'origin': 'interpretation', @@ -461,7 +507,7 @@ def place(self, place, indexed=False): if body not in self.locals: raise ValueError('Unknown local place') elif tag == 'Global': - self.global_value(body['id']) + self.global_value(body['id'], body['generics']) elif tag == 'Projection': self.place(body[0], indexed) projection, detail = variant(body[1]) @@ -483,14 +529,22 @@ def place(self, place, indexed=False): else: raise ValueError(f'Unsupported place {tag}') - def global_value(self, index): + def global_value(self, index, arguments): + global_ = self.crate['global_decls'][index] + value, _ = untag(global_['value']) + tag, producer = variant(value) + if tag == 'Call': + function, _ = producer + kind, callee = variant(function['kind']) + if kind != 'Fun': + raise ValueError('Unresolved global initializer') + self.record_native_call(callee, arguments, kind='global') if index in self.globals: return self.globals.add(index) - global_ = self.crate['global_decls'][index] if global_['global_kind'] != 'NamedConst' or global_['item_meta']['has_errors']: raise ValueError('Unreviewed static or global origin') - self.constant(global_['value']) + self.constant(global_['value'], record_call=False) def operand(self, operand): tag, body = variant(operand) @@ -501,7 +555,17 @@ def operand(self, operand): else: raise ValueError(f'Unsupported operand {tag}') - def constant(self, constant): + def record_native_call(self, callee, arguments, **extra): + fields(arguments, 'regions types const_generics trait_refs') + target = self.functions[callee] + row = {'caller': self.current, 'callee': self.name(target['item_meta']['name']), + 'caller_def_id': self.current_function['def_id'], + 'callee_def_id': callee, + 'type_arguments': [self.ty_name(ty) for ty in arguments['types']], **extra} + self.calls.append(row) + return row + + def constant(self, constant, *, record_call=True): value, ty = untag(constant) self.ty_name(ty) tag, body = variant(value) @@ -516,7 +580,7 @@ def constant(self, constant): self.constant(field) return if tag == 'Global': - self.global_value(body['id']) + self.global_value(body['id'], body['generics']) return if tag == 'Call': function, args = body @@ -524,6 +588,9 @@ def constant(self, constant): raise ValueError('Unresolved constant producer') for arg in args: self.constant(arg) + if record_call: + self.record_native_call(function['kind']['Fun'], function['generics'], + kind='constant') self.visit(function['kind']['Fun']) return if tag == 'TraitConst': @@ -891,7 +958,24 @@ def block(self, block, unwind=False): 'usize', 'core::num::niche_types::NonZeroUsizeInner'] if actual != expected: raise ValueError(f'Unsupported NonZero::new_unchecked instantiation {actual}') - call_evidence = {'caller': self.current, 'callee': name} + arguments = fn['generics'] + fields(arguments, 'regions types const_generics trait_refs') + actual = [self.ty_name(ty) for ty in arguments['types']] + call_evidence = {'caller': self.current, 'callee': name, + 'caller_def_id': self.current_function['def_id'], + 'callee_def_id': callee, 'type_arguments': actual} + if name == MANUALLY_DROP_NEW and (actual != ['T0'] or + any(arguments[key] for key in + ('regions', 'const_generics', 'trait_refs'))): + raise ValueError('Unsupported original ManuallyDrop constructor endpoint') + if name == TRANSMUTE_COPY: + regions = arguments['regions'] + if (actual != [MANUALLY_DROP + '', 'T1'] + or len(regions) != 1 + or variant(regions[0])[0] != 'Body' + or type(variant(regions[0])[1]) is not int + or arguments['const_generics'] or arguments['trait_refs']): + raise ValueError('Unsupported original transmute_copy endpoints or regions') if name == 'core::mem::zeroed': arguments = fn['generics'] if (len(arguments['types']) != 1 or arguments['regions'] @@ -1019,9 +1103,115 @@ def audit(self, roots): if self.name(trait['item_meta']['name']) not in self.law_traits: continue self.audit_implementation(implementation, trait) + self.audit_copy_closures() return {'roots': sorted(roots), 'executions': list(self.visited.values()), 'calls': self.calls, 'empty_drops': list(self.empty_drops.values())} + def audit_copy_closures(self): + """Bound each invocation to one byte choice, including helper calls. + + Count the syntactic call multigraph, not just distinct callees. Loops + and recursion in an owner which can reach copy can repeat a choice; + unrelated numerical loops retain their existing admission rules. + """ + copy_name = [{'Ident': [part, 0]} for part in TRANSMUTE_COPY.split('::')] + copies = {ident for ident, function in self.functions.items() + if function['item_meta']['name'] == copy_name} + if not copies: + return + edges = {} + for row in self.calls: + if 'callee_def_id' in row: + edges.setdefault(row['caller_def_id'], []).append(row['callee_def_id']) + reaching = set(copies) + while True: + added = {owner for owner, children in edges.items() + if any(child in reaching for child in children)} - reaching + if not added: + break + reaching.update(added) + # A fixed concrete instantiation would select a default provider rather + # than retaining the caller's universally quantified byte choice. Every + # local forwarding edge must therefore pass original type variables. + # The primitive's nominal ManuallyDrop endpoint is checked separately. + for row in self.calls: + owner, child = row.get('caller_def_id'), row.get('callee_def_id') + if child not in reaching - copies: + continue + arguments = row.get('type_arguments') + source_indices = {parameter['index'] for parameter in + self.functions[owner]['generics']['types']} + if not isinstance(arguments, list) or not arguments or any( + not isinstance(argument, str) or + (match := re.fullmatch(r'T(0|[1-9][0-9]*)', argument)) is None or + int(match[1]) not in source_indices for argument in arguments): + raise ValueError('Transmute-copy forwarding requires original type variables') + counts, active = {}, set() + + def count(owner): + if owner in active: + raise ValueError('Transmute-copy closure contains recursive calls') + if owner in counts: + return counts[owner] + if owner in copies: + return 1 + active.add(owner) + total = sum(count(child) for child in edges.get(owner, []) + if child in reaching) + active.remove(owner) + if total > 1: + raise ValueError('Transmute-copy closure contains multiple byte choices') + counts[owner] = total + return total + + def structured_loop(value): + if isinstance(value, dict): + if set(value) == {'Loop'}: + return True + return any(structured_loop(child) for child in value.values()) + return isinstance(value, list) and any(map(structured_loop, value)) + + for owner in reaching - copies: + count(owner) + if not self.functions[owner]['generics']['types']: + raise ValueError('Transmute-copy local bodies must be type generic') + stage, body = variant(self.functions[owner]['body']) + if stage == 'Structured': + if structured_loop(body['body']): + raise ValueError('Transmute-copy closure contains a body loop') + elif stage == 'Unstructured': + blocks = body['body'] + graph = {} + for index, block in enumerate(blocks): + tag, term = variant(block['terminator']['kind']) + if tag == 'Goto': + children = [term] + elif tag == 'Switch': + children = term['branches'] + elif tag in {'Call', 'Drop', 'Assert'}: + children = [term['target'], term['on_unwind']] + else: + children = [] + if any(type(child) is not int or not 0 <= child < len(blocks) + for child in children): + raise ValueError('Invalid transmute-copy control-flow edge') + graph[index] = children + seen, pending = set(), set() + + def visit(block): + if block in pending: + raise ValueError('Transmute-copy closure contains a CFG cycle') + if block in seen: + return + pending.add(block) + for child in graph[block]: + visit(child) + pending.remove(block) + seen.add(block) + + for block in graph: + visit(block) + def input_identity(root): """Bind inspection to source, build configuration, and the patched runtime. @@ -1181,6 +1371,11 @@ def check_translation(work, evidence): text = (work / 'Zerocopy/FunsExternal_Template.lean').read_text() signatures = { 'core.mem.zeroed': 'axiom core.mem.zeroed (T : Type) : Result T', + 'core.mem.size_of': 'axiom core.mem.size_of (T : Type) : Result Std.Usize', + 'core.mem.manually_drop.ManuallyDrop.new': + 'axiom core.mem.manually_drop.ManuallyDrop.new {T : Type} : T → Result (core.mem.manually_drop.ManuallyDrop T)', + 'core.mem.transmute_copy': + 'axiom core.mem.transmute_copy {Src : Type} (Dst : Type) : Src → Result Dst', 'core.intrinsics.transmute': 'axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst', 'util.transmute_unchecked': diff --git a/verification/aeneas/control_runner.py b/verification/aeneas/control_runner.py index cda73c5405..e2d46c7d65 100644 --- a/verification/aeneas/control_runner.py +++ b/verification/aeneas/control_runner.py @@ -29,7 +29,8 @@ FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi', 'contracts', 'dependencies', 'admission', 'semantics', 'owned-std') MODELS = ('golden-verification', 'verification') -FIXTURES = ('StdTransmuteAuditProbe.lean', 'ZeroedAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean', +FIXTURES = ('StdTransmuteAuditProbe.lean', 'ZeroedAuditProbe.lean', + 'TransmuteCopyAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean', 'RoundingConstructorControl.lean', 'RoundingDomainControl.lean', 'Zerocopy/ScopeControl.lean', 'Zerocopy/ShapeControl.lean', 'Zerocopy/ModelControl.lean', 'Proofs/WitnessOwnerControl.lean', diff --git a/verification/aeneas/external.json b/verification/aeneas/external.json index f94eec62ef..15f7c33aef 100644 --- a/verification/aeneas/external.json +++ b/verification/aeneas/external.json @@ -38,5 +38,7 @@ {"rust": "core::clone::impls::{core::clone::Clone}::clone", "signature": {"unsafe": false, "inputs": ["&usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "core.clone.CloneUsize"}, {"rust": "core::num::niche_types::{core::clone::Clone}::clone", "signature": {"unsafe": false, "inputs": ["&core::num::niche_types::NonZeroUsizeInner"], "output": "core::num::niche_types::NonZeroUsizeInner", "types": 0, "consts": 0}, "lean": "core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone"}, {"rust": "core::intrinsics::transmute", "signature": {"unsafe": true, "inputs": ["T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "core.intrinsics.transmute", "interpretation_extension": "closed-implicit-owned-provider-v1", "providers": {"u32->[u8;4]": "Zerocopy.stdTransmuteU32ToBytes", "[u8;4]->u32": "Zerocopy.stdTransmuteBytesToU32", "u8->bool": "Zerocopy.stdTransmuteU8ToBool"}}, - {"rust": "core::mem::zeroed", "signature": {"unsafe": true, "inputs": [], "output": "T0", "types": 1, "consts": 0}, "lean": "core.mem.zeroed", "interpretation_extension": "retained-model-provider-v1"} + {"rust": "core::mem::zeroed", "signature": {"unsafe": true, "inputs": [], "output": "T0", "types": 1, "consts": 0}, "lean": "core.mem.zeroed", "interpretation_extension": "retained-model-provider-v1"}, + {"rust": "core::mem::manually_drop::{core::mem::manually_drop::ManuallyDrop}::new", "signature": {"unsafe": false, "inputs": ["T0"], "output": "core::mem::manually_drop::ManuallyDrop", "types": 1, "consts": 0}, "lean": "core.mem.manually_drop.ManuallyDrop.new", "interpretation_extension": "nominal-wrapper-constructor-v1"}, + {"rust": "core::mem::transmute_copy", "signature": {"unsafe": true, "inputs": ["&T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "core.mem.transmute_copy", "interpretation_extension": "retained-model-byte-copy-v1"} ] diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 221b1ee780..c36ccf7fde 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 269:0-287:1 -/ + Source: 'src/util/mod.rs', lines 272:0-290: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 177:0-237:1 -/ + Source: 'src/util/mod.rs', lines 180:0-240: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 313:0-319:1 -/ + Source: 'src/util/mod.rs', lines 316:0-322: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 297:0-303:1 -/ + Source: 'src/util/mod.rs', lines 300:0-306:1 -/ def util.max (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) @@ -3818,6 +3818,42 @@ def util.checks.check_arithmetic massert (i3 = i4) else ok () +/-- [zerocopy::util::macro_util::transmute_copy::{impl zerocopy::util::macro_util::transmute_copy::StaticAssert for (core::marker::PhantomData, core::marker::PhantomData)}::ASSERT] + Source: 'src/util/macros.rs', lines 685:12-688:14 -/ +@[global_simps, irreducible] +def + PairPhantomDataPhantomData.Insts.ZerocopyUtilMacro_utilTransmute_copyStaticAssert.ASSERT + (Src : Type) (Dst : Type) : Result Bool := do + let i ← core.mem.size_of Src + let i1 ← core.mem.size_of Dst + massert (i = i1) + ok (i = i1) + +/-- [zerocopy::util::macro_util::transmute_copy]: + Source: 'src/util/macro_util.rs', lines 557:0-576:1 + Visibility: public -/ +native_models def util.macro_util.transmute_copy + {Src : Type} {Dst : Type} (IntoBytesInst : IntoBytes Src) (FromBytesInst : + FromBytes Dst) (src : Src) : + Result Dst + := do + let b ← + PairPhantomDataPhantomData.Insts.ZerocopyUtilMacro_utilTransmute_copyStaticAssert.ASSERT + Src + Dst + massert b + let src1 ← core.mem.manually_drop.ManuallyDrop.new src + core.mem.transmute_copy Dst src1 + +/-- [zerocopy::util::generic_transmute::transmute_copy_caller]: + Source: 'src/util/generic_transmute.rs', lines 22:0-24:1 -/ +native_models def util.generic_transmute.transmute_copy_caller + {Src : Type} {Dst : Type} (IntoBytesInst : IntoBytes Src) (FromBytesInst : + FromBytes Dst) (src : Src) : + Result Dst + := do + util.macro_util.transmute_copy IntoBytesInst FromBytesInst src + /-- [zerocopy::impls::_::{impl zerocopy::FromZeros for ()}::only_derive_is_allowed_to_implement_this_trait]: Source: 'src/util/macros.rs', lines 165:8-165:62 Visibility: public -/ @@ -5033,6 +5069,18 @@ def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst : IntoBytesInst } +/-- Trait implementation: [zerocopy::util::macro_util::transmute_copy::{impl zerocopy::util::macro_util::transmute_copy::StaticAssert for (core::marker::PhantomData, core::marker::PhantomData)}] + Source: 'src/util/macros.rs', lines 684:8-689:9 -/ +@[reducible] +def + PairPhantomDataPhantomData.Insts.ZerocopyUtilMacro_utilTransmute_copyStaticAssert + (Src : Type) (Dst : Type) : util.macro_util.transmute_copy.StaticAssert + ((core.marker.PhantomData Src) × (core.marker.PhantomData Dst)) := { + ASSERT := + PairPhantomDataPhantomData.Insts.ZerocopyUtilMacro_utilTransmute_copyStaticAssert.ASSERT + Src Dst +} + /-- [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 diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index 4dd18d1124..bcb41c4a7f 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -35,6 +35,15 @@ open Zerocopy @[rust_fun "core::intrinsics::transmute"] axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst +/-- [core::mem::manually_drop::{core::mem::manually_drop::ManuallyDrop}::new]: + Source: '/rustc/library/core/src/mem/manually_drop.rs', lines 180:4-180:49 + Name pattern: [core::mem::manually_drop::{core::mem::manually_drop::ManuallyDrop<@T>}::new] + Visibility: public -/ +@[rust_fun + "core::mem::manually_drop::{core::mem::manually_drop::ManuallyDrop<@T>}::new"] +axiom core.mem.manually_drop.ManuallyDrop.new + {T : Type} : T → Result (core.mem.manually_drop.ManuallyDrop T) + /-- [core::mem::size_of]: Source: '/rustc/library/core/src/mem/mod.rs', lines 375:0-375:34 Name pattern: [core::mem::size_of] @@ -55,6 +64,13 @@ axiom core.mem.align_of (T : Type) : Result Std.Usize Visibility: public -/ @[rust_fun "core::mem::zeroed"] axiom core.mem.zeroed (T : Type) : Result T +/-- [core::mem::transmute_copy]: + Source: '/rustc/library/core/src/mem/mod.rs', lines 1145:0-1145:70 + Name pattern: [core::mem::transmute_copy] + Visibility: public -/ +@[rust_fun "core::mem::transmute_copy"] +axiom core.mem.transmute_copy {Src : Type} (Dst : Type) : Src → Result Dst + /-- [core::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}::clone]: Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22 Name pattern: [core::num::niche_types::{core::clone::Clone}::clone] @@ -116,12 +132,12 @@ axiom core.num.Usize.unchecked_mul : Std.Usize → Std.Usize → Result Std.Usize /-- [zerocopy::util::copy_unchecked]: - Source: 'src/util/mod.rs', lines 331:0-346:1 -/ + Source: 'src/util/mod.rs', lines 334:0-349: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 360:0-371:1 -/ + Source: 'src/util/mod.rs', lines 363:0-374:1 -/ axiom util.copy_unchecked_at : Slice Std.U8 → Slice Std.U8 → Std.Usize → Result (Slice Std.U8) @@ -182,7 +198,7 @@ axiom Array.Insts.ZerocopyTryFromBytes.is_safe Bool /-- [zerocopy::util::transmute_unchecked]: - Source: 'src/util/mod.rs', lines 383:0-412:1 -/ + Source: 'src/util/mod.rs', lines 386:0-415:1 -/ axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst /-- [zerocopy::util::validity::read_byte]: diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 2b8e48c0a6..90bb560955 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -378,4 +378,9 @@ structure trait_checks.Forward (C : Type) where structure wrappers.Unalign (T : Type) where _0 : T +/-- Trait declaration: [zerocopy::util::macro_util::transmute_copy::StaticAssert] + Source: 'src/util/macros.rs', lines 679:8-681:9 -/ +structure util.macro_util.transmute_copy.StaticAssert (Self : Type) where + ASSERT : Result Bool + end Zerocopy diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean index eacf3aa11e..e461e876b6 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -8,6 +8,7 @@ those terms. -/ import Required import ZeroedAudit +import NativeProviderAudit open Lean Elab Command /-! @@ -434,6 +435,7 @@ run_elab do throwError "Execution admission roots disagree with the function binding table" auditStdTransmute bindings auditZeroed bindings + auditNativeProviders bindings let some typesModule := env.getModuleIdx? `Zerocopy.Types | throwError "Raw extracted types must be imported" let some shapesModule := env.getModuleIdx? `ModelShapes diff --git a/verification/aeneas/lean/DeriveModels.lean b/verification/aeneas/lean/DeriveModels.lean index 8315482c12..f5bf63be97 100644 --- a/verification/aeneas/lean/DeriveModels.lean +++ b/verification/aeneas/lean/DeriveModels.lean @@ -509,8 +509,13 @@ private meta def deriveProvider (raw : Name) (count : Nat) (ty.getAppArgs.map some)) mkLambdaFVars #[value] (mkAppN ctor values) mkAppOptM ``wrapperRepresentation #[some fieldTy, some rawTy, some child, some wrap] + -- Constructor application does not insert the defaults used by structure + -- syntax. Supply the empty preference explicitly so generated providers + -- contain no unresolved choice metavariable. + let choice := mkLambda `_raw .default rawTy + (mkApp (mkConst ``List.nil [.zero]) (mkConst ``Rust.Storage.AMByte)) let provider ← mkAppOptM ``RustModel.mk #[some rawTy, some modelTy, - some (mkAppN (mkConst b.decoder levels) all), some representation] + some (mkAppN (mkConst b.decoder levels) all), some representation, some choice] addDefinition b.provider info.levelParams (← mkLambdaFVars all provider) setReducibilityStatus b.provider .reducible addInstance b.provider .global 1000 diff --git a/verification/aeneas/lean/GenericTransmuteContractTests.lean b/verification/aeneas/lean/GenericTransmuteContractTests.lean new file mode 100644 index 0000000000..01beb99609 --- /dev/null +++ b/verification/aeneas/lean/GenericTransmuteContractTests.lean @@ -0,0 +1,61 @@ +/- 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 RequiredModelContracts.GenericTransmute +public import Proofs.GenericTransmute +import all Proofs.GenericTransmute +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace Zerocopy.Proofs + +check_contract Obligations.transmute_copy_spec using transmute_copy_spec +check_contract Obligations.transmute_copy_caller_spec using transmute_copy_caller_spec + +section +variable {Src Dst : Type} (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst] + [sourceLaw : @TraitLaws.into_bytes_initialized Src source ms] + [destinationLaw : @TraitLaws.from_bytes_valid Dst destination md] + [zeroLaw : @TraitLaws.from_zeros_valid Dst destination.FromZerosInst md] + (mathSrc : ms.Model) (decoded : ms.decode src = some mathSrc) + (width : Usize) (sourceSize : core.mem.size_of Src = .ok width) + (destinationSize : core.mem.size_of Dst = .ok width) + (sourceWidth : ms.representation.map (·.byteSize) = some width.val) + (destinationWidth : md.representation.map (·.byteSize) = some width.val) + +example (error : Error) : + ¬ Obligations.transmute_copy_spec_contract Src Dst source destination src ms md (.fail error) := by + intro expected + obtain ⟨raw, _, executed, _⟩ := expected mathSrc decoded + ⟨width, sourceSize, destinationSize, sourceWidth, destinationWidth⟩ + simp at executed + +example : + ¬ Obligations.transmute_copy_caller_spec_contract Src Dst source destination src ms md .div := by + intro expected + obtain ⟨raw, _, executed, _⟩ := expected mathSrc decoded + ⟨width, sourceSize, destinationSize, sourceWidth, destinationWidth⟩ + simp at executed + +-- Even an admitted output is insufficient when it cannot share source bytes. +example (wrong : Dst) (mathWrong : md.Model) (_admitted : md.decode wrong = some mathWrong) + (noShared : ∀ (bytes : List AMByte) (sd : BitDecoder Src) (dd : BitDecoder Dst), + ms.representation = some sd → md.representation = some dd → + sd.run bytes = some src → dd.run bytes ≠ some wrong) : + ¬ Obligations.transmute_copy_spec_contract Src Dst source destination src ms md (.ok wrong) := by + intro expected + obtain ⟨raw, _, executed, _, bytes, sd, dd, hs, hd, sourcePhysical, destinationPhysical⟩ := + expected mathSrc decoded ⟨width, sourceSize, destinationSize, sourceWidth, destinationWidth⟩ + have equal : wrong = raw := by simpa using executed + subst raw + exact noShared bytes sd dd hs hd sourcePhysical destinationPhysical +end + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/ModelPrelude.lean b/verification/aeneas/lean/ModelPrelude.lean index 065d4305ce..60239e648f 100644 --- a/verification/aeneas/lean/ModelPrelude.lean +++ b/verification/aeneas/lean/ModelPrelude.lean @@ -65,6 +65,7 @@ theorem initializedWrapperRepresentation {A B : Type} [ma : RustModel A] Model := ma.Model decode raw := ma.decode raw.value representation := wrapperRepresentation core.mem.manually_drop.ManuallyDrop.mk + representationChoice raw := ma.representationChoice raw.value @[reducible] instance modelCell (T : Type) [ma : RustModel T] : RustModel (core.cell.Cell T) where diff --git a/verification/aeneas/lean/NativeProviderAudit.lean b/verification/aeneas/lean/NativeProviderAudit.lean new file mode 100644 index 0000000000..118eb95221 --- /dev/null +++ b/verification/aeneas/lean/NativeProviderAudit.lean @@ -0,0 +1,261 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Zerocopy.Funs +public import DeriveModels +public meta import Lean +public section + +/-! +An extracted function can receive more than one mathematical interpretation of +the same Lean type. Checking that a provider has the right *type* would therefore +miss a caller that passes the destination's interpretation for the source. + +This audit follows each provider-bearing call back to its compiler identity and +ordered Rust type arguments. It compares the actual type variables and provider +expressions, before reducing them. The static assertion's global initializer is +also a function: omitting it would leave its size queries unaudited. + +Only the type expressions exercised by these native calls are supported here. +A new expression needs an explicit extension; it cannot fall back to equality +of erased Lean carriers. Functional proofs and this binding audit serve different +purposes: a proof about the wrong provider can be perfectly valid Lean. +-/ + +open Lean Meta Elab AeneasSpecs + +private meta def boundaryDefinition (declName : Name) (expected : TSyntax `term) + (binders : Array BinderInfo) : TermElabM Unit := do + let body ← Term.elabTerm expected none + Term.synthesizeSyntheticMVarsNoPostponing + let body ← instantiateMVars body + let some (.defnInfo actual) := (← getEnv).find? declName + | throwError "Byte-copy boundary {declName} must be a definition" + unless actual.levelParams.isEmpty && (← isDefEq actual.type (← inferType body)) && + (← isDefEq actual.value body) do + throwError "Byte-copy boundary {declName} changed its whole signature or interpretation" + forallTelescope actual.type fun inputs _ => do + let actualBinders ← inputs.mapM fun input => return (← input.fvarId!.getDecl).binderInfo + unless actualBinders == binders do + throwError "Byte-copy boundary {declName} changed its argument binders" + +private meta def providerAt (raw : Expr) (params models : Array Expr) : MetaM Expr := + boundModelProvider raw params models + +private meta partial def originalType (text : String) (params : Array Expr) : MetaM Expr := do + if text.startsWith "T" then + if let some index := (text.drop 1).toString.toNat? then + if let some rawTy := params[index]? then return rawTy + if text == "usize" then return mkConst ``Aeneas.Std.Usize + if text == "u32" then return mkConst ``Aeneas.Std.U32 + let wrapper := "core::mem::manually_drop::ManuallyDrop<" + if text.startsWith wrapper && text.endsWith ">" then + let child := ((text.drop wrapper.length).toString.dropEnd 1).toString + return mkApp (mkConst ``core.mem.manually_drop.ManuallyDrop) (← originalType child params) + throwError "Unsupported original type expression in provider-bearing call: {text}" + +private meta partial def callsTo (names : Array Name) (expression : Expr) : Array Expr := + if expression.getAppFn.isConst && names.contains expression.getAppFn.constName! then + #[expression] ++ expression.getAppArgs.foldl + (fun calls arg => calls ++ callsTo names arg) #[] + else + match expression with + | .app fn arg => callsTo names fn ++ callsTo names arg + | .lam _ ty body _ | .forallE _ ty body _ => callsTo names ty ++ callsTo names body + | .letE _ ty value body _ => + callsTo names ty ++ callsTo names value ++ callsTo names body + | .mdata _ body | .proj _ _ body => callsTo names body + | _ => #[] + +private meta def typeInputs (inputs : Array Expr) : MetaM (Array Expr) := + inputs.filterM fun input => do + match ← whnf (← inferType input) with + | .sort level => return !level.isZero + | _ => return false + +private meta def jsonArray (json : Json) (key : String) : MetaM (Array Json) := do + let .ok value := json.getObjValAs? (Array Json) key + | throwError "Native provider audit lacks {key}" + return value + +private meta def jsonNat (json : Json) (key : String) : MetaM Nat := do + let .ok value := json.getObjValAs? Nat key + | throwError "Native provider audit lacks numeric {key}" + return value + +private meta def jsonName (json : Json) : MetaM Name := do + let .ok value := json.getObjValAs? String "lean_name" + | throwError "Native provider audit lacks compiled name" + return value.toName + +/-- Match every retained provider, including those forwarded through constants +and ordinary callers. Missing, extra, duplicated, or reordered calls fail. -/ +meta def auditNativeProviders (bindings : Json) : TermElabM Unit := do + let env ← getEnv + let carrier := ``core.mem.manually_drop.ManuallyDrop + let some shape := getStructureInfo? env carrier + | throwError "ManuallyDrop must retain its nominal stored-value carrier" + let .inductInfo carrierInfo ← getConstInfo carrier + | throwError "ManuallyDrop must retain its nominal stored-value carrier" + unless carrierInfo.levelParams.isEmpty && carrierInfo.numParams == 1 && + carrierInfo.numIndices == 0 && carrierInfo.ctors == [carrier ++ `mk] && + shape.fieldNames == #[`value] do + throwError "ManuallyDrop changed its stored-value carrier" + boundaryDefinition `AeneasSpecs.modelManuallyDrop + (← `(fun (T : Type) [child : AeneasSpecs.RustModel T] => + ({ Model := child.Model, «decode» := fun raw => child.decode raw.value, + representation := child.representation.map + (fun decoder => decoder.map core.mem.manually_drop.ManuallyDrop.mk), + representationChoice := fun raw => child.representationChoice raw.value } : + AeneasSpecs.RustModel (core.mem.manually_drop.ManuallyDrop T)))) + #[.default, .instImplicit] + -- A native constructor and its nominal carrier preserve the payload. None + -- of these definitions grants permission to read a dropped payload. + boundaryDefinition `core.mem.manually_drop.ManuallyDrop.new + (← `(fun {T : Type} (src : T) => + (Aeneas.Std.Result.ok (core.mem.manually_drop.ManuallyDrop.mk src)))) + #[.implicit, .default] + boundaryDefinition `core.mem.transmute_copy + (← `(fun {Src : Type} (Dst : Type) (src : Src) + [source : AeneasSpecs.RustModel Src] [destination : AeneasSpecs.RustModel Dst] => + source.transmuteCopyResult destination src)) + #[.implicit, .default, .default, .instImplicit, .instImplicit] + boundaryDefinition `AeneasSpecs.RustModel.sameSize + (← `(fun (Src Dst : Type) [source : AeneasSpecs.RustModel Src] + [destination : AeneasSpecs.RustModel Dst] => + ∃ width : Aeneas.Std.Usize, + core.mem.size_of Src = .ok width ∧ core.mem.size_of Dst = .ok width ∧ + source.representation.map (·.byteSize) = some width.val ∧ + destination.representation.map (·.byteSize) = some width.val)) + #[.default, .default, .instImplicit, .instImplicit] + let .ok admission := bindings.getObjVal? "admission" + | throwError "Native provider audit requires compiler admission" + let .ok stages := admission.getObjVal? "stages" + | throwError "Native provider audit requires both compiler stages" + let .ok before := stages.getObjVal? "before" + | throwError "Native provider audit lacks original compiler stage" + let .ok lowered := stages.getObjVal? "llbc" + | throwError "Native provider audit lacks final compiler stage" + let beforeCalls ← jsonArray before "calls" + let loweredCalls ← jsonArray lowered "calls" + let text ← IO.FS.readFile "Zerocopy/translation.json" + let .ok native := Json.parse text | throwError "Invalid native provider map" + let functions ← jsonArray native "functions" + let globals ← jsonArray native "globals" + let snapshot ← IO.FS.readFile "zerocopy.llbc" + let .ok snapshot := Json.parse snapshot | throwError "Invalid compiler provider snapshot" + let .ok crate := snapshot.getObjVal? "translated" + | throwError "Missing compiler provider crate" + let globalDecls ← jsonArray crate "global_decls" + let mut owners : Array (Nat × Name) := #[] + let mut targets : Array (Nat × Name) := #[] + for row in functions do + let compiledName ← jsonName row + let ident ← jsonNat row "def_id" + let .ok isOpaque := row.getObjValAs? Bool "is_opaque" + | throwError "Native provider owner lacks its body disposition" + -- Opaque rows name upstream templates, which need not be emitted at that + -- name in our handwritten external module. Their complete interpretations + -- have separate audits. Only these reviewed primitive endpoints seed + -- semantic capture; every emitted native body is inspected below. + if isOpaque && !#[`core.mem.zeroed, `core.mem.transmute_copy, + `core.mem.size_of].contains compiledName then continue + if !isOpaque then owners := owners.push (ident, compiledName) + let info ← getConstInfo compiledName + let semantic ← forallTelescope info.type fun inputs _ => do + return (← splitNativeModels inputs).2.size + if semantic > 0 || compiledName == `core.mem.size_of then + targets := targets.push (ident, compiledName) + for row in globals do + let globalId ← jsonNat row "def_id" + let compiledName ← jsonName row + let matching := globalDecls.filter fun declaration => + declaration.getObjValAs? Nat "def_id" == .ok globalId + unless matching.size == 1 do throwError "Global initializer has no unique compiler owner" + -- A Charon named constant stores its initializer as a typed constant call, + -- rather than exposing the initializer in Aeneas's function inventory. + let initializer := do + let value ← matching[0]!.getObjVal? "value" + let typed ← value.getObjValAs? (Array Json) "Untagged" + let call ← typed[0]!.getObjValAs? (Array Json) "Call" + let kind ← call[0]!.getObjVal? "kind" + kind.getObjValAs? Nat "Fun" + let .ok ident := initializer + | throwError "Native global has no supported compiler initializer" + owners := owners.push (ident, compiledName) + let (semantic, parameterCount) ← forallTelescope (← getConstInfo compiledName).type fun inputs _ => do + let (original, models) ← splitNativeModels inputs + return (models.size, (← typeInputs original).size) + -- A monomorphic constant has no type/provider arguments to bind. Its + -- initializer is still an owner, so every size read inside it is checked. + -- Generic size constants, including StaticAssert, also need their uses + -- checked so callers cannot substitute different endpoint types. + if semantic > 0 || parameterCount > 0 && loweredCalls.any (fun call => + call.getObjValAs? Nat "caller_def_id" == .ok ident && + call.getObjValAs? String "callee" == .ok "core::mem::size_of") then + targets := targets.push (ident, compiledName) + let ids := targets.map Prod.fst + let relevant := fun rows => rows.filter fun row => + (row.getObjValAs? Nat "callee_def_id").toOption.any ids.contains + -- Aeneas shares identical pure size reads within the static assertion. + -- Retain the full compiler inventory, but compare one binding per identical + -- endpoint for this one audited read-only operation. Conversion calls keep + -- their multiplicity, since each could make a different byte choice. + let uniqueSizes := fun rows => rows.foldl (fun (seen : Array Json) row => + if row.getObjValAs? String "callee" == .ok "core::mem::size_of" && seen.contains row + then seen else seen.push row) #[] + let expected := uniqueSizes (relevant loweredCalls) + unless uniqueSizes (relevant beforeCalls) == expected do + throwError "Provider-bearing calls changed original endpoints, owners, or multiplicity" + let mut remaining := expected + for (ownerId, ownerName) in owners do + let some (.defnInfo owner) := (← getEnv).find? ownerName + | throwError "Native provider owner {ownerName} must retain its body" + remaining ← lambdaTelescope owner.value fun inputs body => do + let (originals, models) ← splitNativeModels inputs + let params ← typeInputs originals + let mut found := callsTo (targets.map Prod.snd) body + for input in inputs do found := found ++ callsTo (targets.map Prod.snd) (← inferType input) + let mut pending := remaining + let mut seenSizes : Array Expr := #[] + for call in found do + if call.getAppFn.isConstOf `core.mem.size_of then + if seenSizes.contains call then continue + seenSizes := seenSizes.push call + let some (calleeId, _) := targets.find? (fun target => target.2 == call.getAppFn.constName!) + | throwError "Unknown provider-bearing native call" + let some rowIndex := pending.findIdx? (fun row => + row.getObjValAs? Nat "caller_def_id" == .ok ownerId && + row.getObjValAs? Nat "callee_def_id" == .ok calleeId) + | throwError "Unexpected provider-bearing native call in {ownerName}" + let .ok rustTypes := pending[rowIndex]!.getObjValAs? (Array String) "type_arguments" + | throwError "Provider-bearing call lacks original Rust endpoints" + let args := call.getAppArgs + forallTelescope (← getConstInfo call.getAppFn.constName!).type fun calleeInputs _ => do + let (originalArgs, suffix) ← splitNativeModels calleeInputs + let calleeParams ← typeInputs originalArgs + unless args.size == calleeInputs.size && rustTypes.size == calleeParams.size do + throwError "Provider-bearing call changed its original or semantic arity in {ownerName}" + let expectedTypes ← rustTypes.mapM (originalType · params) + for index in [:calleeParams.size] do + let some position := originalArgs.findIdx? (· == calleeParams[index]!) + | throwError "Native type argument is not an original input" + unless args[position]! == expectedTypes[index]! do + throwError "Provider-bearing call changed an original Rust endpoint in {ownerName}" + for index in [:suffix.size] do + let raw := (← whnf (← inferType suffix[index]!)).getAppArgs[0]! + let some parameter := calleeParams.findIdx? (· == raw) + | throwError "Native provider has no original type parameter" + let canonical ← providerAt expectedTypes[parameter]! params models + unless args[originalArgs.size + index]! == canonical do + throwError "Provider-bearing call changed its exact retained provider in {ownerName}" + pending := pending.extract 0 rowIndex ++ pending.extract (rowIndex + 1) pending.size + return pending + unless remaining.isEmpty do + throwError "Native model providers omit original compiler call witnesses" diff --git a/verification/aeneas/lean/Obligations/GenericTransmute.lean b/verification/aeneas/lean/Obligations/GenericTransmute.lean new file mode 100644 index 0000000000..10e424e2e9 --- /dev/null +++ b/verification/aeneas/lean/Obligations/GenericTransmute.lean @@ -0,0 +1,53 @@ +/- 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 TransmuteModel +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace Zerocopy.Obligations + +/-- The independent domain spells out size-query success and its agreement +with both physical widths. The result must decode from the source's same bytes. +Neither the domain nor the postcondition depends on the implementation. -/ +def transmute_copy_spec_contract (Src Dst : Type) + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + (ms : RustModel Src) (md : RustModel Dst) (run : Result Dst) : Prop := + ∀ [_sourceLaw : @TraitLaws.into_bytes_initialized Src source ms] + [_destinationLaw : @TraitLaws.from_bytes_valid Dst destination md] + [_zeroLaw : @TraitLaws.from_zeros_valid Dst destination.FromZerosInst md] + (mathSrc : ms.Model), ms.decode src = some mathSrc → + (∃ width : Usize, core.mem.size_of Src = .ok width ∧ core.mem.size_of Dst = .ok width ∧ + ms.representation.map (·.byteSize) = some width.val ∧ + md.representation.map (·.byteSize) = some width.val) → + ∃ raw math, run = .ok raw ∧ md.decode raw = some math ∧ + ∃ (bytes : List AMByte) (sd : BitDecoder Src) (dd : BitDecoder Dst), + ms.representation = some sd ∧ md.representation = some dd ∧ + sd.run bytes = some src ∧ dd.run bytes = some raw + +def transmute_copy_spec : Prop := + ∀ (Src Dst : Type) (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst], + @transmute_copy_spec_contract Src Dst source destination src ms md + (@util.macro_util.transmute_copy Src Dst source destination src ms md) + +/-- Both APIs promise the same relation for an arbitrary supplied outcome. -/ +def transmute_copy_caller_spec_contract (Src Dst : Type) + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + (ms : RustModel Src) (md : RustModel Dst) (run : Result Dst) : Prop := + @transmute_copy_spec_contract Src Dst source destination src ms md run + +def transmute_copy_caller_spec : Prop := + ∀ (Src Dst : Type) (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst], + @transmute_copy_caller_spec_contract Src Dst source destination src ms md + (@util.generic_transmute.transmute_copy_caller Src Dst source destination src ms md) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/GenericTransmute.lean b/verification/aeneas/lean/Proofs/GenericTransmute.lean new file mode 100644 index 0000000000..d5d416a3a2 --- /dev/null +++ b/verification/aeneas/lean/Proofs/GenericTransmute.lean @@ -0,0 +1,166 @@ +/- 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 TransmuteModel +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace Zerocopy.Proofs + +/-- The retained static assertion checks both successful size queries before +constructing ManuallyDrop or invoking the byte-copy interpretation. -/ +theorem transmute_copy_eq_primitive {Src Dst : Type} + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst] + (same_size : ∃ width : Usize, core.mem.size_of Src = .ok width ∧ + core.mem.size_of Dst = .ok width) : + util.macro_util.transmute_copy source destination src = + (modelManuallyDrop Src (ma := ms)).transmuteCopyResult md ⟨src⟩ := by + obtain ⟨width, hs, hd⟩ := same_size + simp only [util.macro_util.transmute_copy, + PairPhantomDataPhantomData.Insts.ZerocopyUtilMacro_utilTransmute_copyStaticAssert.ASSERT, + hs, hd] + simp only [Aeneas.Std.massert, core.mem.manually_drop.ManuallyDrop.new, core.mem.transmute_copy] + simp only [bind_ok, ite_true, decide_true] + +/-- This distinct assertion outcome also checks that the extracted guard was +retained. A theorem about only equal-size calls cannot detect its removal. -/ +theorem transmute_copy_rejects_unequal {Src Dst : Type} + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst] (sourceSize destinationSize : Usize) + (hs : core.mem.size_of Src = .ok sourceSize) + (hd : core.mem.size_of Dst = .ok destinationSize) + (different : sourceSize ≠ destinationSize) : + util.macro_util.transmute_copy source destination src = .fail .assertionFailure := by + simp only [util.macro_util.transmute_copy, + PairPhantomDataPhantomData.Insts.ZerocopyUtilMacro_utilTransmute_copyStaticAssert.ASSERT, + hs, hd] + simp [different, Aeneas.Std.massert] + +/-- The native helper's successful size queries establish equal physical +widths. Initialization, source realizability, and destination completeness then +prove that its result is admitted and has a common byte representation. -/ +theorem transmute_copy_admitted {Src Dst : Type} + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst] + (initialized : @RustModel.initializedRepresentation Src ms) + (realizable : @RustModel.realizableRepresentation Src ms) + (complete : @RustModel.completeRepresentation Dst md) + (valid : @isValid Src ms src) + (same_size : RustModel.sameSize Src Dst) : + ∃ dst value, util.macro_util.transmute_copy source destination src = .ok dst ∧ + md.decode dst = some value ∧ RustModel.byteCast src dst := by + obtain ⟨width, sourceSize, destinationSize, sourceWidth, destinationWidth⟩ := same_size + have equalWidths : ms.representation.map (·.byteSize) = md.representation.map (·.byteSize) := + sourceWidth.trans destinationWidth.symm + obtain ⟨dst, value, executed, admitted, related⟩ := + RustModel.transmuteCopyResult_admitted (modelManuallyDrop Src (ma := ms)) md ⟨src⟩ + (initializedManuallyDrop Src initialized) (manuallyDrop_realizable ms realizable) + complete (by simpa only [manuallyDrop_width] using equalWidths) valid + refine ⟨dst, value, ?_, admitted, ?_⟩ + · rw [transmute_copy_eq_primitive source destination src ⟨width, sourceSize, destinationSize⟩] + exact executed + · exact (byteCast_manuallyDrop_iff ms md src dst).mp related + +/-- The extracted caller retains the exact providers and delegates to the +verified helper. It introduces no new semantic premise. -/ +theorem transmute_copy_caller_admitted {Src Dst : Type} + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst] + (initialized : @RustModel.initializedRepresentation Src ms) + (realizable : @RustModel.realizableRepresentation Src ms) + (complete : @RustModel.completeRepresentation Dst md) + (valid : @isValid Src ms src) + (same_size : RustModel.sameSize Src Dst) : + ∃ dst value, util.generic_transmute.transmute_copy_caller source destination src = .ok dst ∧ + md.decode dst = some value ∧ RustModel.byteCast src dst := by + simpa only [util.generic_transmute.transmute_copy_caller] using + transmute_copy_admitted source destination src initialized realizable complete valid same_size + +theorem transmute_copy_spec : Specs.transmute_copy_spec := by + intro Src Dst source destination src ms md sourceLaw destinationLaw _ mathSrc decoded same_size + obtain ⟨initialized, realizable⟩ := + @TraitLaws.into_bytes_initialized.holds Src source ms sourceLaw + have complete := @TraitLaws.from_bytes_valid.holds Dst destination md destinationLaw + obtain ⟨dst, value, executed, admitted, related⟩ := + transmute_copy_admitted source destination src initialized realizable complete + ⟨mathSrc, decoded⟩ same_size + rw [executed] + exact ⟨value, admitted, related⟩ + +theorem transmute_copy_caller_spec : Specs.transmute_copy_caller_spec := by + intro Src Dst source destination src ms md sourceLaw destinationLaw zeroLaw mathSrc decoded same_size + have helper := @transmute_copy_spec Src Dst source destination src ms md + sourceLaw destinationLaw zeroLaw mathSrc decoded same_size + unfold util.generic_transmute.transmute_copy_caller + step with helper as ⟨dst, value, admitted, related⟩ + exact ⟨value, admitted, related⟩ + +/-- Every represented, admitted output occurs in this native helper's family +of executions. Only the source preference changes; both decoders and the Rust +arguments stay fixed. -/ +theorem transmute_copy_covers {Src Dst : Type} + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + (ms : RustModel Src) (md : RustModel Dst) + (same_size : @RustModel.sameSize Src Dst ms md) + (sd : BitDecoder Src) (dd : BitDecoder Dst) + (hs : ms.representation = some sd) (hd : md.representation = some dd) + (bytes : List AMByte) (dst : Dst) (value : md.Model) + (sourcePhysical : sd.run bytes = some src) + (destinationPhysical : dd.run bytes = some dst) + (admitted : md.decode dst = some value) : + @util.macro_util.transmute_copy Src Dst source destination src + (ms.withChoice (fun _ => bytes)) md = .ok dst := by + obtain ⟨size, sourceSize, destinationSize, _, _⟩ := same_size + rw [@transmute_copy_eq_primitive Src Dst source destination src + (ms.withChoice (fun _ => bytes)) md ⟨size, sourceSize, destinationSize⟩] + rw [manuallyDrop_withChoice] + have width : sd.byteSize = dd.byteSize := + (sd.run_length bytes src sourcePhysical).symm.trans (dd.run_length bytes dst destinationPhysical) + exact RustModel.transmuteCopyResult_covers (modelManuallyDrop Src (ma := ms)) md ⟨src⟩ + (sd.map core.mem.manually_drop.ManuallyDrop.mk) dd + (by rw [manuallyDrop_representation, hs]; rfl) hd width bytes dst value + (by simp [BitDecoder.run_map, sourcePhysical]) destinationPhysical admitted + +theorem transmute_copy_caller_covers {Src Dst : Type} + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + (ms : RustModel Src) (md : RustModel Dst) + (same_size : @RustModel.sameSize Src Dst ms md) + (sd : BitDecoder Src) (dd : BitDecoder Dst) + (hs : ms.representation = some sd) (hd : md.representation = some dd) + (bytes : List AMByte) (dst : Dst) (value : md.Model) + (sourcePhysical : sd.run bytes = some src) + (destinationPhysical : dd.run bytes = some dst) + (admitted : md.decode dst = some value) : + @util.generic_transmute.transmute_copy_caller Src Dst source destination src + (ms.withChoice (fun _ => bytes)) md = .ok dst := by + simpa only [util.generic_transmute.transmute_copy_caller] using + transmute_copy_covers source destination src ms md same_size sd dd hs hd + bytes dst value sourcePhysical destinationPhysical admitted + +/-- Universal provider proofs cover every represented output of the actual +extracted helper, including outputs from distinct encodings of one raw input. -/ +theorem transmute_copy_allChoices {Src Dst : Type} + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + (ms : RustModel Src) (md : RustModel Dst) (post : Dst → Prop) + (verified : ∀ choose dst, + @util.macro_util.transmute_copy Src Dst source destination src (ms.withChoice choose) md = + .ok dst → post dst) + (same_size : @RustModel.sameSize Src Dst ms md) + (sd : BitDecoder Src) (dd : BitDecoder Dst) + (hs : ms.representation = some sd) (hd : md.representation = some dd) + (bytes : List AMByte) (dst : Dst) (value : md.Model) + (sourcePhysical : sd.run bytes = some src) + (destinationPhysical : dd.run bytes = some dst) + (admitted : md.decode dst = some value) : post dst := + verified (fun _ => bytes) dst (transmute_copy_covers source destination src ms md + same_size sd dd hs hd bytes dst value sourcePhysical destinationPhysical admitted) + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/GenericTransmute.lean b/verification/aeneas/lean/RequiredModelContracts/GenericTransmute.lean new file mode 100644 index 0000000000..961ec982a9 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/GenericTransmute.lean @@ -0,0 +1,46 @@ +/- 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.GenericTransmute +public import RequiredContracts +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +/-- Expand the authored byte relation for the same arbitrary outcome. This +adapter does not use the native helper's correctness theorem. -/ +@[contract_simps] theorem required_transmute_copy (Src Dst : Type) + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst] (run : Result Dst) + (provided : Specs.transmute_copy_spec_contract Src Dst source destination src run) : + Obligations.transmute_copy_spec_contract Src Dst source destination src ms md run := by + intro sourceLaw destinationLaw zeroLaw mathSrc decoded sameSize + obtain ⟨raw, executed, math, admitted, related⟩ := + (WP.spec_equiv_exists run _).mp (provided mathSrc decoded sameSize) + obtain ⟨bytes, sourcePhysical, destinationPhysical⟩ := related + cases hs : ms.representation with + | none => simp [RustModel.represented, hs] at sourcePhysical + | some sd => + cases hd : md.representation with + | none => simp [RustModel.represented, hd] at destinationPhysical + | some dd => + exact ⟨raw, math, executed, admitted, bytes, sd, dd, rfl, rfl, + by simpa only [RustModel.represented, hs] using sourcePhysical, + by simpa only [RustModel.represented, hd] using destinationPhysical⟩ + +@[contract_simps] theorem required_transmute_copy_caller (Src Dst : Type) + (source : IntoBytes Src) (destination : FromBytes Dst) (src : Src) + [ms : RustModel Src] [md : RustModel Dst] (run : Result Dst) + (provided : Specs.transmute_copy_caller_spec_contract Src Dst source destination src run) : + Obligations.transmute_copy_caller_spec_contract Src Dst source destination src ms md run := by + exact required_transmute_copy Src Dst source destination src run provided + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RustModel.lean b/verification/aeneas/lean/RustModel.lean index 4a54d75ef5..57f3eb1129 100644 --- a/verification/aeneas/lean/RustModel.lean +++ b/verification/aeneas/lean/RustModel.lean @@ -38,6 +38,9 @@ class RustModel (Raw : Type u) where provider cannot establish byte-validity laws. This decoder operates independently of the optional library invariant. -/ representation : Option (Rust.Storage.BitDecoder Raw) := none + /-- A preferred physical representation. Operations check it before use. + Universally varying this field retains every accepted representation. -/ + representationChoice : Raw → List Rust.Storage.AMByte := fun _ => [] -- The associated type is transparent so ordinary rewriting and coercions can -- identify a retained provider's Model with its named mathematical carrier. @@ -71,6 +74,11 @@ def RustModel.realizableRepresentation (Raw : Type u) [m : RustModel Raw] : Prop | some decoder => ∀ raw, @isValid Raw m raw → ∃ bytes, decoder.run bytes = some raw +/-- Change the operational preference without changing either decoder. -/ +@[reducible] def RustModel.withChoice {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List Rust.Storage.AMByte) : RustModel Raw := + { m with representationChoice := choose } + /-- Every initialized representation of the physical width admits a language value and a mathematical value through this same provider. Missing physical semantics fail closed. This law does not establish Rust layout correspondence, diff --git a/verification/aeneas/lean/TransmuteModel.lean b/verification/aeneas/lean/TransmuteModel.lean new file mode 100644 index 0000000000..5d90131c6e --- /dev/null +++ b/verification/aeneas/lean/TransmuteModel.lean @@ -0,0 +1,301 @@ +/- 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 ModelPrelude +@[expose] public section + +/-! +A raw value need not identify its bytes uniquely. Two byte strings can decode +into the same raw value, yet a cast into a byte-observing destination can tell +those strings apart. Selecting one canonical string would discard permitted +Rust outcomes. + +We retain a preferred string in each model provider. Selection validates that +preference and falls back only when another representation exists. The generic +proof quantifies over the provider, and the coverage theorem varies just its +preference while fixing its physical and mathematical decoders. Together those +facts cover every represented outcome without adding effects to Aeneas's Result. + +A preference is a function of the raw value, not an execution history. Admission +therefore rejects repeated conversions, loops, and recursion in this fragment, +and only admits generic forwarding whose provider remains universally bound. +Supporting independent choices at multiple conversions needs a richer model. + +This module proves byte-level admission. Rust correspondence, actual layout, +valid reference access, and the absence of destructor effects remain separate +premises or independently checked obligations. Numeric bytes carry no provenance. +-/ + +open Aeneas.Std Rust.Storage +namespace AeneasSpecs +namespace RustModel + +/-- The physical decoder accepts these bytes as this raw value. -/ +def represented {Raw : Type u} (m : RustModel Raw) (raw : Raw) (bytes : List AMByte) : Prop := + match m.representation with + | none => False + | some decoder => decoder.run bytes = some raw + +@[simp] theorem withChoice_decode {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List AMByte) : (m.withChoice choose).decode = m.decode := rfl + +@[simp] theorem withChoice_representation {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List AMByte) : (m.withChoice choose).representation = m.representation := rfl + +@[simp] theorem withChoice_represented {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List AMByte) (raw : Raw) (bytes : List AMByte) : + (m.withChoice choose).represented raw bytes ↔ m.represented raw bytes := Iff.rfl + +@[simp] theorem withChoice_initialized {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List AMByte) : + @initializedRepresentation Raw (m.withChoice choose) ↔ @initializedRepresentation Raw m := Iff.rfl + +@[simp] theorem withChoice_realizable {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List AMByte) : + @realizableRepresentation Raw (m.withChoice choose) ↔ @realizableRepresentation Raw m := Iff.rfl + +@[simp] theorem withChoice_complete {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List AMByte) : + @completeRepresentation Raw (m.withChoice choose) ↔ @completeRepresentation Raw m := Iff.rfl + +@[simp] theorem withChoice_valid {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List AMByte) (raw : Raw) : + @isValid Raw (m.withChoice choose) raw ↔ @isValid Raw m raw := Iff.rfl + +@[simp] theorem withChoice_zero {Raw : Type u} (m : RustModel Raw) + (choose : Raw → List AMByte) : + @zeroRepresentation Raw (m.withChoice choose) ↔ @zeroRepresentation Raw m := Iff.rfl + +/-- Check the preference, then fall back to an accepted representation. The +fallback establishes existence; varying the preference covers every choice. -/ +noncomputable def selectedBytes {Raw : Type u} (m : RustModel Raw) (raw : Raw) : + Result (List AMByte) := by + classical + exact if preferred : m.represented raw (m.representationChoice raw) then + .ok (m.representationChoice raw) + else if possible : ∃ bytes, m.represented raw bytes then + .ok (Classical.choose possible) + else .fail .undef + +theorem selectedBytes_represented {Raw : Type u} (m : RustModel Raw) (raw : Raw) + (bytes : List AMByte) (selected : m.selectedBytes raw = .ok bytes) : + m.represented raw bytes := by + classical + unfold selectedBytes at selected + split at selected + · have equal : m.representationChoice raw = bytes := by simpa using selected + exact equal ▸ ‹m.represented raw (m.representationChoice raw)› + · split at selected + · have accepted := Classical.choose_spec ‹∃ bytes, m.represented raw bytes› + have equal : Classical.choose ‹∃ bytes, m.represented raw bytes› = bytes := by simpa using selected + exact equal ▸ accepted + · simp at selected + +theorem selectedBytes_exists {Raw : Type u} (m : RustModel Raw) (raw : Raw) + (possible : ∃ bytes, m.represented raw bytes) : + ∃ bytes, m.selectedBytes raw = .ok bytes ∧ m.represented raw bytes := by + classical + unfold selectedBytes + split + · exact ⟨_, rfl, ‹m.represented raw (m.representationChoice raw)›⟩ + · exact ⟨_, rfl, Classical.choose_spec possible⟩ + +/-- A constant preference can select any accepted representation of this input. -/ +theorem selectedBytes_withChoice {Raw : Type u} (m : RustModel Raw) (raw : Raw) + (bytes : List AMByte) (accepted : m.represented raw bytes) : + (m.withChoice (fun _ => bytes)).selectedBytes raw = .ok bytes := by + classical + simp only [selectedBytes, withChoice, represented] at * + exact dif_pos accepted + +/-- Equal-width byte copying followed by language validity and model admission. +This is the selected fragment of transmute_copy, not a model of resource ownership. -/ +noncomputable def transmuteCopyResult {Src : Type u} {Dst : Type v} + (source : RustModel Src) (destination : RustModel Dst) (src : Src) : Result Dst := + match source.representation, destination.representation with + | some sourceDecoder, some destinationDecoder => do + if sourceDecoder.byteSize = destinationDecoder.byteSize then + let bytes ← source.selectedBytes src + let raw ← Result.ofOption (destinationDecoder.run bytes) .undef + let _ ← Result.ofOption (destination.decode raw) .undef + .ok raw + else .fail .undef + | _, _ => .fail .undef + +/-- Both values decode from the same bytes. This relation keeps all accepted +representations, independently of the operational preference. -/ +def byteCastWith {Src : Type u} {Dst : Type v} (source : RustModel Src) + (destination : RustModel Dst) (src : Src) (dst : Dst) : Prop := + ∃ bytes, source.represented src bytes ∧ destination.represented dst bytes + +/-- Contracts retain the source and destination providers implicitly. -/ +def byteCast {Src : Type u} {Dst : Type v} [source : RustModel Src] + [destination : RustModel Dst] (src : Src) (dst : Dst) : Prop := + source.byteCastWith destination src dst + +theorem transmuteCopyResult_of_selected {Src : Type u} {Dst : Type v} + (source : RustModel Src) (destination : RustModel Dst) (src : Src) + (sourceDecoder : BitDecoder Src) (destinationDecoder : BitDecoder Dst) + (hs : source.representation = some sourceDecoder) + (hd : destination.representation = some destinationDecoder) + (width : sourceDecoder.byteSize = destinationDecoder.byteSize) + (bytes : List AMByte) (dst : Dst) (value : destination.Model) + (selected : source.selectedBytes src = .ok bytes) + (physical : destinationDecoder.run bytes = some dst) + (admitted : destination.decode dst = some value) : + source.transmuteCopyResult destination src = .ok dst := by + simp [transmuteCopyResult, hs, hd, width, selected, physical, admitted] + +theorem transmuteCopyResult_rejects_physical {Src : Type u} {Dst : Type v} + (source : RustModel Src) (destination : RustModel Dst) (src : Src) + (sourceDecoder : BitDecoder Src) (destinationDecoder : BitDecoder Dst) + (hs : source.representation = some sourceDecoder) + (hd : destination.representation = some destinationDecoder) + (width : sourceDecoder.byteSize = destinationDecoder.byteSize) + (bytes : List AMByte) (selected : source.selectedBytes src = .ok bytes) + (rejected : destinationDecoder.run bytes = none) : + source.transmuteCopyResult destination src = .fail .undef := by + simp [transmuteCopyResult, hs, hd, width, selected, rejected] + +theorem transmuteCopyResult_rejects_model {Src : Type u} {Dst : Type v} + (source : RustModel Src) (destination : RustModel Dst) (src : Src) + (sourceDecoder : BitDecoder Src) (destinationDecoder : BitDecoder Dst) + (hs : source.representation = some sourceDecoder) + (hd : destination.representation = some destinationDecoder) + (width : sourceDecoder.byteSize = destinationDecoder.byteSize) + (bytes : List AMByte) (dst : Dst) (selected : source.selectedBytes src = .ok bytes) + (physical : destinationDecoder.run bytes = some dst) + (rejected : destination.decode dst = none) : + source.transmuteCopyResult destination src = .fail .undef := by + simp [transmuteCopyResult, hs, hd, width, selected, physical, rejected] + +/-- Initialization, realizability, and destination completeness compose without +selecting a canonical representation as the only possible Rust outcome. -/ +theorem transmuteCopyResult_admitted {Src : Type u} {Dst : Type v} + (source : RustModel Src) (destination : RustModel Dst) (src : Src) + (initialized : @initializedRepresentation Src source) + (realizable : @realizableRepresentation Src source) + (complete : @completeRepresentation Dst destination) + (sameWidth : source.representation.map (·.byteSize) = destination.representation.map (·.byteSize)) + (valid : @isValid Src source src) : + ∃ dst value, source.transmuteCopyResult destination src = .ok dst ∧ + destination.decode dst = some value ∧ source.byteCastWith destination src dst := by + cases hs : source.representation with + | none => simp [initializedRepresentation, hs] at initialized + | some sd => + cases hd : destination.representation with + | none => simp [completeRepresentation, hd] at complete + | some dd => + simp only [initializedRepresentation, hs] at initialized + simp only [realizableRepresentation, hs] at realizable + simp only [completeRepresentation, hd] at complete + have width : sd.byteSize = dd.byteSize := by simpa [hs, hd] using sameWidth + obtain ⟨initial, initialAccepted⟩ := realizable src valid + have possible : ∃ bytes, source.represented src bytes := + ⟨initial, by simpa [represented, hs] using initialAccepted⟩ + obtain ⟨bytes, selected, accepted⟩ := source.selectedBytes_exists src possible + have physical : sd.run bytes = some src := by simpa [represented, hs] using accepted + obtain ⟨dst, value, decoded, admitted⟩ := complete bytes + ((sd.run_length bytes src physical).trans width) (initialized bytes src physical) + exact ⟨dst, value, + transmuteCopyResult_of_selected source destination src sd dd hs hd width bytes dst value + selected decoded admitted, + admitted, bytes, accepted, by simpa [represented, hd] using decoded⟩ + +/-- Every admitted destination interpretation of any source representation is +an execution of the extracted primitive with the same decoders and a changed +preference. This is the coverage fact needed by an all-choices contract. -/ +theorem transmuteCopyResult_covers {Src : Type u} {Dst : Type v} + (source : RustModel Src) (destination : RustModel Dst) (src : Src) + (sourceDecoder : BitDecoder Src) (destinationDecoder : BitDecoder Dst) + (hs : source.representation = some sourceDecoder) + (hd : destination.representation = some destinationDecoder) + (width : sourceDecoder.byteSize = destinationDecoder.byteSize) + (bytes : List AMByte) (dst : Dst) (value : destination.Model) + (sourcePhysical : sourceDecoder.run bytes = some src) + (destinationPhysical : destinationDecoder.run bytes = some dst) + (admitted : destination.decode dst = some value) : + (source.withChoice (fun _ => bytes)).transmuteCopyResult destination src = .ok dst := by + apply transmuteCopyResult_of_selected (source.withChoice (fun _ => bytes)) destination src sourceDecoder destinationDecoder + hs hd width bytes dst value + · exact source.selectedBytes_withChoice src bytes (by simpa [represented, hs] using sourcePhysical) + · exact destinationPhysical + · exact admitted + +/-- A choice-independent postcondition proved for every preference holds for +all represented outcomes. The quantifier cannot be replaced by one provider. -/ +theorem transmuteCopyResult_allChoices {Src : Type u} {Dst : Type v} + (source : RustModel Src) (destination : RustModel Dst) (src : Src) (post : Dst → Prop) + (verified : ∀ choose dst, + (source.withChoice choose).transmuteCopyResult destination src = .ok dst → post dst) + (sourceDecoder : BitDecoder Src) (destinationDecoder : BitDecoder Dst) + (hs : source.representation = some sourceDecoder) + (hd : destination.representation = some destinationDecoder) + (width : sourceDecoder.byteSize = destinationDecoder.byteSize) + (bytes : List AMByte) (dst : Dst) (value : destination.Model) + (sourcePhysical : sourceDecoder.run bytes = some src) + (destinationPhysical : destinationDecoder.run bytes = some dst) + (admitted : destination.decode dst = some value) : post dst := + verified (fun _ => bytes) dst (transmuteCopyResult_covers source destination src + sourceDecoder destinationDecoder hs hd width bytes dst value + sourcePhysical destinationPhysical admitted) + +end RustModel + +/-- ManuallyDrop preserves the preferred bytes as well as the physical decoder. -/ +@[simp] theorem manuallyDrop_choice {T : Type} (m : RustModel T) (raw : T) : + (modelManuallyDrop T (ma := m)).representationChoice ⟨raw⟩ = m.representationChoice raw := rfl + +@[simp] theorem manuallyDrop_representation {T : Type} (m : RustModel T) : + (modelManuallyDrop T (ma := m)).representation = + m.representation.map (·.map core.mem.manually_drop.ManuallyDrop.mk) := rfl + +theorem manuallyDrop_represented {T : Type} (m : RustModel T) (raw : T) (bytes : List AMByte) : + (modelManuallyDrop T (ma := m)).represented ⟨raw⟩ bytes ↔ m.represented raw bytes := by + unfold RustModel.represented + rw [manuallyDrop_representation] + cases h : m.representation with + | none => simp + | some decoder => + simp only [Option.map_some, BitDecoder.run_map] + cases decoder.run bytes <;> simp + +theorem byteCast_manuallyDrop_iff {Src Dst : Type} (source : RustModel Src) + (destination : RustModel Dst) (src : Src) (dst : Dst) : + @RustModel.byteCast (core.mem.manually_drop.ManuallyDrop Src) Dst + (modelManuallyDrop Src (ma := source)) destination ⟨src⟩ dst ↔ + @RustModel.byteCast Src Dst source destination src dst := by + simp only [RustModel.byteCast, RustModel.byteCastWith, manuallyDrop_represented] + +theorem manuallyDrop_withChoice {T : Type} (m : RustModel T) + (choose : T → List AMByte) : + modelManuallyDrop T (ma := m.withChoice choose) = + (modelManuallyDrop T (ma := m)).withChoice (fun raw => choose raw.value) := rfl + +@[simp] theorem manuallyDrop_width {T : Type} (m : RustModel T) : + (modelManuallyDrop T (ma := m)).representation.map (·.byteSize) = + m.representation.map (·.byteSize) := by + change (m.representation.map (·.map core.mem.manually_drop.ManuallyDrop.mk)).map (·.byteSize) = _ + cases h : m.representation <;> simp [BitDecoder.map] + +theorem manuallyDrop_realizable {T : Type} (m : RustModel T) + (realizable : @RustModel.realizableRepresentation T m) : + @RustModel.realizableRepresentation (core.mem.manually_drop.ManuallyDrop T) + (modelManuallyDrop T (ma := m)) := by + cases h : m.representation with + | none => simp [RustModel.realizableRepresentation, h] at realizable + | some decoder => + simp only [RustModel.realizableRepresentation, h] at realizable + unfold RustModel.realizableRepresentation + rw [manuallyDrop_representation, h] + intro raw valid + obtain ⟨bytes, accepted⟩ := realizable raw.value valid + exact ⟨bytes, by simp [BitDecoder.run_map, accepted]⟩ + +end AeneasSpecs diff --git a/verification/aeneas/lean/TransmuteModelTests.lean b/verification/aeneas/lean/TransmuteModelTests.lean new file mode 100644 index 0000000000..6c63e9f27d --- /dev/null +++ b/verification/aeneas/lean/TransmuteModelTests.lean @@ -0,0 +1,155 @@ +/- 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 TransmuteModel +@[expose] public section +open Aeneas.Std Rust.Storage AeneasSpecs +namespace TransmuteModelTests + +-- One raw value has many byte representations. No encoder can designate one +-- of them as the only behavior of a byte-observing cast. +@[reducible] def ambiguousSource : RustModel Unit where + Model := Unit + decode := some + representation := some (byteDecoder.map fun _ => ()) + +@[reducible] def byteDestination : RustModel Rust.Bytes.Byte where + Model := Rust.Bytes.Byte + decode := some + representation := some byteDecoder + +theorem ambiguous_source_initialized : @RustModel.initializedRepresentation Unit ambiguousSource := + BitDecoder.map_initialized _ _ byteDecoder_initialized + +theorem ambiguous_source_realizable : @RustModel.realizableRepresentation Unit ambiguousSource := by + intro raw _ + cases raw + exact ⟨[.init 0], rfl⟩ + +theorem byte_destination_complete : + @RustModel.completeRepresentation Rust.Bytes.Byte byteDestination := by + intro bytes width initialized + obtain ⟨byte, accepted⟩ := byteDecoder_complete bytes width initialized + exact ⟨byte, byte, accepted, rfl⟩ + +-- Both outcomes are included while the mathematical and physical decoders stay fixed. +theorem chooses_zero : + (ambiguousSource.withChoice (fun _ => [.init 0])).transmuteCopyResult byteDestination () = + .ok 0 := by + exact RustModel.transmuteCopyResult_covers ambiguousSource byteDestination () + _ _ rfl rfl rfl [.init 0] 0 0 rfl rfl rfl + +theorem chooses_one : + (ambiguousSource.withChoice (fun _ => [.init 1])).transmuteCopyResult byteDestination () = + .ok 1 := by + exact RustModel.transmuteCopyResult_covers ambiguousSource byteDestination () + _ _ rfl rfl rfl [.init 1] 1 1 rfl rfl rfl + +example : (0 : Rust.Bytes.Byte) ≠ 1 := by decide + +-- Every preference succeeds, including an invalid empty preference; this does +-- not identify the fallback witness with either of the two demonstrated choices. +example (choose : Unit → List AMByte) : + ∃ dst value, + (ambiguousSource.withChoice choose).transmuteCopyResult byteDestination () = .ok dst ∧ + byteDestination.decode dst = some value ∧ + (ambiguousSource.withChoice choose).byteCastWith byteDestination () dst := by + exact RustModel.transmuteCopyResult_admitted _ _ () ambiguous_source_initialized + ambiguous_source_realizable byte_destination_complete rfl ⟨(), rfl⟩ + +@[reducible] def rejectsAllSource : RustModel Unit where + Model := Unit + decode := some + representation := some { byteSize := 1, decode := fun _ => none } + +example : @RustModel.initializedRepresentation Unit rejectsAllSource := by + intro bytes raw accepted + simp [BitDecoder.run] at accepted + +example : ¬ @RustModel.realizableRepresentation Unit rejectsAllSource := by + intro realizable + obtain ⟨bytes, accepted⟩ := realizable () ⟨(), rfl⟩ + simp [BitDecoder.run] at accepted + +example : rejectsAllSource.transmuteCopyResult byteDestination () = .fail .undef := by + have hs : rejectsAllSource.representation = some { byteSize := 1, decode := fun _ => none } := rfl + have hd : byteDestination.representation = some byteDecoder := rfl + have impossible (bytes : List AMByte) : ¬ rejectsAllSource.represented () bytes := by + simp [RustModel.represented, hs, BitDecoder.run] + have selected : rejectsAllSource.selectedBytes () = .fail .undef := by + simp [RustModel.selectedBytes, impossible] + simp [RustModel.transmuteCopyResult, hs, hd, selected, byteDecoder] + +-- Empty Rust types require no invented value and no global Inhabited premise. +@[reducible] def emptySource : RustModel Empty where + Model := Empty + decode raw := nomatch raw + representation := some { byteSize := 0, decode := fun _ => none } + +example : @RustModel.realizableRepresentation Empty emptySource := by + intro raw + exact nomatch raw + +example : @RustModel.initializedRepresentation Empty emptySource := by + intro bytes raw + exact nomatch raw + +example : ¬ @RustModel.completeRepresentation Empty emptySource := by + intro complete + obtain ⟨raw, _, _, _⟩ := complete [] rfl (by simp) + exact nomatch raw + +-- Destination language validity is checked even when a caller asks only True. +@[reducible] def boolDestination : RustModel Bool where + Model := Bool + decode := some + representation := some boolDecoder + +theorem rejects_invalid_bool : + (ambiguousSource.withChoice (fun _ => [.init 2])).transmuteCopyResult boolDestination () = + .fail .undef := by + apply RustModel.transmuteCopyResult_rejects_physical + (ambiguousSource.withChoice (fun _ => [.init 2])) boolDestination () _ _ rfl rfl rfl [.init 2] + · exact ambiguousSource.selectedBytes_withChoice () [.init 2] (by rfl) + · decide + +example : ¬ WP.spec + ((ambiguousSource.withChoice (fun _ => [.init 2])).transmuteCopyResult boolDestination ()) + (fun _ => True) := by + rw [rejects_invalid_bool] + simp + +-- A physical success cannot bypass the destination's mathematical decoder. +@[reducible] def rejectsModelDestination : RustModel Rust.Bytes.Byte where + Model := Unit + decode := fun _ => none + representation := some byteDecoder + +example : + (ambiguousSource.withChoice (fun _ => [.init 0])).transmuteCopyResult rejectsModelDestination () = + .fail .undef := by + apply RustModel.transmuteCopyResult_rejects_model + (ambiguousSource.withChoice (fun _ => [.init 0])) rejectsModelDestination () _ _ rfl rfl rfl [.init 0] 0 + · exact ambiguousSource.selectedBytes_withChoice () [.init 0] (by rfl) + · rfl + · rfl + +example : + ambiguousSource.transmuteCopyResult modelUnit () = .fail .undef := by + have hs : ambiguousSource.representation = some (byteDecoder.map fun _ => ()) := rfl + have hd : modelUnit.representation = some unitDecoder := rfl + simp [RustModel.transmuteCopyResult, hs, hd, BitDecoder.map, byteDecoder, unitDecoder, emptyDecoder] + +example (choose : Unit → List AMByte) : + (modelManuallyDrop Unit (ma := ambiguousSource.withChoice choose)).representationChoice ⟨()⟩ = + choose () := rfl + +#print axioms RustModel.transmuteCopyResult_admitted +#print axioms RustModel.transmuteCopyResult_covers +end TransmuteModelTests diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index d8e1286c6b..b7ccb4038f 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -9,6 +9,7 @@ those terms. -/ module public import Zerocopy.Types public import ModelPrelude +public import TransmuteModel @[expose] public section open Aeneas Aeneas.Std open Zerocopy @@ -218,3 +219,28 @@ noncomputable def Zerocopy.RustLayout.align (T : Type) : Usize := by exact if h : T = Usize then if (cast h x : Usize) = 0#usize then forbiddenExecution else .ok ⟨x⟩ else forbiddenExecution + +-- The constructor preserves the stored value and suppresses its automatic +-- destructor. The separate ownership audit proves that ignored conditional +-- drops cannot execute glue; this function does not model destructor effects. +def core.mem.manually_drop.ManuallyDrop.new {T : Type} (src : T) : + Result (core.mem.manually_drop.ManuallyDrop T) := .ok ⟨src⟩ + +-- Only equal-width, numeric-storage conversions are admitted. The provider +-- suffix is independent of Rust trait dictionaries and retains both endpoints. +-- A universal coverage theorem accounts for every represented source byte +-- sequence; the implementation's preferred sequence is not a canonical ABI. +noncomputable def core.mem.transmute_copy {Src : Type} (Dst : Type) (src : Src) + [source : AeneasSpecs.RustModel Src] [destination : AeneasSpecs.RustModel Dst] : Result Dst := + source.transmuteCopyResult destination src + +-- These are the physical-model/ABI premises for the generic conversion, not +-- additional safety obligations on a Rust caller. The compiler checks equality +-- of actual sizes. Connecting those observations to our byte decoders remains +-- explicit until a verified type-layout model can provide the correspondence. +def AeneasSpecs.RustModel.sameSize (Src Dst : Type) + [source : AeneasSpecs.RustModel Src] [destination : AeneasSpecs.RustModel Dst] : Prop := + ∃ width : Usize, + core.mem.size_of Src = .ok width ∧ core.mem.size_of Dst = .ok width ∧ + source.representation.map (·.byteSize) = some width.val ∧ + destination.representation.map (·.byteSize) = some width.val diff --git a/verification/aeneas/negative-control-family.sh b/verification/aeneas/negative-control-family.sh index b08bbc0e9f..bda6689485 100644 --- a/verification/aeneas/negative-control-family.sh +++ b/verification/aeneas/negative-control-family.sh @@ -24,7 +24,8 @@ 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 ZeroedAuditProbe.lean NegativeControl.lean WeakOutcome.lean + StdTransmuteAuditProbe.lean ZeroedAuditProbe.lean TransmuteCopyAuditProbe.lean + NegativeControl.lean WeakOutcome.lean RoundingConstructorControl.lean RoundingDomainControl.lean Zerocopy/ScopeControl.lean Zerocopy/ShapeControl.lean Zerocopy/ModelControl.lean Proofs/WitnessOwnerControl.lean Proofs/PaddingDependencyControl.lean @@ -316,6 +317,10 @@ 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 +if has_model util.macro_util.transmute_copy; then + python3 -B "$repo/verification/aeneas/tests/transmute_copy_audit_controls.py" \ + --work "$PWD" --runtime "$tools_dir" --evidence "$backup/transmute-copy" +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/prepare.py b/verification/aeneas/prepare.py index ea77e2a56d..e447bc4b22 100644 --- a/verification/aeneas/prepare.py +++ b/verification/aeneas/prepare.py @@ -79,7 +79,7 @@ def retain_native_models(funs): # available. Restrict the extension to the actual primitive's dependency # closure so unrelated native proof terms and anonymous arguments retain # their ordinary upstream elaboration. - dependent = {'core.mem.zeroed'} + dependent = {'core.mem.zeroed', 'core.mem.transmute_copy'} while True: found = {name for name, definition in definitions.items() if any(re.search(r'(? AeneasSpecs.RustModel.byteCast src result +aeneas_spec_end +check_spec_binding Zerocopy.Specs.transmute_copy_caller_spec for Zerocopy.util.generic_transmute.transmute_copy_caller with 5 + +check_model_inputs Zerocopy.util.macro_util.transmute_copy with 2 type parameters +aeneas_spec_begin +spec transmute_copy_spec + for @Zerocopy.util.macro_util.transmute_copy with 2 type parameters + requires(raw) same_size : AeneasSpecs.RustModel.sameSize Src Dst + ensures(raw) result => AeneasSpecs.RustModel.byteCast src result +aeneas_spec_end +check_spec_binding Zerocopy.Specs.transmute_copy_spec for Zerocopy.util.macro_util.transmute_copy with 5 + check_model_inputs Zerocopy.util.padding_needed_for with 0 type parameters aeneas_spec_begin spec padding_lt_alignment diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean index 4c7b510126..16820cd214 100644 --- a/verification/aeneas/projections/TraitLaws.lean +++ b/verification/aeneas/projections/TraitLaws.lean @@ -28,6 +28,7 @@ trait_dictionary @Zerocopy.FromBytes trait_dictionary @Zerocopy.IntoBytes trait_dictionary @Zerocopy.Unaligned trait_dictionary @Zerocopy.trait_checks.ByteCodec +trait_dictionary @Zerocopy.util.macro_util.transmute_copy.StaticAssert trait_invariant from_zeros_valid for @Zerocopy.FromZeros with 1 type parameters where self => AeneasSpecs.RustModel.zeroRepresentation Self diff --git a/verification/aeneas/tests/test_trait_invariants.py b/verification/aeneas/tests/test_trait_invariants.py index f644e3fde6..95cd36b74f 100644 --- a/verification/aeneas/tests/test_trait_invariants.py +++ b/verification/aeneas/tests/test_trait_invariants.py @@ -154,6 +154,68 @@ def test_every_local_impl_requires_binding_and_proof_selection(self): with self.assertRaisesRegex(ValueError, 'lacks its native dictionary'): traits.bind_laws(annotations, work, self.final, self.before) + def test_function_root_nested_unannotated_impl_is_not_a_proof_marker(self): + annotations = inline.Annotations() + annotations['zerocopy::Marker'] = {'kind': 'trait', 'rust': 'zerocopy::Marker', + 'generics': ['Self'], 'theorem': 'marker', 'predicate': 'Self = Self'} + nested_trait = {'def_id': 3, + 'item_meta': meta('zerocopy::helper::StaticAssert'), + 'generics': generics(names=('Self',)), 'types': []} + annotated = {'def_id': 2, 'item_meta': meta('zerocopy::MarkerImpl'), + 'impl_trait': {'id': 0, 'generics': args([{'Scalar': 'Bool'}])}, + 'generics': generics(names=())} + nested = {'def_id': 4, 'item_meta': meta('zerocopy::helper::StaticAssertImpl'), + 'impl_trait': {'id': 3, 'generics': args([{'Scalar': 'Bool'}])}, + 'generics': generics(names=())} + nested['item_meta']['started_from'] = True + self.final['trait_decls'].append(nested_trait) + self.before['trait_decls'].append(copy.deepcopy(nested_trait)) + self.final['trait_impls'] = [annotated, nested] + self.before['trait_impls'] = copy.deepcopy(self.final['trait_impls']) + location = {'file': 'src/lib.rs', 'begin_line': 1, 'end_line': 4} + native = {'crate': 'zerocopy', 'charon_version': '0.1.276', + 'aeneas_version': 'nightly-2026.10.01-ca282ec+nominal-tuple-structs.1', + 'trait_decls': [{'def_id': ident, 'lean_name': raw, + 'rust_name': rust, 'is_local': True, 'source': location} + for ident, raw, rust in [ + (0, 'Zerocopy.Marker', 'zerocopy::Marker'), + (3, 'Zerocopy.helper.StaticAssert', 'zerocopy::helper::StaticAssert')]], + 'trait_impls': [{'def_id': ident, 'lean_name': raw, + 'impl_trait_def_id': trait, 'impl_trait_rust_name': rust, + 'is_local': True, 'source': location} + for ident, raw, trait, rust in [ + (2, 'Zerocopy.Bool.Insts.Marker', 0, 'zerocopy::Marker'), + (4, 'Zerocopy.helper.Bool.Insts.StaticAssert', 3, + 'zerocopy::helper::StaticAssert')]]} + with tempfile.TemporaryDirectory() as tmp: + work = Path(tmp) + (work / 'Zerocopy').mkdir() + (work / 'Zerocopy/translation.json').write_text(json.dumps(native)) + + def bind(): + return traits.bind_laws(annotations, work, self.final, self.before) + + laws, obligations, _ = bind() + self.assertEqual([law['def_id'] for law in laws], [0]) + # The unmarked annotated dependency still needs its exact proof. + self.assertEqual([row['def_id'] for row in obligations], [2]) + self.assertEqual(obligations[0]['proof'], + 'Zerocopy.Proofs.Bool.Insts.Marker_law') + # Neither compiler stage may independently root an unmarked owner + # of an annotated trait, even beside a legitimate nested root. + for crate in (self.before, self.final): + crate['trait_impls'][0]['item_meta']['started_from'] = True + with self.assertRaisesRegex(ValueError, 'roots disagree with bound markers'): + bind() + crate['trait_impls'][0]['item_meta']['started_from'] = False + for crate in (self.before, self.final): + crate['trait_impls'][0]['item_meta']['started_from'] = True + annotations.trait_proofs = [{'file': 'zerocopy/src/lib.rs', + 'syntax': '__marker_impl', 'theorem': None, + 'generics': [], 'const_generics': [], + 'open_line': 1, 'open_col': 0, 'end_line': 4, 'end_col': 1}] + self.assertEqual([row['def_id'] for row in bind()[1]], [2]) + def test_array_impl_retains_usize_const_and_original_application(self): annotations = inline.Annotations() annotations['zerocopy::Marker'] = {'kind': 'trait', 'rust': 'zerocopy::Marker', diff --git a/verification/aeneas/tests/test_transmute_copy_admission.py b/verification/aeneas/tests/test_transmute_copy_admission.py new file mode 100644 index 0000000000..edec033cd2 --- /dev/null +++ b/verification/aeneas/tests/test_transmute_copy_admission.py @@ -0,0 +1,250 @@ +# 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. + +"""Admission diagnostics, without claiming the unit callback is a drop proof. + +Set AENEAS_TRANSMUTE_PROBE to a directory containing the historical probe's +probe.before.ullbc and probe.llbc to exercise real compiler mutations too. +Final verification must run KernelDrops against the fresh production snapshots. +""" +import copy +import json +import os +from pathlib import Path +import sys +import tempfile +import unittest + +ROOT = Path(__file__).resolve().parents[3] +sys.path.insert(0, str(ROOT / 'verification/aeneas')) +import admission +import drop_ownership +import prepare + +PROBE = os.environ.get('AENEAS_TRANSMUTE_PROBE') + + +def nodes(value): + if isinstance(value, dict): + yield value + for child in value.values(): + yield from nodes(child) + elif isinstance(value, list): + for child in value: + yield from nodes(child) + + +class ClosureTests(unittest.TestCase): + def fixture(self, edges, bodies=None): + checked = admission.Admission.__new__(admission.Admission) + bodies = bodies or {} + checked.functions = {i: {'item_meta': {'name': [ + {'Ident': [part, 0]} for part in + (admission.TRANSMUTE_COPY if i == 9 else 'owner' + str(i)).split('::')]}, + 'generics': {'types': [{'index': 0}, {'index': 1}]}, + 'body': bodies.get(i, {'Structured': {'body': {'statements': []}}})} + for i in {9, *edges, *(c for cs in edges.values() for c in cs)}} + checked.calls = [{'caller_def_id': owner, 'callee_def_id': child, + 'type_arguments': ['T0', 'T1']} + for owner, children in edges.items() for child in children] + return checked + + def test_single_choice_through_forwarders(self): + self.fixture({1: [2], 2: [9]}).audit_copy_closures() + + def test_direct_primitive_retains_nominal_manually_drop_endpoint(self): + checked = self.fixture({1: [9]}) + checked.calls[0]['type_arguments'] = [admission.MANUALLY_DROP + '', 'T1'] + checked.audit_copy_closures() + + def test_concrete_forwarding_fails_closed(self): + for arguments in (['u32', 'T1'], ['T0', 'u32'], ['ManuallyDrop', 'T1'], + [], ['T0', 'T2'], ['T0', 'T-1'], ['T0', 'T01']): + with self.subTest(arguments=arguments): + checked = self.fixture({1: [2], 2: [9]}) + checked.calls[0]['type_arguments'] = arguments + with self.assertRaisesRegex(ValueError, 'forwarding requires original type variables'): + checked.audit_copy_closures() + + def test_monomorphic_forwarder_fails_closed(self): + checked = self.fixture({1: [2], 2: [9]}) + checked.functions[1]['generics']['types'] = [] + with self.assertRaisesRegex(ValueError, 'forwarding requires original type variables'): + checked.audit_copy_closures() + + def test_monomorphic_copy_owner_fails_closed(self): + checked = self.fixture({1: [9]}) + checked.functions[1]['generics']['types'] = [] + with self.assertRaisesRegex(ValueError, 'local bodies must be type generic'): + checked.audit_copy_closures() + + def test_generic_forwarding_uses_actual_source_indices(self): + checked = self.fixture({1: [2], 2: [9]}) + checked.functions[1]['generics']['types'] = [{'index': 3}, {'index': 4}] + checked.calls[0]['type_arguments'] = ['T4', 'T3'] + checked.audit_copy_closures() + + def test_duplicate_calls_to_same_helper_count_twice(self): + with self.assertRaisesRegex(ValueError, 'multiple byte choices'): + self.fixture({1: [2, 2], 2: [9]}).audit_copy_closures() + + def test_mutual_recursion_reaching_copy(self): + with self.assertRaisesRegex(ValueError, 'recursive calls'): + self.fixture({1: [2], 2: [1, 9]}).audit_copy_closures() + + def test_structured_loop_reaching_copy(self): + with self.assertRaisesRegex(ValueError, 'body loop'): + self.fixture({1: [9]}, {1: {'Structured': { + 'body': {'kind': {'Loop': {'statements': []}}}}}}).audit_copy_closures() + + def test_cfg_cycle_reaching_copy(self): + with self.assertRaisesRegex(ValueError, 'CFG cycle'): + self.fixture({1: [9]}, {1: {'Unstructured': {'body': [ + {'terminator': {'kind': {'Goto': 0}}}]}}}).audit_copy_closures() + + def test_unrelated_loops_and_recursion_keep_existing_admission(self): + self.fixture({1: [9], 2: [2]}, {2: {'Structured': { + 'body': {'kind': {'Loop': {}}}}}}).audit_copy_closures() + + def test_generic_model_capture_follows_size_and_copy_forwarders(self): + source = ('public import Aeneas\n' + 'def sizes (S D : Type) : Result Bool := do\n' + ' let a ← core.mem.size_of S\n let b ← core.mem.size_of D\n' + ' ok (a = b)\n' + 'def helper {S D : Type} (x : S) : Result D := do\n' + ' core.mem.transmute_copy D x\n' + 'def caller {S D : Type} (x : S) : Result D := helper x\n') + result = prepare.retain_native_models(source) + self.assertNotIn('native_models def sizes', result) + for name in ('helper', 'caller'): + self.assertIn('native_models def ' + name, result) + + +@unittest.skipUnless(PROBE, 'Set AENEAS_TRANSMUTE_PROBE for compiler snapshot diagnostics') +class CompilerProbeTests(unittest.TestCase): + def setUp(self): + self.registry = json.loads((ROOT / 'verification/aeneas/external.json').read_text()) + self.snapshots = [] + for filename in ('probe.before.ullbc', 'probe.llbc'): + data = json.loads((Path(PROBE) / filename).read_text()) + options = data['translated']['options'] + # Preserve historical files; adapt only their reviewed option roster. + options['exclude'] = list(admission.EXCLUDED_PROVIDED_METHODS) + options['opaque'] = [row['rust'] for row in self.registry if row.get('opaque')] + options['opaque'] += [admission.INTERFACE_ONLY_VALIDATORS, + *admission.INTERFACE_ONLY_TYPES] + self.snapshots.append(data) + self.root = 'zerocopy::util::macro_util::aeneas_transmute_copy_caller_probe' + + @staticmethod + def diagnostic_empty_drop(function): + # Deliberately no kernel proof. This callback isolates admission guards; + # it is unsuitable for extraction or any successful verification report. + return {'function_def_id': function['def_id'], + 'body_sha256': drop_ownership.body_digest(function['body'])} + + def check(self, data, registry=None): + return admission.Admission(data, registry or self.registry, + ['zerocopy::IntoBytes', 'zerocopy::FromBytes'], + certify_drops=self.diagnostic_empty_drop).audit([self.root]) + + def test_both_real_compiler_stages_keep_ordered_endpoints_and_global_edge(self): + reports = [self.check(data) for data in self.snapshots] + self.assertEqual(reports[0]['calls'], reports[1]['calls']) + for report in reports: + row = next(row for row in report['calls'] + if row.get('callee') == admission.TRANSMUTE_COPY) + self.assertEqual(row['type_arguments'], [admission.MANUALLY_DROP + '', 'T1']) + self.assertEqual((row['caller_def_id'], row['callee_def_id']), (20, 23)) + global_read = next(row for row in report['calls'] if row.get('kind') == 'global') + self.assertEqual(global_read['callee_def_id'], 25) + self.assertEqual(global_read['type_arguments'], ['T0', 'T1']) + + def test_selected_endpoint_swap_and_region_change_fail_closed(self): + for data in self.snapshots: + for mutation in ('swap', 'region'): + bad = copy.deepcopy(data) + function = next(f for f in bad['translated']['fun_decls'] + if f and f['def_id'] == 20) + call = next(node['Regular'] for node in nodes(function['body']) + if node.get('Regular', {}).get('kind') == {'Fun': 23}) + if mutation == 'swap': + call['generics']['types'].reverse() + else: + call['generics']['regions'] = [] + with self.assertRaisesRegex(ValueError, 'transmute_copy endpoints or regions'): + self.check(bad) + + def test_duplicate_and_recursive_compiler_closures_fail_closed(self): + for data in self.snapshots: + bad = copy.deepcopy(data) + caller = bad['translated']['fun_decls'][11] + stage, body = admission.variant(caller['body']) + if stage == 'Structured': + statements = body['body']['statements'] + original = next(stmt for stmt in statements + if isinstance(stmt['kind'], dict) and 'Call' in stmt['kind']) + duplicate = copy.deepcopy(original) + duplicate['id'] = 100000 + statements.insert(statements.index(original), duplicate) + else: + blocks = body['body'] + original = next(block for block in blocks if + isinstance(block['terminator']['kind'], dict) and + 'Call' in block['terminator']['kind']) + blocks.append(copy.deepcopy(original)) + with self.assertRaisesRegex(ValueError, 'multiple byte choices'): + self.check(bad) + # Add a recursive call alongside the existing path to copy. + call = next(node['Regular'] for node in nodes(caller['body']) + if node.get('Regular', {}).get('kind') == {'Fun': 20}) + call['kind'] = {'Fun': 11} + with self.assertRaisesRegex(ValueError, 'recursive calls'): + self.check(bad) + + def test_signature_and_carrier_mutations_fail_closed(self): + for data in self.snapshots: + bad = copy.deepcopy(data) + bad['translated']['fun_decls'][23]['signature']['is_unsafe'] = False + with self.assertRaisesRegex(ValueError, 'No reviewed interpretation'): + self.check(bad) + for key, value in (('kind', {'Struct': []}), ('generics', { + 'types': [], 'regions': [], 'const_generics': []})): + bad = copy.deepcopy(data) + bad['translated']['type_decls'][6][key] = value + with self.assertRaisesRegex(ValueError, 'ManuallyDrop shape'): + self.check(bad) + + def test_registry_extension_and_external_body_are_exact(self): + for data in self.snapshots: + registry = copy.deepcopy(self.registry) + next(row for row in registry if row['rust'] == admission.TRANSMUTE_COPY)[ + 'interpretation_extension'] = 'unchecked' + with self.assertRaisesRegex(ValueError, 'external boundary changed'): + self.check(data, registry) + bad = copy.deepcopy(data) + bad['translated']['fun_decls'][23]['body'] = {'Intrinsic': {'name': 'transmute'}} + with self.assertRaisesRegex(ValueError, 'external boundary changed'): + self.check(bad) + + def test_native_template_signatures_are_checked(self): + evidence = {'stages': {'llbc': self.check(self.snapshots[1])}} + template = (Path(PROBE) / 'native/FunsExternal_Template.lean').read_text() + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) / 'Zerocopy' + directory.mkdir() + target = directory / 'FunsExternal_Template.lean' + target.write_text(template) + admission.check_translation(Path(tmp), evidence) + target.write_text(template.replace('Src → Result Dst', 'Dst → Result Src')) + with self.assertRaisesRegex(ValueError, 'generated failure-capable signature'): + admission.check_translation(Path(tmp), evidence) + + +if __name__ == '__main__': + unittest.main() diff --git a/verification/aeneas/tests/transmute_copy_audit_controls.py b/verification/aeneas/tests/transmute_copy_audit_controls.py new file mode 100644 index 0000000000..9f4e423c27 --- /dev/null +++ b/verification/aeneas/tests/transmute_copy_audit_controls.py @@ -0,0 +1,264 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Compile byte-copy mutants before challenging their independent binding audit. + +Only a private control-runner project may be changed. Providers retain their +original Raw type, so a type error cannot stand in for detecting a replacement +interpretation. Every command has durable evidence; finally restores sources, +rebuilds the original modules, and reruns the original audit. +""" +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 NativeProviderAudit +open Lean Elab +run_elab do + let contents ← IO.FS.readFile "bindings.json" + let .ok bindings := Json.parse contents | throwError "Invalid control bindings" + auditNativeProviders bindings +''' +GUARD_PROBE = '''import Zerocopy.Funs +open Aeneas.Std AeneasSpecs Zerocopy +-- Removing the guard also makes its simp arguments unused. Suppress that +-- linter here so only the unproved execution proposition rejects the mutant. +set_option linter.unusedSimpArgs false +example {Src Dst : Type} (source : IntoBytes Src) (destination : FromBytes Dst) + (src : Src) [RustModel Src] [RustModel Dst] (sourceSize destinationSize : Usize) + (hs : core.mem.size_of Src = .ok sourceSize) + (hd : core.mem.size_of Dst = .ok destinationSize) + (different : sourceSize ≠ destinationSize) : + util.macro_util.transmute_copy source destination src = .fail .assertionFailure := by + simp only [util.macro_util.transmute_copy, + PairPhantomDataPhantomData.Insts.ZerocopyUtilMacro_utilTransmute_copyStaticAssert.ASSERT, + hs, hd] + try simp [different, Aeneas.Std.massert] +''' +EXACT_PROVIDER = 'Provider-bearing call changed its exact retained provider' +ENDPOINTS = 'Provider-bearing calls changed original endpoints, owners, or multiplicity' +COPY = 'core::mem::transmute_copy' + + +def replace_once(text, before, after): + if text.count(before) != 1: + raise ValueError('Byte-copy mutation requires one exact source boundary: ' + before) + return text.replace(before, after) + + +def changed_provider(raw, field): + value = 'fun _ => []' if field == 'representationChoice' else 'fun _ => none' + return ('{ (inferInstance : AeneasSpecs.RustModel (' + raw + ')) with ' + + field + ' := ' + value + ' }') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--work', type=Path, required=True) + parser.add_argument('--runtime', type=Path, required=True) + parser.add_argument('--evidence', type=Path, required=True) + args = parser.parse_args() + work, runtime, output = (path.resolve() for path in + (args.work, args.runtime, args.evidence)) + 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 private: + raise ValueError('Byte-copy controls require a private control-runner project') + toolchain.validate(ROOT, runtime) + environment = toolchain.runtime_env(runtime) + environment['LEAN_NUM_THREADS'] = '2' + probe = work / 'TransmuteCopyAuditProbe.lean' + if probe.exists() or probe.is_symlink(): + raise ValueError('Byte-copy 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]) + for rust, raw in [('zerocopy::util::macro_util::transmute_copy', + 'Zerocopy.util.macro_util.transmute_copy'), + ('zerocopy::util::generic_transmute::transmute_copy_caller', + 'Zerocopy.util.generic_transmute.transmute_copy_caller')]: + if manifest['bindings'].get(rust, {}).get('raw') != raw: + raise ValueError('Byte-copy controls require the actual helper and caller roots') + for stage in ('before', 'llbc'): + calls = [row for row in manifest['admission']['stages'][stage]['calls'] + if row.get('callee') == COPY] + if len(calls) != 1 or calls[0]['type_arguments'] != [ + 'core::mem::manually_drop::ManuallyDrop', 'T1']: + raise ValueError('Byte-copy controls require the selected original generic endpoints') + output.mkdir(parents=True, exist_ok=False) + 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', '+NativeProviderAudit'] + audit = ['lake', '--old', 'env', 'lean', '-DwarningAsError=true', probe.name] + proof = ['lake', '--old', 'build', '+Proofs.GenericTransmute'] + + 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) + + def compiled_mutant(label, path, before, after, expected): + path.write_text(replace_once(originals[path].decode(), before, after)) + run(label + '-elaboration', build, fresh=True) + run(label + '-rejection', audit, expected) + restore_build('restored-' + label) + + try: + with probe.open('x') as stream: + stream.write(PROBE) + run('positive-elaboration', build, fresh=True) + run('positive-audit', audit) + run('positive-guard-proof', proof, fresh=True) + copy_call = ' core.mem.transmute_copy Dst src1\n' + for field in ('representationChoice', 'decode'): + compiled_mutant('copy-source-' + field, native, copy_call, + ' core.mem.transmute_copy Dst src1 (source := ' + + changed_provider('core.mem.manually_drop.ManuallyDrop Src', field) + ')\n', + EXACT_PROVIDER) + compiled_mutant('copy-destination-decode', native, copy_call, + ' core.mem.transmute_copy Dst src1 (destination := ' + + changed_provider('Dst', 'decode') + ')\n', EXACT_PROVIDER) + # Size queries retain the provider-free ABI interpretation. Swapping + # their original type arguments challenges the StaticAssert binding. + compiled_mutant('static-assert-size-endpoints', native, + ' let i ← core.mem.size_of Src\n let i1 ← core.mem.size_of Dst\n', + ' let i ← core.mem.size_of Dst\n let i1 ← core.mem.size_of Src\n', + 'Provider-bearing call changed an original Rust endpoint') + compiled_mutant('caller-source-provider', native, + ' util.macro_util.transmute_copy IntoBytesInst FromBytesInst src\n', + ' util.macro_util.transmute_copy IntoBytesInst FromBytesInst src\n' + ' (_nativeModel0 := ' + changed_provider('Src', 'decode') + ')\n', EXACT_PROVIDER) + constructor = ('def core.mem.manually_drop.ManuallyDrop.new {T : Type} (src : T) :\n' + ' Result (core.mem.manually_drop.ManuallyDrop T) := .ok ⟨src⟩\n') + compiled_mutant('constructor-result', external, constructor, + constructor.replace('(src : T)', '(_src : T)').replace('.ok ⟨src⟩', '.fail .undef'), + 'Byte-copy boundary core.mem.manually_drop.ManuallyDrop.new changed its whole signature or interpretation') + primitive = ' source.transmuteCopyResult destination src\n' + primitive_error = ('Byte-copy boundary core.mem.transmute_copy changed its whole ' + 'signature or interpretation') + signature = ('noncomputable def core.mem.transmute_copy {Src : Type} ' + '(Dst : Type) (src : Src)\n' + ' [source : AeneasSpecs.RustModel Src] ' + '[destination : AeneasSpecs.RustModel Dst] : Result Dst :=\n') + failing = (signature.replace('(src : Src)', '(_src : Src)') + .replace('[source :', '[_source :') + .replace('[destination :', '[_destination :') + ' .fail .undef\n') + compiled_mutant('copy-always-undef', external, signature + primitive, + failing, primitive_error) + compiled_mutant('copy-without-mathematical-guards', external, primitive, + ' match destination.representation with\n' + ' | none => .fail .undef\n' + ' | some decoder => Result.ofOption\n' + ' (decoder.run (source.representationChoice src)) .undef\n', primitive_error) + + # Equal-size success alone cannot detect a removed guard. Compile the + # mutated helper first, then require the independent unequal-size proof + # to fail. Its theorem promises assertionFailure, distinct from UB. + guard = (' let b ←\n' + ' PairPhantomDataPhantomData.Insts.ZerocopyUtilMacro_utilTransmute_copyStaticAssert.ASSERT\n' + ' Src\n Dst\n massert b\n') + probe.write_text(GUARD_PROBE) + run('positive-size-guard-proposition', audit) + native.write_text(replace_once(originals[native].decode(), guard, '')) + run('missing-size-guard-elaboration', build, fresh=True) + run('missing-size-guard-proof-rejection', audit, 'unsolved goals') + probe.write_text(PROBE) + restore_build('restored-size-guard') + run('restored-size-guard-proof', proof, fresh=True) + + mutant = copy.deepcopy(manifest) + next(row for row in mutant['admission']['stages']['llbc']['calls'] + if row.get('callee') == COPY)['type_arguments'].reverse() + bindings.write_text(json.dumps(mutant, indent=2) + '\n') + run('lowered-endpoint-rejection', audit, ENDPOINTS) + restore_sources() + run('restored-lowered-endpoint-audit', audit) + + mutant = copy.deepcopy(manifest) + for stage in ('before', 'llbc'): + next(row for row in mutant['admission']['stages'][stage]['calls'] + if row.get('callee') == COPY)['type_arguments'] = [ + 'core::mem::manually_drop::ManuallyDrop', 'T0'] + bindings.write_text(json.dumps(mutant, indent=2) + '\n') + run('both-endpoints-rejection', audit, + 'Provider-bearing call changed an original Rust endpoint') + restore_sources() + run('restored-both-endpoints-audit', audit) + + for kind in ('copy', 'global'): + mutant = copy.deepcopy(manifest) + for stage in ('before', 'llbc'): + rows = mutant['admission']['stages'][stage]['calls'] + matches = [row for row in rows if (row.get('callee') == COPY + if kind == 'copy' else row.get('kind') == 'global' and + 'transmute_copy' in row.get('caller', ''))] + if len(matches) != 1: + raise ValueError('Expected one original call witness for ' + kind) + rows.remove(matches[0]) + bindings.write_text(json.dumps(mutant, indent=2) + '\n') + run('missing-' + kind + '-witness-rejection', audit, + 'Unexpected provider-bearing native call') + restore_sources() + run('restored-' + kind + '-witness-audit', audit) + finally: + restore_sources() + if probe.exists(): + probe.write_text(PROBE) + try: + run('restored-positive-elaboration', build, fresh=True) + run('restored-positive-audit', audit) + run('restored-positive-guard-proof', proof, fresh=True) + 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/verification/aeneas/trait_invariants.py b/verification/aeneas/trait_invariants.py index dea4c6de91..aed405cca8 100644 --- a/verification/aeneas/trait_invariants.py +++ b/verification/aeneas/trait_invariants.py @@ -472,11 +472,15 @@ def bind_laws(annotations, work, final, before): if used_proofs != {(p['file'], p['syntax']) for p in getattr(annotations, 'trait_proofs', [])}: raise ValueError('An annotated implementation proof was not bound and checked') # Source roots and dependency dictionaries have different coverage rules. - # Only marked owners may be independently rooted; all local dictionaries - # of annotated traits, including unmarked dependencies, still need proofs. + # A function-root prefix can also select a nested implementation of an + # unannotated trait (for example a static assertion's private trait). Such + # dependencies are not invariant-proof markers. Restrict the root bijection + # to annotated traits; every local dictionary of those traits, including + # unmarked dependencies, still receives its proof obligation above. for crate in (before, final): rooted = {ident for ident, impl in declarations(crate, 'trait_impls').items() - if impl['item_meta'].get('started_from') is True} + if impl['item_meta'].get('started_from') is True + and impl['impl_trait']['id'] in by_id} if rooted != marked_owners: raise ValueError('Compiler implementation roots disagree with bound markers') return laws, implementations, dictionaries diff --git a/zerocopy/Cargo.toml b/zerocopy/Cargo.toml index 657a7981be..be7520fb59 100644 --- a/zerocopy/Cargo.toml +++ b/zerocopy/Cargo.toml @@ -57,6 +57,13 @@ exclude = [".*"] # `stdarch_x86_avx512` feature). no-zerocopy-simd-x86-avx12-1-89-0 = "1.89.0" +# From 1.83.0, const functions may borrow values with interior mutability. +# The generic source of our `transmute_copy` helper may have interior mutability: +# `IntoBytes` guarantees initialization, but does not require `Immutable`. The +# helper therefore needs `const_refs_to_cell`, even though the standard-library +# `transmute_copy` operation has been const since 1.74.0. +no-zerocopy-const-refs-to-cell-1-83-0 = "1.83.0" + # From 1.81.0, Rust supports the `core::error::Error` trait. no-zerocopy-core-error-1-81-0 = "1.81.0" diff --git a/zerocopy/src/util/generic_transmute.rs b/zerocopy/src/util/generic_transmute.rs new file mode 100644 index 0000000000..6980ec685b --- /dev/null +++ b/zerocopy/src/util/generic_transmute.rs @@ -0,0 +1,67 @@ +// 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. + +//! Generic owned conversions through the bounded standard-primitive helper. +//! +//! The independent generic caller keeps both trait bounds in the checked +//! execution closure rather than specializing the conversion to fixture types. + +use crate::{FromBytes, IntoBytes}; + +/// ```aeneas +/// spec transmute_copy_caller_spec +/// requires(raw) same_size : AeneasSpecs.RustModel.sameSize Src Dst +/// ensures(raw) result => AeneasSpecs.RustModel.byteCast src result +/// ``` +const fn transmute_copy_caller(src: Src) -> Dst { + super::macro_util::transmute_copy(src) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[derive(IntoBytes)] + #[repr(transparent)] + struct PanicsOnDrop(u8); + + impl Drop for PanicsOnDrop { + fn drop(&mut self) { + panic!("the consumed source must not be dropped"); + } + } + + #[test] + fn source_is_not_dropped() { + assert_eq!(transmute_copy_caller::<_, u8>(PanicsOnDrop(42)), 42); + } + + #[test] + fn const_and_runtime_conversions() { + const BYTES: [u8; 4] = transmute_copy_caller(0x1234_5678u32); + const VALUE: u32 = transmute_copy_caller(BYTES); + const EMPTY_BYTES: [u8; 0] = transmute_copy_caller(()); + const EMPTY_ALIGNED: [u64; 0] = transmute_copy_caller(EMPTY_BYTES); + const _: () = transmute_copy_caller(EMPTY_ALIGNED); + + assert_eq!(BYTES, 0x1234_5678u32.to_ne_bytes()); + assert_eq!(VALUE, 0x1234_5678); + assert_eq!(EMPTY_BYTES, []); + assert_eq!(EMPTY_ALIGNED, []); + + for value in [0, 1, 0x1234_5678, u32::MAX] { + let bytes: [u8; 4] = transmute_copy_caller(value); + assert_eq!(bytes, value.to_ne_bytes()); + assert_eq!(transmute_copy_caller::<_, u32>(bytes), value); + } + assert_eq!(transmute_copy_caller::<_, [u8; 0]>(()), []); + assert_eq!(transmute_copy_caller::<[u8; 0], [u64; 0]>([]), []); + transmute_copy_caller::<[u64; 0], ()>([]); + } +} diff --git a/zerocopy/src/util/macro_util.rs b/zerocopy/src/util/macro_util.rs index f374a089f4..c950f93ff0 100644 --- a/zerocopy/src/util/macro_util.rs +++ b/zerocopy/src/util/macro_util.rs @@ -510,6 +510,71 @@ pub const fn hash_name(name: &str) -> i128 { i128::from_ne_bytes(hash.to_ne_bytes()) } +/// Transfers the representation of `src` into an equal-sized `Dst`. +/// +/// The source is consumed without running its destructor. The source must have +/// initialized bytes, and every initialized representation must be valid for the +/// destination, as enforced by the trait bounds. +/// +/// # PME +/// +/// Instantiating this function produces a post-monomorphization error unless +/// `size_of::() == size_of::()`. `cargo check` alone may not diagnose +/// an unequal-size instantiation; code generation or const evaluation does. +/// +/// ```compile_fail,E0080 +/// use zerocopy::util::macro_util::transmute_copy; +/// const TOO_LARGE: u16 = transmute_copy(0u8); +/// ``` +/// +/// ```compile_fail,E0080 +/// use zerocopy::util::macro_util::transmute_copy; +/// const TOO_SMALL: u8 = transmute_copy(0u16); +/// ``` +/// +/// ```compile_fail,E0277 +/// use zerocopy::util::macro_util::transmute_copy; +/// // `bool` does not accept every initialized byte representation. +/// const INVALID_DESTINATION: bool = transmute_copy(0u8); +/// ``` +/// +/// ```compile_fail,E0277 +/// use core::mem::MaybeUninit; +/// use zerocopy::util::macro_util::transmute_copy; +/// // `MaybeUninit` does not promise initialized bytes. +/// const UNINITIALIZED_SOURCE: u8 = transmute_copy(MaybeUninit::uninit()); +/// ``` +/// +/// ```aeneas +/// spec transmute_copy_spec +/// requires(raw) same_size : AeneasSpecs.RustModel.sameSize Src Dst +/// ensures(raw) result => AeneasSpecs.RustModel.byteCast src result +/// ``` +#[cfg(not(no_zerocopy_const_refs_to_cell_1_83_0))] +#[cfg_attr(doc_cfg, doc(cfg(rust = "1.83.0")))] +#[inline(always)] +#[must_use] +pub const fn transmute_copy(src: Src) -> Dst { + static_assert!(Src, Dst => mem::size_of::() == mem::size_of::()); + let src = mem::ManuallyDrop::new(src); + // SAFETY: The static assertion establishes equal sizes, and ManuallyDrop + // preserves its inner type's layout and bit validity [1]. Thus the entire + // destination fits in this live source object. IntoBytes guarantees that + // the source representation consists of initialized bytes; FromBytes + // permits constructing Dst from any such bytes. Together these facts + // establish the readable extent and destination validity required by [2], + // including when both types have size zero. [2] permits stricter alignment + // for Dst, so no additional alignment bound is needed. + // + // [2] copies without moving the source. ManuallyDrop inhibits the source + // destructor [1], and the source is never accessed after the copy. Only the + // returned Dst remains available for use or destruction. + // + // [1] https://doc.rust-lang.org/1.74.0/core/mem/struct.ManuallyDrop.html + // [2] https://doc.rust-lang.org/1.74.0/core/mem/fn.transmute_copy.html + unsafe { mem::transmute_copy(&src) } +} + /// Attempts to transmute `Src` into `Dst`. /// /// A helper for `try_transmute!`. diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index 795cec98ce..0c4539426d 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -17,6 +17,9 @@ pub mod macro_util; mod allocation; pub(crate) mod bytewrite; mod checks; +#[cfg(not(no_zerocopy_const_refs_to_cell_1_83_0))] +#[allow(dead_code)] +mod generic_transmute; mod move_checks; #[cfg(target_endian = "little")] #[allow(dead_code)] diff --git a/zerocopy/tests/ui/transmute_mut.msrv.stderr b/zerocopy/tests/ui/transmute_mut.msrv.stderr index 2db6ccc4dc..433f2eab5b 100644 --- a/zerocopy/tests/ui/transmute_mut.msrv.stderr +++ b/zerocopy/tests/ui/transmute_mut.msrv.stderr @@ -82,9 +82,9 @@ error[E0599]: the method `transmute_mut` exists for struct `Wrap<&mut [u8], &mut 87 | const SRC_UNSIZED: &mut [u8; 1] = transmute_mut!(&mut [0u8][..]); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ method cannot be called on `Wrap<&mut [u8], &mut [u8; 1]>` due to unsatisfied trait bounds | - ::: $WORKSPACE/src/util/macro_util.rs:728:1 + ::: $WORKSPACE/src/util/macro_util.rs:793:1 | -728 | pub struct Wrap(pub Src, pub PhantomData); +793 | pub struct Wrap(pub Src, pub PhantomData); | --------------------------------------------------------- doesn't satisfy `Wrap<&mut [u8], &mut [u8; 1]>: TransmuteMutDst` | = note: the following trait bounds were not satisfied: diff --git a/zerocopy/tests/ui/transmute_mut.nightly.stderr b/zerocopy/tests/ui/transmute_mut.nightly.stderr index c590ad005e..40c9950f54 100644 --- a/zerocopy/tests/ui/transmute_mut.nightly.stderr +++ b/zerocopy/tests/ui/transmute_mut.nightly.stderr @@ -34,13 +34,13 @@ help: the trait `FromBytes` is not implemented for `DstA` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::transmute_mut` - --> src/util/macro_util.rs:848:14 + --> src/util/macro_util.rs:913:14 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -845 | pub fn transmute_mut(self) -> &'a mut Dst +910 | pub fn transmute_mut(self) -> &'a mut Dst ... -848 | Dst: FromBytes + IntoBytes, +913 | Dst: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::transmute_mut` = note: this error originates in the macro `transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -60,13 +60,13 @@ help: the trait `IntoBytes` is not implemented for `DstB` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::transmute_mut` - --> src/util/macro_util.rs:848:26 + --> src/util/macro_util.rs:913:26 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -845 | pub fn transmute_mut(self) -> &'a mut Dst +910 | pub fn transmute_mut(self) -> &'a mut Dst ... -848 | Dst: FromBytes + IntoBytes, +913 | Dst: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::transmute_mut` = note: this error originates in the macro `transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -130,13 +130,13 @@ help: the trait `FromBytes` is not implemented for `SrcC` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::transmute_mut` - --> src/util/macro_util.rs:847:14 + --> src/util/macro_util.rs:912:14 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -845 | pub fn transmute_mut(self) -> &'a mut Dst -846 | where -847 | Src: FromBytes + IntoBytes, +910 | pub fn transmute_mut(self) -> &'a mut Dst +911 | where +912 | Src: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::transmute_mut` = note: this error originates in the macro `transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -156,13 +156,13 @@ help: the trait `IntoBytes` is not implemented for `SrcD` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::transmute_mut` - --> src/util/macro_util.rs:847:26 + --> src/util/macro_util.rs:912:26 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -845 | pub fn transmute_mut(self) -> &'a mut Dst -846 | where -847 | Src: FromBytes + IntoBytes, +910 | pub fn transmute_mut(self) -> &'a mut Dst +911 | where +912 | Src: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::transmute_mut` = note: this error originates in the macro `transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -172,9 +172,9 @@ error[E0599]: the method `transmute_mut` exists for struct `zerocopy::util::macr 87 | const SRC_UNSIZED: &mut [u8; 1] = transmute_mut!(&mut [0u8][..]); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | - ::: src/util/macro_util.rs:728:1 + ::: src/util/macro_util.rs:793:1 | -728 | pub struct Wrap(pub Src, pub PhantomData); +793 | pub struct Wrap(pub Src, pub PhantomData); | ------------------------- doesn't satisfy `_: TransmuteMutDst<'_>` | = note: the following trait bounds were not satisfied: diff --git a/zerocopy/tests/ui/transmute_mut.stable.stderr b/zerocopy/tests/ui/transmute_mut.stable.stderr index a86187cae2..784cee9cc5 100644 --- a/zerocopy/tests/ui/transmute_mut.stable.stderr +++ b/zerocopy/tests/ui/transmute_mut.stable.stderr @@ -34,12 +34,12 @@ help: the trait `FromBytes` is not implemented for `DstA` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::transmute_mut` - --> src/util/macro_util.rs:848:14 + --> src/util/macro_util.rs:913:14 | -845 | pub fn transmute_mut(self) -> &'a mut Dst +910 | pub fn transmute_mut(self) -> &'a mut Dst | ------------- required by a bound in this associated function ... -848 | Dst: FromBytes + IntoBytes, +913 | Dst: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::transmute_mut` = note: this error originates in the macro `transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -59,12 +59,12 @@ help: the trait `IntoBytes` is not implemented for `DstB` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::transmute_mut` - --> src/util/macro_util.rs:848:26 + --> src/util/macro_util.rs:913:26 | -845 | pub fn transmute_mut(self) -> &'a mut Dst +910 | pub fn transmute_mut(self) -> &'a mut Dst | ------------- required by a bound in this associated function ... -848 | Dst: FromBytes + IntoBytes, +913 | Dst: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::transmute_mut` = note: this error originates in the macro `transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -128,12 +128,12 @@ help: the trait `FromBytes` is not implemented for `SrcC` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::transmute_mut` - --> src/util/macro_util.rs:847:14 + --> src/util/macro_util.rs:912:14 | -845 | pub fn transmute_mut(self) -> &'a mut Dst +910 | pub fn transmute_mut(self) -> &'a mut Dst | ------------- required by a bound in this associated function -846 | where -847 | Src: FromBytes + IntoBytes, +911 | where +912 | Src: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::transmute_mut` = note: this error originates in the macro `transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -153,12 +153,12 @@ help: the trait `IntoBytes` is not implemented for `SrcD` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::transmute_mut` - --> src/util/macro_util.rs:847:26 + --> src/util/macro_util.rs:912:26 | -845 | pub fn transmute_mut(self) -> &'a mut Dst +910 | pub fn transmute_mut(self) -> &'a mut Dst | ------------- required by a bound in this associated function -846 | where -847 | Src: FromBytes + IntoBytes, +911 | where +912 | Src: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::transmute_mut` = note: this error originates in the macro `transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -168,9 +168,9 @@ error[E0599]: the method `transmute_mut` exists for struct `zerocopy::util::macr 87 | const SRC_UNSIZED: &mut [u8; 1] = transmute_mut!(&mut [0u8][..]); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | - ::: src/util/macro_util.rs:728:1 + ::: src/util/macro_util.rs:793:1 | -728 | pub struct Wrap(pub Src, pub PhantomData); +793 | pub struct Wrap(pub Src, pub PhantomData); | ------------------------- doesn't satisfy `_: TransmuteMutDst<'_>` | = note: the following trait bounds were not satisfied: diff --git a/zerocopy/tests/ui/transmute_ref.msrv.stderr b/zerocopy/tests/ui/transmute_ref.msrv.stderr index b65096ffbc..a5b4edd92b 100644 --- a/zerocopy/tests/ui/transmute_ref.msrv.stderr +++ b/zerocopy/tests/ui/transmute_ref.msrv.stderr @@ -188,9 +188,9 @@ error[E0599]: the method `transmute_ref` exists for struct `Wrap<&[u8], &[u8; 1] 84 | const SRC_UNSIZED: &[u8; 1] = transmute_ref!(&[0u8][..]); | ^^^^^^^^^^^^^^^^^^^^^^^^^^ method cannot be called on `Wrap<&[u8], &[u8; 1]>` due to unsatisfied trait bounds | - ::: $WORKSPACE/src/util/macro_util.rs:728:1 + ::: $WORKSPACE/src/util/macro_util.rs:793:1 | -728 | pub struct Wrap(pub Src, pub PhantomData); +793 | pub struct Wrap(pub Src, pub PhantomData); | --------------------------------------------------------- doesn't satisfy `Wrap<&[u8], &[u8; 1]>: TransmuteRefDst` | = note: the following trait bounds were not satisfied: diff --git a/zerocopy/tests/ui/transmute_ref.nightly.stderr b/zerocopy/tests/ui/transmute_ref.nightly.stderr index e77dd37414..f3fd230739 100644 --- a/zerocopy/tests/ui/transmute_ref.nightly.stderr +++ b/zerocopy/tests/ui/transmute_ref.nightly.stderr @@ -330,9 +330,9 @@ error[E0599]: the method `transmute_ref` exists for struct `zerocopy::util::macr 84 | const SRC_UNSIZED: &[u8; 1] = transmute_ref!(&[0u8][..]); | ^^^^^^^^^^^^^^^^^^^^^^^^^^ | - ::: src/util/macro_util.rs:728:1 + ::: src/util/macro_util.rs:793:1 | -728 | pub struct Wrap(pub Src, pub PhantomData); +793 | pub struct Wrap(pub Src, pub PhantomData); | ------------------------- doesn't satisfy `_: TransmuteRefDst<'_>` | = note: the following trait bounds were not satisfied: diff --git a/zerocopy/tests/ui/transmute_ref.stable.stderr b/zerocopy/tests/ui/transmute_ref.stable.stderr index e0ef6aa36d..606e398e72 100644 --- a/zerocopy/tests/ui/transmute_ref.stable.stderr +++ b/zerocopy/tests/ui/transmute_ref.stable.stderr @@ -306,9 +306,9 @@ error[E0599]: the method `transmute_ref` exists for struct `zerocopy::util::macr 84 | const SRC_UNSIZED: &[u8; 1] = transmute_ref!(&[0u8][..]); | ^^^^^^^^^^^^^^^^^^^^^^^^^^ | - ::: src/util/macro_util.rs:728:1 + ::: src/util/macro_util.rs:793:1 | -728 | pub struct Wrap(pub Src, pub PhantomData); +793 | pub struct Wrap(pub Src, pub PhantomData); | ------------------------- doesn't satisfy `_: TransmuteRefDst<'_>` | = note: the following trait bounds were not satisfied: diff --git a/zerocopy/tests/ui/try_transmute.msrv.stderr b/zerocopy/tests/ui/try_transmute.msrv.stderr index 9b761bb87b..aa1b479c43 100644 --- a/zerocopy/tests/ui/try_transmute.msrv.stderr +++ b/zerocopy/tests/ui/try_transmute.msrv.stderr @@ -5,9 +5,9 @@ error[E0277]: the trait bound `NotZerocopy: TryFromBytes` is not satisfied | ^^^^^^^^^^^^^^^^^^^^^^^ the trait `TryFromBytes` is not implemented for `NotZerocopy` | note: required by a bound in `try_transmute` - --> $WORKSPACE/src/util/macro_util.rs:528:10 + --> $WORKSPACE/src/util/macro_util.rs:593:10 | -528 | Dst: TryFromBytes, +593 | Dst: TryFromBytes, | ^^^^^^^^^^^^ required by this bound in `try_transmute` = note: this error originates in the macro `try_transmute` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -43,9 +43,9 @@ error[E0277]: the trait bound `NotZerocopy: IntoBytes` is not satisfied | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `IntoBytes` is not implemented for `NotZerocopy` | note: required by a bound in `try_transmute` - --> $WORKSPACE/src/util/macro_util.rs:527:10 + --> $WORKSPACE/src/util/macro_util.rs:592:10 | -527 | Src: IntoBytes, +592 | Src: IntoBytes, | ^^^^^^^^^ required by this bound in `try_transmute` = note: this error originates in the macro `try_transmute` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/zerocopy/tests/ui/try_transmute.nightly.stderr b/zerocopy/tests/ui/try_transmute.nightly.stderr index 97889ef135..ad244dc705 100644 --- a/zerocopy/tests/ui/try_transmute.nightly.stderr +++ b/zerocopy/tests/ui/try_transmute.nightly.stderr @@ -37,11 +37,11 @@ help: the trait `TryFromBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::try_transmute` - --> src/util/macro_util.rs:528:10 + --> src/util/macro_util.rs:593:10 | -525 | pub fn try_transmute(src: Src) -> Result> +590 | pub fn try_transmute(src: Src) -> Result> ... -528 | Dst: TryFromBytes, +593 | Dst: TryFromBytes, | ^^^^^^^^^^^^ required by this bound in `try_transmute` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console @@ -111,11 +111,11 @@ help: the trait `IntoBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::try_transmute` - --> src/util/macro_util.rs:527:10 + --> src/util/macro_util.rs:592:10 | -525 | pub fn try_transmute(src: Src) -> Result> -526 | where -527 | Src: IntoBytes, +590 | pub fn try_transmute(src: Src) -> Result> +591 | where +592 | Src: IntoBytes, | ^^^^^^^^^ required by this bound in `try_transmute` = note: this error originates in the macro `try_transmute` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/zerocopy/tests/ui/try_transmute.stable.stderr b/zerocopy/tests/ui/try_transmute.stable.stderr index b8e42be31d..a11f064cef 100644 --- a/zerocopy/tests/ui/try_transmute.stable.stderr +++ b/zerocopy/tests/ui/try_transmute.stable.stderr @@ -37,12 +37,12 @@ help: the trait `TryFromBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::try_transmute` - --> src/util/macro_util.rs:528:10 + --> src/util/macro_util.rs:593:10 | -525 | pub fn try_transmute(src: Src) -> Result> +590 | pub fn try_transmute(src: Src) -> Result> | ------------- required by a bound in this function ... -528 | Dst: TryFromBytes, +593 | Dst: TryFromBytes, | ^^^^^^^^^^^^ required by this bound in `try_transmute` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console @@ -88,12 +88,12 @@ help: the trait `IntoBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::try_transmute` - --> src/util/macro_util.rs:527:10 + --> src/util/macro_util.rs:592:10 | -525 | pub fn try_transmute(src: Src) -> Result> +590 | pub fn try_transmute(src: Src) -> Result> | ------------- required by a bound in this function -526 | where -527 | Src: IntoBytes, +591 | where +592 | Src: IntoBytes, | ^^^^^^^^^ required by this bound in `try_transmute` = note: this error originates in the macro `try_transmute` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/zerocopy/tests/ui/try_transmute_mut.nightly.stderr b/zerocopy/tests/ui/try_transmute_mut.nightly.stderr index 682156afbd..8054e96376 100644 --- a/zerocopy/tests/ui/try_transmute_mut.nightly.stderr +++ b/zerocopy/tests/ui/try_transmute_mut.nightly.stderr @@ -14,13 +14,13 @@ help: the trait `TryFromBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:871:14 + --> src/util/macro_util.rs:936:14 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> ... -871 | Dst: TryFromBytes + IntoBytes, +936 | Dst: TryFromBytes + IntoBytes, | ^^^^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console @@ -42,13 +42,13 @@ help: the trait `IntoBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:871:29 + --> src/util/macro_util.rs:936:29 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> ... -871 | Dst: TryFromBytes + IntoBytes, +936 | Dst: TryFromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -139,13 +139,13 @@ help: the trait `FromBytes` is not implemented for `SrcA` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:870:14 + --> src/util/macro_util.rs:935:14 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> -869 | where -870 | Src: FromBytes + IntoBytes, +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +934 | where +935 | Src: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -165,13 +165,13 @@ help: the trait `IntoBytes` is not implemented for `DstA` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:871:29 + --> src/util/macro_util.rs:936:29 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> ... -871 | Dst: TryFromBytes + IntoBytes, +936 | Dst: TryFromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -191,13 +191,13 @@ help: the trait `IntoBytes` is not implemented for `SrcB` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:870:26 + --> src/util/macro_util.rs:935:26 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> -869 | where -870 | Src: FromBytes + IntoBytes, +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +934 | where +935 | Src: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -217,13 +217,13 @@ help: the trait `IntoBytes` is not implemented for `DstB` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:871:29 + --> src/util/macro_util.rs:936:29 | -834 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { +899 | impl<'a, Src, Dst> Wrap<&'a mut Src, &'a mut Dst> { ... -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> ... -871 | Dst: TryFromBytes + IntoBytes, +936 | Dst: TryFromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/zerocopy/tests/ui/try_transmute_mut.stable.stderr b/zerocopy/tests/ui/try_transmute_mut.stable.stderr index ecf7d48e6d..b4259bbe2f 100644 --- a/zerocopy/tests/ui/try_transmute_mut.stable.stderr +++ b/zerocopy/tests/ui/try_transmute_mut.stable.stderr @@ -14,12 +14,12 @@ help: the trait `TryFromBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:871:14 + --> src/util/macro_util.rs:936:14 | -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> | ----------------- required by a bound in this associated function ... -871 | Dst: TryFromBytes + IntoBytes, +936 | Dst: TryFromBytes + IntoBytes, | ^^^^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console @@ -41,12 +41,12 @@ help: the trait `IntoBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:871:29 + --> src/util/macro_util.rs:936:29 | -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> | ----------------- required by a bound in this associated function ... -871 | Dst: TryFromBytes + IntoBytes, +936 | Dst: TryFromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -113,12 +113,12 @@ help: the trait `FromBytes` is not implemented for `SrcA` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:870:14 + --> src/util/macro_util.rs:935:14 | -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> | ----------------- required by a bound in this associated function -869 | where -870 | Src: FromBytes + IntoBytes, +934 | where +935 | Src: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -138,12 +138,12 @@ help: the trait `IntoBytes` is not implemented for `DstA` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:871:29 + --> src/util/macro_util.rs:936:29 | -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> | ----------------- required by a bound in this associated function ... -871 | Dst: TryFromBytes + IntoBytes, +936 | Dst: TryFromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -163,12 +163,12 @@ help: the trait `IntoBytes` is not implemented for `SrcB` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:870:26 + --> src/util/macro_util.rs:935:26 | -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> | ----------------- required by a bound in this associated function -869 | where -870 | Src: FromBytes + IntoBytes, +934 | where +935 | Src: FromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -188,12 +188,12 @@ help: the trait `IntoBytes` is not implemented for `DstB` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a mut Src, &'a mut Dst>::try_transmute_mut` - --> src/util/macro_util.rs:871:29 + --> src/util/macro_util.rs:936:29 | -868 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> +933 | pub fn try_transmute_mut(self) -> Result<&'a mut Dst, ValidityError<&'a mut Src, Dst>> | ----------------- required by a bound in this associated function ... -871 | Dst: TryFromBytes + IntoBytes, +936 | Dst: TryFromBytes + IntoBytes, | ^^^^^^^^^ required by this bound in `Wrap::<&mut Src, &mut Dst>::try_transmute_mut` = note: this error originates in the macro `try_transmute_mut` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/zerocopy/tests/ui/try_transmute_ref.nightly.stderr b/zerocopy/tests/ui/try_transmute_ref.nightly.stderr index 00a0cd55f2..c5f7df536c 100644 --- a/zerocopy/tests/ui/try_transmute_ref.nightly.stderr +++ b/zerocopy/tests/ui/try_transmute_ref.nightly.stderr @@ -47,13 +47,13 @@ help: the trait `TryFromBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a Src, &'a Dst>::try_transmute_ref` - --> src/util/macro_util.rs:791:14 + --> src/util/macro_util.rs:856:14 | -748 | impl<'a, Src, Dst> Wrap<&'a Src, &'a Dst> { +813 | impl<'a, Src, Dst> Wrap<&'a Src, &'a Dst> { ... -788 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> +853 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> ... -791 | Dst: TryFromBytes + Immutable, +856 | Dst: TryFromBytes + Immutable, | ^^^^^^^^^^^^ required by this bound in `Wrap::<&Src, &Dst>::try_transmute_ref` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console @@ -75,13 +75,13 @@ help: the trait `Immutable` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a Src, &'a Dst>::try_transmute_ref` - --> src/util/macro_util.rs:791:29 + --> src/util/macro_util.rs:856:29 | -748 | impl<'a, Src, Dst> Wrap<&'a Src, &'a Dst> { +813 | impl<'a, Src, Dst> Wrap<&'a Src, &'a Dst> { ... -788 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> +853 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> ... -791 | Dst: TryFromBytes + Immutable, +856 | Dst: TryFromBytes + Immutable, | ^^^^^^^^^ required by this bound in `Wrap::<&Src, &Dst>::try_transmute_ref` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console @@ -174,13 +174,13 @@ help: the trait `IntoBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a Src, &'a Dst>::try_transmute_ref` - --> src/util/macro_util.rs:790:14 + --> src/util/macro_util.rs:855:14 | -748 | impl<'a, Src, Dst> Wrap<&'a Src, &'a Dst> { +813 | impl<'a, Src, Dst> Wrap<&'a Src, &'a Dst> { ... -788 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> -789 | where -790 | Src: IntoBytes + Immutable, +853 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> +854 | where +855 | Src: IntoBytes + Immutable, | ^^^^^^^^^ required by this bound in `Wrap::<&Src, &Dst>::try_transmute_ref` = note: this error originates in the macro `try_transmute_ref` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -200,13 +200,13 @@ help: the trait `Immutable` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a Src, &'a Dst>::try_transmute_ref` - --> src/util/macro_util.rs:790:26 + --> src/util/macro_util.rs:855:26 | -748 | impl<'a, Src, Dst> Wrap<&'a Src, &'a Dst> { +813 | impl<'a, Src, Dst> Wrap<&'a Src, &'a Dst> { ... -788 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> -789 | where -790 | Src: IntoBytes + Immutable, +853 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> +854 | where +855 | Src: IntoBytes + Immutable, | ^^^^^^^^^ required by this bound in `Wrap::<&Src, &Dst>::try_transmute_ref` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console diff --git a/zerocopy/tests/ui/try_transmute_ref.stable.stderr b/zerocopy/tests/ui/try_transmute_ref.stable.stderr index c8093d5496..ce2967cfd2 100644 --- a/zerocopy/tests/ui/try_transmute_ref.stable.stderr +++ b/zerocopy/tests/ui/try_transmute_ref.stable.stderr @@ -47,12 +47,12 @@ help: the trait `TryFromBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a Src, &'a Dst>::try_transmute_ref` - --> src/util/macro_util.rs:791:14 + --> src/util/macro_util.rs:856:14 | -788 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> +853 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> | ----------------- required by a bound in this associated function ... -791 | Dst: TryFromBytes + Immutable, +856 | Dst: TryFromBytes + Immutable, | ^^^^^^^^^^^^ required by this bound in `Wrap::<&Src, &Dst>::try_transmute_ref` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console @@ -74,12 +74,12 @@ help: the trait `Immutable` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a Src, &'a Dst>::try_transmute_ref` - --> src/util/macro_util.rs:791:29 + --> src/util/macro_util.rs:856:29 | -788 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> +853 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> | ----------------- required by a bound in this associated function ... -791 | Dst: TryFromBytes + Immutable, +856 | Dst: TryFromBytes + Immutable, | ^^^^^^^^^ required by this bound in `Wrap::<&Src, &Dst>::try_transmute_ref` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console @@ -148,12 +148,12 @@ help: the trait `IntoBytes` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a Src, &'a Dst>::try_transmute_ref` - --> src/util/macro_util.rs:790:14 + --> src/util/macro_util.rs:855:14 | -788 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> +853 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> | ----------------- required by a bound in this associated function -789 | where -790 | Src: IntoBytes + Immutable, +854 | where +855 | Src: IntoBytes + Immutable, | ^^^^^^^^^ required by this bound in `Wrap::<&Src, &Dst>::try_transmute_ref` = note: this error originates in the macro `try_transmute_ref` (in Nightly builds, run with -Z macro-backtrace for more info) @@ -173,12 +173,12 @@ help: the trait `Immutable` is not implemented for `NotZerocopy` $IMPLEMENTATION_SAMPLES and $OTHER_TYPES others note: required by a bound in `zerocopy::util::macro_util::Wrap::<&'a Src, &'a Dst>::try_transmute_ref` - --> src/util/macro_util.rs:790:26 + --> src/util/macro_util.rs:855:26 | -788 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> +853 | pub fn try_transmute_ref(self) -> Result<&'a Dst, ValidityError<&'a Src, Dst>> | ----------------- required by a bound in this associated function -789 | where -790 | Src: IntoBytes + Immutable, +854 | where +855 | Src: IntoBytes + Immutable, | ^^^^^^^^^ required by this bound in `Wrap::<&Src, &Dst>::try_transmute_ref` = note: the full name for the type has been written to '/long-type-HASH.txt' = note: consider using `--verbose` to print the full type name to the console