Skip to content

Commit

Permalink
update book
Browse files Browse the repository at this point in the history
  • Loading branch information
YaoGalteland committed Mar 27, 2024
1 parent 9127199 commit b9949d0
Show file tree
Hide file tree
Showing 3 changed files with 135 additions and 46 deletions.
4 changes: 3 additions & 1 deletion book/src/design/gadgets/cond_swap.md
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
# Conditional swap

The conditional swap gadgets include two instructions: swap and multiplexer (mux).
We use a multiplexer to compute differently for ZEC or for non-ZEC assets in Orchard protocol.
We use a multiplexer to compute differently for ZEC or for non-ZEC assets in Orchard protocol:

![](https://imgur.com/kDQLoQQ.png)

## Multiplexer

Expand Down
131 changes: 98 additions & 33 deletions book/src/design/gadgets/decomposition.md
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,14 @@
# Decomposition
We present two variants of lookup decomposition: non-optimized and optimized versions.
The optimized version introduces an enhancement specifically targeting [optimized short range check on 4 and 5 bits](https://zcash.github.io/halo2/design/gadgets/decomposition.html#optimized-short-range-check-on-4-and-5-bits).

This analysis of lookup decomposition (call $\texttt{lookup}$) is applied in different contexts:
- [10 bits](https://zcash.github.io/halo2/design/gadgets/decomposition.html#lookup-decomposition) (for running sum $(z_{i} - 2^K \cdot z_{i+1})$)
- [n bits](https://zcash.github.io/halo2/design/gadgets/decomposition.html#short-range-check), where $n\leq 10$. (for a single element short range check)
- [4 and 5](https://zcash.github.io/halo2/design/gadgets/decomposition.html#optimized-short-range-check-on-4-and-5-bits) bits (for optimized short range check)

Furthermore, the [range check](https://zcash.github.io/halo2/design/gadgets/decomposition.html#short-range-decomposition)
approach (call $\texttt{range\_check}$) is used for verifying values within ranges of up to 3 bits

## Decompose into $K$-bit values

Expand Down Expand Up @@ -26,13 +36,27 @@ 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 on $K$ bits
## 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, where $K=10$.
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 three selectors $q_{lookup}$, $q_{running}$ and $q_\mathit{range\_check}$.
$$
\begin{array}{|c|c|c|l|}
\begin{array}{|c|c|c|}
\hline
table_{idx} & table_x & table_y \\\hline
0 & x_{P[0]} & y_{P[0]} \\\hline
1 & x_{P[1]} & y_{P[1]} \\\hline
2 & x_{P[2]} & y_{P[2]} \\\hline
\vdots & \vdots & \vdots \\\hline
2^{10} - 1 & x_{P[2^{10}-1]} & y_{P[2^{10}-1]} \\\hline
\end{array}
$$

The region layout for the lookup decomposition uses a single advice column $z$, and two selectors $q_{lookup}$ and $q_{running}.$
The selector $q_\mathit{range\_check}$ is only used in the optimized version.
$$
\begin{array}{|c|c|c|c|}
\hline
z & q_\mathit{lookup} & q_\mathit{running} & q_\mathit{range\_check} \\\hline
\hline
Expand All @@ -45,23 +69,26 @@ z_n & 0 & 0 & 0 \\\hline
$$

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})$$
- Non-optimized: $$q_\mathit{lookup} \cdot q_\mathit{running} \cdot (z_i - 2^K \cdot z_{i+1})~\text{belongs to}~table_{idx}$$
- Optimized: $$q_\mathit{lookup} \cdot (1 - q_\mathit{range\_check}) \cdot q_\mathit{running} \cdot (z_i - 2^K \cdot z_{i+1})~\text{belongs to}~table_{idx}$$

### Correct number of bits
### Short range check
In the short range check, the field element is directly witnessed.
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|l|}
\begin{array}{|c|c|c|c|}
\hline
\textsf{word} & q_\mathit{lookup} & q_\mathit{running} & q_\mathit{bitshift} & q_\mathit{range\_check}\\\hline
\textsf{word} & q_\mathit{lookup} & q_\mathit{running} & q_\mathit{bitshift} \\\hline
\hline
\alpha & 1 & 0 & 0 & 0 \\\hline
\alpha' & 1 & 0 & 1 & 0 \\\hline
2^{K-n} & 0 & 0 & 0 & 0 \\\hline
\alpha & 1 & 0 & 0 \\\hline
\alpha' & 1 & 0 & 1 \\\hline
2^{K-n} & 0 & 0 & 0 \\\hline
\end{array}
$$

Expand All @@ -74,24 +101,45 @@ $$
\end{array}
$$

### Short range check with 1 fixed column (optimized)
In the optimized version, we move $2^{K-n} $ into a fixed column.

$$
\begin{array}{|c|c|c|c|c|c|}
\hline
\textsf{word} & q_\mathit{lookup} & q_\mathit{running} & q_\mathit{bitshift} & q_\mathit{range\_check}& fixed\_col\\\hline
\hline
\alpha & 1 & 0 & 0 & 0 & 0 \\\hline
\alpha' & 1 & 0 & 1 & 0 & 2^{K-n}\\\hline
\end{array}
$$


The lookup input expression is:
$$q_\mathit{lookup} \cdot (1 - q_\mathit{range\_check}) \cdot (1 - q_\mathit{running}) \cdot \textsf{word}$$
- Non-optimized: $$q_\mathit{lookup} \cdot (1 - q_\mathit{running}) \cdot \textsf{word}~\text{belongs to}~table_{idx}$$
- Optimized: $$q_\mathit{lookup} \cdot (1 - q_\mathit{range\_check}) \cdot (1 - q_\mathit{running}) \cdot \textsf{word}~\text{belongs to}~table_{idx}$$

## Optimized lookup decomposition on 4 and 5 bits
## Optimized short range check 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.
We further optimize the short range check for 4 and 5 bits, whereby the field element is directly witnessed. Using one 4 (or 5)-bit lookup table, we can constrain a field element
$\alpha$ to be 4 (or 5)-bit.

### Lookup table
This optimization adds some rows and one column in the lookup table. The full changes are as follows.

- Added $2^4 + 2^5$ rows in the lookup table
- Added a table_range_check column in the lookup table
- Added 2 selectors: $q_\mathit{range\_check\_4}, q_\mathit{range\_check\_5}$
- Optimized range check on 1 row

### Lookup table (in the optimized version)

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|l|}
\hline
table_{idx} & table_x & table_y & table_{range-check-tag} \\\hline
table_{idx} & table_x & table_y & \text{table\_{range}\_{check}} \\\hline
0 & x_{P[0]} & y_{P[0]} & 0 \\\hline
1 & x_{P[1]} & y_{P[1]} & 0 \\\hline
\vdots & \vdots & \vdots & \vdots \\\hline
Expand All @@ -108,8 +156,6 @@ $$
$$




### 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.
Expand All @@ -124,42 +170,61 @@ q_\mathit{range\_check\_4} & q_\mathit{range\_check\_5} & q_\mathit{range\_check
0 & 1 & 1 & 5 \\\hline
1 & 0 & 1 & 4\\\hline
0 & 0 & 0 & 0 \\\hline
1 & 1 & 1 & 5 \\\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\}$.
Each 4-bit element $\beta$ is range-constrained by a lookup in the lookup table with $\text{table\_{range}\_{check}} = 4$ and $table_{idx}\in \{ 2^{10},\dots, 2^{10} + 2^{4}-1\}$.
Each 5-bit element $\gamma$ is range-constrained by a lookup in the lookup table with $\text{table\_{range}\_{check}} = 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
z_{cur} & num_\mathit{bits} & q_\mathit{lookup} & q_\mathit{range\_check} \\\hline
\beta &4 & 1 & 1 \\\hline
\gamma & 5 & 1 & 1 \\\hline
\end{array}
$$

We have two lookup input expressions:
$$q_\mathit{lookup} \cdot q_\mathit{range\_check}\cdot z_{cur} ~\text{belongs to}~table_{idx}$$
$$q_\mathit{lookup} \cdot q_\mathit{range\_check} \cdot num_\mathit{bits}~\text{belongs to}~\text{table\_{range}\_{check}} $$

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

### Non-optimized lookup expression
$$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)~\text{belongs to}~table_{idx}$$

## 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:
### Optimized lookup expression

#### 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).
$$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 z_{cur} \right]~\text{belongs to}~table_{idx}$$
where $z_i$ and $\textsf{word}$ are the same cell as $z_{cur}$ (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}$$
$$q_\mathit{lookup} \cdot q_\mathit{range\_check} \cdot num_\mathit{bits}~\text{belongs to}~\text{table\_{range}\_{check}}$$
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 lookup decomposition for less than 4 bits
### Remark
The lookup range checks affected by the selector values are summarized as follows:
$$
\begin{array}{|c|c|c|c|}
\hline
q_\mathit{lookup} & q_\mathit{running} & q_\mathit{range\_check} & Remarks \\\hline
0 & \text{0 or 1} & \text{0 or 1} & \text{No range check} \\\hline
1 & 1 & 0 & \text{Running sum decomposition} ((z_{i} - 2^K \cdot z_{i+1}) ~\text{is on 10 bits}) \\\hline
1 & 0 & 0 & \text{Short range check} (z_{cur} ~\text{is on 10 bits}) \\\hline
1 & \text{0 or 1} & 1 & \text{Optimized short range check on 4 or 5 bits} \\\hline
\end{array}
$$

