From 69d6629ac6dcb40ca8818848f20a9c12ec2b0b46 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Sat, 19 Jun 2021 02:11:47 +0800 Subject: [PATCH] chip::mul.rs: Enforce LSB if/else condition On the LSB of the scalar, we assign a point (x,y) = (x_p, -y_p) if LSB = 0, and (0,0) otherwise. This if/else condition must be enforced. Co-authored-by: Sean Bowe --- src/circuit/gadget/ecc/chip.rs | 14 +-- src/circuit/gadget/ecc/chip/mul.rs | 101 ++++++++++++++---- src/circuit/gadget/ecc/chip/mul/complete.rs | 12 +-- src/circuit/gadget/ecc/chip/mul/overflow.rs | 4 +- .../ecc/chip/witness_scalar_fixed/short.rs | 2 +- 5 files changed, 99 insertions(+), 34 deletions(-) diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs index 6c046213..aa5aa073 100644 --- a/src/circuit/gadget/ecc/chip.rs +++ b/src/circuit/gadget/ecc/chip.rs @@ -91,12 +91,12 @@ pub struct EccConfig { pub q_mul_hi: Selector, /// Variable-base scalar multiplication (lo half) 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 + /// Selector used to initialize running sum to zero in variable-base scalar mul pub q_init_z: Selector, - /// Variable-base scalar multiplication (final scalar) - pub q_mul_z: Selector, + /// 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 + pub q_mul_lsb: Selector, /// Variable-base scalar multiplication (overflow check) pub q_mul_overflow: Selector, @@ -171,10 +171,10 @@ impl EccChip { q_add: meta.selector(), q_mul_hi: meta.selector(), q_mul_lo: meta.selector(), - q_mul_decompose_var: meta.selector(), q_init_z: meta.selector(), - q_mul_z: meta.selector(), + q_mul_decompose_var: meta.selector(), q_mul_overflow: meta.selector(), + q_mul_lsb: meta.selector(), mul_fixed: meta.fixed_column(), q_mul_fixed_short: meta.selector(), base_field_fixed: meta.fixed_column(), diff --git a/src/circuit/gadget/ecc/chip/mul.rs b/src/circuit/gadget/ecc/chip/mul.rs index 42a87569..fda5cb89 100644 --- a/src/circuit/gadget/ecc/chip/mul.rs +++ b/src/circuit/gadget/ecc/chip/mul.rs @@ -1,5 +1,8 @@ use super::{add, CellValue, EccConfig, EccPoint, EccScalarVar, Var}; -use crate::constants::{NUM_COMPLETE_BITS, T_Q}; +use crate::{ + circuit::gadget::utilities::copy, + constants::{NUM_COMPLETE_BITS, T_Q}, +}; use std::ops::{Deref, Range}; use bigint::U256; @@ -7,7 +10,7 @@ use ff::PrimeField; use halo2::{ arithmetic::FieldExt, circuit::{Layouter, Region}, - plonk::{ConstraintSystem, Error, Permutation, Selector}, + plonk::{ConstraintSystem, Error, Expression, Permutation, Selector}, poly::Rotation, }; @@ -36,8 +39,10 @@ const COMPLETE_RANGE: Range = INCOMPLETE_LEN..(INCOMPLETE_LEN + NUM_COMPL pub struct Config { // Selector used to constrain the initialization of the running sum to be zero. q_init_z: Selector, - // Selector used to check z_0 = 2*z_1 + k_0 - q_mul_z: Selector, + // 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 perm: Permutation, // Configuration used in complete addition @@ -56,7 +61,8 @@ impl From<&EccConfig> for Config { fn from(ecc_config: &EccConfig) -> Self { let config = Self { q_init_z: ecc_config.q_init_z, - q_mul_z: ecc_config.q_mul_z, + 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(), hi_config: ecc_config.into(), @@ -79,6 +85,10 @@ impl From<&EccConfig> for Config { !add_config_advices.contains(&config.hi_config.z), "hi_config z cannot overlap with complete addition columns." ); + assert!( + !add_config_advices.contains(&config.complete_config.z_complete), + "complete_config z cannot overlap with complete addition columns." + ); config } @@ -94,6 +104,35 @@ impl Config { vec![q_init_z * z] }); + // If `lsb` is 0, (x, y) = (x_p, -y_p). If `lsb` is 1, (x, y) = (0,0). + meta.create_gate("LSB check", |meta| { + let q_mul_lsb = meta.query_selector(self.q_mul_lsb); + + let z_1 = meta.query_advice(self.complete_config.z_complete, Rotation::prev()); + let z_0 = meta.query_advice(self.complete_config.z_complete, Rotation::cur()); + let x_p = meta.query_advice(self.add_config.x_p, Rotation::next()); + let y_p = meta.query_advice(self.add_config.y_p, Rotation::next()); + let x = meta.query_advice(self.add_config.x_qr, Rotation::next()); + let y = meta.query_advice(self.add_config.y_qr, Rotation::next()); + + // z_0 = 2 * z_1 + k_0 + // => k_0 = z_0 - 2 * z_1 + let lsb = z_0 - z_1 * pallas::Base::from_u64(2); + + let one = Expression::Constant(pallas::Base::one()); + + // `lsb` = 0 => (x, y) = (x_p, -y_p) + let lsb0_x = (one.clone() - lsb.clone()) * (x.clone() - x_p); + let lsb0_y = (one - lsb.clone()) * (y.clone() + y_p); + + // `lsb` = 1 => (x, y) = (0,0) + let lsb1_x = lsb.clone() * x; + let lsb1_y = lsb * y; + + std::array::IntoIter::new([lsb0_x, lsb0_y, lsb1_x, lsb1_y]) + .map(move |poly| q_mul_lsb.clone() * poly) + }); + self.hi_config.create_gate(meta); self.lo_config.create_gate(meta); self.complete_config.create_gate(meta); @@ -245,6 +284,9 @@ impl Config { z_1: Z, lsb: Option, ) -> Result<(EccPoint, Z), Error> { + // Enforce switching logic on LSB using a custom gate + self.q_mul_lsb.enable(region, offset)?; + // Assign z_0 = 2⋅z_1 + k_0 let z_0 = { let z_0_val = z_1.value().zip(lsb).map(|(z_1, lsb)| { @@ -259,13 +301,33 @@ impl Config { )?; // Check that z_0 was properly derived from z_1. - self.q_mul_z.enable(region, offset)?; + self.q_mul_decompose_var.enable(region, offset)?; Z(CellValue::new(z_0_cell, z_0_val)) }; + let offset = offset + 1; + + // Copy in `x_p`, `y_p` to use in the LSB gate + copy( + region, + || "copy x_p", + self.add_config.x_p, + offset, + &base.x(), + &self.perm, + )?; + copy( + region, + || "copy y_p", + self.add_config.y_p, + offset, + &base.y(), + &self.perm, + )?; + // If `lsb` is 0, return `Acc + (-P)`. If `lsb` is 1, simply return `Acc + 0`. - let x_p = if let Some(lsb) = lsb { + let x = if let Some(lsb) = lsb { if !lsb { base.x.value() } else { @@ -274,7 +336,8 @@ impl Config { } else { None }; - let y_p = if let Some(lsb) = lsb { + + let y = if let Some(lsb) = lsb { if !lsb { base.y.value().map(|y_p| -y_p) } else { @@ -284,25 +347,27 @@ impl Config { None }; - let x_p_cell = region.assign_advice( - || "x_p", - self.add_config.x_p, + let x_cell = region.assign_advice( + || "x", + self.add_config.x_qr, offset, - || x_p.ok_or(Error::SynthesisError), + || x.ok_or(Error::SynthesisError), )?; - let y_p_cell = region.assign_advice( - || "y_p", - self.add_config.y_p, + let y_cell = region.assign_advice( + || "y", + self.add_config.y_qr, offset, - || y_p.ok_or(Error::SynthesisError), + || y.ok_or(Error::SynthesisError), )?; let p = EccPoint { - x: CellValue::::new(x_p_cell, x_p), - y: CellValue::::new(y_p_cell, y_p), + x: CellValue::::new(x_cell, x), + y: CellValue::::new(y_cell, y), }; + let offset = offset + 1; + // Return the result of the final complete addition as `[scalar]B` let result = self.add_config.assign_region(&p, &acc, offset, region)?; diff --git a/src/circuit/gadget/ecc/chip/mul/complete.rs b/src/circuit/gadget/ecc/chip/mul/complete.rs index 8bd75163..204a41fa 100644 --- a/src/circuit/gadget/ecc/chip/mul/complete.rs +++ b/src/circuit/gadget/ecc/chip/mul/complete.rs @@ -11,7 +11,7 @@ use pasta_curves::{arithmetic::FieldExt, pallas}; pub struct Config { // Selector used to constrain the cells used in complete addition. - q_mul_z: Selector, + q_mul_decompose_var: Selector, // Advice column used to decompose scalar in complete addition. pub z_complete: Column, // Permutation @@ -23,7 +23,7 @@ pub struct Config { impl From<&EccConfig> for Config { fn from(ecc_config: &EccConfig) -> Self { let config = Self { - q_mul_z: ecc_config.q_mul_z, + q_mul_decompose_var: ecc_config.q_mul_decompose_var, z_complete: ecc_config.advices[9], perm: ecc_config.perm.clone(), add_config: ecc_config.into(), @@ -48,7 +48,7 @@ impl Config { meta.create_gate( "Decompose scalar for complete bits of variable-base mul", |meta| { - let q_mul_z = meta.query_selector(self.q_mul_z); + let q_mul_decompose_var = meta.query_selector(self.q_mul_decompose_var); let z_cur = meta.query_advice(self.z_complete, Rotation::cur()); let z_prev = meta.query_advice(self.z_complete, Rotation::prev()); @@ -57,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_z * bool_check] + vec![q_mul_decompose_var * bool_check] }, ); } @@ -84,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_z` queries the previous row, we enable the selector on + // `q_mul_decompose_var` queries the previous row, we enable the selector on // `row + offset + 1` (instead of `row + offset`). - self.q_mul_z.enable(region, row + offset + 1)?; + self.q_mul_decompose_var.enable(region, row + offset + 1)?; } // Use x_a, y_a output from incomplete addition diff --git a/src/circuit/gadget/ecc/chip/mul/overflow.rs b/src/circuit/gadget/ecc/chip/mul/overflow.rs index 923a0199..2a741179 100644 --- a/src/circuit/gadget/ecc/chip/mul/overflow.rs +++ b/src/circuit/gadget/ecc/chip/mul/overflow.rs @@ -17,7 +17,7 @@ use std::iter; pub struct Config { // Selector to check decomposition of lsb - q_mul_z: Selector, + 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 +31,7 @@ pub struct Config { impl From<&EccConfig> for Config { fn from(ecc_config: &EccConfig) -> Self { Self { - q_mul_z: ecc_config.q_mul_z, + 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: [ diff --git a/src/circuit/gadget/ecc/chip/witness_scalar_fixed/short.rs b/src/circuit/gadget/ecc/chip/witness_scalar_fixed/short.rs index 65b4c0a4..861699a0 100644 --- a/src/circuit/gadget/ecc/chip/witness_scalar_fixed/short.rs +++ b/src/circuit/gadget/ecc/chip/witness_scalar_fixed/short.rs @@ -33,7 +33,7 @@ impl Config { let one = Expression::Constant(pallas::Base::one()); let last_window_check = last_window.clone() * (one.clone() - last_window); - let sign_check = (one.clone() + sign.clone()) * (one - sign); + let sign_check = sign.clone() * sign - one; vec![ q_scalar_fixed_short.clone() * last_window_check,