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