From 76b574dc0177535a2e2591be97cd74506a3a8057 Mon Sep 17 00:00:00 2001 From: Ara Adkins Date: Mon, 31 Jul 2023 12:18:47 -0600 Subject: [PATCH] Prepare the repository for publication --- .github/CODEOWNERS | 2 + .github/ISSUE_TEMPLATE/bug_report.md | 24 +++++++ .github/ISSUE_TEMPLATE/task.md | 15 +++++ .github/PULL_REQUEST_TEMPLATE.md | 11 ++++ CONTRIBUTING.md | 76 +++++++++++++++++++++ README.md | 98 ++++++++++++++++++++++++++++ readme.md | 61 ----------------- 7 files changed, 226 insertions(+), 61 deletions(-) create mode 100644 .github/CODEOWNERS create mode 100644 .github/ISSUE_TEMPLATE/bug_report.md create mode 100644 .github/ISSUE_TEMPLATE/task.md create mode 100644 .github/PULL_REQUEST_TEMPLATE.md create mode 100644 CONTRIBUTING.md create mode 100644 README.md delete mode 100644 readme.md diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS new file mode 100644 index 0000000..bc1c4ff --- /dev/null +++ b/.github/CODEOWNERS @@ -0,0 +1,2 @@ +# General Code +* @reilabs/formal diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md new file mode 100644 index 0000000..2fd219d --- /dev/null +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -0,0 +1,24 @@ +--- +name: Bug report +about: Found something wrong? Let us know. +title: "[BUG] " +labels: bug +assignees: '' +--- + +# Describe the Bug + +A clear and concise description of what the bug is. + +# To Reproduce + +Steps to reproduce the behavior: + +1. Go to '...' +2. Click on '....' +3. Scroll down to '....' +4. See error + +# Expected Behaviour + +A clear and concise description of what you expected to happen. diff --git a/.github/ISSUE_TEMPLATE/task.md b/.github/ISSUE_TEMPLATE/task.md new file mode 100644 index 0000000..7a805d9 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/task.md @@ -0,0 +1,15 @@ +--- +name: Task +about: Something that needs doing. +title: "[TASK] " +labels: enhancement +assignees: '' +--- + +# Description + +What is this about? + +# Spec + +Give details. diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md new file mode 100644 index 0000000..805e5f6 --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -0,0 +1,11 @@ +# Summary + + + +# Details + + + +# Checklist + +- [ ] Documentation has been updated if necessary. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..7c730ec --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,76 @@ +# Contributing + +This document exists as a brief introduction for how you can contribute to this +repository. It includes a guide to +[the structure of the repository](#repository-structure), +[building and testing](#building-and-testing) and +[getting your code on `main`](#getting-your-code-on-main). + +If you are new to Go, there is a [guide](#new-to-go) to getting started with the +language that provides some basic resources for getting started. + +> ## Font Display in Powershell +> +> If using Powershell, change font to `NSimSun` to be able to see all characters +> properly. This is taken from +> [this stackoverflow answer](https://stackoverflow.com/a/48029600). + +## Repository Structure + +This repository consists of two primary parts. + +- [`abstractor`](./abstractor): The abstractor, which is responsible for + providing an abstract front-end to various ZK systems. +- [`extractor`](./extractor): The extractor, which is responsible for providing + the interface and tools that allow the generation of the Lean code from the + circuit defined in Go. + +## Building and Testing + +You can build and test the go project as follows. + +1. Clone the repository into a location of your choice. + +```sh +git clone https://github.com/reilabs/gnark-lean-extractor gnark-lean-demo +``` + +2. Build the go circuit project using `go` (meaning that you will need to have + that toolchain set up). + +```sh +cd gnark-lean-abstractor +go build +``` + +3. To run the tests, you can also use `go`. + +```sh +go test +``` + +## Getting Your Code on `main` + +This repository works on a fork and +[pull request](https://github.com/reilabs/gnark-lean-demo/pulls) workflow, with +code review and CI as an integral part of the process. This works as follows: + +1. If necessary, you fork the repository, but if you have access to do so please + create a branch. +2. You make your changes on that branch. +3. Pull request that branch against main. +4. The pull request will be reviewed and CI will be run on it. +5. Once the reviewer(s) have accepted the code and CI has passed, the code will + be merged to `main`. + +## New to Go? + +If you are new to working with [Go](https://go.dev), a great place to start is +the official set of [tutorials](https://go.dev/learn/). They explain how to +[install](https://go.dev/doc/install) and set the language up, as well as an +[interactive tour](https://go.dev/tour/welcome/1) of how to use the language. + +We recommend being familiar with the language and the `go` command-line +interface to the build system and compiler before interacting with the Go +portion of this repository. + diff --git a/README.md b/README.md new file mode 100644 index 0000000..d7a68ba --- /dev/null +++ b/README.md @@ -0,0 +1,98 @@ +

