verifier

the standalone verifier algorithm for zheng. accepts a proof and a public statement, returns accept or reject. the verifier is a nox program — it runs inside the same VM that produced the original trace, enabling recursive proof composition.

the Lens opening today is Brakedown with TensorMerkle authentication: every queried codeword column carries a Merkle path against the commitment root. proof size scales with trace size — see performance for measured numbers. a Merkle-free recursive opening (constant ~2 KiB) was designed but is blocked on a soundness gap; see recursive-brakedown in roadmap/ and lens issue #6.

algorithm

VERIFY(commitment C, statement S, proof pi) -> accept/reject:

  1. INIT TRANSCRIPT
     T = transcript_init(DOMAIN_SEP)
     T.absorb(S)
     T.absorb(C)

  2. SUMCHECK VERIFICATION (k rounds, k = n + 4)
     claim_0 = 0  (constraints must sum to zero)
     for i in 1..k:
       g_i = pi.sumcheck_polynomials[i]
       assert g_i(0) + g_i(1) = claim_{i-1}
       T.absorb(g_i)
       r_i = T.squeeze()
       claim_i = g_i(r_i)

  3. EVALUATION CHECK
     r = (r_1, ..., r_k)
     v = pi.evaluation_value
     assert claim_k = constraint_eval(v, r, S)

  4. LENS VERIFICATION
     assert Brakedown_verify(C, r, v, pi.pcs_opening)
     (TensorMerkle: per-column Merkle path check against the commitment root,
      plus the row-combination consistency check against the encoding)

  return accept

step 2 is pure field arithmetic. step 4 authenticates each queried column against the commitment root via Merkle path, then checks encoding consistency — this is where hashing dominates the verifier's cost (see performance).

constraint evaluation

step 3 checks that the sumcheck's final claim equals constraint_eval(v, r, S). this function reconstructs the constraint polynomial's evaluation at the random point r chosen during sumcheck, using the prover-supplied register evaluation v.

register layout

the trace table has 16 registers per row:

the prover commits to the multilinear extension of each register column. v is the vector of all 16 register evaluations at the random point r: v[j] = f_j(r) where f_j is the multilinear extension of register column j over the boolean hypercube.

selector polynomials

each pattern p in {0, 1, ..., 16} has a Lagrange selector polynomial:

selector_p(x) = product_{q != p} (x - q) / (p - q)

evaluated at v[0] (the pattern tag register at point r), selector_p(v[0]) is 1 when the pattern tag equals p and 0 otherwise. this demultiplexes the single constraint evaluation into the correct pattern.

pattern constraints

each pattern p defines a constraint polynomial C_p over the register values. for example:

• pattern 5 (add): C_5(v) = v[3] + v[4] - v[5] (inputs sum to result)
• pattern 7 (mul): C_7(v) = v[3] * v[4] - v[5] (inputs multiply to result)
• pattern 8 (inv): C_8(v) = v[3] * v[5] - 1 (input times result is one)
• pattern 15 (hash): C_15(v) = hemera(v[3], v[4]) - v[5] (hash of inputs equals result)

all 17 patterns contribute, but the selector zeroes out every pattern except the active one.

the formula

constraint_eval(v, r, S) = eq(r_row, r) * sum_{p=0}^{16} selector_p(v[0]) * C_p(v)

where:

• r_row is the row-dimension component of r (the first n variables, where 2^n is the number of trace rows)
• eq(r_row, r) is the multilinear equality polynomial: eq(a, b) = product_i (a_i * b_i + (1 - a_i)(1 - b_i)), which ties the sumcheck reduction to the specific evaluation point
• the sum over p combines all 17 pattern constraints, weighted by selectors
• C_p(v) evaluates pattern p's constraint using the register values at r

the sumcheck protocol reduces the claim "the constraint polynomial sums to zero over the boolean hypercube" to a single evaluation at a random point. constraint_eval computes that single evaluation. if the prover is honest, every row satisfies its pattern constraint, the sum is zero, and this evaluation matches claim_k.

boundary constraints

