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

Merge pull request #54 from zcash/book-ecc-gadget 

[book] Document ECC gadget in circuit
This commit is contained in:
ying tong 2021-07-09 22:18:16 +08:00 committed by GitHub
parent 74df35ce89 d9f134ac4b
commit 7b3a0c8a29
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 963 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
book/src/SUMMARY.md
View File

@ -17,4 +17,9 @@
- [Signatures](design/signatures.md)
- [Circuit](design/circuit.md)
- [Gadgets](design/circuit/gadgets.md)
- [Elliptic curve cryptography](design/circuit/gadgets/ecc.md)
- [Incomplete and complete addition](design/circuit/gadgets/ecc/addition.md)
- [Fixed-base scalar multiplication](design/circuit/gadgets/ecc/fixed-base-scalar-mul.md)
- [Variable-base scalar multiplication](design/circuit/gadgets/ecc/var-base-scalar-mul.md)
- [Sinsemilla](design/circuit/gadgets/sinsemilla.md)
- [Lookup Range Check](design/circuit/gadgets/lookup_range_check.md)

0
book/src/design/circuit/gadgets/ecc.md Normal file
View File

378
book/src/design/circuit/gadgets/ecc/addition.md Normal file
View File

@ -0,0 +1,378 @@
We will use formulae for curve arithmetic using affine coordinates on short Weierstrass curves,
derived from section 4.1 of [Hüseyin Hışıl's thesis](https://core.ac.uk/download/pdf/10898289.pdf).
## Incomplete addition
- Inputs: $P = (x_p, y_p), Q = (x_q, y_q)$
- Output: $R = P \;⸭\; Q = (x_r, y_r)$
The formulae from Hışıl's thesis are:
- $x_3 = \left(\frac{y_1 - y_2}{x_1 - x_2}\right)^2 - x_1 - x_2$
- $y_3 = \frac{y_1 - y_2}{x_1 - x_2} \cdot (x_1 - x_3) - y_1$
Rename:
- $(x_1, y_1)$ to $(x_q, y_q)$
- $(x_2, y_2)$ to $(x_p, y_p)$
- $(x_3, y_3)$ to $(x_r, y_r)$.
Let $\lambda = \frac{y_q - y_p}{x_q - x_p} = \frac{y_p - y_q}{x_p - x_q}$, which we implement as
$\lambda \cdot (x_p - x_q) = y_p - y_q$
Also,
- $x_r = \lambda^2 - x_q - x_p$
- $y_r = \lambda \cdot (x_q - x_r) - y_q$
which is equivalent to
- $x_r + x_q + x_p = \lambda^2$
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
\end{array}
$
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$
## 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
\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$.)
$$
\begin{aligned}
P + Q &= R\\
(x_p, y_p) + (x_q, y_q) &= (x_r, y_r) \\
\lambda &= \frac{y_q - y_p}{x_q - x_p} \\
x_r &= \lambda^2 - x_p - x_q \\
y_r &= \lambda(x_p - x_r) - y_p
\end{aligned}
$$
For the doubling case, Hışıl's thesis tells us that $\lambda$ has to
instead be computed as $\frac{3x^2}{2y}$.
Define $\mathsf{inv0}(x) = \begin{cases} 0, &\text{if } x = 0 \\ 1/x, &\text{otherwise.} \end{cases}$
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}$
### Constraints
$$
\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
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 \\
6 & q_\mathit{add} \cdot x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda^2 - x_p - x_q - x_r) &=& 0 & x_p \neq 0 \wedge x_q \neq 0 \wedge y_q \neq -y_p \implies x_r = \lambda^2 - x_p - x_q \\
6 & q_\mathit{add} \cdot x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) &=& 0 & x_p \neq 0 \wedge x_q \neq 0 \wedge y_q \neq -y_p \implies y_r = \lambda \cdot (x_p - x_r) - y_p \\\hline
4 & q_\mathit{add} \cdot (1 - x_p \cdot \beta) \cdot (x_r - x_q) &=& 0 & x_p = 0 \implies x_r = x_q \\
4 & q_\mathit{add} \cdot (1 - x_p \cdot \beta) \cdot (y_r - y_q) &=& 0 & x_p = 0 \implies y_r = y_q \\\hline
4 & q_\mathit{add} \cdot (1 - x_q \cdot \gamma) \cdot (x_r - x_p) &=& 0 & x_q = 0 \implies x_r = x_p \\
4 & q_\mathit{add} \cdot (1 - x_q \cdot \gamma) \cdot (y_r - y_p) &=& 0 & x_q = 0 \implies y_r = y_p \\\hline
4 & q_\mathit{add} \cdot (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot x_r &=& 0 & x_q = x_p \wedge y_q = -y_p \implies x_r = 0 \\
4 & q_\mathit{add} \cdot (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot y_r &=& 0 & x_q = x_p \wedge y_q = -y_p \implies y_r = 0 \\\hline
\end{array}
$$
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 \\
\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)) \\
\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
\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
\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
\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).
\end{array}
$$
#### Propositions:
$
\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) \\
\end{array}
$
#### Test cases:
$(x_p, y_p) + (x_q, y_q) = (x_r, y_r)$
* $(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) \\
\end{array}
$
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution
* $(x, y) + (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} \\
\end{array}
$
- Soundness: $(x_r, y_r) = (x_p, y_p)$ is the only solution
* $(0, 0) + (x, y)$
- 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} \\
\end{array}
$
- Soundness: $(x_r, y_r) = (x_q, y_q)$ is the only solution
* $(x, y) + (x, y)$
- 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} \\
\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)$
- 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) \\
\end{array}
$
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution
* $(\zeta x, y) + (x, y)$
- 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 \\
\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.$

