feat: Implement Column annotations for MockProver debugging

[CPerezz]

This PR includes:

• Ability to annotate columns within a Region.
• Ability to annotate lookup table columns.
• Ability to print in 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.

More work can be done in regards of the debugging/reporting. Specially a good first step would be to improve significantly through a refactor both the emitter by using a table-generator crate and also, implementing a way to obtain all the debugging data outside of the circuit so that anyone can implement a debugger (GTK, GUI ...) (This second idea was given by @ed255).

Here I leave the examples of all of the outputs that this PR improves with annotations.

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.

Resolves: #705

[CPerezz]

[Daira: I moved the description of removed features here so that it won't go into the commit message.]

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

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

Note that prover.verify() output could be improved more. The issue is that requires a deeper refactor as goes throug Debug & Display instead of emit. And so, has no access to the prover instance.

In any case, I started a poll so that we can see whether is worth the refactor efforts or maybe not.
See this tweet
This doesn't apply anymore and we should go towards assert_verify usage.

---

Tests are failing now since if you execute $cargo test unassigned_cell you should see the new display format with Column annotations (aside from a lot of warnings)..

[therealyingtong]

Perhaps it would be a more invasive change, but what about adding an annotation: Option<String> to the Column struct, instead of creating a DebugColumn?

[CPerezz]

I'll not lie I've thought about this! So there are two things why I went this way:

1. This was the less invasive way on which I could also improve the VerifyFailure error display. Otherwise, I couldn't print the annotations within the column itself.

2. The type will no longer be Copy. And that (for some quick observations done) leads to a "significant" amount of .clone() in the codebase. I haven't checked anything further introducing the attribute. So some other complexities could be hidden.

I can go into that direction anyway and try to implement it if you want to check how it'll look like. But maybe it's better to do it in a separated PR so that the diff leaves it more clear.

Just LMK what you think @therealyingtong !

[CPerezz]

I noticed Clippy will never pass here until #719 is addressed.

Also, this should be ready for a final round of reviews @therealyingtong

[CPerezz]

The only things left unaddressed are:

• Annotate Instance columns & display in PermutationError the annotations they have.
• Display implementation would require to display the annotations for Lookup, PermutationError and CellNotAssigned. But this will require significant refactors. See: Add support for Column annotations for MockProver debugging privacy-scaling-explorations/halo2#109 (comment)

To explain it quick, since we don't pass a MockProver instance to VerifyFailure::Display/Debug we need to include into VerifyFailure itself a reference to the annotations of "Region-agnostic columns` (Instance and TableColumn) columns.
Doing this changes code in a lot of places. And if desired, should be something to do in a follow-up PR IMO.

Also, would be nice to know if we should leave this under nightly feature or not. (Will be pretty tricky IMO). But we can definitely try.

[CPerezz]

The last commits update this PR to:

• Not use & and lifetimes across the annotation handling.
• Not support custom Display impl with annotations for VerifyFailure.
• Put the correct order of arguments for annotate_lookup_column fn for consistency.
• Rename name_column by annotate_column.

[CPerezz]

This review re-request button got crazy 😅 Apologies. @str4d @therealyingtong this should be ready to be shipped. I can put it under a nightly feature if you consider it.

[Brechtpd]

I have not tested against the code in this PR so this could already be fixed, but on the PSE fork padded() is now also used in cases where text.len() > width, which will make this subtraction panic. The easiest example of this is when the column name is only a single character, which makes width = 1, and then something like text = "x1" needs to be padded and written in this column.

Even if fixed in some other way, some kind of if statement mitigating this problem that may not produce the nicest output but at least never panics no matter the inputs would be a good idea I think.