Merge pull request #5 from arnaucube/fix/circuitcompiler

Fix/circuitcompiler

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
+## 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,18 +15,18 @@ 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
 
 
 ## Usage

circuitcompiler/circuit.go

@@ -2,6 +2,7 @@ package circuitcompiler
 
 import (
 	"errors"
+	"fmt"
 	"math/big"
 	"strconv"
 
@@ -13,9 +14,9 @@ type Circuit struct {
 	NVars         int
 	NPublic       int
 	NSignals      int
-	Inputs        []string
+	PrivateInputs []string
+	PublicInputs  []string
 	Signals       []string
-	PublicSignals []string
 	Witness       []*big.Int
 	Constraints   []Constraint
 	R1CS          struct {
@@ -34,7 +35,8 @@ type Constraint struct {
 	Out     string
 	Literal string
 
-	Inputs []string // in func declaration case
+	PrivateInputs []string // in func declaration case
+	PublicInputs  []string // in func declaration case
 }
 
 func indexInArray(arr []string, e string) int {
@@ -95,11 +97,12 @@ func (circ *Circuit) GenerateR1CS() ([][]*big.Int, [][]*big.Int, [][]*big.Int) {
 
 		// if existInArray(constraint.Out) {
 		if used[constraint.Out] {
-			panic(errors.New("out variable already used: " + constraint.Out))
+			// panic(errors.New("out variable already used: " + constraint.Out))
+			fmt.Println("variable already used")
 		}
 		used[constraint.Out] = true
 		if constraint.Op == "in" {
-			for i := 0; i < len(constraint.Inputs); i++ {
+			for i := 0; i <= len(circ.PublicInputs); i++ {
 				aConstraint[indexInArray(circ.Signals, constraint.Out)] = new(big.Int).Add(aConstraint[indexInArray(circ.Signals, constraint.Out)], big.NewInt(int64(1)))
 				aConstraint, used = insertVar(aConstraint, circ.Signals, constraint.Out, used)
 				bConstraint[0] = big.NewInt(int64(1))
@@ -154,14 +157,23 @@ type Inputs struct {
 
 // CalculateWitness calculates the Witness of a Circuit based on the given inputs
 // witness = [ one, output, publicInputs, privateInputs, ...]
-func (circ *Circuit) CalculateWitness(inputs []*big.Int) ([]*big.Int, error) {
-	if len(inputs) != len(circ.Inputs) {
-		return []*big.Int{}, errors.New("given inputs != circuit.Inputs")
+func (circ *Circuit) CalculateWitness(privateInputs []*big.Int, publicInputs []*big.Int) ([]*big.Int, error) {
+	if len(privateInputs) != len(circ.PrivateInputs) {
+		return []*big.Int{}, errors.New("given privateInputs != circuit.PublicInputs")
+	}
+	if len(publicInputs) != len(circ.PublicInputs) {
+		return []*big.Int{}, errors.New("given publicInputs != circuit.PublicInputs")
 	}
 	w := r1csqap.ArrayOfBigZeros(len(circ.Signals))
 	w[0] = big.NewInt(int64(1))
-	for i, input := range inputs {
-		w[i+2] = input
+	for i, input := range publicInputs {
+		fmt.Println(i + 1)
+		fmt.Println(input)
+		w[i+1] = input
+	}
+	for i, input := range privateInputs {
+		fmt.Println(i + len(publicInputs) + 1)
+		w[i+len(publicInputs)+1] = input
 	}
 	for _, constraint := range circ.Constraints {
 		if constraint.Op == "in" {

circuitcompiler/circuit_test.go

@@ -1,6 +1,7 @@
 package circuitcompiler
 
 import (
+	"encoding/json"
 	"fmt"
 	"math/big"
 	"strings"
@@ -21,64 +22,77 @@ func TestCircuitParser(t *testing.T) {
 			m2 = m1 * s1
 			m3 = m2 + s1
 			out = m3 + 5
+
 	*/
 
-	// flat code
+	// flat code, where er is expected_result
+	// equals(s5, s1)
+	// s1 = s5 * 1
 	flat := `
-	func test(x):
-		aux = x*x
-		y = aux*x
-		z = x + y
-		out = z + 5
+	func test(private s0, public s1):
+		s2 = s0*s0
+		s3 = s2*s0
+		s4 = s0 + s3
+		s5 = s4 + 5
+		s5 = s1 * one
+		out = 1 * 1
 	`
 	parser := NewParser(strings.NewReader(flat))
 	circuit, err := parser.Parse()
 	assert.Nil(t, err)
-	fmt.Println(circuit)
+	fmt.Println("circuit parsed: ", circuit)
 
 	// flat code to R1CS
 	fmt.Println("generating R1CS from flat code")
 	a, b, c := circuit.GenerateR1CS()
-	fmt.Print("function with inputs: ")
-	fmt.Println(circuit.Inputs)
+	fmt.Println("private inputs: ", circuit.PrivateInputs)
+	fmt.Println("public inputs: ", circuit.PublicInputs)
 
-	fmt.Print("signals: ")
-	fmt.Println(circuit.Signals)
+	fmt.Println("signals:", circuit.Signals)
 
 	// expected result
-	b0 := big.NewInt(int64(0))
-	b1 := big.NewInt(int64(1))
-	b5 := big.NewInt(int64(5))
-	aExpected := [][]*big.Int{
-		[]*big.Int{b0, b0, b1, b0, b0, b0},
-		[]*big.Int{b0, b0, b0, b1, b0, b0},
-		[]*big.Int{b0, b0, b1, b0, b1, b0},
-		[]*big.Int{b5, b0, b0, b0, b0, b1},
-	}
-	bExpected := [][]*big.Int{
-		[]*big.Int{b0, b0, b1, b0, b0, b0},
-		[]*big.Int{b0, b0, b1, b0, b0, b0},
-		[]*big.Int{b1, b0, b0, b0, b0, b0},
-		[]*big.Int{b1, b0, b0, b0, b0, b0},
-	}
-	cExpected := [][]*big.Int{
-		[]*big.Int{b0, b0, b0, b1, b0, b0},
-		[]*big.Int{b0, b0, b0, b0, b1, b0},
-		[]*big.Int{b0, b0, b0, b0, b0, b1},
-		[]*big.Int{b0, b1, b0, b0, b0, b0},
-	}
-
-	assert.Equal(t, aExpected, a)
-	assert.Equal(t, bExpected, b)
-	assert.Equal(t, cExpected, c)
+	// b0 := big.NewInt(int64(0))
+	// b1 := big.NewInt(int64(1))
+	// b5 := big.NewInt(int64(5))
+	// aExpected := [][]*big.Int{
+	//         []*big.Int{b0, b0, b1, b0, b0, b0},
+	//         []*big.Int{b0, b0, b0, b1, b0, b0},
+	//         []*big.Int{b0, b0, b1, b0, b1, b0},
+	//         []*big.Int{b5, b0, b0, b0, b0, b1},
+	// }
+	// bExpected := [][]*big.Int{
+	//         []*big.Int{b0, b0, b1, b0, b0, b0},
+	//         []*big.Int{b0, b0, b1, b0, b0, b0},
+	//         []*big.Int{b1, b0, b0, b0, b0, b0},
+	//         []*big.Int{b1, b0, b0, b0, b0, b0},
+	// }
+	// cExpected := [][]*big.Int{
+	//         []*big.Int{b0, b0, b0, b1, b0, b0},
+	//         []*big.Int{b0, b0, b0, b0, b1, b0},
+	//         []*big.Int{b0, b0, b0, b0, b0, b1},
+	//         []*big.Int{b0, b1, b0, b0, b0, b0},
+	// }
+	//
+	// assert.Equal(t, aExpected, a)
+	// assert.Equal(t, bExpected, b)
+	// assert.Equal(t, cExpected, c)
 	fmt.Println(a)
 	fmt.Println(b)
 	fmt.Println(c)
 
 	b3 := big.NewInt(int64(3))
-	inputs := []*big.Int{b3}
+	privateInputs := []*big.Int{b3}
+	b35 := big.NewInt(int64(35))
+	publicInputs := []*big.Int{b35}
 	// Calculate Witness
-	w, err := circuit.CalculateWitness(inputs)
+	w, err := circuit.CalculateWitness(privateInputs, publicInputs)
 	assert.Nil(t, err)
 	fmt.Println("w", w)
+
+	circuitJson, _ := json.Marshal(circuit)
+	fmt.Println("circuit:", string(circuitJson))
+
+	assert.Equal(t, circuit.NPublic, 1)
+	assert.Equal(t, len(circuit.PublicInputs), 1)
+	assert.Equal(t, len(circuit.PrivateInputs), 1)
 }

circuitcompiler/parser.go

@@ -2,7 +2,9 @@ package circuitcompiler
 
 import (
 	"errors"
+	"fmt"
 	"io"
+	"os"
 	"regexp"
 	"strings"
 )
@@ -70,9 +72,45 @@ func (p *Parser) parseLine() (*Constraint, error) {
 		rgx := regexp.MustCompile(`\((.*?)\)`)
 		insideParenthesis := rgx.FindStringSubmatch(line)
 		varsString := strings.Replace(insideParenthesis[1], " ", "", -1)
-		c.Inputs = strings.Split(varsString, ",")
+		allInputs := strings.Split(varsString, ",")
+
+		// from allInputs, get the private and the public separated
+		for _, in := range allInputs {
+			if strings.Contains(in, "private") {
+				input := strings.Replace(in, "private", "", -1)
+				c.PrivateInputs = append(c.PrivateInputs, input)
+			} else if strings.Contains(in, "public") {
+				input := strings.Replace(in, "public", "", -1)
+				c.PublicInputs = append(c.PublicInputs, input)
+			} else {
+				// TODO give more info about the circuit code error
+				fmt.Println("error on declaration of public and private inputs")
+				os.Exit(0)
+			}
+		}
+		return c, nil
+	}
+	if c.Literal == "equals" {
+		// format: `equals(a, b)`
+		line, err := p.s.r.ReadString(')')
+		if err != nil {
+			return c, err
+		}
+		// read string inside ( )
+		rgx := regexp.MustCompile(`\((.*?)\)`)
+		insideParenthesis := rgx.FindStringSubmatch(line)
+		varsString := strings.Replace(insideParenthesis[1], " ", "", -1)
+		params := strings.Split(varsString, ",")
+		fmt.Println("params", params)
+		// TODO
+		c.V1 = params[0]
+		c.V2 = params[1]
 		return c, nil
 	}
+	// if c.Literal == "out" {
+	//         // TODO
+	//         return c, nil
+	// }
 
 	_, lit = p.scanIgnoreWhitespace() // skip =
 	c.Literal += lit
@@ -124,17 +162,51 @@ func (p *Parser) Parse() (*Circuit, error) {
 		if err != nil {
 			break
 		}
+		fmt.Println(constraint)
 		if constraint.Literal == "func" {
 			// one constraint for each input
-			for _, in := range constraint.Inputs {
+			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.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
+			continue
+		}
+		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.Inputs = constraint.Inputs
+			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)
@@ -146,21 +218,26 @@ func (p *Parser) Parse() (*Circuit, error) {
 		if !isVal {
 			circuit.Signals = addToArrayIfNotExist(circuit.Signals, constraint.V2)
 		}
-		if constraint.Out == "out" {
-			// if Out is "out", put it after first value (one) and before the inputs
-			if !existInArray(circuit.Signals, constraint.Out) {
-				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.PublicSignals = append(circuit.PublicSignals, constraint.Out)
-				circuit.NPublic++
-			}
-		} else {
-			circuit.Signals = addToArrayIfNotExist(circuit.Signals, constraint.Out)
-		}
+
+		// 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)
+		// }
 	}
 	circuit.NVars = len(circuit.Signals)
 	circuit.NSignals = len(circuit.Signals)

snark.go

@@ -1,7 +1,6 @@
 package snark
 
 import (
-	"bytes"
 	"fmt"
 	"math/big"
 	"os"
@@ -96,15 +95,15 @@ func GenerateTrustedSetup(witnessLength int, circuit circuitcompiler.Circuit, al
 	var err error
 
 	// input soundness
-	for i := 0; i < len(alphas); i++ {
-		for j := 0; j < len(alphas[i]); j++ {
-			if j <= circuit.NPublic {
-				if bytes.Equal(alphas[i][j].Bytes(), Utils.FqR.Zero().Bytes()) {
-					alphas[i][j] = Utils.FqR.One()
-				}
-			}
-		}
-	}
+	// for i := 0; i < len(alphas); i++ {
+	//         for j := 0; j < len(alphas[i]); j++ {
+	//                 if j <= circuit.NPublic {
+	//                         if bytes.Equal(alphas[i][j].Bytes(), Utils.FqR.Zero().Bytes()) {
+	//                                 alphas[i][j] = Utils.FqR.One()
+	//                         }
+	//                 }
+	//         }
+	// }
 
 	fmt.Println("alphas[1]", alphas[1])
 
@@ -217,7 +216,8 @@ func GenerateTrustedSetup(witnessLength int, circuit circuitcompiler.Circuit, al
 
 	// z pol
 	zpol := []*big.Int{big.NewInt(int64(1))}
-	for i := 1; i < len(circuit.Constraints); i++ {
+	// for i := 0; i < len(circuit.Constraints); i++ {
+	for i := 1; i < len(alphas)-1; i++ {
 		zpol = Utils.PF.Mul(
 			zpol,
 			[]*big.Int{

snark_test.go

@@ -1,6 +1,7 @@
 package snark
 
 import (
+	"bytes"
 	"encoding/json"
 	"fmt"
 	"math/big"
@@ -14,14 +15,18 @@ import (
 )
 
 func TestZkFromFlatCircuitCode(t *testing.T) {
-
 	// compile circuit and get the R1CS
+
+	// circuit function
+	// y = x^3 + x + 5
 	flatCode := `
-	func test(x):
-		aux = x*x
-		y = aux*x
-		z = x + y
-		out = z + 5
+	func test(private s0, public s1):
+		s2 = s0 * s0
+		s3 = s2 * s0
+		s4 = s3 + s0
+		s5 = s4 + 5
+		equals(s1, s5)
+		out = 1 * 1
 	`
 	fmt.Print("\nflat code of the circuit:")
 	fmt.Println(flatCode)
@@ -36,10 +41,14 @@ func TestZkFromFlatCircuitCode(t *testing.T) {
 
 	b3 := big.NewInt(int64(3))
 	privateInputs := []*big.Int{b3}
+	b35 := big.NewInt(int64(35))
+	publicSignals := []*big.Int{b35}
+
 	// wittness
-	w, err := circuit.CalculateWitness(privateInputs)
+	w, err := circuit.CalculateWitness(privateInputs, publicSignals)
 	assert.Nil(t, err)
-	fmt.Println("\nwitness", w)
+	fmt.Println("\n", circuit.Signals)
+	fmt.Println("witness", w)
 
 	// flat code to R1CS
 	fmt.Println("\ngenerating R1CS from flat code")
@@ -58,6 +67,7 @@ func TestZkFromFlatCircuitCode(t *testing.T) {
 	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))
@@ -65,9 +75,6 @@ func TestZkFromFlatCircuitCode(t *testing.T) {
 	fmt.Println("cx length", len(cx))
 	fmt.Println("px length", len(px))
 	fmt.Println("px[last]", px[0])
-	px0 := Utils.PF.F.Add(px[0], big.NewInt(int64(88)))
-	fmt.Println(px0)
-	assert.Equal(t, px0.Bytes(), Utils.PF.F.Zero().Bytes())
 
 	hxQAP := Utils.PF.DivisorPolynomial(px, zxQAP)
 	fmt.Println("hx length", len(hxQAP))
@@ -83,7 +90,7 @@ func TestZkFromFlatCircuitCode(t *testing.T) {
 
 	div, rem := Utils.PF.Div(px, zxQAP)
 	assert.Equal(t, hxQAP, div)
-	assert.Equal(t, rem, r1csqap.ArrayOfBigZeros(4))
+	assert.Equal(t, rem, r1csqap.ArrayOfBigZeros(6))
 
 	// calculate trusted setup
 	setup, err := GenerateTrustedSetup(len(w), *circuit, alphas, betas, gammas)
@@ -97,6 +104,9 @@ func TestZkFromFlatCircuitCode(t *testing.T) {
 	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(6))
 
 	assert.Equal(t, px, Utils.PF.Mul(hxQAP, zxQAP))
 	// hx==px/zx so px==hx*zx
@@ -116,41 +126,52 @@ func TestZkFromFlatCircuitCode(t *testing.T) {
 	// fmt.Println(proof)
 
 	// fmt.Println("public signals:", proof.PublicSignals)
+	fmt.Println("\n", circuit.Signals)
 	fmt.Println("\nwitness", w)
-	// b1 := big.NewInt(int64(1))
-	b35 := big.NewInt(int64(35))
-	// publicSignals := []*big.Int{b1, b35}
-	publicSignals := []*big.Int{b35}
+	b35Verif := big.NewInt(int64(35))
+	publicSignalsVerif := []*big.Int{b35Verif}
 	before := time.Now()
-	assert.True(t, VerifyProof(*circuit, setup, proof, publicSignals, true))
+	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(34))
+	wrongPublicSignalsVerif := []*big.Int{bOtherWrongPublic}
+	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)
@@ -158,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))