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

[book] Remove gadgets documentation. 

The book now instead references the Halo 2 book for relevant circuit
documentation.
This commit is contained in:
therealyingtong 2022-02-04 14:03:45 +08:00 committed by Jack Grigg
parent 159ab53da5
commit e130643508
11 changed files with 30 additions and 1196 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
book/src/SUMMARY.md
View File

@ -17,12 +17,5 @@
- [Signatures](design/signatures.md)
- [Circuit](design/circuit.md)
- [Gadgets](design/circuit/gadgets.md)
- [Elliptic curve cryptography](design/circuit/gadgets/ecc.md)
- [Incomplete and complete addition](design/circuit/gadgets/ecc/addition.md)
- [Fixed-base scalar multiplication](design/circuit/gadgets/ecc/fixed-base-scalar-mul.md)
- [Variable-base scalar multiplication](design/circuit/gadgets/ecc/var-base-scalar-mul.md)
- [Sinsemilla](design/circuit/gadgets/sinsemilla.md)
- [MerkleCRH](design/circuit/gadgets/sinsemilla/merkle-crh.md)
- [CommitIvk](design/circuit/gadgets/sinsemilla/commit-ivk.md)
- [NoteCommit](design/circuit/gadgets/sinsemilla/note-commit.md)
- [Decomposition](design/circuit/gadgets/decomposition.md)
- [CommitIvk](design/circuit/commit-ivk.md)
- [NoteCommit](design/circuit/note-commit.md)

0
book/src/design/circuit/gadgets/sinsemilla/commit-ivk.md → book/src/design/circuit/commit-ivk.md
View File

28
book/src/design/circuit/gadgets.md
View File

