[hermes] Add Charon step

tools/hermes/Cargo.toml

@@ -12,6 +12,7 @@ cargo_metadata = "0.23.1"
 clap = { version = "4.5.57", features = ["derive"] }
 clap-cargo = { version = "0.18.3", features = ["cargo_metadata"] }
 dashmap = "6.1.0"
+env_logger = "0.11.8"
 log = "0.4.29"
 miette = { version = "7.6.0", features = ["derive", "fancy"] }
 proc-macro2 = { version = "1.0.105", features = ["span-locations"] }

tools/hermes/src/charon.rs

@@ -0,0 +1,85 @@
+use std::process::Command;
+
+use anyhow::{bail, Context as _, Result};
+
+use crate::{
+    resolve::{Args, HermesTargetKind, Roots},
+    shadow::HermesArtifact,
+};
+
+pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesArtifact]) -> Result<()> {
+    let charon_root = roots.charon_root();
+
+    std::fs::create_dir_all(&charon_root).context("Failed to create charon output directory")?;
+
+    for artifact in packages {
+        if artifact.start_from.is_empty() {
+            continue;
+        }
+
+        log::info!("Invoking Charon on package '{}'...", artifact.name.package_name);
+
+        let mut cmd = Command::new("charon");
+        cmd.arg("cargo");
+
+        // Output artifacts to target/hermes/<hash>/charon
+        let llbc_path = charon_root.join(artifact.llbc_file_name());
+        log::debug!("Writing .llbc file to {}", llbc_path.display());
+        cmd.arg("--dest-file").arg(llbc_path);
+
+        // Fail fast on errors
+        cmd.arg("--abort-on-error");
+
+        // Start translation from specific entry points
+        cmd.arg("--start-from").arg(artifact.start_from.join(","));
+
+        // Separator for the underlying cargo command
+        cmd.arg("--");
+
+        cmd.arg("--manifest-path").arg(&artifact.shadow_manifest_path);
+
+        match artifact.target_kind {
+            HermesTargetKind::Lib
+            | HermesTargetKind::RLib
+            | HermesTargetKind::ProcMacro
+            | HermesTargetKind::CDyLib
+            | HermesTargetKind::DyLib
+            | HermesTargetKind::StaticLib => {
+                cmd.arg("--lib");
+            }
+            HermesTargetKind::Bin => {
+                cmd.arg("--bin").arg(&artifact.name.target_name);
+            }
+            HermesTargetKind::Example => {
+                cmd.arg("--example").arg(&artifact.name.target_name);
+            }
+            HermesTargetKind::Test => {
+                cmd.arg("--test").arg(&artifact.name.target_name);
+            }
+        }
+
+        // Forward all feature-related flags.
+        if args.features.all_features {
+            cmd.arg("--all-features");
+        }
+        if args.features.no_default_features {
+            cmd.arg("--no-default-features");
+        }
+        for feature in &args.features.features {
+            cmd.arg("--features").arg(feature);
+        }
+
+        // Reuse the main target directory for dependencies to save time.
+        cmd.env("CARGO_TARGET_DIR", &roots.cargo_target_dir);
+
+        log::debug!("Command: {:?}", cmd);
+
+        let status = cmd.status().context("Failed to execute charon")?;
+
+        if !status.success() {
+            bail!("Charon failed with status: {}", status);
+        }
+    }
+
+    Ok(())
+}

tools/hermes/src/main.rs

@@ -1,3 +1,4 @@
+mod charon;
 mod errors;
 mod parse;
 mod resolve;
