zec
/
halo2
mirror of https://github.com/zcash/halo2.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #148 from daira/daira-book-addition 

[book] Fixes to the completeness arguments for cases of complete addition, and a fix to the last step of variable-base scalar multiplication
This commit is contained in:
Daira Hopwood 2021-07-27 02:10:49 +01:00 committed by GitHub
parent 4229ba1dec a6badba32f
commit 29fe6e14fc
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 234 additions and 262 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

423
book/src/design/circuit/gadgets/ecc/addition.md
View File

@ -31,15 +31,13 @@ which is equivalent to
Assuming $x_p \neq x_q$,
$
\begin{array}{|rrll|}
\hline
&(x_r + x_q + x_p) \cdot (x_p - x_q)^2 &=& \lambda^2 \cdot (x_p - x_q)^2\\
\implies &(x_r + x_q + x_p) \cdot (x_p - x_q)^2 &=& (\lambda \cdot (x_p - x_q))^2\\
\\\hline
&y_r &=& \lambda \cdot (x_q - x_r) - y_q\\
\implies &y_r + y_q &=& \lambda \cdot (x_q - x_r)\\
\implies &(y_r + y_q) \cdot (x_p - x_q) &=& \lambda \cdot (x_p - x_q) \cdot (x_q - x_r)\\
\hline
\begin{array}{lrrll}
&&(x_r + x_q + x_p) \cdot (x_p - x_q)^2 &=& \lambda^2 \cdot (x_p - x_q)^2 \\
&\implies &(x_r + x_q + x_p) \cdot (x_p - x_q)^2 &=& \big(\lambda \cdot (x_p - x_q)\big)^2 \\[1.2ex]
\text{and} \\
& &y_r &=& \lambda \cdot (x_q - x_r) - y_q \\
&\implies &y_r + y_q &=& \lambda \cdot (x_q - x_r) \\
&\implies &(y_r + y_q) \cdot (x_p - x_q) &=& \lambda \cdot (x_p - x_q) \cdot (x_q - x_r)
\end{array}
$
@ -47,18 +45,18 @@ Substituting for $\lambda \cdot (x_p - x_q)$, we get the constraints:
- $(x_r + x_q + x_p) \cdot (x_p - x_q)^2 - (y_p - y_q)^2 = 0$
- Note that this constraint is unsatisfiable for $P \;⸭\; (-P)$ (when $P \neq \mathcal{O}$),
and so cannot be used with arbitrary inputs.
- $(y_r + y_q)(x_p - x_q) - (y_p - y_q)(x_q - x_r) = 0$
- $(y_r + y_q) \cdot (x_p - x_q) - (y_p - y_q) \cdot (x_q - x_r) = 0$
## Complete addition
$\begin{array}{rcll}
\mathcal{O} &+& \mathcal{O} &= \mathcal{O} \\
\mathcal{O} &+& (x_q, y_q) &= (x_q, y_q) \\
(x_p, y_p) &+& \mathcal{O} &= (x_p, y_p) \\
(x, y) &+& (x, y) &= [2] (x, y) \\
(x, y) &+& (x, -y) &= \mathcal{O} \\
(x_p, y_p) &+& (x_q, y_q) &= (x_p, y_p) \;⸭\; (x_q, y_q), \text{if } x_p \neq x_q
$\hspace{1em} \begin{array}{rcll}
\mathcal{O} &+& \mathcal{O} &= \mathcal{O} \\[0.4ex]
\mathcal{O} &+& (x_q, y_q) &= (x_q, y_q) \\[0.4ex]
(x_p, y_p) &+& \mathcal{O} &= (x_p, y_p) \\[0.6ex]
(x, y) &+& (x, y) &= [2] (x, y) \\[0.6ex]
(x, y) &+& (x, -y) &= \mathcal{O} \\[0.4ex]
(x_p, y_p) &+& (x_q, y_q) &= (x_p, y_p) \;⸭\; (x_q, y_q), \text{ if } x_p \neq x_q.
\end{array}$
Suppose that we represent $\mathcal{O}$ as $(0, 0)$. ($0$ is not an $x$-coordinate of a valid point because we would need $y^2 = x^3 + 5$, and $5$ is not square in $\mathbb{F}_q$. Also $0$ is not a $y$-coordinate of a valid point because $-5$ is not a cube in $\mathbb{F}_q$.)
@ -80,18 +78,22 @@ Define $\mathsf{inv0}(x) = \begin{cases} 0, &\text{if } x = 0 \\ 1/x, &\text{oth
Witness $\alpha, \beta, \gamma, \delta, \lambda$ where:
* $\alpha = \mathsf{inv0}(x_q - x_p)$
* $\beta = \mathsf{inv0}(x_p)$
* $\gamma = \mathsf{inv0}(x_q)$
* $\delta = \begin{cases}
\mathsf{inv0}(y_q + y_p), &\text{if } x_q = x_p \\
0, &\text{otherwise}
\end{cases}$
* $\lambda = \begin{cases}
\frac{y_q - y_p}{x_q - x_p}, &\text{if } x_q \neq x_p \\[0.5ex]
\frac{3{x_p}^2}{2y_p} &\text{if } x_q = x_p \wedge y_p \neq 0 \\[0.5ex]
0, &\text{otherwise.}
\end{cases}$
$\hspace{1em}
\begin{array}{rl}
\alpha \,\,=&\!\! \mathsf{inv0}(x_q - x_p) \\[0.4ex]
\beta \,\,=&\!\! \mathsf{inv0}(x_p) \\[0.4ex]
\gamma \,\,=&\!\! \mathsf{inv0}(x_q) \\[0.4ex]
\delta \,\,=&\!\! \begin{cases}
\mathsf{inv0}(y_q + y_p), &\text{if } x_q = x_p \\
0, &\text{otherwise}
\end{cases} \\[2.5ex]
\lambda \,\,=&\!\! \begin{cases}
\frac{y_q - y_p}{x_q - x_p}, &\text{if } x_q \neq x_p \\[1.2ex]
\frac{3{x_p}^2}{2y_p} &\text{if } x_q = x_p \wedge y_p \neq 0 \\[0.8ex]
0, &\text{otherwise.}
\end{cases}
\end{array}
$
### Constraints
@ -99,7 +101,7 @@ $$
\begin{array}{|c|rcl|l|}
\hline
\text{Degree} & \text{Constraint}\hspace{7em} &&& \text{Meaning} \\\hline
4 & q_\mathit{add} \cdot (x_q - x_p) \cdot ((x_q - x_p) \cdot \lambda - (y_q - y_p)) &=& 0 & x_q \neq x_p \implies \lambda = \frac{y_q - y_p}{x_q - x_p} \\\hline
4 & q_\mathit{add} \cdot (x_q - x_p) \cdot ((x_q - x_p) \cdot \lambda - (y_q - y_p)) &=& 0 & x_q \neq x_p \implies \lambda = \frac{y_q - y_p}{x_q - x_p} \\\hline \\[-2.3ex]
5 & q_\mathit{add} \cdot (1 - (x_q - x_p) \cdot \alpha) \cdot \left(2y_p \cdot \lambda - 3{x_p}^2\right) &=& 0 & \begin{cases} x_q = x_p \wedge y_p \neq 0 \implies \lambda = \frac{3{x_p}^2}{2y_p} \\ x_q = x_p \wedge y_p = 0 \implies x_p = 0 \end{cases} \\\hline
6 & q_\mathit{add} \cdot x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda^2 - x_p - x_q - x_r) &=& 0 & x_p \neq 0 \wedge x_q \neq 0 \wedge x_q \neq x_p \implies x_r = \lambda^2 - x_p - x_q \\
6 & q_\mathit{add} \cdot x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) &=& 0 & x_p \neq 0 \wedge x_q \neq 0 \wedge x_q \neq x_p \implies y_r = \lambda \cdot (x_p - x_r) - y_p \\
@ -118,120 +120,119 @@ Max degree: 6
### Analysis of constraints
$$
\begin{array}{ccl}
1.&& (x_q - x_p) \cdot ((x_q - x_p) \cdot \lambda - (y_q - y_p)) = 0 \\
&& \\
&& \begin{aligned}
\text{At least one of } &x_q - x_p = 0 \\
\text{or } &(x_q - x_p) \cdot \lambda - (y_q - y_p) = 0 \\
\end{aligned} \\
&& \text{must be satisfied for the constraint to be satisfied.} \\
&& \\
&& \text{If } x_q - x_p \neq 0, \text{ then } (x_q - x_p) \cdot \lambda - (y_q - y_p) = 0 \\
&& \\
&& \text{If } (x_q - x_p) \cdot \lambda - (y_q - y_p) = 0, \text{ then because } x_q - x_p \neq 0, \\
&& \text{ by rearranging both sides we get } \lambda = (y_q - y_p) / (x_q - x_p) \\
&& \\
&& \text{and therefore:}\\
&& \hspace{2em} x_q \neq x_p \implies \lambda = (y_q - y_p) / (x_q - x_p).\\
&& \\
2.&& (1 - (x_q - x_p) \cdot \alpha) \cdot (2y_p \cdot \lambda - 3x_p^2) = 0\\
&& \begin{aligned}
\text{At least one of } &(1 - (x_q - x_p) \cdot \alpha) = 0 \\
\text{or } &(2y_p \cdot \lambda - 3x_p^2) = 0
\end{aligned} \\
&& \text{must be satisfied for the constraint to be satisfied.} \\
&& \\
&& \text{If } x_q = x_p, \text{ then } 1 - (x_q - x_p) \cdot \alpha = 0 \text{ has no solution for } \alpha, \\
&& \text{ so it must be that } 2y_p \cdot \lambda - 3x_p^2 = 0. \\
&& \\
&& \text{If } y_p = 0 \text{ then } x_p = 0, \text{ and the constraint is satisfied.}\\
&& \\
&& \text{If } y_p \neq 0 \text{ by rearranging both sides we get }\\
&& \lambda = 3x_p^2 / 2y_p \\
&& \text{Therefore:} \\
&& \hspace{2em} (x_q = x_p) \wedge y_p \neq 0 \implies \lambda = 3x_p^2 / 2y_p. \\
&& \\
3.& \text{a)} & x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda^2 - x_p - x_q - x_r) = 0 \\
& \text{b)} & x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) = 0 \\
& \text{c)} & x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda^2 - x_p - x_q - x_r) = 0 \\
& \text{d)} & x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) = 0 \\
&& \\
&& \begin{aligned}
\text{At least one of } &x_p = 0 \\
\text{or } &x_p = 0 \\
\text{or } &(x_q - x_p) = 0 \\
\text{or } &(\lambda^2 - x_p - x_q - x_r) = 0 \\
\begin{array}{rl}
1. & (x_q - x_p) \cdot ((x_q - x_p) \cdot \lambda - (y_q - y_p)) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } &x_q - x_p = 0 \\
\text{or } &(x_q - x_p) \cdot \lambda - (y_q - y_p) = 0 \\
\end{aligned} \\
& \text{must be satisfied for the constraint to be satisfied.} \\
& \\
& \text{If } x_q - x_p \neq 0, \text{ then } (x_q - x_p) \cdot \lambda - (y_q - y_p) = 0, \text{ and} \\
& \text{by rearranging both sides we get } \lambda = (y_q - y_p) / (x_q - x_p). \\
& \\
& \text{Therefore:} \\
& \hspace{2em} x_q \neq x_p \implies \lambda = (y_q - y_p) / (x_q - x_p).\\
& \\
2. & (1 - (x_q - x_p) \cdot \alpha) \cdot (2y_p \cdot \lambda - 3x_p^2) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } &(1 - (x_q - x_p) \cdot \alpha) = 0 \\
\text{or } &(2y_p \cdot \lambda - 3x_p^2) = 0
\end{aligned} \\
& \text{must be satisfied for the constraint to be satisfied.} \\
& \\
& \text{If } x_q = x_p, \text{ then } 1 - (x_q - x_p) \cdot \alpha = 0 \text{ has no solution for } \alpha, \\
& \text{so it must be that } 2y_p \cdot \lambda - 3x_p^2 = 0. \\
& \\
& \text{If } x_q = x_p \text{ and } y_p = 0 \text{ then } x_p = 0, \text{ and the constraint is satisfied.}\\
& \\
& \text{If } x_q = x_p \text{ and } y_p \neq 0 \text{ then by rearranging both sides} \\
& \text{we get } \lambda = 3x_p^2 / 2y_p. \\
& \\
& \text{Therefore:} \\
& \hspace{2em} (x_q = x_p) \wedge y_p \neq 0 \implies \lambda = 3x_p^2 / 2y_p. \\
& \\
3.\text{ a)} & x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda^2 - x_p - x_q - x_r) = 0 \\
\text{ b)} & x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) = 0 \\
\text{ c)} & x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda^2 - x_p - x_q - x_r) = 0 \\
\text{ d)} & x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } &x_p = 0 \\
\text{or } &x_p = 0 \\
\text{or } &(x_q - x_p) = 0 \\
\text{or } &(\lambda^2 - x_p - x_q - x_r) = 0 \\
\end{aligned} \\
&& \text{must be satisfied for constraint (a) to be satisfied.} \\
&& \\
&& \text{Let } x_p \neq 0 \wedge x_q \neq 0 \wedge x_q \neq x_p. \\
&& \begin{aligned}
&\text{• Constraint (a) imposes that } x_r = \lambda^2 - x_p - x_q \text{ is satisfied.} \\
&\text{• Similarly, constraint (b) imposes that } y_r = \lambda \cdot (x_p - x_r) - y_p \text{ is satisfied.} \\
\end{aligned} \\
&& \\
&& \text{Let } x_p \neq 0 \wedge x_q \neq 0 \wedge y_q \neq -y_p. \\
&& \begin{aligned}
&\text{• Similarly, constraint (c) imposes that } x_r = \lambda^2 - x_p - x_q \text{ is satisfied.} \\
&\text{• Similarly, constraint (d) imposes that } y_r = \lambda \cdot (x_p - x_r) - y_p \text{ is satisfied.} \\
\end{aligned} \\
&& \\
&& \text{Therefore:} \\
&& \begin{aligned}
&(x_p \neq 0) \wedge (x_q \neq 0) \wedge ((x_q \neq x_p) \vee (y_q \neq -y_p)) \\
& \text{must be satisfied for constraint (a) to be satisfied.} \\
& \\
& \text{If } x_p \neq 0 \wedge x_q \neq 0 \wedge x_q \neq x_p, \\[1.5ex]
& \text{• Constraint (a) imposes that } x_r = \lambda^2 - x_p - x_q. \\
& \text{• Constraint (b) imposes that } y_r = \lambda \cdot (x_p - x_r) - y_p. \\
& \\
& \text{If } x_p \neq 0 \wedge x_q \neq 0 \wedge y_q \neq -y_p, \\[1.5ex]
& \text{• Constraint (c) imposes that } x_r = \lambda^2 - x_p - x_q. \\
& \text{• Constraint (d) imposes that } y_r = \lambda \cdot (x_p - x_r) - y_p. \\
& \\
& \text{Therefore:} \\
& \begin{aligned}
&(x_p \neq 0) \wedge (x_q \neq 0) \wedge ((x_q \neq x_p) \vee (y_q \neq -y_p)) \\
\implies &(x_r = \lambda^2 - x_p - x_q) \wedge (y_r = \lambda \cdot (x_p - x_r) - y_p).
\end{aligned} \\
&& \\
4.& \text{a)} & (1 - x_p \cdot \beta) \cdot (x_r - x_q) = 0 \\
& \text{b)} & (1 - x_p \cdot \beta) \cdot (y_r - y_q) = 0 \\
&& \\
&& \begin{aligned}
\text{At least one of } 1 - x_p \cdot \beta &= 0 \\
\text{or } x_r - x_q &= 0
& \\
4.\text{ a)} & (1 - x_p \cdot \beta) \cdot (x_r - x_q) = 0 \\
\text{ b)} & (1 - x_p \cdot \beta) \cdot (y_r - y_q) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } 1 - x_p \cdot \beta &= 0 \\
\text{or } x_r - x_q &= 0
\end{aligned} \\
&& \\
&& \text{must be satisfied for constraint (a) to be satisfied.} \\
&& \text{If } x_p = 0 \text{ then } 1 - x_p \cdot \beta = 0 \text{ has no solutions for } \beta, \\
&& \text{and so it must be that } x_r - x_q = 0. \\
&& \\
&& \text{Similarly, constraint (b) imposes that } y_r - y_q = 0. \\
&& \\
&& \text{Therefore:} \\
&& \hspace{2em} x_p = 0 \implies (x_r, y_r) = (x_q, y_q). \\
&& \\
5.& \text{a)} & (1 - x_q \cdot \beta) \cdot (x_r - x_p) = 0 \\
& \text{b)} & (1 - x_q \cdot \beta) \cdot (y_r - y_p) = 0 \\
&& \\
&& \begin{aligned}
\text{At least one of } 1 - x_q \cdot \beta &= 0 \\
\text{or } x_r - x_p &= 0
& \text{must be satisfied for constraint (a) to be satisfied.} \\
& \\
& \text{If } x_p = 0 \text{ then } 1 - x_p \cdot \beta = 0 \text{ has no solutions for } \beta, \\
& \text{and so it must be that } x_r - x_q = 0. \\
& \\
& \text{Similarly, constraint (b) imposes that if } x_p = 0 \\
& \text{then } y_r - y_q = 0. \\
& \\
& \text{Therefore:} \\
& \hspace{2em} x_p = 0 \implies (x_r, y_r) = (x_q, y_q). \\
& \\
5.\text{ a)} & (1 - x_q \cdot \beta) \cdot (x_r - x_p) = 0 \\
\text{ b)} & (1 - x_q \cdot \beta) \cdot (y_r - y_p) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } 1 - x_q \cdot \beta &= 0 \\
\text{or } x_r - x_p &= 0
\end{aligned} \\
&& \\
&& \text{must be satisfied for constraint (a) to be satisfied.} \\
&& \\
&& \text{If } x_q = 0 \text{ then } 1 - x_q \cdot \beta = 0 \text{ has no solutions for } \beta, \\
&& \text{and so it must be that } x_r - x_p = 0. \\
&& \\
&& \text{Similarly, constraint (b) imposes that } y_r - y_p = 0. \\
&& \\
&& \text{Therefore:}\\
&& \hspace{2em} x_q = 0 \implies (x_r, y_r) = (x_p, y_p). \\
&& \\
6.& \text{a)} & (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot x_r = 0 \\
& \text{b)} & (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot y_r = 0 \\
&& \\
&& \begin{aligned}
\text{At least one of } &1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta = 0 \\
\text{or } &x_r = 0
& \text{must be satisfied for constraint (a) to be satisfied.} \\
& \\
& \text{If } x_q = 0 \text{ then } 1 - x_q \cdot \beta = 0 \text{ has no solutions for } \beta, \\
& \text{and so it must be that } x_r - x_p = 0. \\
& \\
& \text{Similarly, constraint (b) imposes that if } x_q = 0 \\
& \text{then } y_r - y_p = 0. \\
& \\
& \text{Therefore:} \\
& \hspace{2em} x_q = 0 \implies (x_r, y_r) = (x_p, y_p). \\
& \\
6.\text{ a)} & (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot x_r = 0 \\
\text{ b)} & (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot y_r = 0 \\
& \\
& \begin{aligned}
\text{At least one of } &1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta = 0 \\
\text{or } &x_r = 0
\end{aligned} \\
&& \\
&& \text{must be satisfied for constraint (a) to be satisfied.}
&& \\
&& \text{If } x_r \neq 0, \text{ then it must be that } 1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta = 0. \\
&& \\
&& \text{However, if } x_q = x_p \wedge y_q = -y_p, \text{ then there are no solutions for } \alpha \text { and } \delta. \\
&& \text{Therefore: } x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0).
& \text{must be satisfied for constraint (a) to be satisfied,} \\
& \text{and similarly replacing } x_r \text{ by } y_r. \\
& \\
& \text{If } x_r \neq 0 \text{ or } y_r = 0, \text{ then it must be that } 1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta = 0. \\
& \\
& \text{However, if } x_q = x_p \wedge y_q = -y_p, \text{ then there are no solutions for } \alpha \text { and } \delta. \\
& \\
& \text{Therefore: } \\
& \hspace{2em} x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0).
\end{array}
$$
@ -239,140 +240,116 @@ $$
$
\begin{array}{cl}
(1)& x_q \neq x_p \implies \lambda = (y_q - y_p) / (x_q - x_p). \\
(2)& (x_q = x_p) \wedge y_p \neq 0 \implies \lambda = 3x_p^2 / 2y_p \\
(3)& (x_p \neq 0) \wedge (x_q \neq 0) \wedge ((x_q \neq x_p) \vee (y_q \neq -y_p)) \\
&\implies (x_r = \lambda^2 - x_p - x_q) \wedge (y_r = \lambda \cdot (x_p - x_r) - y_p) \\
(4)& x_p = 0 \implies (x_r, y_r) = (x_q, y_q) \\
(5)& x_q = 0 \implies (x_r, y_r) = (x_p, y_p) \\
(6)& x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0) \\
(1)& x_q \neq x_p \implies \lambda = (y_q - y_p) / (x_q - x_p) \\[0.8ex]
(2)& (x_q = x_p) \wedge y_p \neq 0 \implies \lambda = 3x_p^2 / 2y_p \\[0.8ex]
(3)& (x_p \neq 0) \wedge (x_q \neq 0) \wedge ((x_q \neq x_p) \vee (y_q \neq -y_p)) \\[0.4ex]
&\implies (x_r = \lambda^2 - x_p - x_q) \wedge (y_r = \lambda \cdot (x_p - x_r) - y_p) \\[0.8ex]
(4)& x_p = 0 \implies (x_r, y_r) = (x_q, y_q) \\[0.8ex]
(5)& x_q = 0 \implies (x_r, y_r) = (x_p, y_p) \\[0.8ex]
(6)& x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0)
\end{array}
$
#### Test cases:
#### Cases:
$(x_p, y_p) + (x_q, y_q) = (x_r, y_r)$
Note that we rely on the fact that $0$ is not a valid $x$-coordinate or $y$-coordinate of a
point on the Pallas curve other than $\mathcal{O}$.
* $(0, 0) + (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{ holds because } x_q = x_p \\
(2)&\text{ holds because } y_p = 0 \\
(3)&\text{ holds because } x_p = 0 \\
(4)&\text{ holds because } x_p = 0 \text{ only when } x_r = 0, y_r = 0 \\
(5)&\text{ holds because } x_q = 0 \text{ only when } x_r = 0, y_r = 0 \\
(6)&\text{ holds because } x_q = x_p \wedge y_q = -y_p \text{ only when } (x_r, y_r) = (0, 0) \\
(1)&\text{holds because } x_q = x_p \\
(2)&\text{holds because } y_p = 0 \\
(3)&\text{holds because } x_p = 0 \\
(4)&\text{holds because } (x_r, y_r) = (x_q, y_q) = (0, 0) \\
(5)&\text{holds because } (x_r, y_r) = (x_p, y_p) = (0, 0) \\
(6)&\text{holds because } (x_r, y_r) = (0, 0). \\
\end{array}
$
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution
* $(x, y) + (0, 0)$
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution to $(6).$
* $(x, y) + (0, 0)$ for $(x, y) \neq (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{ holds because } x_q \neq x_p \text{ because 0 is not a valid x-coordinate }\\
&\text{ only when } \lambda = (y_q - y_p) / (x_q - x_p) \text{ which is defined because } x_q \neq x_p \\
(2)&\text{ holds because } x_q \neq x_p \text{ because 0 is not a valid x-coordinate }\\
&\text{ only when } \alpha = (x_q - x_p)^{-1} \\
(3)&\text{ holds because } x_q = 0 \\
(4)&\text{ holds because } x_p \neq 0 \text{ because 0 is not a valid x-coordinate }\\
&\text{ only when } \beta = x_p^{-1} \\
(5)&\text{ holds because } x_q = 0 \text{ only when } (x_r, y_r) = (x_p, y_p) \\
(6)&\text{ holds because } y_p \neq -y_p \text{ because 0 is not a valid y-coordinate}\\
&\text{ only when } \delta = (y_q + y_p)^{-1} \text{ which is defined because 0 is not a valid y-coordinate} \\
(1)&\text{holds because } x_q \neq x_p, \text{ therefore } \lambda = (y_q - y_p) / (x_q - x_p) \text{ is a solution} \\
(2)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ is a solution} \\
(3)&\text{holds because } x_q = 0 \\
(4)&\text{holds because } x_p \neq 0, \text{ therefore } \beta = x_p^{-1} \text{ is a solution} \\
(5)&\text{holds because } (x_r, y_r) = (x_p, y_p) \\
(6)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ and } \delta = 0 \text{ is a solution.}
\end{array}
$
- Soundness: $(x_r, y_r) = (x_p, y_p)$ is the only solution
* $(0, 0) + (x, y)$
- Soundness: $(x_r, y_r) = (x_p, y_p)$ is the only solution to $(5).$
* $(0, 0) + (x, y)$ for $(x, y) \neq (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{ holds because } x_q \neq x_p \text{ because 0 is not a valid x-coordinate} \\
&\text{ only when } \lambda = (y_q - y_p) / (x_q - x_p) \text{ which is defined because } x_q \neq x_p \\
(2)&\text{ holds because } x_q \neq x_p \text{ because 0 is not a valid x-coordinate} \\
&\text{ only when } \alpha = (x_q - x_p)^{-1} \\
(3)&\text{ holds because } x_p = 0 \\
(4)&\text{ holds because } x_p = 0 \\
&\text{ only when } (x_r, y_r) = (x_q, y_q) \\
(5)&\text{ holds because } x_q \neq 0 \text{ because 0 is not a valid x-coordinate} \\
&\text{ only when } \gamma = x_q^{-1} \\
(6)&\text{ holds because } y_p \neq -y_p \text{ because 0 is not a valid y-coordinate} \\
&\text{ only when } \delta = (y_q + y_p)^{-1} \text{which is defined because 0 is not a valid y-coordinate} \\
(1)&\text{holds because } x_q \neq x_p, \text{ therefore } \lambda = (y_q - y_p) / (x_q - x_p) \text{ is a solution} \\
(2)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ is a solution} \\
(3)&\text{holds because } x_p = 0 \\
(4)&\text{holds because } x_p = 0 \text{ only when } (x_r, y_r) = (x_q, y_q) \\
(5)&\text{holds because } x_q \neq 0, \text{ therefore } \gamma = x_q^{-1} \text{ is a solution}\\
(6)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ and } \delta = 0 \text{ is a solution.}
\end{array}
$
- Soundness: $(x_r, y_r) = (x_q, y_q)$ is the only solution
- Soundness: $(x_r, y_r) = (x_q, y_q)$ is the only solution to $(4).$
* $(x, y) + (x, y)$
* $(x, y) + (x, y)$ for $(x, y) \neq (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{ holds because } x_q = x_p \\
(2)&\text{ holds because } x_q = x_p \wedge y_p \neq 0 \text{ (because 0 is not a valid y-coordinate)} \\
&\text{ only when } \lambda = 3x_p^2 / 2y_p \\
(3)&\text{ holds because } x_p \neq 0 \wedge x_q \neq 0 and y_q \neq -y_p \\
&\text{ only when } x_r = \lambda^2 - x_p - x_q \wedge y_r = \lambda * (x_p - x_r) - y_p \\
(4)&\text{ holds because } x_p \neq 0 \text{ only when } \beta = x_p^{-1} \\
(5)&\text{ holds because } x_p \neq 0 \text{ only when } \gamma = x_q^{-1} \\
(6)&\text{ holds because } y_q \neq -y_p \text{ only when } \delta = (y_q + y_p)^{-1} \\
&\text{ which is defined because 0 is not a valid y-coordinate} \\
(1)&\text{holds because } x_q = x_p \\
(2)&\text{holds because } x_q = x_p \wedge y_p \neq 0, \text{ therefore } \lambda = 3x_p^2 / 2y_p \text{ is a solution}\\
(3)&\text{holds because } x_r = \lambda^2 - x_p - x_q \wedge y_r = \lambda \cdot (x_p - x_r) - y_p \text{ in this case} \\
(4)&\text{holds because } x_p \neq 0, \text{ therefore } \beta = x_p^{-1} \text{ is a solution} \\
(5)&\text{holds because } x_p \neq 0, \text{ therefore } \gamma = x_q^{-1} \text{ is a solution} \\
(6)&\text{holds because } x_q = x_p \text{ and } y_q \neq -y_p, \text{ therefore } \alpha = 0 \text{ and } \delta = (y_q + y_p)^{-1} \text{ is a solution.} \\
\end{array}
$
- Soundness: $(x_r, y_r) = (\lambda^2 - x_p - x_q, \lambda * (x_p - x_r) - y_p)$ is the only solution
* $(x, y) + (x, -y)$
- Soundness: $\lambda$ is computed correctly, and $(x_r, y_r) = (\lambda^2 - x_p - x_q, \lambda \cdot (x_p - x_r) - y_p)$ is the only solution.
* $(x, y) + (x, -y)$ for $(x, y) \neq (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{ holds because } x_q = x_p \\
(2)&\text{ holds because } x_q = x_p \wedge y_p \neq 0 \text{ (because 0 is not a valid y-coordinate)} \\
&\text{only when } \lambda = 3x_p^2 / 2y_p \\
(3)&\text{ holds because } x_p \neq 0 \wedge x_q \neq 0 \text{ but } y_q = -y_p \wedge x_q = x_p \\
(4)&\text{ holds because } x_p \neq 0 \text{ only when } \beta = x_p^{-1} \\
(5)&\text{ holds because } x_q \neq 0 \text{ only when } \gamma = x_q^{-1} \\
(6)&\text{ holds because } x_q = x_p \wedge y_q = -y_p \text{ only when } (x_r, y_r) = (0, 0) \\
(1)&\text{holds because } x_q = x_p \\
(2)&\text{holds because } x_q = x_p \wedge y_p \neq 0, \text{ therefore } \lambda = 3x_p^2 / 2y_p \text{ is a solution} \\
&\text{(although } \lambda \text{ is not used in this case)} \\
(3)&\text{holds because } x_q = x_p \text{ and } y_q = -y_p \\
(4)&\text{holds because } x_p \neq 0, \text{ therefore } \beta = x_p^{-1} \text{ is a solution} \\
(5)&\text{holds because } x_q \neq 0, \text{ therefore } \gamma = x_q^{-1} \text{ is a solution} \\
(6)&\text{holds because } (x_r, y_r) = (0, 0) \\
\end{array}
$
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution
* $(\zeta x, y) + (x, y)$
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution to $(6).$
* $(x_p, y_p) + (x_q, y_q)$ for $(x_p, y_p) \neq (0,0)$ and $(x_q, y_q) \neq (0, 0)$ and $x_p \neq x_q$
- Completeness:
$
\begin{array}{cl}
(1)&\text{ holds because } x_q \neq x_p \text{ only when } \lambda = (y_q - y_p) / (x_q - x_p) \\
&\text{ which is defined because } x_q \neq x_p \\
(2)&\text{ holds because } x_p \neq x_p \text{ only when } \alpha = (x_q - x_p)^{-1} \\
&\text{ which is defined because } x_q \neq x_p \\
(3)&\text{ holds because } (x_p \neq 0) \wedge (x_q \neq 0) \wedge (x_q \neq x_p) \\
&\text{ only when } x_r = \lambda^2 - x_p - x_q \wedge y_r = \lambda * (x_p - x_r) - y_p \\
(4)&\text{ holds because } x_p \neq 0 \text{ only when } \beta = x_p^{-1} \\
(5)&\text{ holds because } x_q \neq 0 \text{ only when } \gamma = x_q^{-1} \\
(6)&\text{ holds because } x_q \neq x_p \text{ only when } \delta = 0 \\
(1)&\text{holds because } x_q \neq x_p, \text{ therefore } \lambda = (y_q - y_p) / (x_q - x_p) \text{ is a solution} \\
(2)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ is a solution} \\
(3)&\text{holds because } x_r = \lambda^2 - x_p - x_q \wedge y_r = \lambda \cdot (x_p - x_r) - y_p \text{ in this case} \\
(4)&\text{holds because } x_p \neq 0, \text{ therefore } \beta = x_p^{-1} \text{ is a solution} \\
(5)&\text{holds because } x_q \neq 0, \text{ therefore } \gamma = x_q^{-1} \text{ is a solution} \\
(6)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ and } \delta = 0 \text{ is a solution.}
\end{array}
$
- Soundness: $(x_r, y_r) = (\lambda^2 - x_p - x_q, \lambda * (x_p - x_r) - y_p)$ is the only solution
All remaining cases $(x, y) + (x', y')$ are identical to the case $(\zeta x, y) + (x, y)$ when
$$
\begin{aligned}
\lambda &= (y_q - y_p) / (x_q - x_p) \\
\alpha &= (x_q - x_p)^{-1} \\
\beta &= x_p^{-1} \\
\gamma &= x_q^{-1} \\
\delta &= 0 \\
\end{aligned}
$$
because in all remaining cases, $x_q \neq x_p, x_p \neq 0, x_q \neq 0.$
- Soundness: $\lambda$ is computed correctly, and $(x_r, y_r) = (\lambda^2 - x_p - x_q, \lambda \cdot (x_p - x_r) - y_p)$ is the only solution.

