halo2

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

Documentation

Minimum Supported Rust Version

Requires Rust 1.51 or higher.

Minimum supported Rust version can be changed in the future, but it will be done with a minor version bump.

License

Copyright 2020 The Electric Coin Company.

You may use this package under the Bootstrap Open Source Licence, version 1.0, or at your option, any later version. See the file LICENSE-BOSL for the terms of the Bootstrap Open Source Licence, version 1.0.

The purpose of the BOSL is to allow commercial improvements to the package while ensuring that all improvements are open source. See here for why the BOSL exists.

Concepts

First we'll describe the concepts behind zero-knowledge proof systems; the arithmetization (kind of circuit description) used by Halo 2; and the abstractions we use to build circuit implementations.

Proof systems

The aim of any proof system is to be able to prove interesting mathematical or cryptographic statements.

Typically, in a given protocol we will want to prove families of statements that differ in their public inputs. The prover will also need to show that they know some private inputs that make the statement hold.

To do this we write down a relation, $\mathcal{R}$, that specifies which combinations of public and private inputs are valid.

The terminology above is intended to be aligned with the ZKProof Community Reference.

To be precise, we should distinguish between the relation $\mathcal{R}$, and its implementation to be used in a proof system. We call the latter a circuit.

The language that we use to express circuits for a particular proof system is called an arithmetization. Usually, an arithmetization will define circuits in terms of polynomial constraints on variables over a field.

The process of expressing a particular relation as a circuit is also sometimes called "arithmetization", but we'll avoid that usage.

To create a proof of a statement, the prover will need to know the private inputs, and also intermediate values, called advice values, that are used by the circuit.

We assume that we can compute advice values efficiently from the private and public inputs. The particular advice values will depend on how we write the circuit, not only on the high-level statement.

The private inputs and advice values are collectively called a witness.

Some authors use "witness" as just a synonym for private inputs. But in our usage, a witness includes advice, i.e. it includes all values that the prover supplies to the circuit.

For example, suppose that we want to prove knowledge of a preimage $x$ of a hash function $H$ for a digest $y$:

• The private input would be the preimage $x$.

• The public input would be the digest $y$.

• The relation would be $\{(x,y):H(x)=y\}$.

• For a particular public input $Y$, the statement would be: $\{(x):H(x)=Y\}$.

• The advice would be all of the intermediate values in the circuit implementing the hash function. The witness would be $x$ and the advice.

A Non-interactive Argument allows a prover to create a proof for a given statement and witness. The proof is data that can be used to convince a verifier that there exists a witness for which the statement holds. The security property that such proofs cannot falsely convince a verifier is called soundness.

A Non-interactive Argument of Knowledge (NARK) further convinces the verifier that the prover knew a witness for which the statement holds. This security property is called knowledge soundness, and it implies soundness.

In practice knowledge soundness is more useful for cryptographic protocols than soundness: if we are interested in whether Alice holds a secret key in some protocol, say, we need Alice to prove that she knows the key, not just that it exists.

Knowledge soundness is formalized by saying that an extractor, which can observe precisely how the proof is generated, must be able to compute the witness.

This property is subtle given that proofs can be malleable. That is, depending on the proof system it may be possible to take an existing proof (or set of proofs) and, without knowing the witness(es), modify it/them to produce a distinct proof of the same or a related statement. Higher-level protocols that use malleable proof systems need to take this into account.

Even without malleability, proofs can also potentially be replayed. For instance, we would not want Alice in our example to be able to present a proof generated by someone else, and have that be taken as a demonstration that she knew the key.

If a proof yields no information about the witness (other than that a witness exists and was known to the prover), then we say that the proof system is zero knowledge.

If a proof system produces short proofs —i.e. of length polylogarithmic in the circuit size— then we say that it is succinct. A succinct NARK is called a SNARK (Succinct Non-Interactive Argument of Knowledge).

By this definition, a SNARK need not have verification time polylogarithmic in the circuit size. Some papers use the term efficient to describe a SNARK with that property, but we'll avoid that term since it's ambiguous for SNARKs that support amortized or recursive verification, which we'll get to later.

A zk-SNARK is a zero-knowledge SNARK.

UltraPLONK Arithmetization

The arithmetization used by Halo 2 comes from PLONK, or more precisely its extension UltraPLONK that supports custom gates and lookup arguments. We'll call it UPA (UltraPLONK arithmetization).

The term UPA and some of the other terms we use to describe it are not used in the PLONK paper.

UPA circuits are defined in terms of a rectangular matrix of values. We refer to rows, columns, and cells of this matrix with the conventional meanings.

A UPA circuit depends on a configuration:

• A finite field $\mathbb{F}$, where cell values (for a given statement and witness) will be elements of $\mathbb{F}$.

• The number of columns in the matrix, and a specification of each column as being fixed, advice, or instance. Fixed columns are fixed by the circuit; advice columns correspond to witness values; and instance columns are normally used for public inputs (technically, they can be used for any elements shared between the prover and verifier).

• A subset of the columns that can participate in equality constraints.

• A polynomial degree bound.

• A sequence of polynomial constraints. These are multivariate polynomials over $\mathbb{F}$ that must evaluate to zero for each row. The variables in a polynomial constraint may refer to a cell in a given column of the current row, or a given column of another row relative to this one (with wrap-around, i.e. taken modulo $n$). The maximum degree of each polynomial is given by the polynomial degree bound.

• A sequence of lookup arguments defined over tuples of input expressions (which are multivariate polynomials as above) and table columns.

A UPA circuit also defines:

• The number of rows $n$ in the matrix. $n$ must correspond to the size of a multiplicative subgroup of ${\mathbb{F}}^{\times }$; typically a power of two.

• A sequence of equality constraints, which specify that two given cells must have equal values.

• The values of the fixed columns at each row.

From a circuit description we can generate a proving key and a verification key, which are needed for the operations of proving and verification for that circuit.

Note that we specify the ordering of columns, polynomial constraints, lookup arguments, and equality constraints, even though these do not affect the meaning of the circuit. This makes it easier to define the generation of proving and verification keys as a deterministic process.

Typically, a configuration will define polynomial constraints that are switched off and on by selectors defined in fixed columns. For example, a constraint $q_i\cdot p(...)=0$ can be switched off for a particular row $i$ by setting $q_i=0$. In this case we sometimes refer to a set of constraints controlled by a set of selector columns that are designed to be used together, as a gate. Typically there will be a standard gate that supports generic operations like field multiplication and division, and possibly also custom gates that support more specialized operations.

Chips

The previous section gives a fairly low-level description of a circuit. When implementing circuits we will typically use a higher-level API which aims for the desirable characteristics of auditability, efficiency, modularity, and expressiveness.

Some of the terminology and concepts used in this API are taken from an analogy with integrated circuit design and layout. As for integrated circuits, the above desirable characteristics are easier to obtain by composing chips that provide efficient pre-built implementations of particular functionality.

For example, we might have chips that implement particular cryptographic primitives such as a hash function or cipher, or algorithms like scalar multiplication or pairings.

In UPA, it is possible to build up arbitrary logic just from standard gates that do field multiplication and addition. However, very significant efficiency gains can be obtained by using custom gates.

Using our API, we define chips that "know" how to use particular sets of custom gates. This creates an abstraction layer that isolates the implementation of a high-level circuit from the complexity of using custom gates directly.

Even if we sometimes need to "wear two hats", by implementing both a high-level circuit and the chips that it uses, the intention is that this separation will result in code that is easier to understand, audit, and maintain/reuse. This is partly because some potential implementation errors are ruled out by construction.

Gates in UPA refer to cells by relative references, i.e. to the cell in a given column, and the row at a given offset relative to the one in which the gate's selector is set. We call this an offset reference when the offset is nonzero (i.e. offset references are a subset of relative references).

Relative references contrast with absolute references used in equality constraints, which can point to any cell.

The motivation for offset references is to reduce the number of columns needed in the configuration, which reduces proof size. If we did not have offset references then we would need a column to hold each value referred to by a custom gate, and we would need to use equality constraints to copy values from other cells of the circuit into that column. With offset references, we not only need fewer columns; we also do not need equality constraints to be supported for all of those columns, which improves efficiency.

In R1CS (another arithmetization which may be more familiar to some readers, but don't worry if it isn't), a circuit consists of a "sea of gates" with no semantically significant ordering. Because of offset references, the order of rows in a UPA circuit, on the other hand, is significant. We're going to make some simplifying assumptions and define some abstractions to tame the resulting complexity: the aim will be that, at the gadget level where we do most of our circuit construction, we will not have to deal with relative references or with gate layout explicitly.

We will partition a circuit into regions, where each region contains a disjoint subset of cells, and relative references only ever point within a region. Part of the responsibility of a chip implementation is to ensure that gates that make offset references are laid out in the correct positions in a region.

Given the set of regions and their shapes, we will use a separate floor planner to decide where (i.e. at what starting row) each region is placed. There is a default floor planner that implements a very general algorithm, but you can write your own floor planner if you need to.

Floor planning will in general leave gaps in the matrix, because the gates in a given row did not use all available columns. These are filled in —as far as possible— by gates that do not require offset references, which allows them to be placed on any row.

Chips can also define lookup tables. If more than one table is defined for the same lookup argument, we can use a tag column to specify which table is used on each row. It is also possible to perform a lookup in the union of several tables (limited by the polynomial degree bound).

