From 6b4a3e6360ac52ac73a270b48f2c040c264ca398 Mon Sep 17 00:00:00 2001 From: Nathan Collins Date: Thu, 4 Jan 2024 14:03:32 +0800 Subject: [PATCH 1/7] Rename `ecc::chip::mul::full_width` to `utilities::high_low_decomp` And update imports accordingly. This is in antcipation of generalizing the full-width decomp to support more fields and low bit-widths. --- halo2_gadgets/src/ecc/chip.rs | 8 +++--- halo2_gadgets/src/ecc/chip/mul.rs | 13 +++++---- halo2_gadgets/src/transcript.rs | 27 +++++++++++-------- halo2_gadgets/src/utilities.rs | 1 + .../high_low_decomp.rs} | 11 ++++---- 5 files changed, 33 insertions(+), 27 deletions(-) rename halo2_gadgets/src/{ecc/chip/mul/full_width.rs => utilities/high_low_decomp.rs} (98%) diff --git a/halo2_gadgets/src/ecc/chip.rs b/halo2_gadgets/src/ecc/chip.rs index c4a993ffc..75a2e6246 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 { diff --git a/halo2_gadgets/src/ecc/chip/mul.rs b/halo2_gadgets/src/ecc/chip/mul.rs index f4d144ad6..ed4494eb2 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; @@ -66,7 +65,7 @@ pub struct Config { /// Configuration used to check for overflow overflow_config: overflow::Config, /// Configuration used for full-width scalars - pub full_width_config: full_width::Config, + pub full_width_config: high_low_decomp::Config, } impl Config { @@ -88,7 +87,7 @@ impl 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]); + high_low_decomp::Config::configure(meta, pow2_config, advices[0], advices[1]); let config = Self { q_mul_lsb: meta.selector(), @@ -864,9 +863,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 +878,7 @@ pub mod tests { #[derive(Debug, Clone)] struct BenchScalarDecompSmall { - scalar_decomp: full_width::Config, + scalar_decomp: high_low_decomp::Config, lookup: LookupRangeCheckConfig, } @@ -913,7 +912,7 @@ pub mod tests { 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]); + high_low_decomp::Config::configure(meta, pow2_config, advices[1], advices[2]); Self::Config { scalar_decomp, lookup: lookup_config, diff --git a/halo2_gadgets/src/transcript.rs b/halo2_gadgets/src/transcript.rs index c03aa763c..e26aaf993 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()) 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/ecc/chip/mul/full_width.rs b/halo2_gadgets/src/utilities/high_low_decomp.rs similarity index 98% rename from halo2_gadgets/src/ecc/chip/mul/full_width.rs rename to halo2_gadgets/src/utilities/high_low_decomp.rs index a9aaac867..9c1af36c8 100644 --- a/halo2_gadgets/src/ecc/chip/mul/full_width.rs +++ b/halo2_gadgets/src/utilities/high_low_decomp.rs @@ -17,13 +17,11 @@ //! representable directly (indeed, that's the original motivation for //! decomposing it). use crate::{ - ecc::chip::T_Q, + ecc::chip::{EccScalarVarFullWidth, 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}, @@ -312,8 +310,11 @@ impl Config { #[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}, + ecc::chip::{configs, EccScalarVarFullWidth, T_Q}, + utilities::{ + high_low_decomp::uint::U256, lookup_range_check::LookupRangeCheckConfig, + pow2_range_check, + }, }; use ff::{Field, PrimeField}; use halo2_proofs::{ From ddecabc7aa16573a53e996fdd629e47234fb4d0b Mon Sep 17 00:00:00 2001 From: Nathan Collins Date: Thu, 4 Jan 2024 18:00:50 +0800 Subject: [PATCH 2/7] Generalize the high-low decomp to arbitrary curves and Ks This is a substantial rewrite of much of the module. The core algorithm remains the same, but has been generalized to arbitrary curves and low-part bit-widths `K`. Major changes: - all comments were rewritten to reflect the general case. See the new, extensive module level docs for an overview. - everything is in now terms of an arbitrary curve `C` and low-part bit-width `K`, and in many places the source field `S` of the decomposition is also generalized. We only want to consider `S = C::Base` or `S = C::Scalar`, but the type system won't let us express that directly, so we introduce a new trait `S: ScalarOrBase` that captures this. - internally we have new structs `UncheckedDecomp` and `RangeCheckedDecomp`, which are indexed by the low-part bit-width `K` to hopefully reduce any mistakes related to using the wrong `K`. In the future we'll probably expose `RangeCheckedDecomp` as an opaque type: the only way to get one is to run `range_check_decomp` on an `UncheckedDecomp`, but for now it's still internal, since we just changed the existing `EccScalarVarFullWidth`-based APIs to only use these new types internally. - we no longer use the `U256` stuff to decompose, because that depends on the bit-width of the fields. Instead, we now use `PrimeFieldBits::to_le_bits` to get at bit reprs of field elems, and `PrimeFieldBits::char_le_bits` to get at bit reprs of field moduli. The `PrimeFieldBits` trait is not yet implemented for Pluto/Eris, but that should be the only thing stopping this code from working with Pluto and Eris (well, besides also adding the trivial `ScalarOrBase` impls for Pluto and Eris). It remains to add more extensive tests, and update the book documentation. Along the way I also renamed `high_low_decomp::Config::assign` to the more meaningful `k1_decomp_and_range_check_scalar`. --- .../benches/ecc_circuits/scalar_mul.rs | 8 +- halo2_gadgets/src/ecc/chip.rs | 4 +- halo2_gadgets/src/ecc/chip/mul.rs | 23 +- halo2_gadgets/src/transcript.rs | 8 +- .../src/utilities/high_low_decomp.rs | 653 +++++++++++------- 5 files changed, 430 insertions(+), 266 deletions(-) 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 75a2e6246..329dd7f90 100644 --- a/halo2_gadgets/src/ecc/chip.rs +++ b/halo2_gadgets/src/ecc/chip.rs @@ -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 ed4494eb2..a724d67a6 100644 --- a/halo2_gadgets/src/ecc/chip/mul.rs +++ b/halo2_gadgets/src/ecc/chip/mul.rs @@ -64,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: high_low_decomp::Config, + /// Configuration used high-low decomp and range checking + pub decomp_config: high_low_decomp::Config, } impl Config { @@ -85,8 +85,7 @@ 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 = + let decomp_config = high_low_decomp::Config::configure(meta, pow2_config, advices[0], advices[1]); let config = Self { @@ -97,7 +96,7 @@ impl Config { lo_config, complete_config, overflow_config, - full_width_config, + decomp_config, }; config.create_gate(meta); @@ -878,7 +877,7 @@ pub mod tests { #[derive(Debug, Clone)] struct BenchScalarDecompSmall { - scalar_decomp: high_low_decomp::Config, + high_low_decomp: high_low_decomp::Config, lookup: LookupRangeCheckConfig, } @@ -911,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 = + 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, } } @@ -929,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(()) } @@ -1033,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/transcript.rs b/halo2_gadgets/src/transcript.rs index e26aaf993..0d0723cbc 100644 --- a/halo2_gadgets/src/transcript.rs +++ b/halo2_gadgets/src/transcript.rs @@ -93,7 +93,7 @@ pub struct TranscriptConfigBaseFitsInScalar< const WIDTH: usize, const RATE: usize, > { - scalar_decomp: high_low_decomp::Config, + scalar_decomp: high_low_decomp::Config, pow5config: Pow5Config, } @@ -351,7 +351,7 @@ mod test_poseidon_transcript_chip_base_fits_in_scalar { struct MyConfig { outputs: [Column; NOUTPUTS], pow2: pow2_range_check::Config, - scalar: high_low_decomp::Config, + scalar: high_low_decomp::Config, pow5: Pow5Config, x: Column, y: Column, @@ -431,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/high_low_decomp.rs b/halo2_gadgets/src/utilities/high_low_decomp.rs index 9c1af36c8..ae12893e1 100644 --- a/halo2_gadgets/src/utilities/high_low_decomp.rs +++ b/halo2_gadgets/src/utilities/high_low_decomp.rs @@ -1,78 +1,125 @@ -//! Full-width scalar decomposition and range check. +#![allow(rustdoc::private_intra_doc_links)] +//! Implementation of `K`-high-low scalar decomposition and range checking. //! -//! 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. +//! 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`. //! -//! In short, we implement decomposing an Fq scalar $\alpha$ into high -//! and low parts $h$ and $\ell$, s.t. +//! Decomposition is provided by [`Config::decompose_field_elem`]. //! -//! - $\alpha = 2h + \ell$ -//! - $h \le (q-1)/2$ -//! - $\ell$ is boolean +//! TODO(ntc2): update this doc reference after updating book: //! -//! 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). +//! 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. use crate::{ - ecc::chip::{EccScalarVarFullWidth, T_Q}, + ecc::chip::EccScalarVarFullWidth, sinsemilla::primitives as sinsemilla, - utilities::{bool_check, generic_range_check, pow2_range_check}, + utilities::{self, generic_range_check, pow2_range_check}, }; use halo2_proofs::{ - circuit::{Layouter, Region, Value}, + circuit::{AssignedCell, Layouter, 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 +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, } -// 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); - } +/// 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, } -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. +pub struct Config +where + C::Base: PrimeFieldBits, +{ + /// Selector for range checking `h` and `l`. 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, + /// 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 { +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, + meta: &mut ConstraintSystem, + pow2_config: pow2_range_check::Config, high: Column, low: Column, ) -> Self { @@ -81,6 +128,7 @@ impl Config { 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, @@ -90,211 +138,306 @@ impl 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), - ], - ) - }, - ); + 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 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( + /// 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 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) + 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) } - /// 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: + /// Range constrain `high` and `low` to be a canonical `K=1`-high-low + /// decomposition of a `C::Scalar`-field scalar. /// - /// ```text - /// | high | low | offset | - /// |----------|-----|--------| - /// | h | l | 0 | <-- q_range_check enabled here - /// | h_le_max | eta | 1 | - /// ``` - pub(crate) fn range_check( + /// 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, - decomposed_scalar: EccScalarVarFullWidth, + layouter: &mut impl Layouter, + high: AssignedCell, + low: AssignedCell, ) -> 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"), + 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, - false, + 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( - || "decomposed scalar range check", + || "high-low-decomp range check", |mut region| { - // Enable range check. + 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)?; - 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()); + 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(()) + + Ok(RangeCheckedDecomp { + value: decomp.value, + high: decomp.high.clone(), + low: decomp.low.clone(), + }) }, - )?; - 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( + /// Decompose a field elem from the base or scalar field into + /// `K`-high-low decomp in the base field. + fn decompose_field_elem( &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, - }) + 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) } } @@ -310,9 +453,9 @@ impl Config { #[cfg(test)] mod tests { use crate::{ - ecc::chip::{configs, EccScalarVarFullWidth, T_Q}, + ecc::chip::{configs, T_Q}, utilities::{ - high_low_decomp::uint::U256, lookup_range_check::LookupRangeCheckConfig, + high_low_decomp::UncheckedDecomp, lookup_range_check::LookupRangeCheckConfig, pow2_range_check, }, }; @@ -325,7 +468,28 @@ mod tests { use halo2curves::pasta::pallas; use rand::rngs::OsRng; - use super::q12; + // 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; + + /// (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 { @@ -373,7 +537,7 @@ mod tests { #[derive(Debug, Clone)] struct ScalarDecompConfig { - scalar_decomp: configs::ScalarDecompConfig, + scalar_decomp: configs::ScalarDecompConfig, lookup: LookupRangeCheckConfig, } @@ -429,7 +593,7 @@ mod tests { TestMode::CombinedDecompAndRangeCheck { scalar } => { let decomposed_scalar = config .scalar_decomp - .assign(&mut layouter, &Value::known(scalar))?; + .k1_decomp_and_range_check_scalar(&mut layouter, Value::known(scalar))?; decomposed_scalar .alpha_high .value() @@ -439,7 +603,7 @@ mod tests { 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!" + "Decomposition must satisfy alpha = 2*h + l!" ); }); } @@ -464,17 +628,16 @@ mod tests { 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, + Ok(UncheckedDecomp:: { + value: None, + high, + low, }) }, )?; config .scalar_decomp - .range_check(&mut layouter, decomposed_scalar)?; + .range_check_decomp(&mut layouter, decomposed_scalar)?; } TestMode::NoTest => (), } From 4789545da160aa5352f795a261dbd341c7026def Mon Sep 17 00:00:00 2001 From: Nathan Collins Date: Thu, 18 Jan 2024 11:40:06 +0800 Subject: [PATCH 3/7] No-op-refactor existing tests Generalize existing test setup and `K=1` and `S=pallas::Scalar` tests to general low-bit-width `K` and source field `S` type params. Remains to actually add tests for different `K` and `S`. Also, factor out running tests into new `test_ok()` and `test_err()` funs, and use `prover.assert_satisfied()` in the `test_ok()` case to get better debug output. Unfortunately, `assert_satisfied()` doesn't support custom messages, so we can no longer use the existing descriptive messages in this case to add more context to test failures. --- .../src/utilities/high_low_decomp.rs | 137 ++++++++++-------- 1 file changed, 74 insertions(+), 63 deletions(-) diff --git a/halo2_gadgets/src/utilities/high_low_decomp.rs b/halo2_gadgets/src/utilities/high_low_decomp.rs index ae12893e1..47685f1ef 100644 --- a/halo2_gadgets/src/utilities/high_low_decomp.rs +++ b/halo2_gadgets/src/utilities/high_low_decomp.rs @@ -459,7 +459,7 @@ mod tests { pow2_range_check, }, }; - use ff::{Field, PrimeField}; + use ff::{Field, PrimeField, PrimeFieldBits}; use halo2_proofs::{ circuit::{Layouter, SimpleFloorPlanner, Value}, dev::MockProver, @@ -481,6 +481,8 @@ mod tests { } 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. @@ -509,11 +511,11 @@ mod tests { /// Test modes for the scalar decomposition gadget. #[derive(Copy, Clone)] - enum TestMode { + enum TestMode { /// Decompose the provided scalar, range check the result, and /// check that the decomposition is correct. CombinedDecompAndRangeCheck { - scalar: pallas::Scalar, + scalar: S, }, /// Check that the provided decomposition is canonical. InRangeDecomp { @@ -531,8 +533,8 @@ mod tests { /// Computes a single scalar decomposition. /// Useful for finding the characteristics of the scalar decomposition gadget #[derive(Clone, Copy)] - struct ScalarDecompCircuit { - mode: TestMode, + struct ScalarDecompCircuit { + mode: TestMode, } #[derive(Debug, Clone)] @@ -541,7 +543,23 @@ mod tests { lookup: LookupRangeCheckConfig, } - impl Circuit for ScalarDecompCircuit { + /// 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 + // Need this for use with `PrimeField.to_repr()` to convert to `U256`. + + PrimeField + { + } + impl TestField for S where + S: ScalarOrBase + PrimeFieldBits + PrimeField + { + } + + impl Circuit for ScalarDecompCircuit { type Config = ScalarDecompConfig; type FloorPlanner = SimpleFloorPlanner; @@ -590,28 +608,28 @@ mod tests { match self.mode { // Do a decomposition, range check the result, and // check that the decomposition is correct. - TestMode::CombinedDecompAndRangeCheck { scalar } => { - let decomposed_scalar = config + TestMode::<_, K>::CombinedDecompAndRangeCheck { scalar } => { + let decomp = config + .scalar_decomp + .decompose_field_elem::<_, K>(&mut layouter, Value::known(scalar))?; + let decomp = config .scalar_decomp - .k1_decomp_and_range_check_scalar(&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*h + l!" - ); - }); + .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 } => { + 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| { @@ -628,7 +646,7 @@ mod tests { offset, || Value::known(low), )?; - Ok(UncheckedDecomp:: { + Ok(UncheckedDecomp:: { value: None, high, low, @@ -645,8 +663,25 @@ mod tests { } } + fn test_ok(mode: TestMode) { + 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(mode: TestMode, msg: &str) { + 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 combined_scalar_decomp_and_range_check() { + 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(); @@ -669,23 +704,14 @@ mod tests { .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 - ); + for (_msg, scalar) in scalars.iter().chain(random_scalars.iter()) { + let mode = TestMode::<_, 1>::CombinedDecompAndRangeCheck { scalar: *scalar }; + test_ok(mode); } } #[test] - fn in_range_decomp() { + fn k1_in_range_decomp() { let zero = pallas::Base::zero(); let one = pallas::Base::one(); let pairs = [ @@ -704,25 +730,17 @@ mod tests { // 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, - }, + for (_msg, high, low) in pairs.iter() { + let 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_ok(mode); } } #[test] - fn out_of_range_decomp() { + fn k1_out_of_range_decomp() { let zero = pallas::Base::zero(); let one = pallas::Base::one(); let two = one.double(); @@ -740,18 +758,11 @@ mod tests { ("((q-1)/2, 1)", q12(), one), ]; for (msg, high, low) in pairs.iter() { - let circuit = ScalarDecompCircuit { - mode: TestMode::OutOfRangeDecomp { - high: *high, - low: *low, - }, + let 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 - ); + test_err(mode, msg); } } } From 2e1074d0a79ce989ccd54b74529bf3886fb42802 Mon Sep 17 00:00:00 2001 From: Nathan Collins Date: Thu, 18 Jan 2024 14:12:40 +0800 Subject: [PATCH 4/7] Add random tests for Pallas base and scalar fields New tests: - modulus decomposition for K=1..=10 - scalar decomposition, in-range range checks, and out-of-range range checks, for K=1..=5 and random scalars --- .../src/utilities/high_low_decomp.rs | 140 ++++++++++++++++-- 1 file changed, 129 insertions(+), 11 deletions(-) diff --git a/halo2_gadgets/src/utilities/high_low_decomp.rs b/halo2_gadgets/src/utilities/high_low_decomp.rs index 47685f1ef..6fe3ebc9a 100644 --- a/halo2_gadgets/src/utilities/high_low_decomp.rs +++ b/halo2_gadgets/src/utilities/high_low_decomp.rs @@ -441,19 +441,26 @@ where } } -/// 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. +/// Tests for `K`-high-low decomposition. +/// +/// These tests are all for Pallas, but they should trivially work for +/// Vesta as well. However, they won't work for Pluto/Eris, without +/// changing the `U256` usage to 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::{configs, T_Q}, + ecc::chip::{configs, T_P, T_Q}, utilities::{ high_low_decomp::UncheckedDecomp, lookup_range_check::LookupRangeCheckConfig, pow2_range_check, @@ -466,7 +473,7 @@ mod tests { plonk::{Advice, Circuit, Column, ConstraintSystem}, }; use halo2curves::pasta::pallas; - use rand::rngs::OsRng; + use rand::{random, rngs::OsRng}; // Copied from // ecc:chip::mul::decompose_for_scalar_mul(). I don't @@ -680,6 +687,117 @@ mod tests { ); } + #[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(t: u128) { + 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); + } + + const ITERS: usize = 10; + + #[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() { + 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] + fn random_out_of_range_decomp() { + fn test_one() { + 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 = pallas::Base::from_u128(random()); + let high = h_max + delta; + let low = pallas::Base::ZERO; + let mode = TestMode::::OutOfRangeDecomp { high, low }; + test_err(mode, "random high overflow"); + + // Test values that randomly overflow the low part. + let high = pallas::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] fn k1_combined_decomp_and_range_check() { let zero = pallas::Scalar::zero(); From 7f08184d5c1cebd5b85f46f4709465a68351f98d Mon Sep 17 00:00:00 2001 From: Nathan Collins Date: Thu, 18 Jan 2024 14:59:15 +0800 Subject: [PATCH 5/7] Generalize tests to Pallas and Vesta from Pallas This doesn't really provide much more coverage, since these tests are really about the scalar and base fields, and Pallas and Vesta are a cycle of curves (same set of fields). But this should set us up to easily add tests for Pluto/Eris once PrimeFieldBits (and perhaps other missing constraints) is implemented for Pluto/Eris. This commit includes generalizing the TestField helper trait to TestField. We'd also like to have an analogous TestCurve to define repetitive trait bounds on the curve C's associated fields, but unfortunately that doesn't work (it's a bug; don't believe the hype) :/ Details here: https://github.com/rust-lang/rust/issues/20671#issuecomment-1898036619 --- .../src/utilities/high_low_decomp.rs | 227 +++++++++++------- 1 file changed, 146 insertions(+), 81 deletions(-) diff --git a/halo2_gadgets/src/utilities/high_low_decomp.rs b/halo2_gadgets/src/utilities/high_low_decomp.rs index 6fe3ebc9a..1935d27fa 100644 --- a/halo2_gadgets/src/utilities/high_low_decomp.rs +++ b/halo2_gadgets/src/utilities/high_low_decomp.rs @@ -443,10 +443,9 @@ where /// Tests for `K`-high-low decomposition. /// -/// These tests are all for Pallas, but they should trivially work for -/// Vesta as well. However, they won't work for Pluto/Eris, without -/// changing the `U256` usage to something large enough for -/// Pluto/Eris, e.g. `U512`. +/// 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, @@ -460,19 +459,22 @@ where #[cfg(test)] mod tests { use crate::{ - ecc::chip::{configs, T_P, T_Q}, + ecc::chip::{T_P, T_Q}, utilities::{ high_low_decomp::UncheckedDecomp, lookup_range_check::LookupRangeCheckConfig, pow2_range_check, }, }; - use ff::{Field, PrimeField, PrimeFieldBits}; + use ff::{Field, FromUniformBytes, PrimeField, PrimeFieldBits}; use halo2_proofs::{ circuit::{Layouter, SimpleFloorPlanner, Value}, dev::MockProver, plonk::{Advice, Circuit, Column, ConstraintSystem}, }; - use halo2curves::pasta::pallas; + use halo2curves::{ + pasta::{pallas, vesta}, + CurveAffine, + }; use rand::{random, rngs::OsRng}; // Copied from @@ -518,7 +520,7 @@ mod tests { /// Test modes for the scalar decomposition gadget. #[derive(Copy, Clone)] - enum TestMode { + enum TestMode { /// Decompose the provided scalar, range check the result, and /// check that the decomposition is correct. CombinedDecompAndRangeCheck { @@ -526,13 +528,13 @@ mod tests { }, /// Check that the provided decomposition is canonical. InRangeDecomp { - high: pallas::Base, - low: pallas::Base, + high: C::Base, + low: C::Base, }, /// Check that the provided decomposition is non-canonical. OutOfRangeDecomp { - high: pallas::Base, - low: pallas::Base, + high: C::Base, + low: C::Base, }, NoTest, } @@ -540,14 +542,17 @@ mod tests { /// Computes a single scalar decomposition. /// Useful for finding the characteristics of the scalar decomposition gadget #[derive(Clone, Copy)] - struct ScalarDecompCircuit { - mode: TestMode, + struct ScalarDecompCircuit { + mode: TestMode, } #[derive(Debug, Clone)] - struct ScalarDecompConfig { - scalar_decomp: configs::ScalarDecompConfig, - lookup: LookupRangeCheckConfig, + struct ScalarDecompConfig + where + C::Base: PrimeFieldBits, + { + scalar_decomp: super::Config, + lookup: LookupRangeCheckConfig, } /// Trait-bound alias for all the constraints we want on our @@ -555,19 +560,28 @@ mod tests { /// /// Convenient trait aliases are only available in "nightly": /// https://github.com/rust-lang/rust/issues/41517 - trait TestField: - ScalarOrBase + PrimeFieldBits + 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 + PrimeField + impl TestField for S where + S: ScalarOrBase + PrimeFieldBits + FromUniformBytes<64> + PrimeField { } - impl Circuit for ScalarDecompCircuit { - type Config = ScalarDecompConfig; + 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; @@ -580,7 +594,7 @@ mod tests { } } - fn configure(meta: &mut ConstraintSystem) -> Self::Config { + fn configure(meta: &mut ConstraintSystem) -> Self::Config { let advices: [Column; 3] = [ meta.advice_column(), meta.advice_column(), @@ -595,8 +609,7 @@ mod tests { 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]); + let scalar_decomp = super::Config::configure(meta, pow2_config, advices[1], advices[2]); Self::Config { scalar_decomp, lookup: lookup_config, @@ -606,7 +619,7 @@ mod tests { fn synthesize( &self, config: Self::Config, - mut layouter: impl Layouter, + 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. @@ -615,7 +628,7 @@ mod tests { match self.mode { // Do a decomposition, range check the result, and // check that the decomposition is correct. - TestMode::<_, K>::CombinedDecompAndRangeCheck { scalar } => { + TestMode::<_, _, K>::CombinedDecompAndRangeCheck { scalar } => { let decomp = config .scalar_decomp .decompose_field_elem::<_, K>(&mut layouter, Value::known(scalar))?; @@ -635,8 +648,8 @@ mod tests { // 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 } => { + 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| { @@ -653,7 +666,7 @@ mod tests { offset, || Value::known(low), )?; - Ok(UncheckedDecomp:: { + Ok(UncheckedDecomp:: { value: None, high, low, @@ -670,16 +683,24 @@ mod tests { } } - fn test_ok(mode: TestMode) { + 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(); + let prover = MockProver::::run(11, &circuit, vec![]).unwrap(); // No way to add a custom message to `assert_satisfied()`. prover.assert_satisfied(); } - fn test_err(mode: TestMode, msg: &str) { + 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(); + let prover = MockProver::::run(11, &circuit, vec![]).unwrap(); assert!( prover.verify().is_err(), "Test was expected to fail but it succeeded! {}", @@ -706,9 +727,13 @@ mod tests { (high, low) } - fn test_one_k(t: u128) { + 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, 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!"); @@ -716,86 +741,124 @@ mod tests { } // 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); + 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 = 10; + 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() { + 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 }; + 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_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() { + 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::(); + let (h_max, l_max) = super::Config::::decompose_modulus::(); // Test the smallest overflowing value, i.e. the // modulus itself. - let mode = TestMode::::OutOfRangeDecomp { + let mode = TestMode::::OutOfRangeDecomp { high: h_max, low: l_max, }; test_err(mode, "modulus"); // Test values that randomly overflow the high part. - let delta = pallas::Base::from_u128(random()); + let delta = C::Base::from_u128(random()); let high = h_max + delta; - let low = pallas::Base::ZERO; - let mode = TestMode::::OutOfRangeDecomp { high, low }; + 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 = pallas::Base::ZERO; + let high = C::Base::ZERO; let low = l_max + delta; - let mode = TestMode::::OutOfRangeDecomp { high, low }; + 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_one::(); + test_one::(); + test_one::(); + test_one::(); + test_one::(); + test_one::(); + test_one::(); + test_one::(); + test_one::(); + test_one::(); } #[test] @@ -823,7 +886,9 @@ mod tests { .try_into() .unwrap(); for (_msg, scalar) in scalars.iter().chain(random_scalars.iter()) { - let mode = TestMode::<_, 1>::CombinedDecompAndRangeCheck { scalar: *scalar }; + let mode = TestMode::::CombinedDecompAndRangeCheck { + scalar: *scalar, + }; test_ok(mode); } } @@ -849,7 +914,7 @@ mod tests { ("((q-1)/2, 0)", q12(), zero), ]; for (_msg, high, low) in pairs.iter() { - let mode = TestMode::::OutOfRangeDecomp { + let mode = TestMode::::OutOfRangeDecomp { high: *high, low: *low, }; @@ -876,7 +941,7 @@ mod tests { ("((q-1)/2, 1)", q12(), one), ]; for (msg, high, low) in pairs.iter() { - let mode = TestMode::::OutOfRangeDecomp { + let mode = TestMode::::OutOfRangeDecomp { high: *high, low: *low, }; From 75b4f1acdb0cb5f3342f3a49e5991a1162e08a68 Mon Sep 17 00:00:00 2001 From: Nathan Collins Date: Thu, 18 Jan 2024 18:54:48 +0800 Subject: [PATCH 6/7] [book] Document the K-high-low decomp gadget --- book/src/design/gadgets/decomposition.md | 153 ++++++++++++++---- book/src/design/gadgets/ecc.md | 3 + .../design/gadgets/ecc/var-base-scalar-mul.md | 66 +------- .../src/utilities/high_low_decomp.rs | 6 +- 4 files changed, 129 insertions(+), 99 deletions(-) diff --git a/book/src/design/gadgets/decomposition.md b/book/src/design/gadgets/decomposition.md index c8f3f00fa..917c4f8be 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/src/utilities/high_low_decomp.rs b/halo2_gadgets/src/utilities/high_low_decomp.rs index 1935d27fa..09a72c37c 100644 --- a/halo2_gadgets/src/utilities/high_low_decomp.rs +++ b/halo2_gadgets/src/utilities/high_low_decomp.rs @@ -36,10 +36,8 @@ //! //! Decomposition is provided by [`Config::decompose_field_elem`]. //! -//! TODO(ntc2): update this doc reference after updating book: -//! -//! 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) +//! 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, From 60a913729a627ee78bf1477df5b0967f12bd6639 Mon Sep 17 00:00:00 2001 From: Nathan Collins Date: Wed, 7 Feb 2024 10:06:00 +0800 Subject: [PATCH 7/7] Address reviews MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - fix typo - replace `/=` with `≠` in comments --- book/src/design/gadgets/decomposition.md | 2 +- halo2_gadgets/src/utilities/high_low_decomp.rs | 6 +++--- halo2_gadgets/src/utilities/pow2_range_check.rs | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/book/src/design/gadgets/decomposition.md b/book/src/design/gadgets/decomposition.md index 917c4f8be..08a5d6116 100644 --- a/book/src/design/gadgets/decomposition.md +++ b/book/src/design/gadgets/decomposition.md @@ -105,7 +105,7 @@ 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. +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. diff --git a/halo2_gadgets/src/utilities/high_low_decomp.rs b/halo2_gadgets/src/utilities/high_low_decomp.rs index 09a72c37c..5990a47c2 100644 --- a/halo2_gadgets/src/utilities/high_low_decomp.rs +++ b/halo2_gadgets/src/utilities/high_low_decomp.rs @@ -172,7 +172,7 @@ where // 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 + // Constrain `h ≠ h_max` for use in constraining // `(h = h_max) => (l = 0)`. // // This one is a little subtle: constraints are @@ -208,7 +208,7 @@ where // 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 + // 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 @@ -230,7 +230,7 @@ where // - 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 \/ l = 0 // - h <= h_max // - already checked in the assignment function using strict range check Constraints::with_selector( 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)",