From 7dae8698b6008f15a176b13e4efb06ae652235f3 Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Thu, 15 Jul 2021 22:12:50 +0100 Subject: [PATCH] MockProver: Poison unusable advice cells Circuit developers need to use selectors (or equivalent) to prevent their custom gates from being active on unusable rows. By marking the advice cells in these rows as "poisoned" and tracking this through expressions, we can provide a better error message to developers that indicates the missing selector issue. Closes zcash/halo2#329. --- src/dev.rs | 246 ++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 178 insertions(+), 68 deletions(-) diff --git a/src/dev.rs b/src/dev.rs index 564712e1..989b4f5d 100644 --- a/src/dev.rs +++ b/src/dev.rs @@ -3,7 +3,7 @@ use std::collections::HashMap; use std::fmt; use std::iter; -use std::ops::RangeTo; +use std::ops::{Add, Mul, Range}; use ff::Field; @@ -26,11 +26,6 @@ mod graph; #[cfg_attr(docsrs, doc(cfg(feature = "dev-graph")))] pub use graph::{circuit_dot_graph, layout::CircuitLayout}; -/// Cells that haven't been explicitly assigned to, default to zero. -fn cell_value(cell: Option) -> F { - cell.unwrap_or_else(F::zero) -} - /// The reasons why a particular circuit is not satisfied. #[derive(Debug, PartialEq)] pub enum VerifyFailure { @@ -48,12 +43,17 @@ pub enum VerifyFailure { offset: isize, }, /// A constraint was not satisfied for a particular row. - Constraint { + ConstraintNotSatisfied { /// The polynomial constraint that is not satisfied. constraint: metadata::Constraint, /// The row on which this constraint is not satisfied. row: usize, }, + /// A constraint was active on an unusable row, and is likely missing a selector. + ConstraintPoisoned { + /// The polynomial constraint that is not satisfied. + constraint: metadata::Constraint, + }, /// A lookup input did not exist in its corresponding table. Lookup { /// The index of the lookup that is not satisfied. These indices are assigned in @@ -87,9 +87,16 @@ impl fmt::Display for VerifyFailure { region, gate, column, offset ) } - Self::Constraint { constraint, row } => { + Self::ConstraintNotSatisfied { constraint, row } => { write!(f, "{} is not satisfied on row {}", constraint, row) } + Self::ConstraintPoisoned { constraint } => { + write!( + f, + "{} is active on an unusable row - missing selector?", + constraint + ) + } Self::Lookup { lookup_index, row } => { write!(f, "Lookup {} is not satisfied on row {}", lookup_index, row) } @@ -130,6 +137,76 @@ impl Region { } } +/// The value of a particular cell within the circuit. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum CellValue { + // An unassigned cell. + Unassigned, + // A cell that has been assigned a value. + Assigned(F), + // A unique poisoned cell. + Poison(usize), +} + +/// A value within an expression. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum Value { + Real(F), + Poison, +} + +impl From> for Value { + fn from(value: CellValue) -> Self { + match value { + // Cells that haven't been explicitly assigned to, default to zero. + CellValue::Unassigned => Value::Real(F::zero()), + CellValue::Assigned(v) => Value::Real(v), + CellValue::Poison(_) => Value::Poison, + } + } +} + +impl Add for Value { + type Output = Self; + + fn add(self, rhs: Self) -> Self::Output { + match (self, rhs) { + (Value::Real(a), Value::Real(b)) => Value::Real(a + b), + _ => Value::Poison, + } + } +} + +impl Mul for Value { + type Output = Self; + + fn mul(self, rhs: Self) -> Self::Output { + match (self, rhs) { + (Value::Real(a), Value::Real(b)) => Value::Real(a * b), + // If poison is multiplied by zero, then we treat the poison as unconstrained + // and we don't propagate it. + (Value::Real(x), Value::Poison) | (Value::Poison, Value::Real(x)) if x.is_zero() => { + Value::Real(F::zero()) + } + _ => Value::Poison, + } + } +} + +impl Mul for Value { + type Output = Self; + + fn mul(self, rhs: F) -> Self::Output { + match self { + Value::Real(lhs) => Value::Real(lhs * rhs), + // If poison is multiplied by zero, then we treat the poison as unconstrained + // and we don't propagate it. + Value::Poison if rhs.is_zero() => Value::Real(F::zero()), + _ => Value::Poison, + } + } +} + /// A test prover for debugging circuits. /// /// The normal proving process, when applied to a buggy circuit implementation, might @@ -146,7 +223,7 @@ impl Region { /// circuit::{Layouter, SimpleFloorPlanner}, /// dev::{MockProver, VerifyFailure}, /// pasta::Fp, -/// plonk::{Advice, Circuit, Column, ConstraintSystem, Error}, +/// plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Selector}, /// poly::Rotation, /// }; /// const K: u32 = 5; @@ -156,6 +233,7 @@ impl Region { /// a: Column, /// b: Column, /// c: Column, +/// s: Selector, /// } /// /// #[derive(Clone, Default)] @@ -176,21 +254,24 @@ impl Region { /// let a = meta.advice_column(); /// let b = meta.advice_column(); /// let c = meta.advice_column(); +/// let s = meta.selector(); /// /// meta.create_gate("R1CS constraint", |meta| { /// 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 s = meta.query_selector(s); /// /// // BUG: Should be a * b - c -/// Some(("buggy R1CS", a * b + c)) +/// Some(("buggy R1CS", s * (a * b + c))) /// }); /// -/// MyConfig { a, b, c } +/// MyConfig { a, b, c, s } /// } /// /// fn synthesize(&self, config: MyConfig, mut layouter: impl Layouter) -> Result<(), Error> { /// layouter.assign_region(|| "Example region", |mut region| { +/// config.s.enable(&mut region, 0)?; /// region.assign_advice(|| "a", config.a, 0, || { /// self.a.map(|v| F::from_u64(v)).ok_or(Error::SynthesisError) /// })?; @@ -219,7 +300,7 @@ impl Region { /// let prover = MockProver::::run(K, &circuit, instance).unwrap(); /// assert_eq!( /// prover.verify(), -/// Err(vec![VerifyFailure::Constraint { +/// Err(vec![VerifyFailure::ConstraintNotSatisfied { /// constraint: ((0, "R1CS constraint").into(), 0, "buggy R1CS").into(), /// row: 0 /// }]) @@ -237,16 +318,16 @@ pub struct MockProver { current_region: Option, // The fixed cells in the circuit, arranged as [column][row]. - fixed: Vec>>, + fixed: Vec>>, // The advice cells in the circuit, arranged as [column][row]. - advice: Vec>>, + advice: Vec>>, // The instance cells in the circuit, arranged as [column][row]. instance: Vec>, permutation: permutation::keygen::Assembly, // A range of available rows for assignment and copies. - usable_rows: RangeTo, + usable_rows: Range, } impl Assignment for MockProver { @@ -334,7 +415,7 @@ impl Assignment for MockProver { .advice .get_mut(column.index()) .and_then(|v| v.get_mut(row)) - .ok_or(Error::BoundsFailure)? = Some(to()?.into().evaluate()); + .ok_or(Error::BoundsFailure)? = CellValue::Assigned(to()?.into().evaluate()); Ok(()) } @@ -365,7 +446,7 @@ impl Assignment for MockProver { .fixed .get_mut(column.index()) .and_then(|v| v.get_mut(row)) - .ok_or(Error::BoundsFailure)? = Some(to()?.into().evaluate()); + .ok_or(Error::BoundsFailure)? = CellValue::Assigned(to()?.into().evaluate()); Ok(()) } @@ -432,11 +513,24 @@ impl MockProver { }) .collect::, _>>()?; - let fixed = vec![vec![None; n]; cs.num_fixed_columns]; - let advice = vec![vec![None; n]; cs.num_advice_columns]; + // Fixed columns contain no blinding factors. + let fixed = vec![vec![CellValue::Unassigned; n]; cs.num_fixed_columns]; + // Advice columns contain blinding factors. + let blinding_factors = cs.blinding_factors(); + let usable_rows = n - (blinding_factors + 1); + let advice = vec![ + { + let mut column = vec![CellValue::Unassigned; n]; + // Poison unusable rows. + for (i, cell) in column.iter_mut().enumerate().skip(usable_rows) { + *cell = CellValue::Poison(i); + } + column + }; + cs.num_advice_columns + ]; let permutation = permutation::keygen::Assembly::new(n, &cs.permutation); - let blinding_factors = cs.blinding_factors(); let mut prover = MockProver { n: n as u32, cs, @@ -446,7 +540,7 @@ impl MockProver { advice, instance, permutation, - usable_rows: ..n - (blinding_factors + 1), + usable_rows: 0..usable_rows, }; ConcreteCircuit::FloorPlanner::synthesize(&mut prover, circuit, config)?; @@ -511,16 +605,16 @@ impl MockProver { .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>( + fn load_instance<'a, F: FieldExt, T: ColumnType>( n: i32, row: i32, queries: &'a [(Column, Rotation)], - cells: &'a [Vec>], - ) -> impl Fn(usize) -> F + 'a { + cells: &'a [Vec], + ) -> impl Fn(usize) -> Value + 'a { move |index| { let (column, at) = &queries[index]; let resolved_row = (row + at.0) % n; - cell_value(cells[column.index()][resolved_row as usize]) + Value::Real(cells[column.index()][resolved_row as usize]) } } @@ -528,39 +622,43 @@ impl MockProver { n: i32, row: i32, queries: &'a [(Column, Rotation)], - cells: &'a [Vec], - ) -> impl Fn(usize) -> F + 'a { + cells: &'a [Vec>], + ) -> impl Fn(usize) -> Value + 'a { move |index| { let (column, at) = &queries[index]; let resolved_row = (row + at.0) % n; - cells[column.index()][resolved_row as usize] + cells[column.index()][resolved_row as usize].into() } } 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 { - constraint: ( - (gate_index, gate.name()).into(), - poly_index, - gate.constraint_name(poly_index), - ) - .into(), - row: (row - n) as usize, - }) - } + move |(poly_index, poly)| match poly.evaluate( + &|scalar| Value::Real(scalar), + &load(n, row, &self.cs.fixed_queries, &self.fixed), + &load(n, row, &self.cs.advice_queries, &self.advice), + &load_instance(n, row, &self.cs.instance_queries, &self.instance), + &|a, b| a + b, + &|a, b| a * b, + &|a, scalar| a * scalar, + ) { + Value::Real(x) if x.is_zero() => None, + Value::Real(_) => Some(VerifyFailure::ConstraintNotSatisfied { + constraint: ( + (gate_index, gate.name()).into(), + poly_index, + gate.constraint_name(poly_index), + ) + .into(), + row: (row - n) as usize, + }), + Value::Poison => Some(VerifyFailure::ConstraintPoisoned { + constraint: ( + (gate_index, gate.name()).into(), + poly_index, + gate.constraint_name(poly_index), + ) + .into(), + }), }, ) }) @@ -573,34 +671,36 @@ impl MockProver { .iter() .enumerate() .flat_map(|(lookup_index, lookup)| { - (0..n).filter_map(move |input_row| { + // In the real prover, the lookup expressions are never enforced on + // unusable rows, due to the (1 - (l_last(X) + l_blind(X))) term. + self.usable_rows.clone().filter_map(move |input_row| { let load = |expression: &Expression, row| { expression.evaluate( - &|scalar| scalar, + &|scalar| Value::Real(scalar), &|index| { let query = self.cs.fixed_queries[index]; let column_index = query.0.index(); let rotation = query.1 .0; - cell_value( - self.fixed[column_index] - [(row as i32 + n + rotation) as usize % n as usize], - ) + self.fixed[column_index] + [(row as i32 + n + rotation) as usize % n as usize] + .into() }, &|index| { let query = self.cs.advice_queries[index]; let column_index = query.0.index(); let rotation = query.1 .0; - cell_value( - self.advice[column_index] - [(row as i32 + n + rotation) as usize % n as usize], - ) + self.advice[column_index] + [(row as i32 + n + rotation) as usize % n as usize] + .into() }, &|index| { let query = self.cs.instance_queries[index]; let column_index = query.0.index(); let rotation = query.1 .0; - self.instance[column_index] - [(row as i32 + n + rotation) as usize % n as usize] + Value::Real( + self.instance[column_index] + [(row as i32 + n + rotation) as usize % n as usize], + ) }, &|a, b| a + b, &|a, b| a * b, @@ -613,7 +713,7 @@ impl MockProver { .iter() .map(|c| load(c, input_row)) .collect(); - let lookup_passes = (0..n) + let lookup_passes = (0..n as usize) .map(|table_row| { lookup .table_expressions @@ -641,9 +741,9 @@ impl MockProver { .get_columns() .get(column) .map(|c: &Column| match c.column_type() { - Any::Advice => cell_value(self.advice[c.index()][row]), - Any::Fixed => cell_value(self.fixed[c.index()][row]), - Any::Instance => self.instance[c.index()][row], + Any::Advice => self.advice[c.index()][row], + Any::Fixed => self.fixed[c.index()][row], + Any::Instance => CellValue::Assigned(self.instance[c.index()][row]), }) .unwrap() }; @@ -671,7 +771,7 @@ impl MockProver { }) }; - let errors: Vec<_> = iter::empty() + let mut errors: Vec<_> = iter::empty() .chain(selector_errors) .chain(gate_errors) .chain(lookup_errors) @@ -680,6 +780,16 @@ impl MockProver { if errors.is_empty() { Ok(()) } else { + // Remove any duplicate `ConstraintPoisoned` errors (we check all unavailable + // rows in case the trigger is row-specific, but the error message only points + // at the constraint). + errors.dedup_by(|a, b| match (a, b) { + ( + a @ VerifyFailure::ConstraintPoisoned { .. }, + b @ VerifyFailure::ConstraintPoisoned { .. }, + ) => a == b, + _ => false, + }); Err(errors) } }