Algorithms

The verification key is computed once per circuit and reused for every proof. It contains G1 commitments to the circuit's fixed column polynomials and to the permutation polynomials that encode the copy constraints. All VK data is hashed into a single 32-byte digest that is the first element absorbed by the proof transcript. The H2MO PCS contributes no extra VK commitments — all PCS state lives in the proof.

vk_commits = nb_fixed + nb_cc

// nb_fixed: one G1 per fixed-col polynomial
// (selectors, constants, lookup table cols)

// nb_cc: one G1 per copy-constrained column
// These are the permutation polynomials σᵢ(X)
// that encode which cells must be equal.
// They are fixed (witness-independent) so
// they belong in the VK, not the proof.
nb_cc = (pi > 0 ? 1 : 0)   // instance col
       + (ci > 0 ? 1 : 0)  // committed-instance col
       + chip_cc            // chip advice + fixed cc
       + nb_advice          // extra advice cols (all cc)

vk_size =
  10                    // header bytes
  + 48 · vk_commits

// Extra fixed cols added via --nb-fixed
// and --nb-selectors are not cc, so they
// appear in nb_fixed but not nb_cc.

// Lookup table columns count toward
// nb_fixed (one commit per table col)
// but are not cc.

Proof elements are grouped by the argument that produces them. Each argument contributes a fixed number of commitments and scalar evaluations determined by the circuit structure. Formulas reference key derived parameters defined below.

nb_commitments =
  nb_advice               // one per advice col
  + 2 · nb_lkp            // A_perm + S_perm per lookup
  + ⌈nb_cc / (degree−2)⌉  // permutation product polys Z
  + nb_lkp                // lookup product poly Z
  + nb_trash              // one per trashcan
  + 1                     // vanishing random poly
  + (degree−1)            // vanishing h-splits
  + 2                     // H2MO: F and Pi

// Simplified: degree + nb_advice + 3·nb_lkp
//   + ⌈nb_cc/(degree−2)⌉ + nb_trash + 2

commit_bytes = nb_commitments · 48

nb_scalars =
  nb_evals                    // advice + fixed col queries
  + (ci > 0 ? 1 : 0)          // committed-instance eval
  + 1                         // vanishing random eval
  + nb_cc                     // perm common evals
  + 3·⌈nb_cc/(degree - 2)⌉ - 1  // perm cross-term evals
  + 5 · nb_lkp                // per lookup:
                              //   Z(X), Z(ωX)
                              //   A_perm(X), A_perm(ω⁻¹X)
                              //   S_perm(X)
  + nb_trash                  // one per trashcan
  + max(nb_point_sets, 3)     // H2MO Q evals

scalar_bytes = nb_scalars · 32

These quantities are derived from the circuit structure and appear in both the proof size and verifier cost formulas.

degree = max(
  degree_hint,
  // perm requires ≥ 3
  nb_cc > 0    ? 3 : 0,
  // PlookUp requires ≥ 5
  nb_lkp > 0   ? 5 : 0,
  // trashcan requires ≥ 4
  nb_trash > 0 ? 4 : 0,
  // chip's gate argument degree
  max(chip gate degree)
)

// perm chunk size = degree−2
// nb_perm_chunks = ⌈nb_cc / (degree−2)⌉
// higher degree → fewer Z commits
//              → more h-splits

point_sets = 
  // if any permutation
  (nb_cc>0 ? {{cur,next}, {cur,next,last}}) ∪
  // if any lookup
  (nb_lkp>0 ? {{prev,cur}, {cur,next}}) ∪
  // if any trash
  (nb_trash>0 ? {{cur}}) ∪
  // if any committed instances
  (nb_cis>0 ? {{cur}}) ∪
  // chips gates queries
  {chips gates rotations} ∪
  // chips fixed queries
  {chips fixed rotations}

  // Each distinct rotation group across
  // all column queries becomes one H2MO
  // Q polynomial (one MSM in the verifier).
        

