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>
Bus interaction variables were introduced in order to be able to derive
knowledge about complex expressions used in bus interactions. The system
is quite good in handling affine expressions, though, so in order to
keep the number of variables (and constraints) down, we only replace
non-affine expressions in bus interactions.
```
$ cd openvm
$ 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 44.2s.
optimize-keccak/optimize
time: [4.3703 s 4.3856 s 4.4020 s]
change: [-1.2781% -0.5240% +0.2094%] (p = 0.21 > 0.05)
No change in performance detected.
```
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).
We used to need the Opcode of the APC in order to hard-code it in the PC
lookup. However, for a while, we have removed PC lookups entirely,
hard-coding the PC in the execution bridge receive instead.
This removes the necessity to store the opcode. It was only used as an
ID of the APC. But for this, we can use the PC instead. This has the
added benefit that we can more easily relate it to the original program.
The `BusType` enum in the `autoprecompiles` crate still listed the
OpenVM bus types. Now, the bus types that we actually rely on are
hard-coded (e.g. execution bridge, memory, etc), but there is an `Other`
variant where the integration can add their own types:
92ae7469e8/autoprecompiles/src/bus_map.rs (L5-L19)
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
This PR adds a module to the `riscv-elf` crate that collects labels,
their addresses, and jumpdests from a RV64 ELF binary. It does not
compute debug infos and all the other stuff that the current 32-bit
module does.
---------
Co-authored-by: Steve Wang <qian.wang.wg24@wharton.upenn.edu>
This PR generalizes the memory optimizer to not make any specific
assumptions about the structure of memory bus interactions. This is done
by turning `MemoryBusInteraction` into a trait, which is an associated
type in the `Adapter`. Currently, there is one concrete implementation,
`OpenVmMemoryBusInteraction`.
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.
This change extracts the reachability algorithm and adds a new feature
that we will need for the seqz optimization: Find all variables that are
connected to a stateful bus interaction in any way that does not go
through a certain set of variables. The idea will be that we know of a
more efficient way to compute a certain relation between several input
variables and one output variable. This reachability routine can be used
to determine which constraints are used to compute the relation and can
be replaced by the more efficient routine.
In order to get a feel for the optimizer, I think it is good to also
output the column count. It is rather difficult to get the column count
before optimization, but in the end we are only interested in the effect
of a new optimization step anyway, so I think this is fine.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
Generalizations that make fewer assumptions about the structure of bus
interactions like PC lookups and bus interactions. See comments below.
One change is that we know inline the initial PC (because we know it for
any given basic block), which leads to *all* PC lookups being removed,
slightly improving performance (at least reducing one witness column &
one bus interaction).
---------
Co-authored-by: schaeff <thibaut@powdrlabs.com>
Suggested alternative to #3057: Instead of `start_idx`, we store the
`start_pc` to identify a basic block. Both should uniquely identify the
basic block, but the start PC is useful information on its own (whereas
the `start_idx` only makes sense to someone who knows the entire
program).
See also
https://github.com/powdr-labs/powdr/pull/3055#discussion_r2215738707.
This PR does two things:
- it partially removes the notion of opcode in the autoprecompile crate,
and instead relies on user provided functions to know if an instruction
is allowed/branching
- it uses VmOpcode as much as possible in the openvm crate instead of
usize
After this PR, the only remaining notion of opcode in the apc crate is
in the `SymbolicInstructionStatement` where it is still a single field
element. @georgwiese shared ideas to remove that too, or at least shift
it to the client, see #3055
