Skip to content

perf(rust-kernel): Intern-assigned uids, symbolic Nat offsets, environment-machine WHNF reducer - #442

Open
samuelburnham wants to merge 24 commits into
mainfrom
sb/kernel-perf
Open

perf(rust-kernel): Intern-assigned uids, symbolic Nat offsets, environment-machine WHNF reducer#442
samuelburnham wants to merge 24 commits into
mainfrom
sb/kernel-perf

Conversation

@samuelburnham

@samuelburnham samuelburnham commented Jun 12, 2026

Copy link
Copy Markdown
Member

This pull request implements Rust-kernel and ixon optimizations for the Zisk guest, measured against the base #411 as deterministic guest cycle counts (ziskemu -m) over dumped shard inputs (zisk/scripts/bench-cycles.sh), with every counted run's committed failures publics word verified zero.

Key Results

  • Int16.instRxcHasSize_eq: 5.70 B → 42.0 M guest steps (135.6×); Int32/Int64 variants confirmed at the same magnitude (~42 M) — in-circuit cost is now integer-width-independent
  • Cycle suite total: 17.53 B → 5.77 B steps (3.04×, −67.1%)
  • Environment-machine WHNF (final two kernel commits): −19.3% suite net; Vector.extract_append._proof_1 −32.4%; the Init Array/Vector Extract proof family −22% to −33% each (five multi-billion-step constants)
  • Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual (28.35 B steps, the most expensive constant measured in Init+Std): previously crashed the 512 MB guest (OOM-class null read) → now completes as a valid kernel pass — lazy closures cut peak RAM, not just cycles
  • Kernel hardened against adversarial inputs: term identity moved off per-node content hashing with the threat model documented (docs/kernel_identity.md), blob bytes verified at load in all deserializers