nb_blind =
  2
  + nb_trash
  + max(3, max_advice_queries)

// The last nb_blind rows are random,
// hiding the witness. The verifier
// evaluates the Lagrange basis over
// the full domain (constraint + blind).

// max_advice_queries = max rotation
// set size across advice columns.

The verifier runs in four sequential phases: it first absorbs the VK and public inputs into the transcript, then reads the proof while squeezing Fiat-Shamir challenges, then evaluates all argument expressions as scalar field arithmetic, and finally verifies the KZG opening via the H2MO multi-open scheme. The dominant costs are the per-column scalar products in the permutation argument and the per-gate polynomial evaluations.

Before reading the proof, the verifier absorbs the VK hash and public inputs. While in theory a proof can have more than one committed instance, in practice a maximum of one is usually processed. The full transcript size is: 32 + 48 · ci + 32 + 32 · pi + proof_size bytes. Each squeeze() call hashes everything absorbed so far to produce a 32-byte challenge. Public instance columns are not read from the proof — the verifier recomputes their evaluation from the public inputs using a Lagrange basis evaluation.

After reading all proof elements, the verifier computes the evaluation of each argument at the challenge point X. All operations here are scalar field arithmetic. Gate expressions are the most circuit-specific cost; permutation scales with the number of copy-constrained columns.

Each gate is a polynomial expression over advice and fixed evaluations.

All gate expressions within one chip are processed separately, but could be batched into a single combined expression using random linear combinations, before being aggregated in the vanishing polynomial.

Cost: Gate-specific, scales with the number of scalar ops, constants and columns defined.

Trashcan arguments are midnight-zk specific arguments that ensure the argument selectors are used additively.

Cost: Trashcan-specific, specific, scales with the number of scalar ops, constants and columns defined

For each lookup argument, we need to process both their table and input expressions that are then used to compute their lookup expressions -- five for each of them.            

Cost:
- Per argument: Lookup specific,
usually around 4 mul and 4 add.
- Per lookup: 11 mul + 4 add + 6 sub.

The evaluation of each copy-constrained columns is summed in a product to generate the permutation polynomial. The latter is divided in chunks, depending on the circuit size, before being aggregated in the vanishing polynomial together with combinationas of the permutation evaluations extracted from the transcript.

Cost:
- Per cc column: 3 mul + 3 add + 1 pow,
- Per evaluation: 1 mul + 1 add + 1 neg,
- Per perm chunk: ~7 mul + 2 sub + 1 add,
with #perm_chunk = ⌈nb_cc / (degree - 2)⌉
        

The vanishing argument simply is the aggregation of all previously defined gates via random linear combination, using a transcript's challenge as randomness.
            
Once aggregated, we substract one to the sum, inverse it and multiply it by the vanishing evaluation extracted from the circuit.

Cost: (terms+1) mul + (terms-1) add + 1 inv + 1 sub,
with terms = #gate + 5 · nb_lkp + (1 + 2 · nb_perm_chunks) + nb_trash

Note that as the vanishing polynomial is split into chuncks to make sure not to increase the overall circuit degree, these needs to be recombined. As such, the chunked vanishing commitments extracted from the transcript are aggregated in a MSM of size (degree - 1).

Now that the scalar evaluations have been recomputed, we need to ensure that they are consistent with the commitments. To do so, we perform opening proofs on these through our PCS scheme, and btach them together to reduce costs. The Halo2 Multi-Open scheme reduces all KZG polynomial openings across all rotation sets to a single pairing check. It introduces 4 challenges (X₁, X₂, X₃, X₄) and 2 proof elements (F and Pi). The verifier computes a batched polynomial F as a linear combination of all committed polynomials — grouped by rotation set — and checks that F opens correctly at X₃ using the Pi commitment.

// One Q polynomial per rotation set.
// Q_s = Σⱼ X₁ʲ · cⱼ  (over commits in set s)
// Each Q is accumulated via MSM.

