Processing Fit for 2020, and Not the 1980s
Processing Fit for 2020, and Not the 1980s
Out With The Old, and In With The New: Building A New Computational Engine for our Digital World - zk-SNARKs, and R1CS
We live in a 1980s viewpoint of data processing, and have not really moved forward since then. This processing model often requires access to the original data, even when we just need proof of things. So let’s look to a future, where we preserve the privacy of users, and where we just ask them to prove that they still know things, or to prove that something is true or not, but not reveal the data which makes the attestation.
You never stop learning, so let’s dive into a world of privacy. At the core of this world is the concepts invovled with a method called zk-SNARKs, and which is a fast and efficient zero-knowledge proofs. Within it, Bob can determine that Alice has enough funds in her account to pay him, without actually revealing any of Alice’s transactions, or where Bob can prove to Alice that he still knows his password, without actually revealing it to her.
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 = 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 [here]:
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]
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]
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:
A_0 S x B_0 S - C_0 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!
We will show later — using Python numpy — that 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.
Coding and test
Here is the Golang code I have used [here]:
package main
import (
"fmt"
"math/big"
"strings"
"regexp"
"os"
"strconv"
"github.com/arnaucube/go-snark/circuitcompiler"
)
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
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])}
fmt.Printf("x (Private input): %d\n",x)
fmt.Printf("y (Public input): %d\n\n",y)
str=TrimSpaceNewlineInString(str)
fmt.Printf("Flat: %s\n",str)
parser := circuitcompiler.NewParser(strings.NewReader(str))
circuit, _ := parser.Parse()
fmt.Println("\nThe circuit is defined as:")
fmt.Println(circuit)
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("witness", w)
fmt.Println("\nR1CS from flat code")
a, b, c := circuit.GenerateR1CS()
fmt.Printf("a: %s\n\n",a)
fmt.Printf("b: %s\n\n",b)
fmt.Printf("c: %d\n\n",c)
}
For y=x³+x+5 and with a solution of x=3 for y=35, a sample run is [here]:
x (Private input): 3
y (Public input): 35
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
The circuit is defined as:
&{8 1 8 [s0] [s1] [one s1 s0 b0 s3 s4 s5 out] [] [{in s1 [] []} {in s0 [] []} {* s0 s0 b0 b0=s0*s0 [] []} {* s0 b0 s3 s3=s0*b0 [] []} {+ s3 s0 s4 s4=s3+s0 [] []} {+ s4 5 s5 s5=s4+5 [] []} {* s5 1 s1 equals(s1, s5): s1==s5 * 1 [] []} {* s1 1 s5 equals(s1, s5): s5==s1 * 1 [] []} {* 1 1 out 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]]
Proving with numpy
Unfortunately Go does not have numpy, so let’s use Python to prove that A.S x B.S — C.S=0. The code is:
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]))
Conclusions
We need to move away from our flawed 1970s view of computation, and move into a world where we prove things, without revealing the original data.
Security is not privacy!