Skip to content

Commit

Permalink
feat: gates version in header (#44)
Browse files Browse the repository at this point in the history
* Updated readme

* Added GatesGnark8

* Updated ProvenZk dependency
  • Loading branch information
Eagle941 authored Mar 28, 2024
1 parent 9109bfe commit 37dfe6a
Show file tree
Hide file tree
Showing 14 changed files with 18 additions and 4 deletions.
7 changes: 4 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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 ∧
Expand Down
3 changes: 2 additions & 1 deletion extractor/lean_export.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down
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 := GatesGnark8 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 := 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] ∧
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 := 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
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 := 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] ∧
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 := GatesGnark8 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 := 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] ∧
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 := 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] ∧
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 := GatesGnark8 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 := GatesGnark8 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 := 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]]
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 := 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] ∧
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 := 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 ∧
Expand Down

0 comments on commit 37dfe6a

Please sign in to comment.