KZG recursive verifier

.github/workflows/bench-main.yml

@@ -14,7 +14,7 @@ name: Benchmark main
 #                  compile benchmark) and caches the file for stage 3.
 #   3. benchmark — one job per remaining entry: restore the `.ixe` and
 #                  run the entry's backend over it (aiur, zisk, ooc,
-#                  decompile, aiur-recursive).
+#                  decompile).
 #
 # Each entry uploads to its own bencher testbed/workload, so a threshold
 # reset for one workload never touches another. When the kernel REJECTS a
@@ -231,12 +231,12 @@ jobs:
   # restores the compile job's cached `.ixe` — nothing recompiles here.
   #
   # What each backend measures:
-  #   - aiur prove: the real workload — a full STARK prove per constant,
-  #     one subprocess per constant under the RAM watchdog; a too-large
+  #   - 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. One
+  #     subprocess per constant under the RAM watchdog; a too-large
   #     prove is killed and recorded as a `status: oom` row.
-  #     aiur execute: the fast signal — witness generation only.
-  #     The two modes upload to separate testbeds; shared measure names
-  #     (peak-rss, throughput) mean that mode's phase.
   #   - 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.
@@ -245,12 +245,6 @@ jobs:
   #   - decompile: the inverse of compile. Roundtrip correctness is
   #     checked elsewhere (`ix validate` / roundtrip tests) — this only
   #     measures speed and memory.
-  #   - aiur-recursive: proves the IxVM typecheck of three fixed constants
-  #     (Nat.add_comm, Vector.append, String.split), runs the in-circuit
-  #     verifier over each proof, then proves THAT — the cost of
-  #     recursion at kernel scale. A fixed subset instead of the
-  #     Vectors.csv fan-out: its `env` field names the (already-cached)
-  #     `.ixe` the shared restore step pulls and the constants resolve in.
   benchmark:
     name: ${{ matrix.params.label }}
     needs: [compile, plan]

.github/workflows/bench-pr.yml

@@ -1,7 +1,7 @@
 # `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
 # through chosen prover backend(s) and post a main-vs-PR comparison table.
 #
-#   !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
+#   !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] | all) [execute]
 #     (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
 #      with a note in the config summary)
 #   BENCH_ENVS=InitStd,Mathlib     # which compiled envs (case-insensitive, any registry env;
@@ -23,21 +23,16 @@
 #                                  # its own row instead of the default run's
 #
 # Each backend runs its registry default mode:
-#   - aiur: `prove` (the real workload; the report also shows the
-#     fft-cost / execute-time measured on the way). The bare `execute`
-#     token switches aiur to the fast execute-only mode; the bare
-#     `recursive` token switches it to recursive mode (no bencher
-#     baseline exists for that, and it needs more RAM than CI has — meant
-#     for a bigger manual dispatch).
+#   - aiur: `prove` — the full proof pipeline per constant (stage 1
+#     proves the IxVM typecheck, stage 2 executes and proves the
+#     in-circuit multi-stark verifier over that fresh proof), reported
+#     as the per-stage wall clocks plus their total. The bare `execute`
+#     token switches it to the fast Phase-1-only mode (witness
+#     generation; no bencher baseline exists for that, so the main side
+#     comes from a base-SHA run).
 #   - zisk / sp1 / ooc: `execute`.
 #   - compile: `ix compile <env>.lean` → `<env>.ixe`.
 #   - decompile: `ix decompile` over the compile run's fresh `.ixe`.
-#   - aiur-recursive: fixed IxVM statements (Nat.add_comm plus the
-#     heavy-tier Vector.append and String.split; Array.extract_append
-#     is dropped for now — it OOMs on CI) proved and recursively verified via
-#     bench-typecheck --recursive; always schedules exactly one run
-#     regardless of BENCH_ENVS (the constants resolve in whichever env's
-#     .ixe the entry carries).
 # The bare `fresh` token skips the bencher fetch and re-measures the main
 # side with a local base-SHA run. Nothing in this workflow uploads to
 # bencher, so the canonical baseline is never touched.

.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 in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
-#     `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
+#     `ix-compile`, `ix-decompile`, `aiur`, `zisk-check-execute`, `sp1-check-execute`, `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-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
+        options: [ix-compile, ix-decompile, aiur, zisk-check-execute, sp1-check-execute, ooc-check, all]
       sha:
         description: "Commit to anchor to (default: HEAD)"
         required: false
@@ -77,7 +77,7 @@ jobs:
           # (backendSpecs) minus the runner-arch suffix. Static because this
           # job runs on a cheap runner with no built `ix`; keep in sync when
           # adding a backend.
