feat: second recursion implementation#16
Open
ivokub wants to merge 50 commits into
Open
Conversation
Milestone 1 of the recursive-verifier effort. Adds the gadget primitive layer that future milestones will assemble into a complete verifier circuit: - extfield: E4Expr helpers (Add/Sub/Mul/Square/MulByBase) using v^4=3 reduction, differential-tested against gnark-crypto's koalabear/extensions. - gadgets/poseidon2: full width-16 Poseidon2 AIR (one permutation per row, per-round sbox/post witnesses, external/internal matrix layers). Cross-checked against the native permutation; negative test corrupts a mid-round witness. - gadgets/merkle: Merkle-step gadget with bit-selector and cross-row chaining. Hash-equality constraint via Poseidon2 lookup is left as a TODO for the follow-up milestone. - gadgets/challenger: Fiat-Shamir sponge API (Init/Absorb/Squeeze) on the width-16 MD permutation. Real FS uses width-24 sponge; that variant will be added alongside the actual verifier wiring. - Scaffolding: RecursionInput / AggregationInput, Poseidon2-only config validation, and stubs for buildVerifierCore / buildAggregationCore. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two new gadget primitives for the recursive FRI verifier:
- gadgets/frifold: per-row gadget for one FRI fold step
folded = (P+Q)/2 + alpha * (P-Q) / (2 * omega_j^base)
Both E4-rail (the dominant case in Loom) and base-rail versions.
xInv = omega_j^{-base} is supplied as a witness; computing it from
omega and base via bit-decomposition is deferred to a follow-up gadget.
- gadgets/fribatch: per-row gadget for the gamma-mix step that
incorporates a freshly-introduced level polynomial:
next = expected + gamma * (sel ? LeafQ : LeafP)
with sel a binary selector witness (= 1 iff base >= N_{j+1}/2).
Each gadget is independently testable; tests cover positive paths,
padding-row trivial satisfaction, and negative cases (corrupted folded
value, flipped selector, non-binary selector).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit moves the gadget primitives toward the full FRI verifier by
composing fold across rounds and adding the index-handling building
blocks needed to derive per-round data from a single query position.
- gadgets/friquery: per-query traversal module composing the fold
equation with the chain constraint between consecutive rounds:
expected[k] = (1-bit[k+1])*P[k+1] + bit[k+1]*Q[k+1]
Last-row chain to finalPoly is left as a TODO for the next milestone.
Tested with a real 4-round FRI simulation; chain corruption and
non-binary bits are rejected.
- gadgets/bits: per-row k-bit decomposition of a base-field value
(b_i*(1-b_i)=0 plus sum check). Exposes Register/BuildModule so it
composes with other gadgets in the same module.
- gadgets/binexp: in-circuit binary exponentiation. Given a precomputed
base g and the bit decomposition of v, computes g^v via a running
product chain with degree-2 constraints. Used to derive
xInv = omega^{-base} from a query position; cross-checked against
gnark-crypto Exp for 8 different base values.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two wiring milestones that reduce the verifier-circuit's trust surface
and close the FRI verifier's final-round gap:
- gadgets/friround: per-round FRI fold verifier across many queries.
One module per FRI round, NumQueries rows. The xInv = omega^{-base}
value is no longer supplied as a trusted witness — it is DERIVED
in-circuit via bits.Register + binexp.Register inside the same
module, with omega_j^{-1} baked into binexp's running-product
constants. Tests confirm corruption of base or xInv breaks
verification.
- gadgets/idxselect: multiplexer over a constant E4 table of size 2^k,
indexed by k bit witnesses. Tree-reduces with limb-wise expressions
(degree k, no intermediate witnesses), so a 16-entry table costs only
the 4 output limb columns + the bits gadget. This closes the FRI
verifier's last-round chain target finalPoly[s mod len(finalPoly)].
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… final)
This commit closes the FRI verifier's loop: a single Loom module now
verifies a complete per-query FRI traversal (all fold rounds, the
chain between them, and the finalPoly match) end-to-end.
- friround refactor: split BuildModule into Register (appends to an
existing module) + BuildModule (wraps create+add). Multiple rounds
can now share one module so chain constraints stay intra-module
instead of needing cross-module lookups.
- gadgets/frichain: per-query chain between two consecutive friround
groups. Emits (1) the leaf-selection constraint
expected_j = P_{j+1} + top_bit_j * (Q_{j+1} - P_{j+1})
and (2) bit-inheritance equalities binding the lower k_{j+1} bits of
base_{j+1} to the matching bits of base_j (so base_{j+1} is base_j
with its top bit shed by folding).
- End-to-end test: one module composes friround * numRounds + frichain
links + idxselect over finalPoly. Replays a real native FRI commit
phase on N=16, D=4, two queries; the in-circuit verifier accepts
the proof and rejects round-1's P/Q tampering.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Loom uses multi-degree FRI: extra polynomials of smaller degree are
introduced mid-flow and folded into the running polynomial via a
gamma-mix step. This commit adds the in-circuit equivalent.
- frichain.LinkWithLevel: chain variant for round transitions where a
new level enters. Adds the constraint
expected_j + gamma_l * leaf_l = selected(P_{j+1}, Q_{j+1}, top_bit)
with leaf_l = selected(LeafP_l, LeafQ_l, top_bit) — the level opening
is picked on the same branch as the running fold.
- frichain.RegisterLevel: companion helper that allocates the level's
column names (gamma, leafP, leafQ) inside the same module so the
trace generator can fill them.
- End-to-end test: multi-degree FRI with N=16, D_0=4, D_1=2 (level 1
enters at round 1). Native commit phase replayed, in-circuit
verifier accepts the proof, gamma tampering is rejected.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Without pinning, a malicious prover could supply a different alpha/ gamma per query row and pass the fold equation independently on each row. The FRI challenges are derived once from FS per round/level and must be the same for every query. - friround.Register: adds alpha[i] - Rot(alpha[i], 1) = 0 except at the last row (excluded to avoid the wraparound). Skipped when N < 2 (no other row to compare against). - frichain.LinkWithLevel: same constraint applied to gamma in each level introduction. - Existing tests that padded with zero rows now use 2 real queries (padding with alpha=0 would break pinning). - New negative test TestFriRoundGadgetRejectsVaryingAlpha confirms per-row alpha variation is rejected even when each row's fold equation is internally consistent. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Loom uses two Poseidon2 variants: width-16 for Merkle node compression (already implemented in gadgets/poseidon2) and width-24 for Merkle leaf hashing and the Fiat-Shamir transcript (rate 16 / capacity 8 sponge). This commit adds the width-24 in-circuit gadget, mirroring the existing width-16 layout: - 24-element input + output state per row - 27 rounds (6 full + 21 partial) with degree-3 S-box - per-round (sbox, post) witness snapshots - same external matrix shape (circulant of M4 blocks, 6 chunks) - DIFFERENT internal diagonal (24 entries vs 16) Round constants are pulled from gnark-crypto's NewParameters with width=24, matching Loom's native Poseidon2SpongeHasher seed exactly. Tests cross-check 4 random outputs against the native width-24 permutation lane-by-lane, exercise padding rows, and reject mid-round witness corruption. This unblocks two follow-up milestones: (a) Merkle leaf-hash equality for FRI openings, and (b) in-circuit Fiat-Shamir transcript derivation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Brings in-circuit equivalents of Loom's Merkle hashing functions:
- gadgets/leafhash: ext-rail variant of commitment.Poseidon2LeafHasher.
Wires the width-24 Poseidon2 sponge to absorb (LEAF_TAG, 0, 1, LeafP
limbs, LeafQ limbs, 0...) and exposes the first 8 lanes of the
post-permutation state as the 8-limb digest. Limb ordering is re-
mapped between the sponge's {B0.A0, B0.A1, B1.A0, B1.A1} encoding
and extfield's {B0.A0, B1.A0, B0.A1, B1.A1} order.
- gadgets/nodehash: equivalent of commitment.Poseidon2NodeHasher. The
17-element input (nodeTag, left[8], right[8]) requires TWO width-16
Poseidon2 permutations with Merkle-Damgard feedforward; the gadget
composes two poseidon2.Register calls and links them via input-
equality + feedforward expressions. Output is an 8-limb digest
bound by digest[i] = compress2.In[8+i] + compress2.Out[8+i].
- poseidon2 (width-16) gets a Register variant alongside BuildModule,
matching the friround / poseidon2sponge composition pattern. nodehash
registers two Poseidon2 sub-groups in the same module via Register.
Each gadget cross-checks its digest against the native hasher for 1 and
4 random inputs, and rejects both input-witness tampering and direct
digest tampering.
Together these two gadgets cover the leaf-level and node-level of FRI
Merkle path verification — the next step is to wire them into the
existing gadgets/merkle path traversal so the hash-equality TODO in
merkle/constraints.go can be closed.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The merkle gadget previously had a TODO: it verified bit-selector logic
and inter-row chaining but trusted the trace to fill the parent column
with the correct HashNode output. A malicious prover could claim any
parent and the path would still verify.
This commit wires the new nodehash gadget into each row of the merkle
module:
- gadgets/merkle/constraints.go: after the bit-selector and chaining
constraints, register nodehash.Register with the row's (left, right)
column names. Add a per-row equality constraint
parent[i] == nodehash.Digest[i]
binding every parent to the true Poseidon2-MD HashNode output.
- gadgets/merkle/trace.go: extended to fill the two Poseidon2 sub-
groups (via nodehash.BuildCompressInputs + poseidon2.GenerateTrace)
and the digest columns.
- New negative test TestMerkleGadgetRejectsForgedParent flips a parent
limb while leaving the nodehash sub-trace honest; the hash-equality
constraint now catches what the chain alone couldn't.
The four existing merkle tests continue to pass — the new constraint
is strictly additive, the chain just got stronger.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The merkle gadget previously treated the leaf at row 0 as a free witness: the prover could supply any 8-limb digest there and the path would verify if the rest of the trace was self-consistent. The leaf had to be tied to actual opening data externally. This commit wires the leafhash gadget into the merkle module so the leaf is now constrained to equal leafhash.Digest(LeafP, LeafQ): - gadgets/merkle/columns.go: LeafP / LeafQ column-name helpers, updated package doc. - gadgets/merkle/constraints.go: ColumnNames now exposes LeafP, LeafQ, and LeafHash. BuildModule calls leafhash.RegisterExtLeafHash inside the module and AssertZeroAt(current[i] - LeafHash.Digest[i], 0) binds the leaf at row 0. (Leafhash sub-columns apply at every row; only row 0's digest equality is gated by the Lagrange selector — leafP/leafQ at non-leaf rows can be arbitrary self-consistent values.) - gadgets/merkle/trace.go: Path replaces Leaf with (LeafP, LeafQ); the leaf digest is computed natively via Poseidon2LeafHasher and flows through current at row 0. The leafhash sub-columns are populated by reusing the row-0 (LeafP, LeafQ) values across every row. - Tests rewritten to generate ext-pair leaves and build the native Merkle tree over Poseidon2LeafHasher.HashLeaf outputs. A new negative test TestMerkleGadgetRejectsBadLeafP confirms LeafP tampering at row 0 is caught. The merkle gadget now verifies the FULL path: (LeafP, LeafQ) → leaf digest → up the tree → root. Closes the gap between FRI openings and Merkle commitments end-to-end in the recursion gadget toolbox. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Integration test combining every FRI-side gadget the recursion package
delivers so far:
- friround (per-round) for the fold equation + in-circuit xInv derivation
- frichain for cross-round chaining + bit inheritance
- idxselect for finalPoly[base_last] match at the last round
- merkle (one per layer) for the Merkle path of each opened (LeafP, LeafQ)
pair, leaf-bound via leafhash and node-bound via nodehash
The test:
1. Generates a real native FRI commit phase (N=16, D=4, numRounds=2,
NumQueries=2 to avoid alpha-pinning padding).
2. Builds a verifier program with one fri_verify module + numRounds
merkle modules (one per FRI layer).
3. Replays the proof through the in-circuit verifier; the prover
accepts the trace and the verifier accepts the proof.
4. Confirms each merkle module's last real-step parent equals the
layer's committed root (i.e. the leaf opening verifies all the way
up to a public-input root).
Caveat documented in the test: friround's per-row P/Q values and the
matching merkle's row-0 LeafP/LeafQ are linked only by trace fill —
not by an in-circuit constraint. Adding a cross-module lookup or
permutation argument so a malicious prover cannot fill the two
inconsistently is the next wiring step.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
ExposeIthValueCtx has a Module field used by the prover step (ExposeIthValue reads pg.Modules[_ctx.Module] to size the sparse column it registers in the trace). The AddExposeIthValueStep helper forgot to set it, so the prover panicked with "index out of range" at execution time. The companion helper AddExposeRelativeIthValueStep sets its Module field correctly; this brings AddExposeIthValueStep in line. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The end-to-end test now wires friround's row-0 (P, Q) to merkle's
row-0 (LeafP, LeafQ) using Loom's exposed-values mechanism:
builder.AddExposeIthValueStep("fri_verify",
expr.Col(friGroups[j].P[i]), exposeName("P", j, i), 0)
merkleMod.AssertEqualAt(
expr.Col(merkleCNs[j].LeafP[i]),
expr.Exposed(exposeName("P", j, i)), 0)
The prover step seeds the exposed value from friround's row-0 P limb;
both modules then constrain their respective columns at row 0 against
that single shared value. A malicious prover that fills friround and
merkle inconsistently is caught — either at friround's
AssertEqualAt(P[i], Exposed(...)) or at merkle's
AssertEqualAt(LeafP[i], Exposed(...)).
Constraint: Loom's verifier reconstructs an exposed value's zeta
evaluation using each consuming module's N. For cross-module sharing
to be sound, all consumers must agree on N. The test pads fri_verify
(NumQueries=4) and both merkle modules (capacity=4) to the same
universalN=4. A real verifier with mixed-N modules would either pad
the same way or replace this binding with a cross-module lookup.
A new negative test TestEndToEndFRIVerifierRejectsCrossModuleMismatch
tampers merkle layer 0's LeafP[0] independently of friround's P_0;
verification fails on the new exposed-value constraint.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
In-circuit equivalent of dag.EvalExt — given the inner program's
vanishing-relation DAG and an E4Expr per leaf (holding the column's
value at zeta), produces an E4Expr that evaluates to V(zeta) at the
challenge point.
Two helpers:
- EvalDAG: topological walk over dag.DAG.Nodes building per-node
E4Expr via extfield Add/Sub/Mul/Pow. Caches results so each shared
sub-expression contributes one node.
- PowExt: zeta^n via square-and-multiply (E4Expr level). Works
inline without intermediate witnesses, so the constraint degree
grows with n; tests cover n ∈ {0..16} which stay fast. Production
use with module N >> 32 will require materializing per-step
squarings as witness columns (TODO comment).
Tests build small DAGs (leaf, Add/Sub/Mul, Pow, Fibonacci-style,
constants) and verify that gadget eval matches native dag.EvalExt
bit-for-bit by asserting the gadget's E4Expr equals a witness column
seeded with the native result.
This is the building block for the full AIR-at-zeta check
V(zeta) == (zeta^N - 1) * Q(zeta)
which will be the next milestone — Q(zeta) reconstruction from chunk
columns + the equality assertion.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Builds on EvalDAG + PowExt to encode the per-module check V(zeta) == (zeta^N - 1) * Q(zeta) which closes the inner-program vanishing-relation gap for the recursive verifier. RegisterAIRCheck takes: - mod, the verifier module to attach constraints to - d, the inner module's vanishing-relation DAG - N, the inner module's size - leafValues, column-at-zeta E4Expr per leaf - zeta, the FS challenge E4Expr - chunks, per-AIR-quotient-chunk E4Expr at zeta and emits 4 equality constraints (one per E4 limb), with Q(zeta) reconstructed inline as sum_i chunks[i] * (zeta^N)^i. Tests cover the happy path (synthetic V matches the RHS) and a corruption case (random V at fixed Q is rejected). Constraint degree grows with N (zeta^N is inlined); inner modules up to N ~ 16 stay fast — larger N will need materialized zeta-power columns, same pattern as binexp. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
In-circuit equivalents of the verifier's DEEP-bridge computation
(verifier.checkFRIBridge). Two primitives:
- RegisterDivExt(mod, prefix, num, denom): encodes E4 division as a
4-limb witness column constrained by result * denom == num. The
trace generator fills the witness with native num.Inverse(denom)*num.
This is the building block for every inverse the DEEP bridge needs
(the denominators (z_s - X) and (z_s + X) on the FRI query side).
- RegisterSummand(mod, prefix, v, C, z, X): convenience wrapper that
computes one DEEP-quotient summand (v - C) / (z - X) by combining
extfield subtraction with RegisterDivExt.
Tests cover:
- DivExt: 3 random pairs proved together; tampering with a quotient
limb is rejected.
- Summand: matches the native (v-C)/(z-X) formula bit-for-bit.
- Summand sum: simulates alpha-batching three columns into one
shift-group summand, the typical DEEP-bridge use pattern.
The full DEEP bridge wiring (assembling NumQueries × sizes × shifts
summands into DQ_P / DQ_Q and asserting equality against the FRI
proof's level-0 layer values) builds on these primitives. The
heaviest gadget in the toolbox by line count, but composed of small
reusable pieces.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
In-circuit equivalent of Loom's native FS transcript single-challenge
computation. Builds on poseidon2sponge (the width-24 Poseidon2 gadget)
and adds the cross-row absorb-overwrite + capacity-carry constraints
that the sponge needs to chain consecutive permutations.
API:
challenger24.BuildModule(builder, name, []expr.Expr) ColumnNames
Creates a dedicated module with N = nextPow2(ceil(len/Rate))
rows; row k absorbs the k-th input chunk (overwriting state
[0..len(chunk)-1]) and inherits state[len(chunk)..23] from
row k-1's permutation output (Rot by -1). Row 0 starts from
the zero state. Returns ColumnNames including:
- Sponge: the underlying poseidon2sponge.ColumnNames
- Digest: the 8 limb column names
- DigestRow: the row where the final digest lives
challenger24.GenerateTrace(cn, []koalabear.Element)
Runs the native Poseidon2 sponge step-by-step on the inputs
and returns the (cols, digest). Caller merges cols into the
global trace.
Padding rows beyond nPerms replay an extra all-zero-input
permutation continuation, satisfying every constraint that only
applies at the real rows via AssertEqualAt.
Tests cover:
- Single-permutation (12 < Rate=16 inputs)
- Two-permutation (20 inputs)
- Exactly-Rate (16 inputs, full block, no partial)
- Tampered-digest rejection
All cross-check the gadget's digest against Loom's native
hash.Poseidon2SpongeHasher bit-for-bit.
This is the width-24 counterpart of the earlier width-16
gadgets/challenger draft; the M1 width-16 version was a structural
placeholder and is now superseded for FS use by this gadget.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
First real implementation of buildVerifierCore. The recursive verifier
produced by this stage attests to the AIR-at-zeta relation
V(zeta) == (zeta^N - 1) * Q(zeta)
for every module of the inner program. FRI, Merkle openings, DEEP
bridge, and in-circuit Fiat-Shamir are not yet enforced — those layer
in subsequent stages.
Flow:
1. replayInnerFS mirrors verifier.newVerifierRuntime + .deriveChallenges
natively to derive zeta from the inner proof's commitments (and
every canonical round challenge value).
2. collectLeafValuesAtZeta walks each inner module's DAG and resolves
every leaf-at-zeta. Committed / Rotated / Challenge come directly
from proof.ValuesAtZeta; Lagrange is computed via
poly.LagrangeAtZetaExt. PublicInput and Exposed return errors
(Stage 2+ TODO).
3. A single outer "airverify" module of size N=2 carries every
witness column (zeta + per-leaf E4 + per-chunk E4) and registers
airzeta.RegisterAIRCheck per inner module.
4. The trace is filled with the resolved values; the prover compiles
and proves the outer program; the verifier checks it.
Tests:
- TestBuildVerifierCoreAIROnlyEquality: tiny A==B inner program at
N=4, proves natively, wraps via buildVerifierCore, prove+verify
outer succeeds.
- TestBuildVerifierCoreRejectsBadInnerProof: tampering one
ValueAtZeta in the inner proof yields an outer program whose
prove-or-verify fails — the AIR constraint detects the lie.
Scope limit: the inner program currently must use only Committed /
Rotated / Challenge / Lagrange / Constant leaves. PublicInput and
Exposed support comes next.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…bonacci
Extends Stage-1 (committed/rotated/challenge/Lagrange-only) to cover
the remaining leaf kinds, enabling recursion of real Loom programs.
- inputs.go: RecursionInput now carries PublicInputs (public.Inputs)
alongside Program + Proof. Required so the recursive verifier can
bind the inner statement's public values to its FS replay and
resolve PublicInputColumn leaves at zeta.
- verifier_core.go:
- replayInnerFS now binds PublicInputs.TranscriptElements() to the
initial challenge when non-empty, matching the inner verifier.
- collectLeafValuesAtZeta resolves PublicInputColumn leaves by
Lagrange-summing the statement's public-input Entries, and
ExposedColumn leaves by Lagrange-summing proof.ExposedValues
Entries. New helpers reconstructFromEntries, publicInputEntries,
exposedEntries.
- Tests (5 total now passing):
- TestBuildVerifierCoreFibonacci wraps the canonical 4-row
Fibonacci program (with Lagrange leaves from AssertZeroExceptAt).
- TestBuildVerifierCoreWithExposedValues exposes A's last entry
via AddExposeLastEntryStep; the gadget reconstructs the exposed
value at zeta.
- TestBuildVerifierCoreWithPublicInputs uses an expr.PublicInput
leaf pinned to a verifier-supplied value at row 0.
What's still unsound (next stages):
- zeta is replayed natively; not yet derived in-circuit via FS.
- The recursive verifier doesn't yet check FRI, Merkle openings,
or the DEEP-quotient bridge — those require composing the
existing per-piece gadgets into the outer Program.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…hain
Closes the first soundness gap: zeta is no longer a trusted witness
column filled from the native FS replay. It's now derived in-circuit
by a chain of width-24 Poseidon2 sponges that mirror the inner
proof's Fiat-Shamir transcript.
Architecture:
- One outer "airverify" module of size N = nextPow2(total sponge
permutations across the chain).
- For each FS challenge in the inner proof's chain (canonical_<r>
rounds followed by __zeta), register a challenger24.RegisterAt
sponge starting at the next free row. Each sponge resets state to
zero (matching the native Transcript.ComputeChallenge per-challenge
reset).
- The previous-challenge digest is wired into the next sponge's
chunk_0 via expr.Rot(prev_digest_col, -1) — at the new sponge's
start row, Rot -1 references the previous sponge's digest row.
- The AIR check (per inner module) uses the final sponge's digest as
zeta, and is gated to the digest row via RegisterAIRCheckAtRow.
New helpers:
- gadgets/airzeta.RegisterAIRCheckAtRow + buildAIRRelations split out
so the limb-equality constraints can be applied at a specific row
via AssertZeroAt (used when zeta only has its real value at one
row of the trace).
- gadgets/challenger24.RegisterAt + StartRow on ColumnNames let
multiple sponges share one module at non-overlapping row ranges.
GenerateTraceWithSize now respects StartRow when filling sub-trace
columns.
- computeChallengeChain replays the inner FS transcript to build,
for every challenge, the absorbed-element sequence + digest, with
PrevDigestStart marking where the previous digest goes (constrained
to fit in chunk_0).
The 5 existing buildVerifierCore tests (equality, Fibonacci, exposed,
public-inputs, negative) all pass with this stronger verifier. The
trace's zeta value is no longer free for a malicious prover to choose
— it's the unique sponge output of the inner proof's commitment chain.
Remaining gaps (next stages):
- inner witness values at zeta are still trusted (need FRI
verification in-circuit + Merkle openings + DEEP bridge).
- DEEP_ALPHA and later challenges aren't yet in the chain.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Extends the in-circuit FS chain past zeta to also derive DEEP_ALPHA.
The chain is now:
canonical_<r> (per FS round) -> __zeta -> alpha_DEEP
Each step is a width-24 Poseidon2 sponge in the airverify module,
chained via the prev-digest Rot wiring established in Stage 3.
DEEP_ALPHA bindings are the inner proof's at-zeta values that drive
the DEEP quotient — pulled from input.Proof.ValueAtZetaExt for every
(key, chunk) pair in the prover.DEEPquotientLayout. Bindings remain
constants (extracted from input.Proof) at this stage; they'll be
promoted to witness column references once FRI verification consumes
alpha and we need a malicious prover to not be able to lie about the
inner at-zeta values.
verifier_core.go changes:
- computeChallengeChain now registers DEEP_ALPHA, binds every
Keys/AIRChunks entry of dqLayout, and adds a final chain step.
- buildVerifierCore locates the zeta step in the chain (no longer
the last) for the AIR check and the sanity check.
- Helper extToElements mirrors prover.extToElements for the limb
order Loom's FS uses for E4 bindings.
All 5 existing buildVerifierCore tests still pass. DEEP_ALPHA's
digest is computed in-circuit and ready to be consumed by FRI
verification (next stage).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…itness refs
Promotes DEEP_ALPHA's per-key bindings from constants (baked at
outer-circuit-build time) to expr.Col references over the airverify
module's witness columns. The AIR check and the DEEP_ALPHA sponge
now read the inner at-zeta values from the SAME in-circuit source:
any tampering propagates through both checks consistently, and a
future FRI integration can tie a single witness to its committed
polynomial.
Implementation:
- challengeStep gains a WitnessBindings []witnessBinding field
identifying which 4-element slices of NativeInputs should be
resolved to in-circuit witness columns. computeChallengeChain
populates them for the DEEP_ALPHA step by walking
BuildDeepQuotientLayout's Keys + AIRChunks.
- buildVerifierCore restructured into a pre-pass that allocates
airverify witness columns first (populating per-key column-name
maps keyToLeafCols / keyToChunkCols), then registers the sponges
with witness-ref substitution at the bindings positions, then
registers the AIR checks using the pre-allocated leaf/chunk
expressions.
- The extToElements limb order {B0.A0, B0.A1, B1.A0, B1.A1} is
re-mapped to extfield's {B0.A0, B1.A0, B0.A1, B1.A1} via the
permutation {0, 2, 1, 3}.
Tests: all 5 existing + 1 new
TestBuildVerifierCoreRejectsAtZetaTamperingViaDeepAlpha that tampers
B at zeta and confirms the recursive verifier still rejects (covered
in Stage 4 by the AIR check alone; in Stage 5 it's caught by both
that AND the DEEP_ALPHA derivation reading the same witness).
This is a structural step toward FRI integration: with at-zeta
values now firmly anchored in one set of witness columns, the next
stage can wire FRI verification to bind those same witnesses to the
inner polynomial commitments via Merkle openings + DEEP bridge.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…fri_fold_0
When the inner proof carries FRI data (DeepQuotientCommitment
non-empty), the FS chain in airverify now extends past DEEP_ALPHA to
include fri_fold_0 — the first FRI fold challenge, bound to the
level-0 DEEP-quotient root.
This validates the chain machinery handles FRI-style bindings (FRI
roots from the inner proof, beyond the trace + AIR roots covered by
canonical_r and zeta). The rest of the FRI challenges (fri_fold_j
for j > 0, fri_level_l_gamma, fri_query_k) follow the same pattern
and will land in subsequent commits.
verifier_core.go changes:
- hasFRI flag detects FRI presence via DeepQuotientCommitment.
- When set, fri_fold_0 is registered, bound to
DeepQuotientCommitment[0], and appended to the challengeNames
list — naturally picking up the rest of the chain machinery.
- friFoldName / friLevelGammaName / friQueryName helpers
duplicate fri's unexported challenge-name format strings.
New test TestBuildVerifierCoreNonSkipFRI runs the inner Prove
WITHOUT prover.SkipFRI(), confirming:
- The inner proof actually carries FRI commitments.
- buildVerifierCore extends the chain through fri_fold_0.
- The outer prove+verify (still SkipFRI) succeeds.
All 7 existing buildVerifierCore tests still pass; the new
non-SkipFRI test adds ~4s for inner FRI proving. The recursive
verifier still only checks the AIR relation in-circuit; FRI
verification itself remains the next milestone.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…l FRI challenges
Extends Stage 6 to cover every FS challenge in Loom's FRI verifier:
fri_fold_0
for j in 1..friNumRounds-1:
(fri_level_l_gamma)?
fri_fold_j
fri_query_0 .. fri_query_{NUM_QUERIES-1}
Bindings:
- fri_fold_0 : DeepQuotientCommitment[0] (T_0 root)
- fri_fold_j (j > 0) : DeepQuotientFriProof.FRIRoots[j-1] (T_j root)
- fri_level_l_gamma : DeepQuotientCommitment[l] (level-l root)
- fri_query_0 : transcript_ext_poly(FinalPolyExt) (or base variant)
- fri_query_k (k > 0) : previous query's just-computed digest (DYNAMIC)
The dynamic query binding required restructuring the step loop:
each fri_query_k for k > 0 now reads steps[i-1].NativeDigest (the
previous query's digest) and binds it to fs BEFORE computing this
challenge — matching fri.Prove's interleaved bind+compute pattern.
verifier_core.go additions:
- friNumRounds + levelAtRound derivation (mirrors fri.Verify).
- All FRI challenge registrations + static bindings.
- parseQueryK helper for the dynamic query-chain check.
- log2int helper.
- transcriptBasePolyElements / transcriptExtPolyElements
(duplicating fri's unexported encoding helpers).
- field package import for FinalField branch.
The non-SkipFRI test (TestBuildVerifierCoreNonSkipFRI) now exercises
a chain of: canonical_0, __zeta, alpha_DEEP, fri_fold_0, fri_fold_1,
fri_query_0..3 = 8 sponges, with the per-step native cross-check
validating each digest against fs.ComputeChallenge.
Remaining for full FRI soundness:
- Wire FRI fold verification per query (using the now-in-circuit
alphas, gammas, query positions).
- Wire per-layer Merkle openings.
- Wire DEEP bridge connecting FRI level-0 evaluations to airverify
witness columns.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds TestBuildVerifierCoreNonSkipFRIFibonacci to exercise the full FS chain (canonical_0, __zeta, alpha_DEEP, fri_fold_j, fri_query_k) on a Fibonacci inner program, complementing the equality-program variant. Confirms the chain reconstruction holds across the Lagrange-leaf rotation pattern of AssertZeroExceptAt. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Renames buildVerifierCore -> BuildVerifierCore so callers outside the
recursion package (benchmarks, future aggregation drivers) can build a
verifier circuit from an (innerProgram, innerProof) pair.
Adds verifier_core_bench_test.go covering the full pipeline:
- BenchmarkInnerBuild board.Compile on the inner program
- BenchmarkInnerProve prover.Prove on the inner program
- BenchmarkRecursionBuild BuildVerifierCore
- BenchmarkRecursionProve prover.Prove on the outer (recursion) program
- BenchmarkRecursionVerify verifier.Verify on the outer proof
All five report time + memory via b.ReportAllocs(). Inner is a Fibonacci
4-row program (representative of the small-trace recursion target).
Initial numbers on AMD Ryzen 9 7940HS (count=3, benchstat geomean):
sec/op B/op allocs/op
InnerBuild 18.27 µ 13.97 KiB 233
InnerProve 138.6 µ 55.73 KiB 798
RecursionBuild 1.978 s 723.6 MiB 7.32 M
RecursionProve 198.0 m 113.0 MiB 1.05 M
RecursionVerify 6.198 m 4.626 MiB 1.04 k
RecursionBuild is the clear hotspot — 100x the cost of RecursionProve.
Likely the airzeta DAG-eval expression blowup; future work.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two compounding hotspots in BuildVerifierCore on multi-module inner
proofs (sizes 64/32/16/8, non-SkipFRI):
1. airzeta.PowExt(zeta, N) inlined a degree-N polynomial in zeta's
four limbs. Each E4 squaring roughly squares the per-limb
expression size, so by N=16 the constraint tree has billions of
nodes. Materialize a chain zeta^(2^i) for i=1..log2(maxN) as
witness columns constrained via Square at the __zeta digest row,
then look up the right power per inner module. Each module pays
one cheap E4Expr.Col reference instead of an exponential tree.
2. expr.(*Leaf).Pow(n) for n>2 expanded into squareAndMultiply, which
Clones the running result on every squaring step. expr.Fold over
M relations calls Pow(alpha, 0..M-1), so the total Clone work is
O(sum_i i) = O(M^2). For airverify (thousands of relations from
the sponge chain), this dwarfed everything else. Leaf nodes are
atomic — pruneSearch's case *Leaf explicitly returns nil — so the
Clone-cascade guarding against in-place rewrites is unnecessary
when the base is a Leaf. Always return Pow{leaf, n} instead.
Bench (count=3, AMD Ryzen 9 7940HS):
Before After Speedup
Small / RecursionBuild
time 2.07 s 31.3 ms 66x
memory 754 MB 22.7 MiB 33x
allocs 7.24 M 356 k 20x
Large (sizes 64/32/16/8, non-SkipFRI) / RecursionBuild
time 120 s 189 ms 635x
memory 98 GB 132 MiB 760x
allocs 753 M 1.89 M 400x
Large / RecursionProve
time — (uncaptured) 2.24 s
memory — 594 MiB
allocs — 5.76 M
Large / RecursionVerify
time — (uncaptured) 46.9 ms
memory — 33.2 MiB
allocs — 5.19 k
The expr.(*Leaf).Pow change is shared with the rest of Loom — the
full ./... test suite still passes.
Bench file gained a Small / Large parameterization and a
multi-module Fibonacci inner (sizes 64/32/16/8) so the recursion
verifier now exercises multi-level FRI folding rather than the toy
single-row case.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds a row-gated variant of bits.Register that binds against an existing column (provided by name) and applies its constraints via AssertZeroAt(rowIdx) instead of every row. Two tests cover the happy path and a bit-corruption case at the gated row. Motivation: BuildVerifierCore needs to crack open fri_query_k digest limbs to extract the query position s_k. The digest column already lives in airverify (no new column to allocate), and the decomposition only needs to hold at the sponge's digest row. The doc comment notes the Koalabear corner case: for value < 2^24 - 1 the field constraint admits two 31-bit representations (value and value + p). Probability ~2^-7 per query; acceptable for an initial verifier and matches the lenience taken elsewhere in the FRI stack. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
For each FRI query k, verify that the last fold's output equals
finalPoly[s_k mod len(finalPoly)] — the FRI verifier's final-round
check (internal/fri/fri.go checkQueryExt) realised in-circuit:
1. Decompose fri_query_k's digest[1] into 31 bits via bits.RegisterAt
at the sponge's digest row. The lowest 2 bits give
base_last_k = s_k mod len(finalPoly).
2. Anchor alpha_last (the last fri_fold_{r-1} challenge) by adding a
constant-valued 4-limb E4 column and constraining it to equal the
chain digest at the fri_fold_{r-1} sponge's digest row — same
pattern as the zeta^N witness chain.
3. Per query, allocate trusted LeafP/LeafQ witnesses for the last
fold round (Merkle verification of these leaves is future work).
4. Inline a 4-element E4 mux over (b0 + 2*b1) for xInv = omega^{-i}
and finalPoly[i], compute expected via the standard fold equation
(P+Q)/2 + alpha*(P-Q)*invTwo*xInv, and AssertZeroAt(expected ==
finalPoly_at_base) at the query's digest row.
Stage-gated to fire only when the inner proof carries FRI data
(len(DeepQuotientCommitment) > 0) — SkipFRI workloads are unaffected.
Tests:
- existing TestBuildVerifierCoreNonSkipFRI{,Fibonacci} now also
exercise the final-poly constraints (still pass).
- TestBuildVerifierCoreRejectsBadFRILeaf — flipping LeafPExt at the
last fold round, query 0, breaks the final-poly equation and the
outer verifier rejects.
Bench cost (Large workload, RecursionBuild):
before: 189 ms / 132 MiB / 1.88M allocs
after: 192 ms / 138 MiB / 1.90M allocs
(≈+1.5% time, +5 MiB memory — negligible.)
Soundness note: limited to len(finalPoly)=4 for now (inline mux is
hardcoded to 2-bit indexing). The 31-bit decomposition of digest[1]
has the ~2^-7 Koalabear corner case noted on bits.RegisterAt.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Generalises the Stage 8 final-poly match to every fold round. For each
query k and round j in 0..numRounds-1:
expected_jk = (P+Q)/2 + alpha_j * (P-Q) * invTwo * xInv
is compared to:
- selected leaf at round j+1 (P or Q, picked by the top bit of
base_jk = lowest log2(N_j/2) bits of s_k) when j < numRounds-1, or
- finalPoly[base_last_k] when j = numRounds-1 (existing Stage 8).
Key mechanics:
- Every alpha_j is anchored to its fri_fold_j chain digest at the
sponge's digest row (same pattern as alpha_last in Stage 8 and the
zeta^N witness chain). Off-row the witness columns hold the
constant alpha_j so cross-row references are cheap.
- xInv = omega_j^{-base_jk} is computed by binexp.Register over the
lowest numBaseBits of fri_query_k's 31-bit digest[1] decomposition,
avoiding the 2^numBaseBits-wide constant table the inline mux
would need at large rounds.
- Per (round, query) trusted LeafP/LeafQ are still witnesses; Merkle
openings are the next stage.
A new regression test, TestBuildVerifierCoreRejectsBadFRILeafMidRound,
tampers LeafPExt at round 0 of a 2-round Fibonacci inner proof — the
final-poly check would NOT catch this, but the new cross-round
constraint does.
Cost (Large workload, RecursionBuild):
stage 8: 192 ms / 138 MiB / 1.90 M allocs
stage 9: 194 ms / 147 MiB / 1.94 M allocs
(≈+1% time, +7% memory for adding 6×4=24 cross-round constraints
plus binexp running products across all rounds.)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
For each FRI fold round j (j = 0..numRounds-1) of query 0, build a
separate merkle module (gadgets/merkle) of N = airverify.N. The
module:
- Cross-binds row-0 (LeafP, LeafQ) to the matching
airverify.fri_q0_P_{j} / airverify.fri_q0_Q_{j} witnesses via
AddExposeIthValueStep + expr.Exposed. Same-N reconstruction at
zeta makes the cross-module exposed values consistent.
- Constrains parent[i] at the top-real row (= path depth - 1) to
equal the FRI commitment root for round j: round 0 uses
DeepQuotientCommitment[0]; rounds j>0 use FRIRoots[j-1] — the
same roots already bound into fri_fold_j sponge inputs in the
chain extension.
Together this forces the leaves used in the Stage 9 fold chain to
live in the prover's committed Merkle tree, closing the Stage 9
"trusted LeafP/LeafQ" gap (for query 0).
New regression test: TestBuildVerifierCoreRejectsBadMerkleSibling
tampers a sibling at query 0 round 0. The fold-chain checks never
consume sibling digests, so only the new Merkle verification can
catch it — confirming the stage is actively soundness-relevant, not
piggybacking on earlier layers.
Multi-degree FRI carve-out: when input.Proof.DeepQuotientFriProof
has non-empty LevelQueries (level intros present, e.g. the Large
bench's 64/32/16/8 inner), the Stage 9 cross-round chain constraint
is skipped — the native fold equation at level-intro rounds is
expected_jk + gamma_l * level_leaf == leaf_at_j+1, which the
current chain implementation does not yet model. Final-poly match,
alpha/leaf witnesses, and the new Merkle bindings still apply;
gamma anchoring + level-leaf witnessing is the next stage.
Bench (count=1, AMD Ryzen 9 7940HS), Large workload only:
stage 9 → stage 10
RecursionBuild 194 ms → 318 ms (+64%)
RecursionProve 2.24 s → 2.48 s (+11%)
RecursionVerify 47 ms → 78 ms (+66%)
The added cost comes from 6 merkle modules per outer build, each
with two width-16 Poseidon2 permutations per row and a width-24
sponge for the leaf hash — substantial but localised; future stages
that scale Merkle to all 4 queries should expect a comparable
multiplier.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
For each FRI query q, the verifier reconstructs DQ(omega^sL) and
DQ(-omega^sL) from the AIR-at-zeta values, alpha (DEEP_ALPHA), and
per-bare-column raw samples at the query position, then equates these
to the FRI level-0 layer's (LeafPExt, LeafQExt) — already Stage-9
witnesses and Stage-10 Merkle-bound to the level-0 root for query 0.
Math (single-size = dqLayout.Sizes[0]):
For each shift group j in dqLayout.Shifts[0]:
z_s = zeta * omega_size^shift_j
v_s = sum_k evalAtZ_k * alpha^k
C_X = sum_k sampleP_k * alpha^k
C_negX = sum_k sampleQ_k * alpha^k
DQ_P += (v_s - C_X) * inv(z_s - X)
DQ_Q += (v_s - C_negX) * inv(z_s + X)
AIR-chunks: identical with shift = 0, omega^shift = 1.
X = omega_{N_fri}^sL where sL = digest[1] mod (N_fri/2).
Implementation highlights:
- A separate `zeta_const` 4-limb witness anchored to the __zeta chain
sponge digest at chCN.DigestRow. The existing zetaExpr only holds
the correct value at chCN.DigestRow; the bridge needs zeta usable
at the query digest row, hence the new anchor.
- DEEP_ALPHA anchored to its chain sponge digest at deepAlphaCN's
digest row (mirrors alpha_j / zeta_const).
- alpha^k chain materialized as constant-fill witnesses with
recurrence alpha^k = alpha^{k-1} * alpha (cheap O(K) muls instead
of inline tree blowup).
- X = friDomainGen^sL via binexp.Register over the lowest
log2(N_fri/2) bits of fri_query_q's 31-bit digest[1] decomposition.
- sampleP/sampleQ are trusted constant-fill witnesses filled from
input.Proof.PointSamplings via prover.BuildLayout's
ColSlot / AIRChunkSlot. Per-column Merkle openings are a future
stage.
- 1/(z_s - X), 1/(z_s + X) are witness E4 inverses constrained by
inv * denom = 1 at the query row.
Carve-outs:
- Multi-degree FRI (len(LevelQueries) > 0): skipped. The bridge
requires per-level DEEP quotients and gamma anchoring.
- len(dqLayout.Sizes) > 1: skipped. Same reason.
Tests:
- The four existing non-SkipFRI tests now also exercise Stage 11.
All still pass.
- TestBuildVerifierCoreRejectsBadColumnSample tampers a base-rail
RawLeaf in PointSamplings. Stages 8/9/10 don't reference these
samples; only the bridge does. The outer verifier rejects.
Cost: bench numbers unchanged because the Large workload has
LevelQueries non-empty (gated off), and Small is SkipFRI (no FRI
checks at all). Stage 11 fires only on single-size, non-SkipFRI
inner proofs — covered by the four buildVerifierCore non-SkipFRI
tests, which still complete in ~1.2 s each.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Bind sampleP/Q witnesses introduced in Stage 11 (the DEEP bridge) to
the prover's committed Merkle trees. For each commitment tree t and
each FRI query q the verifier:
1. Builds a multi-pair leaf hash in airverify that absorbs the
sample columns belonging to t (base pairs first in PolyIdx
order, then ext pairs, mirroring native HashLeaf).
2. Exposes the 8 digest limbs from airverify.
3. Builds a new merkle module (no internal leafhash) of N =
airverify.N. Current[i] at row 0 is bound to the exposed
digest; Parent[i] at depth-1 is bound to the tree's committed
root (constants from proof.Commitments).
Gadget additions:
- leafhash.RegisterFlexibleLeafHash takes nbBase base pairs and
nbExt ext pairs and absorbs them into one width-24 Poseidon2
sponge — sponge limb permutation matches the native WriteExt
layout via SpongeLimbOrder.
- merkle.BuildModuleNoLeafHash: same bit / selector / chain /
node-hash constraints as BuildModule, but omits the internal
ext leafhash and leaves Current[0] for the caller to bind.
- merkle.GenerateTraceWithDigest: trace generator for the new
variant, takes the leaf DIGEST directly.
Tree-fit gate: single-block absorption only (input ≤ sponge rate
of 16 elements). For the Fibonacci(n=4) inner this covers the
trace tree (3 base pairs = 9 elements) but skips the AIR-quotient
tree (2 ext pairs = 19 elements > 16). The DEEP bridge equation
still cross-checks those untrusted chunk samples indirectly. A
multi-absorption leafhash variant unlocks the AIR-chunk and
larger-program cases — explicit next-stage work.
Tests:
- All ten existing BuildVerifierCore tests still pass.
- New TestBuildVerifierCoreRejectsBadColumnTreeSibling tampers a
sibling digest in PointSamplings[0][0].Proof. Stages 8/9 never
read column-tree siblings; Stages 10/11 see different
commitments — only Stage 12 catches it. The outer verifier
rejects.
Stage 11's existing TestBuildVerifierCoreRejectsBadColumnSample
remains valid (it tampers a RawLeafBase value; with Stage 12 the
trace becomes self-inconsistent two ways — the bridge equation
AND the column-tree Merkle binding — and either failure rejects).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…trees
leafhash.RegisterFlexibleLeafHash now chains arbitrarily many
Poseidon2 width-24 / rate-16 sponge sub-modules instead of capping
at one absorption block. Per block i:
- state[0..15]: overwritten with input[16i..16i+15] when in range;
block 0 uses zero for unfilled slots; block i>0 carries those
slots from block (i-1).Post[NbRounds-1].
- state[16..23] (the capacity): zero for block 0, carried from
block (i-1) afterwards.
The final block's Post[NbRounds-1][0..7] is the leaf digest. New
helpers:
- FlexibleColumnNames replaces the single-sponge ColumnNames in
the multi-block path (kept distinct from ExtLeafHash's
ColumnNames so existing single-pair callers keep working).
- NumBlocksForFlexible(nbBase, nbExt) computes ceil(inputLen / 16).
- FlexibleLeafSpongeStates(leaf) replays the native sponge in
overwrite mode and returns the per-block 24-element INPUT state
so trace generation can call poseidon2sponge.GenerateTrace once
per block.
Stage 12 (BuildVerifierCore): removes the single-absorption gate.
The Fibonacci(n=4) inner's AIR-quotient tree (2 ext chunks, 19
sponge elements > 16-element rate) is now Merkle-verified end-to-
end alongside the trace tree.
New tests:
- TestFlexibleLeafHashMultiBlock builds an isolated 2-ext-pair
leaf hash and cross-checks the in-circuit digest against
commitment.Poseidon2LeafHasher.HashLeaf (gadget-level).
- TestBuildVerifierCoreRejectsBadAIRChunkSample tampers a
RawLeafExt entry on the AIR-quotient tree. Before this commit
the Stage-12 gate skipped that tree and the corruption could
sneak through; now the multi-block leafhash + Merkle catches
it. The outer verifier rejects.
Bench (Large) unchanged: that workload is multi-degree FRI so
Stage 11/12 stay gated off; benefit shows on the non-SkipFRI
single-size unit tests, which still complete in ~2-3 s each.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Extends the DEEP-quotient bridge to multi-size inner proofs (where
len(dqLayout.Sizes) > 1 and the FRI proof carries LevelQueries). For
each size i and query q the verifier reconstructs DQ_P_i(omega_i^sL_i)
and DQ_Q_i(-omega_i^sL_i) from the AIR-at-zeta values, alpha
(DEEP_ALPHA), and the per-size column / chunk samples at the query
position, then equates them to the matching FRI query leaf:
level 0 -> FRIQueries[q].Layers[0] (Stage 9 witnesses)
level i > 0 -> LevelQueries[i-1][q] (NEW witnesses)
Math is identical to the single-size bridge — same per-shift
accumulators, same denominators (z_s - X), same alpha^k chain (reset
to alpha^0 per size in the native verifier, so the same alphaPow
chain is reused starting at index 0 each iteration). The new bits
are:
- sLBits_i = log2(RATE * sizes[i] / 2). Each size pulls a different
slice of the lowest digest[1] bits via the binexp gadget.
- friDomainGen_i = Generator(RATE * sizes[i]) — different base for
each level's X computation.
- level i > 0 leaves are allocated as constant-fill 4-limb witness
columns from LevelQueries[i-1][q].LeafP/QExt and equated to the
in-circuit DQ_P_i / DQ_Q_i.
Lives in the `else` branch (LevelQueries non-empty); the single-size
path stays unchanged. Per-column Merkle openings for level i > 0
leaves and for the size-i samples are still trusted — those need
Merkle wiring against DeepQuotientCommitment[i] and the original
column trees at the appropriate level, follow-up stages.
Tests:
- New helper makeMultiSizeFibInner builds a 2-size (16, 8)
Fibonacci inner program — small enough for unit-test pace, large
enough to trigger multi-degree FRI.
- TestBuildVerifierCoreMultiDegreeNonSkipFRI proves and verifies
the full pipeline (inner + recursion build + outer prove + outer
verify) end-to-end with Stage 13 firing.
- TestBuildVerifierCoreRejectsBadLevelLeaf tampers
LevelQueries[0][0].LeafPExt. Pre-Stage-13 these leaves were
invisible to the circuit; with Stage 13 their values are pinned
by the bridge equation. Outer verifier rejects.
Bench (Large workload, sizes 64/32/16/8):
Stage 12 -> Stage 13 RecursionBuild 318 ms -> 434 ms (+36%)
memory 251 MiB -> 297 MiB (+18%)
allocs 3.36 M -> 3.80 M (+13%)
The increase is from the per-(query, size) DEEP bridge wiring —
4 sizes × 4 queries × (binexp + samples + inverses + accumulation)
on the Large workload (vs. only the single-size path firing on
Small / unit tests).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lifts Stage 12's tree-Merkle wiring into the multi-degree branch
(Stage 13). For each commitment tree t and FRI query q, the
verifier now:
1. Builds a flexible (multi-block) leafhash in airverify over the
sample witnesses Stage 13 allocates — base pairs first in
PolyIdx order, then ext pairs.
2. Exposes the 8 digest limbs.
3. Constructs a merkle module of N = airverify.N with no
internal leafhash; Current[0] cross-bound to the exposed
digest, top-real-row Parent constrained to the tree's root
from proof.Commitments[t].
Reuses the same colEntry / nativeLeafFor / nativeLeafDigestFor
helpers introduced for single-size Stage 12 and the same
post-AddModule wiring loop — only the sample-column naming
prefix changes (`airverify.deep_md_*` instead of `airverify.deep_*`).
All trees are covered (no single-absorption gate), via the
multi-block flexible leafhash from the previous commit.
Soundness gaps closed:
- Multi-size column-tree leaves at the FRI query positions are
now pinned to the prover's committed trees.
- AIR-quotient trees of any size (1+ ext chunks) are covered.
Still trusted on the multi-degree path:
- LevelQueries[i-1][q] leaves (Stage 13 equates them to DQ_i but
nothing yet binds them to a level commitment).
- Stage 9 cross-round fold chain (gated off for multi-degree —
needs gamma anchoring + level-leaf contribution).
Test: TestBuildVerifierCoreRejectsBadMultiDegreeColumnSibling
tampers a sibling digest on the multi-size inner's trace tree.
Stage 9 (gated off for multi-degree), Stage 10 (different tree),
Stage 11 (single-size only), Stage 13 bridge equation (uses
samples but not siblings) all miss it; only the new per-column
Merkle catches it. Outer verifier rejects.
Bench (Large workload — sizes 64/32/16/8 with non-SkipFRI):
Stage 13 -> Stage 12-MD RecursionBuild 434 ms -> 1.53 s
memory 297 MiB -> 1.04 GiB
allocs 3.80 M -> 13.4 M
RecursionVerify 85 ms -> 468 ms
Substantial cost — 8 merkle modules added per outer build (2
trees × 4 queries on this workload), each with a width-24
flexible-leafhash sponge chain plus the width-16 node-hash AIR.
Inflation tracks the heaviness of in-circuit Poseidon2; future
optimisation would batch / reuse trees rather than per-(tree,
query) modules.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
For each FRI level i > 0 and each query q, bind the LevelQueries[i-1][q]
leaf pair to the level-i commitment root (DeepQuotientCommitment[i])
via an in-circuit Merkle path verification. Closes the soundness gap
left by Stage 13: the multi-degree DEEP bridge equates DQ_i to the
level leaves, but those leaves were otherwise free witnesses until
now.
Mechanics (mirrors Stage 10's per-FRI-layer Merkle, just targeting
the level commitments):
1. For each (level i, query q): expose airverify's 8 level-leaf
limbs (Stage 13 already allocates them as
`airverify.deep_md_levelP/Q_{li}_{qi}_{limb}`).
2. Build a merkle module of N = airverify.N with its internal
single-ext-pair leafhash. Current[0] row-0 binds to the
exposed leaf limbs; top-real-row Parent binds to
DeepQuotientCommitment[i] constants.
3. Trace fill via the existing merkle.GenerateTrace, fed
LevelQueries[i-1][q].Path.
Tests:
- All existing tests still pass; the multi-degree pair
(TestBuildVerifierCoreMultiDegreeNonSkipFRI,
TestBuildVerifierCoreRejectsBadLevelLeaf) now also exercise
Stage 14 — the latter still rejects, now caught by both
Stage 13 (bridge equation) and Stage 14 (Merkle leaf binding).
- New TestBuildVerifierCoreRejectsBadLevelMerkleSibling
tampers a Path.Siblings entry on the level-1 path. Stage 13
only reads leaf values, not siblings — Stage 14 is the only
check that consumes them. Outer verifier rejects.
Bench (Large, sizes 64/32/16/8, 3 levels):
Stage 13+12-MD -> Stage 14
RecursionBuild 1.53 s -> 1.83 s (+20%)
memory 1.04 GiB -> 1.30 GiB (+25%)
allocs 13.4 M -> 16.3 M (+22%)
RecursionVerify 468 ms -> 533 ms (+14%)
Increment is the 12 new merkle modules added per outer build
(3 levels × 4 queries), each carrying a width-16 nodehash AIR
plus a width-24 single-ext-pair leafhash. Sharing or batching
across queries / levels is the next obvious performance target.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reinstates the cross-round fold chain for multi-degree FRI by adding
the gamma-weighted level-leaf term that Stage 9 left out when gating
itself off for multi-degree. For every query k and every non-final
round j the constraint becomes
expected_jk + (gamma_l * level_leaf_jk if level intro at j+1)
==
selected_jk = (1-topBit_j)*pNext + topBit_j*qNext
where level_leaf_jk = (1-topBit_j)*levelP + topBit_j*levelQ uses the
same top-bit selector that picks pNext/qNext, level l = mapping
log2(sizes[0]/sizes[l]) -> l, and gamma_l is the in-circuit
fri_level_l_gamma challenge anchored from the chain.
Mechanics (lives in the multi-degree else branch):
- Level leaves for l > 0 are now allocated up-front in a shared
`levelLeavesAll[l][q]` map; Stage 13's DEEP bridge consumes the
same map (one allocation instead of per-size duplication).
- levelAtRound is recomputed locally from dqLayout.Sizes (same
formula as computeChallengeChain).
- For each l > 0 the fri_level_l_gamma sponge digest is anchored
into a constant-fill 4-limb witness column via AssertZeroAt at
its digest row — same pattern as alpha_j / DEEP_ALPHA.
- The cross-round constraint reuses Stage 9's per-(round, query)
binexp xInv output by name (airverify.fri_q{k}_xInv_{j}.step_K),
avoiding any new binexp module registrations.
Tests:
- All multi-degree tests still pass; the new constraints fire
automatically on TestBuildVerifierCoreMultiDegreeNonSkipFRI.
- New TestBuildVerifierCoreRejectsBadMultiDegreeMidRoundLeaf
tampers FRIQueries[0].Layers[0].LeafPExt on the multi-size inner
proof. Stage 10's per-FRI-layer Merkle for query 0 already
constrains this leaf, so this test exercises *both* defenses
(Stage 10 and Stage 15 cross-round chain). Outer verifier
rejects.
Bench (Large, sizes 64/32/16/8, count=1):
Stage 14 -> Stage 15
RecursionBuild 1.83 s -> 1.83 s (no measurable change)
memory 1.30 GiB -> 1.31 GiB
allocs 16.3 M -> 16.3 M
RecursionVerify 533 ms -> 538 ms
Cost is negligible because Stage 15 reuses Stage 9's existing binexp
sub-modules and Stage 13's level-leaf witnesses; the new constraints
are pure expression-level equalities — no fresh Poseidon2.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The per-FRI-layer Merkle openings now cover every NUM_QUERIES query
instead of only query 0. For each query k in 0..NUM_QUERIES-1 and
each fold round j, the verifier builds a separate merkle module of
N = airverify.N with:
- row-0 LeafP/LeafQ cross-bound to airverify's
`fri_qk_P_{j}` / `fri_qk_Q_{j}` witnesses via expose / Exposed,
- top-real-row parent constrained to the FRI commitment root
(DeepQuotientCommitment[0] for round 0, FRIRoots[j-1] otherwise).
Closes the gap left by the original Stage 10 (query 0 only) — pre-
this commit, queries 1–3 had no Merkle binding on their per-layer
running-poly leaves, so a prover could lie about them and only get
caught by the cross-round fold chain or the DEEP bridge (both of
which constrain leaf VALUES, not the path).
Tests:
- All existing tests still pass. The single-size non-SkipFRI tests
now build 6 × NUM_QUERIES = 24 merkle modules per outer build
(was 6); the multi-degree non-SkipFRI tests similarly.
- New TestBuildVerifierCoreRejectsBadQuery1MerkleSibling tampers a
sibling at FRIQueries[1].Layers[0].Path.Siblings. Pre-this commit
this leaked through; the new constraint catches it. Outer
verifier rejects.
Bench (Large, sizes 64/32/16/8, count=1):
Stage 15 -> Stage 10-all-queries
RecursionBuild 1.83 s -> 2.19 s (+20%)
memory 1.31 GiB -> 1.66 GiB (+27%)
allocs 16.3 M -> 20.7 M (+27%)
RecursionVerify 538 ms -> 631 ms (+17%)
The +20% Build cost is the 18 additional merkle modules
(queries 1–3 across 6 rounds), each carrying its own width-16
nodehash AIR plus a single-ext-pair width-24 leafhash.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Replaces the hardcoded 2-bit e4Select4 mux in Stage 9's final-poly match with a tree-reduction selector e4SelectTree that handles any power-of-two len(finalPoly). The new helper mirrors the idxselect gadget's reduction loop but stays inline (no extra witness column allocations): at each level l the pairs (lo, hi) collapse via lo + bits[l] * (hi - lo), and after k = log2(len(finalPoly)) levels a single E4Expr remains. The previous baseLastBits != 2 gate is dropped; instead we check the table is a positive power of two within Koalabear's 31-bit range. Note on coverage: Loom's current FRI parameter convention (N = RATE * maxN, numRounds = log2(maxN)) gives len(finalPoly) = N / 2^numRounds = RATE = 4 for every program, so the new code path runs the same 2-bit reduction it always did. This commit is future-proofing — the moment Loom adjusts RATE or the FRI rate/degree ratio, the final-poly match keeps working without further changes here. All tests continue to pass; bench (Large) unchanged within noise. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Wires up the recursion package's compression / aggregation public
surface:
- Config.ModulePrefix: namespace knob threaded through every
module / column / expose name BuildVerifierCore emits. Empty by
default; aggregation sets it per-half ("L_" / "R_") so two
sub-verifiers can coexist in the same outer builder.
- buildVerifierCoreInto(builder, input, cfg) — non-public helper
that does the actual wiring against a caller-owned builder; the
BuildVerifierCore public function is now a thin wrapper that
creates a builder, invokes the helper, and compiles.
- BuildAggregationCore(AggregationInput, cfg) — produces a single
board.Program that verifies BOTH inner proofs in one outer
circuit. Drives buildVerifierCoreInto twice into the same
builder with disjoint prefixes, then trace.MergeMatching's the
two witness traces and compiles once.
- AggregateInputs([]RecursionInput, cfg) — binary-tree driver:
level 0 wraps each leaf via BuildVerifierCore + Prove + Verify;
level i >= 1 walks pairs from level i-1 through
BuildAggregationCore + Prove + Verify, halving each pass, until
a single root proof remains. SkipFRI at every level — leaf
soundness is enforced by the recursion-circuit constraints, not
by the outer FRI on the aggregation circuit itself.
Refactor mechanics:
- Single sed-style substitution prepended `mp` ("module prefix"
local) to every `"airverify` / `"merk_` string literal in
verifier_core.go (73 touchpoints). Each module name, column
name, and expose key is now of the form `cfg.ModulePrefix +
"<old name>"`, so passing ModulePrefix="" reproduces the
historical layout exactly.
- merkle.BuildModule / BuildModuleNoLeafHash calls switched from
`&builder` to `builder` since the inner helper now takes
*board.Builder rather than allocating its own.
Tests:
- TestBuildAggregationCorePair builds an aggregation of a 4-row
Fibonacci and a 4-row Equality leaf, proves the outer circuit
end-to-end. Passes in ~0.3 s.
- TestBuildAggregationCoreRejectsBadLeft tampers the left inner
proof's at-zeta value of column A. The aggregated verifier
rejects (the left-half AIR check fails inside the merged
outer constraint set).
- TestAggregateInputsTwoLeaves currently t.Skip's: building the
root aggregation circuit requires running BuildVerifierCore on
a leaf VERIFIER's airverify program — itself a multi-module
program with massive constraint expressions — and board.Compile
doesn't return within 600 s on the current implementation.
Re-enable after the performance work (sharing merkle modules
across queries, expression-tree flattening) lands.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 2 potential issues.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, have a team admin enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 3e849e3. Configure here.
| var digest hash.Digest | ||
| for i := 0; i < DigestLen; i++ { | ||
| digest[i].Set(&cols[cn.Sponge.Post[poseidon2sponge.NbRounds-1][i]][nPerms-1]) | ||
| } |
There was a problem hiding this comment.
GenerateTrace ignores sponge offset
Medium Severity
GenerateTrace always writes sponge inputs at module rows 0..nPerms-1 and reads the digest from row nPerms-1, but RegisterAt wires constraints and DigestRow at startRow+k. With startRow > 0, witness rows no longer match the row-gated equalities, so trace generation diverges from the circuit GenerateTraceWithSize already implements correctly.
Additional Locations (1)
Reviewed by Cursor Bugbot for commit 3e849e3. Configure here.
| } | ||
| if err := verifier.Verify(nil, setup.VerificationKey{}, outerProg, outerProof, verifier.SkipFRI()); err == nil { | ||
| t.Fatalf("aggregated verify accepted tampered left inner proof") | ||
| } |
There was a problem hiding this comment.
Tamper test exits on prove
Low Severity
TestBuildAggregationCoreRejectsBadLeft returns without failing when prover.Prove errors after tampering the left proof. The test title expects rejection at verify time; a silent pass hides regressions where prove fails for unrelated reasons or where a broken verifier never reaches Verify.
Reviewed by Cursor Bugbot for commit 3e849e3. Configure here.
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.
This is a bit more structured implementation of the recursion.
Note
High Risk
Adds security-critical proof-verification logic (FRI, FS, Merkle, AIR) and changes expression/power behavior used during compile; regressions could accept invalid proofs or break compilation.
Overview
Adds a structured
recursionpackage that builds Loom programs to verify inner Poseidon2 proofs, with tree aggregation (BuildAggregationCore,AggregateInputs) and a large set of in-circuit gadgets (E6 field math, AIR-at-zeta, Fiat–Shamir via width-24 sponge, FRI fold/chain/Merkle binding, DEEP bridge, etc.), plus broad prove/verify tests.Two core fixes support that work:
ExposeIthValueCtxnow records the source module so cross-module exposed values reconstruct correctly at zeta, andLeaf.Powstops expanding large exponents into deepMultrees (returns unaryPowinstead) to avoid compile-time blowups on big expressions.Reviewed by Cursor Bugbot for commit 3e849e3. Bugbot is set up for automated code reviews on this repo. Configure here.