Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Verification

This chapter states the canonical acceptance predicate for \(\mathrm{Vega}_{\mathrm{MC}}\). It describes the verifier’s ordered structural checks; byte-exact absorb and squeeze order is fixed separately in the transcript schedule.

Verifier interface

The verifier entry point has the shape

#![allow(unused)]
fn main() {
verify(&self, vk: &VegaMcVerifierKey<E>, num_instances: usize)
  -> Result<(Vec<Vec<E::Scalar>>, Vec<E::Scalar>), VegaError>
}

The proof is accepted exactly when every check below succeeds, in this order. Failure at any step rejects the proof. The returned value is the per-step public values and the core public values; these vectors are the public statement exposed by the proof-system layer.

Canonical acceptance predicate

  1. Check the step count. The supplied num_instances must be nonzero. It must equal the number of step instances carried by the proof, and it must equal the num_steps value bound into the verifier key. These checks prevent a proof for one step count from being replayed under another count.

  2. Restore the shared witness commitment. The proof stores one shared witness commitment, comm_W_shared. The verifier attaches that same commitment to every step instance and to the core instance before any instance validation. After this point, each split instance is interpreted as if it had carried the shared commitment inline.

  3. Validate the split step and core instances. Each step instance is validated against the step split shape. For step index \(i\), the verifier creates a fresh Keccak Fiat–Shamir transcript, absorbs the verifier-key digest, the number of step circuits, the circuit index, and that instance’s public values, then calls the split-instance validation routine described in R1CS and its variants. Validation checks public-value length, checks the commitments required by the shape, absorbs the early witness commitments, re-derives the stored Fiat–Shamir challenges, compares them exactly, and absorbs the rest commitment. The core instance is validated similarly against the core split shape, with the verifier-key digest and core public values as its public transcript context. After validation, the verifier checks that every step instance and the core instance carry the same comm_W_shared.

  4. Convert split instances to regular R1CS instances. The step list is padded to a power of two by repeating the first step instance when necessary. Each padded step instance is converted to a regular instance by combining its split witness commitments and setting its public vector to public values followed by split challenges. The core instance is converted the same way, without step-count padding. This is the strict R1CS layer; relaxed R1CS appears only after the later Nova fold.

  5. Reconstruct the main protocol transcript. The verifier starts the protocol transcript in the same domain as the prover, absorbs the verifier-key digest, the regular core instance, every regular step instance, and the scalar \(T=0\). It computes the padded step-folding round count, the step row round count, and the inner round count. It then draws \(\tau\) and the \(\rho\) challenges used by NeutronNova folding. This chapter records the structure; the transcript schedule fixes the byte-level labels and order.

  6. Validate the verifier-circuit instance and read its public input. The proof’s U_verifier is a multi-round split R1CS instance for the verifier circuit. The verifier validates it against vc_shape, using the live protocol transcript, then converts it to regular form. In regular form, the public vector is the flattened verifier-circuit challenges followed by the verifier-circuit public values, as described in the in-circuit verifier. The verifier requires the challenge prefix length to be

    \[ \ell_b + \ell_x + 1 + \ell_y, \]

    where \(\ell_b\) is the step-folding round count, \(\ell_x\) is the outer row round count, and \(\ell_y\) is the inner round count. The six public values must follow immediately, in this order:

    PositionValue
    0tau_at_rx
    1eval_X_step
    2eval_X_core
    3eq_rho_at_rb
    4quotient_step
    5quotient_core

    The challenge prefix is parsed as \(r_b\), then \(r_x\), then the single bridge challenge \(r\), then \(r_y\).

  7. Fold the step instances and verify the Nova fold. Using \(r_b\), the verifier calls fold_multiple on the regular step instances. This derives the NeutronNova folding weights and linearly combines the step public vectors and witness commitments into one folded step instance. In parallel with that computation, the verifier checks the Nova folding for zero-knowledge proof: it absorbs the random relaxed instance, the regular verifier-circuit instance, and the cross-term commitment, squeezes the Nova fold challenge, and obtains the folded relaxed verifier-circuit instance. The folding background is in NeutronNova folding.

  8. Verify the relaxed-Spartan proof. The verifier runs the Relaxed Spartan verifier over the folded relaxed verifier-circuit instance, using the regular verifier-circuit shape and verifier-circuit commitment key from the verifier key. This proves satisfaction of the masked folded verifier-circuit relation produced by the Nova fold.

  9. Pin the six soundness-binding public values natively. The verifier recomputes the six public values outside the circuit and compares them with the six values exposed by U_verifier. This is the soundness-binding step.

    First, it evaluates the step and core matrix tables at the native verifier points. The row point is \(r_x\), and the column point is the full \(r_y\). For \(\star \in \{\mathrm{step},\mathrm{core}\}\), the verifier computes

    \[ Q_\star = \widetilde{A}_\star(r_x,r_y) + r\,\widetilde{B}_\star(r_x,r_y) + r^2\,\widetilde{C}_\star(r_x,r_y). \]

    The implementation names these values quotient_step and quotient_core. This quotient convention matches the Spartan argument: the batched matrix evaluation is eval_A + r·eval_B + r²·eval_C.

    Next, it evaluates the folded step public-input polynomial and the core public-input polynomial at \(r_y[1..]\). Each public-input table is formed from the leading constant \(1\) followed by the regular instance public vector. It also computes tau_at_rx from the powers polynomial determined by \(\tau\) at \(r_x\), and computes eq_rho_at_rb as the equality-polynomial value \(\widetilde{\mathrm{eq}}(r_b,\rho)\).

    The verifier then applies an exact six-way equality gate:

    \[ (\mathrm{tau\_at\_rx},\mathrm{eval\_X\_step},\mathrm{eval\_X\_core},\mathrm{eq\_rho\_at\_rb},\mathrm{quotient\_step},\mathrm{quotient\_core}) = (x_0,x_1,x_2,x_3,x_4,x_5). \]

    Here \((x_0,\ldots,x_5)\) are the six public values read from U_verifier. Any mismatch rejects.

    This native recomputation is mandatory. The verifier circuit proves the folding and sum-check relations, but the six exposed openings must be tied to the actual verifier key, step instances, core instance, and transcript challenges held by the native verifier. The equality gate closes the soundness gap that would remain if the verifier trusted only the circuit-exposed values.

  10. Verify the final PCS opening. The transcript supplies the folding challenge c_eval. The verifier folds the folded-step witness commitment with the core witness commitment using coefficients \(1\) and c_eval. It also folds the two verifier-circuit evaluation commitments with the same coefficients. The prover-side relation folds the matching blinds. The verifier then checks the zero-knowledge Hyrax/IPA polynomial-commitment opening at the point \(r_y[1..]\), using the folded witness commitment, the folded evaluation commitment, and eval_arg.

Result

If all ten checks pass, verification returns the original per-step public values and the original core public values. Those values are not reinterpreted by the proof system; their application meaning is supplied by the circuits used in setup and proving. The surrounding proving flow is described in Proving, and the privacy layer is described in Zero knowledge.