This is a mirror of the post at https://medium.com/@VitalikButerin/quadratic-arithmetic-programs-from-zero-to-hero-f6d558cea649
There has been a lot of interest lately in the technology behind zk-SNARKs, and people are increasingly trying to demystify something that many have come to call “moon math” due to its perceived sheer indecipherable complexity. zk-SNARKs are indeed quite challenging to grasp, especially due to the sheer number of moving parts that need to come together for the whole thing to work, but if we break the technology down piece by piece then comprehending it becomes simpler.
The purpose of this post is not to serve as a full introduction to zk-SNARKs; it assumes as background knowledge that (i) you know what zk-SNARKs are and what they do, and (ii) know enough math to be able to reason about things like polynomials (if the statement
The steps here can be broken up into two halves. First, zk-SNARKs cannot be applied to any computational problem directly; rather, you have to convert the problem into the right “form” for the problem to operate on. The form is called a “quadratic arithmetic program” (QAP), and transforming the code of a function into one of these is itself highly nontrivial. Along with the process for converting the code of a function into a QAP is another process that can be run alongside so that if you have an input to the code you can create a corresponding solution (sometimes called “witness” to the QAP). After this, there is another fairly intricate process for creating the actual “zero knowledge proof” for this witness, and a separate process for verifying a proof that someone else passes along to you, but these are details that are out of scope for this post.
The example that we will choose is a simple one: proving that you know the solution to a cubic equation:
Let us write out our function as follows:
def qeval(x):
y = x**3
return x + y + 5
The simple special-purpose programming language that we are using here supports basic arithmetic (
You can extend the language to modulo and comparisons by providing bit decompositions (eg.
Let us now go through this process step by step. If you want to do this yourself for any piece of code, I implemented a compiler here (for educational purposes only; not ready for making QAPs for real-world zk-SNARKs quite yet!).
The first step is a “flattening” procedure, where we convert the original code, which may contain arbitrarily complex statements and expressions, into a sequence of statements that are of two forms:
sym_1 = x * x
y = sym_1 * x
sym_2 = y + x
~out = sym_2 + 5
If you read the original code and the code here, you can fairly easily see that the two are equivalent.
Now, we convert this into something called a rank-1 constraint system (R1CS). An R1CS is a sequence of groups of three vectors (
But instead of having just one constraint, we are going to have many constraints: one for each logic gate. There is a standard way of converting a logic gate into a
First, we’ll provide the variable mapping that we’ll use:
'~one', 'x', '~out', 'sym_1', 'y', 'sym_2'
The solution vector will consist of assignments for all of these variables, in that order.
Now, we’ll give the
a = [0, 1, 0, 0, 0, 0]
b = [0, 1, 0, 0, 0, 0]
c = [0, 0, 0, 1, 0, 0]
You can see that if the solution vector contains
Now, let’s go on to the second gate:
a = [0, 0, 0, 1, 0, 0]
b = [0, 1, 0, 0, 0, 0]
c = [0, 0, 0, 0, 1, 0]
In a similar style to the first dot product check, here we’re checking that
Now, the third gate:
a = [0, 1, 0, 0, 1, 0]
b = [1, 0, 0, 0, 0, 0]
c = [0, 0, 0, 0, 0, 1]
Here, the pattern is somewhat different: it’s multiplying the first element in the solution vector by the second element, then by the fifth element, adding the two results, and checking if the sum equals the sixth element. Because the first element in the solution vector is always one, this is just an addition check, checking that the output equals the sum of the two inputs.
Finally, the fourth gate:
a = [5, 0, 0, 0, 0, 1]
b = [1, 0, 0, 0, 0, 0]
c = [0, 0, 1, 0, 0, 0]
Here, we’re evaluating the last check, ~out
And there we have our R1CS with four constraints. The witness is simply the assignment to all the variables, including input, output and internal variables:
[1, 3, 35, 9, 27, 30]
You can compute this for yourself by simply “executing” the flattened code above, starting off with the input variable assignment
The complete R1CS put together is:
A
[0, 1, 0, 0, 0, 0]
[0, 0, 0, 1, 0, 0]
[0, 1, 0, 0, 1, 0]
[5, 0, 0, 0, 0, 1]
B
[0, 1, 0, 0, 0, 0]
[0, 1, 0, 0, 0, 0]
[1, 0, 0, 0, 0, 0]
[1, 0, 0, 0, 0, 0]
C
[0, 0, 0, 1, 0, 0]
[0, 0, 0, 0, 1, 0]
[0, 0, 0, 0, 0, 1]
[0, 0, 1, 0, 0, 0]
The next step is taking this R1CS and converting it into QAP form, which implements the exact same logic except using polynomials instead of dot products. We do this as follows. We go 3from four groups of three vectors of length six to six groups of three degree-3 polynomials, where evaluating the polynomials at each x coordinate represents one of the constraints. That is, if we evaluate the polynomials at
We can make this transformation using something called a Lagrange interpolation. The problem that a Lagrange interpolation solves is this: if you have a set of points (ie.
Let’s do an example. Suppose that we want a polynomial that passes through
(x - 2) * (x - 3)
Which looks like this:
Now, we just need to “rescale” it so that the height at x=1 is right:
(x - 2) * (x - 3) * 3 / ((1 - 2) * (1 - 3))
This gives us:
1.5 * x**2 - 7.5 * x + 9
We then do the same with the other two points, and get two other similar-looking polynomials, except that they “stick out” at
1.5 * x**2 - 5.5 * x + 7
With exactly the coordinates that we want. The algorithm as described above takes
Now, let’s use Lagrange interpolation to transform our R1CS. What we are going to do is take the first value out of every
A polynomials
[-5.0, 9.166, -5.0, 0.833]
[8.0, -11.333, 5.0, -0.666]
[0.0, 0.0, 0.0, 0.0]
[-6.0, 9.5, -4.0, 0.5]
[4.0, -7.0, 3.5, -0.5]
[-1.0, 1.833, -1.0, 0.166]
B polynomials
[3.0, -5.166, 2.5, -0.333]
[-2.0, 5.166, -2.5, 0.333]
[0.0, 0.0, 0.0, 0.0]
[0.0, 0.0, 0.0, 0.0]
[0.0, 0.0, 0.0, 0.0]
[0.0, 0.0, 0.0, 0.0]
C polynomials
[0.0, 0.0, 0.0, 0.0]
[0.0, 0.0, 0.0, 0.0]
[-1.0, 1.833, -1.0, 0.166]
[4.0, -4.333, 1.5, -0.166]
[-6.0, 9.5, -4.0, 0.5]
[4.0, -7.0, 3.5, -0.5]
Coefficients are in ascending order, so the first polynomial above is actually
Let’s try evaluating all of these polynomials at
A results at x=1
0
1
0
0
0
0
B results at x=1
0
1
0
0
0
0
C results at x=1
0
0
0
1
0
0
And lo and behold, what we have here is exactly the same as the set of three vectors for the first logic gate that we created above.
Now what’s the point of this crazy transformation? The answer is that instead of checking the constraints in the R1CS individually, we can now check all of the constraints at the same time by doing the dot product check on the polynomials.
Because in this case the dot product check is a series of additions and multiplications of polynomials, the result is itself going to be a polynomial. If the resulting polynomial, evaluated at every
Note that the resulting polynomial does not itself have to be zero, and in fact in most cases won’t be; it could have any behavior at the points that don’t correspond to any logic gates, as long as the result is zero at all the points that do correspond to some gate. To check correctness, we don’t actually evaluate the polynomial
Now, let’s actually do the dot product check with the polynomials above. First, the intermediate polynomials:
A . s = [43.0, -73.333, 38.5, -5.166]
B . s = [-3.0, 10.333, -5.0, 0.666]
C . s = [-41.0, 71.666, -24.5, 2.833]
Now,
t = [-88.0, 592.666, -1063.777, 805.833, -294.777, 51.5, -3.444]
Now, the minimal polynomial
Z = [24, -50, 35, -10, 1]
And if we divide the result above by
h = t / Z = [-3.666, 17.055, -3.444]
With no remainder.
And so we have the solution for the QAP. If we try to falsify any of the variables in the R1CS solution that we are deriving this QAP solution from — say, set the last one to
Note that the above is a simplification; “in the real world”, the addition, multiplication, subtraction and division will happen not with regular numbers, but rather with finite field elements — a spooky kind of arithmetic which is self-consistent, so all the algebraic laws we know and love still hold true, but where all answers are elements of some finite-sized set, usually integers within the range from
Special thanks to Eran Tromer for helping to explain many details about the inner workings of zk-SNARKs to me.