From 4aceada21a2fef46928fc4ed7accdc994a52fbbe Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Wed, 10 Feb 2021 13:06:22 +0000
Subject: [PATCH 01/17] book: Re-order "Proving system" sub-sections

---
 book/src/SUMMARY.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index e6eb615..ecfd665 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -14,9 +14,9 @@
   - [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)
-    - [Permutation argument](design/proving-system/permutation.md)
     - [Lookup argument](design/proving-system/lookup-argument.md)
+    - [Permutation argument](design/proving-system/permutation.md)
+    - [Multipoint opening argument](design/proving-system/multipoint-opening.md)
     - [Comparison to other work](design/proving-system/comparison.md)
   - [Implementation](design/implementation.md)
   - [Gadgets](design/gadgets.md)

From e666f8b9664e3fa3200e949130713d9276c2ebb5 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Thu, 11 Feb 2021 02:43:56 +0000
Subject: [PATCH 02/17] book: Add summary and succinct description of the Halo
 2 protocol

---
 book/src/design/proving-system.md | 69 +++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)

diff --git a/book/src/design/proving-system.md b/book/src/design/proving-system.md
index adad839..566f2cf 100644
--- a/book/src/design/proving-system.md
+++ b/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.

From 9e9a92a91214f7a53638a7e8be9d4963ffa9c568 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Thu, 11 Feb 2021 03:08:54 +0000
Subject: [PATCH 03/17] book: Add section about circuit commitments

---
 book/src/SUMMARY.md                           |  1 +
 .../proving-system/circuit-commitments.md     | 34 +++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 book/src/design/proving-system/circuit-commitments.md

diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index ecfd665..a921346 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -16,6 +16,7 @@
   - [Proving system](design/proving-system.md)
     - [Lookup argument](design/proving-system/lookup-argument.md)
     - [Permutation argument](design/proving-system/permutation.md)
+    - [Circuit commitments](design/proving-system/circuit-commitments.md)
     - [Multipoint opening argument](design/proving-system/multipoint-opening.md)
     - [Comparison to other work](design/proving-system/comparison.md)
   - [Implementation](design/implementation.md)
diff --git a/book/src/design/proving-system/circuit-commitments.md b/book/src/design/proving-system/circuit-commitments.md
new file mode 100644
index 0000000..2f354a8
--- /dev/null
+++ b/book/src/design/proving-system/circuit-commitments.md
@@ -0,0 +1,34 @@
+# 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.
+
+> The only difference between advice and auxiliary columns, is that the commitments to
+> auxiliary columns are not placed in the proof, and are instead computed by the verifier.
+
+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 (pre-computed by both the prover and
+verifier, using a blinding factor of $1$). $\mathbf{A}$ is constructed by the prover and
+sent to the verifier.
+
+## Committing to the lookup permutations and equality constraint permutations
+
+TBD.
+
+The prover ends up with vectors of commitments $\mathbf{L}$ and $\mathbf{P}$.

From ffa8dacabae46ca0095b959dbebc7ab7f9bd3385 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Thu, 11 Feb 2021 03:10:00 +0000
Subject: [PATCH 04/17] book: Add section about vanishing argument

---
 book/src/SUMMARY.md                         |  1 +
 book/src/design/proving-system/vanishing.md | 79 +++++++++++++++++++++
 2 files changed, 80 insertions(+)
 create mode 100644 book/src/design/proving-system/vanishing.md

diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index a921346..f5a19ff 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -17,6 +17,7 @@
     - [Lookup argument](design/proving-system/lookup-argument.md)
     - [Permutation argument](design/proving-system/permutation.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)
     - [Comparison to other work](design/proving-system/comparison.md)
   - [Implementation](design/implementation.md)
diff --git a/book/src/design/proving-system/vanishing.md b/book/src/design/proving-system/vanishing.md
new file mode 100644
index 0000000..51922ce
--- /dev/null
+++ b/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 inherently represented as a polynomial of degree $d$ (the
+maximum degree of any of the relations). Given that the degree of the assignment
+polynomials (over which these relations are built) is $n - 1$, the full polynomial
+representing each relation has degree $d(n - 1)$.
+
+> 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).

