chore: refactoring for alpha version

extractor/extractor.go

@@ -2,10 +2,11 @@ package extractor
 
 import (
 	"fmt"
-	"gnark-extractor/abstractor"
 	"math/big"
 	"reflect"
 
+	"github.com/reilabs/gnark-extractor/abstractor"
+
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/backend/hint"
 	"github.com/consensys/gnark/frontend"

extractor/extractor_test.go

@@ -2,120 +2,16 @@ package extractor
 
 import (
 	"fmt"
-	"gnark-extractor/abstractor"
+	"log"
 	"testing"
 
+	"github.com/reilabs/gnark-extractor/abstractor"
+
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
 	"github.com/stretchr/testify/assert"
 )
 
-// Example: Semaphore circuit
-type DummyPoseidon2 struct {
-	In_1 frontend.Variable
-	In_2 frontend.Variable
-}
-
-func (gadget DummyPoseidon2) DefineGadget(api abstractor.API) []frontend.Variable {
-	hash := api.Mul(gadget.In_1, gadget.In_2)
-	return []frontend.Variable{hash}
-}
-
-type DummyPoseidon1 struct {
-	In frontend.Variable
-}
-
-func (gadget DummyPoseidon1) DefineGadget(api abstractor.API) []frontend.Variable {
-	hash := api.Mul(gadget.In, gadget.In)
-	return []frontend.Variable{hash}
-}
-
-type MerkleTreeInclusionProof struct {
-	Leaf        frontend.Variable
-	PathIndices []frontend.Variable
-	Siblings    []frontend.Variable
-}
-
-func (gadget MerkleTreeInclusionProof) DefineGadget(api abstractor.API) []frontend.Variable {
-	dummy_poseidon := api.DefineGadget(&DummyPoseidon2{})
-
-	levels := len(gadget.PathIndices)
-	hashes := make([]frontend.Variable, levels+1)
-
-	hashes[0] = gadget.Leaf
-	for i := 0; i < levels; i++ {
-		// Unrolled merkle_tree_inclusion_proof
-		api.AssertIsBoolean(gadget.PathIndices[i])
-		leftHash := dummy_poseidon.Call(DummyPoseidon2{hashes[i], gadget.Siblings[i]})[0]
-		rightHash := dummy_poseidon.Call(DummyPoseidon2{gadget.Siblings[i], hashes[i]})[0]
-		hashes[i+1] = api.Select(gadget.PathIndices[i], rightHash, leftHash)
-	}
-	root := hashes[levels]
-	return []frontend.Variable{root}
-}
-
-type Semaphore struct {
-	IdentityNullifier frontend.Variable   `gnark:",secret"`
-	IdentityTrapdoor  frontend.Variable   `gnark:",secret"`
-	TreePathIndices   []frontend.Variable `gnark:",secret"` // 0 | 1
-	TreeSiblings      []frontend.Variable `gnark:",secret"`
-
-	SignalHash        frontend.Variable `gnark:",public"`
-	ExternalNullifier frontend.Variable `gnark:",public"`
-
-	// Outputs to check
-	NullifierHash frontend.Variable `gnark:",public"`
-	MTRoot        frontend.Variable `gnark:",public"`
-
-	// Working values
-	Levels int
-}
-
-func (circuit *Semaphore) AbsDefine(api abstractor.API) error {
-	// From https://github.com/semaphore-protocol/semaphore/blob/main/packages/circuits/semaphore.circom
-	dummy_poseidon_1 := api.DefineGadget(&DummyPoseidon1{})
-	dummy_poseidon_2 := api.DefineGadget(&DummyPoseidon2{})
-	merkle_tree_inclusion_proof := api.DefineGadget(&MerkleTreeInclusionProof{
-		PathIndices: make([]frontend.Variable, circuit.Levels),
-		Siblings:    make([]frontend.Variable, circuit.Levels),
-	})
-
-	secret := dummy_poseidon_2.Call(DummyPoseidon2{circuit.IdentityNullifier, circuit.IdentityTrapdoor})[0]
-	identity_commitment := dummy_poseidon_1.Call(DummyPoseidon1{secret})[0]
-	nullifierHash := dummy_poseidon_2.Call(DummyPoseidon2{circuit.ExternalNullifier, circuit.IdentityNullifier})[0]
-	api.AssertIsEqual(nullifierHash, circuit.NullifierHash) // Verify
-
-	root := merkle_tree_inclusion_proof.Call(MerkleTreeInclusionProof{
-		Leaf:        identity_commitment,
-		PathIndices: circuit.TreePathIndices,
-		Siblings:    circuit.TreeSiblings,
-	})[0]
-
-	api.AssertIsEqual(root, circuit.MTRoot) // Verify
-	api.Mul(circuit.SignalHash, circuit.SignalHash)
-
-	return nil
-}
-
-func (circuit Semaphore) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
-func TestSemaphore(t *testing.T) {
-	nLevels := 3
-	assignment := Semaphore{
-		Levels:          nLevels,
-		TreePathIndices: make([]frontend.Variable, nLevels),
-		TreeSiblings:    make([]frontend.Variable, nLevels),
-	}
-	assert.Equal(t, len(assignment.TreePathIndices), len(assignment.TreeSiblings), "TreePathIndices and TreeSiblings must have the same length.")
-	err := CircuitToLean(&assignment, ecc.BW6_756)
-	if err != nil {
-		fmt.Println("CircuitToLean error!")
-		fmt.Println(err.Error())
-	}
-}
-
 // Example: circuit with constant parameter
 type SliceGadget struct {
 	In_1 []frontend.Variable
@@ -173,11 +69,11 @@ func TestCircuitWithParameter(t *testing.T) {
 	assignment := CircuitWithParameter{Path: make([]frontend.Variable, 3), Tree: make([]frontend.Variable, 2)}
 	assignment.Param = paramValue
 	assert.Equal(t, assignment.Param, paramValue, "assignment.Param is a const and should be 20.")
-	err := CircuitToLean(&assignment, ecc.BW6_756)
+	out, err := CircuitToLean(&assignment, ecc.BN254)
 	if err != nil {
-		fmt.Println("CircuitToLean error!")
-		fmt.Println(err.Error())
+		log.Fatal(err)
 	}
+	fmt.Println(out)
 }
 
 // Example: circuit with arrays and gadget
@@ -218,11 +114,11 @@ func (circuit MerkleRecover) Define(api frontend.API) error {
 
 func TestMerkleRecover(t *testing.T) {
 	assignment := MerkleRecover{}
-	err := CircuitToLean(&assignment, ecc.BW6_756)
+	out, err := CircuitToLean(&assignment, ecc.BN254)
 	if err != nil {
-		fmt.Println("CircuitToLean error!")
-		fmt.Println(err.Error())
+		log.Fatal(err)
 	}
+	fmt.Println(out)
 }
 
 // Example: circuit with multiple gadgets
@@ -273,9 +169,9 @@ func (circuit TwoGadgets) Define(api frontend.API) error {
 
 func TestTwoGadgets(t *testing.T) {
 	assignment := TwoGadgets{}
-	err := CircuitToLean(&assignment, ecc.BW6_756)
+	out, err := CircuitToLean(&assignment, ecc.BN254)
 	if err != nil {
-		fmt.Println("CircuitToLean error!")
-		fmt.Println(err.Error())
+		log.Fatal(err)
 	}
+	fmt.Println(out)
 }

extractor/lean_export.go

@@ -2,15 +2,35 @@ package extractor
 
 import (
 	"fmt"
-	"gnark-extractor/abstractor"
 	"reflect"
 	"strings"
 
+	"github.com/reilabs/gnark-extractor/abstractor"
+
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
 	"github.com/consensys/gnark/frontend/schema"
 )
 
+func ExportPrelude() string {
+	// Order could be extracted from circuit curve
+	s := `import ProvenZk.Gates
+import ProvenZk.VectorExtensions
+
+namespace Circuit
+
+def Order : ℕ := 21888242871839275222246405745257275088548364400416034343698204186575808495617
+variable [Fact (Nat.Prime Order)]
+abbrev F := ZMod Order`
+
+	return fmt.Sprintf("%s", s)
+}
+
+func ExportFooter() string {
+	s := `end Circuit`
+	return fmt.Sprintf("%s", s)
+}
+
 func ExportGadget(gadget ExGadget) string {
 	kArgsType := "F"
 	if len(gadget.Outputs) > 1 {
@@ -26,7 +46,9 @@ func ExportCircuit(circuit ExCircuit) string {
 		gadgets[i] = ExportGadget(gadget)
 	}
 	circ := fmt.Sprintf("def circuit %s: Prop :=\n%s", genArgs(circuit.Inputs), genCircuitBody(circuit))
-	return fmt.Sprintf("%s\n\n%s", strings.Join(gadgets, "\n\n"), circ)
+	prelude := ExportPrelude()
+	footer := ExportFooter()
+	return fmt.Sprintf("%s\n\n%s\n\n%s\n\n%s", prelude, strings.Join(gadgets, "\n\n"), circ, footer)
 }
 
 func ArrayInit(f schema.Field, v reflect.Value, op Operand) error {
@@ -127,10 +149,10 @@ func GetSchema(circuit any) (*schema.Schema, error) {
 	return schema.New(circuit, tVariable)
 }
 
-func CircuitToLean(circuit abstractor.Circuit, field ecc.ID) error {
+func CircuitToLean(circuit abstractor.Circuit, field ecc.ID) (string, error) {
 	schema, err := GetSchema(circuit)
 	if err != nil {
-		return err
+		return "", err
 	}
 
 	err = CircuitInit(circuit, schema)
@@ -147,17 +169,16 @@ func CircuitToLean(circuit abstractor.Circuit, field ecc.ID) error {
 
 	err = circuit.AbsDefine(&api)
 	if err != nil {
-		return err
+		return "", err
 	}
 
 	extractorCircuit := ExCircuit{
 		Inputs:  GetExArgs(circuit, schema.Fields),
 		Gadgets: api.Gadgets,
 		Code:    api.Code,
 	}
-	fmt.Println(ExportCircuit(extractorCircuit))
-
-	return nil
+	out := ExportCircuit(extractorCircuit)
+	return out, nil
 }
 
 func genNestedArrays(a ExArgType) string {

go.mod

@@ -1,4 +1,4 @@
-module gnark-extractor
+module github.com/reilabs/gnark-extractor
 
 go 1.20
 

readme.md

@@ -4,11 +4,11 @@
 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)
+out, err := CircuitToLean(&assignment, ecc.BN254)
 if err != nil {
-    fmt.Println("CircuitToLean error!")
-    fmt.Println(err.Error())
+    log.Fatal(err)
 }
+fmt.Println(out)
 ```
 The curves supported match the curves present in the library `consensys/gnark`.