Uh oh!
There was an error while loading. Please reload this page.
ci: Standardize benchmarks and input constants - #467
Merged
Conversation
samuelburnhamforce-pushed
the
sb/ci-benchmarks
branch
7 times, most recently
from
July 3, 2026 20:39
07264b9 to
f1ff88aCompareUh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
Contributor
|
Contributor
|
| 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).
Contributor
|
| 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).
Contributor
|
| 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).
Contributor
|
| 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).
samuelburnhamforce-pushed
the
sb/ci-benchmarks
branch
from
July 8, 2026 16:52
1103162 to
b82aed8CompareContributor
|
| 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).
Contributor
|
| 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).
Contributor
|
| 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).
samuelburnham
commented
Jul 8, 2026
MemberAuthor
!bencher-thresholds-reset all |
♻️ Baseline reset queued for: all — will anchor to the merge commit when this PR merges. |
Contributor
|
| 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).
Contributor
|
| 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).
Contributor
|
| 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).
Contributor
|
| 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).
samuelburnham
marked this pull request as ready for review
July 8, 2026 21:46
arthurpaulino
previously approved these changes
Jul 9, 2026
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.
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).
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.
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.
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.
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.
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).
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.
…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.
…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.
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.
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).
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.
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.
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.
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.
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).
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).
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.
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.
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).
…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.
…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).
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.
samuelburnhamforce-pushed
the
sb/ci-benchmarks
branch
from
July 9, 2026 17:59
c8b8650 to
b8a61c3Comparearthurpaulino
approved these changes
Jul 9, 2026
Uh oh!
There was an error while loading. Please reload this page.
♻️ Baseline reset to |
samuelburnham added a commit
that referenced
this pull request
Jul 10, 2026
* 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.
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
3 participants
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.
CI benchmarking:
ix benchLean 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.bench-pr.ymlto use this framework and print the Markdown table as a PR comment (see example comments below).bench-main.ymlto 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.tracing-texrayas 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).Usage
Local benchmarks:
PR comparative benchmarks against main:
Successful runs:
bench-main.yml: https://github.com/argumentcomputer/ix/actions/runs/28976652621bench-pr.yml: https://github.com/argumentcomputer/ix/actions/runs/28976654179Merge after argumentcomputer/tracing-texray#3
Note
Before merge:
aiur-typecheck-x64-32x → aiur-check-prove-x64-32x,zisk-check-x64-32x → zisk-check-execute-x64-32x; archive staleshard-cycles:Nmeasures.aiuras the names have been updated