Small proofs by TomWambsgans · Pull Request #4 · leanEthereum/leanVM-b

TomWambsgans · 2026-07-18T11:29:09Z

using an extension field of 192 bits (a tower of degree 3 over F_2^64)

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>

@unroll

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>

Fix pcs.tex thm:mca-johnson against the primary source (BCHKS25 Thm 4.6, list correlated agreement): the theorem parameter is max(ceil(sqrt(rho)/eta), 3), not the ceil(sqrt(rho)/(2 eta)) of the non-list Thm 1.5 that Flock's Thm 8 quotes, and rho is the slightly reduced rate (k-1)/n. The implementation (johnson_m_param, reduced_rate) already had both right. In ligerito.rs, name misc/pcs.tex as the soundness source of truth and map thm:rbr's per-verifier-message error table onto the validate() checks (max semantics, per-transition 128 bits); replace dangling references to a former appendix. Remove the dead UDR regime (never constructed in production), making eta and expected_eps_ood_bits plain f64. Fix the OOD diagnostic doc (192, not 128) and the INITIAL_FOLDING_FATOR typo. Update doc.tex's PCS paragraph: per-level optimized eta (not 0.02) and 17-bit query grinding (queries close the remaining 111 bits). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The initial sumcheck is the dominant phase of the K-PCS open (~57% at log_n=24), and it allocs+faults two fresh ~100 MB F192 buffers (nf, nb) every fold round, then frees them — the allocator munmaps on drop, so every prove re-pays soft page faults on first touch. Route the fold outputs through the existing F192 scratch pool (primitives::scratch) via a new fold_out_buf helper, and give the consumed input buffers back in SumcheckProverK::fold, so repeated proves reuse resident pages instead of faulting fresh mappings. x86_64-gated to match flock (pooling here measured slower on aarch64, which keeps the fresh-alloc path). Correctness: F192 has no Drop and every fold slot is written before read, so recycled (stale) buffers are sound; all 55 pcs tests pass incl. the log_n 12/16/18 roundtrips. Measured (log_n=24, LIG_K_TRACE, steady state): initial sumcheck ~0.175 s -> ~0.063 s (~2.8x) total open ~0.31 s -> ~0.18 s (~1.7x) Ports the buffer-pooling idea from flock (github.com/succinctlabs/flock), commit "perf: add x86 AVX-512 prover acceleration" (the scratch-pool reuse for the initial-sumcheck fold). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Remove the Ligerito/Ligerito-K split and promote the F2^64-committed implementation to the canonical pcs::ligerito API. - move the shared security/configuration machinery into a private ligerito_config module and re-export it through pcs::ligerito - rename pack_k, ring_switch_k, stack_open_k, and tensor_algebra_k to their canonical module names - drop K suffixes from commitments, proofs, configs, ring-switch types, stack-opening types, helpers, and transcript aliases - migrate lean_vm, flock, recursive aggregation, throughput tests, guest comments, and protocol documentation to the canonical API - keep dense verifier and ring-switch reference paths only for tests, excluding unused helpers from production builds - remove stale compatibility terminology and the superseded extension-field implementation - preserve the existing NEON and AVX/AVX-512 optimized kernels unchanged Verified with: - cargo check --workspace --all-targets - cargo test --workspace --release - PCS_LOG_N=16 PCS_LOG_INV_RATE=1 PCS_SAMPLES=1 cargo test --release -p pcs --test pcs_throughput -- --ignored --nocapture - RAYON_NUM_THREADS=11 cargo run --release -- recursion --n 2 --log-inv-rate 1 - RAYON_NUM_THREADS=11 cargo run --release -- xmss --n-signatures 820 --log-inv-rate 1 - git diff --check

Introduce a VM instruction that reads two F_2^64 memory words and packs them canonically as one F_2^192 word with limbs (lo, hi, 0). Enforce source subfield membership and destination packing through literal-zero memory-bus coordinates, so the invariant is proof-enforced rather than only checked during witness generation. Wire the opcode through execution, traces, AIR, bytecode, layouts, transcript binding, table counts, statistics, and recursive-verifier shape handling. Preserve the existing BLAKE3 Transcript192 mode; no mixed packing mode is needed. Expose pack64x2(a, b) in zkDSL and use it in recursion.py to constrain every serialized Merkle-leaf limb before reassembly, hashing, and row-dot evaluation. Add end-to-end proving and invalid-extension-source tests, Python stubs, and VM/zkDSL documentation.

Remove the Transcript192 BLAKE3 mode and its alternate opcode, leaving one canonical 128+128-bit encoding throughout the VM. Shrink the BLAKE3 AIR table from 51 to 31 columns and reduce its local constraints to the five address bindings while the memory bus and Flock validity proof bind the canonical lanes. Add computed F192 limb advice and destination-target PACK64X2 support, including nested inline zkDSL helpers for transcript absorption, challenge reconstruction, and constrained conversion between canonical Merkle cells and Ligerito transcript words. Update recursion witness generation, documentation, and regression coverage accordingly.

Replace explicit challenge-power expansions across VM AIR constraints, recursive zkDSL verification, and quadratic sumchecks with Horner evaluation. Add shared native and zkDSL helpers for efficient F192 limb reconstruction, mirror every AIR formula on both sides, and update compiler documentation and examples. Include the repository-wide cargo fmt pass.

# Conflicts: # crates/flock/src/blake3.rs # crates/flock/tests/blake3_batch.rs # crates/lean_vm/src/blake3_flock.rs # crates/lean_vm/src/cpu/layout.rs # crates/lean_vm/src/cpu/mod.rs

Brings in main's standard-BLAKE3-chaining protocol (b94b315, b788b1c) ported onto this branch's 192-bit three-lane words, plus the SIMD-batched Merkle hashing, hierarchical tracing and pretty-print reconciliation (both originated here; main's ports superseded where they diverged), and the signers-cache encoding-predicate fingerprint. The chaining port, adapted to canonical 128-bit chunks embedded in 192-bit cells: Op::Blake3 gains a chaining-value base offset (two consecutive cells, each read through the bus as (lo, hi, 0) so the canonical embedding is proof-enforced and the zero top limbs are never committed) and a 128-bit metadata immediate carried in the two low K-lanes of a 192-bit word whose lanes ride two public bytecode slots. The instruction encoding grows from six to nine public columns and the bus from nine to twelve coordinates; the stacked bytecode polynomial takes four selector bits. The BLAKE3 table adds the CV operand/address, two CV memory reads, and the sixth address binding; its eighteen value lanes are virtual, routed to the generalized flock witness (cv words 0..4, metadata words 18..20). The flock circuit takes cv/counter/blen/flags as free input rows with the re-baked family digest, and the branch's bilinear circuit walk is updated to match. vmhash::hash_slice, PCS Merkle leaves, xmss tweak hashes, and the program digest switch from the Merkle-Damgard length-in-IV construction to standard BLAKE3. Guest updates: the recursion guest packs each queried leaf row into a contiguous cell run (level 0 packs two hinted F64 lanes per cell via PACK64X2; deeper levels pack the three serialized F192 limbs per word likewise, preserving the limb K-membership proof) and hashes it as chunk-chained standard BLAKE3 through per-level LIG_LEAF_BLOCKS (level 0: n/8 blocks of 8-byte lanes; deeper: 3n/8 blocks of 24-byte words); the BLAKE3 zerocheck branch grows to six Horner-batched address bindings. The xmss guest uses cv-chained sub-hashes (146 compressions per signature, down from 158). The compiler keeps pack64x2/pack64x2_into/hint_f192_limbs alongside the new blake3 keyword surface and lazy per-scope IV cells (SET from IV_CELLS, registered in the const-cell cache). Kept from this branch where main's ports lagged: the log-inv-rate CLI and per-proof PCS rates, the F64 Ligerito implementation (main's tracing landed in deleted code), the prepared-reduction-witness plumbing, and the per-64-bit-word WOTS encoding. Full workspace suite passes, including both recursion 2-to-1 tests (mixed rates included), xmss aggregation, and main's chaining regressions adapted to three-lane words. The ignored recursion_soundness_binds test fails identically on the pre-merge HEAD (a pre-existing breakage on this branch, not a merge regression). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Merge branch 'main' into small-proof # Conflicts: # crates/flock/src/blake3.rs # crates/flock/tests/blake3_batch.rs # crates/lean_vm/src/blake3_flock.rs # crates/lean_vm/src/cpu/layout.rs # crates/lean_vm/src/cpu/mod.rs flock: reuse prepared reduction witness Retain the fused A·z, B·z, and lincheck layouts created with q_pkd and consume them after commitment instead of regenerating the witness. Add env-gated reduction phase timing and exercise the prepared path in the batch harness. Support StackBuf returns from normal functions Use Horner evaluation for challenge polynomials Replace explicit challenge-power expansions across VM AIR constraints, recursive zkDSL verification, and quadratic sumchecks with Horner evaluation. Add shared native and zkDSL helpers for efficient F192 limb reconstruction, mirror every AIR formula on both sides, and update compiler documentation and examples. Include the repository-wide cargo fmt pass. Simplify recursion hashing to canonical BLAKE3 cells Remove the Transcript192 BLAKE3 mode and its alternate opcode, leaving one canonical 128+128-bit encoding throughout the VM. Shrink the BLAKE3 AIR table from 51 to 31 columns and reduce its local constraints to the five address bindings while the memory bus and Flock validity proof bind the canonical lanes. Add computed F192 limb advice and destination-target PACK64X2 support, including nested inline zkDSL helpers for transcript absorption, challenge reconstruction, and constrained conversion between canonical Merkle cells and Ligerito transcript words. Update recursion witness generation, documentation, and regression coverage accordingly. Add PACK64X2 base-field packing instruction Introduce a VM instruction that reads two F_2^64 memory words and packs them canonically as one F_2^192 word with limbs (lo, hi, 0). Enforce source subfield membership and destination packing through literal-zero memory-bus coordinates, so the invariant is proof-enforced rather than only checked during witness generation. Wire the opcode through execution, traces, AIR, bytecode, layouts, transcript binding, table counts, statistics, and recursive-verifier shape handling. Preserve the existing BLAKE3 Transcript192 mode; no mixed packing mode is needed. Expose pack64x2(a, b) in zkDSL and use it in recursion.py to constrain every serialized Merkle-leaf limb before reassembly, hashing, and row-dot evaluation. Add end-to-end proving and invalid-extension-source tests, Python stubs, and VM/zkDSL documentation. Document MCA error in unique-decoding regime Pretty-print displayed integers with commas pcs: make F64 Ligerito the sole implementation Remove the Ligerito/Ligerito-K split and promote the F2^64-committed implementation to the canonical pcs::ligerito API. - move the shared security/configuration machinery into a private ligerito_config module and re-export it through pcs::ligerito - rename pack_k, ring_switch_k, stack_open_k, and tensor_algebra_k to their canonical module names - drop K suffixes from commitments, proofs, configs, ring-switch types, stack-opening types, helpers, and transcript aliases - migrate lean_vm, flock, recursive aggregation, throughput tests, guest comments, and protocol documentation to the canonical API - keep dense verifier and ring-switch reference paths only for tests, excluding unused helpers from production builds - remove stale compatibility terminology and the superseded extension-field implementation - preserve the existing NEON and AVX/AVX-512 optimized kernels unchanged Verified with: - cargo check --workspace --all-targets - cargo test --workspace --release - PCS_LOG_N=16 PCS_LOG_INV_RATE=1 PCS_SAMPLES=1 cargo test --release -p pcs --test pcs_throughput -- --ignored --nocapture - RAYON_NUM_THREADS=11 cargo run --release -- recursion --n 2 --log-inv-rate 1 - RAYON_NUM_THREADS=11 cargo run --release -- xmss --n-signatures 820 --log-inv-rate 1 - git diff --check pcs: vectorize F192 NTT with AVX-512 improve hierarchical PCS tracing primitives: add AVX-512VBMI bit transpose enable tracing remove 128 bits fields make tests pass add pcs_throughput benchmark pcs/ligerito_k: pool the initial-sumcheck fold buffers (x86_64) The initial sumcheck is the dominant phase of the K-PCS open (~57% at log_n=24), and it allocs+faults two fresh ~100 MB F192 buffers (nf, nb) every fold round, then frees them — the allocator munmaps on drop, so every prove re-pays soft page faults on first touch. Route the fold outputs through the existing F192 scratch pool (primitives::scratch) via a new fold_out_buf helper, and give the consumed input buffers back in SumcheckProverK::fold, so repeated proves reuse resident pages instead of faulting fresh mappings. x86_64-gated to match flock (pooling here measured slower on aarch64, which keeps the fresh-alloc path). Correctness: F192 has no Drop and every fold slot is written before read, so recycled (stale) buffers are sound; all 55 pcs tests pass incl. the log_n 12/16/18 roundtrips. Measured (log_n=24, LIG_K_TRACE, steady state): initial sumcheck ~0.175 s -> ~0.063 s (~2.8x) total open ~0.31 s -> ~0.18 s (~1.7x) Ports the buffer-pooling idea from flock (github.com/succinctlabs/flock), commit "perf: add x86 AVX-512 prover acceleration" (the scratch-pool reuse for the initial-sumcheck fold). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Align Ligerito RBR soundness doc and implementation Fix pcs.tex thm:mca-johnson against the primary source (BCHKS25 Thm 4.6, list correlated agreement): the theorem parameter is max(ceil(sqrt(rho)/eta), 3), not the ceil(sqrt(rho)/(2 eta)) of the non-list Thm 1.5 that Flock's Thm 8 quotes, and rho is the slightly reduced rate (k-1)/n. The implementation (johnson_m_param, reduced_rate) already had both right. In ligerito.rs, name misc/pcs.tex as the soundness source of truth and map thm:rbr's per-verifier-message error table onto the validate() checks (max semantics, per-transition 128 bits); replace dangling references to a former appendix. Remove the dead UDR regime (never constructed in production), making eta and expected_eps_ood_bits plain f64. Fix the OOD diagnostic doc (192, not 128) and the INITIAL_FOLDING_FATOR typo. Update doc.tex's PCS paragraph: per-level optimized eta (not 0.02) and 17-bit query grinding (queries close the remaining 111 bits). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Merge branch 'main' into small-proof pcs.tex (a note on WHIR/Ligerito over binary fields, interpreted as List binding PCS Use query grinding to reduce proof size Optimize Johnson eta per recursive level Use aggressive recursive RS rate schedule Audit and tighten Ligerito soundness parameters Correct the BCHKS25 Johnson proximity-gap parameter to use ceil(sqrt(rho) / eta), and evaluate the theorem at the reduced RS rate (K - 1) / n instead of the nominal encoding rate. Move the global Johnson slack from 0.02 to 1/160, retaining more than 128.8 bits of proximity-gap soundness without grinding while reducing query counts and proof size. Validate exact, unrounded query, proximity, OOD, list-unioned algebraic, and degree-191 ring-switch errors. Clarify the round-by-round security claim and add production-profile regression tests for all supported rates and witness sizes. Make Ligerito rate proof-local and recursion-generic Pass log_inv_rate explicitly through proving instead of process-global state, announce and validate it through Fiat-Shamir alongside layout sizes, and derive commitment/opening parameters from the transcript-bound value. Embed all supported rate/size configurations in the recursion guest so one program can verify mixed-rate inner proofs, while letting the CLI-selected rate independently configure both inner and outer proofs. Add CLI validation, the environment-driven query-count report, mixed-rate regression coverage, and update the README. Move Ligerito to 128-bit Johnson list decoding Raise the global round-by-round soundness target to 128 bits and derive the production Ligerito ladder in the Johnson list-decoding regime over GF192 with eta 0.02. Use the post-commit L0 opening claim as its implicit binding evaluation, and add one explicit OOD evaluation for each recursive commitment. Port those OOD claims through the GF64-committed prover, dense and succinct native verifiers, proof encoding, recursion hint builder, and in-VM recursion verifier. The GF192 margin makes the query, proximity-gap, and OOD-binding terms each clear 128 bits without query or fold grinding. Add parameter assertions and OOD tamper coverage, and update the security documentation. Validated with all PCS, Flock, LeanVM, and recursion release tests, recursion --n 2, and xmss --n-signatures 820. The recursion proof drops from 579.1 KiB to 518.3 KiB and guest cycles from 2,842,984 to 2,591,048. Optimize GF192 ring switching in recursion Factor the GF192 trace-dual basis over its GF64 degree-three tower, replacing the dense 192-by-192 Frobenius table with smaller base and tower tables. Assert the factorization while constructing guest placeholders. Evaluate the two transposed claims and their transparent ring-switch weights in lockstep so they share coefficients, powers, and verifier-weight loads. This reduces the recursion --n 2 guest from 3,235,330 to 2,842,984 cycles (12.1%), the proof from 610.7 to 579.1 KiB, and measured proving time from 13.50s to 9.22s. Merge field-exploration into small-proof Bring over native BLAKE3 circuit-walk verification, compiled recursion-guest caching, and clarified division-by-zero semantics. Adapt the verifier paths and cache key to GF192. Deliberately omit the bus-grinding changes from 97d9c687cd01fbec9987172f56abd810fa2299d7. doc recursion: cache the compiled guest across verifies RecursiveProof::verify recompiled the recursion guest on every call (~235 ms), dwarfing the ~20 ms of actual proof checking. The guest is a pure function of the inner bytecode and the batch size, so recursion_guest_arc caches compiled guests process-wide, keyed by (fs_seed(inner_program), nsub) and capped at 8 shapes, compiling outside the lock (mirrors blake3_flock::setup_for). verify borrows the pristine cached Arc; prover paths clone an owned copy for their witness streams (cpu::Program now derives Clone). Complete recursive verify: 268 ms -> 18.7 ms once a shape is warm, now dominated by the Ligerito opening. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Native verifier evaluates A0/B0 by circuit walking The native verification of a recursive proof paid the ~21M substituted nonzeros of the BLAKE3 matrices twice: check_reduced contracted two eq tables through them to discharge the deferred v_a/v_b claims (~11 ms, forcing the ~300 ms matrices build), and lincheck::verify materialized the alpha-batched column marginal via the CSC fold (~1.2 ms + one-time 22 ms transpose). bilinear_walk_pair (flock.pdf, Circuit walking) computes u^T A0 w and u^T B0 w in O(circuit) field ops (~43 us) by walking the unsubstituted compression cascade over F128T wire values, mirroring build_matrices row for row; a randomized cross-check test ties it to the materialized matrices. check_reduced now walks. lincheck::verify no longer folds comb_vec through the rounds: the final consistency check collapses to one bilinear form against the rank-1 column weight w_col[c] = z_partial[c_skip]*eq(r_inner_rest, c_rest), answered by the new LincheckCircuit::bilinear_form (WalkLincheckCircuit; default None falls back to the marginal + inner product). Transcript unchanged. Proof checking drops ~31 ms -> ~20 ms per recursive verify. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Document the GF192 machine field Update the VM and proving-system specification from the old quadratic GF128 representation to the implemented cubic tower E = GF64[y]/(y^3 + y + 1). Describe three-limb memory words, arithmetic, immediates, memory interactions, instruction tables, and public-input openings. Clarify that BLAKE3 uses canonical 128-bit values embedded in full GF192 cells with a zero top limb, and record that the larger challenge field eliminates grand-product grinding under the instance caps. Also distinguish the zkDSL's 128-bit literal syntax from its 192-bit machine-word type. Use univariate batching for GF192 ring switching Replace the padded eight-challenge coordinate cube with powers of one GF192 Fiat-Shamir challenge. Share that challenge across stacked ring-switch claims and retain the existing GF64 transpose and GF192 transparent-weight evaluation paths. In the recursion guest, compute the trace-dual linearized coefficients directly with Horner evaluation. This removes the equality tree and coordinate-weight buffer, reducing the recursive verifier by 1,510 instructions and 76,746 VM steps relative to the padded baseline while retaining better than 184 bits of batching soundness. feat: migrate recursion and PCS to F192 Move the protocol challenge and machine-word field to the cubic F192 tower while retaining F64 physical columns and canonical 128-bit BLAKE3 cells. - add portable, x86, and AArch64 F192 arithmetic with deferred-reduction kernels - carry all three limbs through the compiler, ISA, trace tables, Flock reductions, transcript, GKR, and public-input binding - generalize K-packed Ligerito, ring switching, tensor algebra, query sampling, and Merkle serialization to 192-bit challenges and folded words - update the recursion guest AIR, claim descriptors, memory binding, packed queries, and Merkle verification, including the rho-point fix for virtual BLAKE claims - remove grand-product bus grinding under the F192 soundness budget and account for the actual 2^192 Ligerito challenge field - refresh DSL documentation and tests, and keep the large BLAKE3 batch benchmark as an explicit release-only benchmark Clarify division by zero semantics Fix bus grinding soundness bound pcs: batch F64 NTT butterflies with NEON docs: align field architecture documentation pcs: batch F64 NTT butterflies with VPCLMUL pcs: optimize tower-field stacked openings Merge branch 'main' into field-exploration pcs: avoid redundant basis initialization work cpu: transmit the PI low lane so the guest skips Frobenius extraction The public-input binding needs both K-lanes of MEM(r) = interp(pi, r) as opening claims. The lane values are deterministic from the seeded pi, but a recursive verifier can't cheaply slice F64 lanes out of the E-valued pi — the old guest recovered them with two 64-squaring Frobenius loops. Instead, transmit the low lane v_lo = MEM_LO(r) (one scalar) and deduce the high lane v_hi = (MEM(r) + v_lo)*Y^-1 from the pi-derived E-value. The guest replays it as one scalar read + one multiply — no Frobenius, no X_INV. This nets a simplification: bind_pi_claim is a single helper returning [ColumnClaim; 2] (reusing multilinear::interp), the transcript add_scalar/ next_scalar is inline at each call site, and the now-dead X_INV constant + its Frobenius baking are deleted (guest and harness). Transcript and claim order are unchanged from the two-lane binding, so it stays sound. Validated in release: cpu 8/8; recursion_2to1, _mixed, _soundness_binds (tamper-rejection), _generic_many all pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv flock: restore standalone BLAKE3 batch benchmark Merge branch 'tower-only-flock' into field-exploration field: remove GHASH and use tower field throughout unify Ligerito protocol configuration sponge: carry the domain-separation tag in lane 2 (main convention) The v2 sponge bound the DS tag in the 4th compress lane, which forced the recursion guest to encode its tags as `k << 64` (the tag in the F128T high lane). Move the tag to the 3rd lane (right after the up-to-two data words) so the guest's tags are plain `1,2,3,4,5` again, matching main's convention. The tag lane is a pure convention (all five values stay distinct and nonzero, so domain separation is unchanged); byte-absorb blocks now carry two data words (16-byte chunks) instead of three, since the tag takes the third lane. Validated end-to-end in release: cpu 8, pcs 103, flock 77, recursion_2to1 + mixed, and recursion_soundness_binds (tamper-rejection) all pass — prover, verifier, and the in-VM guest replay agree on the new transcript. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv recursion: remove the `recursion` feature gate (harness is ported) The gate + `unimplemented!` stub existed only because the recursion harness was unported to the 64-bit machine; now that it works end-to-end, drop the feature so the `recursion` module and the real `run_recursion` are always compiled. `cargo run --release -- recursion --n 2` runs the aggregation with no extra flags (verified: 2 inner proofs aggregate and the recursive proof verifies). Also removes the now-dead `uk` base-field encoder. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv recursion: port the N->1 aggregation to the 64-bit tower protocol Make the in-VM recursion guest verify N->1 recursive proofs on the 64-bit (K=F64, extension F128T) protocol. Each fix addressed a constant or convention that coincided under the old GHASH / 128-bit packing (LOG_PACKING=7) but diverges in the tower with 64-bit packing (LOG_PACKING_K=6): - tower ring-switch trace-dual basis, derived by the same construction over the tower's coordinate basis and verified against the duality property - Fiat-Shamir domain-separation tag in compress lane 3 (the tower sponge) - bit-decomposition reconstruction in the real F128T coordinate basis; the field generator's powers span only F64, so g^i is not the coordinate basis - two-lane 128-bit memory public-input claims (MEM_LO/MEM_HI) via Frobenius lane extraction of the bound public-input words - AIR constraint formulas re-ported for the LO/HI memory split - K-opener transcript realigned to its F128 reference that the guest replays: ordered d-bit-chunk query sampler + surfaced query squeezes, scalar Merkle root binding, 64-wide s_hat_v, struct-based Ligerito observed-scalar replay, and the SLOT_STRIDE_LOG = K_LOG - LOG_PACKING_K terminal identity Validated: recursion_2to1 and recursion_2to1_mixed verify honest recursive proofs; recursion_soundness_binds rejects every tampered hint (the in-VM verifier genuinely binds); pcs 103, cpu 8. No check was weakened or stubbed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv flock: migrate the verifier to the binius tower (F128T) Move flock's verifier (zerocheck + lincheck + the blake3 reduction) to the binius tower field F128T, so a downstream in-VM verifier replays a single field instead of the two-field GHASH/tower bridge. The fast GHASH prover is unchanged (the shift_reduce univariate-skip optimization stays). It now bridges its transcript messages and claims through the real ghash<->tower isomorphism instead of the bit-copy reinterpretation, so its outputs are genuine tower values the F128T verifier checks. The blake3_flock boundary is native tower (no isomorphism on point/value/weights); only the prover-only s_hat_v capture still crosses. Adds the tower phi8 embedding (iso-image of the GHASH basis, exhaustive homomorphism test, images land in F64) and a tower lagrange-weight helper. Validated: 77 flock tests and 8 cpu prove/verify + tamper-rejection tests pass; workspace builds clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv lean_vm: drop the DEREF pointer's always-zero HI lane (K-valued address) The DEREF pointer is constrained to K by `a2 = p·obe` (a2 is a single-lane K address), so its high lane is provably 0. Commit it as a single K lane (deref::P) instead of P_LO/P_HI, with the memory read carrying a literal 0 high lane via the new FlushBuilder::memory_k. The bus balances only if the stored value's HI lane is also 0, which the K constraint guarantees — sound; a debug_assert pins p.c1 == 0 at fill time. Removes one committed column of zeros from the most frequent instruction's table (DEREF, 571/XMSS): committed witness 2^26.180 -> 2^26.170 (~0.7%). Branch-specific (only the 128-bit-memory-word design gives an address a HI lane); no main equivalent. All prove/verify tests pass. Not applied to the JUMP d/f destination words: they are only forced into K on taken branches (b=1); a not-taken branch reads an unconstrained memory word, so forcing HI=0 would reject valid traces. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Merge commit 'b956c4d' into field-exploration # Conflicts: # crates/flock/src/zerocheck.rs Merge commit 'b7e1be2' into field-exploration # Conflicts: # crates/flock/tests/blake3_batch.rs # crates/lean_vm/src/pcs.rs # crates/pcs/src/ligerito.rs Merge commit '9e957fc' into field-exploration # Conflicts: # crates/fiat_shamir/src/sponge.rs # crates/pcs/src/merkle.rs Merge commit '2905de0' into field-exploration # Conflicts: # crates/lean_vm/src/leaf.rs Merge commit '7b74709' into field-exploration # Conflicts: # crates/primitives/src/multilinear.rs Merge commit '086f622' into field-exploration # Conflicts: # crates/lean_vm/src/pcs.rs Merge commit 'b336897' into field-exploration # Conflicts: # crates/lean_vm/src/cpu/layout.rs Merge commit '11e799f' into field-exploration # Conflicts: # crates/lean_compiler/src/lower.rs Merge commit 'a825bf6' into field-exploration # Conflicts: # crates/flock/src/zerocheck.rs # crates/lean_vm/src/tables.rs Merge commit 'bd8b31b' into field-exploration Merge commit '53077e5' into field-exploration field: switch the VM's extension field E to the binius64 tower Make the binius64 tower K[y]/(y^2 + x*y + 1) the shipped degree-2 extension field E, replacing the Artin-Schreier tower K[y]/(y^2 + y + x^61). Same base field K = F64 and identical repr(C){c0,c1} layout, so the ~1,200 call sites are untouched: F128T now names the binius tower (tower_f128.rs, formerly the tower_f128_xy investigation variant), and the old Artin-Schreier tower is kept as F128TArtin (tower_f128_artin.rs) for the field benchmarks only. - Build binius up to full field parity before the swap: From<F64>, AddAssign, the mixed K x E path (mul_base / mul_base_unreduced / a BaseUnreduced accumulator, all tower-independent), Serialize/Deserialize/Hash, the Y const. - Re-derive the GHASH <-> tower isomorphism (iso_f128.rs) for y^2 = x*y + 1. The K-embedding is tower-independent (X unchanged), so only the Y columns move; the j=0 block is byte-identical to the old matrices. gen_iso_xy.rs regenerates and verifies them (100k random multiplicativity + round-trips), replacing the lost scratchpad/iso.py. Correctness verified on aarch64: the whole workspace builds and every test passes -- pcs prover/verifier round-trips, lean_vm (VM, GKR, constraints, the leaf mixed K x E path), and blake3_flock (which maps claims through the re-derived iso at the flock boundary), plus all integration tests. This is the correctness migration only; the batched fold-kernel speedup that motivated it lands separately. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> remove superseded zerocheck kernel field benches: wire the VPCLMULQDQ batched inner product field_bench: new 'inner prod, VPCLMUL' row (x86 vpclmulqdq+avx512f only) running the batched Karatsuba kernel (B=2) for F128T and F128Txy — ~5.5-6.9x the scalar 'deferred' row (0.37 vs 2.3-2.6 ns/term), and it collapses the tower gap from C/B 1.12x (scalar) to 1.00x: wide CLMUL erases binius's deferred-inner-product deficit without flipping it. Banner now reports the VPCLMULQDQ backend. inner_bench: the noise-robust comparator is now generic over the field, with an x86_64 backend ranking scalar-deferred vs vpclmul kara/school at bank counts 1/2/4 for both towers, plus a best-of-each head-to-head. Findings on Zen4: Karatsuba beats schoolbook (0.367 vs 0.393 ns/term) — the reverse of M-series, where PMULL is cheap enough that schoolbook's extra product buys dropping the pre-XOR; on x86 CLMUL throughput is the bound, so the extra CLMUL loses. B=2 wins the bank sweep. Confirms the schoolbook win was Apple-specific. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> field: AVX-512 VPCLMULQDQ batched inner-product kernels for both towers Adds field/vpclmul.rs, a shared AVX-512 batched Karatsuba accumulator: one VPCLMULQDQ does four independent 64x64->128 carry-less products (one per zmm lane), folding four field elements per CLMUL. Two variants — karatsuba_acc (3 CLMUL + shuffle/XOR pre-mix) and schoolbook_acc (4 CLMUL, no pre-mix) — both return the same (Sum p0, Sum p1, Sum pm) triple with a const-generic bank count for ILP. Both degree-2 towers gain inner_unreduced_vpclmul_{kara,school}<B> in their x86_64 modules. F128T and F128Txy are repr(C){c0,c1} with identical layout, so the accumulate is shared; each kernel only supplies its field-specific reduce, reusing the already-tested Unreduced::reduce(). Only the batched accumulate is new arithmetic. Tests check the batched kernels against the scalar deferred reference across 18 lengths (including partial vector groups and the <4 scalar tail), both kernels, bank counts 1/2/4, on both fields. Gated on target_feature vpclmulqdq + avx512f (Zen4 / Sapphire-Rapids-class); -C target-cpu=native enables both. The CLMUL stays 128-bit per lane — this batches four, it does not widen the field multiply. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> field: schoolbook batched inner-product NEON kernel + noise-robust comparator inner_unreduced_neon (the deferred sum_i a_i*b_i hot-loop kernel) was Karatsuba, 3 PMULL/term. On M4 Max PMULL is not the bottleneck, so dropping the per-term am/bm Karatsuba pre-XOR (2 DUP + 2 EOR) in favour of one extra PMULL wins: schoolbook products run ~1.25x faster. inner_unreduced_neon now dispatches to inner_unreduced_school::<2>; inner_unreduced_kara is retained as the comparison alternate. field_bench's "inner prod, NEON kernel" row: the tower kernel drops 0.58 -> 0.47 ns/op. The win was isolated with a noise-robust comparator (bin/inner_bench): it interleaves every method round-robin (rotating order) and ranks by the MINIMUM time across many rounds -- noise only ever adds time, so the min is the cleanest estimate of true speed -- with a per-round win-count as corroboration. That methodology overturned two single-pass "wins" as pure measurement noise: accumulator banking (x1 == x2 == x4) and slice bounds-check removal both do nothing here. Only the schoolbook-vs-Karatsuba product choice moves the number. Also make the field_bench CLMUL-backend banner architecture-aware so it no longer prints "numbers not meaningful" on x86 (which has a real pclmulqdq path), and notes that path is 128-bit CLMUL, not VPCLMULQDQ. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> field: aarch64 NEON path for the binius64 tower (F128Txy) 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> centralize Merkle root encoding centralize F128 byte encoding field: add binius64 degree-2 tower and bench it vs the Artin-Schreier 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> simplify bus claim decomposition share multilinear field helpers naming derive column sizes from layout sources wip field: add x86_64 pclmulqdq path for GF(2^64) and the F128T tower 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> reuse compiler constant pool simplify challenge and table construction deduplicate deterministic test rngs generate phi8 table from basis images Merge branch 'main' into field-exploration 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> signers cache: fold hash-construction fingerprint into the footprint The signer cache filename hashed only the declared XMSS parameters (slot, key range, message, V/W/CHAIN_LENGTH/...). Those are identical across branches that change the hash *construction* underneath — e.g. the Merkle-Damgard IV switching field width (GF(2^128) <-> GF(2^64)) rewrites every digest while touching no constant. Both branches then computed the same filename and the serialized sizes match, so a run on one branch loaded the other's cryptographically-invalid signers and panicked in verification. (cargo clean masked it by wiping the poisoned file.) Fold a known-answer test vector of the real primitives (one tweak_hash, one md_tweak_hash) into footprint(), so any change to digest behavior lands in a distinct cache file. Per-branch caches now coexist instead of clobbering one another. Two BLAKE3 compressions; negligible next to generating a signer. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> unify equality table construction make recursive proof verification atomic vm: 128-bit memory words (E) with 64-bit addressing (K) 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> Merge branch 'main' into field-exploration 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> recursion guest: runtime-sized buffers replace the linear capacity caps HeapBuf sizes carried in the exponent (HeapBufDyn: the alloc hint does an O(1) reverse g-power lookup at witness generation, erroring past 2^20 cells) already existed - the guest now uses them wherever the exact size is a certified runtime g-power at declaration time: - zerocheck_r / flock_point chains: exactly m = K_LOG + tau_5 slots (mr1cs_g); zerocheck_rhos / flock_round chains: exactly m - 6 (mr1cs_g * INV_GEN^6). R1CS_M_CAP and R1CS_ROUNDS_CAP die. - zeta and the nine GKR per-layer chains: exactly mu (+2) slots (g_bus_mu), zeta's declaration moving below the certified bus depth. What stays capacity-sized, and why: STREAM_CAP / YR_SLOT_STRIDE size hint pools (witness-hint lengths are compile-time); QPKD_VARS_CAP and MU_CAP are row STRIDES of two-row / triangle layouts (a runtime stride would unfold every access); GKR_ROUNDS_CAP / GKR_POINTS_CAP are quadratic in mu (a runtime g-power for them needs exponent-domain multiplication, all cost, no cycles saved). recursion_2to1 cycles 2,516,990 -> 2,517,066 (+76: one MUL per materialized runtime size) against exact allocations. Suite 244 + 3 ignored green, heavy recursion suites pass, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Merge pull request #2 from leanEthereum/recursion Recursion ligerito: the fold constants are one knob each - INITIAL_K=5 works Changing INITIAL_K / LEVEL_K / RESIDUAL_MAX_LOG in crates/pcs now propagates everywhere: - lean_vm's LOG_BATCH and LOG_INV_RATE stop re-declaring their own 6 / 1 behind compile-time asserts: they ARE ::pcs::ligerito::INITIAL_K / LOG_INV_RATE_0 (the Merkle leaf width and the L0 fold count are one knob by construction - the L0 commit is reused). The blake3_batch test reads the constants too. - recursion_soundness_binds stops hardcoding the residual shape: the rs_yslot_bits tamper index (the first PADDING slot coordinate, k = yr_log_n) is derived from the fold ladder, and the tamper is skipped when this candidate's yr_log_n equals YR_LOG_CAP (the guest reads only YR_LOG_CAP coords, so no pad coordinate exists and the over-read path it guards is absent - exactly what happens at INITIAL_K=5). Verified by actually flipping the knobs: the FULL workspace suite, both heavy recursion suites, and the xmss CLI all pass at INITIAL_K=5 (the guest re-derives its baked tables from the config, so recursion just works); pcs + rec_aggregation pass at LEVEL_K=4. Shipped values are unchanged (6 / 3 / 5), so derived configs, proofs and cycles are byte-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> ligerito: LigeritoProfile dies; the shipped shape becomes named constants Only one configuration ever ships (the old Secure profile), so the selector enum and its Fast/Slim derivation arms go. What was implicit now has a name in crates/pcs/src/ligerito.rs: - SECURITY_BITS = 120 round-by-round soundness target - LOG_INV_RATE_0 = 1 L0 code rate 2^-1 - QUERY_GRINDING_BITS = 18 query-phase PoW (queries cover 120 - 18) - INITIAL_K = 6 the INITIAL folding factor (L0 folds 2^6 interleaved rows; = PcsParams::log_batch_size) - LEVEL_K = 3 the folding factor of every subsequent level - RESIDUAL_MAX_LOG = 5 folding stops at <= 5 remaining variables: the residual yr (<= 32 coeffs) is sent in clear derive_profile(m, profile) -> derive_config(m); PcsParams loses its profile field; lean_vm pins its LOG_BATCH / LOG_INV_RATE / SECURITY_BITS to the pcs constants with compile-time asserts. The SoundnessRegime enum and the Johnson/OOD analysis + prover/verifier machinery stay for hand-built configs (the OOD roundtrip test constructs them directly); only the profile-driven derivation of them is gone. Derived configs are value-identical to the old Secure profile, so proofs and the recursion guest are untouched (cycles unchanged). Suite 244 + 3 ignored green, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> recursion verifier: derive positions-per-word from depth The Ligerito query decoder took per_word as a separate Const, but it is just FIELD_BITS / depth. Derive it inside decode_query_bits and drop the LIG_POSITIONS_PER_WORD placeholder (guest table + Rust export + caller arg); the write-offset now uses FIELD_BITS // LIG_TREE_DEPTH directly. Pure refactor: identical 128/depth packing, identical emitted code, no cycle change. Removes a redundant parameter and a placeholder threaded through the guest; the decode specialization collapses from __L{depth}_L{per_word} to __L{depth}. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> zkDSL: print(...) - a prover-side debug print `print(expr)` / `print("label", expr)` displays a value at witness generation: the expression evaluates into a cell and a Print hint hangs on a one-instruction no-op anchor, so it fires exactly at that program point, only on the executed path, and adds no constraints (nothing enters the transcript; proving/verification are untouched). The label defaults to the argument's source text. Output goes to stderr as `[print] label = ...` with the friendliest reading: decimal for small integers, g^k for small g-powers, both when they overlap (8 = x^3 shows as `8 (g^3)`), hi:lo hex otherwise, `<unwritten>` for a cell nobody wrote. Allowed inside @inline bodies and loop bodies (free vars flow through). Documented in zkDSL.md; test: tests/print_debug.rs. Suite 244 + 3 ignored green, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> compiler: @inline calls in expression position; eq_weight dedup covers all 4 sites Two compiler-level changes, found while deduplicating the recursion guest's eq-tensor weight loops: 1. @inline calls now work embedded in expressions. An inlined tail return of ANY plain var recorded a RetBind::Gaddr alias (gaddr_of treats every runtime cell as an exp-0 g-address), which only let / tuple bindings consumed; a call inside an expression (7 * f(x), a store's RHS, a single-target match arm) read its never-written dst cell and the stale bind mis-bound the NEXT let. Expression positions now consume the bind (take_inline_ret_cell), materializing aliased returns (free for a var; one MUL for a shifted pointer); Stmt::Let intercepts bare user-fn calls first, keeping the zero-copy alias hand-over of the obs / fs_next idiom byte-identical; multi-target match_range arms materialize into their join cells. Regression test: tests/inline_expr.rs (proves + verifies all three shapes). 2. A compile-time heap index that folds to a non-g-power field constant (buf[0], buf[2], an integer loop var leaking in from a StackBuf conversion) is now a compile-time error instead of a wild-pointer DEREF at proving time - heap cell k is addressed as buf[GEN ** k]. Exactly this bit during the dedup: converting bytecode_sel to a HeapBuf left one plain-int read in the defer_out fill, and the k=0 read lowered to address*0, failing 78k instructions later with zero compile-time signal. Regression test: tests/heap_index.rs. The guest's four eq-tensor weight loops then collapse into one @inline eq_weight(ch, count, idx, msb_span) helper used straight in expression position: row fold weights, query alpha weights, the bytecode selector reduction (bytecode_sel now a HeapBuf), and the lincheck const-pin term (msb_span = K_LOG selects its MSB-first bit walk). recursion_2to1 guest cycles 2,516,950 -> 2,516,990 (+40: the selector's three cells moved from frame to heap). Suite 243 + 3 ignored green, heavy recursion suites pass, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> wip protocol: every Ligerito scalar rides the stream, the opening keeps only hints LigeritoProof was the last pre-stream record struct: sumcheck messages, OOD values, the final message yr, the level roots and both PoW nonce families were transported in the struct and manually re-observed by the verifier. All of them now ride the shared transcript stream at their protocol points - add_scalar/next_scalar for the scalars (bound as written/read), the commit-root two-scalar convention for level roots, and grind/grind_check for the fold + query nonces (raw transport, bound by the grind itself; query grinds push a nonce even at 0 bits, as before). The opening object keeps only the hash-bearing hint data: opened rows + Merkle multi-proofs per level. initial_root leaves the proof entirely - the verifier uses the expected root it already has. Ripples: - SumcheckProver drops its internal transcript accumulation; tests collect the returned messages instead, and the roundtrip tests drive the verifier from the prover's bundle (no more detached/empty-stream verification). Tamper tests corrupt stream words at their layout positions, and lean_vm's validity tamper test corrupts an opened row. - The recursion harness stops extracting lig_sumcheck_msgs / final_msg / level_roots / fold+query nonces into hint pools, and its lincheck tail-offset slice now skips the opening's stream words (counted from the config shapes). - The guest's open_stacked takes the main stream cursor: msg_cursor IS the stream, level roots are two fs_next words (replacing the 3-absorb byte form), yr fills from the stream, and grind nonces are raw cursor reads bound by their DS_POW absorb. Six hint pools die. recursion_2to1 guest cycles 2,537,008 -> 2,516,950. Suite 241 + 3 ignored green (both heavy recursion suites pass), clippy clean, xmss CLI at 157.8 XMSS/s. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> flock: re-add the standalone batch BLAKE3 proving test The purge (2956d38) deleted tests/blake3_bench.rs along with the standalone flock prover API it exercised (prove_fast_timed, flare transcript, statement_digest). This brings the workload back on today's API: witness-gen -> commit -> Blake3Setup::prove_validity_stacked (zerocheck + lincheck reduction, one stacked Ligerito open) -> verify_validity_stacked, over FLOCK_N compressions (default 8192, Secure profile) with per-phase timings and a verify + finish gate - the fast loop for iterating on the flock reduction / PCS without the xmss harness. RAYON_NUM_THREADS=11 FLOCK_N=131072 cargo test --release -p flock \ --test blake3_batch -- --nocapture Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> lean_vm: the Ligerito proof moves out of RingSwitchVerify RingSwitchVerify becomes a plain claims bundle (no lifetime): the opening proof is not ring-switch data, it is the ONE stacked proof covering the slot claims too, so pcs::verify now takes it as its own parameter. The caller (cpu::verify) reads it off the openings hint channel at its protocol point and passes the borrow straight through - dropping the .clone() that copied the whole Merkle-bearing proof (next_opening returns &'a tied to the deserialized Proof, not to the VerifierState borrow), and the stale "BLAKE3 attachment" field doc with it. No protocol change. Suite 240 + 3 ignored green, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> recursion guest: baked prefix-mask table replaces the hinted overlap mask claim_overlap_mask's content is fully determined by the already-pinned claim_nover (the prefix of exactly nover ones), so instead of hinting + certifying it, the guest bakes ALL cap+1 possible prefix masks into one constant table (row t = [k < t]) and each claim selects row nover by pointer arithmetic (nover_g ** YR_LOG_CAP, a 3-MUL square-and-multiply). Mask reads stay one DEREF; the hint stream and the booleanity, monotone-prefix, and popcount pins all vanish (the prefix property holds by construction). The hi-span zero asserts stay and double as the nover <= yr_log_n pin: a larger nover selects a row whose prefix reaches into the asserted span. nover's range check tightens from SIZE_BITS to YR_LOG_CAP + 1, which also pins the row select to the table. (A first attempt wrote the mask with two runtime mul_range loops per claim; loop-call overhead cost +16.5k cycles, so it was dropped for the table select, which is straight-line.) The host stream and its tamper case in recursion_soundness_binds go away; the mask is no longer prover-chosen and the claim_nover tamper covers the overlap path. Parser: an integer log bound folds like any parse-time size, so `assert log x < YR_LOG_CAP + 1` works. recursion_2to1: 2534682 -> 2516928 cycles (-0.7%), bytecode 314764 -> 305887 instructions. recursion_2to1(+mixed) and recursion_soundness_binds pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> zkDSL: list literals — `x = [a, b]` is an initialized StackBuf New sugar for the alloc-then-store idiom: `x = [a, b, …]` allocates a StackBuf of the element count and writes each element in place, through the same stack-store path (copies/constants still defer as aliases), so the emitted code is identical to the manual form. Elements lower before the name rebinds, so `s = [s[1], s[0]]` swaps through the old binding. The recursion guest drops ~25 three-line StackBuf init blocks for it; bytecode is unchanged (314764 instructions, same committed witness). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> recursion guest: walk the flock message regions in order too The flock zerocheck multilinear-round messages (zc_msgs) and lincheck-round messages (lincheck_msgs) were the last "reserve region, offset-read later" sites: `zc_msgs = cursor` / `lincheck_msgs = cursor` plus a bulk skip. Walk them in stream order with fs_next instead. The unroll rounds walk the cursor directly; the flock multilinear mul_range threads it through a new flock_round_cursor heap chain, exactly like the GKR/AIR rounds thread gkr_round_cursor. The `cursor *= nmlv_g * nmlv_g` and `cursor *= GEN ** (2 * LINCHECK_ROUNDS)` skips are gone; the cursor now walks every stream word in order, and the only remaining cursor moves are the heap-chain seeds and the raw grinding nonce. Transcript unchanged: recursion_2to1 / _mixed verify with the committed witness identical (2^26.079). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> recursion guest: fs_next fetches, observes, and advances in one step Rename read_obs -> fs_next and have it return the advanced cursor too, so a stream walk is `fs, x, cursor = fs_next(fs, cursor)` with no manual `cursor *= GEN`. Every per-word read now walks: sequential regions thread a running cursor; fixed-base per-round loops (flock zerocheck/lincheck, the two aggregation sumchecks) thread within each read-pair, which also drops the `* GEN ** (2i+1)` offset multiplies. The three "reserve region, observe it as a block later" sites (zerocheck round-1, lincheck z_partial, ring-switch s_hat_v) now fetch-and-observe as they walk, into small HeapBufs. The only manual cursor moves left are genuine region-skips and the raw grinding nonce (absorbed later as DS_POW). Transcript unchanged: recursion_2to1 / _mixed prove and verify with the committed witness identical (2^26.079). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> compiler: inline multi-return can alias-return a g-address Generalize the inline tail-return binding so each returned value binds into the caller exactly as a `let name = <expr>` would: a `StackBuf` hands over its cell run, a folded g-address hands over its symbolic pointer, both aliased at zero copies; a scalar is copied into its dst cell. Previously only a StackBuf could be alias-returned (and only as the sole return value); a g-address among several returns would materialize into a cell, losing the free compile-time fold and the compile-time bounds check. Replaces the StackBuf-only `Option<Vec<Option<(Off,u32)>>>` record with a `RetBind` enum threaded through lower_return / Stmt::Let / Stmt::LetTuple. New stack_buf test `inline_returns_advanced_cursor` covers returning (StackBuf, scalar, advanced-cursor) together and reading through the cursor. This is what lets the recursion guest's stream walker return the advanced cursor for free: `fs, x, cursor = fs_next(fs, cursor)`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> transcript: drop the flock/pcs sub-protocol domain-separation labels The zerocheck, lincheck, pcs-open-batch, packed-direct, ring-switch, and ligerito-basis sub-protocols each absorbed a `b"flock-*-v0"` label into the Fiat-Shamir transcript. These were redundant: the transcript is a strict hash chain with a fixed, non-adaptive verifier structure, so a segment's position already identifies which sub-protocol it belongs to, and the top-level seed (the flock-family + program digest) separates this proof system from any other. Remove all six labels symmetrically from prover and verifier (crates/flock and crates/pcs) and from the recursion guest's replay, plus the now-dead guest label constants, harness placeholders, and word16 helper. flock (74), pcs (62), lean_vm (15), and rec_aggregation (recursion_2to1 + _mixed) all still prove and verify. The recursion guest shrinks 315445 -> 314920 instructions (1008 fewer BLAKE3 absorbs); a pass requires the native proof and the guest replay to agree, confirming the removal is consistent. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> refactor: give recursion DSL placeholders descriptive names Pure mechanical rename of cryptic placeholders in recursion.rs and the xmss_aggregate/recursion guest; no behavior change. - N_INNER_ROUNDS -> N_FIXED_CHALLENGE_ROUNDS, INNER7 -> FIXED_CHALLENGES, I7INV -> ONE_PLUS_CHALLENGE_INV - {ZC,LC,OB,RS,PD,LIG}LBL A/B -> {ZEROCHECK,LINCHECK,OPEN_BATCH, RING_SWITCH,PACKED_DIRECT,LIGERITO_BASIS}_LABEL_0/1 - GG dropped in favor of the builtin GEN; GINV -> INV_GEN - ILD0/1/2 -> LAGRANGE_INV_0/1/2; ILAM/ICMB/ISDOM -> LAGRANGE_INV_{LAMBDA,COMBINED,S} - PHI -> PHI8_NODES; DELTA -> TRACE_DUAL_BASIS; SEEDB0/1 -> TRANSCRIPT_SEED_0/1 - merge duplicate NCL/NCLAIMS into a single N_CLAIMS Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> fiat-shamir: fuse stream read + sponge absorb into one read_obs The recursion guest repeated `x = cursor[..]; fs = obs(fs, x); cursor *= GEN` at every proof-stream read, maintaining the "observe before it influences a challenge" invariant by hand at each site. Fuse read+observe into one `read_obs(state, cursor) -> (state, x)` so a stream word cannot enter the computation unbound. That needs an @inline to return the sponge state (a StackBuf) alongside the consumed scalar, which the lowering forbade: it aliased a returned StackBuf only when it was the SOLE return value, and a multi-value return routed every element through expr() (panicking on a StackBuf). Generalize `inline_stack_ret` from one `Option<(Off,u32)>` to per-slot `Option<Vec<Option<(Off,u32)>>>`, so each returned value is independently a StackBuf alias or a scalar cell; lower_return / Stmt::Let / Stmt::LetTuple bind each accordingly. `fs` stays a StackBuf and obs/squeeze/absorb are unchanged. Guest transcript is unchanged: the recursion guest compiles byte-identically (315445 instructions, same MUL/DEREF counts), and recursion_2to1 / recursion_2to1_mixed still prove and verify. New stack_buf test covers the inline StackBuf+scalar tuple return in isolation. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> naming feat: cache XMSS benchmark signers to disk Signer generation (keygen over slots 0..=15 + grinding sign) is the untimed setup cost of the aggregation benchmark and dwarfs proving for large batches. Generate each signer once, store the batch to disk under target/signers-cache/, and reload on later runs. The cache is a growing pool keyed on a footprint of the generation parameters (not on n), so bumping LEANVM_XMSS_N only generates the new tail and never re-does a smaller run's work. Also memoized in-process. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> benchmarks perf: fs_seed no longer rebuilds + rehashes the circuit family per process 82f4f74 made every transcript seed depend on the flock circuit-family digest, whose OnceLock init called build_block_r1cs(3) and hashed the matrices entry by entry: ~200 ms of symbolic matrix building (a second copy, next to the setup's own) plus ~250 ms of per-entry blake3::update calls over 21M nonzeros, landing inside the first prove. On XMSS x820 that cost ~6% on a 16-core x86 box and ~25% on an M4 Max (1.6 s prove). Three fixes: - flock::blake3::FAMILY_DIGEST: the digest is a constant of the circuit family, so bake it; family_digest_matches_baked recomputes and compares, failing on any circuit change until the constant is bumped. Same value as before, so fs_seed and the recursion guests are untouched. - build_block_r1cs clones the cached matrices() instead of re-running the symbolic builder: setups and const-pin lookups share one build per process (200 ms -> 72 ms per extra call). - absorb_matrix flattens to one buffer before hashing (244 ms -> ~10 ms), keeping the byte stream (and digest) identical. XMSS x820, 11 threads, x86: 5.55 s before 82f4f74, 5.87-5.94 s after, 5.46 s now. Suite 235 + 3 ignored green, recursion suites pass, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> polish: apply ~104 review findings across all crates Comment/naming/dead-code pass over the new workspace: - fix stale docs referencing purged code (BaseFold targets, jagged, default_config, verify_succinct, prove_batched, record structs) - re-attach doc blocks that had drifted onto the wrong item - rename ceil_log2 -> log2_ceil (naming convention), LigeritoLevelConfig k_levels -> k (scalar, not a collection), VerifyError::PcsAb -> Pcs - delete leftovers: empty impl blocks, unused locals, apply_triple (+test), dead rounds vectors in lincheck, fold_packed_witness_at_z - gate test-only items (#[cfg(test)]): stacked prove/verify wrappers, witness::stack, udr_queries; keep the general NTT entry points pub - fix stale crate paths in misc/doc.tex cargo test --workspace: 234 passed + 3 ignored; ignored recursion suites pass; clippy warning-clean across all targets. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> restructure: vendor/ dies, the repo becomes 8 clean workspace crates crates/ primitives GF(2^128)/GF(2^8) field kernels (+ phi8, g-power helpers), bit transposes, multilinear/eq/Lagrange helpers, the scratch pool, alloc/log2/perf utilities fiat_shamir the VM-native sponge + the ProverState/VerifierState transcript wrappers, now GENERIC over the opening type (the one upward reference the old layout had) pcs additive NTT, Merkle, commit, packing (+ PaddingSpec, moved from zerocheck), ring-switch, Ligerito, and the stacked open/verify facade as lib.rs; exports the concrete Proof/ProverState/VerifierState aliases flock r1cs, zerocheck (+ univariate skip), lincheck, ZClaim, VerifyError, and the BLAKE3 circuit + witness generation (the old flock-prover, as blake3.rs / blake3_witness.rs) lean_vm the VM: cpu (incl. the new cpu::hints with RHint/GPowMap — moved from the compiler, breaking the cpu<->compiler cycle), tables, constraints, witness, gkr, leaf, the stacked-PCS glue, blake3_flock, vmhash lean_compiler the zkDSL front end (ast/ir/lower/parser) + zkDSL.md, with the compiler feature tests + tests/programs/ rec_aggregation the two flagship harnesses as a LIBRARY (run_recursion, run_xmss_aggregation, run_fibonacci) + guests/*.py + the recursion/xmss/fibonacci suites as unit tests xmss unchanged, relocated Root: leanvm-b is now a clap CLI (xmss / recursion / fibonacci) over rec_aggregat…

The test hardcoded the inner proof's stacked log-size as m=22 and derived its residual-pad tamper coordinate from that: yr_pad_idx = yr_log_n(22) = 4. The committed stack for its config has since grown to m=23 (whose ladder has yr_log_n = 5), so coordinate 4 of rs_yslot_bits is a real y-slot index bit, not padding; the honest value there is 1 and the assert_ne tamper-setup check failed before any soundness assertion ran. Derive the stacked size from the batch instead of hardcoding it: build_batch now records each inner proof's layout m (stack_mus), exactly as gen_verify reconstructs it, and the test reads batch.stack_mus[0]. The dispatch-candidate bounds move into shared MU_MIN/MU_MAX consts used by both the placeholder map and the test's YR_LOG_CAP mirror, closing that drift channel too. The config moves to (8, 2^13) (m=24, yr_log_n = 3 < cap) so the residual-slot over-read tamper is exercised rather than skipped, and the silent skip branch becomes a hard assert: a future shape drift that parks yr_log_n at the cap fails the test loudly instead of quietly weakening it. Refresh recursion_generic_many's stale per-config m annotations (all shifted by one: m in {23..26}). All five tamper cases now run and are rejected; the honest proof verifies. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Merge branch 'main' into small-proof Brings in main's standard-BLAKE3-chaining protocol (b94b315, b788b1c) ported onto this branch's 192-bit three-lane words, plus the SIMD-batched Merkle hashing, hierarchical tracing and pretty-print reconciliation (both originated here; main's ports superseded where they diverged), and the signers-cache encoding-predicate fingerprint. The chaining port, adapted to canonical 128-bit chunks embedded in 192-bit cells: Op::Blake3 gains a chaining-value base offset (two consecutive cells, each read through the bus as (lo, hi, 0) so the canonical embedding is proof-enforced and the zero top limbs are never committed) and a 128-bit metadata immediate carried in the two low K-lanes of a 192-bit word whose lanes ride two public bytecode slots. The instruction encoding grows from six to nine public columns and the bus from nine to twelve coordinates; the stacked bytecode polynomial takes four selector bits. The BLAKE3 table adds the CV operand/address, two CV memory reads, and the sixth address binding; its eighteen value lanes are virtual, routed to the generalized flock witness (cv words 0..4, metadata words 18..20). The flock circuit takes cv/counter/blen/flags as free input rows with the re-baked family digest, and the branch's bilinear circuit walk is updated to match. vmhash::hash_slice, PCS Merkle leaves, xmss tweak hashes, and the program digest switch from the Merkle-Damgard length-in-IV construction to standard BLAKE3. Guest updates: the recursion guest packs each queried leaf row into a contiguous cell run (level 0 packs two hinted F64 lanes per cell via PACK64X2; deeper levels pack the three serialized F192 limbs per word likewise, preserving the limb K-membership proof) and hashes it as chunk-chained standard BLAKE3 through per-level LIG_LEAF_BLOCKS (level 0: n/8 blocks of 8-byte lanes; deeper: 3n/8 blocks of 24-byte words); the BLAKE3 zerocheck branch grows to six Horner-batched address bindings. The xmss guest uses cv-chained sub-hashes (146 compressions per signature, down from 158). The compiler keeps pack64x2/pack64x2_into/hint_f192_limbs alongside the new blake3 keyword surface and lazy per-scope IV cells (SET from IV_CELLS, registered in the const-cell cache). Kept from this branch where main's ports lagged: the log-inv-rate CLI and per-proof PCS rates, the F64 Ligerito implementation (main's tracing landed in deleted code), the prepared-reduction-witness plumbing, and the per-64-bit-word WOTS encoding. Full workspace suite passes, including both recursion 2-to-1 tests (mixed rates included), xmss aggregation, and main's chaining regressions adapted to three-lane words. The ignored recursion_soundness_binds test fails identically on the pre-merge HEAD (a pre-existing breakage on this branch, not a merge regression). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Merge branch 'main' into small-proof # Conflicts: # crates/flock/src/blake3.rs # crates/flock/tests/blake3_batch.rs # crates/lean_vm/src/blake3_flock.rs # crates/lean_vm/src/cpu/layout.rs # crates/lean_vm/src/cpu/mod.rs flock: reuse prepared reduction witness Retain the fused A·z, B·z, and lincheck layouts created with q_pkd and consume them after commitment instead of regenerating the witness. Add env-gated reduction phase timing and exercise the prepared path in the batch harness. Support StackBuf returns from normal functions Use Horner evaluation for challenge polynomials Replace explicit challenge-power expansions across VM AIR constraints, recursive zkDSL verification, and quadratic sumchecks with Horner evaluation. Add shared native and zkDSL helpers for efficient F192 limb reconstruction, mirror every AIR formula on both sides, and update compiler documentation and examples. Include the repository-wide cargo fmt pass. Simplify recursion hashing to canonical BLAKE3 cells Remove the Transcript192 BLAKE3 mode and its alternate opcode, leaving one canonical 128+128-bit encoding throughout the VM. Shrink the BLAKE3 AIR table from 51 to 31 columns and reduce its local constraints to the five address bindings while the memory bus and Flock validity proof bind the canonical lanes. Add computed F192 limb advice and destination-target PACK64X2 support, including nested inline zkDSL helpers for transcript absorption, challenge reconstruction, and constrained conversion between canonical Merkle cells and Ligerito transcript words. Update recursion witness generation, documentation, and regression coverage accordingly. Add PACK64X2 base-field packing instruction Introduce a VM instruction that reads two F_2^64 memory words and packs them canonically as one F_2^192 word with limbs (lo, hi, 0). Enforce source subfield membership and destination packing through literal-zero memory-bus coordinates, so the invariant is proof-enforced rather than only checked during witness generation. Wire the opcode through execution, traces, AIR, bytecode, layouts, transcript binding, table counts, statistics, and recursive-verifier shape handling. Preserve the existing BLAKE3 Transcript192 mode; no mixed packing mode is needed. Expose pack64x2(a, b) in zkDSL and use it in recursion.py to constrain every serialized Merkle-leaf limb before reassembly, hashing, and row-dot evaluation. Add end-to-end proving and invalid-extension-source tests, Python stubs, and VM/zkDSL documentation. Document MCA error in unique-decoding regime Pretty-print displayed integers with commas pcs: make F64 Ligerito the sole implementation Remove the Ligerito/Ligerito-K split and promote the F2^64-committed implementation to the canonical pcs::ligerito API. - move the shared security/configuration machinery into a private ligerito_config module and re-export it through pcs::ligerito - rename pack_k, ring_switch_k, stack_open_k, and tensor_algebra_k to their canonical module names - drop K suffixes from commitments, proofs, configs, ring-switch types, stack-opening types, helpers, and transcript aliases - migrate lean_vm, flock, recursive aggregation, throughput tests, guest comments, and protocol documentation to the canonical API - keep dense verifier and ring-switch reference paths only for tests, excluding unused helpers from production builds - remove stale compatibility terminology and the superseded extension-field implementation - preserve the existing NEON and AVX/AVX-512 optimized kernels unchanged Verified with: - cargo check --workspace --all-targets - cargo test --workspace --release - PCS_LOG_N=16 PCS_LOG_INV_RATE=1 PCS_SAMPLES=1 cargo test --release -p pcs --test pcs_throughput -- --ignored --nocapture - RAYON_NUM_THREADS=11 cargo run --release -- recursion --n 2 --log-inv-rate 1 - RAYON_NUM_THREADS=11 cargo run --release -- xmss --n-signatures 820 --log-inv-rate 1 - git diff --check pcs: vectorize F192 NTT with AVX-512 improve hierarchical PCS tracing primitives: add AVX-512VBMI bit transpose enable tracing remove 128 bits fields make tests pass add pcs_throughput benchmark pcs/ligerito_k: pool the initial-sumcheck fold buffers (x86_64) The initial sumcheck is the dominant phase of the K-PCS open (~57% at log_n=24), and it allocs+faults two fresh ~100 MB F192 buffers (nf, nb) every fold round, then frees them — the allocator munmaps on drop, so every prove re-pays soft page faults on first touch. Route the fold outputs through the existing F192 scratch pool (primitives::scratch) via a new fold_out_buf helper, and give the consumed input buffers back in SumcheckProverK::fold, so repeated proves reuse resident pages instead of faulting fresh mappings. x86_64-gated to match flock (pooling here measured slower on aarch64, which keeps the fresh-alloc path). Correctness: F192 has no Drop and every fold slot is written before read, so recycled (stale) buffers are sound; all 55 pcs tests pass incl. the log_n 12/16/18 roundtrips. Measured (log_n=24, LIG_K_TRACE, steady state): initial sumcheck ~0.175 s -> ~0.063 s (~2.8x) total open ~0.31 s -> ~0.18 s (~1.7x) Ports the buffer-pooling idea from flock (github.com/succinctlabs/flock), commit "perf: add x86 AVX-512 prover acceleration" (the scratch-pool reuse for the initial-sumcheck fold). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Align Ligerito RBR soundness doc and implementation Fix pcs.tex thm:mca-johnson against the primary source (BCHKS25 Thm 4.6, list correlated agreement): the theorem parameter is max(ceil(sqrt(rho)/eta), 3), not the ceil(sqrt(rho)/(2 eta)) of the non-list Thm 1.5 that Flock's Thm 8 quotes, and rho is the slightly reduced rate (k-1)/n. The implementation (johnson_m_param, reduced_rate) already had both right. In ligerito.rs, name misc/pcs.tex as the soundness source of truth and map thm:rbr's per-verifier-message error table onto the validate() checks (max semantics, per-transition 128 bits); replace dangling references to a former appendix. Remove the dead UDR regime (never constructed in production), making eta and expected_eps_ood_bits plain f64. Fix the OOD diagnostic doc (192, not 128) and the INITIAL_FOLDING_FATOR typo. Update doc.tex's PCS paragraph: per-level optimized eta (not 0.02) and 17-bit query grinding (queries close the remaining 111 bits). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Merge branch 'main' into small-proof pcs.tex (a note on WHIR/Ligerito over binary fields, interpreted as List binding PCS Use query grinding to reduce proof size Optimize Johnson eta per recursive level Use aggressive recursive RS rate schedule Audit and tighten Ligerito soundness parameters Correct the BCHKS25 Johnson proximity-gap parameter to use ceil(sqrt(rho) / eta), and evaluate the theorem at the reduced RS rate (K - 1) / n instead of the nominal encoding rate. Move the global Johnson slack from 0.02 to 1/160, retaining more than 128.8 bits of proximity-gap soundness without grinding while reducing query counts and proof size. Validate exact, unrounded query, proximity, OOD, list-unioned algebraic, and degree-191 ring-switch errors. Clarify the round-by-round security claim and add production-profile regression tests for all supported rates and witness sizes. Make Ligerito rate proof-local and recursion-generic Pass log_inv_rate explicitly through proving instead of process-global state, announce and validate it through Fiat-Shamir alongside layout sizes, and derive commitment/opening parameters from the transcript-bound value. Embed all supported rate/size configurations in the recursion guest so one program can verify mixed-rate inner proofs, while letting the CLI-selected rate independently configure both inner and outer proofs. Add CLI validation, the environment-driven query-count report, mixed-rate regression coverage, and update the README. Move Ligerito to 128-bit Johnson list decoding Raise the global round-by-round soundness target to 128 bits and derive the production Ligerito ladder in the Johnson list-decoding regime over GF192 with eta 0.02. Use the post-commit L0 opening claim as its implicit binding evaluation, and add one explicit OOD evaluation for each recursive commitment. Port those OOD claims through the GF64-committed prover, dense and succinct native verifiers, proof encoding, recursion hint builder, and in-VM recursion verifier. The GF192 margin makes the query, proximity-gap, and OOD-binding terms each clear 128 bits without query or fold grinding. Add parameter assertions and OOD tamper coverage, and update the security documentation. Validated with all PCS, Flock, LeanVM, and recursion release tests, recursion --n 2, and xmss --n-signatures 820. The recursion proof drops from 579.1 KiB to 518.3 KiB and guest cycles from 2,842,984 to 2,591,048. Optimize GF192 ring switching in recursion Factor the GF192 trace-dual basis over its GF64 degree-three tower, replacing the dense 192-by-192 Frobenius table with smaller base and tower tables. Assert the factorization while constructing guest placeholders. Evaluate the two transposed claims and their transparent ring-switch weights in lockstep so they share coefficients, powers, and verifier-weight loads. This reduces the recursion --n 2 guest from 3,235,330 to 2,842,984 cycles (12.1%), the proof from 610.7 to 579.1 KiB, and measured proving time from 13.50s to 9.22s. Merge field-exploration into small-proof Bring over native BLAKE3 circuit-walk verification, compiled recursion-guest caching, and clarified division-by-zero semantics. Adapt the verifier paths and cache key to GF192. Deliberately omit the bus-grinding changes from 97d9c687cd01fbec9987172f56abd810fa2299d7. doc recursion: cache the compiled guest across verifies RecursiveProof::verify recompiled the recursion guest on every call (~235 ms), dwarfing the ~20 ms of actual proof checking. The guest is a pure function of the inner bytecode and the batch size, so recursion_guest_arc caches compiled guests process-wide, keyed by (fs_seed(inner_program), nsub) and capped at 8 shapes, compiling outside the lock (mirrors blake3_flock::setup_for). verify borrows the pristine cached Arc; prover paths clone an owned copy for their witness streams (cpu::Program now derives Clone). Complete recursive verify: 268 ms -> 18.7 ms once a shape is warm, now dominated by the Ligerito opening. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Native verifier evaluates A0/B0 by circuit walking The native verification of a recursive proof paid the ~21M substituted nonzeros of the BLAKE3 matrices twice: check_reduced contracted two eq tables through them to discharge the deferred v_a/v_b claims (~11 ms, forcing the ~300 ms matrices build), and lincheck::verify materialized the alpha-batched column marginal via the CSC fold (~1.2 ms + one-time 22 ms transpose). bilinear_walk_pair (flock.pdf, Circuit walking) computes u^T A0 w and u^T B0 w in O(circuit) field ops (~43 us) by walking the unsubstituted compression cascade over F128T wire values, mirroring build_matrices row for row; a randomized cross-check test ties it to the materialized matrices. check_reduced now walks. lincheck::verify no longer folds comb_vec through the rounds: the final consistency check collapses to one bilinear form against the rank-1 column weight w_col[c] = z_partial[c_skip]*eq(r_inner_rest, c_rest), answered by the new LincheckCircuit::bilinear_form (WalkLincheckCircuit; default None falls back to the marginal + inner product). Transcript unchanged. Proof checking drops ~31 ms -> ~20 ms per recursive verify. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Document the GF192 machine field Update the VM and proving-system specification from the old quadratic GF128 representation to the implemented cubic tower E = GF64[y]/(y^3 + y + 1). Describe three-limb memory words, arithmetic, immediates, memory interactions, instruction tables, and public-input openings. Clarify that BLAKE3 uses canonical 128-bit values embedded in full GF192 cells with a zero top limb, and record that the larger challenge field eliminates grand-product grinding under the instance caps. Also distinguish the zkDSL's 128-bit literal syntax from its 192-bit machine-word type. Use univariate batching for GF192 ring switching Replace the padded eight-challenge coordinate cube with powers of one GF192 Fiat-Shamir challenge. Share that challenge across stacked ring-switch claims and retain the existing GF64 transpose and GF192 transparent-weight evaluation paths. In the recursion guest, compute the trace-dual linearized coefficients directly with Horner evaluation. This removes the equality tree and coordinate-weight buffer, reducing the recursive verifier by 1,510 instructions and 76,746 VM steps relative to the padded baseline while retaining better than 184 bits of batching soundness. feat: migrate recursion and PCS to F192 Move the protocol challenge and machine-word field to the cubic F192 tower while retaining F64 physical columns and canonical 128-bit BLAKE3 cells. - add portable, x86, and AArch64 F192 arithmetic with deferred-reduction kernels - carry all three limbs through the compiler, ISA, trace tables, Flock reductions, transcript, GKR, and public-input binding - generalize K-packed Ligerito, ring switching, tensor algebra, query sampling, and Merkle serialization to 192-bit challenges and folded words - update the recursion guest AIR, claim descriptors, memory binding, packed queries, and Merkle verification, including the rho-point fix for virtual BLAKE claims - remove grand-product bus grinding under the F192 soundness budget and account for the actual 2^192 Ligerito challenge field - refresh DSL documentation and tests, and keep the large BLAKE3 batch benchmark as an explicit release-only benchmark Clarify division by zero semantics Fix bus grinding soundness bound pcs: batch F64 NTT butterflies with NEON docs: align field architecture documentation pcs: batch F64 NTT butterflies with VPCLMUL pcs: optimize tower-field stacked openings Merge branch 'main' into field-exploration pcs: avoid redundant basis initialization work cpu: transmit the PI low lane so the guest skips Frobenius extraction The public-input binding needs both K-lanes of MEM(r) = interp(pi, r) as opening claims. The lane values are deterministic from the seeded pi, but a recursive verifier can't cheaply slice F64 lanes out of the E-valued pi — the old guest recovered them with two 64-squaring Frobenius loops. Instead, transmit the low lane v_lo = MEM_LO(r) (one scalar) and deduce the high lane v_hi = (MEM(r) + v_lo)*Y^-1 from the pi-derived E-value. The guest replays it as one scalar read + one multiply — no Frobenius, no X_INV. This nets a simplification: bind_pi_claim is a single helper returning [ColumnClaim; 2] (reusing multilinear::interp), the transcript add_scalar/ next_scalar is inline at each call site, and the now-dead X_INV constant + its Frobenius baking are deleted (guest and harness). Transcript and claim order are unchanged from the two-lane binding, so it stays sound. Validated in release: cpu 8/8; recursion_2to1, _mixed, _soundness_binds (tamper-rejection), _generic_many all pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv flock: restore standalone BLAKE3 batch benchmark Merge branch 'tower-only-flock' into field-exploration field: remove GHASH and use tower field throughout unify Ligerito protocol configuration sponge: carry the domain-separation tag in lane 2 (main convention) The v2 sponge bound the DS tag in the 4th compress lane, which forced the recursion guest to encode its tags as `k << 64` (the tag in the F128T high lane). Move the tag to the 3rd lane (right after the up-to-two data words) so the guest's tags are plain `1,2,3,4,5` again, matching main's convention. The tag lane is a pure convention (all five values stay distinct and nonzero, so domain separation is unchanged); byte-absorb blocks now carry two data words (16-byte chunks) instead of three, since the tag takes the third lane. Validated end-to-end in release: cpu 8, pcs 103, flock 77, recursion_2to1 + mixed, and recursion_soundness_binds (tamper-rejection) all pass — prover, verifier, and the in-VM guest replay agree on the new transcript. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv recursion: remove the `recursion` feature gate (harness is ported) The gate + `unimplemented!` stub existed only because the recursion harness was unported to the 64-bit machine; now that it works end-to-end, drop the feature so the `recursion` module and the real `run_recursion` are always compiled. `cargo run --release -- recursion --n 2` runs the aggregation with no extra flags (verified: 2 inner proofs aggregate and the recursive proof verifies). Also removes the now-dead `uk` base-field encoder. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv recursion: port the N->1 aggregation to the 64-bit tower protocol Make the in-VM recursion guest verify N->1 recursive proofs on the 64-bit (K=F64, extension F128T) protocol. Each fix addressed a constant or convention that coincided under the old GHASH / 128-bit packing (LOG_PACKING=7) but diverges in the tower with 64-bit packing (LOG_PACKING_K=6): - tower ring-switch trace-dual basis, derived by the same construction over the tower's coordinate basis and verified against the duality property - Fiat-Shamir domain-separation tag in compress lane 3 (the tower sponge) - bit-decomposition reconstruction in the real F128T coordinate basis; the field generator's powers span only F64, so g^i is not the coordinate basis - two-lane 128-bit memory public-input claims (MEM_LO/MEM_HI) via Frobenius lane extraction of the bound public-input words - AIR constraint formulas re-ported for the LO/HI memory split - K-opener transcript realigned to its F128 reference that the guest replays: ordered d-bit-chunk query sampler + surfaced query squeezes, scalar Merkle root binding, 64-wide s_hat_v, struct-based Ligerito observed-scalar replay, and the SLOT_STRIDE_LOG = K_LOG - LOG_PACKING_K terminal identity Validated: recursion_2to1 and recursion_2to1_mixed verify honest recursive proofs; recursion_soundness_binds rejects every tampered hint (the in-VM verifier genuinely binds); pcs 103, cpu 8. No check was weakened or stubbed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv flock: migrate the verifier to the binius tower (F128T) Move flock's verifier (zerocheck + lincheck + the blake3 reduction) to the binius tower field F128T, so a downstream in-VM verifier replays a single field instead of the two-field GHASH/tower bridge. The fast GHASH prover is unchanged (the shift_reduce univariate-skip optimization stays). It now bridges its transcript messages and claims through the real ghash<->tower isomorphism instead of the bit-copy reinterpretation, so its outputs are genuine tower values the F128T verifier checks. The blake3_flock boundary is native tower (no isomorphism on point/value/weights); only the prover-only s_hat_v capture still crosses. Adds the tower phi8 embedding (iso-image of the GHASH basis, exhaustive homomorphism test, images land in F64) and a tower lagrange-weight helper. Validated: 77 flock tests and 8 cpu prove/verify + tamper-rejection tests pass; workspace builds clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXRdyJAixoTtQ2Uh8WtHBv lean_vm: drop the DEREF pointer's always-zero HI lane (K-valued address) The DEREF pointer is constrained to K by `a2 = p·obe` (a2 is a single-lane K address), so its high lane is provably 0. Commit it as a single K lane (deref::P) instead of P_LO/P_HI, with the memory read carrying a literal 0 high lane via the new FlushBuilder::memory_k. The bus balances only if the stored value's HI lane is also 0, which the K constraint guarantees — sound; a debug_assert pins p.c1 == 0 at fill time. Removes one committed column of zeros from the most frequent instruction's table (DEREF, 571/XMSS): committed witness 2^26.180 -> 2^26.170 (~0.7%). Branch-specific (only the 128-bit-memory-word design gives an address a HI lane); no main equivalent. All prove/verify tests pass. Not applied to the JUMP d/f destination words: they are only forced into K on taken branches (b=1); a not-taken branch reads an unconstrained memory word, so forcing HI=0 would reject valid traces. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Merge commit 'b956c4d' into field-exploration # Conflicts: # crates/flock/src/zerocheck.rs Merge commit 'b7e1be2' into field-exploration # Conflicts: # crates/flock/tests/blake3_batch.rs # crates/lean_vm/src/pcs.rs # crates/pcs/src/ligerito.rs Merge commit '9e957fc' into field-exploration # Conflicts: # crates/fiat_shamir/src/sponge.rs # crates/pcs/src/merkle.rs Merge commit '2905de0' into field-exploration # Conflicts: # crates/lean_vm/src/leaf.rs Merge commit '7b74709' into field-exploration # Conflicts: # crates/primitives/src/multilinear.rs Merge commit '086f622' into field-exploration # Conflicts: # crates/lean_vm/src/pcs.rs Merge commit 'b336897' into field-exploration # Conflicts: # crates/lean_vm/src/cpu/layout.rs Merge commit '11e799f' into field-exploration # Conflicts: # crates/lean_compiler/src/lower.rs Merge commit 'a825bf6' into field-exploration # Conflicts: # crates/flock/src/zerocheck.rs # crates/lean_vm/src/tables.rs Merge commit 'bd8b31b' into field-exploration Merge commit '53077e5' into field-exploration field: switch the VM's extension field E to the binius64 tower Make the binius64 tower K[y]/(y^2 + x*y + 1) the shipped degree-2 extension field E, replacing the Artin-Schreier tower K[y]/(y^2 + y + x^61). Same base field K = F64 and identical repr(C){c0,c1} layout, so the ~1,200 call sites are untouched: F128T now names the binius tower (tower_f128.rs, formerly the tower_f128_xy investigation variant), and the old Artin-Schreier tower is kept as F128TArtin (tower_f128_artin.rs) for the field benchmarks only. - Build binius up to full field parity before the swap: From<F64>, AddAssign, the mixed K x E path (mul_base / mul_base_unreduced / a BaseUnreduced accumulator, all tower-independent), Serialize/Deserialize/Hash, the Y const. - Re-derive the GHASH <-> tower isomorphism (iso_f128.rs) for y^2 = x*y + 1. The K-embedding is tower-independent (X unchanged), so only the Y columns move; the j=0 block is byte-identical to the old matrices. gen_iso_xy.rs regenerates and verifies them (100k random multiplicativity + round-trips), replacing the lost scratchpad/iso.py. Correctness verified on aarch64: the whole workspace builds and every test passes -- pcs prover/verifier round-trips, lean_vm (VM, GKR, constraints, the leaf mixed K x E path), and blake3_flock (which maps claims through the re-derived iso at the flock boundary), plus all integration tests. This is the correctness migration only; the batched fold-kernel speedup that motivated it lands separately. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> remove superseded zerocheck kernel field benches: wire the VPCLMULQDQ batched inner product field_bench: new 'inner prod, VPCLMUL' row (x86 vpclmulqdq+avx512f only) running the batched Karatsuba kernel (B=2) for F128T and F128Txy — ~5.5-6.9x the scalar 'deferred' row (0.37 vs 2.3-2.6 ns/term), and it collapses the tower gap from C/B 1.12x (scalar) to 1.00x: wide CLMUL erases binius's deferred-inner-product deficit without flipping it. Banner now reports the VPCLMULQDQ backend. inner_bench: the noise-robust comparator is now generic over the field, with an x86_64 backend ranking scalar-deferred vs vpclmul kara/school at bank counts 1/2/4 for both towers, plus a best-of-each head-to-head. Findings on Zen4: Karatsuba beats schoolbook (0.367 vs 0.393 ns/term) — the reverse of M-series, where PMULL is cheap enough that schoolbook's extra product buys dropping the pre-XOR; on x86 CLMUL throughput is the bound, so the extra CLMUL loses. B=2 wins the bank sweep. Confirms the schoolbook win was Apple-specific. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> field: AVX-512 VPCLMULQDQ batched inner-product kernels for both towers Adds field/vpclmul.rs, a shared AVX-512 batched Karatsuba accumulator: one VPCLMULQDQ does four independent 64x64->128 carry-less products (one per zmm lane), folding four field elements per CLMUL. Two variants — karatsuba_acc (3 CLMUL + shuffle/XOR pre-mix) and schoolbook_acc (4 CLMUL, no pre-mix) — both return the same (Sum p0, Sum p1, Sum pm) triple with a const-generic bank count for ILP. Both degree-2 towers gain inner_unreduced_vpclmul_{kara,school}<B> in their x86_64 modules. F128T and F128Txy are repr(C){c0,c1} with identical layout, so the accumulate is shared; each kernel only supplies its field-specific reduce, reusing the already-tested Unreduced::reduce(). Only the batched accumulate is new arithmetic. Tests check the batched kernels against the scalar deferred reference across 18 lengths (including partial vector groups and the <4 scalar tail), both kernels, bank counts 1/2/4, on both fields. Gated on target_feature vpclmulqdq + avx512f (Zen4 / Sapphire-Rapids-class); -C target-cpu=native enables both. The CLMUL stays 128-bit per lane — this batches four, it does not widen the field multiply. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> field: schoolbook batched inner-product NEON kernel + noise-robust comparator inner_unreduced_neon (the deferred sum_i a_i*b_i hot-loop kernel) was Karatsuba, 3 PMULL/term. On M4 Max PMULL is not the bottleneck, so dropping the per-term am/bm Karatsuba pre-XOR (2 DUP + 2 EOR) in favour of one extra PMULL wins: schoolbook products run ~1.25x faster. inner_unreduced_neon now dispatches to inner_unreduced_school::<2>; inner_unreduced_kara is retained as the comparison alternate. field_bench's "inner prod, NEON kernel" row: the tower kernel drops 0.58 -> 0.47 ns/op. The win was isolated with a noise-robust comparator (bin/inner_bench): it interleaves every method round-robin (rotating order) and ranks by the MINIMUM time across many rounds -- noise only ever adds time, so the min is the cleanest estimate of true speed -- with a per-round win-count as corroboration. That methodology overturned two single-pass "wins" as pure measurement noise: accumulator banking (x1 == x2 == x4) and slice bounds-check removal both do nothing here. Only the schoolbook-vs-Karatsuba product choice moves the number. Also make the field_bench CLMUL-backend banner architecture-aware so it no longer prints "numbers not meaningful" on x86 (which has a real pclmulqdq path), and notes that path is 128-bit CLMUL, not VPCLMULQDQ. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> field: aarch64 NEON path for the binius64 tower (F128Txy) 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> centralize Merkle root encoding centralize F128 byte encoding field: add binius64 degree-2 tower and bench it vs the Artin-Schreier 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> simplify bus claim decomposition share multilinear field helpers naming derive column sizes from layout sources wip field: add x86_64 pclmulqdq path for GF(2^64) and the F128T tower 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> reuse compiler constant pool simplify challenge and table construction deduplicate deterministic test rngs generate phi8 table from basis images Merge branch 'main' into field-exploration 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> signers cache: fold hash-construction fingerprint into the footprint The signer cache filename hashed only the declared XMSS parameters (slot, key range, message, V/W/CHAIN_LENGTH/...). Those are identical across branches that change the hash *construction* underneath — e.g. the Merkle-Damgard IV switching field width (GF(2^128) <-> GF(2^64)) rewrites every digest while touching no constant. Both branches then computed the same filename and the serialized sizes match, so a run on one branch loaded the other's cryptographically-invalid signers and panicked in verification. (cargo clean masked it by wiping the poisoned file.) Fold a known-answer test vector of the real primitives (one tweak_hash, one md_tweak_hash) into footprint(), so any change to digest behavior lands in a distinct cache file. Per-branch caches now coexist instead of clobbering one another. Two BLAKE3 compressions; negligible next to generating a signer. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> unify equality table construction make recursive proof verification atomic vm: 128-bit memory words (E) with 64-bit addressing (K) 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> Merge branch 'main' into field-exploration 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> recursion guest: runtime-sized buffers replace the linear capacity caps HeapBuf sizes carried in the exponent (HeapBufDyn: the alloc hint does an O(1) reverse g-power lookup at witness generation, erroring past 2^20 cells) already existed - the guest now uses them wherever the exact size is a certified runtime g-power at declaration time: - zerocheck_r / flock_point chains: exactly m = K_LOG + tau_5 slots (mr1cs_g); zerocheck_rhos / flock_round chains: exactly m - 6 (mr1cs_g * INV_GEN^6). R1CS_M_CAP and R1CS_ROUNDS_CAP die. - zeta and the nine GKR per-layer chains: exactly mu (+2) slots (g_bus_mu), zeta's declaration moving below the certified bus depth. What stays capacity-sized, and why: STREAM_CAP / YR_SLOT_STRIDE size hint pools (witness-hint lengths are compile-time); QPKD_VARS_CAP and MU_CAP are row STRIDES of two-row / triangle layouts (a runtime stride would unfold every access); GKR_ROUNDS_CAP / GKR_POINTS_CAP are quadratic in mu (a runtime g-power for them needs exponent-domain multiplication, all cost, no cycles saved). recursion_2to1 cycles 2,516,990 -> 2,517,066 (+76: one MUL per materialized runtime size) against exact allocations. Suite 244 + 3 ignored green, heavy recursion suites pass, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Merge pull request #2 from leanEthereum/recursion Recursion ligerito: the fold constants are one knob each - INITIAL_K=5 works Changing INITIAL_K / LEVEL_K / RESIDUAL_MAX_LOG in crates/pcs now propagates everywhere: - lean_vm's LOG_BATCH and LOG_INV_RATE stop re-declaring their own 6 / 1 behind compile-time asserts: they ARE ::pcs::ligerito::INITIAL_K / LOG_INV_RATE_0 (the Merkle leaf width and the L0 fold count are one knob by construction - the L0 commit is reused). The blake3_batch test reads the constants too. - recursion_soundness_binds stops hardcoding the residual shape: the rs_yslot_bits tamper index (the first PADDING slot coordinate, k = yr_log_n) is derived from the fold ladder, and the tamper is skipped when this candidate's yr_log_n equals YR_LOG_CAP (the guest reads only YR_LOG_CAP coords, so no pad coordinate exists and the over-read path it guards is absent - exactly what happens at INITIAL_K=5). Verified by actually flipping the knobs: the FULL workspace suite, both heavy recursion suites, and the xmss CLI all pass at INITIAL_K=5 (the guest re-derives its baked tables from the config, so recursion just works); pcs + rec_aggregation pass at LEVEL_K=4. Shipped values are unchanged (6 / 3 / 5), so derived configs, proofs and cycles are byte-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> ligerito: LigeritoProfile dies; the shipped shape becomes named constants Only one configuration ever ships (the old Secure profile), so the selector enum and its Fast/Slim derivation arms go. What was implicit now has a name in crates/pcs/src/ligerito.rs: - SECURITY_BITS = 120 round-by-round soundness target - LOG_INV_RATE_0 = 1 L0 code rate 2^-1 - QUERY_GRINDING_BITS = 18 query-phase PoW (queries cover 120 - 18) - INITIAL_K = 6 the INITIAL folding factor (L0 folds 2^6 interleaved rows; = PcsParams::log_batch_size) - LEVEL_K = 3 the folding factor of every subsequent level - RESIDUAL_MAX_LOG = 5 folding stops at <= 5 remaining variables: the residual yr (<= 32 coeffs) is sent in clear derive_profile(m, profile) -> derive_config(m); PcsParams loses its profile field; lean_vm pins its LOG_BATCH / LOG_INV_RATE / SECURITY_BITS to the pcs constants with compile-time asserts. The SoundnessRegime enum and the Johnson/OOD analysis + prover/verifier machinery stay for hand-built configs (the OOD roundtrip test constructs them directly); only the profile-driven derivation of them is gone. Derived configs are value-identical to the old Secure profile, so proofs and the recursion guest are untouched (cycles unchanged). Suite 244 + 3 ignored green, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> recursion verifier: derive positions-per-word from depth The Ligerito query decoder took per_word as a separate Const, but it is just FIELD_BITS / depth. Derive it inside decode_query_bits and drop the LIG_POSITIONS_PER_WORD placeholder (guest table + Rust export + caller arg); the write-offset now uses FIELD_BITS // LIG_TREE_DEPTH directly. Pure refactor: identical 128/depth packing, identical emitted code, no cycle change. Removes a redundant parameter and a placeholder threaded through the guest; the decode specialization collapses from __L{depth}_L{per_word} to __L{depth}. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> zkDSL: print(...) - a prover-side debug print `print(expr)` / `print("label", expr)` displays a value at witness generation: the expression evaluates into a cell and a Print hint hangs on a one-instruction no-op anchor, so it fires exactly at that program point, only on the executed path, and adds no constraints (nothing enters the transcript; proving/verification are untouched). The label defaults to the argument's source text. Output goes to stderr as `[print] label = ...` with the friendliest reading: decimal for small integers, g^k for small g-powers, both when they overlap (8 = x^3 shows as `8 (g^3)`), hi:lo hex otherwise, `<unwritten>` for a cell nobody wrote. Allowed inside @inline bodies and loop bodies (free vars flow through). Documented in zkDSL.md; test: tests/print_debug.rs. Suite 244 + 3 ignored green, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> compiler: @inline calls in expression position; eq_weight dedup covers all 4 sites Two compiler-level changes, found while deduplicating the recursion guest's eq-tensor weight loops: 1. @inline calls now work embedded in expressions. An inlined tail return of ANY plain var recorded a RetBind::Gaddr alias (gaddr_of treats every runtime cell as an exp-0 g-address), which only let / tuple bindings consumed; a call inside an expression (7 * f(x), a store's RHS, a single-target match arm) read its never-written dst cell and the stale bind mis-bound the NEXT let. Expression positions now consume the bind (take_inline_ret_cell), materializing aliased returns (free for a var; one MUL for a shifted pointer); Stmt::Let intercepts bare user-fn calls first, keeping the zero-copy alias hand-over of the obs / fs_next idiom byte-identical; multi-target match_range arms materialize into their join cells. Regression test: tests/inline_expr.rs (proves + verifies all three shapes). 2. A compile-time heap index that folds to a non-g-power field constant (buf[0], buf[2], an integer loop var leaking in from a StackBuf conversion) is now a compile-time error instead of a wild-pointer DEREF at proving time - heap cell k is addressed as buf[GEN ** k]. Exactly this bit during the dedup: converting bytecode_sel to a HeapBuf left one plain-int read in the defer_out fill, and the k=0 read lowered to address*0, failing 78k instructions later with zero compile-time signal. Regression test: tests/heap_index.rs. The guest's four eq-tensor weight loops then collapse into one @inline eq_weight(ch, count, idx, msb_span) helper used straight in expression position: row fold weights, query alpha weights, the bytecode selector reduction (bytecode_sel now a HeapBuf), and the lincheck const-pin term (msb_span = K_LOG selects its MSB-first bit walk). recursion_2to1 guest cycles 2,516,950 -> 2,516,990 (+40: the selector's three cells moved from frame to heap). Suite 243 + 3 ignored green, heavy recursion suites pass, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> wip protocol: every Ligerito scalar rides the stream, the opening keeps only hints LigeritoProof was the last pre-stream record struct: sumcheck messages, OOD values, the final message yr, the level roots and both PoW nonce families were transported in the struct and manually re-observed by the verifier. All of them now ride the shared transcript stream at their protocol points - add_scalar/next_scalar for the scalars (bound as written/read), the commit-root two-scalar convention for level roots, and grind/grind_check for the fold + query nonces (raw transport, bound by the grind itself; query grinds push a nonce even at 0 bits, as before). The opening object keeps only the hash-bearing hint data: opened rows + Merkle multi-proofs per level. initial_root leaves the proof entirely - the verifier uses the expected root it already has. Ripples: - SumcheckProver drops its internal transcript accumulation; tests collect the returned messages instead, and the roundtrip tests drive the verifier from the prover's bundle (no more detached/empty-stream verification). Tamper tests corrupt stream words at their layout positions, and lean_vm's validity tamper test corrupts an opened row. - The recursion harness stops extracting lig_sumcheck_msgs / final_msg / level_roots / fold+query nonces into hint pools, and its lincheck tail-offset slice now skips the opening's stream words (counted from the config shapes). - The guest's open_stacked takes the main stream cursor: msg_cursor IS the stream, level roots are two fs_next words (replacing the 3-absorb byte form), yr fills from the stream, and grind nonces are raw cursor reads bound by their DS_POW absorb. Six hint pools die. recursion_2to1 guest cycles 2,537,008 -> 2,516,950. Suite 241 + 3 ignored green (both heavy recursion suites pass), clippy clean, xmss CLI at 157.8 XMSS/s. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> flock: re-add the standalone batch BLAKE3 proving test The purge (2956d38) deleted tests/blake3_bench.rs along with the standalone flock prover API it exercised (prove_fast_timed, flare transcript, statement_digest). This brings the workload back on today's API: witness-gen -> commit -> Blake3Setup::prove_validity_stacked (zerocheck + lincheck reduction, one stacked Ligerito open) -> verify_validity_stacked, over FLOCK_N compressions (default 8192, Secure profile) with per-phase timings and a verify + finish gate - the fast loop for iterating on the flock reduction / PCS without the xmss harness. RAYON_NUM_THREADS=11 FLOCK_N=131072 cargo test --release -p flock \ --test blake3_batch -- --nocapture Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> lean_vm: the Ligerito proof moves out of RingSwitchVerify RingSwitchVerify becomes a plain claims bundle (no lifetime): the opening proof is not ring-switch data, it is the ONE stacked proof covering the slot claims too, so pcs::verify now takes it as its own parameter. The caller (cpu::verify) reads it off the openings hint channel at its protocol point and passes the borrow straight through - dropping the .clone() that copied the whole Merkle-bearing proof (next_opening returns &'a tied to the deserialized Proof, not to the VerifierState borrow), and the stale "BLAKE3 attachment" field doc with it. No protocol change. Suite 240 + 3 ignored green, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> recursion guest: baked prefix-mask table replaces the hinted overlap mask claim_overlap_mask's content is fully determined by the already-pinned claim_nover (the prefix of exactly nover ones), so instead of hinting + certifying it, the guest bakes ALL cap+1 possible prefix masks into one constant table (row t = [k < t]) and each claim selects row nover by pointer arithmetic (nover_g ** YR_LOG_CAP, a 3-MUL square-and-multiply). Mask reads stay one DEREF; the hint stream and the booleanity, monotone-prefix, and popcount pins all vanish (the prefix property holds by construction). The hi-span zero asserts stay and double as the nover <= yr_log_n pin: a larger nover selects a row whose prefix reaches into the asserted span. nover's range check tightens from SIZE_BITS to YR_LOG_CAP + 1, which also pins the row select to the table. (A first attempt wrote the mask with two runtime mul_range loops per claim; loop-call overhead cost +16.5k cycles, so it was dropped for the table select, which is straight-line.) The host stream and its tamper case in recursion_soundness_binds go away; the mask is no longer prover-chosen and the claim_nover tamper covers the overlap path. Parser: an integer log bound folds like any parse-time size, so `assert log x < YR_LOG_CAP + 1` works. recursion_2to1: 2534682 -> 2516928 cycles (-0.7%), bytecode 314764 -> 305887 instructions. recursion_2to1(+mixed) and recursion_soundness_binds pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> zkDSL: list literals — `x = [a, b]` is an initialized StackBuf New sugar for the alloc-then-store idiom: `x = [a, b, …]` allocates a StackBuf of the element count and writes each element in place, through the same stack-store path (copies/constants still defer as aliases), so the emitted code is identical to the manual form. Elements lower before the name rebinds, so `s = [s[1], s[0]]` swaps through the old binding. The recursion guest drops ~25 three-line StackBuf init blocks for it; bytecode is unchanged (314764 instructions, same committed witness). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> recursion guest: walk the flock message regions in order too The flock zerocheck multilinear-round messages (zc_msgs) and lincheck-round messages (lincheck_msgs) were the last "reserve region, offset-read later" sites: `zc_msgs = cursor` / `lincheck_msgs = cursor` plus a bulk skip. Walk them in stream order with fs_next instead. The unroll rounds walk the cursor directly; the flock multilinear mul_range threads it through a new flock_round_cursor heap chain, exactly like the GKR/AIR rounds thread gkr_round_cursor. The `cursor *= nmlv_g * nmlv_g` and `cursor *= GEN ** (2 * LINCHECK_ROUNDS)` skips are gone; the cursor now walks every stream word in order, and the only remaining cursor moves are the heap-chain seeds and the raw grinding nonce. Transcript unchanged: recursion_2to1 / _mixed verify with the committed witness identical (2^26.079). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> recursion guest: fs_next fetches, observes, and advances in one step Rename read_obs -> fs_next and have it return the advanced cursor too, so a stream walk is `fs, x, cursor = fs_next(fs, cursor)` with no manual `cursor *= GEN`. Every per-word read now walks: sequential regions thread a running cursor; fixed-base per-round loops (flock zerocheck/lincheck, the two aggregation sumchecks) thread within each read-pair, which also drops the `* GEN ** (2i+1)` offset multiplies. The three "reserve region, observe it as a block later" sites (zerocheck round-1, lincheck z_partial, ring-switch s_hat_v) now fetch-and-observe as they walk, into small HeapBufs. The only manual cursor moves left are genuine region-skips and the raw grinding nonce (absorbed later as DS_POW). Transcript unchanged: recursion_2to1 / _mixed prove and verify with the committed witness identical (2^26.079). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> compiler: inline multi-return can alias-return a g-address Generalize the inline tail-return binding so each returned value binds into the caller exactly as a `let name = <expr>` would: a `StackBuf` hands over its cell run, a folded g-address hands over its symbolic pointer, both aliased at zero copies; a scalar is copied into its dst cell. Previously only a StackBuf could be alias-returned (and only as the sole return value); a g-address among several returns would materialize into a cell, losing the free compile-time fold and the compile-time bounds check. Replaces the StackBuf-only `Option<Vec<Option<(Off,u32)>>>` record with a `RetBind` enum threaded through lower_return / Stmt::Let / Stmt::LetTuple. New stack_buf test `inline_returns_advanced_cursor` covers returning (StackBuf, scalar, advanced-cursor) together and reading through the cursor. This is what lets the recursion guest's stream walker return the advanced cursor for free: `fs, x, cursor = fs_next(fs, cursor)`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> transcript: drop the flock/pcs sub-protocol domain-separation labels The zerocheck, lincheck, pcs-open-batch, packed-direct, ring-switch, and ligerito-basis sub-protocols each absorbed a `b"flock-*-v0"` label into the Fiat-Shamir transcript. These were redundant: the transcript is a strict hash chain with a fixed, non-adaptive verifier structure, so a segment's position already identifies which sub-protocol it belongs to, and the top-level seed (the flock-family + program digest) separates this proof system from any other. Remove all six labels symmetrically from prover and verifier (crates/flock and crates/pcs) and from the recursion guest's replay, plus the now-dead guest label constants, harness placeholders, and word16 helper. flock (74), pcs (62), lean_vm (15), and rec_aggregation (recursion_2to1 + _mixed) all still prove and verify. The recursion guest shrinks 315445 -> 314920 instructions (1008 fewer BLAKE3 absorbs); a pass requires the native proof and the guest replay to agree, confirming the removal is consistent. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> refactor: give recursion DSL placeholders descriptive names Pure mechanical rename of cryptic placeholders in recursion.rs and the xmss_aggregate/recursion guest; no behavior change. - N_INNER_ROUNDS -> N_FIXED_CHALLENGE_ROUNDS, INNER7 -> FIXED_CHALLENGES, I7INV -> ONE_PLUS_CHALLENGE_INV - {ZC,LC,OB,RS,PD,LIG}LBL A/B -> {ZEROCHECK,LINCHECK,OPEN_BATCH, RING_SWITCH,PACKED_DIRECT,LIGERITO_BASIS}_LABEL_0/1 - GG dropped in favor of the builtin GEN; GINV -> INV_GEN - ILD0/1/2 -> LAGRANGE_INV_0/1/2; ILAM/ICMB/ISDOM -> LAGRANGE_INV_{LAMBDA,COMBINED,S} - PHI -> PHI8_NODES; DELTA -> TRACE_DUAL_BASIS; SEEDB0/1 -> TRANSCRIPT_SEED_0/1 - merge duplicate NCL/NCLAIMS into a single N_CLAIMS Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> fiat-shamir: fuse stream read + sponge absorb into one read_obs The recursion guest repeated `x = cursor[..]; fs = obs(fs, x); cursor *= GEN` at every proof-stream read, maintaining the "observe before it influences a challenge" invariant by hand at each site. Fuse read+observe into one `read_obs(state, cursor) -> (state, x)` so a stream word cannot enter the computation unbound. That needs an @inline to return the sponge state (a StackBuf) alongside the consumed scalar, which the lowering forbade: it aliased a returned StackBuf only when it was the SOLE return value, and a multi-value return routed every element through expr() (panicking on a StackBuf). Generalize `inline_stack_ret` from one `Option<(Off,u32)>` to per-slot `Option<Vec<Option<(Off,u32)>>>`, so each returned value is independently a StackBuf alias or a scalar cell; lower_return / Stmt::Let / Stmt::LetTuple bind each accordingly. `fs` stays a StackBuf and obs/squeeze/absorb are unchanged. Guest transcript is unchanged: the recursion guest compiles byte-identically (315445 instructions, same MUL/DEREF counts), and recursion_2to1 / recursion_2to1_mixed still prove and verify. New stack_buf test covers the inline StackBuf+scalar tuple return in isolation. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> naming feat: cache XMSS benchmark signers to disk Signer generation (keygen over slots 0..=15 + grinding sign) is the untimed setup cost of the aggregation benchmark and dwarfs proving for large batches. Generate each signer once, store the batch to disk under target/signers-cache/, and reload on later runs. The cache is a growing pool keyed on a footprint of the generation parameters (not on n), so bumping LEANVM_XMSS_N only generates the new tail and never re-does a smaller run's work. Also memoized in-process. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> benchmarks perf: fs_seed no longer rebuilds + rehashes the circuit family per process 82f4f74 made every transcript seed depend on the flock circuit-family digest, whose OnceLock init called build_block_r1cs(3) and hashed the matrices entry by entry: ~200 ms of symbolic matrix building (a second copy, next to the setup's own) plus ~250 ms of per-entry blake3::update calls over 21M nonzeros, landing inside the first prove. On XMSS x820 that cost ~6% on a 16-core x86 box and ~25% on an M4 Max (1.6 s prove). Three fixes: - flock::blake3::FAMILY_DIGEST: the digest is a constant of the circuit family, so bake it; family_digest_matches_baked recomputes and compares, failing on any circuit change until the constant is bumped. Same value as before, so fs_seed and the recursion guests are untouched. - build_block_r1cs clones the cached matrices() instead of re-running the symbolic builder: setups and const-pin lookups share one build per process (200 ms -> 72 ms per extra call). - absorb_matrix flattens to one buffer before hashing (244 ms -> ~10 ms), keeping the byte stream (and digest) identical. XMSS x820, 11 threads, x86: 5.55 s before 82f4f74, 5.87-5.94 s after, 5.46 s now. Suite 235 + 3 ignored green, recursion suites pass, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> polish: apply ~104 review findings across all crates Comment/naming/dead-code pass over the new workspace: - fix stale docs referencing purged code (BaseFold targets, jagged, default_config, verify_succinct, prove_batched, record structs) - re-attach doc blocks that had drifted onto the wrong item - rename ceil_log2 -> log2_ceil (naming convention), LigeritoLevelConfig k_levels -> k (scalar, not a collection), VerifyError::PcsAb -> Pcs - delete leftovers: empty impl blocks, unused locals, apply_triple (+test), dead rounds vectors in lincheck, fold_packed_witness_at_z - gate test-only items (#[cfg(test)]): stacked prove/verify wrappers, witness::stack, udr_queries; keep the general NTT entry points pub - fix stale crate paths in misc/doc.tex cargo test --workspace: 234 passed + 3 ignored; ignored recursion suites pass; clippy warning-clean across all targets. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> restructure: vendor/ dies, the repo becomes 8 clean workspace crates crates/ primitives GF(2^128)/GF(2^8) field kernels (+ phi8, g-power helpers), bit transposes, multilinear/eq/Lagrange helpers, the scratch pool, alloc/log2/perf utilities fiat_shamir the VM-native sponge + the ProverState/VerifierState …

main's `faster Ring Switching verifier for GHASH` is specific to the field this branch removed, so its math does not carry over. Resolution per file: * `pcs/ring_switch.rs`, `pcs/lib.rs`: ours. The new closed form (`linearized_eq_coeffs_eq` and its 15 seed constants) needs two things this branch no longer has. It needs a *power* basis of the opening field, built from the sparse GHASH modulus x^128+x^7+x^2+x+1, whose trace-dual is reversed monomials plus a 7-term correction; our E is the degree-3 tower over GF(2^64), so its F_2 basis is the product basis {base[i] * tower[j]}, not alpha^i. And it needs *eq* coefficients, so that the 128-term sum splits into a 7-factor product; we batch the coordinates univariately with (1, rho, ..., rho^191) instead. Our counterpart optimization is already in: the tower factorization delta[64j+i] = base[i] * tower[j] splits c_k into two Horner evaluations. Main's `RingSwitchVerifierOutput` removal also does not apply, since ours carries `coordinate_weights` rather than an `eq_r_dprime` tensor, and the stacked verifier now lives in `pcs/stack_open.rs`. * `guests/recursion.py`: ours. Same reason, plus git silently took main's `c_table = StackBuf(FIELD_BITS)` outside any conflict hunk; our c_table is written and read at runtime exponents from `mul_range`, so it must stay a HeapBuf. * `rec_aggregation/src/recursion.rs`: ours, taking main's switch to `parse_with_replacements(include_str!(..))`. That part is field-independent: it drops the runtime read of the guest source from CARGO_MANIFEST_DIR. Kept our `TRACE_DUAL_BASE`/`TRACE_DUAL_TOWER` placeholders over main's `RS_COEFF_ORBITS`, and kept the guest cache. The generalized ring-switching note and its CI job come in unchanged; its new closing section documents the GHASH closed form as a specialization of the general construction this branch instantiates at f = 64, e = 192. Full workspace test suite passes, including the two `#[ignore]`d heavy recursion tests. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

main's GHASH closed form (93a4f56) leaned on two properties this branch does not have: a power basis of the opening field, and eq weights whose 128-term sum factors into a 7-fold product. Both have analogues here, so the technique carries over after all; only Step 3 of the note is really weight-specific. Step 2 is generic in the modulus. For q = X^64+X^4+X^3+X+1 we have d = q'(x) = x^2+1, and the Laurent expansion of 1/q at infinity gives Tr(x^m/d) = [m = 63] for every m < 120, so beta_i is again a reversed monomial plus a sparse correction, this time on i < 4 rather than i < 7: beta_i = d^-1 (x^(63-i) + eps_i), eps = [x^3+x^2+1, x^2+x, x+1, 1, 0, ..., 0]. Step 3 changes shape. We batch the 192 coordinates univariately with rho^w, not with an eq tensor, so the weights do not factor over the bits of i and there is no product form. What replaces it is a geometric series: sum_{i<64} u^i = (u^64+1)/(u+1) = (1+u)^63, since 64 is a power of two, an identity that holds for every u including u = 1 where both sides vanish. With u = rho x^(-2^k), A_k = Q_k (1 + rho P_k)^63 + sum_{i<4} rho^i R_k[i]. (1+u)^63 by the 2^t-1 addition chain is 5 squarings and 3 products, so a level costs 13 multiplications: the same O(log f) the eq product reaches, via a different identity. The tower half is unchanged in principle but now also baked. gamma_0 = 1 (Tr_{E/K}(1) = 3 = 1 while Tr(y) and Tr(y^2) are symmetric functions of the roots of y^3+y+1 and vanish), which is also why beta lies in K and A_k has Frobenius period 64. Both orbits are fixed, so the guest bakes all 64 base levels and 192 tower levels instead of squaring a runtime orbit table: the 64x64 and 3x192 Frobenius tables in main() are gone along with their 4.6k products, and verify_sub no longer takes them. Also ported the field-independent half of 93a4f56: eval_rs_eq walks the runtime coordinates outside and the fixed 192 Frobenius powers inside, so z evolves by squaring in registers against one contiguous product row instead of through a stored z-power table. That removes roughly half the memory traffic of the hot 192 x ~38 nest, plus 384 per-level buffer allocations. Same product formula, same result. RAYON_NUM_THREADS=11, recursion --n 2, guest cycles: 2,196,207 before 2,142,542 closed-form coefficients -2.4% 1,977,096 + eval_rs_eq restructuring -9.97% total MUL 710,692 -> 641,783, DEREF 693,814 -> 591,205, data memory 2^21.322 -> 2^21.166. Program grows 609,056 -> 614,490 instructions, still inside the 2^20 pad. Short of main's >15% because the starting point was already better: the tower factorization and the period-64 base had cut coefficient construction to 9.2k products, where main's dense 128x128 Moore transform cost 16.4k. The remaining ring-switch cost is the transposed claim, which is 64 x 192 genuine products either way. New unit test checks the closed form against the dense 192-term Frobenius sum at every level. Full workspace suite passes, including the two ignored heavy recursion tests. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Seventeen warnings across five crates, all pre-existing. None were behavioural; recursion --n 2 still reports 1,977,096 guest cycles and a 376.539 KiB proof. * `pcs/ntt/additive_ntt_f64.rs`: annotate the ten NEON transmutes (missing_transmute_annotations). Only the inner ones in argument position were flagged; the outer ones are pinned by their let binding. uint64x2_t -> poly64x2_t is what vmull_high_p64 wants. * `flock/blake3.rs`: drop three needless borrows. The bindings are already `&[F192]`, so `&a_packed_words` was `&&[F192]`. * `flock/zerocheck/univariate_skip_optimized.rs`: allow identity_op on `xor_apply_byte_into_8_regs`. `0 ^ BH` is the i = 0 case of the `i ^ BH` row-select pattern, and writing it out keeps the four loads visibly parallel; a bare `BH` would hide that. * `pcs/merkle.rs`: `N % 64 == 0` -> `N.is_multiple_of(64)`. * `rec_aggregation/recursion.rs`: `stack_mus` is read only by `recursion_soundness_binds`, which needs the selected dispatch candidate to place its residual-coordinate tamper. Marked `cfg_attr(not(test), allow(dead_code))` rather than deleted. * `xmss`: drop the `primitives` dependency, which nothing in the crate referenced. Also carries an unrelated README edit made alongside: the XMSS aggregation example now runs 890 signatures. `cargo clippy --workspace --all-targets` is clean in both dev and release, as is plain `cargo build --all-targets`. All 263 tests pass, plus every ignored test except `print_ligerito_query_counts`, which is a manual parameter report that panics unless LIGERITO_LOG_INV_RATE and LIGERITO_NUM_VARS are set; it fails identically before this change and passes when given them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The default inner workload committed 2^25.06 words, so it padded to a 2^26 PCS with the top level almost empty. Any layout change that shaves a few percent of real data therefore drops the inner proof a whole PCS level, and a recursion measurement taken across that boundary compares a 2^26 opening against a 2^25 one rather than the verifier itself. 64000 iterations commits 2^25.655 here, filling most of the 2^26 bucket, so the figure stays comparable across layout work. The inner program's DEREF range check gives out just above 66000, so this is close to the ceiling this shape allows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Brings in main's `Tail-call the mul_range loop helper` (1efa725). One conflict, in `lower.rs`: main added a `tail: bool` parameter to `lower_call`, this branch added return-shape assertions in the same `call_into` body. Kept both. Two further call sites needed the new argument -- one auto-merged, and `lower_call(.., physical.len(), ..)`, which only exists here because of the StackBuf-return work. `recursion_soundness_binds` then failed its own precondition: test config's yr_log_n (5) reached YR_LOG_CAP (5) Not a soundness break -- that assert exists so shape drift fails loudly instead of silently skipping the tamper. The tail call removes two instructions per loop iteration, which shrinks the inner witness enough to drop the test's committed log-size from 24 to 23, and 23 is one of the two candidates whose residual log sits exactly at the cap, leaving no pad coordinate to corrupt. Moved the config from (8, 2^13) to (8, 2^14), which restores stack_mu = 24 and yr_log_n = 3, so the over-read path is exercised again. recursion --n 2 on this branch: inner cycles 1,856,262 -> 1,728,250 -6.9% guest cycles 1,975,790 -> 1,961,840 -0.7% JUMP 35,935 -> 21,925 The inner figure matches 2*(64000-1) + 2*(8-1) = 128,012 exactly, as on main. The guest saves 2 cycles for each of ~7,000 tail-called iterations. Full workspace green: 263 tests plus both ignored heavy recursion tests. Clippy clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`{:.2}` applied to the String returned by pretty_f64 is a max-WIDTH spec, not a decimal precision, so the ratio printed as "0." instead of "0.532". Restore pretty_f64 across the whole report block (the pow closure and the [inner] re-print had also drifted to raw {:.2} floats, making the re-print disagree with the one prove_inner emits), widen the pow column back to 9 for the extra digit, and drop a duplicated committed-witness-size line. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

TomWambsgans and others added 30 commits July 4, 2026 21:42

Condense the field-question section to a TLDR

be2a199

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Clarify PCS throughput units (gigabits, not gibibytes)

e2e40d3

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>

wip

416560c

TomWambsgans and others added 8 commits July 16, 2026 15:58

Optimize Johnson eta per recursive level

be2491a

Use query grinding to reduce proof size

9871e88

Merge branch 'main' into small-proof

2f68b07

add pcs_throughput benchmark

6ad0bed

make tests pass

b60c74d

remove 128 bits fields

d8dfe8b

TomWambsgans force-pushed the small-proof branch from 70af811 to d8dfe8b Compare July 18, 2026 12:51

TomWambsgans added 14 commits July 18, 2026 14:05

enable tracing

f1a7750

primitives: add AVX-512VBMI bit transpose

84b70d4

improve hierarchical PCS tracing

32f55ea

pcs: vectorize F192 NTT with AVX-512

68fdc94

Pretty-print displayed integers with commas

3a261aa

Document MCA error in unique-decoding regime

7be40ba

Support StackBuf returns from normal functions

1a2258d

Merge branch 'main' into small-proof

e9f5c3c

# Conflicts: # crates/flock/src/blake3.rs # crates/flock/tests/blake3_batch.rs # crates/lean_vm/src/blake3_flock.rs # crates/lean_vm/src/cpu/layout.rs # crates/lean_vm/src/cpu/mod.rs

TomWambsgans force-pushed the small-proof branch from 3a4f981 to c834012 Compare July 22, 2026 23:32

TomWambsgans and others added 6 commits July 27, 2026 15:00

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Small proofs - #4

Small proofs#4
TomWambsgans wants to merge 101 commits into
mainfrom
small-proof

TomWambsgans commented Jul 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

TomWambsgans commented Jul 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant