[kevaundray]

This PR collects twelve prover-only optimisation ideas, one commit each, for review: the constraint sumcheck, the bus GKR and its leaves, the Keccak reduction's kernels, the NTT and WHIR commits, and witness generation (execute, hints, column fill). It is not meant to be merged as is; pick or discuss individual commits. Proof bytes do not change: the PROOFDIGEST of every benchmark below equals main's, and proof size and committed words are unchanged.

Results

This branch against current main (e5d75f858), per proving pass, ab.sh 3 rounds x 4 repeats (recursion also 5 x 4):

Benchmark	Wall median, main -> PR	Wall min, main -> PR	CPU median, main -> PR	Peak memory, main -> PR
aggregate --xmss 900 --log-inv-rate 1	1.704 -> 1.166 s	0.952 -> 0.843 s	9.80 -> 8.53 s (-13%)	3.21 -> 2.77 GiB
aggregate --sphincs 410 --log-inv-rate 1	2.178 -> 2.210 s	1.758 -> 1.386 s	16.96 -> 16.25 s (-4%)	4.21 -> 4.46 GiB
recursion --n 2 --xmss-per-leaf 900 --log-inv-rate 2, 3 x 4	0.738 -> 0.846 s	0.429 -> 0.569 s	2.80 -> 2.86 s	1.64 -> 1.53 GiB
same, 5 x 4	0.717 -> 0.615 s	0.356 -> 0.360 s	3.00 -> 2.82 s (-6%)

Proof size is unchanged (322.8, 331.8 and 233.4 KiB), as are the table sizes and TOTAL_COMMITTED (2^25.418, 2^26.326, 2^23.845). Peak memory is the CLI's peak memory with --repeat 2, the median of three or four runs each.

Per-stage process CPU, spancpu.sh median, main -> PR. xmss 900 in two separate runs (5 and 8 interleaved rounds), recursion in one (5 rounds):

Stage	xmss 900, 5 rounds	xmss 900, 8 rounds	recursion, 5 rounds
Constraint sumcheck (Prove constraints minus Constraint evals)	0.428 -> 0.407 s	0.462 -> 0.421 s	0.215 -> 0.170 s
Prove bus > Bus GKR	1.055 -> 1.016 s	1.255 -> 0.996 s	0.485 -> 0.359 s
Prove bus > Bus leaves	0.402 -> 0.375 s	0.470 -> 0.436 s	0.166 -> 0.125 s
Keccak reduction > Layer > Skip	1.385 -> 1.142 s	1.364 -> 1.081 s	0.129 -> 0.114 s
Keccak reduction > Layer > Tables	0.596 -> 0.545 s	0.591 -> 0.536 s	0.050 -> 0.041 s
Keccak reduction > Layer > Tail	0.605 -> 0.596 s	0.647 -> 0.640 s	0.086 -> 0.074 s
Commit	1.350 -> 1.369 s	1.344 -> 1.316 s	0.798 -> 0.707 s
PCS open > Commit	0.799 -> 0.768 s	0.839 -> 0.802 s	0.419 -> 0.400 s
PCS open > Open	0.087 -> 0.091 s	0.091 -> 0.107 s	0.066 -> 0.067 s
Execute program	0.293 -> 0.269 s	0.217 -> 0.185 s	0.051 -> 0.038 s
Build witness > Fill columns	0.244 -> 0.218 s	0.261 -> 0.213 s	0.105 -> 0.071 s
Prove	9.284 -> 8.765 s	9.514 -> 8.735 s	3.077 -> 2.659 s

Host: Ryzen 9 7950X3D (16C/32T), shared with other jobs, load average 47 to 105 during the runs, so CPU is the steadier number and wall varies a lot. Every comparison alternates the two binaries round by round (ab.sh, spancpu.sh). The two recursion ab.sh runs disagree on wall; the per-stage CPU of recursion improves in every touched stage.

Ideas

Constraint sumcheck: expand each table's state once, fold with the next message (commit 210a7a93b)

