From f1948a71a82521d51808f7e889e32de1e692df51 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Fri, 1 Sep 2023 15:38:46 +0100
Subject: [PATCH 01/12] Wip

---
 prover/circuit.go | 40 ++++++++++++++++++++++++++++++----------
 1 file changed, 30 insertions(+), 10 deletions(-)

diff --git a/prover/circuit.go b/prover/circuit.go
index d3651b0..4817739 100644
--- a/prover/circuit.go
+++ b/prover/circuit.go
@@ -36,17 +36,33 @@ func (e *bitPatternLengthError) Error() string {
 	return "Bit pattern length was " + strconv.Itoa(e.actualLength) + " not a total number of bytes"
 }
 
-func VerifyProof(api frontend.API, proofSet, helper []frontend.Variable) frontend.Variable {
-	sum := proofSet[0]
-	for i := 1; i < len(proofSet); i++ {
-		api.AssertIsBoolean(helper[i-1])
-		d1 := api.Select(helper[i-1], proofSet[i], sum)
-		d2 := api.Select(helper[i-1], sum, proofSet[i])
-		sum = abstractor.CallGadget(api, poseidon.Poseidon2{In1: d1, In2: d2})[0]
+type VerifyProof struct {
+	Helper   []frontend.Variable
+	ProofSet []frontend.Variable
+}
+
+func (gadget VerifyProof) DefineGadget(api abstractor.API) []frontend.Variable {
+	sum := gadget.ProofSet[0]
+	for i := 1; i < len(gadget.ProofSet); i++ {
+		api.AssertIsBoolean(gadget.Helper[i-1])
+		d1 := api.Select(gadget.Helper[i-1], gadget.ProofSet[i], sum)
+		d2 := api.Select(gadget.Helper[i-1], sum, gadget.ProofSet[i])
+		sum = api.Call(poseidon.Poseidon2{In1: d1, In2: d2})[0]
 	}
-	return sum
+	return []frontend.Variable{sum}
 }
 
+// func VerifyProof(api frontend.API, proofSet, helper []frontend.Variable) frontend.Variable {
+// 	sum := proofSet[0]
+// 	for i := 1; i < len(proofSet); i++ {
+// 		api.AssertIsBoolean(helper[i-1])
+// 		d1 := api.Select(helper[i-1], proofSet[i], sum)
+// 		d2 := api.Select(helper[i-1], sum, proofSet[i])
+// 		sum = abstractor.CallGadget(api, poseidon.Poseidon2{In1: d1, In2: d2})[0]
+// 	}
+// 	return sum
+// }
+
 // SwapBitArrayEndianness Swaps the endianness of the bit pattern in bits,
 // returning the result in newBits.
 //
@@ -161,11 +177,15 @@ func (circuit *MbuCircuit) Define(api frontend.API) error {
 		currentPath := api.ToBinary(currentIndex, circuit.Depth)
 
 		// Verify proof for empty leaf.
-		root = VerifyProof(api, append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...), currentPath)
+		// root = VerifyProof(api, append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...), currentPath)
+		helper := append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...)
+		root = abstractor.CallGadget(api, VerifyProof{helper, currentPath})[0]
 		api.AssertIsEqual(root, prevRoot)
 
 		// Verify proof for idComm.
-		root = VerifyProof(api, append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...), currentPath)
+		// root = VerifyProof(api, append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...), currentPath)
+		helper = append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...)
+		root = abstractor.CallGadget(api, VerifyProof{helper, currentPath})[0]
 
 		// Set root for next iteration.
 		prevRoot = root

From 1777b91d8c945def5de89eabd00ad04ebbc6643c Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Fri, 1 Sep 2023 20:44:36 +0100
Subject: [PATCH 02/12] Wip

---
 prover/circuit.go | 23 +++++------------------
 1 file changed, 5 insertions(+), 18 deletions(-)

diff --git a/prover/circuit.go b/prover/circuit.go
index 4817739..ec27393 100644
--- a/prover/circuit.go
+++ b/prover/circuit.go
@@ -37,8 +37,8 @@ func (e *bitPatternLengthError) Error() string {
 }
 
 type VerifyProof struct {
-	Helper   []frontend.Variable
 	ProofSet []frontend.Variable
+	Helper   []frontend.Variable
 }
 
 func (gadget VerifyProof) DefineGadget(api abstractor.API) []frontend.Variable {
@@ -52,17 +52,6 @@ func (gadget VerifyProof) DefineGadget(api abstractor.API) []frontend.Variable {
 	return []frontend.Variable{sum}
 }
 
-// func VerifyProof(api frontend.API, proofSet, helper []frontend.Variable) frontend.Variable {
-// 	sum := proofSet[0]
-// 	for i := 1; i < len(proofSet); i++ {
-// 		api.AssertIsBoolean(helper[i-1])
-// 		d1 := api.Select(helper[i-1], proofSet[i], sum)
-// 		d2 := api.Select(helper[i-1], sum, proofSet[i])
-// 		sum = abstractor.CallGadget(api, poseidon.Poseidon2{In1: d1, In2: d2})[0]
-// 	}
-// 	return sum
-// }
-
 // SwapBitArrayEndianness Swaps the endianness of the bit pattern in bits,
 // returning the result in newBits.
 //
@@ -177,15 +166,13 @@ func (circuit *MbuCircuit) Define(api frontend.API) error {
 		currentPath := api.ToBinary(currentIndex, circuit.Depth)
 
 		// Verify proof for empty leaf.
-		// root = VerifyProof(api, append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...), currentPath)
-		helper := append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...)
-		root = abstractor.CallGadget(api, VerifyProof{helper, currentPath})[0]
+		proof := append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...)
+		root = abstractor.CallGadget(api, VerifyProof{ProofSet: proof, Helper: currentPath})[0]
 		api.AssertIsEqual(root, prevRoot)
 
 		// Verify proof for idComm.
-		// root = VerifyProof(api, append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...), currentPath)
-		helper = append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...)
-		root = abstractor.CallGadget(api, VerifyProof{helper, currentPath})[0]
+		proof = append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...)
+		root = abstractor.CallGadget(api, VerifyProof{ProofSet: proof, Helper: currentPath})[0]
 
 		// Set root for next iteration.
 		prevRoot = root

From 146ee4c2060ab8ec0ba63ec2180f8e54219037f6 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Fri, 1 Sep 2023 21:54:16 +0100
Subject: [PATCH 03/12] Gadget of VerifyProof

---
 .github/workflows/test.yml                  |   2 +-
 formal-verification/FormalVerification.lean | 123 +++++++++++++++++++-
 main.go                                     |   4 +-
 prover/circuit.go                           |  18 +--
 prover/proving_system.go                    |   5 +-
 5 files changed, 136 insertions(+), 16 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 7826320..70275f2 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -27,7 +27,7 @@ jobs:
     - name: Test
       run: go test
     - name: Export circuit
-      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean
+      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean --proof-size 30
     - name: Build lean project
       run: |
         cd formal-verification
diff --git a/formal-verification/FormalVerification.lean b/formal-verification/FormalVerification.lean
index 70a99d4..fb74125 100644
--- a/formal-verification/FormalVerification.lean
+++ b/formal-verification/FormalVerification.lean
@@ -1,7 +1,7 @@
 import ProvenZk.Gates
 import ProvenZk.Ext.Vector
 
-namespace Poseidon2
+namespace VerifyProof
 
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
@@ -124,4 +124,123 @@ def Poseidon2 (In1: F) (In2: F) (k: F -> Prop): Prop :=
     poseidon_3 vec![0, In1, In2] fun gate_0 =>
     k gate_0[0]
 
