From 0cb6c00412c7c29cf1583d2c29b0e8b35f424316 Mon Sep 17 00:00:00 2001 From: Alexander Camuto Date: Thu, 26 Oct 2023 15:47:48 +0100 Subject: [PATCH 01/11] feat: optionally unblinded advice columns --- halo2_proofs/examples/vector-mul-unblinded.rs | 350 ++++++++++++++++++ halo2_proofs/src/plonk/circuit.rs | 30 ++ halo2_proofs/src/plonk/prover.rs | 24 +- 3 files changed, 399 insertions(+), 5 deletions(-) create mode 100644 halo2_proofs/examples/vector-mul-unblinded.rs diff --git a/halo2_proofs/examples/vector-mul-unblinded.rs b/halo2_proofs/examples/vector-mul-unblinded.rs new file mode 100644 index 0000000000..5b7c08914a --- /dev/null +++ b/halo2_proofs/examples/vector-mul-unblinded.rs @@ -0,0 +1,350 @@ +use std::marker::PhantomData; + +use halo2_proofs::{ + arithmetic::Field, + circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner, Value}, + plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector}, + poly::Rotation, +}; + +// ANCHOR: instructions +trait NumericInstructions: Chip { + /// Variable representing a number. + type Num; + + /// Loads a number into the circuit as a private input. + fn load_unblinded( + &self, + layouter: impl Layouter, + a: &[Value], + ) -> Result, Error>; + + /// Returns `c = a * b`. The caller is responsible for ensuring that `a.len() == b.len()`. + fn mul( + &self, + layouter: impl Layouter, + a: &[Self::Num], + b: &[Self::Num], + ) -> Result, Error>; + + /// Exposes a number as a public input to the circuit. + fn expose_public( + &self, + layouter: impl Layouter, + num: &Self::Num, + row: usize, + ) -> Result<(), Error>; +} +// ANCHOR_END: instructions + +// ANCHOR: chip +/// The chip that will implement our instructions! Chips store their own +/// config, as well as type markers if necessary. +struct FieldChip { + config: FieldConfig, + _marker: PhantomData, +} +// ANCHOR_END: chip + +// ANCHOR: chip-config +/// 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)] +struct FieldConfig { + /// For this chip, we will use two advice columns to implement our instructions. + /// These are also the columns through which we communicate with other parts of + /// the circuit. + advice: [Column; 3], + + /// This is the public input (instance) column. + instance: Column, + + // We need a selector to enable the multiplication gate, so that we aren't placing + // any constraints on cells where `NumericInstructions::mul` is not being used. + // This is important when building larger circuits, where columns are used by + // multiple sets of instructions. + s_mul: Selector, +} + +impl FieldChip { + fn construct(config: >::Config) -> Self { + Self { + config, + _marker: PhantomData, + } + } + + fn configure( + meta: &mut ConstraintSystem, + advice: [Column; 3], + instance: Column, + ) -> >::Config { + meta.enable_equality(instance); + for column in &advice { + meta.enable_equality(*column); + } + let s_mul = meta.selector(); + + // Define our multiplication gate! + meta.create_gate("mul", |meta| { + // To implement multiplication, we need three advice cells and a selector + // cell. We arrange them like so: + // + // | a0 | a1 | a2 | s_mul | + // |-----|-----|-----|-------| + // | lhs | rhs | out | s_mul | + // + // Gates may refer to any relative offsets we want, but each distinct + // offset adds a cost to the proof. The most common offsets are 0 (the + // current row), 1 (the next row), and -1 (the previous row), for which + // `Rotation` has specific constructors. + let lhs = meta.query_advice(advice[0], Rotation::cur()); + let rhs = meta.query_advice(advice[1], Rotation::cur()); + let out = meta.query_advice(advice[2], Rotation::cur()); + let s_mul = meta.query_selector(s_mul); + + // 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. Our expression + // has the following properties: + // - When s_mul = 0, any value is allowed in lhs, rhs, and out. + // - When s_mul != 0, this constrains lhs * rhs = out. + vec![s_mul * (lhs * rhs - out)] + }); + + FieldConfig { + advice, + instance, + s_mul, + } + } +} +// ANCHOR_END: chip-config + +// ANCHOR: chip-impl +impl Chip for FieldChip { + type Config = FieldConfig; + type Loaded = (); + + fn config(&self) -> &Self::Config { + &self.config + } + + fn loaded(&self) -> &Self::Loaded { + &() + } +} +// ANCHOR_END: chip-impl + +// ANCHOR: instructions-impl +/// A variable representing a number. +#[derive(Clone, Debug)] +struct Number(AssignedCell); + +impl NumericInstructions for FieldChip { + type Num = Number; + + fn load_unblinded( + &self, + mut layouter: impl Layouter, + values: &[Value], + ) -> Result, Error> { + let config = self.config(); + + layouter.assign_region( + || "load unblinded", + |mut region| { + values + .iter() + .enumerate() + .map(|(i, value)| { + region + .assign_advice(|| "private input", config.advice[0], i, || *value) + .map(Number) + }) + .collect() + }, + ) + } + + fn mul( + &self, + mut layouter: impl Layouter, + a: &[Self::Num], + b: &[Self::Num], + ) -> Result, Error> { + let config = self.config(); + assert_eq!(a.len(), b.len()); + + #[cfg(feature = "thread-safe-region")] + { + use maybe_rayon::prelude::{ + IndexedParallelIterator, IntoParallelRefIterator, ParallelIterator, + }; + layouter.assign_region( + || "mul", + |region: Region<'_, F>| { + let thread_safe_region = std::sync::Mutex::new(region); + a.par_iter() + .zip(b.par_iter()) + .enumerate() + .map(|(i, (a, b))| { + let mut region = thread_safe_region.lock().unwrap(); + + config.s_mul.enable(&mut region, i)?; + + a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; + b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; + + let value = a.0.value().copied() * b.0.value(); + + // Finally, we do the assignment to the output, returning a + // variable to be used in another part of the circuit. + region + .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) + .map(Number) + }) + .collect() + }, + ) + } + + #[cfg(not(feature = "thread-safe-region"))] + layouter.assign_region( + || "mul", + |mut region: Region<'_, F>| { + a.iter() + .zip(b.iter()) + .enumerate() + .map(|(i, (a, b))| { + config.s_mul.enable(&mut region, i)?; + + a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; + b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; + + let value = a.0.value().copied() * b.0.value(); + + // Finally, we do the assignment to the output, returning a + // variable to be used in another part of the circuit. + region + .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) + .map(Number) + }) + .collect() + }, + ) + } + + fn expose_public( + &self, + mut layouter: impl Layouter, + num: &Self::Num, + row: usize, + ) -> Result<(), Error> { + let config = self.config(); + + layouter.constrain_instance(num.0.cell(), config.instance, row) + } +} +// ANCHOR_END: instructions-impl + +// ANCHOR: circuit +/// The full circuit implementation. +/// +/// In this struct we store the private input variables. We use `Option` because +/// they won't have any value during key generation. During proving, if any of these +/// were `None` we would get an error. +#[derive(Default)] +struct MyCircuit { + a: Vec>, + b: Vec>, +} + +impl Circuit for MyCircuit { + // Since we are using a single chip for everything, we can just reuse its config. + type Config = FieldConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn without_witnesses(&self) -> Self { + Self::default() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + // We create the three advice columns that FieldChip uses for I/O. + let advice = [ + meta.unblinded_advice_column(), + meta.unblinded_advice_column(), + meta.unblinded_advice_column(), + ]; + + // We also need an instance column to store public inputs. + let instance = meta.instance_column(); + + FieldChip::configure(meta, advice, instance) + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let field_chip = FieldChip::::construct(config); + + // Load our private values into the circuit. + let a = field_chip.load_unblinded(layouter.namespace(|| "load a"), &self.a)?; + let b = field_chip.load_unblinded(layouter.namespace(|| "load b"), &self.b)?; + + let ab = field_chip.mul(layouter.namespace(|| "a * b"), &a, &b)?; + + for (i, c) in ab.iter().enumerate() { + // Expose the result as a public input to the circuit. + field_chip.expose_public(layouter.namespace(|| "expose c"), c, i)?; + } + Ok(()) + } +} +// ANCHOR_END: circuit + +fn main() { + use halo2_proofs::dev::MockProver; + use halo2curves::pasta::Fp; + + const N: usize = 20000; + // ANCHOR: test-circuit + // The number of rows in our circuit cannot exceed 2^k. Since our example + // circuit is very small, we can pick a very small value here. + let k = 16; + + // Prepare the private and public inputs to the circuit! + let a = [Fp::from(2); N]; + let b = [Fp::from(3); N]; + let c: Vec = a.iter().zip(b).map(|(&a, b)| a * b).collect(); + + // Instantiate the circuit with the private inputs. + let circuit = MyCircuit { + a: a.iter().map(|&x| Value::known(x)).collect(), + b: b.iter().map(|&x| Value::known(x)).collect(), + }; + + // Arrange the public input. We expose the multiplication result in row 0 + // of the instance column, so we position it there in our public inputs. + let mut public_inputs = c; + + let start = std::time::Instant::now(); + // Given the correct public input, our circuit will verify. + let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap(); + assert_eq!(prover.verify(), Ok(())); + println!("positive test took {:?}", start.elapsed()); + + // If we try some other public input, the proof will fail! + let start = std::time::Instant::now(); + public_inputs[0] += Fp::one(); + let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap(); + assert!(prover.verify().is_err()); + println!("negative test took {:?}", start.elapsed()); + // ANCHOR_END: test-circuit +} diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index ee9fb47fc5..ac865b67df 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -1555,6 +1555,9 @@ pub struct ConstraintSystem { pub(crate) num_selectors: usize, pub(crate) num_challenges: usize, + /// Contains the index of each advice column that is left unblinded. + pub(crate) unblinded_advice_columns: Vec, + /// Contains the phase for each advice column. Should have same length as num_advice_columns. pub(crate) advice_column_phase: Vec, /// Contains the phase for each challenge. Should have same length as num_challenges. @@ -1662,6 +1665,7 @@ impl Default for ConstraintSystem { num_instance_columns: 0, num_selectors: 0, num_challenges: 0, + unblinded_advice_columns: Vec::new(), advice_column_phase: Vec::new(), challenge_phase: Vec::new(), selector_map: vec![], @@ -2139,11 +2143,37 @@ impl ConstraintSystem { tmp } + /// Allocate a new unblinded advice column at `FirstPhase` + pub fn unblinded_advice_column(&mut self) -> Column { + self.unblinded_advice_column_in(FirstPhase) + } + /// Allocate a new advice column at `FirstPhase` pub fn advice_column(&mut self) -> Column { self.advice_column_in(FirstPhase) } + /// Allocate a new advice column in given phase + pub fn unblinded_advice_column_in(&mut self, phase: P) -> Column { + let phase = phase.to_sealed(); + if let Some(previous_phase) = phase.prev() { + self.assert_phase_exists( + previous_phase, + format!("Column in later phase {:?}", phase).as_str(), + ); + } + + let tmp = Column { + index: self.num_advice_columns, + column_type: Advice { phase }, + }; + self.unblinded_advice_columns.push(tmp.index); + self.num_advice_columns += 1; + self.num_advice_queries.push(0); + self.advice_column_phase.push(phase); + tmp + } + /// Allocate a new advice column in given phase pub fn advice_column_in(&mut self, phase: P) -> Column { let phase = phase.to_sealed(); diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index e64f3bfd8c..f6c012804f 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -1,7 +1,7 @@ use ff::{Field, FromUniformBytes, WithSmallOrderMulGroup}; use group::Curve; use rand_core::RngCore; -use std::collections::BTreeSet; +use std::collections::{BTreeSet, HashSet}; use std::ops::RangeTo; use std::{collections::HashMap, iter}; @@ -147,6 +147,7 @@ where k: u32, current_phase: sealed::Phase, advice: Vec, LagrangeCoeff>>, + unblinded_advice: HashSet, challenges: &'a HashMap, instances: &'a [&'a [F]], usable_rows: RangeTo, @@ -319,6 +320,9 @@ where k: params.k(), current_phase, advice: vec![domain.empty_lagrange_assigned(); meta.num_advice_columns], + unblinded_advice: HashSet::from_iter( + meta.unblinded_advice_columns.clone().into_iter(), + ), instances, challenges: &challenges, // The prover will not be allowed to assign values to advice @@ -353,16 +357,26 @@ where ); // Add blinding factors to advice columns - for advice_values in &mut advice_values { + for (column_index, advice_values) in &mut advice_values.iter_mut().enumerate() { for cell in &mut advice_values[unusable_rows_start..] { *cell = Scheme::Scalar::random(&mut rng); + if witness.unblinded_advice.contains(&column_index) { + *cell = Blind::default().0; + } else { + *cell = Scheme::Scalar::random(&mut rng); + } } } // Compute commitments to advice column polynomials - let blinds: Vec<_> = advice_values - .iter() - .map(|_| Blind(Scheme::Scalar::random(&mut rng))) + let blinds: Vec<_> = (0..meta.num_advice_columns) + .map(|i| { + if witness.unblinded_advice.contains(&i) { + Blind::default() + } else { + Blind(Scheme::Scalar::random(&mut rng)) + } + }) .collect(); let advice_commitments_projective: Vec<_> = advice_values .iter() From ed0498b8d65f76ef036cbd697491a684e5912370 Mon Sep 17 00:00:00 2001 From: Alexander Camuto Date: Thu, 26 Oct 2023 16:24:49 +0100 Subject: [PATCH 02/11] Delete vector-mul-unblinded.rs --- halo2_proofs/examples/vector-mul-unblinded.rs | 350 ------------------ 1 file changed, 350 deletions(-) delete mode 100644 halo2_proofs/examples/vector-mul-unblinded.rs diff --git a/halo2_proofs/examples/vector-mul-unblinded.rs b/halo2_proofs/examples/vector-mul-unblinded.rs deleted file mode 100644 index 5b7c08914a..0000000000 --- a/halo2_proofs/examples/vector-mul-unblinded.rs +++ /dev/null @@ -1,350 +0,0 @@ -use std::marker::PhantomData; - -use halo2_proofs::{ - arithmetic::Field, - circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner, Value}, - plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector}, - poly::Rotation, -}; - -// ANCHOR: instructions -trait NumericInstructions: Chip { - /// Variable representing a number. - type Num; - - /// Loads a number into the circuit as a private input. - fn load_unblinded( - &self, - layouter: impl Layouter, - a: &[Value], - ) -> Result, Error>; - - /// Returns `c = a * b`. The caller is responsible for ensuring that `a.len() == b.len()`. - fn mul( - &self, - layouter: impl Layouter, - a: &[Self::Num], - b: &[Self::Num], - ) -> Result, Error>; - - /// Exposes a number as a public input to the circuit. - fn expose_public( - &self, - layouter: impl Layouter, - num: &Self::Num, - row: usize, - ) -> Result<(), Error>; -} -// ANCHOR_END: instructions - -// ANCHOR: chip -/// The chip that will implement our instructions! Chips store their own -/// config, as well as type markers if necessary. -struct FieldChip { - config: FieldConfig, - _marker: PhantomData, -} -// ANCHOR_END: chip - -// ANCHOR: chip-config -/// 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)] -struct FieldConfig { - /// For this chip, we will use two advice columns to implement our instructions. - /// These are also the columns through which we communicate with other parts of - /// the circuit. - advice: [Column; 3], - - /// This is the public input (instance) column. - instance: Column, - - // We need a selector to enable the multiplication gate, so that we aren't placing - // any constraints on cells where `NumericInstructions::mul` is not being used. - // This is important when building larger circuits, where columns are used by - // multiple sets of instructions. - s_mul: Selector, -} - -impl FieldChip { - fn construct(config: >::Config) -> Self { - Self { - config, - _marker: PhantomData, - } - } - - fn configure( - meta: &mut ConstraintSystem, - advice: [Column; 3], - instance: Column, - ) -> >::Config { - meta.enable_equality(instance); - for column in &advice { - meta.enable_equality(*column); - } - let s_mul = meta.selector(); - - // Define our multiplication gate! - meta.create_gate("mul", |meta| { - // To implement multiplication, we need three advice cells and a selector - // cell. We arrange them like so: - // - // | a0 | a1 | a2 | s_mul | - // |-----|-----|-----|-------| - // | lhs | rhs | out | s_mul | - // - // Gates may refer to any relative offsets we want, but each distinct - // offset adds a cost to the proof. The most common offsets are 0 (the - // current row), 1 (the next row), and -1 (the previous row), for which - // `Rotation` has specific constructors. - let lhs = meta.query_advice(advice[0], Rotation::cur()); - let rhs = meta.query_advice(advice[1], Rotation::cur()); - let out = meta.query_advice(advice[2], Rotation::cur()); - let s_mul = meta.query_selector(s_mul); - - // 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. Our expression - // has the following properties: - // - When s_mul = 0, any value is allowed in lhs, rhs, and out. - // - When s_mul != 0, this constrains lhs * rhs = out. - vec![s_mul * (lhs * rhs - out)] - }); - - FieldConfig { - advice, - instance, - s_mul, - } - } -} -// ANCHOR_END: chip-config - -// ANCHOR: chip-impl -impl Chip for FieldChip { - type Config = FieldConfig; - type Loaded = (); - - fn config(&self) -> &Self::Config { - &self.config - } - - fn loaded(&self) -> &Self::Loaded { - &() - } -} -// ANCHOR_END: chip-impl - -// ANCHOR: instructions-impl -/// A variable representing a number. -#[derive(Clone, Debug)] -struct Number(AssignedCell); - -impl NumericInstructions for FieldChip { - type Num = Number; - - fn load_unblinded( - &self, - mut layouter: impl Layouter, - values: &[Value], - ) -> Result, Error> { - let config = self.config(); - - layouter.assign_region( - || "load unblinded", - |mut region| { - values - .iter() - .enumerate() - .map(|(i, value)| { - region - .assign_advice(|| "private input", config.advice[0], i, || *value) - .map(Number) - }) - .collect() - }, - ) - } - - fn mul( - &self, - mut layouter: impl Layouter, - a: &[Self::Num], - b: &[Self::Num], - ) -> Result, Error> { - let config = self.config(); - assert_eq!(a.len(), b.len()); - - #[cfg(feature = "thread-safe-region")] - { - use maybe_rayon::prelude::{ - IndexedParallelIterator, IntoParallelRefIterator, ParallelIterator, - }; - layouter.assign_region( - || "mul", - |region: Region<'_, F>| { - let thread_safe_region = std::sync::Mutex::new(region); - a.par_iter() - .zip(b.par_iter()) - .enumerate() - .map(|(i, (a, b))| { - let mut region = thread_safe_region.lock().unwrap(); - - config.s_mul.enable(&mut region, i)?; - - a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; - b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; - - let value = a.0.value().copied() * b.0.value(); - - // Finally, we do the assignment to the output, returning a - // variable to be used in another part of the circuit. - region - .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) - .map(Number) - }) - .collect() - }, - ) - } - - #[cfg(not(feature = "thread-safe-region"))] - layouter.assign_region( - || "mul", - |mut region: Region<'_, F>| { - a.iter() - .zip(b.iter()) - .enumerate() - .map(|(i, (a, b))| { - config.s_mul.enable(&mut region, i)?; - - a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; - b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; - - let value = a.0.value().copied() * b.0.value(); - - // Finally, we do the assignment to the output, returning a - // variable to be used in another part of the circuit. - region - .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) - .map(Number) - }) - .collect() - }, - ) - } - - fn expose_public( - &self, - mut layouter: impl Layouter, - num: &Self::Num, - row: usize, - ) -> Result<(), Error> { - let config = self.config(); - - layouter.constrain_instance(num.0.cell(), config.instance, row) - } -} -// ANCHOR_END: instructions-impl - -// ANCHOR: circuit -/// The full circuit implementation. -/// -/// In this struct we store the private input variables. We use `Option` because -/// they won't have any value during key generation. During proving, if any of these -/// were `None` we would get an error. -#[derive(Default)] -struct MyCircuit { - a: Vec>, - b: Vec>, -} - -impl Circuit for MyCircuit { - // Since we are using a single chip for everything, we can just reuse its config. - type Config = FieldConfig; - type FloorPlanner = SimpleFloorPlanner; - #[cfg(feature = "circuit-params")] - type Params = (); - - fn without_witnesses(&self) -> Self { - Self::default() - } - - fn configure(meta: &mut ConstraintSystem) -> Self::Config { - // We create the three advice columns that FieldChip uses for I/O. - let advice = [ - meta.unblinded_advice_column(), - meta.unblinded_advice_column(), - meta.unblinded_advice_column(), - ]; - - // We also need an instance column to store public inputs. - let instance = meta.instance_column(); - - FieldChip::configure(meta, advice, instance) - } - - fn synthesize( - &self, - config: Self::Config, - mut layouter: impl Layouter, - ) -> Result<(), Error> { - let field_chip = FieldChip::::construct(config); - - // Load our private values into the circuit. - let a = field_chip.load_unblinded(layouter.namespace(|| "load a"), &self.a)?; - let b = field_chip.load_unblinded(layouter.namespace(|| "load b"), &self.b)?; - - let ab = field_chip.mul(layouter.namespace(|| "a * b"), &a, &b)?; - - for (i, c) in ab.iter().enumerate() { - // Expose the result as a public input to the circuit. - field_chip.expose_public(layouter.namespace(|| "expose c"), c, i)?; - } - Ok(()) - } -} -// ANCHOR_END: circuit - -fn main() { - use halo2_proofs::dev::MockProver; - use halo2curves::pasta::Fp; - - const N: usize = 20000; - // ANCHOR: test-circuit - // The number of rows in our circuit cannot exceed 2^k. Since our example - // circuit is very small, we can pick a very small value here. - let k = 16; - - // Prepare the private and public inputs to the circuit! - let a = [Fp::from(2); N]; - let b = [Fp::from(3); N]; - let c: Vec = a.iter().zip(b).map(|(&a, b)| a * b).collect(); - - // Instantiate the circuit with the private inputs. - let circuit = MyCircuit { - a: a.iter().map(|&x| Value::known(x)).collect(), - b: b.iter().map(|&x| Value::known(x)).collect(), - }; - - // Arrange the public input. We expose the multiplication result in row 0 - // of the instance column, so we position it there in our public inputs. - let mut public_inputs = c; - - let start = std::time::Instant::now(); - // Given the correct public input, our circuit will verify. - let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap(); - assert_eq!(prover.verify(), Ok(())); - println!("positive test took {:?}", start.elapsed()); - - // If we try some other public input, the proof will fail! - let start = std::time::Instant::now(); - public_inputs[0] += Fp::one(); - let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap(); - assert!(prover.verify().is_err()); - println!("negative test took {:?}", start.elapsed()); - // ANCHOR_END: test-circuit -} From 6678d053a3d66564e90863c2eddb22b1f41e8da7 Mon Sep 17 00:00:00 2001 From: dante <45801863+alexander-camuto@users.noreply.github.com> Date: Tue, 31 Oct 2023 15:10:31 +0000 Subject: [PATCH 03/11] Update halo2_proofs/src/plonk/circuit.rs Co-authored-by: Han --- halo2_proofs/src/plonk/circuit.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index ac865b67df..c8a8f625e8 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -2153,7 +2153,7 @@ impl ConstraintSystem { self.advice_column_in(FirstPhase) } - /// Allocate a new advice column in given phase + /// Allocate a new unblinded advice column in given phase pub fn unblinded_advice_column_in(&mut self, phase: P) -> Column { let phase = phase.to_sealed(); if let Some(previous_phase) = phase.prev() { From 127f12d5c3cbdaed3204f2d10edbeeb1656b36ee Mon Sep 17 00:00:00 2001 From: Alexander Camuto <45801863+alexander-camuto@users.noreply.github.com> Date: Tue, 31 Oct 2023 15:22:35 +0000 Subject: [PATCH 04/11] update description --- halo2_proofs/src/plonk/circuit.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index c8a8f625e8..82cb0df08f 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -2153,7 +2153,8 @@ impl ConstraintSystem { self.advice_column_in(FirstPhase) } - /// Allocate a new unblinded advice column in given phase + /// Allocate a new unblinded advice column in given phase. The allows for the generation of deterministic commitments to advice columns + /// which can be used to split large circuits into smaller ones, whose proofs can then be "joined" together by their common witness commitments. pub fn unblinded_advice_column_in(&mut self, phase: P) -> Column { let phase = phase.to_sealed(); if let Some(previous_phase) = phase.prev() { From 3170018254d2e3482e53f01b1b72181e879f1e9b Mon Sep 17 00:00:00 2001 From: dante <45801863+alexander-camuto@users.noreply.github.com> Date: Tue, 31 Oct 2023 15:25:33 +0000 Subject: [PATCH 05/11] Update halo2_proofs/src/plonk/prover.rs Co-authored-by: Han --- halo2_proofs/src/plonk/prover.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index f6c012804f..6d1278305e 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -320,9 +320,7 @@ where k: params.k(), current_phase, advice: vec![domain.empty_lagrange_assigned(); meta.num_advice_columns], - unblinded_advice: HashSet::from_iter( - meta.unblinded_advice_columns.clone().into_iter(), - ), + unblinded_advice: HashSet::from_iter(meta.unblinded_advice_columns.clone()), instances, challenges: &challenges, // The prover will not be allowed to assign values to advice From bf9f53cf5aa045f149411ebf992623ea5afab2db Mon Sep 17 00:00:00 2001 From: dante <45801863+alexander-camuto@users.noreply.github.com> Date: Tue, 31 Oct 2023 15:30:14 +0000 Subject: [PATCH 06/11] Update halo2_proofs/src/plonk/prover.rs Co-authored-by: Han --- halo2_proofs/src/plonk/prover.rs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index 6d1278305e..cfc74ab283 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -355,14 +355,18 @@ where ); // Add blinding factors to advice columns - for (column_index, advice_values) in &mut advice_values.iter_mut().enumerate() { - for cell in &mut advice_values[unusable_rows_start..] { - *cell = Scheme::Scalar::random(&mut rng); - if witness.unblinded_advice.contains(&column_index) { - *cell = Blind::default().0; - } else { + for (column_index, advice_values) in column_indices.iter().zip(&mut advice_values) { + if witness.unblinded_advice.contains(column_index) { + for cell in &mut advice_values[unusable_rows_start..] { *cell = Scheme::Scalar::random(&mut rng); } + } else { + #[cfg(feature = "sanity-checks")] + for cell in &advice_values[unusable_rows_start..] { + assert_eq!(*cell, Scheme::Scalar::ZERO); + } + } + } } } From 51b8f715468e8b65ff1917bcc1be77a9c7e830ce Mon Sep 17 00:00:00 2001 From: dante <45801863+alexander-camuto@users.noreply.github.com> Date: Tue, 31 Oct 2023 15:30:42 +0000 Subject: [PATCH 07/11] Update halo2_proofs/src/plonk/prover.rs Co-authored-by: Han --- halo2_proofs/src/plonk/prover.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index cfc74ab283..89f73bb779 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -371,9 +371,10 @@ where } // Compute commitments to advice column polynomials - let blinds: Vec<_> = (0..meta.num_advice_columns) + let blinds: Vec<_> = column_indices + .iter() .map(|i| { - if witness.unblinded_advice.contains(&i) { + if witness.unblinded_advice.contains(i) { Blind::default() } else { Blind(Scheme::Scalar::random(&mut rng)) From aa0c4570db470fa7639a590261c2767e04ab2c4e Mon Sep 17 00:00:00 2001 From: Alexander Camuto <45801863+alexander-camuto@users.noreply.github.com> Date: Tue, 31 Oct 2023 15:46:36 +0000 Subject: [PATCH 08/11] patch braces --- halo2_proofs/src/plonk/prover.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index 89f73bb779..2a43bf0958 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -367,8 +367,6 @@ where } } } - } - } // Compute commitments to advice column polynomials let blinds: Vec<_> = column_indices From 6ef47dd564aee51e4523b198d832be94c2e7453e Mon Sep 17 00:00:00 2001 From: Alexander Camuto Date: Tue, 7 Nov 2023 12:54:58 +0000 Subject: [PATCH 09/11] Revert "Delete vector-mul-unblinded.rs" This reverts commit ed0498b8d65f76ef036cbd697491a684e5912370. --- halo2_proofs/examples/vector-mul-unblinded.rs | 350 ++++++++++++++++++ 1 file changed, 350 insertions(+) create mode 100644 halo2_proofs/examples/vector-mul-unblinded.rs diff --git a/halo2_proofs/examples/vector-mul-unblinded.rs b/halo2_proofs/examples/vector-mul-unblinded.rs new file mode 100644 index 0000000000..5b7c08914a --- /dev/null +++ b/halo2_proofs/examples/vector-mul-unblinded.rs @@ -0,0 +1,350 @@ +use std::marker::PhantomData; + +use halo2_proofs::{ + arithmetic::Field, + circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner, Value}, + plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector}, + poly::Rotation, +}; + +// ANCHOR: instructions +trait NumericInstructions: Chip { + /// Variable representing a number. + type Num; + + /// Loads a number into the circuit as a private input. + fn load_unblinded( + &self, + layouter: impl Layouter, + a: &[Value], + ) -> Result, Error>; + + /// Returns `c = a * b`. The caller is responsible for ensuring that `a.len() == b.len()`. + fn mul( + &self, + layouter: impl Layouter, + a: &[Self::Num], + b: &[Self::Num], + ) -> Result, Error>; + + /// Exposes a number as a public input to the circuit. + fn expose_public( + &self, + layouter: impl Layouter, + num: &Self::Num, + row: usize, + ) -> Result<(), Error>; +} +// ANCHOR_END: instructions + +// ANCHOR: chip +/// The chip that will implement our instructions! Chips store their own +/// config, as well as type markers if necessary. +struct FieldChip { + config: FieldConfig, + _marker: PhantomData, +} +// ANCHOR_END: chip + +// ANCHOR: chip-config +/// 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)] +struct FieldConfig { + /// For this chip, we will use two advice columns to implement our instructions. + /// These are also the columns through which we communicate with other parts of + /// the circuit. + advice: [Column; 3], + + /// This is the public input (instance) column. + instance: Column, + + // We need a selector to enable the multiplication gate, so that we aren't placing + // any constraints on cells where `NumericInstructions::mul` is not being used. + // This is important when building larger circuits, where columns are used by + // multiple sets of instructions. + s_mul: Selector, +} + +impl FieldChip { + fn construct(config: >::Config) -> Self { + Self { + config, + _marker: PhantomData, + } + } + + fn configure( + meta: &mut ConstraintSystem, + advice: [Column; 3], + instance: Column, + ) -> >::Config { + meta.enable_equality(instance); + for column in &advice { + meta.enable_equality(*column); + } + let s_mul = meta.selector(); + + // Define our multiplication gate! + meta.create_gate("mul", |meta| { + // To implement multiplication, we need three advice cells and a selector + // cell. We arrange them like so: + // + // | a0 | a1 | a2 | s_mul | + // |-----|-----|-----|-------| + // | lhs | rhs | out | s_mul | + // + // Gates may refer to any relative offsets we want, but each distinct + // offset adds a cost to the proof. The most common offsets are 0 (the + // current row), 1 (the next row), and -1 (the previous row), for which + // `Rotation` has specific constructors. + let lhs = meta.query_advice(advice[0], Rotation::cur()); + let rhs = meta.query_advice(advice[1], Rotation::cur()); + let out = meta.query_advice(advice[2], Rotation::cur()); + let s_mul = meta.query_selector(s_mul); + + // 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. Our expression + // has the following properties: + // - When s_mul = 0, any value is allowed in lhs, rhs, and out. + // - When s_mul != 0, this constrains lhs * rhs = out. + vec![s_mul * (lhs * rhs - out)] + }); + + FieldConfig { + advice, + instance, + s_mul, + } + } +} +// ANCHOR_END: chip-config + +// ANCHOR: chip-impl +impl Chip for FieldChip { + type Config = FieldConfig; + type Loaded = (); + + fn config(&self) -> &Self::Config { + &self.config + } + + fn loaded(&self) -> &Self::Loaded { + &() + } +} +// ANCHOR_END: chip-impl + +// ANCHOR: instructions-impl +/// A variable representing a number. +#[derive(Clone, Debug)] +struct Number(AssignedCell); + +impl NumericInstructions for FieldChip { + type Num = Number; + + fn load_unblinded( + &self, + mut layouter: impl Layouter, + values: &[Value], + ) -> Result, Error> { + let config = self.config(); + + layouter.assign_region( + || "load unblinded", + |mut region| { + values + .iter() + .enumerate() + .map(|(i, value)| { + region + .assign_advice(|| "private input", config.advice[0], i, || *value) + .map(Number) + }) + .collect() + }, + ) + } + + fn mul( + &self, + mut layouter: impl Layouter, + a: &[Self::Num], + b: &[Self::Num], + ) -> Result, Error> { + let config = self.config(); + assert_eq!(a.len(), b.len()); + + #[cfg(feature = "thread-safe-region")] + { + use maybe_rayon::prelude::{ + IndexedParallelIterator, IntoParallelRefIterator, ParallelIterator, + }; + layouter.assign_region( + || "mul", + |region: Region<'_, F>| { + let thread_safe_region = std::sync::Mutex::new(region); + a.par_iter() + .zip(b.par_iter()) + .enumerate() + .map(|(i, (a, b))| { + let mut region = thread_safe_region.lock().unwrap(); + + config.s_mul.enable(&mut region, i)?; + + a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; + b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; + + let value = a.0.value().copied() * b.0.value(); + + // Finally, we do the assignment to the output, returning a + // variable to be used in another part of the circuit. + region + .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) + .map(Number) + }) + .collect() + }, + ) + } + + #[cfg(not(feature = "thread-safe-region"))] + layouter.assign_region( + || "mul", + |mut region: Region<'_, F>| { + a.iter() + .zip(b.iter()) + .enumerate() + .map(|(i, (a, b))| { + config.s_mul.enable(&mut region, i)?; + + a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; + b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; + + let value = a.0.value().copied() * b.0.value(); + + // Finally, we do the assignment to the output, returning a + // variable to be used in another part of the circuit. + region + .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) + .map(Number) + }) + .collect() + }, + ) + } + + fn expose_public( + &self, + mut layouter: impl Layouter, + num: &Self::Num, + row: usize, + ) -> Result<(), Error> { + let config = self.config(); + + layouter.constrain_instance(num.0.cell(), config.instance, row) + } +} +// ANCHOR_END: instructions-impl + +// ANCHOR: circuit +/// The full circuit implementation. +/// +/// In this struct we store the private input variables. We use `Option` because +/// they won't have any value during key generation. During proving, if any of these +/// were `None` we would get an error. +#[derive(Default)] +struct MyCircuit { + a: Vec>, + b: Vec>, +} + +impl Circuit for MyCircuit { + // Since we are using a single chip for everything, we can just reuse its config. + type Config = FieldConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn without_witnesses(&self) -> Self { + Self::default() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + // We create the three advice columns that FieldChip uses for I/O. + let advice = [ + meta.unblinded_advice_column(), + meta.unblinded_advice_column(), + meta.unblinded_advice_column(), + ]; + + // We also need an instance column to store public inputs. + let instance = meta.instance_column(); + + FieldChip::configure(meta, advice, instance) + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let field_chip = FieldChip::::construct(config); + + // Load our private values into the circuit. + let a = field_chip.load_unblinded(layouter.namespace(|| "load a"), &self.a)?; + let b = field_chip.load_unblinded(layouter.namespace(|| "load b"), &self.b)?; + + let ab = field_chip.mul(layouter.namespace(|| "a * b"), &a, &b)?; + + for (i, c) in ab.iter().enumerate() { + // Expose the result as a public input to the circuit. + field_chip.expose_public(layouter.namespace(|| "expose c"), c, i)?; + } + Ok(()) + } +} +// ANCHOR_END: circuit + +fn main() { + use halo2_proofs::dev::MockProver; + use halo2curves::pasta::Fp; + + const N: usize = 20000; + // ANCHOR: test-circuit + // The number of rows in our circuit cannot exceed 2^k. Since our example + // circuit is very small, we can pick a very small value here. + let k = 16; + + // Prepare the private and public inputs to the circuit! + let a = [Fp::from(2); N]; + let b = [Fp::from(3); N]; + let c: Vec = a.iter().zip(b).map(|(&a, b)| a * b).collect(); + + // Instantiate the circuit with the private inputs. + let circuit = MyCircuit { + a: a.iter().map(|&x| Value::known(x)).collect(), + b: b.iter().map(|&x| Value::known(x)).collect(), + }; + + // Arrange the public input. We expose the multiplication result in row 0 + // of the instance column, so we position it there in our public inputs. + let mut public_inputs = c; + + let start = std::time::Instant::now(); + // Given the correct public input, our circuit will verify. + let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap(); + assert_eq!(prover.verify(), Ok(())); + println!("positive test took {:?}", start.elapsed()); + + // If we try some other public input, the proof will fail! + let start = std::time::Instant::now(); + public_inputs[0] += Fp::one(); + let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap(); + assert!(prover.verify().is_err()); + println!("negative test took {:?}", start.elapsed()); + // ANCHOR_END: test-circuit +} From 6f4272cfcd91533f9d40c3f52d6e55afc8816cde Mon Sep 17 00:00:00 2001 From: Alexander Camuto Date: Tue, 7 Nov 2023 13:25:38 +0000 Subject: [PATCH 10/11] make example more specific --- halo2_proofs/examples/vector-mul-unblinded.rs | 350 ----------- halo2_proofs/examples/vector-ops-unblinded.rs | 557 ++++++++++++++++++ halo2_proofs/src/plonk/prover.rs | 2 +- 3 files changed, 558 insertions(+), 351 deletions(-) delete mode 100644 halo2_proofs/examples/vector-mul-unblinded.rs create mode 100644 halo2_proofs/examples/vector-ops-unblinded.rs diff --git a/halo2_proofs/examples/vector-mul-unblinded.rs b/halo2_proofs/examples/vector-mul-unblinded.rs deleted file mode 100644 index 5b7c08914a..0000000000 --- a/halo2_proofs/examples/vector-mul-unblinded.rs +++ /dev/null @@ -1,350 +0,0 @@ -use std::marker::PhantomData; - -use halo2_proofs::{ - arithmetic::Field, - circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner, Value}, - plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector}, - poly::Rotation, -}; - -// ANCHOR: instructions -trait NumericInstructions: Chip { - /// Variable representing a number. - type Num; - - /// Loads a number into the circuit as a private input. - fn load_unblinded( - &self, - layouter: impl Layouter, - a: &[Value], - ) -> Result, Error>; - - /// Returns `c = a * b`. The caller is responsible for ensuring that `a.len() == b.len()`. - fn mul( - &self, - layouter: impl Layouter, - a: &[Self::Num], - b: &[Self::Num], - ) -> Result, Error>; - - /// Exposes a number as a public input to the circuit. - fn expose_public( - &self, - layouter: impl Layouter, - num: &Self::Num, - row: usize, - ) -> Result<(), Error>; -} -// ANCHOR_END: instructions - -// ANCHOR: chip -/// The chip that will implement our instructions! Chips store their own -/// config, as well as type markers if necessary. -struct FieldChip { - config: FieldConfig, - _marker: PhantomData, -} -// ANCHOR_END: chip - -// ANCHOR: chip-config -/// 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)] -struct FieldConfig { - /// For this chip, we will use two advice columns to implement our instructions. - /// These are also the columns through which we communicate with other parts of - /// the circuit. - advice: [Column; 3], - - /// This is the public input (instance) column. - instance: Column, - - // We need a selector to enable the multiplication gate, so that we aren't placing - // any constraints on cells where `NumericInstructions::mul` is not being used. - // This is important when building larger circuits, where columns are used by - // multiple sets of instructions. - s_mul: Selector, -} - -impl FieldChip { - fn construct(config: >::Config) -> Self { - Self { - config, - _marker: PhantomData, - } - } - - fn configure( - meta: &mut ConstraintSystem, - advice: [Column; 3], - instance: Column, - ) -> >::Config { - meta.enable_equality(instance); - for column in &advice { - meta.enable_equality(*column); - } - let s_mul = meta.selector(); - - // Define our multiplication gate! - meta.create_gate("mul", |meta| { - // To implement multiplication, we need three advice cells and a selector - // cell. We arrange them like so: - // - // | a0 | a1 | a2 | s_mul | - // |-----|-----|-----|-------| - // | lhs | rhs | out | s_mul | - // - // Gates may refer to any relative offsets we want, but each distinct - // offset adds a cost to the proof. The most common offsets are 0 (the - // current row), 1 (the next row), and -1 (the previous row), for which - // `Rotation` has specific constructors. - let lhs = meta.query_advice(advice[0], Rotation::cur()); - let rhs = meta.query_advice(advice[1], Rotation::cur()); - let out = meta.query_advice(advice[2], Rotation::cur()); - let s_mul = meta.query_selector(s_mul); - - // 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. Our expression - // has the following properties: - // - When s_mul = 0, any value is allowed in lhs, rhs, and out. - // - When s_mul != 0, this constrains lhs * rhs = out. - vec![s_mul * (lhs * rhs - out)] - }); - - FieldConfig { - advice, - instance, - s_mul, - } - } -} -// ANCHOR_END: chip-config - -// ANCHOR: chip-impl -impl Chip for FieldChip { - type Config = FieldConfig; - type Loaded = (); - - fn config(&self) -> &Self::Config { - &self.config - } - - fn loaded(&self) -> &Self::Loaded { - &() - } -} -// ANCHOR_END: chip-impl - -// ANCHOR: instructions-impl -/// A variable representing a number. -#[derive(Clone, Debug)] -struct Number(AssignedCell); - -impl NumericInstructions for FieldChip { - type Num = Number; - - fn load_unblinded( - &self, - mut layouter: impl Layouter, - values: &[Value], - ) -> Result, Error> { - let config = self.config(); - - layouter.assign_region( - || "load unblinded", - |mut region| { - values - .iter() - .enumerate() - .map(|(i, value)| { - region - .assign_advice(|| "private input", config.advice[0], i, || *value) - .map(Number) - }) - .collect() - }, - ) - } - - fn mul( - &self, - mut layouter: impl Layouter, - a: &[Self::Num], - b: &[Self::Num], - ) -> Result, Error> { - let config = self.config(); - assert_eq!(a.len(), b.len()); - - #[cfg(feature = "thread-safe-region")] - { - use maybe_rayon::prelude::{ - IndexedParallelIterator, IntoParallelRefIterator, ParallelIterator, - }; - layouter.assign_region( - || "mul", - |region: Region<'_, F>| { - let thread_safe_region = std::sync::Mutex::new(region); - a.par_iter() - .zip(b.par_iter()) - .enumerate() - .map(|(i, (a, b))| { - let mut region = thread_safe_region.lock().unwrap(); - - config.s_mul.enable(&mut region, i)?; - - a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; - b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; - - let value = a.0.value().copied() * b.0.value(); - - // Finally, we do the assignment to the output, returning a - // variable to be used in another part of the circuit. - region - .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) - .map(Number) - }) - .collect() - }, - ) - } - - #[cfg(not(feature = "thread-safe-region"))] - layouter.assign_region( - || "mul", - |mut region: Region<'_, F>| { - a.iter() - .zip(b.iter()) - .enumerate() - .map(|(i, (a, b))| { - config.s_mul.enable(&mut region, i)?; - - a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; - b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; - - let value = a.0.value().copied() * b.0.value(); - - // Finally, we do the assignment to the output, returning a - // variable to be used in another part of the circuit. - region - .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) - .map(Number) - }) - .collect() - }, - ) - } - - fn expose_public( - &self, - mut layouter: impl Layouter, - num: &Self::Num, - row: usize, - ) -> Result<(), Error> { - let config = self.config(); - - layouter.constrain_instance(num.0.cell(), config.instance, row) - } -} -// ANCHOR_END: instructions-impl - -// ANCHOR: circuit -/// The full circuit implementation. -/// -/// In this struct we store the private input variables. We use `Option` because -/// they won't have any value during key generation. During proving, if any of these -/// were `None` we would get an error. -#[derive(Default)] -struct MyCircuit { - a: Vec>, - b: Vec>, -} - -impl Circuit for MyCircuit { - // Since we are using a single chip for everything, we can just reuse its config. - type Config = FieldConfig; - type FloorPlanner = SimpleFloorPlanner; - #[cfg(feature = "circuit-params")] - type Params = (); - - fn without_witnesses(&self) -> Self { - Self::default() - } - - fn configure(meta: &mut ConstraintSystem) -> Self::Config { - // We create the three advice columns that FieldChip uses for I/O. - let advice = [ - meta.unblinded_advice_column(), - meta.unblinded_advice_column(), - meta.unblinded_advice_column(), - ]; - - // We also need an instance column to store public inputs. - let instance = meta.instance_column(); - - FieldChip::configure(meta, advice, instance) - } - - fn synthesize( - &self, - config: Self::Config, - mut layouter: impl Layouter, - ) -> Result<(), Error> { - let field_chip = FieldChip::::construct(config); - - // Load our private values into the circuit. - let a = field_chip.load_unblinded(layouter.namespace(|| "load a"), &self.a)?; - let b = field_chip.load_unblinded(layouter.namespace(|| "load b"), &self.b)?; - - let ab = field_chip.mul(layouter.namespace(|| "a * b"), &a, &b)?; - - for (i, c) in ab.iter().enumerate() { - // Expose the result as a public input to the circuit. - field_chip.expose_public(layouter.namespace(|| "expose c"), c, i)?; - } - Ok(()) - } -} -// ANCHOR_END: circuit - -fn main() { - use halo2_proofs::dev::MockProver; - use halo2curves::pasta::Fp; - - const N: usize = 20000; - // ANCHOR: test-circuit - // The number of rows in our circuit cannot exceed 2^k. Since our example - // circuit is very small, we can pick a very small value here. - let k = 16; - - // Prepare the private and public inputs to the circuit! - let a = [Fp::from(2); N]; - let b = [Fp::from(3); N]; - let c: Vec = a.iter().zip(b).map(|(&a, b)| a * b).collect(); - - // Instantiate the circuit with the private inputs. - let circuit = MyCircuit { - a: a.iter().map(|&x| Value::known(x)).collect(), - b: b.iter().map(|&x| Value::known(x)).collect(), - }; - - // Arrange the public input. We expose the multiplication result in row 0 - // of the instance column, so we position it there in our public inputs. - let mut public_inputs = c; - - let start = std::time::Instant::now(); - // Given the correct public input, our circuit will verify. - let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap(); - assert_eq!(prover.verify(), Ok(())); - println!("positive test took {:?}", start.elapsed()); - - // If we try some other public input, the proof will fail! - let start = std::time::Instant::now(); - public_inputs[0] += Fp::one(); - let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap(); - assert!(prover.verify().is_err()); - println!("negative test took {:?}", start.elapsed()); - // ANCHOR_END: test-circuit -} diff --git a/halo2_proofs/examples/vector-ops-unblinded.rs b/halo2_proofs/examples/vector-ops-unblinded.rs new file mode 100644 index 0000000000..7e9ebd1d81 --- /dev/null +++ b/halo2_proofs/examples/vector-ops-unblinded.rs @@ -0,0 +1,557 @@ +/// Here we construct two circuits one for adding two vectors and one for multiplying and we check that their transcripts have the same inputs +/// by way of the unblinded inputs. +/// This is a simple example of how to use unblinded inputs to match up circuits that might be proved on different host machines. +use std::marker::PhantomData; + +use ff::FromUniformBytes; +use halo2_proofs::{ + arithmetic::{CurveAffine, Field}, + circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner, Value}, + plonk::*, + poly::{ + commitment::ParamsProver, + ipa::{ + commitment::{IPACommitmentScheme, ParamsIPA}, + multiopen::{ProverIPA, VerifierIPA}, + strategy::AccumulatorStrategy, + }, + Rotation, VerificationStrategy, + }, + transcript::{ + Blake2bRead, Blake2bWrite, Challenge255, TranscriptReadBuffer, TranscriptWriterBuffer, + }, +}; +use rand_core::OsRng; + +// ANCHOR: instructions +trait NumericInstructions: Chip { + /// Variable representing a number. + type Num; + + /// Loads a number into the circuit as an unblinded input this can be matched to inputs in other circuits ! + fn load_unblinded( + &self, + layouter: impl Layouter, + a: &[Value], + ) -> Result, Error>; + + /// Returns `c = a * b`. The caller is responsible for ensuring that `a.len() == b.len()`. + fn mul( + &self, + layouter: impl Layouter, + a: &[Self::Num], + b: &[Self::Num], + ) -> Result, Error>; + + /// Returns `c = a + b`. The caller is responsible for ensuring that `a.len() == b.len()`. + fn add( + &self, + layouter: impl Layouter, + a: &[Self::Num], + b: &[Self::Num], + ) -> Result, Error>; + + /// Exposes a number as a public input to the circuit. + fn expose_public( + &self, + layouter: impl Layouter, + num: &Self::Num, + row: usize, + ) -> Result<(), Error>; +} +// ANCHOR_END: instructions + +// ANCHOR: chip +/// The chip that will implement our instructions! Chips store their own +/// config, as well as type markers if necessary. +struct MultChip { + config: FieldConfig, + _marker: PhantomData, +} + +// ANCHOR: chip +/// The chip that will implement our instructions! Chips store their own +/// config, as well as type markers if necessary. +struct AddChip { + config: FieldConfig, + _marker: PhantomData, +} +// ANCHOR_END: chip + +// ANCHOR: chip-config +/// 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)] +struct FieldConfig { + advice: [Column; 3], + instance: Column, + s: Selector, +} + +impl MultChip { + fn construct(config: >::Config) -> Self { + Self { + config, + _marker: PhantomData, + } + } + + fn configure( + meta: &mut ConstraintSystem, + advice: [Column; 3], + instance: Column, + ) -> >::Config { + meta.enable_equality(instance); + for column in &advice { + meta.enable_equality(*column); + } + let s = meta.selector(); + + // Define our multiplication gate! + meta.create_gate("mul", |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[2], Rotation::cur()); + let s_mul = meta.query_selector(s); + + vec![s_mul * (lhs * rhs - out)] + }); + + FieldConfig { + advice, + instance, + s, + } + } +} + +impl AddChip { + fn construct(config: >::Config) -> Self { + Self { + config, + _marker: PhantomData, + } + } + + fn configure( + meta: &mut ConstraintSystem, + advice: [Column; 3], + instance: Column, + ) -> >::Config { + meta.enable_equality(instance); + for column in &advice { + meta.enable_equality(*column); + } + let s = meta.selector(); + + // Define our multiplication gate! + meta.create_gate("add", |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[2], Rotation::cur()); + let s_add = meta.query_selector(s); + + vec![s_add * (lhs + rhs - out)] + }); + + FieldConfig { + advice, + instance, + s, + } + } +} +// ANCHOR_END: chip-config + +// ANCHOR: chip-impl +impl Chip for MultChip { + type Config = FieldConfig; + type Loaded = (); + + fn config(&self) -> &Self::Config { + &self.config + } + + fn loaded(&self) -> &Self::Loaded { + &() + } +} +// ANCHOR_END: chip-impl + +// ANCHOR: chip-impl +impl Chip for AddChip { + type Config = FieldConfig; + type Loaded = (); + + fn config(&self) -> &Self::Config { + &self.config + } + + fn loaded(&self) -> &Self::Loaded { + &() + } +} + +// ANCHOR: instructions-impl +/// A variable representing a number. +#[derive(Clone, Debug)] +struct Number(AssignedCell); + +impl NumericInstructions for MultChip { + type Num = Number; + + fn load_unblinded( + &self, + mut layouter: impl Layouter, + values: &[Value], + ) -> Result, Error> { + let config = self.config(); + + layouter.assign_region( + || "load unblinded", + |mut region| { + values + .iter() + .enumerate() + .map(|(i, value)| { + region + .assign_advice(|| "unblinded input", config.advice[0], i, || *value) + .map(Number) + }) + .collect() + }, + ) + } + + fn add( + &self, + _: impl Layouter, + _: &[Self::Num], + _: &[Self::Num], + ) -> Result, Error> { + panic!("Not implemented") + } + + fn mul( + &self, + mut layouter: impl Layouter, + a: &[Self::Num], + b: &[Self::Num], + ) -> Result, Error> { + let config = self.config(); + assert_eq!(a.len(), b.len()); + + layouter.assign_region( + || "mul", + |mut region: Region<'_, F>| { + a.iter() + .zip(b.iter()) + .enumerate() + .map(|(i, (a, b))| { + config.s.enable(&mut region, i)?; + + a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; + b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; + + let value = a.0.value().copied() * b.0.value(); + + // Finally, we do the assignment to the output, returning a + // variable to be used in another part of the circuit. + region + .assign_advice(|| "lhs * rhs", config.advice[2], i, || value) + .map(Number) + }) + .collect() + }, + ) + } + + fn expose_public( + &self, + mut layouter: impl Layouter, + num: &Self::Num, + row: usize, + ) -> Result<(), Error> { + let config = self.config(); + + layouter.constrain_instance(num.0.cell(), config.instance, row) + } +} +// ANCHOR_END: instructions-impl + +impl NumericInstructions for AddChip { + type Num = Number; + + fn load_unblinded( + &self, + mut layouter: impl Layouter, + values: &[Value], + ) -> Result, Error> { + let config = self.config(); + + layouter.assign_region( + || "load unblinded", + |mut region| { + values + .iter() + .enumerate() + .map(|(i, value)| { + region + .assign_advice(|| "unblinded input", config.advice[0], i, || *value) + .map(Number) + }) + .collect() + }, + ) + } + + fn mul( + &self, + _: impl Layouter, + _: &[Self::Num], + _: &[Self::Num], + ) -> Result, Error> { + panic!("Not implemented") + } + + fn add( + &self, + mut layouter: impl Layouter, + a: &[Self::Num], + b: &[Self::Num], + ) -> Result, Error> { + let config = self.config(); + assert_eq!(a.len(), b.len()); + + layouter.assign_region( + || "add", + |mut region: Region<'_, F>| { + a.iter() + .zip(b.iter()) + .enumerate() + .map(|(i, (a, b))| { + config.s.enable(&mut region, i)?; + + a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?; + b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?; + + let value = a.0.value().copied() + b.0.value(); + + // Finally, we do the assignment to the output, returning a + // variable to be used in another part of the circuit. + region + .assign_advice(|| "lhs + rhs", config.advice[2], i, || value) + .map(Number) + }) + .collect() + }, + ) + } + + fn expose_public( + &self, + mut layouter: impl Layouter, + num: &Self::Num, + row: usize, + ) -> Result<(), Error> { + let config = self.config(); + + layouter.constrain_instance(num.0.cell(), config.instance, row) + } +} + +#[derive(Default)] +struct MulCircuit { + a: Vec>, + b: Vec>, +} + +impl Circuit for MulCircuit { + // Since we are using a single chip for everything, we can just reuse its config. + type Config = FieldConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn without_witnesses(&self) -> Self { + Self::default() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + // We create the three advice columns that FieldChip uses for I/O. + let advice = [ + meta.unblinded_advice_column(), + meta.unblinded_advice_column(), + meta.unblinded_advice_column(), + ]; + + // We also need an instance column to store public inputs. + let instance = meta.instance_column(); + + MultChip::configure(meta, advice, instance) + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let field_chip = MultChip::::construct(config); + + // Load our unblinded values into the circuit. + let a = field_chip.load_unblinded(layouter.namespace(|| "load a"), &self.a)?; + let b = field_chip.load_unblinded(layouter.namespace(|| "load b"), &self.b)?; + + let ab = field_chip.mul(layouter.namespace(|| "a * b"), &a, &b)?; + + for (i, c) in ab.iter().enumerate() { + // Expose the result as a public input to the circuit. + field_chip.expose_public(layouter.namespace(|| "expose c"), c, i)?; + } + Ok(()) + } +} +// ANCHOR_END: circuit + +#[derive(Default)] +struct AddCircuit { + a: Vec>, + b: Vec>, +} + +impl Circuit for AddCircuit { + // Since we are using a single chip for everything, we can just reuse its config. + type Config = FieldConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn without_witnesses(&self) -> Self { + Self::default() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + // We create the three advice columns that FieldChip uses for I/O. + let advice = [ + meta.unblinded_advice_column(), + meta.unblinded_advice_column(), + meta.unblinded_advice_column(), + ]; + + // We also need an instance column to store public inputs. + let instance = meta.instance_column(); + + AddChip::configure(meta, advice, instance) + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let field_chip = AddChip::::construct(config); + + // Load our unblinded values into the circuit. + let a = field_chip.load_unblinded(layouter.namespace(|| "load a"), &self.a)?; + let b = field_chip.load_unblinded(layouter.namespace(|| "load b"), &self.b)?; + + let ab = field_chip.add(layouter.namespace(|| "a + b"), &a, &b)?; + + for (i, c) in ab.iter().enumerate() { + // Expose the result as a public input to the circuit. + field_chip.expose_public(layouter.namespace(|| "expose c"), c, i)?; + } + Ok(()) + } +} +// ANCHOR_END: circuit + +fn test_prover( + k: u32, + circuit: impl Circuit, + expected: bool, + instances: Vec, +) -> Vec +where + C::Scalar: FromUniformBytes<64>, +{ + let params = ParamsIPA::::new(k); + let vk = keygen_vk(¶ms, &circuit).unwrap(); + let pk = keygen_pk(¶ms, vk, &circuit).unwrap(); + + let proof = { + let mut transcript = Blake2bWrite::<_, _, Challenge255<_>>::init(vec![]); + + create_proof::, ProverIPA, _, _, _, _>( + ¶ms, + &pk, + &[circuit], + &[&[&instances]], + OsRng, + &mut transcript, + ) + .expect("proof generation should not fail"); + + transcript.finalize() + }; + + let accepted = { + let strategy = AccumulatorStrategy::new(¶ms); + let mut transcript = Blake2bRead::<_, _, Challenge255<_>>::init(&proof[..]); + + verify_proof::, VerifierIPA, _, _, _>( + ¶ms, + pk.get_vk(), + strategy, + &[&[&instances]], + &mut transcript, + ) + .map(|strategy| strategy.finalize()) + .unwrap_or_default() + }; + + assert_eq!(accepted, expected); + + proof +} + +fn main() { + use halo2curves::pasta::Fp; + + const N: usize = 10; + // ANCHOR: test-circuit + // The number of rows in our circuit cannot exceed 2^k. Since our example + // circuit is very small, we can pick a very small value here. + let k = 7; + + // Prepare the inputs to the circuit! + let a = [Fp::from(2); N]; + let b = [Fp::from(3); N]; + let c_mul: Vec = a.iter().zip(b).map(|(&a, b)| a * b).collect(); + let c_add: Vec = a.iter().zip(b).map(|(&a, b)| a + b).collect(); + + // Instantiate the mul circuit with the inputs. + let mul_circuit = MulCircuit { + a: a.iter().map(|&x| Value::known(x)).collect(), + b: b.iter().map(|&x| Value::known(x)).collect(), + }; + + // Instantiate the add circuit with the inputs. + let add_circuit = AddCircuit { + a: a.iter().map(|&x| Value::known(x)).collect(), + b: b.iter().map(|&x| Value::known(x)).collect(), + }; + + // the commitments will be the first columns of the proof transcript so we can compare them easily + let proof_1 = test_prover::(k, mul_circuit, true, c_mul); + // the commitments will be the first columns of the proof transcript so we can compare them easily + let proof_2 = test_prover::(k, add_circuit, true, c_add); + + // the commitments will be the first columns of the proof transcript so we can compare them easily + // here we compare the first 10 bytes of the commitments + println!( + "Commitments are equal: {:?}", + proof_1[..10] == proof_2[..10] + ); + // ANCHOR_END: test-circuit +} diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index 2a43bf0958..cd0d7306a9 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -356,7 +356,7 @@ where // Add blinding factors to advice columns for (column_index, advice_values) in column_indices.iter().zip(&mut advice_values) { - if witness.unblinded_advice.contains(column_index) { + if !witness.unblinded_advice.contains(column_index) { for cell in &mut advice_values[unusable_rows_start..] { *cell = Scheme::Scalar::random(&mut rng); } From 41523d67c6c662281952179b0c675159d11e5e3d Mon Sep 17 00:00:00 2001 From: dante <45801863+alexander-camuto@users.noreply.github.com> Date: Tue, 7 Nov 2023 14:45:42 +0000 Subject: [PATCH 11/11] Update circuit.rs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Carlos Pérez <37264926+CPerezz@users.noreply.github.com> --- halo2_proofs/src/plonk/circuit.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 82cb0df08f..cce39c8115 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -2153,7 +2153,7 @@ impl ConstraintSystem { self.advice_column_in(FirstPhase) } - /// Allocate a new unblinded advice column in given phase. The allows for the generation of deterministic commitments to advice columns + /// Allocate a new unblinded advice column in given phase. This allows for the generation of deterministic commitments to advice columns /// which can be used to split large circuits into smaller ones, whose proofs can then be "joined" together by their common witness commitments. pub fn unblinded_advice_column_in(&mut self, phase: P) -> Column { let phase = phase.to_sealed();