Skip to content

Commit

Permalink
update decomposition
Browse files Browse the repository at this point in the history
  • Loading branch information
YaoGalteland committed Mar 6, 2024
1 parent 75ea29c commit bab9cfa
Showing 1 changed file with 73 additions and 3 deletions.
76 changes: 73 additions & 3 deletions book/src/design/gadgets/decomposition.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ $$
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.

Expand All @@ -38,6 +39,7 @@ z_{n-1} & 1 & 1 \\\hline
z_n & 0 & 0 \\\hline
\end{array}
$$

### 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:

Expand Down Expand Up @@ -65,12 +67,80 @@ $$
\end{array}
$$

### Combined lookup expression
Since the lookup decomposition and its short variant both make use of the same lookup table, we combine their lookup input expressions into a single one:
### Generator lookup table

To optimize short range check on 4 and 5 bits, we extend the K-bit lookup table to a lookup table with $2^{10}+2^{4}+2^{5}$ pre-computed random generators.
These are loaded into the following lookup table:

$$
\begin{array}{|c|c|c|c|}
\hline
table_{idx} & table_x & table_y & table_{range\_check\_tag} \\\hline
0 & x_{P[0]} & y_{P[0]} & 0 \\\hline
1 & x_{P[1]} & y_{P[1]} & 0 \\\hline
\vdots & \vdots & \vdots & \vdots \\\hline
2^{10} - 1 & x_{P[2^{10}-1]} & y_{P[2^{10}-1]} & 0 \\\hline
2^{10} + 0 & x_{P[0]} & y_{P[0]} & 4 \\\hline
2^{10}+ 1 & x_{P[1]} & y_{P[1]} & 4 \\\hline
\vdots & \vdots & \vdots & \vdots \\\hline
2^{10} + 2^{4} - 1 & x_{P[2^{4}-1]} & y_{P[2^{4}-1]} & 4 \\\hline
2^{10} + 2^{4} + 0 & x_{P[0]} & y_{P[0]} & 5 \\\hline
2^{10} + 2^{4} + 1 & x_{P[1]} & y_{P[1]} & 5 \\\hline
\vdots & \vdots & \vdots & \vdots \\\hline
2^{10} + 2^{4} + 2^{5} - 1 & x_{P[2^{5}-1]} & y_{P[2^{5}-1]} & 5 \\\hline
\end{array}
$$

## Optimized short range check on 4 and 5 bits
The 4 and 5 bits variant of the lookup decomposition introduces two selectors $q_\mathit{range\_check\_4}$ and $q_\mathit{range\_check\_5}$.
We can calculate $q_\mathit{range\_check}$ to see if the 4-bit and 5-bit checks are activated.
$q_\mathit{range\_check} = 1$ if $q_\mathit{range\_check\_4}=1$ or $q_\mathit{range\_check\_5}=1$.
We further calculate the number of bits in a short field element, denoted as $num_\mathit{bits}$.
$num_\mathit{bits} = 4$ if $q_\mathit{range\_check\_4}=1$, and $num_\mathit{bits} = 5$ if $q_\mathit{range\_check\_5}=1$.

$$
\begin{array}{|c|c|c|c|}
\hline
q_\mathit{range\_check\_4} & q_\mathit{range\_check\_5} & q_\mathit{range\_check} & num_\mathit{bits}\\\hline
0 & 1 & 1 & 5 \\\hline
1 & 0 & 1 & 4\\\hline
0 & 0 & 0 & 0 \\\hline
\end{array}
$$

We have two lookup input expressions:
$$q_\mathit{lookup} \cdot q_\mathit{range\_check}\cdot \textsf{word} $$
$$q_\mathit{lookup} \cdot q_\mathit{range\_check} \cdot num_\mathit{bits}$$

Each 4-bit word $\beta$ is range-constrained by a lookup in the lookup table with $table_{range\_check\_tag} = 4$ and $table_{idx}\in \{ 2^{10},\dots, 2^{10} + 2^{4}-1\}$.
Each 5-bit word $\gamma$ is range-constrained by a lookup in the lookup table with $table_{range\_check\_tag} = 5$ and $table_{idx}\in \{ 2^{10} + 2^{4},\dots, 2^{10} + 2^{4} + 2^{5} - 1\}$.

The region layout for the lookup decomposition shows below.

$$
\begin{array}{|c|c|c|c|}
\hline
\textsf{word} & num_\mathit{bits} & q_\mathit{lookup} & q_\mathit{range\_check} \\\hline
\beta &4 & 1 & 1 \\\hline
\gamma & 5 & 1 & 1 \\\hline
\end{array}
$$



$$q_\mathit{lookup} \cdot \left(q_\mathit{running} \cdot (z_i - 2^K \cdot z_{i+1}) + (1 - q_\mathit{running}) \cdot \textsf{word} \right)$$

### Combined lookup expression
Since the lookup decomposition, its short variant and optimized range checks all make use of the same lookup table, we combine their lookup input expressions into the following two:

#### First lookup expression
$$q_\mathit{lookup} \cdot \left((1 - q_\mathit{range\_check}) \cdot \left(q_\mathit{running} \cdot (z_i - 2^K \cdot z_{i+1}) + (1 - q_\mathit{running}) \cdot \textsf{word}\right) + q_\mathit{range\_check}\cdot \textsf{word} \right)$$
where $z_i$ and $\textsf{word}$ are the same cell (but distinguished here for clarity of usage).
The entire expression switches between adding lookups and directly using the current value based on whether a range check is being performed, effectively integrating different types of lookups and checks within the same framework.

#### Second lookup expression

$$q_\mathit{lookup} \cdot q_\mathit{range\_check} \cdot num_\mathit{bits}$$
This expression activates when both lookup operations and range checks are active, and multiplies by the number of bits (4 or 5) involved in the check. This effectively tags the operation with its bit length, allowing the system to differentiate between 4-bit and 5-bit checks.

## Short range decomposition
For a short range (for instance, $[0, \texttt{range})$ where $\texttt{range} \leq 8$), we can range-constrain each word using a degree-$\texttt{range}$ polynomial constraint instead of a lookup: $$\RangeCheck{word}{range} = \texttt{word} \cdot (1 - \texttt{word}) \cdots (\texttt{range} - 1 - \texttt{word}).$$

0 comments on commit bab9cfa

Please sign in to comment.