feat: verify commitments in groth16 recursion verifier (#1057)

* feat: verify commitments in groth16 recursion verifier fix: emulated MarshalG1 for BN254 * update gnark-crypto version * fix: follow infinity point encoding from gnark-crypto * refactor: embed G1/G2 checks in Pairing interface * chore: add no-op G1/G2 checks for bls24315 for implementing intf * chore: update gnark-crypto dependency * refactor: init curve and pairing in G16 verifier * refactor: Pedersen commitment scheme into package * chore: remove precomputed vk option * refactor: use pedersen init * feat: add complete arithm option * refactor: implicit indexing * chore: simplify writing to hash * feat: restore aux data for folding commitment * refactor: use static hash inside circuit * test: use only test engine for recursion tests * test: remove unused circuit * test: remove unused circuit * test: add all commitment tests * docs: update example to use prover/verifier opts * chore: remove prover check option in favor of tags * feat: add option for subgroup checks --------- Co-authored-by: Ivo Kubjas <[email protected]>
Consensys · Feb 19, 2024 · 45d201a · 45d201a
1 parent 1cc2d6a
commit 45d201a
Show file tree

Hide file tree

Showing 18 changed files with 887 additions and 268 deletions.
diff --git a/go.mod b/go.mod
@@ -7,7 +7,7 @@ require (
 	github.com/blang/semver/v4 v4.0.0
 	github.com/consensys/bavard v0.1.13
 	github.com/consensys/compress v0.2.3
-	github.com/consensys/gnark-crypto v0.12.2-0.20231221171913-5d5eded6bb15
+	github.com/consensys/gnark-crypto v0.12.2-0.20240215234832-d72fcb379d3e
 	github.com/fxamacker/cbor/v2 v2.5.0
 	github.com/google/go-cmp v0.5.9
 	github.com/google/pprof v0.0.0-20230817174616-7a8ec2ada47b

diff --git a/go.sum b/go.sum
@@ -6,8 +6,8 @@ github.com/consensys/bavard v0.1.13 h1:oLhMLOFGTLdlda/kma4VOJazblc7IM5y5QPd2A/Yj
 github.com/consensys/bavard v0.1.13/go.mod h1:9ItSMtA/dXMAiL7BG6bqW2m3NdSEObYWoH223nGHukI=
 github.com/consensys/compress v0.2.3 h1:B34qdHCg2t9Ikd2jS2UnrNZPG9I3PTBet6f5fHmG7to=
 github.com/consensys/compress v0.2.3/go.mod h1:Ne8+cGKjqgjF1dlHapZx38pHzWpaBYhsKxQa+JPl0zM=
-github.com/consensys/gnark-crypto v0.12.2-0.20231221171913-5d5eded6bb15 h1:mcxhrDtXKIepsKXofxSuXRst+41yzAcoNWKIotsjMTQ=
-github.com/consensys/gnark-crypto v0.12.2-0.20231221171913-5d5eded6bb15/go.mod h1:wKqwsieaKPThcFkHe0d0zMsbHEUWFmZcG7KBCse210o=
+github.com/consensys/gnark-crypto v0.12.2-0.20240215234832-d72fcb379d3e h1:MKdOuCiy2DAX1tMp2YsmtNDaqdigpY6B5cZQDJ9BvEo=
+github.com/consensys/gnark-crypto v0.12.2-0.20240215234832-d72fcb379d3e/go.mod h1:wKqwsieaKPThcFkHe0d0zMsbHEUWFmZcG7KBCse210o=
 github.com/coreos/go-systemd/v22 v22.5.0/go.mod h1:Y58oyj3AT4RCenI/lSvhwexgC+NSVTIJ3seZv2GcEnc=
 github.com/davecgh/go-spew v1.1.1 h1:vj9j/u1bqnvCEfJOwUhtlOARqs3+rkHYY13jYWTU97c=
 github.com/davecgh/go-spew v1.1.1/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=

diff --git a/internal/generator/backend/template/representations/gkr.go.tmpl b/internal/generator/backend/template/representations/gkr.go.tmpl
@@ -198,4 +198,4 @@ func GetHashBuilder(name string) (func() hash.Hash, error) {
 		return nil, fmt.Errorf("hash function not found")
 	}
 	return builder, nil
-}
+}
diff --git a/std/algebra/emulated/sw_emulated/point.go b/std/algebra/emulated/sw_emulated/point.go
@@ -129,10 +129,24 @@ func (c *Curve[B, S]) MarshalG1(p AffinePoint[B]) []frontend.Variable {
 	copy(res[len(bx):], by)
 	xZ := c.baseApi.IsZero(x)
 	yZ := c.baseApi.IsZero(y)
-	res[1] = c.api.Mul(xZ, yZ)
+	isZero := c.api.Mul(xZ, yZ)
+	// isZero = 0 -> res[1]=0
+	// isZero = 1, infty bit 0 -> res[1]=0
+	// isZero = 1, infty bit 1 -> res[1]=1
+	res[1] = c.api.Mul(isZero, c.marshalZeroG1())
 	return res
 }
 
