Filling-in The Details of Vitalic’s Excellent zk-SNARKs Article For QAP Processing

Filling-in The Details of Vitalik’s Excellent zk-SNARKs Article For QAP Processing

The demo for R1CS and QAP is given here.

zk-SNARKs is used in blockchain and cryptography applications to provide zero-knowledge proofs — these are fairly easy to create and then are quick to check. We can use them to prove that Bob has enough cryptocurrency to pay Alice, without revealing any of the details of his transactions.

In 2017, Vitalik Buterin provided the classic explanation of zk-SNARKs here (2K claps on Medium):

You really have to read it. But, most people lose it in the translation from R1CS to QAP (Quadratic Arithmetic Program), as the examples make sense, but he skips over some of the details. So let’s go through the R1CS and QAP processes, and use a real-life example. I will use a finite field prime value of r=11, in order to keep our numbers small, but in real-life we would be using a large prime number. All of the values we will have will range from 0 to 10 (the finite field).

A core concept within zk-SNARKs is the usage of R1CS (Rank 1 Constraint System), and which supports an easily verifiable format for zero-knowledge proofs. In this case, we will use the practical example used by Vitalik Buterin to explain zk-SNARKs [here].

Initially, we start off with a proof that Bob knows the solution to a quadratic equation. Vitalik used this example:

x³+x+5==35

You can see that the solution to this is x=3. As he defined in his article, we start by simplifying our equation, so that it involves operations with either add, subtract, multiply and divide:

def qeval(x):
    y = x**3
    return x + y + 5

The next step is to flatten this in the form of a circuit, and where we get a series of statements which take the form of:

x=y(op)z

and where op and can be ‘+’, ‘-’, “*’ or “/”. This basically can be seen as creating a logical circuit, with AND (*), and OR (+) gates. As defined in Vitalik’s case we get:

sym_1 = x * x
y = sym_1 * x
sym_2 = y + x
~out = sym_2 + 5

This can be seen as having two AND gates (multipliers), and then two OR gates (adders). Next, we convert into the R1CS (Rank-1 Constrain System) format, and which defines three vectors: A, B and C. The solution to this is then a vector (S), and where:

S.A⋅S.B⋅S−C⋅S=[0]

In this case the “.’ is a dot product. So let’s look at the result of the processing of the quadratic equation we defined above:

R1CS from flat code
a: [[0 0 1 0 0 0 0 0] [0 0 1 0 0 0 0 0] [0 0 1 0 1 0 0 0] [5 0 0 0 0 1 0 0] [0 0 0 0 0 0 1 0] [0 1 0 0 0 0 0 0] [1 0 0 0 0 0 0 0]]
b: [[0 0 1 0 0 0 0 0] [0 0 0 1 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0]]
c: [[0 0 0 1 0 0 0 0] [0 0 0 0 1 0 0 0] [0 0 0 0 0 1 0 0] [0 0 0 0 0 0 1 0] [0 1 0 0 0 0 0 0] [0 0 0 0 0 0 1 0] [0 0 0 0 0 0 0 1]]

In this case the Witness (Bob) proves that he knows the solution by producing:

witness [1 35 3 9 27 30 35 1]

If we try for the A matrix and the dot product for the witness, we get:

[0 0 1 0 0 0 0 0] [1
[0 0 1 0 0 0 0 0] 35
[0 0 1 0 1 0 0 0] 3
[5 0 0 0 0 1 0 0] 9
[0 0 0 0 0 0 1 0] 27
[0 1 0 0 0 0 0 0] 30
[1 0 0 0 0 0 0 0] 35
                  1]

This gives:

0×1+0×35+1×3+0×9+0×27+0×30+0×35+0×1=3

And next for the B matrix:

[0 0 1 0 0 0 0 0] [1
[0 0 0 1 0 0 0 0] 35
[1 0 0 0 0 0 0 0] 3
[1 0 0 0 0 0 0 0] 9
[1 0 0 0 0 0 0 0] 27
[1 0 0 0 0 0 0 0] 30
[1 0 0 0 0 0 0 0] 35
                  1]

This gives:

0×1+0×35+1×3+0×9+0×27+0×30+0×35+0×1=3

And next for the C matrix:

[0 0 0 1 0 0 0 0] [1 
[0 0 0 0 1 0 0 0]  35
[0 0 0 0 0 1 0 0]  3
[0 0 0 0 0 0 1 0]  9
[0 1 0 0 0 0 0 0]  27
[0 0 0 0 0 0 1 0]  30
[0 0 0 0 0 0 0 1]  35
                   1]

This gives:

0×1+0×35+0×3+1×9+0×27+0×30+0×35+0×1=9

