Started as a small fix but expanded to a complete refactoring of
`PublicDeclaration` and `PublicReference`.
Now public reference work the same way as any reference and the syntax
is without the colon (`:out` -> `out`). `PublicDeclaration` are also put
under definitions in the analyzer. Both public reference and public
declaration use the absolute path, so it's easy to refer from one to the
other now.
This is needed for #2502 to match public reference to public declaration
in the backend. Currently, different namespaces can have public
references with the same name, and it will confuse the backend on which
public reference value to fetch.
Parses query / prover functions of the form
```
query |<i>| std::prover::handle_query(<Y>, <i>, match std::prover::eval(<pc>) {
<value1> => std::prelude::Query::Output(std::convert::int::<fe>(std::prover::eval(<arg1>)), std::prover::eval(<arg2>)),
<value2> => std::prelude::Query::Input(std::convert::int::<fe>(std::prover::eval(<arg1>)), std::convert::int::<fe>(std::prover::eval(<arg2>))),
...
_ => std::prelude::Query::None,
```
i.e. the ones used for "free input" columns.
Also calls the query function from the generated code accordingly.
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
Extracted from #2488, to keep the diff smaller
In #2488, I want to identify a `MachineCallVariable` by a `bus_id: T`
instead of an `identity_id: u64`. As a result, it gets a new `<T>`
parameter, which propagates to `Variable` and quite far into the
codebase. This PR adds it already. The changes here should be quite
mechanic.
The idea behind the "skip" feature was that if we have an update to a
variable coming from solving an identity, this variable causes all
identities that contain the variable to be re-added to the queue. The
identity we currently processed is among those. I thought we do not need
to re-add it because we just processed it, but it turns out that in some
situations, you can derive more information from the same queue item,
for example when a derived range constraint on a variable together with
existing constraints allows you to fully solve the identity.
This improves error reporting because the failing sends are the reason
for the algorithm not finishing. Other non-complete identities are not
important for success.
When adding new fields to `PhantomBusInteraction`, we forgot to update
the `Children` implementation.
- change the definition of `PhantomBusInteraction` to use expressions,
in order for these fields to be visited by the `Children`
implementation. Move the expectation that these fields are simple
references to witgen.
- update the `Children` implementation
cc @qwang98
Identities of the kind
`[ b * clock_0 + c * clock_1 ] in [ byte ];`, which are used in the
arithmetic machine, are currently not process by auto-witjitgen. The
idea is that this results on range constraints for different columns on
different rows.
The mechanism in place previously would only return range constraints in
case a lookup can always be processed, but this is not the case here: We
will never be able to determine a value just from the lookup, the only
information we can get here are range constraints.
TODO:
- [x] it might be that we will never be able to process the lookup (i.e.
emit a call), in that case we should still add the assertion, because
that is what is supposed to be checked. Maybe we should also detect that
it is just a range constraint after all?
Oh I think we will need to make the call in the end, once we know the
value by other means.
Split the `Assignment` struct into two structs and eliminate the
`VariableOrValue` enum.
This simplifies some interfaces or at least makes them more orthogonal.
The QueueItem is turned into a public data structure in turn.
CI fails from my attempt to break this up to several PR, I think it's
probably because materializing the helper column isn't compatible with
our permutation/lookup -> bus witgen infrastructure. #2458, which is
#2457 plus not materializing the helper column in some cases, is passing
all CI. Is it possible to merge this with CI failures which will be
immediately fixed by #2458?
Ready for a final review. Broken up from
https://github.com/powdr-labs/powdr/pull/2449 so that this works end to
end for arbitrary number of columns (both even and odd).
Instead of using and Option for helper columns, which currently bugs
out, this version uses an array and forces the case of odd number of bus
interactions to materialize a helper_last = multiplicity_last /
payloads_last. This has the advantage of passing tests end to end, so we
can debug in another PR.
One curious case is that CI test for block_to_block_with_bus_composite()
failed at the prover stage on the helper column witness constraint
before if I use the bus multi version for it. Maybe some updates on
witness generation for helper is needed (not on the bus accumulator but
on the conversion from non-native permutation/lookup to bus)?
@georgwiese
This change also adds prover functions as a third kind of "queue item".
The biggest change, though, is a refactoring concerning the code that
computes which variables are contained in an identity. The whole
mechanism is changed to handle queue items uniformly.
this PR changes the signature of `Machine::process_plookup` from
```rust
fn process_plookup<'b, Q: QueryCallback<T>>(
&mut self,
mutable_state: &'b MutableState<'a, T, Q>,
identity_id: u64,
caller_rows: &'b RowPair<'b, 'a, T>,
) -> EvalResult<'a, T>;
```
To
```rust
fn process_plookup<'b, Q: QueryCallback<T>>(
&mut self,
mutable_state: &'b MutableState<'a, T, Q>,
identity_id: u64,
parameters: &[AffineExpression<AlgebraicVariable<'a>, T>],
range_constraints: &dyn RangeConstraintSet<AlgebraicVariable<'a>, T>,
) -> EvalResult<'a, T>;
```
Previously, each machine evaluated the parameters themselves, using the
`caller_rows` and the calling bus send, stored in the connection. But in
the future, the calling bus send will not be static, so I moved this to
the caller.
This will enable #2447 and eventually the dynamic bus.
---------
Co-authored-by: chriseth <chris@ethereum.org>
Depends on #2428 and implements the second bullet point from
https://github.com/powdr-labs/powdr/issues/2337#issue-2787875072.
**Test Coverage**
Not sure why CI isn't running but currently `static_bus_multi.asm`
passes test with `cargo run pil test_data/asm/static_bus_multi.asm
--force --linker-mode bus --prove-with mock --field bn254` but NOT if
`--field gl` with all else equal. See bottom for error from `--field
gl`, which are obviously field extension constraints not passing for
`folded` columns.
**Questions**
1. Probably the biggest problem is with the degree-3 bound of Plonky3.
The non batched version already has a degree of 3
(https://github.com/powdr-labs/powdr/blob/main/std/protocols/bus.asm#L86-L89).
Therefore, this batched version has a degree of 4 and therefore doesn't
work with Plonky3. The degree bound issue is also mentioned in #2337.
2. This comment
(https://github.com/powdr-labs/powdr/blob/main/std/protocols/bus.asm#L52-L56)
seems to say that `--field bn254` uses auto witgen and therefore manual
witgen (which I'm trying to test here) isn't working.
3. According to this chunk
(https://github.com/powdr-labs/powdr/blob/main/std/protocols/bus.asm#L60-L69)
Does `--field bn254` correspond to no constraints for line 65 or
whatsoever? With `--field bn254`, it seems that the accumulator adds up
the folded columns but there's no constraint that the folded columns are
correctly calculated from payload, id, and challenges. Am I missing
something? (I think this might also explain why my `--field bn254` test
has no constraint errors for `folded` columns, because they don't
exist?)
4. I checked the following constraint errors against our field extension
APIs and seems that `mul_ext`, `finger_print_inter_with_id`, `add_ext`,
and `constrain_eq_ext` etc. are applied correctly. Any insights on
whether `mock` works with `gl` and/or field extensions to start with? I
still have a last resort of simply hand computing the values from the
error below to see why it's not working with field extension...
```
➜ powdr git:(bus-multi-interaction) ✗ cargo run pil test_data/asm/static_bus_multi.asm --force --linker-mode bus --prove-with mock --field gl
[00:00:05 (ETA: 00:00:00)] ████████████████████ 100% - Starting... Witness generation took 5.538085s
Writing ./commits.bin.
Backend setup for mock...
Setup took 0.0644265s
Generating later-stage witnesses took 0.00s
Machine main has 64 errors
Error: Identity fails on row 0: main::folded_0 = std::prelude::challenge(0, 5) - (123 + (std::prelude::challenge(0, 1) * main::intermediate_fingerprint_0_2 + 11 * std::prelude::challenge(0, 2) * main::intermediate_fingerprint_1_2));
main::intermediate_fingerprint_0_2 = 16683533738167355631
main::intermediate_fingerprint_1_2 = 8619433688316392780
main::folded_0 = 14379784368020248175
std::prelude::challenge(0, 1) = 2206609067086327257
std::prelude::challenge(0, 2) = 11876854719037224982
std::prelude::challenge(0, 5) = 15794382300316794652
Error: Identity fails on row 0: main::folded_0_1 = std::prelude::challenge(0, 6) - (std::prelude::challenge(0, 2) * main::intermediate_fingerprint_0_2 + std::prelude::challenge(0, 1) * main::intermediate_fingerprint_1_2);
main::intermediate_fingerprint_0_2 = 16683533738167355631
main::intermediate_fingerprint_1_2 = 8619433688316392780
main::folded_0_1 = 3590326197943317962
std::prelude::challenge(0, 1) = 2206609067086327257
std::prelude::challenge(0, 2) = 11876854719037224982
std::prelude::challenge(0, 6) = 18147521187885925800
Error: Identity fails on row 0: main::folded_1 = std::prelude::challenge(0, 7) - (456 + (std::prelude::challenge(0, 3) * main::intermediate_fingerprint_0_5 + 11 * std::prelude::challenge(0, 4) * main::intermediate_fingerprint_1_5));
main::intermediate_fingerprint_0_5 = 9393166848595961660
main::intermediate_fingerprint_1_5 = 14353807143801496692
main::folded_1 = 4794846700896775308
std::prelude::challenge(0, 3) = 18270091135093349626
std::prelude::challenge(0, 4) = 6185506036438099345
std::prelude::challenge(0, 7) = 7364705619221056123
Error: Identity fails on row 0: main::folded_1_1 = std::prelude::challenge(0, 8) - (std::prelude::challenge(0, 4) * main::intermediate_fingerprint_0_5 + std::prelude::challenge(0, 3) * main::intermediate_fingerprint_1_5);
main::intermediate_fingerprint_0_5 = 9393166848595961660
main::intermediate_fingerprint_1_5 = 14353807143801496692
main::folded_1_1 = 16858051030421639712
std::prelude::challenge(0, 3) = 18270091135093349626
std::prelude::challenge(0, 4) = 6185506036438099345
std::prelude::challenge(0, 8) = 2404222719611925354
Error: Identity fails on row 0: main::folded_0_2 = std::prelude::challenge(0, 5) - (456 + (std::prelude::challenge(0, 1) * main::intermediate_fingerprint_0_8 + 11 * std::prelude::challenge(0, 2) * main::intermediate_fingerprint_1_8));
main::intermediate_fingerprint_0_8 = 16683533738167355631
main::intermediate_fingerprint_1_8 = 8619433688316392780
main::folded_0_2 = 14379784368020247842
std::prelude::challenge(0, 1) = 2206609067086327257
std::prelude::challenge(0, 2) = 11876854719037224982
std::prelude::challenge(0, 5) = 15794382300316794652
... and 59 more errors
```
Depends on #2426.
With this PR, we use the annotations added in #2412 and #2426 to find
the columns being generated. This allows us to detect when the folded
payload is not persisted as a witness column.
The background is that @Schaeff is working on #2425, which would undo
persisting the folded payloads in some cases, allowing us to spend fewer
witness columns per bus interaction. With this PR, this should be fine:
The column type will change from witness to intermediate, which means
that the bus witgen will not output any folded columns.
It can be tested by changing the `materialize_folded` bool to `false`,
e.g.
[here](e77d3801c1/std/protocols/bus.asm (L48))
and running:
```
cargo run pil test_data/asm/block_to_block.asm \
-o output -f --linker-mode bus --prove-with mock --field gl
```
This used to fail before this PR.
Depends on #2427 (because otherwise a referenced column might be removed
by the optimizer).
This PR is completely analogous to #2412: We add a list of expressions
that evaluate to the folded payload to `PhantomBusInteraction`. This
lets us easily find the referenced columns in the manual bus witgen, see
#2428.
The JIT compiler used for computing fixed column and the new code for
witgen used two different "util" code snippets. Since the field
implementation for the new witgen code is more advanced, it is now moved
to the generic jit compiler and used by both. It also adds some types
that will later be used by prover functions (PilVec, Callable, etc).
Those types were present already in the fixed column jit code.