input base (#411) this PR Δ speedup
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq 5,697,166,200 42,012,168 −99.3% 135.6×
_private.Init.Data.Vector.Extract.0.Vector.extract_append._proof_1 7,690,887,211 3,344,459,375 −56.5% 2.3×
List.mergesort synthetic env 4,005,320,347 2,290,310,593 −42.8% 1.7×
Nat.add_comm 18,690,815 11,532,048 −38.3% 1.6×
Array.binSearchAux._unary 95,800,411 62,862,965 −34.4% 1.5×
Nat.gcd_comm 6,669,821 5,550,752 −16.8% 1.2×
Batteries.RBMap 13,940,412 12,321,092 −11.6% 1.1×
String.append 4,560,304 4,070,450 −10.7% 1.1×
total 17,533,035,521 5,773,119,443 −67.1% 3.04×

Fifteen Commits (oldest first)

  1. bench: guest cycle harness + native single-constant check

    • bench-cycles.sh suite over dumped guest stdins with failures-word validation; check_one example mirrors the guest's reuse-mode check natively

  2. kernel: keep symbolic Nat offsets compact (whnf stuck + offset def-eq)

    • Nat.add x lit / Nat.div|mod x k stay stuck as compact offsets instead of materializing succ^n(x) chains or the division algorithm; bulk offset def-eq decides offset pairs directly
    • The Int16.instRxcHasSize_eq collapse (5.70 B → 56 M) and the UTF-8-codec-class fix

  3. kernel: intern-assigned uids replace per-node blake3 content hashing

    • Term identity becomes intern-table-assigned sequential u64s; shallow structural keys for hash-consing; blake3 stays only at the Ixon boundary (content addresses, Merkle roots, proof-carrying-code claims)
    • The broadest single win: −30–36% on every reduction-heavy input

  4. kernel: memoized prim-family dispatch in the WHNF/def-eq reduction loops

    • Constant heads classified once per address (Native/BitVec/Nat/Decidable/Str); at most one family recognizer runs per iteration instead of the five-probe gauntlet

  5. ixon: defer per-constant address verification to first materialization

    • Constants verify on first get(); blob bytes still verified eagerly at load

  6. bench: add Int32/Int64 instRxcHasSize_eq to the cycle suite

  7. docs: kernel uid identity vs Ixon content addressing

    • Two-layer identity model and why uid collisions are not an attack surface (uids are assigned, never computed from input)

  8. kernel: fix PrimFamily visibility/qualification warnings

  9. kernel: port jcb/fixes H-15 whnf probe pre-filter + H-12 nat output caps

    • Allocation-free transient-nat spine probe ahead of the cache lookup; caps on Nat primitive output sizes

  10. kernel+ixon: harden term identity against adversarial inputs

    • Blob bytes verified against their address at load in all three deserializers; structural equality audited against the adversarial model

  11. kernel: privatize uid-accepting constructors; document cross-shard uid story

  12. docs: design for the environment-machine WHNF port

    • Full design for the Krivine-style machine (ported from the proven IxVM implementation), including the exit-to-outer-loop contract and the known regression class

  13. kernel: environment-machine WHNF (Phase A — lazy substitution on the beta path)

    • whnf_core's App arm enters a closure machine when a beta fires: beta/zeta are O(1) environment pushes; substitution materializes only at machine exits (clo_subst readback), so work is proportional to what the reduction consumes
    • Every exit re-enters the existing loop: ambient zeta, iota, prim dispatch, cheap-mode def-eq flags, and all caches stay byte-identical

  14. kernel: closure-iota at the machine's recursor exit (Phase B)

    • Recursor spines consumed lazily: only the major premise materializes; params/motives/minors and post-major args ride through as closures, so unselected minors (dropped match/Decidable branches) are never substituted and never read back
    • K recursors, literal majors, and struct-eta deliberately miss to the unchanged plain path, preserving the Nat transient-work and linear-rec/offset shortcuts exactly

  15. docs: env-machine WHNF design is implemented (Phases A+B)

@samuelburnham
samuelburnham force-pushed the kernel-riscv branch 7 times, most recently from 582d40b to 61cb1bd Compare June 29, 2026 21:07
Base automatically changed from kernel-riscv to main June 30, 2026 13:41
@samuelburnham
samuelburnham force-pushed the sb/kernel-perf branch 2 times, most recently from 5b0cf31 to 06e1a1d Compare July 24, 2026 01:32
@samuelburnham

samuelburnham commented Jul 24, 2026

Copy link
Copy Markdown
Member Author

!benchmark zisk ooc

@argument-ci-bot

argument-ci-bot Bot commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown

⚠️ Some benchmark jobs failed — results may be partial.

!benchmark — main vs 06e1a1d

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

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

env/constant check-time (main) check-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd 10.963 s 17.971 s +63.9% (1.64× slower) ⚠️ 8.12K 4.95K -39.0% (1.64× slower) ⚠️ 1.88 GiB 1.81 GiB -4.1% 🟢
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual 6.387 s 4.896 s -23.3% (1.30× faster) 🟢 887.050 1.16K +30.5% (1.30× faster) 🟢 1.88 GiB 1.75 GiB -6.7% (1.07× smaller) 🟢
Array.extract_append 1.017 s 769.2 ms -24.4% (1.32× faster) 🟢 1.52K 2.01K +32.2% (1.32× faster) 🟢 1.23 GiB 1.38 GiB +11.8% (1.12× larger) ⚠️
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 529.5 ms 532.6 ms +0.6% 5.09K 5.06K -0.6% 1.23 GiB 1.12 GiB -8.7% (1.10× smaller) 🟢
Vector.extract_append._proof_2 1.012 s 513.8 ms -49.3% (1.97× faster) 🟢 1.29K 2.55K +97.1% (1.97× faster) 🟢 1.42 GiB 1.51 GiB +6.5% (1.07× larger) ⚠️
Char.ofOrdinal_le_of_le 774.1 ms 276.9 ms -64.2% (2.80× faster) 🟢 3.43K 9.60K +179.6% (2.80× faster) 🟢 1.03 GiB 925.72 MiB -12.0% (1.14× smaller) 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 1.015 s 267.3 ms -73.7% (3.80× faster) 🟢 1.79K 6.80K +279.6% (3.80× faster) 🟢 1.45 GiB 1.53 GiB +5.9% (1.06× larger) ⚠️
String.split 264.2 ms 265.2 ms +0.4% 6.71K 6.68K -0.4% 1.19 GiB 1.29 GiB +8.4% (1.08× larger) ⚠️
List.mergeSort 261.6 ms 262.7 ms +0.4% 5.56K 5.53K -0.4% 932.45 MiB 975.80 MiB +4.6% ⚠️
Nat.gcd_comm 254.2 ms 255.0 ms +0.3% 1.53K 1.53K -0.3% 809.72 MiB 848.80 MiB +4.8% ⚠️
Vector.append 255.2 ms 255.0 ms -0.1% 1.95K 1.95K +0.1% 808.94 MiB 760.88 MiB -5.9% (1.06× smaller) 🟢
String.append 253.0 ms 253.1 ms +0.0% 1.21K 1.21K -0.0% 1.12 GiB 1.19 GiB +6.7% (1.07× larger) ⚠️
Nat.sub_le_of_le_add 253.1 ms 252.7 ms -0.2% 671.680 672.790 +0.2% 586.75 MiB 572.40 MiB -2.4%
Nat.add_comm 252.1 ms 252.6 ms +0.2% 166.590 166.280 -0.2% 474.31 MiB 448.05 MiB -5.5% (1.06× smaller) 🟢
Int.gcd 252.6 ms 252.6 ms +0.0% 823.580 823.520 -0.0% 650.78 MiB 650.53 MiB -0.0%

15 env/constants · 8 with regressions · 9 with improvements (|Δ| > 3.0% on any metric).

zisk · InitStd — main from: base run @ 3312c3f (not on bencher)

constant execute-time (main) execute-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% cycles (main) cycles (PR) Δ% constants (main) constants (PR) Δ% shards (main) shards (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 42.805 s n/a n/a 65 n/a n/a 53.80 GiB n/a n/a 18.72B n/a n/a 2,785 n/a n/a 33 n/a
Char.ofOrdinal_le_of_le n/a 29.434 s n/a n/a 94 n/a n/a 53.56 GiB n/a n/a 12.90B n/a n/a 2,776 n/a n/a 22 n/a
Array.extract_append n/a 28.808 s n/a n/a 56 n/a n/a 70.50 GiB n/a n/a 12.48B n/a n/a 1,627 n/a n/a 13 n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 16.974 s n/a n/a 112 n/a n/a 52.95 GiB n/a n/a 7.35B n/a n/a 1,896 n/a n/a 13 n/a
Vector.extract_append._proof_2 n/a 16.387 s n/a n/a 83 n/a n/a 70.52 GiB n/a n/a 7.03B n/a n/a 1,367 n/a n/a 8 n/a
String.split n/a 14.493 s n/a n/a 129 n/a n/a 52.97 GiB n/a n/a 6.42B n/a n/a 1,867 n/a n/a 11 n/a
List.mergeSort n/a 11.234 s n/a n/a 135 n/a n/a 52.76 GiB n/a n/a 4.91B n/a n/a 1,517 n/a n/a 9 n/a
Vector.append n/a 2.477 s n/a n/a 222 n/a n/a 52.42 GiB n/a n/a 1.10B n/a n/a 550 n/a n/a 3 n/a
Nat.gcd_comm n/a 1.683 s n/a n/a 245 n/a n/a 52.08 GiB n/a n/a 742.79M n/a n/a 413 n/a n/a 2 n/a
String.append n/a 820.6 ms n/a n/a 409 n/a n/a 55.34 GiB n/a n/a 360.74M n/a n/a 336 n/a n/a 1 n/a
Int.gcd n/a 566.4 ms n/a n/a 401 n/a n/a 55.19 GiB n/a n/a 245.33M n/a n/a 227 n/a n/a 1 n/a
Nat.sub_le_of_le_add n/a 527.5 ms n/a n/a 356 n/a n/a 55.17 GiB n/a n/a 222.43M n/a n/a 188 n/a n/a 1 n/a
Nat.add_comm n/a 110.0 ms n/a n/a 445 n/a n/a 55.20 GiB n/a n/a 31.51M n/a n/a 49 n/a n/a 1 n/a

13 constants · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

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

Workflow logs

@samuelburnham

samuelburnham commented Jul 24, 2026

Copy link
Copy Markdown
Member Author

!benchmark zisk ooc

@argument-ci-bot

argument-ci-bot Bot commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs cbbad89

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

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

env/constant check-time (main) check-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd 9.461 s 16.468 s +74.1% (1.74× slower) ⚠️ 9.41K 5.41K -42.5% (1.74× slower) ⚠️ 1.90 GiB 2.00 GiB +5.3% (1.05× larger) ⚠️
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual 6.390 s 4.641 s -27.4% (1.38× faster) 🟢 886.700 1.22K +37.7% (1.38× faster) 🟢 1.92 GiB 1.87 GiB -2.4%
Array.extract_append 1.016 s 767.5 ms -24.5% (1.32× faster) 🟢 1.52K 2.02K +32.4% (1.32× faster) 🟢 1.25 GiB 1.53 GiB +23.1% (1.23× larger) ⚠️
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 528.2 ms 531.4 ms +0.6% 5.11K 5.08K -0.6% 1.09 GiB 1.16 GiB +6.2% (1.06× larger) ⚠️
Vector.extract_append._proof_2 1.012 s 512.6 ms -49.3% (1.97× faster) 🟢 1.29K 2.55K +97.4% (1.97× faster) 🟢 1.45 GiB 1.43 GiB -1.1%
Char.ofOrdinal_le_of_le 773.0 ms 275.5 ms -64.4% (2.81× faster) 🟢 3.44K 9.65K +180.5% (2.81× faster) 🟢 982.46 MiB 1.28 GiB +33.4% (1.33× larger) ⚠️
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 764.2 ms 265.3 ms -65.3% (2.88× faster) 🟢 2.38K 6.85K +188.0% (2.88× faster) 🟢 1.37 GiB 1.28 GiB -6.6% (1.07× smaller) 🟢
String.split 263.3 ms 264.5 ms +0.5% 6.73K 6.70K -0.5% 1.24 GiB 1.26 GiB +2.0%
List.mergeSort 261.0 ms 262.0 ms +0.4% 5.57K 5.55K -0.4% 966.89 MiB 1.04 GiB +9.7% (1.10× larger) ⚠️
Vector.append 254.2 ms 255.2 ms +0.4% 1.96K 1.95K -0.4% 701.89 MiB 841.38 MiB +19.9% (1.20× larger) ⚠️
Nat.gcd_comm 253.9 ms 254.2 ms +0.1% 1.54K 1.53K -0.1% 881.78 MiB 841.38 MiB -4.6% 🟢
String.append 253.0 ms 253.0 ms +0.0% 1.21K 1.21K -0.0% 1.15 GiB 1.23 GiB +7.1% (1.07× larger) ⚠️
Int.gcd 252.4 ms 252.7 ms +0.1% 824.160 823.060 -0.1% 729.70 MiB 679.06 MiB -6.9% (1.07× smaller) 🟢
Nat.sub_le_of_le_add 252.5 ms 252.4 ms -0.0% 673.370 673.500 +0.0% 648.44 MiB 594.73 MiB -8.3% (1.09× smaller) 🟢
Nat.add_comm 252.0 ms 252.0 ms -0.0% 166.680 166.700 +0.0% 509.85 MiB 462.18 MiB -9.3% (1.10× smaller) 🟢

15 env/constants · 7 with regressions · 9 with improvements (|Δ| > 3.0% on any metric).

zisk · InitStd — main from: base run @ 7d99a71 (not on bencher)

constant execute-time (main) execute-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% cycles (main) cycles (PR) Δ% constants (main) constants (PR) Δ% shards (main) shards (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 42.342 s n/a n/a 66 n/a n/a 53.80 GiB n/a n/a 18.72B n/a n/a 2,785 n/a n/a 33 n/a
Char.ofOrdinal_le_of_le n/a 29.300 s n/a n/a 95 n/a n/a 53.43 GiB n/a n/a 12.92B n/a n/a 2,776 n/a n/a 22 n/a
Array.extract_append n/a 28.328 s n/a n/a 57 n/a n/a 70.54 GiB n/a n/a 12.48B n/a n/a 1,627 n/a n/a 13 n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 16.641 s n/a n/a 114 n/a n/a 53.01 GiB n/a n/a 7.35B n/a n/a 1,896 n/a n/a 13 n/a
Vector.extract_append._proof_2 n/a 16.227 s n/a n/a 84 n/a n/a 70.59 GiB n/a n/a 7.03B n/a n/a 1,367 n/a n/a 8 n/a
String.split n/a 14.494 s n/a n/a 129 n/a n/a 52.97 GiB n/a n/a 6.42B n/a n/a 1,867 n/a n/a 11 n/a
List.mergeSort n/a 11.006 s n/a n/a 138 n/a n/a 52.79 GiB n/a n/a 4.91B n/a n/a 1,517 n/a n/a 9 n/a
Vector.append n/a 2.414 s n/a n/a 228 n/a n/a 52.43 GiB n/a n/a 1.10B n/a n/a 550 n/a n/a 3 n/a
Nat.gcd_comm n/a 1.660 s n/a n/a 249 n/a n/a 52.09 GiB n/a n/a 743.01M n/a n/a 413 n/a n/a 2 n/a
String.append n/a 819.6 ms n/a n/a 410 n/a n/a 55.34 GiB n/a n/a 360.85M n/a n/a 336 n/a n/a 1 n/a
Int.gcd n/a 553.3 ms n/a n/a 410 n/a n/a 55.19 GiB n/a n/a 245.40M n/a n/a 227 n/a n/a 1 n/a
Nat.sub_le_of_le_add n/a 493.2 ms n/a n/a 381 n/a n/a 55.16 GiB n/a n/a 222.50M n/a n/a 188 n/a n/a 1 n/a
Nat.add_comm n/a 115.2 ms n/a n/a 425 n/a n/a 55.23 GiB n/a n/a 31.53M n/a n/a 49 n/a n/a 1 n/a

13 constants · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

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

Workflow logs

@samuelburnham
samuelburnham force-pushed the sb/kernel-perf branch 2 times, most recently from a77f444 to 64bc041 Compare July 24, 2026 17:08
@samuelburnham

samuelburnham commented Jul 24, 2026

Copy link
Copy Markdown
Member Author

!benchmark zisk ooc

@argument-ci-bot

argument-ci-bot Bot commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs 64bc041

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

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

env/constant check-time (main) check-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd 9.460 s 16.967 s +79.4% (1.79× slower) ⚠️ 9.41K 5.25K -44.2% (1.79× slower) ⚠️ 1.82 GiB 1.98 GiB +8.9% (1.09× larger) ⚠️
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual 6.383 s 4.643 s -27.3% (1.37× faster) 🟢 887.650 1.22K +37.5% (1.37× faster) 🟢 2.04 GiB 1.81 GiB -11.2% (1.13× smaller) 🟢
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 528.4 ms 531.8 ms +0.6% 5.10K 5.07K -0.6% 1.20 GiB 1.16 GiB -2.8%
Array.extract_append 1.016 s 517.6 ms -49.1% (1.96× faster) 🟢 1.52K 2.99K +96.4% (1.96× faster) 🟢 1.19 GiB 1.48 GiB +24.0% (1.24× larger) ⚠️
Vector.extract_append._proof_2 1.012 s 512.6 ms -49.3% (1.97× faster) 🟢 1.29K 2.55K +97.4% (1.97× faster) 🟢 1.52 GiB 1.44 GiB -5.2% (1.05× smaller) 🟢
Char.ofOrdinal_le_of_le 773.1 ms 276.6 ms -64.2% (2.79× faster) 🟢 3.44K 9.61K +179.5% (2.79× faster) 🟢 1.12 GiB 1.55 GiB +38.6% (1.39× larger) ⚠️
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 764.1 ms 265.5 ms -65.3% (2.88× faster) 🟢 2.38K 6.85K +187.8% (2.88× faster) 🟢 1.46 GiB 1.55 GiB +5.9% (1.06× larger) ⚠️
String.split 263.7 ms 264.9 ms +0.4% 6.72K 6.69K -0.4% 1.30 GiB 1.24 GiB -4.8% (1.05× smaller) 🟢
List.mergeSort 261.0 ms 262.0 ms +0.4% 5.57K 5.55K -0.4% 1.02 GiB 1003.31 MiB -3.6% 🟢
Vector.append 255.6 ms 255.4 ms -0.1% 1.95K 1.95K +0.1% 885.11 MiB 930.82 MiB +5.2% (1.05× larger) ⚠️
Nat.gcd_comm 253.8 ms 254.3 ms +0.2% 1.54K 1.53K -0.2% 885.11 MiB 930.82 MiB +5.2% (1.05× larger) ⚠️
String.append 253.0 ms 253.1 ms +0.0% 1.21K 1.21K -0.0% 1.10 GiB 1.19 GiB +7.8% (1.08× larger) ⚠️
Int.gcd 252.6 ms 252.7 ms +0.0% 823.410 823.130 -0.0% 720.55 MiB 724.12 MiB +0.5%
Nat.sub_le_of_le_add 252.6 ms 252.6 ms +0.0% 673.090 673.040 -0.0% 628.77 MiB 609.14 MiB -3.1% 🟢
Nat.add_comm 252.0 ms 252.1 ms +0.0% 166.660 166.630 -0.0% 490.19 MiB 456.57 MiB -6.9% (1.07× smaller) 🟢

15 env/constants · 7 with regressions · 9 with improvements (|Δ| > 3.0% on any metric).

zisk · InitStd — main from: base run @ 6e29ac9 (not on bencher)

constant execute-time (main) execute-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% cycles (main) cycles (PR) Δ% constants (main) constants (PR) Δ% shards (main) shards (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a 41.586 s n/a n/a 67 n/a n/a 53.77 GiB n/a n/a 18.69B n/a n/a 2,785 n/a n/a 33 n/a
Char.ofOrdinal_le_of_le n/a 28.665 s n/a n/a 97 n/a n/a 53.59 GiB n/a n/a 12.95B n/a n/a 2,776 n/a n/a 22 n/a
Array.extract_append n/a 28.108 s n/a n/a 58 n/a n/a 70.63 GiB n/a n/a 12.48B n/a n/a 1,627 n/a n/a 13 n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a 16.340 s n/a n/a 116 n/a n/a 53.00 GiB n/a n/a 7.35B n/a n/a 1,896 n/a n/a 13 n/a
Vector.extract_append._proof_2 n/a 15.866 s n/a n/a 86 n/a n/a 70.61 GiB n/a n/a 7.03B n/a n/a 1,367 n/a n/a 8 n/a
String.split n/a 14.243 s n/a n/a 131 n/a n/a 53.04 GiB n/a n/a 6.42B n/a n/a 1,867 n/a n/a 11 n/a
List.mergeSort n/a 10.813 s n/a n/a 140 n/a n/a 52.79 GiB n/a n/a 4.91B n/a n/a 1,517 n/a n/a 9 n/a
Vector.append n/a 2.397 s n/a n/a 229 n/a n/a 52.42 GiB n/a n/a 1.10B n/a n/a 550 n/a n/a 3 n/a
Nat.gcd_comm n/a 1.643 s n/a n/a 251 n/a n/a 52.08 GiB n/a n/a 743.01M n/a n/a 413 n/a n/a 2 n/a
String.append n/a 801.3 ms n/a n/a 419 n/a n/a 55.35 GiB n/a n/a 360.85M n/a n/a 336 n/a n/a 1 n/a
Int.gcd n/a 534.9 ms n/a n/a 424 n/a n/a 55.18 GiB n/a n/a 245.40M n/a n/a 227 n/a n/a 1 n/a
Nat.sub_le_of_le_add n/a 495.4 ms n/a n/a 379 n/a n/a 55.18 GiB n/a n/a 222.50M n/a n/a 188 n/a n/a 1 n/a
Nat.add_comm n/a 104.5 ms n/a n/a 469 n/a n/a 55.23 GiB n/a n/a 31.53M n/a n/a 49 n/a n/a 1 n/a

13 constants · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

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

Workflow logs

@samuelburnham samuelburnham mentioned this pull request Jul 27, 2026
Merged
@samuelburnham
kernel: uid identity, env-machine WHNF, and reduction-loop perf
9667709 
Rebase of the sb/kernel-perf kernel stack onto main (the early
workspace/backend/sharding commits of this branch were superseded by
their evolved forms merged in #411/#503; this carries only the novel
kernel work, reconciled with main's #473 declared-flag removal and
is_rec_cache):

- intern-assigned uids replace per-node blake3 content hashing: KExpr/
  KUniv identity is a never-reused process-global u64; InternTable keys
  on shallow structural keys (variant tag + child uids + payload);
  cache keys cannot alias across intern-table clears (a stale key can
  only miss). ~20% of guest cycles on reduction-heavy constants came
  from content hashing (app_hash 22-33% cumulative). Design + collision
  analysis in docs/kernel_identity.md.
- adversarial hardening of the uid design: fresh_uid aborts on counter
  exhaustion; literal structural-equality arms compare values as well
  as blob addresses; uid-accepting constructors privatized so a
  caller-supplied uid can never enter a node.
- environment-machine WHNF (design in docs/env_machine_whnf.md):
  Phase A — whnf_core's App arm enters a Krivine-style machine when a
  beta fires; beta/zeta are O(1) environment pushes and substitution
  materializes only at machine exits (clo_subst readback), so a beta
  chain ending in another beta never materializes intermediate bodies.
  Phase B — closure-iota at the machine's recursor exit: only the major
  premise materializes on the main ctor-rule path; the rule RHS
  re-enters the machine with original closures, so unselected minors
  (dropped match/Decidable branches, the UTF-8 codec class) are never
  substituted and never read back.
- memoized prim-family dispatch in the WHNF/def-eq reduction loops:
  classify each head once per iteration via an allocation-free
  app-chain walk + per-address memo (KEnv::prim_family_cache) instead
  of probing all five primitive recognizers per iteration.
- compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod
  base (Lit k) stay stuck in compact form (each keeps its own head, so
  offset def-eq cannot equate /- and +-derived forms); linear-rec
  collapse; offset-aware def-eq.
- H-15 whnf probe pre-filter (allocation-free spine_head_and_len before
  the transient-nat probes) and H-12 output-size caps on native Nat
  arithmetic.
- suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches;
  NatSuccMode::Stuck whnf cache (proves
  ByteArray.utf8DecodeChar?_utf8EncodeChar_append).
- ixon: per-constant address verification deferred to first
  materialization (LazyConstant::get checks pending_addr): constants
  shipped in a closure but never forced by the typechecker are never
  hashed; everything the kernel certifies is still verified when it is
  forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%,
  stringappend -4.2%.
@samuelburnham
kernel: native perf/shard examples (out-of-circuit tooling)
a69b552 
Standalone cargo examples over a .ixe env, bypassing the Lean/FFI
layer, updated to main's steps-based shard cost model
(block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram):

- shard_plan: profile → partition → .ixes manifest, with store-aware
  planning (--store-dir drops work items whose targets the proof store
  already covers, and excludes covered blocks from the partition
  hypergraph — a novel→covered edge is an assumption discharged at
  aggregation, not a cut to minimize); sizes N from machine RAM by
  default.
- perf_check / check_one: native rerun of the guest check_const loop so
  IX_* perf-counter instrumentation can target a single expensive
  constant without re-checking its env.
- heaviest_block / block_reduce_histo / shard_names / manifest_info:
  profiling forensics over blocks and manifests.
@samuelburnham
zisk+sp1: prover batch scripts and logs; bench-compile-init
2d5d348 
- zisk/scripts: prove-batch (sequential shard proving), mem-guard
  (MemAvailable watchdog that kills zisk-host before the OOM killer
  wedges the box), bench-cycles, mergesort-250k repro; reference logs.
- sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with
  WITHOUT_VK_VERIFICATION=1).
- Lean side: bench-compile-init lake exe (imports Init, empty main).
@samuelburnham
zisk: close aggregation soundness gaps (failures word, transitive vk …
d392646 
…pinning)

The aggregate proof was weaker than "these subjects are well-typed":

- The agg guest never read a child's committed failures word (slot 10)
  and hard-committed 0 for its own, so aggregation ERASED the failure
  bit — a kernel-rejected constant could appear under a failures=0 root,
  with only host-side courtesy checks in the way. Every child's failures
  word is now asserted 0 in-circuit.

- vk pinning was not transitive: a child that is itself an aggregate was
  pinned only by its program vk (the shared AGG vk); its own allowed-vk
  set was never inspected. An agg-of-1 built against a rogue allowed set
  (wrapping an arbitrary program's "proof" with forged publics) would
  fold under an honest-looking root. The agg guest now requires every
  aggregate child (allowed-set index ≥ 1, by the new positional
  convention: index 0 = leaf vk, the rest agg vks) to commit THIS
  instance's vks id — the allowed set is uniform down the tree, so the
  pin is recursive. The convention's ordering is bound by the committed
  id hash, which external verifiers already check.

- The host derived the allowed set FROM the untrusted child proofs
  (distinct_vks), so any proof admitted its own program, and a stale
  store folded silently under its old vk. The allowed set is now
  [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk
  after ROM setup); freshly produced proofs are asserted to match;
  stored proofs with a different vk are skipped (re-proven); and the
  root's committed vks id is checked against — and printed for —
  external verifiers.

- A manifest bisection tree whose leaf set differs from the shard id set
  silently dropped proven leaves from the fold while the pre-aggregation
  coverage check (counting proofs PRODUCED, not folded) still passed.
  ShardManifest::from_bytes now rejects such trees, and the host
  additionally checks post-fold that every env target is in the root's
  actual subject set.
@samuelburnham

samuelburnham commented Jul 28, 2026

Copy link
Copy Markdown
Member Author

!benchmark zisk

@argument-ci-bot

argument-ci-bot Bot commented Jul 28, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs d392646

backends: zisk · envs: InitStd · set: primary · shard: 0

zisk · InitStd — main from: base run @ 7ff054b (not on bencher)

constant execute-time (main) execute-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% cycles (main) cycles (PR) Δ% constants (main) constants (PR) Δ% shards (main) shards (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 1m 5.7s 42.029 s -36.0% (1.56× faster) 🟢 42 66 +57.1% (1.57× faster) 🟢 70.51 GiB 53.59 GiB -24.0% (1.32× smaller) 🟢 33.86B 18.67B -44.8% (1.81× fewer) 🟢 2,785 2,785 +0.0% 34 33 -2.9%
Array.extract_append 48.360 s 29.011 s -40.0% (1.67× faster) 🟢 34 56 +64.7% (1.65× faster) 🟢 113.14 GiB 70.54 GiB -37.7% (1.60× smaller) 🟢 23.88B 12.48B -47.7% (1.91× fewer) 🟢 1,627 1,627 +0.0% 13 13 +0.0%
Char.ofOrdinal_le_of_le 52.117 s 28.884 s -44.6% (1.80× faster) 🟢 53 96 +81.1% (1.81× faster) 🟢 82.84 GiB 53.47 GiB -35.5% (1.55× smaller) 🟢 26.70B 12.94B -51.5% (2.06× fewer) 🟢 2,776 2,776 +0.0% 26 22 -15.4% (1.18× fewer) 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 34.894 s 16.539 s -52.6% (2.11× faster) 🟢 54 115 +113.0% (2.13× faster) 🟢 99.26 GiB 53.05 GiB -46.6% (1.87× smaller) 🟢 17.71B 7.35B -58.5% (2.41× fewer) 🟢 1,896 1,896 +0.0% 15 13 -13.3% (1.15× fewer) 🟢
Vector.extract_append._proof_2 27.931 s 16.276 s -41.7% (1.72× faster) 🟢 49 84 +71.4% (1.71× faster) 🟢 113.07 GiB 70.58 GiB -37.6% (1.60× smaller) 🟢 13.62B 7.03B -48.4% (1.94× fewer) 🟢 1,367 1,367 +0.0% 8 8 +0.0%
String.split 19.746 s 14.465 s -26.7% (1.37× faster) 🟢 95 129 +35.8% (1.36× faster) 🟢 52.92 GiB 53.04 GiB +0.2% 10.37B 6.42B -38.0% (1.61× fewer) 🟢 1,867 1,867 +0.0% 11 11 +0.0%
List.mergeSort 15.633 s 11.043 s -29.4% (1.42× faster) 🟢 97 137 +41.2% (1.41× faster) 🟢 52.78 GiB 52.82 GiB +0.1% 8.19B 4.91B -40.1% (1.67× fewer) 🟢 1,517 1,517 +0.0% 9 9 +0.0%
Vector.append 3.287 s 2.432 s -26.0% (1.35× faster) 🟢 167 226 +35.3% (1.35× faster) 🟢 52.42 GiB 52.43 GiB +0.0% 1.75B 1.10B -37.2% (1.59× fewer) 🟢 550 550 +0.0% 3 3 +0.0%
Nat.gcd_comm 2.326 s 1.698 s -27.0% (1.37× faster) 🟢 178 243 +36.5% (1.37× faster) 🟢 52.14 GiB 52.09 GiB -0.1% 1.21B 743.05M -38.6% (1.63× fewer) 🟢 413 413 +0.0% 2 2 +0.0%
String.append 1.142 s 866.6 ms -24.1% (1.32× faster) 🟢 294 388 +32.0% (1.32× faster) 🟢 55.36 GiB 55.35 GiB -0.0% 586.26M 360.87M -38.4% (1.62× fewer) 🟢 336 336 +0.0% 1 1 +0.0%
Int.gcd 800.8 ms 557.5 ms -30.4% (1.44× faster) 🟢 283 407 +43.8% (1.44× faster) 🟢 55.23 GiB 55.19 GiB -0.1% 403.39M 245.42M -39.2% (1.64× fewer) 🟢 227 227 +0.0% 1 1 +0.0%
Nat.sub_le_of_le_add 713.1 ms 512.0 ms -28.2% (1.39× faster) 🟢 264 367 +39.0% (1.39× faster) 🟢 55.20 GiB 55.17 GiB -0.1% 368.19M 222.51M -39.6% (1.65× fewer) 🟢 188 188 +0.0% 1 1 +0.0%
Nat.add_comm 140.0 ms 111.5 ms -20.4% (1.26× faster) 🟢 350 439 +25.4% (1.25× faster) 🟢 55.21 GiB 55.22 GiB +0.0% 52.60M 31.54M -40.0% (1.67× fewer) 🟢 49 49 +0.0% 1 1 +0.0%

13 constants · 0 with regressions · 13 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

@samuelburnham
bench: record tool faults as crash, not oom
decb90e 
A 128+signal death was always recorded as an OOM row, so a zisk mem-planner
segfault (exit 139) rendered as OOM and sent the investigation chasing RAM
budgets instead of a heap-overflow bug. Split the kill statuses: explicit
kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other
signal death records status crash and renders as 💥 CRASH in the compare
table.
@samuelburnham
kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2)
dc1fe89 
The profiler counted whnf entries, def-eq entries, and limb-weighted Nat
arithmetic per constant but dropped them at block aggregation, and nothing
counted term-construction volume at all — leaving the shard cost model only
heartbeats, subst, and bytes to predict guest steps from. Persist all four
op counters per block (format v2) plus a new intern-table visit counter (a
proxy for construction/memory traffic, bumped in intern_expr/intern_univ),
and add a shard_features example that emits a per-shard feature CSV from a
profile + manifest pair for calibrating the cost model against externally
measured shard costs (ziskemu -X on dumped shard inputs).
@samuelburnham
zisk: dump every selected shard's input; skip ROM setup in dump mode
1d9d10c 
--dump-input wrote only the first selected shard and exited, so dumping a
13-shard plan took 13 host invocations. Dump every selected shard in one
run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard
keeps the exact path), and skip client.setup when no proof store is
involved — dump mode never runs the VM and needs the ROM setup (and thus
the proving key) only to derive the shard vk for store filtering.
@samuelburnham
kernel: calibrate the shard planner in Zisk cost units
bd00612 
Replace the heartbeat-based guest-STEP model with one denominated in
ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES +
BASE), so the packing target prices the axes that don't ride the main
trace — DMA/blake3 precompile area and memory ops. Calibration corpus:
118 InitStd shards across 13 constants, each measured with ziskemu -X on
inputs dumped via --dump-input.

  cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq
       + 28.4k*intern (+ 73.2k per cross-ingress byte)

MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per
work item, so intra-shard cache sharing is invisible to per-block
features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram.
On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on
the uid-identity kernel; the intern term carries the memory-traffic/DMA
axis (residual correlation 0.91 with dma_memcpy counts).

Prover models refit on the same corpus. RAM comes from a guarded GPU
prove sweep measured as each prover's systemd-scope cgroup memory.peak —
the OOM-relevant metric CI's watchdog enforces, charging the whole
process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB
low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost
(was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s
measured vs 411s predicted at the largest point).

Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards
(instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within
the actual-cost ceiling; the only violations are the two
INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB
single-leaf), correctly flagged as not fitting the budget.
@samuelburnham
bench: per-constant ooc attribution and a compare top-movers drill-down
c55bde9 
A whole-env ooc regression previously surfaced as one env-keyed number,
with drill-down only into the pre-chosen bench vectors. Now the anon
whole-env check attributes itself: check-rs --per-const <csv> records one
entry per work item (wall nanos, heartbeats, the op counters, and the
predicted Zisk cost via the shard model) from the check loop, and the CLI
joins Lean names from the env's named table (projection-name fallback for
anonymized Muts blocks) so entries survive PRs that shift content
addresses. An entry is ONE constant's (or Muts block's) own check — deps
are lazily ingressed and trusted, each checked in its own entry, with the
consulted closure slice's ingress charged to the entry — so entries sum
to the env total with no double counting. NOT the full-closure scope of
--consts measurements; documented at the recording site, the flag help,
the renderer, and in the rendered output.

