Skip to content

[WIP] More cleanup #2980

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: Gbeca6e8c6a2f4e776c00719d86c9eabf4f63fe2e
Choose a base branch
from
+788 βˆ’609
Open

[WIP] More cleanup #2980

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
366 changes: 146 additions & 220 deletions tools/hermes/src/desugar.rs
View file
Open in desktop

Large diffs are not rendered by default.

31 changes: 19 additions & 12 deletions tools/hermes/src/docs.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
use syn::{Attribute, Expr, ExprLit, Lit, Meta};

/// Extracts the string content of a `#[doc = "..."]` or `/// ...` attribute.
///
/// Returns `None` if the attribute is not a doc comment.
pub fn parse_doc_attr(attr: &Attribute) -> Option<String> {
if !attr.path().is_ident("doc") {
Expand All @@ -24,26 +25,27 @@ pub fn parse_doc_attr(attr: &Attribute) -> Option<String> {
}
}

/// Helper to check if a line is a Hermes directive.
/// Returns the trimmed content if it matches the prefix, otherwise None.
/// This handles the `///@` syntax.
/// Parses a specific Hermes tag from a line.
/// Returns `Some(content)` if the line starts with `///@ <tag>` or `///@<tag>`.
/// Content is trimmed.
/// Example: `parse_hermes_tag("@ lean spec", "lean spec")` -> `Some(...)`
///
/// Checks if the line starts with `///@ <tag>` or `///@<tag>`.
/// Returns `Some(content)` with the content trimmed if there is a match.
///
/// # Example
///
/// `parse_hermes_tag("@ lean spec foo", "lean spec")` -> `Some("foo")`
pub fn parse_hermes_tag<'a>(line: &'a str, tag: &str) -> Option<&'a str> {
let trimmed = line.trim();
if !trimmed.starts_with('@') {
return None;
}

// Check for "@ <tag>" or "@<tag>"
// We expect usage like "@ lean spec"
// Check for "@ <tag>" (with space)
let prefix_space = format!("@ {}", tag);
if let Some(rest) = trimmed.strip_prefix(&prefix_space) {
return Some(rest.trim());
}

// Check for "@<tag>" (no space)
let prefix_nospace = format!("@{}", tag);
if let Some(rest) = trimmed.strip_prefix(&prefix_nospace) {
return Some(rest.trim());
Expand All @@ -53,16 +55,21 @@ pub fn parse_hermes_tag<'a>(line: &'a str, tag: &str) -> Option<&'a str> {
}

/// Checks if a line is a Hermes directive (starts with `@`).
///
/// This is used to filter lines from doc comments that are intended for Hermes
/// rather than for standard Rust documentation.
pub fn is_hermes_directive(line: &str) -> bool {
line.trim().starts_with('@')
}
/// Iterates over all doc attributes, parsing them, splitting into lines,
/// and yielding only those that are Hermes directives (start with `@`).
/// Returns trimmed lines.