Composing chips

In order to combine functionality from several chips, we compose them in a tree. The top-level chip defines a set of fixed, advice, and instance columns, and then specifies how they should be distributed between lower-level chips.

In the simplest case, each lower-level chips will use columns disjoint from the other chips. However, it is allowed to share a column between chips. It is important to optimize the number of advice columns in particular, because that affects proof size.

The result (possibly after optimization) is a UPA configuration. Our circuit implementation will be parameterized on a chip, and can use any features of the supported lower-level chips via the top-level chip.

Our hope is that less expert users will normally be able to find an existing chip that supports the operations they need, or only have to make minor modifications to an existing chip. Expert users will have full control to do the kind of circuit optimizations that ECC is famous for 🙂.

Gadgets

When implementing a circuit, we could use the features of the chips we've selected directly. Typically, though, we will use them via gadgets. This indirection is useful because, for reasons of efficiency and limitations imposed by UPA, the chip interfaces will often be dependent on low-level implementation details. The gadget interface can provide a more convenient and stable API that abstracts away from extraneous detail.

For example, consider a hash function such as SHA-256. The interface of a chip supporting SHA-256 might be dependent on internals of the hash function design such as the separation between message schedule and compression function. The corresponding gadget interface can provide a more convenient and familiar update/finalize API, and can also handle parts of the hash function that do not need chip support, such as padding. This is similar to how accelerated instructions for cryptographic primitives on CPUs are typically accessed via software libraries, rather than directly.

Gadgets can also provide modular and reusable abstractions for circuit programming at a higher level, similar to their use in libraries such as libsnark and bellman. As well as abstracting functions, they can also abstract types, such as elliptic curve points or integers of specific sizes.

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.

Developer tools

The halo2 crate includes several utilities to help you design and implement your circuits.

Mock prover

halo2::dev::MockProver is a tool for debugging circuits, as well as cheaply verifying their correctness in unit tests. The private and public inputs to the circuit are constructed as would normally be done to create a proof, but MockProver::run instead creates an object that will test every constraint in the circuit directly. It returns granular error messages that indicate which specific constraint (if any) is not satisfied.

Circuit visualizations

The dev-graph feature flag exposes several helper methods for creating graphical representations of circuits.

halo2::dev::circuit_layout renders the circuit layout as a grid:

• Columns are layed out from left to right as advice, instance, and fixed. The order of columns is otherwise without meaning.
  • Advice columns have a red background.
  • Instance columns have a white background.
  • Fixed columns have a blue background.
• Regions are shown as labelled green boxes (overlaying the background colour). A region may appear as multiple boxes if some of its columns happen to not be adjacent.
• Cells that have been assigned to by the circuit will be shaded in grey. If any cells are assigned to more than once (which is usually a mistake), they will be shaded darker than the surrounding cells.

halo2::dev::circuit_dot_graph builds a DOT graph string representing the given circuit, which can then be rendered witha variety of layout programs. The graph is built from calls to Layouter::namespace both within the circuit, and inside the gadgets and chips that it uses.

Cost estimator

The cost-model binary takes high-level parameters for a circuit design, and estimates the verification cost, as well as resulting proof size.

Usage: cargo run --example cost-model -- [OPTIONS] k

Positional arguments:
  k                       2^K bound on the number of rows.

Optional arguments:
  -h, --help              Print this message.
  -a, --advice R[,R..]    An advice column with the given rotations. May be repeated.
  -i, --instance R[,R..]  An instance column with the given rotations. May be repeated.
  -f, --fixed R[,R..]     A fixed column with the given rotations. May be repeated.
  -g, --gate-degree D     Maximum degree of the custom gates.
  -l, --lookup N,I,T      A lookup over N columns with max input degree I and max table degree T. May be repeated.
  -p, --permutation N     A permutation over N columns. May be repeated.

For example, to estimate the cost of a circuit with three advice columns and one fixed column (with various rotations), and a maximum gate degree of 4:

<span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.7777700000000001em;vertical-align:-0.19444em;"></span><span class="mord mathnormal">c</span><span class="mord mathnormal">a</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord mathnormal" style="margin-right:0.02778em;">or</span><span class="mord mathnormal">u</span><span class="mord mathnormal">n</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8888799999999999em;vertical-align:-0.19444em;"></span><span class="mord">−</span><span class="mord mathnormal">e</span><span class="mord mathnormal">x</span><span class="mord mathnormal">am</span><span class="mord mathnormal" style="margin-right:0.01968em;">pl</span><span class="mord mathnormal">ecos</span><span class="mord mathnormal">t</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.77777em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">m</span><span class="mord mathnormal">o</span><span class="mord mathnormal">d</span><span class="mord mathnormal">e</span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.66666em;vertical-align:-0.08333em;"></span><span class="mord">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8388800000000001em;vertical-align:-0.19444em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">1</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.72777em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.66666em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">a</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8388800000000001em;vertical-align:-0.19444em;"></span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">−</span><span class="mord">1</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">1</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8888799999999999em;vertical-align:-0.19444em;"></span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord">0</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord">411</span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span><span class="mord mathnormal">ini</span><span class="mord mathnormal">s</span><span class="mord mathnormal">h</span><span class="mord mathnormal">e</span><span class="mord mathnormal">dd</span><span class="mord mathnormal">e</span><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="mopen">[</span><span class="mord mathnormal">u</span><span class="mord mathnormal">n</span><span class="mord mathnormal">o</span><span class="mord mathnormal">pt</span><span class="mord mathnormal">imi</span><span class="mord mathnormal">ze</span><span class="mord mathnormal">d</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">+</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal">d</span><span class="mord mathnormal">e</span><span class="mord mathnormal">b</span><span class="mord mathnormal" style="margin-right:0.03588em;">ug</span><span class="mord mathnormal">in</span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord mathnormal">o</span><span class="mclose">]</span><span class="mord mathnormal">t</span><span class="mord mathnormal">a</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord mathnormal">e</span><span class="mord mathnormal">t</span><span class="mopen">(</span><span class="mord mathnormal">s</span><span class="mclose">)</span><span class="mord mathnormal">in</span><span class="mord">0.03</span><span class="mord mathnormal">s</span><span class="mord mathnormal" style="margin-right:0.00773em;">R</span><span class="mord mathnormal">u</span><span class="mord mathnormal">nnin</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord">‘</span><span class="mord mathnormal">t</span><span class="mord mathnormal">a</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord mathnormal">e</span><span class="mord mathnormal">t</span><span class="mord">/</span><span class="mord mathnormal">d</span><span class="mord mathnormal">e</span><span class="mord mathnormal">b</span><span class="mord mathnormal" style="margin-right:0.03588em;">ug</span><span class="mord">/</span><span class="mord mathnormal">e</span><span class="mord mathnormal">x</span><span class="mord mathnormal">am</span><span class="mord mathnormal" style="margin-right:0.01968em;">pl</span><span class="mord mathnormal">es</span><span class="mord">/</span><span class="mord mathnormal">cos</span><span class="mord mathnormal">t</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.77777em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">m</span><span class="mord mathnormal">o</span><span class="mord mathnormal">d</span><span class="mord mathnormal">e</span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8388800000000001em;vertical-align:-0.19444em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">1</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.72777em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8388800000000001em;vertical-align:-0.19444em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">−</span><span class="mord">1</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">1</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8888799999999999em;vertical-align:-0.19444em;"></span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord">0</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1.036108em;vertical-align:-0.286108em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord">411‘</span><span class="mord mathnormal" style="margin-right:0.07153em;">C</span><span class="mord mathnormal">i</span><span class="mord mathnormal">rc</span><span class="mord mathnormal">u</span><span class="mord mathnormal">i</span><span class="mord mathnormal">t</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03148em;">k</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">11</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">ma</span><span class="mord"><span class="mord mathnormal">x</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.33610799999999996em;"><span style="top:-2.5500000000000003em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight">d</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mord mathnormal">e</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">4</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">a</span><span class="mord mathnormal">d</span><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="mord mathnormal">i</span><span class="mord mathnormal">c</span><span class="mord"><span class="mord mathnormal">e</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.151392em;"><span style="top:-2.5500000000000003em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight">c</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mord mathnormal">o</span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mord mathnormal">u</span><span class="mord mathnormal">mn</span><span class="mord mathnormal">s</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">3</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mord mathnormal">oo</span><span class="mord mathnormal" style="margin-right:0.03148em;">k</span><span class="mord mathnormal">u</span><span class="mord mathnormal">p</span><span class="mord mathnormal">s</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">p</span><span class="mord mathnormal" style="margin-right:0.02778em;">er</span><span class="mord mathnormal">m</span><span class="mord mathnormal">u</span><span class="mord mathnormal">t</span><span class="mord mathnormal">a</span><span class="mord mathnormal">t</span><span class="mord mathnormal">i</span><span class="mord mathnormal">o</span><span class="mord mathnormal">n</span><span class="mord mathnormal">s</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mopen">[</span><span class="mclose">]</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">co</span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mord mathnormal">u</span><span class="mord mathnormal">m</span><span class="mord"><span class="mord mathnormal">n</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.15139200000000003em;"><span style="top:-2.5500000000000003em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.03588em;">q</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.286108em;"><span></span></span></span></span></span></span><span class="mord mathnormal">u</span><span class="mord mathnormal" style="margin-right:0.02778em;">er</span><span class="mord mathnormal">i</span><span class="mord mathnormal">es</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">7</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">p</span><span class="mord mathnormal">o</span><span class="mord mathnormal">in</span><span class="mord"><span class="mord mathnormal">t</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.151392em;"><span style="top:-2.5500000000000003em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight">s</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mord mathnormal">e</span><span class="mord mathnormal">t</span><span class="mord mathnormal">s</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">3</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">es</span><span class="mord mathnormal">t</span><span class="mord mathnormal">ima</span><span class="mord mathnormal">t</span><span class="mord mathnormal" style="margin-right:0.02778em;">or</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord mathnormal" style="margin-right:0.05764em;">E</span><span class="mord mathnormal">s</span><span class="mord mathnormal">t</span><span class="mord mathnormal">ima</span><span class="mord mathnormal">t</span><span class="mord mathnormal" style="margin-right:0.02778em;">or</span><span class="mpunct">,</span></span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">roo</span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord mathnormal">s</span><span class="mord mathnormal">i</span><span class="mord mathnormal">ze</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:0.8888799999999999em;vertical-align:-0.19444em;"></span><span class="mord">1440</span><span class="mord mathnormal">b</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mord mathnormal">t</span><span class="mord mathnormal">es</span><span class="mord mathnormal" style="margin-right:0.22222em;">V</span><span class="mord mathnormal" style="margin-right:0.02778em;">er</span><span class="mord mathnormal">i</span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord mathnormal">i</span><span class="mord mathnormal">c</span><span class="mord mathnormal">a</span><span class="mord mathnormal">t</span><span class="mord mathnormal">i</span><span class="mord mathnormal">o</span><span class="mord mathnormal">n</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:0.69444em;vertical-align:0em;"></span><span class="mord mathnormal">a</span><span class="mord mathnormal" style="margin-right:0.01968em;">tl</span><span class="mord mathnormal">e</span><span class="mord mathnormal">a</span><span class="mord mathnormal">s</span><span class="mord mathnormal">t</span><span class="mord">81.689</span><span class="mord mathnormal">m</span><span class="mord mathnormal">s</span><span class="mord">‘‘‘</span></span></span></span>

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^2\cdot b^2=c.$$

