Merge pull request privacy-scaling-explorations#114 from input-output…

…-hk/dev-feature/gl-113-gen-decomp

Implement K-high-low decomposition and range checking

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
 

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<F>::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.

halo2_gadgets/benches/ecc_circuits/scalar_mul.rs

@@ -103,8 +103,8 @@ impl Circuit<pallas::Base> 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<pallas::Base> 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<pallas::Affine>, ScalarVar)> = None;
         for _ in 0..SCALAR_MUL_ITER {

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<C: CurveAffine> {
     /// The full-width scalar, alpha.
-    value: Value<C::Scalar>,
+    pub(crate) value: Value<C::Scalar>,
     /// The high bits of alpha, i.e. alpha >> 1.
-    alpha_high: AssignedCell<C::Base, C::Base>,
+    pub(crate) alpha_high: AssignedCell<C::Base, C::Base>,
     // The original WIP API used `AssignedCell<bool, C::Base>`, but
     // only `AssignedCell<C::Base, C::Base>` is well supported by the
     // rest of the codebase.
     /// The low bit of alpha, i.e. alpha & 1.
-    alpha_0: AssignedCell<C::Base, C::Base>,
+    pub(crate) alpha_0: AssignedCell<C::Base, C::Base>,
 }
 
 impl<C: CurveAffine> EccScalarVarFullWidth<C> {
@@ -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))
     }
 }

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<pallas::Affine>,
 }
 
 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<pallas::Affine>,
             lookup: LookupRangeCheckConfig<pallas::Base, 10>,
         }
 
@@ -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,