Support Column annotations for better debugging experience

[CPerezz]

Hey. In PSE we are sometimes having bad times debugging zkevm-circuits. The thing resides on the fact that we get traces that do not contain the names of the Columns mainly.

I thought that would be nice to have a way on which we can annotate columns and later on, get the annotations as helpful debug info with the MockProver.

To put an easy example, I wish we could get something like:

  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.

Instead of having Columns called A0 or I3 and so on.. which is the current behaviour.

[CPerezz]

Initial exploration/discussion at #706

[str4d]

Generally +1 on annotating columns somehow. More debugging annotations are always useful!

It's likely going to cause the CLI dev tooling output to get rather unwieldy though; this is where having a GUI or web-based debugging interface would help, as these could be rendered as annotations.

[str4d]

An alternative way to render the column annotations (either always, or as an option) would be to provide a map underneath from the A0-style identifiers to the annotations.

In any case, collecting the annotations (in a similar way to how we collect similar annotations everywhere else, via closures) is definitely something we should do, regardless of how they are rendered.

[CPerezz]

I've extended it a bit. Now the ConstraintNotSatisfied case is also correctly handled as seen here:

  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

The main things left to do are:

• Apply labeling for lookup columns and figure out how to handle global vs regional columns and them annotations
• Fix the prover.verify() output to display the column annotations decently.

[CPerezz]

After 5e88f12 the render of Lookup table columns is enabled. Kudos to @ed255 for the help!!!
This is the current output for the lookups where we show the column that we fail to make the lookup to + the columns involved in the expression that we're looking up at.

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

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

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

The last challenge now is to fix the regular prover.verify() outputs. Since, as you can see here, this is the error we currently have:

thread 'dev::tests::bad_lookup' panicked at 'assertion failed: `(left == right)`
  left: `Err([Lookup { lookup_index: 0, location: InRegion { region: Region 2 ('Faulty synthesis'), offset: 1 } }])`,
 right: `Err([Lookup { lookup_index: 0, location: InRegion { region: Region 2 ('Faulty synthesis'), offset: 1 } }])`', halo2_proofs/src/dev.rs:1150:9

The issue here is that the VerifyFailure contains a LocationFailure which at the same time contains a metadata::Region. And this IS the issue. The HashMap with the Region allocations is not displayed. But the Eq and PartialEq impls which are derived via macros indeed consider the HashMap. Which is None for the hand-made one, and Some(HASHMAP_WITH_THE_ANNOTATIONS) for the fn-made one.

The idea here is:

1. Manually implement Eq and PartialEq for metadata::Region<'a>. So that the HashMap of the annotations is not considered to constraint equality.
2. (And this might be a bit larger), a re-implementation of Display for VerifyFailure struct will be needed so that we can see the error like:

 left: `Err([Lookup { lookup_index: 0, annotation: "Annotation", location: InRegion { region: Region 2 ('Faulty synthesis'), offset: 1 } }])`,

Or the one that would be really helpful:

ConstraintNotSatisfied {
            constraint: Constraint {
                gate: Gate {
                    index: 0,
                    name: "Equality check",
                },
                index: 0,
                name: "",
            },
            location: InRegion {
                region: Region 1 ('Wrong synthesis'),
                offset: 0,
            },
            cell_values: [
                (
                    VirtualCell {
                        name: "",
                        column: Column {
                            column_type: Advice,
                            index: 0,
                            annotation: "This is annotated!"
                        },
                        rotation: 0,
                    },
                    "1",
                ),
                (
                    VirtualCell {
                        name: "",
                        column: Column {
                            column_type: Advice,
                            index: 1,
                            annotation: "This is annotated too"
                        },
                        rotation: 0,
                    },
                    "0",
                ),
                (
                    VirtualCell {
                        name: "",
                        column: Column {
                            column_type: Advice,
                            index: 2,
                            annotation: ""
                        },
                        rotation: 0,
                    },
                    "0x5",
                ),
                (
                    VirtualCell {
                        name: "",
                        column: Column {
                            column_type: Fixed,
                            index: 0,
                            annotation: "FixedColAnn"
                        },
                        rotation: 0,
                    },
                    "0x7",
                ),
            ],
        },

Would you be Ok with these two points @str4d ?? I think specially the second one will be really helpful although will imply a decently-big rework in the Display trait impl.

[CPerezz]

After 08632e1a the format I achieved for the debug display of VerifyFailure::ConstraintNotSatisfied was as follows:

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",
                ),
            ],
        },

As you can see, this requires auxiliary types which are obfuscated to any other part of the lib but that are necessary in order to be able to inject the Column names inside of the Column section itself.
This also required to re-implement manually Debug and Display for this enum.

[therealyingtong]

This issue is also related to #681.