Halo 2 is the upgraded version of Halo, which is developed by ECC using PLONK technology. It makes full use of the features of PLONK, such as custom gate, PLONKup, etc., making it more efficient and convenient to develop zero-knowledge proof circuits with Halo 2.
For details on the principle of Halo 2, please refer to our previous article Halo 2 Principle Explained.
Halo 2 is widely used in many current zkEVM solutions. In this article, we will take a simple example to introduce how to develop Halo 2 circuits.
Halo 2 Circuit System
Before explaining the example, let's get to know something about the proof system of Halo 2. The Halo 2 circuit is defined by matrix/table, and generally uses the rows, columns, and cells of the matrix to represent various special and different meanings.
A circuit depends on the following configuration:
- For finite field F, all cell elements are F field elements.
- Different from another ZKP circuit system bellman, Halo 2's circuit system uses an advice column to represent witnesses, an instance column to public input, and a fixed column to represent the fixed part of the circuit. The lookup table quoted in PLONK is in the fixed column. The selector column is an auxiliary field of the fixed column, which is used to determine under what conditions to activate the gate.
- Part of the columns can be used for equality constraints.
- A polynomial order upper limit.
- A series of polynomial constraints. These are multivariate polynomials in the finite field F, and the result of each row must be 0. The variable in the polynomial constraint can be a cell in a certain column of the current row, or a cell in a certain column relative to the current row.
- A series of lookup tables defined on the input expressions (multivariate polynomials mentioned above) and table columns. This is the PLONKup in PLONK.
- A series of equality constraints are used to specify that two cells have the same value. Students familiar with PLONK know that it is actually a copy constraint.
For the circuit system of Halo 2, see the figure below:
In which:
- The yellow column represented by a is the advice column
- The red column represented by i is the instance column
- The blue column represented by f is a fixed column
- The purple column represented by s is the selector column
For different proofs, advice and instance columns are different. It is easy to understand, because each time a different proof is generated, witness and public input are basically different; while fixed and selector columns are related to the circuit, not the input.
Halo 2 Tools
- Mock Prover
It is a tool used to debug the circuit, which can test every constraint in the circuit in the unit test. It is very important for the circuit development of Halo 2. We need to use halo 2::dev::MockProver to debug the code frequently in the circuit development process. If a constraint does not satisfy the condition, run reports an error, otherwise, it returns normally.
- Circuit_Layout
The circuit_layout can display different parts of the circuit in the form of graphs, such as advice/fixed/instance mentioned above.
- Cost-Model
The cost-model can be used to calculate the size of the proof generated by the circuit, the time it takes to verify, and so on.
Case Study of Halo 2 Circuit Development
As follows, to develop a circuit, a and b as private input and c as public input need to prove that:
a² * b² = c
(1) Define instructions
Because the circuit can be used to prove the description of any scene, for example, to compare sizes. Here the circuit needs to define the circuit of the above scenario in order to prove the above equation. It is the multiplication here. Take the square of a as an example, it can be seen as a multiplied by a. The outermost is the square of a multiplied by the square of b. And our circuit deals with the multiplication of two numbers, so the input and output of instructions are both Num. The interface is as follows:
The interface is as follows:
Among them, Num is used to adapt to the type handled in this interface, load_private is used to load witness, load_constant is used to load constants, mul is used to calculate the multiplication of two numbers, and expose_public is used to set instance.
2. Define chip implementation Most of the time, using Halo 2 for circuit development does not need to define instructions and chips by oneself. These modules implement special functions and belong to the infrastructure. Generally, the ones provided by Halo 2 are sufficient. But if you need to use complex ones that Halo 2 does not provide, you need to implement them yourself, such as implementing an emerging cryptographic algorithm.
If you want to develop a custom chip, you need to implement the chip trait of Halo 2.
Among them, the config function returns to the configuration of the custom chip, and the loaded function returns the loaded data of the custom chip. There is no need to return here.
3. Configure chip The key of a chip is in its config. As follows, our custom chip requires two advice columns, an instance column, a selector column, and a constant.
Among them, the most critical functions configure and enable_equality are used to check the equality of the incoming parameters. In the create_gate function, two active (a, b) are in different columns of the same row, while the result of the multiplication, advice and a are in the next line of the same column, and finally, the function returns to the polynomial constraint: if s_mul is not 0, the check multiplication constraint is activated. If the result is 0, then lhs * rhs-out must be 0, and lhs * rhs = out; if s_mul is 0, the check multiplication constraint is not activated, and any subsequent values are fine, which we don't pay attention to.
4. Implement the chip interface The instructions interface we defined earlier needs to be implemented, and defining the implementation of Number is to encapsulate finite field elements.
Among them, in the most critical function mul, take out two cells from config, check whether the input a and b are equal, and then return a * b. It should be noted that, in addition to row and column, the position of the cell can also be determined by the relative position offset. Generally, there are three types of offsets, 0 representing the current position, 1 representing the next position, and -1 representing the previous position.
5. Construct the circuit The circuit trait is the entrance to the circuit development. We need to define our own circuit structure and access the witness input.
The interfaces defined before are all used here. configure creates a storage column for advice/instance/constant. synthesize uses a custom chip to get the input witness and constant, and finally, calculate the result and return the public input. In fact, it can satisfy most scenarios by simply implementing the circuit trait for general circuit development. Some common functions of the chip have already been implemented in Halo 2.
6. Test circuit The MockProver and CircuitLayout that we mentioned in the chapter about tools can come in handy.
MockProver can check constraints. Checking the verify function you can know how many constraints such as selector, gate, lookup, and permutation have been checked. Using the following code, you can output the circuit layout to show different parts of the circuit. If you are interested, try it yourself and see what the visual layout of the circuit looks like in this simple example.
In this example, the relationship among the circuit, chip, instructions traits, and their implementation is shown in the following figure:
Summary
In this article, we have introduced the basic flow of Halo 2 circuit development, which we hope can be beneficial to readers. With its own novel designs such as row/column/cell/chip/region, the Halo 2 circuit design is quite different from the bellman scheme. The doors in Halo 2, different from the doors of R1CS, use the door design of PLONK more. As we write this article, the AZtec team has released the latest updated algorithm of PLONK-Fflonk. The new algorithm improves the efficiency of verify and saves time of verify. We will wait and see whether the ECC team will integrate Fflonk into Halo 2. As for the principle analysis of Fflonk, please wait for our subsequent articles.
References
Mathematics in Blockchain (Eighty Eleven) - Halo 2 Circuit
[Halo 2 Repo](https://github.com/zcash/halo 2)