@@ -22,6 +23,8 @@ enum Commands {
 }
 
 fn main() -> anyhow::Result<()> {
+    env_logger::init();
+
     if std::env::var("HERMES_UI_TEST_MODE").is_ok() {
         ui_test_shim::run();
         return Ok(());
@@ -31,7 +34,17 @@ fn main() -> anyhow::Result<()> {
     match args.command {
         Commands::Verify(resolve_args) => {
             let roots = resolve::resolve_roots(&resolve_args)?;
-            shadow::build_shadow_crate(&roots)
+            let entry_points = shadow::build_shadow_crate(&roots)?;
+            if entry_points.is_empty() {
+                anyhow::bail!("No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.");
+            }
+            charon::run_charon(&resolve_args, &roots, &entry_points)
         }
     }
 }
+
+/// A no-op function with a Hermes annotation so we can test Hermes on itself.
+///
+/// ```lean
+/// ```
+fn _foo() {}

tools/hermes/src/parse.rs

@@ -45,6 +45,17 @@ pub enum ParsedItem {
 }
 
 impl ParsedItem {
+    pub fn name(&self) -> Option<String> {
+        match self {
+            Self::Fn(item) => Some(item.sig.ident.to_string()),
+            Self::Struct(item) => Some(item.ident.to_string()),
+            Self::Enum(item) => Some(item.ident.to_string()),
+            Self::Union(item) => Some(item.ident.to_string()),
+            Self::Trait(item) => Some(item.ident.to_string()),
+            Self::Impl(_) => None,
+        }
+    }
+
     /// Returns the attributes on this item.
     fn attrs(&self) -> &[Attribute] {
         match self {
@@ -62,7 +73,7 @@ impl ParsedItem {
 #[derive(Debug)]
 pub struct ParsedLeanItem {
     pub item: ParsedItem,
-    module_path: Vec<String>,
+    pub module_path: Vec<String>,
     lean_block: String,
     source_file: Option<PathBuf>,
 }

tools/hermes/src/resolve.rs

@@ -11,44 +11,44 @@ use clap::Parser;
 #[derive(Parser, Debug)]
 pub struct Args {
     #[command(flatten)]
-    manifest: clap_cargo::Manifest,
+    pub manifest: clap_cargo::Manifest,
 
     #[command(flatten)]
-    workspace: clap_cargo::Workspace,
+    pub workspace: clap_cargo::Workspace,
 
     #[command(flatten)]
-    features: clap_cargo::Features,
+    pub features: clap_cargo::Features,
 
     /// Verify the library target
     #[arg(long)]
-    lib: bool,
+    pub lib: bool,
 
     /// Verify specific binary targets
     #[arg(long)]
-    bin: Vec<String>,
+    pub bin: Vec<String>,
 
     /// Verify all binary targets
     #[arg(long)]
-    bins: bool,
+    pub bins: bool,
 
     /// Verify specific example targets
     #[arg(long)]
-    example: Vec<String>,
+    pub example: Vec<String>,
 
     /// Verify all example targets
     #[arg(long)]
-    examples: bool,
+    pub examples: bool,
 
     /// Verify specific test targets
     #[arg(long)]
-    test: Vec<String>,
+    pub test: Vec<String>,
 
     /// Verify all test targets
     #[arg(long)]
-    tests: bool,
+    pub tests: bool,
 }
 
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
 pub enum HermesTargetKind {
     /// A library target (generic).
     Lib,
@@ -98,19 +98,37 @@ impl TryFrom<&TargetKind> for HermesTargetKind {
     }
 }
 
+#[derive(Clone, Debug, Hash, PartialEq, Eq)]
+pub struct HermesTargetName {
+    pub package_name: PackageName,
+    pub target_name: String,
+}
+
+#[derive(Debug)]
+pub struct HermesTarget {
+    pub name: HermesTargetName,
+    pub kind: HermesTargetKind,
+    /// Path to the main source file for this target.
+    pub src_path: PathBuf,
+}
+
 #[derive(Debug)]
 pub struct Roots {
     pub workspace: PathBuf,
     pub cargo_target_dir: PathBuf,
     // E.g., `target/hermes/<hash>`.
     hermes_run_root: PathBuf,
-    pub roots: Vec<(PackageName, HermesTargetKind, PathBuf)>,
+    pub roots: Vec<HermesTarget>,
 }
 
 impl Roots {
     pub fn shadow_root(&self) -> PathBuf {
         self.hermes_run_root.join("shadow")
     }
+
+    pub fn charon_root(&self) -> PathBuf {
+        self.hermes_run_root.join("charon")
+    }
 }
 
 /// Resolves all verification roots.
@@ -151,11 +169,14 @@ pub fn resolve_roots(args: &Args) -> Result<Roots> {
         }
 
         for (target, kind) in targets {
-            roots.roots.push((
-                package.name.clone(),
-                kind.clone(),
-                target.src_path.as_std_path().to_owned(),
-            ));
+            roots.roots.push(HermesTarget {
+                name: HermesTargetName {
+                    package_name: package.name.clone(),
+                    target_name: target.name.clone(),
+                },
+                kind,
+                src_path: target.src_path.as_std_path().to_owned(),
+            });
         }
     }