Introduce the concept of `size` for range constraint. It provides an
upper bound for the number of values in the rang econstraint and can be
different from the range width.
Renames QuadraticSymbolicExpression to GroupedExpression. The advantage
of doing it his way is also that we can slowly change what is called
`QuadraticSymbolicExpression` afer this PR, namely the one with
SymbolicExpression as RuntimeConstant to GroupedExpression and easily
see which on is generic already and which is not.
This PR refactors `QuadraticSymbolicExpression`: I removed the reference
to
[`SymbolicExpression`](f60e9d9f69/constraint-solver/src/quadratic_symbolic_expression.rs (L70)).
It can represent values that are known at runtime, represented as an
expression. We don't need this in the context of APC: Variables are
either unknown or known at compile time, and therefore can be
represented as a `FieldElement` instead.
The idea is to introduce [this
trait](4989be08f3/constraint-solver/src/runtime_constant.rs (L11)),
which is implemented by `SymbolicExpression` and any `T: FieldElement`.
This way, we can continue to use the solver with
`QuadraticSymbolicExpression<SymbolicExpression<T, V>, V>` (equivalent
to the current `QuadraticSymbolicExpression<T, V>`) in the old JIT
pipeline and use the simpler `QuadraticSymbolicExpression<T, V>` in the
APC pipeline.
---------
Co-authored-by: chriseth <chriseth.github@gmail.com>
Based on commit 1dbe4db
- Split into two crates, lib and cli
- upgrade stwo, marked one stwo test `should_panic` @ShuangWu121
- various clippy and fmt fixes linked to the rust version update
- bring all rust versions to 2025-05-14. CI still installs other
versions for openvm which uses them internally. The stable rust version
we test on is bumped to 1.85
- remove `examples` and related tests, which test the powdr crate on the
previous version of powdr (since it uses another nightly). Happy to
discuss this if it's important @leonardoalt
Replace the mechanism of "variable update" by "substitutions". This has
the benefit that we can substitute a variable also by a more complex
value.
The next step (not this PR) would be to also allow substitution by QSEs,
which we will need if we want to apply equivalences.
Enable support for permutation constraints. The main problem with
permutation constraints is that they need a way to disable constraints
and thus this PR adds a feature to guess values for variables that have
not been assigned yet but are also not relevant in any of the
identities, for example because they are multiplied by a value that is
known to be zero.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
This avoids cloning QueueItems and processes the items in a queue
instead of always looking at the "smallest" activated item first.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
If we detect a bit decomposition pattern like `X + Y * 256 + Z * 65536 =
T`, the witgen inference returns a bit decomposition effect. But if the
value of `T` is a known number, we can actually extract the concrete
values for `X`, `Y` and `Z` at compile-time and continue solving with
this additional information.
With this PR, there is no more `.unwrap()` on `BusSend::static_bus_id()`
(previously `bus_id()`) and `BusSend::try_match_static()`.
Note that this will only generate a machine call when the bus ID is
"known concrete". Getting there might require branching. To relax this
(and require only known, but not concrete), I think we could change
[`Effect::MachineCall`](https://github.com/powdr-labs/powdr/blob/main/executor/src/witgen/jit/effect.rs#L25)
to take a symbolic expression instead of a concrete value, but
[`CanProcessCall::can_process_call_fully()`](d039c7bd81/executor/src/witgen/jit/witgen_inference.rs (L625))
still expects a concrete value, which can't easily be changed, so I
think this is the best we can do.
This implement prover functons for the interpreter except for the
"input/output" prover functions. I would like to merge this already
since the input/output prover functions are mainly used in the main
machine which does not have jit support yet anyway.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
This PR is a step towards passing stage-0 public witgen to the backend.
It focuses on modifying the pipeline to separate witness values from
public values. Additional changes to pass stage-1 public witgen is
needed before public values are fully passed to the backend.
Extracted from #2541
Fixes a bug that the machine parts doesn't include the intermediate
definitions that only appear in one of the receives. An example of this
is the [Arith
large](https://github.com/powdr-labs/powdr/blob/main/std/machines/large_field/arith.asm)
machine, which has intermediates like `x1c` in their list of arguments,
but doesn't refer to the in any constraint.
---------
Co-authored-by: chriseth <chris@ethereum.org>
