Compare commits

...

11 Commits

Author SHA1 Message Date
ying tong 08f582cdba
Merge 3039662c07 into 7df93fd855 2024-03-01 11:27:10 -07:00
Daira-Emma Hopwood 7df93fd855
Merge pull request #814 from adria0/fix/mdbook
Fix MD book generation
2024-02-26 23:50:17 +00:00
adria0 daaa638966 fix(mdbook): fix generation 2024-02-22 22:28:36 +01:00
ying tong 3039662c07
Apply suggestions from code review
Co-authored-by: Daira Hopwood <daira@jacaranda.org>
2023-06-28 01:24:15 +08:00
therealyingtong ed2354c7da [book] More detailed description of synthetic blinding factor
Co-authored-by: Lasse Bramer Schmidt <lasse@lasses-air.eduroam.net.au.dk>
2023-06-06 13:35:27 +08:00
therealyingtong dec83010ae Formatting and copy fixes 2023-05-27 15:19:57 +08:00
Lasse Bramer Schmidt 2038845fa0 changed challenge x to indeterminate X in step 19 2023-05-25 10:02:40 +02:00
Lasse Bramer Schmidt ff9f5939d1 added f calculation to protocol 2023-05-25 09:57:35 +02:00
therealyingtong 62757bfa61 Fix step 14; fix v in step 18
Co-authored-by: Daira Hopwood <daira@jacaranda.org>
Co-authored-by: str4d <jack@electriccoin.co>
2023-05-24 02:22:28 +08:00
ying tong 7d77466179
Update book/src/design/protocol.md
Co-authored-by: Daira Hopwood <daira@jacaranda.org>
2023-05-22 19:51:17 +08:00
therealyingtong 67fb6246c3 Update p_poly in protocol to match implementation
p_poly is constructed as a linear combination of q_prime and the
q_polys in steps 18 and 19 of the protocol description.
2023-05-22 00:15:55 +08:00
3 changed files with 26 additions and 22 deletions

View File

@ -12,7 +12,7 @@ jobs:
- uses: actions/checkout@v3
- uses: actions-rs/toolchain@v1
with:
toolchain: nightly
toolchain: '1.76.0'
override: true
# - name: Setup mdBook
@ -26,7 +26,7 @@ jobs:
uses: actions-rs/cargo@v1
with:
command: install
args: mdbook --git https://github.com/HollowMan6/mdBook.git --rev 62e01b34c23b957579c04ee1b24b57814ed8a4d5
args: mdbook --git https://github.com/HollowMan6/mdBook.git --rev 5830c9555a4dc051675d17f1fcb04dd0920543e8
- name: Install mdbook-katex and mdbook-pdf
uses: actions-rs/cargo@v1
@ -40,6 +40,11 @@ jobs:
- name: Build halo2 book
run: mdbook build book/
- uses: actions-rs/toolchain@v1
with:
toolchain: nightly-2023-10-05
override: true
- name: Build latest rustdocs
uses: actions-rs/cargo@v1
with:

View File

@ -14,8 +14,6 @@ title = "The halo2 Book"
macros = "macros.txt"
renderers = ["html"]
[output.katex]
[output.html]
[output.html.print]

View File

