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>
Fixes a soundness bug @chriseth
[found](https://github.com/powdr-labs/powdr/pull/3151/files#r2267259864)
that was introduced in #3151: I thought we can e.g. check `expr` to be 6
bit by checking `4 * expr` to be a byte. That is incorrect, e.g.
$4^{-1}$ would pass the check but should not.
We used the default tuple range checker sizes, but it should be read
from the config. For example, in the reth benchmarks, the sizes are
actually different, leading to potential soundness or completeness bugs.
This PR generalizes the memory optimizer to not make any specific
assumptions about the structure of memory bus interactions. This is done
by turning `MemoryBusInteraction` into a trait, which is an associated
type in the `Adapter`. Currently, there is one concrete implementation,
`OpenVmMemoryBusInteraction`.
Generalizations that make fewer assumptions about the structure of bus
interactions like PC lookups and bus interactions. See comments below.
One change is that we know inline the initial PC (because we know it for
any given basic block), which leads to *all* PC lookups being removed,
slightly improving performance (at least reducing one witness column &
one bus interaction).
---------
Co-authored-by: schaeff <thibaut@powdrlabs.com>
Changes:
- Removed `PolyID`, including the polynomial type. Now
`AlgebraicReference` is just an ID with a name (for display purposes)
- Removed the `Column` type, which would have been essentially the same
as `AlgebraicReference`
- Renamed `legacy_expression` -> `expression`
- Because of the type change, I needed to update checked-in CBOR files.
We can actually encode the `x0` semantics in the memory bus interaction
handler.
Note that this still keeps a register access to `x0` that could be
removed, but now at least we're not allocating 4 witness columns for the
value *and* we might be able to derive more values at compile time.
Reverts powdr-labs/powdr#2827
It leads to a witness bug (OodMismatch, witness does not satisfy the
constraints) in the keccak test with `--inputs 25000 --autoprecompiles
3`
Depend on: https://github.com/powdr-labs/powdr/pull/2808
Mostly the same as: https://github.com/powdr-labs/powdr-openvm/pull/121
Differences:
1. Given that we generate apc for all eligible basic blocks, some apc
fail due to some new optimization applied (currently narrowed down to
`exhaustive_search`). Note that previously in powdr-openvm, apc can be
generated for all eligible basic blocks.
2. Remove basic block that fail to generate apc for from the list of
eligible basic blocks, which requires propogating error information all
the way up to `customize`.