+ +

+ +# Gnark Lean Extractor + +This repository contains a Go library that transpiles +[zero-knowledge](https://en.wikipedia.org/wiki/Zero-knowledge_proof) (ZK) +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 +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. + +## Example + +The following is a brief example of how to design a simple gnark circuit in +conjunction with the extractor library. + +```go +type MyCircuit struct { + In_1 frontend.Variable + In_2 frontend.Variable + Out frontend.Variable +} + +func (circuit *MyCircuit) AbsDefine(api abstractor.API) error { + sum := api.Add(circuit.In_1, circuit.In_2) + api.AssertIsEqual(sum, circuit.Out) + return nil +} + +func (circuit *MyCircuit) Define(api frontend.API) error { + return abstractor.Concretize(api, circuit) +} +``` + +Once you export this to Lean, you get a definition as follows: + +```lean +namespace DummyCircuit + +def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 +variable [Fact (Nat.Prime Order)] +abbrev F := ZMod Order + +def circuit (In_1: F) (In_2: F) (Out: F): Prop := + ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧ + Gates.eq gate_0 Out ∧ + True + +end DummyCircuit +``` + +Further examples of this process with various levels of complexity can be seen +in [`extractor_test.go`](./extractor/extractor_test.go). You can also peruse the +[Gnark Extractor Demo](https://github.com/reilabs/gnark-lean-demo), which uses +this library alongside an implementation of +[Semaphore](https://semaphore.appliedzkp.org). + +## How to Use the Library + +If you are familiar with the [gnark library](https://github.com/consensys/gnark) +(as you will need to be to write ZK circuits), the circuit API in this library +should be familiar. + +Based directly on the gnark interface, this library adds "gadgets" and hence +makes it easy to integrate with existing circuits. To do so, you have to +implement the `AbsDefine` method for the struct that represents your circuit +(`MyCircuit` in the example below). You can use the `abstractor.Concretize` +function to automatically derive an implementation of `Define` for further use +with gnark. + +After doing that, you choose a circuit curve from those present in the +aforementioned gnark library, and then call the extractor function +`CircuitToLean`. + +```go +circuit := MyCircuit{} +out, err := 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' +[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. + diff --git a/readme.md b/readme.md deleted file mode 100644 index a72638d..0000000 --- a/readme.md +++ /dev/null @@ -1,61 +0,0 @@ -# `gnark-lean-extractor` library - -This is a transpiler from `Go` to `Lean` for arithmetic circuits. You can design your circuit in `Go` and export it to `Lean`. -The benefit of this library is the ability to prototype circuits in a high level language and perform formal verification using `Lean`. - -## Example -Here is how a simple circuit is designed using the `gnark-lean-extractor` library: - -```go -type DummyCircuit struct { - In_1 frontend.Variable - In_2 frontend.Variable - Out frontend.Variable -} - -func (circuit *DummyCircuit) AbsDefine(api abstractor.API) error { - sum := api.Add(circuit.In_1, circuit.In_2) - api.AssertIsEqual(sum, circuit.Out) - return nil -} -``` - -Here is how it looks like exported for `Lean`: - -```lean -namespace DummyCircuit - -def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 -variable [Fact (Nat.Prime Order)] -abbrev F := ZMod Order - -def circuit (In_1: F) (In_2: F) (Out: F): Prop := - ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧ - Gates.eq gate_0 Out ∧ - True - -end DummyCircuit -``` - -Further examples are available in `extractor/extractor_test.go` with various levels of complexity. - -## How to use -The circuit API is based on the `consensys/gnark` library with the addition of Gadgets: this makes for easy integration of existing circuits. -To integrate your own circuit, implement the methods `AbsDefine` and `Define` for `MyCircuit` struct. Choose a circuit curve, then call the extractor with the function `CircuitToLean`: - -```go -assignment := MyCircuit{} -out, err := CircuitToLean(&assignment, ecc.BN254) -if err != nil { - log.Fatal(err) -} -fmt.Println(out) -``` - -The curves supported match the curves present in the library `consensys/gnark`. - -`CircuitToLean` returns a string which contains the circuit in a format readable by `Lean`. The `Lean` code depends on the library `proven-zk` for the representation of Gates, Vectors and other useful circuit verification utilities. - -## Notes -If using Powershell, change font to `NSimSun` for correct view of all characters: -[check this answer](https://stackoverflow.com/a/48029600) \ No newline at end of file