perf: Switch Aiur from Keccak to Blake3 hashing

[samuelburnham]

Adopt Blake3 for the multi-stark commitment hash, challenger, and recursive verifier

Spans two coordinated branches: multi-stark@blake3 (the prover/verifier hash)
and ix@bench/blake3 (in-circuit recursive-verifier port + tests + dependency bump).

Summary

Use Blake3 as the multi-stark commitment scheme's hash — the Merkle MMCS
(leaf hash + 2-to-1 compression) and the Fiat–Shamir challenger — and port the
in-circuit recursive verifier to match, including its vk/claims digest
bindings, so the verifier is fully Blake3 with no Keccak on any hot path.
Blake3's lighter permutation (7 rounds, 512-bit state) wins on native hardware
and, far more so, in-circuit, where its mostly byte-aligned rotations avoid the
expensive bit-decomposition the previous hash required.

• Leaf proving (any Aiur program): ~25% faster to prove, no RAM change,
  identical FFT/trace.
• Recursive verification: the fully-Blake3 in-circuit verifier shrinks
  ~65× in FFT and ~60× in execution time — the difference between proving
  the verifier being infeasible on a 250 GB box (baseline: OOM > 200 GB) and
  routine (Blake3: 6.8 GB / 4.8 s).

Changes

multi-stark (branch blake3, 0b260d7)

• src/types.rs: Challenger, Mmcs, and the leaf/compress hashers built on
  Blake3 (SerializingHasher<Blake3>, CompressionFunctionFromHasher<Blake3,2,32>,
  [u8;32] digests, SerializingChallenger64<Val, HashChallenger<u8, Blake3, 32>>).
• Cargo.toml: add p3-blake3.
• Reference-value generators (gen_pcs_refs, gen_challenger_refs, #[cfg(test)]):
  the independent source for the Ix self-test reference digests (leaf/compress,
  the Merkle tree, and the challenger samples).

ix (branch bench/blake3)

• Ix/MultiStark/Pcs.lean: MMCS leaf hash (mmcs_hash_row) and 2-to-1 compression
  (mmcs_compress) over the native Blake3 gadget (Ix/IxVM/Blake3.lean); the dead
  Keccak PaddingFreeSponge (pf_sponge_u64/pf_absorb/u64_pick) is removed.
  Digest stays [U64;4] (= the 32 Blake3 output bytes, LE-grouped).
• Ix/MultiStark/Verifier.lean: the Fiat–Shamir challenger flush uses blake3;
  the generic cons8 list helper is relocated here from Keccak.lean.
• Ix/MultiStark.lean: the vk/claims digest bindings (system_digest,
  claims_digest) use b3_to_digest(blake3(..)) in-circuit; IxVM.blake3 is
  merged; merge keccak is dropped (the verifier no longer compiles any Keccak
  circuit — they were unused/height-0). The Keccak gadget module stays available.
• src/aiur/vk_codec.rs: verifying-key Merkle-cap (de)serialization uses the
  Blake3 32-byte digest ([u8;32]).
• Benchmarks/RecursiveVerifier.lean (+ lakefile.lean exe target): the
  recursive-verifier cost benchmark — proves factorial(5), runs the in-circuit
  verifier, reports FFT and (by default) the full prove timeline via texray. Pass
  --execute-only to skip the prove on a memory-constrained box.
• Cargo.toml / Cargo.lock: bump the multi-stark dependency to blake3 (0b260d7).
• Tests — see the dedicated section below.

---

Cost breakdown

All numbers on a 32-core / 250 GB AVX-512 host, parallel (rayon) build.
"FFT cost" = Σ_circuit width·height·log₂(height) (the prover-work / RAM driver).
Baseline = current main (all-Keccak); Blake3 = this PR (all-Blake3).

1. Aiur program — kernel-constant leaf proving

Workload: full-closure typecheck of 49 Init constants (init.ixe), FFT
1.7 M → 4.0 B, baseline vs Blake3 from the same commit (only the hash differs),
paired per-constant.

FFT, trace shape, and execution (witness-gen) time are hash-independent —
byte-identical between baseline and Blake3, verified across all 49 constants. The
commitment hash only affects the proving step:

• Proving time: 145.7 s → 109.6 s over the 49 constants (−24.8%);
  per-constant geomean 1.51× faster (range 1.04–2.21×). The win shrinks as FFT
  grows and the NTT/quotient overtake the hash: ~−48% at ~1e6 FFT → ~−23% at ~1e8
  → ~−9% at ~4e9, so the typical sharded-workload win is 20–50%.
• Peak proving RAM: flat — mean +0.9% (range −2.8% … +5.4%). Peak RSS is
  dominated by trace/LDE buffers (∝ FFT, identical), not the few-KB hash state.

2. Recursive verifier — verify_multi_stark_proof on factorial(5)

Inner proof: a factorial(5) multi-stark proof (numQueries=3, log_blowup=2,
30 KB). The verifier recomputes the inner proof's Merkle/transcript hashes and
its vk/claims digest bindings in-circuit; this PR makes all of that Blake3.

metric	baseline verifier	Blake3 verifier	Δ
In-circuit FFT	~75 B (¹)	~1.15 B	~65× smaller
Execution time	~60 s	~1 s	~60× faster
Execute peak RAM	6.6 GB	0.45 GB	~15×
Proving time	OOM, does not complete (²)	4.8 s	infeasible → feasible
Proving peak RAM	OOM, ~300 GB extrapolated (²)	6.8 GB	infeasible → feasible

(¹) The baseline verifier's FFT is ~99% in-circuit hashing (the bit-decomposition
rotations of the previous hash). Making the vk/claims bindings Blake3 too — not just
the MMCS and challenger — matters here: the vk binding alone is ~2.5 B of FFT, so a
verifier with Blake3 commitments but Keccak bindings still sits at ~3.75 B; moving
the bindings as well brings it to ~1.15 B (the ~65× figure).

