[specs] introducing specifications

.github/workflows/gh-page.yml

@@ -0,0 +1,48 @@
+name: Deploy Specifications & Docs to GitHub Pages
+
+on:
+  push:
+    branches:
+      - master
+
+jobs:
+  release:
+    name: GitHub Pages
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v2
+
+      - name: Setup OCaml (because of ocaml-gen)
+        run: sudo apt update && sudo apt install ocaml
+
+      - name: Build Rust Documentation
+        run: |
+          rustup install nightly
+          RUSTDOCFLAGS="--enable-index-page -Zunstable-options" cargo +nightly doc --all --no-deps
+
+      - name: Check that up-to-date specification is checked in
+        run: |
+          cargo install cargo-spec
+          cd book/specifications
+          cd kimchi && make build && cd ..
+          cd poly-commitment && make build && cd ..
+          git diff --exit-code
+
+      - name: Build the mdbook
+        run: |
+          cd book
+          cargo install mdbook
+          cargo install mdbook-katex
+          mdbook build
+
+      - name: Arrange website folder hierarchy
+        run: |
+          mv ./target/doc ./book/book/html/rustdoc
+
+      - name: Deploy
+        uses: peaceiris/actions-gh-pages@v3
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: ./book/book/html

README.md

@@ -1,9 +1,12 @@
 # Proof Systems
 
