fix: scs add/mul when recorded constraint is 0

[yelhousni]

Description

In addConstraintExist and mulConstraintExist we re-use cached constraints to avoid introducing new ones and compute a division for the output wire. But when some of the coefficients are 0 we panic because of a div by 0. This PR avoids this by checking if the coefficient is 0.

Type of change

• Bug fix (non-breaking change which fixes an issue)

How has this been tested?

The test TestVarScalarMulG2EdgeCases in

gnark/std/algebra/native/sw_bls12377/g2_test.go

Line 288 in 7cc8816

func TestVarScalarMulG2EdgeCases(t *testing.T) {

fails for PLONK without this PR.

How has this been benchmarked?

N/A

Checklist:

• I have performed a self-review of my code
• I have commented my code, particularly in hard-to-understand areas
• I have made corresponding changes to the documentation
• I have added tests that prove my fix is effective or that my feature works
• I did not modify files generated from templates
• golangci-lint does not output errors locally
• New and existing unit tests pass locally with my changes
• Any dependent changes have been merged and published in downstream modules

[ivokub]

Hmm, I have been looking at the PR and I'm not sure if mulConstraintExists is a right place for the fix. When we get to the condition

if iID, ok := builder.mMulInstructions[h]; ok {

and we encounter the division by zero then it means that there already exists a gate 0 * xA * xB - xc == 0. I think that it would be better to filter it in splitProd and filtering out inputs for which the coefficient is zero.

I'm posting the suggested edit, maybe describes better.

[ivokub]

Suggested edit:

diff --git a/frontend/cs/scs/builder.go b/frontend/cs/scs/builder.go
index 90a64e1e..1c62d37d 100644
--- a/frontend/cs/scs/builder.go
+++ b/frontend/cs/scs/builder.go
@@ -518,7 +518,7 @@ func (builder *builder) addConstraintExist(a, b expr.Term, k constraint.Element)
 			q4 := qR
 			q3 = builder.cs.Mul(q3, q2)
 			q1 = builder.cs.Mul(q1, q4)
-			if q1 == q3 && !q2.IsZero() {
+			if q1 == q3 {
 				// no need to introduce a new constraint;
 				// compute n, the coefficient for the output wire
 				q2, ok = builder.cs.Inverse(q2)
@@ -583,14 +583,14 @@ func (builder *builder) mulConstraintExist(a, b expr.Term) (expr.Term, bool) {
 		// recompute the qM coeff and check that it matches;
 		qM := builder.cs.Mul(a.Coeff, b.Coeff)
 		tm := builder.cs.MakeTerm(qM, 0)
-		N := builder.cs.GetCoefficient(int(c.QM))
-		if int(c.QM) != tm.CoeffID() && !N.IsZero() {
+		if int(c.QM) != tm.CoeffID() {
 			// so we wanted to compute
 			// N * xC == qM*xA*xB
 			// but found a constraint
 			// xC == qM'*xA*xB
 			// the coefficient for our resulting wire is different;
 			// N = qM / qM'
+			N := builder.cs.GetCoefficient(int(c.QM))
 			N, ok := builder.cs.Inverse(N)
 			if !ok {
 				panic("div by 0") // sanity check.
@@ -617,6 +617,10 @@ func (builder *builder) splitProd(acc expr.Term, r expr.LinearExpression) expr.T
 	}
 	// we want to add a constraint such that acc * r[0] == o
 	// let's check if we didn't already constrain a similar product
+	if r[0].Coeff.IsZero() {
+		// we can skip this term, it is zero
+		return builder.splitProd(acc, r[1:])
+	}
 	o, found := builder.mulConstraintExist(acc, r[0])
 
 	if !found {

[ivokub]

In the suggested edit, I also removed the check for addConstraintExists as imo we already filter zero cases out.

I'll also try to implement the test case in https://github.com/Consensys/gnark/blob/master/frontend/cs/scs/api_test.go#L106 to see if my version of the fix works and to ensure we do not have regression in the future.

[ivokub]

Test case for isolating:

type IssueDiv0Circuit2 struct {
	A1, B1 frontend.Variable

	Res1, Res2 frontend.Variable
}

func (c *IssueDiv0Circuit2) Define(api frontend.API) error {
	// case 1
	t1 := api.Mul(api.Mul(0, c.A1), api.Mul(4, c.B1))
	t2 := api.Mul(api.Mul(2, c.A1), api.Mul(5, c.B1))

	// test solver
	api.AssertIsEqual(t1, c.Res1)
	api.AssertIsEqual(t2, c.Res2)
	return nil
}

func TestExistDiv02(t *testing.T) {
	assert := test.NewAssert(t)
	ccs, err := frontend.Compile(ecc.BN254.ScalarField(), scs.NewBuilder, &IssueDiv0Circuit2{})
	if err != nil {
		t.Fatal(err)
	}
	assert.NoError(err)
	w, err := frontend.NewWitness(&IssueDiv0Circuit2{
		A1: 11, B1: 21,
		Res1: 0, Res2: 2310,
	}, ecc.BN254.ScalarField())
	assert.NoError(err)
	solution, err := ccs.Solve(w)
	assert.NoError(err)
}

[ivokub]

Suggested edit:

diff --git a/frontend/cs/scs/api.go b/frontend/cs/scs/api.go
index 12ff9be0..77cb2e50 100644
--- a/frontend/cs/scs/api.go
+++ b/frontend/cs/scs/api.go
@@ -138,6 +138,14 @@ func (builder *builder) Mul(i1, i2 frontend.Variable, in ...frontend.Variable) f
 	if len(vars) == 0 {
 		return builder.cs.ToBigInt(k)
 	}
+	if k.IsZero() {
+		return 0
+	}
+	for i := range vars {
+		if vars[i].Coeff.IsZero() {
+			return 0
+		}
+	}
 	l := builder.mulConstant(vars[0], k)
 
 	return builder.splitProd(l, vars[1:])
diff --git a/frontend/cs/scs/api_test.go b/frontend/cs/scs/api_test.go
index 2c57fed7..40c96720 100644
--- a/frontend/cs/scs/api_test.go
+++ b/frontend/cs/scs/api_test.go
@@ -135,9 +135,6 @@ func (c *IssueDiv0Circuit) Define(api frontend.API) error {
 func TestExistDiv0(t *testing.T) {
 	assert := test.NewAssert(t)
 	ccs, err := frontend.Compile(ecc.BN254.ScalarField(), scs.NewBuilder, &IssueDiv0Circuit{})
-	if err != nil {
-		t.Fatal(err)
-	}
 	assert.NoError(err)
 	w, err := frontend.NewWitness(&IssueDiv0Circuit{
 		A1: 11, B1: 21,
@@ -150,9 +147,70 @@ func TestExistDiv0(t *testing.T) {
 		Res7: 0, Res8: 55,
 	}, ecc.BN254.ScalarField())
 	assert.NoError(err)
-	solution, err := ccs.Solve(w)
+	_, err = ccs.Solve(w)
 	assert.NoError(err)
-	_ = solution
+}
+
+type IssueDiv0Circuit2 struct {
+	A1, B1 frontend.Variable
+
+	Res1, Res2 frontend.Variable
+}
+
+func (c *IssueDiv0Circuit2) Define(api frontend.API) error {
+	// case 1
+	b1 := api.Mul(0, c.A1)
+	b2 := api.Mul(4, c.B1)
+	t1 := api.Mul(b1, b2)
+
+	b3 := api.Mul(2, c.A1)
+	b4 := api.Mul(5, c.B1)
+	t2 := api.Mul(b3, b4)
+
+	// test solver
+	api.AssertIsEqual(t1, c.Res1)
+	api.AssertIsEqual(t2, c.Res2)
+	return nil
+}
+
+func TestExistDiv02(t *testing.T) {
+	assert := test.NewAssert(t)
+	ccs, err := frontend.Compile(ecc.BN254.ScalarField(), scs.NewBuilder, &IssueDiv0Circuit2{})
+	assert.NoError(err)
+	w, err := frontend.NewWitness(&IssueDiv0Circuit2{
+		A1: 11, B1: 21,
+		Res1: 0, Res2: 2310,
+	}, ecc.BN254.ScalarField())
+	assert.NoError(err)
+	_, err = ccs.Solve(w)
+	assert.NoError(err)
+}
+
+type TestZeroMulNoConstraintCircuit struct {
+	A, B frontend.Variable
+}
+
+func (c *TestZeroMulNoConstraintCircuit) Define(api frontend.API) error {
+	// case 1
+	t1 := api.Mul(0, c.A)
+	t2 := api.Mul(t1, c.B)
+
+	t3 := api.Sub(c.A, c.A)
+	t4 := api.Mul(3, t3)
+
+	// test solver
+	api.AssertIsEqual(t2, 0)
+	api.AssertIsEqual(t4, 0)
+	return nil
+}
+
+func TestZeroMulNoConstraint(t *testing.T) {
+	assert := test.NewAssert(t)
+	ccs, err := frontend.Compile(ecc.BN254.ScalarField(), scs.NewBuilder, &TestZeroMulNoConstraintCircuit{})
+	assert.NoError(err)
+	if ccs.GetNbConstraints() != 0 {
+		t.Fatal("expected 0 constraints")
+	}
 }
 
 type mulAccFastTrackCircuit struct {

[ivokub]

Have a look at my proposal -- what this does is that in case of multiplication by zero constant or a term with zero coefficient (for example when we do X-X), then we do not record any constraint at all and instead return constant zero. This should fix the mulConstraintExists issue in general as we should never have a constraint anymore where we have qM == 0.

I also added test cases to isolate the bug and to detect regression and also a test to ensure that we indeed do not record any constraints in this case. Imo with the suggested changes we can revert your change to mulConstraintExists.

[yelhousni]

Have a look at my proposal -- what this does is that in case of multiplication by zero constant or a term with zero coefficient (for example when we do X-X), then we do not record any constraint at all and instead return constant zero. This should fix the mulConstraintExists issue in general as we should never have a constraint anymore where we have qM == 0.

I also added test cases to isolate the bug and to detect regression and also a test to ensure that we indeed do not record any constraints in this case. Imo with the suggested changes we can revert your change to mulConstraintExists.

That makes more sense not to record any zero'ed constraints. I think you can directly apply your edits here or close this PR and open another one.

[ivokub]

I applied my suggestions, but I cannot set you as a reviewer. If looks good then it is good to merge from my side!