• Problem: the table sumcheck's kernels were the passes over the K columns: message_k (about 40% of the kernel samples) and join (about 43%, its loads and stores hottest, so bandwidth bound) each read every column; the folded rounds were only about 18%. Each later round was a message sweep plus a fold sweep.
• Change: a table's first active round builds its unfolded state (lin, left_g, right_g) and its message in one pass over the K columns. Every fold then computes the next round's message from the blocks it just wrote, so a round is one pass. Below sixteen rows per half the old fold and message stay; message_k, join and their row loader are gone.
• Effect: constraint sumcheck CPU -5% and -9% at xmss 900, -21% at recursion. On the older base the kernel samples fell 26%.
• Files: crates/leanvm_core/src/constraints.rs.
• Review notes: the round messages are the same polynomials. On the older base peak memory rose 3.111 -> 3.131 GiB; the per-commit bisection on this base shows no change from this commit.

Bus GKR: two rounds per pass with at least eight threads (commit ee76820d6)

• Problem: the vertical kernels read the whole layer once per sumcheck round, and the bus GKR is one of the largest stages (about 1.1 s CPU at xmss 900), waiting on memory at full thread count.
• Change: a port of upstream leanvm_core: prove the bus GKR two rounds per pass #557 onto main's batched triple GKR. Four rows sharing all but their two lowest index bits form a block; one pass sums a degree-four bivariate grid that gives round j's message and, after its challenge, round j+1's. The next pass folds each block at both challenges and sums the next pair's grid from the folded rows in registers. The identity tail and runs are still skipped, the three trees still run in one dispatch, and rows stay transposed between passes (Quads of F192x8, F192x8::load_blocks).
• Effect: Bus GKR CPU -4% and -21% at xmss 900, -26% at recursion. On the older base the stage's wall median fell about 20%.
• Files: crates/leanvm_core/src/gkr.rs, crates/primitives/src/field/x8.rs.
• Review notes: AVX-512 only, and only with PAIRED_THREADS = 8 or more pool threads: the pairs multiply more, and at one thread they cost 15 to 20% more GKR samples, so fewer threads keep the vertical kernels. Peak resident memory moves with this commit and no other (per-commit bisection): xmss 900 3.21 -> 2.77 GiB, recursion 1.63 -> 1.56 GiB, but sphincs 410 4.20 -> 4.44 GiB. The fold keeps a spare quad buffer per tree and frees the layer's rows after the first pair; with jemalloc keeping freed pages mapped the peak depends on that buffer schedule, and the sphincs increase is not isolated further.

Bus leaves: a push and a pull block share their products (commit 137dfd69f)

• Problem: an interaction's push and pull blocks over one table's columns flush the same coordinates at the same weights but for the count's slot, so their leaf formulas share all but a term or two, yet every block formed all its mixed products. At xmss 900 that was 155M mixed products per proof.
• Change: build_leaves pairs each block of a shape with the block sharing the most terms (Family, at most two members). Per chunk of rows the shared products are summed once, unreduced; each member adds its own terms, reduces and adds its constant. A leaf is the same XOR of the same unreduced products. The pairing removes 64M of the 155M products.
• Effect: Bus leaves CPU -7% in both xmss 900 runs, -25% at recursion.
• Files: crates/leanvm_core/src/leaf.rs.
• Review notes: pairing is greedy and quadratic in the blocks of one shape. KECCAK-instruction with custom output size #724's gated memory counts merge the products of one column pair into one term before pairing; terms still match by source and coefficient, so push and pull of a gated cell still pair.

Keccak skip sums: pivots and GFNI-weighted packs (commit 48cea407b)

