The boolean extractor currently handles newly incoming algebraic
constraints. Substitutions that are performed during solving can lead to
constraints being boolean-extractable where we were not able to do
boolean extraction before. This PR tries to perform boolean extraction
on all constraints that potentially changed because of a substitution.
---------
Co-authored-by: schaeff <thibaut@powdrlabs.com>
In a future PR (#3208) we will try to run boolean extraction on any
newly changed constraint. This can have the risk that we perform boolean
extraction on a constraint where we already have run boolean extraction.
This PR stores a map of substitutions we performed to avoid introducing
a new boolean variable that then just turns out to be equivalent to an
already existing one.
Closes 3202
---------
Co-authored-by: schaeff <thibaut@powdrlabs.com>
The layered trait-based solver structure does provide a clean separation
but if we want to implement #3106 we have to call the boolean extractor
component from the innermost component which is quite difficult to
achieve. Also, most of the layers were just a simple pass-through for
most of the functions.
So this PR collapses the boolean extractor, linearizer and base solver
into one solver. It still keeps the VarTransform layer because it is
convenient to keep the type generic.
Removes the special introduction and removal of bus variables because
the solver can now handle this on its own through the `LinearizedSolver`
component. It also has the benefit that we do not need to run the
optimizer twice any more (once with bus interaction variables and once
without).
Previously we would introduce a new variable type outside of the solver
and replace all bus interactions `bus_interaction(1, x + y * z)` by
`bus_interaction(1, bus_var_1)` and the algebraic constraint `bus_var_1
= x + y * z`.
Now the `LinearizedSolver` is a component inside the solver that
replaces all bus interaction fields (that are not already constants or
simple variables) and also replaces all non-linear components:
`bus_interaction(1, x + y * z)`
becomes
```
bus_interaction(1, v1)
v1 = x + v2
v2 = y * z
```
The reason behind also replacing non-linear parts is because range
constraints are only stored for variables, not for all sub-expressions.
Also if we find the same non-linear sub-expression multiple times, we
can now replace it directly by the same variable.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
Introduce the concept of `size` for range constraint. It provides an
upper bound for the number of values in the rang econstraint and can be
different from the range width.
Adds a solver that introduces new variables for every non-linear
component in an algebraic constraint and also for every bus interaction
field that is not a constant or a variable already.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
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>
Optimize exhaustive search by directly applying assignments and doing it
in the solver, so further exhaustive searches profit from the new
information.
- Initial time for solver optimization in `test_optimize` (release):
4.0 seconds
- Directly apply assignments to the variable sets and constraint system
2.6 seconds
- Directly apply assignments inside the solver (i.e. also update the
range constraints)
2.57 seconds
Extracts boolean variables as alternative constraints for all
constraints in the solver.
The exact implementation adds a layer of the Solver trait on top of an
existing solver where we try to extract a boolean variable for all
constraints that are added to the solver.
The interface is also simplified a little in that we always start out
with an "empty" solver and use the `add_algebraic_constraints` and
`add_bus_interaction` functions to fill it with the system.
This PR adds a new optimizer step:
5568270f77/autoprecompiles/src/constraint_optimizer.rs (L96-L108)
This can be useful to remove "left-over" range constraints, e.g. from
removed memory bus interactions:
- Imagine a memory bus interaction receiving a previous time stamp and
then having a range constraint like `[current_timestamp - prev_timestamp
- 1] in [BIT16]` to enforce that it is smaller than the current
timestamp.
- Then, `prev_timestamp` would only be mentioned in this stateless bus
interaction after the memory bus interaction is removed by the memory
optimizer.
- The `remove_disconnected_columns` step would not remove it, because
`current_timestamp` is also mentioned and it is connected to a stateful
bus interaction.
- The constraint is still redundant: For any value of
`current_timestamp`, the prover could pick a satisfying value for
`current_timestamp - prev_timestamp - 1` (e.g. $0$) and solve for
`prev_timestamp`
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
This way, we guarantee that there are no duplicates, which can cause
performance issues.
Although, it seems like on the OpenVM Keccak test case (#3104), there
are not many duplicates and performance decreases slightly:
```
$ cargo bench --bench optimizer_benchmark
Benchmarking optimize-keccak/optimize: Warming up for 3.0000 s
Warning: Unable to complete 10 samples in 5.0s. You may wish to increase target time to 45.8s.
optimize-keccak/optimize
time: [4.5420 s 4.5712 s 4.6035 s]
change: [+3.5320% +4.2324% +5.0959%] (p = 0.00 < 0.05)
Performance has regressed.
```
Implements a queue over constraint system items such that items are
re-queued when their variables are updated.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
Turns `Solver` into a trait to abstract away the bus interaction handler
and also allow other implementations in the future.
It also makes the solver persistent across optimization loops so that we
do not have to derive the same range constraints all over again.
This is also a preparatory PR to make the solver more independent from
the constraint system: The constraint system inside the solver will have
way more redundancies in the future.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
Removes algebraic constraints that are implied by other algebraic
constraints.
In order to do that, grouped expressions are turned into products of
factors such that these factors are as much normalized as possible. Then
we try to find algebraic constraints that are divisors of other
algebraic constraints (i.e. the factors are subsets).
Sometimes we want to run an optimization that depends on range
constraints. Using the solver is the best way to determine range
constraints, so it should also return them.
Renames QuadraticSymbolicExpression to GroupedExpression. The advantage
of doing it his way is also that we can slowly change what is called
`QuadraticSymbolicExpression` afer this PR, namely the one with
SymbolicExpression as RuntimeConstant to GroupedExpression and easily
see which on is generic already and which is not.
This PR refactors `QuadraticSymbolicExpression`: I removed the reference
to
[`SymbolicExpression`](f60e9d9f69/constraint-solver/src/quadratic_symbolic_expression.rs (L70)).
It can represent values that are known at runtime, represented as an
expression. We don't need this in the context of APC: Variables are
either unknown or known at compile time, and therefore can be
represented as a `FieldElement` instead.
The idea is to introduce [this
trait](4989be08f3/constraint-solver/src/runtime_constant.rs (L11)),
which is implemented by `SymbolicExpression` and any `T: FieldElement`.
This way, we can continue to use the solver with
`QuadraticSymbolicExpression<SymbolicExpression<T, V>, V>` (equivalent
to the current `QuadraticSymbolicExpression<T, V>`) in the old JIT
pipeline and use the simpler `QuadraticSymbolicExpression<T, V>` in the
APC pipeline.
---------
Co-authored-by: chriseth <chriseth.github@gmail.com>