73
book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md
View File

@ -99,58 +99,53 @@ $$
\end{aligned}
$$
Initialize $A_{254} = [2] T.$
for $i$ from $254$ down to $4$:
$\begin{array}{ll}
\hspace{2em}& (\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\
\hspace{2em}& \mathbf{z}_{i} = 2\mathbf{z}_{i+1} + \mathbf{k}_{i}\\
\hspace{2em}& x_{P,i} = x_T\\
\hspace{2em}& y_{P,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)}\\
\hspace{2em}& \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) = y_{A,i} - y_{P,i}\\
\hspace{2em}& \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{P,i}\\
\hspace{2em}& (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) = 2 y_{\mathsf{A},i}\\
\hspace{2em}& \lambda_{2,i}^2 = x_{A,i-1} + x_{R,i} + x_{A,i}\\
\hspace{2em}& \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A,i-1},\\
$\begin{array}{l}
\text{Initialize } A_{254} = [2] T. \\
\\
\text{for } i \text{ from } 254 \text{ down to } 4: \\
\hspace{1.5em} (\mathbf{k}_i)(\mathbf{k}_i-1) = 0 \\
\hspace{1.5em} \mathbf{z}_{i} = 2\mathbf{z}_{i+1} + \mathbf{k}_{i} \\
\hspace{1.5em} x_{P,i} = x_T \\
\hspace{1.5em} y_{P,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)} \\
\hspace{1.5em} \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) = y_{A,i} - y_{P,i} \\
\hspace{1.5em} \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{P,i} \\
\hspace{1.5em} (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) = 2 y_{\mathsf{A},i} \\
\hspace{1.5em} \lambda_{2,i}^2 = x_{A,i-1} + x_{R,i} + x_{A,i} \\
\hspace{1.5em} \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A,i-1}, \\
\end{array}$
where $x_{R,i} = (\lambda_{1,i}^2 - x_{A,i} - x_T).$ After substitution of $x_{P,i}, y_{P,i}, x_{R,i}, y_{A,i}$, and $y_{A,i-1}$, this becomes:
Initialize $A_{254} = [2] T.$
$\begin{array}{l}
\text{Initialize } A_{254} = [2] T. \\
\\
\text{for } i \text{ from } 254 \text{ down to } 4: \\
\hspace{1.5em} \text{// let } \mathbf{k}_{i} = \mathbf{z}_{i} - 2\mathbf{z}_{i+1} \\
\hspace{1.5em} \text{// let } y_{A,i} = \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2} \\[2ex]
\hspace{1.5em} (\mathbf{k}_i)(\mathbf{k}_i-1) = 0 \\
\hspace{1.5em} \lambda_{1,i} \cdot (x_{A,i} - x_T) = y_{A,i} - (2 \mathbf{k}_i - 1) \cdot y_T \\
\hspace{1.5em} \lambda_{2,i}^2 = x_{A,i-1} + \lambda_{1,i}^2 - x_T \\[1ex]
\hspace{1.5em} \begin{cases}
\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A, i-1}, &\text{if } i > 4 \\[0.5ex]
\lambda_{2,4} \cdot (x_{A,4} - x_{A,3}) = y_{A,4} + y_{A,3}^\text{witnessed}, &\text{if } i = 4.
\end{cases}
\end{array}$
for $i$ from $254$ down to $4$:
$$
\begin{aligned}
&\texttt{// let } \mathbf{k}_{i} = \mathbf{z}_{i} - 2\mathbf{z}_{i+1}\\
&\texttt{// let } y_{A,i} = \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2}\\
&(\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\
&\lambda_{1,i} \cdot (x_{A,i} - x_T) = y_{A,i} - (2 \mathbf{k}_i - 1) \cdot y_T\\
&\lambda_{2,i}^2 = x_{A,i-1} + \lambda_{1,i}^2 - x_T\\
\end{aligned}
$$
$$
\begin{cases}
\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A, i-1}, &\text{if } i > 4 \\[0.5ex]
\lambda_{2,4} \cdot (x_{A,4} - x_{A,3}) = y_{A,4} + y_{A,3}^\text{witnessed}, &\text{if } i = 4.
\end{cases}
$$
Here, $y_{A,3}^\text{witnessed}$ is assigned to a cell. This is unlike previous $y_{A,i}$'s, which were implicitly derived from $\lambda_{1,i}, \lambda_{2,i}, x_{A,i}, x_T$, but never actually assigned.
The bits $\mathbf{k}_{3 \dots 1}$ are used in three further steps, using [complete addition](./addition.md#Complete-addition):
for $i$ from $3$ down to $1$:
$\begin{array}{ll}
\hspace{2em}& \texttt{// let } \mathbf{k}_{i} = \mathbf{z}_{i} - 2\mathbf{z}_{i+1}\\
\hspace{2em}& (\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\
\hspace{2em}& (x_{A,i-1}, y_{A,i-1}) = \left((x_{A,i}, y_{A,i}) + (x_T, y_T)\right) + (x_{A,i}, y_{A,i})
$\begin{array}{l}
\text{for } i \text{ from } 3 \text{ down to } 1: \\
\hspace{1.5em} \text{// let } \mathbf{k}_{i} = \mathbf{z}_{i} - 2\mathbf{z}_{i+1} \\[0.5ex]
\hspace{1.5em} (\mathbf{k}_i)(\mathbf{k}_i-1) = 0 \\
\hspace{1.5em} (x_{A,i-1}, y_{A,i-1}) = \left((x_{A,i}, y_{A,i}) + (x_T, y_T)\right) + (x_{A,i}, y_{A,i})
\end{array}$
If the least significant bit is set $\mathbf{k_0} = 1,$ we return the accumulator $A$. Else, if $\mathbf{k_0} = 0,$ we return $A - T$ (also using complete addition).
If the least significant bit $\mathbf{k_0} = 1,$ we set $B = \mathcal{O},$ otherwise we set ${B = -T}$. Then we return ${A + B}$ using complete addition.
Let $B = \begin{cases}
(0, 0), &\text{ if } \mathbf{k_0} = 1,\\
(0, 0), &\text{ if } \mathbf{k_0} = 1, \\
(x_T, -y_T), &\text{ otherwise.}
\end{cases}$