mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-01-10 09:58:20 -05:00
bdf3a5fefa
This PR adds a new optimizer: If a stateless bus interaction (a.k.a. lookup) implements a low-degree function, it is replaced by a polynomial constraint (and range constraints). Some examples include: - `xor(a, 0xff)` (logical `not` on bytes): This is a linear function (`255 - a`) - `xor(a, b)`, where `a` and `b` are known to not have the same bits set: This equals `a + b` - `xor(a, b)`, where `a` and `b` are known to be bit-valued: This is equal to `a + b - 2 * a * b` Doing this replacement has several advantages: - A bus interaction is replaced with a polynomial constraint (which is usually much cheaper) - Because the output is equal to a low-degree expression of the inputs (often linear), the inliner can inline it, so we don't have to commit to it Note that in addition to the linear function, a lookup always *also* enforces a range constraint. These are added to the system by using the API added with the range constraint optimizer (#3151). In many cases, these constraints are redundant and can be removed again by the range constraint optimizer (e.g. the inputs might come from memory, which can be assumed to store byte-constrained words. --------- Co-authored-by: Leo <leo@powdrlabs.com> Co-authored-by: chriseth <chris@ethereum.org>