And now we can see that for A.B−C, for the first value, we get:

A0⋅S×B0⋅S−C0⋅S=3×3−9=0

And so Bob (the witness) has provided the correct first part of the proof. We can then got through the other seven values for each row of A, B and C, and find that the result will be zero. Bob has thus proven that he knows the solution of the quadratic equation!

In this case, A.S is [ 3, 3, 30, 35, 35, 35, 1], B.S is [3, 9, 1, 1, 1, 1, 1], and C.S is [ 9, 27, 30, 35, 35, 35, 1]. The result of A.S x B.S is [ 9, 27, 30, 35, 35, 35, 1], and is we subtract C.S we get: [0, 0, 0, 0, 0, 0, 0]. This proves that Bob knows the solution. In Python we can prove that A.S x B.S — C.S=0:

import numpy

a=[[0,0,1,0,0,0,0,0],[0,0,1,0,0,0,0,0],[0,0,1,0,1,0,0,0],[5,0,0,0,0,1,0,0],[0,0,0,0,0,0,1,0],[0,1,0,0,0,0,0,0],[1,0,0,0,0,0,0,0]]
b=[[0,0,1,0,0,0,0,0],[0,0,0,1,0,0,0,0],[1,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0]]
c=[[0,0,0,1,0,0,0,0],[0,0,0,0,1,0,0,0],[0,0,0,0,0,1,0,0],[0,0,0,0,0,0,1,0],[0,1,0,0,0,0,0,0],[0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,1]]
s=[1,35,3,9,27,30,35,1]
def multi(m, g):
    en = numpy.multiply(m, g)
    return en
def dot(m, g):
    en = numpy.dot(m, g)
    return en
def add(m, g):
    en = numpy.add(m, g)
    return en
def sub(m, g):
    en = numpy.subtract(m, g)
    return en
print "A:\n",a
print "B:\n",b
print "C:\n",c
print "S:\n",s

print "-----------"
res1=dot(a,s)
print ("A.S:",res1)
res2=dot(b,s)
print ("B.S:",res2)
res3=dot(c,s)
print ("C.S:",res3)
res4=multi(res1,res2)
print ("A.S x B.S:",res4)
res5=sub(res4,res3)
print ("A.S x B.S - C.S:",res5)

The result shows that we end up with [0,0,0,0,0,0,0]:

A:
[[0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 1, 0, 1, 0, 0, 0], [5, 0, 0, 0, 0, 1, 0, 0], [0, 0, 0, 0, 0, 0, 1, 0], [0, 1, 0, 0, 0, 0, 0, 0], [1, 0, 0, 0, 0, 0, 0, 0]]
B:
[[0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0], [1, 0, 0, 0, 0, 0, 0, 0], [1, 0, 0, 0, 0, 0, 0, 0], [1, 0, 0, 0, 0, 0, 0, 0], [1, 0, 0, 0, 0, 0, 0, 0], [1, 0, 0, 0, 0, 0, 0, 0]]
C:
[[0, 0, 0, 1, 0, 0, 0, 0], [0, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 1, 0, 0], [0, 0, 0, 0, 0, 0, 1, 0], [0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 1, 0], [0, 0, 0, 0, 0, 0, 0, 1]]
S:
[1, 35, 3, 9, 27, 30, 35, 1]
-----------
('A.S:', array([ 3,  3, 30, 35, 35, 35,  1]))
('B.S:', array([3, 9, 1, 1, 1, 1, 1]))
('C.S:', array([ 9, 27, 30, 35, 35, 35,  1]))
('A.S x B.S:', array([ 9, 27, 30, 35, 35, 35,  1]))
('A.S x B.S - C.S:', array([0, 0, 0, 0, 0, 0, 0]))

R1CS to QAP

Now let’s look at the part that Vitalik perhaps misses out a few details. His explanation is excellent, but it can be hard to follow the details around the QAP processing (from vectors to quadratic equations). Basically we end up with a number of x-points values of 1, 2, 3, … 8. For the first column of the A matrix we get x values of 1, 2, 3, … 8, and the resulting values of 0, 0, 0, 5, 0, 0, 1. The points we are mapping to a polynomial form is thus (1,0), (2,0), (3,0), (4,5), (5,0), (6,0) and (7,1). For QAP we must find a quadratic equation which moves through these points.

Let’s define a finite field of r=11 and look to how we convert from R1CS to QAP. This converts the vector form into a quadratic form. So let’s start with the result [here]:

A: [[0 0 1 0 0 0 0 0] [0 0 1 0 0 0 0 0] [0 0 1 0 1 0 0 0] [5 0 0 0 0 1 0 0] [0 0 0 0 0 0 1 0] [0 1 0 0 0 0 0 0] [1 0 0 0 0 0 0 0]]
B: [[0 0 1 0 0 0 0 0] [0 0 0 1 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0]]
C: [[0 0 0 1 0 0 0 0] [0 0 0 0 1 0 0 0] [0 0 0 0 0 1 0 0] [0 0 0 0 0 0 1 0] [0 1 0 0 0 0 0 0] [0 0 0 0 0 0 1 0] [0 0 0 0 0 0 0 1]]
As: [[2 0 5 7 3 5 0] [4 8 1 5 3 0 1] [10 10 10 2 3 8 2] [0 0 0 0 0 0 0] [2 8 8 6 4 2 3] [9 5 6 0 9 8 7] [10 2 8 8 5 8 3] [0 0 0 0 0 0 0]]
Bs: [[4 9 9 4 1 5 1] [0 0 0 0 0 0 0] [7 7 0 8 4 10 9] [1 6 2 10 6 7 1] [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]]
Cs: [[0 0 0 0 0 0 0] [10 2 8 8 5 8 3] [0 0 0 0 0 0 0] [7 7 0 8 4 10 9] [1 6 2 10 6 7 1] [2 8 8 6 4 2 3] [2 2 7 5 1 8 8] [1 8 8 7 2 9 9]]

Now A vector matrix is:

[0 0 1 0 0 0 0 0]
[0 0 1 0 0 0 0 0]
[0 0 1 0 1 0 0 0]
[5 0 0 0 0 1 0 0]
[0 0 0 0 0 0 1 0]
[0 1 0 0 0 0 0 0]
[1 0 0 0 0 0 0 0]

The result of processing this into polynomial form (As) is:

[2 0 5 7 3 5 0]
[4 8 1 5 3 0 1]
[10 10 10 2 3 8 2]
[0 0 0 0 0 0 0]
[2 8 8 6 4 2 3]
[9 5 6 0 9 8 7]
[10 2 8 8 5 8 3]
[0 0 0 0 0 0 0]

For the first column of the A vector matrix we have (1,0), (2,0), (3,0), (4,5), (5,0), (6,0), and (7,1), and which gives the polynomial of:

0x⁶+5x⁵+3x⁴+7x³+5x²+0x+2

In reverse this matches the first row of the polynomial matrix:

2+0x+5x²+7x³+3x⁴+5x⁵+0x⁶

If we try with the value of x=1 for this polynomial, we get y=0 (1,0). With x=2, we get y=0 (2,0). With x=3 ,we get y=0 (3,0). With x=4 ,we get y=5 (4,5), and so on.

Note all of the values are (mod 11), as we have set r=11.

You can check with this Python code:

for x in range (1,8):
 y=2+0*x + 5*(x**2) + 7*(x**3) + 3*(x**4) + 5*(x**5) + 0*(x**6)
 y= y % 11
 print x,y

We get:

1 0
2 0
3 0
4 5
5 0
6 0
7 1

For the second column of the A vector matrix we have (1,0), (2,0), (3,0), (4,0), (5,0), (6,1), (7,0), and which gives the polynomial of:

4+8x+1x²+5x³+3x⁴+0x⁵+1x⁶

If we run the following Python program:

for x in range (1,8):
 y=4+ 8*x+ 1*(x**2) + 5*(x**3) + 3*(x**4) + 0*(x**5)+ 1 * (x**6)
 y=y%11
 print x,y

We get:

1 0
2 0
3 0
4 0
5 0
6 1
7 0

For the second column of the A vector matrix we have (1,1), (2,1), (3,1), (4,0), (5,0), (6,1), (7,0), and which gives the polynomial of:

10+10x+10x²+2x³+3x⁴+8x⁵+2x⁶

If we run the following Python program:

for x in range (1,8):
        y=10+ 10*x+ 10*(x**2) + 2*(x**3) + 3*(x**4) + 8*(x**5)+ 2 * (x**6)
        y=y%11
        print x,y

We get:

1 1
2 1
3 1
4 0
5 0
6 0
7 0

Coding

The following is the Golang coding [here]:

package main 
import (
 "fmt"
 "math/big"
 "strings"
      "regexp"
 "os"
 "strconv"
 // snark "github.com/arnaucube/go-snark"
 "github.com/arnaucube/go-snark/circuitcompiler"
 "github.com/arnaucube/go-snark/fields"
 "github.com/arnaucube/go-snark/r1csqap"

)
func TrimSpaceNewlineInString(s string) string {
      re := regexp.MustCompile(`LF`)
      return re.ReplaceAllString(s, "\n")
}

