From 72e469ee10a95a91a223a1d4ca69431e2e015b26 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 7 Jul 2021 15:53:43 +0800 Subject: [PATCH] mul_fixed::base_field_elem.rs: Check canonicity of base field element used in fixed-base scalar mul. When using a base field element as the scalar in fixed-base mul, we check the canonicity of its decomposition. --- src/circuit/gadget/ecc/chip/add_incomplete.rs | 6 +- .../ecc/chip/mul_fixed/base_field_elem.rs | 374 +++++++++++++++--- 2 files changed, 317 insertions(+), 63 deletions(-) diff --git a/src/circuit/gadget/ecc/chip/add_incomplete.rs b/src/circuit/gadget/ecc/chip/add_incomplete.rs index 8877bba8..325f2792 100644 --- a/src/circuit/gadget/ecc/chip/add_incomplete.rs +++ b/src/circuit/gadget/ecc/chip/add_incomplete.rs @@ -1,4 +1,4 @@ -use std::array; +use std::{array, collections::HashSet}; use super::{copy, CellValue, EccConfig, EccPoint, Var}; use group::Curve; @@ -38,6 +38,10 @@ impl From<&EccConfig> for Config { } impl Config { + pub(crate) fn advice_columns(&self) -> HashSet> { + core::array::IntoIter::new([self.x_p, self.y_p, self.x_qr, self.y_qr]).collect() + } + pub(super) fn create_gate(&self, meta: &mut ConstraintSystem) { meta.create_gate("incomplete addition gates", |meta| { let q_add_incomplete = meta.query_selector(self.q_add_incomplete); diff --git a/src/circuit/gadget/ecc/chip/mul_fixed/base_field_elem.rs b/src/circuit/gadget/ecc/chip/mul_fixed/base_field_elem.rs index 219a2be1..8ee39925 100644 --- a/src/circuit/gadget/ecc/chip/mul_fixed/base_field_elem.rs +++ b/src/circuit/gadget/ecc/chip/mul_fixed/base_field_elem.rs @@ -1,12 +1,15 @@ use super::super::{EccBaseFieldElemFixed, EccConfig, EccPoint, OrchardFixedBasesFull}; use crate::{ - circuit::gadget::utilities::{copy, CellValue, Var}, - constants::{self, util::decompose_scalar_fixed, NUM_WINDOWS}, + circuit::gadget::utilities::{ + bitrange_subset, copy, lookup_range_check::LookupRangeCheckConfig, CellValue, Var, + }, + constants::{self, util::decompose_scalar_fixed, NUM_WINDOWS, T_P}, + primitives::sinsemilla, }; use halo2::{ circuit::{Layouter, Region}, - plonk::{Column, ConstraintSystem, Error, Expression, Fixed}, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector}, poly::Rotation, }; use pasta_curves::{arithmetic::FieldExt, pallas}; @@ -14,45 +17,66 @@ use pasta_curves::{arithmetic::FieldExt, pallas}; use arrayvec::ArrayVec; pub struct Config { - base_field_fixed: Column, + base_field_fixed_mul: Selector, + base_field_fixed_canon: Selector, + canon_advices: [Column; 3], + lookup_config: LookupRangeCheckConfig, super_config: super::Config<{ constants::NUM_WINDOWS }>, } impl From<&EccConfig> for Config { fn from(config: &EccConfig) -> Self { - Self { - base_field_fixed: config.base_field_fixed, + let config = Self { + base_field_fixed_mul: config.base_field_fixed_mul, + base_field_fixed_canon: config.base_field_fixed_canon, + canon_advices: [config.advices[7], config.advices[8], config.advices[9]], + lookup_config: config.lookup_config.clone(), super_config: config.into(), + }; + + let add_incomplete_advices = config.super_config.add_incomplete_config.advice_columns(); + for canon_advice in config.canon_advices.iter() { + assert!( + !add_incomplete_advices.contains(&canon_advice), + "Deconflict canon_advice columns with incomplete addition columns." + ); } + + config } } impl Config { pub fn create_gate(&self, meta: &mut ConstraintSystem) { + // Check that an expression is in the range [0..range), + // i.e. 0 ≤ word < range. + let range_check = |word: Expression, range: usize| { + (0..range).fold(Expression::Constant(pallas::Base::one()), |acc, i| { + acc * (word.clone() - Expression::Constant(pallas::Base::from_u64(i as u64))) + }) + }; + // Decompose the base field element α into three-bit windows // using a running sum `z`, where z_{i+1} = (z_i - a_i) / (2^3) - // for α = a_0 + (2^3) a_1 + ... + (2^{3(n-1)}) a_{n-1}. - // For a Pallas base field element (255 bits), n = 255 / 3 = 85. + // for α = a_0 + (2^3) a_1 + ... + (2^{3(84)}) a_{84}. // // We set z_0 = α, which implies: // z_1 = (α - a_0) / 2^3, (subtract the lowest 3 bits) - // = a_1 + (2^3) a_2 + ... + 2^{3(n-1)} a_{n-1}, + // = a_1 + (2^3) a_2 + ... + 2^{3(83)} a_{84}, // z_2 = (z_1 - a_1) / 2^3 - // = a_2 + (2^3) a_3 + ... + 2^{3(n-2)} a_{n-1}, + // = a_2 + (2^3) a_3 + ... + 2^{3(82)} a_{84}, // ..., - // z_{n-1} = a_{n-1} - // z_n = (z_{n-1} - a_{n-1}) / 2^3 + // z_{84} = a_{84} + // z_n = (z_{84} - a_{84}) / 2^3 // = 0. // // This gate checks that each a_i = z_i - z_{i+1} * (2^3) is within // 3 bits. + // + // This gate also checks that this window uses the correct y_p and + // interpolated x_p. meta.create_gate("Decompose base field element", |meta| { - // This gate is activated when base_field_fixed = 1 - let fixed_is_one = { - let base_field_fixed = meta.query_fixed(self.base_field_fixed, Rotation::cur()); - let two = Expression::Constant(pallas::Base::from_u64(2)); - base_field_fixed.clone() * (two - base_field_fixed) - }; + let base_field_fixed_mul = meta.query_selector(self.base_field_fixed_mul); let z_cur = meta.query_advice(self.super_config.window, Rotation::cur()); let z_next = meta.query_advice(self.super_config.window, Rotation::next()); @@ -62,40 +86,101 @@ impl Config { let word = z_cur - z_next * pallas::Base::from_u64(constants::H as u64); // (word - 7) * (word - 6) * ... * (word - 1) * word = 0 - let range_check = - (0..constants::H).fold(Expression::Constant(pallas::Base::one()), |acc, i| { - acc * (word.clone() - Expression::Constant(pallas::Base::from_u64(i as u64))) - }); + let range_check = range_check(word.clone(), constants::H); - vec![fixed_is_one * range_check] + self.super_config + .coords_check(meta, base_field_fixed_mul.clone(), word) + .into_iter() + .chain(Some(( + "Decomposition range check", + base_field_fixed_mul * range_check, + ))) }); - meta.create_gate("x_p, y_p checks for BaseFieldElemFixed", |meta| { - // This gate is activated when base_field_fixed = 1 - let fixed_is_one = { - let base_field_fixed = meta.query_fixed(self.base_field_fixed, Rotation::cur()); - let two = Expression::Constant(pallas::Base::from_u64(2)); - base_field_fixed.clone() * (base_field_fixed - two) + // Check that we get z_85 = 0 as the final output of the three-bit decomposition running sum. + // Also check that the base field element is canonical. + meta.create_gate("Canonicity checks", |meta| { + let base_field_fixed_canon = meta.query_selector(self.base_field_fixed_canon); + + let alpha = meta.query_advice(self.canon_advices[0], Rotation::prev()); + // z_85_alpha is constrained to be zero in this gate. + let z_85_alpha = meta.query_advice(self.canon_advices[1], Rotation::prev()); + // The last three bits of α. + let z_84_alpha = meta.query_advice(self.canon_advices[2], Rotation::prev()); + + // Decompose α into three pieces, + // α = α_0 (252 bits) || α_1 (2 bits) || α_2 (1 bit). + // + let alpha_0 = meta.query_advice(self.canon_advices[0], Rotation::cur()); + let alpha_1 = meta.query_advice(self.canon_advices[1], Rotation::cur()); + let alpha_2 = meta.query_advice(self.canon_advices[2], Rotation::cur()); + + let alpha_0_prime = meta.query_advice(self.canon_advices[0], Rotation::next()); + let z_13_alpha_0_prime = meta.query_advice(self.canon_advices[1], Rotation::next()); + let z_13_alpha_0 = meta.query_advice(self.canon_advices[2], Rotation::next()); + + let decomposition_checks = { + // Range-constrain α_1 to be 2 bits + let alpha_1_range_check = range_check(alpha_1.clone(), 1 << 2); + // Boolean-constrain α_2 + let alpha_2_range_check = range_check(alpha_2.clone(), 1 << 1); + // Check that α_1 + 2^2 α_2 = z_84_alpha + let z_84_alpha_check = z_84_alpha.clone() + - (alpha_1 + alpha_2.clone() * pallas::Base::from_u64(1 << 2)); + + // Check that the witnessed α_0 fulfils the constraint α_0 = α - z_84_alpha * 2^252 + let two_pow_252 = pallas::Base::from_u128(1 << 126).square(); + let expected_alpha_0 = alpha - (z_84_alpha * two_pow_252); + + std::iter::empty() + .chain(Some(("alpha_1_range_check", alpha_1_range_check))) + .chain(Some(("alpha_2_range_check", alpha_2_range_check))) + .chain(Some(("z_84_alpha_check", z_84_alpha_check))) + .chain(Some(("alpha_0_check", alpha_0.clone() - expected_alpha_0))) }; - let z_cur = meta.query_advice(self.super_config.window, Rotation::cur()); - let z_next = meta.query_advice(self.super_config.window, Rotation::next()); - let window = z_cur - z_next * pallas::Base::from_u64(constants::H as u64); - self.super_config.coords_check(meta, fixed_is_one, window) - }); - - // Check that we get z_85 = 0 as the final output of the running sum. - meta.create_gate("z_85 = 0", |meta| { - // This gate is activated when base_field_fixed = 2 - let fixed_is_two = { - let base_field_fixed = meta.query_fixed(self.base_field_fixed, Rotation::cur()); - let one = Expression::Constant(pallas::Base::one()); - base_field_fixed.clone() * (base_field_fixed - one) + // Check α_0_prime = α_0 + 2^130 - t_p + let alpha_0_prime_check = { + let two_pow_130 = Expression::Constant(pallas::Base::from_u128(65).square()); + let t_p = Expression::Constant(pallas::Base::from_u128(T_P)); + alpha_0_prime - (alpha_0 + two_pow_130 - t_p) }; - let z_85 = meta.query_advice(self.super_config.window, Rotation::cur()); + // We want to enforce canonicity of a 255-bit base field element, α. + // That is, we want to check that 0 ≤ α < p, where p is Pallas base + // field modulus p = 2^254 + t_p + // = 2^254 + 45560315531419706090280762371685220353. + // Note that t_p < 2^130. + // + // α has been decomposed into three pieces, + // α = α_0 (252 bits) || α_1 (2 bits) || α_2 (1 bit). + // + // If the MSB α_2 = 1, then: + // - α_2 = 1 => α_1 = 0, and + // - α_2 = 1 => α_0 < t_p. To enforce this: + // - α_2 = 1 => 0 ≤ α_0 < 2^130 + // => 13 ten-bit lookups of α_0 + // - α_2 = 1 => 0 ≤ α_0 + 2^130 - t_p < 2^130 + // => 13 ten-bit lookups of α_0 + 2^130 - t_p + // => z_13_alpha_0_prime = 0 + // + let canon_checks = { + std::iter::empty() + .chain(Some(( + "MSB = 1 => z_13_alpha_0 = 0", + alpha_2.clone() * z_13_alpha_0, + ))) + .chain(Some(( + "MSB = 1 => z_13_alpha_0_prime = 0", + alpha_2 * z_13_alpha_0_prime, + ))) + }; - vec![fixed_is_two * z_85] + canon_checks + .chain(decomposition_checks) + .chain(Some(("z_85_alpha = 0", z_85_alpha))) + .chain(Some(("alpha_0_prime check", alpha_0_prime_check))) + .map(move |(name, poly)| (name, base_field_fixed_canon.clone() * poly)) }); } @@ -105,7 +190,7 @@ impl Config { scalar: CellValue, base: OrchardFixedBasesFull, ) -> Result { - layouter.assign_region( + let (result, scalar) = layouter.assign_region( || "Base-field elem fixed-base mul", |mut region| { let offset = 0; @@ -118,7 +203,7 @@ impl Config { offset, &(&scalar).into(), base.into(), - self.base_field_fixed, + self.base_field_fixed_mul, )?; // Increase offset by 1 because the running sum decomposition takes @@ -151,9 +236,187 @@ impl Config { } } - Ok(result) + Ok((result, scalar)) }, - ) + )?; + + // We want to enforce canonicity of a 255-bit base field element, α. + // That is, we want to check that 0 ≤ α < p, where p is Pallas base + // field modulus p = 2^254 + t_p + // = 2^254 + 45560315531419706090280762371685220353. + // Note that t_p < 2^130. + // + // α has been decomposed into three pieces, + // α = α_0 (252 bits) || α_1 (2 bits) || α_2 (1 bit). + // + // If the MSB α_2 = 1, then: + // - α_2 = 1 => α_1 = 0, and + // - α_2 = 1 => α_0 < t_p. To enforce this: + // - α_2 = 1 => 0 ≤ α_0 < 2^130 + // => 13 ten-bit lookups of α_0 + // - α_2 = 1 => 0 ≤ α_0 + 2^130 - t_p < 2^130 + // => 13 ten-bit lookups of α_0 + 2^130 - t_p + // => z_13_alpha_0_prime = 0 + // + let (alpha, running_sum) = (scalar.base_field_elem, &scalar.running_sum); + let z_84_alpha = running_sum[83]; + let z_85_alpha = running_sum[84]; + + let (alpha_0, z_13_alpha_0) = { + // α_0 = α - z_84_alpha * 2^252 + let alpha_0 = alpha + .value() + .zip(z_84_alpha.value()) + .map(|(alpha, z_84_alpha)| { + let two_pow_252 = pallas::Base::from_u128(1 << 126).square(); + alpha - z_84_alpha * two_pow_252 + }); + + let (alpha_0, zs) = self.lookup_config.witness_check( + layouter.namespace(|| "Lookup range check alpha + 2^130 - t_p"), + alpha_0, + 13, + false, + )?; + + (alpha_0, zs[13]) + }; + + let (alpha_0_prime, z_13_alpha_0_prime) = { + // alpha_0_prime = alpha + 2^130 - t_p. + let alpha_0_prime = alpha_0.value().map(|alpha_0| { + let two_pow_130 = pallas::Base::from_u128(65).square(); + let t_p = pallas::Base::from_u128(T_P); + alpha_0 + two_pow_130 - t_p + }); + let (alpha_0_prime, zs) = self.lookup_config.witness_check( + layouter.namespace(|| "Lookup range check alpha_0 + 2^130 - t_p"), + alpha_0_prime, + 13, + false, + )?; + + (alpha_0_prime, zs[13]) + }; + + layouter.assign_region( + || "Canonicity checks", + |mut region| { + let perm = &self.super_config.perm; + + // Activate canonicity check gate + self.base_field_fixed_canon.enable(&mut region, 1)?; + + // Offset 0 + { + let offset = 0; + + // Copy α + copy( + &mut region, + || "Copy α", + self.canon_advices[0], + offset, + &alpha, + perm, + )?; + + // z_85_alpha is constrained to be zero in the custom gate. + copy( + &mut region, + || "Copy z_85_alpha", + self.canon_advices[1], + offset, + &z_85_alpha, + perm, + )?; + + // z_84_alpha = the top three bits of alpha. + copy( + &mut region, + || "Copy z_84_alpha", + self.canon_advices[2], + offset, + &z_84_alpha, + perm, + )?; + } + + // Offset 1 + { + let offset = 1; + + // Decompose α into three pieces, + // α = α_0 (252 bits) || α_1 (2 bits) || α_2 (1 bit). + // Copy α_0 + copy( + &mut region, + || "α_0", + self.canon_advices[0], + offset, + &alpha_0, + perm, + )?; + + // Witness α_1 = α[252..=253] + let alpha_1 = alpha.value().map(|alpha| bitrange_subset(alpha, 252..254)); + region.assign_advice( + || "α_1 = α[252..=253]", + self.canon_advices[1], + offset, + || alpha_1.ok_or(Error::SynthesisError), + )?; + + // Witness the MSB α_2 = α[254] + let alpha_2 = alpha.value().map(|alpha| bitrange_subset(alpha, 254..255)); + region.assign_advice( + || "α_2 = α[254]", + self.canon_advices[2], + offset, + || alpha_2.ok_or(Error::SynthesisError), + )?; + } + + // Offset 2 + { + let offset = 2; + // Copy alpha_0_prime = alpha_0 + 2^130 - t_p. + // We constrain this in the custom gate to be derived correctly. + copy( + &mut region, + || "Copy α_0 + 2^130 - t_p", + self.canon_advices[0], + offset, + &alpha_0_prime, + perm, + )?; + + // Copy z_13_alpha_0_prime + copy( + &mut region, + || "Copy z_13_alpha_0_prime", + self.canon_advices[1], + offset, + &z_13_alpha_0_prime, + perm, + )?; + + // Copy z_13_alpha_0, which is α with the first 130 bits subtracted. + copy( + &mut region, + || "Copy z_13_alpha_0", + self.canon_advices[2], + offset, + &z_13_alpha_0, + perm, + )?; + } + + Ok(()) + }, + )?; + + Ok(result) } fn decompose_base_field_elem( @@ -195,12 +458,7 @@ impl Config { )?; for idx in 0..words.len() { - region.assign_fixed( - || "Decomposition check", - self.base_field_fixed, - offset + idx, - || Ok(pallas::Base::from_u64(1)), - )?; + self.base_field_fixed_mul.enable(region, offset + idx)?; } let offset = offset + 1; @@ -228,14 +486,6 @@ impl Config { running_sum.push(z); } - let offset = offset + words.len() - 1; - region.assign_fixed( - || "Check z_85 = 0", - self.base_field_fixed, - offset, - || Ok(pallas::Base::from_u64(2)), - )?; - Ok(EccBaseFieldElemFixed { base_field_elem, running_sum,