Repository navigation
Replace BLAKE2S by KECCAK-256 - #636
Merged
Merged
Conversation
The one hash is now SHA3-256 (FIPS 202) in a cell encoding: plain SHA3-256 up to 128 bytes, and past that SHA3-256 of the message with the fixed eight bytes 00 00 00 00 00 00 00 80 after every 128. SHA3's 136-byte rate would split a 16-byte VM cell across two blocks; the encoding makes a block eight whole cells, and the gap is lane 16, whose non-final value is also the final block's last padding bit, so the opcode can supply it itself. - primitives::hash: Keccak-f[1600], the cell-encoded SHA3-256 (scalar, streaming, and a lane-transposed batch with AVX-512 (vpternlogq, vprolq), AVX2 and NEON (EOR3/RAX1/BCAX when the SHA3 extension is on) backends), and the zero-prefix state the PCS leaves share. - flock::hash: the Keccak step as a 2^16-slot R1CS block: 25 input lanes, 25 output lanes, the constant wire, and one chi product per bit per round (38,400, chi's multiplicative complexity). Whole-word witness stores, and both matrix walks (forward and transposed) over 64-bit wire lanes. - VM: the SHA3 opcode [m0..m3, tail, cap, out] is one sponge step over a thirteen-cell state: four independently addressed cells (lanes 0..8), a four-cell tail run (8..16), a five-cell cap run (lane 16 alone, then the capacity), thirteen output cells in the same layout. Same seven bytecode operands as BLAKE2s. Fifty virtual value lanes route to q_flock. - zkDSL: `sha3(a, b, out, tail=, state=, len=, final=)` is one block, the compiler placing the padding byte and XORing the message into a carried state; `sha3_cells(run, out)` hashes a whole fixed-length run. A fresh block's constant windows all come from one six-cell run per frame. - Guest: lists of runtime length (key lists, SPHINCS claims, the signer set) need no byte counter any more: every block but the last is whole, so only the last block's shape depends on the length, a small `match`, and the state rides a heap chain between loop frames. The window/base/scaled_log machinery is gone. Hashed byte strings are unchanged (natural concatenations). - Python verifier, LaTeX spec, zkDSL.md, AGENTS.md updated. Compared with the leanVM-b sha3 branch: that one absorbed 32 new bytes per permutation through a Merkle-Damgard chain of 64-byte hashes, read 35 cells and 18 constant cells per hash; this absorbs 128 bytes per permutation, reads 26 cells and sets 6 constants per frame. Permutations per verification: XMSS 138 (BLAKE2s 144 compressions), SPHINCS 513 (531). Every constant a hash reads is set in its own frame, which the prover's unconstrained-read assert checks on every proof; `list_split_rejects_a_ negative_rest` pins the range check that keeps the last block's `match` on a real arm. Measured 2026-09-23 on an AMD Ryzen 7 PRO 8700GE (8 cores, AVX-512), main vs this branch at main's counts: XMSS 900 2.106 s 427 sig/s -> 5.576 s 161 sig/s SPHINCS 245 2.312 s 106 sig/s -> 6.079 s 40 sig/s recursion 2->1 0.640 s -> 1.472 s (leaves of 900) 16 blobs 2.802 s -> 4.624 s proof size 296 KiB -> 340 KiB (XMSS 900) verify 5.9 ms -> 11.0 ms flock batch 152,506 BLAKE2s/s -> 40,359 Keccak/s raw hash (64 B) 716 Mhash/s -> 166 Mhash/s The cost is the witness: 2^16 bits per permutation against 2^14 per compression, 64% of it used. Co-Authored-By: Claude Opus 5.5 (1M context) <[email protected]>
Main restructured the BLAKE2s hash module, rewrote the Merkle builder, renamed lean_vm to leanvm_core and XMSS epoch to leaf_index, removed zk_alloc, and made the interpreter return errors. This branch replaced BLAKE2s with SHA3-256, so the conflicts are resolved in favour of SHA3 with main's structure: - primitives::hash stays the single SHA3 file; main's BLAKE2s kernels, test vectors and split module are dropped. - pcs::merkle takes main's block-at-a-time MerkleBuilder, with the leaf hasher ported to the sponge: shared zero chunks of 128 bytes, no byte counter, and no scalar arm since the batched hasher takes any length. - The interpreter's SHA3 arm returns Fault::NotCanonical (now a cell index and its width) where it panicked. - The guest's WOTS walk is inline as on main, returning the weighted digit as a constant. Its tip is still copied into the contiguous leaf preimage, since a SHA3 output is a whole state and cannot land there directly. - Bytecode pins regenerated for the five programs main's inline match moved. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The VM's SHA3 argument moves from Flock's R1CS zerocheck and lincheck to `crates/keccak_gkr`: a GKR over the rounds that commits a step's state every six rounds, as lanes, in the column still named `q_flock`, and proves the four segments between committed states in parallel. Sixteen instances pack into one binary polynomial of degree at most 23, so a layer's `chi` is one carry-less product per pack and position. The reduction leaves two claims on the column: its 64 bit slices at one point (the ring-switched claim) and the column itself at another (a plain point claim). All three verifiers move together: `leanvm_core::cpu::verify`, `python-verifier/verifier.py` and the recursion guest, which evaluates a claim's 1600 position weights from two points instead of one by one. The deferred claims shrink to the stacked bytecode alone. Annex C of the leanVM document is rewritten for the new protocol. `crates/flock` stays in the workspace as a standalone prover that nothing depends on. The prover builds the reduction's witness while the program executes, a block of 512 steps at a time on other threads, since execution is one thread's work. `cargo leanvm hash` is a new benchmark: a SHA3 hash chain through a whole proof. Measured on an 8-core Ryzen 7 PRO 8700GE, Flock before and this after: - aggregate --xmss 470: 1.66 s, 308.8 KiB to 0.86 s, 291.3 KiB - aggregate --sphincs 125: 2.07 s, 321.0 KiB to 1.25 s, 312.6 KiB - recursion --n 2 --xmss-per-leaf 450: 0.77 s, 216.1 KiB to 0.71 s, 213.6 KiB - hash --n 131072: 2.79 s, 313.3 KiB to about 0.9 s, 324.3 KiB - hash --n 262144: 1.72 s, 336.3 KiB, about 152K hashes/s (Flock cannot prove this size) - keccak_gkr hash_batch at 2^18, standalone: 1.08 s, about 241K permutations/s The SPHINCS, recursion and hash --n 131072 figures predate the last prover changes (witness built during execution, faster input opening) and were not re-measured after them. Hash-only proofs are a few percent larger than Flock's; the three headline benchmarks are smaller. Committing a state every 12 or 24 rounds was measured and rejected: 12 gains nothing as the column is placed, and 24 grows the XMSS proof by 78 KiB. Co-Authored-By: Claude Opus 5.5 <[email protected]> Claude-Session: https://claude.ai/code/session_014rTG2QQ3dYKQnpFhnn71Eq
No reviewer forged a proof or found the three verifiers disagreeing. What they did find: - Four `PowerField` row methods were safe functions over unchecked raw vector stores. They now assert their row lengths. - The vector kernels were gated on different subsets of the features they use, so some feature sets failed to compile. One set gates them all. - `Witness::from_extents` trusted its caller for which blocks were written while being safe to call. It is `unsafe` now, and `Extent::new` says what it actually promises. - No test noticed a Keccak check being deleted from the Python verifier or the recursion guest. Each of the four checks is now tripped by the word it reads last: Python is matched on its error message, the guest on the function and source line its run fails at. Removing any one of the guest's four asserts fails the new test. - The witness built during execution had no test. It is compared with the single-pass build over whole, partial and missing blocks. - The crate never tested a false statement, nor the VM's depth. A committed state that breaks the permutation is now rejected at depth 6, and an end-to-end run at depth 6 folds more than one run of blocks. - The relation label is tied to `DEPTH` by a test. - Stale wording: a VBMI claim, Flock comments citing an annex that no longer describes it, two "flock's instance floor" messages, and AGENTS.md's subcommand list, bench list and thread-pool notes. Left as found: the three unused slots of a step's region carry no weight, so nothing constrains them (nothing reads them either); the guest hardcodes four constants beside the depth placeholder; CI builds for haswell, which compiles none of the AVX-512 kernels. Co-Authored-By: Claude Opus 5.5 <[email protected]> Claude-Session: https://claude.ai/code/session_014rTG2QQ3dYKQnpFhnn71Eq
The flock crate is deleted, along with the code only it used: the GF(2^8) additive NTT and its inverse table in pcs, and F8, the phi_8 table and the Lagrange skip helpers in primitives. What still carried its name is renamed, in all three verifiers and the document: leanvm_core::hash_flock is leanvm_core::keccak, q_flock is q_keccak (QKECCAK_*, qkeccak_*, \qkeccak, \nkeccak), and the annex file is c-keccak-gkr.tex. The CREDIT headers and the citations of the Flock paper stay. CI's bench.yml now proves keccak_gkr's hash_batch, which gains the --json output; its latency includes witness generation. The bench job of the PR that lands this fails at the base commit, which has no keccak_gkr crate. No protocol or performance change: cargo leanvm hash --n 262144 gives 152,346 hashes/s (1.721 s, 336.3 KiB), XMSS 470 0.862 s and 291.3 KiB, on a Ryzen 7 PRO 8700GE. Co-Authored-By: Claude Opus 5.5 <[email protected]> Claude-Session: https://claude.ai/code/session_014rTG2QQ3dYKQnpFhnn71Eq
On aarch64 the four kernels of the layer prover (embed, products, skip_row, fold_group) ran their portable forms, the only vector forms being AVX-512. Each portable carry-less product went through a u128 in general registers, and skip_row XORed every partial product into memory. The NEON forms keep the products and the row's sums in vector registers, two packs or slots to a register, and embed sixteen packs at a time with byte table lookups, the embedding being linear in each nibble. They agree bit for bit with the portable forms, which the kernel test now checks on aarch64 too. x86 is unchanged. On an M4 Max, alternating with the parent: - KECCAK_N_LOG=18 hash_batch: 929 / 935 ms before, 703 / 704 ms after (-24%). Per layer, Skip 51 -> 21 ms, Tables 12.6 -> 9.5 ms, Product 46 -> 40 ms. - cargo leanvm hash --n 262144: 1.274 / 1.252 s before, 1.035 / 0.975 s after (-20%), peak memory unchanged at 7.1 GiB. Tried and dropped: three bit-level rounds instead of four (5% faster on the M4 but 2.5% slower on a Ryzen 7 PRO 8700GE, where Tables and Tail double), cache-blocking Product's bucket adds a digit at a time (no change on the M4, 13% slower Product on the Ryzen), and other bucket digit sizes (flat). Product is now half of a layer, all of it bucket accumulation. Co-Authored-By: Claude Opus 5.5 <[email protected]>
doc/notes/keccak-gkr.tex explains crates/keccak_gkr informally: what is committed, the form of a claim, the six parts of a layer, the two openings it ends on, and why it is sound and fast. Annex C stays the precise description. It credits Hashcaster (morgana-proofs/hashcaster) for the bit-level first sumcheck rounds and Hashcaster 2 (levs57/hashcaster2, with its RMFE-skip note) for packing bits into a polynomial ring and checking the product polynomial through the unpacking map. AGENTS.md points to it. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Each bus block's eq over its selector bits and the rebuild of its offset ran as a mul_range loop, whose every iteration copied eleven captured values into the next frame. A match on the range-checked length now dispatches to one unrolled arm per length, reading the bits, 1 + zeta and the index factors at compile-time offsets from runtime base pointers. Root of recursion --n 2 --xmss-per-leaf 450 --log-inv-rate 2 (non-fill counts): MUL 271021 -> 242563, XOR 140987 -> 136279, DEREF 146665 -> 139051, SET 60448 -> 55087, JUMP 25168 -> 23882. Co-Authored-By: Claude Opus 5.5 <[email protected]>
… loop Each query of a level evaluated prod_t (a_t + b_t * chain_t), reading both coefficients per coordinate. Dividing every factor by b_t once per level leaves prod_t (a_t / b_t + chain_t), one heap read and one multiply less per coordinate, and the level's product of the b_t scales its residual sum once. b_t is a challenge times a nonzero constant, so a zero challenge makes the division unsatisfiable rather than free. Root of recursion --n 2 --xmss-per-leaf 450 --log-inv-rate 2 (non-fill counts): MUL 242563 -> 235247, DEREF 139051 -> 131826, XOR unchanged. Co-Authored-By: Claude Opus 5.5 <[email protected]>
TomWambsgans
marked this pull request as ready for review
October 14, 2026 16:31
Each path level multiplied the path pointer by its compile-time level offset before applying the runtime direction selector, and the cap leaf store rebuilt cap_index^2 twice. The selector now multiplies the bare pointer and the level offset rides the DEREF immediate; the cap leaf pointer is cap * q^4 * selector with the constant node offset folded. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The cap check walked its internal nodes in a mul_range loop, paying per-iteration argument copies and runtime pointer products for every flag and cap cell. Unrolled over the compile-time cap depth, every address is an immediate. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The lane is rebuilt only from its bits at and above nbits, which is itself the claim that the low nbits are zero, so the low bits need no booleanity pin and the runtime zero-check loop goes away. Co-Authored-By: Claude Opus 5.5 <[email protected]>
column_selector computed 1 + bit + point[k] per bit, two XORs. The opening point's 1 + point is now tabulated once per proof, leaving one. Root of recursion --n 2 --xmss-per-leaf 450 --log-inv-rate 2: column_selector XOR 7550 -> 5106, check_opening_terminal XOR 756 -> 812 and DEREF 2704 -> 2814 for the table. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The residual's query loop read the level's coefficient row and set its vanishing constants afresh for every query, and copied its captured values into the next frame. Two queries an iteration share both, with an odd count's last query evaluated after the loop at compile-time indices. Root of recursion --n 2 --xmss-per-leaf 450 --log-inv-rate 2: open_stacked MUL 22482 -> 19782, XOR 15344 -> 15118, DEREF 11712 -> 7708, SET 9042 -> 5242, JUMP 858 -> 634. Bytecode 203937 -> 213340 instructions. Co-Authored-By: Claude Opus 5.5 <[email protected]>
A key list's chain loop carried the 13-cell sponge state through the heap on every block, read and written back, and paid a loop frame's argument copies and its record address per block. A step now hashes four blocks, the states between them staying in the frame, and the tail dispatches on the blocks left over and the last block's keys. The block count splits into quads and a remainder through its exponent's pinned bits. The child list also hoists the coverage pointer's origin out of the loop. Co-Authored-By: Claude Opus 5.5 <[email protected]>
path_ptr * (1 + bit*(1 + g^2)) took two products a level; with path_step = path_ptr * (1 + g^2) hoisted, path_ptr + bit*path_step is the same address for a boolean bit at one product a level. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The bus GKR's round loop called sumcheck_round5 per round, paying a frame's argument and return copies, and addressed a round's record as round^4, three products. The round now runs in the loop body, and the records lie field by field, GKR_ROUNDS_CAP apart, so a round's record and its point coordinates are one product off the counter each. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The query body becomes an inline opening_query, and the level-0 loop (base-field rows, 64 eq weights each) runs two of them per iteration, so each weight read and the iteration's argument copies serve two queries. An odd count runs its first query ahead of the pairs, so the hint streams are still consumed in query order. Extension levels keep one query an iteration, the code size of a pair body there buying little. Co-Authored-By: Claude Opus 5.5 <[email protected]>
A radix-four layer runs 2k rounds, or 2k + 1 at an odd depth, so the round loop now takes two a step, their Fiat-Shamir state, cursor and claim staying in the frame between them, and an odd depth's last round is one call. That halves the loop's frame copies and record traffic. Co-Authored-By: Claude Opus 5.5 <[email protected]>
open_stacked writes 1 + point next to the point it assembles, at no extra read, and every eq factor of the terminal check (the prefix chains, the public-input chain, the ring-switch rows, the column selectors) reads it instead of adding the one itself. The q_keccak slot factors multiply top bit first, so claims sharing their high slot bits share partial products. Root of recursion --n 2 --xmss-per-leaf 450 --log-inv-rate 2 (non-fill counts, run to run noise of a few hundred aside): XOR 133665 -> 133389; check_opening_terminal MUL 2430 -> 2326, eq_prefix_chain XOR 390 -> 262. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The level-0 eq weights over the lane-fold challenges factor as a low (three coordinates) and a high part, so opening_row_weights stores the two factors and a query sums each run of eight lanes against the low factor before scaling it by the high one. A query pair then reads 16 weights rather than 64, for eight more products a query. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The Index coordinate's MLE ran as a mul_range loop over the block's kappa, each iteration copying its captured values into the next frame. A match on the range-checked kappa dispatches to an unrolled product with the factors as constants. Root of recursion --n 2 --xmss-per-leaf 450 --log-inv-rate 2: the two Index loops (MUL 1200, XOR 160, DEREF 320, SET 320, JUMP 84) become index_mle (MUL 160, XOR 80, DEREF 80, SET 84, JUMP 4). Co-Authored-By: Claude Opus 5.5 <[email protected]>
ring_switch_target ran one mul_range iteration per packing row, re-reading the map challenges and copying its captured values each time. Eight rows an iteration share the challenge reads and combine as sum_r x^r L(slice_r) by Horner, the chain carrying x^(8j) and the running sum. Root of recursion --n 2 --xmss-per-leaf 450 --log-inv-rate 2: ring_switch_target MUL 10626 -> 9202, XOR 1024 -> 912, DEREF 1428 -> 308, SET 648 -> 88, JUMP 134 -> 22. Co-Authored-By: Claude Opus 5.5 <[email protected]>
A key list's loop now hashes eight blocks a step instead of four, and the blocks left over go through a one-block loop rather than a sixteen- arm tail, so the last block's dispatch is the original four arms. The block count splits at its exponent's low three bits. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Extend the level-0 tensor factoring to the extension levels: their sixteen eq weights become eight low and two high factors, ten reads a query rather than sixteen, for two more products. The packing of extension rows is now one pack64x2 per pair of limbs, the same instructions as before. Co-Authored-By: Claude Opus 5.5 <[email protected]>
rs_eq_run read and wrote its 64 running products once per coordinate. Two coordinates an iteration halve that; the count splits as 2 * half + odd from advice bits, each boolean-pinned and tied back by g^half * g^half * g^odd == g^count, and an odd count's last coordinate runs after the loop. Root of recursion --n 2 --xmss-per-leaf 450 --log-inv-rate 2: rs_eq_run MUL 6716 -> 6328, DEREF 5996 -> 3184, SET 188 -> 106, JUMP 52 -> 30. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The announced sizes' bits were hinted into a heap buffer and each read back, and each weight g^(2^j) was looked up in g_squares. The bits now live in the frame, pinned boolean by a write-once store, and the weights are compile-time constants. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Query k's dot product is weighted lam^k. Rather than reading lam^k from query_weights each query, the loop runs h <- (h + dot_k) / lam and one product by lam^n (already computed by the caller) restores the sum, so a query reads no weight and needs no weight pointer. Co-Authored-By: Claude Opus 5.5 <[email protected]>
- while_executing: the extents the witness workers write into outlive the thread scope, so a panic in the run or a worker no longer frees them while workers still write - the Python verifier's tamper tests are back: six tampers, each pinned to the exact VerifierError in Rust and the matching message in Python, the Keccak reduction's stream positions read from Summary::keccak_scalars - keccak_gkr: one cfg predicate per file (cfg_select!), the NEON PMULL helpers and the GFNI transpose stage shared with primitives, a dead store in Round::factors removed, Openings::into_pcs_claims replacing leanvm_core's ring_switch_open, bench-only items moved into batch_bench, the output claim computed in parallel and timed as its own stage - verifier: QKECCAK_SLOT_BITS derived from the depth; keccak_f's theta and chi written row by row, which removes the vpgatherqq LLVM emitted for them (hash --log-n 14 verify 9.4 ms to 6.1 ms on Zen 4); slot weights in Horner form, mirrored in Python - sumcheck challenges named challenge, not rho, in all four implementations - pcs: no modulo by LANES, which clippy refused on plain x86-64; primitives: the generic aarch64 xor3 fallback wraps its intrinsic in unsafe - lean_compiler: a message cell wholly past len= is a compile error; docs and tests follow the Keccak transcript (cap=), rate and capacity worded consistently - guest: dead code removed, pack_pair shared, stale citations fixed; the bytecode is unchanged - docs: Annex C gains its soundness section (37 kappa + 902 over |E|, as formal/keccak_gkr proves), padded segments, unconstrained unused slots, one symbol per object (\kin, \kout, \kperm, \kbatch as tau_KECCAK); 136-byte blocks in Annex B; 267 permutations; AGENTS.md's x86 check includes +avx512vbmi - stale BLAKE2s, Flock and output-commitment comments fixed; n_blocks is n_steps where it counts steps, Brow is Krow Co-Authored-By: Claude Opus 5.5 <[email protected]>
- The embedding tables (RMFE, the NEON nibble tables, the x86 affine matrices) are built at compile time: every embed paid a lazy-init check and a non-inlined table load. - Skip's ternary extension is built in NEON registers, fused with the embed, four packs to a vector; the slot order follows the vectors (`mixed_points`, `slot`). - Product groups a block's positions once by 8-bit digits of their weights, over quarters of the packs whose products stay in cache, in place of 6-bit digits per row of the state. - A NEON 64 by 64 bit transpose for Product and the witness. The protocol and the proof are unchanged. On an M4 Max, keccak_gkr's hash_batch at KECCAK_N_LOG=18, eight interleaved runs, median proving time 484.5 ms before and 459.5 ms after (-5.2%): Skip -13%, Product -4%, Tables -2%, witness -11%. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Prover only: the proof is byte-identical (checked at six shapes, depths 6 to 24, and by a test against running every padding block). - The blocks after the last input are all the same all-zero step, so each layer computes the padding block once and weights it by the sum of the eq weights it stands for: Skip skips it (its extension vanishes), Tables and Tail keep a segment's real rows plus one padding row (`Rows`, `pads`), and the openings' `fold_packs` and `Witness::generate` do the same. - x86 Skip (`SkipBlock`) takes eight positions a register, so the extension is register XORs and no slot is spent on padding; x86 Product groups whole payloads (three AVX-512 registers) where other targets keep quarters; `fold_groups` folds both halves of a block and sums their lanes by shuffles; Karatsuba in the x86 `partial` and `fold_row`. - Tables and Tail build each row in cache and publish it with streaming stores. On the Ryzen 7 PRO 8700GE (Zen 4), against 8216589, interleaved runs: aggregate --xmss 900 proving 2.49 s to 2.07 s (Keccak reduction 783 to 374 ms), --sphincs 850 2.685 s to 2.40 s (786 to 497 ms), hash --log-n 17 518 to 409 ms. NEON compiles but is not measured here. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Prover only: the proofs of aggregate --xmss 900, --sphincs 850 and recursion --n 2 are byte-identical to 70eeb4c's, and cycle counts are unchanged. Each part was kept only where its measured gain pays for its lines. - Execution: keccak_f's round in place under AVX-512 (LLVM turned the straight-line round into shuffles there); memory in 2 MB pages with access counts as exponents; trace rows in fixed chunks; witness streams looked up once per run. - Witness: columns filled through a line buffer with streaming stores, memory and count columns in one pass, bytecode columns in one parallel pass, the interpreter's g-power table reused. - Constraints: bus-form products sharing a column factored (`RowForm`). - Bus: 8-lane AVX-512 field kernels (`primitives::field::x8`) and GKR rounds on the transposed layout; eq split in two tables, no serial shrink; the three trees folded in one dispatch, small rounds serially; leaves built once by table with levels 2 and 4 of the tree formed in cache; rows known to be the identity skipped; g^z on the fly; split-eq evaluations at zeta. - PCS: a masked vector for the NTT lanes that do not fill one; the pass plan choosing the deep pass that saves a sweep; the first pass reading scattered rows once per residue; the transposed induce in two sweeps. On the Ryzen 7 PRO 8700GE (Zen 4), against 70eeb4c, interleaved runs: aggregate --xmss 900 2.21-2.26 s to 1.77 s, --sphincs 850 2.63 s to 2.09-2.16 s, recursion --n 2 --xmss-per-leaf 900 0.77 s to 0.60 s (peak memory 11.1 to 9.9 GiB). On an AVX2-only EPYC Milan, neutral to slightly better. Co-Authored-By: Claude Opus 5.5 <[email protected]>
main's 25703e0 carries the non-Keccak optimizations this branch already had (df8dfaf), ported to main, plus the fixes of an adversarial review. This branch's versions are kept, the fixes applied to them: the NTT pass plan never below zero (Apple silicon), the bus's identity runs sorted, a lone product in `RowForm` evaluated directly, the step limit checked against a `KECCAK` row's cells, `BusForm::eval_unreduced` removed. The README keeps this branch's measurements. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The guest conflicted: main sets the chain index in the dispatch arm of a `chain_step` that hashes with BLAKE2s, where this branch inlines the step and hashes with KECCAK. Resolved by writing main's change against this guest, which is the same six lines: `walk`, `walk_group` and `verify_lean_xmss` thread a `tags` run built once before the two layers, the chain step names `tags[i]` where it set `i`, and leanSPHINCS passes `powers` for the table its addresses make it never read. On this branch, leanXMSS aggregation: 1,126.6 cycles a signature to 1,114.4 (marginal, fitted over 64 and 128), 128 signatures 153,896 cycles to 152,371, bytecode 2^18.494 to 2^18.474. README keeps this branch's own benchmark table, main's being its BLAKE2s numbers. Co-Authored-By: Claude Opus 5 <[email protected]>
The Lean proof of the Keccak GKR goes, with its CI job. Annex C keeps the soundness bound, now as the paper argument it is, and says what it leaves out (Fiat-Shamir, the commitment scheme); the crate docs and AGENTS.md point there. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Prover only, proofs byte-identical. AVX2 machines ran the portable code; they now get vector arms for embed, embed_extend, products, skip_row, fold_groups, SkipBlock, the power-basis row kernels and transpose64. The carry-less products are written once over `clmul::Vector`, 128-bit lanes that are `__m128i` with PCLMULQDQ (haswell-class) and `__m256i` with VPCLMULQDQ (Zen 3, Alder Lake). The AVX-512 and NEON arms are unchanged. On h2 (EPYC Milan VM, AVX2 + PCLMULQDQ), interleaved runs: hash --log-n 17 2.20 s to 1.75 s, aggregate --xmss 900 6.38 s to 5.86 s (Keccak reduction 2.40 s to 1.85 s). With VPCLMULQDQ (znver3 build on Zen 4) the layers take a further third less. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The first lane round no longer writes its F192 fold of the witness: it builds the next message from the base lanes (`fold_base_and_msg_blocks`), and the second round rebuilds the fold from the 8-byte base words (`lifted_lane_fold`), two rounds of folding in one formula. Every target takes the same path; proofs are byte-identical. Peak memory, aggregate --xmss 900 / --sphincs 850 / recursion --n 2: 9.49/10.03/9.91 GiB to 8.47/9.02/9.02 GiB on Zen 4, 9.39/9.98/9.82 GiB to 8.36/8.91/8.92 GiB on h2 (AVX2), with proving time slightly lower on both. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Prover only, proofs byte-identical. - NTT: a PCLMULQDQ + AVX2 butterfly, four lanes a call, one carry-less multiply each and one shared reduction, where AVX2 without VPCLMULQDQ fell back to the scalar product; the AVX2 + VPCLMULQDQ butterfly reduces by shifts, as the AVX-512 one does. - Bus: the scalar GKR kernels skip the rows known to be the identity (x86_64; `gkr::SKIP_IDENTITY`), as the AVX-512 path did; the round message weights child 0's line by eq, 14 products where 16 were; the four- and sixteen-tuple leaf products stop at a block's real rows. - 256-bit field kernels for AVX2 + VPCLMULQDQ: `dot_base`, `mul_base8`, and `field::x4` with a four-row leaf builder. On h2 (EPYC Milan VM, AVX2 + PCLMULQDQ), interleaved runs: aggregate --xmss 900 6.41 s to 5.55 s, --sphincs 850 7.50 s to 6.68 s, recursion --n 2 1.82 s to 1.47 s. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Hashes and proofs unchanged. - The final block of each input is read straight into the lane buffer and its padding XORed into the state, where eight memcpy calls per group (each with a vzeroupper) ran with the whole state live and spilled it. - `permute` forms rho/pi by output row, applies chi row by row and gathers the next round's column parities from chi's outputs: the same rounds in an order every x86 backend runs faster. - The hash bench also times a 512-byte input, a 64-word PCS leaf. hash_throughput, 64-byte inputs: h2 (AVX2, 8 threads) 33.5-34.4 to 43.6-43.9 Mhash/s, Zen 4 one thread ~17.2 to ~22.1. aggregate --xmss 900: 6.42 s to 6.38 s on h2, ~1.4% on Zen 4 (noisy host). NEON's codegen changes with the shared round order and is not measured here. Co-Authored-By: Claude Opus 5.5 <[email protected]>
- verifier: verify_keccak returns AnnouncedTableSizes where it asserted its operand lengths. `aggregate` reaches it through replay_unchecked with a child's announced shape, and that path owes the caller InvalidChild rather than a panicking worker thread. The same require carries log_steps >= 4, which is what keeps pack_bits from underflowing and instance[4..] from slicing short. Both callers already satisfy all three, so the reduction behaves as before - keccak_gkr: const asserts for the coupling Part's vector arms rely on. PART divides by four, which pack's as_chunks::<4> needs and which would silently drop products, and PART_WORDS by each arm's lane count, eight with AVX-512, four with AVX2, two with NEON, which add's step_by would otherwise store past the array. The cfgs were changed together correctly when PART went from 8 to PACKS/2, but nothing said they had to be - AGENTS.md: n_lanes lies in [2^(k-1)+1, 2^k] only where mu is log2_ceil(placed) rather than the MIN_MU floor it is clamped to; under the floor it falls as low as 1, which is the clamp placements_of carries Each gated assert was checked by breaking it: the AVX2 one fails the AVX2-only cross-check and stays silent under the AVX-512 one. Co-Authored-By: Claude Opus 5 <[email protected]>
Behavior unchanged: proofs are byte-identical to 4dc0f82 (aggregate --xmss 900, --sphincs 850, recursion --n 2, a blobs mix at rate 3, fibonacci), as are cycle counts and the compiled guest. - keccak_gkr: one copy of `words`, `row_positions`, `state_words`, the fold and the carry-less multiply-accumulate (`basis::add_mul`); the AVX-512 power-basis module served by the generic `clmul::Vector` kernels; `first_claim`'s dead parameter, the literal kernel sizes and the duplicate `LANES` gone; internal modules private. - leanvm_core: `keccak` derives its sizes from `keccak_gkr::Shape` and shares the witness block helpers with `Witness::generate`; the 25 input lanes are windows into q_keccak rather than a copy, routed by one `keccak_value` helper; the virtual columns dropped after their last use; one table for the KECCAK cell operands; the scalar GKR fold walks the identity runs; `x4` takes `x8`'s API so one leaf fill serves both. - pcs: `StackClaim::Strided` and `RingSwitchOpen::qkeccak_vars` (now derived) gone; one scalar NTT tail; one AVX2 butterfly for both tiers. - primitives: one hash backend dispatch, `hash_many` and `hash_many_from_state` as the batched entry points, `keccak_f_many`; `reduce_halves256`. - fiat_shamir: the pending scalars live in the sponge's rate, so absorbing, sampling and grinding share it; grinding runs the raw batched permutation instead of cancelling a hash's padding. - verifiers: `Placement.low` gone; the KECCAK output claims read by index from the table sumcheck's evaluations, not re-checked; named constants for the lanes, rounds and packs; word-wise absorption. - compiler: one heap-to-stack helper, one sponge-cell parser, one previous-state parser. - rec_aggregation: the Keccak guest constants from `Shape`, prefix sums from `xi_offsets`, the leanSPHINCS digest fields from the scheme; `aggregate_two_to_one` exercises the claim-group loop again. Co-Authored-By: Claude Opus 5.5 <[email protected]>
q_keccak is a run of 2^6 columns per KECCAK row, and the two committed states fill only 50 of them, so 14 blocks of zeros rode the stack beside 14 columns of the table that each had a block of their own. The reduction weighs nothing on those slots and proves nothing about them, so they now hold the table's first committed columns (pc, fp, the operands and flags, free, r_0), which become virtual with their claims routed to their slot, exactly as the input lanes already were. The claim list's length and order, the stacking, and the guest's placement walk are unchanged; the guest's constants regenerate themselves from col_kappa_sources. Both openings are claims on the whole block, so they have to fold what rides there now: output_claim evaluates every slot, and open_inputs folds the spare slices at the instance point, a task per group of eight steps with one subset-sum table per group serving every slot. aggregate --xmss 300 --log-inv-rate 1: the committed stack drops 4.4% (21,037,056 to 20,119,552 words), Commit 47.0 to 42.7 ms, PCS open 71.4 to 68.3 ms, the Keccak reduction unchanged at 87.7 ms, proof size 305.3 to 300.0 KiB, peak memory 2.494 to 2.444 GiB. recursion --n 2 --xmss-per-leaf 100: 364,192 to 363,731 guest instructions and 458,325 to 455,169 cycles, the guest certifying 14 fewer committed columns. The relation label is bumped in the three places that bake it, so old and new proofs are domain-separated. Section 7.6 is rewritten around the row and its columns, and Annex C around the run. Co-Authored-By: Claude Opus 5 <[email protected]>
Shape's doc says the witness's raw writes rely on Shape::new's bounds, but it only checked that the depth divides the round count. Shape::new(1 << 63, 12) then left slots * n at 50 * 2^63, which wraps to zero, and stack_log at 69, whose shift masks to 5, so both of Column::new's checks passed on an empty buffer and the writes ran out of bounds: a safe call that segfaulted. One assert in Shape::new covers every such size, since slots <= 2^slot_log makes each of them at most the 2^stack_log words of the committed block. Co-Authored-By: Claude Opus 5 <[email protected]>
The parser had a floor and no ceiling, so `--log-n 64` wrapped `1 << log_n` to one in release and benchmarked 512 permutations, the reduction's own floor, as if the argument had been 9. The ceiling is the largest batch whose committed block the verifiers take: MAX_MU less the slot bits, so 22. Co-Authored-By: Claude Opus 5 <[email protected]>
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
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.
Keccak is still still a placeholder, for now.