From 80cda935d01ed24c28a094158fe6162314e0ad56 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Thu, 31 Aug 2023 21:07:52 +0100
Subject: [PATCH 1/5] Added CI and Lean files

---
 .github/workflows/test.yml                    | 36 ++++++++++++++-----
 .gitignore                                    |  7 ++++
 README.md                                     |  3 ++
 {prover => go-circuit}/circuit.go             |  4 +--
 {prover => go-circuit}/keccak/constants.go    |  0
 {prover => go-circuit}/keccak/keccak.go       |  0
 {prover => go-circuit}/keccak/keccak_test.go  |  0
 {prover => go-circuit}/marshal.go             |  0
 {prover => go-circuit}/poseidon/constants.go  |  0
 {prover => go-circuit}/poseidon/poseidon.go   |  0
 .../poseidon/poseidon_test.go                 |  0
 {prover => go-circuit}/proving_system.go      |  4 +++
 integration_test.go                           |  2 +-
 lean-circuit/LeanCircuit.lean                 |  0
 lean-circuit/Main.lean                        |  5 +++
 lean-circuit/lakefile.lean                    | 22 ++++++++++++
 lean-circuit/lean-toolchain                   |  1 +
 main.go                                       | 28 ++++++++++++++-
 server/server.go                              |  2 +-
 19 files changed, 100 insertions(+), 14 deletions(-)
 rename {prover => go-circuit}/circuit.go (98%)
 rename {prover => go-circuit}/keccak/constants.go (100%)
 rename {prover => go-circuit}/keccak/keccak.go (100%)
 rename {prover => go-circuit}/keccak/keccak_test.go (100%)
 rename {prover => go-circuit}/marshal.go (100%)
 rename {prover => go-circuit}/poseidon/constants.go (100%)
 rename {prover => go-circuit}/poseidon/poseidon.go (100%)
 rename {prover => go-circuit}/poseidon/poseidon_test.go (100%)
 rename {prover => go-circuit}/proving_system.go (98%)
 create mode 100644 lean-circuit/LeanCircuit.lean
 create mode 100644 lean-circuit/Main.lean
 create mode 100644 lean-circuit/lakefile.lean
 create mode 100644 lean-circuit/lean-toolchain

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 27d170e..b86ea86 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -3,13 +3,31 @@ on: push
 jobs:
   build-and-test:
     runs-on: ubuntu-latest
+    timeout-minutes: 600
     steps:
-      - uses: actions/checkout@v2
-      - name: Set up Go
-        uses: actions/setup-go@v2
-        with:
-          go-version: 1.20.3
-      - name: Build
-        run: go build
-      - name: Test
-        run: go test
\ No newline at end of file
+    - name: Checkout repo
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+    - name: Install Elan
+      run: |
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y -v --default-toolchain leanprover/lean4:nightly-2023-07-12
+        echo "LAKE_VERSION=$(~/.elan/bin/lake --version)" >> $GITHUB_ENV
+    - name: Cache dependencies
+      uses: actions/cache@v3
+      with:
+        path: lean-circuit/lake-packages
+        key: "${{ env.LAKE_VERSION }}"
+    - name: Set up Go
+      uses: actions/setup-go@v4
+      with:
+        go-version-file: './go.mod'
+    - name: Build
+      run: go build
+    - name: Export circuit
+      run: ./gnark-mbu extract-circuit --output=lean-circuit/LeanCircuit.lean
+    - name: Build lean project
+      run: |
+        cd lean-circuit
+        ~/.elan/bin/lake exe cache get
+        ~/.elan/bin/lake build
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
index 2da97aa..6af4cd5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,10 @@
 .idea
 out
 gnark-mbu
