[anneal][v2] Add charon execution engine, expand command CLI, and integration tests

anneal/v2/examples/simple.rs

@@ -0,0 +1,7 @@
+pub fn add(left: usize, right: usize) -> usize {
+    left + right
+}
+
+fn main() {
+    println!("Hello, world! {}", add(1, 2));
+}

anneal/v2/src/diagnostics.rs

@@ -242,6 +242,7 @@ impl DiagnosticMapper {
     ///    bytes.
     /// 3. Anneal calls this method to print the error onto the Rust file
     ///    canvas.
+    #[allow(dead_code)]
     pub fn render_raw<F>(
         &mut self,
         file_name: &str,

anneal/v2/src/main.rs

@@ -7,8 +7,16 @@
 // This file may not be copied, modified, or distributed except according to
 // those terms.
 
+use anyhow::Context as _;
 use clap::Parser as _;
 
+mod charon;
+mod diagnostics;
+mod resolve;
+mod scanner;
+mod setup;
+mod util;
+
 /// Anneal: A Literate Verification Toolchain
 #[derive(clap::Parser, Debug)]
 #[command(name = "cargo-anneal", version, about, long_about = None)]
@@ -21,50 +29,77 @@ struct Cli {
 enum Commands {
     /// Setup Anneal dependencies
     Setup(SetupArgs),
+    /// Expand a crate (runs Charon)
+    Expand(ExpandArgs),
+
+    /// Helper to acquire shared or exclusive locks for multi-process integration testing (dev only)
+    #[cfg(feature = "exocrate_tests")]
+    TestLockHelper {
+        /// The role to run as: 'reader-a', 'reader-b', 'writer-a', or 'reader-exclusion'
+        #[arg(long)]
+        role: String,
+        /// Path to the directory to lock
+        #[arg(long)]
+        lock_dir: std::path::PathBuf,
+        /// Path to the shared log file where lock transitions are appended
+        #[arg(long)]
+        log_file: std::path::PathBuf,
+        /// Path to the temporary synchronization signal file
+        #[arg(long)]
+        sig_file: std::path::PathBuf,
+    },
 }
 
 #[derive(clap::Parser, Debug)]
 pub struct SetupArgs {
-    /// Path to a local dependency archive to use instead of downloading.
+    /// Path to a local dependency archive to use instead of downloading
     #[arg(long, value_name = "path-to-local-archive")]
     pub local_archive: Option<std::path::PathBuf>,
 }
 
-exocrate::config! {
-    const CONFIG: Config = Config {
-        rel_dir_path: [".anneal", "toolchain"],
-        versioned_files: &["../Cargo.toml", "../Cargo.lock"],
-    };
+#[derive(clap::Parser, Debug)]
+pub struct ExpandArgs {
+    #[command(flatten)]
+    pub resolve_args: crate::resolve::Args,
+
+    /// Controls where LLBC output is placed on the filesystem
+    #[arg(long, value_name = "output-dir")]
+    pub output_dir: Option<std::path::PathBuf>,
+
+    /// Do not show compilation progress bars
+    #[arg(long)]
+    pub no_progress: bool,
 }
 
-exocrate::parse_remote_archive! {
-    const REMOTE: RemoteArchive = "Cargo.toml" [
-        (linux, x86_64),
-        (macos, x86_64),
-        (linux, aarch64),
-        (macos, aarch64),
-    ];
+fn setup(args: SetupArgs) -> anyhow::Result<()> {
+    crate::setup::run_setup(crate::setup::SetupArgs { local_archive: args.local_archive })
+        .context("Failed to setup toolchain")
 }
 
-fn setup(args: SetupArgs) {
-    let location = if std::env::var("__ANNEAL_LOCAL_DEV").is_ok() {
-        exocrate::Location::Local
-    } else {
-        exocrate::Location::UserGlobal
-    };
-    let source = match args.local_archive {
-        Some(local_archive) => exocrate::Source::Local(local_archive),
-        None => exocrate::Source::Remote(REMOTE),
-    };
-
-    let installation_dir = CONFIG
-        .resolve_installation_dir_or_install(location, source)
-        // FIXME: Implement unified error reporting (e.g., via `anyhow`).
-        .expect("failed to resolve-or-install dependencies");
-    log::info!("anneal toolchain is installed at {:?}", installation_dir);
+fn expand(args: ExpandArgs) -> anyhow::Result<()> {
+    let roots = crate::resolve::resolve_roots(&args.resolve_args)?;
+    let packages = crate::scanner::scan_workspace(&roots)?;
+    if packages.is_empty() {
+        log::warn!("No targets found to expand.");
+        return Ok(());
+    }
+    let mut locked_roots = roots.lock_run_root()?;
+    if let Some(output_dir) = args.output_dir {
+        locked_roots.llbc_override = Some(output_dir);
+    }
+    let toolchain = crate::setup::Toolchain::resolve()?;
+    let show_progress = !args.no_progress;
+    crate::charon::run_charon(
+        &args.resolve_args,
+        &toolchain,
+        &locked_roots,
+        &packages,
+        show_progress,
+    )?;
+    Ok(())
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     // Suppressing timestamps removes a source of nondeterminism that is
     // difficult to work around in integration tests.
     env_logger::builder().format_timestamp(None).init();
@@ -79,18 +114,55 @@ fn main() {
 
     match args.command {
         Commands::Setup(args) => setup(args),
+        Commands::Expand(args) => expand(args),
+
+        #[cfg(feature = "exocrate_tests")]
+        Commands::TestLockHelper { role, lock_dir, log_file, sig_file } => {
+            crate::util::run_test_lock_helper(&role, &lock_dir, &log_file, &sig_file)
+        }
     }
 }
 
 #[cfg(test)]
 mod tests {
     #[cfg(feature = "exocrate_tests")]
     #[test]
-    fn test_setup() {
+    fn test_setup_and_toolchain_paths() {
+        // 1. Run setup.
         super::setup(super::SetupArgs {
             // ASSUMPTION: Dependency builder installs archive at
             // `target/anneal-exocrate.tar.zst`.
             local_archive: Some("target/anneal-exocrate.tar.zst".into()),
         })
+        .expect("Failed to run setup");
+
+        // 2. Once setup completes successfully, resolve the toolchain.
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
+
+        // 3. Verify that all returned paths exist as directories.
+        // Note: these assertions would be more appropriate in the setup.rs module,
+        // but including them here avoids introducing multiple tests that attempt to
+        // extract the (large) anneal exocrate archive.
+        assert!(toolchain.root().is_dir(), "root is not a directory: {:?}", toolchain.root());
+        assert!(
+            toolchain.aeneas_bin_dir().is_dir(),
+            "aeneas_bin_dir is not a directory: {:?}",
+            toolchain.aeneas_bin_dir()
+        );
+        assert!(
+            toolchain.rust_sysroot().is_dir(),
+            "rust_sysroot is not a directory: {:?}",
+            toolchain.rust_sysroot()
+        );
+        assert!(
+            toolchain.rust_bin().is_dir(),
+            "rust_bin is not a directory: {:?}",
+            toolchain.rust_bin()
+        );
+        assert!(
+            toolchain.rust_lib().is_dir(),
+            "rust_lib is not a directory: {:?}",
+            toolchain.rust_lib()
+        );
     }
 }

anneal/v2/src/resolve.rs

@@ -187,10 +187,12 @@ impl<'a> LockedRoots<'a> {
         }
     }
 
+    #[allow(dead_code)]
     pub fn lean_root(&self) -> std::path::PathBuf {
         self.anneal_run_root.path.join("lean")
     }
 
+    #[allow(dead_code)]
     pub fn lean_generated_root(&self) -> std::path::PathBuf {
         self.lean_root().join("generated")
     }

anneal/v2/src/scanner.rs

@@ -91,6 +91,7 @@ impl AnnealArtifact {
     }
 
     /// Returns the name of the `.lean` spec file to use for this artifact.
+    #[allow(dead_code)]
     pub fn lean_spec_file_name(&self) -> String {
         format!("{}.lean", self.artifact_slug())
     }

anneal/v2/src/setup.rs

@@ -70,6 +70,7 @@ impl Toolchain {
         Ok(Self { root })
     }
 
+    #[allow(dead_code)]
     pub fn root(&self) -> &std::path::Path {
         &self.root
     }

anneal/v2/src/util.rs

@@ -41,6 +41,7 @@ impl DirLock {
     ///
     /// Multiple processes can hold shared locks simultaneously, but an
     /// exclusive lock will block until all shared locks are released.
+    #[allow(dead_code)]
     pub(crate) fn lock_shared(path: std::path::PathBuf) -> anyhow::Result<Self> {
         let file = Self::open_lock_file(&path)?;
         file.lock_shared()
@@ -79,6 +80,7 @@ impl DirLock {
 
 /// Walks a directory recursively and replaces string patterns inside `.trace`
 /// files. This is used to patch non-portable paths generated by Lake.
+#[allow(dead_code)]
 pub(crate) fn patch_trace_files(
     dir: &std::path::Path,
     replacements: &[(&str, &str)],

anneal/v2/tests/integration.rs

@@ -0,0 +1,49 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+use std::fs;
+use std::process::Command;
+
+#[cfg(feature = "exocrate_tests")]
+#[test]
+fn test_expand_subcommand_simple() {
+    let temp_dir = tempfile::tempdir().unwrap();
+    let output_dir = temp_dir.path().join("llbc_out");
+
+    let bin_path = std::env::var("CARGO_BIN_EXE_cargo-anneal")
+        .or_else(|_| std::env::var("CARGO_BIN_EXE_cargo_anneal"))
+        .expect("CARGO_BIN_EXE_* not set");
+
+    let mut cmd = Command::new(bin_path);
+    cmd.arg("expand").arg("--example").arg("simple").arg("--output-dir").arg(&output_dir);
+    cmd.arg("--no-progress");
+
+    cmd.env("__ANNEAL_LOCAL_DEV", "1");
+
+    let output = cmd.output().expect("failed to execute cargo-anneal");
+
+    println!("stdout: {}", String::from_utf8_lossy(&output.stdout));
+    println!("stderr: {}", String::from_utf8_lossy(&output.stderr));
+
+    assert!(output.status.success(), "cargo-anneal failed");
+
+    let mut found_llbc = false;
+    if output_dir.exists() {
+        for entry in fs::read_dir(&output_dir).unwrap() {
+            let entry = entry.unwrap();
+            let path = entry.path();
+            if path.is_file() && path.extension().map_or(false, |ext| ext == "llbc") {
+                found_llbc = true;
+                break;
+            }
+        }
+    }
+
+    assert!(found_llbc, "No .llbc file found in output directory {:?}", output_dir);
+}