-          valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
+          valid="aiur ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
           if [ "$EVENT" = workflow_dispatch ]; then
             # Reset the chosen workload(s) at the given commit; no PR scan.
             sha="${INPUT_SHA:-$HEAD_SHA}"
@@ -133,7 +133,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-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
+          valid="aiur ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
           accepted="$valid all"
           # Parse the workload token(s) after the command, lowercased.
           workloads=$(printf '%s' "$BODY" \

Benchmarks/RecursiveVerifier.lean

@@ -30,9 +30,9 @@ lake exe bench-recursive-verifier --execute-only  # skip the outer prove (FFT/ex
   --json <path>    write a benchmark results row (Ix.Benchmark.Results); the
                    row lands after the verifier execute and is refined after
                    the outer prove, so a kill mid-prove keeps the execute
-                   metrics. (A local harness only: CI's aiur-recursive
-                   backend instead drives `bench-typecheck --recursive`
-                   over fixed IxVM statements.)
+                   metrics. (A local harness only: CI's aiur backend
+                   instead drives `bench-typecheck --recursive` over the
+                   curated Vectors.csv constants.)
   --json-name <n>  row key (default: the inner entrypoint name)
   --texray         tracing-texray timeline + RAM; with --json, spans also land
                    at `<json>.spans` for the CI drill-down

Benchmarks/Typecheck.lean

@@ -54,17 +54,17 @@ lake exe bench-typecheck --ixe <path> --consts <n1,n2,…> [--consts-file <p>] [
                  execute it (`recursive-execute-time`, `recursive-fft-cost` — the
                  recursion-cost proxy), then prove that execution end-to-end
                  (`recursive-prove-time`, `recursive-peak-rss`,
-                 `recursive-proof-size`, `recursive-verify-time`). The whole
-                 system, inner prove included, switches to the recursion-tuned
-                 parameters (`recursiveFriParameters`), so recursive rows are
-                 NOT comparable to the standard prove run — they land on
-                 their own testbed (`ix bench run --backend aiur --mode
-                 recursive`; the fixed two-constant subset runs in CI as
-                 `--backend aiur-recursive`). At IxVM scale the recursion
-                 exceeds the CI RAM ceiling (even Nat.add_comm's outer
-                 prove peaks ~195 GiB as of 2026-08), so a watchdog kill
-                 landing as a `status: oom` row (dropped by bmf) is the
-                 expected shape there. With --texray, both
+                 `recursive-proof-size`, `recursive-verify-time`), and close the
+                 row with the stage ledger — `stage1-time` (witness execute +
+                 inner prove), `stage2-time` (verifier execute + outer prove),
+                 `total-time` (their sum; later pipeline stages will fold in
+                 as they land). The whole system, inner prove included,
+                 switches to the recursion-tuned parameters
+                 (`recursiveFriParameters`), so recursive rows are NOT
+                 comparable to a plain prove run's. This is the mode CI's
+                 `aiur` benchmark runs (`ix bench run --backend aiur`): the
+                 full proof pipeline, per constant, over the curated
+                 Vectors.csv selection. With --texray, both
                  proves stream the same `stark/...` span names, so the summed
                  `phase-stark-*` fields cover the pair. Conflicts with
                  --execute-only.
@@ -99,7 +99,9 @@ The JSON is a flat shape (`{ "<name>": { "constants": …, "fft-cost": …,
 "execute-time": …, "prove-time": …, "proof-size": …, "verify-time": …,
 "throughput": …, "peak-rss": …, and with --recursive also "recursive-execute-time": …,
 "recursive-fft-cost": …, "recursive-prove-time": …, "recursive-peak-rss": …,
-"recursive-proof-size": …, "recursive-verify-time": … } }`). `peak-rss` and `throughput` are
+"recursive-proof-size": …, "recursive-verify-time": …, plus the stage ledger
+"stage1-time": …, "stage2-time": …, "total-time": … once the pipeline
+completes } }`). `peak-rss` and `throughput` are
 phase-scoped by MODE: an `--execute-only` row carries the Phase-1 RSS
 high-water and constants/sec over the execute; a prove row carries the
 prover's high-water and constants/sec over the prove (with `prove-time`,
@@ -131,20 +133,20 @@ def recursiveCommitmentParameters : Aiur.CommitmentParameters := {
   capHeight := 0
 }
 
-/-- Recursion FRI parameters for `--recursive`. The query count IS the
-    soundness level, so a real (secure) recursive proof needs a full query
-    count, not a toy handful: 50 queries at log-blowup 2 target ~100 bits,
-    halving the in-circuit verifier's query-proportional work (and the
-    outer prove's footprint) relative to the previous 100-query setting —
-    sized so the run has a chance of fitting CI's weaker hosts. The
-    in-circuit verifier's cost scales with the count; an OOM row still
+/-- Recursion FRI parameters for `--recursive` — the CI `aiur` pipeline
+    benchmark's parameters, applied to the stage-1 and stage-2 proofs
+    alike. The query count IS the soundness level, so a real (secure)
+    recursive proof needs a full query count, not a toy handful — but the
+    in-circuit verifier's work (and the outer prove's footprint) scales
+    with it: 50 queries still OOMs the ~123 GiB CI hosts on the heavy end
+    of the selection, so 40 is the count sized to fit. An OOM row still
     documents the gap between secure recursion and what fits today.
     `--recursive` runs the WHOLE system, inner prove included, under
-    these, so its rows are not comparable to the standard `prove` run's. -/
+    these, so its rows are not comparable to a plain `prove` run's. -/
 def recursiveFriParameters : Aiur.FriParameters := {
   logFinalPolyLen := 0
   maxLogArity := 1
-  numQueries := 50
+  numQueries := 40
   commitProofOfWorkBits := 0
   queryProofOfWorkBits := 0
 }
@@ -218,8 +220,8 @@ def jsonRound (d : Nat) (f : Float) : Json :=
     `peak-rss` and `throughput` are PHASE-SCOPED BY MODE, not by name: an
     execute-only run's row carries the Phase-1 peak and constants/sec over
     the execute; a prove run's row carries the prove-phase peak and
-    constants/sec over the prove. The two modes upload to separate bencher
-    testbeds (aiur-check-execute-* / aiur-check-prove-*), so the shared names never
+    constants/sec over the prove. The two modes store on separate bencher
+    testbeds (aiur-execute-* / aiur-*), so the shared names never
     collide — run the execute run when you want execute-side numbers. -/
 def Result.toJsonEntry (executeOnly : Bool) (r : Result) : String × Json :=
   if r.failed then
@@ -272,6 +274,20 @@ def Result.toJsonEntry (executeOnly : Bool) (r : Result) : String × Json :=
     let fields := match r.recursiveVerifySec with
       | some v => fields ++ [ ("recursive-verify-time", jsonRound 6 v) ]
       | none => fields
+    -- The stage ledger, once the whole pipeline has run: each stage's
+    -- wall clock is its witness execution plus its prove (verification
+    -- is a consumer cost, not a production one), and `total-time` is
+    -- their sum — the headline the `aiur` benchmark sorts on. Emitted
+    -- only with every component present, so it doubles as the row's
+    -- completion marker (the orchestrator's teardown-kill `doneKey`).
+    let fields := match r.proveSec, r.recursiveExecuteSec, r.recursiveProveSec with
+      | some p, some re, some rp =>
+        let stage1 := r.executeSec + p
+        let stage2 := re + rp
+        fields ++ [ ("stage1-time", jsonRound 6 stage1)
+                  , ("stage2-time", jsonRound 6 stage2)
+                  , ("total-time", jsonRound 6 (stage1 + stage2)) ]
+      | _, _, _ => fields
     (r.name, Json.mkObj fields)
 
 /-- Time a thunk, returning its value and the elapsed seconds. The result is
@@ -627,7 +643,7 @@ def typecheckCmd : Cli.Cmd := `[Cli|
     "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 recursive-* metrics; see the module docstring). Uses recursion-tuned FRI parameters. Conflicts with --execute-only."
     "interp";             "Route execution through the generic Aiur bytecode interpreter instead of the codegen'd IxVM kernel - no `lake exe ix codegen` + cargo rebuild needed after `Ix/IxVM/*.lean` edits. Applies to Phase 1, the prove's witness generation, and both --recursive steps. Slower; execute-time rows are not comparable to codegen-mode runs (fft-cost is)."
-    "queries"   : Nat;    "Override the FRI query count of the selected parameter set (default 100, or 50 with --recursive; applies to inner and outer proof alike)."
+    "queries"   : Nat;    "Override the FRI query count of the selected parameter set (default 100, or 40 with --recursive; applies to inner and outer proof alike)."
     texray;               "Enable the tracing-texray timeline + RAM breakdown (per-prove spans on stderr). Combined with --json, per-phase span timings are additionally written to `<json>.spans` as JSON Lines for the CI drill-down. Off by default."
 
 ]