+gnark-mbu.exe
+
+lean-circuit/build
+lean-circuit/.cache
+lean-circuit/lean-packages/*
+lean-circuit/lake-packages/*
+!lean-circuit/lean-packages/manifest.json
diff --git a/README.md b/README.md
index e0f0edf..c1f4591 100644
--- a/README.md
+++ b/README.md
@@ -54,6 +54,9 @@ This part explains the existing cli commands.
         1. output *file path* - File to be writen to  
         2. tree-depth *n* - Depth of a tree  
         3. batch-size *n* - Batch size for Merkle tree updates
+8. extract-circuit - Transpiles the circuit from gnark to Lean
+    Flags:  
+        1. output *file path* - File to be writen to
 
 ## Benchmarks
 
diff --git a/prover/circuit.go b/go-circuit/circuit.go
similarity index 98%
rename from prover/circuit.go
rename to go-circuit/circuit.go
index 73d6dd6..7ed4bdc 100644
--- a/prover/circuit.go
+++ b/go-circuit/circuit.go
@@ -2,8 +2,8 @@ package prover
 
 import (
 	"strconv"
-	"worldcoin/gnark-mbu/prover/keccak"
-	"worldcoin/gnark-mbu/prover/poseidon"
+	"worldcoin/gnark-mbu/go-circuit/keccak"
+	"worldcoin/gnark-mbu/go-circuit/poseidon"
 
 	"github.com/consensys/gnark/frontend"
 )
diff --git a/prover/keccak/constants.go b/go-circuit/keccak/constants.go
similarity index 100%
rename from prover/keccak/constants.go
rename to go-circuit/keccak/constants.go
diff --git a/prover/keccak/keccak.go b/go-circuit/keccak/keccak.go
similarity index 100%
rename from prover/keccak/keccak.go
rename to go-circuit/keccak/keccak.go
diff --git a/prover/keccak/keccak_test.go b/go-circuit/keccak/keccak_test.go
similarity index 100%
rename from prover/keccak/keccak_test.go
rename to go-circuit/keccak/keccak_test.go
diff --git a/prover/marshal.go b/go-circuit/marshal.go
similarity index 100%
rename from prover/marshal.go
rename to go-circuit/marshal.go
diff --git a/prover/poseidon/constants.go b/go-circuit/poseidon/constants.go
similarity index 100%
rename from prover/poseidon/constants.go
rename to go-circuit/poseidon/constants.go
diff --git a/prover/poseidon/poseidon.go b/go-circuit/poseidon/poseidon.go
similarity index 100%
rename from prover/poseidon/poseidon.go
rename to go-circuit/poseidon/poseidon.go
diff --git a/prover/poseidon/poseidon_test.go b/go-circuit/poseidon/poseidon_test.go
similarity index 100%
rename from prover/poseidon/poseidon_test.go
rename to go-circuit/poseidon/poseidon_test.go
diff --git a/prover/proving_system.go b/go-circuit/proving_system.go
similarity index 98%
rename from prover/proving_system.go
rename to go-circuit/proving_system.go
index 63fdc0d..9380fc4 100644
--- a/prover/proving_system.go
+++ b/go-circuit/proving_system.go
@@ -112,6 +112,10 @@ func Setup(treeDepth uint32, batchSize uint32) (*ProvingSystem, error) {
 	return &ProvingSystem{treeDepth, batchSize, pk, vk, ccs}, nil
 }
 
+func ExtractLean() (string, error) {
+	return "", nil
+}
+
 func (ps *ProvingSystem) ExportSolidity(writer io.Writer) error {
 	return ps.VerifyingKey.ExportSolidity(writer)
 }
diff --git a/integration_test.go b/integration_test.go
index a4006d1..7c54e4a 100644
--- a/integration_test.go
+++ b/integration_test.go
@@ -6,7 +6,7 @@ import (
 	"strings"
 	"testing"
 	"worldcoin/gnark-mbu/logging"
-	"worldcoin/gnark-mbu/prover"
+	"worldcoin/gnark-mbu/go-circuit"
 	"worldcoin/gnark-mbu/server"
 )
 
diff --git a/lean-circuit/LeanCircuit.lean b/lean-circuit/LeanCircuit.lean
new file mode 100644
index 0000000..e69de29
diff --git a/lean-circuit/Main.lean b/lean-circuit/Main.lean
new file mode 100644
index 0000000..f3db683
--- /dev/null
+++ b/lean-circuit/Main.lean
@@ -0,0 +1,5 @@
+import ProvenZk.Binary
+import ProvenZk.Hash
+import ProvenZk.Merkle
+
+def main : IO Unit := pure ()
\ No newline at end of file
diff --git a/lean-circuit/lakefile.lean b/lean-circuit/lakefile.lean
new file mode 100644
index 0000000..a468f67
--- /dev/null
+++ b/lean-circuit/lakefile.lean
@@ -0,0 +1,22 @@
+import Lake
+open Lake DSL
+
+package «lean-circuit» {
+  -- add package configuration options here
+}
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"@"ea67efc21e4e1496f0a1d954cd0c0a952523133a"
+
+require ProvenZK from git
+  "https://github.com/reilabs/proven-zk.git"@"v1.0.0"
+
+lean_lib LeanCircuit {
+  -- add library configuration options here
+}
+
+@[default_target]
+lean_exe «lean-circuit» {
+  moreLeanArgs := #["--tstack=1000000"]
+  root := `Main
+}
diff --git a/lean-circuit/lean-toolchain b/lean-circuit/lean-toolchain
new file mode 100644
index 0000000..6be6051
--- /dev/null
+++ b/lean-circuit/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-07-12
diff --git a/main.go b/main.go
index 28a6fcf..5eee2be 100644
--- a/main.go
+++ b/main.go
@@ -10,7 +10,7 @@ import (
 	"os"
 	"os/signal"
 	"worldcoin/gnark-mbu/logging"
-	"worldcoin/gnark-mbu/prover"
+	"worldcoin/gnark-mbu/go-circuit"
 	"worldcoin/gnark-mbu/server"
 )
 
@@ -235,6 +235,32 @@ func main() {
 					return nil
 				},
 			},
+			{
+				Name: "extract-circuit",
+				Flags: []cli.Flag{
+					&cli.StringFlag{Name: "output", Usage: "Output file", Required: true},
+				},
+				Action: func(context *cli.Context) error {
+					path := context.String("output")
+					logging.Logger().Info().Msg("Extracting gnark circuit to Lean")
+					circuit_string, err := prover.ExtractLean()
+					if err != nil {
+						return err
+					}
+					file, err := os.Create(path)
+					defer file.Close()
+					if err != nil {
+						return err
+					}
+					written, err := file.WriteString(circuit_string)
+					if err != nil {
+						return err
+					}
+					logging.Logger().Info().Int("bytesWritten", written).Msg("Lean circuit written to file")
+
+					return nil
+				},
+			},
 		},
 	}
 
diff --git a/server/server.go b/server/server.go
index 244c7ef..01eb481 100644
--- a/server/server.go
+++ b/server/server.go
@@ -9,7 +9,7 @@ import (
 	"worldcoin/gnark-mbu/logging"
 
 	"github.com/prometheus/client_golang/prometheus/promhttp"
-	"worldcoin/gnark-mbu/prover"
+	"worldcoin/gnark-mbu/go-circuit"
 )
 
 type Error struct {

From 35413cc8435f21bb2d825c727af7a18cd1f67404 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Thu, 31 Aug 2023 21:13:28 +0100
Subject: [PATCH 2/5] Added lake manifest

---
 .gitignore                      |  2 +-
 lean-circuit/lake-manifest.json | 45 +++++++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 1 deletion(-)
 create mode 100644 lean-circuit/lake-manifest.json

diff --git a/.gitignore b/.gitignore
index 6af4cd5..6a69267 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,4 +7,4 @@ lean-circuit/build
 lean-circuit/.cache
 lean-circuit/lean-packages/*
 lean-circuit/lake-packages/*
-!lean-circuit/lean-packages/manifest.json
+!lean-circuit/lake-manifest.json
diff --git a/lean-circuit/lake-manifest.json b/lean-circuit/lake-manifest.json
new file mode 100644
index 0000000..144219f
--- /dev/null
+++ b/lean-circuit/lake-manifest.json
@@ -0,0 +1,45 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/EdAyers/ProofWidgets4",
+    "subDir?": null,
+    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.11"}},
+  {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "name": "Cli",
+    "inputRev?": "nightly"}},
+  {"git":
+   {"url": "https://github.com/reilabs/proven-zk.git",
+    "subDir?": null,
+    "rev": "08431b93eeef80f6acbf3d6a6401c02d849f6864",
+    "name": "ProvenZK",
+    "inputRev?": "v1.0.0"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "ea67efc21e4e1496f0a1d954cd0c0a952523133a",
+    "name": "mathlib",
+    "inputRev?": "ea67efc21e4e1496f0a1d954cd0c0a952523133a"}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+    "name": "std",
+    "inputRev?": "main"}}]}

From fd93aeeb4e8f218f8b8bfe0a328260196ba77a40 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Thu, 31 Aug 2023 22:35:10 +0100
Subject: [PATCH 3/5] Reverted structure

---
 .github/workflows/test.yml                             |  6 +++---
 .gitignore                                             | 10 +++++-----
 integration_test.go                                    |  2 +-
 .../{LeanCircuit.lean => FormalVerification.lean}      |  0
 lean-circuit/lake-packages/Cli                         |  1 +
 lean-circuit/lake-packages/ProvenZK                    |  1 +
 lean-circuit/lake-packages/Qq                          |  1 +
 lean-circuit/lake-packages/aesop                       |  1 +
 lean-circuit/lake-packages/mathlib                     |  1 +
 lean-circuit/lake-packages/proofwidgets                |  1 +
 lean-circuit/lake-packages/std                         |  1 +
 lean-circuit/lakefile.lean                             |  6 +++---
 main.go                                                |  2 +-
 {go-circuit => prover}/circuit.go                      |  4 ++--
 {go-circuit => prover}/keccak/constants.go             |  0
 {go-circuit => prover}/keccak/keccak.go                |  0
 {go-circuit => prover}/keccak/keccak_test.go           |  0
 {go-circuit => prover}/marshal.go                      |  0
 {go-circuit => prover}/poseidon/constants.go           |  0
 {go-circuit => prover}/poseidon/poseidon.go            |  0
 {go-circuit => prover}/poseidon/poseidon_test.go       |  0
 {go-circuit => prover}/proving_system.go               |  0
 server/server.go                                       |  2 +-
 23 files changed, 23 insertions(+), 16 deletions(-)
 rename lean-circuit/{LeanCircuit.lean => FormalVerification.lean} (100%)
 create mode 160000 lean-circuit/lake-packages/Cli
 create mode 160000 lean-circuit/lake-packages/ProvenZK
 create mode 160000 lean-circuit/lake-packages/Qq
 create mode 160000 lean-circuit/lake-packages/aesop
 create mode 160000 lean-circuit/lake-packages/mathlib
 create mode 160000 lean-circuit/lake-packages/proofwidgets
 create mode 160000 lean-circuit/lake-packages/std
 rename {go-circuit => prover}/circuit.go (98%)
 rename {go-circuit => prover}/keccak/constants.go (100%)
 rename {go-circuit => prover}/keccak/keccak.go (100%)
 rename {go-circuit => prover}/keccak/keccak_test.go (100%)
 rename {go-circuit => prover}/marshal.go (100%)
 rename {go-circuit => prover}/poseidon/constants.go (100%)
 rename {go-circuit => prover}/poseidon/poseidon.go (100%)
 rename {go-circuit => prover}/poseidon/poseidon_test.go (100%)
 rename {go-circuit => prover}/proving_system.go (100%)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index b86ea86..2479cc0 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -16,7 +16,7 @@ jobs:
     - name: Cache dependencies
       uses: actions/cache@v3
       with:
-        path: lean-circuit/lake-packages
+        path: formal-verification/lake-packages
         key: "${{ env.LAKE_VERSION }}"
     - name: Set up Go
       uses: actions/setup-go@v4
@@ -25,9 +25,9 @@ jobs:
     - name: Build
       run: go build
     - name: Export circuit
-      run: ./gnark-mbu extract-circuit --output=lean-circuit/LeanCircuit.lean
+      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean
     - name: Build lean project
       run: |
-        cd lean-circuit
+        cd formal-verification
         ~/.elan/bin/lake exe cache get
         ~/.elan/bin/lake build
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
index 6a69267..8f53355 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,8 +3,8 @@ out
 gnark-mbu
 gnark-mbu.exe
 
-lean-circuit/build
-lean-circuit/.cache
-lean-circuit/lean-packages/*
-lean-circuit/lake-packages/*
-!lean-circuit/lake-manifest.json
+formal-verification/build
+formal-verification/.cache
+formal-verification/lean-packages/*
+formal-verification/lake-packages/*
+!formal-verification/lake-manifest.json
diff --git a/integration_test.go b/integration_test.go
index 7c54e4a..a4006d1 100644
--- a/integration_test.go
+++ b/integration_test.go
@@ -6,7 +6,7 @@ import (
 	"strings"
 	"testing"
 	"worldcoin/gnark-mbu/logging"
-	"worldcoin/gnark-mbu/go-circuit"
+	"worldcoin/gnark-mbu/prover"
 	"worldcoin/gnark-mbu/server"
 )
 
diff --git a/lean-circuit/LeanCircuit.lean b/lean-circuit/FormalVerification.lean
similarity index 100%
rename from lean-circuit/LeanCircuit.lean
rename to lean-circuit/FormalVerification.lean
diff --git a/lean-circuit/lake-packages/Cli b/lean-circuit/lake-packages/Cli
new file mode 160000
index 0000000..5a858c3
--- /dev/null
+++ b/lean-circuit/lake-packages/Cli
@@ -0,0 +1 @@
+Subproject commit 5a858c32963b6b19be0d477a30a1f4b6c120be7e
diff --git a/lean-circuit/lake-packages/ProvenZK b/lean-circuit/lake-packages/ProvenZK
new file mode 160000
index 0000000..08431b9
--- /dev/null
+++ b/lean-circuit/lake-packages/ProvenZK
@@ -0,0 +1 @@
+Subproject commit 08431b93eeef80f6acbf3d6a6401c02d849f6864
diff --git a/lean-circuit/lake-packages/Qq b/lean-circuit/lake-packages/Qq
new file mode 160000
index 0000000..c0d9516
--- /dev/null
+++ b/lean-circuit/lake-packages/Qq
@@ -0,0 +1 @@
+Subproject commit c0d9516f44d07feee01c1103c8f2f7c24a822b55
diff --git a/lean-circuit/lake-packages/aesop b/lean-circuit/lake-packages/aesop
new file mode 160000
index 0000000..f04538a
--- /dev/null
+++ b/lean-circuit/lake-packages/aesop
@@ -0,0 +1 @@
+Subproject commit f04538ab6ad07642368cf11d2702acc0a9b4bcee
diff --git a/lean-circuit/lake-packages/mathlib b/lean-circuit/lake-packages/mathlib
new file mode 160000
index 0000000..ea67efc
--- /dev/null
+++ b/lean-circuit/lake-packages/mathlib
@@ -0,0 +1 @@
+Subproject commit ea67efc21e4e1496f0a1d954cd0c0a952523133a
diff --git a/lean-circuit/lake-packages/proofwidgets b/lean-circuit/lake-packages/proofwidgets
new file mode 160000
index 0000000..c43db94
--- /dev/null
+++ b/lean-circuit/lake-packages/proofwidgets
@@ -0,0 +1 @@
+Subproject commit c43db94a8f495dad37829e9d7ad65483d68c86b8
diff --git a/lean-circuit/lake-packages/std b/lean-circuit/lake-packages/std
new file mode 160000
index 0000000..dff883c
--- /dev/null
+++ b/lean-circuit/lake-packages/std
@@ -0,0 +1 @@
+Subproject commit dff883c55395438ae2a5c65ad5ddba084b600feb
diff --git a/lean-circuit/lakefile.lean b/lean-circuit/lakefile.lean
index a468f67..01a6328 100644
--- a/lean-circuit/lakefile.lean
+++ b/lean-circuit/lakefile.lean
@@ -1,7 +1,7 @@
 import Lake
 open Lake DSL
 
-package «lean-circuit» {
+package «formal-verification» {
   -- add package configuration options here
 }
 
@@ -11,12 +11,12 @@ require mathlib from git
 require ProvenZK from git
   "https://github.com/reilabs/proven-zk.git"@"v1.0.0"
 
-lean_lib LeanCircuit {
+lean_lib FormalVerification {
   -- add library configuration options here
 }
 
 @[default_target]
-lean_exe «lean-circuit» {
+lean_exe «formal-verification» {
   moreLeanArgs := #["--tstack=1000000"]
   root := `Main
 }
diff --git a/main.go b/main.go
index 5eee2be..e6c5e3f 100644
--- a/main.go
+++ b/main.go
@@ -10,7 +10,7 @@ import (
 	"os"
 	"os/signal"
 	"worldcoin/gnark-mbu/logging"
-	"worldcoin/gnark-mbu/go-circuit"
+	"worldcoin/gnark-mbu/prover"
 	"worldcoin/gnark-mbu/server"
 )
 
diff --git a/go-circuit/circuit.go b/prover/circuit.go
similarity index 98%
rename from go-circuit/circuit.go
rename to prover/circuit.go
index 7ed4bdc..73d6dd6 100644
--- a/go-circuit/circuit.go
+++ b/prover/circuit.go
@@ -2,8 +2,8 @@ package prover
 
 import (
 	"strconv"
-	"worldcoin/gnark-mbu/go-circuit/keccak"
-	"worldcoin/gnark-mbu/go-circuit/poseidon"
+	"worldcoin/gnark-mbu/prover/keccak"
+	"worldcoin/gnark-mbu/prover/poseidon"
 
 	"github.com/consensys/gnark/frontend"
 )
diff --git a/go-circuit/keccak/constants.go b/prover/keccak/constants.go
similarity index 100%
rename from go-circuit/keccak/constants.go
rename to prover/keccak/constants.go
diff --git a/go-circuit/keccak/keccak.go b/prover/keccak/keccak.go
similarity index 100%
rename from go-circuit/keccak/keccak.go
rename to prover/keccak/keccak.go
diff --git a/go-circuit/keccak/keccak_test.go b/prover/keccak/keccak_test.go
similarity index 100%
rename from go-circuit/keccak/keccak_test.go
rename to prover/keccak/keccak_test.go
diff --git a/go-circuit/marshal.go b/prover/marshal.go
similarity index 100%
rename from go-circuit/marshal.go
rename to prover/marshal.go
diff --git a/go-circuit/poseidon/constants.go b/prover/poseidon/constants.go
similarity index 100%
rename from go-circuit/poseidon/constants.go
rename to prover/poseidon/constants.go
diff --git a/go-circuit/poseidon/poseidon.go b/prover/poseidon/poseidon.go
similarity index 100%
rename from go-circuit/poseidon/poseidon.go
rename to prover/poseidon/poseidon.go
diff --git a/go-circuit/poseidon/poseidon_test.go b/prover/poseidon/poseidon_test.go
similarity index 100%
rename from go-circuit/poseidon/poseidon_test.go
rename to prover/poseidon/poseidon_test.go
diff --git a/go-circuit/proving_system.go b/prover/proving_system.go
similarity index 100%
rename from go-circuit/proving_system.go
rename to prover/proving_system.go
diff --git a/server/server.go b/server/server.go
index 01eb481..244c7ef 100644
--- a/server/server.go
+++ b/server/server.go
@@ -9,7 +9,7 @@ import (
 	"worldcoin/gnark-mbu/logging"
 
 	"github.com/prometheus/client_golang/prometheus/promhttp"
-	"worldcoin/gnark-mbu/go-circuit"
+	"worldcoin/gnark-mbu/prover"
 )
 
 type Error struct {

From 5ed755288452c83cddd5904c47e2c175f167c78b Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Thu, 31 Aug 2023 22:36:36 +0100
Subject: [PATCH 4/5] Renamed lean-circuit to formal-verification

---
 {lean-circuit => formal-verification}/FormalVerification.lean | 0
 {lean-circuit => formal-verification}/Main.lean               | 0
 {lean-circuit => formal-verification}/lake-manifest.json      | 0
 {lean-circuit => formal-verification}/lakefile.lean           | 0
 {lean-circuit => formal-verification}/lean-toolchain          | 0
 lean-circuit/lake-packages/Cli                                | 1 -
 lean-circuit/lake-packages/ProvenZK                           | 1 -
 lean-circuit/lake-packages/Qq                                 | 1 -
 lean-circuit/lake-packages/aesop                              | 1 -
 lean-circuit/lake-packages/mathlib                            | 1 -
 lean-circuit/lake-packages/proofwidgets                       | 1 -
 lean-circuit/lake-packages/std                                | 1 -
 12 files changed, 7 deletions(-)
 rename {lean-circuit => formal-verification}/FormalVerification.lean (100%)
 rename {lean-circuit => formal-verification}/Main.lean (100%)
 rename {lean-circuit => formal-verification}/lake-manifest.json (100%)
 rename {lean-circuit => formal-verification}/lakefile.lean (100%)
 rename {lean-circuit => formal-verification}/lean-toolchain (100%)
 delete mode 160000 lean-circuit/lake-packages/Cli
 delete mode 160000 lean-circuit/lake-packages/ProvenZK
 delete mode 160000 lean-circuit/lake-packages/Qq
 delete mode 160000 lean-circuit/lake-packages/aesop
 delete mode 160000 lean-circuit/lake-packages/mathlib
 delete mode 160000 lean-circuit/lake-packages/proofwidgets
 delete mode 160000 lean-circuit/lake-packages/std

diff --git a/lean-circuit/FormalVerification.lean b/formal-verification/FormalVerification.lean
similarity index 100%
rename from lean-circuit/FormalVerification.lean
rename to formal-verification/FormalVerification.lean
diff --git a/lean-circuit/Main.lean b/formal-verification/Main.lean
similarity index 100%
rename from lean-circuit/Main.lean
rename to formal-verification/Main.lean
diff --git a/lean-circuit/lake-manifest.json b/formal-verification/lake-manifest.json
similarity index 100%
rename from lean-circuit/lake-manifest.json
rename to formal-verification/lake-manifest.json
diff --git a/lean-circuit/lakefile.lean b/formal-verification/lakefile.lean
similarity index 100%
rename from lean-circuit/lakefile.lean
rename to formal-verification/lakefile.lean
diff --git a/lean-circuit/lean-toolchain b/formal-verification/lean-toolchain
similarity index 100%
rename from lean-circuit/lean-toolchain
rename to formal-verification/lean-toolchain
diff --git a/lean-circuit/lake-packages/Cli b/lean-circuit/lake-packages/Cli
deleted file mode 160000
index 5a858c3..0000000
--- a/lean-circuit/lake-packages/Cli
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 5a858c32963b6b19be0d477a30a1f4b6c120be7e
diff --git a/lean-circuit/lake-packages/ProvenZK b/lean-circuit/lake-packages/ProvenZK
deleted file mode 160000
index 08431b9..0000000
--- a/lean-circuit/lake-packages/ProvenZK
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 08431b93eeef80f6acbf3d6a6401c02d849f6864
diff --git a/lean-circuit/lake-packages/Qq b/lean-circuit/lake-packages/Qq
deleted file mode 160000
index c0d9516..0000000
--- a/lean-circuit/lake-packages/Qq
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit c0d9516f44d07feee01c1103c8f2f7c24a822b55
diff --git a/lean-circuit/lake-packages/aesop b/lean-circuit/lake-packages/aesop
deleted file mode 160000
index f04538a..0000000
--- a/lean-circuit/lake-packages/aesop
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit f04538ab6ad07642368cf11d2702acc0a9b4bcee
diff --git a/lean-circuit/lake-packages/mathlib b/lean-circuit/lake-packages/mathlib
deleted file mode 160000
index ea67efc..0000000
--- a/lean-circuit/lake-packages/mathlib
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit ea67efc21e4e1496f0a1d954cd0c0a952523133a
diff --git a/lean-circuit/lake-packages/proofwidgets b/lean-circuit/lake-packages/proofwidgets
deleted file mode 160000
index c43db94..0000000
--- a/lean-circuit/lake-packages/proofwidgets
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit c43db94a8f495dad37829e9d7ad65483d68c86b8
diff --git a/lean-circuit/lake-packages/std b/lean-circuit/lake-packages/std
deleted file mode 160000
index dff883c..0000000
--- a/lean-circuit/lake-packages/std
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit dff883c55395438ae2a5c65ad5ddba084b600feb

From ea0769f16d846b6c1855c78841e1e480c4b84222 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Fri, 1 Sep 2023 15:39:52 +0100
Subject: [PATCH 5/5] Added go test

---
 .github/workflows/test.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 2479cc0..7826320 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -24,6 +24,8 @@ jobs:
         go-version-file: './go.mod'
     - name: Build
       run: go build
+    - name: Test
+      run: go test
     - name: Export circuit
       run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean
     - name: Build lean project