From 3e3b1c632bb37a915ddba32afc0e50ccb2f74c76 Mon Sep 17 00:00:00 2001 From: Thomas Piellard Date: Fri, 7 Jan 2022 19:50:08 +0100 Subject: [PATCH] feat: addition of Cmp in the API --- frontend/api.go | 9 +- frontend/cs/plonk/api.go | 26 +++ frontend/cs/r1cs/api.go | 279 +++++++++++++++++-------------- integration_test.go | 1 + internal/backend/circuits/cmp.go | 59 +++++++ test/engine.go | 7 + 6 files changed, 257 insertions(+), 124 deletions(-) create mode 100644 internal/backend/circuits/cmp.go diff --git a/frontend/api.go b/frontend/api.go index 38bd3d5aeb..bc34ea6202 100644 --- a/frontend/api.go +++ b/frontend/api.go @@ -32,12 +32,12 @@ type API interface { // Add returns res = i1+i2+...in Add(i1, i2 Variable, in ...Variable) Variable - // Sub returns res = i1 - i2 - ...in - Sub(i1, i2 Variable, in ...Variable) Variable - // Neg returns -i Neg(i1 Variable) Variable + // Sub returns res = i1 - i2 - ...in + Sub(i1, i2 Variable, in ...Variable) Variable + // Mul returns res = i1 * i2 * ... in Mul(i1, i2 Variable, in ...Variable) Variable @@ -89,6 +89,9 @@ type API interface { // 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 i1i2, 0 if i1=i2, -1 if i1= 0; i-- { + + iszeroi1 := system.IsZero(bi1[i]) + iszeroi2 := system.IsZero(bi2[i]) + + i1i2 := system.And(bi1[i], iszeroi2) + i2i1 := system.And(bi2[i], iszeroi1) + + n := system.Select(i2i1, -1, 0) + m := system.Select(i1i2, 1, n) + + res = system.Select(system.IsZero(res), m, res) + + } + return res +} + // Println behaves like fmt.Println but accepts Variable as parameter // whose value will be resolved at runtime when computed by the solver // Println enables circuit debugging and behaves almost like fmt.Println() diff --git a/frontend/cs/r1cs/api.go b/frontend/cs/r1cs/api.go index ed4325b9c6..4788b8f875 100644 --- a/frontend/cs/r1cs/api.go +++ b/frontend/cs/r1cs/api.go @@ -33,6 +33,9 @@ import ( "github.com/consensys/gnark/internal/utils" ) +// --------------------------------------------------------------------------------------------- +// Arithmetic + // Add returns res = i1+i2+...in func (system *r1CS) Add(i1, i2 frontend.Variable, in ...frontend.Variable) frontend.Variable { @@ -163,32 +166,7 @@ func (system *r1CS) mulConstant(v1, constant compiled.Variable) compiled.Variabl return res } -// Inverse returns res = inverse(v) -func (system *r1CS) Inverse(i1 frontend.Variable) frontend.Variable { - vars, _ := system.toVariables(i1) - - if vars[0].IsConstant() { - // c := vars[0].constantValue(cs) - c := system.constantValue(vars[0]) - if c.IsUint64() && c.Uint64() == 0 { - panic("inverse by constant(0)") - } - - c.ModInverse(c, system.CurveID.Info().Fr.Modulus()) - return system.constant(c) - } - - // allocate resulting frontend.Variable - res := system.newInternalVariable() - - debug := system.AddDebugInfo("inverse", vars[0], "*", res, " == 1") - system.addConstraint(newR1C(res, vars[0], system.one()), debug) - - return res -} - -// Div returns res = i1 / i2 -func (system *r1CS) Div(i1, i2 frontend.Variable) frontend.Variable { +func (system *r1CS) DivUnchecked(i1, i2 frontend.Variable) frontend.Variable { vars, _ := system.toVariables(i1, i2) v1 := vars[0] @@ -197,10 +175,8 @@ func (system *r1CS) Div(i1, i2 frontend.Variable) frontend.Variable { if !v2.IsConstant() { res := system.newInternalVariable() debug := system.AddDebugInfo("div", v1, "/", v2, " == ", res) - v2Inv := system.newInternalVariable() - // note that here we ensure that v2 can't be 0, but it costs us one extra constraint - system.addConstraint(newR1C(v2, v2Inv, system.one()), debug) - system.addConstraint(newR1C(v1, v2Inv, res), debug) + // note that here we don't ensure that divisor is != 0 + system.addConstraint(newR1C(v2, res, v1), debug) return res } @@ -221,7 +197,8 @@ func (system *r1CS) Div(i1, i2 frontend.Variable) frontend.Variable { return system.mulConstant(v1, system.constant(b2).(compiled.Variable)) } -func (system *r1CS) DivUnchecked(i1, i2 frontend.Variable) frontend.Variable { +// Div returns res = i1 / i2 +func (system *r1CS) Div(i1, i2 frontend.Variable) frontend.Variable { vars, _ := system.toVariables(i1, i2) v1 := vars[0] @@ -230,8 +207,10 @@ func (system *r1CS) DivUnchecked(i1, i2 frontend.Variable) frontend.Variable { if !v2.IsConstant() { res := system.newInternalVariable() debug := system.AddDebugInfo("div", v1, "/", v2, " == ", res) - // note that here we don't ensure that divisor is != 0 - system.addConstraint(newR1C(v2, res, v1), debug) + v2Inv := system.newInternalVariable() + // note that here we ensure that v2 can't be 0, but it costs us one extra constraint + system.addConstraint(newR1C(v2, v2Inv, system.one()), debug) + system.addConstraint(newR1C(v1, v2Inv, res), debug) return res } @@ -252,103 +231,32 @@ func (system *r1CS) DivUnchecked(i1, i2 frontend.Variable) frontend.Variable { return system.mulConstant(v1, system.constant(b2).(compiled.Variable)) } -// Xor compute the XOR between two frontend.Variables -func (system *r1CS) Xor(_a, _b frontend.Variable) frontend.Variable { - - vars, _ := system.toVariables(_a, _b) - - a := vars[0] - b := vars[1] - - system.AssertIsBoolean(a) - system.AssertIsBoolean(b) - - // the formulation used is for easing up the conversion to sparse r1cs - res := system.newInternalVariable() - res.IsBoolean = new(bool) - *res.IsBoolean = true - c := system.Neg(res).(compiled.Variable) - c.IsBoolean = new(bool) - *c.IsBoolean = false - c.LinExp = append(c.LinExp, a.LinExp[0], b.LinExp[0]) - aa := system.Mul(a, 2) - system.Constraints = append(system.Constraints, newR1C(aa, b, c)) - - return res -} - -// Or compute the OR between two frontend.Variables -func (system *r1CS) Or(_a, _b frontend.Variable) frontend.Variable { - vars, _ := system.toVariables(_a, _b) +// Inverse returns res = inverse(v) +func (system *r1CS) Inverse(i1 frontend.Variable) frontend.Variable { + vars, _ := system.toVariables(i1) - a := vars[0] - b := vars[1] + if vars[0].IsConstant() { + // c := vars[0].constantValue(cs) + c := system.constantValue(vars[0]) + if c.IsUint64() && c.Uint64() == 0 { + panic("inverse by constant(0)") + } - system.AssertIsBoolean(a) - system.AssertIsBoolean(b) + c.ModInverse(c, system.CurveID.Info().Fr.Modulus()) + return system.constant(c) + } - // the formulation used is for easing up the conversion to sparse r1cs + // allocate resulting frontend.Variable res := system.newInternalVariable() - res.IsBoolean = new(bool) - *res.IsBoolean = true - c := system.Neg(res).(compiled.Variable) - c.IsBoolean = new(bool) - *c.IsBoolean = false - c.LinExp = append(c.LinExp, a.LinExp[0], b.LinExp[0]) - system.Constraints = append(system.Constraints, newR1C(a, b, c)) - - return res -} - -// And compute the AND between two frontend.Variables -func (system *r1CS) And(_a, _b frontend.Variable) frontend.Variable { - vars, _ := system.toVariables(_a, _b) - - a := vars[0] - b := vars[1] - - system.AssertIsBoolean(a) - system.AssertIsBoolean(b) - res := system.Mul(a, b) + debug := system.AddDebugInfo("inverse", vars[0], "*", res, " == 1") + system.addConstraint(newR1C(res, vars[0], system.one()), debug) return res } -// IsZero returns 1 if i1 is zero, 0 otherwise -func (system *r1CS) IsZero(i1 frontend.Variable) frontend.Variable { - vars, _ := system.toVariables(i1) - a := vars[0] - if a.IsConstant() { - // c := a.constantValue(cs) - c := system.constantValue(a) - if c.IsUint64() && c.Uint64() == 0 { - return system.constant(1) - } - return system.constant(0) - } - - debug := system.AddDebugInfo("isZero", a) - - //m * (1 - m) = 0 // constrain m to be 0 or 1 - // a * m = 0 // constrain m to be 0 if a != 0 - // _ = inverse(m + a) // constrain m to be 1 if a == 0 - - // m is computed by the solver such that m = 1 - a^(modulus - 1) - res, err := system.NewHint(hint.IsZero, a) - if err != nil { - // the function errs only if the number of inputs is invalid. - panic(err) - } - m := res[0] - system.addConstraint(newR1C(a, m, system.constant(0)), debug) - - system.AssertIsBoolean(m) - ma := system.Add(m, a) - _ = system.Inverse(ma) - return m - -} +// --------------------------------------------------------------------------------------------- +// Bit operations // ToBinary unpacks a frontend.Variable in binary, // n is the number of bits to select (starting from lsb) @@ -463,6 +371,72 @@ func (system *r1CS) FromBinary(_b ...frontend.Variable) frontend.Variable { return res } +// Xor compute the XOR between two frontend.Variables +func (system *r1CS) Xor(_a, _b frontend.Variable) frontend.Variable { + + vars, _ := system.toVariables(_a, _b) + + a := vars[0] + b := vars[1] + + system.AssertIsBoolean(a) + system.AssertIsBoolean(b) + + // the formulation used is for easing up the conversion to sparse r1cs + res := system.newInternalVariable() + res.IsBoolean = new(bool) + *res.IsBoolean = true + c := system.Neg(res).(compiled.Variable) + c.IsBoolean = new(bool) + *c.IsBoolean = false + c.LinExp = append(c.LinExp, a.LinExp[0], b.LinExp[0]) + aa := system.Mul(a, 2) + system.Constraints = append(system.Constraints, newR1C(aa, b, c)) + + return res +} + +// Or compute the OR between two frontend.Variables +func (system *r1CS) Or(_a, _b frontend.Variable) frontend.Variable { + vars, _ := system.toVariables(_a, _b) + + a := vars[0] + b := vars[1] + + system.AssertIsBoolean(a) + system.AssertIsBoolean(b) + + // the formulation used is for easing up the conversion to sparse r1cs + res := system.newInternalVariable() + res.IsBoolean = new(bool) + *res.IsBoolean = true + c := system.Neg(res).(compiled.Variable) + c.IsBoolean = new(bool) + *c.IsBoolean = false + c.LinExp = append(c.LinExp, a.LinExp[0], b.LinExp[0]) + system.Constraints = append(system.Constraints, newR1C(a, b, c)) + + return res +} + +// And compute the AND between two frontend.Variables +func (system *r1CS) And(_a, _b frontend.Variable) frontend.Variable { + vars, _ := system.toVariables(_a, _b) + + a := vars[0] + b := vars[1] + + system.AssertIsBoolean(a) + system.AssertIsBoolean(b) + + res := system.Mul(a, b) + + return res +} + +// --------------------------------------------------------------------------------------------- +// Conditionals + // Select if i0 is true, yields i1 else yields i2 func (system *r1CS) Select(i0, i1, i2 frontend.Variable) frontend.Variable { @@ -529,6 +503,69 @@ func (system *r1CS) Lookup2(b0, b1 frontend.Variable, i0, i1, i2, i3 frontend.Va return res } +// IsZero returns 1 if i1 is zero, 0 otherwise +func (system *r1CS) IsZero(i1 frontend.Variable) frontend.Variable { + vars, _ := system.toVariables(i1) + a := vars[0] + if a.IsConstant() { + // c := a.constantValue(cs) + c := system.constantValue(a) + if c.IsUint64() && c.Uint64() == 0 { + return system.constant(1) + } + return system.constant(0) + } + + debug := system.AddDebugInfo("isZero", a) + + //m * (1 - m) = 0 // constrain m to be 0 or 1 + // a * m = 0 // constrain m to be 0 if a != 0 + // _ = inverse(m + a) // constrain m to be 1 if a == 0 + + // m is computed by the solver such that m = 1 - a^(modulus - 1) + res, err := system.NewHint(hint.IsZero, a) + if err != nil { + // the function errs only if the number of inputs is invalid. + panic(err) + } + m := res[0] + system.addConstraint(newR1C(a, m, system.constant(0)), debug) + + system.AssertIsBoolean(m) + ma := system.Add(m, a) + _ = system.Inverse(ma) + return m +} + +// Cmp returns 1 if i1>i2, 0 if i1=i2, -1 if i1= 0; i-- { + + iszeroi1 := system.IsZero(bi1[i]) + iszeroi2 := system.IsZero(bi2[i]) + + i1i2 := system.And(bi1[i], iszeroi2) + i2i1 := system.And(bi2[i], iszeroi1) + + n := system.Select(i2i1, -1, 0) + m := system.Select(i1i2, 1, n) + + res = system.Select(system.IsZero(res), m, res) + + } + return res +} + +// --------------------------------------------------------------------------------------------- +// Assertions + // IsConstant returns true if v is a constant known at compile time func (system *r1CS) IsConstant(v frontend.Variable) bool { if _v, ok := v.(compiled.Variable); ok { diff --git a/integration_test.go b/integration_test.go index e0a13d7e4c..8a20ee246e 100644 --- a/integration_test.go +++ b/integration_test.go @@ -37,6 +37,7 @@ func TestIntegrationAPI(t *testing.T) { sort.Strings(keys) for i := range keys { + name := keys[i] tData := circuits.Circuits[name] assert.Run(func(assert *test.Assert) { diff --git a/internal/backend/circuits/cmp.go b/internal/backend/circuits/cmp.go new file mode 100644 index 0000000000..59f19419a7 --- /dev/null +++ b/internal/backend/circuits/cmp.go @@ -0,0 +1,59 @@ +package circuits + +import ( + "github.com/consensys/gnark-crypto/ecc" + "github.com/consensys/gnark/frontend" +) + +type cmpCircuit struct { + A frontend.Variable + B frontend.Variable `gnark:",public"` + R frontend.Variable +} + +func (circuit *cmpCircuit) Define(api frontend.API) error { + r := api.Cmp(circuit.A, circuit.B) + api.AssertIsEqual(r, circuit.R) + return nil +} + +func init() { + + good := []frontend.Circuit{ + &cmpCircuit{ + A: 12346, + B: 12345, + R: 1, + }, + &cmpCircuit{ + A: 12345, + B: 12346, + R: -1, + }, + &cmpCircuit{ + A: 12345, + B: 12345, + R: 0, + }, + } + + bad := []frontend.Circuit{ + &cmpCircuit{ + A: 12345, + B: 12346, + R: 1, + }, + &cmpCircuit{ + A: 12346, + B: 12345, + R: -1, + }, + &cmpCircuit{ + A: 12345, + B: 12345, + R: 1, + }, + } + + addNewEntry("cmp", &cmpCircuit{}, good, bad, []ecc.ID{ecc.BW6_761}) +} diff --git a/test/engine.go b/test/engine.go index 6f8399ad21..9469dedd06 100644 --- a/test/engine.go +++ b/test/engine.go @@ -266,6 +266,13 @@ func (e *engine) IsZero(i1 frontend.Variable) frontend.Variable { return (0) } +// Cmp returns 1 if i1>i2, 0 if i1==i2, -1 if i1