This will be a series of PRs that reduces trace gen code duplication in
multiple powdr APC clients, planned as the follows:
1. [This PR] Simplify OVM client trace gen code using existing
optimization in other client, also unifying data types for later PR.
2. [Next PR] Create `TraceHandler` trait for implementation in different
powdr APC clients, with trait functions mostly generating unified data
types across different clients. Add `TraceHandler` as an associated type
in `Adapter`.
3. [Another PR] Potentially cache `TraceHandler` outputs in the executor
for clients that run execution multiple times (so that we don't
recompute in `generate_trace` each time).
4. [Another PR] Further clean up including potentially revive things
like `is_valid_index`.
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.
