zcash / halo2

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

Check that the conditions for applicability of the selector combining optimization are correctly enforced, and document why #655

Open daira opened 2 years ago

daira commented 2 years ago

From https://zcash.github.io/halo2/design/implementation/selector-combining.html :

Check (or ensure by construction) that all polynomial constraints involving each simple selector $s_i$​ are of the form $si \cdot t{i,j}​ = 0$ where $t_{i,j}$​ do not involve any simple selectors.

See also https://zcash.github.io/halo2/background/polynomials.html#lagrange-basis-functions .

daira commented 2 years ago

@therealyingtong and I reviewed the relevant code. It was correct, but not obviously correct!

Define a simple Expression to be one that contains any simple selector as a subterm.

Define the factors of an Expression to be the set of subterms that are combined only using Expression::{Product,Scaled,Negated}. (The factors can themselves be arbitrary Expressions.)

Define the maximal degree of a selector to be:

The argument is:

All of this should be documented in the code!