From b84003eb6d1e5d15dd4d9a91f18fb3105061b877 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 03:17:40 -0400 Subject: [PATCH] Support generic inline proofs and closed method coverage Resolve annotations on parameterized inherent impls and generic methods against Charon's exact Self identity. Optional closed impl scopes reject every unregistered method, including inactive cfg alternatives. Add bijective named proof slots so support lemmas can sit between registered proofs. Keep generated constants, dependencies, and loop helpers in independently compared scaffolding. Follow helper declarations throughout the proof namespace when checking declared theorem dependencies. gherrit-pr-id: Ggyxdemsrutwypf7tui4otq6shrm2ivah Validation: 25 Python tests and 3 Rust annotation-tool tests; full final golden/live replay and dependency failure controls. --- tools/aeneas-inline/src/main.rs | 64 +++++++++++----- verification/aeneas/inline.py | 93 +++++++++++++++++++----- verification/aeneas/lean/Check.lean | 3 +- verification/aeneas/tests/test_inline.py | 64 ++++++++++++++-- 4 files changed, 183 insertions(+), 41 deletions(-) diff --git a/tools/aeneas-inline/src/main.rs b/tools/aeneas-inline/src/main.rs index b74639215d..29530f3572 100644 --- a/tools/aeneas-inline/src/main.rs +++ b/tools/aeneas-inline/src/main.rs @@ -18,6 +18,8 @@ struct Functions<'a> { source: &'a str, modules: Vec, unsupported: usize, + impl_type: Option, + inherent: bool, functions: Vec, } @@ -32,7 +34,7 @@ impl Functions<'_> { .map_or(self.source[start..].len(), |(byte, _)| byte) } - fn function(&mut self, ident: &syn::Ident, block: &syn::Block) { + fn function(&mut self, ident: &syn::Ident, block: &syn::Block, method: bool) { let open = self.offset(block.brace_token.span.open().start()); assert_eq!(&self.source[open..open + 1], "{", "Invalid function brace span"); let mut path = self.modules.clone(); @@ -41,6 +43,7 @@ impl Functions<'_> { "path": path.join("::"), "open": open, "close": self.offset(block.brace_token.span.close().end()), "supported": self.unsupported == 0, + "method": method, "impl_type": self.impl_type, "inherent": self.inherent, })); } } @@ -53,7 +56,7 @@ impl<'ast> Visit<'ast> for Functions<'_> { } fn visit_item_fn(&mut self, item: &'ast syn::ItemFn) { - self.function(&item.sig.ident, &item.block); + self.function(&item.sig.ident, &item.block, false); // Never attribute nested functions to the enclosing function or method. self.unsupported += 1; visit::visit_item_fn(self, item); @@ -61,16 +64,36 @@ impl<'ast> Visit<'ast> for Functions<'_> { } fn visit_item_impl(&mut self, item: &'ast syn::ItemImpl) { - // Support simple, nongeneric inherent impls in their type's module. - // Qualified Self types, trait impls and generics need explicit identity - // resolution; annotations there must continue to fail closed. + let previous_type = self.impl_type.clone(); + let previous_inherent = self.inherent; + self.impl_type = match item.self_ty.as_ref() { + syn::Type::Path(path) => path.path.segments.last().map(|s| s.ident.to_string()), + _ => None, + }; + self.inherent = item.trait_.is_none(); + // A local named Self may apply the impl's own type parameters. + // Specializations, qualified Self and trait impls still fail closed. let ident = match item.self_ty.as_ref() { - syn::Type::Path(path) if path.qself.is_none() => path.path.get_ident(), + syn::Type::Path(path) if path.qself.is_none() && path.path.segments.len() == 1 => { + let segment = &path.path.segments[0]; + let supported = match &segment.arguments { + syn::PathArguments::None => true, + syn::PathArguments::AngleBracketed(args) => args.args.iter().all(|arg| { + let syn::GenericArgument::Type(syn::Type::Path(arg)) = arg else { + return false; + }; + arg.qself.is_none() + && arg.path.get_ident().is_some_and(|ident| { + item.generics.type_params().any(|param| param.ident == *ident) + }) + }), + _ => false, + }; + supported.then_some(&segment.ident) + } _ => None, }; - if let Some(ident) = ident.filter(|_| { - item.trait_.is_none() && item.generics.params.is_empty() && self.unsupported == 0 - }) { + if let Some(ident) = ident.filter(|_| item.trait_.is_none() && self.unsupported == 0) { self.modules.push(ident.to_string()); visit::visit_item_impl(self, item); self.modules.pop(); @@ -79,15 +102,15 @@ impl<'ast> Visit<'ast> for Functions<'_> { visit::visit_item_impl(self, item); self.unsupported -= 1; } + self.impl_type = previous_type; + self.inherent = previous_inherent; } fn visit_impl_item_fn(&mut self, item: &'ast syn::ImplItemFn) { - let generic = !item.sig.generics.params.is_empty(); - self.unsupported += usize::from(generic); - self.function(&item.sig.ident, &item.block); + self.function(&item.sig.ident, &item.block, true); self.unsupported += 1; visit::visit_impl_item_fn(self, item); - self.unsupported -= 1 + usize::from(generic); + self.unsupported -= 1; } fn visit_item_trait(&mut self, item: &'ast syn::ItemTrait) { @@ -110,8 +133,14 @@ fn inspect(source: &str) -> Result { offset += token.len; } let syntax = syn::parse_file(source)?; - let mut visitor = - Functions { source, modules: Vec::new(), unsupported: 0, functions: Vec::new() }; + let mut visitor = Functions { + source, + modules: Vec::new(), + unsupported: 0, + impl_type: None, + inherent: false, + functions: Vec::new(), + }; visitor.visit_file(&syntax); Ok(json!({"comments": comments, "functions": visitor.functions})) } @@ -157,7 +186,8 @@ mod tests { fn resolves_simple_inherent_methods_and_rejects_other_impl_forms() { for (implementation, supported) in [ ("impl S", true), - ("impl S", false), + ("impl S", true), + ("impl S", false), ("impl Trait for S", false), ("impl m::S", false), ] { @@ -171,6 +201,6 @@ mod tests { } } let value = inspect("impl S { fn f() {} }").unwrap(); - assert_eq!(value["functions"][0]["supported"], false); + assert_eq!(value["functions"][0]["supported"], true); } } diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py index 57374812ea..44ddb6622a 100644 --- a/verification/aeneas/inline.py +++ b/verification/aeneas/inline.py @@ -22,6 +22,7 @@ MARKER = re.compile(r'`{2,}\s*([^\s`]+)') MODEL_SLOT = re.compile(r'@@AENEAS_MODEL\("([^"\n]+)"\)@@') GOLDEN_SLOT = re.compile(r'@@AENEAS_GOLDEN\("([^"\n]+)"\)@@') +PROOF_SLOT = re.compile(r'@@AENEAS_PROOF\("([^"\n]+)"\)@@') def suspicious(text): @@ -36,6 +37,19 @@ def read_source(path): def inventory(root): data = json.loads((root / 'verification/aeneas/inventory.json').read_text()) + if set(data) - {'license', 'version', 'functions', 'covered_impls'}: + raise ValueError('Unknown proof inventory field') + scopes = data.get('covered_impls', []) + if (not isinstance(scopes, list) + or any(not isinstance(scope, dict) or set(scope) != {'file', 'type'} + or not isinstance(scope['file'], str) + or not scope['file'].startswith('zerocopy/src/') + or '..' in Path(scope['file']).parts + or not isinstance(scope['type'], str) + or not re.fullmatch(r'[A-Za-z_][A-Za-z_0-9]*', scope['type']) + for scope in scopes) + or len({(scope['file'], scope['type']) for scope in scopes}) != len(scopes)): + raise ValueError('Invalid or duplicate closed method coverage scope') if data['version'] != 1 or not data['functions']: raise ValueError('Unsupported or empty Aeneas proof inventory') entries = data['functions'] @@ -183,13 +197,35 @@ def char_offset(byte): return found -def discover(root, tool, entries): +def check_coverage(entries, syntax, scopes): + """Require every source-defined inherent method in a covered impl.""" + for scope in scopes: + if (set(scope) != {'file', 'type'} or scope['file'] not in syntax + or not re.fullmatch(r'[A-Za-z_][A-Za-z_0-9]*', scope['type'])): + raise ValueError('Invalid closed method coverage scope') + methods = [function for function in syntax[scope['file']]['functions'] + if function['method'] and function['inherent'] + and function['impl_type'] == scope['type']] + if not methods: + raise ValueError(f'Closed coverage scope has no methods: {scope}') + for function in methods: + if not function['supported']: + raise ValueError(f'Unsupported method in closed coverage scope: {function["path"]}') + matches = [e for e in entries if e['file'] == scope['file'] + and e['syntax'] == function['path']] + if len(matches) != 1: + raise ValueError(f'Missing method proof in closed coverage scope: {function["path"]}') + + +def discover(root, tool, entries, scopes=()): paths = source_files(root, entries) + paths = sorted(set(paths) | {scope['file'] for scope in scopes}) result = subprocess.run([str(tool)], cwd=root, input=json.dumps(paths), text=True, capture_output=True) if result.returncode: raise ValueError(f'Rust syntax inspection failed: {result.stderr}') syntax = json.loads(result.stdout) + check_coverage(entries, syntax, scopes) annotations = {} for file in paths: try: @@ -258,11 +294,22 @@ def expand(match): def assemble(root, annotations, work): wrapper = (root / 'verification/aeneas/lean/Proofs.lean.in').read_text() - if wrapper.count('@@AENEAS_PROOFS@@') != 1: - raise ValueError('Proof wrapper must have exactly one proof slot') ordered = proof_order(list(annotations.values())) - proofs = '\n'.join(a['proof_text'] for a in ordered) - (work / 'Proofs.lean').write_text(wrapper.replace('@@AENEAS_PROOFS@@', proofs)) + if '@@AENEAS_PROOFS@@' in wrapper: + if wrapper.count('@@AENEAS_PROOFS@@') != 1 or PROOF_SLOT.search(wrapper): + raise ValueError('Proof wrapper must have exactly one proof slot') + proofs = '\n'.join(a['proof_text'] for a in ordered) + wrapper = wrapper.replace('@@AENEAS_PROOFS@@', proofs) + else: + # Named slots permit support lemmas between registered function proofs. + # Require the same bijection as the model and golden renderers. + used = PROOF_SLOT.findall(wrapper) + if sorted(used) != sorted(annotations): + raise ValueError('Every annotation must have exactly one proof slot') + wrapper = PROOF_SLOT.sub(lambda m: annotations[m[1]]['proof_text'].rstrip(), wrapper) + if '@@AENEAS_' in wrapper: + raise ValueError('Unexpanded Aeneas proof slot') + (work / 'Proofs.lean').write_text(wrapper) required = ['import Lean', 'import Proofs', 'import Obligations', 'open Lean', ''] for a in annotations.values(): # Normalize total WP and scalar order to independently written arithmetic. @@ -340,9 +387,8 @@ def identity(name): if set(implementation) != {'Ty'}: raise ValueError('Trait impl roots are unsupported') implementation = implementation['Ty'] - if (implementation['kind'] != 'InherentImplBlock' - or any(implementation['params'].values())): - raise ValueError('Generic impl roots are unsupported') + if implementation['kind'] != 'InherentImplBlock': + raise ValueError('Only inherent impl roots are supported') wrapped = implementation['skip_binder'] if set(wrapped) == {'Value'}: body = wrapped['Value'][1] @@ -353,8 +399,8 @@ def identity(name): if set(body) != {'Adt'}: raise ValueError('Inherent Self must resolve to a named type') adt = body['Adt'] - if adt['builtin'] is not None or any(adt['generics'].values()): - raise ValueError('Generic or builtin Self roots are unsupported') + if adt['builtin'] is not None: + raise ValueError('Builtin Self roots are unsupported') self_name = identifiers(type_names.get(adt['id'], [])) prefix = identifiers(name[:index]) if not self_name or self_name[:-1] != prefix: @@ -390,20 +436,17 @@ def split_live(source, entries): # This intentionally supports the pinned generator's root-declaration # layout only. Full-file comparison includes all remaining scaffolding; # unexpected layouts, missing/duplicate roots or new output fail closed. - starts = list(re.finditer(r'^/-- \[(zerocopy::[^\]\n]+)\]:\n', source, re.M)) + starts = list(re.finditer(r'^/-- [^\n]*\n', source, re.M)) def identity(display): if '{' not in display: return display - match = re.fullmatch(r'(.+::)\{([^{}]+)::([A-Za-z_][A-Za-z_0-9]*)\}::' + match = re.fullmatch(r'(.+::)\{([^{}]+)::([A-Za-z_][A-Za-z_0-9]*)(?:<[^{}]+>)?\}::' r'([A-Za-z_][A-Za-z_0-9]*)', display) if not match or match[1] != match[2] + '::': raise ValueError('Unsupported generated inherent method identity') return match[1] + match[3] + '::' + match[4] - identities = [identity(m[1]) for m in starts] - if set(identities) != {e['rust'] for e in entries} or len(starts) != len(entries): - raise ValueError('Pinned Aeneas root declaration layout no longer matches inventory') by_rust = {e['rust']: e for e in entries} replacements = [] models = {} @@ -415,15 +458,30 @@ def identity(display): raise ValueError('Missing generated root documentation or namespace end') declaration_start = close + 3 model = source[declaration_start:end].rstrip() + '\n' - rust = identities[index] + display = re.match(r'/-- \[(zerocopy::[^\]\n]+)\]:', match[0]) + if not display: + continue + rust = identity(display[1]) + if rust not in by_rust: + # Dependencies and constants remain in the full-file scaffolding. + continue entry = by_rust[rust] lines = golden.normalize(model) + # Loop helpers carry the owner's Rust identity; retain their generated + # definitions independently rather than substituting an inline body. + declaration = next((line for line in lines if line.startswith('def ')), '') + if re.match(rf'def {re.escape(entry["model"])}_loop(?:\.body)?(?=\s|\(|$)', declaration): + continue if not lines or not re.match(rf'def {re.escape(entry["model"])}(?=\s|\(|$)', lines[0]): raise ValueError('Unexpected generated Lean root identity') if any(line and not line[0].isspace() for line in lines[1:]): raise ValueError('Unsupported generated root declaration layout') + if rust in models: + raise ValueError('Duplicate generated Lean root identity') models[rust] = model replacements.append((declaration_start, end, f'@@AENEAS_GOLDEN("{entry["golden"]}")@@\n\n')) + if models.keys() != by_rust.keys(): + raise ValueError('Pinned Aeneas root declaration layout no longer matches inventory') for start, end, replacement in reversed(replacements): source = source[:start] + replacement + source[end:] return models, source @@ -460,7 +518,8 @@ def main(): parser.add_argument('--work', type=Path, required=True) args = parser.parse_args() entries = inventory(args.root) - annotations = discover(args.root, args.tool, entries) + scopes = json.loads((args.root / 'verification/aeneas/inventory.json').read_text()).get('covered_impls', []) + annotations = discover(args.root, args.tool, entries, scopes) if args.command == 'bindings': check_bindings(args.root, annotations, args.work / 'zerocopy.llbc') elif args.command == 'update': diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean index c0b42939bd..0d7af38b13 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -38,7 +38,8 @@ run_elab do if used == declName then continue if required.contains used then unless actual.contains used do actual := actual.push used - else if env.getModuleIdxFor? used == some proofModule then + else if env.getModuleIdxFor? used == some proofModule || + (`Zerocopy.Proofs).isPrefixOf (privateToUserName used) then pending := pending.push used for used in actual do unless declared.contains used do diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py index 3bce35f408..a1fa932ffb 100644 --- a/verification/aeneas/tests/test_inline.py +++ b/verification/aeneas/tests/test_inline.py @@ -71,13 +71,30 @@ def test_rejects_comments_statements_and_nested_scopes_before_fence(self): def test_inherent_method_ownership_and_unsupported_impls(self): found = self.parse('mod m { impl S { fn f(self) {\n' + BLOCK + '} } }') self.assertEqual(found[0]['syntax'], 'm::S::f') - for implementation, method in [('impl S', 'fn f()'), + for implementation, method in [('impl S', 'fn f()'), ('impl Trait for S', 'fn f()'), - ('impl m::S', 'fn f()'), - ('impl S', 'fn f()')]: + ('impl m::S', 'fn f()')]: with self.subTest(implementation=implementation, method=method), self.assertRaises(ValueError): self.parse(implementation + ' { ' + method + ' {\n' + BLOCK + '} }') + def test_generic_methods_and_parameterized_self_have_exact_owners(self): + for declaration in ('impl S { fn f(self)', 'impl S { fn f()'): + found = self.parse(declaration + ' {\n' + BLOCK + '} }') + self.assertEqual(found[0]['syntax'], 'S::f') + + def test_closed_method_coverage_detects_unannotated_and_inactive_methods(self): + entry = {**ENTRY, 'syntax': 'S::f'} + scope = {'file': ENTRY['file'], 'type': 'S'} + good = syntax('impl S { fn f(self) { fn harness() {} } }') + inline.check_coverage([entry], {ENTRY['file']: good}, [scope]) + for extra in ('fn missing() {}', '#[cfg(any())] fn inactive() {}'): + bad = syntax('impl S { fn f() {} ' + extra + ' }') + with self.assertRaisesRegex(ValueError, 'Missing method proof'): + inline.check_coverage([entry], {ENTRY['file']: bad}, [scope]) + bad = syntax('impl S { fn f() {} }') + with self.assertRaisesRegex(ValueError, 'Unsupported method'): + inline.check_coverage([entry], {ENTRY['file']: bad}, [scope]) + def test_proof_dependency_order_is_independent_of_source_order(self): caller = {'rust': 'caller', 'depends_on': ['callee']} callee = {'rust': 'callee'} @@ -117,6 +134,25 @@ def test_assembly_orders_proofs_and_records_declared_edges(self): required = (work / 'Required.lean').read_text() self.assertIn('(`Zerocopy.Proofs.caller_spec, #[`Zerocopy.Proofs.callee_spec])', required) + def test_named_proof_slots_have_complete_bijective_coverage(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + wrapper = root / 'verification/aeneas/lean/Proofs.lean.in' + wrapper.parent.mkdir(parents=True) + work = root / 'work' + work.mkdir() + proof = {'rust': 'caller', 'theorem': 'caller_spec', + 'proof_text': 'theorem caller_spec : True := by trivial\n'} + slot = '@@AENEAS_PROOF("caller")@@' + wrapper.write_text('theorem support : True := by trivial\n' + slot) + inline.assemble(root, {'caller': proof}, work) + self.assertIn(proof['proof_text'].rstrip(), (work / 'Proofs.lean').read_text()) + for malformed in ('', slot + slot, slot.replace('caller', 'unknown'), + '@@AENEAS_PROOFS@@' + slot): + with self.subTest(wrapper=malformed), self.assertRaises(ValueError): + wrapper.write_text(malformed) + inline.assemble(root, {'caller': proof}, work) + def test_rejects_near_miss_guards_missing_sections_and_broken_fences(self): variants = [BLOCK.replace('```aeneas', '```Aeneas'), BLOCK.replace('```aeneas', '```aeneos'), @@ -304,7 +340,7 @@ def test_inherent_method_llbc_identity_resolves_named_self(self): llbc = root / 'crate.llbc' llbc.write_text(json.dumps(data)) inline.check_bindings(root, annotations, llbc) - for kind in ('wrong_self', 'missing_self', 'generic', 'trait', 'cross_module'): + for kind in ('wrong_self', 'missing_self', 'trait', 'cross_module'): bad = copy.deepcopy(data) translated = bad['translated'] implementation = translated['fun_decls'][0]['item_meta']['name'][2]['Impl'] @@ -312,8 +348,6 @@ def test_inherent_method_llbc_identity_resolves_named_self(self): translated['type_decls'][0]['item_meta']['name'][-1]['Ident'][0] = 'T' elif kind == 'missing_self': implementation['Ty']['skip_binder']['Deduplicated'] = 99 - elif kind == 'generic': - implementation['Ty']['params']['types'] = ['T'] elif kind == 'trait': implementation.clear() implementation['Trait'] = 0 @@ -333,6 +367,24 @@ def test_generated_inherent_method_identity_and_module_agreement(self): with self.assertRaises(ValueError): inline.split_live(generated.replace('{zerocopy::util::S}', '{zerocopy::other::S}'), [entry]) + def test_dependencies_constants_and_loop_helpers_remain_in_scaffolding(self): + generated = ('namespace Zerocopy\n' + '/-- [zerocopy::util::f]: loop body 0:\n Source: x -/\n' + '@[rust_loop_body]\ndef util.f_loop.body := 1\n\n' + '/-- [zerocopy::util::f]: loop 0:\n Source: x -/\n' + '@[rust_loop]\ndef util.f_loop := 2\n\n' + '/-- [zerocopy::util::f]:\n Source: x -/\n' + 'def util.f :=\n util.f_loop\n\n' + '/-- [zerocopy::util::CONSTANT]\n Source: x -/\n' + 'def util.CONSTANT := 3\n\n' + '/-- [zerocopy::util::dependency]:\n Source: x -/\n' + 'def util.dependency := 4\n\nend Zerocopy\n') + models, scaffold = inline.split_live(generated, [ENTRY]) + self.assertEqual(models[ENTRY['rust']], 'def util.f :=\n util.f_loop\n') + for declaration in ('util.f_loop.body', 'util.f_loop', 'util.CONSTANT', 'util.dependency'): + self.assertIn('def ' + declaration, scaffold) + self.assertNotIn('def util.f :=', scaffold) + if __name__ == '__main__': unittest.main()