[anneal] Update integration tests for Nix

anneal/flake.nix

@@ -596,13 +596,32 @@ EOF
 
           leanBuild = self.packages.${system}.aeneas-compiled;
           rustToolchain = self.packages.${system}.rust-toolchain;
+          leanToolchain = self.packages.${system}.lean-toolchain;
+          aeneasUnpacked = self.packages.${system}.aeneas-unpacked;
 
           buildPhase = ''
-            # 1. Recreate the staging directory layout
+            # 1. Recreate the staging directory layout recursively.
+            #
+            # Why: Since we copy from multiple read-only Nix store paths, we must
+            # recursively set write permissions after each copy. Otherwise, subsequent
+            # copies would crash with `Permission denied` when writing into newly created
+            # read-only chroot folders.
             mkdir -p $TMPDIR/dist_staging
+
             cp -r $leanBuild/* $TMPDIR/dist_staging/
+            chmod -R +w $TMPDIR/dist_staging
+
             cp -r $rustToolchain/* $TMPDIR/dist_staging/
             chmod -R +w $TMPDIR/dist_staging
+
+            cp -r $leanToolchain/* $TMPDIR/dist_staging/
+            chmod -R +w $TMPDIR/dist_staging
+
+            # Copy precompiled Aeneas and Charon binaries from the unpacked release
+            cp $aeneasUnpacked/aeneas $TMPDIR/dist_staging/
+            cp $aeneasUnpacked/charon $TMPDIR/dist_staging/
+            cp $aeneasUnpacked/charon-driver $TMPDIR/dist_staging/
+            chmod -R +w $TMPDIR/dist_staging
 
             # 2. Un-Nixify staging binaries recursively to make them relocatable.
             #
@@ -619,7 +638,13 @@ EOF
                 if patchelf --print-interpreter "$file" >/dev/null 2>&1; then
                   patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 "$file" || true
                 fi
-                patchelf --set-rpath "" "$file" || true
+                # Set relative RPATH pointing to our relocatable toolchain library folders.
+                #
+                # Why: Executables (such as `charon-driver`) require shared compiler
+                # runtime libraries (like `librustc_driver.so`) to execute. We set their RPATH
+                # to use the `$ORIGIN` dynamic linker variable, enabling them to locate
+                # their shared libraries chroot-relatively regardless of the install directory.
+                patchelf --set-rpath '$ORIGIN/lib:$ORIGIN/lib/lean' "$file" || true
                 strip "$file" || true
               fi
             done
@@ -679,6 +704,76 @@ EOF
           '';
         };
 
+        # Standard sandboxed check that compiles the cargo-anneal Rust binary
+        # and executes its integration tests completely offline.
+        # It mounts the precompiled relocatable Zstd toolchain in the store
+        # and feeds it locally via the ANNEAL_TEST_LOCAL_ARCHIVE environment variable.
+        checks.integration-tests = pkgs.stdenv.mkDerivation {
+          pname = "cargo-anneal-integration-tests";
+          version = "0.1.0";
+
+          # Use the Aeneas Cargo project directory as source
+          src = ./.;
+
+          nativeBuildInputs = with pkgs; [
+            cargo
+            rustc
+            git
+            zstd
+            gnutar
+            graphviz
+            openssl
+            pkg-config
+            cacert
+            steam-run
+          ];
+
+          buildInputs = with pkgs; [
+            openssl
+          ];
+
+          # Precompiled monolithic Zstd toolchain package in the Nix store
+          omnibusArchive = self.packages.${system}.omnibus-archive;
+
+          # Set up CARGO_HOME and cache directories inside the writeable sandbox
+          CARGO_HOME = "/build/.cargo";
+          RUSTUP_HOME = "/build/.rustup";
+
+          # OpenSSL package mapping for cargo pkg-config
+          PKG_CONFIG_PATH = "${pkgs.openssl.dev}/lib/pkgconfig";
+
+          buildPhase = ''
+            export HOME=$TMPDIR
+
+            # Feed the absolute Nix store path of the precompiled relocatable Zstd
+            # archive to the test process. The integration test harness reads this
+            # variable and dynamically forwards it via `--local-archive` CLI flags.
+            export ANNEAL_TEST_LOCAL_ARCHIVE="$omnibusArchive"
+
+            # We must use the vendored-sources config to compile offline
+            # from local crates.
+            mkdir -p .cargo
+            cat <<EOF > .cargo/config.toml
+[source.crates-io]
+replace-with = "vendored-sources"
+
+[source.vendored-sources]
+directory = "vendor"
+EOF
+
+            # Run cargo test offline inside the hermetic sandbox!
+            # We filter to only run integration tests to keep execution scoped.
+            echo "Running cargo integration tests..."
+            steam-run cargo test --test integration --offline -- --nocapture
+          '';
+
+          installPhase = ''
+            # Checks only need to write a dummy successful output file to the store
+            echo "Integration tests completed successfully!" > $out
+          '';
+        };
+
+
 
 
 

anneal/src/aeneas.rs

@@ -415,21 +415,15 @@ pub fn generate_lean_workspace(roots: &LockedRoots, artifacts: &[AnnealArtifact]
         // Change name to anneal_verification
         manifest["name"] = serde_json::Value::String("anneal_verification".to_string());
 
-        // Read actual HEAD commit of Aeneas in toolchain
         let toolchain_aeneas_dir = toolchain.root.join("backends").join("lean");
-        let output = Command::new("git")
-            .args(["rev-parse", "HEAD"])
-            .current_dir(&toolchain_aeneas_dir)
-            .output()
-            .context("Failed to run `git rev-parse HEAD` in toolchain Aeneas")?;
 
-        if !output.status.success() {
-            bail!("`git rev-parse HEAD` failed in toolchain Aeneas");
-        }
-        let aeneas_rev = String::from_utf8(output.stdout)
-            .context("Failed to parse git output")?
-            .trim()
-            .to_string();
+        // Use the statically pinned compile-time revision of Aeneas.
+        //
+        // Why: In our hermetic relocatable toolchain, all Aeneas version assets
+        // are strictly locked and precompiled in the store. Wiping out unstable `.git` 
+        // directories inside the FOD prevents dynamic `git rev-parse` executions from 
+        // succeeding. We safely reuse the static build revision directly.
+        let aeneas_rev = env!("ANNEAL_AENEAS_REV").to_string();
 
         // Inject aeneas dependency
         let aeneas_dep = serde_json::json!({
@@ -488,6 +482,21 @@ pub fn generate_lean_workspace(roots: &LockedRoots, artifacts: &[AnnealArtifact]
             bail!("Failed to copy Aeneas directory from toolchain to workspace");
         }
 
+        // Initialize git repository in the copied Aeneas directory.
+        //
+        // Why: The precompiled relocatable toolchain does not contain a `.git` folder.
+        // To prevent `git remote add` from searching upwards and hitting the host's 
+        // git repository (causing `remote origin already exists` errors), we explicitly 
+        // initialize the copied folder as a standalone Git repository inside the sandbox.
+        let status = Command::new("git")
+            .args(["init", "-b", "main", "-q"])
+            .current_dir(&user_aeneas_dir)
+            .status()
+            .context("Failed to run `git init` in Aeneas clone")?;
+        if !status.success() {
+            bail!("`git init` failed in Aeneas clone");
+        }
+
         // Add Git remote 'origin' to match manifest
         let status = Command::new("git")
             .args([