Merge pull request #1346 from o1-labs/dw/update-doc-lookup

Book: revisit some old updates

.github/workflows/gh-page.yml

@@ -41,6 +41,7 @@ jobs:
           # https://github.com/ocaml/setup-ocaml/issues/211#issuecomment-1058882386
           # disable-cache: true
 
+      # This must be the same as in the section "Generate rustdoc locally" in the README.md
       - name: Build Rust Documentation
         run: |
           eval $(opam env)

README.md

@@ -60,3 +60,24 @@ The project is organized in the following way:
 ## Contributing
 
 Check [CONTRIBUTING.md](CONTRIBUTING.md) if you are interested in contributing to this project.
+
+## Generate rustdoc locally
+
+An effort is made to have the documentation being self-contained, referring to the mina book for more details when necessary.
+You can build the rust documentation with
+<!-- This must be the same than the content in .github/workflows/gh-page.yml -->
+```
+rustup install nightly
+RUSTDOCFLAGS="--enable-index-page -Zunstable-options" cargo +nightly doc --all --no-deps
+```
+
+You can visualize the documentation by opening the file `target/doc/index.html`.
+
+## CI
+
+<!-- Please update this section if you add more workflows -->
+The CI will build different targets.
+- [Deploy Specifications & Docs to GitHub Pages](.github/workflows/gh-page.yml).
+  When CI passes on master, the documentation built from the rust code will be
+  available [here](https://o1-labs.github.io/proof-systems/rustdoc) and the book
+  will be available [here](https://o1-labs.github.io/proof-systems).

book/Makefile

@@ -49,3 +49,10 @@ all: check
 
 build: check
 	mdbook build
+
+#
+# use `make clean` to clean the generated artefacts
+#
+
+clean:
+	mdbook clean

book/README.md

@@ -9,6 +9,8 @@ $ # install dependencies
 $ make deps
 $ # serve the page locally
 $ make
+$ # clean
+$ make clean
 ```
 
 The specifications in the book are dynamically generated. Refer to the [specifications/](specifications/) directory.

book/macros.txt

@@ -62,4 +62,7 @@
 \enc:{\small \mathsf{Enc}}
 \gid:{\mathsf{gid}}
 \counter:{\mathsf{counter}}
-\prg:{\small \mathsf{PRG}}
+\prg:{\small \mathsf{PRG}}
+
+\plonk:\mathcal{PlonK}
+\plookup:\textsf{Plookup}

book/specifications/README.md

@@ -15,6 +15,11 @@ Install cargo-spec:
 $ cargo install cargo-spec
 ```
 
+You will also need markdownlint:
+```console
+$ npm install markdownlint-cli -g
+```
+
 ## Render
 
 To produce a specification, simply run the following command:

book/specifications/kimchi/Specification.toml

@@ -32,6 +32,7 @@ table_xor = "../../../kimchi/src/circuits/lookup/tables/xor.rs"
 table_12bit = "../../../kimchi/src/circuits/lookup/tables/range_check.rs"
 lookup = "../../../kimchi/src/circuits/lookup/constraints.rs"
 lookup_index = "../../../kimchi/src/circuits/lookup/index.rs"
+runtime_tables = "../../../kimchi/src/circuits/lookup/runtime_tables.rs"
 
 # setup
 constraint_system = "../../../kimchi/src/circuits/constraints.rs"

book/specifications/kimchi/template.md

@@ -213,6 +213,12 @@ Kimchi currently supports two lookup tables:
 
 {sections.table_12bit}
 
+##### Runtime tables
+
+Another type of lookup tables has been suggested in the [Extended Lookup Tables](../kimchi/extended-lookup-tables.md).
+
+{sections.runtime_tables}
+
 #### The Lookup Selectors
 
 **XorSelector**. Performs 4 queries to the XOR lookup table.

book/src/kimchi/final_check.md

@@ -1,6 +1,6 @@
-# Understanding the implementation of the $f(\zeta) = Z_H(\zeta) t(\zeta)$ check 
+# Understanding the implementation of the $f(\zeta) = Z_H(\zeta) t(\zeta)$ check
 
-Unlike the latest version of vanilla PLONK that implements the the final check using a polynomial opening (via Maller's optimization), we implement it manually. (That is to say, Izaak implemented Maller's optimization for 5-wires.)
+Unlike the latest version of vanilla $\plonk$ that implements the final check using a polynomial opening (via Maller's optimization), we implement it manually. (That is to say, Izaak implemented Maller's optimization for 5-wires.)
 
 But the check is not exactly $f(\zeta) = Z_H(\zeta) t(\zeta)$. This note describes how and why the implementation deviates a little.
 
@@ -70,7 +70,7 @@ $$\begin{align}
     & (w[5](\zeta) + \beta \cdot \sigma[5](\zeta) + \gamma) \cdot \\
     & (w[6](\zeta) + \gamma)
     \end{align}$$
-    
+
 So at the end, when we have to check for the identity $f(\zeta) = Z_H(\zeta) t(\zeta)$ we'll actually have to check something like this (I colored the missing parts on the left hand side of the equation):
 
 $$
@@ -151,7 +151,7 @@ $$
 & = \color{darkred}{(1 - z(\zeta))[\frac{(\zeta^n - 1)}{n(\zeta - 1)} \alpha^{PERM1} + \frac{\omega^{n-k}(\zeta^n - 1)}{n(\zeta - \omega^{n-k})} \alpha^{PERM2}]}
 \end{align}
 $$
-    
+
 finally we extract some terms from the lagrange basis:
 
 $$
@@ -182,7 +182,7 @@ $$
 
 with $\alpha^{PERM0} = \alpha^{17}, \alpha^{PERM1} = \alpha^{18}, \alpha^{PERM2} = \alpha^{19}$
 
-Why do we do things this way? Most likely to reduce 
+Why do we do things this way? Most likely to reduce
 
 Also, about the code:
 
@@ -230,7 +230,7 @@ $$
 
 and `bnd` is:
 
-$$bnd(x) = 
+$$bnd(x) =
     a^{PERM1} \cdot \frac{z(x) - 1}{x - 1}
     +
     a^{PERM2} \cdot \frac{z(x) - 1}{x - sid[n-k]}

book/src/kimchi/lookup.md

@@ -1,12 +1,12 @@
-# Plookup in Kimchi
+# $\plookup$ in Kimchi
 
-In 2020, [plookup](https://eprint.iacr.org/2020/315.pdf) showed how to create lookup proofs. Proofs that some witness values are part of a [lookup table](https://en.wikipedia.org/wiki/Lookup_table). Two years later, an independent team published [plonkup](https://eprint.iacr.org/2022/086) showing how to integrate Plookup into Plonk.
+In 2020, [$\plookup$](https://eprint.iacr.org/2020/315.pdf) showed how to create lookup proofs. Proofs that some witness values are part of a [lookup table](https://en.wikipedia.org/wiki/Lookup_table). Two years later, an independent team published [plonkup](https://eprint.iacr.org/2022/086) showing how to integrate $\plookup$ into $\plonk$.
 
-This document specifies how we integrate plookup in kimchi. It assumes that the reader understands the basics behind plookup.
+This document specifies how we integrate $\plookup$ in kimchi. It assumes that the reader understands the basics behind $\plookup$.
 
 ## Overview
 
-We integrate plookup in kimchi with the following differences:
+We integrate $\plookup$ in kimchi with the following differences:
 
 * we snake-ify the sorted table instead of wrapping it around (see later)
 * we allow fixed-ahead-of-time linear combinations of columns of the queries we make
@@ -16,29 +16,40 @@ We integrate plookup in kimchi with the following differences:
 
 The following document explains the protocol in more detail
 
-### Recap on the grand product argument of plookup
+### Recap on the grand product argument of $\plookup$
 
-As per the Plookup paper, the prover will have to compute three vectors:
+As per the $\plookup$ paper, the prover will have to compute three vectors:
 
 * $f$, the (secret) **query vector**, containing the witness values that the prover wants to prove are part of the lookup table.
 * $t$, the (public) **lookup table**.
 * $s$, the (secret) concatenation of $f$ and $t$, sorted by $t$ (where elements are listed in the order they are listed in $t$).
 
-Essentially, plookup proves that all the elements in $f$ are indeed in the lookup table $t$ if and only if the following multisets are equal:
+Essentially, $\plookup$ proves that all the elements in $f$ are indeed in the lookup table $t$ if and only if the following multisets are equal:
 
 * $\{(1+\beta)f, \text{diff}(t)\}$
 * $\text{diff}(\text{sorted}(f, t))$
 
-where $\text{diff}$ is a new set derived by applying a "randomized difference" between every successive pairs of a vector. For example:
+where $\text{diff}$ is a new set derived by applying a "randomized difference"
+between every successive pairs of a vector, and $(f, t)$ is the set union of $f$
+et $t$.
+
+More precisely, for a set $S =
+\{s_{0}, s_{1}, \cdots, s_{n} \}$, $\text{diff}(S)$ is defined as the set
+$\{s_{0} + \beta s_{1}, s_{1} + \beta s_{2}, \cdots, s_{n - 1} + \beta s_{n}\}$.
+
+For example, with:
 
 * $f = \{5, 4, 1, 5\}$
 * $t = \{1, 4, 5\}$
+
+we have:
+* $\text{sorted}(f,t) = \{1, 1, 4, 4, 5, 5, 5\}$
 * $\{\color{blue}{(1+\beta)f}, \color{green}{\text{diff}(t)}\} = \{\color{blue}{(1+\beta)5, (1+\beta)4, (1+\beta)1, (1+\beta)5}, \color{green}{1+\beta 4, 4+\beta 5}\}$
 * $\text{diff}(\text{sorted}(f, t)) = \{1+\beta 1, 1+\beta 4, 4+\beta 4, 4+\beta 5, 5+\beta 5, 5+\beta 5\}$
 
 > Note: This assumes that the lookup table is a single column. You will see in the next section how to address lookup tables with more than one column.
 
-The equality between the multisets can be proved with the permutation argument of plonk, which would look like enforcing constraints on the following accumulator:
+The equality between the multisets can be proved with the permutation argument of $\plonk$, which would look like enforcing constraints on the following accumulator:
 
 * init: $\mathsf{acc}_0 = 1$
 * final: $\mathsf{acc}_n = 1$
@@ -47,13 +58,13 @@ The equality between the multisets can be proved with the permutation argument o
     \mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(\gamma + (1+\beta) f_{i-1}) \cdot (\gamma + t_{i-1} + \beta t_i)}{(\gamma + s_{i-1} + \beta s_{i})(\gamma + s_{n+i-1} + \beta s_{n+i})}
     $$
 
-Note that the plookup paper uses a slightly different equation to make the proof work. It is possible that the proof would work with the above equation, but for simplicity let's just use the equation published in plookup:
+Note that the $\plookup$ paper uses a slightly different equation to make the proof work. It is possible that the proof would work with the above equation, but for simplicity let's just use the equation published in $\plookup$:
 
 $$
 \mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(1+\beta) \cdot (\gamma + f_{i-1}) \cdot (\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})(\gamma(1+\beta) + s_{n+i-1} + \beta s_{n+i})}
 $$
 
-> Note: in plookup $s$ is longer than $n$ ($|s| = |f| + |t|$), and thus it needs to be split into multiple vectors to enforce the constraint at every $i \in [[0;n]]$. This leads to the two terms in the denominator as shown above, so that the degree of $\gamma (1 + \beta)$ is equal in the nominator and denominator.
+> Note: in $\plookup$ $s$ is longer than $n$ ($|s| = |f| + |t|$), and thus it needs to be split into multiple vectors to enforce the constraint at every $i \in [[0;n]]$. This leads to the two terms in the denominator as shown above, so that the degree of $\gamma (1 + \beta)$ is equal in the nominator and denominator.
 
 ### Lookup tables
 
@@ -74,7 +85,7 @@ Note: the $(0, 0, 0)$ **entry** is at the very end on purpose (as it will be use
 
 ### Querying the table
 
-The plookup paper handles a vector of lookups $f$ which we do not have. So the first step is to create such a table from the witness columns (or registers). To do this, we define the following objects:
+The $\plookup$ paper handles a vector of lookups $f$ which we do not have. So the first step is to create such a table from the witness columns (or registers). To do this, we define the following objects:
 
 * a **query** tells us what registers, in what order, and scaled by how much, are part of a query
 * a **query selector** tells us which rows are using the query. It is pretty much the same as a [gate selector]().
@@ -218,15 +229,15 @@ What about the second vector $s$?
 
 ## The sorted vector $s$
 
-We said earlier that in original plonk the size of $s$ is equal to $|s| = |f|+|t|$, where $f$ encodes queries, and $t$ encodes the lookup table.
+We said earlier that in original $\plonk$ the size of $s$ is equal to $|s| = |f|+|t|$, where $f$ encodes queries, and $t$ encodes the lookup table.
 With our multi-query approach, the second vector $s$ is of the size
 
 $$n \cdot |\#\text{queries}| + |\text{lookup\_table}|$$
 
 That is, it contains the $n$ elements of each **query vectors** (the actual values being looked up, after being combined with the joint combinator, that's $4$ per row), as well as the elements of our lookup table (after being combined as well).
 
 Because the vector $s$ is larger than the domain size $n$, it is split into several vectors of size $n$. Specifically, in the plonkup paper, the two halves of $s$, which are then interpolated as $h_1$ and $h_2$.
-The denominator in plonk in the vector form is
+The denominator in $\plonk$ in the vector form is
 $$
 \big(\gamma(1+\beta) + s_{i-1} + \beta s_{i}\big)\big(\gamma(1+\beta)+s_{n+i-1} + \beta s_{n+i}\big)
 $$
@@ -244,11 +255,11 @@ which is equivalent to checking that $h_1(g^{n-1}) = h_2(1)$.
 
 ## The sorted vector $s$ in kimchi
 
-Since this vector is known only by the prover, and is evaluated as part of the protocol, zero-knowledge must be added to the corresponding polynomial (in case of plookup approach, to $h_1(X),h_2(X)$). To do this in kimchi, we use the same technique as with the other prover polynomials: we randomize the last evaluations (or rows, on the domain) of the polynomial.
+Since this vector is known only by the prover, and is evaluated as part of the protocol, zero-knowledge must be added to the corresponding polynomial (in case of $\plookup$ approach, to $h_1(X),h_2(X)$). To do this in kimchi, we use the same technique as with the other prover polynomials: we randomize the last evaluations (or rows, on the domain) of the polynomial.
 
 This means two things for the lookup grand product argument:
 
-1. We cannot use the wrap around trick to make sure that the list is split in two correctly (enforced by $L_{n-1}(h_1(x) - h_2(g \cdot x)) = 0$ which is equivalent to $h_1(g^{n-1}) = h_2(1)$ in the plookup paper)
+1. We cannot use the wrap around trick to make sure that the list is split in two correctly (enforced by $L_{n-1}(h_1(x) - h_2(g \cdot x)) = 0$ which is equivalent to $h_1(g^{n-1}) = h_2(1)$ in the $\plookup$ paper)
 2. We have even less space to store an entire query vector. Which is actually super correct, as the witness also has some zero-knowledge rows at the end that should not be part of the queries anyway.
 
 The first problem can be solved in two ways: