diff --git a/book/src/design/gadgets/decomposition.md b/book/src/design/gadgets/decomposition.md
index c8f3f00fa..08a5d6116 100644
--- a/book/src/design/gadgets/decomposition.md
+++ b/book/src/design/gadgets/decomposition.md
@@ -1,12 +1,17 @@
# Decomposition and range checking
-This chapter describes gadgets for decomposing a field element into windows of $K$-bits, and checking that a field element is less than a given power of 2.
+This chapter describes gadgets for
-> Note: the $K$ mentioned above is fixed to $K = 10$, since the Orchard circuit has $2^{11}$ rows, and $10$ is the largest integer less than $11$. There is one $2^{10}$ row lookup table in the circuit, which is used to implement the window checks. It could change in the future, but there is much code that assumes $K = 10$ that would need to be updated.
+- decomposing a field element into the high $(N-K)$ bits and low $K$ bits, for $K$ arbitrary and $N$ the bit-width of the field
+- decomposing a field element into windows of $T_\mathcal{O}$ bits, for $T_\mathcal{O} = 10$ in practice
+- checking that a field element is less than $2^n$, for $n$ arbitrary
+- checking that a field element is less than another arbitrary field element
+
+> Note: the $T_\mathcal{O}$ mentioned above is fixed to $T_\mathcal{O} = 10$ in practice, because behind the scenes there is a $2^{T_\mathcal{O}}$ row table, and since the Orchard circuit has $2^{11}$ rows, $T_\mathcal{O} = 10$ is the largest value for which the lookup table will fit. The $T_\mathcal{O}$ could change in the future, but there is much code that assumes it's 10 that would need to be updated. In the code, $T_\mathcal{O}$ is referred to as `sinsemilla::K`.
-## Generic range checking
+## Generic range checking
The `generic_range_check::Config` provides a function
@@ -32,7 +37,7 @@ The constraint complexity of the generic `range_check` is one degree-2 equality
-## Power-of-2 range checking
+## Power-of-2 range checking
The `pow2_range_check::Config` provides a function
@@ -40,41 +45,129 @@ $$
\texttt{pow2\_range\_check}(x{:}~\texttt{AssignedCell<}\mathbb{F}_p\texttt{>}, n{:}~\texttt{usize}, strict{:}~\texttt{bool})
$$
-that returns an $\texttt{AssignedCell<}\mathbb{F}_p\texttt{>}$ value that is constrained to be zero when $x \in [0, 2^n),$ where $2^n \lt p$ is asserted internally; if $strict == \texttt{true},$ then the gadget will enforce this zero check as well. Internally the `pow2_range_check` works by decomposing $n = q \cdot K + r,$ and using the windowed decomposition and short range check gadgets described below to compute something analogous to $x \gg n$ as $(x \gg q\cdot K) \gg r$.
+that returns an $\texttt{AssignedCell<}\mathbb{F}_p\texttt{>}$ value that is constrained to be zero when $x \in [0, 2^n),$ where $2^n \lt p$ is asserted internally; if $strict == \texttt{true},$ then the gadget will enforce this zero check as well. Internally the `pow2_range_check` works by decomposing $n = q \cdot T_\mathcal{O} + r,$ and using the windowed decomposition and short range check gadgets described below to compute something analogous to $x \gg n$ as $(x \gg q\cdot T_\mathcal{O}) \gg r$. Here $T_\mathcal{O}$ is fixed to the bit-width of the lookup table, i.e. 10 in practice.
+
+The constraint complexity of the `pow2_range_check` is one degree-2 equality check, plus the underlying constraint complexity of a non-strict $q$-window decomposition, and an $r$-bit short range check. However, it's optimized to avoid the window decomposition when $q = 0,$ and to avoid the short range check when $r = 0$. Altogether, this amounts to $q + 2 \cdot r$ lookups of a degree-3 expression in a $2^{T_\mathcal{O}}$-bit lookup table, and roughly $q + r + 1$ degree-2 equality constraints.
+
+## High-low Decomposition
+
+Here we describe $K$-high-low decomposition and range checking. First we look at the special case of $K = 1$ to build intuition, then we consider the generalization to arbitrary $K$, and finally we describe the constraint encoding of the range check.
+
+The decomposition and canonical range checking described here are implemented in the `halo2_gadgets::utilities::high_low_decomp` module.
+
+### The $K = 1$ Case
+
+Consider the problem of representing a scalar field scalar $\alpha$ in the base field, when the scalar field modulus $q$ is larger than the base field modulus $p$, and so the scalar field is not a subset of the base field. Because we deal with curves where the scalar and base fields are the same bit width, it's sufficient to break $\alpha$ up into high and low parts $\alpha \gg 1$ and $\alpha \& 1$, which we call $\alpha_0$. In order to ensure that the decomposition of $\alpha$ into $(\alpha \gg 1, \alpha_0)$ was done correctly, we implement a range check on the decomposition. The intuition is that we want to ensure that the decomposition is "canonical", i.e. that it doesn't rely on wraparound mod $q$.
+
+It turns out not all such decompositions are canonical, i.e. it's not sufficient to simply check that a given $h$ and $\ell$ satisfy $\alpha = 2h + \ell$. Suppose $\alpha \in [0, q)$ and we wish to find $h$ and $\ell$ s.t. $\alpha = 2h + \ell$ as integers, and $\ell \in \{0, 1\}.$ However, we must verify the decomposition in a circuit, and so we can only check our equations modulo the base field of our circuit. In modular arithmetic, the equation $\alpha = 2h + \ell$ with $\ell \in \{0, 1\}$ always has two solutions mod $q$, namely
+
+
+$$
+(h, \ell) = (\alpha \gg 1, \alpha_0),
+$$
+
+and
+
+$$
+(h, \ell) = ((\alpha \gg 1) + (q + 2\alpha_0 - 1)/2, 1 - \alpha_0).
+$$
+
+We need to find the first solution, which we call the "canonical" solution, since for that solution $\alpha$ and $2h + \ell$ are equal as integers. For the canonical solution, we have $h \in [0, (q-1)/2)$, except when $\alpha = q-1$, in which case the solution is $h = (q-1)/2$ and $\ell = 0$; when $\ell = 1$ and $h = (q-1)/2$, we get a non-canonical solution to the equation $0 = 2h + \ell \bmod q$, so we can't allow solutions with $h = (q-1)/2$ generally. So, to enforce canonicality, we check that
+
+$$
+h \in [0,(q-1)/2]
+$$
+
+and
+
+$$
+(h = (q-1)/2) \implies (\ell = 0).
+$$
+
+### Decomposition for general $K$
+
+Fix an elliptic curve $C$ and let $\mathbb{F}_b$ and $\mathbb{F}_s$ denote $C$'s base and scalar fields, respectively. Let $m$ be $b$ or $s$, and $K$ be a small positive number — 1, 2, or 3 in practice. Let $N$ be the number of bits used to represent $b$ and $s$, which we assume to have the same bit-width. Our goal is to "canonically" decompose an $F_m$ scalar $\alpha$ into high and low parts $h$ and $\ell$ in $\mathbb{F}_b$, consisting of the high $N - K$ and low $K$ bits of $\alpha$, respectively; we call this a $K$-high-low decomposition.
+
+Let $H := m \gg K$ be the high $N - K$ bits of $m$, and $L := m \& (2^K - 1)$ be the low $K$ bits of $m$. A *canonical decomposition* of $\alpha$ into $h$ and $\ell$ is one for which the following *integer* equations hold:
+
+1) $\alpha = 2^K h + \ell$
+2) $h \le H$
+3) $\ell < 2^K$
+4) $(h = H) \implies (\ell \lt L)$
+
+In practice, for small $K$, we always have $L = 1$, since our fields are chosen to have high 2-adicity, meaning a large power of 2 (typically at least $2^{32}$) divides $m - 1$. This means that in practice the last constraint is simplified to
+
+4) $(h = H) \implies (\ell = 0)$.
+
+### Constraint Encoding of the Canonicality Check
+
+We now explain how all of these constraints are Plonk encoded:
+
+1) We don't enforce this check in the $K$-high-low decomp gadget, but it's easily represented as the degree-1 constraint $\alpha - (2^K h + \ell) = 0$ when $\alpha$ is in the base field (i.e. when $m = b$). When $\alpha$ is not in the base field, this constraint can't be encoded without transporting $h$ and $\ell$ to $\alpha$'s field.
+
+2) The condition $\ell < 2^K$ is encoded using the [power-of-2 range check gadget](#pow2-rc) to compute a value that is zero when $\ell < 2^K$. Behind the scenes this involves two table lookups and a small degree constraint; see the power-of-2 range check docs for more details.
+
+3) The condition $h \le H$ is encoded using the [generic range check gadget](#generic-rc) to compute a value that is zero when $h \le H$. Behind the scenes this involves various small degree constraints and lookups; see the generic range check docs for more details.
-The constraint complexity of the `pow2_range_check` is one degree-2 equality check, plus the underlying constraint complexity of a non-strict $q$-window decomposition, and an $r$-bit short range check. However, it's optimized to avoid the window decomposition when $q = 0,$ and to avoid the short range check when $r = 0$. Altogether, this amounts to $q + 2 \cdot r$ lookups of a degree-3 expression in a $2^{K}$-bit lookup table, and roughly $q + r + 1$ degree-2 equality constraints.
+4) The constraint $(h = H) \implies (\ell = 0)$ is first rewritten as
+
+ $$
+ (h - H \ne 0) \vee (\ell = 0).
+ $$
+
+ Intuitively, a constraint of the form $x \ne 0$ can be encoded as $\exists \eta. 1 - x \cdot \eta = 0$, since if $x = 0$ there is no $\eta$ that satisfies the equation, but if $x \ne 0$ then $\eta = 1/x$ is the solution. However, the Plonk constraints are quantifier free, and so we actually compute $\eta$ in the circuit, as $\eta = inv0(x)$, defined as $1/x$ when $x$ is non-zero, and zero otherwise (the corresponding library function is `Assigned::invert()`); in the constraint check in `config.create_gate(meta)` we simply read in the already computed $\eta$ value. We don't need any constraints enforcing that $\eta$ was computed correctly, since a malicious prover that computes an incorrect $\eta$ can never make us think $x \ne 0$ when in fact $x = 0$, since there is no $\eta$ satisfying $1 - 0 \cdot \eta = 0$, i.e. this encoding is sound.
+
+ So, all together, we have the degree-3 encoding
+
+ $$
+ (1 - (h - H) \cdot \eta) \cdot \ell = 0,
+ $$
+
+ where $\eta$ is expected to have been computed as $inv0(h - H)$.
+
+All of these constraints are conditional on the `q_range_check` selector, so in summary we have the encoded constraints
+
+$$
+\begin{array}{|c|l|l|}
+\hline
+\text{Degree} & \text{Constraint} & \text{ID} \\\hline
+2 & q_\texttt{range\_check} \cdot (\ell < 2^K) = 0 & \text{2} \\\hline
+2 & q_\texttt{range\_check} \cdot (h \le H) = 0 & \text{3} \\\hline
+4 & q_\texttt{range\_check} \cdot (1 - (h - H) \cdot \eta) \cdot \ell = 0 & \text{4} \\\hline
+\end{array}
+$$
-## Decomposition
+## Windowed Decomposition
-Given a field element $\alpha$, these gadgets decompose it into $W$ windows $k_i$ of $K$ bits each, and a remainder $z_W$, s.t. the following decomposition equation holds:
+Given a field element $\alpha$, these gadgets decompose it into $W$ windows $k_i$ of $T_\mathcal{O}$ bits each, and a remainder $z_W$, s.t. the following decomposition equation holds:
$$
-\alpha = k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + \cdots + 2^{(W-1)K} \cdot k_{W-1} + 2^{WK} \cdot z_W.
+\alpha = k_0 + 2^{T_\mathcal{O}} \cdot k_1 + 2^{2T_\mathcal{O}} \cdot k_2 + \cdots + 2^{(W-1)T_\mathcal{O}} \cdot k_{W-1} + 2^{WT_\mathcal{O}} \cdot z_W.
$$
-> Note: in the above decomposition equation, there are no other constraints on $z_W$ beyond the equation. So, whereas each $k_i$ is constrained to fall in the range $[0, 2^K)$, without additional constraints on $z_W$, any choice of the $k_i$ will determine some $z_W$ that satisfies the equation. So, for the equation to be useful, we also need to constrain $z_W$.
+> Note: in the above decomposition equation, there are no other constraints on $z_W$ beyond the equation. So, whereas each $k_i$ is constrained to fall in the range $[0, 2^{T_\mathcal{O}})$, without additional constraints on $z_W$, any choice of the $k_i$ will determine some $z_W$ that satisfies the equation. So, for the equation to be useful, we also need to constrain $z_W$.
-> Note: in the existing implementation $K = 10$, since the Orchard circuit as $2^{11}$ rows, and $10$ is the largest integer less than $11$.
+> Note: in the existing implementation $T_\mathcal{O} = 10$, since the Orchard circuit as $2^{11}$ rows, and $10$ is the largest integer less than $11$. However, there is a reimplementation of this for arbitrary $K$ in `halo2_gadgets::utilities::decompose_running_sum`, altho the interface is not exactly the same as described here. In the code, $T_\mathcal{O}$ is referred to as `sinsemilla::K`.
-This is done using "running sums" $z_i$ for $i \in [0..W],$ and **the running sums $z_i$, not the windows $k_i,$ are what these gadgets actually return**; if needed, the $k_i$ can be computed from the $z_i$, as $k_i = z_i - 2^K z_{i+1}$. The intuition is that $z_i = \alpha \gg i \cdot K$, but the constraints only guarantee this when the full decomposition equation is known to hold in terms of integers, i.e. when the RHS does not overflow mod the field modulus.
+This is done using "running sums" $z_i$ for $i \in [0..W],$ and **the running sums $z_i$, not the windows $k_i,$ are what these gadgets actually return**; if needed, the $k_i$ can be computed from the $z_i$, as $k_i = z_i - 2^{T_\mathcal{O}} z_{i+1}$. The intuition is that $z_i = \alpha \gg i \cdot T_\mathcal{O}$, but the constraints only guarantee this when the full decomposition equation is known to hold in terms of integers, i.e. when the RHS does not overflow mod the field modulus.
-> Note: as implemented, the decomposition is only defined for $W \cdot K \lt 255$, to guarantee that $\alpha - z_W$ fits in a Pallas or Vesta field element.
+> Note: as implemented, the decomposition is only defined for $W \cdot T_\mathcal{O} \lt 255$, to guarantee that $\alpha - z_W$ fits in a Pallas or Vesta field element.
-We initialize the first running sum $z_0 = \alpha,$ and compute subsequent terms $z_{i+1} = \frac{z_i - k_i}{2^{K}}.$ This gives us:
+We initialize the first running sum $z_0 = \alpha,$ and compute subsequent terms $z_{i+1} = \frac{z_i - k_i}{2^{T_\mathcal{O}}}.$ This gives us:
$$
\begin{aligned}
z_0 &= \alpha \\
- &= k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + 2^{3K} \cdot k_3 + \cdots, \\
-z_1 &= (z_0 - k_0) / 2^K \\
- &= k_1 + 2^{K} \cdot k_2 + 2^{2K} \cdot k_3 + \cdots, \\
-z_2 &= (z_1 - k_1) / 2^K \\
- &= k_2 + 2^{K} \cdot k_3 + \cdots, \\
+ &= k_0 + 2^{T_\mathcal{O}} \cdot k_1 + 2^{2T_\mathcal{O}} \cdot k_2 + 2^{3T_\mathcal{O}} \cdot k_3 + \cdots, \\
+z_1 &= (z_0 - k_0) / 2^{T_\mathcal{O}} \\
+ &= k_1 + 2^{T_\mathcal{O}} \cdot k_2 + 2^{2T_\mathcal{O}} \cdot k_3 + \cdots, \\
+z_2 &= (z_1 - k_1) / 2^{T_\mathcal{O}} \\
+ &= k_2 + 2^{T_\mathcal{O}} \cdot k_3 + \cdots, \\
&\vdots \\
\downarrow &\text{ (in strict mode)} \\
-z_W &= (z_{W-1} - k_{W-1}) / 2^K \\
+z_W &= (z_{W-1} - k_{W-1}) / 2^{T_\mathcal{O}} \\
&= 0 \text{ (because } z_{W-1} = k_{W-1} \text{)}
\end{aligned}
$$
@@ -83,14 +176,14 @@ When not in "strict mode", the final running sum $z_W$ is allowed to be
non-zero.
### Strict mode
-Strict mode constrains the final running sum output $z_{W}$ to be zero, thus range-constraining the field element to be within $W \cdot K$ bits. In strict mode, we are also assured that $z_{W-1} = k_{W-1}$ gives us the last window in the decomposition.
+Strict mode constrains the final running sum output $z_{W}$ to be zero, thus range-constraining the field element to be within $W \cdot T_\mathcal{O}$ bits. In strict mode, we are also assured that $z_{W-1} = k_{W-1}$ gives us the last window in the decomposition.
-> Note: Let $\alpha_j$ be the $j^{th}$ bit of $\alpha$, where $\alpha_0$ is the LSB. For $j \ge i$, let $\alpha_{j..i}$ be the number with big-endian binary representation $\alpha_j \alpha_{j-1} \cdots \alpha_i$. Then by induction on $i$, the $i^{th}$ running sum $z_i = (\alpha - \alpha_{(i \cdot K - 1) .. 0})/2^{i \cdot K}$ *as integers*, or equivalently $\alpha \gg i \cdot K,$ i.e. the truncating right bit-shift of $\alpha$ by $i \cdot K$ bits. When not in strict mode, this interpretation of the running sums $z_i$ is not necessarily true without additional constraints on $z_W$; only the [decomposition equation](#decomposition-equation) is guaranteed to hold.
+> Note: Let $\alpha_j$ be the $j^{th}$ bit of $\alpha$, where $\alpha_0$ is the LSB. For $j \ge i$, let $\alpha_{j..i}$ be the number with big-endian binary representation $\alpha_j \alpha_{j-1} \cdots \alpha_i$. Then by induction on $i$, the $i^{th}$ running sum $z_i = (\alpha - \alpha_{(i \cdot T_\mathcal{O} - 1) .. 0})/2^{i \cdot T_\mathcal{O}}$ *as integers*, or equivalently $\alpha \gg i \cdot T_\mathcal{O},$ i.e. the truncating right bit-shift of $\alpha$ by $i \cdot T_\mathcal{O}$ bits. When not in strict mode, this interpretation of the running sums $z_i$ is not necessarily true without additional constraints on $z_W$; only the [decomposition equation](#decomposition-equation) is guaranteed to hold.
## Lookup decomposition
-This gadget makes use of a $K$-bit lookup table to decompose a field element $\alpha$ into $K$-bit words. Each $K$-bit word $k_i = z_i - 2^K \cdot z_{i+1}$ is range-constrained by a lookup in the $K$-bit table.
+This gadget makes use of a $T_\mathcal{O}$-bit lookup table to decompose a field element $\alpha$ into $T_\mathcal{O}$-bit words. Each $T_\mathcal{O}$-bit word $k_i = z_i - 2^{T_\mathcal{O}} \cdot z_{i+1}$ is range-constrained by a lookup in the $T_\mathcal{O}$-bit table.
The region layout for the lookup decomposition uses a single advice column $z$, and two selectors $q_{lookup}$ and $q_{running}.$
$$
@@ -109,10 +202,10 @@ $$
### Short range check
-Using two $K$-bit lookups, we can range-constrain a field element $\alpha$ to be $n$ bits, where $n \leq K.$ To do this:
+Using two $T_\mathcal{O}$-bit lookups, we can range-constrain a field element $\alpha$ to be $n$ bits, where $n \leq T_\mathcal{O}.$ To do this:
-1. Constrain $0 \leq \alpha < 2^K$ to be within $K$ bits using a $K$-bit lookup.
-2. Constrain $0 \leq \alpha \cdot 2^{K - n} < 2^K$ to be within $K$ bits using a $K$-bit lookup.
+1. Constrain $0 \leq \alpha < 2^{T_\mathcal{O}}$ to be within $T_\mathcal{O}$ bits using a $T_\mathcal{O}$-bit lookup.
+2. Constrain $0 \leq \alpha \cdot 2^{T_\mathcal{O} - n} < 2^{T_\mathcal{O}}$ to be within $T_\mathcal{O}$ bits using a $T_\mathcal{O}$-bit lookup.
The short variant of the lookup decomposition introduces a $q_{bitshift}$ selector. The same advice column $z$ has here been renamed to $\textsf{word}$ for clarity:
$$
@@ -122,23 +215,23 @@ $$
\hline
\alpha & 1 & 0 & 0 \\\hline
\alpha' & 1 & 0 & 1 \\\hline
-2^{K-n} & 0 & 0 & 0 \\\hline
+2^{T_\mathcal{O}-n} & 0 & 0 & 0 \\\hline
\end{array}
$$
-where $\alpha' = \alpha \cdot 2^{K - n}.$ Note that $2^{K-n}$ is assigned to a fixed column at keygen, and copied in at proving time. This is used in the gate enabled by the $q_\mathit{bitshift}$ selector to check that $\alpha$ was shifted correctly:
+where $\alpha' = \alpha \cdot 2^{T_\mathcal{O} - n}.$ Note that $2^{T_\mathcal{O}-n}$ is assigned to a fixed column at keygen, and copied in at proving time. This is used in the gate enabled by the $q_\mathit{bitshift}$ selector to check that $\alpha$ was shifted correctly:
$$
\begin{array}{|c|l|}
\hline
\text{Degree} & \text{Constraint} \\\hline
- 2 & q_\mathit{bitshift} \cdot ((\alpha \cdot 2^{K - n}) - \alpha') \\\hline
+ 2 & q_\mathit{bitshift} \cdot ((\alpha \cdot 2^{T_\mathcal{O} - n}) - \alpha') \\\hline
\end{array}
$$
### Combined lookup expression
Since the lookup decomposition and its short variant both make use of the same lookup table, we combine their lookup input expressions into a single one:
-$$q_\mathit{lookup} \cdot \left(q_\mathit{running} \cdot (z_i - 2^K \cdot z_{i+1}) + (1 - q_\mathit{running}) \cdot \textsf{word} \right)$$
+$$q_\mathit{lookup} \cdot \left(q_\mathit{running} \cdot (z_i - 2^{T_\mathcal{O}} \cdot z_{i+1}) + (1 - q_\mathit{running}) \cdot \textsf{word} \right)$$
where $z_i$ and $\textsf{word}$ are the same cell (but distinguished here for clarity of usage).
diff --git a/book/src/design/gadgets/ecc.md b/book/src/design/gadgets/ecc.md
index e1025ee98..c4f76a1a0 100644
--- a/book/src/design/gadgets/ecc.md
+++ b/book/src/design/gadgets/ecc.md
@@ -13,6 +13,9 @@ A non-exhaustive list of assumptions made by `EccChip`:
- Holds for Pallas because $5$ is not square in $\mathbb{F}_q$.
- $0$ is not a $y$-coordinate of a valid point on the curve.
- Holds for Pallas because $-5$ is not a cube in $\mathbb{F}_q$.
+- The base and scalar fields of the Ecc Chip curves have 2-adicity at least 3, i.e. $2^3 \mid p - 1$ and $2^3 \mid q - 1$.
+ - Holds for Pallas, Vesta, Pluto, and Eris, which all have 2-adicity of 32.
+
### Layout
diff --git a/book/src/design/gadgets/ecc/var-base-scalar-mul.md b/book/src/design/gadgets/ecc/var-base-scalar-mul.md
index fde5fe420..103093149 100644
--- a/book/src/design/gadgets/ecc/var-base-scalar-mul.md
+++ b/book/src/design/gadgets/ecc/var-base-scalar-mul.md
@@ -496,68 +496,4 @@ def full_width_vbsm(alpha_high, alpha_0, T):
return acc
```
-### Full-width-scalar decomposition range check
-
-In order to ensure that the decomposition of $\alpha$ into $(\alpha \gg 1, \alpha_0)$ was done correctly, we implement a range check on the decomposition. The intuition is that we want to ensure that the decomposition is "canonical", i.e. that it doesn't rely on wraparound mod $q$. This range check is implemented in `halo2_gadgets::ecc::chip::mul::full_width::range_check`.
-
-Suppose $\alpha \in [0, q)$ and we wish to find $h$ and $\ell$ s.t. $\alpha = 2h + \ell$ as integers, and $\ell \in \{0, 1\}.$ However, we must verify the decomposition in a circuit, and so we can only check our equations modulo the base field of our circuit. In modular arithmetic, the equation $\alpha = 2h + \ell$ with $\ell \in \{0, 1\}$ always has two solutions mod $q$, namely
-
-
-$$
-(h, \ell) = (\alpha \gg 1, \alpha_0),
-$$
-
-and
-
-$$
-(h, \ell) = ((\alpha \gg 1) + (q + 2\alpha_0 - 1)/2, 1 - \alpha_0).
-$$
-
-We need to find the first solution, which we call the "canonical" solution, since for that solution $\alpha$ and $2h + \ell$ are equal as integers. For the canonical solution, we have $h \in [0, (q-1)/2)$, except when $\alpha = q-1$, in which case the solution is $h = (q-1)/2$ and $\ell = 0$; when $\ell = 1$ and $h = (q-1)/2$, we get a non-canonical solution to the equation $0 = 2h + \ell \bmod q$, so we can't allow solutions with $h = (q-1)/2$ generally. So, to enforce canonicality, we check that
-
-$$
-h \in [0,(q-1)/2]
-$$
-
-and
-
-$$
-(h = (q-1)/2) \implies (\ell = 0).
-$$
-
-We now explain how all of these constraints are Plonk encoded:
-
-1) The constraint $\ell \in \{0, 1\}$ is encoded as $\texttt{bool\_check}(\ell) = 0$, i.e. $\ell \cdot (\ell - 1) = 0$ of degree 2.
-
-2) The constraint $h \in [0,(q-1)/2]$ is encoded using the [generic range check gadget](/design/gadgets/decomposition.html#generic-range-check) to compute a value that is zero when $h \le (q-1)/2$. Behind the scenes this involves various small degree constraints and lookups; see the decomposition docs for more details.
-
-3) The constraint $(h = (q-1)/2) \implies (\ell = 0)$ is first rewritten as
-
- $$
- (h - (q-1)/2 \ne 0) \vee (\ell = 0).
- $$
-
- Intuitively, a constraint of the form $x \ne 0$ can be encoded as $\exists \eta. 1 - x \cdot \eta = 0$, since if $x = 0$ there is no $\eta$ that satisfies the equation, but if $x \ne 0$ then $\eta = 1/x$ is the solution. However, the Plonk constraints are quantifier free, and so we actually compute $\eta$ in the circuit, as $\eta = inv0(x)$, defined as $1/x$ when $x$ is non-zero, and zero otherwise (the corresponding library function is `Assigned::invert()`); in the constraint check in `config.create_gate(meta)` we simply read in the already computed $\eta$ value. We don't need any constraints enforcing that $\eta$ was computed correctly, since a malicious prover that computes an incorrect $\eta$ can never make us think $x \ne 0$ when in fact $x = 0$, since there is no $\eta$ satisfying $1 - 0 \cdot \eta = 0$, i.e. this encoding is sound.
-
- So, all together, we have the degree-2 encoding (note that $q$ is a constant)
-
- $$
- (1 - (h - (q-1)/2) \cdot \eta) \cdot \ell = 0,
- $$
-
- where $\eta$ is expected to have been computed as $inv0(h - (q-1)/2)$.
-
-All of these constraints are conditional on the `q_range_check` selector, so in summary we have the encoded constraints
-
-
-$$
-\begin{array}{|c|l|l|}
-\hline
-\text{Degree} & \text{Constraint} & \text{ID} \\\hline
-3 & q_\texttt{range\_check} \cdot \texttt{bool\_check}(\ell) = 0 & \text{1} \\\hline
-2 & q_\texttt{range\_check} \cdot (h \le (q-1)/2) = 0 & \text{2} \\\hline
-3 & q_\texttt{range\_check} \cdot (1 - (h - (q-1)/2) \cdot \eta) \cdot \ell = 0 & \text{3} \\\hline
-\end{array}
-$$
-
-Note that these constraints can be implemented in $\mathbb{F}_p$ or $\mathbb{F}_q$, since $(q+1)/2 \lt p$. However, on the $\mathbb{F}_q$ side, the additional constraint $\alpha = 2h + \ell$ also needs to be checked, to ensure that the decomposition actually decomposes $\alpha$, in addition to being canonical!
+See [$1$-high-low decomposition docs](/design/gadgets/decomposition.html#1-hl-decomp) for a description of how we do the decomposition, and the associated constraints.
diff --git a/halo2_gadgets/benches/ecc_circuits/scalar_mul.rs b/halo2_gadgets/benches/ecc_circuits/scalar_mul.rs
index e746d3c20..7b6d862d7 100644
--- a/halo2_gadgets/benches/ecc_circuits/scalar_mul.rs
+++ b/halo2_gadgets/benches/ecc_circuits/scalar_mul.rs
@@ -103,8 +103,8 @@ impl Circuit for ScalarMulCircuitSmall {
let decomposed_scalar = config
.mul
- .full_width_config
- .assign(&mut layouter, &Value::known(*LARGE_SCALAR))?;
+ .decomp_config
+ .k1_decomp_and_range_check_scalar(&mut layouter, Value::known(*LARGE_SCALAR))?;
let (_point, _scalar) = config.mul.assign_full_width(
layouter.namespace(|| "full-width multiply"),
decomposed_scalar,
@@ -167,8 +167,8 @@ impl Circuit for ScalarMulCircuit {
let decomposed_scalar = config
.inner
.mul
- .full_width_config
- .assign(&mut layouter, &Value::known(*LARGE_SCALAR))?;
+ .decomp_config
+ .k1_decomp_and_range_check_scalar(&mut layouter, Value::known(*LARGE_SCALAR))?;
let mut assign_output: Option<(EccPoint, ScalarVar)> = None;
for _ in 0..SCALAR_MUL_ITER {
diff --git a/halo2_gadgets/src/ecc/chip.rs b/halo2_gadgets/src/ecc/chip.rs
index c4a993ffc..329dd7f90 100644
--- a/halo2_gadgets/src/ecc/chip.rs
+++ b/halo2_gadgets/src/ecc/chip.rs
@@ -34,8 +34,8 @@ pub(super) mod witness_point;
pub mod configs {
pub use super::add::Config as CompleteAddConfig;
pub use super::double::Config as DoubleConfig;
- pub use super::mul::full_width::Config as ScalarDecompConfig;
pub use super::mul::Config as MulVarBaseConfig;
+ pub use crate::utilities::high_low_decomp::Config as ScalarDecompConfig;
}
pub use constants::*;
@@ -412,14 +412,14 @@ impl EccBaseFieldElemFixed {
/// where alpha_high = alpha >> 1.
pub struct EccScalarVarFullWidth {
/// The full-width scalar, alpha.
- value: Value,
+ pub(crate) value: Value,
/// The high bits of alpha, i.e. alpha >> 1.
- alpha_high: AssignedCell,
+ pub(crate) alpha_high: AssignedCell,
// The original WIP API used `AssignedCell`, but
// only `AssignedCell` is well supported by the
// rest of the codebase.
/// The low bit of alpha, i.e. alpha & 1.
- alpha_0: AssignedCell,
+ pub(crate) alpha_0: AssignedCell,
}
impl EccScalarVarFullWidth {
@@ -699,8 +699,8 @@ where
let decomposed_scalar = self
.config()
.mul
- .full_width_config
- .assign(layouter, scalar)?;
+ .decomp_config
+ .k1_decomp_and_range_check_scalar(layouter, *scalar)?;
Ok(ScalarVar::FullWidth(decomposed_scalar))
}
}
diff --git a/halo2_gadgets/src/ecc/chip/mul.rs b/halo2_gadgets/src/ecc/chip/mul.rs
index f4d144ad6..a724d67a6 100644
--- a/halo2_gadgets/src/ecc/chip/mul.rs
+++ b/halo2_gadgets/src/ecc/chip/mul.rs
@@ -1,7 +1,7 @@
use super::{add, EccPoint, EccScalarVarFullWidth, NonIdentityEccPoint, ScalarVar, T_Q};
use crate::{
sinsemilla::primitives as sinsemilla,
- utilities::{bool_check, pow2_range_check, ternary},
+ utilities::{bool_check, high_low_decomp, pow2_range_check, ternary},
};
use std::{
convert::TryInto,
@@ -19,7 +19,6 @@ use halo2curves::pasta::pallas;
use uint::construct_uint;
mod complete;
-pub(crate) mod full_width;
pub(super) mod incomplete;
mod overflow;
@@ -65,8 +64,8 @@ pub struct Config {
complete_config: complete::Config,
/// Configuration used to check for overflow
overflow_config: overflow::Config,
- /// Configuration used for full-width scalars
- pub full_width_config: full_width::Config,
+ /// Configuration used high-low decomp and range checking
+ pub decomp_config: high_low_decomp::Config,
}
impl Config {
@@ -86,9 +85,8 @@ impl Config {
let complete_config = complete::Config::configure(meta, advices[9], add_config);
let overflow_config =
overflow::Config::configure(meta, pow2_config, advices[6..9].try_into().unwrap());
-
- let full_width_config =
- full_width::Config::configure(meta, pow2_config, advices[0], advices[1]);
+ let decomp_config =
+ high_low_decomp::Config::configure(meta, pow2_config, advices[0], advices[1]);
let config = Self {
q_mul_lsb: meta.selector(),
@@ -98,7 +96,7 @@ impl Config {
lo_config,
complete_config,
overflow_config,
- full_width_config,
+ decomp_config,
};
config.create_gate(meta);
@@ -864,9 +862,9 @@ pub mod tests {
#[test]
fn test_cost_model_scalar_decomp() {
- use crate::ecc::chip::mul::full_width;
use crate::ecc::utilities::constants::*;
use crate::utilities::cost_model::circuit_to_csv;
+ use crate::utilities::high_low_decomp;
use crate::utilities::lookup_range_check::LookupRangeCheckConfig;
use halo2_proofs::circuit::*;
use halo2_proofs::plonk::*;
@@ -879,7 +877,7 @@ pub mod tests {
#[derive(Debug, Clone)]
struct BenchScalarDecompSmall {
- scalar_decomp: full_width::Config,
+ high_low_decomp: high_low_decomp::Config,
lookup: LookupRangeCheckConfig,
}
@@ -912,10 +910,10 @@ pub mod tests {
LookupRangeCheckConfig::configure(meta, advices[0], lookup_table);
let pow2_config =
pow2_range_check::Config::configure(meta, advices[0], lookup_config);
- let scalar_decomp =
- full_width::Config::configure(meta, pow2_config, advices[1], advices[2]);
+ let high_low_decomp =
+ high_low_decomp::Config::configure(meta, pow2_config, advices[1], advices[2]);
Self::Config {
- scalar_decomp,
+ high_low_decomp,
lookup: lookup_config,
}
}
@@ -930,8 +928,8 @@ pub mod tests {
config.lookup.load(&mut layouter)?;
config
- .scalar_decomp
- .assign(&mut layouter, &Value::known(*LARGE_SCALAR))?;
+ .high_low_decomp
+ .k1_decomp_and_range_check_scalar(&mut layouter, Value::known(*LARGE_SCALAR))?;
Ok(())
}
@@ -1034,8 +1032,8 @@ pub mod tests {
let decomposed_scalar = config
.mul
- .full_width_config
- .assign(&mut layouter, &Value::known(*LARGE_SCALAR))?;
+ .decomp_config
+ .k1_decomp_and_range_check_scalar(&mut layouter, Value::known(*LARGE_SCALAR))?;
let (_point, _scalar) = config.mul.assign_full_width(
layouter.namespace(|| "full-width multiply"),
decomposed_scalar,
diff --git a/halo2_gadgets/src/ecc/chip/mul/full_width.rs b/halo2_gadgets/src/ecc/chip/mul/full_width.rs
deleted file mode 100644
index a9aaac867..000000000
--- a/halo2_gadgets/src/ecc/chip/mul/full_width.rs
+++ /dev/null
@@ -1,593 +0,0 @@
-//! Full-width scalar decomposition and range check.
-//!
-//! See the variable-base scalar-mul decomposition section of the
-//! [Halo 2 book](http://localhost:3000/design/gadgets/ecc/var-base-scalar-mul.html#handling-full-width-scalar-field-scalars-when-qp)
-//! for more details.
-//!
-//! In short, we implement decomposing an Fq scalar $\alpha$ into high
-//! and low parts $h$ and $\ell$, s.t.
-//!
-//! - $\alpha = 2h + \ell$
-//! - $h \le (q-1)/2$
-//! - $\ell$ is boolean
-//!
-//! We enforce the second two conditions with constraints in
-//! `range_check`, but we don't enforce the first condition, because
-//! we're working in Fp and the Fq element $\alpha$ is not
-//! representable directly (indeed, that's the original motivation for
-//! decomposing it).
-use crate::{
- ecc::chip::T_Q,
- sinsemilla::primitives as sinsemilla,
- utilities::{bool_check, generic_range_check, pow2_range_check},
-};
-
-use super::super::EccScalarVarFullWidth;
-
-use halo2_proofs::{
- circuit::{Layouter, Region, Value},
- plonk::{Advice, Assigned, Column, ConstraintSystem, Constraints, Error, Expression, Selector},
- poly::Rotation,
-};
-use halo2curves::pasta::pallas;
-
-use ff::{Field, PrimeField};
-
-/// (q - 1)/2 = (2^254 + t_q - 1)/2 = 2^253 + (t_q - 1)/2
-fn q12() -> pallas::Base {
- // 2^253.
- let two_253 = pallas::Base::one().double().pow([253]);
- // (t_q - 1)/2.
- let delta = (pallas::Base::from_u128(T_Q) - pallas::Base::one())
- * pallas::Base::from_u128(2).invert().unwrap();
- two_253 + delta
-}
-
-// Copied from
-// ecc:chip::mul::decompose_for_scalar_mul(). I don't
-// understand why there isn't some more natural way to
-// convert an ff point to an int???
-#[allow(clippy::assign_op_pattern)]
-mod uint {
- use uint::construct_uint;
- construct_uint! {
- pub(super) struct U256(4);
- }
-}
-use uint::U256;
-
-#[derive(Copy, Clone, Debug, Eq, PartialEq)]
-/// Config struct for full-width scalar decomposition and range check.
-pub struct Config {
- /// Range check for alpha_high and alpha_0.
- q_range_check: Selector,
- /// Config for range check that alpha_high is less than or equal
- /// to (q-1)/2.
- rc_config: generic_range_check::Config,
- /// High bits of things.
- high: Column,
- /// Low bits of things.
- low: Column,
-}
-
-impl Config {
- /// Configure full-width scalar decomp gadget.
- pub fn configure(
- meta: &mut ConstraintSystem,
- pow2_config: pow2_range_check::Config,
- high: Column,
- low: Column,
- ) -> Self {
- meta.enable_equality(high);
- meta.enable_equality(low);
- let rc_config = generic_range_check::Config::configure(meta, [high, low], pow2_config);
- let config = Self {
- q_range_check: meta.selector(),
- rc_config,
- high,
- low,
- };
- config.create_gate(meta);
- config
- }
-
- /// Create a gate to constrain the canonicality of the decomposition.
- ///
- /// The assignment layout:
- ///
- /// ```text
- /// | high | low | offset |
- /// |----------|-----|--------|
- /// | h | l | 0 | <-- q_range_check enabled here
- /// | h_le_max | eta | 1 |
- /// ```
- fn create_gate(&self, meta: &mut ConstraintSystem) {
- meta.create_gate(
- "Variable-base scalar-mul decomposition range check",
- |meta| {
- let q_range_check = meta.query_selector(self.q_range_check);
- let h = meta.query_advice(self.high, Rotation(0));
- let l = meta.query_advice(self.low, Rotation(0));
- let h_le_max = meta.query_advice(self.high, Rotation(1));
- let eta = meta.query_advice(self.low, Rotation(1));
-
- let one = Expression::Constant(pallas::Base::one());
- let q12 = Expression::Constant(q12());
-
- // Constituant constraints:
- //
- // Constrain l to be boolean.
- let l_is_bool = bool_check(l.clone());
- // Constrain l to be zero.
- let l_is_zero = l;
- // Constrain h = (q-1)/2.
- let h_is_max: Expression = h.clone() - q12;
- // Constrain not(h = (q-1)/2) for use in constraining
- // (h = (q-1)/2) => (l = 0).
- //
- // This one is a little subtle: constraints are
- // encoded to be true when they they're zero, and
- // false otherwise. So to logically negate ("not") a
- // constraint c, we need an expression that is zero
- // when the c is non-zero and non-zero when c is
- // zero. This condition on c can be expressed as
- //
- // there exists eta s.t. 1 - c*eta = 0
- //
- // Now if c is zero, there is no eta that satisfies
- // the above formula. But if c is non-zero, we can use
- // eta = 1/c.
- //
- // In practice, we compute not(x) = 1 - c*inv0(x),
- // where inv0(x) = 1/x when x is non-zero, and inv0(0)
- // = 0. I.e. we choose eta = inv0(x). The library
- // function that computes inv0() is called invert().
- //
- // Ok, but what if eta is not calculated correctly?
- // Afterall, there are no constraints on eta, it's
- // just something we're pulling out of an assigned
- // cell! Well, if we're using not(c) to encode
- //
- // (c => d) == (not(c) \/ d) == ((1 - c*eta) * d)
- //
- // then consider two cases:
- //
- // 1) if c = 0, then no matter what eta is, 1 - c*eta
- // will never be zero (true), so d will necessarily
- // be zero (true) if ((1 - c*eta) * d) is
- // satisfied. I.e. if c is satisfied then d is
- // satisfied, i.e. (c => d) when c is true.
- //
- // 2) if c /= 0, then (c => d) is true independent of
- // d. Now either ((1 - c*eta) * d) is zero (true),
- // because eta was chosen correctly, or ((1 -
- // c*eta) * d) is non-zero (false), and the
- // constraints aren't satisfied.
- //
- // In other words, ((1 - c*eta) * d) is true implies
- // (c => d) is true, and so this encoding is sound. It
- // may not be complete, because a moronic prover could
- // choose the wrong eta, but there's no way for a
- // malicious prover to make ((1 - c*eta) * d) true
- // when (c => d) would be false.
- let h_is_not_max = one - h_is_max * eta;
-
- // Compound constraints:
- //
- // We want to check all of
- //
- // - l is boolean
- // - h is maximal => l = 0
- // - which is equivalent to
- // - not(h is maximal) \/ l = 0
- // - h <= (q-1)/2
- //
- // The one thing we don't check is that alpha = 2*h +
- // l, since that can only be checked in Fq land.
- Constraints::with_selector(
- q_range_check,
- vec![
- ("l is boolean", l_is_bool),
- ("(h = (q-1)/2) => (l = 0)", h_is_not_max * l_is_zero),
- ("(h <= (q-1)/2)", h_le_max),
- ],
- )
- },
- );
- }
-
- /// Decompose Fq scalar alpha into high and low bits alpha_high
- /// and alpha_0, witness the high and low bits, and return the
- /// decomposition.
- pub fn assign(
- &self,
- layouter: &mut impl Layouter,
- scalar: &Value,
- ) -> Result, Error> {
- let decomposed_scalar = layouter.assign_region(
- || "Full-width variable-base mul (assign full-width scalar)",
- |mut region| {
- let offset = 0;
- self.decompose_scalar(&mut region, offset, scalar)
- },
- )?;
- self.range_check(layouter, decomposed_scalar.clone())?;
- Ok(decomposed_scalar)
- }
-
- /// Constrain alpha_high and alpha_0 to be a canonical
- /// decomposition. Note that we can't actually check that they're
- /// a decomposition of alpha, since we can't witness alpha in an
- /// Fp circuit. Hence it's still up to the caller of assign() to
- /// check that the decomposition is correct, i.e. to check that
- /// `2*alpha_high + alpha_0 == alpha` in Fq.
- ///
- /// Resulting layout, as consumed by create_gate:
- ///
- /// ```text
- /// | high | low | offset |
- /// |----------|-----|--------|
- /// | h | l | 0 | <-- q_range_check enabled here
- /// | h_le_max | eta | 1 |
- /// ```
- pub(crate) fn range_check(
- &self,
- layouter: &mut impl Layouter,
- decomposed_scalar: EccScalarVarFullWidth,
- ) -> Result<(), Error> {
- let h = decomposed_scalar.alpha_high;
- // Compute value that is zero when `h <= (q-1)/2`.
- //
- // x <= (q-1)/2 iff x < (q-1)/2 + 1.
- let bound = q12() + pallas::Base::one();
- let h_le_max = self.rc_config.range_check(
- layouter.namespace(|| "h <= (q-1)/2"),
- h.clone(),
- bound,
- false,
- )?;
- layouter.assign_region(
- || "decomposed scalar range check",
- |mut region| {
- // Enable range check.
- self.q_range_check.enable(&mut region, 0)?;
- h.copy_advice(|| "h", &mut region, self.high, 0)?;
- decomposed_scalar
- .alpha_0
- .copy_advice(|| "l", &mut region, self.low, 0)?;
- h_le_max.copy_advice(|| "h_le_max", &mut region, self.high, 1)?;
-
- // Witness the eta := inv0(h - (q-1)/2), where inv0(x) = 0 if x = 0, and 1/x otherwise.
- let h_minus_q12 = h.value().map(|h| h - q12());
- let eta = h_minus_q12.map(|h_minus_q12| Assigned::from(h_minus_q12).invert());
- region.assign_advice(|| "eta", self.low, 1, || eta)?;
- Ok(())
- },
- )?;
- Ok(())
- }
-
- /// Decompose a scalar alpha into (alpha >> 1) and (alpha & 1).
- ///
- /// We don't constrain the canonicality of the decomposition
- /// here. See this comment for the constraints that would be
- /// required:
- ///
- fn decompose_scalar(
- &self,
- region: &mut Region<'_, pallas::Base>,
- offset: usize,
- scalar: &Value,
- ) -> Result, Error> {
- let val_pair = scalar.and_then(|scalar| {
- let scalar_int = U256::from_little_endian(&scalar.to_repr());
- let alpha_high_int = scalar_int >> 1;
- let one_int = U256::from(1);
- let alpha_0_int = scalar_int & one_int;
- // Here U256::0() returns the underlying [u64; 4].
- let alpha_high = pallas::Base::from_raw(alpha_high_int.0);
- let alpha_0 = pallas::Base::from_raw(alpha_0_int.0);
- Value::known((alpha_high, alpha_0))
- });
- let (alpha_high, alpha_0) = val_pair.unzip();
- let alpha_high = region.assign_advice(|| "alpha_high", self.high, offset, || alpha_high)?;
- let alpha_0 = region.assign_advice(|| "alpha_0", self.low, offset, || alpha_0)?;
- Ok(EccScalarVarFullWidth {
- value: *scalar,
- alpha_high,
- alpha_0,
- })
- }
-}
-
-/// Tests for full-width scalar decomposition. These tests were
-/// originally written for a different implementation of the
-/// scalar-decomp range check, but the implementation has since been
-/// greatly simplified by using the newer generic range check
-/// gadget. However, the the generic range check gadget internally
-/// implements a generalization of the approach that used to be
-/// implemented here, so the specific values tested here, altho not
-/// all obviously motivated by the code in this file, should still do
-/// a good job of testing the underlying generic range check gadget.
-#[cfg(test)]
-mod tests {
- use crate::{
- ecc::chip::{configs, mul::full_width::uint::U256, EccScalarVarFullWidth, T_Q},
- utilities::{lookup_range_check::LookupRangeCheckConfig, pow2_range_check},
- };
- use ff::{Field, PrimeField};
- use halo2_proofs::{
- circuit::{Layouter, SimpleFloorPlanner, Value},
- dev::MockProver,
- plonk::{Advice, Circuit, Column, ConstraintSystem},
- };
- use halo2curves::pasta::pallas;
- use rand::rngs::OsRng;
-
- use super::q12;
-
- /// 2^130
- fn two_130() -> pallas::Base {
- pallas::Base::from_u128(1 << 127) * pallas::Base::from_u128(1 << 3)
- }
-
- /// 2^253
- fn two_253() -> pallas::Base {
- pallas::Base::from_u128(1 << 125).square() * pallas::Base::from_u128(1 << 3)
- }
-
- /// (t_q + 1)/2
- fn delta() -> pallas::Base {
- (pallas::Base::from_u128(T_Q) + pallas::Base::one())
- * pallas::Base::from_u128(2).invert().unwrap()
- }
-
- /// Test modes for the scalar decomposition gadget.
- #[derive(Copy, Clone)]
- enum TestMode {
- /// Decompose the provided scalar, range check the result, and
- /// check that the decomposition is correct.
- CombinedDecompAndRangeCheck {
- scalar: pallas::Scalar,
- },
- /// Check that the provided decomposition is canonical.
- InRangeDecomp {
- high: pallas::Base,
- low: pallas::Base,
- },
- /// Check that the provided decomposition is non-canonical.
- OutOfRangeDecomp {
- high: pallas::Base,
- low: pallas::Base,
- },
- NoTest,
- }
-
- /// Computes a single scalar decomposition.
- /// Useful for finding the characteristics of the scalar decomposition gadget
- #[derive(Clone, Copy)]
- struct ScalarDecompCircuit {
- mode: TestMode,
- }
-
- #[derive(Debug, Clone)]
- struct ScalarDecompConfig {
- scalar_decomp: configs::ScalarDecompConfig,
- lookup: LookupRangeCheckConfig,
- }
-
- impl Circuit for ScalarDecompCircuit {
- type Config = ScalarDecompConfig;
-
- type FloorPlanner = SimpleFloorPlanner;
-
- #[cfg(feature = "circuit-params")]
- type Params = ();
-
- fn without_witnesses(&self) -> Self {
- Self {
- mode: TestMode::NoTest,
- }
- }
-
- fn configure(meta: &mut ConstraintSystem) -> Self::Config {
- let advices: [Column; 3] = [
- meta.advice_column(),
- meta.advice_column(),
- meta.advice_column(),
- ];
-
- // Avoid errors about "too few fixed columns are enabled for
- // global constants usage".
- let constants = meta.fixed_column();
- meta.enable_constant(constants);
-
- let lookup_table = meta.lookup_table_column();
- let lookup_config = LookupRangeCheckConfig::configure(meta, advices[0], lookup_table);
- let pow2_config = pow2_range_check::Config::configure(meta, advices[0], lookup_config);
- let scalar_decomp =
- configs::ScalarDecompConfig::configure(meta, pow2_config, advices[1], advices[2]);
- Self::Config {
- scalar_decomp,
- lookup: lookup_config,
- }
- }
-
- fn synthesize(
- &self,
- config: Self::Config,
- mut layouter: impl Layouter,
- ) -> Result<(), halo2_proofs::plonk::Error> {
- // Load 10-bit lookup table. In the Action circuit, this will be
- // provided by the Sinsemilla chip.
- config.lookup.load(&mut layouter)?;
-
- match self.mode {
- // Do a decomposition, range check the result, and
- // check that the decomposition is correct.
- TestMode::CombinedDecompAndRangeCheck { scalar } => {
- let decomposed_scalar = config
- .scalar_decomp
- .assign(&mut layouter, &Value::known(scalar))?;
- decomposed_scalar
- .alpha_high
- .value()
- .zip(decomposed_scalar.alpha_0.value())
- .map(|(h, l)| {
- assert_eq!(
- U256::from_little_endian(&scalar.to_repr()),
- U256::from(2) * U256::from_little_endian(&h.to_repr())
- + U256::from_little_endian(&l.to_repr()),
- "Decomposition must satisfy alpha = 2*alpha_high + alpha_0!"
- );
- });
- }
- // Manually construct a decomposition and range check.
- // Whether we expect this to verify or not depends on
- // the mode.
- TestMode::OutOfRangeDecomp { high, low }
- | TestMode::InRangeDecomp { high, low } => {
- let decomposed_scalar = layouter.assign_region(
- || "Full-width variable-base mul (assign full-width scalar)",
- |mut region| {
- let offset = 0;
- let high = region.assign_advice(
- || "high",
- config.scalar_decomp.high,
- offset,
- || Value::known(high),
- )?;
- let low = region.assign_advice(
- || "low",
- config.scalar_decomp.low,
- offset,
- || Value::known(low),
- )?;
- Ok(EccScalarVarFullWidth {
- // We don't care about the scalar value here, we're only going to range check the decomposition.
- value: Value::known(pallas::Scalar::zero()),
- alpha_high: high,
- alpha_0: low,
- })
- },
- )?;
- config
- .scalar_decomp
- .range_check(&mut layouter, decomposed_scalar)?;
- }
- TestMode::NoTest => (),
- }
- Ok(())
- }
- }
-
- #[test]
- fn combined_scalar_decomp_and_range_check() {
- let zero = pallas::Scalar::zero();
- let one = pallas::Scalar::one();
- let two_253 = pallas::Scalar::from_repr(two_253().to_repr()).unwrap();
- let two_254 = two_253.double();
- let delta = pallas::Scalar::from_repr(delta().to_repr()).unwrap();
- let scalars = [
- ("zero", zero),
- ("one", one),
- ("delta", delta),
- ("2^253", two_253),
- ("2^254", two_254),
- // q-1. This covers the only case where high = (q-1)/2 is allowed.
- ("q - 1", pallas::Scalar::one().neg()),
- ];
- let random_scalars: [(&str, pallas::Scalar); 10] = (0..10)
- .map(|_| {
- let scalar = pallas::Scalar::random(OsRng);
- ("random scalar", scalar)
- })
- .collect::>()
- .try_into()
- .unwrap();
- for (msg, scalar) in scalars.iter().chain(random_scalars.iter()) {
- let circuit = ScalarDecompCircuit {
- mode: TestMode::CombinedDecompAndRangeCheck { scalar: *scalar },
- };
- let prover = MockProver::::run(11, &circuit, vec![]).unwrap();
- assert_eq!(
- prover.verify(),
- Ok(()),
- "Unexpected decomp-and-range-check failure for {} ({:?})",
- msg,
- scalar
- );
- }
- }
-
- #[test]
- fn in_range_decomp() {
- let zero = pallas::Base::zero();
- let one = pallas::Base::one();
- let pairs = [
- // Exercise the `high in [0, 2^253)` part of the range check.
- ("(0,0)", zero, zero),
- ("(2^253 - 1, 1)", two_253() - one, one),
- // Exercise corner cases for the `high in [2^253, 2^253 + delta)` part of
- // the range check.
- ("(2^253, 0)", two_253(), one),
- (
- "(2^253 - 2^130 + delta, 1)",
- two_253() - two_130() + delta(),
- one,
- ),
- ("(2^253 + delta - 1, 0)", two_253() + delta() - one, zero),
- // The only case where high = (q-1)/2 is allowed.
- ("((q-1)/2, 0)", q12(), zero),
- ];
- for (msg, high, low) in pairs.iter() {
- let circuit = ScalarDecompCircuit {
- mode: TestMode::OutOfRangeDecomp {
- high: *high,
- low: *low,
- },
- };
- let prover = MockProver::::run(11, &circuit, vec![]).unwrap();
- assert_eq!(
- prover.verify(),
- Ok(()),
- "Unexpected range check failure for {}",
- msg
- );
- }
- }
-
- #[test]
- fn out_of_range_decomp() {
- let zero = pallas::Base::zero();
- let one = pallas::Base::one();
- let two = one.double();
- let p = one.neg();
- let pairs = [
- // low is out of range.
- ("(0, 2)", zero, two),
- // high is out of range.
- ("(p, 0)", p, zero),
- ("(2^254, 0)", two_253().double(), zero),
- ("(2^254, 1)", two_253().double(), one),
- ("((q-1)/2 + 1, 0)", q12() + one, zero),
- ("(2^253 + 2^130, 1)", two_253() + two_130(), one),
- // high is out of range because low is not zero.
- ("((q-1)/2, 1)", q12(), one),
- ];
- for (msg, high, low) in pairs.iter() {
- let circuit = ScalarDecompCircuit {
- mode: TestMode::OutOfRangeDecomp {
- high: *high,
- low: *low,
- },
- };
- let prover = MockProver::::run(11, &circuit, vec![]).unwrap();
- assert!(
- prover.verify().is_err(),
- "Unexpected range check success for {}",
- msg
- );
- }
- }
-}
diff --git a/halo2_gadgets/src/transcript.rs b/halo2_gadgets/src/transcript.rs
index c03aa763c..0d0723cbc 100644
--- a/halo2_gadgets/src/transcript.rs
+++ b/halo2_gadgets/src/transcript.rs
@@ -7,11 +7,13 @@
//! field fits in the scalar field or vice versa.
use crate::{
- ecc::chip::{mul::full_width, EccScalarVarFullWidth, NonIdentityEccPoint},
- poseidon::duplex::{DuplexChip, DuplexInstructions},
- poseidon::{PoseidonSpongeInstructions, Pow5Chip, Pow5Config},
+ ecc::chip::{EccScalarVarFullWidth, NonIdentityEccPoint},
+ poseidon::{
+ duplex::{DuplexChip, DuplexInstructions},
+ PoseidonSpongeInstructions, Pow5Chip, Pow5Config,
+ },
utilities::{
- lookup_range_check::LookupRangeCheckConfig, pow2_range_check,
+ high_low_decomp, lookup_range_check::LookupRangeCheckConfig, pow2_range_check,
scalar_fits_in_base_range_check,
},
};
@@ -91,7 +93,7 @@ pub struct TranscriptConfigBaseFitsInScalar<
const WIDTH: usize,
const RATE: usize,
> {
- scalar_decomp: full_width::Config,
+ scalar_decomp: high_low_decomp::Config,
pow5config: Pow5Config,
}
@@ -124,7 +126,7 @@ impl TranscriptConfigBaseFitsInScalar; NOUTPUTS],
pow2: pow2_range_check::Config,
- scalar: full_width::Config,
+ scalar: high_low_decomp::Config,
pow5: Pow5Config,
x: Column,
y: Column,
@@ -376,7 +381,7 @@ mod test_poseidon_transcript_chip_base_fits_in_scalar {
let high = meta.advice_column();
let low = meta.advice_column();
- let scalar = full_width::Config::configure(meta, pow2, high, low);
+ let scalar = high_low_decomp::Config::configure(meta, pow2, high, low);
let outputs = (0..NOUTPUTS)
.map(|_| meta.instance_column())
@@ -426,7 +431,9 @@ mod test_poseidon_transcript_chip_base_fits_in_scalar {
let pow5 = Pow5Chip::construct(config.pow5);
// Decompose scalar into two cells and run range proof
- let scalar = config.scalar.assign(&mut layouter, &self.scalar)?;
+ let scalar = config
+ .scalar
+ .k1_decomp_and_range_check_scalar(&mut layouter, self.scalar)?;
let point = layouter.assign_region(
|| "load point",
diff --git a/halo2_gadgets/src/utilities.rs b/halo2_gadgets/src/utilities.rs
index 718b7e7f5..9a67638d2 100644
--- a/halo2_gadgets/src/utilities.rs
+++ b/halo2_gadgets/src/utilities.rs
@@ -13,6 +13,7 @@ pub mod cost_model;
pub mod decompose_running_sum;
pub mod double_and_add;
pub mod generic_range_check;
+pub mod high_low_decomp;
pub mod lookup_range_check;
pub mod pow2_range_check;
pub mod scalar_fits_in_base_range_check;
diff --git a/halo2_gadgets/src/utilities/high_low_decomp.rs b/halo2_gadgets/src/utilities/high_low_decomp.rs
new file mode 100644
index 000000000..5990a47c2
--- /dev/null
+++ b/halo2_gadgets/src/utilities/high_low_decomp.rs
@@ -0,0 +1,949 @@
+#![allow(rustdoc::private_intra_doc_links)]
+//! Implementation of `K`-high-low scalar decomposition and range checking.
+//!
+//! Fix an elliptic curve $C$ and let $F_b$ and $F_s$ denote $C$'s
+//! base and scalar fields, respectively, and let $m$ be $b$ or $s$,
+//! and $K$ be a small positive number -- 1, 2, or 3 in practice. Let
+//! $N$ be the number of bits used to represent $b$ and $s$, which we
+//! assume to have the same bit-width. This module implements
+//! decomposing an $F_m$ scalar $\alpha$ into high and low parts $h$
+//! and $\ell$ in $F_b$, consisting the the high $N - K$ and low $K$
+//! bits of $\alpha$, respectively; we call this a $K$-high-low
+//! decomposition.
+//!
+//! More formally, let $H := (m \gg K)$ be the high $N - K$ bits of
+//! $m$, and $L := m & (2^K - 1)$ be the low $K$ bits of $m$. We
+//! decompose $\alpha$ into $h$ and $\ell$ s.t. the following integer
+//! equations hold:
+//!
+//! 1) $\alpha = 2^K h + \ell$
+//! 2) $h \le H$
+//! 3) $\ell < 2^K$
+//! 4) $(h = H) \implies (\ell \lt L)$
+//!
+//! In practice, for small $K$, we always have $L = 1$, since our
+//! fields are chosen to have high 2-adicity, meaning a large power of
+//! 2 (typically at least $2^32$) divides $m - 1$. This means that in
+//! practice the last constraint is simplified to
+//!
+//! 4) $(h = H) \implies (\ell = 0)$.
+//!
+//! We always enforce the last three conditions with constraints, in
+//! [`Config::range_check_decomp`]. We can only enforce the first
+//! condition when $F_b = F_m$, since otherwise $\alpha$ is not
+//! representable directly in $F_b$; but this condition is never
+//! enforced by `range_check_decomp`.
+//!
+//! Decomposition is provided by [`Config::decompose_field_elem`].
+//!
+//! See the decomposition chapter of the
+//! [Halo 2 book](http://localhost:3000/design/gadgets/ecc/decomposition.html#hl-decomp)
+//! for more details.
+use crate::{
+ ecc::chip::EccScalarVarFullWidth,
+ sinsemilla::primitives as sinsemilla,
+ utilities::{self, generic_range_check, pow2_range_check},
+};
+
+use halo2_proofs::{
+ circuit::{AssignedCell, Layouter, Value},
+ plonk::{Advice, Assigned, Column, ConstraintSystem, Constraints, Error, Expression, Selector},
+ poly::Rotation,
+};
+use halo2curves::{
+ pasta::{pallas, vesta},
+ CurveAffine,
+};
+
+use ff::{Field, FieldBits, PrimeField, PrimeFieldBits};
+
+/// Trait for scalar and base fields of `C`.
+///
+/// If `F: ScalarOrBase` then `F = C::Scalar` or `F = C::Base`, but
+/// we can't actually enforce that directly. See e.g. use in
+/// [`UncheckedDecomp`] below.
+pub trait ScalarOrBase {}
+impl ScalarOrBase for pallas::Base {}
+impl ScalarOrBase for pallas::Scalar {}
+impl ScalarOrBase for vesta::Base {}
+impl ScalarOrBase for vesta::Scalar {}
+
+/// An unchecked `K`-high-low decomp of a `C`-base or scalar element `value`.
+///
+/// The `value` is optional, since it's not always known in practice
+/// (e.g. for decomps used by [`crate::transcript`]).
+struct UncheckedDecomp, const K: usize> {
+ pub value: Option>,
+ pub high: AssignedCell,
+ pub low: AssignedCell,
+}
+
+/// A range checked `K`-high-low decomp of a `C`-base or scalar element `value`.
+///
+/// Like [`UncheckedDecomp`], except the invariant is that `high` and
+/// `low` have been range constrained in the circuit to be a canonical
+/// `K`-high-low decomp of an `S` element. Note that range checking
+/// does not imply any relationship between `value` and `high` and
+/// `low`; indeed, `value` could be unknown.
+struct RangeCheckedDecomp, const K: usize> {
+ value: Option>,
+ high: AssignedCell,
+ low: AssignedCell,
+}
+
+#[derive(Copy, Clone, Debug, Eq, PartialEq)]
+/// Config struct for full-width scalar decomposition and range check.
+pub struct Config
+where
+ C::Base: PrimeFieldBits,
+{
+ /// Selector for range checking `h` and `l`.
+ q_range_check: Selector,
+ /// Config for pow2 range checks.
+ pow2_config: pow2_range_check::Config,
+ /// Config for range checks.
+ rc_config: generic_range_check::Config,
+ /// High bits of things.
+ high: Column,
+ /// Low bits of things.
+ low: Column,
+}
+
+impl Config
+where
+ C::Scalar: PrimeFieldBits + ScalarOrBase,
+ C::Base: PrimeFieldBits + ScalarOrBase,
+{
+ /// Configure full-width scalar decomp gadget.
+ pub fn configure(
+ meta: &mut ConstraintSystem,
+ pow2_config: pow2_range_check::Config,
+ high: Column,
+ low: Column,
+ ) -> Self {
+ meta.enable_equality(high);
+ meta.enable_equality(low);
+ let rc_config = generic_range_check::Config::configure(meta, [high, low], pow2_config);
+ let config = Self {
+ q_range_check: meta.selector(),
+ pow2_config,
+ rc_config,
+ high,
+ low,
+ };
+ config.create_gate(meta);
+ config
+ }
+
+ /// Create a gate to constrain the canonicality of the decomposition.
+ fn create_gate(&self, meta: &mut ConstraintSystem) {
+ // Constrain the canonicality of the decomposition.
+ //
+ // The assignment layout:
+ //
+ // | high | low | offset |
+ // |----------|------------|--------|
+ // | h | l | 0 | <-- q_range_check enabled here
+ // | h_max | eta | 1 |
+ // ```
+ meta.create_gate("High-low-decomp canonicity range check", |meta| {
+ let q_range_check = meta.query_selector(self.q_range_check);
+ let h = meta.query_advice(self.high, Rotation::cur());
+ let l = meta.query_advice(self.low, Rotation::cur());
+ let h_max = meta.query_advice(self.high, Rotation::next());
+ let eta = meta.query_advice(self.low, Rotation::next());
+
+ let one = Expression::Constant(C::Base::ONE);
+
+ // Constituant constraints:
+ //
+ // Constrain `l < L`, which means `l = 0`.
+ //
+ // All of the fields we decompose from have moduli
+ // where `L` is always 1, since all our fields are
+ // chosen to have high 2-adicity to support efficient
+ // FFT: i.e. a large power of 2 divides `m-1`, meaning
+ // that the last many bits of `m` are of the form
+ // `0...01`. This assumption is enforced with an
+ // assert in `range_check_decomp()`, and even it
+ // weren't, the check here would still be sound, it
+ // would just be overly restrictive.
+ let l_lt_max = l;
+ // Constrain `h = h_max`, where `h_max = H`, the high
+ // `N-K` bits of the field modulus.
+ let h_is_max = h.clone() - h_max;
+ // Constrain `h ≠ h_max` for use in constraining
+ // `(h = h_max) => (l = 0)`.
+ //
+ // This one is a little subtle: constraints are
+ // encoded to be true when they're zero, and
+ // false otherwise. So to logically negate ("not") a
+ // constraint c, we need an expression that is zero
+ // when the c is non-zero and non-zero when c is
+ // zero. This condition on c can be expressed as
+ //
+ // there exists eta s.t. 1 - c*eta = 0
+ //
+ // Now if c is zero, there is no eta that satisfies
+ // the above formula. But if c is non-zero, we can use
+ // eta = 1/c.
+ //
+ // In practice, we compute not(x) = 1 - c*inv0(x),
+ // where inv0(x) = 1/x when x is non-zero, and inv0(0)
+ // = 0. I.e. we choose eta = inv0(x). The library
+ // function that computes inv0() is called invert().
+ //
+ // Ok, but what if eta is not calculated correctly?
+ // Afterall, there are no constraints on eta, it's
+ // just something we're pulling out of an assigned
+ // cell! Well, if we're using not(c) to encode
+ //
+ // (c => d) == (not(c) \/ d) == ((1 - c*eta) * d)
+ //
+ // then consider two cases:
+ //
+ // 1) if c = 0, then no matter what eta is, 1 - c*eta
+ // will never be zero (true), so d will necessarily
+ // be zero (true) if ((1 - c*eta) * d) is
+ // satisfied. I.e. if c is satisfied then d is
+ // satisfied, i.e. (c => d) when c is true.
+ //
+ // 2) if c ≠ 0, then (c => d) is true independent of
+ // d. Now either ((1 - c*eta) * d) is zero (true),
+ // because eta was chosen correctly, or ((1 -
+ // c*eta) * d) is non-zero (false), and the
+ // constraints aren't satisfied.
+ //
+ // In other words, ((1 - c*eta) * d) is true implies
+ // (c => d) is true, and so this encoding is sound. It
+ // may not be complete, because a moronic prover could
+ // choose the wrong eta, but there's no way for a
+ // malicious prover to make ((1 - c*eta) * d) true
+ // when (c => d) would be false.
+ let h_is_not_max = one - h_is_max * eta;
+
+ // Compound constraints:
+ //
+ // We want to check all of
+ //
+ // - l < 2^K
+ // - already checked in the assignment function using strict range check
+ // - h = h_max => l = 0
+ // - which is equivalent to
+ // - h ≠ h_max \/ l = 0
+ // - h <= h_max
+ // - already checked in the assignment function using strict range check
+ Constraints::with_selector(
+ q_range_check,
+ [("(h = h_max) => (l < l_max)", h_is_not_max * l_lt_max)],
+ )
+ });
+ }
+
+ /// Decompose an `C::Scalar` scalar `scalar` into high and low bits `h`
+ /// and `l` s.t. `scalar = 2*h + l`, witness and range check the
+ /// decomposition, and return it.
+ ///
+ /// Note: this does not enforce any relationship between `scalar`
+ /// and the resulting decomp.
+ pub fn k1_decomp_and_range_check_scalar(
+ &self,
+ layouter: &mut impl Layouter,
+ scalar: Value,
+ ) -> Result, Error> {
+ let decomp = self.decompose_field_elem::(layouter, scalar)?;
+ let decomp = self.range_check_decomp(layouter, decomp)?;
+ let result = EccScalarVarFullWidth {
+ value: scalar,
+ alpha_high: decomp.high,
+ alpha_0: decomp.low,
+ };
+ Ok(result)
+ }
+
+ /// Range constrain `high` and `low` to be a canonical `K=1`-high-low
+ /// decomposition of a `C::Scalar`-field scalar.
+ ///
+ /// Note that we don't actually check that `high` and `low` are a
+ /// decomposition of some scalar `alpha`, i.e. that `alpha =
+ /// 2*high + low`, since we can't witness a `alpha` from
+ /// `C::Scalar` in our `C::Base` circuit. Hence it's still up to
+ /// the user to check that the decomposition correctly decomposes
+ /// some `C::Scalar`, if they care about that.
+ pub(crate) fn range_check_k1_scalar_decomp(
+ &self,
+ layouter: &mut impl Layouter,
+ high: AssignedCell,
+ low: AssignedCell,
+ ) -> Result<(), Error> {
+ let decomp = UncheckedDecomp:: {
+ value: None,
+ high,
+ low,
+ };
+ self.range_check_decomp(layouter, decomp)?;
+ Ok(())
+ }
+
+ /// Constrain `decomp` to be a canonical `K`-high-low
+ /// decomposition of some `S` elem.
+ ///
+ /// Note that we don't actually check that `decomp` is a
+ /// decomposition of a specific `alpha`, i.e. that `alpha = 2^K *
+ /// decomp.high + decomp.low`, since in the case of full-width
+ /// `alpha` from `C::Scalar`, we can't witness `alpha` in our
+ /// `F_b` circuit anyway, and in some cases the `alpha` may not be
+ /// known.
+ fn range_check_decomp(
+ &self,
+ layouter: &mut impl Layouter,
+ decomp: UncheckedDecomp,
+ ) -> Result, Error>
+ where
+ // We know that `S` is `C::Base` or `C::Scalar`, but the type
+ // system does not :/
+ S: ScalarOrBase + PrimeFieldBits,
+ {
+ let (h_max, l_max) = Self::decompose_modulus::();
+ assert_eq!(
+ l_max,
+ C::Base::ONE,
+ "We assume the low K-bits represent the number 1. This should always be true for small K due to 2-adicity."
+ );
+ let h = decomp.high.clone();
+ // `h <= h_max` iff `h < h_max + 1`.
+ let bound = h_max + C::Base::ONE;
+ // Constrain `h <= h_max`.
+ let strict = true;
+ self.rc_config.range_check(
+ layouter.namespace(|| "h <= h_max"),
+ h.clone(),
+ bound,
+ strict,
+ )?;
+
+ // Constrain `l < 2^K`.
+ let l = decomp.low.clone();
+ let strict = true;
+ self.pow2_config
+ .pow2_range_check(layouter.namespace(|| "l < 2^K"), l, K, strict)?;
+
+ // Resulting layout, as consumed by `create_gate`:
+ //
+ // ```text
+ // | high | low | offset |
+ // |----------|------------|--------|
+ // | h | l | 0 | <-- q_range_check enabled here
+ // | h_max | eta | 1 |
+ // ```
+ layouter.assign_region(
+ || "high-low-decomp range check",
+ |mut region| {
+ region.name_column(|| "high", self.high);
+ region.name_column(|| "low", self.low);
+
+ self.q_range_check.enable(&mut region, 0)?;
+
+ h.copy_advice(|| "h", &mut region, self.high, 0)?;
+ decomp.low.copy_advice(|| "l", &mut region, self.low, 0)?;
+ region.assign_advice_from_constant(|| "h_max", self.high, 1, h_max)?;
+ // Witness the `eta := inv0(h - h_max)`, where
+ // `inv0(x) = 0` if `x = 0`, and `1/x` otherwise.
+ let h_minus_h_max = h.value().map(|&h| h - h_max);
+ let eta = h_minus_h_max.map(|h_minus_h_max| Assigned::from(h_minus_h_max).invert());
+ region.assign_advice(|| "eta", self.low, 1, || eta)?;
+
+ Ok(RangeCheckedDecomp {
+ value: decomp.value,
+ high: decomp.high.clone(),
+ low: decomp.low.clone(),
+ })
+ },
+ )
+ }
+
+ /// Decompose a field elem from the base or scalar field into
+ /// `K`-high-low decomp in the base field.
+ fn decompose_field_elem(
+ &self,
+ layouter: &mut impl Layouter,
+ value: Value,
+ ) -> Result, Error>
+ where
+ S: ScalarOrBase + PrimeFieldBits,
+ {
+ let (high, low) = value
+ .map(|value| {
+ let bits = value.to_le_bits();
+ Self::decompose_bits::(bits)
+ })
+ .unzip();
+ layouter.assign_region(
+ || "Decompose scalar",
+ |mut region| {
+ let offset = 0;
+ let high = region.assign_advice(|| "h", self.high, offset, || high)?;
+ let low = region.assign_advice(|| "l", self.low, offset, || low)?;
+ Ok(UncheckedDecomp {
+ value: Some(value),
+ high,
+ low,
+ })
+ },
+ )
+ }
+
+ /// Decompose `bits` into `K`-high-low decomp in base
+ /// field. Returns pair `(high, low)`.
+ ///
+ /// The `FieldBits` is meant to imply that `bits`
+ /// will have length at least `N`, for `N` the bit-width of
+ /// `C::Base` and `C::Scalar`; we assert this internally.
+ fn decompose_bits(bits: FieldBits) -> (C::Base, C::Base)
+ where
+ S: ScalarOrBase + PrimeFieldBits,
+ {
+ let mut bits = bits.into_iter();
+ let low_bits: Vec = bits.by_ref().take(K).collect();
+ let high_bits: Vec = bits.collect();
+ let low = utilities::le_bits_to_field_elem(&low_bits);
+ let high = utilities::le_bits_to_field_elem(&high_bits);
+
+ // Assert that input is well formed.
+ //
+ // It seems the number of bits in the input `bits` gets
+ // rounded up to the nearest multiple of 8 when computed by
+ // `PrimeFieldBits::{to_le_bits,char_le_bits}`, so we can't
+ // simply check that the number of input bits here is *equal*
+ // to the bit-width of the field. But it should never be less.
+ let num_observed_bits = low_bits.len() + high_bits.len();
+ let num_expected_bits = C::Base::NUM_BITS as usize;
+ assert!(
+ num_observed_bits >= num_expected_bits,
+ "The `bits` are too short! bits.len(): {}, C::Base::NUM_BITS: {}",
+ num_observed_bits,
+ num_expected_bits
+ );
+
+ (high, low)
+ }
+
+ /// Decompose the modulus of the source field into a `K`-high-low
+ /// decomp in the base field. Returns pair `(high, low)`.
+ fn decompose_modulus() -> (C::Base, C::Base)
+ where
+ S: ScalarOrBase + PrimeFieldBits,
+ {
+ let bits = S::char_le_bits();
+ Self::decompose_bits::(bits)
+ }
+}
+
+/// Tests for `K`-high-low decomposition.
+///
+/// These tests are for Pallas and Vesta, but they should also work
+/// for Pluto and Eris, if we replace the `U256` usage with something
+/// large enough for Pluto/Eris, e.g. `U512`.
+///
+/// Some of these tests -- prefixed with `k1_` -- were originally
+/// written for a different implementation of the `1`-high-low decomp,
+/// but the implementation has since been greatly simplified by using
+/// the newer generic range check gadget. However, the the generic
+/// range check gadget internally implements a generalization of the
+/// approach that used to be implemented here for `1`-high-low decomp,
+/// so the specific values tested here, altho not all obviously
+/// motivated by the code in this file, should still do a good job of
+/// testing the underlying generic range check gadget.
+#[cfg(test)]
+mod tests {
+ use crate::{
+ ecc::chip::{T_P, T_Q},
+ utilities::{
+ high_low_decomp::UncheckedDecomp, lookup_range_check::LookupRangeCheckConfig,
+ pow2_range_check,
+ },
+ };
+ use ff::{Field, FromUniformBytes, PrimeField, PrimeFieldBits};
+ use halo2_proofs::{
+ circuit::{Layouter, SimpleFloorPlanner, Value},
+ dev::MockProver,
+ plonk::{Advice, Circuit, Column, ConstraintSystem},
+ };
+ use halo2curves::{
+ pasta::{pallas, vesta},
+ CurveAffine,
+ };
+ use rand::{random, rngs::OsRng};
+
+ // Copied from
+ // ecc:chip::mul::decompose_for_scalar_mul(). I don't
+ // understand why there isn't some more natural way to
+ // convert an ff point to an int???
+ #[allow(clippy::assign_op_pattern)]
+ mod uint {
+ use uint::construct_uint;
+ construct_uint! {
+ pub(super) struct U256(4);
+ }
+ }
+ use uint::U256;
+
+ use super::ScalarOrBase;
+
+ /// (q - 1)/2 = (2^254 + t_q - 1)/2 = 2^253 + (t_q - 1)/2
+ fn q12() -> pallas::Base {
+ // 2^253.
+ let two_253 = pallas::Base::one().double().pow([253]);
+ // (t_q - 1)/2.
+ let delta = (pallas::Base::from_u128(T_Q) - pallas::Base::one())
+ * pallas::Base::from_u128(2).invert().unwrap();
+ two_253 + delta
+ }
+
+ /// 2^130
+ fn two_130() -> pallas::Base {
+ pallas::Base::from_u128(1 << 127) * pallas::Base::from_u128(1 << 3)
+ }
+
+ /// 2^253
+ fn two_253() -> pallas::Base {
+ pallas::Base::from_u128(1 << 125).square() * pallas::Base::from_u128(1 << 3)
+ }
+
+ /// (t_q + 1)/2
+ fn delta() -> pallas::Base {
+ (pallas::Base::from_u128(T_Q) + pallas::Base::one())
+ * pallas::Base::from_u128(2).invert().unwrap()
+ }
+
+ /// Test modes for the scalar decomposition gadget.
+ #[derive(Copy, Clone)]
+ enum TestMode {
+ /// Decompose the provided scalar, range check the result, and
+ /// check that the decomposition is correct.
+ CombinedDecompAndRangeCheck {
+ scalar: S,
+ },
+ /// Check that the provided decomposition is canonical.
+ InRangeDecomp {
+ high: C::Base,
+ low: C::Base,
+ },
+ /// Check that the provided decomposition is non-canonical.
+ OutOfRangeDecomp {
+ high: C::Base,
+ low: C::Base,
+ },
+ NoTest,
+ }
+
+ /// Computes a single scalar decomposition.
+ /// Useful for finding the characteristics of the scalar decomposition gadget
+ #[derive(Clone, Copy)]
+ struct ScalarDecompCircuit {
+ mode: TestMode,
+ }
+
+ #[derive(Debug, Clone)]
+ struct ScalarDecompConfig
+ where
+ C::Base: PrimeFieldBits,
+ {
+ scalar_decomp: super::Config,
+ lookup: LookupRangeCheckConfig,
+ }
+
+ /// Trait-bound alias for all the constraints we want on our
+ /// source fields `S` in tests.
+ ///
+ /// Convenient trait aliases are only available in "nightly":
+ /// https://github.com/rust-lang/rust/issues/41517
+ trait TestField:
+ ScalarOrBase + PrimeFieldBits + FromUniformBytes<64>
+ // Need this for use with `PrimeField.to_repr()` to convert to `U256`.
+ + PrimeField
+ {
+ }
+ impl TestField for S where
+ S: ScalarOrBase + PrimeFieldBits + FromUniformBytes<64> + PrimeField
+ {
+ }
+
+ impl, const K: usize> Circuit
+ for ScalarDecompCircuit
+ where
+ // Unfortunately, we can't simply define a `TestCurve` trait
+ // analogous to `TestField` to handle these repetitive
+ // constraints for us:
+ // https://github.com/rust-lang/rust/issues/20671#issuecomment-1898036619
+ C::Base: TestField,
+ C::Scalar: TestField,
+ {
+ type Config = ScalarDecompConfig;
+
+ type FloorPlanner = SimpleFloorPlanner;
+
+ #[cfg(feature = "circuit-params")]
+ type Params = ();
+
+ fn without_witnesses(&self) -> Self {
+ Self {
+ mode: TestMode::NoTest,
+ }
+ }
+
+ fn configure(meta: &mut ConstraintSystem) -> Self::Config {
+ let advices: [Column; 3] = [
+ meta.advice_column(),
+ meta.advice_column(),
+ meta.advice_column(),
+ ];
+
+ // Avoid errors about "too few fixed columns are enabled for
+ // global constants usage".
+ let constants = meta.fixed_column();
+ meta.enable_constant(constants);
+
+ let lookup_table = meta.lookup_table_column();
+ let lookup_config = LookupRangeCheckConfig::configure(meta, advices[0], lookup_table);
+ let pow2_config = pow2_range_check::Config::configure(meta, advices[0], lookup_config);
+ let scalar_decomp = super::Config::configure(meta, pow2_config, advices[1], advices[2]);
+ Self::Config {
+ scalar_decomp,
+ lookup: lookup_config,
+ }
+ }
+
+ fn synthesize(
+ &self,
+ config: Self::Config,
+ mut layouter: impl Layouter,
+ ) -> Result<(), halo2_proofs::plonk::Error> {
+ // Load 10-bit lookup table. In the Action circuit, this will be
+ // provided by the Sinsemilla chip.
+ config.lookup.load(&mut layouter)?;
+
+ match self.mode {
+ // Do a decomposition, range check the result, and
+ // check that the decomposition is correct.
+ TestMode::<_, _, K>::CombinedDecompAndRangeCheck { scalar } => {
+ let decomp = config
+ .scalar_decomp
+ .decompose_field_elem::<_, K>(&mut layouter, Value::known(scalar))?;
+ let decomp = config
+ .scalar_decomp
+ .range_check_decomp(&mut layouter, decomp)?;
+ // Check correctness of decomp.
+ decomp.high.value().zip(decomp.low.value()).map(|(h, l)| {
+ assert_eq!(
+ U256::from_little_endian(&scalar.to_repr()),
+ U256::from(1 << K) * U256::from_little_endian(&h.to_repr())
+ + U256::from_little_endian(&l.to_repr()),
+ "Decomposition must satisfy alpha = 2^K * h + l!"
+ );
+ });
+ }
+ // Manually construct a decomposition and range check.
+ // Whether we expect this to verify or not depends on
+ // the mode.
+ TestMode::::OutOfRangeDecomp { high, low }
+ | TestMode::::InRangeDecomp { high, low } => {
+ let decomposed_scalar = layouter.assign_region(
+ || "Full-width variable-base mul (assign full-width scalar)",
+ |mut region| {
+ let offset = 0;
+ let high = region.assign_advice(
+ || "high",
+ config.scalar_decomp.high,
+ offset,
+ || Value::known(high),
+ )?;
+ let low = region.assign_advice(
+ || "low",
+ config.scalar_decomp.low,
+ offset,
+ || Value::known(low),
+ )?;
+ Ok(UncheckedDecomp:: {
+ value: None,
+ high,
+ low,
+ })
+ },
+ )?;
+ config
+ .scalar_decomp
+ .range_check_decomp(&mut layouter, decomposed_scalar)?;
+ }
+ TestMode::NoTest => (),
+ }
+ Ok(())
+ }
+ }
+
+ fn test_ok, const K: usize>(mode: TestMode)
+ where
+ C::Base: TestField,
+ C::Scalar: TestField,
+ {
+ let circuit = ScalarDecompCircuit { mode };
+ let prover = MockProver::::run(11, &circuit, vec![]).unwrap();
+ // No way to add a custom message to `assert_satisfied()`.
+ prover.assert_satisfied();
+ }
+
+ fn test_err, const K: usize>(mode: TestMode, msg: &str)
+ where
+ C::Base: TestField,
+ C::Scalar: TestField,
+ {
+ let circuit = ScalarDecompCircuit { mode };
+ let prover = MockProver::::run(11, &circuit, vec![]).unwrap();
+ assert!(
+ prover.verify().is_err(),
+ "Test was expected to fail but it succeeded! {}",
+ msg
+ );
+ }
+
+ #[test]
+ fn decompose_modulus() {
+ // Implement our own version of the modulus decomp
+ // `super::Config::decompose_modulus` using the modulus
+ // "remainder value" `t_m`: here `t_m := m - 2^254`, for `m`
+ // one of the Pallas/Vesta field moduli.
+ //
+ // This "reference" implementation is totally unrelated to the
+ // "production" implementation, which uses
+ // `PrimeFieldBits::char_le_bits`.
+ fn golden_decompose_modulus(t_m: u128) -> (U256, U256) {
+ let q = (U256::from(1) << 254) + U256::from(t_m);
+ let high = q >> K;
+ // Here `2^K - 1` is the number with binary repr of `K`
+ // 1-bits in a row, i.e. the mask for the low `K` bits.
+ let low = q & ((U256::from(1) << K) - 1);
+ (high, low)
+ }
+
+ fn test_one_k, const K: usize>(t: u128)
+ where
+ C::Base: TestField,
+ C::Scalar: TestField,
+ {
+ let (golden_high, golden_low) = golden_decompose_modulus::(t);
+ let (high, low) = super::Config::::decompose_modulus::();
+ let high = U256::from_little_endian(&high.to_repr());
+ let low = U256::from_little_endian(&low.to_repr());
+ assert_eq!(golden_high, high, "High parts aren't equal!");
+ assert_eq!(golden_low, low, "Low parts aren't equal!");
+ }
+
+ // No known use case K > 3, but try a few more.
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ test_one_k::(T_P);
+ test_one_k::(T_Q);
+ }
+
+ const ITERS: usize = 5;
+
+ #[test]
+ /// This test includes a random in-range decomp test internally,
+ /// so we don't implement a separate `random_in_range_decomp()`
+ /// test.
+ fn random_combined_decomp_and_range_check() {
+ fn test_one, const K: usize>()
+ where
+ C::Base: TestField,
+ C::Scalar: TestField,
+ {
+ for _ in 0..ITERS {
+ let scalar: S = S::random(OsRng);
+ let mode = TestMode::::CombinedDecompAndRangeCheck { scalar };
+ test_ok(mode);
+ }
+ }
+
+ // No known use case K > 3, but try a few more.
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ }
+
+ #[test]
+ fn random_out_of_range_decomp() {
+ fn test_one, const K: usize>()
+ where
+ C::Base: TestField,
+ C::Scalar: TestField,
+ {
+ for _ in 0..ITERS {
+ let (h_max, l_max) = super::Config::::decompose_modulus::();
+
+ // Test the smallest overflowing value, i.e. the
+ // modulus itself.
+ let mode = TestMode::::OutOfRangeDecomp {
+ high: h_max,
+ low: l_max,
+ };
+ test_err(mode, "modulus");
+
+ // Test values that randomly overflow the high part.
+ let delta = C::Base::from_u128(random());
+ let high = h_max + delta;
+ let low = C::Base::ZERO;
+ let mode = TestMode::::OutOfRangeDecomp { high, low };
+ test_err(mode, "random high overflow");
+
+ // Test values that randomly overflow the low part.
+ let high = C::Base::ZERO;
+ let low = l_max + delta;
+ let mode = TestMode::::OutOfRangeDecomp { high, low };
+ test_err(mode, "random low overflow");
+ }
+ }
+
+ // No known use case K > 3, but try a few more.
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ test_one::();
+ }
+
+ #[test]
+ fn k1_combined_decomp_and_range_check() {
+ let zero = pallas::Scalar::zero();
+ let one = pallas::Scalar::one();
+ let two_253 = pallas::Scalar::from_repr(two_253().to_repr()).unwrap();
+ let two_254 = two_253.double();
+ let delta = pallas::Scalar::from_repr(delta().to_repr()).unwrap();
+ let scalars = [
+ ("zero", zero),
+ ("one", one),
+ ("delta", delta),
+ ("2^253", two_253),
+ ("2^254", two_254),
+ // q-1. This covers the only case where high = (q-1)/2 is allowed.
+ ("q - 1", pallas::Scalar::one().neg()),
+ ];
+ let random_scalars: [(&str, pallas::Scalar); 10] = (0..10)
+ .map(|_| {
+ let scalar = pallas::Scalar::random(OsRng);
+ ("random scalar", scalar)
+ })
+ .collect::>()
+ .try_into()
+ .unwrap();
+ for (_msg, scalar) in scalars.iter().chain(random_scalars.iter()) {
+ let mode = TestMode::::CombinedDecompAndRangeCheck {
+ scalar: *scalar,
+ };
+ test_ok(mode);
+ }
+ }
+
+ #[test]
+ fn k1_in_range_decomp() {
+ let zero = pallas::Base::zero();
+ let one = pallas::Base::one();
+ let pairs = [
+ // Exercise the `high in [0, 2^253)` part of the range check.
+ ("(0,0)", zero, zero),
+ ("(2^253 - 1, 1)", two_253() - one, one),
+ // Exercise corner cases for the `high in [2^253, 2^253 + delta)` part of
+ // the range check.
+ ("(2^253, 0)", two_253(), one),
+ (
+ "(2^253 - 2^130 + delta, 1)",
+ two_253() - two_130() + delta(),
+ one,
+ ),
+ ("(2^253 + delta - 1, 0)", two_253() + delta() - one, zero),
+ // The only case where high = (q-1)/2 is allowed.
+ ("((q-1)/2, 0)", q12(), zero),
+ ];
+ for (_msg, high, low) in pairs.iter() {
+ let mode = TestMode::::OutOfRangeDecomp {
+ high: *high,
+ low: *low,
+ };
+ test_ok(mode);
+ }
+ }
+
+ #[test]
+ fn k1_out_of_range_decomp() {
+ let zero = pallas::Base::zero();
+ let one = pallas::Base::one();
+ let two = one.double();
+ let p = one.neg();
+ let pairs = [
+ // low is out of range.
+ ("(0, 2)", zero, two),
+ // high is out of range.
+ ("(p, 0)", p, zero),
+ ("(2^254, 0)", two_253().double(), zero),
+ ("(2^254, 1)", two_253().double(), one),
+ ("((q-1)/2 + 1, 0)", q12() + one, zero),
+ ("(2^253 + 2^130, 1)", two_253() + two_130(), one),
+ // high is out of range because low is not zero.
+ ("((q-1)/2, 1)", q12(), one),
+ ];
+ for (msg, high, low) in pairs.iter() {
+ let mode = TestMode::::OutOfRangeDecomp {
+ high: *high,
+ low: *low,
+ };
+ test_err(mode, msg);
+ }
+ }
+}
diff --git a/halo2_gadgets/src/utilities/pow2_range_check.rs b/halo2_gadgets/src/utilities/pow2_range_check.rs
index a9f688c00..dae84f07b 100644
--- a/halo2_gadgets/src/utilities/pow2_range_check.rs
+++ b/halo2_gadgets/src/utilities/pow2_range_check.rs
@@ -191,7 +191,7 @@ impl Config {
// If `r == 0`, we just assign `low_r_bits` to zero. We use
// `assign_advice_from_constant`, so this guarantees that `r =
// 0` / the prover can't cheat, and we don't need to do the
- // `short_range_check` from the `r /= 0` branch.
+ // `short_range_check` from the `r ≠ 0` branch.
let low_r_bits = if r == 0 {
layouter.assign_region(
|| "low_r_bits (== 0)",