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>
Previously, when evaluating APC constraints/bus interactions to
`AirBuilder::Expr` in `AirBuilder::build` implementation of `PowdrAir`,
it's a two step process:
1. Convert APC `AlgebraicExpression` to `SymbolicExpression` via
`algebraic_to_symbolic`
2. Evaluate `SymbolicExpression` to `AirBuilder::Expr`
However, the first step doesn't add any information but was only needed
so that we can use the `SymbolicEvaluator` trait implementation from
`ovm_stark_backend`. Worse, this trait includes data structures that are
not in `AlgebraicExpression` at all (first row, transition,
evaluate_node, etc.) and we had to take care of them in our
implementation.
This PR implemented the following changes:
1. Create an `AlgebraicEvaluator` trait in the APC crate that removes
the extraneous APIs from `SymbolicEvaluator`.
2. Create a `WitnessEvaluator` implementation of this trait that's
generic over the Field, Expr, and Var types, which can be used across
multiple clients.
3. Rewrite `RowEvaluator` with the `AlgebraicEvaluator` trait as well.
Concretely, this removes the `algebraic_to_symbolic` step entirely and
hopefully can speed up proving, if at all.
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
This should be the last thing I identified in OVM witgen (as well as in
other clients) that can be moved to the APC crate instead of done at the
client site.
Depends on and do not merge till after #3277. This simplifies the
complex `genenerate_trace` bound that is generic over the instruction
handler. Before, it attaches too many generic trait bounds of the
instruction handler.
This PR cherry picked from #3251, which attempts to use associated types
of `Adapter` in `TraceHandler`. However we encountered a few problems
with that approach:
1. #3251 requires a generic `A` on `apc::generate_trace<A: Adapter>`,
which requires a complex trait bound fixing concrete types on
`ovm::generate_witness<A: Adapter<Field = F, Instruction = Instr<F>,
InstructionHandler = OriginalAirs<F>, AirId = String>>` . This is
because `apc::generate_trace` expect generic associated types of
`Adapter` while `ovm::generate_witness` can only provide OVM specific
ones, and therefore `ovm::generate_witness` has to fix the trait bound.
This complex trait bound propogates all the way up to
`PowdrChip::generate_air_proof_intput`, `PowdrExecutor`,
`SpecializedExecutor`, `SpecializedConfig`, and more, making the code
base undesirably complex.
2. One "proper" solution to the problem above is to make related inputs
from OVM structs generic on the adapter except the `Field`. However,
this requires a whole refactoring over many struct fields and
potentially making a generic trait `OVMInstructionHandler` apart from
`InstructionHandler`, which we've decided not to pursue at the moment.
3. We have to keep `F` generic in OVM, because we want to support the
field of multiple `StarkConfig`s in OVM, aliased as `Val<SC>` and
frequently appearing with the bound `F = Val<SC>`.
Moral of the day is that refactoring is proper and modular up till the
point where it tags too many generic arguments/bounds that make the code
base explode.
However, a few features we still decided to "cherry pick" from #3251:
1. `TraceHandler` doesn't need to be a trait, as the data structures in
its client site implementation constructors are quite common across
clients and we can therefore make it a `TraceHandler` struct in APC
crate.
2. A further simplification suggested by [a
comment](https://github.com/powdr-labs/powdr/pull/3251#discussion_r2335874344)
in #3251 shows that we can further inline the `TraceHandler` struct away
and simply invoke everything via `generate_trace` in the APC crate.
3. API for `InstructionHandler` which supports fetching of both air and
id.
Inspired by @Schaeff's comment:
https://github.com/powdr-labs/powdr/pull/3246#discussion_r2324844469
A few simplifications:
1. Added `BusInteractionEvaluator` to replace duplicated code in side
effects removal/replay.
2. Removed `RangeCheckerSend` entirely and replace by a simple filter on
bus interactions.
3. Added `ConcreteBusInteraction` with evaluation results for side
effects removal/replay.
All features should be generic over client.
In OVM witgen, we currenlty have (Symbolic)RowEvaluator, which is used
to remove range check side effects (as they are SymbolicExpression
based). We also use it to replay APC bus interactions, which are first
converted from AlgebraicExpression to SymbolicExpression. However, this
step is unnecessary, as this PR creates an (Algebraic)RowEvaluator which
we can use to evaluate APC bus interaction replay. This new row
evaluator is in the APC crate and can be used across different clients.
Depends on #3245.
1. There are a few more methods I was hoping to factor into OVM's
`TraceHandler` implementation, but didn't manage to do so. I'll document
them in comments.
2. Note that in other clients a PR implementing `TraceHandler` will be
opened, so the trait might undergo additional changes if warranted by
other clients.
Roadmap:
1. [#3245] Simplify OVM client trace gen code using existing
optimization in other client, also unifying data types for later PR.
2. [This PR and pair PR in other clients] 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.
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
Currenlty we obtain air name via two methods: `executor.air().name()`,
and `executor.air_name()` and they apparently return different results.
Needed for #3251, so that we can use `Adapter::InstructionHandler` to
get air names of dummy instructions in witgen.
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`.
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.
