[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.
This commit is contained in:
therealyingtong 2021-07-12 11:58:32 +08:00
parent 7b3a0c8a29
commit 2dd23f47b8
6 changed files with 153 additions and 161 deletions

View File

@ -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)

View File

@ -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).$

View File

@ -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 \\

View File

@ -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

View File

@ -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}.$

View File

@ -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.