[hermes] Roll prebuilts

.github/actions/cache/action.yml

@@ -20,7 +20,7 @@ runs:
   steps:
     - name: Restore Cache
       if: inputs.mode == 'restore'
-      uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+      uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
       id: cache
       with:
         path: ~/.cargo/

.github/workflows/hermes.yml

@@ -28,7 +28,7 @@ env:
 jobs:
   hermes_tests:
     name: Hermes Tests
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04-64core
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
@@ -49,7 +49,7 @@ jobs:
         run: |
           set -eo pipefail
           CHARON_TOOLCHAIN="$(cargo metadata --no-deps --format-version 1 \
-            | jq -r '.packages[] | select(.name == "cargo-hermes") | .metadata.hermes.dependencies.charon.rust_toolchain')"
+            | jq -r '.packages[] | select(.name == "cargo-hermes") | .metadata.build_rs.charon_rust_toolchain')"
           rustup toolchain install "$CHARON_TOOLCHAIN"
 
       - name: Install elan (Lean toolchain manager)

tools/hermes/Cargo.toml

@@ -69,13 +69,13 @@ regex.workspace = true
 strip-ansi-escapes = "0.2.1"
 similar = "2.7.0"
 
-[package.metadata.build-rs]
+[package.metadata.build_rs]
 
 # The commit hash of the Aeneas repository to use.
 #
 # FIXME: Add a CI step to verify that this commit exists and matches the
 # toolchain version.
-aeneas_rev = "5918d4719139b5e5ae6e7b63f584b036620b41b7"
+aeneas_rev = "1180be60c7a0e642cb442bfe90fe5cd8c1bb853f"
 
 # 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.
@@ -94,27 +94,31 @@ lean_toolchain = "leanprover/lean4:v4.28.0-rc1"
 # version/commit ID once that's supported
 charon_version = "0.1.174"
 
+# The Rust toolchain required by Charon.
+#
+# FIXME(#3165):
+# - Roll this from `tools/roll-pinned-prebuilts.py`
+# - Auto-install via `rustup` during `cargo hermes setup`
+charon_rust_toolchain = "nightly-2026-02-07"
+
 [package.metadata.hermes.dependencies.aeneas]
 # The per-commit release tag from AeneasVerif/charon
-tag = "build-2026.03.24.085418-5918d4719139b5e5ae6e7b63f584b036620b41b7"
+tag = "build-2026.03.29.102514-1180be60c7a0e642cb442bfe90fe5cd8c1bb853f"
 
 [package.metadata.hermes.dependencies.aeneas.checksums]
-linux-x86_64 = "fd706bf0f39701953d9d8734e9b0a9b8a6c9e71111006d093516748974a0d09a"
-linux-x86_64-aeneas = "1ed68728e18299ba961bc76c0c4897e582fdcfe30ec9b01919e250dc3cb6e65d"
+linux-x86_64 = "8224c76225329c8852e5a8cacf21fee9dc8bf93141a2a9a6ee2a52e3cfc2213f"
+linux-x86_64-aeneas = "0efc2c1c2f695e8e8fc268e6d3aaa20b7bf0a52790250f6ac45dd5f261d52a82"
 linux-x86_64-charon = "bcdc1ef536f863f21367973bd639e5557d36872cd9135d4b13ff84c2bc6df836"
 linux-x86_64-charon-driver = "20379b2051dd51dbea8d720e4041d55afe9241b95ab911e3b06492110450ecd0"
-macos-aarch64 = "d8284bf025cb768aa24cf49bdb66d6723f3c266d9ac95870bd5099d7db677e64"
-macos-aarch64-aeneas = "85f9bbda808c764095fae086e35214e485f40e4c9666f6b84916481e5c7263f8"
+macos-aarch64 = "7a5e9ded37dd21b288dffc68686ea4d254864c7a6b58a49d0bddab44d721114e"
+macos-aarch64-aeneas = "079a6565a1b5ec142548e50cc32db25ce05ae9ee97ee7148da2cb80d7286bd4e"
 macos-aarch64-charon = "6510ace82180cd78875b0631638a200d8e55bc9090c9372ea1dc8eb08511b6fb"
 macos-aarch64-charon-driver = "3c11fcb6c5cd65cd14d9747c7f8ddd1522b608a1e79041c907cb79d3118054b2"
