bench: one shared constant set, runtime zisk sharding, stage-scoped aiur measures

.github/workflows/bench-main.yml

@@ -38,10 +38,10 @@ env:
   COMPILE_DIR: Benchmarks/Compile
 
 jobs:
-  # Build the `ix`, `bench-typecheck`, and `bench-recursive-verifier`
-  # binaries once and cache them; every later job restores them instead of
-  # rebuilding. They are built with -Ctarget-cpu=native, so every job that
-  # runs them must use the same warp runner class.
+  # Build the `ix` and `bench-typecheck` binaries once and cache them;
+  # every later job restores them instead of rebuilding. They are built
+  # with -Ctarget-cpu=native, so every job that runs them must use the
+  # same warp runner class.
   build:
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
@@ -65,10 +65,10 @@ jobs:
       - run: |
           mkdir -p ~/.local/bin
           echo | lake run install            # copies ix -> ~/.local/bin/ix
-          lake build bench-typecheck bench-recursive-verifier
-          cp .lake/build/bin/bench-typecheck .lake/build/bin/bench-recursive-verifier ~/.local/bin/
+          lake build bench-typecheck
+          cp .lake/build/bin/bench-typecheck ~/.local/bin/
           cp "${{ runner.temp }}/benchmark-build-cpu.txt" ~/.local/bin/
-          chmod +x ~/.local/bin/bench-typecheck ~/.local/bin/bench-recursive-verifier
+          chmod +x ~/.local/bin/bench-typecheck
       - uses: actions/cache/save@v6
         with:
           path: ~/.local/bin
@@ -128,7 +128,8 @@ jobs:
         # lake target (Compile<env>), the cache-key suffix, and the
         # bencher row name. Every registry env compiles here; which envs
         # the benchmark job then proves/checks depends on which envs have
-        # constants in Vectors.csv. Add FC once it's on current Lean.
+        # constants in Ix/BenchConstants.lean. Add FC once it's on
+        # current Lean.
         include:
           - { env: InitStd }
           - { env: Lean }
@@ -200,13 +201,14 @@ jobs:
           echo "testbed=$(meta testbed)" >> "$GITHUB_OUTPUT"
           echo "workload=$(meta workload)" >> "$GITHUB_OUTPUT"
           { echo "thresholds<<EOF"; meta thresholds; echo "EOF"; } >> "$GITHUB_OUTPUT"
-      # Pre-cut the closure shards zisk needs for heavy constants
-      # (extract → profile → shard). The zisk runs can cut these lazily
+      # Pre-cut the closure-shard artifacts for this env's zisk constants
+      # (extract → profile → shard; the planner's RAM budget decides each
+      # constant's shard count). The zisk runs can cut these lazily
       # themselves, but doing it here — right next to the fresh `.ixe`,
       # with the toolchain already installed — means they just restore a
       # directory.
       - if: steps.gates.outputs.zkvm == 'true'
-        name: Cut closure shards for heavy primaries
+        name: Cut closure shards for zisk constants
         run: ix bench shard --env ${{ matrix.env }} --ixe ${{ matrix.env }}.ixe
       # Cache the `.ixe` for the benchmark job. IMPORTANT: every restore of
       # this key must list the same paths — actions/cache versions the
@@ -249,16 +251,16 @@ jobs:
   #   - aiur: the proof pipeline — per constant, every stage plus the
   #     total: prove the IxVM typecheck (stage 1), then execute and
   #     prove the in-circuit multi-stark verifier over that fresh proof
-  #     (stage 2); the KZG stages will fold in as they land. Runs the
-  #     registry's fixed pipeline selection rather than the primary
-  #     subset — every stage is paid per constant. One
+  #     (stage 2); the KZG stages will fold in as they land. One
   #     subprocess per constant under the RAM watchdog; a too-large
   #     prove is killed and recorded as a `status: oom` row.
   #   - zisk: executes the same constants in the zkVM (deterministic
