Add support for Column annotations for MockProver debugging

[CPerezz]

This PR particularly includes:

• Ability to annotate columns within a Region.
• Ability to annotate lookup table columns.
• Ability to print for both prover.verify() and prover.assert_verify() the annotations of the Columns that have been declared.
• Ability to print the lookup column queried within a lookup expression that failed.
• Ability to annotate dynamic-lookup columns (Advice Columns used for lookup)

Resolves: #57

Here is a list of all of the prints that you can now get with the annotation support:

Assert_satisfied - Lookup_any

error: lookup input does not exist in table
  (L0, L1) ∉ ("Inst-Table", "Adv-Table")

  Lookup 'lookup' inputs:
    L0 = x1 * x0 + (1 - x1) * 0x2
    ^

    | Cell layout in region 'Faulty synthesis':
    |   | Offset |Witness example| F0 |
    |   +--------+---------------+----+
    |   |    1   |       x0      | x1 | <--{ Lookup 'lookup' inputs queried here
    |
    | Assigned cell values:
    |   x0 = 0x5
    |   x1 = 1

    L1 = x1 * x0 + (1 - x1) * 0x2
    ^

    | Cell layout in region 'Faulty synthesis':
    |   | Offset |Witness example| F0 |
    |   +--------+---------------+----+
    |   |    1   |       x0      | x1 | <--{ Lookup 'lookup' inputs queried here
    |
    | Assigned cell values:
    |   x0 = 0x5
    |   x1 = 1

Assert_satisfied - Lookup_fixed

error: lookup input does not exist in table
  (L0) ∉ ("Table1")

  Lookup 'lookup' inputs:
    L0 = x1 * x0 + (1 - x1) * 0x2
    ^

    | Cell layout in region 'Faulty synthesis':
    |   | Offset |Witness example| F1 |
    |   +--------+---------------+----+
    |   |    1   |       x0      | x1 | <--{ Lookup 'lookup' inputs queried here
    |
    | Assigned cell values:
    |   x0 = 0x5
    |   x1 = 1

Assert_satisfied - ConstraintNotSatisfied

error: constraint not satisfied

  Cell layout in region 'Wrong synthesis':
    | Offset |This is Advice!|This is Advice too!|Another one!|This is a Fixed!|
    +--------+---------------+-------------------+------------+----------------+
    |    0   |       x0      |         x1        |     x2     |       x3       | <--{ Gate 'Equality check' applied here

  Constraint '':
    (S1 * (x0 - x1)) * (x2 - x3) = 0

  Assigned cell values:
    x0 = 1
    x1 = 0
    x2 = 0x5
    x3 = 0x7

Assert_satisfied - CellNotAssigned

error: cell not assigned

  Cell layout in region 'Faulty synthesis':
    | Offset |This is annotated!|This is also annotated!|
    +--------+------------------+-----------------------+
    |    0   |        x0        |                       |
    |    1   |                  |           X           | <--{ X marks the spot! 🦜

  Gate 'Equality check' (applied at offset 1) queries these cells.

Prover.verify - ConstraintNotSatisfied (now includes annotations for VirtualCells)

Err([ConstraintCaseDebug {
    constraint: Constraint {
        gate: Gate {
            index: 0,
            name: "Equality check",
        },
        index: 0,
        name: "",
    },
    location: InRegion {
        region: Region 1 ('Wrong synthesis'),
        offset: 0,
    },
    cell_values: [
        (
            DebugVirtualCell {
                name: "",
                column: DebugColumn {
                    column_type: Advice,
                    index: 0,
                    annotation: "This is Advice!",
                },
                rotation: 0,
            },
            "1",
        ),
        (
            DebugVirtualCell {
                name: "",
                column: DebugColumn {
                    column_type: Advice,
                    index: 1,
                    annotation: "This is Advice too!",
                },
                rotation: 0,
            },
            "0",
        ),
        (
            DebugVirtualCell {
                name: "",
                column: DebugColumn {
                    column_type: Advice,
                    index: 2,
                    annotation: "Another one!",
                },
                rotation: 0,
            },
            "0x5",
        ),
        (
            DebugVirtualCell {
                name: "",
                column: DebugColumn {
                    column_type: Fixed,
                    index: 0,
                    annotation: "This is a Fixed!",
                },
                rotation: 0,
            },
            "0x7",
        ),
    ],
}])

[CPerezz]

With the last commit, all of the debugging functions are working for prover.assert_satisfied(). The missing piece is that the prover.varify() causes a panic due to a stack overflow.

This is clearly an issue with the verify_par and integrate the feature developed upstream with it. Will work on it on the following days. As well as the support for Advice column lookups.

[CPerezz]

Following up with this:
running:

fatal runtime error: stack overflow
[2]    20950 IOT instruction (core dumped)  cargo run --example simple-example

The stack overflow gets indeed verified.
The backtrace doesn't even get to be displayed.

The full MockProver::verify_at_rows works perfectly. This makes clear that the error is located in the Display/Debug impls of the VerifyFailure.

[CPerezz]

The issue was caused by:

halo2/halo2_proofs/src/dev/failure.rs

Lines 273 to 276 in cb9e207

	write!(f, "{:#?}", debug)
	}
	_ => write!(f, "{:#?}", self),
	}

Which invokes againg Debug for any non VerifyFailure::ConstraintNotSatisfied struct that needs to be printed ending up in an infinite loop of recursive calls.

The fix is easy, and just requires apply:

@@ -272,7 +272,7 @@ impl<'a> Debug for VerifyFailure<'a> {
 
                 write!(f, "{:#?}", debug)
             }
-            _ => write!(f, "{:#?}", self),
+            _ => write!(f, "{}", self),

The weird thing is that the error that is displayed via Display trait is indeed VerifyFailure::ConstraintNotSatisfied which should have had been processed before by the Debug call.
Investigating on it!

[CPerezz]

Indeed the error comes from a VerifyFailure::Permutation error which was not being handled and the fix is correct for it.
Will try to print column names for these types of failures too!

[CPerezz]

I think the Advice column annotation for lookups will be left apart from this PR and done in a follow-up one.

The reason being that the refactor required is significantly big and affects much more part of the halo2 API. Therefore, I want to be able to control it better and not block the rest of the annotations.

[CPerezz]

Putting this on hold as I've seen an error while displaying the lookup columns info. Basically since here we can have any expression, we need to handle the print of the annotation differently.

Planning to solve it soon.

[CPerezz]

Last commit introduces support (that works) for Instance columns used as lookup table. And adds the basis for Advice columns used as lookup column. (The latter will require more work on a follow-up PR).

This is how it looks:

---- dev::tests::bad_lookup_any stdout ----
error: lookup input does not exist in table
  (L0) ∉ ("Inst-Table")

  Lookup 'lookup' inputs:
    L0 = x1 * x0 + (1 - x1) * 0x2
    ^

    | Cell layout in region 'Faulty synthesis':
    |   | Offset |Witness example| F0 |
    |   +--------+---------------+----+
    |   |    1   |       x0      | x1 | <--{ Lookup 'lookup' inputs queried here
    |
    | Assigned cell values:
    |   x0 = 0x5
    |   x1 = 1

Also, I included support for Advice columns too. All together looks like:

(L0, L1) ∉ ("Inst-Table", "Adv-Table")

  Lookup 'lookup' inputs:
    L0 = x1 * x0 + (1 - x1) * 0x2
    ^

    | Cell layout in region 'Faulty synthesis':
    |   | Offset |Witness example| F0 |
    |   +--------+---------------+----+
    |   |    1   |       x0      | x1 | <--{ Lookup 'lookup' inputs queried here
    |
    | Assigned cell values:
    |   x0 = 0x5
    |   x1 = 1

    L1 = x1 * x0 + (1 - x1) * 0x2
    ^

    | Cell layout in region 'Faulty synthesis':
    |   | Offset |Witness example| F0 |
    |   +--------+---------------+----+
    |   |    1   |       x0      | x1 | <--{ Lookup 'lookup' inputs queried here
    |
    | Assigned cell values:
    |   x0 = 0x5
    |   x1 = 1

[han0110]

Overall look good to me! Nice work!