@ -330,30 +330,30 @@ In the following protocol, we take it for granted that each polynomial $a_i(X, \
1. $\prover$ and $\verifier$ proceed in the following $n_a$ rounds of interaction, where in round $j$ (starting at $0$)
* $\prover$ sets $a'_j(X) = a_j(X, c_0, c_1, ..., c_{j - 1}, a_0(X, \cdots), ..., a_{j - 1}(X, \cdots, c_{j - 1}))$
* $\prover$ sends a hiding commitment $A_j = \innerprod{\mathbf{a'}}{\mathbf{G}} + [\cdot] W$ where $\mathbf{a'}$ are the coefficients of the univariate polynomial $a'_j(X)$ and $\cdot$ is some random, independently sampled blinding factor elided for exposition. (This elision notation is used throughout this protocol description to simplify exposition.)
* $\prover$ sends a hiding commitment $A_j = \innerprod{\mathbf{a'}}{\mathbf{G}} + [a^*_j] W$ where $\mathbf{a'}$ are the coefficients of the univariate polynomial $a'_j(X)$ and $a^*_j$ is some fresh (random and independently sampled) blinding factor. Similar notation is used throughout this protocol description.
* $\verifier$ responds with a challenge $c_j$.
2. $\prover$ sets $g'(X) = g(X, c_0, c_1, ..., c_{n_a - 1}, \cdots)$.
3. $\prover$ sends a commitment $R = \innerprod{\mathbf{r}}{\mathbf{G}} + [\cdot] W$ where $\mathbf{r} \in \field^n$ are the coefficients of a randomly sampled univariate polynomial $r(X)$ of degree $n - 1$.
3. $\prover$ sends a commitment $R = \innerprod{\mathbf{r}}{\mathbf{G}} + [r^*] W$ where $\mathbf{r} \in \field^n$ are the coefficients of a randomly sampled univariate polynomial $r(X)$ of degree $n - 1$.
4. $\prover$ computes univariate polynomial $h(X) = \frac{g'(X)}{t(X)}$ of degree $n_g(n - 1) - n$.
5. $\prover$ computes at most $n - 1$ degree polynomials $h_0(X), h_1(X), ..., h_{n_g - 2}(X)$ such that $h(X) = \sum\limits_{i=0}^{n_g - 2} X^{ni} h_i(X)$.
6. $\prover$ sends commitments $H_i = \innerprod{\mathbf{h_i}}{\mathbf{G}} + [\cdot] W$ for all $i$ where $\mathbf{h_i}$ denotes the vector of coefficients for $h_i(X)$.
6. $\prover$ sends commitments $H_i = \innerprod{\mathbf{h_i}}{\mathbf{G}} + [h^*_i] W$ for all $i$ where $\mathbf{h_i}$ denotes the vector of coefficients for $h_i(X)$, and $h^*_i$ are fresh blinding factors.
7. $\verifier$ responds with challenge $x$ and computes $H' = \sum\limits_{i=0}^{n_g - 2} [x^{ni}] H_i$.
8. $\prover$ sets $h'(X) = \sum\limits_{i=0}^{n_g - 2} x^{ni} h_i(X)$.
8. $\prover$ sets $h'(X) = \sum\limits_{i=0}^{n_g - 2} x^{ni} h_i(X)$, and synthetic blinding factor $h'^* = \sum\limits_{i=0}^{n_g - 2} x^{ni} h^*_i$.
9. $\prover$ sends $r = r(x)$ and for all $i \in [0, n_a)$ sends $\mathbf{a_i}$ such that $(\mathbf{a_i})_j = a'_i(\omega^{(\mathbf{p_i})_j} x)$ for all $j \in [0, n_e - 1]$.
10. For all $i \in [0, n_a)$ $\prover$ and $\verifier$ set $s_i(X)$ to be the lowest degree univariate polynomial defined such that $s_i(\omega^{(\mathbf{p_i})_j} x) = (\mathbf{a_i})_j$ for all $j \in [0, n_e - 1)$.
11. $\verifier$ responds with challenges $x_1, x_2$ and initializes $Q_0, Q_1, ..., Q_{n_q - 1} = \zero$.
* Starting at $i=0$ and ending at $n_a - 1$ $\verifier$ sets $Q_{\sigma(i)} := [x_1] Q_{\sigma(i)} + A_i$.
* $\verifier$ finally sets $Q_0 := [x_1^2] Q_0 + [x_1] H' + R$.
12. $\prover$ initializes $q_0(X), q_1(X), ..., q_{n_q - 1}(X) = 0$.
* Starting at $i=0$ and ending at $n_a - 1$ $\prover$ sets $q_{\sigma(i)} := x_1 q_{\sigma(i)} + a'(X)$.
* $\prover$ finally sets $q_0(X) := x_1^2 q_0(X) + x_1 h'(X) + r(X)$.
12. $\prover$ initializes $q_0(X), q_1(X), ..., q_{n_q - 1}(X) = 0$ and blinding factors $q^*_0, q^*_1, ..., q^*_{n_q-1} = 0$.
* Starting at $i=0$ and ending at $n_a - 1$ $\prover$ sets $q_{\sigma(i)} := x_1 q_{\sigma(i)} + a'(X)$ and $q^*_{\sigma(i)} := x_1 q^*_{\sigma(i)} + a^*_i$.
* $\prover$ finally sets $q_0(X) := x_1^2 q_0(X) + x_1 h'(X) + r(X)$, and its corresponding synthetic blinding factor $q^*_0 := x_1^2 q^*_0 + x_1 h'^* + r^*$.
13. $\prover$ and $\verifier$ initialize $r_0(X), r_1(X), ..., r_{n_q - 1}(X) = 0$.
* Starting at $i = 0$ and ending at $n_a - 1$ $\prover$ and $\verifier$ set $r_{\sigma(i)}(X) := x_1 r_{\sigma(i)}(X) + s_i(X)$.
* Finally $\prover$ and $\verifier$ set $r_0 := x_1^2 r_0 + x_1 h + r$ and where $h$ is computed by $\verifier$ as $\frac{g'(x)}{t(x)}$ using the values $r, \mathbf{a}$ provided by $\prover$.
14. $\prover$ sends $Q' = \innerprod{\mathbf{q'}}{\mathbf{G}} + [\cdot] W$ where $\mathbf{q'}$ defines the coefficients of the polynomial
14. $\prover$ sends $Q' = \innerprod{\mathbf{q'}}{\mathbf{G}} + [q^{\prime *}] W$ where $q^{\prime *}$ is the synthetic blinding factor calculated in step 12, and $\mathbf{q'}$ defines the coefficients of the polynomial
$$q'(X) = \sum\limits_{i=0}^{n_q - 1}
x_2^i
x_2^{n_q - 1 - i}
\left(
\frac
{q_i(X) - r_i(X)}
@ -369,11 +369,12 @@ $$
15. $\verifier$ responds with challenge $x_3$.
16. $\prover$ sends $\mathbf{u} \in \field^{n_q}$ such that $\mathbf{u}_i = q_i(x_3)$ for all $i \in [0, n_q)$.
17. $\verifier$ responds with challenge $x_4$.
18. $\verifier$ sets $P = Q' + x_4 \sum\limits_{i=0}^{n_q - 1} [x_4^i] Q_i$ and $v = $
18. $\verifier$ sets $P = [x_4^{n_q}]Q' + \sum\limits_{i=0}^{n_q - 1} [x_4^{n_q - 1 - i}] Q_i$ and $v = $
$$
x_4^{n_q} \cdot
\sum\limits_{i=0}^{n_q - 1}
\left(
x_2^i
x_2^{n_q - 1 - i}
\left(
\frac
{ \mathbf{u}_i - r_i(x_3) }
@ -387,19 +388,19 @@ x_2^i
\right)
\right)
+
x_4 \sum\limits_{i=0}^{n_q - 1} x_4 \mathbf{u}_i
\sum\limits_{i=0}^{n_q - 1} x_4^{n_q - 1 - i} \mathbf{u}_i
$$
19. $\prover$ sets $p(X) = q'(X) + [x_4] \sum\limits_{i=0}^{n_q - 1} x_4^i q_i(X)$.
20. $\prover$ samples a random polynomial $s(X)$ of degree $n - 1$ with a root at $x_3$ and sends a commitment $S = \innerprod{\mathbf{s}}{\mathbf{G}} + [\cdot] W$ where $\mathbf{s}$ defines the coefficients of $s(X)$.
19. $\prover$ sets $p(X) = x_4^{n_q} \cdot q'(X) + \sum\limits_{i=0}^{n_q - 1} x_4^{n_q - 1 - i} \cdot q_i(X)$ and the corresponding synthetic blinding factor $p^* = x_4^{n_q} \cdot q'^* + \sum\limits_{i=0}^{n_q - 1} x_4^{n_q - 1 - i} \cdot q^*_i$.
20. $\prover$ samples a random polynomial $s(X)$ of degree $n - 1$ with a root at $x_3$ and sends a commitment $S = \innerprod{\mathbf{s}}{\mathbf{G}} + [s^{*}] W$ where $\mathbf{s}$ defines the coefficients of $s(X)$ and $s^{*}$ is a fresh blinding factor.
21. $\verifier$ responds with challenges $\xi, z$.
22. $\verifier$ sets $P' = P - [v] \mathbf{G}_0 + [\xi] S$.
23. $\prover$ sets $p'(X) = p(X) - p(x_3) + \xi s(X)$ (where $p(x_3)$ should correspond with the verifier's computed value $v$).
23. $\prover$ sets $p'(X) = p(X) - p(x_3) + \xi s(X)$ and $p^{\prime *} = s^* \cdot \xi + p^*$ (where $p(x_3)$ should correspond with the verifier's computed value $v$).
24. Initialize $\mathbf{p'}$ as the coefficients of $p'(X)$ and $\mathbf{G'} = \mathbf{G}$ and $\mathbf{b} = (x_3^0, x_3^1, ..., x_3^{n - 1})$. $\prover$ and $\verifier$ will interact in the following $k$ rounds, where in the $j$th round starting in round $j=0$ and ending in round $j=k-1$:
* $\prover$ sends $L_j = \innerprod{\mathbf{p'}_\hi}{\mathbf{G'}_\lo} + [z \innerprod{\mathbf{p'}_\hi}{\mathbf{b}_\lo}] U + [\cdot] W$ and $R_j = \innerprod{\mathbf{p'}_\lo}{\mathbf{G'}_\hi} + [z \innerprod{\mathbf{p'}_\lo}{\mathbf{b}_\hi}] U + [\cdot] W$.
* $\prover$ sends $L_j = \innerprod{\mathbf{p'}_\hi}{\mathbf{G'}_\lo} + [z \innerprod{\mathbf{p'}_\hi}{\mathbf{b}_\lo}] U + [\ell_j^*] W$ and $R_j = \innerprod{\mathbf{p'}_\lo}{\mathbf{G'}_\hi} + [z \innerprod{\mathbf{p'}_\lo}{\mathbf{b}_\hi}] U + [r_j^*] W$ where $\ell_j^*$ and $r_j^*$ are fresh blinding factors.
* $\verifier$ responds with challenge $u_j$ chosen such that $1 + u_{k-1-j} x_3^{2^j}$ is nonzero.
* $\prover$ and $\verifier$ set $\mathbf{G'} := \mathbf{G'}_\lo + u_j \mathbf{G'}_\hi$ and $\mathbf{b} := \mathbf{b}_\lo + u_j \mathbf{b}_\hi$.
* $\prover$ sets $\mathbf{p'} := \mathbf{p'}_\lo + u_j^{-1} \mathbf{p'}_\hi$.
25. $\prover$ sends $c = \mathbf{p'}_0$ and synthetic blinding factor $f$ computed from the elided blinding factors.
25. $\prover$ sends $c = \mathbf{p'}_0$ and synthetic blinding factor $f = p^{\prime *} + \sum_{j=0}^{k - 1}\left(\ell_j^* \cdot u_j^{-1} + r_j^* \cdot u_j\right)$.
26. $\verifier$ accepts only if $\sum_{j=0}^{k - 1} [u_j^{-1}] L_j + P' + \sum_{j=0}^{k - 1} [u_j] R_j = [c] \mathbf{G'}_0 + [c \mathbf{b}_0 z] U + [f] W$.
### Zero-knowledge and Completeness
@ -825,4 +826,4 @@ Having established that these are each non-rational polynomials of degree at mos
By construction of $h'(X)$ (from the representation $\repr{H'}{\mathbf{G}}$) in step 7 we know that $h'(x) = h(x)$ where by $h(X)$ we refer to the polynomial of degree at most $(n_g - 1) \cdot (n - 1)$ whose coefficients correspond to the concatenated representations of each $\repr{H_i}{\mathbf{G}}$. As before, suppose that $h(X)$ does _not_ take the form $g'(X) / t(X)$. Then because $h(X)$ is determined prior to the choice of $x$ then by the Schwartz-Zippel lemma we know that it would only agree with $g'(X) / t(X)$ at $(n_g - 1) \cdot (n - 1)$ points at most if the polynomials were not equal. By restricting again $|\badch(\trprefix{\tr'}{x})|/|\ch| \leq \frac{(n_g - 1) \cdot (n - 1)}{|\ch|} \leq \epsilon$ we obtain $h(X) = g'(X) / t(X)$ and because $h(X)$ is a non-rational polynomial by the factor theorem we obtain that $g'(X)$ vanishes over the domain $D$.
We now have that $g'(X)$ vanishes over $D$ but wish to show that $g(X, C_0, C_1, \cdots)$ vanishes over $D$ at all points to complete the proof. This just involves a sequence of applying the same technique to each of the challenges; since the polynomial $g(\cdots)$ has degree at most $n_g \cdot (n - 1)$ in any indeterminate by definition, and because each polynomial $a_i(X, C_0, C_1, ..., C_{i - 1}, \cdots)$ is determined prior to the choice of concrete challenge $c_i$ by similarly bounding $|\badch(\trprefix{\tr'}{c_i})|/|\ch| \leq \frac{n_g \cdot (n - 1)}{|\ch|} \leq \epsilon$ we ensure that $g(X, C_0, C_1, \cdots)$ vanishes over $D$, completing the proof.
We now have that $g'(X)$ vanishes over $D$ but wish to show that $g(X, C_0, C_1, \cdots)$ vanishes over $D$ at all points to complete the proof. This just involves a sequence of applying the same technique to each of the challenges; since the polynomial $g(\cdots)$ has degree at most $n_g \cdot (n - 1)$ in any indeterminate by definition, and because each polynomial $a_i(X, C_0, C_1, ..., C_{i - 1}, \cdots)$ is determined prior to the choice of concrete challenge $c_i$ by similarly bounding $|\badch(\trprefix{\tr'}{c_i})|/|\ch| \leq \frac{n_g \cdot (n - 1)}{|\ch|} \leq \epsilon$ we ensure that $g(X, C_0, C_1, \cdots)$ vanishes over $D$, completing the proof.