The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to
the results file (rotated with the local baseline), and ix bench compare
renders a drill-down when both sides carry one, split by evidence
quality — calibrated on a Mathlib A/A run (640K constants, twice through
one binary): wall time swings up to 2.8s from scheduling alone, while
the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9
absolute; worker->item assignment varies uid blocks and uid-keyed hash
iteration order perturbs a few order-sensitive paths; --workers 1 is
exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own
cost OR >= 1e9 outright, both above the drift envelope) lead the
drill-down ranked by percent change, styled like the main table
('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are
quarantined in a labeled noise section capped at 5 rows. On the A/A run
this renders 0 cost movers, the truthful reading.
@samuelburnham
bench: verdict-first cell layout; collapse tables past 5 rows
63a4cbd 
A multi-cell !benchmark comment stacked every cell's full table; long
cells (a 40-constant zisk table) buried the verdicts. Each cell now leads
with its one-line verdict (and any typecheck failures / empty-side
warnings, which stay unconditionally visible), and the comparison table
collapses into a <details> block when it has more than 5 rows — small
cells (the ooc env row, few-constant runs) stay inline. The per-constant
and phase drill-downs were already collapsible.
@samuelburnham
ci: wire the ooc attribution CSV through the !benchmark pipeline
aca6dfe 
bencher.dev stores metric rows only, so the per-constant drill-down needs
the attribution CSVs to travel beside the results files. bench-main
caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores
the base SHA's entry, carries a base-run-produced CSV through the merge
step (which previously renamed base.json into main.json and orphaned it),
and pairs whichever CSV it has with the PR side's.

The main side ends up with exactly two sources: bencher on FULL coverage
(plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun
for anything less — base SHA not uploaded, partial coverage, an ooc
attribution cache miss, or the fresh token. A rerun measures the full
default selection (a BENCH_CONSTS override still narrows it) and its rows
take priority; bencher-fetched rows only fill rows the rerun failed to
produce, and the table's main-source label says which path ran. This
retires the gap-filling machinery (--consts from missing.txt, the
bencher-priority merge arm) — a full rerun is simpler and
self-consistent, at the cost of re-measuring a cell when a PR adds
constants.
@samuelburnham
zisk: drop the vendored guest linker script
b85b0b0 
Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the
riscv64ima-zisk-zkvm-elf linker script in the target spec again, and
passing the vendored copy on top double-defines the rom/ram memory
regions. Both guest build scripts existed only to pass it — remove them
and the script; the toolchain's embedded script is the single source of
the memory layout.
@samuelburnham
zisk: pin the fork branch with the mem-planner fill_padding fix
6c2f4a5 
Bump every zisk fork pin from blake3-precompile (e4057c4) to
blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows
the mem-planner offsets array before fill_padding pads the last page —
the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the
bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the
shard that crashed 4/4 on the old pin executes clean on the new one
(634M cycles, failures=0), as does the full 13-shard plan on the
locally-patched build the fix was developed against.
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 29, 2026
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 29, 2026
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 29, 2026
@samuelburnham
chore: fix clippy lints (casts, qualifications, poison error, let-chain)
4a8117d 
u32::try_from over as-truncation and u64::from over as-widening in
shard_features; drop redundant std::sync:: qualifications; carry the
PoisonError text instead of discarding it; collapse the texray if into a
let-chain; contains() over iter().any() in the holed-work filter.
@samuelburnham
chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if
acf0b4e 
cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build
deliberately skips the guest compilation under clippy, but include_elf!
still demanded the ELF bytes. Gate the embed (and its import) on
cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes
under clippy. Also collapse the texray if into a let-chain, matching the
zisk host. A real release build of the host still works.
@samuelburnham
ci: clippy gates for the zisk and sp1 host workspaces
35b239c 
The root rust-test clippy never enters the standalone zkVM workspaces, so
their warnings accumulated ungated. Add cargo clippy --release
--all-targets -D warnings to both host jobs, after the build so the
release dep artifacts are shared (and, for zisk, the guest ELFs its build
scripts already produced).
@samuelburnham
chore: String.dropEnd over deprecated String.dropRight
7fd520e
@samuelburnham
Unpin ziskup install
4696435
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 29, 2026
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 29, 2026
@samuelburnham
temp: compatibility layer for pre-branch base-SHA compares
dc3dbb3 
Base-SHA compare runs mix the PR's orchestrator with the base's tools
and toolchain, and the base at 7ff054b predates two of this branch's
changes — droppable wholesale after the first green benchmark whose base
includes this branch:

- Re-pin the CI zisk toolchain to the zisk-1.0.0 artifact: the base's
  guests pass -T zisk.ld unconditionally, which only links against the
  non-embedding toolchain (the latest artifact embeds the script and
  double-defines the rom/ram regions — the base zisk run died there,
  n/a-ing the whole main side). Restore the vendored zisk.ld and the
  probing build.rs on the PR side so its guests build against either
  artifact.

- Probe check-rs --help before passing --per-const: the base's check-rs
  dies on the unknown flag, which killed the whole-env ooc row (the
  n/a InitStd/Mathlib main rows).
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 29, 2026
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 29, 2026
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 29, 2026
@samuelburnham

samuelburnham commented Jul 29, 2026

Copy link
Copy Markdown
Member Author

!benchmark ooc fresh

@samuelburnham

samuelburnham commented Jul 29, 2026

Copy link
Copy Markdown
Member Author

!benchmark ooc fresh BENCH_ENVS=Mathlib

@samuelburnham

samuelburnham commented Jul 29, 2026

Copy link
Copy Markdown
Member Author

!benchmark zisk fresh

@argument-ci-bot

argument-ci-bot Bot commented Jul 29, 2026

Copy link
Copy Markdown

⏳ Benchmark running…

backends: ooc · envs: InitStd · set: primary · shard: 0 · baseline: fresh (base-SHA run, bencher bypassed)

Benchmarking dc3dbb3 — this comment will be replaced with the results when the run finishes.

Watch progress

@argument-ci-bot

argument-ci-bot Bot commented Jul 29, 2026

Copy link
Copy Markdown

⏳ Benchmark running…

backends: ooc · envs: Mathlib · set: primary · shard: 0 · baseline: fresh (base-SHA run, bencher bypassed)

Benchmarking dc3dbb3 — this comment will be replaced with the results when the run finishes.

Watch progress

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@johnchandlerburnham johnchandlerburnham johnchandlerburnham left review comments
@arthurpaulino arthurpaulino Awaiting requested review from arthurpaulino

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@samuelburnham @johnchandlerburnham