Define instructions

Firstly, we need to define the instructions that our circuit will rely on. Instructions are the boundary between high-level gadgets and the low-level circuit operations. Instructions may be as coarse or as granular as desired, but in practice you want to strike a balance between an instruction being large enough to effectively optimize its implementation, and small enough that it is meaningfully reusable.

For our circuit, we will use three instructions:

• Load a private number into the circuit.
• Multiply two numbers.
• Expose a number as a public input to the circuit.

We also need a type for a variable representing a number. Instruction interfaces provide associated types for their inputs and outputs, to allow the implementations to represent these in a way that makes the most sense for their optimization goals.

trait NumericInstructions<F: FieldExt>: Chip<F> {
    /// Variable representing a number.
    type Num;

    /// Loads a number into the circuit as a private input.
    fn load_private(&self, layouter: impl Layouter<F>, a: Option<F>) -> Result<Self::Num, Error>;

    /// Returns `c = a * b`.
    fn mul(
        &self,
        layouter: impl Layouter<F>,
        a: Self::Num,
        b: Self::Num,
    ) -> Result<Self::Num, Error>;

    /// Exposes a number as a public input to the circuit.
    fn expose_public(&self, layouter: impl Layouter<F>, num: Self::Num) -> Result<(), Error>;
}

Define a chip implementation

For our circuit, we will build a chip that provides the above numeric instructions for a finite field.

/// The chip that will implement our instructions! Chips store their own
/// config, as well as type markers if necessary.
struct FieldChip<F: FieldExt> {
    config: FieldConfig,
    _marker: PhantomData<F>,
}

Every chip needs to implement the Chip trait. This defines the properties of the chip that a Layouter may rely on when synthesizing a circuit, as well as enabling any initial state that the chip requires to be loaded into the circuit.

impl<F: FieldExt> Chip<F> for FieldChip<F> {
    type Config = FieldConfig;
    type Loaded = ();

    fn config(&self) -> &Self::Config {
        &self.config
    }

    fn loaded(&self) -> &Self::Loaded {
        &()
    }
}

Configure the chip

The chip needs to be configured with the columns, permutations, and gates that will be required to implement all of the desired instructions.

/// Chip state is stored in a config struct. This is generated by the chip
/// during configuration, and then stored inside the chip.
#[derive(Clone, Debug)]
struct FieldConfig {
    /// For this chip, we will use two advice columns to implement our instructions.
    /// These are also the columns through which we communicate with other parts of
    /// the circuit.
    advice: [Column<Advice>; 2],

    // We need to create a permutation between our advice columns. This allows us to
    // copy numbers within these columns from arbitrary rows, which we can use to load
    // inputs into our instruction regions.
    perm: Permutation,

    // We need a selector to enable the multiplication gate, so that we aren't placing
    // any constraints on cells where `NumericInstructions::mul` is not being used.
    // This is important when building larger circuits, where columns are used by
    // multiple sets of instructions.
    s_mul: Selector,

    // The selector for the public-input gate, which uses one of the advice columns.
    s_pub: Selector,
}

impl<F: FieldExt> FieldChip<F> {
    fn construct(config: <Self as Chip<F>>::Config) -> Self {
        Self {
            config,
            _marker: PhantomData,
        }
    }

    fn configure(
        meta: &mut ConstraintSystem<F>,
        advice: [Column<Advice>; 2],
        instance: Column<Instance>,
    ) -> <Self as Chip<F>>::Config {
        let perm = Permutation::new(
            meta,
            &advice
                .iter()
                .map(|column| (*column).into())
                .collect::<Vec<_>>(),
        );
        let s_mul = meta.selector();
        let s_pub = meta.selector();

        // Define our multiplication gate!
        meta.create_gate("mul", |meta| {
            // To implement multiplication, we need three advice cells and a selector
            // cell. We arrange them like so:
            //
            // | a0  | a1  | s_mul |
            // |-----|-----|-------|
            // | lhs | rhs | s_mul |
            // | out |     |       |
            //
            // Gates may refer to any relative offsets we want, but each distinct
            // offset adds a cost to the proof. The most common offsets are 0 (the
            // current row), 1 (the next row), and -1 (the previous row), for which
            // `Rotation` has specific constructors.
            let lhs = meta.query_advice(advice[0], Rotation::cur());
            let rhs = meta.query_advice(advice[1], Rotation::cur());
            let out = meta.query_advice(advice[0], Rotation::next());
            let s_mul = meta.query_selector(s_mul, Rotation::cur());

            // Finally, we return the polynomial expressions that constrain this gate.
            // For our multiplication gate, we only need a single polynomial constraint.
            //
            // The polynomial expressions returned from `create_gate` will be
            // constrained by the proving system to equal zero. Our expression
            // has the following properties:
            // - When s_mul = 0, any value is allowed in lhs, rhs, and out.
            // - When s_mul != 0, this constrains lhs * rhs = out.
            vec![s_mul * (lhs * rhs + out * -F::one())]
        });

        // Define our public-input gate!
        meta.create_gate("public input", |meta| {
            // We choose somewhat-arbitrarily that we will use the second advice
            // column for exposing numbers as public inputs.
            let a = meta.query_advice(advice[1], Rotation::cur());
            let p = meta.query_instance(instance, Rotation::cur());
            let s = meta.query_selector(s_pub, Rotation::cur());

            // We simply constrain the advice cell to be equal to the instance cell,
            // when the selector is enabled.
            vec![s * (p + a * -F::one())]
        });

        FieldConfig {
            advice,
            perm,
            s_mul,
            s_pub,
        }
    }
}

Implement chip traits

/// A variable representing a number.
#[derive(Clone)]
struct Number<F: FieldExt> {
    cell: Cell,
    value: Option<F>,
}

impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
    type Num = Number<F>;

    fn load_private(
        &self,
        mut layouter: impl Layouter<F>,
        value: Option<F>,
    ) -> Result<Self::Num, Error> {
        let config = self.config();

        let mut num = None;
        layouter.assign_region(
            || "load private",
            |mut region| {
                let cell = region.assign_advice(
                    || "private input",
                    config.advice[0],
                    0,
                    || value.ok_or(Error::SynthesisError),
                )?;
                num = Some(Number { cell, value });
                Ok(())
            },
        )?;
        Ok(num.unwrap())
    }

    fn mul(
        &self,
        mut layouter: impl Layouter<F>,
        a: Self::Num,
        b: Self::Num,
    ) -> Result<Self::Num, Error> {
        let config = self.config();

        let mut out = None;
        layouter.assign_region(
            || "mul",
            |mut region: Region<'_, F>| {
                // We only want to use a single multiplication gate in this region,
                // so we enable it at region offset 0; this means it will constrain
                // cells at offsets 0 and 1.
                config.s_mul.enable(&mut region, 0)?;

                // The inputs we've been given could be located anywhere in the circuit,
                // but we can only rely on relative offsets inside this region. So we
                // assign new cells inside the region and constrain them to have the
                // same values as the inputs.
                let lhs = region.assign_advice(
                    || "lhs",
                    config.advice[0],
                    0,
                    || a.value.ok_or(Error::SynthesisError),
                )?;
                let rhs = region.assign_advice(
                    || "rhs",
                    config.advice[1],
                    0,
                    || b.value.ok_or(Error::SynthesisError),
                )?;
                region.constrain_equal(&config.perm, a.cell, lhs)?;
                region.constrain_equal(&config.perm, b.cell, rhs)?;

                // Now we can assign the multiplication result into the output position.
                let value = a.value.and_then(|a| b.value.map(|b| a * b));
                let cell = region.assign_advice(
                    || "lhs * rhs",
                    config.advice[0],
                    1,
                    || value.ok_or(Error::SynthesisError),
                )?;

                // Finally, we return a variable representing the output,
                // to be used in another part of the circuit.
                out = Some(Number { cell, value });
                Ok(())
            },
        )?;

        Ok(out.unwrap())
    }

    fn expose_public(&self, mut layouter: impl Layouter<F>, num: Self::Num) -> Result<(), Error> {
        let config = self.config();

        layouter.assign_region(
            || "expose public",
            |mut region: Region<'_, F>| {
                // Enable the public-input gate.
                config.s_pub.enable(&mut region, 0)?;

                // Load the output into the correct advice column.
                let out = region.assign_advice(
                    || "public advice",
                    config.advice[1],
                    0,
                    || num.value.ok_or(Error::SynthesisError),
                )?;
                region.constrain_equal(&config.perm, num.cell, out)?;

                // We don't assign to the instance column inside the circuit;
                // the mapping of public inputs to cells is provided to the prover.
                Ok(())
            },
        )
    }
}

Build the circuit

Now that we have the instructions we need, and a chip that implements them, we can finally build our circuit!

/// The full circuit implementation.
///
/// In this struct we store the private input variables. We use `Option<F>` because
/// they won't have any value during key generation. During proving, if any of these
/// were `None` we would get an error.
struct MyCircuit<F: FieldExt> {
    a: Option<F>,
    b: Option<F>,
}

impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
    // Since we are using a single chip for everything, we can just reuse its config.
    type Config = FieldConfig;

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        // We create the two advice columns that FieldChip uses for I/O.
        let advice = [meta.advice_column(), meta.advice_column()];

        // We also need an instance column to store public inputs.
        let instance = meta.instance_column();

        FieldChip::configure(meta, advice, instance)
    }

    fn synthesize(&self, cs: &mut impl Assignment<F>, config: Self::Config) -> Result<(), Error> {
        let mut layouter = SingleChipLayouter::new(cs)?;
        let field_chip = FieldChip::<F>::construct(config);

        // Load our private values into the circuit.
        let a = field_chip.load_private(layouter.namespace(|| "load a"), self.a)?;
        let b = field_chip.load_private(layouter.namespace(|| "load b"), self.b)?;

        // We only have access to plain multiplication.
        // We could implement our circuit as:
        //     asq = a*a
        //     bsq = b*b
        //     c   = asq*bsq
        //
        // but it's more efficient to implement it as:
        //     ab = a*b
        //     c  = ab^2
        let ab = field_chip.mul(layouter.namespace(|| "a * b"), a, b)?;
        let c = field_chip.mul(layouter.namespace(|| "ab * ab"), ab.clone(), ab)?;

        // Expose the result as a public input to the circuit.
        field_chip.expose_public(layouter.namespace(|| "expose c"), c)
    }
}

Testing the circuit

halo2::dev::MockProver can be used to test that the circuit is working correctly. The private and public inputs to the circuit are constructed as we will do to create a proof, but by passing them to MockProver::run we get an object that can test every constraint in the circuit, and tell us exactly what is failing (if anything).

    // The number of rows in our circuit cannot exceed 2^k. Since our example
    // circuit is very small, we can pick a very small value here.
    let k = 3;

    // Prepare the private and public inputs to the circuit!
    let a = Fp::from(2);
    let b = Fp::from(3);
    let c = a.square() * b.square();

    // Instantiate the circuit with the private inputs.
    let circuit = MyCircuit {
        a: Some(a),
        b: Some(b),
    };

    // Arrange the public input. We expose the multiplication result in row 6
    // of the instance column, so we position it there in our public inputs.
    let mut public_inputs = vec![Fp::zero(); 1 << k];
    public_inputs[6] = c;

    // Given the correct public input, our circuit will verify.
    let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
    assert_eq!(prover.verify(), Ok(()));

    // If we try some other public input, the proof will fail!
    public_inputs[6] += Fp::one();
    let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
    assert_eq!(
        prover.verify(),
        Err(vec![VerifyFailure::Gate {
            gate_index: 1,
            gate_name: "public input",
            row: 6,
        }])
    );

Full example

