From c3dd969502625baaa6152e90d31ca5c6f37269d3 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 14 Oct 2026 23:41:29 -0400 Subject: [PATCH] Prove FromBytes and FromZeros construction invariants FromBytes must admit every initialized representation, and FromZeros must admit the zero representation. Both promises must also establish the constructed value's library invariants. Give the traits inline laws that require physical and mathematical decoding through the same provider. Prove the marked unit, u8, u32 and generic array impls for both traits, and the Boolean FromZeros impl. Derive zero admission from complete admission. Retain decoder providers when native generic bodies need an external interpretation, preserving the original Rust argument prefix. Check default method ownership and each compiled zeroed call against compiler evidence. Required pointer-based validators retain their signatures but have no execution model: admission rejects calls and their Lean stubs return undef. The opaque pointer carrier supplies only a checked data-type signature. Test missing physical models, rejected library values, Boolean incompleteness, nonzero rejection, and empty or zero-sized arrays. Both total and partial contracts reject forbidden construction even for True posts. Applying the models to Rust retains the documented representation premise; compiler assertions challenge the concrete byte widths. gherrit-pr-id: Gfvlqdcxuhzqx47spnjvui7b6hommtdwk Agent-authored-by: AI agent acting on joshlf's behalf --- tools/aeneas-inline/src/main.rs | 54 +++- verification/aeneas/LOWERING_AUDIT.md | 29 ++ verification/aeneas/README.md | 54 +++- verification/aeneas/admission.py | 153 ++++++++- verification/aeneas/external.json | 3 +- verification/aeneas/golden/Funs.lean | 275 +++++++++++++++- .../aeneas/golden/FunsExternal_Template.lean | 62 ++++ verification/aeneas/golden/Types.lean | 91 +++++- .../aeneas/golden/TypesExternal_Template.lean | 6 + verification/aeneas/inline.py | 35 ++- verification/aeneas/lean/Check.lean | 48 ++- verification/aeneas/lean/DeriveModels.lean | 21 +- verification/aeneas/lean/NativeModels.lean | 143 +++++++++ .../aeneas/lean/NativeModelsTests.lean | 152 +++++++++ .../aeneas/lean/Proofs/FromBytes.lean | 74 +++++ verification/aeneas/lean/RustModel.lean | 96 ++++++ .../aeneas/lean/RustRepresentation.lean | 190 +++++++++++ .../aeneas/lean/RustRepresentationTests.lean | 124 ++++++++ verification/aeneas/lean/SpecsSyntax.lean | 37 ++- .../aeneas/lean/TraitLawsSupport.lean | 77 ++++- .../aeneas/lean/Zerocopy/FunsExternal.lean | 51 +++ .../aeneas/lean/Zerocopy/TypesExternal.lean | 6 + verification/aeneas/lean/ZeroedAudit.lean | 207 ++++++++++++ .../aeneas/negative-control-extraction.sh | 7 + verification/aeneas/prepare.py | 42 +++ .../aeneas/projections/ModelShapes.lean | 10 +- verification/aeneas/projections/Models.lean | 15 +- .../aeneas/projections/TraitLaws.lean | 14 + .../aeneas/tests/producer-controls.sh | 16 +- .../aeneas/tests/std_transmute_controls.py | 6 +- verification/aeneas/tests/test_admission.py | 7 +- .../aeneas/tests/test_default_methods.py | 295 ++++++++++++++++++ verification/aeneas/tests/test_inline.py | 58 +++- verification/aeneas/trait_invariants.py | 114 ++++++- zerocopy/src/impls.rs | 50 ++- zerocopy/src/layout/mod.rs | 8 + zerocopy/src/lib.rs | 8 + .../ui/transmute-ptr-to-usize.nightly.stderr | 18 +- .../ui/transmute-ptr-to-usize.stable.stderr | 16 +- 39 files changed, 2569 insertions(+), 103 deletions(-) create mode 100644 verification/aeneas/lean/NativeModels.lean create mode 100644 verification/aeneas/lean/NativeModelsTests.lean create mode 100644 verification/aeneas/lean/Proofs/FromBytes.lean create mode 100644 verification/aeneas/lean/RustRepresentation.lean create mode 100644 verification/aeneas/lean/RustRepresentationTests.lean create mode 100644 verification/aeneas/lean/ZeroedAudit.lean create mode 100644 verification/aeneas/tests/test_default_methods.py diff --git a/tools/aeneas-inline/src/main.rs b/tools/aeneas-inline/src/main.rs index 67d648e9b8..aa8e709321 100644 --- a/tools/aeneas-inline/src/main.rs +++ b/tools/aeneas-inline/src/main.rs @@ -241,7 +241,10 @@ impl Functions<'_> { if let syn::ReturnType::Type(_, ty) = &sig.output { supported &= !unsupported_borrow(ty, false); } - let (bounds, bounds_supported) = trait_bounds(&sig.generics); + let (bounds, bounds_supported) = trait_bounds_with_context( + &sig.generics, + if method { &self.impl_generics } else { &[] }, + ); supported &= bounds_supported; let mut generics = if method { self.impl_generics.clone() } else { Vec::new() }; for parameter in &sig.generics.params { @@ -304,6 +307,10 @@ fn declaration_start( // These spellings propose source ownership only. The compiler's resolved // predicates, not names from syn, decide which trait dictionary is required. fn trait_bounds(generics: &syn::Generics) -> (Vec, bool) { + trait_bounds_with_context(generics, &[]) +} + +fn trait_bounds_with_context(generics: &syn::Generics, context: &[String]) -> (Vec, bool) { fn bound(subject: &str, bound: &syn::TypeParamBound) -> Option { let syn::TypeParamBound::Trait(bound) = bound else { return None }; if bound.lifetimes.is_some() @@ -345,7 +352,8 @@ fn trait_bounds(generics: &syn::Generics) -> (Vec, bool) { continue; }; supported &= predicate.lifetimes.is_none() - && generics.type_params().any(|p| p.ident == *subject); + && (generics.type_params().any(|p| p.ident == *subject) + || context.iter().any(|name| subject == name)); for predicate in &predicate.bounds { match bound(&subject.to_string(), predicate) { Some(value) => bounds.push(value), @@ -729,6 +737,31 @@ impl<'ast> Visit<'ast> for Functions<'_> { "supported": self.unsupported == 0 && item.generics.params.is_empty() && item.generics.where_clause.is_none(), })); + // A provided method owns a real function body. Its implicit Self type + // and enclosing trait come from this item, not from a guessed path. + // Report these bodies separately so their specs receive the same + // closed annotation census as free functions and inherent methods. + let previous_generics = self.impl_generics.clone(); + self.impl_generics = std::iter::once("Self".to_string()) + .chain(item.generics.type_params().map(|p| p.ident.to_string())) + .collect(); + self.modules.push(item.ident.to_string()); + for member in &item.items { + if let syn::TraitItem::Fn(method) = member { + if let Some(body) = &method.default { + self.function( + &method.sig, + body, + &method.attrs, + true, + &syn::Visibility::Inherited, + ); + self.functions.last_mut().unwrap()["default_trait"] = json!(path.join("::")); + } + } + } + self.modules.pop(); + self.impl_generics = previous_generics; self.unsupported += 1; visit::visit_item_trait(self, item); self.unsupported -= 1; @@ -909,6 +942,23 @@ mod tests { } } + #[test] + fn provided_method_retains_enclosing_self_in_where_clauses() { + let value = inspect( + "mod nested { unsafe trait Marker { fn required(); + fn make() -> Self where Self: Sized { panic!() } + } }", + ) + .unwrap(); + let functions = value["functions"].as_array().unwrap(); + assert_eq!(functions.len(), 1); + assert_eq!(functions[0]["path"], "nested::Marker::make"); + assert_eq!(functions[0]["default_trait"], "nested::Marker"); + assert_eq!(functions[0]["generics"], json!(["Self"])); + assert_eq!(functions[0]["trait_bounds"], json!([{"subject": "Self", "trait": "Sized"}])); + assert_eq!(functions[0]["supported"], true); + } + #[test] fn borrow_policy_distinguishes_shared_inputs_from_outputs_and_fields() { for (ty, input_supported) in [ diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md index 5eeb79b31c..70bd350674 100644 --- a/verification/aeneas/LOWERING_AUDIT.md +++ b/verification/aeneas/LOWERING_AUDIT.md @@ -224,6 +224,35 @@ trait objects. A missing child representation remains unavailable through its wrapper; an available child decoder must carry its actual correspondence and initialization premise. +### Zero construction and construction-trait laws + +`FromBytes` and `FromZeros` consume the same decoder-correspondence premises +above. Their additional mathematical decoding condition records library +validity, rather than treating bit validity as sufficient for every invariant. +The selected nine impl proofs cover unit, u8, u32, Boolean zero construction, +and generic arrays. They do not certify the other construction-trait impls. + +The `core::mem::zeroed` interpretation uses the selected provider's physical +width, all initialized zero bytes, and that provider's mathematical decoder. +Applying it to Rust additionally assumes the selected physical interpretation +has the actual Rust width and represents the resulting Rust value. The existing +primitive and array premises supply that connection for the concrete proofs; +compiler assertions challenge unit, Boolean, byte, u32, and representative array +widths. A successful construction does not assert that initialized padding +survives a typed move. The current resource-free scope adds no claim about +provenance, ownership, destruction, or external-state constructor permission. + +A checked semantic provider suffix extends generic native definitions that use +this boundary. It does not replace their extracted computation or Rust input +prefix. Both the native call audit and the independently written outcome family +retain that provider before choosing an outcome. The exact enclosing trait +bound, if Charon removes it from a default body's computational arguments, is +recovered as a specification premise from original trait/method ownership. +Required pointer-based validators are signature-only dictionary fields: their +whole Lean stubs return undef, and admission rejects every execution of them. +Their opaque Ptr carrier is an audited type constructor, not a value, spatial +model, or proof axiom about pointers. + ### Empty construction and external invariants Size zero does not imply that a value exists, that a Rust constructor may be diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 743f2fb2af..e4fdc3048b 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -505,8 +505,10 @@ The marker has no name or proposition: the Rust header identifies the trait, carrier, and generic bounds. Its proof must cover every original type and const parameter using only those bounds and their model providers. CI binds the marker to its compiler owner. The source census retains inactive and unused source -and checks reserved annotations in macro templates too. Conditional, computed, -inner, misplaced, and unsupported forms fail explicitly. The complete native +and checks reserved annotations in macro templates too. Conditional or computed +annotations, inner annotations, misplaced annotations, and unsupported forms +fail explicitly. Computed ordinary documentation may accompany a literal +annotation; the expanded census must still account for every reserved fence. The complete native HIR attribute census reconciles physical source origin, decoded doc text, fragment order, and multiplicity; direct markers also retain their declaration, signature, body, and source checks. Native evidence is recorded in @@ -524,8 +526,9 @@ the trait's promise. It cannot prove that a future downstream impl keeps that promise. Each selected local impl has a separate ordinary theorem discharging the promise, and Rust's unsafe-trait contract remains the obligation of external implementers. CI also inspects every extracted -implementation method body in the original and final ASTs, even when only the -law refers to the method. +admitted implementation method body in the original and final ASTs, even when +only the law refers to the method. Excluded provided methods cannot execute; +interface-only validators retain their required signatures but cannot be called. This initial bridge accepts traits with only their `Self` parameter and simple generic bounds. It compares compiler-resolved original and final type @@ -784,6 +787,49 @@ pointer provenance, destruction, or general Rust UB-freedom. is outside these laws. See [LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the remaining lowering boundaries. +## `FromBytes`, `FromZeros`, and owned zero construction + +The `FromBytes` law requires every fully initialized byte sequence of the +physical decoder's exact width to produce both a language-valid raw value and +a mathematical value. The `FromZeros` law requires the same two stages for the +all-zero sequence. Both stages use one `RustModel` provider; a physical success +cannot bypass an optional library invariant. A missing physical decoder fails +both laws. These definitions permit padding: neither law promises that a typed +copy preserves the initialized padding bytes used for construction. + +Nine `invariant_proof` markers cover `()` and `u8`/`u32` for both traits, +`bool` for `FromZeros`, and the two generic array impls. Array proofs compose +the actual element decoder and its law, including empty arrays and zero-sized +elements. The completeness lemma also derives the zero law from a `FromBytes` +law. Negative Lean examples distinguish Boolean zero validity from Boolean +validity for every byte, and reject zero construction of nonzero integers or a +value rejected by its library decoder. + +Aeneas normally has no model dictionary in the computation. The downstream +`native_models` elaborator retains a provider only in generic definitions +whose bodies need this boundary. Original Rust arguments remain in their exact +order, followed by implicit semantic providers; anonymous lets retain unused +arguments without changing the body. Contracts reuse those same providers. +They cannot quantify a different decoder after choosing an execution outcome. +The native-input audit distinguishes this checked suffix from source arguments. + +Charon can erase the unused enclosing Self dictionary from a default body. +Source and compiler evidence identify its trait and method slot before that +erasure; the specification receives that exact trait dictionary and law as +premises. These are specification parameters, not replacements for Rust +arguments. Separately, required `TryFromBytes::is_safe` fields retain their +native signatures but have no execution model. Carrying those dictionaries is +allowed; calling an unmodeled validator is rejected at admission. Its opaque +`Ptr` carrier supplies no construction, layout, provenance, or validity facts. + +As with `IntoBytes`, applying these proofs to Rust assumes the physical decoder +has the correct Rust width and language meaning. The primitive and array +interpretations have explicit Reference premises; compiler assertions challenge +the concrete widths. A generic provider is a supplied interpretation, not a +proof of an arbitrary downstream type's representation. These construction laws +cover the selected impls; they do not certify pointer access, external-state +invariants, destructors, or every `FromBytes`/`FromZeros` impl. + ## Native Lean proofs and independent checks `Specs.lean` is generated from the Rust comments in a fixed context containing diff --git a/verification/aeneas/admission.py b/verification/aeneas/admission.py index 8189e05d4a..3f2ca10517 100644 --- a/verification/aeneas/admission.py +++ b/verification/aeneas/admission.py @@ -37,9 +37,58 @@ # resolved reference to an excluded provided method; exclusion never supplies # an opaque implementation or a theorem about its behavior. Required trait # methods, bounds, associated constraints, and original method slots remain. -EXCLUDED_PROVIDED_METHODS = tuple('zerocopy::IntoBytes::' + name for name in ( - 'as_bytes', 'as_mut_bytes', 'write_to', 'write_to_prefix', 'write_to_suffix', - 'as_bytes_mut')) +EXCLUDED_PROVIDED_METHODS = ( + 'zerocopy::IntoBytes::as_bytes', + 'zerocopy::IntoBytes::as_mut_bytes', + 'zerocopy::IntoBytes::write_to', + 'zerocopy::IntoBytes::write_to_prefix', + 'zerocopy::IntoBytes::write_to_suffix', + 'zerocopy::IntoBytes::as_bytes_mut', + 'zerocopy::TryFromBytes::try_ref_from_bytes', + 'zerocopy::TryFromBytes::try_ref_from_prefix', + 'zerocopy::TryFromBytes::try_ref_from_suffix', + 'zerocopy::TryFromBytes::try_mut_from_bytes', + 'zerocopy::TryFromBytes::try_mut_from_prefix', + 'zerocopy::TryFromBytes::try_mut_from_suffix', + 'zerocopy::TryFromBytes::try_ref_from_bytes_with_elems', + 'zerocopy::TryFromBytes::try_ref_from_prefix_with_elems', + 'zerocopy::TryFromBytes::try_ref_from_suffix_with_elems', + 'zerocopy::TryFromBytes::try_mut_from_bytes_with_elems', + 'zerocopy::TryFromBytes::try_mut_from_prefix_with_elems', + 'zerocopy::TryFromBytes::try_mut_from_suffix_with_elems', + 'zerocopy::TryFromBytes::try_read_from_bytes', + 'zerocopy::TryFromBytes::try_read_from_prefix', + 'zerocopy::TryFromBytes::try_read_from_suffix', + 'zerocopy::FromBytes::ref_from_bytes', + 'zerocopy::FromBytes::ref_from_prefix', + 'zerocopy::FromBytes::ref_from_suffix', + 'zerocopy::FromBytes::mut_from_bytes', + 'zerocopy::FromBytes::mut_from_prefix', + 'zerocopy::FromBytes::mut_from_suffix', + 'zerocopy::FromBytes::ref_from_bytes_with_elems', + 'zerocopy::FromBytes::ref_from_prefix_with_elems', + 'zerocopy::FromBytes::ref_from_suffix_with_elems', + 'zerocopy::FromBytes::mut_from_bytes_with_elems', + 'zerocopy::FromBytes::mut_from_prefix_with_elems', + 'zerocopy::FromBytes::mut_from_suffix_with_elems', + 'zerocopy::FromBytes::read_from_bytes', + 'zerocopy::FromBytes::read_from_prefix', + 'zerocopy::FromBytes::read_from_suffix', + 'zerocopy::FromBytes::ref_from', + 'zerocopy::FromBytes::mut_from', + 'zerocopy::FromBytes::slice_from_prefix', + 'zerocopy::FromBytes::slice_from_suffix', + 'zerocopy::FromBytes::mut_slice_from_prefix', + 'zerocopy::FromBytes::mut_slice_from_suffix', + 'zerocopy::FromBytes::read_from', + 'zerocopy::FromZeros::zero', +) + +# These required validators remain dictionary fields with their original +# signatures. Their pointer-based bodies are outside this proof fragment. +# 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',) def digest(path): @@ -123,7 +172,8 @@ def __init__(self, data, registry, law_traits=()): self.before = stages == {'Unstructured'} # Opaque selection comes only from the registry, never from arbitrary # command-line flags which could hide an unsafe local body. - expected = sorted(row['rust'] for row in registry if row.get('opaque')) + expected = sorted([row['rust'] for row in registry if row.get('opaque')] + + [INTERFACE_ONLY_VALIDATORS, *INTERFACE_ONLY_TYPES]) if sorted(options['opaque']) != expected: raise ValueError('Opaque selections disagree with the external interpretation registry') @@ -254,6 +304,8 @@ def visit(self, index): raise ValueError(f'Missing executable dependency {index}') meta = function['item_meta'] name = self.name(meta['name']) + if self.interface_validator(function): + raise ValueError('Execution of a signature-only TryFromBytes validator is unsupported') prototype = self.prototype(function) if meta['has_errors'] or meta['is_extern']: raise ValueError(f'Untranslated or foreign-ABI dependency {name}') @@ -294,6 +346,10 @@ def visit(self, index): or meta['is_local'] or function['body'] != { 'Intrinsic': {'name': 'transmute', 'arg_names': ['src']}}): raise ValueError('Standard transmute reviewed boundary extension changed') + if name == 'core::mem::zeroed' and ( + matches[0].get('interpretation_extension') != 'retained-model-provider-v1' + or meta['is_local']): + raise ValueError('Zeroed construction changed its reviewed model-provider boundary') # 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', @@ -480,7 +536,9 @@ def dictionary(self, reference): self.audit_implementation(impl, trait) for method in impl['methods']: if method is not None: - self.visit(method['skip_binder']['id']) + function = self.functions[method['skip_binder']['id']] + if not self.interface_validator(function): + self.visit(method['skip_binder']['id']) elif tag in {'BuiltinOrAuto', 'Clause'}: trait = self.crate['trait_decls'][reference['trait_decl_ref']['skip_binder']['id']] if trait['methods'] or self.name(trait['item_meta']['name']) in self.law_traits: @@ -560,6 +618,9 @@ def trait_call(self, dispatch, generics, arguments): if not isinstance(method_id, int) or not 0 <= method_id < len(methods) or methods[method_id] is None: raise ValueError('Trait dispatch does not identify a declared method') method = methods[method_id] + if (self.name(trait['item_meta']['name']) == 'zerocopy::TryFromBytes' + and method['skip_binder']['name'] == 'is_safe'): + raise ValueError('Execution of a signature-only TryFromBytes validator is unsupported') if method.get('kind') != {'TraitMethod': [trait['def_id'], method_id]}: raise ValueError('Trait method has the wrong compiler declaration owner') if any(method['params'].get(k) for k in ('types', 'regions', 'const_generics', 'trait_clauses')): @@ -586,13 +647,76 @@ def audit_implementation(self, implementation, trait): raise ValueError('Annotated trait implementation is missing a method body') entry = methods[index] function = self.functions.get(entry['skip_binder']['id']) - source = function.get('src', {}).get('TraitImpl') if function else None - if (entry.get('kind') != {'TraitMethod': [trait['def_id'], index]} - or source is None or source['impl_ref']['id'] != implementation['def_id'] - or source['trait_ref']['id'] != trait['def_id'] or source['item_id'] != index): + source = function.get('src') if function else None + default = source.get('TraitDefault') if isinstance(source, dict) else None + source = source.get('TraitImpl') if isinstance(source, dict) else None + if entry.get('kind') != {'TraitMethod': [trait['def_id'], index]}: raise ValueError('Trait implementation method has the wrong compiler owner') + if source is not None: + if (source['impl_ref']['id'] != implementation['def_id'] + or source['trait_ref']['id'] != trait['def_id'] or source['item_id'] != index): + raise ValueError('Trait implementation method has the wrong compiler owner') + elif default is not None: + declared = method['skip_binder'].get('default') + if (default['trait_ref']['id'] != trait['def_id'] or default['item_id'] != index + or declared is None or declared['id'] != function['def_id'] + or any(method['params'].get(k) for k in + ('regions', 'types', 'const_generics', 'trait_clauses'))): + raise ValueError('Inherited method does not use its declared default body') + import trait_invariants as traits + arguments = entry['skip_binder']['generics'] + actual = [traits.simple_type(t, self.crate, 1) for t in arguments['types']] + expected = [traits.simple_type(t, self.crate) for t in implementation['impl_trait']['generics']['types']] + if actual != expected or arguments['regions'] or arguments['const_generics']: + raise ValueError('Inherited method changed its implementation type arguments') + references = arguments['trait_refs'] + if self.before: + reference = untag(references[0]) if len(references) == 1 else {} + selected = reference.get('kind', {}).get('TraitImpl', {}) + if (selected.get('id') != implementation['def_id'] + or reference.get('trait_decl_ref', {}).get('skip_binder', {}).get('id') != trait['def_id']): + raise ValueError('Inherited method lost its original Self dictionary') + try: + application = traits.default_trait_application( + reference['trait_decl_ref'], self.crate, 2) + supplied = selected['generics'] + fields(supplied, 'regions types const_generics trait_refs') + parameters = implementation['generics'] + if (application != {'id': trait['def_id'], 'arguments': expected} + or supplied['regions'] + or [traits.simple_type(t, self.crate, 1) for t in supplied['types']] + != [['parameter', i] for i in range(len(parameters['types']))] + or [traits.simple_const(c, 1) for c in supplied['const_generics']] + != [['const_parameter', p['index']] for p in + traits.usize_const_parameters(parameters)] + or len(supplied['trait_refs']) != len(parameters['trait_clauses'])): + raise ValueError('Changed Self application') + for supplied_ref, clause in zip(supplied['trait_refs'], parameters['trait_clauses']): + supplied_ref = untag(supplied_ref) + if (supplied_ref['kind'] != {'Clause': {'Bound': [1, clause['clause_id']]}} + or traits.default_trait_application(supplied_ref['trait_decl_ref'], self.crate, 2) + != traits.default_trait_application(clause['trait_'], self.crate, 1)): + raise ValueError('Changed Self argument dictionary') + except (KeyError, TypeError, ValueError) as error: + raise ValueError('Inherited method changed its original Self dictionary application') from error + elif references: + raise ValueError('Unsupported retained default-method Self dictionary') + else: + raise ValueError('Trait implementation method has no native implementation owner') self.visit(entry['skip_binder']['id']) + def interface_validator(self, function): + """Identify an unused required method without admitting its execution.""" + source = function.get('src') + source = source.get('TraitImpl') if isinstance(source, dict) else None + if source is None: + return False + trait = self.crate['trait_decls'][source['trait_ref']['id']] + index = source['item_id'] + return (self.name(trait['item_meta']['name']) == 'zerocopy::TryFromBytes' + and 0 <= index < len(trait['methods']) and trait['methods'][index] is not None + and trait['methods'][index]['skip_binder']['name'] == 'is_safe') + def rvalue(self, rvalue): tag, body = variant(rvalue) if tag == 'Use': @@ -737,6 +861,13 @@ def block(self, block, unwind=False): if actual != expected: raise ValueError(f'Unsupported NonZero::new_unchecked instantiation {actual}') call_evidence = {'caller': self.current, 'callee': name} + if name == 'core::mem::zeroed': + arguments = fn['generics'] + if (len(arguments['types']) != 1 or arguments['regions'] + or arguments['const_generics'] or arguments['trait_refs']): + raise ValueError('Zeroed construction changed its original type arguments') + call_evidence.update(type_arguments=[self.ty_name(arguments['types'][0])], + caller_def_id=self.current_function['def_id']) if name == 'core::intrinsics::transmute': actual = [self.ty_name(ty) for ty in fn['generics']['types']] providers = { @@ -962,6 +1093,7 @@ def guarded_calls(stage): 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.intrinsics.transmute': 'axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst', 'util.transmute_unchecked': @@ -997,7 +1129,8 @@ def main(): print('\n'.join(EXCLUDED_PROVIDED_METHODS)) else: registry = json.loads((args.root / 'verification/aeneas/external.json').read_text()) - print('\n'.join(row['rust'] for row in registry if row.get('opaque'))) + print('\n'.join([row['rust'] for row in registry if row.get('opaque')] + + [INTERFACE_ONLY_VALIDATORS, *INTERFACE_ONLY_TYPES])) if __name__ == '__main__': diff --git a/verification/aeneas/external.json b/verification/aeneas/external.json index d3c0e0f1ce..e55775fc28 100644 --- a/verification/aeneas/external.json +++ b/verification/aeneas/external.json @@ -34,5 +34,6 @@ {"rust": "core::num::{usize}::MAX", "signature": {"unsafe": false, "inputs": [], "output": "usize", "types": 0, "consts": 0}, "lean": "Usize.MAX"}, {"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::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"} ] diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 7b27a3e9a1..bf8af4c75f 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -10,6 +10,7 @@ those terms. -/ -- [zerocopy]: function definitions module public import Aeneas +public import NativeModels public import Zerocopy.Types public import Zerocopy.FunsExternal @[expose] public section @@ -642,6 +643,13 @@ def byteorder.verification.set_u32_be value n byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 +/-- [zerocopy::FromZeros::new_zeroed]: + Source: 'src/lib.rs', lines 3823:4-3829:5 + Visibility: public -/ +@[trait_default] +native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do + core.mem.zeroed Self + /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::XorCodec}::decode]: Source: 'src/trait_checks.rs', lines 41:4-43:5 -/ def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.decode @@ -791,6 +799,112 @@ def trait_checks.check_array_into_bytes : Result Unit := do trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize (Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes)) +/-- [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 -/ +def + Tuple.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- [zerocopy::impls::_::{impl zerocopy::TryFromBytes for ()}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 153:8-153:62 + Visibility: public -/ +def + Tuple.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_::{impl zerocopy::TryFromBytes for ()}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Tuple.Insts.ZerocopyTryFromBytes : TryFromBytes Unit := { + only_derive_is_allowed_to_implement_this_trait := + Tuple.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + is_safe := fun {A : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment A) => Tuple.Insts.ZerocopyTryFromBytes.is_safe + pointerinvariantAlignmentInst +} + +/-- Trait implementation: [zerocopy::impls::_::{impl zerocopy::FromZeros for ()}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Tuple.Insts.ZerocopyFromZeros : FromZeros Unit := { + TryFromBytesInst := Tuple.Insts.ZerocopyTryFromBytes + only_derive_is_allowed_to_implement_this_trait := + Tuple.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + new_zeroed := FromZeros.new_zeroed.default Unit +} + +/-- [zerocopy::impls::_::{impl zerocopy::FromBytes for ()}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + Tuple.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_::{impl zerocopy::FromBytes for ()}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Tuple.Insts.ZerocopyFromBytes : FromBytes Unit := { + FromZerosInst := Tuple.Insts.ZerocopyFromZeros + only_derive_is_allowed_to_implement_this_trait := + Tuple.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::FromZeros for u8}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U8.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u8}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 153:8-153:62 + Visibility: public -/ +def + U8.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u8}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U8.Insts.ZerocopyTryFromBytes : TryFromBytes Std.U8 := { + only_derive_is_allowed_to_implement_this_trait := + U8.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + is_safe := fun {A : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment A) => U8.Insts.ZerocopyTryFromBytes.is_safe + pointerinvariantAlignmentInst +} + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::FromZeros for u8}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U8.Insts.ZerocopyFromZeros : FromZeros Std.U8 := { + TryFromBytesInst := U8.Insts.ZerocopyTryFromBytes + only_derive_is_allowed_to_implement_this_trait := + U8.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + new_zeroed := FromZeros.new_zeroed.default Std.U8 +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::FromBytes for u8}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U8.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::FromBytes for u8}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U8.Insts.ZerocopyFromBytes : FromBytes Std.U8 := { + FromZerosInst := U8.Insts.ZerocopyFromZeros + only_derive_is_allowed_to_implement_this_trait := + U8.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait +} + /-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for i8}::only_derive_is_allowed_to_implement_this_trait]: Source: 'src/util/macros.rs', lines 165:8-165:62 Visibility: public -/ @@ -836,6 +950,58 @@ def I16.Insts.ZerocopyIntoBytes : IntoBytes Std.I16 := { I16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait } +/-- [zerocopy::impls::_#1::{impl zerocopy::FromZeros for u32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U32.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 153:8-153:62 + Visibility: public -/ +def + U32.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U32.Insts.ZerocopyTryFromBytes : TryFromBytes Std.U32 := { + only_derive_is_allowed_to_implement_this_trait := + U32.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + is_safe := fun {A : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment A) => U32.Insts.ZerocopyTryFromBytes.is_safe + pointerinvariantAlignmentInst +} + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::FromZeros for u32}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U32.Insts.ZerocopyFromZeros : FromZeros Std.U32 := { + TryFromBytesInst := U32.Insts.ZerocopyTryFromBytes + only_derive_is_allowed_to_implement_this_trait := + U32.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + new_zeroed := FromZeros.new_zeroed.default Std.U32 +} + +/-- [zerocopy::impls::_#1::{impl zerocopy::FromBytes for u32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U32.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::FromBytes for u32}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U32.Insts.ZerocopyFromBytes : FromBytes Std.U32 := { + FromZerosInst := U32.Insts.ZerocopyFromZeros + only_derive_is_allowed_to_implement_this_trait := + U32.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait +} + /-- [zerocopy::impls::_#1::{impl zerocopy::IntoBytes for u32}::only_derive_is_allowed_to_implement_this_trait]: Source: 'src/util/macros.rs', lines 165:8-165:62 Visibility: public -/ @@ -958,6 +1124,42 @@ def Isize.Insts.ZerocopyIntoBytes : IntoBytes Std.Isize := { Isize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait } +/-- [zerocopy::impls::_#2::{impl zerocopy::FromZeros for bool}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def Bool.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- [zerocopy::impls::_#3::{impl zerocopy::TryFromBytes for bool}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 140:8-140:62 + Visibility: public -/ +def + Bool.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#3::{impl zerocopy::TryFromBytes for bool}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def Bool.Insts.ZerocopyTryFromBytes : TryFromBytes Bool := { + only_derive_is_allowed_to_implement_this_trait := + Bool.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + is_safe := fun {A : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment A) => Bool.Insts.ZerocopyTryFromBytes.is_safe + pointerinvariantAlignmentInst +} + +/-- Trait implementation: [zerocopy::impls::_#2::{impl zerocopy::FromZeros for bool}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def Bool.Insts.ZerocopyFromZeros : FromZeros Bool := { + TryFromBytesInst := Bool.Insts.ZerocopyTryFromBytes + only_derive_is_allowed_to_implement_this_trait := + Bool.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + new_zeroed := FromZeros.new_zeroed.default Bool +} + /-- [zerocopy::impls::_#4::{impl zerocopy::IntoBytes for char}::only_derive_is_allowed_to_implement_this_trait]: Source: 'src/util/macros.rs', lines 165:8-165:62 Visibility: public -/ @@ -1639,6 +1841,69 @@ def core.marker.PhantomData.Insts.ZerocopyIntoBytes (T : Type) : IntoBytes T } +/-- [zerocopy::impls::_#23::{impl zerocopy::FromZeros for [T; N]}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + Array.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + {T : Type} (N : Std.Usize) (FromZerosInst : FromZeros T) : Result Unit := do + ok () + +/-- [zerocopy::impls::_#23::{impl zerocopy::TryFromBytes for [T; N]}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 140:8-140:62 + Visibility: public -/ +def + Array.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (N : Std.Usize) (TryFromBytesInst : TryFromBytes T) : + Result Unit + := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#23::{impl zerocopy::TryFromBytes for [T; N]}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def Array.Insts.ZerocopyTryFromBytes {T : Type} (N : Std.Usize) + (TryFromBytesInst : TryFromBytes T) : TryFromBytes (Array T N) := { + only_derive_is_allowed_to_implement_this_trait := + Array.Insts.ZerocopyTryFromBytes.only_derive_is_allowed_to_implement_this_trait + N TryFromBytesInst + is_safe := fun {A : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment A) => Array.Insts.ZerocopyTryFromBytes.is_safe + TryFromBytesInst pointerinvariantAlignmentInst +} + +/-- Trait implementation: [zerocopy::impls::_#23::{impl zerocopy::FromZeros for [T; N]}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +native_models def Array.Insts.ZerocopyFromZeros {T : Type} (N : Std.Usize) (FromZerosInst : + FromZeros T) : FromZeros (Array T N) := { + TryFromBytesInst := Array.Insts.ZerocopyTryFromBytes N + FromZerosInst.TryFromBytesInst + only_derive_is_allowed_to_implement_this_trait := + Array.Insts.ZerocopyFromZeros.only_derive_is_allowed_to_implement_this_trait + N FromZerosInst + new_zeroed := FromZeros.new_zeroed.default (Array T N) +} + +/-- [zerocopy::impls::_#23::{impl zerocopy::FromBytes for [T; N]}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + Array.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (N : Std.Usize) (FromBytesInst : FromBytes T) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#23::{impl zerocopy::FromBytes for [T; N]}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +native_models def Array.Insts.ZerocopyFromBytes {T : Type} (N : Std.Usize) (FromBytesInst : + FromBytes T) : FromBytes (Array T N) := { + FromZerosInst := Array.Insts.ZerocopyFromZeros N FromBytesInst.FromZerosInst + only_derive_is_allowed_to_implement_this_trait := + Array.Insts.ZerocopyFromBytes.only_derive_is_allowed_to_implement_this_trait + N FromBytesInst +} + /-- [zerocopy::wrappers::_::{impl zerocopy::IntoBytes for zerocopy::wrappers::Unalign}::only_derive_is_allowed_to_implement_this_trait]: Source: 'src/util/macros.rs', lines 165:8-165:62 Visibility: public -/ @@ -1823,25 +2088,25 @@ def util.min else ok a /-- [zerocopy::util::owned_transmute::to_bytes_native]: - Source: 'src/util/owned_transmute.rs', lines 29:0-33:1 -/ + Source: 'src/util/owned_transmute.rs', lines 30:0-34:1 -/ def util.owned_transmute.to_bytes_native (value : Std.U32) : Result (Array Std.U8 4#usize) := do core.intrinsics.transmute (Array Std.U8 4#usize) value /-- [zerocopy::util::owned_transmute::to_bytes]: - Source: 'src/util/owned_transmute.rs', lines 22:0-24:1 -/ + Source: 'src/util/owned_transmute.rs', lines 23:0-25:1 -/ def util.owned_transmute.to_bytes (value : Std.U32) : Result (Array Std.U8 4#usize) := do util.owned_transmute.to_bytes_native value /-- [zerocopy::util::owned_transmute::from_bytes]: - Source: 'src/util/owned_transmute.rs', lines 44:0-48:1 -/ + Source: 'src/util/owned_transmute.rs', lines 45:0-49:1 -/ def util.owned_transmute.from_bytes (bytes : Array Std.U8 4#usize) : Result Std.U32 := do core.intrinsics.transmute Std.U32 bytes /-- [zerocopy::util::owned_transmute::checked_bool]: - Source: 'src/util/owned_transmute.rs', lines 59:0-67:1 -/ + Source: 'src/util/owned_transmute.rs', lines 60:0-68:1 -/ def util.owned_transmute.checked_bool (byte : Std.U8) : Result (Option Bool) := do if byte < 2#u8 @@ -1850,7 +2115,7 @@ def util.owned_transmute.checked_bool else ok none /-- [zerocopy::util::owned_transmute::round_trip_checks]: - Source: 'src/util/owned_transmute.rs', lines 75:0-79:1 -/ + Source: 'src/util/owned_transmute.rs', lines 76:0-80:1 -/ def util.owned_transmute.round_trip_checks (value : Std.U32) : Result Unit := do let bytes ← util.owned_transmute.to_bytes value diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index 2a05df9bda..598b7d38a4 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -35,6 +35,12 @@ open Zerocopy @[rust_fun "core::intrinsics::transmute"] axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst +/-- [core::mem::zeroed]: + Source: '/rustc/library/core/src/mem/mod.rs', lines 755:0-755:36 + Name pattern: [core::mem::zeroed] + Visibility: public -/ +@[rust_fun "core::mem::zeroed"] axiom core.mem.zeroed (T : Type) : Result T + /-- [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] @@ -57,6 +63,62 @@ axiom core.num.nonzero.NonZero.get core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) : core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T +/-- [zerocopy::impls::_::{impl zerocopy::TryFromBytes for ()}::is_safe]: + Source: 'src/util/macros.rs', lines 155:8-160:9 + Visibility: public -/ +axiom Tuple.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment Alignment) : + pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly Unit) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result + Bool + +/-- [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u8}::is_safe]: + Source: 'src/util/macros.rs', lines 155:8-160:9 + Visibility: public -/ +axiom U8.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment Alignment) : + pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly Std.U8) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result + Bool + +/-- [zerocopy::impls::_#1::{impl zerocopy::TryFromBytes for u32}::is_safe]: + Source: 'src/util/macros.rs', lines 155:8-160:9 + Visibility: public -/ +axiom U32.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment Alignment) : + pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly Std.U32) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result + Bool + +/-- [zerocopy::impls::_#3::{impl zerocopy::TryFromBytes for bool}::is_safe]: + Source: 'src/util/macros.rs', lines 143:8-148:9 + Visibility: public -/ +axiom Bool.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment Alignment) : + pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly Bool) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result + Bool + +/-- [zerocopy::impls::_#23::{impl zerocopy::TryFromBytes for [T; N]}::is_safe]: + Source: 'src/util/macros.rs', lines 143:8-148:9 + Visibility: public -/ +axiom Array.Insts.ZerocopyTryFromBytes.is_safe + {T : Type} {Alignment : Type} {N : Std.Usize} (TryFromBytesInst : + TryFromBytes T) (pointerinvariantAlignmentInst : pointer.invariant.Alignment + Alignment) : + pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly (Array T N)) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result + Bool + /-- [zerocopy::util::copy_unchecked]: Source: 'src/util/mod.rs', lines 313:0-328:1 -/ axiom util.copy_unchecked diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index d91799ec1f..d54dc0e86d 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -177,8 +177,91 @@ structure byteorder.F64 (O : Type) where _0 : Array Std.U8 8#usize _1 : core.marker.PhantomData O +/-- [zerocopy::wrappers::read_only_def::ReadOnly] + Source: 'src/wrappers.rs', lines 630:4-634:5 + Visibility: public -/ +structure wrappers.read_only_def.ReadOnly (T : Type) where + inner : T + +/-- [zerocopy::pointer::invariant::Initialized] + Source: 'src/pointer/invariant.rs', lines 227:0-227:23 + Visibility: public -/ +inductive pointer.invariant.Initialized where + +/-- [zerocopy::pointer::invariant::Shared] + Source: 'src/pointer/invariant.rs', lines 133:0-133:18 + Visibility: public -/ +inductive pointer.invariant.Shared where + +/-- Trait declaration: [zerocopy::pointer::invariant::sealed::Sealed] + Source: 'src/pointer/invariant.rs', lines 296:4-296:23 + Visibility: public -/ +structure pointer.invariant.sealed.Sealed (Self : Type) where + +/-- Trait declaration: [zerocopy::pointer::invariant::Aliasing] + Source: 'src/pointer/invariant.rs', lines 37:0-41:1 + Visibility: public -/ +structure pointer.invariant.Aliasing (Self : Type) where + IS_EXCLUSIVE : Result Bool + sealedSealedInst : pointer.invariant.sealed.Sealed Self + +/-- Trait declaration: [zerocopy::pointer::invariant::Read] + Source: 'src/pointer/invariant.rs', lines 277:0-277:33 + Visibility: public -/ +structure pointer.invariant.Read (Self : Type) (A : Type) (R : Type) where + AliasingInst : pointer.invariant.Aliasing A + +/-- [zerocopy::pointer::invariant::Safe] + Source: 'src/pointer/invariant.rs', lines 238:0-238:16 + Visibility: public -/ +inductive pointer.invariant.Safe where + +/-- Trait declaration: [zerocopy::pointer::invariant::Reference] + Source: 'src/pointer/invariant.rs', lines 121:0-121:41 + Visibility: public -/ +structure pointer.invariant.Reference (Self : Type) where + AliasingInst : pointer.invariant.Aliasing Self + sealedSealedInst : pointer.invariant.sealed.Sealed Self + +/-- Trait declaration: [zerocopy::pointer::invariant::Alignment] + Source: 'src/pointer/invariant.rs', lines 44:0-56:1 + Visibility: public -/ +structure pointer.invariant.Alignment (Self : Type) where + sealedSealedInst : pointer.invariant.sealed.Sealed Self + read : forall {T : Type} {A : Type} {R : Type} (coremarkerCopyInst : + core.marker.Copy T) (ReadInst : pointer.invariant.Read T A R) + (ReferenceInst : pointer.invariant.Reference A), pointer.ptr.def.Ptr T (A + × Self × pointer.invariant.Safe) A Self pointer.invariant.Safe → Result + T + +/-- Trait declaration: [zerocopy::TryFromBytes] + Source: 'src/lib.rs', lines 1901:0-3451:1 + Visibility: public -/ +structure TryFromBytes (Self : Type) where + only_derive_is_allowed_to_implement_this_trait : Result Unit + is_safe : forall {A : Type} (pointerinvariantAlignmentInst : + pointer.invariant.Alignment A), pointer.ptr.def.Ptr + (wrappers.read_only_def.ReadOnly Self) (pointer.invariant.Shared × A × + pointer.invariant.Initialized) pointer.invariant.Shared A + pointer.invariant.Initialized → Result Bool + +/-- Trait declaration: [zerocopy::FromZeros] + Source: 'src/lib.rs', lines 3708:0-4070:1 + Visibility: public -/ +structure FromZeros (Self : Type) where + TryFromBytesInst : TryFromBytes Self + only_derive_is_allowed_to_implement_this_trait : Result Unit + new_zeroed : Result Self + +/-- Trait declaration: [zerocopy::FromBytes] + Source: 'src/lib.rs', lines 4298:0-5710:1 + Visibility: public -/ +structure FromBytes (Self : Type) where + FromZerosInst : FromZeros Self + only_derive_is_allowed_to_implement_this_trait : Result Unit + /-- Trait declaration: [zerocopy::IntoBytes] - Source: 'src/lib.rs', lines 5941:0-6446:1 + Source: 'src/lib.rs', lines 5949:0-6454:1 Visibility: public -/ structure IntoBytes (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit @@ -204,10 +287,4 @@ structure trait_checks.Forward (C : Type) where structure wrappers.Unalign (T : Type) where _0 : T -/-- [zerocopy::wrappers::read_only_def::ReadOnly] - Source: 'src/wrappers.rs', lines 630:4-634:5 - Visibility: public -/ -structure wrappers.read_only_def.ReadOnly (T : Type) where - inner : T - end Zerocopy diff --git a/verification/aeneas/golden/TypesExternal_Template.lean b/verification/aeneas/golden/TypesExternal_Template.lean index da94ce8f16..9273738dc5 100644 --- a/verification/aeneas/golden/TypesExternal_Template.lean +++ b/verification/aeneas/golden/TypesExternal_Template.lean @@ -138,3 +138,9 @@ axiom core.num.niche_types.NonZeroIsizeInner : Type @[rust_type "core::num::nonzero::NonZero"] axiom core.num.nonzero.NonZero (T : Type) (Clause0_NonZeroInner : Type) : Type +/-- [zerocopy::pointer::ptr::def::Ptr] + Source: 'src/pointer/ptr.rs', lines 57:4-73:5 + Visibility: public -/ +axiom pointer.ptr.def.Ptr (T : Type) (I : Type) (Clause0_Aliasing : Type) + (Clause0_Alignment : Type) (Clause0_Validity : Type) : Type + diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py index 06776f48bd..ba6b2cef7c 100644 --- a/verification/aeneas/inline.py +++ b/verification/aeneas/inline.py @@ -363,9 +363,10 @@ def char_offset(byte): if (owner.get('include_str_docs') and (not owner.get('macro_input') or any(suspicious(doc['text']) for doc in docs))): raise ValueError('Direct include_str! in owner doc expressions is unsupported; use literal outer docs') - if (owner.get('kind') != 'trait' and owner.get('computed_docs') - and any(suspicious(doc['text']) for doc in docs)): - raise ValueError('Computed doc strings on function or nominal type owners are unsupported; use literal outer docs') + # Ordinary computed documentation may accompany literal annotations + # (for example new_zeroed's generated assembly documentation). It is + # never an annotation source. The mandatory expanded-origin census + # later rejects any additional fence produced by such an expression. content, lines, fragments = [], [], [] for doc in docs: owned.add((doc['start'], doc['end'])) @@ -459,6 +460,7 @@ def char_offset(byte): found.append({'syntax': owner['path'], 'kind': kind, 'theorem': name, 'copy_span': copy_span, 'method': bool(owner.get('method')), + 'default_trait': owner.get('default_trait'), 'declaration_begin': owner.get('declaration_start', owner['start']), 'declaration_end': owner['close'], 'doc_fragments': [{'begin': d.get('origin_start', d['start']), @@ -789,7 +791,7 @@ def generated_bindings(source, annotations, types_source=None): # Pinned Aeneas marks a wrapper consisting only of a loop call as # reducible. Accept that exact attribute; arbitrary declaration prefixes # must not conceal a different owner or declaration kind. - header = re.match(r'(?:@\[reducible\]\n)?def (' + IDENTIFIER + + header = re.match(r'(?:@\[(?:reducible|trait_default)\]\n)?(?:native_models )?def (' + IDENTIFIER + r'(?:\.' + IDENTIFIER + r')*)\b', declaration) if not header: raise ValueError(f'Unsupported generated root declaration for {rust}') @@ -1001,6 +1003,7 @@ def save_bindings(root, annotations, work, development=False): bindings[rust]['dictionary_count'] = len(getattr(annotations, 'function_dictionaries', {}).get(rust, [])) bindings[rust]['dictionary_names'] = a.get('dictionary_names', []) bindings[rust]['trait_clauses'] = getattr(annotations, 'function_dictionaries', {}).get(rust, []) + bindings[rust]['erased_self_bound'] = a.get('erased_self_bound') trait_laws, trait_impl_laws, trait_dictionaries = [], [], [] if (any(a.get('kind') == 'trait' for a in annotations.values()) or getattr(annotations, 'trait_proofs', []) @@ -1187,6 +1190,13 @@ def assemble(root, annotations, work, development=False): if not re.fullmatch(IDENTIFIER + r'(?:\.' + IDENTIFIER + ')*', model): raise ValueError('Invalid verified generated model name') lines = a['spec_text'].rstrip('\n').split('\n') + erased = bindings[a['rust']].get('erased_self_bound') + if erased: + matches = [row for row in manifest['trait_dictionaries'] if row['def_id'] == erased['trait_def_id']] + if len(matches) != 1: + raise ValueError('Erased default-method bound lacks its native trait dictionary') + specs.append(f'default_trait_body {model} for {matches[0]["raw"]} ' + f'with {len(erased["arguments"])} type parameters') clause = a['clause_line'] application = f'@{model} with {len(a["generics"])} type parameters' dictionary_count = bindings[a['rust']].get('dictionary_count', 0) @@ -1308,6 +1318,19 @@ def check_bindings(root, annotations, llbc): annotations.external_type_parameters = None source_digest(root, annotations) translated = json.loads(llbc.read_text())['translated'] + # Charon also serializes declarations needed only for pretty printing. + # Its ordered groups identify the actual translation dependency closure. + # Do not request models for an enum merely mentioned in that extra data. + ordered_types = set() + for group in translated.get('ordered_decls', []): + if 'Type' in group: + kind, values = next(iter(group['Type'].items())) + if kind == 'NonRec': + ordered_types.add(values) + elif kind == 'Rec': + ordered_types.update(values) + else: + raise ValueError('Unsupported native type declaration group') if [root for root in translated.get('options', {}).get('start_from', []) if root.startswith(('@span:', '@doc-origin:'))] != [ impl_root(marker) for marker in annotations.trait_proofs]: @@ -1642,6 +1665,8 @@ def position(point): for declaration in translated.get('type_decls', []): if not declaration or declaration['item_meta'].get('is_local') is not True: continue + if 'ordered_decls' in translated and declaration['def_id'] not in ordered_types: + continue meta = declaration['item_meta'] kind = declaration.get('kind') if not isinstance(kind, dict) or not (set(kind) <= {'Struct', 'Enum'}): @@ -1677,6 +1702,8 @@ def position(point): continue meta = declaration.get('item_meta', {}) if category is None: + if 'ordered_decls' in translated and declaration['def_id'] not in ordered_types: + continue kind = declaration.get('kind') if not isinstance(kind, dict) or set(kind) not in ({'Struct'}, {'Enum'}): continue diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean index 29ef24344a..eacf3aa11e 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -7,6 +7,7 @@ This file may not be copied, modified, or distributed except according to those terms. -/ import Required +import ZeroedAudit open Lean Elab Command /-! @@ -216,6 +217,10 @@ run_elab do | throwError "Missing pinned opaque carrier {carrier}" unless info.levelParams.isEmpty && (← Meta.isDefEq info.type expectedCarrier) do throwError "Opaque carrier {carrier} changed its type-only signature" + -- The interface audit below independently checks Ptr's exact data signature + -- and all uncallable validator stubs before this axiom list is used. + let opaqueCarriers := if env.contains `Zerocopy.pointer.ptr.def.Ptr then + opaqueCarriers.push `Zerocopy.pointer.ptr.def.Ptr else opaqueCarriers -- ABI inputs are functions returning data, with no proposition asserting -- alignment, size, or correctness. A changed type could smuggle a theorem -- into the allowed axiom list, so check their exact compiled signatures. @@ -428,6 +433,7 @@ run_elab do unless roots.size == rootNames.size && rootNames.all roots.contains do throwError "Execution admission roots disagree with the function binding table" auditStdTransmute bindings + auditZeroed bindings let some typesModule := env.getModuleIdx? `Zerocopy.Types | throwError "Raw extracted types must be imported" let some shapesModule := env.getModuleIdx? `ModelShapes @@ -437,6 +443,7 @@ run_elab do let mut expectedTypes : Array Name := #[] let mut expectedLocalRust : Array String := #[] let mut expectedModels : Array Name := #[] + let mut expectedDefaults : Array Name := #[] for (rustName, entry) in entries.toArray do let .ok kind := entry.getObjValAs? String "kind" | throwError "Binding for {rustName} must name its owner kind" @@ -457,6 +464,38 @@ run_elab do let .ok sourceInputs := entry.getObjValAs? (Array String) "inputs" | throwError "Function binding for {rustName} must name its original value inputs" let specName := (`Zerocopy.Specs).str sourceSpec + -- A provided method may lose its unused Self dictionary during lowering. + -- The source/compiler binder records that exact bound; the compiled + -- registry must add precisely that trait as a specification premise. + let .ok erased := entry.getObjVal? "erased_self_bound" + | throwError "Function binding must record its enclosing-bound disposition" + let registeredDefault ← AeneasSpecs.defaultTraitBody? rawName + if erased == Json.null then + unless registeredDefault.isNone do + throwError "Unexpected enclosing trait premise on {rawName}" + else + let .ok traitRust := erased.getObjValAs? String "rust" + | throwError "Erased Self bound must name its original Rust trait" + let .ok traitId := erased.getObjValAs? Nat "trait_def_id" + | throwError "Erased Self bound must retain its compiler trait identity" + let .ok arguments := erased.getObjValAs? (Array Json) "arguments" + | throwError "Erased Self bound must retain its original type arguments" + unless arguments == (Array.range generics.size).map + (fun index => toJson #[toJson "parameter", toJson index]) do + throwError "Unsupported enclosing trait instantiation on {rawName}" + let .ok dictionaries := bindings.getObjValAs? (Array Json) "trait_dictionaries" + | throwError "Missing native trait dictionary inventory" + let owners := dictionaries.filter fun row => + row.getObjValAs? String "rust" == .ok traitRust && + row.getObjValAs? Nat "def_id" == .ok traitId + unless owners.size == 1 do throwError "Erased Self bound lost its exact native owner" + let .ok traitRaw := owners[0]!.getObjValAs? String "raw" + | throwError "Missing enclosing trait's compiled dictionary" + let some owner := registeredDefault + | throwError "Missing compiled enclosing trait premise for {rawName}" + unless owner.trait == traitRaw.toName && owner.parameterCount == arguments.size do + throwError "Compiled enclosing trait premise changed its Rust owner on {rawName}" + expectedDefaults := expectedDefaults.push rawName unless env.getModuleIdxFor? specName == some specsModule do throwError "Function binding for {rustName} does not name a compiled inline specification" let (boundModel, boundInputs) ← AeneasSpecs.specBinding specName @@ -464,8 +503,11 @@ run_elab do -- specBinding already checked each argument's original variable identity. let .ok dictionaryCount := entry.getObjValAs? Nat "dictionary_count" | throwError "Function binding for {rustName} must count its original trait dictionaries" + let semanticCount ← Meta.forallTelescope (← getConstInfo rawName).type fun native _ => do + let (_, models) ← AeneasSpecs.splitNativeModels native + pure models.size unless boundModel == rawName && - boundInputs == generics.size + dictionaryCount + sourceInputs.size do + boundInputs == generics.size + dictionaryCount + sourceInputs.size + semanticCount do throwError "Compiled specification {specName} changed its source model or original input prefix" else if kind == "type" then if expectedTypes.contains rawName then @@ -505,6 +547,10 @@ run_elab do throwError "Unannotated model must use its nominal Fields carrier: {rawName}" else throwError "Unsupported binding kind {kind} for {rustName}" + let defaults ← AeneasSpecs.defaultTraitBodies + unless defaults.size == expectedDefaults.size && + defaults.all (fun owner => expectedDefaults.contains owner.function) do + throwError "Compiled enclosing trait premises disagree with source bindings" -- This image is classified from LLBC type and trait declarations in live -- mode. Every compiled raw inductive must belong to exactly one class; -- local nominals must also have the source-bound model/provider entry above. diff --git a/verification/aeneas/lean/DeriveModels.lean b/verification/aeneas/lean/DeriveModels.lean index 0e852ef2e4..8315482c12 100644 --- a/verification/aeneas/lean/DeriveModels.lean +++ b/verification/aeneas/lean/DeriveModels.lean @@ -9,6 +9,7 @@ those terms. -/ module public import ModelPrelude public import ModelCompletion +public import NativeModels public meta import Lean public import TraitDictionarySupport public section @@ -67,7 +68,7 @@ meta def modelBinding (raw : Name) : MetaM (Name × Name × Name × Name × Nat) return (b.fields, b.model, b.decoder, b.provider, b.generics) /-- One dictionary for every original Rust generic, including unused parameters. -/ -meta def withModelDictionaries (params : Array Expr) +meta def withBoundModelDictionaries (params retained : Array Expr) (k : Array Expr → TermElabM α) : TermElabM α := do let rec loop (i : Nat) (dicts : Array Expr) : TermElabM α := do if h : i < params.size then @@ -75,11 +76,20 @@ meta def withModelDictionaries (params : Array Expr) unless (← whnf (← inferType param)).isSort do throwError "Only Rust type parameters are supported in model generation" let classType ← mkAppM ``RustModel #[param] - withLocalDecl (Name.mkSimple s!"_rustModel{i}") .instImplicit classType fun dict => - loop (i + 1) (dicts.push dict) + let matching ← retained.filterM fun model => do isDefEq (← inferType model) classType + if matching.size > 1 then throwError "Repeated retained model provider" + if matching.size == 1 then + loop (i + 1) (dicts.push matching[0]!) + else + withLocalDecl (Name.mkSimple s!"_rustModel{i}") .instImplicit classType fun dict => + loop (i + 1) (dicts.push dict) else k dicts loop 0 #[] +meta def withModelDictionaries (params : Array Expr) + (k : Array Expr → TermElabM α) : TermElabM α := + withBoundModelDictionaries params #[] k + /-- These restrictions describe the supported extracted shape. Indexed types and recursive groups would require additional carrier and decoding semantics; accepting them through the simple constructor traversal would invent a model. -/ @@ -566,11 +576,12 @@ must fail even if a later clause would ignore the affected value. -/ elab "check_model_inputs " functionId:ident " with " count:num " type " "parameters" : command => Command.liftTermElabM do let function ← realizeGlobalConstNoOverloadWithInfo functionId - forallTelescope (← getConstInfo function).type fun inputs result => do + forallTelescope (← getConstInfo function).type fun allInputs result => do + let (inputs, retained) ← splitNativeModels allInputs unless count.getNat ≤ inputs.size do throwError "Invalid Rust generic prefix count" let traitCount ← traitDictionaryCount inputs count.getNat let params := inputs.extract 0 count.getNat - withModelDictionaries params fun dicts => do + withBoundModelDictionaries params retained fun dicts => do for input in inputs.extract (count.getNat + traitCount) inputs.size do let _ ← boundModelProvider (← inferType input) params dicts let result ← whnf result diff --git a/verification/aeneas/lean/NativeModels.lean b/verification/aeneas/lean/NativeModels.lean new file mode 100644 index 0000000000..3f9162b857 --- /dev/null +++ b/verification/aeneas/lean/NativeModels.lean @@ -0,0 +1,143 @@ +/- 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 RustModel +public meta import Lean +public section + +/-! +Native definitions retain their original arguments while section-variable +capture supplies only the model providers their elaborated bodies use. Every +original argument occurs in an anonymous let around the unchanged source body; +these lets preserve otherwise-unused arguments and reduce to that body. +The supported input is the native generator's named, typed binder groups and +nonrecursive `:=` declarations without auxiliary declarations. +-/ + +open Lean Meta Elab Command +namespace AeneasSpecs + +private meta def nativeModelRaw? (input : Expr) : MetaM (Option Expr) := do + let type ← whnf (← inferType input) + if type.getAppFn.isConstOf ``RustModel && type.getAppArgs.size == 1 then + return some type.getAppArgs[0]! + return none + +/-- Split the original Rust argument prefix from its canonical model suffix. +Models must be instance arguments for distinct original type variables, in +their original order. A container model or an independently equal type cannot +stand in for the exact original variable. +-/ +meta def splitNativeModels (inputs : Array Expr) : + MetaM (Array Expr × Array Expr) := do + for input in inputs do + unless input.isFVar do + throwError "Native model arguments require local telescope variables" + let mut firstModel := inputs.size + while firstModel > 0 do + if (← nativeModelRaw? inputs[firstModel - 1]!).isNone then break + firstModel := firstModel - 1 + let original := inputs.extract 0 firstModel + let models := inputs.extract firstModel inputs.size + for input in original do + if (← nativeModelRaw? input).isSome then + throwError "Native RustModel arguments must form a trailing suffix" + let mut previous : Option Nat := none + for model in models do + unless (← model.fvarId!.getDecl).binderInfo.isInstImplicit do + throwError "Native RustModel suffix arguments must be instance implicit" + let some raw ← nativeModelRaw? model + | throwError "Missing native RustModel argument" + unless raw.isFVar do + throwError "Native models require an exact original type variable" + let mut position : Option Nat := none + for index in [:original.size] do + if original[index]! == raw then position := some index + let some index := position + | throwError "Native model type is not an original argument" + let .sort level ← whnf (← inferType raw) + | throwError "Native models require Type-valued original arguments" + if level.isZero then + throwError "Native models require Type-valued original arguments" + if previous.any (· >= index) then + throwError "Native model suffix must follow original type order without duplicates" + previous := some index + return (original, models) + +private meta def nativeBinderNames (binder : Syntax) : + CommandElabM (Array (TSyntax `ident) × Bool) := do + let (names, type) ← if binder.isOfKind ``Parser.Term.explicitBinder || + binder.isOfKind ``Parser.Term.implicitBinder then do + unless binder[2].getNumArgs == 2 && + (!binder.isOfKind ``Parser.Term.explicitBinder || binder[3].isNone) do + throwErrorAt binder "native_models requires typed binders without defaults" + pure (binder[1].getArgs, (⟨binder[2][1]⟩ : TSyntax `term)) + else if binder.isOfKind ``Parser.Term.instBinder then do + unless binder[1][0].isIdent do + throwErrorAt binder "native_models requires named instance arguments" + pure (#[binder[1][0]], (⟨binder[2]⟩ : TSyntax `term)) + else throwErrorAt binder + "native_models requires named, typed explicit, implicit, or instance binders" + let names ← names.mapM fun binderId => do + unless binderId.isIdent do + throwErrorAt binderId "native_models does not support anonymous arguments" + pure (⟨binderId⟩ : TSyntax `ident) + let isType := match type with + | `(Type) => true + | _ => false + return (names, isType) + +elab mods:declModifiers "native_models " "def " id:declId + sig:optDeclSig val:declVal : command => do + -- Native output has no declaration-local universe binder or equation/where + -- declarations. Reject them rather than relocating their binding scopes. + unless id.raw[1].getArgs.isEmpty do + throwErrorAt id "native_models does not support declaration-local universes" + let `(declVal| := $body) := val + | throwErrorAt val "native_models requires a plain := body" + let binders := sig.raw[0].getArgs + let mut names : Array (TSyntax `ident) := #[] + let mut types : Array (TSyntax `ident) := #[] + for binder in binders do + let (bound, isType) ← nativeBinderNames binder + for binderId in bound do + if names.any (·.getId == binderId.getId) then + throwErrorAt binderId "native_models requires distinct argument names" + names := names.push binderId + if isType then types := types.push binderId + Command.withScope (fun scope => scope) do + if !binders.isEmpty then + let binders := binders.map (fun binder => + (⟨binder⟩ : TSyntax ``Parser.Term.bracketedBinder)) + elabCommand (← `(command| variable $binders*)) + let mut occupied := names + for type in types do + let mut index := 0 + let mut provider := mkIdent <| Name.mkSimple s!"_nativeModel{index}" + while occupied.any (·.getId == provider.getId) do + index := index + 1 + provider := mkIdent <| Name.mkSimple s!"_nativeModel{index}" + occupied := occupied.push provider + elabCommand (← `(variable [$provider : AeneasSpecs.RustModel $type])) + let mut retained : TSyntax `term := ⟨body.raw⟩ + for binderId in names.reverse do + -- Explicit application also retains higher-rank arguments without + -- inserting their own implicit inputs or instance arguments. + let arg : TSyntax `term := + ⟨mkNode ``Parser.Term.explicit #[mkAtom "@", binderId.raw]⟩ + retained ← `(term| let _ := $arg; $retained) + let sig : TSyntax ``Parser.Command.optDeclSig := + ⟨sig.raw.setArg 0 (mkNullNode #[])⟩ + let val : TSyntax ``Parser.Command.declVal := + ⟨val.raw.setArg 1 retained.raw⟩ + let definition := mkNode ``Parser.Command.definition #[ + mkAtom "def", id.raw, sig.raw, val.raw, mkNullNode #[]] + elabCommand (mkNode ``Parser.Command.declaration #[mods.raw, definition]) + +end AeneasSpecs diff --git a/verification/aeneas/lean/NativeModelsTests.lean b/verification/aeneas/lean/NativeModelsTests.lean new file mode 100644 index 0000000000..a10039c058 --- /dev/null +++ b/verification/aeneas/lean/NativeModelsTests.lean @@ -0,0 +1,152 @@ +/- 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 NativeModels +@[expose] public section +open AeneasSpecs Aeneas.Std Aeneas.Std.Result Lean Meta Elab Command +set_option linter.unusedVariables false +set_option linter.unusedSectionVars false +set_option linter.overlappingInstances false + +namespace NativeModelsTests + +def modeledLeaf (T : Type) [RustModel T] : Result T := .fail .undef +structure ComputationalDict (T : Type) where run : T → Nat + +@[reducible] +native_models def independent (T : Type) {U : Type} (unused : Nat) + (dict : ComputationalDict T) : Nat := 7 +native_models def dependent (T : Type) {U : Type} (unused : Nat) + (dict : ComputationalDict T) : Result T := modeledLeaf T +native_models def interleaved (unused : Nat) (T U : Type) + (dict : ComputationalDict U) : Result U := modeledLeaf U +native_models def both (T U : Type) (unused : Nat) : Result (T × U) := do + let t ← modeledLeaf T + let u ← modeledLeaf U + ok (t, u) +native_models def higher {T : Type} (dict : {V : Type} → V → V) + (unused : Nat) : Nat := 8 +native_models def instanceArgument (T : Type) [inh : Inhabited T] + (unused : Nat) : T := default +native_models def typeReturn (T U : Type) (unused : Nat) : Type := T +native_models def untypedReturn (T : Type) (unused : Nat) := 3 +native_models def noArguments : Nat := 4 + +-- A dependent do-body used to elaborate under the beta wrapper's fresh type. +-- The anonymous lets must retain Self without changing the expected Result Self. +@[trait_default] +native_models def defaultDo (Self : Type) : Result Self := do + modeledLeaf Self +example (Self : Type) [m : RustModel Self] : + @defaultDo Self m = @modeledLeaf Self m := rfl +native_models def typedResult (T : Type) (x : T) : Option (ModelOf T) := + RustModel.decode x +native_models def containerResult (T : Type) (xs : List T) : Option (ModelOf (List T)) := + RustModel.decode xs +native_models def laterIndependent (T : Type) (unused : Nat) : Nat := 9 +native_models def preservesUndef (T : Type) (unused : Nat) : Result T := .fail .undef +native_models def providerCollision (T : Type) (_nativeModel0 : Nat) : Result T := modeledLeaf T + +example (T U : Type) (n : Nat) (dict : ComputationalDict T) : + @independent T U n dict = 7 := rfl +example (T U : Type) (n : Nat) (dict : ComputationalDict T) [m : RustModel T] : + @dependent T U n dict m = @modeledLeaf T m := rfl +example (T U : Type) (n : Nat) (dict : ComputationalDict U) [m : RustModel U] : + @interleaved n T U dict m = @modeledLeaf U m := rfl +example (T U : Type) (n : Nat) [mt : RustModel T] [mu : RustModel U] : + @both T U n mt mu = (do let t ← @modeledLeaf T mt; let u ← @modeledLeaf U mu; ok (t, u)) := rfl +example (T : Type) (dict : {V : Type} → V → V) (n : Nat) : + @higher T dict n = 8 := rfl +example (T : Type) [i : Inhabited T] (n : Nat) : + @instanceArgument T i n = i.default := rfl +example (T U : Type) (n : Nat) : typeReturn T U n = T := rfl +example (T : Type) (x : T) [m : RustModel T] : + @typedResult T x m = m.decode x := rfl +example (T : Type) (xs : List T) [m : RustModel T] : + @containerResult T xs m = (@modelList T m).decode xs := rfl +example (T : Type) (n : Nat) : @preservesUndef T n = .fail .undef := rfl +example (T : Type) (n : Nat) [m : RustModel T] : + @providerCollision T n m = @modeledLeaf T m := rfl + +run_meta do + for (decl, expectedNames, suffixCount) in #[ + (``independent, #[`T, `U, `unused, `dict], 0), + (``dependent, #[`T, `U, `unused, `dict], 1), + (``defaultDo, #[`Self], 1), + (``noArguments, #[], 0), + (``untypedReturn, #[`T, `unused], 0), + (``interleaved, #[`unused, `T, `U, `dict], 1), + (``both, #[`T, `U, `unused], 2), + (``higher, #[`T, `dict, `unused], 0), + (``instanceArgument, #[`T, `inh, `unused], 0), + (``typeReturn, #[`T, `U, `unused], 0), + (``preservesUndef, #[`T, `unused], 0), + (``typedResult, #[`T, `x], 1), + (``containerResult, #[`T, `xs], 1), + (``laterIndependent, #[`T, `unused], 0), + (``providerCollision, #[`T, `_nativeModel0], 1)] do + forallTelescope (← inferType (mkConst decl)) fun args _ => do + let (original, models) ← splitNativeModels args + unless original.size == expectedNames.size && models.size == suffixCount do + throwError "Wrong native model argument counts for {decl}" + for arg in original, expected in expectedNames do + unless (← arg.fvarId!.getDecl).userName == expected do + throwError "Wrong native argument order for {decl}" + + +-- Ordinary explicit headers keep these deliberately malformed suffixes intact. +def badMiddle (T : Type) [m : RustModel T] (n : Nat) : Nat := n +def badExplicit (T : Type) (m : RustModel T) : Nat := 0 +def badOrder (T U : Type) [mu : RustModel U] [mt : RustModel T] : Nat := 0 +def badDuplicate (T : Type) [m1 : RustModel T] [m2 : RustModel T] : Nat := 0 +def badContainer (T : Type) [m : RustModel (List T)] : Nat := 0 +def badConcrete [m : RustModel Nat] : Nat := 0 + +run_meta do + for decl in #[``badMiddle, ``badExplicit, ``badOrder, ``badDuplicate, + ``badContainer, ``badConcrete] do + forallTelescope (← inferType (mkConst decl)) fun args _ => do + let rejected ← try + let _ ← splitNativeModels args + pure false + catch _ => pure true + unless rejected do throwError "Expected malformed model suffix rejection: {decl}" + let rejected ← try + let _ ← splitNativeModels #[mkConst ``Nat] + pure false + catch _ => pure true + unless rejected do throwError "Expected non-variable rejection" + +/-- error: native_models requires typed binders without defaults -/ +#guard_msgs in +native_models def rejectsDefault (x : Nat := 2) : Nat := x + +/-- error: native_models does not support anonymous arguments -/ +#guard_msgs in +native_models def rejectsAnonymous (_ : Nat) : Nat := 0 + +/-- error: native_models does not support declaration-local universes -/ +#guard_msgs in +native_models def rejectsUniverse.{u} (T : Type u) : Type u := T + +/-- error: native_models requires a plain := body -/ +#guard_msgs in +native_models def rejectsEquations : Nat → Nat + | n => n + +/-- error: native_models requires distinct argument names -/ +#guard_msgs in +native_models def rejectsShadow (T : Type) (T : Type) : Type := T + +/-- error: native_models requires a plain := body -/ +#guard_msgs in +native_models def rejectsWhere (x : Nat) : Nat := aux x +where aux (x : Nat) := x + +end NativeModelsTests diff --git a/verification/aeneas/lean/Proofs/FromBytes.lean b/verification/aeneas/lean/Proofs/FromBytes.lean new file mode 100644 index 0000000000..5e104dd827 --- /dev/null +++ b/verification/aeneas/lean/Proofs/FromBytes.lean @@ -0,0 +1,74 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import TraitLaws +public import RustRepresentation +@[expose] public section + +/-! +Each law names an actual extracted implementation dictionary and retains its +canonical mathematical provider. Primitive laws use the shared representation +proofs. Arrays preserve the original type, length, and element dictionary, then +use that element's provider and trait laws. These are representation-admission +proofs; Rust layout correspondence and method-body correctness are separate +obligations. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +@[instance] theorem Tuple.Insts.ZerocopyFromZeros_law : + TraitLaws.from_zeros_valid Unit Zerocopy.Tuple.Insts.ZerocopyFromZeros := + ⟨zeroUnit⟩ + +@[instance] theorem Tuple.Insts.ZerocopyFromBytes_law : + TraitLaws.from_bytes_valid Unit Zerocopy.Tuple.Insts.ZerocopyFromBytes := + ⟨completeUnit⟩ + +@[instance] theorem U8.Insts.ZerocopyFromZeros_law : + TraitLaws.from_zeros_valid U8 Zerocopy.U8.Insts.ZerocopyFromZeros := + ⟨zeroUScalar .U8⟩ + +@[instance] theorem U8.Insts.ZerocopyFromBytes_law : + TraitLaws.from_bytes_valid U8 Zerocopy.U8.Insts.ZerocopyFromBytes := + ⟨completeUScalar .U8⟩ + +@[instance] theorem U32.Insts.ZerocopyFromZeros_law : + TraitLaws.from_zeros_valid U32 Zerocopy.U32.Insts.ZerocopyFromZeros := + ⟨zeroUScalar .U32⟩ + +@[instance] theorem U32.Insts.ZerocopyFromBytes_law : + TraitLaws.from_bytes_valid U32 Zerocopy.U32.Insts.ZerocopyFromBytes := + ⟨completeUScalar .U32⟩ + +@[instance] theorem Bool.Insts.ZerocopyFromZeros_law : + TraitLaws.from_zeros_valid Bool Zerocopy.Bool.Insts.ZerocopyFromZeros := + ⟨zeroBool⟩ + +@[instance] theorem Array.Insts.ZerocopyFromZeros_law + {T : Type} (N : Usize) (dictionary : FromZeros T) [meaning : RustModel T] + [law : TraitLaws.from_zeros_valid T dictionary] : + TraitLaws.from_zeros_valid (Aeneas.Std.Array T N) + (Zerocopy.Array.Insts.ZerocopyFromZeros N dictionary) := + ⟨RustModel.zero_array T N + (@TraitLaws.from_zeros_valid.holds T dictionary meaning law)⟩ + +-- FromBytes also supplies its actual FromZeros parent dictionary's law. The +-- complete array proof uses the stronger element admission promise, while the +-- theorem retains both premises required by that native trait bound. +@[instance] theorem Array.Insts.ZerocopyFromBytes_law + {T : Type} (N : Usize) (dictionary : FromBytes T) [meaning : RustModel T] + [law : TraitLaws.from_bytes_valid T dictionary] + [_parentLaw : TraitLaws.from_zeros_valid T dictionary.FromZerosInst] : + TraitLaws.from_bytes_valid (Aeneas.Std.Array T N) + (Zerocopy.Array.Insts.ZerocopyFromBytes N dictionary) := + ⟨RustModel.complete_array T N + (@TraitLaws.from_bytes_valid.holds T dictionary meaning law)⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RustModel.lean b/verification/aeneas/lean/RustModel.lean index 1aed812ae2..45c33f0d89 100644 --- a/verification/aeneas/lean/RustModel.lean +++ b/verification/aeneas/lean/RustModel.lean @@ -63,6 +63,37 @@ def RustModel.initializedRepresentation (Raw : Type u) [m : RustModel Raw] : Pro | none => False | some decoder => decoder.Initialized +/-- 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, +resource ownership, or the other obligations of a FromBytes implementation. -/ +def RustModel.completeRepresentation (Raw : Type u) [m : RustModel Raw] : Prop := + match m.representation with + | none => False + | some decoder => ∀ bytes, bytes.length = decoder.byteSize → + Rust.Storage.Initialized bytes → + ∃ raw value, decoder.run bytes = some raw ∧ m.decode raw = some value + +/-- The all-zero initialized representation admits both decoding stages of the +same provider. Returning its value makes no claim that output padding retains +the initialized input bytes. -/ +def RustModel.zeroRepresentation (Raw : Type u) [m : RustModel Raw] : Prop := + match m.representation with + | none => False + | some decoder => ∃ raw value, + decoder.run (List.replicate decoder.byteSize (Rust.Storage.AMByte.init 0)) = some raw ∧ + m.decode raw = some value + +/-- Completeness includes the fully initialized all-zero representation. -/ +theorem RustModel.completeRepresentation_zeroRepresentation (Raw : Type u) [m : RustModel Raw] + (complete : RustModel.completeRepresentation Raw) : RustModel.zeroRepresentation Raw := by + cases available : m.representation with + | none => simp [RustModel.completeRepresentation, available] at complete + | some decoder => + simp only [RustModel.completeRepresentation, available] at complete + simp only [RustModel.zeroRepresentation, available] + exact complete _ (by simp) (by simp [Rust.Storage.Initialized]) + /-- Constructing a typed value from bytes requires language-level decoding. The unsupported-model case also fails closed. No invalid Raw is produced. -/ def RustModel.decodeBitsResult {Raw : Type u} (m : RustModel Raw) @@ -87,6 +118,71 @@ def RustModel.decodeBytesResult {Raw : Type u} (m : RustModel Raw) (bytes : List Rust.Storage.AMByte) : Result m.Model := m.decodeResult (m.decodeBitsResult bytes) +/-- Zero initialization returns a raw value only after both the physical and +mathematical decoders accept it. Neither a default value nor a failed model +check can create a successful result. Input bytes are not retained in Raw. -/ +def RustModel.zeroedResult {Raw : Type u} (m : RustModel Raw) : Result Raw := + match m.representation with + | none => .fail .undef + | some decoder => do + let raw ← Result.ofOption + (decoder.run (List.replicate decoder.byteSize (Rust.Storage.AMByte.init 0))) .undef + let _ ← Result.ofOption (m.decode raw) .undef + .ok raw + +/-- Inline contracts can retain the inferred provider while naming the exact +raw value produced by guarded zero initialization. -/ +def RustModel.zeroedValue {Raw : Type u} [m : RustModel Raw] (raw : Raw) : Prop := + m.zeroedResult = .ok raw + +/-- Observe zero initialization through the same retained provider. -/ +def RustModel.zeroedModel {Raw : Type u} (m : RustModel Raw) : Result m.Model := + m.decodeResult m.zeroedResult + +/-- A zero-initialization success records physical decoding and model admission; +no fact about the initialized state of padding in the returned Raw is inferred. -/ +theorem RustModel.zeroedResult_eq_ok_iff {Raw : Type u} (m : RustModel Raw) (raw : Raw) : + m.zeroedResult = .ok raw ↔ ∃ decoder, m.representation = some decoder ∧ + decoder.run (List.replicate decoder.byteSize (Rust.Storage.AMByte.init 0)) = some raw ∧ + ∃ value, m.decode raw = some value := by + cases available : m.representation with + | none => simp [RustModel.zeroedResult, available] + | some decoder => + simp only [RustModel.zeroedResult, available] + cases language : decoder.run + (List.replicate decoder.byteSize (Rust.Storage.AMByte.init 0)) with + | none => simp_all + | some output => + cases model : m.decode output <;> simp_all <;> rintro rfl <;> simp_all + +/-- The guarded zero operation fails exactly when this provider cannot admit +its zero representation. This is model admission failure, not a claim that +an optional mathematical rejection must cause undefined behavior in Rust. -/ +theorem RustModel.zeroedResult_eq_fail_iff {Raw : Type u} (m : RustModel Raw) : + m.zeroedResult = .fail .undef ↔ ¬ @RustModel.zeroRepresentation Raw m := by + cases available : m.representation with + | none => simp [RustModel.zeroedResult, RustModel.zeroRepresentation, available] + | some decoder => + cases language : decoder.run + (List.replicate decoder.byteSize (Rust.Storage.AMByte.init 0)) with + | none => simp_all [RustModel.zeroedResult, RustModel.zeroRepresentation] + | some raw => + cases model : m.decode raw <;> + simp_all [RustModel.zeroedResult, RustModel.zeroRepresentation] + +/-- The zero law supplies a successful guarded construction with its admitted +mathematical witness, retaining the provider used to state the law. -/ +theorem RustModel.zeroedResult_admitted {Raw : Type u} (m : RustModel Raw) + (zero : @RustModel.zeroRepresentation Raw m) : + ∃ raw value, m.zeroedResult = .ok raw ∧ m.decode raw = some value := by + cases available : m.representation with + | none => simp [RustModel.zeroRepresentation, available] at zero + | some decoder => + simp only [RustModel.zeroRepresentation, available] at zero + obtain ⟨raw, value, language, model⟩ := zero + exact ⟨raw, value, + (m.zeroedResult_eq_ok_iff raw).mpr ⟨decoder, available, language, value, model⟩, model⟩ + /-- Explicit metadata-indexed language decoding. No metadata is guessed from byte length, and every rejected width, representation, or metadata returns undef. -/ def RustModel.decodeStorageBitsResult {Raw : Type u} {Metadata : Type v} diff --git a/verification/aeneas/lean/RustRepresentation.lean b/verification/aeneas/lean/RustRepresentation.lean new file mode 100644 index 0000000000..f32519c520 --- /dev/null +++ b/verification/aeneas/lean/RustRepresentation.lean @@ -0,0 +1,190 @@ +/- 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 +import all RustModel +import all ModelPrelude +@[expose] public section + +/-! +These laws concern fixed-size numeric abstract-machine bytes and the retained +physical and mathematical decoders. They establish representation admission, +not Rust provenance, ownership, destruction, or an ABI correspondence. In +particular, zero initialization need not preserve input padding in a raw value. +-/ + +open Aeneas.Std Rust.Storage +namespace AeneasSpecs + +/-- Mapping a complete integer representation to an Aeneas scalar retains every +bit pattern. The mathematical provider observes that same scalar. -/ +theorem completeUScalar (ty : UScalarTy) : + RustModel.completeRepresentation (UScalar ty) := by + intro bytes width initialized + obtain ⟨word, physical⟩ := integerDecoder_complete (ty.numBits / 8) .little bytes width initialized + refine ⟨⟨word.cast (AeneasAdapter.unsigned_byte_width ty)⟩, _, ?_, rfl⟩ + change ((integerDecoder (ty.numBits / 8) .little).map _).run bytes = _ + rw [BitDecoder.run_map, physical] + rfl + +theorem completeIScalar (ty : IScalarTy) : + RustModel.completeRepresentation (IScalar ty) := by + intro bytes width initialized + obtain ⟨word, physical⟩ := integerDecoder_complete (ty.numBits / 8) .little bytes width initialized + refine ⟨⟨word.cast (AeneasAdapter.signed_byte_width ty)⟩, _, ?_, rfl⟩ + change ((integerDecoder (ty.numBits / 8) .little).map _).run bytes = _ + rw [BitDecoder.run_map, physical] + rfl + +theorem zeroUScalar (ty : UScalarTy) : RustModel.zeroRepresentation (UScalar ty) := + RustModel.completeRepresentation_zeroRepresentation _ (completeUScalar ty) + +theorem zeroIScalar (ty : IScalarTy) : RustModel.zeroRepresentation (IScalar ty) := + RustModel.completeRepresentation_zeroRepresentation _ (completeIScalar ty) + +theorem completeUnit : RustModel.completeRepresentation Unit := by + intro bytes width _ + exact ⟨(), (), emptyDecoder_complete () bytes width, rfl⟩ + +theorem zeroUnit : RustModel.zeroRepresentation Unit := + RustModel.completeRepresentation_zeroRepresentation _ completeUnit + +/-- Boolean zero admission does not assert that every byte is a boolean. -/ +theorem zeroBool : RustModel.zeroRepresentation Bool := + ⟨false, false, boolDecoder_run_zero, rfl⟩ + +/-- Count elements rather than dividing by their width. The same argument +therefore handles empty arrays and zero-sized elements. Each accepted element +also retains the witness from the supplied mathematical decoder. -/ +private theorem arrayDecode_model_complete {Raw Model : Type u} + (element : BitDecoder Raw) (decode : Raw → Option Model) (allowed : AMByte → Prop) + (complete : ∀ bytes, bytes.length = element.byteSize → + (∀ byte ∈ bytes, allowed byte) → + ∃ raw value, element.run bytes = some raw ∧ decode raw = some value) + (n : Nat) (bytes : List AMByte) (width : bytes.length = n * element.byteSize) + (all : ∀ byte ∈ bytes, allowed byte) : + ∃ (raw : { values : List Raw // values.length = n }) (values : List Model), + arrayDecode element n bytes = some raw ∧ decodeList decode raw.val = some values := by + induction n generalizing bytes with + | zero => + have empty : bytes = [] := List.length_eq_zero_iff.mp (by simpa using width) + subst bytes + exact ⟨⟨[], rfl⟩, [], rfl, rfl⟩ + | succ n ih => + have sizeBound : element.byteSize ≤ bytes.length := by + rw [Nat.succ_mul] at width + omega + have headWidth : (bytes.take element.byteSize).length = element.byteSize := by + simp [List.length_take, Nat.min_eq_left sizeBound] + have tailWidth : (bytes.drop element.byteSize).length = n * element.byteSize := by + simp only [List.length_drop] + rw [Nat.succ_mul] at width + omega + obtain ⟨head, value, acceptedHead, decodedHead⟩ := complete _ headWidth + (fun byte member => all byte (List.mem_of_mem_take member)) + obtain ⟨tail, values, acceptedTail, decodedTail⟩ := ih _ tailWidth + (fun byte member => all byte (List.mem_of_mem_drop member)) + refine ⟨⟨head :: tail.val, by simp [tail.property]⟩, value :: values, ?_, ?_⟩ + · simp only [arrayDecode, acceptedHead, acceptedTail] + rfl + · simp [decodeList, decodedHead, decodedTail] + +/-- Array completeness uses exactly the element provider supplied to the +canonical array provider, including its mathematical admission check. -/ +theorem RustModel.complete_array (α : Type u) [ma : RustModel α] (n : Usize) + (element : RustModel.completeRepresentation α) : + @RustModel.completeRepresentation (Aeneas.Std.Array α n) (@modelArray α n ma) := by + cases available : ma.representation with + | none => simp [RustModel.completeRepresentation, available] at element + | some decoder => + simp only [RustModel.completeRepresentation, available] at element + unfold RustModel.completeRepresentation + rw [show (@modelArray α n ma).representation = ma.representation.map (fun element => + (arrayDecoder element n.val).map + (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl] + rw [available] + simp only [Option.map_some] + change ∀ bytes, bytes.length = n.val * decoder.byteSize → Initialized bytes → _ + intro bytes width initialized + obtain ⟨raw, values, physical, decoded⟩ := arrayDecode_model_complete decoder ma.decode + (fun byte => ∃ value, byte = AMByte.init value) element n.val bytes width initialized + refine ⟨Aeneas.Std.Array.from raw.val raw.property, + ⟨values, (decodeList_length ma.decode decoded).trans raw.property⟩, ?_, ?_⟩ + · rw [BitDecoder.run_map] + simp [BitDecoder.run, arrayDecoder, width, physical] + · have modelDecoded : decodeList ma.decode + (Aeneas.Std.Array.from raw.val raw.property).val = some values := by + simpa only [Aeneas.Std.Array.from_val] using decoded + dsimp only [RustModel.decode] + split + · rename_i rejected + rw [modelDecoded] at rejected + contradiction + · rename_i output accepted + have same := Option.some.inj (accepted.symm.trans modelDecoded) + cases same + rfl + +private theorem allzero_eq_replicate (bytes : List AMByte) + (all : ∀ byte ∈ bytes, byte = AMByte.init 0) : + bytes = List.replicate bytes.length (AMByte.init 0) := by + induction bytes with + | nil => rfl + | cons byte rest ih => + have head := all byte (by simp) + have tail := ih (fun value member => all value (by simp [member])) + rw [List.length_cons, List.replicate_succ, head] + exact congrArg (AMByte.init 0 :: ·) tail + +/-- Zero arrays need only the element zero law. They do not require complete +admission of all initialized element patterns. -/ +theorem RustModel.zero_array (α : Type u) [ma : RustModel α] (n : Usize) + (element : RustModel.zeroRepresentation α) : + @RustModel.zeroRepresentation (Aeneas.Std.Array α n) (@modelArray α n ma) := by + cases available : ma.representation with + | none => simp [RustModel.zeroRepresentation, available] at element + | some decoder => + simp only [RustModel.zeroRepresentation, available] at element + have zeroComplete : ∀ bytes, bytes.length = decoder.byteSize → + (∀ byte ∈ bytes, byte = AMByte.init 0) → + ∃ raw value, decoder.run bytes = some raw ∧ ma.decode raw = some value := by + intro bytes width all + have same := allzero_eq_replicate bytes all + rw [width] at same + simpa only [same] using element + obtain ⟨raw, values, physical, decoded⟩ := arrayDecode_model_complete decoder ma.decode + (fun byte => byte = AMByte.init 0) zeroComplete n.val + (List.replicate (n.val * decoder.byteSize) (AMByte.init 0)) (by simp) (by simp) + unfold RustModel.zeroRepresentation + rw [show (@modelArray α n ma).representation = ma.representation.map (fun element => + (arrayDecoder element n.val).map + (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl] + rw [available] + simp only [Option.map_some] + refine ⟨Aeneas.Std.Array.from raw.val raw.property, + ⟨values, (decodeList_length ma.decode decoded).trans raw.property⟩, ?_, ?_⟩ + · change ((arrayDecoder decoder n.val).map _).run + (List.replicate (n.val * decoder.byteSize) (AMByte.init 0)) = _ + rw [BitDecoder.run_map] + simp only [BitDecoder.run, arrayDecoder, List.length_replicate, ↓reduceIte, physical, + Option.map_some] + · have modelDecoded : decodeList ma.decode + (Aeneas.Std.Array.from raw.val raw.property).val = some values := by + simpa only [Aeneas.Std.Array.from_val] using decoded + dsimp only [RustModel.decode] + split + · rename_i rejected + rw [modelDecoded] at rejected + contradiction + · rename_i output accepted + have same := Option.some.inj (accepted.symm.trans modelDecoded) + cases same + rfl + +end AeneasSpecs diff --git a/verification/aeneas/lean/RustRepresentationTests.lean b/verification/aeneas/lean/RustRepresentationTests.lean new file mode 100644 index 0000000000..f3b391717f --- /dev/null +++ b/verification/aeneas/lean/RustRepresentationTests.lean @@ -0,0 +1,124 @@ +/- 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 RustRepresentation +import all RustModel +import all ModelPrelude +@[expose] public section + +/-! +These tests challenge representation admission, including the distinction +between physical validity and a retained provider's optional invariant. They +are pure Lean model tests, not executions of invalid Rust. +-/ + +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage +namespace RustRepresentationTests + +example (ty : UScalarTy) : RustModel.completeRepresentation (UScalar ty) := completeUScalar ty +example (ty : IScalarTy) : RustModel.completeRepresentation (IScalar ty) := completeIScalar ty +example (ty : UScalarTy) : RustModel.zeroRepresentation (UScalar ty) := zeroUScalar ty +example (ty : IScalarTy) : RustModel.zeroRepresentation (IScalar ty) := zeroIScalar ty +example : RustModel.completeRepresentation Unit := completeUnit +example : RustModel.zeroRepresentation Bool := zeroBool + +example : RustModel.completeRepresentation (Aeneas.Std.Array U16 (3#usize)) := + RustModel.complete_array _ _ (completeUScalar .U16) +example : RustModel.completeRepresentation (Aeneas.Std.Array Unit (4#usize)) := + RustModel.complete_array _ _ completeUnit +example : RustModel.completeRepresentation (Aeneas.Std.Array U8 (0#usize)) := + RustModel.complete_array _ _ (completeUScalar .U8) +example : RustModel.zeroRepresentation + (Aeneas.Std.Array (Aeneas.Std.Array Bool (2#usize)) (3#usize)) := + RustModel.zero_array _ _ (RustModel.zero_array _ _ zeroBool) + +-- An initialized byte of value two refutes boolean completeness, although +-- zero itself is admitted. This is a proved counterexample, not a tactic failure. +example : ¬ RustModel.completeRepresentation Bool := by + intro complete + obtain ⟨raw, value, physical, _⟩ := complete [AMByte.init 2] rfl (by simp [Initialized]) + rw [boolDecoder_run_two] at physical + contradiction + +-- NonZero rejects the integer zero pattern at its physical decoding stage. +theorem nonzeroU8_not_zero : ¬ RustModel.zeroRepresentation + (core.num.nonzero.NonZero U8 core.num.niche_types.NonZeroU8Inner) := by + intro zero + obtain ⟨raw, value, physical, _⟩ := zero + change none = some raw at physical + contradiction +example : ¬ RustModel.completeRepresentation + (core.num.nonzero.NonZero U8 core.num.niche_types.NonZeroU8Inner) := by + intro complete + have zero := RustModel.completeRepresentation_zeroRepresentation _ complete + obtain ⟨raw, value, physical, _⟩ := zero + change none = some raw at physical + contradiction +example : (modelNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).zeroedResult = + .fail .undef := + ((modelNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner).zeroedResult_eq_fail_iff).mpr + nonzeroU8_not_zero + +-- Missing physical semantics fail closed even for an inhabited raw carrier. +example : ¬ RustModel.completeRepresentation Nat := by + simp [RustModel.completeRepresentation, RustModel.representation] +example : ¬ RustModel.zeroRepresentation Nat := by + simp [RustModel.zeroRepresentation, RustModel.representation] +example : modelNat.zeroedResult = .fail .undef := rfl + +-- The same physical domain with a provider rejecting zero must reject the +-- zero law and the guarded operation. Physical success alone is insufficient. +@[reducible] def rejectsZero : RustModel U8 where + Model := Unit + decode raw := if raw.val = 0 then none else some () + representation := some (uScalarBitDecoder .U8) + +theorem rejectsZero_not_zero : ¬ @RustModel.zeroRepresentation U8 rejectsZero := by + intro zero + obtain ⟨raw, value, physical, model⟩ := zero + change some (0#u8) = some raw at physical + cases Option.some.inj physical + change none = some value at model + contradiction +example : rejectsZero.zeroedResult = .fail .undef := + rejectsZero.zeroedResult_eq_fail_iff.mpr rejectsZero_not_zero + +theorem bool_zeroed : modelBool.zeroedResult = .ok false := by + exact (modelBool.zeroedResult_eq_ok_iff false).mpr ⟨boolDecoder, rfl, rfl, false, rfl⟩ +example : modelUnit.zeroedResult = .ok () := by + exact (modelUnit.zeroedResult_eq_ok_iff ()).mpr ⟨unitDecoder, rfl, rfl, (), rfl⟩ +example : (modelUScalar .U16).zeroedResult = .ok (0#u16) := by + exact ((modelUScalar .U16).zeroedResult_eq_ok_iff _).mpr + ⟨uScalarBitDecoder .U16, rfl, rfl, unsignedWord (0#u16), rfl⟩ +example : (modelIScalar .I16).zeroedResult = .ok (0#i16) := by + exact ((modelIScalar .I16).zeroedResult_eq_ok_iff _).mpr + ⟨iScalarBitDecoder .I16, rfl, rfl, signedWord (0#i16), rfl⟩ +example : modelBool.zeroedModel = .ok false := by + unfold RustModel.zeroedModel + rw [bool_zeroed, RustModel.decodeResult_ok] + rfl +example : RustModel.zeroedValue false := bool_zeroed + +-- Zero law success retains the actual provider's mathematical witness. +example {Raw : Type} (m : RustModel Raw) (law : @RustModel.zeroRepresentation Raw m) : + ∃ raw value, m.zeroedResult = .ok raw ∧ m.decode raw = some value := + m.zeroedResult_admitted law + +-- Permitting divergence must not permit a forbidden zero construction. The +-- same backstop applies even if the caller discards the result entirely. +example {Raw : Type} (m : RustModel Raw) (rejected : ¬ @RustModel.zeroRepresentation Raw m) : + ¬ WP.spec m.zeroedResult (fun _ => True) := by + rw [m.zeroedResult_eq_fail_iff.mpr rejected] + simp +example {Raw : Type} (m : RustModel Raw) (rejected : ¬ @RustModel.zeroRepresentation Raw m) : + ¬ WP.dspec m.zeroedResult (fun _ => True) := by + rw [m.zeroedResult_eq_fail_iff.mpr rejected] + simp + +end RustRepresentationTests diff --git a/verification/aeneas/lean/SpecsSyntax.lean b/verification/aeneas/lean/SpecsSyntax.lean index 65d1658ba7..ce0f326850 100644 --- a/verification/aeneas/lean/SpecsSyntax.lean +++ b/verification/aeneas/lean/SpecsSyntax.lean @@ -68,8 +68,12 @@ no decoded witness, ghost, or requirement can enter this argument prefix. -/ private meta partial def withOriginalInputs (carrier : Expr) (inputs : Array Expr) (k : Array Expr → Expr → Elab.Term.TermElabM Expr) : Elab.Term.TermElabM Expr := do match carrier with - | .forallE binderName domain body _ => - Meta.withLocalDeclD binderName.eraseMacroScopes domain fun input => do + | .forallE binderName domain body info => + -- Preserve semantic instance arguments so elaboration and the native-input + -- audit see the exact provider used by the computation. Source arguments + -- remain explicit in the specification as before. + let info := if info.isInstImplicit then info else BinderInfo.default + Meta.withLocalDecl binderName.eraseMacroScopes info domain fun input => do checkFreshNames inputs #[input] withOriginalInputs (body.instantiate1 input) (inputs.push input) k | _ => k inputs carrier @@ -191,7 +195,8 @@ private meta def postcondition (posts : Array Syntax) (raws maths : Array Expr) | _ => throwErrorAt function "A specification must name a bare extracted function constant" let functionName ← Elab.realizeGlobalConstNoOverloadWithInfo id let functionExpr ← Meta.mkConstWithFreshMVarLevels functionName - withOriginalInputs (← Meta.inferType functionExpr) #[] fun originals returnType => do + withOriginalInputs (← Meta.inferType functionExpr) #[] fun allInputs returnType => do + let (originals, retained) ← splitNativeModels allInputs -- The generated count identifies the source generic prefix. Check both -- sides of the boundary: counted parameters must be Type-valued, and -- later value arguments must not contain an omitted type parameter. @@ -214,8 +219,9 @@ private meta def postcondition (posts : Array Syntax) (raws maths : Array Expr) let computationalDictionaries := originals.extract count.getNat (count.getNat + traitCount) let raws := originals.extract (count.getNat + traitCount) originals.size let inputNames ← raws.mapM fun raw => return (← raw.fvarId!.getDecl).userName - withModelDictionaries params fun dictionaries => - withTraitLawAssumptions computationalDictionaries params dictionaries fun traitEvidence => do + withBoundModelDictionaries params retained fun dictionaries => + withDefaultTraitDictionary functionName params fun enclosing => + withTraitLawAssumptions (computationalDictionaries ++ enclosing) params dictionaries fun traitEvidence => do -- Fix all automatic providers before introducing decoded witnesses, -- dependent ghosts, requirements, or their local instances. let providers ← raws.mapM fun raw => do @@ -224,7 +230,8 @@ private meta def postcondition (posts : Array Syntax) (raws maths : Array Expr) withDecodedInputs raws providers 0 #[] #[] fun maths equations => do let decodedPrefix := (maths.zip equations).foldl (fun inputs pair => inputs ++ #[pair.1, pair.2]) #[] - let boundPrefix := originals ++ dictionaries ++ traitEvidence ++ decodedPrefix + let supplemental := dictionaries.filter (!retained.contains ·) + let boundPrefix := originals ++ retained ++ supplemental ++ enclosing ++ traitEvidence ++ decodedPrefix withClauseScope raws maths false <| Elab.Term.elabBinders ghosts fun ghostInputs => do -- Restore raw names as the baseline for each clause-specific scope. let mut lctx ← getLCtx @@ -238,7 +245,7 @@ private meta def postcondition (posts : Array Syntax) (raws maths : Array Expr) -- Execute on the untouched raw prefix. Total WP.spec excludes -- panic and divergence; partial WP.dspec allows divergence but -- still checks every successful return and excludes panic. - let call := mkAppN functionExpr originals + let call := mkAppN functionExpr (originals ++ retained) let wp := if mode.getNat == 0 then ``WP.spec else ``WP.dspec let body ← Meta.mkAppM wp #[call, post] Elab.Term.synthesizeSyntheticMVarsNoPostponing @@ -306,11 +313,15 @@ meta def specBinding (specName : Name) : MetaM (Name × Nat) := do let arguments := call.getAppArgs unless inputs.size ≥ arguments.size do throwError "Specification {specName} has more model arguments than bound inputs" - -- Exact expression identity rejects reordered, replaced, or reconstructed - -- arguments, even when a replacement might compute the same value. + -- This prefix includes any retained semantic providers because execution + -- depends on them. The independent Rust count below excludes that suffix. for index in [:arguments.size] do unless arguments[index]!.consumeMData == inputs[index]! do throwError "Specification {specName} model input {index + 1} is not its original bound variable" + forallTelescope (← inferType call.getAppFn) fun native _ => do + let _ ← splitNativeModels native + unless arguments.size == native.size do + throwError "Specification {specName} has a different native argument inventory" pure (modelName, arguments.size) /-- The contract family abstracts only the audited execution node. Original @@ -326,7 +337,8 @@ meta def abstractSpecContract (specName : Name) : MetaM Expr := do let body := body.consumeMData let args := body.getAppArgs let call := args[1]! - -- Keep original arguments outside the outcome binder. All dictionaries, + -- Keep the exact execution arguments, including retained semantic providers, + -- outside the outcome binder. Additional specification dictionaries, -- witnesses, ghosts, and premises belong to the one outcome inside it. withLocalDeclD `_executionOutcome (← inferType call) fun outcome => do let predicate := mkAppN body.getAppFn #[args[0]!, outcome, args[2]!] @@ -389,7 +401,10 @@ elab "check_spec_binding " candidate:ident " for " extractedId:ident " with " co let (actualModel, inputCount) ← withRef candidate (specBinding specName) unless actualModel == modelName do throwErrorAt candidate "Specification {specName} does not call the expected model {modelName}" - unless inputCount == count.getNat do + let semanticCount ← forallTelescope (← getConstInfo modelName).type fun native _ => do + let (_, models) ← splitNativeModels native + pure models.size + unless inputCount == count.getNat + semanticCount do throwErrorAt candidate "Specification {specName} does not bind exactly {count.getNat} model inputs" checkSpecContract specName diff --git a/verification/aeneas/lean/TraitLawsSupport.lean b/verification/aeneas/lean/TraitLawsSupport.lean index 341a59621a..03d30dfa0f 100644 --- a/verification/aeneas/lean/TraitLawsSupport.lean +++ b/verification/aeneas/lean/TraitLawsSupport.lean @@ -72,6 +72,37 @@ meta def withTraitLawAssumptions (dictionaries params models : Array Expr) (k : Array Expr → TermElabM α) : TermElabM α := visitDictionaryLaws (dictionaries.toList.map (fun dictionary => (dictionary, []))) params models #[] k +/-- This registry records a compiler-checked Self bound removed from a default +method's computational arguments. It supplies a specification premise only; +the dictionary is never passed to the extracted body. -/ +structure DefaultTraitBody where + function : Name + trait : Name + parameterCount : Nat + +meta initialize defaultTraitBodyExtension : + SimplePersistentEnvExtension DefaultTraitBody (NameMap DefaultTraitBody) ← + registerSimplePersistentEnvExtension { + addEntryFn := fun state entry => state.insert entry.function entry + addImportedFn := fun entries => entries.foldl (fun state rows => + rows.foldl (fun state row => state.insert row.function row) state) {} } + +meta def defaultTraitBody? (function : Name) : MetaM (Option DefaultTraitBody) := do + return (defaultTraitBodyExtension.getState (← getEnv)).find? function + +meta def defaultTraitBodies : MetaM (Array DefaultTraitBody) := do + return (defaultTraitBodyExtension.getState (← getEnv)).toArray.map (·.2) + +meta def withDefaultTraitDictionary (function : Name) (params : Array Expr) + (k : Array Expr → TermElabM α) : TermElabM α := do + let some owner ← defaultTraitBody? function | return ← k #[] + unless owner.parameterCount ≤ params.size do throwError "Invalid enclosing trait parameter prefix" + let carrier := mkAppN (← mkConstWithFreshMVarLevels owner.trait) + (params.extract 0 owner.parameterCount) + unless (← traitDictionary? carrier).isSome do + throwError "Default method's enclosing trait is not a registered dictionary" + withLocalDeclD `_enclosingTrait carrier fun dictionary => k #[dictionary] + private meta def bareConstant (stx : Syntax) : TermElabM Name := do let id ← match stx with | `(@$id:ident) => pure id @@ -88,6 +119,17 @@ elab "trait_dictionary " raw:term:max : command => Command.liftTermElabM do throwErrorAt raw "An extracted trait dictionary must produce a Type" modifyEnv (traitLawExtension.addEntry · {raw := declName}) +elab "default_trait_body " functionId:ident " for " traitId:ident + " with " count:num " type " "parameters" : command => Command.liftTermElabM do + let function ← realizeGlobalConstNoOverloadWithInfo functionId + let trait ← realizeGlobalConstNoOverloadWithInfo traitId + if (← defaultTraitBody? function).isSome then + throwError "Duplicate enclosing trait bound for {function}" + forallTelescope (← getConstInfo trait).type fun params result => do + unless params.size == count.getNat && result.isSort do + throwError "Default method's enclosing trait has a different parameter count" + modifyEnv (defaultTraitBodyExtension.addEntry · {function, trait, parameterCount := count.getNat}) + private meta def expressionText (expression : Expr) : TermElabM String := do return (← withOptions (fun options => (options.setBool `pp.explicit true) |>.setBool `pp.universes false) (ppExpr expression)).pretty 100000 @@ -180,7 +222,8 @@ meta def checkTraitImplementationNativeParameters (implementation : Name) : MetaM Unit := do unless constParameters.size == constCount do throwError "Trait implementation changed its original const inventory" - forallTelescope (← getConstInfo implementation).type fun inputs _ => do + forallTelescope (← getConstInfo implementation).type fun allInputs _ => do + let (inputs, _) ← splitNativeModels allInputs unless inputs.size == typeCount + constCount + dictionaryCount do throwError "Trait implementation changed its original native parameter count" for input in inputs.extract 0 typeCount do @@ -207,7 +250,8 @@ cannot acquire an arbitrary extra premise that simply assumes the implementation -/ meta def traitImplementationObligation (law implementation : Name) : TermElabM Expr := do let implementationExpr ← mkConstWithFreshMVarLevels implementation - forallTelescope (← inferType implementationExpr) fun inputs result => do + forallTelescope (← inferType implementationExpr) fun nativeInputs result => do + let (inputs, retained) ← splitNativeModels nativeInputs let some binding ← traitDictionary? result | throwError "Implementation does not return an extracted trait dictionary" unless binding.law == some law do @@ -221,17 +265,17 @@ meta def traitImplementationObligation (law implementation : Name) : TermElabM E dictionaries := dictionaries.push input else if ← isDefEq carrier (mkConst ``Aeneas.Std.Usize) then pure () else throwError "Unsupported non-dictionary implementation parameter: {carrier}" - withModelDictionaries params fun models => + withBoundModelDictionaries params retained fun models => withTraitLawAssumptions dictionaries params models fun evidence => do - let dictionary := mkAppN implementationExpr inputs + let dictionary := mkAppN implementationExpr nativeInputs let target ← traitLawProposition binding result dictionary params models -- Only providers actually used by the target or input laws are indices. -- In particular, an output law is never introduced as an assumption. let evidenceTypes ← evidence.mapM fun e => inferType e - let used := models.filter fun provider => - target.containsFVar provider.fvarId! || - evidenceTypes.any (·.containsFVar provider.fvarId!) - mkForallFVars (inputs ++ used ++ evidence) target + let used := models.filter fun provider => !retained.contains provider && + (target.containsFVar provider.fvarId! || + evidenceTypes.any (·.containsFVar provider.fvarId!)) + mkForallFVars (nativeInputs ++ used ++ evidence) target /-- The native implementation determines its witness name; no second roster can omit an implementation while retaining its authored proof. -/ @@ -251,6 +295,7 @@ meta def auditTraitImplementationProof (law implementation proof : Name) : TermE unless original.size ≤ inputs.size do throwError "Trait implementation proof omitted original native inputs" let nativeInputs := inputs.extract 0 original.size + let (rustInputs, retained) ← splitNativeModels nativeInputs let subst (e : Expr) := e.replaceFVars original nativeInputs for i in [:original.size] do unless ← isDefEq (← inferType nativeInputs[i]!) (subst (← inferType original[i]!)) do @@ -262,7 +307,7 @@ meta def auditTraitImplementationProof (law implementation proof : Name) : TermE throwError "Implementation returns a different annotated trait" let mut params := #[] let mut pending : List (Expr × List Name) := [] - for input in nativeInputs do + for input in rustInputs do let carrier ← inferType input if (← whnf carrier).isSort then params := params.push input else if (← traitDictionary? carrier).isSome then @@ -273,9 +318,13 @@ meta def auditTraitImplementationProof (law implementation proof : Name) : TermE -- the placeholders referenced by the actual input laws or conclusion. let rec providers (index : Nat) (models : Array Expr) : TermElabM Unit := do if index < params.size then - withLocalDecl (Name.mkSimple s!"_auditModel{index}") .instImplicit - (← mkAppM ``RustModel #[params[index]!]) fun provider => - providers (index + 1) (models.push provider) + let carrier ← mkAppM ``RustModel #[params[index]!] + let matching ← retained.filterM fun provider => do isDefEq (← inferType provider) carrier + if matching.size == 1 then + providers (index + 1) (models.push matching[0]!) + else + withLocalDecl (Name.mkSimple s!"_auditModel{index}") .instImplicit + carrier fun provider => providers (index + 1) (models.push provider) else do let inspect (binding : TraitLawBinding) (carrier dictionary : Expr) : MetaM Expr := do let some className := binding.law | throwError "Missing annotated law" @@ -303,8 +352,8 @@ meta def auditTraitImplementationProof (law implementation proof : Name) : TermE if (← traitDictionary? (← inferType parent)).isSome then parents := parents ++ [(parent, binding.raw :: ancestors)] queue := parents ++ queue - let used := models.filter fun provider => - target.containsFVar provider.fvarId! || laws.any (fun entry => entry.1.containsFVar provider.fvarId!) + let used := models.filter fun provider => !retained.contains provider && + (target.containsFVar provider.fvarId! || laws.any (fun entry => entry.1.containsFVar provider.fvarId!)) unless inputs.size == nativeInputs.size + used.size + laws.size do throwError "Trait implementation proof omitted required inputs or added premises" let meanings := inputs.extract nativeInputs.size (nativeInputs.size + used.size) diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index 68313fb2df..f2eb383889 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -8,6 +8,7 @@ those terms. -/ module public import Zerocopy.Types +public import ModelPrelude @[expose] public section open Aeneas Aeneas.Std open Zerocopy @@ -26,6 +27,56 @@ def core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone -- propagate it rather than turn it into a successful return or divergence. def Zerocopy.forbiddenExecution {α : Type} : Result α := .fail .undef +-- The native default constructor retains this interpretation's model provider +-- as an implicit semantic parameter. Decoding must succeed before a typed +-- result is returned; neither an absent decoder nor a rejected bit pattern +-- supplies a default value. The physical decoder's Rust correspondence is an +-- explicit premise, checked against the supported native layout profiles. +noncomputable def core.mem.zeroed (T : Type) [model : AeneasSpecs.RustModel T] : Result T := + model.zeroedResult + +-- These required validator fields carry their actual native signatures. Their +-- pointer-based implementations have no admitted execution semantics yet. +-- Keeping a field is not permission to call it: admission rejects every such +-- call, and the compiled audit requires these whole definitions to return +-- undef. They let representation laws mention real FromZeros/FromBytes +-- dictionaries without asserting anything about TryFromBytes validation. +def Zerocopy.Tuple.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (_alignment : pointer.invariant.Alignment Alignment) + (_candidate : pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly Unit) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized) : Result Bool := + .fail .undef + +def Zerocopy.U8.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (_alignment : pointer.invariant.Alignment Alignment) + (_candidate : pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly U8) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized) : Result Bool := + .fail .undef + +def Zerocopy.U32.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (_alignment : pointer.invariant.Alignment Alignment) + (_candidate : pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly U32) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized) : Result Bool := + .fail .undef + +def Zerocopy.Bool.Insts.ZerocopyTryFromBytes.is_safe + {Alignment : Type} (_alignment : pointer.invariant.Alignment Alignment) + (_candidate : pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly Bool) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized) : Result Bool := + .fail .undef + +def Zerocopy.Array.Insts.ZerocopyTryFromBytes.is_safe + {T Alignment : Type} {N : Usize} (_element : TryFromBytes T) + (_alignment : pointer.invariant.Alignment Alignment) + (_candidate : pointer.ptr.def.Ptr (wrappers.read_only_def.ReadOnly (Aeneas.Std.Array T N)) + (pointer.invariant.Shared × Alignment × pointer.invariant.Initialized) + pointer.invariant.Shared Alignment pointer.invariant.Initialized) : Result Bool := + .fail .undef + -- This is an interpretation of the whole Rust helper, whose raw-pointer body -- is deliberately opaque to extraction. Valid input references supply separate -- readable source and exclusive destination regions. The additional length diff --git a/verification/aeneas/lean/Zerocopy/TypesExternal.lean b/verification/aeneas/lean/Zerocopy/TypesExternal.lean index 41ca7b502f..b4db59b501 100644 --- a/verification/aeneas/lean/Zerocopy/TypesExternal.lean +++ b/verification/aeneas/lean/Zerocopy/TypesExternal.lean @@ -42,3 +42,9 @@ structure core.cell.Cell (T : Type) where structure core.cell.UnsafeCell (T : Type) where value : T + +-- Required TryFromBytes validator signatures mention Ptr even when no +-- validator is executed. Keep that carrier abstract: it grants no construction, +-- memory access, or provenance facts. Admission rejects Ptr as a value-domain +-- execution carrier, and Check audits this exact type-only signature. +axiom Zerocopy.pointer.ptr.def.Ptr (T I Aliasing Alignment Validity : Type) : Type diff --git a/verification/aeneas/lean/ZeroedAudit.lean b/verification/aeneas/lean/ZeroedAudit.lean new file mode 100644 index 0000000000..2167cc4f02 --- /dev/null +++ b/verification/aeneas/lean/ZeroedAudit.lean @@ -0,0 +1,207 @@ +/- 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 NativeModels +public meta import Lean +public section + +open Lean Meta Elab + +/-! +The zero-initialization primitive receives its semantic provider from the native +caller's retained model suffix. Audit the whole interpretation, the original +compiler call inventory, and each compiled application independently of its +functional proof. The pointer carrier and validator fields support dictionary +signatures only; their presence supplies no pointer execution semantics. +-/ + +private meta partial def zeroedCalls (expression : Expr) : Array Expr := + if expression.getAppFn.isConstOf `core.mem.zeroed then + #[expression] ++ expression.getAppArgs.foldl + (fun found arg => found ++ zeroedCalls arg) #[] + else + match expression with + | .app fn arg => zeroedCalls fn ++ zeroedCalls arg + | .lam _ ty body _ | .forallE _ ty body _ => + zeroedCalls ty ++ zeroedCalls body + | .letE _ ty value body _ => + zeroedCalls ty ++ zeroedCalls value ++ zeroedCalls body + | .mdata _ body | .proj _ _ body => zeroedCalls body + | _ => #[] + +private meta def checkZeroedDefinition (declName : Name) + (expected : TSyntax `term) (binders : Array BinderInfo) : TermElabM Unit := do + let expectedBody ← Term.elabTerm expected none + Term.synthesizeSyntheticMVarsNoPostponing + let expectedBody ← instantiateMVars expectedBody + let env ← getEnv + let some (.defnInfo actual) := env.find? declName + | throwError "Zeroed boundary declaration {declName} must be a definition" + unless actual.levelParams.isEmpty && + (← isDefEq actual.type (← inferType expectedBody)) && + (← isDefEq actual.value expectedBody) do + throwError "Zeroed boundary declaration {declName} changed its full signature or body" + forallTelescope actual.type fun inputs _ => do + let actualBinders ← inputs.mapM fun input => do + return (← input.fvarId!.getDecl).binderInfo + unless actualBinders == binders do + throwError "Zeroed boundary declaration {declName} changed its argument binders" + +/-- Pin the opaque pointer data carrier and all five interface-only validators +whenever this interface boundary is present, independently of zeroed calls. -/ +meta def auditInterfaceOnlyCarriers : TermElabM Unit := do + let env ← getEnv + let declarations := #[`Zerocopy.pointer.ptr.def.Ptr, + `Zerocopy.Tuple.Insts.ZerocopyTryFromBytes.is_safe, + `Zerocopy.U8.Insts.ZerocopyTryFromBytes.is_safe, + `Zerocopy.U32.Insts.ZerocopyTryFromBytes.is_safe, + `Zerocopy.Bool.Insts.ZerocopyTryFromBytes.is_safe, + `Zerocopy.Array.Insts.ZerocopyTryFromBytes.is_safe] + unless declarations.any env.contains do return + let some (.axiomInfo carrier) := env.find? `Zerocopy.pointer.ptr.def.Ptr + | throwError "Zeroed interfaces require the pinned opaque Ptr carrier" + let expectedCarrier ← Term.elabType (← `(Type → Type → Type → Type → Type → Type)) + unless carrier.levelParams.isEmpty && (← isDefEq carrier.type expectedCarrier) do + throwError "Opaque Ptr carrier changed its five-argument data-only signature" + forallTelescope carrier.type fun inputs _ => do + unless inputs.size == 5 do + throwError "Opaque Ptr carrier changed its number of type arguments" + for input in inputs do + unless (← input.fvarId!.getDecl).binderInfo == .default do + throwError "Opaque Ptr carrier changed its explicit type arguments" + for (declName, raw) in #[(`Zerocopy.Tuple.Insts.ZerocopyTryFromBytes.is_safe, + (← `(Unit))), + (`Zerocopy.U8.Insts.ZerocopyTryFromBytes.is_safe, + (← `(Aeneas.Std.U8))), + (`Zerocopy.U32.Insts.ZerocopyTryFromBytes.is_safe, + (← `(Aeneas.Std.U32))), + (`Zerocopy.Bool.Insts.ZerocopyTryFromBytes.is_safe, + (← `(Bool)))] do + checkZeroedDefinition declName (← `(fun {Alignment : Type} + (_alignment : Zerocopy.pointer.invariant.Alignment Alignment) + (_candidate : Zerocopy.pointer.ptr.def.Ptr + (Zerocopy.wrappers.read_only_def.ReadOnly $raw) + (Zerocopy.pointer.invariant.Shared × Alignment × + Zerocopy.pointer.invariant.Initialized) + Zerocopy.pointer.invariant.Shared Alignment + Zerocopy.pointer.invariant.Initialized) => + (Aeneas.Std.Result.fail Aeneas.Std.Error.undef : Aeneas.Std.Result Bool))) + #[.implicit, .default, .default] + checkZeroedDefinition `Zerocopy.Array.Insts.ZerocopyTryFromBytes.is_safe + (← `(fun {T Alignment : Type} {N : Aeneas.Std.Usize} + (_element : Zerocopy.TryFromBytes T) + (_alignment : Zerocopy.pointer.invariant.Alignment Alignment) + (_candidate : Zerocopy.pointer.ptr.def.Ptr + (Zerocopy.wrappers.read_only_def.ReadOnly (Aeneas.Std.Array T N)) + (Zerocopy.pointer.invariant.Shared × Alignment × + Zerocopy.pointer.invariant.Initialized) + Zerocopy.pointer.invariant.Shared Alignment + Zerocopy.pointer.invariant.Initialized) => + (Aeneas.Std.Result.fail Aeneas.Std.Error.undef : Aeneas.Std.Result Bool))) + #[.implicit, .implicit, .implicit, .default, .default, .default] + +/-- Check that every emitted native zeroed call retains the exact original type +variable and that variable's exact model provider. Compiler call rows retain +ownership and multiplicity across lowering; split-loop bodies consume the same +owner's aggregate inventory. Only the currently extracted T0 endpoint is +supported, so adding another endpoint requires an explicit audit extension. -/ +meta def auditZeroed (bindings : Json) : TermElabM Unit := do + auditInterfaceOnlyCarriers + unless (← getEnv).contains `core.mem.zeroed do return + checkZeroedDefinition `core.mem.zeroed + (← `(fun (T : Type) [model : AeneasSpecs.RustModel T] => model.zeroedResult)) + #[.default, .instImplicit] + let .ok admission := bindings.getObjVal? "admission" + | throwError "Zeroed requires original compiler admission" + let .ok stages := admission.getObjVal? "stages" + | throwError "Zeroed requires both compiler admission stages" + let .ok original := stages.getObjVal? "before" + | throwError "Zeroed lacks original compiler admission" + let .ok lowered := stages.getObjVal? "llbc" + | throwError "Zeroed lacks lowered compiler admission" + let .ok originalCalls := original.getObjValAs? (Array Json) "calls" + | throwError "Zeroed lacks original compiler call evidence" + let .ok loweredCalls := lowered.getObjValAs? (Array Json) "calls" + | throwError "Zeroed lacks lowered compiler call evidence" + let originalZeroed := originalCalls.filter fun row => + row.getObjValAs? String "callee" == .ok "core::mem::zeroed" + let loweredZeroed := loweredCalls.filter fun row => + row.getObjValAs? String "callee" == .ok "core::mem::zeroed" + unless originalZeroed == loweredZeroed do + throwError "Zeroed changed original Rust type arguments, ownership, or multiplicity" + let .ok executions := lowered.getObjValAs? (Array Json) "executions" + | throwError "Zeroed lacks the complete admitted execution closure" + for row in loweredZeroed do + let .ok rust := row.getObjValAs? String "caller" + | throwError "Zeroed compiler call lacks its Rust owner" + let .ok _ := row.getObjValAs? Nat "caller_def_id" + | throwError "Zeroed compiler call lacks its original compiler identity" + unless row.getObjValAs? (Array String) "type_arguments" == .ok #["T0"] do + throwError "Unsupported original Rust zeroed endpoint in {rust}" + unless executions.any (fun execution => + execution.getObjValAs? String "rust" == .ok rust && + execution.getObjValAs? String "origin" == .ok "body") do + throwError "Zeroed call owner {rust} is not an admitted native body" + let nativeText ← IO.FS.readFile "Zerocopy/translation.json" + let .ok native := Json.parse nativeText + | throwError "Invalid native zeroed call map" + let .ok functions := native.getObjValAs? (Array Json) "functions" + | throwError "Missing native zeroed function inventory" + let env ← getEnv + let mut names : Array Name := #[] + let mut remaining := loweredZeroed + -- Native dictionaries can spell a Rust owner differently from admission. + -- Inspect every emitted body and match calls by their compiler identities, + -- rather than skipping helpers whose displayed owner names differ. + for candidate in functions do + let .ok isOpaque := candidate.getObjValAs? Bool "is_opaque" + | throwError "Native zeroed owner lacks its body disposition" + if isOpaque then continue + let .ok ident := candidate.getObjValAs? Nat "def_id" + | throwError "Native zeroed owner lacks its compiler identity" + let .ok raw := candidate.getObjValAs? String "lean_name" + | throwError "Native zeroed owner lacks its compiled name" + unless !names.contains raw.toName do + throwError "Repeated native zeroed owner {raw}" + names := names.push raw.toName + let some (.defnInfo owner) := env.find? raw.toName + | throwError "Native zeroed owner {raw} must retain its compiled body" + remaining ← lambdaTelescope owner.value fun inputs body => do + let mut calls := zeroedCalls body + for input in inputs do + calls := calls ++ zeroedCalls (← inferType input) + if calls.isEmpty then return remaining + let (original, models) ← AeneasSpecs.splitNativeModels inputs + let typeInputs ← original.filterM fun input => do + match ← whnf (← inferType input) with + | .sort level => return !level.isZero + | _ => return false + let some target := typeInputs[0]? + | throwError "Native zeroed owner {raw} lacks original Rust type variable T0" + let matchingModels ← models.filterM fun model => do + let type ← whnf (← inferType model) + return type.getAppFn.isConstOf ``AeneasSpecs.RustModel && + type.getAppArgs == #[target] + unless matchingModels.size == 1 do + throwError "Native zeroed owner {raw} lacks the exact retained T0 provider" + let mut unconsumed := remaining + for call in calls do + let args := call.getAppArgs + unless args.size == 2 && args[0]! == target && + args[1]! == matchingModels[0]! do + throwError "Native zeroed call in {raw} changed its original type or retained provider" + let some index := unconsumed.findIdx? (fun row => + row.getObjValAs? Nat "caller_def_id" == .ok ident) + | throwError "Unexpected compiled zeroed call in {raw}" + unconsumed := unconsumed.extract 0 index ++ + unconsumed.extract (index + 1) unconsumed.size + return unconsumed + unless remaining.isEmpty do + throwError "Compiled zeroed calls omit original compiler call witnesses" diff --git a/verification/aeneas/negative-control-extraction.sh b/verification/aeneas/negative-control-extraction.sh index 428776083e..f0929e8e33 100644 --- a/verification/aeneas/negative-control-extraction.sh +++ b/verification/aeneas/negative-control-extraction.sh @@ -35,10 +35,17 @@ if manifest.get('version') != 3 or manifest.get('mode') != 'verified-live': functions = {row['raw'] for row in manifest['bindings'].values() if row['kind'] == 'function'} print('storage' if 'Zerocopy.util.safety_checks.checked_bool' in functions else '') print('into-bytes' if any(row['rust'] == 'zerocopy::IntoBytes' for row in manifest['trait_laws']) else '') +image = manifest.get('type_image') +if not isinstance(image, list) or not all( + isinstance(row, dict) and isinstance(row.get('category'), str) for row in image): + raise SystemExit('Invalid verified type-image capabilities for extraction controls') +print('unemitted' if any(row['category'] == 'unemitted-uninhabited' for row in image) else '') PY ) if [[ $capabilities == *into-bytes* ]]; then run python3 -B verification/aeneas/tests/trait_const_binding_controls.py "$project" +fi +if [[ $capabilities == *unemitted* ]]; then run python3 -B verification/aeneas/tests/unemitted_type_controls.py "$project" fi if [[ $capabilities == *storage* ]]; then diff --git a/verification/aeneas/prepare.py b/verification/aeneas/prepare.py index d8a2f39655..ea77e2a56d 100644 --- a/verification/aeneas/prepare.py +++ b/verification/aeneas/prepare.py @@ -54,6 +54,47 @@ def rename_copy_fields(types, funs): return types, funs +def retain_native_models(funs): + """Elaborate native bodies with only the semantic providers they use. + + The Lean command parses the original declaration, preserves its argument + prefix, and adds an implicit provider suffix when an external operation + needs one. No function expression or Rust argument is replaced here. + Unsupported declaration forms fail in that command rather than being + silently edited by a second Lean parser. + """ + if 'public import NativeModels\n' in funs or 'native_models def' in funs: + raise ValueError('Native model extension must be applied exactly once') + if funs.count('public import Aeneas\n') != 1: + raise ValueError('Native function imports changed') + funs = funs.replace('public import Aeneas\n', + 'public import Aeneas\npublic import NativeModels\n') + starts = list(re.finditer(r'^def\s+([A-Za-z_][A-Za-z_0-9.]*)\b', funs, re.MULTILINE)) + if not starts: + raise ValueError('Native function inventory is empty') + definitions = {match[1]: funs[match.start(): + starts[index + 1].start() if index + 1 < len(starts) else len(funs)] + for index, match in enumerate(starts)} + # A missed dependency fails Lean elaboration because no model provider is + # 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'} + while True: + found = {name for name, definition in definitions.items() + if any(re.search(r'(? @@ -25,4 +33,10 @@ trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type trait_invariant into_bytes_initialized for @Zerocopy.IntoBytes with 1 type parameters where self => AeneasSpecs.RustModel.initializedRepresentation Self +trait_invariant from_zeros_valid for @Zerocopy.FromZeros with 1 type parameters where self => + AeneasSpecs.RustModel.zeroRepresentation Self + +trait_invariant from_bytes_valid for @Zerocopy.FromBytes with 1 type parameters where self => + AeneasSpecs.RustModel.completeRepresentation Self + end Zerocopy.TraitLaws diff --git a/verification/aeneas/tests/producer-controls.sh b/verification/aeneas/tests/producer-controls.sh index c1729890b6..f28eec8e4a 100755 --- a/verification/aeneas/tests/producer-controls.sh +++ b/verification/aeneas/tests/producer-controls.sh @@ -41,6 +41,20 @@ if [[ $mode != check ]]; then mkdir -p "$work/Controls" roots=aeneas_admission_controls::valid,aeneas_admission_controls::ignored,aeneas_admission_controls::before_divergence boundary=aeneas_admission_controls::util::transmute_unchecked +# Admission checks the same interface-only opacity profile for toy crates. +# The fixture defines none of these types or validator methods. +opaque_args=(--opaque "$boundary") +while IFS= read -r selector; do + [[ -z "$selector" ]] || opaque_args+=(--opaque "$selector") +done < <(python3 - "$repo" <<'PYOPAQUE' +from pathlib import Path +import sys +sys.path.insert(0, str(Path(sys.argv[1]) / 'verification/aeneas')) +import admission +print(admission.INTERFACE_ONLY_VALIDATORS) +print(*admission.INTERFACE_ONLY_TYPES, sep='\n') +PYOPAQUE +) # These are the same reviewed exclusions as the production extraction. The # toy crate defines none of those methods, but admission checks the full profile. excluded_args=() @@ -52,7 +66,7 @@ done < <(python3 -B verification/aeneas/admission.py exclude) CHARON_ADMISSION_SNAPSHOT="$work/controls.before.ullbc" \ CARGO_TARGET_DIR="$work/rust" \ "$tools_dir/charon" cargo --preset=aeneas --sysroot default \ - --mir promoted --no-dedup-serialized-ast --opaque "$boundary" \ + --mir promoted --no-dedup-serialized-ast "${opaque_args[@]}" \ "${excluded_args[@]}" \ --start-from "$roots" --dest-file "$work/controls.llbc" \ --abort-on-error --error-on-warnings -- --lib --locked --offline diff --git a/verification/aeneas/tests/std_transmute_controls.py b/verification/aeneas/tests/std_transmute_controls.py index 3b32c4eef9..c95c8bf3c7 100644 --- a/verification/aeneas/tests/std_transmute_controls.py +++ b/verification/aeneas/tests/std_transmute_controls.py @@ -40,10 +40,12 @@ def admission_controls(work, evidence): data = json.loads((work / filename).read_text()) baseline = admission.Admission(data, registry, laws) baseline.audit([owner]) + # These exact compiler paths need no rendering of unrelated opaque + # signatures, which may legitimately mention unsupported storage types. helper = next(f for f in baseline.functions.values() - if baseline.name(f['item_meta']['name']) == owner + '_native') + if f['item_meta']['name'] == [{'Ident': [part, 0]} for part in (owner + '_native').split('::')]) intrinsic = next(i for i, f in baseline.functions.items() - if baseline.name(f['item_meta']['name']) == 'core::intrinsics::transmute') + if f['item_meta']['name'] == [{'Ident': [part, 0]} for part in 'core::intrinsics::transmute'.split('::')]) calls = [node['Regular'] for node in nodes(helper['body']) if node.get('Regular', {}).get('kind', {}).get('Fun') == intrinsic] if len(calls) != 1: diff --git a/verification/aeneas/tests/test_admission.py b/verification/aeneas/tests/test_admission.py index de8ef8409f..37716030e6 100644 --- a/verification/aeneas/tests/test_admission.py +++ b/verification/aeneas/tests/test_admission.py @@ -33,6 +33,9 @@ def setUp(self): # Only unused provided methods can be excluded; any executable reference # is a compiler error, also covered by native front-end controls. self.data['translated']['options']['exclude'] = list(admission.EXCLUDED_PROVIDED_METHODS) + self.interface_opaque = [admission.INTERFACE_ONLY_VALIDATORS, + *admission.INTERFACE_ONLY_TYPES] + self.data['translated']['options']['opaque'].extend(self.interface_opaque) self.registry = json.loads((ROOT / 'verification/aeneas/external.json').read_text()) # This historical fixture selects only its original opaque helpers. # Keep its evidence bytes intact as the production registry grows; @@ -145,7 +148,7 @@ def test_supertrait_dispatch_preserves_original_clause_and_parent_application(se def test_missing_registration_is_not_an_opaque_success(self): self.registry = [r for r in self.registry if not r.get('opaque')] - self.data['translated']['options']['opaque'] = [] + self.data['translated']['options']['opaque'] = self.interface_opaque with self.assertRaisesRegex(ValueError, 'No reviewed interpretation'): self.check() @@ -154,7 +157,7 @@ def test_callee_annotations_never_exempt_unsupported_effects(self): # interpretation. Inspecting the caller must still reject its assembly. callee = self.data['translated']['fun_decls'][1] self.registry = [r for r in self.registry if not r.get('opaque')] - self.data['translated']['options']['opaque'] = [] + self.data['translated']['options']['opaque'] = self.interface_opaque callee['item_meta']['attr_info']['attributes'] = [{'DocComment': '```aeneas'}] callee['body'] = copy.deepcopy(self.data['translated']['fun_decls'][0]['body']) callee['body']['Unstructured']['body'][0]['terminator']['kind'] = {'InlineAsm': { diff --git a/verification/aeneas/tests/test_default_methods.py b/verification/aeneas/tests/test_default_methods.py new file mode 100644 index 0000000000..c3adee9b00 --- /dev/null +++ b/verification/aeneas/tests/test_default_methods.py @@ -0,0 +1,295 @@ +# Copyright 2026 The Fuchsia Authors +# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT + +"""Mutate compiler owner evidence independently of executable-body checks.""" + +import copy +from pathlib import Path +import sys +import unittest +from unittest import mock + +sys.path.insert(0, str(Path(__file__).resolve().parents[1])) +import admission +import trait_invariants as traits + + +def arguments(types=(), references=(), consts=()): + return {'regions': [], 'types': list(types), 'const_generics': list(consts), + 'trait_refs': list(references)} + + +def parameter(depth=None, index=0): + return {'TypeVar': {'Free': index} if depth is None else {'Bound': [depth, index]}} + + +def metadata(rust): + return {'name': [{'Ident': [p, 0]} for p in rust.split('::')], + 'span': {'source': rust}, 'is_local': True} + + +def binder(reference): + return {'regions': [], 'skip_binder': reference} + + +def trait_reference(types, trait=0): + return {'id': trait, 'generics': arguments(types)} + + +def default_fixture(): + params = {'types': [], 'regions': [], 'const_generics': [], 'trait_clauses': []} + function = {'def_id': 3, 'item_meta': metadata('zerocopy::Marker::make'), + 'src': {'TraitDefault': {'trait_ref': trait_reference([parameter()]), 'item_id': 2}}, + 'generics': {'types': [{'name': 'Self'}], 'trait_clauses': []}} + method = {'params': params, 'kind': {'TraitMethod': [0, 2]}, 'skip_binder': { + 'name': 'make', 'item_meta': copy.deepcopy(function['item_meta']), + 'default': {'id': 3, 'generics': arguments([parameter()])}}} + trait = {'def_id': 0, 'item_meta': metadata('zerocopy::Marker'), + 'generics': {'types': [{'name': 'Self'}]}, 'methods': [None, None, method]} + final = {'trait_decls': [trait], 'fun_decls': [function]} + before = copy.deepcopy(final) + old = before['fun_decls'][0] + old['src']['TraitDefault']['trait_ref']['generics']['types'] = [parameter(0)] + old['generics']['trait_clauses'] = [{'clause_id': 0, 'origin': 'TraitSelf', + 'trait_': binder(trait_reference([parameter(1)]))}] + before['trait_decls'][0]['methods'][2]['skip_binder']['default']['generics'] = arguments( + [parameter(1)], [{'kind': 'SelfId', + 'trait_decl_ref': binder(trait_reference([parameter(2)]))}]) + annotation = {'default_trait': 'Marker', 'generics': ['Self'], 'trait_bounds': []} + return annotation, function, final, before + + +class DefaultOwnerTests(unittest.TestCase): + def setUp(self): + self.annotation, self.function, self.final, self.before = default_fixture() + + def check(self): + return traits.check_function_bounds(self.annotation, self.function, + self.final, self.before, {'zerocopy::Marker'}) + + def test_exact_default_retains_only_the_erased_self_obligation(self): + self.assertEqual(self.check(), []) + self.assertEqual(self.annotation['erased_self_bound'], { + 'rust': 'zerocopy::Marker', 'arguments': [['parameter', 0]], + 'trait_def_id': 0, 'method_id': 2}) + + def test_missing_or_changed_source_and_compiler_owner_reject(self): + mutations = [ + lambda: self.annotation.pop('default_trait'), + lambda: self.annotation.update(default_trait='Other'), + lambda: self.function.update(src='TopLevel'), + lambda: self.before['fun_decls'][0].update(src='TopLevel'), + lambda: self.before['fun_decls'].clear(), + lambda: self.function['src']['TraitDefault'].pop('trait_ref'), + lambda: self.before['fun_decls'][0]['src']['TraitDefault'].pop('trait_ref'), + lambda: self.before['fun_decls'][0]['src']['TraitDefault'].update(item_id=1), + lambda: self.final['trait_decls'][0]['item_meta'].update(name=metadata('zerocopy::Other')['name']), + ] + for mutate in mutations: + self.setUp() + mutate() + with self.subTest(mutation=mutate), self.assertRaises(ValueError): + self.check() + + def test_top_level_string_without_default_annotation_remains_ordinary(self): + self.annotation.pop('default_trait') + self.function['src'] = 'TopLevel' + self.assertEqual(traits.default_method_owner( + self.annotation, self.function, self.final, self.before), None) + + def test_missing_or_wrong_declared_default_slot_rejects(self): + for stage in ('before', 'final'): + for mutation in ('missing', 'required', 'wrong_function', 'wrong_kind', 'wrong_name'): + self.setUp() + crate = getattr(self, stage) + slot = crate['trait_decls'][0]['methods'][2] + if mutation == 'missing': + crate['trait_decls'][0]['methods'][2] = None + elif mutation == 'required': + slot['skip_binder']['default'] = None + elif mutation == 'wrong_function': + slot['skip_binder']['default']['id'] += 1 + elif mutation == 'wrong_kind': + slot['kind']['TraitMethod'][1] = 1 + else: + slot['skip_binder']['item_meta'] = metadata('zerocopy::Marker::other') + with self.subTest(stage=stage, mutation=mutation), self.assertRaises(ValueError): + self.check() + + def test_same_id_default_slot_type_or_dictionary_mutations_reject(self): + for stage in ('before', 'final'): + for mutation in ('slot_type', 'source_extra_args', 'slot_extra_args', 'dictionary'): + self.setUp() + crate = getattr(self, stage) + slot = crate['trait_decls'][0]['methods'][2]['skip_binder']['default'] + if mutation == 'slot_type': + slot['generics']['types'] = [{'Scalar': 'Bool'}] + elif mutation == 'source_extra_args': + crate['fun_decls'][0]['src']['TraitDefault']['trait_ref']['generics']['trait_refs'] = ['SelfId'] + elif mutation == 'slot_extra_args': + slot['generics']['regions'] = ['Static'] + elif stage == 'before': + slot['generics']['trait_refs'][0]['trait_decl_ref']['skip_binder']['generics']['types'] = [{'Scalar': 'Bool'}] + else: + slot['generics']['trait_refs'] = [{'kind': 'SelfId'}] + with self.subTest(stage=stage, mutation=mutation), self.assertRaises(ValueError): + self.check() + + def test_erased_self_never_licenses_erasure_of_another_bound(self): + self.before['fun_decls'][0]['generics']['trait_clauses'].append({ + 'clause_id': 1, 'origin': 'WhereClauseOnFn', + 'trait_': binder(trait_reference([parameter(1)]))}) + with self.assertRaisesRegex(ValueError, 'lost or changed'): + self.check() + + +class DefaultAdmissionTests(unittest.TestCase): + def setUp(self): + _, function, final, before = default_fixture() + self.function = function + self.trait = final['trait_decls'][0] + self.implementation = {'def_id': 0, 'impl_trait': trait_reference([{'Scalar': 'Bool'}]), + 'generics': {'types': [], 'const_generics': [], 'trait_clauses': []}, + 'methods': [None, None, {'kind': {'TraitMethod': [0, 2]}, + 'skip_binder': {'id': 3, 'generics': arguments([{'Scalar': 'Bool'}])}}]} + self.checked = object.__new__(admission.Admission) + self.checked.before = False + self.checked.crate = final + self.checked.functions = {3: function} + self.checked.visit = mock.Mock() + + def check(self): + self.checked.audit_implementation(self.implementation, self.trait) + + def original_dictionary(self): + self.checked.before = True + self.reference = {'kind': {'TraitImpl': {'id': 0, 'generics': arguments()}}, + 'trait_decl_ref': binder(trait_reference([{'Scalar': 'Bool'}]))} + self.implementation['methods'][2]['skip_binder']['generics']['trait_refs'] = [self.reference] + + def test_shared_actual_default_is_visited_after_ownership_validation(self): + for original in (False, True): + if original: + self.original_dictionary() + self.check() + self.assertEqual(self.checked.visit.call_args_list, [mock.call(3), mock.call(3)]) + + def test_top_level_string_is_controlled_rejection(self): + self.function['src'] = 'TopLevel' + with self.assertRaisesRegex(ValueError, 'native implementation owner'): + self.check() + + def test_wrong_default_owner_slot_and_type_reject_before_visiting(self): + for mutation in ('owner', 'slot', 'type', 'function'): + self.setUp() + if mutation == 'owner': + self.function['src']['TraitDefault']['trait_ref']['id'] = 1 + elif mutation == 'slot': + self.function['src']['TraitDefault']['item_id'] = 1 + elif mutation == 'type': + self.implementation['methods'][2]['skip_binder']['generics']['types'] = [parameter()] + else: + self.trait['methods'][2]['skip_binder']['default']['id'] = 4 + with self.subTest(mutation=mutation), self.assertRaises(ValueError): + self.check() + self.checked.visit.assert_not_called() + + def test_same_dictionary_ids_with_wrong_trait_application_reject(self): + self.original_dictionary() + self.reference['trait_decl_ref']['skip_binder']['generics']['types'] = [{'Scalar': 'Char'}] + with self.assertRaisesRegex(ValueError, 'Self dictionary'): + self.check() + self.checked.visit.assert_not_called() + + def test_same_dictionary_id_with_unjustified_impl_arguments_reject(self): + for field, value in [('types', [{'Scalar': 'Bool'}]), + ('const_generics', ['invented']), ('trait_refs', ['invented'])]: + self.setUp() + self.original_dictionary() + self.reference['kind']['TraitImpl']['generics'][field] = value + with self.subTest(field=field), self.assertRaisesRegex(ValueError, 'Self dictionary'): + self.check() + self.checked.visit.assert_not_called() + + def generic_dictionary(self): + self.original_dictionary() + def length(depth, index=0): + return [{'Var': {'Bound': [depth, index]}}, traits.USIZE] + def array(depth): + return {'Array': [parameter(depth), length(depth), None]} + self.implementation['generics'] = { + 'types': [{'name': 'T'}], + 'const_generics': [{'index': 0, 'name': 'N', 'ty': traits.USIZE}], + 'trait_clauses': [{'clause_id': 7, + 'trait_': binder(trait_reference([parameter(1)]))}]} + self.implementation['impl_trait']['generics']['types'] = [array(0)] + self.implementation['methods'][2]['skip_binder']['generics']['types'] = [array(1)] + self.reference['trait_decl_ref']['skip_binder']['generics']['types'] = [array(2)] + self.reference['kind']['TraitImpl']['generics'] = arguments( + [parameter(1)], [{'kind': {'Clause': {'Bound': [1, 7]}}, + 'trait_decl_ref': binder(trait_reference([parameter(2)]))}], [length(1)]) + + def test_generic_self_dictionary_keeps_types_consts_and_bound_dictionary(self): + self.generic_dictionary() + self.check() + self.checked.visit.assert_called_once_with(3) + + def test_generic_self_dictionary_mutations_reject(self): + for mutation in ('type', 'const', 'clause_id', 'clause_type'): + self.setUp() + self.generic_dictionary() + supplied = self.reference['kind']['TraitImpl']['generics'] + if mutation == 'type': + supplied['types'][0] = parameter(1, 1) + elif mutation == 'const': + supplied['const_generics'][0][0]['Var']['Bound'][1] = 1 + elif mutation == 'clause_id': + supplied['trait_refs'][0]['kind']['Clause']['Bound'][1] = 8 + else: + supplied['trait_refs'][0]['trait_decl_ref']['skip_binder']['generics']['types'] = [{'Scalar': 'Bool'}] + with self.subTest(mutation=mutation), self.assertRaisesRegex(ValueError, 'Self dictionary'): + self.check() + self.checked.visit.assert_not_called() + + def test_missing_or_retained_self_dictionary_rejects(self): + self.checked.before = True + with self.assertRaisesRegex(ValueError, 'Self dictionary'): + self.check() + self.original_dictionary() + self.checked.before = False + with self.assertRaisesRegex(ValueError, 'retained default-method Self dictionary'): + self.check() + + +class InterfaceValidatorTests(unittest.TestCase): + def setUp(self): + function = {'def_id': 3, 'item_meta': metadata('zerocopy::validator'), + 'body': 'Opaque', 'src': {'TraitImpl': { + 'impl_ref': {'id': 0}, 'trait_ref': {'id': 0}, 'item_id': 1}}} + trait = {'def_id': 0, 'item_meta': metadata('zerocopy::TryFromBytes'), + 'methods': [None, {'skip_binder': {'name': 'is_safe'}}]} + implementation = {'def_id': 0, 'impl_trait': {'id': 0}, + 'methods': [None, {'skip_binder': {'id': 3}}]} + self.checked = object.__new__(admission.Admission) + self.checked.crate = {'trait_decls': [trait], 'trait_impls': [implementation]} + self.checked.functions = {3: function} + self.checked.visited = {} + self.checked.law_traits = set() + self.reference = {'kind': {'TraitImpl': {'id': 0}}, + 'trait_decl_ref': {'skip_binder': {'id': 0}}} + + def test_carrying_signature_only_dictionary_does_not_admit_its_execution(self): + self.checked.dictionary(self.reference) + self.assertEqual(self.checked.visited, {}) + with self.assertRaisesRegex(ValueError, 'signature-only TryFromBytes validator'): + self.checked.visit(3) + self.assertEqual(self.checked.visited, {}) + + def test_actual_trait_dispatch_to_validator_rejects(self): + with self.assertRaisesRegex(ValueError, 'signature-only TryFromBytes validator'): + self.checked.trait_call([self.reference, 1], arguments(), []) + self.assertEqual(self.checked.visited, {}) + + +if __name__ == '__main__': + unittest.main() diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py index 62bfafa929..f0264af05d 100644 --- a/verification/aeneas/tests/test_inline.py +++ b/verification/aeneas/tests/test_inline.py @@ -438,8 +438,9 @@ def test_unannotated_computed_docs_are_outside_the_annotation_language(self): with self.subTest(owner=owner, attr=attr): self.assertEqual(self.parse(attr + '\n' + owner), []) - def test_computed_docs_cannot_mix_with_literal_function_or_type_annotations(self): - type_block = '/// ```aeneas\n/// model BoxValue := Fields\\ndecode self => self\n/// ```\n' + def test_computed_docs_do_not_hide_literal_function_or_type_annotations(self): + type_block = ('/// ```aeneas\n/// model BoxValue := Fields\n' + '/// decode self => self\n/// ```\n') for owner, block in (('fn f(x: usize) {}', BLOCK), ('struct Box(usize);', type_block), ('enum Box { Empty }', type_block)): @@ -447,14 +448,61 @@ def test_computed_docs_cannot_mix_with_literal_function_or_type_annotations(self '#[doc = condVersionLink!("version", "link")]', '#[cfg_attr(any(), doc = condVersionLink!("version", "link"))]'): for docs in (attr + '\n' + block, block + attr + '\n'): - with self.subTest(owner=owner, docs=docs), self.assertRaisesRegex( - ValueError, 'Computed doc strings'): - self.parse(docs + owner) + with self.subTest(owner=owner, docs=docs): + self.assertEqual(len(self.parse(docs + owner)), 1) # Macro output supplies no source annotation; an empty extraction fails. with tempfile.TemporaryDirectory() as tmp, self.assertRaisesRegex( ValueError, 'No Aeneas specifications discovered'): fixture(Path(tmp), '#[doc = contract_docs!()]\nfn f(x: usize) {}') + def test_computed_docs_census_rejects_unowned_expanded_fences(self): + attribute = '#[doc = ordinary_docs!()]\n' + with tempfile.TemporaryDirectory() as tmp: + annotations = fixture(Path(tmp), attribute + BLOCK + 'fn f(x: usize) {}\n') + evidence = origins(annotations) + computed = {'file': 'src/util/mod.rs', 'begin': 0, + 'end': len(attribute) - 1, 'outer': True, + 'text': 'ordinary generated documentation'} + evidence['nodes'][0]['docs'].insert(0, computed) + inline.reconcile_origins(annotations, evidence) + for placement in ('same_owner', 'unannotated_owner'): + bad = copy.deepcopy(evidence) + extra = copy.deepcopy(computed) + extra['text'] = '```aeneas\nspec hidden\n ensures r => True\n```' + if placement == 'same_owner': + bad['nodes'][0]['docs'][0] = extra + else: + bad['nodes'].append({'owner': 'zerocopy::unannotated', + 'node_kind': 'function', 'docs': [extra]}) + with self.subTest(placement=placement), self.assertRaisesRegex( + ValueError, 'lacks an authored source fragment'): + inline.reconcile_origins(annotations, bad) + + def test_original_ast_requires_the_expanded_doc_census(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + source = '#[doc = ordinary_docs!()]\n' + BLOCK + 'fn f(x: usize) {}\n' + annotations = fixture(root, source) + data = llbc(annotations[RUST], source) + path = root / 'zerocopy.llbc' + path.write_text(json.dumps(data)) + (root / 'zerocopy.before.ullbc').write_text(json.dumps(data)) + with self.assertRaisesRegex(ValueError, 'mandatory native annotation origin census'): + inline.check_bindings(root, annotations, path) + + def test_provided_method_keeps_implicit_self_and_enclosing_trait(self): + source = ('mod nested { unsafe trait Marker {\n' + 'fn required();\n' + '/// ```aeneas\n/// spec make_spec\n/// ensures r => r = r\n/// ```\n' + '#[doc = ordinary_docs!()]\n' + 'fn make() -> Self where Self: Sized { panic!() }\n' + '} }') + [annotation] = self.parse(source) + self.assertEqual(annotation['syntax'], 'nested::Marker::make') + self.assertEqual(annotation['default_trait'], 'nested::Marker') + self.assertEqual(annotation['generics'], ['Self']) + self.assertEqual(annotation['trait_bounds'], [{'subject': 'Self', 'trait': 'Sized'}]) + def test_literal_docs_are_owned_and_conditional_computed_and_inner_docs_rejected(self): source = '#[doc = "```aeneas\\nspec f_spec\\n ensures r => r = x\\n```"]\nfn f(x: usize) {}' self.assertEqual(self.parse(source)[0]['spec_text'], 'spec f_spec\n ensures r => r = x\n') diff --git a/verification/aeneas/trait_invariants.py b/verification/aeneas/trait_invariants.py index 692b74ad9b..dea4c6de91 100644 --- a/verification/aeneas/trait_invariants.py +++ b/verification/aeneas/trait_invariants.py @@ -176,10 +176,108 @@ def retained_clauses(function, crate, annotated_traits): return result +def default_type_arguments(arguments, crate, bound_depth): + """Read the restricted type application without discarding other arguments.""" + if (not isinstance(arguments, dict) + or set(arguments) != {'regions', 'types', 'const_generics', 'trait_refs'} + or arguments['regions'] or arguments['const_generics']): + raise ValueError('Unsupported default-method type application') + return [simple_type(t, crate, bound_depth) for t in arguments['types']] + + +def default_trait_application(reference, crate, bound_depth): + if (not isinstance(reference, dict) or set(reference) != {'regions', 'skip_binder'} + or reference['regions']): + raise ValueError('Unsupported default-method dictionary binder') + reference = reference['skip_binder'] + if not isinstance(reference, dict) or set(reference) != {'id', 'generics'}: + raise ValueError('Missing default-method dictionary application') + arguments = reference['generics'] + if arguments['trait_refs']: + raise ValueError('Unsupported default-method nested dictionary') + return {'id': reference['id'], + 'arguments': default_type_arguments(arguments, crate, bound_depth)} + + +def default_method_owner(annotation, function, final, before): + """Recover only the enclosing trait's compiler-identified default bound. + + Charon can remove an unused Self dictionary from a provided method. The + body then remains independent of the dictionary's operations, but its + specification still needs the trait's promise. Preserve that promise as a + specification parameter; never add it to the extracted Rust input prefix. + """ + source = function.get('src') + source = source.get('TraitDefault') if isinstance(source, dict) else None + proposed = annotation.get('default_trait') + if source is None: + if proposed: + raise ValueError('Source default method lacks its compiler trait owner') + return None + if not proposed or before is None: + raise ValueError('Default method requires source and original compiler ownership') + if (not isinstance(source, dict) or set(source) != {'trait_ref', 'item_id'} + or not isinstance(source['trait_ref'], dict) + or set(source['trait_ref']) != {'id', 'generics'}): + raise ValueError('Default method lacks its compiler trait application') + originals = declarations(before, 'fun_decls') + original = originals.get(function['def_id']) + old_source = original.get('src') if original else None + old_source = old_source.get('TraitDefault') if isinstance(old_source, dict) else None + trait = declarations(final, 'trait_decls').get(source['trait_ref']['id']) + old_trait = declarations(before, 'trait_decls').get(source['trait_ref']['id']) + if (not isinstance(old_source, dict) or set(old_source) != {'trait_ref', 'item_id'} + or not isinstance(old_source['trait_ref'], dict) + or set(old_source['trait_ref']) != {'id', 'generics'} + or trait is None or old_trait is None + or original['item_meta']['name'] != function['item_meta']['name'] + or old_source['item_id'] != source['item_id'] + or old_source['trait_ref']['id'] != source['trait_ref']['id'] + or name(trait['item_meta']) != 'zerocopy::' + proposed + or old_trait['item_meta']['name'] != trait['item_meta']['name']): + raise ValueError('Default method changed its enclosing Rust trait') + source_args = source['trait_ref']['generics'] + old_args = old_source['trait_ref']['generics'] + arguments = default_type_arguments(source_args, final, 0) + old_arguments = default_type_arguments(old_args, before, 0) + if (source_args['trait_refs'] or old_args['trait_refs'] + or arguments != old_arguments + or arguments != [['parameter', i] for i in range(len(trait['generics']['types']))]): + raise ValueError('Unsupported default-method trait instantiation') + for owner, crate_function, crate in ((trait, function, final), (old_trait, original, before)): + index = source['item_id'] + methods = owner['methods'] + if not isinstance(index, int) or not 0 <= index < len(methods) or methods[index] is None: + raise ValueError('Default method lacks its original trait method slot') + method = methods[index] + declared = method['skip_binder'].get('default') + if (method['kind'] != {'TraitMethod': [owner['def_id'], index]} + or declared is None or declared.get('id') != crate_function['def_id'] + or method['skip_binder']['item_meta']['name'] != crate_function['item_meta']['name']): + raise ValueError('Default method does not implement its declared trait slot') + application = declared['generics'] + if default_type_arguments(application, crate, 1) != arguments: + raise ValueError('Default method slot changed its original type application') + self_clauses = [c for c in crate_function['generics']['trait_clauses'] + if c.get('origin') == 'TraitSelf'] + references = application['trait_refs'] + if self_clauses: + reference = unwrap(references[0]) if len(references) == 1 else {} + if (reference.get('kind') != 'SelfId' + or default_trait_application(reference['trait_decl_ref'], crate, 2) + != {'id': owner['def_id'], 'arguments': arguments}): + raise ValueError('Default method slot lost its original Self dictionary') + elif references: + raise ValueError('Default method slot gained a Self dictionary') + return {'rust': name(trait['item_meta']), 'arguments': arguments, + 'trait_def_id': trait['def_id'], 'method_id': source['item_id']} + + def check_function_bounds(annotation, function, final, before, annotated_traits): """Compare semantic applications, never pre/post clause ordinals.""" after = retained_clauses(function, final, annotated_traits) - if not after and not annotation.get('trait_bounds'): + owner = default_method_owner(annotation, function, final, before) + if not after and not annotation.get('trait_bounds') and owner is None: return [] if before is None: raise ValueError('Generic trait roots require the original admission AST') @@ -197,6 +295,16 @@ def check_function_bounds(annotation, function, final, before, annotated_traits) original_predicates = [predicate(c, before) for c in original['generics'].get('trait_clauses', [])] expected = [p for p in original_predicates if p['rust'] not in MARKERS] + if owner: + self_clauses = [predicate(c, before) for c in original['generics']['trait_clauses'] + if c.get('origin') == 'TraitSelf'] + if len(self_clauses) != 1 or key(self_clauses[0]) != key(owner): + raise ValueError('Default method lacks its original enclosing Self bound') + # Only this exact, unused Self clause may disappear. All other bounds + # must survive the normal semantic-application comparison below. + if not any(key(p) == key(owner) for p in after): + expected.remove(self_clauses[0]) + annotation['erased_self_bound'] = owner erased_laws = [p for p in original_predicates if p['rust'] in MARKERS and p['rust'] in annotated_traits] if erased_laws or Counter(map(key, expected)) != Counter(map(key, after)): @@ -209,6 +317,10 @@ def check_function_bounds(annotation, function, final, before, annotated_traits) if p['arguments'] == [['parameter', index]] and (p['rust'] == bound['trait'] or p['rust'].endswith('::' + bound['trait']))] + if not candidates and bound['trait'] in {'Sized', 'core::marker::Sized'}: + # The admitted compiler preset hides this builtin marker. Any + # same-spelled user trait still has a resolved dictionary above. + continue if len(candidates) != 1: raise ValueError('Source trait bound lacks an exact resolved compiler application') return after diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index e3d2c10f14..48f1f24774 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -30,7 +30,15 @@ use crate::pointer::cast::{CastSizedExact, CastUnsized}; #[allow(clippy::multiple_unsafe_ops_per_block)] const _: () = unsafe { unsafe_impl!( - (): Immutable, TryFromBytes, FromZeros, FromBytes, + (): Immutable, TryFromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + FromZeros, + /// ```aeneas + /// invariant_proof + /// ``` + FromBytes, /// ```aeneas /// invariant_proof /// ``` @@ -72,7 +80,15 @@ const _: () = unsafe { #[allow(clippy::multiple_unsafe_ops_per_block)] const _: () = unsafe { unsafe_impl!( - u8: Immutable, TryFromBytes, FromZeros, FromBytes, + u8: Immutable, TryFromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + FromZeros, + /// ```aeneas + /// invariant_proof + /// ``` + FromBytes, /// ```aeneas /// invariant_proof /// ``` @@ -101,7 +117,15 @@ const _: () = unsafe { IntoBytes, ); unsafe_impl!( - u32: Immutable, TryFromBytes, FromZeros, FromBytes, + u32: Immutable, TryFromBytes, + /// ```aeneas + /// invariant_proof + /// ``` + FromZeros, + /// ```aeneas + /// invariant_proof + /// ``` + FromBytes, /// ```aeneas /// invariant_proof /// ``` @@ -178,7 +202,11 @@ const _: () = unsafe { #[allow(clippy::multiple_unsafe_ops_per_block)] const _: () = unsafe { unsafe_impl!( - bool: Immutable, FromZeros, + bool: Immutable, + /// ```aeneas + /// invariant_proof + /// ``` + FromZeros, /// ```aeneas /// invariant_proof /// ``` @@ -1165,8 +1193,18 @@ const _: () = unsafe { // any safety invariants that we must fix before returning. <[T] as TryFromBytes>::is_safe(c) }); - unsafe_impl!(const N: usize, T: FromZeros => FromZeros for [T; N]); - unsafe_impl!(const N: usize, T: FromBytes => FromBytes for [T; N]); + unsafe_impl!( + /// ```aeneas + /// invariant_proof + /// ``` + const N: usize, T: FromZeros => FromZeros for [T; N] + ); + unsafe_impl!( + /// ```aeneas + /// invariant_proof + /// ``` + const N: usize, T: FromBytes => FromBytes for [T; N] + ); // SAFETY: As shown above, arrays concatenate their elements without extra // padding. `T: IntoBytes` guarantees that each element's entire storage is // initialized, so every byte of the array is initialized too, including for diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index b93b34761e..d20ae69d15 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -2049,6 +2049,14 @@ mod tests { } const _: () = { + // Challenge the concrete widths used by the byte-decoder models. These + // assertions check this compiler and target, not the Reference itself. + const_assert!(mem::size_of::<()>() == 0); + const_assert!(mem::size_of::() == 1); + const_assert!(mem::size_of::() == 1); + const_assert!(mem::size_of::() == 4); + const_assert!(mem::size_of::<[u32; 3]>() == 12); + const_assert!(mem::size_of::<[(); 3]>() == 0); const_assert!(mem::align_of::() == 1); const_assert!(mem::align_of::() == 1); assert_compiler_layout::(::LAYOUT); diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index ea6b1cbb28..1497cae629 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -3701,6 +3701,10 @@ where not(no_zerocopy_diagnostic_on_unimplemented_1_78_0), diagnostic::on_unimplemented(note = "Consider adding `#[derive(FromZeros)]` to `{Self}`") )] +/// ```aeneas +/// invariant from_zeros_valid for self => +/// AeneasSpecs.RustModel.zeroRepresentation Self +/// ``` pub unsafe trait FromZeros: TryFromBytes { // The `Self: Sized` bound makes it so that `FromZeros` is still object // safe. @@ -4287,6 +4291,10 @@ pub use zerocopy_derive::FromBytes; not(no_zerocopy_diagnostic_on_unimplemented_1_78_0), diagnostic::on_unimplemented(note = "Consider adding `#[derive(FromBytes)]` to `{Self}`") )] +/// ```aeneas +/// invariant from_bytes_valid for self => +/// AeneasSpecs.RustModel.completeRepresentation Self +/// ``` pub unsafe trait FromBytes: FromZeros { // The `Self: Sized` bound makes it so that `FromBytes` is still object // safe. diff --git a/zerocopy/tests/ui/transmute-ptr-to-usize.nightly.stderr b/zerocopy/tests/ui/transmute-ptr-to-usize.nightly.stderr index a9012843bf..c7381ae470 100644 --- a/zerocopy/tests/ui/transmute-ptr-to-usize.nightly.stderr +++ b/zerocopy/tests/ui/transmute-ptr-to-usize.nightly.stderr @@ -14,15 +14,15 @@ help: the trait `IntoBytes` is implemented for `usize` 30 | unsafe impl $trait for $ty { | ^^^^^^^^^^^^^^^^^^^^^^^^^^ | - ::: src/impls.rs:145:5 - | -145 | / unsafe_impl!( -146 | | usize: Immutable, TryFromBytes, FromZeros, FromBytes, -147 | | /// ```aeneas -148 | | /// invariant_proof -149 | | /// ``` -150 | | IntoBytes, -151 | | ); + ::: src/impls.rs:169:5 + | +169 | / unsafe_impl!( +170 | | usize: Immutable, TryFromBytes, FromZeros, FromBytes, +171 | | /// ```aeneas +172 | | /// invariant_proof +173 | | /// ``` +174 | | IntoBytes, +175 | | ); | |_____- in this macro invocation note: required by a bound in `POINTER_VALUE::transmute` --> $DIR/transmute-ptr-to-usize.rs:21:30 diff --git a/zerocopy/tests/ui/transmute-ptr-to-usize.stable.stderr b/zerocopy/tests/ui/transmute-ptr-to-usize.stable.stderr index 716d42e339..87cdad618d 100644 --- a/zerocopy/tests/ui/transmute-ptr-to-usize.stable.stderr +++ b/zerocopy/tests/ui/transmute-ptr-to-usize.stable.stderr @@ -14,15 +14,15 @@ help: the trait `IntoBytes` is implemented for `usize` 30 | unsafe impl $trait for $ty { | ^^^^^^^^^^^^^^^^^^^^^^^^^^ | - ::: src/impls.rs:145:5 + ::: src/impls.rs:169:5 | -145 | / unsafe_impl!( -146 | | usize: Immutable, TryFromBytes, FromZeros, FromBytes, -147 | | /// ```aeneas -148 | | /// invariant_proof -149 | | /// ``` -150 | | IntoBytes, -151 | | ); +169 | / unsafe_impl!( +170 | | usize: Immutable, TryFromBytes, FromZeros, FromBytes, +171 | | /// ```aeneas +172 | | /// invariant_proof +173 | | /// ``` +174 | | IntoBytes, +175 | | ); | |_____- in this macro invocation note: required by a bound in `POINTER_VALUE::transmute` --> $DIR/transmute-ptr-to-usize.rs:21:30