From 47a2d9c275d1f86e5d3aeef8946453df75096aa7 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Thu, 29 Feb 2024 18:38:42 +0000
Subject: [PATCH 1/3] Updated readme

---
 README.md                         | 15 ++++++++++++---
 extractor/test/my_circuit_test.go |  4 ++--
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 84f9ae9..59e6d01 100644
--- a/README.md
+++ b/README.md
@@ -22,6 +22,10 @@ For an overview of how to use this library, see both the [example](#example) and
 contributing, or are new to Go, please see our
 [contributing guidelines](./CONTRIBUTING.md) for more information.
 
+## Compatibility table
+This version of `gnark-lean-extractor` is compatible with `gnark v0.8.x`.
+It is recommended to import [`ProvenZK-v1.3.0`](https://github.com/reilabs/proven-zk/tree/v1.3.0) in Lean4 to process the circuits extracted with this version of `gnark-lean-extractor`.
+
 ## Example
 
 The following is a brief example of how to design a simple gnark circuit in
@@ -45,9 +49,14 @@ func (circuit MyCircuit) Define(api frontend.API) error {
 }
 ```
 
-Once you export this to Lean, you get a definition as follows:
+Once you export `MyCircuit` to Lean, you obtain the following definition:
 
 ```lean
+import ProvenZk.Gates
+import ProvenZk.Ext.Vector
+
+set_option linter.unusedVariables false
+
 namespace MyCircuit
 
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
@@ -87,7 +96,7 @@ aforementioned gnark library, and then call the extractor function
 
 ```go
 circuit := MyCircuit{}
-out, err := CircuitToLean(&circuit, ecc.BN254)
+out, err := extractor.CircuitToLean(&circuit, ecc.BN254)
 if err != nil {
     log.Fatal(err)
 }
@@ -95,7 +104,7 @@ fmt.Println(out)
 ```
 
 `CircuitToLean` returns a string which contains the circuit output in a format
-that can be read by the Lean language. The lean code depends on Reilabs'
+that can be read by the Lean language. The Lean code depends on Reilabs'
 [ProvenZK](https://github.com/reilabs/proven-zk) library in order to represent
 gates and other components of the circuit. In doing so, it makes the extracted
 circuit formally verifiable.
diff --git a/extractor/test/my_circuit_test.go b/extractor/test/my_circuit_test.go
index 577317d..5dbc41f 100644
--- a/extractor/test/my_circuit_test.go
+++ b/extractor/test/my_circuit_test.go
@@ -23,8 +23,8 @@ func (circuit *MyCircuit) Define(api frontend.API) error {
 }
 
 func TestMyCircuit(t *testing.T) {
-	assignment := MyCircuit{}
-	out, err := extractor.CircuitToLean(&assignment, ecc.BN254)
+	circuit := MyCircuit{}
+	out, err := extractor.CircuitToLean(&circuit, ecc.BN254)
 	if err != nil {
 		log.Fatal(err)
 	}

From eb5aa69e0c2e864e7b9205cfbe3c094402c76fc9 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Mar 2024 22:09:49 +0000
Subject: [PATCH 2/3] Added GatesGnark8

---
 README.md                           | 7 ++++---
 extractor/lean_export.go            | 3 ++-
 test/TestAnotherCircuit.lean        | 1 +
 test/TestCircuitWithParameter.lean  | 1 +
 test/TestDeletionMbuCircuit.lean    | 1 +
 test/TestExtractCircuits.lean       | 1 +
 test/TestExtractGadgets.lean        | 1 +
 test/TestExtractGadgetsVectors.lean | 1 +
 test/TestGadgetExtraction.lean      | 1 +
 test/TestMerkleRecover.lean         | 1 +
 test/TestMyCircuit.lean             | 1 +
 test/TestSlicesOptimisation.lean    | 1 +
 test/TestToBinaryCircuit.lean       | 1 +
 test/TestTwoGadgets.lean            | 1 +
 14 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 59e6d01..fb3fb74 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,7 @@ circuits from [Go](https://go.dev) to [Lean](https://leanprover.github.io). In
 particular, it deals with circuits constructed as part of the
 [gnark](https://github.com/ConsenSys/gnark) proof system.
 
-This makes it possible to take existing gnark circuits and export them to Lean
+This makes possible to take existing gnark circuits and export them to Lean
 for later formal verification.
 
 For an overview of how to use this library, see both the [example](#example) and
@@ -22,9 +22,9 @@ For an overview of how to use this library, see both the [example](#example) and
 contributing, or are new to Go, please see our
 [contributing guidelines](./CONTRIBUTING.md) for more information.
 
-## Compatibility table
+## Compatibility
 This version of `gnark-lean-extractor` is compatible with `gnark v0.8.x`.
-It is recommended to import [`ProvenZK-v1.3.0`](https://github.com/reilabs/proven-zk/tree/v1.3.0) in Lean4 to process the circuits extracted with this version of `gnark-lean-extractor`.
+It is recommended to import [`ProvenZK-659b51e94d4c5160c5d93b92323f0d0dda05c3ad`](https://github.com/reilabs/proven-zk/tree/659b51e94d4c5160c5d93b92323f0d0dda05c3ad) in Lean4 to process the circuits extracted with this version of `gnark-lean-extractor`.
 
 ## Example
 
@@ -62,6 +62,7 @@ namespace MyCircuit
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 Order
 
 def circuit (In_1: F) (In_2: F) (Out: F): Prop :=
     ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧
diff --git a/extractor/lean_export.go b/extractor/lean_export.go
index 3bb487d..819c3bb 100644
--- a/extractor/lean_export.go
+++ b/extractor/lean_export.go
@@ -35,7 +35,8 @@ namespace %s
 
 def Order : ℕ := 0x%s
 variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order`, trimmedName, order.Text(16))
+abbrev F := ZMod Order
+abbrev Gates := %s Order`, trimmedName, order.Text(16), "GatesGnark8")
 
 	return s
 }
diff --git a/test/TestAnotherCircuit.lean b/test/TestAnotherCircuit.lean
index fb065b5..d94896d 100644
--- a/test/TestAnotherCircuit.lean
+++ b/test/TestAnotherCircuit.lean
@@ -8,6 +8,7 @@ namespace AnotherCircuit
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 Order
 
 def IntArrayGadget_4 (In: Vector F 4) (k: Vector F 3 -> Prop): Prop :=
     ∃gate_0, Gates.from_binary In gate_0 ∧
diff --git a/test/TestCircuitWithParameter.lean b/test/TestCircuitWithParameter.lean
index 2fdcd96..8f25822 100644
--- a/test/TestCircuitWithParameter.lean
+++ b/test/TestCircuitWithParameter.lean
@@ -8,6 +8,7 @@ namespace CircuitWithParameter
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 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] ∧
diff --git a/test/TestDeletionMbuCircuit.lean b/test/TestDeletionMbuCircuit.lean
index 680a783..c477707 100644
--- a/test/TestDeletionMbuCircuit.lean
+++ b/test/TestDeletionMbuCircuit.lean
@@ -8,6 +8,7 @@ namespace DeletionMbuCircuit
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 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
diff --git a/test/TestExtractCircuits.lean b/test/TestExtractCircuits.lean
index dea3173..d99bdc7 100644
--- a/test/TestExtractCircuits.lean
+++ b/test/TestExtractCircuits.lean
@@ -8,6 +8,7 @@ namespace MultipleCircuits
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 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] ∧
diff --git a/test/TestExtractGadgets.lean b/test/TestExtractGadgets.lean
index 128d0ac..89e19b9 100644
--- a/test/TestExtractGadgets.lean
+++ b/test/TestExtractGadgets.lean
@@ -8,6 +8,7 @@ namespace MultipleGadgets
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 Order
 
 def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧
diff --git a/test/TestExtractGadgetsVectors.lean b/test/TestExtractGadgetsVectors.lean
index 19d8286..69dae8a 100644
--- a/test/TestExtractGadgetsVectors.lean
+++ b/test/TestExtractGadgetsVectors.lean
@@ -8,6 +8,7 @@ namespace MultipleGadgetsVectors
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 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] ∧
diff --git a/test/TestGadgetExtraction.lean b/test/TestGadgetExtraction.lean
index 5faa800..1f2a9e2 100644
--- a/test/TestGadgetExtraction.lean
+++ b/test/TestGadgetExtraction.lean
@@ -8,6 +8,7 @@ namespace VectorGadget
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 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] ∧
diff --git a/test/TestMerkleRecover.lean b/test/TestMerkleRecover.lean
index e70d028..eff0016 100644
--- a/test/TestMerkleRecover.lean
+++ b/test/TestMerkleRecover.lean
@@ -8,6 +8,7 @@ namespace MerkleRecover
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 Order
 
 def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧
diff --git a/test/TestMyCircuit.lean b/test/TestMyCircuit.lean
index 431f4f8..ca2142b 100644
--- a/test/TestMyCircuit.lean
+++ b/test/TestMyCircuit.lean
@@ -8,6 +8,7 @@ namespace MyCircuit
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 Order
 
 
 
diff --git a/test/TestSlicesOptimisation.lean b/test/TestSlicesOptimisation.lean
index 15dab1c..09041ea 100644
--- a/test/TestSlicesOptimisation.lean
+++ b/test/TestSlicesOptimisation.lean
@@ -8,6 +8,7 @@ namespace SlicesOptimisation
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 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]]
diff --git a/test/TestToBinaryCircuit.lean b/test/TestToBinaryCircuit.lean
index 01a2ca9..ac67461 100644
--- a/test/TestToBinaryCircuit.lean
+++ b/test/TestToBinaryCircuit.lean
@@ -8,6 +8,7 @@ namespace ToBinaryCircuit
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 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] ∧
diff --git a/test/TestTwoGadgets.lean b/test/TestTwoGadgets.lean
index 764688d..c8b1f9e 100644
--- a/test/TestTwoGadgets.lean
+++ b/test/TestTwoGadgets.lean
@@ -8,6 +8,7 @@ namespace TwoGadgets
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark8 Order
 
 def MyWidget_11 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧

From 4cb4ba87f30b206b1c6e28cd4c3c482c33dc93d4 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Mar 2024 22:50:36 +0000
Subject: [PATCH 3/3] Updated ProvenZk dependency

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

diff --git a/README.md b/README.md
index fb3fb74..4577e6e 100644
--- a/README.md
+++ b/README.md
@@ -24,7 +24,7 @@ contributing, or are new to Go, please see our
 
 ## Compatibility
 This version of `gnark-lean-extractor` is compatible with `gnark v0.8.x`.
-It is recommended to import [`ProvenZK-659b51e94d4c5160c5d93b92323f0d0dda05c3ad`](https://github.com/reilabs/proven-zk/tree/659b51e94d4c5160c5d93b92323f0d0dda05c3ad) in Lean4 to process the circuits extracted with this version of `gnark-lean-extractor`.
+It is recommended to import [`ProvenZK-v1.4.0`](https://github.com/reilabs/proven-zk/tree/v1.4.0) in Lean4 to process the circuits extracted with this version of `gnark-lean-extractor`.
 
 ## Example