Check transcript binding of recursion circuits (stacked on #595)

[kevaundray]

This PR was created with Claude Code, prompted by @kevaundray.

Stacked on #595 (based on its head 793fbc1, which merges upstream riscv-exploration at dfb7570, #630: flock's reductions before the bus), with upstream riscv-exploration d0b0f82 (#631) merged in.

Adds lake exe checkbind, a transcript binding check over the recursion builder dumps that checkrec already replays, with a kernel-checked verdict, and proves the claim union's coverage check sound on the circuit. Also adds lake exe checkdesign (a model of rec::tree::design for every tree shape, compared with Rust, now including the claims a node takes, exposes and binds) and lake exe checkedges (the tree's edges from the dumps), makes collision resistance an event of the ideal compression model, and reduces the AIR link to the checks' claims on the committed witness.

Correction

As first stated in this PR, sumcheck_test_sound and odd_test_sound were vacuous. Their answers val r had to hold every constraint, each squeeze's compression included (Holds), and to agree on what is absorbed before round i whenever their challenges before i agreed; the round's challenge is the compression of what was absorbed, so it agreed too, forcing r i = r' i, and no answers existed once E has two elements. They are now stated in the random-oracle view: each transcript seeds its challenges one step after the block they read (chalSeeds), each transcript carries a second rule set reading none of its own absorb blocks' or squeezes' rows (Transcript.rulesRO, dropOf, Cert.marksRO) which the round certificates bind with, and the answers are RomAnswers c s T (every constraint and replayed call but the tests and transcript T's own rows, HoldsP/Facts; collision resistance away from them). RomExample.sumcheck_answers_exist, odd_answers_exist and pow_answers_exist exhibit answers meeting every premise but acceptance, at every challenge vector, on a circuit whose challenges are squeezes of its transcript's blocks. pow_test_sound now reads the trial digest's first word as the oracle's answer. The tests' binding (tests_by, tests_determined, the union theorems) keeps the full rule set: checkbind's verdict and every test's binding time are unchanged on all 17 dumps and the fixture.

The check

• Transcripts are found from the dump: duplex absorb blocks (counter role 2 to 5) and squeezes (output tag), chained by chaining value.
• Determination rules over wire limbs, each with a justification (Bind.Just) naming a row, an equality or a public row: a slot limb is its table's form of the columns it reads, SPLIT word and bits give each other, a constant mux bit picks a message word, a compression at a constant final word gives its output, inv's product gives each factor from the other, equalities that are not tests hold both ways, collision resistance gives a compression's inputs from its output and a chaining value from four consecutive output-stream words, and a union product is a function of its pool's digests, begin and selection bits and its point.
• A test is an eq_e/eq_k/eq_e_const/eq_k_const whose wires depend, through the calls that make wires, on a squeeze. Every test must be bound by one transcript.
• union.rs marks each pool and product in the trace (Builder::mark, tracing only). The certificate names, call for call, where each pool, product and point is.

Kernel-checked

Bind.Cert.accepts is the verdict: every rule's justification checks against the circuit, each transcript is a chain of compressions from a constant, the unions' calls are where the certificate says, every field equality reading a challenge is a test, some transcript's replay of the recorded firings gives every test's limbs a binding time, each union's coverage entry holds, each named sumcheck's rounds, proof-of-work check, GKR odd layer, GKR radix-four top layer, claim split and WHIR sumcheck are where the certificate says (Cert.sumchecksOk, PowCert.ok, Cert.oddsOk, Cert.lateOk), and their challenges are drawn in order from the oracle's words (Cert.chalsOk). Premises are named where used: HashCR (two hash rows given the same output ports, one by each assignment, are given the same input ports) and WindowCR (an output window of one chaining value fixes it); the random-oracle rule set's validity needs them only away from the squeeze rows (HashCRP, WindowCRP).

