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.

recursive Brakedown opening check is pure field arithmetic. no Merkle verification, no hash-dominated bottleneck. proof size: ~2 KiB (sumcheck ~0.5 KiB + evaluation ~0.3 KiB + Lens opening ~1.3 KiB).

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)
     (recursive tensor check, O(lambda log log N) field ops)

  return accept

step 2 is pure field arithmetic. step 4 is pure field arithmetic (matrix-vector product check via recursive Brakedown). the entire verification loop is field-op dominated.

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 recursive Brakedown. three cost tiers depending on optimization level:

the ~825 tier is the practical target. breakdown:

the ~89 tier replaces hemera-based Fiat-Shamir with algebraic challenges derived from the field structure. all verification becomes pure field arithmetic.

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 is entirely field arithmetic — no hash jets needed in the Lens check. hemera is used only for Fiat-Shamir transcript (squeezing challenges), reducing the hash dependency in the recursive verifier.

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

verification time is independent of the original computation size. a proof of a 300-constraint identity check and a proof of a million-constraint neural network inference verify in the same time.

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))  // ~825 constraints
proof_C = zheng.prove(zheng.verify(proof_B))  // ~825 constraints

each recursion level costs ~825 constraints, regardless of the original computation size. proof size remains constant: ~2 KiB.

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