WARNING: This is a toy implementation with many pitfalls and bugs and is NOT intented to be securely deployed, do ABSOLUTELY NOT use it in any production setting, you've been warned! For example, this implementation keeps around very sensitive information during trusted setup or proof generation. The goal is to learn how the different proofs system work.

Playsnark: a playground to learn proofs systems

The goal of this code is to learn different proofs systems from the ground up. It is written in a very explanatory way with lots of comments explaining equations. It is NOT meant to be performant (at least yet!). It contains full arithmetization step with R1CS and QAP and the output can be plugged into multiple proof systems. The code is tested at each of these levels and to highlight what is the satisfying "equation" that the prover is trying to prove.

Currently two proofs systems exists:

• The original Pinocchio proof system (called PHGR13 in the code and litterature) kinda of the first practical proof systems that made it out there.
• Groth16 paper which is what is deployed in most zkSNARK application nowadays.

R1CS

The code in r1cs.go shows how to translate any function into R1CS format including the different variables and gates.
For example, to construct a circuit for the equation x^3 + x + 5 = 35, you need to decompose the operation with addition and multiplication gates.

c := NewR1CS()
c.NewInput("x")
c.NewOutput("out")
// u = x * x
c.NewVar("u")
// v = u * x
c.NewVar("v")
// w = v + x
c.NewVar("w")

// u = x * x
c.Mul("x", "x", "u")
// v = u * x
c.Mul("u", "x", "v")
// w = v + x
c.Add("v", "x", "w")
// out = w + 5
c.AddConst("w", 5, "out")

Then you can construct the solution vector, giving one value to each variable, as the following, where r is the R1CS struct. The intermediate values are the one constructed when first giving the value 3 to the variable x. Note: in R1CS, we have the first variable as being the variable "const" which just takes the value 1, this is useful when doing addition. Then we have the input variables ("x") and then the output variables ("out"), then the intermediate variables ("v","w","y").

var solution = make(Vector, len(r.vars))
solution[r.vars.IndexOf("const")] = 1
solution[r.vars.IndexOf("x")] = 3
solution[r.vars.IndexOf("out")] = 35
// v = x * x = 3 * 3
solution[r.vars.IndexOf("u")] = 9
// v = u * x = 9 * 3
solution[r.vars.IndexOf("v")] = 27
// w = v + x = 27 + 3
solution[r.vars.IndexOf("w")] = 30

Quadratic Arithmetic Programs (QAP)

Now that we got the R1CS part, we need to translate it to equations involving polynomials. To do so, we create one polynomial for each variable, which evaluates to the value of the variable for each gate, with one polynomial for the left input, the right input and the output of each gate. For example the fourth polynomial (representing "u") for the output of the gate 1 evaluates to 1 because "u = x * x", so u is the output.

You can create the QAP from the R1CS as following:

r1cs := createR1CS()
qap := ToQAP(r1cs)

and verify if the QAP is formed correctly by giving a witness to the problem and see if the QAP equation resolves (see the qap.go for more info):

s := createWitness(r1cs)
require.True(t, qap.IsValid(s))

Proofs systems

Pinochio

Trusted Setup

Thr Pinocchio proof system which requires a trusted setup for the prover and verifier. It enables the prover to blindly evaluates the polynomials of the QAP above, where blindly means it evaluates them at a unknown point s.

You can simply generate a trusted setup for the current circuit like so:

r1cs := createR1CS()
qap := ToQAP(r1cs)
setup := NewPHGR13TrustedSetup(qap)

The trusted setup has two parts, the evaluation key required by the prover to evaluate its circuit with its witness and produce a valid proof, and the verification key that is required from the verifier to verify a proof. Note that this implementation keeps other materials that we call "toxic waste" that should not be kept around after the trusted setup, but for the sake of comprehension and testing, we keep it. For example, using the toxic waste, you could generate a malicious proof passing the verification routine but does not guarantee that the prover knows a witness to the circuit.

type TrustedSetup struct {
	EK EvalKey         // required by the prover
	VK VerificationKey // required by the verifier
	t  ToxicWaste      // to be deleted - left for testing
}

Generating Proof

The prover then needs the evaluation key, the QAP polynomials and the solution vector:

r1cs := createR1CS()
s := createWitness(r1cs)
qap := ToQAP(r1cs)
setup := NewPHGR13TrustedSetup(qap)
proof := PHGR13Prove(setup.EK, qap, s)

Verifiying proof

The verifier then runs three basic check with the proof, the verification key of the trusted setup and the QAP, which are all explained in depth in pinocchio.go:PHGR13Verify():

• Division check: looks if the QAP equation resolves "in the exponent"
• Correct polynomial check: We check that the prover correctly used the polynomials of the QAP, the ones that were blindly evaluated in CRS individually.
• Linear combination check: We check that the prover used the same value for the variables for the three polynomials

You can do so as the following:

r1cs := createR1CS()
s := createWitness(r1cs)
qap := ToQAP(r1cs)
diff := qap.nbVars - qap.nbIO
setup := NewPHGR13TrustedSetup(qap)
proof := PHGR13Prove(setup.EK, qap, s)
fmt.Println(PHGR13Verify(setup.VK, qap, proof, s[:diff]))

Note the diff variable is just because in this test we have access to everything. In reality, the verifier only needs the values of the input / outputs so we restrict the solution vector to these variable when giving it to the verifier.

Groth16

Groth16 is an improvement to PHGR13 that brings smaller trusted setup, faster proving time and faster verification time as well as smaller proof. API is drastically similar except I haven't separated the trusted setup part into two as with PHGR13. The implementation is the straightforward implementation from the paper:

r1cs := createR1CS()
s := createWitness(r1cs)
qap := ToQAP(r1cs)
diff := qap.nbVars - qap.nbIO
setup := NewGroth16TrustedSetup(qap)
proof := Groth16Prove(setup, qap, s)
fmt.Println(Groth16Verify(setup, qap, proof, s[:diff]))

Resources

Well the first one I used is the series of Vitalik blog post, then I looked at this more technical small paper and finally to implement correctly the Pinocchio proof system I used the original paper as well as the paper derived after that succintly describes the algorithm using an asymmetric pairing from Ben-Sasson, Chiesa, Tromer and Virza.