## 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}).$$



46 changes: 34 additions & 12 deletions book/src/design/gadgets/sinsemilla.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -180,25 +180,47 @@ $$
$$

### Generator lookup table
The Sinsemilla circuit makes use of $2^{10}$ pre-computed random generators. These are loaded into a lookup table:
The Sinsemilla circuit makes use of pre-computed random generators. These are loaded into a lookup table.
We implemented two variants of lookup tables for range checks: [non-optimized](https://zcash.github.io/halo2/design/gadgets/decomposition.html#lookup-decomposition) and [optimized versions](https://zcash.github.io/halo2/design/gadgets/decomposition.html#lookup-table-in-the-optimized-version).

### Hash optimization
The optimization suggests using a witness point (instead of a public point) as the initial point (Q) of the hash.
In the optimized version, the y coordinate of $Q$ ($y_Q$) should be placed in an advice column, not in the fixed column.
This optimization involves splitting the evaluation of the ZEC hash and the ZSA hash into a common prefix and a different suffix,
in order to evaluate the hash on the common prefix only once. To do that, we have to implement a gadget to be able to
evaluate a hash from a private initial point (instead of a public initial point). We also need a multiplexer gate that takes
as input (choice, left, right) where left and right are non-identity points and returns left if choice=0 and right if
choice=1. The [graph](https://zcash.github.io/halo2/design/gadgets/cond_swap.html) shows where each new gadget (hash from private initial point and MUX on non-identity points) will be used.


### Layout (non-optimized)
$$
\begin{array}{|c|c|c|}
\begin{array}{|c|c|c|c|c|c|c|c|c|c|}
\hline
table_{idx} & table_x & table_y \\\hline
0 & x_{P[0]} & y_{P[0]} \\\hline
1 & x_{P[1]} & y_{P[1]} \\\hline
2 & x_{P[2]} & y_{P[2]} \\\hline
\vdots & \vdots & \vdots \\\hline
2^{10} - 1 & x_{P[2^{10}-1]} & y_{P[2^{10}-1]} \\\hline
\text{Step} & x_A & x_P & bits & \lambda_1 & \lambda_2 & q_{S1} & q_{S2} & q_{S4} & \textsf{fixed\_y\_Q}\\\hline
0 & x_Q & x_{P[m_1]} & z_0 & \lambda_{1,0} & \lambda_{2,0} & 1 & 1 & 1 & y_Q \\\hline
1 & x_{A,1} & x_{P[m_2]} & z_1 & \lambda_{1,1} & \lambda_{2,1} & 1 & 1 & 0 & 0 \\\hline
2 & x_{A,2} & x_{P[m_3]} & z_2 & \lambda_{1,2} & \lambda_{2,2} & 1 & 1 & 0 & 0 \\\hline
\vdots & \vdots & \vdots & \vdots & \vdots & \vdots & 1 & 1 & 0 & 0 \\\hline
n-1 & x_{A,n-1} & x_{P[m_n]} & z_{n-1} & \lambda_{1,n-1} & \lambda_{2,n-1} & 1 & 0 & 0 & 0 \\\hline
0' & x'_{A,0} & x_{P[m'_1]} & z'_0 & \lambda'_{1,0} & \lambda'_{2,0} & 1 & 1 & 0 & 0 \\\hline
1' & x'_{A,1} & x_{P[m'_2]} & z'_1 & \lambda'_{1,1} & \lambda'_{2,1} & 1 & 1 & 0 & 0 \\\hline
2' & x'_{A,2} & x_{P[m'_3]} & z'_2 & \lambda'_{1,2} & \lambda'_{2,2} & 1 & 1 & 0 & 0 \\\hline
\vdots & \vdots & \vdots & \vdots & \vdots & \vdots & 1 & 1 & 0 & 0 \\\hline
n-1' & x'_{A,n-1} & x_{P[m'_n]} & z'_{n-1} & \lambda'_{1,n-1} & \lambda'_{2,n-1} & 1 & 2 & 0 & 0 \\\hline
n' & x'_{A,n} & & & y_{A,n} & & 0 & 0 & 0 & 0 \\\hline
\end{array}
$$
Assign the coordinates of the initial public point $Q$ to $x_A$ and $\textsf{fixed\_y\_Q}$.
$x_Q$, $z_0$, $z'_0$, etc. are copied in using equality constraints.


### Layout
### Layout (optimized)
$$
\begin{array}{|c|c|c|c|c|c|c|c|c|c|}
\hline
\text{Step} & x_A & x_P & bits & \lambda_1 & \lambda_2 & q_{S1} & q_{S2} & q_{S4} \\\hline
-1 & & y_{Q} & & & & 0 & 0 & 1 \\\hline
& & y_{Q} & & & & & & \\\hline
0 & x_Q & x_{P[m_1]} & z_0 & \lambda_{1,0} & \lambda_{2,0} & 1 & 1 & 1 \\\hline
1 & x_{A,1} & x_{P[m_2]} & z_1 & \lambda_{1,1} & \lambda_{2,1} & 1 & 1 & 0 \\\hline
2 & x_{A,2} & x_{P[m_3]} & z_2 & \lambda_{1,2} & \lambda_{2,2} & 1 & 1 & 0 \\\hline
Expand All @@ -212,7 +234,8 @@ $$
n' & x'_{A,n} & & & y_{A,n} & & 0 & 0 & 0 \\\hline
\end{array}
$$
Assign the coordinates of the initial private point $Q$ to $x_A$ and $x_P$.
Assign the coordinates of the initial private point $Q$ to $x_A$ and $x_P$.
$y_Q$ is moved to $x_P$ advice column because this column already used the three rotations prev, curr and next.
$x_Q$, $z_0$, $z'_0$, etc. are copied in using equality constraints.

### Optimized Sinsemilla gate
Expand All @@ -231,7 +254,6 @@ The Halo 2 circuit API can automatically substitute $y_{P,i}$, $x_{R,i}$, $Y_{A,
$Y_{A,i+1}$, so we don't need to do that manually.

- $x_{A,0} = x_Q$
- $x_{P,-1} = y_Q$
- $2 \cdot y_Q = Y_{A,0}$
- for $i$ from $0$ up to $n-1$:
- $(m_{i+1},\, x_{P,i},\, y_{P,i}) \in \mathcal{P}$
Expand Down

0 comments on commit b9949d0

Please sign in to comment.