-  #     cycle counts; proving would need a GPU, so execute-only). Reuses
-  #     the pre-cut zkshards-<env>/ dirs; builds its Rust host in-job.
+  #     cycle counts; proving would need a GPU, so execute-only). Each
+  #     constant runs as the shard partition the planner's RAM budget
+  #     sized for it (one shard when it fits), reusing the pre-cut
+  #     zkshards-<env>/ dirs; builds its Rust host in-job.
   #   - ooc: the same kernel run out-of-circuit and in parallel (much
-  #     faster). One whole-env row plus one row per primary constant.
+  #     faster). One whole-env row plus one row per constant.
   #   - decompile: the inverse of compile. Roundtrip correctness is
   #     checked elsewhere (`ix validate` / roundtrip tests) — this only
   #     measures speed and memory.
@@ -350,18 +352,27 @@ jobs:
           key: bench-perconst-${{ github.sha }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }}
       # Convert rows for upload even when the run step failed: bmf drops
       # every non-ok row (rejected or OOM), so only clean measurements
-      # reach bencher.
+      # reach bencher. bmf exits nonzero when NO ok rows survive — the
+      # steady state for a cell whose only constant exceeds the RAM
+      # ceiling (the OOM row documents the gap) — so that skips the
+      # upload without failing the job; the run step above is the
+      # failure authority. The `cat` still fails the step when bmf died
+      # before writing a file (a real infrastructure error).
       - name: Convert to Bencher Metric Format
         id: bmf
         if: ${{ !cancelled() }}
         run: |
-          ix bench bmf --in bench.json --out bench-bmf.json
+          if ix bench bmf --in bench.json --out bench-bmf.json; then
+            echo "nonempty=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "nonempty=false" >> "$GITHUB_OUTPUT"
+          fi
           cat bench-bmf.json
       # Upload under this entry's testbed and workload. The threshold
       # flags (and the reasoning behind each bound) live next to the
       # backend in Ix/Cli/BenchCmd.lean.
       - uses: ./.github/actions/bencher-track
-        if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
+        if: ${{ !cancelled() && steps.bmf.outputs.nonempty == 'true' }}
         with:
           testbed: ${{ matrix.params.testbed }}
           workload: ${{ matrix.params.workload }}

.github/workflows/bench-pr.yml

@@ -1,4 +1,4 @@
-# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
+# `!benchmark` PR command: run the shared constant set (Ix/BenchConstants.lean)
 # through chosen prover backend(s) and post a base-vs-PR comparison table.
 # 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.
@@ -10,13 +10,11 @@
 #                                  #  defaults to every env for compile/decompile, InitStd
 #                                  #  for the rest)
 #   BENCH_CONSTS=Nat.gcd,Y        # bench exactly these constants on the per-constant
-#                                  #  backends (overrides the curated selection). Each name's
-#                                  #  env is found automatically — Vectors.csv row first, else
-#                                  #  defining module, else Mathlib (FLT for FLT.* names) — so
-#                                  #  BENCH_ENVS is never required; a single-env BENCH_ENVS
-#                                  #  still forces placement
-#   BENCH_FULL=1                   # run the full curated set, not just primary
-#   BENCH_SHARD=1                  # restrict to the multi-shard target constants
+#                                  #  backends (overrides the shared selection). Each name's
+#                                  #  env is found automatically — benchConstants entry first,
+#                                  #  else defining module, else Mathlib (FLT for FLT.* names)
+#                                  #  — so BENCH_ENVS is never required; a single-env
+#                                  #  BENCH_ENVS still forces placement
 #   BENCH_PHASES=1                 # add per-constant phase drill-downs to the comment
 #   RUST_LOG=info                  # passthrough env (allowlisted)
 #   IX_COMPILE_EAGER=1             # compile-knob passthrough (also IX_COMPILE_DEMOTE /
@@ -38,11 +36,8 @@
 #     in-circuit multi-stark verifier over that fresh proof), reported
 #     as one comparison table per stage — witness execute, prove, peak
 #     RAM, proof size, verify — closing with the pipeline ledger (total