• Problem: the AVX-512 SkipBlock was bound by the carry-less multiplier port: it weighed every product of a row by its position's weight, 40 VPCLMULQDQ per mixed point and eight slices, 208k per block.
• Change: a row's five products go by three pivots, each a factor its products share. A weight times an embedding is linear in the pack's bits, so per-position affine byte maps (SkipWeights, built once a layer) give the weighted packs already reduced with GF2P8AFFINEQB; a mixed point then costs 18 VPCLMULQDQ (94k per block plus 38k affine ops that overlap the multiplier).
• Effect: Skip CPU -18% and -21% at xmss 900, -12% at recursion. On the older base SkipBlock::run alone was about 33% fewer cycles per block.
• Files: crates/keccak_gkr/src/kernels.rs, crates/keccak_gkr/src/prover.rs.
• Review notes: the sums are a polynomial congruent to the old ones modulo the minimal polynomial, so the evaluated values are equal. Only the AVX-512 + GFNI arm changes; the other arms keep the old kernels behind the same interface.

Keccak round values: without reducing the factor B (commit 2e33b7205)

• Problem: Round::add_pair is CLMUL bound (carry-less products about 45% of its samples): it reduced B[j] for both rows of a pair (Karatsuba's six products plus Barrett's twelve per row), then took two dot products with T[j + 2].
• Change: the x86 kernel (PowerField::round_dot) leaves B as six words and meets T[j + 2] with it as two halves of three: 72 carry-less products per entry where there were 96. B + B' is weights * (T1 + T1'), so the value at infinity needs no second B. The sums grow to nine words, congruent to the old ones.
• Effect: Keccak Tables CPU (where add_pair runs) -9% in both xmss 900 runs, recursion 0.050 -> 0.041 s; Tail, which also calls it, is flat. On the older base add_pair's cycle samples fell about 19%.
• Files: crates/keccak_gkr/src/power.rs, crates/keccak_gkr/src/prover.rs.
• Review notes: x86 only; the other arms keep reducing B (round_dot_rows), which is also the new kernel's test oracle.

NTT short last chunk: skip the empty vector (commit ca23a5f5d)

• Problem: the AVX-512 register kernels take two eight-lane vectors of a row at a time. The L0 base encode's rows of 56 words are three such chunks and one of a single vector, and the kernel ran both vectors of that last chunk, the second all zeros: 64 lanes of work for 56 in every sweep of the deep pass and of the openings' row rebuilds.
• Change: the last chunk runs the kernel on the vectors that hold lanes only, each count an inlined call of its own. Rows of whole chunks are unchanged.
• Effect: together with the next commit, Commit CPU at xmss 900 is within noise on this base (+1% and -2%), recursion -11%. On the older base Commit fell 1.456 -> 1.322 s and the kernel alone went from 0.31 to 0.37 ns per butterfly to 0.26.
• Files: crates/pcs/src/ntt/kernels.rs.
• Review notes: AVX-512 only. A per-commit span run (4 rounds) did not separate this commit's effect from the host's noise at xmss 900.

NTT depth first: run the layers depth first past L1 (commit e5f837c28)

• Problem: run_layers swept each fused group of layers over the whole buffer before the next. A deep task is an L2 budget of rows or more (1.5 MiB at the level-2 encode), so each sweep streamed it through L2 and spilled to L3.
• Change: a buffer larger than L1 (4096 words) runs depth first: after a sweep, each block of the sweep's last layer runs its remaining layers while it is in cache. Same butterflies and twiddles in another order. With live (the openings' pruned rebuilds) the order stays breadth first.
• Effect: shares the Commit numbers of the previous block. On the older base the kernel alone gained 7 to 13% per butterfly, but in the prover the deep pass waits on its DRAM reads and the stage moved within noise.
• Files: crates/pcs/src/ntt/layers.rs.
• Review notes: the weakest idea here: a clear kernel gain that the prover does not resolve at xmss 900.

WHIR extension encode: keep only the message when every layer is deep (commit f35ec0b61)

