diff --git a/src/zk/gadget/range_check.rs b/src/zk/gadget/range_check.rs index 41eb8deed..9a4757c4e 100644 --- a/src/zk/gadget/range_check.rs +++ b/src/zk/gadget/range_check.rs @@ -15,6 +15,7 @@ pub struct RangeCheckConfig { pub k_values_table: TableColumn, } +#[derive(Clone, Debug)] pub struct RangeCheckChip { config: RangeCheckConfig, _marker: PhantomData, @@ -36,10 +37,14 @@ impl Chip } impl RangeCheckChip { + pub fn construct(config: RangeCheckConfig) -> Self { + Self { config, _marker: PhantomData } + } + pub fn configure( meta: &mut ConstraintSystem, k_values_table: TableColumn, - ) -> >::Config { + ) -> RangeCheckConfig { let z = meta.advice_column(); let s_rc = meta.complex_selector(); @@ -80,60 +85,68 @@ impl RangeCheckChip, - element: AssignedCell, + layouter: &mut impl Layouter, + value: Value, + offset: usize, + num_of_bits: usize, + num_of_windows: usize, + ) -> Result<(), Error> { + layouter.assign_region( + || "name", + |mut region: Region<'_, F>| { + let z_0 = region.assign_advice(|| "z_0", self.config.z, offset, || value)?; + self.decompose(region, z_0, offset, num_of_bits, num_of_windows)?; + Ok(()) + }, + ) + } + + pub fn decompose( + &self, + mut region: Region<'_, F>, + z_0: AssignedCell, + offset: usize, num_of_bits: usize, num_of_windows: usize, ) -> Result<(), Error> { assert!(WINDOW_SIZE * num_of_windows < num_of_bits + WINDOW_SIZE); - layouter.assign_region( - || "name", - |mut region: Region<'_, F>| { - // enable selectors - for index in 0..num_of_windows { - self.config.s_rc.enable(&mut region, index); - } + // enable selectors + for index in 0..num_of_windows { + self.config.s_rc.enable(&mut region, index + offset)?; + } - // copy element to z_0 - let z_0 = element.copy_advice(|| "z_0", &mut region, self.config.z, 0)?; + let mut z_values: Vec> = vec![z_0.clone()]; + let mut z = z_0.clone(); + let decomposed_chunks = z_0 + .value() + .map(|val| decompose_value::(val, num_of_bits)) + .transpose_vec(num_of_windows); - let mut z_values: Vec> = vec![z_0.clone()]; - let mut z = z_0.clone(); - let decomposed_chunks = z_0 - .value() - .map(|val| decompose_value::(val, num_of_bits)) - .transpose_vec(num_of_windows); + let two_pow_k_inverse = Value::known(F::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(); + let chunk_value = + chunk.map(|c| F::from(c.iter().fold(0, |acc, c| (acc << 1) + *c as u64))); + // z_next = (z_curr - k_i) / 2^K + let z_next = (z_curr - chunk_value) * two_pow_k_inverse; + region.assign_advice( + || format!("z_{}", i + offset + 1), + self.config.z, + i + offset, + || z_next, + )? + }; + z_values.push(z_next.clone()); + z = z_next.clone(); + } - let two_pow_k_inverse = - Value::known(F::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(); - let chunk_value = chunk - .map(|c| F::from(c.iter().fold(0, |acc, c| (acc << 1) + *c as u64))); - // z_next = (z_curr - k_i) / 2^K - let z_next = (z_curr - chunk_value) * two_pow_k_inverse; - region.assign_advice( - || format!("z_{}", i + 1), - self.config.z, - i + 1, - || z_next, - )? - }; - z_values.push(z_next.clone()); - z = z_next.clone(); - } + assert!(z_values.len() == num_of_windows + 1); - assert!(z_values.len() == num_of_windows + 1); - - region.constrain_constant(z_values.last().unwrap().cell(), F::zero())?; - - Ok(()) - }, - ); + region.constrain_constant(z_values.last().unwrap().cell(), F::zero())?; Ok(()) } @@ -162,3 +175,68 @@ pub fn decompose_value( }) .collect() } + +#[cfg(test)] +mod tests { + use super::*; + use group::ff::PrimeFieldBits; + use halo2_proofs::{ + arithmetic::FieldExt, + circuit::{SimpleFloorPlanner, Value}, + dev::MockProver, + plonk::Circuit, + }; + use pasta_curves::pallas; + + struct MyCircuit< + F: FieldExt + PrimeFieldBits, + const WINDOW_SIZE: usize, + const NUM_OF_BITS: usize, + const NUM_OF_WINDOWS: usize, + > { + value: Value, + } + + impl< + F: FieldExt + PrimeFieldBits, + const WINDOW_SIZE: usize, + const NUM_OF_BITS: usize, + const NUM_OF_WINDOWS: usize, + > Circuit for MyCircuit + { + type Config = RangeCheckConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn without_witnesses(&self) -> Self { + Self { value: Value::unknown() } + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let table_column = meta.lookup_table_column(); + RangeCheckChip::::configure(meta, table_column) + } + + fn synthesize( + &self, + config: Self::Config, + layouter: impl Layouter, + ) -> Result<(), Error> { + let chip = RangeCheckChip::::construct(config.clone()); + + // construct `WINDOW_SIZE` lookup table + RangeCheckChip::::load_k_table(&mut layouter, config.k_values_table); + + chip.witness_range_check(&mut layouter, self.value, 0, NUM_OF_BITS, NUM_OF_WINDOWS); + + Ok(()) + } + } + + #[test] + fn test_bit() { + let value = pallas::Base::from(rand::random::()); + let circuit = MyCircuit:: { value: Value::known(value) }; + let prover = MockProver::run(8, &circuit, vec![]).unwrap(); + assert_ne!(prover.verify(), Ok(())); + } +}