feat: gates version in header

README.md

@@ -14,17 +14,17 @@ 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
 [usage guide](#how-to-use-the-library) below. If you are interested in
 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-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
 
@@ -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 ∧

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
 }

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 ∧

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] ∧

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

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] ∧

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 ∧

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] ∧

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] ∧

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 ∧

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
 
 
 

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]]

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] ∧

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 ∧