chore: Remove alternate ZK backends

.github/workflows/bench-pr.yml

@@ -3,7 +3,7 @@
 # The base is the PR's own base branch — main for an unstacked PR, the
 # parent PR's head for a stacked one — and the report is labelled with it.
 #
-#   !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] | all) [execute]
+#   !benchmark ([aiur] [ooc] [compile] [decompile] | all) [execute]
 #   BENCH_ENVS=InitStd,Mathlib     # which compiled envs (case-insensitive, any registry env;
 #                                  #  defaults to every env for compile/decompile, InitStd
 #                                  #  for the rest)
@@ -569,23 +569,6 @@ jobs:
         with:
           name: benchmark-env-${{ matrix.params.env }}
       # ---------- PR side ----------
-      # zkVM runs build their Rust host in-run, so they need the Rust
-      # toolchain plus the backend's own toolchain and system deps.
-      - name: Set up zkVM Rust toolchain
-        if: matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1'
-        uses: $/.github/actions/setup-rust-toolchain
-        with:
-          cache-workspaces: ${{ matrix.params.backend }}
-          cache-key: ${{ matrix.params.backend }}
-      - name: Install SP1
-        if: matrix.params.backend == 'sp1'
-        uses: $/.github/actions/install-sp1
-      - name: Install Zisk
-        if: matrix.params.backend == 'zisk'
-        uses: $/.github/actions/install-zisk
-        with:
-          proving-key: false
-
       # The PR side runs first: `ix bench run` selects its constants from
       # the shared set (Ix/BenchConstants.lean), and pr.json's row names
       # become the canonical name list this run measures — the base-side
@@ -598,11 +581,6 @@ jobs:
         # the job, after the table upload.
         continue-on-error: true
         run: |
-          if [ "$BACKEND" = zisk ]; then
-            # ZisK's ASM microservices mmap with MAP_LOCKED: raise the memlock
-            # hard limit in this shell so the spawned tools inherit it.
-            sudo prlimit --pid $$ --memlock=unlimited:unlimited
-          fi
           if [ "$BACKEND" = compile ]; then
             # The compile job already measured this env's compile (same
             # runner class, binaries, and command) — reuse its row instead
@@ -855,9 +833,6 @@ jobs:
           # Cached base .ixe when the restore above hit; else the base run
           # compiles it fresh (no flag).
           [ -f "base/$BENV.ixe" ] && flags="$flags --ixe base/$BENV.ixe"
-          if [ "$BACKEND" = zisk ]; then
-            sudo prlimit --pid $$ --memlock=unlimited:unlimited
-          fi
           ix bench run --backend "$BACKEND" --env "$BENV" --mode "$MODE" \
             --repo base \
             --out "$GITHUB_WORKSPACE/base.json" $flags

.github/workflows/bencher-thresholds-reset.yml

@@ -22,7 +22,7 @@ name: Bencher thresholds reset
 #     cancel by removing it before merge. Naming convention: one label per token,
 #     `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
 #     testbed stem in Ix/Cli/BenchCmd.lean (backendSpecs):
-#     `ix-compile`, `ix-decompile`, `aiur`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
+#     `ix-compile`, `ix-decompile`, `aiur`, `ooc-check`) or
 #     `all` (the merge step expands an `all` label into every workload). Labeling
 #     requires Triage+, so PR authors from forks cannot self-queue a reset. The
 #     label shares the command/workflow name; the ref it moves is
@@ -44,7 +44,7 @@ on:
         # GitHub requires literal choice options, so this list stays static:
         # keep it (and the jobs' valid= lists below) in sync with the
         # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
-        options: [ix-compile, ix-decompile, aiur, aiur-sharded-env-check, zisk-check-execute, sp1-check-execute, ooc-check, all]
+        options: [ix-compile, ix-decompile, aiur, aiur-sharded-env-check, ooc-check, all]
       sha:
         description: "Commit to anchor to (default: HEAD)"
         required: false
@@ -78,7 +78,7 @@ jobs:
           # (backendSpecs), before its hardware suffix. Static because this
           # job runs on a cheap runner with no built `ix`; keep in sync when
           # adding a backend.
-          valid="aiur aiur-sharded-env-check ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
+          valid="aiur aiur-sharded-env-check ix-compile ix-decompile ooc-check"
           if [ "$EVENT" = workflow_dispatch ]; then
             # Reset the chosen workload(s) at the given commit; no PR scan.
             sha="${INPUT_SHA:-$HEAD_SHA}"
@@ -137,7 +137,7 @@ jobs:
           # which the merge job expands into every workload). Same static
           # list as the reset job; keep both in sync with backendSpecs in
           # Ix/Cli/BenchCmd.lean.
