From f08f0011800f610466539e578b3dbb49ef97ac3e Mon Sep 17 00:00:00 2001 From: Eagle941 <8973725+Eagle941@users.noreply.github.com> Date: Mon, 26 Jun 2023 18:04:05 +0100 Subject: [PATCH] feat: implemented gates and single entry point (#7) * Added Lean template. Implemented AssertIsDifferent * Added support for chained ops * Added du, neg, mac * Refactored Neg, MulAcc, Div, DivUnchecked, Inverse * Added Boolean gates and refactoring * Added lookup and select ops. Added support for callback format * Added cmp and le * Moved Lean files to other repo. Added function to create Proj array * Added ConstantValue implementation * Prototype single entry point * Added support for vector arguments * Added ToBinary and FromBinary. Improved panic messages * Fixed implicit parameter for from_binary. Added optional gate explicit type. * Refactored tests and added second example * Added field in code extractor * Fixed dependency file * Replaced Bit with F * Improved interface to initialise circuit * Added readme * Streamlined user API and using NewSchema to identify fields to initialise * Added support for nested arrays as circuit fields --- extractor/extractor.go | 110 ++++++++++----- extractor/extractor_test.go | 102 +++++++++++--- extractor/lean_export.go | 266 +++++++++++++++++++++++++++++++++--- go.mod | 6 +- readme.md | 19 +++ 5 files changed, 430 insertions(+), 73 deletions(-) create mode 100644 readme.md diff --git a/extractor/extractor.go b/extractor/extractor.go index 31ced67..f98dda8 100644 --- a/extractor/extractor.go +++ b/extractor/extractor.go @@ -2,10 +2,13 @@ package extractor import ( "fmt" - "github.com/consensys/gnark/backend/hint" - "github.com/consensys/gnark/frontend" "gnark-extractor/abstractor" "math/big" + "reflect" + + "github.com/consensys/gnark-crypto/ecc" + "github.com/consensys/gnark/backend/hint" + "github.com/consensys/gnark/frontend" ) type Operand interface { @@ -24,15 +27,19 @@ type Gate struct { func (_ Gate) isOperand() {} +// Input is used to save the position of the argument in the +// list of arguments of the circuit function. type Input struct { Index int } func (_ Input) isOperand() {} +// Index is the index to be accessed in the array +// Operand[Index] type Proj struct { - Index int Operand Operand + Index int } func (_ Proj) isOperand() {} @@ -46,18 +53,25 @@ type OpKind int const ( OpAdd OpKind = iota OpMulAcc - OpMul - OpNeg + OpNegative OpSub + OpMul OpDiv OpDivUnchecked OpInverse OpToBinary OpFromBinary OpXor - OpAnd OpOr + OpAnd + OpSelect + OpLookup + OpIsZero + OpCmp OpAssertEq + OpAssertNotEq + OpAssertIsBool + OpAssertLessEqual ) func (_ OpKind) isOp() {} @@ -91,14 +105,25 @@ func (g *ExGadget) Call(args ...frontend.Variable) []frontend.Variable { outs[0] = gate } else { for i := range g.Outputs { - outs[i] = Proj{i, gate} + outs[i] = Proj{gate, i} } } return outs } +type ExArgType struct { + Size int + Type *ExArgType +} + +type ExArg struct { + Name string + Kind reflect.Kind + Type ExArgType +} + type ExCircuit struct { - Inputs []string + Inputs []ExArg Gadgets []ExGadget Code []App } @@ -106,6 +131,11 @@ type ExCircuit struct { type CodeExtractor struct { Code []App Gadgets []ExGadget + Field ecc.ID +} + +func operandFromArray(arg []frontend.Variable) Operand { + return arg[0].(Proj).Operand } func sanitizeVars(args ...frontend.Variable) []Operand { @@ -119,8 +149,10 @@ func sanitizeVars(args ...frontend.Variable) []Operand { case big.Int: casted := arg.(big.Int) ops[i] = Const{&casted} + case []frontend.Variable: + ops[i] = operandFromArray(arg.([]frontend.Variable)) default: - fmt.Printf("invalid argument %#v\n", arg) + fmt.Printf("invalid argument of type %T\n%#v\n", arg, arg) panic("invalid argument") } } @@ -141,7 +173,7 @@ func (ce *CodeExtractor) MulAcc(a, b, c frontend.Variable) frontend.Variable { } func (ce *CodeExtractor) Neg(i1 frontend.Variable) frontend.Variable { - return ce.AddApp(OpNeg, i1, -1) + return ce.AddApp(OpNegative, i1) } func (ce *CodeExtractor) Sub(i1, i2 frontend.Variable, in ...frontend.Variable) frontend.Variable { @@ -165,12 +197,20 @@ func (ce *CodeExtractor) Inverse(i1 frontend.Variable) frontend.Variable { } func (ce *CodeExtractor) ToBinary(i1 frontend.Variable, n ...int) []frontend.Variable { - //TODO implement me - panic("implement me") + nbBits := ce.Field.ScalarField().BitLen() + if len(n) == 1 { + nbBits = n[0] + if nbBits < 0 { + panic("Number of bits in ToBinary must be > 0") + } + } + gate := ce.AddApp(OpToBinary, i1, nbBits) + return []frontend.Variable{gate} } func (ce *CodeExtractor) FromBinary(b ...frontend.Variable) frontend.Variable { - return ce.AddApp(OpFromBinary, b...) + // Packs in little-endian + return ce.AddApp(OpFromBinary, append([]frontend.Variable{}, b...)...) } func (ce *CodeExtractor) Xor(a, b frontend.Variable) frontend.Variable { @@ -186,23 +226,19 @@ func (ce *CodeExtractor) And(a, b frontend.Variable) frontend.Variable { } func (ce *CodeExtractor) Select(b frontend.Variable, i1, i2 frontend.Variable) frontend.Variable { - //TODO implement me - panic("implement me") + return ce.AddApp(OpSelect, b, i1, i2) } func (ce *CodeExtractor) Lookup2(b0, b1 frontend.Variable, i0, i1, i2, i3 frontend.Variable) frontend.Variable { - //TODO implement me - panic("implement me") + return ce.AddApp(OpLookup, b0, b1, i0, i1, i2, i3) } func (ce *CodeExtractor) IsZero(i1 frontend.Variable) frontend.Variable { - //TODO implement me - panic("implement me") + return ce.AddApp(OpIsZero, i1) } func (ce *CodeExtractor) Cmp(i1, i2 frontend.Variable) frontend.Variable { - //TODO implement me - panic("implement me") + return ce.AddApp(OpCmp, i1, i2) } func (ce *CodeExtractor) AssertIsEqual(i1, i2 frontend.Variable) { @@ -210,38 +246,48 @@ func (ce *CodeExtractor) AssertIsEqual(i1, i2 frontend.Variable) { } func (ce *CodeExtractor) AssertIsDifferent(i1, i2 frontend.Variable) { - //TODO implement me - panic("implement me") + ce.AddApp(OpAssertNotEq, i1, i2) } func (ce *CodeExtractor) AssertIsBoolean(i1 frontend.Variable) { - //TODO implement me - panic("implement me") + ce.AddApp(OpAssertIsBool, i1) } func (ce *CodeExtractor) AssertIsLessOrEqual(v frontend.Variable, bound frontend.Variable) { - //TODO implement me - panic("implement me") + ce.AddApp(OpAssertLessEqual, v, bound) } func (ce *CodeExtractor) Println(a ...frontend.Variable) { - //TODO implement me panic("implement me") } func (ce *CodeExtractor) Compiler() frontend.Compiler { - //TODO implement me panic("implement me") } func (ce *CodeExtractor) NewHint(f hint.Function, nbOutputs int, inputs ...frontend.Variable) ([]frontend.Variable, error) { - //TODO implement me panic("implement me") } func (ce *CodeExtractor) ConstantValue(v frontend.Variable) (*big.Int, bool) { - //TODO implement me - panic("implement me") + switch v.(type) { + case Const: + return v.(Const).Value, true + case Proj: + switch v.(Proj).Operand.(type) { + case Const: + return v.(Proj).Operand.(Const).Value, true + default: + return nil, false + } + case int64: + return big.NewInt(v.(int64)), true + case big.Int: + casted := v.(big.Int) + return &casted, true + default: + return nil, false + } } func (ce *CodeExtractor) DefineGadget(name string, arity int, constructor func(api abstractor.API, args ...frontend.Variable) []frontend.Variable) abstractor.Gadget { diff --git a/extractor/extractor_test.go b/extractor/extractor_test.go index 87ba85f..01f56b9 100644 --- a/extractor/extractor_test.go +++ b/extractor/extractor_test.go @@ -2,12 +2,80 @@ package extractor import ( "fmt" - "github.com/consensys/gnark/frontend" "gnark-extractor/abstractor" "testing" + + "github.com/consensys/gnark-crypto/ecc" + "github.com/consensys/gnark/frontend" ) -func defineExample(api abstractor.API) { +type CircuitWithParameter struct { + In frontend.Variable `gnark:",public"` + Param int +} + +func (circuit *CircuitWithParameter) AbsDefine(api abstractor.API) error { + api.AssertIsEqual(circuit.Param, circuit.In) + + return nil +} + +func (circuit CircuitWithParameter) Define(api frontend.API) error { + return abstractor.Concretize(api, &circuit) +} + +func TestCircuitWithParameter(t *testing.T) { + assignment := CircuitWithParameter{} + assignment.Param = 20 + err := CircuitToLean(&assignment, ecc.BW6_756) + if err != nil { + fmt.Println("CircuitToLean error!") + fmt.Println(err.Error()) + } +} + +type MerkleRecover struct { + Root frontend.Variable `gnark:",public"` + Element frontend.Variable `gnark:",public"` + Path [20]frontend.Variable `gnark:",secret"` + Proof [20]frontend.Variable `gnark:",secret"` +} + +func (circuit *MerkleRecover) AbsDefine(api abstractor.API) error { + hash := api.DefineGadget("hash", 2, func(api abstractor.API, args ...frontend.Variable) []frontend.Variable { + return []frontend.Variable{api.Mul(args[0], args[1])} + }) + + current := circuit.Element + for i := 0; i < len(circuit.Path); i++ { + leftHash := hash.Call(current, circuit.Proof[i])[0] + rightHash := hash.Call(circuit.Proof[i], current)[0] + current = api.Select(circuit.Path[i], rightHash, leftHash) + } + api.AssertIsEqual(current, circuit.Root) + + return nil +} + +func (circuit MerkleRecover) Define(api frontend.API) error { + return abstractor.Concretize(api, &circuit) +} + +func TestMerkleRecover(t *testing.T) { + assignment := MerkleRecover{} + err := CircuitToLean(&assignment, ecc.BW6_756) + if err != nil { + fmt.Println("CircuitToLean error!") + fmt.Println(err.Error()) + } +} + +type TwoGadgets struct { + In_1 frontend.Variable + In_2 frontend.Variable +} + +func (circuit *TwoGadgets) AbsDefine(api abstractor.API) error { my_widget := api.DefineGadget("my_widget", 2, func(api abstractor.API, args ...frontend.Variable) []frontend.Variable { sum := api.Add(args[0], args[1]) mul := api.Mul(args[0], args[1]) @@ -20,23 +88,23 @@ func defineExample(api abstractor.API) { r := api.Mul(mul, snd[0]) return []frontend.Variable{r} }) - i1 := Input{0} - i2 := Input{1} - sum := api.Add(i1, i2) - prod := api.Mul(i1, i2) + + sum := api.Add(circuit.In_1, circuit.In_2) + prod := api.Mul(circuit.In_1, circuit.In_2) my_snd_widget.Call(sum, prod) + + return nil } -func TestExtractor(t *testing.T) { - api := CodeExtractor{ - Code: []App{}, - Gadgets: []ExGadget{}, - } - defineExample(&api) - circuit := ExCircuit{ - Inputs: []string{"i1", "i2"}, - Gadgets: api.Gadgets, - Code: api.Code, +func (circuit TwoGadgets) Define(api frontend.API) error { + return abstractor.Concretize(api, &circuit) +} + +func TestTwoGadgets(t *testing.T) { + assignment := TwoGadgets{} + err := CircuitToLean(&assignment, ecc.BW6_756) + if err != nil { + fmt.Println("CircuitToLean error!") + fmt.Println(err.Error()) } - fmt.Println(ExportCircuit(circuit)) } diff --git a/extractor/lean_export.go b/extractor/lean_export.go index 03b82e8..3c0b4cc 100644 --- a/extractor/lean_export.go +++ b/extractor/lean_export.go @@ -2,7 +2,13 @@ package extractor import ( "fmt" + "gnark-extractor/abstractor" + "reflect" "strings" + + "github.com/consensys/gnark-crypto/ecc" + "github.com/consensys/gnark/frontend" + "github.com/consensys/gnark/frontend/schema" ) func ExportGadget(gadget ExGadget) string { @@ -10,9 +16,9 @@ func ExportGadget(gadget ExGadget) string { if len(gadget.Outputs) > 1 { kArgsType = fmt.Sprintf("Vect F %d", len(gadget.Outputs)) } - inAssignment := make([]string, gadget.Arity) + inAssignment := make([]ExArg, gadget.Arity) for i := 0; i < gadget.Arity; i++ { - inAssignment[i] = fmt.Sprintf("in_%d", i) + inAssignment[i] = ExArg{fmt.Sprintf("in_%d", i), reflect.Interface, ExArgType{1, nil}} } return fmt.Sprintf("def %s %s (k: %s -> Prop): Prop :=\n%s", gadget.Name, genArgs(inAssignment), kArgsType, genGadgetBody(inAssignment, gadget)) } @@ -26,10 +32,144 @@ func ExportCircuit(circuit ExCircuit) string { return fmt.Sprintf("%s\n\n%s", strings.Join(gadgets, "\n\n"), circ) } -func genArgs(inAssignment []string) string { +func ArrayInit(f schema.Field, v reflect.Value, op Operand) error { + for i := 0; i < f.ArraySize; i++ { + op := Proj{op, i} + switch len(f.SubFields) { + case 1: + ArrayInit(f.SubFields[0], v.Index(i), op) + case 0: + value := reflect.ValueOf(op) + v.Index(i).Set(value) + default: + panic("Only nested arrays supported in SubFields") + } + } + return nil +} + +func CircuitInit(class abstractor.Circuit, schema *schema.Schema) error { + // https://stackoverflow.com/a/49704408 + // https://stackoverflow.com/a/14162161 + // https://stackoverflow.com/a/63422049 + + // The purpose of this function is to initialise the + // struct fields with Operand interfaces for being + // processed by the Extractor. + v := reflect.ValueOf(class) + if v.Type().Kind() == reflect.Ptr { + ptr := v + v = ptr.Elem() + } else { + ptr := reflect.New(reflect.TypeOf(class)) + temp := ptr.Elem() + temp.Set(v) + } + + for j, f := range schema.Fields { + field_name := f.Name + field := v.FieldByName(field_name) + field_type := field.Type() + + // Can't assign an array to another array, therefore + // initialise each element in the array + if field_type.Kind() == reflect.Array || field_type.Kind() == reflect.Slice { + tmp_c := reflect.ValueOf(&class).Elem() + tmp := reflect.New(tmp_c.Elem().Type()).Elem() + tmp.Set(tmp_c.Elem()) + ArrayInit(f, tmp.Elem().FieldByName(field_name), Input{j}) + tmp_c.Set(tmp) + } else if field_type.Kind() == reflect.Interface { + init := Input{j} + value := reflect.ValueOf(init) + + tmp_c := reflect.ValueOf(&class).Elem() + tmp := reflect.New(tmp_c.Elem().Type()).Elem() + tmp.Set(tmp_c.Elem()) + tmp.Elem().FieldByName(field_name).Set(value) + tmp_c.Set(tmp) + } else { + fmt.Printf("Skipped type %s\n", field_type.Kind()) + } + } + return nil +} + +func KindOfField(a interface{}, s string) reflect.Kind { + v := reflect.ValueOf(a).Elem() + f := v.FieldByName(s) + return f.Kind() +} + +func CircuitArgs(field schema.Field) ExArgType { + // Handling only subfields which are nested arrays + switch len(field.SubFields) { + case 1: + subType := CircuitArgs(field.SubFields[0]) + return ExArgType{field.ArraySize, &subType} + case 0: + return ExArgType{field.ArraySize, nil} + default: + panic("Only nested arrays supported in SubFields") + } +} + +func CircuitToLean(circuit abstractor.Circuit, field ecc.ID) error { + schema, err := frontend.NewSchema(circuit) + if err != nil { + return err + } + + err = CircuitInit(circuit, schema) + if err != nil { + fmt.Println("CircuitInit error!") + fmt.Println(err.Error()) + } + + api := CodeExtractor{ + Code: []App{}, + Gadgets: []ExGadget{}, + Field: field, + } + + err = circuit.AbsDefine(&api) + if err != nil { + return err + } + + var circuitInputs []ExArg + for _, f := range schema.Fields { + kind := KindOfField(circuit, f.Name) + arg := ExArg{f.Name, kind, CircuitArgs(f)} + circuitInputs = append(circuitInputs, arg) + } + + extractorCircuit := ExCircuit{ + Inputs: circuitInputs, + Gadgets: api.Gadgets, + Code: api.Code, + } + fmt.Println(ExportCircuit(extractorCircuit)) + + return nil +} + +func genNestedArrays(a ExArgType) string { + if a.Type != nil { + return fmt.Sprintf("Vector (%s) %d", genNestedArrays(*a.Type), a.Size) + } + return fmt.Sprintf("Vector F %d", a.Size) +} + +func genArgs(inAssignment []ExArg) string { args := make([]string, len(inAssignment)) for i, in := range inAssignment { - args[i] = fmt.Sprintf("(%s: F)", in) + switch in.Kind { + case reflect.Array, reflect.Slice: + args[i] = fmt.Sprintf("(%s: %s)", in.Name, genNestedArrays(in.Type)) + default: + args[i] = fmt.Sprintf("(%s: F)", in.Name) + } } return strings.Join(args, " ") } @@ -70,7 +210,7 @@ func assignGateVars(code []App, additional ...Operand) []string { return gateVars } -func genGadgetCall(gateVar string, inAssignment []string, gateVars []string, gadget *ExGadget, args []Operand) string { +func genGadgetCall(gateVar string, inAssignment []ExArg, gateVars []string, gadget *ExGadget, args []Operand) string { name := gadget.Name operands := strings.Join(operandExprs(args, inAssignment, gateVars), " ") binder := "_" @@ -80,40 +220,121 @@ func genGadgetCall(gateVar string, inAssignment []string, gateVars []string, gad return fmt.Sprintf(" %s %s fun %s =>\n", name, operands, binder) } -func genOpCall(gateVar string, inAssignment []string, gateVars []string, op Op, args []Operand) string { +func genGateOp(op Op) string { name := "unknown" switch op { case OpAdd: name = "add" - case OpMul: - name = "mul" + case OpMulAcc: + name = "mul_acc" + case OpNegative: + name = "neg" case OpSub: name = "sub" + case OpMul: + name = "mul" + case OpDivUnchecked: + name = "div_unchecked" case OpDiv: name = "div" + case OpInverse: + name = "inv" + case OpXor: + name = "xor" + case OpOr: + name = "or" + case OpAnd: + name = "and" + case OpSelect: + name = "select" + case OpLookup: + name = "lookup" + case OpIsZero: + name = "is_zero" + case OpCmp: + name = "cmp" case OpAssertEq: name = "eq" + case OpAssertNotEq: + name = "ne" + case OpAssertIsBool: + name = "is_bool" + case OpAssertLessEqual: + name = "le" + case OpFromBinary: + name = "from_binary" + case OpToBinary: + name = "to_binary" + } + + return fmt.Sprintf("Gates.%s", name) +} + +func getGateName(gateVar string, explicit bool) string { + varName := "_ignored_" + if gateVar != "" { + varName = gateVar } + if explicit { + return fmt.Sprintf("(%s : F)", varName) + } + return varName +} + +func genGateBinder(gateVar string) string { + gateName := getGateName(gateVar, false) + return fmt.Sprintf("∃%s, %s = ", gateName, gateName) +} + +func genFunctionalGate(gateVar string, op Op, operands []string) string { + return fmt.Sprintf(" %s%s %s ∧\n", genGateBinder(gateVar), genGateOp(op), strings.Join(operands, " ")) +} + +func genCallbackGate(gateVar string, op Op, operands []string) string { + gateName := getGateName(gateVar, false) + return fmt.Sprintf(" ∃%s, %s %s %s ∧\n", gateName, genGateOp(op), strings.Join(operands, " "), gateName) +} + +func genGenericGate(op Op, operands []string) string { + return fmt.Sprintf(" %s %s ∧\n", genGateOp(op), strings.Join(operands, " ")) +} + +func genOpCall(gateVar string, inAssignment []ExArg, gateVars []string, op Op, args []Operand) string { + // functional is set to true when the op returns a value functional := false + callback := false switch op { - case OpAdd, OpMul, OpSub, OpDiv: + case OpDivUnchecked, OpDiv, OpInverse, OpXor, OpOr, OpAnd, OpSelect, OpLookup, OpCmp, OpIsZero, OpToBinary, OpFromBinary: + callback = true + case OpAdd, OpMulAcc, OpNegative, OpSub, OpMul: functional = true } - name = fmt.Sprintf("Gates.%s", name) - operands := strings.Join(operandExprs(args, inAssignment, gateVars), " ") + + operands := operandExprs(args, inAssignment, gateVars) if functional { - varName := "_ignored_" - if gateVar != "" { - varName = gateVar + // if an operation supports infinite length of arguments, + // turn it into a chain of operations + switch op { + case OpAdd, OpSub, OpMul: + { + finalStr := genFunctionalGate(gateVar, op, operands[0:2]) + for len(operands) > 2 { + operands = operands[1:] + operands[0] = getGateName(gateVar, false) + finalStr += genFunctionalGate(gateVar, op, operands[0:2]) + } + return finalStr + } } - binder := fmt.Sprintf("∃%s, %s = ", varName, varName) - return fmt.Sprintf(" %s%s %s ∧\n", binder, name, operands) + return genFunctionalGate(gateVar, op, operands) + } else if callback { + return genCallbackGate(gateVar, op, operands) } else { - return fmt.Sprintf(" %s %s ∧\n", name, operands) + return genGenericGate(op, operands) } } -func genLine(app App, gateVar string, inAssignment []string, gateVars []string) string { +func genLine(app App, gateVar string, inAssignment []ExArg, gateVars []string) string { switch app.Op.(type) { case *ExGadget: return genGadgetCall(gateVar, inAssignment, gateVars, app.Op.(*ExGadget), app.Args) @@ -123,7 +344,7 @@ func genLine(app App, gateVar string, inAssignment []string, gateVars []string) return "" } -func genGadgetBody(inAssignment []string, gadget ExGadget) string { +func genGadgetBody(inAssignment []ExArg, gadget ExGadget) string { gateVars := assignGateVars(gadget.Code, gadget.Outputs...) lines := make([]string, len(gadget.Code)) for i, app := range gadget.Code { @@ -148,10 +369,10 @@ func genCircuitBody(circuit ExCircuit) string { return strings.Join(append(lines, lastLine), "") } -func operandExpr(operand Operand, inAssignment []string, gateVars []string) string { +func operandExpr(operand Operand, inAssignment []ExArg, gateVars []string) string { switch operand.(type) { case Input: - return inAssignment[operand.(Input).Index] + return inAssignment[operand.(Input).Index].Name case Gate: return gateVars[operand.(Gate).Index] case Proj: @@ -159,11 +380,12 @@ func operandExpr(operand Operand, inAssignment []string, gateVars []string) stri case Const: return operand.(Const).Value.Text(10) default: + fmt.Printf("Type %T\n", operand) panic("not yet supported") } } -func operandExprs(operands []Operand, inAssignment []string, gateVars []string) []string { +func operandExprs(operands []Operand, inAssignment []ExArg, gateVars []string) []string { exprs := make([]string, len(operands)) for i, operand := range operands { exprs[i] = operandExpr(operand, inAssignment, gateVars) diff --git a/go.mod b/go.mod index 4341b2e..994b2d8 100644 --- a/go.mod +++ b/go.mod @@ -2,12 +2,14 @@ module gnark-extractor go 1.20 -require github.com/consensys/gnark v0.8.0 +require ( + github.com/consensys/gnark v0.8.0 + github.com/consensys/gnark-crypto v0.9.1 +) require ( github.com/blang/semver/v4 v4.0.0 // indirect github.com/consensys/bavard v0.1.13 // indirect - github.com/consensys/gnark-crypto v0.9.1 // indirect github.com/mattn/go-colorable v0.1.12 // indirect github.com/mattn/go-isatty v0.0.14 // indirect github.com/mmcloughlin/addchain v0.4.0 // indirect diff --git a/readme.md b/readme.md new file mode 100644 index 0000000..6714cfe --- /dev/null +++ b/readme.md @@ -0,0 +1,19 @@ +# `gnark-extractor` library + +## How to use +Implement the methods `AbsDefine` and `Define` for `MyCircuit` struct. Choose a curve to test the circuit on, then call the Lean extractor the following way: +```go +assignment := MyCircuit{} +err := CircuitToLean(&assignment, ecc.BW6_756) +if err != nil { + fmt.Println("CircuitToLean error!") + fmt.Println(err.Error()) +} +``` +The curves supported match the curves present in the library `consensys/gnark`. + +`CircuitToLean` prints in the `stdout` the circuit to be imported in Lean4 for verification. The Lean code depends on library `proven-zk` for the representation of Gates. + +## Windows +If using Powershell, change font to `NSimSun` for correct view of all characters: +[check this answer](https://stackoverflow.com/a/48029600) \ No newline at end of file