diff --git a/Cargo.toml b/Cargo.toml index 8c3e796e..2411e161 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -21,6 +21,7 @@ rustdoc-args = [ "--html-in-header", "katex-header.html" ] [dependencies] aes = "0.6" arrayvec = "0.7.0" +bigint = "4" bitvec = "0.22" blake2b_simd = "0.5" ff = "0.10" diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs index c160b1c8..2cf189dc 100644 --- a/src/circuit/gadget/ecc.rs +++ b/src/circuit/gadget/ecc.rs @@ -427,6 +427,7 @@ mod tests { meta.advice_column(), ]; + let lookup_table = meta.fixed_column(); let perm = meta.permutation( &advices .iter() @@ -434,7 +435,7 @@ mod tests { .collect::>(), ); - EccChip::configure(meta, advices, perm) + EccChip::configure(meta, advices, lookup_table, perm) } fn synthesize( @@ -443,7 +444,11 @@ mod tests { config: Self::Config, ) -> Result<(), Error> { let mut layouter = SingleChipLayouter::new(cs)?; - let chip = EccChip::construct(config); + let chip = EccChip::construct(config.clone()); + + // Load 10-bit lookup table. In the Action circuit, this will be + // provided by the Sinsemilla chip. + config.lookup_config.load(&mut layouter)?; // Generate a random point P let p_val = pallas::Point::random(rand::rngs::OsRng).to_affine(); // P diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs index c3e29cfd..26acdc6a 100644 --- a/src/circuit/gadget/ecc/chip.rs +++ b/src/circuit/gadget/ecc/chip.rs @@ -1,6 +1,11 @@ use super::EccInstructions; -use crate::circuit::gadget::utilities::{copy, CellValue, Var}; -use crate::constants::{self, OrchardFixedBasesFull, ValueCommitV}; +use crate::{ + circuit::gadget::utilities::{ + copy, lookup_range_check::LookupRangeCheckConfig, CellValue, Var, + }, + constants::{self, OrchardFixedBasesFull, ValueCommitV}, + primitives::sinsemilla, +}; use arrayvec::ArrayVec; use group::prime::PrimeCurveAffine; @@ -78,8 +83,10 @@ pub struct EccConfig { /// Incomplete addition pub q_add_incomplete: Selector, + /// Complete addition pub q_add: Selector, + /// Variable-base scalar multiplication (hi half) pub q_mul_hi: Selector, /// Variable-base scalar multiplication (lo half) @@ -89,19 +96,27 @@ pub struct EccConfig { /// Selector used in scalar decomposition for variable-base scalar mul pub q_init_z: Selector, /// Variable-base scalar multiplication (final scalar) - pub q_mul_complete: Selector, + pub q_mul_z: Selector, + /// Variable-base scalar multiplication (overflow check) + pub q_mul_overflow: Selector, + /// Fixed-base full-width scalar multiplication pub q_mul_fixed: Selector, + /// Fixed-base signed short scalar multiplication pub q_mul_fixed_short: Selector, + /// Witness point pub q_point: Selector, /// Witness full-width scalar for fixed-base scalar mul pub q_scalar_fixed: Selector, /// Witness signed short scalar for full-width fixed-base scalar mul pub q_scalar_fixed_short: Selector, + /// Permutation pub perm: Permutation, + /// 10-bit lookup + pub lookup_config: LookupRangeCheckConfig, } /// A chip implementing EccInstructions @@ -132,8 +147,12 @@ impl EccChip { pub fn configure( meta: &mut ConstraintSystem, advices: [Column; 10], + lookup_table: Column, perm: Permutation, ) -> >::Config { + let lookup_config = + LookupRangeCheckConfig::configure(meta, advices[9], lookup_table, perm.clone()); + let config = EccConfig { advices, lagrange_coeffs: [ @@ -153,13 +172,15 @@ impl EccChip { q_mul_lo: meta.selector(), q_mul_decompose_var: meta.selector(), q_init_z: meta.selector(), - q_mul_complete: meta.selector(), + q_mul_z: meta.selector(), + q_mul_overflow: meta.selector(), q_mul_fixed: meta.selector(), q_mul_fixed_short: meta.selector(), q_point: meta.selector(), q_scalar_fixed: meta.selector(), q_scalar_fixed_short: meta.selector(), perm, + lookup_config, }; // Create witness point gate @@ -193,13 +214,13 @@ impl EccChip { config.create_gate(meta); } - // Create witness scalar_fixed gate that only apploes to short scalars + // Create witness scalar_fixed gate that only applies to short scalars { let config: witness_scalar_fixed::short::Config = (&config).into(); config.create_gate(meta); } - // Create fixed-base scalar mul gate that os used in both full-width + // Create fixed-base scalar mul gate that is used in both full-width // and short multiplication. { let mul_fixed_config: mul_fixed::Config<{ constants::NUM_WINDOWS }> = (&config).into(); @@ -217,6 +238,17 @@ impl EccChip { } } +/// A base-field element used as the scalar in variable-base scalar multiplication. +#[derive(Copy, Clone, Debug)] +pub struct EccScalarVar(CellValue); +impl std::ops::Deref for EccScalarVar { + type Target = CellValue; + + fn deref(&self) -> &CellValue { + &self.0 + } +} + /// A full-width scalar used for fixed-base scalar multiplication. /// This is decomposed in chunks of `window_width` bits in little-endian order. /// For example, if `window_width` = 3, we will have [k_0, k_1, ..., k_n] @@ -243,7 +275,7 @@ pub struct EccScalarFixedShort { impl EccInstructions for EccChip { type ScalarFixed = EccScalarFixed; type ScalarFixedShort = EccScalarFixedShort; - type ScalarVar = CellValue; + type ScalarVar = EccScalarVar; type Point = EccPoint; type X = CellValue; type FixedPoints = OrchardFixedBasesFull; @@ -277,12 +309,12 @@ impl EccInstructions for EccChip { || "Witness scalar for variable-base mul", |mut region| { let cell = region.assign_advice( - || "Witness scalar var", + || "witness scalar var", config.advices[0], 0, || value.ok_or(Error::SynthesisError), )?; - Ok(CellValue::new(cell, value)) + Ok(EccScalarVar(CellValue::new(cell, value))) }, ) } @@ -360,9 +392,10 @@ impl EccInstructions for EccChip { base: &Self::Point, ) -> Result { let config: mul::Config = self.config().into(); - layouter.assign_region( - || "variable-base scalar mul", - |mut region| config.assign_region(scalar, base, 0, &mut region), + config.assign( + layouter.namespace(|| "variable-base scalar mul"), + *scalar, + base, ) } diff --git a/src/circuit/gadget/ecc/chip/mul.rs b/src/circuit/gadget/ecc/chip/mul.rs index 53cfffa1..42a87569 100644 --- a/src/circuit/gadget/ecc/chip/mul.rs +++ b/src/circuit/gadget/ecc/chip/mul.rs @@ -1,12 +1,13 @@ -use super::{add, copy, CellValue, EccConfig, EccPoint, Var}; +use super::{add, CellValue, EccConfig, EccPoint, EccScalarVar, Var}; use crate::constants::{NUM_COMPLETE_BITS, T_Q}; use std::ops::{Deref, Range}; -use ff::{PrimeField, PrimeFieldBits}; +use bigint::U256; +use ff::PrimeField; use halo2::{ arithmetic::FieldExt, - circuit::Region, - plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector}, + circuit::{Layouter, Region}, + plonk::{ConstraintSystem, Error, Permutation, Selector}, poly::Rotation, }; @@ -14,6 +15,7 @@ use pasta_curves::pallas; mod complete; mod incomplete; +mod overflow; // Bits used in incomplete addition. k_{254} to k_{4} inclusive const INCOMPLETE_LEN: usize = pallas::Scalar::NUM_BITS as usize - 1 - NUM_COMPLETE_BITS; @@ -32,38 +34,35 @@ const INCOMPLETE_LO_RANGE: Range = (INCOMPLETE_LEN / 2)..INCOMPLETE_LEN; const COMPLETE_RANGE: Range = INCOMPLETE_LEN..(INCOMPLETE_LEN + NUM_COMPLETE_BITS); pub struct Config { - // Selector used to constrain the cells used in complete addition. - q_mul_complete: Selector, - // Selector used to check recovery of the original scalar after decomposition. - q_mul_decompose_var: Selector, // Selector used to constrain the initialization of the running sum to be zero. q_init_z: Selector, - // Advice column used to decompose scalar in complete addition. - z_complete: Column, - // Advice column where the scalar is copied for use in the final recovery check. - scalar: Column, + // Selector used to check z_0 = 2*z_1 + k_0 + q_mul_z: Selector, // Permutation perm: Permutation, // Configuration used in complete addition add_config: add::Config, // Configuration used for `hi` bits of the scalar - hi_config: incomplete::Config, + hi_config: incomplete::HiConfig, // Configuration used for `lo` bits of the scalar - lo_config: incomplete::Config, + lo_config: incomplete::LoConfig, + // Configuration used for complete addition part of double-and-add algorithm + complete_config: complete::Config, + // Configuration used to check for overflow + overflow_config: overflow::Config, } impl From<&EccConfig> for Config { fn from(ecc_config: &EccConfig) -> Self { let config = Self { - q_mul_complete: ecc_config.q_mul_complete, - q_mul_decompose_var: ecc_config.q_mul_decompose_var, q_init_z: ecc_config.q_init_z, - z_complete: ecc_config.advices[9], - scalar: ecc_config.advices[1], + q_mul_z: ecc_config.q_mul_z, perm: ecc_config.perm.clone(), add_config: ecc_config.into(), - hi_config: incomplete::Config::hi_config(ecc_config), - lo_config: incomplete::Config::lo_config(ecc_config), + hi_config: ecc_config.into(), + lo_config: ecc_config.into(), + complete_config: ecc_config.into(), + overflow_config: ecc_config.into(), }; assert_eq!( @@ -76,10 +75,6 @@ impl From<&EccConfig> for Config { ); let add_config_advices = config.add_config.advice_columns(); - assert!( - !add_config_advices.contains(&config.z_complete), - "z_complete cannot overlap with complete addition columns." - ); assert!( !add_config_advices.contains(&config.hi_config.z), "hi_config z cannot overlap with complete addition columns." @@ -91,192 +86,183 @@ impl From<&EccConfig> for Config { impl Config { pub(super) fn create_gate(&self, meta: &mut ConstraintSystem) { - self.hi_config.create_gate(meta); - self.lo_config.create_gate(meta); - - let complete_config: complete::Config = self.into(); - complete_config.create_gate(meta); - - self.create_init_scalar_gate(meta); - self.create_final_scalar_gate(meta); - } - - /// Gate used to check that the running sum for scalar decomposition is initialized to zero. - fn create_init_scalar_gate(&self, meta: &mut ConstraintSystem) { + // Gate used to check that the running sum for scalar decomposition is initialized to zero. meta.create_gate("Initialize running sum for variable-base mul", |meta| { let q_init_z = meta.query_selector(self.q_init_z); let z = meta.query_advice(self.hi_config.z, Rotation::cur()); vec![q_init_z * z] }); + + self.hi_config.create_gate(meta); + self.lo_config.create_gate(meta); + self.complete_config.create_gate(meta); + self.overflow_config.create_gate(meta); } - /// Gate used to check final scalar is recovered. - fn create_final_scalar_gate(&self, meta: &mut ConstraintSystem) { - meta.create_gate("Decompose scalar for variable-base mul", |meta| { - let q_mul_decompose_var = meta.query_selector(self.q_mul_decompose_var); - let scalar = meta.query_advice(self.scalar, Rotation::cur()); - let z_cur = meta.query_advice(self.z_complete, Rotation::cur()); - - // The scalar field `F_q = 2^254 + t_q`. - // -((2^127)^2) = -(2^254) = t_q (mod q) - let t_q = -(pallas::Scalar::from_u128(1u128 << 127).square()); - let t_q = pallas::Base::from_bytes(&t_q.to_bytes()).unwrap(); - - // Check that `k = scalar + t_q` - vec![q_mul_decompose_var * (scalar + Expression::Constant(t_q) - z_cur)] - }); - } - - pub(super) fn assign_region( + pub(super) fn assign( &self, - scalar: &CellValue, + mut layouter: impl Layouter, + alpha: EccScalarVar, base: &EccPoint, - offset: usize, - region: &mut Region<'_, pallas::Base>, ) -> Result { - // Decompose the scalar bitwise (big-endian bit order). - let bits = decompose_for_scalar_mul(scalar.value()); - let bits_incomplete_hi = &bits[INCOMPLETE_HI_RANGE]; - let bits_incomplete_lo = &bits[INCOMPLETE_LO_RANGE]; - let lsb = bits[pallas::Scalar::NUM_BITS as usize - 1]; + let (result, zs): (EccPoint, Vec>) = layouter.assign_region( + || "variable-base scalar mul", + |mut region| { + let offset = 0; + // Decompose `k = alpha + t_q` bitwise (big-endian bit order). + let bits = decompose_for_scalar_mul(alpha.value()); - // Initialize the accumulator `acc = [2]base` - let acc = self - .add_config - .assign_region(&base, &base, offset, region)?; + // Define ranges for each part of the algorithm. + let bits_incomplete_hi = &bits[INCOMPLETE_HI_RANGE]; + let bits_incomplete_lo = &bits[INCOMPLETE_LO_RANGE]; + let lsb = bits[pallas::Scalar::NUM_BITS as usize - 1]; - // Increase the offset by 1 after complete addition. - let offset = offset + 1; + // Initialize the accumulator `acc = [2]base` + let acc = self + .add_config + .assign_region(&base, &base, offset, &mut region)?; - // Initialize the running sum for scalar decomposition to zero - let z_init = { - // Constrain the initialization of `z` to equal zero. - self.q_init_z.enable(region, offset)?; + // Increase the offset by 1 after complete addition. + let offset = offset + 1; - let z_val = pallas::Base::zero(); - let z_cell = - region.assign_advice(|| "initial z", self.hi_config.z, offset, || Ok(z_val))?; + // Initialize the running sum for scalar decomposition to zero + let z_init = { + // Constrain the initialization of `z` to equal zero. + self.q_init_z.enable(&mut region, offset)?; - Z(CellValue::new(z_cell, Some(z_val))) - }; + let z_val = pallas::Base::zero(); + let z_cell = region.assign_advice( + || "initial z", + self.hi_config.z, + offset, + || Ok(z_val), + )?; - // Increase the offset by 1 after initializing `z`. - let offset = offset + 1; + Z(CellValue::new(z_cell, Some(z_val))) + }; - // Double-and-add (incomplete addition) for the `hi` half of the scalar decomposition - let (x_a, y_a, zs_incomplete_hi) = self.hi_config.double_and_add( - region, - offset, - &base, - bits_incomplete_hi, - (X(acc.x), Y(acc.y.value()), z_init), + // Increase the offset by 1 after initializing `z`. + let offset = offset + 1; + + // Double-and-add (incomplete addition) for the `hi` half of the scalar decomposition + let (x_a, y_a, zs_incomplete_hi) = self.hi_config.double_and_add( + &mut region, + offset, + &base, + bits_incomplete_hi, + (X(acc.x), Y(acc.y.value()), z_init), + )?; + + // Double-and-add (incomplete addition) for the `lo` half of the scalar decomposition + let z = &zs_incomplete_hi[zs_incomplete_hi.len() - 1]; + let (x_a, y_a, zs_incomplete_lo) = self.lo_config.double_and_add( + &mut region, + offset, + &base, + bits_incomplete_lo, + (x_a, y_a, *z), + )?; + + // Move from incomplete addition to complete addition. + // Inside incomplete::double_and_add, the offset was increase once after initialization + // of the running sum. + // Then, the final assignment of double-and-add was made on row + offset + 1. + // Outside of incomplete addition, we must account for these offset increases by adding + // 2 to the incomplete addition length. + let offset = offset + INCOMPLETE_LO_RANGE.len() + 2; + + // Complete addition + let (acc, zs_complete) = { + let z = &zs_incomplete_lo[zs_incomplete_lo.len() - 1]; + // Bits used in complete addition. k_{3} to k_{1} inclusive + // The LSB k_{0} is handled separately. + let bits_complete = &bits[COMPLETE_RANGE]; + self.complete_config.assign_region( + &mut region, + offset, + bits_complete, + base, + x_a, + y_a, + *z, + )? + }; + + // Each iteration of the complete addition uses two rows. + let offset = offset + COMPLETE_RANGE.len() * 2; + + // Process the least significant bit + let z_1 = zs_complete.last().unwrap(); + let (result, z_0) = self.process_lsb(&mut region, offset, base, acc, *z_1, lsb)?; + + #[cfg(test)] + // Check that the correct multiple is obtained. + { + use group::Curve; + + let base = base.point(); + let alpha = alpha + .value() + .map(|alpha| pallas::Scalar::from_bytes(&alpha.to_bytes()).unwrap()); + let real_mul = base.zip(alpha).map(|(base, alpha)| base * alpha); + let result = result.point(); + + if let (Some(real_mul), Some(result)) = (real_mul, result) { + assert_eq!(real_mul.to_affine(), result); + } + } + + let zs = { + let mut zs = vec![z_init]; + zs.extend_from_slice(&zs_incomplete_hi); + zs.extend_from_slice(&zs_incomplete_lo); + zs.extend_from_slice(&zs_complete); + zs.extend_from_slice(&[z_0]); + assert_eq!(zs.len(), pallas::Scalar::NUM_BITS as usize + 1); + + // This reverses zs to give us [z_0, z_1, ..., z_{254}, z_{255}]. + zs.reverse(); + zs + }; + + Ok((result, zs)) + }, )?; - // Double-and-add (incomplete addition) for the `lo` half of the scalar decomposition - let z = &zs_incomplete_hi[zs_incomplete_hi.len() - 1]; - let (x_a, y_a, zs_incomplete_lo) = self.lo_config.double_and_add( - region, - offset, - &base, - bits_incomplete_lo, - (x_a, y_a, *z), - )?; - - // Move from incomplete addition to complete addition. - // Inside incomplete::double_and_add, the offset was increase once after initialization - // of the running sum. - // Then, the final assignment of double-and-add was made on row + offset + 1. - // Outside of incomplete addition, we must account for these offset increases by adding - // 2 to the incomplete addition length. - let offset = offset + INCOMPLETE_LO_RANGE.len() + 2; - - // Complete addition - let (acc, zs_complete) = { - let z = &zs_incomplete_lo[zs_incomplete_lo.len() - 1]; - let complete_config: complete::Config = self.into(); - // Bits used in complete addition. k_{3} to k_{1} inclusive - // The LSB k_{0} is handled separately. - let bits_complete = &bits[COMPLETE_RANGE]; - complete_config.assign_region(region, offset, bits_complete, base, x_a, y_a, *z)? - }; - - // Each iteration of the complete addition uses two rows. - let offset = offset + COMPLETE_RANGE.len() * 2; - - // Process the least significant bit - let z = &zs_complete[zs_complete.len() - 1]; - let (result, z_final) = self.process_lsb(region, offset, scalar, base, acc, lsb, *z)?; - - #[cfg(test)] - // Check that the correct multiple is obtained. - { - use group::Curve; - - let base = base.point(); - let scalar = scalar - .value() - .map(|scalar| pallas::Scalar::from_bytes(&scalar.to_bytes()).unwrap()); - let real_mul = base.zip(scalar).map(|(base, scalar)| base * scalar); - let result = result.point(); - - if let (Some(real_mul), Some(result)) = (real_mul, result) { - assert_eq!(real_mul.to_affine(), result); - } - } - - let mut zs = vec![z_init]; - zs.extend_from_slice(&zs_incomplete_hi); - zs.extend_from_slice(&zs_incomplete_lo); - zs.extend_from_slice(&zs_complete); - zs.extend_from_slice(&[z_final]); - - // This reverses zs to give us [z_0, z_1, ..., z_{254}, z_{255}]. - zs.reverse(); + self.overflow_config + .overflow_check(layouter.namespace(|| "overflow check"), alpha, &zs)?; Ok(result) } - #[allow(clippy::too_many_arguments)] fn process_lsb( &self, region: &mut Region<'_, pallas::Base>, offset: usize, - _scalar: &CellValue, base: &EccPoint, acc: EccPoint, + z_1: Z, lsb: Option, - z: Z, ) -> Result<(EccPoint, Z), Error> { - // Copy in the penultimate `z_1` value. - copy( - region, - || "penultimate z_1 running sum", - self.z_complete, - offset, - &z.0, - &self.perm, - )?; - - // Increase offset after copying in `z_1`. - let offset = offset + 1; - - // Assign the final `z_0` value. - let z = { - let z_val = z.0.value().zip(lsb).map(|(z_val, lsb)| { - pallas::Base::from_u64(2) * z_val + pallas::Base::from_u64(lsb as u64) + // Assign z_0 = 2⋅z_1 + k_0 + let z_0 = { + let z_0_val = z_1.value().zip(lsb).map(|(z_1, lsb)| { + let lsb = pallas::Base::from_u64(lsb as u64); + z_1 * pallas::Base::from_u64(2) + lsb }); - let z_cell = region.assign_advice( - || "final z_0", - self.z_complete, + let z_0_cell = region.assign_advice( + || "z_0", + self.complete_config.z_complete, offset, - || z_val.ok_or(Error::SynthesisError), + || z_0_val.ok_or(Error::SynthesisError), )?; - Z(CellValue::new(z_cell, z_val)) - }; - // Enforce that the final bit decomposition from `z_1` to `z_0` was done correctly. - self.q_mul_complete.enable(region, offset)?; + // Check that z_0 was properly derived from z_1. + self.q_mul_z.enable(region, offset)?; + + Z(CellValue::new(z_0_cell, z_0_val)) + }; // If `lsb` is 0, return `Acc + (-P)`. If `lsb` is 1, simply return `Acc + 0`. let x_p = if let Some(lsb) = lsb { @@ -301,14 +287,14 @@ impl Config { let x_p_cell = region.assign_advice( || "x_p", self.add_config.x_p, - offset + 1, + offset, || x_p.ok_or(Error::SynthesisError), )?; let y_p_cell = region.assign_advice( || "y_p", self.add_config.y_p, - offset + 1, + offset, || y_p.ok_or(Error::SynthesisError), )?; @@ -318,11 +304,9 @@ impl Config { }; // Return the result of the final complete addition as `[scalar]B` - let result = self - .add_config - .assign_region(&p, &acc, offset + 1, region)?; + let result = self.add_config.assign_region(&p, &acc, offset, region)?; - Ok((result, z)) + Ok((result, z_0)) } } @@ -360,29 +344,36 @@ impl Deref for Z { } fn decompose_for_scalar_mul(scalar: Option) -> Vec> { - let bits = scalar.map(|scalar| { + let bitstring = scalar.map(|scalar| { // We use `k = scalar + t_q` in the double-and-add algorithm, where // the scalar field `F_q = 2^254 + t_q`. - let k = { - let scalar = pallas::Scalar::from_bytes(&scalar.to_bytes()).unwrap(); - scalar + pallas::Scalar::from_u128(T_Q) + // Note that the addition `scalar + t_q` is not reduced. + // + let scalar = U256::from_little_endian(&scalar.to_bytes()); + let t_q = U256::from_little_endian(&T_Q.to_le_bytes()); + let k = scalar + t_q; + + // Big-endian bit representation of `k`. + let bitstring: Vec = { + let mut le_bytes = [0u8; 32]; + k.to_little_endian(&mut le_bytes); + le_bytes.iter().fold(Vec::new(), |mut bitstring, byte| { + let bits = (0..8) + .map(|shift| (byte >> shift) % 2 == 1) + .collect::>(); + bitstring.extend_from_slice(&bits); + bitstring + }) }; - // `k` is decomposed bitwise (big-endian) into `[k_n, ..., lsb]`, where - // each `k_i` is a bit and `scalar = k_n * 2^n + ... + k_1 * 2 + lsb`. - let mut bits: Vec = k - .to_le_bits() - .into_iter() - .take(pallas::Scalar::NUM_BITS as usize) - .collect(); - bits.reverse(); - assert_eq!(bits.len(), pallas::Scalar::NUM_BITS as usize); - - bits + // Take the first 255 bits. + let mut bitstring = bitstring[0..pallas::Scalar::NUM_BITS as usize].to_vec(); + bitstring.reverse(); + bitstring }); - if let Some(bits) = bits { - bits.into_iter().map(Some).collect() + if let Some(bitstring) = bitstring { + bitstring.into_iter().map(Some).collect() } else { vec![None; pallas::Scalar::NUM_BITS as usize] } @@ -401,14 +392,13 @@ pub mod tests { zero: &Point, p: &Point, ) -> Result<(), Error> { + // [a]B let scalar_val = pallas::Base::rand(); let scalar = ScalarVar::new( chip.clone(), layouter.namespace(|| "ScalarVar"), Some(scalar_val), )?; - - // [a]B p.mul(layouter.namespace(|| "mul"), &scalar)?; // [a]𝒪 should return an error since variable-base scalar multiplication @@ -419,6 +409,15 @@ pub mod tests { // [0]B should return (0,0) since variable-base scalar multiplication // uses complete addition for the final bits of the scalar. let scalar_val = pallas::Base::zero(); + let scalar = ScalarVar::new( + chip.clone(), + layouter.namespace(|| "ScalarVar"), + Some(scalar_val), + )?; + p.mul(layouter.namespace(|| "mul"), &scalar)?; + + // [-1]B (the largest possible base field element) + let scalar_val = -pallas::Base::one(); let scalar = ScalarVar::new(chip, layouter.namespace(|| "ScalarVar"), Some(scalar_val))?; p.mul(layouter.namespace(|| "mul"), &scalar)?; diff --git a/src/circuit/gadget/ecc/chip/mul/complete.rs b/src/circuit/gadget/ecc/chip/mul/complete.rs index 67b08996..8bd75163 100644 --- a/src/circuit/gadget/ecc/chip/mul/complete.rs +++ b/src/circuit/gadget/ecc/chip/mul/complete.rs @@ -1,4 +1,4 @@ -use super::super::{add, copy, CellValue, EccPoint, Var}; +use super::super::{add, copy, CellValue, EccConfig, EccPoint, Var}; use super::{COMPLETE_RANGE, X, Y, Z}; use halo2::{ @@ -11,23 +11,31 @@ use pasta_curves::{arithmetic::FieldExt, pallas}; pub struct Config { // Selector used to constrain the cells used in complete addition. - q_mul_complete: Selector, + q_mul_z: Selector, // Advice column used to decompose scalar in complete addition. - z_complete: Column, + pub z_complete: Column, // Permutation perm: Permutation, // Configuration used in complete addition add_config: add::Config, } -impl From<&super::Config> for Config { - fn from(config: &super::Config) -> Self { - Self { - q_mul_complete: config.q_mul_complete, - z_complete: config.z_complete, - perm: config.perm.clone(), - add_config: config.add_config.clone(), - } +impl From<&EccConfig> for Config { + fn from(ecc_config: &EccConfig) -> Self { + let config = Self { + q_mul_z: ecc_config.q_mul_z, + z_complete: ecc_config.advices[9], + perm: ecc_config.perm.clone(), + add_config: ecc_config.into(), + }; + + let add_config_advices = config.add_config.advice_columns(); + assert!( + !add_config_advices.contains(&config.z_complete), + "z_complete cannot overlap with complete addition columns." + ); + + config } } @@ -40,7 +48,7 @@ impl Config { meta.create_gate( "Decompose scalar for complete bits of variable-base mul", |meta| { - let q_mul_complete = meta.query_selector(self.q_mul_complete); + let q_mul_z = meta.query_selector(self.q_mul_z); let z_cur = meta.query_advice(self.z_complete, Rotation::cur()); let z_prev = meta.query_advice(self.z_complete, Rotation::prev()); @@ -49,7 +57,7 @@ impl Config { // (k_i) ⋅ (k_i - 1) = 0 let bool_check = k.clone() * (k + Expression::Constant(-pallas::Base::one())); - vec![q_mul_complete * bool_check] + vec![q_mul_z * bool_check] }, ); } @@ -76,9 +84,9 @@ impl Config { // Each iteration uses 2 rows (two complete additions) let row = 2 * row; // Check scalar decomposition for each iteration. Since the gate enabled by - // `q_mul_complete` queries the previous row, we enable the selector on + // `q_mul_z` queries the previous row, we enable the selector on // `row + offset + 1` (instead of `row + offset`). - self.q_mul_complete.enable(region, row + offset + 1)?; + self.q_mul_z.enable(region, row + offset + 1)?; } // Use x_a, y_a output from incomplete addition diff --git a/src/circuit/gadget/ecc/chip/mul/incomplete.rs b/src/circuit/gadget/ecc/chip/mul/incomplete.rs index 17bea752..feae9c3a 100644 --- a/src/circuit/gadget/ecc/chip/mul/incomplete.rs +++ b/src/circuit/gadget/ecc/chip/mul/incomplete.rs @@ -1,4 +1,4 @@ -use std::array; +use std::{array, ops::Deref}; use super::super::{copy, CellValue, EccConfig, EccPoint, Var}; use super::{INCOMPLETE_HI_RANGE, INCOMPLETE_LO_RANGE, X, Y, Z}; @@ -32,11 +32,12 @@ pub(super) struct Config { pub(super) perm: Permutation, } -impl Config { - // Columns used in processing the `hi` bits of the scalar. - // `x_p, y_p` are shared across the `hi` and `lo` halves. - pub(super) fn hi_config(ecc_config: &EccConfig) -> Self { - Self { +// Columns used in processing the `hi` bits of the scalar. +// `x_p, y_p` are shared across the `hi` and `lo` halves. +pub(super) struct HiConfig(Config); +impl From<&EccConfig> for HiConfig { + fn from(ecc_config: &EccConfig) -> Self { + let config = Config { num_bits: INCOMPLETE_HI_RANGE.len(), q_mul: ecc_config.q_mul_hi, x_p: ecc_config.advices[0], @@ -46,13 +47,24 @@ impl Config { lambda1: ecc_config.advices[4], lambda2: ecc_config.advices[5], perm: ecc_config.perm.clone(), - } + }; + Self(config) } +} +impl Deref for HiConfig { + type Target = Config; - // Columns used in processing the `lo` bits of the scalar. - // `x_p, y_p` are shared across the `hi` and `lo` halves. - pub(super) fn lo_config(ecc_config: &EccConfig) -> Self { - Self { + fn deref(&self) -> &Config { + &self.0 + } +} + +// Columns used in processing the `lo` bits of the scalar. +// `x_p, y_p` are shared across the `hi` and `lo` halves. +pub(super) struct LoConfig(Config); +impl From<&EccConfig> for LoConfig { + fn from(ecc_config: &EccConfig) -> Self { + let config = Config { num_bits: INCOMPLETE_LO_RANGE.len(), q_mul: ecc_config.q_mul_lo, x_p: ecc_config.advices[0], @@ -62,9 +74,19 @@ impl Config { lambda1: ecc_config.advices[8], lambda2: ecc_config.advices[2], perm: ecc_config.perm.clone(), - } + }; + Self(config) } +} +impl Deref for LoConfig { + type Target = Config; + fn deref(&self) -> &Config { + &self.0 + } +} + +impl Config { // Gate for incomplete addition part of variable-base scalar multiplication. pub(super) fn create_gate(&self, meta: &mut ConstraintSystem) { meta.create_gate("Incomplete addition for variable-base scalar mul", |meta| { diff --git a/src/circuit/gadget/ecc/chip/mul/overflow.rs b/src/circuit/gadget/ecc/chip/mul/overflow.rs new file mode 100644 index 00000000..923a0199 --- /dev/null +++ b/src/circuit/gadget/ecc/chip/mul/overflow.rs @@ -0,0 +1,244 @@ +use super::super::{copy, CellValue, EccConfig, EccScalarVar, Var}; +use super::Z; +use crate::{ + circuit::gadget::utilities::lookup_range_check::LookupRangeCheckConfig, constants::T_Q, + primitives::sinsemilla, +}; +use halo2::{ + circuit::Layouter, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector}, + poly::Rotation, +}; + +use ff::Field; +use pasta_curves::{arithmetic::FieldExt, pallas}; + +use std::iter; + +pub struct Config { + // Selector to check decomposition of lsb + q_mul_z: Selector, + // Selector to check z_0 = alpha + t_q (mod p) + q_mul_overflow: Selector, + // 10-bit lookup table + lookup_config: LookupRangeCheckConfig, + // Advice columns + advices: [Column; 3], + // Permutation + perm: Permutation, +} + +impl From<&EccConfig> for Config { + fn from(ecc_config: &EccConfig) -> Self { + Self { + q_mul_z: ecc_config.q_mul_z, + q_mul_overflow: ecc_config.q_mul_overflow, + lookup_config: ecc_config.lookup_config.clone(), + advices: [ + ecc_config.advices[0], + ecc_config.advices[1], + ecc_config.advices[2], + ], + perm: ecc_config.perm.clone(), + } + } +} + +impl Config { + pub(super) fn create_gate(&self, meta: &mut ConstraintSystem) { + meta.create_gate("overflow checks", |meta| { + let q_mul_overflow = meta.query_selector(self.q_mul_overflow); + + // Constant expressions + let one = Expression::Constant(pallas::Base::one()); + let two_pow_124 = Expression::Constant(pallas::Base::from_u128(1 << 124)); + let two_pow_130 = + two_pow_124.clone() * Expression::Constant(pallas::Base::from_u128(1 << 6)); + + let z_0 = meta.query_advice(self.advices[0], Rotation::prev()); + let z_130 = meta.query_advice(self.advices[0], Rotation::cur()); + let eta = meta.query_advice(self.advices[0], Rotation::next()); + + let k_254 = meta.query_advice(self.advices[1], Rotation::prev()); + let alpha = meta.query_advice(self.advices[1], Rotation::cur()); + + // s_minus_lo_130 = s - sum_{i = 0}^{129} 2^i ⋅ s_i + let s_minus_lo_130 = meta.query_advice(self.advices[1], Rotation::next()); + + let s = meta.query_advice(self.advices[2], Rotation::cur()); + let s_check = s - (alpha.clone() + k_254.clone() * two_pow_130); + + // q = 2^254 + t_q is the Pallas scalar field modulus. + // We cast t_q into the base field to check alpha + t_q (mod p). + let t_q = pallas::Base::from_u128(T_Q); + let t_q = Expression::Constant(t_q); + + // z_0 - alpha - t_q = 0 (mod p) + let recovery = z_0 - alpha - t_q; + + // k_254 * (z_130 - 2^124) = 0 + let lo_zero = k_254.clone() * (z_130.clone() - two_pow_124); + + // k_254 * s_minus_lo_130 = 0 + let s_minus_lo_130_check = k_254.clone() * s_minus_lo_130.clone(); + + // (1 - k_254) * (1 - z_130 * eta) * s_minus_lo_130 = 0 + let canonicity = (one.clone() - k_254) * (one - z_130 * eta) * s_minus_lo_130; + + iter::empty() + .chain(Some(s_check)) + .chain(Some(recovery)) + .chain(Some(lo_zero)) + .chain(Some(s_minus_lo_130_check)) + .chain(Some(canonicity)) + .map(|poly| q_mul_overflow.clone() * poly) + .collect::>() + }); + } + + pub(super) fn overflow_check( + &self, + mut layouter: impl Layouter, + alpha: EccScalarVar, + zs: &[Z], // [z_0, z_1, ..., z_{254}, z_{255}] + ) -> Result<(), Error> { + // s = alpha + k_254 ⋅ 2^130 is witnessed here, and then copied into + // the decomposition as well as the overflow check gate. + // In the overflow check gate, we check that s is properly derived + // from alpha and k_254. + let s = { + let k_254 = *zs[254]; + let s_val = alpha + .value() + .zip(k_254.value()) + .map(|(alpha, k_254)| alpha + k_254 * pallas::Base::from_u128(1 << 65).square()); + + layouter.assign_region( + || "s = alpha + k_254 ⋅ 2^130", + |mut region| { + let s_cell = region.assign_advice( + || "s = alpha + k_254 ⋅ 2^130", + self.advices[0], + 0, + || s_val.ok_or(Error::SynthesisError), + )?; + Ok(CellValue::new(s_cell, s_val)) + }, + )? + }; + + // Subtract the first 130 low bits of s = alpha + k_254 ⋅ 2^130 + // using thirteen 10-bit lookups, s_{0..=129} + let s_minus_lo_130 = + self.s_minus_lo_130(layouter.namespace(|| "decompose s_{0..=129}"), s)?; + + layouter.assign_region( + || "overflow check", + |mut region| { + let offset = 0; + + // Enable overflow check gate + self.q_mul_overflow.enable(&mut region, offset + 1)?; + + // Copy `z_0` + copy( + &mut region, + || "copy z_0", + self.advices[0], + offset, + &*zs[0], + &self.perm, + )?; + + // Copy `z_130` + copy( + &mut region, + || "copy z_130", + self.advices[0], + offset + 1, + &*zs[130], + &self.perm, + )?; + + // Witness η = inv0(z_130), where inv0(x) = 0 if x = 0, 1/x otherwise + { + let eta = zs[130].value().map(|z_130| { + if z_130 == pallas::Base::zero() { + pallas::Base::zero() + } else { + z_130.invert().unwrap() + } + }); + region.assign_advice( + || "η = inv0(z_130)", + self.advices[0], + offset + 2, + || eta.ok_or(Error::SynthesisError), + )?; + } + + // Copy `k_254` = z_254 + copy( + &mut region, + || "copy k_254", + self.advices[1], + offset, + &*zs[254], + &self.perm, + )?; + + // Copy original alpha + copy( + &mut region, + || "copy original alpha", + self.advices[1], + offset + 1, + &*alpha, + &self.perm, + )?; + + // Copy weighted sum of the decomposition of s = alpha + k_254 ⋅ 2^130. + copy( + &mut region, + || "copy s_minus_lo_130", + self.advices[1], + offset + 2, + &s_minus_lo_130, + &self.perm, + )?; + + // Copy witnessed s to check that it was properly derived from alpha and k_254. + copy( + &mut region, + || "copy s", + self.advices[2], + offset + 1, + &s, + &self.perm, + )?; + + Ok(()) + }, + )?; + + Ok(()) + } + + fn s_minus_lo_130( + &self, + mut layouter: impl Layouter, + s: CellValue, + ) -> Result, Error> { + // Number of k-bit words we can use in the lookup decomposition. + let num_words = 130 / sinsemilla::K; + assert!(num_words * sinsemilla::K == 130); + + // Decompose the low 130 bits of `s` using thirteen 10-bit lookups. + let zs = self.lookup_config.copy_check( + layouter.namespace(|| "Decompose low 130 bits of s"), + s, + num_words, + )?; + Ok(zs[zs.len() - 1]) + } +} diff --git a/src/spec.rs b/src/spec.rs index 44e19c48..66ba9780 100644 --- a/src/spec.rs +++ b/src/spec.rs @@ -240,6 +240,12 @@ pub(crate) fn extract_p_bottom(point: CtOption) -> CtOption(bits: &[bool; L]) -> F { + F::from_u64(lebs2ip::(bits)) +} + /// The u64 integer represented by an L-bit little-endian bitstring. /// /// # Panics