boundary constraints enforce the public statement S at specific trace positions. these are point evaluations at binary coordinates (vertices of the hypercube):

• at row 0: f_14(0, 0, ..., 0) = 0 (status is running), f_15(0, 0, ..., 0) = 0 (step counter starts at zero)
• at the final row: f_14(1, 1, ..., 1) = 1 (status is halted)
• program hash: the commitment to the opcode column must match S.program_hash
• input/output: f_3(0, ..., 0) = S.input_hash and f_5(last_row) = S.output_hash
• focus bound: f_6(0, ..., 0) - f_7(last_row) <= S.focus_bound

boundary constraints are folded into the same sumcheck by adding them as additional terms with their own random combiners (drawn from the transcript).

relationship to sumcheck

the sumcheck protocol (step 2) starts with claim_0 = 0 because a valid trace satisfies all constraints on every row, so the constraint polynomial sums to zero over the hypercube. after k rounds of interaction, the verifier holds a random point r and a final claim claim_k. step 3 asserts claim_k = constraint_eval(v, r, S): the reduced claim equals the actual constraint evaluation at r. step 4 then verifies (via Brakedown) that v is the correct evaluation of the committed polynomials at r. together, steps 3 and 4 complete the sumcheck verification — step 3 checks algebraic consistency, step 4 checks that the prover did not lie about v.

cost breakdown

the verifier uses TensorMerkle Brakedown: every queried column is authenticated by a Merkle path against the commitment root, so hashing — not field arithmetic — dominates. see performance for the full component breakdown; summary:

a Merkle-free design (recursive Brakedown, targeting ~825 constraints generic / ~89 with algebraic Fiat-Shamir) was analyzed but is blocked on a soundness gap in the recursive opening — see recursive-brakedown in roadmap/ and lens issue #6. those numbers are the target if that gap closes, not the current cost.

nox pattern decomposition

every verifier operation maps to native nox patterns:

no external primitive enters the verification loop. the verifier is closed under the nox instruction set. consequence: verify(proof) can itself be proven, and verify(verify(proof)) too, to arbitrary depth.

Brakedown opening verification with TensorMerkle is hash-dominated: each queried column needs a Merkle path checked against the commitment root. hemera is used both for that and for the Fiat-Shamir transcript.

input/output format

INPUTS (public):
  commitment:  [u8; 32]              // hemera digest
  statement:   Statement {
    program_hash: [u8; 32],           // hash of the nox program
    input_hash:   [u8; 32],           // hash of public inputs
    output_hash:  [u8; 32],           // hash of public outputs
    focus_bound:  u64,                // maximum focus consumed
  }

PROOF:
  sumcheck_polynomials: Vec<Vec<GoldilocksElement>>,
  evaluation_value:     GoldilocksElement,
  pcs_opening:          BrakedownProof,

OUTPUT:
  accept / reject

verification time

see performance for the derivation. verification time is dominated by Merkle-path checks over the queried columns, not by the trace size directly — but proof size (and so the number of columns to check) does grow with trace size, unlike the constant-size claim a Merkle-free lens would give.

recursive verification

when the verifier runs as a nox program, its execution trace can be proven by zheng. the recursive proof attests that a previous proof was valid.

proof_A = zheng.prove(computation)            // ~|C| constraints
proof_B = zheng.prove(zheng.verify(proof_A))  // ~70,000 constraints (with jets)
proof_C = zheng.prove(zheng.verify(proof_B))  // ~70,000 constraints (with jets)

each recursion level costs ~70,000 constraints with jets (~600,000 without) — see performance. commit currently rejects axis/look openings for recursive composition (CommitError::UnsupportedRecursiveOpening); the native decider path works, recursive composition beyond that is release-blocked.

with HyperNova folding, recursive composition drops further: ~30 field ops + 1 hemera hash per fold step, with one decider proof at the end. see recursion for folding-first composition.

see transcript for Fiat-Shamir construction, sumcheck for the core protocol, Brakedown for the Lens opening verification, constraints for the AIR format, nox for the VM