halo2 proving system anatomy

DoHoon Kim·2025년 4월 9일

목록 보기

1/4

In this post, we will discuss about halo2 proving system and EVM verifier code of halo2 proof. Since I worked on EVM verifier written in Yul assembly, there were significant progress on making EVM verifier more readable, auditable, reusable, and scalable. The most recent work on this is the great work from EZKL team which made EVM verifier to be reusable from many application circuits by abstracting the circuit-specific information (verification key) from the verifier. I will review their architecture in depth later.

It is crucial to correctly understand how halo2 proving system works to understand how EVM verifier works. Let's dive into the halo2 proving system step-by-step. However, I will assume the reader of this post is already familiar with PLONK arithmetization, KZG polynomial commitment scheme and some basic arguments that constitute the protocol.

halo2 overview

Below is the basic material for the explanation of halo2 proving system. Let's say proving system is instantiated on the scalar field $\mathbb{F}_p$ of the elliptic curve that supports bilinear pairing that is required by KZG polynomial commitment scheme. The circuit has $m$ columns and each of column has size of $2^k$ rows. We have to make sure that for the prime $p$ , $p-1$ is divisible by $2^k$ , since it guarantees that $2^k$ -th primitive root of unity exists in $\mathbb{F}_p^{\times}$ (otherwise, it does not exist). Thus, we will assume $T \cdot 2^S + 1 = p$ for odd integer $T$ and $k \le S$ . Let's denote $\omega$ as $2^k$ -th primitive root of unity and $\delta$ as $T$ -th primitive root of unity. I will also denote $l_n(X)$ as the $n$ -th Lagrange basis polynomial for $0 \le n \lt 2^k$ .

There are basic lookup argument and permutation argument that are used for proving the correctness of the circuit. Let's see each of them.

Lookup argument

halo2's lookup argument is also called subset argument since halo2's lookup argument ensures that for some vectors $A, S$ , every element of $A$ is contained in $S$ . This statement is slightly weaker than indexed lookup argument, which ensures that each element of $A$ is positioned at the index $i$ in $S$ . However, we can tweak subset argument to work like indexed lookup argument. We will see this later.

To prove the statement for vectors $A, S$ , every element of A is contained in $S$ , the prover will first sort the vectors $A, S$ into $A', S'$ to meet the following rules.

The first element of $A'$ should be the same with the first element of $S'$ .

Every element of $A'$ should be the same with the corresponding element of $S'$ or the previous element of it in $A'$ .

So the rules force that every element of $A'$ is the same with some element in $S'$ and the elements with the same values are consecutive in the row.

The prover should prove the following:

$A', S'$ are some permutations of $A, S$ .

$A', S'$ meet the rules that are specified as above.

To prove the permutation, the prover uses product argument and produces new polynomial $Z_L(X)$ that satisfies the following:

Z_L(\omega X) (A'(X) + \beta) (S'(X) + \gamma) - Z_L(X)(A(X) + \beta)(S(X) + \gamma) = 0 \\ l_0(X) (1 - Z_L(X)) = 0

Next, to prove that $A', S'$ meet the rules that are specified as above, the prover should prove the following relations:

(A'(X) - S'(X)) (A'(X) - A'(\omega^{-1}X)) = 0 \\ l_0(X) (A'(X) - S'(X)) = 0

Permutation argument for equality constraints

In permutation argument, the prover will permute the values of the cells for which the equality constraints are enabled. To express this in general, let's assume that equality constraints are enabled across $m$ columns.

The system will label each cell with the unique element in $\mathbb{F}^{\times}$ that expresses the position. For the cell in column $i$ and row $j$ , it will be labeled using $\delta^i \cdot \omega^j$ . Let $\sigma = \{s_i(X)\}_{i=1}^m$ is the vector of polynomials that represent permutations of each column. The permutation will be composed of cycles in which the cells have the same values.

The prover of permutation argument wants to prove that for some permutation $\sigma$ , the permutation satisfies the following:

\{(label, value)\} = \{(\sigma(label), value)\}

i.e.

\{(\delta^i \cdot \omega^j, v_i(\omega^j)) |_{i=0, \dots, m-1, j = 0, \dots, 2^k-1}\} = \{(s_i(\omega^j), v_i(\omega^j)) |_{i=0, \dots, m-1, j = 0, \dots, 2^k-1}\}

The equality denotes the set equality. So this can be proved using product argument, by constructing the equation:

\prod_{i=0}^{m-1} \prod_{j=0}^{2^k-1} \frac{v_i(\omega^j) + \beta \cdot \delta^i \cdot \omega^j + \gamma}{v_i(\omega^j) + \beta \cdot s_i(\omega^j) + \gamma} = 1

$\beta, \gamma$ are challenges sampled by verifier. The prover computes the polynomial $Z_P(X)$ that satisfies the following:

l_0(X) (1 - Z_P(X)) = 0 \\ Z_P(\omega^{j+1}) = \prod_{h=0}^j \prod_{i=0}^{m-1} \frac{v_i(\omega^h) + \beta \cdot \delta^i \cdot \omega^h + \gamma}{v_i(\omega^h) + \beta \cdot s_i(\omega^h) + \gamma} \\ = Z_P(\omega^j) \cdot \prod_{i=0}^{m-1} \frac{v_i(\omega^j) + \beta \cdot \delta^i \cdot \omega^j + \gamma}{v_i(\omega^j) + \beta \cdot s_i(\omega^j) + \gamma}

In general, $Z_P(X)$ satisfies:

l_0(X) (1 - Z_P(X)) = 0 \\ Z_P(\omega X) \cdot \prod_{i=0}^{m-1} (v_i(X) + \beta \cdot s_i(X) + \gamma) = Z_P(X) \cdot \prod_{i=0}^{m-1}(v_i(X) + \beta \cdot \delta^i \cdot X + \gamma)

Vanishing argument

In vanishing argument, the prover computes the quotient polynomial that attests to the various relations imposed by circuit gates, equality constraints, and lookup argument. If $n = 2^k$ is the number of rows, the polynomial $X^n-1$ has the roots that are all the $n$ -th roots of unity. If the relations hold over the domain, then the polynomials should be divisible by $X^n-1$ .

h(X) = \frac{gate_0(X) + y \cdot gate_1(X) + y^2 \cdot gate_2(X) + \dots}{(X^n-1)}

$y$ is the challenge sampled by the verifier and used for random linear combination of all the relations.

Protocol - Committing

Now, we can describe the first half of the protocol. In the first half of the proving, the prover must commit to all the polynomials before opening them.

Protocol - Opening

DoHoon Kim

Researcher & Developer

다음 포스트