zec
/
orchard
mirror of https://github.com/zcash/orchard.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

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.
This commit is contained in:
therealyingtong 2021-07-07 15:53:43 +08:00
parent b69094036c
commit 72e469ee10
2 changed files with 317 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/circuit/gadget/ecc/chip/add_incomplete.rs
View File

@ -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<Column<Advice>> {
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<pallas::Base>) {
meta.create_gate("incomplete addition gates", |meta| {
let q_add_incomplete = meta.query_selector(self.q_add_incomplete);

374
src/circuit/gadget/ecc/chip/mul_fixed/base_field_elem.rs
View File

@ -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<Fixed>,
base_field_fixed_mul: Selector,
base_field_fixed_canon: Selector,
canon_advices: [Column<Advice>; 3],
lookup_config: LookupRangeCheckConfig<pallas::Base, { sinsemilla::K }>,
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<pallas::Base>) {
// Check that an expression is in the range [0..range),
// i.e. 0 ≤ word < range.
let range_check = |word: Expression<pallas::Base>, 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<pallas::Base>,
base: OrchardFixedBasesFull,
) -> Result<EccPoint, Error> {
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,