(²) Proving the baseline verifier OOMs. Measured under a hard 200 GB cgroup cap
(box-safe), killed mid-prove with the heaviest stages still ahead:

prove stage	peak RSS
aiur/execute	8.5 GB
aiur/witness	98.1 GB
stark/stage1_commit	166.2 GB
stark/lookup_messages	185.8 GB
stark/batch_inverse	198.8 GB → cgroup-killed at 200 GB (before quotient/fri_open)

Extrapolating the remaining stages puts the baseline verifier prove at ~300 GB —
over the 240 GB shutoff. The Blake3 verifier proves comfortably, peaking at 6.8 GB.

3. Supporting microbenchmarks

• Raw native hash (off-circuit, AVX-512): Blake3's smaller state / fewer rounds
  give it the edge on native throughput — the source of the ~25% leaf-proving win.
  (p3-blake3 is scalar-per-leaf; a future packed Blake3 hasher would widen it.)
• In-circuit hash gadget: Blake3 is far cheaper in-circuit (bit-decomposition
  rotations dominate the previous hash). At verifier scale this compounds to ~65×.

---

Tests

All green under the exact CI invocations (lake test -- --ignored … multi-stark recursive-verifier and IxTests -- ffi).

• Self-test reference values regenerated for Blake3 (Ix/MultiStark/Tests.lean):
  pcs_hash_test (leaf/compress), pcs_merkle_test (Merkle verify_batch root +
  tamper), sample_bits_test and pcs_challenger4_test (challenger samples). All
  references come from the multi-stark gen_pcs_refs/gen_challenger_refs
  generators; the leaf digests were cross-checked independently with b3sum.
• End-to-end (Tests/MultiStark.lean::endToEndSuite, the recursive-verifier
  runner): host-side vk/claims digests use Blake3.Rust.hash; the verifier accepts
  the honest factorial(5) proof and rejects a tampered proof byte and a tampered
  claim.
• Blake3 FFI lifecycle (Tests/FFI/Lifecycle.lean, run under ffi): new tests
  mirroring the Keccak ones — official empty-input vector, multi-update == one-shot,
  20-update destructor stress, 4 KB large-input determinism.

Methodology

• Both hashes built from the same commit; the leaf bench's two bench-typecheck
  binaries differ only in the multi-stark hash (FFT-identity confirms apples-to-apples).
• The baseline verifier prove was run under systemd-run --user --scope -p MemoryMax=200G -p MemorySwapMax=0 so a runaway allocation is cgroup-OOM-killed
  (just that process), never tripping the box-level 240 GB shutoff.
• Per-stage timing/RAM via tracing-texray; peak RSS via /usr/bin/time -v.
• lake exe bench-recursive-verifier reproduces §2 (proves by default, ~4.8 s / ~6.8 GB;
  --execute-only for FFT/exec only).

Caveats

1. Verifier FFT/exec carry ±~15% run-to-run noise because the multi-stark
   prover is non-deterministic under parallel (rayon): the same statement
   yields byte-different (valid) proofs, so the verifier authenticates slightly
   different Merkle paths. Confirmed: factorial(5) proof hashes differ across
   parallel runs but are identical single-threaded (RAYON_NUM_THREADS=1); Aiur
   execution FFT is deterministic (factorial(5) execute FFT = 201.627075,
   every run). Worth a separate upstream determinism fix; it does not affect
   correctness or the order-of-magnitude conclusions.
2. Baseline-verifier prove RAM (~300 GB) is extrapolated past the 200 GB cap
   (measured to 198.8 GB with quotient/fri_open still ahead). The infeasibility
   is measured; the exact peak is not.

Dependency ordering

multi-stark@blake3 must merge first; the ix Cargo.toml already pins the
dependency to its branch HEAD (0b260d7) — re-pin to the merge commit on merge.

Follow-ups

• File the parallel-proving non-determinism upstream (Caveat 1).
• Optionally add a packed Blake3 hasher (inter-leaf SIMD) to widen the leaf win. Note the Plonky3 Blake3 implementation is still missing "modifications to tune BLAKE3 for hashing small leaves"
• Native-field Poseidon1/2 for the in-circuit verifier hash (algebraic ≪ bit-oriented
  in-circuit) as a future, larger recursion lever.

Note

After argumentcomputer/multi-stark#61

[samuelburnham]

!benchmark aiur

[argument-ci-bot]

!benchmark — main vs 979953e

backends: aiur=prove · envs: InitStd · set: primary · shard: 0

aiur · InitStd · prove — main from: bencher @ e6daffc + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	54.673 s	55.998 s	+2.4%	52.860	51.610	-2.4%	100.92 GiB	100.87 GiB	-0.1%	11.994 s	11.637 s	-3.0%	207.3 ms	219.4 ms	+5.8% (1.06× slower) ⚠️	33.27 MiB	33.27 MiB	+0.0%	42.43B	42.43B	+0.0%
Array.extract_append	53.870 s	54.067 s	+0.4%	31.670	31.550	-0.4%	92.88 GiB	92.84 GiB	-0.0%	12.228 s	12.357 s	+1.1%	224.7 ms	206.0 ms	-8.3% (1.09× faster) 🟢	33.27 MiB	33.27 MiB	+0.0%	40.03B	40.03B	+0.0%
Char.ofOrdinal_le_of_le	42.892 s	42.801 s	-0.2%	66.730	66.870	+0.2%	76.03 GiB	76.05 GiB	+0.0%	8.771 s	8.893 s	+1.4%	207.9 ms	207.0 ms	-0.4%	33.27 MiB	33.27 MiB	+0.0%	32.73B	32.73B	+0.0%
Vector.extract_append._proof_2	30.833 s	31.503 s	+2.2%	46.740	45.740	-2.1%	53.51 GiB	53.40 GiB	-0.2%	6.897 s	6.840 s	-0.8%	241.7 ms	220.3 ms	-8.8% (1.10× faster) 🟢	33.19 MiB	33.19 MiB	+0.0%	23.34B	23.34B	+0.0%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	26.135 s	26.822 s	+2.6%	75.490	73.560	-2.6%	48.59 GiB	48.62 GiB	+0.1%	4.367 s	4.273 s	-2.2%	211.1 ms	211.3 ms	+0.1%	33.19 MiB	33.19 MiB	+0.0%	17.43B	17.43B	+0.0%
String.split	24.649 s	25.171 s	+2.1%	79.070	77.430	-2.1%	47.06 GiB	47.06 GiB	-0.0%	3.980 s	4.001 s	+0.5%	211.6 ms	213.3 ms	+0.8%	33.19 MiB	33.19 MiB	+0.0%	15.99B	15.99B	+0.0%
List.mergeSort	16.643 s	16.862 s	+1.3%	96.020	94.770	-1.3%	29.81 GiB	29.81 GiB	+0.0%	2.759 s	2.782 s	+0.9%	251.2 ms	213.3 ms	-15.1% (1.18× faster) 🟢	33.19 MiB	33.19 MiB	+0.0%	11.63B	11.63B	+0.0%
Vector.append	5.569 s	5.236 s	-6.0% (1.06× faster) 🟢	101.640	108.090	+6.3% (1.06× faster) 🟢	8.96 GiB	9.00 GiB	+0.4%	522.0 ms	526.0 ms	+0.8%	215.2 ms	202.3 ms	-6.0% (1.06× faster) 🟢	32.96 MiB	32.96 MiB	+0.0%	2.60B	2.60B	+0.0%
Nat.gcd_comm	4.183 s	4.140 s	-1.0%	99.220	100.230	+1.0%	7.09 GiB	7.08 GiB	-0.1%	341.5 ms	348.2 ms	+1.9%	202.2 ms	215.0 ms	+6.4% (1.06× slower) ⚠️	32.96 MiB	32.96 MiB	+0.0%	1.75B	1.75B	+0.0%
String.append	2.964 s	2.983 s	+0.6%	119.100	118.340	-0.6%	4.55 GiB	4.44 GiB	-2.6%	189.5 ms	186.1 ms	-1.8%	199.3 ms	197.8 ms	-0.7%	32.89 MiB	32.89 MiB	+0.0%	967.65M	967.65M	+0.0%
Int.gcd	2.469 s	2.327 s	-5.7% (1.06× faster) 🟢	92.760	98.400	+6.1% (1.06× faster) 🟢	3.25 GiB	3.27 GiB	+0.6%	122.8 ms	124.0 ms	+0.9%	197.9 ms	206.6 ms	+4.4% ⚠️	32.89 MiB	32.89 MiB	+0.0%	605.84M	605.84M	+0.0%
Nat.sub_le_of_le_add	2.230 s	2.163 s	-3.0% 🟢	85.200	87.860	+3.1% 🟢	3.06 GiB	3.01 GiB	-1.7%	95.8 ms	93.7 ms	-2.2%	198.1 ms	216.7 ms	+9.4% (1.09× slower) ⚠️	32.89 MiB	32.89 MiB	+0.0%	510.60M	510.60M	+0.0%
Nat.add_comm	1.122 s	1.152 s	+2.7%	45.470	44.260	-2.7%	1.46 GiB	1.44 GiB	-1.3%	15.6 ms	14.4 ms	-8.0% (1.09× faster) 🟢	210.9 ms	195.1 ms	-7.5% (1.08× faster) 🟢	32.76 MiB	32.76 MiB	+0.0%	53.90M	53.90M	+0.0%
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 18.8s	1m 19.1s	+0.3%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	261.03B	+0.0%

