diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs index 2b9e0c6c..046ede72 100644 --- a/src/circuit/gadget/ecc/chip.rs +++ b/src/circuit/gadget/ecc/chip.rs @@ -12,7 +12,7 @@ use pasta_curves::{arithmetic::CurveAffine, pallas}; pub(super) mod add; pub(super) mod add_incomplete; -// pub(super) mod mul; +pub(super) mod mul; // pub(super) mod mul_fixed; pub(super) mod witness_point; // pub(super) mod witness_scalar_fixed; @@ -86,6 +86,8 @@ pub struct EccConfig { pub q_mul_lo: Selector, /// Selector used in scalar decomposition for variable-base scalar mul pub q_mul_decompose_var: Selector, + /// 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, /// Fixed-base full-width scalar multiplication @@ -150,6 +152,7 @@ impl EccChip { q_mul_hi: meta.selector(), q_mul_lo: meta.selector(), q_mul_decompose_var: meta.selector(), + q_init_z: meta.selector(), q_mul_complete: meta.selector(), q_mul_fixed: meta.selector(), q_mul_fixed_short: meta.selector(), @@ -177,6 +180,12 @@ impl EccChip { add_config.create_gate(meta); } + // Create variable-base scalar mul gates + { + let mul_config: mul::Config = (&config).into(); + mul_config.create_gate(meta); + } + config } } @@ -311,11 +320,15 @@ impl EccInstructions for EccChip { fn mul( &self, - _layouter: &mut impl Layouter, - _scalar: &Self::ScalarVar, - _base: &Self::Point, + layouter: &mut impl Layouter, + scalar: &Self::ScalarVar, + base: &Self::Point, ) -> Result { - todo!() + let config: mul::Config = self.config().into(); + layouter.assign_region( + || "variable-base scalar mul", + |mut region| config.assign_region(scalar, base, 0, &mut region), + ) } fn mul_fixed( diff --git a/src/circuit/gadget/ecc/chip/mul.rs b/src/circuit/gadget/ecc/chip/mul.rs new file mode 100644 index 00000000..53cfffa1 --- /dev/null +++ b/src/circuit/gadget/ecc/chip/mul.rs @@ -0,0 +1,427 @@ +use super::{add, copy, CellValue, EccConfig, EccPoint, Var}; +use crate::constants::{NUM_COMPLETE_BITS, T_Q}; +use std::ops::{Deref, Range}; + +use ff::{PrimeField, PrimeFieldBits}; +use halo2::{ + arithmetic::FieldExt, + circuit::Region, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector}, + poly::Rotation, +}; + +use pasta_curves::pallas; + +mod complete; +mod incomplete; + +// 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; +const INCOMPLETE_RANGE: Range = 0..INCOMPLETE_LEN; + +// Bits k_{254} to k_{4} inclusive are used in incomplete addition. +// The `hi` half is k_{254} to k_{130} inclusive (length 125 bits). +const INCOMPLETE_HI_RANGE: Range = 0..(INCOMPLETE_LEN / 2); + +// Bits k_{254} to k_{4} inclusive are used in incomplete addition. +// The `lo` half is k_{129} to k_{4} inclusive (length 126 bits). +const INCOMPLETE_LO_RANGE: Range = (INCOMPLETE_LEN / 2)..INCOMPLETE_LEN; + +// Bits k_{3} to k_{1} inclusive are used in complete addition. +// Bit k_{0} is handled separately. +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, + // Permutation + perm: Permutation, + // Configuration used in complete addition + add_config: add::Config, + // Configuration used for `hi` bits of the scalar + hi_config: incomplete::Config, + // Configuration used for `lo` bits of the scalar + lo_config: incomplete::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], + 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), + }; + + assert_eq!( + config.hi_config.x_p, config.lo_config.x_p, + "x_p is shared across hi and lo halves." + ); + assert_eq!( + config.hi_config.y_p, config.lo_config.y_p, + "y_p is shared across hi and lo halves." + ); + + 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." + ); + + 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) { + 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] + }); + } + + /// 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( + &self, + scalar: &CellValue, + 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]; + + // Initialize the accumulator `acc = [2]base` + let acc = self + .add_config + .assign_region(&base, &base, offset, region)?; + + // Increase the offset by 1 after complete addition. + let offset = offset + 1; + + // 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)?; + + let z_val = pallas::Base::zero(); + let z_cell = + region.assign_advice(|| "initial z", self.hi_config.z, offset, || Ok(z_val))?; + + Z(CellValue::new(z_cell, Some(z_val))) + }; + + // 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( + 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( + 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(); + + Ok(result) + } + + #[allow(clippy::too_many_arguments)] + fn process_lsb( + &self, + region: &mut Region<'_, pallas::Base>, + offset: usize, + _scalar: &CellValue, + base: &EccPoint, + acc: EccPoint, + 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) + }); + let z_cell = region.assign_advice( + || "final z_0", + self.z_complete, + offset, + || z_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)?; + + // If `lsb` is 0, return `Acc + (-P)`. If `lsb` is 1, simply return `Acc + 0`. + let x_p = if let Some(lsb) = lsb { + if !lsb { + base.x.value() + } else { + Some(pallas::Base::zero()) + } + } else { + None + }; + let y_p = if let Some(lsb) = lsb { + if !lsb { + base.y.value().map(|y_p| -y_p) + } else { + Some(pallas::Base::zero()) + } + } else { + None + }; + + let x_p_cell = region.assign_advice( + || "x_p", + self.add_config.x_p, + offset + 1, + || x_p.ok_or(Error::SynthesisError), + )?; + + let y_p_cell = region.assign_advice( + || "y_p", + self.add_config.y_p, + offset + 1, + || y_p.ok_or(Error::SynthesisError), + )?; + + let p = EccPoint { + x: CellValue::::new(x_p_cell, x_p), + y: CellValue::::new(y_p_cell, y_p), + }; + + // Return the result of the final complete addition as `[scalar]B` + let result = self + .add_config + .assign_region(&p, &acc, offset + 1, region)?; + + Ok((result, z)) + } +} + +#[derive(Clone, Debug)] +// `x`-coordinate of the accumulator. +struct X(CellValue); +impl Deref for X { + type Target = CellValue; + + fn deref(&self) -> &Self::Target { + &self.0 + } +} + +#[derive(Copy, Clone, Debug)] +// `y`-coordinate of the accumulator. +struct Y(Option); +impl Deref for Y { + type Target = Option; + + fn deref(&self) -> &Self::Target { + &self.0 + } +} + +#[derive(Copy, Clone, Debug)] +// Cumulative sum `z` used to decompose the scalar. +struct Z(CellValue); +impl Deref for Z { + type Target = CellValue; + + fn deref(&self) -> &Self::Target { + &self.0 + } +} + +fn decompose_for_scalar_mul(scalar: Option) -> Vec> { + let bits = 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) + }; + + // `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 + }); + + if let Some(bits) = bits { + bits.into_iter().map(Some).collect() + } else { + vec![None; pallas::Scalar::NUM_BITS as usize] + } +} + +#[cfg(test)] +pub mod tests { + use halo2::{circuit::Layouter, plonk::Error}; + use pasta_curves::{arithmetic::FieldExt, pallas}; + + use crate::circuit::gadget::ecc::{EccInstructions, Point, ScalarVar}; + + pub fn test_mul + Clone + Eq + std::fmt::Debug>( + chip: EccChip, + mut layouter: impl Layouter, + zero: &Point, + p: &Point, + ) -> Result<(), Error> { + 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 + // uses incomplete addition at the beginning of its double-and-add. + zero.mul(layouter.namespace(|| "mul"), &scalar) + .expect_err("[a]𝒪 should return an error"); + + // [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, layouter.namespace(|| "ScalarVar"), Some(scalar_val))?; + p.mul(layouter.namespace(|| "mul"), &scalar)?; + + Ok(()) + } +} diff --git a/src/circuit/gadget/ecc/chip/mul/complete.rs b/src/circuit/gadget/ecc/chip/mul/complete.rs new file mode 100644 index 00000000..67b08996 --- /dev/null +++ b/src/circuit/gadget/ecc/chip/mul/complete.rs @@ -0,0 +1,224 @@ +use super::super::{add, copy, CellValue, EccPoint, Var}; +use super::{COMPLETE_RANGE, X, Y, Z}; + +use halo2::{ + circuit::Region, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector}, + poly::Rotation, +}; + +use pasta_curves::{arithmetic::FieldExt, pallas}; + +pub struct Config { + // Selector used to constrain the cells used in complete addition. + q_mul_complete: Selector, + // Advice column used to decompose scalar in complete addition. + 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 Config { + /// Gate used to check scalar decomposition is correct. + /// This is used to check the bits used in complete addition, since the incomplete + /// addition gate (controlled by `q_mul`) already checks scalar decomposition for + /// the other bits. + pub(super) fn create_gate(&self, meta: &mut ConstraintSystem) { + 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 z_cur = meta.query_advice(self.z_complete, Rotation::cur()); + let z_prev = meta.query_advice(self.z_complete, Rotation::prev()); + + // k_{i} = z_{i} - 2⋅z_{i+1} + let k = z_cur - Expression::Constant(pallas::Base::from_u64(2)) * z_prev; + // (k_i) ⋅ (k_i - 1) = 0 + let bool_check = k.clone() * (k + Expression::Constant(-pallas::Base::one())); + + vec![q_mul_complete * bool_check] + }, + ); + } + + #[allow(clippy::type_complexity)] + #[allow(non_snake_case)] + #[allow(clippy::too_many_arguments)] + pub(super) fn assign_region( + &self, + region: &mut Region<'_, pallas::Base>, + offset: usize, + bits: &[Option], + base: &EccPoint, + x_a: X, + y_a: Y, + z: Z, + ) -> Result<(EccPoint, Vec>), Error> { + // Make sure we have the correct number of bits for the complete addition + // part of variable-base scalar mul. + assert_eq!(bits.len(), COMPLETE_RANGE.len()); + + // Enable selectors for complete range + for row in 0..COMPLETE_RANGE.len() { + // 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 + // `row + offset + 1` (instead of `row + offset`). + self.q_mul_complete.enable(region, row + offset + 1)?; + } + + // Use x_a, y_a output from incomplete addition + let mut acc = { + // Copy in x_a output from incomplete addition + let x_a = copy( + region, + || "x_a output from incomplete addition", + self.add_config.x_qr, + offset, + &x_a.0, + &self.perm, + )?; + + // Assign final `y_a` output from incomplete addition + let y_a_cell = region.assign_advice( + || "y_a", + self.add_config.y_qr, + offset, + || y_a.ok_or(Error::SynthesisError), + )?; + + EccPoint { + x: x_a, + y: CellValue::::new(y_a_cell, *y_a), + } + }; + + // Copy running sum `z` from incomplete addition + let mut z = { + let z = copy( + region, + || "Copy `z` running sum from incomplete addition", + self.z_complete, + offset, + &z, + &self.perm, + )?; + Z(z) + }; + + // Store interstitial running sum `z`s in vector + let mut zs: Vec> = Vec::new(); + + // Complete addition + for (iter, k) in bits.iter().enumerate() { + // Each iteration uses 2 rows (two complete additions) + let row = 2 * iter; + + // Copy `z` running sum from previous iteration. + copy( + region, + || "Copy `z` running sum from previous iteration", + self.z_complete, + row + offset, + &z, + &self.perm, + )?; + + // Update `z`. + z = { + // z_next = z_cur * 2 + k_next + let z_val = z.value().zip(k.as_ref()).map(|(z_val, k)| { + pallas::Base::from_u64(2) * z_val + pallas::Base::from_u64(*k as u64) + }); + let z_cell = region.assign_advice( + || "z", + self.z_complete, + row + offset + 1, + || z_val.ok_or(Error::SynthesisError), + )?; + Z(CellValue::new(z_cell, z_val)) + }; + zs.push(z); + + // Assign `x_p` for complete addition + let x_p = { + let x_p_val = base.x.value(); + let x_p_cell = region.assign_advice( + || "x_p", + self.add_config.x_p, + row + offset, + || x_p_val.ok_or(Error::SynthesisError), + )?; + CellValue::::new(x_p_cell, x_p_val) + }; + + // Assign `y_p` for complete addition. + let y_p = { + let y_p = base.y.value(); + + // If the bit is set, use `y`; if the bit is not set, use `-y` + let y_p = y_p + .zip(k.as_ref()) + .map(|(y_p, k)| if !k { -y_p } else { y_p }); + + let y_p_cell = region.assign_advice( + || "y_p", + self.add_config.y_p, + row + offset, + || y_p.ok_or(Error::SynthesisError), + )?; + CellValue::::new(y_p_cell, y_p) + }; + + // U = P if the bit is set; U = -P is the bit is not set. + let U = EccPoint { x: x_p, y: y_p }; + + // Acc + U + let tmp_acc = self + .add_config + .assign_region(&U, &acc, row + offset, region)?; + + // Copy acc from `x_a`, `y_a` over to `x_p`, `y_p` on the next row + acc = { + let acc_x = copy( + region, + || "copy acc x_a", + self.add_config.x_p, + row + offset + 1, + &acc.x, + &self.perm, + )?; + let acc_y = copy( + region, + || "copy acc y_a", + self.add_config.y_p, + row + offset + 1, + &acc.y, + &self.perm, + )?; + + EccPoint { x: acc_x, y: acc_y } + }; + + // Acc + U + Acc + acc = self + .add_config + .assign_region(&acc, &tmp_acc, row + offset + 1, region)?; + } + Ok((acc, zs)) + } +} diff --git a/src/circuit/gadget/ecc/chip/mul/incomplete.rs b/src/circuit/gadget/ecc/chip/mul/incomplete.rs new file mode 100644 index 00000000..17bea752 --- /dev/null +++ b/src/circuit/gadget/ecc/chip/mul/incomplete.rs @@ -0,0 +1,296 @@ +use std::array; + +use super::super::{copy, CellValue, EccConfig, EccPoint, Var}; +use super::{INCOMPLETE_HI_RANGE, INCOMPLETE_LO_RANGE, X, Y, Z}; +use ff::Field; +use halo2::{ + circuit::Region, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector}, + poly::Rotation, +}; + +use pasta_curves::{arithmetic::FieldExt, pallas}; + +pub(super) struct Config { + // Number of bits covered by this incomplete range. + num_bits: usize, + // Selector used to constrain the cells used in incomplete addition. + pub(super) q_mul: Selector, + // Cumulative sum used to decompose the scalar. + pub(super) z: Column, + // x-coordinate of the accumulator in each double-and-add iteration. + pub(super) x_a: Column, + // x-coordinate of the point being added in each double-and-add iteration. + pub(super) x_p: Column, + // y-coordinate of the point being added in each double-and-add iteration. + pub(super) y_p: Column, + // lambda1 in each double-and-add iteration. + pub(super) lambda1: Column, + // lambda2 in each double-and-add iteration. + pub(super) lambda2: Column, + // Permutation + 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 { + num_bits: INCOMPLETE_HI_RANGE.len(), + q_mul: ecc_config.q_mul_hi, + x_p: ecc_config.advices[0], + y_p: ecc_config.advices[1], + z: ecc_config.advices[9], + x_a: ecc_config.advices[3], + lambda1: ecc_config.advices[4], + lambda2: ecc_config.advices[5], + perm: ecc_config.perm.clone(), + } + } + + // 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 { + num_bits: INCOMPLETE_LO_RANGE.len(), + q_mul: ecc_config.q_mul_lo, + x_p: ecc_config.advices[0], + y_p: ecc_config.advices[1], + z: ecc_config.advices[6], + x_a: ecc_config.advices[7], + lambda1: ecc_config.advices[8], + lambda2: ecc_config.advices[2], + perm: ecc_config.perm.clone(), + } + } + + // 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| { + let q_mul = meta.query_selector(self.q_mul); + let z_cur = meta.query_advice(self.z, Rotation::cur()); + let z_prev = meta.query_advice(self.z, Rotation::prev()); + let x_a_cur = meta.query_advice(self.x_a, Rotation::cur()); + let x_a_next = meta.query_advice(self.x_a, Rotation::next()); + let x_p_cur = meta.query_advice(self.x_p, Rotation::cur()); + let x_p_next = meta.query_advice(self.x_p, Rotation::next()); + let y_p_cur = meta.query_advice(self.y_p, Rotation::cur()); + let y_p_next = meta.query_advice(self.y_p, Rotation::next()); + let lambda1_cur = meta.query_advice(self.lambda1, Rotation::cur()); + let lambda2_cur = meta.query_advice(self.lambda2, Rotation::cur()); + let lambda1_next = meta.query_advice(self.lambda1, Rotation::next()); + let lambda2_next = meta.query_advice(self.lambda2, Rotation::next()); + + // The current bit in the scalar decomposition, k_i = z_i - 2⋅z_{i+1}. + // Recall that we assigned the cumulative variable `z_i` in descending order, + // i from n down to 0. So z_{i+1} corresponds to the `z_prev` query. + let k = z_cur - Expression::Constant(pallas::Base::from_u64(2)) * z_prev; + + // y_{A,i} = (λ_{1,i} + λ_{2,i}) + // * (x_{A,i} - (λ_{1,i}^2 - x_{A,i} - x_{P,i})) / 2 + let y_a_cur = (lambda1_cur.clone() + lambda2_cur.clone()) + * (x_a_cur.clone() + - (lambda1_cur.clone() * lambda1_cur.clone() + - x_a_cur.clone() + - x_p_cur.clone())) + * pallas::Base::TWO_INV; + + // y_{A,i+1} = (λ_{1,i+1} + λ_{2,i+1}) + // * (x_{A,i+1} - (λ_{1,i+1}^2 - x_{A,i+1} - x_{P,i+1})) / 2 + let y_a_next = (lambda1_next.clone() + lambda2_next) + * (x_a_next.clone() + - (lambda1_next.clone() * lambda1_next - x_a_next.clone() - x_p_next.clone())) + * pallas::Base::TWO_INV; + + // Check booleanity of decomposition. + let bool_check = k.clone() * (k.clone() + Expression::Constant(-pallas::Base::one())); + + // The base used in double-and-add remains constant. We check that its + // x- and y- coordinates are the same throughout. + let x_p_check = x_p_cur.clone() - x_p_next; + let y_p_check = y_p_cur.clone() - y_p_next; + + // λ_{1,i}⋅(x_{A,i} − x_{P,i}) − y_{A,i} + (2k_i - 1) y_{P,i} = 0 + let poly1 = lambda1_cur.clone() * (x_a_cur.clone() - x_p_cur.clone()) - y_a_cur.clone() + + (k * pallas::Base::from_u64(2) + Expression::Constant(-pallas::Base::one())) + * y_p_cur; + + // (λ_{1,i} + λ_{2,i})⋅(x_{A,i} − (λ_{1,i}^2 − x_{A,i} − x_{P,i})) − 2y_{A,i}) = 0 + let poly2 = { + let lambda_neg = lambda1_cur.clone() + lambda2_cur.clone(); + let lambda1_expr = + lambda1_cur.clone() * lambda1_cur.clone() - x_a_cur.clone() - x_p_cur.clone(); + lambda_neg * (x_a_cur.clone() - lambda1_expr) + - Expression::Constant(pallas::Base::from_u64(2)) * y_a_cur.clone() + }; + + // λ_{2,i}^2 − x_{A,i+1} −(λ_{1,i}^2 − x_{A,i} − x_{P,i}) − x_{A,i} = 0 + let poly3 = lambda2_cur.clone() * lambda2_cur.clone() + - x_a_next.clone() + - (lambda1_cur.clone() * lambda1_cur) + + x_p_cur; + + // λ_{2,i}⋅(x_{A,i} − x_{A,i+1}) − y_{A,i} − y_{A,i+1} = 0 + let poly4 = lambda2_cur * (x_a_cur - x_a_next) - y_a_cur - y_a_next; + + array::IntoIter::new([bool_check, x_p_check, y_p_check, poly1, poly2, poly3, poly4]) + .map(move |poly| q_mul.clone() * poly) + }); + } + + // We perform incomplete addition on all but the last three bits of the + // decomposed scalar. + // We split the bits in the incomplete addition range into "hi" and "lo" + // halves and process them side by side, using the same rows but with + // non-overlapping columns. + // Returns (x, y, z). + #[allow(clippy::type_complexity)] + pub(super) fn double_and_add( + &self, + region: &mut Region<'_, pallas::Base>, + offset: usize, + base: &EccPoint, + bits: &[Option], + acc: (X, Y, Z), + ) -> Result<(X, Y, Vec>), Error> { + // Check that we have the correct number of bits for this double-and-add. + assert_eq!(bits.len(), self.num_bits); + + // Handle exceptional cases + let (x_p, y_p) = (base.x.value(), base.y.value()); + let (x_a, y_a) = (acc.0.value(), acc.1 .0); + + if let (Some(x_a), Some(y_a), Some(x_p), Some(y_p)) = (x_a, y_a, x_p, y_p) { + // A is point at infinity + if (x_p == pallas::Base::zero() && y_p == pallas::Base::zero()) + // Q is point at infinity + || (x_a == pallas::Base::zero() && y_a == pallas::Base::zero()) + // x_p = x_a + || (x_p == x_a) + { + return Err(Error::SynthesisError); + } + } + + // Enable `q_mul` on all but the last row of the incomplete range. + for row in 1..(self.num_bits - 1) { + self.q_mul.enable(region, offset + row)?; + } + + // Initialise the running `z` sum for the scalar bits. + let mut z = copy(region, || "starting z", self.z, offset, &acc.2, &self.perm)?; + + // Increase offset by 1; we used row 0 for initializing `z`. + let offset = offset + 1; + + // Define `x_p`, `y_p` + let x_p = base.x.value(); + let y_p = base.y.value(); + + // Initialise acc + let mut x_a = copy( + region, + || "starting x_a", + self.x_a, + offset, + &acc.0, + &self.perm, + )?; + let mut y_a = *acc.1; + + // Initialise vector to store all interstitial `z` running sum values. + let mut zs: Vec> = Vec::new(); + + // Incomplete addition + for (row, k) in bits.iter().enumerate() { + // z_{i} = 2 * z_{i+1} + k_i + let z_val = z.value().zip(k.as_ref()).map(|(z_val, k)| { + pallas::Base::from_u64(2) * z_val + pallas::Base::from_u64(*k as u64) + }); + let z_cell = region.assign_advice( + || "z", + self.z, + row + offset, + || z_val.ok_or(Error::SynthesisError), + )?; + z = CellValue::new(z_cell, z_val); + zs.push(Z(z)); + + // Assign `x_p`, `y_p` + region.assign_advice( + || "x_p", + self.x_p, + row + offset, + || x_p.ok_or(Error::SynthesisError), + )?; + region.assign_advice( + || "y_p", + self.y_p, + row + offset, + || y_p.ok_or(Error::SynthesisError), + )?; + + // If the bit is set, use `y`; if the bit is not set, use `-y` + let y_p = y_p + .zip(k.as_ref()) + .map(|(y_p, k)| if !k { -y_p } else { y_p }); + + // Compute and assign λ1⋅(x_A − x_P) = y_A − y_P + let lambda1 = y_a + .zip(y_p) + .zip(x_a.value()) + .zip(x_p) + .map(|(((y_a, y_p), x_a), x_p)| (y_a - y_p) * (x_a - x_p).invert().unwrap()); + region.assign_advice( + || "lambda1", + self.lambda1, + row + offset, + || lambda1.ok_or(Error::SynthesisError), + )?; + + // x_R = λ1^2 - x_A - x_P + let x_r = lambda1 + .zip(x_a.value()) + .zip(x_p) + .map(|((lambda1, x_a), x_p)| lambda1 * lambda1 - x_a - x_p); + + // λ2 = (2(y_A) / (x_A - x_R)) - λ1 + let lambda2 = + lambda1 + .zip(y_a) + .zip(x_a.value()) + .zip(x_r) + .map(|(((lambda1, y_a), x_a), x_r)| { + pallas::Base::from_u64(2) * y_a * (x_a - x_r).invert().unwrap() - lambda1 + }); + region.assign_advice( + || "lambda2", + self.lambda2, + row + offset, + || lambda2.ok_or(Error::SynthesisError), + )?; + + // Compute and assign `x_a` for the next row + let x_a_new = lambda2 + .zip(x_a.value()) + .zip(x_r) + .map(|((lambda2, x_a), x_r)| lambda2 * lambda2 - x_a - x_r); + y_a = lambda2 + .zip(x_a.value()) + .zip(x_a_new) + .zip(y_a) + .map(|(((lambda2, x_a), x_a_new), y_a)| lambda2 * (x_a - x_a_new) - y_a); + let x_a_val = x_a_new; + let x_a_cell = region.assign_advice( + || "x_a", + self.x_a, + row + offset + 1, + || x_a_val.ok_or(Error::SynthesisError), + )?; + x_a = CellValue::new(x_a_cell, x_a_val); + } + + Ok((X(x_a), Y(y_a), zs)) + } +} diff --git a/src/constants.rs b/src/constants.rs index ee9b943d..4c488692 100644 --- a/src/constants.rs +++ b/src/constants.rs @@ -20,6 +20,14 @@ pub mod util; pub use load::{OrchardFixedBase, OrchardFixedBasesFull, ValueCommitV}; +/// The Pallas scalar field modulus is $q = 2^{254} + \mathsf{t_q}$. +/// +pub(crate) const T_Q: u128 = 45560315531506369815346746415080538113; + +/// The Pallas base field modulus is $p = 2^{254} + \mathsf{t_p}$. +/// +pub(crate) const T_P: u128 = 45560315531419706090280762371685220353; + /// $\mathsf{MerkleDepth^{Orchard}}$ pub(crate) const MERKLE_DEPTH_ORCHARD: usize = 32;