Skip to content

Commit

Permalink
Added GatesGnark9 header and updated to v3
Browse files Browse the repository at this point in the history
  • Loading branch information
Eagle941 committed Mar 28, 2024
1 parent 006ee56 commit 501e57e
Show file tree
Hide file tree
Showing 26 changed files with 36 additions and 34 deletions.
6 changes: 4 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,11 @@ contributing, or are new to Go, please see our
[contributing guidelines](./CONTRIBUTING.md) for more information.

## Compatibility
This version of `gnark-lean-extractor` is compatible with `gnark v0.8.x`.
This version of `gnark-lean-extractor` is compatible with `gnark v0.9.x`.
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`.

For compatibility with `gnark v0.8.x`, use `gnark-lean-extractor-v2.2.0`.

## Example

The following is a brief example of how to design a simple gnark circuit in
Expand Down Expand Up @@ -62,7 +64,7 @@ namespace MyCircuit
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark8 Order
abbrev Gates := GatesGnark9 Order
def circuit (In_1: F) (In_2: F) (Out: F): Prop :=
∃gate_0, gate_0 = Gates.add In_1 In_2 ∧
Expand Down
2 changes: 1 addition & 1 deletion extractor/extractor.go
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ import (
"github.com/consensys/gnark/frontend"
"github.com/consensys/gnark/frontend/schema"

"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
)

type Operand interface {
Expand Down
2 changes: 1 addition & 1 deletion extractor/interface.go
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
"golang.org/x/exp/slices"
)

Expand Down
2 changes: 1 addition & 1 deletion extractor/lean_export.go
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ namespace %s
def Order : ℕ := 0x%s
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := %s Order`, trimmedName, order.Text(16), "GatesGnark8")
abbrev Gates := %s Order`, trimmedName, order.Text(16), "GatesGnark9")

return s
}
Expand Down
2 changes: 1 addition & 1 deletion extractor/misc.go
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ import (
"github.com/consensys/gnark/frontend"
"github.com/consensys/gnark/frontend/schema"
"github.com/mitchellh/copystructure"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
)

// recoverError is used in the top level interface to prevent panic
Expand Down
4 changes: 2 additions & 2 deletions extractor/test/another_circuit_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v2/extractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/extractor"
)

// Example: Gadget with nested array of int
Expand Down
4 changes: 2 additions & 2 deletions extractor/test/circuit_with_parameter_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v2/extractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/extractor"
"github.com/stretchr/testify/assert"
)

Expand Down
4 changes: 2 additions & 2 deletions extractor/test/deletion_mbu_circuit_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v2/extractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/extractor"
)

// Example: Mismatched arguments error
Expand Down
4 changes: 2 additions & 2 deletions extractor/test/merkle_recover_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v2/extractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/extractor"
)

// Example: circuit with arrays and gadget
Expand Down
2 changes: 1 addition & 1 deletion extractor/test/my_circuit_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/extractor"
"github.com/reilabs/gnark-lean-extractor/v3/extractor"
)

// Example: readme circuit
Expand Down
4 changes: 2 additions & 2 deletions extractor/test/slices_optimisation_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v2/extractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/extractor"
)

// Example: checking slices optimisation
Expand Down
4 changes: 2 additions & 2 deletions extractor/test/to_binary_circuit_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v2/extractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/extractor"
)

// Example: Gadget that returns a vector
Expand Down
4 changes: 2 additions & 2 deletions extractor/test/two_gadgets_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ import (

"github.com/consensys/gnark-crypto/ecc"
"github.com/consensys/gnark/frontend"
"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
"github.com/reilabs/gnark-lean-extractor/v2/extractor"
"github.com/reilabs/gnark-lean-extractor/v3/abstractor"
"github.com/reilabs/gnark-lean-extractor/v3/extractor"
)

// Example: circuit with multiple gadgets
Expand Down
2 changes: 1 addition & 1 deletion go.mod
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
module github.com/reilabs/gnark-lean-extractor/v2
module github.com/reilabs/gnark-lean-extractor/v3

go 1.20

Expand Down
2 changes: 1 addition & 1 deletion test/TestAnotherCircuit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ namespace AnotherCircuit
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
variable [Fact (Nat.Prime Order)]
abbrev F := ZMod Order
abbrev Gates := GatesGnark8 Order
abbrev Gates := GatesGnark9 Order

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



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

Please sign in to comment.