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