+// different curves have different marshalling for zero point
+func (c *Curve[B, S]) marshalZeroG1() frontend.Variable {
+	var fp B
+	unusedBits := 64 - (fp.Modulus().BitLen() % 64)
+	if unusedBits >= 3 {
+		return 1
+	}
+	return 0
+}
+
 // Neg returns an inverse of p. It doesn't modify p.
 func (c *Curve[B, S]) Neg(p *AffinePoint[B]) *AffinePoint[B] {
 	return &AffinePoint[B]{

diff --git a/std/algebra/emulated/sw_emulated/point_test.go b/std/algebra/emulated/sw_emulated/point_test.go
@@ -121,6 +121,46 @@ func TestMarshalG1(t *testing.T) {
 	})
 }
 
+func TestMarshalG1OnBN254(t *testing.T) {
+	assert := test.NewAssert(t)
+	testFn := func(r fr_bn.Element) {
+		var P bn254.G1Affine
+		P.ScalarMultiplicationBase(r.BigInt(new(big.Int)))
+
+		gBytes := P.Marshal()
+
+		nbBytes := 2 * fr_bn.Bytes
+		nbBits := nbBytes * 8
+		circuit := &MarshalG1Test[emulated.BN254Fp, emulated.BN254Fr]{
+			R: make([]frontend.Variable, nbBits),
+		}
+		witness := &MarshalG1Test[emulated.BN254Fp, emulated.BN254Fr]{
+			G: AffinePoint[emulated.BN254Fp]{
+				X: emulated.ValueOf[emulated.BN254Fp](P.X),
+				Y: emulated.ValueOf[emulated.BN254Fp](P.Y),
+			},
+			R: make([]frontend.Variable, nbBits),
+		}
+		for i := 0; i < nbBytes; i++ {
+			for j := 0; j < 8; j++ {
+				witness.R[i*8+j] = (gBytes[i] >> (7 - j)) & 1
+			}
+		}
+		err := test.IsSolved(circuit, witness, testCurve.ScalarField())
+		assert.NoError(err)
+	}
+	assert.Run(func(assert *test.Assert) {
+		var r fr_bn.Element
+		r.SetRandom()
+		testFn(r)
+	})
+	assert.Run(func(assert *test.Assert) {
+		var r fr_bn.Element
+		r.SetZero()
+		testFn(r)
+	})
+}
+
 type NegTest[T, S emulated.FieldParams] struct {
 	P, Q AffinePoint[T]
 }

diff --git a/std/algebra/interfaces.go b/std/algebra/interfaces.go
@@ -99,4 +99,10 @@ type Pairing[G1El G1ElementT, G2El G2ElementT, GtEl GtElementT] interface {
 
 	// AssertIsEqual asserts the equality of the inputs.
 	AssertIsEqual(*GtEl, *GtEl)
+
+	// AssertIsOnG1 asserts that the input is on the G1 curve.
+	AssertIsOnG1(*G1El)
+
+	// AssertIsOnG2 asserts that the input is on the G2 curve.
+	AssertIsOnG2(*G2El)
 }
diff --git a/std/algebra/native/sw_bls12377/pairing2.go b/std/algebra/native/sw_bls12377/pairing2.go
@@ -91,76 +91,6 @@ func (c *Curve) AssertIsEqual(P, Q *G1Affine) {
 	P.AssertIsEqual(c.api, *Q)
 }
 
