Currently just the bus.asm call is created. Next step will be editing
`bus.rs` linker to do this call for backends that needs the native bus
interaction.
A key quesiton remains whether we need to import the backend crate or
create another linker mode in the linker crate in order to distinguish
which cases to pass down the native bus interaction vs which cases to
call `bus_multi_linker`.
A third solution is to make both `bus_multi_linker` and
`bus_native_linker` call in `bus.rs`, and this will create both
`BusInteraction` and `PhantomBusInteraction` for all backends, and some
backends can just ignore the native `BusInteraction`, similar to what
we've done for native lookup and permutation.
Ready for review. Depends on #2479 merged, which is currently in a chain
of 3 PRs that need merging.
Inspired by Chris' comment here:
https://github.com/powdr-labs/powdr/pull/2465#discussion_r1954166247
This PR will remove anything in the like of
`bus_send(BusInteraction::Send(...))`, because the "send" is duplicated
information. Instead, it will just be `bus` or `bus_multi` that handles
both the send and the receive cases.
Linker and tests that depend on these APIs are also updated.
Solves #2470. Depends on #2465. Approval will only works after merging
#2465.
The following is a response to #2470 and motivation of this PR:
Chance of collission:
For 24-bits:
100 interactions: 0.000295000053831429
1000 interactions: 0.02933425835911685
10000 interactions: 0.9492338975723106
For 30-bits (theoretically the largest we could get to without changing
pil code due to field prime of bb and m31):
100 interactions: 4.610036260510597e-06
1000 interactions: 0.0004650875835883195
10000 interactions: 0.04549425469529611
Neither look ideal, but I think after
https://github.com/powdr-labs/powdr/pull/2469, bus linker mode should
always have 2 bus interactions only. For user defined bus interactions,
they can intentionally input IDs that don't clash, so I think just using
30-bit interaction id should be good enough for 29 bits of security
(under 2 interactions linker case).
Ready for review. Solves #2460. Depends on #2469. Prior bug fixed (due
to an error in the `bus.asm` code update when unwrapping the new
`BusInteraction` enum type.
Ready for review. Depends on #2468. Implements bullet point number 2
mentioned in #2468.
The biggest challenge would be adding the multiplicity columns and an
additional constraint `(1 - selector) * multiplicity = 0` for the lookup
case, and this can be achieve by two methods:
1. Adding the array of column and array of constraints at the linker
level.
2. Create another PIL function that batch permutation receives and
lookup receives to the same bus multi interaction.
I'm opting for method 2 because method 1 likely requires lots of
processing of numerous lower level ast `Expression` types, which would
likely look a lot messier than method 2.
---------
Co-authored-by: schaeff <thibaut@powdrlabs.com>
Ready for review. Depends on #2459, which depends on #2457.
1. Added `lookup_multi_receive` and `permutation_multi_receive` APIs for
the linker and test files to use.
2. Modified linker to use the multi version by default. This in practice
reduces the number of bus interactions to 2 or 3 (depending if we only
have permutation, only have lookup, or have both). This can be furthur
optimized by directly using `bus_multi_receive` function in the linker,
but requires more processing of lower level expressions, which I'd leave
to another PR. In practice, this would reduce the number of bus
interactions from 2 or 3 to always 2. This is currently being
implemented in #2469.
3. Added test cases to the pipeline.
- separate the native and bus linker as two implementations of a
`LinkerBackend` trait
- refactor the object data structures to simplify linker implementation
- change the bus linker to use the bus directly and use a single receive
per operation, with the `interaction_id` being hash based
- pull the permutation selector array treatment into the linker, since
it should be linker specific (per link for native, per operation for
bus)
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
Co-authored-by: chriseth <chris@ethereum.org>
Co-authored-by: Leo <leo@powdrlabs.com>
Depends on #2360
Changes the semantics of the `PhantomBusInteraction.latch` field
slightly, to make my life easier with #2351. Basically, we want it to be
exactly what the RHS selector would have been in a lookup / permutation:
A fixed column latch for a lookup, and equal to the multiplicity for the
permutation. This way, witgen can treat it just like it treats selectors
now.
Eventually, I think we should remove the latch again. The permutation
latch is equal to the multiplicity anyway, and the lookup latch should
be detectable by looking for a constraint like `(1 - latch) *
multiplicity = 0;`.
We need this for witness generation.
This propagates to `bus_interaction`, `bus_receive`, `lookup_receive`
and `permutation_receive` also taking a latch.
This PR uses `LinkerMode::Bus` in all tests which:
- Are on Goldilocks or BN254 (the bus is not implemented for smaller
fields), AND
- Are tested with the mock prover or Plonky3 (while Halo2 does support
the bus in principle, its runtime is exponential, because it inlines
intermediate polynomials)
This is true for most tests.
Doing so, I came across a few bugs. I added comments for them below.
- Replace the rule which sets all degrees to that of main if it is
static and use a CLI flag instead: `--degrees-mode`
- Adjust tests to run mostly on vadcop
- Tweak tests to reduce wasted rows
Refactor of the linker to enable creating statements both in the source
and in the target of a link. Instead of creating a vector of statements,
we create a (name=>namespace) map.
The linker mode is exposed in the CLI, and currently defaults to the
native lookup/permutation statements.
Bus linking can be activated the following way:
```console
cargo run pil test_data/asm/vm_to_block_unique_interface.asm --force --linker-mode bus
```
TODO:
- [x] absolute names
This PR does a few things:
- unify `Input/DataIdentifier` into a single `Input` query that takes
(channel,idx) and returns a field element
- Output query takes (channel, fe)
- change the related prover functions to reflect this
This interface is used by, but not the same, as the input/output for the
riscv machine.
How to use these to input/output bytes or serialized data is a job of
the runtime implementation.
We currently hardcode the range of degrees that variable degree machines
are preprocessed for. Expose that in machines instead.
This changes pil namespaces to accept a min and max degree:
```
namespace main(123..456);
namespace main(5); // allowed for backward compatibility, translates to `5..5`
```
It adds two new builtins:
```
std::prover::min_degree
std::prover::max_degree
```
And sets the behavior of the `std::prover::degree` builtin to only
succeed if `min_degree` and `max_degree` are equal.
This PR fixes issue #1728.
1) Removes the blank space that was printed even if the body of the
blocks was empty.
2) Adds the Precedence trait to LambdaExpressions to correctly handle
the use of parentheses.
When creating the ROM machine, give it a degree:
- if the VM has a degree, pass the same degree to its ROM machine (this
is required to support the monolithic case where all degrees must match)
- otherwise, pass the length of the ROM
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
What we can have after this PR:
- only dynamic namespaces
- dynamic main, others dynamic or static
What we still cannot have:
- static main and another machines dynamic
The change to `_linker_first_step` can be reverted after #1565
The previous version of link_merging.asm is not working correctly since
the `operation sub<1>` implementation is wrong. With this PR, `operation
sub<1>` implementation is fixed.
This PR continues the task to replace lookups by links. The advantages
of this approach are:
- with a link, the two machines can have different degrees and be proven
separately
- with a lookup, only a monolithic proof works
- some backends such as Plonky3 do not support lookups
- this is backwards compatible, since in the monolithic setting, links
are turned into lookups
In the compiler, we currently reduce each machine to another machine
which has only pil code and links. To this end, in the case of virtual
machines, we encode the program in fixed columns. This change introduces
a separate machine to store the ROM. Therefore, each VM gets turned into
not one, but two machines:
```
machine MyVM {
}
```
becomes
```
machine MyVM {
MyVMROM _rom;
}
machine MyVMROM {
}
```
We introduce a new name alongside the original name, which pollutes the
module. When raised, it was decided that we should not currently allow
defining the ROM machine *inside* the VM.
A better long term solution would be to have a generic `ROM` machine in
the stdlib which can be instantiated with the fixed columns which encode
the program, using them in the `get_line` operation. There are a few
missing pieces in the asm language to enable that.
Before: all machines must have the same degree, no degree gets replaced
with the main degree
After: machines can have different degrees, no degree gets replaced with
the main degree
We'll probably need another change to support dynamic degree but this
should be enough for machines of different, static, degree.
Merge compatible `link`s into a single permutation/lookup.
We only consider merging links from different instructions, as a single
instruction can be active at a time.
Links with next references are ignored due to a limitation in witgen
(left a TODO so its easily fixed upon witgen support)
This PR builds on top of #1393.
It mainly modifies the grammar by changing the way SelectedExpressions
are declared, to allow blocks to be empty.
---------
Co-authored-by: chriseth <chris@ethereum.org>
Allow VM instructions to use the `link` notation, unifying the way
machines are linked from VMs and block machines.
Previous syntax for "external instructions" not allowed anymore, and
should use the new `link` syntax.
This PR is part of issue https://github.com/powdr-labs/powdr/pull/1345.
In particular, it adds the struct Number to Expressions to homogenize
the structure before including source references.
Adds binary operation precedence support to avoid unnecessary
parentheses in expression printed format
- #962
---------
Co-authored-by: chriseth <chris@ethereum.org>
