mirror of https://github.com/zcash/halo2.git
dev: Enable `VerifyFailure::ConstraintNotSatisfied` to point to region offsets
This commit is contained in:
parent
5520d13480
commit
558e03aa93
|
@ -25,9 +25,9 @@ and this project adheres to Rust's notion of
|
||||||
- `halo2::dev::VerifyFailure` has been overhauled:
|
- `halo2::dev::VerifyFailure` has been overhauled:
|
||||||
- `VerifyFailure::ConstraintNotSatisfied` now has a `cell_values` field,
|
- `VerifyFailure::ConstraintNotSatisfied` now has a `cell_values` field,
|
||||||
storing the values of the cells used in the unsatisfied constraint.
|
storing the values of the cells used in the unsatisfied constraint.
|
||||||
- The `row` field of `VerifyFailure::Lookup` has been replaced by a `location`
|
- The `row` fields of `VerifyFailure::{ConstraintNotSatisfied, Lookup}` have
|
||||||
field, which can now indicate whether the location falls within an assigned
|
been replaced by `location` fields, which can now indicate whether the
|
||||||
region.
|
location falls within an assigned region.
|
||||||
- `halo2::plonk::ConstraintSystem::enable_equality` and
|
- `halo2::plonk::ConstraintSystem::enable_equality` and
|
||||||
`halo2::plonk::ConstraintSystem::query_any` now take `Into<Column<Any>>` instead
|
`halo2::plonk::ConstraintSystem::query_any` now take `Into<Column<Any>>` instead
|
||||||
of `Column<Any>` as a parameter to avoid excesive `.into()` usage.
|
of `Column<Any>` as a parameter to avoid excesive `.into()` usage.
|
||||||
|
|
27
src/dev.rs
27
src/dev.rs
|
@ -139,8 +139,11 @@ pub enum VerifyFailure {
|
||||||
ConstraintNotSatisfied {
|
ConstraintNotSatisfied {
|
||||||
/// The polynomial constraint that is not satisfied.
|
/// The polynomial constraint that is not satisfied.
|
||||||
constraint: metadata::Constraint,
|
constraint: metadata::Constraint,
|
||||||
/// The row on which this constraint is not satisfied.
|
/// The location at which this constraint is not satisfied.
|
||||||
row: usize,
|
///
|
||||||
|
/// `FailureLocation::OutsideRegion` is usually caused by a constraint that does
|
||||||
|
/// not contain a selector, and as a result is active on every row.
|
||||||
|
location: FailureLocation,
|
||||||
/// The values of the virtual cells used by this constraint.
|
/// The values of the virtual cells used by this constraint.
|
||||||
cell_values: Vec<(metadata::VirtualCell, String)>,
|
cell_values: Vec<(metadata::VirtualCell, String)>,
|
||||||
},
|
},
|
||||||
|
@ -195,10 +198,10 @@ impl fmt::Display for VerifyFailure {
|
||||||
}
|
}
|
||||||
Self::ConstraintNotSatisfied {
|
Self::ConstraintNotSatisfied {
|
||||||
constraint,
|
constraint,
|
||||||
row,
|
location,
|
||||||
cell_values,
|
cell_values,
|
||||||
} => {
|
} => {
|
||||||
writeln!(f, "{} is not satisfied on row {}", constraint, row)?;
|
writeln!(f, "{} is not satisfied {}", constraint, location)?;
|
||||||
for (name, value) in cell_values {
|
for (name, value) in cell_values {
|
||||||
writeln!(f, "- {} = {}", name, value)?;
|
writeln!(f, "- {} = {}", name, value)?;
|
||||||
}
|
}
|
||||||
|
@ -357,7 +360,7 @@ impl<F: Group + Field> Mul<F> for Value<F> {
|
||||||
/// use halo2::{
|
/// use halo2::{
|
||||||
/// arithmetic::FieldExt,
|
/// arithmetic::FieldExt,
|
||||||
/// circuit::{Layouter, SimpleFloorPlanner},
|
/// circuit::{Layouter, SimpleFloorPlanner},
|
||||||
/// dev::{MockProver, VerifyFailure},
|
/// dev::{FailureLocation, MockProver, VerifyFailure},
|
||||||
/// pasta::Fp,
|
/// pasta::Fp,
|
||||||
/// plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector},
|
/// plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector},
|
||||||
/// poly::Rotation,
|
/// poly::Rotation,
|
||||||
|
@ -438,7 +441,10 @@ impl<F: Group + Field> Mul<F> for Value<F> {
|
||||||
/// prover.verify(),
|
/// prover.verify(),
|
||||||
/// Err(vec![VerifyFailure::ConstraintNotSatisfied {
|
/// Err(vec![VerifyFailure::ConstraintNotSatisfied {
|
||||||
/// constraint: ((0, "R1CS constraint").into(), 0, "buggy R1CS").into(),
|
/// constraint: ((0, "R1CS constraint").into(), 0, "buggy R1CS").into(),
|
||||||
/// row: 0,
|
/// location: FailureLocation::InRegion {
|
||||||
|
/// region: (0, "Example region").into(),
|
||||||
|
/// offset: 0,
|
||||||
|
/// },
|
||||||
/// cell_values: vec![
|
/// cell_values: vec![
|
||||||
/// (((Any::Advice, 0).into(), 0).into(), "0x2".to_string()),
|
/// (((Any::Advice, 0).into(), 0).into(), "0x2".to_string()),
|
||||||
/// (((Any::Advice, 1).into(), 0).into(), "0x4".to_string()),
|
/// (((Any::Advice, 1).into(), 0).into(), "0x4".to_string()),
|
||||||
|
@ -829,7 +835,12 @@ impl<F: FieldExt> MockProver<F> {
|
||||||
gate.constraint_name(poly_index),
|
gate.constraint_name(poly_index),
|
||||||
)
|
)
|
||||||
.into(),
|
.into(),
|
||||||
row: (row - n) as usize,
|
location: FailureLocation::find_expressions(
|
||||||
|
&self.cs,
|
||||||
|
&self.regions,
|
||||||
|
(row - n) as usize,
|
||||||
|
Some(poly).into_iter(),
|
||||||
|
),
|
||||||
cell_values: util::cell_values(
|
cell_values: util::cell_values(
|
||||||
gate,
|
gate,
|
||||||
poly,
|
poly,
|
||||||
|
@ -1181,7 +1192,7 @@ mod tests {
|
||||||
Err(vec![VerifyFailure::Lookup {
|
Err(vec![VerifyFailure::Lookup {
|
||||||
lookup_index: 0,
|
lookup_index: 0,
|
||||||
location: FailureLocation::InRegion {
|
location: FailureLocation::InRegion {
|
||||||
region: (2, "Faulty synthesis".to_owned()).into(),
|
region: (2, "Faulty synthesis").into(),
|
||||||
offset: 1,
|
offset: 1,
|
||||||
}
|
}
|
||||||
}])
|
}])
|
||||||
|
|
|
@ -164,3 +164,12 @@ impl From<(usize, String)> for Region {
|
||||||
Region { index, name }
|
Region { index, name }
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl From<(usize, &str)> for Region {
|
||||||
|
fn from((index, name): (usize, &str)) -> Self {
|
||||||
|
Region {
|
||||||
|
index,
|
||||||
|
name: name.to_owned(),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
Loading…
Reference in New Issue