From 182c7018411e00b38f194e145ca8959dc782b63a Mon Sep 17 00:00:00 2001 From: guorong009 Date: Tue, 6 Aug 2024 04:55:40 +0800 Subject: [PATCH 01/17] chore: add unit test for TracingFloorPlanner --- halo2_frontend/Cargo.toml | 3 + halo2_frontend/src/dev.rs | 119 +++++++++++++++++++++++++++++++++++++- 2 files changed, 121 insertions(+), 1 deletion(-) diff --git a/halo2_frontend/Cargo.toml b/halo2_frontend/Cargo.toml index 1dd4a2a2d..926c3a159 100644 --- a/halo2_frontend/Cargo.toml +++ b/halo2_frontend/Cargo.toml @@ -43,6 +43,9 @@ tabbycat = { version = "0.1", features = ["attributes"], optional = true } proptest = "1" rand_core = { version = "0.6", default-features = false, features = ["getrandom"] } serde_json = "1" +tracing-subscriber = { version = "0.3" } +tracing = "0.1" +tracing-capture = "0.1" [target.'cfg(all(target_arch = "wasm32", target_os = "unknown"))'.dev-dependencies] getrandom = { version = "0.2", features = ["js"] } diff --git a/halo2_frontend/src/dev.rs b/halo2_frontend/src/dev.rs index 2958a3202..b24a5c25c 100644 --- a/halo2_frontend/src/dev.rs +++ b/halo2_frontend/src/dev.rs @@ -1258,7 +1258,7 @@ mod tests { use super::{FailureLocation, MockProver, VerifyFailure}; use crate::circuit::{Layouter, SimpleFloorPlanner, Value}; - use crate::dev::{CellValue, InstanceValue}; + use crate::dev::{CellValue, InstanceValue, TracingFloorPlanner}; use crate::plonk::{ Advice, Circuit, Column, ConstraintSystem, Error, Expression, Fixed, Instance, Selector, TableColumn, @@ -2256,4 +2256,121 @@ mod tests { // if this verifies correctly -> we have an issue and we are missing a range check assert_eq!(prover.verify(), Ok(())); } + + #[test] + fn test_tracing_floor_planner() { + use tracing_capture::{CaptureLayer, SharedStorage}; + use tracing_subscriber::layer::SubscriberExt; + + const K: u32 = 4; + + #[derive(Clone)] + struct TestCircuitConfig { + a: Column, + b: Column, + c: Column, + d: Column, + q: Selector, + } + + struct TestCircuit {} + + impl Circuit for TestCircuit { + type Config = TestCircuitConfig; + type FloorPlanner = TracingFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let b = meta.advice_column(); + let c = meta.advice_column(); + let d = meta.fixed_column(); + let q = meta.selector(); + + meta.create_gate("Equality check", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let b = cells.query_advice(b, Rotation::cur()); + let c = cells.query_advice(c, Rotation::cur()); + let d = cells.query_fixed(d, Rotation::cur()); + let q = cells.query_selector(q); + + // If q is enabled, a and b must be assigned to. + vec![q * (a - b) * (c - d)] + }); + + TestCircuitConfig { a, b, c, d, q } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "Correct synthesis", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Assign b = 1. + region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?; + + // Assign c = 5. + region.assign_advice( + || "c", + config.c, + 0, + || Value::known(Fp::from(5u64)), + )?; + // Assign d = 7. + region.assign_fixed( + || "d", + config.d, + 0, + || Value::known(Fp::from(7u64)), + )?; + Ok(()) + }, + )?; + + Ok(()) + } + } + + // // At the start of your test, enable tracing. + // tracing_subscriber::fmt() + // .with_max_level(tracing::Level::DEBUG) + // .with_ansi(false) + // .without_time() + // .init(); + + let subscriber = tracing_subscriber::fmt() + .with_max_level(tracing::Level::DEBUG) + .with_ansi(false) + .without_time() + .finish(); + let storage = SharedStorage::default(); + let subscriber = subscriber.with(CaptureLayer::new(&storage)); + tracing::subscriber::set_global_default(subscriber).unwrap(); + + // run the prover to check if every step is traced. + let prover = MockProver::run(K, &TestCircuit {}, vec![]).unwrap(); + assert_eq!(prover.verify(), Ok(())); + + // check if all tracing logs are captured + let storage = storage.lock(); + assert_eq!(storage.all_spans().len(), 12); + for span in storage.all_spans() { + let metadata = span.metadata(); + assert_eq!(*metadata.level(), tracing::Level::DEBUG); + } + } } From d299460e22050b2ae6401011a9dbbc1dd242df15 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Tue, 6 Aug 2024 10:21:21 +0800 Subject: [PATCH 02/17] chore: add unit test for "CircuitGates" --- halo2_frontend/src/dev.rs | 65 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 64 insertions(+), 1 deletion(-) diff --git a/halo2_frontend/src/dev.rs b/halo2_frontend/src/dev.rs index b24a5c25c..31c9248dc 100644 --- a/halo2_frontend/src/dev.rs +++ b/halo2_frontend/src/dev.rs @@ -1258,7 +1258,7 @@ mod tests { use super::{FailureLocation, MockProver, VerifyFailure}; use crate::circuit::{Layouter, SimpleFloorPlanner, Value}; - use crate::dev::{CellValue, InstanceValue, TracingFloorPlanner}; + use crate::dev::{CellValue, CircuitGates, InstanceValue, TracingFloorPlanner}; use crate::plonk::{ Advice, Circuit, Column, ConstraintSystem, Error, Expression, Fixed, Instance, Selector, TableColumn, @@ -2373,4 +2373,67 @@ mod tests { assert_eq!(*metadata.level(), tracing::Level::DEBUG); } } + + #[test] + fn test_gates() { + #[derive(Clone)] + struct TestCircuitConfig { + a: Column, + b: Column, + c: Column, + d: Column, + q: Selector, + } + + struct TestCircuit {} + + impl Circuit for TestCircuit { + type Config = TestCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let b = meta.advice_column(); + let c = meta.advice_column(); + let d = meta.fixed_column(); + let q = meta.selector(); + + meta.create_gate("Equality check", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let b = cells.query_advice(b, Rotation::cur()); + let c = cells.query_advice(c, Rotation::cur()); + let d = cells.query_fixed(d, Rotation::cur()); + let q = cells.query_selector(q); + + // If q is enabled, a and b must be assigned to. + vec![q * (a - b) * (c - d)] + }); + + TestCircuitConfig { a, b, c, d, q } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize(&self, _: Self::Config, _: impl Layouter) -> Result<(), Error> { + unreachable!(); + } + } + + let gates = CircuitGates::collect::(); + assert_eq!( + format!("{}", gates), + r#####"Equality check: +- (S0 * (A0@0 - A1@0)) * (A2@0 - F0@0) +Total gates: 1 +Total custom constraint polynomials: 1 +Total negations: 2 +Total additions: 2 +Total multiplications: 2 +"##### + ) + } } From 17a3f072160c5a40397d4dac3448b89389cc50a4 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Tue, 6 Aug 2024 10:34:41 +0800 Subject: [PATCH 03/17] refactor: move unit tests to own files --- halo2_frontend/src/dev.rs | 182 +------------------------------- halo2_frontend/src/dev/gates.rs | 77 ++++++++++++++ halo2_frontend/src/dev/tfp.rs | 127 ++++++++++++++++++++++ 3 files changed, 205 insertions(+), 181 deletions(-) diff --git a/halo2_frontend/src/dev.rs b/halo2_frontend/src/dev.rs index 31c9248dc..2958a3202 100644 --- a/halo2_frontend/src/dev.rs +++ b/halo2_frontend/src/dev.rs @@ -1258,7 +1258,7 @@ mod tests { use super::{FailureLocation, MockProver, VerifyFailure}; use crate::circuit::{Layouter, SimpleFloorPlanner, Value}; - use crate::dev::{CellValue, CircuitGates, InstanceValue, TracingFloorPlanner}; + use crate::dev::{CellValue, InstanceValue}; use crate::plonk::{ Advice, Circuit, Column, ConstraintSystem, Error, Expression, Fixed, Instance, Selector, TableColumn, @@ -2256,184 +2256,4 @@ mod tests { // if this verifies correctly -> we have an issue and we are missing a range check assert_eq!(prover.verify(), Ok(())); } - - #[test] - fn test_tracing_floor_planner() { - use tracing_capture::{CaptureLayer, SharedStorage}; - use tracing_subscriber::layer::SubscriberExt; - - const K: u32 = 4; - - #[derive(Clone)] - struct TestCircuitConfig { - a: Column, - b: Column, - c: Column, - d: Column, - q: Selector, - } - - struct TestCircuit {} - - impl Circuit for TestCircuit { - type Config = TestCircuitConfig; - type FloorPlanner = TracingFloorPlanner; - #[cfg(feature = "circuit-params")] - type Params = (); - - fn configure(meta: &mut ConstraintSystem) -> Self::Config { - let a = meta.advice_column(); - let b = meta.advice_column(); - let c = meta.advice_column(); - let d = meta.fixed_column(); - let q = meta.selector(); - - meta.create_gate("Equality check", |cells| { - let a = cells.query_advice(a, Rotation::cur()); - let b = cells.query_advice(b, Rotation::cur()); - let c = cells.query_advice(c, Rotation::cur()); - let d = cells.query_fixed(d, Rotation::cur()); - let q = cells.query_selector(q); - - // If q is enabled, a and b must be assigned to. - vec![q * (a - b) * (c - d)] - }); - - TestCircuitConfig { a, b, c, d, q } - } - - fn without_witnesses(&self) -> Self { - Self {} - } - - fn synthesize( - &self, - config: Self::Config, - mut layouter: impl Layouter, - ) -> Result<(), Error> { - layouter.assign_region( - || "Correct synthesis", - |mut region| { - // Enable the equality gate. - config.q.enable(&mut region, 0)?; - - // Assign a = 1. - region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; - - // Assign b = 1. - region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?; - - // Assign c = 5. - region.assign_advice( - || "c", - config.c, - 0, - || Value::known(Fp::from(5u64)), - )?; - // Assign d = 7. - region.assign_fixed( - || "d", - config.d, - 0, - || Value::known(Fp::from(7u64)), - )?; - Ok(()) - }, - )?; - - Ok(()) - } - } - - // // At the start of your test, enable tracing. - // tracing_subscriber::fmt() - // .with_max_level(tracing::Level::DEBUG) - // .with_ansi(false) - // .without_time() - // .init(); - - let subscriber = tracing_subscriber::fmt() - .with_max_level(tracing::Level::DEBUG) - .with_ansi(false) - .without_time() - .finish(); - let storage = SharedStorage::default(); - let subscriber = subscriber.with(CaptureLayer::new(&storage)); - tracing::subscriber::set_global_default(subscriber).unwrap(); - - // run the prover to check if every step is traced. - let prover = MockProver::run(K, &TestCircuit {}, vec![]).unwrap(); - assert_eq!(prover.verify(), Ok(())); - - // check if all tracing logs are captured - let storage = storage.lock(); - assert_eq!(storage.all_spans().len(), 12); - for span in storage.all_spans() { - let metadata = span.metadata(); - assert_eq!(*metadata.level(), tracing::Level::DEBUG); - } - } - - #[test] - fn test_gates() { - #[derive(Clone)] - struct TestCircuitConfig { - a: Column, - b: Column, - c: Column, - d: Column, - q: Selector, - } - - struct TestCircuit {} - - impl Circuit for TestCircuit { - type Config = TestCircuitConfig; - type FloorPlanner = SimpleFloorPlanner; - #[cfg(feature = "circuit-params")] - type Params = (); - - fn configure(meta: &mut ConstraintSystem) -> Self::Config { - let a = meta.advice_column(); - let b = meta.advice_column(); - let c = meta.advice_column(); - let d = meta.fixed_column(); - let q = meta.selector(); - - meta.create_gate("Equality check", |cells| { - let a = cells.query_advice(a, Rotation::cur()); - let b = cells.query_advice(b, Rotation::cur()); - let c = cells.query_advice(c, Rotation::cur()); - let d = cells.query_fixed(d, Rotation::cur()); - let q = cells.query_selector(q); - - // If q is enabled, a and b must be assigned to. - vec![q * (a - b) * (c - d)] - }); - - TestCircuitConfig { a, b, c, d, q } - } - - fn without_witnesses(&self) -> Self { - Self {} - } - - fn synthesize(&self, _: Self::Config, _: impl Layouter) -> Result<(), Error> { - unreachable!(); - } - } - - let gates = CircuitGates::collect::(); - assert_eq!( - format!("{}", gates), - r#####"Equality check: -- (S0 * (A0@0 - A1@0)) * (A2@0 - F0@0) -Total gates: 1 -Total custom constraint polynomials: 1 -Total negations: 2 -Total additions: 2 -Total multiplications: 2 -"##### - ) - } } diff --git a/halo2_frontend/src/dev/gates.rs b/halo2_frontend/src/dev/gates.rs index 5c48bbed4..b2682c111 100644 --- a/halo2_frontend/src/dev/gates.rs +++ b/halo2_frontend/src/dev/gates.rs @@ -308,3 +308,80 @@ impl fmt::Display for CircuitGates { writeln!(f, "Total multiplications: {}", self.total_multiplications) } } + +#[cfg(test)] +mod tests { + use halo2_middleware::poly::Rotation; + use halo2curves::pasta::Fp; + + use crate::{ + circuit::{Layouter, SimpleFloorPlanner}, + plonk::{Advice, Column, Error, Fixed, Selector}, + }; + + use super::*; + + #[test] + fn test_circuit_gates() { + #[allow(unused)] + #[derive(Clone)] + struct TestCircuitConfig { + a: Column, + b: Column, + c: Column, + d: Column, + q: Selector, + } + + struct TestCircuit {} + + impl Circuit for TestCircuit { + type Config = TestCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let b = meta.advice_column(); + let c = meta.advice_column(); + let d = meta.fixed_column(); + let q = meta.selector(); + + meta.create_gate("Equality check", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let b = cells.query_advice(b, Rotation::cur()); + let c = cells.query_advice(c, Rotation::cur()); + let d = cells.query_fixed(d, Rotation::cur()); + let q = cells.query_selector(q); + + // If q is enabled, a and b must be assigned to. + vec![q * (a - b) * (c - d)] + }); + + TestCircuitConfig { a, b, c, d, q } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize(&self, _: Self::Config, _: impl Layouter) -> Result<(), Error> { + unreachable!(); + } + } + + let gates = CircuitGates::collect::(); + assert_eq!( + format!("{}", gates), + r#####"Equality check: +- (S0 * (A0@0 - A1@0)) * (A2@0 - F0@0) +Total gates: 1 +Total custom constraint polynomials: 1 +Total negations: 2 +Total additions: 2 +Total multiplications: 2 +"##### + ) + } +} diff --git a/halo2_frontend/src/dev/tfp.rs b/halo2_frontend/src/dev/tfp.rs index 0d02d1d2b..fa492f52e 100644 --- a/halo2_frontend/src/dev/tfp.rs +++ b/halo2_frontend/src/dev/tfp.rs @@ -509,3 +509,130 @@ impl<'cs, F: Field, CS: Assignment> Assignment for TracingAssignment<'cs, // We exit namespace spans in TracingLayouter. } } + +#[cfg(test)] +mod tests { + use halo2_middleware::poly::Rotation; + use halo2curves::pasta::Fp; + + use crate::{circuit::SimpleFloorPlanner, dev::MockProver}; + + use super::*; + + #[test] + fn test_tracing_floor_planner() { + use tracing_capture::{CaptureLayer, SharedStorage}; + use tracing_subscriber::layer::SubscriberExt; + + const K: u32 = 4; + + #[derive(Clone)] + struct TestCircuitConfig { + a: Column, + b: Column, + c: Column, + d: Column, + q: Selector, + } + + struct TestCircuit {} + + impl Circuit for TestCircuit { + type Config = TestCircuitConfig; + type FloorPlanner = TracingFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let b = meta.advice_column(); + let c = meta.advice_column(); + let d = meta.fixed_column(); + let q = meta.selector(); + + meta.create_gate("Equality check", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let b = cells.query_advice(b, Rotation::cur()); + let c = cells.query_advice(c, Rotation::cur()); + let d = cells.query_fixed(d, Rotation::cur()); + let q = cells.query_selector(q); + + // If q is enabled, a and b must be assigned to. + vec![q * (a - b) * (c - d)] + }); + + TestCircuitConfig { a, b, c, d, q } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "Correct synthesis", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Assign b = 1. + region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?; + + // Assign c = 5. + region.assign_advice( + || "c", + config.c, + 0, + || Value::known(Fp::from(5u64)), + )?; + // Assign d = 7. + region.assign_fixed( + || "d", + config.d, + 0, + || Value::known(Fp::from(7u64)), + )?; + Ok(()) + }, + )?; + + Ok(()) + } + } + + // // At the start of your test, enable tracing. + // tracing_subscriber::fmt() + // .with_max_level(tracing::Level::DEBUG) + // .with_ansi(false) + // .without_time() + // .init(); + + let subscriber = tracing_subscriber::fmt() + .with_max_level(tracing::Level::DEBUG) + .with_ansi(false) + .without_time() + .finish(); + let storage = SharedStorage::default(); + let subscriber = subscriber.with(CaptureLayer::new(&storage)); + tracing::subscriber::set_global_default(subscriber).unwrap(); + + // run the prover to check if every step is traced. + let prover = MockProver::run(K, &TestCircuit {}, vec![]).unwrap(); + assert_eq!(prover.verify(), Ok(())); + + // check if all tracing logs are captured + let storage = storage.lock(); + assert_eq!(storage.all_spans().len(), 12); + for span in storage.all_spans() { + let metadata = span.metadata(); + assert_eq!(*metadata.level(), tracing::Level::DEBUG); + } + } +} From 671a802a0c7b49712e1c9460181adc62c9445544 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Tue, 6 Aug 2024 11:29:05 +0800 Subject: [PATCH 04/17] chore: add some test for "failure" mod --- halo2_frontend/src/dev/failure.rs | 285 ++++++++++++++++++++++++++++++ 1 file changed, 285 insertions(+) diff --git a/halo2_frontend/src/dev/failure.rs b/halo2_frontend/src/dev/failure.rs index a11d382af..4e8199513 100644 --- a/halo2_frontend/src/dev/failure.rs +++ b/halo2_frontend/src/dev/failure.rs @@ -876,3 +876,288 @@ impl VerifyFailure { } } } + +#[cfg(test)] +mod tests { + use halo2_middleware::poly::Rotation; + use halo2curves::pasta::Fp; + + use crate::{ + circuit::{Layouter, SimpleFloorPlanner, Value}, + plonk::{Advice, Circuit, Error, Fixed, Selector}, + }; + + use super::*; + + #[test] + fn test_failure_constraint_not_satisfied() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + a: Column, + b: Column, + c: Column, + d: Column, + q: Selector, + } + + struct FaultyCircuit {} + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let b = meta.advice_column(); + let c = meta.advice_column(); + let d = meta.fixed_column(); + let q = meta.selector(); + + meta.create_gate("Equality check", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let b = cells.query_advice(b, Rotation::cur()); + let c = cells.query_advice(c, Rotation::cur()); + let d = cells.query_fixed(d, Rotation::cur()); + let q = cells.query_selector(q); + + // If q is enabled, a and b must be assigned to. + vec![q * (a - b) * (c - d)] + }); + + FaultyCircuitConfig { a, b, c, d, q } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "Correct synthesis", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Assign b = 1. + region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?; + + // Assign c = 5. + region.assign_advice( + || "c", + config.c, + 0, + || Value::known(Fp::from(5u64)), + )?; + // Assign d = 7. + region.assign_fixed( + || "d", + config.d, + 0, + || Value::known(Fp::from(7u64)), + )?; + Ok(()) + }, + )?; + layouter.assign_region( + || "Wrong synthesis", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Assign b = 0. + region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::zero()))?; + + // Name Column a + region.name_column(|| "This is Advice!", config.a); + // Name Column b + region.name_column(|| "This is Advice too!", config.b); + + // Assign c = 5. + region.assign_advice( + || "c", + config.c, + 0, + || Value::known(Fp::from(5u64)), + )?; + // Assign d = 7. + region.assign_fixed( + || "d", + config.d, + 0, + || Value::known(Fp::from(7u64)), + )?; + + // Name Column c + region.name_column(|| "Another one!", config.c); + // Name Column d + region.name_column(|| "This is a Fixed!", config.d); + + // Note that none of the terms cancel eachother. Therefore we will have a constraint that is non satisfied for + // the `Equalty check` gate. + Ok(()) + }, + ) + } + } + + let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); + let errs = prover.verify().unwrap_err(); + + assert_eq!(errs.len(), 1); + assert_eq!( + format!("{}", errs[0]), + r#####"Constraint 0 in gate 0 ('Equality check') is not satisfied in Region 1 ('Wrong synthesis') at offset 0 +- Column('Advice', 0 - This is Advice!)@0 = 1 +- Column('Advice', 1 - This is Advice too!)@0 = 0 +- Column('Advice', 2 - Another one!)@0 = 0x5 +- Column('Fixed', 0 - This is a Fixed!)@0 = 0x7 +"##### + ); + } + + #[test] + fn test_failure_cell_not_assigned() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + a: Column, + b: Column, + c: Column, + d: Column, + q: Selector, + } + + struct FaultyCircuit {} + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let b = meta.advice_column(); + let c = meta.advice_column(); + let d = meta.fixed_column(); + let q = meta.selector(); + + meta.create_gate("Equality check", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let b = cells.query_advice(b, Rotation::cur()); + let c = cells.query_advice(c, Rotation::cur()); + let d = cells.query_fixed(d, Rotation::cur()); + let q = cells.query_selector(q); + + // If q is enabled, a and b must be assigned to. + vec![q * (a - b) * (c - d)] + }); + + FaultyCircuitConfig { a, b, c, d, q } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "Correct synthesis", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Assign b = 1. + region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?; + + // Assign c = 5. + region.assign_advice( + || "c", + config.c, + 0, + || Value::known(Fp::from(5u64)), + )?; + // Assign d = 7. + region.assign_fixed( + || "d", + config.d, + 0, + || Value::known(Fp::from(7u64)), + )?; + Ok(()) + }, + )?; + layouter.assign_region( + || "Wrong synthesis", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Name Column a + region.name_column(|| "This is Advice!", config.a); + // Name Column b + region.name_column(|| "This is Advice too!", config.b); + + // Assign c = 5. + region.assign_advice( + || "c", + config.c, + 0, + || Value::known(Fp::from(5u64)), + )?; + // Assign d = 7. + region.assign_fixed( + || "d", + config.d, + 0, + || Value::known(Fp::from(7u64)), + )?; + + // Name Column c + region.name_column(|| "Another one!", config.c); + // Name Column d + region.name_column(|| "This is a Fixed!", config.d); + + // Note that none of the terms cancel eachother. Therefore we will have a constraint that is non satisfied for + // the `Equalty check` gate. + Ok(()) + }, + ) + } + } + + let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); + let errs = prover.verify().unwrap_err(); + + assert_eq!(errs.len(), 2); + assert_eq!( + format!("{}", errs[0]), + r#####"Region 1 ('Wrong synthesis') uses Gate 0 ('Equality check') at offset 1, which requires cell in column Column { index: 1, column_type: Advice } at offset 0 with annotation Some("This is Advice too!") to be assigned."##### + ); + } +} From 5d6bfdb483fca9d744913f1fa5e3d566eec24713 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Tue, 6 Aug 2024 11:38:45 +0800 Subject: [PATCH 05/17] chore: fix codecov warning --- halo2_frontend/src/dev/gates.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/halo2_frontend/src/dev/gates.rs b/halo2_frontend/src/dev/gates.rs index b2682c111..b95cbd955 100644 --- a/halo2_frontend/src/dev/gates.rs +++ b/halo2_frontend/src/dev/gates.rs @@ -338,8 +338,6 @@ mod tests { impl Circuit for TestCircuit { type Config = TestCircuitConfig; type FloorPlanner = SimpleFloorPlanner; - #[cfg(feature = "circuit-params")] - type Params = (); fn configure(meta: &mut ConstraintSystem) -> Self::Config { let a = meta.advice_column(); From c1e35f7a2579bcf29352d89129d1be30d7f08729 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Tue, 6 Aug 2024 11:44:45 +0800 Subject: [PATCH 06/17] chore: another try for codecov warning --- halo2_frontend/src/dev/gates.rs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/halo2_frontend/src/dev/gates.rs b/halo2_frontend/src/dev/gates.rs index b95cbd955..6ca620463 100644 --- a/halo2_frontend/src/dev/gates.rs +++ b/halo2_frontend/src/dev/gates.rs @@ -338,6 +338,8 @@ mod tests { impl Circuit for TestCircuit { type Config = TestCircuitConfig; type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); fn configure(meta: &mut ConstraintSystem) -> Self::Config { let a = meta.advice_column(); @@ -369,7 +371,10 @@ mod tests { } } - let gates = CircuitGates::collect::(); + let gates = CircuitGates::collect::( + #[cfg(feature = "circuit-params")] + (), + ); assert_eq!( format!("{}", gates), r#####"Equality check: From e80703edd2368a6b60130968dfcbf3516f5bc029 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Wed, 7 Aug 2024 21:33:55 +0800 Subject: [PATCH 07/17] chore: remove unused pub --- halo2_middleware/src/expression.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2_middleware/src/expression.rs b/halo2_middleware/src/expression.rs index 1cbb557ed..91d0feb30 100644 --- a/halo2_middleware/src/expression.rs +++ b/halo2_middleware/src/expression.rs @@ -65,7 +65,7 @@ impl Expression { } } - pub fn write_identifier(&self, writer: &mut W) -> std::io::Result<()> { + fn write_identifier(&self, writer: &mut W) -> std::io::Result<()> { match self { Expression::Constant(scalar) => write!(writer, "{scalar:?}"), Expression::Var(v) => v.write_identifier(writer), From d665a5e64521f112aafb8ae4f9cb30c4345b212b Mon Sep 17 00:00:00 2001 From: guorong009 Date: Wed, 7 Aug 2024 22:07:09 +0800 Subject: [PATCH 08/17] chore: add identifier test for frontend expression --- .../src/plonk/circuit/expression.rs | 47 +++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/halo2_frontend/src/plonk/circuit/expression.rs b/halo2_frontend/src/plonk/circuit/expression.rs index 3a991d198..a6560063f 100644 --- a/halo2_frontend/src/plonk/circuit/expression.rs +++ b/halo2_frontend/src/plonk/circuit/expression.rs @@ -1097,7 +1097,10 @@ impl Product for Expression { #[cfg(test)] mod tests { + use crate::plonk::{AdviceQuery, FixedQuery, Selector}; + use super::Expression; + use halo2_middleware::poly::Rotation; use halo2curves::bn256::Fr; #[test] @@ -1137,4 +1140,48 @@ mod tests { assert_eq!(happened, expected); } + + #[test] + fn identifier() { + let sum_expr: Expression = Expression::Sum( + Box::new(Expression::Constant(1.into())), + Box::new(Expression::Constant(2.into())), + ); + assert_eq!(sum_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001+0x0000000000000000000000000000000000000000000000000000000000000002)"); + + let prod_expr: Expression = Expression::Product( + Box::new(Expression::Constant(1.into())), + Box::new(Expression::Constant(2.into())), + ); + assert_eq!(prod_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001*0x0000000000000000000000000000000000000000000000000000000000000002)"); + + let scaled_expr: Expression = + Expression::Scaled(Box::new(Expression::Constant(1.into())), 100.into()); + assert_eq!(scaled_expr.identifier(), "0x0000000000000000000000000000000000000000000000000000000000000001*0x0000000000000000000000000000000000000000000000000000000000000064"); + + // simulate the expressions being used in a circuit + let l: Expression = Expression::Advice(AdviceQuery { + index: None, + column_index: 0, + rotation: Rotation::cur(), + }); + let r: Expression = Expression::Advice(AdviceQuery { + index: None, + column_index: 1, + rotation: Rotation::cur(), + }); + let o: Expression = Expression::Advice(AdviceQuery { + index: None, + column_index: 2, + rotation: Rotation::cur(), + }); + let sl: Expression = Expression::Selector(Selector(0, false)); + let sr: Expression = Expression::Selector(Selector(1, false)); + let sm: Expression = Expression::Selector(Selector(2, false)); + let so: Expression = Expression::Selector(Selector(3, false)); + let c: Expression = Expression::Fixed(FixedQuery { index: None, column_index: 0, rotation: Rotation::cur()}); + + let simple_plonk_expr = sl * l.clone() + sr * r.clone() + sm * (l * r) - so * o + c; + assert_eq!(simple_plonk_expr.identifier(), "(((((selector[0]*advice[0][0])+(selector[1]*advice[1][0]))+(selector[2]*(advice[0][0]*advice[1][0])))+(-(selector[3]*advice[2][0])))+fixed[0][0])"); + } } From d6855653166014582642ef61a701884942c7d8a4 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Wed, 7 Aug 2024 22:30:22 +0800 Subject: [PATCH 09/17] chore: add unit tests for "Expression*" --- halo2_backend/src/plonk/circuit.rs | 114 ++++++++++++++++++ .../src/plonk/circuit/expression.rs | 8 +- halo2_middleware/src/expression.rs | 96 +++++++++++++++ 3 files changed, 216 insertions(+), 2 deletions(-) diff --git a/halo2_backend/src/plonk/circuit.rs b/halo2_backend/src/plonk/circuit.rs index a754bf4bf..cd7c6c663 100644 --- a/halo2_backend/src/plonk/circuit.rs +++ b/halo2_backend/src/plonk/circuit.rs @@ -366,3 +366,117 @@ fn shuffle_argument_required_degree(arg: &shuffle::Argume // (1 - (l_last + l_blind)) (z(\omega X) (s(X) + \gamma) - z(X) (a(X) + \gamma)) std::cmp::max(2 + shuffle_degree, 2 + input_degree) } + +#[cfg(test)] +mod tests { + use super::{Any, ExpressionBack, QueryBack, VarBack}; + + use halo2_middleware::poly::Rotation; + use halo2curves::bn256::Fr; + + #[test] + fn expressionback_iter_sum() { + let exprs: Vec> = vec![ + ExpressionBack::Constant(1.into()), + ExpressionBack::Constant(2.into()), + ExpressionBack::Constant(3.into()), + ]; + let happened: ExpressionBack = exprs.into_iter().sum(); + let expected: ExpressionBack = ExpressionBack::Sum( + Box::new(ExpressionBack::Sum( + Box::new(ExpressionBack::Constant(1.into())), + Box::new(ExpressionBack::Constant(2.into())), + )), + Box::new(ExpressionBack::Constant(3.into())), + ); + + assert_eq!(happened, expected); + } + + #[test] + fn expressionback_iter_product() { + let exprs: Vec> = vec![ + ExpressionBack::Constant(1.into()), + ExpressionBack::Constant(2.into()), + ExpressionBack::Constant(3.into()), + ]; + let happened: ExpressionBack = exprs.into_iter().product(); + let expected: ExpressionBack = ExpressionBack::Product( + Box::new(ExpressionBack::Product( + Box::new(ExpressionBack::Constant(1.into())), + Box::new(ExpressionBack::Constant(2.into())), + )), + Box::new(ExpressionBack::Constant(3.into())), + ); + + assert_eq!(happened, expected); + } + + #[test] + fn expressionback_identifier() { + let sum_expr: ExpressionBack = ExpressionBack::Sum( + Box::new(ExpressionBack::Constant(1.into())), + Box::new(ExpressionBack::Constant(2.into())), + ); + assert_eq!(sum_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001+0x0000000000000000000000000000000000000000000000000000000000000002)"); + + let prod_expr: ExpressionBack = ExpressionBack::Product( + Box::new(ExpressionBack::Constant(1.into())), + Box::new(ExpressionBack::Constant(2.into())), + ); + assert_eq!(prod_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001*0x0000000000000000000000000000000000000000000000000000000000000002)"); + + // simulate the expressios being used in a circuit + let l: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { + index: 0, + column_index: 0, + column_type: Any::Advice, + rotation: Rotation::cur(), + })); + let r: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { + index: 1, + column_index: 1, + column_type: Any::Advice, + rotation: Rotation::cur(), + })); + let o: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { + index: 2, + column_index: 2, + column_type: Any::Advice, + rotation: Rotation::cur(), + })); + let c: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { + index: 3, + column_index: 0, + column_type: Any::Fixed, + rotation: Rotation::cur(), + })); + let sl: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { + index: 4, + column_index: 1, + column_type: Any::Fixed, + rotation: Rotation::cur(), + })); + let sr: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { + index: 5, + column_index: 2, + column_type: Any::Fixed, + rotation: Rotation::cur(), + })); + let sm: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { + index: 6, + column_index: 3, + column_type: Any::Fixed, + rotation: Rotation::cur(), + })); + let so: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { + index: 7, + column_index: 4, + column_type: Any::Fixed, + rotation: Rotation::cur(), + })); + + let simple_plonk_expr = sl * l.clone() + sr * r.clone() + sm * (l * r) - so * o + c; + assert_eq!(simple_plonk_expr.identifier(), "(((((Query(QueryBack { index: 4, column_index: 1, column_type: Fixed, rotation: Rotation(0) })*Query(QueryBack { index: 0, column_index: 0, column_type: Advice, rotation: Rotation(0) }))+(Query(QueryBack { index: 5, column_index: 2, column_type: Fixed, rotation: Rotation(0) })*Query(QueryBack { index: 1, column_index: 1, column_type: Advice, rotation: Rotation(0) })))+(Query(QueryBack { index: 6, column_index: 3, column_type: Fixed, rotation: Rotation(0) })*(Query(QueryBack { index: 0, column_index: 0, column_type: Advice, rotation: Rotation(0) })*Query(QueryBack { index: 1, column_index: 1, column_type: Advice, rotation: Rotation(0) }))))+(-(Query(QueryBack { index: 7, column_index: 4, column_type: Fixed, rotation: Rotation(0) })*Query(QueryBack { index: 2, column_index: 2, column_type: Advice, rotation: Rotation(0) }))))+Query(QueryBack { index: 3, column_index: 0, column_type: Fixed, rotation: Rotation(0) }))"); + } +} diff --git a/halo2_frontend/src/plonk/circuit/expression.rs b/halo2_frontend/src/plonk/circuit/expression.rs index a6560063f..31d53bea3 100644 --- a/halo2_frontend/src/plonk/circuit/expression.rs +++ b/halo2_frontend/src/plonk/circuit/expression.rs @@ -1179,8 +1179,12 @@ mod tests { let sr: Expression = Expression::Selector(Selector(1, false)); let sm: Expression = Expression::Selector(Selector(2, false)); let so: Expression = Expression::Selector(Selector(3, false)); - let c: Expression = Expression::Fixed(FixedQuery { index: None, column_index: 0, rotation: Rotation::cur()}); - + let c: Expression = Expression::Fixed(FixedQuery { + index: None, + column_index: 0, + rotation: Rotation::cur(), + }); + let simple_plonk_expr = sl * l.clone() + sr * r.clone() + sm * (l * r) - so * o + c; assert_eq!(simple_plonk_expr.identifier(), "(((((selector[0]*advice[0][0])+(selector[1]*advice[1][0]))+(selector[2]*(advice[0][0]*advice[1][0])))+(-(selector[3]*advice[2][0])))+fixed[0][0])"); } diff --git a/halo2_middleware/src/expression.rs b/halo2_middleware/src/expression.rs index 91d0feb30..e6240d60e 100644 --- a/halo2_middleware/src/expression.rs +++ b/halo2_middleware/src/expression.rs @@ -172,3 +172,99 @@ impl Product for Expression { .unwrap_or(Expression::Constant(F::ONE)) } } + +#[cfg(test)] +mod tests { + + use crate::{ + circuit::{Any, ExpressionMid, QueryMid, VarMid}, + poly::Rotation, + }; + use halo2curves::bn256::Fr; + + #[test] + fn iter_sum() { + let exprs: Vec> = vec![ + ExpressionMid::Constant(1.into()), + ExpressionMid::Constant(2.into()), + ExpressionMid::Constant(3.into()), + ]; + let happened: ExpressionMid = exprs.into_iter().sum(); + let expected: ExpressionMid = ExpressionMid::Sum( + Box::new(ExpressionMid::Sum( + Box::new(ExpressionMid::Constant(1.into())), + Box::new(ExpressionMid::Constant(2.into())), + )), + Box::new(ExpressionMid::Constant(3.into())), + ); + + assert_eq!(happened, expected); + } + + #[test] + fn iter_product() { + let exprs: Vec> = vec![ + ExpressionMid::Constant(1.into()), + ExpressionMid::Constant(2.into()), + ExpressionMid::Constant(3.into()), + ]; + let happened: ExpressionMid = exprs.into_iter().product(); + let expected: ExpressionMid = ExpressionMid::Product( + Box::new(ExpressionMid::Product( + Box::new(ExpressionMid::Constant(1.into())), + Box::new(ExpressionMid::Constant(2.into())), + )), + Box::new(ExpressionMid::Constant(3.into())), + ); + + assert_eq!(happened, expected); + } + + #[test] + fn identifier() { + let sum_expr: ExpressionMid = ExpressionMid::Sum( + Box::new(ExpressionMid::Constant(1.into())), + Box::new(ExpressionMid::Constant(2.into())), + ); + assert_eq!(sum_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001+0x0000000000000000000000000000000000000000000000000000000000000002)"); + + let prod_expr: ExpressionMid = ExpressionMid::Product( + Box::new(ExpressionMid::Constant(1.into())), + Box::new(ExpressionMid::Constant(2.into())), + ); + assert_eq!(prod_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001*0x0000000000000000000000000000000000000000000000000000000000000002)"); + + // simulate the expressios being used in a circuit + let l: ExpressionMid = ExpressionMid::Var(VarMid::Query(QueryMid::new( + Any::Advice, + 0, + Rotation::cur(), + ))); + let r: ExpressionMid = ExpressionMid::Var(VarMid::Query(QueryMid::new( + Any::Advice, + 1, + Rotation::cur(), + ))); + let o: ExpressionMid = ExpressionMid::Var(VarMid::Query(QueryMid::new( + Any::Advice, + 2, + Rotation::cur(), + ))); + let c: ExpressionMid = + ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 0, Rotation::cur()))); + let sl: ExpressionMid = + ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 1, Rotation::cur()))); + let sr: ExpressionMid = + ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 2, Rotation::cur()))); + let sm: ExpressionMid = + ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 3, Rotation::cur()))); + let so: ExpressionMid = + ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 4, Rotation::cur()))); + + let simple_plonk_expr = sl * l.clone() + sr * r.clone() + sm * (l * r) - so * o + c; + assert_eq!( + simple_plonk_expr.identifier(), + "(((((f1*a0)+(f2*a1))+(f3*(a0*a1)))+(-(f4*a2)))+f0)" + ); + } +} From 6dcebb100837e79807cf30d52f316719ab05475f Mon Sep 17 00:00:00 2001 From: guorong009 Date: Thu, 8 Aug 2024 11:10:16 +0800 Subject: [PATCH 10/17] chore: improve unit tests for "frontend/dev/cost" --- halo2_frontend/src/dev/cost.rs | 471 ++++++++++++++++++++++++++++++++- 1 file changed, 470 insertions(+), 1 deletion(-) diff --git a/halo2_frontend/src/dev/cost.rs b/halo2_frontend/src/dev/cost.rs index 870a7e600..7cf75065c 100644 --- a/halo2_frontend/src/dev/cost.rs +++ b/halo2_frontend/src/dev/cost.rs @@ -555,6 +555,475 @@ mod tests { Ok(()) } } - CircuitCost::::measure(K, &MyCircuit).proof_size(1); + let cost = CircuitCost::::measure(K, &MyCircuit); + + let marginal_proof_size = cost.marginal_proof_size(); + assert_eq!(usize::from(marginal_proof_size), 0); + + 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).expect("todo"); + let res = region + .assign_advice_from_instance( + || "", + config.instance, + 0, + config.a, + offset, + ) + .expect("todo"); + // 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]) + .expect("todo"); + instance_copy.push(res.clone()); + let (res, _) = config + .assign_gate(&mut region, &mut offset, Some(res), [0, 6, 7, 1]) + .expect("todo"); + instance_copy.push(res.clone()); + let (res, _) = config + .assign_gate(&mut region, &mut offset, Some(res), [0, 8, 9, 1]) + .expect("todo"); + instance_copy.push(res.clone()); + let (res, _) = config + .assign_gate( + &mut region, + &mut offset, + Some(res), + [0, 0xffffffff, 0xdeadbeef, 1], + ) + .expect("todo"); + let _ = config + .assign_gate( + &mut region, + &mut offset, + Some(res), + [0, 0xabad1d3a, 0x12345678, 0x42424242], + ) + .expect("todo"); + 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]) + .expect("todo"); + offset += 1; + let (_, abcd2) = config + .assign_gate(&mut region, &mut offset, None, [2, 3, 1, 1]) + .expect("todo"); + offset += 1; + let (_, abcd3) = config + .assign_gate(&mut region, &mut offset, None, [4, 2, 1, 1]) + .expect("todo"); + offset += 1; + region + .constrain_equal(abcd1[1].cell(), abcd2[0].cell()) + .expect("todo"); + region + .constrain_equal(abcd2[0].cell(), abcd3[1].cell()) + .expect("todo"); + 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]) + .expect("todo"); + offset += 1; + let (_, abcd2) = config + .assign_gate(&mut region, &mut offset, None, [2, 9, 1, 1]) + .expect("todo"); + offset += 1; + let (_, abcd3) = config + .assign_gate(&mut region, &mut offset, None, [9, 2, 1, 1]) + .expect("todo"); + offset += 1; + region + .constrain_equal(abcd1[1].cell(), abcd1[3].cell()) + .expect("todo"); + region + .constrain_equal(abcd2[1].cell(), abcd1[3].cell()) + .expect("todo"); + region + .constrain_equal(abcd3[0].cell(), abcd1[3].cell()) + .expect("todo"); + + // 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), + ) + .expect("todo"); + region + .assign_fixed( + || "", + config.s_ltable, + offset, + || Value::known(F::ONE), + ) + .expect("todo"); + 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) + .expect("todo"); + region + .assign_advice(|| "", config.b, offset, || lookup_row1) + .expect("todo"); + 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) + .expect("todo"); + region + .assign_advice(|| "", config.c, offset, || table_row1) + .expect("todo"); + 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) + .expect("todo"); + let rlc = challenge.map(|ch| { + let [a, b, ..] = abcd; + F::from(a) + ch * F::from(b) + }); + region + .assign_advice(|| "", config.e, offset - 1, || rlc) + .expect("todo"); + 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), + ) + .expect("todo"); + region + .assign_fixed( + || "", + config.s_stable, + offset, + || Value::known(F::ONE), + ) + .expect("todo"); + let shuffle_row0 = Value::known(F::from(*shuffle_row)); + region + .assign_advice(|| "", config.a, offset, || shuffle_row0) + .expect("todo"); + let table_row0 = Value::known(F::from(*table_row)); + region + .assign_advice(|| "", config.b, offset, || table_row0) + .expect("todo"); + 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) + .expect("todo"); + 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); } } From 7ed9ce464e0e0c1fa5e233d720be86ce0f8c411a Mon Sep 17 00:00:00 2001 From: guorong009 Date: Thu, 8 Aug 2024 18:21:31 +0800 Subject: [PATCH 11/17] chore: improve unit tests for "frontend/dev/failure" --- halo2_frontend/src/dev/failure.rs | 157 ++++++++++++++++++++++++++++++ 1 file changed, 157 insertions(+) diff --git a/halo2_frontend/src/dev/failure.rs b/halo2_frontend/src/dev/failure.rs index 4e8199513..ad7c76235 100644 --- a/halo2_frontend/src/dev/failure.rs +++ b/halo2_frontend/src/dev/failure.rs @@ -1018,6 +1018,75 @@ mod tests { let errs = prover.verify().unwrap_err(); assert_eq!(errs.len(), 1); + // debug printing + assert_eq!( + format!("{:?}", errs[0]), + r#####"ConstraintCaseDebug { + constraint: Constraint { + gate: Gate { + index: 0, + name: "Equality check", + }, + index: 0, + name: "", + }, + location: InRegion { + region: Region 1 ('Wrong synthesis'), + offset: 0, + }, + cell_values: [ + ( + DebugVirtualCell { + name: "", + column: DebugColumn { + column_type: Advice, + index: 0, + annotation: "This is Advice!", + }, + rotation: 0, + }, + "1", + ), + ( + DebugVirtualCell { + name: "", + column: DebugColumn { + column_type: Advice, + index: 1, + annotation: "This is Advice too!", + }, + rotation: 0, + }, + "0", + ), + ( + DebugVirtualCell { + name: "", + column: DebugColumn { + column_type: Advice, + index: 2, + annotation: "Another one!", + }, + rotation: 0, + }, + "0x5", + ), + ( + DebugVirtualCell { + name: "", + column: DebugColumn { + column_type: Fixed, + index: 0, + annotation: "This is a Fixed!", + }, + rotation: 0, + }, + "0x7", + ), + ], +}"##### + ); + // display printing assert_eq!( format!("{}", errs[0]), r#####"Constraint 0 in gate 0 ('Equality check') is not satisfied in Region 1 ('Wrong synthesis') at offset 0 @@ -1160,4 +1229,92 @@ mod tests { r#####"Region 1 ('Wrong synthesis') uses Gate 0 ('Equality check') at offset 1, which requires cell in column Column { index: 1, column_type: Advice } at offset 0 with annotation Some("This is Advice too!") to be assigned."##### ); } + + #[test] + fn test_failure_instance_cell_not_assigned() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + a: Column, + b: Column, + c: Column, + d: Column, + q: Selector, + } + + struct FaultyCircuit {} + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let b = meta.advice_column(); + let c = meta.advice_column(); + let d = meta.instance_column(); + let q = meta.selector(); + + meta.enable_equality(c); + meta.enable_equality(d); + + meta.create_gate("Addition check", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let b = cells.query_advice(b, Rotation::cur()); + let c = cells.query_advice(c, Rotation::cur()); + let q = cells.query_selector(q); + + vec![q * (a + b - c)] + }); + + FaultyCircuitConfig { a, b, c, d, q } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "Instance value not assigned", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Assign b = 1. + region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?; + + // Assign & constraint c = 2. + region.assign_advice_from_instance(|| "c", config.d, 0, config.c, 0)?; + + Ok(()) + }, + )?; + Ok(()) + } + } + + let prover = MockProver::run(K, &FaultyCircuit {}, vec![vec![]]).unwrap(); + let errs = prover.verify().unwrap_err(); + + assert_eq!(errs.len(), 1); + assert_eq!( + format!("{}", errs[0]), + r#####"Constraint 0 in gate 0 ('Addition check') is not satisfied in Region 0 ('Instance value not assigned') at offset 0 +- Column('Advice', 0 - )@0 = 1 +- Column('Advice', 1 - )@0 = 1 +- Column('Advice', 2 - )@0 = 0 +"##### + ); + } } From 543cd61d24904927c83917fc797b3461c6a3e7a9 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Mon, 12 Aug 2024 13:57:38 +0800 Subject: [PATCH 12/17] fix: improve the "serialization" example --- halo2_proofs/tests/serialization.rs | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) diff --git a/halo2_proofs/tests/serialization.rs b/halo2_proofs/tests/serialization.rs index 54e350d7d..96fbdddde 100644 --- a/halo2_proofs/tests/serialization.rs +++ b/halo2_proofs/tests/serialization.rs @@ -8,8 +8,7 @@ use halo2_debug::test_rng; use halo2_proofs::{ circuit::{Layouter, SimpleFloorPlanner, Value}, plonk::{ - create_proof, keygen_pk, keygen_vk_custom, pk_read, verify_proof, Advice, Circuit, Column, - ConstraintSystem, ErrorFront, Fixed, Instance, + create_proof, keygen_pk, keygen_vk_custom, pk_read, verify_proof, vk_read, Advice, Circuit, Column, ConstraintSystem, ErrorFront, Fixed, Instance }, poly::{ kzg::{ @@ -141,8 +140,29 @@ fn test_serialization() { let compress_selectors = true; let vk = keygen_vk_custom(¶ms, &circuit, compress_selectors) .expect("vk should not fail"); - let pk = keygen_pk(¶ms, vk, &circuit).expect("pk should not fail"); + let pk = keygen_pk(¶ms, vk.clone(), &circuit).expect("pk should not fail"); + // serialization test for vk + let f = File::create("serialization-test.vk").unwrap(); + let mut writer = BufWriter::new(f); + vk.write(&mut writer, SerdeFormat::RawBytes).unwrap(); + writer.flush().unwrap(); + + let f = File::open("serialization-test.vk").unwrap(); + let mut reader = BufReader::new(f); + #[allow(clippy::unit_arg)] + let vk = vk_read::( + &mut reader, + SerdeFormat::RawBytes, + k, + &circuit, + compress_selectors, + ) + .unwrap(); + + std::fs::remove_file("serialization-test.vk").unwrap(); + + // serialization test for pk let f = File::create("serialization-test.pk").unwrap(); let mut writer = BufWriter::new(f); pk.write(&mut writer, SerdeFormat::RawBytes).unwrap(); @@ -162,6 +182,7 @@ fn test_serialization() { std::fs::remove_file("serialization-test.pk").unwrap(); + // create & verify proof let instances: Vec>> = vec![vec![vec![circuit.0]]]; let mut transcript = Blake2bWrite::<_, _, Challenge255<_>>::init(vec![]); create_proof::< @@ -193,7 +214,7 @@ fn test_serialization() { SingleStrategy, >( &verifier_params, - pk.get_vk(), + &vk, // pk.get_vk() strategy, instances.as_slice(), &mut transcript From 29f7167541affbf2df8a5edb5ecbe133caf42d05 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Mon, 12 Aug 2024 14:30:02 +0800 Subject: [PATCH 13/17] chore: fmt --- halo2_proofs/tests/serialization.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/halo2_proofs/tests/serialization.rs b/halo2_proofs/tests/serialization.rs index 96fbdddde..2bf9c23b8 100644 --- a/halo2_proofs/tests/serialization.rs +++ b/halo2_proofs/tests/serialization.rs @@ -8,7 +8,8 @@ use halo2_debug::test_rng; use halo2_proofs::{ circuit::{Layouter, SimpleFloorPlanner, Value}, plonk::{ - create_proof, keygen_pk, keygen_vk_custom, pk_read, verify_proof, vk_read, Advice, Circuit, Column, ConstraintSystem, ErrorFront, Fixed, Instance + create_proof, keygen_pk, keygen_vk_custom, pk_read, verify_proof, vk_read, Advice, Circuit, + Column, ConstraintSystem, ErrorFront, Fixed, Instance, }, poly::{ kzg::{ From 081a70c199e52cb42780d54ee978c8b361294fb2 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Wed, 25 Sep 2024 11:18:21 +0800 Subject: [PATCH 14/17] fix: improve some code parts --- halo2_frontend/src/dev/cost.rs | 62 ++++++++++++++--------------- halo2_frontend/src/dev/tfp.rs | 12 +++--- halo2_proofs/tests/serialization.rs | 2 +- 3 files changed, 37 insertions(+), 39 deletions(-) diff --git a/halo2_frontend/src/dev/cost.rs b/halo2_frontend/src/dev/cost.rs index 7cf75065c..9e5f2a1c7 100644 --- a/halo2_frontend/src/dev/cost.rs +++ b/halo2_frontend/src/dev/cost.rs @@ -773,7 +773,7 @@ mod tests { let mut offset = 0; let mut instance_copy = Vec::new(); // First "a" value comes from instance - config.s_instance.enable(&mut region, offset).expect("todo"); + config.s_instance.enable(&mut region, offset).unwrap(); let res = region .assign_advice_from_instance( || "", @@ -782,19 +782,19 @@ mod tests { config.a, offset, ) - .expect("todo"); + .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]) - .expect("todo"); + .unwrap(); instance_copy.push(res.clone()); let (res, _) = config .assign_gate(&mut region, &mut offset, Some(res), [0, 6, 7, 1]) - .expect("todo"); + .unwrap(); instance_copy.push(res.clone()); let (res, _) = config .assign_gate(&mut region, &mut offset, Some(res), [0, 8, 9, 1]) - .expect("todo"); + .unwrap(); instance_copy.push(res.clone()); let (res, _) = config .assign_gate( @@ -803,7 +803,7 @@ mod tests { Some(res), [0, 0xffffffff, 0xdeadbeef, 1], ) - .expect("todo"); + .unwrap(); let _ = config .assign_gate( &mut region, @@ -811,53 +811,53 @@ mod tests { Some(res), [0, 0xabad1d3a, 0x12345678, 0x42424242], ) - .expect("todo"); + .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]) - .expect("todo"); + .unwrap(); offset += 1; let (_, abcd2) = config .assign_gate(&mut region, &mut offset, None, [2, 3, 1, 1]) - .expect("todo"); + .unwrap(); offset += 1; let (_, abcd3) = config .assign_gate(&mut region, &mut offset, None, [4, 2, 1, 1]) - .expect("todo"); + .unwrap(); offset += 1; region .constrain_equal(abcd1[1].cell(), abcd2[0].cell()) - .expect("todo"); + .unwrap(); region .constrain_equal(abcd2[0].cell(), abcd3[1].cell()) - .expect("todo"); + .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]) - .expect("todo"); + .unwrap(); offset += 1; let (_, abcd2) = config .assign_gate(&mut region, &mut offset, None, [2, 9, 1, 1]) - .expect("todo"); + .unwrap(); offset += 1; let (_, abcd3) = config .assign_gate(&mut region, &mut offset, None, [9, 2, 1, 1]) - .expect("todo"); + .unwrap(); offset += 1; region .constrain_equal(abcd1[1].cell(), abcd1[3].cell()) - .expect("todo"); + .unwrap(); region .constrain_equal(abcd2[1].cell(), abcd1[3].cell()) - .expect("todo"); + .unwrap(); region .constrain_equal(abcd3[0].cell(), abcd1[3].cell()) - .expect("todo"); + .unwrap(); // Enable a dynamic lookup (powers of two) let table: Vec<_> = @@ -874,7 +874,7 @@ mod tests { offset, || Value::known(F::ONE), ) - .expect("todo"); + .unwrap(); region .assign_fixed( || "", @@ -882,23 +882,23 @@ mod tests { offset, || Value::known(F::ONE), ) - .expect("todo"); + .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) - .expect("todo"); + .unwrap(); region .assign_advice(|| "", config.b, offset, || lookup_row1) - .expect("todo"); + .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) - .expect("todo"); + .unwrap(); region .assign_advice(|| "", config.c, offset, || table_row1) - .expect("todo"); + .unwrap(); offset += 1; } @@ -907,14 +907,14 @@ mod tests { config.s_rlc.enable(&mut region, offset)?; let (_, _) = config .assign_gate(&mut region, &mut offset, None, abcd) - .expect("todo"); + .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) - .expect("todo"); + .unwrap(); offset += 1; } @@ -931,7 +931,7 @@ mod tests { offset, || Value::known(F::ONE), ) - .expect("todo"); + .unwrap(); region .assign_fixed( || "", @@ -939,15 +939,15 @@ mod tests { offset, || Value::known(F::ONE), ) - .expect("todo"); + .unwrap(); let shuffle_row0 = Value::known(F::from(*shuffle_row)); region .assign_advice(|| "", config.a, offset, || shuffle_row0) - .expect("todo"); + .unwrap(); let table_row0 = Value::known(F::from(*table_row)); region .assign_advice(|| "", config.b, offset, || table_row0) - .expect("todo"); + .unwrap(); offset += 1; } @@ -994,7 +994,7 @@ mod tests { loop { let (rows, instance_copy) = self .synthesize_unit(config, &mut layouter, id, unit_id) - .expect("todo"); + .unwrap(); if total_rows == 0 { for (i, instance) in instance_copy.iter().enumerate() { layouter.constrain_instance( diff --git a/halo2_frontend/src/dev/tfp.rs b/halo2_frontend/src/dev/tfp.rs index fa492f52e..cee9a4128 100644 --- a/halo2_frontend/src/dev/tfp.rs +++ b/halo2_frontend/src/dev/tfp.rs @@ -607,13 +607,11 @@ mod tests { } } - // // At the start of your test, enable tracing. - // tracing_subscriber::fmt() - // .with_max_level(tracing::Level::DEBUG) - // .with_ansi(false) - // .without_time() - // .init(); - + // At the start of your test, enable tracing. + // + // Following setup of `SharedStorage` and `tracing_subscriber::fmt` is just for this test. + // For real tests, you don't need to do this. + // Check the example in the doc of [`TracingFloorPlanner`] for details. let subscriber = tracing_subscriber::fmt() .with_max_level(tracing::Level::DEBUG) .with_ansi(false) diff --git a/halo2_proofs/tests/serialization.rs b/halo2_proofs/tests/serialization.rs index 328d637cb..b0e8ef4c4 100644 --- a/halo2_proofs/tests/serialization.rs +++ b/halo2_proofs/tests/serialization.rs @@ -215,7 +215,7 @@ fn test_serialization() { SingleStrategy, >( &verifier_params, - &vk, // pk.get_vk() + &vk, strategy, instances.as_slice(), &mut transcript From c5016259e5860cf3d268734e281507f590e15490 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Wed, 25 Sep 2024 16:05:36 +0800 Subject: [PATCH 15/17] test: remove "identifier" tests --- halo2_backend/src/plonk/circuit.rs | 72 +------------------ .../src/plonk/circuit/expression.rs | 51 ------------- halo2_middleware/src/expression.rs | 53 +------------- 3 files changed, 2 insertions(+), 174 deletions(-) diff --git a/halo2_backend/src/plonk/circuit.rs b/halo2_backend/src/plonk/circuit.rs index cd7c6c663..5dd6aa06e 100644 --- a/halo2_backend/src/plonk/circuit.rs +++ b/halo2_backend/src/plonk/circuit.rs @@ -369,9 +369,7 @@ fn shuffle_argument_required_degree(arg: &shuffle::Argume #[cfg(test)] mod tests { - use super::{Any, ExpressionBack, QueryBack, VarBack}; - - use halo2_middleware::poly::Rotation; + use super::ExpressionBack; use halo2curves::bn256::Fr; #[test] @@ -411,72 +409,4 @@ mod tests { assert_eq!(happened, expected); } - - #[test] - fn expressionback_identifier() { - let sum_expr: ExpressionBack = ExpressionBack::Sum( - Box::new(ExpressionBack::Constant(1.into())), - Box::new(ExpressionBack::Constant(2.into())), - ); - assert_eq!(sum_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001+0x0000000000000000000000000000000000000000000000000000000000000002)"); - - let prod_expr: ExpressionBack = ExpressionBack::Product( - Box::new(ExpressionBack::Constant(1.into())), - Box::new(ExpressionBack::Constant(2.into())), - ); - assert_eq!(prod_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001*0x0000000000000000000000000000000000000000000000000000000000000002)"); - - // simulate the expressios being used in a circuit - let l: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { - index: 0, - column_index: 0, - column_type: Any::Advice, - rotation: Rotation::cur(), - })); - let r: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { - index: 1, - column_index: 1, - column_type: Any::Advice, - rotation: Rotation::cur(), - })); - let o: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { - index: 2, - column_index: 2, - column_type: Any::Advice, - rotation: Rotation::cur(), - })); - let c: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { - index: 3, - column_index: 0, - column_type: Any::Fixed, - rotation: Rotation::cur(), - })); - let sl: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { - index: 4, - column_index: 1, - column_type: Any::Fixed, - rotation: Rotation::cur(), - })); - let sr: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { - index: 5, - column_index: 2, - column_type: Any::Fixed, - rotation: Rotation::cur(), - })); - let sm: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { - index: 6, - column_index: 3, - column_type: Any::Fixed, - rotation: Rotation::cur(), - })); - let so: ExpressionBack = ExpressionBack::Var(VarBack::Query(QueryBack { - index: 7, - column_index: 4, - column_type: Any::Fixed, - rotation: Rotation::cur(), - })); - - let simple_plonk_expr = sl * l.clone() + sr * r.clone() + sm * (l * r) - so * o + c; - assert_eq!(simple_plonk_expr.identifier(), "(((((Query(QueryBack { index: 4, column_index: 1, column_type: Fixed, rotation: Rotation(0) })*Query(QueryBack { index: 0, column_index: 0, column_type: Advice, rotation: Rotation(0) }))+(Query(QueryBack { index: 5, column_index: 2, column_type: Fixed, rotation: Rotation(0) })*Query(QueryBack { index: 1, column_index: 1, column_type: Advice, rotation: Rotation(0) })))+(Query(QueryBack { index: 6, column_index: 3, column_type: Fixed, rotation: Rotation(0) })*(Query(QueryBack { index: 0, column_index: 0, column_type: Advice, rotation: Rotation(0) })*Query(QueryBack { index: 1, column_index: 1, column_type: Advice, rotation: Rotation(0) }))))+(-(Query(QueryBack { index: 7, column_index: 4, column_type: Fixed, rotation: Rotation(0) })*Query(QueryBack { index: 2, column_index: 2, column_type: Advice, rotation: Rotation(0) }))))+Query(QueryBack { index: 3, column_index: 0, column_type: Fixed, rotation: Rotation(0) }))"); - } } diff --git a/halo2_frontend/src/plonk/circuit/expression.rs b/halo2_frontend/src/plonk/circuit/expression.rs index 31d53bea3..3a991d198 100644 --- a/halo2_frontend/src/plonk/circuit/expression.rs +++ b/halo2_frontend/src/plonk/circuit/expression.rs @@ -1097,10 +1097,7 @@ impl Product for Expression { #[cfg(test)] mod tests { - use crate::plonk::{AdviceQuery, FixedQuery, Selector}; - use super::Expression; - use halo2_middleware::poly::Rotation; use halo2curves::bn256::Fr; #[test] @@ -1140,52 +1137,4 @@ mod tests { assert_eq!(happened, expected); } - - #[test] - fn identifier() { - let sum_expr: Expression = Expression::Sum( - Box::new(Expression::Constant(1.into())), - Box::new(Expression::Constant(2.into())), - ); - assert_eq!(sum_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001+0x0000000000000000000000000000000000000000000000000000000000000002)"); - - let prod_expr: Expression = Expression::Product( - Box::new(Expression::Constant(1.into())), - Box::new(Expression::Constant(2.into())), - ); - assert_eq!(prod_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001*0x0000000000000000000000000000000000000000000000000000000000000002)"); - - let scaled_expr: Expression = - Expression::Scaled(Box::new(Expression::Constant(1.into())), 100.into()); - assert_eq!(scaled_expr.identifier(), "0x0000000000000000000000000000000000000000000000000000000000000001*0x0000000000000000000000000000000000000000000000000000000000000064"); - - // simulate the expressions being used in a circuit - let l: Expression = Expression::Advice(AdviceQuery { - index: None, - column_index: 0, - rotation: Rotation::cur(), - }); - let r: Expression = Expression::Advice(AdviceQuery { - index: None, - column_index: 1, - rotation: Rotation::cur(), - }); - let o: Expression = Expression::Advice(AdviceQuery { - index: None, - column_index: 2, - rotation: Rotation::cur(), - }); - let sl: Expression = Expression::Selector(Selector(0, false)); - let sr: Expression = Expression::Selector(Selector(1, false)); - let sm: Expression = Expression::Selector(Selector(2, false)); - let so: Expression = Expression::Selector(Selector(3, false)); - let c: Expression = Expression::Fixed(FixedQuery { - index: None, - column_index: 0, - rotation: Rotation::cur(), - }); - - let simple_plonk_expr = sl * l.clone() + sr * r.clone() + sm * (l * r) - so * o + c; - assert_eq!(simple_plonk_expr.identifier(), "(((((selector[0]*advice[0][0])+(selector[1]*advice[1][0]))+(selector[2]*(advice[0][0]*advice[1][0])))+(-(selector[3]*advice[2][0])))+fixed[0][0])"); - } } diff --git a/halo2_middleware/src/expression.rs b/halo2_middleware/src/expression.rs index e6240d60e..f0c202f13 100644 --- a/halo2_middleware/src/expression.rs +++ b/halo2_middleware/src/expression.rs @@ -176,10 +176,7 @@ impl Product for Expression { #[cfg(test)] mod tests { - use crate::{ - circuit::{Any, ExpressionMid, QueryMid, VarMid}, - poly::Rotation, - }; + use crate::circuit::ExpressionMid; use halo2curves::bn256::Fr; #[test] @@ -219,52 +216,4 @@ mod tests { assert_eq!(happened, expected); } - - #[test] - fn identifier() { - let sum_expr: ExpressionMid = ExpressionMid::Sum( - Box::new(ExpressionMid::Constant(1.into())), - Box::new(ExpressionMid::Constant(2.into())), - ); - assert_eq!(sum_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001+0x0000000000000000000000000000000000000000000000000000000000000002)"); - - let prod_expr: ExpressionMid = ExpressionMid::Product( - Box::new(ExpressionMid::Constant(1.into())), - Box::new(ExpressionMid::Constant(2.into())), - ); - assert_eq!(prod_expr.identifier(), "(0x0000000000000000000000000000000000000000000000000000000000000001*0x0000000000000000000000000000000000000000000000000000000000000002)"); - - // simulate the expressios being used in a circuit - let l: ExpressionMid = ExpressionMid::Var(VarMid::Query(QueryMid::new( - Any::Advice, - 0, - Rotation::cur(), - ))); - let r: ExpressionMid = ExpressionMid::Var(VarMid::Query(QueryMid::new( - Any::Advice, - 1, - Rotation::cur(), - ))); - let o: ExpressionMid = ExpressionMid::Var(VarMid::Query(QueryMid::new( - Any::Advice, - 2, - Rotation::cur(), - ))); - let c: ExpressionMid = - ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 0, Rotation::cur()))); - let sl: ExpressionMid = - ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 1, Rotation::cur()))); - let sr: ExpressionMid = - ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 2, Rotation::cur()))); - let sm: ExpressionMid = - ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 3, Rotation::cur()))); - let so: ExpressionMid = - ExpressionMid::Var(VarMid::Query(QueryMid::new(Any::Fixed, 4, Rotation::cur()))); - - let simple_plonk_expr = sl * l.clone() + sr * r.clone() + sm * (l * r) - so * o + c; - assert_eq!( - simple_plonk_expr.identifier(), - "(((((f1*a0)+(f2*a1))+(f3*(a0*a1)))+(-(f4*a2)))+f0)" - ); - } } From b81e32d59372abc1ff2a429f861584609a3ade5c Mon Sep 17 00:00:00 2001 From: guorong009 Date: Wed, 25 Sep 2024 18:22:51 +0800 Subject: [PATCH 16/17] feat: add 2 examples for serialization and circuit cost --- .gitignore | 3 +- halo2_proofs/examples/circuit-cost.rs | 122 ++++++++++++++++++ halo2_proofs/examples/serialization.rs | 171 +++++++++++++++++++++++++ 3 files changed, 295 insertions(+), 1 deletion(-) create mode 100644 halo2_proofs/examples/circuit-cost.rs create mode 100644 halo2_proofs/examples/serialization.rs diff --git a/.gitignore b/.gitignore index 123de7b25..11874446a 100644 --- a/.gitignore +++ b/.gitignore @@ -6,4 +6,5 @@ Cargo.lock .DS_Store layout.png -serialization-test.pk +serialization-example.vk +serialization-example.pk diff --git a/halo2_proofs/examples/circuit-cost.rs b/halo2_proofs/examples/circuit-cost.rs new file mode 100644 index 000000000..bafcf6afa --- /dev/null +++ b/halo2_proofs/examples/circuit-cost.rs @@ -0,0 +1,122 @@ +use halo2_frontend::dev::CircuitCost; +use halo2_proofs::{ + circuit::{Layouter, SimpleFloorPlanner, Value}, + plonk::{Advice, Circuit, Column, ConstraintSystem, ErrorFront, Fixed, Instance}, + poly::Rotation, +}; +use halo2curves::pasta::{Eq, Fp}; + +#[derive(Clone, Copy)] +struct StandardPlonkConfig { + a: Column, + b: Column, + c: Column, + q_a: Column, + q_b: Column, + q_c: Column, + q_ab: Column, + constant: Column, + #[allow(dead_code)] + instance: Column, +} + +impl StandardPlonkConfig { + fn configure(meta: &mut ConstraintSystem) -> Self { + let [a, b, c] = [(); 3].map(|_| meta.advice_column()); + let [q_a, q_b, q_c, q_ab, constant] = [(); 5].map(|_| meta.fixed_column()); + let instance = meta.instance_column(); + + [a, b, c].map(|column| meta.enable_equality(column)); + + meta.create_gate( + "q_a·a + q_b·b + q_c·c + q_ab·a·b + constant + instance = 0", + |meta| { + let [a, b, c] = [a, b, c].map(|column| meta.query_advice(column, Rotation::cur())); + let [q_a, q_b, q_c, q_ab, constant] = [q_a, q_b, q_c, q_ab, constant] + .map(|column| meta.query_fixed(column, Rotation::cur())); + let instance = meta.query_instance(instance, Rotation::cur()); + Some( + q_a * a.clone() + + q_b * b.clone() + + q_c * c + + q_ab * a * b + + constant + + instance, + ) + }, + ); + + StandardPlonkConfig { + a, + b, + c, + q_a, + q_b, + q_c, + q_ab, + constant, + instance, + } + } +} + +#[derive(Clone, Default)] +struct StandardPlonk(Fp); + +impl Circuit for StandardPlonk { + type Config = StandardPlonkConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn without_witnesses(&self) -> Self { + Self::default() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + StandardPlonkConfig::configure(meta) + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), ErrorFront> { + layouter.assign_region( + || "", + |mut region| { + region.assign_advice(|| "", config.a, 0, || Value::known(self.0))?; + region.assign_fixed(|| "", config.q_a, 0, || Value::known(-Fp::one()))?; + + region.assign_advice(|| "", config.a, 1, || Value::known(-Fp::from(5u64)))?; + for (idx, column) in (1..).zip([ + config.q_a, + config.q_b, + config.q_c, + config.q_ab, + config.constant, + ]) { + region.assign_fixed(|| "", column, 1, || Value::known(Fp::from(idx as u64)))?; + } + + let a = region.assign_advice(|| "", config.a, 2, || Value::known(Fp::one()))?; + a.copy_advice(|| "", &mut region, config.b, 3)?; + a.copy_advice(|| "", &mut region, config.c, 4)?; + Ok(()) + }, + ) + } +} + +fn main() { + const K: u32 = 6; + let circuit = StandardPlonk(Fp::one()); + + let cost = CircuitCost::::measure(K, &circuit); + + let marginal_proof_size = cost.marginal_proof_size(); + println!("Marginal proof size: {}", usize::from(marginal_proof_size)); + + let proof_size = cost.proof_size(1); + println!("Proof size: {}", usize::from(proof_size)); +} diff --git a/halo2_proofs/examples/serialization.rs b/halo2_proofs/examples/serialization.rs new file mode 100644 index 000000000..e1cdd9ee4 --- /dev/null +++ b/halo2_proofs/examples/serialization.rs @@ -0,0 +1,171 @@ +use std::{ + fs::File, + io::{BufReader, BufWriter, Write}, +}; + +use ff::Field; +use halo2_debug::test_rng; +use halo2_proofs::{ + circuit::{Layouter, SimpleFloorPlanner, Value}, + plonk::{ + keygen_pk_custom, keygen_vk_custom, pk_read, vk_read, Advice, Circuit, Column, + ConstraintSystem, ErrorFront, Fixed, Instance, ProvingKey, VerifyingKey, + }, + poly::{kzg::commitment::ParamsKZG, Rotation}, + SerdeFormat, +}; +use halo2curves::bn256::{Bn256, Fr, G1Affine}; + +#[derive(Clone, Copy)] +struct StandardPlonkConfig { + a: Column, + b: Column, + c: Column, + q_a: Column, + q_b: Column, + q_c: Column, + q_ab: Column, + constant: Column, + #[allow(dead_code)] + instance: Column, +} + +impl StandardPlonkConfig { + fn configure(meta: &mut ConstraintSystem) -> Self { + let [a, b, c] = [(); 3].map(|_| meta.advice_column()); + let [q_a, q_b, q_c, q_ab, constant] = [(); 5].map(|_| meta.fixed_column()); + let instance = meta.instance_column(); + + [a, b, c].map(|column| meta.enable_equality(column)); + + meta.create_gate( + "q_a·a + q_b·b + q_c·c + q_ab·a·b + constant + instance = 0", + |meta| { + let [a, b, c] = [a, b, c].map(|column| meta.query_advice(column, Rotation::cur())); + let [q_a, q_b, q_c, q_ab, constant] = [q_a, q_b, q_c, q_ab, constant] + .map(|column| meta.query_fixed(column, Rotation::cur())); + let instance = meta.query_instance(instance, Rotation::cur()); + Some( + q_a * a.clone() + + q_b * b.clone() + + q_c * c + + q_ab * a * b + + constant + + instance, + ) + }, + ); + + StandardPlonkConfig { + a, + b, + c, + q_a, + q_b, + q_c, + q_ab, + constant, + instance, + } + } +} + +#[derive(Clone, Default)] +struct StandardPlonk(Fr); + +impl Circuit for StandardPlonk { + type Config = StandardPlonkConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn without_witnesses(&self) -> Self { + Self::default() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + StandardPlonkConfig::configure(meta) + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), ErrorFront> { + layouter.assign_region( + || "", + |mut region| { + region.assign_advice(|| "", config.a, 0, || Value::known(self.0))?; + region.assign_fixed(|| "", config.q_a, 0, || Value::known(-Fr::one()))?; + + region.assign_advice(|| "", config.a, 1, || Value::known(-Fr::from(5u64)))?; + for (idx, column) in (1..).zip([ + config.q_a, + config.q_b, + config.q_c, + config.q_ab, + config.constant, + ]) { + region.assign_fixed(|| "", column, 1, || Value::known(Fr::from(idx as u64)))?; + } + + let a = region.assign_advice(|| "", config.a, 2, || Value::known(Fr::one()))?; + a.copy_advice(|| "", &mut region, config.b, 3)?; + a.copy_advice(|| "", &mut region, config.c, 4)?; + Ok(()) + }, + ) + } +} + +fn setup( + k: u32, + compress_selectors: bool, +) -> (StandardPlonk, VerifyingKey, ProvingKey) { + let mut rng = test_rng(); + + let circuit = StandardPlonk(Fr::random(&mut rng)); + let params = ParamsKZG::::setup(k, &mut rng); + + let vk = keygen_vk_custom(¶ms, &circuit, compress_selectors).expect("vk should not fail"); + let pk = keygen_pk_custom(¶ms, vk.clone(), &circuit, compress_selectors) + .expect("pk should not fail"); + + (circuit, vk, pk) +} + +fn main() { + let k = 4; + let compress_selectors = true; + + let (circuit, vk, pk) = setup(k, compress_selectors); + + // choose (de)serialization format + let format = SerdeFormat::RawBytes; + + // serialization for vk + let f = File::create("serialization-example.vk").unwrap(); + let mut writer = BufWriter::new(f); + vk.write(&mut writer, format).unwrap(); + writer.flush().unwrap(); + + // deserialization for vk + let f = File::open("serialization-example.vk").unwrap(); + let mut reader = BufReader::new(f); + let _vk = + vk_read::(&mut reader, format, k, &circuit, compress_selectors) + .unwrap(); + + // serialization for pk + let f = File::create("serialization-example.pk").unwrap(); + let mut writer = BufWriter::new(f); + pk.write(&mut writer, format).unwrap(); + writer.flush().unwrap(); + + // deserialization for pk + let f = File::open("serialization-example.pk").unwrap(); + let mut reader = BufReader::new(f); + let _pk = + pk_read::(&mut reader, format, k, &circuit, compress_selectors) + .unwrap(); +} From 3971b7f90538f041bb9729aa12537454be0dc7ed Mon Sep 17 00:00:00 2001 From: guorong009 Date: Thu, 26 Sep 2024 14:54:45 +0800 Subject: [PATCH 17/17] test: remove extra unit test in "cost" --- halo2_frontend/src/dev/cost.rs | 463 --------------------------------- 1 file changed, 463 deletions(-) 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); - } }