/// Iterates over all doc attributes of an item, parses them, splits them into lines,
/// and yields only those lines that are Hermes directives (start with `@`).
///
/// This helper abstracts away the complexity of parsing `#[doc = "..."]` attributes
/// and filtering for irrelevant comments.
pub fn iter_hermes_lines(attrs: &[Attribute]) -> impl Iterator<Item = String> + '_ {
attrs.iter().flat_map(|attr| {
if let Some(doc) = parse_doc_attr(attr) {
// We must collect to separate lifetime from `doc`
doc.lines()
.map(|line| line.trim().to_string())
.filter(|line| is_hermes_directive(line))
Expand Down
2 changes: 1 addition & 1 deletion tools/hermes/src/include/Std.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ namespace Hermes.Std.Memory

variable {T : Type}

def ConstPtr (T : Type) := ConstRawPtr T
abbrev ConstPtr (T : Type) := ConstRawPtr T

-- Maps a pointer to its address
opaque addr (ptr : ConstPtr T) : Nat
Expand Down
33 changes: 28 additions & 5 deletions tools/hermes/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,17 +6,40 @@
// This file may not be copied, modified, or distributed except according to
// those terms.

//! Hermes: A verification orchestrator for Rust.
//! Hermes: A Literate Verification Orchestrator for Rust.
//!
//! This library provides the core logic for the `cargo-hermes` CLI tool, including:
//! - Parsing Rust code for verification annotations.
//! - Orchestrating the execution of Charon and Aeneas.
//! - Stitching generated Lean code with user-provided proofs.
//! Hermes facilitates the verification of Rust crates by integrating with
//! [Charon](https://github.com/AeneasVerif/charon) and [Aeneas](https://github.com/AeneasVerif/aeneas).
//!
//! It provides a seamless pipeline that:
//! 1. **Scaffolds** a "Shadow Crate" to sanitize Rust code for verification (removing unsafe, mocking models).
//! 2. **Extracts** the crate to LLBC (Low-Level Borrow Calculus) using Charon.
//! 3. **Translates** LLBC to Lean 4 models using Aeneas.
//! 4. **Stitches** user-provided proofs (written in Rust doc comments) into the generated Lean project.
//! 5. **Verifies** the final result using Lean's build system (`lake`).
//!
//! This library exposes the core modules used by the `cargo-hermes` binary.

/// Handles the "desugaring" of high-level Hermes specifications (e.g., `///@ ensure ...`)
/// into valid Lean code.
pub mod desugar;

/// Helper utilities for parsing Rust documentation attributes and extracting Hermes directives.
pub mod docs;

/// Wrappers around external tools (Charon, Aeneas, Lake) to handle their invocation.
pub mod orchestration;

/// logic for parsing Rust source files to extract functions, structs, and their attached
/// Hermes annotations (`///@ ...`).
pub mod parser;

/// The core pipeline definition, orchestrating the end-to-end verification flow.
pub mod pipeline;

/// logic for creating and sanitizing the "Shadow Crate", which is the version of the crate
/// actually seen by the verification tools.
pub mod shadow;

/// Utilities for translating Rust types and signatures into their Lean equivalents during stitching.
pub mod translator;
30 changes: 23 additions & 7 deletions tools/hermes/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,10 @@ use anyhow::Result;
use cargo_hermes::pipeline::{Sorry, run_pipeline};
use clap::{Parser, Subcommand};

/// The primary CLI entry point for `cargo-hermes`.
///
/// This enum defines the command-line interface, which is invoked as `cargo hermes ...`.
/// The `bin_name = "cargo"` attribute ensures that it parses correctly when called via Cargo.
#[derive(Parser, Debug)]
#[command(name = "cargo-hermes")]
#[command(bin_name = "cargo")]
Expand All @@ -28,22 +32,34 @@ pub struct HermesArgs {

#[derive(Subcommand, Debug)]
pub enum Commands {
/// Verify the current crate
/// Verify a crate or script
Verify {
/// Optional crate name
/// The name of the crate to verify.
///
/// If not provided, it is inferred from `Cargo.toml`.
#[arg(long)]
crate_name: Option<String>,
/// Path to generated files directory

/// Destination directory where generated artifacts (Lean code, LLBC) will be output.
///
/// Defaults to `verification`.
#[arg(long, default_value = "verification")]
dest: PathBuf,
/// Path to local Aeneas repository (specifically backends/lean)

/// Path to the local Aeneas repository (specifically `backends/lean`).
///
/// If not provided, Hermes will attempt to fetch Aeneas from git (in `lakefile.lean`).
#[arg(long)]
aeneas_path: Option<PathBuf>,
/// Path to Cargo.toml or Cargo script

/// Path to the `Cargo.toml` manifest or a standalone Rust script.
///
/// If pointing to a script (`.rs`), Hermes treats it as a single-file crate.
#[arg(long)]
manifest_path: Option<PathBuf>,
/// Allow missing proofs (substitutes 'sorry') and instruct Lean to accept 'sorry'

/// If set, instructs Lean to accept `sorry` (missing proofs) without failing verification.
///
/// This is useful for incremental development.
#[arg(long)]
allow_sorry: bool,
},
Expand Down
14 changes: 12 additions & 2 deletions tools/hermes/src/orchestration.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,24 +12,29 @@ use anyhow::{Context, Result, anyhow};

/// Runs the Charon tool to extract LLBC (Low-Level Borrow Calculus) from the crate.
///
/// Charon is the frontend for Aeneas. It analyzes the Rust code and produces a serialized
/// representation of the borrow-checked IR.
///
/// # Arguments
/// * `crate_root` - Path to the root of the crate to analyze.
/// * `dest_file` - Destination path for the LLBC file (e.g. `.../crate.llbc`).
/// * `manifest_path` - Optional path to a specific Cargo.toml or script file.
/// * `opaque_funcs` - List of fully qualified function names to mark as opaque.
/// * `opaque_funcs` - List of fully qualified function names to mark as opaque (Charon won't analyze their bodies).
/// * `start_from` - List of modules to start analysis from (selective extraction).
pub fn run_charon(
crate_root: &Path,
dest_file: &Path,
manifest_path: Option<&Path>,
opaque_funcs: &[String],
start_from: &[String],
) -> Result<()> {
let crate_root = crate_root.to_str().unwrap();
let dest_file = dest_file.to_str().unwrap();

log::debug!("Running charon in {:?}", crate_root);
let mut cmd = Command::new("charon");

// Avoid deadlock with outer cargo
// Avoid deadlock with outer cargo.
cmd.env_remove("CARGO_TARGET_DIR");

// Triggered when we convert `unsafe { ... }` into `{ ... }`.
Expand All @@ -45,6 +50,11 @@ pub fn run_charon(
cmd.arg(func);
}

if !start_from.is_empty() {
cmd.arg("--start-from");
cmd.arg(start_from.join(","));
}

if let Some(path) = manifest_path {
cmd.arg("--");
if path.extension().is_some_and(|e| e == "rs") {
Expand Down
Loading
Loading