From 91a90f1d9dd1e4ccdf482484119739307e377835 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Thu, 11 Feb 2021 15:27:45 +0000
Subject: [PATCH 05/17] book: Renumber multipoint opening challenges to match
 implementation

---
 .../proving-system/multipoint-opening.md      | 44 +++++++++----------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/book/src/design/proving-system/multipoint-opening.md b/book/src/design/proving-system/multipoint-opening.md
index 1030f96..1f23cd5 100644
--- a/book/src/design/proving-system/multipoint-opening.md
+++ b/book/src/design/proving-system/multipoint-opening.md
@@ -18,26 +18,26 @@ $$
 
 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$, at which we evaluate $a(X), b(X), c(X), d(X)$.
 2. The prover provides evaluations of each polynomial at each point of interest:
-   $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.
+   $a(x), b(x), c(x), d(x), c(\omega x), d(\omega x)$
+3. Sample random $x_1$, 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_2(X) &=& c(X) &+& x_4 d(X)
+    q_1(X) &=& a(X) &+& x_1 b(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(\omega x_3) + x_4 d(\omega x_3)
+                    c(x) + x_1 d(x),
+                    c(\omega x) + x_1 d(\omega x)
                 ]
             ]
     ```
@@ -48,33 +48,33 @@ The multipoint opening optimisation proceeds as such:
     $$
     \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(\omega x_3) &=& c(\omega x_3) + x_4 d(\omega x_3) \\
+        &r_2(x) &=& c(x) + x_1 d(x) \\
+        &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`:
     `f_polys`
     $$
     \begin{array}{rcl}
-    f_1(X) &=& \frac{ q_1(X) - r_1(X)}{X - x_3} \\
-    f_2(X) &=& \frac{ q_2(X) - r_2(X)}{(X - x_3)(X - \omega 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)(X - \omega x)} \\
     \end{array}
     $$
 
