Skip to content

Commit

Permalink
fixes #1227: api.AssertIsLessOrEqual incorrect behavior on R1CS with …
Browse files Browse the repository at this point in the history
…constant variable (#1228)

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

* rename 1226 to 1227
  • Loading branch information
gbotrel authored Jul 26, 2024
1 parent d6d85d4 commit 70baf16
Show file tree
Hide file tree
Showing 3 changed files with 36 additions and 20 deletions.
28 changes: 11 additions & 17 deletions frontend/cs/r1cs/api_assertions.go
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand All @@ -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 {
Expand Down
4 changes: 1 addition & 3 deletions frontend/cs/r1cs/builder.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
24 changes: 24 additions & 0 deletions internal/regression_tests/issue1227/issue_1227_test.go
Original file line number Diff line number Diff line change
@@ -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
}

0 comments on commit 70baf16

Please sign in to comment.