@ -1 +1,29 @@
# Gadgets
The Orchard circuit makes use of the following gadgets from the `halo2_gadgets` crate:
- [Elliptic curve](https://zcash.github.io/halo2/design/gadgets/ecc.html):
- `FixedPoint`
- `FixedPointBaseField`
- `FixedPointShort`
- `NonIdentityPoint`
- `Point`
- Poseidon:
- `Hash<ConstantLength>`
- [Sinsemilla](https://zcash.github.io/halo2/design/gadgets/sinsemilla.html):
- `CommitDomain`
- `Message`
- `MessagePiece`
- [`MerklePath`](https://zcash.github.io/halo2/design/gadgets/sinsemilla/merkle-crh.html)
It instantiates the instruction sets required for these gadgets with the following chips:
- `halo2_gadgets::ecc::chip::EccChip`
- `halo2_gadgets::poseidon::Pow5Chip`
- [`halo2_gadgets::sinsemilla::chip::SinsemillaChip`](https://zcash.github.io/halo2/design/gadgets/sinsemilla.html#plonk--halo-2-constraints)
- [`halo2_gadgets::sinsemilla::merkle::chip::MerkleChip`](https://zcash.github.io/halo2/design/gadgets/sinsemilla/merkle-crh.html#circuit-components)
- `halo2_gadgets::utilities::UtilitiesInstructions`
- [`halo2_gadgets::utilities::lookup_range_check::LookupRangeCheckConfig`](https://zcash.github.io/halo2/design/gadgets/decomposition.html#lookup-decomposition)
It also makes use of the following utility functions for standardising constraints:
- `halo2_gadgets::utilities::{bitrange_subset, bool_check}`

76
book/src/design/circuit/gadgets/decomposition.md
View File

@ -1,76 +0,0 @@
# Decomposition
Given a field element $\alpha$, these gadgets decompose it into $W$ $K$-bit windows $$\alpha = k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + \cdots + 2^{(W-1)K} \cdot k_{W-1}$$ where each $k_i$ a $K$-bit value.
This is done using a running sum $z_i, i \in [0..W).$ We initialize the running sum $z_0 = \alpha,$ and compute subsequent terms $z_{i+1} = \frac{z_i - k_i}{2^{K}}.$ This gives us:
$$
\begin{aligned}
z_0 &= \alpha \\
&= k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + 2^{3K} \cdot k_3 + \cdots, \\
z_1 &= (z_0 - k_0) / 2^K \\
&= k_1 + 2^{K} \cdot k_2 + 2^{2K} \cdot k_3 + \cdots, \\
z_2 &= (z_1 - k_1) / 2^K \\
&= k_2 + 2^{K} \cdot k_3 + \cdots, \\
&\vdots \\
\downarrow &\text{ (in strict mode)} \\
z_W &= (z_{W-1} - k_{W-1}) / 2^K \\
&= 0 \text{ (because } z_{W-1} = k_{W-1} \text{)}
\end{aligned}
$$
### Strict mode
Strict mode constrains the running sum output $z_{W}$ to be zero, thus range-constraining the field element to be within $W \cdot K$ bits.
In strict mode, we are also assured that $z_{W-1} = k_{W-1}$ gives us the last window in the decomposition.
## Lookup decomposition
This gadget makes use of a $K$-bit lookup table to decompose a field element $\alpha$ into $K$-bit words. Each $K$-bit word $k_i = z_i - 2^K \cdot z_{i+1}$ is range-constrained by a lookup in the $K$-bit table.
The region layout for the lookup decomposition uses a single advice column $z$, and two selectors $q_{lookup}$ and $q_{running}.$
$$
\begin{array}{|c|c|c|}
\hline
z & q_\mathit{lookup} & q_\mathit{running} \\\hline
\hline
z_0 & 1 & 1 \\\hline
z_1 & 1 & 1 \\\hline
\vdots & \vdots & \vdots \\\hline
z_{n-1} & 1 & 1 \\\hline
z_n & 0 & 0 \\\hline
\end{array}
$$
### Short range check
Using two $K$-bit lookups, we can range-constrain a field element $\alpha$ to be $n$ bits, where $n \leq K.$ To do this:
1. Constrain $0 \leq \alpha < 2^K$ to be within $K$ bits using a $K$-bit lookup.
2. Constrain $0 \leq \alpha \cdot 2^{K - n} < 2^K$ to be within $K$ bits using a $K$-bit lookup.
The short variant of the lookup decomposition introduces a $q_{bitshift}$ selector. The same advice column $z$ has here been renamed to $\textsf{word}$ for clarity:
$$
\begin{array}{|c|c|c|c|}
\hline
\textsf{word} & q_\mathit{lookup} & q_\mathit{running} & q_\mathit{bitshift} \\\hline
\hline
\alpha & 1 & 0 & 0 \\\hline
\alpha' & 1 & 0 & 1 \\\hline
2^{K-n} & 0 & 0 & 0 \\\hline
\end{array}
$$
where $\alpha' = \alpha \cdot 2^{K - n}.$ Note that $2^{K-n}$ is assigned to a fixed column at keygen, and copied in at proving time. This is used in the gate enabled by the $q_\mathit{bitshift}$ selector to check that $\alpha$ was shifted correctly:
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
2 & q_\mathit{bitshift} \cdot (\alpha' - (\alpha \cdot 2^{K - n})) \\\hline
\end{array}
$$
### Combined lookup expression
Since the lookup decomposition and its short variant both make use of the same lookup table, we combine their lookup input expressions into a single one:
$$q_\mathit{lookup} \cdot \left(q_\mathit{running} \cdot (z_i - 2^K \cdot z_{i+1}) + (1 - q_\mathit{running}) \cdot \textsf{word} \right)$$
where $z_i$ and $\textsf{word}$ are the same cell (but distinguished here for clarity of usage).
## Short range decomposition
For a short range (for instance, $[0, \texttt{range})$ where $\texttt{range} \leq 8$), we can range-constrain each word using a degree-$\texttt{range}$ polynomial constraint instead of a lookup: $$\RangeCheck{word}{range} = \texttt{word} \cdot (1 - \texttt{word}) \cdots (\texttt{range} - 1 - \texttt{word}).$$

0
book/src/design/circuit/gadgets/ecc.md
View File

355
book/src/design/circuit/gadgets/ecc/addition.md
View File

@ -1,355 +0,0 @@
We will use formulae for curve arithmetic using affine coordinates on short Weierstrass curves,
derived from section 4.1 of [Hüseyin Hışıl's thesis](https://core.ac.uk/download/pdf/10898289.pdf).
## Incomplete addition
- Inputs: $P = (x_p, y_p), Q = (x_q, y_q)$
- Output: $R = P \;⸭\; Q = (x_r, y_r)$
The formulae from Hışıl's thesis are:
- $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$
Rename:
- $(x_1, y_1)$ to $(x_q, y_q)$
- $(x_2, y_2)$ to $(x_p, y_p)$
- $(x_3, y_3)$ to $(x_r, y_r)$.
Let $\lambda = \frac{y_q - y_p}{x_q - x_p} = \frac{y_p - y_q}{x_p - x_q}$, which we implement as
$\lambda \cdot (x_p - x_q) = y_p - y_q$
Also,
- $x_r = \lambda^2 - x_q - x_p$
- $y_r = \lambda \cdot (x_q - x_r) - y_q$
which is equivalent to
- $x_r + x_q + x_p = \lambda^2$
Assuming $x_p \neq x_q$,
$
\begin{array}{lrrll}
&&(x_r + x_q + x_p) \cdot (x_p - x_q)^2 &=& \lambda^2 \cdot (x_p - x_q)^2 \\
&\implies &(x_r + x_q + x_p) \cdot (x_p - x_q)^2 &=& \big(\lambda \cdot (x_p - x_q)\big)^2 \\[1.2ex]
\text{and} \\
& &y_r &=& \lambda \cdot (x_q - x_r) - y_q \\
&\implies &y_r + y_q &=& \lambda \cdot (x_q - x_r) \\
&\implies &(y_r + y_q) \cdot (x_p - x_q) &=& \lambda \cdot (x_p - x_q) \cdot (x_q - x_r)
\end{array}
$
Substituting for $\lambda \cdot (x_p - x_q)$, we get the constraints:
- $(x_r + x_q + x_p) \cdot (x_p - x_q)^2 - (y_p - y_q)^2 = 0$
- Note that this constraint is unsatisfiable for $P \;⸭\; (-P)$ (when $P \neq \mathcal{O}$),
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$
## Complete addition
$\hspace{1em} \begin{array}{rcll}
\mathcal{O} &+& \mathcal{O} &= \mathcal{O} \\[0.4ex]
\mathcal{O} &+& (x_q, y_q) &= (x_q, y_q) \\[0.4ex]
(x_p, y_p) &+& \mathcal{O} &= (x_p, y_p) \\[0.6ex]
(x, y) &+& (x, y) &= [2] (x, y) \\[0.6ex]
(x, y) &+& (x, -y) &= \mathcal{O} \\[0.4ex]
(x_p, y_p) &+& (x_q, y_q) &= (x_p, y_p) \;⸭\; (x_q, y_q), \text{ if } x_p \neq x_q.
\end{array}$
Suppose that we represent $\mathcal{O}$ as $(0, 0)$. ($0$ is not an $x$-coordinate of a valid point because we would need $y^2 = x^3 + 5$, and $5$ is not square in $\mathbb{F}_q$. Also $0$ is not a $y$-coordinate of a valid point because $-5$ is not a cube in $\mathbb{F}_q$.)
$$
\begin{aligned}
P + Q &= R\\
(x_p, y_p) + (x_q, y_q) &= (x_r, y_r) \\
\lambda &= \frac{y_q - y_p}{x_q - x_p} \\
x_r &= \lambda^2 - x_p - x_q \\
y_r &= \lambda(x_p - x_r) - y_p
\end{aligned}
$$
For the doubling case, Hışıl's thesis tells us that $\lambda$ has to
instead be computed as $\frac{3x^2}{2y}$.
Define $\mathsf{inv0}(x) = \begin{cases} 0, &\text{if } x = 0 \\ 1/x, &\text{otherwise.} \end{cases}$
Witness $\alpha, \beta, \gamma, \delta, \lambda$ where:
$\hspace{1em}
\begin{array}{rl}
\alpha \,\,=&\!\! \mathsf{inv0}(x_q - x_p) \\[0.4ex]
\beta \,\,=&\!\! \mathsf{inv0}(x_p) \\[0.4ex]
\gamma \,\,=&\!\! \mathsf{inv0}(x_q) \\[0.4ex]
\delta \,\,=&\!\! \begin{cases}
\mathsf{inv0}(y_q + y_p), &\text{if } x_q = x_p \\
0, &\text{otherwise}
\end{cases} \\[2.5ex]
\lambda \,\,=&\!\! \begin{cases}
\frac{y_q - y_p}{x_q - x_p}, &\text{if } x_q \neq x_p \\[1.2ex]
\frac{3{x_p}^2}{2y_p} &\text{if } x_q = x_p \wedge y_p \neq 0 \\[0.8ex]
0, &\text{otherwise.}
\end{cases}
\end{array}
$
### Constraints
$$
\begin{array}{|c|rcl|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]
5 & q_\mathit{add} \cdot (1 - (x_q - x_p) \cdot \alpha) \cdot \left(2y_p \cdot \lambda - 3{x_p}^2\right) &=& 0 & \begin{cases} x_q = x_p \wedge y_p \neq 0 \implies \lambda = \frac{3{x_p}^2}{2y_p} \\ x_q = x_p \wedge y_p = 0 \implies x_p = 0 \end{cases} \\\hline
6 & q_\mathit{add} \cdot x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda^2 - x_p - x_q - x_r) &=& 0 & x_p \neq 0 \wedge x_q \neq 0 \wedge x_q \neq x_p \implies x_r = \lambda^2 - x_p - x_q \\
6 & q_\mathit{add} \cdot x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) &=& 0 & x_p \neq 0 \wedge x_q \neq 0 \wedge x_q \neq x_p \implies y_r = \lambda \cdot (x_p - x_r) - y_p \\
6 & q_\mathit{add} \cdot x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda^2 - x_p - x_q - x_r) &=& 0 & x_p \neq 0 \wedge x_q \neq 0 \wedge y_q \neq -y_p \implies x_r = \lambda^2 - x_p - x_q \\
6 & q_\mathit{add} \cdot x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) &=& 0 & x_p \neq 0 \wedge x_q \neq 0 \wedge y_q \neq -y_p \implies y_r = \lambda \cdot (x_p - x_r) - y_p \\\hline
4 & q_\mathit{add} \cdot (1 - x_p \cdot \beta) \cdot (x_r - x_q) &=& 0 & x_p = 0 \implies x_r = x_q \\
4 & q_\mathit{add} \cdot (1 - x_p \cdot \beta) \cdot (y_r - y_q) &=& 0 & x_p = 0 \implies y_r = y_q \\\hline
4 & q_\mathit{add} \cdot (1 - x_q \cdot \gamma) \cdot (x_r - x_p) &=& 0 & x_q = 0 \implies x_r = x_p \\
4 & q_\mathit{add} \cdot (1 - x_q \cdot \gamma) \cdot (y_r - y_p) &=& 0 & x_q = 0 \implies y_r = y_p \\\hline
4 & q_\mathit{add} \cdot (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot x_r &=& 0 & x_q = x_p \wedge y_q = -y_p \implies x_r = 0 \\
4 & q_\mathit{add} \cdot (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot y_r &=& 0 & x_q = x_p \wedge y_q = -y_p \implies y_r = 0 \\\hline
\end{array}
$$
Max degree: 6
### Analysis of constraints
$$
\begin{array}{rl}
1. & (x_q - x_p) \cdot ((x_q - x_p) \cdot \lambda - (y_q - y_p)) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } &x_q - x_p = 0 \\
\text{or } &(x_q - x_p) \cdot \lambda - (y_q - y_p) = 0 \\
\end{aligned} \\
& \text{must be satisfied for the constraint to be satisfied.} \\
& \\
& \text{If } x_q - x_p \neq 0, \text{ then } (x_q - x_p) \cdot \lambda - (y_q - y_p) = 0, \text{ and} \\
& \text{by rearranging both sides we get } \lambda = (y_q - y_p) / (x_q - x_p). \\
& \\
& \text{Therefore:} \\
& \hspace{2em} x_q \neq x_p \implies \lambda = (y_q - y_p) / (x_q - x_p).\\
& \\
2. & (1 - (x_q - x_p) \cdot \alpha) \cdot (2y_p \cdot \lambda - 3x_p^2) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } &(1 - (x_q - x_p) \cdot \alpha) = 0 \\
\text{or } &(2y_p \cdot \lambda - 3x_p^2) = 0
\end{aligned} \\
& \text{must be satisfied for the constraint to be satisfied.} \\
& \\
& \text{If } x_q = x_p, \text{ then } 1 - (x_q - x_p) \cdot \alpha = 0 \text{ has no solution for } \alpha, \\
& \text{so it must be that } 2y_p \cdot \lambda - 3x_p^2 = 0. \\
& \\
& \text{If } x_q = x_p \text{ and } y_p = 0 \text{ then } x_p = 0, \text{ and the constraint is satisfied.}\\
& \\
& \text{If } x_q = x_p \text{ and } y_p \neq 0 \text{ then by rearranging both sides} \\
& \text{we get } \lambda = 3x_p^2 / 2y_p. \\
& \\
& \text{Therefore:} \\
& \hspace{2em} (x_q = x_p) \wedge y_p \neq 0 \implies \lambda = 3x_p^2 / 2y_p. \\
& \\
3.\text{ a)} & x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda^2 - x_p - x_q - x_r) = 0 \\
\text{ b)} & x_p \cdot x_q \cdot (x_q - x_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) = 0 \\
\text{ c)} & x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda^2 - x_p - x_q - x_r) = 0 \\
\text{ d)} & x_p \cdot x_q \cdot (y_q + y_p) \cdot (\lambda \cdot (x_p - x_r) - y_p - y_r) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } &x_p = 0 \\
\text{or } &x_p = 0 \\
\text{or } &(x_q - x_p) = 0 \\
\text{or } &(\lambda^2 - x_p - x_q - x_r) = 0 \\
\end{aligned} \\
& \text{must be satisfied for constraint (a) to be satisfied.} \\
& \\
& \text{If } x_p \neq 0 \wedge x_q \neq 0 \wedge x_q \neq x_p, \\[1.5ex]
& \text{• Constraint (a) imposes that } x_r = \lambda^2 - x_p - x_q. \\
& \text{• Constraint (b) imposes that } y_r = \lambda \cdot (x_p - x_r) - y_p. \\
& \\
& \text{If } x_p \neq 0 \wedge x_q \neq 0 \wedge y_q \neq -y_p, \\[1.5ex]
& \text{• Constraint (c) imposes that } x_r = \lambda^2 - x_p - x_q. \\
& \text{• Constraint (d) imposes that } y_r = \lambda \cdot (x_p - x_r) - y_p. \\
& \\
& \text{Therefore:} \\
& \begin{aligned}
&(x_p \neq 0) \wedge (x_q \neq 0) \wedge ((x_q \neq x_p) \vee (y_q \neq -y_p)) \\
\implies &(x_r = \lambda^2 - x_p - x_q) \wedge (y_r = \lambda \cdot (x_p - x_r) - y_p).
\end{aligned} \\
& \\
4.\text{ a)} & (1 - x_p \cdot \beta) \cdot (x_r - x_q) = 0 \\
\text{ b)} & (1 - x_p \cdot \beta) \cdot (y_r - y_q) = 0 \\
& \\
& \begin{aligned}
\text{At least one of } 1 - x_p \cdot \beta &= 0 \\
\text{or } x_r - x_q &= 0
\end{aligned} \\
& \text{must be satisfied for constraint (a) to be satisfied.} \\
& \\
& \text{If } x_p = 0 \text{ then } 1 - x_p \cdot \beta = 0 \text{ has no solutions for } \beta, \\
& \text{and so it must be that } x_r - x_q = 0. \\
& \\
& \text{Similarly, constraint (b) imposes that if } x_p = 0 \\
& \text{then } y_r - y_q = 0. \\
& \\
& \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 \\
& \\
& \begin{aligned}
\text{At least one of } 1 - x_q \cdot \beta &= 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{and so it must be that } x_r - x_p = 0. \\
& \\
& \text{Similarly, constraint (b) imposes that if } x_q = 0 \\
& \text{then } y_r - y_p = 0. \\
& \\
& \text{Therefore:} \\
& \hspace{2em} x_q = 0 \implies (x_r, y_r) = (x_p, y_p). \\
& \\
6.\text{ a)} & (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot x_r = 0 \\
\text{ b)} & (1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta) \cdot y_r = 0 \\
& \\
& \begin{aligned}
\text{At least one of } &1 - (x_q - x_p) \cdot \alpha - (y_q + y_p) \cdot \delta = 0 \\
\text{or } &x_r = 0
\end{aligned} \\
& \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{However, if } x_q = x_p \wedge y_q = -y_p, \text{ then there are no solutions for } \alpha \text { and } \delta. \\
& \\
& \text{Therefore: } \\
& \hspace{2em} x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0).
\end{array}
$$
#### Propositions:
$
\begin{array}{cl}
(1)& x_q \neq x_p \implies \lambda = (y_q - y_p) / (x_q - x_p) \\[0.8ex]
(2)& (x_q = x_p) \wedge y_p \neq 0 \implies \lambda = 3x_p^2 / 2y_p \\[0.8ex]
(3)& (x_p \neq 0) \wedge (x_q \neq 0) \wedge ((x_q \neq x_p) \vee (y_q \neq -y_p)) \\[0.4ex]
&\implies (x_r = \lambda^2 - x_p - x_q) \wedge (y_r = \lambda \cdot (x_p - x_r) - y_p) \\[0.8ex]
(4)& x_p = 0 \implies (x_r, y_r) = (x_q, y_q) \\[0.8ex]
(5)& x_q = 0 \implies (x_r, y_r) = (x_p, y_p) \\[0.8ex]
(6)& x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0)
\end{array}
$
#### Cases:
$(x_p, y_p) + (x_q, y_q) = (x_r, y_r)$
Note that we rely on the fact that $0$ is not a valid $x$-coordinate or $y$-coordinate of a
point on the Pallas curve other than $\mathcal{O}$.
* $(0, 0) + (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{holds because } x_q = x_p \\
(2)&\text{holds because } y_p = 0 \\
(3)&\text{holds because } x_p = 0 \\
(4)&\text{holds because } (x_r, y_r) = (x_q, y_q) = (0, 0) \\
(5)&\text{holds because } (x_r, y_r) = (x_p, y_p) = (0, 0) \\
(6)&\text{holds because } (x_r, y_r) = (0, 0). \\
\end{array}
$
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution to $(6).$
* $(x, y) + (0, 0)$ for $(x, y) \neq (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{holds because } x_q \neq x_p, \text{ therefore } \lambda = (y_q - y_p) / (x_q - x_p) \text{ is a solution} \\
(2)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ is a solution} \\
(3)&\text{holds because } x_q = 0 \\
(4)&\text{holds because } x_p \neq 0, \text{ therefore } \beta = x_p^{-1} \text{ is a solution} \\
(5)&\text{holds because } (x_r, y_r) = (x_p, y_p) \\
(6)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ and } \delta = 0 \text{ is a solution.}
\end{array}
$
- Soundness: $(x_r, y_r) = (x_p, y_p)$ is the only solution to $(5).$
* $(0, 0) + (x, y)$ for $(x, y) \neq (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{holds because } x_q \neq x_p, \text{ therefore } \lambda = (y_q - y_p) / (x_q - x_p) \text{ is a solution} \\
(2)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ is a solution} \\
(3)&\text{holds because } x_p = 0 \\
(4)&\text{holds because } x_p = 0 \text{ only when } (x_r, y_r) = (x_q, y_q) \\
(5)&\text{holds because } x_q \neq 0, \text{ therefore } \gamma = x_q^{-1} \text{ is a solution}\\
(6)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ and } \delta = 0 \text{ is a solution.}
\end{array}
$
- Soundness: $(x_r, y_r) = (x_q, y_q)$ is the only solution to $(4).$
* $(x, y) + (x, y)$ for $(x, y) \neq (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{holds because } x_q = x_p \\
(2)&\text{holds because } x_q = x_p \wedge y_p \neq 0, \text{ therefore } \lambda = 3x_p^2 / 2y_p \text{ is a solution}\\
(3)&\text{holds because } x_r = \lambda^2 - x_p - x_q \wedge y_r = \lambda \cdot (x_p - x_r) - y_p \text{ in this case} \\
(4)&\text{holds because } x_p \neq 0, \text{ therefore } \beta = x_p^{-1} \text{ is a solution} \\
(5)&\text{holds because } x_p \neq 0, \text{ therefore } \gamma = x_q^{-1} \text{ is a solution} \\
(6)&\text{holds because } x_q = x_p \text{ and } y_q \neq -y_p, \text{ therefore } \alpha = 0 \text{ and } \delta = (y_q + y_p)^{-1} \text{ is a solution.} \\
\end{array}
$
- Soundness: $\lambda$ is computed correctly, and $(x_r, y_r) = (\lambda^2 - x_p - x_q, \lambda \cdot (x_p - x_r) - y_p)$ is the only solution.
* $(x, y) + (x, -y)$ for $(x, y) \neq (0, 0)$
- Completeness:
$
\begin{array}{cl}
(1)&\text{holds because } x_q = x_p \\
(2)&\text{holds because } x_q = x_p \wedge y_p \neq 0, \text{ therefore } \lambda = 3x_p^2 / 2y_p \text{ is a solution} \\
&\text{(although } \lambda \text{ is not used in this case)} \\
(3)&\text{holds because } x_q = x_p \text{ and } y_q = -y_p \\
(4)&\text{holds because } x_p \neq 0, \text{ therefore } \beta = x_p^{-1} \text{ is a solution} \\
(5)&\text{holds because } x_q \neq 0, \text{ therefore } \gamma = x_q^{-1} \text{ is a solution} \\
(6)&\text{holds because } (x_r, y_r) = (0, 0) \\
\end{array}
$
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution to $(6).$
* $(x_p, y_p) + (x_q, y_q)$ for $(x_p, y_p) \neq (0,0)$ and $(x_q, y_q) \neq (0, 0)$ and $x_p \neq x_q$
- Completeness:
$
\begin{array}{cl}
(1)&\text{holds because } x_q \neq x_p, \text{ therefore } \lambda = (y_q - y_p) / (x_q - x_p) \text{ is a solution} \\
(2)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ is a solution} \\
(3)&\text{holds because } x_r = \lambda^2 - x_p - x_q \wedge y_r = \lambda \cdot (x_p - x_r) - y_p \text{ in this case} \\
(4)&\text{holds because } x_p \neq 0, \text{ therefore } \beta = x_p^{-1} \text{ is a solution} \\
(5)&\text{holds because } x_q \neq 0, \text{ therefore } \gamma = x_q^{-1} \text{ is a solution} \\
(6)&\text{holds because } x_q \neq x_p, \text{ therefore } \alpha = (x_q - x_p)^{-1} \text{ and } \delta = 0 \text{ is a solution.}
\end{array}
$
- Soundness: $\lambda$ is computed correctly, and $(x_r, y_r) = (\lambda^2 - x_p - x_q, \lambda \cdot (x_p - x_r) - y_p)$ is the only solution.

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

