mirror of https://github.com/zcash/halo2.git
Merge pull request #286 from zcash/constraint-annotations
Enable annotating individual constraints within gates
This commit is contained in:
commit
879509491f
|
@ -364,6 +364,7 @@ fn main() {
|
||||||
gate_index: 1,
|
gate_index: 1,
|
||||||
gate_name: "public input",
|
gate_name: "public input",
|
||||||
constraint_index: 0,
|
constraint_index: 0,
|
||||||
|
constraint_name: "",
|
||||||
row: 6,
|
row: 6,
|
||||||
}])
|
}])
|
||||||
);
|
);
|
||||||
|
|
|
@ -631,6 +631,7 @@ fn main() {
|
||||||
gate_index: 0,
|
gate_index: 0,
|
||||||
gate_name: "public input",
|
gate_name: "public input",
|
||||||
constraint_index: 0,
|
constraint_index: 0,
|
||||||
|
constraint_name: "",
|
||||||
row: 7,
|
row: 7,
|
||||||
}])
|
}])
|
||||||
);
|
);
|
||||||
|
|
20
src/dev.rs
20
src/dev.rs
|
@ -59,6 +59,9 @@ pub enum VerifyFailure {
|
||||||
/// from the closure passed to `ConstraintSystem::create_gate` during
|
/// from the closure passed to `ConstraintSystem::create_gate` during
|
||||||
/// `Circuit::configure`.
|
/// `Circuit::configure`.
|
||||||
constraint_index: usize,
|
constraint_index: usize,
|
||||||
|
/// The name of the unsatisfied constraint. This is specified by the gate creator
|
||||||
|
/// (such as a chip implementation), and is not enforced to be unique.
|
||||||
|
constraint_name: &'static str,
|
||||||
/// The row on which this constraint is not satisfied.
|
/// The row on which this constraint is not satisfied.
|
||||||
row: usize,
|
row: usize,
|
||||||
},
|
},
|
||||||
|
@ -103,12 +106,21 @@ impl fmt::Display for VerifyFailure {
|
||||||
gate_index,
|
gate_index,
|
||||||
gate_name,
|
gate_name,
|
||||||
constraint_index,
|
constraint_index,
|
||||||
|
constraint_name,
|
||||||
row,
|
row,
|
||||||
} => {
|
} => {
|
||||||
write!(
|
write!(
|
||||||
f,
|
f,
|
||||||
"Constraint {} in gate {} ('{}') is not satisfied on row {}",
|
"Constraint {}{} in gate {} ('{}') is not satisfied on row {}",
|
||||||
constraint_index, gate_index, gate_name, row
|
constraint_index,
|
||||||
|
if constraint_name.is_empty() {
|
||||||
|
String::new()
|
||||||
|
} else {
|
||||||
|
format!(" ('{}')", constraint_name)
|
||||||
|
},
|
||||||
|
gate_index,
|
||||||
|
gate_name,
|
||||||
|
row
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
Self::Lookup { lookup_index, row } => {
|
Self::Lookup { lookup_index, row } => {
|
||||||
|
@ -176,7 +188,7 @@ impl fmt::Display for VerifyFailure {
|
||||||
/// let c = meta.query_advice(c, Rotation::cur());
|
/// let c = meta.query_advice(c, Rotation::cur());
|
||||||
///
|
///
|
||||||
/// // BUG: Should be a * b - c
|
/// // BUG: Should be a * b - c
|
||||||
/// vec![a * b + c]
|
/// Some(("buggy R1CS", a * b + c))
|
||||||
/// });
|
/// });
|
||||||
///
|
///
|
||||||
/// MyConfig { a, b, c }
|
/// MyConfig { a, b, c }
|
||||||
|
@ -213,6 +225,7 @@ impl fmt::Display for VerifyFailure {
|
||||||
/// gate_index: 0,
|
/// gate_index: 0,
|
||||||
/// gate_name: "R1CS constraint",
|
/// gate_name: "R1CS constraint",
|
||||||
/// constraint_index: 0,
|
/// constraint_index: 0,
|
||||||
|
/// constraint_name: "buggy R1CS",
|
||||||
/// row: 0
|
/// row: 0
|
||||||
/// }])
|
/// }])
|
||||||
/// );
|
/// );
|
||||||
|
@ -502,6 +515,7 @@ impl<F: FieldExt> MockProver<F> {
|
||||||
gate_index,
|
gate_index,
|
||||||
gate_name: gate.name(),
|
gate_name: gate.name(),
|
||||||
constraint_index: poly_index,
|
constraint_index: poly_index,
|
||||||
|
constraint_name: gate.constraint_name(poly_index),
|
||||||
row: (row - n) as usize,
|
row: (row - n) as usize,
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
|
@ -486,9 +486,37 @@ impl<Col: Into<Column<Any>>> From<(Col, Rotation)> for VirtualCell {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// An individual polynomial constraint.
|
||||||
|
///
|
||||||
|
/// These are returned by the closures passed to `ConstraintSystem::create_gate`.
|
||||||
|
#[derive(Debug)]
|
||||||
|
pub struct Constraint<F: Field> {
|
||||||
|
name: &'static str,
|
||||||
|
poly: Expression<F>,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<F: Field> From<Expression<F>> for Constraint<F> {
|
||||||
|
fn from(poly: Expression<F>) -> Self {
|
||||||
|
Constraint { name: "", poly }
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<F: Field> From<(&'static str, Expression<F>)> for Constraint<F> {
|
||||||
|
fn from((name, poly): (&'static str, Expression<F>)) -> Self {
|
||||||
|
Constraint { name, poly }
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<F: Field> From<Expression<F>> for Vec<Constraint<F>> {
|
||||||
|
fn from(poly: Expression<F>) -> Self {
|
||||||
|
vec![Constraint { name: "", poly }]
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Clone, Debug)]
|
#[derive(Clone, Debug)]
|
||||||
pub(crate) struct Gate<F: Field> {
|
pub(crate) struct Gate<F: Field> {
|
||||||
name: &'static str,
|
name: &'static str,
|
||||||
|
constraint_names: Vec<&'static str>,
|
||||||
polys: Vec<Expression<F>>,
|
polys: Vec<Expression<F>>,
|
||||||
/// We track queried selectors separately from other cells, so that we can use them to
|
/// We track queried selectors separately from other cells, so that we can use them to
|
||||||
/// trigger debug checks on gates.
|
/// trigger debug checks on gates.
|
||||||
|
@ -501,6 +529,10 @@ impl<F: Field> Gate<F> {
|
||||||
self.name
|
self.name
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub(crate) fn constraint_name(&self, constraint_index: usize) -> &'static str {
|
||||||
|
self.constraint_names[constraint_index]
|
||||||
|
}
|
||||||
|
|
||||||
pub(crate) fn polynomials(&self) -> &[Expression<F>] {
|
pub(crate) fn polynomials(&self) -> &[Expression<F>] {
|
||||||
&self.polys
|
&self.polys
|
||||||
}
|
}
|
||||||
|
@ -726,19 +758,36 @@ impl<F: Field> ConstraintSystem<F> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Create a new gate
|
/// Creates a new gate.
|
||||||
pub fn create_gate(
|
///
|
||||||
|
/// # Panics
|
||||||
|
///
|
||||||
|
/// A gate is required to contain polynomial constraints. This method will panic if
|
||||||
|
/// `constraints` returns an empty iterator.
|
||||||
|
pub fn create_gate<C: Into<Constraint<F>>, Iter: IntoIterator<Item = C>>(
|
||||||
&mut self,
|
&mut self,
|
||||||
name: &'static str,
|
name: &'static str,
|
||||||
f: impl FnOnce(&mut VirtualCells<'_, F>) -> Vec<Expression<F>>,
|
constraints: impl FnOnce(&mut VirtualCells<'_, F>) -> Iter,
|
||||||
) {
|
) {
|
||||||
let mut cells = VirtualCells::new(self);
|
let mut cells = VirtualCells::new(self);
|
||||||
let polys = f(&mut cells);
|
let constraints = constraints(&mut cells);
|
||||||
let queried_selectors = cells.queried_selectors;
|
let queried_selectors = cells.queried_selectors;
|
||||||
let queried_cells = cells.queried_cells;
|
let queried_cells = cells.queried_cells;
|
||||||
|
|
||||||
|
let (constraint_names, polys): (_, Vec<_>) = constraints
|
||||||
|
.into_iter()
|
||||||
|
.map(|c| c.into())
|
||||||
|
.map(|c| (c.name, c.poly))
|
||||||
|
.unzip();
|
||||||
|
|
||||||
|
assert!(
|
||||||
|
!polys.is_empty(),
|
||||||
|
"Gates must contain at least one constraint."
|
||||||
|
);
|
||||||
|
|
||||||
self.gates.push(Gate {
|
self.gates.push(Gate {
|
||||||
name,
|
name,
|
||||||
|
constraint_names,
|
||||||
polys,
|
polys,
|
||||||
queried_selectors,
|
queried_selectors,
|
||||||
queried_cells,
|
queried_cells,
|
||||||
|
|
Loading…
Reference in New Issue