Repository navigation
leanXMSS and leanSPHINCS verifier circuits on the recursion machine, proved in Clean - #610
Draft
kevaundray wants to merge 39 commits into
Draft
kevaundray wants to merge 39 commits into
kevaundray wants to merge 39 commits into
Conversation
…hereum#595, vendor the XMSS specification, author the leanXMSS verifier circuit in Lean
…-rec to the CLI, and check the Rust circuit is the Lean one with checkxmss
… on the host's known answers, and author its recursion-machine circuit in Lean
…tures verify over words
…erification with Option.elim so the kernel never reduces a symbolic hash
… words' bytes, with decoding onto
…uilder's methods and an honest assignment for every verifying batch
…; aggregate signature-circuit proofs in trees with leaf families, mixed trees and topology-checked roots
…udit this branch's theorems, build and check every module in CI
Benchmarks: base against this PR, on one runnerdc7bb92 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; FibonacciProver stages
PCS
leanSPHINCSProver stages
leanXMSS
Prover stages
Every resultBLAKE2s
Prover stages
Fibonacci
Prover stages
Field and transpose kernels
Flock
PCS
leanSPHINCS
Prover stages
leanXMSS
Prover stages
|
…y on the words' bytes, with decoding onto
…_iff) and audit it
… pool of fourteen entries routed to the chains by a five-stage EXK mux network, the entry's tweak word checked by step 1; re-prove soundness and completeness
Rec.Tables: STEP and LINK slot forms and identities, their pushed and pulled tuples (step_spec, link_tuples, stepPush_next). Rec.Builder: the tables, chainStep and link. Rec.Contracts: Sat holds STEP and LINK rows to their identities, Balanced is the dynamic multiset balance, Accepts both; chainStep_good, link_good, Balanced.count_key and Balanced.unique. GenerateRec emits the new forms into clean.rs; checkrec and checkxmss parse chain_step and link and finish eight tables.
…n machine STEP rows pull a chain step's input at its position's key and push its output at the next position's; LINK rows push a chain's tip at its digit's position and pull its end at position 7. Each table has an activity fixed column (one on the circuit's rows), and bit 63 keeps dynamic keys apart from slot keys. The forms are GenerateRec's (clean.rs), with the new scaled product coordinate leaf::Coord::ScaledProd. Builder::chain_step and Builder::link build the rows, and finish records an unbalanced multiset. Table order is now EMUL, EXK, HASH, SPLIT, CAST, STEP, LINK, PUB, so every circuit's PUB slot keys, fixed columns, airs and bus blocks change: existing circuits' proofs and dumps are not byte-identical to before.
…the wire classes of the circuit already held
…eps the digits need; re-prove acceptance over the dynamic balance
…s, leanXMSS chains walked on the bus (exactly the steps the digits need), acceptance re-proved over the dynamic balance
… at bit 32, so leanXMSS and leanSPHINCS chains share the table; leanXMSS passes tweak0(1, 0) and its chain proofs are stated over any base and tag
…Ethereum#608 claim width check) into the leanXMSS/leanSPHINCS circuits Tree, signature circuits and in-circuit verifier move to SessionId sessions and recorded openings. A first-level node over recursion-circuit leaves binds each leaf's statement by the digest its transcript would squeeze right after the instance (instance_digest; rows: Transcript::digest_so_far), in place of the statement hash the old transcript was seeded with. The Lean transcript model follows in the next commit.
…e session seed, words absorbed and squeezed, the digest, the new proof of work; trace k_to_d and model it The duplex core (counters, hold-back, output blocks) is unchanged by leanEthereum#607. What changed and is modelled: the seed node is init(session) (the old seed with a zero statement half), the instance is the first message, roots are four words, COMMIT/POW_BASE/NONCE are gone (the terminal binding is four squeezed words), and proof of work hashes a squeezed challenge with a u64 nonce and checks the trial word's top bits. Builder::k_to_d, now used by the transcript, is traced, with a Lean model and contract, so checkrec replays tree circuits.
… dense values are the tree's polynomials only A table with no rows, other than HASH and PUB, is absent: Table::height_log gives it no height (rec::table::Heights), and RecLayout keeps the present owned tables, which alone have committed columns (witness::Source::Absent otherwise), bus blocks (indexed among the present tables), summands, fixed columns and claims. The verifier reads the heights off the circuit or the tree's shape (RecShape), never the proof, so a proof with rows in a table the verifier expects absent is a proof of another shape and is refused (the_heights_fix_the_absent_tables). A circuit's floor keeps a table present; Tree::converge's fixed point starts from no table and keeps one absent only while every kind's circuit lacks it. The tree statement's DenseValues section has one word per dense polynomial the tree has (StatementLayout::new takes Design::present). The session tag encodes an absent height as 2^64 - 1 and moves to leanvm-tree-12. CircuitStats reports an absent table's height as none. cargo leanvm bench --cycles-only now equals riscv-exploration d3c7f9d on every tracked count, the aggregate-leanxmss cases included: 2to1-first rows 138530 -> 138529, proven-rows 231426 -> 231424, committed 5981211 -> 5981184; 2to1-node rows 120668 -> 119413; 4to1-first rows 275682 -> 275681, proven-rows 461826 -> 461824, committed 11962395 -> 11962368; 4to1-node rows 252644 -> 250195.
… its circuit
XmssBatch and SphincsBatch build their circuit once, one part per signature
(Builder::parts), and record each fold of a constant or an EMUL/EXK row. A
proof replays the parts for their values alone (Replay::values): the folds are
read back, so wires are numbered as the build numbered them, with no rows,
wire classes, kinds or dedup maps, and the parts run in parallel, each into its
own stretch of the values, hash rows and statement. A part reads of earlier
parts only the constants and rows over them it folds into, whose values are the
circuit's own; the build checks it for rows and the replay for reads. Each part
checks its own step and link rows; only when some part's dynamic tuples do not
balance are the circuit's counted together, so the failures are the build's,
in its order.
The dynamic check evaluates each table's tuple forms once rather than per row
(Table::dynamic_tuples replaces row_dynamic). Assignment shares its slot wires
with the replay (Arc). Builder::finish_values is gone.
Calls, circuits and dumps are unchanged ('cargo leanvm circuits' output is
byte-identical). 'Build circuit' at 16 threads: leanxmss-rec n=400 69.5 ms ->
2.8 ms, leansphincs-rec n=104 58.2 ms -> 3.1 ms (single traced runs).
# Conflicts: # crates/leanvm_core/src/rec/circuit/mod.rs
…um#615 signer sets, leanEthereum#613 claim sets and union in rows) into the leanXMSS/leanSPHINCS circuits The host crates keep exporting the signing constants and one-message signers for the recursion circuits beside the new signer-set batches; leaf_block stays traced and is now d_const of its counter word then the new Builder::block's row.
… merge, which picked them up unfinished; the next commit adds them whole
…model them: Model.hashBlock, Model.dToHalves, their contracts, leafBlock_eq leaf_block is d_const of its counter word then block's row (Model.leafBlock_eq, by rfl); checkrec parses block and d_to_halves. No tree or signature dump calls them yet; the claim-set trees of leanEthereum#614 will.
This was referenced Oct 11, 2026
…d leanXMSS/leanSPHINCS trees A tree is built from one leaf family (`Tree::new(Leaves, TreeShape)`): RISC-V proofs of one program, or proofs of one recursion circuit. The session tag names that family as before (program digest and leaf shape, or the leaf circuit's session, statement length, heights and rate), so a tree proof of another tree fails its recursion proof's verification as a child or root; nothing checks the scheme otherwise. Deleted: the multi-family selector (`Kind::First(i)`, kind codes past two, kind bits with indicator checks and per-kind masks), several leaf circuits stacked in `W_leaf` by slot, `TreeError::Families` and `ForeignChild`, `Tree::kinds`, the unused `Builder::sum`, `aggregate --mixed/--mixed-n` and the mixed-tree test. The kind is one bit again (`Kind::First`, `Kind::Node`, `Kind::ALL`), `DenseTerm::top` one coordinate, `W_leaf` the leaf circuit's stack. DOMAIN is leanvm-tree-13. Rows and committed words of every tree circuit are unchanged (cycles-only counts identical to 5c821f8); only the session constant and no-op builder calls in the node's trace differ. New test `a_tree_refuses_another_familys_tree_proofs`: leanXMSS and leanSPHINCS trees (same heights and statement layout) refuse each other's first-level nodes and nodes as children and roots with the error the proof gets under the other session alone (bus GKR layer mismatch); RISC-V and leanXMSS trees refuse each other's at the statement length.
…eanEthereum#626: claim-set trees, tiers, places) Upstream's places, tiers, claim-set and union design, with this branch's one leaf family per tree: - Design has `family: Family` (RISC-V runs of one program, or proofs of one leaf circuit) beside upstream's places and tiers. Circuit leaves are for trees of outputs only: a claim-set tree over them is `TreeError::CircuitClaims`. - DensePoly is [Bytecode, Image, Leaf, Fixed, Wide]; a statement holds values for the polynomials the tree has only. A first-level node carries claims on the polynomials its leaves fix; every other proof on all of them. - The statement digest's level enum is `Items` (upstream's design has its own `Level`). - `Tree::new(Leaves, TreeShape { arity_0, arity, rate, claims })`; `Leaf`, `Subtree` verification and absent tables (`Heights`) as before, with upstream's `known()`, positions and `TreeError::Circuit`. - `FixedLayout::polynomial` stacks a tier's circuits by kind index over the absent-aware layout. - LVMT 18, tree DOMAIN leanvm-tree-15.
…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).
…ignatures as one group A leanXMSS or leanSPHINCS batch's proof publishes one claim per signature (label: the scheme word, the epoch where the scheme has one, the message; member: the key's root and public parameter), as the scheme's guest writes its signer set. The first-level node holds every claim's label to the first's, chains the set's written form over the leaf statement's wires and hands the union that digest. The claim layout joins the session of claim-set trees. XmssBatch::claim_set and SphincsBatch::claim_set give the set; TreeError::CircuitClaims is gone. cargo leanvm aggregate --capacity N [--groups G] proves claim-set trees over guest or circuit leaves.
…before the bus); leanvm-tree-17, LVMT 20
…now fails at flock's zerocheck, its first stage
… its leaf program's): its tests build trees from Leaves::Runs
…zero-knowledge leaves, leanEthereum#631, leanEthereum#633, leanEthereum#634): the circuits, trees and CLI on upstream's layout and APIs; circuit leaves are never zero knowledge
This branch has not been deployed
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.
leanXMSS and leanSPHINCS verification as circuits on the recursion machine, authored and proved in Lean over the model of the builder, built call for call by Rust, on the CLI, and aggregatable in trees. Trees are single-scheme: one leaf family per tree, bound by the tree session.
What is proved
Kernel-checked, axioms
propext,Classical.choice,Quot.soundonly (verification/circuits/Audit.leanchecks 245 theorems against that list; CI also runsleancheckerper module).LeanVMCircuits.Xmss.accepted_iff: for every statement, the circuit forn ≤ 2^22signatures (Xmss/Circuit.lean) has an accepting assignment (Accepts:Satand the dynamic bus balance) iff each signature slot states a public key, message and epoch for which some signature makes the Ethereum XMSS specification'sverifytrue. Spec:EthCryptographySpecs/Xmssvendored verbatim at ethereum/cryptography-specs@d1331f02 (scripts/check-xmss-spec.sh), compiling unchanged on Lean 4.33.1.LeanVMCircuits.Sphincs.accepted_iff: the same for leanSPHINCS (n ≤ 2^20) (Sphincs/Circuit.lean) againstLeanSphincs.verify. No external leanSPHINCS specification or pinned reference exists;Spec/LeanSphincsis a Lean transcription of the guest's verifier (programs/leansphincs/guest, each definition citing the lines it transcribes), checked against the host's known answer (public key bytes and the BLAKE2s of the signature) by#guardin Lean's evaluator.sound+completeagainst a word-levelWords.verify, plus a bridge fromWords.verifyto the specification'sverifyon the words' bytes (including that the specification's BLAKE2s is RFC 7693Fchained as the builder chains it, and the 52-byte leanSPHINCS encoding hash), plus onto lemmas for the decoders. Completeness rests on new completeness contracts for the builder's methods (Xmss/CompleteBuilder.lean); soundness on Author leanVM circuits in Clean, prove them, and export them to Rust #595's method contracts.Design: per signature, statement words are exposed
Ewords; every hash is a builderchain(orleafBlockfor the 52-byte encoding); target sums are checked asX^sum = X^195(XMSS) orX^191(SPHINCS) inK; Merkle sides areEarithmetic on index bits. leanXMSS chains are rows of two new recursion-machine tables on the bus: a LINK row per chain pushes(its digit's position, tip)and pulls(position 7, end), and each of the 99 STEP rows per signature (42 x 7 - 195, exactly the steps a valid signature needs) pulls its input at its tweak word's position and pushes its hash at the next position (Xmss/Paths.leanproves the per-key count argument: balance and the fixed step count leave every chain walked once from its digit to 7). leanSPHINCS chains are walked the same way, 103 STEP rows per layer (42 x 7 - 191), the tag(3j + layer)keeping signatures and layers apart (n ≤ 2^20); STEP's base column carries each scheme's tweak bytes.What is trusted
Accepts(Rec/Contracts.lean) is the relation assumed to follow from a recursion proof:SatandBalanced, the multiset of tuples the STEP and LINK rows push equal to the multiset they pull.Sat: wires in one class carry equal values (the copy-cycle bus;Rec/Bus.leanproves this from exact balance), each row's slots carry its table's forms over columns satisfying its identities,HASHrows carry a satisfying assignment of the exported Boolean BLAKE2s artifact,PUBrows carry their constants and statement words. Trusted: the proof system's soundness yieldsAccepts(for the balance, the bus's grand product over the dynamic blocks); Rust'sHASHtable circuit is that artifact (the flock circuits are not generated from Lean on this branch); the Lean SPHINCS transcription is the scheme; the export check covers the dumped sizes.Export and CLI
crates/leanvm_core/src/rec/{xmss,sphincs}.rsmake the Lean circuits' builder calls in the same order (XmssBatch,SphincsBatch: prove, verify, proof bytes).cargo leanvm circuits(--features circuits) dumps them for n = 1, 2, 3, 400 (XMSS) and 1, 2, 3, 104 (SPHINCS);lake exe checkxmsschecks each dump replays through the builder model and equals the Lean-authored circuit (CI:rec-builder-model.yml).cargo leanvm leanxmss-rec --n 400 [--tamper],cargo leanvm leansphincs-rec --n 104 [--tamper].cargo leanvm aggregate --program leanxmss-rec|leansphincs-rec --n N --leaves L --arity0 A0 --arity A [--capacity C [--groups G]]: with--capacity, a claim-set tree (also over theleanxmss/leansphincsguests' leaves).Aggregation: what changed in
rec::treeTrees are single-scheme: a tree has exactly one leaf family (
Leaves::Runsfor RISC-V proofs of one program as before,Leaves::Circuitfor proofs of one signature circuit;XmssBatch/SphincsBatch::leaves()), bound by the tree session: its tag names the family (the program digest and leaf shape, or the leaf circuit's session, statement length, heights and rate), so a tree proof verifies only under a tree of its own family. A signature first-level node verifies each raw proof with the existingRecShapeat the raw circuit's own heights, rate and session, turns its fixed-column hints into claims on a new dense polynomialW_leaf(the leaf circuit's fixed columns), and exposes the usualTreeStatementwith a digest over the leaves' statement digests (instance_digest). The kind stays one bit,W_nodestacks the two kinds' circuits, a carried claim on a polynomial the leaves do not fix is weighed by the child's kind, and the root settles exactly the polynomials its kind carries; a statement holds values only for the polynomials the tree has.Tree::verifytakes the expected topology (Subtree), which makes unbalanced trees verifiable. Versions bumped (LVMT18, tree session tagleanvm-tree-15). Raw signature proofs are not re-proven. The tree's first-level circuits are Rust only (not modeled in Lean).Another family's proof is refused by the session or the statement, not by a scheme check (there is none in the code);
a_tree_refuses_another_familys_tree_proofschecks both cases:RecError::Flock(FlockError::Zerocheck(ZerocheckError::TerminalMismatch))), surfacing asTreeError::Child { index, .. }fromprove_nodeand asTreeError::Rootfromverify, each carrying exactly the error the proof's own circuit gives under the other session.known()refuses the proof before reading it, withTreeError::Circuit(0)from bothprove_nodeandverify.Claim-set trees over circuit leaves
Claim-set trees (#614) take signature-circuit leaves too, one scheme per tree, so signer-set aggregation works with circuit leaves. A leaf publishes one group, one claim per signature, exactly as the scheme's guest writes its signer set: label
[scheme, epoch, m0..m3](leanXMSS, scheme 1) or[2, 0, m0..m3](leanSPHINCS), member[r0, r1, p0, p1](the key's root then public parameter). The leaf circuit and its Lean proofs are unchanged: the claims are read from the statement words the leaf's transcript absorbs.rec/tree/leaf_set.rs:ClaimLayoutsays which statement word (or constant) each label and member word is. In the first-level circuit, each leaf's claims get their label words held equal to the first claim's (eq_k, so a leaf with two epochs or messages has no proof), and the set's written form (header, members two to a block, end) is chained over the statement wires withBuilder::block. That digest is what the union reads in place of a RISC-V leaf's committed one. A tree of outputs keepsinstance_digest, and the claim-set first level skips it.XmssBatch::claim_setandSphincsBatch::claim_setgive a batch's set in claim order (XmssError::Label/SphincsError::Labelif the claims are not of one epoch and message).Tree::aggregate_leavestakesClaimLeaf::new(batch.leaf(..), &set)and refuses withTreeError::LeafClaimsa set the statement does not state.TreeError::CircuitClaimsis gone.leanxmss_host::batch(4).setandleansphincs_host::batch(2).set); a 4-leaf leanXMSS claim-set tree states the canonical guest set of the four signers; a leaf given another leaf's set is refused; claims of two messages make no set and no satisfied rows (leaf_setunit tests over 0 to 4 claims).Paired against claim-set trees over the guests' leaves: same signers, same sets, same capacity, one binary at bca51cc, alternating under the bench lock at 1-minute load below 12, 16 threads 2 rounds and 1 thread 2 rounds (values per round, 16 / 1 threads). The leaves are copies of one proof, so every set is one leaf's 400 or 104 claims. Whole tree = every node after the leaf proofs.
W_leafnatively), and peak memory is about half the guest trees' (1.8 to 1.9 against 3.2 to 3.6 GiB).Duplicated from #595
Unchanged copies of #595's (
kw/clean-circuits-adder-20261010@ 2db90c1)LeanVMCircuits/Rec/*,Blake2s/*(withoutEmit), the generic closure (Adder,Lowering,Flatten,Export,Completeness,Gates,AdderFamily),CheckRec.lean,GenerateRec.lean, lakefile/manifest/toolchain, and the Rust builder trace (circuit-trace/circuitsfeatures,Circuit::dump,Tree::circuit_dump,rec/clean.rs,table.rs),rec-builder-model.yml.Audit.lean,README.md, the root module andclean-circuits.ymlare trimmed to this branch.Measurements
AMD Ryzen 9 7950X3D (16 cores, 32 threads), 62 GiB. Proof log-inv-rate 1 (aggregation leaves at 2, tree proofs at 1). Paired runs alternating guest and circuit under
flock /tmp/leanvm-bench.lock, each started at 1-minute load below 12, one binary at dbc9ad8 (the guests publish signer sets since #612; rows and committed words of every circuit below are unchanged at the head). Single proofs: 3 runs of--repeat 3at 16 threads, 2 runs at 1 thread; values per run. A circuit proof's verifier also builds the circuit from n once (about 80 ms), not included. Peak memory and proof sizes after #630 are under Upstream merges and CI.Circuit build caching (e6d7041):
XmssBatch::new/SphincsBatch::newrecord the circuit as one part per signature, andprovereplays each part for its values in parallel (Builder::parts,Replay) instead of re-running every builder call. 9f2381f before, e6d7041 after, alternating, medians of 3 runs ("Build circuit" from traced runs, proving from--repeat 5):Proofs are byte-identical before and after (at 1 and 16 threads) and the dumped builder calls unchanged.
Single-scheme aggregation trees, 16 / 1 threads (one run each at dbc9ad8; whole tree = every node after the leaf proofs):
Circuit trees' roots verify slower than RISC-V trees' because the root evaluates
W_leaf, the leaf circuit's fixed columns, natively.Removing the selector (the kind bits, indicator constraints and per-kind masks that let a tree take more than one leaf family; 5c821f8 before, 1a14303 after) shrinks nothing. Rows per table and committed words are identical before and after for every tree, and the leanXMSS and leanSPHINCS trees' nodes are identical to each other (STEP and LINK absent everywhere):
Paired timings (release binaries alternating under the bench lock, 16 threads 3 rounds, 1 thread 2 rounds; whole tree, values per round) are within noise:
First-level, node and root-verify times are within noise too, peak memory is equal (1.65 to 1.89 GiB), and node proofs differ by under 1 KiB (for example 243.0 and 242.8 KiB).
Upstream merges and CI
fiat_shamir: spongefish-style transcript over the BLAKE2s duplex #607 (spongefish transcript) and pcs: refuse claim widths that do not fit a usize #608: merged (5740d40). Byte level, the duplex core (counters, hold-back, output blocks) is unchanged; the seed is
init(session)(the old seed with a zero statement half), the instance is the first message, roots are four words, the COMMIT/POW_BASE/NONCE nodes are gone and proof of work hashes a squeezed challenge with au64nonce.Rec.Duplexis remodelled accordingly (5e5390a, also in Author leanVM circuits in Clean, prove them, and export them to Rust #595);Builder::k_to_dis traced and modelled. A first-level node over circuit leaves binds each leaf's statement by the 32 bytes its transcript would squeeze right after the instance (instance_digest; rowsTranscript::digest_so_far, two hash rows per leaf).signers: signer sets, their digest and canonical form #611/leanxmss, leansphincs: leaf guests publish signer sets #612/rec: claim sets and their union in rows #613/signers: bring riscv-exploration to the restructured signer sets #615: merged (dbc9ad8); the new public
Builder::blockandBuilder::d_to_halvesare traced and modelled (5c821f8, also for Author leanVM circuits in Clean, prove them, and export them to Rust #595). No tree circuit changed because of the builder.tree: claim-set trees that anyone combines #614/tree: height-tiered claim-set trees, small proofs at heights of their own #618/tree: soundness fix, bind the claim-set union's run placement before its challenge #626 (claim-set trees, tiers, union): merged (785614c). Upstream's places, tiers, claim-set and union design is kept, with this branch's one leaf family per tree (
Design.family) beside it. Dense polynomials areBytecode, Image, Leaf, Fixed, Wide, a statement holding values for the ones the tree has.Tree::new(Leaves, TreeShape { arity_0, arity, rate, claims }). No builder call or Lean file changed: the tree dumps differ from 1a14303 only in the session-derived constants, andcheckrec/checkxmssaccept every dump.cargo leanvm bench --cycles-onlyis identical to b094d00 for every tracked case (the aggregate first-level and node rows, proven rows and committed words included).tree: a lone child of any size, absent places at every claim-set node #627 (lone children and absent places at every claim-set node) and pcs: restrict the stacked opening to callers that bind its claims #609 (stacked-opening lint): merged (07df524). Versions were then
leanvm-tree-16andLVMT19, one above upstream's 15 and 18.leanvm-claim-union-3is upstream's, since this branch does not change the union. tree: a lone child of any size, absent places at every claim-set node #627's two pin tests (..._keeps_tree_12s_heights_and_layout) take this branch's heights (STEP and LINK absent), and their session bytes are pinned as this branch derives them, because the tag also names the leaf family. No new caller ofCommittedStack::openorStackCommitment::verify.leanvm_core, doc: prove flock's reductions before the bus #630 (flock's reductions before the bus) and tree: tests that a claim-set tree is its leaf program's, so leanXMSS and leanSPHINCS never mix #628 (a claim-set tree is its leaf program's; tests only): merged (c65b918, 747b534). The recursion machine's proof is commit, flock, bus and tables, opening, in
prove_withand inTableArgument::verify_core, which node circuits replay; the STEP and LINK tables need nothing of their own, being bus and table-sumcheck blocks like the others. Versions areleanvm-tree-17andLVMT20, one above upstream's 16 and 19;LVMP17, thev2session tag andleanvm-rv64im-13are upstream's.a_tree_refuses_another_familys_tree_proofsnow expects a proof under the other family's session to fail at flock's zerocheck, the first stage. tree: tests that a claim-set tree is its leaf program's, so leanXMSS and leanSPHINCS never mix #628's tests build their trees fromLeaves::Runsand pass. The tree dumps change (node circuits verify children in the new order);checkrecandcheckxmssaccept every fresh dump, the leanXMSS and leanSPHINCS circuit dumps are byte-identical, andGenerateRecreproducesrec/clean.rs. Paired peak memory after leanvm_core, doc: prove flock's reductions before the bus #630 (bca51cc before, 3a026fb after, alternating under the bench lock, 2 rounds each at 16 threads; trees of outputs). Rows and committed words are unchanged for every proof and tree node. Flock's batch is freed before the bus, so a circuit proof's peak falls by 0.16 to 0.21 GiB; a leanXMSS guest tree's peak lies elsewhere and is unchanged. Proving times in these runs were taken beside other jobs and are not reported; the tables above keep their binaries' numbers.CI at 747b534: every check passes (Test, Counts, the Lean
proofsandreplayjobs, the iOS and Android release builds); onlybuild-pdfskips, as usual. Counts are unchanged.Counts: at 48a0d09 the guest trees grew (2-to-1 first rows 138537 to 138538, proven rows 231424 to 231426, committed 5981184 to 5981211; node rows 119464 to 120721; 4-to-1 first 275693 to 275694, node 250255 to 252703, proven rows +2, committed +27). Causes: an empty STEP and LINK table still committed one padding row each (18 + 9 words, 2 proven rows), node circuits verified those tables of every child, and the tree statement carried a value word for
W_leafeven in trees without circuit leaves (the first level's +1 PUB row). Fixed (5b6d01c): a table with no rows is absent (Heights = PerRecTable<Option<usize>>; fixed by the heights the verifier holds, nothing committed, no bus blocks, constraints, opening share or verifier rows; tree session tag bumped), and a statement holds values for the dense polynomials the tree has only.cargo leanvm bench --cycles-onlyis now identical to the base for every tracked case.flock: a bit pass leaves every worker tasks on a small circuit #631, doc: zero-knowledge leaves #619 to rec: aggregation trees over zero-knowledge leaves #624 (zero-knowledge leaves), leanvm, primitives: put every module where it belongs #633 and primitives, fiat_shamir, zk, pcs, flock, rec: std-grade APIs and module layout #634 (module layout and std-grade APIs): merged (fcead06). The branch follows upstream's layout and names. The builder is one
rec/circuit.rs, with this branch's dynamic chains and parts replay beside it inrec/circuit/{chain,parts}.rs.Builder::eqandBuilder::exposeare traced aseq_e/eq_k/eq_dandexpose_e, and theArithimpl'smulandsquareare traced as before, so the dumps andcheckrec/checkxmssare unchanged in format.XmssBatch/SphincsBatchhold aCircuitKey, andLeafCircuitholds the batch's&CircuitKey.TreeShapehas noleaffield: the leaf shape is the family's (Leaves::Runs { program, shape }), andTreeShape::depthreplacesroot_kind. The CLI formats table stats itself (bench::pretty_integer), soTableStatshas noDisplay.Rec/Emit.leanemitscrate::buspaths intoclean.rs.Zero knowledge: RISC-V leaves may be zero knowledge, as upstream's trees allow (
Leaves::RunswithLeafShape::zero_knowledge(),--zkonaggregatewith a guest program). The tree session names the leaf kind (one more byte in theRunstag), so a ZK tree and a plain tree over one program never share a session. Signature-circuit leaves (Leaves::Circuit) are recursion proofs, which are never zero knowledge, so that combination is refused:--zkwithleanxmss-rec/leansphincs-rec, or with those programs asaggregateleaves, is a CLI error. Versions:LVMT20 andleanvm-tree-17stay one above upstream's 19 and 16.LVMP17 andleanvm-rv64im-13are upstream's. The two..._keeps_tree_12s_heights_and_layouttests pin the new session bytes; heights and layout are unchanged.Checks at dc7bb92: fmt; clippyall (haswell 1.97 and 1.99, native 1.99), system-alloc, AVX-512, ARM64,
--features circuits; docall; testall (541 passed);lake build,Audit.lean,leanchecker LeanVMCircuits.Rec.Emit,checkrecandcheckxmsson fresh dumps, and theGenerateRecdiff, all exit 0. Release smoke:leanxmss-rec --n 400andleansphincs-rec --n 104prove, serialize and verify, and refuse a tampered signature. Trees of outputs and claim-set trees (capacity 801 and 209) over four circuit leaves prove and verify. A ZK tree overleanxmssguest leaves proves and verifies.--zkwith circuit leaves is refused.a_tree_refuses_another_familys_tree_proofspasses.Recursion machine: STEP and LINK tables
Two tables join EMUL, EXK, HASH, SPLIT, CAST, PUB (order EMUL EXK HASH SPLIT CAST STEP LINK PUB). Their rows put data-keyed tuples
(key, x0, x1, ACT, 0)on the existing bus (the leaf multiset framework already balances any degree-2 forms; the machine used it only for copy cycles):ACTis a new public fixed column (1 on a table's rows, 0 on padding), bit 63 of every dynamic key keeps them apart from slot keys, and a committeda(wired to 1 on real rows) makes zero padding rows push what they pull. STEP's tweak word is its nine position bits over2^8; its push key is the pull key's position plus one, the carry over bits 32 to 34 asX^32 a + X^33 a s0 + X^34 a s0 s1. NewCoord::ScaledProdinleaf. Lean:Rec.Modeltables,chainStep/link,Rec.Tablesforms (GenerateRec emits them intoclean.rs),BalancedandAcceptsinRec.Contracts. Tamper tests: a wrong step input, swapped or missing steps, a mismatched link end, a cycle of steps at a chain index past 41, a padding row carrying a tuple (refused by the prover's bus; with a forged ACT the verifier rejects).Not done
The export check is per dumped size; the tree's signature first-level circuits (and their claim-set reading) are not modeled in Lean; no tracked
benchcases for the circuit paths;CheckXmssdoes not parsek_to_d,blockord_to_halves(signature circuits do not call them).