From 82de980a032cbda5df68f319ddddd149a98d948f Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 20 Nov 2023 21:04:28 +0000
Subject: [PATCH] Removed gnark interface

---
 parser/interface.go                        | 103 -------------
 parser/misc.go                             |  38 -----
 parser/parser.go                           | 161 ---------------------
 parser/test/another_circuit_test.go        |  58 --------
 parser/test/circuit_with_parameter_test.go |  88 -----------
 parser/test/deletion_mbu_circuit_test.go   |  82 -----------
 parser/test/merkle_recover_test.go         |  50 -------
 parser/test/my_circuit_test.go             |  32 ----
 parser/test/slices_optimisation_test.go    | 106 --------------
 parser/test/to_binary_circuit_test.go      |  87 -----------
 parser/test/two_gadgets_test.go            | 117 ---------------
 parser/test/utils_test.go                  |  62 --------
 test/TestAnotherCircuit.lean               |  24 ---
 test/TestCircuitWithParameter.lean         |  53 -------
 test/TestDeletionMbuCircuit.lean           |  20 ---
 test/TestExtractCircuits.lean              | 134 -----------------
 test/TestExtractGadgets.lean               |  42 ------
 test/TestExtractGadgetsVectors.lean        |  28 ----
 test/TestGadgetExtraction.lean             |  18 ---
 test/TestMerkleRecover.lean                |  80 ----------
 test/TestMyCircuit.lean                    |  19 ---
 test/TestSlicesOptimisation.lean           |  35 -----
 test/TestToBinaryCircuit.lean              |  28 ----
 test/TestTwoGadgets.lean                   |  31 ----
 24 files changed, 1496 deletions(-)
 delete mode 100644 parser/interface.go
 delete mode 100644 parser/misc.go
 delete mode 100644 parser/parser.go
 delete mode 100644 parser/test/another_circuit_test.go
 delete mode 100644 parser/test/circuit_with_parameter_test.go
 delete mode 100644 parser/test/deletion_mbu_circuit_test.go
 delete mode 100644 parser/test/merkle_recover_test.go
 delete mode 100644 parser/test/my_circuit_test.go
 delete mode 100644 parser/test/slices_optimisation_test.go
 delete mode 100644 parser/test/to_binary_circuit_test.go
 delete mode 100644 parser/test/two_gadgets_test.go
 delete mode 100644 parser/test/utils_test.go
 delete mode 100644 test/TestAnotherCircuit.lean
 delete mode 100644 test/TestCircuitWithParameter.lean
 delete mode 100644 test/TestDeletionMbuCircuit.lean
 delete mode 100644 test/TestExtractCircuits.lean
 delete mode 100644 test/TestExtractGadgets.lean
 delete mode 100644 test/TestExtractGadgetsVectors.lean
 delete mode 100644 test/TestGadgetExtraction.lean
 delete mode 100644 test/TestMerkleRecover.lean
 delete mode 100644 test/TestMyCircuit.lean
 delete mode 100644 test/TestSlicesOptimisation.lean
 delete mode 100644 test/TestToBinaryCircuit.lean
 delete mode 100644 test/TestTwoGadgets.lean