-This repository contains various zk-SNARK protocol implementations for recursive SNARK composition.
+This repository contains various zk-SNARK protocol implementations for recursive SNARK composition. [See here for the rust documentation](https://o1-labs.github.io/proof-systems/rustdoc).
+
+Organization:
 
 ```
 proof-systems/
+├── book # the mina book, RFCs, and specifications
 ├── cairo # a Cairo runner written in rust
 ├── curves/ # our curves (for now just the pasta curves)
 ├── groupmap/ # TODO: description

book/.gitignore

@@ -0,0 +1 @@
+book

book/README.md

@@ -0,0 +1,16 @@
+# Mina book
+
+This directory holds the code related to documentation and specifications of the proof systems.
+
+It is built with [mdbook](https://rust-lang.github.io/mdBook/), which you can use to serve the page via the following command:
+
+```console
+$ # setup
+$ cargo install mdbook
+$ cargo install mdbook-katex
+$ cargo install mdbook-linkcheck
+$ # serve the page locally
+$ mdbook serve
+```
+
+The specifications in the book are dynamically generated. Refer to the [specifications/](specifications/) directory.

book/book.toml

@@ -0,0 +1,14 @@
+[book]
+authors = ["Izaak Meckler", "Vanishree Rao", "Matthew Ryan", "Joseph Spadavecchia", "David Wong", "Vitaly Zelov"]
+language = "en"
+multilingual = false
+src = "src"
+title = "Mina book"
+
+[output.html]
+site-url = "/proof-systems/"
+curly-quotes = true
+git-repository-url = "https://www.github.com/o1-labs/proof-systems"
+
+# for LaTeX
+[preprocessor.katex]

book/specifications/README.md

@@ -0,0 +1,47 @@
+# Specifications
+
+The `specifications/` directory hosts specifications-related code:
+
+* [poly-commitment/](poly-commitment/) contains the specification for the polynomial commitment scheme
+* [kimchi/](kimchi/) contains the specification for the proof system
+
+The specifications are written using [cargo-spec](https://crates.io/crates/cargo-spec), which combines markdown files as well as text extracted directly from the code.
+
+## Set up
+
+Install cargo-spec:
+
+```console
+$ cargo install cargo-spec
+```
+
+## Render
+
+To produce a specification, simply run the following command:
+
+```console
+$ cd <spec_folder> && make build
+```
+
+If you want to watch for any changes, you can also run the following command:
+
+```console
+$ cd <spec_folder> && make watch
+```
+
+## How to edit the specifications
+
+Each folder has the following files:
+
+* a `Specification.toml` file that lists some metadata, the path to a template file, and a list of files to parse for the specification.
+* a `template.md` template, which is used as the main specification. Some placeholders will be replaced with information parsed from the code.
+
+Each file listed in the `Specification.toml` have special comments (`//~`) that will be extracted verbatim, and placed within the template.
+
+The idea is to keep as much of the specification close to the source, so that modification of the code and the spec can be done in the same place.
+
+## How to edit the deployment
+
+The specifications are built into the Mina book, and deployed to Github pages, via [this Github Action](/.github/workflows/website.yml).
+
+The Github Action ensures that the generated specifications that are pushed to the remote repository are also up to date.

book/specifications/kimchi/Makefile

@@ -0,0 +1,11 @@
+.PHONY: build watch
+
+OUT_FILE := ../../src/specs/kimchi.md
+
+# builds the specification once
+build:
+	cargo spec --output-file $(OUT_FILE)
+
+# watches specification-related files and rebuilds them on the fly
+watch:
+	cargo spec --output-file $(OUT_FILE) watch

book/specifications/kimchi/Specification.toml

@@ -0,0 +1,26 @@
+[metadata]
+name = "Kimchi"
+description = "This specification describes the Kimchi proof system."
+version = "0.1.0"
+authors = ["TODO: ENTER ALL THE NAMES"]
+
+[config]
+template = "template.md"
+
+[sections]
+permutation = "../../../kimchi/src/circuits/polynomials/permutation.rs"
+lookup = "../../../kimchi/src/circuits/polynomials/lookup.rs"
+
+# gates
+chacha = "../../../kimchi/src/circuits/polynomials/chacha.rs"
+complete_add = "../../../kimchi/src/circuits/polynomials/complete_add.rs"
+endomul_scalar = "../../../kimchi/src/circuits/polynomials/endomul_scalar.rs"
+endosclmul = "../../../kimchi/src/circuits/polynomials/endosclmul.rs"
+generic = "../../../kimchi/src/circuits/polynomials/generic.rs"
+poseidon = "../../../kimchi/src/circuits/polynomials/poseidon.rs"
+varbasemul = "../../../kimchi/src/circuits/polynomials/varbasemul.rs"
+
+constraint_system = "../../../kimchi/src/circuits/constraints.rs"
+indexes = "../../../kimchi/src/index.rs"
+prover = "../../../kimchi/src/prover.rs"
+verifier = "../../../kimchi/src/verifier.rs"

book/specifications/kimchi/template.md

@@ -0,0 +1,4 @@
+# Kimchi
+
+This document specifies the kimchi variant of PLONK.
+

book/specifications/poly-commitment/Makefile

@@ -0,0 +1,11 @@
+.PHONY: build watch
+
+OUT_FILE := ../../src/specs/poly-commitment.md
+
+# builds the specification once
+build:
+	cargo spec --output-file $(OUT_FILE)
+
+# watches specification-related files and rebuilds them on the fly
+watch:
+	cargo spec --output-file $(OUT_FILE) watch

book/specifications/poly-commitment/Specification.toml

@@ -0,0 +1,11 @@
+[metadata]
+name = "Polynomial Commitment"
+description = "This specification describes the Kimchi polynomial commitment."
+version = "0.1.0"
+authors = ["TODO: ENTER ALL THE NAMES"]
+
+[config]
+template = "template.md"
+
+[sections]
+verifier = "../../poly-commitment/src/lib.rs"

book/specifications/poly-commitment/template.md

@@ -0,0 +1,7 @@
+# Kimchi Polynomial Commitment
+
+Our polynomial commitment scheme is a bootleproof-type of commitment scheme, which is a mix of:
+
+* The polynomial commitment scheme described in appendix A.1 of the [PCD paper](https://eprint.iacr.org/2020/1618).
+* The zero-knowledge opening described in section 3.1 of the [HALO paper](https://eprint.iacr.org/2019/1021).
+

book/src/SUMMARY.md

@@ -0,0 +1,9 @@
+# Summary
+
+- [Introduction](./introduction.md)
+
+# Specifications
+
+- [Pasta curves](./specs/pasta.md)
+- [Polynomial commitment](./specs/poly-commitment.md)
+- [Kimchi](./specs/kimchi.md)

book/src/introduction.md

@@ -0,0 +1,3 @@
+# Introduction
+
+This page hosts specifications for some of the cryptographic algorithms of [Mina](https://minaprotocol.com/). [For the Rust documentation, see here](/rustdoc).

book/src/specs/kimchi.md

@@ -0,0 +1,106 @@
+# Kimchi
+
+This document specifies the kimchi variant of PLONK.
+
+## Overview
+
+The document follows the following structure:
+
+TODO: simply create a ToC no?
+
+1. **Setup**. A one-time setup for the proof system.
+2. **Per-circuit setup**. A one-time setup for each circuit that are used in the proof system.
+3. **Proof creation**. How to create a proof.
+4. **Proof verification**. How to verify a proof.
+
+## Dependencies
+
+### Polynomial Commitments
+
+Refer to the [specification on polynomial commitments](). We make use of the following functions from that specification:
+
+- `PolyCom.non_hiding_commit(poly) -> PolyCom::NonHidingCommitment`
+- `PolyCom.commit(poly) -> PolyCom::HidingCommitment`
+- `PolyCom.evaluation_proof(poly, commitment, point) -> EvaluationProof`
+- `PolyCom.verify(commitment, point, evaluation, evaluation_proof) -> bool`
+
+### Poseidon hash function
+
+Refer to the [specification on Poseidon](). We make use of the following functions from that specification:
+
+- `Poseidon.init(params) -> FqSponge`
+- `Poseidon.update(field_elem)`
+- `Poseidon.finalize() -> FieldElem`
+
+specify the following functions on top:
+
+- `Poseidon.produce_challenge()` (TODO: uses the endomorphism)
+- `Poseidon.to_fr_sponge() -> state_of_fq_sponge_before_eval, FrSponge`
+
+### Pasta
+
+Kimchi is made to work on cycles of curves, so the protocol switch between two fields Fq and Fr, where Fq represents the base field and Fr represents the scalar field.
+
+## Constraints
+
+### Permutation
+
+
+
+### Lookup
+
+
+
+### Gates
+
+#### Generic Gate
+
+
+
+#### Poseidon
+
+
+
+#### chacha 
+
+
+
+#### complete_add 
+
+
+
+#### endomul_scalar 
+
+
+
+#### endosclmul 
+
+
+
+#### poseidon 
+
+
+
+#### varbasemul 
+
+
+
+## constraint system creation (circuit creation)
+
+
+
+## prover and verifier index creation
+
+
+
+## proof data structure
+
+TKTK
+
+## proof creation
+
+
+
+## proof verification
+
+