14 constants · 4 regressed · 5 improved (|Δ| > 3.0% on any metric).

Workflow logs

[samuelburnham]

!benchmark aiur-recursive

[argument-ci-bot]

!benchmark — main vs 7416ea3

backends: aiur-recursive · envs: InitStd · set: primary · shard: 0

aiur-recursive · InitStd — main from: bencher @ c7c3bd6 + base run (1 new)

proof	recursive-prove-time (main)	recursive-prove-time (PR)	Δ%	recursive-peak-ram (main)	recursive-peak-ram (PR)	Δ%	recursive-proof-size (main)	recursive-proof-size (PR)	Δ%	recursive-verify-time (main)	recursive-verify-time (PR)	Δ%	recursive-execute-time (main)	recursive-execute-time (PR)	Δ%	recursive-fft-cost (main)	recursive-fft-cost (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%
factorial-q3-b2	OOM	3.458 s	n/a	OOM	6.68 GiB	n/a	OOM	1021.01 KiB	n/a	OOM	8.4 ms	n/a	42.929 s	538.9 ms	-98.7% (79.67× faster) 🟢	72.56B	1.19B	-98.4% (61.09× fewer) 🟢	332.8 ms	212.7 ms	-36.1% (1.56× faster) 🟢	29.42 KiB	29.42 KiB	+0.0%	393.0 µs	330.0 µs	-16.0% (1.19× faster) 🟢	416.17 MiB	417.21 MiB	+0.2%
square-q1-b1	52.277 s	1.813 s	-96.5% (28.84× faster) 🟢	83.43 GiB	2.66 GiB	-96.8% (31.35× smaller) 🟢	624.49 KiB	709.56 KiB	+13.6% (1.14× larger) ⚠️	5.7 ms	5.6 ms	-0.9%	17.491 s	270.8 ms	-98.5% (64.59× faster) 🟢	32.22B	668.52M	-97.9% (48.19× fewer) 🟢	265.2 ms	168.3 ms	-36.6% (1.58× faster) 🟢	11.71 KiB	11.71 KiB	+0.0%	186.0 µs	171.0 µs	-8.1% (1.09× faster) 🟢	311.46 MiB	319.44 MiB	+2.6%

2 proofs · 1 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

[samuelburnham]

!benchmark

[argument-ci-bot]

!benchmark — main vs 03e039b

backends: aiur=prove · envs: InitStd · set: primary · shard: 0

aiur · InitStd · prove — main from: bencher @ e94c81a + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	1m 27.4s	57.238 s	-34.5% (1.53× faster) 🟢	33.070	50.490	+52.7% (1.53× faster) 🟢	100.74 GiB	100.69 GiB	-0.0%	13.400 s	11.761 s	-12.2% (1.14× faster) 🟢	293.1 ms	213.5 ms	-27.2% (1.37× faster) 🟢	33.27 MiB	33.27 MiB	+0.0%	42.43B	42.43B	+0.0%
Array.extract_append	1m 23.5s	54.179 s	-35.1% (1.54× faster) 🟢	20.430	31.490	+54.1% (1.54× faster) 🟢	92.63 GiB	92.70 GiB	+0.1%	13.871 s	12.342 s	-11.0% (1.12× faster) 🟢	277.9 ms	230.2 ms	-17.2% (1.21× faster) 🟢	33.27 MiB	33.27 MiB	+0.0%	40.03B	40.03B	+0.0%
Char.ofOrdinal_le_of_le	1m 6.7s	43.369 s	-35.0% (1.54× faster) 🟢	42.890	65.990	+53.9% (1.54× faster) 🟢	75.85 GiB	75.83 GiB	-0.0%	9.940 s	8.817 s	-11.3% (1.13× faster) 🟢	267.0 ms	210.8 ms	-21.1% (1.27× faster) 🟢	33.27 MiB	33.27 MiB	+0.0%	32.73B	32.73B	+0.0%
Vector.extract_append._proof_2	48.663 s	31.795 s	-34.7% (1.53× faster) 🟢	29.610	45.320	+53.1% (1.53× faster) 🟢	53.34 GiB	53.31 GiB	-0.1%	7.754 s	6.772 s	-12.7% (1.15× faster) 🟢	262.9 ms	217.2 ms	-17.4% (1.21× faster) 🟢	33.19 MiB	33.19 MiB	+0.0%	23.34B	23.34B	+0.0%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	41.869 s	26.057 s	-37.8% (1.61× faster) 🟢	47.120	75.720	+60.7% (1.61× faster) 🟢	48.43 GiB	48.36 GiB	-0.1%	5.060 s	4.294 s	-15.1% (1.18× faster) 🟢	262.6 ms	204.3 ms	-22.2% (1.29× faster) 🟢	33.19 MiB	33.19 MiB	+0.0%	17.43B	17.43B	+0.0%
String.split	39.604 s	25.094 s	-36.6% (1.58× faster) 🟢	49.210	77.670	+57.8% (1.58× faster) 🟢	46.80 GiB	46.87 GiB	+0.2%	4.623 s	3.967 s	-14.2% (1.17× faster) 🟢	256.6 ms	214.4 ms	-16.5% (1.20× faster) 🟢	33.19 MiB	33.19 MiB	+0.0%	15.99B	15.99B	+0.0%
List.mergeSort	26.085 s	17.115 s	-34.4% (1.52× faster) 🟢	61.260	93.370	+52.4% (1.52× faster) 🟢	29.68 GiB	29.63 GiB	-0.2%	3.197 s	2.754 s	-13.8% (1.16× faster) 🟢	296.7 ms	208.9 ms	-29.6% (1.42× faster) 🟢	33.19 MiB	33.19 MiB	+0.0%	11.63B	11.63B	+0.0%
Vector.append	7.479 s	5.260 s	-29.7% (1.42× faster) 🟢	75.670	107.600	+42.2% (1.42× faster) 🟢	8.36 GiB	8.55 GiB	+2.4%	646.1 ms	530.4 ms	-17.9% (1.22× faster) 🟢	264.8 ms	212.0 ms	-20.0% (1.25× faster) 🟢	32.96 MiB	32.96 MiB	+0.0%	2.60B	2.60B	+0.0%
Nat.gcd_comm	6.238 s	4.178 s	-33.0% (1.49× faster) 🟢	66.530	99.330	+49.3% (1.49× faster) 🟢	6.88 GiB	6.93 GiB	+0.8%	430.4 ms	356.7 ms	-17.1% (1.21× faster) 🟢	246.5 ms	209.8 ms	-14.9% (1.17× faster) 🟢	32.96 MiB	32.96 MiB	+0.0%	1.75B	1.75B	+0.0%
String.append	4.081 s	2.991 s	-26.7% (1.36× faster) 🟢	86.500	118.020	+36.4% (1.36× faster) 🟢	4.28 GiB	4.33 GiB	+1.2%	239.4 ms	196.0 ms	-18.1% (1.22× faster) 🟢	247.4 ms	201.9 ms	-18.4% (1.23× faster) 🟢	32.89 MiB	32.89 MiB	+0.0%	967.65M	967.65M	+0.0%
Int.gcd	3.230 s	2.341 s	-27.5% (1.38× faster) 🟢	70.900	97.840	+38.0% (1.38× faster) 🟢	3.10 GiB	3.10 GiB	+0.3%	156.5 ms	124.5 ms	-20.5% (1.26× faster) 🟢	240.7 ms	198.4 ms	-17.6% (1.21× faster) 🟢	32.89 MiB	32.89 MiB	+0.0%	605.84M	605.84M	+0.0%
Nat.sub_le_of_le_add	2.869 s	2.194 s	-23.5% (1.31× faster) 🟢	66.230	86.610	+30.8% (1.31× faster) 🟢	2.89 GiB	2.86 GiB	-1.0%	122.2 ms	101.9 ms	-16.6% (1.20× faster) 🟢	249.1 ms	198.3 ms	-20.4% (1.26× faster) 🟢	32.89 MiB	32.89 MiB	+0.0%	510.60M	510.60M	+0.0%
Nat.add_comm	1.504 s	1.118 s	-25.6% (1.34× faster) 🟢	33.910	45.600	+34.5% (1.34× faster) 🟢	1.29 GiB	1.27 GiB	-1.2%	18.5 ms	13.3 ms	-28.4% (1.40× faster) 🟢	244.2 ms	195.8 ms	-19.8% (1.25× faster) 🟢	32.76 MiB	32.76 MiB	+0.0%	53.90M	53.90M	+0.0%
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 18.7s	1m 18.9s	+0.3%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	261.03B	+0.0%

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

Workflow logs

[samuelburnham]

!benchmark aiur-recursive

[argument-ci-bot]

!benchmark — main vs 6bf1430

backends: aiur-recursive · envs: InitStd · set: primary · shard: 0

aiur-recursive · InitStd — main from: base run @ e94c81a (not on bencher)

proof	recursive-prove-time (main)	recursive-prove-time (PR)	Δ%	recursive-peak-ram (main)	recursive-peak-ram (PR)	Δ%	recursive-proof-size (main)	recursive-proof-size (PR)	Δ%	recursive-verify-time (main)	recursive-verify-time (PR)	Δ%	recursive-execute-time (main)	recursive-execute-time (PR)	Δ%	recursive-fft-cost (main)	recursive-fft-cost (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%
factorial-q100-b2	OOM	31.232 s	n/a	OOM	74.71 GiB	n/a	OOM	15.84 MiB	n/a	OOM	123.1 ms	n/a	OOM	8.850 s	n/a	OOM	17.97B	n/a	OOM	245.2 ms	n/a	OOM	848.61 KiB	n/a	OOM	6.4 ms	n/a	OOM	410.41 MiB	n/a
square-q100-b1	OOM	22.585 s	n/a	OOM	43.54 GiB	n/a	OOM	15.76 MiB	n/a	OOM	112.8 ms	n/a	13m 8.2s	7.532 s	-99.0% (104.64× faster) 🟢	1.32T	15.42B	-98.8% (85.44× fewer) 🟢	311.5 ms	176.7 ms	-43.3% (1.76× faster) 🟢	782.05 KiB	782.05 KiB	+0.0%	8.0 ms	5.3 ms	-33.5% (1.50× faster) 🟢	311.89 MiB	322.62 MiB	+3.4% ⚠️

2 proofs · 1 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs