Skip to content

Support generic inline proofs and closed method coverage #3741

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
joshlf wants to merge 1 commit into from
Closed

Support generic inline proofs and closed method coverage #3741

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
64 changes: 47 additions & 17 deletions tools/aeneas-inline/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ struct Functions<'a> {
source: &'a str,
modules: Vec<String>,
unsupported: usize,
impl_type: Option<String>,
inherent: bool,
functions: Vec<Value>,
}

Expand All @@ -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();
Expand All @@ -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,
}));
}
}
Expand All @@ -53,24 +56,44 @@ 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);
self.unsupported -= 1;
}

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();
Expand All @@ -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) {
Expand All @@ -110,8 +133,14 @@ fn inspect(source: &str) -> Result<Value, syn::Error> {
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}))
}
Expand Down Expand Up @@ -157,7 +186,8 @@ mod tests {
fn resolves_simple_inherent_methods_and_rejects_other_impl_forms() {
for (implementation, supported) in [
("impl S", true),
("impl<T> S<T>", false),
("impl<T> S<T>", true),
("impl S<u8>", false),
("impl Trait for S", false),
("impl m::S", false),
] {
Expand All @@ -171,6 +201,6 @@ mod tests {
}
}
let value = inspect("impl S { fn f<T>() {} }").unwrap();
assert_eq!(value["functions"][0]["supported"], false);
assert_eq!(value["functions"][0]["supported"], true);
}
}
93 changes: 76 additions & 17 deletions verification/aeneas/inline.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand All @@ -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']
Expand Down Expand Up @@ -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']]
Comment on lines +206 to +208

@chatgpt-codex-connector chatgpt-codex-connector Bot Oct 2, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Reject macros in closed impl coverage

When a covered impl contains at least one explicit method plus an associated-item macro such as generate_methods!(), the syntax tool reports only the explicit ImplItemFn nodes, so this list can be fully matched while the macro expands to additional unregistered methods. That makes the new “closed” coverage check silently certify incomplete coverage; either expand such macros or fail closed whenever a covered impl contains an uninspectable associated-item macro.

Useful? React with 👍 / 👎.

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:
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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]
Expand All @@ -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:
Expand Down Expand Up @@ -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 = {}
Expand All @@ -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:
Comment on lines +461 to +465

@chatgpt-codex-connector chatgpt-codex-connector Bot Oct 2, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Skip unknown roots before enforcing inherent identity syntax

When generated Funs.lean contains an unregistered dependency with a braced identity outside this narrow inherent-method grammar—for example a local trait method displayed as {impl Trait for Type}::method—identity() raises here before the subsequent rust not in by_rust branch can preserve it as scaffolding. Consequently --update-goldens fails instead of retaining valid dependency output; unsupported identities should only be rejected when they correspond to an inventoried root.

Useful? React with 👍 / 👎.

# 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
Comment on lines +470 to +474

@chatgpt-codex-connector chatgpt-codex-connector Bot Oct 2, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Preserve every numbered loop helper

When an annotated function has multiple loops, Aeneas must disambiguate the later generated loop declarations with a numbered variant of the model’s _loop name while their documentation still carries the owning Rust identity. This regex accepts only the unsuffixed first helper, so a later helper is treated as the registered root and fails the following model-identity check, preventing golden updates for multi-loop functions. Classify loop helpers from their generated attribute/documentation or accept the generator’s numbered loop-name variants.

Useful? React with 👍 / 👎.

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
Expand Down Expand Up @@ -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':
Expand Down
3 changes: 2 additions & 1 deletion verification/aeneas/lean/Check.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading