This PR changes `pub(crate)` visibility of the fields of
`GroupedExpression` back to `non-pub` as it was before the extraction of
the solving routines. The solving routines do not really need write
access to those fields and read-access is obtained using `components()`.
Removes the bit decomposition solver inside GroupedExpression /
AlgebraicConstraint.
Its functionality is now mostly taken over by the constraint splitter.
This is not fully true: The constraint splitter only works for offsets
that are constant, but this should not be a hindrance for our current
use-cases. If we need it, it should not be too difficult to extend it,
we only need to extend the final part of the `find_solution` function,
where it checks if the solution is unique.
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
Splits constraints into multiple independent ones based on the following
idea:
Suppose we have the constraint `x + k * y + c = 0` with `x` and `y`
being variables (or expressions containing variables) and `k` and `c`
are constants. Furthermore, the range constraints of `x` and `y` are
such that no wrapping occurs in the operations, i.e. the constraint is
equivalent to the same constraint on the integers (where field elements
larger than half the modulus are mapped to negative numbers).
Then the same constraint is also true modulo `k`, where we get `x % k +
c % k = 0`. If this equation has a unique solution `s` in the range
constraints for `x`, we get a new constraint `x - s = 0`. We can
subtract that constraint from the original to get `k * y + c - s = 0`
and iterate.
Closes https://github.com/powdr-labs/powdr/issues/3108
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
This moves the reachability analysis module from the autoprecompiles
crate to the constraint solver create. I will need it in that crate in
an upcoming PR and it also does not have any autoprecompiles-specific
code.
I also changed the code to use `IndexedConstraintSystem` instead of
`ConstraintSystem`.
Derives `Clone` (and some other traits) for `ConstraintRef`. Since it is
a reference, it should implement Clone.
Note that `Clone` for `AlgebraicConstraint` is only auto-derived if `V`
is `Clone`, which is the case if `V` is a reference.
In order to make the optimizer clearer, this PR tries to put all
optimization passes one after another in `optimize_constraints`.
Also removes `JournalingConstraintSystem`.
TODO:
- [x] Figure out what to do about the `JournalingConstraintSystem`
- remove `Deref` for `AlgebraicConstraint` so we cannot call functions
that expect `&GroupedExpression`
- make constraint solver work over constraints instead of expressions
- move algebraic expression to its own module, along with said solver
- make more components like the boolean extractor work on
`AlgebraicConstraint<&E>`
I got confused before about what is an expression and what is a
constraint.
For example, in boolean extraction, we return an expression which I
thought was the boolean. But it turns out the expression is the new
constraint.
Similarly, there are some things that we can do for constraints which
wouldn't work for expression: for example, `2 * x == 0` can be replaced
by `x == 0`. But `2 * x` as an expression cannot be replaced by `x`.
This PR introduces a wrapper and uses it where possible.
Some caveats:
- This PR implements `Deref` and `DerefMut` for the constraint, which
means that we can call any function which takes a reference to an
expression by passing a constraint. This partially defeats the purpose
of the change, as we can by mistake call a function which would only be
meant for expressions. This is fixed in #3220
- This PR keeps the `solve` functions as before, where they run on
expressions, not constraints. This does not make sense in my opinion, as
solving should be for constraints only, however here's an example which
would break if we made this change: if we are solving the constraint `a
* b = 0` we want to solve the constraint `a = 0`. This would require
creating a constraint out of `a` on the fly, which is not implemented in
this PR. This is fixed in #3220
This new optimizer step removes duplicate factors in a single algebraic
constraint.
It was detected by the assertion that is now commented, which assumed
that if all factors of one constraint also appear in another constraint
then the number of factors is also less or equal the number of factors
in the other constraint.
By running the duplicate factor removal right before that other step
this assumption gets true.
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.
