From 3ed388e6bbe16f1a36d6cdf1c787542dad4afd21 Mon Sep 17 00:00:00 2001 From: Daira Hopwood Date: Tue, 27 Jul 2021 01:51:28 +0100 Subject: [PATCH 1/4] [book] src/design/circuit/gadgets/ecc/addition.md: formatting. Signed-off-by: Daira Hopwood --- .../design/circuit/gadgets/ecc/addition.md | 291 +++++++++--------- 1 file changed, 146 insertions(+), 145 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/addition.md b/book/src/design/circuit/gadgets/ecc/addition.md index 7a27f37e..f24e2625 100644 --- a/book/src/design/circuit/gadgets/ecc/addition.md +++ b/book/src/design/circuit/gadgets/ecc/addition.md @@ -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,117 @@ 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{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{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)) \\ + & \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. \\[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{Let } 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 } 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 } 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{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: } \\ + & \hspace{2em} x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0). \end{array} $$ @@ -239,13 +238,13 @@ $$ $ \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} $ @@ -269,6 +268,7 @@ $(x_p, y_p) + (x_q, y_q) = (x_r, y_r)$ - Soundness: $(x_r, y_r) = (0, 0)$ is the only solution * $(x, y) + (0, 0)$ + - Completeness: $ @@ -288,6 +288,7 @@ $(x_p, y_p) + (x_q, y_q) = (x_r, y_r)$ - Soundness: $(x_r, y_r) = (x_p, y_p)$ is the only solution * $(0, 0) + (x, y)$ + - Completeness: $ From 3dfefe0e85de27d49ffeaf89047913eb2916c9c7 Mon Sep 17 00:00:00 2001 From: Daira Hopwood Date: Tue, 13 Jul 2021 19:31:32 +0100 Subject: [PATCH 2/4] [book] src/design/circuit/gadgets/ecc/addition.md: correctness and clarity. Signed-off-by: Daira Hopwood --- .../design/circuit/gadgets/ecc/addition.md | 154 ++++++++---------- 1 file changed, 65 insertions(+), 89 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/addition.md b/book/src/design/circuit/gadgets/ecc/addition.md index f24e2625..ff24da0d 100644 --- a/book/src/design/circuit/gadgets/ecc/addition.md +++ b/book/src/design/circuit/gadgets/ecc/addition.md @@ -129,9 +129,7 @@ $$ \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{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:} \\ @@ -148,9 +146,10 @@ $$ & \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 } x_q = x_p \text{ and } 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{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. \\ @@ -168,11 +167,11 @@ $$ \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. \\[1.5ex] + & \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{Let } x_p \neq 0 \wedge x_q \neq 0 \wedge y_q \neq -y_p. \\[1.5ex] + & \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. \\ & \\ @@ -194,7 +193,8 @@ $$ & \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{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). \\ @@ -211,7 +211,8 @@ $$ & \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{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). \\ @@ -223,9 +224,10 @@ $$ \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{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{ then it must be that } 1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta = 0. \\ + & \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. \\ & \\ @@ -248,132 +250,106 @@ $ \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. From 7895a2a082836e6349297acfaffe9b69005df399 Mon Sep 17 00:00:00 2001 From: Daira Hopwood Date: Thu, 15 Jul 2021 15:27:55 +0100 Subject: [PATCH 3/4] [book] src/design/circuit/gadgets/ecc/var-base-scalar-mul.md: more formatting. Signed-off-by: Daira Hopwood --- .../gadgets/ecc/var-base-scalar-mul.md | 69 +++++++++---------- 1 file changed, 32 insertions(+), 37 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md index 1d416ca7..edc72d4c 100644 --- a/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md @@ -99,52 +99,47 @@ $$ \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). From a6badba32f318e2290897f0ce657c31df7797598 Mon Sep 17 00:00:00 2001 From: Daira Hopwood Date: Tue, 27 Jul 2021 01:56:56 +0100 Subject: [PATCH 4/4] [book] src/design/circuit/gadgets/ecc/var-base-scalar-mul.md: we always do addition (possibly of the zero point) at the end of variable-base scalar mul. Signed-off-by: Daira Hopwood --- book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md index edc72d4c..9d193db1 100644 --- a/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md @@ -142,10 +142,10 @@ $\begin{array}{l} \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}$