Small proofs - #4
Open
TomWambsgans wants to merge 140 commits into
Open
Conversation
Two >128-bit alternatives to F128, NEON/PMULL-optimized: - F192 = GF((2^64)^3), y^3+y+1 over x^64+x^4+x^3+x+1: Karatsuba-3, 9 PMULL per mul (+ schoolbook and scalar-reduce variants). - F160 = GF((2^32)^5), y^5+y^2+1 over x^32+x^7+x^3+x^2+1: Montgomery 13-mult 5-term formula (+ Karatsuba-15, schoolbook). Both ship deferred-reduction accumulators (F192Unreduced / F160Unreduced), square(), Fermat inv(), portable fallbacks, and tests: NEON-vs-reference, independent Python vectors, field axioms, and computational irreducibility proofs of all four moduli. F128 gains a 2-PMULL square(), now used by its inv(). src/bin/field_bench.rs benchmarks mul latency/throughput, deferred inner products, add/square/inv, and all mul variants. Verdict on M-series: F192 mul latency ~1.04x F128, deferred inner product ~1.5x; F160 strictly dominated (PMULL wastes half its width on 32-bit coefficients). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
F192 is the chosen field; the GF((2^32)^5) alternative is dropped (PMULL wastes half its width on 32-bit coefficients — it was strictly dominated). The benchmark and integration tests now cover F128 vs F192 only. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
WP1+WP3+WP4 of the 64-bit transition: - field/gf2_64.rs: first-class F64 (1-PMULL mul, primitivity test). - field/tower_f128.rs: F128T = K[y]/(y^2+y+x^61) (Artin-Schreier, trace-1 pinned). NEON-resident kernels: mul 5 PMULL with a vectorized pair fold, mul_base (K x E) 2 PMULL, square 5 PMULL. - ntt/additive_ntt_f64.rs: LCH additive NTT over K mirroring the F128 twin (interleaved SoA, fused 2-layer sweeps, cache-blocked parallel), inner loops on a NEON lane-pair butterfly kernel. - pcs/ligerito_k.rs: full recursive Ligerito prover + dense verifier committing F64 codewords (8-byte symbols) and folding/opening over F128T, including the sparse transposed-NTT basis induction and LIG_K_TRACE phase timing. Secure-profile shapes reused (soundness constants are F128-era pending a K derivation). 10 in-module tests: roundtrips, determinism, tamper rejections, dense==sparse induce. - bins: ligerito_bench (bits committed+opened per second, both per-bit and per-word framings) and commit_parts_bench (NTT/Merkle split). Measured (M-series, Secure, rate 1/2): per committed bit the K pipeline runs at 0.66-0.92x of the F128 one (2x elements per bit: one extra fold level and NTT layer at equal byte volume); per machine word (the VM view, where words halve from 128 to 64 bits) it is 1.04-1.16x faster while committing half the bytes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Port of recursive_verifier_with_basis_succinct to the K/F128T types: closed-form residual evaluation of the induced bases (K-side W-hat recurrence lifted by mul_base), byte-identical transcript replay against the prover (tapered fold-grinding indices, query sampling, alpha_last/beta_last after yr, index-consumption checks). Tests: 13 in ligerito_k (succinct roundtrips incl. the sparse-induce path, tamper rejections, dense/succinct verdict agreement over randomized tamper kinds); 35/35 lib-wide. The throughput bench's K correctness gate now runs through the succinct verifier. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
phi: F128 (GHASH) <-> F128T (tower over GF(2^64)), constructed offline (root of x^64+x^4+x^3+x+1 inside GHASH's 2^64-subfield via Cantor-Zassenhaus, Artin-Schreier solve for y, matrix inversion) and verified multiplicative/additive at build time and in tests (2000 random products). The 64-bit transition's flock boundary: the zerocheck (phi_8, GF(2^8) NTT, univariate skip) stays entirely in GHASH and its output claims map through phi before the K-committed ring switch, which is exact on bit-valued multilinears since phi fixes F_2. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The 64-bit transition's single ring switch (f = 64, e = 128, the note's unrelated-degrees case): pack_k (64 bits per F64 word, bit-identical to the old 128-bit packing reinterpreted), tensor_algebra_k (rectangular 64x128 transpose s_hat_v -> t_w, plus the square E-tensor algebra for succinct evaluation), ring_switch_k (prove/verify/verify_succinct with generalized prefix weights: plain eq for point claims, phi-mapped phi_8 Lagrange weights for flock's univariate-skip claim; eval_rs_eq_k via Theta = sum eq(q,y) (x) eq(z,y) folded by the r'' tensor). End-to-end tests reduce a bit witness claim through ligerito_k and verify dense + succinct; a claim-preserving s_hat_v forgery is rejected. 51/51 lib tests. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The K/F128T analog of open/verify_opening_batch_mixed_ligerito_stacked: point and strided stack claims plus ring-switched q_pkd claims (ring_switch_k) gamma-combined into one b_stack and target, opened by a single recursive_prover_with_basis_k over the full stack; succinct verification assembles the combined eval_b closure with prefix-amortized eval_rs_eq (an improvement over the F128 layer's per-position recomputation), handling both residual regimes. Tamper tests cover every claim kind; proof determinism pinned. 54/54 vendor tests. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The main-crate half of the 64-bit transition (transition doc WP5+WP7): machine words, memory cells, registers, immediates, table columns and the committed stack move to K = GF(2^64) (g = x, ord 2^64-1); every challenge, sumcheck/GKR value, bus fingerprint and evaluation claim lives in the tower E = F128T; the transcript stream is Vec<F128T> over a byte-identical sponge (shared lane helpers keep the GHASH-typed Challenger path in lockstep for the vendored flock code). - PCS: commit_k + the stacked batch-mixed K opening (stack_open_k), LOG_PACKING 6, Secure profile, 120-bit target kept. - BLAKE3 ISA: operands are 4-cell quads (12 value slots, 12 bus ops, PIN_SLOTS [0,1,2,3,18,19], stride K_LOG-6); q_pkd is the lo/hi flattening of flock's packed witness (layout unchanged, M_BASE=640 is 64-aligned). - flock boundary: the zerocheck stays GHASH; its (ab, c) claims cross into the tower via the field isomorphism with phi_8 Lagrange prefix weights and the full x_inner_rest ++ x_outer suffix (invariant asserted). - Instance caps: log_mem <= 32, per-table rows < 2^32, bytecode <= 2^32, keeping all g-power counting arguments exact under ord(g). - xmss: MD IV size element in GF(2^64); WOTS encoding re-budgeted to 21 digits per 64-bit word (grinding unchanged). cargo testall green (41 tests incl. xmss_vm and hash_chain); vendor untouched (54/54 flock-core, 17/17 flock-prover). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
doc.tex: the machine field is K = GF(2^64) (g = x, order 2^64-1) with the two-field convention stated once in the preliminaries (K-valued columns, E-valued challenges, |E| = 2^128); PCS section rewritten to the actual Ligerito Secure profile (K-commit, E-open, 120-bit, per-claim batching coefficients); BLAKE3 table at 4-word quads with 12 memory reads and the single f=64/e=128 ring switching crossed through the GHASH-to-tower isomorphism; instance caps and the counting bound R < 2^39 << ord(g); public input pinned to the shipped [F64; 2]. All pre-existing em dashes removed. transition-to-64-bits.tex: Status paragraph in the plan section: all work packages landed, testall green; two deltas versus plan (zerocheck kept in GHASH behind the isomorphism instead of retargeted; no flock-prover re-layout since M_BASE = 640 is 64-aligned); measured demo numbers. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The compiler lowered every indexed heap access as SET(const) + MUL + DEREF even though the DEREF instruction carries a compile-time offset exponent end to end (executor, constraint, bytecode bus). Constant g-power indices (1, GEN, GEN ** k, power-of-two literals, products of those, and the constant factor of buf[r * GEN**k]) now fold into beta at zero instruction cost across all five access paths (reads, stores, runtime blake3 and hint_witness slices). Also: GEN ** (expr) with compile-time integer expressions in the DSL, a branch-scoped constant cell cache (one SET per distinct constant per scope), x*1 / x+0 / if x == 0 identities, and direct-into-return-slot lowering. The XMSS aggregation program drops its now-redundant cursors (walk and Merkle tweaks are direct constant-indexed reads) and shares slot pointers per signature. Semantics, hint streams and the scheme are byte-identical. Cycles per XMSS verification (N=64): 4692.6 -> 3214.4, which is 7.4% BELOW the pre-transition 3472.7; at N=1024: 3200.8 cycles/XMSS, 108.3 XMSS/s, 666 KiB proof. Remaining above-baseline opcode is DEREF (+276/XMSS), the inherent 4-cell heap bridging width. testall green. LEANVM_PC_HISTO=1 now prints an executed-count histogram beside the disassembly (env-gated, zero overhead unset). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Profiling the XMSS aggregation (N=1024, 2^28-word stack) against main showed proving at 0.5x the old wall clock despite 7% fewer cycles; the gap was almost entirely allocation behavior, not arithmetic: - recursive_prover_with_basis_k now borrows the witness (&[F64]); the stacked opener passed stack.to_vec(), a 2.1 GB copy per prove. - b_stack is alloc_uninit + parallel zero fill; vec![F128T::ZERO; n] bypasses the calloc fast path and zero-wrote 4.3 GB single-threaded. - Point-claim folds: parallel gamma-seeded eq builder (build_eq_table_ext_parallel / _seeded_into) writing into one reused scratch buffer, then a multiply-free parallel accumulate; was a serial per-claim build_eq_table_ext (2.4 s of the open). Proof bytes pinned identical (bincode hash) before/after. - Removing the copies also takes the peak working set below the paging threshold, speeding every other phase. Also: F128T::mul2 batched NEON kernel (8 PMULL + 3 pair folds per two products, 40% faster on serial dependence chains) ships in the vendor for latency-bound callers; measurement showed the GKR loops are throughput/port-bound so they stay scalar, with rationale comments at each candidate loop. Two redundant unsafe blocks fixed (zero warnings). LEANVM_PROFILE now splits reduction/ring/stack-open and the bus phases; LIG_K_TRACE covers the stacked opener. XMSS N=1024: 105.9 -> 157.7 XMSS/s, proof 666.0 KiB unchanged. testall 41/41, vendor 56/56. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
ring_switch_k::prove: the suffix eq tensor now builds with the parallel builder (was 502 ms serial of the 714 ms total at the XMSS 2^28 stack); fold_1b_rows_k gains a method-of-four-Russians kernel (8-word transpose groups, two 16-entry subset-sum tables, one 8x8 bit transpose per byte position, density-independent) dispatched for multiple-of-8 lengths with the scalar bit-scan kept as fallback and an equality test across lengths. Ring-switch proves: 714 -> 205 ms. leaf::decompose_prove: claim values are transcript-independent within one decompose_formula call (no challenge sampled between claims), so all column MLE evaluations now run in one rayon pass and replay through the transcript in the original byte-identical order (debug assert re-derives serially). Decompose: 316 -> 39 ms. Proof bytes hash-pinned identical. XMSS N=1024: 157.7 -> 180.2 XMSS/s (main before the transition: 229.6). testall 41/41, vendor 57/57. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
New section benchmarking F128T (tower mul, mul2 pair), F64 (K x K) and mul_base (K x E) against the GHASH rows, closing the WP1 leftover. First numbers show the K kernels are implementation-bound, not math-bound: F64 at 0.64 ns/op throughput barely ties GHASH's full 128-bit mul at 0.70 (shift-XOR folds and NEON-to-GPR crossings burn the 1-PMULL budget), tower E x E at 3.41 vs 0.70. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Why the tower is not fundamentally slower than GHASH (measured field table, the three implementation gaps, the one structural serial fold), where the initial 2x wall-clock regression actually came from (memory cliffs and serial builds, all fixed transcript-byte-identical), the witness elements-vs-bits accounting, current phase profile vs main, and the ranked remaining work. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Rewrite of the GF(2^64) and F128T NEON multiplies at GHASH kernel quality: PMULL/PMULL2 products on register lanes (no GPR round trips mid-kernel), reductions via PMULL-by-0x1B folds with a TBL variant for the 4-bit second-order overflow, and a parallel 192-bit fold for the tower that eliminates the serial reduce-then-multiply-by-x^61 chain (word 1 folds by x^64 mod P, word 2 by x^128 mod P, the Frobenius square). NTT butterflies switch to the PMULL pair reduce. All variants exposed in field_bench; agreement tests (10k randoms per kernel) added; proof bytes hash-pinned unchanged. Measured (ns/op, latency / 8-chain throughput): F128T mul 10.10 / 3.42 -> 6.91 / 1.28 (GHASH ref 0.71) F128T mul_base 6.50 / 1.16 -> 5.14 / 0.70 F128T mul2 6.18 / 2.18 -> 3.49 / 1.46 F64 mul 4.84 / 0.64 -> 4.82 / 0.50 NTT (64 MB codeword): 6.7 -> 5.3 ms. End to end (XMSS N=1024): 178.6 -> 210.5 XMSS/s; gkr 1327 -> 939 ms; commit 969 -> 759 ms. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Scoreboard at 210.5 XMSS/s; new PCS head-to-head section: per-bit 0.79-0.88x (open-side element scaling), per-word 1.2-1.34x faster, and the padding accident doubling positions at the XMSS instance size. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Add MiB witness sizes per row and the plausibility decomposition of the 18 Gbit/s = 2.2 GiB/s figure (bandwidth-bound NTT + parallel BLAKE3). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The PCS tables and scoreboard now report GiB and GiB/s (bit-based rates read as bytes caused confusion); ligerito_bench prints GiB/s and MiB witness sizes. The field-question TLDR now states plainly that GHASH E x E is 1.8x faster per multiply today, attributes the origin (reduction granularity + tuning lineage, partly closable, ~1.2-1.4x probably inherent), and gives the design's actual answer: E x E is rare, surviving only in GKR at ~19% of the prove. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Port main's features onto the 64-bit GF(2^64) machine-word design:
- Flexible BLAKE3 on 64-bit words: the four input chunks (ins[0..3], each
spanning two consecutive cells) are addressed independently; the output
spans four consecutive cells. Five bytecode operand slots, five address
bindings, twelve memory reads per row. The DSL's copy/zero alias
forwarding becomes pair-aware (chunk_src): a chunk forwards only when its
two cells stay contiguous at the source, else it materializes.
- VM-native hashing over F64 words: vmhash::compress = the Blake3 opcode
(8 words in, 4 out), hash_slice's length-in-IV marker is now a K-field
g-power, and the vendored merkle leaf hash follows the same convention
(so a recursive verifier replays transcript, program digest, and PCS
leaves with one routine).
- VM-native Fiat-Shamir sponge: 256-bit chaining value = [F64; 4] advanced
only by the opcode compression, domain tags in the last block word,
E = F128T scalars as two K-lanes per block ("leanvm-b/transcript/v2").
- Program digest via vmhash::hash_slice (3 F64 words per op).
- Zerocheck/GKR keep the tower field but adopt main's free node-{0,1,g}
interpolation (new mul_by_g_e: lane-wise shift-fold on F128T), scratch
reuse, incremental eq-table folding, and ping-pong fold buffers.
- Compiler: main's @unroll inlining, GAddr/fconst compile-time folding,
alias forwarding, and compile-time if-folding coexist with the branch's
const-cell cache and beta-immediate folds (heap_addr falls back to
array_ptr's constant-factor fold).
- xmss_aggregate.py: 64-bit two-cell-value layout parametrized by the
host-supplied placeholders; branchless Merkle child ordering ported to
two words.
- JUMP inverse hints deferred to one batched Montgomery inversion; GPowMap
fast hasher keyed on F64's single limb.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ot loops Field level (vendor/flock-core tower_f128, the GHASH-parity move): - F128TUnreduced: the three unreduced Karatsuba sub-products of an E x E multiply, XOR-accumulated, one 5-PMULL reduction per sum (reduction is GF(2)-linear). 3 PMULL per term instead of 8. - F128TBaseUnreduced: the two unreduced lanes of a K x E mul_base, one reduce_pair per sum. 2 PMULL per term. - inner_unreduced_neon: register-resident deferred inner product; 0.62 ns/op = exact GHASH parity (was 1.36 per-term-reduced, 2.2x). - Three new single-mul kernel variants (vector-resident karatsuba/ schoolbook, schoolbook shift-tail) benched via field_bench --variants: none beat the default 8-PMULL parallel-fold; kept as alternates. Prover wiring (bit-identical proofs; reduction commutes with XOR): - GKR round message: the outer eq*(even*odd) products XOR-accumulate unreduced, one reduction per accumulator per round (bus 440 -> 385 ms). - Zerocheck round messages: same deferral of the outer eq*C products. - Bus leaf rows: the alpha-weighted coordinate sum accumulates raw mul_base lanes, one pair reduction per row. XMSS N=1024, 11 threads: 395 -> ~410 XMSS/s. field_bench is also simplified to the single F128-vs-F128T table (F192 and the old per-kernel sections removed; preflight now checks the two representations against each other through the explicit isomorphism). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The round messages (u_0, u_2) of round_msg_lsb_base/ext and both fused fold_and_msg kernels accumulated per-term-reduced products; they now XOR-accumulate unreduced parts (mul_base_unreduced / mul_unreduced) and reduce once per chunk. The fold writes `(1+r)x + ry` likewise pay one reduction instead of two. Bit-identical (reduction commutes with XOR). Initial sumcheck 129.5 -> 110 ms at XMSS N=820; the loop is near its memory-bandwidth floor, so wall-clock effect is small. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The K ring switch predated two optimizations the F128 layer got and never picked them up: - Split eq tensors (build_eq_split_ext + fold_ext_elems_split): the suffix tensor factors as eq_lo x eq_hi (2·2^(n/2) entries); entries are reconstructed on the fly for the rs_eq_ind fold, and the full 2^n tensor is never materialized. Field multiplication is exact, so reconstruction is bit-identical to the full build. - Precomputed s_hat_v: flock's reduction already captures the 128 bit-slice MLEs (WitnessClaim.s_hat_v); ring_claim now recombines them into the 64-wide K-packing values — 64-word y = 2y'+b is the b-half of 128-word y', so s64[i] = (1+c)·s128[i] + c·s128[i+64] with c the first inner-rest coordinate — and ring_switch_k::prove skips fold_1b_rows entirely (values hard-checked against the claim, transcript identical). RingSwitchClaimK gains an optional prover-side s_hat_v field (verifier bundles leave it None); the no-precompute fallback reconstructs the tensor from the factors and runs the standard fold. XMSS N=820: ring-switch proves 93 -> 39 ms (eq split 0.03 ms, s_hat 0.00 ms — matching main's front-end), stack open 576 -> ~522 ms. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Reconcile main's 8-crate workspace restructure + one-shared-transcript
protocol with this branch's 64-bit field transition (K = GF(2^64) machine
words opened over the tower E = GF(2^128)).
Structural: adopt main's `crates/*` layout and `fiat_shamir` crate; the
K-variant PCS files (ligerito_k, ring_switch_k, stack_open_k, pack_k,
tensor_algebra_k, additive_ntt_f64) and the tower field modules move under
crates/{pcs,primitives}. Hint machinery (RHint, GPowMap, grow_gpow) lives in
lean_vm::cpu::hints. Bench binaries move into their owning crates.
Field/transcript: the shared Fiat-Shamir sponge is F64-word / F128T-scalar;
the GHASH-typed F128 consumers (flock zerocheck/lincheck, the F128 Ligerito
twin) ferry through raw lane lifts (pcs::as_e / as_ghash) at their transcript
touchpoints - no arithmetic crosses representations. flock's reduction and
the F128 Ligerito are generic over the opening type so lean_vm can drive them
with its stacked Ligerito-K proof on one transcript.
Protocol: keep main's RLC-batched three-tree bus GKR, dedup'd claim
decomposition, and single-seed statement binding, retyped to E; keep the
branch's K-committed stacked opening as the sole PCS path (the F128 stacked
opener stays for its own tests).
Deferred: the n->1 recursion harness (crates/rec_aggregation/src/recursion.rs
+ guests/recursion.py) is gated behind the `recursion` feature - it dissects
the proof stream word-for-word and needs porting to the 64-bit-word layout.
Tests: workspace builds warning-free; primitives/fiat_shamir/pcs/flock/
lean_vm/lean_compiler/xmss and the XMSS-aggregation + fibonacci harnesses all
pass.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Memory words become 128-bit elements of the tower E = GF(2^128) so a recursion guest can do native 128-bit field arithmetic, while addresses, the pc/fp, read counters, operands, opcodes, and domain separators stay in the 64-bit subfield K = GF(2^64) (g-powers of order 2^64-1). This keeps the branch's base-field-commit / extension-open PCS win: only data costs 128 bits, addressing stays 64. Representation & protocol: - Each 128-bit word is committed as its two K-lanes (_lo/_hi), two ordinary F64 columns in the one stacked K-witness; the PCS/stacking/Merkle layer is untouched. The E-value is reassembled (lo + hi*y) only in the constraint zerocheck and at the opening point, never in the commitment. - MUL_NATIVE = the E tower product, XOR = 128-bit xor, both written as degree-2 E-relations on the value lanes, so the zerocheck is unchanged. - On the bus a memory value rides two K-coordinates (widest tuple stays 9); the memory image is two lanes; the public-input binding is one claim per lane. - Words used as addresses (DEREF pointer, JUMP destination/frame) are forced into K by the single-lane address/selection constraints, and witness-gen errors if such a word has a nonzero high lane. - BLAKE3: a 128-bit chunk is one cell, so a row reads six cells (four inputs, two-cell digest); the 12 value lanes map 1:1 onto the same 12 flock q_pkd slots (flock packing unchanged). DSL: - 128-bit literals: an integer literal is the raw 128-bit bit pattern (low 64 = K-lane, high 64 = y-lane); 2**64 is the tower generator y, so a guest packs two lanes as `lo + hi * (2**64)`. KVal::Const, lit_field, parse_const, try_field_const, const_cell, Alias::Const, and fconsts migrate F64 -> F128T; g-power/address constants embed via .into(). - blake3 lowering: a 256-bit operand is two 128-bit cells (chunk = one cell, digest = two cells). Guests: all hashing guests rewritten to the 2-cell layout and revalidated (6 blake3 .py programs, the stack_buf suite, the hash_chain benchmark, and the xmss aggregation guest + driver — WORDS_PER_VALUE 2->1, WORDS_PER_BLOCK 4->2, the WOTS encoding reconstructed into one cell via the y literal). The `recursion` harness stays feature-gated off (awaits its own guest port). Docs: doc.tex, transition-to-64-bits.tex, and zkDSL.md updated to the hybrid design. Full workspace test suite green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Brings in the signers-cache footprint fix, main's "unify equality table construction" and "make recursive proof verification atomic" refactors. Conflict resolutions (11 hunks, 5 files): - signers_cache.rs: clean merge (the fix originated on both sides identically). - multilinear.rs, constraints.rs, gkr.rs, pcs/ligerito.rs: kept the field-exploration (dual-lane) versions. main's changes here were purely the eq_table -> build_eq rename from "unify equality table construction", which merged the base's two eq-table constructors into one. That unification is invalid under the dual-lane design: here eq_table (over F128T, the VM constraint lane) and build_eq (over F128, the PCS lane) are DISTINCT functions for different field types, not duplicates. Taking main's rename would also have dropped ligerito's `crate::as_ghash` conversions that map tower-field samples into F128 for the PCS, breaking the K PCS path. - rec_aggregation/lib.rs: took main's new atomic-verification exports (RecursiveProof, RecursiveVerifyError, run_recursion) but kept them under field-exploration's `#[cfg(feature = "recursion")]` gate, since the n->1 recursion harness still awaits the 64-bit guest port. recursion.rs itself auto-merged to main's version (compiled only with the feature). Verified: `cargo build --release` (default features) and `cargo test --workspace` both pass (pcs 98, primitives 50, lean_vm 16, flock 74, rec_aggregation 3, xmss 7; no failures). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
F128 already had an x86_64 pclmulqdq path, but the tower field F128T and its F64 base had only an aarch64 PMULL kernel plus a naive software fallback, so on x86 every tower multiply ran software (~27 ns) while F128 used hardware clmul (~2.4 ns). Since the prover runs its whole polynomial arithmetic over F128T, that 11x per-mul gap made XMSS aggregation prove ~3x slower on x86 than on main, despite identical VM work (same cycles, instruction mix, and memory). Mirror the aarch64 kernels with x86_64 pclmulqdq: - gf2_64: one CLMUL product + a two-CLMUL fold by 0x1B (= x^64 mod P). - tower_f128: 3-CLMUL Karatsuba over the scalar coefficients, then the tower reduction c0 = reduce(p0) + x^61·reduce(p1), c1 = reduce(pm + p0); plus the deferred-reduction kernels (mul_unreduced/reduce, mul_base_unreduced/reduce) the sumcheck hot loop uses. Wired behind cfg(all(target_arch = "x86_64", target_feature = "pclmulqdq")); aarch64 and the software fallback are unchanged. Verified against the software oracle (new x86_variants_match_software test, 10k random cases: mul, square, and both deferred paths) and the full workspace suite (304 tests). On this AMD box, xmss --n-signatures 820 goes 53.6 -> 136.3 XMSS/s (proving 15.3s -> 6.0s); the deferred inner product goes from 11.7x to 1.10x of F128. Credit: binius64 <https://github.com/binius-zk/binius64> for the GF(2^64) base-field CLMUL and the deferred-reduction structure (its Monbijou field is this same GF(2^64)); the degree-2 extension differs (ours is Artin-Schreier y^2+y+x^61, not their y^2+xy+1), so the extension reduction follows our field. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… tower Adds F128Txy, a GF((2^64)^2) tower K[y]/(y²+x·y+1) — binius64's tower choice — over the same base field K as tower_f128's Artin-Schreier K[y]/(y²+y+x^61). Same 3-CLMUL Karatsuba products; only the degree-2 fold differs (a shift-by-x vs a multiply by x^61), so benchmarking the two isolates the tower choice. Carries only the ops the comparison needs (eager mul, the deferred- reduction pair, square, inv), with an x86 pclmulqdq path plus a software fallback, and tests for the defining relation, field axioms, deferred- reduction linearity, and x86-vs-software agreement. field_bench grows a third column (C: F128Txy) and a C/B ratio that isolates the fold difference. On x86 the binius fold wins every mul-bound metric (C/B 0.58–0.85x); the deferred inner-product loop is the lone exception at ~1.13x, where per-term reduction is amortized away. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
F128Txy shipped with only an x86 pclmulqdq path and a software fallback, so on aarch64 the field_bench head-to-head ran it in scalar software while the Artin-Schreier tower (F128T) used NEON PMULL — a ~60x apples-to-oranges gap that made the tower comparison meaningless on M-series. Add a NEON kernel that mirrors tower_f128's so only the degree-2 fold differs: 3-PMULL Karatsuba products, then each output limb reduced with the same two-PMULL tail. The binius fold y^2 = x*y + 1 folds one word fewer than the Artin-Schreier x^61 fold (a 128-bit p1<<1 vs a 192-bit fold), so mul_neon is 7 PMULL vs F128T's 8. Also route mul_unreduced and the deferred kreduce_u128 through NEON, and add a test that both NEON paths (fused mul_neon and mul_unreduced_neon + reduce) match the software reference over 10k inputs. With the fold now measured fairly on M4 Max (field_bench C/B): binius wins the throughput-bound muls ~0.87-0.92x and ties on latency/deferred — same direction as x86 (0.58-0.85x) but a smaller margin, since abundant PMULL throughput shrinks the one-word fold saving. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Correct the MLE interpolation identity, configurable Ligerito rates, bus soundness degree, BLAKE3 read bound, bytecode shape, recursive transcript framing, and closed-form ring-switch evaluation. Remove obsolete deferred u32 material and distinguish the general ring-switch reduction, GHASH example, and F64/F192 recursion specialization. Refresh README benchmarks on the current branch and host, publish branch-local specification source alongside the main PDF link, and make all three LaTeX notes compile without warnings. Run LaTeX checks on pull requests and add release-mode workspace test, strict clippy, and strict rustdoc CI.
Compile documentation pull requests in read-only jobs, while reserving contents: write for main-branch and manually dispatched release publication.
`DBG_PROF` gave per-function cycle counts, but the recursion guest spends most of its cycles in one 180k-instruction straight-line function and in ~1,100 lowered loops whose `__loopN` names say nothing. Four dumps make that legible: - `DBG_PROF_DUMP=path`: the raw per-pc counts plus the function table, so an offline pass can bucket one function's straight-line cycles by source region (the `SET fp[x] = g^<entry>` of each lowered loop's call site is a landmark, and lowered code follows source order). - `DBG_LOOPS=1`: prints `__loopN in <fn> for <var> in <bound>` at lowering. - `DBG_DISASM=path` / `DBG_PLACEHOLDERS=path`: the guest disassembly and the baked constants, to read alongside the profile. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Frame cells are write-once, so a cell holds one value for the whole run and value numbering needs no dataflow analysis. Dropping a repeated pure op (SET of a constant, XOR, MUL) is then a local rewrite. About 5% of the recursion guest's instructions were exact repeats: addresses recomputed per access, the loop counter advanced twice per iteration, and constants re-materialized in each fresh frame. Three restrictions keep it sound, and all three come from write-once memory: only pure ops (a DEREF is a memory equality that rides the bus), only cells written once in the function (this is what protects the XOR-then-SET assert idiom), and only local cells, since the caller writes a callee's arguments and reads its returns out of the callee frame. The pass is block-local: folding across a branch could point a read at a cell the taken path never wrote, and an unwritten cell is prover-chosen. tests/cse.rs pins the cases where a duplicate is not dead: a constant returned from a function, duplicated call arguments, both arms of a branch setting the same constant, and a failing assert still conflicting. DBG_NO_CSE=1 disables the pass, DBG_CSE=1 reports it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A pooled claim's low_eq is the prefix product of (1 + p_k + ris_k) over its point buffer p. The factors depend only on WHICH buffer the claim reads, never on the claim, so all 162 claims were running the same product loop and stopping at different lengths: 136 on rho, 18 on the qpkd/rho pair, 5 on zeta, 3 on pi. Build one prefix-product chain per buffer and let each claim read the partial product at its own certified length. Chain entry t is built only from inputs with index < t, so a garbage tail past a buffer's written extent cannot corrupt a shorter prefix, and the existing length pins keep every read inside the written span (low_len <= cplen <= the buffer's extent, and nlow <= lenris). 1,440,752 -> 1,337,348 guest cycles at --n 2 --log-inv-rate 2. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The eval_b terminal needs final_msg's multilinear at each claim's y-slot point. It built the full eq tensor of the point (a 2^(cap+1) buffer per claim) and dotted it against final_msg. Successive folding gives the same value with about half the work and no tensor buffer: each coordinate contributes the pair (1 + p_k, p_k) either way. The slot coordinates now go straight into fold weights in frame cells, so the fold reads them as instruction operands. 1,337,348 -> 1,284,210 guest cycles. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The padding-surplus ladder and the placement-offset rebuild both need 1 + g^(2^k) once per bit, and both were loading g^(2^k) from the g_squares heap buffer and adding one, every time. Precompute the 34 values into a StackBuf, where each entry is an instruction operand rather than a load. 1,284,210 -> 1,265,034 guest cycles. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The coordinate weights and the F2-linear batching map determine each other:
weights[w] = Phi(b_w), and Phi's linearized coefficients are
c_k = sum_w weights[w] * dual_w^(2^k). We fixed the weights first, as rho^w,
which forces a generically FULL 192-term Phi and a closed form (baked orbit
tables, a geometric series) just to build its coefficients. A recursive
verifier's cost is linear in the term count, so fix the coefficients instead:
Phi(v) = sum_{l < 64} rho^l v^(2^l), weights[w] = Phi(b_w).
Soundness improves. For an error delta on the transposed columns, fixed before
rho, the check misses it only if sum_{l<64} rho^l W_l = 0 with
W_l = sum_w b_w^(2^l) delta_w. Writing w = 64m+i and b_w = x^i y^m, W_l splits
over the K-basis {1, y^(2^l), y^(2*2^l)} (Frobenius fixes K setwise and
[E:K] = 3 is prime), and each K-part is the Moore matrix of K's power basis
applied to delta, which is invertible. So delta != 0 forces some W_l != 0 and
the error survives with probability at most 63/2^192, against 191/2^192 before.
64 terms is also the floor: with 3|S| < 192 K-equations in 192 K-unknowns a
nonzero delta lies in the kernel for every coefficient choice.
The transcript is unchanged (still one rho). Deletes the closed-form machinery
and its baked tables. The Rust test column_weights_match_the_row_side_
linearized_map pins the column/row identity the guest relies on, and the Python
reference verifier is updated in lockstep. Documented in ring-switching.tex.
1,265,034 -> 1,116,326 guest cycles.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Each bus block ran its own (gamma + fp_b)^DELTA square-and-multiply over
COUNT_BITS bits. Every flush block of a table takes its kappa from the same
certified source (tau_t) and its real row count from the same count_t, so a
whole group shares one DELTA and
prod_b (gamma + fp_b)^DELTA == (prod_b (gamma + fp_b))^DELTA,
which is one ladder per (side, table): 14 instead of 82. The DELTA pin is now
per group and uses the same certified count_gpows[t] and g^(2^tau_t) each block
read before, so it states the same thing.
The framework blocks are REAL_IS_FULL_CUBE, which equals N_TABLES, so the table
loop skips them: real = 2^kappa makes DELTA = 0 by construction and their
ladder was forced to return 1 anyway, since g^DELTA == 1 with COUNT_BITS bits
far below the group order pins every bit to zero. Dropping it removes a hint,
not a constraint.
1,116,326 -> 1,057,626 guest cycles, and the program now fits a 2^19 bytecode
cube instead of 2^20, which halves the bytecode table and takes native verify
from 57ms to 32ms.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A Cell deref unifies the two cells it names, so writing a value into a heap slot that already holds one IS an equality check, at one instruction instead of the three an assert takes (load, XOR, SET). The Ligerito level roots were read off the stream into level_roots_*, then compared against each query's recomputed root; storing the recomputed root back into the same slot states the same thing. 1,057,626 -> 1,056,498 guest cycles. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
decode_query_bits reconstructs the squeezed word from its 192 hinted bits and cuts it into query positions. Both were per-bit: one constant multiply for the position, another for the reconstruction, plus an XOR/SET booleanity assert. Inside one 64-bit limb the coordinate basis is the polynomial basis, so COORD_BASIS[s + b] = COORD_BASIS[s] * COORD_BASIS[b] with no reduction. A group's whole contribution to the reconstruction is therefore one multiply by the position value it already forms. Groups that straddle a limb boundary split into the two runs that stay inside a limb, and the position recombines as p_lo + X^cut * p_hi, which concatenates the bit runs. Booleanity becomes a store of t*t back into the cell that holds t, saving the XOR and SET. Every bit is still boolean-constrained and the full 192-coordinate reconstruction is still asserted, so the positions stay pinned to the squeezed word. The group identity is exact, not a relaxation. 1,056,498 -> 1,014,306 guest cycles. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The per-level residual folds final_msg against the novel-basis weight pair (1, w), not (1 + w, w), so half of fold_final_msg's multiplies were by the constant 1. fold_monomial_msg computes lo + w*hi per level instead. 1,014,306 -> 998,558 guest cycles. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
An opened row above level 0 arrives as flat K limbs, three per F192 word. The loop read all 24 limbs to build the packed cells for the leaf hash, then read them all again to reassemble the words for the row dot. A pack holds lane(2k) + Y*lane(2k+1) exactly, so once the limbs are in frame cells, word w is one multiply-add off the pack covering its even limb pair: the even-w case adds Y^2 * limb(3w+2) to a pack, the odd-w case shifts a pack by Y and adds limb(3w). Identical values, since PACK64X2 already forces every limb into K and pins the packed cell. 998,558 -> 987,560 guest cycles. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
TomWambsgans
force-pushed
the
small-proof
branch
from
August 1, 2026 21:05
8e78199 to
b02e6e3
Compare
The note ended with a GHASH worked example and a "recursion specialization"
that derived a closed form for coefficients we no longer compute. Both are
gone. In their place, one section that develops the case we actually run,
f = 64 and e = 192 over K = GF(2^64) and E = K[Theta]/(Theta^3 + Theta + 1):
- the two specializations, stated separately, since only the second is new:
batching with one challenge rather than an eq tensor is what folds the
weighted claim into the PCS opening, and that holds for any weights;
- the choice of map. The weights and the map determine each other, and the VM
pays per nonzero coefficient of the map, so we fix the map at 64 terms and
let the 192 weights follow;
- why 64 terms suffice: the coordinate splits over the K-basis {1, u, u^2} of E
because [E:K] = 3 is prime, and the remaining systems are Moore matrices of a
basis of K, hence invertible. Error 63/2^192;
- why 64 is the floor: the error map sends K^192 into K^{3|S|}, so a support
below 64 leaves a kernel error that passes with probability one;
- where the verifier applies the map, and what it costs.
doc.tex 13's appendix carried the old dense-weight definition, its 191/2^192
bound and the deleted closed form; it now matches, and cites the note for the
optimality argument. Both PDFs build clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Inline fixed-depth Merkle path verification in the recursion guest, saving 13,248 cycles on the canonical 2-to-1 benchmark while keeping the bytecode within the existing 2^19 domain.\n\nReplace the 64-multiplication ring-switch linearized map with a composition of six two-term Frobenius maps at shifts 32, 16, 8, 4, 2, and 1. The composition retains all 64 Frobenius terms required to bind the 192 transposed coordinates, but applies the map with 63 squarings and six general multiplications. This saves another 36,178 guest cycles.\n\nAccount for the exact total challenge degree below 2^32 in the Rust and Python Ligerito parameter derivations. Keep the native prover, native verifier, recursion guest, and standalone Python verifier transcript-compatible. Add tests for full Frobenius support, distinct challenge monomials, the degree bound, and agreement between the composed and expanded maps.\n\nUpdate the generalized ring-switching note and protocol documentation to describe the implemented construction and its soundness argument.\n\nThe release recursion --n 2 benchmark falls from 1,248,296 to 1,198,870 guest cycles (-49,426, 3.96%) with 521,594 instructions, still padded to 2^19.
# Conflicts: # crates/lean_compiler/src/lower.rs
The note sampled the batching point in the packing field F_{2^f} and ran
the reduction's sumcheck there. At f = 64 that caps soundness around
2^-58, so it does not describe what the code does: the challenges, the
weights and the Ligerito opening point are all F192, and only the packed
witness is F64.
Introduce L, a field containing both F_{2^f} and F_{2^e} and large enough
that 1/|L| is negligible. The batching scalars are sampled in L, the
sumcheck runs over L, its output point lies in L^m, and the soundness
error becomes (2m + l)/|L|. Fact 2's map lands in L rather than in an
ad hoc compositum. In the worked example the compositum of K and E is E
itself and 192 bits suffice, so L = E, and the Schwartz-Zippel bound is
now stated over E: sampling in K instead would give only 2^-32.
The example is presented as an example, with no reference to a
particular system. Along the way, notation and proofs:
- X and Y for the tower generators, no residue sentence; the hypercube
variable becomes z, freeing y; the product basis is indexed by i and j
and the m coordinates by n; the six challenges are gamma_p, no longer
colliding with the packing degree f; the recurrence index is p, no
longer colliding with t_w; Phi_s, B_s and T_s keep the subscript.
- lambda_w is now used in every display that defines it away.
- Argue what was asserted: irreducibility of Y^3+Y+1 over K, that the
six shifts hit every Frobenius exponent once with its own monomial,
and that the claim map is a bijection because it transposes the bit
matrix. Type the input a of the recurrence.
- Fact 1 takes neutral dummies, since it is also applied to non-Boolean
arguments; the example's cost no longer omits the squaring ladder.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Port main's arbitrary-prefix GKR optimization to the F192 small-proof implementation. The prover omits trailing identity leaves while preserving the verifier and proof format byte-for-byte. Release benchmarks before this merge commit: - recursion --n 2 --log-inv-rate 2: ~4.91 -> 4.631 s - xmss --n-signatures 890 --log-inv-rate 1: ~6.54 -> 6.445 s Validation: release GKR tests and the complete release workspace suite on the identical F192 change.
The note derived a general reduction between two unrelated extension
degrees and then instantiated it. Nothing else uses the general form, and
the generality cost a layer of notation: an ambient field L, two abstract
bases, the transposed claims t_w, and an eq-tensor batching that the
instance immediately replaces.
Rewrite it for the concrete case. K and E are gone; the two fields are
written out as F_2^64 and F_2^192 throughout. The reduction is now derived
rather than specialized: fix an F_2-linear Phi, take the weight
Phi(eq(r,z)), and the completeness identity falls out because the bit
slices pass through Phi.
The soundness argument is rebuilt around what makes 64 the right number
of Frobenius terms:
- The transpose is no longer imposed up front. It appears as one line of
index bookkeeping on the error, so the 192 F_2^64-coordinates show up
when the argument needs them.
- The Moore matrix is replaced. For fixed j the 64 equations say that a
polynomial of degree at most 63 vanishes at the 64 distinct conjugates
of X, so it is zero.
- Necessity is a dimension count: 192 unknowns over F_2^64 against 3 per
term, so the support needs 64 terms, and 64 terms give exactly 192
equations.
- The coefficients of the drawn map have a closed form,
c_k = prod_{p : k_p = 1} gamma_p^(2^(k mod 2^(5-p))), from which the
degree bound behind 2^-160 follows instead of being asserted.
Reviewed by four agents. They found the soundness criterion as first
written was unsatisfiable (it asked a fixed map to have trivial kernel on
a space of 192 F_2^64-dimensions mapping into 3), and that the drawn
map's support is only generically full. Both are fixed. Every equation,
every field constant and every cost figure was re-derived independently,
and the description was checked against crates/pcs/src/ring_switch.rs.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Each doubling level of `eq_table` did two field multiplies per pair — one by `r` and one by `1 + r`. In characteristic 2 the second is redundant: `e · (1 + r) = e + e · r`, so the low child is the high child XOR the parent. That halves the multiplies in every eq-table build, and is orthogonal to the existing note about batching: `rk` is loop-invariant either way, and the scalar product still beats `F192::mul2` here. The table was also built fully sequentially, though a level's pairs are independent. Levels wide enough to cover rayon's dispatch now split across threads. `eq_table` is on the verifier's path (the lean_vm constraint and GKR verifiers, and flock's univariate skip re-export it), so the new test keeps a verbatim copy of the old implementation and asserts equality element by element — random points on both sides of the parallel threshold, plus every Boolean point up to n = 10, where `1 + r` collapses to 0 or 1 and a representation difference would be most likely to surface. Measured in isolation on AMD Ryzen 7 PRO 8700GE (Zen 4), RAYON_NUM_THREADS=12, `xmss --n-signatures 890 --log-inv-rate 1`, against the same branch with only this commit reverted, medians of 13 interleaved rounds, Mann-Whitney z: bus grand-product 859 -> 833 ms -3.03% (z=+4.3) whole prove 6260 -> 6220 ms -0.64% (z=+3.1) That matches the -2.8% (z=+6.2) the same change measured on main's F128 tree, which is the cross-check worth having: the identity is field-agnostic, and so is the gain. Credit: https://snark.fast/ Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VJ32hU5mFQs5yLxdNAuqaL
The prover sizes rayon's global pool to the performance-core count and pins its workers to USER_INTERACTIVE QoS, so on Apple Silicon the efficiency cores sit idle for the whole proof. Widening the main pool to include them is a known regression, not a win: kernels that partition into one equal band per worker gate their barrier on the slowest core, so a band landing on an E-core stalls every P-core at the join. `primitives::epool` takes the opposite shape — the main pool is untouched, and a separate UTILITY-QoS pool of `hw.perflevel1.logicalcpu` threads drains the *same* atomic chunk queue. Because chunks are claimed one at a time rather than partitioned up front, a slow E-core simply claims fewer of them and owns at most one outstanding chunk at the join. Merkle leaf and parent hashing are the natural consumers: fixed-size independent groups, no cross-group dependency, one join at the end. Chunk `g` writes only its own output range, so the result is identical whichever pool claims it — this is byte-oriented and so carries over from the F128 tree unchanged. Off Apple Silicon, and whenever the sysctl probe fails, there is no helper pool and the queue falls back to rayon's ordinary split; with `RAYON_NUM_THREADS=1` it runs inline and spawns nothing. Measured together with the eight-wide BLAKE3 kernel that follows: both land on L0 hashing and this run did not separate them. See that commit. Credit: https://snark.fast/ Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VJ32hU5mFQs5yLxdNAuqaL
Upstream BLAKE3's NEON `hash_many` is degree 4. Within one 4-lane state the sixteen compression words form a single add/xor/rotate dependency chain, and a 4-lane state occupies only half of AArch64's 32 vector registers — so the chain, not the issue width, sets the pace. Keep two independent 4-lane states in flight and interleave them instruction-for-instruction inside the G function. That doubles the independent work available to the out-of-order engine at every step while still fitting both states and both message blocks in registers. Generalized over leaf size rather than pinned to 1 KiB as on main: this branch commits an F64 L0 codeword, so a leaf is 64 lanes x 8 bytes = 512 bytes, and the recursion levels use other widths again. Any positive multiple of 64 up to 1024 is exactly one whole BLAKE3 chunk, which lets the kernel pin the rest of the contract — unkeyed, counter zero, CHUNK_START on block 0 and CHUNK_END | ROOT on the last. Each output is then byte-identical to `blake3::hash(leaf)`, which the new tests check against the blake3 crate at all five dispatched sizes and for batches that are and are not multiples of eight. Remainders finish on upstream `hash_many`, so no padding or over-read is needed. Measured on M4 Max, RAYON_NUM_THREADS=11, via `tests/pcs_throughput.rs` at PCS_LOG_N=24 rate 1/2, medians of 15 interleaved rounds, Mann-Whitney z — this commit plus the efficiency-core pool before it: L0 hashing 23.10 -> 13.50 ms -41.6% (z=+4.3) commit total 51.20 -> 42.70 ms -16.6% (z=+4.1) L0 NTT 31.40 -> 29.70 ms -5.4% (z=+0.4, untouched) open 118.70 -> 120.00 ms +1.1% (z=-0.1, untouched) 512-byte leaves are 8 dependent compression blocks rather than the 16 a 1 KiB leaf gives, so there was reason to expect the two-state ILP trick to have less to hide behind here. It does not: the gain is larger than the -28.6% measured at 1 KiB on main. Credit: https://snark.fast/ Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VJ32hU5mFQs5yLxdNAuqaL
At the top layers each NTT layer is a separate full-buffer sweep, so the pass count — not the arithmetic — sets the cost: the codeword does not fit in any cache, and every sweep is a DRAM round-trip of the whole buffer. The existing fused-2 kernel already halves that; radix-8 applies three layers per pass and cuts the remaining sweeps by another third. This branch's lane kernel is already 8-wide on both NEON and AVX-512, so unlike the F128 version on main there is no lane batching to add — the eight participating rows simply stay L1-resident across all twelve butterflies, the same way the four rows do in the fused-2 kernel. Also adds real coverage for the fused passes. `interleaved_lanes_are_independent_ntts` runs at `log_d = 7`, below the driver's `log_d < 8` bail-out, so it only ever exercised the scalar path and passed vacuously for everything in the parallel driver, fused-2 included. The new test uses shapes with `n_top >= 3` (which is what selects radix-8) and a non-zero `start_layer`, since the commit path enters at `log_inv_rate`. Verified by mutation: perturbing one twiddle in the new kernel makes it fail. Measured on M4 Max, RAYON_NUM_THREADS=11, via `tests/pcs_throughput.rs` at PCS_LOG_N=24 rate 1/2, medians of 15 interleaved rounds, Mann-Whitney z: L0 NTT 57.30 -> 51.60 ms -10.0% (z=+2.3) commit 103.50 -> 81.70 ms -21.1% (z=+3.1, includes the hashing commits) open 244.70 -> 242.10 ms -1.1% (z=+1.0, untouched) Two caveats on that run: the host was in a degraded state (absolute times were ~2x an earlier run of the same binaries), and z=+2.3 is marginal. The result is kept because the direction matches the mechanism — one third fewer full-buffer sweeps — and matches the same change on main, which measured -15.9% (z=+7.3) on the F128 NTT. Credit: https://snark.fast/ Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VJ32hU5mFQs5yLxdNAuqaL
`hash_leaves_batched_uninit` dispatched only powers of two, so any other leaf width fell through to the `par_iter` arm that hashes one leaf at a time with no cross-leaf SIMD at all. The Ligerito recursion levels hit exactly that: they commit F192 rows, so a leaf is `num_interleaved * 24` bytes — 192 at the eight-lane levels. A multiple of 64, so still exactly one BLAKE3 chunk and perfectly valid for `hash_many`, but not a power of two, so it missed every batched arm. Add 192, 384 and 768 alongside the existing widths. These also flow into the eight-wide NEON kernel, which already generalizes over any multiple of 64 up to 1024. The tests cover all eight dispatched widths against `blake3::hash`. Not separately benchmarked: the throughput harness reports L0 hashing, and these are the recursion levels, which it does not break out. Credit: https://snark.fast/ Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VJ32hU5mFQs5yLxdNAuqaL
Two changes to the tiled partial-fold inner kernel:
* The 8 z index bytes of a stripe are consecutive, so read them with one
unaligned 8-byte scalar load and shift them out of the register instead of
issuing eight LDRBs. The kernel already spends a table load per index; a
second load per index nearly doubled its load-port pressure for data that
was already in a register.
* Sweep stripes in pairs and fold both table lookups into each vector
accumulator with a single EOR3 (ARMv8.2 SHA3, enabled by the workspace's
`-C target-cpu=native`). That halves the accumulator updates and the
serial dependency chain through each of the 8 live accumulators. Only the
`c0`/`c1` limbs benefit — `c2` is a scalar u64 and just takes two XORs,
which is why the gain here is smaller than on main's F128 tree.
Both are exact: the fold is a plain XOR-sum over stripes, so regrouping the
terms cannot change the result. Verified by mutation — dropping one paired
term makes the existing lincheck tests fail.
Measured on M4 Max, RAYON_NUM_THREADS=11, `xmss --n-signatures 890
--log-inv-rate 1`, medians of 25 interleaved rounds, Mann-Whitney z:
Flock reduction 535 -> 530 ms -0.93% (z=+2.0)
whole prove 4150 -> 4150 ms 0.00% (z=+0.4)
z=+2.0 is marginal, and the effect is too small to show at whole-prove
granularity. Kept because the direction and rough magnitude match the same
change on main, which measured -2.1% on this phase (z=+4.9), and because it
is strictly fewer loads and a shorter dependency chain.
Credit: https://snark.fast/
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VJ32hU5mFQs5yLxdNAuqaL
TomWambsgans
force-pushed
the
small-proof
branch
from
August 3, 2026 06:45
44cb3b1 to
0103bab
Compare
x86 had no tiled fold kernel at all: `partial_fold_packed_z_best` routed AArch64 to the register-tiled NEON gather and sent every other target to the generic `partial_fold_packed_z_fast_padded`. `VPTERNLOGQ` is the exact counterpart of AArch64's `EOR3` — an arbitrary three-input bitwise function in one instruction — so immediate 0x96 (`a ^ b ^ c`) folds a paired-stripe accumulate the same way. F192 is `#[repr(C)]`, so a 128-bit load at `&c0` covers the `(c0, c1)` pair exactly as the NEON kernel's `vld1q_u64` does; `c2` stays scalar in both. The iblock/oblock drivers and the oblock threshold are widened from `target_arch = "aarch64"` to also cover x86-64 with AVX-512 + AVX-512VL. Measured on AMD Ryzen 7 PRO 8700GE (Zen 4), RAYON_NUM_THREADS=12, `xmss --n-signatures 890 --log-inv-rate 1`, medians of 13 interleaved rounds: Flock reduction 770 -> 763 ms -0.91% (z=+2.8) whole prove 6500 -> 6510 ms +0.15% (z=-1.1) Significant on its own phase but small in absolute terms — 7 ms of a 6.5 s prove, 0.11%. It is kept because it closes a real platform gap rather than for the number: the generic path x86 was taking is evidently already decent, which is itself the finding. Correctness is covered by the existing lincheck tests on x86, verified by mutation (dropping one paired term fails them). Credit: https://snark.fast/ Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VJ32hU5mFQs5yLxdNAuqaL
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
1 participant
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.
using an extension field of 192 bits (a tower of degree 3 over F_2^64)