-#     time and the run's RAM ceiling). Its default selection is a fixed
-#     three-constant list, not the primary subset (`fixedSelections` in
-#     Ix/Cli/BenchCmd.lean): every stage is paid per constant, so the
-#     default set is what one host can finish. BENCH_FULL=1 and
-#     BENCH_CONSTS still override. The bare `execute`
+#     time and the run's RAM ceiling). BENCH_CONSTS overrides the shared
+#     selection. The bare `execute`
 #     token switches it to the fast Phase-1-only mode (witness
 #     generation; no bencher baseline exists for that, so the base side
 #     comes from a base-SHA run).
@@ -145,8 +140,8 @@ jobs:
             -f head-sha="${{ steps.comment-branch.outputs.head_sha }}" \
             -f comment-body="$COMMENT_BODY"
 
-  # Select or build the PR's `ix`, `bench-typecheck`, and
-  # `bench-recursive-verifier` once, then publish them as a run-scoped
+  # Select or build the PR's `ix` and `bench-typecheck` once, then
+  # publish them as a run-scoped
   # artifact for every later job. Normal runs may select a persistent
   # head-SHA cache. A cached `ix` may bootstrap command parsing, but `fresh`
   # replaces the full bundle before it is published to benchmark jobs.
@@ -163,8 +158,6 @@ jobs:
       revision: ${{ steps.target.outputs.revision }}
       matrix: ${{ steps.parse.outputs.matrix }}
       envs: ${{ steps.parse.outputs.envs }}
-      shard: ${{ steps.parse.outputs.shard }}
-      full: ${{ steps.parse.outputs.full }}
       fresh: ${{ steps.parse.outputs.fresh }}
       passthrough-env: ${{ steps.parse.outputs.passthrough-env }}
       config-summary: ${{ steps.parse.outputs.config-summary }}
@@ -233,10 +226,10 @@ jobs:
       - name: Build benchmark binaries
         if: steps.parse.outputs.fresh == '1' || steps.bins.outputs.cache-hit != 'true'
         run: |
-          lake build ix bench-typecheck bench-recursive-verifier
-          cp .lake/build/bin/ix .lake/build/bin/bench-typecheck .lake/build/bin/bench-recursive-verifier ~/.local/bin/
+          lake build ix bench-typecheck
+          cp .lake/build/bin/ix .lake/build/bin/bench-typecheck ~/.local/bin/
           cp "${{ runner.temp }}/benchmark-build-cpu.txt" ~/.local/bin/
-          chmod +x ~/.local/bin/ix ~/.local/bin/bench-typecheck ~/.local/bin/bench-recursive-verifier
+          chmod +x ~/.local/bin/ix ~/.local/bin/bench-typecheck
       # Cache entries are immutable and may lack optional provenance. Keep the
       # run artifact's shape stable and state explicitly when its build host is
       # unknown.
@@ -254,7 +247,7 @@ jobs:
       - name: Package run binaries
         run: >-
           tar -C "$HOME/.local/bin" -cf benchmark-binaries.tar
-          ix bench-typecheck bench-recursive-verifier benchmark-build-cpu.txt
+          ix bench-typecheck benchmark-build-cpu.txt
       - name: Upload run binaries
         uses: actions/upload-artifact@v7
         with:
@@ -485,8 +478,6 @@ jobs:
       BASE_SHA: ${{ inputs.base-sha }}
       BASE_REF: ${{ inputs.base-ref }}
       HEAD_SHA: ${{ needs.build.outputs.revision }}
-      SHARD: ${{ needs.build.outputs.shard }}
-      FULL: ${{ needs.build.outputs.full }}
       FRESH: ${{ needs.build.outputs.fresh }}
     steps:
       # The PR is checked out at the workspace root (the local composite
@@ -562,9 +553,9 @@ jobs:
 
       # ---------- PR side ----------
       # The PR side runs first: `ix bench run` selects its constants from
