Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: removed abstractor.API #41

Merged
merged 11 commits into from
Sep 25, 2023
Merged
Show file tree
Hide file tree
Changes from 9 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 1 addition & 24 deletions abstractor/abstractor.go
Original file line number Diff line number Diff line change
Expand Up @@ -7,33 +7,10 @@ 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
Eagle941 marked this conversation as resolved.
Show resolved Hide resolved
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