Uh oh!
There was an error while loading. Please reload this page.
ci: Fix bencher.dev thresholds - #459
Merged
Merged
Conversation
samuelburnhamforce-pushed
the
ci-benchmarking
branch
from
June 30, 2026 18:26
dc9f973 to
8edcaceComparesamuelburnhamforce-pushed
the
ci-benchmarking
branch
from
June 30, 2026 18:26
8edcace to
1ad4bd0Comparearthurpaulino
approved these changes
Jun 30, 2026
Uh oh!
There was an error while loading. Please reload this page.
samuelburnham added a commit
that referenced
this pull request
Jul 2, 2026
Rebased onto main (post #411 + #459) and integrated with the renamed bench-main.yml and reworked bencher-track interface. - Benchmarks/Vectors.csv: single shared source of truth (71 library constants from Init/Std/Mathlib/Lean). Consumed by Aiur (bench-typecheck --manifest), the zkVM hosts, and shell. - bench-pr.yml: `!benchmark [aiur] [zisk] [sp1|all] [execute|prove]` over the curated set, posting a main-vs-PR table; main results cached by base SHA. Hardened: comment body from env (no injection), allowlisted env parsing. - .github/scripts/{bench.py,run.sh}: parse/manifest/compare/comment, and the compile-.ixe + backend driver (cycles/execute-time/throughput/peak-rss, plus shards/max-shard-cycles for sharded runs). - .github/actions/install-{sp1,zisk}: shared zkVM toolchain + deps install, used by bench-pr.yml, bench-main.yml, and riscv-bench.yml. - bench-main.yml: add zkvm-execute (Zisk/SP1 cycle counts + time/RAM) and native-check (native parallel `ix check --anon` throughput) jobs, using the new bencher-track workload/thresholds interface. - bench-typecheck: add --constant / --skip-deps (align with the zkVM hosts; --skip-deps replaces --subject-only) and --execute-only (fast execute path).
samuelburnham added a commit
that referenced
this pull request
Jul 2, 2026
Rebased onto main (post #411 + #459) and integrated with the renamed bench-main.yml and reworked bencher-track interface. - Benchmarks/Vectors.csv: single shared source of truth (71 library constants from Init/Std/Mathlib/Lean). Consumed by Aiur (bench-typecheck --manifest), the zkVM hosts, and shell. - bench-pr.yml: `!benchmark [aiur] [zisk] [sp1|all] [execute|prove]` over the curated set, posting a main-vs-PR table; main results cached by base SHA. Hardened: comment body from env (no injection), allowlisted env parsing. - .github/scripts/{bench.py,run.sh}: parse/manifest/compare/comment, and the compile-.ixe + backend driver (cycles/execute-time/throughput/peak-rss, plus shards/max-shard-cycles for sharded runs). - .github/actions/install-{sp1,zisk}: shared zkVM toolchain + deps install, used by bench-pr.yml, bench-main.yml, and riscv-bench.yml. - bench-main.yml: add zkvm-execute (Zisk/SP1 cycle counts + time/RAM) and native-check (native parallel `ix check --anon` throughput) jobs, using the new bencher-track workload/thresholds interface. - bench-typecheck: add --constant / --skip-deps (align with the zkVM hosts; --skip-deps replaces --subject-only) and --execute-only (fast execute path).
samuelburnham added a commit
that referenced
this pull request
Jul 3, 2026
Rebased onto main (post #411 + #459) and integrated with the renamed bench-main.yml and reworked bencher-track interface. - Benchmarks/Vectors.csv: single shared source of truth (71 library constants from Init/Std/Mathlib/Lean). Consumed by Aiur (bench-typecheck --manifest), the zkVM hosts, and shell. - bench-pr.yml: `!benchmark [aiur] [zisk] [sp1|all] [execute|prove]` over the curated set, posting a main-vs-PR table; main results cached by base SHA. Hardened: comment body from env (no injection), allowlisted env parsing. - .github/scripts/{bench.py,run.sh}: parse/manifest/compare/comment, and the compile-.ixe + backend driver (cycles/execute-time/throughput/peak-rss, plus shards/max-shard-cycles for sharded runs). - .github/actions/install-{sp1,zisk}: shared zkVM toolchain + deps install, used by bench-pr.yml, bench-main.yml, and riscv-bench.yml. - bench-main.yml: add zkvm-execute (Zisk/SP1 cycle counts + time/RAM) and native-check (native parallel `ix check --anon` throughput) jobs, using the new bencher-track workload/thresholds interface. - bench-typecheck: add --constant / --skip-deps (align with the zkVM hosts; --skip-deps replaces --subject-only) and --execute-only (fast execute path).
samuelburnham added a commit
that referenced
this pull request
Jul 8, 2026
Rebased onto main (post #411 + #459) and integrated with the renamed bench-main.yml and reworked bencher-track interface. - Benchmarks/Vectors.csv: single shared source of truth (71 library constants from Init/Std/Mathlib/Lean). Consumed by Aiur (bench-typecheck --manifest), the zkVM hosts, and shell. - bench-pr.yml: `!benchmark [aiur] [zisk] [sp1|all] [execute|prove]` over the curated set, posting a main-vs-PR table; main results cached by base SHA. Hardened: comment body from env (no injection), allowlisted env parsing. - .github/scripts/{bench.py,run.sh}: parse/manifest/compare/comment, and the compile-.ixe + backend driver (cycles/execute-time/throughput/peak-rss, plus shards/max-shard-cycles for sharded runs). - .github/actions/install-{sp1,zisk}: shared zkVM toolchain + deps install, used by bench-pr.yml, bench-main.yml, and riscv-bench.yml. - bench-main.yml: add zkvm-execute (Zisk/SP1 cycle counts + time/RAM) and native-check (native parallel `ix check --anon` throughput) jobs, using the new bencher-track workload/thresholds interface. - bench-typecheck: add --constant / --skip-deps (align with the zkVM hosts; --skip-deps replaces --subject-only) and --execute-only (fast execute path).
samuelburnham added a commit
that referenced
this pull request
Jul 9, 2026
Rebased onto main (post #411 + #459) and integrated with the renamed bench-main.yml and reworked bencher-track interface. - Benchmarks/Vectors.csv: single shared source of truth (71 library constants from Init/Std/Mathlib/Lean). Consumed by Aiur (bench-typecheck --manifest), the zkVM hosts, and shell. - bench-pr.yml: `!benchmark [aiur] [zisk] [sp1|all] [execute|prove]` over the curated set, posting a main-vs-PR table; main results cached by base SHA. Hardened: comment body from env (no injection), allowlisted env parsing. - .github/scripts/{bench.py,run.sh}: parse/manifest/compare/comment, and the compile-.ixe + backend driver (cycles/execute-time/throughput/peak-rss, plus shards/max-shard-cycles for sharded runs). - .github/actions/install-{sp1,zisk}: shared zkVM toolchain + deps install, used by bench-pr.yml, bench-main.yml, and riscv-bench.yml. - bench-main.yml: add zkvm-execute (Zisk/SP1 cycle counts + time/RAM) and native-check (native parallel `ix check --anon` throughput) jobs, using the new bencher-track workload/thresholds interface. - bench-typecheck: add --constant / --skip-deps (align with the zkVM hosts; --skip-deps replaces --subject-only) and --execute-only (fast execute path).
samuelburnham added a commit
that referenced
this pull request
Jul 9, 2026
* fix(zisk): drop --max-witness-stored flag, use Zisk's default cap
Lowering the witness cap below Zisk's built-in default (10) was measured to
have a negligible effect on host RAM and prove time for the kernel typecheck
workload, so the CLI override (which defaulted to 5) is removed and the prover
uses EmbeddedOpts::default(). Drop the now-stale flag mentions and per-RAM
tuning guidance from the README, the cost-model doc, and the shard.rs model
comments.
* feat(ci): CSV-driven !benchmark + Zisk/SP1/native benchmarks
Rebased onto main (post #411 + #459) and integrated with the renamed
bench-main.yml and reworked bencher-track interface.
- Benchmarks/Vectors.csv: single shared source of truth (71 library constants
from Init/Std/Mathlib/Lean). Consumed by Aiur (bench-typecheck --manifest),
the zkVM hosts, and shell.
- bench-pr.yml: `!benchmark [aiur] [zisk] [sp1|all] [execute|prove]` over the
curated set, posting a main-vs-PR table; main results cached by base SHA.
Hardened: comment body from env (no injection), allowlisted env parsing.
- .github/scripts/{bench.py,run.sh}: parse/manifest/compare/comment, and the
compile-.ixe + backend driver (cycles/execute-time/throughput/peak-rss, plus
shards/max-shard-cycles for sharded runs).
- .github/actions/install-{sp1,zisk}: shared zkVM toolchain + deps install,
used by bench-pr.yml, bench-main.yml, and riscv-bench.yml.
- bench-main.yml: add zkvm-execute (Zisk/SP1 cycle counts + time/RAM) and
native-check (native parallel `ix check --anon` throughput) jobs, using the
new bencher-track workload/thresholds interface.
- bench-typecheck: add --constant / --skip-deps (align with the zkVM hosts;
--skip-deps replaces --subject-only) and --execute-only (fast execute path).
* test(ci): trigger bench-pr.yml on pull_request (TEMPORARY)
issue_comment workflows only run from the default branch, so the `!benchmark`
path can't be exercised on a PR branch. Add a pull_request trigger (base/head
from the PR payload; empty comment → parser defaults) to test pre-merge.
Revert before merge — delete the `pull_request:` trigger; the dual base/head
resolution and `|| pull_request.number` fallbacks are harmless to keep.
* feat(ci): default to ~11 primary constants
The full curated set (~60 InitStd) is too slow to run on every !benchmark and on
the bencher prove/zkVM jobs. Add a `primary` column to Vectors.csv marking 11
constants spanning shape (nat/list/array/int/string/vector/multiset, defs +
proofs) and the cheap→heavy cost range (incl. 3 shard targets), and make it the
default:
- bench.py manifest --primary; parse honors BENCH_FULL (run the full set).
- bench-pr.yml: !benchmark defaults to the primary subset; BENCH_FULL=1 runs the
whole curated set.
- bench-main.yml: prove + zkvm-execute derive constants from `manifest --primary`
(replacing the hardcoded lists), so all backends bench the same set from the one
source of truth. The tier filter keeps prove on the cheap primaries (heavy ones
would OOM a single-shard prove); execute/native get the heavy ones for scale.
* feat(ci): native backend on !benchmark + bencher parity/cleanup
Bring both surfaces (!benchmark PR comment and bencher.dev) to parity across all
four backends and remove the test scaffolding.
- Native kernel on !benchmark: add a `native` backend (whole-env `ix check
--anon`, the parallel out-of-circuit kernel) — bench.py backend/runner/metrics,
a run.sh `native` branch, and a GNU-time install for native PR cells. `all`
now fans out aiur/zisk/sp1/native.
- run.sh: single-source the Aiur path through a per-constant bench-typecheck loop
(per-constant peak-rss), add a per-constant `timeout` to the zkVM execute path
(heavy primaries can't hang a job), and accept the env arg case-insensitively
(bencher reuses the cached InitStd.ixe; bench-pr compiles initStd.ixe).
- bench-main.yml: the prove and native-check jobs now drive run.sh too (dedup
with the PR path); zkvm-execute gains the Mathlib env to match prove/native.
- bench-thresholds-reset.yml: register the zisk / sp1 / native-check workloads.
- bench-pr.yml: drop the temporary pull_request trigger (keep the harmless
dual-SHA / number fallbacks).
- docs/benchmarking.md: document the two surfaces, backends, Vectors.csv, the
!benchmark grammar, and the bencher workloads / threshold resets.
* feat(ci): Aiur proves all primaries that fit 128GB; native checks primaries too
- Aiur prove now covers the whole primary subset: bench.py exempts --primary from
the prove cheap-tier cap, and run.sh proves each constant whose Aiur fft-cost
fits the prover RAM ceiling (AIUR_PROVE_MAX_FFT, ~128 GB at 2.34 GB per billion
fft) and execute-only's the rest — so heavy primaries (only Vector.extract_append
at ~145 GB) still report execute metrics instead of being dropped. BENCH_FULL
prove stays capped at the cheap tier so it doesn't balloon.
- native now reports two views per env: the whole env (`ix check --anon`, keyed by
env) and a per-primary subject check (`ix check --consts`, keyed by constant) —
apples-to-apples with the zkVM --skip-deps execute. Wired into both the
native-check bencher job and the !benchmark native backend.
- run.sh: fix a stream-corruption bug — tool stdout and ::warning::/::notice:: now
go to logs/stderr so only JSON reaches the per-constant `jq -s` merge.
* feat(ci): texray per-phase drill-down + child-process-aware peak RAM
Route every backend's peak-rss and per-phase timings through tracing-texray:
- peak-rss now comes from the fork's process-tree sampler, so Zisk's ASM
microservices' memory (tens of GB in separate PIDs) is captured — a bare
/proc/self/status read of the host missed it. Verified on real execute
runs: sp1 ~9GB, zisk ~49GB peak.
- zisk/sp1 hosts and bench-typecheck self-report cycles/time/throughput/
peak-rss via --json, retiring run.sh's grep/awk/time parsing. They also
emit per-phase span timings via --texray-json; native check-rs reports
peak-rss as a 6th ##check## field.
- run.sh folds span timings into a per-constant `phases` object; bench.py
renders a collapsible per-phase drill-down in the !benchmark comparison,
and bench-main.yml tracks phase:<span> measures on bencher.
tracing-texray is pinned to the argumentcomputer/tracing-texray json-ram
branch (rev 15ae57c), which adds the process-tree RSS sampler + JSON sink.
* refactor(ci): rename backend native→ooc; suffix bencher workloads with -check
- Backend `native` is renamed to `ooc` (out-of-circuit) throughout: the
BACKENDS tuple in bench.py, the run.sh case arm, the `native-check` job
in bench-main.yml (now `ooc-check`), the `\!benchmark` grammar in
bench-pr.yml, and docs/benchmarking.md.
- Bencher workload names carry an explicit `-check` suffix so the tracked
identity is self-describing: `aiur-check`, `zisk-check`, `sp1-check`,
`ooc-check` (was `aiur`, `zisk`, `sp1`, `native-check`). Reset workflow
tokens (options / valid / accepted / error text), tag-reference comments,
and the bencher-track action's docstring updated to match.
- Clarify the `\!benchmark` grammar: `([aiur] [zisk] [sp1] [ooc] | all)` —
`all` is an alternative to the whole backend list, not just to `ooc`.
* refactor(ci): bencher-first !benchmark, unified --consts CLI, RAM harness
**bench.py !benchmark surface**
- `fetch-main`: queries bencher.dev's public reports API for `branch=main` at
the base SHA, filters results by `--names`, and reshapes into the neutral
`{ "<name>": { "<metric>": v } }` shape. Replaces the actions/cache layer;
bench-pr.yml falls back to a local base run only when bencher hasn't
ingested the base SHA yet. TODO left for non-main base branches.
- Mode is fixed per backend (`aiur=prove`, others=`execute`); the optional
bare `execute` token in `!benchmark` flips aiur to `--execute-only`.
Grammar drops `[execute|prove]` and `BENCH_GPU`; zkVM prove paths removed.
- Single runner `warp-ubuntu-latest-x64-32x` for every cell; testbeds
unified to `<backend>-check-x64-32x`; `MAIN_TESTBEDS` maps (backend, mode)
to the slug.
- `compare` renders the OOM sentinel `{"oom": true}` as `OOM` cells + `n/a`
Δ%. Regression/improvement flags fire on every metric column (previously
only the first); summary counts distinct constants; worst names constant
+ metric. `_human` is unit-aware: bytes → GiB/MiB, seconds → µs/ms/s/m,
counts → K/M/B/T.
- Sub-span (per-constant phase) drill-down removed with a TODO; `run.sh`'s
`merge_phases` and `bench-main.yml`'s `phase:<span>` flattening still
populate the neutral JSON for later reinstatement.
**CLI unification** (bench-typecheck, zisk-host, sp1-host)
- Dropped `--constant`; added `--consts <n1,n2,…>` (comma-list, clap
`value_delimiter` on the Rust hosts) and `--consts-file <path>`.
Multi-const runs loop the single-const path per name, accumulating one
entry per name via a merge-safe `write_json_entry`.
- Dropped `--texray-json <path>` and `--no-texray`. `--texray` (bool) alone
toggles the tracing-texray subscriber; combined with `--json <path>`,
span timings auto-write to `<json>.spans`.
- Inline `#[cfg(test)] mod cli_tests` in each Rust host covers
value-delimiter parsing, `--consts` `requires`, and `collect_consts`
union/dedup.
**Vectors.csv**
- Removed `aiur_fft`, `zisk_cycles` (measurements live in bencher, never
here). Rows can now omit trailing zero fields; parser tolerates 3+ cols.
- Primary set curated: renamed `Vector.extract_append` →
`Vector.extract_append._proof_1` (kept as shard_target); promoted
`Vector.append` and `Nat.sub_le_of_le_add` to primary; added the un-
shardable Init constants from the Zisk cost-model doc's canonical 12
(`Char.ofOrdinal_le_of_le`, `Array.extract_append._proof_1_1`, the
`SInt.Int{8,16,32,64}.instRxcHasSize_eq` family with the case corrected),
plus `ByteArray.utf8DecodeChar?_utf8EncodeChar_append`, `String.append`,
`IxVMPrim.nat_pow_big`, and
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`.
Trimmed obvious duplicates (`Array.qsort`, `Int.ediv`, `List.dropLast`,
`List.range`, `UInt32.toNat`, `Std.Time.Month.Offset.ofNat`).
**RAM harness** (run.sh, aiur prove)
- Tier gate removed. Every constant attempts a full prove.
- `watch_ram_kill` samples `ps -eo pid,ppid,rss` every ~3 s and SIGKILLs
the tree if it exceeds `AIUR_PROVE_MAX_RSS_GB` (default 120 GB — 8 GB
headroom under 128 GB). Killed constants record `{"oom": true}` for the
compare table.
**Misc**
- `install-zisk`'s description now correctly says the proving key is
installed (`client.setup()` loads const-trees before execute too).
- `bencher-track`'s workload description enumerates all options.
- `zisk/Cargo.toml`'s patch example uses `/path/to/…`, not `/home/ubuntu`.
- `docs/zisk-cycle-cost-model.md` finding #4 disambiguates
"not-shardable" (mutual blocks only) from "not full-closure-single-leaf
provable" (the canonical 12).
- `riscv-bench.yml` still on the temporary `sb/ci-benchmarks` push
trigger; drop before merge.
* feat(ci): compile as a !benchmark backend; full-closure zkVM parity; threshold + doc cleanup
**`compile` as a !benchmark backend**
- bench.py: `DEFAULT_MODE["compile"]="compile"`,
`MAIN_TESTBEDS[("compile","compile")]="ix-compile-x64-32x"`,
`METRICS[("compile","compile")]=["compile-time","throughput","file-size",
"constants"]`. `cmd_manifest` short-circuits on `--backend compile`: writes
a one-line names.txt with the CamelCase env slug (`InitStd` / `Lean` /
`Mathlib` / `FLT`) and skips the CSV. New `--backend` arg on manifest.
- run.sh: setup step teed to `$compile_log` for every backend; `compile`
ignores REUSE_IXE (needs a fresh compile to measure) and parses
`##benchmark## <elapsed_ms> <bytes> <constants>` into the neutral
`{ "<CamelCase>": {"compile-time","file-size","constants","throughput"} }`
shape. Compile job on main (`bench-main.yml` testbed
`ix-compile-x64-32x`) is the same run bencher already stores.
- bench-pr.yml: `!benchmark ([aiur] [zisk] [sp1] [ooc] [compile] | all)`;
manifest step passes `--backend "$BACKEND"`.
**zkVM parity with ooc (drop `--skip-deps`)**
- run.sh zisk/sp1 branch: `--consts <c>` without `--skip-deps` so the check
is directly comparable to `ooc`'s `ix check-rs --consts <c>` (also
full-closure). Comparing subject-only zkVM against full-closure ooc mixed
in-circuit-vs-out-of-circuit overhead with scope; both are now
full-closure, so the delta isolates just the overhead.
**Threshold semantics for deterministic-but-directional measures**
- bench-main.yml zkvm-execute (now zkvm-typecheck): `cycles`, `shards`,
`max-shard-cycles` change from pinned `0/0` to `upper 0 / lower _`.
These are deterministic (no noise) but a real guest / packer improvement
legitimately drops them; the old pin flagged wins as regressions.
`constants` (definitional count) stays `0/0`.
**docs/benchmarking.md — stale content swept**
- Removed the "design-level skips post a note explaining why" paragraph
(that machinery was already removed).
- Replaced the `cheap → prove / heavy → execute-only` fallback description
with the RAM-watchdog reality (attempts prove for every primary; OOMs go
through as `{"oom": true}` sentinels rendered `OOM`).
- Backends table adds `compile`; drops metrics `aiur` doesn't actually emit.
- "Constant set": ~20 primaries in ~68 total (was ~11 in ~60); notes tier
is informational-only now, rows may omit trailing zeros, and `compile`
short-circuits the CSV.
- Per-measure threshold breakdown replaces the incorrect "Deterministic
measures … are pinned exactly" claim.
- "Not yet covered" now lists three real TODOs (zkVM prove, per-constant
phase drill-down, non-main base branches) with pointers to the in-code
TODO markers.
**Code comment audit** — every touched comment/docstring re-read; stale
references to `--skip-deps` parity, tier-based fallback, sub-span
drill-down, and cache-hit rendering all updated to match implementation.
* feat(ci): annotate compare table cells with ratio (1.5x faster/slower)
Δ% is easier to interpret at scale when paired with a ratio — e.g.
`-33.3% (1.50x faster)` for a big prove-time drop; `+15.2% (1.15x slower)`
for a real execute-time regression. Only shown when the factor is >= 1.05x
(roughly ±5% in either direction) so sub-noise deltas don't get
`(1.02x slower)` clutter next to `+1.1%`. Cell format cascades cleanly:
`{Δ%} [(1.NN× {slower|faster})] [emoji]`.
* fix(ci): review fixes — full-closure check-rs, OOM/polarity/caching, dedup
Fixes from the branch-wide review, plus build-once caching and a dedup pass.
**check-rs full-closure mode (new kernel FFI)**
- `rs_kernel_check_anon_consts`: resolve displayed names via the env's
`named` map (the zkVM hosts' resolution), then anon-check the seeds'
FULL dependency closures via the existing `closure_addrs` +
`build_anon_work` primitives — no sub-env serialization. `skip_deps`
restricts to subject-only. `index_anon_work` extracted so the whole-env
and filtered paths share the result-slot indexing.
- `ix check-rs --anon --consts <names>` now runs that (full-closure default,
`--skip-deps` opt-out — the hosts' CLI shape); meta-mode seeded checks are
unchanged (subject-only, bisect flows intact). run.sh's ooc per-constant
view uses it, so ooc-vs-zkVM deltas genuinely isolate in-circuit overhead
(both sides now full-closure anon; previously ooc was subject-only meta).
**OOM sentinel end-to-end**
- run.sh merges `oom: true` INTO already-measured Phase-1 metrics (was:
overwrite); compare renders OOM only for the missing metrics.
- `bench.py bmf` (one neutral→BMF converter replacing four hand-copied
jq/awk pipelines in bench-main.yml) strips the boolean sentinel — one
OOM row no longer fails the whole bencher upload. This also covers the
zkVM execute path, which gained its own RAM watchdog + sentinel.
- Watchdog: setsid + process-group kill (reaches all descendants); kernel
OOM beating the 3 s sampler (exit 137, no marker) labels OOM instead of
silently dropping; per-constant wall-clock timeouts (AIUR_PROVE_TIMEOUT
50m / AIUR_EXECUTE_TIMEOUT 25m); $out re-merged per constant so a
job-level kill keeps completed rows.
**compare correctness**
- throughput is higher-is-better: flags/worst/ratio direction-aware
(HIGHER_IS_BETTER + _badness).
- Ratio wording follows metric kind: times faster/slower, bytes
larger/smaller, counts more/fewer.
- `execute-peak-rss`: Phase-1 RSS high-water sampled at the Phase 1/2
boundary in bench-typecheck (both modes) and adopted by the zkVM hosts'
execute JSON — one name for "execute-phase peak" on every backend;
bare `peak-rss` reserved for prove-phase peaks. aiur-execute compares
it apples-to-apples against prove-run baselines (raw peak-rss would
dwarf it).
- One-side-empty tables get a loud note (e.g. CLI-incompatible base).
- Tidy JSON: bench-typecheck emits decimal `JsonNumber`s (`jsonRound`)
instead of Float's full binary repr.
**fetch-main robustness**
- Retry with backoff + newest-first pagination (base SHA beyond page one
no longer forces a permanent fallback).
- Exit codes honored by bench-pr.yml: 3 (transient) → local fallback;
2 (BACKEND_TABLE / bench-main drift) fails the cell loudly.
- ooc whole-env row keyed CamelCase on both sides (benv_cc table in
run.sh, ENV_CC in bench.py) and admitted past the --names filter.
**build-once + caching (bench-pr.yml)**
- New build job: ix + bench-typecheck built once per head SHA (they embed
the IxVM kernel/prover), cached as `bench-bins-<sha>`; cells restore
into .bins/pr instead of per-cell Lean builds. Re-running \!benchmark on
the same commit skips the build.
- Base fallback restores bench-main's own `bench-bins-`/`bench-ixe-`
caches (toolchain cmp + mathlib-oleans guard) before paying for a
from-scratch base build. PR-side .ixe cached across cells.
- Cache keys renamed `aiur-bench-bins-`/`aiur-ixe-` →
`bench-bins-`/`bench-ixe-` (they serve every backend).
- run.sh resolves tools in-tree first, then PATH (`resolve_bin`).
**dedup**
- bench.py: DEFAULT_MODE + METRICS + MAIN_TESTBEDS collapsed into one
BACKEND_TABLE (mode / testbed / per-mode metrics).
- bench-main's compile job routes through run.sh's compile backend + bmf —
the `##benchmark##` line is parsed in exactly one place (run.sh gains
`flt` in its env table for the FLT matrix cell).
- `Ix.Cli.ConstsFile`: one names-file/comma-list parser (inline-`#`
comments, dedup) shared by check-rs meta+anon, bench-typecheck, and
`ix compile --exclude-file` — closes the whole-line-vs-inline comment
drift across the five previous copies.
**hosts**
- clap `requires = "consts"` dropped from --json/--skip-deps (rejected
valid --consts-file-only runs); validated in main after collect_consts.
zisk's multi-`--ixe` guard now covers --consts-file.
**misc**
- Vectors.csv / docs tier semantics corrected (manifest-only consumer);
stale prove-fallback comments fixed; tracing-texray bumped to bd4faa08;
push-to-main workflows drop their concurrency groups (every merged
commit must be benchmarked; a later merge must never cancel one).
Verified: cargo check -p ix-ffi, lake build ix / bench-typecheck, live
runs of the new check-rs mode against a 480 MB Init/Std env (closure =
34 items / 42 targets for Nat.add_comm; --skip-deps = 1; missing names
error loudly), bmf/parse/compare dry-runs, YAML + bash -n + AST checks.
zisk/sp1 host crates compile-verified in CI only (local sandbox lacks
the pil2-proofman C++ toolchain).
* ci: convert riscv-bench into a zkVM host build+test gate (no proving key)
bench-main.yml's zkvm-execute job now runs real executions of both hosts
on every main push, but tolerates per-constant failures by design
(dropped rows, OOM sentinels) — it never turns red on a breakage. This
workflow becomes the red-X signal instead, kept cheap:
- Build-only + unit tests: `cargo build --release --bin <host>` plus
`cargo test --release --bin <host>`, which covers the clap surface
run.sh drives (--consts comma-splitting, --consts-file union/dedup,
shard-plan conflicts). No execution, so no fixture compile job, no
minimal.ixe artifact, no memlock prlimit.
- install-zisk gains a `proving-key` input (default true): the key is
loaded at runtime by `client.setup()`, never at build time, so the
build gate skips the ~3 GB download + const-tree regeneration.
- Renamed "RISC-V bench" → "zkVM host build" (it no longer benchmarks).
- The TEMPORARY sb/ci-benchmarks push trigger (from the mid-branch test
commit) reverts to main-only here; the tip commit is its sole carrier.
The runtime/typecheck smoke signal (executing myReflEq and asserting
failures == 0) is retired: that coverage now lives in zkvm-execute's
real runs, at the cost of being warnings-not-red-X.
* fix(ci): pre-build proofman-starks-lib-c to serialize the shared make
zisk-host pulls zisk-sdk as both a dependency and a build-dependency, so
cargo compiles proofman-starks-lib-c as two units whose build scripts can
run concurrently — and both run `make` inside the SHARED
~/.cargo/git/checkouts/pil2-proofman-* source tree (not OUT_DIR). On a
cold runner the Makefile stamp is absent, so both units take the
`make clean` + `make -j` path and race: one unit's clean deletes build/
while the other's g++ is mid-compile, dying with "opening dependency
file ….d: No such file or directory" (g++ writes .d files at the END of
compilation, so the dir vanished underneath it). Warm runners never hit
it — the stamp short-circuits the clean — which is why the race only
surfaced on this branch's cold cache (lockfile change → new rust-cache
key).
install-zisk now builds the sys crate solo first: its build script runs
once, `make` completes, the stamp lands; both units of the subsequent
parallel build then skip the clean and their `make -j` is a no-op. Same
total work, just ordered. The proper fix is an flock around the make in
pil2-proofman's build.rs — worth an upstream PR.
* fix(ci): resolve run.sh tool binaries lazily at their use sites
`resolve_bin ix` ran unconditionally at startup, but bench-main's
zkvm-execute job legitimately has no `ix` anywhere: it restores only the
`.ixe` cache (REUSE_IXE=1 skips the compile step) and builds its zkVM
host via cargo — before the resolve_bin refactor that job never touched
`ix` at all, so the eager check regressed it with "ix not found
(in-tree or PATH)". Resolve per use site instead: the compile step and
the ooc branch resolve `ix`, the aiur branch resolves `bench-typecheck`,
and the zkVM branch needs neither.
* fix(ci): classify alloc-abort proves as OOM, sweep Zisk shm, fix vector names
Three fixes for the failing bench-main runs:
- run.sh: a heavy prove can die of memory without tripping the watchdog or
the kernel OOM killer — one huge trace allocation fails and the runtime
aborts (SIGABRT, exit 134) with an allocator message. looks_like_oom()
folds that third case into the OOM classification so those constants get
an OOM row instead of being dropped. Non-OOM failures now log the first
lines of the tool output so drops are diagnosable from the job log.
- run.sh: after a watchdog group-kill, the Zisk host never runs its
Drop-time cleanup of /dev/shm/ZISK_* segments (multi-GB; the MT output
segment alone starts at 6 GB), so the next host launch fails creating its
own segments before Zisk's startup stale-pid sweep runs — exactly one
dropped constant after every OOM kill (the alternating OOM/exit-1 pattern
in the zisk-execute logs). Sweep the debris between constants.
- Vectors.csv: IxVMPrim.nat_pow_big removed (kernel primitive, never
present in compiled envs); Vector.extract_append._proof_1 →
._proof_2 and Array.extract_append._proof_1_1 → Array.extract_append
(proof-term names are toolchain-dependent; both replacements verified
against a freshly compiled initStd.ixe and measured heavy:
fft-cost 23.4e9 / 40.1e9).
* ci: move the zkVM host build gate into ci.yml; comment out the sp1 benchmarks
riscv-bench.yml's two jobs (build + unit-test the Zisk/SP1 hosts, no
execution, no proving key) are cheap enough (~5 min with warm caches) to
gate every PR commit, and ci.yml already has exactly the triggers and
per-ref cancellation they need — so they move there and the standalone
workflow goes away.
sp1 benchmarks are commented out for now — the execute run is too slow:
the sp1 cell of bench-main's zkvm-execute matrix and bench-pr's Install
SP1 step. Uncomment both to re-enable. The \!benchmark backend-subset
selection is unchanged.
* fix(aiur): populate trace rows for UnconstrainedBigUintDivMod
The op (added with the native execution pipeline, #463) pushes two values
onto the value map during execution — the quotient/remainder list-head
pointers — and the constraint generator allocates two auxiliary columns
for them, but the trace populator treated it as a no-op. Every ValIdx and
witness column after the first big-Nat division in a block was therefore
off by two, and trace population panicked with "index out of bounds" at
trace.rs:308 — the exit-134 failures on every big-Nat-heavy prove in the
bench-main aiur job (List.mergeSort, String.split, the SInt
instRxcHasSize_eq family, Multiset.sort, …). Reproducible in seconds
with any Nat-division user, e.g. `bench-typecheck --consts Nat.repr`.
The trace arm now mirrors the execute arm: recompute (q, r) with
num_bigint and resolve the head pointers execution already recorded in
memory[10] via a read-only twin of build_klimbs_u64, pushing both as map
entries + auxiliary columns.
Verified: Nat.repr proves end-to-end (panicked before); `lake test --
--ignored aiur ixvm` passes; clippy clean.
* feat(bench): track Aiur proof-size and verify-time
Prover changes can trade prove speed against proof size or verification
cost, so Phase 2 now serializes each fresh proof (proof-size, bytes) and
verifies it (verify-time; a verification failure is reported loudly and
drops only that measure). The full-closure path rebuilds the Array-G
claim from proveAddrWithEnv's serialized claim bytes — verify_claim's
input is the 32-G blake3 digest of those bytes, the same recipe as
`ix verify`.
Both measures flow through the neutral JSON into the PR compare table
(bench.py aiur prove metrics + byte/second unit mapping) and onto
bencher (verify-time 10% upper, proof-size 5% upper).
Measured: Nat.add_comm proves in 1.63s, verifies in 0.19s, 33.4 MB proof.
* feat(ci): env-sharded zisk execute via ix profile → ix shard manifests
The constants that OOM as single full-closure leaves (extract_append
proofs, the instRxcHasSize_eq family, …) are only measurable under env
sharding — their checks fit in one manifest shard each, with deps checked
in other shards (docs/zisk-cycle-cost-model.md, finding 4). Wire the
existing offline partitioner into CI instead of any per-constant
sharding:
- compile job: after the compile benchmark, `ix profile <Env>.ixe` →
`ix shard --max-ram 120` for InitStd/Mathlib; the `.ixes` manifest is
cached next to the `.ixe` (every restore of that key lists the same
paths — actions/cache versions entries by path list).
- zisk-host: `--shard-plan --execute --json` now writes one env-level
row — total cycles, shards, max-shard-cycles, execute-time,
throughput, execute-peak-rss, and a per-shard `shard-cycles`
breakdown — keyed by the new `--json-name` (default: manifest stem).
- run.sh: the zkVM guest-run dance (setsid + RAM watchdog + OOM
classification + shm sweep + merge) is factored into one `zkvm_run`
helper; when a `.ixes` sits next to the `.ixe` (bench-main only — the
\!benchmark PR path has none) the zisk branch appends the env-sharded
run after the per-constant loop.
- bench.py bmf: nested-object flattening generalized — `phases` →
`phase:<span>` as before, any other dict (e.g. `shard-cycles`) →
`<key>:<sub>` — so per-shard cycles land on bencher as un-thresholded
measures while the thresholded aggregates (cycles, shards,
max-shard-cycles) do the alerting.
zkvm job timeout 60 → 150 min: the whole-env run (own 60m cap inside
run.sh) rides on top of the per-constant loop.
* feat(ci): fill partial bencher misses from a targeted base run
fetch-main previously treated main.json as all-or-nothing: any name
bencher lacked at the base SHA (typically constants the PR itself adds
to Vectors.csv) silently rendered n/a. It now writes the uncovered
subset to --missing-out and still exits 0; bench-pr runs the base
checkout on JUST those names and merges under bencher's rows (bencher
wins overlaps — it is the canonical main side), so a brand-new constant
gets a real main-vs-PR delta on its first \!benchmark. The full-set base
fallback (exit 3, SHA not ingested) is unchanged.
* feat(ci): PR side cuts its own zisk shard manifest
A PR can change the kernel's cost profile, so the env-sharded zisk run
must not inherit main's partition. run.sh now cuts the manifest in-place
(ix profile → ix shard) whenever one isn't already sitting next to the
.ixe — the profiler counts heartbeats rather than wall time, so an
unchanged tree re-partitions deterministically and per-shard comparisons
stay meaningful. bench-main's compile-job manifest keeps pre-empting the
generation on the main side; the \!benchmark PR side profiles its own
tree (manifest cached per head SHA under bench-pr-ixes-*). The base
fallback reuses bench-main's cached manifest and pays the env-sharded
run only on a full bencher miss — a partial miss means bencher already
holds main's env row (ZISK_ENV_SHARD=0 skips it).
bench-pr benchmark timeout 120 → 180 min for the zisk cell's worst case
(per-constant loop + profile + the env execute's own 60m cap).
* feat(ci): per-shard execute-time and peak RAM in the zisk env row
The shard breakdown carried cycles only. Each shard now also records its
guest execute time (SDK-reported) and its RAM high-water — the texray
sampler's peak is reset before every shard, so the windows are
independent and the env row's execute-peak-rss becomes their max (the
run's execution-phase high-water; setup RAM no longer counted). Uploaded
as shard-time:<k> / shard-peak-rss:<k> alongside shard-cycles:<k>, all
un-thresholded like phase:<span>.
No prove-side equivalent yet: zisk proving isn't wired up in CI at all
(needs a GPU runner), so there is no prove-time for any zisk row.
* feat(ix): compile --consts seed selection + `ix shard extract` subcommand
Two ways to get a closure-only `.ixe` for one constant:
- `ix compile <file.lean> --consts <n1,n2,…>` (+ --consts-file): seed the
compile by exact constant name instead of the whole import env, with
transitive deps via the existing collectDeps — same names vocabulary as
`ix check --consts`. Mutually exclusive with --module.
- `ix shard extract <env.ixe> --consts <n1,n2,…> --out <sub.ixe>`: the
sharding pipeline's scoping step — cut the closure out of an EXISTING
env without recompiling from source. The output carries the closure's
genuine constant bytes, blobs, and reducibility hints (build_sub_env,
now shared via sub_env_of), plus a name→address entry per closure
constant so `--consts`-style tools still resolve. Metadata is dropped
(real ConstantMeta references name addresses throughout its tree and
would need the full hash-consed name index) — extracted envs serve the
anon pipeline; meta-mode tools need the source env. A mutual-block
member extracts its whole block.
Verified against a fresh initStd.ixe: both forms produce envs whose
bench-typecheck fft-cost is bit-identical to the full-env run
(content addressing at work), and extract → ix profile → ix shard
composes cleanly (Int8.instRxcHasSize_eq: 2.1 MB closure env,
16.08e9 steps → 11 shards at the 120 GiB cap).
* feat(ci): closure-sharded zisk execute for heavy primaries
Replaces the whole-env sharded run (wrong scope: all of InitStd is
1.94e12 steps / 1263 shards, and its biggest atomic block is INFEASIBLE
under the cap) with per-constant closure sharding through the canonical
pipeline. For each heavy-tier primary, run.sh runs `ix shard extract`
(closure-only env, no recompile) → `ix profile` → `ix shard --max-ram
120`, then one `zisk-host --shard-plan --execute` run executes the
shards sequentially — the constant's row carries totals plus the
per-shard shard-{cycles,time,peak-rss}:<k> breakdown, uploaded to
bencher like every other measure. Cheap primaries keep the single-leaf
--consts run.
- run.sh: cut_closure_shards (also exposed as the `cutshards` backend so
bench-main's compile job pre-cuts through the same code path) +
heavy-tier dispatch in the zisk loop (ZISK_HEAVY_NAMES). A constant
whose partition still can't fit (atomic mutual block over the cap)
OOMs under the RAM watchdog: honest OOM row, remaining shards skipped,
loop proceeds to the next constant. Cutting failures fall back to the
single-leaf run.
- bench.py manifest --heavy-out: the selected heavy-tier names, from
Vectors.csv's tier column.
- bench-main: the compile job pre-cuts zkshards-<Bench>/ next to the
fresh .ixe (it has ix + the toolchain; the zkvm job stays Lean-free)
and ships it to the zkvm job in the sha-keyed bench-ixe-* cache entry.
- bench-pr: the PR side cuts its own artifacts fresh every run (cheap —
seconds per closure — and a PR can change the cost profile; profiling
counts heartbeats, so an unchanged tree re-partitions
deterministically); the base fallback reuses bench-main's pre-cut dir.
* feat(bench): reject typecheck failures loudly — fail fast, ❌ row, red job
A constant the kernel rejects is a correctness regression, not a
benchmark datum. End to end:
- zisk-host: every sharded loop (shard-plan execute + prove, whole-env
execute + leaf prove) bails on the FIRST failing shard via the shared
reject_failures helper — mirroring the OOM kill, which also cancels
the constant's remaining shards — instead of accumulating failures
across the full manifest. sp1 and the single-leaf paths already bailed
immediately.
- run.sh: a zkVM failure whose log carries the host's "kernel typecheck
produced" abort records the neutral `{"failed": true}` sentinel (an
::error:: annotation, not a silent drop); ooc does the same when
##check## reports failures. bench-typecheck marks Phase-1 check errors
failed and skips them in Phase 2. Failure warnings now print the log's
head AND tail (the host's abort lands at the end of a mid-manifest
log).
- bench.py compare: `failed` renders ❌ cells (outranking OOM) plus a
bold "FAILED TO TYPECHECK on the <side> side" note under the table;
bmf strips the sentinel so rejected rows never reach bencher.
- workflows: prove/zkvm/ooc jobs (bench-main) and the benchmark cell
(bench-pr) exit nonzero when the neutral JSON carries a failed row —
AFTER the clean rows upload / the table posts, so the red X lands on
the commit/PR without losing the report.
* test(ci): trigger bench-main on branch pushes (TEMPORARY)
Drop this commit before merging. The zkVM build gate needs no branch
trigger — it lives in ci.yml now and runs on pull_request.
* feat(bench): ix bench orchestrator + neutral row contract; retire run.sh/bench.py
One orchestrator, `ix bench`, now runs every benchmark cell locally and in
CI, over a single tool contract with no output scraping:
- crates/bench (ix-bench) + Ix/Benchmark/Neutral.lean: the neutral rows
contract — { name: { status: ok|rejected|oom, ...metrics } }, flushed per
name, with typed exit codes (0 ok / 2 usage / 3 kernel rejection). Hosts'
duplicated helpers (write_json_entry, collect_consts, peak_rss_bytes)
move here.
- zisk-host/sp1-host: rejection writes the row (status: rejected) and exits
3 instead of an error string the harness had to grep.
- ix check-rs --json: whole-env row, or per-name independently-timed
closure rows (env loaded once) via an optional json path on the existing
rs_kernel_check_anon_consts extern; ##check## markers removed. The
triplicated env-load/name-resolution prefix in the FFI is now one loader.
- ix compile --json: compile row; ##benchmark## marker removed. The
displayed-name fallback no longer rescans the env per missing name.
- bench-typecheck: status rows + exit 3; per-constant RSS windows (sampler
reset per name) via a new texray reset binding.
- ix bench run/compare/bmf/fetch-main/comment/matrix (Lean): manifest from
Vectors.csv, spawn under .github/scripts/watchdog.sh (TERM→grace→KILL
tree-RSS sidecar), resume loop marking a killed constant's row oom and
continuing, zisk heavy-tier closure sharding, empty-rows-is-red gate,
local baselines under .bench/ so a bare rerun compares against the
previous run. compare renders the same Markdown table locally and in CI;
bmf drops non-ok rows so rejected/OOM constants never reach bencher;
fetch-main keeps the newest report at a SHA (was oldest-wins).
- Benchmarks/bench-config.json: single registry (env slugs/modules,
backends, testbeds, modes). Workflow matrices are generated from it
(ix bench matrix), the \!benchmark parser reads it, thresholds-reset
derives its workload lists from it.
- Workflows: every measurement step is one `ix bench run` + `ix bench bmf`;
the four copy-pasted jq typecheck gates are gone (exit codes redden the
step); run.sh deleted; bench.py reduced to the pre-build comment parser.
bench-pr's base side runs only the names bencher lacked (--names-file).
- No per-constant timeouts: job-level timeout-minutes is the only clock.
zisk-host/sp1-host compile is validated by ci.yml's zkvm build gates (their
toolchains aren't available locally).
* test(ci): TEMPORARY triggers to exercise the bench workflows from this branch
Revert before merge (every hunk is marked TEMPORARY):
- bench-main.yml runs on pushes to sb/ci-benchmarks, not just main.
- bench-pr.yml also runs on pull_request (head-ref gated to this branch):
a push to the branch's open PR fires `synchronize`, whose payload carries
the base/head SHAs and PR number that issue_comment needs an action to
look up. pull_request runs use a fixed cheap command (`\!benchmark ooc
compile`) so every push exercises fetch-main → run → compare → comment
end to end and posts the table on the PR.
* refactor(bench): drop the "neutral" vocabulary for the results format
"Neutral" described what the format isn't (backend-specific) rather than
what it is. The shared per-constant results file is now just the
"benchmark results JSON" / "results rows", and the Lean module moves
accordingly: Ix/Benchmark/Neutral.lean → Ix/Benchmark/Results.lean
(namespace Ix.Benchmark.Results). Comments, CLI help text, and docs
updated to match; no behavioral change.
* fix(ci): isolate the App token from PR-derived code in bench-pr
CodeQL flagged the comment job (untrusted checkout TOCTOU + untrusted
code execution in a privileged issue_comment workflow): it checked out
the PR head and ran the PR-built `ix bench comment` in the same job that
later mints the GitHub App token, so a malicious commit — including one
force-pushed after the \!benchmark authorization — could hijack the job
and reach the token.
Split it: an unprivileged `assemble` job (contents: read, no secrets)
checks out the PR and runs `ix bench comment`, uploading the finished
body as an artifact; the `comment` job keeps the token but now performs
no checkout and runs no repo-derived code — artifact download, token
mint, post. Untrusted checkouts in the build/benchmark/assemble jobs
also stop persisting the workflow token in .git.
* fix(ci): passthrough-env step failed on every cell (heredoc terminator)
The step interpolated the passthrough lines into a quoted heredoc inside
a YAML block scalar: the indentation put the PTENV terminator off column
0, so bash never found it, swallowed the stray lines, and the loop's
final [ -n ] test made the step exit 1 — on every cell, since the
passthrough is usually empty.
Deliver the lines via an env var and filter blanks with sed (exit 0
either way). This also removes inline ${{ }} interpolation from the
script body.
* feat(bench): announce each constant before its execute/prove
A watchdog kill or OOM mid-prove left no way to tell which constant was
in flight — bench-typecheck printed a constant's line only after it
finished. Both phases now print a flushed
`[i/N] proving <name> (fft-cost=…)` line first, so the crash site is
always named in the log (and matches the row `ix bench run` marks oom).
* fix(bench): don't relabel deterministic tool failures as per-constant OOM
The first \!benchmark run on the transition PR rendered every main-side
ooc row as OOM: bencher had no base data, the fallback ran main's ix —
which predates --json — and each spawn died instantly with a usage
error. The resume loop read every death as a kill of the in-flight
constant, poisoning all 18 names one spawn at a time.
Only a killed tool (exit ≥ 128: watchdog TERM/KILL or the kernel OOM
killer) now implicates the in-flight constant; any other nonzero exit is
deterministic and aborts the remaining names loudly. compare gains the
matching one-side-empty note ("main produced no results — often a
CLI-incompatible base binary") instead of a silent all-n/a column.
* refactor(bench): one-line side-failure notes in the compare table
The two-sentence diagnosis repeated per failing cell was noise; the
workflow logs carry the why.
* feat(bench): track peak RSS on the compile cell
Every other backend reports its RAM high-water; compile didn't only
because the old marker line never carried one. Window the tree-RSS
sampler around the serialize step (the loaded Lean env stays in the
baseline — RSS is absolute) and add peak-rss to the compile metrics.
* refactor(bench): render file-size as env-size in the compare table
The JSON key / bencher measure slug stays file-size (renaming would
orphan its threshold and history; bencher plots it as "Environment
Size") — only the table column label changes.
* refactor(bench): cutshards backend → `ix bench shard` subcommand
It measures nothing and emits no rows, so modeling it as a backend
forced a dummy registry entry (enabled: false, no testbed) into
bench-config.json. As a sibling of `run` the pseudo-entry disappears and
the name reads as what it does.
* feat(bench): execute-side throughput + surface both Aiur RAM peaks
The execute and prove RAM high-waters were already measured in separate
sampler windows (execute-peak-rss before any proving allocations,
peak-rss per prove), but the prove table only displayed the prove peak —
execute-peak-rss now joins the prove-mode columns. bench-typecheck also
records execute-throughput (closure constants/sec over Phase 1, the
witness-generation analog of the proving throughput), rendered
higher-is-better like its prove-side counterpart.
* refactor(bench): drop the compile mode - the compile backend runs as execute
Three mode tokens for two real behaviors: only aiur distinguishes
prove/execute, so a third mode existing solely to label the compile
backend's single behavior was registry noise. Its metrics key and
default_mode move to execute; cell labels/baselines become
compile-<env>-execute.
* refactor(bench): rename the prove-phase peak to prove-peak-rss
With execute-peak-rss now beside it in the prove table, a bare peak-rss
was ambiguous. The rename covers everywhere the value is a prove-phase
high-water: bench-typecheck rows, both zkVM hosts' prove paths, and the
aiur prove columns. ooc and compile keep plain peak-rss — their single
phase leaves nothing to disambiguate. Fresh bencher measure; the old
peak-rss series on the aiur testbed is orphaned (pipeline is new, no
meaningful history lost).
* refactor(bench): bare peak-rss everywhere, phases separated by testbed
Revert the prove-peak-rss/execute-peak-rss/execute-throughput naming:
metric names stay simple and phase scoping moves to the storage layer.
The aiur backend's two modes become two cells on their own bencher
testbeds (aiur-execute-* / aiur-prove-*, replacing aiur-check-*): an
execute row carries the Phase-1 peak-rss and constants/sec throughput, a
prove row the prover's peak and constants/prove-sec — shared names, no
collision, because the modes never share a row or a testbed. bench-main
gains the aiur execute cell (mode joins the matrix); bench-config
testbeds may now be per-mode objects (fetch-main and the
thresholds-reset jq handle both shapes). zisk/sp1 rows return to bare
peak-rss, and throughput's cross-backend unit reuse stays as is.
Also: integer columns render with thousands separators (105,492).
* feat(bench): aiur execute-only is local-only; CI uploads the prove run
The prove run simulates the real workload and measures Phase 1
(execute-time, fft-cost) inside the same process en route, so a separate
CI execute cell added runtime without adding signal. bench-main's aiur
job is back to a single prove cell per env (testbed/workload
aiur-prove); the standalone-execute testbed and per-mode testbed objects
are gone (config testbeds are plain strings again); the \!benchmark
`execute` token is removed from the grammar. `ix bench run --backend
aiur --mode execute` remains as a fast local dev loop with .bench/
baselines — it just never reaches bencher or the PR comment.
* feat(bench): restore the \!benchmark execute token
`\!benchmark aiur execute` runs the Phase-1-only cell on a PR again. PR
cells never upload to bencher, so the only correctness wrinkle is the
main side: bencher stores each backend's DEFAULT mode only, and the
shared measure names (peak-rss, throughput) mean that mode's phase —
fetch-main now exits 3 for any non-default mode, so an execute cell's
main side is always measured fresh on the base checkout instead of
misreading prove-phase numbers as execute-phase ones.
* feat(bench): bench-main runs aiur execute and prove as separate cells
Both modes upload to their own testbeds (aiur-execute-* / aiur-prove-*),
so a \!benchmark aiur cell of either kind always finds a cached main-side
baseline on bencher — no base-checkout fallback for the execute mode
(the previous non-default-mode guard in fetch-main is gone; per-mode
testbed objects return to the config, and the thresholds-reset jq
handles both shapes again). Costs one extra Phase-1 run per env per main
push; measure names stay bare, phase-scoped by the cell.
* fix(ci): concise matrix job names
Without an explicit name, GitHub appends every matrix value to the job
title — the PR benchmark cell showed backend, env, slug, mode, runner,
AND the label (which alone is the cell id). Name the matrix jobs from
their cell coordinates: <backend>-<env>[-<mode>].
* refactor(bench): aiur testbeds keep the subject word — aiur-check-{prove,execute}
The suite's testbeds name what they measure (zisk-check, ooc-check);
aiur-prove/aiur-execute dropped the subject. Both cells benchmark the
kernel typecheck — prove/execute are modes of it — so the testbeds are
now aiur-check-prove-x64-32x / aiur-check-execute-x64-32x (workloads
aiur-check-prove / aiur-check-execute).
History migration (before the next push of this branch): rename bencher
testbed aiur-typecheck-x64-32x -> aiur-check-prove-x64-32x, and copy the
reset tag: bencher-thresholds-reset-aiur -> the same commit tagged as
bencher-thresholds-reset-aiur-check-prove.
* refactor(bench): drop the BENCH_TIER PR knob; render peak-rss as peak-ram
BENCH_TIER was a four-hop plumbing chain (parse → output → env → --tier)
whose default is a no-op: the tier column's real consumers — zisk's
heavy-shard routing and the prove --full cheap default — read
Vectors.csv inside `ix bench run`, which keeps --tier for local use.
An unknown BENCH_TIER= line in a comment now just falls off the
allowlist. Vectors.csv's header also catches up with the ix bench era.
peak-rss renders as peak-ram in compare tables (display only, like
env-size — the bencher measure slug is unchanged).
* refactor(bench): one env spelling — InitStd everywhere
Collapse the env-key/slug pair (initStd/InitStd) inherited from run.sh's
benv/benv_cc split. The TitleCase name is now the single identifier: the
registry key, the \!benchmark token (matched case-insensitively), the
`ix bench run --env` value, the `<env>.ixe` filename, the zkshards-<env>
dir, the cache-key suffix, the cell label, and the env-keyed bencher
benchmark name. The registry drops the slug field, matrix cells drop the
slug member, EnvInfo loses its slug, and Vectors.csv's env column is
TitleCase. Cache paths change spelling but keys are SHA-scoped, so no
migration.
* fix(bench): satisfy clippy without allows
cast_precision_loss on the per-name throughput: convert the closure
count through u32 (exact in f64) instead of a raw usize cast. The
exit-code constants become u8 — ExitCode::from is their only numeric
consumer, which also drops the hosts' `as u8` casts.
* feat(bench): print throughput + peak RAM on bench-typecheck's log lines
The rows always carried them; the per-constant console lines only
showed constants/fft-cost/execute (and the prove line omitted its
peak), so a reader scanning the CI log saw neither.
* refactor(bench): shared instrumentation for aiur execute metrics
Supersedes the ad-hoc per-line arithmetic from the previous commit:
- The standalone execute FFI entries (dispatch_execute /
rs_aiur_toplevel_execute_ixvm) now carry the same aiur/execute_ixvm
span the prove pipeline emits, so Phase-1 duration and RAM Δ/peak
stream through the one texray channel — and land in <json>.spans —
instead of being computed per benchmark.
- bench-typecheck installs the texray subscriber before Phase 1 (bare
--texray previously deferred it to the prove phase).
- The per-constant console line formats throughput via the benchmark
framework's Throughput.formatRate; the hand-rolled rate and GiB math
is gone.
* feat(bench): one process per constant; span timings become phase:* measures
Per-constant backends (aiur, zkVM) now spawn one tool process per
constant, like the original run.sh granularity: a kill costs exactly
that constant (row marked oom, keeping whatever the tool flushed) and
the resume loop's first-missing-row inference is deleted. The payoff is
span attribution for free — each spawn truncates <out>.spans at startup,
so after it exits the file IS that constant's window; ix bench run folds
it into the row as flat phase:<span> fields (aiur tracing spans and the
zkVM hosts' record_manual entries alike, no tool changes).
The flat keys pass through bmf untouched as independent bencher measures
(witness gen, stage commits, quotient, ... each get a trend line) and
come back from fetch-main in the same shape; compare renders them as a
collapsible per-constant drill-down after the main table.
bench-typecheck switches from whole-file rewrites to the shared
merge-style row writes (Results.writeEntry) so per-constant processes
can share one results file. ooc keeps its single multi-name process: the
check-rs rows mode already attributes per name with the env loaded once,
and out-of-circuit checks don't approach the RAM ceiling.
* feat(bench): nest each constant's phase table in its own drop-down
One collapsed drill-down per cell, one collapsible entry per constant
inside it — 17 constants no longer expand into one wall of tables.
* feat(bench): per-constant phase drop-downs directly under the main table
The main table keeps every constant's high-level row; each constant
with phase data gets its own top-level collapsed mini-table, opened
individually — no outer wrapper to expand first.
* fix(bench): verified review findings — panic strategy, gate completeness, atomic rows
1. zisk host workspace drops panic="abort": with it, every deterministic
panic (e.g. a missing .ixe expect) exits SIGABRT=134, which
runPerConstant reads as an OOM kill — a broken host became a green
cell of all-oom rows with an empty upload. Unwinding panics exit 101
and hit the loud abort path; SIGABRT stays reserved for real
allocation-failure OOMs. (sp1-host already unwound; guests keep their
own profiles in their excluded workspaces.)
2. The gate now checks COMPLETENESS, not just emptiness: every selected
name (plus the env-keyed row for ooc/compile) owes exactly one row,
so an aborted loop, a killed ooc batch, or a dropped whole-env check
exits 1 instead of shipping a quietly partial green cell.
3. Row writes are atomic (temp + rename) on both sides — Lean writeEntry
(markOom/mergeSpans now route through it) and Rust write_json_entry.
A KILL mid-write previously truncated the shared accumulator, which
the tolerant readers silently reset to {}, losing every prior row.
4. A watchdog kill during teardown (row already carries the mode's
completion metric, e.g. prove-time — the prover releasing tens of GB
right after the final write) no longer relabels the finished row oom
and out of the upload. Plus dead nested-phases vocabulary: bmf's
phases special case, the row-shape docs, and the stale drill-down
bullet all catch up with the flat phase:<span> keys.
* chore(zisk): drop the panic-strategy comment
* fix(ci): create-github-app-token deprecated app-id in favor of client-id
The input accepts the numeric App ID as well (the JWT issuer claim
takes either), so the TOKEN_APP_ID secret is unchanged.
* refactor(bench): registry as Lean code — bench-config.json and bench.py deleted
The JSON registry existed to share env/backend data across three
runtimes: ix bench (Lean), the pre-build Python comment parser, and the
thresholds-reset jq. Eliminate the other two consumers and the file has
no reason to exist:
- The registry is now typed Lean data (envSpecs/backendSpecs in
Ix/Cli/BenchCmd.lean) — one language, one owner, and the getObjVal?
chains in run/shard/compare/fetch-main/matrix collapse into struct
lookups. The --config flags disappear.
- \!benchmark parsing moves into `ix bench parse` (COMMENT_BODY →
GITHUB_OUTPUT, same allowlist grammar), run at the end of bench-pr's
build job right after the ix binary exists; the setup job keeps only
the authorization gate and SHA resolution, and the matrix/config
outputs move to the build job. The last Python is gone.
- bencher-thresholds-reset keeps static workload lists with a sync note
pointing at backendSpecs — it runs on cheap runners with no built ix,
and its dispatch options were already forced static by GitHub.
* refactor(bench): local-first CLI — parse previews, comment becomes report
The ix bench surface should be generic CLI infra that CI merely calls,
not CI infra that happens to be a CLI:
- `parse` takes the command via --comment (a local dry-run preview of
which cells a \!benchmark schedules), falling back to the COMMENT_BODY
env var; the Actions-format machine outputs are written only when
$GITHUB_OUTPUT is set instead of spilling to stdout.
- `comment` → `report`: assemble per-cell tables into one Markdown
report, readable locally with zero flags; the commit/logs links only
render when the PR workflow passes --head/--repo-url/--run-id, and
--out is optional (always printed).
* refactor(bench): group the CI adapters under ix bench ci
parse and matrix exist for the workflows; the top-level listing now
reads as the local tools plus one clearly-labeled ci namespace.
* docs(bench): full accuracy pass on the benchmarking docs
- gate guarantee stated correctly: every selected name owes a row (not
just non-empty), so a partial cell can't be green
- bench-pr shape caught up with the parse move (setup only authorizes
and resolves SHAs; build ends with ix bench ci parse) and the
assemble/comment privilege split
- watchdog section covers the teardown-kill exception and the
single-process ooc/compile cells
- grammar adds the sp1 token and enumerates the passthrough allowlist
- local usage gains a single-constant aiur walkthrough and the
fetch-main flow for comparing a local run against main's bencher data
- README benchmark section links here instead of just the bencher plots
* refactor(bench): CI data out of the generic registry
benchRunner was a runs-on matrix field only ix bench ci parse consumes —
it moves next to the ci adapters as ciRunner. The 120 GB default ceiling
was really "the CI runner's 128 GB minus headroom" posing as a universal
constant; defaultCeilingGb now derives from the machine's own RAM
(/proc/meminfo MemTotal minus 8 GiB, floor 8, conservative 16 when
unreadable), so CI lands where it always did and a workstation gets a
ceiling that actually protects it.
* fix(bench): baselines move to the framework's .lake/benches root
.bench/ duplicated an existing convention: Ix.Benchmark already writes
all benchmark output under BENCH_OUTPUT_DIR (default .lake/benches).
ix bench saveBaseline and compare now share that root — one output
convention, and baselines stop polluting git status.
* fix(bench): watchdog must never lose the race to the runner
The bitblast prove OOM took the whole job down ("The operation was
canceled"): tree-RSS was 7 GB past the 120 GB ceiling before the 3s
sampler saw it, and the fixed 10s TERM grace let the prover keep
allocating until the VM thrashed, the runner agent missed its heartbeat,
and GitHub canceled the job before any kill landed.
- sample every 1s instead of 3s (the breach is seen ~GBs earlier)
- the grace only continues while the tree is BELOW the ceiling: still
at/above it after TERM means still allocating -> KILL immediately.
Rows are flushed as tools go, so nothing of value needs the grace.
- default ceiling headroom widens to MemTotal minus 12 GiB (the 128 GiB
runner lands at 116): it must absorb ~two sampling periods of
allocation past the ceiling plus the OS and runner agent.
Verified live: a 2 GB allocation under a 1 GB ceiling gets TERM'd and
exits 143 within a second.
* fix(ci): derive the benched-env gate from the registry
The compile job's shard-cut and cache-save conditionals hand-copied
'InitStd || Mathlib'; a step now asks the in-job ix (ci matrix --kind
envs) whether matrix.env is benched, so adding a benched env is a
registry-only change.
* fix(bench): per-shard data uploads as benchmarks, not one measure per index
toBmf flattened nested shard breakdowns to shard-cycles:0,
shard-cycles:1, ... — a new bencher MEASURE per shard index, spamming
the measure list with dozens of dynamically-named entries. Multiplicity
belongs in the benchmark-name dimension: each shard now uploads as
<name>/shard-<idx> sharing the parent row's measure slugs (cycles,
execute-time, peak-rss). The rows JSON keeps its nested shape; only the
bencher projection changes.
* fix(ci): threshold the compile cell's peak-rss
peak-rss joined the compile metrics but never its thresholds list, so
bencher warned 'No Threshold found' and the measure could never alert.
Same 10% upper bound as the other cells' peak-rss.
* fix(bench): enforce the RAM ceiling with RLIMIT_DATA, sampler as backstop
The aiur prove OOM still took the runner down: tree-RSS was 13 GB past
the ceiling at the FIRST sample after the breach — the prover's commit
phases allocate multiple GB/s across 32 threads, faster than any
sampling cadence can react. Sampling-based kills fundamentally lose
that race; by the time the sampler sees the spike the VM is thrashing
and GitHub cancels the job before the TERM lands.
watchdog.sh now sets RLIMIT_DATA to the ceiling on the spawned command:
the allocation that would cross the line fails inside the process, and
Rust's handle_alloc_error / Lean's OOM panic abort on the spot (SIGABRT
= 134 ≥ 128 → oom row) with zero overshoot. The tree-RSS sampler stays
as the backstop for what a per-process limit can't see: the sum across
Zisk's ASM microservice tree.
Verified: a 2 GB allocation under a 1 GB ceiling now fails in-process
instantly (no TERM path), normal commands unaffected.
* fix(bench): never upload an empty BMF report
A cell whose rows all end oom/rejected — or that failed before
producing rows — left bmf writing {} and the \!cancelled() upload step
sending it to bencher, which rejects it as 'No benchmarks found'.
bmf now exits 1 when zero benchmarks survive the non-ok filter, and the
bencher-track steps gate on the bmf step's outcome as well as
\!cancelled(): clean rows still upload past an exit-3 run, but an empty
report skips the upload instead of failing it.
* fix(bench): absolute watchdog path; exec failure is not an OOM
The zisk cell's empty bencher upload traced to a broken spawn, not a
benchmark: the hosts run with the zisk/ workspace as cwd, where the
repo-relative ./.github/scripts/watchdog.sh fails to exec. Lean reports
that as exit 255, which runPerConstant read as a kill — both constants
got fake oom rows, the completeness gate saw every row present and
passed, and bmf stripped the non-ok rows down to {}.
The watchdog path is now resolved to an absolute path before any spawn,
and exit 255 (never a signal death; our kills are 134/137/143) aborts
the cell loudly instead of minting oom rows.
* fix(ci): say where the main side actually came from in the table title
The fetch-main exit-3 case wrote the literal 'source=ran', rendering as
'main from: ran'. All three cases now name the source and base SHA:
'bencher @ <sha7>', 'bencher @ <sha7> + base run (N new)', or
'base run @ <sha7> (not on bencher)'.
* fix(bench): only annotate the mode for multi-mode backends in the summary
'ooc=execute compile=execute' implied a choice that doesn't exist;
single-mode backends now print bare, aiur keeps aiur=prove/execute.
* fix(bench): drop the mode from single-mode cells' table titles
Same rule as the config summary: 'compile · InitStd · execute' names a
mode nobody chose; aiur keeps its prove/execute segment.
* fix(bench): fixed 120 GB default ceiling; RLIMIT_DATA stays everywhere
The Mathlib compile hit the MemTotal-derived 111 GB ceiling with room
to spare in physical RAM: RLIMIT_DATA caps virtual data mappings, and
Lean's allocator reserves well beyond true RSS, so the derived value
was too tight for the biggest legitimate workload. Rather than
per-backend enforcement modes, keep one simple rule: the rlimit works,
set it to a flat 120 GB (what the sampler ceiling always was) and let
--ceiling-gb override on smaller machines.
* feat(bench): cgroup memory.max as the watchdog's primary enforcement
The kernel primitive both prior layers approximated: memory.max caps
the tree's RESIDENT memory and (with memory.oom.group) OOM-kills the
whole group atomically at the ceiling, exiting 137 — no sampling race
for the prover's GB/s bursts, no virtual-memory false trips for Lean's
allocator slack (only actual pages are charged), and Zisk's ASM
microservices sum into the same budget. Used when cgroup v2 and
passwordless sudo are available (the CI runners); otherwise the
RLIMIT_DATA + tree-RSS-sampler fallback remains for local runs, with a
log line naming the active mode.
* feat(bench): cgroup-only watchdog — no fallback, fail loudly
The RLIMIT_DATA + tree-RSS-sampler fallback is gone: a run whose
ceiling cannot be enforced is not a benchmark run. watchdog.sh now
requires cgroup v2 + passwordless sudo and exits 2 with a plain reason
otherwise; ix bench run likewise hard-fails when the watchdog script is
missing instead of running unguarded. The sampler machinery
(tree_pids/tree_rss_kb/TERM-grace loop) is deleted with it.
* fix(bench): sampler-only watchdog with adaptive cadence
Revert the cgroup mode (and the earlier RLIMIT_DATA layer): back to the
plain tree-RSS sampler, sudo-free and identical everywhere. The burst
problem is handled by cadence instead of a kernel cap: sampling drops
from ~1s to 0.2s once the tree is within 20 GB of the ceiling (100 GB
at the default 120), and the post-TERM grace re-checks every 0.2s,
KILLing immediately while the tree is still at the ceiling. Worst-case
overshoot shrinks from GB-per-second x seconds to x ~0.4s.
ix bench run still hard-fails when the watchdog script is missing — an
unenforced ceiling is not a benchmark run.
* fix(bench): restore the RAM-derived default ceiling
The flat 120 was a leftover from the RLIMIT_DATA era (a VA cap needed
fixed slack above RSS); for the sampler it protects nothing on machines
with less RAM and leaves ~3 GB of headroom on the 123 GiB runner. Back
to MemTotal minus 12 GiB (runner: 111; 64 GiB workstation: 52), which
the adaptive fast-cadence zone sits under wherever the run happens.
* refactor(bench): zkvm testbeds gain the mode suffix (zisk-check-execute)
Same lesson aiur taught: shared measure names (peak-rss, throughput)
mean that mode's phase, so a future zisk/sp1 prove mode needs its own
testbed — and an unsuffixed zisk-check silently meaning "execute only"
is the asymmetry we just cleaned up for aiur. Renaming now rides the
merge's existing bencher migration (console rename + reset-all) instead
of paying a second cycle later.
The zkvm job derives testbed/workload from the cell's mode, so a prove
cell would land on zisk-check-prove-x64-32x with no workflow edits.
* feat(ci): bench-pr prepare stage — compile ea…
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes erroneous alerts for the bencher.dev benchmarks on main, which were due to a brittle threshold reset mechanism between Lean toolchain bumps. This PR instead sets a manual threshold reset action, which triggers either by a
!bencher-thresholds-reset <ix-compile|aiur|all>PR comment or a manualworkflow_dispatchaction after merge.These should be used whenever a new baseline is expected to be set by a PR, either from a performance improvement (e.g. lowering Aiur FFTs) or regression (e.g. more constants added to Mathlib on a toolchain bump). The baselines are split by workload, so changes to
ix-compileneed not affect the baseline foraiur. Currently all thresholds for a given workload are reset together, so any new metrics from the first few runs on a new baseline should be carefully reviewed for any performance changes.Future work: Add Zisk and SP1 benchmarks to bencher.dev and integrate with the new threshold/alert system.
Note
Before merge, we'll need to update the testbed for Ix compilation from
warp-ubuntu-x64-32xtoix-compile-x64-32xvia the bencher API/web console to ensure the history is preserved.