halo2

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

Documentation

License

Copyright 2020 The Electric Coin Company.

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\ast (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\ast 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.

Design

Permutation argument

Given that gates in halo2 circuits operate "locally" (on cells in the current row or defined relative rows), it is common to need to copy a value from some arbitrary cell into the current row for use in a gate. This is performed with an equality constraint, which enforces that the source and destination cells contain the same value.

We implement these equality constraints by constructing a permutation that represents the constraints, and then using a permutation argument within the proof to enforce them.

Notation

A permutation is a one-to-one and onto mapping of a set onto itself. A permutation can be factored uniquely into a composition of cycles (up to ordering of cycles, and rotation of each cycle).

We sometimes use cycle notation to write permutations. Let $(abc)$ denote a cycle where $a$ maps to $b$, $b$ maps to $c$, and $c$ maps to $a$ (with the obvious generalisation to arbitrary-sized cycles). Writing two or more cycles next to each other denotes a composition of the corresponding permutations. For example, $(ab)(cd)$ denotes the permutation that maps $a$ to $b$, $b$ to $a$, $c$ to $d$, and $d$ to $c$.

Constructing the permutation

Goal

We want to construct a permutation in which each subset of variables that are in a equality-constraint set form a cycle. For example, suppose that we have a circuit that defines the following equality constraints:

• $a\equiv b$
• $a\equiv c$
• $d\equiv e$

From this we have the equality-constraint sets $\{a,b,c\}$ and $\{d,e\}$. We want to construct the permutation:

$$(abc)(de)$$

which defines the mapping of $[a,b,c,d,e]$ to $[b,c,a,e,d]$.

Algorithm

We need to keep track of the set of cycles, which is a set of disjoint sets. Efficient data structures for this problem are known; for the sake of simplicity we choose one that is not asymptotically optimal but is easy to implement.

We represent the current state as:

• an array $\mathsf{m}\mathsf{a}\mathsf{p}\mathsf{p}\mathsf{i}\mathsf{n}\mathsf{g}$ for the permutation itself;
• an auxiliary array $\mathsf{a}\mathsf{u}\mathsf{x}$ that keeps track of a distinguished element of each cycle;
• another array $\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}$ that keeps track of the size of each cycle.

We have the invariant that for each element $x$ in a given cycle $C$, $\mathsf{a}\mathsf{u}\mathsf{x}(x)$ points to the same element $c\in C$. This allows us to quickly decide whether two given elements $x$ and $y$ are in the same cycle, by checking whether $\mathsf{a}\mathsf{u}\mathsf{x}(x)=\mathsf{a}\mathsf{u}\mathsf{x}(y)$. Also, $\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(x))$ gives the size of the cycle containing $x$. (This is guaranteed only for $\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(x)))$, not for $\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(x)$.)

The algorithm starts with a representation of the identity permutation: for all $x$, we set $\mathsf{m}\mathsf{a}\mathsf{p}\mathsf{p}\mathsf{i}\mathsf{n}\mathsf{g}(x)=x$, $\mathsf{a}\mathsf{u}\mathsf{x}(x)=x$, and $\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(x)=1$.

To add an equality constraint $left\equiv right$:

1. Check whether $left$ and $right$ are already in the same cycle, i.e. whether $\mathsf{a}\mathsf{u}\mathsf{x}(left)=\mathsf{a}\mathsf{u}\mathsf{x}(right)$. If so, there is nothing to do.
2. Otherwise, $left$ and $right$ belong to different cycles. Make $left$ the larger cycle and $right$ the smaller one, by swapping them iff $\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(left))<\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(right))$.
3. Following the mapping around the right (smaller) cycle, for each element $x$ set $\mathsf{a}\mathsf{u}\mathsf{x}(x)=\mathsf{a}\mathsf{u}\mathsf{x}(left)$.
4. Splice the smaller cycle into the larger one by swapping $\mathsf{m}\mathsf{a}\mathsf{p}\mathsf{p}\mathsf{i}\mathsf{n}\mathsf{g}(left)$ with $\mathsf{m}\mathsf{a}\mathsf{p}\mathsf{p}\mathsf{i}\mathsf{n}\mathsf{g}(right)$.

For example, given two disjoint cycles $(ABCD)$ and $(EFGH)$:

A +---> B
^       +
|       |
+       v
D <---+ C       E +---> F
                ^       +
                |       |
                +       v
                H <---+ G

After adding constraint $B\equiv E$ the above algorithm produces the cycle:

A +---> B +-------------+
^                       |
|                       |
+                       v
D <---+ C <---+ E       F
                ^       +
                |       |
                +       v
                H <---+ G

Broken alternatives

If we did not check whether $left$ and $right$ were already in the same cycle, then we could end up undoing an equality constraint. For example, if we have the following constraints:

• $a\equiv b$
• $b\equiv c$
• $c\equiv d$
• $b\equiv d$

and we tried to implement adding an equality constraint just using step 4 of the above algorithm, then we would end up constructing the cycle $(ab)(cd)$, rather than the correct $(abcd)$.

Argument specification

TODO: Document what we do with the permutation once we have it.