diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index e6eb615..9265ae9 100644 --- a/book/src/SUMMARY.md +++ b/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) diff --git a/book/src/design/proving-system.md b/book/src/design/proving-system.md index adad839..e2b2599 100644 --- a/book/src/design/proving-system.md +++ b/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. 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..06d844c --- /dev/null +++ b/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. 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..7ccc9b2 --- /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 comparison](comparison.md#bcms20-appendix-a2) for details. +> +> [BCMS20]: https://eprint.iacr.org/2020/499 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 diff --git a/book/src/design/proving-system/multipoint-opening.md b/book/src/design/proving-system/multipoint-opening.md index 1030f96..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,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)$. -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. -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`: $$ \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) ] ] ``` 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(\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`: +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_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)$: +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_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),$$ +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. 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. diff --git a/book/src/design/proving-system/vanishing.md b/book/src/design/proving-system/vanishing.md new file mode 100644 index 0000000..60025da --- /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 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).