book: Add summary and succinct description of the Halo 2 protocol

book/src/design/proving-system.md

@@ -1 +1,70 @@
 # Proving system
+
+The Halo 2 proving system can be broken down into five stages:
+
+1. Commit to polynomials encoding the main components of the circuit:
+   - Cell assignments.
+   - Permuted values for each lookup argument.
+   - Equality constraint permutations.
+   - Products for each lookup argument.
+2. Construct the vanishing argument to constrain all circuit relations to zero:
+   - Custom gates.
+   - Lookup argument rules.
+   - Equality constraint permutation rules.
+3. Evaluate the above polynomials at all necessary points:
+   - All relative rotations used by custom gates across all columns.
+   - Vanishing argument pieces.
+4. Construct the multipoint opening argument to check that all evaluations are consistent
+   with their respective commitments.
+5. Run the inner product argument to create a polynomial commitment opening proof for the
+   multipoint opening argument polynomial.
+
+These stages are presented in turn across this section of the book.
+
+## Example
+
+To aid our explanations, we will at times refer to the following example constraint
+system:
+
+- Four advice columns $a, b, c, d$.
+- One fixed column $f$.
+- Three custom gates:
+  - $a \cdot b \cdot c_{-1} - d = 0$
+  - $f_{-1}(c) = 0$
+  - $f(d \cdot a) = 0$
+
+## tl;dr
+
+The table below provides a (probably too) succinct description of the Halo 2 protocol.
+This description will likely be replaced by the Halo 2 paper and security proof, but for
+now serves as a summary of the following sub-sections.
+
+| Prover                                                                      |         | Verifier                           |
+| --------------------------------------------------------------------------- | ------- | ---------------------------------- |
+|                                                                             | $\larr$ | $t(X) = (X^n - 1)$                 |
+|                                                                             | $\larr$ | $F = [F_0, F_1, \dots, F_{m - 1}]$ |
+| $\mathbf{A} = [A_0, A_1, \dots, A_{m - 1}]$                                 | $\rarr$ |                                    |
+|                                                                             | $\larr$ | $\theta$                           |
+| $\mathbf{L} = [(A'_0, S'_0), \dots, (A'_{m - 1}, S'_{m - 1})]$              | $\rarr$ |                                    |
+|                                                                             | $\larr$ | $\beta, \gamma$                    |
+| $\mathbf{P} = [P_0, P_1, \dots, P_{m - 1}]$                                 | $\rarr$ |                                    |
+|                                                                             | $\larr$ | $y$                                |
+| $h(X) = \frac{\text{gate}_0(X) + \dots + y^i \cdot \text{gate}_i(X)}{t(X)}$ |         |                                    |
+| $h(X) = h_0(X) + \dots + X^{n(d-1)} h_{d-1}(X)$                             |         |                                    |
+| $\mathbf{H} = [H_0, H_1, \dots, H_{d-1}]$                                   | $\rarr$ |                                    |
+|                                                                             | $\larr$ | $x$                                |
+| $evals = [A_0(x), \dots, H_{d - 1}(x)]$                                     | $\rarr$ |                                    |
+|                                                                             |         | Checks $h(x)$                      |
+|                                                                             | $\larr$ | $x_1, x_2$                         |
+| Constructs $h'(X)$ multipoint opening poly                                  |         |                                    |
+| $U = \text{Commit}(h'(X))$                                                  | $\rarr$ |                                    |
+|                                                                             | $\larr$ | $x_3$                              |
+| $q_\text{evals} = [Q_0(x_3), Q_1(x_3), \dots]$                              | $\rarr$ |                                    |
+| $u_\text{eval} = U(x_3)$                                                    | $\rarr$ |                                    |
+|                                                                             | $\larr$ | $x_4$                              |
+
+Then the prover and verifier perform:
+
+$$\text{InnerProduct}(\text{LinCom}(Q, U, x_4), x_3, \text{LinCom}(q_\text{evals}, u_\text{eval}, x_4)).$$
+
+> TODO: Write up protocol components that provide zero-knowledge.