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.
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 denote a cycle where maps to maps to and maps to (with the obvious generalization to arbitrary-sized cycles). Writing two or more cycles next to each other denotes a composition of the corresponding permutations. For example, denotes the permutation that maps to to to and to
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:
From this we have the equality-constraint sets and We want to construct the permutation:
which defines the mapping of to
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 for the permutation itself;
- an auxiliary array that keeps track of a distinguished element of each cycle;
- another array that keeps track of the size of each cycle.
We have the invariant that for each element in a given cycle points to the same element This allows us to quickly decide whether two given elements and are in the same cycle, by checking whether Also, gives the size of the cycle containing (This is guaranteed only for not for )
The algorithm starts with a representation of the identity permutation: for all we set and
To add an equality constraint :
- Check whether and are already in the same cycle, i.e. whether If so, there is nothing to do.
- Otherwise, and belong to different cycles. Make the larger cycle and the smaller one, by swapping them iff
- Following the mapping around the right (smaller) cycle, for each element set
- Splice the smaller cycle into the larger one by swapping with
For example, given two disjoint cycles and :
A +---> B ^ + | | + v D <---+ C E +---> F ^ + | | + v H <---+ G
After adding constraint the above algorithm produces the cycle:
A +---> B +-------------+ ^ | | | + v D <---+ C <---+ E F ^ + | | + v H <---+ G
If we did not check whether and were already in the same cycle, then we could end up undoing an equality constraint. For example, if we have the following constraints:
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 rather than the correct
We need to check a permutation of cells in columns, represented in Lagrange basis by polynomials
We will label each cell in those columns with a unique element of
Suppose that we have a permutation on these labels, in which the cycles correspond to equality-constraint sets.
If we consider the set of pairs , then the values within each cycle are equal if and only if permuting the label in each pair by yields the same set:
Since the labels are distinct, set equality is the same as multiset equality, which we can check using a product argument.
Let be a root of unity and let be a root of unity, where with odd and We will use as the label for the cell in the th row of the th column of the permutation argument.
We represent by a vector of polynomials such that
Notice that the identity permutation can be represented by the vector of polynomials such that
We will use a challenge to compress each pair to Just as in the product argument we used for lookups, we also use a challenge to randomize each term of the product.
Now given our permutation represented by over columns represented by we want to ensure that:
Here represents the unpermuted pair, and represents the permuted pair.
Let be such that and for :
Then it is sufficient to enforce the rules:
This assumes that the number of columns is such that the polynomial in the first rule above fits within the degree bound of the PLONK configuration. We will see below how to handle a larger number of columns.
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 are all distinct quadratic non-residues, provided that the number of columns that are enabled for equality is no more than , which always holds in practice for the curves used in Halo 2.
Similarly to the lookup argument, we need an adjustment to the above argument to account for the last rows of each column being filled with random values.
We limit the number of usable rows to We add two selectors, defined in the same way as for the lookup argument:
- is set to on the last rows, and elsewhere;
- is set to only on row and elsewhere (i.e. it is set on the row in between the usable rows and the blinding rows).
We enable the product rule from above only for the usable rows:
The rule that is enabled on row remains the same:
Since we can no longer rely on the wraparound to ensure that each product becomes again at we would instead need to constrain This raises the same problem that was described for the lookup argument. So we allow to be either zero or one:
which gives perfect completeness and zero knowledge.
The halo2 implementation does not in practice limit the number of columns for which equality constraints can be enabled. Therefore, it must solve the problem that the above approach might yield a product rule with a polynomial that exceeds the PLONK configuration's degree bound. The degree bound could be raised, but this would be inefficient if no other rules require a larger degree.
Instead, we split the product across sets of columns, using product columns and we use another rule to copy the product from the end of one column set to the beginning of the next.
That is, for we have:
For simplicity this is written assuming that the number of columns enabled for equality constraints is a multiple of ; if not then the products for the last column set will have fewer than terms.
For the first column set we have:
For each subsequent column set, we use the following rule to copy to the start of the next column set, :
For the last column set, we allow to be either zero or one:
which gives perfect completeness and zero knowledge as before.