Add MockProver::assert_satisfied with pretty-printed failures
#480
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
str4d
force-pushed
the
477-mockprover-pretty-failures
branch
from
b3f2c7f
to
cbcaf58
Compare
Codecov Report
@@ Coverage Diff @@
## main #480 +/- ##
==========================================
- Coverage 67.96% 65.85% -2.12%
==========================================
Files 47 49 +2
Lines 5891 6088 +197
==========================================
+ Hits 4004 4009 +5
- Misses 1887 2079 +192
Continue to review full report at Codecov.
|
str4d
force-pushed
the
477-mockprover-pretty-failures
branch
6 times, most recently
from
9fadbd1
to
2fe6f57
Compare
This is equivalent to `assert_eq!(mock_prover.verify(), Ok(()))`, but pretty-prints the verification failures instead of debug-printing them. In its initial state, it just prints the `Display` impl.
An example failure, shown via `assert_eq!(err, Ok(()))`:
```
left: `Err([ConstraintNotSatisfied { constraint: Constraint { gate: Gate { index: 0, name: "R1CS constraint" }, index: 0, name: "buggy R1CS" }, location: InRegion { region: Region { index: 0, name: "Example region" }, offset: 1 }, cell_values: [(VirtualCell { name: "", column: Column { column_type: Advice, index: 0 }, rotation: 0 }, "0x2"), (VirtualCell { name: "", column: Column { column_type: Advice, index: 1 }, rotation: -1 }, "0x4"), (VirtualCell { name: "", column: Column { column_type: Advice, index: 2 }, rotation: 1 }, "0x8")] }])`,
right: `Ok(())`',
```
Via `impl Display for VerifyFailure`:
```
Constraint 0 ('buggy R1CS') in gate 0 ('R1CS constraint') is not satisfied in Region 0 ('Example region') at offset 1
- Column('Advice', 0)@0 = 0x2
- Column('Advice', 1)@-1 = 0x4
- Column('Advice', 2)@1 = 0x8
```
Via `VerifyFailure::emit`:
```
error: constraint not satisfied
Cell layout in region 'Example region':
| Offset | A0 | A1 | A2 |
+--------+----+----+----+
| 0 | | x1 | |
| 1 | x0 | | | <--{ Gate 'R1CS constraint' applied here
| 2 | | | x2 |
Constraint 'buggy R1CS':
S0 * (x0 * x1 + x2) = 0
Assigned cell values:
x0 = 0x2
x1 = 0x4
x2 = 0x8
```
The `dev::tests::bad_lookup` test case, shown via `assert_eq!(err, Ok(()))`:
```
left: `Err([Lookup { lookup_index: 0, location: InRegion { region: Region { index: 2, name: "Faulty synthesis" }, offset: 1 } }])`,
right: `Ok(())`',
```
Via `impl Display for VerifyFailure`:
```
Lookup 0 is not satisfied in Region 2 ('Faulty synthesis') at offset 1
```
Via `VerifyFailure::emit`:
```
error: lookup input does not exist in table
(L0) ∉ (F0)
Lookup inputs:
L0 = x1 * x0 + (1 - x1) * 0x2
^
| Cell layout in region 'Faulty synthesis':
| | Offset | A0 | F1 |
| +--------+----+----+
| | 1 | x0 | x1 | <--{ Lookup inputs queried here
|
| Assigned cell values:
| x0 = 0x5
| x1 = 1
```
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.
```
str4d
force-pushed
the
477-mockprover-pretty-failures
branch
from
2fe6f57
to
57596ca
Compare
|
Rebased to fix merge conflicts in the changelog. |
|
Idea: we could add pretty-printing as a feature of MockProver, not just in case of failures. |
daira
reviewed
Apr 19, 2022
daira
reviewed
Apr 19, 2022
daira
reviewed
Apr 19, 2022
| if a.contains(' ') { | ||
| format!("-({})", a) | ||
| } else { | ||
| format!("-{}", a) |
There was a problem hiding this comment.
This doesn't contain space, so technically you could end up with --x instead of -(-x). It probably doesn't matter; I can't see a case where the result would be ambiguous.
Co-authored-by: Daira Hopwood <daira@jacaranda.org>
|
re-utACK 69c138c |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is equivalent to
assert_eq!(mock_prover.verify(), Ok(())), but pretty-prints the verification failures instead of debug-printing them.This PR has special handling for the following failure cases:
VerifyFailure::CellNotAssignedVerifyFailure::ConstraintNotSatisfiedVerifyFailure::LookupAll other failure cases print the
Displayimpl.Closes #477.