• tests_by: each test's limbs, at their binding time k, are in the closure of what one transcript's first k blocks absorb, and of the statement only once k passes its last block (certifyT_sound). checkbind_sound is its weaker form with the whole transcript.
• tests_determined (premises HashCR, WindowCR): on two assignments holding every constraint but the tests (Holds, implied by Model.Sat) and agreeing on what a transcript's first k blocks absorb (and the statement past its last block), k the test's binding time, each test's wires agree. A test bound after its latest challenge (a round-by-round sumcheck check) is thus a function of the blocks before the next challenge.
• tests_cover: no field equality the circuit keeps as a constraint reads a wire the verified scan marks as reading a challenge (taintStep). The classification is not a premise of any theorem's soundness: each is stated for assignments satisfying Holds, which Sat.holds gives from Model.Sat whatever the classification.
• unionsValid (premise HashCR): each union product is a function of its digests, begin and selection bits and point. From Model.replayR_sound (a replay with the tests' equalities relaxed builds the circuit without its tests, so every other call's contract holds under Holds), PoolParse.parse_unique (a run's chain followed back from its end to its start bit fixes its kind bits and blocks), PoolCert.pool_sem, PoolCert.pool_unique, prod_agree, claim_valid.
• union_cover (premise HashCR between the assignments): if in one assignment holding every constraint but the tests the two pools' claims on are different multisets, the points (X, A) of S^5 at which some assignment with the same digests, begin and selection bits holds every constraint but the tests and the coverage test are at most a 4N/|S| fraction. From point_sem (the weights are eq(A, k)), prod_closed/prod_slotsAt (a product is UnionSound.slotsAt of its pool's slots, tuples (1, label, member)), slots_bits, slots_agree, and UnionSound.coverage_sound (Schwartz-Zippel; poly_injective is lem:gp via Clean's eq_of_fingerprintProduct_eq).
• union_sound (premises HashCR, WindowCR, and the challenge uniform on S^5): the union's theorem on an accepted circuit. The certificate names each union's coverage test, its two products and its transcript (Bind.Cover); Cert.coversOk checks the test's wires are the products' outputs at one point, every product has an entry, the transcript binds what both pools commit to (PoolCert.committed), the declared pool has one digest and does not select, and the children's pool's run one-hot closes at its last digest (PoolCert.endOk, union::PoolShape::rows's closing eq_e_const checks). Fix what the transcript absorbs by an assignment in which the selected child claims and the declared claims differ; if at each outcome of the challenge the prover answers with an assignment holding every constraint but the tests and absorbing the same words, the outcomes at which its point is the challenge and the coverage test holds are at most a 4N/|S| fraction.
• Pool claims are the named sets (Rec/PoolClaims.lean, premise PoolClaims.ChainCR: no pool row's compression collides with the chain of a named set's blocks). A set's written form (ClaimSet.blocks, ClaimSet::items) and digest (ClaimSet.digest, under blakeF, the compression a block row computes). run_reads: a run whose expected digest is a set's reads that set's blocks item for item. reads_sum/readC_blocks: the pool's items read the sum of the claims of the sets its runs name. pool_claims: claims on are at most that sum, and that sum without selection. cur_runAt: the run one-hot of a chunk is at the number of begin bits set so far, so under endOk every run is a distinct digest's. decl_claims: the declared pool's claims on are the declared set's; sel_claims: the children's pool's claims on are among the sum of the children's sets. union_sound_sets (via sets_differ): union_sound with the premise that the declared set's claims are not among the children's.
• union_sound_queries, union_sound_sets_queries (Rec/Composition.lean): the union bound over Q transcripts a prover may try, each with its own uniform point, the prover answering with the one it picks: at most a Q · 4N/|S| fraction.
• Sumcheck.sumcheck_sound, Sumcheck.sumcheck_sound_frac (Rec/Sumcheck.lean): sumcheck's round-by-round soundness at the protocol level. For an instance whose honest round polynomials have degree at most d, a prover whose round polynomials (degree at most d) may depend on the challenges so far, and a false claim, the verifier accepts at at most n · d · |S|^(n-1) challenge vectors of S^n, an n · d / |S| fraction. The instance carries each round's eq weight when factored out (Sumcheck.lin); Sumcheck.sumcheck_sound_fun is the bound for a prover given by its round polynomials at each challenge vector, round i's reading only the challenges before it.
• Sumcheck on the circuit (Rec/Rounds.lean, Rec/RoundSound.lean). Every sumcheck reads its rounds with Verifier::read_round (the claim fixes one coefficient, so each round's check holds by construction) and its next claim with poly_eval; its one test is the last claim against the verifier's value. checkbind finds each such test's rounds back to the input claim and records a Bind.SumcheckCert (a Bind.RoundCert per round: the fold past the fixed coefficient, the fixed coefficient's call, Horner's mul_adds, the challenge's k_to_e of three squeezed words and its time in the transcript). The verdict checks the calls, that the test is a test of the last claim, that each challenge is squeezed from the chaining value of the transcript's block time (RoundCert.chalOk), and that what the round's prover sends, its eq weight and the input claim are bound by those blocks (SumcheckCert.boundOk); a table sumcheck's input claim reads hinted fixed-column evaluations, which the certificate names (SumcheckCert.hints, each a claim the reduction takes, an edge term value) and binds the claim with as seeds. sumRound_sem: where the replayed calls hold, the round polynomial Sumcheck.polyOf of the coefficients has degree at most d, passes the round's check against the claim and is the next claim at the challenge. sumcheck_test_sound (premises HashCR, WindowCR between answers; the honest instance Sumcheck.Inst as an explicit interface, with the circuit's eq weights): for answers indexed by the challenge vectors r of S^n, holding every constraint but the tests, with challenges r, agreeing on the blocks before round i's challenge when their challenges before round i agree, and an input claim that is not the instance's sum, the vectors at which the test holds with its other side the instance's final value, and the hints are their true values, are at most n · d · |S|^(n-1) (Sumcheck.sumcheck_sound_on). RomExample.sumcheck_hinted_answers_exist exhibits hinted answers.
• Proof of work: Bind.PowCert names check_pow's trial compression, the d_to_k and split of its first word and the eq_k_const tests of its top b bits. pow_sem: where the tests hold the word is below 2^(64-b). grinding_bound: a prover picking one of Q trials, each first word uniform, passes at at most a Q / 2^b fraction of the outcomes; pow_test_sound is both on an accepted circuit.
• GKR's odd layer (no sumcheck): Bind.OddCert names the values combined at λ, the children's products combined at λ, the test, and each value's line through its children at the next challenge; Cert.oddsOk checks the calls, both challenges' squeezes, the values bound before λ and the children before the next challenge. odd_sem reads them; odd_test_sound (true children as the explicit honest instance): if some value is not its children's product, the pairs of challenges at which the test holds and every next claim is its value's true line are at most an m/|S| fraction.
• The tree (Rec/TreeSound.lean): a node's statement words are the next verifier's claims. TreeSound.tree_sound: over a tree (nodes, root at depth zero, parents one level up), if at each node off an event bad v a true statement makes its input claims true, a child's statement is true when its parent's input claims are, and the root's statement is true, then off every node's event every node's statement and input claims are true; tree_sound_frac/tree_sound_eps: the failures are at most the sum of the nodes' fractions. In every dump the test bound only with the statement is the reduction's last check, certified with the other sumchecks.
• Late tests (Rec/WhirRounds.lean, Rec/LateSound.lean), each in the random-oracle view of its own transcript: GKR's radix-four top layer (TopCert, top_test_sound: an (m + 1)/|S| fraction, card_plane_zero), the table sumcheck's residual (resid_sem, within sumcheck_test_sound, its hinted fixed-column claims bound as seeds and counted at their true values), a leaf's program claim split (SplitCert, split_test_sound: the split is exact), and WHIR's sumcheck read with fold and batch rounds (WhirCert, QuadCert, PExpr, whir_test_sound: n · d / |S| over all its rounds from the opening's first claim). A batch round reads rows the Merkle paths bind through the query positions, squeezed from the same chaining value as the batching challenge λ: the certificate names λ's own squeezed words (own) and binds the round's atoms with the other words of that chaining value as seeds at λ's time (WhirRound.seeds, Cert.timesX, timesX_sound, whirBound_closure, ro_agree), and WhirAnswers asks answers to agree on those words. RomExample.top_answers_exist and whir_answers_exist (a batch and a fold round) exhibit their answers.
• A prover's run (Rec/Run.lean). Bind.Run: an assignment at each oracle ρ (the answers at its transcript's squeezes' output words), in the random-oracle view, its squeezes' outputs ρ's answers, what its first k blocks absorb a function of the answers drawn by k, and, off a collision event C of its execution, collision-free against any execution sharing its prefix on the rows that prefix binds (Run.cr, PairCR). Collision resistance is asked of nothing else: rule validity only for the rules a derivation fires (closure_agree_on), and collision and window rules fired from a prefix read only rows live on it (RowLive, HashCRP/WindowCRP on live rows, rules_valid). Each challenge's k_to_e reads three squeezed words (ChalCert.read), and the verdict now checks every certified check's challenges are drawn in order from the oracle's words (Cert.chalsOk: each word a challenge seed one step after its challenge's time only, a place of its digest, none shared, times not decreasing, increasing for WHIR). oracleAt own ρ r puts a challenge vector's coordinates in place of those words; at any oracle the run's assignments there are SumcheckAnswers, OddAnswers, TopAnswers and WhirAnswers on every accepted circuit (Run.sumcheckAnswers, ...), good off C at the substituted oracle. The substitution is a lens (card_lens, run_frac), so each round theorem holds as a fraction of uniform oracles off C: sumcheck_run_sound_at, odd_run_sound_at, top_run_sound_at, whir_run_sound_at (the input claim bound before the first challenge, sumcheck_claim_agree with its hints as seeds), and run_frac_off charges C once. Proof of work's oracle is the trial compression's answer: pow_sem/pow_test_sound ask every call but that compression (FactsBut), and pow_run_sound bounds a run whose Q trials are answered by uniform oracle words by Q / 2^b. RomExample.run_exists gives a run meeting every premise but acceptance; RomExample.chalsOk_mutations shows the check rejecting a shared word, a late challenge, challenges out of order and a word past its digest's four, and on a dump a sumcheck challenge's k_to_e reading one word twice is rejected.
• The design model (Rec/Design.lean, Rec/DesignKind.lean): Design for every shape Tree::new accepts (places, tiers, kinds and positions, unions, the statement's layout, converge over an abstract heights oracle), with structural theorems for every accepted shape (tier_iff, position_code, code_position, children_tier, section_unique, converge_fits, converge_least, ...). Model.kindRows is Design::kind_bits and Model.limbRows the child's limbs as builder programs; Model.nodeRows_good: for every accepted shape and node position, whatever the transcribed rows (if they keep the builder's invariant), every child's kind is a kind of its tier, its top bits select that circuit's block of the fixed polynomial, is_node is zero exactly at the first level, and its verifier is given its words' limbs (ChildBound). checkdesign compares the model with Rust on 600 shapes (rec::tree::design_tests, fixtures/design-summaries.txt) checks the kind rows and limbs of every child of the 17 dumps against the model, and checks each circuit exposes its own kind code first (kind_exposed, kindConst_ev: a child satisfied at the words its parent's verifier reads has its own code as the kind word the parent binds).
• The tree's edges (Rec/Edges.lean, checkedges): the dumps mark each child's statement words, the layout and the claims the reduction takes. Edges.EdgeCert.edge: in every satisfying assignment, every claim a child's words make at its kind's scale (nodeScale, from the calls computing it, ScaleCert) is among the reduction's claims, and the digest read is the words' halves. Edges.InstCert.verifies: the child's verifier (RecShape::verify) absorbs the words as its transcript's instance before any challenge (the count, then each word's limbs, as the native instance) and reads them into the public table's columns (statement_at, VerifiesAt). Edges.tree_sound_certs: tree_sound over certified circuits, a child's statement being the words its parent's verifier reads (treeStmt), with the recursive verifier's soundness at that statement (hrec) as the premise on a child; Edges.sat_tree gives every node's circuit satisfied at its treeStmt. A verifier's soundness holds off an event of its challenges: Edges.tree_sound_certs_off takes hrec only off an event badRec v per child (sat_tree_at, hedge_at: the induction at one outcome), and Edges.tree_sound_certs_frac bounds the outcomes at which some node's statement or input claims fail by the sum over the nodes of their bad and badRec fractions.
• The recursive verifier at a child, decomposed (Rec/RecParts.lean). hrec now also receives the parent's satisfied circuit. The parent's verifier of a child is a list of certified checks, each reducing input claims to output claims; where the parent's circuit is satisfied a check lets a false input through with true outputs only on its event (RecParts.Ok.test), and each check's outputs are later checks' inputs or openings of the child's committed witness, true off the PCS event (RecParts.Ok.flow, Add executable Lean WHIR and checked list-binding composition #551's ε_PCS). RecParts.ins_ok: off those events every check's inputs are true; RecParts.least_ok: the least such events satisfy the premises for any claims; RecParts.hrec: hrec off the checks' events, pcsBad and crBad from the AIR link (hair); Edges.tree_sound_parts: the tree's failures are at most the sum over the nodes of their bad, checks' events, pcsBad and crBad fractions. Each certified check is such a part (sumcheck_part, whir_part, odd_part, top_part), its event bounded at each oracle with no premise that its input is false (sumcheck_run_sound_at, whir_run_sound_at, odd_run_sound_at, top_run_sound_at: the input is bound before the check's first challenge, sumcheck_claim_agree, card_at). The AIR link is the premise left: where the parent's circuit is satisfied, every check's inputs true (the AIR's constraint and bus claims on the child's committed witness), no compression colliding and the parent's verifier reading statement st, the child's circuit is satisfied at st.
• The bus (Rec/BusBalance.lean): BusBlocks::new pulls each slot's key and limbs and pushes its next key with the same limbs (a Rust test, rec::bus::tests::every_slot_pulls_its_key_and_pushes_its_next_with_its_limbs, checks the plan slot by slot), and bus::verify_balance's fingerprint weights are the union's eq(A, k) over four challenges. balanced_of_eq: equal sides, encoded injectively, are Balanced. bus_balance_sound: if they do not balance, the points (β, A) of S^5 at which the two products agree are at most a 4n/|S| fraction (UnionSound.coverage_sound). bus_copy_sound: with next the classes' cycles, the points at which the products agree but two slots of one class differ are at most that fraction (copy_argument).
• The design's claims (Rec/DesignClaims.lean, checkdesign). The summaries now hold, per shape, the statement's edge layout, Design::carried on a statement of labeled words, Reduced::statement on labeled reduction outputs (two round counts and presences), each tier's Design::fixed_claim on labeled hints of every fixed column at zero heights and at heights differing per table and tier, and once NodeClaims::bind_state of a labeled state; checkdesign compares each with the model on all 600 shapes (carriedOk, exposedOk, fixedOk, bindOk, each with kernel-checked mutations it rejects), and computes each tier's fixed stack's variables from its columns' instead of reading them. Proven for every layout: stmtClaims_stmtOf (what a parent reads off a node's exposed statement is exactly the node's reduction outputs; reduced_dense_mem, reduced_matrix_mem, stmt_exposed: the tree's step at a node is the reduction's soundness on those outputs); offset_aligned, offset_disjoint, offset_fits, block_spec (the fixed stack's placement); term_reads and fresh_fixed_reads (a fresh fixed term, column c at its prefix, its block and the child's kind bits, reads the extension of column c of the child's own circuit, for any column values, the multilinear extension modeled lowest coordinate first); bindState_good, bindState_binds (the two bound scalars are the final digest's words and determine it); digestHalves_good, digest_roundtrip (a parent's halves_to_d reads the digest the child's digest_halves_rows wrote, top limbs zero). digestRows_good (Kind::digest_rows computes the tree statement digest of its tag and items in every satisfying assignment; the summaries hold Rust's node digest of labeled children's digests for every tree of outputs, compared with the model's own BLAKE2s, nodeDigestOk). tierMode_scale (a child's scale, in its tier's mode, is zero exactly at the first level and one at every node), which checkedges now checks of each dump's children (modeOk). The edge marks' parser moved to Rec/EdgeMarks.lean for both checkers. Rust: design_tests emits the new lines; carried, fixed_claim, Reduced::statement and bind_state are pub(super) for it.
• Collisions as an event (Rec/Collision.lean). An adaptive prover against a uniform compression oracle: Collision.birthday_frac (two distinct queries of the first Q collide on at most a Q(Q-1)/(2|Y|) fraction of oracles, by resampling the first fresh query of a colliding pair), Collision.win_frac (a window hit: two output blocks of each of two chaining values, alike off the chaining value, agreeing on four words straddling them, 2Q(Q-1)(Q-2)/|K|^4, charged to the last first query of the four). The window rule now takes the two blocks' other input words (counter, finalization, message: constants in an output block) as premises, which is what makes the window a four-word event; it was bounded by a two-word near hit, 3Q(Q-1)/(2|K|^2), which capped the proof near 2^64 queries. A mutation test rejects a window without them or of two chaining values. Off the events Bind.pairCR_of_oracle gives PairCR of assignments whose live non-squeeze hash rows are oracle queries (Bind.OracleRows). Edges.crEvent, Edges.crBad_frac (a child's crBad over Ω₀ × oracle is at most epsCR of its query count), Edges.PcsBound (Add executable Lean WHIR and checked list-binding composition #551's Whir.SpongefishCurrentKnowledgeFinal.current_knowledge at 8198d0b as the stated interface for pcsBad), Edges.tree_sound_eps (tree_sound_parts with epsPCS v + epsCR v).
• The AIR link (Rec/AirLink.lean). A committed witness (heights and columns per table, the public value columns included) and the AIR's claims of it (AirLink.Claims: row counts within the heights and 2^32, each circuit row satisfying its table, public columns carrying each public row's constant or statement word, the bus balanced with next the slots' class cycles). AirLink.sat_of_claims: they give Model.Sat at the statement, for the assignment reading each wire off its class's first slot; claims_of_sat the converse for an honest witness (non-vacuity), and three circuits no witness meets (mutations). The bus is derived from the GKR root's two products agreeing at a draw off busDraws (bus_of_product, busDraws_card, busBad_frac: 4 · slots / |E|). AirLink.hair_of_air derives hair from AirLink.ChecksGiveRows (true check inputs give the rows' claims and the products' agreement, off crBad and the constraint batch's event batchBad), and AirLink.tree_sound_air is tree_sound_parts with it. Rec/TreeBound.lean: AirLink.tree_sound_bound (each event's fraction replaced by its bound: epsPCS v + epsCR v + epsBus v + epsBatch v per child beside its reduction's and checks' events), tree_sound_crEvent (crBad the ideal model's crEvent, bounded by epsCR of the child's queries) and tree_sound_ideal (the bus also bounded, 4 · slots / |E|); Rec/AirBatch.lean: the constraint batch as TableArgument::verify and constraints::verify check it (at the bus's point ζ and ξ, the bus forms' sums plus Σ_j ξ^(2+j) C_j(ζ) over the 66 HASH and SPLIT identities vanish, AirLink.BatchClaim); a broken identity leaves it holding on at most (n + 67)/|E| of the draws (batchDraws_card: Schwartz-Zippel in ζ, roots in ξ; mutation badSplit_rejected), and tables_of gives every row its table's identities off them. The remaining premise is AirLink.ChecksGiveBatch (true check inputs give row counts, public columns, the hash rows' flock witnesses, the batch claim and the products' agreement at their draws); tree_sound_batch and tree_sound_ideal_batch are the bounds with epsBatch v = (n v + 67)/|E|, the draws taken uniform after the commitment. epsPCS stays the Add executable Lean WHIR and checked list-binding composition #551 interface.
• Digest edges (Rec/DigestEdges.lean, checkedges). Edges.DigestCert names the calls by which a wrap states its only child's digest (the halves_to_d of the child's statement words 1 and 2) and a node of a tree of outputs Kind::Node::digest_rows of its children's digests, exposed as digest_halves_rows writes it at statement positions 1 and 2; DigestCert.exposed, wrap_states and node_states prove them sound where every call holds, and wrap_mutations, node_mutations are kernel-checked mutations. checkedges finds and checks the certificate on every wrap and output-node dump, and rejects a wrap's dump with its halves' exposures swapped and a node's dump with its children hashed out of order or its header's count replaced.
• Committed instances and the AIR's draws as Fiat-Shamir draws (Rec/Run.lean, Rec/AirRun.lean). Bind.CommittedBefore: a function of what the transcript absorbs before a time, as the committed witness is through its commitment; Bind.Run.committed_at makes it fixed across the challenge vectors put in when every challenge is drawn after (Bind.draws_not_fixed: the draws are not). The run theorems sumcheck_run_sound_at, whir_run_sound_at, odd_run_sound_at and top_run_sound_at take the honest instance, the hints' true values and the true children as such functions of the oracle (Run.sumcheck_committed and the like). AirLink.busRun_frac and AirLink.batchRun_frac bound the bus's and the batch's draw events by 4N/|E| and (n + 66 + 1)/|E| with the draws a run's challenges after the commitment and the prover adaptive, and AirLink.tree_sound_run is the tree's bound over a uniform oracle with no lens premise.
• Add executable Lean WHIR and checked list-binding composition #551's bound in PcsBound's terms (Rec/PcsMatch.lean). Edges.Pcs551 takes Whir.SpongefishCurrentKnowledgeFinal.current_knowledge's conclusion in its own form (the uniform average over a primitive oracle and coins of the indicator of native acceptance with extraction failure, at most ∑ k : Fin 4, finalBound Q_k, finalBound verbatim), a map from the recursion's outcomes with fibers of one size, and pcsBad v inside its event's preimage; Edges.pcsBound_of_551 gives PcsBound. Edges.compress_fiber discharges the fiber premise for the ideal compression model's outcomes read through an injective encoding of Add executable Lean WHIR and checked list-binding composition #551's 833-bit node into the 14-word compression input and an output bijection.
• The scale's value (Rec/DesignKind.lean). Model.kindRows_good now proves a child's is_node zero at the first level and one at every node for every accepted shape (Model.prod_zero_or_one), not only zero exactly at the first level.
• The collision term per execution and the prover model (Rec/CrScale.lean). A run's cr is now asked between two executions sharing a prefix both off their execution's event, which every round theorem has (its two answers are both good). Bind.Run.cr_of_extract derives it by straight-line extraction from a causal prover (its queries before a squeeze are shared by the executions agreeing by then), normalized (its rows are among its first Q compression queries, consistent with the oracle), whose rows the prefix binds output words the prefix fixed (hout: an earlier answer, or one of at most B targets its answers by then fix). Bind.oracleRows_of_late: a row whose input is first queried after the squeeze answers a word fixed before it, a collision if that word is an earlier answer and otherwise a late hit on a target (Collision.LateHit, at most Q · B / |V|^4 of the oracles: Collision.late_card, Edges.lateEvent_frac). So a later query hitting a word the prefix fixed is a collision only when the word is an earlier answer; a word written without being computed is a preimage target, now its own term Edges.epsLate. Bind.out_of_prefix: the previous premise (every such row a prefix query) implies hout. AirLink.tree_sound_exec charges each child's epsCR K (Q v) + epsLate K (Q v) (B v) once, its checks' round bounds holding at every compression oracle (frac_prod_le). AirLink.tree_sound_end is the end-to-end statement for one tree: per child D v / |E| (its reduction's, checks', bus's and batch's terms), Add executable Lean WHIR and checked list-binding composition #551's Σ_k finalBound (Q_k) (pcsBound_of_551), epsCR and epsLate, summed over the nodes. Edges.tree_bound_deployed (|E| = 2^192, Edges.card_E): for at most 2^10 nodes with D ≤ 2^40, 2^64 compression queries and 2^86 targets per child, the bound is below 2^-19 at Add executable Lean WHIR and checked list-binding composition #551 budgets of 2^20 per binding shape and below 2^-7 at 2^32; Edges.pcs_dominates: Add executable Lean WHIR and checked list-binding composition #551's query term, about 2^-51.1 per query and shape, dominates (at least 2^-18 per child at 2^32, while the compression terms at 2^64 queries are below 2^-62). Edges.exec_bound_deployed bounds the compression terms alone against Q (below 2^-7 for Q ≤ 2^82) and Edges.epsCR_cap puts the window term past one at 2^86.
• The table sumcheck's and bus GKR's honest instances (Rec/AirBatch.lean). AirLink.ChecksGiveInst states ChecksGiveBatch's claims as the honest instances' values on the committed witness: the table sumcheck's input claim, the bus totals' σ_0 + ξ σ_1, is AirLink.tableSum (the bus forms' weighted sums and each identity's ξ^(2+j) C_j(ζ)), and the bus GKR's root claims are AirLink.pullRoot and AirLink.pushRoot, held equal by bus::verify_balance. checksGiveBatch_of_inst gives ChecksGiveBatch from it, the batch's bus parts the forms' sums less the totals (batchClaim_of_sum, productClaim_iff).
• The table sumcheck over tables of different heights as an instance (Rec/TableSum.lean). Sumcheck.mvInst is the honest instance of a polynomial on the Boolean cube with no eq weight factored out (mvInst_sum, mvInst_ok, mvInst_final, mvInst_weight). AirLink.tableInst is constraints::verify's: n rounds from the highest variable down, each table active in its own variables (eq(ζ_m, r) = 1 + ζ_m + r) and sitting out the rest at their corner (r), its summand TableSummand::batch on its columns' multilinear extensions. tableInst_sum: its sum is AirLink.tableSum at the forms' honest sums, each table summing its own rows (corner_sum); tableInst_ok (degree 3 and up), tableInst_final (the verifier's folded weights, foldWeight_eq, times the summands at the columns' extensions at chi), tableInst_weight (no eq weight). The committed witness is taken at a layout (committedAt: heights 2^τ, the public columns the verifier's at the statement), and AirLink.ChecksGiveTable gives ChecksGiveInst and ChecksGiveRows where the layout holds the rows (checksGiveInst_of_table, checksGiveRows_of_table).
• The table sumcheck named on the dumps (Bind.TableCert, checkbind). Each residual sumcheck is named as a table sumcheck: its rounds read no eq weight, its input claim is the mul_add of the bus totals at ξ, and a GKR first layer before it reads one root for both trees; checkbind fails a dump where one is missing or fails TableCert.ok, and all 17 dumps name every residual (0 to 4 per circuit). TableCert.sem, answers_weight and claim_iff read the named check's input claim as the totals' σ_0 + ξ σ_1; TableCert.okIn's mutation tests reject swapped totals, another claim, an eq-weighted round and two roots.
• The table sumcheck's residual certified term by term (Rec/TableResid.lean, Bind.ResidCert, checkbind). Each of its five terms names its weight's calls (from a one, a mul_add(w, add(ζ_m, r_j), w) per round where its table is active and a mul(w, r_j) where it sits out), its column claims, its push and pull forms at them (BusForm::at), their mul_add(ξ, pull, push) and its identities in allIds' order (BusForm::at_constants, the model's words) at the powers ξ^(2 + j). ResidCert.sem: where the calls hold, the residual terms sum to Σ_T foldWeight ζ τ_T r · summandAt forms ξ T col_T at the named point, τs, forms and column claims; ResidCert.final_eq: at the committed witness's τs, the forms forms and column claims the columns' extensions at chi r, that is tableInst_final. checkbind fails a dump where a table sumcheck's residual is not so named; all 17 dumps name every one. Mutation tests reject a weight with another τ, an identity with another word or read as another table's, identities out of order, a form reading another column and a wrong power of ξ.
• bus::verify_balance's decomposition modelled (Rec/BusDecompose.lean). AirLink.leaf_decompose: a side's leaf claim Σ_x eq(ζ, x) L(x) over blocks at their offsets is Σ_b sel_b Σ_z eq(ζ[..κ_b], z) leaf_b(z) + (1 - Σ_b sel_b). A table block's leaf β + Σ_i w_i c_i over its row's coordinates (DCoord) is its form (blockQuad, BusForm::accumulate) plus its virtual coordinates (blockKnown). side_decompose: the leaf claim is the framework part (framework) plus each table's form (sideForm) summed over its rows; totals_eq_formSums: the derived totals framework + Ṽ(ζ) are formSums in characteristic two; tableClaim_of_leaves: with both sides' totals so and no row breaking an identity, the totals' σ_0 + ξ σ_1 is tableInst's sum over the bus point's first N coordinates (formSums_restrict).
• Normalization and causality dropped from the prover model (Rec/CrScale.lean). Bind.Run.cr_of_normal: the prover normalized to query every hash row's input after its own Q queries (Collision.normalize, extra_mem_queries) needs only its output a function of its first Q answers and its rows consistent with the oracle, its events counting Q + |rows| queries. Bind.Run.cr_of_staged: a staged prover (Bind.Staged: its query and transcript time at its answers read only the challenges drawn by any time it has not passed) is causal (hcaus_of_staged, the queries before it passes k being stageN); cr_of_extract asks causality only along the prover's own answers.
• The bus GKR's layers (Rec/GkrInst.lean). Sumcheck.eqInst is the honest instance of an eq-weighted sum with each round's eq weight factored out (v.read_round(5, claim, Some(eq_point))). A product tree's levels (level_two, level_four, level_root) make the bus's honest roots its trees' roots (pullRoot_eq_level, pushRoot_eq_level). AirLink.layerInst is a radix-four layer's honest instance: its sum the claim Σ_t λ^t Ṽ_t(p) at the honest level values, degree 4, round i weighted by p_i, its final value the children's honest products at λ; next_claim (and odd_next for the odd layer) makes the layer's next claim, interp(interp(a, b, low), interp(c, d, low), high), the level below's value at [low, high] ++ r, so the honest values carry from the root to the leaves.
• Each table sumcheck's bus GKR named from root to totals (Bind.GkrCert, Bind.LayerCert, checkbind). Its first layer is a top or odd layer reading the root as both trees' value; each radix-four layer past it is a certified sumcheck with no residual whose input claim is the layer's claim over the previous layer's next claims, whose final side is its children's expected product, whose rounds' eq weights are the previous layer's point and whose next claims are a top layer's lines (LayerCert.chain); each total is the add of a framework share and the last layer's next claim. A GKR is paired with its table sumcheck by the chain that reaches that sumcheck's totals, so circuits verifying several children name each one's own. checkbind fails a dump where a table sumcheck has no GKR or one fails GkrCert.ok; every node dump names one per child (10 to 40 layers past the first per circuit), and the first-level dumps, which verify leaf proofs, have none. LayerCert.layer_sem reads a named layer's wires in AirLink.layerInst's form; GkrCert.sem and LayerCert.link_sem read the chain; mutation tests reject totals reading another wire, a first layer reading two roots, a layer round reading another eq weight and a layer whose values are not the previous next claims (GkrCert.okIn, LayerCert.linkOk).
• The layout and rounds hypotheses discharged for a tree Tree::converge built (Rec/Heights.lean). AirLink.layoutFits_converge: every circuit Design.converge returns, its heights holding its rows, fits its tier's layout within MAX_TAU (LayoutFits, via converge_fits); taus_le_rounds: every owned table's τ is at most the rounds constraints::verify runs, the tallest owned table's (tableInst_sum now asks it of the owned tables only, the public table being in no summand). AirLink.checksGiveRows_of_converge is checksGiveRows_of_table with both hypotheses replaced by the tree's building facts (each child its position's circuit at the converged heights, read at its tier's heights, Circuit::heights holding its rows). A one-tier example converges in the kernel.
• The AIR link's premise read off the named checks (Rec/Named.lean). AirLink.checksGiveTable_of_named: where the parent accepts its certificate and names the table sumcheck, ChecksGiveTable holds with the totals, root and ξ the named wires' values, given parts whose named table sumcheck's input is its honest instance tableInst's sum on the committed witness, whose bus GKR first layer's input is the named root being both trees' honest roots, and whose flock check's input is Flocked; TableCert.claim_iff reads the named input claim off the parent's facts. named_inputs is its non-vacuity.
• Circuit::heights transcribed (Rec/Heights.lean). AirLink.circuitHeights is Table::height_log of each table's rows (log2_ceil_usize, and for the hash table min_n_blocks_log at flock's floor) at least its floor; heightsHold_circuit proves it holds the rows, and checksGiveRows_of_tree is checksGiveRows_of_converge at those heights with HeightsHold discharged. Rust tests compare height_log with the transcription (rec::table::tests::a_tables_height_is_the_proven_transcription_and_holds_its_rows) and check the remaining building facts on a tree of one tier and one of two: each circuit Tree::converge returns has its tier's heights, at which a node reads its children, and they hold its rows (rec::tree::tests::every_circuit_is_at_its_tiers_converged_heights_which_hold_its_rows).
• GKR layers as checks of RecParts (Rec/GkrParts.lean). Bind.layer_part: where the parent's circuit holds a linked radix-four layer's calls and its sumcheck's test, its next claims true (each tree's level below at [low, high] ++ r) make its values, the previous layer's next claims, true (each tree's level at the previous point), off its sumcheck's event against layerInst (sumcheckFalse, bounded by sumcheck_run_sound_at), the line event LineBad (at most 2|S| of the pairs (low, high), lineBad_card via card_plane_zero) and the λ event LamBad (at most one λ, lamBad_card). checkbind now asks each layer to draw its challenges as a top layer's (LayerCert.chalOk, GkrCert.layersOk: λ, low, high in order from its transcript, its children bound by low's time, LayerCert.boundOk, and its values by λ's time with the words squeezed with λ but its own as seeds, LayerCert.lamOk: the sibling-word argument of WHIR's batch rounds, as the values read the previous layer's high, squeezed from the chaining value λ is squeezed from; both with mutation tests), and Bind.layer_run_sound_at bounds the line and λ events together over a run by 3 / |E| off the run's collision event (the values fixed across λ at each (low, high), Run.sib_agree, the children across (low, high) at each λ); LayerCert.chal_eval makes the challenge wires layer_part reads the oracle's.
• Several tried transcripts (Rec/Tries.lean). An outcome is an oracle per try on its transcript's words with the compression oracle they share; try i's event may read every try's oracle. Bind.frac_fix_le: an event at most an ε fraction of try i's oracle and the compression oracle at every value of the other tries' oracles is at most ε of all outcomes (with the others fixed as whole functions, try i is an oracle algorithm on its own oracle, the setting of Bind.Run and tree_sound_end). Bind.frac_pick_le: whichever try the prover outputs, its event is at most the sum of the tries' bounds (frac_pick_le_mul: m · ε; bitPick_frac an example). Edges.tries_bound_deployed folds it into the end-to-end bound.

Regression fixture

verification/circuits/fixtures/pre626-claimset-two-tier-circuit-1.txt.xz is a two-tier node circuit from #595 with b094d00 (#626) reverted. Its coverage test is unbound: the children's pool product reads begin bits no transcript absorbs. CI runs checkbind on every current dump and checkbind --expect-unbound on the fixture.

Status

All 17 dumps of the merged head (with the leanXMSS-100 2 to 1 tree over zero-knowledge leaves, first and node) are accepted with no unbound test and no uncertified eq_e test (2 union products and one coverage entry per union circuit); the fixture is rejected. checkbind rejects a dump with a WHIR sumcheck not certified from the opening's first claim, or with a hint that is not a claim the reduction takes; on a node dump, a query's k_to_e reading λ's own words and zeroed edge term values are each rejected. Per circuit, in the random-oracle rule set, 2 to 54 tests close a certified sumcheck (45 to 687 rounds, up to 4 by a residual, whose input claims read up to 408 hints), 85 to 340 are the bits of 5 to 20 proof-of-work checks, 0 to 4 close a certified GKR odd layer, 0 to 4 a radix-four top layer, 1 to 4 a WHIR sumcheck from the opening's first claim (29 to 124 rounds, 5 to 20 of them batch rounds) and 0 to 4 a claim split. checkdesign passes on the 600 shapes and the 17 dumps, checkedges on the 17 dumps. Audit lists only propext, Classical.choice, Quot.sound; leanchecker passes on every changed module.

The capstone bound per execution. As first stated the run theorems' Bind.Run asked every two answers of a run's family (one per challenge vector, |E|^n of them) not to collide, which only a query count covering every answer's compressions gave, so the bound was vacuous. Now collision resistance is asked only between answers sharing the prefix before a check's challenge, on the rows that prefix binds, both off their execution's event, charged once per execution (run_frac_off, tree_sound_exec), and the window term is a four-word event. The step from one execution's queries to the prefix rows is straight-line extraction (Run.cr_of_extract), which adds the late-hit term Q · B / |V|^4. End to end (tree_sound_end, tree_bound_deployed) the level is set by #551's PCS term, about Q_k · 2^-51.1 per binding shape and child: below 2^-7 for 2^10 nodes at budgets 2^32, the compression terms negligible beside it up to 2^64 queries. Over m tried transcripts, an oracle per try and the compression oracle shared, the output try fails on at most m / 2^7 (m / 2^19 at budgets 2^20), Q counting every compression query the prover makes (tries_bound_deployed).

Not proven: the rest of the AIR link's premise, AirLink.ChecksGiveTable: that the named table sumcheck's and bus GKR's input claims are true on the committed witness (reduced by checksGiveTable_of_named to parts whose named checks' inputs are their honest instances' claims; what stays is that such parts meet RecParts.Ok with the round theorems' events, each check's outputs being the inputs of the checks after it down to the opening; each GKR layer past the top meets RecParts.Ok.test off its sumcheck's, line and λ events, layer_part, the last two bounded over a run by layer_run_sound_at), that the circuit's forms and framework shares are AirLink.sideForm and AirLink.framework over the bus's blocks and the GKR's leaf layer is those blocks at BusBlocks::new's offsets (the decomposition is modelled, AirLink.side_decompose, totals_eq_formSums, tableClaim_of_leaves, but the circuit's selector, weight and accumulation calls are not certified), that the table sumcheck's named forms are those forms and its named column claims the columns' extensions at chi r the opening checks (ResidCert.final_eq's premises; the residual itself is certified term by term, ResidCert.sem), and the hash rows' packed witnesses (Flocked, flock's reduction); LayoutFits and τ ≤ n hold for a tree Tree::converge built (checksGiveRows_of_tree, HeightsHold proven of the transcribed Circuit::heights), with its building facts as premises, checked by Rust tests; #551's theorem itself (Edges.Pcs551.knowledge, a separate Lean 4.34 project) and pcsBad's inclusion in its event (Edges.Pcs551.sub: the parent's rows as #551's native acceptance of the child's opening, its extracted witness the committed one); the prover model's hout in Run.cr_of_staged (the rows a prefix binds output words fixed before the prover passes the prefix's time, at most B targets, true of a Merkle opening against an absorbed root and its paths' inner digests but not derived from the closure's rules), with the prover staged, its output a function of its first Q answers and its rows consistent with the oracle (the ideal model's compression); the reductions' bad events, entering tree_sound_end through D v; over several tried transcripts, that each try with the other tries' oracles fixed meets tree_sound_end's premises (tries_bound_deployed's hend); the design model's remaining transcribed rows (each child's verifier past its statement, with its statement weights and share wiring, the union's digest, the reduction's rows, the first level) and its heights oracle, beyond what checkrec, checkdesign and checkedges check on the 17 dumps and checkdesign on the 600 summaries; the GKR's own product claim beyond its certified radix-four layers (its odd layer), and the model's classes being the Rust classes beyond the seventeen dumps checkrec compares. The README's "End-to-end composition" states the target theorem and which parts #551 (Whir.StackWHIRROM.rom_list_binding_numeric, Whir.CommitmentAnchor.selected_unique, Whir.CommitmentAnchor.joint_opening_probability_numeric), #600 (callers bind each opening to its commitment record) and this PR supply.