Skip to content

Commit

Permalink
restructuring decomposition
Browse files Browse the repository at this point in the history
  • Loading branch information
YaoGalteland committed Mar 13, 2024
1 parent 39584d2 commit 9127199
Showing 1 changed file with 41 additions and 25 deletions.
66 changes: 41 additions & 25 deletions book/src/design/gadgets/decomposition.md
Original file line number Diff line number Diff line change
@@ -1,20 +1,23 @@
# Decomposition

## Decompose into $K$-bit values

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+1} = \frac{z_i - k_i}{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, \\
&= 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, \\
&= 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 \\
&= k_2 + 2^{K} \cdot k_3 + \cdots, \\
&\vdots \\
\downarrow &\text{ (in strict mode)} \\
z_W &= (z_{W-1} - k_{W-1}) / 2^K \\
&= 0 \text{ (because } z_{W-1} = k_{W-1} \text{)}
&= 0 \text{ (because } z_{W-1} = k_{W-1} \text{)}
\end{aligned}
$$

Expand All @@ -23,38 +26,42 @@ Strict mode constrains the running sum output $z_{W}$ to be zero, thus range-con

In strict mode, we are also assured that $z_{W-1} = k_{W-1}$ gives us the last window in the decomposition.

## Lookup decomposition
## Lookup decomposition on $K$ bits

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.

The region layout for the lookup decomposition uses a single advice column $z$, and two selectors $q_{lookup}$ and $q_{running}.$
The region layout for the lookup decomposition uses a single advice column $z$, and three selectors $q_{lookup}$, $q_{running}$ and $q_\mathit{range\_check}$.
$$
\begin{array}{|c|c|c|}
\begin{array}{|c|c|c|l|}
\hline
z & q_\mathit{lookup} & q_\mathit{running} \\\hline
z & q_\mathit{lookup} & q_\mathit{running} & q_\mathit{range\_check} \\\hline
\hline
z_0 & 1 & 1 \\\hline
z_1 & 1 & 1 \\\hline
\vdots & \vdots & \vdots \\\hline
z_{n-1} & 1 & 1 \\\hline
z_n & 0 & 0 \\\hline
z_0 & 1 & 1 & 0 \\\hline
z_1 & 1 & 1 & 0 \\\hline
\vdots & \vdots & \vdots & \vdots\\\hline
z_{n-1} & 1 & 1 & 0 \\\hline
z_n & 0 & 0 & 0 \\\hline
\end{array}
$$

### Short range check
For each $i,$ the lookup input expression is:
$$q_\mathit{lookup} \cdot (1 - q_\mathit{range\_check}) \cdot q_\mathit{running} \cdot (z_i - 2^K \cdot z_{i+1})$$

### Correct number of bits
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.

The short variant of the lookup decomposition introduces a $q_{bitshift}$ selector. The same advice column $z$ has here been renamed to $\textsf{word}$ for clarity:
$$
\begin{array}{|c|c|c|c|}
\begin{array}{|c|c|c|c|l|}
\hline
\textsf{word} & q_\mathit{lookup} & q_\mathit{running} & q_\mathit{bitshift} \\\hline
\textsf{word} & q_\mathit{lookup} & q_\mathit{running} & q_\mathit{bitshift} & q_\mathit{range\_check}\\\hline
\hline
\alpha & 1 & 0 & 0 \\\hline
\alpha' & 1 & 0 & 1 \\\hline
2^{K-n} & 0 & 0 & 0 \\\hline
\alpha & 1 & 0 & 0 & 0 \\\hline
\alpha' & 1 & 0 & 1 & 0 \\\hline
2^{K-n} & 0 & 0 & 0 & 0 \\\hline
\end{array}
$$

Expand All @@ -67,9 +74,18 @@ $$
\end{array}
$$

### Generator lookup table
The lookup input expression is:
$$q_\mathit{lookup} \cdot (1 - q_\mathit{range\_check}) \cdot (1 - q_\mathit{running}) \cdot \textsf{word}$$

## Optimized lookup decomposition on 4 and 5 bits

The cost of a lookup protocol depends on the size of the lookup table.
To optimize short range check on 4 and 5 bits,
this gadget makes use of a 4(or 5)-bit lookup table (instead of the 10-bit table) to decompose a field element α into 4(or 5)-bit words.

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

$$
Expand All @@ -94,7 +110,7 @@ $$



## Optimized short range check on 4 and 5 bits
### Lookup decomposition 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$.
Expand Down Expand Up @@ -132,7 +148,7 @@ $$



### Combined lookup expression
## 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
Expand All @@ -145,5 +161,5 @@ The entire expression switches between adding lookups and directly using the cur
$$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
## Short lookup decomposition for less than 4 bits
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 9127199

Please sign in to comment.