Notes for bus in stwo

related to this PR

Test case

cargo install --path ./cli-rs

compile with the correct field

powdr-rs compile riscv/tests/riscv_data/keccak -o output --field bb

cargo run --features stwo pil  output/keccak.asm --linker-mode native  -o output --force --field m31  --prove-with stwo> result.txt

This can give keccak_opt.pil file with lookup identity, it is native lookup, it doesn’t have multiplicity columns

Get multiplicities.

check –linker-mode bus, see if there are PhantomLookupIdentity, bus related identity that has multiplicity

this command first, with m31 field

cargo run --features stwo pil  output/keccak.asm --linker-mode bus  -o output --force --field m31

Yes, the pil file will have a lot of this

 Constr::PhantomBusInteraction(-main_bit12::multiplicity, 835461721, [main_bit12::BIT12], 1, [main_bit12::folded, main_bit12::folded_1, main_bit12::folded_2, main_bit12::folded_3], [main_bit12::acc, main_bit12::acc_1, main_bit12::acc_2, main_bit12::acc_3], Option::None);
namespace main_bit2(4);

as m31 will have a lot of fold, let’s check bn254 field

Thought 1: I can use bus mode, but without using stage 1, then I would commit more columns, but I don’t commit to stage 1 columns

PhantomBusInteractionIdentity looks like

in keccak_opt for bn254 native, there is a lookup:

main::instr_add_wrap $ [0, main::tmp1_h, main::tmp1_l, main::tmp3_h, main::tmp3_l, main::tmp4_h, main::tmp4_l] 
is 
main_add_sub::latch * main_add_sub::sel[1] $ [main_add_sub::operation_id, main_add_sub::A_h, main_add_sub::A_l, main_add_sub::B_h, main_add_sub::B_l, main_add_sub::C_h, main_add_sub::C_l];

it is a permutation

keccak.asm use m31 bus mode, get identity:

Though 2: find multiplicity generation function, any?

Found an easier test case to implement, bus_lookup.asm

use std::protocols::bus::bus;
use std::protocols::bus::BusInteraction;
use std::protocols::lookup_via_bus::lookup_receive;

machine Main with degree: 8 {

    col fixed x = [1, 5, 2, 6, 4, 2, 6, 3];
    col witness y;

    // Pre-compute f(x) = x + 1 for all x in [1, 8]
    col fixed INC_X = [1, 2, 3, 4, 5, 6, 7, 8];
    col fixed INC_Y = [2, 3, 4, 5, 6, 7, 8, 9];

    let LOOKUP_ID = 42;
    bus(BusInteraction::Send(LOOKUP_ID, [x, y], 1));
    lookup_receive(LOOKUP_ID, 1, [INC_X, INC_Y]);
}

for this file, I removed all the stage 1 related witness, only the phantombusinteration left, end up this pil: bus_lookup_opt_without_stage1_constraint:

namespace main(16);
    col fixed x = [1_fe, 5_fe, 2_fe, 6_fe, 4_fe, 2_fe, 6_fe, 3_fe, 1_fe, 5_fe, 2_fe, 6_fe, 4_fe, 2_fe, 6_fe, 3_fe];
    col witness y;
    col fixed INC_X = [1_fe, 2_fe, 3_fe, 4_fe, 5_fe, 6_fe, 7_fe, 8_fe, 9_fe, 10_fe, 11_fe, 12_fe, 13_fe, 14_fe, 15_fe, 16_fe];
    col fixed INC_Y = [2_fe, 3_fe, 4_fe, 5_fe, 6_fe, 7_fe, 8_fe, 9_fe, 10_fe, 11_fe, 12_fe, 13_fe, 14_fe, 15_fe, 16_fe, 17_fe];
    col witness stage(1) folded;
    col witness stage(1) folded_1;
    col witness stage(1) folded_2;
    col witness stage(1) folded_3;
    col witness stage(1) acc;
    col witness stage(1) acc_1;
    col witness stage(1) acc_2;
    col witness stage(1) acc_3;
    Constr::PhantomBusInteraction(1, 42, [main::x, main::y], 1, [main::folded, main::folded_1, main::folded_2, main::folded_3], [main::acc, main::acc_1, main::acc_2, main::acc_3], Option::None);
    col witness multiplicities;
    col witness stage(1) folded_4;
    col witness stage(1) folded_5;
    col witness stage(1) folded_6;
    col witness stage(1) folded_7;
    col witness stage(1) acc_4;
    col witness stage(1) acc_5;
    col witness stage(1) acc_6;
    col witness stage(1) acc_7;
    Constr::PhantomBusInteraction(-main::multiplicities, 42, [main::INC_X, main::INC_Y], 1, [main::folded_4, main::folded_5, main::folded_6, main::folded_7], [main::acc_4, main::acc_5, main::acc_6, main::acc_7], Option::None);

use this command to run successfully.

cargo run --features stwo pil  output/bus_lookup_opt_without_stage1_constraints.pil  -o output --force --field m31  --prove-with stwo> result.txt

now try bus_multi_lookup.asm

Another thought: proving everying thing together and logup by stwo as extra.

write notes in next blog