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 denote a cycle where maps to , maps to , and maps to (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, denotes the permutation that maps to , to , to , and to .

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:

From this we have the equality-constraint sets and . We want to construct the permutation:

which defines the mapping of to .

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 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 :

  1. Check whether and are already in the same cycle, i.e. whether . If so, there is nothing to do.
  2. Otherwise, and belong to different cycles. Make the larger cycle and the smaller one, by swapping them iff .
  3. Set .
  4. Following the mapping around the right (smaller) cycle, for each element set .
  5. 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

Broken alternatives

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 .

Argument specification

We need to check a permutation of cells in columns, represented in Lagrange basis by polynomials .

We first label each cell in those columns with a unique element of .

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.

If we have a permutation , we can represent it as a vector of polynomials such that .

Notice that the identity permutation can be represented by the vector of polynomials such that .

Now given our permutation represented by over columns represented by , we want to ensure that:

Let be such that and for :

Then it is sufficient to enforce the constraints:

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.