[anneal][release] Publish Nix-built toolchain archives

.github/workflows/anneal.yml

@@ -30,6 +30,44 @@ env:
 
 jobs:
 
+  static_checks:
+    name: Anneal Static Checks
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          persist-credentials: false
+
+      - name: Install stable Rust
+        uses: dtolnay/rust-toolchain@e97e2d8cc328f1b50210efc529dca0028893a2d9 # zizmor: ignore[superfluous-actions]
+        with:
+          toolchain: stable
+
+      - name: Test Anneal support scripts
+        run: |
+          set -euo pipefail
+          export PYTHONDONTWRITEBYTECODE=1
+          python3 -m py_compile \
+            anneal/tools/check-release-pr-files.py \
+            anneal/tools/test_exocrate_metadata_helpers.py \
+            anneal/tools/test_release_pr_files.py \
+            anneal/tools/collect-release-archive-metadata.py \
+            anneal/tools/update-exocrate-metadata.py \
+            anneal/v2/tests/test_prune_lake_cache.py \
+            anneal/v2/prune-lake-cache.py \
+            anneal/v2/rewrite-lake-vendor.py
+          python3 -m unittest discover -s anneal/tools -p 'test_*.py'
+          python3 -m unittest discover -s anneal/v2/tests -p 'test_*.py'
+          bash anneal/tools/check-release-flow-dry-run.sh
+
+      - name: Install Nix
+        uses: DeterminateSystems/determinate-nix-action@441b9e401ac050c38a07d8313748c5c2d17e8aff # v3.6.1
+
+      - name: Check V2 flake evaluation
+        run: bash anneal/v2/check-flake-eval.sh
+
   anneal_tests:
     name: Anneal Tests
     runs-on: ubuntu-latest
@@ -285,6 +323,14 @@ jobs:
           archive="$(readlink -f target/anneal-exocrate.tar.zst)"
           rm target/anneal-exocrate.tar.zst
           cp "$archive" target/anneal-exocrate.tar.zst
+          archive_size="$(python3 -c 'import os, sys; print(os.path.getsize(sys.argv[1]))' target/anneal-exocrate.tar.zst)"
+          max_github_release_asset_size=2147483647
+          printf 'Built anneal-exocrate.tar.zst (%s bytes)\n' "$archive_size"
+          if [ "$archive_size" -gt "$max_github_release_asset_size" ]; then
+            echo "::error::anneal-exocrate.tar.zst is ${archive_size} bytes, which exceeds GitHub's ${max_github_release_asset_size}-byte release asset limit."
+            exit 1
+          fi
+          nix build "${nix_args[@]}" .#omnibus-archive-layout-check --no-link
         working-directory: anneal/v2
 
       # Re-enable the AppArmor namespace restriction to restore the runner host's default security posture.
@@ -388,7 +434,7 @@ jobs:
       # https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/collaborating-on-repositories-with-code-quality-features/troubleshooting-required-status-checks#handling-skipped-but-required-checks
       if: failure()
       runs-on: ubuntu-latest
-      needs: [anneal_tests, verify_examples, v2_nix_cache, v2]
+      needs: [static_checks, anneal_tests, verify_examples, v2_nix_cache, v2]
       steps:
         - name: Mark the job as failed
           run: exit 1

anneal/Cargo.toml

@@ -107,60 +107,6 @@ aeneas_rev = "42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4"
 # The Lean toolchain version to use. This must match the version of Lean used
 # by Aeneas in the `lean-toolchain` file in the commit above.
 lean_toolchain = "leanprover/lean4:v4.30.0-rc2"
