This repository was archived by the owner on Sep 12, 2026. It is now read-only.
Recursive aggregation - #9
Merged
Merged
Conversation
Replace the recursion over a phony inner program with the real thing: one guest (`guests/aggregate.py`) serving every node of an aggregation tree, verifying raw XMSS signatures and sub-proofs of itself against one shared (message, epoch), and publishing the sorted deduplicated union of their signer sets. Modelled on leanVM's single-message path. The bytecode is compiled to a fixed point on its own size: the recursion placeholders depend on the inner bytecode's log size, and the inner bytecode is now this one. Its digest needs no fixed point, riding the statement instead of the code, which is also what keeps a whole tree on one bytecode. Coverage carries the security claim. A write-once slot per declared signer is written once by each raw signature and each child key, with the running count as the value so a repeated slot is a conflict, and a final count makes the cover exact. Every declared signer is therefore backed by a real signature or a verified child. Each node exports one deferred claim per fixed polynomial (the stacked bytecode and flock's A0/B0) and batches its children's carried claims with the fresh ones its verifications raise, 2n down to one; only the root's are discharged natively. A carried matrix claim enters as a plain eq weight beside the fresh quirky-eq/lincheck one. Two protocol gaps this uncovered, both invisible to the phony program: - The ring-switch weight assumed the q_flock claim was no longer than the WHIR fold rounds. That is false for any BLAKE2s-dominated inner proof, i.e. every real aggregation. Its top coordinates now continue into the residual challenges, with rs_nover hinted and pinned as the point claims pin theirs. - A child must commit at least 2^MU_MIN for the parent to have an opening arm. Program::min_log_committed grows the SET table through the existing fill blocks until a small run clears the floor. Paying it in fill rows rather than in a padded commitment keeps the committed size a function of the announced table heights, so neither the verifier nor the guest gains a parameter to certify. Also: runtime-bounded range checks in the zkDSL (`assert log x < log n`, same three instructions, one hoisted MUL for the bound cell); Ord on XmssPublicKey; and a signer cache that no longer repeats every 256 signers, which silently shrank any batch above that once the union deduplicates. Adversarially reviewed. The statement digest, the coverage bijection and the batching all hold; the review turned up a non-converging floor search, a terminal-weight cross-check that was dead in release and too weak to catch correlated drift, a parser that accepted more bounds as runtime than it should, and a leaked sponge trace on a failed child. `aggregate_hints_bind` tampers sixteen witness streams and requires each to be rejected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The claim batching was the one part of an aggregation node that ran single-threaded, and it cost more than half as much as proving. 462 ms to 49 ms, and a 2->1 step over 900-signature leaves from 1.37 s to 0.96 s. The flock reduction contracted the R1CS matrices once per claim, walking tens of millions of nonzeros each time. Now one pass serves every claim, parallel over rows, with the claim weights interleaved so a nonzero costs one fetch of n adjacent weights rather than n fetches into n tables. The row contraction is a scatter, so workers accumulate private column vectors and the dispatcher adds them. The matrices are fixed, so they are cached in CSR with 16-bit column indices. The bytecode reduction exploited nothing about its polynomial. Nine encoding columns sit inside sixteen stacking slots, so nearly half the table is structurally zero, and folding LSB-first pairs entries within a slot, which keeps that window aligned all the way down: the row rounds now run on the populated part alone and the slot rounds take their weights from a closed form. Round zero runs against the K-valued table itself, so the bytecode never materializes as 2^23 extension elements. The batching weights are built as an outer product of two half-length eq tables instead of one full table per claim summed together. What is left is at the instruction-throughput floor for visiting every nonzero: a cached CSR with quarter-size indices changed nothing, and four times the claims costs 1.47x the time, so neither memory traffic nor per-claim work binds it. Going further means visiting fewer nonzeros, which the rank-1 structure of every claim weight would allow. Safe to tune aggressively: the guest verifies both sumchecks in circuit, so an error here fails a test rather than passing quietly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Proving cost is the sum of each table padded to a power of two, so cycles only matter when they cross one. Two boundaries were within reach of the aggregation loops in main. DEREF sits at 2^18.25 and the whole signer path holds 54k of them, so 2^18 is unreachable; but memory sat at 2^20.04 and needed only 42k cells to drop log_mem from 21 to 20, which halves the committed memory. That is the one taken. Memory is dominated by loop frames rather than by buffers: every mul_range iteration allocates one, and a frame costs far more cells than the body it holds. So both key loops, the node's own set digest and each child's reconstruction, now take two keys per iteration. The chain is untouched: still one compression per key, two of them per frame. pubkeys_hash needs no change, the statement is unchanged, and an aggregate built before this still verifies. The only new witness is a parity, hinted as (half, odd) and pinned by half*half*odd == n_keys with odd range-checked below 2, whose unique solution is half = n/2 and odd = n % 2; the odd key out is absorbed in a one-shot branch, both arms writing the digest cells for the join to read. 2->1 over 900-signature leaves: prove 778 ms to 549 ms, the whole step 942 ms to 731 ms, committed 2^25.05 to 2^24.86, proof 289 to 279 KiB. The margin is thin. mem_used is 1,043k against a 1,048,576 ceiling, about thirty more signers, and past that log_mem returns to 21 and the win goes with it. Widening it means the per-signer buffers (all_pubkeys, pk_chain, cover and sub_chain are seven cells a signer between them), not the frames. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Verification was 50 ms, nearly all of it one thing: `mle_eval` over the 2^23-entry stacked bytecode is a fully sequential fold, `fold_low_k` then `fold_ladder`, about 12.6M dependent operations. It is paid twice, once by `cpu::verify` for the proof's own bytecode claim and once by the deferred recompute at a different point. `mle_eval_par` fans both folds out; `mle_eval` stays scalar because it is also called from inside a dispatch (`leaf.rs`, the per-column claim walk), where nesting deadlocks. Two entry points rather than a runtime "am I in a task" flag: the choice is a property of the call site, and the pool's nesting assert stays a live canary instead of being consulted. Three sites are outermost and large enough to want it: `bytecode_claim`, reached from both `prove_balance` and `verify_balance` after their own dispatches have returned; `decompose_formula`'s public-column arm, the nine encoding columns; and `DeferredClaim::recompute`. The ladder folds out of place while rounds are big, since folding in place reads `cur[2i]` where another task writes `cur[i]`. Node verification 50 ms to 17 ms, leaf 37 ms to 14 ms, and proving picks up a little on the way. Worth recording what this was not: the flock matrix walk, the obvious suspect at 89M nonzeros between A0 and B0, is 164 us. Also adapts the recursion section of the doc, which still described one claim per sub-proof and called carrying claims forward unexposed, and refreshes the README benchmarks. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The rename of recursion.rs to aggregation.rs defeated git's rename detection, so main's three edits are ported by hand: the lincheck rounds carry two coefficients rather than three evaluations, `raw.merkle_openings` becomes `raw.merkle`, and the LAG4_INV placeholders go, the table sumcheck no longer interpolating a cubic. The guest merged on its own, the rename to aggregate.py being detected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The tweak table and the Merkle bits were absorbed two cells a block, half of every block going to re-inject the chaining state. Both loops are unrolled, so the byte counter is a compile-time immediate and a plain BLAKE2s is expressible here as it was for the statement: the label takes the leading block and the two tables follow, four cells at a time. Each block is hashed out of the frame it was hinted into. Routing the cells through the heap first, which reads more naturally, costs 370 DEREF and 270 cells: a blake2s operand is addressed as `fp · g^immediate`, so a heap-resident one is loaded back a DEREF per cell. The hint entries widen from two cells to four to match, which is what pins both tables to whole blocks, asserted. Measured on a 50-signature leaf: BLAKE2S 2^12.864 to 2^12.846, cycles 86,888 to 86,800, memory unchanged. With this the signer-set chain and the Fiat-Shamir sponge are the only long hashes left on a re-injected state, and neither can stream: their lengths are runtime, and the counter is not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
TomWambsgans
force-pushed
the
recursive-aggregation
branch
from
August 13, 2026 15:49
5105d6e to
34559ce
Compare
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 subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.