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`.
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.
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)
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.
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.
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.
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.
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>
In the `hint_k256_inverse_field_10x26` and `hint_k256_sqrt_field_10x26`
functions, this PR ensures that the returned result actually consists of
26 bits limbs, as the name suggests. (Except for the most significant
limb, which is 22 bits.) This means that the field element is weakly
normalized and can be used safely by the guest program.
Extracted from #3130
See [this
comment](https://github.com/powdr-labs/powdr/pull/3130/files#r2268175800):
> If the bit value is not in range, `handle_variable_range_checker` will
return the expected range, and `handle_bus_interaction_checked` will
intersect it with the previous range constraint (a known number), notice
the ranges don't overlap, and return an error.
As part of #3130, it might happen that the brute-force algorithm tries
to set the `bits` field to an out-of-range value. As mentioned in the
comment above, this would anyway result in an error if
`handle_bus_interaction_checked` is used, so panicking here is overly
strict.
Fixes a soundness bug @chriseth
[found](https://github.com/powdr-labs/powdr/pull/3151/files#r2267259864)
that was introduced in #3151: I thought we can e.g. check `expr` to be 6
bit by checking `4 * expr` to be a byte. That is incorrect, e.g.
$4^{-1}$ would pass the check but should not.
We used 5 for OpenVM's default constraint max degree bound for a long
time since that's what was in their SDK example, but they actually use
and suggest app log blowup = 1 for app proofs, which leads to max_degree
= 3. This PR changes the default to 3.
The basic PR is quite simple, see the first commit. A lot of the
`max_degree` propagation in the second commit is because of the
`get_air_metrics` function that needs it to call an OpenVM internal
function, and the max degree is not available in any existing data
structure at that point.
I thought the easiest was just to add it to these functions, and I had
to change one trait. But that felt easier/less invasive than changing
associated types/constants of other traits. @Schaeff let me know if this
is fine or if you prefer another route.
collect the following metrics for autoprecompiles:
- `(before|after)_opt_(cols|constraints|interactions)`
- `total_apc_gen_time`
- `apc_gen_time` per autoprecompile
- `num_calls` per autoprecompile
We used the default tuple range checker sizes, but it should be read
from the config. For example, in the reth benchmarks, the sizes are
actually different, leading to potential soundness or completeness bugs.
Currently we get a file not found error for input of
`effectiveness_plot.py`, because the `cargo prove` with no APC case
doesn't generate `apc_candidates.json` as input for the Python script
anymore after #3109.
This PR fixes this error and now `run_guest_benches.sh` runs on the
server, though I'm not sure if all nightly tests will be fixed that
aren't run on CI yet.
Two reasons for this:
- When making changes to the optimizer, the diffs in the snapshots show
immediately which columns got removed
- When looking for more optimizations, it's also useful to go through
each column and ask "Why do we need this column?"
When the input is non-square, the prover returns the square root of the
input times a predefined non-quadratic residue.
The idea is that the guest should also prove the non-square case, so it
must check that:
`result * result == input * PREDEFINED_NON_QR`.
Chose `3` as the predefined non_qr.
