From 50fb46ab14f80d5b3d5de7f78bea9ff15a1954b3 Mon Sep 17 00:00:00 2001 From: "Eduard S." Date: Thu, 28 Dec 2023 18:18:47 +0100 Subject: [PATCH] Make progress on testing fe-be split --- halo2_proofs/src/plonk/circuit.rs | 84 ++++- halo2_proofs/src/plonk/keygen.rs | 14 +- halo2_proofs/src/poly.rs | 25 +- halo2_proofs/tests/frontend_backend_split.rs | 372 ++++++++++++++----- 4 files changed, 401 insertions(+), 94 deletions(-) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index caa70bb029..3a786dc37c 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -3,7 +3,7 @@ use crate::circuit::layouter::SyncDeps; use crate::dev::metadata; use crate::{ circuit::{Layouter, Region, Value}, - poly::{LagrangeCoeff, Polynomial, Rotation}, + poly::{batch_invert_assigned, LagrangeCoeff, Polynomial, Rotation}, }; use core::cmp::max; use core::ops::{Add, Mul}; @@ -1677,6 +1677,88 @@ pub struct ConstraintSystemV2Backend { // pub(crate) minimum_degree: Option, } +/// TODO: Document. Frontend function +pub fn compile_circuit>( + k: u32, + circuit: &ConcreteCircuit, + compress_selectors: bool, +) -> Result, Error> { + let n = 2usize.pow(k); + let mut cs = ConstraintSystem::default(); + #[cfg(feature = "circuit-params")] + let config = ConcreteCircuit::configure_with_params(&mut cs, circuit.params()); + #[cfg(not(feature = "circuit-params"))] + let config = ConcreteCircuit::configure(&mut cs); + let cs = cs; + + if n < cs.minimum_rows() { + return Err(Error::not_enough_rows_available(k)); + } + + let mut assembly = crate::plonk::keygen::Assembly { + k, + fixed: vec![Polynomial::new_empty(n, F::ZERO.into()); cs.num_fixed_columns], + permutation: permutation::keygen::Assembly::new(n, &cs.permutation), + selectors: vec![vec![false; n as usize]; cs.num_selectors], + usable_rows: 0..n as usize - (cs.blinding_factors() + 1), + _marker: std::marker::PhantomData, + }; + + // Synthesize the circuit to obtain URS + ConcreteCircuit::FloorPlanner::synthesize( + &mut assembly, + circuit, + config, + cs.constants.clone(), + )?; + + let mut fixed = batch_invert_assigned(assembly.fixed); + let (cs, selector_polys) = if compress_selectors { + cs.compress_selectors(assembly.selectors.clone()) + } else { + // After this, the ConstraintSystem should not have any selectors: `verify` does not need them, and `keygen_pk` regenerates `cs` from scratch anyways. + let selectors = std::mem::take(&mut assembly.selectors); + cs.directly_convert_selectors_to_fixed(selectors) + }; + fixed.extend( + selector_polys + .into_iter() + .map(|poly| Polynomial::new_lagrange_from_vec(poly)), + ); + + let cs2 = ConstraintSystemV2Backend { + num_fixed_columns: cs.num_fixed_columns, + num_advice_columns: cs.num_advice_columns, + num_instance_columns: cs.num_instance_columns, + num_challenges: cs.num_challenges, + unblinded_advice_columns: cs.unblinded_advice_columns, + advice_column_phase: cs.advice_column_phase.iter().map(|p| p.0).collect(), + challenge_phase: cs.challenge_phase.iter().map(|p| p.0).collect(), + gates: cs + .gates + .iter() + .map(|g| GateV2Backend { + name: g.name.clone(), + constraint_names: g.constraint_names.clone(), + polys: g.polys.clone(), + }) + .collect(), + permutation: cs.permutation, + lookups: cs.lookups, + shuffles: cs.shuffles, + general_column_annotations: cs.general_column_annotations, + }; + let preprocessing = PreprocessingV2 { + permutation: assembly.permutation, + fixed, + }; + + Ok(CompiledCircuitV2 { + cs: cs2, + preprocessing, + }) +} + impl ConstraintSystemV2Backend { /// Compute the degree of the constraint system (the maximum degree of all /// constraints). diff --git a/halo2_proofs/src/plonk/keygen.rs b/halo2_proofs/src/plonk/keygen.rs index b8891ce26e..a3ea376c6b 100644 --- a/halo2_proofs/src/plonk/keygen.rs +++ b/halo2_proofs/src/plonk/keygen.rs @@ -51,14 +51,14 @@ where /// Assembly to be used in circuit synthesis. #[derive(Debug)] -struct Assembly { - k: u32, - fixed: Vec, LagrangeCoeff>>, - permutation: permutation::keygen::Assembly, - selectors: Vec>, +pub(crate) struct Assembly { + pub(crate) k: u32, + pub(crate) fixed: Vec, LagrangeCoeff>>, + pub(crate) permutation: permutation::keygen::Assembly, + pub(crate) selectors: Vec>, // A range of available rows for assignment and copies. - usable_rows: Range, - _marker: std::marker::PhantomData, + pub(crate) usable_rows: Range, + pub(crate) _marker: std::marker::PhantomData, } impl Assignment for Assembly { diff --git a/halo2_proofs/src/poly.rs b/halo2_proofs/src/poly.rs index c52e982f19..68b33f0d47 100644 --- a/halo2_proofs/src/poly.rs +++ b/halo2_proofs/src/poly.rs @@ -65,8 +65,29 @@ impl Basis for ExtendedLagrangeCoeff {} /// basis. #[derive(Clone, Debug)] pub struct Polynomial { - values: Vec, - _marker: PhantomData, + pub(crate) values: Vec, + pub(crate) _marker: PhantomData, +} + +impl Polynomial { + pub(crate) fn new_empty(size: usize, zero: F) -> Self { + Polynomial { + values: vec![zero; size], + _marker: PhantomData, + } + } +} + +impl Polynomial { + /// Obtains a polynomial in Lagrange form when given a vector of Lagrange + /// coefficients of size `n`; panics if the provided vector is the wrong + /// length. + pub(crate) fn new_lagrange_from_vec(values: Vec) -> Polynomial { + Polynomial { + values, + _marker: PhantomData, + } + } } impl Index for Polynomial { diff --git a/halo2_proofs/tests/frontend_backend_split.rs b/halo2_proofs/tests/frontend_backend_split.rs index 8ef9030989..dfd7d9223a 100644 --- a/halo2_proofs/tests/frontend_backend_split.rs +++ b/halo2_proofs/tests/frontend_backend_split.rs @@ -7,9 +7,10 @@ use halo2_proofs::arithmetic::Field; use halo2_proofs::circuit::{AssignedCell, Cell, Layouter, Region, SimpleFloorPlanner, Value}; use halo2_proofs::dev::MockProver; use halo2_proofs::plonk::{ - create_proof as create_plonk_proof, keygen_pk, keygen_vk, verify_proof as verify_plonk_proof, - Advice, Assigned, Circuit, Column, ConstraintSystem, Error, Expression, Fixed, Instance, - ProvingKey, Selector, TableColumn, VerifyingKey, + compile_circuit, create_proof, keygen_pk, keygen_pk_v2, keygen_vk, keygen_vk_v2, verify_proof, + Advice, Assigned, Challenge, Circuit, Column, CompiledCircuitV2, ConstraintSystem, + ConstraintSystemV2Backend, Error, Expression, FirstPhase, Fixed, Instance, ProvingKey, + SecondPhase, Selector, TableColumn, VerifyingKey, }; use halo2_proofs::poly::commitment::{CommitmentScheme, ParamsProver, Prover, Verifier}; use halo2_proofs::poly::Rotation; @@ -41,28 +42,91 @@ struct MyCircuitConfig { s_shuffle: Column, s_stable: Column, - // Instance + // 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 { + fn assign_gate>( + &self, + region: &mut Region<'_, F>, + offset: &mut usize, + a_assigned: Option>, + abcd: [u64; 4], + ) -> Result<(AssignedCell, [AssignedCell; 4]), Error> { + 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], + )) + } +} + #[derive(Clone)] -struct MyCircuit { +struct MyCircuit { + k: u32, + input: u64, _marker: std::marker::PhantomData, } -impl> Circuit for MyCircuit { - type Config = MyCircuitConfig; - type FloorPlanner = SimpleFloorPlanner; - #[cfg(feature = "circuit-params")] - type Params = (); - - fn without_witnesses(&self) -> Self { +impl, const WIDTH_FACTOR: usize> MyCircuit { + fn new(k: u32, input: u64) -> Self { Self { + k, + input, _marker: std::marker::PhantomData {}, } } - fn configure(meta: &mut ConstraintSystem) -> MyCircuitConfig { + fn instance(&self) -> Vec { + let mut instance = Vec::new(); + let res = F::from(self.input); + instance.push(res); + let (b, c, d) = (3, 4, 1); + let res = res + F::from(b) * F::from(c) * F::from(d); + instance.push(res); + let (b, c, d) = (6, 7, 1); + let res = res + F::from(b) * F::from(c) * F::from(d); + instance.push(res); + let (b, c, d) = (8, 9, 1); + let res = res + F::from(b) * F::from(c) * F::from(d); + instance.push(res); + instance.push(F::from(2)); + instance.push(F::from(2)); + instance + } + + fn instances(&self) -> Vec> { + let instance = self.instance(); + (0..WIDTH_FACTOR).map(|_| instance.clone()).collect() + } + + fn configure_single(meta: &mut ConstraintSystem) -> MyCircuitConfig { let s_gate = meta.selector(); let a = meta.advice_column(); let b = meta.advice_column(); @@ -79,6 +143,11 @@ impl> Circuit for MyCircuit { 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); @@ -117,6 +186,21 @@ impl> Circuit for MyCircuit { lhs.into_iter().zip(rhs.into_iter()).collect() }); + meta.create_gate("gate_rlc", |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, @@ -125,65 +209,53 @@ impl> Circuit for MyCircuit { d, s_lookup, s_ltable, + s_rlc, + e, + challenge, s_shuffle, s_stable, + s_instance, instance, } } - fn synthesize( + fn synthesize_unit( &self, - config: MyCircuitConfig, - mut layouter: impl Layouter, - ) -> Result<(), Error> { - let assign_gate = |region: &mut Region<'_, F>, - offset: &mut usize, - a_assigned: Option>, - abcd: [u64; 4]| - -> Result<(AssignedCell, [AssignedCell; 4]), Error> { - let [a, b, c, d] = abcd; - config.s_gate.enable(region, *offset); - let a_assigned = if let Some(a_assigned) = a_assigned { - a_assigned - } else { - region.assign_advice(|| "", config.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(b))); - let b_assigned = region.assign_advice(|| "", config.b, *offset, || b)?; - let c_assigned = region.assign_advice(|| "", config.c, *offset, || c)?; - let d_assigned = region.assign_fixed(|| "", config.d, *offset, || d)?; - *offset += 1; - let res = a - .zip(b.zip(c.zip(d))) - .map(|(a, (b, (c, d)))| *a + b * c * d); - // let res = a + b * c * d; - let res_assigned = region.assign_advice(|| "", config.a, *offset, || res)?; - Ok(( - res_assigned, - [a_assigned, b_assigned, c_assigned, d_assigned], - )) - }; - - let instances = layouter.assign_region( - || "single", + config: &MyCircuitConfig, + layouter: &mut impl Layouter, + ) -> Result<(usize, Vec>), Error> { + let challenge = layouter.get_challenge(config.challenge); + let (rows, instance_copy) = layouter.assign_region( + || "unit", |mut region| { let mut offset = 0; - let mut instances = Vec::new(); + let mut instance_copy = Vec::new(); + // First "a" value comes from instance + config.s_instance.enable(&mut region, offset); + let res = region.assign_advice_from_instance( + || "", + config.instance, + 0, + config.a, + offset, + )?; // Enable the gate on a few consecutive rows with rotations - let (res, _) = assign_gate(&mut region, &mut offset, None, [2, 3, 4, 1])?; - instances.push(res.clone()); - let (res, _) = assign_gate(&mut region, &mut offset, Some(res), [0, 6, 7, 1])?; - instances.push(res.clone()); - let (res, _) = assign_gate(&mut region, &mut offset, Some(res), [0, 8, 9, 1])?; - instances.push(res.clone()); - let (res, _) = assign_gate( + let (res, _) = + config.assign_gate(&mut region, &mut offset, Some(res), [0, 3, 4, 1])?; + instance_copy.push(res.clone()); + let (res, _) = + config.assign_gate(&mut region, &mut offset, Some(res), [0, 6, 7, 1])?; + instance_copy.push(res.clone()); + let (res, _) = + config.assign_gate(&mut region, &mut offset, Some(res), [0, 8, 9, 1])?; + instance_copy.push(res.clone()); + let (res, _) = config.assign_gate( &mut region, &mut offset, Some(res), [0, 0xffffffff, 0xdeadbeef, 1], )?; - let _ = assign_gate( + let _ = config.assign_gate( &mut region, &mut offset, Some(res), @@ -192,23 +264,29 @@ impl> Circuit for MyCircuit { offset += 1; // Enable the gate on non-consecutive rows with advice-advice copy constraints enabled - let (_, abcd1) = assign_gate(&mut region, &mut offset, None, [5, 2, 1, 1])?; + let (_, abcd1) = + config.assign_gate(&mut region, &mut offset, None, [5, 2, 1, 1])?; offset += 1; - let (_, abcd2) = assign_gate(&mut region, &mut offset, None, [2, 3, 1, 1])?; + let (_, abcd2) = + config.assign_gate(&mut region, &mut offset, None, [2, 3, 1, 1])?; offset += 1; - let (_, abcd3) = assign_gate(&mut region, &mut offset, None, [4, 2, 1, 1])?; + let (_, abcd3) = + config.assign_gate(&mut region, &mut offset, None, [4, 2, 1, 1])?; offset += 1; region.constrain_equal(abcd1[1].cell(), abcd2[0].cell())?; region.constrain_equal(abcd2[0].cell(), abcd3[1].cell())?; - instances.push(abcd1[1].clone()); - instances.push(abcd2[0].clone()); + 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) = assign_gate(&mut region, &mut offset, None, [5, 9, 1, 9])?; + let (_, abcd1) = + config.assign_gate(&mut region, &mut offset, None, [5, 9, 1, 9])?; offset += 1; - let (_, abcd2) = assign_gate(&mut region, &mut offset, None, [2, 9, 1, 1])?; + let (_, abcd2) = + config.assign_gate(&mut region, &mut offset, None, [2, 9, 1, 1])?; offset += 1; - let (_, abcd3) = assign_gate(&mut region, &mut offset, None, [9, 2, 1, 1])?; + let (_, abcd3) = + config.assign_gate(&mut region, &mut offset, None, [9, 2, 1, 1])?; offset += 1; region.constrain_equal(abcd1[1].cell(), abcd1[3].cell())?; region.constrain_equal(abcd2[1].cell(), abcd1[3].cell())?; @@ -234,6 +312,17 @@ impl> Circuit for MyCircuit { 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 (_, abcd1) = config.assign_gate(&mut region, &mut offset, None, abcd)?; + let rlc = challenge + .zip(abcd1[0].value().zip(abcd1[1].value())) + .map(|(ch, (a, b))| *a + ch * b); + region.assign_advice(|| "", config.e, offset - 1, || rlc)?; + 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]; @@ -254,34 +343,149 @@ impl> Circuit for MyCircuit { offset += 1; } - Ok(instances) + Ok((offset, instance_copy)) }, )?; - println!("DBG instances: {:?}", instances); - for (i, instance) in instances.iter().enumerate() { - layouter.constrain_instance(instance.cell(), config.instance, i)?; - } + 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(|_| Self::configure_single(meta)) + .collect() + } + fn synthesize( + &self, + config: Vec, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + // 2 queries from first gate, 3 for permutation argument, 1 for multipoen, 1 for off-by-one + // errors, 1 for off-by-two errors? + let unusable_rows = 2 + 3 + 1 + 1 + 1; + let max_rows = 2usize.pow(self.k) - unusable_rows; + for config in &config { + let mut total_rows = 0; + loop { + let (rows, instance_copy) = self.synthesize_unit(config, &mut layouter)?; + 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; + } + } + assert!(total_rows <= max_rows); + } Ok(()) } } -use halo2curves::bn256::Fr; +use halo2_proofs::poly::kzg::commitment::{KZGCommitmentScheme, ParamsKZG, ParamsVerifierKZG}; +use halo2_proofs::poly::kzg::multiopen::{ProverSHPLONK, VerifierSHPLONK}; +use halo2_proofs::poly::kzg::strategy::SingleStrategy; +use halo2curves::bn256::{Bn256, Fr, G1Affine}; +use rand_core::block::BlockRng; +use rand_core::block::BlockRngCore; + +// One number generator, that can be used as a deterministic Rng, outputing fixed values. +struct OneNg {} + +impl BlockRngCore for OneNg { + type Item = u32; + type Results = [u32; 16]; + + fn generate(&mut self, results: &mut Self::Results) { + for elem in results.iter_mut() { + *elem = 1; + } + } +} #[test] -fn test_mycircuit() { - let k = 8; - let circuit: MyCircuit = MyCircuit { - _marker: std::marker::PhantomData {}, - }; - let instance = vec![ - Fr::from(0x1d), - Fr::from(0xf5), - Fr::from(0x2f5), - Fr::from(0x2), - Fr::from(0x2), - ]; - let prover = MockProver::run(k, &circuit, vec![instance]).unwrap(); +fn test_mycircuit_mock() { + let k = 6; + const WIDTH_FACTOR: usize = 2; + let circuit: MyCircuit = MyCircuit::new(k, 42); + let instances = circuit.instances(); + let prover = MockProver::run(k, &circuit, instances).unwrap(); prover.assert_satisfied(); } + +#[test] +fn test_mycircuit_full_legacy() { + let k = 6; + const WIDTH_FACTOR: usize = 1; + let circuit: MyCircuit = MyCircuit::new(k, 42); + + // Setup + let params = ParamsKZG::::new(k); + let verifier_params = params.verifier_params(); + let vk = keygen_vk(¶ms, &circuit).expect("keygen_vk should not fail"); + let pk = keygen_pk(¶ms, vk.clone(), &circuit).expect("keygen_pk should not fail"); + + // Proving + let instances = circuit.instances(); + let instances_slice: &[&[Fr]] = &(instances + .iter() + .map(|instance| instance.as_slice()) + .collect::>()); + + let rng = BlockRng::new(OneNg {}); + let mut transcript = Blake2bWrite::<_, G1Affine, Challenge255<_>>::init(vec![]); + create_proof::, ProverSHPLONK<'_, Bn256>, _, _, _, _>( + ¶ms, + &pk, + &[circuit.clone()], + &[instances_slice], + rng, + &mut transcript, + ) + .expect("proof generation should not fail"); + let proof = transcript.finalize(); + + // Verify + let mut verifier_transcript = + Blake2bRead::<_, G1Affine, Challenge255<_>>::init(proof.as_slice()); + let strategy = SingleStrategy::new(&verifier_params); + + verify_proof::, VerifierSHPLONK<'_, Bn256>, _, _, _>( + ¶ms, + &vk, + strategy, + &[instances_slice], + &mut verifier_transcript, + ) + .expect("verify succeeds"); +} + +#[test] +fn test_mycircuit_full_split() { + let k = 6; + const WIDTH_FACTOR: usize = 1; + let circuit: MyCircuit = MyCircuit::new(k, 42); + let compiled_circuit = compile_circuit(k, &circuit, false).unwrap(); + + // Setup + let params = ParamsKZG::::new(k); + let verifier_params = params.verifier_params(); + let vk = keygen_vk_v2(¶ms, &compiled_circuit).expect("keygen_vk should not fail"); + let pk = + keygen_pk_v2(¶ms, vk.clone(), &compiled_circuit).expect("keygen_pk should not fail"); +}