WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 107.5 s

[MauroToscano]

Draft. The WHIR pipeline's best configuration, complete on top of main: the per-table GPU recursion, the WHIR recursion with its three optimisation rounds, and the ZisK-style proof-format levers (formerly #1007), with main merged. Block 25368371 proves in 107.45 s.

The number

Block 25368371 on the FAST box (Ryzen 9 9950X, RTX 5090 32 GB), RPX commitments, 15 epochs at 2^21. ABBA on one binary: the new default against the legacy format, two arms each, alternated.

configuration	block wall	host peak	recursion hash permutations
this branch, default format	107.45 s (107.1, 107.8)	23.8 GiB	6.49 M
same binary, legacy format (this PR before the format levers)	128.00 s (127.8, 128.2)	32.5 GiB	10.27 M

That is −20.55 s (−16.1 %). A no-knob run on the final code read 107.0 s, with a permutation census and program ids identical to the arms above. For reference, the STARK pipeline measured 159.35 s before these levers and 129.55 s with them, in the same kind of ABBA.

What is in the branch

• Per-table GPU recursion (Per-table GPU recursion (RPX) with ZisK-style proof formats: block 25368371 in 121.7 s #985): per-table STARK proofs of each epoch on the device, LFM wraps and nodes, one root for the block.
• WHIR recursion: WHIR base proofs, the WHIR-verifier wrap, the global wrap and the interior on the device. The first full version proved the block in 148.9 s, already including the VRAM budget read from the driver (−8.3 s). Evictable leaf-layer retention on the card (−9.1 s), then fan-in 3 in the interior plus the global child proved inside level 0's pool (−11.9 s), took it to 128.3 s.
• Proof-format levers, taken from ZisK's recursion. One ZfFormat (prover/src/zf_format.rs) parses five LAMBDA_VM_ZF_* knobs once and prints one ZF FORMAT: banner. The default is cap=auto whir_cap=auto fri=dp one_row=0 whir_folds=first6:
  • Merkle caps on every STARK and WHIR tree. Paths stop at a verifier-chosen height c ≤ 3, and the cap rides at the end of each tree's first path, so the proof structs are unchanged. WHIR: −1.85 s on the recursion proofs, −0.95 s on the base proofs.
  • FRI folds by 2^d per committed layer, one challenge each, with a verifier-side DP schedule: −7.35 s.
  • A six-variable first WHIR fold, schedule [6,4,4,4,4,3] at 25 variables: one round and three grinds fewer per chain, −9.30 s.
  • One-row openings with a committed FRI input (LAMBDA_VM_ZF_ONE_ROW=auto) are built on host, GPU and in-guest, but off here: they cost +3.2 s on this pipeline. They are on in the STARK pipeline's PR (Per-table GPU recursion (RPX) with ZisK-style proof formats: block 25368371 in 121.7 s #985), where they save 8 s.
  • Every knob keeps its off value, and ZfFormat::LEGACY stays pinned by a golden test. The RV64 recursion guest verifies only the legacy format.
• main: perf(alloc): compile jemalloc's never-purge policy into the binary #996 (jemalloc never-purge compiled into the CLI).

Soundness of the format levers

Query counts, grinding bits and blowup are unchanged.

• Caps. The root is still the commitment. The cap is hashed to the root once per tree, and each path must reach the cap node the query index selects. Path lengths are checked exactly, including at c = 0.
• FRI folds by 2^d. This is Haböck (eprint 2022/1216) Protocol 1 / Theorem 2 with reduction factors 2^d. Only Σaᵢ changes, in a term that stays more than 50 bits below the dominant one.
• One-row openings. This is batched FRI with the DEEP codeword committed before the first fold challenge, the layout Plonky3 uses. The query index is uniform over the whole domain.
• WHIR first fold. Only the grouping of variables into rounds changes. Every error term is invariant or shrinks with fewer rounds, and queries stay 112 per round.

Fixed along the way

• One-row verify. The verifier's Phase-A transcript replay absorbed the row-pair root of one-row preprocessed tables, which rejected honest proofs that publish values.
• Device byte-parity tests now run on a card. S3/S2 vector proofs and LFM proofs are byte-identical between CPU and GPU.
• Comments are self-contained. The format code's comments point at nothing outside the repository.

Gate and CI

The final gate ran at d8ffc0702, whose prover library is identical to this branch's; main's merge adds only CLI and test files. It ran on the FAST box:

• The lib suite passed exactly 1534, with 0 failed and 90 ignored. The stark suite passed exactly 395, with 0 failed and 6 ignored.
• 79 of 80 targeted lines passed at their exact pre-registered counts.
• Device parity held on every line. Banners, WHIR pins, and the in-guest twin and node checks were green.
• The 80th line was killed for memory at full test parallelism. It passes 23 / 0 / 1 with --test-threads=3.

In CI, one prover shard's hosted runner receives a shutdown signal and SIGKILLs epoch_chunk_multiplier; this branch failed the same way before the format levers. That test passes on the box.

Open decisions

1. Merging. This PR and the STARK PR (Per-table GPU recursion (RPX) with ZisK-style proof formats: block 25368371 in 121.7 s #985) carry the same code and differ only in the one_row default. A per-pipeline default would let one PR carry both.
2. Security. A proven-128 audit is under way against ZisK's accounting (BCHKS25 Johnson-bound bounds, per-phase grinding). Our query phase already matches theirs.
3. Protocol changes. W3 (WHIR query carry-over) and W4 (the WHIR paper's rate schedule) are analysed, not built.
4. An LFM lookup chip would let larger caps pay.
5. RV64 proof bytes are not reproducible across processes, because six table builders order rows by HashMap iteration.