recursive verifier minimization - #561
Open
gabriel-barrett wants to merge 15 commits into
Open
Conversation
Member
Author
|
!benchmark aiur-recursive fresh |
|
| constant | 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) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
String.split |
34.584 s | 34.167 s | -1.2% | 102.24 GiB | 89.64 GiB | -12.3% (1.14× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 33.8 ms | 25.1 ms | -25.8% (1.35× faster) 🟢 | 5.756 s | 4.984 s | -13.4% (1.15× faster) 🟢 | 174.60B | 194.51B | +11.4% (1.11× more) |
15.705 s | 15.803 s | +0.6% | 11.27 MiB | 10.85 MiB | -3.7% 🟢 | 71.4 ms | 73.0 ms | +2.2% | 31.73 GiB | 32.41 GiB | +2.2% |
Vector.append |
31.958 s | 32.349 s | +1.2% | 90.49 GiB | 87.50 GiB | -3.3% 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 32.3 ms | 26.9 ms | -16.7% (1.20× faster) 🟢 | 5.214 s | 4.251 s | -18.5% (1.23× faster) 🟢 | 157.39B | 167.71B | +6.6% (1.07× more) |
4.289 s | 4.284 s | -0.1% | 10.48 MiB | 10.06 MiB | -4.0% 🟢 | 64.6 ms | 66.7 ms | +3.2% |
7.17 GiB | 7.41 GiB | +3.3% |
Nat.add_comm |
22.682 s | 20.995 s | -7.4% (1.08× faster) 🟢 | 60.29 GiB | 55.99 GiB | -7.1% (1.08× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 33.3 ms | 25.0 ms | -24.7% (1.33× faster) 🟢 | 3.809 s | 3.145 s | -17.4% (1.21× faster) 🟢 | 113.93B | 119.13B | +4.6% |
1.093 s | 1.097 s | +0.4% | 9.15 MiB | 8.74 MiB | -4.5% 🟢 | 56.0 ms | 54.4 ms | -2.9% | 3.69 GiB | 4.08 GiB | +10.8% (1.11× larger) |
Member
Author
|
!benchmark aiur fresh |
|
| 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 |
34.999 s | 34.815 s | -0.5% | 76.890 | 77.290 | +0.5% | 69.09 GiB | 70.56 GiB | +2.1% | 8.787 s | 8.831 s | +0.5% | 135.7 ms | 137.3 ms | +1.2% | 21.77 MiB | 20.96 MiB | -3.7% 🟢 | 126.12B | 133.37B | +5.7% (1.06× more) |
Char.ofOrdinal_le_of_le |
28.733 s | 29.730 s | +3.5% |
92.090 | 89 | -3.4% |
56.31 GiB | 63.15 GiB | +12.2% (1.12× larger) |
6.779 s | 6.767 s | -0.2% | 137.8 ms | 131.1 ms | -4.9% (1.05× faster) 🟢 | 21.78 MiB | 20.97 MiB | -3.7% 🟢 | 99.10B | 104.44B | +5.4% (1.05× more) |
Array.extract_append |
24.644 s | 24.793 s | +0.6% | 62.570 | 62.200 | -0.6% | 47.42 GiB | 48.17 GiB | +1.6% | 5.882 s | 5.877 s | -0.1% | 141.2 ms | 129.1 ms | -8.5% (1.09× faster) 🟢 | 21.60 MiB | 20.79 MiB | -3.7% 🟢 | 86.05B | 89.21B | +3.7% |
Vector.extract_append._proof_2 |
16.337 s | 16.333 s | -0.0% | 79.700 | 79.710 | +0.0% | 31.36 GiB | 31.71 GiB | +1.1% | 3.614 s | 3.596 s | -0.5% | 134.2 ms | 130.8 ms | -2.5% | 21.44 MiB | 20.63 MiB | -3.8% 🟢 | 53.57B | 55.86B | +4.3% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
16.505 s | 16.140 s | -2.2% | 109.780 | 112.270 | +2.3% | 32.38 GiB | 33.06 GiB | +2.1% | 3.416 s | 3.403 s | -0.4% | 133.3 ms | 127.9 ms | -4.0% 🟢 | 21.62 MiB | 20.81 MiB | -3.7% 🟢 | 51.47B | 54.68B | +6.2% (1.06× more) |
String.split |
15.640 s | 15.741 s | +0.6% | 112.850 | 112.130 | -0.6% | 31.71 GiB | 32.39 GiB | +2.1% | 3.268 s | 3.187 s | -2.5% | 135.5 ms | 135.9 ms | +0.2% | 21.78 MiB | 20.97 MiB | -3.7% 🟢 | 48.07B | 50.90B | +5.9% (1.06× more) |
List.mergeSort |
12.409 s | 12.372 s | -0.3% | 116.690 | 117.040 | +0.3% | 24.54 GiB | 24.88 GiB | +1.4% | 2.436 s | 2.454 s | +0.7% | 140.0 ms | 130.5 ms | -6.8% (1.07× faster) 🟢 | 21.68 MiB | 20.87 MiB | -3.7% 🟢 | 35.66B | 37.87B | +6.2% (1.06× more) |
Vector.append |
4.276 s | 4.202 s | -1.7% | 113.410 | 115.410 | +1.8% | 7.55 GiB | 7.21 GiB | -4.4% 🟢 | 738.3 ms | 722.9 ms | -2.1% | 125.5 ms | 130.2 ms | +3.7% |
20.25 MiB | 19.44 MiB | -4.0% 🟢 | 8.67B | 9.14B | +5.4% (1.05× more) |
Nat.gcd_comm |
3.270 s | 3.304 s | +1.0% | 119.250 | 118.040 | -1.0% | 6.16 GiB | 6.36 GiB | +3.3% |
545.1 ms | 533.8 ms | -2.1% | 126.0 ms | 126.6 ms | +0.5% | 20.08 MiB | 19.27 MiB | -4.0% 🟢 | 5.48B | 5.87B | +7.2% (1.07× more) |
String.append |
2.434 s | 2.445 s | +0.4% | 124.880 | 124.330 | -0.4% | 4.67 GiB | 4.69 GiB | +0.4% | 427.4 ms | 405.9 ms | -5.0% (1.05× faster) 🟢 | 118.1 ms | 113.7 ms | -3.8% 🟢 | 19.34 MiB | 18.53 MiB | -4.2% 🟢 | 3.04B | 3.25B | +7.0% (1.07× more) |
Int.gcd |
2.030 s | 2.120 s | +4.4% |
102.460 | 98.120 | -4.2% |
4.59 GiB | 4.55 GiB | -1.0% | 359.6 ms | 353.4 ms | -1.7% | 120.1 ms | 109.5 ms | -8.8% (1.10× faster) 🟢 | 18.91 MiB | 18.10 MiB | -4.3% 🟢 | 1.96B | 2.09B | +6.8% (1.07× more) |
Nat.sub_le_of_le_add |
1.867 s | 1.885 s | +1.0% | 91.070 | 90.190 | -1.0% | 5.44 GiB | 4.70 GiB | -13.6% (1.16× smaller) 🟢 | 367.9 ms | 347.6 ms | -5.5% (1.06× faster) 🟢 | 124.0 ms | 113.2 ms | -8.7% (1.10× faster) 🟢 | 19.29 MiB | 18.48 MiB | -4.2% 🟢 | 1.70B | 1.81B | +6.5% (1.07× more) |
Nat.add_comm |
1.072 s | 1.113 s | +3.8% |
39.170 | 37.740 | -3.7% |
4.08 GiB | 3.68 GiB | -9.8% (1.11× smaller) 🟢 | 275.1 ms | 252.1 ms | -8.3% (1.09× faster) 🟢 | 109.2 ms | 101.5 ms | -7.1% (1.08× faster) 🟢 | 17.67 MiB | 16.89 MiB | -4.4% 🟢 | 274.30M | 287.17M | +4.7% |
Split blake3_compress into an @-inlined blake3_compress_init (state assembly from cv/block/counter/len/flags) and a staged blake3_compress(stage, state) that runs one round per row through recursion, with the message-schedule permutation applied between rows and stage 7 folding the working halves into the digest. The 7 unrolled rounds previously ran in one straight-line circuit, paying width for every round: blake3_compress 1080 + blake3_compress_inner_j 1192 -> staged blake3_compress 925 (inner_j @-inlined; height 654 -> 5544). Layer = &LayerNode: thread the chunk-tree layer as a pointer instead of a by-value enum, so it crosses circuit boundaries as 1 column instead of a 33-wide value. Also inline-call blake3 at its call sites (the hash drivers are their own circuits; the wrapper only added one). Measured on bench-recursive-verifier --execute-only --use-bytecode --queries 3 (factorial(5)): total width 11239 -> 9711 (-13.6%), FFT cost 5.51e8 -> 5.05e8 (-8.4%). Regenerated aiur_ixvm.rs + aiur_multi_stark.rs.
Routes execution through the generic Aiur bytecode interpreter instead of the codegen'd IxVM kernel, so Ix/IxVM/*.lean edits can be benched with just a Lean rebuild - no ix codegen + cargo cycle. Covers Phase 1 (checkAddrWithEnv / Toplevel.execute), the prove's witness generation (proveAddrWithEnv gains the same useBytecode toggle the check path already had; the Rust side picks Toplevel::execute over execute_ixvm), and both --recursive steps (executeMultiStark / proveMultiStark, whose toggles already existed). fft-cost is executor-independent; execute-time rows are not comparable to codegen-mode runs.
Convert ~40 call sites to the inline form (@fn): the entrypoint chain (read_proof, read_system, read_claims, verify, ood_verify, fiat_shamir, pcs_fri_verify), the deserializer wrapper layer (read_commitments, read_fri_proof, read_active, read_merkle_cap_at, the single-site read_*_vec wrappers, read_digest_at, read_ext_at, read_sys_params, read_vk_digest, read_sys_lookup, cons_shape7), the OOD/PCS helpers (trace_selectors, trace_vanishing, build_publics, ood_composition, ood_prep_rows, opt_commit_cap, mmcs_root, digest_eq, inject_maybe, compress_ordered, recon_evals, flatten2, ro_x, b3_rows, seed_tag_onto, claims_onto, ext_is_zero, read_one_claim), and b3_to_digest (pure wiring; each of its 5 call sites paid ~33 columns for re-indexing). A single-call-site circuit costs its inputs + outputs + fixed overhead (selector, stage-2 and quotient floors, the caller's call lookup) for no benefit -- call arguments are free, so callers typically get narrower or grow by ~1 column (read_digest_vec_at_n 54 -> 55 while absorbing read_digest_at's 43-wide circuit). None of the inlined bodies are lookup-heavy branchless fns (those would double their stage-2 cost inside a branchy caller). read_preprocessed and read_sys_circuit stay cross-circuit: a let-bound match inside a body that is itself spliced as a let-RHS trips the inliner ("Non-tail match in arbitrary position"); verify and ood_verify needed a var let at the call site for the same reason. Measured on bench-recursive-verifier --execute-only --use-bytecode (factorial(5)): total width 9711 -> 8697 (-10.4%), circuits 202 -> 158; FFT cost at q=50 3.62e9 -> 3.59e9. Regenerated aiur_multi_stark.rs.
…record reader
Four width reductions, all measured (bench-recursive-verifier
--execute-only --use-bytecode, factorial(5)):
- ch_sample8 pops its 8 bytes directly, flushing at most once up front:
the output buffer always holds a multiple of 8 bytes at a draw
boundary (flushes refill 32, draws take 8, observes clear), so the
per-byte ch_sample_byte circuit (82 wide x 736 rows at q=50) was pure
overhead; the two arms' pops share columns. 124 -> 117 combined.
- ch_sample_bits decomposes only the low 4 sampled bytes: 32 bits bound
every log-height (Goldilocks two-adicity), and take_bits aborts on the
Nil match past the available bits exactly as it did at 64. The full 8
bytes are still drawn (Fiat-Shamir alignment). sample8_bits's circuit
disappears: 130 -> 69 combined.
- two_adic_gen derives g_k = g_{k+1}^2 from the maximal 2^32 generator
instead of a 33-arm table whose default arm alone cost 32 aux + 33
selectors: 73 -> 17, memoized chain of <= 32 rows. bits <= 32 is now
load-bearing, so the proof-advice sources are bounded: log_degrees
entries (u8_less_than guard in ood_loop) and log_gmax (u32_less_than
guard in pcs_fri_verify).
- read_sys_circuit computes gslots branch-free (groups + eq_zero(groups))
so its body has no let-bound match and can @-inline into
read_sys_circuits_n (the match had tripped the inliner); also bind
verify_one_query's three identical heights_all calls once.
261 -> 185 combined for the vk record reader.
Total width 8697 -> 8520, circuits 158 -> 155, FFT cost at q=50
3.588e9 -> 3.583e9 (the dead sampler rows outweigh the new guards).
Regenerated aiur_multi_stark.rs.
A digest is 32 columns, so every digest crossing a circuit boundary -- input, call output, list node -- paid 32 where a pointer pays 1. Add DigestP = &Digest and thread it through the whole Merkle chain: the proof/commit-phase authentication paths and the caps deserialize as List<DigestP> (read_digest_vec_at_n / read_vk_cap_n store each digest), mmcs_compress and leaf_hash_at take/return pointers, and mmcs_fold's running node is a pointer. Bytes are loaded only where actually consumed: block assembly in mmcs_compress, the cap observation in cap_onto, and the root equality in mmcs_verify. digest_eq / b3_to_digest / mmcs_hash_row / digest_onto stay value-based, so the self-tests only wrap literals in store(). Aiur's store is content-addressed (execute.rs keys memory queries by value), so pointer identity == digest identity and the cross-query compress memoization is preserved (mmcs_compress cache hits unchanged at q=50). The indirection moves work into memory[32] (78 -> 8.7k rows), far cheaper than the width it removes: mmcs_fold 297 -> 49 at height 10.5k (its FFT share 5.8% -> 1.0%). Measured on bench-recursive-verifier --execute-only --use-bytecode (factorial(5)): total width 8520 -> 8166, circuits 155 -> 153, FFT cost at q=50 3.583e9 -> 3.426e9 (-4.4%). multi-stark self-tests and the recursive-verifier end-to-end suite (accept + codegen/interp parity + both tamper rejections) pass. Regenerated aiur_multi_stark.rs.
mmcs_verify compared the recomputed root against the cap entry by loading both digests (2x32 aux) into an 8-limb field comparison. With digests content-addressed (previous commit), pointer equality IS digest equality: the executor keys memory by value so equal digests share a pointer, and the memory argument binds one pointer to one value, so equal pointers imply equal digests. One eq_zero(ptr_val - ptr_val) -- the same pattern as the IxVM kernel's address equality. mmcs_verify 97 -> 22. ood_composition read the 8 logUp coordinate values (beta, gamma, acc_initial, acc_final) back out of the publics list it had just built -- 8 list_lookup calls for values already in hand as the challenge / accumulator ext elements. Take them as direct arguments (call args are free) and keep the publics list only for the node graph's Public(idx) leaves. ood_loop 285 -> 251. Measured on bench-recursive-verifier --execute-only --use-bytecode (factorial(5)): total width 8166 -> 8057, FFT cost at q=50 3.426e9 -> 3.423e9. Both test suites pass (accept + codegen/interp parity + both tamper rejections). Regenerated aiur_multi_stark.rs.
…lpers verify and ood_verify matched on the single-constructor Proof; rewrite as irrefutable let-destructures (the Sys/SysParams pattern) — one fewer matchContinue selector each in the spliced entrypoint. (Tried and rejected: making the entrypoint fully single-path for k=2 lookup grouping — enum destructures and Nil-assertions still lower through match ctrl, so the selector count stays > 1 and un-inlining opt_commit_cap to remove its two-arm match was a net loss; it stays spliced.) Inline-call the remaining single-site observation helpers: b3_flatten_onto (57 wide, one site in ch_sample8's flush arm) and digest_onto (49 wide, one site in cap_onto). read_node/read_preprocessed /prep_onto stay cross-circuit — the inliner rejects a callee whose body is leading lets + a tail match (the fresh-local wrap in Source.lean::expandOnce only handles a bare match core), which is worth fixing separately: ~75 width is stranded behind it. Measured on bench-recursive-verifier --execute-only --use-bytecode (factorial(5)): total width 8057 -> 7979, circuits 153 -> 151, FFT cost at q=50 unchanged (3.423e9). Both test suites pass. Regenerated aiur_multi_stark.rs.
prep_onto turned out to splice fine — the earlier batch's failure was read_node's alone (a bare-match body is safe; the inliner only rejects leading lets + a tail match whose result carries a multi-variant enum, minimized in the InlineRepro G3 case). read_node has exactly that shape (SysNode is multi-variant), so it is folded in by hand instead: read_nodes_n's arm reads the tag and runs the 16-way node match with the cons + recursion continuation duplicated into every arm — exclusive arms share aux/lookup columns (max, not sum), so the duplication is free and read_node's 49-wide circuit disappears (read_nodes_n 26 -> 59). read_preprocessed and read_opt_commit stay: their parents (read_proof / read_system) are themselves spliced into the entrypoint, and a tail match returning even a single-variant wrapper with a multi-variant field still trips the inliner (InlineRepro case I). Measured on bench-recursive-verifier --execute-only --use-bytecode (factorial(5)): total width 7979 -> 7951, circuits 151 -> 149. Both test suites pass. Regenerated aiur_multi_stark.rs.
The entrypoint carried the vk and claims Blake3 digests as 64 raw byte columns of public input. Pack 4 LE bytes per field element instead -- injective in Goldilocks (2^32 < p, unlike full 8-byte limbs) -- so each digest is 8 elements and the public input drops 64 -> 16 columns. The in-circuit side packs blake3's native 4-byte output words with pure wiring (b3_pack, always @-inlined); verifierPubInput is the recipe's single home and the tests now consume it instead of hand-building the byte-per-element form. NOTE: this changes the public-input wire format of verify_multi_stark_proof (any external caller must re-derive inputs via verifierPubInput). Measured on bench-recursive-verifier --execute-only --use-bytecode (factorial(5)): total width 7951 -> 7903 (entrypoint 782 -> 734). Both test suites pass. Regenerated aiur_multi_stark.rs.
The Fiat-Shamir claims segment (u64 count, then per claim a u64 length prefix and raw u64 values, all as 8 LE bytes) is byte-identical to the claims wire encoding: serializeClaims produces exactly what verify_multiple_claims observes, the entrypoint asserts the claims stream fully consumed, and the old claim_vals_onto observed the raw limbs unreduced -- so the equivalence is exact even for adversarial non-canonical bytes. Hand fiat_shamir the cbytes stream as the transcript tail instead of re-serializing the parsed claims, and drop claims_onto / claims_each_onto / claim_vals_onto along with the two list_length_u64 monomorphs only they used. Also observe the sampled lookup/fingerprint challenges back as one 16-byte segment concat each instead of two full-buffer snoc walks. Measured on bench-recursive-verifier --execute-only --use-bytecode (factorial(5)): total width 7903 -> 7784, circuits 149 -> 146. Both test suites pass. Regenerated aiur_multi_stark.rs.
ro_fold accumulated ro += ap * (p_z - p_x) * q per column, with q = 1/(zeta - x) constant across a matrix-point's columns, over a List<Goldilocks> that lanes_to_gl materialized (526k stores/loads at kernel scale) just for this walk. Two changes: - Take the raw wire lane list directly: limb_to_field is pure wiring, so the conversion pass, its circuit (28 wide), and its per-lane memory[3] nodes all disappear. - Accumulate the q-free sum s = sum(ap_i * (p_z_i - p_x_i)) and let bucket_update apply q once per matrix-point: one ext mul removed from the per-column loop (1.1M rows at kernel scale). Dropping q from ro_fold's arguments also uncovered memoization: calls now key on (rows, opened, alpha, ap) alone, and content-addressed stores give structurally equal opened rows the same pointer, so repeated openings hit the cache (ro_fold height 6935 -> 3433 at factorial q=50). Measured on bench-recursive-verifier --execute-only --use-bytecode (factorial(5)): total width 7784 -> 7752, circuits 146 -> 145, FFT cost at q=50 3.423e9 -> 3.408e9. Both test suites pass (ro_fold_test re-pinned against the reference with q applied outside). Regenerated aiur_multi_stark.rs.
Same packing as the recursive verifier's entrypoint: the claim digest enters verify_claim as 8 field elements of 4 packed LE bytes instead of 32 raw byte columns (-24 input columns on the production kernel system). run_claim needs the digest for exactly two things and both take the packed form freely: the ch-0 io key (keys are execution-side only -- io_get_info has no lookup, so key width costs nothing) and the blake3 binding, now an 8-word packed compare via b3_pack, which moves to the shared Blake3 module so both toplevels use one definition. verify_check / verify_const keep byte inputs: they store their input as a content-addressed Addr, where packing would force a byte decomposition; both are pruned from production anyway. The kernel's claim shrinks 32 -> 8 public values, which also shrinks what the recursive verifier hashes and fingerprints per claim. Key / input builders updated in lockstep: ClaimHarness.packedDigestKey (Lean), packed_digest_key in aiur_ixvm_witness.rs (Rust), VerifyCmd, bench-typecheck. Validated: bench-typecheck --execute-only Nat.add_comm (Rust witness builder + codegen'd kernel), kernel-tutorial (374 checks, Lean harness), multi-stark + recursive-verifier suites. Regenerated aiur_ixvm.rs + aiur_multi_stark.rs.
The kernelCheckEntries pins and the shard-pipeline pin predate this branch: the blake3 one-committed-row-per-round staging trades width for height, which raises the kernel's execution FFT ~0.1-7% per constant (blake3 is shared into the kernel toplevel), and the packed claim digest moves them a further ~0.001%. Bump all 79 pins + the shard pin to the measured values; the full --ignored ixvm suite (kernel checks, claim smokes, arena negatives, exploit corpus, codegen parity, shard pipeline) passes clean against them.
Formatter pass over the previous commit's addition, and u32::from instead of as-casts per clippy.
gabriel-barrett
force-pushed
the
blake3-minimization
branch
from
August 18, 2026 13:43
a60394e to
03b9661
Compare
Member
Author
|
!benchmark aiur-recursive fresh |
Member
Author
|
!benchmark recursive fresh |
|
| constant | 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) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
String.split |
34.103 s | 34.684 s | +1.7% | 101.97 GiB | 93.88 GiB | -7.9% (1.09× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 43.0 ms | 27.7 ms | -35.5% (1.55× faster) 🟢 | 5.702 s | 5.029 s | -11.8% (1.13× faster) 🟢 | 174.32B | 199.68B | +14.5% (1.15× more) |
16.341 s | 16.733 s | +2.4% | 11.40 MiB | 10.98 MiB | -3.7% 🟢 | 71.0 ms | 68.0 ms | -4.2% 🟢 | 33.47 GiB | 34.19 GiB | +2.2% |
Vector.append |
31.148 s | 32.074 s | +3.0% | 91.40 GiB | 87.50 GiB | -4.3% 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 39.2 ms | 26.0 ms | -33.7% (1.51× faster) 🟢 | 5.028 s | 4.219 s | -16.1% (1.19× faster) 🟢 | 155.07B | 168.90B | +8.9% (1.09× more) |
4.227 s | 4.243 s | +0.4% | 10.63 MiB | 10.21 MiB | -4.0% 🟢 | 66.6 ms | 62.4 ms | -6.3% (1.07× faster) 🟢 | 7.47 GiB | 6.85 GiB | -8.3% (1.09× smaller) 🟢 |
Nat.add_comm |
21.915 s | 21.372 s | -2.5% | 60.44 GiB | 57.49 GiB | -4.9% (1.05× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 32.2 ms | 25.3 ms | -21.6% (1.28× faster) 🟢 | 3.828 s | 3.241 s | -15.3% (1.18× faster) 🟢 | 117.10B | 123.53B | +5.5% (1.05× more) |
1.079 s | 1.094 s | +1.5% | 9.31 MiB | 8.90 MiB | -4.4% 🟢 | 58.2 ms | 53.8 ms | -7.4% (1.08× faster) 🟢 | 3.97 GiB | 3.79 GiB | -4.7% 🟢 |
|
| constant | 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) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
33.946 s | 37.038 s | +9.1% (1.09× slower) |
101.35 GiB | 93.87 GiB | -7.4% (1.08× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 43.8 ms | 25.5 ms | -41.6% (1.71× faster) 🟢 | 5.681 s | 4.989 s | -12.2% (1.14× faster) 🟢 | 175.42B | 198.88B | +13.4% (1.13× more) |
17.402 s | 17.514 s | +0.6% | 11.33 MiB | 10.91 MiB | -3.7% 🟢 |
String.split |
33.867 s | 35.540 s | +4.9% |
101.55 GiB | 94.04 GiB | -7.4% (1.08× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 47.0 ms | 25.3 ms | -46.2% (1.86× faster) 🟢 | 5.747 s | 5.036 s | -12.4% (1.14× faster) 🟢 | 174.32B | 199.68B | +14.5% (1.15× more) |
16.354 s | 17.088 s | +4.5% |
11.40 MiB | 10.98 MiB | -3.7% 🟢 |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
34.719 s | 34.268 s | -1.3% | 104.82 GiB | 94.28 GiB | -10.1% (1.11× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 33.4 ms | 26.4 ms | -20.9% (1.26× faster) 🟢 | 5.870 s | 5.022 s | -14.4% (1.17× faster) 🟢 | 183.37B | 201.90B | +10.1% (1.10× more) |
37.949 s | 37.512 s | -1.2% | 11.41 MiB | 10.99 MiB | -3.7% 🟢 |
Char.ofOrdinal_le_of_le |
34.589 s | 34.194 s | -1.1% | 103.77 GiB | 94.30 GiB | -9.1% (1.10× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 34.0 ms | 25.8 ms | -24.2% (1.32× faster) 🟢 | 5.916 s | 4.999 s | -15.5% (1.18× faster) 🟢 | 183.64B | 201.75B | +9.9% (1.10× more) |
27.360 s | 29.081 s | +6.3% (1.06× slower) |
11.42 MiB | 11.00 MiB | -3.7% 🟢 |
List.mergeSort |
34.809 s | 34.172 s | -1.8% | 102.78 GiB | 89.60 GiB | -12.8% (1.15× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 32.3 ms | 25.2 ms | -22.0% (1.28× faster) 🟢 | 5.681 s | 4.881 s | -14.1% (1.16× faster) 🟢 | 176.45B | 192.53B | +9.1% (1.09× more) |
12.670 s | 13.009 s | +2.7% | 11.36 MiB | 10.94 MiB | -3.7% 🟢 |
Vector.extract_append._proof_2 |
34.079 s | 33.342 s | -2.2% | 102.70 GiB | 88.26 GiB | -14.1% (1.16× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 38.7 ms | 29.1 ms | -24.8% (1.33× faster) 🟢 | 5.695 s | 4.907 s | -13.8% (1.16× faster) 🟢 | 177.37B | 190.81B | +7.6% (1.08× more) |
22.303 s | 22.848 s | +2.4% | 11.23 MiB | 10.81 MiB | -3.7% 🟢 |
Vector.append |
31.182 s | 33.115 s | +6.2% (1.06× slower) |
91.24 GiB | 87.52 GiB | -4.1% 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 37.1 ms | 28.5 ms | -23.1% (1.30× faster) 🟢 | 5.060 s | 4.246 s | -16.1% (1.19× faster) 🟢 | 155.07B | 168.90B | +8.9% (1.09× more) |
4.203 s | 4.283 s | +1.9% | 10.63 MiB | 10.21 MiB | -4.0% 🟢 |
Nat.gcd_comm |
30.855 s | 33.085 s | +7.2% (1.07× slower) |
90.65 GiB | 87.58 GiB | -3.4% 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 40.2 ms | 27.0 ms | -32.8% (1.49× faster) 🟢 | 5.020 s | 4.236 s | -15.6% (1.19× faster) 🟢 | 152.39B | 167.66B | +10.0% (1.10× more) |
3.284 s | 3.330 s | +1.4% | 10.54 MiB | 10.12 MiB | -4.0% 🟢 |
Int.gcd |
24.004 s | 32.925 s | +37.2% (1.37× slower) |
67.69 GiB | 87.50 GiB | +29.3% (1.29× larger) |
5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 37.2 ms | 27.3 ms | -26.7% (1.36× faster) 🟢 | 4.505 s | 3.950 s | -12.3% (1.14× faster) 🟢 | 142.13B | 158.91B | +11.8% (1.12× more) |
2.028 s | 2.117 s | +4.4% |
9.94 MiB | 9.52 MiB | -4.2% 🟢 |
Array.extract_append |
34.158 s | 32.570 s | -4.7% 🟢 | 103.41 GiB | 90.18 GiB | -12.8% (1.15× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 32.0 ms | 25.4 ms | -20.6% (1.26× faster) 🟢 | 5.800 s | 4.912 s | -15.3% (1.18× faster) 🟢 | 178.75B | 199.15B | +11.4% (1.11× more) |
38.922 s | 39.017 s | +0.2% | 11.36 MiB | 10.94 MiB | -3.7% 🟢 |
Nat.sub_le_of_le_add |
23.608 s | 32.164 s | +36.2% (1.36× slower) |
66.54 GiB | 87.53 GiB | +31.5% (1.32× larger) |
5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 32.0 ms | 24.8 ms | -22.6% (1.29× faster) 🟢 | 4.447 s | 3.886 s | -12.6% (1.14× faster) 🟢 | 138.97B | 157.47B | +13.3% (1.13× more) |
1.855 s | 1.892 s | +2.0% | 10.13 MiB | 9.71 MiB | -4.1% 🟢 |
String.append |
30.814 s | 31.363 s | +1.8% | 88.66 GiB | 87.51 GiB | -1.3% | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 39.4 ms | 25.6 ms | -35.0% (1.54× faster) 🟢 | 4.749 s | 3.944 s | -17.0% (1.20× faster) 🟢 | 145.74B | 160.06B | +9.8% (1.10× more) |
2.429 s | 2.405 s | -1.0% | 10.16 MiB | 9.74 MiB | -4.1% 🟢 |
Nat.add_comm |
21.799 s | 21.761 s | -0.2% | 60.77 GiB | 57.42 GiB | -5.5% (1.06× smaller) 🟢 | 5.27 MiB | 3.97 MiB | -24.7% (1.33× smaller) 🟢 | 32.4 ms | 25.6 ms | -20.8% (1.26× faster) 🟢 | 3.859 s | 3.192 s | -17.3% (1.21× faster) 🟢 | 117.10B | 123.53B | +5.5% (1.05× more) |
1.074 s | 1.069 s | -0.5% | 9.31 MiB | 8.90 MiB | -4.4% 🟢 |
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual |
OOM | OOM | n/a | OOM | OOM | n/a | OOM | OOM | n/a | OOM | OOM | n/a | OOM | OOM | n/a | OOM | OOM | n/a | OOM | OOM | n/a | OOM | OOM | n/a |
spin 0.9.8 -> 0.9.9 and 0.10.0 -> 0.10.1: both locked versions were yanked upstream, tripping cargo-deny's yanked check. h2 0.4.13 -> 0.4.16: RUSTSEC-2026-0258 (unbounded empty DATA frames, low severity, via iroh -> hickory). Only reachable with --all-features, which is what CI's cargo-deny-action runs — a plain `cargo deny check` stays green either way. Patch bumps only; aiur tests, clippy, fmt, deny (both invocations) green.
gabriel-barrett
force-pushed
the
blake3-minimization
branch
from
August 18, 2026 14:33
c2a2fdb to
ba50ad1
Compare
arthurpaulino
approved these changes
Aug 18, 2026
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 free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 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.
Summary
Reduce the width and FFT cost of the recursive verifier by restructuring BLAKE3 compression, removing unnecessary circuit boundaries, narrowing several verifier operations, and representing large values more efficiently across circuit boundaries.
For the measured
factorial(5)recursive-verifier workload, total circuit width decreases from 11,239 to 7,784 (30.7% reduction), while the circuit count decreases from 202 to 146.Main changes
Stage BLAKE3 compression across rows
Previously, all seven BLAKE3 rounds were unrolled into one wide, straight-line circuit. This PR changes
blake3_compressinto a staged recursive circuit:blake3_compress_initassembles the initial state and is always inlined.This changes the compression circuit from:
blake3_compress: 1,080 columnsblake3_compress_inner_j: 1,192 columnsto:
blake3_compress: 925 columnsThe tradeoff is additional height: 654 → 5,544 rows, in exchange for substantially lower width.
Measured end-to-end:
Inline single-use and pure-wiring helpers
Inline approximately 40 single-call-site functions across:
A dedicated circuit has fixed input, output, selector, quotient, and lookup-communication costs. For single-use branchless helpers, those costs provide no benefit.
This reduces:
Additional single-site helpers are subsequently inlined or folded into their callers, bringing the final circuit count to 146.
Narrow challenger sampling
ch_sample8now pops eight bytes directly and flushes at most once.ch_sample_bitsdecomposes only the low four sampled bytes.This removes unnecessary per-byte sampling and 64-bit decomposition work.
Compute the two-adic generator iteratively
Replace the 33-arm
two_adic_gentable with a memoized squaring chain starting from the maximal (2^{32}) generator:This reduces the corresponding circuit width from 73 to 17 columns.
Narrow verification-key deserialization
Together with the challenger and generator changes:
Thread Merkle digests by pointer
A digest occupies 32 columns when passed by value, while a pointer occupies one.
This PR introduces DigestP = &Digest and uses pointers throughout:
Digest bytes are loaded only where their contents are actually consumed.
Because Aiur memory is content-addressed, digest pointer identity is equivalent to digest value identity. Existing cross-query compression memoization is preserved.
Notably:
Compare Merkle roots by pointer
Since digest memory is content-addressed, the recomputed root can be checked against the cap entry using pointer equality instead of loading and comparing two 32-byte digests.
This reduces mmcs_verify from 97 to 22 columns.
Pass logUp values directly
ood_composition previously read eight logUp coordinate values back from the public-values list immediately after constructing it.
These values are now passed directly as arguments, while the list remains available for public-node lookups.
This reduces ood_loop from 285 to 251 columns.
Simplify proof and node deserialization
This removes additional single-use circuit boundaries while preserving the existing wire format.
Pack public digest inputs
The verifier previously exposed the verification-key and claims digests as 64 individual byte-valued public inputs.
This PR packs each group of four little-endian bytes into one field element. The packing is injective over Goldilocks because (2^{32} < p).
As a result:
Important
This changes the public-input wire format of verify_multi_stark_proof.
External callers should construct the new representation through
verifierPubInput.
Observe claims bytes directly
The serialized claims stream is already byte-identical to the corresponding Fiat–Shamir transcript segment.
Instead of parsing the claims and then serializing them again for observation, the verifier now observes the original claims bytes verbatim.
This also:
Final measured totals:
Benchmarking support
Add --interp to bench-typecheck, allowing execution through the generic Aiur bytecode interpreter.
This supports fast iteration on Ix/IxVM/*.lean without requiring IxVM code generation and a Rust rebuild after every change.
The option applies to:
FFT-cost measurements remain executor-independent. Execution-time measurements should not be compared directly between interpreter and generated-code modes.
Validation
The following were run across the commits in this PR:
Generated IxVM and multi-STARK Rust code has been updated.