Skip to content

Commit

Permalink
feat: void return gadgets, multiple circuits export and Vector op…
Browse files Browse the repository at this point in the history
…timisation (#38)

* Added check in CallGadget

* Added support for gadgets with no return types

* Fixed const type coercion

* Added support for extraction of multiple gadgets

* Added support of Compiler interface

* Improved gadget naming

* Fixes to nested array of int in gadgets

* Added uninitialised structs

* Fixed sanitizeVars to support all flavours of ints

* Added extraction of multiple circuits

* Added vector optimisation

* Added vector optimisation in gadget return

* Added size check in isVectorComplete

* Added support for array of ints as parameters

* Fixed debug

* Fixed use of append

* Improved gotest

* Fixed gate vector optimisation

* Fixed clone gadget function

* Added 2dim slices optimisation

* Added tests

* Added support of n-dim slices optimisation

* Added support for multiple gadget return types

* Fix replaceArg

* Fixed nested slices

* Moved public mathods to interface.go

* Tests moved to test folder

* Moving generic functions to file misc.go

* Added comments and refactoring

* Added comments and error handling

* Gofmt
  • Loading branch information
Eagle941 authored Sep 25, 2023
1 parent 4298585 commit 4ac7e56
Show file tree
Hide file tree
Showing 31 changed files with 2,136 additions and 519 deletions.
8 changes: 4 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -40,15 +40,15 @@ func (circuit *MyCircuit) AbsDefine(api abstractor.API) error {
return nil
}

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

Once you export this to Lean, you get a definition as follows:

```lean
namespace DummyCircuit
namespace MyCircuit
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
Expand All @@ -59,7 +59,7 @@ def circuit (In_1: F) (In_2: F) (Out: F): Prop :=
Gates.eq gate_0 Out ∧
True
end DummyCircuit
end MyCircuit
```

Further examples of this process with various levels of complexity can be seen
Expand Down
15 changes: 11 additions & 4 deletions abstractor/abstractor.go
Original file line number Diff line number Diff line change
Expand Up @@ -3,19 +3,19 @@ package abstractor
import "github.com/consensys/gnark/frontend"

type Gadget interface {
Call(gadget GadgetDefinition) []frontend.Variable
Call(gadget GadgetDefinition) interface{}
}

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

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

frontend.API
Call(gadget GadgetDefinition) []frontend.Variable
Call(gadget GadgetDefinition) interface{}
}

type Circuit interface {
Expand All @@ -27,6 +27,13 @@ func Concretize(api frontend.API, circuit Circuit) error {
return circuit.AbsDefine(&Concretizer{api})
}

func CallGadget(api frontend.API, circuit GadgetDefinition) []frontend.Variable {
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})
}
4 changes: 2 additions & 2 deletions abstractor/concretizer.go
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ type ConcreteGadget struct {
api API
}

func (g *ConcreteGadget) Call(gadget GadgetDefinition) []frontend.Variable {
func (g *ConcreteGadget) Call(gadget GadgetDefinition) interface{} {
return gadget.DefineGadget(g.api)
}

Expand Down Expand Up @@ -122,7 +122,7 @@ func (c *Concretizer) DefineGadget(gadget GadgetDefinition) Gadget {
return &ConcreteGadget{c}
}

func (c *Concretizer) Call(gadget GadgetDefinition) []frontend.Variable {
func (c *Concretizer) Call(gadget GadgetDefinition) interface{} {
return c.DefineGadget(gadget).Call(gadget)
}

Expand Down
Loading

0 comments on commit 4ac7e56

Please sign in to comment.