Finalize bus related tasks (afaik)

[qwang98]

There will be three tasks left TODO, with the second depending on the first and the third on the second.

First Task: one bus interaction per object/machine (DONE in #2486)

In bus linker, instead of using two sets of accumulator columns per object/machine, i.e. one for all bus sends (BusInteraction::Send inputs via bus_multi) and one for all bus receives (both lookup and permutation via bus_multi_receive_batch_lookup_permutation), we can batch all bus interactions. This will require adding another function bus_multi_linker: (id, selector, payload[], type)[] (note that this is not correct syntax just illustrative) where type has three potential values: 0 if it's a bus send, 1 if it's a bus receive for lookup, and 2 if it's a bus receive for permutation. This function will only be used by the linker and user should not tamper with it. This function will replace bus_multi and bus_multi_receive_batch_lookup_permutation as the sole function to be used in the linker.

Second Task: one bus interaction for all objects (SEE A POC IN #2487)

Completing the first task yields results like this:

namespace main(8);
    ...
    std::protocols::bus::bus_multi_linker([(454118344, 1, [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return], 0)]);
namespace main__rom(4);
    ...
    std::protocols::bus::bus_multi_linker([(454118344, main__rom::latch, [main__rom::operation_id, main__rom::p_line, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return], 1)]);

Because all columns names are absolute paths (except main), I'm hypothesizing that we can just have one bus interaction pil statement inside main that references all bus send and receives from all machines. Is this actually possible? @Schaeff. Doing this will require changing up the LinkerBackend trait (https://github.com/powdr-labs/powdr/blob/main/linker/src/lib.rs#L29-L60), because currently bus interaction statement is added within process_object, and we would need an extra statement within function link that inserts the single bus interaction statement after processing objects, which obviously doesn't apply to the native linking mode.

The end result will look like:

namespace main(8);
    ...
    std::protocols::bus::bus_multi_linker([
(454118344, 1, [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return], 0)
(454118344, main__rom::latch, [main__rom::operation_id, main__rom::p_line, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return], 1)
]);
namespace main__rom(4);
    ...

Third Task

Now that the second task is done, we need to constrain the accumulator to be zero. I remember seeing somewhere in the code base or a PR or an issue that we should expose the accumulator columns in the publics (honestly I have no idea what this means), and this might involve editing the backend, so would appreciate some thoughts from @Schaeff. Basically would you mind providing me some data structure/file to look at, so I can get some more grounded sense of the pipeline? Thanks! :)

[georgwiese]

First Task: one bus interaction per object/machine

Very cool :)

Because all columns names are absolute paths (except main), I'm hypothesizing that we can just have one bus interaction pil statement inside main that references all bus send and receives from all machines.

I'm not sure how this would work! Maybe there is some misunderstanding.

Different machines have different number of rows, so they cannot interact directly using polynomial constraints. For example, the std::machines::range::Byte machine has 256 rows, but a machine using it might have many more, so they wouldn't be able to share the accumulator column, right? I think one accumulator per machine is the best we can do.

In essence, each machine has its own trace matrix (of different heights) and is proven independently (*). Each machine has its own "local" bus accumulator and the final value (just a single extension field element) is exposed as a public. So then, the verifier verifies all proofs individually, sums up the local bus accumulators (there is only one per machine, so this is not too much work), and asserts that the sum is zero.

Third Task

We currently support exposing specific cells of the trace as publics, this is an example. I'm not sure what the support is for adding publics in PIL functions currently.

So I think this task has two components: Exposing the final accumulator values (I think it's tricky because we don't know the number of rows at compile time?) and adding the verifier logic to add the check that they actually sum to 0.

I think this task is has much less priority that the previous one, because while it is essential for soundness, I wouldn't expect this step to introduce significant overhead (as opposed to the bus accumulators). So, we can iterate on the design and get realistic performance estimates without implementing this task. I think we'll also want to change some things around publics (#1633), so it might make sense to do that first.

(*): This is simplifying a bit; the backend might be able to share some work between these proofs, but there is no constraint between machines from the PoV of the proving backend. Our "composite" backend literary produces an independent proof per machine; but Plonky3 for example does this in a more integrated and efficient way.

[qwang98]

Thanks for the write up! I think from your answer I would push the first task towards the end, and then maybe work on the publics stuff you quoted. I'll postpone adding accumulator to publics. After that I'd do some random PR reviews, unless you think there are some other stuffs to be done on the bus front.