halo2

IMPORTANT: This library is being actively developed and should not be used in production software.

You may use this package under the Transitive Grace Period Public Licence, version 1.0, or at your option, any later version. See the file LICENSE-TGPPL for the terms of the Transitive Grace Period Public Licence, version 1.0.

The purpose of the TGPPL is to allow commercial improvements to the package while ensuring that all improvements are eventually open source. See here for why the TGPPL exists, graphically illustrated on three slides.

Concepts

User Documentation

You're probably here because you want to write circuits? Excellent!

This section will guide you through the process of creating circuits with halo2.

A simple example

Let's start with a simple circuit, to introduce you to the common APIs and how they are used. The circuit will take a public input $c$ , and will prove knowledge of two private inputs $a$ and $b$ such that

$a \cdot b = c .$


#![allow(unused)]
fn main() {
extern crate halo2;
use halo2::arithmetic::FieldExt;

struct MyCircuit<F: FieldExt> {
    a: F,
    b: F,
}
}

TODO

Lookup tables

In normal programs, you can trade memory for CPU to improve performance, by pre-computing and storing lookup tables for some part of the computation. We can do the same thing in halo2 circuits!

A lookup table can be thought of as enforcing a relation between variables, where the relation is expressed as a table. Assuming we have only one lookup argument in our constraint system, the total size of tables is constrained by the size of the circuit: each table entry costs one row, and it also costs one row to do each lookup.

TODO

Gadgets

Tips and tricks

This section contains various ideas and snippets that you might find useful while writing halo2 circuits.

Small range constraints

A common constraint used in R1CS circuits is the boolean constraint: $b * (1 - b) = 0$ . This constraint can only be satisfied by $b = 0$ or $b = 1$ .

In halo2 circuits, you can similarly constrain a cell to have one of a small set of values. For example, to constrain $a$ to the range $[0 . . 5]$ , you would create a gate of the form:

$a \cdot (1 - a) \cdot (2 - a) \cdot (3 - a) \cdot (4 - a) = 0$

while to constraint $c$ to be either 7 or 13, you would use:

$(7 - c) \cdot (13 - c) = 0$

The underlying principle here is that we create a polynomial constraint with roots at each value in the set of possible values we want to allow. In R1CS circuits, the maximum supported polynomial degree is 2 (due to all constraints being of the form $a * b = c$ ). In halo2 circuits, you can use arbitrary-degree polynomials - with the proviso that higher-degree constraints are more expensive to use.

Note that the roots don't have to be constants; for example $(a - x) \cdot (a - y) \cdot (a - z) = 0$ will constrain $a$ to be equal to one of ${x, y, z}$ where the latter can be arbitrary polynomials, as long as the whole expression stays within the maximum degree bound.

The halo2 Book