From e01fb150187acb0599480144c6c7866c9a20ba32 Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Fri, 4 Jun 2021 02:56:35 +0100 Subject: [PATCH 1/4] dev: Fix bug in cell assignment checker The simple example was broken because it uses an instance column in a gate. MockProver now assumes all instance cells are assigned to, since this happens outside the circuit and outside its purview. --- src/dev.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/dev.rs b/src/dev.rs index 1681ce0a..326485f5 100644 --- a/src/dev.rs +++ b/src/dev.rs @@ -379,7 +379,8 @@ impl MockProver { Any::Fixed => { self.fixed[cell.column.index()][cell_row].is_some() } - Any::Instance => unreachable!(), + // Instance column cells are assigned outside the circuit. + Any::Instance => true, } { None } else { From 47061ade3d01632de800a7d3fe0a5984ae2af9bd Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Fri, 4 Jun 2021 03:01:09 +0100 Subject: [PATCH 2/4] dev: Report indices of unsatisfied constraints Now that gates may contain multiple constraints, we need to inform developers about which specific constraints are failing within gates. --- examples/simple-example.rs | 3 +- examples/two-chip.rs | 3 +- src/dev.rs | 129 ++++++++++++++++++++----------------- 3 files changed, 73 insertions(+), 62 deletions(-) diff --git a/examples/simple-example.rs b/examples/simple-example.rs index 0a6ee77e..c57ebf41 100644 --- a/examples/simple-example.rs +++ b/examples/simple-example.rs @@ -360,9 +360,10 @@ fn main() { let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap(); assert_eq!( prover.verify(), - Err(vec![VerifyFailure::Gate { + Err(vec![VerifyFailure::Constraint { gate_index: 1, gate_name: "public input", + constraint_index: 0, row: 6, }]) ); diff --git a/examples/two-chip.rs b/examples/two-chip.rs index 6b0290dc..23dea6fa 100644 --- a/examples/two-chip.rs +++ b/examples/two-chip.rs @@ -627,9 +627,10 @@ fn main() { let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap(); assert_eq!( prover.verify(), - Err(vec![VerifyFailure::Gate { + Err(vec![VerifyFailure::Constraint { gate_index: 0, gate_name: "public input", + constraint_index: 0, row: 7, }]) ); diff --git a/src/dev.rs b/src/dev.rs index 326485f5..38966acc 100644 --- a/src/dev.rs +++ b/src/dev.rs @@ -43,16 +43,21 @@ pub enum VerifyFailure { /// a chip implementation), and may not be unique. gate_name: &'static str, }, - /// A gate was not satisfied for a particular row. - Gate { - /// The index of the gate that is not satisfied. These indices are assigned in the - /// order in which `ConstraintSystem::create_gate` is called during - /// `Circuit::configure`. + /// A constraint was not satisfied for a particular row. + Constraint { + /// The index of the gate containing the unsatisfied constraint. These indices are + /// assigned in the order in which `ConstraintSystem::create_gate` is called + /// during `Circuit::configure`. gate_index: usize, - /// The name of the gate that is not satisfied. These are specified by the gate - /// creator (such as a chip implementation), and may not be unique. + /// The name of the gate containing the unsatisfied constraint. This is specified + /// by the gate creator (such as a chip implementation), and may not be unique. gate_name: &'static str, - /// The row on which this gate is not satisfied. + /// The index of the polynomial constraint within the gate that is not satisfied. + /// These indices correspond to the order in which the constraints are returned + /// from the closure passed to `ConstraintSystem::create_gate` during + /// `Circuit::configure`. + constraint_index: usize, + /// The row on which this constraint is not satisfied. row: usize, }, /// A lookup input did not exist in its corresponding table. @@ -157,9 +162,10 @@ pub enum VerifyFailure { /// let prover = MockProver::::run(K, &circuit, instance).unwrap(); /// assert_eq!( /// prover.verify(), -/// Err(vec![VerifyFailure::Gate { +/// Err(vec![VerifyFailure::Constraint { /// gate_index: 0, /// gate_name: "R1CS constraint", +/// constraint_index: 0, /// row: 0 /// }]) /// ); @@ -397,62 +403,65 @@ impl MockProver { }); // Check that all gates are satisfied for all rows. - let gate_errors = self - .cs - .gates - .iter() - .enumerate() - .flat_map(|(gate_index, gate)| { - // We iterate from n..2n so we can just reduce to handle wrapping. - (n..(2 * n)).flat_map(move |row| { - fn load_opt<'a, F: FieldExt, T: ColumnType>( - n: i32, - row: i32, - queries: &'a [(Column, Rotation)], - cells: &'a [Vec>], - ) -> impl Fn(usize) -> F + 'a { - move |index| { - let (column, at) = &queries[index]; - let resolved_row = (row + at.0) % n; - cell_value(cells[column.index()][resolved_row as usize]) + let gate_errors = + self.cs + .gates + .iter() + .enumerate() + .flat_map(|(gate_index, gate)| { + // We iterate from n..2n so we can just reduce to handle wrapping. + (n..(2 * n)).flat_map(move |row| { + fn load_opt<'a, F: FieldExt, T: ColumnType>( + n: i32, + row: i32, + queries: &'a [(Column, Rotation)], + cells: &'a [Vec>], + ) -> impl Fn(usize) -> F + 'a { + move |index| { + let (column, at) = &queries[index]; + let resolved_row = (row + at.0) % n; + cell_value(cells[column.index()][resolved_row as usize]) + } } - } - fn load<'a, F: FieldExt, T: ColumnType>( - n: i32, - row: i32, - queries: &'a [(Column, Rotation)], - cells: &'a [Vec], - ) -> impl Fn(usize) -> F + 'a { - move |index| { - let (column, at) = &queries[index]; - let resolved_row = (row + at.0) % n; - cells[column.index()][resolved_row as usize] + fn load<'a, F: FieldExt, T: ColumnType>( + n: i32, + row: i32, + queries: &'a [(Column, Rotation)], + cells: &'a [Vec], + ) -> impl Fn(usize) -> F + 'a { + move |index| { + let (column, at) = &queries[index]; + let resolved_row = (row + at.0) % n; + cells[column.index()][resolved_row as usize] + } } - } - gate.polynomials().iter().filter_map(move |poly| { - if poly.evaluate( - &|scalar| scalar, - &load_opt(n, row, &self.cs.fixed_queries, &self.fixed), - &load_opt(n, row, &self.cs.advice_queries, &self.advice), - &load(n, row, &self.cs.instance_queries, &self.instance), - &|a, b| a + &b, - &|a, b| a * &b, - &|a, scalar| a * scalar, - ) == F::zero() - { - None - } else { - Some(VerifyFailure::Gate { - gate_index, - gate_name: gate.name(), - row: (row - n) as usize, - }) - } + gate.polynomials().iter().enumerate().filter_map( + move |(poly_index, poly)| { + if poly.evaluate( + &|scalar| scalar, + &load_opt(n, row, &self.cs.fixed_queries, &self.fixed), + &load_opt(n, row, &self.cs.advice_queries, &self.advice), + &load(n, row, &self.cs.instance_queries, &self.instance), + &|a, b| a + &b, + &|a, b| a * &b, + &|a, scalar| a * scalar, + ) == F::zero() + { + None + } else { + Some(VerifyFailure::Constraint { + gate_index, + gate_name: gate.name(), + constraint_index: poly_index, + row: (row - n) as usize, + }) + } + }, + ) }) - }) - }); + }); // Check that all lookups exist in their respective tables. let lookup_errors = From ff2a500e9a20ac42f50ac90364cacdd16f23b6d9 Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Fri, 4 Jun 2021 03:18:11 +0100 Subject: [PATCH 3/4] dev: impl fmt::Display for VerifyFailure --- src/dev.rs | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/src/dev.rs b/src/dev.rs index 38966acc..b1a904d6 100644 --- a/src/dev.rs +++ b/src/dev.rs @@ -2,6 +2,7 @@ use std::collections::HashMap; use std::convert::TryInto; +use std::fmt; use std::iter; use ff::Field; @@ -82,6 +83,51 @@ pub enum VerifyFailure { }, } +impl fmt::Display for VerifyFailure { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Cell { + column, + row, + gate_index, + gate_name, + } => { + write!( + f, + "Cell ({:?}, {}) was not assigned to, but it is used by active gate {} ('{}').", + column, row, gate_index, gate_name + ) + } + Self::Constraint { + gate_index, + gate_name, + constraint_index, + row, + } => { + write!( + f, + "Constraint {} in gate {} ('{}') is not satisfied on row {}", + constraint_index, gate_index, gate_name, row + ) + } + Self::Lookup { lookup_index, row } => { + write!(f, "Lookup {} is not satisfied on row {}", lookup_index, row) + } + Self::Permutation { + perm_index, + column, + row, + } => { + write!( + f, + "Permutation {} is not satisfied by cell ({:?}, {})", + perm_index, column, row + ) + } + } + } +} + /// A test prover for debugging circuits. /// /// The normal proving process, when applied to a buggy circuit implementation, might From 483c872cbeb8956f87ec2cb33f71a4a3622b919c Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Fri, 4 Jun 2021 15:18:52 +0100 Subject: [PATCH 4/4] dev: Clarify gate name documentation --- src/dev.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/dev.rs b/src/dev.rs index b1a904d6..d291f269 100644 --- a/src/dev.rs +++ b/src/dev.rs @@ -41,7 +41,7 @@ pub enum VerifyFailure { /// `ConstraintSystem::create_gate` is called during `Circuit::configure`. gate_index: usize, /// The name of the active gate. These are specified by the gate creator (such as - /// a chip implementation), and may not be unique. + /// a chip implementation), and is not enforced to be unique. gate_name: &'static str, }, /// A constraint was not satisfied for a particular row. @@ -51,7 +51,8 @@ pub enum VerifyFailure { /// during `Circuit::configure`. gate_index: usize, /// The name of the gate containing the unsatisfied constraint. This is specified - /// by the gate creator (such as a chip implementation), and may not be unique. + /// by the gate creator (such as a chip implementation), and is not enforced to be + /// unique. gate_name: &'static str, /// The index of the polynomial constraint within the gate that is not satisfied. /// These indices correspond to the order in which the constraints are returned