You can find the source code for this example here.

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 $[\mathrm{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.

Small set interpolation

We can use Lagrange interpolation to create a polynomial constraint that maps $f(X)=Y$ for small sets of $X\in \{x_i\},Y\in \{y_i\}$.

For instance, say we want to map a 2-bit value to a "spread" version interleaved with zeros. We first precompute the evaluations at each point:

$$\begin{array}{rcl}00\to 0000& ⟹& 0\to 0\\ 01\to 0001& ⟹& 1\to 1\\ 10\to 0100& ⟹& 2\to 4\\ 11\to 0101& ⟹& 3\to 5\end{array}$$

Then, we construct the Lagrange basis polynomial for each point using the identity: $$l_j(X)=\prod _{0\le m<k,m\ne j}\frac{x-x_m}{x_j-x_m},$$ where $k$ is the number of data points. ($k=4$ in our example above.)

Recall that the Lagrange basis polynomial $l_j(X)$ evaluates to $1$ at $X=x_j$ and $0$ at all other $x_i,j\ne i.$

Continuing our example, we get four Lagrange basis polynomials:

$$\begin{array}{ccc}{l}_0(X)& =& \frac{(X-3)(X-2)(X-1)}{(-3)(-2)(-1)}\\ l_1(X)& =& \frac{(X-3)(X-2)(X)}{(-2)(-1)(1)}\\ l_2(X)& =& \frac{(X-3)(X-1)(X)}{(-1)(1)(2)}\\ l_3(X)& =& \frac{(X-2)(X-1)(X)}{(1)(2)(3)}\end{array}$$

Our polynomial constraint is then

$$\begin{array}{cccccccccccl}& f(0)\cdot l_0(X)& +& f(1)\cdot l_1(X)& +& f(2)\cdot l_2(X)& +& f(3)\cdot l_3(X)& -& f(X)& =& 0\\ ⟹& 0\cdot l_0(X)& +& 1\cdot l_1(X)& +& 4\cdot l_2(X)& +& 5\cdot l_3(X)& -& f(X)& =& 0.\end{array}$$

Design

Note on Language

We use slightly different language than others to describe PLONK concepts. Here's the overview:

1. We like to think of PLONK-like arguments as tables, where each column corresponds to a "wire". We refer to entries in this table as "cells".
2. We like to call "selector polynomials" and so on "fixed columns" instead. We then refer specifically to a "selector constraint" when a cell in a fixed column is being used to control whether a particular constraint is enabled in that row.
3. We call the other polynomials "advice columns" usually, when they're populated by the prover.
4. We use the term "rule" to refer to a "gate" like $$A(X)\cdot q_A(X)+B(X)\cdot q_B(X)+A(X)\cdot B(X)\cdot q_M(X)+C(X)\cdot q_C(X)=0.$$
   • TODO: Check how consistent we are with this, and update the code and docs to match.

Proving system

The Halo 2 proving system can be broken down into five stages:

1. Commit to polynomials encoding the main components of the circuit:
   • Cell assignments.
   • Permuted values and products for each lookup argument.
   • Equality constraint permutations.
2. Construct the vanishing argument to constrain all circuit relations to zero:
   • Standard and custom gates.
   • Lookup argument rules.
   • Equality constraint permutation rules.
3. Evaluate the above polynomials at all necessary points:
   • All relative rotations used by custom gates across all columns.
   • Vanishing argument pieces.
4. Construct the multipoint opening argument to check that all evaluations are consistent with their respective commitments.
5. Run the inner product argument to create a polynomial commitment opening proof for the multipoint opening argument polynomial.

These stages are presented in turn across this section of the book.

Example

To aid our explanations, we will at times refer to the following example constraint system:

• Four advice columns $a,b,c,d$.
• One fixed column $f$.
• Three custom gates:
  • $a\cdot b\cdot c_{-1}-d=0$
  • $f_{-1}\cdot c=0$
  • $f\cdot d\cdot a=0$

tl;dr

The table below provides a (probably too) succinct description of the Halo 2 protocol. This description will likely be replaced by the Halo 2 paper and security proof, but for now serves as a summary of the following sub-sections.

Then the prover and verifier:

• Construct $\text{finalPoly}(X)$ as a linear combination of $\mathbf{Q}$ and $U$ using powers of $x_4$;
• Construct $\text{finalPolyEval}$ as the equivalent linear combination of ${\mathbf{q}}_{\text{evals}}$ and $u_{\text{eval}}$; and
• Perform $\text{InnerProduct}(\text{finalPoly}(X),x_3,\text{finalPolyEval}).$

TODO: Write up protocol components that provide zero-knowledge.

Lookup argument

halo2 uses the following lookup technique, which allows for lookups in arbitrary sets, and is arguably simpler than Plookup.

Note on Language

In addition to the general notes on language:

• We call the $Z(X)$ polynomial (the grand product argument polynomial for the permutation argument) the "permutation product" column.

Technique Description

We express lookups in terms of a "subset argument" over a table with $2^k$ rows (numbered from 0), and columns $A$ and $S$.

The goal of the subset argument is to enforce that every cell in $A$ is equal to some cell in $S$. This means that more than one cell in $A$ can be equal to the same cell in $S$, and some cells in $S$ don't need to be equal to any of the cells in $A$.

• $S$ might be fixed, but it doesn't need to be. That is, we can support looking up values in either fixed or variable tables (where the latter includes advice columns).
• $A$ and $S$ can contain duplicates. If the sets represented by $A$ and/or $S$ are not naturally of size $2^k$, we extend $S$ with duplicates and $A$ with dummy values known to be in $S$.
  • Alternatively we could add a "lookup selector" that controls which elements of the $A$ column participate in lookups. This would modify the occurrence of $A(X)$ in the permutation rule below to replace $A$ with, say, $S_0$ if a lookup is not selected.

Let ${\ell }_i$ be the Lagrange basis polynomial that evaluates to $1$ at row $i$, and $0$ otherwise.

We start by allowing the prover to supply permutation columns of $A$ and $S$. Let's call these $A^{\prime }$ and $S^{\prime }$, respectively. We can enforce that they are permutations using a permutation argument with product column $Z$ with the rules:

$$Z(X)(A(X)+\beta )(S(X)+\gamma )-Z({\omega }^{-1}X)(A^{\prime }(X)+\beta )(S^{\prime }(X)+\gamma )=0$$$${\ell }_0(X)(Z(X)-1)=0$$

This is a version of the permutation argument which allows $A^{\prime }$ and $S^{\prime }$ to be permutations of $A$ and $S$, respectively, but doesn't specify the exact permutations. $\beta$ and $\gamma$ are separate challenges so that we can combine these two permutation arguments into one without worrying that they might interfere with each other.

The goal of these permutations is to allow $A^{\prime }$ and $S^{\prime }$ to be arranged by the prover in a particular way:

1. All the cells of column $A^{\prime }$ are arranged so that like-valued cells are vertically adjacent to each other. This could be done by some kind of sorting algorithm, but all that matters is that like-valued cells are on consecutive rows in column $A^{\prime }$, and that $A^{\prime }$ is a permutation of $A$.
2. The first row in a sequence of like values in $A^{\prime }$ is the row that has the corresponding value in $S^{\prime }.$ Apart from this constraint, $S^{\prime }$ is any arbitrary permutation of $S$.

Now, we'll enforce that either $A_i^{\prime }=S_i^{\prime }$ or that $A_i^{\prime }=A_{i-1}^{\prime }$, using the rule

$$(A^{\prime }(X)-S^{\prime }(X))\cdot (A^{\prime }(X)-A^{\prime }({\omega }^{-1}X))=0$$

In addition, we enforce $A_0^{\prime }=S_0^{\prime }$ using the rule

$${\ell }_0(X)\cdot (A^{\prime }(X)-S^{\prime }(X))=0$$

Together these constraints effectively force every element in $A^{\prime }$ (and thus $A$) to equal at least one element in $S^{\prime }$ (and thus $S$). Proof: by induction on prefixes of the rows.

Cost

• There is the original column $A$ and the fixed column $S$.
• There is a permutation product column $Z$.
• There are the two permutations $A^{\prime }$ and $S^{\prime }$.
• The gates are all of low degree.

Generalizations

halo2's lookup argument implementation generalizes the above technique in the following ways:

• $A$ and $S$ can be extended to multiple columns, combined using a random challenge. $A^{\prime }$ and $S^{\prime }$ stay as single columns.
  • The commitments to the columns of $S$ can be precomputed, then combined cheaply once the challenge is known by taking advantage of the homomorphic property of Pedersen commitments.
  • The columns of $A$ can be given as arbitrary polynomial expressions using relative references. These will be substituted into the product column constraint, subject to the maximum degree bound. This potentially saves one or more advice columns.
• Then, a lookup argument for an arbitrary-width relation can be implemented in terms of a subset argument, i.e. to constrain $\mathcal{R}(x,y,...)$ in each row, consider $\mathcal{R}$ as a set of tuples $S$ (using the method of the previous point), and check that $(x,y,...)\in \mathcal{R}$.
  • In the case where $\mathcal{R}$ represents a function, this implicitly also checks that the inputs are in the domain. This is typically what we want, and often saves an additional range check.
• We can support multiple tables in the same circuit, by combining them into a single table that includes a tag column to identify the original table.
  • The tag column could be merged with the "lookup selector" mentioned earlier, if this were implemented.

These generalizations are similar to those in sections 4 and 5 of the Plookup paper. That is, the differences from Plookup are in the subset argument. This argument can then be used in all the same ways; for instance, the optimized range check technique in section 5 of the Plookup paper can also be used with this subset argument.

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{mapping}$ for the permutation itself;
• an auxiliary array $\mathsf{aux}$ that keeps track of a distinguished element of each cycle;
• another array $\mathsf{sizes}$ that keeps track of the size of each cycle.

We have the invariant that for each element $x$ in a given cycle $C$, $\mathsf{aux}(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{aux}(x)=\mathsf{aux}(y)$. Also, $\mathsf{sizes}(\mathsf{aux}(x))$ gives the size of the cycle containing $x$. (This is guaranteed only for $\mathsf{sizes}(\mathsf{aux}(x)))$, not for $\mathsf{sizes}(x)$.)

The algorithm starts with a representation of the identity permutation: for all $x$, we set $\mathsf{mapping}(x)=x$, $\mathsf{aux}(x)=x$, and $\mathsf{sizes}(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{aux}(left)=\mathsf{aux}(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{sizes}(\mathsf{aux}(left))<\mathsf{sizes}(\mathsf{aux}(right))$.
3. Set $\mathsf{sizes}(\mathsf{aux}(left))):=\mathsf{sizes}(\mathsf{aux}(left)))+\mathsf{sizes}(\mathsf{aux}(right)))$.
4. Following the mapping around the right (smaller) cycle, for each element $x$ set $\mathsf{aux}(x):=\mathsf{aux}(left)$.
5. Splice the smaller cycle into the larger one by swapping $\mathsf{mapping}(left)$ with $\mathsf{mapping}(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 5 of the above algorithm, then we would end up constructing the cycle $(ab)(cd)$, rather than the correct $(abcd)$.

Argument specification

We need to check a permutation of cells in $m$ columns, represented in Lagrange basis by polynomials $p_0,\dots ,p_{m-1}$.

We first label each cell in those $m$ columns with a unique element of ${\mathbb{F}}^{\times }$.

Let $\omega$ be a $2^k$ root of unity and let $\delta$ be a $T$ root of unity, where $T\cdot 2^S+1=p$ with $T$ odd and $k\le S$. We will use ${\delta }^i\cdot {\omega }^j\in {\mathbb{F}}^{\times }$ as the label for the cell in the $j$th row of the $i$th column of the permutation argument.

If we have a permutation $\sigma (\mathsf{column}:i,\mathsf{row}:j)=(\mathsf{column}:i^{\prime },\mathsf{row}:j^{\prime })$, we can represent it as a vector of $m$ polynomials $s_i(X)$ such that $s_i({\omega }^j)={\delta }^{i^{\prime }}\cdot {\omega }^{j^{\prime }}$.

Notice that the identity permutation can be represented by the vector of $m$ polynomials ${\mathsf{ID}}_i(X)$ such that ${\mathsf{ID}}_i(X)={\delta }^i\cdot X$.

Now given our permutation represented by $s_0,\dots ,s_{m-1}$ over columns represented by $p_0,\dots ,p_{m-1}$, we want to ensure that: $$\prod _{i=0}^{m-1}\prod _{j=0}^{n-1}\left(\frac{p_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{p_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }\right)=1$$

Let $Z_P$ be such that $Z_P({\omega }^0)=Z_P({\omega }^n)=1$ and for $0\le j<n$: $$\begin{array}{rl}{Z}_P({\omega }^{j+1})& =\prod _{h=0}^j\prod _{i=0}^{m-1}\frac{p_i({\omega }^h)+\beta \cdot {\delta }^i\cdot {\omega }^h+\gamma }{p_i({\omega }^h)+\beta \cdot s_i({\omega }^h)+\gamma }\\ & =Z_P({\omega }^j)\prod _{i=0}^{m-1}\frac{p_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{p_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }\end{array}$$

Then it is sufficient to enforce the constraints: $$\begin{gathered} l_0\cdot (Z_P(X)-1)=0 \\ {Z}_P(\omega X)\cdot \prod _{i=0}^{m-1}\left(p_i(X)+\beta \cdot s_i(X)+\gamma \right)-Z_P(X)\cdot \prod _{i=0}^{m-1}\left(p_i(X)+\beta \cdot {\delta }^i\cdot X+\gamma \right)=0 \end{gathered}$$

The optimization used to obtain the simple representation of the identity permutation was suggested by Vitalik Buterin for PLONK, and is described at the end of section 8 of the PLONK paper. Note that the ${\delta }^i$ are all distinct quadratic non-residues.

Circuit commitments

Committing to the circuit assignments

At the start of proof creation, the prover has a table of cell assignments that it claims satisfy the constraint system. The table has $n=2^k$ rows, and is broken into advice, instance, and fixed columns. We define $F_{i,j}$ as the assignment in the $j$th row of the $i$th fixed column. Without loss of generality, we'll similarly define $A_{i,j}$ to represent the advice and instance assignments.

We separate fixed columns here because they are provided by the verifier, whereas the advice and instance columns are provided by the prover. In practice, the commitments to instance and fixed columns are computed by both the prover and verifier, and only the advice commitments are stored in the proof.

To commit to these assignments, we construct Lagrange polynomials of degree $n-1$ for each column, over an evaluation domain of size $n$ (where $\omega$ is the $n$th primitive root of unity):

• $a_i(X)$ interpolates such that $a_i({\omega }^j)=A_{i,j}$.
• $f_i(X)$ interpolates such that $f_i({\omega }^j)=F_{i,j}$.

We then create a blinding commitment to the polynomial for each column:

$$\mathbf{A}=[\text{Commit}(a_0(X)),\dots ,\text{Commit}(a_i(X))]$$ $$\mathbf{F}=[\text{Commit}(f_0(X)),\dots ,\text{Commit}(f_i(X))]$$

$\mathbf{F}$ is constructed as part of key generation, using a blinding factor of $1$. $\mathbf{A}$ is constructed by the prover and sent to the verifier.

Committing to the lookup permutations

The verifier starts by sampling $\theta$, which is used to keep individual columns within lookups independent. Then, the prover commits to the permutations for each lookup as follows:

• Given a lookup with input column polynomials $[A_0(X),\dots ,A_{m-1}(X)]$ and table column polynomials $[S_0(X),\dots ,S_{m-1}(X)]$, the prover constructs two compressed polynomials

  $$A_{\text{compressed}}(X)={\theta }^{m-1}{A}_0(X)+{\theta }^{m-2}{A}_1(X)+\cdots +\theta A_{m-2}(X)+A_{m-1}(X)$$ $$S_{\text{compressed}}(X)={\theta }^{m-1}{S}_0(X)+{\theta }^{m-2}{S}_1(X)+\cdots +\theta S_{m-2}(X)+S_{m-1}(X)$$

• The prover then permutes $A_{\text{compressed}}(X)$ and $S_{\text{compressed}}(X)$ according to the rules of the lookup argument, obtaining $A^{\prime }(X)$ and $S^{\prime }(X)$.

Finally, the prover creates blinding commitments for all of the lookups

$$\mathbf{L}=\left[(\text{Commit}(A^{\prime }(X))),\text{Commit}(S^{\prime }(X))),\dots \right]$$

and sends them to the verifier.

Committing to the equality constraint permutations

The verifier samples $\beta$ and $\gamma$.

For each equality constraint argument:

• The prover constructs a vector $P$:

$$P_j=\prod _{i=0}^{m-1}\frac{p_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{p_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }$$

• The prover constructs a polynomial $Z_P$ which has a Lagrange basis representation corresponding to a running product of $P$, starting at $Z_P(1)=1$.

See the Permutation argument section for more detail.

The prover creates blinding commitments to each $Z_P$ polynomial:

$${\mathbf{Z}}_{\mathbf{P}}=\left[\text{Commit}(Z_P(X)),\dots \right]$$

and sends them to the verifier.

Committing to the lookup permutation product columns

In addition to committing to the individual permuted lookups, for each lookup, the prover needs to commit to the permutation product column:

• The prover constructs a vector $P$:

$$P_j=\frac{(A_{\text{compressed}}({\omega }^j)+\beta )(S_{\text{compressed}}({\omega }^j)+\gamma )}{(A^{\prime }({\omega }^j)+\beta )(S^{\prime }({\omega }^j)+\gamma )}$$

• The prover constructs a polynomial $Z_L$ which has a Lagrange basis representation corresponding to a running product of $P$, starting at $Z_L(1)=1$.

$\beta$ and $\gamma$ are used to combine the permutation arguments for $A^{\prime }(X)$ and $S^{\prime }(X)$ while keeping them independent. We can reuse $\beta$ and $\gamma$ from the equality constraint permutation here because they serve the same purpose in both places, and we aren't trying to combine the lookup and equality constraint permutation arguments. The important thing here is that the verifier samples $\beta$ and $\gamma$ after the prover has created $\mathbf{A}$, $\mathbf{F}$, and $\mathbf{L}$ (and thus commited to all the cell values used in lookup columns, as well as $A^{\prime }(X)$ and $S^{\prime }(X)$ for each lookup).

As before, the prover creates blinding commitments to each $Z_L$ polynomial:

$${\mathbf{Z}}_{\mathbf{L}}=\left[\text{Commit}(Z_L(X)),\dots \right]$$

and sends them to the verifier.

Vanishing argument

Having committed to the circuit assignments, the prover now needs to demonstrate that the various circuit relations are satisfied:

• The custom gates, represented by polynomials ${\text{gate}}_i(X)$.
• The rules of the lookup arguments.
• The rules of the equality constraint permutations.

Each of these relations is represented as a polynomial of degree $d$ (the maximum degree of any of the relations) with respect to the circuit columns. Given that the degree of the assignment polynomials for each column is $n-1$, the relation polynomials have degree $d(n-1)$ with respect to $X$.

In our example, these would be the gate polynomials, of degree $3n-3$:

• ${\text{gate}}_0(X)=a_0(X)\cdot a_1(X)\cdot a_2(X{\omega }^{-1})-a_3(X)$
• ${\text{gate}}_1(X)=f_0(X{\omega }^{-1})\cdot a_2(X)$
• ${\text{gate}}_2(X)=f_0(X)\cdot a_3(X)\cdot a_0(X)$

A relation is satisfied if its polynomial is equal to zero. One way to demonstrate this is to divide each polynomial relation by the vanishing polynomial $t(X)=(X^n-1)$, which is the lowest-degree monomial that has roots at every ${\omega }^i$. If relation's polynomial is perfectly divisible by $t(X)$, it is equal to zero over the domain (as desired).

This simple construction would require a polynomial commitment per relation. Instead, we commit to all of the circuit relations simultaneously: the verifier samples $y$, and then the prover constructs the quotient polynomial

$$h(X)=\frac{{\text{gate}}_0(X)+y\cdot {\text{gate}}_1(X)+\cdots +y^i\cdot {\text{gate}}_i(X)+\dots }{t(X)},$$

where the numerator is a random (the prover commits to the cell assignments before the verifier samples $y$) linear combination of the circuit relations.

• If the numerator polynomial (in formal indeterminate $X$) is perfectly divisible by $t(X)$, then with high probability all relations are satisfied.
• Conversely, if at least one relation is not satisfied, then with high probability $h(x)\cdot t(x)$ will not equal the evaluation of the numerator at $x$. In this case, the numerator polynomial would not be perfectly divisible by $t(X)$.

Committing to $h(X)$

$h(X)$ has degree $(d-1)n-d$ (because the divisor $t(X)$ has degree $n$). However, the polynomial commitment scheme we use for Halo 2 only supports committing to polynomials of degree $n-1$ (which is the maximum degree that the rest of the protocol needs to commit to). Instead of increasing the cost of the polynomial commitment scheme, the prover split $h(X)$ into pieces of degree $n-1$

$$h_0(X)+X^n{h}_1(X)+\cdots +X^{n(d-1)}{h}_{d-1}(X),$$

and produces blinding commitments to each piece

$$\mathbf{H}=[\text{Commit}(h_0(X)),\text{Commit}(h_1(X)),\dots ,\text{Commit}(h_{d-1}(X))].$$

Evaluating the polynomials

At this point, all properties of the circuit have been committed to. The verifier now wants to see if the prover committed to the correct $h(X)$ polynomial. The verifier samples $x$, and the prover produces the purported evaluations of the various polynomials at $x$, for all the relative offsets used in the circuit, as well as $h(X)$.

In our example, this would be:

• $a_0(x)$
• $a_1(x)$
• $a_2(x)$, $a_2(x{\omega }^{-1})$
• $a_3(x)$
• $f_0(x)$, $f_0(x{\omega }^{-1})$
• $h_0(x)$, ..., $h_{d-1}(x)$

The verifier checks that these evaluations satisfy the form of $h(X)$:

$$\frac{{\text{gate}}_0(x)+\cdots +y^i\cdot {\text{gate}}_i(x)+\dots }{t(x)}=h_0(x)+\cdots +x^{n(d-1)}{h}_{d-1}(x)$$

Now content that the evaluations collectively satisfy the gate constraints, the verifier needs to check that the evaluations themselves are consistent with the original circuit commitments, as well as $\mathbf{H}$. To implement this efficiently, we use a multipoint opening argument.

Multipoint opening argument

Consider the commitments $A,B,C,D$ to polynomials $a(X),b(X),c(X),d(X)$. Let's say that $a$ and $b$ were queried at the point $x$, while $c$ and $d$ were queried at both points $x$ and $\omega x$. (Here, $\omega$ is the primitive root of unity in the multiplicative subgroup over which we constructed the polynomials).

To open these commitments, we could create a polynomial $Q$ for each point that we queried at (corresponding to each relative rotation used in the circuit). But this would not be efficient in the circuit; for example, $c(X)$ would appear in multiple polynomials.

Instead, we can group the commitments by the sets of points at which they were queried: $$\begin{array}{ccccc}& \{x\}& & \{x,\omega x\}& \\ & A& & C& \\ & B& & D& \end{array}$$

For each of these groups, we combine them into a polynomial set, and create a single $Q$ for that set, which we open at each rotation.

Optimisation steps

The multipoint opening optimisation takes as input:

• A random $x$ sampled by the verifier, at which we evaluate $a(X),b(X),c(X),d(X)$.
• Evaluations of each polynomial at each point of interest, provided by the prover: $a(x),b(x),c(x),d(x),c(\omega x),d(\omega x)$

These are the outputs of the vanishing argument.

The multipoint opening optimisation proceeds as such:

1. Sample random $x_1$, to keep $a,b,c,d$ linearly independent.

2. Accumulate polynomials and their corresponding evaluations according to the point set at which they were queried: q_polys: $$\begin{array}{rcclc}{q}_1(X)& =& a(X)& +& x_{1}b(X)\\ q_2(X)& =& c(X)& +& x_{1}d(X)\end{array}$$ q_eval_sets:

           [
               [a(x) + x_1 b(x)],
               [
                   c(x) + x_1 d(x),
                   c(\omega x) + x_1 d(\omega x)
               ]
           ]
   

   NB: q_eval_sets is a vector of sets of evaluations, where the outer vector goes over the point sets, and the inner vector goes over the points in each set.

3. Interpolate each set of values in q_eval_sets: r_polys: $$\begin{array}{cccc}{r}_1(X)s.t.& & & \\ & r_1(x)& =& a(x)+x_{1}b(x)\\ r_2(X)s.t.& & & \\ & r_2(x)& =& c(x)+x_{1}d(x)\\ & r_2(\omega x)& =& c(\omega x)+x_{1}d(\omega x)\end{array}$$

4. Construct f_polys which check the correctness of q_polys: f_polys $$\begin{array}{rcl}{f}_1(X)& =& \frac{q_1(X)-r_1(X)}{X-x}\\ f_2(X)& =& \frac{q_2(X)-r_2(X)}{(X-x)(X-\omega x)}\end{array}$$

   If $q_1(x)=r_1(x)$, then $f_1(X)$ should be a polynomial. If $q_2(x)=r_2(x)$ and $q_2(\omega x)=r_2(\omega x)$ then $f_2(X)$ should be a polynomial.

5. Sample random $x_2$ to keep the f_polys linearly independent.

6. Construct $f(X)=f_1(X)+x_2{f}_2(X)$.

7. Sample random $x_3$, at which we evaluate $f(X)$: $$\begin{array}{rcccl}f(x_3)& =& f_1(x_3)& +& x_2{f}_2(x_3)\\ & =& \frac{q_1(x_3)-r_1(x_3)}{x_3-x}& +& x_2\frac{q_2(x_3)-r_2(x_3)}{(x_3-x)(x_3-\omega x)}\end{array}$$

8. Sample random $x_4$ to keep $f(X)$ and q_polys linearly independent.

9. Construct final_poly, $$final\_poly(X)=f(X)+x_4{q}_1(X)+x_4^2{q}_2(X),$$ which is the polynomial we commit to in the inner product argument.

Inner product argument

Halo 2 uses a polynomial commitment scheme for which we can create polynomial commitment opening proofs, based around the Inner Product Argument.

TODO: Explain Halo 2's variant of the IPA.

It is very similar to ${\text{PC}}_{\text{DL}}.\text{Open}$ from Appendix A.2 of BCMS20. See this comparison for details.

Comparison to other work

BCMS20 Appendix A.2

Appendix A.2 of BCMS20 describes a polynomial commitment scheme that is similar to the one described in BGH19 (BCMS20 being a generalization of the original Halo paper). Halo 2 builds on both of these works, and thus itself uses a polynomial commitment scheme that is very similar to the one in BCMS20.

The following table provides a mapping between the variable names in BCMS20, and the equivalent objects in Halo 2 (which builds on the nomenclature from the Halo paper):

Halo 2's polynomial commitment scheme differs from Appendix A.2 of BCMS20 in two ways:

1. Step 8 of the $\text{Open}$ algorithm computes a "non-hiding" commitment $C^{\prime }$ prior to the inner product argument, which opens to the same value as $C$ but is a commitment to a randomly-drawn polynomial. The remainder of the protocol involves no blinding. By contrast, in Halo 2 we blind every single commitment that we make (even for instance and fixed polynomials, though using a blinding factor of 1 for the fixed polynomials); this makes the protocol simpler to reason about. As a consequence of this, the verifier needs to handle the cumulative blinding factor at the end of the protocol, and so there is no need to derive an equivalent to $C^{\prime }$ at the start of the protocol.

   • $C^{\prime }$ is also an input to the random oracle for ${\xi }_0$; in Halo 2 we utilize a transcript that has already committed to the equivalent components of $C^{\prime }$ prior to sampling $z$.

2. The ${\text{PC}}_{\text{DL}}.\text{SuccinctCheck}$ subroutine (Figure 2 of BCMS20) computes the initial group element $C_0$ by adding $[v]H^{\prime }=[vϵ]H$, which requires two scalar multiplications. Instead, we subtract $[v]G_0$ from the original commitment $P$, so that we're effectively opening the polynomial at the point to the value zero. The computation $[v]G_0$ is more efficient in the context of recursion because $G_0$ is a fixed base (so we can use lookup tables).

Implementation

Halo 2 proofs

Proofs as opaque byte streams

In proving system implementations like bellman, there is a concrete Proof struct that encapsulates the proof data, is returned by a prover, and can be passed to a verifier.

halo2 does not contain any proof-like structures, for several reasons:

• The Proof structures would contain vectors of (vectors of) curve points and scalars. This complicates serialization/deserialization of proofs because the lengths of these vectors depend on the configuration of the circuit. However, we didn't want to encode the lengths of vectors inside of proofs, because at runtime the circuit is fixed, and thus so are the proof sizes.
• It's easy to accidentally put stuff into a Proof structure that isn't also placed in the transcript, which is a hazard when developing and implementing a proving system.
• We needed to be able to create multiple PLONK proofs at the same time; these proofs share many different substructures when they are for the same circuit.

Instead, halo2 treats proof objects as opaque byte streams. Creation and consumption of these byte streams happens via the transcript:

• The TranscriptWrite trait represents something that we can write proof components to (at proving time).
• The TranscriptRead trait represents something that we can read proof components from (at verifying time).

Crucially, implementations of TranscriptWrite are responsible for simultaneously writing to some std::io::Write buffer at the same time that they hash things into the transcript, and similarly for TranscriptRead/std::io::Read.

As a bonus, treating proofs as opaque byte streams ensures that verification accounts for the cost of deserialization, which isn't negligible due to point compression.

Proof encoding

A Halo 2 proof, constructed over a curve $E({\mathbb{F}}_p)$, is encoded as a stream of:

• Points $P\in E({\mathbb{F}}_p)$) (for commitments to polynomials), and
• Scalars $s\in {\mathbb{F}}_q$) (for evaluations of polynomials, and blinding values).

For the Pallas and Vesta curves, both points and scalars have 32-byte encodings, meaning that proofs are always a multiple of 32 bytes.

The halo2 crate supports proving multiple instances of a circuit simultaneously, in order to share common proof components and protocol logic.

In the encoding description below, we will use the following circuit-specific constants:

• $k$ - the size parameter of the circuit (which has $2^k$ rows).
• $A$ - the number of advice columns.
• $F$ - the number of fixed columns.
• $I$ - the number of instance columns.
• $L$ - the number of lookup arguments.
• $P$ - the number of permutation arguments.
• ${\text{Col}}_P$ - the number of columns involved in permutation argument $P$.
• $D$ - the maximum degree for the quotient polynomial.
• $Q_A$ - the number of advice column queries.
• $Q_F$ - the number of fixed column queries.
• $Q_I$ - the number of instance column queries.
• $M$ - the number of instances of the circuit that are being proven simultaneously.

As the proof encoding directly follows the transcript, we can break the encoding into sections matching the Halo 2 protocol:

• PLONK commitments:

  • $A$ points (repeated $M$ times).
  • $2L$ points (repeated $M$ times).
  • $P$ points (repeated $M$ times).
  • $L$ points (repeated $M$ times).

• Vanishing argument:

  • $D-1$ points.
  • $Q_I$ scalars (repeated $M$ times).
  • $Q_A$ scalars (repeated $M$ times).
  • $Q_F$ scalars.
  • $D-1$ scalars.

• PLONK evaluations:

  • $(2+{\text{Col}}_P)\times P$ scalars (repeated $M$ times).
  • $5L$ scalars (repeated $M$ times).

• Multiopening argument:

  • 1 point.
  • 1 scalar per set of points in the multiopening argument.

• Polynomial commitment scheme:

  • $1+2k$ points.
  • $2$ scalars.

Fields

The Pasta curves that we use in halo2 are designed to be highly 2-adic, meaning that a large $2^S$ multiplicative subgroup exists in each field. That is, we can write $p-1\equiv 2^S\cdot T$ with $T$ odd. For both Pallas and Vesta, $S=32$; this helps to simplify the field implementations.

Sarkar square-root algorithm (table-based variant)

We use a technique from Sarkar2020 to compute square roots in halo2. The intuition behind the algorithm is that we can split the task into computing square roots in each multiplicative subgroup.

Suppose we want to find the square root of $u$ modulo one of the Pasta primes $p$, where $u$ is a non-zero square in ${\mathbb{Z}}_p^{\times }$. We define a $2^S$ root of unity $g=z^T$ where $z$ is a non-square in ${\mathbb{Z}}_p^{\times }$, and precompute the following tables:

$$gtab=\left[\begin{array}{cccc}{g}^0& g^1& ...& g^{2^8-1}\\ (g^{2^8}{)}^0& (g^{2^8}{)}^1& ...& (g^{2^8}{)}^{2^8-1}\\ (g^{2^{16}}{)}^0& (g^{2^{16}}{)}^1& ...& (g^{2^{16}}{)}^{2^8-1}\\ (g^{2^{24}}{)}^0& (g^{2^{24}}{)}^1& ...& (g^{2^{24}}{)}^{2^8-1}\end{array}\right]$$

$$invtab=\left[\begin{array}{cccc}(g^{2^{-24}}{)}^0& (g^{2^{-24}}{)}^1& ...& (g^{2^{-24}}{)}^{2^8-1}\end{array}\right]$$

Let $v=u^{(T-1)/2}$. We can then define $x=uv\cdot v=u^T$ as an element of the $2^S$ multiplicative subgroup.

Let $x_3=x,x_2=x_3^{2^8},x_1=x_2^{2^8},x_0=x_1^{2^8}.$

i = 0, 1

Using $invtab$, we lookup $t_0$ such that $$x_0=(g^{2^{-24}}{)}^{t_0}⟹x_0\cdot g^{t_0\cdot 2^{24}}=1.$$

Define ${\alpha }_1=x_1\cdot (g^{2^{16}}{)}^{t_0}.$

i = 2

Lookup $t_1$ s.t. $$\begin{array}{ll}{\alpha }_1=(g^{2^{-24}}{)}^{t_1}& ⟹x_1\cdot (g^{2^{16}}{)}^{t_0}=(g^{2^{-24}}{)}^{t_1}\\ & ⟹x_1\cdot g^{(t_0+2^8\cdot t_1)\cdot 2^{16}}=1.\end{array}$$

Define ${\alpha }_2=x_2\cdot (g^{2^8}{)}^{t_0+2^8\cdot t_1}.$

i = 3

Lookup $t_2$ s.t.

$$\begin{array}{ll}{\alpha }_2=(g^{2^{-24}}{)}^{t_2}& ⟹x_2\cdot (g^{2^8}{)}^{t_0+2^8\cdot t_1}=(g^{2^{-24}}{)}^{t_2}\\ & ⟹x_2\cdot g^{(t_0+2^8\cdot t_1+2^{16}\cdot t_2)\cdot 2^8}=1.\end{array}$$

Define ${\alpha }_3=x_3\cdot g^{t_0+2^8\cdot t_1+2^{16}\cdot t_2}.$

Final result

Lookup $t_3$ such that

$$\begin{array}{ll}{\alpha }_3=(g^{2^{-24}}{)}^{t_3}& ⟹x_3\cdot g^{t_0+2^8\cdot t_1+2^{16}\cdot t_2}=(g^{2^{-24}}{)}^{t_3}\\ & ⟹x_3\cdot g^{t_0+2^8\cdot t_1+2^{16}\cdot t_2+2^{24}\cdot t_3}=1.\end{array}$$

Let $t=t_0+2^8\cdot t_1+2^{16}\cdot t_2+2^{24}\cdot t_3$.

We can now write $$\begin{array}{lclcl}{x}_3\cdot g^t=1& ⟹& x_3& =& g^{-t}\\ & ⟹& u{v}^2& =& g^{-t}\\ & ⟹& uv& =& v^{-1}\cdot g^{-t}\\ & ⟹& uv\cdot g^{t/2}& =& v^{-1}\cdot g^{-t/2}.\end{array}$$

Squaring the RHS, we observe that $(v^{-1}{g}^{-t/2}{)}^2=v^{-2}{g}^{-t}=u.$ Therefore, the square root of $u$ is $uv\cdot g^{t/2}$; the first part we computed earlier, and the second part can be computed with three multiplications using lookups in $gtab$.

Gadgets

In this section we document some example gadgets and chip designs that are suitable for Halo 2.

Neither these gadgets, nor their implementations, have been reviewed, and they should not be used in production.

SHA-256

Specification

SHA-256 is specified in NIST FIPS PUB 180-4.

Unlike the specification, we use $⊞$ for addition modulo $2^{32}$, and $+$ for field addition. $\oplus$ is used for XOR.

Gadget interface

SHA-256 maintains state in eight 32-bit variables. It processes input as 512-bit blocks, but internally splits these blocks into 32-bit chunks. We therefore designed the SHA-256 gadget to consume input in 32-bit chunks.

Chip instructions

The SHA-256 gadget requires a chip with the following instructions:

#![allow(unused)]
fn main() {
extern crate halo2;
use halo2::plonk::Error;
use std::fmt;

trait Chip: Sized {}
trait Layouter<C: Chip> {}
const BLOCK_SIZE: usize = 16;
const DIGEST_SIZE: usize = 8;

pub trait Sha256Instructions: Chip {
    /// Variable representing the SHA-256 internal state.
    type State: Clone + fmt::Debug;
    /// Variable representing a 32-bit word of the input block to the SHA-256 compression
    /// function.
    type BlockWord: Copy + fmt::Debug;

    /// Places the SHA-256 IV in the circuit, returning the initial state variable.
    fn initialization_vector(layouter: &mut impl Layouter<Self>) -> Result<Self::State, Error>;

    /// Starting from the given initial state, processes a block of input and returns the
    /// final state.
    fn compress(
        layouter: &mut impl Layouter<Self>,
        initial_state: &Self::State,
        input: [Self::BlockWord; BLOCK_SIZE],
    ) -> Result<Self::State, Error>;

    /// Converts the given state into a message digest.
    fn digest(
        layouter: &mut impl Layouter<Self>,
        state: &Self::State,
    ) -> Result<[Self::BlockWord; DIGEST_SIZE], Error>;
}
}

TODO: Add instruction for computing padding.

This set of instructions was chosen to strike a balance between the reusability of the instructions, and the scope for chips to internally optimise them. In particular, we considered splitting the compression function into its constituent parts (Ch, Maj etc), and providing a compression function gadget that implemented the round logic. However, this would prevent chips from using relative references between the various parts of a compression round. Having an instruction that implements all compression rounds is also similar to the Intel SHA extensions, which provide an instruction that performs multiple compression rounds.

16-bit table chip for SHA-256

This chip implementation is based around a single 16-bit lookup table. It requires a minimum of $2^{16}$ circuit rows, and is therefore suitable for use in larger circuits.

We target a maximum constraint degree of $9$. That will allow us to handle constraining carries and "small pieces" to a range of up to $\{\mathrm{0..7}\}$ in one row.

Compression round

There are $64$ compression rounds. Each round takes 32-bit values $A,B,C,D,E,F,G,H$ as input, and performs the following operations:

$$\begin{array}{rcl}Ch(E,F,G)& =& (E\wedge F)\oplus (\neg E\wedge G)\\ Maj(A,B,C)& =& (A\wedge B)\oplus (A\wedge C)\oplus (B\wedge C)\\ & =& count(A,B,C)\ge 2\\ {\Sigma }_0(A)& =& (A⋙2)\oplus (A⋙13)\oplus (A⋙22)\\ {\Sigma }_1(E)& =& (E⋙6)\oplus (E⋙11)\oplus (E⋙25)\\ H^{\prime }& =& H+Ch(E,F,G)+{\Sigma }_1(E)+K_t+W_t\\ E_{new}& =& reduc{e}_6(H^{\prime }+D)\\ A_{new}& =& reduc{e}_7(H^{\prime }+Maj(A,B,C)+{\Sigma }_0(A))\end{array}$$

where $reduc{e}_i$ must handle a carry $0\le carry<i$.

Define $\mathtt{spread}$ as a table mapping a $16$-bit input to an output interleaved with zero bits. We do not require a separate table for range checks because $\mathtt{spread}$ can be used.

Modular addition

To implement addition modulo $2^{32}$, we note that this is equivalent to adding the operands using field addition, and then masking away all but the lowest 32 bits of the result. For example, if we have two operands $a$ and $b$:

$$a⊞b=c,$$

we decompose each operand (along with the result) into 16-bit chunks:

$$(a_L:{\mathbb{Z}}_{2^{16}},a_H:{\mathbb{Z}}_{2^{16}})⊞(b_L:{\mathbb{Z}}_{2^{16}},b_H:{\mathbb{Z}}_{2^{16}})=(c_L:{\mathbb{Z}}_{2^{16}},c_H:{\mathbb{Z}}_{2^{16}}),$$

and then reformulate the constraint using field addition:

$$\mathsf{carry}\cdot 2^{32}+c_H\cdot 2^{16}+c_L=(a_H+b_H)\cdot 2^{16}+a_L+b_L.$$