From 70baf16c1b70a93c453637f4ac4fd4cc8c9aac62 Mon Sep 17 00:00:00 2001
From: Gautam Botrel <gautam.botrel@gmail.com>
Date: Fri, 26 Jul 2024 09:26:12 -0500
Subject: [PATCH] fixes #1227: api.AssertIsLessOrEqual incorrect behavior on
 R1CS with constant variable (#1228)

* adds builder.Mul(aBits[i], builder.cstOne())

* rename 1226 to 1227
---
 frontend/cs/r1cs/api_assertions.go            | 28 ++++++++-----------
 frontend/cs/r1cs/builder.go                   |  4 +--
 .../issue1227/issue_1227_test.go              | 24 ++++++++++++++++
 3 files changed, 36 insertions(+), 20 deletions(-)
 create mode 100644 internal/regression_tests/issue1227/issue_1227_test.go

diff --git a/frontend/cs/r1cs/api_assertions.go b/frontend/cs/r1cs/api_assertions.go
index 328194685c..e62679d11b 100644
--- a/frontend/cs/r1cs/api_assertions.go
+++ b/frontend/cs/r1cs/api_assertions.go
@@ -129,9 +129,13 @@ func (builder *builder) mustBeLessOrEqVar(a, bound frontend.Variable) {
 	// here bound is NOT a constant,
 	// but a can be either constant or a wire.
 
-	_, aConst := builder.constantValue(a)
-
 	nbBits := builder.cs.FieldBitLen()
+	if ca, aConst := builder.constantValue(a); aConst {
+		// if a is a constant, we only need the number of bits of a;
+		// the binary decomposition of the bound will fail if nbBits(bound) > nbBits(a)
+		ba := builder.cs.ToBigInt(ca)
+		nbBits = ba.BitLen()
+	}
 
 	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs(), bits.OmitModulusCheck())
 	boundBits := bits.ToBinary(builder, bound, bits.WithNbDigits(nbBits))
@@ -152,28 +156,18 @@ func (builder *builder) mustBeLessOrEqVar(a, bound frontend.Variable) {
 		// else
 		// 		p[i] = p[i+1] * a[i]
 		//		t = 0
+
 		v := builder.Mul(p[i+1], aBits[i])
-		p[i] = builder.Select(boundBits[i], v, p[i+1])
 
+		p[i] = builder.Select(boundBits[i], v, p[i+1])
 		t := builder.Select(boundBits[i], zero, p[i+1])
-
-		// (1 - t - ai) * ai == 0
-		var l frontend.Variable
-		l = builder.cstOne()
-		l = builder.Sub(l, t, aBits[i])
-
 		// note if bound[i] == 1, this constraint is (1 - ai) * ai == 0
 		// → this is a boolean constraint
 		// if bound[i] == 0, t must be 0 or 1, thus ai must be 0 or 1 too
 
-		if aConst {
-			// aBits[i] is a constant;
-			l = builder.Mul(l, aBits[i])
-			// TODO @gbotrel this constraint seems useless.
-			added = append(added, builder.cs.AddR1C(builder.newR1C(l, zero, zero), builder.genericGate))
-		} else {
-			added = append(added, builder.cs.AddR1C(builder.newR1C(l, aBits[i], zero), builder.genericGate))
-		}
+		// (1 - t - ai) * ai == 0
+		l := builder.Sub(builder.cstOne(), t, aBits[i])
+		added = append(added, builder.cs.AddR1C(builder.newR1C(l, builder.Mul(aBits[i], builder.cstOne()), zero), builder.genericGate))
 	}
 
 	if debug.Debug {
diff --git a/frontend/cs/r1cs/builder.go b/frontend/cs/r1cs/builder.go
index 3102addbb5..bb0ac3c50c 100644
--- a/frontend/cs/r1cs/builder.go
+++ b/frontend/cs/r1cs/builder.go
@@ -211,9 +211,7 @@ func (builder *builder) getLinearExpression(_l interface{}) constraint.LinearExp
 	case constraint.LinearExpression:
 		L = tl
 	default:
-		if debug.Debug {
-			panic("invalid input for getLinearExpression") // sanity check
-		}
+		panic("invalid input for getLinearExpression") // sanity check
 	}
 
 	return L
diff --git a/internal/regression_tests/issue1227/issue_1227_test.go b/internal/regression_tests/issue1227/issue_1227_test.go
new file mode 100644
index 0000000000..3315f54d26
--- /dev/null
+++ b/internal/regression_tests/issue1227/issue_1227_test.go
@@ -0,0 +1,24 @@
+package issue1226
+
+import (
+	"testing"
+
+	"github.com/consensys/gnark/frontend"
+	"github.com/consensys/gnark/test"
+)
+
+type Circuit struct {
+	X frontend.Variable
+}
+
+func (circuit *Circuit) Define(api frontend.API) error {
+	api.AssertIsLessOrEqual(1, circuit.X)
+	return nil
+}
+
+func TestConstantPath(t *testing.T) {
+	assert := test.NewAssert(t)
+	assert.CheckCircuit(&Circuit{},
+		test.WithValidAssignment(&Circuit{X: 1}),   // 1 <= 1 --> true
+		test.WithInvalidAssignment(&Circuit{X: 0})) // 1 <= 0 --> false
+}