Repository navigation
leanvm-cli: claim-set trees in aggregate --signers and the tracked benchmarks - #617
Merged
kevaundray merged 40 commits intoOct 14, 2026
Merged
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.
The leanXMSS and leanSPHINCS guests now read their signatures in groups and commit one value, the digest of the signer set they verified (leanvm_guest::signers), instead of committing every claim. So a leaf's output is BLAKE2s of its signer set's digest, which a signer-set tree can rebuild from the set's claims. - leanXMSS advice: the number of groups, then per group its leaf index (below 2^32), message and count, then that many (key, signature) entries read in place. Each signature is verified at its group's leaf index and message; the guest writes one XMSS group per advice group and each key as its Merkle root then public parameter. - leanSPHINCS advice: the number of groups, then per group its message and count, then the entries. A set writes SPHINCS claims as runs of one message, so a group opens a run only if it has a signature and its message differs from the open run's: the output is the set's digest whatever the advice's grouping. - Hosts: batch(n) is one group (one leaf index and message for leanXMSS, one message for leanSPHINCS), and batch_groups(&[Group]) takes several, with overlapping signer ranges, so a key can sign in several groups. Both return a Batch: the Run (advice and expected output) and the leanvm::SignerSet the guest proves, in the advice's order and not canonical. A leanXMSS key signs at one leaf index, so a signer at two leaf indices is two keys; at one leaf index it signs several messages under one key. - Tests: the expected output, a native stream over the advice and the guest on the interpreter agree for one group of every count up to 5 (3 for leanSPHINCS), several groups, several messages at one leaf index and one key in several groups; a changed signature, group message or out-of-range leaf index traps. - Rebuilt both ELFs; the CLI's workloads take batch(n).run.
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.
… benchmarks `cargo leanvm aggregate --signers` (leanxmss, leansphincs) proves distinct leaves, each publishing its signer set (`--n` signatures split over `--groups` messages, `--overlap` percent of each group's signers the previous leaf's), then the tree bottom-up with aggregate_leaves / aggregate (`--arity0`, nodes of up to `--arity`, the last of a level fewer), the root declaring its union or half of it (`--declare`), within `--max-claims` / `--max-groups` (Capacity::MAIN by default), and verifies the root with verify_signers. It reports the union, each used circuit's rows and committed words, each kind's proving time, the root's verifying time and the proving's heap peak. Workload carries the signer set a signature guest publishes. Tracked: counted aggregate-signers-leanxmss-400-2to1 (capacity 1601/16) and -4to1 (6401/16), every node arity reported; proven aggregate-signers-leanxmss-100-2to1-16thread (401/16) and -4to1-16thread (1601/16). Measured (32-vCPU x86-64, 16-thread pool): - Positional counted tree rows unchanged vs kw/signer-set-guests (diff of `bench --cycles-only --markdown` only adds the signer rows). - Counted signer trees, rows / committed: 400-2to1 first 216,604 / 2^22.63, node 199,753 / 2^22.63; 400-4to1 first 570,214, node2 421,725, node3 488,230, node(4) 554,742, all 2^24.51. - Capacity::MAIN, arity_0 4, arity 16, leanxmss-8 leaves: Tree::new 20.5 to 23.4 s (heap peak 8.46 GiB, RSS 12.6 GiB); every circuit committed 2^26.63; first EMUL 1,335,268, node2 EMUL 1,246,742, node16 EMUL 1,770,629; warm proving first 1.18 to 1.42 s, node16 1.96 to 2.37 s, node2 1.30 to 1.35 s; proving heap peak 5.54 / 5.83 / 5.54 GiB; process max RSS 15.3 GiB. - Proven, --repeat 3, ABBA against the positional tree: 2to1 first 0.083 vs 0.080/0.083 s, node 0.086/0.087 vs 0.083/0.089 s, heap 0.312 GiB both; 4to1 first 0.156/0.159 vs 0.142/0.152 s, node 0.168/0.180 vs 0.154/0.163 s, heap 0.62 GiB both.
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.
…ner-set-cli # Conflicts: # bins/leanvm/src/tracked.rs # bins/leanvm/src/workload.rs # programs/leansphincs/guest/src/main.rs # programs/leansphincs/host/src/lib.rs # programs/leansphincs/leansphincs.elf # programs/leanxmss/guest/src/main.rs # programs/leanxmss/host/src/lib.rs # programs/leanxmss/leanxmss.elf
Each signature guest's host signer set reaches the tree as a ClaimSet through its label_groups (labels of six words, members of four); the tree proves with ClaimLeaf, aggregate_leaves and aggregate and checks the root with verify_claims. The capacity stays a parameter (--max-claims, --max-groups); the flags keep their names. Counted recursion rows unchanged by the port: aggregate-signers-leanxmss-400-2to1 first 216,604, node 199,753 (2^22.63); 400-4to1 first 570,214, node2 421,725, node3 488,230, node 554,742 (2^24.51). The positional trees' rows are unchanged too; leanxmss-400 and leansphincs-104 cycles move with the restructured guests (768,711 to 768,713, 973,689 to 969,940).
Exact counts
|
Benchmarks: base against this PR, on one runner56179da merged into its base, against the base 37c1525: 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
FibonacciProver stages
Flock
Other benchmarks
Prover stages
leanSPHINCSProver stages
leanXMSS
Prover stages
Every resultBLAKE2s
Prover stages
Fibonacci
Prover stages
Field and transpose kernels
Flock
Other benchmarks
Prover stages
PCS
leanSPHINCS
Prover stages
leanXMSS
Prover stages
|
…ner-set-cli # Conflicts: # bins/leanvm/src/tracked.rs
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 14, 2026
…er-20261010 The circuits dump names each position by its NodeCircuit, so the tracked signer-set trees' circuits are dumped under their benchmark names; all twenty-three dumps pass checkrec with the existing Lean model.
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 14, 2026
…lean-rec-soundness The circuits dump writes each signer-set tree's node circuit of every arity (-node2, -node3, -node for the largest) instead of one -node file per position, and checkdesign and checkedges read the aggregate-signers-* dumps as one-tier claim-set trees of capacity 1601 and 6401 in 16 groups, so all 23 dumps are checked.
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 14, 2026
…eanEthereum#617) into kw/clean-rec-soundness
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.
Fifth of the signer-set aggregation stack, after #614 (claim-set trees), #618 (height tiers), #626 and #627: the CLI proves claim-set trees over leanXMSS and leanSPHINCS leaves, and the tracked benchmarks count and prove them. A tree is its leaf program's, so each tree is of one scheme.
cargo leanvm aggregate --signers(leanxmss or leansphincs; fibonacci is refused) proves--leavesdistinct runs, each publishing its signer set, then the tree bottom-up withTree::aggregate_leavesandTree::aggregate, and verifies the root by its set alone (Tree::verify_claims). The capacity is a parameter,--max-claimsand--max-groups, required with no default, and the tree has one tier (ClaimShape::new): it sets every circuit's heights, and main's capacity is far heavier than these trees need (see #614). Each leaf splits its--nsignatures across--groups, groupjsigning messagej, and--overlappercent of each group's signers are the previous leaf's, so the union is smaller than the sum. A level's last node takes fewer children (a lone child is taken by the node of two, its other place absent);--declare halfhas the root declare half its union. It reports the union and the sum, each used circuit's rows and committed words, per-circuit proving times and proof sizes,Tree::new, the root's verification, the heap peak and peak RSS. The positionalaggregateis unchanged.The claims are the programs':
Workloadcarries aleanvm::aggregate::ClaimSetbuilt fromleanxmss_host::SignerSet::label_groups()orleansphincs_host::SignerSet::label_groups(), and the CLI never looks inside the union or assumes a capacity.Tracked: counted
aggregate-signers-leanxmss-400-2to1(capacity 1,601 claims in 16 groups) and-4to1(6,401 in 16), every node arity reported (-nodethe largest,-node<k>the smaller); provenaggregate-signers-leanxmss-100-2to1-16thread(401 in 16) and-4to1-16thread(1,601 in 16), over copies of one leaf proof, so every node's children overlap entirely; both proven cases joinbench.yml's matrix. Positional names and numbers are unchanged.Counts (
bench --cycles-onlyat riscv-exploration dfb7570, identical at 37c1525, one tier,ClaimShape::new(capacity)): only these rows are added.The positional trees are 2^22.51 (2to1) and 2^23.51 (4to1).
Proven (before #618, #626 and #627, which change the union by a few rows and no proven height; Ryzen 9 7950X3D, 16-thread pool,
target-cpu=native, one binary, positional and signer-set cases alternating ABBA, 8 runs each, medians):The positional cases against riscv-exploration with #614 (
scripts/ab.sh, 5 alternating rounds): proving time within -0.2% to +1.6%, every interval spanning zero; proof sizes and allocations identical; heap peaks within 0.02%.Tests: the overlap arithmetic; an end-to-end tree for leanxmss and leansphincs (6 leaves at arity 2, so a node takes a lone child, its other place absent, the root declaring half), which also checks each host's
label_groups()digest is its guest's output. Release smoke at dfb7570:aggregate --signersover 6 leaves of leanxmss and of leansphincs (3 groups, 50% overlap, declare half), at arity 4 and at arity 2 (a lone child), proves and verifies.Merge of riscv-exploration 37c1525 (#631, #619 to #624, #633, #634): the CLI follows the new
benchAPI (pretty_integerandpretty_f64frombench, closures toPlantake no pass argument,Plansuppresses tracing itself,Plan::defaultandwithout_cooldownreplace the hand-built plans). #634 removedTree::node_stats, which nothing in the library read; this PR restores it besideTree::stats, since the tracked counts report every node arity of a signer-set tree through it. No protocol, session or wire format changes, so no version moves.Zero-knowledge leaves work with signer sets: with
--zk,aggregate --signersproves zero-knowledge leaves and shapes the tree's leaf as a zero-knowledge one (LeafShape::zero_knowledge), as plainaggregatedoes; the tree's own proofs stay plain. The tracked benchmarks remain plain proofs and still refuse--zk.Checks at 56179da: formatting, haswell Clippy on Rust 1.97 and 1.99, native Clippy on 1.99, AVX-512 and ARM64 Clippy, system allocator CLI Clippy, rustdoc and the complete local release workspace suite pass. Release smoke:
aggregate --signersover 6 leaves of leanxmss and of leansphincs (3 groups, 50% overlap, declare half) at arity 2 and 4, and over 6 zero-knowledge leanxmss leaves at arity 2, proves and verifies the root by its set.bench --cycles-only --markdownprints the same counts as at dfb7570.