From 43c1dac54e2ee20ae3253c11a32e9a69cf10f641 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Thu, 5 Jan 2023 17:45:18 +0100 Subject: [PATCH 1/6] fix: Support dynamic lookups in `MockProver::assert_verify` Since lookups can only be `Fixed` in Halo2-upstream, we need to add custom suport for the error rendering of dynamic lookups which doesn't come by default when we rebase to upstream. This means that now we have to print not only `AdviceQuery` results to render the `Expression` that is being looked up. But also support `Instance`, `Advice`, `Challenge` or any other expression types that are avaliable. This addresses the rendering issue, renaming also the `table_columns` variable for `lookup_columns` as the columns do not have the type `TableColumn` by default as opposite to what happens upstream. --- halo2_proofs/src/dev/failure.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index c3c7ab93a9..2fcb2a1fc8 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -398,18 +398,18 @@ fn render_lookup( // Recover the fixed columns from the table expressions. We don't allow composite // expressions for the table side of lookups. - let table_columns = lookup.table_expressions.iter().map(|expr| { + let lookup_columns = lookup.table_expressions.iter().map(|expr| { expr.evaluate( &|_| panic!("no constants in table expressions"), &|_| panic!("no selectors in table expressions"), &|query| format!("F{}", query.column_index), - &|_| panic!("no advice columns in table expressions"), - &|_| panic!("no instance columns in table expressions"), - &|_| panic!("no challenges in table expressions"), - &|_| panic!("no negations in table expressions"), - &|_, _| panic!("no sums in table expressions"), - &|_, _| panic!("no products in table expressions"), - &|_, _| panic!("no scaling in table expressions"), + &|query| format! {"A{}", query.column_index}, + &|query| format! {"I{}", query.column_index}, + &|challenge| format! {"C{}", challenge.index()}, + &|query| format! {"-{}", query}, + &|a, b| format! {"{} + {}", a,b}, + &|a, b| format! {"{} * {}", a,b}, + &|a, b| format! {"{} * {:?}", a, b}, ) }); @@ -441,7 +441,7 @@ fn render_lookup( eprint!("{}L{}", if i == 0 { "" } else { ", " }, i); } eprint!(") ∉ ("); - for (i, column) in table_columns.enumerate() { + for (i, column) in lookup_columns.enumerate() { eprint!("{}{}", if i == 0 { "" } else { ", " }, column); } eprintln!(")"); From 442099e8340ffdb477131e76092fc1a17c1a9227 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Thu, 5 Jan 2023 17:52:15 +0100 Subject: [PATCH 2/6] fix: Don't error and emit empty String for Empty queries --- halo2_proofs/src/dev/failure/emitter.rs | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index 0e792367c7..3ab2b1e4f2 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -120,15 +120,18 @@ pub(super) fn expression_to_string( &|query| { layout .get(&query.rotation.0) - .unwrap() - .get( - &( - Any::Advice(Advice { phase: query.phase }), - query.column_index, + .map(|map| { + map.get( + &( + Any::Advice(Advice { phase: query.phase }), + query.column_index, + ) + .into(), ) - .into(), - ) - .unwrap() + }) + .flatten() + .cloned() + .unwrap_or_else(|| String::new()) .clone() }, &|query| { From a9e0f99d680efbbcb96a9c8c790e26ad9257aac2 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Thu, 5 Jan 2023 17:53:30 +0100 Subject: [PATCH 3/6] feat: Add `assert_sarisfied_par` fn to `MockProver` --- halo2_proofs/src/dev.rs | 42 +++++++++++++++++++++++++++++++---------- 1 file changed, 32 insertions(+), 10 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index b5b92d390f..905b425fd6 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -1315,6 +1315,27 @@ impl MockProver { panic!("circuit was not satisfied"); } } + + /// Panics if the circuit being checked by this `MockProver` is not satisfied. + /// + /// Any verification failures will be pretty-printed to stderr before the function + /// panics. + /// + /// Internally, this function uses a parallel aproach in order to verify the `MockProver` contents. + /// + /// Apart from the stderr output, this method is equivalent to: + /// ```ignore + /// assert_eq!(prover.verify_par(), Ok(())); + /// ``` + pub fn assert_satisfied_par(&self) { + if let Err(errs) = self.verify_par() { + for err in errs { + err.emit(self); + eprintln!(); + } + panic!("circuit was not satisfied"); + } + } } #[cfg(test)] @@ -1392,16 +1413,17 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - assert_eq!( - prover.verify(), - Err(vec![VerifyFailure::CellNotAssigned { - gate: (0, "Equality check").into(), - region: (0, "Faulty synthesis".to_owned()).into(), - gate_offset: 1, - column: Column::new(1, Any::advice()), - offset: 1, - }]) - ); + prover.assert_satisfied(); + // assert_eq!( + // prover.verify(), + // Err(vec![VerifyFailure::CellNotAssigned { + // gate: (0, "Equality check").into(), + // region: (0, "Faulty synthesis".to_owned()).into(), + // gate_offset: 1, + // column: Column::new(1, Any::advice()), + // offset: 1, + // }]) + // ); } #[test] From 681ee43b1ccc1a8c951af2695b8d4564749db9bf Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 9 Jan 2023 10:45:11 +0100 Subject: [PATCH 4/6] fix: Address clippy errors --- halo2_proofs/src/dev/failure/emitter.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index 3ab2b1e4f2..a6d2af4ece 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -120,7 +120,7 @@ pub(super) fn expression_to_string( &|query| { layout .get(&query.rotation.0) - .map(|map| { + .and_then(|map| { map.get( &( Any::Advice(Advice { phase: query.phase }), @@ -129,7 +129,6 @@ pub(super) fn expression_to_string( .into(), ) }) - .flatten() .cloned() .unwrap_or_else(|| String::new()) .clone() From 6eebe6a56f81789978b82bfac1c7fa3d2830a6a4 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 9 Jan 2023 10:46:17 +0100 Subject: [PATCH 5/6] chore: Address review comments --- halo2_proofs/src/dev.rs | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index 905b425fd6..e275f198c3 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -1413,17 +1413,16 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - prover.assert_satisfied(); - // assert_eq!( - // prover.verify(), - // Err(vec![VerifyFailure::CellNotAssigned { - // gate: (0, "Equality check").into(), - // region: (0, "Faulty synthesis".to_owned()).into(), - // gate_offset: 1, - // column: Column::new(1, Any::advice()), - // offset: 1, - // }]) - // ); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::CellNotAssigned { + gate: (0, "Equality check").into(), + region: (0, "Faulty synthesis".to_owned()).into(), + gate_offset: 1, + column: Column::new(1, Any::advice()), + offset: 1, + }]) + ); } #[test] From f1ca2daf4348e5ff0e43b81b48efa5d837f0862b Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 9 Jan 2023 11:06:05 +0100 Subject: [PATCH 6/6] chore: Fix clippy lints --- halo2_proofs/src/dev/failure/emitter.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index a6d2af4ece..91525a20aa 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -130,8 +130,7 @@ pub(super) fn expression_to_string( ) }) .cloned() - .unwrap_or_else(|| String::new()) - .clone() + .unwrap_or_default() }, &|query| { layout