Skip to content

Commit

Permalink
chore: removed abstractor.API (#41)
Browse files Browse the repository at this point in the history
* Removed abstractor.API

* refactor call

* moved interface to abstractor

* moved interface to abstractor
  • Loading branch information
Eagle941 authored Sep 25, 2023
1 parent a97a25e commit bbace65
Show file tree
Hide file tree
Showing 14 changed files with 88 additions and 265 deletions.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ type MyCircuit struct {
Out frontend.Variable
}

func (circuit *MyCircuit) AbsDefine(api abstractor.API) error {
func (circuit *MyCircuit) Define(api abstractor.API) error {
sum := api.Add(circuit.In_1, circuit.In_2)
api.AssertIsEqual(sum, circuit.Out)
return nil
Expand Down
26 changes: 1 addition & 25 deletions abstractor/abstractor.go
Original file line number Diff line number Diff line change
Expand Up @@ -7,33 +7,9 @@ type Gadget interface {
}

type GadgetDefinition interface {
DefineGadget(api API) interface{}
DefineGadget(api frontend.API) interface{}
}

type API interface {
frontend.API
DefineGadget(gadget GadgetDefinition) Gadget

frontend.API
Call(gadget GadgetDefinition) interface{}
}

type Circuit interface {
frontend.Circuit
AbsDefine(api API) error
}

func Concretize(api frontend.API, circuit Circuit) error {
return circuit.AbsDefine(&Concretizer{api})
}

func CallGadget(api frontend.API, circuit GadgetDefinition) interface{} {
_, ok := api.(API)
if ok {
// The consequence of calling CallGadget with abstractor.API is that
// the circuit is extracted as a single function instead of
// splitting in sub-circuits
panic("abstractor.CallGadget can't be called with abstractor.API")
}
return circuit.DefineGadget(&Concretizer{api})
}
129 changes: 0 additions & 129 deletions abstractor/concretizer.go

This file was deleted.

41 changes: 41 additions & 0 deletions abstractor/interface.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
// This file contains the public API for using the extractor.
// The Call functions are used to call gadgets and get their returnd object.
// These methods are prepared for doing automated casting from interface{}.
// Alternatively it's possible to do manual casting by calling
// abstractor.Call() and casting the result to the needed type.
package abstractor

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

// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
func Call(api frontend.API, gadget GadgetDefinition) frontend.Variable {
if abs, ok := api.(API); ok {
return abs.Call(gadget).(frontend.Variable)
} else {
return gadget.DefineGadget(api).(frontend.Variable)
}
}

// CallVoid is used to call a Gadget which doesn't return anything
func CallVoid(api frontend.API, gadget GadgetDefinition) {
Call(api, gadget)
}

// Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
func Call1(api frontend.API, gadget GadgetDefinition) []frontend.Variable {
return Call(api, gadget).([]frontend.Variable)
}

// Call2 is used to call a Gadget which returns a [][]frontend.Variable
// (i.e. `Vector (Vector F a) b` in Lean)
func Call2(api frontend.API, gadget GadgetDefinition) [][]frontend.Variable {
return Call(api, gadget).([][]frontend.Variable)
}

// Call3 is used to call a Gadget which returns a [][][]frontend.Variable
// (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
func Call3(api frontend.API, gadget GadgetDefinition) [][][]frontend.Variable {
return Call(api, gadget).([][][]frontend.Variable)
}
3 changes: 1 addition & 2 deletions extractor/extractor.go
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,11 @@ import (
"math/big"
"reflect"

"github.com/reilabs/gnark-lean-extractor/v2/abstractor"

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/backend/hint"
"github.com/consensys/gnark/frontend"
"github.com/consensys/gnark/frontend/schema"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
)

type Operand interface {
Expand Down
43 changes: 6 additions & 37 deletions extractor/interface.go
Original file line number Diff line number Diff line change
@@ -1,8 +1,4 @@
// This file contains the public API for using the extractor.
// The Call functions are used to call gadgets and get their returnd object.
// These methods are prepared for doing automated casting from interface{}.
// Alternatively it's possible to do manual casting by calling
// abstractor.API.Call() and casting the result to the needed type.
// This file contains the public API for running the extractor.
package extractor

import (
Expand All @@ -15,38 +11,11 @@ import (
"golang.org/x/exp/slices"
)

// CallVoid is used to call a Gadget which doesn't return anything
func CallVoid(api abstractor.API, gadget abstractor.GadgetDefinition) {
api.Call(gadget)
}

// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
func Call(api abstractor.API, gadget abstractor.GadgetDefinition) frontend.Variable {
return api.Call(gadget).(frontend.Variable)
}

// Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
func Call1(api abstractor.API, gadget abstractor.GadgetDefinition) []frontend.Variable {
return api.Call(gadget).([]frontend.Variable)
}

// Call2 is used to call a Gadget which returns a [][]frontend.Variable
// (i.e. `Vector (Vector F a) b` in Lean)
func Call2(api abstractor.API, gadget abstractor.GadgetDefinition) [][]frontend.Variable {
return api.Call(gadget).([][]frontend.Variable)
}

// Call3 is used to call a Gadget which returns a [][][]frontend.Variable
// (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
func Call3(api abstractor.API, gadget abstractor.GadgetDefinition) [][][]frontend.Variable {
return api.Call(gadget).([][][]frontend.Variable)
}

// CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`
// CircuitToLeanWithName and CircuitToLean aren't joined in a single function
// CircuitToLean(circuit abstractor.Circuit, field ecc.ID, namespace ...string) because the long term view
// is to add an optional parameter to support custom `set_option` directives in the header.
func CircuitToLeanWithName(circuit abstractor.Circuit, field ecc.ID, namespace string) (out string, err error) {
func CircuitToLeanWithName(circuit frontend.Circuit, field ecc.ID, namespace string) (out string, err error) {
defer recoverError()

schema, err := getSchema(circuit)
Expand All @@ -62,7 +31,7 @@ func CircuitToLeanWithName(circuit abstractor.Circuit, field ecc.ID, namespace s
FieldID: field,
}

err = circuit.AbsDefine(&api)
err = circuit.Define(&api)
if err != nil {
return "", err
}
Expand All @@ -80,7 +49,7 @@ func CircuitToLeanWithName(circuit abstractor.Circuit, field ecc.ID, namespace s
// CircuitToLean exports a `circuit` to Lean over a `field` with the namespace being the
// struct name of `circuit`
// When the namespace argument is not defined, it uses the name of the struct circuit
func CircuitToLean(circuit abstractor.Circuit, field ecc.ID) (string, error) {
func CircuitToLean(circuit frontend.Circuit, field ecc.ID) (string, error) {
name := getStructName(circuit)
return CircuitToLeanWithName(circuit, field, name)
}
Expand Down Expand Up @@ -110,7 +79,7 @@ func GadgetToLean(gadget abstractor.GadgetDefinition, field ecc.ID) (string, err
}

// ExtractCircuits is used to export a series of `circuits` to Lean over a `field` under `namespace`.
func ExtractCircuits(namespace string, field ecc.ID, circuits ...abstractor.Circuit) (out string, err error) {
func ExtractCircuits(namespace string, field ecc.ID, circuits ...frontend.Circuit) (out string, err error) {
defer recoverError()

api := CodeExtractor{
Expand Down Expand Up @@ -142,7 +111,7 @@ func ExtractCircuits(namespace string, field ecc.ID, circuits ...abstractor.Circ
past_circuits = append(past_circuits, name)

circuitInit(circuit, schema)
err = circuit.AbsDefine(&api)
err = circuit.Define(&api)
if err != nil {
return "", err
}
Expand Down
10 changes: 3 additions & 7 deletions extractor/test/another_circuit_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ type IntArrayGadget struct {
NestedMatrix [2][2]int
}

func (gadget IntArrayGadget) DefineGadget(api abstractor.API) interface{} {
func (gadget IntArrayGadget) DefineGadget(api frontend.API) interface{} {
r := api.FromBinary(gadget.In...)
api.Mul(gadget.Matrix[0], gadget.Matrix[1])
return []frontend.Variable{r, r, r}
Expand All @@ -28,8 +28,8 @@ type AnotherCircuit struct {
Matrix [2][2]int
}

func (circuit *AnotherCircuit) AbsDefine(api abstractor.API) error {
r := extractor.Call1(api, IntArrayGadget{
func (circuit *AnotherCircuit) Define(api frontend.API) error {
r := abstractor.Call1(api, IntArrayGadget{
circuit.In,
circuit.Matrix[0],
circuit.Matrix,
Expand All @@ -41,10 +41,6 @@ func (circuit *AnotherCircuit) AbsDefine(api abstractor.API) error {
return nil
}

func (circuit AnotherCircuit) Define(api frontend.API) error {
return abstractor.Concretize(api, &circuit)
}

func TestAnotherCircuit(t *testing.T) {
m := [2][2]int{
{0, 36},
Expand Down
16 changes: 6 additions & 10 deletions extractor/test/circuit_with_parameter_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ type ReturnItself struct {
Out []frontend.Variable
}

func (gadget ReturnItself) DefineGadget(api abstractor.API) interface{} {
func (gadget ReturnItself) DefineGadget(api frontend.API) interface{} {
for i := 0; i < len(gadget.In_1); i++ {
gadget.Out[i] = api.Mul(gadget.In_1[i], gadget.In_1[i])
}
Expand All @@ -30,7 +30,7 @@ type SliceGadget struct {
In_2 []frontend.Variable
}

func (gadget SliceGadget) DefineGadget(api abstractor.API) interface{} {
func (gadget SliceGadget) DefineGadget(api frontend.API) interface{} {
for i := 0; i < len(gadget.In_1); i++ {
api.Mul(gadget.In_1[i], gadget.In_2[i])
}
Expand All @@ -46,10 +46,10 @@ type CircuitWithParameter struct {
Param int
}

func (circuit *CircuitWithParameter) AbsDefine(api abstractor.API) error {
func (circuit *CircuitWithParameter) Define(api frontend.API) error {
D := make([]frontend.Variable, 3)
for i := 0; i < len(circuit.Path); i++ {
D = extractor.Call1(api, ReturnItself{
D = abstractor.Call1(api, ReturnItself{
In_1: circuit.Path,
Out: D,
})
Expand All @@ -66,19 +66,15 @@ func (circuit *CircuitWithParameter) AbsDefine(api abstractor.API) error {

dec := api.FromBinary(bin...)
api.AssertIsEqual(circuit.Param, dec)
extractor.Call(api, SliceGadget{circuit.Path, circuit.Path})
abstractor.Call(api, SliceGadget{circuit.Path, circuit.Path})

api.Mul(circuit.Path[0], circuit.Path[0])
extractor.Call(api, SliceGadget{circuit.Tree, circuit.Tree})
abstractor.Call(api, SliceGadget{circuit.Tree, circuit.Tree})
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) {
paramValue := 20
assignment := CircuitWithParameter{Path: make([]frontend.Variable, 3), Tree: make([]frontend.Variable, 2)}
Expand Down
Loading

0 comments on commit bbace65

Please sign in to comment.