-
-# The Rust toolchain required by Charon.
-#
-# FIXME(#3165):
-# - Roll this from `tools/roll-pinned-prebuilts.py`
-# - Auto-install via `rustup` during `cargo anneal setup`
-charon_rust_toolchain = "nightly-2026-02-07"
-
-[package.metadata.anneal.dependencies.aeneas]
-# The per-commit release tag from AeneasVerif/charon
-tag = "build-2026.04.07.112215-42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4"
-
-[package.metadata.anneal.dependencies.aeneas.checksums]
-linux-aarch64 = "a250ef38be509f69ff4c5fb35eded165255fae6f659172837cd3053978de863f"
-linux-x86_64 = "a448682a154590e65b0794c42487583352375fc04bdd6b2418324f6ecafcc94f"
-macos-aarch64 = "1dbeaafe875bec173e0d2cf3c6bbfa63d6c591d3ec554bafb0d2c3c52e1ded6d"
-macos-x86_64 = "e977c28b72ec041d4f13df0acc77ab59040743a9659b4eefffb71eb420cd5df6"
-
-[package.metadata.anneal.dependencies.rust]
-tag = "nightly-2026-02-07"
-date = "2026-02-07"
-
-[package.metadata.anneal.dependencies.rust.checksums]
-linux-x86_64-rustc = "f58a30c9fa9add81d0e99209fd960aa429f0a4ff7a37f9044e5d9eb1a598c925"
-linux-x86_64-rust-std = "1b06ef4654bcacd06c4f14094ca9bfe8d8bd4129c96b6b6594e3a9cf0d0214d2"
-linux-x86_64-rustc-dev = "7f120343b7153e166261558b07efb8081781cfdd617e5a59ac0e144cbbe9b3df"
-linux-x86_64-llvm-tools-preview = "4ca90ae6805121c591bb35998c12c69e6f77f9f7cc93edd72a26dfc017f0c098"
-linux-x86_64-miri-preview = "c90b56d0c094d6599f827b5feebb6a105af536b3540924fa373356a38f296d33"
-linux-x86_64-cargo = "414e784933c550d7b7c88bbaaa0578609c2c618c9d664ae9a966ce914c54b383"
-
-linux-aarch64-rustc = "cd781f03a07803fa6048e9848992c88d5b7311a5570e702754b8fc271e780a79"
-linux-aarch64-rust-std = "c7e9d1d54ccd6a9426be2de7b1e22d5a6eb4c0e18d0cff5c2dfe5e6a836d1e61"
-linux-aarch64-rustc-dev = "552302886c5a3ff8f97d55838efd48ec7876ccfc544f334affa6da59a159fc57"
-linux-aarch64-llvm-tools-preview = "1aa7233de3856fb213b7c1927e3d3378b5484a18adbb631bc116ff63fbbb151e"
-linux-aarch64-miri-preview = "de65c893bbcf186150204c27de29b408d6bbc59a49b6327119461cefafbc1b42"
-linux-aarch64-cargo = "c85804bd8644035d7981b28e3832ac54f7cbcce1e406319b32dff6ca55d0305c"
-
-macos-x86_64-rustc = "c17ebb6d433fd9cd09b6ca59c2e8c18114e0fd54917997a1b6dcaa1187d0dd23"
-macos-x86_64-rust-std = "8d3f34cc047d2daa578615e9ade5b9e80cda2b1a9d14677f1d901d52e840ea35"
-macos-x86_64-rustc-dev = "817b2b71d70b07f3f5dfb897b47598b1d64d2d789a71a1250d2123d53262adc5"
-macos-x86_64-llvm-tools-preview = "506df88302ff5bb3e652b743ceda9284e7a7fb96fd4c2b3c159a4bdacd815f22"
-macos-x86_64-miri-preview = "19f717a65f4c07065b732f43bd14e10303108fc68194e3b7d8d2d574736e4735"
-macos-x86_64-cargo = "3ee21dcd2266293458d58c417d3b0aa351bb4d567d20ed15552f992a6f2f3fe5"
-
-macos-aarch64-rustc = "7f3e916728eaecf5e32ec98a132d21aa677f2f9a9c08527ebbd1025755fda537"
-macos-aarch64-rust-std = "888548770827ece8c90fdc8efcb3a3fab0c38823d1f163535aaeec2f325c8001"
-macos-aarch64-rustc-dev = "3bed787e9d2b8dc21691bcb33ded3fe9b45f57f46d50fc82c4e2d7c6ea35f519"
-macos-aarch64-llvm-tools-preview = "df48a63ebccf2b983b450390908a58e8955bb6d38f8a84ad68dbcef3815aa9c9"
-macos-aarch64-miri-preview = "c99b5930e32cdddaa10fb08af3235fec9fede2327b9e4704591bae41c9e329d7"
-macos-aarch64-cargo = "6615a0d863d962e2479ce49b3312516abdbdf2403fd3796590cc5823f35d2202"
-
-rust-src = "404582b3ef31783b3ee390382e149736cc5d49e5b04d4d1ac39d1371a4ddedca"
-
-
 [[test]]
 name = "integration"
 harness = false

anneal/build.rs

@@ -28,12 +28,7 @@ fn main() {
         .and_then(|m| m.get("build_rs"))
         .expect("Cargo.toml must have [package.metadata.build_rs] section");
 
-    // Key in `Cargo.toml` -> Environment variable name
-    let vars = [
-        ("aeneas_rev", "ANNEAL_AENEAS_REV"),
-        ("lean_toolchain", "ANNEAL_LEAN_TOOLCHAIN"),
-        ("charon_rust_toolchain", "ANNEAL_CHARON_RUST_TOOLCHAIN"),
-    ];
+    let vars = [("aeneas_rev", "ANNEAL_AENEAS_REV"), ("lean_toolchain", "ANNEAL_LEAN_TOOLCHAIN")];
 
     for (key, env_var) in vars {
         let value = build_rs_metadata
@@ -44,39 +39,6 @@ fn main() {
         println!("cargo:rustc-env={}={}", env_var, value);
     }
 
-    // Parse [package.metadata.anneal.dependencies]
-    if let Some(anneal_metadata) = cargo_toml
-        .get("package")
-        .and_then(|p| p.get("metadata"))
-        .and_then(|m| m.get("anneal"))
-        .and_then(|h| h.get("dependencies"))
-        .and_then(|d| d.as_table())
-    {
-        for (dep_name, dep_meta) in anneal_metadata {
-            let dep_upper = dep_name.to_uppercase();
-            if let Some(tag) = dep_meta.get("tag").and_then(|t| t.as_str()) {
-                println!("cargo:rustc-env=ANNEAL_{}_TAG={}", dep_upper, tag);
-            }
-
-            if let Some(date) = dep_meta.get("date").and_then(|t| t.as_str()) {
-                println!("cargo:rustc-env=ANNEAL_{}_DATE={}", dep_upper, date);
-            }
-
-            if let Some(checksums) = dep_meta.get("checksums").and_then(|c| c.as_table()) {
-                for (platform, checksum) in checksums {
-                    if let Some(hash) = checksum.as_str() {
-                        // Standardize platform name for env var (dashes -> underscores, upper case)
-                        let env_platform = platform.replace('-', "_").to_uppercase();
-                        println!(
-                            "cargo:rustc-env=ANNEAL_{}_CHECKSUM_{}={}",
-                            dep_upper, env_platform, hash
-                        );
-                    }
-                }
-            }
-        }
-    }
-
     if let Some(exocrate_metadata) = cargo_toml
         .get("package")
         .and_then(|p| p.get("metadata"))