From 34bae7dc028a3f1458ca646baa9edc147d3fc7ea Mon Sep 17 00:00:00 2001 From: parazyd Date: Mon, 18 Jul 2022 22:48:44 +0200 Subject: [PATCH] zk/gadget: Clean up. --- src/zk/gadget/even_bits.rs | 246 --------------------------- src/zk/gadget/greater_than.rs | 214 ----------------------- src/zk/gadget/{cmp.rs => is_zero.rs} | 0 src/zk/gadget/less_than.rs | 5 +- src/zk/gadget/mod.rs | 14 +- src/zk/gadget/native_range_check.rs | 3 +- src/zk/vm.rs | 31 +--- 7 files changed, 8 insertions(+), 505 deletions(-) delete mode 100644 src/zk/gadget/even_bits.rs delete mode 100644 src/zk/gadget/greater_than.rs rename src/zk/gadget/{cmp.rs => is_zero.rs} (100%) diff --git a/src/zk/gadget/even_bits.rs b/src/zk/gadget/even_bits.rs deleted file mode 100644 index 52267e411..000000000 --- a/src/zk/gadget/even_bits.rs +++ /dev/null @@ -1,246 +0,0 @@ -use std::{marker::PhantomData, ops::Deref}; - -use halo2_proofs::{ - arithmetic::FieldExt, - circuit::{AssignedCell, Chip, Layouter, Region, Value}, - plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector, TableColumn}, - poly::Rotation, -}; - -/// Chip state is stored in a config struct. This is generated by the -/// chip during configuration, and then stored inside the chip -#[derive(Clone, Debug)] -pub struct EvenBitsConfig { - advice: [Column; 2], - even_bits: TableColumn, - - s_decompose: Selector, -} - -impl EvenBitsConfig { - pub fn load_private( - &self, - mut layouter: impl Layouter, - value: Value, - ) -> Result, Error> { - layouter.assign_region( - || "load private", - |mut region| region.assign_advice(|| "private input", self.advice[0], 0, || value), - ) - } -} - -#[derive(Clone, Debug)] -pub struct EvenBitsChip { - config: EvenBitsConfig, - _marker: PhantomData, -} - -impl Chip for EvenBitsChip { - type Config = EvenBitsConfig; - type Loaded = (); - - fn config(&self) -> &Self::Config { - &self.config - } - - fn loaded(&self) -> &Self::Loaded { - &() - } -} - -impl EvenBitsChip { - pub fn construct(config: >::Config) -> Self { - Self { config, _marker: PhantomData } - } - - pub fn configure(meta: &mut ConstraintSystem) -> >::Config { - let advice = [meta.advice_column(), meta.advice_column()]; - for column in &advice { - meta.enable_equality(*column); - } - - let s_decompose = meta.complex_selector(); - let even_bits = meta.lookup_table_column(); - - meta.create_gate("decompose", |meta| { - let lhs = meta.query_advice(advice[0], Rotation::cur()); - let rhs = meta.query_advice(advice[1], Rotation::cur()); - let out = meta.query_advice(advice[0], Rotation::next()); - let s_decompose = meta.query_selector(s_decompose); - - // Finally, we return the polynomial expressions that constrain this gate. - // For our multiplication gate, we only need a single polynomial constraint. - // - // The polynomial expressions returned from `create_gate` will be - // constrained by the proving system to equal zero. - vec![s_decompose * (lhs + Expression::Constant(F::from(2)) * rhs - out)] - }); - - let _ = meta.lookup(|meta| { - let lookup = meta.query_selector(s_decompose); - let a = meta.query_advice(advice[0], Rotation::cur()); - - vec![(lookup * a, even_bits)] - }); - - let _ = meta.lookup(|meta| { - let lookup = meta.query_selector(s_decompose); - let b = meta.query_advice(advice[1], Rotation::cur()); - - vec![(lookup * b, even_bits)] - }); - - EvenBitsConfig { advice, even_bits, s_decompose } - } - - // Allocates all even bits in a table for the word size WORD_BITS. - // `2^(WORD_BITS/2)` rows of the constraint system - pub fn alloc_table(&self, layouter: &mut impl Layouter) -> Result<(), Error> { - layouter.assign_table( - || "even bits table", - |mut table| { - for i in 0..2usize.pow(WORD_BITS / 2) { - table.assign_cell( - || format!("even_bits row {}", i), - self.config.even_bits, - i, - || Value::known(F::from(even_bits_at(i) as u64)), - )?; - } - Ok(()) - }, - ) - } -} - -fn even_bits_at(mut i: usize) -> usize { - let mut r = 0; - let mut c = 0; - - while i != 0 { - let lower_bit = i % 2; - r += lower_bit * 4usize.pow(c); - i >>= 1; - c += 1; - } - - r -} - -/// A newtype of a field element containing only bits that were in the -/// even position of the decomposed element. -/// All odd bits will be zero. -#[derive(Clone, Copy, Debug)] -pub struct EvenBits(pub W); - -impl Deref for EvenBits { - type Target = W; - - fn deref(&self) -> &Self::Target { - &self.0 - } -} - -/// A newtype of a field element containing only bits thet were in the -/// odd position of the decomposed element. -/// All odd bits will be right shifted by 1 into even positions. -/// All odd bits will be zero. -#[derive(Clone, Copy, Debug)] -pub struct OddBits(pub W); - -impl Deref for OddBits { - type Target = W; - - fn deref(&self) -> &Self::Target { - &self.0 - } -} - -pub trait EvenBitsLookup: Chip { - type Word; - - #[allow(clippy::type_complexity)] - fn decompose( - &self, - layouter: impl Layouter, - c: Self::Word, - ) -> Result<(EvenBits, OddBits), Error>; -} - -impl EvenBitsLookup for EvenBitsChip { - type Word = AssignedCell; - - fn decompose( - &self, - mut layouter: impl Layouter, - c: Self::Word, - ) -> Result<(EvenBits, OddBits), Error> { - let config = self.config(); - - layouter.assign_region( - || "decompose", - |mut region: Region<'_, F>| { - config.s_decompose.enable(&mut region, 0)?; - - let o_eo = c.value().cloned().map(decompose); - let e_cell = region - .assign_advice(|| "even bits", config.advice[0], 0, || o_eo.map(|eo| *eo.0)) - .map(EvenBits)?; - - let o_cell = region - .assign_advice(|| "odd bits", config.advice[1], 0, || o_eo.map(|eo| *eo.1)) - .map(OddBits)?; - - c.copy_advice(|| "out", &mut region, config.advice[0], 1)?; - Ok((e_cell, o_cell)) - }, - ) - } -} - -fn decompose(word: F) -> (EvenBits, OddBits) { - assert!(word <= F::from_u128(u128::MAX)); - - let mut even_only = word.to_repr(); - even_only.as_mut().iter_mut().for_each(|bits| { - *bits &= 0b01010101; - }); - - let mut odd_only = word.to_repr(); - odd_only.as_mut().iter_mut().for_each(|bits| { - *bits &= 0b10101010; - }); - - let even_only = EvenBits(F::from_repr(even_only).unwrap()); - let odd_only = F::from_repr(odd_only).unwrap(); - let odds_in_even = OddBits(F::from_u128(odd_only.get_lower_128() >> 1)); - (even_only, odds_in_even) -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn even_bits_at_test() { - assert_eq!(0b0, even_bits_at(0)); - assert_eq!(0b1, even_bits_at(1)); - assert_eq!(0b100, even_bits_at(2)); - assert_eq!(0b101, even_bits_at(3)); - } - - #[test] - fn decompose_even_odd_test() { - use pasta_curves::pallas; - let odds = 0xAAAA; - let evens = 0x5555; - let (e, o) = decompose(pallas::Base::from_u128(odds)); - assert_eq!(e.get_lower_128(), 0); - assert_eq!(o.get_lower_128(), odds >> 1); - let (e, o) = decompose(pallas::Base::from_u128(evens)); - assert_eq!(e.get_lower_128(), evens); - assert_eq!(o.get_lower_128(), 0); - } -} -// diff --git a/src/zk/gadget/greater_than.rs b/src/zk/gadget/greater_than.rs deleted file mode 100644 index 32478c723..000000000 --- a/src/zk/gadget/greater_than.rs +++ /dev/null @@ -1,214 +0,0 @@ -use std::marker::PhantomData; - -use halo2_proofs::{ - arithmetic::FieldExt, - circuit::{AssignedCell, Chip, Layouter, Region, Value}, - plonk::{Advice, Column, ConstraintSystem, Error, Expression, Instance, Selector}, - poly::Rotation, -}; - -use pasta_curves::pallas; - -#[derive(Clone, Debug)] -pub struct GreaterThanConfig { - pub advice: [Column; 2], - pub instance: Column, - s_gt: Selector, -} - -pub struct GreaterThanChip { - config: GreaterThanConfig, - _marker: PhantomData, -} - -impl Chip for GreaterThanChip { - type Config = GreaterThanConfig; - type Loaded = (); - - fn config(&self) -> &Self::Config { - &self.config - } - - fn loaded(&self) -> &Self::Loaded { - &() - } -} - -impl GreaterThanChip { - pub fn construct(config: >::Config) -> Self { - Self { config, _marker: PhantomData } - } - - /* - pub fn configure(meta: &mut ConstraintSystem) -> >::Config { - //let constant = meta.fixed_column(); - //meta.enable_constant(constant); - - let advice = [meta.advice_column(), meta.advice_column()]; - - for column in &advice { - meta.enable_equality(*column); - } - - let s_gt = meta.selector(); - - meta.create_gate("greater than", |meta| { - let lhs = meta.query_advice(advice[0], Rotation::cur()); - let rhs = meta.query_advice(advice[1], Rotation::cur()); - - // This value is `lhs - rhs` if `lhs !> rhs` and `2^W - (lhs - rhs)` if `lhs > rhs` - let helper = meta.query_advice(advice[0], Rotation::next()); - - let is_greater = meta.query_advice(advice[1], Rotation::next()); - let s_gt = meta.query_selector(s_gt); - - vec![ - s_gt * (lhs - rhs + helper - - Expression::Constant(F::from(2_u64.pow(WORD_BITS))) * is_greater), - ] - }); - - GreaterThanConfig { advice, s_gt } - } - - pub fn configure(meta: &mut ConstraintSystem) -> >::Config { - let advice = [meta.advice_column(), meta.advice_column()]; - - - let s_gt = meta.selector(); - - meta.create_gate("greater than", |meta| { - let lhs = meta.query_advice(advice[0], Rotation::cur()); - let rhs = meta.query_advice(advice[1], Rotation::cur()); - - // This value is `lhs - rhs` if `lhs !> rhs` and `2^W - (lhs - rhs)` if `lhs > rhs` - let helper = meta.query_advice(advice[0], Rotation::next()); - - let is_greater = meta.query_advice(advice[1], Rotation::next()); - let s_gt = meta.query_selector(s_gt); - - vec![ - s_gt * (lhs - rhs + helper - - Expression::Constant(F::from(2_u64.pow(WORD_BITS))) * is_greater), - ] - }); - - GreaterThanConfig { advice, s_gt } - } - */ - pub fn configure( - meta: &mut ConstraintSystem, - advice: [Column; 2], - instance: Column, - ) -> >::Config { - for column in &advice { - meta.enable_equality(*column); - } - - let s_gt = meta.selector(); - - meta.create_gate("greater than", |meta| { - let lhs = meta.query_advice(advice[0], Rotation::cur()); - let rhs = meta.query_advice(advice[1], Rotation::cur()); - - // This value is `lhs - rhs` if `lhs !> rhs` and `2^W - (lhs - rhs)` if `lhs > rhs` - let helper = meta.query_advice(advice[0], Rotation::next()); - - let is_greater = meta.query_advice(advice[1], Rotation::next()); - let s_gt = meta.query_selector(s_gt); - - vec![ - s_gt * (lhs - rhs + helper - - Expression::Constant(F::from(2_u64.pow(WORD_BITS))) * is_greater), - ] - }); - - GreaterThanConfig { advice, instance, s_gt } - } -} - -pub trait GreaterThanInstruction: Chip { - type Word; - - fn greater_than( - &self, - layouter: impl Layouter, - a: Self::Word, - b: Self::Word, - ) -> Result<(Self::Word, Self::Word), Error>; -} - -#[derive(Clone, Debug)] -pub struct Word(pub AssignedCell); - -impl From> for Word { - fn from(cell: AssignedCell) -> Self { - Self(cell) - } -} - -impl GreaterThanInstruction - for GreaterThanChip -{ - type Word = Word; - - fn greater_than( - &self, - mut layouter: impl Layouter, - a: Self::Word, - b: Self::Word, - ) -> Result<(Self::Word, Self::Word), Error> { - let config = self.config(); - - layouter.assign_region( - || "greater than", - |mut region: Region<'_, pallas::Base>| { - config.s_gt.enable(&mut region, 0)?; - - a.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?; - b.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?; - - let helper_cell = region - .assign_advice( - || "max minus diff", - config.advice[0], - 1, - || { - let is_greater = a.0.value().inner().unwrap().get_lower_128() > - b.0.value().get_lower_128(); - a.0.value().and_then(|a| { - b.0.value().map(|b| { - let x = *a - *b; - - (if is_greater { - pallas::Base::from(2_u64.pow(WORD_BITS)) - } else { - pallas::Base::zero() - }) - x - }) - }) - }, - ) - .map(Word)?; - - let is_greater_cell = region - .assign_advice( - || "is greater", - config.advice[1], - 1, - || { - let is_greater = a.0.value().inner().unwrap().get_lower_128() > - b.0.value().get_lower_128(); - Value::known(if is_greater { - pallas::Base::one() - } else { - pallas::Base::zero() - }) - }, - ) - .map(Word)?; - Ok((helper_cell, is_greater_cell)) - }, - ) - } -} diff --git a/src/zk/gadget/cmp.rs b/src/zk/gadget/is_zero.rs similarity index 100% rename from src/zk/gadget/cmp.rs rename to src/zk/gadget/is_zero.rs diff --git a/src/zk/gadget/less_than.rs b/src/zk/gadget/less_than.rs index b66c45b0b..67a858b70 100644 --- a/src/zk/gadget/less_than.rs +++ b/src/zk/gadget/less_than.rs @@ -1,11 +1,10 @@ -use halo2_gadgets::utilities::FieldValue; use halo2_proofs::{ arithmetic::FieldExt, circuit::{AssignedCell, Chip, Layouter, Region, Value}, + pasta::pallas, plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector, TableColumn}, poly::Rotation, }; -use pasta_curves::pallas; use super::native_range_check::{NativeRangeCheckChip, NativeRangeCheckConfig}; @@ -200,9 +199,9 @@ mod tests { use halo2_proofs::{ circuit::{floor_planner, Value}, dev::{CircuitLayout, MockProver}, + pasta::pallas, plonk::Circuit, }; - use pasta_curves::pallas; macro_rules! test_circuit { ($window_size:expr, $num_bits:expr, $num_windows:expr) => { diff --git a/src/zk/gadget/mod.rs b/src/zk/gadget/mod.rs index 39a776a1c..72537afd0 100644 --- a/src/zk/gadget/mod.rs +++ b/src/zk/gadget/mod.rs @@ -4,14 +4,8 @@ pub mod arithmetic; /// Field-native range check gadget; pub mod native_range_check; -/// Even-bits lookup table -pub mod even_bits; - -// Greater than comparison gadget; -//pub mod greater_than; - -/// Comparison gadget -pub mod cmp; - -// Less than gadget +// Field-native less than comparison gadget pub mod less_than; + +/// is_zero comparison gadget +pub mod is_zero; diff --git a/src/zk/gadget/native_range_check.rs b/src/zk/gadget/native_range_check.rs index 0ba2ab80e..ba2c06668 100644 --- a/src/zk/gadget/native_range_check.rs +++ b/src/zk/gadget/native_range_check.rs @@ -130,8 +130,7 @@ impl let mut z_values: Vec> = vec![z_0.clone()]; let mut z = z_0.clone(); - let decomposed_chunks = - z_0.value().map(|val| Self::decompose_value(val)).transpose_vec(NUM_WINDOWS); + let decomposed_chunks = z_0.value().map(Self::decompose_value).transpose_vec(NUM_WINDOWS); let two_pow_k_inverse = Value::known(pallas::Base::from(1 << WINDOW_SIZE as u64).invert().unwrap()); diff --git a/src/zk/vm.rs b/src/zk/vm.rs index 3e3a0cbe2..276d52463 100644 --- a/src/zk/vm.rs +++ b/src/zk/vm.rs @@ -24,10 +24,7 @@ use halo2_proofs::{ use log::debug; use pasta_curves::{group::Curve, pallas, Fp}; -use super::gadget::{ - arithmetic::{ArithChip, ArithConfig, ArithInstruction}, - even_bits::{EvenBitsChip, EvenBitsConfig}, -}; +use super::gadget::arithmetic::{ArithChip, ArithConfig, ArithInstruction}; use super::assign_free_advice; pub use super::vm_stack::{StackVar, Witness}; @@ -51,8 +48,6 @@ pub struct VmConfig { _sinsemilla_cfg2: SinsemillaConfig, poseidon_config: PoseidonConfig, arith_config: ArithConfig, - evenbits_config: EvenBitsConfig, - //greaterthan_config: GreaterThanConfig, } impl VmConfig { @@ -93,14 +88,6 @@ impl VmConfig { fn arithmetic_chip(&self) -> ArithChip { ArithChip::construct(self.arith_config.clone()) } - - fn evenbits_chip(&self) -> EvenBitsChip { - EvenBitsChip::construct(self.evenbits_config.clone()) - } - - //fn greaterthan_chip(&self) -> GreaterThanChip { - // GreaterThanChip::construct(self.greaterthan_config.clone()) - // } } #[derive(Clone, Default)] @@ -200,13 +187,6 @@ impl Circuit for ZkCircuit { // Configuration for the Arithmetic chip let arith_config = ArithChip::configure(meta, advices[7], advices[8], advices[6]); - // Configuration for the EvenBits chip - let evenbits_config = EvenBitsChip::::configure(meta); - - // Configuration for the GreaterThan chip - //let greaterthan_config = - // GreaterThanChip::::configure(meta, [advices[8], advices[9]], primary); - // Configuration for a Sinsemilla hash instantiation and a // Merkle hash instantiation using this Sinsemilla instance. // Since the Sinsemilla config uses only 5 advice columns, @@ -247,8 +227,6 @@ impl Circuit for ZkCircuit { _sinsemilla_cfg2, poseidon_config, arith_config, - evenbits_config, - //greaterthan_config, } } @@ -274,13 +252,6 @@ impl Circuit for ZkCircuit { // Construct the Arithmetic chip. let arith_chip = config.arithmetic_chip(); - // Construct the EvenBits chip. - let eb_chip = config.evenbits_chip(); - eb_chip.alloc_table(&mut layouter.namespace(|| "alloc table"))?; - - // Construct the GreaterThan chip. - //let gt_chip = config.greaterthan_chip(); - // This constant one is used for short multiplication let one = assign_free_advice( layouter.namespace(|| "Load constant one"),