halo2 uses the following lookup technique, which allows for lookups in arbitrary sets, and is arguably simpler than Plookup.
In addition to the general notes on language:
- We call the polynomial (the grand product argument polynomial for the permutation argument) the "permutation product" column.
For ease of explanation, we'll first describe a simplified version of the argument that ignores zero knowledge.
We express lookups in terms of a "subset argument" over a table with rows (numbered from 0), and columns and
The goal of the subset argument is to enforce that every cell in is equal to some cell in This means that more than one cell in can be equal to the same cell in and some cells in don't need to be equal to any of the cells in
- 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).
- and can contain duplicates. If the sets represented by and/or are not
naturally of size we extend with duplicates and with dummy values known
to be in
- Alternatively we could add a "lookup selector" that controls which elements of the column participate in lookups. This would modify the occurrence of in the permutation rule below to replace with, say, if a lookup is not selected.
Let be the Lagrange basis polynomial that evaluates to at row and otherwise.
We start by allowing the prover to supply permutation columns of and Let's call these and respectively. We can enforce that they are permutations using a permutation argument with product column with the rules:
i.e. provided that division by zero does not occur, we have for all :
This is a version of the permutation argument which allows and to be permutations of and respectively, but doesn't specify the exact permutations. and 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 and to be arranged by the prover in a particular way:
- All the cells of column 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 and that is a permutation of
- The first row in a sequence of like values in is the row that has the corresponding value in Apart from this constraint, is any arbitrary permutation of
Now, we'll enforce that either or that using the rule
In addition, we enforce using the rule
(The term of the first rule here has no effect at row even though "wraps", because of the second rule.)
Together these constraints effectively force every element in (and thus ) to equal at least one element in (and thus ). Proof: by induction on prefixes of the rows.
In order to achieve zero knowledge for the PLONK-based proof system, we will need the last rows of each column to be filled with random values. This requires an adjustment to the lookup argument, because these random values would not satisfy the constraints described above.
We limit the number of usable rows to We add two selectors:
- 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 constraints from above only for the usable rows:
The rules that are enabled on row remain the same:
Since we can no longer rely on the wraparound to ensure that the product becomes again at we would instead need to constrain to However, there is a potential difficulty: if any of the values or are zero for then it might not be possible to satisfy the permutation argument. This occurs with negligble probability over choices of and but is an obstacle to achieving perfect zero knowledge (because an adversary can rule out witnesses that would cause this situation), as well as perfect completeness.
To ensure both perfect completeness and perfect zero knowledge, we allow to be either zero or one:
Now if or are zero for some we can set for satisfying the constraint system.
Note that the challenges and are chosen after committing to and (and to and ), so the prover cannot force the case where some or is zero to occur. Since this case occurs with negligible probability, soundness is not affected.
- There is the original column and the fixed column
- There is a permutation product column
- There are the two permutations and
- The gates are all of low degree.
halo2's lookup argument implementation generalizes the above technique in the following ways:
- and can be extended to multiple columns, combined using a random challenge.
and stay as single columns.
- The commitments to the columns of can be precomputed, then combined cheaply once the challenge is known by taking advantage of the homomorphic property of Pedersen commitments.
- The columns of 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 in each row, consider
as a set of tuples (using the method of the previous point), and check
- In the case where 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.