zec
/
halo2
mirror of https://github.com/zcash/halo2.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #573 from zcash/str4d/chip-review 

Changes from `halo2_gadgets` review
This commit is contained in:
str4d 2022-05-10 22:54:45 +01:00 committed by GitHub
parent bdf84a5bb5 91e1106a1e
commit 50921f95f7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
48 changed files with 1260 additions and 627 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
book/macros.txt
View File

@ -20,6 +20,7 @@
# Circuit constraint helper methods
\BoolCheck:{\texttt{bool\_check}({#1})}
\Ternary:{\texttt{ternary}({{#1}, {#2}, {#3}})}
\RangeCheck:{\texttt{range\_check}({#1, #2})}
\ShortLookupRangeCheck:{\texttt{short\_lookup\_range\_check}({#1})}

1
book/src/SUMMARY.md
View File

@ -28,6 +28,7 @@
- [Selector combining](design/implementation/selector-combining.md)
- [Gadgets](design/gadgets.md)
- [Elliptic curve cryptography](design/gadgets/ecc.md)
- [Witnessing points](design/gadgets/ecc/witnessing-points.md)
- [Incomplete and complete addition](design/gadgets/ecc/addition.md)
- [Fixed-base scalar multiplication](design/gadgets/ecc/fixed-base-scalar-mul.md)
- [Variable-base scalar multiplication](design/gadgets/ecc/var-base-scalar-mul.md)

2
book/src/design/gadgets/decomposition.md
View File

@ -61,7 +61,7 @@ $$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
2 & q_\mathit{bitshift} \cdot (\alpha' - (\alpha \cdot 2^{K - n})) \\\hline
2 & q_\mathit{bitshift} \cdot ((\alpha \cdot 2^{K - n}) - \alpha') \\\hline
\end{array}
$$

50
book/src/design/gadgets/ecc.md
View File

@ -0,0 +1,50 @@
# Elliptic Curves
## `EccChip`
`halo2_gadgets` provides a chip that implements `EccInstructions` using 10 advice columns.
The chip is currently restricted to the Pallas curve, but will be extended to support the
[Vesta curve](https://github.com/zcash/halo2/issues/578) in the near future.
### Chip assumptions
A non-exhaustive list of assumptions made by `EccChip`:
- $0$ is not an $x$-coordinate of a valid point on the curve.
- Holds for Pallas because $5$ is not square in $\mathbb{F}_q$.
- $0$ is not a $y$-coordinate of a valid point on the curve.
- Holds for Pallas because $-5$ is not a cube in $\mathbb{F}_q$.
### Layout
The following table shows how columns are used by the gates for various chip sub-areas:
- $W$ - witnessing points.
- $AI$ - incomplete point addition.
- $AC$ - complete point addition.
- $MF$ - Fixed-base scalar multiplication.
- $MVI$ - variable-base scalar multiplication, incomplete rounds.
- $MVC$ - variable-base scalar multiplication, complete rounds.
- $MVO$ - variable-base scalar multiplication, overflow check.
$$
\begin{array}{|c||c|c|c|c|c|c|c|c|c|c|}
\hline
\text{Sub-area} & a_0 & a_1 & a_2 & a_3 & a_4 & a_5 & a_6 & a_7 & a_8 & a_9 \\\hline
\hline
W & x & y \\\hline
\hline
AI & x_p & y_p & x_q & y_q \\\hline
& & & x_r & y_r \\\hline
\hline
AC & x_p & y_p & x_q & y_q & \lambda & \alpha & \beta & \gamma & \delta & \\\hline
& & & x_r & y_r \\\hline
\hline
MF & x_p & y_p & x_q & y_q & \text{window} & u \\\hline
& & & x_r & y_r \\\hline
\hline
MVI & x_p & y_p & \lambda_2^{lo} & x_A^{hi} & \lambda_1^{hi} & \lambda_2^{hi} & z^{lo} & x_A^{lo} & \lambda_1^{lo} & z^{hi} \\\hline
\hline
MVC & x_p & y_p & x_q & y_q & \lambda & \alpha & \beta & \gamma & \delta & z^{complete} \\\hline
& & & x_r & y_r \\\hline
\end{array}
$$

22
book/src/design/gadgets/ecc/addition.md
View File

@ -41,6 +41,16 @@ So we get the constraints:
and so cannot be used with arbitrary inputs.
- $(y_r + y_q) \cdot (x_p - x_q) - (y_p - y_q) \cdot (x_q - x_r) = 0.$
### Constraints
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
4 & q_\text{add-incomplete} \cdot \left( (x_r + x_q + x_p) \cdot (x_p - x_q)^2 - (y_p - y_q)^2 \right) = 0 \\\hline
3 & q_\text{add-incomplete} \cdot \left( (y_r + y_q) \cdot (x_p - x_q) - (y_p - y_q) \cdot (x_q - x_r) \right) = 0 \\\hline
\end{array}
$$
## Complete addition
@ -92,7 +102,7 @@ $
### Constraints
$$
\begin{array}{|c|rcl|l|}
\begin{array}{|c|lcl|l|}
\hline
\text{Degree} & \text{Constraint}\hspace{7em} &&& \text{Meaning} \\\hline
4 & q_\mathit{add} \cdot (x_q - x_p) \cdot ((x_q - x_p) \cdot \lambda - (y_q - y_p)) &=& 0 & x_q \neq x_p \implies \lambda = \frac{y_q - y_p}{x_q - x_p} \\\hline \\[-2.3ex]
@ -193,16 +203,16 @@ $$
& \text{Therefore:} \\
& \hspace{2em} x_p = 0 \implies (x_r, y_r) = (x_q, y_q). \\
& \\
5.\text{ a)} & (1 - x_q \cdot \beta) \cdot (x_r - x_p) = 0 \\
\text{ b)} & (1 - x_q \cdot \beta) \cdot (y_r - y_p) = 0 \\
5.\text{ a)} & (1 - x_q \cdot \gamma) \cdot (x_r - x_p) = 0 \\
\text{ b)} & (1 - x_q \cdot \gamma) \cdot (y_r - y_p) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } 1 - x_q \cdot \beta &= 0 \\
\text{At least one of } 1 - x_q \cdot \gamma &= 0 \\
\text{or } x_r - x_p &= 0
\end{aligned} \\
& \text{must be satisfied for constraint (a) to be satisfied.} \\
& \\
& \text{If } x_q = 0 \text{ then } 1 - x_q \cdot \beta = 0 \text{ has no solutions for } \beta, \\
& \text{If } x_q = 0 \text{ then } 1 - x_q \cdot \gamma = 0 \text{ has no solutions for } \gamma, \\
& \text{and so it must be that } x_r - x_p = 0. \\
& \\
& \text{Similarly, constraint (b) imposes that if } x_q = 0 \\
@ -221,7 +231,7 @@ $$
& \text{must be satisfied for constraint (a) to be satisfied,} \\
& \text{and similarly replacing } x_r \text{ by } y_r. \\
& \\
& \text{If } x_r \neq 0 \text{ or } y_r = 0, \text{ then it must be that } 1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta = 0. \\
& \text{If } x_r \neq 0 \text{ or } y_r \neq 0, \text{ then it must be that } 1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta = 0. \\
& \\
& \text{However, if } x_q = x_p \wedge y_q = -y_p, \text{ then there are no solutions for } \alpha \text { and } \delta. \\
& \\

25
book/src/design/gadgets/ecc/fixed-base-scalar-mul.md
View File

@ -13,22 +13,15 @@ A $255$-bit scalar from $\mathbb{F}_q$. We decompose a full-width scalar $\alpha
$$\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})$.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
9 & q_\text{scalar-fixed} \cdot \left(\sum\limits_{i=0}^7{w - i}\right) = 0 \\\hline
\end{array}
$$
The scalar multiplication will be computed correctly for $k_{0..84}$ representing any
integer in the range $[0, 2^{255})$ - that is, the scalar is allowed to be non-canonical.
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{decompose-base-field} \cdot \RangeCheck{\text{word}}{2^3} = 0 \\\hline
9 & q_\texttt{mul\_fixed\_full} \cdot \RangeCheck{\text{word}}{2^3} = 0 \\\hline
\end{array}
$$
where $\RangeCheck{\text{word}}{\texttt{range}} = \text{word} \cdot (1 - \text{word}) \cdots (\texttt{range} - 1 - \text{word}).$
@ -48,7 +41,7 @@ $$
\hline
\text{Degree} & \text{Constraint} \\\hline
5 & q_\text{canon-base-field} \cdot \RangeCheck{\alpha_1}{2^2} = 0 \\\hline
3 & q_\text{canon-base-field} \cdot \RangeCheck{\alpha_2}{2^1} = 0 \\\hline
3 & q_\text{canon-base-field} \cdot \BoolCheck{\alpha_2} = 0 \\\hline
2 & q_\text{canon-base-field} \cdot \left(z_{84} - (\alpha_1 + \alpha_2 \cdot 2^2)\right) = 0 \\\hline
\end{array}
$$
@ -74,9 +67,10 @@ $$
\begin{array}{|c|l|l|}
\hline
\text{Degree} & \text{Constraint} & \text{Comment} \\\hline
2 & q_\text{canon-base-field} \cdot (\alpha_0' - (\alpha_0 + 2^{130} - t_\mathbb{P})) = 0 \\\hline
3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot \alpha_1 = 0 & \alpha_2 = 1 \implies \alpha_1 = 0 \\\hline
3 & q_\text{canon-base-field} \cdot \alpha_2 \cdot \textsf{alpha\_0\_hi\_120} = 0 & \text{Constrain $\alpha_0$ to be a $132$-bit value} \\\hline
4 & q_\text{canon-base-field} \cdot \alpha_2 \cdot k_{43} \cdot (1 - k_{43}) = 0 & \text{Constrain $\alpha_0[130..\!\!=\!\!131]$ to $0$} \\\hline
4 & q_\text{canon-base-field} \cdot \alpha_2 \cdot \BoolCheck{k_{43}} = 0 & \text{Constrain $\alpha_0[130..\!\!=\!\!131]$ to $0$} \\\hline
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}
$$
@ -102,8 +96,8 @@ $$
\begin{array}{|c|l|l|}
\hline
\text{Degree} & \text{Constraint} & \text{Comment} \\\hline
3 & q_\text{scalar-fixed-short} \cdot \BoolCheck{k_{21}} = 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
3 & q_\texttt{mul\_fixed\_short} \cdot \BoolCheck{k_{21}} = 0 & \text{The last window must be a single bit.}\\\hline
3 & q_\texttt{mul\_fixed\_short} \cdot \left(s^2 - 1\right) = 0 &\text{The sign must be $1$ or $-1$.}\\\hline
\end{array}
$$
where $\BoolCheck{x} = x \cdot (1 - x)$.
@ -174,7 +168,8 @@ $$
\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
3 & q_\texttt{mul\_fixed\_short} \cdot \left(P'_y - P_y\right) \cdot \left(P'_y + P_y\right) = 0 \\\hline
3 & q_\texttt{mul\_fixed\_short} \cdot \left(s \cdot P'_y - P_y\right) = 0 \\\hline
\end{array}
$$

91
book/src/design/gadgets/ecc/var-base-scalar-mul.md
View File

@ -88,7 +88,7 @@ for i from 2 down to 0 {
return (k_0 = 0) ? (Acc + (-T)) : Acc // complete addition
```
## Constraint program for optimized double-and-add (incomplete addition)
## Constraint program for optimized double-and-add
Define a running sum $\mathbf{z_j} = \sum_{i=j}^{n} (\mathbf{k}_{i} \cdot 2^{i-j})$, where $n = 254$ and:
$$
@ -108,13 +108,13 @@ $\begin{array}{l}
\hspace{1.5em} x_{P,i} = x_T \\
\hspace{1.5em} y_{P,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)} \\
\hspace{1.5em} \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) = y_{A,i} - y_{P,i} \\
\hspace{1.5em} \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{P,i} \\
\hspace{1.5em} x_{R,i} = \lambda_{1,i}^2 - x_{A,i} - x_{P,i} \\
\hspace{1.5em} (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) = 2 y_{\mathsf{A},i} \\
\hspace{1.5em} \lambda_{2,i}^2 = x_{A,i-1} + x_{R,i} + x_{A,i} \\
\hspace{1.5em} \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A,i-1}, \\
\hspace{1.5em} \lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A,i-1}. \\
\end{array}$
where $x_{R,i} = (\lambda_{1,i}^2 - x_{A,i} - x_T).$ The helper $\BoolCheck{x} = x \cdot (1 - x)$.
The helper $\BoolCheck{x} = x \cdot (1 - x)$.
After substitution of $x_{P,i}, y_{P,i}, x_{R,i}, y_{A,i}$, and $y_{A,i-1}$, this becomes:
$\begin{array}{l}
@ -154,8 +154,8 @@ Output $(x_{A,0}, y_{A,0}) + B$.
(Note that $(0, 0)$ represents $\mathcal{O}$.)
## Incomplete addition
### Circuit design
We need six advice columns to witness $(x_T, y_T, \lambda_1, \lambda_2, x_{A,i}, \mathbf{z}_i)$. However, since $(x_T, y_T)$ are the same, we can perform two incomplete additions in a single row, reusing the same $(x_T, y_T)$. We split the scalar bits used in incomplete addition into $hi$ and $lo$ halves and process them in parallel. This means that we effectively have two for loops:
- the first, covering the $hi$ half for $i$ from $254$ down to $130$, with a special case at $i = 130$; and
- the second, covering the $lo$ half for the remaining $i$ from $129$ down to $4$, with a special case at $i = 4$.
@ -169,7 +169,7 @@ $$
x_T & y_T & \mathbf{z}_{253} & x_{A,253} & \lambda_{1,253} & \lambda_{2,253} & 0 & 1 & 0 & \mathbf{z}_{128} & x_{A,128} & \lambda_{1,128} & \lambda_{2,128} & 0 & 1 & 0 \\\hline
\vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots \\\hline
x_T & y_T & \mathbf{z}_{130} & x_{A,130} & \lambda_{1,130} & \lambda_{2,130} & 0 & 0 & 1 & \mathbf{z}_5 & x_{A,5} & \lambda_{1,5} & \lambda_{2,5} & 0 & 1 & 0 \\\hline
& & & x_{A,129} & y_{A,129} & & & & & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} & 0 & 0 & 1 \\\hline
x_T & y_T & & x_{A,129} & y_{A,129} & & & & & \mathbf{z}_4 & x_{A,4} & \lambda_{1,4} & \lambda_{2,4} & 0 & 0 & 1 \\\hline
& & & & & & & & & & x_{A,3} & y_{A,3} & & & & \\\hline
\end{array}
@ -183,7 +183,7 @@ $$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
3 & q_1 \cdot \left(y_{A,n}^\text{witnessed} - y_{A,n}\right) = 0 \\\hline
4 & q_1 \cdot \left(y_{A,n}^\text{witnessed} - y_{A,n}\right) = 0 \\\hline
\end{array}
$$
where
@ -205,13 +205,14 @@ $$
2 & q_2 \cdot \left(y_{T,cur} - y_{T,next}\right) = 0 \\\hline
3 & q_2 \cdot \BoolCheck{\mathbf{k}_i} = 0, \text{ where } \mathbf{k}_i = \mathbf{z}_{i} - 2\mathbf{z}_{i+1} \\\hline
4 & q_2 \cdot \left(\lambda_{1,i} \cdot (x_{A,i} - x_{T,i}) - y_{A,i} + (2\mathbf{k}_i - 1) \cdot y_{T,i}\right) = 0 \\\hline
3 & q_2 \cdot \left(\lambda_{2,i}^2 - x_{A,i-1} - \lambda_{1,i}^2 + x_{T,i}\right) = 0 \\\hline
3 & q_2 \cdot \left(\lambda_{2,i}^2 - x_{A,i-1} - x_{R,i} - x_{A,i}\right) = 0 \\\hline
3 & q_2 \cdot \left(\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) - y_{A,i} - y_{A,i-1}\right) = 0 \\\hline
\end{array}
$$
where
$$
\begin{aligned}
x_{R,i} &= \lambda_{1,i}^2 - x_{A,i} - x_T, \\
y_{A,i} &= \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2}, \\
y_{A,i-1} &= \frac{(\lambda_{1,i-1} + \lambda_{2,i-1}) \cdot (x_{A,i-1} - (\lambda_{1,i-1}^2 - x_{A,i-1} - x_T))}{2}, \\
\end{aligned}
@ -225,18 +226,80 @@ $$
\text{Degree} & \text{Constraint} \\\hline
3 & q_3 \cdot \BoolCheck{\mathbf{k}_i} = 0, \text{ where } \mathbf{k}_i = \mathbf{z}_{i} - 2\mathbf{z}_{i+1} \\\hline
4 & q_3 \cdot \left(\lambda_{1,i} \cdot (x_{A,i} - x_{T,i}) - y_{A,i} + (2\mathbf{k}_i - 1) \cdot y_{T,i}\right) = 0 \\\hline
3 & q_3 \cdot \left(\lambda_{2,i}^2 - x_{A,i-1} - \lambda_{1,i}^2 + x_{T,i}\right) = 0 \\\hline
3 & q_3 \cdot \left(\lambda_{2,i}^2 - x_{A,i-1} - x_{R,i} - x_{A,i}\right) = 0 \\\hline
3 & q_3 \cdot \left(\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) - y_{A,i} - y_{A,i-1}^\text{witnessed}\right) = 0 \\\hline
\end{array}
$$
where
$$
\begin{aligned}
x_{R,i} &= \lambda_{1,i}^2 - x_{A,i} - x_T, \\
y_{A,i} &= \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2},\\
y_{A,i-1}^\text{witnessed} &\text{ is witnessed.}
\end{aligned}
$$
## Complete addition
We reuse the [complete addition](addition.md#complete-addition) constraints to implement
the final $c$ rounds of double-and-add. This requires two rows per round because we need
9 advice columns for each complete addition. In the 10th advice column we stash the other
cells that we need to correctly implement the double-and-add:
- The base $y$ coordinate, so we can conditionally negate it as input to one of the
complete additions.
- The running sum, which we constrain over two rows instead of sequentially.
### Layout
$$
\begin{array}{|c|c|c|c|c|c|c|c|c|c|c|}
a_0 & a_1 & a_2 & a_3 & a_4 & a_5 & a_6 & a_7 & a_8 & a_9 & q_\texttt{mul\_decompose\_var} \\\hline
x_T & y_p & x_A & y_A & \lambda_1 & \alpha_1 & \beta_1 & \gamma_1 & \delta_1 & z_{i+1} & 0 \\\hline
x_A & y_A & x_q & y_q & \lambda_2 & \alpha_2 & \beta_2 & \gamma_2 & \delta_2 & y_T & 1 \\\hline
& & x_r & y_r & & & & & & z_i & 0 \\\hline
\end{array}
$$
### Constraints <a name="complete-gate">
In addition to the complete addition constraints, we define the following gate:
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
& q_\texttt{mul\_decompose\_var} \cdot \BoolCheck{\mathbf{k}_i} = 0 \\\hline
& q_\texttt{mul\_decompose\_var} \cdot \Ternary{\mathbf{k}_i}{y_T - y_p}{y_T + y_p} = 0 \\\hline
\end{array}
$$
where $\mathbf{k}_i = \mathbf{z}_{i} - 2\mathbf{z}_{i+1}$.
## LSB
### Layout
$$
\begin{array}{|c|c|c|c|c|c|c|c|c|c|c|}
a_0 & a_1 & a_2 & a_3 & a_4 & a_5 & a_6 & a_7 & a_8 & a_9 & q_\texttt{mul\_lsb} \\\hline
x_p & y_p & x_A & y_A & \lambda & \alpha & \beta & \gamma & \delta & z_1 & 1 \\\hline
x_T & y_T & x_r & y_r & & & & & & z_0 & 0 \\\hline
\end{array}
$$
### Constraints <a name="lsb-gate">
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
& q_\texttt{mul\_lsb} \cdot \BoolCheck{\mathbf{k}_0} = 0 \\\hline
& q_\texttt{mul\_lsb} \cdot \Ternary{\mathbf{k}_0}{x_p}{x_p - x_T} = 0 \\\hline
& q_\texttt{mul\_lsb} \cdot \Ternary{\mathbf{k}_0}{y_p}{y_p + y_T} = 0 \\\hline
\end{array}
$$
where $\mathbf{k}_0 = \mathbf{z}_0 - 2\mathbf{z}_1$.
## Overflow check
$\mathbf{z}_i$ cannot overflow for any $i \geq 1$, because it is a weighted sum of bits only up to $2^{n-1} = 2^{253}$, which is smaller than $p$ (and also $q$).
@ -318,11 +381,11 @@ $$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
2 & \text{q\_mul}^\text{overflow} \cdot \left(s - (\alpha + \mathbf{k}_{254} \cdot 2^{130})\right) = 0 \\\hline
2 & \text{q\_mul}^\text{overflow} \cdot \left(\mathbf{z}_0 - \alpha - t_q\right) = 0 \\\hline
3 & \text{q\_mul}^\text{overflow} \cdot \left(\mathbf{k}_{254} \cdot (\mathbf{z}_{130} - 2^{124})\right) = 0 \\\hline
3 & \text{q\_mul}^\text{overflow} \cdot \left(\mathbf{k}_{254} \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}\right) = 0 \\\hline
5 & \text{q\_mul}^\text{overflow} \cdot \left((1 - \mathbf{k}_{254}) \cdot (1 - \mathbf{z}_{130} \cdot \eta) \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}\right) = 0 \\\hline
2 & q_\texttt{mul\_overflow} \cdot \left(s - (\alpha + \mathbf{k}_{254} \cdot 2^{130})\right) = 0 \\\hline
2 & q_\texttt{mul\_overflow} \cdot \left(\mathbf{z}_0 - \alpha - t_q\right) = 0 \\\hline
3 & q_\texttt{mul\_overflow} \cdot \left(\mathbf{k}_{254} \cdot (\mathbf{z}_{130} - 2^{124})\right) = 0 \\\hline
3 & q_\texttt{mul\_overflow} \cdot \left(\mathbf{k}_{254} \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}\right) = 0 \\\hline
5 & q_\texttt{mul\_overflow} \cdot \left((1 - \mathbf{k}_{254}) \cdot (1 - \mathbf{z}_{130} \cdot \eta) \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}\right) = 0 \\\hline
\end{array}
$$
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.

35
book/src/design/gadgets/ecc/witnessing-points.md Normal file
View File

@ -0,0 +1,35 @@
# Witnessing points
We represent elliptic curve points in the circuit in their affine representation $(x, y)$.
The identity is represented as the pseudo-coordinate $(0, 0)$, which we
[assume](../ecc.md#chip-assumptions) is not a valid point on the curve.
## Non-identity points
To constrain a coordinate pair $(x, y)$ as representing a valid point on the curve, we
directly check the curve equation. For Pallas and Vesta, this is:
$$y^2 = x^3 + 5$$
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
4 & q_\text{point}^\text{non-id} \cdot (y^2 - x^3 - 5) = 0 \\\hline
\end{array}
$$
## Points including the identity
To allow $(x, y)$ to represent either a valid point on the curve, or the pseudo-coordinate
$(0, 0)$, we define a separate gate that enforces the curve equation check unless both $x$
and $y$ are zero.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
5 & (q_\text{point} \cdot x) \cdot (y^2 - x^3 - 5) = 0 \\\hline
5 & (q_\text{point} \cdot y) \cdot (y^2 - x^3 - 5) = 0 \\\hline
\end{array}
$$

146
book/src/design/gadgets/sinsemilla.md
View File

@ -46,7 +46,44 @@ Note that unlike a simple Pedersen commitment, this commitment scheme ($\textsf{
## Efficient implementation
The aim of the design is to optimize the number of bits that can be processed for each step of the algorithm (which requires a doubling and addition in $\mathbb{G}$) for a given table size. Using a single table of size $2^k$ group elements, we can process $k$ bits at a time.
## Constraint program
### Incomplete addition
In each step of Sinsemilla we want to compute $A_{i+1} := (A_i \;⸭\; P_i) \;⸭\; A_i$. Let
$R_i := A_i \;⸭\; P_i$ be the intermediate result such that $A_{i+1} := A_i \;⸭\; R_i$.
Recalling the [incomplete addition formulae](ecc/addition.md#incomplete-addition):
$$
\begin{aligned}
x_3 &= \left(\frac{y_1 - y_2}{x_1 - x_2}\right)^2 - x_1 - x_2 \\
y_3 &= \frac{y_1 - y_2}{x_1 - x_2} \cdot (x_1 - x_3) - y_1 \\
\end{aligned}
$$
Let $\lambda = \frac{y_1 - y_2}{x_1 - x_2}$. Substituting the coordinates for each of the
incomplete additions in turn, and rearranging, we get
$$
\begin{aligned}
\lambda_{1,i} &= \frac{y_{A,i} - y_{P,i}}{x_{A,i} - x_{P,i}} \\
&\implies y_{A,i} - y_{P,i} = \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) \\
&\implies y_{P,i} = y_{A,i} - \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) \\
x_{R,i} &= \lambda_{1,i}^2 - x_{A,i} - x_{P,i} \\
y_{R,i} &= \lambda_{1,i} \cdot (x_{A,i} - x_{R,i}) - y_{A,i} \\
\end{aligned}
$$
and
$$
\begin{aligned}
\lambda_{2,i} &= \frac{y_{A,i} - y_{R,i}}{x_{A,i} - x_{R,i}} \\
&\implies y_{A,i} - y_{R,i} = \lambda_{2,i} \cdot (x_{A,i} - x_{R,i}) \\
&\implies y_{A,i} - \left( \lambda_{1,i} \cdot (x_{A,i} - x_{R,i}) - y_{A,i} \right) = \lambda_{2,i} \cdot (x_{A,i} - x_{R,i}) \\
&\implies 2 \cdot y_{A,i} = (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) \\
x_{A,i+1} &= \lambda_{2,i}^2 - x_{A,i} - x_{R,i} \\
y_{A,i+1} &= \lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) - y_{A,i}. \\
\end{aligned}
$$
### Constraint program
Let $\mathcal{P} = \left\{(j,\, x_{P[j]},\, y_{P[j]}) \text{ for } j \in \{0..2^k - 1\}\right\}$.
Input: $m_{1..=n}$. (The message words are 1-indexed here, as in the [protocol spec](https://zips.z.cash/protocol/nu5.pdf#concretesinsemillahash), but we start the loop from $i = 0$ so that $(x_{A,i}, y_{A,i})$ corresponds to $\mathsf{Acc}_i$ in the protocol spec.)
@ -70,15 +107,77 @@ We have an $n$-bit message $m = m_1 + 2^k m_2 + ... + 2^{k\cdot (n-1)} m_n$. (No
Initialise the running sum $z_0 = \alpha$ and define $z_{i + 1} := \frac{z_{i} - m_{i+1}}{2^K}$. We will end up with $z_n = 0.$
Rearranging gives us an expression for each word of the original message $m_{i+1} = z_{i} - 2^k \cdot z_{i + 1}$, which we can look up in the table.
Rearranging gives us an expression for each word of the original message
$m_{i+1} = z_{i} - 2^k \cdot z_{i + 1}$, which we can look up in the table. We position
$z_{i}$ and $z_{i + 1}$ in adjacent rows of the same column, so we can sequentially apply
the constraint across the entire message.
In other words, $z_{n-i} = \sum\limits_{h=0}^{i-1} 2^{kh} \cdot m_{h+1}$.
> For a little-endian decomposition as used here, the running sum is initialized to the scalar and ends at 0. For a big-endian decomposition as used in [variable-base scalar multiplication](https://hackmd.io/o9EzZBwxSWSi08kQ_fMIOw), the running sum would start at 0 and end with recovering the original scalar.
>
> The running sum only applies to message words within a single field element, i.e. if $n \geq \mathtt{PrimeField::NUM\_BITS}$ then we will have several disjoint running sums. A longer message can be constructed by splitting the message words across several field elements, and then running several instances of the constraints below. An additional $q_{S2}$ selector is set to $0$ for the last step of each element, except for the last element where it is set to $2$.
>
> In order to support chaining multiple field elements without a gap, we will use a slightly more complicated expression for $m_{i+1}$ that effectively forces $\mathbf{z}_n$ to zero for the last step of each element, as indicated by $q_{S2}$. This allows the cell that would have been $\mathbf{z}_n$ to be used to reinitialize the running sum for the next element.
### Efficient packing
The running sum only applies to message words within a single field element. That means if
$n \geq \mathtt{PrimeField::NUM\_BITS}$ then we will need several disjoint running sums. A
longer message can be constructed by splitting the message words across several field
elements, and then running several instances of the constraints below.
The expression for $m_{i+1}$ above requires $n + 1$ rows in the $z_{i}$ column, leaving a
one-row gap in adjacent columns and making $\mathsf{Acc}_i$ tricker to accumulate. In
order to support chaining multiple field elements without a gap, we use a slightly more
complicated expression for $m_{i+1}$ that includes a selector:
$$m_{i+1} = z_{i} - 2^k \cdot q_{run,i} \cdot z_{i+1}$$
This effectively forces $\mathbf{z}_n$ to zero for the last step of each element, which
allows the cell that would have been $\mathbf{z}_n$ to be used to reinitialize the running
sum for the next element.
With this sorted out, the incomplete addition accumulator can eliminate $y_{A,i}$ almost
entirely, by substituting for $x$ and $\lambda$ values in the current and next rows. The
two exceptions are at the start of Sinsemilla (where we need to constrain the accumulator
to have initial value $Q$), and the end (where we need to witness $y_{A,n}$ for use
outside of Sinsemilla).
### Selectors
We need a total of four logical selectors to:
- Control the Sinsemilla gate and lookup.
- Distinguish between the last message word in a running sum and its earlier words.
- Mark the start of Sinsemilla.
- Mark the end of Sinsemilla.
We use regular selector columns for the Sinsemilla gate selector $q_{S1}$ and Sinsemilla
start selector $q_{S4}.$ The other two selectors are synthesized from a single fixed
column $q_{S2}$ as follows:
$$
\begin{aligned}
q_{S3} &= q_{S2} \cdot (q_{S2} - 1) \\
q_{run} &= q_{S2} - q_{S3} \\
\end{aligned}
$$
$$
\begin{array}{|c|c|c|}
\hline
q_{S2} & q_{S3} & q_{run} \\\hline
0 & 0 & 0 \\\hline
1 & 0 & 1 \\\hline
2 & 2 & 0 \\\hline
\end{array}
$$
We set $q_{S2}$ to $1$ on most Sinsemilla rows, and $0$ for the last step of each element,
except for the last element where it is set to $2$. We can then use $q_{S3}$ to toggle
between constraining the substituted $y_{A,i+1}$ on adjacent rows, and the witnessed
$y_{A,n}$ at the end of Sinsemilla:
$$
\lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) = y_{A,i} + \frac{2 - q_{S3}}{2} \cdot y_{A,i+1} + \frac{q_{S3}}{2} \cdot y_{A,n}
$$
### Generator lookup table
The Sinsemilla circuit makes use of $2^{10}$ pre-computed random generators. These are loaded into a lookup table:
@ -95,26 +194,25 @@ $$
$$
### Layout
Note: $q_{S3}$ is synthesized from $q_{S1}$ and $q_{S2}$; it is shown here only for clarity.
$$
\begin{array}{|c|c|c|c|c|c|c|c|c|c|c|}
\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_{S3} & q_{S4} & \textsf{fixed\_y\_Q}\\\hline
0 & x_Q & x_{P[m_1]} & z_0 & \lambda_{1,0} & \lambda_{2,0} & 1 & 1 & 0 & 1 & y_Q \\\hline
1 & x_{A,1} & x_{P[m_2]} & z_1 & \lambda_{1,1} & \lambda_{2,1} & 1 & 1 & 0 & 0 & 0 \\\hline
2 & x_{A,2} & x_{P[m_3]} & z_2 & \lambda_{1,2} & \lambda_{2,2} & 1 & 1 & 0 & 0 & 0 \\\hline
\vdots & \vdots & \vdots & \vdots & \vdots & \vdots & 1 & 1 & 0 & 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 & 0 \\\hline
0' & x'_{A,0} & x_{P[m'_1]} & z'_0 & \lambda'_{1,0} & \lambda'_{2,0} & 1 & 1 & 0 & 0 & 0 \\\hline
1' & x'_{A,1} & x_{P[m'_2]} & z'_1 & \lambda'_{1,1} & \lambda'_{2,1} & 1 & 1 & 0 & 0 & 0 \\\hline
2' & x'_{A,2} & x_{P[m'_3]} & z'_2 & \lambda'_{1,2} & \lambda'_{2,2} & 1 & 1 & 0 & 0 & 0 \\\hline
\vdots & \vdots & \vdots & \vdots & \vdots & \vdots & 1 & 1 & 0 & 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 & 2 & 0 & 0 \\\hline
n' & x'_{A,n} & & & y_{A,n} & & 0 & 0 & 0 & 0 & 0 \\\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}
$$
$x_Q$, $z_0$, $z'_0$, etc. would be copied in using equality constraints.
$x_Q$, $z_0$, $z'_0$, etc. are copied in using equality constraints.
### Optimized Sinsemilla gate
$$
@ -122,12 +220,14 @@ $$
\text{For } i \in [0, n), \text{ let} &x_{R,i} &=& \lambda_{1,i}^2 - x_{A,i} - x_{P,i} \\
&Y_{A,i} &=& (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) \\
&y_{P,i} &=& Y_{A,i}/2 - \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) \\
&m_{i+1} &=& z_{i} - 2^k \cdot (q_{S2,i} - q_{S3,i}) \cdot z_{i+1} \\
&m_{i+1} &=& z_{i} - q_{run,i} \cdot z_{i+1} \cdot 2^k \\
&q_{run} &=& q_{S2} - q_{S3} \\
&q_{S3} &=& q_{S2} \cdot (q_{S2} - 1)
\end{array}
$$
The Halo 2 circuit API can automatically substitute $y_{P,i}$, $x_{R,i}$, $y_{A,i}$, and $y_{A,i+1}$, so we don't need to do that manually.
The Halo 2 circuit API can automatically substitute $y_{P,i}$, $x_{R,i}$, $Y_{A,i}$, and
$Y_{A,i+1}$, so we don't need to do that manually.
- $x_{A,0} = x_Q$
- $2 \cdot y_Q = Y_{A,0}$

117
book/src/design/gadgets/sinsemilla/merkle-crh.md
View File

@ -10,27 +10,58 @@ where:
- ${\textsf{left}\star} = \textsf{I2LEBSP}_{\ell_{\textsf{Merkle}}^{\textsf{Orchard}}}(\textsf{left})$,
- ${\textsf{right}\star} = \textsf{I2LEBSP}_{\ell_{\textsf{Merkle}}^{\textsf{Orchard}}}(\textsf{right})$,
with $\ell_{\textsf{Merkle}}^{\textsf{Orchard}} = 255.$ $\textsf{left}$ and $\textsf{right}$ are allowed to be non-canonical $255$-bit encodings.
with $\ell_{\textsf{Merkle}}^{\textsf{Orchard}} = 255.$ $\textsf{left}\star$ and
$\textsf{right}\star$ are allowed to be non-canonical $255$-bit encodings of
$\textsf{left}$ and $\textsf{right}$.
We break these inputs into the following `MessagePiece`s:
Sinsemilla operates on multiples of 10 bits, so we start by decomposing the message into
chunks:
$$
\begin{aligned}
a \text{ (250 bits)} &= a_0 \,||\, a_1 \\
&= {l\star} \,||\, (\text{bits } 0..=239 \text{ of } \textsf{ left }) \\
b \text{ (20 bits)} &= b_0 \,||\, b_1 \,||\, b_2 \\
&= (\text{bits } 240..=249 \text{ of } \textsf{left}) \,||\, (\text{bits } 250..=254 \text{ of } \textsf{left}) \,||\, (\text{bits } 0..=4 \text{ of } \textsf{right}) \\
c \text{ (250 bits)} &= \text{bits } 5..=254 \text{ of } \textsf{right}
l\star &= a_0 \\
\textsf{left}\star &= a_1 \bconcat b_0 \bconcat b_1 \\
&= (\text{bits } 0..=239 \text{ of } \textsf{ left }) \bconcat
(\text{bits } 240..=249 \text{ of } \textsf{left}) \bconcat
(\text{bits } 250..=254 \text{ of } \textsf{left}) \\
\textsf{right}\star &= b_2 \bconcat c \\
&= (\text{bits } 0..=4 \text{ of } \textsf{right}) \bconcat
(\text{bits } 5..=254 \text{ of } \textsf{right})
\end{aligned}
$$
$a,b,c$ are constrained by the $\textsf{SinsemillaHash}$ to be $250$ bits, $20$ bits, and $250$ bits respectively.
Then we recompose the chunks into `MessagePiece`s:
In a custom gate, we check this message decomposition by enforcing the following constraints:
$$
\begin{array}{|c|l|}
\hline
\text{Length (bits)} & \text{Piece} \\\hline
250 & a = a_0 \bconcat a_1 \\
20 & b = b_0 \bconcat b_1 \bconcat b_2 \\
250 & c \\\hline
\end{array}
$$
1. $a_0 = l$
<br>
$z_{1,a}$, the index-1 running sum output of $\textsf{SinsemillaHash}(a)$, is copied into the gate. $z_{1,a}$ has been constrained by the $\textsf{SinsemillaHash}$ to be $240$ bits. We recover the subpieces $a_0, a_1$ using $a, z_{1,a}$:
Each message piece is constrained by $\SinsemillaHash$ to its stated length. Additionally,
$\textsf{left}$ and $\textsf{right}$ are witnessed as field elements, so we know that they
are canonical. However, we need additional constraints to enforce that the chunks are the
correct bit lengths (or else they could overlap in the decompositions and allow the prover
to witness an arbitrary $\SinsemillaHash$ message).
Some of these constraints can be implemented with reusable circuit gadgets. We define a
custom gate controlled by the selector $q_\mathsf{decompose}$ to hold the remaining
constraints.
## Bit length constraints
Chunk $c$ is directly constrained by Sinsemilla. We constrain the remaining chunks with
the following constraints:
### $a_0, a_1$
$z_{1,a}$, the index-1 running sum output of $\textsf{SinsemillaHash}(a)$, is copied into
the gate. $z_{1,a}$ has been constrained by $\textsf{SinsemillaHash}$ to be $240$ bits,
and is precisely $a_1$. We recover chunk $a_0$ using $a, z_{1,a}:$
$$
\begin{aligned}
z_{1,a} &= \frac{a - a_0}{2^{10}}\\
@ -38,12 +69,13 @@ z_{1,a} &= \frac{a - a_0}{2^{10}}\\
\implies a_0 &= a - z_{1,a} \cdot 2^{10}.
\end{aligned}
$$
$l + 1$ is loaded into a fixed column at each layer of the hash. It is used both as a gate selector, and to fix the value of $l$. We check that $$a_0 = (l + 1) - 1.$$
> Note: The reason for using $l + 1$ instead of $l$ is that $l = 0$ when $\textsf{layer} = 31$ (hashing two leaves). We cannot have a zero-valued selector, since a constraint gated by a zero-valued selector is never checked.
2. $b_1 + 2^5 \cdot b_2 = z_{1,b}$
<br>
$z_{1,b}$, the index-1 running sum output of $\textsf{SinsemillaHash}(b)$, is copied into the gate. $z_{1,b}$ has been constrained by the $\textsf{SinsemillaHash}$ to be $10$ bits. We witness the subpieces $b_1, b_2$ outside this gate, and constrain them each to be $5$ bits. Inside the gate, we check that $$b_1 + 2^5 \cdot b_2 = z_{1,b}.$$
### $b_0, b_1, b_2$
$z_{1,b}$, the index-1 running sum output of $\textsf{SinsemillaHash}(b)$, is copied into
the gate. $z_{1,b}$ has been constrained by $\textsf{SinsemillaHash}$ to be $10$ bits. We
witness the subpieces $b_1, b_2$ outside this gate, and constrain them each to be $5$
bits. Inside the gate, we check that $$b_1 + 2^5 \cdot b_2 = z_{1,b}.$$
We also recover the subpiece $b_0$ using $(b, z_{1,b})$:
$$
\begin{aligned}
@ -52,18 +84,61 @@ z_{1,b} &= \frac{b - b_{0..=10}}{2^{10}}\\
\end{aligned}
$$
### Constraints
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
& \ShortLookupRangeCheck{b_1, 5} \\\hline
& \ShortLookupRangeCheck{b_2, 5} \\\hline
2 & q_\mathsf{decompose} \cdot (z_{1,b} - (b_1 + b_2 \cdot 2^5)) = 0 \\\hline
\end{array}
$$
where $\ShortLookupRangeCheck{}$ is a
[short lookup range check](../decomposition.md#short-range-check).
## Decomposition constraints
We have now derived or witnessed every subpiece, and range-constrained every subpiece:
- $a_0$ ($10$ bits), derived as $a_0 = a - 2^{10} \cdot z_{1,a}$;
- $a_1$ ($240$ bits), equal to $z_{1,a}$;
- $b_0$ ($10$ bits), derived as $b_0 = b - 2^{10} \cdot z_{1,b}$;
- $b_1$ ($5$ bits) is witnessed and constrained outside the gate;
- $b_2$ ($5$ bits) is witnessed and constrained outside the gate;
- $b_1 + 2^5 \cdot b_2$ is constrained to equal $z_{1, b}$,
and we use them to reconstruct the original field element inputs:
- $c$ ($250$ bits) is witnessed and constrained outside the gate.
- $b_1 + 2^5 \cdot b_2$ is constrained to equal $z_{1, b}$.
3. $\mathsf{left} = a_1 + 2^{240} \cdot b_0 + 2^{254} \cdot b_1$
We can now use them to reconstruct the original field element inputs:
4. $\mathsf{right} = b_2 + 2^5 \cdot c$
$$
\begin{align}
l &= a_0 \\
\mathsf{left} &= a_1 + 2^{240} \cdot b_0 + 2^{250} \cdot b_1 \\
\mathsf{right} &= b_2 + 2^5 \cdot c
\end{align}
$$
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
2 & q_\mathsf{decompose} \cdot (a_0 - l) = 0 \\\hline
2 & q_\mathsf{decompose} \cdot (a_1 + (b_0 + b_1 \cdot 2^{10}) \cdot 2^{240} - \mathsf{left}) = 0 \\\hline
2 & q_\mathsf{decompose} \cdot (b_2 + c \cdot 2^5 - \mathsf{right}) = 0 \\\hline
\end{array}
$$
## Region layout
$$
\begin{array}{|c|c|c|c|c|c}
& & & & & q_\mathsf{decompose} \\\hline
a & b & c & \mathsf{left} & \mathsf{right} & 1 \\\hline
z_{1,a} &z_{1,b} & b_1 & b_2 & l & 0 \\\hline
\end{array}
$$
## Circuit components
The Orchard circuit spans $10$ advice columns while the $\textsf{Sinsemilla}$ chip only uses $5$ advice columns. We distribute the path hashing evenly across two $\textsf{Sinsemilla}$ chips to make better use of the available circuit area. Since the output from the previous layer hash is copied into the next layer hash, we maintain continuity even when moving from one chip to the other.

31
halo2_gadgets/CHANGELOG.md
View File

@ -7,22 +7,33 @@ and this project adheres to Rust's notion of
## [Unreleased]
### Added
- `halo2_gadgets::sinsemilla::MessagePiece::from_subpieces`
- `halo2_gadgets::utilities`:
- `FieldValue` trait.
- `RangeConstrained` newtype wrapper.
- `halo2_gadgets::ecc`:
- `EccInstructions::witness_scalar_var` API to witness a full-width scalar
used in variable-base scalar multiplication.
- `EccInstructions::witness_scalar_fixed`, to witness a full-width scalar
used in fixed-base scalar multiplication.
- `EccInstructions::scalar_fixed_from_signed_short`, to construct a signed
short scalar used in fixed-base scalar multiplication from its magnitude and
sign.
- `BaseFitsInScalarInstructions` trait that can be implemented for a curve
whose base field fits into its scalar field. This provides a method
`scalar_var_from_base` that converts a base field element that exists as
a variable in the circuit, into a scalar to be used in variable-base
scalar multiplication.
- `ScalarFixed::new`
- `ScalarFixedShort::new`
- `ScalarVar::new` and `ScalarVar::from_base` gadget APIs.
- `halo2_gadgets::ecc::chip`:
- `ScalarVar` enum with `BaseFieldElem` and `FullWidth` variants. `FullWidth`
is unimplemented for `halo2_gadgets v0.1.0`.
- `halo2_gadgets::poseidon`:
- `primitives` (moved from `halo2_gadgets::primitives::poseidon`)
- `halo2_gadgets::sinsemilla`:
- `primitives` (moved from `halo2_gadgets::primitives::sinsemilla`)
- `MessagePiece::from_subpieces`
### Changed
- `halo2_gadgets::ecc`:
@ -30,8 +41,26 @@ and this project adheres to Rust's notion of
of being restricted to a base field element.
- `EccInstructions::mul` now takes a `Self::ScalarVar` as argument, instead
of assuming that the scalar fits in a base field element `Self::Var`.
- `EccInstructions::mul_fixed` now takes a `Self::ScalarFixed` as argument,
instead of requiring that the chip always witness a new scalar.
- `EccInstructions::mul_fixed_short` now takes a `Self::ScalarFixedShort` as
argument, instead of the magnitude and sign directly.
- `FixedPoint::mul` now takes `ScalarFixed` instead of `Option<C::Scalar>`.
- `FixedPointShort::mul` now takes `ScalarFixedShort` instead of
`(EccChip::Var, EccChip::Var)`.
- `halo2_gadgets::ecc::chip`:
- `FixedPoint::u` now returns `Vec<[<C::Base as PrimeField>::Repr; H]>`
instead of `Vec<[[u8; 32]; H]>`.
- `ScalarKind` has been renamed to `FixedScalarKind`.
- `halo2_gadgets::sinsemilla`:
- `CommitDomain::{commit, short_commit}` now take the trapdoor `r` as an
`ecc::ScalarFixed<C, EccChip>` instead of `Option<C::Scalar>`.
- `merkle::MerklePath` can now be constructed with more or fewer than two
`MerkleChip`s.
### Removed
- `halo2_gadgets::primitives` (use `halo2_gadgets::poseidon::primitives` or
`halo2_gadgets::sinsemilla::primitives` instead).
## [0.1.0-beta.3] - 2022-04-06
### Changed

6
halo2_gadgets/benches/poseidon.rs
View File

@ -11,9 +11,9 @@ use halo2_proofs::{
};
use pasta_curves::{pallas, vesta};
use halo2_gadgets::{
poseidon::{Hash, Pow5Chip, Pow5Config},
primitives::poseidon::{self, ConstantLength, Spec},
use halo2_gadgets::poseidon::{
primitives::{self as poseidon, ConstantLength, Spec},
Hash, Pow5Chip, Pow5Config,
};
use std::convert::TryInto;
use std::marker::PhantomData;

6
halo2_gadgets/benches/primitives.rs
View File

@ -1,8 +1,8 @@
use criterion::{criterion_group, criterion_main, BenchmarkId, Criterion};
use ff::Field;
use halo2_gadgets::primitives::{
poseidon::{self, ConstantLength, P128Pow5T3},
sinsemilla,
use halo2_gadgets::{
poseidon::primitives::{self as poseidon, ConstantLength, P128Pow5T3},
sinsemilla::primitives as sinsemilla,
};
use pasta_curves::pallas;

110
halo2_gadgets/src/ecc.rs
View File

@ -1,4 +1,4 @@
//! Gadgets for elliptic curve operations.
//! Elliptic curve operations.
use std::fmt::Debug;
@ -75,6 +75,21 @@ pub trait EccInstructions<C: CurveAffine>:
value: Option<C::Scalar>,
) -> Result<Self::ScalarVar, Error>;
/// Witnesses a full-width scalar to be used in fixed-base multiplication.
fn witness_scalar_fixed(
&self,
layouter: &mut impl Layouter<C::Base>,
value: Option<C::Scalar>,
) -> Result<Self::ScalarFixed, Error>;
/// Converts a magnitude and sign that exists as variables in the circuit into a
/// signed short scalar to be used in fixed-base scalar multiplication.
fn scalar_fixed_from_signed_short(
&self,
layouter: &mut impl Layouter<C::Base>,
magnitude_sign: (Self::Var, Self::Var),
) -> Result<Self::ScalarFixedShort, Error>;
/// Extracts the x-coordinate of a point.
fn extract_p<Point: Into<Self::Point> + Clone>(point: &Point) -> Self::X;
@ -108,16 +123,16 @@ pub trait EccInstructions<C: CurveAffine>:
fn mul_fixed(
&self,
layouter: &mut impl Layouter<C::Base>,
scalar: Option<C::Scalar>,
scalar: &Self::ScalarFixed,
base: &<Self::FixedPoints as FixedPoints<C>>::FullScalar,
) -> Result<(Self::Point, Self::ScalarFixed), Error>;
/// Performs fixed-base scalar multiplication using a short signed scalar, returning
/// `[magnitude * sign] base`.
/// `[scalar] base`.
fn mul_fixed_short(
&self,
layouter: &mut impl Layouter<C::Base>,
magnitude_sign: (Self::Var, Self::Var),
scalar: &Self::ScalarFixedShort,
base: &<Self::FixedPoints as FixedPoints<C>>::ShortScalar,
) -> Result<(Self::Point, Self::ScalarFixedShort), Error>;
@ -154,17 +169,7 @@ pub trait FixedPoints<C: CurveAffine>: Debug + Eq + Clone {
type Base: Debug + Eq + Clone;
}
/// An element of the given elliptic curve's base field, that is used as a scalar
/// in variable-base scalar mul.
///
/// It is not true in general that a scalar field element fits in a curve's
/// base field, and in particular it is untrue for the Pallas curve, whose
/// scalar field `Fq` is larger than its base field `Fp`.
///
/// However, the only use of variable-base scalar mul in the Orchard protocol
/// is in deriving diversified addresses `[ivk] g_d`, and `ivk` is guaranteed
/// to be in the base field of the curve. (See non-normative notes in
/// https://zips.z.cash/protocol/nu5.pdf#orchardkeycomponents.)
/// An integer representing an element of the scalar field for a specific elliptic curve.
#[derive(Debug)]
pub struct ScalarVar<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
@ -198,21 +203,58 @@ impl<C: CurveAffine, EccChip: BaseFitsInScalarInstructions<C>> ScalarVar<C, EccC
}
}
/// A full-width element of the given elliptic curve's scalar field, to be used for fixed-base scalar mul.
/// An integer representing an element of the scalar field for a specific elliptic curve,
/// for [`FixedPoint`] scalar multiplication.
#[derive(Debug)]
pub struct ScalarFixed<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
inner: EccChip::ScalarFixed,
}
/// A signed short element of the given elliptic curve's scalar field, to be used for fixed-base scalar mul.
impl<C: CurveAffine, EccChip: EccInstructions<C>> ScalarFixed<C, EccChip> {
/// Witnesses the given full-width scalar.
///
/// Depending on the `EccChip` implementation, this may either witness the scalar
/// immediately, or delay witnessing until its first use in [`FixedPoint::mul`].
pub fn new(
chip: EccChip,
mut layouter: impl Layouter<C::Base>,
value: Option<C::Scalar>,
) -> Result<Self, Error> {
let scalar = chip.witness_scalar_fixed(&mut layouter, value);
scalar.map(|inner| ScalarFixed { chip, inner })
}
}
/// A signed short (64-bit) integer represented as an element of the scalar field for a
/// specific elliptic curve, to be used for [`FixedPointShort`] scalar multiplication.
#[derive(Debug)]
pub struct ScalarFixedShort<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
inner: EccChip::ScalarFixedShort,
}
/// A non-identity elliptic curve point over the given curve.
impl<C: CurveAffine, EccChip: EccInstructions<C>> ScalarFixedShort<C, EccChip> {
/// Converts the given signed short scalar.
///
/// `magnitude_sign` must be a tuple of two circuit-assigned values:
/// - An unsigned integer of at most 64 bits.
/// - A sign value that is either 1 or -1.
///
/// Depending on the `EccChip` implementation, the scalar may either be constrained
/// immediately by this constructor, or lazily constrained when it is first used in
/// [`FixedPointShort::mul`].
pub fn new(
chip: EccChip,
mut layouter: impl Layouter<C::Base>,
magnitude_sign: (EccChip::Var, EccChip::Var),
) -> Result<Self, Error> {
let scalar = chip.scalar_fixed_from_signed_short(&mut layouter, magnitude_sign);
scalar.map(|inner| ScalarFixedShort { chip, inner })
}
}
/// A point on a specific elliptic curve that is guaranteed to not be the identity.
#[derive(Copy, Clone, Debug)]
pub struct NonIdentityPoint<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
@ -330,7 +372,7 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq>
}
}
/// An elliptic curve point over the given curve.
/// A point on a specific elliptic curve.
#[derive(Copy, Clone, Debug)]
pub struct Point<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> {
chip: EccChip,
@ -392,8 +434,7 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> Point<C,
}
}
/// The affine short Weierstrass x-coordinate of an elliptic curve point over the
/// given curve.
/// The affine short Weierstrass x-coordinate of a point on a specific elliptic curve.
#[derive(Debug)]
pub struct X<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
@ -412,26 +453,29 @@ impl<C: CurveAffine, EccChip: EccInstructions<C>> X<C, EccChip> {
}
}
/// A constant elliptic curve point over the given curve, for which window tables have
/// been provided to make scalar multiplication more efficient.
/// Precomputed multiples of a fixed point, for full-width scalar multiplication.
///
/// Used in scalar multiplication with full-width scalars.
/// Fixing the curve point enables window tables to be baked into the circuit, making
/// scalar multiplication more efficient. These window tables are tuned to full-width
/// scalar multiplication.
#[derive(Clone, Debug)]
pub struct FixedPoint<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
inner: <EccChip::FixedPoints as FixedPoints<C>>::FullScalar,
}
/// A constant elliptic curve point over the given curve, used in scalar multiplication
/// with a base field element
/// Precomputed multiples of a fixed point, that can be multiplied by base-field elements.
///
/// Fixing the curve point enables window tables to be baked into the circuit, making
/// scalar multiplication more efficient. These window tables are tuned to scalar
/// multiplication by base-field elements.
#[derive(Clone, Debug)]
pub struct FixedPointBaseField<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
inner: <EccChip::FixedPoints as FixedPoints<C>>::Base,
}
/// A constant elliptic curve point over the given curve, used in scalar multiplication
/// with a short signed exponent
/// Precomputed multiples of a fixed point, for short signed scalar multiplication.
#[derive(Clone, Debug)]
pub struct FixedPointShort<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
@ -444,10 +488,11 @@ impl<C: CurveAffine, EccChip: EccInstructions<C>> FixedPoint<C, EccChip> {
pub fn mul(
&self,
mut layouter: impl Layouter<C::Base>,
by: Option<C::Scalar>,
by: ScalarFixed<C, EccChip>,
) -> Result<(Point<C, EccChip>, ScalarFixed<C, EccChip>), Error> {
assert_eq!(self.chip, by.chip);
self.chip
.mul_fixed(&mut layouter, by, &self.inner)
.mul_fixed(&mut layouter, &by.inner, &self.inner)
.map(|(point, scalar)| {
(
Point {
@ -502,10 +547,11 @@ impl<C: CurveAffine, EccChip: EccInstructions<C>> FixedPointShort<C, EccChip> {
pub fn mul(
&self,
mut layouter: impl Layouter<C::Base>,
magnitude_sign: (EccChip::Var, EccChip::Var),
by: ScalarFixedShort<C, EccChip>,
) -> Result<(Point<C, EccChip>, ScalarFixedShort<C, EccChip>), Error> {
assert_eq!(self.chip, by.chip);
self.chip
.mul_fixed_short(&mut layouter, magnitude_sign, &self.inner)
.mul_fixed_short(&mut layouter, &by.inner, &self.inner)
.map(|(point, scalar)| {
(
Point {

59
halo2_gadgets/src/ecc/chip.rs
View File

@ -2,12 +2,12 @@
use super::{BaseFitsInScalarInstructions, EccInstructions, FixedPoints};
use crate::{
primitives::sinsemilla,
sinsemilla::primitives as sinsemilla,
utilities::{lookup_range_check::LookupRangeCheckConfig, UtilitiesInstructions},
};
use arrayvec::ArrayVec;
use ff::Field;
use ff::{Field, PrimeField};
use group::prime::PrimeCurveAffine;
use halo2_proofs::{
circuit::{AssignedCell, Chip, Layouter},
@ -26,6 +26,9 @@ pub(super) mod witness_point;
pub use constants::*;
// Exposed for Sinsemilla.
pub(crate) use mul::incomplete::DoubleAndAdd;
/// A curve point represented in affine (x, y) coordinates, or the
/// identity represented as (0, 0).
/// Each coordinate is assigned to a cell.
@ -130,7 +133,7 @@ impl From<NonIdentityEccPoint> for EccPoint {
}
}
/// Configuration for the ECC chip
/// Configuration for [`EccChip`].
#[derive(Clone, Debug, Eq, PartialEq)]
#[allow(non_snake_case)]
pub struct EccConfig<FixedPoints: super::FixedPoints<pallas::Affine>> {
@ -210,7 +213,7 @@ pub trait FixedPoint<C: CurveAffine>: std::fmt::Debug + Eq + Clone {
fn generator(&self) -> C;
/// Returns the $u$ values for this fixed point.
fn u(&self) -> Vec<[[u8; 32]; H]>;
fn u(&self) -> Vec<[<C::Base as PrimeField>::Repr; H]>;
/// Returns the $z$ value for this fixed point.
fn z(&self) -> Vec<u64>;
@ -221,7 +224,7 @@ pub trait FixedPoint<C: CurveAffine>: std::fmt::Debug + Eq + Clone {
}
}
/// A chip implementing EccInstructions
/// An [`EccInstructions`] chip that uses 10 advice columns.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct EccChip<FixedPoints: super::FixedPoints<pallas::Affine>> {
config: EccConfig<FixedPoints>,
@ -283,8 +286,6 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> EccChip<FixedPoints> {
meta,
lagrange_coeffs,
advices[4],
advices[0],
advices[1],
advices[5],
add,
add_incomplete,
@ -328,7 +329,9 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> EccChip<FixedPoints> {
#[derive(Clone, Debug)]
pub struct EccScalarFixed {
value: Option<pallas::Scalar>,
windows: ArrayVec<AssignedCell<pallas::Base, pallas::Base>, { NUM_WINDOWS }>,
/// The circuit-assigned windows representing this scalar, or `None` if the scalar has
/// not been used yet.
windows: Option<ArrayVec<AssignedCell<pallas::Base, pallas::Base>, { NUM_WINDOWS }>>,
}
// TODO: Make V a `u64`
@ -353,7 +356,10 @@ type MagnitudeSign = (MagnitudeCell, SignCell);
pub struct EccScalarFixedShort {
magnitude: MagnitudeCell,
sign: SignCell,
running_sum: ArrayVec<AssignedCell<pallas::Base, pallas::Base>, { NUM_WINDOWS_SHORT + 1 }>,
/// The circuit-assigned running sum constraining this signed short scalar, or `None`
/// if the scalar has not been used yet.
running_sum:
Option<ArrayVec<AssignedCell<pallas::Base, pallas::Base>, { NUM_WINDOWS_SHORT + 1 }>>,
}
/// A base field element used for fixed-base scalar multiplication.
@ -391,7 +397,9 @@ pub enum ScalarVar {
/// However, the only use of variable-base scalar mul in the Orchard protocol
/// is in deriving diversified addresses `[ivk] g_d`, and `ivk` is guaranteed
/// to be in the base field of the curve. (See non-normative notes in
/// https://zips.z.cash/protocol/nu5.pdf#orchardkeycomponents.)
/// [4.2.3 Orchard Key Components][orchardkeycomponents].)
///
/// [orchardkeycomponents]: https://zips.z.cash/protocol/protocol.pdf#orchardkeycomponents
BaseFieldElem(AssignedCell<pallas::Base, pallas::Base>),
/// A full-width scalar. This is unimplemented for halo2_gadgets v0.1.0.
FullWidth,
@ -464,6 +472,31 @@ where
todo!()
}
fn witness_scalar_fixed(
&self,
_layouter: &mut impl Layouter<pallas::Base>,
value: Option<pallas::Scalar>,
) -> Result<Self::ScalarFixed, Error> {
Ok(EccScalarFixed {
value,
// This chip uses lazy witnessing.
windows: None,
})
}
fn scalar_fixed_from_signed_short(
&self,
_layouter: &mut impl Layouter<pallas::Base>,
(magnitude, sign): MagnitudeSign,
) -> Result<Self::ScalarFixedShort, Error> {
Ok(EccScalarFixedShort {
magnitude,
sign,
// This chip uses lazy constraining.
running_sum: None,
})
}
fn extract_p<Point: Into<Self::Point> + Clone>(point: &Point) -> Self::X {
let point: EccPoint = (point.clone()).into();
point.x()
@ -519,7 +552,7 @@ where
fn mul_fixed(
&self,
layouter: &mut impl Layouter<pallas::Base>,
scalar: Option<pallas::Scalar>,
scalar: &Self::ScalarFixed,
base: &<Self::FixedPoints as FixedPoints<pallas::Affine>>::FullScalar,
) -> Result<(Self::Point, Self::ScalarFixed), Error> {
let config = self.config().mul_fixed_full.clone();
@ -533,13 +566,13 @@ where
fn mul_fixed_short(
&self,
layouter: &mut impl Layouter<pallas::Base>,
magnitude_sign: MagnitudeSign,
scalar: &Self::ScalarFixedShort,
base: &<Self::FixedPoints as FixedPoints<pallas::Affine>>::ShortScalar,
) -> Result<(Self::Point, Self::ScalarFixedShort), Error> {
let config = self.config().mul_fixed_short.clone();
config.assign(
layouter.namespace(|| format!("short fixed-base mul of {:?}", base)),
magnitude_sign,
scalar,
base,
)
}

88
halo2_gadgets/src/ecc/chip/add.rs
View File

@ -89,7 +89,7 @@ impl Config {
}
fn create_gate(&self, meta: &mut ConstraintSystem<pallas::Base>) {
meta.create_gate("complete addition gates", |meta| {
meta.create_gate("complete addition", |meta| {
let q_add = meta.query_selector(self.q_add);
let x_p = meta.query_advice(self.x_p, Rotation::cur());
let y_p = meta.query_advice(self.y_p, Rotation::cur());
@ -109,14 +109,20 @@ impl Config {
let delta = meta.query_advice(self.delta, Rotation::cur());
// Useful composite expressions
// (x_q − x_p)
let x_q_minus_x_p = x_q.clone() - x_p.clone();
// (x_p - x_r)
let x_p_minus_x_r = x_p.clone() - x_r.clone();
// (y_q + y_p)
let y_q_plus_y_p = y_q.clone() + y_p.clone();
// α ⋅(x_q - x_p)
let if_alpha = (x_q.clone() - x_p.clone()) * alpha;
let if_alpha = x_q_minus_x_p.clone() * alpha;
// β ⋅ x_p
let if_beta = x_p.clone() * beta;
// γ ⋅ x_q
let if_gamma = x_q.clone() * gamma;
// δ ⋅(y_p + y_q)
let if_delta = (y_q.clone() + y_p.clone()) * delta;
// δ ⋅(y_q + y_p)
let if_delta = y_q_plus_y_p.clone() * delta;
// Useful constants
let one = Expression::Constant(pallas::Base::one());
@ -125,13 +131,11 @@ impl Config {
// (x_q − x_p)⋅((x_q − x_p)⋅λ − (y_q−y_p)) = 0
let poly1 = {
let x_q_minus_x_p = x_q.clone() - x_p.clone(); // (x_q − x_p)
let y_q_minus_y_p = y_q.clone() - y_p.clone(); // (y_q − y_p)
let incomplete = x_q_minus_x_p.clone() * lambda.clone() - y_q_minus_y_p; // (x_q − x_p)⋅λ − (y_q−y_p)
// q_add ⋅(x_q − x_p)⋅((x_q − x_p)⋅λ − (y_q−y_p))
x_q_minus_x_p * incomplete
x_q_minus_x_p.clone() * incomplete
};
// (1 - (x_q - x_p)⋅α)⋅(2y_p ⋅λ - 3x_p^2) = 0
@ -144,70 +148,58 @@ impl Config {
(one.clone() - if_alpha.clone()) * tangent_line
};
// x_p⋅x_q⋅(x_q - x_p)⋅(λ^2 - x_p - x_q - x_r) = 0
let secant_line = lambda.clone().square() - x_p.clone() - x_q.clone() - x_r.clone(); // (λ^2 - x_p - x_q - x_r)
let poly3 = {
let x_q_minus_x_p = x_q.clone() - x_p.clone(); // (x_q - x_p)
// (λ^2 - x_p - x_q - x_r)
let nonexceptional_x_r =
lambda.clone().square() - x_p.clone() - x_q.clone() - x_r.clone();
// (λ ⋅(x_p - x_r) - y_p - y_r)
let nonexceptional_y_r = lambda * x_p_minus_x_r - y_p.clone() - y_r.clone();
// x_p⋅x_q⋅(x_q - x_p)⋅(λ^2 - x_p - x_q - x_r)
x_p.clone() * x_q.clone() * x_q_minus_x_p * secant_line.clone()
};
// x_p⋅x_q⋅(x_q - x_p)⋅(λ^2 - x_p - x_q - x_r) = 0
let poly3a =
x_p.clone() * x_q.clone() * x_q_minus_x_p.clone() * nonexceptional_x_r.clone();
// x_p⋅x_q⋅(x_q - x_p)⋅(λ ⋅(x_p - x_r) - y_p - y_r) = 0
let poly4 = {
let x_q_minus_x_p = x_q.clone() - x_p.clone(); // (x_q - x_p)
let x_p_minus_x_r = x_p.clone() - x_r.clone(); // (x_p - x_r)
// x_p⋅x_q⋅(x_q - x_p)⋅(λ ⋅(x_p - x_r) - y_p - y_r)
x_p.clone()
* x_q.clone()
* x_q_minus_x_p
* (lambda.clone() * x_p_minus_x_r - y_p.clone() - y_r.clone())
};
let poly3b = x_p.clone() * x_q.clone() * x_q_minus_x_p * nonexceptional_y_r.clone();
// x_p⋅x_q⋅(y_q + y_p)⋅(λ^2 - x_p - x_q - x_r) = 0
let poly5 = {
let y_q_plus_y_p = y_q.clone() + y_p.clone(); // (y_q + y_p)
// x_p⋅x_q⋅(y_q + y_p)⋅(λ^2 - x_p - x_q - x_r)
x_p.clone() * x_q.clone() * y_q_plus_y_p * secant_line
};
let poly3c = x_p.clone() * x_q.clone() * y_q_plus_y_p.clone() * nonexceptional_x_r;
// x_p⋅x_q⋅(y_q + y_p)⋅(λ ⋅(x_p - x_r) - y_p - y_r) = 0
let poly6 = {
let y_q_plus_y_p = y_q.clone() + y_p.clone(); // (y_q + y_p)
let x_p_minus_x_r = x_p.clone() - x_r.clone(); // (x_p - x_r)
// x_p⋅x_q⋅(y_q + y_p)⋅(λ ⋅(x_p - x_r) - y_p - y_r)
x_p.clone()
* x_q.clone()
* y_q_plus_y_p
* (lambda * x_p_minus_x_r - y_p.clone() - y_r.clone())
};
let poly3d = x_p.clone() * x_q.clone() * y_q_plus_y_p * nonexceptional_y_r;
// (1 - x_p * β) * (x_r - x_q) = 0
let poly7 = (one.clone() - if_beta.clone()) * (x_r.clone() - x_q);
let poly4a = (one.clone() - if_beta.clone()) * (x_r.clone() - x_q);
// (1 - x_p * β) * (y_r - y_q) = 0
let poly8 = (one.clone() - if_beta) * (y_r.clone() - y_q);
let poly4b = (one.clone() - if_beta) * (y_r.clone() - y_q);
// (1 - x_q * γ) * (x_r - x_p) = 0
let poly9 = (one.clone() - if_gamma.clone()) * (x_r.clone() - x_p);
let poly5a = (one.clone() - if_gamma.clone()) * (x_r.clone() - x_p);
// (1 - x_q * γ) * (y_r - y_p) = 0
let poly10 = (one.clone() - if_gamma) * (y_r.clone() - y_p);
let poly5b = (one.clone() - if_gamma) * (y_r.clone() - y_p);
// ((1 - (x_q - x_p) * α - (y_q + y_p) * δ)) * x_r
let poly11 = (one.clone() - if_alpha.clone() - if_delta.clone()) * x_r;
let poly6a = (one.clone() - if_alpha.clone() - if_delta.clone()) * x_r;
// ((1 - (x_q - x_p) * α - (y_q + y_p) * δ)) * y_r
let poly12 = (one - if_alpha - if_delta) * y_r;
let poly6b = (one - if_alpha - if_delta) * y_r;
Constraints::with_selector(
q_add,
[
poly1, poly2, poly3, poly4, poly5, poly6, poly7, poly8, poly9, poly10, poly11,
poly12,
("1", poly1),
("2", poly2),
("3a", poly3a),
("3b", poly3b),
("3c", poly3c),
("3d", poly3d),
("4a", poly4a),
("4b", poly4b),
("5a", poly5a),
("5b", poly5b),
("6a", poly6a),
("6b", poly6b),
],
)
});

26
halo2_gadgets/src/ecc/chip/mul.rs
View File

@ -1,6 +1,6 @@
use super::{add, EccPoint, NonIdentityEccPoint, ScalarVar, T_Q};
use crate::{
primitives::sinsemilla,
sinsemilla::primitives as sinsemilla,
utilities::{bool_check, lookup_range_check::LookupRangeCheckConfig, ternary},
};
use std::{
@ -20,7 +20,7 @@ use uint::construct_uint;
use pasta_curves::pallas;
mod complete;
mod incomplete;
pub(super) mod incomplete;
mod overflow;
/// Number of bits for which complete addition needs to be used in variable-base
@ -35,7 +35,7 @@ const INCOMPLETE_RANGE: Range<usize> = 0..INCOMPLETE_LEN;
// The `hi` half is k_{254} to k_{130} inclusive (length 125 bits).
// (It is a coincidence that k_{130} matches the boundary of the
// overflow check described in [the book](https://zcash.github.io/halo2/design/gadgets/ecc/var-base-scalar-mul.html#overflow-check).)
const INCOMPLETE_HI_RANGE: Range<usize> = 0..(INCOMPLETE_LEN / 2);
const INCOMPLETE_HI_RANGE: Range<usize> = 0..INCOMPLETE_HI_LEN;
const INCOMPLETE_HI_LEN: usize = INCOMPLETE_LEN / 2;
// Bits k_{254} to k_{4} inclusive are used in incomplete addition.
@ -92,7 +92,7 @@ impl Config {
config.create_gate(meta);
assert_eq!(
config.hi_config.x_p, config.lo_config.x_p,
config.hi_config.double_and_add.x_p, config.lo_config.double_and_add.x_p,
"x_p is shared across hi and lo halves."
);
assert_eq!(
@ -110,7 +110,7 @@ impl Config {
"incomplete config z cannot overlap with complete addition columns."
);
assert!(
!add_config_outputs.contains(&config.hi_config.lambda1),
!add_config_outputs.contains(&config.hi_config.double_and_add.lambda_1),
"incomplete config lambda1 cannot overlap with complete addition columns."
);
}
@ -120,7 +120,7 @@ impl Config {
"incomplete config z cannot overlap with complete addition columns."
);
assert!(
!add_config_outputs.contains(&config.lo_config.lambda1),
!add_config_outputs.contains(&config.lo_config.double_and_add.lambda_1),
"incomplete config lambda1 cannot overlap with complete addition columns."
);
}
@ -184,7 +184,7 @@ impl Config {
let bits_incomplete_lo = &bits[INCOMPLETE_LO_RANGE];
let lsb = bits[pallas::Scalar::NUM_BITS as usize - 1];
// Initialize the accumulator `acc = [2]base`
// Initialize the accumulator `acc = [2]base` using complete addition.
let acc =
self.add_config
.assign_region(&base_point, &base_point, offset, &mut region)?;
@ -192,7 +192,12 @@ impl Config {
// Increase the offset by 1 after complete addition.
let offset = offset + 1;
// Initialize the running sum for scalar decomposition to zero
// Initialize the running sum for scalar decomposition to zero.
//
// `incomplete::Config::double_and_add` will copy this cell directly into
// itself. This is fine because we are just assigning the same value to
// the same cell twice, and then applying an equality constraint between
// the cell and itself (which the permutation argument treats as a no-op).
let z_init = Z(region.assign_advice_from_constant(
|| "z_init = 0",
self.hi_config.z,
@ -225,6 +230,7 @@ impl Config {
// Then, the final assignment of double-and-add was made on row + offset + 1.
// Outside of incomplete addition, we must account for these offset increases by adding
// 2 to the incomplete addition length.
assert!(INCOMPLETE_LO_RANGE.len() >= INCOMPLETE_HI_RANGE.len());
let offset = offset + INCOMPLETE_LO_RANGE.len() + 2;
// Complete addition
@ -440,7 +446,7 @@ fn decompose_for_scalar_mul(scalar: Option<&pallas::Base>) -> Vec<Option<bool>>
let t_q = U256::from_little_endian(&T_Q.to_le_bytes());
let k = scalar + t_q;
// Big-endian bit representation of `k`.
// Little-endian bit representation of `k`.
let bitstring: Vec<bool> = {
let mut le_bytes = [0u8; 32];
k.to_little_endian(&mut le_bytes);
@ -453,7 +459,7 @@ fn decompose_for_scalar_mul(scalar: Option<&pallas::Base>) -> Vec<Option<bool>>
})
};
// Take the first 255 bits.
// Take the first 255 bits, and reverse to get the big-endian bit representation.
let mut bitstring = bitstring[0..pallas::Scalar::NUM_BITS as usize].to_vec();
bitstring.reverse();
bitstring

8
halo2_gadgets/src/ecc/chip/mul/complete.rs
View File

@ -168,6 +168,14 @@ impl Config {
.zip(k.as_ref())
.map(|(base_y, k)| if !k { -base_y } else { base_y });
// Assign the conditionally-negated y coordinate into the cell it will be
// used from by both the complete addition gate, and the decomposition and
// conditional negation gate.
//
// The complete addition gate will copy this cell onto itself. This is
// fine because we are just assigning the same value to the same cell
// twice, and then applying an equality constraint between the cell and
// itself (which the permutation argument treats as a no-op).
region.assign_advice(
|| "y_p",
self.add_config.y_p,

152
halo2_gadgets/src/ecc/chip/mul/incomplete.rs
View File

@ -12,22 +12,63 @@ use halo2_proofs::{
use pasta_curves::{arithmetic::FieldExt, pallas};
/// A helper struct for implementing single-row double-and-add using incomplete addition.
#[derive(Copy, Clone, Debug, Eq, PartialEq)]
pub(crate) struct DoubleAndAdd {
// x-coordinate of the accumulator in each double-and-add iteration.
pub(crate) x_a: Column<Advice>,
// x-coordinate of the point being added in each double-and-add iteration.
pub(crate) x_p: Column<Advice>,
// lambda1 in each double-and-add iteration.
pub(crate) lambda_1: Column<Advice>,
// lambda2 in each double-and-add iteration.
pub(crate) lambda_2: Column<Advice>,
}
impl DoubleAndAdd {
/// Derives the expression `x_r = lambda_1^2 - x_a - x_p`.
pub(crate) fn x_r(
&self,
meta: &mut VirtualCells<pallas::Base>,
rotation: Rotation,
) -> Expression<pallas::Base> {
let x_a = meta.query_advice(self.x_a, rotation);
let x_p = meta.query_advice(self.x_p, rotation);
let lambda_1 = meta.query_advice(self.lambda_1, rotation);
lambda_1.square() - x_a - x_p
}
/// Derives the expression `Y_A = (lambda_1 + lambda_2) * (x_a - x_r)`.
///
/// Note that this is missing the factor of `1/2`; the Sinsemilla constraints factor
/// it out, so we leave it up to the caller to handle it.
#[allow(non_snake_case)]
pub(crate) fn Y_A(
&self,
meta: &mut VirtualCells<pallas::Base>,
rotation: Rotation,
) -> Expression<pallas::Base> {
let x_a = meta.query_advice(self.x_a, rotation);
let lambda_1 = meta.query_advice(self.lambda_1, rotation);
let lambda_2 = meta.query_advice(self.lambda_2, rotation);
(lambda_1 + lambda_2) * (x_a - self.x_r(meta, rotation))
}
}
#[derive(Copy, Clone, Debug, Eq, PartialEq)]
pub(crate) struct Config<const NUM_BITS: usize> {
// Selectors used to constrain the cells used in incomplete addition.
pub(super) q_mul: (Selector, Selector, Selector),
// Selector constraining the first row of incomplete addition.
pub(super) q_mul_1: Selector,
// Selector constraining the main loop of incomplete addition.
pub(super) q_mul_2: Selector,
// Selector constraining the last row of incomplete addition.
pub(super) q_mul_3: Selector,
// Cumulative sum used to decompose the scalar.
pub(super) z: Column<Advice>,
// x-coordinate of the accumulator in each double-and-add iteration.
pub(super) x_a: Column<Advice>,
// x-coordinate of the point being added in each double-and-add iteration.
pub(super) x_p: Column<Advice>,
// Logic specific to merged double-and-add.
pub(super) double_and_add: DoubleAndAdd,
// y-coordinate of the point being added in each double-and-add iteration.
pub(super) y_p: Column<Advice>,
// lambda1 in each double-and-add iteration.
pub(super) lambda1: Column<Advice>,
// lambda2 in each double-and-add iteration.
pub(super) lambda2: Column<Advice>,
}
impl<const NUM_BITS: usize> Config<NUM_BITS> {
@ -37,20 +78,24 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
x_a: Column<Advice>,
x_p: Column<Advice>,
y_p: Column<Advice>,
lambda1: Column<Advice>,
lambda2: Column<Advice>,
lambda_1: Column<Advice>,
lambda_2: Column<Advice>,
) -> Self {
meta.enable_equality(z);
meta.enable_equality(lambda1);
meta.enable_equality(lambda_1);
let config = Self {
q_mul: (meta.selector(), meta.selector(), meta.selector()),
q_mul_1: meta.selector(),
q_mul_2: meta.selector(),
q_mul_3: meta.selector(),
z,
x_a,
x_p,
double_and_add: DoubleAndAdd {
x_a,
x_p,
lambda_1,
lambda_2,
},
y_p,
lambda1,
lambda2,
};
config.create_gate(meta);
@ -62,19 +107,12 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
fn create_gate(&self, meta: &mut ConstraintSystem<pallas::Base>) {
// Closure to compute x_{R,i} = λ_{1,i}^2 - x_{A,i} - x_{P,i}
let x_r = |meta: &mut VirtualCells<pallas::Base>, rotation: Rotation| {
let x_a = meta.query_advice(self.x_a, rotation);
let x_p = meta.query_advice(self.x_p, rotation);
let lambda_1 = meta.query_advice(self.lambda1, rotation);
lambda_1.square() - x_a - x_p
self.double_and_add.x_r(meta, rotation)
};
// Closure to compute y_{A,i} = (λ_{1,i} + λ_{2,i}) * (x_{A,i} - x_{R,i}) / 2
let y_a = |meta: &mut VirtualCells<pallas::Base>, rotation: Rotation| {
let x_a = meta.query_advice(self.x_a, rotation);
let lambda_1 = meta.query_advice(self.lambda1, rotation);
let lambda_2 = meta.query_advice(self.lambda2, rotation);
(lambda_1 + lambda_2) * (x_a - x_r(meta, rotation)) * pallas::Base::TWO_INV
self.double_and_add.Y_A(meta, rotation) * pallas::Base::TWO_INV
};
// Constraints used for q_mul_{2, 3} == 1
@ -87,17 +125,17 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
// z_{i+1}
let z_prev = meta.query_advice(self.z, Rotation::prev());
// x_{A,i}
let x_a_cur = meta.query_advice(self.x_a, Rotation::cur());
let x_a_cur = meta.query_advice(self.double_and_add.x_a, Rotation::cur());
// x_{A,i-1}
let x_a_next = meta.query_advice(self.x_a, Rotation::next());
let x_a_next = meta.query_advice(self.double_and_add.x_a, Rotation::next());
// x_{P,i}
let x_p_cur = meta.query_advice(self.x_p, Rotation::cur());
let x_p_cur = meta.query_advice(self.double_and_add.x_p, Rotation::cur());
// y_{P,i}
let y_p_cur = meta.query_advice(self.y_p, Rotation::cur());
// λ_{1,i}
let lambda1_cur = meta.query_advice(self.lambda1, Rotation::cur());
let lambda1_cur = meta.query_advice(self.double_and_add.lambda_1, Rotation::cur());
// λ_{2,i}
let lambda2_cur = meta.query_advice(self.lambda2, Rotation::cur());
let lambda2_cur = meta.query_advice(self.double_and_add.lambda_2, Rotation::cur());
let y_a_cur = y_a(meta, Rotation::cur());
@ -130,23 +168,23 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
// q_mul_1 == 1 checks
meta.create_gate("q_mul_1 == 1 checks", |meta| {
let q_mul_1 = meta.query_selector(self.q_mul.0);
let q_mul_1 = meta.query_selector(self.q_mul_1);
let y_a_next = y_a(meta, Rotation::next());
let y_a_witnessed = meta.query_advice(self.lambda1, Rotation::cur());
let y_a_witnessed = meta.query_advice(self.double_and_add.lambda_1, Rotation::cur());
Constraints::with_selector(q_mul_1, Some(("init y_a", y_a_witnessed - y_a_next)))
});
// q_mul_2 == 1 checks
meta.create_gate("q_mul_2 == 1 checks", |meta| {
let q_mul_2 = meta.query_selector(self.q_mul.1);
let q_mul_2 = meta.query_selector(self.q_mul_2);
let y_a_next = y_a(meta, Rotation::next());
// x_{P,i}
let x_p_cur = meta.query_advice(self.x_p, Rotation::cur());
let x_p_cur = meta.query_advice(self.double_and_add.x_p, Rotation::cur());
// x_{P,i-1}
let x_p_next = meta.query_advice(self.x_p, Rotation::next());
let x_p_next = meta.query_advice(self.double_and_add.x_p, Rotation::next());
// y_{P,i}
let y_p_cur = meta.query_advice(self.y_p, Rotation::cur());
// y_{P,i-1}
@ -168,8 +206,8 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
// q_mul_3 == 1 checks
meta.create_gate("q_mul_3 == 1 checks", |meta| {
let q_mul_3 = meta.query_selector(self.q_mul.2);
let y_a_final = meta.query_advice(self.lambda1, Rotation::next());
let q_mul_3 = meta.query_selector(self.q_mul_3);
let y_a_final = meta.query_advice(self.double_and_add.lambda_1, Rotation::next());
Constraints::with_selector(q_mul_3, for_loop(meta, y_a_final))
});
}
@ -212,16 +250,16 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
// Set q_mul values
{
// q_mul_1 = 1 on offset 0
self.q_mul.0.enable(region, offset)?;
self.q_mul_1.enable(region, offset)?;
let offset = offset + 1;
// q_mul_2 = 1 on all rows after offset 0, excluding the last row.
for idx in 0..(NUM_BITS - 1) {
self.q_mul.1.enable(region, offset + idx)?;
self.q_mul_2.enable(region, offset + idx)?;
}
// q_mul_3 = 1 on the last row.
self.q_mul.2.enable(region, offset + NUM_BITS - 1)?;
self.q_mul_3.enable(region, offset + NUM_BITS - 1)?;
}
// Initialise double-and-add
@ -230,12 +268,18 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
let z = acc.2.copy_advice(|| "starting z", region, self.z, offset)?;
// Initialise acc
let x_a = acc
.0
.copy_advice(|| "starting x_a", region, self.x_a, offset + 1)?;
let y_a = acc
.1
.copy_advice(|| "starting y_a", region, self.lambda1, offset)?;
let x_a = acc.0.copy_advice(
|| "starting x_a",
region,
self.double_and_add.x_a,
offset + 1,
)?;
let y_a = acc.1.copy_advice(
|| "starting y_a",
region,
self.double_and_add.lambda_1,
offset,
)?;
(x_a, y_a.value().cloned(), z)
};
@ -264,7 +308,7 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
// Assign `x_p`, `y_p`
region.assign_advice(
|| "x_p",
self.x_p,
self.double_and_add.x_p,
row + offset,
|| x_p.ok_or(Error::Synthesis),
)?;
@ -288,7 +332,7 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
.map(|(((y_a, y_p), x_a), x_p)| (y_a - y_p) * (x_a - x_p).invert().unwrap());
region.assign_advice(
|| "lambda1",
self.lambda1,
self.double_and_add.lambda_1,
row + offset,
|| lambda1.ok_or(Error::Synthesis),
)?;
@ -297,7 +341,7 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
let x_r = lambda1
.zip(x_a.value())
.zip(x_p)
.map(|((lambda1, x_a), x_p)| lambda1 * lambda1 - x_a - x_p);
.map(|((lambda1, x_a), x_p)| lambda1.square() - x_a - x_p);
// λ2 = (2(y_A) / (x_A - x_R)) - λ1
let lambda2 =
@ -310,7 +354,7 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
});
region.assign_advice(
|| "lambda2",
self.lambda2,
self.double_and_add.lambda_2,
row + offset,
|| lambda2.ok_or(Error::Synthesis),
)?;
@ -328,7 +372,7 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
let x_a_val = x_a_new;
x_a = region.assign_advice(
|| "x_a",
self.x_a,
self.double_and_add.x_a,
row + offset + 1,
|| x_a_val.ok_or(Error::Synthesis),
)?;
@ -337,7 +381,7 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
// Witness final y_a
let y_a = region.assign_advice(
|| "y_a",
self.lambda1,
self.double_and_add.lambda_1,
offset + NUM_BITS,
|| y_a.ok_or(Error::Synthesis),
)?;

5
halo2_gadgets/src/ecc/chip/mul/overflow.rs
View File

@ -1,5 +1,8 @@
use super::{T_Q, Z};
use crate::{primitives::sinsemilla, utilities::lookup_range_check::LookupRangeCheckConfig};
use crate::{
sinsemilla::primitives as sinsemilla, utilities::lookup_range_check::LookupRangeCheckConfig,
};
use halo2_proofs::circuit::AssignedCell;
use halo2_proofs::{
circuit::Layouter,

192
halo2_gadgets/src/ecc/chip/mul_fixed.rs
View File

@ -6,7 +6,10 @@ use crate::utilities::decompose_running_sum::RunningSumConfig;
use std::marker::PhantomData;
use group::{ff::PrimeField, Curve};
use group::{
ff::{PrimeField, PrimeFieldBits},
Curve,
};
use halo2_proofs::{
circuit::{AssignedCell, Region},
plonk::{
@ -42,10 +45,6 @@ pub struct Config<FixedPoints: super::FixedPoints<pallas::Affine>> {
// Decomposition of an `n-1`-bit scalar into `k`-bit windows:
// a = a_0 + 2^k(a_1) + 2^{2k}(a_2) + ... + 2^{(n-1)k}(a_{n-1})
window: Column<Advice>,
// x-coordinate of the multiple of the fixed base at the current window.
x_p: Column<Advice>,
// y-coordinate of the multiple of the fixed base at the current window.
y_p: Column<Advice>,
// y-coordinate of accumulator (only used in the final row).
u: Column<Advice>,
// Configuration for `add`
@ -61,8 +60,6 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
meta: &mut ConstraintSystem<pallas::Base>,
lagrange_coeffs: [Column<Fixed>; H],
window: Column<Advice>,
x_p: Column<Advice>,
y_p: Column<Advice>,
u: Column<Advice>,
add_config: add::Config,
add_incomplete_config: add_incomplete::Config,
@ -78,34 +75,22 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
lagrange_coeffs,
fixed_z: meta.fixed_column(),
window,
x_p,
y_p,
u,
add_config,
add_incomplete_config,
_marker: PhantomData,
};
// Check relationships between this config and `add_config`.
// Check relationships between `add_config` and `add_incomplete_config`.
assert_eq!(
config.x_p, config.add_config.x_p,
"add is used internally in mul_fixed."
config.add_config.x_p, config.add_incomplete_config.x_p,
"add and add_incomplete are used internally in mul_fixed."
);
assert_eq!(
config.y_p, config.add_config.y_p,
"add is used internally in mul_fixed."
config.add_config.y_p, config.add_incomplete_config.y_p,
"add and add_incomplete are used internally in mul_fixed."
);
// Check relationships between this config and `add_incomplete_config`.
assert_eq!(
config.x_p, config.add_incomplete_config.x_p,
"add_incomplete is used internally in mul_fixed."
);
assert_eq!(
config.y_p, config.add_incomplete_config.y_p,
"add_incomplete is used internally in mul_fixed."
);
for advice in [config.x_p, config.y_p, config.window, config.u].iter() {
for advice in [config.window, config.u].iter() {
assert_ne!(
*advice, config.add_config.x_qr,
"Do not overlap with output columns of add."
@ -152,8 +137,8 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
meta: &mut VirtualCells<'_, pallas::Base>,
window: Expression<pallas::Base>,
) -> Vec<(&'static str, Expression<pallas::Base>)> {
let y_p = meta.query_advice(self.y_p, Rotation::cur());
let x_p = meta.query_advice(self.x_p, Rotation::cur());
let y_p = meta.query_advice(self.add_config.y_p, Rotation::cur());
let x_p = meta.query_advice(self.add_config.x_p, Rotation::cur());
let z = meta.query_fixed(self.fixed_z, Rotation::cur());
let u = meta.query_advice(self.u, Rotation::cur());
@ -205,7 +190,7 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
// Process all windows excluding least and most significant windows
let acc = self.add_incomplete::<F, NUM_WINDOWS>(region, offset, acc, base, scalar)?;
// Process most significant window using complete addition
// Process most significant window
let mul_b = self.process_msb::<F, NUM_WINDOWS>(region, offset, base, scalar)?;
Ok((acc, mul_b))
@ -269,23 +254,23 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
Ok(())
}
/// Assigns the values used to process a window.
fn process_window<F: FixedPoint<pallas::Affine>, const NUM_WINDOWS: usize>(
&self,
region: &mut Region<'_, pallas::Base>,
offset: usize,
w: usize,
k: Option<pallas::Scalar>,
k_usize: Option<usize>,
window_scalar: Option<pallas::Scalar>,
base: &F,
) -> Result<NonIdentityEccPoint, Error> {
let base_value = base.generator();
let base_u = base.u();
assert_eq!(base_u.len(), NUM_WINDOWS);
// Compute [(k_w + 2) ⋅ 8^w]B
// Compute [window_scalar]B
let mul_b = {
let mul_b =
k.map(|k| base_value * (k + *TWO_SCALAR) * H_SCALAR.pow(&[w as u64, 0, 0, 0]));
let mul_b = window_scalar.map(|scalar| base_value * scalar);
let mul_b = mul_b.map(|mul_b| mul_b.to_affine().coordinates().unwrap());
let x = mul_b.map(|mul_b| {
@ -295,7 +280,7 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
});
let x = region.assign_advice(
|| format!("mul_b_x, window {}", w),
self.x_p,
self.add_config.x_p,
offset + w,
|| x.ok_or(Error::Synthesis),
)?;
@ -307,7 +292,7 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
});
let y = region.assign_advice(
|| format!("mul_b_y, window {}", w),
self.y_p,
self.add_config.y_p,
offset + w,
|| y.ok_or(Error::Synthesis),
)?;
@ -335,7 +320,7 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
let w = 0;
let k0 = scalar.windows_field()[0];
let k0_usize = scalar.windows_usize()[0];
self.process_window::<_, NUM_WINDOWS>(region, offset, w, k0, k0_usize, base)
self.process_lower_bits::<_, NUM_WINDOWS>(region, offset, w, k0, k0_usize, base)
}
fn add_incomplete<F: FixedPoint<pallas::Affine>, const NUM_WINDOWS: usize>(
@ -348,19 +333,28 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
) -> Result<NonIdentityEccPoint, Error> {
let scalar_windows_field = scalar.windows_field();
let scalar_windows_usize = scalar.windows_usize();
assert_eq!(scalar_windows_field.len(), NUM_WINDOWS);
for (w, (k, k_usize)) in scalar_windows_field[..(scalar_windows_field.len() - 1)]
.iter()
.zip(scalar_windows_usize[..(scalar_windows_field.len() - 1)].iter())
for (w, (k, k_usize)) in scalar_windows_field
.into_iter()
.zip(scalar_windows_usize)
.enumerate()
// The MSB is processed separately.
.take(NUM_WINDOWS - 1)
// Skip k_0 (already processed).
.skip(1)
{
// Compute [(k_w + 2) ⋅ 8^w]B
//
// This assigns the coordinates of the returned point into the input cells for
// the incomplete addition gate, which will then copy them into themselves.
let mul_b =
self.process_window::<_, NUM_WINDOWS>(region, offset, w, *k, *k_usize, base)?;
self.process_lower_bits::<_, NUM_WINDOWS>(region, offset, w, k, k_usize, base)?;
// Add to the accumulator
// Add to the accumulator.
//
// After the first loop, the accumulator will already be in the input cells
// for the incomplete addition gate, and will be copied into themselves.
acc = self
.add_incomplete_config
.assign_region(&mul_b, &acc, offset + w, region)?;
@ -368,6 +362,23 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
Ok(acc)
}
/// Assigns the values used to process a window that does not contain the MSB.
fn process_lower_bits<F: FixedPoint<pallas::Affine>, const NUM_WINDOWS: usize>(
&self,
region: &mut Region<'_, pallas::Base>,
offset: usize,
w: usize,
k: Option<pallas::Scalar>,
k_usize: Option<usize>,
base: &F,
) -> Result<NonIdentityEccPoint, Error> {
// `scalar = [(k_w + 2) ⋅ 8^w]
let scalar = k.map(|k| (k + *TWO_SCALAR) * (*H_SCALAR).pow(&[w as u64, 0, 0, 0]));
self.process_window::<_, NUM_WINDOWS>(region, offset, w, k_usize, scalar, base)
}
/// Assigns the values used to process the window containing the MSB.
fn process_msb<F: FixedPoint<pallas::Affine>, const NUM_WINDOWS: usize>(
&self,
region: &mut Region<'_, pallas::Base>,
@ -375,59 +386,25 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
base: &F,
scalar: &ScalarFixed,
) -> Result<NonIdentityEccPoint, Error> {
// Assign u = (y_p + z_w).sqrt() for the most significant window
{
let u_val = scalar.windows_usize()[NUM_WINDOWS - 1]
.map(|k| pallas::Base::from_repr(base.u()[NUM_WINDOWS - 1][k]).unwrap());
region.assign_advice(
|| "u",
self.u,
offset + NUM_WINDOWS - 1,
|| u_val.ok_or(Error::Synthesis),
)?;
}
let k_usize = scalar.windows_usize()[NUM_WINDOWS - 1];
// offset_acc = \sum_{j = 0}^{NUM_WINDOWS - 2} 2^{FIXED_BASE_WINDOW_SIZE*j + 1}
let offset_acc = (0..(NUM_WINDOWS - 1)).fold(pallas::Scalar::zero(), |acc, w| {
acc + (*TWO_SCALAR).pow(&[FIXED_BASE_WINDOW_SIZE as u64 * w as u64 + 1, 0, 0, 0])
});
// `scalar = [k * 8^84 - offset_acc]`, where `offset_acc = \sum_{j = 0}^{83} 2^{FIXED_BASE_WINDOW_SIZE*j + 1}`.
// `scalar = [k * 8^(NUM_WINDOWS - 1) - offset_acc]`.
let scalar = scalar.windows_field()[scalar.windows_field().len() - 1]
.map(|k| k * (*H_SCALAR).pow(&[(NUM_WINDOWS - 1) as u64, 0, 0, 0]) - offset_acc);
let mul_b = {
let mul_b = scalar.map(|scalar| base.generator() * scalar);
let mul_b = mul_b.map(|mul_b| mul_b.to_affine().coordinates().unwrap());
let x = mul_b.map(|mul_b| {
let x = *mul_b.x();
assert!(x != pallas::Base::zero());
x
});
let x = region.assign_advice(
|| format!("mul_b_x, window {}", NUM_WINDOWS - 1),
self.x_p,
offset + NUM_WINDOWS - 1,
|| x.ok_or(Error::Synthesis),
)?;
let y = mul_b.map(|mul_b| {
let y = *mul_b.y();
assert!(y != pallas::Base::zero());
y
});
let y = region.assign_advice(
|| format!("mul_b_y, window {}", NUM_WINDOWS - 1),
self.y_p,
offset + NUM_WINDOWS - 1,
|| y.ok_or(Error::Synthesis),
)?;
NonIdentityEccPoint { x, y }
};
Ok(mul_b)
self.process_window::<_, NUM_WINDOWS>(
region,
offset,
NUM_WINDOWS - 1,
k_usize,
scalar,
base,
)
}
}
@ -456,8 +433,11 @@ impl From<&EccBaseFieldElemFixed> for ScalarFixed {
}
impl ScalarFixed {
// The scalar decomposition was done in the base field. For computation
// outside the circuit, we now convert them back into the scalar field.
/// The scalar decomposition was done in the base field. For computation
/// outside the circuit, we now convert them back into the scalar field.
///
/// This function does not require that the base field fits inside the scalar field,
/// because the window size fits into either field.
fn windows_field(&self) -> Vec<Option<pallas::Scalar>> {
let running_sum_to_windows = |zs: Vec<AssignedCell<pallas::Base, pallas::Base>>| {
(0..(zs.len() - 1))
@ -467,17 +447,31 @@ impl ScalarFixed {
let word = z_cur
.zip(z_next)
.map(|(z_cur, z_next)| z_cur - z_next * *H_BASE);
// This assumes that the endianness of the encodings of pallas::Base
// and pallas::Scalar are the same. They happen to be, but we need to
// be careful if this is generalised.
word.map(|word| pallas::Scalar::from_repr(word.to_repr()).unwrap())
})
.collect::<Vec<_>>()
};
match self {
Self::BaseFieldElem(scalar) => running_sum_to_windows(scalar.running_sum.to_vec()),
Self::Short(scalar) => running_sum_to_windows(scalar.running_sum.to_vec()),
Self::Short(scalar) => running_sum_to_windows(
scalar
.running_sum
.as_ref()
.expect("EccScalarFixedShort has been constrained")
.to_vec(),
),
Self::FullWidth(scalar) => scalar
.windows
.as_ref()
.expect("EccScalarFixed has been witnessed")
.iter()
.map(|bits| {
// This assumes that the endianness of the encodings of pallas::Base
// and pallas::Scalar are the same. They happen to be, but we need to
// be careful if this is generalised.
bits.value()
.map(|value| pallas::Scalar::from_repr(value.to_repr()).unwrap())
})
@ -485,22 +479,22 @@ impl ScalarFixed {
}
}
// The scalar decomposition is guaranteed to be in three-bit windows,
// so we also cast the least significant 4 bytes in their serialisation
// into usize for convenient indexing into `u`-values
/// The scalar decomposition is guaranteed to be in three-bit windows, so we construct
/// `usize` indices from the lowest three bits of each window field element for
/// convenient indexing into `u`-values.
fn windows_usize(&self) -> Vec<Option<usize>> {
self.windows_field()
.iter()
.map(|window| {
if let Some(window) = window {
// TODO: Remove this trait dependency
use pasta_curves::arithmetic::SqrtRatio;
let window = window.get_lower_32() as usize;
assert!(window < H);
Some(window)
} else {
None
}
window.map(|window| {
window
.to_le_bits()
.iter()
.by_vals()
.take(FIXED_BASE_WINDOW_SIZE)
.rev()
.fold(0, |acc, b| 2 * acc + if b { 1 } else { 0 })
})
})
.collect::<Vec<_>>()
}

7
halo2_gadgets/src/ecc/chip/mul_fixed/base_field_elem.rs
View File

@ -1,8 +1,9 @@
use super::super::{EccBaseFieldElemFixed, EccPoint, FixedPoints, NUM_WINDOWS, T_P};
use super::H_BASE;
use crate::utilities::bool_check;
use crate::{
primitives::sinsemilla,
sinsemilla::primitives as sinsemilla,
utilities::{bitrange_subset, lookup_range_check::LookupRangeCheckConfig, range_check},
};
@ -84,7 +85,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
// Range-constrain α_1 to be 2 bits
let alpha_1_range_check = range_check(alpha_1.clone(), 1 << 2);
// Boolean-constrain α_2
let alpha_2_range_check = range_check(alpha_2.clone(), 1 << 1);
let alpha_2_range_check = bool_check(alpha_2.clone());
// Check that α_1 + 2^2 α_2 = z_84_alpha
let z_84_alpha_check = z_84_alpha.clone()
- (alpha_1.clone() + alpha_2.clone() * pallas::Base::from(1 << 2));
@ -140,7 +141,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
)))
.chain(Some((
"MSB = 1 => a_43 = 0 or 1",
alpha_2.clone() * range_check(a_43, 2),
alpha_2.clone() * bool_check(a_43),
)))
.chain(Some((
"MSB = 1 => z_13_alpha_0_prime = 0",

59
halo2_gadgets/src/ecc/chip/mul_fixed/full_width.rs
View File

@ -43,7 +43,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
.coords_check(meta, window.clone())
.into_iter()
// Constrain each window to a 3-bit value:
// 1 * (window - 0) * (window - 1) * ... * (window - 7)
// window * (1 - window) * ... * (7 - window)
.chain(Some(("window range check", range_check(window, H)))),
)
});
@ -64,7 +64,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
Ok(EccScalarFixed {
value: scalar,
windows,
windows: Some(windows),
})
}
@ -87,10 +87,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
decompose_word::<pallas::Scalar>(&scalar, SCALAR_NUM_BITS, FIXED_BASE_WINDOW_SIZE)
});
// Store the scalar decomposition
let mut windows: ArrayVec<AssignedCell<pallas::Base, pallas::Base>, NUM_WINDOWS> =
ArrayVec::new();
// Transpose `Option<Vec<u8>>` into `Vec<Option<pallas::Base>>`.
let scalar_windows: Vec<Option<pallas::Base>> = if let Some(windows) = scalar_windows {
assert_eq!(windows.len(), NUM_WINDOWS);
windows
@ -101,6 +98,9 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
vec![None; NUM_WINDOWS]
};
// Store the scalar decomposition
let mut windows: ArrayVec<AssignedCell<pallas::Base, pallas::Base>, NUM_WINDOWS> =
ArrayVec::new();
for (idx, window) in scalar_windows.into_iter().enumerate() {
let window_cell = region.assign_advice(
|| format!("k[{:?}]", offset + idx),
@ -117,7 +117,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
pub fn assign(
&self,
mut layouter: impl Layouter<pallas::Base>,
scalar: Option<pallas::Scalar>,
scalar: &EccScalarFixed,
base: &<Fixed as FixedPoints<pallas::Affine>>::FullScalar,
) -> Result<(EccPoint, EccScalarFixed), Error>
where
@ -129,7 +129,11 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
|mut region| {
let offset = 0;
let scalar = self.witness(&mut region, offset, scalar)?;
// Lazily witness the scalar.
let scalar = match scalar.windows {
None => self.witness(&mut region, offset, scalar.value),
Some(_) => todo!("unimplemented for halo2_gadgets v0.1.0"),
}?;
let (acc, mul_b) = self.super_config.assign_region_inner::<_, NUM_WINDOWS>(
&mut region,
@ -184,7 +188,7 @@ pub mod tests {
use crate::ecc::{
chip::{EccChip, FixedPoint as _, H},
tests::{FullWidth, TestFixedBases},
FixedPoint, NonIdentityPoint, Point,
FixedPoint, NonIdentityPoint, Point, ScalarFixed,
};
pub(crate) fn test_mul_fixed(
@ -227,8 +231,13 @@ pub mod tests {
// [a]B
{
let scalar_fixed = pallas::Scalar::random(OsRng);
let by = ScalarFixed::new(
chip.clone(),
layouter.namespace(|| "random a"),
Some(scalar_fixed),
)?;
let (result, _) = base.mul(layouter.namespace(|| "random [a]B"), Some(scalar_fixed))?;
let (result, _) = base.mul(layouter.namespace(|| "random [a]B"), by)?;
constrain_equal_non_id(
chip.clone(),
layouter.namespace(|| "random [a]B"),
@ -243,14 +252,19 @@ pub mod tests {
// (There is another *non-canonical* sequence
// 5333333333333333333333333333333333333333332711161673731021062440252244051273333333333 in octal.)
{
const LAST_DOUBLING: &str = "1333333333333333333333333333333333333333333333333333333333333333333333333333333333334";
let h = pallas::Scalar::from(H as u64);
let scalar_fixed = "1333333333333333333333333333333333333333333333333333333333333333333333333333333333334"
.chars()
.fold(pallas::Scalar::zero(), |acc, c| {
acc * &h + &pallas::Scalar::from(c.to_digit(8).unwrap() as u64)
});
let (result, _) =
base.mul(layouter.namespace(|| "mul with double"), Some(scalar_fixed))?;
let scalar_fixed = LAST_DOUBLING
.chars()
.fold(pallas::Scalar::zero(), |acc, c| {
acc * &h + &pallas::Scalar::from(c.to_digit(8).unwrap() as u64)
});
let by = ScalarFixed::new(
chip.clone(),
layouter.namespace(|| LAST_DOUBLING),
Some(scalar_fixed),
)?;
let (result, _) = base.mul(layouter.namespace(|| "mul with double"), by)?;
constrain_equal_non_id(
chip.clone(),
@ -265,7 +279,9 @@ pub mod tests {
// on the last step.
{
let scalar_fixed = pallas::Scalar::zero();
let (result, _) = base.mul(layouter.namespace(|| "mul by zero"), Some(scalar_fixed))?;
let zero =
ScalarFixed::new(chip.clone(), layouter.namespace(|| "0"), Some(scalar_fixed))?;
let (result, _) = base.mul(layouter.namespace(|| "mul by zero"), zero)?;
if let Some(is_identity) = result.inner().is_identity() {
assert!(is_identity);
}
@ -274,7 +290,12 @@ pub mod tests {
// [-1]B is the largest scalar field element.
{
let scalar_fixed = -pallas::Scalar::one();
let (result, _) = base.mul(layouter.namespace(|| "mul by -1"), Some(scalar_fixed))?;
let neg_1 = ScalarFixed::new(
chip.clone(),
layouter.namespace(|| "-1"),
Some(scalar_fixed),
)?;
let (result, _) = base.mul(layouter.namespace(|| "mul by -1"), neg_1)?;
constrain_equal_non_id(
chip,
layouter.namespace(|| "mul by -1"),

57
halo2_gadgets/src/ecc/chip/mul_fixed/short.rs
View File

@ -35,9 +35,9 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
fn create_gate(&self, meta: &mut ConstraintSystem<pallas::Base>) {
meta.create_gate("Short fixed-base mul gate", |meta| {
let q_mul_fixed_short = meta.query_selector(self.q_mul_fixed_short);
let y_p = meta.query_advice(self.super_config.y_p, Rotation::cur());
let y_p = meta.query_advice(self.super_config.add_config.y_p, Rotation::cur());
let y_a = meta.query_advice(self.super_config.add_config.y_qr, Rotation::cur());
// z_21
// z_21 = k_21
let last_window = meta.query_advice(self.super_config.u, Rotation::cur());
let sign = meta.query_advice(self.super_config.window, Rotation::cur());
@ -46,12 +46,16 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
// Check that last window is either 0 or 1.
let last_window_check = bool_check(last_window);
// Check that sign is either 1 or -1.
let sign_check = sign.clone() * sign.clone() - one;
let sign_check = sign.clone().square() - one;
// `(x_a, y_a)` is the result of `[m]B`, where `m` is the magnitude.
// We conditionally negate this result using `y_p = y_a * s`, where `s` is the sign.
// Check that the final `y_p = y_a` or `y_p = -y_a`
//
// This constraint is redundant / unnecessary, because `sign` is constrained
// to -1 or 1 by `sign_check`, and `negation_check` therefore permits a strict
// subset of the cases that this constraint permits.
let y_check = (y_p.clone() - y_a.clone()) * (y_p.clone() + y_a.clone());
// Check that the correct sign is witnessed s.t. sign * y_p = y_a
@ -69,6 +73,10 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
});
}
/// Constraints `magnitude` to be at most 66 bits.
///
/// The final window is separately constrained to be a single bit, which completes the
/// 64-bit range constraint.
fn decompose(
&self,
region: &mut Region<'_, pallas::Base>,
@ -90,14 +98,14 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
Ok(EccScalarFixedShort {
magnitude,
sign,
running_sum: (*running_sum).as_slice().try_into().unwrap(),
running_sum: Some((*running_sum).as_slice().try_into().unwrap()),
})
}
pub fn assign(
&self,
mut layouter: impl Layouter<pallas::Base>,
magnitude_sign: MagnitudeSign,
scalar: &EccScalarFixedShort,
base: &<Fixed as FixedPoints<pallas::Affine>>::ShortScalar,
) -> Result<(EccPoint, EccScalarFixedShort), Error>
where
@ -110,7 +118,14 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
let offset = 0;
// Decompose the scalar
let scalar = self.decompose(&mut region, offset, magnitude_sign.clone())?;
let scalar = match scalar.running_sum {
None => self.decompose(
&mut region,
offset,
(scalar.magnitude.clone(), scalar.sign.clone()),
),
Some(_) => todo!("unimplemented for halo2_gadgets v0.1.0"),
}?;
let (acc, mul_b) = self
.super_config
@ -153,7 +168,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
// Copy last window to `u` column.
// (Although the last window is not a `u` value; we are copying it into the `u`
// column because there is an available cell there.)
let z_21 = scalar.running_sum[21].clone();
let z_21 = scalar.running_sum.as_ref().unwrap()[21].clone();
z_21.copy_advice(|| "last_window", &mut region, self.super_config.u, offset)?;
// Conditionally negate `y`-coordinate
@ -173,7 +188,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
// Assign final `y` to `y_p` column and return final point
let y_var = region.assign_advice(
|| "y_var",
self.super_config.y_p,
self.super_config.add_config.y_p,
offset,
|| y_val.ok_or(Error::Synthesis),
)?;
@ -243,7 +258,7 @@ pub mod tests {
ecc::{
chip::{EccChip, FixedPoint, MagnitudeSign},
tests::{Short, TestFixedBases},
FixedPointShort, NonIdentityPoint, Point,
FixedPointShort, NonIdentityPoint, Point, ScalarFixedShort,
},
utilities::{lookup_range_check::LookupRangeCheckConfig, UtilitiesInstructions},
};
@ -327,7 +342,12 @@ pub mod tests {
*magnitude,
*sign,
)?;
test_short.mul(layouter.namespace(|| *name), magnitude_sign)?
let by = ScalarFixedShort::new(
chip.clone(),
layouter.namespace(|| "signed short scalar"),
magnitude_sign,
)?;
test_short.mul(layouter.namespace(|| *name), by)?
};
// Move from base field into scalar field
let scalar = {
@ -361,7 +381,12 @@ pub mod tests {
*magnitude,
*sign,
)?;
test_short.mul(layouter.namespace(|| *name), magnitude_sign)?
let by = ScalarFixedShort::new(
chip.clone(),
layouter.namespace(|| "signed short scalar"),
magnitude_sign,
)?;
test_short.mul(layouter.namespace(|| *name), by)?
};
if let Some(is_identity) = result.inner().is_identity() {
assert!(is_identity);
@ -443,7 +468,7 @@ pub mod tests {
) -> Result<(), Error> {
let column = config.advices[0];
let short_config = config.mul_fixed_short;
let short_config = config.mul_fixed_short.clone();
let magnitude_sign = {
let magnitude = self.load_private(
layouter.namespace(|| "load magnitude"),
@ -452,10 +477,14 @@ pub mod tests {
)?;
let sign =
self.load_private(layouter.namespace(|| "load sign"), column, self.sign)?;
(magnitude, sign)
ScalarFixedShort::new(
EccChip::construct(config),
layouter.namespace(|| "signed short scalar"),
(magnitude, sign),
)?
};
short_config.assign(layouter, magnitude_sign, &Short)?;
short_config.assign(layouter, &magnitude_sign.inner, &Short)?;
Ok(())
}

19
halo2_gadgets/src/lib.rs
View File

@ -1,4 +1,18 @@
//! # halo2_gadgets
//! This crate provides various common gadgets and chips for use with `halo2_proofs`.
//!
//! # Gadgets
//!
//! Gadgets are an abstraction for writing reusable and interoperable circuit logic. They
//! do not create any circuit constraints or assignments themselves, instead interacting
//! with the circuit through a defined "instruction set". A circuit developer uses gadgets
//! by instantiating them with a particular choice of chip.
//!
//! # Chips
//!
//! Chips implement the low-level circuit constraints. The same instructions may be
//! implemented by multiple chips, enabling different performance trade-offs to be made.
//! Chips can be highly optimised by their developers, as long as they conform to the
//! defined instructions.
#![cfg_attr(docsrs, feature(doc_cfg))]
// Temporary until we have more of the crate implemented.
@ -12,8 +26,7 @@
pub mod ecc;
pub mod poseidon;
#[cfg(feature = "unstable")]
#[cfg_attr(docsrs, doc(cfg(feature = "unstable")))]
pub mod sha256;
pub mod sinsemilla;
pub mod utilities;
pub mod primitives;

7
halo2_gadgets/src/poseidon.rs
View File

@ -1,4 +1,4 @@
//! Gadget and chips for the Poseidon algebraic hash function.
//! The Poseidon algebraic hash function.
use std::convert::TryInto;
use std::fmt;
@ -14,9 +14,8 @@ use halo2_proofs::{
mod pow5;
pub use pow5::{Pow5Chip, Pow5Config, StateWord};
use crate::primitives::poseidon::{
Absorbing, ConstantLength, Domain, Spec, SpongeMode, Squeezing, State,
};
pub mod primitives;
use primitives::{Absorbing, ConstantLength, Domain, Spec, SpongeMode, Squeezing, State};
/// A word from the padded input to a Poseidon sponge.
#[derive(Clone, Debug)]

17
halo2_gadgets/src/poseidon/pow5.rs
View File

@ -10,12 +10,11 @@ use halo2_proofs::{
poly::Rotation,
};
use super::{PaddedWord, PoseidonInstructions, PoseidonSpongeInstructions};
use crate::primitives::poseidon::{Domain, Mds, Spec, State};
use crate::{
primitives::poseidon::{Absorbing, Squeezing},
utilities::Var,
use super::{
primitives::{Absorbing, Domain, Mds, Spec, Squeezing, State},
PaddedWord, PoseidonInstructions, PoseidonSpongeInstructions,
};
use crate::utilities::Var;
/// Configuration for a [`Pow5Chip`].
#[derive(Clone, Debug)]
@ -608,9 +607,9 @@ mod tests {
use rand::rngs::OsRng;
use super::{PoseidonInstructions, Pow5Chip, Pow5Config, StateWord};
use crate::{
poseidon::Hash,
primitives::poseidon::{self, ConstantLength, P128Pow5T3 as OrchardNullifier, Spec},
use crate::poseidon::{
primitives::{self as poseidon, ConstantLength, P128Pow5T3 as OrchardNullifier, Spec},
Hash,
};
use std::convert::TryInto;
use std::marker::PhantomData;
@ -850,7 +849,7 @@ mod tests {
#[test]
fn hash_test_vectors() {
for tv in crate::primitives::poseidon::test_vectors::fp::hash() {
for tv in crate::poseidon::primitives::test_vectors::fp::hash() {
let message = [
pallas::Base::from_repr(tv.input[0]).unwrap(),
pallas::Base::from_repr(tv.input[1]).unwrap(),

2
halo2_gadgets/src/primitives/poseidon.rs → halo2_gadgets/src/poseidon/primitives.rs
View File

@ -291,7 +291,7 @@ pub trait Domain<F: FieldExt, const RATE: usize> {
/// A Poseidon hash function used with constant input length.
///
/// Domain specified in section 4.2 of https://eprint.iacr.org/2019/458.pdf
/// Domain specified in [ePrint 2019/458 section 4.2](https://eprint.iacr.org/2019/458.pdf).
#[derive(Clone, Copy, Debug)]
pub struct ConstantLength<const L: usize>;

7
halo2_gadgets/src/primitives/poseidon/fp.rs → halo2_gadgets/src/poseidon/primitives/fp.rs
View File

@ -1,6 +1,11 @@
//! https://github.com/daira/pasta-hadeshash
//! Constants for using Poseidon with the Pallas field.
//!
//! The constants can be reproduced by running the following Sage script from
//! [this repository](https://github.com/daira/pasta-hadeshash):
//!
//! ```text
//! $ sage generate_parameters_grain.sage 1 0 255 3 8 56 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001
//! ```
use pasta_curves::pallas;
// Number of round constants: 192

7
halo2_gadgets/src/primitives/poseidon/fq.rs → halo2_gadgets/src/poseidon/primitives/fq.rs
View File

@ -1,6 +1,11 @@
//! https://github.com/daira/pasta-hadeshash
//! Constants for using Poseidon with the Vesta field.
//!
//! The constants can be reproduced by running the following Sage script from
//! [this repository](https://github.com/daira/pasta-hadeshash):
//!
//! ```text
//! sage generate_parameters_grain.sage 1 0 255 3 8 56 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
//! ```
use pasta_curves::vesta;
// Number of round constants: 192

0
halo2_gadgets/src/primitives/poseidon/grain.rs → halo2_gadgets/src/poseidon/primitives/grain.rs
View File

0
halo2_gadgets/src/primitives/poseidon/mds.rs → halo2_gadgets/src/poseidon/primitives/mds.rs
View File

10
halo2_gadgets/src/primitives/poseidon/p128pow5t3.rs → halo2_gadgets/src/poseidon/primitives/p128pow5t3.rs
View File

@ -75,7 +75,7 @@ mod tests {
super::{fp, fq},
Fp, Fq,
};
use crate::primitives::poseidon::{permute, ConstantLength, Hash, Spec};
use crate::poseidon::primitives::{permute, ConstantLength, Hash, Spec};
/// The same Poseidon specification as poseidon::P128Pow5T3, but constructed
/// such that its constants will be generated at runtime.
@ -250,7 +250,7 @@ mod tests {
{
let (round_constants, mds, _) = super::P128Pow5T3::constants();
for tv in crate::primitives::poseidon::test_vectors::fp::permute() {
for tv in crate::poseidon::primitives::test_vectors::fp::permute() {
let mut state = [
Fp::from_repr(tv.initial_state[0]).unwrap(),
Fp::from_repr(tv.initial_state[1]).unwrap(),
@ -268,7 +268,7 @@ mod tests {
{
let (round_constants, mds, _) = super::P128Pow5T3::constants();
for tv in crate::primitives::poseidon::test_vectors::fq::permute() {
for tv in crate::poseidon::primitives::test_vectors::fq::permute() {
let mut state = [
Fq::from_repr(tv.initial_state[0]).unwrap(),
Fq::from_repr(tv.initial_state[1]).unwrap(),
@ -286,7 +286,7 @@ mod tests {
#[test]
fn hash_test_vectors() {
for tv in crate::primitives::poseidon::test_vectors::fp::hash() {
for tv in crate::poseidon::primitives::test_vectors::fp::hash() {
let message = [
Fp::from_repr(tv.input[0]).unwrap(),
Fp::from_repr(tv.input[1]).unwrap(),
@ -298,7 +298,7 @@ mod tests {
assert_eq!(result.to_repr(), tv.output);
}
for tv in crate::primitives::poseidon::test_vectors::fq::hash() {
for tv in crate::poseidon::primitives::test_vectors::fq::hash() {
let message = [
Fq::from_repr(tv.input[0]).unwrap(),
Fq::from_repr(tv.input[1]).unwrap(),

0
halo2_gadgets/src/primitives/poseidon/test_vectors.rs → halo2_gadgets/src/poseidon/primitives/test_vectors.rs
View File

8
halo2_gadgets/src/primitives.rs
View File

@ -1,8 +0,0 @@
//! Primitives used in the Orchard protocol.
// TODO:
// - DH stuff
// - EphemeralPublicKey
// - EphemeralSecretKey
pub mod poseidon;
pub mod sinsemilla;

2
halo2_gadgets/src/sha256.rs
View File

@ -1,4 +1,4 @@
//! Gadget and chips for the [SHA-256] hash function.
//! The [SHA-256] hash function.
//!
//! [SHA-256]: https://tools.ietf.org/html/rfc6234

23
halo2_gadgets/src/sinsemilla.rs
View File

@ -1,4 +1,6 @@
//! Gadgets for the Sinsemilla hash function.
//! The [Sinsemilla] hash function.
//!
//! [Sinsemilla]: https://zips.z.cash/protocol/protocol.pdf#concretesinsemillahash
use crate::{
ecc::{self, EccInstructions, FixedPoints},
utilities::{FieldValue, RangeConstrained, Var},
@ -11,6 +13,7 @@ use std::fmt::Debug;
pub mod chip;
pub mod merkle;
mod message;
pub mod primitives;
/// The set of circuit instructions required to use the [`Sinsemilla`](https://zcash.github.io/halo2/design/gadgets/sinsemilla.html) gadget.
/// This trait is bounded on two constant parameters: `K`, the number of bits
@ -223,7 +226,9 @@ where
}
/// Constructs a `MessagePiece` by concatenating a sequence of [`RangeConstrained`]
/// subpieces.
/// subpiece values.
///
/// The `MessagePiece` is assigned to the circuit, but not constrained in any way.
///
/// # Panics
///
@ -414,7 +419,7 @@ where
&self,
mut layouter: impl Layouter<C::Base>,
message: Message<C, SinsemillaChip, K, MAX_WORDS>,
r: Option<C::Scalar>,
r: ecc::ScalarFixed<C, EccChip>,
) -> Result<
(
ecc::Point<C, EccChip>,
@ -437,7 +442,7 @@ where
&self,
mut layouter: impl Layouter<C::Base>,
message: Message<C, SinsemillaChip, K, MAX_WORDS>,
r: Option<C::Scalar>,
r: ecc::ScalarFixed<C, EccChip>,
) -> Result<(ecc::X<C, EccChip>, Vec<SinsemillaChip::RunningSum>), Error> {
assert_eq!(self.M.sinsemilla_chip, message.chip);
let (p, zs) = self.commit(layouter.namespace(|| "commit"), message, r)?;
@ -460,7 +465,8 @@ pub(crate) mod tests {
};
use crate::{
primitives::sinsemilla::{self, K},
ecc::ScalarFixed,
sinsemilla::primitives::{self as sinsemilla, K},
{
ecc::{
chip::{find_zs_and_us, EccChip, EccConfig, H, NUM_WINDOWS},
@ -685,12 +691,17 @@ pub(crate) mod tests {
(0..500).map(|_| Some(rand::random::<bool>())).collect();
let (result, _) = {
let r = ScalarFixed::new(
ecc_chip.clone(),
layouter.namespace(|| "r"),
Some(r_val),
)?;
let message = Message::from_bitstring(
chip2,
layouter.namespace(|| "witness message"),
message.clone(),
)?;
test_commit.commit(layouter.namespace(|| "commit"), message, Some(r_val))?
test_commit.commit(layouter.namespace(|| "commit"), message, r)?
};
// Witness expected result.

77
halo2_gadgets/src/sinsemilla/chip.rs
View File

@ -2,14 +2,14 @@
use super::{
message::{Message, MessagePiece},
CommitDomains, HashDomains, SinsemillaInstructions,
primitives as sinsemilla, CommitDomains, HashDomains, SinsemillaInstructions,
};
use crate::{
primitives::sinsemilla,
{
ecc::{chip::NonIdentityEccPoint, FixedPoints},
utilities::lookup_range_check::LookupRangeCheckConfig,
ecc::{
chip::{DoubleAndAdd, NonIdentityEccPoint},
FixedPoints,
},
utilities::lookup_range_check::LookupRangeCheckConfig,
};
use std::marker::PhantomData;
@ -47,21 +47,10 @@ where
q_sinsemilla4: Selector,
/// Fixed column used to load the y-coordinate of the domain $Q$.
fixed_y_q: Column<Fixed>,
/// Advice column used to store the x-coordinate of the accumulator at each
/// iteration of the hash.
x_a: Column<Advice>,
/// Advice column used to store the x-coordinate of the generator corresponding
/// to the message word at each iteration of the hash. This is looked up in the
/// generator table.
x_p: Column<Advice>,
/// Logic specific to merged double-and-add.
double_and_add: DoubleAndAdd,
/// Advice column used to load the message.
bits: Column<Advice>,
/// Advice column used to store the $\lambda_1$ intermediate value at each
/// iteration.
lambda_1: Column<Advice>,
/// Advice column used to store the $\lambda_2$ intermediate value at each
/// iteration.
lambda_2: Column<Advice>,
/// Advice column used to witness message pieces. This may or may not be the same
/// column as `bits`.
witness_pieces: Column<Advice>,
@ -81,16 +70,31 @@ where
{
/// Returns an array of all advice columns in this config, in arbitrary order.
pub(super) fn advices(&self) -> [Column<Advice>; 5] {
[self.x_a, self.x_p, self.bits, self.lambda_1, self.lambda_2]
[
self.double_and_add.x_a,
self.double_and_add.x_p,
self.bits,
self.double_and_add.lambda_1,
self.double_and_add.lambda_2,
]
}
/// Returns the lookup range check config used in this config.
pub fn lookup_config(&self) -> LookupRangeCheckConfig<pallas::Base, { sinsemilla::K }> {
self.lookup_config
}
/// Derives the expression `q_s3 = (q_s2) * (q_s2 - 1)`.
fn q_s3(&self, meta: &mut VirtualCells<pallas::Base>) -> Expression<pallas::Base> {
let one = Expression::Constant(pallas::Base::one());
let q_s2 = meta.query_fixed(self.q_sinsemilla2, Rotation::cur());
q_s2.clone() * (q_s2 - one)
}
}
/// A chip that implements 10-bit Sinsemilla using a lookup table and 5 advice columns.
///
/// [Chip description](https://zcash.github.io/halo2/design/gadgets/sinsemilla.html#plonk--halo-2-constraints).
#[derive(Eq, PartialEq, Clone, Debug)]
pub struct SinsemillaChip<Hash, Commit, Fixed>
where
@ -162,11 +166,13 @@ where
q_sinsemilla2: meta.fixed_column(),
q_sinsemilla4: meta.selector(),
fixed_y_q,
x_a: advices[0],
x_p: advices[1],
double_and_add: DoubleAndAdd {
x_a: advices[0],
x_p: advices[1],
lambda_1: advices[3],
lambda_2: advices[4],
},
bits: advices[2],
lambda_1: advices[3],
lambda_2: advices[4],
witness_pieces,
generator_table: GeneratorTableConfig {
table_idx: lookup.0,
@ -185,18 +191,12 @@ where
// Closures for expressions that are derived multiple times
// x_r = lambda_1^2 - x_a - x_p
let x_r = |meta: &mut VirtualCells<pallas::Base>, rotation| {
let x_a = meta.query_advice(config.x_a, rotation);
let x_p = meta.query_advice(config.x_p, rotation);
let lambda_1 = meta.query_advice(config.lambda_1, rotation);
lambda_1.square() - x_a - x_p
config.double_and_add.x_r(meta, rotation)
};
// Y_A = (lambda_1 + lambda_2) * (x_a - x_r)
let Y_A = |meta: &mut VirtualCells<pallas::Base>, rotation| {
let x_a = meta.query_advice(config.x_a, rotation);
let lambda_1 = meta.query_advice(config.lambda_1, rotation);
let lambda_2 = meta.query_advice(config.lambda_2, rotation);
(lambda_1 + lambda_2) * (x_a - x_r(meta, rotation))
config.double_and_add.Y_A(meta, rotation)
};
// Check that the initial x_A, x_P, lambda_1, lambda_2 are consistent with y_Q.
@ -215,17 +215,12 @@ where
meta.create_gate("Sinsemilla gate", |meta| {
let q_s1 = meta.query_selector(config.q_sinsemilla1);
// q_s3 = (q_s2) * (q_s2 - 1)
let q_s3 = {
let one = Expression::Constant(pallas::Base::one());
let q_s2 = meta.query_fixed(config.q_sinsemilla2, Rotation::cur());
q_s2.clone() * (q_s2 - one)
};
let q_s3 = config.q_s3(meta);
let lambda_1_next = meta.query_advice(config.lambda_1, Rotation::next());
let lambda_2_cur = meta.query_advice(config.lambda_2, Rotation::cur());
let x_a_cur = meta.query_advice(config.x_a, Rotation::cur());
let x_a_next = meta.query_advice(config.x_a, Rotation::next());
let lambda_1_next = meta.query_advice(config.double_and_add.lambda_1, Rotation::next());
let lambda_2_cur = meta.query_advice(config.double_and_add.lambda_2, Rotation::cur());
let x_a_cur = meta.query_advice(config.double_and_add.x_a, Rotation::cur());
let x_a_next = meta.query_advice(config.double_and_add.x_a, Rotation::next());
// x_r = lambda_1^2 - x_a_cur - x_p
let x_r = x_r(meta, Rotation::cur());

28
halo2_gadgets/src/sinsemilla/chip/generator_table.rs
View File

@ -1,4 +1,3 @@
use crate::primitives::sinsemilla::{self, SINSEMILLA_S};
use halo2_proofs::{
circuit::Layouter,
plonk::{ConstraintSystem, Error, Expression, TableColumn},
@ -6,6 +5,7 @@ use halo2_proofs::{
};
use super::{CommitDomains, FixedPoints, HashDomains};
use crate::sinsemilla::primitives::{self as sinsemilla, SINSEMILLA_S};
use pasta_curves::{arithmetic::FieldExt, pallas};
/// Table containing independent generators S[0..2^k]
@ -39,33 +39,25 @@ impl GeneratorTableConfig {
meta.lookup(|meta| {
let q_s1 = meta.query_selector(config.q_sinsemilla1);
let q_s2 = meta.query_fixed(config.q_sinsemilla2, Rotation::cur());
let q_s3 = {
let one = Expression::Constant(pallas::Base::one());
q_s2.clone() * (q_s2.clone() - one)
};
let q_s3 = config.q_s3(meta);
let q_run = q_s2 - q_s3;
// m_{i+1} = z_{i} - 2^K * (q_s2 - q_s3) * z_{i + 1}
// m_{i+1} = z_{i} - 2^K * q_{run,i} * z_{i + 1}
// Note that the message words m_i's are 1-indexed while the
// running sum z_i's are 0-indexed.
let word = {
let z_cur = meta.query_advice(config.bits, Rotation::cur());
let z_next = meta.query_advice(config.bits, Rotation::next());
z_cur - ((q_s2 - q_s3) * z_next * pallas::Base::from(1 << sinsemilla::K))
z_cur - (q_run * z_next * pallas::Base::from(1 << sinsemilla::K))
};
let x_p = meta.query_advice(config.x_p, Rotation::cur());
let x_p = meta.query_advice(config.double_and_add.x_p, Rotation::cur());
// y_{p,i} = (Y_{A,i} / 2) - lambda1 * (x_{A,i} - x_{P,i}),
// where Y_{A,i} = (lambda1_i + lambda2_i) * (x_{A,i} - x_{R,i}),
// x_{R,i} = lambda1^2 - x_{A,i} - x_{P,i}
//
// y_{p,i} = (Y_{A,i} / 2) - lambda1 * (x_{A,i} - x_{P,i})
let y_p = {
let lambda1 = meta.query_advice(config.lambda_1, Rotation::cur());
let lambda2 = meta.query_advice(config.lambda_2, Rotation::cur());
let x_a = meta.query_advice(config.x_a, Rotation::cur());
let x_r = lambda1.clone().square() - x_a.clone() - x_p.clone();
let Y_A = (lambda1.clone() + lambda2) * (x_a.clone() - x_r);
let lambda1 = meta.query_advice(config.double_and_add.lambda_1, Rotation::cur());
let x_a = meta.query_advice(config.double_and_add.x_a, Rotation::cur());
let Y_A = config.double_and_add.Y_A(meta, Rotation::cur());
(Y_A * pallas::Base::TWO_INV) - (lambda1 * (x_a - x_p.clone()))
};

74
halo2_gadgets/src/sinsemilla/chip/hash_to_point.rs
View File

@ -1,15 +1,17 @@
use super::super::{CommitDomains, HashDomains, SinsemillaInstructions};
use super::{NonIdentityEccPoint, SinsemillaChip};
use crate::{
ecc::FixedPoints,
sinsemilla::primitives::{self as sinsemilla, lebs2ip_k, INV_TWO_POW_K, SINSEMILLA_S},
};
use crate::ecc::FixedPoints;
use crate::primitives::sinsemilla::{self, lebs2ip_k, INV_TWO_POW_K, SINSEMILLA_S};
use halo2_proofs::circuit::AssignedCell;
use halo2_proofs::{
circuit::{Chip, Region},
plonk::Error,
plonk::{Assigned, Error},
};
use group::ff::{Field, PrimeField, PrimeFieldBits};
use group::ff::{PrimeField, PrimeFieldBits};
use pasta_curves::{
arithmetic::{CurveAffine, FieldExt},
pallas,
@ -55,13 +57,17 @@ where
config.q_sinsemilla4.enable(region, offset)?;
region.assign_fixed(|| "fixed y_q", config.fixed_y_q, offset, || Ok(y_q))?;
(Some(y_q)).into()
(Some(y_q.into())).into()
};
// Constrain the initial x_q to equal the x-coordinate of the domain's `Q`.
let mut x_a: X<pallas::Base> = {
let x_a =
region.assign_advice_from_constant(|| "fixed x_q", config.x_a, offset, x_q)?;
let x_a = region.assign_advice_from_constant(
|| "fixed x_q",
config.double_and_add.x_a,
offset,
x_q.into(),
)?;
x_a.into()
};
@ -90,7 +96,7 @@ where
// Assign the final y_a.
let y_a_cell = region.assign_advice(
|| "y_a",
config.lambda_1,
config.double_and_add.lambda_1,
offset,
|| y_a.ok_or(Error::Synthesis),
)?;
@ -101,13 +107,13 @@ where
{
region.assign_advice(
|| "dummy lambda2",
config.lambda_2,
config.double_and_add.lambda_2,
offset,
|| Ok(pallas::Base::zero()),
)?;
region.assign_advice(
|| "dummy x_p",
config.x_p,
config.double_and_add.x_p,
offset,
|| Ok(pallas::Base::zero()),
)?;
@ -120,8 +126,11 @@ where
#[allow(non_snake_case)]
// Check equivalence to result from primitives::sinsemilla::hash_to_point
{
use crate::primitives::sinsemilla::{K, S_PERSONALIZATION};
use crate::sinsemilla::message::MessagePiece;
use crate::sinsemilla::{
message::MessagePiece,
primitives::{K, S_PERSONALIZATION},
};
use group::{prime::PrimeCurveAffine, Curve};
use pasta_curves::arithmetic::CurveExt;
@ -150,8 +159,11 @@ where
let expected_point = bitstring
.chunks(K)
.fold(Q.to_curve(), |acc, chunk| (acc + S(chunk)) + acc);
let actual_point =
pallas::Affine::from_xy(*x_a.value().unwrap(), *y_a.value().unwrap()).unwrap();
let actual_point = pallas::Affine::from_xy(
x_a.value().unwrap().evaluate(),
y_a.value().unwrap().evaluate(),
)
.unwrap();
assert_eq!(expected_point.to_affine(), actual_point);
}
}
@ -164,7 +176,7 @@ where
}
}
Ok((
NonIdentityEccPoint::from_coordinates_unchecked(x_a.0, y_a),
NonIdentityEccPoint::from_coordinates_unchecked(x_a.0.evaluate(), y_a.evaluate()),
zs_sum,
))
}
@ -326,7 +338,7 @@ where
// Assign `x_p`
region.assign_advice(
|| "x_p",
config.x_p,
config.double_and_add.x_p,
offset + row,
|| x_p.ok_or(Error::Synthesis),
)?;
@ -338,12 +350,12 @@ where
.zip(y_a.0)
.zip(x_p)
.zip(y_p)
.map(|(((x_a, y_a), x_p), y_p)| (y_a - y_p) * (x_a - x_p).invert().unwrap());
.map(|(((x_a, y_a), x_p), y_p)| (y_a - y_p) * (x_a - x_p).invert());
// Assign lambda_1
region.assign_advice(
|| "lambda_1",
config.lambda_1,
config.double_and_add.lambda_1,
offset + row,
|| lambda_1.ok_or(Error::Synthesis),
)?;
@ -361,13 +373,13 @@ where
let lambda_2 = {
let lambda_2 = x_a.value().zip(y_a.0).zip(x_r).zip(lambda_1).map(
|(((x_a, y_a), x_r), lambda_1)| {
pallas::Base::from(2) * y_a * (x_a - x_r).invert().unwrap() - lambda_1
y_a * pallas::Base::from(2) * (x_a - x_r).invert() - lambda_1
},
);
region.assign_advice(
|| "lambda_2",
config.lambda_2,
config.double_and_add.lambda_2,
offset + row,
|| lambda_2.ok_or(Error::Synthesis),
)?;
@ -384,7 +396,7 @@ where
let x_a_cell = region.assign_advice(
|| "x_a",
config.x_a,
config.double_and_add.x_a,
offset + row + 1,
|| x_a_new.ok_or(Error::Synthesis),
)?;
@ -410,18 +422,18 @@ where
}
/// The x-coordinate of the accumulator in a Sinsemilla hash instance.
struct X<F: FieldExt>(AssignedCell<F, F>);
struct X<F: FieldExt>(AssignedCell<Assigned<F>, F>);
impl<F: FieldExt> From<AssignedCell<F, F>> for X<F> {
fn from(cell_value: AssignedCell<F, F>) -> Self {
impl<F: FieldExt> From<AssignedCell<Assigned<F>, F>> for X<F> {
fn from(cell_value: AssignedCell<Assigned<F>, F>) -> Self {
X(cell_value)
}
}
impl<F: FieldExt> Deref for X<F> {
type Target = AssignedCell<F, F>;
type Target = AssignedCell<Assigned<F>, F>;
fn deref(&self) -> &AssignedCell<F, F> {
fn deref(&self) -> &AssignedCell<Assigned<F>, F> {
&self.0
}
}
@ -431,18 +443,18 @@ impl<F: FieldExt> Deref for X<F> {
/// This is never actually witnessed until the last round, since it
/// can be derived from other variables. Thus it only exists as a field
/// element, not a `CellValue`.
struct Y<F: FieldExt>(Option<F>);
struct Y<F: FieldExt>(Option<Assigned<F>>);
impl<F: FieldExt> From<Option<F>> for Y<F> {
fn from(value: Option<F>) -> Self {
impl<F: FieldExt> From<Option<Assigned<F>>> for Y<F> {
fn from(value: Option<Assigned<F>>) -> Self {
Y(value)
}
}
impl<F: FieldExt> Deref for Y<F> {
type Target = Option<F>;
type Target = Option<Assigned<F>>;
fn deref(&self) -> &Option<F> {
fn deref(&self) -> &Option<Assigned<F>> {
&self.0
}
}

54
halo2_gadgets/src/sinsemilla/merkle.rs
View File

@ -11,7 +11,6 @@ use super::{HashDomains, SinsemillaInstructions};
use crate::utilities::{
cond_swap::CondSwapInstructions, i2lebsp, transpose_option_array, UtilitiesInstructions,
};
use std::iter;
pub mod chip;
@ -55,11 +54,11 @@ pub struct MerklePath<
const PATH_LENGTH: usize,
const K: usize,
const MAX_WORDS: usize,
const PAR: usize,
> where
MerkleChip: MerkleInstructions<C, PATH_LENGTH, K, MAX_WORDS> + Clone,
{
chip_1: MerkleChip,
chip_2: MerkleChip,
chips: [MerkleChip; PAR],
domain: MerkleChip::HashDomains,
leaf_pos: Option<u32>,
// The Merkle path is ordered from leaves to root.
@ -72,21 +71,27 @@ impl<
const PATH_LENGTH: usize,
const K: usize,
const MAX_WORDS: usize,
> MerklePath<C, MerkleChip, PATH_LENGTH, K, MAX_WORDS>
const PAR: usize,
> MerklePath<C, MerkleChip, PATH_LENGTH, K, MAX_WORDS, PAR>
where
MerkleChip: MerkleInstructions<C, PATH_LENGTH, K, MAX_WORDS> + Clone,
{
/// Constructs a [`MerklePath`].
///
/// A circuit may have many more columns available than are required by a single
/// `MerkleChip`. To make better use of the available circuit area, the `MerklePath`
/// gadget will distribute its path hashing across each `MerkleChip` in `chips`, such
/// that each chip processes `ceil(PATH_LENGTH / PAR)` layers (with the last chip
/// processing fewer layers if the division is inexact).
pub fn construct(
chip_1: MerkleChip,
chip_2: MerkleChip,
chips: [MerkleChip; PAR],
domain: MerkleChip::HashDomains,
leaf_pos: Option<u32>,
path: Option<[C::Base; PATH_LENGTH]>,
) -> Self {
assert_ne!(PAR, 0);
Self {
chip_1,
chip_2,
chips,
domain,
leaf_pos,
path,
@ -101,22 +106,26 @@ impl<
const PATH_LENGTH: usize,
const K: usize,
const MAX_WORDS: usize,
> MerklePath<C, MerkleChip, PATH_LENGTH, K, MAX_WORDS>
const PAR: usize,
> MerklePath<C, MerkleChip, PATH_LENGTH, K, MAX_WORDS, PAR>
where
MerkleChip: MerkleInstructions<C, PATH_LENGTH, K, MAX_WORDS> + Clone,
{
/// Calculates the root of the tree containing the given leaf at this Merkle path.
///
/// Implements [Zcash Protocol Specification Section 4.9: Merkle Path Validity][merklepath].
///
/// [merklepath]: https://zips.z.cash/protocol/protocol.pdf#merklepath
pub fn calculate_root(
&self,
mut layouter: impl Layouter<C::Base>,
leaf: MerkleChip::Var,
) -> Result<MerkleChip::Var, Error> {
// A Sinsemilla chip uses 5 advice columns, but the full Orchard action circuit
// uses 10 advice columns. We distribute the path hashing across two Sinsemilla
// chips to make better use of the available circuit area.
let chips = iter::empty()
.chain(iter::repeat(self.chip_1.clone()).take(PATH_LENGTH / 2))
.chain(iter::repeat(self.chip_2.clone()));
// Each chip processes `ceil(PATH_LENGTH / PAR)` layers.
let layers_per_chip = (PATH_LENGTH + PAR - 1) / PAR;
// Assign each layer to a chip.
let chips = (0..PATH_LENGTH).map(|i| self.chips[i / layers_per_chip].clone());
// The Merkle path is ordered from leaves to root, which is consistent with the
// little-endian representation of `pos` below.
@ -138,6 +147,9 @@ where
// we have `l` = 32 - 31 - 1 = 0.
// On the other hand, when `layer = 0` (the final sibling on the Merkle path),
// we have `l` = 32 - 0 - 1 = 31.
// Constrain which of (node, sibling) is (left, right) with a conditional swap
// tied to the current bit of the position.
let pair = {
let pair = (node, *sibling);
@ -145,11 +157,10 @@ where
chip.swap(layouter.namespace(|| "node position"), pair, *pos)?
};
// Each `hash_layer` consists of 52 Sinsemilla words:
// - l (10 bits) = 1 word
// - left (255 bits) || right (255 bits) = 51 words (510 bits)
// Compute the node in layer l from its children:
// M^l_i = MerkleCRH(l, M^{l+1}_{2i}, M^{l+1}_{2i+1})
node = chip.hash_layer(
layouter.namespace(|| format!("hash l {}", l)),
layouter.namespace(|| format!("MerkleCRH({}, left, right)", l)),
Q,
l,
pair.0,
@ -286,8 +297,7 @@ pub mod tests {
)?;
let path = MerklePath {
chip_1,
chip_2,
chips: [chip_1, chip_2],
domain: TestHashDomain,
leaf_pos: self.leaf_pos,
path: self.merkle_path,
@ -308,7 +318,7 @@ pub mod tests {
(sibling, &node)
};
use crate::primitives::sinsemilla;
use crate::sinsemilla::primitives as sinsemilla;
let merkle_crh = sinsemilla::HashDomain::from_Q(TestHashDomain.Q().into());
merkle_crh

203
halo2_gadgets/src/sinsemilla/merkle/chip.rs
View File

@ -10,7 +10,8 @@ use pasta_curves::{arithmetic::FieldExt, pallas};
use super::MerkleInstructions;
use crate::{
primitives::sinsemilla,
sinsemilla::{primitives as sinsemilla, MessagePiece},
utilities::RangeConstrained,
{
ecc::FixedPoints,
sinsemilla::{
@ -18,7 +19,6 @@ use crate::{
CommitDomains, HashDomains, SinsemillaInstructions,
},
utilities::{
bitrange_subset,
cond_swap::{CondSwapChip, CondSwapConfig, CondSwapInstructions},
UtilitiesInstructions,
},
@ -27,7 +27,7 @@ use crate::{
use group::ff::PrimeField;
/// Configuration for the `MerkleChip` implementation.
#[derive(Clone, Debug)]
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct MerkleConfig<Hash, Commit, Fixed>
where
Hash: HashDomains<pallas::Affine>,
@ -41,7 +41,16 @@ where
}
/// Chip implementing `MerkleInstructions`.
#[derive(Clone, Debug)]
///
/// This chip specifically implements `MerkleInstructions::hash_layer` as the `MerkleCRH`
/// function `hash = SinsemillaHash(Q, 𝑙⋆ || left⋆ || right⋆)`, where:
/// - `𝑙⋆ = I2LEBSP_10(l)`
/// - `left⋆ = I2LEBSP_255(left)`
/// - `right⋆ = I2LEBSP_255(right)`
///
/// This chip does **NOT** constrain `left⋆` and `right⋆` to be canonical encodings of
/// `left` and `right`.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct MerkleChip<Hash, Commit, Fixed>
where
Hash: HashDomains<pallas::Affine>,
@ -98,13 +107,11 @@ where
// The message pieces `a`, `b`, `c` are constrained by Sinsemilla to be
// 250 bits, 20 bits, and 250 bits respectively.
//
/*
The pieces and subpieces are arranged in the following configuration:
| A_0 | A_1 | A_2 | A_3 | A_4 | q_decompose |
-------------------------------------------------------
| a | b | c | left | right | 1 |
| z1_a | z1_b | b_1 | b_2 | l | |
*/
// The pieces and subpieces are arranged in the following configuration:
// | A_0 | A_1 | A_2 | A_3 | A_4 | q_decompose |
// -------------------------------------------------------
// | a | b | c | left | right | 1 |
// | z1_a | z1_b | b_1 | b_2 | l | 0 |
meta.create_gate("Decomposition check", |meta| {
let q_decompose = meta.query_selector(q_decompose);
let l_whole = meta.query_advice(advices[4], Rotation::next());
@ -122,14 +129,13 @@ where
let right_node = meta.query_advice(advices[4], Rotation::cur());
// a = a_0||a_1 = l || (bits 0..=239 of left)
// Check that a_0 = l
//
// z_1 of SinsemillaHash(a) = a_1
// => a_0 = a - (a_1 * 2^10)
let z1_a = meta.query_advice(advices[0], Rotation::next());
let a_1 = z1_a;
// a_0 = a - (a_1 * 2^10)
let a_0 = a_whole - a_1.clone() * pallas::Base::from(1 << 10);
let l_check = a_0 - l_whole;
// Derive a_0 (constrained by SinsemillaHash to be 10 bits)
let a_0 = a_whole - a_1.clone() * two_pow_10;
// b = b_0||b_1||b_2
// = (bits 240..=249 of left) || (bits 250..=254 of left) || (bits 0..=4 of right)
@ -165,7 +171,7 @@ where
Constraints::with_selector(
q_decompose,
[
("l_check", l_check),
("l_check", a_0 - l_whole),
("left_check", left_check),
("right_check", right_check),
("b1_b2_check", b1_b2_check),
@ -191,9 +197,9 @@ impl<Hash, Commit, F, const MERKLE_DEPTH: usize>
MerkleInstructions<pallas::Affine, MERKLE_DEPTH, { sinsemilla::K }, { sinsemilla::C }>
for MerkleChip<Hash, Commit, F>
where
Hash: HashDomains<pallas::Affine>,
Hash: HashDomains<pallas::Affine> + Eq,
F: FixedPoints<pallas::Affine>,
Commit: CommitDomains<pallas::Affine, F, Hash>,
Commit: CommitDomains<pallas::Affine, F, Hash> + Eq,
{
#[allow(non_snake_case)]
fn hash_layer(
@ -215,93 +221,95 @@ where
// b = b_0||b_1||b_2
// = (bits 240..=249 of left) || (bits 250..=254 of left) || (bits 0..=4 of right)
// c = bits 5..=254 of right
//
// We start by witnessing all of the individual pieces, and range-constraining the
// short pieces b_1 and b_2.
// `a = a_0||a_1` = `l` || (bits 0..=239 of `left`)
let a = {
let a = {
// a_0 = l
let a_0 = bitrange_subset(&pallas::Base::from(l as u64), 0..10);
// a_1 = (bits 0..=239 of `left`)
let a_1 = left.value().map(|value| bitrange_subset(value, 0..240));
a_1.map(|a_1| a_0 + a_1 * pallas::Base::from(1 << 10))
};
self.witness_message_piece(layouter.namespace(|| "Witness a = a_0 || a_1"), a, 25)?
};
let a = MessagePiece::from_subpieces(
self.clone(),
layouter.namespace(|| "Witness a = a_0 || a_1"),
[
RangeConstrained::bitrange_of(Some(&pallas::Base::from(l as u64)), 0..10),
RangeConstrained::bitrange_of(left.value(), 0..240),
],
)?;
// b = b_0 || b_1 || b_2
// = (bits 240..=249 of left) || (bits 250..=254 of left) || (bits 0..=4 of right)
let (b_1, b_2, b) = {
// b_0 = (bits 240..=249 of `left`)
let b_0 = left.value().map(|value| bitrange_subset(value, 240..250));
let b_0 = RangeConstrained::bitrange_of(left.value(), 240..250);
// b_1 = (bits 250..=254 of `left`)
// Constrain b_1 to 5 bits.
let b_1 = {
let b_1 = left
.value()
.map(|value| bitrange_subset(value, 250..(pallas::Base::NUM_BITS as usize)));
config
.sinsemilla_config
.lookup_config()
.witness_short_check(layouter.namespace(|| "Constrain b_1 to 5 bits"), b_1, 5)?
};
let b_1 = RangeConstrained::witness_short(
&config.sinsemilla_config.lookup_config(),
layouter.namespace(|| "b_1"),
left.value(),
250..(pallas::Base::NUM_BITS as usize),
)?;
// b_2 = (bits 0..=4 of `right`)
// Constrain b_2 to 5 bits.
let b_2 = {
let b_2 = right.value().map(|value| bitrange_subset(value, 0..5));
let b_2 = RangeConstrained::witness_short(
&config.sinsemilla_config.lookup_config(),
layouter.namespace(|| "b_2"),
right.value(),
0..5,
)?;
config
.sinsemilla_config
.lookup_config()
.witness_short_check(layouter.namespace(|| "Constrain b_2 to 5 bits"), b_2, 5)?
};
let b = {
let b = b_0
.zip(b_1.value())
.zip(b_2.value())
.map(|((b_0, b_1), b_2)| {
b_0 + b_1 * pallas::Base::from(1 << 10) + b_2 * pallas::Base::from(1 << 15)
});
self.witness_message_piece(
layouter.namespace(|| "Witness b = b_0 || b_1 || b_2"),
b,
2,
)?
};
let b = MessagePiece::from_subpieces(
self.clone(),
layouter.namespace(|| "Witness b = b_0 || b_1 || b_2"),
[b_0, b_1.value(), b_2.value()],
)?;
(b_1, b_2, b)
};
let c = {
// `c = bits 5..=254 of `right`
let c = right
.value()
.map(|value| bitrange_subset(value, 5..(pallas::Base::NUM_BITS as usize)));
self.witness_message_piece(layouter.namespace(|| "Witness c"), c, 25)?
};
// c = bits 5..=254 of `right`
let c = MessagePiece::from_subpieces(
self.clone(),
layouter.namespace(|| "Witness c"),
[RangeConstrained::bitrange_of(
right.value(),
5..(pallas::Base::NUM_BITS as usize),
)],
)?;
// hash = SinsemillaHash(Q, 𝑙⋆ || left⋆ || right⋆)
//
// `hash = ⊥` is handled internally to `SinsemillaChip::hash_to_point`: incomplete
// addition constraints allows ⊥ to occur, and then during synthesis it detects
// these edge cases and raises an error (aborting proof creation).
//
// Note that MerkleCRH as-defined maps ⊥ to 0. This is for completeness outside
// the circuit (so that the ⊥ does not propagate into the type system). The chip
// explicitly doesn't map ⊥ to 0; in fact it cannot, as doing so would require
// constraints that amount to using complete addition. The rationale for excluding
// this map is the same as why Sinsemilla uses incomplete addition: this situation
// yields a nontrivial discrete log relation, and by assumption it is hard to find
// these.
let (point, zs) = self.hash_to_point(
layouter.namespace(|| format!("hash at l = {}", l)),
Q,
vec![a.clone(), b.clone(), c.clone()].into(),
vec![a.inner(), b.inner(), c.inner()].into(),
)?;
let hash = Self::extract(&point);
// `SinsemillaChip::hash_to_point` returns the running sum for each `MessagePiece`.
// Grab the outputs we need for the decomposition constraints.
let z1_a = zs[0][1].clone();
let z1_b = zs[1][1].clone();
// Check that the pieces have been decomposed properly.
/*
The pieces and subpieces are arranged in the following configuration:
| A_0 | A_1 | A_2 | A_3 | A_4 | q_decompose |
-------------------------------------------------------
| a | b | c | left | right | 1 |
| z1_a | z1_b | b_1 | b_2 | l | |
*/
//
// The pieces and subpieces are arranged in the following configuration:
// | A_0 | A_1 | A_2 | A_3 | A_4 | q_decompose |
// -------------------------------------------------------
// | a | b | c | left | right | 1 |
// | z1_a | z1_b | b_1 | b_2 | l | 0 |
{
layouter.assign_region(
|| "Check piece decomposition",
@ -319,14 +327,26 @@ where
// Offset 0
// Copy and assign `a` at the correct position.
a.cell_value()
.copy_advice(|| "copy a", &mut region, config.advices[0], 0)?;
a.inner().cell_value().copy_advice(
|| "copy a",
&mut region,
config.advices[0],
0,
)?;
// Copy and assign `b` at the correct position.
b.cell_value()
.copy_advice(|| "copy b", &mut region, config.advices[1], 0)?;
b.inner().cell_value().copy_advice(
|| "copy b",
&mut region,
config.advices[1],
0,
)?;
// Copy and assign `c` at the correct position.
c.cell_value()
.copy_advice(|| "copy c", &mut region, config.advices[2], 0)?;
c.inner().cell_value().copy_advice(
|| "copy c",
&mut region,
config.advices[2],
0,
)?;
// Copy and assign the left node at the correct position.
left.copy_advice(|| "left", &mut region, config.advices[3], 0)?;
// Copy and assign the right node at the correct position.
@ -338,21 +358,22 @@ where
// Copy and assign z_1 of SinsemillaHash(b) = b_1
z1_b.copy_advice(|| "z1_b", &mut region, config.advices[1], 1)?;
// Copy `b_1`, which has been constrained to be a 5-bit value
b_1.copy_advice(|| "b_1", &mut region, config.advices[2], 1)?;
b_1.inner()
.copy_advice(|| "b_1", &mut region, config.advices[2], 1)?;
// Copy `b_2`, which has been constrained to be a 5-bit value
b_2.copy_advice(|| "b_2", &mut region, config.advices[3], 1)?;
b_2.inner()
.copy_advice(|| "b_2", &mut region, config.advices[3], 1)?;
Ok(())
},
)?;
}
let result = Self::extract(&point);
// Check layer hash output against Sinsemilla primitives hash
#[cfg(test)]
{
use crate::{primitives::sinsemilla::HashDomain, utilities::i2lebsp};
use crate::{sinsemilla::primitives::HashDomain, utilities::i2lebsp};
use group::ff::PrimeFieldBits;
if let (Some(left), Some(right)) = (left.value(), right.value()) {
@ -377,11 +398,11 @@ where
let expected = merkle_crh.hash(message.into_iter()).unwrap();
assert_eq!(expected.to_repr(), result.value().unwrap().to_repr());
assert_eq!(expected.to_repr(), hash.value().unwrap().to_repr());
}
}
Ok(result)
Ok(hash)
}
}

2
halo2_gadgets/src/primitives/sinsemilla.rs → halo2_gadgets/src/sinsemilla/primitives.rs
View File

@ -1,4 +1,4 @@
//! The Sinsemilla hash function and commitment scheme.
//! Implementation of Sinsemilla outside the circuit.
use group::{Curve, Wnaf};
use halo2_proofs::arithmetic::{CurveAffine, CurveExt};

0
halo2_gadgets/src/primitives/sinsemilla/addition.rs → halo2_gadgets/src/sinsemilla/primitives/addition.rs
View File

4
halo2_gadgets/src/primitives/sinsemilla/sinsemilla_s.rs → halo2_gadgets/src/sinsemilla/primitives/sinsemilla_s.rs
View File

@ -1,9 +1,9 @@
use super::K;
use pasta_curves::pallas;
/// The precomputed bases for the Sinsemilla hash function.
/// The precomputed bases for the [Sinsemilla hash function][concretesinsemillahash].
///
/// https://zips.z.cash/protocol/protocol.pdf#concretesinsemillahash
/// [concretesinsemillahash]: https://zips.z.cash/protocol/protocol.pdf#concretesinsemillahash
pub const SINSEMILLA_S: [(pallas::Base, pallas::Base); 1 << K] = [
(
pallas::Base::from_raw([

2
halo2_gadgets/src/utilities/cond_swap.rs
View File

@ -46,7 +46,7 @@ impl<F: FieldExt> Chip<F> for CondSwapChip<F> {
}
/// Configuration for the [`CondSwapChip`].
#[derive(Clone, Debug)]
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CondSwapConfig {
q_swap: Selector,
a: Column<Advice>,

3
halo2_gadgets/src/utilities/lookup_range_check.rs
View File

@ -400,7 +400,8 @@ mod tests {
use super::LookupRangeCheckConfig;
use super::super::lebs2ip;
use crate::primitives::sinsemilla::K;
use crate::sinsemilla::primitives::K;
use ff::{Field, PrimeFieldBits};
use halo2_proofs::{
circuit::{Layouter, SimpleFloorPlanner},

42
halo2_proofs/src/plonk/assigned.rs
View File

@ -121,6 +121,13 @@ impl<F: Field> Add<F> for Assigned<F> {
}
}
impl<F: Field> Add<F> for &Assigned<F> {
type Output = Assigned<F>;
fn add(self, rhs: F) -> Assigned<F> {
*self + rhs
}
}
impl<F: Field> Add<&Assigned<F>> for Assigned<F> {
type Output = Assigned<F>;
fn add(self, rhs: &Self) -> Assigned<F> {
@ -128,6 +135,20 @@ impl<F: Field> Add<&Assigned<F>> for Assigned<F> {
}
}
impl<F: Field> Add<Assigned<F>> for &Assigned<F> {
type Output = Assigned<F>;
fn add(self, rhs: Assigned<F>) -> Assigned<F> {
*self + rhs
}
}
impl<F: Field> Add<&Assigned<F>> for &Assigned<F> {
type Output = Assigned<F>;
fn add(self, rhs: &Assigned<F>) -> Assigned<F> {
*self + *rhs
}
}
impl<F: Field> AddAssign for Assigned<F> {
fn add_assign(&mut self, rhs: Self) {
*self = *self + rhs;
@ -154,6 +175,13 @@ impl<F: Field> Sub<F> for Assigned<F> {
}
}
impl<F: Field> Sub<F> for &Assigned<F> {
type Output = Assigned<F>;
fn sub(self, rhs: F) -> Assigned<F> {
*self - rhs
}
}
impl<F: Field> Sub<&Assigned<F>> for Assigned<F> {
type Output = Assigned<F>;
fn sub(self, rhs: &Self) -> Assigned<F> {
@ -161,6 +189,20 @@ impl<F: Field> Sub<&Assigned<F>> for Assigned<F> {
}
}
impl<F: Field> Sub<Assigned<F>> for &Assigned<F> {
type Output = Assigned<F>;
fn sub(self, rhs: Assigned<F>) -> Assigned<F> {
*self - rhs
}
}
impl<F: Field> Sub<&Assigned<F>> for &Assigned<F> {
type Output = Assigned<F>;
fn sub(self, rhs: &Assigned<F>) -> Assigned<F> {
*self - *rhs
}
}
impl<F: Field> SubAssign for Assigned<F> {
fn sub_assign(&mut self, rhs: Self) {
*self = *self - rhs;