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

lookup_range_check.rs: Downgrade from Chip to Config. 

We need to be able to toggle the lookup on and off on specific
offsets. These offsets are often assigned outside the logic of
the decomposition.
This commit is contained in:
therealyingtong 2021-06-13 09:40:50 +08:00
parent cdab5bf8c4
commit b299a51b31
1 changed files with 94 additions and 170 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

264
src/circuit/gadget/utilities/lookup_range_check.rs
View File

@ -3,8 +3,8 @@
use crate::primitives::sinsemilla::lebs2ip_k;
use halo2::{
circuit::{Chip, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation, Selector},
circuit::{Layouter, Region},
plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation},
poly::Rotation,
};
use std::marker::PhantomData;
@ -13,77 +13,33 @@ use ff::PrimeFieldBits;
use super::*;
pub trait LookupRangeCheckInstructions<
F: FieldExt + PrimeFieldBits + PrimeFieldBits,
const K: usize,
>: UtilitiesInstructions<F>
{
/// Decomposes a field element into K-bit words using a running sum.
/// Constrains each word to K bits using a lookup table.
///
/// Panics
///
/// Panics if `num_words` is greater than F::NUM_BITS / K, i.e. there are
/// more words than can fit in a field element.
#[allow(clippy::type_complexity)]
fn lookup_range_check(
&self,
layouter: impl Layouter<F>,
words: CellValue<F>,
num_words: usize,
) -> Result<Vec<CellValue<F>>, Error>;
}
#[derive(Clone, Debug)]
pub struct LookupRangeCheckChip<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize> {
config: LookupRangeCheckConfig<K>,
_marker: PhantomData<F>,
}
impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize> Chip<F>
for LookupRangeCheckChip<F, K>
{
type Config = LookupRangeCheckConfig<K>;
type Loaded = ();
fn config(&self) -> &Self::Config {
&self.config
}
fn loaded(&self) -> &Self::Loaded {
&()
}
}
#[derive(Debug, Clone)]
pub struct LookupRangeCheckConfig<const K: usize> {
q_lookup: Selector,
q_decompose: Selector,
pub struct LookupRangeCheckConfig<F: FieldExt + PrimeFieldBits, const K: usize> {
q_lookup: Column<Fixed>, // This is passed in.
running_sum: Column<Advice>,
table_idx: Column<Fixed>,
perm: Permutation,
_marker: PhantomData<F>,
}
impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize> LookupRangeCheckChip<F, K> {
impl<F: FieldExt + PrimeFieldBits, const K: usize> LookupRangeCheckConfig<F, K> {
pub fn configure(
meta: &mut ConstraintSystem<F>,
q_lookup: Column<Fixed>,
running_sum: Column<Advice>,
table_idx: Column<Fixed>,
perm: Permutation,
) -> LookupRangeCheckConfig<K> {
let q_lookup = meta.selector();
let q_decompose = meta.selector();
) -> Self {
let config = LookupRangeCheckConfig {
q_lookup,
q_decompose,
running_sum,
table_idx,
perm,
_marker: PhantomData,
};
meta.lookup(|meta| {
let q_lookup = meta.query_selector(config.q_lookup);
let q_lookup = meta.query_fixed(config.q_lookup, Rotation::cur());
let z_cur = meta.query_advice(config.running_sum, Rotation::cur());
let z_next = meta.query_advice(config.running_sum, Rotation::next());
// z_i = 2^{K}⋅z_{i + 1} + a_i
@ -98,7 +54,6 @@ impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize> LookupRangeC
}
pub fn load(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
let config = self.config().clone();
layouter.assign_region(
|| "table_idx",
|mut gate| {
@ -106,7 +61,7 @@ impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize> LookupRangeC
for index in 0..(1 << K) {
gate.assign_fixed(
|| "table_idx",
config.table_idx,
self.table_idx,
index,
|| Ok(F::from_u64(index as u64)),
)?;
@ -116,26 +71,10 @@ impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize> LookupRangeC
)
}
pub fn construct(config: LookupRangeCheckConfig<K>) -> Self {
LookupRangeCheckChip {
config,
_marker: PhantomData,
}
}
}
impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize> UtilitiesInstructions<F>
for LookupRangeCheckChip<F, K>
{
type Var = CellValue<F>;
}
impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize>
LookupRangeCheckInstructions<F, K> for LookupRangeCheckChip<F, K>
{
fn lookup_range_check(
&self,
mut layouter: impl Layouter<F>,
region: &mut Region<'_, F>,
offset: usize,
words: CellValue<F>,
num_words: usize,
) -> Result<Vec<CellValue<F>>, Error> {
@ -143,8 +82,6 @@ impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize>
assert!(num_words <= F::NUM_BITS as usize / K);
let num_bits = num_words * K;
let config = self.config().clone();
// Take first num_bits bits of `words`.
let bits = words.value().map(|words| {
words
@ -167,69 +104,59 @@ impl<F: FieldExt + PrimeFieldBits + PrimeFieldBits, const K: usize>
vec![None; num_words]
};
layouter.assign_region(
|| format!("{}-bit decomposition", K),
|mut region| {
let offset = 0;
// Copy `words` and initialize running sum `z_0 = words` to decompose it.
let z_0 = copy(
region,
|| "copy words",
self.running_sum,
offset,
&words,
&self.perm,
)?;
// Copy `words` and initialize running sum `z_0 = words` to decompose it.
let z_0 = copy(
&mut region,
|| "copy words",
config.running_sum,
offset,
&words,
&config.perm,
let mut zs = vec![z_0];
// Assign cumulative sum such that
// z_i = 2^{K}⋅z_{i + 1} + a_i
// => z_{i + 1} = (z_i - a_i) / (2^K)
//
// For `words` = a_0 + 2^10 a_1 + ... + 2^{120} a_{12}}, initialize z_0 = `words`.
// If `words` fits in 130 bits, we end up with z_{13} = 0.
let mut z = z_0;
let inv_2_pow_k = F::from_u64(1u64 << K).invert().unwrap();
for (idx, word) in bits.iter().enumerate() {
let word = word
.clone()
.map(|word| F::from_u64(lebs2ip_k(&word) as u64));
// z_next = (z_cur - m_cur) / 2^K
z = {
let z_val = z
.value()
.zip(word)
.map(|(z, word)| (z - word) * inv_2_pow_k);
// Assign z_next
let z_cell = region.assign_advice(
|| format!("z_{:?}", idx + 1),
self.running_sum,
offset + idx + 1,
|| z_val.ok_or(Error::SynthesisError),
)?;
let mut zs = vec![z_0];
CellValue::new(z_cell, z_val)
};
zs.push(z);
}
// Assign cumulative sum such that
// z_i = 2^{K}⋅z_{i + 1} + a_i
// => z_{i + 1} = (z_i - a_i) / (2^K)
//
// For `words` = a_0 + 2^10 a_1 + ... + 2^{120} a_{12}}, initialize z_0 = `words`.
// If `words` fits in 130 bits, we end up with z_{13} = 0.
let mut z = z_0;
let inv_2_pow_k = F::from_u64(1u64 << K).invert().unwrap();
for (idx, word) in bits.iter().enumerate() {
let word = word
.clone()
.map(|word| F::from_u64(lebs2ip_k(&word) as u64));
// Enable selector to activate lookup.
config.q_lookup.enable(&mut region, offset + idx)?;
// z_next = (z_cur - m_cur) / 2^K
z = {
let z_val = z
.value()
.zip(word)
.map(|(z, word)| (z - word) * inv_2_pow_k);
// Assign z_next
let z_cell = region.assign_advice(
|| format!("z_{:?}", idx + 1),
config.running_sum,
offset + idx + 1,
|| z_val.ok_or(Error::SynthesisError),
)?;
CellValue::new(z_cell, z_val)
};
zs.push(z);
}
Ok(zs)
},
)
Ok(zs)
}
}
#[cfg(test)]
mod tests {
use super::super::{UtilitiesInstructions, Var};
use super::{LookupRangeCheckChip, LookupRangeCheckConfig, LookupRangeCheckInstructions};
use super::super::{CellValue, UtilitiesInstructions, Var};
use super::LookupRangeCheckConfig;
use crate::primitives::sinsemilla::{lebs2ip_k, K};
use ff::PrimeFieldBits;
use halo2::{
@ -247,16 +174,27 @@ mod tests {
_marker: PhantomData<F>,
}
impl<F: FieldExt + PrimeFieldBits> UtilitiesInstructions<F> for MyCircuit<F> {
type Var = CellValue<F>;
}
impl<F: FieldExt + PrimeFieldBits> Circuit<F> for MyCircuit<F> {
type Config = LookupRangeCheckConfig<K>;
type Config = LookupRangeCheckConfig<F, K>;
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let running_sum = meta.advice_column();
let table_idx = meta.fixed_column();
let q_lookup = meta.fixed_column();
let perm = meta.permutation(&[running_sum.into()]);
LookupRangeCheckChip::<F, K>::configure(meta, running_sum, table_idx, perm)
LookupRangeCheckConfig::<F, K>::configure(
meta,
q_lookup,
running_sum,
table_idx,
perm,
)
}
fn synthesize(
@ -266,57 +204,43 @@ mod tests {
) -> Result<(), Error> {
let mut layouter = SingleChipLayouter::new(cs)?;
let chip = LookupRangeCheckChip::<F, K>::construct(config.clone());
// Load table_idx
chip.load(&mut layouter)?;
config.load(&mut layouter)?;
let num_words = 6;
let words_and_expected_final_zs = [
(F::from_u64((1 << (num_words * K)) - 1), F::zero()), // a word that is within num_words * K bits long
(F::from_u64(1 << (num_words * K)), F::one()), // a word that is just over num_words * K bits long
];
// Test a word that is within num_words * K bits long.
{
let words = F::from_u64((1 << (num_words * K)) - 1);
let expected_zs = expected_zs::<F, K>(words, num_words);
for (words, expected_final_z) in words_and_expected_final_zs.iter() {
let expected_zs = expected_zs::<F, K>(*words, num_words);
// Load the value to be decomposed into the circuit.
let words = chip.load_private(
let words = self.load_private(
layouter.namespace(|| "words"),
config.running_sum,
Some(words),
)?;
let zs = chip.lookup_range_check(
layouter.namespace(|| "range check"),
words,
num_words,
Some(*words),
)?;
assert_eq!(expected_zs[expected_zs.len() - 1], F::zero());
let zs = layouter.assign_region(
|| "word within range",
|mut region| {
for idx in 0..num_words {
// Assign fixed column to activate lookup.
region.assign_fixed(
|| format!("lookup on row {}", idx),
config.q_lookup,
idx,
|| Ok(F::one()),
)?;
}
for (expected_z, z) in expected_zs.into_iter().zip(zs.iter()) {
if let Some(z) = z.value() {
assert_eq!(expected_z, z);
}
}
}
// Test a word that is just over num_words * K bits long.
{
let words = F::from_u64(1 << (num_words * K));
let expected_zs = expected_zs::<F, K>(words, num_words);
// Load the value to be decomposed into the circuit.
let words = chip.load_private(
layouter.namespace(|| "words"),
config.running_sum,
Some(words),
)?;
let zs = chip.lookup_range_check(
layouter.namespace(|| "range check"),
words,
num_words,
config.lookup_range_check(&mut region, 0, words, num_words)
},
)?;
assert_eq!(expected_zs[expected_zs.len() - 1], F::one());
assert_eq!(expected_zs[expected_zs.len() - 1], *expected_final_z);
for (expected_z, z) in expected_zs.into_iter().zip(zs.iter()) {
if let Some(z) = z.value() {