From b379981087e3a6e1cc988bae01b19edbd09c255a Mon Sep 17 00:00:00 2001 From: arnaucube Date: Sat, 11 May 2019 23:06:02 +0200 Subject: [PATCH] add circuit compiler equals(a, b) syntax, complete flow working well (from compiler to verification) --- README.md | 6 +- circuitcompiler/parser.go | 62 +++++++++++++-------- snark_test.go | 113 +++++++++++++++++++++++++++----------- 3 files changed, 123 insertions(+), 58 deletions(-) diff --git a/README.md b/README.md index 86e573f..354c59a 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ zkSNARK library implementation in Go - `Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture`, Eli Ben-Sasson, Alessandro Chiesa, Eran Tromer, Madars Virza https://eprint.iacr.org/2013/879.pdf - `Pinocchio: Nearly practical verifiable computation`, Bryan Parno, Craig Gentry, Jon Howell, Mariana Raykova https://eprint.iacr.org/2013/279.pdf -## Caution, Warning, etc +## Caution, Warning Implementation of the zkSNARK [Pinocchio protocol](https://eprint.iacr.org/2013/279.pdf) from scratch in Go to understand the concepts. Do not use in production. Not finished, implementing this in my free time to understand it better, so I don't have much time. @@ -15,17 +15,15 @@ Current implementation status: - [x] Finite Fields (1, 2, 6, 12) operations - [x] G1 and G2 curve operations - [x] BN128 Pairing -- [ ] circuit code compiler +- [x] circuit code compiler - [ ] code to flat code (improve circuit compiler) - [x] flat code compiler - - [ ] private & public inputs. fix circuit compiler - [x] circuit to R1CS - [x] polynomial operations - [x] R1CS to QAP - [x] generate trusted setup - [x] generate proofs - [x] verify proofs with BN128 pairing - - [ ] fix 4th pairing proofs generation & verification: ê(Vkx+piA, piB) == ê(piH, Vkz) * ê(piC, G2) - [ ] move witness calculation outside the setup phase - [ ] Groth16 - [ ] multiple optimizations diff --git a/circuitcompiler/parser.go b/circuitcompiler/parser.go index 51c9a20..d168669 100644 --- a/circuitcompiler/parser.go +++ b/circuitcompiler/parser.go @@ -103,6 +103,8 @@ func (p *Parser) parseLine() (*Constraint, error) { params := strings.Split(varsString, ",") fmt.Println("params", params) // TODO + c.V1 = params[0] + c.V2 = params[1] return c, nil } // if c.Literal == "out" { @@ -163,21 +165,24 @@ func (p *Parser) Parse() (*Circuit, error) { fmt.Println(constraint) if constraint.Literal == "func" { // one constraint for each input - for _, in := range constraint.PrivateInputs { + for _, in := range constraint.PublicInputs { newConstr := &Constraint{ Op: "in", Out: in, } circuit.Constraints = append(circuit.Constraints, *newConstr) nInputs++ + circuit.Signals = addToArrayIfNotExist(circuit.Signals, in) + circuit.NPublic++ } - for _, in := range constraint.PublicInputs { + for _, in := range constraint.PrivateInputs { newConstr := &Constraint{ Op: "in", Out: in, } circuit.Constraints = append(circuit.Constraints, *newConstr) nInputs++ + circuit.Signals = addToArrayIfNotExist(circuit.Signals, in) } circuit.PublicInputs = constraint.PublicInputs circuit.PrivateInputs = constraint.PrivateInputs @@ -186,6 +191,22 @@ func (p *Parser) Parse() (*Circuit, error) { if constraint.Literal == "equals" { // TODO fmt.Println("circuit.Signals", circuit.Signals) + constr1 := &Constraint{ + Op: "*", + V1: constraint.V2, + V2: "1", + Out: constraint.V1, + Literal: "equals(" + constraint.V1 + ", " + constraint.V2 + "): " + constraint.V1 + "==" + constraint.V2 + " * 1", + } + circuit.Constraints = append(circuit.Constraints, *constr1) + constr2 := &Constraint{ + Op: "*", + V1: constraint.V1, + V2: "1", + Out: constraint.V2, + Literal: "equals(" + constraint.V1 + ", " + constraint.V2 + "): " + constraint.V2 + "==" + constraint.V1 + " * 1", + } + circuit.Constraints = append(circuit.Constraints, *constr2) continue } circuit.Constraints = append(circuit.Constraints, *constraint) @@ -197,31 +218,26 @@ func (p *Parser) Parse() (*Circuit, error) { if !isVal { circuit.Signals = addToArrayIfNotExist(circuit.Signals, constraint.V2) } - // fmt.Println("---") - // fmt.Println(circuit.PublicInputs[0]) - // fmt.Println(constraint.Out) - // fmt.Println(constraint.Out == circuit.PublicInputs[0]) - // fmt.Println("---") // if constraint.Out == "out" { // if Out is "out", put it after first value (one) and before the inputs // if constraint.Out == circuit.PublicInputs[0] { - if existInArray(circuit.PublicInputs, constraint.Out) { - // if Out is a public signal, put it after first value (one) and before the private inputs - if !existInArray(circuit.Signals, constraint.Out) { - // if already don't exists in signal array - signalsCopy := copyArray(circuit.Signals) - var auxSignals []string - auxSignals = append(auxSignals, signalsCopy[0]) - auxSignals = append(auxSignals, constraint.Out) - auxSignals = append(auxSignals, signalsCopy[1:]...) - circuit.Signals = auxSignals - // circuit.PublicInputs = append(circuit.PublicInputs, constraint.Out) - circuit.NPublic++ - } - } else { - circuit.Signals = addToArrayIfNotExist(circuit.Signals, constraint.Out) - } + // if existInArray(circuit.PublicInputs, constraint.Out) { + // // if Out is a public signal, put it after first value (one) and before the private inputs + // if !existInArray(circuit.Signals, constraint.Out) { + // // if already don't exists in signal array + // signalsCopy := copyArray(circuit.Signals) + // var auxSignals []string + // auxSignals = append(auxSignals, signalsCopy[0]) + // auxSignals = append(auxSignals, constraint.Out) + // auxSignals = append(auxSignals, signalsCopy[1:]...) + // circuit.Signals = auxSignals + // // circuit.PublicInputs = append(circuit.PublicInputs, constraint.Out) + // circuit.NPublic++ + // } + // } else { + circuit.Signals = addToArrayIfNotExist(circuit.Signals, constraint.Out) + // } } circuit.NVars = len(circuit.Signals) circuit.NSignals = len(circuit.Signals) diff --git a/snark_test.go b/snark_test.go index d416bfe..147cf96 100644 --- a/snark_test.go +++ b/snark_test.go @@ -25,8 +25,7 @@ func TestZkFromFlatCircuitCode(t *testing.T) { s3 = s2 * s0 s4 = s3 + s0 s5 = s4 + 5 - s1 = s5 * 1 - s5 = s1 * 1 + equals(s1, s5) out = 1 * 1 ` fmt.Print("\nflat code of the circuit:") @@ -127,6 +126,7 @@ func TestZkFromFlatCircuitCode(t *testing.T) { // fmt.Println(proof) // fmt.Println("public signals:", proof.PublicSignals) + fmt.Println("\n", circuit.Signals) fmt.Println("\nwitness", w) b35Verif := big.NewInt(int64(35)) publicSignalsVerif := []*big.Int{b35Verif} @@ -140,31 +140,38 @@ func TestZkFromFlatCircuitCode(t *testing.T) { assert.True(t, !VerifyProof(*circuit, setup, proof, wrongPublicSignalsVerif, true)) } -/* func TestZkMultiplication(t *testing.T) { - - // compile circuit and get the R1CS flatCode := ` - func test(a, b): - out = a * b + func test(private a, private b, public c): + d = a * b + equals(c, d) + out = 1 * 1 ` + fmt.Print("\nflat code of the circuit:") + fmt.Println(flatCode) // parse the code parser := circuitcompiler.NewParser(strings.NewReader(flatCode)) circuit, err := parser.Parse() assert.Nil(t, err) + fmt.Println("\ncircuit data:", circuit) + circuitJson, _ := json.Marshal(circuit) + fmt.Println("circuit:", string(circuitJson)) b3 := big.NewInt(int64(3)) b4 := big.NewInt(int64(4)) - inputs := []*big.Int{b3, b4} + privateInputs := []*big.Int{b3, b4} + b12 := big.NewInt(int64(12)) + publicSignals := []*big.Int{b12} + // wittness - w, err := circuit.CalculateWitness(inputs) + w, err := circuit.CalculateWitness(privateInputs, publicSignals) assert.Nil(t, err) - - fmt.Println("circuit") - fmt.Println(circuit.NPublic) + fmt.Println("\n", circuit.Signals) + fmt.Println("witness", w) // flat code to R1CS + fmt.Println("\ngenerating R1CS from flat code") a, b, c := circuit.GenerateR1CS() fmt.Println("\nR1CS:") fmt.Println("a:", a) @@ -172,43 +179,87 @@ func TestZkMultiplication(t *testing.T) { fmt.Println("c:", c) // R1CS to QAP - alphas, betas, gammas, zx := Utils.PF.R1CSToQAP(a, b, c) + // TODO zxQAP is not used and is an old impl, bad calculated. TODO remove + alphas, betas, gammas, zxQAP := Utils.PF.R1CSToQAP(a, b, c) fmt.Println("qap") - fmt.Println("alphas", alphas) - fmt.Println("betas", betas) - fmt.Println("gammas", gammas) + fmt.Println("alphas", len(alphas)) + fmt.Println("alphas[1]", alphas[1]) + fmt.Println("betas", len(betas)) + fmt.Println("gammas", len(gammas)) + fmt.Println("zx length", len(zxQAP)) + assert.True(t, !bytes.Equal(alphas[1][1].Bytes(), big.NewInt(int64(0)).Bytes())) ax, bx, cx, px := Utils.PF.CombinePolynomials(w, alphas, betas, gammas) + fmt.Println("ax length", len(ax)) + fmt.Println("bx length", len(bx)) + fmt.Println("cx length", len(cx)) + fmt.Println("px length", len(px)) + fmt.Println("px[last]", px[0]) - hx := Utils.PF.DivisorPolynomial(px, zx) + hxQAP := Utils.PF.DivisorPolynomial(px, zxQAP) + fmt.Println("hx length", len(hxQAP)) // hx==px/zx so px==hx*zx - assert.Equal(t, px, Utils.PF.Mul(hx, zx)) + assert.Equal(t, px, Utils.PF.Mul(hxQAP, zxQAP)) // p(x) = a(x) * b(x) - c(x) == h(x) * z(x) abc := Utils.PF.Sub(Utils.PF.Mul(ax, bx), cx) assert.Equal(t, abc, px) - hz := Utils.PF.Mul(hx, zx) - assert.Equal(t, abc, hz) + hzQAP := Utils.PF.Mul(hxQAP, zxQAP) + assert.Equal(t, abc, hzQAP) - div, rem := Utils.PF.Div(px, zx) - assert.Equal(t, hx, div) - assert.Equal(t, rem, r1csqap.ArrayOfBigZeros(1)) + div, rem := Utils.PF.Div(px, zxQAP) + assert.Equal(t, hxQAP, div) + assert.Equal(t, rem, r1csqap.ArrayOfBigZeros(4)) // calculate trusted setup - setup, err := GenerateTrustedSetup(len(w), *circuit, alphas, betas, gammas, zx) + setup, err := GenerateTrustedSetup(len(w), *circuit, alphas, betas, gammas) assert.Nil(t, err) + fmt.Println("\nt:", setup.Toxic.T) - // piA = g1 * A(t), piB = g2 * B(t), piC = g1 * C(t), piH = g1 * H(t) - proof, err := GenerateProofs(*circuit, setup, hx, w) + // zx and setup.Pk.Z should be the same (currently not, the correct one is the calculation used inside GenerateTrustedSetup function), the calculation is repeated. TODO avoid repeating calculation + // assert.Equal(t, zxQAP, setup.Pk.Z) + + fmt.Println("hx pk.z", hxQAP) + hx := Utils.PF.DivisorPolynomial(px, setup.Pk.Z) + fmt.Println("hx pk.z", hx) + // assert.Equal(t, hxQAP, hx) + div, rem = Utils.PF.Div(px, setup.Pk.Z) + assert.Equal(t, hx, div) + assert.Equal(t, rem, r1csqap.ArrayOfBigZeros(4)) + + assert.Equal(t, px, Utils.PF.Mul(hxQAP, zxQAP)) + // hx==px/zx so px==hx*zx + assert.Equal(t, px, Utils.PF.Mul(hx, setup.Pk.Z)) + + // check length of polynomials H(x) and Z(x) + assert.Equal(t, len(hx), len(px)-len(setup.Pk.Z)+1) + assert.Equal(t, len(hxQAP), len(px)-len(zxQAP)+1) + + // fmt.Println("pk.Z", len(setup.Pk.Z)) + // fmt.Println("zxQAP", len(zxQAP)) + + proof, err := GenerateProofs(*circuit, setup, w, px) assert.Nil(t, err) - // assert.True(t, VerifyProof(*circuit, setup, proof, false)) - b35 := big.NewInt(int64(35)) - publicSignals := []*big.Int{b35} - assert.True(t, VerifyProof(*circuit, setup, proof, publicSignals, true)) + // fmt.Println("\n proofs:") + // fmt.Println(proof) + + // fmt.Println("public signals:", proof.PublicSignals) + fmt.Println("\n", circuit.Signals) + fmt.Println("\nwitness", w) + b12Verif := big.NewInt(int64(12)) + publicSignalsVerif := []*big.Int{b12Verif} + before := time.Now() + assert.True(t, VerifyProof(*circuit, setup, proof, publicSignalsVerif, true)) + fmt.Println("verify proof time elapsed:", time.Since(before)) + + // check that with another public input the verification returns false + bOtherWrongPublic := big.NewInt(int64(11)) + wrongPublicSignalsVerif := []*big.Int{bOtherWrongPublic} + assert.True(t, !VerifyProof(*circuit, setup, proof, wrongPublicSignalsVerif, true)) } -*/ + /* func TestZkFromHardcodedR1CS(t *testing.T) { b0 := big.NewInt(int64(0))