Skip to content

Commit

Permalink
Updated readme
Browse files Browse the repository at this point in the history
  • Loading branch information
Eagle941 committed Feb 29, 2024
1 parent bbace65 commit 47a2d9c
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 5 deletions.
15 changes: 12 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,10 @@ For an overview of how to use this library, see both the [example](#example) and
contributing, or are new to Go, please see our
[contributing guidelines](./CONTRIBUTING.md) for more information.

## Compatibility table
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`.

## Example

The following is a brief example of how to design a simple gnark circuit in
Expand All @@ -45,9 +49,14 @@ func (circuit MyCircuit) Define(api frontend.API) error {
}
```

Once you export this to Lean, you get a definition as follows:
Once you export `MyCircuit` to Lean, you obtain the following definition:

```lean
import ProvenZk.Gates
import ProvenZk.Ext.Vector
set_option linter.unusedVariables false
namespace MyCircuit
def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
Expand Down Expand Up @@ -87,15 +96,15 @@ aforementioned gnark library, and then call the extractor function

```go
circuit := MyCircuit{}
out, err := CircuitToLean(&circuit, ecc.BN254)
out, err := extractor.CircuitToLean(&circuit, ecc.BN254)
if err != nil {
log.Fatal(err)
}
fmt.Println(out)
```

`CircuitToLean` returns a string which contains the circuit output in a format
that can be read by the Lean language. The lean code depends on Reilabs'
that can be read by the Lean language. The Lean code depends on Reilabs'
[ProvenZK](https://github.com/reilabs/proven-zk) library in order to represent
gates and other components of the circuit. In doing so, it makes the extracted
circuit formally verifiable.
Expand Down
4 changes: 2 additions & 2 deletions extractor/test/my_circuit_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ func (circuit *MyCircuit) Define(api frontend.API) error {
}

func TestMyCircuit(t *testing.T) {
assignment := MyCircuit{}
out, err := extractor.CircuitToLean(&assignment, ecc.BN254)
circuit := MyCircuit{}
out, err := extractor.CircuitToLean(&circuit, ecc.BN254)
if err != nil {
log.Fatal(err)
}
Expand Down

0 comments on commit 47a2d9c

Please sign in to comment.