Prepare the repository for publication

.github/CODEOWNERS

@@ -0,0 +1,2 @@
+# General Code
+* @reilabs/formal

.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.

.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.

.github/PULL_REQUEST_TEMPLATE.md

@@ -0,0 +1,11 @@
+# Summary
+
+<!-- What is this PR about? -->
+
+# Details
+
+<!-- What do you want the reviewers to focus on? Anything important that they should know? -->
+
+# Checklist
+
+- [ ] Documentation has been updated if necessary.

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.
+

README.md

@@ -0,0 +1,98 @@
+<p align=center>
+  <img src="https://user-images.githubusercontent.com/5780639/237803894-e2344067-aa77-488e-b2d0-6f980524dced.svg"/>
+</p>
+
+# 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.
+