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