Move addition sections into ecc.rs

This commit is contained in:
therealyingtong 2021-04-17 12:53:10 +08:00
parent cd809c57dc
commit 96d60b3f13
5 changed files with 77 additions and 76 deletions

View File

@ -18,7 +18,5 @@
- [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)

View File

@ -1 +1,76 @@
# Elliptic Curve Cryptography
# Elliptic Curve Cryptography
## 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$
## 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) ✓\\
(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}$
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|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 \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

View File

@ -1,61 +0,0 @@
# 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) ✓\\
(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}$
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|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 \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

View File

@ -1,12 +0,0 @@
# 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$

View File

@ -67,6 +67,7 @@ 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: