Halo2 Cheatsheet

tags: explainers

We are using halo2 with the PSE fork. The official documentation is the halo2 book as well as the rustdocs.

There are many concepts and many are hard to grasp when first interacting with the API. This living doc serves as a troubleshooting page to address common questions that arise.

PLONKish arithmetization

PLONKish arithmetization is the format in which you specify a ZK circuit design to the Halo2 API.

It is helpful to read this PLONK example first as a warm-up.

PLONKish arithmetization is a more general framework than PLONK in which you are filling in a big matrix with an arbitrary number of columns and 2^K rows (for Fast Fourier Transform (FFT) purposes the row number must be a power of 2). There are several different kinds of columns:

• Advice
• Fixed
• Selector
• Table

Advice columns are the ones where the entries (called witnesses) are filled in each time you produce a proof. So they correspond to the execution trace of whatever computation you are ZK proving.

The other columns {Fixed, Selector, Table} are all decided once and for all and then committed to by the Prover and Verifier by encoding them into proving key and verifying key.

• Fixed columns contain constant numbers. These are used either if you need a constant number in some computation as part of witness calculation, or if you specify a constant number as part of a custom gate
• Selectors are the same as fixed columns except they only take values 0,1. They are used purely to turn on/off gates & lookup arguments. There is also some slight performance improvement on the backend because they use bool values instead of field elements so computations are faster.
  • There is another more advanced optimization of selector combining that I will not go over
• Table columns are used for lookup tables: this is a powerful feature (and our primary reason for using Halo2) where you can fill in a column with pre-determined numbers, and then there is a constraint to check that an advice value must equal one of the numbers in the column. For example, a common use case is to have a column with 0,...,2^n - 1,0,0,... in order to check that a number is n bits or less. You can also perform lookup arguments on tuples of advice values using tuples of Table Columns.
  • To check a number is n bits or less is equivalent to checking it is in the range [0, 2^n). Since the column can be longer than 2^n in length, we need every element in the column to be in the range [0, 2^n). The default way to do this is to just fill it with 0,..., 2^n - 1 and then fill the rest with 0s.

Scaffolding

There is a lot of overhead to setting up any halo2 environment. Fortunately, you can usually just copy/paste the same skeleton around at the beginning, and VSCode will also auto-suggest the rest.

We have provided some basic examples and scaffolding here.

In particular you can see the various commands needed to run the actual production-used prover.

Walkthrough

Creating a circuit entails creating a struct that implements the Circuit trait:

/// This is a trait that circuits provide implementations for so that the
/// backend prover can ask the circuit to synthesize using some given
/// [`ConstraintSystem`] implementation.
pub trait Circuit<F: Field> {
    /// This is a configuration object that stores things like columns.
    type Config: Clone;
    /// The floor planner used for this circuit. This is an associated type of the
    /// `Circuit` trait because its behaviour is circuit-critical.
    type FloorPlanner: FloorPlanner;

    /// Returns a copy of this circuit with no witness values (i.e. all witnesses set to
    /// `None`). For most circuits, this will be equal to `Self::default()`.
    fn without_witnesses(&self) -> Self;

    /// The circuit is given an opportunity to describe the exact gate
    /// arrangement, column arrangement, etc.
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config;

    /// Given the provided `cs`, synthesize the circuit. The concrete type of
    /// the caller will be different depending on the context, and they may or
    /// may not expect to have a witness present.
    fn synthesize(&self, config: Self::Config, layouter: impl Layouter<F>) -> Result<(), Error>;
}

The Config is another struct you must define that contains the information about what types & numbers of columns the circuit will have. It is created in the configure function. One important thing to note is that Config is passed immutably to synthesize, so the struct should not contain any data that you want to change during witness generation.

The general design is that one thinks of a Config as a "chip", which can be built up out of smaller chips. Each chip can then have some built in functions that are called during witness generation.

The configure function is also where you define all your custom gates using meta.create_gate and creating lookup table rules with meta.lookup. For an example of creating a lookup table, see here. The actual values of lookup table are filled in during synthesize.

