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()