## ProvenZK

This repository contains `proven-zk`

, a library designed to assist in the
Lean-based analysis and verification of
zero-knowledge (ZK)
circuits. It is currently developed to work with
gnark circuits extracted from Go using
Reilabs' Gnark Extractor, but
may be expanded to work with other ZK systems in the future.

For an overview of how how you can use the library, and the components it provides. If you would like to contribute, or are looking for some resources on getting started with Lean, please see our contributing guide.

### How to Use the Library

We assume that you are building your lean projects using the `lake`

tool, and
hence have a `lakefile.lean`

. You can add the library as a dependency to that
file as follows.

```
require ProvenZK from git
"https://github.com/reilabs/proven-zk.git"
```

### Components

The library provides a number of components that are useful for the formal verification of zero knowledge circuits.

The basic definitions of the gates can be found in
`Gates.lean`

, and
`Vector.lean`

and are the core components used to
represent gates and vectors in the formal representation of these circuits.

You can import these as follows:

```
import ProvenZk.Gates
import ProvenZk.Ext.Vector
```

The gates in ProvenZK are implemented using modular arithmetic using the
`ZMod`

type from Mathlib 4.
For available operations please see the definitions in
`Gates.lean`

.

The other main components of the library contain of multiple theorems to assist with the formal verification of circuits. These are as follows:

`import ProvenZK.Binary`

: The definition of the`Bits`

type, as well as various theorems to assist in working with the`to_binary`

and`from_binary`

functions.`import ProvenZK.Hash`

: The definition of the perfect hash to be used for the purposes of formal verification.`import ProvenZK.Merkle`

: The definition of the merkle tree and associated theorems that assist in the formal verification of circuits working with this data type.

In addition to these main interfaces to the library, there are additional helper functions and theorems that can be found in the following files.

```
import ProvenZk.Ext.Range
import ProvenZk.Ext.Matrix
import ProvenZk.Ext.List
```