[book] Document ECC gadget in circuit

book/src/SUMMARY.md

@@ -16,3 +16,9 @@
   - [Nullifiers](design/nullifiers.md)
   - [Signatures](design/signatures.md)
   - [Circuit](design/circuit.md)
+    - [Gadgets](design/circuit/gadgets.md)
+      - [Elliptic curve cryptography](design/circuit/gadgets/ecc.md)
+        - [Complete addition](design/circuit/gadgets/ecc/complete-add.md)
+        - [Incomplete addition](design/circuit/gadgets/ecc/incomplete-add.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)

book/src/design/circuit/gadgets/ecc.md

@@ -0,0 +1 @@
+# Elliptic Curve Cryptography

book/src/design/circuit/gadgets/ecc/complete-add.md

@@ -0,0 +1,52 @@
+# 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$.)
+
+$$
+\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, $\lambda$ has to instead be computed as $\frac{3x^2}{2y}$.
+
+Witness $\lambda, \alpha, \beta, \gamma, \delta, A, B, C, D$.
+
+$
+\begin{array}{rcl|l}
+&&& Meaning \\\hline
+            A \cdot (1-A) &=& 0 & A \in \mathbb{B} \\
+            B \cdot (1-B) &=& 0 & B \in \mathbb{B} \\
+            C \cdot (1-C) &=& 0 & C \in \mathbb{B} \\
+            D \cdot (1-D) &=& 0 & D \in \mathbb{B} \\
+ (x_q - x_p) \cdot \alpha &=& 1-A & x_q = x_p \implies A \\
+          x_p \cdot \beta &=& 1-B & x_p = 0 \implies B \\
+              B \cdot x_p &=& 0 & B \implies x_p = 0 \\
+         x_q \cdot \gamma &=& 1-C & x_q = 0 \implies C \\
+              C \cdot x_q &=& 0 & C \implies x_q = 0 \\
+ (y_q + y_p) \cdot \delta &=& 1-D & y_q = -y_p \implies D \\
+(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} \\
+A \cdot \left(2y_p \cdot \lambda - 3{x_p}^2\right) &=& 0 & A \wedge y_p \neq 0 \implies \lambda = \frac{3{x_p}^2}{2y_p} \\
+(1-B) \cdot (1-C) \cdot (\lambda^2 - x_p - x_q - x_r) + B \cdot (x_r - x_q) &=& 0 & (¬B \wedge ¬C \implies x_r = \lambda^2 - x_p - x_q) \wedge (B \implies x_r = x_q) \\
+(1-B) \cdot (1-C) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) + B \cdot (y_r - y_q) &=& 0 & (¬B \wedge ¬C \implies y_r = \lambda \cdot (x_p - x_r) - y_p) \wedge (B \implies y_r = y_q) \\
+      C \cdot (x_r - x_p) &=& 0 & C \implies x_r = x_p \\
+      C \cdot (y_r - y_p) &=& 0 & C \implies y_r = y_p \\
+              D \cdot x_r &=& 0 & D \implies x_r = 0 \\
+              D \cdot y_r &=& 0 & D \implies y_r = 0 \\
+\end{array}
+$
+
+Max degree: 4

book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md

@@ -0,0 +1,66 @@
+# Fixed-base scalar multiplication
+
+There are $5$ fixed bases in the Orchard protocol:
+- $\mathcal{K}^{\mathsf{Orchard}}$, used in deriving the nullifier;
+- $\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).$$
+
+## 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..84][0..7]$ such that:
+
+- for the first 84 rows $M[0..83][0..7]$: $M[w][k] = [(k+1) \cdot (2^3)^w]B$
+- in the last row $M[84][0..7]$: $M[w][k] = [k \cdot (2^3)^w - \sum\limits_{j=0}^{83} (2^3)^j]B$
+
+The additional $(k + 1)$ 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 $- \sum\limits_{j=0}^{83} (2^3)^j$.
+
+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..7]$ to the $x$-coordinate of the multiple $M[w][k]$, i.e. 
+    - $\mathcal{L}_x(k) = ([(k + 1) \cdot 8^w] B)_x$ for $w \in [0..83]$;
+    - $\mathcal{L}_x(k) = ([k \cdot (8)^w - \sum\limits_{j=0}^{83} (8)^j] B)_x$ for $w = 84$; and
+- 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..7], w \in [0..84]$ 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 such:
+
+1. For each $k_w, w \in [0..84], k_w \in [0..7]$ 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. Use [incomplete addition](./incomplete-add.md) to sum the $M[w][k_w]$'s, resulting in $[\alpha]B$.
+
+Constraints:
+ - $x_w = \mathcal{L}_x[w](k_w)$;
+ - $y_w^2 = x_w^3 + b,$ where $b = 5$ (from the Pallas curve equation);
+ - $u_w^2 = y_w + Z[w].$
+
+### 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 can reuse the window table from full-width fixed-base scalar multiplication, but with only $\mathsf{ceil}(64 / 3) = 22$ windows.