-// AssertIsOnCurve asserts if p belongs to the curve. It doesn't modify p.
-func (c *Curve) AssertIsOnCurve(p *G1Affine) {
-	// (X,Y) ∈ {Y² == X³ + 1} U (0,0)
-
-	// if p=(0,0) we assign b=0 and continue
-	selector := c.api.And(c.api.IsZero(p.X), c.api.IsZero(p.Y))
-	b := c.api.Select(selector, 0, 1)
-
-	left := c.api.Mul(p.Y, p.Y)
-	right := c.api.Mul(p.X, c.api.Mul(p.X, p.X))
-	right = c.api.Add(right, b)
-	c.api.AssertIsEqual(left, right)
-}
-
-func (c *Curve) AssertIsOnG1(P *G1Affine) {
-	// 1- Check P is on the curve
-	c.AssertIsOnCurve(P)
-
-	// 2- Check P has the right subgroup order
-	// [x²]ϕ(P)
-	phiP := G1Affine{
-		X: c.api.Mul(P.X, "80949648264912719408558363140637477264845294720710499478137287262712535938301461879813459410945"),
-		Y: P.Y,
-	}
-	var _P G1Affine
-	_P.scalarMulBySeed(c.api, &phiP)
-	_P.scalarMulBySeed(c.api, &_P)
-	_P.Neg(c.api, _P)
-
-	// [r]Q == 0 <==>  P = -[x²]ϕ(P)
-	P.AssertIsEqual(c.api, _P)
-}
-
-// AssertIsOnTwist asserts if p belongs to the curve. It doesn't modify p.
-func (c *Curve) AssertIsOnTwist(p *G2Affine) {
-	// (X,Y) ∈ {Y² == X³ + 1/u} U (0,0)
-
-	// if p=(0,0) we assign b=0 and continue
-	selector := c.api.And(p.P.X.IsZero(c.api), p.P.Y.IsZero(c.api))
-	var zero fields_bls12377.E2
-	zero.SetZero()
-	b := fields_bls12377.E2{
-		A0: 0,
-		A1: "155198655607781456406391640216936120121836107652948796323930557600032281009004493664981332883744016074664192874906",
-	}
-	b.Select(c.api, selector, zero, b)
-
-	var left, right fields_bls12377.E2
-	left.Square(c.api, p.P.Y)
-	right.Square(c.api, p.P.X)
-	right.Mul(c.api, right, p.P.X)
-	right.Add(c.api, right, b)
-	left.AssertIsEqual(c.api, right)
-}
-
-func (c *Curve) AssertIsOnG2(P *G2Affine) {
-	// 1- Check P is on the curve
-	c.AssertIsOnTwist(P)
-
-	// 2- Check P has the right subgroup order
-	// [x₀]Q
-	var xP, psiP g2AffP
-	xP.scalarMulBySeed(c.api, &P.P)
-	// ψ(Q)
-	psiP.psi(c.api, &P.P)
-
-	// [r]Q == 0 <==>  ψ(Q) == [x₀]Q
-	xP.AssertIsEqual(c.api, psiP)
-}
-
 // Neg negates P and returns the result. Does not modify P.
 func (c *Curve) Neg(P *G1Affine) *G1Affine {
 	res := &G1Affine{
@@ -380,6 +310,76 @@ func (p *Pairing) AssertIsEqual(e1, e2 *GT) {
 	e1.AssertIsEqual(p.api, *e2)
 }
 
+// AssertIsOnCurve asserts if p belongs to the curve. It doesn't modify p.
+func (c *Pairing) AssertIsOnCurve(p *G1Affine) {
+	// (X,Y) ∈ {Y² == X³ + 1} U (0,0)
+
+	// if p=(0,0) we assign b=0 and continue
+	selector := c.api.And(c.api.IsZero(p.X), c.api.IsZero(p.Y))
+	b := c.api.Select(selector, 0, 1)
+
+	left := c.api.Mul(p.Y, p.Y)
+	right := c.api.Mul(p.X, c.api.Mul(p.X, p.X))
+	right = c.api.Add(right, b)
+	c.api.AssertIsEqual(left, right)
+}
+
+func (c *Pairing) AssertIsOnG1(P *G1Affine) {
+	// 1- Check P is on the curve
+	c.AssertIsOnCurve(P)
+
+	// 2- Check P has the right subgroup order
+	// [x²]ϕ(P)
+	phiP := G1Affine{
+		X: c.api.Mul(P.X, "80949648264912719408558363140637477264845294720710499478137287262712535938301461879813459410945"),
+		Y: P.Y,
+	}
+	var _P G1Affine
+	_P.scalarMulBySeed(c.api, &phiP)
+	_P.scalarMulBySeed(c.api, &_P)
+	_P.Neg(c.api, _P)
+
+	// [r]Q == 0 <==>  P = -[x²]ϕ(P)
+	P.AssertIsEqual(c.api, _P)
+}
+
+// AssertIsOnTwist asserts if p belongs to the curve. It doesn't modify p.
+func (c *Pairing) AssertIsOnTwist(p *G2Affine) {
+	// (X,Y) ∈ {Y² == X³ + 1/u} U (0,0)
+
+	// if p=(0,0) we assign b=0 and continue
+	selector := c.api.And(p.P.X.IsZero(c.api), p.P.Y.IsZero(c.api))
+	var zero fields_bls12377.E2
+	zero.SetZero()
+	b := fields_bls12377.E2{
+		A0: 0,
+		A1: "155198655607781456406391640216936120121836107652948796323930557600032281009004493664981332883744016074664192874906",
+	}
+	b.Select(c.api, selector, zero, b)
+
+	var left, right fields_bls12377.E2
+	left.Square(c.api, p.P.Y)
+	right.Square(c.api, p.P.X)
+	right.Mul(c.api, right, p.P.X)
+	right.Add(c.api, right, b)
+	left.AssertIsEqual(c.api, right)
+}
+
+func (c *Pairing) AssertIsOnG2(P *G2Affine) {
+	// 1- Check P is on the curve
+	c.AssertIsOnTwist(P)
+
+	// 2- Check P has the right subgroup order
+	// [x₀]Q
+	var xP, psiP g2AffP
+	xP.scalarMulBySeed(c.api, &P.P)
+	// ψ(Q)
+	psiP.psi(c.api, &P.P)
+
+	// [r]Q == 0 <==>  ψ(Q) == [x₀]Q
+	xP.AssertIsEqual(c.api, psiP)
+}
+
 // NewG1Affine allocates a witness from the native G1 element and returns it.
 func NewG1Affine(v bls12377.G1Affine) G1Affine {
 	return G1Affine{

diff --git a/std/algebra/native/sw_bls12377/pairing_test.go b/std/algebra/native/sw_bls12377/pairing_test.go
@@ -64,12 +64,9 @@ type pairingBLS377 struct {
 }
 
 func (circuit *pairingBLS377) Define(api frontend.API) error {
-	cr, err := NewCurve(api)
-	if err != nil {
-		return err
-	}
-	cr.AssertIsOnG1(&circuit.P)
-	cr.AssertIsOnG2(&circuit.Q)
+	pr := NewPairing(api)
+	pr.AssertIsOnG1(&circuit.P)
+	pr.AssertIsOnG2(&circuit.Q)
 	pairingRes, _ := Pair(api, []G1Affine{circuit.P}, []G2Affine{circuit.Q})
 	pairingRes.AssertIsEqual(api, circuit.Res)
 
@@ -224,12 +221,9 @@ type groupMembership struct {
 }
 
 func (circuit *groupMembership) Define(api frontend.API) error {
-	cr, err := NewCurve(api)
-	if err != nil {
-		return err
-	}
-	cr.AssertIsOnG1(&circuit.P)
-	cr.AssertIsOnG2(&circuit.Q)
+	pr := NewPairing(api)
+	pr.AssertIsOnG1(&circuit.P)
+	pr.AssertIsOnG2(&circuit.Q)
 
 	return nil
 }

diff --git a/std/algebra/native/sw_bls24315/pairing2.go b/std/algebra/native/sw_bls24315/pairing2.go
@@ -306,6 +306,14 @@ func (p *Pairing) AssertIsEqual(e1, e2 *GT) {
 	e1.AssertIsEqual(p.api, *e2)
 }
 
+func (p *Pairing) AssertIsOnG1(P *G1Affine) {
+	panic("not implemented")
+}
+
+func (p *Pairing) AssertIsOnG2(P *G2Affine) {
+	panic("not implemented")
+}
+
 // NewG1Affine allocates a witness from the native G1 element and returns it.
 func NewG1Affine(v bls24315.G1Affine) G1Affine {
 	return G1Affine{