Skip to content

ci: Standardize benchmarks and input constants#467

Merged
samuelburnham merged 100 commits into
mainfrom
sb/ci-benchmarks
Jul 9, 2026
Merged

ci: Standardize benchmarks and input constants#467
samuelburnham merged 100 commits into
mainfrom
sb/ci-benchmarks

Conversation

@samuelburnham

@samuelburnham samuelburnham commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

CI benchmarking:

  • ix bench Lean CLI for comprehensive local and CI benchmarks of ix compilation and typechecking over multiple backends, against a curated set of constants. Provides comparative runs against local history, or current main (fetches cached bencher.dev results), and formats them in a Markdown table.
  • Updates bench-pr.yml to use this framework and print the Markdown table as a PR comment (see example comments below).
  • Updates bench-main.yml to fully bench all backends and upload them to bencher.dev, except for RISC-V proving for now due to GPU requirements. SP1 is also left as a TODO.
  • Now tracks per-phase span measurements from tracing-texray as first-class benchmark metrics, and uploads them to bencher.dev for regression testing and also direct PR comparison in the comment table with a collapsible drop-down view (not fully tested).
  • Adds a RAM watchdog via systemd-run cgroups to prevent an OOM constant from killing the runner and failing the workflow.
  • Moves the benchmark binaries onto AVX-512-compatible runner after testing that the Warpbuild 32 vCPU runner (AMD EPYC 9R45 in all my tests) has full AVX-512 support. This should provide a one-time speedup that more accurately tracks production performance.

Usage

Local benchmarks:

# Compare local runs
ix bench run --backend aiur --env InitStd --mode execute --consts Nat.add_comm --ixe initstd.ixe
ix bench compare --backend aiur --env InitStd --mode execute --consts Nat.add_comm
# Compare against main
ix bench fetch-main --sha $(git rev-parse origin/main) \
    --backend aiur --mode execute --consts Nat.add_comm --out main.json
ix bench compare --backend aiur --env InitStd --mode execute \
    --main main.json --pr .lake/benches/aiur-InitStd-execute.json

PR comparative benchmarks against main:

!benchmark [aiur] [zisk] [sp1] [ooc] [compile] | all  [execute]
# Optional env vars
BENCH_ENVS=InitStd,Mathlib
BENCH_FULL=1 # the env's full curated set (56 InitStd / 10 Mathlib consts) instead of the default primary subset (17 InitStd / 2 Mathlib)
BENCH_SHARD=1 # restrict to the multi-shard target constants
RUST_LOG=info

Successful runs:

Merge after argumentcomputer/tracing-texray#3

Note

Before merge:

  • Bencher console: rename aiur-typecheck-x64-32x → aiur-check-prove-x64-32x, zisk-check-x64-32x → zisk-check-execute-x64-32x; archive stale shard-cycles:N measures.
  • Delete the old threshold Git tags for aiur as the names have been updated

@samuelburnham
samuelburnham force-pushed the sb/ci-benchmarks branch 7 times, most recently from 07264b9 to f1ff88a Compare July 3, 2026 20:39
github-advanced-security[bot]
github-advanced-security AI found potential problems Jul 7, 2026
View reviewed changes
Comment thread .github/workflows/bench-pr.yml Fixed
Comment thread .github/workflows/bench-pr.yml Fixed
@argument-ci-bot

argument-ci-bot Bot commented Jul 7, 2026

Copy link
Copy Markdown

!benchmark — main vs b56201f

backends: ooc=execute compile=compile · envs: initStd · set: primary · tier: auto · shard: 0

No result tables were produced — see the workflow logs.

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 7, 2026

Copy link
Copy Markdown

!benchmark — main vs 70d60b8

backends: ooc=execute compile=compile · envs: initStd · set: primary · tier: auto · shard: 0

compile · initStd · compile — main from: bencher

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% file-size (main) file-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd n/a 4.222 s n/a n/a 24.99K n/a n/a 306.41 MiB n/a n/a 105492 n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · initStd · execute — main from: ran

constant throughput (main) throughput (PR) Δ% check-time (main) check-time (PR) Δ% peak-rss (main) peak-rss (PR) Δ%
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq OOM 6.86K n/a OOM 264.7 ms n/a OOM 1.16 GiB n/a
String.split OOM 6.71K n/a OOM 264.0 ms n/a OOM 971.84 MiB n/a
InitStd n/a 6.08K n/a n/a 14.644 s n/a n/a 1.48 GiB n/a
List.mergeSort OOM 5.56K n/a OOM 261.5 ms n/a OOM 802.59 MiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append OOM 5.09K n/a OOM 529.6 ms n/a OOM 998.39 MiB n/a
Char.ofOrdinal_le_of_le OOM 3.44K n/a OOM 773.9 ms n/a OOM 980.05 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq OOM 2.38K n/a OOM 764.8 ms n/a OOM 841.74 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq OOM 2.37K n/a OOM 764.8 ms n/a OOM 977.59 MiB n/a
Vector.append OOM 1.96K n/a OOM 254.4 ms n/a OOM 665.40 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq OOM 1.79K n/a OOM 1.015 s n/a OOM 853.80 MiB n/a
Nat.gcd_comm OOM 1.53K n/a OOM 254.2 ms n/a OOM 640.46 MiB n/a
Array.extract_append OOM 1.52K n/a OOM 1.017 s n/a OOM 1.04 GiB n/a
Vector.extract_append._proof_2 OOM 1.29K n/a OOM 1.012 s n/a OOM 916.29 MiB n/a
String.append OOM 1.21K n/a OOM 253.1 ms n/a OOM 1.01 GiB n/a
Int.gcd OOM 823.880 n/a OOM 252.5 ms n/a OOM 616.14 MiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual OOM 821.770 n/a OOM 6.895 s n/a OOM 1.73 GiB n/a
Nat.sub_le_of_le_add OOM 673.120 n/a OOM 252.6 ms n/a OOM 568.05 MiB n/a
Nat.add_comm OOM 166.670 n/a OOM 252.0 ms n/a OOM 457.39 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs 431ae38

