Skip to content

[WIP] Parser + --allow-sorry #2969

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

Open
joshlf wants to merge 1 commit into
base: Gb0d4d182a8f82f845a81ba9cd36038cef442a30e
Choose a base branch
from
Open

[WIP] Parser + --allow-sorry #2969

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
2 changes: 2 additions & 0 deletions tools/Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions tools/hermes/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,3 +9,5 @@ clap = { version = "4.5.56", features = ["derive"] }
regex = "1.12.2"
walkdir = "2.5.0"
cargo_metadata = "0.18"
syn = { version = "2.0.114", features = ["full", "visit", "extra-traits"] }
quote = "1.0.43"
11 changes: 8 additions & 3 deletions tools/hermes/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
use std::path::PathBuf;

use anyhow::Result;
use cargo_hermes::pipeline::run_pipeline;
use cargo_hermes::pipeline::{Sorry, run_pipeline};
use clap::{Parser, Subcommand};

#[derive(Parser, Debug)]
Expand Down Expand Up @@ -43,14 +43,19 @@ pub enum Commands {
/// Path to Cargo.toml or Cargo script
#[arg(long)]
manifest_path: Option<PathBuf>,
/// Allow missing proofs (substitutes 'sorry') and instruct Lean to accept 'sorry'
#[arg(long)]
allow_sorry: bool,
},
}

fn main() -> Result<()> {
let CargoCli::Hermes(args) = CargoCli::parse();
let Commands::Verify { crate_name, dest, aeneas_path, manifest_path } = args.command;
let Commands::Verify { crate_name, dest, aeneas_path, manifest_path, allow_sorry } =
args.command;

let crate_root = std::env::current_dir()?;
let dest = dest.canonicalize()?;
run_pipeline(crate_name, &crate_root, &dest, aeneas_path, manifest_path)
let sorry_mode = if allow_sorry { Sorry::AllowSorry } else { Sorry::RejectSorry };
run_pipeline(crate_name, &crate_root, &dest, aeneas_path, manifest_path, sorry_mode)
}
226 changes: 172 additions & 54 deletions tools/hermes/src/parser.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,70 +6,188 @@
// This file may not be copied, modified, or distributed except according to
// those terms.

use std::sync::LazyLock;
use anyhow::{Result, bail};
use syn::{
Attribute, ItemFn, parse_file,
visit::{self, Visit},
};

use anyhow::Result;
use regex::Regex;

