Merge pull request #622 from zcash/patch-mockprover-query_instance

[MockProver] Check for instance values in gate queries.

halo2_proofs/src/dev.rs

@@ -283,7 +283,7 @@ pub struct MockProver<F: Group + Field> {
     // The advice cells in the circuit, arranged as [column][row].
     advice: Vec<Vec<CellValue<F>>>,
     // The instance cells in the circuit, arranged as [column][row].
-    instance: Vec<Vec<F>>,
+    instance: Vec<Vec<InstanceValue<F>>>,
 
     selectors: Vec<Vec<bool>>,
 
@@ -293,6 +293,21 @@ pub struct MockProver<F: Group + Field> {
     usable_rows: Range<usize>,
 }
 
+#[derive(Debug, Clone, PartialEq, Eq)]
+enum InstanceValue<F: Field> {
+    Assigned(F),
+    Padding,
+}
+
+impl<F: Field> InstanceValue<F> {
+    fn value(&self) -> F {
+        match self {
+            InstanceValue::Assigned(v) => *v,
+            InstanceValue::Padding => F::zero(),
+        }
+    }
+}
+
 impl<F: Field + Group> Assignment<F> for MockProver<F> {
     fn enter_region<NR, N>(&mut self, name: N)
     where
@@ -349,7 +364,7 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
         self.instance
             .get(column.index())
             .and_then(|column| column.get(row))
-            .map(|v| circuit::Value::known(*v))
+            .map(|v| circuit::Value::known(v.value()))
             .ok_or(Error::BoundsFailure)
     }
 
@@ -486,13 +501,17 @@ impl<F: FieldExt> MockProver<F> {
 
         let instance = instance
             .into_iter()
-            .map(|mut instance| {
+            .map(|instance| {
                 if instance.len() > n - (cs.blinding_factors() + 1) {
                     return Err(Error::InstanceTooLarge);
                 }
 
-                instance.resize(n, F::zero());
-                Ok(instance)
+                let mut instance_values = vec![InstanceValue::Padding; n];
+                for (idx, value) in instance.into_iter().enumerate() {
+                    instance_values[idx] = InstanceValue::Assigned(value);
+                }
+
+                Ok(instance_values)
             })
             .collect::<Result<Vec<_>, _>>()?;
 
@@ -576,17 +595,37 @@ impl<F: FieldExt> MockProver<F> {
                                 // Determine where this cell should have been assigned.
                                 let cell_row = ((gate_row + n + cell.rotation.0) % n) as usize;
 
-                                // Check that it was assigned!
-                                if r.cells.contains(&(cell.column, cell_row)) {
-                                    None
-                                } else {
-                                    Some(VerifyFailure::CellNotAssigned {
-                                        gate: (gate_index, gate.name()).into(),
-                                        region: (r_i, r.name.clone()).into(),
-                                        gate_offset: *selector_row,
-                                        column: cell.column,
-                                        offset: cell_row as isize - r.rows.unwrap().0 as isize,
-                                    })
+                                match cell.column.column_type() {
+                                    Any::Instance => {
+                                        // Handle instance cells, which are not in the region.
+                                        let instance_value =
+                                            &self.instance[cell.column.index()][cell_row];
+                                        match instance_value {
+                                            InstanceValue::Assigned(_) => None,
+                                            _ => Some(VerifyFailure::InstanceCellNotAssigned {
+                                                gate: (gate_index, gate.name()).into(),
+                                                region: (r_i, r.name.clone()).into(),
+                                                gate_offset: *selector_row,
+                                                column: cell.column.try_into().unwrap(),
+                                                row: cell_row,
+                                            }),
+                                        }
+                                    }
+                                    _ => {
+                                        // Check that it was assigned!
+                                        if r.cells.contains(&(cell.column, cell_row)) {
+                                            None
+                                        } else {
+                                            Some(VerifyFailure::CellNotAssigned {
+                                                gate: (gate_index, gate.name()).into(),
+                                                region: (r_i, r.name.clone()).into(),
+                                                gate_offset: *selector_row,
+                                                column: cell.column,
+                                                offset: cell_row as isize
+                                                    - r.rows.unwrap().0 as isize,
+                                            })
+                                        }
+                                    }
                                 }
                             })
                         })
@@ -693,7 +732,8 @@ impl<F: FieldExt> MockProver<F> {
                                 let rotation = query.1 .0;
                                 Value::Real(
                                     self.instance[column_index]
-                                        [(row as i32 + n + rotation) as usize % n as usize],
+                                        [(row as i32 + n + rotation) as usize % n as usize]
+                                        .value(),
                                 )
                             },
                             &|a| -a,
@@ -796,7 +836,10 @@ impl<F: FieldExt> MockProver<F> {
                     .map(|c: &Column<Any>| match c.column_type() {
                         Any::Advice => self.advice[c.index()][row],
                         Any::Fixed => self.fixed[c.index()][row],
-                        Any::Instance => CellValue::Assigned(self.instance[c.index()][row]),
+                        Any::Instance => {
+                            let cell: &InstanceValue<F> = &self.instance[c.index()][row];
+                            CellValue::Assigned(cell.value())
+                        }
                     })
                     .unwrap()
             };

halo2_proofs/src/dev/failure.rs

@@ -11,7 +11,7 @@ use super::{
 };
 use crate::{
     dev::Value,
-    plonk::{Any, Column, ConstraintSystem, Expression, Gate},
+    plonk::{Any, Column, ConstraintSystem, Expression, Gate, Instance},
 };
 
 mod emitter;
@@ -124,6 +124,20 @@ pub enum VerifyFailure {
         /// offset 0, but the gate uses `Rotation::prev()`).
         offset: isize,
     },
+    /// An instance cell used in an active gate was not assigned to.
+    InstanceCellNotAssigned {
+        /// The index of the active gate.
+        gate: metadata::Gate,
+        /// The region in which this gate was activated.
+        region: metadata::Region,
+        /// The offset (relative to the start of the region) at which the active gate
+        /// queries this cell.
+        gate_offset: usize,
+        /// The column in which this cell should be assigned.
+        column: Column<Instance>,
+        /// The absolute row at which this cell should be assigned.
+        row: usize,
+    },
     /// A constraint was not satisfied for a particular row.
     ConstraintNotSatisfied {
         /// The polynomial constraint that is not satisfied.
@@ -186,6 +200,19 @@ impl fmt::Display for VerifyFailure {
                     region, gate, gate_offset, column, offset
                 )
             }
+            Self::InstanceCellNotAssigned {
+                gate,
+                region,
+                gate_offset,
+                column,
+                row,
+            } => {
+                write!(
+                    f,
+                    "{} uses {} at offset {}, which requires cell in instance column {:?} at row {} to be assigned.",
+                    region, gate, gate_offset, column, row
+                )
+            }
             Self::ConstraintNotSatisfied {
                 constraint,
                 location,

halo2_proofs/src/dev/util.rs

@@ -3,7 +3,7 @@ use std::collections::BTreeMap;
 use group::ff::Field;
 use pasta_curves::arithmetic::FieldExt;
 
-use super::{metadata, CellValue, Value};
+use super::{metadata, CellValue, InstanceValue, Value};
 use crate::{
     plonk::{
         AdviceQuery, Any, Column, ColumnType, Expression, FixedQuery, Gate, InstanceQuery,
@@ -90,12 +90,13 @@ pub(super) fn load_instance<'a, F: FieldExt, T: ColumnType, Q: Into<AnyQuery> +
     n: i32,
     row: i32,
     queries: &'a [(Column<T>, Rotation)],
-    cells: &'a [Vec<F>],
+    cells: &'a [Vec<InstanceValue<F>>],
 ) -> impl Fn(Q) -> Value<F> + 'a {
     move |query| {
         let (column, at) = &queries[query.into().index];
         let resolved_row = (row + at.0) % n;
-        Value::Real(cells[column.index()][resolved_row as usize])
+        let cell = &cells[column.index()][resolved_row as usize];
+        Value::Real(cell.value())
     }
 }