• Problem: WHIR levels 2 to 4 plan a deep pass only: each task builds its cosets from the message, hands them to the leaf hasher, then streamed them out as the finished codeword (200, 100 and 50 MiB at xmss 900 on the older base), although on x86 (REBUILD_OVER_STORE) the commit only needs the codeword before its deep layers, which for these plans is the message's replicas.
• Change: the encode writes no buffer: it keeps the message itself as Codeword::BeforeDeep, and a query's row runs the deep layers of its sub-block from it, pruned to the queried rows, as rows read from any codeword kept before its deep layers already do.
• Effect: PCS open > Commit CPU -4% in both xmss 900 runs (this stage also runs the NTT commits' kernels), recursion -5%; PCS open > Open rises (0.087 -> 0.091 s, 0.091 -> 0.107 s) since the queried rows are finished on demand. On the older base this stopped allocating 350 MiB of level 2 to 4 codewords at xmss 900.
• Files: crates/pcs/src/ntt/deep.rs, crates/pcs/src/ntt/encode.rs, crates/pcs/src/ntt/openings.rs, crates/pcs/src/ntt/tests.rs.
• Review notes: level 1, the L0 base encode and the Apple path (which keeps the whole codeword) are unchanged. The deferred-deep test gains a shape whose tasks span several replicas.

Execute access counts: advanced in the access itself (commit bbf8c4c33)

• Problem: after an instruction's reads and stores, a second pass of bump_access_count went over the row's cells again, each touch re-checking the page cover; the interpreter's loop is cache-miss bound and single-threaded on the critical path.
• Change: Mem::read and Mem::put_counted return the cell's access count and advance it in the same touch, in flush order, so aliased operands still pair each access with its own count. Cells are indexed without bounds checks past ensure. cells_of_state is specialized on the layout like state_of_cells. Since KECCAK-instruction with custom output size #724 a KECCAK row writes only the output cells its bytecode requests; put_counted runs on those, and a cell not written keeps count 0, as on main.
• Effect: with the two hints commits, Execute program CPU -8% and -15% at xmss 900, -25% at recursion. On the older base this commit cut user instructions per execute 19% (778M -> 627M) without moving cycles in the loop itself.
• Files: crates/leanvm_core/src/cpu/execute.rs, crates/leanvm_core/src/keccak.rs.
• Review notes: the unchecked indexing relies on at calling ensure first (SAFETY comments). DEREF's store side keeps its separate bumps.

Hints index: g-power slots carry their keys behind per-slot tags (commit 76c2a226e)

• Problem: GPow's reverse index and coarse index held only the exponent and confirmed a candidate against the forward table, a random read of a table as large as the address space per probe. On the older base GPow::resolve drew 23% of the execute loop's L2 misses.
• Change: a slot holds (key, exponent), and a byte per slot holds eight tag bits of the keys homed there, so a lookup of an absent key (all but the last of up to 64 probes a resolve makes) reads one byte of an array a sixteenth the slots' size. Resolve inserts the exponent it found directly.
• Effect: shares the Execute program numbers above. On the older base the L2-miss share fell 23% -> 12% and cycles in GPow, the index, hint streams and inverses 75M -> 56M per execute.
• Files: crates/leanvm_core/src/cpu/hints.rs.
• Review notes: soundness is unaffected: hints stay untrusted witness data; this changes only how the interpreter finds an exponent.

Fill columns: each table's columns in one pass over its rows (commit 46bba9b95)

• Problem: every table filled its columns in four to six parallel passes over its trace rows (PC, FP, operands and words, counts, bytecode count), each re-reading the rows and re-decoding the instruction. JUMP's w = 1/c was a serial pass over all rows building three temporary arrays.
• Change: FillCtx::cols takes the list of local columns it writes, so each table fills all its columns in one dispatch and one decode per row; KECCAK lists every column but the input lanes. JUMP's inversion is a Montgomery batch per line of eight rows inside the same pass. Since KECCAK-instruction with custom output size #724 the KECCAK row also carries its OUT_TWO and OUT_ALL flags and its output lanes are the input lanes permuted again; the one pass forms both per row, as main's separate passes did. Rows::iter is gone.
• Effect: with the next commit, Fill columns CPU -11% and -18% at xmss 900, -32% at recursion. On the older base this commit alone cut Fill columns 12%.
• Files: crates/leanvm_core/src/tables.rs, crates/leanvm_core/src/cpu/trace.rs.
• Review notes: the column order inside each closure must match the cols list; a mismatch would show as a wrong witness, so the tests and digests are the check.

Strided g-powers: the interpreter keeps strides, the fill builds the table (commit 0fc4679d7)

• Problem: the interpreter grew a table of every power g^0..g^k as far as the run addressed (about 4M entries, 32 MiB, plus the copies of its doublings), serially and on the critical path, and handed it to the fill.
• Change: GPow keeps g^(64j) for the covered strides and g^0..g^63, so g^k is one product; the coarse index is built from the strides as before. Program::build makes the fill's table with primitives::field::g_powers across the pool. Execution::gpow is gone.
• Effect: shares the Execute program and Fill columns numbers above. On the older base GPow::extend left the profile and cycles in GPow, hints and inverses fell 56M -> 47M per execute; the traced Execute program min went 142 -> 124 ms over the three execute commits.
• Files: crates/leanvm_core/src/cpu/execute.rs, crates/leanvm_core/src/cpu/hints.rs, crates/leanvm_core/src/cpu/layout.rs.
• Review notes: GPow::pow now asserts the exponent is covered, where the table index would have panicked; the fill's table is always built rather than borrowed from the run.

How to verify

cargo test --release -p leanvm_core -p keccak_gkr -p pcs -p primitives -p lean_compiler -p rec_aggregation
cargo test --release -p leanvm --test api

Both pass on this branch; cargo fmt --all --check and cargo clippy --release -p leanvm_core -p keccak_gkr -p pcs -p primitives --all-targets -- -D warnings are clean. Proofs were checked by digest: throwaway builds of main and of this branch with a measurement patch print a hash of the proof bytes, and they match on every benchmark: 7d91b8513bdd4b03 (aggregate xmss 900), 3c41e153f8b2ee37 (aggregate sphincs 410), aa4b2ebd7a6989b2 (recursion). Every benchmark run also verifies its proof.

Commits

1. 210a7a93b constraints: expand each table's state once, fold with the next message
2. ee76820d6 leanvm_core: prove the bus GKR two rounds per pass with enough threads
3. 137dfd69f leanvm_core: form the products a push and a pull block share once
4. 48cea407b keccak_gkr: skip sums by pivots and GFNI-weighted packs
5. 2e33b7205 keccak_gkr: round values without reducing the factor B
6. ca23a5f5d pcs: skip the empty vector of an AVX-512 sweep's short last chunk
7. e5f837c28 pcs: run the NTT's layers depth first past L1
8. f35ec0b61 pcs: keep only the message of an extension encode whose layers are all deep
9. bbf8c4c33 execute: advance access counts in the access that reads or writes the cell
10. 76c2a226e hints: g-power index slots carry their keys, behind per-slot tags
11. 46bba9b95 tables: fill each table's columns in one pass over its rows
12. 0fc4679d7 hints: forward g-powers as strides times a first stride; the fill builds the table

[github-actions]

Benchmarks: base against this PR, on one runner

0fc4679 merged into its base, against the base e5d75f8: 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).

Threads shows the named configuration; default means no thread count is encoded in the benchmark ID.

Keccak GKR

benchmark	threads	runner	measure	base	this PR	change
keccak-hash-batch-262144	default	x86-64	Proving time	5.62 s	5.54 s	-1.26% (-2.16% to -0.59%)

Every result

Keccak GKR

benchmark	threads	runner	CPU	measure	base	this PR	change
keccak-hash-batch-262144	default	arm64	Neoverse-N2	Proving time	3.86 s	3.85 s	-0.38% (-2.01% to -0.19%)
keccak-hash-batch-262144	default	x86-64	INTEL(R) XEON(R) PLATINUM 8573C	Proving time	5.62 s	5.54 s	-1.26% (-2.16% to -0.59%)