backends: ooc=execute compile=compile · envs: initStd · set: primary · tier: auto · shard: 0

compile · initStd · compile — main from: bencher

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ% peak-rss (main) peak-rss (PR) Δ%
InitStd n/a 3.955 s n/a n/a 26.67K n/a n/a 306.41 MiB n/a n/a 105492 n/a n/a 10.67 GiB n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · initStd · execute — main from: ran

constant throughput (main) throughput (PR) Δ% check-time (main) check-time (PR) Δ% peak-rss (main) peak-rss (PR) Δ%
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 6.87K n/a n/a 264.4 ms n/a n/a 1.19 GiB n/a
String.split n/a 6.72K n/a n/a 263.8 ms n/a n/a 1.07 GiB n/a
InitStd n/a 6.41K n/a n/a 13.881 s n/a n/a 1.47 GiB n/a
List.mergeSort n/a 5.56K n/a n/a 261.7 ms n/a n/a 858.98 MiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 5.10K n/a n/a 528.9 ms n/a n/a 1.01 GiB n/a
Char.ofOrdinal_le_of_le n/a 3.44K n/a n/a 774.0 ms n/a n/a 1.10 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 2.38K n/a n/a 764.5 ms n/a n/a 880.31 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 2.38K n/a n/a 764.6 ms n/a n/a 815.45 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 2.37K n/a n/a 764.6 ms n/a n/a 979.52 MiB n/a
Vector.append n/a 1.95K n/a n/a 254.8 ms n/a n/a 667.94 MiB n/a
Nat.gcd_comm n/a 1.53K n/a n/a 254.9 ms n/a n/a 681.33 MiB n/a
Array.extract_append n/a 1.52K n/a n/a 1.017 s n/a n/a 1.01 GiB n/a
Vector.extract_append._proof_2 n/a 1.29K n/a n/a 1.012 s n/a n/a 1.07 GiB n/a
String.append n/a 1.21K n/a n/a 252.8 ms n/a n/a 965.88 MiB n/a
Int.gcd n/a 824.190 n/a n/a 252.4 ms n/a n/a 619.82 MiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 822.230 n/a n/a 6.891 s n/a n/a 1.72 GiB n/a
Nat.sub_le_of_le_add n/a 673.260 n/a n/a 252.5 ms n/a n/a 564.67 MiB n/a
Nat.add_comm n/a 166.640 n/a n/a 252.0 ms n/a n/a 451.35 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs 7d3388b

backends: ooc=execute compile=execute · envs: initStd · set: primary · tier: auto · shard: 0

compile · initStd · execute — main from: bencher

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ% peak-rss (main) peak-rss (PR) Δ%
InitStd n/a 4.352 s n/a n/a 24.24K n/a n/a 306.41 MiB n/a n/a 105,492 n/a n/a 10.59 GiB n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · initStd · execute — main from: ran

constant throughput (main) throughput (PR) Δ% check-time (main) check-time (PR) Δ% peak-rss (main) peak-rss (PR) Δ%
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 6.86K n/a n/a 264.6 ms n/a n/a 1.15 GiB n/a
String.split n/a 6.71K n/a n/a 263.9 ms n/a n/a 1.05 GiB n/a
InitStd n/a 6.41K n/a n/a 13.882 s n/a n/a 1.50 GiB n/a
List.mergeSort n/a 5.56K n/a n/a 261.4 ms n/a n/a 838.87 MiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 5.09K n/a n/a 529.5 ms n/a n/a 982.43 MiB n/a
Char.ofOrdinal_le_of_le n/a 3.44K n/a n/a 773.9 ms n/a n/a 1.06 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 2.38K n/a n/a 764.7 ms n/a n/a 917.39 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 2.38K n/a n/a 764.8 ms n/a n/a 812.00 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 2.37K n/a n/a 764.7 ms n/a n/a 1.01 GiB n/a
Vector.append n/a 1.96K n/a n/a 254.3 ms n/a n/a 659.75 MiB n/a
Nat.gcd_comm n/a 1.54K n/a n/a 253.9 ms n/a n/a 643.67 MiB n/a
Array.extract_append n/a 1.52K n/a n/a 1.017 s n/a n/a 920.13 MiB n/a
Vector.extract_append._proof_2 n/a 1.29K n/a n/a 1.012 s n/a n/a 978.00 MiB n/a
String.append n/a 1.21K n/a n/a 253.0 ms n/a n/a 1.02 GiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 853.640 n/a n/a 6.637 s n/a n/a 1.80 GiB n/a
Int.gcd n/a 824.010 n/a n/a 252.4 ms n/a n/a 612.75 MiB n/a
Nat.sub_le_of_le_add n/a 673.230 n/a n/a 252.5 ms n/a n/a 568.57 MiB n/a
Nat.add_comm n/a 166.670 n/a n/a 252.0 ms n/a n/a 467.85 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs 1103162

backends: ooc=execute compile=execute · envs: InitStd · set: primary · shard: 0

compile · InitStd · execute — main from: bencher

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd n/a 4.301 s n/a n/a 24.53K n/a n/a 306.41 MiB n/a n/a 105,492 n/a n/a 10.61 GiB n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · InitStd · execute — main from: ran

constant throughput (main) throughput (PR) Δ% check-time (main) check-time (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 6.86K n/a n/a 264.6 ms n/a n/a 1.33 GiB n/a
String.split n/a 6.71K n/a n/a 264.3 ms n/a n/a 1.12 GiB n/a
InitStd n/a 6.30K n/a n/a 14.129 s n/a n/a 1.50 GiB n/a
List.mergeSort n/a 5.56K n/a n/a 261.4 ms n/a n/a 931.07 MiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 5.09K n/a n/a 529.7 ms n/a n/a 1.02 GiB n/a
Char.ofOrdinal_le_of_le n/a 3.44K n/a n/a 773.7 ms n/a n/a 887.48 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 2.38K n/a n/a 765.2 ms n/a n/a 841.39 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 2.37K n/a n/a 764.7 ms n/a n/a 1.08 GiB n/a
Vector.append n/a 1.96K n/a n/a 254.4 ms n/a n/a 669.67 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 1.79K n/a n/a 1.015 s n/a n/a 914.25 MiB n/a
Nat.gcd_comm n/a 1.53K n/a n/a 255.3 ms n/a n/a 657.64 MiB n/a
Array.extract_append n/a 1.52K n/a n/a 1.017 s n/a n/a 1.16 GiB n/a
Vector.extract_append._proof_2 n/a 1.29K n/a n/a 1.012 s n/a n/a 1.11 GiB n/a
String.append n/a 1.21K n/a n/a 253.0 ms n/a n/a 1.08 GiB n/a
Int.gcd n/a 823.880 n/a n/a 252.5 ms n/a n/a 607.91 MiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 821.940 n/a n/a 6.893 s n/a n/a 1.64 GiB n/a
Nat.sub_le_of_le_add n/a 673.360 n/a n/a 252.5 ms n/a n/a 547.86 MiB n/a
Nat.add_comm n/a 166.540 n/a n/a 252.2 ms n/a n/a 435.36 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs b82aed8

backends: ooc=execute compile=execute · envs: InitStd · set: primary · shard: 0

compile · InitStd · execute — main from: bencher

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd n/a 3.947 s n/a n/a 26.73K n/a n/a 11.24 GiB n/a n/a 306.43 MiB n/a n/a 105,492 n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · InitStd · execute — main from: ran

constant check-time (main) check-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd n/a 10.412 s n/a n/a 8.55K n/a n/a 2.05 GiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 6.404 s n/a n/a 884.740 n/a n/a 1.91 GiB n/a
Array.extract_append n/a 1.017 s n/a n/a 1.52K n/a n/a 1.25 GiB n/a
Vector.extract_append._proof_2 n/a 1.013 s n/a n/a 1.29K n/a n/a 1.36 GiB n/a
Char.ofOrdinal_le_of_le n/a 775.5 ms n/a n/a 3.43K n/a n/a 1.10 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.19 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 765.5 ms n/a n/a 2.37K n/a n/a 1.09 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 765.5 ms n/a n/a 2.37K n/a n/a 1.15 GiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 531.6 ms n/a n/a 5.07K n/a n/a 1.16 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 266.5 ms n/a n/a 6.82K n/a n/a 1.38 GiB n/a
String.split n/a 264.7 ms n/a n/a 6.70K n/a n/a 1.19 GiB n/a
List.mergeSort n/a 262.3 ms n/a n/a 5.54K n/a n/a 998.22 MiB n/a
Nat.gcd_comm n/a 255.0 ms n/a n/a 1.53K n/a n/a 765.08 MiB n/a
Vector.append n/a 254.5 ms n/a n/a 1.96K n/a n/a 702.54 MiB n/a
Nat.sub_le_of_le_add n/a 253.2 ms n/a n/a 671.490 n/a n/a 601.42 MiB n/a
String.append n/a 253.0 ms n/a n/a 1.21K n/a n/a 1.01 GiB n/a
Int.gcd n/a 252.5 ms n/a n/a 823.710 n/a n/a 636.20 MiB n/a
Nat.add_comm n/a 251.9 ms n/a n/a 166.730 n/a n/a 484.27 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs 930ebb8

backends: ooc=execute compile=execute · envs: InitStd · set: primary · shard: 0

compile · InitStd · execute — main from: bencher

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd n/a 4.355 s n/a n/a 24.22K n/a n/a 11.14 GiB n/a n/a 306.43 MiB n/a n/a 105,492 n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · InitStd · execute — main from: ran

constant check-time (main) check-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd n/a 10.409 s n/a n/a 8.55K n/a n/a 2.03 GiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 6.151 s n/a n/a 921.220 n/a n/a 1.98 GiB n/a
Array.extract_append n/a 1.018 s n/a n/a 1.52K n/a n/a 1.23 GiB n/a
Vector.extract_append._proof_2 n/a 1.013 s n/a n/a 1.29K n/a n/a 1.36 GiB n/a
Char.ofOrdinal_le_of_le n/a 775.3 ms n/a n/a 3.43K n/a n/a 1.05 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 765.7 ms n/a n/a 2.37K n/a n/a 1.12 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 765.7 ms n/a n/a 2.37K n/a n/a 1.10 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.20 GiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 531.2 ms n/a n/a 5.08K n/a n/a 1.18 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 266.8 ms n/a n/a 6.81K n/a n/a 1.46 GiB n/a
String.split n/a 265.0 ms n/a n/a 6.69K n/a n/a 1.31 GiB n/a
List.mergeSort n/a 262.1 ms n/a n/a 5.55K n/a n/a 1013.36 MiB n/a
Nat.gcd_comm n/a 255.0 ms n/a n/a 1.53K n/a n/a 891.58 MiB n/a
Vector.append n/a 254.6 ms n/a n/a 1.96K n/a n/a 745.38 MiB n/a
String.append n/a 253.0 ms n/a n/a 1.21K n/a n/a 1.13 GiB n/a
Int.gcd n/a 252.5 ms n/a n/a 823.670 n/a n/a 762.65 MiB n/a
Nat.sub_le_of_le_add n/a 252.5 ms n/a n/a 673.360 n/a n/a 651.23 MiB n/a
Nat.add_comm n/a 252.2 ms n/a n/a 166.570 n/a n/a 508.57 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs d69aaee

backends: ooc=execute compile=execute · envs: InitStd · set: primary · shard: 0

compile · InitStd · execute — main from: bencher

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd n/a 4.231 s n/a n/a 24.93K n/a n/a 11.03 GiB n/a n/a 306.43 MiB n/a n/a 105,492 n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · InitStd · execute — main from: ran

constant check-time (main) check-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd n/a 10.159 s n/a n/a 8.76K n/a n/a 2.09 GiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 6.151 s n/a n/a 921.090 n/a n/a 2.04 GiB n/a
Array.extract_append n/a 1.018 s n/a n/a 1.52K n/a n/a 1.10 GiB n/a
Vector.extract_append._proof_2 n/a 1.013 s n/a n/a 1.29K n/a n/a 1.33 GiB n/a
Char.ofOrdinal_le_of_le n/a 775.1 ms n/a n/a 3.43K n/a n/a 1.16 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 765.5 ms n/a n/a 2.37K n/a n/a 939.29 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 765.4 ms n/a n/a 2.38K n/a n/a 1014.35 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 765.4 ms n/a n/a 2.37K n/a n/a 1.25 GiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 530.7 ms n/a n/a 5.08K n/a n/a 1.15 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 266.5 ms n/a n/a 6.82K n/a n/a 1.51 GiB n/a
String.split n/a 265.1 ms n/a n/a 6.69K n/a n/a 1.25 GiB n/a
List.mergeSort n/a 262.1 ms n/a n/a 5.55K n/a n/a 1008.04 MiB n/a
Nat.gcd_comm n/a 254.7 ms n/a n/a 1.53K n/a n/a 775.05 MiB n/a
Vector.append n/a 254.5 ms n/a n/a 1.96K n/a n/a 730.16 MiB n/a
String.append n/a 252.9 ms n/a n/a 1.21K n/a n/a 1.24 GiB n/a
Nat.sub_le_of_le_add n/a 252.7 ms n/a n/a 672.780 n/a n/a 616.39 MiB n/a
Int.gcd n/a 252.5 ms n/a n/a 823.830 n/a n/a 666.57 MiB n/a
Nat.add_comm n/a 252.0 ms n/a n/a 166.690 n/a n/a 499.68 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@samuelburnham

samuelburnham commented Jul 8, 2026

Copy link
Copy Markdown
Member Author

!bencher-thresholds-reset all

@github-actions github-actions Bot added the bencher-thresholds-reset:all bencher baseline reset queued on merge label Jul 8, 2026
@github-actions

github-actions Bot commented Jul 8, 2026

Copy link
Copy Markdown

♻️ Baseline reset queued for: all — will anchor to the merge commit when this PR merges.

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs 8595ee8

backends: ooc compile · envs: InitStd · set: primary · shard: 0

compile · InitStd — main from: bencher @ e8dbdb4

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd n/a 4.258 s n/a n/a 24.78K n/a n/a 11.27 GiB n/a n/a 306.43 MiB n/a n/a 105,492 n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · InitStd — main from: base run @ e8dbdb4 (not on bencher)

constant check-time (main) check-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd n/a 10.158 s n/a n/a 8.76K n/a n/a 2.04 GiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 6.151 s n/a n/a 921.140 n/a n/a 2.01 GiB n/a
Array.extract_append n/a 1.018 s n/a n/a 1.52K n/a n/a 988.55 MiB n/a
Vector.extract_append._proof_2 n/a 1.013 s n/a n/a 1.29K n/a n/a 1.32 GiB n/a
Char.ofOrdinal_le_of_le n/a 775.3 ms n/a n/a 3.43K n/a n/a 1.29 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.05 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.16 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 765.5 ms n/a n/a 2.37K n/a n/a 1.24 GiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 530.9 ms n/a n/a 5.08K n/a n/a 1.20 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 266.3 ms n/a n/a 6.82K n/a n/a 1.38 GiB n/a
String.split n/a 265.4 ms n/a n/a 6.68K n/a n/a 1.26 GiB n/a
List.mergeSort n/a 261.9 ms n/a n/a 5.55K n/a n/a 1004.43 MiB n/a
Nat.gcd_comm n/a 254.8 ms n/a n/a 1.53K n/a n/a 813.46 MiB n/a
Vector.append n/a 254.5 ms n/a n/a 1.96K n/a n/a 740.42 MiB n/a
String.append n/a 252.9 ms n/a n/a 1.21K n/a n/a 1.08 GiB n/a
Nat.add_comm n/a 252.6 ms n/a n/a 166.290 n/a n/a 503.77 MiB n/a
Int.gcd n/a 252.5 ms n/a n/a 823.900 n/a n/a 707.26 MiB n/a
Nat.sub_le_of_le_add n/a 252.4 ms n/a n/a 673.440 n/a n/a 634.98 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs 94e942d

backends: ooc compile · envs: InitStd · set: primary · shard: 0

compile · InitStd — main from: bencher @ e8dbdb4

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd n/a 4.050 s n/a n/a 26.05K n/a n/a 11.11 GiB n/a n/a 306.43 MiB n/a n/a 105,492 n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · InitStd — main from: base run @ e8dbdb4 (not on bencher)

constant check-time (main) check-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd n/a 10.426 s n/a n/a 8.54K n/a n/a 2.00 GiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 6.149 s n/a n/a 921.510 n/a n/a 1.97 GiB n/a
Array.extract_append n/a 1.018 s n/a n/a 1.52K n/a n/a 1.13 GiB n/a
Vector.extract_append._proof_2 n/a 1.013 s n/a n/a 1.29K n/a n/a 1.33 GiB n/a
Char.ofOrdinal_le_of_le n/a 775.1 ms n/a n/a 3.43K n/a n/a 1.20 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 765.7 ms n/a n/a 2.37K n/a n/a 1.12 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 991.18 MiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.22 GiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 531.0 ms n/a n/a 5.08K n/a n/a 1.20 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 266.6 ms n/a n/a 6.81K n/a n/a 1.37 GiB n/a
String.split n/a 265.1 ms n/a n/a 6.68K n/a n/a 1.28 GiB n/a
List.mergeSort n/a 262.1 ms n/a n/a 5.55K n/a n/a 990.69 MiB n/a
Nat.gcd_comm n/a 255.1 ms n/a n/a 1.53K n/a n/a 776.26 MiB n/a
Vector.append n/a 254.6 ms n/a n/a 1.96K n/a n/a 681.59 MiB n/a
String.append n/a 253.0 ms n/a n/a 1.21K n/a n/a 1.04 GiB n/a
Nat.sub_le_of_le_add n/a 252.5 ms n/a n/a 673.220 n/a n/a 604.52 MiB n/a
Int.gcd n/a 252.5 ms n/a n/a 823.790 n/a n/a 672.67 MiB n/a
Nat.add_comm n/a 251.9 ms n/a n/a 166.760 n/a n/a 477.46 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs 5fa582b

backends: ooc compile · envs: InitStd · set: primary · shard: 0

compile · InitStd — main from: bencher @ e8dbdb4

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd n/a 3.993 s n/a n/a 26.42K n/a n/a 11.05 GiB n/a n/a 306.43 MiB n/a n/a 105,492 n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · InitStd — main from: base run @ e8dbdb4 (not on bencher)

constant check-time (main) check-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd n/a 10.677 s n/a n/a 8.34K n/a n/a 2.11 GiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 6.148 s n/a n/a 921.570 n/a n/a 1.86 GiB n/a
Array.extract_append n/a 1.018 s n/a n/a 1.52K n/a n/a 1.12 GiB n/a
Vector.extract_append._proof_2 n/a 1.013 s n/a n/a 1.29K n/a n/a 1.25 GiB n/a
Char.ofOrdinal_le_of_le n/a 775.1 ms n/a n/a 3.43K n/a n/a 1.12 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.18 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.06 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.12 GiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 530.7 ms n/a n/a 5.08K n/a n/a 1.17 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 266.6 ms n/a n/a 6.81K n/a n/a 1.38 GiB n/a
String.split n/a 265.1 ms n/a n/a 6.68K n/a n/a 1.29 GiB n/a
List.mergeSort n/a 262.0 ms n/a n/a 5.55K n/a n/a 1.03 GiB n/a
Nat.gcd_comm n/a 254.7 ms n/a n/a 1.53K n/a n/a 855.45 MiB n/a
Vector.append n/a 254.5 ms n/a n/a 1.96K n/a n/a 715.77 MiB n/a
String.append n/a 252.9 ms n/a n/a 1.21K n/a n/a 1.04 GiB n/a
Nat.sub_le_of_le_add n/a 252.6 ms n/a n/a 673.030 n/a n/a 612.18 MiB n/a
Int.gcd n/a 252.5 ms n/a n/a 823.860 n/a n/a 724.20 MiB n/a
Nat.add_comm n/a 252.2 ms n/a n/a 166.550 n/a n/a 479.64 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 8, 2026

Copy link
Copy Markdown

!benchmark — main vs 3c3d090

backends: ooc compile · envs: InitStd · set: primary · shard: 0

compile · InitStd — main from: bencher @ e8dbdb4

constant compile-time (main) compile-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd n/a 4.039 s n/a n/a 26.12K n/a n/a 11.25 GiB n/a n/a 306.43 MiB n/a n/a 105,492 n/a

1 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

ooc · InitStd — main from: base run @ e8dbdb4 (not on bencher)

constant check-time (main) check-time (PR) Δ% throughput (main) throughput (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd n/a 10.174 s n/a n/a 8.75K n/a n/a 2.05 GiB n/a
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual n/a 6.151 s n/a n/a 921.220 n/a n/a 1.99 GiB n/a
Array.extract_append n/a 1.018 s n/a n/a 1.52K n/a n/a 1.21 GiB n/a
Vector.extract_append._proof_2 n/a 1.013 s n/a n/a 1.29K n/a n/a 1.30 GiB n/a
Char.ofOrdinal_le_of_le n/a 775.2 ms n/a n/a 3.43K n/a n/a 1.06 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.08 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq n/a 765.6 ms n/a n/a 2.37K n/a n/a 1.19 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 765.5 ms n/a n/a 2.37K n/a n/a 1.12 GiB n/a
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 531.3 ms n/a n/a 5.08K n/a n/a 1.14 GiB n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq n/a 266.4 ms n/a n/a 6.82K n/a n/a 1.30 GiB n/a
String.split n/a 265.2 ms n/a n/a 6.68K n/a n/a 1.29 GiB n/a
List.mergeSort n/a 262.0 ms n/a n/a 5.55K n/a n/a 1012.01 MiB n/a
Nat.gcd_comm n/a 254.9 ms n/a n/a 1.53K n/a n/a 783.17 MiB n/a
Vector.append n/a 254.4 ms n/a n/a 1.96K n/a n/a 736.90 MiB n/a
String.append n/a 252.9 ms n/a n/a 1.21K n/a n/a 956.42 MiB n/a
Int.gcd n/a 252.4 ms n/a n/a 824.030 n/a n/a 669.97 MiB n/a
Nat.sub_le_of_le_add n/a 252.4 ms n/a n/a 673.580 n/a n/a 605.84 MiB n/a
Nat.add_comm n/a 252.0 ms n/a n/a 166.690 n/a n/a 482.89 MiB n/a

18 constants · 0 regressed · 0 improved (|Δ| > 3.0% on any metric).

⚠️ no main-side results (base run failed — see the workflow logs).

Workflow logs

@samuelburnham
samuelburnham marked this pull request as ready for review July 8, 2026 21:46
arthurpaulino
arthurpaulino previously approved these changes Jul 9, 2026
View reviewed changes
@samuelburnham
fix(zisk): drop --max-witness-stored flag, use Zisk's default cap
eb5bb19 
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.
@samuelburnham
feat(ci): CSV-driven !benchmark + Zisk/SP1/native benchmarks
0e4097f 
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
test(ci): trigger bench-pr.yml on pull_request (TEMPORARY)
22fb53d 
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.
@samuelburnham
fix(bench): sampler-only watchdog with adaptive cadence
1f84dfb 
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.
@samuelburnham
fix(bench): restore the RAM-derived default ceiling
d0c0062 
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.
@samuelburnham
refactor(bench): zkvm testbeds gain the mode suffix (zisk-check-execute)
d513eb7 
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.
@samuelburnham
feat(ci): bench-pr prepare stage — compile each env's .ixe once
507eae9 
The per-cell .ixe cache only helped re-runs: on a fresh commit every
same-env cell missed the cold cache simultaneously and paid its own ix
compile in parallel. A prepare job (matrix over ci parse's new
prep-envs output — envs consumed by non-compile cells) now compiles
each .ixe once and publishes it under the key the cells already
restore, so cells start warm. Skipped for compile-only requests, whose
cells compile fresh by design; a prepare failure stops the cells (they
would just re-fail the same compile lazily).
@samuelburnham
fix(bench): watchdog survives memory-bandwidth bursts and shm undercount
cc93a6b 
Two more runner deaths, two measured causes:

1. aiur prove crossed the ceiling by 13 GB inside one 0.2s sample —
   first-touch of pre-reserved prover buffers grows RSS at memory
   bandwidth, which no cadence outruns. Headroom widens to 24 GiB (the
   ~123 GiB runner's ceiling drops 111 → 99) so the worst measured
   overshoot plus OS/agent fits, and the sampler now TERMs on a
   one-sample linear projection (level + last delta), buying back one
   sample of reaction time — verified live: the kill fires before the
   ceiling is crossed on a steep ramp.

2. zisk died at a nominal 0.4 GB over: the ASM services' locked shared
   segments are under-attributed by per-process RSS. /dev/shm usage now
   counts into the tree total.
@samuelburnham
refactor(bench): watchdog watches MemAvailable — one number, no summa…
fa59b17 
…tion

Everything hairy in the sampler (two ps/awk tree walks, the /dev/shm
add-on, adaptive cadence, trajectory projection, conditional grace)
existed to reconstruct a number the kernel already publishes:
/proc/meminfo MemAvailable, its own estimate of what can be allocated
without thrashing. It natively accounts for everything the tree
consumes (RSS, locked shm, page tables) plus everything else on the
host, and correctly ignores reclaimable page cache.

The watchdog now kills the tree when MemAvailable < MemTotal - ceiling,
at a fixed 0.25s cadence (a meminfo read is ~free, so no adaptive zone)
with a plain TERM -> 2s -> KILL (rows are flushed continuously; the
grace was only ever for destructors). The floor never drops below 4 GiB
so an oversized ceiling still protects the host, and a machine without
/proc/meminfo is refused loudly. ~40 lines shorter, and strictly harder
to fool than the tree-RSS sum it replaces.
@samuelburnham
chore(bench): watchdog cadence 0.25s -> 0.5s
1f23eea
@samuelburnham
fix(ci): build the bench binaries on warp — end the instruction-set l…
dfa0cdc 
…ottery

A 50-run log sweep showed the ubuntu-latest build hosts hand out 4 CPU
models, baking AVX-512 into the -Ctarget-cpu=native binaries on only
~18% of builds — main's history randomly flipped Plonky3 codepaths
between pushes, and main-vs-PR comparisons crossed ISAs ~30% of the
time. The warp fleet is CPU-uniform (AMD EPYC 9R45 / Intel, all
AVX-512), so building there makes the ISA deterministic AND faster.

Every job that runs the binaries moves with the build (a non-AVX-512
GitHub host would SIGILL): bench-main's plan, bench-pr's build (parse)
and assemble (report). setup/comment/thresholds-reset run no ix and
stay on ubuntu-latest. The Log build CPU step stays, as the check that
a regression wasn't a fleet change.
@samuelburnham
refactor(ci): one lean-action for both bench-pr build paths
92627aa 
The cache-hit and cache-miss branches each carried their own
lean-action step (build vs provision-only); a computed build flag
collapses them — miss builds, hit provisions the toolchain the
restored binaries need.
@samuelburnham
fix(bench): per-backend watchdog headroom — compile gets a thin floor
2bbea93 
The 24 GiB headroom killed the Mathlib compile 3 GB from completion
(machine-wide usage ~99.6 GB vs the 99 ceiling): that headroom is sized
for the aiur prover's memory-bandwidth bursts (~13 GB between samples),
while ix compile grows build-paced at a few GB/s and legitimately peaks
near 100 GB. One number can't serve both on a 123 GB machine, so the
headroom moves into the registry per backend: 24 GiB default (provers),
12 for compile (runner ceiling 111, ~11 GB above the measured Mathlib
peak, floor still 4x its worst per-sample growth).
@samuelburnham
refactor(bench): flat 110 GB default ceiling for all backends
9152ca7 
With the MemAvailable watchdog, the per-backend headroom machinery
reduces to one number: 110 sits above the largest legitimate workload
(Mathlib ix compile, ~100 GB) and leaves a ~13 GB free floor on the
~123 GiB runner; the script's 4 GiB minimum floor keeps smaller
machines protected when the default exceeds their RAM. Deletes the
headroomGb registry field and the /proc/meminfo parsing in Lean.
@samuelburnham
fix(bench): default ceiling = machine RAM minus 15 GB
b854fe3 
Derived again (a flat 110 protects nothing on smaller machines and
tracks nothing when the runner class changes): MemTotal - 15 puts the
~123 GiB runner at ~108, above Mathlib ix compile's ~100 GB peak, with
the 15 GB as the MemAvailable kill floor. Same rule for every backend.
@samuelburnham
fix(ci): file-size rides a ±1% band instead of an exact pin
8669d75 
The serialized env size wiggles slightly run-to-run, so the 0/0 pin
alerts on noise. A 1% band still catches real serialization-format
regressions (~32 MB on Mathlib) while tolerating the wiggle. constants
stays pinned — the count is deterministic. That the .ixe is not
byte-reproducible at all is worth its own investigation for a
content-addressed store; noted in the threshold comment.
@samuelburnham
chore(ci): trim the warp-build comment
b292342
@samuelburnham
chore(ci): CPU log prints the actual AVX flag set
5db9a39 
Replaces the avx512f present/absent binary with the full avx2/avx512*
flag list from cpuinfo (or 'absent'), so a regression can be traced to
exactly which extensions the build host offered.
@samuelburnham
chore(ci): pure-Lean ix subcommands run on cheap hosts
a1f58c5 
plan (ci matrix) and assemble (bench report) never execute the Rust
objects where the warp build's AVX-512 lives — Lean code is compiled by
leanc at baseline ISA, and Rust has no life-before-main initializers.
Each job's comment records the assumption: move back to warp if ix
startup or these subcommands ever touch the FFI. The build/prepare/
benchmark/compile jobs keep warp (they compile with target-cpu=native
or execute the prover FFI).
@samuelburnham
feat(bench): watchdog is a systemd-run memory scope — sampler deleted
585608e 
Validated on both ubuntu-latest and warp runners (ix-cpu-info's
cgroup-memcap.yml): systemd-run --user --scope -p MemoryMax=<G>
-p MemorySwapMax=0 hard-caps the tool's cgroup; the kernel OOM-kills at
the ceiling with SIGKILL (exit 137, the orchestrator's OOM signal). No
sampler cadence to race, no tree to sum, no burst arithmetic — the
cgroup charges the whole tree's resident memory and cached allocator
reservations don't count.

The script shrinks to an exec: a passwordless-sudo enable-linger boots
the user manager on CI (no-op locally where a session provides one),
XDG_RUNTIME_DIR is defaulted, and systemd-run replaces the process. No
fallback: without a user bus it fails loudly (exit 1 -> the cell
aborts).
@samuelburnham
chore(ci): revert the TEMPORARY test triggers
cdd6166 
bench-main runs on pushes to main only again; bench-pr is
issue_comment-only — the pull_request trigger, its fixed test command,
the head-ref gate, and the || fallbacks in concurrency/SHA-resolution/
comment-target all go with it. The OOM enforcement and both workflows
were verified end to end from this branch before the revert.
@samuelburnham
fix(bench): OOM-kill the whole scope, not its biggest process
fda8f83 
The zisk shard-plan run for the heavy bitblast block exposed the hole:
a plain systemd scope doesn't set memory.oom.group, so at the cap the
kernel killed only the biggest process — Zisk's ASM MT service — and
the surviving host converted the memory kill into a clean exit 1, which
the orchestrator (correctly) treats as a deterministic failure and
aborts the cell instead of recording the oom row this expected-OOM
constant should produce.

The wrapper now writes memory.oom.group=1 on the scope's cgroup (user-
delegated, no sudo) before exec'ing the tool: breach -> the whole tree
dies with SIGKILL -> exit 137 -> oom row, same semantics the sampler
era had. Failure to set it exits 2 rather than running with
single-victim kill semantics.
@samuelburnham
feat(bench): ix bench run --consts
4e002e2 
One-off runs no longer need a names file: --consts takes the same
comma-separated grammar as the tools, unioned with --names-file via
ConstsFile.gather (the machinery every other consumer already uses).
@samuelburnham
refactor(bench): explicit --ixe replaces --reuse-ixe; comma lists rep…
f8c2fc2 
…lace name files

- ix bench run/shard take --ixe <path> (must exist, used as-is; no flag
  = compile fresh) instead of the magic reuse-if-present flag. The
  workflows pass the cache-restored path explicitly; bench-pr guards
  with [ -f ] so a missed cache still compiles rather than failing.
- ix bench run drops --names-file: --consts (comma-separated, the
  tools' grammar) is the one selection override. bench-pr's targeted
  base run builds the list with paste -sd, from fetch-main's
  missing-out file.
- fetch-main gains --consts alongside the workflow-facing --names file
  (unioned), so the local compare-vs-main flow needs no temp files.
@samuelburnham
feat(ci): bench-pr compiles each env exactly once — prepare becomes c…
c7372ee 
…ompile

The prepare job compiled the .ixe for the prover cells while a
compile-backend cell compiled the same env again for measurement. The
renamed compile job (prepare was ambiguous) now runs for every
requested env and serves both purposes: it publishes the .ixe the
prover cells restore, and its measured row is published too
(bench-pr-row-<sha>-<env>) for the compile cell to reuse as its PR side
— same runner class, same binaries, same command. A row-cache miss just
means the compile cell compiles and measures itself, as before.

ci parse's prep-envs output simplifies to envs (all requested envs).
@samuelburnham
chore: bump tracing-texray to the merged fork commit
b8a61c3 
The rss-sampler/json-sink additions this branch relied on landed
upstream in argumentcomputer/tracing-texray; pin the merged commit
465bbca in place of the pre-merge fork rev.
@samuelburnham
samuelburnham merged commit 49945d1 into main Jul 9, 2026
17 of 18 checks passed
@samuelburnham
samuelburnham deleted the sb/ci-benchmarks branch July 9, 2026 18:10
@github-actions

github-actions Bot commented Jul 9, 2026

Copy link
Copy Markdown

♻️ Baseline reset to 49945d1 for: aiur-check-execute aiur-check-prove ix-compile ooc-check sp1-check-execute zisk-check-execute

samuelburnham added a commit that referenced this pull request Jul 10, 2026
@samuelburnham
ci: Add ix bench plots command to set bencher plots (#483)
e6daffc 
* bench: curate Vectors.csv by measured workload distinctness

Local aiur prove runs plus per-constant closure profiles (targets,
ingress bytes, fft-cost) showed a third of the cheap tier measuring
the same thing:

- drop the base-cost floor duplicates (3-9 constant closures, <13 kB,
  prove within noise of each other): Acc.rec, Trans.mk, Sum.elim,
  Prod.map, Option.bind, Array.toList — Eq.rec stays as the recursor
  representative, Except.bind for monadic bind, WellFounded.fix for
  recursion combinators;
- drop Nat.toDigits (strictly inside Nat.repr's closure), Array.filter
  and Array.foldlM (within 1.5x of Array.map, which stays), Int.add
  (scale twin of primary Nat.add_comm; Int is covered by emod/gcd);
- drop the Int8/Int16/Int32 instRxcHasSize_eq triplets (byte-identical
  siblings of the kept Int64) and the trivials Nat, HEq, HEq.rec,
  Nat.add;
- add Std.HashMap as HEAVY: 1,982-constant closure, 2.28 MB ingress,
  84.6 s / 49 GiB / 18.4B FFTs proved locally — 6-40x every cheap
  constant on every axis.

The prove-feasible full set is now 20 constants spanning recursors,
WF recursion, monadic bind, List/Array, Nat/Int/BitVec/USize
arithmetic, decidability, bytes/strings, hashing, and (via the heavy
tier) big structures.

* fix(bench): align tracing-texray pins with the root workspace

The zisk and sp1 hosts pinned tracing-texray at an older rev than the
root workspace (bumped in #467), so cargo linked TWO instances of the
crate into each host: main() started one instance's RSS sampler while
ix_bench::peak_rss_bytes() read the other's never-started one — always
None — and the resulting null was dropped by `ix bench bmf`'s
numeric-fields filter. Net effect: every zisk upload silently lost
peak-rss (parent and per-shard rows alike) since the pin diverged.

Align both hosts on the root rev and re-lock; cargo tree confirms a
single shared instance, so the sampler the host starts is the one the
row emission reads.

* bench: zisk rows report constants and shards

constants = the named constants certified over the checked closure —
the pre-shard input set, the same universe the aiur rows count via
closureFrom. The cheap paths emit the cover size; the shard-plan path
emits `needed` (targets this run answers for), computed before shard
partitioning and store-reuse filtering, so neither sharding overhead
nor covered-shard skips distort it. Anon-work dedup shrinks the WORK
item count, never this number; sharding's extra work stays visible in
cycles/execute-time where it belongs.

shards was already emitted on shard-plan rows; a non-sharded execute
now reports 1 (a single leaf IS one shard) instead of omitting the
field and rendering n/a in the compare table.

bench-main pins constants 0/0 on the zkvm testbeds like the other
cells: it is deterministic, and a drop means lost coverage, not a win.

* bench: compare-table and !benchmark upgrades

- aiur prove cells report throughput (constants/prove-time was already
  uploaded and thresholded; the registry column list just omitted it —
  every other cell follows the time/throughput/peak-rss convention).
- zisk compare tables gain constants and shards columns, next to cycles.
- The per-constant phase drill-downs are now opt-in via BENCH_PHASES=1
  (a passthrough config key): the spans are noisy and dynamically
  named, so the default comment stays at the headline measures.
- KEY=VALUE config parses inline on the command line too, whitespace-
  separated — the single-line form for bench-pr.yml's manual
  workflow_dispatch, whose input box cannot hold newlines. Inline keys
  are strict (an unknown key rejects, like a typo'd backend); config
  lines stay lenient since comment prose contains `=`.

* bench: `ix bench plots` — registry-driven bencher dashboard sync

One plot per (testbed, measure) bench-main tracks, one line per
benchmark row the cell uploads, plus the cross-kernel input-constants
overlay (aiur and zisk report the same pre-shard closure count, so the
paired lines must coincide — separation is a coverage-drift tripwire).
Titles, dashboard ordering, redundancy skips, and canonical measure
units live here as typed data; the spec derives from the registry +
Vectors.csv, so nothing is hand-listed.

Idempotent, keyed by title: matching plots are kept (index
re-asserted), stale ones deleted and recreated (the plot PATCH endpoint
only takes index/title/window), hand-pinned ones untouched. The sync
also asserts measure units — bencher auto-creates measures with
placeholder units on first upload, leaving plots unitless.

All bencher.dev traffic goes through the bencher CLI; --dry-run
previews with no key. bencher-plots.yml dispatches it manually (like
bencher-thresholds-reset) off the freshest bench-bins cache: run it
after a registry change has merged AND bench-main has built it — the
registry is compiled into the binary, and a new constant only gets its
plot line once its first rows upload.

* fix(ci): bench-pr Mathlib env — mathlib lives in the Benchmarks/Compile subpackage

BENCH_ENVS=Mathlib died at 'Get Mathlib Cache' with 'unknown executable
cache': use-mathlib-cache runs `lake exe cache get`, and mathlib is a
dependency of the Benchmarks/Compile subpackage, not the root workspace
lean-action was pointed at. bench-main had this right; bench-pr now
mirrors it:

- compile job: provision from Benchmarks/Compile (same toolchain as
  root) and `lake build Compile<env>` before the measured compile;
- benchmark cells: no mathlib cache at all — the .ixe comes from the
  compile job, and the lazy Mathlib fallback fails loudly rather than
  fetching oleans it still couldn't build;
- base side: the build action stays on the base root (it builds ix);
  a separate step fetches/builds base mathlib oleans in the subpackage
  when a Mathlib cell must re-run the base.

* ci: bench-pr cells fail on a compile-cache miss instead of recompiling

The benchmark cells carried two lazy fallbacks for artifacts the
compile job publishes in the same run: a missing compile row made the
compile cell re-measure the compile in-cell, and a missing `.ixe` made
`ix bench run` recompile the env fresh. Neither could ever work for
the Mathlib env (its oleans live only in the compile job's subpackage
provisioning), so the fallbacks meant InitStd and Mathlib failed
differently for the same infrastructure problem.

Both restores are now fail-on-cache-miss and the run step always
passes `--ixe`: the artifacts were published moments earlier, so a
miss is an infrastructure failure and every env fails the same way,
loudly, at the restore step. The in-cell "Save PR .ixe" step goes with
the fallback that produced it.

* bench: throughput means constants per second on every backend

The zkVM hosts uploaded cycles/second under the same `throughput` slug
every other cell used for constants/second, so the shared measure had
no honest unit (and the dashboard showed a generic "per second"). The
hosts now report constants/second like everyone else — cheap zisk rows
over the certified cover, shard-plan rows over the pre-shard `needed`
set, sp1 over its checked count (its stdout already printed this
number; the row disagreed) — via one shared `ix_bench::throughput`
calculator. A zkVM's cycle rate stays derivable from its `cycles` and
`execute-time` fields.

The bencher measure's canonical units become "constants / second".

NB: the first post-merge zisk upload drops throughput by orders of
magnitude (meaning change, not a regression) — reset the
zisk-check-execute baseline (!bencher-thresholds-reset) right after,
or the 10% lower bound alerts.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@arthurpaulino arthurpaulino arthurpaulino approved these changes
+1 more reviewer
@github-advanced-security github-advanced-security[bot] github-advanced-security[bot] left review comments
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

bencher-thresholds-reset:all bencher baseline reset queued on merge

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@samuelburnham @arthurpaulino @github-advanced-security