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>`
As a real-life example, consider this constraint:
```
(opcode_loadb_flag0_1 + opcode_loadb_flag1_1) *
(
from_state__timestamp_0
- rs1_aux_cols__base__prev_timestamp_1
- rs1_aux_cols__base__timestamp_lt_aux__lower_decomp__0_1
- 131072 * rs1_aux_cols__base__timestamp_lt_aux__lower_decomp__1_1
- + 2
) = 0
```
And assume that `rs1_aux_cols__base__prev_timestamp_1` does not appear
in other constraints, i.e., is a free variable.
Then this constraint is redundant: For any assignment of the other
variables, the prover can always solve for the value of
`rs1_aux_cols__base__prev_timestamp_1` that makes the second factor
evaluate to 0.
The previous implementation would not catch that: It would just call
`constraint.try_solve_for(free_variable).is_some()`, which would return
`false`, see the implementation of `try_solve_for`:
c5b35ea4b0/constraint-solver/src/grouped_expression.rs (L511-L533)
The code removed here is an execution optimization to not have to
perform more computation than needed. However it relies on some
assumptions on the optimizer that don't always hold, therefore it's
safer to remove it.
This fixes some benchmarks that were broken on nightly.
- Remove all crates that are not linked with `autoprecompiles`,
`openvm`, `constraint-solver`
- Remove tests and artifacts linked with removed crates
- Adjust CI
manual ecc using msm with the version that does not use pippenger, which
is cheaper
INFO │ ┝━ ｉ [info]: total_trace_cells = 12_704_468 (excluding
preprocessed)
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
We used to export instruction in their JSON format, e.g.
`{"opcode":512,"a":1879048082,"b":1879048082,"c":2013265793,"d":268435454,"e":268435454,"f":0,"g":0}`.
I changed this to be the pretty-printed string instead. I think this
makes more sense, because we don't reading them like this is hard and we
don't want to re-implement the pretty-printing in Python.
I checked that currently our Python scripts don't really read this
value, they only use the length of the list, so this PR doesn't break
them. In the future, I'm hoping to get Claude to generate an interactive
version of the effectiveness plot, so that we can also explore the
source code of each block.
Nightly has been failing for a while. We should fix that, but by moving
ignored the tests after the benchmarks, we should at least get nightly
benchmark results again (and test our most important guest programs).
I think this is also a good idea in general, because we often manually
run nightly to get the latest benchmarks on a particular branch. This
way, we get results earlier.
I started a manual run on this branch:
https://github.com/powdr-labs/powdr/actions/runs/17212171321
Introduce `PgoAdapter` which wraps `Adapter` and can call apc
generation. Removes the match statements over the pgo method. Breaking
change. Now the client can pick some pgo implementations like
`pgo::CellPgo` and use it like
`CellPgo::<MyAdapter>::new(pgo_data).generate_apcs(blocks)`. The client
can also implement `PgoAdapter<A: Adapter>` for its own pgo
implementation.
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.
After #3209, it is no longer necessary to list OpenVM's "bitwise lookup"
bus in the `BusType` enum, which lives in the VM-agnostic
`autoprecompiles` crate.
Having an extra function for this used to make sense when we were
calling it twice (once with and once without bus interaction variables),
but that got removed with #3171. I think now inlining this is easier to
read.
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>
Summary: We do not need to add the range constraint on the output
because the output is uniquely determined by the formula and the range
constraints on the inputs.
Details:
This slightly improves the "low degree bus interaction optimizer". It
replaces a bus interaction by an algebraic constraint and simple range
constraints in the following way:
1. It performs exhaustive search about which of the non-constant fields
in the bus interaction are inputs and which (only one) is the output
2. Determines currently-known range constraints on inputs and outputs
3. Using exhaustive search, chooses a candidate function and checks that
for all input values in the range constraints, the candidate computes
the same output as the bus interaction would (i.e. the bus interaction
also allows exactly one output compatible with the concrete values for
the inputs).
4. If such a candidate is function, it replaces the bus interaction by
the candidate turned into an algebraic constraint and simple range
constraints (the ones determined in the beginning)
This PR changes the mechanism in that it does not re-add range
constraints for the output, only for the inputs. The reason is that the
algebraic constraint directly computes the value for the output for all
inputs within the range constraints of the input. So the algebraic
constraint already enforces the range constraint on the output from the
range constraints on the inputs.
Previously, for successful tests, it would still update the expectation
file and print that it did so, even though the contents were the same.
Now the "update" message is only printed if the contents are actually
different.
The feature is actually used in the crate. It did not produce a build
error because we never compile crates individually and it's enough for
the feature to be enabled in some crate.