diff --git a/parser/interface.go b/parser/interface.go
deleted file mode 100644
index 722ba9b..0000000
--- a/parser/interface.go
+++ /dev/null
@@ -1,103 +0,0 @@
-package parser
-
-import (
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
-	"golang.org/x/exp/slices"
-)
-
-// 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 extractor.ExtractorCircuit, field ecc.ID, namespace string) (out string, err error) {
-	defer recoverError()
-
-	schema, err := getSchema(circuit)
-	if err != nil {
-		return "", err
-	}
-
-	extractor.CircuitInit(circuit, schema)
-
-	api := GetExtractor(field)
-	err = circuit.Define(&api)
-	if err != nil {
-		return "", err
-	}
-
-	return extractor.GenerateLeanCode(namespace, &api.ext, circuit, schema.Fields)
-}
-
-// 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 extractor.ExtractorCircuit, field ecc.ID) (string, error) {
-	name := getStructName(circuit)
-	return CircuitToLeanWithName(circuit, field, name)
-}
-
-// GadgetToLeanWithName exports a `gadget` to Lean over a `field` with `namespace`
-// Same notes written for CircuitToLeanWithName apply to GadgetToLeanWithName and GadgetToLean
-func GadgetToLeanWithName(gadget abstractor.GadgetDefinition, field ecc.ID, namespace string) (out string, err error) {
-	defer recoverError()
-
-	api := GetExtractor(field)
-	api.DefineGadget(gadget)
-	return extractor.ExportGadgetsOnly(namespace, api.ext.GetGadgets(), api.ext.GetField()), nil
-}
-
-// GadgetToLean exports a `gadget` to Lean over a `field`
-func GadgetToLean(gadget abstractor.GadgetDefinition, field ecc.ID) (string, error) {
-	name := getStructName(gadget)
-	return GadgetToLeanWithName(gadget, field, name)
-}
-
-// ExtractCircuits is used to export a series of `circuits` to Lean over a `field` under `namespace`.
-func ExtractCircuits(namespace string, field ecc.ID, circuits ...extractor.ExtractorCircuit) (out string, err error) {
-	defer recoverError()
-
-	api := GetExtractor(field)
-
-	var circuits_extracted []string
-	var past_circuits []string
-
-	for _, circuit := range circuits {
-		schema, err := getSchema(circuit)
-		if err != nil {
-			return "", err
-		}
-		name := extractor.GenerateCircuitName(circuit, schema.Fields)
-		if slices.Contains(past_circuits, name) {
-			continue
-		}
-		past_circuits = append(past_circuits, name)
-
-		extractor.CircuitInit(circuit, schema)
-		err = circuit.Define(&api)
-		if err != nil {
-			return "", err
-		}
-
-		circuit_def := extractor.GenerateLeanCircuit(name, &api.ext, circuit, schema.Fields)
-		circuits_extracted = append(circuits_extracted, circuit_def)
-
-		// Resetting elements for next circuit
-		api.ext.ResetCode()
-	}
-
-	return extractor.GenerateLeanCircuits(namespace, &api.ext, circuits_extracted), nil
-}
-
-// ExtractGadgets is used to export a series of `gadgets` to Lean over a `field` under `namespace`.
-func ExtractGadgets(namespace string, field ecc.ID, gadgets ...abstractor.GadgetDefinition) (out string, err error) {
-	defer recoverError()
-
-	api := GetExtractor(field)
-
-	for _, gadget := range gadgets {
-		api.DefineGadget(gadget)
-	}
-	return extractor.ExportGadgetsOnly(namespace, api.ext.GetGadgets(), api.ext.GetField()), nil
-}
diff --git a/parser/misc.go b/parser/misc.go
deleted file mode 100644
index 21a0188..0000000
--- a/parser/misc.go
+++ /dev/null
@@ -1,38 +0,0 @@
-package parser
-
-import (
-	"errors"
-	"flag"
-	"fmt"
-	"reflect"
-	"runtime/debug"
-
-	"github.com/consensys/gnark/frontend"
-	"github.com/consensys/gnark/frontend/schema"
-)
-
-// getSchema is a cloned version of NewSchema without constraints
-func getSchema(circuit any) (*schema.Schema, error) {
-	tVariable := reflect.ValueOf(struct{ A frontend.Variable }{}).FieldByName("A").Type()
-	return schema.New(circuit, tVariable)
-}
-
-// getStructName returns the name of struct a
-func getStructName(a any) string {
-	return reflect.TypeOf(a).Elem().Name()
-}
-
-// recoverError is used in the top level interface to prevent panic
-// caused by any of the methods in the extractor from propagating
-// When go is running in test mode, it prints the stack trace to aid
-// debugging.
-func recoverError() (err error) {
-	if recover() != nil {
-		if flag.Lookup("test.v") != nil {
-			stack := string(debug.Stack())
-			fmt.Println(stack)
-		}
-		err = errors.New("Panic extracting circuit to Lean")
-	}
-	return nil
-}
diff --git a/parser/parser.go b/parser/parser.go
deleted file mode 100644
index a3f8f20..0000000
--- a/parser/parser.go
+++ /dev/null
@@ -1,161 +0,0 @@
-package parser
-
-import (
-	"math/big"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/backend/hint"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
-)
-
-// `CodeParser` implements the frontend.API as required by consensys/gnark
-type CodeParser struct {
-	ext extractor.CodeExtractor
-}
-
-// Keep GetExtractor for easy chaining of extractors
-func GetExtractor(field ecc.ID) CodeParser {
-	return CodeParser{ext: extractor.GetExtractor(field)}
-}
-
-func (ce *CodeParser) Call(gadget abstractor.GadgetDefinition) interface{} {
-	// Deep copying `gadget` because `DefineGadget` needs to modify the gadget fields.
-	// This was done as a replacement to the initial method of declaring gadgets using
-	// a direct call to `Define Gadget` within the circuit and then calling GadgetDefinition.Call
-	clonedGadget := extractor.CloneGadget(gadget)
-	g := ce.DefineGadget(clonedGadget)
-	return g.Call(gadget)
-}
-
-func (ce *CodeParser) Add(i1, i2 frontend.Variable, in ...frontend.Variable) frontend.Variable {
-	return ce.ext.Add(i1, i2, in...)
-}
-
-func (ce *CodeParser) MulAcc(a, b, c frontend.Variable) frontend.Variable {
-	return ce.ext.MulAcc(a, b, c)
-}
-
-func (ce *CodeParser) Neg(i1 frontend.Variable) frontend.Variable {
-	return ce.ext.Neg(i1)
-}
-
-func (ce *CodeParser) Sub(i1, i2 frontend.Variable, in ...frontend.Variable) frontend.Variable {
-	return ce.ext.Sub(i1, i2, in...)
-}
-
-func (ce *CodeParser) Mul(i1, i2 frontend.Variable, in ...frontend.Variable) frontend.Variable {
-	return ce.ext.Mul(i1, i2, in...)
-}
-
-func (ce *CodeParser) DivUnchecked(i1, i2 frontend.Variable) frontend.Variable {
-	return ce.ext.DivUnchecked(i1, i2)
-}
-
-func (ce *CodeParser) Div(i1, i2 frontend.Variable) frontend.Variable {
-	return ce.ext.Div(i1, i2)
-}
-
-func (ce *CodeParser) Inverse(i1 frontend.Variable) frontend.Variable {
-	return ce.ext.Inverse(i1)
-}
-
-func (ce *CodeParser) ToBinary(i1 frontend.Variable, n ...int) []frontend.Variable {
-	return ce.ext.ToBinary(i1, n...)
-}
-
-func (ce *CodeParser) FromBinary(b ...frontend.Variable) frontend.Variable {
-	return ce.ext.FromBinary(b...)
-}
-
-func (ce *CodeParser) Xor(a, b frontend.Variable) frontend.Variable {
-	return ce.ext.Xor(a, b)
-}
-
-func (ce *CodeParser) Or(a, b frontend.Variable) frontend.Variable {
-	return ce.ext.Or(a, b)
-}
-
-func (ce *CodeParser) And(a, b frontend.Variable) frontend.Variable {
-	return ce.ext.And(a, b)
-}
-
-func (ce *CodeParser) Select(b frontend.Variable, i1, i2 frontend.Variable) frontend.Variable {
-	return ce.ext.Select(b, i1, i2)
-}
-
-func (ce *CodeParser) Lookup2(b0, b1 frontend.Variable, i0, i1, i2, i3 frontend.Variable) frontend.Variable {
-	return ce.ext.Lookup2(b0, b1, i0, i1, i2, i3)
-}
-
-func (ce *CodeParser) IsZero(i1 frontend.Variable) frontend.Variable {
-	return ce.ext.IsZero(i1)
-}
-
-func (ce *CodeParser) Cmp(i1, i2 frontend.Variable) frontend.Variable {
-	return ce.ext.Cmp(i1, i2)
-}
-
-func (ce *CodeParser) AssertIsEqual(i1, i2 frontend.Variable) {
-	ce.ext.AssertIsEqual(i1, i2)
-}
-
-func (ce *CodeParser) AssertIsDifferent(i1, i2 frontend.Variable) {
-	ce.ext.AssertIsDifferent(i1, i2)
-}
-
-func (ce *CodeParser) AssertIsBoolean(i1 frontend.Variable) {
-	ce.ext.AssertIsBoolean(i1)
-}
-
-func (ce *CodeParser) AssertIsLessOrEqual(v frontend.Variable, bound frontend.Variable) {
-	ce.ext.AssertIsLessOrEqual(v, bound)
-}
-
-func (ce *CodeParser) Println(a ...frontend.Variable) {
-	// ce.ext.Println(a...)
-	panic("Not implemented")
-}
-
-func (ce *CodeParser) Compiler() frontend.Compiler {
-	// return ce.ext.Compiler()
-	panic("Not implemented")
-}
-
-func (ce *CodeParser) MarkBoolean(v frontend.Variable) {
-	// ce.ext.MarkBoolean(v)
-	panic("Not implemented")
-}
-
-func (ce *CodeParser) IsBoolean(v frontend.Variable) bool {
-	// return ce.ext.IsBoolean(v)
-	panic("Not implemented")
-}
-
-func (ce *CodeParser) Field() *big.Int {
-	return ce.ext.Field()
-}
-
-func (ce *CodeParser) FieldBitLen() int {
-	return ce.ext.FieldBitLen()
-}
-
-func (ce *CodeParser) Commit(v ...frontend.Variable) (frontend.Variable, error) {
-	// return ce.ext.Commit(v...)
-	panic("Not implemented")
-}
-
-func (ce *CodeParser) NewHint(f hint.Function, nbOutputs int, inputs ...frontend.Variable) ([]frontend.Variable, error) {
-	// return ce.ext.NewHint(f, nbOutputs, inputs...)
-	panic("Not implemented")
-}
-
-func (ce *CodeParser) ConstantValue(v frontend.Variable) (*big.Int, bool) {
-	return ce.ext.ConstantValue(v)
-}
-
-func (ce *CodeParser) DefineGadget(gadget abstractor.GadgetDefinition) abstractor.Gadget {
-	schema, _ := getSchema(gadget)
-	return ce.ext.DefineGadget(gadget, ce, schema)
-}
diff --git a/parser/test/another_circuit_test.go b/parser/test/another_circuit_test.go
deleted file mode 100644
index 06375f7..0000000
--- a/parser/test/another_circuit_test.go
+++ /dev/null
@@ -1,58 +0,0 @@
-package parser_test
-
-import (
-	"log"
-	"testing"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/parser"
-)
-
-// Example: Gadget with nested array of int
-type IntArrayGadget struct {
-	In           []frontend.Variable
-	Matrix       [2]int
-	NestedMatrix [2][2]int
-}
-
-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}
-}
-
-type AnotherCircuit struct {
-	In     []frontend.Variable
-	Matrix [2][2]int
-}
-
-func (circuit *AnotherCircuit) Define(api frontend.API) error {
-	r := abstractor.Call1(api, IntArrayGadget{
-		circuit.In,
-		circuit.Matrix[0],
-		circuit.Matrix,
-	})
-
-	api.FromBinary(r[1:3]...)
-	api.FromBinary(r[0:2]...)
-	api.FromBinary(r...)
-	return nil
-}
-
-func TestAnotherCircuit(t *testing.T) {
-	m := [2][2]int{
-		{0, 36},
-		{1, 44},
-	}
-	assignment := AnotherCircuit{
-		In:     make([]frontend.Variable, 4),
-		Matrix: m,
-	}
-	out, err := parser.CircuitToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
diff --git a/parser/test/circuit_with_parameter_test.go b/parser/test/circuit_with_parameter_test.go
deleted file mode 100644
index d599288..0000000
--- a/parser/test/circuit_with_parameter_test.go
+++ /dev/null
@@ -1,88 +0,0 @@
-package parser_test
-
-import (
-	"log"
-	"testing"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/parser"
-	"github.com/stretchr/testify/assert"
-)
-
-// Example: circuit with constant parameter
-type ReturnItself struct {
-	In_1 []frontend.Variable
-	Out  []frontend.Variable
-}
-
-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])
-	}
-
-	return gadget.Out
-}
-
-type SliceGadget struct {
-	In_1 []frontend.Variable
-	In_2 []frontend.Variable
-}
-
-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])
-	}
-
-	r := api.FromBinary(gadget.In_1...)
-	return r
-}
-
-type CircuitWithParameter struct {
-	In    frontend.Variable   `gnark:",public"`
-	Path  []frontend.Variable `gnark:",public"`
-	Tree  []frontend.Variable `gnark:",public"`
-	Param int
-}
-
-func (circuit *CircuitWithParameter) Define(api frontend.API) error {
-	D := make([]frontend.Variable, 3)
-	for i := 0; i < len(circuit.Path); i++ {
-		D = abstractor.Call1(api, ReturnItself{
-			In_1: circuit.Path,
-			Out:  D,
-		})
-		api.AssertIsEqual(D[1], D[2])
-	}
-
-	api.FromBinary(circuit.Path...)
-	api.FromBinary(D...)
-	api.FromBinary(D[1], D[2], D[0])
-	api.FromBinary(D[1], 0, D[0])
-	api.FromBinary(D[1:3]...)
-	bin := api.ToBinary(circuit.In)
-	bin = api.ToBinary(circuit.Param)
-
-	dec := api.FromBinary(bin...)
-	api.AssertIsEqual(circuit.Param, dec)
-	abstractor.Call(api, SliceGadget{circuit.Path, circuit.Path})
-
-	api.Mul(circuit.Path[0], circuit.Path[0])
-	abstractor.Call(api, SliceGadget{circuit.Tree, circuit.Tree})
-	api.AssertIsEqual(circuit.Param, circuit.In)
-
-	return nil
-}
-
-func TestCircuitWithParameter(t *testing.T) {
-	paramValue := 20
-	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.")
-	out, err := parser.CircuitToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
diff --git a/parser/test/deletion_mbu_circuit_test.go b/parser/test/deletion_mbu_circuit_test.go
deleted file mode 100644
index 7e7a712..0000000
--- a/parser/test/deletion_mbu_circuit_test.go
+++ /dev/null
@@ -1,82 +0,0 @@
-package parser_test
-
-import (
-	"log"
-	"testing"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/parser"
-)
-
-// Example: Mismatched arguments error
-type DeletionProof struct {
-	DeletionIndices []frontend.Variable
-	PreRoot         frontend.Variable
-	IdComms         []frontend.Variable
-	MerkleProofs    [][]frontend.Variable
-
-	BatchSize int
-	Depth     int
-}
-
-func (gadget DeletionProof) DefineGadget(api frontend.API) interface{} {
-	return gadget.PreRoot
-}
-
-type DeletionMbuCircuit struct {
-	// single public input
-	InputHash frontend.Variable `gnark:",public"`
-
-	// private inputs, but used as public inputs
-	DeletionIndices []frontend.Variable `gnark:"input"`
-	PreRoot         frontend.Variable   `gnark:"input"`
-	PostRoot        frontend.Variable   `gnark:"input"`
-
-	// private inputs
-	IdComms      []frontend.Variable   `gnark:"input"`
-	MerkleProofs [][]frontend.Variable `gnark:"input"`
-
-	BatchSize int
-	Depth     int
-}
-
-func (circuit *DeletionMbuCircuit) Define(api frontend.API) error {
-	root := abstractor.Call(api, DeletionProof{
-		DeletionIndices: circuit.DeletionIndices,
-		PreRoot:         circuit.PreRoot,
-		IdComms:         circuit.IdComms,
-		MerkleProofs:    circuit.MerkleProofs,
-		BatchSize:       circuit.BatchSize,
-		Depth:           circuit.Depth,
-	})
-
-	// Final root needs to match.
-	api.AssertIsEqual(root, circuit.PostRoot)
-
-	return nil
-}
-
-func TestDeletionMbuCircuit(t *testing.T) {
-	batchSize := 2
-	treeDepth := 3
-	proofs := make([][]frontend.Variable, batchSize)
-	for i := 0; i < int(batchSize); i++ {
-		proofs[i] = make([]frontend.Variable, treeDepth)
-	}
-
-	assignment := DeletionMbuCircuit{
-		DeletionIndices: make([]frontend.Variable, batchSize),
-		IdComms:         make([]frontend.Variable, batchSize),
-		MerkleProofs:    proofs,
-
-		BatchSize: int(batchSize),
-		Depth:     int(treeDepth),
-	}
-	out, err := parser.CircuitToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
diff --git a/parser/test/merkle_recover_test.go b/parser/test/merkle_recover_test.go
deleted file mode 100644
index 308514e..0000000
--- a/parser/test/merkle_recover_test.go
+++ /dev/null
@@ -1,50 +0,0 @@
-package parser_test
-
-import (
-	"log"
-	"testing"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/parser"
-)
-
-// Example: circuit with arrays and gadget
-type DummyHash struct {
-	In_1 frontend.Variable
-	In_2 frontend.Variable
-}
-
-func (gadget DummyHash) DefineGadget(api frontend.API) interface{} {
-	r := api.Mul(gadget.In_1, gadget.In_2)
-	return r
-}
-
-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) Define(api frontend.API) error {
-	current := circuit.Element
-	for i := 0; i < len(circuit.Path); i++ {
-		leftHash := abstractor.Call(api, DummyHash{current, circuit.Proof[i]})
-		rightHash := abstractor.Call(api, DummyHash{circuit.Proof[i], current})
-		current = api.Select(circuit.Path[i], rightHash, leftHash)
-	}
-	api.AssertIsEqual(current, circuit.Root)
-
-	return nil
-}
-
-func TestMerkleRecover(t *testing.T) {
-	assignment := MerkleRecover{}
-	out, err := parser.CircuitToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
diff --git a/parser/test/my_circuit_test.go b/parser/test/my_circuit_test.go
deleted file mode 100644
index 2bd73cb..0000000
--- a/parser/test/my_circuit_test.go
+++ /dev/null
@@ -1,32 +0,0 @@
-package parser_test
-
-import (
-	"log"
-	"testing"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/parser"
-)
-
-// Example: readme circuit
-type MyCircuit struct {
-	In_1 frontend.Variable
-	In_2 frontend.Variable
-	Out  frontend.Variable
-}
-
-func (circuit *MyCircuit) Define(api frontend.API) error {
-	sum := api.Add(circuit.In_1, circuit.In_2)
-	api.AssertIsEqual(sum, circuit.Out)
-	return nil
-}
-
-func TestMyCircuit(t *testing.T) {
-	assignment := MyCircuit{}
-	out, err := parser.CircuitToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
diff --git a/parser/test/slices_optimisation_test.go b/parser/test/slices_optimisation_test.go
deleted file mode 100644
index 5d59119..0000000
--- a/parser/test/slices_optimisation_test.go
+++ /dev/null
@@ -1,106 +0,0 @@
-package parser_test
-
-import (
-	"log"
-	"testing"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/parser"
-)
-
-// Example: checking slices optimisation
-type TwoSlices struct {
-	TwoDim [][]frontend.Variable
-}
-
-func (gadget TwoSlices) DefineGadget(api frontend.API) interface{} {
-	return gadget.TwoDim
-}
-
-type ThreeSlices struct {
-	ThreeDim [][][]frontend.Variable
-}
-
-func (gadget ThreeSlices) DefineGadget(api frontend.API) interface{} {
-	return gadget.ThreeDim
-}
-
-type SlicesGadget struct {
-	TwoDim   [][]frontend.Variable
-	ThreeDim [][][]frontend.Variable
-}
-
-func (gadget SlicesGadget) DefineGadget(api frontend.API) interface{} {
-	return append(gadget.ThreeDim[0][0], gadget.TwoDim[0]...)
-}
-
-type SlicesOptimisation struct {
-	Test     frontend.Variable
-	Id       []frontend.Variable
-	TwoDim   [][]frontend.Variable
-	ThreeDim [][][]frontend.Variable
-}
-
-func (circuit *SlicesOptimisation) Define(api frontend.API) error {
-	abstractor.Call1(api, SlicesGadget{
-		TwoDim:   circuit.TwoDim,
-		ThreeDim: circuit.ThreeDim,
-	})
-	abstractor.Call1(api, SlicesGadget{
-		TwoDim:   [][]frontend.Variable{circuit.TwoDim[1], circuit.TwoDim[0]},
-		ThreeDim: [][][]frontend.Variable{circuit.ThreeDim[1], circuit.ThreeDim[0]},
-	})
-	abstractor.Call1(api, SlicesGadget{
-		TwoDim:   [][]frontend.Variable{{circuit.TwoDim[1][1]}, {circuit.TwoDim[1][0]}},
-		ThreeDim: [][][]frontend.Variable{circuit.ThreeDim[1], circuit.ThreeDim[0], circuit.ThreeDim[1]},
-	})
-	abstractor.Call1(api, SlicesGadget{
-		TwoDim:   [][]frontend.Variable{circuit.TwoDim[1], {circuit.TwoDim[1][0], circuit.TwoDim[0][0], circuit.TwoDim[1][1]}},
-		ThreeDim: circuit.ThreeDim,
-	})
-	abstractor.Call2(api, TwoSlices{
-		TwoDim: circuit.TwoDim,
-	})
-	a := abstractor.Call3(api, ThreeSlices{
-		ThreeDim: circuit.ThreeDim,
-	})
-	b := abstractor.Call3(api, ThreeSlices{
-		ThreeDim: a,
-	})
-	abstractor.Call3(api, ThreeSlices{
-		ThreeDim: b,
-	})
-
-	return nil
-}
-
-func TestSlicesOptimisation(t *testing.T) {
-	depthOne := 2
-	depthTwo := 3
-	depthThree := 4
-	twoSlice := make([][]frontend.Variable, depthOne)
-	for i := 0; i < int(depthOne); i++ {
-		twoSlice[i] = make([]frontend.Variable, depthTwo)
-	}
-
-	threeSlice := make([][][]frontend.Variable, depthOne)
-	for x := 0; x < int(depthOne); x++ {
-		threeSlice[x] = make([][]frontend.Variable, depthTwo)
-		for y := 0; y < int(depthTwo); y++ {
-			threeSlice[x][y] = make([]frontend.Variable, depthThree)
-		}
-	}
-
-	assignment := SlicesOptimisation{
-		Id:       make([]frontend.Variable, depthTwo),
-		TwoDim:   twoSlice,
-		ThreeDim: threeSlice,
-	}
-	out, err := parser.CircuitToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
diff --git a/parser/test/to_binary_circuit_test.go b/parser/test/to_binary_circuit_test.go
deleted file mode 100644
index 6193328..0000000
--- a/parser/test/to_binary_circuit_test.go
+++ /dev/null
@@ -1,87 +0,0 @@
-package parser_test
-
-import (
-	"log"
-	"testing"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/parser"
-)
-
-// Example: Gadget that returns a vector
-type OptimisedVectorGadget struct {
-	In frontend.Variable
-}
-
-func (gadget OptimisedVectorGadget) DefineGadget(api frontend.API) interface{} {
-	return api.ToBinary(gadget.In, 3)
-}
-
-// Example: ToBinary behaviour and nested Slice
-type VectorGadget struct {
-	In_1   []frontend.Variable
-	In_2   []frontend.Variable
-	Nested [][]frontend.Variable
-}
-
-func (gadget VectorGadget) DefineGadget(api frontend.API) interface{} {
-	var sum frontend.Variable
-	for i := 0; i < len(gadget.In_1); i++ {
-		sum = api.Mul(gadget.In_1[i], gadget.In_2[i])
-	}
-	return []frontend.Variable{sum, sum, sum}
-}
-
-type ToBinaryCircuit struct {
-	In     frontend.Variable     `gnark:",public"`
-	Out    frontend.Variable     `gnark:",public"`
-	Double [][]frontend.Variable `gnark:",public"`
-}
-
-func (circuit *ToBinaryCircuit) Define(api frontend.API) error {
-	bin := api.ToBinary(circuit.In, 3)
-	bout := api.ToBinary(circuit.Out, 3)
-
-	api.Add(circuit.Double[2][2], circuit.Double[1][1], circuit.Double[0][0])
-	api.Mul(bin[1], bout[1])
-	d := abstractor.Call1(api, VectorGadget{circuit.Double[2][:], circuit.Double[0][:], circuit.Double})
-	api.Mul(d[2], d[1])
-
-	return nil
-}
-
-func TestGadgetExtraction(t *testing.T) {
-	dim_1 := 3
-	dim_2 := 3
-	doubleSlice := make([][]frontend.Variable, dim_1)
-	for i := 0; i < int(dim_1); i++ {
-		doubleSlice[i] = make([]frontend.Variable, dim_2)
-	}
-	assignment := VectorGadget{
-		In_1:   make([]frontend.Variable, dim_2),
-		In_2:   make([]frontend.Variable, dim_2),
-		Nested: doubleSlice,
-	}
-	out, err := parser.GadgetToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
-
-func TestToBinaryCircuit(t *testing.T) {
-	dim_1 := 3
-	dim_2 := 3
-	doubleSlice := make([][]frontend.Variable, dim_1)
-	for i := 0; i < int(dim_1); i++ {
-		doubleSlice[i] = make([]frontend.Variable, dim_2)
-	}
-	assignment := ToBinaryCircuit{Double: doubleSlice}
-	out, err := parser.CircuitToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
diff --git a/parser/test/two_gadgets_test.go b/parser/test/two_gadgets_test.go
deleted file mode 100644
index 23cbbe8..0000000
--- a/parser/test/two_gadgets_test.go
+++ /dev/null
@@ -1,117 +0,0 @@
-package parser_test
-
-import (
-	"log"
-	"testing"
-
-	"github.com/consensys/gnark-crypto/ecc"
-	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-	"github.com/reilabs/gnark-lean-extractor/v2/parser"
-)
-
-// Example: circuit with multiple gadgets
-type MyWidget struct {
-	Test_1 frontend.Variable
-	Test_2 frontend.Variable
-	Num    uint32
-}
-
-func (gadget MyWidget) DefineGadget(api frontend.API) interface{} {
-	sum := api.Add(gadget.Test_1, gadget.Test_2)
-	mul := api.Mul(gadget.Test_1, gadget.Test_2)
-	r := api.Div(sum, mul)
-	api.AssertIsBoolean(gadget.Num)
-	return r
-}
-
-type MySecondWidget struct {
-	Test_1 frontend.Variable
-	Test_2 frontend.Variable
-	Num    int
-}
-
-func (gadget MySecondWidget) DefineGadget(api frontend.API) interface{} {
-	mul := api.Mul(gadget.Test_1, gadget.Test_2)
-	snd := abstractor.Call(api, MyWidget{gadget.Test_1, gadget.Test_2, uint32(gadget.Num)})
-	api.Mul(mul, snd)
-	return nil
-}
-
-type TwoGadgets struct {
-	In_1 frontend.Variable
-	In_2 frontend.Variable
-	Num  int
-}
-
-func (circuit *TwoGadgets) Define(api frontend.API) error {
-	sum := api.Add(circuit.In_1, circuit.In_2)
-	prod := api.Mul(circuit.In_1, circuit.In_2)
-	abstractor.CallVoid(api, MySecondWidget{sum, prod, circuit.Num})
-	return nil
-}
-
-func TestTwoGadgets(t *testing.T) {
-	assignment := TwoGadgets{Num: 11}
-	out, err := parser.CircuitToLean(&assignment, ecc.BN254)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
-
-func TestExtractGadgets(t *testing.T) {
-	assignment_1 := DummyHash{}
-	assignment_2 := MySecondWidget{Num: 11}
-	assignment_3 := MySecondWidget{Num: 9}
-	out, err := parser.ExtractGadgets("MultipleGadgets", ecc.BN254, &assignment_1, &assignment_2, &assignment_3)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
-
-func TestExtractGadgetsVectors(t *testing.T) {
-	dim_1 := 3
-	dim_2 := 3
-	doubleSlice := make([][]frontend.Variable, dim_1)
-	for i := 0; i < int(dim_1); i++ {
-		doubleSlice[i] = make([]frontend.Variable, dim_2)
-	}
-	assignment_1 := VectorGadget{
-		In_1:   make([]frontend.Variable, dim_2),
-		In_2:   make([]frontend.Variable, dim_2),
-		Nested: doubleSlice,
-	}
-	assignment_2 := ReturnItself{
-		In_1: make([]frontend.Variable, dim_1),
-		Out:  make([]frontend.Variable, dim_1),
-	}
-	assignment_3 := OptimisedVectorGadget{}
-	out, err := parser.ExtractGadgets("MultipleGadgetsVectors", ecc.BN254, &assignment_1, &assignment_2, &assignment_3)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
-
-func TestExtractCircuits(t *testing.T) {
-	assignment_1 := TwoGadgets{Num: 11}
-	assignment_2 := MerkleRecover{}
-
-	dim_1 := 3
-	dim_2 := 3
-	doubleSlice := make([][]frontend.Variable, dim_1)
-	for i := 0; i < int(dim_1); i++ {
-		doubleSlice[i] = make([]frontend.Variable, dim_2)
-	}
-	assignment_3 := ToBinaryCircuit{Double: doubleSlice}
-	assignment_4 := TwoGadgets{Num: 6}
-	assignment_5 := TwoGadgets{Num: 6}
-
-	out, err := parser.ExtractCircuits("MultipleCircuits", ecc.BN254, &assignment_3, &assignment_2, &assignment_1, &assignment_4, &assignment_5)
-	if err != nil {
-		log.Fatal(err)
-	}
-	checkOutput(t, out)
-}
diff --git a/parser/test/utils_test.go b/parser/test/utils_test.go
deleted file mode 100644
index d487416..0000000
--- a/parser/test/utils_test.go
+++ /dev/null
@@ -1,62 +0,0 @@
-package parser_test
-
-import (
-	"bytes"
-	"crypto/sha256"
-	"errors"
-	"fmt"
-	"io"
-	"log"
-	"os"
-	"testing"
-)
-
-// saveOutput can be called once when creating/changing a test to generate
-// the reference result
-func saveOutput(filename string, testOutput string) {
-	f, err := os.Create(filename)
-	if err != nil {
-		log.Fatal(err)
-	}
-	defer f.Close()
-
-	_, err = f.WriteString(testOutput)
-	if err != nil {
-		log.Fatal(err)
-	}
-}
-
-// checkOutput performs a check of the circuit generated by the extractor.
-// If the hashes don't match, the circuit generated by the extractor is printed.
-func checkOutput(t *testing.T, testOutput string) {
-	// I assume tests are executed from the extractor/test directory
-	filename := fmt.Sprintf("../../test/%s.lean", t.Name())
-
-	// https://stackoverflow.com/a/66405130
-	if _, err := os.Stat(filename); errors.Is(err, os.ErrNotExist) {
-		saveOutput(filename, testOutput)
-	}
-
-	f, err := os.Open(filename)
-	if err != nil {
-		log.Fatalf("Error checking test output\n\n%s\n\n%s\n\n", err, testOutput)
-	}
-	defer f.Close()
-
-	h := sha256.New()
-	if _, err := io.Copy(h, f); err != nil {
-		log.Fatal(err)
-	}
-
-	correctHash := h.Sum(nil)
-
-	h.Reset()
-	if _, err := h.Write([]byte(testOutput)); err != nil {
-		log.Fatal(err)
-	}
-	testResultHash := h.Sum(nil)
-	if !bytes.Equal(correctHash, testResultHash) {
-		t.Logf("This circuit doesn't match the result in the test folder\n\n%s", testOutput)
-		t.Fail()
-	}
-}
diff --git a/test/TestAnotherCircuit.lean b/test/TestAnotherCircuit.lean
deleted file mode 100644
index fb065b5..0000000
--- a/test/TestAnotherCircuit.lean
+++ /dev/null
@@ -1,24 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace AnotherCircuit
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def IntArrayGadget_4 (In: Vector F 4) (k: Vector F 3 -> Prop): Prop :=
-    ∃gate_0, Gates.from_binary In gate_0 ∧
-    ∃_ignored_, _ignored_ = Gates.mul (0:F) (36:F) ∧
-    k vec![gate_0, gate_0, gate_0]
-
-def circuit (In: Vector F 4): Prop :=
-    IntArrayGadget_4 In fun gate_0 =>
-    ∃_ignored_, Gates.from_binary vec![gate_0[1], gate_0[2]] _ignored_ ∧
-    ∃_ignored_, Gates.from_binary vec![gate_0[0], gate_0[1]] _ignored_ ∧
-    ∃_ignored_, Gates.from_binary gate_0 _ignored_ ∧
-    True
-
-end AnotherCircuit
\ No newline at end of file
diff --git a/test/TestCircuitWithParameter.lean b/test/TestCircuitWithParameter.lean
deleted file mode 100644
index 2fdcd96..0000000
--- a/test/TestCircuitWithParameter.lean
+++ /dev/null
@@ -1,53 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace CircuitWithParameter
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def ReturnItself_3_3 (In_1: Vector F 3) (Out: Vector F 3) (k: Vector F 3 -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.mul In_1[0] In_1[0] ∧
-    ∃gate_1, gate_1 = Gates.mul In_1[1] In_1[1] ∧
-    ∃gate_2, gate_2 = Gates.mul In_1[2] In_1[2] ∧
-    k vec![gate_0, gate_1, gate_2]
-
-def SliceGadget_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (k: F -> Prop): Prop :=
-    ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧
-    ∃_ignored_, _ignored_ = Gates.mul In_1[1] In_2[1] ∧
-    ∃_ignored_, _ignored_ = Gates.mul In_1[2] In_2[2] ∧
-    ∃gate_3, Gates.from_binary In_1 gate_3 ∧
-    k gate_3
-
-def SliceGadget_2_2 (In_1: Vector F 2) (In_2: Vector F 2) (k: F -> Prop): Prop :=
-    ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧
-    ∃_ignored_, _ignored_ = Gates.mul In_1[1] In_2[1] ∧
-    ∃gate_2, Gates.from_binary In_1 gate_2 ∧
-    k gate_2
-
-def circuit (In: F) (Path: Vector F 3) (Tree: Vector F 2): Prop :=
-    ReturnItself_3_3 Path vec![(0:F), (0:F), (0:F)] fun gate_0 =>
-    Gates.eq gate_0[1] gate_0[2] ∧
-    ReturnItself_3_3 Path gate_0 fun gate_2 =>
-    Gates.eq gate_2[1] gate_2[2] ∧
-    ReturnItself_3_3 Path gate_2 fun gate_4 =>
-    Gates.eq gate_4[1] gate_4[2] ∧
-    ∃_ignored_, Gates.from_binary Path _ignored_ ∧
-    ∃_ignored_, Gates.from_binary gate_4 _ignored_ ∧
-    ∃_ignored_, Gates.from_binary vec![gate_4[1], gate_4[2], gate_4[0]] _ignored_ ∧
-    ∃_ignored_, Gates.from_binary vec![gate_4[1], (0:F), gate_4[0]] _ignored_ ∧
-    ∃_ignored_, Gates.from_binary vec![gate_4[1], gate_4[2]] _ignored_ ∧
-    ∃_ignored_, Gates.to_binary In 254 _ignored_ ∧
-    ∃gate_12, Gates.to_binary (20:F) 254 gate_12 ∧
-    ∃gate_13, Gates.from_binary gate_12 gate_13 ∧
-    Gates.eq (20:F) gate_13 ∧
-    SliceGadget_3_3 Path Path fun _ =>
-    ∃_ignored_, _ignored_ = Gates.mul Path[0] Path[0] ∧
-    SliceGadget_2_2 Tree Tree fun _ =>
-    Gates.eq (20:F) In ∧
-    True
-
-end CircuitWithParameter
\ No newline at end of file
diff --git a/test/TestDeletionMbuCircuit.lean b/test/TestDeletionMbuCircuit.lean
deleted file mode 100644
index 680a783..0000000
--- a/test/TestDeletionMbuCircuit.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace DeletionMbuCircuit
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def DeletionProof_2_2_3_2_2_3 (DeletionIndices: Vector F 2) (PreRoot: F) (IdComms: Vector F 2) (MerkleProofs: Vector (Vector F 3) 2) (k: F -> Prop): Prop :=
-    k PreRoot
-
-def circuit (InputHash: F) (DeletionIndices: Vector F 2) (PreRoot: F) (PostRoot: F) (IdComms: Vector F 2) (MerkleProofs: Vector (Vector F 3) 2): Prop :=
-    DeletionProof_2_2_3_2_2_3 DeletionIndices PreRoot IdComms MerkleProofs fun gate_0 =>
-    Gates.eq gate_0 PostRoot ∧
-    True
-
-end DeletionMbuCircuit
\ No newline at end of file
diff --git a/test/TestExtractCircuits.lean b/test/TestExtractCircuits.lean
deleted file mode 100644
index dea3173..0000000
--- a/test/TestExtractCircuits.lean
+++ /dev/null
@@ -1,134 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace MultipleCircuits
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def VectorGadget_3_3_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (Nested: Vector (Vector F 3) 3) (k: Vector F 3 -> Prop): Prop :=
-    ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧
-    ∃_ignored_, _ignored_ = Gates.mul In_1[1] In_2[1] ∧
-    ∃gate_2, gate_2 = Gates.mul In_1[2] In_2[2] ∧
-    k vec![gate_2, gate_2, gate_2]
-
-def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧
-    k gate_0
-
-def MyWidget_11 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧
-    ∃gate_1, gate_1 = Gates.mul Test_1 Test_2 ∧
-    ∃gate_2, Gates.div gate_0 gate_1 gate_2 ∧
-    Gates.is_bool (11:F) ∧
-    k gate_2
-
-def MySecondWidget_11 (Test_1: F) (Test_2: F) : Prop :=
-    ∃gate_0, gate_0 = Gates.mul Test_1 Test_2 ∧
-    MyWidget_11 Test_1 Test_2 fun gate_1 =>
-    ∃_ignored_, _ignored_ = Gates.mul gate_0 gate_1 ∧
-    True
-
-def MyWidget_6 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧
-    ∃gate_1, gate_1 = Gates.mul Test_1 Test_2 ∧
-    ∃gate_2, Gates.div gate_0 gate_1 gate_2 ∧
-    Gates.is_bool (6:F) ∧
-    k gate_2
-
-def MySecondWidget_6 (Test_1: F) (Test_2: F) : Prop :=
-    ∃gate_0, gate_0 = Gates.mul Test_1 Test_2 ∧
-    MyWidget_6 Test_1 Test_2 fun gate_1 =>
-    ∃_ignored_, _ignored_ = Gates.mul gate_0 gate_1 ∧
-    True
-
-def ToBinaryCircuit_3_3 (In: F) (Out: F) (Double: Vector (Vector F 3) 3): Prop :=
-    ∃gate_0, Gates.to_binary In 3 gate_0 ∧
-    ∃gate_1, Gates.to_binary Out 3 gate_1 ∧
-    ∃_ignored_, _ignored_ = Gates.add Double[2][2] Double[1][1] ∧
-    ∃_ignored_, _ignored_ = Gates.add _ignored_ Double[0][0] ∧
-    ∃_ignored_, _ignored_ = Gates.mul gate_0[1] gate_1[1] ∧
-    VectorGadget_3_3_3_3 Double[2] Double[0] Double fun gate_4 =>
-    ∃_ignored_, _ignored_ = Gates.mul gate_4[2] gate_4[1] ∧
-    True
-
-def MerkleRecover_20_20 (Root: F) (Element: F) (Path: Vector F 20) (Proof: Vector F 20): Prop :=
-    DummyHash Element Proof[0] fun gate_0 =>
-    DummyHash Proof[0] Element fun gate_1 =>
-    ∃gate_2, Gates.select Path[0] gate_1 gate_0 gate_2 ∧
-    DummyHash gate_2 Proof[1] fun gate_3 =>
-    DummyHash Proof[1] gate_2 fun gate_4 =>
-    ∃gate_5, Gates.select Path[1] gate_4 gate_3 gate_5 ∧
-    DummyHash gate_5 Proof[2] fun gate_6 =>
-    DummyHash Proof[2] gate_5 fun gate_7 =>
-    ∃gate_8, Gates.select Path[2] gate_7 gate_6 gate_8 ∧
-    DummyHash gate_8 Proof[3] fun gate_9 =>
-    DummyHash Proof[3] gate_8 fun gate_10 =>
-    ∃gate_11, Gates.select Path[3] gate_10 gate_9 gate_11 ∧
-    DummyHash gate_11 Proof[4] fun gate_12 =>
-    DummyHash Proof[4] gate_11 fun gate_13 =>
-    ∃gate_14, Gates.select Path[4] gate_13 gate_12 gate_14 ∧
-    DummyHash gate_14 Proof[5] fun gate_15 =>
-    DummyHash Proof[5] gate_14 fun gate_16 =>
-    ∃gate_17, Gates.select Path[5] gate_16 gate_15 gate_17 ∧
-    DummyHash gate_17 Proof[6] fun gate_18 =>
-    DummyHash Proof[6] gate_17 fun gate_19 =>
-    ∃gate_20, Gates.select Path[6] gate_19 gate_18 gate_20 ∧
-    DummyHash gate_20 Proof[7] fun gate_21 =>
-    DummyHash Proof[7] gate_20 fun gate_22 =>
-    ∃gate_23, Gates.select Path[7] gate_22 gate_21 gate_23 ∧
-    DummyHash gate_23 Proof[8] fun gate_24 =>
-    DummyHash Proof[8] gate_23 fun gate_25 =>
-    ∃gate_26, Gates.select Path[8] gate_25 gate_24 gate_26 ∧
-    DummyHash gate_26 Proof[9] fun gate_27 =>
-    DummyHash Proof[9] gate_26 fun gate_28 =>
-    ∃gate_29, Gates.select Path[9] gate_28 gate_27 gate_29 ∧
-    DummyHash gate_29 Proof[10] fun gate_30 =>
-    DummyHash Proof[10] gate_29 fun gate_31 =>
-    ∃gate_32, Gates.select Path[10] gate_31 gate_30 gate_32 ∧
-    DummyHash gate_32 Proof[11] fun gate_33 =>
-    DummyHash Proof[11] gate_32 fun gate_34 =>
-    ∃gate_35, Gates.select Path[11] gate_34 gate_33 gate_35 ∧
-    DummyHash gate_35 Proof[12] fun gate_36 =>
-    DummyHash Proof[12] gate_35 fun gate_37 =>
-    ∃gate_38, Gates.select Path[12] gate_37 gate_36 gate_38 ∧
-    DummyHash gate_38 Proof[13] fun gate_39 =>
-    DummyHash Proof[13] gate_38 fun gate_40 =>
-    ∃gate_41, Gates.select Path[13] gate_40 gate_39 gate_41 ∧
-    DummyHash gate_41 Proof[14] fun gate_42 =>
-    DummyHash Proof[14] gate_41 fun gate_43 =>
-    ∃gate_44, Gates.select Path[14] gate_43 gate_42 gate_44 ∧
-    DummyHash gate_44 Proof[15] fun gate_45 =>
-    DummyHash Proof[15] gate_44 fun gate_46 =>
-    ∃gate_47, Gates.select Path[15] gate_46 gate_45 gate_47 ∧
-    DummyHash gate_47 Proof[16] fun gate_48 =>
-    DummyHash Proof[16] gate_47 fun gate_49 =>
-    ∃gate_50, Gates.select Path[16] gate_49 gate_48 gate_50 ∧
-    DummyHash gate_50 Proof[17] fun gate_51 =>
-    DummyHash Proof[17] gate_50 fun gate_52 =>
-    ∃gate_53, Gates.select Path[17] gate_52 gate_51 gate_53 ∧
-    DummyHash gate_53 Proof[18] fun gate_54 =>
-    DummyHash Proof[18] gate_53 fun gate_55 =>
-    ∃gate_56, Gates.select Path[18] gate_55 gate_54 gate_56 ∧
-    DummyHash gate_56 Proof[19] fun gate_57 =>
-    DummyHash Proof[19] gate_56 fun gate_58 =>
-    ∃gate_59, Gates.select Path[19] gate_58 gate_57 gate_59 ∧
-    Gates.eq gate_59 Root ∧
-    True
-
-def TwoGadgets_11 (In_1: F) (In_2: F): Prop :=
-    ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧
-    ∃gate_1, gate_1 = Gates.mul In_1 In_2 ∧
-    MySecondWidget_11 gate_0 gate_1 ∧
-    True
-
-def TwoGadgets_6 (In_1: F) (In_2: F): Prop :=
-    ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧
-    ∃gate_1, gate_1 = Gates.mul In_1 In_2 ∧
-    MySecondWidget_6 gate_0 gate_1 ∧
-    True
-
-end MultipleCircuits
\ No newline at end of file
diff --git a/test/TestExtractGadgets.lean b/test/TestExtractGadgets.lean
deleted file mode 100644
index 128d0ac..0000000
--- a/test/TestExtractGadgets.lean
+++ /dev/null
@@ -1,42 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace MultipleGadgets
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧
-    k gate_0
-
-def MyWidget_11 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧
-    ∃gate_1, gate_1 = Gates.mul Test_1 Test_2 ∧
-    ∃gate_2, Gates.div gate_0 gate_1 gate_2 ∧
-    Gates.is_bool (11:F) ∧
-    k gate_2
-
-def MySecondWidget_11 (Test_1: F) (Test_2: F) : Prop :=
-    ∃gate_0, gate_0 = Gates.mul Test_1 Test_2 ∧
-    MyWidget_11 Test_1 Test_2 fun gate_1 =>
-    ∃_ignored_, _ignored_ = Gates.mul gate_0 gate_1 ∧
-    True
-
-def MyWidget_9 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧
-    ∃gate_1, gate_1 = Gates.mul Test_1 Test_2 ∧
-    ∃gate_2, Gates.div gate_0 gate_1 gate_2 ∧
-    Gates.is_bool (9:F) ∧
-    k gate_2
-
-def MySecondWidget_9 (Test_1: F) (Test_2: F) : Prop :=
-    ∃gate_0, gate_0 = Gates.mul Test_1 Test_2 ∧
-    MyWidget_9 Test_1 Test_2 fun gate_1 =>
-    ∃_ignored_, _ignored_ = Gates.mul gate_0 gate_1 ∧
-    True
-
-end MultipleGadgets
\ No newline at end of file
diff --git a/test/TestExtractGadgetsVectors.lean b/test/TestExtractGadgetsVectors.lean
deleted file mode 100644
index 19d8286..0000000
--- a/test/TestExtractGadgetsVectors.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace MultipleGadgetsVectors
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def VectorGadget_3_3_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (Nested: Vector (Vector F 3) 3) (k: Vector F 3 -> Prop): Prop :=
-    ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧
-    ∃_ignored_, _ignored_ = Gates.mul In_1[1] In_2[1] ∧
-    ∃gate_2, gate_2 = Gates.mul In_1[2] In_2[2] ∧
-    k vec![gate_2, gate_2, gate_2]
-
-def ReturnItself_3_3 (In_1: Vector F 3) (Out: Vector F 3) (k: Vector F 3 -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.mul In_1[0] In_1[0] ∧
-    ∃gate_1, gate_1 = Gates.mul In_1[1] In_1[1] ∧
-    ∃gate_2, gate_2 = Gates.mul In_1[2] In_1[2] ∧
-    k vec![gate_0, gate_1, gate_2]
-
-def OptimisedVectorGadget (In: F) (k: Vector F 3 -> Prop): Prop :=
-    ∃gate_0, Gates.to_binary In 3 gate_0 ∧
-    k gate_0
-
-end MultipleGadgetsVectors
\ No newline at end of file
diff --git a/test/TestGadgetExtraction.lean b/test/TestGadgetExtraction.lean
deleted file mode 100644
index 5faa800..0000000
--- a/test/TestGadgetExtraction.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace VectorGadget
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def VectorGadget_3_3_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (Nested: Vector (Vector F 3) 3) (k: Vector F 3 -> Prop): Prop :=
-    ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧
-    ∃_ignored_, _ignored_ = Gates.mul In_1[1] In_2[1] ∧
-    ∃gate_2, gate_2 = Gates.mul In_1[2] In_2[2] ∧
-    k vec![gate_2, gate_2, gate_2]
-
-end VectorGadget
\ No newline at end of file
diff --git a/test/TestMerkleRecover.lean b/test/TestMerkleRecover.lean
deleted file mode 100644
index e70d028..0000000
--- a/test/TestMerkleRecover.lean
+++ /dev/null
@@ -1,80 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace MerkleRecover
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧
-    k gate_0
-
-def circuit (Root: F) (Element: F) (Path: Vector F 20) (Proof: Vector F 20): Prop :=
-    DummyHash Element Proof[0] fun gate_0 =>
-    DummyHash Proof[0] Element fun gate_1 =>
-    ∃gate_2, Gates.select Path[0] gate_1 gate_0 gate_2 ∧
-    DummyHash gate_2 Proof[1] fun gate_3 =>
-    DummyHash Proof[1] gate_2 fun gate_4 =>
-    ∃gate_5, Gates.select Path[1] gate_4 gate_3 gate_5 ∧
-    DummyHash gate_5 Proof[2] fun gate_6 =>
-    DummyHash Proof[2] gate_5 fun gate_7 =>
-    ∃gate_8, Gates.select Path[2] gate_7 gate_6 gate_8 ∧
-    DummyHash gate_8 Proof[3] fun gate_9 =>
-    DummyHash Proof[3] gate_8 fun gate_10 =>
-    ∃gate_11, Gates.select Path[3] gate_10 gate_9 gate_11 ∧
-    DummyHash gate_11 Proof[4] fun gate_12 =>
-    DummyHash Proof[4] gate_11 fun gate_13 =>
-    ∃gate_14, Gates.select Path[4] gate_13 gate_12 gate_14 ∧
-    DummyHash gate_14 Proof[5] fun gate_15 =>
-    DummyHash Proof[5] gate_14 fun gate_16 =>
-    ∃gate_17, Gates.select Path[5] gate_16 gate_15 gate_17 ∧
-    DummyHash gate_17 Proof[6] fun gate_18 =>
-    DummyHash Proof[6] gate_17 fun gate_19 =>
-    ∃gate_20, Gates.select Path[6] gate_19 gate_18 gate_20 ∧
-    DummyHash gate_20 Proof[7] fun gate_21 =>
-    DummyHash Proof[7] gate_20 fun gate_22 =>
-    ∃gate_23, Gates.select Path[7] gate_22 gate_21 gate_23 ∧
-    DummyHash gate_23 Proof[8] fun gate_24 =>
-    DummyHash Proof[8] gate_23 fun gate_25 =>
-    ∃gate_26, Gates.select Path[8] gate_25 gate_24 gate_26 ∧
-    DummyHash gate_26 Proof[9] fun gate_27 =>
-    DummyHash Proof[9] gate_26 fun gate_28 =>
-    ∃gate_29, Gates.select Path[9] gate_28 gate_27 gate_29 ∧
-    DummyHash gate_29 Proof[10] fun gate_30 =>
-    DummyHash Proof[10] gate_29 fun gate_31 =>
-    ∃gate_32, Gates.select Path[10] gate_31 gate_30 gate_32 ∧
-    DummyHash gate_32 Proof[11] fun gate_33 =>
-    DummyHash Proof[11] gate_32 fun gate_34 =>
-    ∃gate_35, Gates.select Path[11] gate_34 gate_33 gate_35 ∧
-    DummyHash gate_35 Proof[12] fun gate_36 =>
-    DummyHash Proof[12] gate_35 fun gate_37 =>
-    ∃gate_38, Gates.select Path[12] gate_37 gate_36 gate_38 ∧
-    DummyHash gate_38 Proof[13] fun gate_39 =>
-    DummyHash Proof[13] gate_38 fun gate_40 =>
-    ∃gate_41, Gates.select Path[13] gate_40 gate_39 gate_41 ∧
-    DummyHash gate_41 Proof[14] fun gate_42 =>
-    DummyHash Proof[14] gate_41 fun gate_43 =>
-    ∃gate_44, Gates.select Path[14] gate_43 gate_42 gate_44 ∧
-    DummyHash gate_44 Proof[15] fun gate_45 =>
-    DummyHash Proof[15] gate_44 fun gate_46 =>
-    ∃gate_47, Gates.select Path[15] gate_46 gate_45 gate_47 ∧
-    DummyHash gate_47 Proof[16] fun gate_48 =>
-    DummyHash Proof[16] gate_47 fun gate_49 =>
-    ∃gate_50, Gates.select Path[16] gate_49 gate_48 gate_50 ∧
-    DummyHash gate_50 Proof[17] fun gate_51 =>
-    DummyHash Proof[17] gate_50 fun gate_52 =>
-    ∃gate_53, Gates.select Path[17] gate_52 gate_51 gate_53 ∧
-    DummyHash gate_53 Proof[18] fun gate_54 =>
-    DummyHash Proof[18] gate_53 fun gate_55 =>
-    ∃gate_56, Gates.select Path[18] gate_55 gate_54 gate_56 ∧
-    DummyHash gate_56 Proof[19] fun gate_57 =>
-    DummyHash Proof[19] gate_56 fun gate_58 =>
-    ∃gate_59, Gates.select Path[19] gate_58 gate_57 gate_59 ∧
-    Gates.eq gate_59 Root ∧
-    True
-
-end MerkleRecover
\ No newline at end of file
diff --git a/test/TestMyCircuit.lean b/test/TestMyCircuit.lean
deleted file mode 100644
index 431f4f8..0000000
--- a/test/TestMyCircuit.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace MyCircuit
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-
-
-def circuit (In_1: F) (In_2: F) (Out: F): Prop :=
-    ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧
-    Gates.eq gate_0 Out ∧
-    True
-
-end MyCircuit
\ No newline at end of file
diff --git a/test/TestSlicesOptimisation.lean b/test/TestSlicesOptimisation.lean
deleted file mode 100644
index 15dab1c..0000000
--- a/test/TestSlicesOptimisation.lean
+++ /dev/null
@@ -1,35 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace SlicesOptimisation
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def SlicesGadget_3_2_4_3_2 (TwoDim: Vector (Vector F 3) 2) (ThreeDim: Vector (Vector (Vector F 4) 3) 2) (k: Vector F 7 -> Prop): Prop :=
-    k vec![ThreeDim[0][0][0], ThreeDim[0][0][1], ThreeDim[0][0][2], ThreeDim[0][0][3], TwoDim[0][0], TwoDim[0][1], TwoDim[0][2]]
-
-def SlicesGadget_1_2_4_3_3 (TwoDim: Vector (Vector F 1) 2) (ThreeDim: Vector (Vector (Vector F 4) 3) 3) (k: Vector F 5 -> Prop): Prop :=
-    k vec![ThreeDim[0][0][0], ThreeDim[0][0][1], ThreeDim[0][0][2], ThreeDim[0][0][3], TwoDim[0][0]]
-
-def TwoSlices_3_2 (TwoDim: Vector (Vector F 3) 2) (k: Vector (Vector F 3) 2 -> Prop): Prop :=
-    k TwoDim
-
-def ThreeSlices_4_3_2 (ThreeDim: Vector (Vector (Vector F 4) 3) 2) (k: Vector (Vector (Vector F 4) 3) 2 -> Prop): Prop :=
-    k ThreeDim
-
-def circuit (Test: F) (Id: Vector F 3) (TwoDim: Vector (Vector F 3) 2) (ThreeDim: Vector (Vector (Vector F 4) 3) 2): Prop :=
-    SlicesGadget_3_2_4_3_2 TwoDim ThreeDim fun _ =>
-    SlicesGadget_3_2_4_3_2 vec![TwoDim[1], TwoDim[0]] vec![vec![ThreeDim[1][0], ThreeDim[1][1], ThreeDim[1][2]], vec![ThreeDim[0][0], ThreeDim[0][1], ThreeDim[0][2]]] fun _ =>
-    SlicesGadget_1_2_4_3_3 vec![vec![TwoDim[1][1]], vec![TwoDim[1][0]]] vec![vec![ThreeDim[1][0], ThreeDim[1][1], ThreeDim[1][2]], vec![ThreeDim[0][0], ThreeDim[0][1], ThreeDim[0][2]], vec![ThreeDim[1][0], ThreeDim[1][1], ThreeDim[1][2]]] fun _ =>
-    SlicesGadget_3_2_4_3_2 vec![TwoDim[1], vec![TwoDim[1][0], TwoDim[0][0], TwoDim[1][1]]] ThreeDim fun _ =>
-    TwoSlices_3_2 TwoDim fun _ =>
-    ThreeSlices_4_3_2 ThreeDim fun gate_5 =>
-    ThreeSlices_4_3_2 gate_5 fun gate_6 =>
-    ThreeSlices_4_3_2 gate_6 fun _ =>
-    True
-
-end SlicesOptimisation
\ No newline at end of file
diff --git a/test/TestToBinaryCircuit.lean b/test/TestToBinaryCircuit.lean
deleted file mode 100644
index 01a2ca9..0000000
--- a/test/TestToBinaryCircuit.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace ToBinaryCircuit
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def VectorGadget_3_3_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (Nested: Vector (Vector F 3) 3) (k: Vector F 3 -> Prop): Prop :=
-    ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧
-    ∃_ignored_, _ignored_ = Gates.mul In_1[1] In_2[1] ∧
-    ∃gate_2, gate_2 = Gates.mul In_1[2] In_2[2] ∧
-    k vec![gate_2, gate_2, gate_2]
-
-def circuit (In: F) (Out: F) (Double: Vector (Vector F 3) 3): Prop :=
-    ∃gate_0, Gates.to_binary In 3 gate_0 ∧
-    ∃gate_1, Gates.to_binary Out 3 gate_1 ∧
-    ∃_ignored_, _ignored_ = Gates.add Double[2][2] Double[1][1] ∧
-    ∃_ignored_, _ignored_ = Gates.add _ignored_ Double[0][0] ∧
-    ∃_ignored_, _ignored_ = Gates.mul gate_0[1] gate_1[1] ∧
-    VectorGadget_3_3_3_3 Double[2] Double[0] Double fun gate_4 =>
-    ∃_ignored_, _ignored_ = Gates.mul gate_4[2] gate_4[1] ∧
-    True
-
-end ToBinaryCircuit
\ No newline at end of file
diff --git a/test/TestTwoGadgets.lean b/test/TestTwoGadgets.lean
deleted file mode 100644
index 764688d..0000000
--- a/test/TestTwoGadgets.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-import ProvenZk.Gates
-import ProvenZk.Ext.Vector
-
-set_option linter.unusedVariables false
-
-namespace TwoGadgets
-
-def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
-variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order
-
-def MyWidget_11 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop :=
-    ∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧
-    ∃gate_1, gate_1 = Gates.mul Test_1 Test_2 ∧
-    ∃gate_2, Gates.div gate_0 gate_1 gate_2 ∧
-    Gates.is_bool (11:F) ∧
-    k gate_2
-
-def MySecondWidget_11 (Test_1: F) (Test_2: F) : Prop :=
-    ∃gate_0, gate_0 = Gates.mul Test_1 Test_2 ∧
-    MyWidget_11 Test_1 Test_2 fun gate_1 =>
-    ∃_ignored_, _ignored_ = Gates.mul gate_0 gate_1 ∧
-    True
-
-def circuit (In_1: F) (In_2: F): Prop :=
-    ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧
-    ∃gate_1, gate_1 = Gates.mul In_1 In_2 ∧
-    MySecondWidget_11 gate_0 gate_1 ∧
-    True
-
-end TwoGadgets
\ No newline at end of file