Merge pull request #160 from a16z/book

feat: Init Jolt Book

.github/workflows/deploy-mdbook.yml

@@ -0,0 +1,27 @@
+name: Deploy mdBook to GCS
+
+on:
+  push:
+    branches:
+      - main 
+      - jolt
+
+jobs:
+  deploy:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v2
+
+    - name: Set up Cloud SDK
+      uses: google-github-actions/setup-gcloud@master
+      with:
+        service_account_key: ${{ secrets.GCP_SA_KEY }}
+        project_id: ${{ secrets.GCP_PROJECT_ID }}
+
+    - name: Build mdBook
+      run: |
+        curl -L https://github.com/rust-lang/mdBook/releases/latest/download/mdbook-v0.4.12-x86_64-unknown-linux-gnu.tar.gz | tar xzf -
+        ./mdbook build
+
+    - name: Deploy to Google Cloud Storage
+      run: gsutil -m rsync -d -r ./book gs://$GCS_BUCKET_NAME

book/.gitignore

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

book/README.md

@@ -0,0 +1,6 @@
+# Jolt Book
+The Jolt Book runs on [mdBook](https://rust-lang.github.io/mdBook/). Serve locally with `cd book && mdbook serve`.
+
+## Deps
+- `cargo install mdbook`
+- `cargo install mdbook-katex`: Latex is rendered at compile time with [mdbook-katex](https://github.com/lzanini/mdbook-katex).

book/book.toml

@@ -0,0 +1,9 @@
+[book]
+authors = []
+language = "en"
+multilingual = false
+src = "src"
+title = "JoltBook"
+
+[preprocessor.katex]
+after = ["links"]

book/src/SUMMARY.md

@@ -0,0 +1,17 @@
+# Summary
+
+- [Intro](./intro.md)
+- [Using Jolt](./using_jolt.md)
+- [How it works](./how_it_works.md)
+    - [Lookups](./how/lookups.md)
+    - [Memory Checking](./how/memory-checking.md)
+    - [GKR](./how/gkr.md)
+    - [Jolt](./how/jolt.md)
+- [Background](./background.md)
+    - [Sumcheck](./background/sumcheck.md)
+    - [Multilinear Extensions](./background/multilinear-extensions.md)
+    - [Eq Extension](./background/eq-polynomial.md)
+    - [Batched Polynomial Openings](./background/batched-openings.md)
+- [Dev](./dev/README.md)
+    - [Install](./dev/install.md)
+    - [Tools](./dev/tools.md)

book/src/background.md

@@ -0,0 +1,5 @@
+# Background
+If you're interested in learning the nitty gritty details of SNARKs including questions like 'why', 'is it sound', you should read [Proofs and Args ZK](https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf) by Thaler. If you're simply interested in 'how', this section is for you.
+- [Sumcheck](./background/sumcheck.md)
+- [Multilinear Extensions](./background/multilinear-extensions.md)
+- [EQ Polynomial](./background/eq-polynomial.md)

book/src/background/batched-openings.md

@@ -0,0 +1,4 @@
+# Batched Openings
+At the end of the sumcheck protocol, the verifier must evaluate many multilinear polynomials at a single point. For polynomials which the verifier cannot compute on their own, they depend on the verification of a PCS opening proof provided by the prover. To save on verifier costs, all polynomials opened at the same point can be combined to a single opening proof.
+
+The best reading on the subject can be found in **Section 16.1** of the [Textbook](https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf).

book/src/background/eq-polynomial.md

@@ -0,0 +1,13 @@
+# Eq Extension
+The $\widetilde{eq}$ MLE is useful throughout the protocol
+$$
+\widetilde{eq}(r,x) = \begin{cases} 
+1 & \text{if } r = x \\
+\mathbb{F} & \text{otherwise}
+\end{cases}
+$$
+
+
+$$
+\widetilde{eq}(r,x) = \prod_{i=1}^{\log(m)} (r_i \cdot x_i + (1 - r_i) \cdot (1 - x_i)) \quad \text{where } r, x \in \{0,1\}^{\log(m)}
+$$

book/src/background/multilinear-extensions.md

@@ -0,0 +1,32 @@
+# Multilinear Extensions 
+For any $v$-variate polynomial $g(x_1, ... x_v)$ polynomial, it's multilinear extension $f(x_1, ... x_v)$ is the polynomial which agrees over all $2^v$ points $x \in \{0,1\}^v$: $g(x_1, ... x_v) = \tilde{f}(x_1, ... x_v) \forall x \in \{0,1\}^v$. By the Schwartz-Zippel lemma, if $g$ and $f$ disagree at even a single input, then $g$ and $f$ must disagree *almost everywhere*.
+
+For more precise details please read **Section 3.5 of [Proofs and Args ZK](https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf)**. 
+
+## Engineering
+In practice, MLE's are stored as the vector of evaluations over the $v$-variate boolean hypercube $\{0,1\}^v$. There are two important algorithms over multilinear extensions: single variable binding, evaluation.
+
+### Single Variable Binding
+With a single streaming pass over all $n$ evaluations we can "bind" a single variable of the $v$-variate multilinear extension to a point $r$. This is a critical sub-algorithm in sumcheck. During the binding the number of evaluation points used to represent the MLE gets reduced by a factor of 2:
+- **Before:** $\tilde{f}(x_1, ... x_v): \{0,1\}^v \to \mathbb{F}$
+- **After:** $\tilde{f}(x_1, ... x_{v-1}): \{0,1\}^{v-1} \to \mathbb{F}$
+
+Assuming your MLE is represented as a 1-D vector of $2^v$ evaluations $E$ over the $v$-variate boolean hypercube $\{0,1\}^v$, indexed little-endian
+- $E[1] = \tilde{f}(0,0,0,1)$
+- $E[5] = \tilde{f}(0,1,0,1)$
+- $E[8] = \tilde{f}(1,0,0,0)$
+
+Then we can transform the vector $E \to E'$ representing the transformation from $\tilde{f}(x_1, ... x_v) \to \tilde{f'}(r, x_1, ... x_{v-1})$ by "binding" the evaluations vector to a point $r$.
+
+```python
+let n = 2^v;
+let half = n / 2;
+for i in 0..half {
+    let low = E[i];
+    let high = E[half + i];
+    E[i] = low + r * (high - low);
+}
+```
+
+### Multi Variable Binding
+Another common algorithm is to take the MLE $\tilde{f}(x_1, ... x_v)$ and compute its evaluation at a single $v$-variate point outside the boolean hypercube $x \in \mathbb{F}^v$. This algorithm can be performed in $O(n log(n))$ time by preforming the single variable binding algorithm $log(n)$ times.

book/src/background/sumcheck.md

@@ -0,0 +1,22 @@
+# Sumcheck
+*Adapted from the [Thaler13](https://eprint.iacr.org/2013/351.pdf) exposition. For a detailed introduction to sumcheck see Chapter 4.1 of [the textbook](https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf).*
+
+Suppose we are given a $v$-variate polynomial $g$ defined over a finite field $\mathbb{F}$. The purpose of the sumcheck protocol is to compute the sum:
+
+$$ H := \sum_{b_1 \in \{0,1\}} \sum_{b_2 \in \{0,1\}} \cdots \sum_{b_v \in \{0,1\}} g(b_1, \ldots, b_v). $$
+
+In order to execute the protocol, the verifier needs to be able to evaluate $g(r_1, \ldots, r_v)$ for a randomly chosen vector $(r_1, \ldots, r_v) \in \mathbb{F}^v$ – see the paragraph preceding Proposition 1 below.
+
+The protocol proceeds in $v$ rounds as follows. In the first round, the prover sends a polynomial $g_1(X_1)$, and claims that 
+
+$$ g_1(X_1) = \sum_{x_2, \ldots, x_v \in \{0,1\}^{v-1}} g(X_1, x_2, \ldots, x_v). $$
+
+Observe that if $g_1$ is as claimed, then $H = g_1(0) + g_1(1)$. Also observe that the polynomial $g_1(X_1)$ has degree $\text{deg}_1(g)$, the degree of variable $x_1$ in $g$. Hence $g_1$ can be specified with $\text{deg}_1(g) + 1$ field elements. In our implementation, $P$ will specify $g$ by sending the evaluation of $g$ at each point in the set $\{0,1, \ldots, \text{deg}_1(g)\}$.
+
+Then, in round $j > 1$, $V$ chooses a value $r_{j-1}$ uniformly at random from $\mathbb{F}$ and sends $r_{j-1}$ to $P$. We will often refer to this step by saying that variable $j - 1$ gets bound to value $r_{j-1}$. In return, the prover sends a polynomial $g_j(X_j)$, and claims that
+
+$$ g_j(X_j) = \sum_{(x_{j+1}, \ldots, x_v) \in \{0,1\}^{v-j}} g(r_1, \ldots, r_{j-1}, X_j, x_{j+1}, \ldots, x_v). \quad (1) $$
+
+The verifier compares the two most recent polynomials by checking that $g_{j-1}(r_{j-1}) = g_j(0) + g_j(1)$, and rejecting otherwise. The verifier also rejects if the degree of $g_j$ is too high: each $g_j$ should have degree $\text{deg}_j(g)$, the degree of variable $x_j$ in $g$.
+
+In the final round, the prover has sent $g_v(X_v)$ which is claimed to be $g(r_1, \ldots, r_{v-1}, X_v)$. $V$ now checks that $g_v(r_v) = g(r_1, \ldots, r_v)$ (recall that we assumed $V$ can evaluate $g$ at this point). If this test succeeds, and so do all previous tests, then the verifier accepts, and is convinced that $H = g_1(0) + g_1(1)$.

book/src/dev/README.md

@@ -0,0 +1,4 @@
+# Dev
+For more information on setting up your development environment, see [Installation Guide](./install.md).
+
+For details on the tools used in the Jolt development process, refer to [Development Tools](./tools.md).

book/src/dev/install.md

@@ -0,0 +1,14 @@
+# Development Installation
+## Rust
+- `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh`
+- `rustup target add riscv32i-unknown-none-elf`
+
+## Circom
+Install from source:
+- `git clone https://github.com/iden3/circom.git`
+- `cd circom && cargo build --release`
+- `cargo install --path circom`
+
+
+## mdBook
+`cargo install mdbook`

book/src/dev/tools.md

@@ -0,0 +1,12 @@
+# Development Tools
+## Tracing
+Jolt is instrumented using [tokio-rs/tracing](https://github.com/tokio-rs/tracing). These traces can be displayed using the `--format chrome` flag, for example:
+`cargo run -p jolt-core --release -- trace --name sha3 --format chrome`
+
+After tracing, files can be found in the workspace root with a name `trace-<timestamp>.json`. Load these traces into `chrome://tracing` or `https://ui.perfetto.dev/`.
+
+![Tracing in Jolt](../imgs/tracing.png)
+
+
+## Objdump
+Debugging the emulator / tracer can be hard. Use `riscv64-unknown-elf-objdump` to compare the actual ELF to the `.bytecode` / `.jolttrace` files.

book/src/how/gkr.md

@@ -0,0 +1,35 @@
+# GKR
+GKR is a SNARK protocol for binary trees of multiplication / addition gates. The standard form allows combinations of both using a wiring predicate $\tilde{V}_i$, and two additional MLEs $\tilde{add}_i$ and $\tilde{mult}_i$. 
+
+$\widetilde{V}_i(j)$ evaluates to the value of he circuit at the $i$-th layer in the $j$-th gate. For example $\tilde{V}_1(0)$ corresponds to the output gate.
+
+$\widetilde{add}_i(j)$ evaluates to 1 if the $j$-th gate of the $i$-th layer is an addition gate.
+
+$\widetilde{mult}_i(j)$ evaluates to 1 if the $j$-th gate of the $i$-th layer is a multiplication gate.
+
+The sumcheck protocol is applied to the following:
+$$
+\tilde{V}_i(z) = \sum_{(p,\omega_1,\omega_2) \in \{0,1\}^{s_i+2s_{i+1}}} f_{i,z}(p,\omega_1,\omega_2),
+$$
+
+where
+
+$$
+f_i(z, p, \omega_1, \omega_2) = \beta_{s_i}(z, p) \cdot \tilde{add}_i(p, \omega_1, \omega_2)(\tilde{V}_{i+1}(\omega_1) + \tilde{V}_{i+1}(\omega_2)) + \tilde{mult}_i(p, \omega_1, \omega_2)\tilde{V}_{i+1}(\omega_1) \cdot \tilde{V}_{i+1}(\omega_2)
+$$
+$$
+\beta_{s_i}(z, p) = \prod_{j=1}^{s_i} ((1-z_j)(1-p_j) + z_j p_j).
+$$
+
+
+Lasso and Jolt implement the [Thaler13](https://eprint.iacr.org/2013/351.pdf) version of GKR which is optimized for the far simpler case of a binary tree of multiplication gates. This simplifies each sumcheck to:
+$$
+\tilde{V}_i(z) = \sum_{p \in \{0,1\}^{s_i}} g^{(i)}_z(p),
+$$
+
+where
+
+$$
+g^{(i)}_z(p) = \beta_{s_i}(z, p) \cdot \tilde{V}_{i+1}(p,0) \cdot \tilde{V}_{i+1}(p,1)
+$$
+GKR is utilized in [memory-checking](./memory-checking.html) for the multi-set permutation check.

book/src/how/jolt.md

@@ -0,0 +1,50 @@
+# Jolt
+*Note: This section is still under construction. Expect more details in the future.*
+
+`TODO`
+- 3 phases of memory checking + primary sumcheck + r1cs
+- subtable flags -> instruction flags
+- R1CS checks
+
+## Instruction Collation
+The "primary sumcheck" collation when generalized from Lasso -> Jolt looks as follows for a trace of length $m$ and a VM with $f$ unique instructions.
+
+$$
+\sum_{x \in \{0,1\}^{log(m)}} [\widetilde{eq}(r,x) \cdot \sum_{f \in \{0,1\}^{log(F)}} {\widetilde{flags_f}(x) \cdot g_f(\text{terms}_f(x))]}
+$$
+
+$\widetilde{flags_f}(x) = 1$ if the $f$-th instruction is used during the $x$-th step of the trace when. $x \in \{0,1\}^{log(m)}$ 
+
+$g_f(...)$ is the collation function used by the $f$-th instruction.
+
+$terms_f(x) = [E_1(x), ... E_\alpha(x)]$ where $\alpha$ is the number of independent memories used by an instruction. For simple instructions like the EQ instruction, $\alpha = C$, $terms_f(x) = [E_1(x), ... E_C(x)]$. More complicated instructions such LT might have $terms_f(x) = [E_{eq}(x), E_{lt1}(x), E_{lt2}(x)]$. The exact layout is dependent on the number of subtables required by the decomposition of the instruction. The mappings can be found in the `JoltInstruction::subtable` method implementations.
+
+### Metal Model
+For a given $r = x \in \{0,1\}^{log(m)}$ (think integer index of the instruction within the trace), $\widetilde{eq} = 0$ for all but one term of the outer sum. Similarly all $\widetilde{flags_f}(x) = 0$ for all but one term of the inner sum. Leaving just the collation function of a single instruction, evaluting to the collated lookup output of the single instruction. In reality $r$ is a random point $r \in \mathbb{F}^{log(m)}$ selected by the verifier over the course of the protocol. The evaluation point provides a distance amplified encoding of the entire trace of instructions.
+
+
+To illustrate more concretely imagine a 2 instruction VM for LT and EQ instructions with $C=1$.
+
+$$
+\sum_{x \in \{0,1\}^{\log_2(m)}}{\widetilde{eq}(r,x) \cdot [ \widetilde{flags}_{LT}(x) \cdot g_{LT}(E_{LT}(x)) + \widetilde{flags}_{EQ}(x) \cdot g_{EQ}(E_{EQ}(x))]}
+$$
+
+
+## Subtable Flags
+`TODO`
+- We then use memory checking to determine that each of the memories $E_i$ is well formed
+- At a given step of the CPU only a single instruction will be used, that means that only that instruction's subtables will be used. For the rest of the memories we insert a no_op with (a, v) = 0. But we still have to increment the timestamp associated with (a, v) = 0 to ensure that offline memory checking works. In order to make the GKR trees cheaper to comptue and sumcheck we'll add a single additional layer to the GKR tree. During this layer we'll "toggle" each of the GKR leaves to "1" in the case that it is an unused step of the CPU. This will make the binary tree of multiplication gates cheaper. We'll toggle based on a new flags polynomial called $subtable-flags_f$ which is the sum of all of the $instruction-flags_f$ used in the instruction collation above.
+- The function to compute each of the leaves becomes $leaf[i] = \text{subtable-flags}[i] \cdot \text{fingerprint}[i] + (1 - \text{subtable-flags}[i])$
+
+
+## Read Write Memory (VM RAM)
+
+In contrast to our standard procedures for offline memory checking, the registers and RAM within this context are considered *writable* memory. This distinction introduces additional verification requirements:
+
+- The multiset equality typically expressed as $I \cdot W = R \cdot F$ is not adequate for ensuring the accuracy of read values. It is essential to also verify that each read operation retrieves a value that was written in a previous step.
+
+- To formalize this, we assert that the timestamp of each read operation, denoted as $\text{read\_timestamp}$, must not exceed the global timestamp at that particular step. The global timestamp is a monotonically increasing sequence starting from 0 and ending at $\text{TRACE\_LENGTH}$.
+
+- The verification of $\text{read\_timestamp} \leq \text{global\_timestamp}$ is equivalent to confirming that $\text{read\_timestamp}$ falls within the range $[0, \text{TRACE\_LENGTH}]$ and that the difference $(\text{global\_timestamp} - \text{read\_timestamp})$ is also within the same range.
+
+- The process of ensuring that both $\text{read\_timestamp}$ and $(\text{global\_timestamp} - \text{read\_timestamp})$ lie within the specified range is known as range-checking. This is the procedure implemented in `timestamp_range_check.rs`.

book/src/how/lookups.md

@@ -0,0 +1,8 @@
+# Lookups
+Lasso is a lookup argument. Lookup arguments allow the prover to convince the verifier that a set of values $Q$ is a subset of a lookup table $T$. Lasso is a special lookup argument with highly desirable asymptotic costs largely correlated to the number of queries $Q$ rather than the length of of the table $T$.
+
+A conversational background on lookups can be found [here](https://a16zcrypto.com/posts/article/building-on-lasso-and-jolt/). In short: Lookups are great for zkVMs as they allow constant cost / developer complexity for the prover algorithm per VM instruction.
+
+## Lasso
+A detailed engineering overview of Lasso can be found [here](https://www.youtube.com/watch?v=iDcXj9Vx3zY).
+![Lasso SVG](../imgs/lasso.svg)

book/src/how/memory-checking.md

@@ -0,0 +1,50 @@
+# Offline Memory Checking
+Offline memory checking is a method that enables a prover to demonstrate to a verifier that a read/write memory was used correctly. In such a memory system, values $v$ can be written to addresses $a$ and subsequently retrieved. This technique allows the verifier to efficiently confirm that the prover adhered to the memory's rules.
+
+Jolt utilizes offline memory checking in the Bytecode prover, Lookup prover, and RAM prover.
+
+## Initialization Algorithm
+### `TODO`: 
+- Initialize four timestamp counters
+- Implicitly assume a read operation before each write
+
+## Multiset Check
+Define $read$ and $write$ as subsets, and $init$ and $final$ as subsets:
+$$
+read, write \subseteq \{(a_i, v_i, t_i) \,|\, i \in [0, m]\}
+$$
+$$
+init, final \subseteq \{(a_i, v_i, t_i) \,|\, i \in [0, M]\}
+$$
+Here, $a_i$, $v_i$, and $t_i$ represent the address, value, and timestamp respectively, with $m$ being the total number of memory operations and $M$ the size of the RAM.
+
+The verifier checks that the combination of $read$ and $final$ matches $write$ and $init$, disregarding the sequence of elements, known as a permutation check:
+$$
+read \cup final = write \cup init
+$$
+Jolt conducts this check using a homomorphic hash function applied to each set:
+$$
+H(read) = \prod_{(a_i, v_i, t_i) \in read} h(a_i, v_i, t_i)
+$$
+$$
+H(write) = \prod_{(a_i, v_i, t_i) \in write} h(a_i, v_i, t_i)
+$$
+$$
+H(init) = \prod_{(a_j, v_j, t_j) \in init} h(a_j, v_j, t_j)
+$$
+$$
+H(final) = \prod_{(a_j, v_j, t_j) \in final} h(a_j, v_j, t_j)
+$$
+The hash function $h$ is defined as:
+$$
+h_{\gamma, \tau}(a, v, t) = a \cdot \gamma^2 + v \cdot \gamma + t - \tau
+$$
+
+This multiset hashing process is represented by a binary tree of multiplication gates and is computed using an [optimized GKR protocol](https://eprint.iacr.org/2013/351.pdf).
+
+## References
+- [Original Paper on Memory Correctness](https://www.researchgate.net/publication/226386605_Checking_the_correctness_of_memories/link/0c960526fe9ab32634000000/download?_tp=eyJjb250ZXh0Ijp7ImZpcnN0UGFnZSI6InB1YmxpY2F0aW9uIiwicGFnZSI6InB1YmxpY2F0aW9uIn19)
+- [Spice Protocol](https://eprint.iacr.org/2018/907.pdf)
+- [Spartan Protocol](https://eprint.iacr.org/2019/550.pdf)
+- [Lasso Protocol](https://people.cs.georgetown.edu/jthaler/Lasso-paper.pdf)
+- [Thaler13 Protocol](https://eprint.iacr.org/2013/351.pdf)

book/src/how_it_works.md

@@ -0,0 +1,5 @@
+# How it works
+1. [Lookups](./how/lookups.md)
+2. [Memory Checking](./how/memory-checking.md)
+3. [GKR](./how/gkr.md)
+4. [Jolt](./jolt.md)