CVE-2023-44378: Incorrect Comparison (CWE-697)
value: gnark is a zk-SNARK library that offers a high-level API to design circuits. Prior to version 0.9.0, for some in-circuit values, it is possible to construct two valid decomposition to bits. In addition to the canonical decomposition of `a`, for small values there exists a second decomposition for `a+r` (where `r` is the modulus the values are being reduced by). The second decomposition was possible due to overflowing the field where the values are defined. Upgrading to version 0.9.0 should fix the issue without needing to change the calls to value comparison methods.
CWE description: The product compares two entities in a security-relevant context, but the comparison is incorrect, which may lead to resultant weaknesses.
CVSS v3 base score: 5.5
Published: 2023-10-09T14:15Z
Repository: https://github.com/Consensys/gnark
Language: Go
Files changed: frontend/api.go, frontend/cs/r1cs/api.go, frontend/cs/r1cs/api_assertions.go, frontend/cs/scs/api.go, frontend/cs/scs/api_assertions.go, internal/backend/circuits/hint.go, internal/regression_tests/doc.go, internal/regression_tests/issue_836_test.go, std/math/bits/conversion.go, std/math/bits/conversion_binary.go, std/math/bits/intf_constcheck.go, test/engine.go
Commit date: 2023-09-19 10:26:49 +0200
Commit message: fix: assert that the binary decomposition of a variable is less than the modulus (#835)

The issue was reported by Marcin Kostrzewa @ Reilabs (@kustosz).

* test: add internal regression test pacakge for tracking filed bugs

* test: add test for reproducing non-unique binary decomposition

* refactor: make comparison against a constant bound public

Even though the method is public this method is not listable as we export
interfaces with smaller method sets. The method can be accessed by implicitly
implementing interface with the method `MustBeLessOrEqCst(aBits
[]frontend.Variable, bound *big.Int, aForDebug frontend.Variable)`.

We use the method for checking in `std/math/bits` package that the binary
decomposition of the bound returned by hint is less than the modulus.

* feat: add option to omit uniqueness check when binary decomposing value

* fix: check that the binary decomposition is unique when nbBits=modlen

* refactor: use bits gadget directly for option control

* docs: describe in documentation alternatives to Cmp and LEQ

* test: add test for math/cmp cases

* feat: add TestEngine checking

* test: reduce binary decomposition length to accomodate tinyfield

* refactor: rename to OmitModulusCheck

* fix: limit decomposition length to fieldbitlen

* feat: allow less than nbBits in constant comparison

* test: update circuit statistics

* feat: allow decomposition length be longer than field length

* Revert "feat: add TestEngine checking"

This reverts commit 8da5d07924d2faf0d014f1e00781516fa0070dff.

* test: implement constant comparison for test engine

* test: rename file to track issue
Diff: diff --git a/frontend/api.go b/frontend/api.go
index 20a29c9d..6b23049f 100644
--- a/frontend/api.go
+++ b/frontend/api.go
@@ -98,11 +98,18 @@ type API interface {
 	Lookup2(b0, b1 Variable, i0, i1, i2, i3 Variable) Variable
 
 	// IsZero returns 1 if a is zero, 0 otherwise
 	IsZero(i1 Variable) Variable
 
-	// Cmp returns 1 if i1>i2, 0 if i1=i2, -1 if i1<i2
+	// Cmp returns:
+	//  * 1 if i1>i2,
+	//  * 0 if i1=i2,
+	//  * -1 if i1<i2.
+	//
+	// If the absolute difference between the variables i1 and i2 is known, then
+	// it is more efficient to use the bounded methdods in package
+	// [github.com/consensys/gnark/std/math/bits].
 	Cmp(i1, i2 Variable) Variable
 
 	// ---------------------------------------------------------------------------------------------
 	// Assertions
 
@@ -113,11 +120,15 @@ type API interface {
 	AssertIsDifferent(i1, i2 Variable)
 
 	// AssertIsBoolean fails if v != 0 ∥ v != 1
 	AssertIsBoolean(i1 Variable)
 
-	// AssertIsLessOrEqual fails if  v > bound
+	// AssertIsLessOrEqual fails if v > bound.
+	//
+	// If the absolute difference between the variables b and bound is known, then
+	// it is more efficient to use the bounded methdods in package
+	// [github.com/consensys/gnark/std/math/bits].
 	AssertIsLessOrEqual(v Variable, bound Variable)
 
 	// Println behaves like fmt.Println but accepts cd.Variable as parameter
 	// whose value will be resolved at runtime when computed by the solver
 	Println(a ...Variable)
diff --git a/frontend/cs/r1cs/api.go b/frontend/cs/r1cs/api.go
index 797bba08..bef33307 100644
--- a/frontend/cs/r1cs/api.go
+++ b/frontend/cs/r1cs/api.go
@@ -17,16 +17,17 @@ limitations under the License.
 package r1cs
 
 import (
 	"errors"
 	"fmt"
-	"github.com/consensys/gnark/internal/utils"
 	"path/filepath"
 	"reflect"
 	"runtime"
 	"strings"
 
+	"github.com/consensys/gnark/internal/utils"
+
 	"github.com/consensys/gnark/debug"
 	"github.com/consensys/gnark/frontend/cs"
 
 	"github.com/consensys/gnark/constraint"
 	"github.com/consensys/gnark/constraint/solver"
@@ -568,13 +569,16 @@ func (builder *builder) IsZero(i1 frontend.Variable) frontend.Variable {
 }
 
 // Cmp returns 1 if i1>i2, 0 if i1=i2, -1 if i1<i2
 func (builder *builder) Cmp(i1, i2 frontend.Variable) frontend.Variable {
 
-	vars, _ := builder.toVariables(i1, i2)
-	bi1 := builder.ToBinary(vars[0], builder.cs.FieldBitLen())
-	bi2 := builder.ToBinary(vars[1], builder.cs.FieldBitLen())
+	nbBits := builder.cs.FieldBitLen()
+	// in AssertIsLessOrEq we omitted comparison against modulus for the left
+	// side as if `a+r<b` implies `a<b`, then here we compute the inequality
+	// directly.
+	bi1 := bits.ToBinary(builder, i1, bits.WithNbDigits(nbBits))
+	bi2 := bits.ToBinary(builder, i2, bits.WithNbDigits(nbBits))
 
 	res := builder.cstZero()
 
 	for i := builder.cs.FieldBitLen() - 1; i >= 0; i-- {
 
diff --git a/frontend/cs/r1cs/api_assertions.go b/frontend/cs/r1cs/api_assertions.go
index 3c249f48..2ea2ec15 100644
--- a/frontend/cs/r1cs/api_assertions.go
+++ b/frontend/cs/r1cs/api_assertions.go
@@ -97,14 +97,16 @@ func (builder *builder) AssertIsLessOrEqual(v frontend.Variable, bound frontend.
 		if bv.Cmp(bb) == 1 {
 			panic(fmt.Sprintf("AssertIsLessOrEqual: %s > %s", bv.String(), bb.String()))
 		}
 	}
 
+	nbBits := builder.cs.FieldBitLen()
+	vBits := bits.ToBinary(builder, v, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
+
 	// bound is constant
 	if bConst {
-		vv := builder.toVariable(v)
-		builder.mustBeLessOrEqCst(vv, builder.cs.ToBigInt(cb))
+		builder.MustBeLessOrEqCst(vBits, builder.cs.ToBigInt(cb), v)
 		return
 	}
 
 	builder.mustBeLessOrEqVar(v, bound)
 }
@@ -117,12 +119,12 @@ func (builder *builder) mustBeLessOrEqVar(a, bound frontend.Variable) {
 
 	debug := builder.newDebugInfo("mustBeLessOrEq", a, " <= ", bound)
 
 	nbBits := builder.cs.FieldBitLen()
 
-	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
-	boundBits := builder.ToBinary(bound, nbBits)
+	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs(), bits.OmitModulusCheck())
+	boundBits := bits.ToBinary(builder, bound, bits.WithNbDigits(nbBits))
 
 	// constraint added
 	added := make([]int, 0, nbBits)
 
 	p := make([]frontend.Variable, nbBits+1)
@@ -164,28 +166,33 @@ func (builder *builder) mustBeLessOrEqVar(a, bound frontend.Variable) {
 
 	builder.cs.AttachDebugInfo(debug, added)
 
 }
 
-func (builder *builder) mustBeLessOrEqCst(a expr.LinearExpression, bound *big.Int) {
+// MustBeLessOrEqCst asserts that value represented using its bit decomposition
+// aBits is less or equal than constant bound. The method boolean constraints
+// the bits in aBits, so the caller can provide unconstrained bits.
+func (builder *builder) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
 
 	nbBits := builder.cs.FieldBitLen()
+	if len(aBits) > nbBits {
+		panic("more input bits than field bit length")
+	}
+	for i := len(aBits); i < nbBits; i++ {
+		aBits = append(aBits, 0)
+	}
 
 	// ensure the bound is positive, it's bit-len doesn't matter
 	if bound.Sign() == -1 {
 		panic("AssertIsLessOrEqual: bound must be positive")
 	}
 	if bound.BitLen() > nbBits {
 		panic("AssertIsLessOrEqual: bound is too large, constraint will never be satisfied")
 	}
 
 	// debug info
-	debug := builder.newDebugInfo("mustBeLessOrEq", a, " <= ", builder.toVariable(bound))
-
-	// note that at this stage, we didn't boolean-constraint these new variables yet
-	// (as opposed to ToBinary)
-	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
+	debug := builder.newDebugInfo("mustBeLessOrEq", aForDebug, " <= ", builder.toVariable(bound))
 
 	// t trailing bits in the bound
 	t := 0
 	for i := 0; i < nbBits; i++ {
 		if bound.Bit(i) == 0 {
diff --git a/frontend/cs/scs/api.go b/frontend/cs/scs/api.go
index 75764878..57c47fb8 100644
--- a/frontend/cs/scs/api.go
+++ b/frontend/cs/scs/api.go
@@ -472,12 +472,16 @@ func (builder *builder) IsZero(i1 frontend.Variable) frontend.Variable {
 }
 
 // Cmp returns 1 if i1>i2, 0 if i1=i2, -1 if i1<i2
 func (builder *builder) Cmp(i1, i2 frontend.Variable) frontend.Variable {
 
-	bi1 := builder.ToBinary(i1, builder.cs.FieldBitLen())
-	bi2 := builder.ToBinary(i2, builder.cs.FieldBitLen())
+	nbBits := builder.cs.FieldBitLen()
+	// in AssertIsLessOrEq we omitted comparison against modulus for the left
+	// side as if `a+r<b` implies `a<b`, then here we compute the inequality
+	// directly.
+	bi1 := bits.ToBinary(builder, i1, bits.WithNbDigits(nbBits))
+	bi2 := bits.ToBinary(builder, i2, bits.WithNbDigits(nbBits))
 
 	var res frontend.Variable
 	res = 0
 
 	for i := builder.cs.FieldBitLen() - 1; i >= 0; i-- {
diff --git a/frontend/cs/scs/api_assertions.go b/frontend/cs/scs/api_assertions.go
index 06e5f899..3b0d489e 100644
--- a/frontend/cs/scs/api_assertions.go
+++ b/frontend/cs/scs/api_assertions.go
@@ -21,11 +21,10 @@ import (
 	"math/big"
 
 	"github.com/consensys/gnark/debug"
 	"github.com/consensys/gnark/frontend"
 	"github.com/consensys/gnark/frontend/internal/expr"
-	"github.com/consensys/gnark/internal/utils"
 	"github.com/consensys/gnark/std/math/bits"
 )
 
 // AssertIsEqual fails if i1 != i2
 func (builder *builder) AssertIsEqual(i1, i2 frontend.Variable) {
@@ -129,26 +128,45 @@ func (builder *builder) AssertIsBoolean(i1 frontend.Variable) {
 
 }
 
 // AssertIsLessOrEqual fails if  v > bound
 func (builder *builder) AssertIsLessOrEqual(v frontend.Variable, bound frontend.Variable) {
-	switch b := bound.(type) {
-	case expr.Term:
+	cv, vConst := builder.constantValue(v)
+	cb, bConst := builder.constantValue(bound)
+
+	// both inputs are constants
+	if vConst && bConst {
+		bv, bb := builder.cs.ToBigInt(cv), builder.cs.ToBigInt(cb)
+		if bv.Cmp(bb) == 1 {
+			panic(fmt.Sprintf("AssertIsLessOrEqual: %s > %s", bv.String(), bb.String()))
+		}
+	}
+
+	nbBits := builder.cs.FieldBitLen()
+	vBits := bits.ToBinary(builder, v, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
+
+	// bound is constant
+	if bConst {
+		builder.MustBeLessOrEqCst(vBits, builder.cs.ToBigInt(cb), v)
+		return
+	}
+
+	if b, ok := bound.(expr.Term); ok {
 		builder.mustBeLessOrEqVar(v, b)
-	default:
-		builder.mustBeLessOrEqCst(v, utils.FromInterface(b))
+	} else {
+		panic(fmt.Sprintf("expected bound type expr.Term, got %T", bound))
 	}
 }
 
 func (builder *builder) mustBeLessOrEqVar(a frontend.Variable, bound expr.Term) {
 
 	debug := builder.newDebugInfo("mustBeLessOrEq", a, " <= ", bound)
 
 	nbBits := builder.cs.FieldBitLen()
 
-	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
-	boundBits := builder.ToBinary(bound, nbBits)
+	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs(), bits.OmitModulusCheck())
+	boundBits := bits.ToBinary(builder, bound, bits.WithNbDigits(nbBits)) // enforces range check against modulus
 
 	p := make([]frontend.Variable, nbBits+1)
 	p[nbBits] = 1
 
 	for i := nbBits - 1; i >= 0; i-- {
@@ -189,36 +207,33 @@ func (builder *builder) mustBeLessOrEqVar(a frontend.Variable, bound expr.Term)
 
 	}
 
 }
 
-func (builder *builder) mustBeLessOrEqCst(a frontend.Variable, bound big.Int) {
+// MustBeLessOrEqCst asserts that value represented using its bit decomposition
+// aBits is less or equal than constant bound. The method boolean constraints
+// the bits in aBits, so the caller can provide unconstrained bits.
+func (builder *builder) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
 
 	nbBits := builder.cs.FieldBitLen()
+	if len(aBits) > nbBits {
+		panic("more input bits than field bit length")
+	}
+	for i := len(aBits); i < nbBits; i++ {
+		aBits = append(aBits, 0)
+	}
 
 	// ensure the bound is positive, it's bit-len doesn't matter
 	if bound.Sign() == -1 {
 		panic("AssertIsLessOrEqual: bound must be positive")
 	}
 	if bound.BitLen() > nbBits {
 		panic("AssertIsLessOrEqual: bound is too large, constraint will never be satisfied")
 	}
 
-	if ca, ok := builder.constantValue(a); ok {
-		// a is constant, compare the big int values
-		ba := builder.cs.ToBigInt(ca)
-		if ba.Cmp(&bound) == 1 {
-			panic(fmt.Sprintf("AssertIsLessOrEqual: %s > %s", ba.String(), bound.String()))
-		}
-	}
-
 	// debug info
-	debug := builder.newDebugInfo("mustBeLessOrEq", a, " <= ", bound)
-
-	// note that at this stage, we didn't boolean-constraint these new variables yet
-	// (as opposed to ToBinary)
-	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
+	debug := builder.newDebugInfo("mustBeLessOrEq", aForDebug, " <= ", bound)
 
 	// t trailing bits in the bound
 	t := 0
 	for i := 0; i < nbBits; i++ {
 		if bound.Bit(i) == 0 {
diff --git a/internal/backend/circuits/hint.go b/internal/backend/circuits/hint.go
index 4154ab65..2489ce1e 100644
--- a/internal/backend/circuits/hint.go
+++ b/internal/backend/circuits/hint.go
@@ -65,11 +65,11 @@ func (circuit *recursiveHint) Define(api frontend.API) error {
 	linearExpression := api.Add(circuit.A, w1[0])
 
 	// api.ToBinary calls another hint (bits.NBits) with linearExpression as input
 	// however, when the solver will resolve bits[...] it will need to detect w1 as a dependency
 	// in order to compute the correct linearExpression value
-	bits := api.ToBinary(linearExpression, 10)
+	bits := api.ToBinary(linearExpression, 6)
 
 	a := api.FromBinary(bits...)
 
 	api.AssertIsEqual(a, 45)
 
diff --git a/internal/regression_tests/doc.go b/internal/regression_tests/doc.go
new file mode 100644
index 00000000..d44a4382
--- /dev/null
+++ b/internal/regression_tests/doc.go
@@ -0,0 +1,2 @@
+// Package regressiontests includes tests to avoid re-introducing regressions.
+package regressiontests
diff --git a/internal/regression_tests/issue_836_test.go b/internal/regression_tests/issue_836_test.go
new file mode 100644
index 00000000..3cd2e8f0
--- /dev/null
+++ b/internal/regression_tests/issue_836_test.go
@@ -0,0 +1,167 @@
+package regressiontests
+
+import (
+	"fmt"
+	"math/big"
+	"testing"
+
+	"github.com/consensys/gnark/constraint/solver"
+	"github.com/consensys/gnark/frontend"
+	"github.com/consensys/gnark/std/math/cmp"
+	"github.com/consensys/gnark/test"
+)
+
+type CmpCircuit struct {
+	Left      frontend.Variable
+	Right     frontend.Variable
+	ExpCmpRes frontend.Variable
+}
+
+func (c *CmpCircuit) Define(api frontend.API) error {
+	r := api.Cmp(c.Left, c.Right)
+	api.AssertIsEqual(r, c.ExpCmpRes)
+	return nil
+}
+
+type AssertIsLessOrEqCircuit struct {
+	Smaller, Bigger frontend.Variable
+}
+
+func (c *AssertIsLessOrEqCircuit) Define(api frontend.API) error {
+	api.AssertIsLessOrEqual(c.Smaller, c.Bigger)
+	return nil
+}
+
+type MathCmpAssertIsLessOrEqCircuitBounded struct {
+	Left  frontend.Variable
+	Right frontend.Variable
+}
+
+func (c *MathCmpAssertIsLessOrEqCircuitBounded) Define(api frontend.API) error {
+	cmper := cmp.NewBoundedComparator(api, big.NewInt(6), false)
+	cmper.AssertIsLessEq(c.Left, c.Right)
+	return nil
+}
+
+type MathCmpAssertIsLessOrEqCircuitFull struct {
+	Left  frontend.Variable
+	Right frontend.Variable
+}
+
+func (c *MathCmpAssertIsLessOrEqCircuitFull) Define(api frontend.API) error {
+	api.AssertIsEqual(1, cmp.IsLessOrEqual(api, c.Left, c.Right))
+	return nil
+}
+
+func getNBitsHint() (solver.HintID, error) {
+	for _, v := range solver.GetRegisteredHints() {
+		if solver.GetHintName(v) == "github.com/consensys/gnark/std/math/bits.nBits" {
+			return solver.GetHintID(v), nil
+		}
+	}
+	return 0, fmt.Errorf("nBits hint not found")
+}
+
+func TestIssue836Cmp(t *testing.T) {
+	assert := test.NewAssert(t)
+	assignmentNoHintGood := CmpCircuit{
+		Left:      10,
+		Right:     5,
+		ExpCmpRes: 1,
+	}
+	assignmentNoHintBad := CmpCircuit{
+		Left:      5,
+		Right:     10,
+		ExpCmpRes: 1,
+	}
+	assignmentHintBad := CmpCircuit{
+		Left:      10,
+		Right:     5,
+		ExpCmpRes: -1,
+	}
+	toReplaceHint, err := getNBitsHint()
+	if err != nil {
+		t.Fatalf("couldn't find hint to replace: %v", err)
+	}
+	assert.CheckCircuit(&CmpCircuit{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
+	assert.CheckCircuit(&CmpCircuit{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
+}
+
+func TestIssue836AssertIsLess(t *testing.T) {
+	assert := test.NewAssert(t)
+	assignmentNoHintGood := AssertIsLessOrEqCircuit{
+		Smaller: 5,
+		Bigger:  10,
+	}
+	assignmentNoHintBad := AssertIsLessOrEqCircuit{
+		Smaller: 11,
+		Bigger:  10,
+	}
+	assignmentHintBad := AssertIsLessOrEqCircuit{
+		Smaller: 10,
+		Bigger:  5,
+	}
+	toReplaceHint, err := getNBitsHint()
+	if err != nil {
+		t.Fatalf("couldn't find hint to replace: %v", err)
+	}
+	assert.CheckCircuit(&AssertIsLessOrEqCircuit{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
+	assert.CheckCircuit(&AssertIsLessOrEqCircuit{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
+}
+
+func TestIssue836MathCmpAssertIsLessEqBounded(t *testing.T) {
+	assert := test.NewAssert(t)
+	assignmentNoHintGood := MathCmpAssertIsLessOrEqCircuitBounded{
+		Left:  5,
+		Right: 10,
+	}
+	assignmentNoHintBad := MathCmpAssertIsLessOrEqCircuitBounded{
+		Left:  11,
+		Right: 10,
+	}
+	assignmentHintBad := MathCmpAssertIsLessOrEqCircuitBounded{
+		Left:  10,
+		Right: 5,
+	}
+	toReplaceHint, err := getNBitsHint()
+	if err != nil {
+		t.Fatalf("couldn't find hint to replace: %v", err)
+	}
+	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitBounded{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
+	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitBounded{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
+}
+
+func TestIssueXXXMathCmpAssertIsLessEqFull(t *testing.T) {
+	assert := test.NewAssert(t)
+	assignmentNoHintGood := MathCmpAssertIsLessOrEqCircuitFull{
+		Left:  5,
+		Right: 10,
+	}
+	assignmentNoHintBad := MathCmpAssertIsLessOrEqCircuitFull{
+		Left:  11,
+		Right: 10,
+	}
+	assignmentHintBad := MathCmpAssertIsLessOrEqCircuitFull{
+		Left:  10,
+		Right: 5,
+	}
+	toReplaceHint, err := getNBitsHint()
+	if err != nil {
+		t.Fatalf("couldn't find hint to replace: %v", err)
+	}
+	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitFull{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
+	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitFull{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
+}
+
+func maliciousNbitsHint(mod *big.Int, inputs []*big.Int, results []*big.Int) error {
+	n := inputs[0]
+	// This is a malicious hint. If n is less equal than 5, then add the
+	// modulus. This creates a non-unique binary decomposition of the value.
+	if n.Cmp(big.NewInt(5)) <= 0 {
+		n = n.Add(n, mod)
+	}
+	for i := 0; i < len(results); i++ {
+		results[i].SetUint64(uint64(n.Bit(i)))
+	}
+	return nil
+}
diff --git a/internal/stats/latest.stats b/internal/stats/latest.stats
index 9046cc8a..1d6fab6f 100644
Binary files a/internal/stats/latest.stats and b/internal/stats/latest.stats differ
diff --git a/std/math/bits/conversion.go b/std/math/bits/conversion.go
index 87e00795..e003b950 100644
--- a/std/math/bits/conversion.go
+++ b/std/math/bits/conversion.go
@@ -49,20 +49,28 @@ func FromBase(api frontend.API, base Base, digits []frontend.Variable, opts ...B
 
 type baseConversionConfig struct {
 	NbDigits             int
 	UnconstrainedOutputs bool
 	UnconstrainedInputs  bool
+
+	omitModulusCheck bool
 }
 
 // BaseConversionOption configures the behaviour of scalar decomposition.
 type BaseConversionOption func(opt *baseConversionConfig) error
 
-// WithNbDigits sets the resulting number of digits (nbDigits) to be used in the base conversion.
-// nbDigits must be > 0. If nbDigits is lower than the length of full decomposition and
-// WithUnconstrainedOutputs option is not used, then the conversion functions will generate an
-// unsatisfiable constraint. If WithNbDigits option is not set, then the full decomposition is
-// returned.
+// WithNbDigits sets the resulting number of digits (nbDigits) to be used in the
+// base conversion.
+//
+// nbDigits must be > 0. If nbDigits is lower than the length of full
+// decomposition and [WithUnconstrainedOutputs] option is not used, then the
+// conversion functions will generate an unsatisfiable constraint.
+//
+// If nbDigits is larger than the bitlength of the modulus, then the returned
+// slice has length nbDigits with excess bits being 0.
+//
+// If WithNbDigits option is not set, then the full decomposition is returned.
 func WithNbDigits(nbDigits int) BaseConversionOption {
 	return func(opt *baseConversionConfig) error {
 		if nbDigits <= 0 {
 			return errors.New("nbDigits <= 0")
 		}
@@ -90,5 +98,23 @@ func WithUnconstrainedInputs() BaseConversionOption {
 	return func(opt *baseConversionConfig) error {
 		opt.UnconstrainedInputs = true
 		return nil
 	}
 }
+
+// OmitModulusCheck omits the comparison against native field modulus in
+// case the bitlength of the decomposed value (if [WithNbDigits] not set or set
+// to bitlength of the native modulus) eqals bitlength of the modulus.
+//
+// The check is otherwise required as there are possibly multiple correct binary
+// decompositions. For example, when decomposing small a the decomposition could
+// return the slices for both a or a+r, where r is the native modulus and the
+// enforced constraints are correct due to implicit modular reduction by r.
+//
+// This option can be used in case the decomposed output is manually checked to
+// be unique or if uniqueness is not required.
+func OmitModulusCheck() BaseConversionOption {
+	return func(opt *baseConversionConfig) error {
+		opt.omitModulusCheck = true
+		return nil
+	}
+}
diff --git a/std/math/bits/conversion_binary.go b/std/math/bits/conversion_binary.go
index 693f477b..55060e5a 100644
--- a/std/math/bits/conversion_binary.go
+++ b/std/math/bits/conversion_binary.go
@@ -54,16 +54,28 @@ func toBinary(api frontend.API, v frontend.Variable, opts ...BaseConversionOptio
 		if err := o(&cfg); err != nil {
 			panic(err)
 		}
 	}
 
+	// by default we also check that the value to be decomposed is less than the
+	// modulus. However, we can omit the check when the number of bits we want
+	// to decompose to is less than the modulus or it was strictly requested.
+	omitReducednessCheck := cfg.omitModulusCheck || cfg.NbDigits < api.Compiler().FieldBitLen()
+
 	// when cfg.NbDigits == 1, v itself has to be a binary digit. This if clause
 	// saves one constraint.
 	if cfg.NbDigits == 1 {
 		api.AssertIsBoolean(v)
 		return []frontend.Variable{v}
 	}
+	// if we decompose into more bits than fieldbitlen then the rest would be
+	// always zeros. Reduce the always-zeros to have fewer edge-cases elsewhere.
+	var paddingBits int
+	if cfg.NbDigits > api.Compiler().FieldBitLen() {
+		paddingBits = cfg.NbDigits - api.Compiler().FieldBitLen()
+		cfg.NbDigits = api.Compiler().FieldBitLen()
+	}
 
 	c := big.NewInt(1)
 
 	bits, err := api.Compiler().NewHint(nBits, cfg.NbDigits, v)
 	if err != nil {
@@ -80,8 +92,23 @@ func toBinary(api frontend.API, v frontend.Variable, opts ...BaseConversionOptio
 		}
 	}
 
 	// record the constraint Σ (2**i * b[i]) == a
 	api.AssertIsEqual(Σbi, v)
+	if !omitReducednessCheck {
+		if cmper, ok := api.Compiler().(bitsComparatorConstant); ok {
+			bound := new(big.Int).Sub(api.Compiler().Field(), big.NewInt(1))
+			cmper.MustBeLessOrEqCst(bits, api.Compiler().Field(), bound)
+		} else {
+			panic("builder does not expose comparison to constant")
+		}
+	}
+
+	// restore the zero bits which exceed the field bit-length when requested by
+	// setting WithNbDigits larger than the field bitlength.
+	bits = append(bits, make([]frontend.Variable, paddingBits)...)
+	for i := cfg.NbDigits; i < len(bits); i++ {
+		bits[i] = 0 // frontend.Variable is interface{}, we get nil pointer err if trying to access it.
+	}
 
 	return bits
 }
diff --git a/std/math/bits/intf_constcheck.go b/std/math/bits/intf_constcheck.go
new file mode 100644
index 00000000..44def042
--- /dev/null
+++ b/std/math/bits/intf_constcheck.go
@@ -0,0 +1,14 @@
+package bits
+
+import (
+	"math/big"
+
+	"github.com/consensys/gnark/frontend"
+)
+
+// bitsComparatorConstant allows to use the built-in comparison against a
+// constant bound. We use the direct implementation due to the added efficiency
+// of directly creating constraints instead of using API.
+type bitsComparatorConstant interface {
+	MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable)
+}
diff --git a/test/engine.go b/test/engine.go
index 6028cf0b..d62c6924 100644
--- a/test/engine.go
+++ b/test/engine.go
@@ -736,5 +736,29 @@ func (e *engine) ToCanonicalVariable(v frontend.Variable) frontend.CanonicalVari
 }
 
 func (e *engine) SetGkrInfo(info constraint.GkrInfo) error {
 	return fmt.Errorf("not implemented")
 }
+
+// MustBeLessOrEqCst implements method comparing value given by its bits aBits
+// to a bound.
+func (e *engine) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
+	v := new(big.Int)
+	for i, b := range aBits {
+		bb, ok := b.(*big.Int)
+		if !ok {
+			panic("not big.Int bit")
+		}
+		if !bb.IsUint64() {
+			panic("given bit large")
+		}
+		bbu := uint(bb.Uint64())
+		if bbu > 1 {
+			fmt.Println(bbu)
+			panic("given bit is not a bit")
+		}
+		v.SetBit(v, i, bbu)
+	}
+	if v.Cmp(bound) > 0 {
+		panic(fmt.Sprintf("%d > %d", v, bound))
+	}
+}

Vulnerable code: 	// Cmp returns 1 if i1>i2, 0 if i1=i2, -1 if i1<i2
	// AssertIsLessOrEqual fails if  v > bound
	"github.com/consensys/gnark/internal/utils"
	vars, _ := builder.toVariables(i1, i2)
	bi1 := builder.ToBinary(vars[0], builder.cs.FieldBitLen())
	bi2 := builder.ToBinary(vars[1], builder.cs.FieldBitLen())
		vv := builder.toVariable(v)
		builder.mustBeLessOrEqCst(vv, builder.cs.ToBigInt(cb))
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
	boundBits := builder.ToBinary(bound, nbBits)
func (builder *builder) mustBeLessOrEqCst(a expr.LinearExpression, bound *big.Int) {
	debug := builder.newDebugInfo("mustBeLessOrEq", a, " <= ", builder.toVariable(bound))

	// note that at this stage, we didn't boolean-constraint these new variables yet
	// (as opposed to ToBinary)
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
	bi1 := builder.ToBinary(i1, builder.cs.FieldBitLen())
	bi2 := builder.ToBinary(i2, builder.cs.FieldBitLen())
	"github.com/consensys/gnark/internal/utils"
	switch b := bound.(type) {
	case expr.Term:
	default:
		builder.mustBeLessOrEqCst(v, utils.FromInterface(b))
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
	boundBits := builder.ToBinary(bound, nbBits)
func (builder *builder) mustBeLessOrEqCst(a frontend.Variable, bound big.Int) {
	if ca, ok := builder.constantValue(a); ok {
		// a is constant, compare the big int values
		ba := builder.cs.ToBigInt(ca)
		if ba.Cmp(&bound) == 1 {
			panic(fmt.Sprintf("AssertIsLessOrEqual: %s > %s", ba.String(), bound.String()))
		}
	}

	debug := builder.newDebugInfo("mustBeLessOrEq", a, " <= ", bound)

	// note that at this stage, we didn't boolean-constraint these new variables yet
	// (as opposed to ToBinary)
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
	bits := api.ToBinary(linearExpression, 10)
// WithNbDigits sets the resulting number of digits (nbDigits) to be used in the base conversion.
// nbDigits must be > 0. If nbDigits is lower than the length of full decomposition and
// WithUnconstrainedOutputs option is not used, then the conversion functions will generate an
// unsatisfiable constraint. If WithNbDigits option is not set, then the full decomposition is
// returned.
Fixed code: 	// Cmp returns:
	//  * 1 if i1>i2,
	//  * 0 if i1=i2,
	//  * -1 if i1<i2.
	//
	// If the absolute difference between the variables i1 and i2 is known, then
	// it is more efficient to use the bounded methdods in package
	// [github.com/consensys/gnark/std/math/bits].
	// AssertIsLessOrEqual fails if v > bound.
	//
	// If the absolute difference between the variables b and bound is known, then
	// it is more efficient to use the bounded methdods in package
	// [github.com/consensys/gnark/std/math/bits].
	"github.com/consensys/gnark/internal/utils"

	nbBits := builder.cs.FieldBitLen()
	// in AssertIsLessOrEq we omitted comparison against modulus for the left
	// side as if `a+r<b` implies `a<b`, then here we compute the inequality
	// directly.
	bi1 := bits.ToBinary(builder, i1, bits.WithNbDigits(nbBits))
	bi2 := bits.ToBinary(builder, i2, bits.WithNbDigits(nbBits))
	nbBits := builder.cs.FieldBitLen()
	vBits := bits.ToBinary(builder, v, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())

		builder.MustBeLessOrEqCst(vBits, builder.cs.ToBigInt(cb), v)
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs(), bits.OmitModulusCheck())
	boundBits := bits.ToBinary(builder, bound, bits.WithNbDigits(nbBits))
// MustBeLessOrEqCst asserts that value represented using its bit decomposition
// aBits is less or equal than constant bound. The method boolean constraints
// the bits in aBits, so the caller can provide unconstrained bits.
func (builder *builder) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
	if len(aBits) > nbBits {
		panic("more input bits than field bit length")
	}
	for i := len(aBits); i < nbBits; i++ {
		aBits = append(aBits, 0)
	}
	debug := builder.newDebugInfo("mustBeLessOrEq", aForDebug, " <= ", builder.toVariable(bound))
	nbBits := builder.cs.FieldBitLen()
	// in AssertIsLessOrEq we omitted comparison against modulus for the left
	// side as if `a+r<b` implies `a<b`, then here we compute the inequality
	// directly.
	bi1 := bits.ToBinary(builder, i1, bits.WithNbDigits(nbBits))
	bi2 := bits.ToBinary(builder, i2, bits.WithNbDigits(nbBits))
	cv, vConst := builder.constantValue(v)
	cb, bConst := builder.constantValue(bound)

	// both inputs are constants
	if vConst && bConst {
		bv, bb := builder.cs.ToBigInt(cv), builder.cs.ToBigInt(cb)
		if bv.Cmp(bb) == 1 {
			panic(fmt.Sprintf("AssertIsLessOrEqual: %s > %s", bv.String(), bb.String()))
		}
	}

	nbBits := builder.cs.FieldBitLen()
	vBits := bits.ToBinary(builder, v, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())

	// bound is constant
	if bConst {
		builder.MustBeLessOrEqCst(vBits, builder.cs.ToBigInt(cb), v)
		return
	}

	if b, ok := bound.(expr.Term); ok {
	} else {
		panic(fmt.Sprintf("expected bound type expr.Term, got %T", bound))
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs(), bits.OmitModulusCheck())
	boundBits := bits.ToBinary(builder, bound, bits.WithNbDigits(nbBits)) // enforces range check against modulus
// MustBeLessOrEqCst asserts that value represented using its bit decomposition
// aBits is less or equal than constant bound. The method boolean constraints
// the bits in aBits, so the caller can provide unconstrained bits.
func (builder *builder) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
	if len(aBits) > nbBits {
		panic("more input bits than field bit length")
	}
	for i := len(aBits); i < nbBits; i++ {
		aBits = append(aBits, 0)
	}
	debug := builder.newDebugInfo("mustBeLessOrEq", aForDebug, " <= ", bound)
	bits := api.ToBinary(linearExpression, 6)
// Package regressiontests includes tests to avoid re-introducing regressions.
package regressiontests
package regressiontests

import (
	"fmt"
	"math/big"
	"testing"

	"github.com/consensys/gnark/constraint/solver"
	"github.com/consensys/gnark/frontend"
	"github.com/consensys/gnark/std/math/cmp"
	"github.com/consensys/gnark/test"
)

type CmpCircuit struct {
	Left      frontend.Variable
	Right     frontend.Variable
	ExpCmpRes frontend.Variable
}

func (c *CmpCircuit) Define(api frontend.API) error {
	r := api.Cmp(c.Left, c.Right)
	api.AssertIsEqual(r, c.ExpCmpRes)
	return nil
}

type AssertIsLessOrEqCircuit struct {
	Smaller, Bigger frontend.Variable
}

func (c *AssertIsLessOrEqCircuit) Define(api frontend.API) error {
	api.AssertIsLessOrEqual(c.Smaller, c.Bigger)
	return nil
}

type MathCmpAssertIsLessOrEqCircuitBounded struct {
	Left  frontend.Variable
	Right frontend.Variable
}

func (c *MathCmpAssertIsLessOrEqCircuitBounded) Define(api frontend.API) error {
	cmper := cmp.NewBoundedComparator(api, big.NewInt(6), false)
	cmper.AssertIsLessEq(c.Left, c.Right)
	return nil
}

type MathCmpAssertIsLessOrEqCircuitFull struct {
	Left  frontend.Variable
	Right frontend.Variable
}

func (c *MathCmpAssertIsLessOrEqCircuitFull) Define(api frontend.API) error {
	api.AssertIsEqual(1, cmp.IsLessOrEqual(api, c.Left, c.Right))
	return nil
}

func getNBitsHint() (solver.HintID, error) {
	for _, v := range solver.GetRegisteredHints() {
		if solver.GetHintName(v) == "github.com/consensys/gnark/std/math/bits.nBits" {
			return solver.GetHintID(v), nil
		}
	}
	return 0, fmt.Errorf("nBits hint not found")
}

func TestIssue836Cmp(t *testing.T) {
	assert := test.NewAssert(t)
	assignmentNoHintGood := CmpCircuit{
		Left:      10,
		Right:     5,
		ExpCmpRes: 1,
	}
	assignmentNoHintBad := CmpCircuit{
		Left:      5,
		Right:     10,
		ExpCmpRes: 1,
	}
	assignmentHintBad := CmpCircuit{
		Left:      10,
		Right:     5,
		ExpCmpRes: -1,
	}
	toReplaceHint, err := getNBitsHint()
	if err != nil {
		t.Fatalf("couldn't find hint to replace: %v", err)
	}
	assert.CheckCircuit(&CmpCircuit{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
	assert.CheckCircuit(&CmpCircuit{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
}

func TestIssue836AssertIsLess(t *testing.T) {
	assert := test.NewAssert(t)
	assignmentNoHintGood := AssertIsLessOrEqCircuit{
		Smaller: 5,
		Bigger:  10,
	}
	assignmentNoHintBad := AssertIsLessOrEqCircuit{
		Smaller: 11,
		Bigger:  10,
	}
	assignmentHintBad := AssertIsLessOrEqCircuit{
		Smaller: 10,
		Bigger:  5,
	}
	toReplaceHint, err := getNBitsHint()
	if err != nil {
		t.Fatalf("couldn't find hint to replace: %v", err)
	}
	assert.CheckCircuit(&AssertIsLessOrEqCircuit{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
	assert.CheckCircuit(&AssertIsLessOrEqCircuit{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
}

func TestIssue836MathCmpAssertIsLessEqBounded(t *testing.T) {
	assert := test.NewAssert(t)
	assignmentNoHintGood := MathCmpAssertIsLessOrEqCircuitBounded{
		Left:  5,
		Right: 10,
	}
	assignmentNoHintBad := MathCmpAssertIsLessOrEqCircuitBounded{
		Left:  11,
		Right: 10,
	}
	assignmentHintBad := MathCmpAssertIsLessOrEqCircuitBounded{
		Left:  10,
		Right: 5,
	}
	toReplaceHint, err := getNBitsHint()
	if err != nil {
		t.Fatalf("couldn't find hint to replace: %v", err)
	}
	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitBounded{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitBounded{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
}

func TestIssueXXXMathCmpAssertIsLessEqFull(t *testing.T) {
	assert := test.NewAssert(t)
	assignmentNoHintGood := MathCmpAssertIsLessOrEqCircuitFull{
		Left:  5,
		Right: 10,
	}
	assignmentNoHintBad := MathCmpAssertIsLessOrEqCircuitFull{
		Left:  11,
		Right: 10,
	}
	assignmentHintBad := MathCmpAssertIsLessOrEqCircuitFull{
		Left:  10,
		Right: 5,
	}
	toReplaceHint, err := getNBitsHint()
	if err != nil {
		t.Fatalf("couldn't find hint to replace: %v", err)
	}
	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitFull{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitFull{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
}

func maliciousNbitsHint(mod *big.Int, inputs []*big.Int, results []*big.Int) error {
	n := inputs[0]
	// This is a malicious hint. If n is less equal than 5, then add the
	// modulus. This creates a non-unique binary decomposition of the value.
	if n.Cmp(big.NewInt(5)) <= 0 {
		n = n.Add(n, mod)
	}
	for i := 0; i < len(results); i++ {
		results[i].SetUint64(uint64(n.Bit(i)))
	}
	return nil
}

	omitModulusCheck bool
// WithNbDigits sets the resulting number of digits (nbDigits) to be used in the
// base conversion.
//
// nbDigits must be > 0. If nbDigits is lower than the length of full
// decomposition and [WithUnconstrainedOutputs] option is not used, then the
// conversion functions will generate an unsatisfiable constraint.
//
// If nbDigits is larger than the bitlength of the modulus, then the returned
// slice has length nbDigits with excess bits being 0.
//
// If WithNbDigits option is not set, then the full decomposition is returned.

// OmitModulusCheck omits the comparison against native field modulus in
// case the bitlength of the decomposed value (if [WithNbDigits] not set or set
// to bitlength of the native modulus) eqals bitlength of the modulus.
//
// The check is otherwise required as there are possibly multiple correct binary
// decompositions. For example, when decomposing small a the decomposition could
// return the slices for both a or a+r, where r is the native modulus and the
// enforced constraints are correct due to implicit modular reduction by r.
//
// This option can be used in case the decomposed output is manually checked to
// be unique or if uniqueness is not required.
func OmitModulusCheck() BaseConversionOption {
	return func(opt *baseConversionConfig) error {
		opt.omitModulusCheck = true
		return nil
	}
}
	// by default we also check that the value to be decomposed is less than the
	// modulus. However, we can omit the check when the number of bits we want
	// to decompose to is less than the modulus or it was strictly requested.
	omitReducednessCheck := cfg.omitModulusCheck || cfg.NbDigits < api.Compiler().FieldBitLen()

	// if we decompose into more bits than fieldbitlen then the rest would be
	// always zeros. Reduce the always-zeros to have fewer edge-cases elsewhere.
	var paddingBits int
	if cfg.NbDigits > api.Compiler().FieldBitLen() {
		paddingBits = cfg.NbDigits - api.Compiler().FieldBitLen()
		cfg.NbDigits = api.Compiler().FieldBitLen()
	}
	if !omitReducednessCheck {
		if cmper, ok := api.Compiler().(bitsComparatorConstant); ok {
			bound := new(big.Int).Sub(api.Compiler().Field(), big.NewInt(1))
			cmper.MustBeLessOrEqCst(bits, api.Compiler().Field(), bound)
		} else {
			panic("builder does not expose comparison to constant")
		}
	}

	// restore the zero bits which exceed the field bit-length when requested by
	// setting WithNbDigits larger than the field bitlength.
	bits = append(bits, make([]frontend.Variable, paddingBits)...)
	for i := cfg.NbDigits; i < len(bits); i++ {
		bits[i] = 0 // frontend.Variable is interface{}, we get nil pointer err if trying to access it.
	}
package bits

import (
	"math/big"

	"github.com/consensys/gnark/frontend"
)

// bitsComparatorConstant allows to use the built-in comparison against a
// constant bound. We use the direct implementation due to the added efficiency
// of directly creating constraints instead of using API.
type bitsComparatorConstant interface {
	MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable)
}

// MustBeLessOrEqCst implements method comparing value given by its bits aBits
// to a bound.
func (e *engine) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
	v := new(big.Int)
	for i, b := range aBits {
		bb, ok := b.(*big.Int)
		if !ok {
			panic("not big.Int bit")
		}
		if !bb.IsUint64() {
			panic("given bit large")
		}
		bbu := uint(bb.Uint64())
		if bbu > 1 {
			fmt.Println(bbu)
			panic("given bit is not a bit")
		}
		v.SetBit(v, i, bbu)
	}
	if v.Cmp(bound) > 0 {
		panic(fmt.Sprintf("%d > %d", v, bound))
	}
}