mirror of https://github.com/zcash/halo2.git
dev: Add a custom `VerifyFailure::CellNotAssigned` emitter
The `dev::tests::unassigned_cell` test case, shown via `assert_eq!(err, Ok(()))`:
```
left: `Err([CellNotAssigned { gate: Gate { index: 0, name: "Equality check" }, region: Region { index: 0, name: "Faulty synthesis" }, gate_offset: 1, column: Column { index: 1, column_type: Advice }, offset: 1 }])`,
right: `Ok(())`',
```
Via `impl Display for VerifyFailure`:
```
Region 0 ('Faulty synthesis') uses Gate 0 ('Equality check') at offset 1, which requires cell in column Column { index: 1, column_type: Advice } at offset 1 to be assigned.
```
Via `VerifyFailure::emit`:
```
error: cell not assigned
Cell layout in region 'Faulty synthesis':
| Offset | A0 | A1 |
+--------+----+----+
| 0 | x0 | |
| 1 | | X | <--{ X marks the spot! 🦜
Gate 'Equality check' (applied at offset 1) queries these cells.
```
This commit is contained in:
parent
369ff521d3
commit
57596cab36
|
@ -213,6 +213,70 @@ impl fmt::Display for VerifyFailure {
|
|||
}
|
||||
}
|
||||
|
||||
/// Renders `VerifyFailure::CellNotAssigned`.
|
||||
///
|
||||
/// ```text
|
||||
/// error: cell not assigned
|
||||
/// Cell layout in region 'Faulty synthesis':
|
||||
/// | Offset | A0 | A1 |
|
||||
/// +--------+----+----+
|
||||
/// | 0 | x0 | |
|
||||
/// | 1 | | X | <--{ X marks the spot! 🦜
|
||||
///
|
||||
/// Gate 'Equality check' (applied at offset 1) queries these cells.
|
||||
/// ```
|
||||
fn render_cell_not_assigned<F: Field>(
|
||||
gates: &[Gate<F>],
|
||||
gate: &metadata::Gate,
|
||||
region: &metadata::Region,
|
||||
gate_offset: usize,
|
||||
column: Column<Any>,
|
||||
offset: isize,
|
||||
) {
|
||||
// Collect the necessary rendering information:
|
||||
// - The columns involved in this gate.
|
||||
// - How many cells are in each column.
|
||||
// - The grid of cell values, indexed by rotation.
|
||||
let mut columns = BTreeMap::<metadata::Column, usize>::default();
|
||||
let mut layout = BTreeMap::<i32, BTreeMap<metadata::Column, _>>::default();
|
||||
for (i, cell) in gates[gate.index].queried_cells().iter().enumerate() {
|
||||
let cell_column = cell.column.into();
|
||||
*columns.entry(cell_column).or_default() += 1;
|
||||
layout
|
||||
.entry(cell.rotation.0)
|
||||
.or_default()
|
||||
.entry(cell_column)
|
||||
.or_insert_with(|| {
|
||||
if cell.column == column && gate_offset as i32 + cell.rotation.0 == offset as i32 {
|
||||
"X".to_string()
|
||||
} else {
|
||||
format!("x{}", i)
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
eprintln!("error: cell not assigned");
|
||||
emitter::render_cell_layout(
|
||||
" ",
|
||||
&FailureLocation::InRegion {
|
||||
region: region.clone(),
|
||||
offset: gate_offset,
|
||||
},
|
||||
&columns,
|
||||
&layout,
|
||||
|row_offset, rotation| {
|
||||
if (row_offset.unwrap() + rotation) as isize == offset {
|
||||
eprint!(" <--{{ X marks the spot! 🦜");
|
||||
}
|
||||
},
|
||||
);
|
||||
eprintln!();
|
||||
eprintln!(
|
||||
" Gate '{}' (applied at offset {}) queries these cells.",
|
||||
gate.name, gate_offset
|
||||
);
|
||||
}
|
||||
|
||||
/// Renders `VerifyFailure::ConstraintNotSatisfied`.
|
||||
///
|
||||
/// ```text
|
||||
|
@ -241,14 +305,14 @@ fn render_constraint_not_satisfied<F: Field>(
|
|||
// - How many cells are in each column.
|
||||
// - The grid of cell values, indexed by rotation.
|
||||
let mut columns = BTreeMap::<metadata::Column, usize>::default();
|
||||
let mut layout = BTreeMap::<i32, BTreeMap<metadata::Column, usize>>::default();
|
||||
let mut layout = BTreeMap::<i32, BTreeMap<metadata::Column, _>>::default();
|
||||
for (i, (cell, _)) in cell_values.iter().enumerate() {
|
||||
*columns.entry(cell.column).or_default() += 1;
|
||||
layout
|
||||
.entry(cell.rotation)
|
||||
.or_default()
|
||||
.entry(cell.column)
|
||||
.or_insert(i);
|
||||
.or_insert(format!("x{}", i));
|
||||
}
|
||||
|
||||
eprintln!("error: constraint not satisfied");
|
||||
|
@ -393,14 +457,14 @@ fn render_lookup<F: FieldExt>(
|
|||
// - How many cells are in each column.
|
||||
// - The grid of cell values, indexed by rotation.
|
||||
let mut columns = BTreeMap::<metadata::Column, usize>::default();
|
||||
let mut layout = BTreeMap::<i32, BTreeMap<metadata::Column, usize>>::default();
|
||||
let mut layout = BTreeMap::<i32, BTreeMap<metadata::Column, _>>::default();
|
||||
for (i, (cell, _)) in cell_values.iter().enumerate() {
|
||||
*columns.entry(cell.column).or_default() += 1;
|
||||
layout
|
||||
.entry(cell.rotation)
|
||||
.or_default()
|
||||
.entry(cell.column)
|
||||
.or_insert(i);
|
||||
.or_insert(format!("x{}", i));
|
||||
}
|
||||
|
||||
if i != 0 {
|
||||
|
@ -431,6 +495,20 @@ impl VerifyFailure {
|
|||
/// Emits this failure in pretty-printed format to stderr.
|
||||
pub(super) fn emit<F: FieldExt>(&self, prover: &MockProver<F>) {
|
||||
match self {
|
||||
Self::CellNotAssigned {
|
||||
gate,
|
||||
region,
|
||||
gate_offset,
|
||||
column,
|
||||
offset,
|
||||
} => render_cell_not_assigned(
|
||||
&prover.cs.gates,
|
||||
gate,
|
||||
region,
|
||||
*gate_offset,
|
||||
*column,
|
||||
*offset,
|
||||
),
|
||||
Self::ConstraintNotSatisfied {
|
||||
constraint,
|
||||
location,
|
||||
|
|
|
@ -28,7 +28,7 @@ pub(super) fn render_cell_layout(
|
|||
prefix: &str,
|
||||
location: &FailureLocation,
|
||||
columns: &BTreeMap<metadata::Column, usize>,
|
||||
layout: &BTreeMap<i32, BTreeMap<metadata::Column, usize>>,
|
||||
layout: &BTreeMap<i32, BTreeMap<metadata::Column, String>>,
|
||||
highlight_row: impl Fn(Option<i32>, i32),
|
||||
) {
|
||||
let col_width = |cells: usize| cells.to_string().len() + 3;
|
||||
|
@ -87,7 +87,7 @@ pub(super) fn render_cell_layout(
|
|||
padded(
|
||||
' ',
|
||||
width,
|
||||
&row.get(col).map(|i| format!("x{}", i)).unwrap_or_default()
|
||||
row.get(col).map(|s| s.as_str()).unwrap_or_default()
|
||||
)
|
||||
);
|
||||
}
|
||||
|
@ -98,17 +98,17 @@ pub(super) fn render_cell_layout(
|
|||
|
||||
pub(super) fn expression_to_string<F: Field>(
|
||||
expr: &Expression<F>,
|
||||
layout: &BTreeMap<i32, BTreeMap<metadata::Column, usize>>,
|
||||
layout: &BTreeMap<i32, BTreeMap<metadata::Column, String>>,
|
||||
) -> String {
|
||||
expr.evaluate(
|
||||
&util::format_value,
|
||||
&|_| panic!("virtual selectors are removed during optimization"),
|
||||
&|query, column, rotation| {
|
||||
if let Some(i) = layout
|
||||
if let Some(label) = layout
|
||||
.get(&rotation.0)
|
||||
.and_then(|row| row.get(&(Any::Fixed, column).into()))
|
||||
{
|
||||
format!("x{}", i)
|
||||
label.clone()
|
||||
} else if rotation.0 == 0 {
|
||||
// This is most likely a merged selector
|
||||
format!("S{}", query)
|
||||
|
@ -118,24 +118,20 @@ pub(super) fn expression_to_string<F: Field>(
|
|||
}
|
||||
},
|
||||
&|_, column, rotation| {
|
||||
format!(
|
||||
"x{}",
|
||||
layout
|
||||
.get(&rotation.0)
|
||||
.unwrap()
|
||||
.get(&(Any::Advice, column).into())
|
||||
.unwrap()
|
||||
)
|
||||
layout
|
||||
.get(&rotation.0)
|
||||
.unwrap()
|
||||
.get(&(Any::Advice, column).into())
|
||||
.unwrap()
|
||||
.clone()
|
||||
},
|
||||
&|_, column, rotation| {
|
||||
format!(
|
||||
"x{}",
|
||||
layout
|
||||
.get(&rotation.0)
|
||||
.unwrap()
|
||||
.get(&(Any::Instance, column).into())
|
||||
.unwrap()
|
||||
)
|
||||
layout
|
||||
.get(&rotation.0)
|
||||
.unwrap()
|
||||
.get(&(Any::Instance, column).into())
|
||||
.unwrap()
|
||||
.clone()
|
||||
},
|
||||
&|a| {
|
||||
if a.contains(' ') {
|
||||
|
|
|
@ -143,7 +143,7 @@ impl From<(Gate, usize, &'static str)> for Constraint {
|
|||
}
|
||||
|
||||
/// Metadata about an assigned region within a circuit.
|
||||
#[derive(Debug, PartialEq)]
|
||||
#[derive(Clone, Debug, PartialEq)]
|
||||
pub struct Region {
|
||||
/// The index of the region. These indices are assigned in the order in which
|
||||
/// `Layouter::assign_region` is called during `Circuit::synthesize`.
|
||||
|
|
Loading…
Reference in New Issue