mirror of https://github.com/zcash/halo2.git
[book] decomposition.md: Merge lookup arguments for normal and short variants.
This commit is contained in:
parent
29fe6e14fc
commit
65ff84da0a
|
@ -22,25 +22,51 @@ $$
|
||||||
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.
|
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.
|
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
|
||||||
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.
|
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}.$
|
||||||
|
$$
|
||||||
|
\begin{array}{|c|c|c|}
|
||||||
|
\hline
|
||||||
|
z & q_{lookup} & q_{running} \\\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
|
||||||
|
\end{array}
|
||||||
|
$$
|
||||||
### Short range check
|
### 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:
|
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.
|
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.
|
2. Constrain $0 \leq \alpha \cdot 2^{K - n} < 2^K$ to be within $K$ bits using a $K$-bit lookup.
|
||||||
|
|
||||||
## Short range decomposition
|
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:
|
||||||
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|c|c|c|}
|
||||||
|
\hline
|
||||||
|
\textsf{word} & q_{lookup} & q_{running} & q_{bitshift} \\\hline
|
||||||
|
\alpha & 1 & 0 & 0 \\\hline
|
||||||
|
\alpha' & 1 & 0 & 1 \\\hline
|
||||||
|
2^{K-n} & 0 & 0 & 0 \\\hline
|
||||||
|
\end{array}
|
||||||
|
$$
|
||||||
|
|
||||||
|
where $\alpha' = \alpha \cdot 2^{K - n}.$ Note that $2^{K-n}$ is assigned to a fixed column at keygen, and copied in at proving time. This is used in the gate enabled by the $q_{bitshift}$ selector to check that $\alpha$ was shifted correctly:
|
||||||
$$
|
$$
|
||||||
\begin{array}{|c|l|}
|
\begin{array}{|c|l|}
|
||||||
\hline
|
\hline
|
||||||
\text{Degree} & \text{Constraint} \\\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
|
2 & q_{bitshift} \cdot (\alpha' - (\alpha \cdot 2^{K - n})) \\\hline
|
||||||
2 & q_\text{strict} \cdot z_W = 0 \\\hline
|
|
||||||
\end{array}
|
\end{array}
|
||||||
$$
|
$$
|
||||||
where $\texttt{range\_check}(k_i, \texttt{range}) = k_i \cdot (1 - k_i) \cdots (\texttt{range} - 1 - k_i).$
|
|
||||||
|
### Combined lookup expression
|
||||||
|
Since the lookup decomposition and its short variant both make use of the same lookup table, we can combine their lookup input expressions into a single one:
|
||||||
|
|
||||||
|
$$q_{lookup} \cdot \left(q_{running} \cdot (z_i - 2^K \cdot z_{i+1}) + (1 - q_{running}) \cdot \textsf{word} \right).$$
|
||||||
|
|
||||||
|
## Short range decomposition
|
||||||
|
For a short range (for instance, $2^K \leq 8$), we can range-constrain each word using a degree-$2^K$ polynomial constraint instead of a lookup: $$\texttt{range\_check(word, range)} = \texttt{word} \cdot (1 - \texttt{word}) \cdots (\texttt{range} - 1 - \texttt{word}).$$
|
||||||
|
|
Loading…
Reference in New Issue