-          valid="aiur aiur-sharded-env-check ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
+          valid="aiur aiur-sharded-env-check ix-compile ix-decompile ooc-check"
           accepted="$valid all"
           # Parse the workload token(s) after the command, lowercased.
           workloads=$(printf '%s' "$BODY" \

.github/workflows/nix.yml

@@ -64,11 +64,6 @@ jobs:
       - run: nix flake check --print-build-logs --accept-flake-config
       # Run the real build and test commands inside the development environment.
       - run: nix develop --accept-flake-config --command bash -c "lake build && lake test"
-      # Realize the zkVM shells so they're verified and pushed to the cache,
-      # and smoke-test each shell's toolchain entrypoint.
-      # TODO: Re-enable once the zkVM shells build in CI.
-      # - run: nix develop --print-build-logs --accept-flake-config .#zisk --command cargo-zisk --version
-      # - run: nix develop --print-build-logs --accept-flake-config .#sp1 --command cargo prove --version
 
   nix-gate:
     if: ${{ always() }}

Benchmarks/Typecheck.lean

@@ -30,8 +30,7 @@ lake exe bench-typecheck --ixe <path> --consts <n1,n2,…> [--consts-file <p>] [
                         (writes `foo.ixe`). Required.
   --consts <n1,n2,…>    comma-separated fully-qualified constant names to
                         benchmark (e.g. `Nat.add_comm,String.append`). Same
-                        flag/shape as `ix check --consts`, `zisk-host --consts`,
-                        and `sp1-host --consts`.
+                        flag/shape as `ix check --consts`.
   --consts-file <path>  additionally read names from a file: one per line, blank
                         lines and `#` comments ignored. Unions with --consts.
 
@@ -42,7 +41,7 @@ lake exe bench-typecheck --ixe <path> --consts <n1,n2,…> [--consts-file <p>] [
 
   --skip-deps    check only each target itself (verify_const, trusting its
                  deps) instead of its whole transitive closure (verify_claim,
-                 the default). Same flag as `zisk-host --skip-deps`; reserved
+                 the default). Reserved
                  for targets too expensive to full-closure-check.
   --json <path>  write results JSON to <path> (per constant, plus one pair row
                  with --join). Off by default: normal CLI usage prints only
@@ -978,10 +977,10 @@ def typecheckCmd : Cli.Cmd := `[Cli|
 
   FLAGS:
     "ixe"          : String; "Path to a serialized `Ixon.Env` (e.g. produced by `ix compile`). Required."
-    "consts"       : String; "Comma-separated fully-qualified constant names to benchmark (e.g. `Nat.add_comm,String.append`). Same flag/shape as `ix check --consts`, `zisk-host --consts`, and `sp1-host --consts`."
+    "consts"       : String; "Comma-separated fully-qualified constant names to benchmark (e.g. `Nat.add_comm,String.append`). Same flag/shape as `ix check --consts`."
     "consts-file"  : String; "Additionally read constant names from a file (one per line; `#` comments and blank lines ignored). Unions with --consts."
     "json"      : String; "Write results JSON to this path (per constant, plus one pair row with --join). Off by default; normal CLI usage prints only the human-readable summary."
-    "skip-deps";          "Check only each target itself (verify_const, trusting its deps) instead of re-checking its whole transitive closure (verify_claim). Same flag as `zisk-host --skip-deps`."
+    "skip-deps";          "Check only each target itself (verify_const, trusting its deps) instead of re-checking its whole transitive closure (verify_claim)."
     "execute-only";       "Execute only (Phase 1: constants / fft-cost / execute-time) and skip proving. The fast per-PR `execute`-mode signal."
     "recursive";          "After each prove, execute and then prove the in-circuit multi-stark verifier over the fresh proof (the fri-verifier-* metrics; see the module docstring). Uses recursion-tuned FRI parameters. Conflicts with --execute-only."
     "join";               "With --recursive and exactly two resolved constants, prove each as a singleton CheckEnv shard, then execute/prove/verify one direct flat aggregate join (ix_aggr shape 2). Emits a dedicated `left + right` row with join-* metrics. Conflicts with --skip-deps, --execute-only, and --interp."

Cargo.toml

@@ -10,10 +10,6 @@ members = [
   "crates/ixon",
   "crates/kernel",
 ]
-# `zisk/`, `sp1/`, and `sp1-compress/` are their own Cargo workspaces built
-# via their respective zkVM toolchains; excluded so host workspace ops don't
-# pick them up.
-exclude = ["zisk", "sp1", "sp1-compress", "multi-stark"]
 resolver = "2"
 
 [profile.dev]