diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b1702c60f7..c6cd03bdc7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -8,12 +8,10 @@ jobs:
runs-on: ${{ matrix.os }}
strategy:
matrix:
- # We don't need to test across multiple platforms yet
- # os: [ubuntu-latest, windows-latest, macOS-latest]
- os: [ubuntu-latest]
+ os: [ubuntu-latest, windows-latest, macOS-latest]
steps:
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
- uses: actions-rs/toolchain@v1
with:
override: false
@@ -33,7 +31,7 @@ jobs:
- wasm32-wasi
steps:
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
- uses: actions-rs/toolchain@v1
with:
override: false
@@ -50,7 +48,7 @@ jobs:
runs-on: ubuntu-latest
steps:
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
- uses: actions-rs/toolchain@v1
with:
override: false
@@ -66,7 +64,7 @@ jobs:
runs-on: ubuntu-latest
steps:
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
# Use stable for this to ensure that cargo-tarpaulin can be built.
- uses: actions-rs/toolchain@v1
with:
@@ -82,16 +80,14 @@ jobs:
command: tarpaulin
args: --all-features --timeout 600 --out Xml
- name: Upload coverage to Codecov
- uses: codecov/codecov-action@v1
- with:
- token: ${{secrets.CODECOV_TOKEN}}
+ uses: codecov/codecov-action@v3.1.0
doc-links:
name: Intra-doc links
runs-on: ubuntu-latest
steps:
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
- uses: actions-rs/toolchain@v1
with:
override: false
@@ -113,7 +109,7 @@ jobs:
timeout-minutes: 30
runs-on: ubuntu-latest
steps:
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
- uses: actions-rs/toolchain@v1
with:
override: false
diff --git a/.github/workflows/lints-stable.yml b/.github/workflows/lints-stable.yml
index ffeb79375f..7666dae1df 100644
--- a/.github/workflows/lints-stable.yml
+++ b/.github/workflows/lints-stable.yml
@@ -5,12 +5,12 @@ on: pull_request
jobs:
clippy:
- name: Clippy (1.51.0)
+ name: Clippy (1.56.1)
timeout-minutes: 30
runs-on: ubuntu-latest
steps:
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
- uses: actions-rs/toolchain@v1
with:
components: clippy
@@ -18,6 +18,6 @@ jobs:
- name: Run clippy
uses: actions-rs/clippy-check@v1
with:
- name: Clippy (1.51.0)
+ name: Clippy (1.56.1)
token: ${{ secrets.GITHUB_TOKEN }}
args: --all-features --all-targets -- -D warnings
diff --git a/.gitignore b/.gitignore
index 1bd93e286e..f2af733bf1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,3 +3,4 @@
Cargo.lock
.vscode
**/*.html
+.DS_Store
diff --git a/COPYING b/COPYING
deleted file mode 100644
index 6bec3985f5..0000000000
--- a/COPYING
+++ /dev/null
@@ -1,35 +0,0 @@
-Copyright 2020-2021 The Electric Coin Company
-
-This package ("Original Work") is licensed under the terms of the Bootstrap Open
-Source License, version 1.0, or at your option, any later version ("BOSL"). See
-the file ./LICENSE-BOSL for the terms of the Bootstrap Open Source Licence,
-version 1.0.
-
-Only if this Original Work is included as part of the distribution of one of the
-following projects ("the Project"):
-
-- The Zcash projects published by the Electric Coin Company,
-- The Zebra project published by the Zcash Foundation,
-
-then License is granted to use this package under the BOSL as modified by the
-following clarification and special exception. This exception applies only to
-the Original Work when linked or combined with the Project and not to the
-Original Work when linked, combined, or included in or with any other software
-or project or on a standalone basis.
-
- Under the terms of the BOSL, linking or combining this Original Work with
- the Project creates a Derivative Work based upon the Original Work and the
- terms of the BOSL thus apply to both the Original Work and that Derivative
- Work. As a special exception to the BOSL, and to allow this Original Work to
- be linked and combined with the Project without having to apply the BOSL to
- the other portions of the Project, you are granted permission to link or
- combine this Original Work with the Project and to copy and distribute the
- resulting work ("Resulting Work") under the open source license applicable
- to the Project ("Project License"), provided that any portions of this
- Original Work included in the Resulting Work remain subject to the BOSL. For
- clarity, you may continue to treat all other portions of the Project under
- the Project License, provided that you comply with the BOSL with respect to
- the Original Work. If you modify this Original Work, your version of the
- Original Work must remain under the BOSL. You may also extend this exception
- to your version, but you are not obligated to do so. If you do not wish to
- do so, delete this exception statement from your version.
diff --git a/COPYING.md b/COPYING.md
new file mode 100644
index 0000000000..4f1b0b77b4
--- /dev/null
+++ b/COPYING.md
@@ -0,0 +1,16 @@
+# License
+
+Licensed under either of
+
+ * Apache License, Version 2.0, ([LICENSE-APACHE](LICENSE-APACHE) or http://www.apache.org/licenses/LICENSE-2.0)
+ * MIT license ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT)
+
+at your option.
+
+# Contribution
+
+Unless you explicitly state otherwise, any contribution intentionally
+submitted for inclusion in the work by you, as defined in the Apache-2.0
+license, shall be dual licensed as above, without any additional terms or
+conditions.
+
diff --git a/README.md b/README.md
index 5fe417bca3..69167e0716 100644
--- a/README.md
+++ b/README.md
@@ -1,12 +1,10 @@
# halo2 [](https://crates.io/crates/halo2) #
-**IMPORTANT**: This library is in beta, and should not be used in production software.
-
## [Documentation](https://docs.rs/halo2)
## Minimum Supported Rust Version
-Requires Rust **1.51** or higher.
+Requires Rust **1.56.1** or higher.
Minimum supported Rust version can be changed in the future, but it will be done with a
minor version bump.
@@ -18,14 +16,17 @@ The `RAYON_NUM_THREADS` environment variable can be used to set the number of th
## License
-Copyright 2020-2021 The Electric Coin Company.
+Licensed under either of
+
+ * Apache License, Version 2.0, ([LICENSE-APACHE](LICENSE-APACHE) or
+ http://www.apache.org/licenses/LICENSE-2.0)
+ * MIT license ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT)
+
+at your option.
-You may use this package under the Bootstrap Open Source Licence, version 1.0,
-or at your option, any later version. See the file [`COPYING`](COPYING) for
-more details, and [`LICENSE-BOSL`](LICENSE-BOSL) for the terms of the Bootstrap
-Open Source Licence, version 1.0.
+### Contribution
-The purpose of the BOSL is to allow commercial improvements to the package
-while ensuring that all improvements are open source. See
-[here](https://electriccoin.co/blog/introducing-tgppl-a-radically-new-type-of-open-source-license/)
-for why the BOSL exists.
+Unless you explicitly state otherwise, any contribution intentionally
+submitted for inclusion in the work by you, as defined in the Apache-2.0
+license, shall be dual licensed as above, without any additional terms or
+conditions.
diff --git a/book/macros.txt b/book/macros.txt
index 6ec36ee757..22eab46299 100644
--- a/book/macros.txt
+++ b/book/macros.txt
@@ -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})}
@@ -51,7 +52,7 @@
\bottom:{\perp}
\alg:{#1_\textnormal{alg}}
\zero:{\mathcal{O}}
-\dlrel:{\mathsf{dl-rel}}
+\dlrel:{\textsf{dl-rel}}
\game:{\mathsf{G}}
\innerprod:{\langle{#1},{#2}\rangle}
\dlgame:{\mathsf{G}^\dlrel_{\group,n}}
@@ -61,4 +62,15 @@
\halo:{\textsf{Halo}}
\lo:{\textnormal{lo}}
\hi:{\textnormal{hi}}
-\protocol:{\halo}
\ No newline at end of file
+\protocol:{\halo}
+\extractwitness:{\textnormal{ExtractWitness}}
+\pfail:{p_\textnormal{fail}}
+\repr:\{\kern-0.1em {#1} \kern-0.1em\}^{#2}
+\rep:{\repr{#1}{}}
+\repv:{\repr{#1}{\mathbf{#2}}_{#3}}
+\dlreladv:{\mathcal{H}}
+\mr:{\mathcal{M}^{#1}_{#2}({#3})}
+\mv:{\mr{\mathbf{#1}}{#2}{#3}}
+\m:{\mr{#1}{}{#2}}
+\z:{\mathcal{Z}_{#1}({#2}, {#3})}
+\trprefix:{{#1}|_{#2}}
diff --git a/book/src/IDENTIFIERS.json b/book/src/IDENTIFIERS.json
new file mode 100644
index 0000000000..2508a78a0f
--- /dev/null
+++ b/book/src/IDENTIFIERS.json
@@ -0,0 +1,25 @@
+{
+ "decompose-combined-lookup": "design/gadgets/decomposition.html#combined-lookup-expression",
+ "decompose-short-lookup": "design/gadgets/decomposition.html#short-range-check",
+ "decompose-short-range": "design/gadgets/decomposition.html#short-range-decomposition",
+ "ecc-complete-addition": "design/gadgets/ecc/addition.html#complete-addition-constraints",
+ "ecc-incomplete-addition": "design/gadgets/ecc/addition.html#incomplete-addition-constraints",
+ "ecc-fixed-mul-base-canonicity": "design/gadgets/ecc/fixed-base-scalar-mul.html#base-field-element",
+ "ecc-fixed-mul-coordinates": "design/gadgets/ecc/fixed-base-scalar-mul.html#constrain-coordinates",
+ "ecc-fixed-mul-full-word": "design/gadgets/ecc/fixed-base-scalar-mul.html#full-width-scalar",
+ "ecc-fixed-mul-load-base": "design/gadgets/ecc/fixed-base-scalar-mul.html#load-fixed-base",
+ "ecc-fixed-mul-short-msb": "design/gadgets/ecc/fixed-base-scalar-mul.html#constrain-short-signed-msb",
+ "ecc-fixed-mul-short-conditional-neg": "design/gadgets/ecc/fixed-base-scalar-mul.html#constrain-short-signed-conditional-neg",
+ "ecc-var-mul-complete-gate": "design/gadgets/ecc/var-base-scalar-mul.html#complete-gate",
+ "ecc-var-mul-incomplete-first-row": "design/gadgets/ecc/var-base-scalar-mul.html#incomplete-first-row-gate",
+ "ecc-var-mul-incomplete-last-row": "design/gadgets/ecc/var-base-scalar-mul.html#incomplete-last-row-gate",
+ "ecc-var-mul-incomplete-main-loop": "design/gadgets/ecc/var-base-scalar-mul.html#incomplete-main-loop-gate",
+ "ecc-var-mul-lsb-gate": "design/gadgets/ecc/var-base-scalar-mul.html#lsb-gate",
+ "ecc-var-mul-overflow": "design/gadgets/ecc/var-base-scalar-mul.html#overflow-check-constraints",
+ "ecc-var-mul-witness-scalar": "design/gadgets/ecc/var-base-scalar-mul.html#witness-scalar",
+ "ecc-witness-point": "design/gadgets/ecc/witnessing-points.html#points-including-the-identity",
+ "ecc-witness-non-identity-point": "design/gadgets/ecc/witnessing-points.html#non-identity-points",
+ "sinsemilla-constraints": "design/gadgets/sinsemilla.html#optimized-sinsemilla-gate",
+ "sinsemilla-merkle-crh-bit-lengths": "design/gadgets/sinsemilla/merkle-crh.html#bit-length-constraints",
+ "sinsemilla-merkle-crh-decomposition": "design/gadgets/sinsemilla/merkle-crh.html#decomposition-constraints"
+}
\ No newline at end of file
diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index ed1b2b262c..259af2f141 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -25,8 +25,10 @@
- [Implementation](design/implementation.md)
- [Proofs](design/implementation/proofs.md)
- [Fields](design/implementation/fields.md)
+ - [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)
diff --git a/book/src/background/curves.md b/book/src/background/curves.md
index 36f3e409d2..2600127ddf 100644
--- a/book/src/background/curves.md
+++ b/book/src/background/curves.md
@@ -155,10 +155,10 @@ when adding two distinct points.
### Point addition
We now add two points with distinct $x$-coordinates, $P = (x_0, y_0)$ and $Q = (x_1, y_1),$
where $x_0 \neq x_1,$ to obtain $R = P + Q = (x_2, y_2).$ The line $\overline{PQ}$ has slope
-$$\lambda = frac{y_1 - y_0}{x_1 - x_0} \implies y - y_0 = \lambda \cdot (x - x_0).$$
+$$\lambda = \frac{y_1 - y_0}{x_1 - x_0} \implies y - y_0 = \lambda \cdot (x - x_0).$$
Using the expression for $\overline{PQ}$, we compute $y$-coordinate $-y_2$ of $-R$ as:
-$$-y_2 - y_0 = \lambda \cdot (x_2 - x_0) \implies \boxed{y_2 = (x_0 - x_2) - y_0}.$$
+$$-y_2 - y_0 = \lambda \cdot (x_2 - x_0) \implies \boxed{y_2 =\lambda (x_0 - x_2) - y_0}.$$
Plugging the expression for $\overline{PQ}$ into the curve equation $y^2 = x^3 + b$ yields
$$
@@ -193,7 +193,7 @@ Important notes:
Imagine that $\mathbb{F}_p$ has a primitive cube root of unity, or in other words that
$3 | p - 1$ and so an element $\zeta_p$ generates a $3$-order multiplicative subgroup.
Notice that a point $(x, y)$ on our example elliptic curve $y^2 = x^3 + b$ has two cousin
-points: $(\zeta_p x, \zeta_p^2 x)$, because the computation $x^3$ effectively kills the
+points: $(\zeta_p x,y), (\zeta_p^2 x,y)$, because the computation $x^3$ effectively kills the
$\zeta$ component of the $x$-coordinate. Applying the map $(x, y) \mapsto (\zeta_p x, y)$
is an application of an endomorphism over the curve. The exact mechanics involved are
complicated, but when the curve has a prime $q$ number of points (and thus a prime
diff --git a/book/src/background/fields.md b/book/src/background/fields.md
index fa03e36871..325637010a 100644
--- a/book/src/background/fields.md
+++ b/book/src/background/fields.md
@@ -248,7 +248,7 @@ odd, and so half of all elements are squares.
In order to compute the square root, we can first raise the element
$a = \alpha^i \cdot \beta^j$ to the power $t$ to "kill" the $t$-order component, giving
-$$a^t = \alpha^{it \pmod 2^k} \cdot \beta^{jt \pmod t} = \alpha^{it \pmod 2^k}$$
+$$a^t = \alpha^{it \pmod {2^k}} \cdot \beta^{jt \pmod t} = \alpha^{it \pmod {2^k}}$$
and then raise this result to the power $t^{-1} \pmod{2^k}$ to undo the effect of the
original exponentiation on the $2^k$-order component:
diff --git a/book/src/background/groups.md b/book/src/background/groups.md
index 12b622bfdc..da8cbc385e 100644
--- a/book/src/background/groups.md
+++ b/book/src/background/groups.md
@@ -36,14 +36,14 @@ Assuming the discrete log assumption holds, Pedersen commitments are also perfec
and computationally binding:
* **hiding**: the adversary chooses messages $m_0, m_1.$ The committer commits to one of
- these messages $c = \text{Commit}(m_b;r), b \in \{0,1\}.$ Given $c,$ the probability of
+ these messages $c = \text{Commit}(m_b,r), b \in \{0,1\}.$ Given $c,$ the probability of
the adversary guessing the correct $b$ is no more than $\frac{1}{2}$.
* **binding**: the adversary cannot pick two different messages $m_0 \neq m_1,$ and
randomness $r_0, r_1,$ such that $\text{Commit}(m_0,r_0) = \text{Commit}(m_1,r_1).$
### Vector Pedersen commitment
We can use a variant of the Pedersen commitment scheme to commit to multiple messages at
-once, $\mathbf{m} = (m_1, \cdots, m_n)$. This time, we'll have to sample a corresponding
+once, $\mathbf{m} = (m_0, \cdots, m_{n-1})$. This time, we'll have to sample a corresponding
number of random public generators $\mathbf{G} = (G_0, \cdots, G_{n-1}),$ along with a
single random generator $H$ as before (for use in hiding). Then, our commitment scheme is:
@@ -57,10 +57,10 @@ $$
> TODO: is this positionally binding?
-## Diffie--Hellman
+## Diffie–Hellman
-An example of a protocol that uses cryptographic groups is Diffie--Hellman key agreement
-[[DH1976]]. The Diffie--Hellman protocol is a method for two users, Alice and Bob, to
+An example of a protocol that uses cryptographic groups is Diffie–Hellman key agreement
+[[DH1976]]. The Diffie–Hellman protocol is a method for two users, Alice and Bob, to
generate a shared private key. It proceeds as follows:
1. Alice and Bob publicly agree on two prime numbers, $p$ and $G,$ where $p$ is large and
@@ -83,7 +83,7 @@ $g, p, A = [a]G,$ and $B = [b]G$: in other words, they would need to either get
discrete logarithm $a$ from $A = [a]G$ or $b$ from $B = [b]G,$ which we assume to be
computationally infeasible in $\mathbb{F}_p^\times.$
-More generally, protocols that use similar ideas to Diffie--Hellman are used throughout
+More generally, protocols that use similar ideas to Diffie–Hellman are used throughout
cryptography. One way of instantiating a cryptographic group is as an
[elliptic curve](curves.md). Before we go into detail on elliptic curves, we'll describe
some algorithms that can be used for any group.
diff --git a/book/src/background/pc-ipa.md b/book/src/background/pc-ipa.md
index 323c3fce95..63410c8ddb 100644
--- a/book/src/background/pc-ipa.md
+++ b/book/src/background/pc-ipa.md
@@ -53,7 +53,7 @@ $\mathbf{b}^{(k)} := \mathbf{b}.$ In each round $j = k, k-1, \cdots, 1$:
$$
\begin{aligned}
L_j &= \langle\mathbf{a_{lo}^{(j)}}, \mathbf{G_{hi}^{(j)}}\rangle + [l_j]H + [\langle\mathbf{a_{lo}^{(j)}}, \mathbf{b_{hi}^{(j)}}\rangle] U\\
-R_j &= \langle\mathbf{a_{hi}^{(j)}}, \mathbf{G_{lo}^{(j)}}\rangle + [l_j]H + [\langle\mathbf{a_{hi}^{(j)}}, \mathbf{b_{lo}^{(j)}}\rangle] U\\
+R_j &= \langle\mathbf{a_{hi}^{(j)}}, \mathbf{G_{lo}^{(j)}}\rangle + [r_j]H + [\langle\mathbf{a_{hi}^{(j)}}, \mathbf{b_{lo}^{(j)}}\rangle] U\\
\end{aligned}
$$
diff --git a/book/src/background/polynomials.md b/book/src/background/polynomials.md
index 6ed4a0c16f..7846233724 100644
--- a/book/src/background/polynomials.md
+++ b/book/src/background/polynomials.md
@@ -178,7 +178,7 @@ most points." Formally, it can be written as follows:
> Let $p(x_1, x_2, \cdots, x_n)$ be a nonzero polynomial of $n$ variables with degree $d$.
> Let $S$ be a finite set of numbers with at least $d$ elements in it. If we choose random
-> $\alpha_1, \alpha_1, \cdots, \alpha_n$ from $S$,
+> $\alpha_1, \alpha_2, \cdots, \alpha_n$ from $S$,
> $$\text{Pr}[p(\alpha_1, \alpha_2, \cdots, \alpha_n) = 0] \leq \frac{d}{|S|}.$$
In the familiar univariate case $p(X)$, this reduces to saying that a nonzero polynomial
@@ -279,7 +279,7 @@ we can reconstruct its coefficient form in the Lagrange basis:
$$A(X) = \sum_{i = 0}^{n-1} A(x_i)\mathcal{L_i}(X), $$
-where $X \in \{x_0, x_1,\cdots, x_{1-n}\}.$
+where $X \in \{x_0, x_1,\cdots, x_{n-1}\}.$
## References
[^master-thm]: [Dasgupta, S., Papadimitriou, C. H., & Vazirani, U. V. (2008). "Algorithms" (ch. 2). New York: McGraw-Hill Higher Education.](https://people.eecs.berkeley.edu/~vazirani/algorithms/chap2.pdf)
diff --git a/book/src/background/recursion.md b/book/src/background/recursion.md
index 30bf19fbf0..4b6ce7430f 100644
--- a/book/src/background/recursion.md
+++ b/book/src/background/recursion.md
@@ -14,7 +14,7 @@ polynomial with degree $2^k - 1.$
| | |
| -------- | -------- |
-|
+
+$$
+\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
@@ -95,10 +99,10 @@ $\hspace{1em}
\end{array}
$
-### Constraints
+### 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]
@@ -199,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 \\
@@ -227,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. \\
& \\
diff --git a/book/src/design/gadgets/ecc/fixed-base-scalar-mul.md b/book/src/design/gadgets/ecc/fixed-base-scalar-mul.md
index 244a955c1b..dbeece496d 100644
--- a/book/src/design/gadgets/ecc/fixed-base-scalar-mul.md
+++ b/book/src/design/gadgets/ecc/fixed-base-scalar-mul.md
@@ -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}
$$
@@ -97,13 +91,13 @@ $\mathsf{v^{old}}$ and $\mathsf{v^{new}}$ are each already constrained to $64$ b
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:
+
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
+4 & q_1 \cdot \left(y_{A,n}^\text{witnessed} - y_{A,n}\right) = 0 \\\hline
\end{array}
$$
where
@@ -194,7 +194,7 @@ y_{A,n}^\text{witnessed} &\text{ is witnessed.}
\end{aligned}
$$
-#### $q_2 = 1$
+### $q_2 = 1$
This gate is used on all rows corresponding to the for loop except the last.
$$
@@ -205,19 +205,20 @@ $$
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}
$$
-#### $q_3 = 1$
+### $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|}
@@ -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
+
+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
+
+$$
+\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.
diff --git a/book/src/design/gadgets/ecc/witnessing-points.md b/book/src/design/gadgets/ecc/witnessing-points.md
new file mode 100644
index 0000000000..1159f37d16
--- /dev/null
+++ b/book/src/design/gadgets/ecc/witnessing-points.md
@@ -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}
+$$
diff --git a/book/src/design/gadgets/sha256/table16.md b/book/src/design/gadgets/sha256/table16.md
index d9b241e42c..00c1ad6692 100644
--- a/book/src/design/gadgets/sha256/table16.md
+++ b/book/src/design/gadgets/sha256/table16.md
@@ -488,7 +488,7 @@ Output: $\Sigma_1(E) = R^{even} = R_0^{even} + 2^{16} R_1^{even}$
### σ_0 gate
#### v1
-v1 of the $\sigma_0$ gate takes in a word that's split into $(3, 4, 11, 14)$-bit chunks (already constrained by message scheduling). We refer to these chunks respectively as $(a(3), b(4), c(11), d(14)).$ $b(4$ is further split into two 2-bit chunks $b(4)^{lo},b(4)^{hi}.$ We witness the spread versions of the small chunks. We already have $\texttt{spread}(c(11))$ and $\texttt{spread}(d(14))$ from the message scheduling.
+v1 of the $\sigma_0$ gate takes in a word that's split into $(3, 4, 11, 14)$-bit chunks (already constrained by message scheduling). We refer to these chunks respectively as $(a(3), b(4), c(11), d(14)).$ $b(4)$ is further split into two 2-bit chunks $b(4)^{lo},b(4)^{hi}.$ We witness the spread versions of the small chunks. We already have $\texttt{spread}(c(11))$ and $\texttt{spread}(d(14))$ from the message scheduling.
$(X ⋙ 7) \oplus (X ⋙ 18) \oplus (X ≫ 3)$ is equivalent to
$(X ⋙ 7) \oplus (X ⋘ 14) \oplus (X ≫ 3)$.
diff --git a/book/src/design/gadgets/sinsemilla.md b/book/src/design/gadgets/sinsemilla.md
index 4a1b466ba4..b5fee9fc46 100644
--- a/book/src/design/gadgets/sinsemilla.md
+++ b/book/src/design/gadgets/sinsemilla.md
@@ -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}$
diff --git a/book/src/design/gadgets/sinsemilla/merkle-crh.md b/book/src/design/gadgets/sinsemilla/merkle-crh.md
index fc8e6a10f0..774c7eea4d 100644
--- a/book/src/design/gadgets/sinsemilla/merkle-crh.md
+++ b/book/src/design/gadgets/sinsemilla/merkle-crh.md
@@ -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}
+$$
+
+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:
-1. $a_0 = l$
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
+ inkscape:isstock="true"
+ inkscape:collect="always">
+ inkscape:isstock="true">
+ inkscape:isstock="true">
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
- image/svg+xml
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ image/svg+xml
+
+
+
+
+ 7 A B C D 7 7
+ 7
-
+ id="g1861">
B C D A
+ C 7
7 7 7 7
+
+ A 7
A B C D 7 3 7
+ 7 ≠ B σ
+ id="g1868">
B C D A
+
A 7
+
+ 3 7 C
+
+
+
+
+
+
+
+ σ
+
+
+
+
+
+ 7 C B A D
+
+
+
+
+
+ σ
+
+
+
+
A B C σ
diff --git a/book/src/design/proving-system/vanishing.md b/book/src/design/proving-system/vanishing.md
index 60025da7e7..72e1e21ee3 100644
--- a/book/src/design/proving-system/vanishing.md
+++ b/book/src/design/proving-system/vanishing.md
@@ -41,7 +41,7 @@ verifier samples $y$) linear combination of the circuit relations.
## Committing to $h(X)$
-$h(X)$ has degree $(d - 1)n - d$ (because the divisor $t(X)$ has degree $n$). However, the
+$h(X)$ has degree $d(n - 1) - n$ (because the divisor $t(X)$ has degree $n$). However, the
polynomial commitment scheme we use for Halo 2 only supports committing to polynomials of
degree $n - 1$ (which is the maximum degree that the rest of the protocol needs to commit
to). Instead of increasing the cost of the polynomial commitment scheme, the prover split
diff --git a/book/src/user/tips-and-tricks.md b/book/src/user/tips-and-tricks.md
index f4c880acb0..b2d7be0d95 100644
--- a/book/src/user/tips-and-tricks.md
+++ b/book/src/user/tips-and-tricks.md
@@ -14,7 +14,7 @@ the form:
$$a \cdot (1 - a) \cdot (2 - a) \cdot (3 - a) \cdot (4 - a) = 0$$
-while to constraint $c$ to be either 7 or 13, you would use:
+while to constrain $c$ to be either 7 or 13, you would use:
$$(7 - c) \cdot (13 - c) = 0$$
diff --git a/halo2/CHANGELOG.md b/halo2/CHANGELOG.md
index 62f528e75e..19cfec4d18 100644
--- a/halo2/CHANGELOG.md
+++ b/halo2/CHANGELOG.md
@@ -6,6 +6,8 @@ and this project adheres to Rust's notion of
[Semantic Versioning](https://semver.org/spec/v2.0.0.html).
## [Unreleased]
+
+## [0.1.0-beta.2] - 2022-02-14
### Removed
- Everything (moved to `halo2_proofs` crate).
diff --git a/halo2/Cargo.toml b/halo2/Cargo.toml
index 68a660a6e8..7a6bbaa94f 100644
--- a/halo2/Cargo.toml
+++ b/halo2/Cargo.toml
@@ -1,21 +1,25 @@
[package]
name = "halo2"
-version = "0.1.0-beta.1"
+version = "0.1.0-beta.2"
authors = [
- "Sean Bowe ",
- "Ying Tong Lai ",
- "Daira Hopwood ",
"Jack Grigg ",
]
-edition = "2018"
-license-file = "../COPYING"
+edition = "2021"
+rust-version = "1.56.1"
+description = "[BETA] Fast zero-knowledge proof-carrying data implementation with no trusted setup"
+license = "MIT OR Apache-2.0"
repository = "https://github.com/zcash/halo2"
documentation = "https://docs.rs/halo2"
readme = "../README.md"
+categories = ["cryptography"]
+keywords = ["halo", "proofs", "recursive", "zkp", "zkSNARKs"]
[package.metadata.docs.rs]
all-features = true
-rustdoc-args = ["--cfg", "docsrs", "--html-in-header", "../katex-header.html"]
+rustdoc-args = ["--cfg", "docsrs", "--html-in-header", "katex-header.html"]
[dependencies]
-halo2_proofs = { version = "0.1.0-beta.1", path = "../halo2_proofs" }
+halo2_proofs = { version = "0.2", path = "../halo2_proofs" }
+
+[lib]
+bench = false
diff --git a/katex-header.html b/halo2/katex-header.html
similarity index 100%
rename from katex-header.html
rename to halo2/katex-header.html
diff --git a/halo2_gadgets/CHANGELOG.md b/halo2_gadgets/CHANGELOG.md
index df364a5cc8..41019f9cea 100644
--- a/halo2_gadgets/CHANGELOG.md
+++ b/halo2_gadgets/CHANGELOG.md
@@ -7,10 +7,115 @@ and this project adheres to Rust's notion of
## [Unreleased]
+## [0.2.0] - 2022-06-23
+### Added
+- `halo2_gadgets::utilities::RangeConstrained>::bitrange_of`
+
+### Changed
+All APIs that represented witnessed values as `Option` now represent them as
+`halo2_proofs::circuit::Value`. The core API changes are listed below.
+
+- Migrated to `halo2_proofs 0.2.0`.
+- The following APIs now take `Value<_>` instead of `Option<_>`:
+ - `halo2_gadgets::ecc`:
+ - `EccInstructions::{witness_point, witness_point_non_id}`
+ - `EccInstructions::{witness_scalar_var, witness_scalar_fixed}`
+ - `ScalarVar::new`
+ - `ScalarFixed::new`
+ - `NonIdentityPoint::new`
+ - `Point::new`
+ - `halo2_gadgets::sinsemilla`:
+ - `SinsemillaInstructions::witness_message_piece`
+ - `MessagePiece::{from_field_elem, from_subpieces}`
+ - `halo2_gadgets::sinsemilla::merkle`:
+ - `MerklePath::construct`
+ - `halo2_gadgets::utilities`:
+ - `UtilitiesInstructions::load_private`
+ - `RangeConstrained::witness_short`
+ - `halo2_gadgets::utilities::cond_swap`:
+ - `CondSwapInstructions::swap`
+ - `halo2_gadgets::utilities::decompose_running_sum`:
+ - `RunningSumConfig::witness_decompose`
+ - `halo2_gadgets::utilities::lookup_range_check`:
+ - `LookupRangeCheckConfig::{witness_check, witness_short_check}`
+- The following APIs now return `Value<_>` instead of `Option<_>`:
+ - `halo2_gadgets::ecc::chip`:
+ - `EccPoint::{point, is_identity}`
+ - `NonIdentityEccPoint::point`
+ - `halo2_gadgets::utilities`:
+ - `FieldValue::value`
+ - `Var::value`
+ - `RangeConstrained::value`
+- `halo2_gadgets::sha256::BlockWord` is now a newtype wrapper around
+ `Value` instead of `Option`.
+
+### Removed
+- `halo2_gadgets::utilities::RangeConstrained>::bitrange_of`
+
+## [0.1.0] - 2022-05-10
+### Added
+- `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
-- pass in an additional `rng: impl RngCore` argument to `builder::InProgress::create_proof`, `builder::Bundle::create_proof`, `circuit::Proof::create`.
+- `halo2_gadgets::ecc`:
+ - `EccInstructions::ScalarVar` is now treated as a full-width scalar, instead
+ 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`.
+ - `FixedPointShort::mul` now takes `ScalarFixedShort` instead of
+ `(EccChip::Var, EccChip::Var)`.
+- `halo2_gadgets::ecc::chip`:
+ - `FixedPoint::u` now returns `Vec<[::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` instead of `Option`.
+ - `merkle::MerklePath` can now be constructed with more or fewer than two
+ `MerkleChip`s.
+
### Removed
-- `orchard::value::ValueSum::from_raw`
+- `halo2_gadgets::primitives` (use `halo2_gadgets::poseidon::primitives` or
+ `halo2_gadgets::sinsemilla::primitives` instead).
+
+## [0.1.0-beta.3] - 2022-04-06
+### Changed
+- Migrated to `halo2_proofs 0.1.0-beta.4`.
+
+## [0.1.0-beta.2] - 2022-03-22
+### Changed
+- Migrated to `halo2_proofs 0.1.0-beta.3`.
-## [0.1.0-beta.1] - 2021-12-17
+## [0.1.0-beta.1] - 2022-02-14
Initial release!
diff --git a/halo2_gadgets/Cargo.toml b/halo2_gadgets/Cargo.toml
index 3174693386..e07d3af198 100644
--- a/halo2_gadgets/Cargo.toml
+++ b/halo2_gadgets/Cargo.toml
@@ -1,6 +1,6 @@
[package]
name = "halo2_gadgets"
-version = "0.0.0"
+version = "0.2.0"
authors = [
"Sean Bowe ",
"Jack Grigg ",
@@ -8,29 +8,30 @@ authors = [
"Ying Tong Lai ",
"Kris Nuttycombe ",
]
-edition = "2018"
-description = "[BETA] Reusable gadgets and chip implementations for Halo 2"
-license-file = "../COPYING"
+edition = "2021"
+rust-version = "1.56.1"
+description = "Reusable gadgets and chip implementations for Halo 2"
+license = "MIT OR Apache-2.0"
repository = "https://github.com/zcash/halo2"
readme = "README.md"
categories = ["cryptography"]
-keywords = ["zcash"]
+keywords = ["halo", "proofs", "zcash", "zkp", "zkSNARKs"]
[package.metadata.docs.rs]
all-features = true
-rustdoc-args = ["--cfg", "docsrs", "--html-in-header", "../katex-header.html"]
+rustdoc-args = ["--cfg", "docsrs", "--html-in-header", "katex-header.html"]
[dependencies]
arrayvec = "0.7.0"
-bitvec = "0.22"
-ff = "0.11"
-group = "0.11"
-halo2_proofs = { version = "=0.1.0-beta.1", path = "../halo2_proofs" }
+bitvec = "1"
+ff = "0.12"
+group = "0.12"
+halo2_proofs = { version = "0.2", path = "../halo2_proofs" }
lazy_static = "1"
proptest = { version = "1.0.0", optional = true }
rand = "0.8"
subtle = "2.3"
-uint = "=0.9.1" # uint 0.9.2 bumps the MSRV to 1.56.1
+uint = "0.9.2" # MSRV 1.56.1
# Developer tooling dependencies
plotters = { version = "0.3.0", optional = true }
@@ -40,7 +41,7 @@ criterion = "0.3"
proptest = "1.0.0"
[target.'cfg(unix)'.dev-dependencies]
-pprof = { version = "=0.6.1", features = ["criterion", "flamegraph"] }
+pprof = { version = "0.8", features = ["criterion", "flamegraph"] } # MSRV 1.56
[lib]
bench = false
diff --git a/halo2_gadgets/README.md b/halo2_gadgets/README.md
index db1aa509ae..4ed744f81f 100644
--- a/halo2_gadgets/README.md
+++ b/halo2_gadgets/README.md
@@ -1,8 +1,6 @@
# halo2_gadgets [](https://crates.io/crates/halo2_gadgets) #
-**IMPORTANT**: This library is being actively developed and should not be used in production software.
-
-Requires Rust 1.51+.
+Requires Rust 1.56.1+.
## Documentation
@@ -11,14 +9,17 @@ Requires Rust 1.51+.
## License
-Copyright 2020-2021 The Electric Coin Company.
+Licensed under either of
+
+ * Apache License, Version 2.0, ([LICENSE-APACHE](LICENSE-APACHE) or
+ http://www.apache.org/licenses/LICENSE-2.0)
+ * MIT license ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT)
+
+at your option.
-You may use this package under the Bootstrap Open Source Licence, version 1.0,
-or at your option, any later version. See the file [`COPYING`](COPYING) for
-more details, and [`LICENSE-BOSL`](LICENSE-BOSL) for the terms of the Bootstrap
-Open Source Licence, version 1.0.
+### Contribution
-The purpose of the BOSL is to allow commercial improvements to the package
-while ensuring that all improvements are open source. See
-[here](https://electriccoin.co/blog/introducing-tgppl-a-radically-new-type-of-open-source-license/)
-for why the BOSL exists.
+Unless you explicitly state otherwise, any contribution intentionally
+submitted for inclusion in the work by you, as defined in the Apache-2.0
+license, shall be dual licensed as above, without any additional terms or
+conditions.
diff --git a/halo2_gadgets/katex-header.html b/halo2_gadgets/katex-header.html
new file mode 100644
index 0000000000..98e85904fa
--- /dev/null
+++ b/halo2_gadgets/katex-header.html
@@ -0,0 +1,15 @@
+);
+pub struct BlockWord(pub Value);
#[derive(Clone, Debug)]
/// Little-endian bits (up to 64 bits)
@@ -129,26 +129,26 @@ impl AssignedBits {
annotation: A,
column: impl Into>,
offset: usize,
- value: Option,
+ value: Value,
) -> Result
where
A: Fn() -> AR,
AR: Into,
>::Error: std::fmt::Debug,
{
- let value: Option<[bool; LEN]> = value.map(|v| v.try_into().unwrap());
- let value: Option> = value.map(|v| v.into());
+ let value: Value<[bool; LEN]> = value.map(|v| v.try_into().unwrap());
+ let value: Value> = value.map(|v| v.into());
let column: Column = column.into();
match column.column_type() {
Any::Advice => {
region.assign_advice(annotation, column.try_into().unwrap(), offset, || {
- value.clone().ok_or(Error::Synthesis)
+ value.clone()
})
}
Any::Fixed => {
region.assign_fixed(annotation, column.try_into().unwrap(), offset, || {
- value.clone().ok_or(Error::Synthesis)
+ value.clone()
})
}
_ => panic!("Cannot assign to instance column"),
@@ -158,7 +158,7 @@ impl AssignedBits {
}
impl AssignedBits<16> {
- fn value_u16(&self) -> Option {
+ fn value_u16(&self) -> Value {
self.value().map(|v| v.into())
}
@@ -167,23 +167,23 @@ impl AssignedBits<16> {
annotation: A,
column: impl Into>,
offset: usize,
- value: Option,
+ value: Value,
) -> Result
where
A: Fn() -> AR,
AR: Into,
{
let column: Column = column.into();
- let value: Option> = value.map(|v| v.into());
+ let value: Value> = value.map(|v| v.into());
match column.column_type() {
Any::Advice => {
region.assign_advice(annotation, column.try_into().unwrap(), offset, || {
- value.clone().ok_or(Error::Synthesis)
+ value.clone()
})
}
Any::Fixed => {
region.assign_fixed(annotation, column.try_into().unwrap(), offset, || {
- value.clone().ok_or(Error::Synthesis)
+ value.clone()
})
}
_ => panic!("Cannot assign to instance column"),
@@ -193,7 +193,7 @@ impl AssignedBits<16> {
}
impl AssignedBits<32> {
- fn value_u32(&self) -> Option {
+ fn value_u32(&self) -> Value {
self.value().map(|v| v.into())
}
@@ -202,23 +202,23 @@ impl AssignedBits<32> {
annotation: A,
column: impl Into>,
offset: usize,
- value: Option,
+ value: Value,
) -> Result
where
A: Fn() -> AR,
AR: Into,
{
let column: Column = column.into();
- let value: Option> = value.map(|v| v.into());
+ let value: Value> = value.map(|v| v.into());
match column.column_type() {
Any::Advice => {
region.assign_advice(annotation, column.try_into().unwrap(), offset, || {
- value.clone().ok_or(Error::Synthesis)
+ value.clone()
})
}
Any::Fixed => {
region.assign_fixed(annotation, column.try_into().unwrap(), offset, || {
- value.clone().ok_or(Error::Synthesis)
+ value.clone()
})
}
_ => panic!("Cannot assign to instance column"),
@@ -376,10 +376,10 @@ trait Table16Assignment {
lookup: &SpreadInputs,
a_3: Column,
row: usize,
- r_0_even: Option<[bool; 16]>,
- r_0_odd: Option<[bool; 16]>,
- r_1_even: Option<[bool; 16]>,
- r_1_odd: Option<[bool; 16]>,
+ r_0_even: Value<[bool; 16]>,
+ r_0_odd: Value<[bool; 16]>,
+ r_1_even: Value<[bool; 16]>,
+ r_1_odd: Value<[bool; 16]>,
) -> Result<
(
(AssignedBits<16>, AssignedBits<16>),
@@ -428,10 +428,10 @@ trait Table16Assignment {
lookup: &SpreadInputs,
a_3: Column,
row: usize,
- r_0_even: Option<[bool; 16]>,
- r_0_odd: Option<[bool; 16]>,
- r_1_even: Option<[bool; 16]>,
- r_1_odd: Option<[bool; 16]>,
+ r_0_even: Value<[bool; 16]>,
+ r_0_odd: Value<[bool; 16]>,
+ r_1_even: Value<[bool; 16]>,
+ r_1_odd: Value<[bool; 16]>,
) -> Result<(AssignedBits<16>, AssignedBits<16>), Error> {
let (even, _odd) = self.assign_spread_outputs(
region, lookup, a_3, row, r_0_even, r_0_odd, r_1_even, r_1_odd,
diff --git a/halo2_gadgets/src/sha256/table16/compression.rs b/halo2_gadgets/src/sha256/table16/compression.rs
index b22b2ef4fa..ecff28bab4 100644
--- a/halo2_gadgets/src/sha256/table16/compression.rs
+++ b/halo2_gadgets/src/sha256/table16/compression.rs
@@ -4,7 +4,7 @@ use super::{
AssignedBits, BlockWord, SpreadInputs, SpreadVar, Table16Assignment, ROUNDS, STATE,
};
use halo2_proofs::{
- circuit::Layouter,
+ circuit::{Layouter, Value},
pairing::bn256::Fr,
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
poly::Rotation,
@@ -27,12 +27,12 @@ pub trait UpperSigmaVar<
const D_LEN: usize,
>
{
- fn spread_a(&self) -> Option<[bool; A_LEN]>;
- fn spread_b(&self) -> Option<[bool; B_LEN]>;
- fn spread_c(&self) -> Option<[bool; C_LEN]>;
- fn spread_d(&self) -> Option<[bool; D_LEN]>;
+ fn spread_a(&self) -> Value<[bool; A_LEN]>;
+ fn spread_b(&self) -> Value<[bool; B_LEN]>;
+ fn spread_c(&self) -> Value<[bool; C_LEN]>;
+ fn spread_d(&self) -> Value<[bool; D_LEN]>;
- fn xor_upper_sigma(&self) -> Option<[bool; 64]> {
+ fn xor_upper_sigma(&self) -> Value<[bool; 64]> {
self.spread_a()
.zip(self.spread_b())
.zip(self.spread_c())
@@ -128,15 +128,15 @@ impl AbcdVar {
}
impl UpperSigmaVar<4, 22, 18, 20> for AbcdVar {
- fn spread_a(&self) -> Option<[bool; 4]> {
+ fn spread_a(&self) -> Value<[bool; 4]> {
self.a.spread.value().map(|v| v.0)
}
- fn spread_b(&self) -> Option<[bool; 22]> {
+ fn spread_b(&self) -> Value<[bool; 22]> {
self.b.spread.value().map(|v| v.0)
}
- fn spread_c(&self) -> Option<[bool; 18]> {
+ fn spread_c(&self) -> Value<[bool; 18]> {
self.c_lo
.spread
.value()
@@ -153,7 +153,7 @@ impl UpperSigmaVar<4, 22, 18, 20> for AbcdVar {
})
}
- fn spread_d(&self) -> Option<[bool; 20]> {
+ fn spread_d(&self) -> Value<[bool; 20]> {
self.d.spread.value().map(|v| v.0)
}
}
@@ -217,7 +217,7 @@ impl EfghVar {
}
impl UpperSigmaVar<12, 10, 28, 14> for EfghVar {
- fn spread_a(&self) -> Option<[bool; 12]> {
+ fn spread_a(&self) -> Value<[bool; 12]> {
self.a_lo
.spread
.value()
@@ -232,7 +232,7 @@ impl UpperSigmaVar<12, 10, 28, 14> for EfghVar {
})
}
- fn spread_b(&self) -> Option<[bool; 10]> {
+ fn spread_b(&self) -> Value<[bool; 10]> {
self.b_lo
.spread
.value()
@@ -247,11 +247,11 @@ impl UpperSigmaVar<12, 10, 28, 14> for EfghVar {
})
}
- fn spread_c(&self) -> Option<[bool; 28]> {
+ fn spread_c(&self) -> Value<[bool; 28]> {
self.c.spread.value().map(|v| v.0)
}
- fn spread_d(&self) -> Option<[bool; 14]> {
+ fn spread_d(&self) -> Value<[bool; 14]> {
self.d.spread.value().map(|v| v.0)
}
}
@@ -266,7 +266,7 @@ impl From<(AssignedBits<16>, AssignedBits<16>)> for RoundWordDense {
}
impl RoundWordDense {
- pub fn value(&self) -> Option {
+ pub fn value(&self) -> Value {
self.0
.value_u16()
.zip(self.1.value_u16())
@@ -284,7 +284,7 @@ impl From<(AssignedBits<32>, AssignedBits<32>)> for RoundWordSpread {
}
impl RoundWordSpread {
- pub fn value(&self) -> Option {
+ pub fn value(&self) -> Value {
self.0
.value_u32()
.zip(self.1.value_u32())
@@ -922,7 +922,7 @@ impl CompressionConfig {
layouter: &mut impl Layouter,
state: State,
) -> Result<[BlockWord; DIGEST_SIZE], Error> {
- let mut digest = [BlockWord(Some(0)); DIGEST_SIZE];
+ let mut digest = [BlockWord(Value::known(0)); DIGEST_SIZE];
layouter.assign_region(
|| "digest",
|mut region| {
@@ -984,10 +984,10 @@ mod tests {
let digest = config.compression.digest(&mut layouter, state)?;
for (idx, digest_word) in digest.iter().enumerate() {
- assert_eq!(
- (digest_word.0.unwrap() as u64 + IV[idx] as u64) as u32,
- super::compression_util::COMPRESSION_OUTPUT[idx]
- );
+ digest_word.0.assert_if_known(|digest_word| {
+ (*digest_word as u64 + IV[idx] as u64) as u32
+ == super::compression_util::COMPRESSION_OUTPUT[idx]
+ });
}
Ok(())
diff --git a/halo2_gadgets/src/sha256/table16/compression/compression_gates.rs b/halo2_gadgets/src/sha256/table16/compression/compression_gates.rs
index 4c0a03dde2..e22a10210c 100644
--- a/halo2_gadgets/src/sha256/table16/compression/compression_gates.rs
+++ b/halo2_gadgets/src/sha256/table16/compression/compression_gates.rs
@@ -1,6 +1,9 @@
use super::super::{util::*, Gate};
-use halo2_proofs::{arithmetic::FieldExt, plonk::Expression};
-use std::{array, marker::PhantomData};
+use halo2_proofs::{
+ arithmetic::FieldExt,
+ plonk::{Constraint, Constraints, Expression},
+};
+use std::marker::PhantomData;
pub struct CompressionGate(PhantomData);
@@ -32,7 +35,11 @@ impl CompressionGate {
spread_word_lo: Expression,
word_hi: Expression,
spread_word_hi: Expression,
- ) -> impl Iterator- )> {
+ ) -> Constraints<
+ F,
+ (&'static str, Expression
),
+ impl Iterator- )>,
+ > {
let check_spread_and_range =
Gate::three_bit_spread_and_range(c_lo.clone(), spread_c_lo.clone())
.chain(Gate::three_bit_spread_and_range(
@@ -63,12 +70,14 @@ impl
CompressionGate {
+ spread_word_lo * (-F::one())
+ spread_word_hi * F::from(1 << 32) * (-F::one());
- check_spread_and_range
- .chain(Some(("range_check_tag_b", range_check_tag_b)))
- .chain(Some(("range_check_tag_d", range_check_tag_d)))
- .chain(Some(("dense_check", dense_check)))
- .chain(Some(("spread_check", spread_check)))
- .map(move |(name, poly)| (name, s_decompose_abcd.clone() * poly))
+ Constraints::with_selector(
+ s_decompose_abcd,
+ check_spread_and_range
+ .chain(Some(("range_check_tag_b", range_check_tag_b)))
+ .chain(Some(("range_check_tag_d", range_check_tag_d)))
+ .chain(Some(("dense_check", dense_check)))
+ .chain(Some(("spread_check", spread_check))),
+ )
}
// Decompose `E,F,G,H` words
@@ -94,7 +103,11 @@ impl CompressionGate {
spread_word_lo: Expression,
word_hi: Expression,
spread_word_hi: Expression,
- ) -> impl Iterator- )> {
+ ) -> Constraints<
+ F,
+ (&'static str, Expression
),
+ impl Iterator- )>,
+ > {
let check_spread_and_range =
Gate::three_bit_spread_and_range(a_lo.clone(), spread_a_lo.clone())
.chain(Gate::three_bit_spread_and_range(
@@ -128,12 +141,14 @@ impl
CompressionGate {
+ spread_word_lo * (-F::one())
+ spread_word_hi * F::from(1 << 32) * (-F::one());
- check_spread_and_range
- .chain(Some(("range_check_tag_c", range_check_tag_c)))
- .chain(Some(("range_check_tag_d", range_check_tag_d)))
- .chain(Some(("dense_check", dense_check)))
- .chain(Some(("spread_check", spread_check)))
- .map(move |(name, poly)| (name, s_decompose_efgh.clone() * poly))
+ Constraints::with_selector(
+ s_decompose_efgh,
+ check_spread_and_range
+ .chain(Some(("range_check_tag_c", range_check_tag_c)))
+ .chain(Some(("range_check_tag_d", range_check_tag_d)))
+ .chain(Some(("dense_check", dense_check)))
+ .chain(Some(("spread_check", spread_check))),
+ )
}
// s_upper_sigma_0 on abcd words
@@ -151,7 +166,7 @@ impl CompressionGate {
spread_c_mid: Expression,
spread_c_hi: Expression,
spread_d: Expression,
- ) -> impl Iterator- )> {
+ ) -> Option<(&'static str, Expression
)> {
let spread_witness = spread_r0_even
+ spread_r0_odd * F::from(2)
+ (spread_r1_even + spread_r1_odd * F::from(2)) * F::from(1 << 32);
@@ -176,7 +191,7 @@ impl CompressionGate {
let xor = xor_0 + xor_1 + xor_2;
let check = spread_witness + (xor * -F::one());
- std::iter::empty().chain(Some(("s_upper_sigma_0", s_upper_sigma_0 * check)))
+ Some(("s_upper_sigma_0", s_upper_sigma_0 * check))
}
// s_upper_sigma_1 on efgh words
@@ -194,7 +209,7 @@ impl CompressionGate {
spread_b_hi: Expression,
spread_c: Expression,
spread_d: Expression,
- ) -> impl Iterator- )> {
+ ) -> Option<(&'static str, Expression
)> {
let spread_witness = spread_r0_even
+ spread_r0_odd * F::from(2)
+ (spread_r1_even + spread_r1_odd * F::from(2)) * F::from(1 << 32);
@@ -220,7 +235,7 @@ impl CompressionGate {
let xor = xor_0 + xor_1 + xor_2;
let check = spread_witness + (xor * -F::one());
- std::iter::empty().chain(Some(("s_upper_sigma_1", s_upper_sigma_1 * check)))
+ Some(("s_upper_sigma_1", s_upper_sigma_1 * check))
}
// First part of choice gate on (E, F, G), E ∧ F
@@ -235,7 +250,7 @@ impl CompressionGate {
spread_e_hi: Expression,
spread_f_lo: Expression,
spread_f_hi: Expression,
- ) -> impl Iterator- )> {
+ ) -> Option<(&'static str, Expression
)> {
let lhs_lo = spread_e_lo + spread_f_lo;
let lhs_hi = spread_e_hi + spread_f_hi;
let lhs = lhs_lo + lhs_hi * F::from(1 << 32);
@@ -246,7 +261,7 @@ impl CompressionGate {
let check = lhs + rhs * -F::one();
- std::iter::empty().chain(Some(("s_ch", s_ch * check)))
+ Some(("s_ch", s_ch * check))
}
// Second part of Choice gate on (E, F, G), ¬E ∧ G
@@ -263,7 +278,11 @@ impl CompressionGate {
spread_e_neg_hi: Expression,
spread_g_lo: Expression,
spread_g_hi: Expression,
- ) -> impl Iterator- )> {
+ ) -> Constraints<
+ F,
+ (&'static str, Expression
),
+ impl Iterator- )>,
+ > {
let neg_check = {
let evens = Self::ones() * F::from(MASK_EVEN_32 as u64);
// evens - spread_e_lo = spread_e_neg_lo
@@ -284,9 +303,7 @@ impl
CompressionGate {
let rhs_odd = spread_q0_odd + spread_q1_odd * F::from(1 << 32);
let rhs = rhs_even + rhs_odd * F::from(2);
- neg_check
- .chain(Some(("s_ch_neg", lhs - rhs)))
- .map(move |(name, poly)| (name, s_ch_neg.clone() * poly))
+ Constraints::with_selector(s_ch_neg, neg_check.chain(Some(("s_ch_neg", lhs - rhs))))
}
// Majority gate on (A, B, C)
@@ -303,7 +320,7 @@ impl CompressionGate {
spread_b_hi: Expression,
spread_c_lo: Expression,
spread_c_hi: Expression,
- ) -> impl Iterator- )> {
+ ) -> Option<(&'static str, Expression
)> {
let maj_even = spread_m_0_even + spread_m_1_even * F::from(1 << 32);
let maj_odd = spread_m_0_odd + spread_m_1_odd * F::from(1 << 32);
let maj = maj_even + maj_odd * F::from(2);
@@ -313,7 +330,7 @@ impl CompressionGate {
let c = spread_c_lo + spread_c_hi * F::from(1 << 32);
let sum = a + b + c;
- std::iter::empty().chain(Some(("maj", s_maj * (sum - maj))))
+ Some(("maj", s_maj * (sum - maj)))
}
// s_h_prime to get H' = H + Ch(E, F, G) + s_upper_sigma_1(E) + K + W
@@ -335,7 +352,7 @@ impl CompressionGate {
k_hi: Expression,
w_lo: Expression,
w_hi: Expression,
- ) -> impl Iterator- )> {
+ ) -> Option<(&'static str, Expression
)> {
let lo = h_lo + ch_lo + ch_neg_lo + sigma_e_lo + k_lo + w_lo;
let hi = h_hi + ch_hi + ch_neg_hi + sigma_e_hi + k_hi + w_hi;
@@ -344,7 +361,7 @@ impl CompressionGate {
let check = sum - (h_prime_carry * F::from(1 << 32)) - h_prime;
- std::iter::empty().chain(Some(("s_h_prime", s_h_prime * check)))
+ Some(("s_h_prime", s_h_prime * check))
}
// s_a_new to get A_new = H' + Maj(A, B, C) + s_upper_sigma_0(A)
@@ -360,7 +377,7 @@ impl CompressionGate {
maj_abc_hi: Expression,
h_prime_lo: Expression,
h_prime_hi: Expression,
- ) -> impl Iterator- )> {
+ ) -> Option<(&'static str, Expression
)> {
let lo = sigma_a_lo + maj_abc_lo + h_prime_lo;
let hi = sigma_a_hi + maj_abc_hi + h_prime_hi;
let sum = lo + hi * F::from(1 << 16);
@@ -368,7 +385,7 @@ impl CompressionGate {
let check = sum - (a_new_carry * F::from(1 << 32)) - a_new;
- std::iter::empty().chain(Some(("s_a_new", s_a_new * check)))
+ Some(("s_a_new", s_a_new * check))
}
// s_e_new to get E_new = H' + D
@@ -382,7 +399,7 @@ impl CompressionGate {
d_hi: Expression,
h_prime_lo: Expression,
h_prime_hi: Expression,
- ) -> impl Iterator- )> {
+ ) -> Option<(&'static str, Expression
)> {
let lo = h_prime_lo + d_lo;
let hi = h_prime_hi + d_hi;
let sum = lo + hi * F::from(1 << 16);
@@ -390,7 +407,7 @@ impl CompressionGate {
let check = sum - (e_new_carry * F::from(1 << 32)) - e_new;
- std::iter::empty().chain(Some(("s_e_new", s_e_new * check)))
+ Some(("s_e_new", s_e_new * check))
}
// s_digest on final round
@@ -409,17 +426,19 @@ impl CompressionGate {
lo_3: Expression,
hi_3: Expression,
word_3: Expression,
- ) -> impl Iterator- )> {
+ ) -> impl IntoIterator
- > {
let check_lo_hi = |lo: Expression
, hi: Expression, word: Expression| {
lo + hi * F::from(1 << 16) - word
};
- array::IntoIter::new([
- ("check_lo_hi_0", check_lo_hi(lo_0, hi_0, word_0)),
- ("check_lo_hi_1", check_lo_hi(lo_1, hi_1, word_1)),
- ("check_lo_hi_2", check_lo_hi(lo_2, hi_2, word_2)),
- ("check_lo_hi_3", check_lo_hi(lo_3, hi_3, word_3)),
- ])
- .map(move |(name, poly)| (name, s_digest.clone() * poly))
+ Constraints::with_selector(
+ s_digest,
+ [
+ ("check_lo_hi_0", check_lo_hi(lo_0, hi_0, word_0)),
+ ("check_lo_hi_1", check_lo_hi(lo_1, hi_1, word_1)),
+ ("check_lo_hi_2", check_lo_hi(lo_2, hi_2, word_2)),
+ ("check_lo_hi_3", check_lo_hi(lo_3, hi_3, word_3)),
+ ],
+ )
}
}
diff --git a/halo2_gadgets/src/sha256/table16/compression/compression_util.rs b/halo2_gadgets/src/sha256/table16/compression/compression_util.rs
index 418ff259b3..9506fdcaf0 100644
--- a/halo2_gadgets/src/sha256/table16/compression/compression_util.rs
+++ b/halo2_gadgets/src/sha256/table16/compression/compression_util.rs
@@ -6,7 +6,7 @@ use crate::sha256::table16::{
util::*, AssignedBits, SpreadVar, SpreadWord, StateWord, Table16Assignment,
};
use halo2_proofs::{
- circuit::Region,
+ circuit::{Region, Value},
pairing::bn256::Fr,
plonk::{Advice, Column, Error},
};
@@ -39,70 +39,77 @@ pub const SUBREGION_MAIN_WORD: usize =
DECOMPOSE_ABCD + SIGMA_0_ROWS + DECOMPOSE_EFGH + SIGMA_1_ROWS + CH_ROWS + MAJ_ROWS;
pub const SUBREGION_MAIN_ROWS: usize = SUBREGION_MAIN_LEN * SUBREGION_MAIN_WORD;
+/// The initial round.
+pub struct InitialRound;
+
+/// A main round index.
+#[derive(Debug, Copy, Clone)]
+pub struct MainRoundIdx(usize);
+
/// Round index.
#[derive(Debug, Copy, Clone)]
pub enum RoundIdx {
Init,
- Main(usize),
+ Main(MainRoundIdx),
+}
+
+impl From for RoundIdx {
+ fn from(_: InitialRound) -> Self {
+ RoundIdx::Init
+ }
}
-impl RoundIdx {
+impl From for RoundIdx {
+ fn from(idx: MainRoundIdx) -> Self {
+ RoundIdx::Main(idx)
+ }
+}
+
+impl MainRoundIdx {
pub(crate) fn as_usize(&self) -> usize {
- match self {
- Self::Main(idx) => *idx,
- _ => panic!(),
- }
+ self.0
}
}
-impl From for RoundIdx {
+impl From for MainRoundIdx {
fn from(idx: usize) -> Self {
- Self::Main(idx)
+ MainRoundIdx(idx)
}
}
-impl std::ops::Add for RoundIdx {
+impl std::ops::Add for MainRoundIdx {
type Output = Self;
fn add(self, rhs: usize) -> Self::Output {
- match self {
- Self::Main(idx) => Self::Main(idx + rhs),
- _ => panic!(),
- }
+ MainRoundIdx(self.0 + rhs)
}
}
-impl Ord for RoundIdx {
+impl Ord for MainRoundIdx {
fn cmp(&self, other: &Self) -> std::cmp::Ordering {
- match (self, other) {
- (Self::Main(idx_0), Self::Main(idx_1)) => idx_0.cmp(idx_1),
- _ => panic!(),
- }
+ self.0.cmp(&other.0)
}
}
-impl PartialOrd for RoundIdx {
+impl PartialOrd for MainRoundIdx {
fn partial_cmp(&self, other: &Self) -> Option {
Some(self.cmp(other))
}
}
-impl PartialEq for RoundIdx {
+impl PartialEq for MainRoundIdx {
fn eq(&self, other: &Self) -> bool {
- match (self, other) {
- (Self::Main(idx_0), Self::Main(idx_1)) => idx_0 == idx_1,
- _ => panic!(),
- }
+ self.0 == other.0
}
}
-impl Eq for RoundIdx {}
+impl Eq for MainRoundIdx {}
/// Returns starting row number of a compression round
pub fn get_round_row(round_idx: RoundIdx) -> usize {
match round_idx {
RoundIdx::Init => 0,
- RoundIdx::Main(idx) => {
+ RoundIdx::Main(MainRoundIdx(idx)) => {
assert!(idx < 64);
(idx as usize) * SUBREGION_MAIN_WORD
}
@@ -113,81 +120,73 @@ pub fn get_decompose_e_row(round_idx: RoundIdx) -> usize {
get_round_row(round_idx)
}
-pub fn get_decompose_f_row(round_idx: RoundIdx) -> usize {
- assert!(matches!(round_idx, RoundIdx::Init));
- get_decompose_e_row(round_idx) + DECOMPOSE_EFGH
+pub fn get_decompose_f_row(round_idx: InitialRound) -> usize {
+ get_decompose_e_row(round_idx.into()) + DECOMPOSE_EFGH
}
-pub fn get_decompose_g_row(round_idx: RoundIdx) -> usize {
+pub fn get_decompose_g_row(round_idx: InitialRound) -> usize {
get_decompose_f_row(round_idx) + DECOMPOSE_EFGH
}
-pub fn get_upper_sigma_1_row(round_idx: RoundIdx) -> usize {
- assert!(matches!(round_idx, RoundIdx::Main(_)));
- get_decompose_e_row(round_idx) + DECOMPOSE_EFGH + 1
+pub fn get_upper_sigma_1_row(round_idx: MainRoundIdx) -> usize {
+ get_decompose_e_row(round_idx.into()) + DECOMPOSE_EFGH + 1
}
-pub fn get_ch_row(round_idx: RoundIdx) -> usize {
- assert!(matches!(round_idx, RoundIdx::Main(_)));
- get_decompose_e_row(round_idx) + DECOMPOSE_EFGH + SIGMA_1_ROWS + 1
+pub fn get_ch_row(round_idx: MainRoundIdx) -> usize {
+ get_decompose_e_row(round_idx.into()) + DECOMPOSE_EFGH + SIGMA_1_ROWS + 1
}
-pub fn get_ch_neg_row(round_idx: RoundIdx) -> usize {
+pub fn get_ch_neg_row(round_idx: MainRoundIdx) -> usize {
get_ch_row(round_idx) + CH_ROWS / 2
}
pub fn get_decompose_a_row(round_idx: RoundIdx) -> usize {
match round_idx {
RoundIdx::Init => get_h_row(round_idx) + DECOMPOSE_EFGH,
- _ => get_ch_neg_row(round_idx) - 1 + CH_ROWS / 2,
+ RoundIdx::Main(mri) => get_ch_neg_row(mri) - 1 + CH_ROWS / 2,
}
}
-pub fn get_upper_sigma_0_row(round_idx: RoundIdx) -> usize {
- assert!(matches!(round_idx, RoundIdx::Main(_)));
- get_decompose_a_row(round_idx) + DECOMPOSE_ABCD + 1
+pub fn get_upper_sigma_0_row(round_idx: MainRoundIdx) -> usize {
+ get_decompose_a_row(round_idx.into()) + DECOMPOSE_ABCD + 1
}
-pub fn get_decompose_b_row(round_idx: RoundIdx) -> usize {
- assert!(matches!(round_idx, RoundIdx::Init));
- get_decompose_a_row(round_idx) + DECOMPOSE_ABCD
+pub fn get_decompose_b_row(round_idx: InitialRound) -> usize {
+ get_decompose_a_row(round_idx.into()) + DECOMPOSE_ABCD
}
-pub fn get_decompose_c_row(round_idx: RoundIdx) -> usize {
+pub fn get_decompose_c_row(round_idx: InitialRound) -> usize {
get_decompose_b_row(round_idx) + DECOMPOSE_ABCD
}
-pub fn get_maj_row(round_idx: RoundIdx) -> usize {
- assert!(matches!(round_idx, RoundIdx::Main(_)));
+pub fn get_maj_row(round_idx: MainRoundIdx) -> usize {
get_upper_sigma_0_row(round_idx) + SIGMA_0_ROWS
}
// Get state word rows
pub fn get_h_row(round_idx: RoundIdx) -> usize {
match round_idx {
- RoundIdx::Init => get_decompose_g_row(round_idx) + DECOMPOSE_EFGH,
- _ => get_ch_row(round_idx) - 1,
+ RoundIdx::Init => get_decompose_g_row(InitialRound) + DECOMPOSE_EFGH,
+ RoundIdx::Main(mri) => get_ch_row(mri) - 1,
}
}
-pub fn get_h_prime_row(round_idx: RoundIdx) -> usize {
- assert!(matches!(round_idx, RoundIdx::Main(_)));
+pub fn get_h_prime_row(round_idx: MainRoundIdx) -> usize {
get_ch_row(round_idx)
}
pub fn get_d_row(round_idx: RoundIdx) -> usize {
match round_idx {
- RoundIdx::Init => get_decompose_c_row(round_idx) + DECOMPOSE_ABCD,
- _ => get_ch_row(round_idx) + 2,
+ RoundIdx::Init => get_decompose_c_row(InitialRound) + DECOMPOSE_ABCD,
+ RoundIdx::Main(mri) => get_ch_row(mri) + 2,
}
}
-pub fn get_e_new_row(round_idx: RoundIdx) -> usize {
- assert!(matches!(round_idx, RoundIdx::Main(_)));
- get_d_row(round_idx)
+pub fn get_e_new_row(round_idx: MainRoundIdx) -> usize {
+ get_d_row(round_idx.into())
}
-pub fn get_a_new_row(round_idx: RoundIdx) -> usize {
+pub fn get_a_new_row(round_idx: MainRoundIdx) -> usize {
get_maj_row(round_idx)
}
@@ -204,7 +203,7 @@ impl CompressionConfig {
&self,
region: &mut Region<'_, Fr>,
row: usize,
- val: Option,
+ val: Value,
) -> Result {
self.s_decompose_abcd.enable(region, row)?;
@@ -214,7 +213,7 @@ impl CompressionConfig {
let a_6 = self.extras[2];
let spread_pieces = val.map(AbcdVar::pieces);
- let spread_pieces = transpose_option_vec(spread_pieces, 6);
+ let spread_pieces = spread_pieces.transpose_vec(6);
let a = SpreadVar::without_lookup(
region,
@@ -275,7 +274,7 @@ impl CompressionConfig {
&self,
region: &mut Region<'_, Fr>,
row: usize,
- val: Option,
+ val: Value,
) -> Result {
self.s_decompose_efgh.enable(region, row)?;
@@ -285,7 +284,7 @@ impl CompressionConfig {
let a_6 = self.extras[2];
let spread_pieces = val.map(EfghVar::pieces);
- let spread_pieces = transpose_option_vec(spread_pieces, 6);
+ let spread_pieces = spread_pieces.transpose_vec(6);
let a_lo = SpreadVar::without_lookup(
region,
@@ -346,7 +345,7 @@ impl CompressionConfig {
&self,
region: &mut Region<'_, Fr>,
round_idx: RoundIdx,
- a_val: Option,
+ a_val: Value,
) -> Result {
let row = get_decompose_a_row(round_idx);
@@ -359,7 +358,7 @@ impl CompressionConfig {
&self,
region: &mut Region<'_, Fr>,
round_idx: RoundIdx,
- e_val: Option,
+ e_val: Value,
) -> Result {
let row = get_decompose_e_row(round_idx);
@@ -371,7 +370,7 @@ impl CompressionConfig {
pub(super) fn assign_upper_sigma_0(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
word: AbcdVar,
) -> Result<(AssignedBits<16>, AssignedBits<16>), Error> {
// Rename these here for ease of matching the gates to the specification.
@@ -406,11 +405,11 @@ impl CompressionConfig {
// Calculate R_0^{even}, R_0^{odd}, R_1^{even}, R_1^{odd}
let r = word.xor_upper_sigma();
- let r_0: Option<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
+ let r_0: Value<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
let r_0_even = r_0.map(even_bits);
let r_0_odd = r_0.map(odd_bits);
- let r_1: Option<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
+ let r_1: Value<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
let r_1_even = r_1.map(even_bits);
let r_1_odd = r_1.map(odd_bits);
@@ -429,7 +428,7 @@ impl CompressionConfig {
pub(super) fn assign_upper_sigma_1(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
word: EfghVar,
) -> Result<(AssignedBits<16>, AssignedBits<16>), Error> {
// Rename these here for ease of matching the gates to the specification.
@@ -465,11 +464,11 @@ impl CompressionConfig {
// Calculate R_0^{even}, R_0^{odd}, R_1^{even}, R_1^{odd}
// Calculate R_0^{even}, R_0^{odd}, R_1^{even}, R_1^{odd}
let r = word.xor_upper_sigma();
- let r_0: Option<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
+ let r_0: Value<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
let r_0_even = r_0.map(even_bits);
let r_0_odd = r_0.map(odd_bits);
- let r_1: Option<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
+ let r_1: Value<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
let r_1_even = r_1.map(even_bits);
let r_1_odd = r_1.map(odd_bits);
@@ -489,10 +488,10 @@ impl CompressionConfig {
&self,
region: &mut Region<'_, Fr>,
row: usize,
- r_0_even: Option<[bool; 16]>,
- r_0_odd: Option<[bool; 16]>,
- r_1_even: Option<[bool; 16]>,
- r_1_odd: Option<[bool; 16]>,
+ r_0_even: Value<[bool; 16]>,
+ r_0_odd: Value<[bool; 16]>,
+ r_1_even: Value<[bool; 16]>,
+ r_1_odd: Value<[bool; 16]>,
) -> Result<(AssignedBits<16>, AssignedBits<16>), Error> {
let a_3 = self.extras[0];
@@ -513,7 +512,7 @@ impl CompressionConfig {
pub(super) fn assign_ch(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
spread_halves_e: RoundWordSpread,
spread_halves_f: RoundWordSpread,
) -> Result<(AssignedBits<16>, AssignedBits<16>), Error> {
@@ -540,16 +539,16 @@ impl CompressionConfig {
.1
.copy_advice(|| "spread_f_hi", region, a_4, row + 1)?;
- let p: Option<[bool; 64]> = spread_halves_e
+ let p: Value<[bool; 64]> = spread_halves_e
.value()
.zip(spread_halves_f.value())
.map(|(e, f)| i2lebsp(e + f));
- let p_0: Option<[bool; 32]> = p.map(|p| p[..32].try_into().unwrap());
+ let p_0: Value<[bool; 32]> = p.map(|p| p[..32].try_into().unwrap());
let p_0_even = p_0.map(even_bits);
let p_0_odd = p_0.map(odd_bits);
- let p_1: Option<[bool; 32]> = p.map(|p| p[32..].try_into().unwrap());
+ let p_1: Value<[bool; 32]> = p.map(|p| p[32..].try_into().unwrap());
let p_1_even = p_1.map(even_bits);
let p_1_odd = p_1.map(odd_bits);
@@ -559,7 +558,7 @@ impl CompressionConfig {
pub(super) fn assign_ch_neg(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
spread_halves_e: RoundWordSpread,
spread_halves_g: RoundWordSpread,
) -> Result<(AssignedBits<16>, AssignedBits<16>), Error> {
@@ -615,7 +614,7 @@ impl CompressionConfig {
spread_neg_e_hi,
)?;
- let p: Option<[bool; 64]> = {
+ let p: Value<[bool; 64]> = {
let spread_neg_e = spread_neg_e_lo
.zip(spread_neg_e_hi)
.map(|(lo, hi)| lebs2ip(&lo) + (1 << 32) * lebs2ip(&hi));
@@ -624,11 +623,11 @@ impl CompressionConfig {
.map(|(neg_e, g)| i2lebsp(neg_e + g))
};
- let p_0: Option<[bool; 32]> = p.map(|p| p[..32].try_into().unwrap());
+ let p_0: Value<[bool; 32]> = p.map(|p| p[..32].try_into().unwrap());
let p_0_even = p_0.map(even_bits);
let p_0_odd = p_0.map(odd_bits);
- let p_1: Option<[bool; 32]> = p.map(|p| p[32..].try_into().unwrap());
+ let p_1: Value<[bool; 32]> = p.map(|p| p[32..].try_into().unwrap());
let p_1_even = p_1.map(even_bits);
let p_1_odd = p_1.map(odd_bits);
@@ -639,10 +638,10 @@ impl CompressionConfig {
&self,
region: &mut Region<'_, Fr>,
row: usize,
- r_0_even: Option<[bool; 16]>,
- r_0_odd: Option<[bool; 16]>,
- r_1_even: Option<[bool; 16]>,
- r_1_odd: Option<[bool; 16]>,
+ r_0_even: Value<[bool; 16]>,
+ r_0_odd: Value<[bool; 16]>,
+ r_1_even: Value<[bool; 16]>,
+ r_1_odd: Value<[bool; 16]>,
) -> Result<(AssignedBits<16>, AssignedBits<16>), Error> {
let a_3 = self.extras[0];
let (_even, odd) = self.assign_spread_outputs(
@@ -662,7 +661,7 @@ impl CompressionConfig {
pub(super) fn assign_maj(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
spread_halves_a: RoundWordSpread,
spread_halves_b: RoundWordSpread,
spread_halves_c: RoundWordSpread,
@@ -698,17 +697,17 @@ impl CompressionConfig {
.1
.copy_advice(|| "spread_c_hi", region, a_5, row + 1)?;
- let m: Option<[bool; 64]> = spread_halves_a
+ let m: Value<[bool; 64]> = spread_halves_a
.value()
.zip(spread_halves_b.value())
.zip(spread_halves_c.value())
.map(|((a, b), c)| i2lebsp(a + b + c));
- let m_0: Option<[bool; 32]> = m.map(|m| m[..32].try_into().unwrap());
+ let m_0: Value<[bool; 32]> = m.map(|m| m[..32].try_into().unwrap());
let m_0_even = m_0.map(even_bits);
let m_0_odd = m_0.map(odd_bits);
- let m_1: Option<[bool; 32]> = m.map(|m| m[32..].try_into().unwrap());
+ let m_1: Value<[bool; 32]> = m.map(|m| m[32..].try_into().unwrap());
let m_1_even = m_1.map(even_bits);
let m_1_odd = m_1.map(odd_bits);
@@ -720,7 +719,7 @@ impl CompressionConfig {
pub(super) fn assign_h_prime(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
h: RoundWordDense,
ch: (AssignedBits<16>, AssignedBits<16>),
ch_neg: (AssignedBits<16>, AssignedBits<16>),
@@ -751,8 +750,8 @@ impl CompressionConfig {
let k_lo: [bool; 16] = k[..16].try_into().unwrap();
let k_hi: [bool; 16] = k[16..].try_into().unwrap();
{
- AssignedBits::<16>::assign_bits(region, || "k_lo", a_6, row - 1, Some(k_lo))?;
- AssignedBits::<16>::assign_bits(region, || "k_hi", a_6, row, Some(k_hi))?;
+ AssignedBits::<16>::assign_bits(region, || "k_lo", a_6, row - 1, Value::known(k_lo))?;
+ AssignedBits::<16>::assign_bits(region, || "k_hi", a_6, row, Value::known(k_hi))?;
}
// Assign and copy w
@@ -773,7 +772,10 @@ impl CompressionConfig {
(ch.0.value_u16(), ch.1.value_u16()),
(ch_neg.0.value_u16(), ch_neg.1.value_u16()),
(sigma_1.0.value_u16(), sigma_1.1.value_u16()),
- (Some(lebs2ip(&k_lo) as u16), Some(lebs2ip(&k_hi) as u16)),
+ (
+ Value::known(lebs2ip(&k_lo) as u16),
+ Value::known(lebs2ip(&k_hi) as u16),
+ ),
(w.0.value_u16(), w.1.value_u16()),
]);
@@ -788,9 +790,9 @@ impl CompressionConfig {
},
)?;
- let h_prime: Option<[bool; 32]> = h_prime.map(|w| i2lebsp(w.into()));
- let h_prime_lo: Option<[bool; 16]> = h_prime.map(|w| w[..16].try_into().unwrap());
- let h_prime_hi: Option<[bool; 16]> = h_prime.map(|w| w[16..].try_into().unwrap());
+ let h_prime: Value<[bool; 32]> = h_prime.map(|w| i2lebsp(w.into()));
+ let h_prime_lo: Value<[bool; 16]> = h_prime.map(|w| w[..16].try_into().unwrap());
+ let h_prime_hi: Value<[bool; 16]> = h_prime.map(|w| w[16..].try_into().unwrap());
let h_prime_lo =
AssignedBits::<16>::assign_bits(region, || "h_prime_lo", a_7, row + 1, h_prime_lo)?;
@@ -805,7 +807,7 @@ impl CompressionConfig {
pub(super) fn assign_e_new(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
d: &RoundWordDense,
h_prime: &RoundWordDense,
) -> Result {
@@ -842,7 +844,7 @@ impl CompressionConfig {
pub(super) fn assign_a_new(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
maj: (AssignedBits<16>, AssignedBits<16>),
sigma_0: (AssignedBits<16>, AssignedBits<16>),
h_prime: RoundWordDense,
@@ -899,17 +901,17 @@ impl CompressionConfig {
lo_col: Column,
hi_row: usize,
hi_col: Column,
- word: Option,
+ word: Value,
) -> Result {
- let word: Option<[bool; 32]> = word.map(|w| i2lebsp(w.into()));
+ let word: Value<[bool; 32]> = word.map(|w| i2lebsp(w.into()));
let lo = {
- let lo: Option<[bool; 16]> = word.map(|w| w[..16].try_into().unwrap());
+ let lo: Value<[bool; 16]> = word.map(|w| w[..16].try_into().unwrap());
AssignedBits::<16>::assign_bits(region, || "lo", lo_col, lo_row, lo)?
};
let hi = {
- let hi: Option<[bool; 16]> = word.map(|w| w[16..].try_into().unwrap());
+ let hi: Value<[bool; 16]> = word.map(|w| w[16..].try_into().unwrap());
AssignedBits::<16>::assign_bits(region, || "hi", hi_col, hi_row, hi)?
};
@@ -922,15 +924,15 @@ impl CompressionConfig {
&self,
region: &mut Region<'_, Fr>,
row: usize,
- word: Option,
+ word: Value,
) -> Result<(RoundWordDense, RoundWordSpread), Error> {
// Rename these here for ease of matching the gates to the specification.
let a_7 = self.extras[3];
let a_8 = self.extras[4];
- let word: Option<[bool; 32]> = word.map(|w| i2lebsp(w.into()));
- let lo: Option<[bool; 16]> = word.map(|w| w[..16].try_into().unwrap());
- let hi: Option<[bool; 16]> = word.map(|w| w[16..].try_into().unwrap());
+ let word: Value<[bool; 32]> = word.map(|w| i2lebsp(w.into()));
+ let lo: Value<[bool; 16]> = word.map(|w| w[..16].try_into().unwrap());
+ let hi: Value<[bool; 16]> = word.map(|w| w[16..].try_into().unwrap());
let w_lo = SpreadVar::without_lookup(region, a_7, row, a_8, row, lo.map(SpreadWord::new))?;
let w_hi =
diff --git a/halo2_gadgets/src/sha256/table16/compression/subregion_digest.rs b/halo2_gadgets/src/sha256/table16/compression/subregion_digest.rs
index 69b3a8654b..988194a509 100644
--- a/halo2_gadgets/src/sha256/table16/compression/subregion_digest.rs
+++ b/halo2_gadgets/src/sha256/table16/compression/subregion_digest.rs
@@ -1,7 +1,7 @@
use super::super::{super::DIGEST_SIZE, BlockWord, RoundWordDense};
use super::{compression_util::*, CompressionConfig, State};
use halo2_proofs::{
- circuit::Region,
+circuit::{Region, Value},
pairing::bn256::Fr,
plonk::{Advice, Column, Error},
};
@@ -85,7 +85,7 @@ impl CompressionConfig {
hi_col: Column,
word_col: Column,
dense_halves: RoundWordDense,
- ) -> Result, Error> {
+ ) -> Result, Error> {
dense_halves.0.copy_advice(|| "lo", region, lo_col, row)?;
dense_halves.1.copy_advice(|| "hi", region, hi_col, row)?;
diff --git a/halo2_gadgets/src/sha256/table16/compression/subregion_initial.rs b/halo2_gadgets/src/sha256/table16/compression/subregion_initial.rs
index 0df23b8609..19331002c3 100644
--- a/halo2_gadgets/src/sha256/table16/compression/subregion_initial.rs
+++ b/halo2_gadgets/src/sha256/table16/compression/subregion_initial.rs
@@ -1,6 +1,6 @@
use super::super::{RoundWord, StateWord, STATE};
use super::{compression_util::*, CompressionConfig, State};
-use halo2_proofs::{circuit::Region, pairing::bn256::Fr, plonk::Error};
+use halo2_proofs::{circuit::{Region, Value}, pairing::bn256::Fr, plonk::Error};
impl CompressionConfig {
#[allow(clippy::many_single_char_names)]
@@ -12,26 +12,28 @@ impl CompressionConfig {
let a_7 = self.extras[3];
// Decompose E into (6, 5, 14, 7)-bit chunks
- let e = self.decompose_e(region, RoundIdx::Init, Some(iv[4]))?;
+ let e = self.decompose_e(region, RoundIdx::Init, Value::known(iv[4]))?;
// Decompose F, G
- let f = self.decompose_f(region, RoundIdx::Init, Some(iv[5]))?;
- let g = self.decompose_g(region, RoundIdx::Init, Some(iv[6]))?;
+ let f = self.decompose_f(region, InitialRound, Value::known(iv[5]))?;
+ let g = self.decompose_g(region, InitialRound, Value::known(iv[6]))?;
// Assign H
let h_row = get_h_row(RoundIdx::Init);
- let h = self.assign_word_halves_dense(region, h_row, a_7, h_row + 1, a_7, Some(iv[7]))?;
+ let h =
+ self.assign_word_halves_dense(region, h_row, a_7, h_row + 1, a_7, Value::known(iv[7]))?;
// Decompose A into (2, 11, 9, 10)-bit chunks
- let a = self.decompose_a(region, RoundIdx::Init, Some(iv[0]))?;
+ let a = self.decompose_a(region, RoundIdx::Init, Value::known(iv[0]))?;
// Decompose B, C
- let b = self.decompose_b(region, RoundIdx::Init, Some(iv[1]))?;
- let c = self.decompose_c(region, RoundIdx::Init, Some(iv[2]))?;
+ let b = self.decompose_b(region, InitialRound, Value::known(iv[1]))?;
+ let c = self.decompose_c(region, InitialRound, Value::known(iv[2]))?;
// Assign D
let d_row = get_d_row(RoundIdx::Init);
- let d = self.assign_word_halves_dense(region, d_row, a_7, d_row + 1, a_7, Some(iv[3]))?;
+ let d =
+ self.assign_word_halves_dense(region, d_row, a_7, d_row + 1, a_7, Value::known(iv[3]))?;
Ok(State::new(
StateWord::A(a),
@@ -60,9 +62,9 @@ impl CompressionConfig {
// Decompose F, G
let f = f.dense_halves.value();
- let f = self.decompose_f(region, RoundIdx::Init, f)?;
+ let f = self.decompose_f(region, InitialRound, f)?;
let g = g.dense_halves.value();
- let g = self.decompose_g(region, RoundIdx::Init, g)?;
+ let g = self.decompose_g(region, InitialRound, g)?;
// Assign H
let h = h.value();
@@ -75,9 +77,9 @@ impl CompressionConfig {
// Decompose B, C
let b = b.dense_halves.value();
- let b = self.decompose_b(region, RoundIdx::Init, b)?;
+ let b = self.decompose_b(region, InitialRound, b)?;
let c = c.dense_halves.value();
- let c = self.decompose_c(region, RoundIdx::Init, c)?;
+ let c = self.decompose_c(region, InitialRound, c)?;
// Assign D
let d = d.value();
@@ -99,8 +101,8 @@ impl CompressionConfig {
fn decompose_b(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
- b_val: Option,
+ round_idx: InitialRound,
+ b_val: Value,
) -> Result {
let row = get_decompose_b_row(round_idx);
@@ -112,8 +114,8 @@ impl CompressionConfig {
fn decompose_c(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
- c_val: Option,
+ round_idx: InitialRound,
+ c_val: Value,
) -> Result {
let row = get_decompose_c_row(round_idx);
@@ -125,8 +127,8 @@ impl CompressionConfig {
fn decompose_f(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
- f_val: Option,
+ round_idx: InitialRound,
+ f_val: Value,
) -> Result {
let row = get_decompose_f_row(round_idx);
@@ -138,8 +140,8 @@ impl CompressionConfig {
fn decompose_g(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
- g_val: Option,
+ round_idx: InitialRound,
+ g_val: Value,
) -> Result {
let row = get_decompose_g_row(round_idx);
diff --git a/halo2_gadgets/src/sha256/table16/compression/subregion_main.rs b/halo2_gadgets/src/sha256/table16/compression/subregion_main.rs
index 8faf1e2194..719400c59a 100644
--- a/halo2_gadgets/src/sha256/table16/compression/subregion_main.rs
+++ b/halo2_gadgets/src/sha256/table16/compression/subregion_main.rs
@@ -7,12 +7,10 @@ impl CompressionConfig {
pub fn assign_round(
&self,
region: &mut Region<'_, Fr>,
- round_idx: RoundIdx,
+ round_idx: MainRoundIdx,
state: State,
schedule_word: &(AssignedBits<16>, AssignedBits<16>),
) -> Result {
- assert!(matches!(round_idx, RoundIdx::Main(_)));
-
let a_3 = self.extras[0];
let a_4 = self.extras[1];
let a_7 = self.extras[3];
@@ -70,7 +68,7 @@ impl CompressionConfig {
if round_idx < 63.into() {
// Assign and copy A_new
- let a_new_row = get_decompose_a_row(round_idx + 1);
+ let a_new_row = get_decompose_a_row((round_idx + 1).into());
a_new_dense
.0
.copy_advice(|| "a_new_lo", region, a_7, a_new_row)?;
@@ -79,7 +77,7 @@ impl CompressionConfig {
.copy_advice(|| "a_new_hi", region, a_7, a_new_row + 1)?;
// Assign and copy E_new
- let e_new_row = get_decompose_e_row(round_idx + 1);
+ let e_new_row = get_decompose_e_row((round_idx + 1).into());
e_new_dense
.0
.copy_advice(|| "e_new_lo", region, a_7, e_new_row)?;
@@ -88,10 +86,10 @@ impl CompressionConfig {
.copy_advice(|| "e_new_hi", region, a_7, e_new_row + 1)?;
// Decompose A into (2, 11, 9, 10)-bit chunks
- let a_new = self.decompose_a(region, round_idx + 1, a_new_val)?;
+ let a_new = self.decompose_a(region, (round_idx + 1).into(), a_new_val)?;
// Decompose E into (6, 5, 14, 7)-bit chunks
- let e_new = self.decompose_e(region, round_idx + 1, e_new_val)?;
+ let e_new = self.decompose_e(region, (round_idx + 1).into(), e_new_val)?;
Ok(State::new(
StateWord::A(a_new),
diff --git a/halo2_gadgets/src/sha256/table16/message_schedule.rs b/halo2_gadgets/src/sha256/table16/message_schedule.rs
index cf7c2b1812..52d68a1cc2 100644
--- a/halo2_gadgets/src/sha256/table16/message_schedule.rs
+++ b/halo2_gadgets/src/sha256/table16/message_schedule.rs
@@ -435,8 +435,10 @@ mod tests {
// Run message_scheduler to get W_[0..64]
let (w, _) = config.message_schedule.process(&mut layouter, inputs)?;
for (word, test_word) in w.iter().zip(MSG_SCHEDULE_TEST_OUTPUT.iter()) {
- let word: u32 = lebs2ip(&word.value().unwrap()) as u32;
- assert_eq!(word, *test_word);
+ word.value().assert_if_known(|bits| {
+ let word: u32 = lebs2ip(bits) as u32;
+ word == *test_word
+ });
}
Ok(())
}
diff --git a/halo2_gadgets/src/sha256/table16/message_schedule/schedule_gates.rs b/halo2_gadgets/src/sha256/table16/message_schedule/schedule_gates.rs
index 52d58bd0b1..fab51bd373 100644
--- a/halo2_gadgets/src/sha256/table16/message_schedule/schedule_gates.rs
+++ b/halo2_gadgets/src/sha256/table16/message_schedule/schedule_gates.rs
@@ -1,6 +1,6 @@
use super::super::Gate;
use halo2_proofs::{arithmetic::FieldExt, plonk::Expression};
-use std::{array, marker::PhantomData};
+use std::marker::PhantomData;
pub struct ScheduleGate(PhantomData);
@@ -29,7 +29,8 @@ impl ScheduleGate {
+ (word * (-F::one()));
let carry_check = Gate::range_check(carry, 0, 3);
- array::IntoIter::new([("word_check", word_check), ("carry_check", carry_check)])
+ [("word_check", word_check), ("carry_check", carry_check)]
+ .into_iter()
.map(move |(name, poly)| (name, s_word.clone() * poly))
}
@@ -39,9 +40,9 @@ impl ScheduleGate {
lo: Expression,
hi: Expression,
word: Expression,
- ) -> impl Iterator- )> {
+ ) -> Option<(&'static str, Expression
)> {
let check = lo + hi * F::from(1 << 16) - word;
- std::iter::empty().chain(Some(("s_decompose_0", s_decompose_0 * check)))
+ Some(("s_decompose_0", s_decompose_0 * check))
}
/// s_decompose_1 for W_1 to W_13
@@ -65,11 +66,12 @@ impl ScheduleGate {
let range_check_tag_c = Gate::range_check(tag_c, 0, 2);
let range_check_tag_d = Gate::range_check(tag_d, 0, 4);
- array::IntoIter::new([
+ [
("decompose_check", decompose_check),
("range_check_tag_c", range_check_tag_c),
("range_check_tag_d", range_check_tag_d),
- ])
+ ]
+ .into_iter()
.map(move |(name, poly)| (name, s_decompose_1.clone() * poly))
}
@@ -101,11 +103,12 @@ impl ScheduleGate {
let range_check_tag_d = Gate::range_check(tag_d, 0, 0);
let range_check_tag_g = Gate::range_check(tag_g, 0, 3);
- array::IntoIter::new([
+ [
("decompose_check", decompose_check),
("range_check_tag_g", range_check_tag_g),
("range_check_tag_d", range_check_tag_d),
- ])
+ ]
+ .into_iter()
.map(move |(name, poly)| (name, s_decompose_2.clone() * poly))
}
@@ -130,11 +133,12 @@ impl ScheduleGate {
let range_check_tag_a = Gate::range_check(tag_a, 0, 1);
let range_check_tag_d = Gate::range_check(tag_d, 0, 3);
- array::IntoIter::new([
+ [
("decompose_check", decompose_check),
("range_check_tag_a", range_check_tag_a),
("range_check_tag_d", range_check_tag_d),
- ])
+ ]
+ .into_iter()
.map(move |(name, poly)| (name, s_decompose_3.clone() * poly))
}
diff --git a/halo2_gadgets/src/sha256/table16/message_schedule/schedule_util.rs b/halo2_gadgets/src/sha256/table16/message_schedule/schedule_util.rs
index 7fd25bc1bd..dc20bbdc4d 100644
--- a/halo2_gadgets/src/sha256/table16/message_schedule/schedule_util.rs
+++ b/halo2_gadgets/src/sha256/table16/message_schedule/schedule_util.rs
@@ -1,6 +1,6 @@
use super::super::AssignedBits;
use super::MessageScheduleConfig;
-use halo2_proofs::{circuit::Region, pairing::bn256::Fr, plonk::Error};
+use halo2_proofs::{circuit::{Region, Value}, pairing::bn256::Fr, plonk::Error};
#[cfg(test)]
use super::super::{super::BLOCK_SIZE, BlockWord, ROUNDS};
@@ -57,22 +57,22 @@ pub fn get_word_row(word_idx: usize) -> usize {
#[cfg(test)]
pub fn msg_schedule_test_input() -> [BlockWord; BLOCK_SIZE] {
[
- BlockWord(Some(0b01100001011000100110001110000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000000000)),
- BlockWord(Some(0b00000000000000000000000000011000)),
+ BlockWord(Value::known(0b01100001011000100110001110000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000000000)),
+ BlockWord(Value::known(0b00000000000000000000000000011000)),
]
}
@@ -149,7 +149,7 @@ impl MessageScheduleConfig {
pub fn assign_word_and_halves(
&self,
region: &mut Region<'_, Fr>,
- word: Option,
+ word: Value,
word_idx: usize,
) -> Result<(AssignedBits<32>, (AssignedBits<16>, AssignedBits<16>)), Error> {
// Rename these here for ease of matching the gates to the specification.
diff --git a/halo2_gadgets/src/sha256/table16/message_schedule/subregion1.rs b/halo2_gadgets/src/sha256/table16/message_schedule/subregion1.rs
index 01a165e3cb..1a58cf917d 100644
--- a/halo2_gadgets/src/sha256/table16/message_schedule/subregion1.rs
+++ b/halo2_gadgets/src/sha256/table16/message_schedule/subregion1.rs
@@ -1,6 +1,6 @@
use super::super::{util::*, AssignedBits, BlockWord, SpreadVar, SpreadWord, Table16Assignment};
use super::{schedule_util::*, MessageScheduleConfig};
-use halo2_proofs::{circuit::Region, pairing::bn256::Fr, plonk::Error};
+use halo2_proofs::{circuit::{Region, Value}, pairing::bn256::Fr, plonk::Error};
use std::convert::TryInto;
// A word in subregion 1
@@ -17,23 +17,23 @@ pub struct Subregion1Word {
}
impl Subregion1Word {
- fn spread_a(&self) -> Option<[bool; 6]> {
+ fn spread_a(&self) -> Value<[bool; 6]> {
self.a.value().map(|v| v.spread())
}
- fn spread_b(&self) -> Option<[bool; 8]> {
+ fn spread_b(&self) -> Value<[bool; 8]> {
self.b.value().map(|v| v.spread())
}
- fn spread_c(&self) -> Option<[bool; 22]> {
+ fn spread_c(&self) -> Value<[bool; 22]> {
self.spread_c.value().map(|v| v.0)
}
- fn spread_d(&self) -> Option<[bool; 28]> {
+ fn spread_d(&self) -> Value<[bool; 28]> {
self.spread_d.value().map(|v| v.0)
}
- fn xor_lower_sigma_0(&self) -> Option<[bool; 64]> {
+ fn xor_lower_sigma_0(&self) -> Value<[bool; 64]> {
self.spread_a()
.zip(self.spread_b())
.zip(self.spread_c())
@@ -100,7 +100,7 @@ impl MessageScheduleConfig {
fn decompose_subregion1_word(
&self,
region: &mut Region<'_, Fr>,
- word: Option<[bool; 32]>,
+ word: Value<[bool; 32]>,
index: usize,
) -> Result {
let row = get_word_row(index);
@@ -117,7 +117,7 @@ impl MessageScheduleConfig {
word[18..32].to_vec(),
]
});
- let pieces = transpose_option_vec(pieces, 4);
+ let pieces = pieces.transpose_vec(4);
// Assign `a` (3-bit piece)
let a =
@@ -168,7 +168,7 @@ impl MessageScheduleConfig {
// Split `b` (4-bit chunk) into `b_hi` and `b_lo`
// Assign `b_lo`, `spread_b_lo`
- let b_lo: Option<[bool; 2]> = word.b.value().map(|b| b.0[..2].try_into().unwrap());
+ let b_lo: Value<[bool; 2]> = word.b.value().map(|b| b.0[..2].try_into().unwrap());
let spread_b_lo = b_lo.map(spread_bits);
{
AssignedBits::<2>::assign_bits(region, || "b_lo", a_3, row - 1, b_lo)?;
@@ -178,7 +178,7 @@ impl MessageScheduleConfig {
// Split `b` (2-bit chunk) into `b_hi` and `b_lo`
// Assign `b_hi`, `spread_b_hi`
- let b_hi: Option<[bool; 2]> = word.b.value().map(|b| b.0[2..].try_into().unwrap());
+ let b_hi: Value<[bool; 2]> = word.b.value().map(|b| b.0[2..].try_into().unwrap());
let spread_b_hi = b_hi.map(spread_bits);
{
AssignedBits::<2>::assign_bits(region, || "b_hi", a_5, row - 1, b_hi)?;
@@ -197,11 +197,11 @@ impl MessageScheduleConfig {
// Calculate R_0^{even}, R_0^{odd}, R_1^{even}, R_1^{odd}
let r = word.xor_lower_sigma_0();
- let r_0: Option<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
+ let r_0: Value<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
let r_0_even = r_0.map(even_bits);
let r_0_odd = r_0.map(odd_bits);
- let r_1: Option<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
+ let r_1: Value<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
let r_1_even = r_1.map(even_bits);
let r_1_odd = r_1.map(odd_bits);
diff --git a/halo2_gadgets/src/sha256/table16/message_schedule/subregion2.rs b/halo2_gadgets/src/sha256/table16/message_schedule/subregion2.rs
index 77622b56f0..62cd428599 100644
--- a/halo2_gadgets/src/sha256/table16/message_schedule/subregion2.rs
+++ b/halo2_gadgets/src/sha256/table16/message_schedule/subregion2.rs
@@ -1,6 +1,6 @@
use super::super::{util::*, AssignedBits, Bits, SpreadVar, SpreadWord, Table16Assignment};
use super::{schedule_util::*, MessageScheduleConfig, MessageWord};
-use halo2_proofs::{circuit::Region, pairing::bn256::Fr, plonk::Error};
+use halo2_proofs::{circuit::{Region, Value}, pairing::bn256::Fr, plonk::Error};
use std::convert::TryInto;
/// A word in subregion 2
@@ -20,35 +20,35 @@ pub struct Subregion2Word {
}
impl Subregion2Word {
- fn spread_a(&self) -> Option<[bool; 6]> {
+ fn spread_a(&self) -> Value<[bool; 6]> {
self.a.value().map(|v| v.spread())
}
- fn spread_b(&self) -> Option<[bool; 8]> {
+ fn spread_b(&self) -> Value<[bool; 8]> {
self.b.value().map(|v| v.spread())
}
- fn spread_c(&self) -> Option<[bool; 6]> {
+ fn spread_c(&self) -> Value<[bool; 6]> {
self.c.value().map(|v| v.spread())
}
- fn spread_d(&self) -> Option<[bool; 14]> {
+ fn spread_d(&self) -> Value<[bool; 14]> {
self.spread_d.value().map(|v| v.0)
}
- fn spread_e(&self) -> Option<[bool; 2]> {
+ fn spread_e(&self) -> Value<[bool; 2]> {
self.e.value().map(|v| v.spread())
}
- fn spread_f(&self) -> Option<[bool; 2]> {
+ fn spread_f(&self) -> Value<[bool; 2]> {
self.f.value().map(|v| v.spread())
}
- fn spread_g(&self) -> Option<[bool; 26]> {
+ fn spread_g(&self) -> Value<[bool; 26]> {
self.spread_g.value().map(|v| v.0)
}
- fn xor_sigma_0(&self) -> Option<[bool; 64]> {
+ fn xor_sigma_0(&self) -> Value<[bool; 64]> {
self.spread_a()
.zip(self.spread_b())
.zip(self.spread_c())
@@ -98,7 +98,7 @@ impl Subregion2Word {
})
}
- fn xor_sigma_1(&self) -> Option<[bool; 64]> {
+ fn xor_sigma_1(&self) -> Value<[bool; 64]> {
self.spread_a()
.zip(self.spread_b())
.zip(self.spread_c())
@@ -260,11 +260,7 @@ impl MessageScheduleConfig {
|| format!("carry_{}", new_word_idx),
a_9,
get_word_row(new_word_idx - 16) + 1,
- || {
- carry
- .map(|carry| Fr::from(carry as u64))
- .ok_or(Error::Synthesis)
- },
+ || carry.map(|carry| Fr::from(carry as u64)),
)?;
let (word, halves) = self.assign_word_and_halves(region, word, new_word_idx)?;
w.push(MessageWord(word));
@@ -294,7 +290,7 @@ impl MessageScheduleConfig {
fn decompose_word(
&self,
region: &mut Region<'_, Fr>,
- word: Option<&Bits<32>>,
+ word: Value<&Bits<32>>,
index: usize,
) -> Result {
let row = get_word_row(index);
@@ -310,7 +306,7 @@ impl MessageScheduleConfig {
word[19..32].to_vec(),
]
});
- let pieces = transpose_option_vec(pieces, 7);
+ let pieces = pieces.transpose_vec(7);
// Rename these here for ease of matching the gates to the specification.
let a_3 = self.extras[0];
@@ -320,14 +316,14 @@ impl MessageScheduleConfig {
let a = AssignedBits::<3>::assign_bits(region, || "a", a_3, row - 1, pieces[0].clone())?;
// Assign `b` (4-bit piece) lookup
- let spread_b: Option> = pieces[1].clone().map(SpreadWord::try_new);
+ let spread_b: Value> = pieces[1].clone().map(SpreadWord::try_new);
let spread_b = SpreadVar::with_lookup(region, &self.lookup, row + 1, spread_b)?;
// Assign `c` (3-bit piece)
let c = AssignedBits::<3>::assign_bits(region, || "c", a_4, row - 1, pieces[2].clone())?;
// Assign `d` (7-bit piece) lookup
- let spread_d: Option> = pieces[3].clone().map(SpreadWord::try_new);
+ let spread_d: Value> = pieces[3].clone().map(SpreadWord::try_new);
let spread_d = SpreadVar::with_lookup(region, &self.lookup, row, spread_d)?;
// Assign `e` (1-bit piece)
@@ -378,7 +374,7 @@ impl MessageScheduleConfig {
// Split `b` (4-bit chunk) into `b_hi` and `b_lo`
// Assign `b_lo`, `spread_b_lo`
- let b_lo: Option<[bool; 2]> = word.b.value().map(|b| b.0[..2].try_into().unwrap());
+ let b_lo: Value<[bool; 2]> = word.b.value().map(|b| b.0[..2].try_into().unwrap());
let spread_b_lo = b_lo.map(spread_bits);
{
AssignedBits::<2>::assign_bits(region, || "b_lo", a_3, row - 1, b_lo)?;
@@ -388,7 +384,7 @@ impl MessageScheduleConfig {
// Split `b` (2-bit chunk) into `b_hi` and `b_lo`
// Assign `b_hi`, `spread_b_hi`
- let b_hi: Option<[bool; 2]> = word.b.value().map(|b| b.0[2..].try_into().unwrap());
+ let b_hi: Value<[bool; 2]> = word.b.value().map(|b| b.0[2..].try_into().unwrap());
let spread_b_hi = b_hi.map(spread_bits);
{
AssignedBits::<2>::assign_bits(region, || "b_hi", a_5, row - 1, b_hi)?;
@@ -433,11 +429,11 @@ impl MessageScheduleConfig {
// Calculate R_0^{even}, R_0^{odd}, R_1^{even}, R_1^{odd}
let r = word.xor_sigma_0();
- let r_0: Option<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
+ let r_0: Value<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
let r_0_even = r_0.map(even_bits);
let r_0_odd = r_0.map(odd_bits);
- let r_1: Option<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
+ let r_1: Value<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
let r_1_even = r_1.map(even_bits);
let r_1_odd = r_1.map(odd_bits);
@@ -468,11 +464,11 @@ impl MessageScheduleConfig {
// Calculate R_0^{even}, R_0^{odd}, R_1^{even}, R_1^{odd}
// Calculate R_0^{even}, R_0^{odd}, R_1^{even}, R_1^{odd}
let r = word.xor_sigma_1();
- let r_0: Option<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
+ let r_0: Value<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
let r_0_even = r_0.map(even_bits);
let r_0_odd = r_0.map(odd_bits);
- let r_1: Option<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
+ let r_1: Value<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
let r_1_even = r_1.map(even_bits);
let r_1_odd = r_1.map(odd_bits);
diff --git a/halo2_gadgets/src/sha256/table16/message_schedule/subregion3.rs b/halo2_gadgets/src/sha256/table16/message_schedule/subregion3.rs
index 3f0985e981..8894bca2d2 100644
--- a/halo2_gadgets/src/sha256/table16/message_schedule/subregion3.rs
+++ b/halo2_gadgets/src/sha256/table16/message_schedule/subregion3.rs
@@ -1,6 +1,6 @@
use super::super::{util::*, AssignedBits, Bits, SpreadVar, SpreadWord, Table16Assignment};
use super::{schedule_util::*, MessageScheduleConfig, MessageWord};
-use halo2_proofs::{circuit::Region, pairing::bn256::Fr, plonk::Error};
+use halo2_proofs::{circuit::{Region, Value}, pairing::bn256::Fr, plonk::Error};
use std::convert::TryInto;
// A word in subregion 3
@@ -18,23 +18,23 @@ pub struct Subregion3Word {
}
impl Subregion3Word {
- fn spread_a(&self) -> Option<[bool; 20]> {
+ fn spread_a(&self) -> Value<[bool; 20]> {
self.spread_a.value().map(|v| v.0)
}
- fn spread_b(&self) -> Option<[bool; 14]> {
+ fn spread_b(&self) -> Value<[bool; 14]> {
self.b.value().map(|v| v.spread())
}
- fn spread_c(&self) -> Option<[bool; 4]> {
+ fn spread_c(&self) -> Value<[bool; 4]> {
self.c.value().map(|v| v.spread())
}
- fn spread_d(&self) -> Option<[bool; 26]> {
+ fn spread_d(&self) -> Value<[bool; 26]> {
self.spread_d.value().map(|v| v.0)
}
- fn xor_lower_sigma_1(&self) -> Option<[bool; 64]> {
+ fn xor_lower_sigma_1(&self) -> Value<[bool; 64]> {
self.spread_a()
.zip(self.spread_b())
.zip(self.spread_c())
@@ -167,20 +167,13 @@ impl MessageScheduleConfig {
|| format!("W_{}", new_word_idx),
a_5,
get_word_row(new_word_idx - 16) + 1,
- || {
- word.map(|word| Fr::from(word as u64))
- .ok_or(Error::Synthesis)
- },
+ || word.map(|word| Fr::from(word as u64)),
)?;
region.assign_advice(
|| format!("carry_{}", new_word_idx),
a_9,
get_word_row(new_word_idx - 16) + 1,
- || {
- carry
- .map(|carry| Fr::from(carry as u64))
- .ok_or(Error::Synthesis)
- },
+ || carry.map(|carry| Fr::from(carry as u64)),
)?;
let (word, halves) = self.assign_word_and_halves(region, word, new_word_idx)?;
w.push(MessageWord(word));
@@ -200,7 +193,7 @@ impl MessageScheduleConfig {
fn decompose_subregion3_word(
&self,
region: &mut Region<'_, Fr>,
- word: Option<&Bits<32>>,
+ word: Value<&Bits<32>>,
index: usize,
) -> Result {
let row = get_word_row(index);
@@ -217,7 +210,7 @@ impl MessageScheduleConfig {
word[19..32].to_vec(),
]
});
- let pieces = transpose_option_vec(pieces, 4);
+ let pieces = pieces.transpose_vec(4);
// Assign `a` (10-bit piece)
let spread_a = pieces[0].clone().map(SpreadWord::try_new);
@@ -264,21 +257,21 @@ impl MessageScheduleConfig {
// b_lo (2-bit chunk)
{
- let b_lo: Option<[bool; 2]> = word.b.value().map(|v| v[0..2].try_into().unwrap());
+ let b_lo: Value<[bool; 2]> = word.b.value().map(|v| v[0..2].try_into().unwrap());
let b_lo = b_lo.map(SpreadWord::<2, 4>::new);
SpreadVar::without_lookup(region, a_3, row - 1, a_4, row - 1, b_lo)?;
}
// b_mid (2-bit chunk)
{
- let b_mid: Option<[bool; 2]> = word.b.value().map(|v| v[2..4].try_into().unwrap());
+ let b_mid: Value<[bool; 2]> = word.b.value().map(|v| v[2..4].try_into().unwrap());
let b_mid = b_mid.map(SpreadWord::<2, 4>::new);
SpreadVar::without_lookup(region, a_5, row - 1, a_6, row - 1, b_mid)?;
}
// b_hi (3-bit chunk)
{
- let b_hi: Option<[bool; 3]> = word.b.value().map(|v| v[4..7].try_into().unwrap());
+ let b_hi: Value<[bool; 3]> = word.b.value().map(|v| v[4..7].try_into().unwrap());
let b_hi = b_hi.map(SpreadWord::<3, 6>::new);
SpreadVar::without_lookup(region, a_5, row + 1, a_6, row + 1, b_hi)?;
}
@@ -301,11 +294,11 @@ impl MessageScheduleConfig {
// (10, 7, 2, 13)
// Calculate R_0^{even}, R_0^{odd}, R_1^{even}, R_1^{odd}
let r = word.xor_lower_sigma_1();
- let r_0: Option<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
+ let r_0: Value<[bool; 32]> = r.map(|r| r[..32].try_into().unwrap());
let r_0_even = r_0.map(even_bits);
let r_0_odd = r_0.map(odd_bits);
- let r_1: Option<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
+ let r_1: Value<[bool; 32]> = r.map(|r| r[32..].try_into().unwrap());
let r_1_even = r_1.map(even_bits);
let r_1_odd = r_1.map(odd_bits);
diff --git a/halo2_gadgets/src/sha256/table16/spread_table.rs b/halo2_gadgets/src/sha256/table16/spread_table.rs
index 870e9b01be..29413a7ef7 100644
--- a/halo2_gadgets/src/sha256/table16/spread_table.rs
+++ b/halo2_gadgets/src/sha256/table16/spread_table.rs
@@ -1,7 +1,7 @@
use super::{util::*, AssignedBits};
use halo2_proofs::{
arithmetic::FieldExt,
- circuit::{Chip, Layouter, Region},
+ circuit::{Chip, Layouter, Region, Value},
pairing::bn256::Fr,
plonk::{Advice, Column, ConstraintSystem, Error, TableColumn},
poly::Rotation,
@@ -68,7 +68,7 @@ impl SpreadWord {
/// A variable stored in advice columns corresponding to a row of [`SpreadTableConfig`].
#[derive(Clone, Debug)]
pub(super) struct SpreadVar {
- pub tag: Option,
+ pub tag: Value,
pub dense: AssignedBits,
pub spread: AssignedBits,
}
@@ -78,7 +78,7 @@ impl SpreadVar {
region: &mut Region<'_, Fr>,
cols: &SpreadInputs,
row: usize,
- word: Option>,
+ word: Value>,
) -> Result {
let tag = word.map(|word| word.tag);
let dense_val = word.map(|word| word.dense);
@@ -88,7 +88,7 @@ impl SpreadVar {
|| "tag",
cols.tag,
row,
- || tag.map(|tag| Fr::from(tag as u64)).ok_or(Error::Synthesis),
+ || tag.map(|tag| Fr::from(tag as u64)),
)?;
let dense =
@@ -106,7 +106,7 @@ impl SpreadVar {
dense_row: usize,
spread_col: Column,
spread_row: usize,
- word: Option 
| Since $G$ is a commitment, it can be checked in an inner product argument. The verifier circuit witnesses $G$ and brings $G, u_1, \cdots, u_k$ out as public inputs to the proof $\pi.$ The next verifier instance checks $\pi$ using the inner product argument; this includes checking that $G = \text{Commit}(g(X, u_1, \cdots, u_k))$ evaluates at some random point to the expected value for the given challenges $u_1, \cdots, u_k.$ Recall from the [previous section](#Polynomial-commitment-using-inner-product-argument) that this check only requires $\log d$ work.