Added gnark switch

reilabs · Nov 29, 2023 · f91bd79 · f91bd79
1 parent 9fdbd13
commit f91bd79
Show file tree

Hide file tree

Showing 15 changed files with 18 additions and 4 deletions.
diff --git a/go.mod b/go.mod
@@ -5,7 +5,7 @@ go 1.20
 require (
 	github.com/consensys/gnark v0.8.0
 	github.com/consensys/gnark-crypto v0.9.1
-	github.com/reilabs/lean-circuit-compiler v0.0.0-20231121161717-dbb1e041674f
+	github.com/reilabs/lean-circuit-compiler v0.0.0-20231129181745-d11ee38d5b78
 	github.com/stretchr/testify v1.8.1
 	golang.org/x/exp v0.0.0-20230905200255-921286631fa9
 )

diff --git a/go.sum b/go.sum
@@ -35,6 +35,8 @@ github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZb
 github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4=
 github.com/reilabs/lean-circuit-compiler v0.0.0-20231121161717-dbb1e041674f h1:Tc0JpVwbO3201BRJmzsAOoFHnu8+JNP1t3xfobx3KoI=
 github.com/reilabs/lean-circuit-compiler v0.0.0-20231121161717-dbb1e041674f/go.mod h1:omNt4iZc1iRuWNHG9O0ltoGG2MuizDELooBIrxVgz8E=
+github.com/reilabs/lean-circuit-compiler v0.0.0-20231129181745-d11ee38d5b78 h1:e+dtLJo1iliiX+OanXlWXIYAzVFgV+sRd1pv3U0G1ts=
+github.com/reilabs/lean-circuit-compiler v0.0.0-20231129181745-d11ee38d5b78/go.mod h1:omNt4iZc1iRuWNHG9O0ltoGG2MuizDELooBIrxVgz8E=
 github.com/rogpeppe/go-internal v1.10.0 h1:TMyTOH3F/DB16zRVcYyreMH6GnZZrwQVAoYjRBZyWFQ=
 github.com/rogpeppe/go-internal v1.10.0/go.mod h1:UQnix2H7Ngw/k4C5ijL5+65zddjncjaFoBhdsK/akog=
 github.com/rs/xid v1.4.0/go.mod h1:trrq9SKmegXys3aeAKXMUTdJsYXVwGY3RLcfgqegfbg=

diff --git a/parser/interface.go b/parser/interface.go
@@ -45,7 +45,7 @@ func GadgetToLeanWithName(gadget abstractor.GadgetDefinition, field ecc.ID, name
 
 	api := GetExtractor(field)
 	api.DefineGadget(gadget)
-	return extractor.ExportGadgetsOnly(namespace, api.ext.GetGadgets(), api.ext.GetField()), nil
+	return extractor.ExportGadgetsOnly(namespace, api.ext.GetGadgets(), api.ext.GetField(), extractor.Gnark8), nil
 }
 
 // GadgetToLean exports a `gadget` to Lean over a `field`
@@ -87,7 +87,7 @@ func ExtractCircuits(namespace string, field ecc.ID, circuits ...extractor.Extra
 		api.ext.ResetCode()
 	}
 
-	return extractor.GenerateLeanCircuits(namespace, &api.ext, circuits_extracted), nil
+	return extractor.GenerateLeanCircuits(namespace, &api.ext, circuits_extracted, extractor.Gnark8), nil
 }
 
 // ExtractGadgets is used to export a series of `gadgets` to Lean over a `field` under `namespace`.
@@ -99,5 +99,5 @@ func ExtractGadgets(namespace string, field ecc.ID, gadgets ...abstractor.Gadget
 	for _, gadget := range gadgets {
 		api.DefineGadget(gadget)
 	}
-	return extractor.ExportGadgetsOnly(namespace, api.ext.GetGadgets(), api.ext.GetField()), nil
+	return extractor.ExportGadgetsOnly(namespace, api.ext.GetGadgets(), api.ext.GetField(), extractor.Gnark8), nil
 }
diff --git 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 := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace CircuitWithParameter
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace DeletionMbuCircuit
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace MultipleCircuits
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace MultipleGadgets
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace MultipleGadgetsVectors
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace VectorGadget
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace MerkleRecover
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace MyCircuit
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 Order
 
 
 

diff --git 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 := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace ToBinaryCircuit
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 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
@@ -8,6 +8,7 @@ namespace TwoGadgets
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark_8 Order
 
 def MyWidget_11 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