From c074990bb99a65ab301387600f290c0d1a91c15d Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Mon, 29 Mar 2021 14:01:05 +0800 Subject: [PATCH 01/29] [book] Document ECC gadget in circuit --- book/src/SUMMARY.md | 6 ++ book/src/design/circuit/gadgets.md | 0 book/src/design/circuit/gadgets/ecc.md | 1 + .../circuit/gadgets/ecc/complete-add.md | 52 +++++++++ .../gadgets/ecc/fixed-base-scalar-mul.md | 66 ++++++++++++ .../circuit/gadgets/ecc/incomplete-add.md | 12 +++ .../gadgets/ecc/var-base-scalar-mul.md | 102 ++++++++++++++++++ 7 files changed, 239 insertions(+) create mode 100644 book/src/design/circuit/gadgets.md create mode 100644 book/src/design/circuit/gadgets/ecc.md create mode 100644 book/src/design/circuit/gadgets/ecc/complete-add.md create mode 100644 book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md create mode 100644 book/src/design/circuit/gadgets/ecc/incomplete-add.md create mode 100644 book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index e8420281..836449af 100644 --- a/book/src/SUMMARY.md +++ b/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) diff --git a/book/src/design/circuit/gadgets.md b/book/src/design/circuit/gadgets.md new file mode 100644 index 00000000..e69de29b diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md new file mode 100644 index 00000000..40ed41e4 --- /dev/null +++ b/book/src/design/circuit/gadgets/ecc.md @@ -0,0 +1 @@ +# Elliptic Curve Cryptography \ No newline at end of file diff --git a/book/src/design/circuit/gadgets/ecc/complete-add.md b/book/src/design/circuit/gadgets/ecc/complete-add.md new file mode 100644 index 00000000..72b80643 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md new file mode 100644 index 00000000..558a7e54 --- /dev/null +++ b/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. diff --git a/book/src/design/circuit/gadgets/ecc/incomplete-add.md b/book/src/design/circuit/gadgets/ecc/incomplete-add.md new file mode 100644 index 00000000..938cee6b --- /dev/null +++ b/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$ \ No newline at end of file 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 new file mode 100644 index 00000000..d1ce854f --- /dev/null +++ b/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. +$ \ No newline at end of file From 137066e056b9b216a272909f1a16b87a63a5fdc3 Mon Sep 17 00:00:00 2001 From: ying tong Date: Fri, 9 Apr 2021 16:51:14 +0800 Subject: [PATCH 02/29] Apply suggestions from code review Co-authored-by: str4d Co-authored-by: Daira Hopwood --- .../circuit/gadgets/ecc/complete-add.md | 45 +++++++++++-------- .../gadgets/ecc/fixed-base-scalar-mul.md | 22 +++++---- .../gadgets/ecc/var-base-scalar-mul.md | 20 ++++++--- 3 files changed, 53 insertions(+), 34 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/complete-add.md b/book/src/design/circuit/gadgets/ecc/complete-add.md index 72b80643..0b91f57c 100644 --- a/book/src/design/circuit/gadgets/ecc/complete-add.md +++ b/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 \ No newline at end of file +Max degree: 4 diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 558a7e54..37de167c 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/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$. 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 d1ce854f..4a1bb52a 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 @@ -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. -$ \ No newline at end of file +$$ +\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} +$$ From cd809c57dc44769a45c4581d3d76178de393a34c Mon Sep 17 00:00:00 2001 From: ying tong Date: Fri, 9 Apr 2021 16:53:35 +0800 Subject: [PATCH 03/29] Apply suggestions from code review Co-authored-by: str4d --- book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 4a1bb52a..e701dc7d 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 @@ -92,7 +92,7 @@ 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, $$ From 96d60b3f137fc4ec7803562af7914107f49eed26 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Sat, 17 Apr 2021 12:53:10 +0800 Subject: [PATCH 04/29] Move addition sections into ecc.rs --- book/src/SUMMARY.md | 2 - book/src/design/circuit/gadgets/ecc.md | 77 ++++++++++++++++++- .../circuit/gadgets/ecc/complete-add.md | 61 --------------- .../circuit/gadgets/ecc/incomplete-add.md | 12 --- .../gadgets/ecc/var-base-scalar-mul.md | 1 + 5 files changed, 77 insertions(+), 76 deletions(-) delete mode 100644 book/src/design/circuit/gadgets/ecc/complete-add.md delete mode 100644 book/src/design/circuit/gadgets/ecc/incomplete-add.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 836449af..306b8074 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -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) diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md index 40ed41e4..5c4b7e48 100644 --- a/book/src/design/circuit/gadgets/ecc.md +++ b/book/src/design/circuit/gadgets/ecc.md @@ -1 +1,76 @@ -# Elliptic Curve Cryptography \ No newline at end of file +# 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 diff --git a/book/src/design/circuit/gadgets/ecc/complete-add.md b/book/src/design/circuit/gadgets/ecc/complete-add.md deleted file mode 100644 index 0b91f57c..00000000 --- a/book/src/design/circuit/gadgets/ecc/complete-add.md +++ /dev/null @@ -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 diff --git a/book/src/design/circuit/gadgets/ecc/incomplete-add.md b/book/src/design/circuit/gadgets/ecc/incomplete-add.md deleted file mode 100644 index 938cee6b..00000000 --- a/book/src/design/circuit/gadgets/ecc/incomplete-add.md +++ /dev/null @@ -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$ \ No newline at end of file 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 e701dc7d..9dcbb174 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 @@ -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: From 33b4192c0d4131eba07427177f796ad18f652c94 Mon Sep 17 00:00:00 2001 From: ying tong Date: Thu, 22 Apr 2021 17:10:33 +0800 Subject: [PATCH 05/29] Apply suggestions from code review Co-authored-by: Daira Hopwood Co-authored-by: str4d --- book/src/design/circuit/gadgets/ecc.md | 14 +++++++------- .../circuit/gadgets/ecc/fixed-base-scalar-mul.md | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md index 5c4b7e48..ae3cbedd 100644 --- a/book/src/design/circuit/gadgets/ecc.md +++ b/book/src/design/circuit/gadgets/ecc.md @@ -5,13 +5,13 @@ 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}$ +- $\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$ +- $(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 @@ -34,8 +34,8 @@ $$ \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 \\ + \lambda &= \frac{y_p - y_q}{x_p - x_q} \\ + x_r &= \lambda^2 - x_q - x_p \\ y_r &= \lambda(x_p - x_r) - y_p \end{aligned} $$ diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 37de167c..e02b7983 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -14,8 +14,8 @@ $$\alpha = k_0 + k_1 \cdot (2^3)^1 + \cdots + k_{84} \cdot (2^3)^{84}, k_i \in [ ## 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..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..84)[0..8)$: $$M[w][k] = [(k+1) \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^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, i.e. we subtract $\sum\limits_{j=0}^{83} (2^3)^j$. @@ -23,7 +23,7 @@ For each window of fixed-base multiples $M[w] = (M[w][0], \cdots, M[w][7]), w \i - 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 + 1) \cdot 8^w] B)_x &\text{for } w \in [0..84); \\ ([k \cdot (8)^w - \sum\limits_{j=0}^{83} (8)^j] B)_x &\text{for } w = 84; \text{ and} \end{cases} $$ @@ -40,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..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. Use [incomplete addition](./incomplete-add.md) to sum the $M[w][k_w]$'s, resulting in $[\alpha]B$. From b4c3805e2220a3152abd5011beb8b05b1f66fda5 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 22 Apr 2021 17:39:27 +0800 Subject: [PATCH 06/29] Address further review comments. Co-authored-by: Daira Hopwood Co-authored-by: str4d --- book/src/design/circuit/gadgets/ecc.md | 18 ++++++++++-------- .../gadgets/ecc/fixed-base-scalar-mul.md | 6 +++--- 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md index ae3cbedd..491fc791 100644 --- a/book/src/design/circuit/gadgets/ecc.md +++ b/book/src/design/circuit/gadgets/ecc.md @@ -1,17 +1,19 @@ # Elliptic Curve Cryptography ## Incomplete addition -Inputs: $P = (x_P, y_P), Q = (x_Q, y_Q)$ -Output: $A = P + Q = (x_A, y_A)$ +- Inputs: $P = (x_p, y_p), Q = (x_q, y_q)$ +- Output: $R = P + Q = (x_r, y_r)$ 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$ +- $x_r = \lambda^2 - x_q - x_p$ +- $y_r = \lambda(x_q - x_r) - 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$ +- $(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)$, 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 @@ -36,7 +38,7 @@ P + Q &= R\\ (x_p, y_p) + (x_q, y_q) &= (x_r, y_r) \\ \lambda &= \frac{y_p - y_q}{x_p - x_q} \\ x_r &= \lambda^2 - x_q - x_p \\ - y_r &= \lambda(x_p - x_r) - y_p + y_r &= \lambda(x_q - x_r) - y_q \end{aligned} $$ @@ -73,4 +75,4 @@ A \cdot \left(2y_p \cdot \lambda - 3{x_p}^2\right) &=& 0 & A \wedge y_p \neq 0 & \end{array} $ -Max degree: 4 +Max degree: $4$ diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index e02b7983..71a3394c 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -19,8 +19,8 @@ Then, we precompute multiples of the fixed base $B$ for each window. This takes 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. +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 + 1) \cdot 8^w] B)_x &\text{for } w \in [0..84); \\ @@ -32,7 +32,7 @@ For each window of fixed-base multiples $M[w] = (M[w][0], \cdots, M[w][7]), w \i 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 +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. From e881b19b6a457ede0a1804d2164cda634a7ba201 Mon Sep 17 00:00:00 2001 From: ying tong Date: Fri, 23 Apr 2021 22:03:04 +0800 Subject: [PATCH 07/29] Apply suggestions from code review Co-authored-by: Daira Hopwood --- book/src/design/circuit/gadgets/ecc.md | 8 +++++++- .../design/circuit/gadgets/ecc/fixed-base-scalar-mul.md | 3 ++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md index 491fc791..61fb19e1 100644 --- a/book/src/design/circuit/gadgets/ecc.md +++ b/book/src/design/circuit/gadgets/ecc.md @@ -11,7 +11,8 @@ Formulae: Substituting for $\lambda$, 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)$, and so cannot be used with arbitrary inputs. + - 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$ @@ -76,3 +77,8 @@ A \cdot \left(2y_p \cdot \lambda - 3{x_p}^2\right) &=& 0 & A \wedge y_p \neq 0 & $ Max degree: $4$ + +Note: It is the cross-interaction of the two $B$ constraints that fully constrain +the implications. For example, the contrapositive of the first constraint's implication +$x_p = 0 \implies B$ is $¬B \implies x_p \neq 0$, which is the other half of the +second constraint's implication. The same applies to $C$. diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 71a3394c..8d328f01 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -67,4 +67,5 @@ $$ 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. +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. From 1e0c644a81cb9bf89294c40221001fef7d309ff2 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 6 May 2021 19:42:11 +0800 Subject: [PATCH 08/29] Detail optimised variable-base scalar mul --- .../gadgets/ecc/var-base-scalar-mul.md | 106 ++++++++++++++---- 1 file changed, 86 insertions(+), 20 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 9dcbb174..8725dd12 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 @@ -82,28 +82,94 @@ So the last three iterations of the loop ($i = 2..0$) need to use [complete addi } 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): - -$$ -\lambda_{2,i}^2 - (x_{A,i+1} + (\lambda_{1,i}^2 - x_{A,i} - x_{P,i}) + x_{A,i}) = 0, -$$ +## 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} -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. + &\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{aligned} + &(\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\ + &\mathbf{z}_{i} = 2\mathbf{z}_{i+1} + \mathbf{k}_{i}\\ + & x_{U,i} = x_T\\ + & y_{U,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)}\\ + & \lambda_{1,i} \cdot (x_{A,i} - x_{U,i}) = y_{A,i} - y_{U,i}\\ + & \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{U,i}\\ + & (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) = 2 y_{\mathsf{A},i}\\ + & \lambda_{2,i}^2 = x_{A,i-1} + x_{R,i} + x_{A,i}\\ + & \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A,i-1}\\ + +\end{aligned} +$$ + +After substitution of $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} + &// \text{let } \mathbf{k}_i = \mathbf{z}_{i+1} - 2\mathbf{z}_i\\ + &// \text{let } x_{R,i} = (\lambda_{1,i}^2 - x_{A,i} - x_T)\\ + &// \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}\\ + &(\mathbf{z}_{i+1} - 2\mathbf{z}_i)(\mathbf{z}_{i+1} - 2\mathbf{z}_i - 1) = 0\\ + &\lambda_{1,i} \cdot (x_{A,i} - x_T) = \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2} - (2 \cdot (\mathbf{z}_{i+1} - 2\mathbf{z}_i) - 1) \cdot y_T\\ + &\lambda_{2,i}^2 = x_{A,i-1} + (\lambda_{1,i}^2 - x_{A,i} - x_T) + x_{A,i}\\ + &\text{if } i > 3 \text{ then } 2 \cdot \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) =\\ + &\hspace{2em}(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T)) +\\ + &\hspace{2em}(\lambda_{1,i-1} + \lambda_{2,i-1}) \cdot (x_{A,i-1} - (\lambda_{1,i-1}^2 - x_{A,i-1} - x_T))\\ +\end{aligned} +$$ + +$\lambda_{2,3} \cdot (x_{A,3} - x_{A,2}) = \frac{(\lambda_{1,3} + \lambda_{2,3}) \cdot (x_{A,3} - (\lambda_{1,3}^2 - x_{A,3} - x_T))\hspace{2em}}{2} + y_{A,2}$ + +The bits $\mathbf{k}_{3 \dots 1}$ are used in double-and-add using [complete addition](./complete-add.md). + +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). + +Output $(x_{A,0}, y_{A,0})$ + +### 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: + +$$ +\begin{array}{|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} & z^{lo} & x_A^{lo} & \lambda_1^{lo} & \lambda_2^{lo} \\\hline + & & 0 & 2[T]_x & & & \mathbf{z}_{129} & x_{A,129} & & \\\hline + x_T & y_T & \mathbf{z}_{254} & x_{A,254} & \lambda_{1,254} & \lambda_{2,254} & \mathbf{z}_{128} & x_{A,128} & \lambda_{1,128} & \lambda_{2,128} \\\hline + x_T & y_T & \mathbf{z}_{253} & x_{A,253} & \lambda_{1,253} & \lambda_{2,253} & \mathbf{z}_{127} & x_{A,127} & \lambda_{1,127} & \lambda_{2,127} \\\hline + \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} & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} \\\hline + x_T & y_T & \mathbf{z}_{129} & x_{A,129} & \lambda_{1,129} & \lambda_{2,129} & \mathbf{z}_3 & x_{A,3} & \lambda_{1,3} & \lambda_{2,3} \\\hline +\end{array} +$$ + +For each $hi$ and $lo$ half, the following constraints are enforced: +$$ +\begin{array}{|c|l|} +\hline +\text{Degree} & \text{Constraint} \\\hline +2 & q_{ECC,i} \cdot (\mathbf{z}_{i+1} - 2\mathbf{z}_i - \mathbf{k}_i) = 0 \\\hline +3 & q_{ECC,i} \cdot \mathbf{k}_i \cdot (\mathbf{k}_i - 1) = 0 \\\hline +4 & q_{ECC,i} \cdot \left(\lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) - y_{A,i} + (2\mathbf{k}_i - 1) \cdot y_{P,i}\right) = 0 \\\hline +4 & q_{ECC,i} \cdot \left((\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_{P,i})) - 2 y_{A,i}\right) = 0 \\\hline +3 & q_{ECC,i} \cdot \left(\lambda_{2,i}^2 - x_{A,i+1} - (\lambda_{1,i}^2 - x_{A,i} - x_{P,i}) - x_{A,i}\right) = 0 \\\hline +3 & q_{ECC,i} \cdot \left(\lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) - y_{A,i} - y_{A,i+1}\right) = 0 \\\hline +2 & q_{ECC,i} \cdot \left(x_{P,i} - x_{P,i-1}\right) = 0 \\\hline +2 & q_{ECC,i} \cdot \left(y_{P,i} - y_{P,i-1}\right) = 0 \\\hline +\end{array} +$$ \ No newline at end of file From 0903ae23e70e52e66691149acd09d31fab78d08a Mon Sep 17 00:00:00 2001 From: ying tong Date: Fri, 21 May 2021 17:43:08 +0800 Subject: [PATCH 09/29] Use correct symbol in incomplete addition section Co-authored-by: Daira Hopwood --- book/src/design/circuit/gadgets/ecc.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md index 61fb19e1..e1748d47 100644 --- a/book/src/design/circuit/gadgets/ecc.md +++ b/book/src/design/circuit/gadgets/ecc.md @@ -2,7 +2,7 @@ ## Incomplete addition - Inputs: $P = (x_p, y_p), Q = (x_q, y_q)$ -- Output: $R = P + Q = (x_r, y_r)$ +- Output: $R = P \;⸭\; Q = (x_r, y_r)$ Formulae: - $\lambda \cdot (x_p - x_q) = y_p - y_q$ From 58e3da88c274fa0261d61d550dfec224e74311b4 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Sun, 23 May 2021 10:26:55 +0800 Subject: [PATCH 10/29] Document point doubling constraints --- book/src/design/circuit/gadgets/ecc.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md index e1748d47..f7ee5165 100644 --- a/book/src/design/circuit/gadgets/ecc.md +++ b/book/src/design/circuit/gadgets/ecc.md @@ -1,5 +1,18 @@ # Elliptic Curve Cryptography +## Point doubling +- Input: $P = (x_p, y_p)$ +- Output: $[2]P = (x_r, y_r)$ + +Formulae: +$\lambda = \frac{3 x_p^2}{2 \cdot y_p}$ +$x_r = \lambda^2 - 2 \cdot x_p$ +$y_r = \lambda(x_p - x_r) - y_p$ + +Substituting for $\lambda$, we get the constraints: +- $4 \cdot y_p^2(x_r + 2 \cdot x_p) - 9 x_p^4 = 0$ +- $2 \cdot y_p(y_r + y_p) - 3 x_p^2(x_p - x_r) = 0$ + ## Incomplete addition - Inputs: $P = (x_p, y_p), Q = (x_q, y_q)$ - Output: $R = P \;⸭\; Q = (x_r, y_r)$ From 2699703b0271d1ae0f945a49449752a6b49e9342 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Tue, 25 May 2021 00:20:18 +0800 Subject: [PATCH 11/29] Update fixed-base window formulae --- .../circuit/gadgets/ecc/fixed-base-scalar-mul.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 8d328f01..0008295e 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -14,17 +14,17 @@ $$\alpha = k_0 + k_1 \cdot (2^3)^1 + \cdots + k_{84} \cdot (2^3)^{84}, k_i \in [ ## 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+1) \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^3)^j]B$$ +- 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 + 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$. +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}$. 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 + 1) \cdot 8^w] B)_x &\text{for } w \in [0..84); \\ - ([k \cdot (8)^w - \sum\limits_{j=0}^{83} (8)^j] B)_x &\text{for } w = 84; \text{ and} + ([(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. From 12feacf4173d27fd1f0bf18e3e2e96b0178a44eb Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Tue, 25 May 2021 14:07:17 +0800 Subject: [PATCH 12/29] Fix complete addition constraints --- book/src/design/circuit/gadgets/ecc.md | 70 +++++++++++++------------- 1 file changed, 36 insertions(+), 34 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md index f7ee5165..84b1b6ef 100644 --- a/book/src/design/circuit/gadgets/ecc.md +++ b/book/src/design/circuit/gadgets/ecc.md @@ -58,40 +58,42 @@ $$ 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$. +Define $\mathsf{inv0}(x) = \begin{cases} 0, &\text{if } x = 0 \\ 1/x, &\text{otherwise.} \end{cases}$ -$ -\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 \\ +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{Complete} \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{Complete} \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{Complete} \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{Complete} \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{Complete} \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{Complete} \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{Complete} \cdot (1 - x_p \cdot \beta) \cdot (x_r - x_q) &=& 0 & x_p = 0 \implies x_r = x_q \\ +4 & q_\mathit{Complete} \cdot (1 - x_p \cdot \beta) \cdot (y_r - y_q) &=& 0 & x_p = 0 \implies y_r = y_q \\\hline +4 & q_\mathit{Complete} \cdot (1 - x_q \cdot \gamma) \cdot (x_r - x_p) &=& 0 & x_q = 0 \implies x_r = x_p \\ +4 & q_\mathit{Complete} \cdot (1 - x_q \cdot \gamma) \cdot (y_r - y_p) &=& 0 & x_q = 0 \implies y_r = y_p \\\hline +4 & q_\mathit{Complete} \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{Complete} \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: $4$ - -Note: It is the cross-interaction of the two $B$ constraints that fully constrain -the implications. For example, the contrapositive of the first constraint's implication -$x_p = 0 \implies B$ is $¬B \implies x_p \neq 0$, which is the other half of the -second constraint's implication. The same applies to $C$. +Max degree: 6 From e2ac3715f1a99de481076c9f49c8a6706fe53ec1 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 27 May 2021 13:33:06 +0800 Subject: [PATCH 13/29] Explain (k+2) offset in fixed-base window formulae --- .../circuit/gadgets/ecc/fixed-base-scalar-mul.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 0008295e..c5ee0658 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -19,6 +19,14 @@ Then, we precompute multiples of the fixed base $B$ for each window. This takes 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 summing the multiples of $B$ at each window 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. $$ @@ -43,7 +51,10 @@ Given a decomposed scalar $\alpha$ and a fixed base $B$, we compute $[\alpha]B$ 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. Use [incomplete addition](./incomplete-add.md) to sum the $M[w][k_w]$'s, resulting in $[\alpha]B$. +4. For all windows but the last, use [incomplete addition](./incomplete-add.md) to sum the $M[w][k_w]$'s, resulting in $[\alpha]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)$. Constraints: - $x_w = \mathcal{L}_x[w](k_w)$; From ab96225f0fe4e03bc7f94b656dc3a07efeafbacb Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 9 Jun 2021 18:23:02 +0800 Subject: [PATCH 14/29] ecc::addition.md: Update complete addition constraints. Add constraint analysis and proofs of completeness and soundness. --- book/src/SUMMARY.md | 1 + book/src/design/circuit/gadgets/ecc.md | 99 ----- .../design/circuit/gadgets/ecc/addition.md | 337 ++++++++++++++++++ .../gadgets/ecc/var-base-scalar-mul.md | 12 +- 4 files changed, 344 insertions(+), 105 deletions(-) create mode 100644 book/src/design/circuit/gadgets/ecc/addition.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 306b8074..40a9d3fe 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -18,5 +18,6 @@ - [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) diff --git a/book/src/design/circuit/gadgets/ecc.md b/book/src/design/circuit/gadgets/ecc.md index 84b1b6ef..e69de29b 100644 --- a/book/src/design/circuit/gadgets/ecc.md +++ b/book/src/design/circuit/gadgets/ecc.md @@ -1,99 +0,0 @@ -# Elliptic Curve Cryptography - -## Point doubling -- Input: $P = (x_p, y_p)$ -- Output: $[2]P = (x_r, y_r)$ - -Formulae: -$\lambda = \frac{3 x_p^2}{2 \cdot y_p}$ -$x_r = \lambda^2 - 2 \cdot x_p$ -$y_r = \lambda(x_p - x_r) - y_p$ - -Substituting for $\lambda$, we get the constraints: -- $4 \cdot y_p^2(x_r + 2 \cdot x_p) - 9 x_p^4 = 0$ -- $2 \cdot y_p(y_r + y_p) - 3 x_p^2(x_p - x_r) = 0$ - -## Incomplete addition -- Inputs: $P = (x_p, y_p), Q = (x_q, y_q)$ -- Output: $R = P \;⸭\; Q = (x_r, y_r)$ - -Formulae: -- $\lambda \cdot (x_p - x_q) = y_p - y_q$ -- $x_r = \lambda^2 - x_q - x_p$ -- $y_r = \lambda(x_q - x_r) - y_q$ - -Substituting for $\lambda$, 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 - -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_p - y_q}{x_p - x_q} \\ - x_r &= \lambda^2 - x_q - x_p \\ - y_r &= \lambda(x_q - x_r) - y_q -\end{aligned} -$$ - -For the doubling case, $\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{Complete} \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{Complete} \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{Complete} \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{Complete} \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{Complete} \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{Complete} \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{Complete} \cdot (1 - x_p \cdot \beta) \cdot (x_r - x_q) &=& 0 & x_p = 0 \implies x_r = x_q \\ -4 & q_\mathit{Complete} \cdot (1 - x_p \cdot \beta) \cdot (y_r - y_q) &=& 0 & x_p = 0 \implies y_r = y_q \\\hline -4 & q_\mathit{Complete} \cdot (1 - x_q \cdot \gamma) \cdot (x_r - x_p) &=& 0 & x_q = 0 \implies x_r = x_p \\ -4 & q_\mathit{Complete} \cdot (1 - x_q \cdot \gamma) \cdot (y_r - y_p) &=& 0 & x_q = 0 \implies y_r = y_p \\\hline -4 & q_\mathit{Complete} \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{Complete} \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 diff --git a/book/src/design/circuit/gadgets/ecc/addition.md b/book/src/design/circuit/gadgets/ecc/addition.md new file mode 100644 index 00000000..8014ee1a --- /dev/null +++ b/book/src/design/circuit/gadgets/ecc/addition.md @@ -0,0 +1,337 @@ +## Incomplete addition +- Inputs: $P = (x_p, y_p), Q = (x_q, y_q)$ +- Output: $R = P \;⸭\; Q = (x_r, y_r)$ + +Formulae: +- $\lambda \cdot (x_p - x_q) = y_p - y_q$ +- $x_r = \lambda^2 - x_q - x_p$ +- $y_r = \lambda(x_q - x_r) - y_q$ + +Substituting for $\lambda$, 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, $\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 } :: 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{ then by rearranging both sides we get }\\ + && \lambda = 3x_p^2 / 2y_p \\ + && \text{Therefore } :: (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 } :: x_p = 0 => (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 } :: 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.$ \ No newline at end of file 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 8725dd12..8f3fd6bf 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 @@ -49,15 +49,15 @@ We use an optimized double-and-add algorithm is (copied from ["Faster variable-b The maximum value of $acc$ is: ``` - <--n 1s---> - 1011111111111 -= 1100000000000 - 1 + <--- n 1s ---> + 1011111...111111 += 1100000...000000 - 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). +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. @@ -69,7 +69,7 @@ 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: +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: Acc := [2] T for i from 253 down to 3 { @@ -136,7 +136,7 @@ $$ $\lambda_{2,3} \cdot (x_{A,3} - x_{A,2}) = \frac{(\lambda_{1,3} + \lambda_{2,3}) \cdot (x_{A,3} - (\lambda_{1,3}^2 - x_{A,3} - x_T))\hspace{2em}}{2} + y_{A,2}$ -The bits $\mathbf{k}_{3 \dots 1}$ are used in double-and-add using [complete addition](./complete-add.md). +The bits $\mathbf{k}_{3 \dots 1}$ are used in double-and-add using [complete addition](./addition.md#Complete-addition). 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 02a732b921d04272e33df164e84eb8b2b5734905 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 9 Jun 2021 18:27:34 +0800 Subject: [PATCH 15/29] fixed-base-scalar-mul.md: Include G^{Orchard} fixed base --- .../design/circuit/gadgets/ecc/fixed-base-scalar-mul.md | 3 ++- .../design/circuit/gadgets/ecc/var-base-scalar-mul.md | 9 +++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index c5ee0658..a1fd9b24 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -1,7 +1,8 @@ # Fixed-base scalar multiplication -There are $5$ fixed bases in the Orchard protocol: +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}}$. 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 8f3fd6bf..47aa45e8 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 @@ -122,13 +122,14 @@ for $i$ from $254$ down to $4$: $$ \begin{aligned} - &// \text{let } \mathbf{k}_i = \mathbf{z}_{i+1} - 2\mathbf{z}_i\\ - &// \text{let } x_{R,i} = (\lambda_{1,i}^2 - x_{A,i} - x_T)\\ - &// \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}\\ + &\texttt{// let } \mathbf{k}_i = \mathbf{z}_{i+1} - 2\mathbf{z}_i\\ + &\texttt{// let } x_{R,i} = (\lambda_{1,i}^2 - x_{A,i} - x_T)\\ + &\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{z}_{i+1} - 2\mathbf{z}_i)(\mathbf{z}_{i+1} - 2\mathbf{z}_i - 1) = 0\\ &\lambda_{1,i} \cdot (x_{A,i} - x_T) = \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2} - (2 \cdot (\mathbf{z}_{i+1} - 2\mathbf{z}_i) - 1) \cdot y_T\\ &\lambda_{2,i}^2 = x_{A,i-1} + (\lambda_{1,i}^2 - x_{A,i} - x_T) + x_{A,i}\\ - &\text{if } i > 3 \text{ then } 2 \cdot \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) =\\ + & \\ + &\texttt{if } i > 3 \texttt{ then } 2 \cdot \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) =\\ &\hspace{2em}(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T)) +\\ &\hspace{2em}(\lambda_{1,i-1} + \lambda_{2,i-1}) \cdot (x_{A,i-1} - (\lambda_{1,i-1}^2 - x_{A,i-1} - x_T))\\ \end{aligned} From f46a2a4c40a6eae31d80e1624f728a9b118ed9c9 Mon Sep 17 00:00:00 2001 From: ying tong Date: Wed, 9 Jun 2021 18:31:06 +0800 Subject: [PATCH 16/29] Apply suggestions from code review Co-authored-by: Daira Hopwood --- .../src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md | 6 +++--- book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index a1fd9b24..ed168010 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -25,7 +25,7 @@ The additional $(k + 2)$ term lets us avoid adding the point at infinity in the > * $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 summing the multiples of $B$ at each window using incomplete addition. +> 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)$: @@ -47,7 +47,7 @@ where $k \in [0..8), w \in [0..85)$ and $c_k$'s are the coefficients for each po 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: +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$. @@ -55,7 +55,7 @@ Given a decomposed scalar $\alpha$ and a fixed base $B$, we compute $[\alpha]B$ 4. For all windows but the last, use [incomplete addition](./incomplete-add.md) to sum the $M[w][k_w]$'s, resulting in $[\alpha]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)$. +> 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: - $x_w = \mathcal{L}_x[w](k_w)$; 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 47aa45e8..6fd9fd87 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 @@ -19,7 +19,7 @@ Thus, given a scalar $\alpha$, we witness the boolean decomposition of $k = \alp $$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): +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: > > Acc := [2] T > for i from n-1 down to 0 { @@ -173,4 +173,4 @@ $$ 2 & q_{ECC,i} \cdot \left(x_{P,i} - x_{P,i-1}\right) = 0 \\\hline 2 & q_{ECC,i} \cdot \left(y_{P,i} - y_{P,i-1}\right) = 0 \\\hline \end{array} -$$ \ No newline at end of file +$$ From 1ea8397a7c3a4456a05e406c05461ce3854d86ff Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 9 Jun 2021 18:44:57 +0800 Subject: [PATCH 17/29] variable-base-scalar-mul.md: Disable book tests. --- .../gadgets/ecc/var-base-scalar-mul.md | 82 ++++++++++--------- 1 file changed, 43 insertions(+), 39 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 6fd9fd87..3ddfabdf 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 @@ -20,35 +20,39 @@ $$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: -> -> 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: +```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 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: + +```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 @@ -71,16 +75,18 @@ 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: - 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 +```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: @@ -95,9 +101,7 @@ $$ Initialize $A_{254} = [2] T$ - for $i$ from $254$ down to $4$: - $$ \begin{aligned} &(\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\ From 6c34956c1876b4a930fdbd553139b502b9c5263a Mon Sep 17 00:00:00 2001 From: str4d Date: Thu, 1 Jul 2021 13:46:48 +0100 Subject: [PATCH 18/29] book: Remove superfluous checkmarks Co-authored-by: Daira Hopwood --- book/src/design/circuit/gadgets/ecc/addition.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/addition.md b/book/src/design/circuit/gadgets/ecc/addition.md index 8014ee1a..671dbab9 100644 --- a/book/src/design/circuit/gadgets/ecc/addition.md +++ b/book/src/design/circuit/gadgets/ecc/addition.md @@ -17,12 +17,12 @@ Substituting for $\lambda$, we get the constraints: ## 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 ✓ +\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$.) @@ -334,4 +334,4 @@ $$ \delta &= 0 \\ \end{aligned} $$ -because in all remaining cases, $x_q \neq x_p, x_p \neq 0, x_q \neq 0.$ \ No newline at end of file +because in all remaining cases, $x_q \neq x_p, x_p \neq 0, x_q \neq 0.$ From 68acc33caed3d7450b828fa60221ac20fd29729a Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 2 Jul 2021 00:17:12 +0800 Subject: [PATCH 19/29] [book] Document overflow check for variable-base scalar mul. --- .../gadgets/ecc/var-base-scalar-mul.md | 78 +++++++++++++++++++ 1 file changed, 78 insertions(+) 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 3ddfabdf..8de32dd9 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 @@ -178,3 +178,81 @@ $$ 2 & q_{ECC,i} \cdot \left(y_{P,i} - y_{P,i-1}\right) = 0 \\\hline \end{array} $$ + +## 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) \\ + & & \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: + +$\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)$. + +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: + +$s = \alpha + \mathbf{k}_{254} \cdot 2^{130}$ +$\mathbf{z}_0 = \alpha + t_q \pmod{p}$ +$\mathbf{k}_{254} \cdot (\mathbf{z}_{130} - 2^{124}) = 0$ +$\mathbf{k}_{254} \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i) = 0$ +$(1 - \mathbf{k}_{254}) \cdot (1 - \mathbf{z}_{130} \cdot \eta) \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i) = 0$ + +where $\sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i$ can be computed by another running sum. [TODO: be explicit about how to do that.] From 902dbbb700849b99584597ac314304270ff074e8 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 2 Jul 2021 16:42:10 +0800 Subject: [PATCH 20/29] [book] Fix window table sum expression in fixed-base scalar mul. Co-authored-by: Jack Grigg --- book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index ed168010..5bc97e0b 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -52,7 +52,7 @@ Given a decomposed scalar $\alpha$ and a fixed base $B$, we compute $[\alpha]B$ 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]B$. +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. From 802334892d7f4d37ed11a34bdf2f691b91b8897f Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 2 Jul 2021 16:42:49 +0800 Subject: [PATCH 21/29] [book] Constrain first and last rows in incomplete addition secton of variable-base scalar mul. Co-authored-by: Jack Grigg --- .../gadgets/ecc/var-base-scalar-mul.md | 113 ++++++++++++------ 1 file changed, 75 insertions(+), 38 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 8de32dd9..d6c3a076 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 @@ -32,7 +32,7 @@ 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. +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: @@ -59,7 +59,7 @@ The maximum value of `acc` is: ``` = $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$. +> 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). @@ -99,47 +99,42 @@ $$ \end{aligned} $$ -Initialize $A_{254} = [2] T$ +Initialize $A_{254} = [2] T.$ for $i$ from $254$ down to $4$: $$ \begin{aligned} &(\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\ &\mathbf{z}_{i} = 2\mathbf{z}_{i+1} + \mathbf{k}_{i}\\ - & x_{U,i} = x_T\\ - & y_{U,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)}\\ - & \lambda_{1,i} \cdot (x_{A,i} - x_{U,i}) = y_{A,i} - y_{U,i}\\ - & \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{U,i}\\ + & x_{P,i} = x_T\\ + & y_{P,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)}\\ + & \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) = y_{A,i} - y_{P,i}\\ + & \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{P,i}\\ & (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) = 2 y_{\mathsf{A},i}\\ & \lambda_{2,i}^2 = x_{A,i-1} + x_{R,i} + x_{A,i}\\ - & \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A,i-1}\\ - + & \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A,i-1},\\ \end{aligned} $$ -After substitution of $y_{P,i}$, $x_{R,i}$, $y_{A,i}$, and $y_{A,i+1}$, this becomes: +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$ +Initialize $A_{254} = [2] T.$ for $i$ from $254$ down to $4$: $$ \begin{aligned} - &\texttt{// let } \mathbf{k}_i = \mathbf{z}_{i+1} - 2\mathbf{z}_i\\ - &\texttt{// let } x_{R,i} = (\lambda_{1,i}^2 - x_{A,i} - x_T)\\ + &\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{z}_{i+1} - 2\mathbf{z}_i)(\mathbf{z}_{i+1} - 2\mathbf{z}_i - 1) = 0\\ - &\lambda_{1,i} \cdot (x_{A,i} - x_T) = \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2} - (2 \cdot (\mathbf{z}_{i+1} - 2\mathbf{z}_i) - 1) \cdot y_T\\ - &\lambda_{2,i}^2 = x_{A,i-1} + (\lambda_{1,i}^2 - x_{A,i} - x_T) + x_{A,i}\\ + &(\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\\ & \\ - &\texttt{if } i > 3 \texttt{ then } 2 \cdot \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) =\\ - &\hspace{2em}(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T)) +\\ - &\hspace{2em}(\lambda_{1,i-1} + \lambda_{2,i-1}) \cdot (x_{A,i-1} - (\lambda_{1,i-1}^2 - x_{A,i-1} - x_T))\\ + &\texttt{if } i > 4 \texttt{ then } \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A, i-1}\\ \end{aligned} $$ - -$\lambda_{2,3} \cdot (x_{A,3} - x_{A,2}) = \frac{(\lambda_{1,3} + \lambda_{2,3}) \cdot (x_{A,3} - (\lambda_{1,3}^2 - x_{A,3} - x_T))\hspace{2em}}{2} + y_{A,2}$ +Outside the for loop, we witness $y_{A,3}$, and constrain $$\lambda_{2,4} \cdot (x_{A,4} - x_{A,3}) = \frac{(\lambda_{1,4} + \lambda_{2,4}) \cdot (x_{A,4} - (\lambda_{1,4}^2 - x_{A,4} - x_T))}{2} + y_{A,3}.$$ The bits $\mathbf{k}_{3 \dots 1}$ are used in double-and-add using [complete addition](./addition.md#Complete-addition). @@ -151,33 +146,75 @@ Output $(x_{A,0}, y_{A,0})$ 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: $$ -\begin{array}{|c|c|c|c|c|c|c|c|c|c|} +\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} & z^{lo} & x_A^{lo} & \lambda_1^{lo} & \lambda_2^{lo} \\\hline - & & 0 & 2[T]_x & & & \mathbf{z}_{129} & x_{A,129} & & \\\hline - x_T & y_T & \mathbf{z}_{254} & x_{A,254} & \lambda_{1,254} & \lambda_{2,254} & \mathbf{z}_{128} & x_{A,128} & \lambda_{1,128} & \lambda_{2,128} \\\hline - x_T & y_T & \mathbf{z}_{253} & x_{A,253} & \lambda_{1,253} & \lambda_{2,253} & \mathbf{z}_{127} & x_{A,127} & \lambda_{1,127} & \lambda_{2,127} \\\hline - \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} & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} \\\hline - x_T & y_T & \mathbf{z}_{129} & x_{A,129} & \lambda_{1,129} & \lambda_{2,129} & \mathbf{z}_3 & x_{A,3} & \lambda_{1,3} & \lambda_{2,3} \\\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}_{129} & & y_{A,128} & & 1 \\\hline + x_T & y_T & \mathbf{z}_{254} & x_{A,254} = 2[T]_x & \lambda_{1,254} & \lambda_{2,254} & 2 & \mathbf{z}_{128} & x_{A,128} & \lambda_{1,128} & \lambda_{2,128} & 2 \\\hline + x_T & y_T & \mathbf{z}_{253} & x_{A,253} & \lambda_{1,253} & \lambda_{2,253} & 2 & \mathbf{z}_{127} & x_{A,127} & \lambda_{1,127} & \lambda_{2,127} & 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} & 2 & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} & 2 \\\hline + x_T & y_T & \mathbf{z}_{129} & x_{A,129} & \lambda_{1,129} & \lambda_{2,129} & 2 & & x_{A,3} & y_{A,3} & & 3 \\\hline + & & & x_{A,128} & y_{A,128} & & 3 & & & & & \\\hline \end{array} $$ -For each $hi$ and $lo$ half, the following constraints are enforced: +For each $hi$ and $lo$ half + +- on row 0: 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 -2 & q_{ECC,i} \cdot (\mathbf{z}_{i+1} - 2\mathbf{z}_i - \mathbf{k}_i) = 0 \\\hline -3 & q_{ECC,i} \cdot \mathbf{k}_i \cdot (\mathbf{k}_i - 1) = 0 \\\hline -4 & q_{ECC,i} \cdot \left(\lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) - y_{A,i} + (2\mathbf{k}_i - 1) \cdot y_{P,i}\right) = 0 \\\hline -4 & q_{ECC,i} \cdot \left((\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_{P,i})) - 2 y_{A,i}\right) = 0 \\\hline -3 & q_{ECC,i} \cdot \left(\lambda_{2,i}^2 - x_{A,i+1} - (\lambda_{1,i}^2 - x_{A,i} - x_{P,i}) - x_{A,i}\right) = 0 \\\hline -3 & q_{ECC,i} \cdot \left(\lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) - y_{A,i} - y_{A,i+1}\right) = 0 \\\hline -2 & q_{ECC,i} \cdot \left(x_{P,i} - x_{P,i-1}\right) = 0 \\\hline -2 & q_{ECC,i} \cdot \left(y_{P,i} - y_{P,i-1}\right) = 0 \\\hline +5 & q_{mul,i}^{one} \cdot \left(y_{A,i} - \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2}\right) = 0 \\\hline \end{array} $$ +where +$$ +\begin{aligned} +q_{mul,i}^{one} &= q_{mul,i} \cdot (2 - q_{mul, i}) \cdot (3 - q_{mul, i}),\\ +y_{A,i} &\text{ is witnessed.} +\end{aligned} +$$ + +- on all rows excluding the last: +$$ +\begin{array}{|c|l|} +\hline +\text{Degree} & \text{Constraint} \\\hline +4 & q_{mul,i}^{two} \cdot \left(x_{T,cur} - x_{T,next}\right) = 0 \\\hline +4 & q_{mul,i}^{two} \cdot \left(y_{T,cur} - y_{T,next}\right) = 0 \\\hline +5 & q_{mul,i}^{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,i}^{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,i}^{two} \cdot \left(\lambda_{2,i}^2 - x_{A,i-1} - \lambda_{1,i}^2 + x_{T,i}\right) = 0 \\\hline +5 & q_{mul,i}^{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,i}^{two} &= q_{mul,i} \cdot (1 - q_{mul, i}) \cdot (3 - q_{mul, i}),\\ +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} +$$ + +- on the last row: check that $y_A$ has been witnessed correctly. +$$ +\begin{array}{|c|l|} +\hline +\text{Degree} & \text{Constraint} \\\hline +5 & q_{mul,i}^{three} \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,i}^{three} &= q_{mul,i} \cdot (1 - q_{mul, i}) \cdot (2 - q_{mul, i}),\\ +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{ is witnessed.} +\end{aligned} +$$ ## Overflow check From 1a531cf6196f6b1683ea6e49f92d9f0b3fc44d3d Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 2 Jul 2021 21:41:31 +0800 Subject: [PATCH 22/29] [book] Correct hi and lo ranges in constraint table Co-authored-by: Jack Grigg --- .../circuit/gadgets/ecc/var-base-scalar-mul.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 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 d6c3a076..bd9cb34f 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 @@ -149,13 +149,13 @@ $$ \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}_{129} & & y_{A,128} & & 1 \\\hline - x_T & y_T & \mathbf{z}_{254} & x_{A,254} = 2[T]_x & \lambda_{1,254} & \lambda_{2,254} & 2 & \mathbf{z}_{128} & x_{A,128} & \lambda_{1,128} & \lambda_{2,128} & 2 \\\hline - x_T & y_T & \mathbf{z}_{253} & x_{A,253} & \lambda_{1,253} & \lambda_{2,253} & 2 & \mathbf{z}_{127} & x_{A,127} & \lambda_{1,127} & \lambda_{2,127} & 2 \\\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} & 2 & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} & 2 \\\hline - x_T & y_T & \mathbf{z}_{129} & x_{A,129} & \lambda_{1,129} & \lambda_{2,129} & 2 & & x_{A,3} & y_{A,3} & & 3 \\\hline - & & & x_{A,128} & y_{A,128} & & 3 & & & & & \\\hline + x_T & y_T & \mathbf{z}_{130} & x_{A,130} & \lambda_{1,130} & \lambda_{2,130} & 2 & \mathbf{z}_5 & x_{A,5} & \lambda_{1,5} & \lambda_{2,5} & 2 \\\hline + & & & x_{A,129} & y_{A,129} & & 3 & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} & 2 \\\hline + & & & & & & & & x_{A,3} & y_{A,3} & & 3 \\\hline \end{array} $$ From 2b4d9fda49ef47019f39e9ff68794c18720d52c0 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 2 Jul 2021 22:44:01 +0800 Subject: [PATCH 23/29] [book] Correct q_mul = 3 case. Co-authored-by: Jack Grigg --- .../gadgets/ecc/var-base-scalar-mul.md | 66 +++++++++++-------- 1 file changed, 40 insertions(+), 26 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 bd9cb34f..e7e9a884 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 @@ -130,11 +130,14 @@ $$ &(\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\\ - & \\ - &\texttt{if } i > 4 \texttt{ then } \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A, i-1}\\ \end{aligned} $$ -Outside the for loop, we witness $y_{A,3}$, and constrain $$\lambda_{2,4} \cdot (x_{A,4} - x_{A,3}) = \frac{(\lambda_{1,4} + \lambda_{2,4}) \cdot (x_{A,4} - (\lambda_{1,4}^2 - x_{A,4} - x_T))}{2} + y_{A,3}.$$ +$$ +\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} +$$ The bits $\mathbf{k}_{3 \dots 1}$ are used in double-and-add using [complete addition](./addition.md#Complete-addition). @@ -143,7 +146,10 @@ If the least significant bit is set $\mathbf{k_0} = 1,$ we return the accumulato Output $(x_{A,0}, y_{A,0})$ ### 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: +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|} @@ -153,66 +159,74 @@ $$ 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} & 2 & \mathbf{z}_5 & x_{A,5} & \lambda_{1,5} & \lambda_{2,5} & 2 \\\hline - & & & x_{A,129} & y_{A,129} & & 3 & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} & 2 \\\hline - & & & & & & & & x_{A,3} & y_{A,3} & & 3 \\\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 +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. -- on row 0: check that $\lambda_1, \lambda_2$ are initialized to values consistent with the initial $y_A.$ +#### $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,i}^{one} \cdot \left(y_{A,i} - \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2}\right) = 0 \\\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,i}^{one} &= q_{mul,i} \cdot (2 - q_{mul, i}) \cdot (3 - q_{mul, i}),\\ -y_{A,i} &\text{ is witnessed.} +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} $$ -- on all rows excluding the last: +#### $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,i}^{two} \cdot \left(x_{T,cur} - x_{T,next}\right) = 0 \\\hline -4 & q_{mul,i}^{two} \cdot \left(y_{T,cur} - y_{T,next}\right) = 0 \\\hline -5 & q_{mul,i}^{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,i}^{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,i}^{two} \cdot \left(\lambda_{2,i}^2 - x_{A,i-1} - \lambda_{1,i}^2 + x_{T,i}\right) = 0 \\\hline -5 & q_{mul,i}^{two} \cdot \left(\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) - y_{A,i} - y_{A,i-1}\right) = 0 \\\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,i}^{two} &= q_{mul,i} \cdot (1 - q_{mul, i}) \cdot (3 - q_{mul, i}),\\ +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} $$ -- on the last row: check that $y_A$ has been witnessed correctly. +#### $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,i}^{three} \cdot \left(\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) - y_{A,i} - y_{A,i-1}\right) = 0 \\\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,i}^{three} &= q_{mul,i} \cdot (1 - q_{mul, i}) \cdot (2 - q_{mul, i}),\\ -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{ is witnessed.} +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} $$ @@ -254,7 +268,7 @@ 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) \\ - & & \big(\mathbf{k}_{254} = 0 \implies (\alpha \in [0, 2^{130}) \;\vee\; \mathbf{k}_{253..130} \text{ are not all } 0)\big) \;\wedge \\ + &\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}$ From 6479598b27c89348a97ee245c508c59df8817819 Mon Sep 17 00:00:00 2001 From: ying tong Date: Sat, 3 Jul 2021 18:37:35 +0800 Subject: [PATCH 24/29] Apply suggestions from code review Co-authored-by: str4d --- .../gadgets/ecc/fixed-base-scalar-mul.md | 26 +++++++++++++--- .../gadgets/ecc/var-base-scalar-mul.md | 31 +++++++++++++------ 2 files changed, 44 insertions(+), 13 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 5bc97e0b..34ce2fe3 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -58,9 +58,17 @@ Given a decomposed scalar $\alpha$ and a fixed base $B$, we compute $[\alpha]B$ > 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: - - $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].$ +$$ +\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 @@ -80,4 +88,14 @@ $$ 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. +but with only $\mathsf{ceil}(64 / 3) = 22$ windows. In addition to the 21 full-width 3-bit +constraints, we have two additional constraints: + +$$ +\begin{array}{|c|l|} +\hline +\text{Degree} & \text{Constraint} \\\hline +3 & q_\text{scalar-fixed-short} \cdot \left(\mathbf{m}_0 \cdot (1 - \mathbf{m}_0)\right) = 0 \\\hline +3 & q_\text{scalar-fixed-short} \cdot \left(s^2 - 1\right) = 0 \\\hline +\end{array} +$$ 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 e7e9a884..e1ea1bd8 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 @@ -242,7 +242,7 @@ Since overflow can only occur in the final step that constrains $\mathbf{z}_0 = ### 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).$ +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}$. @@ -250,8 +250,10 @@ 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}$ @@ -268,6 +270,7 @@ 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}$ @@ -290,9 +293,13 @@ Finally, we can merge the $130$-bit decompositions for the $\mathbf{k}_{254} = 0 Let $s = \alpha + \mathbf{k}_{254} \cdot 2^{130}$. The constraints for the overflow check are: -$\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)$. +$$ +\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}$ @@ -300,10 +307,16 @@ Witness $\eta = \mathsf{inv0}(\mathbf{z}_{130})$, and decompose $s \bmod p$ as $ Then the needed gates are: -$s = \alpha + \mathbf{k}_{254} \cdot 2^{130}$ -$\mathbf{z}_0 = \alpha + t_q \pmod{p}$ -$\mathbf{k}_{254} \cdot (\mathbf{z}_{130} - 2^{124}) = 0$ -$\mathbf{k}_{254} \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i) = 0$ -$(1 - \mathbf{k}_{254}) \cdot (1 - \mathbf{z}_{130} \cdot \eta) \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i) = 0$ +$$ +\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)\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)\right) = 0 \\\hline +\end{array} +$$ where $\sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i$ can be computed by another running sum. [TODO: be explicit about how to do that.] From 32f9622c231bf747c82de764525c5a1b29a3458a Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Sat, 3 Jul 2021 19:26:46 +0800 Subject: [PATCH 25/29] [book] Document lookup range check and its use in overflow check. --- book/src/SUMMARY.md | 1 + .../gadgets/ecc/var-base-scalar-mul.md | 8 +++--- .../circuit/gadgets/lookup_range_check.md | 27 +++++++++++++++++++ 3 files changed, 33 insertions(+), 3 deletions(-) create mode 100644 book/src/design/circuit/gadgets/lookup_range_check.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index a55cc6b1..faa11f28 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -22,3 +22,4 @@ - [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) 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 e1ea1bd8..37d8c743 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 @@ -314,9 +314,11 @@ $$ 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)\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)\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. -where $\sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i$ can be computed by another running sum. [TODO: be explicit about how to do that.] +#### 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}.$ diff --git a/book/src/design/circuit/gadgets/lookup_range_check.md b/book/src/design/circuit/gadgets/lookup_range_check.md new file mode 100644 index 00000000..b81a9df9 --- /dev/null +++ b/book/src/design/circuit/gadgets/lookup_range_check.md @@ -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. \ No newline at end of file From 091592e1109863119e30a27e45840cf808063079 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 7 Jul 2021 17:10:18 +0800 Subject: [PATCH 26/29] [book] Document canonicity check for fixed-base scalar mul when base field element is used as the scalar. --- .../gadgets/ecc/fixed-base-scalar-mul.md | 83 ++++++++++++++++++- 1 file changed, 79 insertions(+), 4 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 34ce2fe3..833dea66 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -12,6 +12,16 @@ 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).$$ +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: @@ -88,14 +98,79 @@ $$ 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. In addition to the 21 full-width 3-bit -constraints, we have two additional constraints: +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(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(83)} k_{84},\\ +z_2 &= (z_1 - k_1) / 2^3\\ + &= k_2 + (2^3) k_3 + ... + 2^{3(82)} k_{84},\\ + &\cdots,\\ +z_{84} &= k_{84}\\ +z_{85} &= (z_{84} - k_{84}) / 2^3\\ + &= 0. +\end{aligned} +$$ + +Since we don't directly witness this decomposition, 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 -3 & q_\text{scalar-fixed-short} \cdot \left(\mathbf{m}_0 \cdot (1 - \mathbf{m}_0)\right) = 0 \\\hline -3 & q_\text{scalar-fixed-short} \cdot \left(s^2 - 1\right) = 0 \\\hline +9 & q_\text{decompose-base-field} \cdot \texttt{range\_check}(z_i - z_{i+1} \cdot (2^3), 8) = 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), 4) = 0 \\\hline +3 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_2), 2) = 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 ≤ \alpha_0 < 2^{130}$ + - $\alpha_2 = 1 \implies 0 ≤ \alpha_0 + 2^{130} - t_p < 2^{130}$ + +This will involve 13 ten-bit [lookups](../lookup_range_check.md) for each $\alpha_0$ and $\alpha_0' \equiv \alpha_0 + 2^{130} - t_p$, where we constrain the $z_{13}$ running sum output of each lookup to be $0$ if $\alpha_2 = 1.$ +$$ +\begin{array}{|c|l|} +\hline +\text{Degree} & \text{Constraint} \\\hline +3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot \alpha_1 = 0 \\\hline +3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot z_{13}(\texttt{lookup}(\alpha_0, 13)) = 0 \\\hline +3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot z_{13}(\texttt{lookup}(\alpha_0', 13)) = 0 \\\hline \end{array} $$ From afc8d9a142874c7aacb657085e8f2ec5df2f9d4f Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 8 Jul 2021 09:03:59 +0800 Subject: [PATCH 27/29] [book] Eliminate alpha_0 lookup decomposition when checking canonicity of base field element used in fixed-base mul. --- .../gadgets/ecc/fixed-base-scalar-mul.md | 30 +++++++++++++------ 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 833dea66..418eeca5 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -134,7 +134,7 @@ z_{85} &= (z_{84} - k_{84}) / 2^3\\ \end{aligned} $$ -Since we don't directly witness this decomposition, 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$. +Since we don't directly witness the three-bit values, 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 @@ -161,16 +161,28 @@ $$ 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 ≤ \alpha_0 < 2^{130}$ - - $\alpha_2 = 1 \implies 0 ≤ \alpha_0 + 2^{130} - t_p < 2^{130}$ + - $\alpha_2 = 1 \implies 0 \leq \alpha_0 < 2^{130}$, + - $\alpha_2 = 1 \implies 0 \leq \alpha_0 + 2^{130} - t_p < 2^{130}$ -This will involve 13 ten-bit [lookups](../lookup_range_check.md) for each $\alpha_0$ and $\alpha_0' \equiv \alpha_0 + 2^{130} - t_p$, where we constrain the $z_{13}$ running sum output of each lookup to be $0$ if $\alpha_2 = 1.$ +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{array}{|c|l|} +\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} - 2^3 \cdot z_{44}.$ + +To check that $0 \leq \alpha_0 + 2^{130} - t_p < 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} \\\hline -3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot \alpha_1 = 0 \\\hline -3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot z_{13}(\texttt{lookup}(\alpha_0, 13)) = 0 \\\hline -3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot z_{13}(\texttt{lookup}(\alpha_0', 13)) = 0 \\\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} - t_p < 2^{130}\\\hline \end{array} $$ From 2febafbdfec567609b102667970cfa06fb0c632f Mon Sep 17 00:00:00 2001 From: ying tong Date: Thu, 8 Jul 2021 16:40:44 +0800 Subject: [PATCH 28/29] Apply suggestions from code review Co-authored-by: Daira Hopwood Co-authored-by: str4d --- .../design/circuit/gadgets/ecc/addition.md | 47 ++++++++++++++++--- .../gadgets/ecc/fixed-base-scalar-mul.md | 17 ++++++- 2 files changed, 56 insertions(+), 8 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/addition.md b/book/src/design/circuit/gadgets/ecc/addition.md index 671dbab9..2c0ad682 100644 --- a/book/src/design/circuit/gadgets/ecc/addition.md +++ b/book/src/design/circuit/gadgets/ecc/addition.md @@ -1,13 +1,47 @@ +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)$ -Formulae: -- $\lambda \cdot (x_p - x_q) = y_p - y_q$ -- $x_r = \lambda^2 - x_q - x_p$ -- $y_r = \lambda(x_q - x_r) - y_q$ +The formulae from Hışıl's thesis are: -Substituting for $\lambda$, we get the constraints: +- $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. @@ -37,7 +71,8 @@ P + Q &= R\\ \end{aligned} $$ -For the doubling case, $\lambda$ has to instead be computed as $\frac{3x^2}{2y}$. +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}$ diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index 418eeca5..d6775400 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -12,6 +12,19 @@ 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).$$ +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|} @@ -153,8 +166,8 @@ $$ \begin{array}{|c|l|} \hline \text{Degree} & \text{Constraint} \\\hline -5 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_1), 4) = 0 \\\hline -3 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_2), 2) = 0 \\\hline +5 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_1, 4) = 0 \\\hline +3 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_2, 2) = 0 \\\hline 2 & q_\text{canon-base-field} \cdot \left(z_{84} - (\alpha_1 + \alpha_2 \cdot 2^2)\right) = 0 \\\hline \end{array} $$ From d9f134ac4b0008c14c42f5c1d15128ee850a30d1 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 9 Jul 2021 09:54:36 +0800 Subject: [PATCH 29/29] [book] Details and formatting changes. Co-authored-by: Daira Hopwood --- .../design/circuit/gadgets/ecc/addition.md | 24 +++++---- .../gadgets/ecc/fixed-base-scalar-mul.md | 41 ++++++++++----- .../gadgets/ecc/var-base-scalar-mul.md | 51 ++++++++++++------- 3 files changed, 75 insertions(+), 41 deletions(-) diff --git a/book/src/design/circuit/gadgets/ecc/addition.md b/book/src/design/circuit/gadgets/ecc/addition.md index 2c0ad682..b089b151 100644 --- a/book/src/design/circuit/gadgets/ecc/addition.md +++ b/book/src/design/circuit/gadgets/ecc/addition.md @@ -30,6 +30,7 @@ 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\\ @@ -40,6 +41,7 @@ Assuming $x_p \neq x_q$, \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$ @@ -130,7 +132,8 @@ $$ && \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 } :: x_q \neq x_p \implies \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} @@ -144,9 +147,10 @@ $$ && \\ && \text{If } y_p = 0 \text{ then } x_p = 0, \text{ and the constraint is satisfied.}\\ && \\ - && \text{If } y_p \neq 0 \text{ then by rearranging both sides we get }\\ + && \text{If } y_p \neq 0 \text{ by rearranging both sides we get }\\ && \lambda = 3x_p^2 / 2y_p \\ - && \text{Therefore } :: (x_q = x_p) \wedge y_p \neq 0 \implies \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 \\ @@ -173,9 +177,9 @@ $$ &\text{• Similarly, constraint (d) imposes that } y_r = \lambda \cdot (x_p - x_r) - y_p \text{ is satisfied.} \\ \end{aligned} \\ && \\ - && \text{Therefore} \\ + && \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)) \\ + &(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} \\ && \\ @@ -193,7 +197,8 @@ $$ && \\ && \text{Similarly, constraint (b) imposes that } y_r - y_q = 0. \\ && \\ - && \text{Therefore } :: x_p = 0 => (x_r, y_r) = (x_q, y_q). \\ + && \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 \\ @@ -210,7 +215,8 @@ $$ && \\ && \text{Similarly, constraint (b) imposes that } y_r - y_p = 0. \\ && \\ - && \text{Therefore } :: x_q = 0 \implies (x_r, y_r) = (x_p, y_p). \\ + && \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 \\ @@ -225,7 +231,7 @@ $$ && \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{Therefore: } x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0). \end{array} $$ @@ -337,7 +343,7 @@ $(x_p, y_p) + (x_q, y_q) = (x_r, y_r)$ \end{array} $ - - Soundness: (x_r, y_r) = (0, 0) is the only solution + - Soundness: $(x_r, y_r) = (0, 0)$ is the only solution * $(\zeta x, y) + (x, y)$ diff --git a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md index d6775400..ba70441a 100644 --- a/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/fixed-base-scalar-mul.md @@ -131,15 +131,15 @@ 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(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.) +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(83)} k_{84},\\ + &= 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(82)} k_{84},\\ + &= 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\\ @@ -147,27 +147,27 @@ z_{85} &= (z_{84} - k_{84}) / 2^3\\ \end{aligned} $$ -Since we don't directly witness the three-bit values, 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$. +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), 8) = 0 \\\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) }.$$ +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, 4) = 0 \\\hline -3 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_2, 2) = 0 \\\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} $$ @@ -178,7 +178,7 @@ If the MSB $\alpha_2 = 0$ is not set, then $\alpha < 2^{254} < p.$ However, in t - $\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: +- 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}\\ @@ -186,16 +186,31 @@ z_{44} &= k_{44} + 2^3 k_{45} + \cdots + 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} - 2^3 \cdot z_{44}.$ +- 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.$ -To check that $0 \leq \alpha_0 + 2^{130} - t_p < 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.$ +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} - t_p < 2^{130}\\\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. 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 37d8c743..344917a8 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 @@ -102,19 +102,17 @@ $$ Initialize $A_{254} = [2] T.$ for $i$ from $254$ down to $4$: -$$ -\begin{aligned} - &(\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\ - &\mathbf{z}_{i} = 2\mathbf{z}_{i+1} + \mathbf{k}_{i}\\ - & x_{P,i} = x_T\\ - & y_{P,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)}\\ - & \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) = y_{A,i} - y_{P,i}\\ - & \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{P,i}\\ - & (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) = 2 y_{\mathsf{A},i}\\ - & \lambda_{2,i}^2 = x_{A,i-1} + x_{R,i} + x_{A,i}\\ - & \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A,i-1},\\ -\end{aligned} -$$ +$\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: @@ -138,18 +136,33 @@ $$ \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 double-and-add using [complete addition](./addition.md#Complete-addition). +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). -Output $(x_{A,0}, y_{A,0})$ +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$. +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|}