Recursion#2
Open
TomWambsgans wants to merge 193 commits into
Open
Conversation
The primitive behind Merkle query-index extraction and PoW leading-zero checks: a GF(2^128) element is its 128-bit polynomial-basis vector, and the basis monomial x^i equals GEN**i for i<128, so we hint the bits, boolean- constrain each (b*b==b), reconstruct Sigma b_i*GEN**i via a compile-time-folded running weight, and assert equality. Full-width so reconstruction is exact. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The transcript sponge is the blake3-opcode compression with a domain tag in the second word: observe = compress(cv,[x,DS_SCALAR]), sample = compress(cv,[0, DS_SQUEEZE]). The guest re-derives byte-identical challenges to vmhash::compress (the opcode's Rust twin) — the core of replaying an inner proof's transcript. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…verifier spec Completes the Fiat-Shamir challenger surface the recursion verifier needs, all validated in-circuit against vmhash::compress: - transcript reader: read a hinted inner-proof stream via a GEN-cursor, absorb each scalar (next_scalar), then sample (the transcript-replay mechanic). - observe_bytes(root): length-frame + two DS_BYTE words = the level-commit binding. Key reconciliation from the Ligerito verifier spec: leanVM-b OVERRIDES flock's Challenger trait (transcript.rs), so the PCS drives leanVM-b's own compress-sponge (not flock's native FsChallenger). observe_f128_slice and sample_f128_vec use the trait defaults (per-element / n sequential), so the whole PCS challenger surface is exactly the sponge already validated here. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…gen)
First code-generated verifier: a Rust emitter unrolls gkr::verify_product for a
fixed mu into straight-line zkDSL (the real verifier will dispatch runtime mu to
such variants via match_range, as the reference's whir.py does). The guest
replays a REAL gkr::prove_product transcript fed as a hint_witness stream —
running every eq-trick round check and Lagrange interpolation at nodes {0,1,g}
(inverse-denominators baked as constants), threading the sponge and the running
claim itself — and publishes the final leaf-claim value, pinned via write-once to
the value the native verifier returns. Verified across mu in {1,2,3,5}.
Also adds fs_ref::seed_cv: a faithful Rust mirror of Sponge seeding, so the guest
starts its transcript replay from the exact chaining value (the harness will bake
this in). That the sampled challenges matched proves the seed reproduction.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Leaf hash = the length-in-IV MD chain vmhash::hash_slice (== flock merkle::hash_leaf); internal nodes = compress(left,right) with sibling order gated by the query-index bit (idx&1, LSB-first bottom-up) via an if-branch over boolean-constrained bits. Validated against Rust-built trees for every query at depths 1..4. (Batched octopus multi-proof reuses this per query; shared-node handling comes at assembly.) Foundational primitives for the Ligerito verifier are now all in place: bit-decomposition, FS sponge (observe/sample/bytes/reader), degree-2 sumcheck/GKR, and Merkle path verification. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Zerocheck replay (constraints.rs): the degree-2 sumcheck core with the zerocheck
wrapper — sample eta + point r up front, claim starts 0, close with
claim == eq_acc*c_eval(eta,evals). Test constraint c=a+b (column equality);
validated tau in {1,2,3} against native constraints::prove/verify. The 6-table
verifier will codegen a per-table c_eval (AIR-evaluator codegen).
misc/recursion-plan.md documents the architecture, the done gadgets (bit-decomp,
FS sponge, GKR sumcheck, Merkle, zerocheck), and the remaining assembly (Ligerito
opening: RoundQuad sumcheck, sample_distinct_queries, octopus multi-proof,
ring-switch tensor, enforced-sum/residual; flock reduction; full replay + harness).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The last foundational pattern: a mul_range loop whose bound is a RUNTIME g-power,
threading the 256-bit chaining value through a write-once HeapBuf (Fibonacci
idiom, since mul_range can't carry a StackBuf and memory is write-once). Step j
reads cv_j at cells 2j,2j+1 and writes cv_{j+1} at 2j+2,2j+3; cv_N is then read
back at the runtime address nbound*nbound. This is the pattern every runtime-
length loop in the Ligerito verifier (query loops, runtime round counts) will use.
All primitive patterns for the Ligerito assembly are now validated in-circuit:
bit-decomp, FS sponge, degree-2 sumcheck (GKR + zerocheck), Merkle path, and the
runtime-count carried loop.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The Ligerito-specific sumcheck flavor: 2-eval messages {u_0,u_2}, running quad
u(X)=c+bX+aX² rebuilt each round as (c=u_0, b=t_r+u_2, a=u_2) — baking the
u(0)+u(1)=t_r consistency in — advancing t_r <- u(ri) per fold. The guest replays
the fold (read msg0 -> quad -> per fold {sample ri; t_r=eval; read msg; rebuild})
and pins the final t_r; validated k in {1,3,6} vs a Rust reference. Both sumcheck
flavors are now in hand (eq-trick for GKR/zerocheck, RoundQuad for Ligerito).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Composes three GKR product verifiers over ONE shared transcript into a single guest and checks push_root == pull_root (the two bus sides are the same multiset) and count_root != 0 (via a hinted inverse — assert has no !=, so nonzero is proven by exhibiting x^-1). This is the essence of leanVM-b's bus balance argument, and the first multi-sub-protocol COMPOSITION: several sumchecks + a cross-product relation replayed end-to-end against a real leaf-style transcript. emit_gkr_verify_body factors the GKR replay into a tag-prefixed reusable emitter so multiple products verify back-to-back sharing the sponge/stream cursor. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Two findings that reshape the remaining path: (1) the harness compiles the guest for ONE known inner-proof shape, so all sizes are compile-time constants and the straight-line codegen suffices — no runtime match_range dispatch needed for a first end-to-end; (2) no compiler enrichment was needed for any primitive. Also scopes the genuinely-hard remaining sub-problems (ring-switch 128x128 transpose, F8 Lagrange, FRI/NTT fold math, octopus multi-proof) and the Rust-mirror method. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
First real stage of the actual Ligerito opening (ring_switch::verify_succinct's
claim check): rebuild the 128 claim weights from HINTED z_skip + x_outer_0 and
check Sigma weights[i]*s_hat_v[i] == claim. weights[i] = lambda_{i&63}(z_skip) *
eq(x_outer_0, i>>6), with lambda_j the phi8 F8-Lagrange basis — numerators
prod_{l!=j}(z+s_l) formed in O(64) via prefix/suffix products, s_l = PHI_8_TABLE[l]
and the inverse-denominators baked as constants. Validated against flock's own
build_claim_weights + claim_check. This exercises genuine runtime F8-Lagrange, one
of the opening's four hard sub-problems.
Adds flare as a dev-dependency so gadget tests can cross-check against flock's PCS
primitives directly.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The second (and heaviest) half of ring_switch::verify_succinct: the 128x128 bit-transpose s_hat_u = T(s_hat_v) folded against eq_r_dprime. Reordered to sumcheck_claim = Sigma_i x^i*(Sigma_b bit_b(s_hat_v[i])*eq[b]); per row the guest hints the 128 bits, boolean-checks them, reconstructs Sigma bit_b*GEN^b == s_hat_v[i] (pinning the bits), and folds Sigma bit_b*eq[b]. The inner b-loop is a helper function compiled ONCE and called 128x, so the ~80k-op transpose is a few hundred bytecode instructions, not a flat unroll (which would be ~80k lines). Cross-checked against flock's tensor_algebra_transpose + inner_product; proves in ~4s. Both hard halves of verify_succinct (phi8 F8-Lagrange claim check + the transpose) are now validated in-circuit. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…stage 1) End-to-end port of the first stage of leanVM-b's Ligerito opening, verified against native flock: seed the compress-sponge, absorb the protocol label, observe the 128 s_hat_v, sample r'' (7), build_eq(r''), run the claim check (Sigma weights*s_hat_v == claim), and the transpose fold (Sigma_i x^i * Sigma_b bit_b(s_hat_v[i])*eq[b]) == native sumcheck_claim. The sponge-derived r'' must match native for the fold to agree, so this exercises the whole stage together. A complete, real Ligerito-opening sub-protocol verified in the guest language — the whir.py-analog milestone at the stage level. Retires both hard sub-problems of stage 1 (phi8 F8-Lagrange + 128x128 transpose). Composes: seed_cv, observe loop (helper), sample, build_eq, weighted inner product, transpose (helper). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
leanVM-b's opening is verify_opening_batch_mixed_ligerito_stacked -> ligerito::recursive_verifier_with_basis_succinct (Ligerito backend). The single-claim verify_opening -> basefold::verify path (NTT fri_fold_coset) is a different scheme leanVM-b does NOT use; drop it from the plan. ring_switch:: verify_succinct (stage 1, done) is shared by the stacked Ligerito path, and the RoundQuad sumcheck gadget is the Ligerito core fold — so no work is wasted. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The Ligerito core's sample_distinct_queries draws a runtime number of challenges
via sample_f128 to derive query indices. This validates squeezing inside a
mul_range with a RUNTIME bound, threading BOTH the sponge chaining value AND an
accumulator through write-once HeapBufs (step j: cv_{j+1}=compress(cv_j,[0,
DS_SQUEEZE]), fold cv_{j+1}[0] into a running XOR), reading the result back at the
runtime address nbound. Matches a native squeeze loop.
With this, every constituent capability of the Ligerito core is validated:
RoundQuad fold, squeeze-loop query sampling, Merkle path, bit extraction, eq-table
/dot-product arithmetic, runtime loops + helper functions, and the complete
ring_switch::verify_succinct (opening stage 1). Remaining: the multi-level
assembly of recursive_verifier_with_basis_succinct + top-level batch + harness.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Drives flock's real recursive Ligerito prover + succinct verifier at a tiny config (log_n=8, initial_k=2, k_0=2, r=1, 1 query/level) with a leanVM-b ProverState challenger (the compress-sponge the guest replays), and confirms native accept. With 1 query/level the octopus multi-proof degenerates to a single Merkle path (depth 7 at L0, 5 at the last level), num_interleaved=4, yr_len=16, 6 sumcheck messages — the concrete shapes the zkDSL port consumes. Widens ligero_commit / eval_sk_at_vks / induce_sumcheck_* / ceil_log2 / LigeroWitness to pub in the vendored flock so tests can drive + cross-check the tiny instance. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… port spec Extends fs_ref to a stateful Sponge mirror and replays recursive_verifier_with_ basis_succinct for the tiny instance step-by-step (prologue, L0 lane fold, L0 query + enforced-sum glue, recursive-level folds, last-level yr observe + query, and the residual: induce_sumcheck_evaluate_at_residual per level + eq_eval eval_b + terminal inner==t_r). The mirror reaches inner == t_r, matching native accept — so the exact challenge order, RoundQuad arithmetic, enforced sums, residual formula and terminal check are all confirmed. This executable mirror IS the porting spec for the zkDSL guest; it also extracts the query samples (q0, q_last) whose bits the guest hints. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A complete zkDSL port of recursive_verifier_with_basis_succinct — leanVM-b's ACTUAL Ligerito opening scheme — verified end-to-end against a REAL flock LigeritoProof, proven and checked by leanVM-b's own prover/verifier. The guest replays the full protocol: sponge (label/target/roots/sumcheck msgs/yr/nonces), the RoundQuad sumcheck (prologue + L0 lane fold + level fold), the enforced-sum glue, single-path Merkle opens (leaf MD-hash + walk by query-index bits, with the bits pinned by full 128-bit decomposition of the sampled query values), and the residual check (novel-basis Ŵ_k recurrence per level with sks_vks constants + eval_b + terminal inner == t_r). Cross-checked against a Rust mirror that matches native accept. This is the whir.py analog for leanVM-b: a working recursive PCS-opening verifier in the guest language. Tiny config (log_n=8, 1 query/level) for tractability; the codegen is config-driven so it scales to the production shape (more folds, queries, levels — same structure, no new capability). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
500-XMSS proof -> committed 2^25.3 -> mu=26 -> flock config m33_secure (log_n=26): 6 levels, initial_k=6, r=5, queries [290,177,145,132,126,124] (994 total Merkle opens), rates [1..6], recursive_ks [3;5], fold_grinding_bits [11,10,8,6,4,2] (real leading-zero PoW), yr_log_n=5, 27 sumcheck messages, octopus multi-proofs (3443 hashes at L0), 64-lane L0 leaves. Native drive works: commit ~47s (2^26 witness), recursive prove ~4.3s, native verify ~15ms. This is the shape the in-circuit guest verifier must handle for production-scale recursion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ed in Rust Extends fs_ref::Sponge with verify_pow (leading-zero PoW mirror) + sample_distinct_ queries (rejection). The m33 probe now runs a general mirror reproducing the entire 6-level production verifier: prologue + L0 lane fold with fold-PoW + per-level query phases (sample_distinct_queries + alpha + enforced-sum glue) + last-level yr + the residual over all 994 queries. Reaches inner == t_r (matches native accept). This is the executable porting spec for the m33 guest verifier — every challenge, PoW nonce, query set, enforced sum and residual reproduced exactly. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Refactors the m33 mirror into a reusable, config-driven run_mirror(cfg, proof, z, target, label) that replays the full verifier for any Ligerito config and returns per-level query data (sorted positions, raw samples, alpha, beta) + ris + ctx info. Adds a small dev config (log_n=12, 3 levels, queries [6,5,4], fold-PoW [3,2,1]) for fast iteration on the guest port — and it exercises the rejection path (level 1: N=5, T=6 raw samples). Foundation for the config-driven guest verifier codegen. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The m33 config grinds fold challenges (bits 11,10,8,6,4,2). verify_pow computes base=compress(cv,[0,DS_POW]), then requires compress(base,[nonce,DS_POW]) has enough leading zero bits. Matched exactly: pow_bits_ok checks the low full bytes zero PLUS the top extra bits of byte full (MSB-first within a byte). The guest recomputes both compressions, decomposes the digest word, and asserts that exact zero-bit set. All primitives the production m33 verifier needs are now validated in-circuit. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Renames the working end-to-end verifier test to test_recursive_ligerito and prints cycles / per-opcode counts / committed witness / proof size / prove+verify time, like the XMSS benchmark. Runs the complete in-circuit Ligerito opening verifier against a real flock LigeritoProof. Current config is the tiny one (log_n=8, 1 query/level): 2722 cycles, 64 BLAKE3, 2^17.6 committed, 450 KiB proof, ~0.6s prove, 30ms verify. Scaling the config to m33 (500-XMSS shape) is the in-progress assembly. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…placements) Per feedback, stop embedding long zkDSL in Rust format! strings. The Ligerito opening verifier now lives in tests/ligerito_verifier.py — a readable zkDSL program with sponge/merkle/fold helpers (obs/absorb/sqz/chk/hleaf/mstep/foldyr) and *_PLACEHOLDER constants filled per proof, exactly like the reference recursion.py. test_recursive_ligerito loads it via parse_file_with_replacements, drives a real proof + the config-driven run_mirror, and prints XMSS-style stats. Also simplifies the terminal: the per-y sum becomes folds of yr (MLE eval / weighted fold), removing 16 EVB constants and the per-y unroll. Still verifies end-to-end. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The tiny Ligerito verifier is fully expressed in tests/ligerito_verifier.py, so the ~215-line Rust format!-string emitter is gone. 17 gadget tests green (+1 ignored m33 probe). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ort) Per direction: the verification algorithm must not dedup/sort queries — that is a proof-STORAGE compression only. Changed the vendored flock _with_basis prover + succinct verifier to sample query positions in transcript order (no dedup, no sort) and verify each opening with its own single Merkle path (sample_queries_ordered + merkle_paths_for + verify_level_opens_perquery), instead of the sorted-distinct octopus. enforced_sum/residual now range over the sample-order query list. The octopus stays available for the legacy/dense paths as storage compression. This keeps the core verifier flat, so the in-circuit port carries NO dedup/sort/ octopus logic. Validated: small-config mirror (T=N now) and m33 native verify + mirror both reach inner == t_r. fs_ref mirror updated to sample-order. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…m33 opening pattern Verifies N independent per-query Merkle openings in ONE mul_range loop (body compiled once); each query has one single path, offsets derived from the counter x=g^i (leaf at x^2, path at x^4, bits at x^2). mul_range bodies can call helper functions (hleaf2/mstep). This is how the m33 verifier opens ~994 queries without unrolling — no dedup/sort, one path per query. With this, every m33 pattern is validated: runtime Merkle loop, runtime squeeze loop, fold-PoW leading-zero, RoundQuad, enforced-sum + residual folds. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…+enforced loops) gen_lig_tr emits the config-driven multi-level Ligerito verifier t_r core as zkDSL .py: sponge replay, RoundQuad lane/recursive folds, per-fold PoW leading-zero checks, and per-level query phases built as mul_range runtime loops (sample-advance loop + enforced_sum accumulator loop + glue) — the m33 opening pattern, no dedup/sort. Test ml_tr_small drives a real 3-level small-config proof; the guest t_r matches the mirror exactly (with fold grinding [3,2,1]): 8956 cycles, 119 BLAKE3. Enforced loop indexes eq via a g-power cursor (buffer[g^c]=cell c), not the buffer pointer. Remaining for full end-to-end: per-query Merkle loops + residual loops + terminal inner==t_r, then scale the same generator to the m33 config. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…int) Push and pull have equal depth by construction (matched bus-block pairs), so their grand-product trees now run in parallel sharing every challenge: per round the prover sends push`s message triple then pull`s, the verifier checks both against the SAME eq accumulator and samples ONE challenge; likewise one line challenge per layer. Both trees reduce to leaf claims at ONE shared point zeta. Sound by the standard union bound (two degree-2 differences per shared challenge). The count tree still runs alone. The shared point collapses everything downstream: - the six public bytecode columns are opened ONCE (bytecode_vals 12 -> 6); both bytecode blocks read the same evaluations (per-block indexing); - ONE reduced stacked-bytecode claim per sub instead of two; - the deferred region carries one bytecode point (DEFER_SIZE loses kbc + 1); - the aggregation`s bytecode batching handles NSUB claims, not 2*NSUB; - the guest stores zeta once (ZOFF[pull] == ZOFF[push] == 0). gkr.rs grows prove/verify_product_pair (single-tree code refactored into a shared LayerState + round_message/fold/shrink_eq helpers; the pair shares one eq table since the challenges coincide). leaf.rs uses the pair for push/pull. The guest`s GKR section splits into a lockstep pair block (a second claim chain, sumcheck_round3_pair reading six messages per round) and the single count block. Suite green (66 + 2 ignored, binding + broad shapes). recursion_2to1: 3,067,394 -> 2,962,938 cycles (-3.4%). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…pull Follow-ups to the lockstep GKR, both exploiting the shared push/pull point: 1. Claim dedup (native + guest). A column read by two blocks with the same kappa - across the pair (nearly every pull coord duplicates its push twin: addresses, values, counts as GCol/Col, pc/fp, operands, MEM) or within a side - now streams and opens ONCE. leaf.rs decompose_prove/verify share one claims list and look up (col, point) before streaming; duplicates reuse the recorded value (never re-streamed - a streamed-but-unopened copy would be a free knob). The guest mirrors with baked per-coord tables COORD_FRESH / COORD_CLAIM_SLOT (dedup key (group, col, kappa); the count side has its own point so it never dedups against the pair). Pool size NCL: 299 -> 190; the gamma batching, eval_b terminal, PCS opening batch, and proof stream all shrink with it. 2. Pull-side decompose reuse (guest). Pull blocks mirror push blocks (same kappas and offsets, generator-asserted) at the same zeta, so each pull block reuses its push twin`s eq_hi and Index-MLE value instead of recomputing offset advice + selector chains; the packing loop now skips pull entirely (its sort_order slots go unread). Pull`s own GKR-claim identity still binds everything it reuses. Suite green (66 + 2 ignored, binding + broad shapes). recursion_2to1: 2,962,938 -> 2,682,050 cycles (-9.5%; -14.5% total with the lockstep change, from 3,067,394). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review pass over the last two commits, cutting the code they added. Instead of running the two lockstep sumchecks side by side (double messages, a second claim chain, a dedicated sumcheck_round3_pair), the prover λ-combines the two trees` round messages so each layer is ONE standard sumcheck on the combined summand eq*(ea*oa + λ*eb*ob): - rounds send 3 scalars instead of 6 and the guest handles them with the UNCHANGED sumcheck_round3 (sumcheck_round3_pair deleted); - each layer binds the four tail evaluations, checks the combined product identity eq*(e0a*e1a + λ*e0b*e1b), samples the line challenge, then a FRESH λ - which pins the individual tail values inside the bound combination (Schwartz-Zippel); the last layer`s individuals are pinned by the decompose identities against the PCS-opened columns; - the guest`s pair and count blocks collapse into ONE loop body (run 0 = pair, run 1 = count) whose pair-only steps fold away at compile time; the round claim_b chain dies, replaced by two pair-only layer chains (pull value + λ). verify_recursive.py: -241/+154 this commit; net vs pre-lockstep the whole feature is +64 lines. Stream shrinks (3 msgs/round); suite green (66 + 2 ignored). recursion_2to1: 2,682,050 -> 2,665,640 (total -13.1% from 3,067,394 pre-lockstep). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The count grand product joins the push/pull RLC batch. count.mu <= push.mu always (each count column rides one push flush; the state flush has none), so the count tree is PADDED with identity leaves up to the pair`s depth: one line in leaf.rs (count_lay.mu = push_lay.mu) - build_leaves already fills the cube with 1 and decompose_formula already accounts the padding mass as 1 - sum(sel). The product is unchanged, so the count-root-nonzero semantics are untouched. gkr: prove/verify_product_pair generalize to prove/verify_product_triple (round messages combined with weights 1, λ, λ²; six tail evaluations; fresh λ per layer pins the individuals). The guest`s two-run GKR loop becomes ONE pass - no run branches, singleton chain buffers - and the cascade: - ONE shared point zeta for all three trees: the count-side claims dedup against push`s (the count columns already appear as GCol in push flushes at the same kappa), so the dedup key drops its group component and the count blocks contribute ZERO fresh pool claims; - annmus_count dies: there is ONE bus depth, hinted once (annmus_push) and certified against push`s block total only (count needs no depth cert - its depth is the pad target); - ZOFF dies: zeta shrinks to one MU_CAP region, every claim descriptor offset is 0. Suite green (66 + 2 ignored, binding + broad shapes). recursion_2to1: 2,665,640 -> 2,546,748 (-4.5%; -17.0% cumulative from 3,067,394 before the GKR work). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The triple prover/verifier returned three (root, LeafClaim) tuples whose
points were the same vector cloned twice - the type hid the one structural
fact the batch guarantees. They now return a ProductTriple { roots: [F128; 3],
point: Vec<F128>, values: [F128; 3] }, and the internals collapse into arrays
and loops (trees/msgs/evals indexed 0..3, Horner-combined). leaf.rs reads
bus_gkr.point once for all three decompositions and the bytecode opening.
Bit-identical transcript; suite green (66 + 2 ignored), same cycles.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The bus transcript was alpha -> grind -> gamma, leaving alpha outside the PoW window (its soundness rested only on the re-rolling-alpha-costs-a-fresh- commitment argument, >= 2^MIN_MU hashes). Grinding first puts BOTH bus challenges behind the PoW: re-rolling either means redoing it. Same ops, strictly stronger and simpler to reason about; the recommitment argument remains as a secondary justification in the grand_product_grinding_bits doc. Native prove/verify_balance and the guest reorder together; suite green (66 + 2 ignored), same cycles. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…die) grind_check computes its digest in-circuit, so its bit decomposition is hint_decompose_bits advice, filled and verified inside the helper - the grind_bits, fold_grind_bits, and query_grind_hint witness streams die, and grind_check loses its bits_ptr parameter. Same for decode_query_bits: the squeezed word is in-circuit, so query_index_bits dies too (the bits row is allocated per call; query_bit_ptrs still points into it for the Merkle direction bits). The LIG_QUERY_BITS_LEN/OFF tables and all four generator emissions (plus the bits_of flattening) are gone. Verification is unchanged (booleanity + reconstruction + zero-window); only the bits` source moves from the generator to runtime advice. Suite green (66 + 2 ignored); recursion_2to1 2,546,748 -> 2,544,338. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The bus depth was hinted only because the grind needed it before the mus cert ran. But block_kappa derives purely from kappa_base (available right after the count gadget), and log2_ceil_in_the_exponent is advice + asserts with no sponge or stream interaction - so the whole derivation moves BEFORE the bus section and g_bus_mu is computed outright: block kappas, push side total, log2_ceil. The hint, its tie assert, and the generator emission die; the transcript is unchanged (native untouched). The guest now hints NO structural quantity at all except dims_g[0] = g^log_mem (pinned to the announced word). Suite green (66 + 2 ignored); same cycles. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… hints die) Sweep for remaining hint-then-certify patterns replaceable by computation: - dims_g[0] = g^log_mem: assembled from the announced word`s advice-decomposed bits (new helper g_power_of_word: bits tie back to the word, g^L is P g^(bit_j 2^j)). The dims_g hint dies - the guest now hints NO structural quantity at all - and with it the g^j -> j lookup table (g_logs), whose only use was that pin: exponent_tables returns 2 tables, verify_sub loses a param. - pi_mem_slack / pi_fold_slack: divisions off the hinted min (g_log_mem / pi_cplen, fold_cap / pi_cplen), range-checked as before. - claim_low_len / claim_sel_len: divisions off claim_nover, the ONE genuine branch advice per claim (low_len = cplen / nover, seln = fold_cap * nover / nlow); the old tie asserts become definitions, the product pins and range checks stay, and the per-claim block reorders so the lengths exist before the low chain. claim_low_len stays as a guest-FILLED buffer (the y-slot overlap pointers re-read it); its binding tamper retires with the stream. Suite green (66 + 2 ignored); recursion_2to1 2,544,334 -> 2,543,410. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
cargo clippy --fix handled the mechanical ones (needless refs, repeat().take() -> repeat_n, collapsible ifs, same-type cast, manual += , len() == 0, enumerate with discarded index). By hand: parser`s constant division uses checked_div; lower`s specialized_body return gets a SpecializedBody type alias; execute`s six trace-row vecs are individual lets instead of one tuple type; leaf`s decompose_prove keeps its 8th arg (the shared dedup context) under an explicit allow; dead bits_of removed from the harness (all bit hints are advice now); index loops in the tests iterate their slices; flock-core`s perf_core_count_cached is allowed dead off-aarch64 (its caller is aarch64-only). Suite green (66 + 2 ignored), same cycles. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
B3TABLEN said nothing and SD abbreviated too much: the baked per-candidate flock statement-digest tables are now STATEMENT_DIGEST_TAB_0/1 with STATEMENT_DIGEST_TAB_LEN rows (guest locals statement_digest_tab_*/ statement_digest_*). The magic-5 family goes with them: tau5_g -> tau_blake3_g, and the count gadget keeps its generic per-iteration count_bits, aliased to blake3_count_bits below the loop for the constant-pin claim (the old bits5 alias dies). Suite green (66 + 2 ignored).
…nding flock`s mid-protocol bind_statement (label + per-instance digest + commitment root) was a standalone-system artifact. Everything it bound now binds earlier and once: - fs_seed (cpu::fs_seed): ONE 32-byte digest, as two field words, of everything fixed about the proving environment - the flock circuit FAMILY (per-block R1CS matrices + shape params, the new BlockR1cs::family_digest, which deliberately EXCLUDES the instance count: the instance is block-diagonal, m copies of the same matrices) and the program bytecode digest. It leads every transcript ([seed, seed, pi, pi]), so all challenges depend on the circuit version and the program before anything else. - the instance count is bound by the announced-sizes absorb; - the commitment root was already bound right after them. Both vendored entry points (Blake3Setup::prove/verify_reduction) drop the bind symmetrically; standalone flock paths keep theirs. The recursion guest carries the INNER program`s fs_seed in its public input (one hint, replacing inner_digest): it leads each sub transcript and folds into own_pi, so the outer statement pins the whole inner environment with one word pair. The guest`s bind_statement section dies, with the per-candidate STATEMENT_DIGEST_TAB_0/1 bake, R1CSLBL, and the tau table-bound assert (tau stays bounded by the count gadget < 34 = every flock buffer cap, and more tightly by q_pkd`s kappa feeding the dispatch-bounded committed size m). Suite green (66 + 2 ignored); recursion_2to1 2,543,410 -> 2,543,274. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…n claims The circuit always proves the same configuration (cv = IV, counter = 0, block_len = 64, flags = CHUNK_START|CHUNK_END|ROOT), so the constants move from per-proof claims into the circuit itself: the free-input rows for those bits become constant rows (set bit: z_const * z_const = z_s, clear bit: empty rows), leaving only the 512 message bits free. The lincheck const-wire pin stays load-bearing: an all-zero block still satisfies the matrices, and it is the all-ones constant column that activates the constant rows. All three witness emitters agree (matrix builder, lincheck walker, packed/batch-major row witnesses: constant rows now have a = b = z = val, the b side is no longer all-ones there), and witness generation asserts conformance up front. Consequences: - the three BLAKE3 pin claims disappear everywhere: native prove/verify (blake3_pin_point / blake3_pin_claims / mle_of_ones_then_zeros deleted), the guest (PIN_VALUES, PIN_ZETA_OFF, the pin_chain telescoping and 3 pool claims), and the harness descriptors (ncl formula loses its +3). The constants now bind through family_digest -> fs_seed, where a never-customized constant belongs. - padding instances become the pinned compression of the zero message, i.e. blake3(0^64): every batched instance, padding included, is a genuine BLAKE3 of one 64-byte block. The bool-witness path pads the same way. - vendored cleanups while there: the dead chain_e2e_tests module deleted (this fork dropped the chain API; chains are impossible under pinning), which un-broke the vendored test build and surfaced a stale layout test + stale offset comments from before the 128-alignment (M_BASE 513 -> 640); both fixed to the true layout. Vendored lib tests: 19 passed. recursion_2to1 guest cycles 2,543,274 -> 2,536,980. Suite 65 + 2 ignored, all green (one test fewer: the deleted helper took its unit test with it). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…er dies flock's challenger abstraction (Challenger trait, streaming-BLAKE3 FsChallenger, RandomChallenger, unsound-challenger feature) is gone. The whole stack now draws verifier randomness from ONE shared transcript, written in leanVM-b's own vocabulary: - flare::sponge: the VM-native Merkle-Damgard sponge (moved verbatim from src/transcript.rs, with compress, the domain tags, grinding, and the diagnostic trace, which the sponge now records itself); - flare::transcript: Proof / ProverState / VerifierState (moved from src/transcript.rs; they only need F128, LigeritoProof and the sponge, all already in flock-core). src/transcript.rs and vmhash::compress become re-export shims, so leanVM-b code is untouched. Every flock protocol function now takes the side-appropriate state, exactly like leanVM-b's own: prove/open take ps: &mut ProverState, verify take vs: &mut VerifierState (~70 signatures across zerocheck, lincheck, pcs, basefold, ligerito, ring_switch, jagged, verifier, prover, blake3). Side- agnostic sponge utilities (the Ligerito query samplers, standalone bind_statement) take &mut Sponge via the new ps/vs.sponge_mut() seam. The wrappers grow the FS-only methods the sub-protocols need (absorb_bytes, observe_scalars, raw grind_pow/verify_pow whose nonces ride flock's own proof structs, and VerifierState::detached for standalone flock proofs with no leanVM transport). Transcript bytes are UNCHANGED on the integrated path: the wrapper methods delegate to the same sponge ops the old Challenger adapter used. Proof: the recursion guest is untouched and recursion_2to1 passes at the same 2,536,980 cycles. Making the vendored test targets compile for the first time surfaced pre-existing rot, all confirmed failing at HEAD too: - packed-direct-only openings (n_rs = 0): the verifier sampled r_dprime that the prover never sampled (it lives inside the skipped ring-switch batch). Fixed by guarding on n_rs in all three verifiers; leanVM-b always has n_rs = 2, so its transcripts are unaffected. - the standalone permutation module (unused: leanVM-b runs its own GKR bus): deleted, like the chain code before it. - two batched-vs-sequential ring-switch comparisons stale since gamma-baking: #[ignore]d with the reason. Suites: workspace 60 + 2 ignored recursion tests, all green; flock-core 231 passed (was: did not compile); flock-prover 19 passed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
flock scalar sub-proofs used to be bincode-serialized structs pushed as raw hint bytes on the stream and re-absorbed by the verifier replay. Now they are ordinary transcript traffic, indistinguishable from leanVM-b own scalars: - prove side: zerocheck (round1_ab, round1_c, per-round pairs, final a/b), lincheck (round pairs, z_partial) and ring-switch (s_hat_v per claim) call ps.add_scalar at the exact points they previously observed, so transmit and bind are one act and the stream order IS the protocol order; - verify side: vs.next_scalar at the mirror points (bound at read), the functions reassemble the old structs from their reads and return them as passive records for summaries and the recursion harness (ReductionReplay, StackedOpeningSummary.ring_switches); - final_c_eval is no longer transported at all: the verifier interpolates it from the already-bound round1_c (it was checked against exactly that), so the field was redundant transport; - the composite opening structs collapse: OpeningProof / BatchOpeningProof / BatchOpeningProofLigerito / Blake3StackProof lose their streamed parts and reduce to the hash-bearing artifact (BaseFoldProof or LigeritoProof); standalone R1csProof(Ligerito) carries only pcs_open; - write_stack_proof / read_stack_proof / hint_bytes / next_hint_bytes and the bincode dependency of the flock path are deleted; cpu prove just hint_opening()s the one Ligerito, cpu verify next_opening()s it. The sponge sequence is unchanged (absorbs happen at the same protocol points, reads bind exactly where observes did), and the flock words land in the stream region past everything the guest cursor walks. Proof: the guest AND the recursion harness are byte-for-byte untouched, and recursion_2to1 passes at the same 2,536,980 cycles. Vendored tamper tests now flip stream words (the honest way to tamper a streamed proof). Suites: leanVM 60 + 2 ignored, flock-core 231, flock-prover 19, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Follow-through on the stream fusion: now that flock zerocheck / lincheck / ring-switch words are ordinary stream scalars, the guest does not need them re-hinted. The cursor, parked exactly at the flock region when the flock section begins, just keeps walking: - zc_round1 / zc_msgs / zc_finals / lincheck_msgs / z_partial / s_hat_v are now ALIASES into the stream hint (pointer + advance), not separate hinted buffers. The runtime-length zerocheck round region is skipped with cursor *= nmlv_g^2 (g^(2*n_mlv), already certified). - the harness drops the six duplicated hint entries and their extraction (the finals and lincheck rounds stay as matpart inputs); the guest header hint list shrinks. Sponge ops are unchanged (the obs points just read aliased words), so this is a pure de-duplication: about 1000 hinted witness cells per aggregation gone, +28 cycles of cursor arithmetic (2,536,980 -> 2,537,008). Suite 60 + 2 ignored green, clippy clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
ZerocheckProof, LincheckProof and RingSwitchProof are gone. They had already
stopped being transport (the scalars ride the shared stream); this removes
their last role as verifier-reassembled records:
- prove functions return just their claims (plus captures); the batched
ring-switch returns plain outputs;
- verify functions return just claims/outputs; verify_bind returns the read
s_hat_v slice as a plain Vec;
- ReductionReplay = { ab, c, zc_claim, lc_claim }; ProveCore,
VerifySummary and StackedOpeningSummary lose their record fields;
- the recursion harness takes its matpart inputs from the claims
(zc_claim.a_eval/b_eval) and tail-slices the lincheck rounds and z_partial
from proof.stream (fixed offsets from the end: 2x128 s_hat_v, then 64
z_partial, then the round pairs) — the transport-level tool reads the
transport;
- vendored tests compare streams instead of records (determinism, shape,
precomputed-vs-baseline); the two already-#[ignore]d stale batched-vs-
sequential comparisons die with the fields they compared.
recursion_2to1 unchanged at 2,537,008 cycles (guest untouched). Suites:
leanVM 60 + 2 ignored, flock-core 231 (ignored 13 -> 11), flock-prover 19,
clippy clean.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ver, config machinery)
The repo now contains ONLY what recursion + XMSS aggregation reach (plus the
compiler feature tests and the fibonacci demo). Deleted end to end, with the
call chains verified by an 8-area reachability audit:
- BaseFold PCS (basefold.rs), the jagged PCS (jagged.rs), and the DP24
tensor-algebra module: the stacked Ligerito opening is the ONE live PCS
path. pcs.rs shrinks to commit + the two stacked open/verify fns and their
claim-combination core (which also loses the packed-direct plumbing and
the BaseFold round-0 prime the Ligerito path never read).
- The standalone flock prover/verifier: prover.rs (whole file),
Blake3Setup::{prove, prove_fast*, prove_ligerito, verify*}, the batch-major
witness layout, the Blake3LincheckCircuit walker, R1csProof/R1csClaim/
bind_statement, verifier.rs (reduced to the VerifyError enum), the
ring-switch single-claim prove/dense verify/succinct verify wrappers,
lincheck/zerocheck non-capture prove wrappers, SparseMatrixCircuit and the
sparse row-fold, the deg4 zerocheck/NTT variants, the parallel-NTT module,
and the dead r1cs packed-apply family + statement_digest (superseded by
family_digest).
- Ligerito dead surface: the eval-point and l0 provers, the dense verifier,
the whole TOML/embedded-config machinery with vendor configs/ (42 files),
the proof-size estimator, and their test suites. derive_profile is the one
config entry left.
- Dead deps/features: toml, bincode, serde_json, serde (flock-prover),
hash-count; blake3 becomes a dev-dep of flock-prover.
- Tests: blake3_bench.rs and rs_eq_linearized_probe.rs deleted; vendored
tests of dead paths deleted; tests of LIVE paths kept and ported off dead
scaffolding (CscCircuit instead of the sparse walker, succinct Ligerito
verifier instead of dense, naive scalar oracles instead of deleted mfr
kernels, the const-wire-pin negative test rewritten against the kept
zerocheck+lincheck entry points).
- Repo files: tracked __pycache__ artifact removed (+ .gitignore), empty
examples/ dir, misc/recursion-generic-plan.md, stale root TeX leftovers.
- leanvm src: fold_low, single-tree GKR (prove/verify_product, LeafClaim,
pad_to_pow2), Stacked::pcs_point, SlotClaim::value, Program::digest()
accessor + Display impl, parse_file, and two garbled doc comments fixed.
Everything validates: workspace 58 tests + 2 ignored recursion suites green,
flock-core 161, flock-prover 9, clippy clean, recursion_2to1 at the same
2,537,008 guest cycles.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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_aggregation. Every flock-derived file keeps its credit header (blake3.rs /
blake3_witness.rs gained theirs); generic helpers extracted downward kept the
attribution note (multilinear::build_eq / lagrange_weights_naive).
Boundary moves that make the layering acyclic: PaddingSpec -> pcs::pack,
build_eq + lagrange_weights_naive -> primitives::multilinear,
bit_transpose_64bytes -> primitives::bits, RHint machinery -> lean_vm::cpu,
the pcs<->lincheck seam test -> flock. Clippy is warning-clean workspace-wide
(with upstream-style kernel allows in [workspace.lints]).
Suite: 235 tests green + 3 ignored (2 heavyweight recursion suites — both
pass when run — plus 1 pre-existing); CLI smoke-tested on all three
subcommands (recursion 2->1 verifies end to end).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
…ocess 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>
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>
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.