Update multi-stark for hybrid CUDA scheduling

.github/workflows/nix.yml

@@ -8,6 +8,11 @@ on:
 permissions:
   contents: read
 
+# Build locally when a binary cache is temporarily unavailable.
+env:
+  NIX_CONFIG: |
+    fallback = true
+
 concurrency:
   group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
   cancel-in-progress: true
@@ -34,7 +39,7 @@ jobs:
       - uses: ./.github/actions/authenticate-github-fetches
       # Ix CLI
       - run: nix build --print-build-logs --accept-flake-config
-      - run: nix run .#ix -- --help
+      - run: nix run --accept-flake-config .#ix -- --help
       # A single invocation lets Nix schedule independent checks concurrently.
       - run: nix flake check --print-build-logs --accept-flake-config
 

Cargo.toml

@@ -56,7 +56,7 @@ libc = "0.2"
 log = "0.4"
 memmap2 = "0.9"
 mimalloc = { version = "0.1", default-features = false }
-multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "a8aab731af8d2a5e15f390cd2ef14af4fc42d7d3" }
+multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "c683c69ccb0499fc4528ece39f292f53b8c71609" }
 nom = "7.1.3"
 num-bigint = "0.4.6"
 quickcheck = "1.0.3"

crates/compile/src/compile/aux_gen/recursor.rs

@@ -2914,7 +2914,15 @@ mod tests {
         cnst: ConstantVal {
           name: rec_name.clone(),
           level_params: vec![],
-          typ: LeanExpr::sort(Level::zero()),
+          // Keep the source recursor dependent on its inductive, as a real
+          // recursor's major premise would. A bare Sort makes the stub an
+          // independent scheduler root that can compile before aux_gen
+          // replaces it with the canonical recursor.
+          typ: epi(
+            n("major"),
+            LeanExpr::cnst(ind.clone(), vec![]),
+            LeanExpr::sort(Level::zero()),
+          ),
         },
         all: all.to_vec(),
         num_params: Nat::from(0u64),
@@ -3993,8 +4001,8 @@ mod tests {
     // one (gate: `lean_env.get(rec_name).is_some()`). The minimal
     // `build_alpha_collapse_env` doesn't add the auxiliary constants Lean
     // would normally generate, so insert stub `.rec` entries here. Note: the
-    // stubs only have to exist for the gate; aux_gen replaces their contents
-    // with the regenerated value.
+    // stubs retain the inductive dependency so the scheduler runs aux_gen
+    // before compiling them; aux_gen replaces their contents.
     let all = vec![a.clone(), b.clone()];
     let _ = insert_aux_stub_rec(&mut env, &all, &a);
     let _ = insert_aux_stub_rec(&mut env, &all, &b);

flake.nix

@@ -104,7 +104,7 @@
           # Pins the Rust toolchain
           rustToolchain = fenix.packages.${system}.fromToolchainFile {
             file = ./rust-toolchain.toml;
-            sha256 = "sha256-P30Tm3O7vQAE725YtDCDHGjNrSsfZO4us11UwJGZSJo=";
+            sha256 = "sha256-p8h3Sl/YRByZfZTAKXdsvF6xEenXKrXSVvpphmZENH4=";
           };
 
           # Rust package

rust-toolchain.toml

@@ -1,4 +1,4 @@
 [toolchain]
 # The default profile includes rustc, rust-std, cargo, rust-docs, rustfmt and clippy.
 profile = "default"
-channel = "1.98"
+channel = "1.98.1"