From 2dd23f47b80da03c202f7cad2d04e7494ca7e433 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Mon, 12 Jul 2021 11:58:32 +0800 Subject: [PATCH] [book] Update constraints for short signed fixed-base mul. Previously, we witnessed the magnitude of a short signed scalar directly as three-bit windows. Now, we decompose and range-constrain it using a running sum. --- book/src/SUMMARY.md | 2 +- .../design/circuit/gadgets/decomposition.md | 42 +++ .../design/circuit/gadgets/ecc/addition.md | 2 +- .../gadgets/ecc/fixed-base-scalar-mul.md | 239 ++++++++---------- .../gadgets/ecc/var-base-scalar-mul.md | 2 +- .../circuit/gadgets/lookup_range_check.md | 27 -- 6 files changed, 153 insertions(+), 161 deletions(-) create mode 100644 book/src/design/circuit/gadgets/decomposition.md delete mode 100644 book/src/design/circuit/gadgets/lookup_range_check.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index faa11f28..728f7ba2 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -22,4 +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) + - [Decomposition](design/circuit/gadgets/decomposition.md) diff --git a/book/src/design/circuit/gadgets/decomposition.md b/book/src/design/circuit/gadgets/decomposition.md new file mode 100644 index 00000000..9c3eaeb9 --- /dev/null +++ b/book/src/design/circuit/gadgets/decomposition.md @@ -0,0 +1,42 @@ +# Decomposition +Given a field element $\alpha$, these gadgets decompose it into $W$ $K$-bit windows $$\alpha = k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + \cdots + 2^{(W-1)K} \cdot k_{W-1}$$ where each $k_i$ a $K$-bit value. + +This is done using a running sum $z_i, i \in [0..W).$ We initialize the running sum $z_0 = \alpha,$ 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} +$$ + +### Strict mode +Strict mode constrains the running sum output $z_{W}$ to be zero, thus range-constraining the field element to be within $W \cdot K$ bits. + +In strict mode, we are also assured that $z_{W-1} = k_{W-1}$ gives us the last window in the decomposition. + +## Lookup decomposition +This gadget makes use of a $K$-bit lookup table to decompose a field element $\alpha$ into $K$-bit words. 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. + +### 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. + +## Short range decomposition +For a short range (for instance, $2^K \leq 8$), we can range-constrain each word using a polynomial constraint instead of a lookup: + +$$ +\begin{array}{|c|l|} +\hline +\text{Degree} & \text{Constraint} \\\hline +2^K + 1 & q_\text{decompose-base-field} \cdot \texttt{range\_check}(z_i - z_{i+1} \cdot 2^K, 2^K) = 0 \\\hline +\end{array} +$$ +where $\texttt{range\_check}(k_i, \texttt{range}) = k_i \cdot (1 - k_i) \cdots (\texttt{range} - 1 - k_i).$ diff --git a/book/src/design/circuit/gadgets/ecc/addition.md b/book/src/design/circuit/gadgets/ecc/addition.md index b089b151..7a27f37e 100644 --- a/book/src/design/circuit/gadgets/ecc/addition.md +++ b/book/src/design/circuit/gadgets/ecc/addition.md @@ -215,7 +215,7 @@ $$ && \\ && \text{Similarly, constraint (b) imposes that } y_r - y_p = 0. \\ && \\ - && \text{Therefore:} + && \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 \\ 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 ba70441a..8426f656 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 @@ -6,16 +6,14 @@ There are $6$ fixed bases in the Orchard protocol: - $\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: +## Decompose scalar +We support fixed-base scalar multiplication with three types of scalars: +### Full-width scalar +A $255$-bit scalar 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).$$ 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|} @@ -25,139 +23,22 @@ $$ \end{array} $$ -At the point of witnessing the scalar, we range-constrain each $3$-bit word of its decomposition. +We range-constrain each $3$-bit word of the scalar decomposition using a polynomial range-check constraint: $$ \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 +9 & q_\text{decompose-base-field} \cdot \texttt{range\_check}(\text{word}, 2^3) = 0 \\\hline \end{array} $$ -where $\texttt{range\_check}(k_i, \texttt{range}) = k_i \cdot (1 - k_i) \cdots (\texttt{range} - 1 - k_i).$ +where $\texttt{range\_check}(\text{word}, \texttt{range}) = \text{word} \cdot (1 - \text{word}) \cdots (\texttt{range} - 1 - \text{word}).$ -## 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: +### Base field element +We support using a base field element as the scalar in fixed-base multiplication. This occurs, for example, in the scalar multiplication for the nullifier computation of the Action circuit $\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. -- 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$$ +Decompose the base field element $\alpha$ into three-bit windows, and range-constrain each window, using the [short range decomposition](../decomposition.md#short-range-decomposition) gadget in strict mode, with $W = 85, K = 3.$ -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 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)$: -- 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 + 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. - -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..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. - -## Fixed-base scalar multiplication -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$. -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 - 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. - -Constraints: -$$ -\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 -$$ --(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 compute the window table in a similar way to full-width fixed-base scalar multiplication, -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 \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 \cdot 83} k_{84},\\ -z_2 &= (z_1 - k_1) / 2^3\\ - &= 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\\ - &= 0. -\end{aligned} -$$ - -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, 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}.$ +If $k_{0..84}$ is witnessed directly then no issue of canonicity arises. However, because the scalar is given as a base field element here, care must be taken to ensure a canonical representation, since $2^{255} > p$. That is, we must 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) }.$$ @@ -188,7 +69,7 @@ z_{44} &= k_{44} + 2^3 k_{45} + \cdots + 2^{3 \cdot (84 - 44)} k_{84}\\ $$ - 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.$ -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.$ +Define $\alpha'_0 = \alpha_0 + 2^{130} - t_p$. To check that $0 \leq \alpha'_0 < 2^{130},$ we use 13 ten-bit [lookups](../decomposition.md#lookup-decomposition), 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 @@ -199,6 +80,102 @@ $$ 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} $$ +### Short signed scalar +A short signed scalar is witnessed as a magnitude $m$ and sign $s$ such that +$$ +s \in \{-1, 1\} \\ +m \in [0, 2^{64}) \\ +\mathsf{v^{old}} - \mathsf{v^{new}} = s \cdot m. +$$ + +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}}$). + +Decompose the magnitude $m$ into three-bit windows, and range-constrain each window, using the [short range decomposition](../decomposition.md#short-range-decomposition) gadget in strict mode, with $W = 22, K = 3.$ + +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} +$$ + +## 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..W)[0..8)$ such that: + +- for the first (W-1) rows $M[0..(W-1))[0..8)$: $$M[w][k] = [(k+2) \cdot (2^3)^w]B$$ +- in the last row $M[W-1][0..8)$: $$M[w][k] = [k \cdot (2^3)^w - \sum\limits_{j=0}^{83} 2^{3j+1}]B$$ + +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}^{W-2} 2^{(W-2)j+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 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..(W-1))$: +- 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 + 2) \cdot (2^3)^w] B)_x &\text{for } w \in [0..(W-1)); \\ + ([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. + +Repeating this for all $W$ windows, we end up with: +- an $W \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..8), w \in [0..85)$ and $c_k$'s are the coefficients for each power of $k$; and +- a length-$W$ 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 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$. +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 - 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. + +Constraints: +$$ +\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). + +### Signed short exponent +Recall that the signed short exponent is witnessed as a $64-$bit magnitude $m$, and a sign $s \in {1, -1}.$ Using the above algorithm, we compute $P = [m] \mathcal{B}$. Then, to get the final result $P',$ we conditionally negate $P$ using $(x, y) \mapsto (x, s \cdot y)$. + +Constraints: +$$ +\begin{array}{|c|l|} +\hline +\text{Degree} & \text{Constraint} \\\hline +3 & q_\text{mul-fixed-short} \cdot \left(s \cdot P_y - P'_y\right) = 0 \\\hline +\end{array} +$$ ## Layout 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 344917a8..6595a40d 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 @@ -334,4 +334,4 @@ $$ 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. #### 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}.$ +We make use of a $10$-bit [lookup range check](../decomposition.md#lookup-decomposition) 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 deleted file mode 100644 index b81a9df9..00000000 --- a/book/src/design/circuit/gadgets/lookup_range_check.md +++ /dev/null @@ -1,27 +0,0 @@ -# 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