Merge pull request #177 from zcash/book-proving-system

[book] Fill out design section about proving system

book/src/SUMMARY.md

@@ -14,9 +14,12 @@
   - [Tips and tricks](user/tips-and-tricks.md)
 - [Design](design.md)
   - [Proving system](design/proving-system.md)
-    - [Multipoint opening argument](design/proving-system/multipoint-opening.md)
+    - [Lookup argument](design/proving-system/lookup.md)
     - [Permutation argument](design/proving-system/permutation.md)
-    - [Lookup argument](design/proving-system/lookup-argument.md)
+    - [Circuit commitments](design/proving-system/circuit-commitments.md)
+    - [Vanishing argument](design/proving-system/vanishing.md)
+    - [Multipoint opening argument](design/proving-system/multipoint-opening.md)
+    - [Inner product argument](design/proving-system/inner-product.md)
     - [Comparison to other work](design/proving-system/comparison.md)
   - [Implementation](design/implementation.md)
   - [Gadgets](design/gadgets.md)

book/src/design/proving-system.md

@@ -1 +1,74 @@
 # 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 and products for each lookup argument.
+   - Equality constraint permutations.
+2. Construct the vanishing argument to constrain all circuit relations to zero:
+   - Standard and 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} \cdot c = 0$
+  - $f \cdot 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$ |                                    |
+| $\mathbf{Z} = [Z_0, Z_1, \dots, Z_{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$                              |
+| $\mathbf{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:
+
+- Construct $\text{finalPoly}(X)$ as a linear combination of $\mathbf{Q}$ and $U$ using
+  powers of $x_4$;
+- Construct $\text{finalPolyEval}$ as the equivalent linear combination of
+  $\mathbf{q}_\text{evals}$ and $u_\text{eval}$; and
+- Perform $\text{InnerProduct}(\text{finalPoly}(X), x_3, \text{finalPolyEval}).$
+
+> TODO: Write up protocol components that provide zero-knowledge.

book/src/design/proving-system/circuit-commitments.md

@@ -0,0 +1,84 @@
+# Circuit commitments
+
+## Committing to the circuit assignments
+
+At the start of proof creation, the prover has a table of cell assignments that it claims
+satisfy the constraint system. The table has $n = 2^k$ rows, and is broken into advice,
+auxiliary, and fixed columns. We define $F_{i,j}$ as the assignment in the $j$th row of
+the $i$th fixed column. Without loss of generality, we'll similarly define $A_{i,j}$ to
+represent the advice and auxiliary assignments.
+
+> We separate fixed columns here because they are provided by the verifier, whereas the
+> advice and auxiliary columns are provided by the prover. In practice, the commitments to
+> auxiliary and fixed columns are computed by both the prover and verifier, and only the
+> advice commitments are stored in the proof.
+
+To commit to these assignments, we construct Lagrange polynomials of degree $n - 1$ for
+each column, over an evaluation domain of size $n$ (where $\omega$ is the $n$th primitive
+root of unity):
+
+- $a_i(X)$ interpolates such that $a_i(\omega^j) = A_{i,j}$.
+- $f_i(X)$ interpolates such that $f_i(\omega^j) = F_{i,j}$.
+
+We then create a blinding commitment to the polynomial for each column:
+
+$$\mathbf{A} = [\text{Commit}(a_0(X)), \dots, \text{Commit}(a_i(X))]$$
+$$\mathbf{F} = [\text{Commit}(f_0(X)), \dots, \text{Commit}(f_i(X))]$$
+
+$\mathbf{F}$ is constructed as part of key generation, using a blinding factor of $1$.
+$\mathbf{A}$ is constructed by the prover and sent to the verifier.
+
+## Committing to the lookup permutations
+
+The verifier starts by sampling $\theta$, which is used to keep individual columns within
+lookups independent. Then, the prover commits to the permutations for each lookup as
+follows:
+
+- Given a lookup with input column polynomials $[A_0(X), \dots, A_{m-1}(X)]$ and table
+  column polynomials $[S_0(X), \dots, S_{m-1}]$, the prover constructs two compressed
+  polynomials
+
+  $$A_\text{compressed}(X) = \theta^{m-1} A_0(X) + \theta^{m-2} A_1(X) + \dots + \theta A_{m-2}(X) + A_{m-1}(X)$$
+  $$S_\text{compressed}(X) = \theta^{m-1} S_0(X) + \theta^{m-2} S_1(X) + \dots + \theta S_{m-2}(X) + S_{m-1}(X)$$
+
+- The prover then permutes $A_\text{compressed}(X)$ and $S_\text{compressed}(X)$ according
+  to the [rules of the lookup argument](lookup.md), obtaining $A'(X)$ and $S'(X)$.
+
+Finally, the prover creates blinding commitments for all of the lookups
+
+$$\mathbf{L} = \left[ (\text{Commit}(A'(X))), \text{Commit}(S'(X))), \dots \right]$$
+
+and sends them to the verifier.
+
+## Committing to the equality constraint permutations
+
+- The verifier samples $\beta$ and $\gamma$.
+- For each permutation, the prover constructs the corresponding
+  [constraint polynomial](permutation.md#argument-specification).
+- The prover creates blinding commitments to every constraint polynomial
+
+  $$\mathbf{P} = \left[\text{Commit}(p(X))), \dots \right]$$
+
+  and sends them to the verifier.
+
+## Committing to the lookup permutation product columns
+
+In addition to committing to the individual permuted lookups, the prover needs to commit
+to the permutation product column
+
+$$Z(X) = \frac{(A_\text{compressed}(X) + \beta)(S_\text{compressed}(X) + \gamma)}{(A'(X) + \beta)(S'(X) + \gamma)}$$
+
+$\beta$ and $\gamma$ are used to combine the permutation arguments for $A'(X)$ and $S'(X)$
+while keeping them independent. We can reuse $\beta$ and $\gamma$ from the equality
+constraint permutation here because they serve the same purpose in both places, and we
+aren't trying to combine the lookup and equality constraint permutation arguments. The
+important thing here is that the verifier samples $\beta$ and $\gamma$ after the prover
+has created $\mathbf{A}$, $\mathbf{F}$, and $\mathbf{L}$ (and thus commited to all the
+cell values used in lookup columns, as well as $A'(X)$ and $S'(X)$ for each lookup).
+
+As before, the prover creates blinding commitments to the permutation product column for
+every lookup
+
+$$\mathbf{Z} = \left[\text{Commit}(Z(X))), \dots \right]$$
+
+and sends them to the verifier.

book/src/design/proving-system/inner-product.md

@@ -0,0 +1,11 @@
+# Inner product argument
+
+Halo 2 uses a polynomial commitment scheme for which we can create polynomial commitment
+opening proofs, based around the Inner Product Argument.
+
+> TODO: Explain Halo 2's variant of the IPA.
+>
+> It is very similar to $\text{PC}_\text{DL}.\text{Open}$ from Appendix A.2 of [BCMS20].
+> See [this comparison](comparison.md#bcms20-appendix-a2) for details.
+>
+> [BCMS20]: https://eprint.iacr.org/2020/499

book/src/design/proving-system/multipoint-opening.md

@@ -6,8 +6,11 @@ were queried at both points $x$ and $\omega x$. (Here, $\omega$ is the primitive
 root of unity in the multiplicative subgroup over which we constructed the
 polynomials).
 
-We can group the commitments in terms of the sets of points at which they were
+To open these commitments, we could create a polynomial $Q$ for each point that we queried
-queried:
+at (corresponding to each relative rotation used in the circuit). But this would not be
+efficient in the circuit; for example, $c(X)$ would appear in multiple polynomials.
+
+Instead, we can group the commitments by the sets of points at which they were queried:
 $$
 \begin{array}{cccc}
 &\{x\}&     &\{x, \omega x\}& \\
@@ -16,65 +19,75 @@ $$
 \end{array}
 $$
 
+For each of these groups, we combine them into a polynomial set, and create a single $Q$
+for that set, which we open at each rotation.
+
+## Optimisation steps
+
+The multipoint opening optimisation takes as input:
+
+- A random $x$ sampled by the verifier, at which we evaluate $a(X), b(X), c(X), d(X)$.
+- Evaluations of each polynomial at each point of interest, provided by the prover:
+  $a(x), b(x), c(x), d(x), c(\omega x), d(\omega x)$
+
+These are the outputs of the [vanishing argument](vanishing.md#evaluating-the-polynomials).
+
 The multipoint opening optimisation proceeds as such:
 
-1. Sample random $x_3$, at which we evaluate $a(X), b(X), c(X), d(X)$.
+1. Sample random $x_1$, to keep $a, b, c, d$ linearly independent.
-2. The prover provides evaluations of each polynomial at each point of interest:
+2. Accumulate polynomials and their corresponding evaluations according
-   $a(x_3), b(x_3), c(x_3), d(x_3), c(\omega x_3), d(\omega x_3)$
-3. Sample random $x_4$, to keep $a, b, c, d$ linearly independent.
-4. Accumulate polynomials and their corresponding evaluations according
    to the point set at which they were queried:
     `q_polys`:
     $$
     \begin{array}{rccl}
-    q_1(X) &=& a(X) &+& x_4 b(X) \\
+    q_1(X) &=& a(X) &+& x_1 b(X) \\
-    q_2(X) &=& c(X) &+& x_4 d(X)
+    q_2(X) &=& c(X) &+& x_1 d(X)
     \end{array}
     $$
     `q_eval_sets`:
     ```math
             [
-                [a(x_3) + x_4 b(x_3)],
+                [a(x) + x_1 b(x)],
                 [
-                    c(x_3) + x_4 d(x_3),
+                    c(x) + x_1 d(x),
-                    c(\omega x_3) + x_4 d(\omega x_3)
+                    c(\omega x) + x_1 d(\omega x)
                 ]
             ]
     ```
     NB: `q_eval_sets` is a vector of sets of evaluations, where the outer vector
     goes over the point sets, and the inner vector goes over the points in each set.
-5. Interpolate each set of values in `q_eval_sets`:
+3. Interpolate each set of values in `q_eval_sets`:
     `r_polys`:
     $$
     \begin{array}{cccc}
     r_1(X) s.t.&&& \\
-        &r_1(x_3) &=& a(x_3) + x_4 b(x_3) \\
+        &r_1(x) &=& a(x) + x_1 b(x) \\
     r_2(X) s.t.&&& \\
-        &r_2(x_3) &=& c(x_3) + x_4 d(x_3) \\
+        &r_2(x) &=& c(x) + x_1 d(x) \\
-        &r_2(\omega x_3) &=& c(\omega x_3) + x_4 d(\omega x_3) \\
+        &r_2(\omega x) &=& c(\omega x) + x_1 d(\omega x) \\
     \end{array}
     $$
-6. Construct `f_polys` which check the correctness of `q_polys`:
+4. Construct `f_polys` which check the correctness of `q_polys`:
     `f_polys`
     $$
     \begin{array}{rcl}
-    f_1(X) &=& \frac{ q_1(X) - r_1(X)}{X - x_3} \\
+    f_1(X) &=& \frac{ q_1(X) - r_1(X)}{X - x} \\
-    f_2(X) &=& \frac{ q_2(X) - r_2(X)}{(X - x_3)(X - \omega x_3)} \\
+    f_2(X) &=& \frac{ q_2(X) - r_2(X)}{(X - x)(X - \omega x)} \\
     \end{array}
     $$
 
-    If $q_1(x_3) = r_1(x_3)$, then $f_1(X)$ should be a polynomial.
+    If $q_1(x) = r_1(x)$, then $f_1(X)$ should be a polynomial.
-    If $q_2(x_3) = r_2(x_3)$ and $q_2(\omega x_3) = r_2(\omega x_3)$
+    If $q_2(x) = r_2(x)$ and $q_2(\omega x) = r_2(\omega x)$
     then $f_2(X)$ should be a polynomial.
-7. Sample random $x_5$ to keep the `f_polys` linearly independent.
+5. Sample random $x_2$ to keep the `f_polys` linearly independent.
-8. Construct $f(X) = f_1(X) + x_5 f_2(X)$.
+6. Construct $f(X) = f_1(X) + x_2 f_2(X)$.
-9. Sample random $x_6$, at which we evaluate $f(X)$:
+7.  Sample random $x_3$, at which we evaluate $f(X)$:
     $$
     \begin{array}{rcccl}
-    f(x_6) &=& f_1(x_6) &+& x_5 f_2(x_6) \\
+    f(x_3) &=& f_1(x_3) &+& x_2 f_2(x_3) \\
-           &=& \frac{q_1(x_6) - r_1(x_6)}{x_6 - x_3} &+& x_5\frac{q_2(x_6) - r_2(x_6)}{(x_6 - x_3)(x_6 - \omega x_3)}
+           &=& \frac{q_1(x_3) - r_1(x_3)}{x_3 - x} &+& x_2\frac{q_2(x_3) - r_2(x_3)}{(x_3 - x)(x_3 - \omega x)}
     \end{array}
     $$
-10. Sample random $x_7$ to keep $f(X)$ and `q_polys` linearly independent.
+8.  Sample random $x_4$ to keep $f(X)$ and `q_polys` linearly independent.
-11. Construct `final_poly`, $$final\_poly(X) = f(X) + x_7 q_1(X) + x_7^2 q_2(X),$$
+9.  Construct `final_poly`, $$final\_poly(X) = f(X) + x_4 q_1(X) + x_4^2 q_2(X),$$
     which is the polynomial we commit to in the inner product argument.

book/src/design/proving-system/permutation.md

@@ -123,4 +123,12 @@ correct $(a\ b\ c\ d)$.
 
 ## Argument specification
 
-TODO: Document what we do with the permutation once we have it.
+Given a permutation between advice columns $[p_0(X), \dots, p_j(X)]$, the permutation is
+constrained by the rule
+
+$$p(X) = \prod_0^j \frac{p_j(X) + \beta \delta^j X + \gamma}{p_j(X) + \beta s_j(X) + \gamma}$$
+
+where:
+- $p_j(X)$ is the $j$th advice column in this permutation.
+- $s_j(X)$ is a pseudo-column containing the permutation of $p_j(X)$.
+- $\delta$ is a $t$ root of unity, where $t \cdot 2^s + 1 = p$ with t odd.

book/src/design/proving-system/vanishing.md

@@ -0,0 +1,79 @@
+# Vanishing argument
+
+Having committed to the circuit assignments, the prover now needs to demonstrate that the
+various circuit relations are satisfied:
+
+- The custom gates, represented by polynomials $\text{gate}_i(X)$.
+- The rules of the lookup arguments.
+- The rules of the equality constraint permutations.
+
+Each of these relations is represented as a polynomial of degree $d$ (the maximum degree
+of any of the relations) with respect to the circuit columns. Given that the degree of the
+assignment polynomials for each column is $n - 1$, the relation polynomials have degree
+$d(n - 1)$ with respect to $X$.
+
+> In our [example](../proving-system.md#example), these would be the gate polynomials, of
+> degree $3n - 3$:
+>
+> - $\text{gate}_0(X) = a_0(X) \cdot a_1(X) \cdot a_2(X \omega^{-1}) - a_3(X)$
+> - $\text{gate}_1(X) = f_0(X \omega^{-1}) \cdot a_2(X)$
+> - $\text{gate}_2(X) = f_0(X) \cdot a_3(X) \cdot a_0(X)$
+
+A relation is satisfied if its polynomial is equal to zero. One way to demonstrate this is
+to divide each polynomial relation by the vanishing polynomial $t(X) = (X^n - 1)$, which
+is the lowest-degree monomial that has roots at every $\omega^i$. If relation's polynomial
+is perfectly divisible by $t(X)$, it is equal to zero over the domain (as desired).
+
+This simple construction would require a polynomial commitment per relation. Instead, we
+commit to all of the circuit relations simultaneously: the verifier samples $y$, and then
+the prover constructs the quotient polynomial
+
+$$h(X) = \frac{\text{gate}_0(X) + y \cdot \text{gate}_1(X) + \dots + y^i \cdot \text{gate}_i(X) + \dots}{t(X)},$$
+
+where the numerator is a random (the prover commits to the cell assignments before the
+verifier samples $y$) linear combination of the circuit relations.
+
+- If the numerator polynomial (in formal indeterminate $X$) is perfectly divisible by
+  $t(X)$, then with high probability all relations are satisfied.
+- Conversely, if at least one relation is not satisfied, then with high probability
+  $h(x) \cdot t(x)$ will not equal the evaluation of the numerator at $x$. In this case,
+  the numerator polynomial would not be perfectly divisible by $t(X)$.
+
+## Committing to $h(X)$
+
+$h(X)$ has degree $(d - 1)n - d$ (because the divisor $t(X)$ has degree $n$). However, the
+polynomial commitment scheme we use for Halo 2 only supports committing to polynomials of
+degree $n - 1$ (which is the maximum degree that the rest of the protocol needs to commit
+to). Instead of increasing the cost of the polynomial commitment scheme, the prover split
+$h(X)$ into pieces of degree $n - 1$
+
+$$h_0(X) + X^n h_1(X) + \dots + X^{n(d-1)} h_{d-1}(X),$$
+
+and produces blinding commitments to each piece
+
+$$\mathbf{H} = [\text{Commit}(h_0(X)), \text{Commit}(h_1(X)), \dots, \text{Commit}(h_{d-1}(X))].$$
+
+## Evaluating the polynomials
+
+At this point, all properties of the circuit have been committed to. The verifier now
+wants to see if the prover committed to the correct $h(X)$ polynomial. The verifier
+samples $x$, and the prover produces the purported evaluations of the various polynomials
+at $x$, for all the relative offsets used in the circuit, as well as $h(X)$.
+
+> In our [example](../proving-system.md#example), this would be:
+>
+> - $a_0(x)$
+> - $a_1(x)$
+> - $a_2(x)$, $a_2(x \omega^{-1})$
+> - $a_3(x)$
+> - $f_0(x)$, $f_0(x \omega^{-1})$
+> - $h_0(x)$, ..., $h_{d-1}(x)$
+
+The verifier checks that these evaluations satisfy the form of $h(X)$:
+
+$$\frac{\text{gate}_0(x) + \dots + y^i \cdot \text{gate}_i(x) + \dots}{t(x)} = h_0(x) + \dots + x^{n(d-1)} h_{d-1}(x)$$
+
+Now content that the evaluations collectively satisfy the gate constraints, the verifier
+needs to check that the evaluations themselves are consistent with the original
+[circuit commitments](circuit-commitments.md), as well as $\mathbf{H}$. To implement this
+efficiently, we use a [multipoint opening argument](multipoint-opening.md).