book/src/design/circuit/gadgets/ecc/incomplete-add.md

@@ -0,0 +1,12 @@
+# Incomplete addition
+Inputs: $P = (x_P, y_P), Q = (x_Q, y_Q)$
+Output: $A = P + Q = (x_A, y_A)$
+
+Formulae:
+- $\lambda \cdot (x_p - x_{q}) = y_p - y_{q}$
+- $x_{a} = \lambda^2 - x_{q} - x_p$
+- $y_{a} = \lambda(x_{q} - x_{a}) - y_{q}$
+
+Substituting for $\lambda$, we get the constraints:
+- $(x_{a} + x_{q} + x_p) \cdot (x_p - x_q)^2 - (y_p - y_{q})^2 = 0$
+- $(y_{a} + y_{q})(x_p - x_{q}) - (y_p - y_{q})(x_{q} - x_{a}) = 0$

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

@@ -0,0 +1,102 @@
+# 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 is (copied from ["Faster variable-base scalar multiplication in zk-SNARK circuits"](https://github.com/zcash/zcash/issues/3924), with some variable name changes):
+> 
+>     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 the large prime-order subgroup, 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:
+> 
+>     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:
+```
+    <--n 1s--->
+  1011111111111
+= 1100000000000 - 1
+```
+= $2^{n+1} + 2^n - 1$
+
+> The assertion labelled X obviously cannot fail because $u \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](./complete-add.md).
+
+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.
+
+> 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](./complete-add.md), as does the conditional subtraction at the end. Writing this out using ⸭ for incomplete addition (as we do in the spec), we have:
+
+    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
+For each round $i$ of incomplete addition, we are computing $A_{i+1} = A_i + P_i + A_i$, where $A = (x_a, y_a)$ is the accumulated sum and $P = (x_p, y_p)$ is the point we are adding.
+
+We compute $\lambda_{1, i}, \lambda_{2, i}$:
+- $\lambda_{1, i} = \frac{y_{A,i} - y_{P, i}}{x_{A,i} - x_{P, i}},$
+- $\lambda_{2, i} = \frac{y_{A, i} + y_{A, i+1}}{x_{A,i} - x_{A, i+1}}$
+
+and similarly for $\lambda_{1, i+1}, \lambda_{2, i+1}$.
+
+We witness $x_{A,i}, x_{P,i}, x_{A, i+1},$ and $\lambda_{1, i}, \lambda_{2, i}, \lambda_{1, i+1}, \lambda_{2, i+1},$ and specify the following constraints on them (copied from ["Faster variable-base scalar multiplication in zk-SNARK circuits"](https://github.com/zcash/zcash/issues/3924), with some variable name changes):
+
+1. $
+\lambda_{2,i}^2 - (x_{A,i+1} + (\lambda_{1,i}^2 - x_{A,i} - x_{P,i}) + x_{A,i}) = 0,
+$ and
+
+2. $
+2 \cdot \lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) - \big(
+        (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_{P,i})) +
+        (\lambda_{1,i+1} + \lambda_{2,i+1}) \cdot (x_{A,i+1} - (\lambda_{1,i+1}^2 - x_{A,i+1} - x_{P,i+1}))\big) = 0.
+$