book: Document commitments to lookup and equality constraint arguments

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)$                             |         |                                    |

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.

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.