-      # Vectors.csv, and pr.json's row names become the canonical name
-      # list this run measures — the base-side fetch below asks bencher
-      # for exactly those names.
+      # the shared set (Ix/BenchConstants.lean), and pr.json's row names
+      # become the canonical name list this run measures — the base-side
+      # fetch below asks bencher for exactly those names.
       - name: Run backend on PR → pr.json
         id: pr-run
         # Exit 3 = the kernel rejected a constant on the PR side (rows are
@@ -586,8 +577,6 @@ jobs:
             exit 0
           fi
           flags=""
-          [ "$FULL" = 1 ] && flags="$flags --full"
-          [ "$SHARD" = 1 ] && flags="$flags --shard-only"
           [ -n "$CONSTS" ] && flags="$flags --consts $CONSTS"
           ix bench run --backend "$BACKEND" --env "$BENV" --mode "$MODE" \
             --ixe "$BENV.ixe" --out "$GITHUB_WORKSPACE/pr.json" $flags
@@ -735,10 +724,10 @@ jobs:
              && cmp -s lean-toolchain base/lean-toolchain; then
             if [ "$BENV" != Mathlib ] || [ "$ixe" = true ]; then
               mkdir -p base/.lake/build/bin
-              mv ~/.local/bin/ix ~/.local/bin/bench-typecheck ~/.local/bin/bench-recursive-verifier base/.lake/build/bin/ 2>/dev/null || true
+              mv ~/.local/bin/ix ~/.local/bin/bench-typecheck base/.lake/build/bin/ 2>/dev/null || true
               mv ~/.local/bin/benchmark-build-cpu.txt base/.lake/build/bin/ 2>/dev/null || true
               [ -x base/.lake/build/bin/ix ] && [ -x base/.lake/build/bin/bench-typecheck ] \
-                && [ -x base/.lake/build/bin/bench-recursive-verifier ] && cached=true
+                && cached=true
             fi
           fi
           echo "cached=$cached" >> "$GITHUB_OUTPUT"
@@ -758,14 +747,14 @@ jobs:
         with:
           label: Base benchmark binary build CPU
           output-file: base/.lake/build/bin/benchmark-build-cpu.txt
-      - name: Build base (ix, bench-typecheck, bench-recursive-verifier)
+      - name: Build base (ix, bench-typecheck)
         if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true'
         uses: leanprover/lean-action@v1
         with:
           lake-package-directory: base
           auto-config: false
           build: true
-          build-args: "ix bench-typecheck bench-recursive-verifier"
+          build-args: "ix bench-typecheck"
           use-github-cache: false
       # For a mathlib-importing env (Mathlib, FLT), the base-side compile
       # resolves imports from the base tree's Benchmarks/Compile
@@ -789,8 +778,9 @@ jobs:
       # produced no results" note instead of a silent all-n/a table.
       #
       # Partial bencher miss: run just the uncovered names (via --consts).
-      # They are typically constants the PR itself adds, which the base
-      # tree's Vectors.csv doesn't list — so --csv points at the PR's copy.
+      # They are typically constants the PR itself adds; the PR's `ix`
+      # carries the PR's compiled-in constant set, so the base side
+      # selects them without any extra plumbing.
       # Full miss: run the normal selection (or the BENCH_CONSTS override).
       - name: Run backend on base → merge into main.json
         if: steps.decide.outputs.run-base == 'true'
@@ -805,8 +795,6 @@ jobs:
             sudo prlimit --pid $$ --memlock=unlimited:unlimited
           fi
           flags=""
-          [ "$FULL" = 1 ] && flags="$flags --full"
-          [ "$SHARD" = 1 ] && flags="$flags --shard-only"
           if [ -n "$CONSTS" ]; then
             # BENCH_CONSTS override: the base side must measure the same
             # explicit names, not the default selection.
@@ -820,7 +808,6 @@ jobs:
           [ -f "base/$BENV.ixe" ] && flags="$flags --ixe base/$BENV.ixe"
           ix bench run --backend "$BACKEND" --env "$BENV" --mode "$MODE" \
             --repo base \
-            --csv "$GITHUB_WORKSPACE/Benchmarks/Vectors.csv" \
             --out "$GITHUB_WORKSPACE/base.json" $flags
           echo "base-side ix bench run exit $?"
           set -e

.github/workflows/bencher-plots.yml

@@ -2,8 +2,8 @@ name: Sync bencher dashboard plots
 
 # Manual bencher op, like bencher-thresholds-reset: `ix bench plots` syncs
 # the dashboard plots to the registry (one plot per tracked (testbed,
-# measure) plus the input-constants and Zisk-heavy-shards cross-cutting
-# plots; see Ix/Cli/BenchPlots.lean for the keep/replace semantics).
+# measure) plus the cross-cutting input-constants plot; see
+# Ix/Cli/BenchPlots.lean for the keep/replace semantics).
 # Dispatch it after a registry change —
 # new primary constant, measure-list edit, plot-title change — has merged
 # to main AND bench-main has run on it: the registry is compiled into the

.github/workflows/merge-tests.yml

@@ -22,22 +22,38 @@ jobs:
           - name: Lake ignored tests (compile pipeline)
             kind: lake
             runner: warp-ubuntu-latest-x64-32x
-            test_args: --ignored compile-pipeline
-          - name: Lake ignored tests (kernel)
+            test_args: >-
+              --ignored
+              rust-canon-roundtrip serial-canon-roundtrip parallel-canon-roundtrip
+              graph-cross condense-cross rust-serialize ixon-corpus
+              rust-decompile validate-aux aux-gen-diff decompile-diff
+          - name: Lake ignored tests (compile)
             kind: lake
             runner: warp-ubuntu-latest-x64-32x
-            test_args: --ignored kernel
+            test_args: --ignored compile
+          - name: Lake ignored tests (decompile)
+            kind: lake
+            runner: warp-ubuntu-latest-x64-32x
+            test_args: --ignored decompile
           - name: Lake ignored tests (misc)
             kind: lake
             runner: warp-ubuntu-latest-x64-32x
-            test_args: --ignored --exclude=compile-pipeline,kernel,typecheckers
+            test_args: >-
+              --ignored
+              shard-map catalog-fixtures commit-io
+              kernel-ixon-roundtrip kernel-tutorial kernel-check-env kernel-check-const
+              rust-kernel-build-primitives rust-kernel-build-prim-origs ixvm
             zk_voting: true
           - name: Valgrind FFI
             kind: valgrind
             runner: warp-ubuntu-latest-x64-8x
           - name: Ix.Tc verification and parity
             kind: tc
             runner: warp-ubuntu-latest-x64-16x
+            test_args: >-
+              --ignored
+              tc-anon-diff tc-init tc-tutorial tc-roundtrip tc-ingress-meta
+              tc-pins tc-accel-diff lean4lean
     runs-on: ${{ matrix.runner }}
     steps:
       - name: Validate merge-test variant
@@ -137,7 +153,7 @@ jobs:
         run: lake test --wfail -- tc-unit
       - name: Run Ix.Tc ignored tests
         if: ${{ matrix.kind == 'tc' }}
-        run: lake test --wfail -- --ignored typecheckers
+        run: lake test --wfail -- ${{ matrix.test_args }}
 
   merge-tests-result:
     name: Merge tests

Benchmarks/RecursionDebug.lean

@@ -30,8 +30,12 @@ lake exe bench-recursion-debug --ixe init.ixe --const Array.extract_append --mod
   --reprove        force a fresh prove even when blobs exist
   --skip-deps      subject-only check (`verify_const`) instead of the
                    full-closure `verify_claim` default
-  --queries N      FRI numQueries (default 100 — matches bench-typecheck
-                   --recursive); must match between prove and replay!
+  --queries N      FRI numQueries (default 100; the pipeline's
+                   `recursiveFriParameters` in Benchmarks/Typecheck.lean
+                   runs 50 with no query PoW, while this tool grinds 20
+                   PoW bits — pass --queries 50 when a replay should
+                   mirror the pipeline's query count); must match between
+                   prove and replay!
   --mode M         how to run the recursive verifier over the saved proof:
                      native    codegen'd Rust verifier (default; the
                                production path bench-typecheck uses)