From cd7ad5b975a9a76487a5a5afbc6b9bc069569f49 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 15 Oct 2026 14:42:34 -0400 Subject: [PATCH] Retain every type argument in native trait laws Allow inline invariants on type-parameterized traits and type-only bounds, including conditional impls whose bound subject is a nominal wrapper. Source parsing records supported syntax and bound arity; compiler-resolved applications remain authoritative for every ordered argument. Compare original and final applications, generic bounds, and implied parent bounds. Reject unsupported argument kinds, changed arity, and associated-type constraints before assembling a law. Keep the existing native dictionary and proof-input audits. Add parser and binding regression tests for reordered, repeated, missing, and unsupported arguments. gherrit-pr-id: Gh45pumwesnecey6ydwcy7kg5ucsvnr34 Agent-authored-by: AI agent acting on joshlf's behalf --- tools/aeneas-inline/src/main.rs | 198 +++++++++++-- verification/aeneas/tests/test_admission.py | 9 +- verification/aeneas/tests/test_inline.py | 33 ++- .../aeneas/tests/test_trait_invariants.py | 264 ++++++++++++++++++ verification/aeneas/trait_invariants.py | 68 ++++- 5 files changed, 536 insertions(+), 36 deletions(-) diff --git a/tools/aeneas-inline/src/main.rs b/tools/aeneas-inline/src/main.rs index aa8e709321..5021ae7c10 100644 --- a/tools/aeneas-inline/src/main.rs +++ b/tools/aeneas-inline/src/main.rs @@ -244,6 +244,7 @@ impl Functions<'_> { let (bounds, bounds_supported) = trait_bounds_with_context( &sig.generics, if method { &self.impl_generics } else { &[] }, + false, ); supported &= bounds_supported; let mut generics = if method { self.impl_generics.clone() } else { Vec::new() }; @@ -304,23 +305,57 @@ fn declaration_start( } } +// Trait argument spellings only gate the supported syntax. Native compiler +// applications retain every identity; this is not a Rust type resolver. +fn nominal_type_argument(ty: &syn::Type) -> bool { + matches!(ty, syn::Type::Path(ty) if ty.qself.is_none() && type_argument_path(&ty.path)) +} + +fn type_argument_path(path: &syn::Path) -> bool { + let last = path.segments.len().saturating_sub(1); + path.segments.iter().enumerate().all(|(index, segment)| { + match &segment.arguments { + syn::PathArguments::None => true, + syn::PathArguments::AngleBracketed(arguments) if index == last => { + !arguments.args.is_empty() + && arguments.args.iter().all(|argument| { + matches!(argument, syn::GenericArgument::Type(ty) if nominal_type_argument(ty)) + }) + } + _ => false, + } + }) +} + // 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, &[]) + trait_bounds_with_context(generics, &[], true) } -fn trait_bounds_with_context(generics: &syn::Generics, context: &[String]) -> (Vec, bool) { - fn bound(subject: &str, bound: &syn::TypeParamBound) -> Option { +fn trait_bounds_with_context( + generics: &syn::Generics, + context: &[String], + nominal_subjects: bool, +) -> (Vec, bool) { + fn bound(subject: Option<&str>, bound: &syn::TypeParamBound) -> Option { let syn::TypeParamBound::Trait(bound) = bound else { return None }; if bound.lifetimes.is_some() || !matches!(bound.modifier, syn::TraitBoundModifier::None) - || bound.path.segments.iter().any(|s| !matches!(s.arguments, syn::PathArguments::None)) + || !type_argument_path(&bound.path) { return None; } - Some(json!({"subject": subject, - "trait": bound.path.segments.iter().map(|s| s.ident.to_string()).collect::>().join("::")})) + let mut result = json!({"subject": subject, + "trait": bound.path.segments.iter().map(|s| s.ident.to_string()).collect::>().join("::")}); + if let Some(syn::PathSegment { + arguments: syn::PathArguments::AngleBracketed(arguments), + .. + }) = bound.path.segments.last() + { + result["argument_count"] = json!(arguments.args.len()); + } + Some(result) } let mut bounds = Vec::new(); // Only usize const parameters have a supported native dictionary carrier. @@ -330,8 +365,12 @@ fn trait_bounds_with_context(generics: &syn::Generics, context: &[String]) -> (V matches!(¶meter.ty, syn::Type::Path(ty) if ty.qself.is_none() && ty.path.is_ident("usize")) }); for parameter in generics.type_params() { + supported &= parameter.default.is_none(); for predicate in ¶meter.bounds { - match bound(¶meter.ident.to_string(), predicate) { + if maybe_sized(predicate) { + continue; + } + match bound(Some(¶meter.ident.to_string()), predicate) { Some(value) => bounds.push(value), None => supported = false, } @@ -343,19 +382,32 @@ fn trait_bounds_with_context(generics: &syn::Generics, context: &[String]) -> (V supported = false; continue; }; - let syn::Type::Path(subject) = &predicate.bounded_ty else { - supported = false; - continue; - }; - let Some(subject) = subject.path.get_ident().filter(|_| subject.qself.is_none()) else { - supported = false; - continue; + let subject = match &predicate.bounded_ty { + syn::Type::Path(subject) if subject.qself.is_none() => subject, + _ => { + supported = false; + continue; + } }; + let variable = subject + .path + .get_ident() + .filter(|subject| { + generics.type_params().any(|p| p.ident == **subject) + || context.iter().any(|name| *subject == name) + }) + .map(ToString::to_string); + // Conditional wrapper impls may constrain a nominal Self such as + // UnsafeCell. Their exact compiler applications are compared by + // the impl binder, so null records no guessed source identity. supported &= predicate.lifetimes.is_none() - && (generics.type_params().any(|p| p.ident == *subject) - || context.iter().any(|name| subject == name)); + && (variable.is_some() + || (nominal_subjects && nominal_type_argument(&predicate.bounded_ty))); for predicate in &predicate.bounds { - match bound(&subject.to_string(), predicate) { + if maybe_sized(predicate) { + continue; + } + match bound(variable.as_deref(), predicate) { Some(value) => bounds.push(value), None => supported = false, } @@ -634,7 +686,9 @@ impl<'ast> Visit<'ast> for Functions<'_> { "docs": self.docs(&item.attrs), "computed_docs": computed_docs, "include_str_docs": include_str_docs, "inputs": [], "generics": item.generics.type_params().map(|p| p.ident.to_string()).collect::>(), - "supported": self.unsupported == 0 && supported && negative.is_none(), + "supported": self.unsupported == 0 && supported && negative.is_none() + && item.generics.lifetimes().next().is_none() + && type_argument_path(trait_path), "const_generics": item.generics.const_params().map(|p| p.ident.to_string()).collect::>(), "trait_path": trait_path.segments.iter().map(|s| s.ident.to_string()).collect::>().join("::"), "trait_bounds": bounds, @@ -725,6 +779,8 @@ impl<'ast> Visit<'ast> for Functions<'_> { let mut path = self.modules.clone(); path.push(item.ident.to_string()); let (computed_docs, include_str_docs) = doc_flags(&item.attrs); + let (bounds, bounds_supported) = + trait_bounds_with_context(&item.generics, &["Self".to_string()], false); self.traits.push(json!({ "path": path.join("::"), "kind": "trait", "declaration_start": self.offset(declaration_start(&item.vis, @@ -732,10 +788,12 @@ impl<'ast> Visit<'ast> for Functions<'_> { "start": self.offset(item.trait_token.span.start()), "close": self.offset(item.span().end()), "inputs": [], "docs": self.docs(&item.attrs), "computed_docs": computed_docs, - "include_str_docs": include_str_docs, + "include_str_docs": include_str_docs, "trait_bounds": bounds, "generics": std::iter::once("Self".to_string()).chain(item.generics.type_params().map(|p| p.ident.to_string())).collect::>(), - "supported": self.unsupported == 0 && item.generics.params.is_empty() - && item.generics.where_clause.is_none(), + "supported": self.unsupported == 0 + && item.generics.lifetimes().next().is_none() + && item.generics.const_params().next().is_none() + && bounds_supported, })); // A provided method owns a real function body. Its implicit Self type // and enclosing trait come from this item, not from a guessed path. @@ -942,6 +1000,104 @@ mod tests { } } + #[test] + fn parameterized_traits_keep_type_parameters_and_optional_sized() { + let value = inspect("pub unsafe trait TransmuteFrom {}").unwrap(); + assert_eq!(value["traits"][0]["supported"], true); + assert_eq!(value["traits"][0]["generics"], json!(["Self", "Src", "SV", "DV"])); + let bounded = + inspect("pub unsafe trait TransmuteFrom {}") + .unwrap(); + assert_eq!(bounded["traits"][0]["supported"], true); + assert_eq!( + bounded["traits"][0]["trait_bounds"], + json!([ + {"subject": "SV", "trait": "Validity"}, + {"subject": "DV", "trait": "Validity"}, + ]) + ); + let conditional = inspect("trait Marker where Self: Other, T: Validity {}").unwrap(); + assert_eq!(conditional["traits"][0]["supported"], true); + assert_eq!( + conditional["traits"][0]["trait_bounds"], + json!([ + {"subject": "Self", "trait": "Other", "argument_count": 1}, + {"subject": "T", "trait": "Validity"}, + ]) + ); + for source in [ + "trait Marker<'a, T> {}", + "trait Marker {}", + "trait Marker {}", + "trait Marker {}", + "trait Marker where Cell: Other {}", + ] { + assert_eq!(inspect(source).unwrap()["traits"][0]["supported"], false, "{source}"); + } + } + + #[test] + fn parameterized_bounds_record_arity_without_resolving_argument_types() { + let value = inspect( + "fn f() + where Dst: crate::TransmuteFrom + Marker {}", + ) + .unwrap(); + assert_eq!(value["functions"][0]["supported"], true); + assert_eq!( + value["functions"][0]["trait_bounds"], + json!([ + {"subject": "Dst", "trait": "crate::TransmuteFrom", "argument_count": 3}, + {"subject": "Dst", "trait": "Marker"}, + ]) + ); + let sized = inspect("fn f() where T: ?Sized {}").unwrap(); + assert_eq!(sized["functions"][0]["supported"], true); + assert_eq!(sized["functions"][0]["trait_bounds"], json!([])); + for bound in [ + "Trait<'static>", + "Trait", + "Trait", + "Trait<3>", + "Trait<&'static u8>", + "Trait<[T; 3]>", + "Trait fn(&'a T)>", + "for<'a> Trait", + "?Other", + ] { + let source = format!("fn f() where T: {bound} {{}}"); + assert_eq!(inspect(&source).unwrap()["functions"][0]["supported"], false, "{bound}"); + } + } + + #[test] + fn only_impl_markers_accept_nominal_bound_subjects() { + let value = inspect( + "unsafe impl TransmuteFrom, Safe, Safe> for UnsafeCell + where T: TransmuteFrom, Safe, Safe>, + UnsafeCell: TransmuteFrom {}", + ) + .unwrap(); + assert_eq!(value["trait_impls"][0]["supported"], true); + assert_eq!( + value["trait_impls"][0]["trait_bounds"], + json!([ + {"subject": "T", "trait": "TransmuteFrom", "argument_count": 3}, + {"subject": null, "trait": "TransmuteFrom", "argument_count": 3}, + ]) + ); + for source in [ + "fn f() where UnsafeCell: Trait {}", + "unsafe impl<'a, T> Trait for S {}", + "unsafe impl Trait for S {}", + "unsafe impl Trait<'static> for S {}", + ] { + let report = inspect(source).unwrap(); + let group = if source.starts_with("fn ") { "functions" } else { "trait_impls" }; + assert_eq!(report[group][0]["supported"], false, "{source}"); + } + } + #[test] fn provided_method_retains_enclosing_self_in_where_clauses() { let value = inspect( diff --git a/verification/aeneas/tests/test_admission.py b/verification/aeneas/tests/test_admission.py index 07a9d680a3..90db01c45b 100644 --- a/verification/aeneas/tests/test_admission.py +++ b/verification/aeneas/tests/test_admission.py @@ -84,7 +84,11 @@ def abstract_trait_fixture(self): params = {'types': [], 'regions': [], 'const_generics': [], 'trait_clauses': []} signature = {'abi': 'Rust', 'is_variadic': False, 'is_unsafe': False, 'inputs': [], 'output': {'Untagged': {'Scalar': 'Bool'}}} - trait = {'def_id': 0, 'item_meta': {'name': [{'Ident': ['zerocopy', 0]}, + trait_parameters = {'types': [{'index': 0, 'name': 'Self', 'variance': 'Unknown'}], + 'regions': [], 'const_generics': [], 'trait_clauses': [], + 'regions_outlive': [], 'types_outlive': [], 'trait_type_constraints': []} + trait = {'def_id': 0, 'generics': trait_parameters, + 'item_meta': {'name': [{'Ident': ['zerocopy', 0]}, {'Ident': ['Codec', 0]}]}, 'methods': [{'params': params, 'kind': {'TraitMethod': [0, 0]}, 'skip_binder': {'signature': signature, 'item_meta': {'has_errors': False, 'is_extern': False}}}]} @@ -137,7 +141,8 @@ def test_supertrait_dispatch_preserves_original_clause_and_parent_application(se checked.current_function['generics']['trait_clauses'][0]['trait_'] = child_reference['trait_decl_ref'] parent_clause = {'clause_id': 6, 'trait_': copy.deepcopy(reference['trait_decl_ref'])} parent_clause['trait_']['skip_binder']['generics']['types'] = [{'TypeVar': {'Bound': [1, 0]}}] - child = {'def_id': 1, 'methods': [], 'item_meta': {'name': [{'Ident': ['zerocopy', 0]}, + child = {'def_id': 1, 'generics': copy.deepcopy(trait['generics']), + 'methods': [], 'item_meta': {'name': [{'Ident': ['zerocopy', 0]}, {'Ident': ['Child', 0]}]}, 'implied_clauses': [parent_clause]} checked.crate['trait_decls'].append(child) reference['kind'] = {'ParentClause': [child_reference, 6]} diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py index f0264af05d..d3807a4e63 100644 --- a/verification/aeneas/tests/test_inline.py +++ b/verification/aeneas/tests/test_inline.py @@ -95,6 +95,31 @@ def setUp(self): def parse(self, source): return inline.parse_file(source, syntax(source)) + def test_parameterized_trait_declaration_retains_marker_bound_census(self): + source = ('/// ```aeneas\n/// invariant law for self => True\n/// ```\n' + 'pub unsafe trait TransmuteFrom {}') + [annotation] = self.parse(source) + self.assertEqual(annotation['generics'], ['Self', 'Src', 'SV', 'DV']) + self.assertEqual(annotation['trait_bounds'], [ + {'subject': 'SV', 'trait': 'Validity'}, + {'subject': 'DV', 'trait': 'Validity'}]) + + def test_parameterized_annotation_syntax_rejects_unsupported_generic_forms(self): + law = '/// ```aeneas\n/// invariant law for self => True\n/// ```\n' + marker = '/// ```aeneas\n/// invariant_proof\n/// ```\n' + for declaration in [ + "trait Marker<'a, T> {}", 'trait Marker {}', + 'trait Marker {}', + 'trait Marker where T: Other {}', + "trait Marker where T: for<'a> Other {}", + 'impl Marker for T where T: Other {}', + "impl Marker for T where T: Other<'static> {}", + "impl Marker for T where T: for<'a> Other {}"]: + prefix = law if declaration.startswith('trait ') else marker + with self.subTest(declaration=declaration), self.assertRaisesRegex( + ValueError, 'unsupported Rust owner'): + self.parse(prefix + declaration) + def test_unemitted_native_nominal_requires_exact_unannotated_empty_owner(self): rust = 'zerocopy::private::Never' source = {'file': 'zerocopy/src/private.rs', 'syntax': 'Never', @@ -371,8 +396,12 @@ def test_generic_trait_bound_source_evidence(self): declaration = self.parse(BLOCK + signature)[0] self.assertEqual(declaration['generics'], ['T']) self.assertEqual(declaration['trait_bounds'][0]['subject'], 'T') - for signature in ('fn f>(x: usize) {}', - 'fn f(x: usize) {}', + parameterized = self.parse(BLOCK + 'fn f>(x: usize) {}')[0] + self.assertEqual(parameterized['trait_bounds'], + [{'subject': 'T', 'trait': 'Marker', 'argument_count': 1}]) + optional = self.parse(BLOCK + 'fn f(x: usize) {}')[0] + self.assertEqual(optional['trait_bounds'], []) + for signature in ('fn f(x: usize) {}', 'fn f(x: usize) where T::Assoc: Marker {}'): with self.assertRaisesRegex(ValueError, 'unsupported Rust owner'): self.parse(BLOCK + signature) diff --git a/verification/aeneas/tests/test_trait_invariants.py b/verification/aeneas/tests/test_trait_invariants.py index 95cd36b74f..cd46983448 100644 --- a/verification/aeneas/tests/test_trait_invariants.py +++ b/verification/aeneas/tests/test_trait_invariants.py @@ -296,6 +296,270 @@ def test_const_expressions_and_non_usize_lengths_fail_closed(self): with self.assertRaises(ValueError): traits.simple_const(value) + def parameterized_function(self): + self.trait['item_meta'] = meta('zerocopy::TransmuteFrom') + self.trait['generics'] = generics(names=('Self', 'Src', 'SV', 'DV')) + self.function['generics'] = generics([clause(7)], names=('Src', 'Dst', 'SV', 'DV')) + self.function['generics']['trait_clauses'][0]['trait_']['skip_binder']['generics'] = args( + [{'TypeVar': {'Free': i}} for i in (1, 0, 2, 3)]) + self.before = copy.deepcopy(self.final) + original = self.before['fun_decls'][0]['generics']['trait_clauses'][0] + original['clause_id'] = 2 + original['trait_']['skip_binder']['generics'] = args( + [{'TypeVar': {'Bound': [1, i]}} for i in (1, 0, 2, 3)]) + self.annotation = {'generics': ['Src', 'Dst', 'SV', 'DV'], + 'trait_bounds': [{'subject': 'Dst', 'trait': 'TransmuteFrom', 'argument_count': 3}]} + + def check(): + return traits.check_function_bounds(self.annotation, self.function, + self.final, self.before, {'zerocopy::TransmuteFrom'}) + return check + + def test_parameterized_bound_matches_original_self_and_arity(self): + check = self.parameterized_function() + self.assertEqual(check()[0]['arguments'], + [['parameter', i] for i in (1, 0, 2, 3)]) + bound = self.annotation['trait_bounds'][0] + for key, wrong in [('subject', 'Src'), ('subject', None), + ('argument_count', 2), ('argument_count', 4), + ('argument_count', -1), ('argument_count', True)]: + saved = bound[key] + bound[key] = wrong + with self.subTest(key=key, value=wrong), self.assertRaises(ValueError): + check() + bound[key] = saved + bound.pop('argument_count') + with self.assertRaisesRegex(ValueError, 'exact resolved compiler application'): + check() + + def test_parameterized_bound_keeps_every_argument_identity_and_order(self): + check = self.parameterized_function() + application = self.function['generics']['trait_clauses'][0]['trait_']['skip_binder'] + original = copy.deepcopy(application['generics']['types']) + for left in range(4): + for right in range(left + 1, 4): + changed = copy.deepcopy(original) + changed[left], changed[right] = changed[right], changed[left] + application['generics']['types'] = changed + with self.subTest(swap=(left, right)), self.assertRaisesRegex( + ValueError, 'lost or changed a required source bound'): + check() + for changed in [original[:-1], original + original[-1:], + original[:-1] + original[:1]]: + application['generics']['types'] = changed + with self.assertRaises(ValueError): + check() + application['generics']['types'] = original + self.function['generics']['trait_clauses'].append(copy.deepcopy( + self.function['generics']['trait_clauses'][0])) + with self.assertRaisesRegex(ValueError, 'lost or changed a required source bound'): + check() + + def test_parameterized_trait_declaration_preserves_generic_and_implied_bounds(self): + self.parameterized_function() + validity = {'def_id': 3, 'item_meta': meta('zerocopy::Validity'), + 'generics': generics(names=('Self',)), 'types': []} + parent = {'def_id': 4, 'item_meta': meta('zerocopy::Parent'), + 'generics': generics(names=('Self',)), 'types': []} + for crate in (self.final, self.before): + crate['trait_decls'].extend(copy.deepcopy([validity, parent])) + for index in (2, 3): + bound = clause(index, {'Free': index}) + bound['trait_']['skip_binder']['id'] = 3 + crate['trait_decls'][0]['generics']['trait_clauses'].append(bound) + implied = clause(0) + implied['trait_']['skip_binder']['id'] = 4 + crate['trait_decls'][0]['implied_clauses'] = [implied] + annotations = inline.Annotations() + annotations['zerocopy::TransmuteFrom'] = { + 'kind': 'trait', 'rust': 'zerocopy::TransmuteFrom', + 'generics': ['Self', 'Src', 'SV', 'DV'], + 'trait_bounds': [{'subject': 'SV', 'trait': 'Validity'}, + {'subject': 'DV', 'trait': 'Validity'}, + {'subject': 'Self', 'trait': 'Parent'}], + 'theorem': 'transmute_from', 'predicate': 'True'} + location = {'file': 'src/lib.rs', 'begin_line': 1, 'end_line': 4} + native = {'crate': 'zerocopy', 'charon_version': '0.1.276', + 'aeneas_version': 'nightly-2026.10.01-ca282ec+nominal-tuple-structs.1', + 'trait_decls': [{'def_id': ident, 'lean_name': 'Zerocopy.' + label, + 'rust_name': 'zerocopy::' + label, 'is_local': True, 'source': location} + for ident, label in [(0, 'TransmuteFrom'), (3, 'Validity'), (4, 'Parent')]], + 'trait_impls': []} + with tempfile.TemporaryDirectory() as tmp: + work = Path(tmp) + (work / 'Zerocopy').mkdir() + (work / 'Zerocopy/translation.json').write_text(json.dumps(native)) + + def bind(): + return traits.bind_laws(annotations, work, self.final, self.before) + + self.assertEqual(bind()[0][0]['generic_count'], 4) + # Actual Charon output puts both parameter bounds in implied_clauses. + for crate in (self.final, self.before): + declaration = crate['trait_decls'][0] + declaration['implied_clauses'].extend(declaration['generics']['trait_clauses']) + declaration['generics']['trait_clauses'] = [] + self.assertEqual(bind()[0][0]['generic_count'], 4) + for crate in (self.final, self.before): + declaration = crate['trait_decls'][0] + declaration['generics']['trait_clauses'] = declaration['implied_clauses'][1:] + declaration['implied_clauses'] = declaration['implied_clauses'][:1] + parameters = self.trait['generics']['types'] + parameters[2], parameters[3] = parameters[3], parameters[2] + with self.assertRaisesRegex(ValueError, 'original type-only parameters'): + bind() + parameters[2], parameters[3] = parameters[3], parameters[2] + # Clause order and ordinals may change; semantic identities may not. + self.trait['generics']['trait_clauses'].reverse() + self.assertEqual(bind()[0][0]['generic_count'], 4) + for field in ('trait_clauses', 'implied_clauses'): + container = self.trait['generics'] if field == 'trait_clauses' else self.trait + saved = copy.deepcopy(container[field]) + container[field] = [] + with self.subTest(field=field), self.assertRaisesRegex(ValueError, 'dictionary law'): + bind() + container[field] = saved + bound = self.trait['generics']['trait_clauses'][0] + application = bound['trait_']['skip_binder']['generics'] + application['types'][0] = {'TypeVar': {'Free': 1}} + with self.assertRaisesRegex(ValueError, 'generic normalization'): + bind() + application['types'][0] = {'TypeVar': {'Free': 3}} + for crate in (self.final, self.before): + crate['trait_decls'][0]['generics']['trait_clauses'] = [] + with self.assertRaisesRegex(ValueError, 'exact resolved compiler application'): + bind() + + def test_parameterized_function_cannot_omit_either_stage_bound(self): + for crate_name in ('final', 'before'): + check = self.parameterized_function() + getattr(self, crate_name)['fun_decls'][0]['generics']['trait_clauses'] = [] + with self.subTest(stage=crate_name), self.assertRaisesRegex( + ValueError, 'lost or changed a required source bound'): + check() + + def test_parameterized_impl_preserves_the_complete_native_application(self): + self.parameterized_function() + annotations = inline.Annotations() + annotations['zerocopy::TransmuteFrom'] = { + 'kind': 'trait', 'rust': 'zerocopy::TransmuteFrom', + 'generics': ['Self', 'Src', 'SV', 'DV'], + 'theorem': 'transmute_from', 'predicate': 'True'} + implementation = {'def_id': 2, 'item_meta': meta('zerocopy::TransmuteImpl'), + 'impl_trait': {'id': 0, 'generics': args([ + {'TypeVar': {'Free': i}} for i in (1, 0, 2, 3)])}, + 'generics': generics(names=('Src', 'Dst', 'SV', 'DV'))} + self.final['trait_impls'] = [implementation] + self.before['trait_impls'] = [copy.deepcopy(implementation)] + location = {'file': 'src/lib.rs', 'begin_line': 1, 'end_line': 4} + native = {'crate': 'zerocopy', 'charon_version': '0.1.276', + 'aeneas_version': 'nightly-2026.10.01-ca282ec+nominal-tuple-structs.1', + 'trait_decls': [{'def_id': 0, 'lean_name': 'Zerocopy.TransmuteFrom', + 'rust_name': 'zerocopy::TransmuteFrom', 'is_local': True, 'source': location}], + 'trait_impls': [{'def_id': 2, 'lean_name': 'Zerocopy.TransmuteImpl', + 'impl_trait_def_id': 0, 'impl_trait_rust_name': 'zerocopy::TransmuteFrom', + 'is_local': True, 'source': location}]} + with tempfile.TemporaryDirectory() as tmp: + work = Path(tmp) + (work / 'Zerocopy').mkdir() + (work / 'Zerocopy/translation.json').write_text(json.dumps(native)) + + def bind(): + return traits.bind_laws(annotations, work, self.final, self.before) + + self.assertEqual(bind()[1][0]['rust_type'], + [['parameter', i] for i in (1, 0, 2, 3)]) + for crate_name in ('final', 'before'): + application = getattr(self, crate_name)['trait_impls'][0]['impl_trait']['generics'] + for field in ('regions', 'const_generics', 'trait_refs'): + application[field] = [{}] + try: + with self.subTest(stage=crate_name, field=field), self.assertRaisesRegex( + ValueError, 'Unsupported dependent trait-law arguments'): + bind() + finally: + application[field] = [] + original = copy.deepcopy(application['types']) + for left in range(4): + for right in range(left + 1, 4): + changed = copy.deepcopy(original) + changed[left], changed[right] = changed[right], changed[left] + application['types'] = changed + with self.subTest(stage=crate_name, swap=(left, right)), self.assertRaisesRegex( + ValueError, 'lost its original Rust type application'): + bind() + for changed in (original[:-1], original + original[-1:], + original[:-1] + original[:1]): + application['types'] = changed + with self.subTest(stage=crate_name, types=changed), self.assertRaises(ValueError): + bind() + application['types'] = original + for crate in (self.final, self.before): + crate['type_decls'] = [ + {'def_id': 5, 'item_meta': meta('zerocopy::Cell')}, + {'def_id': 6, 'item_meta': meta('zerocopy::UnsafeCell')}] + nominal_bound = clause() + nominal_bound['trait_']['skip_binder']['generics'] = args([ + {'Adt': {'id': 5, 'builtin': None, + 'generics': args([{'TypeVar': {'Free': 0}}])}}, + *[{'TypeVar': {'Free': i}} for i in (0, 2, 3)]]) + crate['trait_impls'][0]['generics']['trait_clauses'] = [nominal_bound] + self.assertEqual(bind()[1][0]['dictionary_count'], 1) + bound = implementation['generics']['trait_clauses'][0] + subject = bound['trait_']['skip_binder']['generics']['types'][0] + subject['Adt']['id'] = 6 + with self.assertRaisesRegex(ValueError, 'changed its required dictionaries'): + bind() + subject['Adt']['id'] = 5 + implementation['generics']['trait_clauses'] = [] + with self.assertRaisesRegex(ValueError, 'changed its required dictionaries'): + bind() + self.before['trait_impls'][0]['generics']['trait_clauses'] = [] + # Comparing both stages is insufficient if both have discarded a + # required formal argument. Native declaration arity also matters. + for crate in (self.final, self.before): + crate['trait_impls'][0]['impl_trait']['generics']['types'].pop() + with self.assertRaisesRegex(ValueError, 'declared type arity'): + bind() + + def test_parameterized_bound_keeps_nominal_argument_identity(self): + check = self.parameterized_function() + for crate in (self.final, self.before): + crate['type_decls'] = [{'def_id': 5, 'item_meta': meta('zerocopy::Cell')}, + {'def_id': 6, 'item_meta': meta('zerocopy::UnsafeCell')}] + app = crate['fun_decls'][0]['generics']['trait_clauses'][0]['trait_']['skip_binder'] + app['generics']['types'][1] = {'Adt': {'id': 5, 'builtin': None, + 'generics': args([app['generics']['types'][1]])}} + self.assertEqual(check()[0]['arguments'][1], + ['nominal', 'zerocopy::Cell', [['parameter', 0]]]) + app = self.function['generics']['trait_clauses'][0]['trait_']['skip_binder'] + app['generics']['types'][1]['Adt']['id'] = 6 + with self.assertRaisesRegex(ValueError, 'lost or changed a required source bound'): + check() + + def test_parameterized_bound_rejects_native_equalities_and_lifetimes(self): + for field in ('regions', 'trait_type_constraints'): + check = self.parameterized_function() + for crate in (self.final, self.before): + crate['trait_decls'][0]['generics'][field] = [{}] + with self.subTest(owner='trait', field=field), self.assertRaises(ValueError): + check() + for crate_name in ('final', 'before'): + check = self.parameterized_function() + crate = getattr(self, crate_name) + crate['fun_decls'][0]['generics']['trait_type_constraints'] = [{}] + with self.subTest(owner=crate_name), self.assertRaisesRegex(ValueError, 'constraints'): + check() + for binder in (True, False): + check = self.parameterized_function() + clause_ref = self.function['generics']['trait_clauses'][0]['trait_'] + if binder: + clause_ref['regions'] = [{}] + else: + clause_ref['skip_binder']['generics']['regions'] = ['Static'] + with self.subTest(binder=binder), self.assertRaises(ValueError): + check() + def test_supertrait_graph_keeps_native_parent_identities(self): parent = {'def_id': 3, 'item_meta': meta('zerocopy::Parent'), 'generics': generics(names=('Self',)), 'types': []} diff --git a/verification/aeneas/trait_invariants.py b/verification/aeneas/trait_invariants.py index aed405cca8..8f1d0d7d75 100644 --- a/verification/aeneas/trait_invariants.py +++ b/verification/aeneas/trait_invariants.py @@ -142,6 +142,18 @@ def simple_type(value, crate, bound_depth=0): raise ValueError('Trait-law carrier erasure or associated types are unsupported') +def type_only_trait_arguments(arguments, arity): + """Reject discarded argument kinds before comparing compiler applications.""" + if (not isinstance(arguments, dict) + or set(arguments) != {'regions', 'types', 'const_generics', 'trait_refs'} + or not isinstance(arguments['types'], list) + or any(arguments[k] for k in ('regions', 'const_generics', 'trait_refs'))): + raise ValueError('Unsupported dependent trait-law arguments') + if len(arguments['types']) != arity: + raise ValueError('Trait-law application changed its declared type arity') + return arguments['types'] + + def predicate(clause, crate): bound = clause.get('trait_', clause.get('trait')) if not isinstance(bound, dict) or bound.get('regions'): @@ -150,13 +162,15 @@ def predicate(clause, crate): trait = declarations(crate, 'trait_decls').get(reference['id']) if trait is None: raise ValueError('Trait clause lacks its compiler declaration') - args = reference['generics'] - if any(args.get(k) for k in ('regions', 'const_generics', 'trait_refs')): + if (trait['generics'].get('regions') + or trait['generics'].get('const_generics') + or trait['generics'].get('trait_type_constraints')): raise ValueError('Unsupported dependent trait-law arguments') + types = type_only_trait_arguments(reference['generics'], len(trait['generics']['types'])) return {'rust': name(trait['item_meta']), # The original AST has an item binder outside the (empty) # RegionBinder. unbind_item_vars makes these Free in final LLBC. - 'arguments': [simple_type(t, crate, 1) for t in args['types']], + 'arguments': [simple_type(t, crate, 1) for t in types], 'clause_id': clause['clause_id']} @@ -275,6 +289,8 @@ def default_method_owner(annotation, function, final, before): def check_function_bounds(annotation, function, final, before, annotated_traits): """Compare semantic applications, never pre/post clause ordinals.""" + if function['generics'].get('trait_type_constraints'): + raise ValueError('Associated-type constraints in trait roots are unsupported') after = retained_clauses(function, final, annotated_traits) owner = default_method_owner(annotation, function, final, before) if not after and not annotation.get('trait_bounds') and owner is None: @@ -286,6 +302,8 @@ def check_function_bounds(annotation, function, final, before, annotated_traits) if len(originals) != 1: raise ValueError('Generic trait root lacks an unambiguous original compiler owner') original = originals[0] + if original['generics'].get('trait_type_constraints'): + raise ValueError('Associated-type constraints in original trait roots are unsupported') if original['item_meta']['span'] != function['item_meta']['span']: raise ValueError('Generic trait root changed its original compiler source owner') original_names = [p['name'] for p in original['generics']['types']] @@ -309,21 +327,33 @@ def check_function_bounds(annotation, function, final, before, annotated_traits) if p['rust'] in MARKERS and p['rust'] in annotated_traits] if erased_laws or Counter(map(key, expected)) != Counter(map(key, after)): raise ValueError('Trait normalization lost or changed a required source bound') + check_source_bounds(annotation, original_predicates) + return after + + +def check_source_bounds(annotation, original_predicates): + """Resolve source bound subjects and arities through original native clauses.""" # Source syntax is only a proposed location/name. The resolved pre-AST # applications must explain every written bound on an original type variable. for bound in annotation.get('trait_bounds', []): + if bound['subject'] not in annotation['generics']: + raise ValueError('Source trait bound requires an original type-variable subject') index = annotation['generics'].index(bound['subject']) + argument_count = bound.get('argument_count', 0) + if type(argument_count) is not int or argument_count < 0: + raise ValueError('Source trait bound has an invalid type argument count') candidates = [p for p in original_predicates - if p['arguments'] == [['parameter', index]] + if len(p['arguments']) == argument_count + 1 + and p['arguments'][0] == ['parameter', index] and (p['rust'] == bound['trait'] or p['rust'].endswith('::' + bound['trait']))] - if not candidates and bound['trait'] in {'Sized', 'core::marker::Sized'}: + if (not candidates and argument_count == 0 + 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 def read_translation(work, final): @@ -387,14 +417,24 @@ def bind_laws(annotations, work, final, before): annotation = trait_annotations[rust] if ident not in native_traits: raise ValueError(f'Annotated trait lacks a native dictionary: {rust}') - if [p['name'] for p in trait['generics']['types']] != annotation['generics']: - raise ValueError('Trait invariant associated-type lifting is unsupported') + if (trait['generics'].get('regions') or trait['generics'].get('const_generics') + or trait['generics'].get('trait_type_constraints') or trait.get('types') + or [p['name'] for p in trait['generics']['types']] != annotation['generics']): + raise ValueError('Trait invariant requires original type-only parameters without associated types') original = declarations(before, 'trait_decls').get(ident) if before else None if (original is None or original['item_meta']['name'] != trait['item_meta']['name'] - or original.get('types') or original['generics'].get('trait_type_constraints')): + or original.get('types') or original['generics'].get('trait_type_constraints') + or original['generics'].get('regions') or original['generics'].get('const_generics') + or [p['name'] for p in original['generics']['types']] != annotation['generics']): raise ValueError('Trait invariant requires an original trait without associated types') + original_bounds = retained_clauses(original, before, trait_annotations) + final_bounds = retained_clauses(trait, final, trait_annotations) + if Counter(map(key, original_bounds)) != Counter(map(key, final_bounds)): + raise ValueError('Trait generic normalization lost or changed a required dictionary law') original_parents = [predicate(c, before) for c in original.get('implied_clauses', [])] final_parents = [predicate(c, final) for c in trait.get('implied_clauses', [])] + check_source_bounds(annotation, [predicate(c, before) + for c in original['generics'].get('trait_clauses', [])] + original_parents) if (any(p['rust'] in MARKERS and p['rust'] in trait_annotations for p in original_parents) or Counter(key(p) for p in original_parents if p['rust'] not in MARKERS) != Counter(key(p) for p in final_parents if p['rust'] not in MARKERS)): @@ -424,6 +464,8 @@ def bind_laws(annotations, work, final, before): or name(declarations(before, 'trait_decls')[original['impl_trait']['id']]['item_meta']) != law['rust']): raise ValueError('Trait implementation lacks its original compiler owner') + if original['generics'].get('regions') or original['generics'].get('trait_type_constraints'): + raise ValueError('Unsupported original generic trait-law implementation') const_parameters = usize_const_parameters(generics) if const_parameters != usize_const_parameters(original['generics']): raise ValueError('Trait implementation normalization changed its original const parameters') @@ -432,9 +474,13 @@ def bind_laws(annotations, work, final, before): or Counter(map(key, retained_clauses(original, before, trait_annotations))) != Counter(map(key, retained_clauses(implementation, final, trait_annotations)))): raise ValueError('Trait implementation normalization changed its required dictionaries') - types = [simple_type(t, final) for t in implementation['impl_trait']['generics']['types']] + arguments = type_only_trait_arguments( + implementation['impl_trait']['generics'], law['generic_count']) + original_arguments = type_only_trait_arguments( + original['impl_trait']['generics'], law['generic_count']) + types = [simple_type(t, final) for t in arguments] original_types = [simple_type(lift_original_type(t, before, final), before) - for t in original['impl_trait']['generics']['types']] + for t in original_arguments] check_application_parameters(types, len(generics['types']), len(const_parameters)) check_application_parameters(original_types, len(original['generics']['types']), len(const_parameters)) if types != original_types: