From 4d69dec00f3a9892e0f41f992895385a4590ce86 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 2 Jul 2021 16:41:18 +0800 Subject: [PATCH] mul::incomplete.rs: Constrain first and last y_a values. Co-authored-by: Jack Grigg --- src/circuit/gadget/ecc/chip.rs | 8 +- src/circuit/gadget/ecc/chip/mul.rs | 19 +- src/circuit/gadget/ecc/chip/mul/complete.rs | 13 +- src/circuit/gadget/ecc/chip/mul/incomplete.rs | 273 ++++++++++++------ src/circuit/gadget/ecc/chip/mul/overflow.rs | 3 - 5 files changed, 201 insertions(+), 115 deletions(-) diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs index fa1db983..2665bd30 100644 --- a/src/circuit/gadget/ecc/chip.rs +++ b/src/circuit/gadget/ecc/chip.rs @@ -88,9 +88,9 @@ pub struct EccConfig { pub q_add: Selector, /// Variable-base scalar multiplication (hi half) - pub q_mul_hi: Selector, + pub q_mul_hi: Column, /// Variable-base scalar multiplication (lo half) - pub q_mul_lo: Selector, + pub q_mul_lo: Column, /// Selector used to enforce boolean decomposition in variable-base scalar mul pub q_mul_decompose_var: Selector, /// Selector used to enforce switching logic on LSB in variable-base scalar mul @@ -179,8 +179,8 @@ impl EccChip { fixed_z: meta.fixed_column(), q_add_incomplete: meta.selector(), q_add: meta.selector(), - q_mul_hi: meta.selector(), - q_mul_lo: meta.selector(), + q_mul_hi: meta.fixed_column(), + q_mul_lo: meta.fixed_column(), q_mul_decompose_var: meta.selector(), q_mul_overflow: meta.selector(), q_mul_lsb: meta.selector(), diff --git a/src/circuit/gadget/ecc/chip/mul.rs b/src/circuit/gadget/ecc/chip/mul.rs index 09768c06..147c489d 100644 --- a/src/circuit/gadget/ecc/chip/mul.rs +++ b/src/circuit/gadget/ecc/chip/mul.rs @@ -39,8 +39,6 @@ const COMPLETE_RANGE: Range = INCOMPLETE_LEN..(INCOMPLETE_LEN + NUM_COMPL pub struct Config { // Fixed column used to constrain the initialization of the running sum to be zero. constants: Column, - // Selector used to check z_i = 2*z_{i+1} + k_i - q_mul_decompose_var: Selector, // Selector used to check switching logic on LSB q_mul_lsb: Selector, // Permutation @@ -61,7 +59,6 @@ impl From<&EccConfig> for Config { fn from(ecc_config: &EccConfig) -> Self { let config = Self { constants: ecc_config.constants, - q_mul_decompose_var: ecc_config.q_mul_decompose_var, q_mul_lsb: ecc_config.q_mul_lsb, perm: ecc_config.perm.clone(), add_config: ecc_config.into(), @@ -180,26 +177,23 @@ impl Config { 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( &mut region, offset, &base, bits_incomplete_hi, - (X(acc.x), Y(acc.y.value()), z_init), + (X(acc.x), Y(acc.y), 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 z = &zs_incomplete_hi.last().expect("should not be empty"); 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), + (x_a, y_a, **z), )?; // Move from incomplete addition to complete addition. @@ -299,9 +293,6 @@ impl Config { || z_0_val.ok_or(Error::SynthesisError), )?; - // Check that z_0 was properly derived from z_1. - self.q_mul_decompose_var.enable(region, offset)?; - Z(CellValue::new(z_0_cell, z_0_val)) }; @@ -387,9 +378,9 @@ impl Deref for X { #[derive(Copy, Clone, Debug)] // `y`-coordinate of the accumulator. -struct Y(Option); +struct Y(CellValue); impl Deref for Y { - type Target = Option; + type Target = CellValue; fn deref(&self) -> &Self::Target { &self.0 diff --git a/src/circuit/gadget/ecc/chip/mul/complete.rs b/src/circuit/gadget/ecc/chip/mul/complete.rs index 204a41fa..245be9c2 100644 --- a/src/circuit/gadget/ecc/chip/mul/complete.rs +++ b/src/circuit/gadget/ecc/chip/mul/complete.rs @@ -102,17 +102,16 @@ impl Config { )?; // Assign final `y_a` output from incomplete addition - let y_a_cell = region.assign_advice( - || "y_a", + let y_a = copy( + region, + || "y_a output from incomplete addition", self.add_config.y_qr, offset, - || y_a.ok_or(Error::SynthesisError), + &y_a.0, + &self.perm, )?; - EccPoint { - x: x_a, - y: CellValue::::new(y_a_cell, *y_a), - } + EccPoint { x: x_a, y: y_a } }; // Copy running sum `z` from incomplete addition diff --git a/src/circuit/gadget/ecc/chip/mul/incomplete.rs b/src/circuit/gadget/ecc/chip/mul/incomplete.rs index feae9c3a..16aff5b3 100644 --- a/src/circuit/gadget/ecc/chip/mul/incomplete.rs +++ b/src/circuit/gadget/ecc/chip/mul/incomplete.rs @@ -1,11 +1,13 @@ -use std::{array, ops::Deref}; +use std::ops::Deref; 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}, + plonk::{ + Advice, Column, ConstraintSystem, Error, Expression, Fixed, Permutation, VirtualCells, + }, poly::Rotation, }; @@ -15,7 +17,7 @@ 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, + pub(super) q_mul: Column, // Cumulative sum used to decompose the scalar. pub(super) z: Column, // x-coordinate of the accumulator in each double-and-add iteration. @@ -90,74 +92,128 @@ 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| { - 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()); + let q_mul = meta.query_fixed(self.q_mul, Rotation::cur()); - // 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; + // Useful constants + let one = Expression::Constant(pallas::Base::one()); + let two = Expression::Constant(pallas::Base::from_u64(2)); + let three = Expression::Constant(pallas::Base::from_u64(3)); - // 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() + // Closures for expressions that are derived multiple times + // x_{R,i} = λ_{1,i}^2 - x_{A,i} - x_{P,i} + let x_r = |meta: &mut VirtualCells, rotation| { + let x_a = meta.query_advice(self.x_a, rotation); + let x_p = meta.query_advice(self.x_p, rotation); + let lambda_1 = meta.query_advice(self.lambda1, rotation); + lambda_1.square() - x_a - x_p }; - // λ_{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; + // y_{A,i} = (λ_{1,i} + λ_{2,i}) * (x_{A,i} - x_{R,i}) / 2 + let y_a = |meta: &mut VirtualCells, rotation: Rotation| { + let x_a = meta.query_advice(self.x_a, rotation); + let lambda_1 = meta.query_advice(self.lambda1, rotation); + let lambda_2 = meta.query_advice(self.lambda2, rotation); - // λ_{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; + (lambda_1 + lambda_2) * (x_a - x_r(meta, rotation)) * pallas::Base::TWO_INV + }; - array::IntoIter::new([bool_check, x_p_check, y_p_check, poly1, poly2, poly3, poly4]) - .map(move |poly| q_mul.clone() * poly) + let y_a_cur = y_a(meta, Rotation::cur()); + let y_a_next = y_a(meta, Rotation::next()); + + // q_mul == 1 + let q_mul_one_checks = { + let q_mul_is_one = + q_mul.clone() * (two.clone() - q_mul.clone()) * (three.clone() - q_mul.clone()); + let y_a_witnessed = meta.query_advice(self.lambda1, Rotation::cur()); + let y_a = y_a_next.clone(); + Some(("init y_a", q_mul_is_one * (y_a - y_a_witnessed))) + }; + + // q_mul == 2 + let q_mul_two_checks = { + let q_mul_is_two = + q_mul.clone() * (one.clone() - q_mul.clone()) * (three - q_mul.clone()); + + // z_i + let z_cur = meta.query_advice(self.z, Rotation::cur()); + // z_{i+1} + let z_prev = meta.query_advice(self.z, Rotation::prev()); + // x_{A,i} + let x_a_cur = meta.query_advice(self.x_a, Rotation::cur()); + // x_{A,i-1} + let x_a_next = meta.query_advice(self.x_a, Rotation::next()); + // x_{P,i} + let x_p_cur = meta.query_advice(self.x_p, Rotation::cur()); + // x_{P,i-1} + let x_p_next = meta.query_advice(self.x_p, Rotation::next()); + // y_{P,i} + let y_p_cur = meta.query_advice(self.y_p, Rotation::cur()); + // y_{P,i-1} + let y_p_next = meta.query_advice(self.y_p, Rotation::next()); + // λ_{1,i} + let lambda1_cur = meta.query_advice(self.lambda1, Rotation::cur()); + // λ_{2,i} + let lambda2_cur = meta.query_advice(self.lambda2, Rotation::cur()); + + // 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 - z_prev * pallas::Base::from_u64(2); + // Check booleanity of decomposition. + let bool_check = k.clone() * (one.clone() - k.clone()); + + // 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 * (x_a_cur.clone() - x_p_cur) - y_a_cur.clone() + + (k * pallas::Base::from_u64(2) - one.clone()) * y_p_cur; + + // λ_{2,i}^2 − x_{A,i-1} − x_{R,i} − x_{A,i} = 0 + let secant_line = lambda2_cur.clone().square() + - x_a_next.clone() + - x_r(meta, Rotation::cur()) + - x_a_cur.clone(); + + // λ_{2,i}⋅(x_{A,i} − x_{A,i-1}) − y_{A,i} − y_{A,i-1} = 0 + let poly3 = lambda2_cur * (x_a_cur - x_a_next) - y_a_cur - y_a_next; + + std::iter::empty() + .chain(Some(( + "bool_check when q_mul = 2", + q_mul_is_two.clone() * bool_check, + ))) + .chain(Some(("x_p_check", q_mul_is_two.clone() * x_p_check))) + .chain(Some(("y_p_check", q_mul_is_two.clone() * y_p_check))) + .chain(Some(("poly1", q_mul_is_two.clone() * poly1))) + .chain(Some(("secant_line", q_mul_is_two.clone() * secant_line))) + .chain(Some(("poly3", q_mul_is_two * poly3))) + }; + + // q_mul == 3 + let q_mul_three_checks = { + let q_mul_is_three = q_mul.clone() * (one - q_mul.clone()) * (two - q_mul); + let y_a_final = meta.query_advice(self.lambda1, Rotation::cur()); + let x_a_final = meta.query_advice(self.x_a, Rotation::cur()); + + // λ_{2,prev}⋅(x_{A,prev} − x_{A,final}) − y_{A,prev} − y_{A,final} = 0 + let poly3 = { + let lambda2_prev = meta.query_advice(self.lambda2, Rotation::prev()); + let x_a_prev = meta.query_advice(self.x_a, Rotation::prev()); + let y_a_prev = y_a(meta, Rotation::prev()); + + lambda2_prev * (x_a_prev - x_a_final) - y_a_prev - y_a_final + }; + + Some(("final y_a", q_mul_is_three * poly3)) + }; + + std::iter::empty() + .chain(q_mul_one_checks) + .chain(q_mul_two_checks) + .chain(q_mul_three_checks) }); } @@ -181,7 +237,7 @@ impl Config { // 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); + let (x_a, y_a) = (acc.0.value(), acc.1.value()); 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 @@ -195,32 +251,64 @@ impl Config { } } - // 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)?; + // Set q_mul values + { + // q_mul = 1 on offset 0 + region.assign_fixed( + || "q_mul = 1", + self.q_mul, + offset, + || Ok(pallas::Base::one()), + )?; + + // q_mul = 2 on all rows after offset 0, excluding the last row. + for idx in 1..(self.num_bits) { + region.assign_fixed( + || "q_mul = 2", + self.q_mul, + offset + idx, + || Ok(pallas::Base::from_u64(2)), + )?; + } + + // q_mul = 3 on the last row. + region.assign_fixed( + || "q_mul = 3", + self.q_mul, + offset + self.num_bits + 1, + || Ok(pallas::Base::from_u64(3)), + )?; } - // Initialise the running `z` sum for the scalar bits. - let mut z = copy(region, || "starting z", self.z, offset, &acc.2, &self.perm)?; + // Initialise double-and-add + let (mut x_a, mut y_a, mut z) = { + // Initialise the running `z` sum for the scalar bits. + let z = copy(region, || "starting z", self.z, offset, &acc.2, &self.perm)?; + + // Initialise acc + let x_a = copy( + region, + || "starting x_a", + self.x_a, + offset + 1, + &acc.0, + &self.perm, + )?; + let y_a = copy( + region, + || "starting y_a", + self.lambda1, + offset, + &acc.1, + &self.perm, + )?; + + (x_a, y_a.value(), z) + }; // 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(); @@ -297,7 +385,7 @@ impl Config { let x_a_new = lambda2 .zip(x_a.value()) .zip(x_r) - .map(|((lambda2, x_a), x_r)| lambda2 * lambda2 - x_a - x_r); + .map(|((lambda2, x_a), x_r)| lambda2.square() - x_a - x_r); y_a = lambda2 .zip(x_a.value()) .zip(x_a_new) @@ -313,6 +401,17 @@ impl Config { x_a = CellValue::new(x_a_cell, x_a_val); } + // Witness final y_a + let y_a = { + let cell = region.assign_advice( + || "y_a", + self.lambda1, + offset + self.num_bits, + || y_a.ok_or(Error::SynthesisError), + )?; + CellValue::new(cell, y_a) + }; + Ok((X(x_a), Y(y_a), zs)) } } diff --git a/src/circuit/gadget/ecc/chip/mul/overflow.rs b/src/circuit/gadget/ecc/chip/mul/overflow.rs index 794d9f39..c5350480 100644 --- a/src/circuit/gadget/ecc/chip/mul/overflow.rs +++ b/src/circuit/gadget/ecc/chip/mul/overflow.rs @@ -16,8 +16,6 @@ use pasta_curves::{arithmetic::FieldExt, pallas}; use std::iter; pub struct Config { - // Selector to check decomposition of lsb - q_mul_decompose_var: Selector, // Selector to check z_0 = alpha + t_q (mod p) q_mul_overflow: Selector, // 10-bit lookup table @@ -31,7 +29,6 @@ pub struct Config { impl From<&EccConfig> for Config { fn from(ecc_config: &EccConfig) -> Self { Self { - q_mul_decompose_var: ecc_config.q_mul_decompose_var, q_mul_overflow: ecc_config.q_mul_overflow, lookup_config: ecc_config.lookup_config.clone(), advices: [