2020-12-21 15:00:39 -08:00
|
|
|
//! Tools for developing circuits.
|
|
|
|
|
2021-05-27 06:03:12 -07:00
|
|
|
use std::collections::HashMap;
|
2021-06-03 19:18:11 -07:00
|
|
|
use std::fmt;
|
2021-05-27 06:03:12 -07:00
|
|
|
use std::iter;
|
|
|
|
|
2020-12-21 15:00:39 -08:00
|
|
|
use ff::Field;
|
|
|
|
|
2021-06-11 08:39:34 -07:00
|
|
|
use crate::plonk::Assigned;
|
2020-12-21 15:00:39 -08:00
|
|
|
use crate::{
|
|
|
|
arithmetic::{FieldExt, Group},
|
2021-01-22 08:57:38 -08:00
|
|
|
plonk::{
|
2021-02-18 23:07:08 -08:00
|
|
|
permutation, Advice, Any, Assignment, Circuit, Column, ColumnType, ConstraintSystem, Error,
|
2021-06-21 11:10:59 -07:00
|
|
|
Expression, Fixed, FloorPlanner, Permutation, Selector,
|
2021-01-22 08:57:38 -08:00
|
|
|
},
|
2021-01-07 04:42:04 -08:00
|
|
|
poly::Rotation,
|
2020-12-21 15:00:39 -08:00
|
|
|
};
|
|
|
|
|
2021-06-23 05:14:49 -07:00
|
|
|
pub mod metadata;
|
|
|
|
|
2021-01-22 13:13:11 -08:00
|
|
|
#[cfg(feature = "dev-graph")]
|
|
|
|
mod graph;
|
|
|
|
|
|
|
|
#[cfg(feature = "dev-graph")]
|
|
|
|
#[cfg_attr(docsrs, doc(cfg(feature = "dev-graph")))]
|
2021-06-08 04:06:48 -07:00
|
|
|
pub use graph::{circuit_dot_graph, layout::CircuitLayout};
|
2021-01-22 13:13:11 -08:00
|
|
|
|
2021-05-27 06:03:12 -07:00
|
|
|
/// Cells that haven't been explicitly assigned to, default to zero.
|
|
|
|
fn cell_value<F: Field>(cell: Option<F>) -> F {
|
|
|
|
cell.unwrap_or_else(F::zero)
|
|
|
|
}
|
|
|
|
|
2020-12-21 15:00:39 -08:00
|
|
|
/// The reasons why a particular circuit is not satisfied.
|
|
|
|
#[derive(Debug, PartialEq)]
|
|
|
|
pub enum VerifyFailure {
|
2021-05-27 06:02:13 -07:00
|
|
|
/// A cell used in an active gate was not assigned to.
|
|
|
|
Cell {
|
2021-06-23 05:14:49 -07:00
|
|
|
/// The index of the active gate.
|
|
|
|
gate: metadata::Gate,
|
|
|
|
/// The region in which this cell should be assigned.
|
|
|
|
region: metadata::Region,
|
2021-06-18 09:25:02 -07:00
|
|
|
/// The column in which this cell should be assigned.
|
2021-05-27 06:02:13 -07:00
|
|
|
column: Column<Any>,
|
2021-06-18 09:25:02 -07:00
|
|
|
/// 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,
|
2021-05-27 06:02:13 -07:00
|
|
|
},
|
2021-06-03 19:01:09 -07:00
|
|
|
/// A constraint was not satisfied for a particular row.
|
|
|
|
Constraint {
|
2021-06-23 05:14:49 -07:00
|
|
|
/// The polynomial constraint that is not satisfied.
|
|
|
|
constraint: metadata::Constraint,
|
2021-06-03 19:01:09 -07:00
|
|
|
/// The row on which this constraint is not satisfied.
|
2020-12-23 11:32:39 -08:00
|
|
|
row: usize,
|
|
|
|
},
|
2020-12-21 15:00:39 -08:00
|
|
|
/// A lookup input did not exist in its corresponding table.
|
2020-12-23 11:32:39 -08:00
|
|
|
Lookup {
|
|
|
|
/// The index of the lookup that is not satisfied. These indices are assigned in
|
|
|
|
/// the order in which `ConstraintSystem::lookup` is called during
|
|
|
|
/// `Circuit::configure`.
|
|
|
|
lookup_index: usize,
|
|
|
|
/// The row on which this lookup is not satisfied.
|
|
|
|
row: usize,
|
|
|
|
},
|
2020-12-21 21:56:30 -08:00
|
|
|
/// A permutation did not preserve the original value of a cell.
|
|
|
|
Permutation {
|
2020-12-23 11:32:39 -08:00
|
|
|
/// The index of the permutation that is not satisfied. These indices are assigned
|
|
|
|
/// in the order in which `ConstraintSystem::lookup` is called during
|
|
|
|
/// `Circuit::configure`.
|
2020-12-21 21:56:30 -08:00
|
|
|
perm_index: usize,
|
2020-12-23 11:32:39 -08:00
|
|
|
/// The column in which this permutation is not satisfied.
|
2020-12-21 21:56:30 -08:00
|
|
|
column: usize,
|
2020-12-23 11:32:39 -08:00
|
|
|
/// The row on which this permutation is not satisfied.
|
2020-12-21 21:56:30 -08:00
|
|
|
row: usize,
|
|
|
|
},
|
2020-12-21 15:00:39 -08:00
|
|
|
}
|
|
|
|
|
2021-06-03 19:18:11 -07:00
|
|
|
impl fmt::Display for VerifyFailure {
|
|
|
|
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
|
|
|
match self {
|
|
|
|
Self::Cell {
|
2021-06-23 05:14:49 -07:00
|
|
|
gate,
|
|
|
|
region,
|
2021-06-03 19:18:11 -07:00
|
|
|
column,
|
2021-06-18 09:25:02 -07:00
|
|
|
offset,
|
2021-06-03 19:18:11 -07:00
|
|
|
} => {
|
|
|
|
write!(
|
|
|
|
f,
|
2021-06-23 05:14:49 -07:00
|
|
|
"{} uses {}, which requires cell in column {:?} at offset {} to be assigned.",
|
|
|
|
region, gate, column, offset
|
2021-06-03 19:18:11 -07:00
|
|
|
)
|
|
|
|
}
|
2021-06-23 05:14:49 -07:00
|
|
|
Self::Constraint { constraint, row } => {
|
|
|
|
write!(f, "{} is not satisfied on row {}", constraint, row)
|
2021-06-03 19:18:11 -07:00
|
|
|
}
|
|
|
|
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
|
|
|
|
)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2021-06-18 08:48:25 -07:00
|
|
|
#[derive(Debug)]
|
|
|
|
struct Region {
|
|
|
|
/// The name of the region. Not required to be unique.
|
|
|
|
name: String,
|
2021-06-18 09:25:02 -07:00
|
|
|
/// The row that this region starts on, if known.
|
|
|
|
start: Option<usize>,
|
2021-06-18 08:48:25 -07:00
|
|
|
/// The selectors that have been enabled in this region. All other selectors are by
|
|
|
|
/// construction not enabled.
|
|
|
|
enabled_selectors: HashMap<Selector, Vec<usize>>,
|
|
|
|
/// 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<Any>, usize)>,
|
|
|
|
}
|
|
|
|
|
2021-06-18 09:25:02 -07:00
|
|
|
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);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-12-23 11:32:39 -08:00
|
|
|
/// A test prover for debugging circuits.
|
|
|
|
///
|
|
|
|
/// The normal proving process, when applied to a buggy circuit implementation, might
|
|
|
|
/// return proofs that do not validate when they should, but it can't indicate anything
|
|
|
|
/// other than "something is invalid". `MockProver` can be used to figure out _why_ these
|
|
|
|
/// are invalid: it stores all the private inputs along with the circuit internals, and
|
|
|
|
/// then checks every constraint manually.
|
2020-12-23 11:33:31 -08:00
|
|
|
///
|
|
|
|
/// # Examples
|
|
|
|
///
|
|
|
|
/// ```
|
|
|
|
/// use halo2::{
|
|
|
|
/// arithmetic::FieldExt,
|
2021-06-21 11:10:59 -07:00
|
|
|
/// circuit::{Layouter, SimpleFloorPlanner},
|
2020-12-23 11:33:31 -08:00
|
|
|
/// dev::{MockProver, VerifyFailure},
|
|
|
|
/// pasta::Fp,
|
2021-06-21 11:10:59 -07:00
|
|
|
/// plonk::{Advice, Circuit, Column, ConstraintSystem, Error},
|
2021-01-14 12:31:48 -08:00
|
|
|
/// poly::Rotation,
|
2020-12-23 11:33:31 -08:00
|
|
|
/// };
|
|
|
|
/// const K: u32 = 5;
|
|
|
|
///
|
2021-01-20 05:48:51 -08:00
|
|
|
/// #[derive(Copy, Clone)]
|
2020-12-23 11:33:31 -08:00
|
|
|
/// struct MyConfig {
|
|
|
|
/// a: Column<Advice>,
|
|
|
|
/// b: Column<Advice>,
|
|
|
|
/// c: Column<Advice>,
|
|
|
|
/// }
|
|
|
|
///
|
2021-06-21 11:10:59 -07:00
|
|
|
/// #[derive(Clone, Default)]
|
2020-12-23 11:33:31 -08:00
|
|
|
/// struct MyCircuit {
|
|
|
|
/// a: Option<u64>,
|
|
|
|
/// b: Option<u64>,
|
|
|
|
/// }
|
|
|
|
///
|
|
|
|
/// impl<F: FieldExt> Circuit<F> for MyCircuit {
|
|
|
|
/// type Config = MyConfig;
|
2021-06-21 11:10:59 -07:00
|
|
|
/// type FloorPlanner = SimpleFloorPlanner;
|
|
|
|
///
|
|
|
|
/// fn without_witnesses(&self) -> Self {
|
|
|
|
/// Self::default()
|
|
|
|
/// }
|
2020-12-23 11:33:31 -08:00
|
|
|
///
|
|
|
|
/// fn configure(meta: &mut ConstraintSystem<F>) -> MyConfig {
|
|
|
|
/// let a = meta.advice_column();
|
|
|
|
/// let b = meta.advice_column();
|
|
|
|
/// let c = meta.advice_column();
|
|
|
|
///
|
2021-01-22 11:46:06 -08:00
|
|
|
/// meta.create_gate("R1CS constraint", |meta| {
|
2021-01-14 12:31:48 -08:00
|
|
|
/// let a = meta.query_advice(a, Rotation::cur());
|
|
|
|
/// let b = meta.query_advice(b, Rotation::cur());
|
|
|
|
/// let c = meta.query_advice(c, Rotation::cur());
|
2020-12-23 11:33:31 -08:00
|
|
|
///
|
|
|
|
/// // BUG: Should be a * b - c
|
2021-06-03 19:41:06 -07:00
|
|
|
/// Some(("buggy R1CS", a * b + c))
|
2020-12-23 11:33:31 -08:00
|
|
|
/// });
|
|
|
|
///
|
|
|
|
/// MyConfig { a, b, c }
|
|
|
|
/// }
|
|
|
|
///
|
2021-06-21 11:10:59 -07:00
|
|
|
/// fn synthesize(&self, config: MyConfig, mut layouter: impl Layouter<F>) -> Result<(), Error> {
|
|
|
|
/// layouter.assign_region(|| "Example region", |mut region| {
|
|
|
|
/// region.assign_advice(|| "a", config.a, 0, || {
|
|
|
|
/// self.a.map(|v| F::from_u64(v)).ok_or(Error::SynthesisError)
|
|
|
|
/// })?;
|
|
|
|
/// region.assign_advice(|| "b", config.b, 0, || {
|
|
|
|
/// self.b.map(|v| F::from_u64(v)).ok_or(Error::SynthesisError)
|
|
|
|
/// })?;
|
|
|
|
/// region.assign_advice(|| "c", config.c, 0, || {
|
|
|
|
/// self.a
|
|
|
|
/// .and_then(|a| self.b.map(|b| F::from_u64(a * b)))
|
|
|
|
/// .ok_or(Error::SynthesisError)
|
|
|
|
/// })?;
|
|
|
|
/// Ok(())
|
2020-12-23 11:33:31 -08:00
|
|
|
/// })
|
|
|
|
/// }
|
|
|
|
/// }
|
|
|
|
///
|
|
|
|
/// // Assemble the private inputs to the circuit.
|
|
|
|
/// let circuit = MyCircuit {
|
|
|
|
/// a: Some(2),
|
|
|
|
/// b: Some(4),
|
|
|
|
/// };
|
|
|
|
///
|
|
|
|
/// // This circuit has no public inputs.
|
2021-02-14 09:30:36 -08:00
|
|
|
/// let instance = vec![];
|
2020-12-23 11:33:31 -08:00
|
|
|
///
|
2021-02-14 09:30:36 -08:00
|
|
|
/// let prover = MockProver::<Fp>::run(K, &circuit, instance).unwrap();
|
2020-12-23 11:33:31 -08:00
|
|
|
/// assert_eq!(
|
|
|
|
/// prover.verify(),
|
2021-06-03 19:01:09 -07:00
|
|
|
/// Err(vec![VerifyFailure::Constraint {
|
2021-06-23 05:14:49 -07:00
|
|
|
/// constraint: ((0, "R1CS constraint").into(), 0, "buggy R1CS").into(),
|
2020-12-23 11:33:31 -08:00
|
|
|
/// row: 0
|
2021-05-18 08:32:15 -07:00
|
|
|
/// }])
|
2020-12-23 11:33:31 -08:00
|
|
|
/// );
|
|
|
|
/// ```
|
2020-12-23 11:32:39 -08:00
|
|
|
#[derive(Debug)]
|
2021-02-10 03:36:25 -08:00
|
|
|
pub struct MockProver<F: Group + Field> {
|
2020-12-21 15:00:39 -08:00
|
|
|
n: u32,
|
|
|
|
cs: ConstraintSystem<F>,
|
|
|
|
|
2021-06-18 08:48:25 -07:00
|
|
|
/// The regions in the circuit.
|
|
|
|
regions: Vec<Region>,
|
|
|
|
/// The current region being assigned to. Will be `None` after the circuit has been
|
|
|
|
/// synthesized.
|
|
|
|
current_region: Option<Region>,
|
2021-05-27 06:03:12 -07:00
|
|
|
|
2020-12-21 15:00:39 -08:00
|
|
|
// The fixed cells in the circuit, arranged as [column][row].
|
2021-05-27 06:03:12 -07:00
|
|
|
fixed: Vec<Vec<Option<F>>>,
|
2020-12-21 15:00:39 -08:00
|
|
|
// The advice cells in the circuit, arranged as [column][row].
|
2021-05-27 06:03:12 -07:00
|
|
|
advice: Vec<Vec<Option<F>>>,
|
2021-02-14 09:30:36 -08:00
|
|
|
// The instance cells in the circuit, arranged as [column][row].
|
|
|
|
instance: Vec<Vec<F>>,
|
2020-12-21 15:00:39 -08:00
|
|
|
|
2020-12-21 21:56:30 -08:00
|
|
|
permutations: Vec<permutation::keygen::Assembly>,
|
2020-12-21 15:00:39 -08:00
|
|
|
}
|
|
|
|
|
|
|
|
impl<F: Field + Group> Assignment<F> for MockProver<F> {
|
2021-06-18 08:48:25 -07:00
|
|
|
fn enter_region<NR, N>(&mut self, name: N)
|
2021-01-22 08:43:36 -08:00
|
|
|
where
|
|
|
|
NR: Into<String>,
|
|
|
|
N: FnOnce() -> NR,
|
|
|
|
{
|
2021-06-18 08:48:25 -07:00
|
|
|
assert!(self.current_region.is_none());
|
|
|
|
self.current_region = Some(Region {
|
|
|
|
name: name().into(),
|
2021-06-18 09:25:02 -07:00
|
|
|
start: None,
|
2021-06-18 08:48:25 -07:00
|
|
|
enabled_selectors: HashMap::default(),
|
|
|
|
cells: vec![],
|
|
|
|
});
|
2021-01-22 08:43:36 -08:00
|
|
|
}
|
|
|
|
|
2021-06-18 08:48:25 -07:00
|
|
|
fn exit_region(&mut self) {
|
|
|
|
self.regions.push(self.current_region.take().unwrap());
|
|
|
|
}
|
2021-01-22 08:43:36 -08:00
|
|
|
|
2021-05-27 04:43:32 -07:00
|
|
|
fn enable_selector<A, AR>(
|
|
|
|
&mut self,
|
|
|
|
annotation: A,
|
|
|
|
selector: &Selector,
|
|
|
|
row: usize,
|
|
|
|
) -> Result<(), Error>
|
|
|
|
where
|
|
|
|
A: FnOnce() -> AR,
|
|
|
|
AR: Into<String>,
|
|
|
|
{
|
2021-06-18 08:48:25 -07:00
|
|
|
// 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
|
2021-05-27 06:03:12 -07:00
|
|
|
.entry(*selector)
|
|
|
|
.or_default()
|
|
|
|
.push(row);
|
|
|
|
|
2021-05-27 04:43:32 -07:00
|
|
|
// Selectors are just fixed columns.
|
|
|
|
self.assign_fixed(annotation, selector.0, row, || Ok(F::one()))
|
|
|
|
}
|
|
|
|
|
2021-06-11 08:39:34 -07:00
|
|
|
fn assign_advice<V, VR, A, AR>(
|
2020-12-21 15:00:39 -08:00
|
|
|
&mut self,
|
2021-01-22 08:57:38 -08:00
|
|
|
_: A,
|
|
|
|
column: Column<Advice>,
|
2020-12-21 15:00:39 -08:00
|
|
|
row: usize,
|
2021-01-22 08:57:38 -08:00
|
|
|
to: V,
|
|
|
|
) -> Result<(), Error>
|
|
|
|
where
|
2021-06-11 08:39:34 -07:00
|
|
|
V: FnOnce() -> Result<VR, Error>,
|
|
|
|
VR: Into<Assigned<F>>,
|
2021-01-22 08:57:38 -08:00
|
|
|
A: FnOnce() -> AR,
|
|
|
|
AR: Into<String>,
|
|
|
|
{
|
2021-06-18 08:48:25 -07:00
|
|
|
if let Some(region) = self.current_region.as_mut() {
|
2021-06-18 09:25:02 -07:00
|
|
|
region.update_start(row);
|
2021-06-18 08:48:25 -07:00
|
|
|
region.cells.push((column.into(), row));
|
|
|
|
}
|
|
|
|
|
2020-12-21 15:00:39 -08:00
|
|
|
*self
|
|
|
|
.advice
|
|
|
|
.get_mut(column.index())
|
|
|
|
.and_then(|v| v.get_mut(row))
|
2021-06-11 08:39:34 -07:00
|
|
|
.ok_or(Error::BoundsFailure)? = Some(to()?.into().evaluate());
|
2020-12-21 15:00:39 -08:00
|
|
|
|
|
|
|
Ok(())
|
|
|
|
}
|
|
|
|
|
2021-06-11 08:39:34 -07:00
|
|
|
fn assign_fixed<V, VR, A, AR>(
|
2020-12-21 15:00:39 -08:00
|
|
|
&mut self,
|
2021-01-22 08:57:38 -08:00
|
|
|
_: A,
|
|
|
|
column: Column<Fixed>,
|
2020-12-21 15:00:39 -08:00
|
|
|
row: usize,
|
2021-01-22 08:57:38 -08:00
|
|
|
to: V,
|
|
|
|
) -> Result<(), Error>
|
|
|
|
where
|
2021-06-11 08:39:34 -07:00
|
|
|
V: FnOnce() -> Result<VR, Error>,
|
|
|
|
VR: Into<Assigned<F>>,
|
2021-01-22 08:57:38 -08:00
|
|
|
A: FnOnce() -> AR,
|
|
|
|
AR: Into<String>,
|
|
|
|
{
|
2021-06-18 08:48:25 -07:00
|
|
|
if let Some(region) = self.current_region.as_mut() {
|
2021-06-18 09:25:02 -07:00
|
|
|
region.update_start(row);
|
2021-06-18 08:48:25 -07:00
|
|
|
region.cells.push((column.into(), row));
|
|
|
|
}
|
|
|
|
|
2020-12-21 15:00:39 -08:00
|
|
|
*self
|
|
|
|
.fixed
|
|
|
|
.get_mut(column.index())
|
|
|
|
.and_then(|v| v.get_mut(row))
|
2021-06-11 08:39:34 -07:00
|
|
|
.ok_or(Error::BoundsFailure)? = Some(to()?.into().evaluate());
|
2020-12-21 15:00:39 -08:00
|
|
|
|
|
|
|
Ok(())
|
|
|
|
}
|
|
|
|
|
|
|
|
fn copy(
|
|
|
|
&mut self,
|
2021-02-18 22:53:26 -08:00
|
|
|
permutation: &Permutation,
|
2021-02-18 23:07:08 -08:00
|
|
|
left_column: Column<Any>,
|
2020-12-21 15:00:39 -08:00
|
|
|
left_row: usize,
|
2021-02-18 23:07:08 -08:00
|
|
|
right_column: Column<Any>,
|
2020-12-21 15:00:39 -08:00
|
|
|
right_row: usize,
|
|
|
|
) -> Result<(), crate::plonk::Error> {
|
2020-12-21 21:56:30 -08:00
|
|
|
// Check bounds first
|
2021-02-18 22:53:26 -08:00
|
|
|
if permutation.index() >= self.permutations.len() {
|
2020-12-21 21:56:30 -08:00
|
|
|
return Err(Error::BoundsFailure);
|
|
|
|
}
|
|
|
|
|
2021-02-18 23:07:08 -08:00
|
|
|
let left_column_index = permutation
|
|
|
|
.mapping()
|
|
|
|
.iter()
|
|
|
|
.position(|c| c == &left_column)
|
|
|
|
.ok_or(Error::SynthesisError)?;
|
|
|
|
let right_column_index = permutation
|
|
|
|
.mapping()
|
|
|
|
.iter()
|
|
|
|
.position(|c| c == &right_column)
|
|
|
|
.ok_or(Error::SynthesisError)?;
|
|
|
|
|
|
|
|
self.permutations[permutation.index()].copy(
|
|
|
|
left_column_index,
|
|
|
|
left_row,
|
|
|
|
right_column_index,
|
|
|
|
right_row,
|
|
|
|
)
|
2020-12-21 15:00:39 -08:00
|
|
|
}
|
2021-01-22 10:36:42 -08:00
|
|
|
|
|
|
|
fn push_namespace<NR, N>(&mut self, _: N)
|
|
|
|
where
|
|
|
|
NR: Into<String>,
|
|
|
|
N: FnOnce() -> NR,
|
|
|
|
{
|
|
|
|
// TODO: Do something with namespaces :)
|
|
|
|
}
|
|
|
|
|
|
|
|
fn pop_namespace(&mut self, _: Option<String>) {
|
|
|
|
// TODO: Do something with namespaces :)
|
|
|
|
}
|
2020-12-21 15:00:39 -08:00
|
|
|
}
|
|
|
|
|
|
|
|
impl<F: FieldExt> MockProver<F> {
|
2020-12-23 11:32:39 -08:00
|
|
|
/// Runs a synthetic keygen-and-prove operation on the given circuit, collecting data
|
|
|
|
/// about the constraints and their assignments.
|
2020-12-21 15:00:39 -08:00
|
|
|
pub fn run<ConcreteCircuit: Circuit<F>>(
|
|
|
|
k: u32,
|
|
|
|
circuit: &ConcreteCircuit,
|
2021-02-14 09:30:36 -08:00
|
|
|
instance: Vec<Vec<F>>,
|
2020-12-21 15:00:39 -08:00
|
|
|
) -> Result<Self, Error> {
|
2020-12-21 21:56:30 -08:00
|
|
|
let n = 1 << k;
|
|
|
|
|
2020-12-21 15:00:39 -08:00
|
|
|
let mut cs = ConstraintSystem::default();
|
|
|
|
let config = ConcreteCircuit::configure(&mut cs);
|
|
|
|
|
2021-05-27 06:03:12 -07:00
|
|
|
let fixed = vec![vec![None; n as usize]; cs.num_fixed_columns];
|
|
|
|
let advice = vec![vec![None; n as usize]; cs.num_advice_columns];
|
2020-12-21 21:56:30 -08:00
|
|
|
let permutations = cs
|
|
|
|
.permutations
|
|
|
|
.iter()
|
|
|
|
.map(|p| permutation::keygen::Assembly::new(n as usize, p))
|
|
|
|
.collect();
|
2020-12-21 15:00:39 -08:00
|
|
|
|
|
|
|
let mut prover = MockProver {
|
2020-12-21 21:56:30 -08:00
|
|
|
n,
|
2020-12-21 15:00:39 -08:00
|
|
|
cs,
|
2021-06-18 08:48:25 -07:00
|
|
|
regions: vec![],
|
|
|
|
current_region: None,
|
2020-12-21 15:00:39 -08:00
|
|
|
fixed,
|
|
|
|
advice,
|
2021-02-14 09:30:36 -08:00
|
|
|
instance,
|
2020-12-21 21:56:30 -08:00
|
|
|
permutations,
|
2020-12-21 15:00:39 -08:00
|
|
|
};
|
|
|
|
|
2021-06-21 11:10:59 -07:00
|
|
|
ConcreteCircuit::FloorPlanner::synthesize(&mut prover, circuit, config)?;
|
2020-12-21 15:00:39 -08:00
|
|
|
|
|
|
|
Ok(prover)
|
|
|
|
}
|
|
|
|
|
2021-05-18 08:32:15 -07:00
|
|
|
/// Returns `Ok(())` if this `MockProver` is satisfied, or a list of errors indicating
|
|
|
|
/// the reasons that the circuit is not satisfied.
|
|
|
|
pub fn verify(&self) -> Result<(), Vec<VerifyFailure>> {
|
2020-12-21 15:00:39 -08:00
|
|
|
let n = self.n as i32;
|
|
|
|
|
2021-06-18 08:48:25 -07:00
|
|
|
// 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
|
2021-05-27 06:03:12 -07:00
|
|
|
.iter()
|
|
|
|
// Assume that if a queried selector is enabled, the user wants to use the
|
|
|
|
// corresponding gate in some way.
|
|
|
|
//
|
|
|
|
// TODO: This will trip up on the reverse case, where leaving a selector
|
|
|
|
// 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.
|
2021-06-18 08:48:25 -07:00
|
|
|
.enumerate()
|
2021-06-21 10:19:15 -07:00
|
|
|
.filter(move |(_, g)| g.queried_selectors().contains(selector))
|
2021-06-18 08:48:25 -07:00
|
|
|
.flat_map(move |(gate_index, gate)| {
|
2021-05-27 06:03:12 -07:00
|
|
|
at.iter().flat_map(move |selector_row| {
|
2021-06-04 08:18:51 -07:00
|
|
|
// Selectors are queried with no rotation.
|
|
|
|
let gate_row = *selector_row as i32;
|
2021-05-27 06:03:12 -07:00
|
|
|
|
|
|
|
gate.queried_cells().iter().filter_map(move |cell| {
|
|
|
|
// 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!
|
2021-06-18 08:48:25 -07:00
|
|
|
if r.cells.contains(&(cell.column, cell_row)) {
|
2021-05-27 06:03:12 -07:00
|
|
|
None
|
|
|
|
} else {
|
|
|
|
Some(VerifyFailure::Cell {
|
2021-06-23 05:14:49 -07:00
|
|
|
gate: (gate_index, gate.name()).into(),
|
|
|
|
region: (r_i, r.name.clone()).into(),
|
2021-05-27 06:03:12 -07:00
|
|
|
column: cell.column,
|
2021-06-18 09:25:02 -07:00
|
|
|
offset: cell_row as isize - r.start.unwrap() as isize,
|
2021-05-27 06:03:12 -07:00
|
|
|
})
|
|
|
|
}
|
|
|
|
})
|
|
|
|
})
|
|
|
|
})
|
2021-06-18 08:48:25 -07:00
|
|
|
})
|
|
|
|
});
|
2021-05-27 06:03:12 -07:00
|
|
|
|
2020-12-21 15:00:39 -08:00
|
|
|
// Check that all gates are satisfied for all rows.
|
2021-06-03 19:01:09 -07:00
|
|
|
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<T>, Rotation)],
|
|
|
|
cells: &'a [Vec<Option<F>>],
|
|
|
|
) -> 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])
|
|
|
|
}
|
2021-05-18 08:32:15 -07:00
|
|
|
}
|
2021-06-03 19:01:09 -07:00
|
|
|
|
|
|
|
fn load<'a, F: FieldExt, T: ColumnType>(
|
|
|
|
n: i32,
|
|
|
|
row: i32,
|
|
|
|
queries: &'a [(Column<T>, Rotation)],
|
|
|
|
cells: &'a [Vec<F>],
|
|
|
|
) -> 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]
|
|
|
|
}
|
2021-05-27 06:44:02 -07:00
|
|
|
}
|
2021-06-03 19:01:09 -07:00
|
|
|
|
|
|
|
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 {
|
2021-06-23 05:14:49 -07:00
|
|
|
constraint: (
|
|
|
|
(gate_index, gate.name()).into(),
|
|
|
|
poly_index,
|
|
|
|
gate.constraint_name(poly_index),
|
|
|
|
)
|
|
|
|
.into(),
|
2021-06-03 19:01:09 -07:00
|
|
|
row: (row - n) as usize,
|
|
|
|
})
|
|
|
|
}
|
|
|
|
},
|
|
|
|
)
|
2021-05-27 06:44:02 -07:00
|
|
|
})
|
2021-06-03 19:01:09 -07:00
|
|
|
});
|
2020-12-21 15:00:39 -08:00
|
|
|
|
|
|
|
// Check that all lookups exist in their respective tables.
|
2021-05-18 08:32:15 -07:00
|
|
|
let lookup_errors =
|
|
|
|
self.cs
|
|
|
|
.lookups
|
|
|
|
.iter()
|
|
|
|
.enumerate()
|
|
|
|
.flat_map(|(lookup_index, lookup)| {
|
|
|
|
(0..n).filter_map(move |input_row| {
|
|
|
|
let load = |expression: &Expression<F>, row| {
|
|
|
|
expression.evaluate(
|
|
|
|
&|scalar| scalar,
|
|
|
|
&|index| {
|
|
|
|
let query = self.cs.fixed_queries[index];
|
|
|
|
let column_index = query.0.index();
|
|
|
|
let rotation = query.1 .0;
|
2021-05-27 06:03:12 -07:00
|
|
|
cell_value(
|
|
|
|
self.fixed[column_index]
|
|
|
|
[(row as i32 + n + rotation) as usize % n as usize],
|
|
|
|
)
|
2021-05-18 08:32:15 -07:00
|
|
|
},
|
|
|
|
&|index| {
|
|
|
|
let query = self.cs.advice_queries[index];
|
|
|
|
let column_index = query.0.index();
|
|
|
|
let rotation = query.1 .0;
|
2021-05-27 06:03:12 -07:00
|
|
|
cell_value(
|
|
|
|
self.advice[column_index]
|
|
|
|
[(row as i32 + n + rotation) as usize % n as usize],
|
|
|
|
)
|
2021-05-18 08:32:15 -07:00
|
|
|
},
|
|
|
|
&|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]
|
|
|
|
},
|
|
|
|
&|a, b| a + b,
|
|
|
|
&|a, b| a * b,
|
|
|
|
&|a, scalar| a * scalar,
|
|
|
|
)
|
|
|
|
};
|
|
|
|
|
|
|
|
let inputs: Vec<_> = lookup
|
|
|
|
.input_expressions
|
2021-02-11 18:24:55 -08:00
|
|
|
.iter()
|
2021-05-18 08:32:15 -07:00
|
|
|
.map(|c| load(c, input_row))
|
|
|
|
.collect();
|
|
|
|
let lookup_passes = (0..n)
|
|
|
|
.map(|table_row| {
|
|
|
|
lookup
|
|
|
|
.table_expressions
|
|
|
|
.iter()
|
|
|
|
.map(move |c| load(c, table_row))
|
|
|
|
})
|
|
|
|
.any(|table_row| table_row.eq(inputs.iter().cloned()));
|
|
|
|
if lookup_passes {
|
|
|
|
None
|
|
|
|
} else {
|
|
|
|
Some(VerifyFailure::Lookup {
|
|
|
|
lookup_index,
|
|
|
|
row: input_row as usize,
|
|
|
|
})
|
|
|
|
}
|
2021-02-11 18:24:55 -08:00
|
|
|
})
|
2021-05-18 08:32:15 -07:00
|
|
|
});
|
2020-12-21 15:00:39 -08:00
|
|
|
|
2020-12-21 21:56:30 -08:00
|
|
|
// Check that permutations preserve the original values of the cells.
|
2021-05-18 08:32:15 -07:00
|
|
|
let perm_errors =
|
|
|
|
self.permutations
|
2020-12-21 21:56:30 -08:00
|
|
|
.iter()
|
2021-05-18 08:32:15 -07:00
|
|
|
.enumerate()
|
|
|
|
.flat_map(|(perm_index, assembly)| {
|
|
|
|
// Original values of columns involved in the permutation
|
|
|
|
let original = |perm_index: usize, column, row| {
|
|
|
|
self.cs.permutations[perm_index]
|
|
|
|
.get_columns()
|
2021-05-27 06:03:12 -07:00
|
|
|
.get(column)
|
|
|
|
.map(|c: &Column<Any>| 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],
|
2021-05-18 08:32:15 -07:00
|
|
|
})
|
2021-05-27 06:03:12 -07:00
|
|
|
.unwrap()
|
2021-05-18 08:32:15 -07:00
|
|
|
};
|
|
|
|
|
|
|
|
// Iterate over each column of the permutation
|
|
|
|
assembly
|
|
|
|
.mapping
|
|
|
|
.iter()
|
|
|
|
.enumerate()
|
|
|
|
.flat_map(move |(column, values)| {
|
|
|
|
// Iterate over each row of the column to check that the cell's
|
|
|
|
// value is preserved by the mapping.
|
|
|
|
values.iter().enumerate().filter_map(move |(row, cell)| {
|
|
|
|
let original_cell = original(perm_index, column, row);
|
|
|
|
let permuted_cell = original(perm_index, cell.0, cell.1);
|
|
|
|
if original_cell == permuted_cell {
|
|
|
|
None
|
|
|
|
} else {
|
|
|
|
Some(VerifyFailure::Permutation {
|
|
|
|
perm_index,
|
|
|
|
column,
|
|
|
|
row,
|
|
|
|
})
|
|
|
|
}
|
|
|
|
})
|
|
|
|
})
|
|
|
|
});
|
|
|
|
|
2021-05-27 06:03:12 -07:00
|
|
|
let errors: Vec<_> = iter::empty()
|
|
|
|
.chain(selector_errors)
|
|
|
|
.chain(gate_errors)
|
2021-05-18 08:32:15 -07:00
|
|
|
.chain(lookup_errors)
|
|
|
|
.chain(perm_errors)
|
|
|
|
.collect();
|
|
|
|
if errors.is_empty() {
|
|
|
|
Ok(())
|
|
|
|
} else {
|
|
|
|
Err(errors)
|
2020-12-21 21:56:30 -08:00
|
|
|
}
|
2020-12-21 15:00:39 -08:00
|
|
|
}
|
|
|
|
}
|
2021-05-27 06:02:13 -07:00
|
|
|
|
|
|
|
#[cfg(test)]
|
|
|
|
mod tests {
|
|
|
|
use pasta_curves::Fp;
|
|
|
|
|
|
|
|
use super::{MockProver, VerifyFailure};
|
|
|
|
use crate::{
|
2021-06-21 11:10:59 -07:00
|
|
|
circuit::{Layouter, SimpleFloorPlanner},
|
|
|
|
plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector},
|
2021-05-27 06:02:13 -07:00
|
|
|
poly::Rotation,
|
|
|
|
};
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
fn unassigned_cell() {
|
|
|
|
const K: u32 = 4;
|
|
|
|
|
|
|
|
#[derive(Clone)]
|
|
|
|
struct FaultyCircuitConfig {
|
|
|
|
a: Column<Advice>,
|
|
|
|
q: Selector,
|
|
|
|
}
|
|
|
|
|
|
|
|
struct FaultyCircuit {}
|
|
|
|
|
|
|
|
impl Circuit<Fp> for FaultyCircuit {
|
|
|
|
type Config = FaultyCircuitConfig;
|
2021-06-21 11:10:59 -07:00
|
|
|
type FloorPlanner = SimpleFloorPlanner;
|
2021-05-27 06:02:13 -07:00
|
|
|
|
|
|
|
fn configure(meta: &mut ConstraintSystem<Fp>) -> Self::Config {
|
|
|
|
let a = meta.advice_column();
|
|
|
|
let b = meta.advice_column();
|
|
|
|
let q = meta.selector();
|
|
|
|
|
|
|
|
meta.create_gate("Equality check", |cells| {
|
|
|
|
let a = cells.query_advice(a, Rotation::prev());
|
|
|
|
let b = cells.query_advice(b, Rotation::cur());
|
2021-06-04 08:18:51 -07:00
|
|
|
let q = cells.query_selector(q);
|
2021-05-27 06:02:13 -07:00
|
|
|
|
|
|
|
// If q is enabled, a and b must be assigned to.
|
|
|
|
vec![q * (a - b)]
|
|
|
|
});
|
|
|
|
|
|
|
|
FaultyCircuitConfig { a, q }
|
|
|
|
}
|
|
|
|
|
2021-06-21 11:10:59 -07:00
|
|
|
fn without_witnesses(&self) -> Self {
|
|
|
|
Self {}
|
|
|
|
}
|
|
|
|
|
2021-05-27 06:02:13 -07:00
|
|
|
fn synthesize(
|
|
|
|
&self,
|
|
|
|
config: Self::Config,
|
2021-06-21 11:10:59 -07:00
|
|
|
mut layouter: impl Layouter<Fp>,
|
2021-05-27 06:02:13 -07:00
|
|
|
) -> Result<(), Error> {
|
|
|
|
layouter.assign_region(
|
|
|
|
|| "Faulty synthesis",
|
|
|
|
|mut region| {
|
|
|
|
// Enable the equality gate.
|
2021-06-18 09:25:02 -07:00
|
|
|
config.q.enable(&mut region, 1)?;
|
2021-05-27 06:02:13 -07:00
|
|
|
|
|
|
|
// Assign a = 0.
|
2021-06-18 09:25:02 -07:00
|
|
|
region.assign_advice(|| "a", config.a, 0, || Ok(Fp::zero()))?;
|
2021-05-27 06:02:13 -07:00
|
|
|
|
|
|
|
// BUG: Forget to assign b = 0! This could go unnoticed during
|
|
|
|
// development, because cell values default to zero, which in this
|
|
|
|
// case is fine, but for other assignments would be broken.
|
|
|
|
Ok(())
|
|
|
|
},
|
|
|
|
)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap();
|
|
|
|
assert_eq!(
|
|
|
|
prover.verify(),
|
|
|
|
Err(vec![VerifyFailure::Cell {
|
2021-06-23 05:14:49 -07:00
|
|
|
gate: (0, "Equality check").into(),
|
|
|
|
region: (0, "Faulty synthesis".to_owned()).into(),
|
2021-05-27 06:02:13 -07:00
|
|
|
column: Column::new(1, Any::Advice),
|
2021-06-18 09:25:02 -07:00
|
|
|
offset: 1,
|
2021-05-27 06:02:13 -07:00
|
|
|
}])
|
|
|
|
);
|
|
|
|
}
|
|
|
|
}
|