diff --git a/src/dev.rs b/src/dev.rs index bea7da10..01556338 100644 --- a/src/dev.rs +++ b/src/dev.rs @@ -32,10 +32,20 @@ fn cell_value(cell: Option) -> F { pub enum VerifyFailure { /// A cell used in an active gate was not assigned to. Cell { - /// The column in which this cell is located. + /// The index of the region in which this cell should be assigned. These indices + /// are assigned in the order in which `Layouter::assign_region` is called during + /// `Circuit::synthesize`. + region_index: usize, + /// The name of the region in which this cell should be assigned. This is + /// specified by the region creator (such as a chip implementation), and is not + /// enforced to be unique. + region_name: String, + /// The column in which this cell should be assigned. column: Column, - /// The row in which this cell is located. - row: usize, + /// The offset (relative to the start of the region) at which this cell should be + /// assigned. This may be negative (for example, if a selector enables a gate at + /// offset 0, but the gate uses `Rotation::prev()`). + offset: isize, /// The index of the active gate. These indices are assigned in the order in which /// `ConstraintSystem::create_gate` is called during `Circuit::configure`. gate_index: usize, @@ -90,15 +100,17 @@ impl fmt::Display for VerifyFailure { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Self::Cell { + region_index, + region_name, column, - row, + offset, gate_index, gate_name, } => { write!( f, - "Cell ({:?}, {}) was not assigned to, but it is used by active gate {} ('{}').", - column, row, gate_index, gate_name + "Region {} ('{}') uses gate {} ('{}'), which requires cell in column {:?} at offset {} to be assigned.", + region_index, region_name, gate_index, gate_name, column, offset ) } Self::Constraint { @@ -140,6 +152,32 @@ impl fmt::Display for VerifyFailure { } } +#[derive(Debug)] +struct Region { + /// The name of the region. Not required to be unique. + name: String, + /// The row that this region starts on, if known. + start: Option, + /// The selectors that have been enabled in this region. All other selectors are by + /// construction not enabled. + enabled_selectors: HashMap>, + /// The cells assigned in this region. We store this as a `Vec` so that if any cells + /// are double-assigned, they will be visibly darker. + cells: Vec<(Column, usize)>, +} + +impl Region { + fn update_start(&mut self, row: usize) { + // The region start is the earliest row assigned to. + let mut start = self.start.unwrap_or(row); + if row < start { + // The first row assigned was not at start 0 within the region. + start = row; + } + self.start = Some(start); + } +} + /// A test prover for debugging circuits. /// /// The normal proving process, when applied to a buggy circuit implementation, might @@ -234,9 +272,11 @@ pub struct MockProver { n: u32, cs: ConstraintSystem, - /// The selectors that have been enabled in the circuit. All other selectors are by - /// construction not enabled. - enabled_selectors: HashMap>, + /// The regions in the circuit. + regions: Vec, + /// The current region being assigned to. Will be `None` after the circuit has been + /// synthesized. + current_region: Option, // The fixed cells in the circuit, arranged as [column][row]. fixed: Vec>>, @@ -249,14 +289,23 @@ pub struct MockProver { } impl Assignment for MockProver { - fn enter_region(&mut self, _: N) + fn enter_region(&mut self, name: N) where NR: Into, N: FnOnce() -> NR, { + assert!(self.current_region.is_none()); + self.current_region = Some(Region { + name: name().into(), + start: None, + enabled_selectors: HashMap::default(), + cells: vec![], + }); } - fn exit_region(&mut self) {} + fn exit_region(&mut self) { + self.regions.push(self.current_region.take().unwrap()); + } fn enable_selector( &mut self, @@ -268,8 +317,12 @@ impl Assignment for MockProver { A: FnOnce() -> AR, AR: Into, { - // Track that this selector was enabled. - self.enabled_selectors + // Track that this selector was enabled. We require that all selectors are enabled + // inside some region (i.e. no floating selectors). + self.current_region + .as_mut() + .unwrap() + .enabled_selectors .entry(*selector) .or_default() .push(row); @@ -290,6 +343,11 @@ impl Assignment for MockProver { A: FnOnce() -> AR, AR: Into, { + if let Some(region) = self.current_region.as_mut() { + region.update_start(row); + region.cells.push((column.into(), row)); + } + *self .advice .get_mut(column.index()) @@ -311,6 +369,11 @@ impl Assignment for MockProver { A: FnOnce() -> AR, AR: Into, { + if let Some(region) = self.current_region.as_mut() { + region.update_start(row); + region.cells.push((column.into(), row)); + } + *self .fixed .get_mut(column.index()) @@ -389,7 +452,8 @@ impl MockProver { let mut prover = MockProver { n, cs, - enabled_selectors: HashMap::default(), + regions: vec![], + current_region: None, fixed, advice, instance, @@ -406,14 +470,13 @@ impl MockProver { pub fn verify(&self) -> Result<(), Vec> { let n = self.n as i32; - // Check that all cells used in instantiated gates have been assigned to. - let selector_errors = self - .cs - .gates - .iter() - .enumerate() - .flat_map(|(gate_index, gate)| { - gate.queried_selectors() + // Check that within each region, all cells used in instantiated gates have been + // assigned to. + let selector_errors = self.regions.iter().enumerate().flat_map(|(r_i, r)| { + r.enabled_selectors.iter().flat_map(move |(selector, at)| { + // Find the gates enabled by this selector + self.cs + .gates .iter() // Assume that if a queried selector is enabled, the user wants to use the // corresponding gate in some way. @@ -422,8 +485,9 @@ impl MockProver { // un-enabled keeps a gate enabled. We could alternatively require that // every selector is explicitly enabled or disabled on every row? But that // seems messy and confusing. - .filter_map(|s| self.enabled_selectors.get(&s)) - .flat_map(move |at| { + .enumerate() + .filter(move |(_, g)| g.queried_selectors().contains(&selector)) + .flat_map(move |(gate_index, gate)| { at.iter().flat_map(move |selector_row| { // Selectors are queried with no rotation. let gate_row = *selector_row as i32; @@ -433,21 +497,14 @@ impl MockProver { let cell_row = ((gate_row + n + cell.rotation.0) % n) as usize; // Check that it was assigned! - if match cell.column.column_type() { - Any::Advice => { - self.advice[cell.column.index()][cell_row].is_some() - } - Any::Fixed => { - self.fixed[cell.column.index()][cell_row].is_some() - } - // Instance column cells are assigned outside the circuit. - Any::Instance => true, - } { + if r.cells.contains(&(cell.column, cell_row)) { None } else { Some(VerifyFailure::Cell { + region_index: r_i, + region_name: r.name.clone(), column: cell.column, - row: cell_row, + offset: cell_row as isize - r.start.unwrap() as isize, gate_index, gate_name: gate.name(), }) @@ -455,7 +512,8 @@ impl MockProver { }) }) }) - }); + }) + }); // Check that all gates are satisfied for all rows. let gate_errors = @@ -656,7 +714,6 @@ mod tests { #[test] fn unassigned_cell() { const K: u32 = 4; - const FAULTY_ROW: usize = 2; #[derive(Clone)] struct FaultyCircuitConfig { @@ -696,15 +753,10 @@ mod tests { || "Faulty synthesis", |mut region| { // Enable the equality gate. - config.q.enable(&mut region, FAULTY_ROW)?; + config.q.enable(&mut region, 1)?; // Assign a = 0. - region.assign_advice( - || "a", - config.a, - FAULTY_ROW - 1, - || Ok(Fp::zero()), - )?; + region.assign_advice(|| "a", config.a, 0, || Ok(Fp::zero()))?; // BUG: Forget to assign b = 0! This could go unnoticed during // development, because cell values default to zero, which in this @@ -719,8 +771,10 @@ mod tests { assert_eq!( prover.verify(), Err(vec![VerifyFailure::Cell { + region_index: 0, + region_name: "Faulty synthesis".to_owned(), column: Column::new(1, Any::Advice), - row: FAULTY_ROW, + offset: 1, gate_index: 0, gate_name: "Equality check" }])