-    If $q_1(x_3) = r_1(x_3)$, 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_1(x) = r_1(x)$, then $f_1(X)$ should be a polynomial.
+    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.
-8. Construct $f(X) = f_1(X) + x_5 f_2(X)$.
-9. Sample random $x_6$, at which we evaluate $f(X)$:
+7. Sample random $x_2$ to keep the `f_polys` linearly independent.
+8. Construct $f(X) = f_1(X) + x_2 f_2(X)$.
+9.  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) \\
-           &=& \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)}
+    f(x_3) &=& f_1(x_3) &+& x_2 f_2(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.
-11. Construct `final_poly`, $$final\_poly(X) = f(X) + x_7 q_1(X) + x_7^2 q_2(X),$$
+10. Sample random $x_4$ to keep $f(X)$ and `q_polys` linearly independent.
+11. 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.

From 6da0adb4e107bfa6729d248d4a67e7baf6ae2dc6 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Thu, 11 Feb 2021 15:41:42 +0000
Subject: [PATCH 06/17] book: Refactor the multipoint opening argument section

---
 .../proving-system/multipoint-opening.md      | 41 ++++++++++++-------
 1 file changed, 27 insertions(+), 14 deletions(-)

diff --git a/book/src/design/proving-system/multipoint-opening.md b/book/src/design/proving-system/multipoint-opening.md
index 1f23cd5..ee60a71 100644
--- a/book/src/design/proving-system/multipoint-opening.md
+++ b/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
-queried:
+To open these commitments, we could create a polynomial $Q$ for each point that we 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,13 +19,23 @@ $$
 \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$, at which we evaluate $a(X), b(X), c(X), d(X)$.
-2. The prover provides evaluations of each polynomial at each point of interest:
-   $a(x), b(x), c(x), d(x), c(\omega x), d(\omega x)$
-3. Sample random $x_1$, to keep $a, b, c, d$ linearly independent.
-4. Accumulate polynomials and their corresponding evaluations according
+1. Sample random $x_1$, to keep $a, b, c, d$ linearly independent.
+2. Accumulate polynomials and their corresponding evaluations according
    to the point set at which they were queried:
     `q_polys`:
     $$
@@ -43,7 +56,7 @@ The multipoint opening optimisation proceeds as such:
     ```
     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}
@@ -54,7 +67,7 @@ The multipoint opening optimisation proceeds as such:
         &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}
@@ -66,15 +79,15 @@ The multipoint opening optimisation proceeds as such:
     If $q_1(x) = r_1(x)$, then $f_1(X)$ should be a polynomial.
     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_2$ to keep the `f_polys` linearly independent.
-8. Construct $f(X) = f_1(X) + x_2 f_2(X)$.
-9.  Sample random $x_3$, at which we evaluate $f(X)$:
+5. Sample random $x_2$ to keep the `f_polys` linearly independent.
+6. Construct $f(X) = f_1(X) + x_2 f_2(X)$.
+7.  Sample random $x_3$, at which we evaluate $f(X)$:
     $$
     \begin{array}{rcccl}
     f(x_3) &=& f_1(x_3) &+& x_2 f_2(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_4$ to keep $f(X)$ and `q_polys` linearly independent.
-11. Construct `final_poly`, $$final\_poly(X) = f(X) + x_4 q_1(X) + x_4^2 q_2(X),$$
+8.  Sample random $x_4$ to keep $f(X)$ and `q_polys` linearly independent.
+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.

From 7b7346c462d6eb8029f147df578fda3dd1f493b6 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Thu, 11 Feb 2021 19:41:00 +0000
Subject: [PATCH 07/17] book: Add a placeholder page for explaining the IPA

For now, it directs readers to the existing comparision page, which
describes Halo 2's IPA relative to another work.
---
 book/src/SUMMARY.md                             |  1 +
 book/src/design/proving-system/inner-product.md | 11 +++++++++++
 2 files changed, 12 insertions(+)
 create mode 100644 book/src/design/proving-system/inner-product.md

diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index f5a19ff..930d34a 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -19,6 +19,7 @@
     - [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)
diff --git a/book/src/design/proving-system/inner-product.md b/book/src/design/proving-system/inner-product.md
new file mode 100644
index 0000000..185fbf4
--- /dev/null
+++ b/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 comparision](comparison.md#bcms20-appendix-a2) for details.
+>
+> [BCMS20]: https://eprint.iacr.org/2020/499

From 59010c4674c8cb0b8a7b9234ab821130a893e32f Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Thu, 11 Feb 2021 21:22:18 +0000
Subject: [PATCH 08/17] book: Document commitments to lookup and equality
 constraint arguments

---
 book/src/design/proving-system.md             |  3 +-
 .../proving-system/circuit-commitments.md     | 52 +++++++++++++++++--
 book/src/design/proving-system/permutation.md | 10 +++-
 3 files changed, 60 insertions(+), 5 deletions(-)

diff --git a/book/src/design/proving-system.md b/book/src/design/proving-system.md
index 566f2cf..a9c63b3 100644
--- a/book/src/design/proving-system.md
+++ b/book/src/design/proving-system.md
@@ -45,9 +45,10 @@ now serves as a summary of the following sub-sections.
 |                                                                             | $\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$ |                                    |
+| $\mathbf{L}_p = [(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{L}_c = [L_0, L_1, \dots, L_{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)$                             |         |                                    |
diff --git a/book/src/design/proving-system/circuit-commitments.md b/book/src/design/proving-system/circuit-commitments.md
index 2f354a8..e2910f5 100644
--- a/book/src/design/proving-system/circuit-commitments.md
+++ b/book/src/design/proving-system/circuit-commitments.md
@@ -27,8 +27,54 @@ $\mathbf{F}$ is constructed as part of key generation (pre-computed by both the
 verifier, using a blinding factor of $1$). $\mathbf{A}$ is constructed by the prover and
 sent to the verifier.
 
-## Committing to the lookup permutations and equality constraint permutations
+## Committing to the lookup permutations
 
-TBD.
+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:
 
-The prover ends up with vectors of commitments $\mathbf{L}$ and $\mathbf{P}$.
+- 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-argument.md), obtaining $A'(X)$ and $S'(X)$.
+
+Finally, the prover creates blinding commitments for all of the lookups
+
+$$\mathbf{L}_p = \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 permutations
+
+In addition to committing to the individual permuted lookups, the prover needs to commit
+to constraint polynomials that enforce the correct relation between the permuted lookups
+and their un-permuted forms:
+
+$$L(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.
+
+As before, the prover creates blinding commitments for every constraint polynomial
+
+$$\mathbf{L}_c = \left[\text{Commit}(L(X))), \dots \right]$$
+
+and sends them to the verifier.
diff --git a/book/src/design/proving-system/permutation.md b/book/src/design/proving-system/permutation.md
index dfa0f77..a16f3ce 100644
--- a/book/src/design/proving-system/permutation.md
+++ b/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.

From 0a2fb4781da16004909363d6ae6a03271e15a960 Mon Sep 17 00:00:00 2001
From: str4d <jack@electriccoin.co>
Date: Sat, 13 Feb 2021 03:43:35 +1300
Subject: [PATCH 09/17] book: Small changes from review

Co-authored-by: Daira Hopwood <daira@jacaranda.org>
---
 book/src/design/proving-system.md               | 2 +-
 book/src/design/proving-system/inner-product.md | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/book/src/design/proving-system.md b/book/src/design/proving-system.md
index a9c63b3..280b5cf 100644
--- a/book/src/design/proving-system.md
+++ b/book/src/design/proving-system.md
@@ -8,7 +8,7 @@ The Halo 2 proving system can be broken down into five stages:
    - Equality constraint permutations.
    - Products for each lookup argument.
 2. Construct the vanishing argument to constrain all circuit relations to zero:
-   - Custom gates.
+   - Standard and custom gates.
    - Lookup argument rules.
    - Equality constraint permutation rules.
 3. Evaluate the above polynomials at all necessary points:
diff --git a/book/src/design/proving-system/inner-product.md b/book/src/design/proving-system/inner-product.md
index 185fbf4..7ccc9b2 100644
--- a/book/src/design/proving-system/inner-product.md
+++ b/book/src/design/proving-system/inner-product.md
@@ -6,6 +6,6 @@ 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 comparision](comparison.md#bcms20-appendix-a2) for details.
+> See [this comparison](comparison.md#bcms20-appendix-a2) for details.
 >
 > [BCMS20]: https://eprint.iacr.org/2020/499

From f30cbcbfc91e0d0fedc9336326e5ebc4255810b9 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Fri, 12 Feb 2021 14:48:05 +0000
Subject: [PATCH 10/17] book: Fix notation in example constraint system

---
 book/src/design/proving-system.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/book/src/design/proving-system.md b/book/src/design/proving-system.md
index 280b5cf..04e1eba 100644
--- a/book/src/design/proving-system.md
+++ b/book/src/design/proving-system.md
@@ -30,8 +30,8 @@ system:
 - One fixed column $f$.
 - Three custom gates:
   - $a \cdot b \cdot c_{-1} - d = 0$
-  - $f_{-1}(c) = 0$
-  - $f(d \cdot a) = 0$
+  - $f_{-1} \cdot c = 0$
+  - $f \cdot d \cdot a = 0$
 
 ## tl;dr
 

From 2c647009fcfe9d8913df517646e6c4b84b9763b2 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Fri, 12 Feb 2021 15:06:33 +0000
Subject: [PATCH 11/17] book: Fix notation for committing to lookup permutation
 product columns

---
 book/src/design/proving-system.md                  |  4 ++--
 .../design/proving-system/circuit-commitments.md   | 14 +++++++-------
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/book/src/design/proving-system.md b/book/src/design/proving-system.md
index 04e1eba..8cc801f 100644
--- a/book/src/design/proving-system.md
+++ b/book/src/design/proving-system.md
@@ -45,10 +45,10 @@ now serves as a summary of the following sub-sections.
 |                                                                             | $\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}_p = [(A'_0, S'_0), \dots, (A'_{m - 1}, S'_{m - 1})]$            | $\rarr$ |                                    |
+| $\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{L}_c = [L_0, L_1, \dots, L_{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)$                             |         |                                    |
diff --git a/book/src/design/proving-system/circuit-commitments.md b/book/src/design/proving-system/circuit-commitments.md
index e2910f5..60b07c0 100644
--- a/book/src/design/proving-system/circuit-commitments.md
+++ b/book/src/design/proving-system/circuit-commitments.md
@@ -45,7 +45,7 @@ follows:
 
 Finally, the prover creates blinding commitments for all of the lookups
 
-$$\mathbf{L}_p = \left[ (\text{Commit}(A'(X))), \text{Commit}(S'(X))), \dots \right]$$
+$$\mathbf{L} = \left[ (\text{Commit}(A'(X))), \text{Commit}(S'(X))), \dots \right]$$
 
 and sends them to the verifier.
 
@@ -60,21 +60,21 @@ and sends them to the verifier.
 
   and sends them to the verifier.
 
-## Committing to the lookup permutations
+## Committing to the lookup permutation product columns
 
 In addition to committing to the individual permuted lookups, the prover needs to commit
-to constraint polynomials that enforce the correct relation between the permuted lookups
-and their un-permuted forms:
+to the permutation product column
 
-$$L(X) = \frac{(A_\text{compressed}(X) + \beta)(S_\text{compressed}(X) + \gamma)}{(A'(X) + \beta)(S'(X) + \gamma)}$$
+$$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.
 
-As before, the prover creates blinding commitments for every constraint polynomial
+As before, the prover creates blinding commitments to the permutation product column for
+every lookup
 
-$$\mathbf{L}_c = \left[\text{Commit}(L(X))), \dots \right]$$
+$$\mathbf{Z} = \left[\text{Commit}(Z(X))), \dots \right]$$
 
 and sends them to the verifier.

From 3181a21cbabb010e9276434476e815acc9b51518 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Fri, 12 Feb 2021 15:06:58 +0000
Subject: [PATCH 12/17] book: Add beta and gamma requirements for lookup
 permutation product

Co-authored-by: Daira Hopwood <daira@jacaranda.org>
---
 book/src/design/proving-system/circuit-commitments.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/book/src/design/proving-system/circuit-commitments.md b/book/src/design/proving-system/circuit-commitments.md
index 60b07c0..df2b390 100644
--- a/book/src/design/proving-system/circuit-commitments.md
+++ b/book/src/design/proving-system/circuit-commitments.md
@@ -70,7 +70,10 @@ $$Z(X) = \frac{(A_\text{compressed}(X) + \beta)(S_\text{compressed}(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.
+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

From 7820083c0d4f5037598cd97d4975cee6ccfc0025 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Fri, 12 Feb 2021 15:13:16 +0000
Subject: [PATCH 13/17] book: Reword paragraph about degree of relation
 polynomials

---
 book/src/design/proving-system/vanishing.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/book/src/design/proving-system/vanishing.md b/book/src/design/proving-system/vanishing.md
index 51922ce..60025da 100644
--- a/book/src/design/proving-system/vanishing.md
+++ b/book/src/design/proving-system/vanishing.md
@@ -7,10 +7,10 @@ various circuit relations are satisfied:
 - The rules of the lookup arguments.
 - The rules of the equality constraint permutations.
 
-Each of these relations is inherently represented as a polynomial of degree $d$ (the
-maximum degree of any of the relations). Given that the degree of the assignment
-polynomials (over which these relations are built) is $n - 1$, the full polynomial
-representing each relation has degree $d(n - 1)$.
+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$:

From 576796037a4c6e08a7489ddcd98621c8b1bbe142 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Fri, 12 Feb 2021 15:15:05 +0000
Subject: [PATCH 14/17] book: Move lookup argument design page to have
 consistent URI

---
 book/src/SUMMARY.md                                             | 2 +-
 book/src/design/proving-system/circuit-commitments.md           | 2 +-
 .../src/design/proving-system/{lookup-argument.md => lookup.md} | 0
 3 files changed, 2 insertions(+), 2 deletions(-)
 rename book/src/design/proving-system/{lookup-argument.md => lookup.md} (100%)

diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index 930d34a..9265ae9 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -14,7 +14,7 @@
   - [Tips and tricks](user/tips-and-tricks.md)
 - [Design](design.md)
   - [Proving system](design/proving-system.md)
-    - [Lookup argument](design/proving-system/lookup-argument.md)
+    - [Lookup argument](design/proving-system/lookup.md)
     - [Permutation argument](design/proving-system/permutation.md)
     - [Circuit commitments](design/proving-system/circuit-commitments.md)
     - [Vanishing argument](design/proving-system/vanishing.md)
diff --git a/book/src/design/proving-system/circuit-commitments.md b/book/src/design/proving-system/circuit-commitments.md
index df2b390..d970e1f 100644
--- a/book/src/design/proving-system/circuit-commitments.md
+++ b/book/src/design/proving-system/circuit-commitments.md
@@ -41,7 +41,7 @@ follows:
   $$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-argument.md), obtaining $A'(X)$ and $S'(X)$.
+  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
 
diff --git a/book/src/design/proving-system/lookup-argument.md b/book/src/design/proving-system/lookup.md
similarity index 100%
rename from book/src/design/proving-system/lookup-argument.md
rename to book/src/design/proving-system/lookup.md

From 67b6d197aa25c8b660f9af3af14061dd4f670c0c Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Fri, 12 Feb 2021 15:18:12 +0000
Subject: [PATCH 15/17] book: Tweak wording for proving system stage 1
 commitments

---
 book/src/design/proving-system.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/book/src/design/proving-system.md b/book/src/design/proving-system.md
index 8cc801f..46be339 100644
--- a/book/src/design/proving-system.md
+++ b/book/src/design/proving-system.md
@@ -4,9 +4,8 @@ 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.
+   - Permuted values and products for each lookup argument.
    - Equality constraint permutations.
-   - Products for each lookup argument.
 2. Construct the vanishing argument to constrain all circuit relations to zero:
    - Standard and custom gates.
    - Lookup argument rules.

From 126abd151ccc89a7ad7b00582e1ca05b1ef261ba Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Fri, 12 Feb 2021 15:26:28 +0000
Subject: [PATCH 16/17] book: Clarify why fixed columns are shown separately in
 commitments

---
 book/src/design/proving-system/circuit-commitments.md | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/book/src/design/proving-system/circuit-commitments.md b/book/src/design/proving-system/circuit-commitments.md
index d970e1f..06d844c 100644
--- a/book/src/design/proving-system/circuit-commitments.md
+++ b/book/src/design/proving-system/circuit-commitments.md
@@ -8,8 +8,10 @@ auxiliary, and fixed columns. We define $F_{i,j}$ as the assignment in the $j$th
 the $i$th fixed column. Without loss of generality, we'll similarly define $A_{i,j}$ to
 represent the advice and auxiliary assignments.
 
-> The only difference between advice and auxiliary columns, is that the commitments to
-> auxiliary columns are not placed in the proof, and are instead computed by the verifier.
+> 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
@@ -23,9 +25,8 @@ 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 (pre-computed by both the prover and
-verifier, using a blinding factor of $1$). $\mathbf{A}$ is constructed by the prover and
-sent to the verifier.
+$\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
 

From 4739aaae5c8d23702c229a9e8b7099c0bd0619f3 Mon Sep 17 00:00:00 2001
From: Jack Grigg <jack@electriccoin.co>
Date: Fri, 12 Feb 2021 16:05:44 +0000
Subject: [PATCH 17/17] book: Clarify IPA inputs in tl;dr section

---
 book/src/design/proving-system.md | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/book/src/design/proving-system.md b/book/src/design/proving-system.md
index 46be339..e2b2599 100644
--- a/book/src/design/proving-system.md
+++ b/book/src/design/proving-system.md
@@ -59,12 +59,16 @@ now serves as a summary of the following sub-sections.
 | 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$ |                                    |
+| $\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 perform:
+Then the prover and verifier:
 
-$$\text{InnerProduct}(\text{LinCom}(Q, U, x_4), x_3, \text{LinCom}(q_\text{evals}, u_\text{eval}, x_4)).$$
+- 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.