mirror of https://github.com/zcash/orchard.git
[book] Details and formatting changes.
Co-authored-by: Daira Hopwood <daira@jacaranda.org>
This commit is contained in:
therealyingtong
parent
2febafbdfe
commit
d9f134ac4b
|
|
@ -30,6 +30,7 @@ which is equivalent to
|
|||
|
||||
Assuming $x_p \neq x_q$,
|
||||
|
||||
$
|
||||
\begin{array}{|rrll|}
|
||||
\hline
|
||||
&(x_r + x_q + x_p) \cdot (x_p - x_q)^2 &=& \lambda^2 \cdot (x_p - x_q)^2\\
|
||||
|
|
@ -40,6 +41,7 @@ Assuming $x_p \neq x_q$,
|
|||
\implies &(y_r + y_q) \cdot (x_p - x_q) &=& \lambda \cdot (x_p - x_q) \cdot (x_q - x_r)\\
|
||||
\hline
|
||||
\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$
|
||||
|
|
@ -130,7 +132,8 @@ $$
|
|||
&& \text{If } (x_q - x_p) \cdot \lambda - (y_q - y_p) = 0, \text{ then because } x_q - x_p \neq 0, \\
|
||||
&& \text{ by rearranging both sides we get } \lambda = (y_q - y_p) / (x_q - x_p) \\
|
||||
&& \\
|
||||
&& \text{and therefore } :: x_q \neq x_p \implies \lambda = (y_q - y_p) / (x_q - x_p).\\
|
||||
&& \text{and 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}
|
||||
|
|
@ -144,9 +147,10 @@ $$
|
|||
&& \\
|
||||
&& \text{If } y_p = 0 \text{ then } x_p = 0, \text{ and the constraint is satisfied.}\\
|
||||
&& \\
|
||||
&& \text{If } y_p \neq 0 \text{ then by rearranging both sides we get }\\
|
||||
&& \text{If } y_p \neq 0 \text{ by rearranging both sides we get }\\
|
||||
&& \lambda = 3x_p^2 / 2y_p \\
|
||||
&& \text{Therefore } :: (x_q = x_p) \wedge y_p \neq 0 \implies \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 \\
|
||||
|
|
@ -173,9 +177,9 @@ $$
|
|||
&\text{• Similarly, constraint (d) imposes that } y_r = \lambda \cdot (x_p - x_r) - y_p \text{ is satisfied.} \\
|
||||
\end{aligned} \\
|
||||
&& \\
|
||||
&& \text{Therefore} \\
|
||||
&& \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)) \\
|
||||
&(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} \\
|
||||
&& \\
|
||||
|
|
@ -193,7 +197,8 @@ $$
|
|||
&& \\
|
||||
&& \text{Similarly, constraint (b) imposes that } y_r - y_q = 0. \\
|
||||
&& \\
|
||||
&& \text{Therefore } :: x_p = 0 => (x_r, y_r) = (x_q, y_q). \\
|
||||
&& \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 \\
|
||||
|
|
@ -210,7 +215,8 @@ $$
|
|||
&& \\
|
||||
&& \text{Similarly, constraint (b) imposes that } y_r - y_p = 0. \\
|
||||
&& \\
|
||||
&& \text{Therefore } :: x_q = 0 \implies (x_r, y_r) = (x_p, y_p). \\
|
||||
&& \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 \\
|
||||
|
|
@ -225,7 +231,7 @@ $$
|
|||
&& \text{If } x_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. \\
|
||||
&& \text{Therefore } : x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0).
|
||||
&& \text{Therefore: } x_q = x_p \wedge y_q = -y_p \implies (x_r, y_r) = (0, 0).
|
||||
\end{array}
|
||||
$$
|
||||
|
||||
|
|
@ -337,7 +343,7 @@ $(x_p, y_p) + (x_q, y_q) = (x_r, y_r)$
|
|||
\end{array}
|
||||
$
|
||||
|
||||
- Soundness: (x_r, y_r) = (0, 0) is the only solution
|
||||
- Soundness: $(x_r, y_r) = (0, 0)$ is the only solution
|
||||
|
||||
* $(\zeta x, y) + (x, y)$
|
||||
|
||||
|
|
|
|||
|
|
@ -131,15 +131,15 @@ We support using a base field element as the scalar in fixed-base multiplication
|
|||
This is used in
|
||||
$\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 using a running sum $z$, where $z_{i+1} = (z_i - a_i) / (2^3)$ for $$\alpha = a_0 + (2^3) a_1 + ... + (2^{3(84)}) a_{84}.$$ (This running sum $z$ is not to be confused with the $Z$ array used to check the $y$-coordinate of a fixed-base window.)
|
||||
Decompose the base field element $\alpha$ into three-bit windows using a running sum $z$, where $z_{i+1} = (z_i - a_i) / 2^3$ for $$\alpha = a_0 + 2^3 a_1 + ... + 2^{3 \cdot 84} a_{84}.$$ (This running sum $z$ is not to be confused with the $Z$ array used to check the $y$-coordinate of a fixed-base window.)
|
||||
|
||||
We set $z_0 = \alpha$, which means:
|
||||
$$
|
||||
\begin{aligned}
|
||||
z_1 &= (\alpha - k_0) / 2^3, \text{ (subtract the lowest 3 bits)}\\
|
||||
&= k_1 + (2^3) k_2 + ... + 2^{3(83)} k_{84},\\
|
||||
&= k_1 + 2^3 k_2 + ... + 2^{3 \cdot 83} k_{84},\\
|
||||
z_2 &= (z_1 - k_1) / 2^3\\
|
||||
&= k_2 + (2^3) k_3 + ... + 2^{3(82)} k_{84},\\
|
||||
&= k_2 + 2^3 k_3 + ... + 2^{3 \cdot 82} k_{84},\\
|
||||
&\cdots,\\
|
||||
z_{84} &= k_{84}\\
|
||||
z_{85} &= (z_{84} - k_{84}) / 2^3\\
|
||||
|
|
@ -147,27 +147,27 @@ z_{85} &= (z_{84} - k_{84}) / 2^3\\
|
|||
\end{aligned}
|
||||
$$
|
||||
|
||||
Since we don't directly witness the three-bit values, we must range-constrain the difference at each step of the running sum. We also constrain the final output of the running sum to be $0$.
|
||||
We must range-constrain the difference at each step of the running sum. We also constrain the final output of the running sum to be $0$.
|
||||
$$
|
||||
\begin{array}{|c|l|}
|
||||
\hline
|
||||
\text{Degree} & \text{Constraint} \\\hline
|
||||
9 & q_\text{decompose-base-field} \cdot \texttt{range\_check}(z_i - z_{i+1} \cdot (2^3), 8) = 0 \\\hline
|
||||
9 & q_\text{decompose-base-field} \cdot \texttt{range\_check}(z_i - z_{i+1} \cdot 2^3, 2^3) = 0 \\\hline
|
||||
2 & q_\text{decompose-base-field} \cdot z_{85} = 0 \\\hline
|
||||
\end{array}
|
||||
$$
|
||||
|
||||
We also enforce canonicity of this decomposition. That is, we want to 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) }.$$
|
||||
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 \texttt{range\_check}(\alpha_1, 4) = 0 \\\hline
|
||||
3 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_2, 2) = 0 \\\hline
|
||||
5 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\alpha_1, 2^2) = 0 \\\hline
|
||||
3 & q_\text{canon-base-field} \cdot \texttt{range\_check}(\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}
|
||||
$$
|
||||
|
|
@ -178,7 +178,7 @@ If the MSB $\alpha_2 = 0$ is not set, then $\alpha < 2^{254} < p.$ However, in t
|
|||
- $\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:
|
||||
- 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}\\
|
||||
|
|
@ -186,16 +186,31 @@ z_{44} &= k_{44} + 2^3 k_{45} + \cdots + 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} - 2^3 \cdot z_{44}.$
|
||||
- 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.$
|
||||
|
||||
To check that $0 \leq \alpha_0 + 2^{130} - t_p < 2^{130},$ we use 13 ten-bit [lookups](../lookup_range_check.md), where we constrain the $z_{13}$ running sum output of the lookup to be $0$ if $\alpha_2 = 1.$
|
||||
Define $\alpha'_0 = \alpha_0 + 2^{130} - t_p$. To check that $0 \leq \alpha'_0 < 2^{130},$ we use 13 ten-bit [lookups](../lookup_range_check.md), 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} - t_p < 2^{130}\\\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}
|
||||
$$
|
||||
|
||||
## 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.
|
||||
|
|
|
|||
|
|
@ -102,19 +102,17 @@ $$
|
|||
Initialize $A_{254} = [2] T.$
|
||||
|
||||
for $i$ from $254$ down to $4$:
|
||||
$$
|
||||
\begin{aligned}
|
||||
&(\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\
|
||||
&\mathbf{z}_{i} = 2\mathbf{z}_{i+1} + \mathbf{k}_{i}\\
|
||||
& x_{P,i} = x_T\\
|
||||
& y_{P,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)}\\
|
||||
& \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) = y_{A,i} - y_{P,i}\\
|
||||
& \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{P,i}\\
|
||||
& (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) = 2 y_{\mathsf{A},i}\\
|
||||
& \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},\\
|
||||
\end{aligned}
|
||||
$$
|
||||
$\begin{array}{ll}
|
||||
\hspace{2em}& (\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\
|
||||
\hspace{2em}& \mathbf{z}_{i} = 2\mathbf{z}_{i+1} + \mathbf{k}_{i}\\
|
||||
\hspace{2em}& x_{P,i} = x_T\\
|
||||
\hspace{2em}& y_{P,i} = (2 \mathbf{k}_i - 1) \cdot y_T \hspace{2em}\text{(conditionally negate)}\\
|
||||
\hspace{2em}& \lambda_{1,i} \cdot (x_{A,i} - x_{P,i}) = y_{A,i} - y_{P,i}\\
|
||||
\hspace{2em}& \lambda_{1,i}^2 = x_{R,i} + x_{A,i} + x_{P,i}\\
|
||||
\hspace{2em}& (\lambda_{1,i} + \lambda_{2,i}) \cdot (x_{A,i} - x_{R,i}) = 2 y_{\mathsf{A},i}\\
|
||||
\hspace{2em}& \lambda_{2,i}^2 = x_{A,i-1} + x_{R,i} + x_{A,i}\\
|
||||
\hspace{2em}& \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).$ After substitution of $x_{P,i}, y_{P,i}, x_{R,i}, y_{A,i}$, and $y_{A,i-1}$, this becomes:
|
||||
|
||||
|
|
@ -138,18 +136,33 @@ $$
|
|||
\lambda_{2,4} \cdot (x_{A,4} - x_{A,3}) = y_{A,4} + y_{A,3}^\text{witnessed}, &\text{if } i = 4.
|
||||
\end{cases}
|
||||
$$
|
||||
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 double-and-add using [complete addition](./addition.md#Complete-addition).
|
||||
The bits $\mathbf{k}_{3 \dots 1}$ are used in three further steps, using [complete addition](./addition.md#Complete-addition):
|
||||
|
||||
for $i$ from $3$ down to $1$:
|
||||
$\begin{array}{ll}
|
||||
\hspace{2em}& \texttt{// let } \mathbf{k}_{i} = \mathbf{z}_{i} - 2\mathbf{z}_{i+1}\\
|
||||
\hspace{2em}& (\mathbf{k}_i)(\mathbf{k}_i-1) = 0\\
|
||||
\hspace{2em}& (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 is set $\mathbf{k_0} = 1,$ we return the accumulator $A$. Else, if $\mathbf{k_0} = 0,$ we return $A - T$ (also using complete addition).
|
||||
|
||||
Output $(x_{A,0}, y_{A,0})$
|
||||
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$.
|
||||
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|}
|
||||
|
|
|
|||
Loading…
Reference in New Issue