From 1f7b4241d7e6c60542d50631c28de1d37f2fbe9b Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 20 Aug 2026 14:31:16 -0400 Subject: [PATCH 1/4] bench: one shared constant set, runtime zisk sharding, stage-scoped aiur measures MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The benchmark suite ran different constants per backend, curated through Benchmarks/Vectors.csv's tier/shard_target/primary columns plus a fixed aiur selection, and the aiur pipeline's stage measures collided with the plain Phase-1 names via a mode-scoping convention. This consolidates all of it. Shared constant set. Ix/BenchConstants.lean (a plain importable array of (name, env)) replaces Vectors.csv as the single selection: every per-constant backend (aiur, zisk, ooc, lean4lean) runs the same constants, now including Std.HashMap, Lean.Json, and Multiset.sort at the heavy end. The tier/shard_target/primary columns, fixedSelections, --full/--tier/--shard-only/--csv flags, and the BENCH_FULL/BENCH_SHARD tokens are gone with the CSV. benchExclusions shrinks to hard infeasibility only: bitblast on the zkVMs, whose ~18B-step atomic mutual block crashes the ZisK executor and cannot be split by the shard cutter. bitblast itself is commented out of the set with a re-add note — its Aiur prove exceeds any current host, so a scheduled run could only re-document the same OOM; --consts/BENCH_CONSTS still run it on demand. Runtime zisk sharding. With the tier column gone, every zisk constant goes through extract → profile → `ix shard --max-ram ` at bench time: the planner's RAM budget sizes the partition from the closure's predicted cost, so a closure that fits gets a one-shard plan and runs as a single leaf. Artifacts still pre-cut in bench-main's compile job and ride the zkshards cache; a failed cut falls back to the whole closure under the watchdog. Formerly-light constants now measure from their extracted sub-env (host peak-rss tightens once; guest cycles unchanged). Stage-scoped aiur measures. The pipeline's measures rename from the plain/recursive- split to a uniform stage- prefix (stage1-prove-time, stage2-fft-cost, …) so the KZG stages join as stage3-/stage4- without renames. stagePrefixOf/dropStagePrefix move to the registry and parse the prefix generically; formatting kinds, units, improvement direction, and stage-table labels all derive from the base name. The execute mode keeps plain Phase-1 names on its own testbed, so the modes no longer share measure names at all. Throughput returns as a column in every stage table plus the ledger (stage1-/stage2-throughput, and pipeline-throughput = constants / total-time), emitted by bench-typecheck; none carry thresholds — constants is pinned exactly, so each is the pure inverse of an already-bounded time. bench-recursive-verifier adopts the same stage1-/stage2- keys. Dashboard. New plots: Aiur Total Throughput, Aiur Total Peak RAM Usage (which stage sets the ceiling can shift as stages are added), and Aiur Stage 1 Proof Size (it sizes stage 2's in-circuit workload). The input-constants overlay renames to Kernel Input Constants and sources from the zisk testbed — sharded execution keeps every closure feasible, so its rows upload even where the aiur prove OOMs and the row is dropped. Zisk Shards becomes a regular full-set plot (runtime-planned counts, flat at 1 for closures that fit). The sync now warn-skips a measure bencher hasn't seen yet, like benchmarks and testbeds, so it can run at any point mid-migration. CI hardening. bench-main's upload step no longer fails on a cell whose every row OOM'd — the new single-constant aiur cells (Lean, Mathlib) may have that as their steady state — the empty bmf result skips the upload and the run step stays the failure authority. A bench-measures unit suite pins the stage-prefix parsing edge cases. Migration: the renamed measures start fresh bencher series (the old recursive-* measures orphan; other testbeds keep the plain names). After this lands on main, let bench-main finish, then dispatch the plots sync. A !benchmark aiur run before that first bench-main completes shows n/a base columns for the stage measures; no threshold reset is needed. --- .github/workflows/bench-main.yml | 37 ++-- .github/workflows/bench-pr.yml | 41 ++-- .github/workflows/bencher-plots.yml | 4 +- Benchmarks/RecursiveVerifier.lean | 30 +-- Benchmarks/Typecheck.lean | 128 ++++++------ Benchmarks/Vectors.csv | 75 ------- Ix/BenchConstants.lean | 48 +++++ Ix/Cli/BenchCmd.lean | 294 +++++++++++----------------- Ix/Cli/BenchPlots.lean | 140 ++++++------- Ix/Cli/BenchReport.lean | 99 ++++------ Tests/Ix/BenchMeasures.lean | 40 ++++ Tests/Main.lean | 2 + docs/benchmarking.md | 85 ++++---- 13 files changed, 469 insertions(+), 554 deletions(-) delete mode 100644 Benchmarks/Vectors.csv create mode 100644 Ix/BenchConstants.lean create mode 100644 Tests/Ix/BenchMeasures.lean diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 99b052871..5cd43480f 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -128,7 +128,8 @@ jobs: # lake target (Compile), 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<> "$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-/ 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-/ 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 }} diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index 3bdaeeb52..ec1fa45f2 100644 --- a/.github/workflows/bench-pr.yml +++ b/.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). @@ -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 }} @@ -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 @@ -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 diff --git a/.github/workflows/bencher-plots.yml b/.github/workflows/bencher-plots.yml index 172176bd1..2db968c67 100644 --- a/.github/workflows/bencher-plots.yml +++ b/.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 diff --git a/Benchmarks/RecursiveVerifier.lean b/Benchmarks/RecursiveVerifier.lean index 40d050f63..b71c14aa5 100644 --- a/Benchmarks/RecursiveVerifier.lean +++ b/Benchmarks/RecursiveVerifier.lean @@ -32,17 +32,17 @@ lake exe bench-recursive-verifier --execute-only # skip the outer prove (FFT/ex the outer prove, so a kill mid-prove keeps the execute metrics. (A local harness only: CI's aiur backend instead drives `bench-typecheck --recursive` over the - curated Vectors.csv constants.) + shared benchmark constants (Ix.BenchConstants).) --json-name row key (default: the inner entrypoint name) --texray tracing-texray timeline + RAM; with --json, spans also land at `.spans` for the CI drill-down ``` -Row metrics: `prove-time`/`proof-size`/`verify-time` (the INNER statement), -`peak-rss` (inner-prove window), `recursive-execute-time`/`recursive-fft-cost` (the +Row metrics: `stage1-prove-time`/`stage1-proof-size`/`stage1-verify-time` (the INNER statement), +`stage1-peak-rss` (inner-prove window), `stage2-execute-time`/`stage2-fft-cost` (the verifier's execution and its in-circuit cost — the recursion-cost proxy), and -`recursive-prove-time`/`recursive-peak-rss`/`recursive-proof-size`/ -`recursive-verify-time` (the outer prove — the headline recursion metrics). +`stage2-prove-time`/`stage2-peak-rss`/`stage2-proof-size`/ +`stage2-verify-time` (the outer prove — the headline recursion metrics). Determinism note: the multi-stark prover is **non-deterministic under `parallel`** (the same statement yields byte-different valid proofs run-to-run), so the @@ -178,12 +178,12 @@ def main (args : List String) : IO UInt32 := do -- there still leaves these metrics on disk (the orchestrator merges -- `status: oom` in over them). let baseFields : List (String × Lean.Json) := - [ ("prove-time", jsonRound 6 (secs it0 it1)) - , ("proof-size", Lean.toJson proofBytes.size) - , ("verify-time", jsonRound 6 (secs it1 it2)) - , ("peak-rss", Lean.toJson innerPeak) - , ("recursive-execute-time", jsonRound 6 (secs e0 e1)) - , ("recursive-fft-cost", jsonRound 0 stats.totalFftCost) ] + [ ("stage1-prove-time", jsonRound 6 (secs it0 it1)) + , ("stage1-proof-size", Lean.toJson proofBytes.size) + , ("stage1-verify-time", jsonRound 6 (secs it1 it2)) + , ("stage1-peak-rss", Lean.toJson innerPeak) + , ("stage2-execute-time", jsonRound 6 (secs e0 e1)) + , ("stage2-fft-cost", jsonRound 0 stats.totalFftCost) ] writeRow' baseFields if !doProve then return 0 @@ -206,8 +206,8 @@ def main (args : List String) : IO UInt32 := do IO.eprintln "outer proof failed to verify" return 1 writeRow' <| baseFields ++ - [ ("recursive-prove-time", jsonRound 6 (secs t0 t1)) - , ("recursive-peak-rss", Lean.toJson outerPeak) - , ("recursive-proof-size", Lean.toJson nbytes) - , ("recursive-verify-time", jsonRound 6 (secs t1 t2)) ] + [ ("stage2-prove-time", jsonRound 6 (secs t0 t1)) + , ("stage2-peak-rss", Lean.toJson outerPeak) + , ("stage2-proof-size", Lean.toJson nbytes) + , ("stage2-verify-time", jsonRound 6 (secs t1 t2)) ] return 0 diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 156848368..dd8331a73 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -51,10 +51,10 @@ lake exe bench-typecheck --ixe --consts [--consts-file

] [ proving — the fast `execute`-mode signal. --recursive after each constant's prove, run the in-circuit multi-stark verifier (`verify_multi_stark_proof`) over the fresh proof: - execute it (`recursive-execute-time`, `recursive-fft-cost` — the + execute it (`stage2-execute-time`, `stage2-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`), and close the + (`stage2-prove-time`, `stage2-peak-rss`, + `stage2-proof-size`, `stage2-verify-time`), and close the row with the pipeline ledger — `total-time` (each stage's prove, summed; a prove already contains its own witness execution, so the standalone execute times are NOT added, @@ -66,8 +66,8 @@ lake exe bench-typecheck --ixe --consts [--consts-file

] [ (`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 + full proof pipeline, per constant, over the shared + benchmark constants (Ix.BenchConstants). With --texray, both proves stream the same `stark/...` span names, so the summed `phase-stark-*` fields cover the pair. Conflicts with --execute-only. @@ -98,18 +98,16 @@ first). A name absent from the env or whose execution errors is skipped with a warning, so a single bad name never fails the run. The harness imposes no time limit; bound a run with an external `timeout` if needed. -The JSON is a flat shape (`{ "": { "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": …, plus the pipeline -ledger "total-time": …, "pipeline-peak-rss": … -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`, -`proof-size`, `verify-time` present only once proven). The two modes are -stored on separate bencher testbeds, so the shared names never collide. Any +The JSON is a flat shape. An `--execute-only` row carries the plain +Phase-1 fields (`{ "": { "constants": …, "fft-cost": …, +"execute-time": …, "throughput": …, "peak-rss": … } }`); a `--recursive` +pipeline row stage-qualifies every stage measure (`"stage1-execute-time"`, +`"stage1-fft-cost"`, `"stage1-prove-time"`, `"stage1-throughput"`, +`"stage1-peak-rss"`, `"stage1-proof-size"`, `"stage1-verify-time"`, the +same seven as `"stage2-…"`, and `stage3-`/`stage4-` when the KZG stages +land), plus the pipeline ledger `"total-time"`, `"pipeline-throughput"`, +`"pipeline-peak-rss"` once the pipeline completes. Each stage's peak-rss +and throughput are scoped to that stage's own prove window. Any bencher-specific reshaping is the caller's job (see `.github/workflows/bench-main.yml`). -/ @@ -219,75 +217,85 @@ def jsonRound (d : Nat) (f : Float) : Json := else Int.ofNat scaled.round.toUInt64.toNat Json.num ⟨m, d⟩ -/-- Flat results object: `name → { constants, fft-cost, execute-time, … }`. - No bencher-specific shaping. +/-- Flat results object: `name → { constants, … }`. No bencher-specific + shaping. - `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 store on separate bencher - testbeds (aiur-execute-* / aiur-*), so the shared names never - collide — run the execute run when you want execute-side numbers. -/ + Measure names are MODE-SCOPED: an execute-only run's row carries the + plain Phase-1 fields (`fft-cost`, `execute-time`, `throughput`, + `peak-rss`); a pipeline run stage-qualifies every stage measure + (`stage1-…`, `stage2-…`), each stage's peak and constants/sec scoped + to its own prove window. The two modes store on separate bencher + testbeds (aiur-execute-* / aiur-*). -/ def Result.toJsonEntry (executeOnly : Bool) (r : Result) : String × Json := if r.failed then (r.name, Json.mkObj [("status", Json.str "rejected")]) else let base : List (String × Json) := [ ("status", Json.str "ok") - , ("constants", Lean.toJson r.constants) - , ("fft-cost", jsonRound 0 r.fftCost) - , ("execute-time", jsonRound 6 r.executeSec) ] + , ("constants", Lean.toJson r.constants) ] if executeOnly then + let fields := base ++ + [ ("fft-cost", jsonRound 0 r.fftCost) + , ("execute-time", jsonRound 6 r.executeSec) ] let fields := if r.executeSec > 0 then - base ++ [ ("throughput", jsonRound 2 (r.constants.toFloat / r.executeSec)) ] - else base + fields ++ [ ("throughput", jsonRound 2 (r.constants.toFloat / r.executeSec)) ] + else fields let fields := match r.executePeakRss with | some n => fields ++ [ ("peak-rss", Lean.toJson n) ] | none => fields (r.name, Json.mkObj fields) else - -- prove-time, the proving throughput, and the prove-phase peak are - -- present only once proven. + let fields := base ++ + [ ("stage1-fft-cost", jsonRound 0 r.fftCost) + , ("stage1-execute-time", jsonRound 6 r.executeSec) ] + -- stage1-prove-time, the proving throughput, and the prove-phase + -- peak are present only once proven. let fields := match r.proveSec with - | some p => base ++ [ ("prove-time", jsonRound 6 p) - , ("throughput", jsonRound 2 (r.constants.toFloat / p)) ] - | none => base + | some p => fields ++ [ ("stage1-prove-time", jsonRound 6 p) + , ("stage1-throughput", + jsonRound 2 (r.constants.toFloat / p)) ] + | none => fields let fields := match r.peakRss with - | some n => fields ++ [ ("peak-rss", Lean.toJson n) ] + | some n => fields ++ [ ("stage1-peak-rss", Lean.toJson n) ] | none => fields let fields := match r.proofSize with - | some n => fields ++ [ ("proof-size", Lean.toJson n) ] + | some n => fields ++ [ ("stage1-proof-size", Lean.toJson n) ] | none => fields let fields := match r.verifySec with - | some v => fields ++ [ ("verify-time", jsonRound 6 v) ] + | some v => fields ++ [ ("stage1-verify-time", jsonRound 6 v) ] | none => fields - -- The recursion metrics (--recursive), in measurement order; the - -- execute-side pair lands before the outer prove runs, so an OOM'd - -- outer prove still leaves them on disk. + -- The stage-2 metrics, in measurement order; the execute-side pair + -- lands before the outer prove runs, so an OOM'd outer prove still + -- leaves them on disk. let fields := match r.recursiveExecuteSec, r.recursiveFftCost with - | some s, some c => fields ++ [ ("recursive-execute-time", jsonRound 6 s) - , ("recursive-fft-cost", jsonRound 0 c) ] + | some s, some c => fields ++ [ ("stage2-execute-time", jsonRound 6 s) + , ("stage2-fft-cost", jsonRound 0 c) ] | _, _ => fields let fields := match r.recursiveProveSec with - | some s => fields ++ [ ("recursive-prove-time", jsonRound 6 s) ] + | some s => fields ++ [ ("stage2-prove-time", jsonRound 6 s) + , ("stage2-throughput", + jsonRound 2 (r.constants.toFloat / s)) ] | none => fields let fields := match r.recursivePeakRss with - | some n => fields ++ [ ("recursive-peak-rss", Lean.toJson n) ] + | some n => fields ++ [ ("stage2-peak-rss", Lean.toJson n) ] | none => fields let fields := match r.recursiveProofSize with - | some n => fields ++ [ ("recursive-proof-size", Lean.toJson n) ] + | some n => fields ++ [ ("stage2-proof-size", Lean.toJson n) ] | none => fields let fields := match r.recursiveVerifySec with - | some v => fields ++ [ ("recursive-verify-time", jsonRound 6 v) ] + | some v => fields ++ [ ("stage2-verify-time", jsonRound 6 v) ] | none => fields -- The pipeline ledger, once the whole pipeline has run. -- `total-time` is each stage's prove, summed. A stage's prove is -- the WHOLE cost of producing that stage's proof: `prove_ixvm` runs -- the executor itself (the `aiur/execute_ixvm` span) before - -- generating the witness, so the Phase-1 `execute-time` beside it is + -- generating the witness, so the `stage1-execute-time` beside it is -- a SECOND, standalone run — instrumentation for `constants` and - -- `fft-cost`, not a step of proving. Adding the two would count the - -- execution twice. Verification is likewise excluded: a consumer - -- cost, not a production one. + -- `stage1-fft-cost`, not a step of proving. Adding the two would + -- count the execution twice. Verification is likewise excluded: a + -- consumer cost, not a production one. + -- `pipeline-throughput` is `constants` over `total-time` — the + -- end-to-end checking rate, per-stage throughputs being scoped to + -- their own prove. -- `pipeline-peak-rss` is the whole run's RAM high-water: the -- per-phase windows reset, so no single `peak-rss` answers "how much -- RAM does this pipeline need" — their maximum does. Emitted @@ -296,7 +304,9 @@ def Result.toJsonEntry (executeOnly : Bool) (r : Result) : String × Json := let fields := match r.proveSec, r.recursiveExecuteSec, r.recursiveProveSec with | some p, some _, some rp => let peaks := [r.executePeakRss, r.peakRss, r.recursivePeakRss].reduceOption - fields ++ [ ("total-time", jsonRound 6 (p + rp)) ] + fields ++ [ ("total-time", jsonRound 6 (p + rp)) + , ("pipeline-throughput", + jsonRound 2 (r.constants.toFloat / (p + rp))) ] ++ (match peaks.max? with | some n => [("pipeline-peak-rss", Lean.toJson n)] | none => []) @@ -575,9 +585,9 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do , proofSize := some proofBytes.size, verifySec := verifySec? }, addr) writeJson (ordered.map (·.1)) -- Phase 3 (--recursive): the in-circuit verifier over the fresh - -- proof — execute it (recursive-execute-time / recursive-fft-cost), then prove - -- that execution (recursive-prove-time / recursive-peak-rss / - -- recursive-proof-size / recursive-verify-time). A reject on the execute + -- proof — execute it (stage2-execute-time / stage2-fft-cost), then prove + -- that execution (stage2-prove-time / stage2-peak-rss / + -- stage2-proof-size / stage2-verify-time). A reject on the execute -- is a correctness alarm, reported loudly with the recursive fields -- left absent — never a benchmark datum. if let some (vCompiled, vIdx, vSystem) := vCtx then @@ -598,7 +608,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let rvStats := Aiur.computeStats vCompiled qc vSystem.circuitShapes (logBlowup := commitParams.logBlowup) IO.println s!" {r.name}: recursive={rvSec}s \ - recursive-fft-cost={rvStats.totalFftCost}" + stage2-fft-cost={rvStats.totalFftCost}" -- The per-circuit breakdown names where the verifier's cost -- lives (deserialization vs blake3 vs FRI); texray-gated like -- the other detailed diagnostics. @@ -626,8 +636,8 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do | .error e => IO.eprintln s!" outer verify {r.name} FAILED: {e}" pure none - IO.println s!" {r.name}: recursive-prove={rvProveSec}s \ - recursive-verify={rvVerifySec}s outer proof={rvProofBytes.size} bytes" + IO.println s!" {r.name}: stage2-prove={rvProveSec}s \ + stage2-verify={rvVerifySec}s outer proof={rvProofBytes.size} bytes" let (row, _) := ordered[i]! ordered := ordered.set! i ({ row with recursiveProveSec := some rvProveSec @@ -654,7 +664,7 @@ def typecheckCmd : Cli.Cmd := `[Cli| "json" : String; "Write per-constant results JSON to this path. 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`." "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." + "recursive"; "After each prove, execute and then prove the in-circuit multi-stark verifier over the fresh proof (the stage2-* 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)." texray; "Enable the tracing-texray timeline + RAM breakdown (per-prove spans on stderr). Combined with --json, per-phase span timings are additionally written to `.spans` as JSON Lines for the CI drill-down. Off by default." diff --git a/Benchmarks/Vectors.csv b/Benchmarks/Vectors.csv deleted file mode 100644 index 1e85d04d8..000000000 --- a/Benchmarks/Vectors.csv +++ /dev/null @@ -1,75 +0,0 @@ -# Benchmark constant vectors -- single shared source of truth for which -# constants to run, selected per cell by `ix bench run` (see -# Ix/Cli/BenchCmd.lean, whose registry holds everything that isn't a -# per-constant row). Measurements (fft, cycles, prove-time, …) live in the -# benchmark results JSON each tool emits and in bencher.dev — never here. -# -# Columns (shard_target and primary default to 0 when trailing; most rows only -# carry the first three): -# name fully-qualified Lean name (resolves via NameResolve.resolveIxeAddr). -# env compile target / .ixe it resolves in: InitStd | Lean | Mathlib. -# tier cheap = prove-feasible on a CI runner; heavy = a single-shard -# prove exceeds the RAM watchdog ceiling (expect an OOM row). -# `ix bench run` proves every selected constant regardless of -# tier (--full prove runs default to cheap; --tier overrides); -# heavy zisk constants run as their closure-shard partition, -# pre-cut by `ix bench shard`. -# shard_target 1 = heavy constant designated as a multi-shard prove target -# (--shard-only restricts to these). -# primary 1 = part of the primary subset spanning shape + the -# cheap->heavy cost range. Default for the !benchmark PR -# comment and the bench-main cells (full set via BENCH_FULL=1 -# / --full). -name,env,tier,shard_target,primary -Eq.rec,InitStd,cheap -Except.bind,InitStd,cheap -WellFounded.fix,InitStd,cheap -List.filterMap,InitStd,cheap -BitVec.toFin,InitStd,cheap -Std.HashMap,InitStd,heavy -Nat.add_comm,InitStd,cheap,0,1 -USize.toNat,InitStd,cheap -Nat.decEq,InitStd,cheap -ByteSlice.ofByteArray,InitStd,cheap -Nat.decLe,InitStd,cheap -Nat.strongRecOn,InitStd,cheap -Int.emod,InitStd,cheap -Nat.sub_le_of_le_add,InitStd,cheap,0,1 -BitVec.add,InitStd,cheap -Int.gcd,InitStd,cheap,0,1 -Array.map,InitStd,cheap -Lean.Name.hash,InitStd,cheap -BitVec.umod,InitStd,cheap -Nat.repr,InitStd,cheap -String.intercalate,InitStd,heavy -_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec,InitStd,heavy -Char.toLower,InitStd,heavy -Nat.gcd_comm,InitStd,heavy,0,1 -Int.emod_emod_of_dvd,InitStd,heavy -Array.append_assoc,InitStd,heavy -Vector.append,InitStd,heavy,0,1 -Fin.foldl,InitStd,heavy -List.mergeSort,InitStd,heavy,1,1 -Array.binSearch,InitStd,heavy,1 -Array.qsortOrd,InitStd,heavy -String.split,InitStd,heavy,0,1 -Std.Time.Week.Offset.ofMilliseconds,InitStd,heavy -Vector.extract_append._proof_2,InitStd,heavy,1,1 -ByteArray.utf8DecodeChar?_utf8EncodeChar_append,InitStd,heavy,0,1 -String.append,InitStd,cheap,0,1 -_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq,InitStd,heavy,0,1 -Char.ofOrdinal_le_of_le,InitStd,heavy,0,1 -Array.extract_append,InitStd,heavy,0,1 -Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual,InitStd,heavy,0,1 -Lean.Expr.replace,Lean,cheap -Lean.Json,Lean,heavy,0,1 -List.Sorted,Mathlib,cheap -Nat.choose,Mathlib,cheap -Nat.factorial,Mathlib,cheap,0,1 -Nat.fib,Mathlib,cheap -GCDMonoid.gcd,Mathlib,heavy -Nat.Prime.two_le,Mathlib,heavy -Finset.prod,Mathlib,heavy -Finset.sum,Mathlib,heavy -Polynomial.eval,Mathlib,heavy -Multiset.sort,Mathlib,heavy,1,1 diff --git a/Ix/BenchConstants.lean b/Ix/BenchConstants.lean new file mode 100644 index 000000000..cee6bc26a --- /dev/null +++ b/Ix/BenchConstants.lean @@ -0,0 +1,48 @@ +/- + The shared benchmark constant set: the single source of truth for which + constants every per-constant benchmark backend (aiur, zisk, sp1, ooc, + lean4lean) runs. Every backend runs this same set — spanning the cheap → + heavy cost range across the registry envs — so their numbers stay + comparable per constant; the only per-backend carve-outs are the hard + feasibility exclusions in `Ix.Cli.BenchCmd.benchExclusions`. + + `env` names the registry env (`Ix.Cli.BenchCmd.envSpecs` / + `.ixe`) the constant resolves in. Whether a zisk execution runs + whole or as a closure-shard partition is decided at bench runtime by + the shard planner's budget, not declared here. +-/ +module + +public section + +namespace Ix.BenchConstants + +/-- One benchmark constant: a fully-qualified Lean name and the registry + env it resolves in. -/ +structure BenchConstant where + name : String + env : String + +def benchConstants : Array BenchConstant := #[ + { name := "Nat.add_comm", env := "InitStd" }, + { name := "String.append", env := "InitStd" }, + { name := "Array.extract_append", env := "InitStd" }, + { name := "ByteArray.utf8DecodeChar?_utf8EncodeChar_append", + env := "InitStd" }, + { name := "_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq", + env := "InitStd" }, + { name := "Char.ofOrdinal_le_of_le", env := "InitStd" }, + { name := "Std.HashMap", env := "InitStd" }, + -- TODO: re-add bitblast once a prover can carry it. Its ~18B-step + -- atomic mutual block crashes the zkVM executors (`benchExclusions`) + -- and exceeds any current host's RAM on the Aiur prove, so a scheduled + -- run could only re-document the same OOM every push. Until then it + -- runs on demand via `--consts` / BENCH_CONSTS, which bypass the + -- curated set. + -- { name := "Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual", + -- env := "InitStd" }, + { name := "Lean.Json", env := "Lean" }, + { name := "Multiset.sort", env := "Mathlib" } +] + +end Ix.BenchConstants diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index c68bd30d3..015d733d1 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -5,8 +5,8 @@ A run executes one parameter combination: (backend, env, mode). The orchestrator: - 1. selects constant names from `Benchmarks/Vectors.csv` (filters ported - from the `!benchmark` manifest: env, tier, primary subset, shard flag); + 1. selects the env's constants from the shared set + (`Ix.BenchConstants`), minus the `(backend, mode)` exclusions; 2. resolves the env's `.ixe` (an explicit `--ixe` path, else `ix compile` — except for the `compile` backend, where the compile IS the benchmark); @@ -37,6 +37,7 @@ module public import Cli public import Lean.Data.Json +public import Ix.BenchConstants public import Ix.Benchmark.Results public import Ix.Cli.ConstsFile @@ -44,107 +45,40 @@ public section open System (FilePath) open Ix.Benchmark.Results +open Ix.BenchConstants namespace Ix.Cli.BenchCmd -/-- One `Vectors.csv` row (comments/header dropped). `shardTarget` and - `primary` default to false when the trailing columns are omitted. -/ -structure VectorRow where - name : String - env : String - tier : String - shardTarget : Bool - primary : Bool - -def parseVectorsCsv (contents : String) : Array VectorRow := - (contents.splitOn "\n").filterMap (fun line => - let s := ((line.splitOn "#").head?.getD "").trimAscii.toString - if s.isEmpty then none else - let cols := (s.splitOn ",").map (·.trimAscii.toString) - match cols with - | name :: env :: tier :: rest => - if name == "name" || name.isEmpty then none - else some { - name, env, tier - shardTarget := rest.head?.getD "0" == "1" - primary := (rest.drop 1).head?.getD "0" == "1" - } - | _ => none) |>.toArray - /-- Per-constant benchmark exclusions: `(name, backend, mode)` a constant must NOT run for, `"*"` wildcarding a dimension. Applied on top of the - `Vectors.csv` selection, for constants feasible in some cells but not - others — a closure that executes on Aiur but OOMs the Zisk/SP1 zkVM - executor, or one that executes but is prove-infeasible. `--consts` runs - bypass this: an explicit request always runs. -/ + shared `benchConstants` set, for the constants that are hard-infeasible + in a cell — not merely expensive (a too-large prove records an honest + `oom` row instead). `--consts` runs bypass this: an explicit request + always runs. -/ def benchExclusions : List (String × String × String) := let bitblast := "Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual" [ -- ~18B-step atomic mutual block: Aiur executes it, but the zkVM - -- executor OOMs (ASM MO crash) and no single-shard prove fits. + -- executor OOMs (ASM MO crash) before any measurement lands. (bitblast, "zisk", "*"), - (bitblast, "sp1", "*"), - (bitblast, "aiur", "prove"), - -- Executes on Aiur (and the zkVMs) but is Aiur-prove-infeasible. - ("Lean.Json", "aiur", "prove") ] + (bitblast, "sp1", "*") ] /-- Whether `benchExclusions` bars `name` from this `(backend, mode)`. -/ def isExcluded (name backend mode : String) : Bool := benchExclusions.any fun (n, b, m) => n == name && (b == "*" || b == backend) && (m == "*" || m == mode) -/-- `(backend, mode)` combinations whose default selection is this fixed - name list instead of the `Vectors.csv` primary subset. The primary - subset is sized for a one-prove benchmark; a run that walks the whole - proof pipeline pays every stage per constant, so its default set is - sized to what one CI host can finish. `--full`, `--shard-only`, and an - explicit `--consts` request all bypass it, and the names still have to - be `Vectors.csv` rows of the env being run — this narrows the curated - selection, it does not add to it. -/ -def fixedSelections : List (String × String × List String) := - [ -- The aiur pipeline's cost range: two cheap-tier constants for the - -- small end, and four heavy-tier ones for the expensive end, where - -- the stage-2 prover meets the host's RAM ceiling. - ("aiur", "prove", - ["Nat.add_comm", - "String.append", - "Array.extract_append", - "ByteArray.utf8DecodeChar?_utf8EncodeChar_append", - "_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq", - "Char.ofOrdinal_le_of_le"]) ] - -/-- The fixed default selection for this `(backend, mode)`, if any. -/ -def fixedSelectionFor (backend mode : String) : Option (List String) := - (fixedSelections.find? fun (b, m, _) => - b == backend && (m == "*" || m == mode)).map (·.2.2) - -/-- Manifest selection, mirroring the `!benchmark` config surface: the env's - rows, restricted to the primary subset — or the `(backend, mode)`'s - `fixedSelections` list where it has one — unless `full`, to `tier` when - given (prove-mode full runs default to `cheap` — the prove-feasible - set), to shard targets under `shardOnly`, and minus the - `(backend, mode)` exclusions in `benchExclusions`. -/ -def selectNames (rows : Array VectorRow) (env : String) (backend : String) - (mode : String) (full : Bool) (tier : String) (shardOnly : Bool) : - Array VectorRow := Id.run do - let effTier := - if tier != "" then tier - else if mode == "prove" && full then "cheap" - else "all" - let fixed := if full || shardOnly then none - else fixedSelectionFor backend mode - rows.filter fun r => - r.env == env - && (match fixed with - | some names => names.contains r.name - | none => full || r.primary) - && (effTier == "all" || r.tier == effTier) - && (!shardOnly || r.shardTarget) - && !isExcluded r.name backend mode +/-- The env's slice of the shared `benchConstants` set, minus the + `(backend, mode)` exclusions — the one selection every per-constant + backend runs. -/ +def selectNames (env : String) (backend : String) (mode : String) : + Array BenchConstant := + benchConstants.filter fun c => + c.env == env && !isExcluded c.name backend mode /-! ## The registry — single source of truth for the benchmark pipeline -`Benchmarks/Vectors.csv` holds the per-constant rows; everything else lives +`Ix.BenchConstants` holds the shared constant set; everything else lives here, in one language with one owner. The workflows never read it directly: `ix bench ci matrix` serves the job matrices and `ix bench ci parse` the `!benchmark` runs, both post-build. (`bencher-thresholds-reset.yml` keeps @@ -176,10 +110,10 @@ def findEnv (token : String) : Option EnvSpec := · `perEnv` — one row per compiled env, keyed by the env name itself; runs over EVERY compiled env. The env-keyed compile/decompile pair: a `.ixe` producer and its consumer, both measuring the whole env. - · `perConstant` — one row per selected `Vectors.csv` constant, over - the envs whose CSV rows select any — an env joins this fan-out by - gaining rows, not by a registry flag. The prove/execute backends - (aiur, zisk, sp1). + · `perConstant` — one row per selected `benchConstants` entry, over + the envs whose entries select any — an env joins this fan-out by + gaining constants, not by a registry flag. The prove/execute + backends (aiur, zisk, sp1). · `perConstantWithEnv` — `perConstant` plus a whole-env row (ooc). -/ inductive BenchInputs | perEnv @@ -194,10 +128,31 @@ def workloadOf (testbed : String) : String := if testbed.endsWith "-x64-32x" then (testbed.dropEnd 8).toString else testbed +/-- The stage qualifier a pipeline measure carries ahead of its base name, + if any: `stage-` scopes a measure to pipeline stage N (any number + of stages — the KZG stages join as `stage3-`/`stage4-` without + touching this), `pipeline-` to the whole run. Stripped wherever a + measure is interpreted by its base name (formatting kind, units) or + labelled under a heading that already says the stage. -/ +def stagePrefixOf (metric : String) : Option String := + if metric.startsWith "pipeline-" then some "pipeline-" else + if !metric.startsWith "stage" then none else + let digits := + (metric.drop "stage".length).toString.toList.takeWhile (·.isDigit) + if digits.isEmpty then none else + let p := s!"stage{String.ofList digits}-" + if metric.startsWith p then some p else none + +/-- `metric` with its stage qualifier removed, if it has one. -/ +def dropStagePrefix (metric : String) : String := + match stagePrefixOf metric with + | some p => (metric.drop p.length).toString + | none => metric + /-- One benchmark backend. Backends with several modes schedule one bench-main - matrix entry per (mode, testbed) — shared measure names (`peak-rss`, - `throughput`) mean that mode's phase, and a `!benchmark` request of either - mode finds a cached bencher baseline. -/ + matrix entry per (mode, testbed); each mode's measures live on its own + testbed (aiur's pipeline mode stage-qualifies its measure names, while + its standalone execute mode keeps the plain Phase-1 names). -/ structure BackendSpec where name : String defaultMode : String @@ -223,10 +178,11 @@ structure BackendSpec where metrics : List (String × List String) /-- (mode, [(stage title, that stage's measures)]) for a mode whose run walks a multi-stage pipeline: the compare table splits into one - table per stage, so a stage's measures keep their plain names - (`prove-time`, `peak-rss`) across stages instead of competing for - one row. List order is render order, so the closing entry is the - ledger over the whole run. -/ + table per stage. A stage's measures carry their `stage-` + qualifier (`stage1-prove-time`) — the stage tables strip it for + display (`sectionLabelDrop`), so columns still read plain. List + order is render order, so the closing entry is the ledger over the + whole run. -/ stages : List (String × List (String × List String)) := [] /-- Regression bounds per tracked measure: (measure, upper, lower), each bound a percentage over the baseline as a decimal fraction ("0.10"), @@ -271,17 +227,19 @@ def backendSpecs : List BackendSpec := [ unscheduled := ["execute"], stages := [("prove", [("Stage 1 — IxVM on FRI", - ["execute-time", "prove-time", "peak-rss", "proof-size", - "verify-time", "fft-cost"]), + ["stage1-execute-time", "stage1-prove-time", "stage1-throughput", + "stage1-peak-rss", "stage1-proof-size", "stage1-verify-time", + "stage1-fft-cost"]), ("Stage 2 — FRI recursion on FRI", - ["recursive-execute-time", "recursive-prove-time", - "recursive-peak-rss", "recursive-proof-size", - "recursive-verify-time", "recursive-fft-cost"]), - ("Pipeline total", ["total-time", "pipeline-peak-rss"])])], + ["stage2-execute-time", "stage2-prove-time", "stage2-throughput", + "stage2-peak-rss", "stage2-proof-size", "stage2-verify-time", + "stage2-fft-cost"]), + ("Pipeline total", + ["total-time", "pipeline-throughput", "pipeline-peak-rss"])])], metrics := [("execute", ["execute-time", "throughput", "peak-rss", "fft-cost"])], - -- fft-cost is deterministic but only ever drops on a real Aiur win → - -- upper-only 5% instead of a hard pin. recursive-fft-cost drifts + -- stage1-fft-cost is deterministic but only ever drops on a real Aiur + -- win → upper-only 5% instead of a hard pin. stage2-fft-cost drifts -- ~±15% run-to-run (the parallel prover emits byte-different valid -- proofs, so the verifier authenticates different Merkle paths) → -- the loose 25% bound. Proof sizes are structural (fixed query count @@ -289,18 +247,21 @@ def backendSpecs : List BackendSpec := [ -- is the two prove times summed, and a sum cannot breach a -- percentage bound unless one of its terms already breached the same -- one — so it could only ever duplicate an alert the proves fired. - thresholds := [("constants", "0", "0"), ("fft-cost", "0.05", "_"), - ("recursive-fft-cost", "0.25", "_"), - ("execute-time", "0.10", "_"), ("prove-time", "0.10", "_"), - ("recursive-execute-time", "0.10", "_"), - ("recursive-prove-time", "0.10", "_"), - ("peak-rss", "0.10", "_"), - ("recursive-peak-rss", "0.10", "_"), + -- The throughputs likewise carry no bound: `constants` is pinned + -- exactly, so each is the pure inverse of an already-bounded time. + thresholds := [("constants", "0", "0"), ("stage1-fft-cost", "0.05", "_"), + ("stage2-fft-cost", "0.25", "_"), + ("stage1-execute-time", "0.10", "_"), + ("stage1-prove-time", "0.10", "_"), + ("stage2-execute-time", "0.10", "_"), + ("stage2-prove-time", "0.10", "_"), + ("stage1-peak-rss", "0.10", "_"), + ("stage2-peak-rss", "0.10", "_"), ("pipeline-peak-rss", "0.10", "_"), - ("proof-size", "0.05", "_"), - ("recursive-proof-size", "0.05", "_"), - ("verify-time", "0.10", "_"), - ("recursive-verify-time", "0.10", "_")] }, + ("stage1-proof-size", "0.05", "_"), + ("stage2-proof-size", "0.05", "_"), + ("stage1-verify-time", "0.10", "_"), + ("stage2-verify-time", "0.10", "_")] }, { name := "zisk", defaultMode := "execute", inputs := .perConstant, testbeds := [("execute", "zisk-check-execute-x64-32x")], metrics := [("execute", ["execute-time", "throughput", "peak-rss", @@ -330,7 +291,7 @@ def backendSpecs : List BackendSpec := [ -- yardstick for the Ix kernels (`ooc` / `ix check-lean`) on the same -- libraries. Checks the env's library from its oleans (no `.ixe`): -- whole-library row (module-parallel replay of the import closure) plus - -- one full-closure row per primary, mirroring ooc's row shape and + -- one full-closure row per constant, mirroring ooc's row shape and -- metric names so cross-kernel tables line up. Disabled in CI until a -- bencher testbed exists — `ix bench run --backend lean4lean` works -- locally regardless (`disabled` only gates the CI matrix and @@ -406,37 +367,34 @@ def BackendSpec.scheduledModes (b : BackendSpec) : List String := /-- The envs this backend's runs cover, from its `inputs`: `perEnv` covers every registry env; the per-constant backends cover the envs where at - least one primary constant is selected in ANY scheduled mode — an env - joins their fan-out by gaining rows, not by a registry flag, and a - constant excluded from one mode (e.g. prove) still keeps its env if - another scheduled mode (e.g. execute) runs it. -/ -def BackendSpec.envNames (b : BackendSpec) (rows : Array VectorRow) : - List String := + least one constant is selected in ANY scheduled mode — an env joins + their fan-out by gaining constants, not by a registry flag, and a + constant excluded from one mode still keeps its env if another + scheduled mode runs it. -/ +def BackendSpec.envNames (b : BackendSpec) : List String := let names := envSpecs.map (·.name) match b.inputs with | .perEnv => names | .perConstant | .perConstantWithEnv => names.filter fun env => b.scheduledModes.any fun m => - !(selectNames rows env b.name m - (full := false) (tier := "") (shardOnly := false)).isEmpty + !(selectNames env b.name m).isEmpty /-- The benchmark row names this backend uploads — the bencher slugs the dashboard plots and compare table key on — from its `inputs`: env-keyed backends key one row per compiled env; the per-constant backends select - from `Vectors.csv` over their env set (`perConstantWithEnv` prepends a - whole-env row). Dynamic shard sub-rows (`/shard-N`) are + from `benchConstants` over their env set (`perConstantWithEnv` prepends + a whole-env row). Dynamic shard sub-rows (`/shard-N`) are excluded — the parent row carries the headline trend. -/ -def BackendSpec.benchmarkNames (b : BackendSpec) (rows : Array VectorRow) - (mode : String) : Array String := Id.run do +def BackendSpec.benchmarkNames (b : BackendSpec) (mode : String) : + Array String := Id.run do match b.inputs with | .perEnv => return (envSpecs.map (·.name)).toArray | .perConstant | .perConstantWithEnv => let mut ns : Array String := #[] - for env in b.envNames rows do + for env in b.envNames do if b.inputs == .perConstantWithEnv then ns := ns.push env - ns := ns ++ (selectNames rows env b.name mode - (full := false) (tier := "") (shardOnly := false)).map (·.name) + ns := ns ++ (selectNames env b.name mode).map (·.name) return ns /-- Default RAM watchdog ceiling, same rule for all backends: the @@ -599,7 +557,7 @@ def ensureIxe (repo : String) (info : EnvSpec) (explicit : Option String) : throw <| IO.userError s!"ix compile {info.module} failed (exit {exit})" return ixe -/-- Cut the closure-shard artifacts for one heavy constant: `ix shard +/-- Cut the closure-shard artifacts for one constant: `ix shard extract` (standalone closure env) → `ix profile` → `ix shard` (heartbeat-profiled min-cut manifest, capped by predicted RAM). Skips work when the artifacts already exist. Returns `(ixe, ixes)` on @@ -690,8 +648,6 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do let mode := (p.flag? "mode").map (·.as! String) |>.getD spec.defaultMode let repo := (p.flag? "repo").map (·.as! String) |>.getD "." let out := (p.flag? "out").map (·.as! String) |>.getD "bench.json" - let full := p.hasFlag "full" - let tier := (p.flag? "tier").map (·.as! String) |>.getD "" let ceilingGb : Nat ← match p.flag? "ceiling-gb" with | some f => pure (f.as! Nat) | none => defaultCeilingGb @@ -706,23 +662,14 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do else do p.printError s!"error: no watchdog at {watchdogPath} (--watchdog overrides)" return exitUsage - let csv := (p.flag? "csv").map (·.as! String) - |>.getD s!"{repo}/Benchmarks/Vectors.csv" - let rows := parseVectorsCsv (← IO.FS.readFile csv) - -- `--consts` overrides the CSV selection — a one-off local run, or - -- bench-pr's targeted base run over just the constants bencher lacked; - -- tier metadata still comes from the CSV so heavy zisk names keep - -- their sharded pipeline. + -- `--consts` overrides the shared-set selection — a one-off local run, + -- or bench-pr's targeted base run over just the constants bencher + -- lacked. let wanted := ((p.flag? "consts").map (fun f => Ix.Cli.ConstsFile.parseCommaList (f.as! String))).getD #[] - let selected := - if wanted.isEmpty then - selectNames rows env backend mode full tier (p.hasFlag "shard-only") - else - wanted.map fun n => - (rows.find? (fun r => r.name == n && r.env == env)).getD - { name := n, env, tier := "cheap", shardTarget := false, primary := false } - let names := selected.map (·.name) + let names := + if wanted.isEmpty then (selectNames env backend mode).map (·.name) + else wanted IO.eprintln s!"[bench] run {backend}-{env}-{mode}: {names.size} constant(s)" -- Fresh accumulator per run. @@ -761,7 +708,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do "--per-const", s!"{out}.perconst.csv"] if exit != 0 && exit != exitRejected then IO.eprintln s!"[bench] whole-env check failed (exit {exit})" - -- … plus one full-closure row per primary. ONE process for all names + -- … plus one full-closure row per constant. ONE process for all names -- (unlike the per-constant backends below): the check-rs rows mode -- attributes per name internally with the env loaded once — a -- per-constant process would re-pay the multi-minute Mathlib env parse @@ -784,7 +731,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do #[modulePath, "--json", out, "--json-name", info.name] if exit != 0 && exit != exitRejected then IO.eprintln s!"[bench] whole-library replay failed (exit {exit})" - -- … plus one full-closure row per primary. ONE process for all names + -- … plus one full-closure row per constant. ONE process for all names -- (the ooc pattern): the imported env is shared across the closure -- replays instead of re-paying the library import per name. if !names.isEmpty then @@ -825,20 +772,20 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do IO.eprintln s!"[bench] cargo build {host} failed (exit {build})" return 1 let bin := (← IO.FS.realPath s!"{work}/target/release/{host}").toString - -- Heavy-tier zisk constants run as their closure-shard partition (a - -- single full-closure leaf would blow the runner's RAM); everything - -- else runs as one host process per constant like the aiur runs. - let heavy := if backend == "zisk" - then (selected.filter (·.tier == "heavy")).map (·.name) else #[] - let light := names.filter (!heavy.contains ·) - runPerConstant outAbs light "execute-time" fun name => - runGuarded watchdog ceilingGb bin - #["--execute", "--ixe", ixeAbs, "--consts", name, - "--json", outAbs, "--texray"] (cwd := some work) + -- zisk decides sharding at run time, per constant: the closure is + -- extracted and profiled, and the shard planner's RAM budget sizes + -- the partition from the closure's predicted cost — a closure that + -- fits gets a one-shard plan and runs as a single leaf. The artifacts + -- are cached under `zkshards-/` (pre-cut next to the fresh + -- `.ixe` by `ix bench shard` when available). A failed cut falls + -- back to the whole closure from the env's `.ixe` — the watchdog + -- then records the honest OOM row if it doesn't fit. sp1 always + -- runs whole closures. let ix ← resolveBin repo "ix" - runPerConstant outAbs heavy "execute-time" fun name => do - let plan ← cutClosureShards ix ixe s!"{repo}/zkshards-{env}" - name ceilingGb + runPerConstant outAbs names "execute-time" fun name => do + let plan ← if backend == "zisk" + then cutClosureShards ix ixe s!"{repo}/zkshards-{env}" name ceilingGb + else pure none match plan with | some (subIxe, manifest) => runGuarded watchdog ceilingGb bin @@ -867,7 +814,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do return code /-- `ix bench shard`: pre-cut the closure-shard artifacts for the env's - heavy-tier constants into `zkshards-/` — `ix shard extract` → + zisk constants into `zkshards-/` — `ix shard extract` → `ix profile` → `ix shard` per name, skipping names whose artifacts already exist. Not a benchmark run (no rows, no watchdog): bench-main's compile job runs it next to the fresh `.ixe` so the artifacts ride the @@ -882,15 +829,11 @@ def runBenchShardCmd (p : Cli.Parsed) : IO UInt32 := do let ceilingGb : Nat ← match p.flag? "ceiling-gb" with | some f => pure (f.as! Nat) | none => defaultCeilingGb - let csv := (p.flag? "csv").map (·.as! String) - |>.getD s!"{repo}/Benchmarks/Vectors.csv" - let rows := parseVectorsCsv (← IO.FS.readFile csv) - let heavy := (rows.filter fun r => - r.env == env && r.primary && r.tier == "heavy").map (·.name) - IO.eprintln s!"[bench] shard {env}: {heavy.size} heavy constant(s)" + let names := (selectNames env "zisk" "execute").map (·.name) + IO.eprintln s!"[bench] shard {env}: {names.size} constant(s)" let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String)) let ix ← resolveBin repo "ix" - for name in heavy do + for name in names do let _ ← cutClosureShards ix ixe s!"{repo}/zkshards-{env}" name ceilingGb return 0 @@ -907,11 +850,7 @@ def benchRunCmd : Cli.Cmd := `[Cli| mode : String; "prove | execute (default: the backend's defaultMode)" out : String; "Benchmark results JSON output path (default: bench.json)" repo : String; "Checkout to benchmark: tools resolve from /.lake/build/bin first, then PATH (default: .)" - csv : String; "Vectors path (default: /Benchmarks/Vectors.csv)" - full; "Run the env's full curated set instead of the primary subset" - consts : String; "Run exactly these comma-separated names instead of the Vectors.csv selection (same grammar as the tools' --consts)" - tier : String; "cheap | heavy | all — tier filter (default: all; prove-mode --full defaults to cheap)" - "shard-only"; "Restrict to shard_target rows" + consts : String; "Run exactly these comma-separated names instead of the shared benchConstants selection (same grammar as the tools' --consts)" ixe : String; "Path to an existing .ixe env to use (default: compile fresh; ignored by the compile backend)" "ceiling-gb" : Nat; "RAM watchdog ceiling in GB (default: machine RAM minus 15 GB)" watchdog : String; "Watchdog wrapper path (default: /.github/scripts/watchdog.sh; missing = run unguarded)" @@ -920,12 +859,11 @@ def benchRunCmd : Cli.Cmd := `[Cli| open Ix.Cli.BenchCmd in def benchShardCmd : Cli.Cmd := `[Cli| "shard" VIA runBenchShardCmd; - "Pre-cut closure-shard artifacts (ix shard extract → profile → shard) for the env's heavy-tier constants into zkshards-/; skips names already cut. The zisk runs cut lazily when these are absent — this front-loads the work so the artifacts can be cached once per commit." + "Pre-cut closure-shard artifacts (ix shard extract → profile → shard) for the env's zisk constants into zkshards-/; skips names already cut. The zisk runs cut lazily when these are absent — this front-loads the work so the artifacts can be cached once per commit." FLAGS: env : String; "Benchmark env from the registry (default: InitStd)" repo : String; "Checkout to shard: tools resolve from /.lake/build/bin first, then PATH (default: .)" - csv : String; "Vectors path (default: /Benchmarks/Vectors.csv)" ixe : String; "Path to an existing .ixe env to use (default: compile fresh)" "ceiling-gb" : Nat; "Predicted-RAM cap per shard, passed to `ix shard --max-ram` (default: machine RAM minus 15 GB)" ] diff --git a/Ix/Cli/BenchPlots.lean b/Ix/Cli/BenchPlots.lean index 29a9d2a97..6aae4f2c8 100644 --- a/Ix/Cli/BenchPlots.lean +++ b/Ix/Cli/BenchPlots.lean @@ -1,10 +1,10 @@ /- `ix bench plots`: sync the bencher.dev dashboard plots to the benchmark registry — one plot per (testbed, measure) that bench-main.yml tracks, - with one line per benchmark row uploaded there, plus two cross-cutting - plots: the shared input-constants trend and the Zisk-shards-per-heavy- - primary trend. The spec derives from the registry - (`Ix.Cli.BenchCmd`) + `Vectors.csv`, so nothing is hand-listed, and + with one line per benchmark row uploaded there, plus the cross-cutting + shared input-constants trend. The spec derives from the registry + (`Ix.Cli.BenchCmd`) + the shared constant set (`Ix.BenchConstants`), so + nothing is hand-listed, and every join is on the bencher SLUG (the row-key identity uploads use; display names are console-editable and never consulted). @@ -14,8 +14,8 @@ endpoint only takes index/title/window, not dimensions). The registry owns the dashboard: every plot whose title is not in the desired set is deleted, so each sync converges to exactly the registry's plots — a - hand-created plot does not survive a sync. A registry benchmark - — or a whole testbed — bencher hasn't seen yet (first upload still + hand-created plot does not survive a sync. A registry benchmark, + measure, or whole testbed bencher hasn't seen yet (first upload still pending) is skipped with a warning and picked up on the next sync. The sync also asserts every measure's canonical units (`unitsFor`) — @@ -60,25 +60,27 @@ def plotTitle (workload measure : String) : String := | "ix-decompile", "throughput" => "Ix Decompile Throughput" | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage" | "aiur", "total-time" => "Aiur Total Time" - | "aiur", "prove-time" => "Aiur Stage 1 Time" - | "aiur", "recursive-prove-time" => "Aiur Stage 2 Time" - | "aiur", "fft-cost" => "Aiur Stage 1 FFT Cost" - | "aiur", "recursive-fft-cost" => "Aiur Stage 2 FFT Cost" - | "aiur", "recursive-verify-time" => "Aiur Stage 2 Verify Time" - | "aiur", "recursive-peak-rss" => "Aiur Stage 2 Peak RAM Usage" - | "aiur", "recursive-proof-size" => "Aiur Stage 2 Proof Size" + | "aiur", "pipeline-throughput" => "Aiur Total Throughput" + | "aiur", "pipeline-peak-rss" => "Aiur Total Peak RAM Usage" + | "aiur", "stage1-prove-time" => "Aiur Stage 1 Time" + | "aiur", "stage2-prove-time" => "Aiur Stage 2 Time" + | "aiur", "stage1-fft-cost" => "Aiur Stage 1 FFT Cost" + | "aiur", "stage2-fft-cost" => "Aiur Stage 2 FFT Cost" + | "aiur", "stage2-verify-time" => "Aiur Stage 2 Verify Time" + | "aiur", "stage2-peak-rss" => "Aiur Stage 2 Peak RAM Usage" + | "aiur", "stage1-proof-size" => "Aiur Stage 1 Proof Size" + | "aiur", "stage2-proof-size" => "Aiur Stage 2 Proof Size" | "zisk-check-execute", "execute-time" => "Zisk Execute Time" | "zisk-check-execute", "throughput" => "Zisk Execute Throughput" | "zisk-check-execute", "peak-rss" => "Zisk Execute Peak RAM Usage" | "zisk-check-execute", "cycles" => "Zisk Cycles" + | "zisk-check-execute", "shards" => "Zisk Shards" | "ooc-check", "check-time" => "OOC Check Time" | "ooc-check", "throughput" => "OOC Check Throughput" | "ooc-check", "peak-rss" => "OOC Check Peak RAM Usage" | w, m => s!"{w}: {m}" -/-- Tracked but not plotted solo. Zisk `shards` is charted below - over the heavy-tier primaries alone (light constants are pinned at a - single shard, a flat line at 1), not over the full set here; zisk +/-- Tracked but not plotted solo. Zisk `constants` charts on the input-constants plot below instead of alone. `ix-decompile` reuses the compile run's `.ixe`, so its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix Input Constants" @@ -87,23 +89,32 @@ def plotTitle (workload measure : String) : String := that stage's `prove-time` — a prove runs its own witness execution, so it is the whole cost of producing the stage's proof, and the standalone `execute-time` beside it is a second, instrumentation-only - run. The rest of the stage detail (stage-1 peak-rss / proof-size / - verify-time, and the whole-run `pipeline-peak-rss`) is tracked for - the compare table but not plotted: the stage-1 detail's cost is - inside `prove-time` and the deterministic `fft-cost` trend, and the - pipeline peak is the terminal stage's peak. -/ + run. Stage-1 peak-rss / verify-time are tracked for the compare + table but not plotted: their cost is inside `prove-time` and the + deterministic `fft-cost` trend, and stage 1's proof is an + intermediate artifact consumed by the next stage. Stage-1 + `proof-size` IS plotted: it sizes the next stage's in-circuit + verification workload. The whole-run `pipeline-peak-rss` too: which stage + sets the run's RAM ceiling can shift as pipeline stages are added, + so no per-stage peak plot stands in for it. The per-stage + throughputs are table columns only — over the exactly-pinned + `constants` they are the plotted stage times inverted — while the + end-to-end `pipeline-throughput` gets the backend's one throughput + plot, comparable with the other backends'. -/ def plotSkips : List (String × String) := - [("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"), + [("zisk-check-execute", "constants"), ("ix-decompile", "file-size"), ("ix-decompile", "constants"), - ("aiur", "peak-rss"), ("aiur", "proof-size"), ("aiur", "verify-time"), - ("aiur", "execute-time"), ("aiur", "recursive-execute-time"), - ("aiur", "pipeline-peak-rss")] + ("aiur", "stage1-peak-rss"), ("aiur", "stage1-verify-time"), + ("aiur", "stage1-execute-time"), ("aiur", "stage2-execute-time"), + ("aiur", "stage1-throughput"), ("aiur", "stage2-throughput")] /-- Canonical units per measure slug, asserted on every sync: bencher auto-creates a measure with placeholder units ("Measure (units)") on its first upload, leaving plots unitless — and a console edit would drift from this list, so the sync re-asserts it. Phase spans are - wall-clock seconds. -/ + wall-clock seconds. A stage-qualified slug (`stage1-prove-time`, + `pipeline-peak-rss`) carries its base measure's units, so only base + names are listed. -/ def unitsFor (slug : String) : Option String := if slug.startsWith "phase-" then some "seconds (s)" else [("execute-peak-rss", "bytes (B)"), @@ -113,6 +124,7 @@ def unitsFor (slug : String) : Option String := ("prove-time", "seconds (s)"), ("verify-time", "seconds (s)"), ("check-time", "seconds (s)"), + ("total-time", "seconds (s)"), ("peak-rss", "bytes (B)"), ("file-size", "bytes (B)"), ("proof-size", "bytes (B)"), @@ -121,15 +133,8 @@ def unitsFor (slug : String) : Option String := ("max-shard-cycles", "cycles"), ("shards", "shards"), ("fft-cost", "FFTs"), - ("recursive-execute-time", "seconds (s)"), - ("recursive-prove-time", "seconds (s)"), - ("recursive-verify-time", "seconds (s)"), - ("recursive-peak-rss", "bytes (B)"), - ("recursive-proof-size", "bytes (B)"), - ("recursive-fft-cost", "FFTs"), - ("total-time", "seconds (s)"), - ("pipeline-peak-rss", "bytes (B)"), - ("throughput", "constants / second")].lookup slug + ("throughput", "constants / second")].lookup + (BenchCmd.dropStagePrefix slug) /-- Dashboard group order (compile first, then the aiur pipeline, zisk, ooc); unranked workloads (a future backend) sort last. -/ @@ -148,7 +153,7 @@ structure PlotSpec where adds a whole-env row. Dynamic sub-rows (`/shard-N`) are left out: their multiplicity shifts with the shard manifest, and the parent row carries the headline trend. -/ -def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do +def plotSpecs : Array PlotSpec := Id.run do let mut specs : Array PlotSpec := #[] for b in BenchCmd.backendSpecs do if b.disabled.isSome then continue @@ -158,7 +163,7 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do if b.unscheduled.contains mode then continue specs := specs.push { testbed, measures := b.metricsFor mode, - benchmarks := b.benchmarkNames rows mode } + benchmarks := b.benchmarkNames mode } return specs.qsort fun a b => workloadOrder.idxOf (workloadOf a.testbed) < workloadOrder.idxOf (workloadOf b.testbed) @@ -282,14 +287,11 @@ def runPlotsCmd (p : Cli.Parsed) : IO UInt32 := do let branch := (p.flag? "branch").map (·.as! String) |>.getD "main" let window := (p.flag? "window").map (·.as! Nat) |>.getD 7257600 let xAxis := (p.flag? "x-axis").map (·.as! String) |>.getD "version" - let csv := (p.flag? "csv").map (·.as! String) - |>.getD "Benchmarks/Vectors.csv" let dryRun := p.hasFlag "dry-run" if !dryRun && (← IO.getEnv "BENCHER_API_KEY").isNone then p.printError "error: set BENCHER_API_KEY (or pass --dry-run)" return 2 - let rows := BenchCmd.parseVectorsCsv (← IO.FS.readFile csv) - let specs := plotSpecs rows + let specs := plotSpecs let branches ← fetchAll project "branch" let testbeds ← fetchAll project "testbed" @@ -334,53 +336,42 @@ def runPlotsCmd (p : Cli.Parsed) : IO UInt32 := do s!"warn: {spec.testbed}: benchmark '{n}' not on bencher yet — skipped" for measure in spec.measures do if plotSkips.contains (workload, measure) then continue + -- A measure bencher hasn't seen yet (first upload after a rename or + -- a new tracked measure still pending) has no series to plot: warn + -- and skip, like a not-yet-uploaded benchmark or testbed. Its + -- existing plot (if any) is removed below and recreated by a later + -- sync once data lands. let some measureUuid := findUuid measures "slug" measure - | p.printError s!"error: no measure slug '{measure}'"; return 1 + | IO.eprintln s!"warn: measure '{measure}' not on bencher yet — skipped"; continue let title := plotTitle workload measure desired := desired.push { title, testbeds := #[testbedUuid], benchmarks := benchUuids, measure := measureUuid, window := windowFor title window } - -- Input-constants trend over the primary set. aiur and zisk report the - -- SAME named-constant count for each checked closure (the pre-shard input - -- set, unaffected by anon-work dedup or shard partitioning), so the count - -- is shared: sourcing it from both testbeds drew every constant twice. - -- The aiur run is the single source (it always uploads `constants`), - -- so each primary is one line. + -- Input-constants trend over the shared constant set. The kernel + -- backends (aiur, zisk, ooc) report the SAME named-constant count for + -- each checked closure (the pre-shard input set, unaffected by + -- anon-work dedup or shard partitioning), so the count is shared: + -- sourcing it from more than one testbed would draw every constant + -- multiple times. The zisk run is the single source: its sharded + -- execution keeps every closure feasible, so its rows (and their + -- `constants`) upload even where the aiur prove OOMs and the row is + -- dropped; only zisk's excluded names lack a line, and those have no + -- completed upload from any backend. let overlay : Option DesiredPlot := do - let aiurTb ← findUuid testbeds "slug" "aiur-x64-32x" + let ziskTb ← findUuid testbeds "slug" "zisk-check-execute-x64-32x" let consts ← findUuid measures "slug" "constants" - let primaries ← (specs.find? (·.testbed == "aiur-x64-32x")).map + let names ← (specs.find? (·.testbed == "zisk-check-execute-x64-32x")).map (·.benchmarks.filterMap (findUuid benchmarks "name" ·)) - return { title := "Aiur/Zisk Input Constants", - testbeds := #[aiurTb], benchmarks := primaries, - measure := consts, window := windowFor "Aiur/Zisk Input Constants" window } + return { title := "Kernel Input Constants", + testbeds := #[ziskTb], benchmarks := names, + measure := consts, window := windowFor "Kernel Input Constants" window } match overlay with | some d => desired := desired.push d | none => do IO.eprintln "warn: input-constants plot skipped (missing testbed or measure)" - -- Zisk shards over time, one line per HEAVY-tier primary — the constants - -- whose closure is cut into a multi-shard partition. Light constants run - -- as a single shard (a flat line at 1), so they're left out; the full-set - -- `shards` plot stays in `plotSkips`. - let ziskShards : Option DesiredPlot := do - let ziskTb ← findUuid testbeds "slug" "zisk-check-execute-x64-32x" - let shardsM ← findUuid measures "slug" "shards" - let heavy := (BenchCmd.envSpecs.map (·.name)).foldl - (init := (#[] : Array String)) fun acc env => - acc ++ (BenchCmd.selectNames rows env "zisk" "execute" - (full := false) (tier := "heavy") (shardOnly := false)).map (·.name) - return { title := "Zisk Shards", testbeds := #[ziskTb], - benchmarks := heavy.filterMap (findUuid benchmarks "name" ·), - measure := shardsM, window := windowFor "Zisk Shards" window } - match ziskShards with - | some d => desired := desired.push d - | none => do - IO.eprintln - "warn: Zisk shards plot skipped (missing testbed or measure)" - -- The registry owns the dashboard: delete every plot whose title isn't -- in the desired set, so each sync converges to exactly the registry's -- plots (a renamed or de-listed plot goes away instead of lingering @@ -411,7 +402,7 @@ end Ix.Cli.BenchPlots open Ix.Cli.BenchPlots in def benchPlotsCmd : Cli.Cmd := `[Cli| plots VIA runPlotsCmd; - "Sync the bencher.dev dashboard plots to the registry: one plot per tracked (testbed, measure) plus the shared input-constants and Zisk heavy-shards plots. Needs the bencher CLI; writes need BENCHER_API_KEY (plot create/delete permission)." + "Sync the bencher.dev dashboard plots to the registry: one plot per tracked (testbed, measure) plus the shared input-constants plot. Needs the bencher CLI; writes need BENCHER_API_KEY (plot create/delete permission)." FLAGS: "dry-run"; "Print the create/replace/keep decisions without writing (no key needed)" @@ -419,5 +410,4 @@ def benchPlotsCmd : Cli.Cmd := `[Cli| branch : String; "Branch whose series the plots track (default: main)" window : Nat; "Seconds of history per plot (default: 7257600 = 12 weeks)" "x-axis" : String; "date_time | version (default: version)" - csv : String; "Vectors path (default: Benchmarks/Vectors.csv)" ] diff --git a/Ix/Cli/BenchReport.lean b/Ix/Cli/BenchReport.lean index b6f5254bd..aa1e39cd0 100644 --- a/Ix/Cli/BenchReport.lean +++ b/Ix/Cli/BenchReport.lean @@ -33,22 +33,11 @@ namespace Ix.Cli.BenchReport /-! ## Metric formatting -/ -/-- Stage qualifiers a pipeline measure carries ahead of its base name: - `recursive-` scopes a measure to the recursion stage, `pipeline-` to - the whole run. Stripped wherever a measure is interpreted by its base - name (formatting kind) or labelled under a heading that already says - the stage. -/ -def stagePrefixes : List String := ["recursive-", "pipeline-"] - -/-- `metric` with its stage qualifier removed, if it has one. -/ -def dropStagePrefix (metric : String) : String := - match stagePrefixes.find? (fun p => metric.startsWith p) with - | some p => (metric.drop p.length).toString - | none => metric +open Ix.Cli.BenchCmd (stagePrefixOf dropStagePrefix) /-- Per-metric formatting kind. Metric names are the results-JSON keys the tools emit (see the registry in Ix.Cli.BenchCmd). A stage-qualified - metric formats like its base counterpart (`recursive-peak-rss` and + metric formats like its base counterpart (`stage2-peak-rss` and `pipeline-peak-rss` like `peak-rss`, …). Unknown metrics fall through to a generic decimal rendering. -/ def metricKind (metric : String) : String := @@ -68,12 +57,13 @@ def metricKind (metric : String) : String := (renaming one would orphan its threshold/history); only the table rendering differs. `file-size` is the serialized `.ixe` env — bencher plots it as "Environment Size"; `peak-rss` reads better as plain RAM, - in every slug that embeds it (`recursive-peak-rss` → …-peak-ram); + in every slug that embeds it (`stage2-peak-rss` → …-peak-ram); `throughput` carries its unit here because the runs print bare magnitudes (matching `unitsFor`'s "constants / second" on bencher). -/ def metricLabel (metric : String) : String := if metric == "file-size" then "env-size" - else if metric == "throughput" then "throughput (const/s)" + else if dropStagePrefix metric == "throughput" then + metric.replace "throughput" "throughput (const/s)" else metric.replace "peak-rss" "peak-ram" /-- Group a digit string by thousands: `"105492"` → `"105,492"`. -/ @@ -138,7 +128,8 @@ def human (v : Option Float) (metric : String) : String := constants checked per second on EVERY backend (`ix_bench::throughput` is the one calculator; a zkVM's cycle rate stays derivable from its cycles / execute-time fields). -/ -def higherIsBetter (metric : String) : Bool := metric == "throughput" +def higherIsBetter (metric : String) : Bool := + dropStagePrefix metric == "throughput" /-! ## Row access -/ @@ -195,10 +186,11 @@ structure CompareSection where /-- The stage qualifier shared by every one of a section's measures, if they share one. A stage table's heading already says which stage it - is, so its columns read `prove-time`, not `recursive-prove-time`. -/ + is, so its columns read `prove-time`, not `stage1-prove-time`. -/ def sectionLabelDrop (metrics : Array String) : String := - if metrics.isEmpty then "" else - (stagePrefixes.find? fun p => metrics.all (·.startsWith p)).getD "" + match metrics[0]?.bind stagePrefixOf with + | some p => if metrics.all (·.startsWith p) then p else "" + | none => "" structure CompareArgs where mainRows : Json @@ -797,7 +789,7 @@ def runFetchMainCmd (p : Cli.Parsed) : IO UInt32 := do let names ← Ix.Cli.ConstsFile.gather p "consts" "names" if (p.flag? "consts").isNone && (p.flag? "names").isNone then pure none else - -- The env-keyed row (ooc whole-env, compile) isn't a Vectors.csv + -- The env-keyed row (ooc whole-env, compile) isn't a benchmark -- constant; admit it past the names filter explicitly. match (p.flag? "env").map (·.as! String) with | some env => pure (some (names.push env)) @@ -886,24 +878,20 @@ def runFetchMainCmd (p : Cli.Parsed) : IO UInt32 := do job needs verbatim: the display label, the bencher testbed/workload pair, and the rendered `--threshold-*` flags, so the workflow hardcodes none of it. -/ -def runMatrixCmd (p : Cli.Parsed) : IO UInt32 := do - let csv := (p.flag? "csv").map (·.as! String) - |>.getD "Benchmarks/Vectors.csv" - let rows := Ix.Cli.BenchCmd.parseVectorsCsv (← IO.FS.readFile csv) +def runMatrixCmd (_ : Cli.Parsed) : IO UInt32 := do let mut entries : Array Json := #[] for b in Ix.Cli.BenchCmd.backendSpecs do if b.disabled.isSome then continue for (mode, testbed) in b.testbeds do if b.unscheduled.contains mode then continue - for env in b.envNames rows do + for env in b.envNames do -- Skip a per-constant cell whose selection is empty in THIS mode: -- an env stays in `envNames` because some scheduled mode runs it, - -- but a constant excluded from one mode (e.g. Lean's only primary - -- constant is prove-excluded) leaves that (env, mode) cell empty — - -- scheduling it would waste a job and expect a row that never lands. + -- but a constant excluded from one mode leaves that (env, mode) + -- cell empty — scheduling it would waste a job and expect a row + -- that never lands. if b.inputs == .perConstant - && (Ix.Cli.BenchCmd.selectNames rows env b.name mode - (full := false) (tier := "") (shardOnly := false)).isEmpty then + && (Ix.Cli.BenchCmd.selectNames env b.name mode).isEmpty then continue let label := s!"{b.name}-{env}-{mode}" entries := entries.push <| Json.mkObj @@ -951,16 +939,14 @@ def parseError (msg : String) : IO UInt32 := do decompile), InitStd for the rest) BENCH_CONSTS=Nat.gcd,… (bench exactly these constants on the per-constant backends, overriding the - curated selection. Each name's env is - found automatically: its Vectors.csv - row first, else its defining module - (Init/Std → InitStd, Lean → Lean), - else Mathlib — or FLT for FLT.* names - — so BENCH_ENVS is never required. A - single-env BENCH_ENVS still forces - placement.) - BENCH_FULL=1 (full curated set, not just primary) - BENCH_SHARD=1 (only the multi-shard target constants) + shared selection. Each name's env is + found automatically: its + `benchConstants` entry first, else its + defining module (Init/Std → InitStd, + Lean → Lean), else Mathlib — or FLT + for FLT.* names — so BENCH_ENVS is + never required. A single-env + BENCH_ENVS still forces placement.) BENCH_PHASES=1 / RUST_LOG=… / WITHOUT_VK_VERIFICATION=… / RUSTFLAGS=… / IX_COMPILE_EAGER=… / IX_COMPILE_DEMOTE=… / IX_COMPILE_WORKERS=… / IX_DECOMPILE_KENV_CLEAR_ENTRIES=… @@ -1043,8 +1029,6 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do -- `=`, so only recognized keys are consulted there). let mut envs : Array String := #[] let mut consts : Array String := #[] - let mut shard := "0" - let mut full := "0" let mut passthrough : Array String := #[] let mut cfgEntries : Array (String × Bool) := (cfgToks.map ((·, true))).toArray @@ -1077,8 +1061,6 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do | "BENCH_CONSTS" => for tok in Ix.Cli.ConstsFile.parseCommaList val do if !consts.contains tok then consts := consts.push tok - | "BENCH_SHARD" => if val == "1" then shard := "1" - | "BENCH_FULL" => if val == "1" then full := "1" | k => if ["BENCH_PHASES", "RUST_LOG", "WITHOUT_VK_VERIFICATION", "RUSTFLAGS", "IX_COMPILE_EAGER", "IX_COMPILE_DEMOTE", @@ -1087,17 +1069,17 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do passthrough := passthrough.push s!"{k}={val}" else if strict then return ← parseError s!"unknown config key `{k}` in the \ - benchmark command (expected BENCH_ENVS / BENCH_CONSTS / \ - BENCH_FULL / BENCH_SHARD, or passthrough: BENCH_PHASES, \ + benchmark command (expected BENCH_ENVS / BENCH_CONSTS, \ + or passthrough: BENCH_PHASES, \ RUST_LOG, WITHOUT_VK_VERIFICATION, RUSTFLAGS, \ IX_COMPILE_EAGER, IX_COMPILE_DEMOTE, IX_COMPILE_WORKERS, \ IX_DECOMPILE_KENV_CLEAR_ENTRIES)" | [] => continue -- BENCH_CONSTS: bench exactly these constants on the per-constant - -- backends, overriding the curated selection (`ix bench run --consts` + -- backends, overriding the shared selection (`ix bench run --consts` -- downstream). Each name finds its own env — no BENCH_ENVS needed: - -- 1. a Vectors.csv row wins (curated attribution); + -- 1. a `benchConstants` entry wins (curated attribution); -- 2. otherwise, locate the name by defining module: import the -- `Lean` environment (toolchain oleans only — its closure IS the -- Lean bench env, and it contains InitStd's) and map the module @@ -1108,16 +1090,13 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do -- An explicit single-env BENCH_ENVS still overrides the attribution. let mut constsByEnv : Array (String × Array String) := #[] if !consts.isEmpty then - let csvPath := (p.flag? "csv").map (·.as! String) - |>.getD "Benchmarks/Vectors.csv" - let rows := Ix.Cli.BenchCmd.parseVectorsCsv - (← try IO.FS.readFile csvPath catch _ => pure "") - -- Loaded lazily, once, and only when some name has no CSV row. + -- Loaded lazily, once, and only when some name has no curated entry. let mut lookupEnv? : Option Lean.Environment := none for n in consts do - let csvOwners := - ((rows.filter (·.name == n)).map (·.env)).toList.eraseDups - let mut owners := csvOwners + let curatedOwners := + ((Ix.BenchConstants.benchConstants.filter (·.name == n)).map + (·.env)).toList.eraseDups + let mut owners := curatedOwners if owners.isEmpty then let env ← match lookupEnv? with | some e => pure e @@ -1204,8 +1183,7 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do let modes := " ".intercalate (backends.map (fun b => if b.testbeds.length > 1 then s!"{b.name}={modeFor b}" else b.name)).toList - let mut summary := s!"backends: `{modes}` · envs: `{",".intercalate allEnvs.toList}` · \ - set: `{if full == "1" then "full" else "primary"}` · shard: `{shard}`" + let mut summary := s!"backends: `{modes}` · envs: `{",".intercalate allEnvs.toList}`" if !consts.isEmpty then summary := summary ++ s!" · consts: `{",".intercalate consts.toList}`" if freshFlag then @@ -1225,7 +1203,6 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do let h ← IO.FS.Handle.mk outPath IO.FS.Mode.append h.putStr <| s!"matrix={(Json.arr entries).compress}\n" ++ s!"envs={(Json.arr (allEnvs.map Json.str)).compress}\n" - ++ s!"shard={shard}\nfull={full}\n" ++ s!"fresh={if freshFlag then 1 else 0}\n" ++ s!"config-summary={summary}\n" ++ "passthrough-env<` points the run at another checkout: the *measured* tools @@ -103,12 +93,11 @@ a PR tree and compare them — exactly what the PR workflow does. | backend | what it measures | tool | |---|---|---| -| `aiur` | Aiur STARK check, one bench-main cell per mode on its own testbed: prove — the real-workload simulation (prove-time, proof-size, verify-time, peak-rss, plus fft-cost / execute-time from its own Phase 1) — and execute, the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss). `!benchmark aiur [execute]` picks the mode. A third mode, recursive (`bench-typecheck --recursive`), additionally executes AND proves the in-circuit multi-stark verifier over each fresh proof — the whole system runs under recursion-tuned FRI parameters, so its rows land on their own testbed (`aiur-check-recursive`) and are not comparable to the prove cell's. Unscheduled (the full selection is too heavy for per-push CI — the large closures exceed the RAM ceiling and land as OOM rows — so no CI job runs it and nothing uploads to its testbed; the `aiur-recursive` cell below tracks the same measurement over a fixed two-constant subset): run it locally (`ix bench run --backend aiur --mode recursive`) or request it on demand with `!benchmark aiur recursive` — meant for a bigger manual dispatch | `bench-typecheck` | -| `aiur-recursive` | IxVM recursion on two fixed constants at the ~100-query soundness level (`Nat.add_comm`, the cheap-tier small end; `Array.extract_append`, the heavy-tier kernel-scale one): prove each constant's IxVM typecheck, run the in-circuit multi-stark verifier over the fresh proof (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 same measurement as aiur's recursive mode, but over a fixed subset instead of the `Vectors.csv` fan-out: always exactly one cell regardless of `BENCH_ENVS`, with the constants resolved in whichever env's `.ixe` the cell carries | `bench-typecheck --recursive` | -| `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (1 when unsharded) | `zisk-host` | +| `aiur` | the Aiur 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 (the KZG stages fold in as they land), closed by the pipeline ledger (total-time, pipeline-throughput, pipeline-peak-rss). The whole system runs under the recursion-tuned FRI parameters. A second mode, execute, is the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss) — unscheduled, local/on-demand only (`!benchmark aiur execute`) | `bench-typecheck --recursive` | +| `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (the runtime-planned partition size; 1 when the closure fits) | `zisk-host` | | `sp1` | SP1 VM execute (currently disabled in the registry) | `sp1-host` | -| `ooc` | out-of-circuit Rust kernel: whole-env row + one full-closure row per primary (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-rs --json` | -| `lean4lean` | the reference Lean4-in-Lean4 kernel ([digama0/lean4lean](https://github.com/digama0/lean4lean), required by the lakefile at a pinned rev) — the external yardstick for the Ix kernels on the same libraries. Olean-driven (no `.ixe`): the whole-library row replays every module in the env's import closure through lean4lean, module-parallel (check-time, constants, throughput, peak-rss; tune parallelism with `LEAN_NUM_THREADS`), plus one full-closure row per primary (the name's transitive closure into a fresh kernel env), mirroring ooc's row shape. Registry-disabled for CI (no bencher testbed yet); `ix bench run --backend lean4lean` works locally regardless | `bench-lean4lean` | +| `ooc` | out-of-circuit Rust kernel: whole-env row + one full-closure row per constant (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-rs --json` | +| `lean4lean` | the reference Lean4-in-Lean4 kernel ([digama0/lean4lean](https://github.com/digama0/lean4lean), required by the lakefile at a pinned rev) — the external yardstick for the Ix kernels on the same libraries. Olean-driven (no `.ixe`): the whole-library row replays every module in the env's import closure through lean4lean, module-parallel (check-time, constants, throughput, peak-rss; tune parallelism with `LEAN_NUM_THREADS`), plus one full-closure row per constant (the name's transitive closure into a fresh kernel env), mirroring ooc's row shape. Registry-disabled for CI (no bencher testbed yet); `ix bench run --backend lean4lean` works locally regardless | `bench-lean4lean` | | `compile` | `ix compile .lean → .ixe`: compile-time, file-size, constants, throughput | `ix compile --json` | | `decompile` | inverse of compile — `ix decompile .ixe → Lean consts`: decompile-time, throughput, peak-rss, constants, file-size (input `.ixe`). Consumes the compile cell's `.ixe` rather than producing one; a malformed decompile reddens the cell. Deep roundtrip fidelity is gated by the canonical checks (`ix validate` / roundtrip tests), which need the original Lean env the `.ixe` can't supply | `ix decompile --json` | @@ -149,19 +138,23 @@ approach the ceiling, and a kill there means missing rows and a red cell. There are **no per-constant timeouts**; the job-level `timeout-minutes` is the only clock. -Heavy-tier zisk constants (whose single-leaf closure would blow the runner's -RAM) run as their closure-shard partition instead: `ix shard extract` → -`ix profile` → `ix shard` cut a manifest, and one `--shard-plan` host run -executes the shards sequentially, emitting the constant's row with per-shard +Every zisk constant runs as a closure-shard partition sized at bench +runtime: `ix shard extract` → `ix profile` → `ix shard` cut a manifest +whose shard count comes from the planner's RAM budget (a closure that +fits gets a one-shard plan), and one `--shard-plan` host run executes the +shards sequentially, emitting the constant's row with per-shard breakdowns. bench-main's compile job pre-cuts these artifacts -(`ix bench shard`) and ships them via cache. +(`ix bench shard`) and ships them via cache; a zisk run cuts lazily when +they're absent, and falls back to the whole closure if the cut fails. ## Registry and constant set -- **`Benchmarks/Vectors.csv`** — the curated constants: one row per - `(name, env, tier[, shard_target[, primary]])`. `tier: heavy` marks - constants whose full prove is expected to OOM (they still run; the row - records it). `primary: 1` is the default `!benchmark` subset. +- **`Ix/BenchConstants.lean`** — the shared constant set: one + `(name, env)` entry per benchmark constant, compiled into `ix`. + Every per-constant backend runs this same set (a constant whose prove + exceeds the host's RAM still runs; the row records the OOM), minus the + hard feasibility exclusions in `benchExclusions` + (`Ix/Cli/BenchCmd.lean`). - **The registry** (`envSpecs`/`backendSpecs` in `Ix/Cli/BenchCmd.lean`) — everything else: env modules, backends (disabled reason, default mode, bencher testbeds, compare columns). Typed Lean data with one owner: the @@ -179,13 +172,14 @@ breakdowns. bench-main's compile job pre-cuts these artifacts ## `!benchmark` grammar ``` -!benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) - [execute | recursive] [fresh] [KEY=VALUE …] +!benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] | all) + [execute] [fresh] [KEY=VALUE …] BENCH_ENVS=InitStd,Mathlib # default InitStd (case-insensitive); a # compile-only request may name any registry # env (Lean, FLT compile fine, just unbenched) -BENCH_FULL=1 # full curated set, not just primary -BENCH_SHARD=1 # only the multi-shard target constants +BENCH_CONSTS=Nat.gcd,… # bench exactly these constants on the + # per-constant backends (each name's env is + # found automatically) BENCH_PHASES=1 # add the per-constant phase drill-downs # to the comment (off by default) RUST_LOG=info # passthrough env (allowlist: BENCH_PHASES, @@ -202,7 +196,7 @@ The `KEY=VALUE` config works both as lines below the command (the comment form above) and inline on the command line, whitespace-separated — the single-line form for `bench-pr.yml`'s manual workflow_dispatch, whose input box can't hold newlines: -`!benchmark aiur execute BENCH_ENVS=InitStd,Mathlib BENCH_FULL=1`. +`!benchmark aiur execute BENCH_ENVS=InitStd,Mathlib`. The `IX_COMPILE_*` settings change compile-time RAM and speed but produce a bit-identical `.ixe`, so normal `.ixe` and compile-row caches are keyed only by @@ -212,9 +206,9 @@ benchmarked commit. Parsed by `ix bench ci parse` in the PR build job, right after the `ix` binary exists — the registry lives in Lean, so nothing pre-build reads it (and no Python remains). Mode defaults per backend from the registry; the -bare `execute` token flips `aiur` to Phase-1 only, and `recursive` to its -recursive mode (unscheduled testbed, so no bencher baseline; OOMs the -standard CI host — meant for a bigger manual dispatch). The bare `fresh` +bare `execute` token flips `aiur` from the full proof pipeline to the fast +Phase-1-only mode (unscheduled testbed, so no bencher baseline — its base +side comes from a base-SHA run). The bare `fresh` token makes every cell bypass its bencher baseline and keeps persistent cached benchmark binaries, compiled `.ixe` files, and compile rows out of measured jobs. A cached head `ix` may bootstrap the canonical command parser, but the @@ -230,10 +224,9 @@ untouched. SHA) → `plan` (`ix bench ci matrix` → job matrices) + `compile` (per env: `ix bench run --backend compile`, cache the `.ixe` and pre-cut zisk shards separately) → -`aiur` (execute + prove cells) / `zkvm-execute` / `ooc-check` (each: restore caches, one -`ix bench run … --ixe`, `ix bench bmf`, upload via -`.github/actions/bencher-track`) / `aiur-recursive` (same shape — it -restores the cached `.ixe` its fixed constants resolve in). A kernel +one `benchmark` job per remaining cell — aiur / zisk / ooc / decompile — +(each: restore caches, one `ix bench run … --ixe`, `ix bench bmf`, +upload via `.github/actions/bencher-track`). A kernel rejection exits 3 and reddens the run step while the clean rows still upload. @@ -242,7 +235,7 @@ to — main-branch trend lines, one per benchmark row the cell uploads, plus the cross-kernel input-constants overlay. Registry-derived like the job matrices (titles, ordering, and skips live in `Ix/Cli/BenchPlots.lean`), so rerun the sync -after changing the registry or the primary constants — either locally +after changing the registry or the constant set — either locally (needs the bencher CLI and a user API key in `BENCHER_API_KEY`; `--dry-run` previews) or via the `bencher-plots.yml` workflow_dispatch (run it after bench-main has built the merged registry). Idempotent: @@ -280,10 +273,8 @@ only an explicit `fresh` request bypasses the measured-product caches. execute-only. - **sp1** — disabled in the registry (execute too slow per push); re-enable it there and it returns to the matrices and the parser. -- **aiur recursive over the full selection in CI** — the `aiur-recursive` - cell tracks IxVM recursion on its two fixed constants, but the full - `Vectors.csv` fan-out of `bench-typecheck --recursive` is too heavy for - per-push CI (the large closures exceed the RAM ceiling and land as OOM - rows), so the `aiur-check-recursive` testbed is registered but - unscheduled: no bench-main job and no `!benchmark` token. Run it - locally with `ix bench run --backend aiur --mode recursive`. +- **aiur prove numbers for the biggest closures** — every constant in the + shared set runs the full pipeline, but the largest ones exceed the CI + host's RAM ceiling and land as honest `oom` rows, which never upload + (`ix bench bmf` drops non-`ok` rows) — their trend lines stay empty + until the prover's RAM drops under the ceiling. From 52cc8c6149c6b7a501521a0629785d0b5ac17019 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 20 Aug 2026 18:14:59 -0400 Subject: [PATCH 2/4] ci: balance Lake ignored merge tests --- .github/workflows/merge-tests.yml | 26 +++++++++++--- README.md | 7 ++-- Tests/Main.lean | 58 ++++--------------------------- 3 files changed, 30 insertions(+), 61 deletions(-) diff --git a/.github/workflows/merge-tests.yml b/.github/workflows/merge-tests.yml index 66803f3a6..2e616d037 100644 --- a/.github/workflows/merge-tests.yml +++ b/.github/workflows/merge-tests.yml @@ -22,15 +22,27 @@ 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 @@ -38,6 +50,10 @@ jobs: - 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 diff --git a/README.md b/README.md index 9677b8b3c..7dffe9ceb 100644 --- a/README.md +++ b/README.md @@ -199,11 +199,10 @@ cells locally, and `!benchmark` runs them on a PR — see - Most tests require at least 32 GB RAM - The `compile` and `decompile` tests require 128 GB RAM - `ixvm` generates ZK proofs and uses significant CPU -- `lake test -- --ignored ` runs one or more expensive suites, runners, or groups by name -- Ignored groups: `compile-pipeline`, `kernel`, and `typecheckers` -- `--exclude=` excludes ignored suites, runners, or groups from a full ignored-test run +- `lake test -- --ignored ` runs one or more expensive suites or runners by name +- `--exclude=` excludes ignored suites or runners from a full ignored-test run - `lake test -- --include-ignored` runs both primary and expensive test suites -- `lake test -- --include-ignored ` runs all primary suites plus selected expensive suites, runners, or groups +- `lake test -- --include-ignored ` runs all primary suites plus selected expensive suites or runners - `lake test -- cli` runs CLI integration tests - `lake test -- rust-compile` runs the Rust cross-compilation diagnostic diff --git a/Tests/Main.lean b/Tests/Main.lean index d54b77f69..3a92f4d42 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -131,50 +131,6 @@ def ignoredSuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ ("tc-ingress-meta", Tests.Tc.IngressMeta.suite), ] -/-- Related ignored suites and runners that can be selected or excluded together. -/ -def ignoredGroups : Std.HashMap String (List String) := .ofList [ - ("compile-pipeline", [ - "rust-canon-roundtrip", - "serial-canon-roundtrip", - "parallel-canon-roundtrip", - "graph-cross", - "condense-cross", - "compile", - "decompile", - "rust-serialize", - "ixon-corpus", - "rust-decompile", - "validate-aux", - "aux-gen-diff", - "decompile-diff", - ]), - ("kernel", [ - "kernel-ixon-roundtrip", - "kernel-tutorial", - "kernel-check-env", - "kernel-check-const", - "rust-kernel-build-primitives", - "rust-kernel-build-prim-origs", - "ixvm", - ]), - ("typecheckers", [ - "tc-anon-diff", - "tc-init", - "tc-tutorial", - "tc-roundtrip", - "tc-ingress-meta", - "tc-pins", - "tc-accel-diff", - "lean4lean", - ]), -] - -private def expandIgnoredNames (names : List String) : List String := - (names.flatMap fun name => - match ignoredGroups[name]? with - | some members => members - | none => [name]).eraseDups - /-- Primary test runners — quick suites run by default alongside `primarySuites`, but kept as deferred `IO` actions (not `TestSeq` values) so their setup — Aiur system builds, STARK proofs — does not @@ -343,15 +299,13 @@ def main (args : List String) : IO UInt32 := do let runIgnored := args.contains "--ignored" let includeIgnored := args.contains "--include-ignored" - -- `--exclude=a,b,c` drops named ignored suites, runners, or groups. - let rawExcludeSet : List String := + -- `--exclude=a,b,c` drops named ignored suites and runners from an unfiltered sweep. + let excludeSet : List String := match args.find? (·.startsWith "--exclude=") with | some a => (a.drop ("--exclude=".length)).toString.splitOn "," |>.filter fun s => !s.isEmpty | none => [] - let excludeSet := expandIgnoredNames rawExcludeSet let filterArgs := args.filter fun a => a != "--ignored" && a != "--include-ignored" && !a.startsWith "--exclude=" - let ignoredFilterArgs := expandIgnoredNames filterArgs -- Run primary tests unless --ignored (without --include-ignored) is specified if !runIgnored || includeIgnored then @@ -385,16 +339,16 @@ def main (args : List String) : IO UInt32 := do -- that matches nothing is an ERROR, not a silent no-op: otherwise a typo -- runs (or excludes) nothing and still reports success having executed -- nothing. - for arg in ignoredFilterArgs ++ excludeSet do + for arg in filterArgs ++ excludeSet do if !(allRunners.any fun (key, _) => key == arg) && !ignoredSuites.contains arg then IO.eprintln s!"error: no ignored suite or runner named '{arg}'" return 1 let suites := excludeSet.foldl (fun m k => m.erase k) ignoredSuites let runners := allRunners.filter fun (key, _) => !excludeSet.contains key - let mut result ← LSpec.lspecIO suites ignoredFilterArgs - let filtered := if ignoredFilterArgs.isEmpty then runners - else ignoredFilterArgs.filterMap fun arg => runners.find? fun (key, _) => key == arg + let mut result ← LSpec.lspecIO suites filterArgs + let filtered := if filterArgs.isEmpty then runners + else filterArgs.filterMap fun arg => runners.find? fun (key, _) => key == arg for (_, action) in filtered do let r ← action if r != 0 then result := r From e3f742ccfd85ec32bf94abd1f9987549b091ccb0 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 20 Aug 2026 19:02:04 -0400 Subject: [PATCH 3/4] Fix Zisk bench error --- zisk/host/src/main.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/zisk/host/src/main.rs b/zisk/host/src/main.rs index b54b3792d..5039f7aae 100644 --- a/zisk/host/src/main.rs +++ b/zisk/host/src/main.rs @@ -1211,9 +1211,12 @@ async fn run_shard_plan( // The trusted vk of the shard guest, derived from the embedded ELF (its // ROM setup ran in `run` before this point). Anchors the allowed set the // agg guest pins children against and gates which stored proofs may fold. - // Dump mode without a store returns before any vk use and skips ROM setup - // entirely, so the vk is not derivable there — leave it empty. - let shard_vk = if args.dump_input.is_none() || args.store_dir.is_some() { + // Dump and execute modes without a store return before any vk use, and + // may run without a proving key — where ROM setup cannot happen and the + // vk is not derivable — so they must not derive one; leave it empty. + let shard_vk = if (args.dump_input.is_none() && !args.execute) + || args.store_dir.is_some() + { guest_vk_bytes(&SHARD_PROGRAM)? } else { Vec::new() From b6a536d50a768a5972c1df7c702d891c7c7745e0 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 20 Aug 2026 21:39:33 -0400 Subject: [PATCH 4/4] bench: name the aiur stage measures ixvm-/fri-verifier-; retire the toy recursion harness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The pipeline's stage measures were prefixed ordinally (stage1-/stage2-), which says nothing about what a stage proves and would leave stage3-/ stage4- equally opaque when the KZG stages land. They rename to the stage's subject: ixvm-* for the IxVM-typecheck prove, fri-verifier-* for the in-circuit FRI verifier over that proof (seven measures each: execute-time, prove-time, throughput, peak-rss, proof-size, verify-time, fft-cost). The ledger keeps total-time / pipeline-throughput / pipeline-peak-rss. The `!benchmark` stage tables retitle to "IxVM on FRI" / "FRI verifier on FRI"; their columns still strip the prefix under the heading. Plot titles follow ("Aiur IxVM Time", "Aiur FRI Verifier Time", …). The prefix machinery simplifies from stage- parsing to a named list (stagePrefixes = ixvm-/fri-verifier-/pipeline-) that the KZG stages extend; formatting kind, units, improvement direction, and stage-table labels all still derive from the stripped base name, and bench-measures pins the parsing. Nothing with the short-lived stage- slugs ever uploaded, so bencher history is untouched. bench-recursive-verifier is retired: since #567 the aiur benchmark IS the recursion measurement — bench-typecheck --recursive drives the same Ix.MultiStark verifier over real constants' proofs — and CI only ever built and shipped the toy-factorial harness without measuring through it (its correctness coverage lives in Tests/MultiStark.lean's aiur-prove / aiur-hashes runners). The exe, its lakefile target, and the build / package / base-restore plumbing in both bench workflows go with it. bench-recursion-debug stays: the prove-once/replay debugging harness for the recursive verifier (from #527), used by hand only. In its remaining inner-vs-outer split, the local harness's outer metrics take fri-verifier-* and the inner statement keeps plain names. Docstring corrections along the way: the aiur registry comment counted five stage columns (it is seven since throughput landed) and omitted pipeline-throughput from the ledger; bench-recursion-debug claimed its --queries default matches the pipeline (the pipeline runs 50 queries with no query PoW; the tool defaults to 100 with 20 PoW bits — now documented as such); plot-skip and docs prose name the actual slugs. --- .github/workflows/bench-main.yml | 14 +- .github/workflows/bench-pr.yml | 20 +-- Benchmarks/RecursionDebug.lean | 8 +- Benchmarks/RecursiveVerifier.lean | 213 ------------------------------ Benchmarks/Typecheck.lean | 69 +++++----- Ix/Cli/BenchCmd.lean | 118 +++++++++-------- Ix/Cli/BenchPlots.lean | 34 ++--- Ix/Cli/BenchReport.lean | 6 +- Tests/Ix/BenchMeasures.lean | 28 ++-- docs/benchmarking.md | 7 +- lakefile.lean | 4 - 11 files changed, 153 insertions(+), 368 deletions(-) delete mode 100644 Benchmarks/RecursiveVerifier.lean diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 5cd43480f..b2d2fa400 100644 --- a/.github/workflows/bench-main.yml +++ b/.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 diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index ec1fa45f2..8db31799e 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -140,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. @@ -226,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. @@ -247,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: @@ -724,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" @@ -747,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 diff --git a/Benchmarks/RecursionDebug.lean b/Benchmarks/RecursionDebug.lean index 8bc203020..1b5bff892 100644 --- a/Benchmarks/RecursionDebug.lean +++ b/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) diff --git a/Benchmarks/RecursiveVerifier.lean b/Benchmarks/RecursiveVerifier.lean deleted file mode 100644 index b71c14aa5..000000000 --- a/Benchmarks/RecursiveVerifier.lean +++ /dev/null @@ -1,213 +0,0 @@ -import Ix.Aiur.Meta -import Ix.Aiur.Protocol -import Ix.Aiur.Compiler -import Ix.Aiur.Statistics -import Ix.MultiStark -import Ix.TracingTexray -import Ix.Benchmark.Results - -open Aiur - -/-! -# Recursive-verifier cost benchmark - -Proves a tiny fixed statement with the multi-stark backend, runs the in-circuit -recursive verifier (`verify_multi_stark_proof`) over that proof, then proves -and verifies THAT execution — the end-to-end recursion step. Mirrors the setup -of `Tests/MultiStark.lean::endToEndSuite`, but measures cost instead of -asserting accept/reject. - -``` -lake exe bench-recursive-verifier # factorial(5), q=100 (soundness level — heavy) -lake exe bench-recursive-verifier --queries 3 # cheap local run (toy soundness) -lake exe bench-recursive-verifier --execute-only # skip the outer prove (FFT/exec only) - - --trivial square(5) instead of factorial(5) — the per-statement floor - --queries N FRI query count (default 100 = soundness level; pass a - small value for a cheap local run) - --log-blowup N log2 blowup (default 2) - --pow N query PoW bits (default 0) - --json 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 backend - instead drives `bench-typecheck --recursive` over the - shared benchmark constants (Ix.BenchConstants).) - --json-name row key (default: the inner entrypoint name) - --texray tracing-texray timeline + RAM; with --json, spans also land - at `.spans` for the CI drill-down -``` - -Row metrics: `stage1-prove-time`/`stage1-proof-size`/`stage1-verify-time` (the INNER statement), -`stage1-peak-rss` (inner-prove window), `stage2-execute-time`/`stage2-fft-cost` (the -verifier's execution and its in-circuit cost — the recursion-cost proxy), and -`stage2-prove-time`/`stage2-peak-rss`/`stage2-proof-size`/ -`stage2-verify-time` (the outer prove — the headline recursion metrics). - -Determinism note: the multi-stark prover is **non-deterministic under `parallel`** -(the same statement yields byte-different valid proofs run-to-run), so the -verifier authenticates slightly different Merkle paths and its FFT drifts ~±15%. -Aiur *execution* FFT is deterministic; pin the inner proof with -`RAYON_NUM_THREADS=1` for exactly reproducible numbers. --/ - -def factorialProgram : Source.Toplevel := ⟦ - pub fn factorial(n: G) -> G { - match n { - 0 => 1, - _ => n * factorial(n - 1), - } - } -⟧ - -/-- The most trivial provable statement (`--trivial`): one non-recursive -function, no memory — the floor of the verifier's per-statement cost. -/ -def squareProgram : Source.Toplevel := ⟦ - pub fn square(n: G) -> G { - n * n - } -⟧ - -/-- `--queries N`-style overrides for parameter sweeps (e.g. pairing a run -against a config another commit could complete); defaults are the standard -recursion-tuned set. -/ -def argNat (args : List String) (flag : String) (dflt : Nat) : Nat := - match args.dropWhile (· != flag) with - | _ :: v :: _ => v.toNat?.getD dflt - | _ => dflt - -def argStr (args : List String) (flag : String) : Option String := - match args.dropWhile (· != flag) with - | _ :: v :: _ => some v - | _ => none - -def recCommitParams (args : List String) : Aiur.CommitmentParameters := - { logBlowup := argNat args "--log-blowup" 2, capHeight := 0 } -def innerFri (args : List String) : Aiur.FriParameters := - { logFinalPolyLen := argNat args "--final-poly" 0, maxLogArity := 1, - numQueries := argNat args "--queries" 100, - commitProofOfWorkBits := 0, queryProofOfWorkBits := argNat args "--pow" 0 } - -def secs (t0 t1 : Nat) : Float := (Float.ofNat (t1 - t0)) / 1e9 - -open Ix.Benchmark.Results in -def main (args : List String) : IO UInt32 := do - let doProve := !args.contains "--execute-only" - let recCommitParams := recCommitParams args - let innerFri := innerFri args - let jsonOut := argStr args "--json" - IO.println s!"params: logBlowup={recCommitParams.logBlowup} \ - numQueries={innerFri.numQueries} finalPoly={innerFri.logFinalPolyLen} \ - pow={innerFri.queryProofOfWorkBits}" - -- Inner proof: factorial(5) (or `square(5)` under --trivial) under the - -- multi-stark backend. - let (program, entry) := - if args.contains "--trivial" then (squareProgram, `square) - else (factorialProgram, `factorial) - let rowName := (argStr args "--json-name").getD entry.toString - -- Same texray/sampler arrangement as bench-typecheck: the RSS sampler - -- always runs (peak-rss windows), the timeline only under --texray, and - -- with --json too the spans stream to `.spans`. - TracingTexray.startSampler - if args.contains "--texray" then - TracingTexray.init {} - if let some path := jsonOut then TracingTexray.jsonSink s!"{path}.spans" - let writeRow' := fun (fields : List (String × Lean.Json)) => - match jsonOut with - | some path => writeRow path rowName "ok" fields - | none => pure () - let facCompiled ← match program.compile with - | .ok c => pure c - | .error e => IO.eprintln s!"inner compile failed: {e}"; return 1 - let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams innerFri - let facIdx := facCompiled.getFuncIdx entry |>.get! - IO.println s!"proving inner {entry}(5)…" - TracingTexray.resetPeakTreeRss - let it0 ← IO.monoNanosNow - let (claim, proof, _) := facSystem.prove facIdx #[Aiur.G.ofNat 5] default - let proofBytes := proof.toBytes - let it1 ← IO.monoNanosNow - let innerOk := facSystem.verify claim proof matches .ok _ - let it2 ← IO.monoNanosNow - let innerPeak ← TracingTexray.peakTreeRssBytes - IO.println s!"inner PROVE: {secs it0 it1} s, \ - proof {proofBytes.size} bytes; inner VERIFY: \ - {secs it1 it2} s ({if innerOk then "ok" else "FAILED"})" - if !innerOk then - IO.eprintln "inner proof failed to verify" - return 1 - -- Proof (advice, channel 0), vk (channel 1), claims (channel 2), plus the - -- Blake3-bound vk/claims digests as public input (the FRI params ride in - -- the digest-bound vk). The advice buffer is built natively in Rust from - -- the raw byte blobs (`executeMultiStark` / `proveMultiStark`). - let claimBytes := MultiStark.serializeClaims #[claim] - let vkBytes := facSystem.vkBytes - let pubInput := MultiStark.verifierPubInput vkBytes claimBytes - -- Compile the verifier toplevel and run it over the proof. - let vTop ← match MultiStark.multiStark with - | .ok t => pure t - | .error e => IO.eprintln s!"verifier merge failed: {e}"; return 1 - let vCompiled ← match vTop.compile with - | .ok c => pure c - | .error e => IO.eprintln s!"verifier compile failed: {e}"; return 1 - let vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof |>.get! - IO.println "executing verify_multi_stark_proof…" - -- `--use-bytecode`: route through the generic Aiur interpreter instead of - -- the codegen'd verifier (same escape hatch as `ix check --use-bytecode`; - -- useful for iterating on `Ix/MultiStark/*.lean` without regenerating - -- `crates/ixvm-codegen/src/aiur_multi_stark.rs`, and for measuring the - -- interpreter ↔ codegen gap). - let useBytecode := args.contains "--use-bytecode" - let e0 ← IO.monoNanosNow - match vCompiled.bytecode.executeMultiStark vIdx pubInput proofBytes vkBytes - claimBytes useBytecode with - | .error e => IO.eprintln s!"verifier execution REJECTED: {e}"; return 1 - | .ok (_, qc) => - let e1 ← IO.monoNanosNow - -- One-shot shapes: `vSystem` (below) exists only when `--prove` is set, - -- and `--log-blowup` is configurable here — thread it into the model. - let vShapes := Aiur.circuitShapes vCompiled.bytecode recCommitParams innerFri - let stats := Aiur.computeStats vCompiled qc vShapes - (logBlowup := recCommitParams.logBlowup) - IO.println s!"verifier accepted, execute {secs e0 e1} s" - IO.println s!"\n=== recursive verifier in-circuit cost ===" - IO.println s!"totalFftCost = {stats.totalFftCost}" - IO.println "\n=== per-circuit breakdown (top FFT contributors) ===" - Aiur.printStats stats - -- The execute-side row lands before the outer prove, so an OOM kill - -- there still leaves these metrics on disk (the orchestrator merges - -- `status: oom` in over them). - let baseFields : List (String × Lean.Json) := - [ ("stage1-prove-time", jsonRound 6 (secs it0 it1)) - , ("stage1-proof-size", Lean.toJson proofBytes.size) - , ("stage1-verify-time", jsonRound 6 (secs it1 it2)) - , ("stage1-peak-rss", Lean.toJson innerPeak) - , ("stage2-execute-time", jsonRound 6 (secs e0 e1)) - , ("stage2-fft-cost", jsonRound 0 stats.totalFftCost) ] - writeRow' baseFields - if !doProve then - return 0 - -- PROVE the verifier execution (multi-stark): the recursion step itself. - IO.println "\n=== PROVING the verifier (multi-stark) ===" - let vSystem := AiurSystem.build vCompiled.bytecode recCommitParams innerFri - TracingTexray.resetPeakTreeRss - let t0 ← IO.monoNanosNow - let (vclaim, vproof) := vSystem.proveMultiStark vIdx pubInput proofBytes - vkBytes claimBytes - let nbytes := vproof.toBytes.size -- force the (lazy, pure) prove to run - let t1 ← IO.monoNanosNow - let outerPeak ← TracingTexray.peakTreeRssBytes - let outerOk := vSystem.verify vclaim vproof matches .ok _ - let t2 ← IO.monoNanosNow - IO.println s!"verifier PROVE time: {secs t0 t1} s, proof {nbytes} bytes" - IO.println s!"verifier proof VERIFY time: \ - {secs t1 t2} s ({if outerOk then "ok" else "FAILED"})" - if !outerOk then - IO.eprintln "outer proof failed to verify" - return 1 - writeRow' <| baseFields ++ - [ ("stage2-prove-time", jsonRound 6 (secs t0 t1)) - , ("stage2-peak-rss", Lean.toJson outerPeak) - , ("stage2-proof-size", Lean.toJson nbytes) - , ("stage2-verify-time", jsonRound 6 (secs t1 t2)) ] - return 0 diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index dd8331a73..4bdd9e125 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -51,10 +51,10 @@ lake exe bench-typecheck --ixe --consts [--consts-file

] [ proving — the fast `execute`-mode signal. --recursive after each constant's prove, run the in-circuit multi-stark verifier (`verify_multi_stark_proof`) over the fresh proof: - execute it (`stage2-execute-time`, `stage2-fft-cost` — the + execute it (`fri-verifier-execute-time`, `fri-verifier-fft-cost` — the recursion-cost proxy), then prove that execution end-to-end - (`stage2-prove-time`, `stage2-peak-rss`, - `stage2-proof-size`, `stage2-verify-time`), and close the + (`fri-verifier-prove-time`, `fri-verifier-peak-rss`, + `fri-verifier-proof-size`, `fri-verifier-verify-time`), and close the row with the pipeline ledger — `total-time` (each stage's prove, summed; a prove already contains its own witness execution, so the standalone execute times are NOT added, @@ -101,11 +101,11 @@ limit; bound a run with an external `timeout` if needed. The JSON is a flat shape. An `--execute-only` row carries the plain Phase-1 fields (`{ "": { "constants": …, "fft-cost": …, "execute-time": …, "throughput": …, "peak-rss": … } }`); a `--recursive` -pipeline row stage-qualifies every stage measure (`"stage1-execute-time"`, -`"stage1-fft-cost"`, `"stage1-prove-time"`, `"stage1-throughput"`, -`"stage1-peak-rss"`, `"stage1-proof-size"`, `"stage1-verify-time"`, the -same seven as `"stage2-…"`, and `stage3-`/`stage4-` when the KZG stages -land), plus the pipeline ledger `"total-time"`, `"pipeline-throughput"`, +pipeline row stage-qualifies every stage measure (`"ixvm-execute-time"`, +`"ixvm-fft-cost"`, `"ixvm-prove-time"`, `"ixvm-throughput"`, +`"ixvm-peak-rss"`, `"ixvm-proof-size"`, `"ixvm-verify-time"`, the +same seven as `"fri-verifier-…"`, and further stage prefixes when the +KZG stages land), plus the pipeline ledger `"total-time"`, `"pipeline-throughput"`, `"pipeline-peak-rss"` once the pipeline completes. Each stage's peak-rss and throughput are scoped to that stage's own prove window. Any bencher-specific reshaping is the caller's job (see @@ -127,8 +127,7 @@ def friParameters : Aiur.FriParameters := { queryProofOfWorkBits := 0 } -/-- Recursion-tuned commitment parameters for `--recursive`, matching - `bench-recursive-verifier`'s defaults. -/ +/-- Recursion-tuned commitment parameters for `--recursive`. -/ def recursiveCommitmentParameters : Aiur.CommitmentParameters := { logBlowup := 2 capHeight := 0 @@ -223,7 +222,7 @@ def jsonRound (d : Nat) (f : Float) : Json := Measure names are MODE-SCOPED: an execute-only run's row carries the plain Phase-1 fields (`fft-cost`, `execute-time`, `throughput`, `peak-rss`); a pipeline run stage-qualifies every stage measure - (`stage1-…`, `stage2-…`), each stage's peak and constants/sec scoped + (`ixvm-…`, `fri-verifier-…`), each stage's peak and constants/sec scoped to its own prove window. The two modes store on separate bencher testbeds (aiur-execute-* / aiur-*). -/ def Result.toJsonEntry (executeOnly : Bool) (r : Result) : String × Json := @@ -245,52 +244,52 @@ def Result.toJsonEntry (executeOnly : Bool) (r : Result) : String × Json := (r.name, Json.mkObj fields) else let fields := base ++ - [ ("stage1-fft-cost", jsonRound 0 r.fftCost) - , ("stage1-execute-time", jsonRound 6 r.executeSec) ] - -- stage1-prove-time, the proving throughput, and the prove-phase + [ ("ixvm-fft-cost", jsonRound 0 r.fftCost) + , ("ixvm-execute-time", jsonRound 6 r.executeSec) ] + -- ixvm-prove-time, the proving throughput, and the prove-phase -- peak are present only once proven. let fields := match r.proveSec with - | some p => fields ++ [ ("stage1-prove-time", jsonRound 6 p) - , ("stage1-throughput", + | some p => fields ++ [ ("ixvm-prove-time", jsonRound 6 p) + , ("ixvm-throughput", jsonRound 2 (r.constants.toFloat / p)) ] | none => fields let fields := match r.peakRss with - | some n => fields ++ [ ("stage1-peak-rss", Lean.toJson n) ] + | some n => fields ++ [ ("ixvm-peak-rss", Lean.toJson n) ] | none => fields let fields := match r.proofSize with - | some n => fields ++ [ ("stage1-proof-size", Lean.toJson n) ] + | some n => fields ++ [ ("ixvm-proof-size", Lean.toJson n) ] | none => fields let fields := match r.verifySec with - | some v => fields ++ [ ("stage1-verify-time", jsonRound 6 v) ] + | some v => fields ++ [ ("ixvm-verify-time", jsonRound 6 v) ] | none => fields -- The stage-2 metrics, in measurement order; the execute-side pair -- lands before the outer prove runs, so an OOM'd outer prove still -- leaves them on disk. let fields := match r.recursiveExecuteSec, r.recursiveFftCost with - | some s, some c => fields ++ [ ("stage2-execute-time", jsonRound 6 s) - , ("stage2-fft-cost", jsonRound 0 c) ] + | some s, some c => fields ++ [ ("fri-verifier-execute-time", jsonRound 6 s) + , ("fri-verifier-fft-cost", jsonRound 0 c) ] | _, _ => fields let fields := match r.recursiveProveSec with - | some s => fields ++ [ ("stage2-prove-time", jsonRound 6 s) - , ("stage2-throughput", + | some s => fields ++ [ ("fri-verifier-prove-time", jsonRound 6 s) + , ("fri-verifier-throughput", jsonRound 2 (r.constants.toFloat / s)) ] | none => fields let fields := match r.recursivePeakRss with - | some n => fields ++ [ ("stage2-peak-rss", Lean.toJson n) ] + | some n => fields ++ [ ("fri-verifier-peak-rss", Lean.toJson n) ] | none => fields let fields := match r.recursiveProofSize with - | some n => fields ++ [ ("stage2-proof-size", Lean.toJson n) ] + | some n => fields ++ [ ("fri-verifier-proof-size", Lean.toJson n) ] | none => fields let fields := match r.recursiveVerifySec with - | some v => fields ++ [ ("stage2-verify-time", jsonRound 6 v) ] + | some v => fields ++ [ ("fri-verifier-verify-time", jsonRound 6 v) ] | none => fields -- The pipeline ledger, once the whole pipeline has run. -- `total-time` is each stage's prove, summed. A stage's prove is -- the WHOLE cost of producing that stage's proof: `prove_ixvm` runs -- the executor itself (the `aiur/execute_ixvm` span) before - -- generating the witness, so the `stage1-execute-time` beside it is + -- generating the witness, so the `ixvm-execute-time` beside it is -- a SECOND, standalone run — instrumentation for `constants` and - -- `stage1-fft-cost`, not a step of proving. Adding the two would + -- `ixvm-fft-cost`, not a step of proving. Adding the two would -- count the execution twice. Verification is likewise excluded: a -- consumer cost, not a production one. -- `pipeline-throughput` is `constants` over `total-time` — the @@ -585,9 +584,9 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do , proofSize := some proofBytes.size, verifySec := verifySec? }, addr) writeJson (ordered.map (·.1)) -- Phase 3 (--recursive): the in-circuit verifier over the fresh - -- proof — execute it (stage2-execute-time / stage2-fft-cost), then prove - -- that execution (stage2-prove-time / stage2-peak-rss / - -- stage2-proof-size / stage2-verify-time). A reject on the execute + -- proof — execute it (fri-verifier-execute-time / fri-verifier-fft-cost), then prove + -- that execution (fri-verifier-prove-time / fri-verifier-peak-rss / + -- fri-verifier-proof-size / fri-verifier-verify-time). A reject on the execute -- is a correctness alarm, reported loudly with the recursive fields -- left absent — never a benchmark datum. if let some (vCompiled, vIdx, vSystem) := vCtx then @@ -608,7 +607,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let rvStats := Aiur.computeStats vCompiled qc vSystem.circuitShapes (logBlowup := commitParams.logBlowup) IO.println s!" {r.name}: recursive={rvSec}s \ - stage2-fft-cost={rvStats.totalFftCost}" + fri-verifier-fft-cost={rvStats.totalFftCost}" -- The per-circuit breakdown names where the verifier's cost -- lives (deserialization vs blake3 vs FRI); texray-gated like -- the other detailed diagnostics. @@ -636,8 +635,8 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do | .error e => IO.eprintln s!" outer verify {r.name} FAILED: {e}" pure none - IO.println s!" {r.name}: stage2-prove={rvProveSec}s \ - stage2-verify={rvVerifySec}s outer proof={rvProofBytes.size} bytes" + IO.println s!" {r.name}: fri-verifier-prove={rvProveSec}s \ + fri-verifier-verify={rvVerifySec}s outer proof={rvProofBytes.size} bytes" let (row, _) := ordered[i]! ordered := ordered.set! i ({ row with recursiveProveSec := some rvProveSec @@ -664,7 +663,7 @@ def typecheckCmd : Cli.Cmd := `[Cli| "json" : String; "Write per-constant results JSON to this path. 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`." "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 stage2-* metrics; see the module docstring). Uses recursion-tuned FRI parameters. Conflicts with --execute-only." + "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." "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)." texray; "Enable the tracing-texray timeline + RAM breakdown (per-prove spans on stderr). Combined with --json, per-phase span timings are additionally written to `.spans` as JSON Lines for the CI drill-down. Off by default." diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index 015d733d1..49b74db10 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -128,20 +128,18 @@ def workloadOf (testbed : String) : String := if testbed.endsWith "-x64-32x" then (testbed.dropEnd 8).toString else testbed -/-- The stage qualifier a pipeline measure carries ahead of its base name, - if any: `stage-` scopes a measure to pipeline stage N (any number - of stages — the KZG stages join as `stage3-`/`stage4-` without - touching this), `pipeline-` to the whole run. Stripped wherever a - measure is interpreted by its base name (formatting kind, units) or - labelled under a heading that already says the stage. -/ +/-- The stage qualifiers a pipeline measure may carry ahead of its base + name — one per pipeline stage, named for what the stage proves + (`ixvm-`: the IxVM typecheck; `fri-verifier-`: the in-circuit FRI + verifier over the previous proof; the KZG stages add their own + entries as they land) — plus `pipeline-` for the whole run. Stripped + wherever a measure is interpreted by its base name (formatting kind, + units) or labelled under a heading that already says the stage. -/ +def stagePrefixes : List String := ["ixvm-", "fri-verifier-", "pipeline-"] + +/-- The stage qualifier `metric` carries, if any. -/ def stagePrefixOf (metric : String) : Option String := - if metric.startsWith "pipeline-" then some "pipeline-" else - if !metric.startsWith "stage" then none else - let digits := - (metric.drop "stage".length).toString.toList.takeWhile (·.isDigit) - if digits.isEmpty then none else - let p := s!"stage{String.ofList digits}-" - if metric.startsWith p then some p else none + stagePrefixes.find? (metric.startsWith ·) /-- `metric` with its stage qualifier removed, if it has one. -/ def dropStagePrefix (metric : String) : String := @@ -178,8 +176,8 @@ structure BackendSpec where metrics : List (String × List String) /-- (mode, [(stage title, that stage's measures)]) for a mode whose run walks a multi-stage pipeline: the compare table splits into one - table per stage. A stage's measures carry their `stage-` - qualifier (`stage1-prove-time`) — the stage tables strip it for + table per stage. A stage's measures carry their stage + qualifier (`ixvm-prove-time`) — the stage tables strip it for display (`sectionLabelDrop`), so columns still read plain. List order is render order, so the closing entry is the ledger over the whole run. -/ @@ -205,18 +203,20 @@ structure BackendSpec where def backendSpecs : List BackendSpec := [ -- aiur: the proof-pipeline benchmark (bench-typecheck --recursive) — - -- every stage of the pipeline, per constant, plus the total. Stage 1 - -- proves the constant's IxVM typecheck; stage 2 executes the - -- in-circuit multi-stark verifier over the fresh stage-1 proof and - -- proves THAT execution; the KZG stages will join as stages 3/4 when - -- they land, folding into the same ledger. Each stage reports the same - -- five columns — witness execute, prove, peak RAM, proof size, verify - -- — and the closing ledger table carries `total-time` (the stages' - -- proves, summed — each prove already runs its own witness execution, - -- so the standalone execute times are instrumentation and are not - -- added) and the run's RAM ceiling. The whole system runs under the - -- recursion-tuned parameters — 50 FRI queries at log-blowup 2 for the - -- stage-1 and stage-2 proofs alike, the soundness level taking + -- every stage of the pipeline, per constant, plus the total. The ixvm + -- stage proves the constant's IxVM typecheck; the fri-verifier stage + -- executes the in-circuit multi-stark verifier over that fresh proof + -- and proves THAT execution; the KZG stages will join as stages 3/4 + -- when they land, folding into the same ledger. Each stage reports the + -- same seven columns — witness execute, prove, throughput, peak RAM, + -- proof size, verify, FFT cost — and the closing ledger table carries + -- `total-time` (the stages' proves, summed — each prove already runs + -- its own witness execution, so the standalone execute times are + -- instrumentation and are not added), the end-to-end + -- `pipeline-throughput`, and the run's RAM ceiling. The whole system + -- runs under the + -- recursion-tuned parameters — 50 FRI queries at log-blowup 2 for + -- both stages' proofs alike, the soundness level taking -- precedence over fitting every constant in the host's RAM (see -- `recursiveFriParameters` in Benchmarks/Typecheck.lean). execute is -- the fast Phase-1-only signal (witness generation, no proving), @@ -226,42 +226,44 @@ def backendSpecs : List BackendSpec := [ ("execute", "aiur-execute-x64-32x")], unscheduled := ["execute"], stages := [("prove", - [("Stage 1 — IxVM on FRI", - ["stage1-execute-time", "stage1-prove-time", "stage1-throughput", - "stage1-peak-rss", "stage1-proof-size", "stage1-verify-time", - "stage1-fft-cost"]), - ("Stage 2 — FRI recursion on FRI", - ["stage2-execute-time", "stage2-prove-time", "stage2-throughput", - "stage2-peak-rss", "stage2-proof-size", "stage2-verify-time", - "stage2-fft-cost"]), + [("IxVM on FRI", + ["ixvm-execute-time", "ixvm-prove-time", "ixvm-throughput", + "ixvm-peak-rss", "ixvm-proof-size", "ixvm-verify-time", + "ixvm-fft-cost"]), + ("FRI verifier on FRI", + ["fri-verifier-execute-time", "fri-verifier-prove-time", + "fri-verifier-throughput", "fri-verifier-peak-rss", + "fri-verifier-proof-size", "fri-verifier-verify-time", + "fri-verifier-fft-cost"]), ("Pipeline total", ["total-time", "pipeline-throughput", "pipeline-peak-rss"])])], metrics := [("execute", ["execute-time", "throughput", "peak-rss", "fft-cost"])], - -- stage1-fft-cost is deterministic but only ever drops on a real Aiur - -- win → upper-only 5% instead of a hard pin. stage2-fft-cost drifts - -- ~±15% run-to-run (the parallel prover emits byte-different valid - -- proofs, so the verifier authenticates different Merkle paths) → - -- the loose 25% bound. Proof sizes are structural (fixed query count - -- and path depth) → the tight 5%. `total-time` carries NO bound: it - -- is the two prove times summed, and a sum cannot breach a - -- percentage bound unless one of its terms already breached the same - -- one — so it could only ever duplicate an alert the proves fired. - -- The throughputs likewise carry no bound: `constants` is pinned - -- exactly, so each is the pure inverse of an already-bounded time. - thresholds := [("constants", "0", "0"), ("stage1-fft-cost", "0.05", "_"), - ("stage2-fft-cost", "0.25", "_"), - ("stage1-execute-time", "0.10", "_"), - ("stage1-prove-time", "0.10", "_"), - ("stage2-execute-time", "0.10", "_"), - ("stage2-prove-time", "0.10", "_"), - ("stage1-peak-rss", "0.10", "_"), - ("stage2-peak-rss", "0.10", "_"), + -- ixvm-fft-cost is deterministic but only ever drops on a real Aiur + -- win → upper-only 5% instead of a hard pin. fri-verifier-fft-cost + -- drifts ~±15% run-to-run (the parallel prover emits byte-different + -- valid proofs, so the verifier authenticates different Merkle + -- paths) → the loose 25% bound. Proof sizes are structural (fixed + -- query count and path depth) → the tight 5%. `total-time` carries + -- NO bound: it is the two prove times summed, and a sum cannot + -- breach a percentage bound unless one of its terms already breached + -- the same one — so it could only ever duplicate an alert the proves + -- fired. The throughputs likewise carry no bound: `constants` is + -- pinned exactly, so each is the pure inverse of an already-bounded + -- time. + thresholds := [("constants", "0", "0"), ("ixvm-fft-cost", "0.05", "_"), + ("fri-verifier-fft-cost", "0.25", "_"), + ("ixvm-execute-time", "0.10", "_"), + ("ixvm-prove-time", "0.10", "_"), + ("fri-verifier-execute-time", "0.10", "_"), + ("fri-verifier-prove-time", "0.10", "_"), + ("ixvm-peak-rss", "0.10", "_"), + ("fri-verifier-peak-rss", "0.10", "_"), ("pipeline-peak-rss", "0.10", "_"), - ("stage1-proof-size", "0.05", "_"), - ("stage2-proof-size", "0.05", "_"), - ("stage1-verify-time", "0.10", "_"), - ("stage2-verify-time", "0.10", "_")] }, + ("ixvm-proof-size", "0.05", "_"), + ("fri-verifier-proof-size", "0.05", "_"), + ("ixvm-verify-time", "0.10", "_"), + ("fri-verifier-verify-time", "0.10", "_")] }, { name := "zisk", defaultMode := "execute", inputs := .perConstant, testbeds := [("execute", "zisk-check-execute-x64-32x")], metrics := [("execute", ["execute-time", "throughput", "peak-rss", diff --git a/Ix/Cli/BenchPlots.lean b/Ix/Cli/BenchPlots.lean index 6aae4f2c8..c1c8037ab 100644 --- a/Ix/Cli/BenchPlots.lean +++ b/Ix/Cli/BenchPlots.lean @@ -62,14 +62,14 @@ def plotTitle (workload measure : String) : String := | "aiur", "total-time" => "Aiur Total Time" | "aiur", "pipeline-throughput" => "Aiur Total Throughput" | "aiur", "pipeline-peak-rss" => "Aiur Total Peak RAM Usage" - | "aiur", "stage1-prove-time" => "Aiur Stage 1 Time" - | "aiur", "stage2-prove-time" => "Aiur Stage 2 Time" - | "aiur", "stage1-fft-cost" => "Aiur Stage 1 FFT Cost" - | "aiur", "stage2-fft-cost" => "Aiur Stage 2 FFT Cost" - | "aiur", "stage2-verify-time" => "Aiur Stage 2 Verify Time" - | "aiur", "stage2-peak-rss" => "Aiur Stage 2 Peak RAM Usage" - | "aiur", "stage1-proof-size" => "Aiur Stage 1 Proof Size" - | "aiur", "stage2-proof-size" => "Aiur Stage 2 Proof Size" + | "aiur", "ixvm-prove-time" => "Aiur IxVM Time" + | "aiur", "fri-verifier-prove-time" => "Aiur FRI Verifier Time" + | "aiur", "ixvm-fft-cost" => "Aiur IxVM FFT Cost" + | "aiur", "fri-verifier-fft-cost" => "Aiur FRI Verifier FFT Cost" + | "aiur", "fri-verifier-verify-time" => "Aiur FRI Verifier Verify Time" + | "aiur", "fri-verifier-peak-rss" => "Aiur FRI Verifier Peak RAM Usage" + | "aiur", "ixvm-proof-size" => "Aiur IxVM Proof Size" + | "aiur", "fri-verifier-proof-size" => "Aiur FRI Verifier Proof Size" | "zisk-check-execute", "execute-time" => "Zisk Execute Time" | "zisk-check-execute", "throughput" => "Zisk Execute Throughput" | "zisk-check-execute", "peak-rss" => "Zisk Execute Peak RAM Usage" @@ -89,11 +89,11 @@ def plotTitle (workload measure : String) : String := that stage's `prove-time` — a prove runs its own witness execution, so it is the whole cost of producing the stage's proof, and the standalone `execute-time` beside it is a second, instrumentation-only - run. Stage-1 peak-rss / verify-time are tracked for the compare - table but not plotted: their cost is inside `prove-time` and the - deterministic `fft-cost` trend, and stage 1's proof is an - intermediate artifact consumed by the next stage. Stage-1 - `proof-size` IS plotted: it sizes the next stage's in-circuit + run. The ixvm stage's peak-rss / verify-time are tracked for the + compare table but not plotted: their cost is inside `ixvm-prove-time` + and the deterministic `ixvm-fft-cost` trend, and that stage's proof + is an intermediate artifact consumed by the next stage. Its + `ixvm-proof-size` IS plotted: it sizes the next stage's in-circuit verification workload. The whole-run `pipeline-peak-rss` too: which stage sets the run's RAM ceiling can shift as pipeline stages are added, so no per-stage peak plot stands in for it. The per-stage @@ -104,15 +104,15 @@ def plotTitle (workload measure : String) : String := def plotSkips : List (String × String) := [("zisk-check-execute", "constants"), ("ix-decompile", "file-size"), ("ix-decompile", "constants"), - ("aiur", "stage1-peak-rss"), ("aiur", "stage1-verify-time"), - ("aiur", "stage1-execute-time"), ("aiur", "stage2-execute-time"), - ("aiur", "stage1-throughput"), ("aiur", "stage2-throughput")] + ("aiur", "ixvm-peak-rss"), ("aiur", "ixvm-verify-time"), + ("aiur", "ixvm-execute-time"), ("aiur", "fri-verifier-execute-time"), + ("aiur", "ixvm-throughput"), ("aiur", "fri-verifier-throughput")] /-- Canonical units per measure slug, asserted on every sync: bencher auto-creates a measure with placeholder units ("Measure (units)") on its first upload, leaving plots unitless — and a console edit would drift from this list, so the sync re-asserts it. Phase spans are - wall-clock seconds. A stage-qualified slug (`stage1-prove-time`, + wall-clock seconds. A stage-qualified slug (`ixvm-prove-time`, `pipeline-peak-rss`) carries its base measure's units, so only base names are listed. -/ def unitsFor (slug : String) : Option String := diff --git a/Ix/Cli/BenchReport.lean b/Ix/Cli/BenchReport.lean index aa1e39cd0..4b8e59629 100644 --- a/Ix/Cli/BenchReport.lean +++ b/Ix/Cli/BenchReport.lean @@ -37,7 +37,7 @@ open Ix.Cli.BenchCmd (stagePrefixOf dropStagePrefix) /-- Per-metric formatting kind. Metric names are the results-JSON keys the tools emit (see the registry in Ix.Cli.BenchCmd). A stage-qualified - metric formats like its base counterpart (`stage2-peak-rss` and + metric formats like its base counterpart (`fri-verifier-peak-rss` and `pipeline-peak-rss` like `peak-rss`, …). Unknown metrics fall through to a generic decimal rendering. -/ def metricKind (metric : String) : String := @@ -57,7 +57,7 @@ def metricKind (metric : String) : String := (renaming one would orphan its threshold/history); only the table rendering differs. `file-size` is the serialized `.ixe` env — bencher plots it as "Environment Size"; `peak-rss` reads better as plain RAM, - in every slug that embeds it (`stage2-peak-rss` → …-peak-ram); + in every slug that embeds it (`fri-verifier-peak-rss` → …-peak-ram); `throughput` carries its unit here because the runs print bare magnitudes (matching `unitsFor`'s "constants / second" on bencher). -/ def metricLabel (metric : String) : String := @@ -186,7 +186,7 @@ structure CompareSection where /-- The stage qualifier shared by every one of a section's measures, if they share one. A stage table's heading already says which stage it - is, so its columns read `prove-time`, not `stage1-prove-time`. -/ + is, so its columns read `prove-time`, not `ixvm-prove-time`. -/ def sectionLabelDrop (metrics : Array String) : String := match metrics[0]?.bind stagePrefixOf with | some p => if metrics.all (·.startsWith p) then p else "" diff --git a/Tests/Ix/BenchMeasures.lean b/Tests/Ix/BenchMeasures.lean index 4e3974096..7a83e6276 100644 --- a/Tests/Ix/BenchMeasures.lean +++ b/Tests/Ix/BenchMeasures.lean @@ -16,24 +16,24 @@ open LSpec Ix.Cli.BenchCmd namespace Tests.Ix.BenchMeasures def testStagePrefix : TestSeq := - test "stage1- strips" (dropStagePrefix "stage1-prove-time" == "prove-time") - ++ test "stage2- strips" (dropStagePrefix "stage2-peak-rss" == "peak-rss") - ++ test "multi-digit stage strips" - (dropStagePrefix "stage12-fft-cost" == "fft-cost") + test "ixvm- strips" (dropStagePrefix "ixvm-prove-time" == "prove-time") + ++ test "fri-verifier- strips" + (dropStagePrefix "fri-verifier-peak-rss" == "peak-rss") ++ test "pipeline- strips" (dropStagePrefix "pipeline-throughput" == "throughput") - ++ test "stage1- prefix identified" - (stagePrefixOf "stage1-verify-time" == some "stage1-") + ++ test "ixvm- prefix identified" + (stagePrefixOf "ixvm-verify-time" == some "ixvm-") + ++ test "fri-verifier- prefix identified" + (stagePrefixOf "fri-verifier-fft-cost" == some "fri-verifier-") ++ test "unqualified name passes through" (dropStagePrefix "execute-time" == "execute-time") - ++ test "stage without digits is not a qualifier" - (stagePrefixOf "stage-time" == none) - ++ test "stage digits without dash is not a qualifier" - (stagePrefixOf "stage1time" == none) - ++ test "stage prefix inside a word is not a qualifier" - (stagePrefixOf "stagehand-time" == none) - ++ test "bare stage name passes through" - (dropStagePrefix "stages" == "stages") + ++ test "prefix without dash is not a qualifier" + (stagePrefixOf "ixvmtime" == none) + ++ test "fri- alone is not a qualifier" + (stagePrefixOf "fri-fold-time" == none) + ++ test "phase spans pass through" + (dropStagePrefix "phase-stark-stage1-commit" + == "phase-stark-stage1-commit") def suite : List TestSeq := [testStagePrefix] diff --git a/docs/benchmarking.md b/docs/benchmarking.md index c6ac133c6..758b658a2 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -93,7 +93,7 @@ a PR tree and compare them — exactly what the PR workflow does. | backend | what it measures | tool | |---|---|---| -| `aiur` | the Aiur 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 (the KZG stages fold in as they land), closed by the pipeline ledger (total-time, pipeline-throughput, pipeline-peak-rss). The whole system runs under the recursion-tuned FRI parameters. A second mode, execute, is the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss) — unscheduled, local/on-demand only (`!benchmark aiur execute`) | `bench-typecheck --recursive` | +| `aiur` | the Aiur proof pipeline, per constant: the `ixvm` stage proves the IxVM typecheck, the `fri-verifier` stage executes and proves the in-circuit multi-stark verifier over that fresh proof (the KZG stages fold in as they land, each with its own measure prefix), closed by the pipeline ledger (total-time, pipeline-throughput, pipeline-peak-rss). Each stage's measures carry its prefix (`ixvm-prove-time`, `fri-verifier-fft-cost`, …). The whole system runs under the recursion-tuned FRI parameters. A second mode, execute, is the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss) — unscheduled, local/on-demand only (`!benchmark aiur execute`) | `bench-typecheck --recursive` | | `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (the runtime-planned partition size; 1 when the closure fits) | `zisk-host` | | `sp1` | SP1 VM execute (currently disabled in the registry) | `sp1-host` | | `ooc` | out-of-circuit Rust kernel: whole-env row + one full-closure row per constant (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-rs --json` | @@ -102,10 +102,7 @@ a PR tree and compare them — exactly what the PR workflow does. | `decompile` | inverse of compile — `ix decompile .ixe → Lean consts`: decompile-time, throughput, peak-rss, constants, file-size (input `.ixe`). Consumes the compile cell's `.ixe` rather than producing one; a malformed decompile reddens the cell. Deep roundtrip fidelity is gated by the canonical checks (`ix validate` / roundtrip tests), which need the original Lean env the `.ixe` can't supply | `ix decompile --json` | All tools emit the same rows, and all the constant-driven ones take the same -`--consts`/`--consts-file` grammar. (`bench-recursive-verifier`, the local -toy-statement harness for parameter sweeps, instead takes its config as -flags — `--trivial`, `--queries`, `--log-blowup` — with the row name -supplied via `--json-name`.) The ooc and zkVM cells share per-constant +`--consts`/`--consts-file` grammar. The ooc and zkVM cells share per-constant **full-closure** scope, so their delta isolates in-circuit vs out-of-circuit overhead. diff --git a/lakefile.lean b/lakefile.lean index 7c1f43ca8..5df0808a5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -143,10 +143,6 @@ lean_exe «bench-typecheck» where root := `Benchmarks.Typecheck supportInterpreter := true -lean_exe «bench-recursive-verifier» where - root := `Benchmarks.RecursiveVerifier - supportInterpreter := true - lean_exe «bench-recursion-debug» where root := `Benchmarks.RecursionDebug supportInterpreter := true