Apply suggestions from code review

Co-authored-by: str4d <jack@electriccoin.co>
Co-authored-by: Daira Hopwood <daira@jacaranda.org>

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

@@ -1,5 +1,7 @@
 # Complete addition
 
+To implement complete addition inside the circuit, we need to check the following cases:
+
 $\begin{array}{rcll}
 \mathcal{O} &+& \mathcal{O} &= \mathcal{O} ✓\\
 \mathcal{O} &+& (x_q, y_q)  &= (x_q, y_q) ✓\\
@@ -9,7 +11,9 @@ $\begin{array}{rcll}
  (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$.)
+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}
@@ -26,27 +30,32 @@ 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
+\begin{array}{rcl|rcl}
+\text{Constraint} &&& \text{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 \\
+ (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 \wedge ¬C &\implies& x_r = \lambda^2 - x_p - x_q) \\
++ B \cdot (x_r - x_q) &=& 0 & \wedge (B &\implies& x_r = x_q) \\
+\\
+(1-B) \cdot (1-C) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) && & (¬B \wedge ¬C &\implies& y_r = \lambda \cdot (x_p - x_r) - y_p) \\
++ B \cdot (y_r - y_q) &=& 0 & \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
+Max degree: 4

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

@@ -12,18 +12,22 @@ In most cases, we multiply the fixed bases by $255-$bit scalars from $\mathbb{F}
 $$\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:
+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..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$
+- 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$.
+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, i.e. we subtract $\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.
+- 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) = \begin{cases}
+    ([(k + 1) \cdot 8^w] B)_x &\text{for } w \in [0..83]; \\
+    ([k \cdot (8)^w - \sum\limits_{j=0}^{83} (8)^j] 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
@@ -36,7 +40,7 @@ We load these precomputed values into fixed columns whenever we do fixed-base sc
 ## 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].$
+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$.

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

@@ -61,7 +61,8 @@ So to entirely avoid exceptional cases, we would need $2^{n+1} + 2^n - 1 < (q-1)
 
 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
+```python
+sage: q = 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
 sage: 2^253 + 2^252 - 1 < (q-1)//2
 False
 sage: 2^252 + 2^251 - 1 < (q-1)//2
@@ -93,10 +94,15 @@ We witness $x_{A,i}, x_{P,i}, x_{A, i+1},$ and $\lambda_{1, i}, \lambda_{2, i},
 
 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.
-$
+$$
+\begin{aligned}
+2 \cdot &\lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) - \big( \\
+    &\begin{aligned}
+        (\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})) \\
+    \end{aligned} \\
+\big) &= 0.
+\end{aligned}
+$$