Getting Started with Halo2
For developers who want to write ZK circuits in Halo2
Firstly, we highly recommend that you use VSCode and the rust analyzer extension  especially when first learning halo2, the autocomplete and peek are extremely useful in learning the available API commands.
Learning Rust
The Rust book is a good place to get started: the first 5 chapters are elementary and effectively mandatory to read. For more advanced Halo2 usage, it is necessary to know about closures (Ch 13). Later it may be helpful to know about smart pointers (Ch 15), though for performance it's best to not use them when possible.
Our recommendation: to ramp up as quickly as possible, read the first 5 chapters of the Rust book and then try to write a ZK circuit using halo2lib. Rust questions are bound to come up as you go, and you can find answers onthefly with Google and the Rust book.
To learn rust best practices, we recommend turning on cargo clippy
instead of just cargo check
in VSCode>Rust analyzer>Check on save command.
Halo2lib
In the rest of this doc we will explain how to write ZK circuits using the halo2lib library. We created the halo2lib library to have a faster, easier API to develop in Halo2.
Simplified interface
In halo2lib
, the basic frontend interface is that you have a table with two columns and a number of rows which you can specify. The first column, known as the advice column, consists of numbers (called witnesses), which the Prover gets to fill in on a perproof basis. The second column, known as the selector column, consists of boolean numbers (0 or 1), which are determined once and for all when the circuit is created. After circuit creation, the selector column is shared with both the prover and the verifier (in some form).
Advice  Selector 

$a_0$  $s_0$ 
$a_1$  $s_1$ 
$a_2$  $s_2$ 
$\vdots$  $\vdots$ 
What prevents the prover from putting arbitrary numbers into the advice column is that we impose a single "custom gate" which must hold on every 4 consecutive rows: with a, b, c, d
in a single (vertical) advice column and a selector cell q
as below:
Advice  Selector 

a  q 
b  
c  
d 
the constrain
must hold. This gate is applied at every row, so at each row you specify whether q
is 0
or 1
to turn on/off the gate. If q = 1
, then you impose a + b * c == d
. If q = 0
, then there is no constraint. (Implicitly, this assumes that the last 3 rows have 0
in the selector column.)
The reason that this constraint must hold on every row is due to the nature of the proving system, which uses polynomial commitment schemes behind the scenes.
In this framework, to design a circuit you:
Provide an algorithm that specifies how the Prover should fill in the advice column on each run of a computation.
Specify which cells to turn the selector "on" (place a
1
in the cell). By default all cells have value0
.
Below we will walk through some examples showing how to use the halo2lib
API. You can skip ahead to see the list of available functions in this API here.
Examples walkthrough
We have provided some examples of how to use halo2lib
in a quicksetup sandboxed environment in the halo2scaffold repository. We will walk through the examples there as a way to explain the halo2lib
API in more detail.
In this example, we have a single function some_algorithm_in_zk
that has all the custom computation logic for our ZK circuit. In this case it is a computation that only takes in one input number x
. The computation computes x > x**2 + 72
and outputs this as a public output.
main()
main()
In the main()
function, we then specify the specific value of x
we want to run the ZK proof on (in this case generated randomly using Fr::random(OsRng)
) and then call mock(some_algorithm_in_zk, x)
to run the MockProver
on this circuit with input x
. Here, scaffold::mock
is a helper function we have provided that does some boilerplate setup for converting some_algorithm_in_zk
into a ZK circuit and then calling the mock prover. The mock prover performs the witness assignment computations and then checks using normal programming logic whether the gate constraints are all satisfied. By this we mean that it does not run the true ZK proving system (such as for example computing polynomial commitment schemes).
If you uncomment out the line
in main()
, this will run the true ZK prover and verifier algorithms (involving polynomial commitment schemes). The extra parameter Fr::zero()
here is a technicality: in the initial creation of the circuit (creating the Prover and Verifier binaries), the API still needs to have an input value for x
. Since in main()
we only run the Prover and Verifier algorithms on one input x
, the make sure everything works properly we use a different value Fr::zero()
in the circuit creation portion to make sure there is no hidden inputspecific logic in our circuit.
some_algorithm_in_zk
some_algorithm_in_zk
We now inspect the actual computation in ZK we want to perform. The function format is:
It is customary to write reusable functions where the numbers are in a generic prime field F
. Here ScalarField
is a rust trait that implements all of the operations you would expect of a prime field. Note that in main()
we always specialize to F = Fr
which is the scalar field of a specific elliptic curve BN254.
The parameter ctx
is a mutable reference to a struct Context<F>
. This is roughly the data of the running list of numbers you are putting into the Advice and Selector columns we described above.
In this computation, we take a single field element as input, x: F
. In general you can replace F
by any type that you would like to use to describe your input.
Lastly we have make_public
, which is a mutable reference to a vector of AssignedValue
s. We'll talk about AssignedValue
s below, but you can assume this vector starts off empty; then you push onto it any witness values that you would like to make public. By default, all witness values are considered private, so you must consciously decide to make something public.
Let's begin looking at the code inside some_algorithm_in_zk
now.
Here the x: F
on the right hand side is our initial input. We need to add it into our system in order to do anything with it. This is done by ctx.load_witness
, which places the value x
in the first row of our table:
Advice  Selector 


