Pretty print polynomial constraint errors

[moreSocratic]

VerifyFailure currently produces long hard to read errors. It takes manual work to map cell values in the error back to the variables in the polynomial constraint. We should provide a pretty printed instance of the polynomial constraint with queries substituted for cell values.

E.g. a multiplication where the result cell has been erroneously assigned lhs * rhs + 1

halo2/halo2_proofs/examples/simple-example.rs

Line 116 in ccfe3e8

vec![s_mul * (lhs * rhs - out)]

Currently we get errors like this:

        ConstraintNotSatisfied {
            constraint: Constraint {
                gate: Gate {
                    index: 0,
                    name: "mul",
                },
                index: 0,
                name: "",
            },
            location: InRegion {
                region: Region {
                    index: 3,
                    name: "mul",
                },
                offset: 0,
            },
            cell_values: [
                (
                    VirtualCell {
                        name: "",
                        column: Column {
                            column_type: Advice,
                            index: 0,
                        },
                        rotation: 0,
                    },
                    "0x2",
                ),
                (
                    VirtualCell {
                        name: "",
                        column: Column {
                            column_type: Advice,
                            index: 0,
                        },
                        rotation: 1,
                    },
                    "0x7",
                ),
                (
                    VirtualCell {
                        name: "",
                        column: Column {
                            column_type: Advice,
                            index: 1,
                        },
                        rotation: 0,
                    },
                    "0x3",
                ),
            ],
        },

I'd like to also get a pretty printed version of the error above:

Constraint "mull" not satisfied in region "mul" at offset 0
 s_mul * (lhs * rhs - out)
 = 1 * (2 * 3 - 7)
 = -1

#681 is a step towards being able to pretty print, but is insufficient for the example above.
Queries at rotations having different variable names, and substitution of simple selectors (s_mul) require extending queries and or the Expression AST with metadata.

[str4d]

Have you tried using MockProver::assert_satisfied instead of MockProver::verify? assert_satisfied pretty-prints the errors (except for permutation errors IIRC which haven't had a pretty printer implemented yet) before panicking. verify returns the typed errors and doesn't print anything because it is enabling the caller to programmatically introspect the errors (e.g. to check that an expected error does occur for some test circuit) rather than visually do so.

[moreSocratic]

I had not, That's a lot better. The only real improvement would be preserving variable names.