Repository navigation
Faster single-thread aggregation: padding tails summed once, a live-prefix dense reduction, and four smaller prover changes - #501
Merged
tcoratger merged 35 commits intoOct 7, 2026
Conversation
- mul_lanes_avx512: the reduction's spill is one vpshufb lookup of the top
nibble and g(x) takes doublings, so fewer ops share the shift/shuffle
pipes with the unpacks (VPCLMULQDQ zmm issues every other cycle on Zen 4).
- radix-8 and radix-4 groups keep their rows in registers: each row is
loaded and stored once per group, not once per layer.
- run_layers puts the leftover one or two layers first (largest blocks)
and walks twiddles block to block with one XOR (TwiddleWalk) instead
of a subset sum per block; twiddles_radix8 is gone.
Byte-identical: fibonacci 2M rate 1 digest 87a8a891167e3b9a, leanxmss 400
744c5cfc65b1157d. cargo test --release -p pcs passes.
1T (LEANVM_NUM_THREADS=1, taskset -c 2), base / this, two runs each:
leanxmss 400: Commit 602, 601 -> 580, 572 ms; PCS open Commit L1-L4
380, 381 -> 349, 349 ms; Prove 5500, 5490 -> 5470, 5390 ms.
fibonacci 2M: Commit 1160, 1150 -> 1110 ms (other run disturbed, load 11);
L1-L4 798, 796 -> 746 ms.
Kernel probe, 48 lanes in L1: 0.343 -> 0.308 ns per lane-butterfly.
32T leanxmss 400: Commit 67.6, 66.9 -> 65.6, 71.7 ms (second run had every
stage slower, machine noise); proving unchanged within noise.
…s the lane-major stack in place - With one worker (gated on the planned worker count; 32 threads keep the old plan) a gathered group takes up to 64 adjacent residues: they share every twiddle, so the group is one transform of R*n lanes, its copies in and out are R*n-word runs (whole lines, so streaming stores stop splitting lines) and the 41- or 35-lane scalar tail disappears. LONE_GATHER_WORDS bounds the scratch (32 MiB). - encode_lane_major_with: commit no longer transposes the stack into the codeword. When the first gathered pass takes >= 8 residues, it reads each lane's 8-word lines straight from the lane-major message and turns 8x8 blocks around in registers (gather_lanes, AVX-512). Otherwise (32T, small domains, other targets) it transposes first as before. - transform_for takes the worker count, so tests pin the one-worker plan. Byte-identical (same digests). cargo test --release -p pcs passes; tests cover the lone plan for in-place, no-message and lane-major encodes. Measured together with the next commit (see there).
…ctor for 2-7 spare lanes
- gather_lanes walks one lane octet's lines front to back (8 lines per
lane per row group), which halves the lane-major read time at 1T.
- Rows ending in 2 to 7 lanes past a whole vector (fibonacci's 35 lanes)
take one masked vector in separate #[inline(never)] sweeps; folding the
mask into the common loop cost the whole-vector shapes about 5%.
Byte-identical: fibonacci 2M 87a8a891167e3b9a, leanxmss 400
744c5cfc65b1157d. cargo test --release -p pcs passes.
This and the previous two commits, 1T, base / this, A B A B:
leanxmss 400: Commit 606, 608 -> 484, 484 ms; L1-L4 378, 378 -> 360, 350;
Prove 5480, 5430 -> 5370, 5320 ms.
fibonacci 2M: Commit 1150, 1150 -> 835, 830 ms; L1-L4 795, 797 -> 731, 730;
Prove 9180, 9250 -> 8900, 8850 ms.
32T leanxmss 400 (--repeat 3): Commit 68.4, 67.5 -> 66.5, 67.3 ms; proving
0.556, 0.568 -> 0.559, 0.578 s (+-2 to 4% spreads): unchanged.
Probe (1T, xmss shape, commit alone): transpose 50 + gathered in 39 + out 50
ms became gathered in 45 + out 22 ms.
With one worker the deep pass takes fit3 rows whenever the plan has a
gathered pass: its L3 is its own, a deep layer costs about the same from
L3 as from L2, and the smaller gathered groups read the lane-major stack
faster. 32T planning is unchanged.
Probe (1T, encode + Merkle alone): leanxmss base commit 482 -> 459 ms,
its L1 extension commit 236 -> 231 ms, fibonacci's L1 493 -> 472 ms
(fibonacci's base commit already took fit3).
Byte-identical: fibonacci 2M 87a8a891167e3b9a, leanxmss 400
744c5cfc65b1157d. cargo test --release -p pcs passes.
All four commits, 1T, base / this, A B A B:
leanxmss 400: Commit 604, 607 -> 464, 523 ms (second run noisy);
L1-L4 378, 377 -> 342, 344 ms; Prove 5470, 5460 -> 5260, 5400 ms.
fibonacci 2M: Commit 1170, 1160 -> 837, 898 ms; L1-L4 794, 809 -> 706,
709 ms; Prove 10100 (disturbed), 9370 -> 8830, 8890 ms.
32T leanxmss 400: Commit 66.6, 71.4 -> 66.8, 68.7 ms; proving 0.558, 0.58
-> 0.572, 0.629 s (last run +-21.7%, load 6.8): no change beyond noise.
pcs throughput bench, 1T, PCS_LOG_N=22 (load 7 to 11): commit 47.9, 63.6
-> 43.0, 42.8 ms; encode alone 29.7, 33.7 -> 25.6, 24.7 ms.
…k circuits; HASH's unrolled ALU, LOAD, STORE, LD, SD and SHIFT (`ClassSpec::witness`) and every clock circuit (`Clock::witness`) now write their packed witness by word arithmetic instead of the 64-lane walk of their gate list. Each generator computes the circuit's values natively and writes its rows in the order the circuit makes its products through `rv::circuits::Products`, which keeps each table's current word in a register and stores it once full. ALU's 192 interleaved logic rows go through `Products::push_interleaved3` (BMI2 `pdep`, with a portable spread elsewhere). DIV, EXT, and MUL off AVX2 still walk. HASH's generator was already word arithmetic, but it ORed each carry run into the tables at a slot read from a table the circuit build recorded. It is now unrolled by a macro: every run's place is a constant, so the rows are written with no branch and no read, and the recorded runs (`CARRIES`) are gone. A run starts above bit 0 only on round 0's first `c + d` of a column G, whose `c` is still the IV. `class_flock::Prepared::build` still asserts that every output port of every instance is what the interpreter computed. Tests: `semantics::tests::word_witness_is_the_walk` checks ALU, LOAD, STORE, LD, SD and SHIFT on a grid of edge instances (every legal flag word; zero, one, all ones and the sign bits in every operand; every shift amount from 0 to 64 and all ones, with and without high bits; every byte offset of a cell, so every misalignment of every width; cells with every byte's sign bit set or clear) plus 4096 random ones (half decoder-shaped, half edge-biased words in every port, flags included). Each instance is compared alone with the bit-by-bit walk, then the whole batch's packed tables and lincheck stripes with the 64-lane walk. The clock's test covers every table's clock circuit and one with all 32 slots on 4096 rows (padding, first and last cycle, all ones, random; previous timestamps around the row's, live bit flipped, zero, all ones, random); HASH's covers all-zero, all-ones and sign-bit blocks and edge counters. Mutations (a dropped carry, a wrong fill bit, a wrong sign bit, the clock's top carry, a short HASH carry run) each fail their test. The portable spread is tested with target-cpu=x86-64-v2. Byte-identical proofs: serialized proof digests equal to the base's for leanxmss 400, fibonacci 2M and leanda 1 blob, at 1 and 32 threads. Measured on a Ryzen 9 7950X3D, shared host, base (77077c6) and this commit alternated, `--tracing`, loads 3.4 to 12.6: One thread (LEANVM_NUM_THREADS=1, taskset -c 2): leanxmss 400 Build flock witnesses 390, 398 -> 209, 212 ms proving 5.448, 5.475 -> 5.286, 5.298 s fibonacci 2M Build flock witnesses 571, 577 -> 297, 309 ms proving 9.191, 9.225 -> 8.961, 8.921 s leanda 1 blob Build flock witnesses 426, 425 -> 262, 261 ms proving 5.633, 5.670 -> 5.486, 5.508 s 32 threads: leanxmss 400 Build flock witnesses 47.4, 49.4 -> 47.2, 47.0 ms proving 0.558, 0.561 -> 0.588, 0.576 s fibonacci 2M Build flock witnesses 71.2, 71.4 -> 70.8, 69.1 ms proving 0.923, 0.923 -> 0.931, 0.947 s leanda 1 blob Build flock witnesses 52.4, 51.5 -> 50.2, 49.3 ms proving 0.601, 0.587 -> 0.600, 0.600 s At 32 threads the span and the proving totals stay within the run to run spread; `--repeat 3` runs at load under 10: leanxmss 0.557 to 0.566 s for the base and 0.559 to 0.601 s for this commit, fibonacci 0.906 to 0.942 s and 0.913 to 0.932 s.
…s committed column
The generators now take the destination for z (`Circuit::generate_witness_{from,with,batched}_into`, the allocating forms wrapping them through `witness::with_z`), and the driver shows each instance's z to a `check` closure while its group is still in the worker's scratch. `Prepared::build` passes the class's window of the committed stack as z and checks every output port against the interpreter there, so the second pass that reread z, checked the ports and copied z into the window is gone, and `Prepared` no longer keeps its own copy of z: `Prepared::prove` reads it from the stack.
Byte-identical proofs: serialized proof digests equal to the base's for leanxmss 400, fibonacci 2M and leanda 1 blob, at 1 and 32 threads. Tests: cargo test --release -p flock, the word-witness pins and leanvm_core's suite.
Measured on a Ryzen 9 7950X3D, shared host at load 3 to 12, the previous commit and this one alternated.
32 threads, --repeat 3, proving:
leanxmss 400 0.559, 0.564 -> 0.545, 0.545 s
fibonacci 2M 0.927, 0.926 -> 0.879, 0.882 s
leanda 1 blob 0.602, 0.607 -> 0.576, 0.587 s
32 threads, --tracing:
leanxmss 400 Build flock witnesses 49.4, 46.6 -> 26.6, 27.7 ms Flock reductions 122, 122 -> 117, 134 ms
fibonacci 2M Build flock witnesses 70.1, 69.5 -> 38.5, 39.3 ms Flock reductions 159, 166 -> 168, 164 ms
leanda 1 blob Build flock witnesses 50.3, 50.7 -> 31.6, 30.2 ms Flock reductions 116, 113 -> 118, 114 ms
One thread, --tracing (LEANVM_NUM_THREADS=1, taskset -c 2):
leanxmss 400 Build flock witnesses 211 -> 188 ms proving 5.265 -> 5.256 s
fibonacci 2M Build flock witnesses 290 -> 274 ms proving 8.910 -> 8.857 s
leanda 1 blob Build flock witnesses 261 -> 242 ms proving 5.518 -> 5.512 s
Peak memory: leanxmss 3.00 -> 2.75 GiB (32 threads), 2.91 -> 2.66 GiB (one); leanda 3.22 -> 2.95, 3.13 -> 2.86 GiB; fibonacci 4.70 -> 4.81, 4.67 -> 4.79 GiB.
The plan with wide gathered groups (up to 64 adjacent residues), the L3 deep pass and the lane-major stack read in place now runs whenever the transform is planned for at most FEW_WORKERS = 2 workers, not one alone. The tests plan for 1, 2 and 3 workers, so both sides of the gate are pinned to the scalar reference whatever the pool's size. Gate, measured on a Ryzen 9 7950X3D (workers pinned to the 32 MiB L3 CCD), Commit span of the base encode, one-worker gate / the plan at every count, two runs each: 2 workers (2 cores): leanxmss 400 307, 287 -> 281, 245 ms; leanda 305, 329 -> 263, 255 ms; fibonacci 2M 549 -> 467, 511 ms 4 workers (2 cores + SMT): leanxmss 220, 216 -> 232, 234 ms; fibonacci 406, 408 -> 455, 447 ms; leanda 235, 235 -> 238, 264 ms 4 workers (4 cores): leanxmss 148, 147 -> 164, 180 ms; leanda 157, 182 -> 193, 166 ms 8 workers (8 cores): leanxmss 92.5, 87.2 -> 132, 133 ms; leanda 116, 128 -> 141, 141 ms 32 workers, pcs throughput bench PCS_LOG_N=24 rate 1: commit 24.4, 24.0 -> 30.8, 30.9 ms; encode alone 16.5, 16.3 -> 24.6, 24.6 ms Three workers were not measured and keep the narrow plan. This branch against upstream 77077c6, Commit span (base encode), runs base -> this: 1 worker: leanxmss 601, 613, 613 -> 533, 472, 458 ms; fibonacci 1160, 1150, 1150 -> 846, 836, 850 ms; leanda 646, 663, 648 -> 484, 493, 497 ms 2 workers: leanxmss 279, 312, 312 -> 326, 260, 262 ms; fibonacci 550, 540, 540 -> 452, 461, 457 ms; leanda 335, 334, 336 -> 266, 281, 276 ms 4 workers (2 cores + SMT, the narrow plan): leanxmss 260, 259 -> 238, 238 ms; fibonacci 462, 473 -> 434, 429 ms; leanda 286, 257 -> 262, 260 ms 8 workers: leanxmss 92.7, 91.0 -> 90.3, 90.7 ms; fibonacci 171, 171 -> 163, 164 ms; leanda 98.7, 98.4 -> 99.2, 92.4 ms 32 workers: leanxmss 67.0, 67.3 -> 65.6, 64.9 ms; fibonacci 125, 120 -> 121, 119 ms; leanda 69.9, 71.3 -> 69.2, 69.9 ms Byte-identical proofs: leanxmss 400, fibonacci 2M and leanda 1 hash to the same digest on base and branch at every worker count. cargo test --release -p pcs passes, natively (AVX-512), with target-cpu=znver3 (the AVX2 arm) and on aarch64 under qemu.
…s and limb addresses
The stacked opening's lifted weight was filled twice per proof: once by the first pass (the Basis span) and again by the first lane fold (Sumcheck round 4), each fill paying the ring-switch map (apply_sliced_add), the point claims' eq tables and the scatter. On a pool of at most KEEP_WEIGHT_MAX_THREADS (4) workers the first pass now also streams each filled chunk into a dense buffer, and the first fold reads that back as Basis::Dense instead of filling it again. On a larger pool the refill, spread over the workers, costs less than writing the weight out and reading it back, so that path is unchanged. Proofs are byte-identical.
Measured on a 7950X3D, cargo leanvm aggregate --n 100 --leaves 4 --arity0 2 --arity 2 --repeat 3 --cooldown 1, AGG1_NOTREE, pooled per-pass medians (min) over alternating base/branch rounds, loads 1 to 12:
1T (5 rounds a side, taskset -c 2)
first-level node base 0.978 s (0.969) branch 0.960 s (0.954) -1.8%
node base 1.046 s (1.035) branch 1.025 s (1.018) -2.0%
32T (3 rounds a side, gate off)
first-level node base 0.148 s (0.144) branch 0.148 s (0.143)
node base 0.175 s (0.169) branch 0.174 s (0.169)
Spans at 1T (tracing, one pass): first-level node Basis 79.0 -> 89.1 ms, Sumcheck round 4 73.1 -> 43.9 ms, PCS open 289 -> 270 ms; node Basis 76.9 -> 89.2 ms, round 4 72.4 -> 43.8 ms, PCS open 292 -> 275 ms; leaf Basis 100 -> 113 ms, round 4 84.8 -> 47.6 ms.
Crossover (PCS open, store vs refill, tracing): 2T -9 and -6 ms, 4T -3 and -3 ms, 32T +5 to +7 ms, which sets the gate at 4.
Peak memory at 1T grows by the kept weight (24 bytes per committed word): aggregate 1.02 -> 1.31 GiB, leanxmss --n 100 0.83 -> 1.08 GiB. leanxmss --n 100 at 1T: 1.002 -> 0.986 s (pooled per-pass medians, 3 rounds a side).
A high-rate encode of a short message (the last WHIR level: 4 message rows, rate 2^13) cut its deep pass into one task per 4-row sub-block, so the Merkle builder got 4 leaves per call, short of a hash batch, and hashed them one by one. A task now runs 2^MIN_TASK_LOG rows of contiguous sub-blocks and hands them over at once. The rows, the codeword and the tree are unchanged. Measured on the 7950X3D (aggregate --n 100 --leaves 4, 2 alternating rounds, --repeat 3, load under 10), upstream f774828 vs this: - level-4 extension commit at 1T: 21.3 ms -> 3.4 ms (span tree) - 1T first-level node 972 -> 955 ms, node 1039 -> 1019 ms, leanXMSS-100 leaf 1011 -> 994 ms - 32T first-level node 152 -> 145 ms, node 174 -> 170 ms Proof digests unchanged (leaf, first-level node, node).
Tree::new already builds each circuit's fixed columns. Proving a node (prove_rows) and reading a child (read, which prove_node calls for every child and verify calls for the root) built them again through TableArgument::of, a serial pass over every slot of every table. They now take the tree's columns (Circuit::prove_with, Circuit::verify_to_raw_with); Circuit::prove and verify_to_raw still build their own. Measured on the 7950X3D, upstream f774828 vs this, aggregate --n 100: - sampled profile at 1T: FixedColumns::of is 0.51% of a first-level node proof (about 5 ms) and 1.19% of a node proof (about 12 ms: the prover's build and one per child read) - 32T, 2 alternating rounds: node 174/180 -> 167/170 ms; first-level node 152/149 -> 145/152 ms (within noise) - 1T end to end is within the run-to-run noise of these rounds (host load 4 to 13) Proof digests unchanged (leaf, first-level node, node).
On top of leanEthereum#463's generate_witness_with_into: HashBatch writes z into the stack's packed-witness window and copies each live row's 18 port words into the port buffers while the row is in cache (the padding rows' ports are one fill afterwards), so the 2^15-instance z (64 MiB) is neither allocated nor copied into the stack, and the ports are no longer gathered by 18 strided passes over it. The flock reduction reads z from the stack. Measured on the 7950X3D, leanEthereum#463 (ddbef89) vs this, aggregate --n 100, 1T: - Build witness span 43.3/43.4 -> 38.0/38.6 ms (first-level node and node, 2 traced runs each) - end to end at 1T within noise (load 2 to 12); 32T first-level node 155/152 -> 139/153 ms, node 172/188 -> 166/185 ms Proof digests unchanged (leaf, first-level node, node).
…ghts, fused rounds The node's dense reduction was a degree-two sumcheck over the whole fixed polynomial (2^22 entries) against a full weight table, each round a products pass and two fold passes. Prover only; the transcript, the verifier and every proof byte are unchanged. - Live prefix. The weight table is zero past the blocks its terms touch (about 1.45M of the node's 4.2M entries), so every round folds and sums that prefix alone. Where the prefix's last entry pairs with one past it, that entry is the polynomial's value on its block at the challenges so far, an `mle_eval_par` of the table as given; those blocks partition the rest of the table, so the final value is still exact. - Factored weights. Terms of one block sharing their low coordinates are one group (each of the node's blocks has two terms at one point, so one group). While every block has at most two groups, the weight table is never written out: a round sums each block's low table against the table's run, then scales by the high entry, until the low tables are bound (10 rounds); then it is written out once at that level and folded from there. Otherwise (the first level's bytecode, 18 groups) it is written out at the start, in one pass with the first message. - Fused rounds. Each round folds the table (and the weights once written) tile by tile and builds the next round's message from the folded tile in L1, with `mul4`, `mul_base8` and unreduced `mul_unreduced4` sums reduced once per message. - The matrix reduction's row and column rounds fold and build the next message in one pass the same way (`FoldTable::fold_pair`). - `round(i)` is now `message()`, the message the last bind built. A new test reduces claims whose blocks leave a prefix odd at several rounds, with factored and written-out parts, and checks the verifier accepts and the values are the polynomials'. Measured on the 7950X3D, `aggregate --n 100 --leaves 4 --arity0 2 --arity 2 --repeat 3`, AGG1_NOTREE, alternating base (f774828) and branch runs; "proving" means of 3 passes, runs with 1-minute load above 20 or a disturbed pass dropped (loads in parentheses). 1T (taskset -c 2): - first-level node: base 0.973 s (9.1), 0.991 s (6.5), 0.972 s (9.9), median 0.973 s; branch 0.971 s (13.7), 0.958 s (10.7), median 0.965 s - node: base 1.042 s (9.1), 1.052 s (6.5), 1.039 s (9.9), median 1.042 s; branch 0.993 s (13.7), 0.975 s (10.7), and per-pass medians 0.990 s, 0.980 s of two runs with one disturbed pass each, median 0.985 s (-5.5%) 32T: - first-level node: base 0.149 s (9.6), 0.153 s (11.6), 0.160 s (13.7), median 0.153 s; branch 0.149 s (10.8), 0.149 s (10.1), 0.158 s (13.7), median 0.149 s - node: base 0.176 s (9.6), 0.203 s (11.6), 0.192 s (13.7), median 0.192 s; branch 0.156 s (10.8), 0.155 s (10.1), 0.169 s (13.7), median 0.156 s Spans (--tracing, one pass), base then branch: - 1T first-level: Reduce claims 25.7 to 13.2 ms (Dense reduction 17.2 to 5.25 ms, Matrix reduction 8.55 to 7.90 ms) - 1T node: Reduce claims 85.4 to 25.4 ms (Dense reduction 70.7 to 12.0 ms, Matrix reduction 14.7 to 13.3 ms) - 32T first-level: Reduce claims 8.99 to 6.33 ms (Dense reduction 2.61 to 0.99 ms) - 32T node: Reduce claims 35.1 to 12.9 ms (Dense reduction 25.6 to 4.53 ms, Matrix reduction 9.47 to 8.35 ms) Digests equal base at --n 100 (leaf 1ddc4572a71ec2af, first 6cc4ab4bf8ee46b7, node d0d2b1643bb63a90) and --n 400 (leaf 9311cba19de1b111, first cac5d72e17c200f1, node bc70f47ff4643d4b).
A batch padded to a power of two ends in copies of one padding instance: the recursion machine's HASH table (about 20k to 23k live rows of 2^15) and every RISC-V table's fill rows. The zerocheck binds the lowest variables first, so while it binds bits inside an instance (or inside a group of instances), every group past the live ones has the same per-round polynomial and the same folded tables. The prover now sums the head (the live instances, rounded up to the kernel's unit of work) as before, sums the cube's last group once, and adds it weighted by the tail's eq mass, sum_{g >= head} eq(r_groups, g), which is one plus the mass below the head and costs O(log) products. Field arithmetic is exact, so every message is unchanged and the proof bytes are identical.
- `PaddingSpec::live_blocks` and `PaddingSpec::tail` split a kernel's cube at the tail; a group is a block, or enough whole blocks for the kernel's smallest cube, so small circuits and rounds that bind instance bits split too.
- Round 1 (univariate skip), the paired bit passes, the storing bit pass and the paired table passes take the split; the storing and table passes write the last group in place and copy it over the tail, so the stored tables stay whole and the single-round tail is untouched.
- `reduction::Instance::live` carries the count; `HashBatch` sets it to its row count, and `class_flock::prove_reductions` detects each RISC-V batch's tail from its packed `z` (`reduction::live_instances`). The verifier and the proof are unchanged.
- Test: `an_identical_tail_changes_no_word` pins the proof stream and claims of a batch told of its tail to the one not told, with random live instances and identical tails starting at block 0, mid step, mid task and past every step, over shapes reaching every kernel (both table-pass arities included).
Measured on the 7950X3D, `aggregate --n 100 --leaves 4 --arity0 2 --arity 2 --repeat 3 --cooldown 1` with AGG1_NOTREE=1, proving time (mean of 3 passes), base f774828:
| node kind, threads | base runs | branch runs | median change |
| ------------------- | ---------------- | ----------------------- | ------------- |
| first-level, 1T | 0.971, 0.974 s | 0.907, 0.900, 0.902 s | -7.2% |
| node, 1T | 1.041, 1.041 s | 0.952, 0.952, 0.951 s | -8.5% |
| first-level, 32T | 0.150, 0.147 s | 0.144, 0.143 s | -3% (noise) |
| node, 32T | 0.174, 0.175 s | 0.173, 0.171 s | -1.5% (noise) |
Spreads 0.1% to 2.2% at 1T, 1.4% to 4.7% at 32T; loads 2.7 to 4.9 at start. An earlier pair of 1T rounds at loads 1 to 5 gave base 0.973, 0.977 / 1.038, 1.043 s.
Span tree, 1T, one tracing pass each: first-level Flock reduction 249 -> 170 ms (Round 1 91.8 -> 57.9, Rounds 149 -> 104, Lincheck 8.6 unchanged), node 237 -> 147 ms (Round 1 79.4 -> 50.4, Rounds 149 -> 88.1). HASH holds 22,871 (first-level) and 19,665 (node) live rows of 32,768.
Leaf, `leanxmss --n 100 --repeat 3 --cooldown 1`: 1T base 1.009, 1.041, 0.999 s, branch 0.989, 0.973, 0.971 s (clean pair 0.999 -> 0.971, -2.8%); 32T base 0.141, 0.145 s, branch 0.144, 0.143 s. Its Flock reductions span 250 -> 222 ms at 1T.
Digests unchanged at n = 100 (leaf 1ddc4572a71ec2af, first 6cc4ab4bf8ee46b7, node d0d2b1643bb63a90) and n = 400 (leaf 9311cba19de1b111, first cac5d72e17c200f1, node bc70f47ff4643d4b).
# Conflicts: # crates/flock/src/zerocheck.rs # crates/flock/src/zerocheck/multilinear.rs
# Conflicts: # crates/leanvm_core/src/class_flock.rs
# Conflicts: # crates/pcs/src/ntt/additive_ntt_f64.rs
# Conflicts: # crates/leanvm_core/src/rec/proof.rs
Collaborator
Author
|
Opening this to mainly collect a bunch of different unmerged optimisations to see their diff. (Some of them in isolation only give a marginal change) On my server, I get numbers so also want to see if they are reproducible on the github CI |
Collaborator
Author
|
Also not clear we want all or any of these |
Benchmarks: base against this PR, on one runnerdc24a75 merged into its base, against the base 556206d: each benchmark run in turns on one runner, base and PR 5 times each. A size is shown when it changed; a time or a peak memory when it moved the same way in every round and its median by at least 1% (the change is the median ratio, with the rounds' range). Proving time
Prover stages
Verifying time
Peak memory
allocations
heap-peak
Every resultProving time
Prover stages
Verifying time
Time per operation
Proof size
Peak memory
allocations
heap-peak
|
) Upstream's one reduction API (leanEthereum#512) owns each batch's witness in `Instance`; leanEthereum#463 and the hash witness change write `z` straight into the committed column, and padskip adds the batch's live instances. The merged `Instance` borrows `z`, `A·z`, `B·z` and the stripes and carries `live`; `Instance::new` takes a `z` held apart (the committed column) and the rest as `flock::Tables`, `Instance::of` a whole `Witness`, both reading the tail off `z`. The `_into` generators return `Tables`. The prover keeps each class batch's `Tables` and the hash rows' `HashBatch` between the commit and the reduction, as `Prepared` and `HashBatch` did. `Fill` takes leanEthereum#463's word-level generators (`Fill::Instance` for ALU, LOAD, STORE, LD, SD, SHIFT); the clock circuits keep theirs. The NTT's lane butterflies keep leanEthereum#464's register kernels and gain the transposed butterfly upstream added, in registers.
# Conflicts: # crates/leanvm_core/src/class_flock.rs
# Conflicts: # crates/flock/src/reduction.rs # crates/leanvm_core/src/class_flock.rs # crates/leanvm_core/src/rec/proof.rs
PR 464 (the commit NTT plan for few workers) is open on its own, so this branch no longer carries it. Its three files go back to upstream's versions: pcs/src/ntt/additive_ntt_f64.rs, pcs/src/ntt.rs and pcs/src/whir/commit.rs. That also drops the AVX-512 register kernels, including the register version of upstream's transposed butterfly, which belonged to PR 464's register path. The deep-task sizing of kw/agg1-ntt-tasks goes back onto upstream's AdditiveNttF64::transform as it was first written: a deep task takes 2^MIN_TASK_LOG (64) rows of contiguous sub-blocks and hands them to the row sink at once. The codeword and the tree are unchanged. Nothing else in this branch used PR 464.
Collaborator
Author
|
@tcoratger do you think this is worth it? |
tcoratger
approved these changes
Oct 7, 2026
Collaborator
Yes this is definitely important in my opinion, just merged :) |
This was referenced Oct 7, 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.
#463 (word-level witnesses) is merged upstream now, so its part comes from the base. This PR's own changes are the six prover changes below, each also published as a branch of its own. A related open PR, #464 (the commit NTT plan for few workers), changes the same NTT function as section 3. This branch no longer contains it (
dc24a752took it out); whichever of the two lands second merges the other.Every change is prover-only: the verifier, the transcript and the proofs are unchanged, byte for byte.
The base now includes #523 (leaves at rate 1/4, a two-scalar transcript step, stratified WHIR queries), so this PR is #501 on top of #523. Measured locally (Ryzen 9 7950X3D) on that same combination, while this branch still contained #464 and before #518 to #521 landed, against upstream before #523 (
468c67cd), the aggregator time per leaf of a 2-to-1 tree over leanXMSS-400 leaves falls by 46% at 32 threads (0.168 to 0.091 s) and by 56% at one thread (0.969 to 0.425 s); #523 alone gives -30% and -43%, so these changes take another 23% off on top of it at both thread counts. The 4-to-1 tree at 32 threads falls by 44% (0.098 to 0.055 s per leaf).Where single-thread aggregation spends its time
A 2-to-1 aggregation node (
cargo leanvm aggregate --n 100 --leaves 4 --arity0 2 --arity 2, the shape CI tracks asaggregate-leanxmss-100-2to1and-1thread) proves one recursion proof over two children: the first-level node verifies two leanXMSS RISC-V proofs in rows, the node two first-level recursion proofs. Both have the same circuit heights (EMUL 2^17, EXK 2^16, HASH 2^15, CAST 2^13, SPLIT and PUB 2^10; 10.16M committed words).On one thread, upstream at
f774828dtook 974 ms for the first-level node and 1041 ms for the node. The recursion proof is 95% of it (about 911 ms):f774828d)#463 and #465 (both merged since) and #464 (open, a separate PR) take the witness, the base commit, the bus and the constraints. They leave the HASH zerocheck, the opening and the node's claim reduction as they are; the changes here go after those, plus two smaller leftovers.
1. The zerocheck sums a batch's identical padding tail once
Branch
kw/agg1-padskip(7a88b966, onf774828d).flock::reduction::Instancegainslive, the instances before the identical tail. The zerocheck kernels (Round 1's univariate skip, the paired and storing bit passes, the paired table passes) sum the live head as before, run once on the last group, and add it weighted by the tail's eq mass, which is one plus the mass below the head (a logarithmic number of products). The storing passes copy the last group over the tail, so later rounds see whole tables.HashBatchsetsliveto its row count;class_flock::prove_reductionsfinds each RISC-V batch's tail in its committedz(reduction::live_instances).livecontributes the same polynomial times its eq weight, so their sum is the last group's polynomial times the sum of their eq weights. The folded tables of identical groups are identical, so copying the last one gives the tables the full pass would write. A new flock test pins the proof of a batch told of its tail to one not told, with tails at block, step and task boundaries, mid-block, past every step, and at block 0.f774828d: first-level node 973 to 902 ms (-7.2%), node 1041 to 952 ms (-8.5%); the flock reduction 249 to 170 ms and 237 to 147 ms. The leanXMSS 100 leaf 0.999 to 0.971 s. At 32 threads within noise (the zerocheck span 17.4 to 13.5 ms).2. The tree's dense claim reduction runs over the live prefix, with factored weights and fused rounds
Branch
kw/agg1-densefuse(0d2c7e0f, onf774828d).mle_eval_parof the table). Terms of a block that share their low coordinates form a group; with at most two groups per block the weights stay factored (a low eq table times a high entry) for the first rounds and are never written out at full size. Each round folds tile by tile and builds the next message from the folded tile while it is in L1. The matrix reduction's rounds fold and build their message in one pass too.f774828d: Reduce claims 25.7 to 13.2 ms (first-level node) and 85.4 to 25.4 ms (node); node 1042 to 985 ms (-5.5%), first-level node 973 to 965 ms. At 32T, Reduce claims 9.0 to 6.3 ms and 35.1 to 12.9 ms.3. A deep NTT task covers at least 64 rows
Branch
kw/agg1-ntt-tasks(b4af9163, onf774828d).AdditiveNttF64::transformgives each deep task2^MIN_TASK_LOG(64) rows of contiguous sub-blocks and hands them to the Merkle builder at once. Only encodes whose deep sub-blocks hold fewer than 64 rows change: in leanXMSS 100 that is the last WHIR level (4-row sub-blocks, now 16 to a task), while the base commit's sub-blocks hold 2^10 rows and run as in the base.f774828d: the level-4 commit 21.3 to 3.4 ms; first-level node 972 to 955 ms, node 1039 to 1019 ms; the leanXMSS 100 leaf 1011 to 994 ms (its last WHIR level has the same shape). At 32T, first-level node 152 to 145 ms, node 174 to 170 ms.transform; it adds theMessageenum (rows or lanes) and its few-worker plan. This branch carries this change on upstream's NTT alone. The two compose: the grouped deep pass matches on pcs: a cheaper commit NTT plan when few workers run #464'sMessage::Rows, and a lane-major message never reaches the deep pass. Whichever of the two lands second takes that resolution.4. Small pools keep the opening's weight from its first pass
Branch
kw/agg1-openweight(21cc3b39, onf774828d).KEEP_WEIGHT_MAX_THREADS), the first pass also writes each filled chunk into a dense buffer, which the first fold reads asBasis::Dense. Larger pools keep refilling, which is cheaper there (2T -9/-6 ms, 4T -3/-3 ms, 32T +5 to +7 ms when kept).f774828d: first pass 79 to 89 ms, first lane fold 73 to 44 ms, PCS open 289 to 270 ms; first-level node 978 to 960 ms, node 1046 to 1025 ms; the leanXMSS 100 leaf 1.002 to 0.986 s. 32T unchanged (the gate is off).5. A tree proves and reads with the fixed columns it built once
Branch
kw/agg1-fixed(7e875365, onf774828d).Tree::newalready builds each circuit's fixed columns, butCircuit::proveandverify_to_raw(once per child inprove_node) rebuilt them, a serial pass over every slot of every table.Circuit::prove_withandCircuit::verify_to_raw_withtake the tree's columns;Circuit::proveandverify_to_rawkeep building their own.f774828d:FixedColumns::ofwas 0.5% of a first-level node's proof and 1.2% of a node's in a sampled profile (about 5 and 12 ms at 1T); end to end at 1T inside run-to-run noise. At 32T, where the pass is serial, the node 174/180 to 167/170 ms.6. The HASH rows' packed witness is generated straight into the stack
Branch
kw/agg1-hashwit(af9403dc, on #463 atddbef89c).RecWitness::buildallocated the 2^15-instancez(64 MiB), copied it into the stack's packed-witness window, then gathered the 18 port columns by 18 strided passes over it.generate_witness_with_into,zis written into the stack window and each live row's port words are copied while the row is in cache (through thecheckcallback; the padding rows' ports are one fill afterwards). The flock reduction readszfrom the stack. In this branch the ports go into their own buffers, as upstream keeps them since primitives: write unwritten buffers through MaybeUninit slots, and hash the digest's words as little-endian #485.hash, and the padding row (outsidehash) is skipped by the callback and filled after.Combined result
Measured in the study on
f774828dwith the six changes plus #463, #464 and #465 (one thread, quiet host, medians of 3 alternating rounds of--repeat 3):--n 100f774828dThat is -30% on the first-level node and -35% on the node at one thread, and the same at 400 signatures (first-level node 974 to 700 ms, node 1043 to 678 ms). The changes' gains add up: the five without #463/#464/#465 took the first-level node to 857 ms and the node to 844 ms.
CI's bench comment on
dc24a752(this branch merged into its base, against the base556206d7, which includes #463 and #523, so these numbers measure the six changes alone; base and PR run in turns on one runner, 5 rounds each, medians with the rounds' range):x86-64 (AMD EPYC 7763)
arm64 (Neoverse-N2)
12b931df, which contained pcs: a cheaper commit NTT plan when few workers run #464 (same bench, each against its own base run): the x86-64 single-thread cases lose the most. On x86-64 the 2-to-1 single-thread first-level node goes from -16.42% to -13.92% and its node from -18.72% to -15.11% (those two ran on an Intel Xeon Platinum 8573C before and an EPYC 7763 now); on an EPYC 7763 both times, leanxmss-100-1thread goes from -11.53% to -10.27%, its commit stage from -5.33% to +1.73% against the base, and the 4-to-1 nodes from -16.11%/-16.41% to -15.35%/-15.78%. On arm64 the 2-to-1 single-thread nodes go from -18.18%/-19.12% to -17.80%/-18.44%, leanxmss-100-1thread from -13.67% to -15.19%, and its commit stage from -2.50% to -0.11%. The multi-thread aggregation and leanXMSS cases move by less than 1.8 points either way.heap-peakfell on the aggregation cases (10.3% on x86-64, 4.35% on arm64). The kept opening weight (section 4) is the change that adds a buffer, on pools of at most 4 workers; see its memory trade.allocationsrose by 4.2% on the 2-to-1 node, 2.15% on the 4-to-1 node, and 1.05% to 3.1% on the RISC-V proving cases.#464 taken out
dc24a752takes #464 out of this branch.pcs/src/ntt/additive_ntt_f64.rs,pcs/src/ntt.rsandpcs/src/whir/commit.rs, the only files #464 changes, are upstream's at556206d7again. That also drops #464's AVX-512 register kernels, with the register version of upstream's transposed butterfly an earlier merge had added for them. Section 3's deep-task grouping is applied again onto upstream'stransform, as it was first written onf774828d(the patch applies unchanged). Nothing else in the branch used #464.Fitting the current upstream
This branch merges
riscv-explorationat556206d7with plain merge commits:c4997182(upstream atc0a6aab3),57ecea24(4189283c) and12b931df(556206d7);dc24a752then takes #464 out (above). Upstream since the earlier merges:Instanceborrowingz,flock::Tables, the_intogenerators,FlockId::tablesandFlockId::instance, the recursion's hash batch as aWitness). The merge's three conflicts are the six changes' own lines against their absence: inflock/src/reduction.rsandleanvm_core/src/class_flock.rs, the padding tail'sliveonInstance(section 1) and its doc lines; inleanvm_core/src/rec/proof.rs,HashBatch, which writeszinto the stack window and the ports while each row is in cache (section 6), against upstream's copy of aWitness. Each keeps this branch's side, and the merged tree is the same as57ecea24's.TableArgument::verify_core, andverify_to_raw_withhands it the tree's prebuilt fixed columns (section 5) rather than building them again. The prover still pairsFlockId::ALLwith its reductions incpu/program.rs, so that file keeps theFlockIdimport that upstream's verifier no longer needs. The test of the reduction in both verifiers takes upstream's stage checks over this branch's owned batches (Instance::ofborrows each batch's witness).flock/src/zerocheck/round1.rs, where upstream also dropped thek_skipargument; the tail's recursive call follows, and the kernel no longer needs itstoo_many_argumentsexception. The GF(2^8) NTT moved frompcs::ntttoflock::zerocheck::nttuntouched;pcs::nttis upstream's since pcs: a cheaper commit NTT plan when few workers run #464 is out. The kept weight (section 4) stays inpcs/src/whir/sumcheck.rsandstack_open.rs, which no longer importsBasis; the fused matrix rounds (section 2) takeSkipDomainfrom its new home inflock::zerocheck.shielded-258case runs the changes too.class_flockdrops itsLOG_PACKINGimport.Merge with current upstream (earlier)
The prototypes were built on
f774828d; an earlier merge broughtriscv-explorationat72ea1121(after #465, #498, #493, #491, #492, #485 and others), then #463, #464 andkw/agg1-hashwit, with plain merge commits.kw/agg1-padskipagainst primitives: write unwritten buffers through MaybeUninit slots, and hash the digest's words as little-endian #485: the bit pass's storing kernel and the paired table pass now writeMaybeUninitslots (Box::new_uninit_slice, the ping-pong scratch's spare capacity), and the tail's last-group copy works on those slots after the recursive pass on the last group has written them.kw/agg1-densefuseandkw/agg1-openweightagainst primitives: write unwritten buffers through MaybeUninit slots, and hash the digest's words as little-endian #485: their two buffers written before being read (the dense reduction's weight and table buffers, the kept opening weight) moved fromuninit_vecto spare capacity throughprimitives::write_onlyand toBox::new_uninit_slice, set to their length only after the pass.kw/agg1-padskipagainst leanvm_core: word-level witnesses for the ALU, memory, shift and clock circuits #463:prove_reductionstakes each batch'szfrom its committed column and finds the tail there.kw/agg1-ntt-tasksagainst pcs: a cheaper commit NTT plan when few workers run #464: the grouped deep pass matched on pcs: a cheaper commit NTT plan when few workers run #464'sMessage::Rows(gone with pcs: a cheaper commit NTT plan when few workers run #464 sincedc24a752).kw/agg1-hashwitagainst leanvm_core: word-level witnesses for the ALU, memory, shift and clock circuits #463's current head and primitives: write unwritten buffers through MaybeUninit slots, and hash the digest's words as little-endian #485: the ports are their ownMaybeUninitbuffers rather than stack windows, andHashBatchkeepslivefor the padding tail.A later merge brought upstream to
468c67cd(#503 to #517). Upstream's flockInstanceowns its witness, while #463 and section 6 writezstraight into the committed column: the mergedInstanceborrowszand carrieslive, and a newflock::Tablesholds the rest of a witness. #463's word-level generators plug into upstream'sFill. #464's AVX-512 NTT register kernels stayed then, with a register version of upstream's transposed butterfly (both gone with #464 sincedc24a752).Circuit::proveandverify_to_raware test-only now.Checks
dc24a752and of upstream at556206d7are identical for leanXMSS 400 and 100, Fibonacci 2M at--log-inv-rate 1, leanDA 1, andcargo leanvm aggregate --n 100 --leaves 4 --arity0 2 --arity 2(the leaf at rate 1/4, the first-level node and the node), at 1 and 32 workers, built natively (Zen 4, AVX-512) and with-C target-cpu=haswell. Earlier heads matched upstream the same way (12b931dfagainst556206d7, also at--n 400;57ecea24against4189283c;c4997182againstc0a6aab3).dc24a752:cargo test --release -p pcs(43 tests) natively, with each of CI's SIMD flag sets (x86-64-v3with+gfni,+vpclmulqdq,+pclmulqdq,+aes,x86-64-v3with+vpclmulqdq,+pclmulqdq), withhaswell, and for aarch64 (neoverse-n2with+aes,+sha3) underqemu-aarch64-static;cargo test --release -p leanvm_core --lib(203 tests) and-p flock -p primitives -p fiat_shamir(103 tests) natively.cargo test --release -p leanvm_core --test verifiers: 29 passed, 3 ignored (the same#[ignore]tests as upstream).cargo fmt --all --check;cargo clippyallwith haswell flags on Rust 1.97 and 1.99 and natively on 1.99; the AVX-512 clippy step and the ARM64 clippy leg (neoverse-n2,--target aarch64-unknown-linux-gnu);cargo docall.dc24a752: every job passed,cargo testallincluded.