Repository navigation
tree: a lone child of any size, absent places at every claim-set node - #627
Merged
kevaundray merged 36 commits intoOct 12, 2026
Merged
kevaundray merged 36 commits into
kevaundray merged 36 commits into
Conversation
A signer set is the claims an aggregate publishes: XMSS groups of keys that signed one message at one leaf index, and SPHINCS (key, message) claims. Its digest is a chain of BLAKE2s compressions, one per item (a group header, a block of two keys, the end), each item's counter saying what it is, so a parse of the blocks is fixed by their counters and a recursion circuit can read a set of any shape in fixed rows. - leanvm_guest::signers: SignerStream, the digest a guest writes one group and one key at a time. - leanvm::SignerSet: the claims, their written form and digest (cross-checked against the guest's stream), the canonical form a root must publish (check, with main's capacity: fewer than 2^16 claims, at most 1,024 groups), from_claims, and bytes that refuse trailing data.
A node of a signer-set tree reads its children's sets from their digests, declares a set of their claims, and proves every declared claim is a selected child claim: - Each side is a pool of items, one compression of a set's written form each; an item's kind is hinted bits that give its counter word, so a run's chain equals its set's digest only if it is read as that set. - The children share one pool, a run each starting at a chunk boundary; a one-hot over the children, moved on at each chunk that begins a run, says which digest each run's end must hold. So the pools are fixed by the digests before any challenge. - A challenge point drawn from a transcript of the digests and the packed selection bits checks the product of the selected child claims' factors against the declared claims': a claim's fingerprint carries its scheme, leaf index and message, so a key backs only a claim of its own group. Builder: block (a compression whose counter and finalization words are a wire), d_to_halves (a digest's halves in one cast row), Compression::with_flags.
A tree's shape now chooses its semantics. A tree of outputs is as before: its root states its leaves' outputs in order. A signer-set tree (TreeShape::signers, a capacity) aggregates signer sets as leanVM main does: - A leaf publishes a signer set: its output is the hash of its set's digest. - Each tree proof declares a set, by default the union of its children's sets, or any covered part of it (Tree::aggregate_leaves, Tree::aggregate). Its rows run the union gadget, so every declared claim is one of its children's; duplicates and dropped claims are simply unselected. - Anyone combines any proofs of the tree: there is a node circuit for every arity from two to the tree's largest, all of one height, and one child is taken twice. Aggregate pairs a proof with its set, for handing between provers. - The root's verifier takes the set alone (Tree::verify_signers): canonical, within the capacity, stated by the root. A child's kind is now its circuit's index: with more than two circuits the rows hold it to an index and split it, its bits selecting the circuit's block of the fixed polynomial, whose top now has as many variables as the index has bits. A dense claim's top is a list of coordinates. Positional and signer-set operations refuse the other semantics, and both the semantics and the capacity are in the session. Versions: LVMT 14 to 15, leanvm-tree-11 to leanvm-tree-12. Docs: e-recursion.tex, Signer-set trees, and the circuit identity for several kinds.
The tree's union gadget no longer knows what a claim means. A claim set is groups of claims sharing a 6-word label, each with 4-word members; it is written and hashed as before (a header a group, two members a block, the end, each block's counter saying what it is), and the gadget's fingerprint tuple is (1, label, member). What labels and members mean is the programs': rec::tree::multiset defines the format, its digest and its canonical form (labels strictly increasing, members strictly increasing, groups non-empty). - rec/tree/signers.rs becomes rec/tree/union.rs, over ClaimSet; its session tag is leanvm-claim-union-1. - rec/tree/multiset.rs: ClaimSet, ClaimGroup, Claim, Capacity, ClaimSetError, the written form and digest, bytes. - A test hands the rows an uncovered claim, which the product refuses.
Merges the generic union gadget and renames the tree's API to claim sets: TreeShape::claims, ClaimLeaf, Aggregate { proof, claims }, Tree::verify_claims, and the errors with them. The core keeps no signer types: a leaf program says what its claims mean and hands the tree a ClaimSet. The recursion annex describes the claim-set tree with labels and members.
leanEthereum#612 was merged at its head from before the restructure, so riscv-exploration re-added leanvm::SignerSet and leanvm_guest::signers, its guests wrote the old format, and the hosts imported two SignerSets and failed to compile (E0252). This brings it to the restructured tree: the programs own their signer sets (leanxmss::signers and leansphincs::signers in the guest libraries, SignerSet in each host), the guests' main writes the digest through its library's Stream, the hosts' Batch holds the program's SignerSet, and the SDK keeps only blake2s_compress, the portable counterpart of precompile::blake2s_compress. leanvm::SignerSet and leanvm_guest::signers are removed again, and both ELFs are rebuilt.
The programs own their signer sets (leanEthereum#615); the core keeps only the scheme-agnostic claim sets.
… a wrap of large proofs
…nd the tiers in the recursion chapter
…fake large circuit, small tiers; docs of the large node's children
…sion tag's parts in the protocol chapter
…hild too large to take twice is a large proof's wrap
…ne child is taken once whatever its set's size
…claim-set tree's tree-12 heights, layout and tag; LVMT 18, leanvm-tree-15, leanvm-claim-union-3
Benchmarks: base against this PR, on one runner35aa022 merged into its base, against the base b094d00: each benchmark run in turns on one runner, base and PR 5 times each. A size is shown when it changed; a time or a peak memory when it moved the same way in every round and its median by at least 1% (the change is the median ratio, with the rounds' range). Threads shows the named configuration; BLAKE2sProver stages
Flock
leanSPHINCS
Prover stages
leanXMSS
Prover stages
Every resultBLAKE2s
Prover stages
Fibonacci
Prover stages
Field and transpose kernels
Flock
PCS
leanSPHINCS
Prover stages
leanXMSS
Prover stages
|
This was referenced Oct 12, 2026
This was referenced Oct 12, 2026
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 12, 2026
…bsent places, leanEthereum#609 stacked-opening lint) Tree session leanvm-tree-16 and LVMT 19, above upstream's. leanEthereum#627's pinned-heights tests take this branch's PerRecTable heights (STEP and LINK absent) and pin the session tags as this branch derives them (they name the leaf family).
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 12, 2026
…clean-circuits-adder-20261010
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 12, 2026
…claim-trees-per-program
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 12, 2026
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.
Follow-up to #618 from the reviews of #614 and #618.
A lone child of any size within the capacity.
Tree::aggregatetook a lone child twice by the node of two, whose children's pool holds about one capacity's worth of items. So a set of more than about half the capacity (atCapacity::MAIN, one group of 40,000 claims) could not be narrowed or republished: the fill failed and surfaced asTreeError::Capacity. The fixtures missed it because their capacities fit in one chunk. Now every claim-set node takes from one child to its arity, as #618's large node already did: the places past its children verify a repeat of the first child and are absent, their sets read as the empty set's, so a lone child's set needs room in the pool once. The first level still verifies all its leaves.Absent bits bound before the challenge. Each absent bit is held Boolean by a
SPLITrow, and its packed words now enter the union's transcript instance beside the digests read, so every wire that decides which pool slots are read is fixed before(X, A)is drawn (the rule #626 applies to the runs' begin bits). Reading a child as empty only removes claims a declared claim could be selected from, so an absent place backs nothing.Tests.
leanvm-tree-12(tree: claim-set trees that anyone combines #614): a tree of outputs keeps its heights, statement layout and session tag but for the version; a one-tier claim-set tree keeps its heights, layout and tag, its nodes adding the absent places.Wideclaim; small tiers past the tree's (TreeError::SmallTier); two-tier trees differing only in the small tier refusing each other's proofs; a lone large proof taken by the large node.Docs. The recursion chapter's absent children now cover every claim-set node, and the protocol chapter lists the recursion tag's parts.
Versions. Merges #626: the absent words join its instance after the digests read and before each pool's begin and selection words. Circuits and the union's instance change:
LVMT18,leanvm-tree-15andleanvm-claim-union-3, above #626's 17, 14 and 2.Upstream's red Test.
a_tiered_first_level_and_union_stay_within_their_capacities(merged with #618) asserted that a lone four-claim child is large because taking it twice overflowed the small tier; here a lone child is taken once, so the test's lone child is the two-tier fixture's large pair, which is past the small tier's capacity and goes to the large node.