[hermes] Invoke Aeneas

tools/hermes/src/aeneas.rs

@@ -0,0 +1,56 @@
+use std::process::Command;
+
+use anyhow::{bail, Context, Result};
+
+use crate::{resolve::Roots, scanner::HermesArtifact};
+
+pub fn run_aeneas(roots: &Roots, artifacts: &[HermesArtifact]) -> Result<()> {
+    let llbc_root = roots.llbc_root();
+    let lean_generated_root = roots.lean_generated_root();
+
+    for artifact in artifacts {
+        if artifact.start_from.is_empty() {
+            log::debug!(
+                "Skipping artifact '{}' because it has no entry points",
+                artifact.name.target_name
+            );
+            continue;
+        }
+
+        log::debug!("Invoking Aeneas on artifact '{}'...", artifact.name.target_name);
+
+        let llbc_path = llbc_root.join(artifact.llbc_file_name());
+        let output_dir = lean_generated_root.join(artifact.artifact_slug());
+
+        std::fs::create_dir_all(&output_dir).context("Failed to create Aeneas output directory")?;
+
+        let mut cmd = Command::new("aeneas");
+
+        cmd.arg("-backend").arg("lean");
+        cmd.arg("-dest").arg(&output_dir);
+        cmd.arg("-split-files");
+        cmd.arg("-no-lean-default-lakefile");
+        cmd.arg("-decreases-clauses");
+        cmd.arg("-abort-on-error");
+
+        // TODO: Handle opaque functions (`unsafe(axiom)`).
+        // We need to parse these from the AST and pass them as `-opaque module::params::...`
+        cmd.arg(&llbc_path);
+
+        log::debug!("Command: {:?}", cmd);
+
+        let output = cmd.output().context("Failed to spawn aeneas")?;
+
+        if !output.status.success() {
+            let stderr = String::from_utf8_lossy(&output.stderr);
+            bail!(
+                "Aeneas failed for package '{}' with status: {}\nstderr:\n{}",
+                artifact.name.package_name,
+                output.status,
+                stderr
+            );
+        }
+    }
+
+    Ok(())
+}

tools/hermes/src/charon.rs

@@ -12,9 +12,9 @@ use crate::{
 };
 
 pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesArtifact]) -> Result<()> {
-    let charon_root = roots.charon_root();
+    let llbc_root = roots.llbc_root();
 
-    std::fs::create_dir_all(&charon_root).context("Failed to create charon output directory")?;
+    std::fs::create_dir_all(&llbc_root).context("Failed to create LLBC output directory")?;
 
     for artifact in packages {
         if artifact.start_from.is_empty() {
@@ -26,8 +26,8 @@ pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesArtifact]) -> Re
         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());
+        // Output artifacts to target/hermes/<hash>/llbc
+        let llbc_path = llbc_root.join(artifact.llbc_file_name());
         log::debug!("Writing .llbc file to {}", llbc_path.display());
         cmd.arg("--dest-file").arg(llbc_path);
 

tools/hermes/src/main.rs

@@ -1,3 +1,4 @@
+mod aeneas;
 mod charon;
 mod diagnostics;
 mod errors;
@@ -37,9 +38,11 @@ fn main() -> anyhow::Result<()> {
             let roots = resolve::resolve_roots(&resolve_args)?;
             let packages = scanner::scan_workspace(&roots)?;
             if packages.is_empty() {
-                anyhow::bail!("No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.");
+                log::warn!("No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.");
+                return Ok(());
             }
-            charon::run_charon(&resolve_args, &roots, &packages)
+            charon::run_charon(&resolve_args, &roots, &packages)?;
+            aeneas::run_aeneas(&roots, &packages)
         }
     }
 }

tools/hermes/src/resolve.rs

@@ -125,8 +125,12 @@ pub struct Roots {
 }
 
 impl Roots {
-    pub fn charon_root(&self) -> PathBuf {
-        self.hermes_run_root.join("charon")
+    pub fn llbc_root(&self) -> PathBuf {
+        self.hermes_run_root.join("llbc")
+    }
+
+    pub fn lean_generated_root(&self) -> PathBuf {
+        self.hermes_run_root.join("lean").join("generated")
     }
 }
 

tools/hermes/src/scanner.rs

@@ -22,11 +22,13 @@ pub struct HermesArtifact {
 }
 
 impl HermesArtifact {
-    /// Returns the name of the `.llbc` file to use for this artifact.
+    /// Returns a unique "slug" for this artifact, used for file naming.
     ///
     /// Guarantees uniqueness based on manifest path even if multiple packages
     /// have the same name.
-    pub fn llbc_file_name(&self) -> String {
+    ///
+    /// Format: `{package_name}-{target_name}-{hash:08x}`
+    pub fn artifact_slug(&self) -> String {
         fn hash<T: Hash>(t: &T) -> u64 {
             let mut s = std::collections::hash_map::DefaultHasher::new();
             t.hash(&mut s);
@@ -40,7 +42,13 @@ impl HermesArtifact {
         let h1 = hash(&self.name.target_name);
         let h2 = hash(&self.target_kind);
         let h = hash(&[h0, h1, h2]);
-        format!("{}-{}-{:08x}.llbc", self.name.package_name, self.name.target_name, h)
+
+        format!("{}-{}-{:08x}", self.name.package_name, self.name.target_name, h)
+    }
+
+    /// Returns the name of the `.llbc` file to use for this artifact.
+    pub fn llbc_file_name(&self) -> String {
+        format!("{}.llbc", self.artifact_slug())
     }
 }
 

tools/hermes/tests/fixtures/cfg_blind_spot/expected_status.txt

@@ -0,0 +1 @@
+failure

tools/hermes/tests/fixtures/cfg_blind_spot/expected_stderr.txt

@@ -0,0 +1 @@
+Charon failed with status

tools/hermes/tests/fixtures/cfg_blind_spot/source/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "cfg_blind_spot"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"

tools/hermes/tests/fixtures/cfg_blind_spot/source/src/lib.rs

@@ -0,0 +1,6 @@
+#[cfg(target_os = "haiku")]
+mod ghost {
+    /// ```lean
+    /// ```
+    pub fn hidden() {}
+}

tools/hermes/tests/fixtures/external_path_dep/extra.rs

@@ -0,0 +1,3 @@
+/// ```lean
+/// ```
+pub fn foo() {}

tools/hermes/tests/fixtures/external_path_dep/hermes.toml

@@ -0,0 +1,5 @@
+[[artifact]]
+package = "external_path_dep"
+target = "external_path_dep"
+should_exist = true
+kind = "llbc"

tools/hermes/tests/fixtures/external_path_dep/source/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "external_path_dep"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"

tools/hermes/tests/fixtures/external_path_dep/source/src/lib.rs

@@ -0,0 +1,2 @@
+#[path = "../../../extra.rs"]
+mod extra;

tools/hermes/tests/fixtures/hidden_syntax_error/expected_status.txt

@@ -0,0 +1 @@
+failure

tools/hermes/tests/fixtures/hidden_syntax_error/expected_stderr.txt

@@ -0,0 +1 @@
+error

tools/hermes/tests/fixtures/hidden_syntax_error/source/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "hidden_syntax_error"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"

tools/hermes/tests/fixtures/hidden_syntax_error/source/src/lib.rs

@@ -0,0 +1,4 @@
+#[cfg(all())]
+mod broken {
+     fn syntax_error( {  // Missing closing parenthesis
+}

tools/hermes/tests/fixtures/macro_blind_spot/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/macro_blind_spot/source/Cargo.toml

@@ -2,3 +2,6 @@
 name = "macro_blind_spot"
 version = "0.1.0"
 edition = "2021"
+
+[lib]
+path = "src/lib.rs"

tools/hermes/tests/fixtures/macro_blind_spot/source/src/hidden.rs

@@ -0,0 +1,3 @@
+/// ```lean
+/// ```
+pub fn foo() {}

tools/hermes/tests/fixtures/macro_blind_spot/source/src/lib.rs

@@ -1,9 +1,2 @@
-macro_rules! make_proof {
-    () => {
-        /// ```lean
-        /// theorem hidden_proof : True := trivial
-        /// ```
-        pub fn hidden_proof() {}
-    }
-}
-make_proof!();
+macro_rules! gen_mod { ($n:ident) => { mod $n; } }
+gen_mod!(hidden);

tools/hermes/tests/fixtures/map_canonical_mismatch/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/map_canonical_mismatch/expected_stderr.txt

@@ -1 +1 @@
-Error: No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.
+No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.

tools/hermes/tests/fixtures/map_external_dep/expected_stderr.txt

@@ -1 +1 @@
-[External Error] external error
+Diagnostic error in charon

tools/hermes/tests/fixtures/map_macro_expansion/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/map_macro_expansion/expected_stderr.txt

@@ -1 +1 @@
-Error: No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.
+No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.

tools/hermes/tests/fixtures/map_mixed_diagnostics/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/map_mixed_diagnostics/expected_stderr.txt

@@ -1 +1 @@
-Error: No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.
+No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.

tools/hermes/tests/fixtures/map_relative_path/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/map_relative_path/expected_stderr.txt

@@ -1 +1 @@
-Error: No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.
+No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.

tools/hermes/tests/fixtures/map_std_lib/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/map_std_lib/expected_stderr.txt

@@ -1 +1 @@
-Error: No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.
+No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.

tools/hermes/tests/fixtures/map_std_library/expected_stderr.txt

@@ -1 +1 @@
-[External Error] std error
+Diagnostic error in charon

tools/hermes/tests/fixtures/map_symlinked_file/expected_stderr.txt

@@ -1,6 +1 @@
-  × something bad
-   ╭─[[PROJECT_ROOT]/src/untransformed.rs:1:1]
- 1 │ pub fn untouched() {}
-   · ─────┬────
-   ·      ╰── oops
-   ╰────
+Diagnostic error in charon

tools/hermes/tests/fixtures/map_workspace_path_dep/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/map_workspace_path_dep/expected_stderr.txt

@@ -1 +1 @@
-Error: No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.
+No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.

tools/hermes/tests/fixtures/no_specs/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/orphaned_entry/hermes.toml

@@ -0,0 +1,5 @@
+[[artifact]]
+package = "orphaned_entry"
+target = "orphaned_entry"
+should_exist = true
+kind = "llbc"

tools/hermes/tests/fixtures/orphaned_entry/source/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "orphaned_entry"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"

tools/hermes/tests/fixtures/orphaned_entry/source/src/lib.rs

@@ -0,0 +1,3 @@
+/// ```lean
+/// ```
+fn private_helper() {}

tools/hermes/tests/fixtures/split_personality_mod/hermes.toml

@@ -0,0 +1,11 @@
+[[artifact]]
+package = "split_personality_mod"
+target = "split_personality_mod" # The lib target name
+should_exist = true
+kind = "llbc"
+
+[[artifact]]
+package = "split_personality_mod"
+target = "split_personality_mod"
+should_exist = true
+kind = "lean"

tools/hermes/tests/fixtures/split_personality_mod/source/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "split_personality_mod"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"

tools/hermes/tests/fixtures/split_personality_mod/source/src/a.rs

@@ -0,0 +1,3 @@
+/// ```lean
+/// ```
+pub fn foo() {}

tools/hermes/tests/fixtures/split_personality_mod/source/src/lib.rs

@@ -0,0 +1,3 @@
+mod a;
+#[path = "a.rs"]
+mod b;

tools/hermes/tests/fixtures/warnings_vs_errors/expected_status.txt

@@ -1 +1 @@
-failure
+success

tools/hermes/tests/fixtures/warnings_vs_errors/expected_stderr.txt

@@ -1 +1 @@
-Error: No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.
+No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.