216
book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md Normal file
View File

@ -0,0 +1,216 @@
# Fixed-base scalar multiplication
There are $6$ fixed bases in the Orchard protocol:
- $\mathcal{K}^{\mathsf{Orchard}}$, used in deriving the nullifier;
- $\mathcal{G}^{\mathsf{Orchard}}$, used in spend authorization;
- $\mathcal{R}$ base for $\mathsf{NoteCommit}^{\mathsf{Orchard}}$;
- $\mathcal{V}$ and $\mathcal{R}$ bases for $\mathsf{ValueCommit}^{\mathsf{Orchard}}$; and
- $\mathcal{R}$ base for $\mathsf{Commit}^{\mathsf{ivk}}$.
## Witness scalar
In most cases, we multiply the fixed bases by $255-$bit scalars from $\mathbb{F}_q$. We decompose a full-width scalar $\alpha$ into $85$ $3$-bit windows:
$$\alpha = k_0 + k_1 \cdot (2^3)^1 + \cdots + k_{84} \cdot (2^3)^{84}, k_i \in [0..2^3).$$
The scalar multiplication will be computed correctly for $k_{0..84}$ representing any integer in the range $[0, 2^{255})$.
If $k_{0..84}$ is witnessed directly then no issue of canonicity arises. If the scalar is given as a base field element, then
care must be taken to ensure a canonical representation, since $2^{255} > p$. This occurs, for example, in the scalar
multiplication for the nullifier computation of the Action circuit.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
9 & q_\text{scalar-fixed} \cdot 1 \cdot \left(\sum\limits_{i=0}^7{w - i}\right) = 0 \\\hline
\end{array}
$$
At the point of witnessing the scalar, we range-constrain each $3$-bit word of its decomposition.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
9 & q_\text{witness-scalar-fixed} \cdot \texttt{range\_check}(k_i, 8) = 0 \\\hline
\end{array}
$$
where $\texttt{range\_check}(k_i, \texttt{range}) = k_i \cdot (1 - k_i) \cdots (\texttt{range} - 1 - k_i).$
## Load fixed base
Then, we precompute multiples of the fixed base $B$ for each window. This takes the form of a window table: $M[0..85)[0..8)$ such that:
- for the first 84 rows $M[0..84)[0..8)$: $$M[w][k] = [(k+2) \cdot (2^3)^w]B$$
- in the last row $M[84][0..8)$: $$M[w][k] = [k \cdot (2^3)^w - \sum\limits_{j=0}^{83} 2^{3j+1}]B$$
The additional $(k + 2)$ term lets us avoid adding the point at infinity in the case $k = 0$. We offset these accumulated terms by subtracting them in the final window, i.e. we subtract $\sum\limits_{j=0}^{83} 2^{3j+1}$.
> Note: Although an offset of $(k + 1)$ would naively suffice, it introduces an edge case when $k_0 = 7, k_1= 0$.
> In this case, the window table entries evaluate to the same point:
> * $M[0][k_0] = [(7+1)*(2^3)^0]B = [8]B,$
> * $M[1][k_1] = [(0+1)*(2^3)^1]B = [8]B.$
>
> In fixed-base scalar multiplication, we sum the multiples of $B$ at each window (except the last) using incomplete addition.
> Since the point doubling case is not handled by incomplete addition, we avoid it by using an offset of $(k+2).$
For each window of fixed-base multiples $M[w] = (M[w][0], \cdots, M[w][7]), w \in [0..84)$:
- Define a Lagrange interpolation polynomial $\mathcal{L}_x(k)$ that maps $k \in [0..8)$ to the $x$-coordinate of the multiple $M[w][k]$, i.e.
$$
\mathcal{L}_x(k) = \begin{cases}
([(k + 2) \cdot (2^3)^w] B)_x &\text{for } w \in [0..84); \\
([k \cdot (2^3)^w - \sum\limits_{j=0}^{83} 2^{3j+1}] B)_x &\text{for } w = 84; \text{ and}
\end{cases}
$$
- Find a value $z_w$ such that $z_w + (M[w][k])_y$ is a square $u^2$ in the field, but the wrong-sign $y$-coordinate $z_w - (M[w][k])_y$ does not produce a square.
Repeating this for all $85$ windows, we end up with:
- an $85 \times 8$ table $\mathcal{L}_x$ storing $8$ coefficients interpolating the $x-$coordinate for each window. Each $x$-coordinate interpolation polynomial will be of the form
$$\mathcal{L}_x[w](k) = c_0 + c_1 \cdot k + c_2 \cdot k^2 + \cdots + c_7 \cdot k^7,$$
where $k \in [0..8), w \in [0..85)$ and $c_k$'s are the coefficients for each power of $k$; and
- a length-$85$ array $Z$ of $z_w$'s.
We load these precomputed values into fixed columns whenever we do fixed-base scalar multiplication in the circuit.
## Fixed-base scalar multiplication
Given a decomposed scalar $\alpha$ and a fixed base $B$, we compute $[\alpha]B$ as follows:
1. For each $k_w, w \in [0..85), k_w \in [0..8)$ in the scalar decomposition, witness the $x$- and $y$-coordinates $(x_w,y_w) = M[w][k_w].$
2. Check that $(x_w, y_w)$ is on the curve: $y_w^2 = x_w^3 + b$.
3. Witness $u_w$ such that $y_w + z_w = u_w^2$.
4. For all windows but the last, use [incomplete addition](./incomplete-add.md) to sum the $M[w][k_w]$'s, resulting in $[\alpha - k_{84} \cdot (2^3)^{84} + \sum\limits_{j=0}^{83} 2^{3j+1}]B$.
5. For the last window, use complete addition $M[83][k_{83}] + M[84][k_{84}]$ and return the final result.
> Note: complete addition is required in the final step to correctly map $[0]B$ to a representation of the point at infinity, $(0,0)$; and also to handle a corner case for which the last step is a doubling.
Constraints:
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
8 & q_\text{mul-fixed} \cdot \left( \mathcal{L}_x[w](k_w) - x_w \right) = 0 \\\hline
4 & q_\text{mul-fixed} \cdot \left( y_w^2 - x_w^3 - b \right) = 0 \\\hline
3 & q_\text{mul-fixed} \cdot \left( u_w^2 - y_w - Z[w] \right) = 0 \\\hline
\end{array}
$$
where $b = 5$ (from the Pallas curve equation).
### Fixed-base scalar multiplication with signed short exponent
This is used for $\mathsf{ValueCommit^{Orchard}}$. We want to compute $\mathsf{ValueCommit^{Orchard}_{rcv}}(\mathsf{v^{old}} - \mathsf{v^{new}}) = [\mathsf{v^{old}} - \mathsf{v^{new}}] \mathcal{V} + [\mathsf{rcv}] \mathcal{R}$, where
$$
-(2^{64}-1) \leq \mathsf{v^{old}} - \mathsf{v^{new}} \leq 2^{64}-1
$$
$\mathsf{v^{old}}$ and $\mathsf{v^{new}}$ are each already constrained to $64$ bits (by their use as inputs to $\mathsf{NoteCommit^{Orchard}}$).
Witness the sign $s$ and magnitude $m$ such that
$$
s \in \{-1, 1\} \\
m \in [0, 2^{64}) \\
\mathsf{v^{old}} - \mathsf{v^{new}} = s \cdot m
$$
Then compute $P = [m] \mathcal{V}$, and conditionally negate $P$ using $(x, y) \mapsto (x, s \cdot y)$.
We compute the window table in a similar way to full-width fixed-base scalar multiplication,
but with only $\mathsf{ceil}(64 / 3) = 22$ windows:
$$\alpha_\textsf{short} = k_0 + k_1 \cdot (2^3)^1 + \cdots + k_{21} \cdot (2^3)^{21}, k_i \in [0..2^3).$$
In addition to the $21$ full-width $3$-bit constraints, we have two additional constraints:
$$
\begin{array}{|c|l|l|}
\hline
\text{Degree} & \text{Constraint} & \text{Comment} \\\hline
3 & q_\text{scalar-fixed-short} \cdot \left(k_{21} \cdot (1 - k_{21})\right) = 0 & \text{The last window must be a single bit.}\\\hline
3 & q_\text{scalar-fixed-short} \cdot \left(s^2 - 1\right) = 0 &\text{The sign must be $1$ or $-1$.}\\\hline
\end{array}
$$
### Fixed-base scalar multiplication using base field element
We support using a base field element as the scalar in fixed-base multiplication.
This is used in
$\mathsf{DeriveNullifier_{nk}} = \mathsf{Extract}_\mathbb{P}\left(\left[(\mathsf{PRF_{nk}^{nfOrchard}}(\rho) + \psi) \bmod{q_\mathbb{P}}\right]\mathcal{K}^\mathsf{Orchard} + \mathsf{cm}\right)$: here, the scalar $$\left[(\mathsf{PRF_{nk}^{nfOrchard}}(\rho) + \psi) \bmod{q_\mathbb{P}}\right]$$ is the result of a base field addition.
Decompose the base field element $\alpha$ into three-bit windows using a running sum $z$, where $z_{i+1} = (z_i - a_i) / 2^3$ for $$\alpha = a_0 + 2^3 a_1 + ... + 2^{3 \cdot 84} a_{84}.$$ (This running sum $z$ is not to be confused with the $Z$ array used to check the $y$-coordinate of a fixed-base window.)
We set $z_0 = \alpha$, which means:
$$
\begin{aligned}
z_1 &= (\alpha - k_0) / 2^3, \text{ (subtract the lowest 3 bits)}\\
&= k_1 + 2^3 k_2 + ... + 2^{3 \cdot 83} k_{84},\\
z_2 &= (z_1 - k_1) / 2^3\\
&= k_2 + 2^3 k_3 + ... + 2^{3 \cdot 82} k_{84},\\
&\cdots,\\
z_{84} &= k_{84}\\
z_{85} &= (z_{84} - k_{84}) / 2^3\\
&= 0.
\end{aligned}
$$
We must range-constrain the difference at each step of the running sum. We also constrain the final output of the running sum to be $0$.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
9 & q_\text{decompose-base-field} \cdot \texttt{range\_check}(z_i - z_{i+1} \cdot 2^3, 2^3) = 0 \\\hline
2 & q_\text{decompose-base-field} \cdot z_{85} = 0 \\\hline
\end{array}
$$
We also enforce canonicity of this decomposition. That is, we want to check that $0 \leq \alpha < p,$ where $p$ the is Pallas base field modulus $$p = 2^{254} + t_p = 2^{254} + 45560315531419706090280762371685220353.$$ Note that $t_p < 2^{130}.$
To do this, we decompose $\alpha$ into three pieces: $$\alpha = \alpha_0 \text{ (252 bits) } \,||\, \alpha_1 \text{ (2 bits) } \,||\, \alpha_2 \text{ (1 bit) }.$$
We check the correctness of this decomposition by:
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
5 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_1, 2^2) = 0 \\\hline
3 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_2, 2^1) = 0 \\\hline
2 & q_\text{canon-base-field} \cdot \left(z_{84} - (\alpha_1 + \alpha_2 \cdot 2^2)\right) = 0 \\\hline
\end{array}
$$
If the MSB $\alpha_2 = 0$ is not set, then $\alpha < 2^{254} < p.$ However, in the case where $\alpha_2 = 1$, we must check:
- $\alpha_2 = 1 \implies \alpha_1 = 0;$
- $\alpha_2 = 1 \implies \alpha_0 < t_p$:
- $\alpha_2 = 1 \implies 0 \leq \alpha_0 < 2^{130}$,
- $\alpha_2 = 1 \implies 0 \leq \alpha_0 + 2^{130} - t_p < 2^{130}$
To check that $0 \leq \alpha_0 < 2^{130},$ we make use of the three-bit running sum decomposition:
- Firstly, we constrain $\alpha_0$ to be a $132$-bit value by enforcing its high $120$ bits to be all-zero. We can get $\textsf{alpha\_0\_hi\_120}$ from the decomposition:
$$
\begin{aligned}
z_{44} &= k_{44} + 2^3 k_{45} + \cdots + 2^{3 \cdot (84 - 44)} k_{84}\\
\implies \textsf{alpha\_0\_hi\_120} &= z_{44} - 2^{3 \cdot (84 - 44)} k_{84}\\
&= z_{44} - 2^{3 \cdot (40)} z_{84}.
\end{aligned}
$$
- Then, we constrain bits $130..\!\!=\!\!131$ of $\alpha_0$ to be zeroes; in other words, we constrain the three-bit word $k_{43} = \alpha[129..\!\!=\!\!131] = \alpha_0[129..\!\!=\!\!131] \in \{0, 1\}.$ We make use of the running sum decomposition to obtain $k_{43} = z_{43} - z_{44} \cdot 2^3.$
Define $\alpha'_0 = \alpha_0 + 2^{130} - t_p$. To check that $0 \leq \alpha'_0 < 2^{130},$ we use 13 ten-bit [lookups](../lookup_range_check.md), where we constrain the $z_{13}$ running sum output of the lookup to be $0$ if $\alpha_2 = 1.$
$$
\begin{array}{|c|l|l|}
\hline
\text{Degree} & \text{Constraint} & \text{Comment} \\\hline
3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot \alpha_1 = 0 & \alpha_2 = 1 \implies \alpha_1 = 0 \\\hline
3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot \textsf{alpha\_0\_hi\_120} = 0 & \text{Constrain $\alpha_0$ to be a $132$-bit value} \\\hline
4 & q_\text{canon-base-field} \cdot \alpha_2 \cdot k_{43} \cdot (1 - k_{43}) = 0 & \text{Constrain $\alpha_0[130..\!\!=\!\!131]$ to $0$} \\\hline
3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot z_{13}(\texttt{lookup}(\alpha_0', 13)) = 0 & \alpha_2 = 1 \implies 0 \leq \alpha'_0 < 2^{130}\\\hline
\end{array}
$$
## Layout
$$
\begin{array}{|c|c|c|c|c|c|c|c|}
\hline
x_P & y_P & x_{QR} & y_{QR} & u & \text{window} & L_{0..=7} & \textsf{fixed\_z} \\\hline
x_{P,0} & y_{P,0} & & & u_0 & \text{window}_0 & L_{0..=7,0} & \textsf{fixed\_z}_0 \\\hline
x_{P,1} & y_{P,1} & x_{Q,1} = x_{P,0} & y_{Q,1} = y_{P,0} & u_1 & \text{window}_1 & L_{0..=7,1} & \textsf{fixed\_z}_1 \\\hline
x_{P,2} & y_{P,2} & x_{Q,2} = x_{R,1} & y_{Q,2} = y_{R,1} & u_2 & \text{window}_2 & L_{0..=7,1} & \textsf{fixed\_z}_2 \\\hline
\vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots \\\hline
\end{array}
$$
Note: this doesn't include the last row that uses [complete addition](./addition.md#Complete-addition). In the implementation this is allocated in a different region.

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

@ -0,0 +1,337 @@
# Variable-base scalar multiplication
In the Orchard circuit we need to check $\mathsf{pk_d} = [\mathsf{ivk}] \mathsf{g_d}$ where $\mathsf{ivk} \in [0, p)$ and the scalar field is $\mathbb{F}_q$ with $p < q$.
We have $p = 2^{254} + t_p$ and $q = 2^{254} + t_q$, for $t_p, t_q < 2^{128}$.
## Witness scalar
We're trying to compute $[\alpha] T$ for $\alpha \in [0, q)$. Set $k = \alpha + t_q$ and $n = 254$. Then we can compute
$\begin{array}{cl}
[2^{254} + (\alpha + t_q)] T &= [2^{254} + (\alpha + t_q) - (2^{254} + t_q)] T \\
&= [\alpha] T
\end{array}$
provided that $\alpha + t_q \in [0, 2^{n+1})$, i.e. $\alpha < 2^{n+1} - t_q$ which covers the whole range we need because in fact $2^{255} - t_q > q$.
Thus, given a scalar $\alpha$, we witness the boolean decomposition of $k = \alpha + t_q.$ (We use big-endian bit order for convenient input into the variable-base scalar multiplication algorithm.)
$$k = k_{254} \cdot 2^{254} + k_{253} \cdot 2^{253} + \cdots + k_0.$$
## Variable-base scalar multiplication
We use an optimized double-and-add algorithm, copied from ["Faster variable-base scalar multiplication in zk-SNARK circuits"](https://github.com/zcash/zcash/issues/3924) with some variable name changes:
```ignore
Acc := [2] T
for i from n-1 down to 0 {
P := k_{i+1} ? T : −T
Acc := (Acc + P) + Acc
}
return (k_0 = 0) ? (Acc - T) : Acc
```
It remains to check that the x-coordinates of each pair of points to be added are distinct.
When adding points in a prime-order group, we can rely on Theorem 3 from Appendix C of the [Halo paper](https://eprint.iacr.org/2019/1021.pdf), which says that if we have two such points with nonzero indices wrt a given odd-prime order base, where the indices taken in the range $-(q-1)/2..(q-1)/2$ are distinct disregarding sign, then they have different x-coordinates. This is helpful, because it is easier to reason about the indices of points occurring in the scalar multiplication algorithm than it is to reason about their x-coordinates directly.
So, the required check is equivalent to saying that the following "indexed version" of the above algorithm never asserts:
```ignore
acc := 2
for i from n-1 down to 0 {
p = k_{i+1} ? 1 : −1
assert acc ≠ ± p
assert (acc + p) ≠ acc // X
acc := (acc + p) + acc
assert 0 < acc ≤ (q-1)/2
}
if k_0 = 0 {
assert acc ≠ 1
acc := acc - 1
}
```
The maximum value of `acc` is:
```ignore
<--- n 1s --->
1011111...111111
= 1100000...000000 - 1
```
= $2^{n+1} + 2^n - 1$
> The assertion labelled X obviously cannot fail because $p \neq 0$. It is possible to see that acc is monotonically increasing except in the last conditional. It reaches its largest value when $k$ is maximal, i.e. $2^{n+1} + 2^n - 1$.
So to entirely avoid exceptional cases, we would need $2^{n+1} + 2^n - 1 < (q-1)/2$. But we can use $n$ larger by $c$ if the last $c$ iterations use [complete addition](./addition.md#Complete-addition).
The first $i$ for which the algorithm using **only** incomplete addition fails is going to be $252$, since $2^{252+1} + 2^{252} - 1 > (q - 1)/2$. We need $n = 254$ to make the wraparound technique above work.
```python
sage: q = 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
sage: 2^253 + 2^252 - 1 < (q-1)//2
False
sage: 2^252 + 2^251 - 1 < (q-1)//2
True
```
So the last three iterations of the loop ($i = 2..0$) need to use [complete addition](./addition.md#Complete-addition), as does the conditional subtraction at the end. Writing this out using ⸭ for incomplete addition (as we do in the spec), we have:
```ignore
Acc := [2] T
for i from 253 down to 3 {
P := k_{i+1} ? T : −T
Acc := (Acc ⸭ P) ⸭ Acc
}
for i from 2 down to 0 {
P := k_{i+1} ? T : −T
Acc := (Acc + P) + Acc // complete addition
}
return (k_0 = 0) ? (Acc + (-T)) : Acc // complete addition
```
## Constraint program for optimized double-and-add (incomplete addition)
Define a running sum $\mathbf{z_j} = \sum_{i=j}^{n} (\mathbf{k}_{i} \cdot 2^{i-j})$, where $n = 254$ and:
$$
\begin{aligned}
&\mathbf{z}_{n+1} = 0,\\
&\mathbf{z}_{n} = \mathbf{k}_{n}, \hspace{2em}\text{(most significant bit)}\\
&\mathbf{z}_0 = k.\\
\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},\\
\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.$
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})
\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).
Let $B = \begin{cases}
(0, 0), &\text{ if } \mathbf{k_0} = 1,\\
(x_T, -y_T), &\text{ otherwise.}
\end{cases}$
Output $(x_{A,0}, y_{A,0}) + B$.
(Note that $(0, 0)$ represents $\mathcal{O}$.)
### Circuit design
We need six advice columns to witness $(x_T, y_T, \lambda_1, \lambda_2, x_{A,i}, \mathbf{z}_i)$. However, since $(x_T, y_T)$ are the same, we can perform two incomplete additions in a single row, reusing the same $(x_T, y_T)$. We split the scalar bits used in incomplete addition into $hi$ and $lo$ halves and process them in parallel. This means that we effectively have two for loops:
- the first, covering the $hi$ half for $i$ from $254$ down to $130$, with a special case at $i = 130$; and
- the second, covering the $lo$ half for the remaining $i$ from $129$ down to $4$, with a special case at $i = 4$.
$$
\begin{array}{|c|c|c|c|c|c|c|c|c|c|c|c|}
\hline
x_T & y_T & z^{hi} & x_A^{hi} & \lambda_1^{hi} & \lambda_2^{hi} &q_{mul}^{hi}& z^{lo} & x_A^{lo} & \lambda_1^{lo} & \lambda_2^{lo} &q_{mul}^{lo}\\\hline
& & \mathbf{z}_{255} = 0 & & y_{A,254}=2[T]_y & & 1 & \mathbf{z}_{130} & & y_{A,129} & & 1 \\\hline
x_T & y_T & \mathbf{z}_{254} & x_{A,254} = 2[T]_x & \lambda_{1,254} & \lambda_{2,254} & 2 & \mathbf{z}_{129} & x_{A,129} & \lambda_{1,129} & \lambda_{2,129} & 2 \\\hline
x_T & y_T & \mathbf{z}_{253} & x_{A,253} & \lambda_{1,253} & \lambda_{2,253} & 2 & \mathbf{z}_{128} & x_{A,128} & \lambda_{1,128} & \lambda_{2,128} & 2 \\\hline
\vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots \\\hline
x_T & y_T & \mathbf{z}_{130} & x_{A,130} & \lambda_{1,130} & \lambda_{2,130} & 3 & \mathbf{z}_5 & x_{A,5} & \lambda_{1,5} & \lambda_{2,5} & 2 \\\hline
& & & x_{A,129} & y_{A,129} & & & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} & 3 \\\hline
& & & & & & & & x_{A,3} & y_{A,3} & & \\\hline
\end{array}
$$
For each $hi$ and $lo$ half, we have three sets of gates. Note that $i$ is going from $255..=3$; $i$ is NOT indexing the rows.
#### $q_{mul} = 1$
This gate is only used on the first row (before the for loop). We check that $\lambda_1, \lambda_2$ are initialized to values consistent with the initial $y_A.$
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
5 & q_{mul}^{one} \cdot \left(y_{A,n}^\text{witnessed} - y_{A,n}\right) = 0 \\\hline
\end{array}
$$
where
$$
\begin{aligned}
q_{mul}^{one} &= q_{mul} \cdot (2 - q_{mul}) \cdot (3 - q_{mul}),\\
y_{A,n} &= \frac{(\lambda_{1,n} + \lambda_{2,n}) \cdot (x_{A,n} - (\lambda_{1,n}^2 - x_{A,n} - x_T))}{2},\\
y_{A,n}^\text{witnessed} &\text{ is witnessed.}
\end{aligned}
$$
#### $q_{mul} = 2$
This gate is used on all rows corresponding to the for loop except the last.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
4 & q_{mul}^{two} \cdot \left(x_{T,cur} - x_{T,next}\right) = 0 \\\hline
4 & q_{mul}^{two} \cdot \left(y_{T,cur} - y_{T,next}\right) = 0 \\\hline
5 & q_{mul}^{two} \cdot \mathbf{k}_i \cdot (\mathbf{k}_i - 1) = 0, \text{ where } \mathbf{k}_i = \mathbf{z}_{i} - 2\mathbf{z}_{i+1} \\\hline
6 & q_{mul}^{two} \cdot \left(\lambda_{1,i} \cdot (x_{A,i} - x_{T,i}) - y_{A,i} + (2\mathbf{k}_i - 1) \cdot y_{T,i}\right) = 0 \\\hline
5 & q_{mul}^{two} \cdot \left(\lambda_{2,i}^2 - x_{A,i-1} - \lambda_{1,i}^2 + x_{T,i}\right) = 0 \\\hline
5 & q_{mul}^{two} \cdot \left(\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) - y_{A,i} - y_{A,i-1}\right) = 0 \\\hline
\end{array}
$$
where
$$
\begin{aligned}
q_{mul}^{two} &= q_{mul} \cdot (1 - q_{mul}) \cdot (3 - q_{mul}),\\
y_{A,i} &= \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2}, \\
y_{A,i-1} &= \frac{(\lambda_{1,i-1} + \lambda_{2,i-1}) \cdot (x_{A,i-1} - (\lambda_{1,i-1}^2 - x_{A,i-1} - x_T))}{2}, \\
\end{aligned}
$$
#### $q_{mul} = 3$
This gate is used on the final iteration of the for loop, handling the special case where we check that the output $y_A$ has been witnessed correctly.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
5 & q_{mul}^{three} \cdot \mathbf{k}_i \cdot (\mathbf{k}_i - 1) = 0, \text{ where } \mathbf{k}_i = \mathbf{z}_{i} - 2\mathbf{z}_{i+1} \\\hline
6 & q_{mul}^{three} \cdot \left(\lambda_{1,i} \cdot (x_{A,i} - x_{T,i}) - y_{A,i} + (2\mathbf{k}_i - 1) \cdot y_{T,i}\right) = 0 \\\hline
5 & q_{mul}^{three} \cdot \left(\lambda_{2,i}^2 - x_{A,i-1} - \lambda_{1,i}^2 + x_{T,i}\right) = 0 \\\hline
5 & q_{mul}^{three} \cdot \left(\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) - y_{A,i} - y_{A,i-1}^\text{witnessed}\right) = 0 \\\hline
\end{array}
$$
where
$$
\begin{aligned}
q_{mul}^{three} &= q_{mul} \cdot (1 - q_{mul}) \cdot (2 - q_{mul}),\\
y_{A,i} &= \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2},\\
y_{A,i-1}^\text{witnessed} &\text{ is witnessed.}
\end{aligned}
$$
## Overflow check
$\mathbf{z}_i$ cannot overflow for any $i \geq 1$, because it is a weighted sum of bits only up to $2^{n-1} = 2^{253}$, which is smaller than $p$ (and also $q$).
However, $\mathbf{z}_0 = \alpha + t_q$ *can* overflow $[0, p)$.
Since overflow can only occur in the final step that constrains $\mathbf{z}_0 = 2 \cdot \mathbf{z}_1 + \mathbf{k}_0$, we have $\mathbf{z}_0 = k \pmod{p}$. It is then sufficient to also check that $\mathbf{z}_0 = \alpha + t_q \pmod{p}$ (so that $k = \alpha + t_q \pmod{p}$) and that $k \in [t_q, p + t_q)$. These conditions together imply that $k = \alpha + t_q$ as an integer, and so $2^{254} + k = \alpha \pmod{q}$ as required.
> Note: the bits $\mathbf{k}_{254..0}$ do not represent a value reduced modulo $q$, but rather a representation of the unreduced $\alpha + t_q$.
### Optimized check for $k \in [t_q, p + t_q)$
Since $t_p + t_q < 2^{130}$, we have $$[t_q, p + t_q) = [t_q, t_q + 2^{130}) \;\cup\; [2^{130}, 2^{254}) \;\cup\; \big([2^{254}, 2^{254} + 2^{130}) \;\cap\; [p + t_q - 2^{130}, p + t_q)\big).$$
We may assume that $k = \alpha + t_q \pmod{p}$.
Therefore,
$\begin{array}{rcl}
k \in [t_q, p + t_q) &\Leftrightarrow& \big(k \in [t_q, t_q + 2^{130}) \;\vee\; k \in [2^{130}, 2^{254})\big) \;\vee\; \\
& & \big(k \in [2^{254}, 2^{254} + 2^{130}) \;\wedge\; k \in [p + t_q - 2^{130}, p + t_q)\big) \\
\\
&\Leftrightarrow& \big(\mathbf{k}_{254} = 0 \implies (k \in [t_q, t_q + 2^{130}) \;\vee\; k \in [2^{130}, 2^{254}))\big) \;\wedge \\
& & \big(\mathbf{k}_{254} = 1 \implies (k \in [2^{254}, 2^{254} + 2^{130}) \;\wedge\; k \in [p + t_q - 2^{130}, p + t_q)\big) \\
\\
&\Leftrightarrow& \big(\mathbf{k}_{254} = 0 \implies (\alpha \in [0, 2^{130}) \;\vee\; k \in [2^{130}, 2^{254})\big) \;\wedge \\
& & \big(\mathbf{k}_{254} = 1 \implies (k \in [2^{254}, 2^{254} + 2^{130}) \;\wedge\; (\alpha + 2^{130}) \bmod p \in [0, 2^{130}))\big) \;\;Ⓐ
\end{array}$
> Given $k \in [2^{254}, 2^{254} + 2^{130})$, we prove equivalence of $k \in [p + t_q - 2^{130}, p + t_q)$ and $(\alpha + 2^{130}) \bmod p \in [0, 2^{130})$ as follows:
> * shift the range by $2^{130} - p - t_q$ to give $k + 2^{130} - p - t_q \in [0, 2^{130})$;
> * observe that $k + 2^{130} - p - t_q$ is guaranteed to be in $[2^{130} - t_p - t_q, 2^{131} - t_p - t_q)$ and therefore cannot overflow or underflow modulo $p$;
> * using the fact that $k = \alpha + t_q \pmod{p}$, observe that $(k + 2^{130} - p - t_q) \bmod p = (\alpha + t_q + 2^{130} - p - t_q) \bmod p = (\alpha + 2^{130}) \bmod p$.
>
> (We can see in a different way that this is correct by observing that it checks whether $\alpha \bmod p \in [p - 2^{130}, p)$, so the upper bound is aligned as we would expect.)
Now, we can continue optimizing from $Ⓐ$:
$\begin{array}{rcl}
k \in [t_q, p + t_q) &\Leftrightarrow& \big(\mathbf{k}_{254} = 0 \implies (\alpha \in [0, 2^{130}) \;\vee\; k \in [2^{130}, 2^{254})\big) \;\wedge \\
& & \big(\mathbf{k}_{254} = 1 \implies (k \in [2^{254}, 2^{254} + 2^{130}) \;\wedge\; (\alpha + 2^{130}) \bmod p \in [0, 2^{130}))\big) \\
\\
&\Leftrightarrow& \big(\mathbf{k}_{254} = 0 \implies (\alpha \in [0, 2^{130}) \;\vee\; \mathbf{k}_{253..130} \text{ are not all } 0)\big) \;\wedge \\
& & \big(\mathbf{k}_{254} = 1 \implies (\mathbf{k}_{253..130} \text{ are all } 0 \;\wedge\; (\alpha + 2^{130}) \bmod p \in [0, 2^{130}))\big)
\end{array}$
Constraining $\mathbf{k}_{253..130}$ to be all-$0$ or not-all-$0$ can be implemented almost "for free", as follows.
Recall that $\mathbf{z}_i = \sum_{h=i}^{n} (\mathbf{k}_{h} \cdot 2^{h-i})$, so we have:
$\begin{array}{rcl}
\mathbf{z}_{130} &=& \sum_{h=130}^{254} (\mathbf{k}_h \cdot 2^{h-130}) \\
\mathbf{z}_{130} &=& \mathbf{k}_{254} \cdot 2^{254-130} + \sum_{h=130}^{253} (\mathbf{k}_h \cdot 2^{h-130}) \\
\mathbf{z}_{130} - \mathbf{k}_{254} \cdot 2^{124} &=& \sum_{h=130}^{253} (\mathbf{k}_h \cdot 2^{h-130})
\end{array}$
So $\mathbf{k}_{253..130}$ are all $0$ exactly when $\mathbf{z}_{130} = \mathbf{k}_{254} \cdot 2^{124}$.
Finally, we can merge the $130$-bit decompositions for the $\mathbf{k}_{254} = 0$ and $\mathbf{k}_{254} = 1$ cases by checking that $(\alpha + \mathbf{k}_{254} \cdot 2^{130}) \bmod p \in [0, 2^{130})$.
### Overflow check constraints
Let $s = \alpha + \mathbf{k}_{254} \cdot 2^{130}$. The constraints for the overflow check are:
$$
\begin{aligned}
\mathbf{z}_0 &= \alpha + t_q \pmod{p} \\
\mathbf{k}_{254} = 1 \implies \big(\mathbf{z}_{130} &= 2^{124} \;\wedge\; s \bmod p \in [0, 2^{130})\big) \\
\mathbf{k}_{254} = 0 \implies \big(\mathbf{z}_{130} &\neq 0 \;\vee\; s \bmod p \in [0, 2^{130})\big)
\end{aligned}
$$
Define $\mathsf{inv0}(x) = \begin{cases} 0, &\text{if } x = 0 \\ 1/x, &\text{otherwise.} \end{cases}$
Witness $\eta = \mathsf{inv0}(\mathbf{z}_{130})$, and decompose $s \bmod p$ as $\mathbf{s}_{129..0}$.
Then the needed gates are:
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
2 & q_\text{mul}^\text{overflow} \cdot \left(s - (\alpha + \mathbf{k}_{254} \cdot 2^{130})\right) = 0 \\\hline
2 & q_\text{mul}^\text{overflow} \cdot \left(\mathbf{z}_0 - \alpha - t_q\right) = 0 \\\hline
3 & q_\text{mul}^\text{overflow} \cdot \left(\mathbf{k}_{254} \cdot (\mathbf{z}_{130} - 2^{124})\right) = 0 \\\hline
3 & q_\text{mul}^\text{overflow} \cdot \left(\mathbf{k}_{254} \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}\right) = 0 \\\hline
5 & q_\text{mul}^\text{overflow} \cdot \left((1 - \mathbf{k}_{254}) \cdot (1 - \mathbf{z}_{130} \cdot \eta) \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}\right) = 0 \\\hline
\end{array}
$$
where $(s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}$ can be computed by another running sum. Note that the factor of $1/2^{130}$ has no effect on the constraint, since the RHS is zero.
#### Running sum range check
We make use of a $10$-bit [lookup range check](../lookup_range_check.md) in the circuit to subtract the low $130$ bits of $\mathbf{s}$. The range check subtracts the first $13 \cdot 10$ bits of $\mathbf{s},$ and right-shifts the result to give $(s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}.$

27
book/src/design/circuit/gadgets/lookup_range_check.md Normal file
View File

@ -0,0 +1,27 @@
# Lookup decomposition
This gadget makes use of a $K$-bit lookup table to decompose a field element $\alpha$ into $K$-bit words. Firstly, express $$\alpha = k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + \cdots,$$ where each $k_i$ a $K$-bit value.
We initialize the running sum $z_0 = \mathbf{s},$ and compute subsequent terms $z_i = \frac{z_{i - 1} - k_{i-1}}{2^{K}}.$ This gives us:
$$
\begin{aligned}
z_0 &= \alpha \\
&= k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + 2^{3K} \cdot k_3 + \cdots, \\
z_1 &= (z_0 - k_0) / 2^K \\
&= k_1 + 2^{K} \cdot k_2 + 2^{2K} \cdot k_3 + \cdots, \\
z_2 &= (z_1 - k_1) / 2^K \\
&= k_2 + 2^{K} \cdot k_3 + \cdots, \\
&\vdots
\end{aligned}
$$
Each $K$-bit word $k_i = z_i - 2^K \cdot z_{i+1}$ is range-constrained by a lookup in the $K$-bit table. This gadget takes in $\alpha, n$ and returns $(z_0, z_1, \cdots, z_n).$
## Strict mode
Strict mode constrains the running sum output $z_{n}$ to be zero, thus range-constraining the field element to be within $n \cdot K$ bits.
## Short range check
Using two $K$-bit lookups, we can range-constrain a field element $\alpha$ to be $n$ bits, where $n \leq K.$ To do this:
1. Constrain $0 \leq \alpha < 2^K$ to be within $K$ bits using a $K$-bit lookup.
2. Constrain $0 \leq \alpha \cdot 2^{K - n} < 2^K$ to be within $K$ bits using a $K$-bit lookup.