diff --git a/halo2_frontend/src/dev/cost.rs b/halo2_frontend/src/dev/cost.rs index 9e5f2a1c7..68d883e18 100644 --- a/halo2_frontend/src/dev/cost.rs +++ b/halo2_frontend/src/dev/cost.rs @@ -563,467 +563,4 @@ mod tests { let proof_size = cost.proof_size(1); assert_eq!(usize::from(proof_size), 608); } - - #[test] - fn test_circuit_cost_from_complex_circuit() { - use crate::{ - circuit::{AssignedCell, Layouter, Region}, - plonk::{Error as ErrorFront, Expression, FirstPhase, SecondPhase}, - }; - - #[derive(Clone)] - struct MyCircuitConfig { - // A gate that uses selector, fixed, advice, has addition, multiplication and rotation - // s_gate[0] * (a[0] + b[0] * c[0] * d[0] - a[1]) - s_gate: Selector, - a: Column, - b: Column, - c: Column, - d: Column, - - // Copy constraints between columns (a, b) and (a, d) - - // A dynamic lookup: s_lookup * [1, a[0], b[0]] in s_ltable * [1, d[0], c[0]] - s_lookup: Column, - s_ltable: Column, - - // A shuffle: s_shufle * [1, a[0]] shuffle_of s_stable * [1, b[0]] - s_shuffle: Column, - s_stable: Column, - - // A FirstPhase challenge and SecondPhase column. We define the following gates: - // s_rlc * (a[0] + challenge * b[0] - e[0]) - // s_rlc * (c[0] + challenge * d[0] - e[0]) - s_rlc: Selector, - e: Column, - challenge: Challenge, - - // Instance with a gate: s_instance * (a[0] - instance[0]) - s_instance: Selector, - instance: Column, - } - - impl MyCircuitConfig { - #[allow(clippy::type_complexity)] - fn assign_gate>( - &self, - region: &mut Region<'_, F>, - offset: &mut usize, - a_assigned: Option>, - abcd: [u64; 4], - ) -> Result<(AssignedCell, [AssignedCell; 4]), ErrorFront> { - let [a, b, c, d] = abcd; - self.s_gate.enable(region, *offset)?; - let a_assigned = if let Some(a_assigned) = a_assigned { - a_assigned - } else { - region.assign_advice(|| "", self.a, *offset, || Value::known(F::from(a)))? - }; - let a = a_assigned.value(); - let [b, c, d] = [b, c, d].map(|v| Value::known(F::from(v))); - let b_assigned = region.assign_advice(|| "", self.b, *offset, || b)?; - let c_assigned = region.assign_advice(|| "", self.c, *offset, || c)?; - let d_assigned = region.assign_fixed(|| "", self.d, *offset, || d)?; - *offset += 1; - // let res = a + b * c * d; - let res = a - .zip(b.zip(c.zip(d))) - .map(|(a, (b, (c, d)))| *a + b * c * d); - let res_assigned = region.assign_advice(|| "", self.a, *offset, || res)?; - Ok(( - res_assigned, - [a_assigned, b_assigned, c_assigned, d_assigned], - )) - } - } - - #[allow(dead_code)] - #[derive(Clone)] - struct MyCircuit { - k: u32, - input: u64, - _marker: std::marker::PhantomData, - } - - impl, const WIDTH_FACTOR: usize> MyCircuit { - fn new(k: u32, input: u64) -> Self { - Self { - k, - input, - _marker: std::marker::PhantomData {}, - } - } - - fn configure_single(meta: &mut ConstraintSystem, id: usize) -> MyCircuitConfig { - let s_gate = meta.selector(); - let a = meta.advice_column(); - let b = meta.advice_column(); - let c = meta.advice_column(); - let d = meta.fixed_column(); - - meta.enable_equality(a); - meta.enable_equality(b); - meta.enable_equality(d); - - let s_lookup = meta.fixed_column(); - let s_ltable = meta.fixed_column(); - - let s_shuffle = meta.fixed_column(); - let s_stable = meta.fixed_column(); - - let s_rlc = meta.selector(); - let e = meta.advice_column_in(SecondPhase); - let challenge = meta.challenge_usable_after(FirstPhase); - - let s_instance = meta.selector(); - let instance = meta.instance_column(); - meta.enable_equality(instance); - - let one = Expression::Constant(F::ONE); - - meta.create_gate(format!("gate_a.{id}"), |meta| { - let s_gate = meta.query_selector(s_gate); - let b = meta.query_advice(b, Rotation::cur()); - let a1 = meta.query_advice(a, Rotation::next()); - let a0 = meta.query_advice(a, Rotation::cur()); - let c = meta.query_advice(c, Rotation::cur()); - let d = meta.query_fixed(d, Rotation::cur()); - - vec![s_gate * (a0 + b * c * d - a1)] - }); - - meta.lookup_any(format!("lookup.{id}"), |meta| { - let s_lookup = meta.query_fixed(s_lookup, Rotation::cur()); - let s_ltable = meta.query_fixed(s_ltable, Rotation::cur()); - let a = meta.query_advice(a, Rotation::cur()); - let b = meta.query_advice(b, Rotation::cur()); - let c = meta.query_advice(c, Rotation::cur()); - let d = meta.query_fixed(d, Rotation::cur()); - let lhs = [one.clone(), a, b].map(|c| c * s_lookup.clone()); - let rhs = [one.clone(), d, c].map(|c| c * s_ltable.clone()); - lhs.into_iter().zip(rhs).collect() - }); - - meta.shuffle(format!("shuffle.{id}"), |meta| { - let s_shuffle = meta.query_fixed(s_shuffle, Rotation::cur()); - let s_stable = meta.query_fixed(s_stable, Rotation::cur()); - let a = meta.query_advice(a, Rotation::cur()); - let b = meta.query_advice(b, Rotation::cur()); - let lhs = [one.clone(), a].map(|c| c * s_shuffle.clone()); - let rhs = [one.clone(), b].map(|c| c * s_stable.clone()); - lhs.into_iter().zip(rhs).collect() - }); - - meta.create_gate(format!("gate_rlc.{id}"), |meta| { - let s_rlc = meta.query_selector(s_rlc); - let a = meta.query_advice(a, Rotation::cur()); - let b = meta.query_advice(b, Rotation::cur()); - let c = meta.query_advice(c, Rotation::cur()); - let d = meta.query_fixed(d, Rotation::cur()); - let e = meta.query_advice(e, Rotation::cur()); - let challenge = meta.query_challenge(challenge); - - vec![ - s_rlc.clone() * (a + challenge.clone() * b - e.clone()), - s_rlc * (c + challenge * d - e), - ] - }); - - MyCircuitConfig { - s_gate, - a, - b, - c, - d, - s_lookup, - s_ltable, - s_rlc, - e, - challenge, - s_shuffle, - s_stable, - s_instance, - instance, - } - } - - fn synthesize_unit( - &self, - config: &MyCircuitConfig, - layouter: &mut impl Layouter, - id: usize, - unit_id: usize, - ) -> Result<(usize, Vec>), ErrorFront> { - let challenge = layouter.get_challenge(config.challenge); - let (rows, instance_copy) = layouter.assign_region( - || format!("unit.{id}-{unit_id}"), - |mut region| { - // Column annotations - region.name_column(|| format!("a.{id}"), config.a); - region.name_column(|| format!("b.{id}"), config.b); - region.name_column(|| format!("c.{id}"), config.c); - region.name_column(|| format!("d.{id}"), config.d); - region.name_column(|| format!("e.{id}"), config.e); - region.name_column(|| format!("instance.{id}"), config.instance); - region.name_column(|| format!("s_lookup.{id}"), config.s_lookup); - region.name_column(|| format!("s_ltable.{id}"), config.s_ltable); - region.name_column(|| format!("s_shuffle.{id}"), config.s_shuffle); - region.name_column(|| format!("s_stable.{id}"), config.s_stable); - - let mut offset = 0; - let mut instance_copy = Vec::new(); - // First "a" value comes from instance - config.s_instance.enable(&mut region, offset).unwrap(); - let res = region - .assign_advice_from_instance( - || "", - config.instance, - 0, - config.a, - offset, - ) - .unwrap(); - // Enable the gate on a few consecutive rows with rotations - let (res, _) = config - .assign_gate(&mut region, &mut offset, Some(res), [0, 3, 4, 1]) - .unwrap(); - instance_copy.push(res.clone()); - let (res, _) = config - .assign_gate(&mut region, &mut offset, Some(res), [0, 6, 7, 1]) - .unwrap(); - instance_copy.push(res.clone()); - let (res, _) = config - .assign_gate(&mut region, &mut offset, Some(res), [0, 8, 9, 1]) - .unwrap(); - instance_copy.push(res.clone()); - let (res, _) = config - .assign_gate( - &mut region, - &mut offset, - Some(res), - [0, 0xffffffff, 0xdeadbeef, 1], - ) - .unwrap(); - let _ = config - .assign_gate( - &mut region, - &mut offset, - Some(res), - [0, 0xabad1d3a, 0x12345678, 0x42424242], - ) - .unwrap(); - offset += 1; - - // Enable the gate on non-consecutive rows with advice-advice copy constraints enabled - let (_, abcd1) = config - .assign_gate(&mut region, &mut offset, None, [5, 2, 1, 1]) - .unwrap(); - offset += 1; - let (_, abcd2) = config - .assign_gate(&mut region, &mut offset, None, [2, 3, 1, 1]) - .unwrap(); - offset += 1; - let (_, abcd3) = config - .assign_gate(&mut region, &mut offset, None, [4, 2, 1, 1]) - .unwrap(); - offset += 1; - region - .constrain_equal(abcd1[1].cell(), abcd2[0].cell()) - .unwrap(); - region - .constrain_equal(abcd2[0].cell(), abcd3[1].cell()) - .unwrap(); - instance_copy.push(abcd1[1].clone()); - instance_copy.push(abcd2[0].clone()); - - // Enable the gate on non-consecutive rows with advice-fixed copy constraints enabled - let (_, abcd1) = config - .assign_gate(&mut region, &mut offset, None, [5, 9, 1, 9]) - .unwrap(); - offset += 1; - let (_, abcd2) = config - .assign_gate(&mut region, &mut offset, None, [2, 9, 1, 1]) - .unwrap(); - offset += 1; - let (_, abcd3) = config - .assign_gate(&mut region, &mut offset, None, [9, 2, 1, 1]) - .unwrap(); - offset += 1; - region - .constrain_equal(abcd1[1].cell(), abcd1[3].cell()) - .unwrap(); - region - .constrain_equal(abcd2[1].cell(), abcd1[3].cell()) - .unwrap(); - region - .constrain_equal(abcd3[0].cell(), abcd1[3].cell()) - .unwrap(); - - // Enable a dynamic lookup (powers of two) - let table: Vec<_> = - (0u64..=10).map(|exp| (exp, 2u64.pow(exp as u32))).collect(); - let lookups = [(2, 4), (2, 4), (10, 1024), (0, 1), (2, 4)]; - for (table_row, lookup_row) in table - .iter() - .zip(lookups.iter().chain(std::iter::repeat(&(0, 1)))) - { - region - .assign_fixed( - || "", - config.s_lookup, - offset, - || Value::known(F::ONE), - ) - .unwrap(); - region - .assign_fixed( - || "", - config.s_ltable, - offset, - || Value::known(F::ONE), - ) - .unwrap(); - let lookup_row0 = Value::known(F::from(lookup_row.0)); - let lookup_row1 = Value::known(F::from(lookup_row.1)); - region - .assign_advice(|| "", config.a, offset, || lookup_row0) - .unwrap(); - region - .assign_advice(|| "", config.b, offset, || lookup_row1) - .unwrap(); - let table_row0 = Value::known(F::from(table_row.0)); - let table_row1 = Value::known(F::from(table_row.1)); - region - .assign_fixed(|| "", config.d, offset, || table_row0) - .unwrap(); - region - .assign_advice(|| "", config.c, offset, || table_row1) - .unwrap(); - offset += 1; - } - - // Enable RLC gate 3 times - for abcd in [[3, 5, 3, 5], [8, 9, 8, 9], [111, 222, 111, 222]] { - config.s_rlc.enable(&mut region, offset)?; - let (_, _) = config - .assign_gate(&mut region, &mut offset, None, abcd) - .unwrap(); - let rlc = challenge.map(|ch| { - let [a, b, ..] = abcd; - F::from(a) + ch * F::from(b) - }); - region - .assign_advice(|| "", config.e, offset - 1, || rlc) - .unwrap(); - offset += 1; - } - - // Enable a dynamic shuffle (sequence from 0 to 15) - let table: Vec<_> = (0u64..16).collect(); - let shuffle = [0u64, 2, 4, 6, 8, 10, 12, 14, 1, 3, 5, 7, 9, 11, 13, 15]; - assert_eq!(table.len(), shuffle.len()); - - for (table_row, shuffle_row) in table.iter().zip(shuffle.iter()) { - region - .assign_fixed( - || "", - config.s_shuffle, - offset, - || Value::known(F::ONE), - ) - .unwrap(); - region - .assign_fixed( - || "", - config.s_stable, - offset, - || Value::known(F::ONE), - ) - .unwrap(); - let shuffle_row0 = Value::known(F::from(*shuffle_row)); - region - .assign_advice(|| "", config.a, offset, || shuffle_row0) - .unwrap(); - let table_row0 = Value::known(F::from(*table_row)); - region - .assign_advice(|| "", config.b, offset, || table_row0) - .unwrap(); - offset += 1; - } - - Ok((offset, instance_copy)) - }, - )?; - - Ok((rows, instance_copy)) - } - } - - impl, const WIDTH_FACTOR: usize> Circuit for MyCircuit { - type Config = Vec; - type FloorPlanner = SimpleFloorPlanner; - #[cfg(feature = "circuit-params")] - type Params = (); - - fn without_witnesses(&self) -> Self { - self.clone() - } - - fn configure(meta: &mut ConstraintSystem) -> Vec { - assert!(WIDTH_FACTOR > 0); - (0..WIDTH_FACTOR) - .map(|id| Self::configure_single(meta, id)) - .collect() - } - - fn synthesize( - &self, - config: Vec, - mut layouter: impl Layouter, - ) -> Result<(), ErrorFront> { - // - 2 queries from first gate - // - 3 for permutation argument - // - 1 for multipoen - // - 1 for the last row of grand product poly to check that the product result is 1 - // - 1 for off-by-one errors - let unusable_rows = 2 + 3 + 1 + 1 + 1; - let max_rows = 2usize.pow(self.k) - unusable_rows; - for (id, config) in config.iter().enumerate() { - let mut total_rows = 0; - let mut unit_id = 0; - loop { - let (rows, instance_copy) = self - .synthesize_unit(config, &mut layouter, id, unit_id) - .unwrap(); - if total_rows == 0 { - for (i, instance) in instance_copy.iter().enumerate() { - layouter.constrain_instance( - instance.cell(), - config.instance, - 1 + i, - )?; - } - } - total_rows += rows; - if total_rows + rows > max_rows { - break; - } - unit_id += 1; - } - assert!(total_rows <= max_rows); - } - Ok(()) - } - } - - const K: u32 = 6; - let my_circuit = MyCircuit::::new(K, 42); - let cost = CircuitCost::>::measure(K, &my_circuit); - - let marginal_proof_size = cost.marginal_proof_size(); - assert_eq!(usize::from(marginal_proof_size), 1376); - - let proof_size = cost.proof_size(1); - assert_eq!(usize::from(proof_size), 3008); - } }