From 4d64237cb38cbccfd920054e71e0f71178ba0ba8 Mon Sep 17 00:00:00 2001 From: Janmajaya Mall Date: Tue, 19 Jul 2022 00:00:33 +0530 Subject: [PATCH] zk/gadget/less_than: Fixed less_than chip + tests pass --- src/zk/gadget/less_than.rs | 278 +++++++++++++++------------- src/zk/gadget/mod.rs | 2 +- src/zk/gadget/native_range_check.rs | 8 +- 3 files changed, 154 insertions(+), 134 deletions(-) diff --git a/src/zk/gadget/less_than.rs b/src/zk/gadget/less_than.rs index aadf16964..35ebd88b6 100644 --- a/src/zk/gadget/less_than.rs +++ b/src/zk/gadget/less_than.rs @@ -1,46 +1,42 @@ -use std::marker::PhantomData; - -use group::ff::PrimeFieldBits; +use halo2_gadgets::utilities::FieldValue; use halo2_proofs::{ arithmetic::FieldExt, circuit::{AssignedCell, Chip, Layouter, Region, Value}, plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector, TableColumn}, poly::Rotation, }; +use pasta_curves::pallas; -use super::range_check::{RangeCheckChip, RangeCheckConfig}; +use super::native_range_check::{NativeRangeCheckChip, NativeRangeCheckConfig}; #[derive(Clone, Debug)] -pub struct LessThanConfig { +pub struct LessThanConfig< + const WINDOW_SIZE: usize, + const NUM_OF_BITS: usize, + const NUM_OF_WINDOWS: usize, +> { pub s_lt: Selector, pub a: Column, pub b: Column, pub a_offset: Column, - - pub range_a_config: RangeCheckConfig, - pub range_a_offset_config: RangeCheckConfig, + pub range_a_config: NativeRangeCheckConfig, + pub range_a_offset_config: NativeRangeCheckConfig, pub k_values_table: TableColumn, } #[derive(Clone, Debug)] pub struct LessThanChip< - F: FieldExt + PrimeFieldBits, - const NUM_OF_BITS: usize, const WINDOW_SIZE: usize, + const NUM_OF_BITS: usize, const NUM_OF_WINDOWS: usize, > { - config: LessThanConfig, - _marker: PhantomData, + config: LessThanConfig, } -impl< - F: FieldExt + PrimeFieldBits, - const NUM_OF_BITS: usize, - const WINDOW_SIZE: usize, - const NUM_OF_WINDOWS: usize, - > Chip for LessThanChip +impl + Chip for LessThanChip { - type Config = LessThanConfig; + type Config = LessThanConfig; type Loaded = (); fn config(&self) -> &Self::Config { @@ -52,24 +48,20 @@ impl< } } -impl< - F: FieldExt + PrimeFieldBits, - const NUM_OF_BITS: usize, - const WINDOW_SIZE: usize, - const NUM_OF_WINDOWS: usize, - > LessThanChip +impl + LessThanChip { - pub fn construct(config: LessThanConfig) -> Self { - Self { config, _marker: PhantomData } + pub fn construct(config: LessThanConfig) -> Self { + Self { config } } pub fn configure( - meta: &mut ConstraintSystem, + meta: &mut ConstraintSystem, a: Column, b: Column, a_offset: Column, k_values_table: TableColumn, - ) -> LessThanConfig { + ) -> LessThanConfig { let s_lt = meta.selector(); meta.enable_equality(a); @@ -77,9 +69,20 @@ impl< meta.enable_equality(a_offset); // configure range check for `a` and `offset` - let range_a_config = RangeCheckChip::::configure(meta, k_values_table); + let z = meta.advice_column(); + let range_a_config = + NativeRangeCheckChip::::configure( + meta, + z, + k_values_table, + ); + let z = meta.advice_column(); let range_a_offset_config = - RangeCheckChip::::configure(meta, k_values_table); + NativeRangeCheckChip::::configure( + meta, + z, + k_values_table, + ); let config = LessThanConfig { s_lt, @@ -96,7 +99,7 @@ impl< let a = meta.query_advice(config.a, Rotation::cur()); let b = meta.query_advice(config.b, Rotation::cur()); let a_offset = meta.query_advice(config.a_offset, Rotation::cur()); - let two_pow_m = Expression::Constant(F::from(1 << NUM_OF_BITS)); + let two_pow_m = Expression::Constant(pallas::Base::from_u128(1 << NUM_OF_BITS)); // a_offset - 2^m + b - a = 0 vec![s_lt * (a_offset - two_pow_m + b - a)] }); @@ -106,14 +109,14 @@ impl< pub fn witness_less_than( &self, - layouter: &mut impl Layouter, - a: Value, - b: Value, + mut layouter: impl Layouter, + a: Value, + b: Value, offset: usize, ) -> Result<(), Error> { let (a, _, a_offset) = layouter.assign_region( - || "less than", - |mut region: Region<'_, F>| { + || "a less than b", + |mut region: Region<'_, pallas::Base>| { let a = region.assign_advice(|| "a", self.config.a, offset, || a)?; let b = region.assign_advice(|| "b", self.config.b, offset, || b)?; let a_offset = self.less_than(region, a.clone(), b.clone(), offset)?; @@ -121,21 +124,21 @@ impl< }, )?; - self.less_than_range_check(layouter, a, a_offset, offset)?; + self.less_than_range_check(layouter, a, a_offset)?; Ok(()) } pub fn copy_less_than( &self, - layouter: &mut impl Layouter, - a: AssignedCell, - b: AssignedCell, + mut layouter: impl Layouter, + a: AssignedCell, + b: AssignedCell, offset: usize, ) -> Result<(), Error> { let (a, _, a_offset) = layouter.assign_region( - || "less than", - |mut region: Region<'_, F>| { + || "a less than b", + |mut region: Region<'_, pallas::Base>| { let a = a.copy_advice(|| "a", &mut region, self.config.a, offset)?; let b = b.copy_advice(|| "b", &mut region, self.config.b, offset)?; let a_offset = self.less_than(region, a.clone(), b.clone(), offset)?; @@ -143,50 +146,48 @@ impl< }, )?; - self.less_than_range_check(layouter, a, a_offset, offset)?; + self.less_than_range_check(layouter, a, a_offset)?; Ok(()) } pub fn less_than_range_check( &self, - layouter: &mut impl Layouter, - a: AssignedCell, - a_offset: AssignedCell, - offset: usize, + mut layouter: impl Layouter, + a: AssignedCell, + a_offset: AssignedCell, ) -> Result<(), Error> { let range_a_chip = - RangeCheckChip::::construct(self.config.range_a_config.clone()); + NativeRangeCheckChip::::construct( + self.config.range_a_config.clone(), + ); let range_a_offset_chip = - RangeCheckChip::::construct(self.config.range_a_offset_config.clone()); + NativeRangeCheckChip::::construct( + self.config.range_a_offset_config.clone(), + ); - range_a_chip.copy_range_check(layouter, a, offset, NUM_OF_BITS, NUM_OF_WINDOWS)?; - range_a_offset_chip.copy_range_check( - layouter, - a_offset, - offset, - NUM_OF_BITS, - NUM_OF_WINDOWS, - )?; + range_a_chip.copy_range_check(layouter.namespace(|| "a copy_range_check"), a)?; + range_a_offset_chip + .copy_range_check(layouter.namespace(|| "a_offset copy_range_check"), a_offset)?; Ok(()) } pub fn less_than( &self, - mut region: Region<'_, F>, - a: AssignedCell, - b: AssignedCell, + mut region: Region<'_, pallas::Base>, + a: AssignedCell, + b: AssignedCell, offset: usize, - ) -> Result, Error> { + ) -> Result, Error> { // enable `less_than` selector self.config.s_lt.enable(&mut region, offset)?; // assign `a + offset` - let two_pow_m = F::from(1 << NUM_OF_BITS); + let two_pow_m = pallas::Base::from_u128(1 << 64); let a_offset = a.value().zip(b.value()).map(|(a, b)| *a + (two_pow_m - b)); let a_offset = - region.assign_advice(|| "offset", self.config.a_offset, offset, || a_offset)?; + region.assign_advice(|| "a_offset", self.config.a_offset, offset, || a_offset)?; Ok(a_offset) } @@ -195,105 +196,120 @@ impl< #[cfg(test)] mod tests { use super::*; - use group::ff::PrimeFieldBits; use halo2_proofs::{ - arithmetic::FieldExt, circuit::{floor_planner, Value}, dev::{CircuitLayout, MockProver}, plonk::Circuit, }; use pasta_curves::pallas; - struct LessThanCircuit< - F: FieldExt + PrimeFieldBits, - const WINDOW_SIZE: usize, - const NUM_OF_BITS: usize, - const NUM_OF_WINDOWS: usize, - > { - a: Value, - b: Value, - } + macro_rules! test_circuit { + ($window_size:expr, $num_bits:expr, $num_windows:expr) => { + #[derive(Default)] + struct LessThanCircuit { + a: Value, + b: Value, + } - impl< - F: FieldExt + PrimeFieldBits, - const WINDOW_SIZE: usize, - const NUM_OF_BITS: usize, - const NUM_OF_WINDOWS: usize, - > Circuit for LessThanCircuit - { - type Config = LessThanConfig; - type FloorPlanner = floor_planner::V1; + impl Circuit for LessThanCircuit { + type Config = + (LessThanConfig<$window_size, $num_bits, $num_windows>, Column); + type FloorPlanner = floor_planner::V1; - fn without_witnesses(&self) -> Self { - Self { a: Value::unknown(), b: Value::unknown() } - } + fn without_witnesses(&self) -> Self { + Self { a: Value::unknown(), b: Value::unknown() } + } - fn configure(meta: &mut ConstraintSystem) -> Self::Config { - let a = meta.advice_column(); - let b = meta.advice_column(); - let a_offset = meta.advice_column(); + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let w = meta.advice_column(); + meta.enable_equality(w); - let k_values_table = meta.lookup_table_column(); + let a = meta.advice_column(); + let b = meta.advice_column(); + let a_offset = meta.advice_column(); - let constants = meta.fixed_column(); - meta.enable_constant(constants); + let k_values_table = meta.lookup_table_column(); - LessThanChip::::configure( - meta, - a, - b, - a_offset, - k_values_table, - ) - } + let constants = meta.fixed_column(); + meta.enable_constant(constants); - fn synthesize( - &self, - config: Self::Config, - mut layouter: impl Layouter, - ) -> Result<(), Error> { - let less_than_chip = - LessThanChip::::construct( - config.clone(), - ); + ( + LessThanChip::<$window_size, $num_bits, $num_windows>::configure( + meta, + a, + b, + a_offset, + k_values_table, + ), + w, + ) + } - RangeCheckChip::::load_k_table(&mut layouter, config.k_values_table)?; + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let less_than_chip = + LessThanChip::<$window_size, $num_bits, $num_windows>::construct( + config.0.clone(), + ); - less_than_chip.witness_less_than(&mut layouter, self.a, self.b, 0)?; + NativeRangeCheckChip::<$window_size, $num_bits, $num_windows>::load_k_table( + &mut layouter, + config.0.k_values_table, + )?; - Ok(()) - } + less_than_chip.witness_less_than(layouter, self.a, self.b, 0)?; + + Ok(()) + } + } + }; } #[test] fn less_than() { - let k = 15; + test_circuit!(3, 64, 22); + let k = 8; - let valid_a_vals = vec![pallas::Base::from(15)]; - let valid_b_vals = vec![pallas::Base::from(11)]; + let valid_a_vals = vec![pallas::Base::from(13)]; + let valid_b_vals = vec![pallas::Base::from(15)]; - // use plotters::prelude::*; - // let circuit = LessThanCircuit:: { - // a: Value::known(pallas::Base::zero()), - // b: Value::known(pallas::Base::one()), - // }; - // let root = BitMapBackend::new("target/lessthan_circuit_layout.png", (3840, 2160)) - // .into_drawing_area(); - // CircuitLayout::default().render(k, &circuit, &root).unwrap(); + let invalid_a_vals = vec![pallas::Base::from(14)]; + let invalid_b_vals = vec![pallas::Base::from(11)]; + + use plotters::prelude::*; + let circuit = LessThanCircuit { + a: Value::known(pallas::Base::zero()), + b: Value::known(pallas::Base::one()), + }; + let root = BitMapBackend::new("target/lessthan_circuit_layout.png", (3840, 2160)) + .into_drawing_area(); + CircuitLayout::default().render(k, &circuit, &root).unwrap(); for i in 0..valid_a_vals.len() { let a = valid_a_vals[i]; let b = valid_b_vals[i]; - println!("{:?} < {:?}", a, b); + println!("64 bit (valid) {:?} < {:?} check", a, b); - let circuit = LessThanCircuit:: { - a: Value::known(a), - b: Value::known(b), - }; + let circuit = LessThanCircuit { a: Value::known(a), b: Value::known(b) }; let prover = MockProver::run(k, &circuit, vec![]).unwrap(); prover.assert_satisfied(); } + + for i in 0..invalid_a_vals.len() { + let a = invalid_a_vals[i]; + let b = invalid_b_vals[i]; + + println!("64 bit (invalid) {:?} < {:?} check", a, b); + + let circuit = LessThanCircuit { a: Value::known(a), b: Value::known(b) }; + + let prover = MockProver::run(k, &circuit, vec![]).unwrap(); + assert!(prover.verify().is_err()) + } } } diff --git a/src/zk/gadget/mod.rs b/src/zk/gadget/mod.rs index 91d73ead6..39a776a1c 100644 --- a/src/zk/gadget/mod.rs +++ b/src/zk/gadget/mod.rs @@ -14,4 +14,4 @@ pub mod even_bits; pub mod cmp; // Less than gadget -//pub mod less_than; +pub mod less_than; diff --git a/src/zk/gadget/native_range_check.rs b/src/zk/gadget/native_range_check.rs index a2b6da48c..f58a817c5 100644 --- a/src/zk/gadget/native_range_check.rs +++ b/src/zk/gadget/native_range_check.rs @@ -75,7 +75,6 @@ impl /// `k_values_table` should be reused across different chips /// which is why we don't limit it to a specific instance. pub fn load_k_table( - &self, layouter: &mut impl Layouter, k_values_table: TableColumn, ) -> Result<(), plonk::Error> { @@ -135,6 +134,7 @@ impl let two_pow_k_inverse = Value::known(pallas::Base::from(1 << WINDOW_SIZE as u64).invert().unwrap()); + for (i, chunk) in decomposed_chunks.iter().enumerate() { let z_next = { let z_curr = z.value().copied(); @@ -223,6 +223,7 @@ mod tests { meta.enable_equality(w); let z = meta.advice_column(); let table_column = meta.lookup_table_column(); + let constants = meta.fixed_column(); meta.enable_constant(constants); ( @@ -244,7 +245,10 @@ mod tests { NativeRangeCheckChip::<$window_size, $num_bits, $num_windows>::construct( config.0.clone(), ); - rangecheck_chip.load_k_table(&mut layouter, config.0.k_values_table)?; + NativeRangeCheckChip::<$window_size, $num_bits, $num_windows>::load_k_table( + &mut layouter, + config.0.k_values_table, + )?; let a = assign_free_advice(layouter.namespace(|| "load a"), config.1, self.a)?; rangecheck_chip