zcash / halo2

The Halo2 zero-knowledge proving system
https://zcash.github.io/halo2/
Other
743 stars 499 forks source link

Enable easier debugging for equality constraints improving `VerifyFailure` #468

Open CPerezz opened 2 years ago

CPerezz commented 2 years ago

After implementing keccak with Halo2. One of the most complex things that I found was that debugging equality constraint errors was quite complex.

The reason, the VerifyFailure::Permutation does not contain any information about the Cell values that are being constrained nor any annotations for them.

That forces to go for solutions like: FJdQj2RX0AMS3fa Where you comment out all the equality constraints and uncomment one-by-one until you hit the one that is causing the error.

While this works, after discussing with @therealyingtong the issue she suggested to do something along the lines of:

/// A [`Layouter`] for a single-chip circuit.
pub struct SingleChipLayouter<'a, F: Field, CS: Assignment<F> + 'a> {
    cs: &'a mut CS,
    constants: Vec<Column<Fixed>>,
    /// Stores the starting row for each region.
    regions: Vec<(String, RegionStart)>, // Includes the name of the `Region`.
    /// Stores the first empty row for each column.
    columns: HashMap<RegionColumn, usize>,
    /// Stores the table fixed columns.
    table_columns: Vec<TableColumn>,
    _marker: PhantomData<F>,
}

Maybe another possibility is to see how we can extend the Permutation enum branch without major refactors but still including more info that is useful to better locate the errors.

I would like to work on that and try to come up with something if it's Ok. Otherways, if you consider is something that the Halo2 team shoud taggle, will just leave the suggestions I have.

Thanks for this amazing piece of software!!! :smile:

str4d commented 2 years ago

I think a good starting point would be to refactor VerifyFailure::Permutation to use location: FailureLocation instead of row: usize. Identifying the actual region responsible was much harder than just listing the row, which was sufficient for my purposes back when I first wrote MockProver. But we've now done that work for lookups, and extended it to regular constraint failures; it makes sense that we should do the same for equality constraints.

Ideally, the failure information would include a pair of locations, pointing at the specific equality constraint that is actually failing. This is even harder to track, but is where I want us to end up. I should also pick a better name than VerifyFailure::Permutation with this end goal in mind...