func main() {
 str:="func exp3(private a):LF\tb = a * aLF\tc = a * bLF\treturn cLFLFfunc main(private s0, public s1):LF\ts3 = exp3(s0)LF\ts4 = s3 + s0LF\ts5 = s4 + 5LF\tequals(s1, s5)LF\tout = 1 * 1"
 x:=3
 y:=35
 rval:="11"
 argCount := len(os.Args[1:])
        if (argCount>0) {str= os.Args[1]}
        if (argCount>1) {x,_= strconv.Atoi(os.Args[2])}
        if (argCount>2) {y,_= strconv.Atoi(os.Args[3])}
        if (argCount>3) {rval= os.Args[4]}
 fmt.Printf("x (Private input): %d, y (Public input): %d\n",x,y)
 fmt.Printf("r (Prime): %s\n",rval)
 str=TrimSpaceNewlineInString(str)
 fmt.Printf("Flat: %s\n",str)
 parser := circuitcompiler.NewParser(strings.NewReader(str))
 circuit, _ := parser.Parse()

 val1 := big.NewInt(int64(x))
 privateVal := []*big.Int{val1}
 val2 := big.NewInt(int64(y))
 publicVal := []*big.Int{val2}
 // witness
 w, _ := circuit.CalculateWitness(privateVal, publicVal)
 fmt.Println("\nWitness: ", w)
 fmt.Println("\nR1CS from flat code")
 a, b, c := circuit.GenerateR1CS()
 fmt.Printf("a: %s\n",a)
 fmt.Printf("b: %s\n",b)
 fmt.Printf("c: %d\n\n",c)

 r, _ := new(big.Int).SetString(rval, 10)
  f:= fields.NewFq(r)
 // new Polynomial Field
 pf := r1csqap.NewPolynomialField(f)
 alphas, betas, gammas, _ := pf.R1CSToQAP(a, b, c)
 fmt.Printf("As: %d\n\n",alphas) 
 fmt.Printf("Bs: %d\n\n",betas) 
 fmt.Printf("Cs: %d\n\n",gammas) 
 _, _, _, px := pf.CombinePolynomials(w, alphas, betas, gammas)
 fmt.Printf("\nCombined: %d\n",px) 
}

For y=x³+x+5 for x=3 and y=35, and where x is the private value, and y is the public value. A sample run is [here]:

x (Private input): 3, y (Public input): 35
r (Prime): 11
Flat: func exp3(private a):
 b = a * a
 c = a * b
 return c
func main(private s0, public s1):
 s3 = exp3(s0)
 s4 = s3 + s0
 s5 = s4 + 5
 equals(s1, s5)
 out = 1 * 1
Witness:  [1 35 3 9 27 30 35 1]
R1CS from flat code
a: [[0 0 1 0 0 0 0 0] [0 0 1 0 0 0 0 0] [0 0 1 0 1 0 0 0] [5 0 0 0 0 1 0 0] [0 0 0 0 0 0 1 0] [0 1 0 0 0 0 0 0] [1 0 0 0 0 0 0 0]]
b: [[0 0 1 0 0 0 0 0] [0 0 0 1 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0] [1 0 0 0 0 0 0 0]]
c: [[0 0 0 1 0 0 0 0] [0 0 0 0 1 0 0 0] [0 0 0 0 0 1 0 0] [0 0 0 0 0 0 1 0] [0 1 0 0 0 0 0 0] [0 0 0 0 0 0 1 0] [0 0 0 0 0 0 0 1]]
As: [[2 0 5 7 3 5 0] [4 8 1 5 3 0 1] [10 10 10 2 3 8 2] [0 0 0 0 0 0 0] [2 8 8 6 4 2 3] [9 5 6 0 9 8 7] [10 2 8 8 5 8 3] [0 0 0 0 0 0 0]]
Bs: [[4 9 9 4 1 5 1] [0 0 0 0 0 0 0] [7 7 0 8 4 10 9] [1 6 2 10 6 7 1] [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]]
Cs: [[0 0 0 0 0 0 0] [10 2 8 8 5 8 3] [0 0 0 0 0 0 0] [7 7 0 8 4 10 9] [1 6 2 10 6 7 1] [2 8 8 6 4 2 3] [2 2 7 5 1 8 8] [1 8 8 7 2 9 9]]

Combined: [0 5 10 10 2 5 0 2 1 9 6 6 10]

Conclusions

Go read the zk-SNARKs article:

I have read it in so much detail, and is very well explained. If you are a bit confused about the R1C2 to QAP process, have a look at this real-life demo: