Skip to content

Commit

Permalink
Fixed gnark version
Browse files Browse the repository at this point in the history
  • Loading branch information
Eagle941 committed Nov 29, 2023
1 parent 176ff5e commit fe8ef53
Show file tree
Hide file tree
Showing 15 changed files with 22 additions and 6 deletions.
2 changes: 1 addition & 1 deletion go.mod
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ go 1.20
require (
github.com/consensys/gnark v0.9.1
github.com/consensys/gnark-crypto v0.12.2-0.20231013160410-1f65e75b6dfb
github.com/reilabs/lean-circuit-compiler v0.0.0-20231121161717-dbb1e041674f
github.com/reilabs/lean-circuit-compiler v0.0.0-20231129183530-39ea82720a07
github.com/stretchr/testify v1.8.4
golang.org/x/exp v0.0.0-20230905200255-921286631fa9
)
Expand Down
4 changes: 4 additions & 0 deletions go.sum
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,10 @@ 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/reilabs/lean-circuit-compiler v0.0.0-20231129183530-39ea82720a07 h1:ygU73nU3dBkRWyMaW9QoxQcDeos9Py8nxwxj1HTnKGg=
github.com/reilabs/lean-circuit-compiler v0.0.0-20231129183530-39ea82720a07/go.mod h1:omNt4iZc1iRuWNHG9O0ltoGG2MuizDELooBIrxVgz8E=
github.com/rogpeppe/go-internal v1.11.0 h1:cWPaGQEPrBb5/AsnsZesgZZ9yb1OQ+GOISoDNXVBh4M=
github.com/rs/xid v1.5.0/go.mod h1:trrq9SKmegXys3aeAKXMUTdJsYXVwGY3RLcfgqegfbg=
github.com/rs/zerolog v1.30.0 h1:SymVODrcRsaRaSInD9yQtKbtWqwsfoPcRff/oRXLj4c=
Expand Down
10 changes: 5 additions & 5 deletions parser/interface.go
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ func CircuitToLeanWithName(circuit extractor.ExtractorCircuit, field ecc.ID, nam
return "", err
}

return extractor.GenerateLeanCode(namespace, &api.ext, circuit, schema.Fields)
return extractor.GenerateLeanCode(namespace, &api.ext, circuit, schema.Fields, extractor.Gnark9)
}

// CircuitToLean exports a `circuit` to Lean over a `field` with the namespace being the
Expand All @@ -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.Gnark9), nil
}

// GadgetToLean exports a `gadget` to Lean over a `field`
Expand Down Expand Up @@ -80,14 +80,14 @@ func ExtractCircuits(namespace string, field ecc.ID, circuits ...extractor.Extra
return "", err
}

circuit_def := extractor.GenerateLeanCircuit(name, &api.ext, circuit, schema.Fields)
circuit_def := extractor.GenerateLeanCircuit(name, &api.ext, circuit, schema.Fields, extractor.Gnark9)
circuits_extracted = append(circuits_extracted, circuit_def)

// Resetting elements for next circuit
api.ext.ResetCode()
}

return extractor.GenerateLeanCircuits(namespace, &api.ext, circuits_extracted), nil
return extractor.GenerateLeanCircuits(namespace, &api.ext, circuits_extracted, extractor.Gnark9), nil
}

// ExtractGadgets is used to export a series of `gadgets` to Lean over a `field` under `namespace`.
Expand All @@ -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.Gnark9), nil
}
1 change: 1 addition & 0 deletions test/TestAnotherCircuit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace AnotherCircuit
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 Order

def IntArrayGadget_4 (In: Vector F 4) (k: Vector F 3 -> Prop): Prop :=
∃gate_0, Gates.from_binary In gate_0 ∧
Expand Down
1 change: 1 addition & 0 deletions test/TestCircuitWithParameter.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace CircuitWithParameter
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 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] ∧
Expand Down
1 change: 1 addition & 0 deletions test/TestDeletionMbuCircuit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace DeletionMbuCircuit
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 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
Expand Down
1 change: 1 addition & 0 deletions test/TestExtractCircuits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace MultipleCircuits
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 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] ∧
Expand Down
1 change: 1 addition & 0 deletions test/TestExtractGadgets.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace MultipleGadgets
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 Order

def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop :=
∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧
Expand Down
1 change: 1 addition & 0 deletions test/TestExtractGadgetsVectors.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace MultipleGadgetsVectors
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 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] ∧
Expand Down
1 change: 1 addition & 0 deletions test/TestGadgetExtraction.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace VectorGadget
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 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] ∧
Expand Down
1 change: 1 addition & 0 deletions test/TestMerkleRecover.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace MerkleRecover
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 Order

def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop :=
∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧
Expand Down
1 change: 1 addition & 0 deletions test/TestMyCircuit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace MyCircuit
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 Order



Expand Down
1 change: 1 addition & 0 deletions test/TestSlicesOptimisation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace SlicesOptimisation
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 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]]
Expand Down
1 change: 1 addition & 0 deletions test/TestToBinaryCircuit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace ToBinaryCircuit
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 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] ∧
Expand Down
1 change: 1 addition & 0 deletions test/TestTwoGadgets.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ namespace TwoGadgets
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark_9 Order

def MyWidget_11 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop :=
∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧
Expand Down

0 comments on commit fe8ef53

Please sign in to comment.