Powers of X₁: max_commits_per_set muls
Powers of X₄: (nb_point_sets + 1) muls

Per point set s:
  MSM of size |commits in s|
  decompress_point per commit
  mul + add per scalar eval (X₁ power)
  add_point + scale (X₄ accumulation)

Total: nb_point_sets MSM calls

// F(X₃) from Q evaluations:
// r_s = Lagrange interpolation of
//       (eval_points_s, evals_s) at X₃
// F(X₃) = Σ_s x₂ˢ · (Q_s(X₃) − r_s)
//               / Π_s (X₃ − ωʳ)  ← denom

Per set: lagrange_eval + denom product
  + 1 batch_inversion (all sets)
  + mul + sub + mul + add (fold)

Final commitment check:
  2 add_point + 2 scale + 2 decompress
  → 1 Miller loop + 1 final pairing

Recursive circuits embed the accumulator and the VK hash directly in the public inputs. The accumulator is composed of 2 G1 elements for checking the equation: \[ e(\mathsf{acc}_\mathsf{left},\, g_2) \overset{?}{=} e(\mathsf{acc}_\mathsf{right},\, \mathsf{srs}.g_2) \] It is split in a variable part, that is handled in circuit, and their powers, and a fixed one, that is handled outside the circuit. Each part is as a BLS12-381 G1 point represented in two coordinates, each coordinate further split into 7 field-element limbs. The verification has to recompute both parts and combine them before doing a permutation check.

PIs added by IVC (per step):
  VK hash                   // 1 field element
  acc_var_left  = (xL, yL)  // 2 · 7 limbs = 14 scalars
  acc_var_left_power        // 1 scalar
  acc_var_right = (xR, yR)  // 2 · 7 limbs = 14 scalars
  acc_var_right_power       // 1 scalar
  acc_fixed                 // vk_size + 3 scalars

  Total extra PIs: 34 + vk_len field elements

// Each coordinate is encoded in NB_LIMBS = 7 field-element limbs. The verifier performs a Horner-style recombination on integers:

for coord in [x, y]:
  for limb in 0..NB_LIMBS:
    add()    // accumulate limb
    mul()    // shift by limb base
  mod(p)     // convert integer to scalar

Total cost:
28 multiplications, 28 additions, 4 modular reductions.

// Once both coordinates are assembled, we compute the point via compressed representation from them. Step by step, this is: 
- Encode the `x` coordinate as 48 bytes
- Set the 5th bit to 1 if `y` is positive
- Set the 6th bit to 1 if the point is zero
- Set the 7th bit to 1 to show the point is compressed

// Once the point is reconstructed, we multiply it by the corresponding scalar extracted from the public input.

Total cost:
  1 integer addition, 1 compression, 1 decompression, 1 point multiplication.

// Because the VK commitments are stored in compressed form, each must be decompressed.
vk_len decompress

// One MSM covers all commitments.
let acc_fixed = msm(vk_commits, -g2,
           pis, cis)

Total Cost:
1 MSM of size (vk_len + 3),  vk_len decompress
        

// The right sides of the fixed and variable accumulators are added together to form the combined right accumulator. No batching coefficient are needed as they are just splits of the same structure.

acc_right = acc_right_var + acc_fixed

Total Cost:
1 point addition

// Compress the 2 accumulator points and 2 proof points as a hash input:
inputs = compress_point() · 4

// Generate a byte digest:
digest = hash_bytes(inputs)

// Convert it to scalar:
λ = digest.from_int_scalar()

// Scale and fold each side into the proof's existing left and right G1 pairs:
l = pi_left + λ · acc_left
r = pi_right + λ · acc_right

// Run the Miller loops on each side:
ml = miller_loop(l, srs.g2)
mr = miller_loop(r, g2)

// Perform the final exponentiation of the pairing check:
final_exp(ml, mr)