/// Represents a specification block extracted from the source code.
///
/// Contains the function name it applies to and the raw body of the specification.
/// Represents a function parsed from the source code, including its signature and attached specs.
#[derive(Debug, Clone)]
pub struct SpecBlock {
pub function_name: String,
pub body: String,
pub struct ParsedFunction {
pub fn_name: String,
pub generics: syn::Generics,
pub spec: Option<String>,
pub proof: Option<String>,
}

/// Represents a proof block extracted from the source code.
///
/// Contains the raw body of the proof.
#[derive(Debug, Clone)]
pub struct ProofBlock {
pub body: String,
pub struct ExtractedBlocks {
pub functions: Vec<ParsedFunction>,
}

#[derive(Debug, Clone)]
pub struct ExtractedBlocks {
pub specs: Vec<SpecBlock>,
pub proofs: Vec<ProofBlock>,
struct SpecVisitor {
functions: Vec<ParsedFunction>,
errors: Vec<anyhow::Error>,
}

/// Extracts both specification and proof blocks from the provided source content.
///
/// This function uses regular expressions to find blocks formatted as:
/// - `/*@ lean spec function_name ... @*/`
/// - `/*@ proof ... @*/`
pub fn extract_blocks(content: &str) -> Result<ExtractedBlocks> {
// Regex matches:
// - Start with `/*@`
// - `lean spec` followed by function name
// - Capture function name in `fn_name`
// - Capture content in `body` (non-greedy)
// - End with `@*/`
static SPEC_RE: LazyLock<Regex> = LazyLock::new(|| {
Regex::new(r"(?ms)/\*\@\s*lean\s+spec\s+(?P<fn_name>\w+)\s+(?P<body>.*?)\s*@\*/").unwrap()
});

// Regex matches:
// - Start with `/*@`
// - `proof`
// - Capture content in `body` (non-greedy)
// - End with `@*/`
static PROOF_RE: LazyLock<Regex> =
LazyLock::new(|| Regex::new(r"(?ms)/\*\@\s*proof\s+(?P<body>.*?)\s*@\*/").unwrap());

let mut specs = Vec::new();
for cap in SPEC_RE.captures_iter(content) {
specs.push(SpecBlock {
function_name: cap["fn_name"].to_string(),
body: cap["body"].trim().to_string(),
});
impl SpecVisitor {
fn new() -> Self {
Self { functions: Vec::new(), errors: Vec::new() }
}

fn check_attrs_for_misplaced_spec(&mut self, attrs: &[Attribute], item_kind: &str) {
for attr in attrs {
if let Some(doc_str) = parse_doc_attr(attr) {
if doc_str.trim_start().starts_with("@") {
self.errors.push(anyhow::anyhow!(
"Found `///@` spec usage on a {}, but it is only allowed on functions.",
item_kind
));
}
}
}
}
}

impl<'ast> Visit<'ast> for SpecVisitor {
fn visit_item_fn(&mut self, node: &'ast ItemFn) {
let fn_name = node.sig.ident.to_string();
let mut spec_lines = Vec::new();
let mut proof_lines = Vec::new();
let mut current_mode = None; // None, Some("spec"), Some("proof")

for attr in &node.attrs {
if let Some(doc_str) = parse_doc_attr(attr) {
let trimmed = doc_str.trim();
// Check for ///@ marker (doc comment starting with @)
if trimmed.starts_with('@') {
// Check if it's a new block start
if let Some(content) = trimmed.strip_prefix("@ lean spec") {
current_mode = Some("spec");
spec_lines.push(content.to_string());
} else if let Some(content) = trimmed.strip_prefix("@ lean model") {
current_mode = Some("spec"); // Treat model as spec
spec_lines.push(content.to_string());
} else if let Some(content) = trimmed.strip_prefix("@ proof") {
current_mode = Some("proof");
proof_lines.push(content.to_string());
} else {
// Continuation line
match current_mode {
Some("spec") => {
// strip leading @ and space?
// User types `///@ ...` -> extracted `@ ...`
// If we just extract `@`, we get ` ...`
// The user might put `///@ ...`.
// If I strip `@`, I get ` ...`.
// I should probably strip the leading `@` and one optional space?
// `trimmed` starts with `@`.
Comment on lines +78 to +84
Copy link
Contributor

@gemini-code-assist gemini-code-assist bot Feb 2, 2026

Choose a reason for hiding this comment

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

medium

These comments appear to be leftover development notes. They can be removed to improve code clarity.

let content = &trimmed[1..];
spec_lines.push(content.to_string());
}
Some("proof") => {
let content = &trimmed[1..];
proof_lines.push(content.to_string());
}
None => {
// Orphaned @ line? or maybe not meant for us?
self.errors.push(anyhow::anyhow!("Found `///@` line without preceding `lean spec` or `proof` on function '{}'", fn_name));
}
_ => {} // Should not be possible with current_mode logic
}
}
}
}
}

let spec = if !spec_lines.is_empty() {
let full_spec = spec_lines.join("\n");
let trimmed_spec = full_spec.trim();
// Strip function name from the beginning of the spec
if let Some(rest) = trimmed_spec.strip_prefix(fn_name.as_str()) {
Some(rest.trim().to_string())
} else {
Some(trimmed_spec.to_string())
}
} else {
None
};

let proof = if !proof_lines.is_empty() { Some(proof_lines.join("\n")) } else { None };

if spec.is_some() || proof.is_some() {
self.functions.push(ParsedFunction {
fn_name,
generics: node.sig.generics.clone(),
spec,
proof,
});
}

// Continue visiting children
visit::visit_item_fn(self, node);
}

fn visit_item_struct(&mut self, node: &'ast syn::ItemStruct) {
self.check_attrs_for_misplaced_spec(&node.attrs, "struct");
visit::visit_item_struct(self, node);
}

fn visit_item_enum(&mut self, node: &'ast syn::ItemEnum) {
self.check_attrs_for_misplaced_spec(&node.attrs, "enum");
visit::visit_item_enum(self, node);
}

fn visit_item_mod(&mut self, node: &'ast syn::ItemMod) {
self.check_attrs_for_misplaced_spec(&node.attrs, "module");
visit::visit_item_mod(self, node);
}

fn visit_item_const(&mut self, node: &'ast syn::ItemConst) {
self.check_attrs_for_misplaced_spec(&node.attrs, "const");
visit::visit_item_const(self, node);
}

// Catch-all for other items with attributes?
// Ideally we'd cover all items, but these are the most common places users might mistakenly put docs.
// Let's also cover TypeAlias and Trait

fn visit_item_type(&mut self, node: &'ast syn::ItemType) {
self.check_attrs_for_misplaced_spec(&node.attrs, "type alias");
visit::visit_item_type(self, node);
}

fn visit_item_trait(&mut self, node: &'ast syn::ItemTrait) {
self.check_attrs_for_misplaced_spec(&node.attrs, "trait");
visit::visit_item_trait(self, node);
}
}

fn parse_doc_attr(attr: &Attribute) -> Option<String> {
if !attr.path().is_ident("doc") {
return None;
}

// syn 2.0: doc = "..." is a NameValue meta
match &attr.meta {
syn::Meta::NameValue(nv) => match &nv.value {
syn::Expr::Lit(syn::ExprLit { lit: syn::Lit::Str(s), .. }) => Some(s.value()),
_ => None,
},
_ => None,
}
}

pub fn extract_blocks(content: &str) -> Result<ExtractedBlocks> {
let ast = parse_file(content)?;
let mut visitor = SpecVisitor::new();
visitor.visit_file(&ast);

let mut proofs = Vec::new();
for cap in PROOF_RE.captures_iter(content) {
proofs.push(ProofBlock { body: cap["body"].trim().to_string() });
if !visitor.errors.is_empty() {
// Return the first error for now, or bundle them
let msg = visitor.errors.iter().map(|e| e.to_string()).collect::<Vec<_>>().join("\n");
bail!("Spec extraction failed:\n{}", msg);
}

Ok(ExtractedBlocks { specs, proofs })
Ok(ExtractedBlocks { functions: visitor.functions })
}
Loading
Loading