-macos-x86_64 = "72ab5f3a22f7e666acd4c954600f4d963e34e22b900f222ce26b267939a0b4d2"
-macos-x86_64-aeneas = "72a9078abeb9c989f07da25a7f541f01e0ad62214a9475e27d24cf58ebd8a740"
+macos-x86_64 = "a909c3aa7813dd5f32b481d0c96e2b5ea3a729fa1898470b993055e778576459"
+macos-x86_64-aeneas = "7a001aa2b9f786a3978a25a68291dd0f56c0c4f069b59b782f7fb84ab206a49e"
 macos-x86_64-charon = "926c5ff8495c19b7a6f3aff1a3861970bae11bd374cf114ac3924a27bcae9ee7"
 macos-x86_64-charon-driver = "03e6617fe122f29111bf16538a5ba8f0beac6698ce473d99069439d30fa552e8"
 
-[package.metadata.hermes.dependencies.charon]
-rust_toolchain = "nightly-2025-01-26"
-
 [[test]]
 name = "integration"
 harness = false

tools/hermes/build.rs

@@ -17,18 +17,19 @@ fn main() {
     let cargo_toml: toml::Value =
         toml::from_str(&cargo_toml_content).expect("failed to parse Cargo.toml");
 
-    // We expect the metadata to be under `[package.metadata.build-rs]`.
+    // We expect the metadata to be under `[package.metadata.build_rs]`.
     let build_rs_metadata = cargo_toml
         .get("package")
         .and_then(|p| p.get("metadata"))
-        .and_then(|m| m.get("build-rs"))
-        .expect("Cargo.toml must have [package.metadata.build-rs] section");
+        .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", "HERMES_AENEAS_REV"),
         ("lean_toolchain", "HERMES_LEAN_TOOLCHAIN"),
         ("charon_version", "HERMES_CHARON_EXPECTED_VERSION"),
+        ("charon_rust_toolchain", "HERMES_CHARON_RUST_TOOLCHAIN"),
     ];
 
     for (key, env_var) in vars {

tools/hermes/src/charon.rs

@@ -288,10 +288,7 @@ fn check_charon_version(toolchain: &crate::setup::Toolchain) -> Result<()> {
 /// installed via rustup. If it is missing, we provide a helpful error message
 /// with the installation command.
 fn check_rustup_toolchain() -> Result<()> {
-    // FIXME: We should probably parse this from Charon's metadata or a central
-    // place. For now, it's pinned to a specific nightly in Charon's build.
-    // In the future, Hermes could also manage the rustup toolchain.
-    let nightly_version = "nightly-2025-01-26";
+    let nightly_version = env!("HERMES_CHARON_RUST_TOOLCHAIN");
 
     let output = Command::new("rustup")
         .args(["toolchain", "list"])

tools/hermes/tests/fixtures/expand_output/expected-aeneas.stdout

@@ -32,7 +32,8 @@ set_option maxHeartbeats 1000000
 namespace expand_output
 
 /-- [expand_output::foo]:
-    Source: 'src/lib.rs', lines 3:0-3:15 -/
+    Source: 'src/lib.rs', lines 3:0-3:15
+    Visibility: public -/
 def foo : Result Unit := do
   ok ()
 

tools/hermes/tests/fixtures/expand_output/expected-all.stdout

@@ -32,7 +32,8 @@ set_option maxHeartbeats 1000000
 namespace expand_output
 
 /-- [expand_output::foo]:
-    Source: 'src/lib.rs', lines 3:0-3:15 -/
+    Source: 'src/lib.rs', lines 3:0-3:15
+    Visibility: public -/
 def foo : Result Unit := do
   ok ()
 

tools/hermes/tests/fixtures/extern_never_verified/out.txt

@@ -14,12 +14,14 @@ set_option maxHeartbeats 1000000
 namespace extern_never_verified
 
 /-- [extern_never_verified::S]
-    Source: 'src/lib.rs', lines 12:0-12:13 -/
+    Source: 'src/lib.rs', lines 12:0-12:13
+    Visibility: public -/
 @[reducible]
 def S := Unit
 
 /-- [extern_never_verified::SafeArray]
-    Source: 'src/lib.rs', lines 50:0-52:1 -/
+    Source: 'src/lib.rs', lines 50:0-52:1
+    Visibility: public -/
 structure SafeArray (N : Std.Usize) where
   data : Array Std.U8 N
 
@@ -46,27 +48,32 @@ noncomputable section
 namespace extern_never_verified
 
 /-- [extern_never_verified::{extern_never_verified::S}::bar]:
-    Source: 'src/lib.rs', lines 17:4-19:5 -/
+    Source: 'src/lib.rs', lines 17:4-19:5
+    Visibility: public -/
 def S.bar (x : Std.U32) : Result Std.U32 := do
   ok x
 
 /-- [extern_never_verified::inner::{extern_never_verified::S}::baz]:
-    Source: 'src/lib.rs', lines 28:8-30:9 -/
+    Source: 'src/lib.rs', lines 28:8-30:9
+    Visibility: public -/
 def inner.S.baz (x : Std.U32) : Result Std.U32 := do
   ok x
 
 /-- [extern_never_verified::{extern_never_verified::SafeArray<N>}::len]:
-    Source: 'src/lib.rs', lines 61:4-63:5 -/
+    Source: 'src/lib.rs', lines 61:4-63:5
+    Visibility: public -/
 def SafeArray.len {N : Std.Usize} (self : SafeArray N) : Result Std.Usize := do
   ok N
 
 /-- [extern_never_verified::diverge]:
-    Source: 'src/lib.rs', lines 72:0-74:1 -/
+    Source: 'src/lib.rs', lines 72:0-74:1
+    Visibility: public -/
 def diverge : Result Never := do
   fail panic
 
 /-- [extern_never_verified::die]:
-    Source: 'src/lib.rs', lines 82:0-84:1 -/
+    Source: 'src/lib.rs', lines 82:0-84:1
+    Visibility: public -/
 def die (x : Std.U32) : Result (Never × Std.U32) := do
   fail panic
 
@@ -87,15 +94,18 @@ set_option maxHeartbeats 1000000
 open extern_never_verified
 
 /-- [extern_never_verified::a::b::foo]:
-    Source: 'src/lib.rs', lines 6:8-8:9 -/
+    Source: 'src/lib.rs', lines 6:8-8:9
+    Visibility: public -/
 axiom a.b.foo : Std.U32 → Result Std.U32
 
 /-- [extern_never_verified::ffi::ext_fn]:
-    Source: 'src/lib.rs', lines 40:8-40:37 -/
+    Source: 'src/lib.rs', lines 40:8-40:37
+    Visibility: public -/
 axiom ffi.ext_fn : Std.U32 → Result Std.U32
 
 /-- [extern_never_verified::ffi::diverge]:
-    Source: 'src/lib.rs', lines 46:8-46:30 -/
+    Source: 'src/lib.rs', lines 46:8-46:30
+    Visibility: public -/
 axiom ffi.diverge : Result Never
 
 

tools/hermes/tests/fixtures/setup_e2e/expected.stdout

@@ -1,2 +1,2 @@
-Downloading: http://127.0.0.1:<PORT>/build-2026.03.24.085418-5918d4719139b5e5ae6e7b63f<HASH>/aeneas-linux-x86_64.tar.gz
-Successfully installed toolchain vbuild-2026.03.24.085418-5918d4719139b5e5ae6e7b63f<HASH>
+Downloading: http://127.0.0.1:<PORT>/build-2026.03.29.102514-1180be60c7a0e642cb442bfe<HASH>/aeneas-linux-x86_64.tar.gz
+Successfully installed toolchain vbuild-2026.03.29.102514-1180be60c7a0e642cb442bfe<HASH>

tools/hermes/tests/fixtures/setup_repair/hermes.toml

@@ -44,4 +44,4 @@ args = ["setup"]
 
 [[test.phases]]
 name = "Verify aeneas is repaired"
-action = "assert_toolchain_binary aeneas 1ed68728e18299ba961bc76c0c4897e582fdcfe30ec9b01919e250dc3cb6e65d"
+action = "assert_toolchain_binary aeneas 0efc2c1c2f695e8e8fc268e6d3aaa20b7bf0a52790250f6ac45dd5f261d52a82"

tools/hermes/tests/fixtures/type_features/expected.stderr

@@ -116,5 +116,5 @@ Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
 Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66
 Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40
 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71
-Called from Dune__exe__Main in file "Main.ml", lines 715-716, characters 8-37
+Called from Dune__exe__Main in file "Main.ml", lines 726-727, characters 8-37
 

tools/hermes/tests/fixtures/unions/expected.stderr

@@ -18,5 +18,5 @@ Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
 Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66
 Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40
 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71
-Called from Dune__exe__Main in file "Main.ml", lines 715-716, characters 8-37
+Called from Dune__exe__Main in file "Main.ml", lines 726-727, characters 8-37
 

tools/hermes/tests/integration.rs

@@ -1371,8 +1371,8 @@ fn run_toolchain_versioning_test(path: &Path) -> datatest_stable::Result<()> {
     let metadata = cargo_toml
         .get("package")
         .and_then(|p| p.get("metadata"))
-        .and_then(|m| m.get("build-rs"))
-        .expect("Cargo.toml must have [package.metadata.build-rs]");
+        .and_then(|m| m.get("build_rs"))
+        .expect("Cargo.toml must have [package.metadata.build_rs]");
 
     let expected_rev = metadata.get("aeneas_rev").and_then(|v| v.as_str()).unwrap();
     let expected_toolchain = metadata.get("lean_toolchain").and_then(|v| v.as_str()).unwrap();
@@ -2012,8 +2012,8 @@ fn get_expected_charon_version() -> String {
     let metadata = cargo_toml
         .get("package")
         .and_then(|p| p.get("metadata"))
-        .and_then(|m| m.get("build-rs"))
-        .expect("Cargo.toml must have [package.metadata.build-rs]");
+        .and_then(|m| m.get("build_rs"))
+        .expect("Cargo.toml must have [package.metadata.build_rs]");
 
     metadata.get("charon_version").and_then(|v| v.as_str()).unwrap().to_string()
 }

tools/hermes/tools/roll-pinned-prebuilts.py

@@ -246,11 +246,11 @@ def update_cargo_toml(aeneas_meta, charon_meta, dry_run=False):
     try:
         metadata = doc["package"]["metadata"]
 
-        # Update the build-rs section, which defines the environment variables
+        # Update the build_rs section, which defines the environment variables
         # injected into the Hermes build process.
-        metadata["build-rs"]["aeneas_rev"] = aeneas_meta["commit"]
-        metadata["build-rs"]["lean_toolchain"] = aeneas_meta["lean_toolchain"]
-        metadata["build-rs"]["charon_version"] = charon_meta["version"]
+        metadata["build_rs"]["aeneas_rev"] = aeneas_meta["commit"]
+        metadata["build_rs"]["lean_toolchain"] = aeneas_meta["lean_toolchain"]
+        metadata["build_rs"]["charon_version"] = charon_meta["version"]
 
         # Update the hermes.dependencies section, which defines the download URLs
         # and checksums used by the 'cargo hermes setup' command.