ZK Fundamentals: Intermediate Representations
We cover e.g. NP characterization, Boolean Satisfiability, R1CS, Plonkish arithmatization, and Customizable Constraint System (CCS)
This is the sixth article from our series exploring ZK fundamentals, zero knowledge proofs and related notions. Read the first ones here:
ZK Fundamental series:
📚 Part I: What is a proof?
📚 Part II: Interactive Proofs
📚 Part III: Zero-Knowledge
📚 Part IV: The Fiat-Shamir Transform
📚 Part V: Succinctness
📚 Part VI: Intermediate representations
In past articles, we have seen how interaction and randomness can be used in the construction of powerful proof systems. We have defined the paradoxical notion of zero-knowledge, which defies all our intuition about what is possible. We discussed how to capture this notion mathematically and introduced various definitions of zero-knowledge according to the soundness required.
We have seen how things can be rendered non-interactive, which led us to the discussion of various computational models, i.e., the Standard Model, the Common Reference String Model and the Random Oracle Model.
Lastly, we discussed succinctness and have seen that surprisingly, the verifier does not need to read the whole proof to be convinced by it. The buzzword here was the PCP Theorem, one of the biggest achievements in complexity theory.
With all this background covered, we are now in a position to follow and appreciate the dizzying developments in this domain. Before diving into the world of ingenious ideas and mesmerizing constructions that have come up in recent years, we have to take a short break and talk a bit about representations.
This article can be considered medium to advanced level and includes math. We cover topics such as NP characterization, Boolean Satisfiability, R1CS, Plonkish Arithmetization, and the Customizable Constraint System (CCS).
An NP characterization
Given an NP language L, using our proof system we want to provide proofs for statements of the form x ∈ L.
So, there is a corresponding relation Rʟ, efficiently computable, such that:
In the first article on Zero-Knowledge Proofs (see the chapter “The class N P” ), we have seen that there is a certain subclass of languages within NP, called the NP-complete languages, which can be used to “simulate” all other languages in NP.
Wait, what is NP language?
NP stand for Non-deterministic Polynomial time. For a language to be in NP, there must be a quick (polynomial-time) method (the relation Rʟ above) to verify whether a given string belongs to that language, provided you are given the correct certificate or witness (the element w above)
“NP-complete language” represents the most challenging problems within NP, characterized by the property that any problem in NP can be efficiently transformed into an instance of the NP-complete problem.
Let’s continue:
Given an NP-complete language L in NP, for any other language M in NP, membership questions for M can be reduced to a question about membership of a corresponding element in L.
We mentioned graph 3-coloring is in NP: given a graph, a proper coloring can be verified efficiently. Moreover, it is NP-complete: given any other language in NP, it is possible to transform membership questions for this language into a question about 3-colorability of a corresponding graph. In this sense, graph 3-coloring provides a way of representing problems.
It is however not the most suitable one for providing proofs. In other words, if you want to prove to someone that you performed a computation, it might not be the most efficient way to turn it first into a graph coloring instance and then provide a proof that you know a coloring.
Boolean Satisfiability
A much more efficient and commonly employed way is to use satisfiability problems. Given a boolean formula (a formula in propositional logic) which is built from boolean variables and constants using the operations:
- AND (∧, conjunction)
- OR (∨, disjunction) and
- NOT (¬ , negation),
…the question is to determine whether there is a satisfying interpretation, i.e., if there is an assignment of logical values (TRUE or FALSE) to the variables in the formula such that it evaluates to TRUE.
The corresponding language (set of all satisfiable boolean formulas) is denoted by SAT and is the first language shown to be NP-complete. It is immediate to see that SAT ∈ NP: given a formula and a witness (a satisfying assignment) it is easy to check that with the given assignment the formula evaluates to TRUE.
Showing that other NP languages can be efficiently reduced to SAT instances (i.e. to show that SAT is NP-hard) is more involved. We have to show that for any language L in NP, there is an efficiently computable reduction map F such that for any x we have x ∈ L if and only if F(x) ∈ SAT.
We have to provide a way of doing this reduction independently of the language from NP that is being considered. The idea is to take the verification procedure of the NP language and turn it into a boolean formula whose different parts are just checking the validity of various steps in the verification procedure.
The witness fed into the verification procedure is turned into the assignment satisfying the resulting formula. So checking if a given assignment satisfies the boolean formula in fact just checks that the verification procedure on the witness from which the assignment was obtained is done correctly. This is the famous Cook-Levin Theorem. Great expositions of its proof are abundant.
SAT is in fact a more efficient universal (NP-complete) way of representing our problems.
We can even go further. Thinking of TRUE and FALSE as 1 and 0 seen as integers modulo 2, the operation AND turns into multiplication, to negate we just subtract 1. OR can be expressed using AND and NOT by De Morgan’s law. So it is easy to show that SAT is equivalent to solving multivariate polynomial equations with coefficients in the integers modulo 2 (addition corresponding to XOR).
Although at first, this might seem just like a notational change, in fact, a lot is gained! Now we have the whole machinery of algebra at our disposal, which helps us substantially in the construction of proof systems (try defining an analog of elliptic curves starting with graphs rather than finite fields).
More generally one can consider polynomials with coefficients in the integers modulo a prime p, with the usual addition and multiplication modulo p, i.e. a finite field 𝔽ₚ of order p and ask whether there are assignments of elements in 𝔽ₚ to the variables that make the polynomial evaluate to 0. Let’s call this the arithmetic satisfiability problem (as opposed to boolean satisfiability). It is NP-complete and we again have an NP characterization that we can use to express things in. It is a generalization of usual boolean satisfiability (satisfiability of boolean circuits), is very expressive and intimately related to powerful constructs from number theory and algebraic geometry.
Tailoring your polynomials like a dress
As it turns out, most general polynomial systems are too general to be efficient in practice.
In particular, it is difficult for certain gadgets in the proof system to handle equations in their full generality. Restricting polynomials to a special form and using gadgets tailored specifically to that form has proven to be not only easier conceptually but also better from a computational perspective.
When restricting to a subclass we have to take care however that the subclass is equally expressive. Restricting for instance only to linear equations as they are easier to handle might not be the best idea, as we lose in expressiveness.
What the right definition of the subclass of equations is depends on several criteria:
- It should be easy to convert given instances to this subclass (if converting instances to representations creates a big overhead, even the best prover will be useless)
- It should fit suitably into the larger constructions within which it is used
- It should be efficient, etc.
So, the right representation, like a suit, has to be tailored according to your needs. And coming up with the right representation is an art on its own. We need to strike a fine balance.
Having for instance very simple building blocks might cause the size of the representation to explode. Having too complicated ones, on the other hand, might lead to indigestible huge blocks that cannot be handled at once.
Tailoring the language to a very particular type of problems might help with efficiency for those, but we will have to pay a toll for the more general cases.
And most importantly, the representation should be adequate for the larger proof system that will build on it. The proof system will take the representation and will turn it according to its inner workings into a form it will operate on.
Hence this representation is called an intermediate representation (IR). Reducing the initial problem (statement to be proven) to the intermediate representation is called the frontend, and the proof system yielding proof from the intermediate representation is called the backend.
Over the years several representations have proven their worth and have become the prevalent ones, each with their own virtue.
We will spend the rest of this article introducing some of the popular intermediate representations.
R1CS: Rank-1 Constraint System
Let us start with one of the first intermediate representations, R1CS, Rank-1 Constraint System.
It is simple, elegant and stood the test of time. We had introduced it already in our previous articles on NOVA, so let us revisit it.
These are polynomial equations (arithmetic circuits) of a particular shape: Rather than having one big polynomial of possibly high degree, we have several equations, each of degree at most 2 and each of a particular type (rank 1).
It consists of several equations, each of the type:
a(Z) ḃ(Z) — c(Z) = 0
Where Z = (z₁, …, zᵣ) is the vector of variables,
a(Z) = a₁ • z₁ + … + aᵣ • zᵣ
b(Z) = b₁ • z₁ + … + bᵣ • zᵣ
c(Z) = c₁ • z₁ + … + cᵣ • zᵣ
are linear functions of the variables. Here the aᵢ, bᵢ, cᵢ are constants in the finite field 𝔽ₚ
So each equation is of the form
(a₁ • z₁ + … + aᵣ • zᵣ) • (b₁ • z₁ + … + bᵣ • zᵣ) — (c₁ • z₁ + … + cᵣ • zᵣ) = 0
Note that this is only one of the polynomials. To define the arithmetic circuit we allow several polynomials of this form:
(aᵢ,₁ • z₁ + … + aᵢ,ᵣ • zᵣ) • (bᵢ,₁ • z₁ + … + bᵢ,ᵣ • zᵣ) — (c₁,ᵢ • z₁ + … + cᵢ,ᵣ • zᵣ) = 0
for various values of i.
Most of these coefficients will be assumed to be zero, so the polynomials are sparse.
In case you have any doubts about the expressivity of such systems (if we restrict to degree 2 polynomials, ones of a particular form on top of that, how can we express more general polynomial equations?), a moment of reflection will reveal that everything is OK, as we can always increase the number of variables, introducing intermediate (dummy) variables, to recover higher degree polynomials:
We can express x² as the product of the two linear polynomials x and x. To express x³ we would just introduce a new dummy variable w and use the R1CS equation x • x — w = 0 to define w as x² and would have x³ at our disposal as w • x = (x²) * x. This process is known as flattening.
Why would one come up with such a definition?
One reason is historic: it is a generalization of a construction that is applied to circuits. A circuit consists of various input wires, which can be fed into addition and multiplication gates. The outputs of these gates can again be fed into gates.
For each multiplication gate we add a constraint. The multiplication has a left input and a right input and an output, hence a(Z), b(Z), and c(Z), and the relation between them.
The two inputs can be outputs from additions (hence we allow linear combinations). The output should in fact be just one variable, where here it is a linear combination, but as said above, this is a generalization.
Another way to look at this is that R1CS is tailored to the proof system it is going to be used with. This has to do with a certain gadget used in the proof system (for instance in the case of Pinocchio) that is employed, namely pairings of elliptic curves. These can be used to prove equations of the form
A(x) • B(X) - C(X) = Z(x) • Q(X)
that result from the rank-1 constraint, but would not work directly for equations involving more complicated terms.
One thing to note is that in rank-1 constraint systems linear combinations of variables (so multiplication by fixed scalars and additions) can be fed directly into the three terms (the terms are in fact linear combinations). So taking linear combinations (and hence addition) is for free in R1CS.
Plonkish Arithmetization
Next, we want to introduce a constraint system that has come to be known as Plonkish arithmetization.
See the nice paper Customizable constraint systems for succinct arguments by Setty, Thaler and Wahby for a nice introduction.
Let’s build this up bit by bit. We will use multivariate polynomials to define gates.
For an addition gate, we would use:
…to define X₂ to be the sum of X₀ and X₁
For a multiplication gate, we would use:
…to define X₂ to be the product of X₀ and X₁
We want to have more general gates (called custom gates) than just addition and multiplication, so we allow more general multivariate polynomials
In this case:
- Setting X₃ equal to 1 we would get a multiplication gate
- Setting X₃ equal to 0 we would get an addition gate
In general, by introducing k selector variables we can simulate different polynomials, turning them on or off accordingly.
Given such a gate, we want to use it several times with different inputs. So for each time the gate is used to add a constraint we specify the input to the polynomial using a vector T
Here the input also includes the selector constants and we don’t distinguish between those and the input/witness variables. We form a vector z consisting of the input, witness and the selector constants, say of length k.
Now T[0] will give the index of z at which the element to be substituted for X₀ is located. So for X₀ we substitute z[T[0]], for X₁ we substitute z[T[1]], etc. In general, there will be several such constraints, so we will have several indexing vectors T₀, T₁, …, Tₘ₋₁
Customizable Constraint System (CCS)
We will finish with an intermediate representation introduced by Setty, Thaler and Wahby, namely Customizable Constraint System, short CCS.
CCS is general enough to have R1CS and Plonkish Arithmetization, as well as AIR (Algebraic Intermediate Representation), which is used in STARKs, as particular cases.
In the rank-1 constraint system introduced above we had two terms, one consisting of a product of two linear combinations A(x) • B(x) and one consisting of a product of 1 linear combination, hence just a linear combination — C(X). There is no reason to restrict to just two terms, and have 2 and 1 factor in these.
Allowing several terms, each consisting of a product of several linear combinations we arrive at what is called a customizable constraint system. It clearly generalized R1CS and it is not difficult to see that Plonkish arithmetization can also be seen as a special case of CCS.
In the paper Setty, Thaler and Wahby show that the proof system Spartan (which works for R1CS) can easily be modified to work CCS and compiling with a polynomial commitment scheme one obtains SNARKS for CCS, which they named SuperSpartan.
Final thoughts
As Wittgenstein said, all we know is what we have words for. This doesn’t apply only to our daily languages, but also to the NP language and the corresponding representation we use to express the statement we want to provide a proof for. The representation is what we build on and it is decisive in what we can do on top of it.
As detailed above, the representation should be expressive, efficient (compact), flexible enough to be suitable for a variety of statements and well-suited to be used within the larger proof system. So rather than being just an abstruse notational detail, it is one of the pillars on which the full complex construction of the proof system rests.
This article aimed to give a first glimpse of some of the representations that are around and to show why they are important. Now that we have covered the basic notions and have our representation, we are ready to embark on a journey into the wild worlds of proof system with its ingenious and thrilling constructions.
Author: Alp Bassa, Research Scientist at Veridise
Want to learn more about Veridise?
Twitter | Lens | LinkedIn | Github | Request Audit