@ -1,194 +0,0 @@
# Fixed-base scalar multiplication
There are $6$ fixed bases in the Orchard protocol:
- $\mathcal{K}^{\mathsf{Orchard}}$, used in deriving the nullifier;
- $\mathcal{G}^{\mathsf{Orchard}}$, used in spend authorization;
- $\mathcal{R}$ base for $\mathsf{NoteCommit}^{\mathsf{Orchard}}$;
- $\mathcal{V}$ and $\mathcal{R}$ bases for $\mathsf{ValueCommit}^{\mathsf{Orchard}}$; and
- $\mathcal{R}$ base for $\mathsf{Commit}^{\mathsf{ivk}}$.
## Decompose scalar
We support fixed-base scalar multiplication with three types of scalars:
### Full-width scalar
A $255$-bit scalar from $\mathbb{F}_q$. We decompose a full-width scalar $\alpha$ into $85$ $3$-bit windows:
$$\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}
$$
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
\end{array}
$$
where $\RangeCheck{\text{word}}{\texttt{range}} = \text{word} \cdot (1 - \text{word}) \cdots (\texttt{range} - 1 - \text{word}).$
### Base field element
We support using a base field element as the scalar in fixed-base multiplication. This occurs, for example, in the scalar multiplication for the nullifier computation of the Action circuit $\mathsf{DeriveNullifier_{nk}} = \mathsf{Extract}_\mathbb{P}\left(\left[(\mathsf{PRF_{nk}^{nfOrchard}}(\rho) + \psi) \bmod{q_\mathbb{P}}\right]\mathcal{K}^\mathsf{Orchard} + \mathsf{cm}\right)$: here, the scalar $$\left[(\mathsf{PRF_{nk}^{nfOrchard}}(\rho) + \psi) \bmod{q_\mathbb{P}}\right]$$ is the result of a base field addition.
Decompose the base field element $\alpha$ into three-bit windows, and range-constrain each window, using the [short range decomposition](../decomposition.md#short-range-decomposition) gadget in strict mode, with $W = 85, K = 3.$
If $k_{0..84}$ is witnessed directly then no issue of canonicity arises. However, because the scalar is given as a base field element here, care must be taken to ensure a canonical representation, since $2^{255} > p$. That is, we must check that $0 \leq \alpha < p,$ where $p$ the is Pallas base field modulus $$p = 2^{254} + t_p = 2^{254} + 45560315531419706090280762371685220353.$$ Note that $t_p < 2^{130}.$
To do this, we decompose $\alpha$ into three pieces: $$\alpha = \alpha_0 \text{ (252 bits) } \,||\, \alpha_1 \text{ (2 bits) } \,||\, \alpha_2 \text{ (1 bit) }.$$
We check the correctness of this decomposition by:
$$
\begin{array}{|c|l|}
\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
2 & q_\text{canon-base-field} \cdot \left(z_{84} - (\alpha_1 + \alpha_2 \cdot 2^2)\right) = 0 \\\hline
\end{array}
$$
If the MSB $\alpha_2 = 0$ is not set, then $\alpha < 2^{254} < p.$ However, in the case where $\alpha_2 = 1$, we must check:
- $\alpha_2 = 1 \implies \alpha_1 = 0;$
- $\alpha_2 = 1 \implies \alpha_0 < t_p$:
- $\alpha_2 = 1 \implies 0 \leq \alpha_0 < 2^{130}$,
- $\alpha_2 = 1 \implies 0 \leq \alpha_0 + 2^{130} - t_p < 2^{130}$
To check that $0 \leq \alpha_0 < 2^{130},$ we make use of the three-bit running sum decomposition:
- Firstly, we constrain $\alpha_0$ to be a $132$-bit value by enforcing its high $120$ bits to be all-zero. We can get $\textsf{alpha\_0\_hi\_120}$ from the decomposition:
$$
\begin{aligned}
z_{44} &= k_{44} + 2^3 k_{45} + \cdots + 2^{3 \cdot (84 - 44)} k_{84}\\
\implies \textsf{alpha\_0\_hi\_120} &= z_{44} - 2^{3 \cdot (84 - 44)} k_{84}\\
&= z_{44} - 2^{3 \cdot (40)} z_{84}.
\end{aligned}
$$
- Then, we constrain bits $130..\!\!=\!\!131$ of $\alpha_0$ to be zeroes; in other words, we constrain the three-bit word $k_{43} = \alpha[129..\!\!=\!\!131] = \alpha_0[129..\!\!=\!\!131] \in \{0, 1\}.$ We make use of the running sum decomposition to obtain $k_{43} = z_{43} - z_{44} \cdot 2^3.$
Define $\alpha'_0 = \alpha_0 + 2^{130} - t_p$. To check that $0 \leq \alpha'_0 < 2^{130},$ we use 13 ten-bit [lookups](../decomposition.md#lookup-decomposition), where we constrain the $z_{13}$ running sum output of the lookup to be $0$ if $\alpha_2 = 1.$
$$
\begin{array}{|c|l|l|}
\hline
\text{Degree} & \text{Constraint} & \text{Comment} \\\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
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}
$$
### Short signed scalar
A short signed scalar is witnessed as a magnitude $m$ and sign $s$ such that
$$
s \in \{-1, 1\} \\
m \in [0, 2^{64}) \\
\mathsf{v^{old}} - \mathsf{v^{new}} = s \cdot m.
$$
This is used for $\mathsf{ValueCommit^{Orchard}}$. We want to compute $\mathsf{ValueCommit^{Orchard}_{rcv}}(\mathsf{v^{old}} - \mathsf{v^{new}}) = [\mathsf{v^{old}} - \mathsf{v^{new}}] \mathcal{V} + [\mathsf{rcv}] \mathcal{R}$, where
$$
-(2^{64}-1) \leq \mathsf{v^{old}} - \mathsf{v^{new}} \leq 2^{64}-1
$$
$\mathsf{v^{old}}$ and $\mathsf{v^{new}}$ are each already constrained to $64$ bits (by their use as inputs to $\mathsf{NoteCommit^{Orchard}}$).
Decompose the magnitude $m$ into three-bit windows, and range-constrain each window, using the [short range decomposition](../decomposition.md#short-range-decomposition) gadget in strict mode, with $W = 22, K = 3.$
We have two additional constraints:
$$
\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
\end{array}
$$
where $\BoolCheck{x} = x \cdot (1 - x)$.
## Load fixed base
Then, we precompute multiples of the fixed base $B$ for each window. This takes the form of a window table: $M[0..W)[0..8)$ such that:
- for the first (W-1) rows $M[0..(W-1))[0..8)$: $$M[w][k] = [(k+2) \cdot (2^3)^w]B$$
- in the last row $M[W-1][0..8)$: $$M[w][k] = [k \cdot (2^3)^w - \sum\limits_{j=0}^{83} 2^{3j+1}]B$$
The additional $(k + 2)$ term lets us avoid adding the point at infinity in the case $k = 0$. We offset these accumulated terms by subtracting them in the final window, i.e. we subtract $\sum\limits_{j=0}^{W-2} 2^{3j+1}$.
> Note: Although an offset of $(k + 1)$ would naively suffice, it introduces an edge case when $k_0 = 7, k_1= 0$.
> In this case, the window table entries evaluate to the same point:
> * $M[0][k_0] = [(7+1)*(2^3)^0]B = [8]B,$
> * $M[1][k_1] = [(0+1)*(2^3)^1]B = [8]B.$
>
> In fixed-base scalar multiplication, we sum the multiples of $B$ at each window (except the last) using incomplete addition.
> Since the point doubling case is not handled by incomplete addition, we avoid it by using an offset of $(k+2).$
For each window of fixed-base multiples $M[w] = (M[w][0], \cdots, M[w][7]), w \in [0..(W-1))$:
- Define a Lagrange interpolation polynomial $\mathcal{L}_x(k)$ that maps $k \in [0..8)$ to the $x$-coordinate of the multiple $M[w][k]$, i.e.
$$
\mathcal{L}_x(k) = \begin{cases}
([(k + 2) \cdot (2^3)^w] B)_x &\text{for } w \in [0..(W-1)); \\
([k \cdot (2^3)^w - \sum\limits_{j=0}^{83} 2^{3j+1}] B)_x &\text{for } w = 84; \text{ and}
\end{cases}
$$
- Find a value $z_w$ such that $z_w + (M[w][k])_y$ is a square $u^2$ in the field, but the wrong-sign $y$-coordinate $z_w - (M[w][k])_y$ does not produce a square.
Repeating this for all $W$ windows, we end up with:
- an $W \times 8$ table $\mathcal{L}_x$ storing $8$ coefficients interpolating the $x-$coordinate for each window. Each $x$-coordinate interpolation polynomial will be of the form
$$\mathcal{L}_x[w](k) = c_0 + c_1 \cdot k + c_2 \cdot k^2 + \cdots + c_7 \cdot k^7,$$
where $k \in [0..8), w \in [0..85)$ and $c_k$'s are the coefficients for each power of $k$; and
- a length-$W$ array $Z$ of $z_w$'s.
We load these precomputed values into fixed columns whenever we do fixed-base scalar multiplication in the circuit.
## Fixed-base scalar multiplication
Given a decomposed scalar $\alpha$ and a fixed base $B$, we compute $[\alpha]B$ as follows:
1. For each $k_w, w \in [0..85), k_w \in [0..8)$ in the scalar decomposition, witness the $x$- and $y$-coordinates $(x_w,y_w) = M[w][k_w].$
2. Check that $(x_w, y_w)$ is on the curve: $y_w^2 = x_w^3 + b$.
3. Witness $u_w$ such that $y_w + z_w = u_w^2$.
4. For all windows but the last, use [incomplete addition](./incomplete-add.md) to sum the $M[w][k_w]$'s, resulting in $[\alpha - k_{84} \cdot (2^3)^{84} + \sum\limits_{j=0}^{83} 2^{3j+1}]B$.
5. For the last window, use complete addition $M[83][k_{83}] + M[84][k_{84}]$ and return the final result.
> Note: complete addition is required in the final step to correctly map $[0]B$ to a representation of the point at infinity, $(0,0)$; and also to handle a corner case for which the last step is a doubling.
Constraints:
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
8 & q_\text{mul-fixed} \cdot \left( \mathcal{L}_x[w](k_w) - x_w \right) = 0 \\\hline
4 & q_\text{mul-fixed} \cdot \left( y_w^2 - x_w^3 - b \right) = 0 \\\hline
3 & q_\text{mul-fixed} \cdot \left( u_w^2 - y_w - Z[w] \right) = 0 \\\hline
\end{array}
$$
where $b = 5$ (from the Pallas curve equation).
### Signed short exponent
Recall that the signed short exponent is witnessed as a $64-$bit magnitude $m$, and a sign $s \in {1, -1}.$ Using the above algorithm, we compute $P = [m] \mathcal{B}$. Then, to get the final result $P',$ we conditionally negate $P$ using $(x, y) \mapsto (x, s \cdot y)$.
Constraints:
$$
\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
\end{array}
$$
## Layout
$$
\begin{array}{|c|c|c|c|c|c|c|c|}
\hline
x_P & y_P & x_{QR} & y_{QR} & u & \text{window} & L_{0..=7} & \textsf{fixed\_z} \\\hline
x_{P,0} & y_{P,0} & & & u_0 & \text{window}_0 & L_{0..=7,0} & \textsf{fixed\_z}_0 \\\hline
x_{P,1} & y_{P,1} & x_{Q,1} = x_{P,0} & y_{Q,1} = y_{P,0} & u_1 & \text{window}_1 & L_{0..=7,1} & \textsf{fixed\_z}_1 \\\hline
x_{P,2} & y_{P,2} & x_{Q,2} = x_{R,1} & y_{Q,2} = y_{R,1} & u_2 & \text{window}_2 & L_{0..=7,1} & \textsf{fixed\_z}_2 \\\hline
\vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots \\\hline
\end{array}
$$
Note: this doesn't include the last row that uses [complete addition](./addition.md#Complete-addition). In the implementation this is allocated in a different region.

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

@ -1,331 +0,0 @@
# Variable-base scalar multiplication
In the Orchard circuit we need to check $\mathsf{pk_d} = [\mathsf{ivk}] \mathsf{g_d}$ where $\mathsf{ivk} \in [0, p)$ and the scalar field is $\mathbb{F}_q$ with $p < q$.
We have $p = 2^{254} + t_p$ and $q = 2^{254} + t_q$, for $t_p, t_q < 2^{128}$.
## Witness scalar
We're trying to compute $[\alpha] T$ for $\alpha \in [0, q)$. Set $k = \alpha + t_q$ and $n = 254$. Then we can compute
$\begin{array}{cl}
[2^{254} + (\alpha + t_q)] T &= [2^{254} + (\alpha + t_q) - (2^{254} + t_q)] T \\
&= [\alpha] T
\end{array}$
provided that $\alpha + t_q \in [0, 2^{n+1})$, i.e. $\alpha < 2^{n+1} - t_q$ which covers the whole range we need because in fact $2^{255} - t_q > q$.
Thus, given a scalar $\alpha$, we witness the boolean decomposition of $k = \alpha + t_q.$ (We use big-endian bit order for convenient input into the variable-base scalar multiplication algorithm.)
$$k = k_{254} \cdot 2^{254} + k_{253} \cdot 2^{253} + \cdots + k_0.$$
## Variable-base scalar multiplication
We use an optimized double-and-add algorithm, copied from ["Faster variable-base scalar multiplication in zk-SNARK circuits"](https://github.com/zcash/zcash/issues/3924) with some variable name changes:
```ignore
Acc := [2] T
for i from n-1 down to 0 {
P := k_{i+1} ? T : −T
Acc := (Acc + P) + Acc
}
return (k_0 = 0) ? (Acc - T) : Acc
```
It remains to check that the x-coordinates of each pair of points to be added are distinct.
When adding points in a prime-order group, we can rely on Theorem 3 from Appendix C of the [Halo paper](https://eprint.iacr.org/2019/1021.pdf), which says that if we have two such points with nonzero indices wrt a given odd-prime order base, where the indices taken in the range $-(q-1)/2..(q-1)/2$ are distinct disregarding sign, then they have different x-coordinates. This is helpful, because it is easier to reason about the indices of points occurring in the scalar multiplication algorithm than it is to reason about their x-coordinates directly.
So, the required check is equivalent to saying that the following "indexed version" of the above algorithm never asserts:
```ignore
acc := 2
for i from n-1 down to 0 {
p = k_{i+1} ? 1 : −1
assert acc ≠ ± p
assert (acc + p) ≠ acc // X
acc := (acc + p) + acc
assert 0 < acc ≤ (q-1)/2
}
if k_0 = 0 {
assert acc ≠ 1
acc := acc - 1
}
```
The maximum value of `acc` is:
```ignore
<--- n 1s --->
1011111...111111
= 1100000...000000 - 1
```
= $2^{n+1} + 2^n - 1$
> The assertion labelled X obviously cannot fail because $p \neq 0$. It is possible to see that acc is monotonically increasing except in the last conditional. It reaches its largest value when $k$ is maximal, i.e. $2^{n+1} + 2^n - 1$.
So to entirely avoid exceptional cases, we would need $2^{n+1} + 2^n - 1 < (q-1)/2$. But we can use $n$ larger by $c$ if the last $c$ iterations use [complete addition](./addition.md#Complete-addition).
The first $i$ for which the algorithm using **only** incomplete addition fails is going to be $252$, since $2^{252+1} + 2^{252} - 1 > (q - 1)/2$. We need $n = 254$ to make the wraparound technique above work.
```python
sage: q = 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
sage: 2^253 + 2^252 - 1 < (q-1)//2
False
sage: 2^252 + 2^251 - 1 < (q-1)//2
True
```
So the last three iterations of the loop ($i = 2..0$) need to use [complete addition](./addition.md#Complete-addition), as does the conditional subtraction at the end. Writing this out using ⸭ for incomplete addition (as we do in the spec), we have:
```ignore
Acc := [2] T
for i from 253 down to 3 {
P := k_{i+1} ? T : −T
Acc := (Acc ⸭ P) ⸭ Acc
}
for i from 2 down to 0 {
P := k_{i+1} ? T : −T
Acc := (Acc + P) + Acc // complete addition
}
return (k_0 = 0) ? (Acc + (-T)) : Acc // complete addition
```
## Constraint program for optimized double-and-add (incomplete addition)
Define a running sum $\mathbf{z_j} = \sum_{i=j}^{n} (\mathbf{k}_{i} \cdot 2^{i-j})$, where $n = 254$ and:
$$
\begin{aligned}
&\mathbf{z}_{n+1} = 0,\\
&\mathbf{z}_{n} = \mathbf{k}_{n}, \hspace{2em}\text{(most significant bit)}\\
&\mathbf{z}_0 = k.\\
\end{aligned}
$$
$\begin{array}{l}
\text{Initialize } A_{254} = [2] T. \\
\\
\text{for } i \text{ from } 254 \text{ down to } 4: \\
\hspace{1.5em} \BoolCheck{\mathbf{k}_i} = 0 \\
\hspace{1.5em} \mathbf{z}_{i} = 2\mathbf{z}_{i+1} + \mathbf{k}_{i} \\
\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} (\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}, \\
\end{array}$
where $x_{R,i} = (\lambda_{1,i}^2 - x_{A,i} - x_T).$ 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}
\text{Initialize } A_{254} = [2] T. \\
\\
\text{for } i \text{ from } 254 \text{ down to } 4: \\
\hspace{1.5em} \text{// let } \mathbf{k}_{i} = \mathbf{z}_{i} - 2\mathbf{z}_{i+1} \\
\hspace{1.5em} \text{// let } y_{A,i} = \frac{(\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - (\lambda_{1,i}^2 - x_{A,i} - x_T))}{2} \\[2ex]
\hspace{1.5em} \BoolCheck{\mathbf{k}_i} = 0 \\
\hspace{1.5em} \lambda_{1,i} \cdot (x_{A,i} - x_T) = y_{A,i} - (2 \mathbf{k}_i - 1) \cdot y_T \\
\hspace{1.5em} \lambda_{2,i}^2 = x_{A,i-1} + \lambda_{1,i}^2 - x_T \\[1ex]
\hspace{1.5em} \begin{cases}
\lambda_{2,i} \cdot (x_{A,i} - x_{A,i-1}) = y_{A,i} + y_{A, i-1}, &\text{if } i > 4 \\[0.5ex]
\lambda_{2,4} \cdot (x_{A,4} - x_{A,3}) = y_{A,4} + y_{A,3}^\text{witnessed}, &\text{if } i = 4.
\end{cases}
\end{array}$
Here, $y_{A,3}^\text{witnessed}$ is assigned to a cell. This is unlike previous $y_{A,i}$'s, which were implicitly derived from $\lambda_{1,i}, \lambda_{2,i}, x_{A,i}, x_T$, but never actually assigned.
The bits $\mathbf{k}_{3 \dots 1}$ are used in three further steps, using [complete addition](./addition.md#Complete-addition):
$\begin{array}{l}
\text{for } i \text{ from } 3 \text{ down to } 1: \\
\hspace{1.5em} \text{// let } \mathbf{k}_{i} = \mathbf{z}_{i} - 2\mathbf{z}_{i+1} \\[0.5ex]
\hspace{1.5em} \BoolCheck{\mathbf{k}_i} = 0 \\
\hspace{1.5em} (x_{A,i-1}, y_{A,i-1}) = \left((x_{A,i}, y_{A,i}) + (x_T, y_T)\right) + (x_{A,i}, y_{A,i})
\end{array}$
If the least significant bit $\mathbf{k_0} = 1,$ we set $B = \mathcal{O},$ otherwise we set ${B = -T}$. Then we return ${A + B}$ using complete addition.
Let $B = \begin{cases}
(0, 0), &\text{ if } \mathbf{k_0} = 1, \\
(x_T, -y_T), &\text{ otherwise.}
\end{cases}$
Output $(x_{A,0}, y_{A,0}) + B$.
(Note that $(0, 0)$ represents $\mathcal{O}$.)
### 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$.
$$
\begin{array}{|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|}
\hline
x_T & y_T & z^{hi} & x_A^{hi} & \lambda_1^{hi} & \lambda_2^{hi} & q_1^{hi} & q_2^{hi} & q_3^{hi} & z^{lo} & x_A^{lo} & \lambda_1^{lo} & \lambda_2^{lo} & q_1^{lo} & q_2^{lo} & q_3^{lo} \\\hline
& & \mathbf{z}_{255} = 0 & & y_{A,254}=2[T]_y & & 1 & 0 & 0 & \mathbf{z}_{130} & & y_{A,129} & & 1 & 0 & 0 \\\hline
x_T & y_T & \mathbf{z}_{254} & x_{A,254} = 2[T]_x & \lambda_{1,254} & \lambda_{2,254} & 0 & 1 & 0 & \mathbf{z}_{129} & x_{A,129} & \lambda_{1,129} & \lambda_{2,129} & 0 & 1 & 0 \\\hline
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_{A,3} & y_{A,3} & & & & \\\hline
\end{array}
$$
For each $hi$ and $lo$ half, we have three sets of gates. Note that $i$ is going from $255..=3$; $i$ is NOT indexing the rows.
#### $q_1 = 1$
This gate is only used on the first row (before the for loop). We check that $\lambda_1, \lambda_2$ are initialized to values consistent with the initial $y_A.$
$$
\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
\end{array}
$$
where
$$
\begin{aligned}
y_{A,n} &= \frac{(\lambda_{1,n} + \lambda_{2,n}) \cdot (x_{A,n} - (\lambda_{1,n}^2 - x_{A,n} - x_T))}{2},\\
y_{A,n}^\text{witnessed} &\text{ is witnessed.}
\end{aligned}
$$
#### $q_2 = 1$
This gate is used on all rows corresponding to the for loop except the last.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
2 & q_2 \cdot \left(x_{T,cur} - x_{T,next}\right) = 0 \\\hline
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} \cdot (x_{A,i} - x_{A,i-1}) - y_{A,i} - y_{A,i-1}\right) = 0 \\\hline
\end{array}
$$
where
$$
\begin{aligned}
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}
$$
#### $q_3 = 1$
This gate is used on the final iteration of the for loop, handling the special case where we check that the output $y_A$ has been witnessed correctly.
$$
\begin{array}{|c|l|}
\hline
\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} \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}
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}
$$
## 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$).
However, $\mathbf{z}_0 = \alpha + t_q$ *can* overflow $[0, p)$.
Since overflow can only occur in the final step that constrains $\mathbf{z}_0 = 2 \cdot \mathbf{z}_1 + \mathbf{k}_0$, we have $\mathbf{z}_0 = k \pmod{p}$. It is then sufficient to also check that $\mathbf{z}_0 = \alpha + t_q \pmod{p}$ (so that $k = \alpha + t_q \pmod{p}$) and that $k \in [t_q, p + t_q)$. These conditions together imply that $k = \alpha + t_q$ as an integer, and so $2^{254} + k = \alpha \pmod{q}$ as required.
> Note: the bits $\mathbf{k}_{254..0}$ do not represent a value reduced modulo $q$, but rather a representation of the unreduced $\alpha + t_q$.
### Optimized check for $k \in [t_q, p + t_q)$
Since $t_p + t_q < 2^{130}$, we have $$[t_q, p + t_q) = [t_q, t_q + 2^{130}) \;\cup\; [2^{130}, 2^{254}) \;\cup\; \big([2^{254}, 2^{254} + 2^{130}) \;\cap\; [p + t_q - 2^{130}, p + t_q)\big).$$
We may assume that $k = \alpha + t_q \pmod{p}$.
Therefore,
$\begin{array}{rcl}
k \in [t_q, p + t_q) &\Leftrightarrow& \big(k \in [t_q, t_q + 2^{130}) \;\vee\; k \in [2^{130}, 2^{254})\big) \;\vee\; \\
& & \big(k \in [2^{254}, 2^{254} + 2^{130}) \;\wedge\; k \in [p + t_q - 2^{130}, p + t_q)\big) \\
\\
&\Leftrightarrow& \big(\mathbf{k}_{254} = 0 \implies (k \in [t_q, t_q + 2^{130}) \;\vee\; k \in [2^{130}, 2^{254}))\big) \;\wedge \\
& & \big(\mathbf{k}_{254} = 1 \implies (k \in [2^{254}, 2^{254} + 2^{130}) \;\wedge\; k \in [p + t_q - 2^{130}, p + t_q)\big) \\
\\
&\Leftrightarrow& \big(\mathbf{k}_{254} = 0 \implies (\alpha \in [0, 2^{130}) \;\vee\; k \in [2^{130}, 2^{254})\big) \;\wedge \\
& & \big(\mathbf{k}_{254} = 1 \implies (k \in [2^{254}, 2^{254} + 2^{130}) \;\wedge\; (\alpha + 2^{130}) \bmod p \in [0, 2^{130}))\big) \;\;Ⓐ
\end{array}$
> Given $k \in [2^{254}, 2^{254} + 2^{130})$, we prove equivalence of $k \in [p + t_q - 2^{130}, p + t_q)$ and $(\alpha + 2^{130}) \bmod p \in [0, 2^{130})$ as follows:
> * shift the range by $2^{130} - p - t_q$ to give $k + 2^{130} - p - t_q \in [0, 2^{130})$;
> * observe that $k + 2^{130} - p - t_q$ is guaranteed to be in $[2^{130} - t_p - t_q, 2^{131} - t_p - t_q)$ and therefore cannot overflow or underflow modulo $p$;
> * using the fact that $k = \alpha + t_q \pmod{p}$, observe that $(k + 2^{130} - p - t_q) \bmod p = (\alpha + t_q + 2^{130} - p - t_q) \bmod p = (\alpha + 2^{130}) \bmod p$.
>
> (We can see in a different way that this is correct by observing that it checks whether $\alpha \bmod p \in [p - 2^{130}, p)$, so the upper bound is aligned as we would expect.)
Now, we can continue optimizing from $Ⓐ$:
$\begin{array}{rcl}
k \in [t_q, p + t_q) &\Leftrightarrow& \big(\mathbf{k}_{254} = 0 \implies (\alpha \in [0, 2^{130}) \;\vee\; k \in [2^{130}, 2^{254})\big) \;\wedge \\
& & \big(\mathbf{k}_{254} = 1 \implies (k \in [2^{254}, 2^{254} + 2^{130}) \;\wedge\; (\alpha + 2^{130}) \bmod p \in [0, 2^{130}))\big) \\
\\
&\Leftrightarrow& \big(\mathbf{k}_{254} = 0 \implies (\alpha \in [0, 2^{130}) \;\vee\; \mathbf{k}_{253..130} \text{ are not all } 0)\big) \;\wedge \\
& & \big(\mathbf{k}_{254} = 1 \implies (\mathbf{k}_{253..130} \text{ are all } 0 \;\wedge\; (\alpha + 2^{130}) \bmod p \in [0, 2^{130}))\big)
\end{array}$
Constraining $\mathbf{k}_{253..130}$ to be all-$0$ or not-all-$0$ can be implemented almost "for free", as follows.
Recall that $\mathbf{z}_i = \sum_{h=i}^{n} (\mathbf{k}_{h} \cdot 2^{h-i})$, so we have:
$\begin{array}{rcl}
\mathbf{z}_{130} &=& \sum_{h=130}^{254} (\mathbf{k}_h \cdot 2^{h-130}) \\
\mathbf{z}_{130} &=& \mathbf{k}_{254} \cdot 2^{254-130} + \sum_{h=130}^{253} (\mathbf{k}_h \cdot 2^{h-130}) \\
\mathbf{z}_{130} - \mathbf{k}_{254} \cdot 2^{124} &=& \sum_{h=130}^{253} (\mathbf{k}_h \cdot 2^{h-130})
\end{array}$
So $\mathbf{k}_{253..130}$ are all $0$ exactly when $\mathbf{z}_{130} = \mathbf{k}_{254} \cdot 2^{124}$.
Finally, we can merge the $130$-bit decompositions for the $\mathbf{k}_{254} = 0$ and $\mathbf{k}_{254} = 1$ cases by checking that $(\alpha + \mathbf{k}_{254} \cdot 2^{130}) \bmod p \in [0, 2^{130})$.
### Overflow check constraints
Let $s = \alpha + \mathbf{k}_{254} \cdot 2^{130}$. The constraints for the overflow check are:
$$
\begin{aligned}
\mathbf{z}_0 &= \alpha + t_q \pmod{p} \\
\mathbf{k}_{254} = 1 \implies \big(\mathbf{z}_{130} &= 2^{124} \;\wedge\; s \bmod p \in [0, 2^{130})\big) \\
\mathbf{k}_{254} = 0 \implies \big(\mathbf{z}_{130} &\neq 0 \;\vee\; s \bmod p \in [0, 2^{130})\big)
\end{aligned}
$$
Define $\mathsf{inv0}(x) = \begin{cases} 0, &\text{if } x = 0 \\ 1/x, &\text{otherwise.} \end{cases}$
Witness $\eta = \mathsf{inv0}(\mathbf{z}_{130})$, and decompose $s \bmod p$ as $\mathbf{s}_{129..0}$.
Then the needed gates are:
$$
\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
\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.
#### Running sum range check
We make use of a $10$-bit [lookup range check](../decomposition.md#lookup-decomposition) in the circuit to subtract the low $130$ bits of $\mathbf{s}$. The range check subtracts the first $13 \cdot 10$ bits of $\mathbf{s},$ and right-shifts the result to give $(s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}.$

162
book/src/design/circuit/gadgets/sinsemilla.md
View File

@ -1,162 +0,0 @@
# Sinsemilla
## Overview
Sinsemilla is a collision-resistant hash function and commitment scheme designed to be efficient in algebraic circuit models that support [lookups](https://zcash.github.io/halo2/design/proving-system/lookup.html), such as PLONK or Halo 2.
The security properties of Sinsemilla are similar to Pedersen hashes; it is **not** designed to be used where a random oracle, PRF, or preimage-resistant hash is required. **The only claimed security property of the hash function is collision-resistance for fixed-length inputs.**
Sinsemilla is roughly 4 times less efficient than the algebraic hashes Rescue and Poseidon inside a circuit, but around 19 times more efficient than Rescue outside a circuit. Unlike either of these hashes, the collision resistance property of Sinsemilla can be proven based on cryptographic assumptions that have been well-established for at least 20 years. Sinsemilla can also be used as a computationally binding and perfectly hiding commitment scheme.
The general approach is to split the message into $k$-bit pieces, and for each piece, select from a table of $2^k$ bases in our cryptographic group. We combine the selected bases using a double-and-add algorithm. This ends up being provably as secure as a vector Pedersen hash, and makes advantageous use of the lookup facility supported by Halo 2.
## Description
This section is an outline of how Sinsemilla works: for the normative specification, refer to [§5.4.1.9 Sinsemilla Hash Function](https://zips.z.cash/protocol/protocol.pdf#concretesinsemillahash) in the protocol spec. The incomplete point addition operator, ⸭, that we use below is also defined there.
Let $\mathbb{G}$ be a cryptographic group of prime order $q$. We write $\mathbb{G}$ additively, with identity $\mathcal{O}$, and using $[m] P$ for scalar multiplication of $P$ by $m$.
Let $k \geq 1$ be an integer chosen based on efficiency considerations (the table size will be $2^k$). Let $n$ be an integer, fixed for each instantiation, such that messages are $kn$ bits, where $2^n \leq \frac{q-1}{2}$. We use zero-padding to the next multiple of $k$ bits if necessary.
$\textsf{Setup}$: Choose $Q$ and $P[0..2^k - 1]$ as $2^k + 1$ independent, verifiably random generators of $\mathbb{G}$, using a suitable hash into $\mathbb{G}$, such that none of $Q$ or $P[0..2^k - 1]$ are $\mathcal{O}$.
> In Orchard, we define $Q$ to be dependent on a domain separator $D$. The protocol specification uses $\mathcal{Q}(D)$ in place of $Q$ and $\mathcal{S}(m)$ in place of $P[m]$.
$\textsf{Hash}(M)$:
- Split $M$ into $n$ groups of $k$ bits. Interpret each group as a $k$-bit little-endian integer $m_i$.
- let $\mathsf{Acc}_0 := Q$
- for $i$ from $0$ up to $n-1$:
- let $\mathsf{Acc}_{i+1} := (\mathsf{Acc}_i \;⸭\; P[m_{i+1}]) \;⸭\; \mathsf{Acc}_i$
- return $\mathsf{Acc}_n$
Let $\textsf{ShortHash}(M)$ be the $x$-coordinate of $\textsf{Hash}(M)$. (This assumes that $\mathbb{G}$ is a prime-order elliptic curve in short Weierstrass form, as is the case for Pallas and Vesta.)
> It is slightly more efficient to express a double-and-add $[2] A + R$ as $(A + R) + A$. We also use incomplete additions: it is shown in the [Sinsemilla security argument](https://zips.z.cash/protocol/protocol.pdf#sinsemillasecurity) that in the case where $\mathbb{G}$ is a prime-order short Weierstrass elliptic curve, an exceptional case for addition would lead to finding a discrete logarithm, which can be assumed to occur with negligible probability even for adversarial input.
### Use as a commitment scheme
Choose another generator $H$ independently of $Q$ and $P[0..2^k - 1]$.
The randomness $r$ for a commitment is chosen uniformly on $[0, q)$.
Let $\textsf{Commit}_r(M) = \textsf{Hash}(M) \;⸭\; [r] H$.
Let $\textsf{ShortCommit}_r(M)$ be the $x\text{-coordinate}$ of $\textsf{Commit}_r(M)$. (This again assumes that $\mathbb{G}$ is a prime-order elliptic curve in short Weierstrass form.)
Note that unlike a simple Pedersen commitment, this commitment scheme ($\textsf{Commit}$ or $\textsf{ShortCommit}$) is not additively homomorphic.
## 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
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.)
Output: $(x_{A,n},\, y_{A,n})$.
- $(x_{A,0},\, y_{A,0}) = Q$
- for $i$ from $0$ up to $n-1$:
- $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}$
- $2 \cdot y_{A,i} = (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i})$
- $(m_{i+1},\, x_{P,i},\, y_{P,i}) \in \mathcal{P}$
- $\lambda_{2,i}^2 = x_{A,i+1} + x_{R,i} + x_{A,i}$
- $\lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) = y_{A,i} + y_{A,i+1}$
## PLONK / Halo 2 constraints
### Message decomposition
We have an $n$-bit message $m = m_1 + 2^k m_2 + ... + 2^{k\cdot (n-1)} m_n$. (Note that the message words are 1-indexed as in the [protocol spec](https://zips.z.cash/protocol/nu5.pdf#concretesinsemillahash).)
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.
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.
### Generator lookup table
The Sinsemilla circuit makes use of $2^{10}$ pre-computed random generators. These are loaded into a lookup table:
$$
\begin{array}{|c|c|c|}
\hline
table_{idx} & table_x & table_y \\\hline
0 & x_{P[0]} & y_{P[0]} \\\hline
1 & x_{P[1]} & y_{P[1]} \\\hline
2 & x_{P[2]} & y_{P[2]} \\\hline
\vdots & \vdots & \vdots \\\hline
2^{10} - 1 & x_{P[2^{10}-1]} & y_{P[2^{10}-1]} \\\hline
\end{array}
$$
### 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|}
\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
\end{array}
$$
$x_Q$, $z_0$, $z'_0$, etc. would be copied in using equality constraints.
### Optimized Sinsemilla gate
$$
\begin{array}{lrcl}
\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} \\
&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.
- $x_{A,0} = x_Q$
- $2 \cdot y_Q = Y_{A,0}$
- for $i$ from $0$ up to $n-1$:
- $(m_{i+1},\, x_{P,i},\, y_{P,i}) \in \mathcal{P}$
- $\lambda_{2,i}^2 = x_{A,i+1} + x_{R,i} + x_{A,i}$
- $4 \cdot \lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) = 2 \cdot Y_{A,i} + (2 - q_{S3}) \cdot Y_{A,i+1} + 2 q_{S3} \cdot y_{A,n}$
Note that each term of the last constraint is multiplied by $4$ relative to the constraint program given earlier. This is a small optimization that avoids divisions by $2$.
By gating the lookup expression on $q_{S1}$, we avoid the need to fill in unused cells with dummy values to pass the lookup argument. The optimized lookup value (using a default index of $0$) is:
$$
\begin{array}{ll}
(&q_{S1} \cdot m_{i+1}, \\
&q_{S1} \cdot x_{P,i} + (1 - q_{S1}) \cdot x_{P,0}, \\
&q_{S1} \cdot y_{P,i} + (1 - q_{S1}) \cdot y_{P,0} \;\;\;)
\end{array}
$$
This increases the degree of the lookup argument to $6$.
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
4 & q_{S4} \cdot (2 \cdot y_Q - Y_{A,0}) = 0 \\\hline
6 & q_{S1,i} \Rightarrow (m_{i+1},\, x_{P,i},\, y_{P,i}) \in \mathcal{P} \\\hline
3 & q_{S1,i} \cdot \big(\lambda_{2,i}^2 - (x_{A,i+1} + x_{R,i} + x_{A,i})\big) \\\hline
5 & q_{S1,i} \cdot \left(4 \cdot \lambda_{2,i} \cdot (x_{A,i} - x_{A,i+1}) - (2 \cdot Y_{A,i} + (2 - q_{S3,i}) \cdot Y_{A,i+1} + 2 \cdot q_{S3,i} \cdot y_{A,n})\right) = 0 \\\hline
\end{array}
$$

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

@ -1,69 +0,0 @@
# MerkleCRH
## Message decomposition
$\mathsf{SinsemillaHash}$ is used in the [$\mathsf{MerkleCRH^{Orchard}}$ hash function](https://zips.z.cash/protocol/protocol.pdf#orchardmerklecrh). The input to $\mathsf{SinsemillaHash}$ is:
$${l\star} \,||\, {\textsf{left}\star} \,||\, {\textsf{right}\star},$$
where:
- ${l\star} = \textsf{I2LEBSP}_{10}(l) = \textsf{I2LEBSP}_{10}(\textsf{MerkleDepth}^\textsf{Orchard} - 1 - \textsf{layer})$,
- ${\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.
We break these inputs into the following `MessagePiece`s:
$$
\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}
\end{aligned}
$$
$a,b,c$ are constrained by the $\textsf{SinsemillaHash}$ to be $250$ bits, $20$ bits, and $250$ bits respectively.
In a custom gate, we check this message decomposition by enforcing the following constraints:
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}$:
$$
\begin{aligned}
z_{1,a} &= \frac{a - a_0}{2^{10}}\\
&= a_1 \\
\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}.$$
We also recover the subpiece $b_0$ using $(b, z_{1,b})$:
$$
\begin{aligned}
z_{1,b} &= \frac{b - b_{0..=10}}{2^{10}}\\
\implies b_0 &= b - (z_{1,b} \cdot 2^{10}).
\end{aligned}
$$
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:
3. $\mathsf{left} = a_1 + 2^{240} \cdot b_0 + 2^{254} \cdot b_1$
4. $\mathsf{right} = b_2 + 2^5 \cdot c$
## 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.

0
book/src/design/circuit/gadgets/sinsemilla/note-commit.md → book/src/design/circuit/note-commit.md
View File