-end Poseidon2
\ No newline at end of file
+def VerifyProof_30_30 (Proof: Vector F 30) (Path: Vector F 30) (k: F -> Prop): Prop :=
+    Gates.is_bool Path[0] ∧
+    ∃gate_1, Gates.select Path[0] Proof[1] Proof[0] gate_1 ∧
+    ∃gate_2, Gates.select Path[0] Proof[0] Proof[1] gate_2 ∧
+    Poseidon2 gate_1 gate_2 fun gate_3 =>
+    Gates.is_bool Path[1] ∧
+    ∃gate_5, Gates.select Path[1] Proof[2] gate_3 gate_5 ∧
+    ∃gate_6, Gates.select Path[1] gate_3 Proof[2] gate_6 ∧
+    Poseidon2 gate_5 gate_6 fun gate_7 =>
+    Gates.is_bool Path[2] ∧
+    ∃gate_9, Gates.select Path[2] Proof[3] gate_7 gate_9 ∧
+    ∃gate_10, Gates.select Path[2] gate_7 Proof[3] gate_10 ∧
+    Poseidon2 gate_9 gate_10 fun gate_11 =>
+    Gates.is_bool Path[3] ∧
+    ∃gate_13, Gates.select Path[3] Proof[4] gate_11 gate_13 ∧
+    ∃gate_14, Gates.select Path[3] gate_11 Proof[4] gate_14 ∧
+    Poseidon2 gate_13 gate_14 fun gate_15 =>
+    Gates.is_bool Path[4] ∧
+    ∃gate_17, Gates.select Path[4] Proof[5] gate_15 gate_17 ∧
+    ∃gate_18, Gates.select Path[4] gate_15 Proof[5] gate_18 ∧
+    Poseidon2 gate_17 gate_18 fun gate_19 =>
+    Gates.is_bool Path[5] ∧
+    ∃gate_21, Gates.select Path[5] Proof[6] gate_19 gate_21 ∧
+    ∃gate_22, Gates.select Path[5] gate_19 Proof[6] gate_22 ∧
+    Poseidon2 gate_21 gate_22 fun gate_23 =>
+    Gates.is_bool Path[6] ∧
+    ∃gate_25, Gates.select Path[6] Proof[7] gate_23 gate_25 ∧
+    ∃gate_26, Gates.select Path[6] gate_23 Proof[7] gate_26 ∧
+    Poseidon2 gate_25 gate_26 fun gate_27 =>
+    Gates.is_bool Path[7] ∧
+    ∃gate_29, Gates.select Path[7] Proof[8] gate_27 gate_29 ∧
+    ∃gate_30, Gates.select Path[7] gate_27 Proof[8] gate_30 ∧
+    Poseidon2 gate_29 gate_30 fun gate_31 =>
+    Gates.is_bool Path[8] ∧
+    ∃gate_33, Gates.select Path[8] Proof[9] gate_31 gate_33 ∧
+    ∃gate_34, Gates.select Path[8] gate_31 Proof[9] gate_34 ∧
+    Poseidon2 gate_33 gate_34 fun gate_35 =>
+    Gates.is_bool Path[9] ∧
+    ∃gate_37, Gates.select Path[9] Proof[10] gate_35 gate_37 ∧
+    ∃gate_38, Gates.select Path[9] gate_35 Proof[10] gate_38 ∧
+    Poseidon2 gate_37 gate_38 fun gate_39 =>
+    Gates.is_bool Path[10] ∧
+    ∃gate_41, Gates.select Path[10] Proof[11] gate_39 gate_41 ∧
+    ∃gate_42, Gates.select Path[10] gate_39 Proof[11] gate_42 ∧
+    Poseidon2 gate_41 gate_42 fun gate_43 =>
+    Gates.is_bool Path[11] ∧
+    ∃gate_45, Gates.select Path[11] Proof[12] gate_43 gate_45 ∧
+    ∃gate_46, Gates.select Path[11] gate_43 Proof[12] gate_46 ∧
+    Poseidon2 gate_45 gate_46 fun gate_47 =>
+    Gates.is_bool Path[12] ∧
+    ∃gate_49, Gates.select Path[12] Proof[13] gate_47 gate_49 ∧
+    ∃gate_50, Gates.select Path[12] gate_47 Proof[13] gate_50 ∧
+    Poseidon2 gate_49 gate_50 fun gate_51 =>
+    Gates.is_bool Path[13] ∧
+    ∃gate_53, Gates.select Path[13] Proof[14] gate_51 gate_53 ∧
+    ∃gate_54, Gates.select Path[13] gate_51 Proof[14] gate_54 ∧
+    Poseidon2 gate_53 gate_54 fun gate_55 =>
+    Gates.is_bool Path[14] ∧
+    ∃gate_57, Gates.select Path[14] Proof[15] gate_55 gate_57 ∧
+    ∃gate_58, Gates.select Path[14] gate_55 Proof[15] gate_58 ∧
+    Poseidon2 gate_57 gate_58 fun gate_59 =>
+    Gates.is_bool Path[15] ∧
+    ∃gate_61, Gates.select Path[15] Proof[16] gate_59 gate_61 ∧
+    ∃gate_62, Gates.select Path[15] gate_59 Proof[16] gate_62 ∧
+    Poseidon2 gate_61 gate_62 fun gate_63 =>
+    Gates.is_bool Path[16] ∧
+    ∃gate_65, Gates.select Path[16] Proof[17] gate_63 gate_65 ∧
+    ∃gate_66, Gates.select Path[16] gate_63 Proof[17] gate_66 ∧
+    Poseidon2 gate_65 gate_66 fun gate_67 =>
+    Gates.is_bool Path[17] ∧
+    ∃gate_69, Gates.select Path[17] Proof[18] gate_67 gate_69 ∧
+    ∃gate_70, Gates.select Path[17] gate_67 Proof[18] gate_70 ∧
+    Poseidon2 gate_69 gate_70 fun gate_71 =>
+    Gates.is_bool Path[18] ∧
+    ∃gate_73, Gates.select Path[18] Proof[19] gate_71 gate_73 ∧
+    ∃gate_74, Gates.select Path[18] gate_71 Proof[19] gate_74 ∧
+    Poseidon2 gate_73 gate_74 fun gate_75 =>
+    Gates.is_bool Path[19] ∧
+    ∃gate_77, Gates.select Path[19] Proof[20] gate_75 gate_77 ∧
+    ∃gate_78, Gates.select Path[19] gate_75 Proof[20] gate_78 ∧
+    Poseidon2 gate_77 gate_78 fun gate_79 =>
+    Gates.is_bool Path[20] ∧
+    ∃gate_81, Gates.select Path[20] Proof[21] gate_79 gate_81 ∧
+    ∃gate_82, Gates.select Path[20] gate_79 Proof[21] gate_82 ∧
+    Poseidon2 gate_81 gate_82 fun gate_83 =>
+    Gates.is_bool Path[21] ∧
+    ∃gate_85, Gates.select Path[21] Proof[22] gate_83 gate_85 ∧
+    ∃gate_86, Gates.select Path[21] gate_83 Proof[22] gate_86 ∧
+    Poseidon2 gate_85 gate_86 fun gate_87 =>
+    Gates.is_bool Path[22] ∧
+    ∃gate_89, Gates.select Path[22] Proof[23] gate_87 gate_89 ∧
+    ∃gate_90, Gates.select Path[22] gate_87 Proof[23] gate_90 ∧
+    Poseidon2 gate_89 gate_90 fun gate_91 =>
+    Gates.is_bool Path[23] ∧
+    ∃gate_93, Gates.select Path[23] Proof[24] gate_91 gate_93 ∧
+    ∃gate_94, Gates.select Path[23] gate_91 Proof[24] gate_94 ∧
+    Poseidon2 gate_93 gate_94 fun gate_95 =>
+    Gates.is_bool Path[24] ∧
+    ∃gate_97, Gates.select Path[24] Proof[25] gate_95 gate_97 ∧
+    ∃gate_98, Gates.select Path[24] gate_95 Proof[25] gate_98 ∧
+    Poseidon2 gate_97 gate_98 fun gate_99 =>
+    Gates.is_bool Path[25] ∧
+    ∃gate_101, Gates.select Path[25] Proof[26] gate_99 gate_101 ∧
+    ∃gate_102, Gates.select Path[25] gate_99 Proof[26] gate_102 ∧
+    Poseidon2 gate_101 gate_102 fun gate_103 =>
+    Gates.is_bool Path[26] ∧
+    ∃gate_105, Gates.select Path[26] Proof[27] gate_103 gate_105 ∧
+    ∃gate_106, Gates.select Path[26] gate_103 Proof[27] gate_106 ∧
+    Poseidon2 gate_105 gate_106 fun gate_107 =>
+    Gates.is_bool Path[27] ∧
+    ∃gate_109, Gates.select Path[27] Proof[28] gate_107 gate_109 ∧
+    ∃gate_110, Gates.select Path[27] gate_107 Proof[28] gate_110 ∧
+    Poseidon2 gate_109 gate_110 fun gate_111 =>
+    Gates.is_bool Path[28] ∧
+    ∃gate_113, Gates.select Path[28] Proof[29] gate_111 gate_113 ∧
+    ∃gate_114, Gates.select Path[28] gate_111 Proof[29] gate_114 ∧
+    Poseidon2 gate_113 gate_114 fun gate_115 =>
+    k gate_115
+
+end VerifyProof
\ No newline at end of file
diff --git a/main.go b/main.go
index e6c5e3f..f91462a 100644
--- a/main.go
+++ b/main.go
@@ -239,11 +239,13 @@ func main() {
 				Name: "extract-circuit",
 				Flags: []cli.Flag{
 					&cli.StringFlag{Name: "output", Usage: "Output file", Required: true},
+					&cli.StringFlag{Name: "proof-size", Usage: "Length of Proof vector", Required: true},
 				},
 				Action: func(context *cli.Context) error {
 					path := context.String("output")
+					proofSize := uint32(context.Uint("proof-size"))
 					logging.Logger().Info().Msg("Extracting gnark circuit to Lean")
-					circuit_string, err := prover.ExtractLean()
+					circuit_string, err := prover.ExtractLean(proofSize)
 					if err != nil {
 						return err
 					}
diff --git a/prover/circuit.go b/prover/circuit.go
index ec27393..00a4cef 100644
--- a/prover/circuit.go
+++ b/prover/circuit.go
@@ -37,16 +37,16 @@ func (e *bitPatternLengthError) Error() string {
 }
 
 type VerifyProof struct {
-	ProofSet []frontend.Variable
-	Helper   []frontend.Variable
+	Proof []frontend.Variable
+	Path  []frontend.Variable
 }
 
 func (gadget VerifyProof) DefineGadget(api abstractor.API) []frontend.Variable {
-	sum := gadget.ProofSet[0]
-	for i := 1; i < len(gadget.ProofSet); i++ {
-		api.AssertIsBoolean(gadget.Helper[i-1])
-		d1 := api.Select(gadget.Helper[i-1], gadget.ProofSet[i], sum)
-		d2 := api.Select(gadget.Helper[i-1], sum, gadget.ProofSet[i])
+	sum := gadget.Proof[0]
+	for i := 1; i < len(gadget.Proof); i++ {
+		api.AssertIsBoolean(gadget.Path[i-1])
+		d1 := api.Select(gadget.Path[i-1], gadget.Proof[i], sum)
+		d2 := api.Select(gadget.Path[i-1], sum, gadget.Proof[i])
 		sum = api.Call(poseidon.Poseidon2{In1: d1, In2: d2})[0]
 	}
 	return []frontend.Variable{sum}
@@ -167,12 +167,12 @@ func (circuit *MbuCircuit) Define(api frontend.API) error {
 
 		// Verify proof for empty leaf.
 		proof := append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...)
-		root = abstractor.CallGadget(api, VerifyProof{ProofSet: proof, Helper: currentPath})[0]
+		root = abstractor.CallGadget(api, VerifyProof{Proof: proof, Path: currentPath})[0]
 		api.AssertIsEqual(root, prevRoot)
 
 		// Verify proof for idComm.
 		proof = append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...)
-		root = abstractor.CallGadget(api, VerifyProof{ProofSet: proof, Helper: currentPath})[0]
+		root = abstractor.CallGadget(api, VerifyProof{Proof: proof, Path: currentPath})[0]
 
 		// Set root for next iteration.
 		prevRoot = root
diff --git a/prover/proving_system.go b/prover/proving_system.go
index 76fdd2e..24b2bdc 100644
--- a/prover/proving_system.go
+++ b/prover/proving_system.go
@@ -7,7 +7,6 @@ import (
 	"io"
 	"math/big"
 	"worldcoin/gnark-mbu/logging"
-	"worldcoin/gnark-mbu/prover/poseidon"
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/backend/groth16"
@@ -115,8 +114,8 @@ func Setup(treeDepth uint32, batchSize uint32) (*ProvingSystem, error) {
 	return &ProvingSystem{treeDepth, batchSize, pk, vk, ccs}, nil
 }
 
-func ExtractLean() (string, error) {
-	assignment := poseidon.Poseidon2{}
+func ExtractLean(proofSize uint32) (string, error) {
+	assignment := VerifyProof{Proof: make([]frontend.Variable, proofSize), Path: make([]frontend.Variable, proofSize)}
 	return extractor.GadgetToLean(&assignment, ecc.BN254)
 }
 

From 5036caa456b0979acadb9b9ba0e973c6506a9a5a Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Fri, 1 Sep 2023 22:05:12 +0100
Subject: [PATCH 04/12] Added VerifyRound

---
 formal-verification/FormalVerification.lean | 154 +++++---------------
 prover/circuit.go                           |  19 ++-
 2 files changed, 52 insertions(+), 121 deletions(-)

diff --git a/formal-verification/FormalVerification.lean b/formal-verification/FormalVerification.lean
index fb74125..b213aea 100644
--- a/formal-verification/FormalVerification.lean
+++ b/formal-verification/FormalVerification.lean
@@ -124,123 +124,43 @@ def Poseidon2 (In1: F) (In2: F) (k: F -> Prop): Prop :=
     poseidon_3 vec![0, In1, In2] fun gate_0 =>
     k gate_0[0]
 
-def VerifyProof_30_30 (Proof: Vector F 30) (Path: Vector F 30) (k: F -> Prop): Prop :=
-    Gates.is_bool Path[0] ∧
-    ∃gate_1, Gates.select Path[0] Proof[1] Proof[0] gate_1 ∧
-    ∃gate_2, Gates.select Path[0] Proof[0] Proof[1] gate_2 ∧
+def ProofRound (Direction: F) (Hash: F) (Sibling: F) (k: F -> Prop): Prop :=
+    Gates.is_bool Direction ∧
+    ∃gate_1, Gates.select Direction Hash Sibling gate_1 ∧
+    ∃gate_2, Gates.select Direction Sibling Hash gate_2 ∧
     Poseidon2 gate_1 gate_2 fun gate_3 =>
-    Gates.is_bool Path[1] ∧
-    ∃gate_5, Gates.select Path[1] Proof[2] gate_3 gate_5 ∧
-    ∃gate_6, Gates.select Path[1] gate_3 Proof[2] gate_6 ∧
-    Poseidon2 gate_5 gate_6 fun gate_7 =>
-    Gates.is_bool Path[2] ∧
-    ∃gate_9, Gates.select Path[2] Proof[3] gate_7 gate_9 ∧
-    ∃gate_10, Gates.select Path[2] gate_7 Proof[3] gate_10 ∧
-    Poseidon2 gate_9 gate_10 fun gate_11 =>
-    Gates.is_bool Path[3] ∧
-    ∃gate_13, Gates.select Path[3] Proof[4] gate_11 gate_13 ∧
-    ∃gate_14, Gates.select Path[3] gate_11 Proof[4] gate_14 ∧
-    Poseidon2 gate_13 gate_14 fun gate_15 =>
-    Gates.is_bool Path[4] ∧
-    ∃gate_17, Gates.select Path[4] Proof[5] gate_15 gate_17 ∧
-    ∃gate_18, Gates.select Path[4] gate_15 Proof[5] gate_18 ∧
-    Poseidon2 gate_17 gate_18 fun gate_19 =>
-    Gates.is_bool Path[5] ∧
-    ∃gate_21, Gates.select Path[5] Proof[6] gate_19 gate_21 ∧
-    ∃gate_22, Gates.select Path[5] gate_19 Proof[6] gate_22 ∧
-    Poseidon2 gate_21 gate_22 fun gate_23 =>
-    Gates.is_bool Path[6] ∧
-    ∃gate_25, Gates.select Path[6] Proof[7] gate_23 gate_25 ∧
-    ∃gate_26, Gates.select Path[6] gate_23 Proof[7] gate_26 ∧
-    Poseidon2 gate_25 gate_26 fun gate_27 =>
-    Gates.is_bool Path[7] ∧
-    ∃gate_29, Gates.select Path[7] Proof[8] gate_27 gate_29 ∧
-    ∃gate_30, Gates.select Path[7] gate_27 Proof[8] gate_30 ∧
-    Poseidon2 gate_29 gate_30 fun gate_31 =>
-    Gates.is_bool Path[8] ∧
-    ∃gate_33, Gates.select Path[8] Proof[9] gate_31 gate_33 ∧
-    ∃gate_34, Gates.select Path[8] gate_31 Proof[9] gate_34 ∧
-    Poseidon2 gate_33 gate_34 fun gate_35 =>
-    Gates.is_bool Path[9] ∧
-    ∃gate_37, Gates.select Path[9] Proof[10] gate_35 gate_37 ∧
-    ∃gate_38, Gates.select Path[9] gate_35 Proof[10] gate_38 ∧
-    Poseidon2 gate_37 gate_38 fun gate_39 =>
-    Gates.is_bool Path[10] ∧
-    ∃gate_41, Gates.select Path[10] Proof[11] gate_39 gate_41 ∧
-    ∃gate_42, Gates.select Path[10] gate_39 Proof[11] gate_42 ∧
-    Poseidon2 gate_41 gate_42 fun gate_43 =>
-    Gates.is_bool Path[11] ∧
-    ∃gate_45, Gates.select Path[11] Proof[12] gate_43 gate_45 ∧
-    ∃gate_46, Gates.select Path[11] gate_43 Proof[12] gate_46 ∧
-    Poseidon2 gate_45 gate_46 fun gate_47 =>
-    Gates.is_bool Path[12] ∧
-    ∃gate_49, Gates.select Path[12] Proof[13] gate_47 gate_49 ∧
-    ∃gate_50, Gates.select Path[12] gate_47 Proof[13] gate_50 ∧
-    Poseidon2 gate_49 gate_50 fun gate_51 =>
-    Gates.is_bool Path[13] ∧
-    ∃gate_53, Gates.select Path[13] Proof[14] gate_51 gate_53 ∧
-    ∃gate_54, Gates.select Path[13] gate_51 Proof[14] gate_54 ∧
-    Poseidon2 gate_53 gate_54 fun gate_55 =>
-    Gates.is_bool Path[14] ∧
-    ∃gate_57, Gates.select Path[14] Proof[15] gate_55 gate_57 ∧
-    ∃gate_58, Gates.select Path[14] gate_55 Proof[15] gate_58 ∧
-    Poseidon2 gate_57 gate_58 fun gate_59 =>
-    Gates.is_bool Path[15] ∧
-    ∃gate_61, Gates.select Path[15] Proof[16] gate_59 gate_61 ∧
-    ∃gate_62, Gates.select Path[15] gate_59 Proof[16] gate_62 ∧
-    Poseidon2 gate_61 gate_62 fun gate_63 =>
-    Gates.is_bool Path[16] ∧
-    ∃gate_65, Gates.select Path[16] Proof[17] gate_63 gate_65 ∧
-    ∃gate_66, Gates.select Path[16] gate_63 Proof[17] gate_66 ∧
-    Poseidon2 gate_65 gate_66 fun gate_67 =>
-    Gates.is_bool Path[17] ∧
-    ∃gate_69, Gates.select Path[17] Proof[18] gate_67 gate_69 ∧
-    ∃gate_70, Gates.select Path[17] gate_67 Proof[18] gate_70 ∧
-    Poseidon2 gate_69 gate_70 fun gate_71 =>
-    Gates.is_bool Path[18] ∧
-    ∃gate_73, Gates.select Path[18] Proof[19] gate_71 gate_73 ∧
-    ∃gate_74, Gates.select Path[18] gate_71 Proof[19] gate_74 ∧
-    Poseidon2 gate_73 gate_74 fun gate_75 =>
-    Gates.is_bool Path[19] ∧
-    ∃gate_77, Gates.select Path[19] Proof[20] gate_75 gate_77 ∧
-    ∃gate_78, Gates.select Path[19] gate_75 Proof[20] gate_78 ∧
-    Poseidon2 gate_77 gate_78 fun gate_79 =>
-    Gates.is_bool Path[20] ∧
-    ∃gate_81, Gates.select Path[20] Proof[21] gate_79 gate_81 ∧
-    ∃gate_82, Gates.select Path[20] gate_79 Proof[21] gate_82 ∧
-    Poseidon2 gate_81 gate_82 fun gate_83 =>
-    Gates.is_bool Path[21] ∧
-    ∃gate_85, Gates.select Path[21] Proof[22] gate_83 gate_85 ∧
-    ∃gate_86, Gates.select Path[21] gate_83 Proof[22] gate_86 ∧
-    Poseidon2 gate_85 gate_86 fun gate_87 =>
-    Gates.is_bool Path[22] ∧
-    ∃gate_89, Gates.select Path[22] Proof[23] gate_87 gate_89 ∧
-    ∃gate_90, Gates.select Path[22] gate_87 Proof[23] gate_90 ∧
-    Poseidon2 gate_89 gate_90 fun gate_91 =>
-    Gates.is_bool Path[23] ∧
-    ∃gate_93, Gates.select Path[23] Proof[24] gate_91 gate_93 ∧
-    ∃gate_94, Gates.select Path[23] gate_91 Proof[24] gate_94 ∧
-    Poseidon2 gate_93 gate_94 fun gate_95 =>
-    Gates.is_bool Path[24] ∧
-    ∃gate_97, Gates.select Path[24] Proof[25] gate_95 gate_97 ∧
-    ∃gate_98, Gates.select Path[24] gate_95 Proof[25] gate_98 ∧
-    Poseidon2 gate_97 gate_98 fun gate_99 =>
-    Gates.is_bool Path[25] ∧
-    ∃gate_101, Gates.select Path[25] Proof[26] gate_99 gate_101 ∧
-    ∃gate_102, Gates.select Path[25] gate_99 Proof[26] gate_102 ∧
-    Poseidon2 gate_101 gate_102 fun gate_103 =>
-    Gates.is_bool Path[26] ∧
-    ∃gate_105, Gates.select Path[26] Proof[27] gate_103 gate_105 ∧
-    ∃gate_106, Gates.select Path[26] gate_103 Proof[27] gate_106 ∧
-    Poseidon2 gate_105 gate_106 fun gate_107 =>
-    Gates.is_bool Path[27] ∧
-    ∃gate_109, Gates.select Path[27] Proof[28] gate_107 gate_109 ∧
-    ∃gate_110, Gates.select Path[27] gate_107 Proof[28] gate_110 ∧
-    Poseidon2 gate_109 gate_110 fun gate_111 =>
-    Gates.is_bool Path[28] ∧
-    ∃gate_113, Gates.select Path[28] Proof[29] gate_111 gate_113 ∧
-    ∃gate_114, Gates.select Path[28] gate_111 Proof[29] gate_114 ∧
-    Poseidon2 gate_113 gate_114 fun gate_115 =>
-    k gate_115
+    k gate_3
+
+def VerifyProof_30_30 (Proof: Vector F 30) (Path: Vector F 30) (k: F -> Prop): Prop :=
+    ProofRound Path[0] Proof[1] Proof[0] fun gate_0 =>
+    ProofRound Path[1] Proof[2] gate_0 fun gate_1 =>
+    ProofRound Path[2] Proof[3] gate_1 fun gate_2 =>
+    ProofRound Path[3] Proof[4] gate_2 fun gate_3 =>
+    ProofRound Path[4] Proof[5] gate_3 fun gate_4 =>
+    ProofRound Path[5] Proof[6] gate_4 fun gate_5 =>
+    ProofRound Path[6] Proof[7] gate_5 fun gate_6 =>
+    ProofRound Path[7] Proof[8] gate_6 fun gate_7 =>
+    ProofRound Path[8] Proof[9] gate_7 fun gate_8 =>
+    ProofRound Path[9] Proof[10] gate_8 fun gate_9 =>
+    ProofRound Path[10] Proof[11] gate_9 fun gate_10 =>
+    ProofRound Path[11] Proof[12] gate_10 fun gate_11 =>
+    ProofRound Path[12] Proof[13] gate_11 fun gate_12 =>
+    ProofRound Path[13] Proof[14] gate_12 fun gate_13 =>
+    ProofRound Path[14] Proof[15] gate_13 fun gate_14 =>
+    ProofRound Path[15] Proof[16] gate_14 fun gate_15 =>
+    ProofRound Path[16] Proof[17] gate_15 fun gate_16 =>
+    ProofRound Path[17] Proof[18] gate_16 fun gate_17 =>
+    ProofRound Path[18] Proof[19] gate_17 fun gate_18 =>
+    ProofRound Path[19] Proof[20] gate_18 fun gate_19 =>
+    ProofRound Path[20] Proof[21] gate_19 fun gate_20 =>
+    ProofRound Path[21] Proof[22] gate_20 fun gate_21 =>
+    ProofRound Path[22] Proof[23] gate_21 fun gate_22 =>
+    ProofRound Path[23] Proof[24] gate_22 fun gate_23 =>
+    ProofRound Path[24] Proof[25] gate_23 fun gate_24 =>
+    ProofRound Path[25] Proof[26] gate_24 fun gate_25 =>
+    ProofRound Path[26] Proof[27] gate_25 fun gate_26 =>
+    ProofRound Path[27] Proof[28] gate_26 fun gate_27 =>
+    ProofRound Path[28] Proof[29] gate_27 fun gate_28 =>
+    k gate_28
 
 end VerifyProof
\ No newline at end of file
diff --git a/prover/circuit.go b/prover/circuit.go
index 00a4cef..a6f7d75 100644
--- a/prover/circuit.go
+++ b/prover/circuit.go
@@ -36,6 +36,20 @@ func (e *bitPatternLengthError) Error() string {
 	return "Bit pattern length was " + strconv.Itoa(e.actualLength) + " not a total number of bytes"
 }
 
+type ProofRound struct {
+	Direction frontend.Variable
+	Hash      frontend.Variable
+	Sibling   frontend.Variable
+}
+
+func (gadget ProofRound) DefineGadget(api abstractor.API) []frontend.Variable {
+	api.AssertIsBoolean(gadget.Direction)
+	d1 := api.Select(gadget.Direction, gadget.Hash, gadget.Sibling)
+	d2 := api.Select(gadget.Direction, gadget.Sibling, gadget.Hash)
+	sum := api.Call(poseidon.Poseidon2{In1: d1, In2: d2})[0]
+	return []frontend.Variable{sum}
+}
+
 type VerifyProof struct {
 	Proof []frontend.Variable
 	Path  []frontend.Variable
@@ -44,10 +58,7 @@ type VerifyProof struct {
 func (gadget VerifyProof) DefineGadget(api abstractor.API) []frontend.Variable {
 	sum := gadget.Proof[0]
 	for i := 1; i < len(gadget.Proof); i++ {
-		api.AssertIsBoolean(gadget.Path[i-1])
-		d1 := api.Select(gadget.Path[i-1], gadget.Proof[i], sum)
-		d2 := api.Select(gadget.Path[i-1], sum, gadget.Proof[i])
-		sum = api.Call(poseidon.Poseidon2{In1: d1, In2: d2})[0]
+		sum = api.Call(ProofRound{Direction: gadget.Path[i-1], Hash: gadget.Proof[i], Sibling: sum})[0]
 	}
 	return []frontend.Variable{sum}
 }

From 3497407e1ef9531cf509fe1ea06da13a3e9a1479 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Fri, 1 Sep 2023 22:08:04 +0100
Subject: [PATCH 05/12] Fixed Lean namespace

---
 .../Poseidon/Correctness.lean                 | 34 +++++++++----------
 .../SemanticEquivalence.lean                  |  6 ++--
 2 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/formal-verification/FormalVerification/Poseidon/Correctness.lean b/formal-verification/FormalVerification/Poseidon/Correctness.lean
index f8f5687..a3b431b 100644
--- a/formal-verification/FormalVerification/Poseidon/Correctness.lean
+++ b/formal-verification/FormalVerification/Poseidon/Correctness.lean
@@ -5,7 +5,7 @@ import Mathlib
 import ProvenZk
 
 open Matrix
-open Poseidon2 (F Order)
+open VerifyProof (F Order)
 
 variable [Fact (Nat.Prime Order)]
 
@@ -64,16 +64,16 @@ def half_rounds_cps
     half_round state (Vector.ofFn fun i => cfg.round_constants[init_const + i]!) fun state' =>
         half_rounds_cps cfg half_round state' (init_const + cfg.t) round_count k
 
-lemma sbox_uncps (A : F) (k : F -> Prop): Poseidon2.sbox A k = k (A ^ 5) := by
-  unfold Poseidon2.sbox
+lemma sbox_uncps (A : F) (k : F -> Prop): VerifyProof.sbox A k = k (A ^ 5) := by
+  unfold VerifyProof.sbox
   simp [Gates.mul]
   apply iff_to_eq
   repeat (rw [pow_succ])
   rw [pow_zero, mul_one, mul_assoc]
 
 lemma mds_3_uncps (S : Vector F 3) (k : Vector F 3 -> Prop):
-  Poseidon2.mds_3 S k = k (mds_matmul Constants.x5_254_3 S) := by
-  simp [Poseidon2.mds_3, Gates.add, Gates.mul]
+  VerifyProof.mds_3 S k = k (mds_matmul Constants.x5_254_3 S) := by
+  simp [VerifyProof.mds_3, Gates.add, Gates.mul]
   apply iff_to_eq
   simp [mds_matmul, Constants.x5_254_3, Constants.x5_254_3_MDS_matrix]
   simp [Vector.to_column, Matrix.to_vector, Vector.ofFn]
@@ -89,8 +89,8 @@ lemma mds_3_uncps (S : Vector F 3) (k : Vector F 3 -> Prop):
   rfl
 
 lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
-  Poseidon2.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by
-  unfold Poseidon2.fullRound_3_3
+  VerifyProof.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by
+  unfold VerifyProof.fullRound_3_3
   unfold Gates.add
   simp [Gates.add, sbox_uncps, mds_3_uncps, full_round]
   apply iff_to_eq
@@ -102,8 +102,8 @@ lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
   conv => rhs ; rw [←Vector.ofFn_get S]
 
 lemma half_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
-  Poseidon2.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by
-  unfold Poseidon2.halfRound_3_3
+  VerifyProof.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by
+  unfold VerifyProof.halfRound_3_3
   unfold Gates.add
   simp [Gates.add, sbox_uncps, mds_3_uncps, partial_round]
   apply iff_to_eq
@@ -151,7 +151,7 @@ lemma partial_rounds_3_uncps
   {S : Vector F 3}
   {start count : Nat}
   {k : Vector F 3 -> Prop}:
-  half_rounds_cps Constants.x5_254_3 Poseidon2.halfRound_3_3 S start count k = k (partial_rounds Constants.x5_254_3 S start count) := by
+  half_rounds_cps Constants.x5_254_3 VerifyProof.halfRound_3_3 S start count k = k (partial_rounds Constants.x5_254_3 S start count) := by
   apply partial_rounds_uncps
   apply half_round_3_uncps
 
@@ -192,7 +192,7 @@ lemma full_rounds_3_uncps
   {S : Vector F 3}
   {start count : Nat}
   {k : Vector F 3 -> Prop}:
-  full_rounds_cps Constants.x5_254_3 Poseidon2.fullRound_3_3 S start count k = k (full_rounds Constants.x5_254_3 S start count) := by
+  full_rounds_cps Constants.x5_254_3 VerifyProof.fullRound_3_3 S start count k = k (full_rounds Constants.x5_254_3 S start count) := by
   apply full_rounds_uncps
   apply full_round_3_uncps
 
@@ -200,9 +200,9 @@ lemma fold_vec_2 {v : Vector F 2}: vec![v[0], v[1]] = v := by
     conv => rhs; rw [←Vector.ofFn_get v]
 
 def looped_poseidon_3 (inp : Vector F 3) (k: Vector F 3 -> Prop): Prop :=
-    full_rounds_cps Constants.x5_254_3 Poseidon2.fullRound_3_3 inp 0 4 fun state =>
-    half_rounds_cps Constants.x5_254_3 Poseidon2.halfRound_3_3 state 12 57  fun state' =>
-    full_rounds_cps Constants.x5_254_3 Poseidon2.fullRound_3_3 state' 183 4 k
+    full_rounds_cps Constants.x5_254_3 VerifyProof.fullRound_3_3 inp 0 4 fun state =>
+    half_rounds_cps Constants.x5_254_3 VerifyProof.halfRound_3_3 state 12 57  fun state' =>
+    full_rounds_cps Constants.x5_254_3 VerifyProof.fullRound_3_3 state' 183 4 k
 
 lemma fold_vec_3 {v : Vector F 3}: vec![v[0], v[1], v[2]] = v := by
     conv => rhs; rw [←Vector.ofFn_get v]
@@ -210,9 +210,9 @@ lemma fold_vec_3 {v : Vector F 3}: vec![v[0], v[1], v[2]] = v := by
 set_option maxRecDepth 2048
 
 theorem looped_poseidon_3_go (inp : Vector F 3) (k : Vector F 3 -> Prop):
-    Poseidon2.poseidon_3 inp k = looped_poseidon_3 inp k := by
+    VerifyProof.poseidon_3 inp k = looped_poseidon_3 inp k := by
     unfold looped_poseidon_3
-    unfold Poseidon2.poseidon_3
+    unfold VerifyProof.poseidon_3
     simp [full_rounds_cps, half_rounds_cps, getElem!, fold_vec_3, Vector.ofFn]
     rfl
 
@@ -295,7 +295,7 @@ theorem perm_folded_go (cfg : Constants) (input_words : Vector cfg.F cfg.t):
   }
 
 theorem poseidon_3_correct (inp : Vector F 3) (k : Vector F 3 -> Prop):
-  Poseidon2.poseidon_3 inp k = k (Poseidon.perm Constants.x5_254_3 inp) := by
+  VerifyProof.poseidon_3 inp k = k (Poseidon.perm Constants.x5_254_3 inp) := by
   simp [
     looped_poseidon_3_go,
     looped_poseidon_3,
diff --git a/formal-verification/FormalVerification/SemanticEquivalence.lean b/formal-verification/FormalVerification/SemanticEquivalence.lean
index 15e0743..2a31eab 100644
--- a/formal-verification/FormalVerification/SemanticEquivalence.lean
+++ b/formal-verification/FormalVerification/SemanticEquivalence.lean
@@ -6,12 +6,12 @@ import FormalVerification
 import FormalVerification.Poseidon.Spec
 import FormalVerification.Poseidon.Correctness
 
-open Poseidon2 (F Order)
+open VerifyProof (F Order)
 
 variable [Fact (Nat.Prime Order)]
 
 def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0, a.get 0, a.get 1]).get 0
 
-lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : Poseidon2.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
-    simp [Poseidon2.Poseidon2, poseidon₂, poseidon_3_correct, getElem]
+lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : VerifyProof.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
+    simp [VerifyProof.Poseidon2, poseidon₂, poseidon_3_correct, getElem]
     rfl
\ No newline at end of file

From b144a6a60b4237c10212ee569427cd196dd68f29 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Fri, 1 Sep 2023 22:40:23 +0100
Subject: [PATCH 06/12] Equivalence of ProofRound

---
 .../FormalVerification/SemanticEquivalence.lean   | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/formal-verification/FormalVerification/SemanticEquivalence.lean b/formal-verification/FormalVerification/SemanticEquivalence.lean
index 2a31eab..11cda7e 100644
--- a/formal-verification/FormalVerification/SemanticEquivalence.lean
+++ b/formal-verification/FormalVerification/SemanticEquivalence.lean
@@ -14,4 +14,17 @@ def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0,
 
 lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : VerifyProof.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
     simp [VerifyProof.Poseidon2, poseidon₂, poseidon_3_correct, getElem]
-    rfl
\ No newline at end of file
+    rfl
+
+lemma ProofRound_uncps {direction: F} {hash: F} {sibling: F} {k: F -> Prop} : 
+    VerifyProof.ProofRound direction hash sibling k ↔
+    is_bit direction ∧ k (match Dir.nat_to_dir direction.val with
+    | Dir.left => poseidon₂ vec![sibling, hash]
+    | Dir.right => poseidon₂ vec![hash, sibling]) := by
+    simp [VerifyProof.ProofRound, Gates.is_bool, Gates.select, Gates.is_bool]
+    intro hb
+    cases hb <;> {
+        simp [*]
+        simp [Dir.nat_to_dir, ZMod.val, Order]
+        rw [Poseidon2_uncps]
+    }
\ No newline at end of file

From bcf008cf39764e53f5e006ae311e6ed31cfd57c1 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Sat, 2 Sep 2023 19:55:32 +0100
Subject: [PATCH 07/12] Added verification of VerifyProof

---
 .github/workflows/test.yml                    |  1 +
 formal-verification/FormalVerification.lean   |  5 ++-
 .../SemanticEquivalence.lean                  | 41 ++++++++++++++++++-
 main.go                                       |  2 +-
 prover/circuit.go                             |  2 +
 prover/proving_system.go                      |  3 +-
 6 files changed, 49 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 70275f2..47c3d49 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -1,5 +1,6 @@
 name: Test
 on: push
+concurrency: testing_environment
 jobs:
   build-and-test:
     runs-on: ubuntu-latest
diff --git a/formal-verification/FormalVerification.lean b/formal-verification/FormalVerification.lean
index b213aea..92b8c99 100644
--- a/formal-verification/FormalVerification.lean
+++ b/formal-verification/FormalVerification.lean
@@ -131,7 +131,7 @@ def ProofRound (Direction: F) (Hash: F) (Sibling: F) (k: F -> Prop): Prop :=
     Poseidon2 gate_1 gate_2 fun gate_3 =>
     k gate_3
 
-def VerifyProof_30_30 (Proof: Vector F 30) (Path: Vector F 30) (k: F -> Prop): Prop :=
+def VerifyProof_31_30 (Proof: Vector F 31) (Path: Vector F 30) (k: F -> Prop): Prop :=
     ProofRound Path[0] Proof[1] Proof[0] fun gate_0 =>
     ProofRound Path[1] Proof[2] gate_0 fun gate_1 =>
     ProofRound Path[2] Proof[3] gate_1 fun gate_2 =>
@@ -161,6 +161,7 @@ def VerifyProof_30_30 (Proof: Vector F 30) (Path: Vector F 30) (k: F -> Prop): P
     ProofRound Path[26] Proof[27] gate_25 fun gate_26 =>
     ProofRound Path[27] Proof[28] gate_26 fun gate_27 =>
     ProofRound Path[28] Proof[29] gate_27 fun gate_28 =>
-    k gate_28
+    ProofRound Path[29] Proof[30] gate_28 fun gate_29 =>
+    k gate_29
 
 end VerifyProof
\ No newline at end of file
diff --git a/formal-verification/FormalVerification/SemanticEquivalence.lean b/formal-verification/FormalVerification/SemanticEquivalence.lean
index 11cda7e..c840730 100644
--- a/formal-verification/FormalVerification/SemanticEquivalence.lean
+++ b/formal-verification/FormalVerification/SemanticEquivalence.lean
@@ -10,6 +10,8 @@ open VerifyProof (F Order)
 
 variable [Fact (Nat.Prime Order)]
 
+abbrev D := 30
+
 def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0, a.get 0, a.get 1]).get 0
 
 lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : VerifyProof.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
@@ -27,4 +29,41 @@ lemma ProofRound_uncps {direction: F} {hash: F} {sibling: F} {k: F -> Prop} :
         simp [*]
         simp [Dir.nat_to_dir, ZMod.val, Order]
         rw [Poseidon2_uncps]
-    }
\ No newline at end of file
+    }
+
+def proof_rounds (Siblings : Vector F (n+1)) (PathIndices : Vector F n) (k : F -> Prop) : Prop :=
+  match n with
+  | Nat.zero => k Siblings.head
+  | Nat.succ _ => VerifyProof.ProofRound PathIndices.head Siblings.tail.head Siblings.head fun next =>
+    proof_rounds (next ::ᵥ Siblings.tail.tail) PathIndices.tail k
+
+lemma proof_rounds_uncps
+  {Leaf : F}
+  {Siblings : Vector F n}
+  {PathIndices : Vector F n}
+  {k : F -> Prop}:
+  proof_rounds (Leaf ::ᵥ Siblings) PathIndices k ↔
+  is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings Leaf) := by
+  induction PathIndices, Siblings using Vector.inductionOn₂ generalizing Leaf with
+  | nil =>
+    simp [is_vector_binary]
+    rfl
+  | @cons n ix sib ixes sibs ih =>
+    simp [MerkleTree.recover_tail_reverse_equals_recover, MerkleTree.recover_tail, proof_rounds]
+    simp [ProofRound_uncps, is_vector_binary_cons, and_assoc, ih]
+    intros
+    rfl
+
+lemma VerifyProof_looped (PathIndices: Vector F D) (Siblings: Vector F (D+1)) (k: F -> Prop):
+    VerifyProof.VerifyProof_31_30 Siblings PathIndices k =
+      proof_rounds Siblings PathIndices k := by
+    unfold VerifyProof.VerifyProof_31_30
+    simp [proof_rounds]
+    rw [←Vector.ofFn_get (v := PathIndices)]
+    rw [←Vector.ofFn_get (v := Siblings)]
+    rfl
+
+lemma VerifyProof_31_30_uncps {PathIndices: Vector F D} {Siblings: Vector F (D+1)} {k : F -> Prop}:
+    VerifyProof.VerifyProof_31_30 (Siblings.head ::ᵥ Siblings.tail) PathIndices k ↔
+    is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings.tail Siblings.head) := by
+    simp only [VerifyProof_looped, proof_rounds_uncps]
\ No newline at end of file
diff --git a/main.go b/main.go
index f91462a..7849b82 100644
--- a/main.go
+++ b/main.go
@@ -239,7 +239,7 @@ func main() {
 				Name: "extract-circuit",
 				Flags: []cli.Flag{
 					&cli.StringFlag{Name: "output", Usage: "Output file", Required: true},
-					&cli.StringFlag{Name: "proof-size", Usage: "Length of Proof vector", Required: true},
+					&cli.StringFlag{Name: "proof-size", Usage: "Length of Proof vector (i.e. depth of tree)", Required: true},
 				},
 				Action: func(context *cli.Context) error {
 					path := context.String("output")
diff --git a/prover/circuit.go b/prover/circuit.go
index a6f7d75..7dedb57 100644
--- a/prover/circuit.go
+++ b/prover/circuit.go
@@ -176,6 +176,8 @@ func (circuit *MbuCircuit) Define(api frontend.API) error {
 		currentIndex := api.Add(circuit.StartIndex, i)
 		currentPath := api.ToBinary(currentIndex, circuit.Depth)
 
+		// len(circuit.MerkleProofs[i]) === circuit.Depth
+		// len(circuit.IdComms) === circuit.BatchSize
 		// Verify proof for empty leaf.
 		proof := append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...)
 		root = abstractor.CallGadget(api, VerifyProof{Proof: proof, Path: currentPath})[0]
diff --git a/prover/proving_system.go b/prover/proving_system.go
index 24b2bdc..0f294ba 100644
--- a/prover/proving_system.go
+++ b/prover/proving_system.go
@@ -115,7 +115,8 @@ func Setup(treeDepth uint32, batchSize uint32) (*ProvingSystem, error) {
 }
 
 func ExtractLean(proofSize uint32) (string, error) {
-	assignment := VerifyProof{Proof: make([]frontend.Variable, proofSize), Path: make([]frontend.Variable, proofSize)}
+	// Not checking for proofSize === 0
+	assignment := VerifyProof{Proof: make([]frontend.Variable, proofSize+1), Path: make([]frontend.Variable, proofSize)}
 	return extractor.GadgetToLean(&assignment, ecc.BN254)
 }
 

From 4f045fc241136b8ec87f448e76578b5f1f4a704a Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Tue, 5 Sep 2023 15:08:38 +0100
Subject: [PATCH 08/12] Replaced proof-size with tree-depth

---
 .github/workflows/test.yml | 2 +-
 main.go                    | 6 +++---
 prover/proving_system.go   | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 47c3d49..77aa3ba 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -28,7 +28,7 @@ jobs:
     - name: Test
       run: go test
     - name: Export circuit
-      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean --proof-size 30
+      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean --tree-depth 30
     - name: Build lean project
       run: |
         cd formal-verification
diff --git a/main.go b/main.go
index 7849b82..be8b6cb 100644
--- a/main.go
+++ b/main.go
@@ -239,13 +239,13 @@ func main() {
 				Name: "extract-circuit",
 				Flags: []cli.Flag{
 					&cli.StringFlag{Name: "output", Usage: "Output file", Required: true},
-					&cli.StringFlag{Name: "proof-size", Usage: "Length of Proof vector (i.e. depth of tree)", Required: true},
+					&cli.UintFlag{Name: "tree-depth", Usage: "Merkle tree depth", Required: true},
 				},
 				Action: func(context *cli.Context) error {
 					path := context.String("output")
-					proofSize := uint32(context.Uint("proof-size"))
+					treeDepth := uint32(context.Uint("tree-depth"))
 					logging.Logger().Info().Msg("Extracting gnark circuit to Lean")
-					circuit_string, err := prover.ExtractLean(proofSize)
+					circuit_string, err := prover.ExtractLean(treeDepth)
 					if err != nil {
 						return err
 					}
diff --git a/prover/proving_system.go b/prover/proving_system.go
index 0f294ba..0f3f483 100644
--- a/prover/proving_system.go
+++ b/prover/proving_system.go
@@ -114,9 +114,9 @@ func Setup(treeDepth uint32, batchSize uint32) (*ProvingSystem, error) {
 	return &ProvingSystem{treeDepth, batchSize, pk, vk, ccs}, nil
 }
 
-func ExtractLean(proofSize uint32) (string, error) {
-	// Not checking for proofSize === 0
-	assignment := VerifyProof{Proof: make([]frontend.Variable, proofSize+1), Path: make([]frontend.Variable, proofSize)}
+func ExtractLean(treeDepth uint32) (string, error) {
+	// Not checking for treeDepth === 0
+	assignment := VerifyProof{Proof: make([]frontend.Variable, treeDepth+1), Path: make([]frontend.Variable, treeDepth)}
 	return extractor.GadgetToLean(&assignment, ecc.BN254)
 }
 

From f8d579f644a60d6ce7e2efaca94a67d624e6421b Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Tue, 5 Sep 2023 16:09:57 +0100
Subject: [PATCH 09/12] Updated extractor version

---
 go.mod | 2 +-
 go.sum | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/go.mod b/go.mod
index b25a896..49d0ac4 100644
--- a/go.mod
+++ b/go.mod
@@ -25,7 +25,7 @@ require (
 	github.com/prometheus/client_model v0.3.0 // indirect
 	github.com/prometheus/common v0.37.0 // indirect
 	github.com/prometheus/procfs v0.8.0 // indirect
-	github.com/reilabs/gnark-lean-extractor v1.1.0 // indirect
+	github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df // indirect
 	github.com/rogpeppe/go-internal v1.10.0 // indirect
 	github.com/russross/blackfriday/v2 v2.1.0 // indirect
 	github.com/xrash/smetrics v0.0.0-20201216005158-039620a65673 // indirect
diff --git a/go.sum b/go.sum
index 9f8f69c..db19aaf 100644
--- a/go.sum
+++ b/go.sum
@@ -228,6 +228,8 @@ github.com/reilabs/gnark-lean-extractor v1.0.1-0.20230831190435-992a084cf5ea h1:
 github.com/reilabs/gnark-lean-extractor v1.0.1-0.20230831190435-992a084cf5ea/go.mod h1:FuCRQ2kdpdImOzmzFUqMoCMQxn+Nol+AmzPDWlBZLA8=
 github.com/reilabs/gnark-lean-extractor v1.1.0 h1:vxB8Nhzf/TDS4sVM/qvaxJRod+u/mOFdCny/61Z00Bs=
 github.com/reilabs/gnark-lean-extractor v1.1.0/go.mod h1:FuCRQ2kdpdImOzmzFUqMoCMQxn+Nol+AmzPDWlBZLA8=
+github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df h1:aCdrzgCm8Xkxz+I35qE0vDU7AtUP9EZkmEKx4eLCuGU=
+github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df/go.mod h1:FuCRQ2kdpdImOzmzFUqMoCMQxn+Nol+AmzPDWlBZLA8=
 github.com/rogpeppe/go-internal v1.3.0/go.mod h1:M8bDsm7K2OlrFYOpmOWEs/qY81heoFRclV5y23lUDJ4=
 github.com/rogpeppe/go-internal v1.9.0 h1:73kH8U+JUqXU8lRuOHeVHaa/SZPifC7BkcraZVejAe8=
 github.com/rogpeppe/go-internal v1.9.0/go.mod h1:WtVeX8xhTBvf0smdhujwtBcq4Qrzq/fJaraNFVN+nFs=

From 03f99b96b11685a0ad3f4ad6e3935d39f7d95bc3 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Tue, 5 Sep 2023 16:41:44 +0100
Subject: [PATCH 10/12] Updated namespace

---
 formal-verification/FormalVerification.lean   |  4 +--
 .../Poseidon/Correctness.lean                 | 36 +++++++++----------
 .../SemanticEquivalence.lean                  | 18 +++++-----
 prover/insertion_proving_system.go            |  2 +-
 4 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/formal-verification/FormalVerification.lean b/formal-verification/FormalVerification.lean
index 92b8c99..b0e890a 100644
--- a/formal-verification/FormalVerification.lean
+++ b/formal-verification/FormalVerification.lean
@@ -1,7 +1,7 @@
 import ProvenZk.Gates
 import ProvenZk.Ext.Vector
 
-namespace VerifyProof
+namespace SemaphoreMTB
 
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
@@ -164,4 +164,4 @@ def VerifyProof_31_30 (Proof: Vector F 31) (Path: Vector F 30) (k: F -> Prop): P
     ProofRound Path[29] Proof[30] gate_28 fun gate_29 =>
     k gate_29
 
-end VerifyProof
\ No newline at end of file
+end SemaphoreMTB
\ No newline at end of file
diff --git a/formal-verification/FormalVerification/Poseidon/Correctness.lean b/formal-verification/FormalVerification/Poseidon/Correctness.lean
index a3b431b..66d911a 100644
--- a/formal-verification/FormalVerification/Poseidon/Correctness.lean
+++ b/formal-verification/FormalVerification/Poseidon/Correctness.lean
@@ -5,7 +5,7 @@ import Mathlib
 import ProvenZk
 
 open Matrix
-open VerifyProof (F Order)
+open SemaphoreMTB (F Order)
 
 variable [Fact (Nat.Prime Order)]
 
@@ -64,16 +64,16 @@ def half_rounds_cps
     half_round state (Vector.ofFn fun i => cfg.round_constants[init_const + i]!) fun state' =>
         half_rounds_cps cfg half_round state' (init_const + cfg.t) round_count k
 
-lemma sbox_uncps (A : F) (k : F -> Prop): VerifyProof.sbox A k = k (A ^ 5) := by
-  unfold VerifyProof.sbox
+lemma sbox_uncps (A : F) (k : F -> Prop): SemaphoreMTB.sbox A k = k (A ^ 5) := by
+  unfold SemaphoreMTB.sbox
   simp [Gates.mul]
   apply iff_to_eq
   repeat (rw [pow_succ])
   rw [pow_zero, mul_one, mul_assoc]
 
 lemma mds_3_uncps (S : Vector F 3) (k : Vector F 3 -> Prop):
-  VerifyProof.mds_3 S k = k (mds_matmul Constants.x5_254_3 S) := by
-  simp [VerifyProof.mds_3, Gates.add, Gates.mul]
+  SemaphoreMTB.mds_3 S k = k (mds_matmul Constants.x5_254_3 S) := by
+  simp [SemaphoreMTB.mds_3, Gates.add, Gates.mul]
   apply iff_to_eq
   simp [mds_matmul, Constants.x5_254_3, Constants.x5_254_3_MDS_matrix]
   simp [Vector.to_column, Matrix.to_vector, Vector.ofFn]
@@ -89,8 +89,8 @@ lemma mds_3_uncps (S : Vector F 3) (k : Vector F 3 -> Prop):
   rfl
 
 lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
-  VerifyProof.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by
-  unfold VerifyProof.fullRound_3_3
+  SemaphoreMTB.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by
+  unfold SemaphoreMTB.fullRound_3_3
   unfold Gates.add
   simp [Gates.add, sbox_uncps, mds_3_uncps, full_round]
   apply iff_to_eq
@@ -102,8 +102,8 @@ lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
   conv => rhs ; rw [←Vector.ofFn_get S]
 
 lemma half_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
-  VerifyProof.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by
-  unfold VerifyProof.halfRound_3_3
+  SemaphoreMTB.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by
+  unfold SemaphoreMTB.halfRound_3_3
   unfold Gates.add
   simp [Gates.add, sbox_uncps, mds_3_uncps, partial_round]
   apply iff_to_eq
@@ -151,7 +151,7 @@ lemma partial_rounds_3_uncps
   {S : Vector F 3}
   {start count : Nat}
   {k : Vector F 3 -> Prop}:
-  half_rounds_cps Constants.x5_254_3 VerifyProof.halfRound_3_3 S start count k = k (partial_rounds Constants.x5_254_3 S start count) := by
+  half_rounds_cps Constants.x5_254_3 SemaphoreMTB.halfRound_3_3 S start count k = k (partial_rounds Constants.x5_254_3 S start count) := by
   apply partial_rounds_uncps
   apply half_round_3_uncps
 
@@ -192,7 +192,7 @@ lemma full_rounds_3_uncps
   {S : Vector F 3}
   {start count : Nat}
   {k : Vector F 3 -> Prop}:
-  full_rounds_cps Constants.x5_254_3 VerifyProof.fullRound_3_3 S start count k = k (full_rounds Constants.x5_254_3 S start count) := by
+  full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 S start count k = k (full_rounds Constants.x5_254_3 S start count) := by
   apply full_rounds_uncps
   apply full_round_3_uncps
 
@@ -200,9 +200,9 @@ lemma fold_vec_2 {v : Vector F 2}: vec![v[0], v[1]] = v := by
     conv => rhs; rw [←Vector.ofFn_get v]
 
 def looped_poseidon_3 (inp : Vector F 3) (k: Vector F 3 -> Prop): Prop :=
-    full_rounds_cps Constants.x5_254_3 VerifyProof.fullRound_3_3 inp 0 4 fun state =>
-    half_rounds_cps Constants.x5_254_3 VerifyProof.halfRound_3_3 state 12 57  fun state' =>
-    full_rounds_cps Constants.x5_254_3 VerifyProof.fullRound_3_3 state' 183 4 k
+    full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 inp 0 4 fun state =>
+    half_rounds_cps Constants.x5_254_3 SemaphoreMTB.halfRound_3_3 state 12 57  fun state' =>
+    full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 state' 183 4 k
 
 lemma fold_vec_3 {v : Vector F 3}: vec![v[0], v[1], v[2]] = v := by
     conv => rhs; rw [←Vector.ofFn_get v]
@@ -210,9 +210,9 @@ lemma fold_vec_3 {v : Vector F 3}: vec![v[0], v[1], v[2]] = v := by
 set_option maxRecDepth 2048
 
 theorem looped_poseidon_3_go (inp : Vector F 3) (k : Vector F 3 -> Prop):
-    VerifyProof.poseidon_3 inp k = looped_poseidon_3 inp k := by
+    SemaphoreMTB.poseidon_3 inp k = looped_poseidon_3 inp k := by
     unfold looped_poseidon_3
-    unfold VerifyProof.poseidon_3
+    unfold SemaphoreMTB.poseidon_3
     simp [full_rounds_cps, half_rounds_cps, getElem!, fold_vec_3, Vector.ofFn]
     rfl
 
@@ -295,7 +295,7 @@ theorem perm_folded_go (cfg : Constants) (input_words : Vector cfg.F cfg.t):
   }
 
 theorem poseidon_3_correct (inp : Vector F 3) (k : Vector F 3 -> Prop):
-  VerifyProof.poseidon_3 inp k = k (Poseidon.perm Constants.x5_254_3 inp) := by
+  SemaphoreMTB.poseidon_3 inp k = k (Poseidon.perm Constants.x5_254_3 inp) := by
   simp [
     looped_poseidon_3_go,
     looped_poseidon_3,
@@ -305,4 +305,4 @@ theorem poseidon_3_correct (inp : Vector F 3) (k : Vector F 3 -> Prop):
     perm_folded_go,
     perm_folded
   ]
-  rfl
+  rfl
\ No newline at end of file
diff --git a/formal-verification/FormalVerification/SemanticEquivalence.lean b/formal-verification/FormalVerification/SemanticEquivalence.lean
index c840730..cdf88b2 100644
--- a/formal-verification/FormalVerification/SemanticEquivalence.lean
+++ b/formal-verification/FormalVerification/SemanticEquivalence.lean
@@ -6,7 +6,7 @@ import FormalVerification
 import FormalVerification.Poseidon.Spec
 import FormalVerification.Poseidon.Correctness
 
-open VerifyProof (F Order)
+open SemaphoreMTB (F Order)
 
 variable [Fact (Nat.Prime Order)]
 
@@ -14,16 +14,16 @@ abbrev D := 30
 
 def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0, a.get 0, a.get 1]).get 0
 
-lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : VerifyProof.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
-    simp [VerifyProof.Poseidon2, poseidon₂, poseidon_3_correct, getElem]
+lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : SemaphoreMTB.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
+    simp [SemaphoreMTB.Poseidon2, poseidon₂, poseidon_3_correct, getElem]
     rfl
 
 lemma ProofRound_uncps {direction: F} {hash: F} {sibling: F} {k: F -> Prop} : 
-    VerifyProof.ProofRound direction hash sibling k ↔
+    SemaphoreMTB.ProofRound direction hash sibling k ↔
     is_bit direction ∧ k (match Dir.nat_to_dir direction.val with
     | Dir.left => poseidon₂ vec![sibling, hash]
     | Dir.right => poseidon₂ vec![hash, sibling]) := by
-    simp [VerifyProof.ProofRound, Gates.is_bool, Gates.select, Gates.is_bool]
+    simp [SemaphoreMTB.ProofRound, Gates.is_bool, Gates.select, Gates.is_bool]
     intro hb
     cases hb <;> {
         simp [*]
@@ -34,7 +34,7 @@ lemma ProofRound_uncps {direction: F} {hash: F} {sibling: F} {k: F -> Prop} :
 def proof_rounds (Siblings : Vector F (n+1)) (PathIndices : Vector F n) (k : F -> Prop) : Prop :=
   match n with
   | Nat.zero => k Siblings.head
-  | Nat.succ _ => VerifyProof.ProofRound PathIndices.head Siblings.tail.head Siblings.head fun next =>
+  | Nat.succ _ => SemaphoreMTB.ProofRound PathIndices.head Siblings.tail.head Siblings.head fun next =>
     proof_rounds (next ::ᵥ Siblings.tail.tail) PathIndices.tail k
 
 lemma proof_rounds_uncps
@@ -55,15 +55,15 @@ lemma proof_rounds_uncps
     rfl
 
 lemma VerifyProof_looped (PathIndices: Vector F D) (Siblings: Vector F (D+1)) (k: F -> Prop):
-    VerifyProof.VerifyProof_31_30 Siblings PathIndices k =
+    SemaphoreMTB.VerifyProof_31_30 Siblings PathIndices k =
       proof_rounds Siblings PathIndices k := by
-    unfold VerifyProof.VerifyProof_31_30
+    unfold SemaphoreMTB.VerifyProof_31_30
     simp [proof_rounds]
     rw [←Vector.ofFn_get (v := PathIndices)]
     rw [←Vector.ofFn_get (v := Siblings)]
     rfl
 
 lemma VerifyProof_31_30_uncps {PathIndices: Vector F D} {Siblings: Vector F (D+1)} {k : F -> Prop}:
-    VerifyProof.VerifyProof_31_30 (Siblings.head ::ᵥ Siblings.tail) PathIndices k ↔
+    SemaphoreMTB.VerifyProof_31_30 (Siblings.head ::ᵥ Siblings.tail) PathIndices k ↔
     is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings.tail Siblings.head) := by
     simp only [VerifyProof_looped, proof_rounds_uncps]
\ No newline at end of file
diff --git a/prover/insertion_proving_system.go b/prover/insertion_proving_system.go
index 719554d..997a78c 100644
--- a/prover/insertion_proving_system.go
+++ b/prover/insertion_proving_system.go
@@ -97,7 +97,7 @@ func SetupInsertion(treeDepth uint32, batchSize uint32) (*ProvingSystem, error)
 func ExtractLean(treeDepth uint32) (string, error) {
 	// Not checking for treeDepth === 0
 	assignment := VerifyProof{Proof: make([]frontend.Variable, treeDepth+1), Path: make([]frontend.Variable, treeDepth)}
-	return extractor.GadgetToLean(&assignment, ecc.BN254)
+	return extractor.GadgetToLeanWithName(&assignment, ecc.BN254, "SemaphoreMTB")
 }
 
 func (ps *ProvingSystem) ProveInsertion(params *InsertionParameters) (*Proof, error) {

From dd8f278e1a4c52b8ab0ab3995c034cc3956e9fbc Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Tue, 5 Sep 2023 16:44:25 +0100
Subject: [PATCH 11/12] Updated readme

---
 README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index c1f4591..798226b 100644
--- a/README.md
+++ b/README.md
@@ -56,7 +56,8 @@ This part explains the existing cli commands.
         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
+        1. output *file path* - File to be written to
+        2. tree-depth *n* - Merkle tree depth
 
 ## Benchmarks
 

From 4f83b02f5fabee17085894e3ee8a330d86cbe956 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Tue, 5 Sep 2023 16:44:44 +0100
Subject: [PATCH 12/12] Updated readme

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 798226b..2943c5c 100644
--- a/README.md
+++ b/README.md
@@ -51,7 +51,7 @@ This part explains the existing cli commands.
         2. input-hash *hash* - Hash of all public inputs  
 7. r1cs - Builds an r1cs and writes it to a file  
     Flags:  
-        1. output *file path* - File to be writen to  
+        1. output *file path* - File to be written 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