The synthesize function can be thought of as performing the actual computation (aka witness generation), filling in all the advice values for a particular proof. However it is also used to specify when to turn on which custom gates / lookup arguments, and what equality constraints to impose. (It is easier to logic about these constraints while executing the computation.)

However because of this, the above Circuit trait (and the synthesize function in particular) are called in several distinct settings: verifying key generation, proving key generation, actual proof generation. Some functions do different things (or even nothing) in these different settings. In the vkey and pkey generation settings, we only care about non-advice cells – which should not depend on values in the advice cells.

For this reason, as a security feature, the API has wrapped advice values in a Value<F> struct, which is basically a wrapper for Option<F> with arithmetic operator overloading. The point is just that you should be able to create vkey & pkey even if these values are Value::unknown().

FAQ: Config vs. Chip vs. Circuit

After looking at some example Halo2 code, you will soon find two names that often occur: Config and Chip and Circuit. There is often some confusion around these.

Ideologically, a Config is simply the skeleton of the circuit: it is a struct that remembers how many columns of each type the circuit has and assigns each column an index for later reference.

On the other hand, a Chip is a collection of functions that you would like the circuit to be able to calculate and constrain. For example, given a, b you may want <Chip>.add(a,b) to constrain out == a + b using your gates and supply the witness value for out (equal to a + b).

However as you might have noticed, there is no reason you cannot simply add the Chip functions to the Config struct itself. And often this is what is done in practice for convenience. As a result, something can be named RangeConfig but actually also perform the functionalities of a RangeChip.

We usually only call a struct a _Circuit if it implements the Halo2 Circuit trait. Usually the MyCircuit struct only contains the specific inputs to the ZK circuit. The implementation of the Circuit specifies the Config struct (aka the circuit's skeleton), and then the synthesize function calls functions provided by various Chips to compute and constrain the desired computation in ZK.

In summary, a Config and a Chip together can be thought of as a re-usable gadget with some functionality, which can be placed into multiple different circuits. A circuit is the final assembly of a collection of Configs and Chips together with a specify ordering of function calls to Chip functions. The Circuit is then compiled to produce the final output in the form of two binaries that run the Prover and Verifier programs.

If this all went over your head on first reading, that's totally fine!

Cost modeling

This section gives a very incomplete sketch of some heuristics around how to think about Halo2 performance and costs.

The overall goal is to get the time spent in create_proof call to be as fast as possible. This separates into the time spent doing everything in synthesize function (aka witness generation / front end stuff) and then all the backend computations to generate the final proof (these are mostly FFTs and elliptic curve operations).

One might want to separately measure just the time spent in the synthesize call because the backend computation speed can vary more drastically depending on parallelization / multi-threading. But to stay focused, we will just target the total proving time.

Predicting the time cost of a halo2 circuit turns out to be rather difficult. Often you just need to run the end result to know definitively. Some general guidelines are:

• Obviously the more cells you use the slower it'll be
• For two circuits with the same number of cells, the one with more columns (hence less rows) is usually faster because stuff can be parallelized on a per-column basis in the backend. This is only true up to a certain point, and also the fact that rows must be power of 2 has an impact.
• High degree custom gates are slower.
• Lookup arguments are approximately similar to a degree 4 custom gate.
• The number of operations needed to evaluate the expression for your custom gate has some performance impact
• If different custom gates access rows at different Rotation(offset)s, then the number of distinct sets of rotation offsets impacts speed a lot
• Empirically, accessing a large number of rotation offsets also seems to have performance impact, but that may just be because the number of operations goes up

For large circuits, the time spent in witness generation is also a concern. There it is mostly normal computing performance considerations, but something to keep in mind is that the halo2 backend stores numbers in the prime field

${\mathbb{F}}_r$, where r = 21888242871839275222246405745257275088548364400416034343698204186575808495617 is 254 bits. This means the backend stores every number as a fixed 4-tupe of u64 and every arithmetic operation is a BigInt modular arithmetic operation (these have been optimized using Montgomery form but still expensive). If the circuit operations are mostly with small u64 numbers and use normal compute architecture, it may be worth keeping track of everything on the front end with u64, and only converting to Fr when assigning a cell. Note the conversion to Fr involves a field multiplication because it is really converting from "normal" form to Montgomery form.