2022-02-01 17:36:36 -08:00
|
|
|
use std::collections::BTreeMap;
|
|
|
|
use std::iter;
|
|
|
|
|
2022-02-01 18:50:11 -08:00
|
|
|
use group::ff::Field;
|
|
|
|
|
2022-02-01 17:36:36 -08:00
|
|
|
use super::FailureLocation;
|
2022-02-01 18:50:11 -08:00
|
|
|
use crate::{
|
|
|
|
dev::{metadata, util},
|
|
|
|
plonk::{Any, Expression},
|
|
|
|
};
|
2022-02-01 17:36:36 -08:00
|
|
|
|
|
|
|
fn padded(p: char, width: usize, text: &str) -> String {
|
|
|
|
let pad = width - text.len();
|
|
|
|
format!(
|
|
|
|
"{}{}{}",
|
|
|
|
iter::repeat(p).take(pad - pad / 2).collect::<String>(),
|
|
|
|
text,
|
|
|
|
iter::repeat(p).take(pad / 2).collect::<String>(),
|
|
|
|
)
|
|
|
|
}
|
|
|
|
|
|
|
|
/// Renders a cell layout around a given failure location.
|
|
|
|
///
|
|
|
|
/// `highlight_row` is called at the end of each row, with the offset of the active row
|
|
|
|
/// (if `location` is in a region), and the rotation of the current row relative to the
|
|
|
|
/// active row.
|
|
|
|
pub(super) fn render_cell_layout(
|
2022-02-01 19:00:00 -08:00
|
|
|
prefix: &str,
|
2022-02-01 17:36:36 -08:00
|
|
|
location: &FailureLocation,
|
|
|
|
columns: &BTreeMap<metadata::Column, usize>,
|
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.
```
2022-02-02 05:02:45 -08:00
|
|
|
layout: &BTreeMap<i32, BTreeMap<metadata::Column, String>>,
|
2022-02-01 17:36:36 -08:00
|
|
|
highlight_row: impl Fn(Option<i32>, i32),
|
|
|
|
) {
|
|
|
|
let col_width = |cells: usize| cells.to_string().len() + 3;
|
|
|
|
|
|
|
|
// If we are in a region, show rows at offsets relative to it. Otherwise, just show
|
|
|
|
// the rotations directly.
|
|
|
|
let offset = match location {
|
|
|
|
FailureLocation::InRegion { region, offset } => {
|
2022-02-01 19:00:00 -08:00
|
|
|
eprintln!("{}Cell layout in region '{}':", prefix, region.name);
|
|
|
|
eprint!("{} | Offset |", prefix);
|
2022-02-01 17:36:36 -08:00
|
|
|
Some(*offset as i32)
|
|
|
|
}
|
|
|
|
FailureLocation::OutsideRegion { row } => {
|
2022-02-01 19:00:00 -08:00
|
|
|
eprintln!("{}Cell layout at row {}:", prefix, row);
|
|
|
|
eprint!("{} |Rotation|", prefix);
|
2022-02-01 17:36:36 -08:00
|
|
|
None
|
|
|
|
}
|
|
|
|
};
|
|
|
|
|
|
|
|
// Print the assigned cells, and their region offset or rotation.
|
|
|
|
for (column, cells) in columns {
|
|
|
|
let width = col_width(*cells);
|
|
|
|
eprint!(
|
|
|
|
"{}|",
|
|
|
|
padded(
|
|
|
|
' ',
|
|
|
|
width,
|
|
|
|
&format!(
|
|
|
|
"{}{}",
|
|
|
|
match column.column_type {
|
|
|
|
Any::Advice => "A",
|
|
|
|
Any::Fixed => "F",
|
|
|
|
Any::Instance => "I",
|
|
|
|
},
|
|
|
|
column.index,
|
|
|
|
)
|
|
|
|
)
|
|
|
|
);
|
|
|
|
}
|
|
|
|
eprintln!();
|
2022-02-01 19:00:00 -08:00
|
|
|
eprint!("{} +--------+", prefix);
|
2022-02-01 17:36:36 -08:00
|
|
|
for cells in columns.values() {
|
|
|
|
eprint!("{}+", padded('-', col_width(*cells), ""));
|
|
|
|
}
|
|
|
|
eprintln!();
|
|
|
|
for (rotation, row) in layout {
|
|
|
|
eprint!(
|
2022-02-01 19:00:00 -08:00
|
|
|
"{} |{}|",
|
|
|
|
prefix,
|
2022-02-01 17:36:36 -08:00
|
|
|
padded(' ', 8, &(offset.unwrap_or(0) + rotation).to_string())
|
|
|
|
);
|
|
|
|
for (col, cells) in columns {
|
|
|
|
let width = col_width(*cells);
|
|
|
|
eprint!(
|
|
|
|
"{}|",
|
|
|
|
padded(
|
|
|
|
' ',
|
|
|
|
width,
|
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.
```
2022-02-02 05:02:45 -08:00
|
|
|
row.get(col).map(|s| s.as_str()).unwrap_or_default()
|
2022-02-01 17:36:36 -08:00
|
|
|
)
|
|
|
|
);
|
|
|
|
}
|
|
|
|
highlight_row(offset, *rotation);
|
|
|
|
eprintln!();
|
|
|
|
}
|
|
|
|
}
|
2022-02-01 18:50:11 -08:00
|
|
|
|
|
|
|
pub(super) fn expression_to_string<F: Field>(
|
|
|
|
expr: &Expression<F>,
|
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.
```
2022-02-02 05:02:45 -08:00
|
|
|
layout: &BTreeMap<i32, BTreeMap<metadata::Column, String>>,
|
2022-02-01 18:50:11 -08:00
|
|
|
) -> String {
|
|
|
|
expr.evaluate(
|
|
|
|
&util::format_value,
|
|
|
|
&|_| panic!("virtual selectors are removed during optimization"),
|
|
|
|
&|query, column, rotation| {
|
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.
```
2022-02-02 05:02:45 -08:00
|
|
|
if let Some(label) = layout
|
2022-02-01 18:50:11 -08:00
|
|
|
.get(&rotation.0)
|
|
|
|
.and_then(|row| row.get(&(Any::Fixed, column).into()))
|
|
|
|
{
|
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.
```
2022-02-02 05:02:45 -08:00
|
|
|
label.clone()
|
2022-02-01 18:50:11 -08:00
|
|
|
} else if rotation.0 == 0 {
|
|
|
|
// This is most likely a merged selector
|
|
|
|
format!("S{}", query)
|
|
|
|
} else {
|
|
|
|
// No idea how we'd get here...
|
|
|
|
format!("F{}@{}", column, rotation.0)
|
|
|
|
}
|
|
|
|
},
|
|
|
|
&|_, column, rotation| {
|
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.
```
2022-02-02 05:02:45 -08:00
|
|
|
layout
|
|
|
|
.get(&rotation.0)
|
|
|
|
.unwrap()
|
|
|
|
.get(&(Any::Advice, column).into())
|
|
|
|
.unwrap()
|
|
|
|
.clone()
|
2022-02-01 18:50:11 -08:00
|
|
|
},
|
|
|
|
&|_, column, rotation| {
|
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.
```
2022-02-02 05:02:45 -08:00
|
|
|
layout
|
|
|
|
.get(&rotation.0)
|
|
|
|
.unwrap()
|
|
|
|
.get(&(Any::Instance, column).into())
|
|
|
|
.unwrap()
|
|
|
|
.clone()
|
2022-02-01 18:50:11 -08:00
|
|
|
},
|
|
|
|
&|a| {
|
|
|
|
if a.contains(' ') {
|
|
|
|
format!("-({})", a)
|
|
|
|
} else {
|
|
|
|
format!("-{}", a)
|
|
|
|
}
|
|
|
|
},
|
|
|
|
&|a, b| {
|
|
|
|
if let Some(b) = b.strip_prefix('-') {
|
|
|
|
format!("{} - {}", a, b)
|
|
|
|
} else {
|
|
|
|
format!("{} + {}", a, b)
|
|
|
|
}
|
|
|
|
},
|
|
|
|
&|a, b| match (a.contains(' '), b.contains(' ')) {
|
|
|
|
(false, false) => format!("{} * {}", a, b),
|
|
|
|
(false, true) => format!("{} * ({})", a, b),
|
|
|
|
(true, false) => format!("({}) * {}", a, b),
|
|
|
|
(true, true) => format!("({}) * ({})", a, b),
|
|
|
|
},
|
|
|
|
&|a, s| {
|
|
|
|
if a.contains(' ') {
|
|
|
|
format!("({}) * {}", a, util::format_value(s))
|
|
|
|
} else {
|
|
|
|
format!("{} * {}", a, util::format_value(s))
|
|
|
|
}
|
|
|
|
},
|
|
|
|
)
|
|
|
|
}
|