We explain in this post how to think about and leverage the type of arithmetization used in PLONK. In its most general form, we refer to such an arithmetization as a Randomized Air with Preprocessing, RAP for short. However, in practice it will usually be convenient to work with restricted cases of RAPs, that we call turbo-Plonk and ultra-Plonk programs. We will explain all these terms!
Our starting point is Algebraic Intermediate Representations - AIRs; this is the arithmetization used by STARKWARE.
An AIR[1]
An execution trace
A STARK enables proving we know a valid execution trace for
Let's look at a classical example - the Fibonacci sequence.
We use width
And we use the constraint polynomials
A valid trace of length
1 | 1 |
2 | 3 |
5 | 8 |
13 | 21 |
That is, a valid trace must contain consecutive elements of the Fibonacci sequence. So, for example, adding a boundary condition on the second value of the fourth row being 21 would validate this is indeed the correct 8'th Fibonacci element.
In a Preprocessed AIR, or PAIR
An execution trace now consists of the
(We refer to the columns supplied by the prover as the witness part of the execution trace.)
For example when
The constraint polynomials
To illustrate the power of PAIRs let's see how we can use them to simulate an AIR where the constraints are different for different rows.[3]
A natural example is an AIR where for some rows we would like to perform an addition of the row values (and, say, obtain the addition result in the first column of the row below); and for the other rows we wish to perform multiplication.
For this purpose we define the PAIR
The single constraint polynomial of
The variable
It is clear that an addition or multiplication relation is enforced according to the value of
For example, in a program where we wish to perform two additions and then a multiplication the execution trace could look like this (note that the last row is unconstrained):
Because the predefined columns can be used in this way to select the operation, they are often referred to as "selectors".[4]
The above example hints and suggests the typical way people design a PAIR: We predefine several sets of constraints, thinking of each one as a "gate".
Then, when designing our final program we assign one of these gates to each row. As in the above example, selectors will be used to "compile" our program into a PAIR.
It is worth noting that in addition to using the selectors to switch between gates, many times a gate itself will use selectors to enable more flexibility. A typical example is a gate for elliptic curve addition by a predefined point - the predefined point will be encoded in the selector values.
Our final model allows rounds of interaction, where the verifier sends random field elements, and the prover can subsequently add more columns after seeing these field elements.
The constraint polynomials will now be able to use the verifier randomness as additional variables.
We'll call such a program a RAP - Randomized AIR with Preprocessing.
Let's illustrate RAPs with the following example. Suppose we had a width 2 AIR and wanted to check that the columns provided by the prover are a permutation of each other.
Suppose the values of these columns are
From the Schwartz-Zippel Lemma we know that to check they are a permutation of each other it suffices to check that for a uniformly chosen
With high probability over
A RAP of length
If
Additonally, the program must check
For this purpose
Note that applying this on row
or assuming
which inductively enforces the
For illustration, here's what a valid execution trace of this program what look like, when
What is perhaps philosophically interesting here, is that randomness enables a local constraint (between adjacent rows) to verify a global property (the columns being a permutation of each other).
RAPs are more powerful than PAIRs; however, for program design it is usually convenient to just think of a PAIR, while allowing oneself to use as a black box some special functionalites of a RAP. Later, the program will be compiled to the final RAP.
One such special functionality of a RAP that is very useful is enforcing copy constraints.
This means enforcing that certain elements of the trace are equal. For example "The second element of the first column
A turbo-plonk program is a PAIR with the extra ability to define copy constraints between any two elements of the execution trace.
Copy constraints enable a designer to abstract away explicitly thinking about the execution trace and PAIR, and rather design a program like this:
The above might seem trivial and not saying much. However, the reason copy constraints are essential for this simplified design approach, is that when a witness variable participates in two gates, a copy constraint will ensure the same value is indeed used in both gates, even though they might end up appearing in totally different rows in the actual RAP.
An ultra-Plonk program[5] is a turbo-Plonk program with an extra, very powerful, type of gate called a lookup gate.
What this means is that as part of designing the program, we define a set of tables
Now, when designing the program; we are allowed to use lookup gates that have the form: "Check that the tuple of these
At this point, the leap from RAPs to programs with such functionalities might seem a bit magical. See this post for details on how copy constraints and lookup tables can indeed be implemented via the multiset check we showed in the previous section.
Enabling lookup gates has a significant cost in the final SNARK; as a rule of thumb it pays off once the number of lookups is as large as the table.
For a program designer, it will usually be convenient to work with turbo and ultra-plonk programs, thinking what gates to apply on which witness variables. This is already pretty low-level and both complicated and versatile enough! However, it is good sometimes to remember there is a RAP under the hood, that when needed, might be used to get more specific/efficient functionality taking advantage of the verifier randomness.
If you are familiar with SNARK development and literature you've probably seen the R1CS constraint format, where all constraints have the form
R1CS nicely captures the constraint format of a sequence of works starting from [GGPR] up to the optimized version of Groth. This line of work relies on checking verifier equations on a secret element in the exponent. As we currently have at our disposal cryptographic
However the polynomial IOP approach to constructing SNARKs, that perhaps explicitly started with Sonic, enables a more flexible constraint format. In particular, it is possible to use constraints of degree larger than two.
When using the GGPR approach R1CS has a nice theoretical advatange - no need for the random oracle model; and a nice practical advantage - the number of prover group exponentiations doesn't depend on the number or fan-in of the addition gates. However, obtaining these advantages requires a per circuit trusted setup.
Assuming we are using universal setup systems like Sonic, Plonk and Marlin, it might be harder to argue we should restrict ourselves to R1CS.
See Definition 1 here for the fully general description of AIRs by STARKWARE. ↩︎
One could ask why have constraints just between elements of two consecutive rows? Indeed, the general definition of AIRs is parameterized by a set of "masks"
In fact, STARKWARE's general definition of AIRs does have partial ability to have different constraints for different rows. The reason it is partial, is the verifier has to pay a price in the arithmetic complexity of the vanishing polynomial of that subset of rows. (Again, see here for exact details.) ↩︎
See Section 6 of the Plonk paper and the turbo-Plonk paper for more examples of using selectors. ↩︎
Electric Coin Company define a very similar notion of ultra-Plonk Arithmetization as part of the Halo 2 project. One main difference is both their definition and implementation allow constraints between rows in arbitrary offsets. ↩︎