To use x
later, we want a pointer to both the value of x
and its location in the table (i.e., it's row index). This is what is returned in the x
on the left hand side, which is of type AssignedValue<F>
. The AssignedValue
struct is simply a pointer containing the information of value and cell location.
This assigned x
can now be thought of as a private input: by default all witness values in Halo2 are considered private. If we want to make this a public input, i.e., an input the Verifier has access to, we need to explicitly add it to the list of public values:
(The order you push values to make_public
determines the order the public values are read by the Verifier.)
Now we want to make use of the existing library functions of halo2lib
. These are contained in GateChip
. This struct only needs to be created once for the duration of the program. It contains some precomputed constants for optimization and is otherwise just a container for various common functions we found helpful for development. The list of available functions is provided below.
For example, we would like to compute x**2
. GateChip
contains a mul
function, so we can call
What this function does behind the scenes is assign intermediate numbers to the advice column and turn on the appropriate selectors to properly constrain the computation logic (both by mutating ctx
). It then returns an AssignedValue
pointing to the output of the multiplication operation, somewhere in our table.
If we look at the function declaration of mul
, it is
We have described all the structs here except QuantumCell<F>
.
What is a QuantumCell
?
QuantumCell
?A QuantumCell
is a convenience enum we have introduced because there are several slightly different scenarios under which you want to add a value into the advice column:
You want to reuse or reference an existing value from some previous part of your computation. In this case the previous value is already in the table, so it is in the form of an
AssignedValue
. This corresponds to theExisting
enum option. More technically, what happens when you add an existing cella
into the table is that it will assign a new cell into the advice column with value equal to the value ofa
. Then it will impose an equality constraint between the new cell and the cell ofa
so the Verifier has a guarantee that these two cells are always equal.You want to add an entirely new number into the table. For example, this was the case when we were supplying a private input. This corresponds to the
Witness(F)
option.The
WitnessFraction
option is similar toWitness
but is used for optimization purposes, so we won't go over it here (and on first pass you never need to use it).You want to use a number in your computation that should be a known constant. Here "known" means known at circuit creation time to both the Prover and Verifier. This corresponds to the
Constant(F)
option. What happens behind the scenes when you assign a constant number is that there is actually another secret "Fixed" column in the table which is fixed at circuit creation time. When you assign aConstant
number, you are adding this number to the Fixed column, adding the number as a witness to the Advice column, and then imposing an equality constraint between the two corresponding cells.
When you place a number into the table, we do want you to be mindful of which of these cases you are using. However this mindfulness should not lead to extra code bloat or excessive case handling. Instead, you just need to specify which enum
option in QuantumCell
it corresponds to, and the technical operations described above are done for you.
Now that we have discussed QuantumCell
, we mention that an equivalent way to call gate.mul(ctx, x, x)
is to write
However we discovered that most "values" used in a computation are usually pointers to values from previous functions, aka AssignedValue
. Therefore we removed the necessity to always type Existing
. Now whenever you specify an AssignedValue,
rust is smart enough to infer it is of enum option Existing
.
Now the rest of this code snippet should make sense:
We took the result of the x**2
computation, x_sq
, add the constant number 72
to it, and then declare this output witness value public.
In our discussion we have distinguished between public inputs vs outputs because this is the more familiar viewpoint from a Prover computation perspective. However Halo2 does not make this distinction: since the Verifier sees all public inputs and outputs at the same time, there is no distinction in Halo2 between inputs and outputs. This is why both the input and the output were pushed to the same make_public
vector.
This got us through an entire complete ZK computation! You can run
to see the MockProver run in action.
But wait, there's more code in the example?
Diving deeper: ctx.assign_region
ctx.assign_region
What is gate.mul
really doing behind the scenes? Remember our table started off with just
Advice  Selector 

 0 
The call gate.mul(ctx, x, x)
fills in the following values into our table:
Advice  Selector 

 0 
 1 
 0 
 0 
 0 
and constrains that the advice values in rows 2, 3 must equal the one in row 0. Observe that the selector value 1
in row 1 imposes the constrain 0 + x * x == x**2
, which constrains that the value in row 4 must equal the product of the values in rows 2, 3.
If you look at the implementation of mul
, this is exactly what the function is doing by making the following "raw" calls:
The ctx.assign_region
function can be thought of as a lowlevel function to write assemblylevel code. The first argument tells the system to lay down 4 new values. The second argument specifies the relative row offsets (with respect to the tobelaiddown values) to turn on (put a 1
in) selector cells. Because we already had 1
row in our table, the argument [0]
tells it to enable the selector in row 1 + 0 = 1
. Lastly, assign_region
only lays down the cells. To access the AssignedValue
s, you can call ctx.get(isize)
to access an index in the current list of advice values. Asking for ctx.get(1)
returns the last advice value, which is the pointer to the cell where the witness value x**2
gets assigned.
Note that in this lowlevel language, we had to separately supply the witness value val
for x**2
. This is first inserted into the table as a Witness
because this is the first time the system has seen the value; then separately the selector is what constrains that this value must be correctly computed. Lastly, once it is inserted into the table, we use the pointer to its position as an AssignedValue
for downstream computations.
The pattern of calling ctx.assign_region
and then ctx.get(1)
is so common that we provide a convenience function ctx.assign_region_last
that does both at once.
Optimizing
First, it is an exercise to see that the function calls up to now result in the following table:
Advice  Selector 

 0 
 1 
 0 
 0 
 0 
 1 
 0 
 0 
 0 
In the halo2lib
interface, one can estimate cost modeling by simply counting the total number of advice cells used by the circuit. In this case, we have used 9
advice cells total. Can we do better?
Yes! Because our custom gate is of the form s * (a + b * c  d) == 0
, it is uniquely wellsuited for the multiplythenadd operation. We could instead use the following table:
Advice  Selector 

 0 
 1 
 0 
 0 
 0 
We implement this with the following code:
Finally, this multiplyandadd pattern is common enough that we provide a special function that does the above assignment for you:
For debugging purposes or to create tests to check your circuit's computation against some other rustnative computation, do you print out any of the witness values in the circuit and do assertion checks using usual rust commands:
This completes the walkthrough of the halo2_lib.rs
example. To write your own circuit, you can copy halo2_lib.rs
to its own file my_example.rs
, replace some_algorithm_in_zk
with your own implementation, and run
Again, you can find the available API functions for GateInstructions
here.
When interacting with numbers in a ZK circuit, one often ends up needing an operation called range_check
of constraining that a field element number x
is within a certain number of bits. In halo2lib
, we offer this functionality in a separate RangeChip
.
The available functions for RangeChip
are provided below.
RangeChip
is a generalization of GateChip
from the previous example. In fact, a RangeChip
contains a GateChip
(and its associated functions) which can be accessed via
The general structure of some_algorithm_in_zk
is the same in this example as in the previous example.
You only need to create a RangeChip
once for the entire duration of the circuit runtime (which automatically creates a GateChip
as well).
The default constructor for RangeChip
requires an additional parameter lookup_bits
. For compatibility with some automatic circuit setup stuff hidden in the scaffold::mock
function, you should always get this from the environmental variable LOOKUP_BITS
:
Now given some x: AssignedValue<F>
, we can check that it has 64 bits, i.e., constrain that x
is in [0, 2**64)
using the function
Note that range_check
allows you to perform a range check on an arbitrary number of bits, independent of the value of lookup_bits
. This is because we have already implemented some extra logic in range_check
to provide this extra level of generality.
Diving deeper: lookup tables
Why is RangeChip
a separate struct from GateChip
? This is because behind the scenes, the implementation of range_check
uses a new Halo2 feature: lookup tables. We will not go into the details around lookup tables here, but an overview is that we create a table with the numbers [0, 2**lookup_bits)
. Then Halo2 provides an API features that allows us to constrain whether a field element appear in this table.
For example, if lookup_bits = 8
, we can prove a number is in 64
bits by decomposing it into 8 bytes (8
bits each), proving the decomposition is correct, and additionally use the lookup table to prove each byte is actually a byte.
Without a lookup table, the traditional way to perform all range checks is to decompose a number into its bit representation, prove the bit decomposition is correct, and then prove each bit is a bit. For large bits to range check, you can see how the lookup table approach can be more efficient than the bit decomposition approach.
Technical detail: How to choose LOOKUP_BITS
LOOKUP_BITS
You can run this example via
Here the environment variable DEGREE
specifies that the circuit will have 2**DEGREE
rows. You can let LOOKUP_BITS
be any (nonzero) number less than DEGREE
. As we mentioned, the value of LOOKUP_BITS
doesn't affect the functionality of range_check
.
However, the choice of LOOKUP_BITS
will affect circuit performance. Here are some rough guidelines:
If you know you will only do lookups on a fixed number of bits, then set
LOOKUP_BITS
to that number.If you will be doing variable length range checks, generally you should set
LOOKUP_BITS = DEGREE  1
.
We recommend ignoring this example unless you are already familiar with the Poseidon hash function and have a particular need to use it in your ZK circuit.
The structure of this example is very similar to the one in the halo2_lib example. Here we call the function hash_two
instead of some_algorithm_in_zk
. In this case there are two input field elements x, y
so the second parameter field has type [F; 2]
.
We load both x, y
into the table as private inputs, and then make them public.
We create a GateChip
as usual. Now we create a separate PoseidonChip
. This stores the precomputed round constants for the Poseidon hash. It is made mutable
because it also stores the state of the Poseidon sponge, which changes as you call other functions.
This "absorbs" both x, y
into the Poseidon sponge. This mutates the state stored inside poseidon
.
This squeezes out a new hash from the Poseidon sponge. The squeeze
function gives an example of how you can structure a general reusable library function that builds on top of halo2lib
: squeeze(ctx, &gate)
takes in both the ctx
and gate: GateChip
; internally it does some computation in a very similar way to how some_algorithm_in_zk
is structured.
So general template for how to structure a reusable function that uses GateChip
would be:
where the input type could for example be AssignedValue<F>
or Vec<AssignedValue<F>>
.
Available API functions
GateChip
functions
GateChip
functionsThe list of available functions in GateChip
is below. For more details, see the GateInstructions
trait, which GateChip
implements.
Basic arithmetic operations
Unary assertion operations
Bit operations
Array selection functions
Accumulating functions
RangeChip
functions
RangeChip
functionsSimilarly, we provide the list of functions in RangeChip
. For more details, see the RangeInstructions
trait, which RangeChip
implements.
Range check
Comparison operations
Integer remainder operations
halo2ecc
halo2ecc
To see an entire library of elliptic curve cryptographic primitives that we built on top of GateChip
and RangeChip
, see the crate halo2ecc
.
Exercise
What is the most optimal way to compute the dot product $(a_0,\dotsc, a_n) \cdot (b_0,\dotsc,b_n) = a_0\cdot b_0 + \dotsc + a_n \cdot b_n$ using just the halo2lib
gate above?
Here "compute" means that you can copy in the values of $a_0,\dotsc,a_n, b_0,\dotsc,b_n$ into any cells you want. And you should have enough constraints to constrain that the final cell must have value equal to the dot product.
You can find a solution to this exercise in our code.
Feature: more columns
In our description of the halo2lib
interface above, we had a single advice column and a single selector column. For a big computation, the number of rows in this table will get very large. For the Prover, this means they need to perform certain operations on a very large vector (column). These operations include Fast Fourier Transform and certain elliptic curve operations (multiscalar multiplication). For performance, it is generally faster to parallelize such operations across multiple vectors of shorter length instead of a single large vector.
In the halo2 context, this translates to the preference for multiple columns in a table with less rows (while keeping total number of cells the same). There is a natural way to do this: we simply take our single advice column and single selector column, divide it up into chunks, and rearrange the table to have more columns:
Advice 0  Selector 0  Advice 1  Selector 1  ... 

$a_0$  $s_0$  $b_0$  $t_0$  
$a_1$  $s_1$  $b_1$  $t_1$  
$a_2$  $s_2$  $b_2$  $t_2$  
$\vdots$  $\vdots$  $\vdots$  $\vdots$ 
(We glossed over that there is a technicality that you should not divide a column in the middle of an "enabled" gate.)
The halo2lib
does this division from 1
column into multiple columns automatically: you specify the environmental variable DEGREE
, which specifies that the desired number of rows of the circuit is 2 ** DEGREE
(it must be a power of two for FFT reasons). Then halo2lib
will autoconfigure your circuit from 1
column into the minimum number of columns necessary to fit within the desired number of rows.
Why not just increase the number of columns indefinitely? There is a limit to parallelism, so generally the proving time vs. number of columns plot looks parabolic: as you increase number of columns (while keeping number of cells the same), the proving time will decrease up to a point before starting to increase again.
Lastly, the improvement to proving time performance from increasing the number of columns is not free. It comes at the cost of increasing the burden of computation for the Verifier. On the CPU this means longer Verifier times. On the EVM this means to verify a ZK proof onchain, the gas cost increases as you increase the number of columns used.
Saved reading for later
If you find that halo2lib
does not provide enough functionality for your ZK circuit needs, or if you are just curious, you can check out the full "vanilla" Halo2 API documention in the halo2 book.
We have also assembled a Halo2 Cheatsheet with a growing collection of observations we found helpful when first interacting with the vanilla Halo2 API.
Last updated