Witgen: Use bus natively #2361

georgwiese · 2025-01-19T00:39:32Z

Depends on #2371

This PR introduces a new Identity, which is similar to powdr_ast::analyzed::Identity, but it only has "bus send" and "bus receive" variants, instead of (phantom) lookup / permutation / bus interaction. Any lookup or permutation gets translated to an equivalent pair of bus interactions. This abstracts how the machine connection is implemented exactly.

Right now, we assume that each bus send and receive has a compile-time interaction ID, by which they can be statically matched. This is always the case if the interaction originated from a lookup or permutation, so this is fully backward-compatible.

But what this already gives us is many-to-one relationships: We can have several sends with the same interaction ID, that map to the same receive. As a result, we can drastically remove the number of receives, as Thibaut is doing in #2359.

As a next step, we can also make the send interaction ID dynamic, which allows for a reduction of sends. For that, we need to relax the assumption that the interaction ID is known at compile time and match while solving the constraint system.

Benchmark results

executor-benchmark/keccak
                        time:   [11.928 s 12.248 s 12.611 s]
                        change: [-5.4383% -2.0982% +1.2884%] (p = 0.26 > 0.05)
                        No change in performance detected.

georgwiese · 2025-01-19T01:16:38Z

Current state:
witgen::global_constraints::test::constraints_propagation_phantom_lookups is failing because range constraint multiplicities are wrong, but they are remove in #2356. This error could actually propagate and lead to some multiplicities not generated. So it makes sense to rebase after #2356 is merged and then see what's still failing.

executor/src/lib.rs

georgwiese · 2025-01-22T00:52:50Z

executor/src/witgen/machines/mod.rs

+                let receive = send
+                    .try_match_static(bus_receives)
+                    .expect("No matching receive!");
+                let multiplicity_column = if receive.is_unconstrained() {


This multiplicity column is only referenced rarely and I think can be removed in a follow-up PR. For now, I try to preserve the old behavior to minimize code changes.

georgwiese · 2025-01-22T01:03:06Z

test_data/asm/block_to_block_with_bus.asm

-    bus_receive(ARITH_INTERACTION_ID, [0, x, y, z], latch * used, latch);
+    col witness bus_selector;
+    std::utils::force_bool(bus_selector);
+    bus_receive(ARITH_INTERACTION_ID, [0, x, y, z], latch * bus_selector, latch * bus_selector);


This is an interesting one. In this test, we use a normal link and a bus interaction in parallel. Bus interactions used to be ignored, but now we actually do each call twice. That's fine, but then we need a new selector, because otherwise it makes the permutation argument invalid.

georgwiese · 2025-01-22T01:03:54Z

test_data/asm/block_to_block_with_bus_different_sizes.asm

-    // Witgen will choose the degree 8.
-    min_degree: 4,
-    max_degree: 8,
+    // Witgen will choose the degree 4.


Because each call happens twice (see above), I made the main machine smaller, so the submachine is still big enough.

github-actions

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: `adaee1f`	Previous: `dcf7ad9`	Ratio
`evaluator-benchmark/std::math::ff::inverse`	`8367` ns/iter (`± 5`)	`6891` ns/iter (`± 7`)	`1.21`
`evaluator-benchmark/std::math::ff::mul`	`1399` ns/iter (`± 1`)	`1091` ns/iter (`± 2`)	`1.28`
`evaluator-benchmark/sqrt_879882356`	`37171` ns/iter (`± 25`)	`29796` ns/iter (`± 29`)	`1.25`
`evaluator-benchmark/sqrt_1882356`	`31062` ns/iter (`± 18`)	`25014` ns/iter (`± 20`)	`1.24`
`evaluator-benchmark/sqrt_1187956`	`31010` ns/iter (`± 17`)	`24875` ns/iter (`± 22`)	`1.25`
`evaluator-benchmark/sqrt_56`	`21719` ns/iter (`± 14`)	`17577` ns/iter (`± 14`)	`1.24`
`evaluator-benchmark/sort_33`	`957278` ns/iter (`± 2595`)	`786193` ns/iter (`± 864`)	`1.22`
`evaluator-benchmark/sort_100`	`3291219` ns/iter (`± 3341`)	`2727854` ns/iter (`± 5186`)	`1.21`
`evaluator-benchmark/sort_300`	`11502917` ns/iter (`± 20460`)	`9522945` ns/iter (`± 34285`)	`1.21`

This comment was automatically generated by workflow using github-action-benchmark.

This is something I came across in #2361: The `FixedLookupMachine` does not recognize lookups of the form `[...] in [col1, col2, 3, col4]`. The reason that this was not an issue before is that the PIL optimizer simplifies such lookups. But it does not if they are represented as bus interactions. With this PR, the `FixedLookupMachine` looks for either fixed columns or compile-time constants on the RHS.

Co-authored-by: chriseth <[email protected]>

qwang98 · 2025-01-24T04:05:40Z

executor/src/witgen/data_structures/identity.rs

+    /// binary value. If it is zero, the multiplicity must be zero as well.
+    /// For example, it could also be a binary fixed column, indicating
+    /// where the multiplicity can be non-zero.
+    pub selected_tuple: SelectedExpressions<T>,


bus.asm line I'm referring to: https://github.com/powdr-labs/powdr/blob/main/std/protocols/bus.asm#L32

Does selected_tuple.expression contain id and tuple from bus.asm and selected_tuple.selector contain latch from bus.asm?

Yes, except the ID is separate, see convert_phantom_bus_interaction. I'm pretty sure this will change in the future, for now, this is designed to be close to the lookups / permutations we're working with before, to keep the code changes reasonable.

qwang98 · 2025-01-24T04:06:01Z

executor/src/witgen/data_structures/identity.rs

+    /// committed.
+    /// Note that this is the absolute multiplicity, i.e., the negation has
+    /// been removed.
+    pub multiplicity: Option<AlgebraicExpression<T>>,


bus.asm line I'm referring to: https://github.com/powdr-labs/powdr/blob/main/std/protocols/bus.asm#L32

Does multiplicity contain multiplicity from bus.asm?

Yes, if this came from a phantom bus interaction.

qwang98 · 2025-01-24T04:08:34Z

executor/src/witgen/data_structures/identity.rs

+use powdr_number::FieldElement;
+
+#[derive(Clone, Eq, PartialEq, Hash, Debug)]
+pub struct BusSend<T> {


BusSend contains no multiplicity because multiplicity equals selector for sends (basically all binary)?

qwang98 · 2025-01-24T04:35:17Z

executor/src/witgen/data_structures/identity.rs

+    pub fn is_unconstrained(&self) -> bool {
+        // TODO: This always works in practice, but we should properly check the
+        // range constraints on the multiplicity column.
+        self.multiplicity.as_ref() != Some(&self.selected_tuple.selector)
+    }
+}


Relatedly, I wonder why we never constrain that selectors sent to the bus are binary. A couple places where it could be done:
https://github.com/powdr-labs/powdr/blob/main/std/protocols/permutation_via_bus.asm#L18-L25
https://github.com/powdr-labs/powdr/blob/main/std/protocols/lookup_via_bus.asm#L17-L27
latch here: https://github.com/powdr-labs/powdr/blob/main/std/protocols/bus.asm#L132-L135

Does it mean that we assume that selectors are properly constrained already in the main machine and sub machines before they are unpacked for bus interactions?

I guess the analogy is a native lookup / permutation: It also doesn't add any range constraints on its arguments. Arguably it should, but for now we want the PIL functions to be usable as a drop-in replacement for native lookups / permutations, so that we can support both without too many edge cases.

qwang98 · 2025-01-24T04:51:50Z

executor/src/witgen/data_structures/identity.rs

+    right: &SelectedExpressions<T>,
+    rhs_multiplicity: Option<AlgebraicExpression<T>>,
+) -> Vec<Identity<T>> {
+    // +1 because we want to be sure it is non-zero


Very small point but do we want the interaction ID to be non zero because it's fed into the denominator of LogUp? However wouldn't the LogUp equation still ensure proper lookup because we also have linear combination of regular columns in the lookup/permutation?

I think allowing zero would be a soundness bug. The reason is that the way we fingerprint tuples before sending it to the bus is that the fingerprint of $(a, b, c)$ is the same as $(0, 0, 0, 0, a, b, c)$ (you can pad arbitrary numbers of zeros to the left). The ID is the left most element. So it would be ambiguous if it could be zero!

Although, now that I think about it, in this case, the ID is only introduced for witgen and doesn't actually appear in the witness, so maybe I'll just remove that.

Also I think the translation from send/receive to polynomial constraints should do the +1 because that is where this restriction is introduced.

There are no polynomial constraints involved here though, this code translates (phantom or native) lookup / permutation arguments.

I changed the interaction ID to come from the ID counter instead. Also, the counter is initialized with max(max_interaction_id, max_bus_id) + 1 now, so this also solves the problem of potentially colliding IDs if you have bus interactions and lookups / permutations (which happens more often than I thought, e.g. when you have a native lookup but also links, and use --linker-mode bus).

qwang98 · 2025-01-24T05:01:19Z

executor/src/witgen/data_structures/identity.rs

+    // TODO: We should instead analyze the range constraints of the
+    // multiplicity expression.


Why? Just looking at the sign of multiplicity is enough to distinguish between send and receive?

No, see the TODO ;)

As long as you use the std lib and don't create your own phantom bus interactions manually, it should always work though.

Ah, sorry, I misread your comment and thought you meant the opposite.

For example, using -m as multiplicity is recognized correctly as a send, but not -1 * m. Also -(-m) will be recognized as a receive, but is a send ;)

qwang98 · 2025-01-24T05:06:17Z

executor/src/witgen/data_structures/identity.rs

+        true => Identity::BusReceive(BusReceive {
+            id: bus_interaction.id,
+            interaction_id,
+            multiplicity: Some(multiplicity),
+            selected_tuple,
+        }),
+        false => {
+            assert_eq!(multiplicity, bus_interaction.latch);
+            Identity::BusSend(BusSend {
+                id: bus_interaction.id,
+                interaction_id: AlgebraicExpression::Number(interaction_id),
+                selected_tuple,
+            })
+        }


Quite minor but why do we have T for the interaction_id field of the inner BusReceive but AlgebraicExpression<T> for the interaction_id field of the inner BusSend type?

Because we expect that receives have a static one, but receives could be dynamic. For example, you could have a receive with ID (instr_mul + instr_add) * ARITH_ID + instr_keccak * KECCAK_ID.

qwang98 · 2025-01-24T09:00:13Z

std/protocols/lookup_via_bus.asm

-
-    // Add an annotation for witness generation
-    to_phantom_lookup(lookup_constraint, multiplicities);


Why don't we need lookup/permutation annotations anymore? Is it becasue we can match caller and callee via interaction_id? It looks like we also removed references to PhantomBusInteraction in this PR. Does it mean that this line is no longer needed? https://github.com/powdr-labs/powdr/blob/main/std/protocols/bus.asm#L36

Relatedly, will each submachine have the same interaction_id for all sends and receives?

Before this PR, we completely ignored PhantomBusInteractions in witgen, now we take it seriously. See the warning I just removed: 9e8dbef

If we would still yield a phantom lookup, we would say that each call has to execute twice, which disagrees with the constraints.

So, we still need the phantom bus interaction, but we don't also need the phantom lookup / permutation anymore.

chriseth · 2025-01-24T09:51:03Z

executor/src/witgen/machines/machine_extractor.rs

+            // We're only interested in bus receives, and polynomial identities
+            // for sure don't translate to bus receives, so we can filter them out.
+            .filter(|identity| !matches!(identity, AnalyzedIdentity::Polynomial(_)))
+            .flat_map(|identity| convert_identity(&mut dummy_id_counter, identity))


Is there really no better way than re-doing the conversion all over again here just to get the multiplicity columns?

OK, I stored them in the global range constraints. This also removes the need for the machine extractor to know about the analyzed identity!

chriseth · 2025-01-24T09:53:27Z

I'm also not very happy than the code in the machine extractor now has three different abstractions of the same concept: Analyzed::Lookup, Machine::Connection and now BusSend/BusReceive

chriseth · 2025-01-24T09:55:24Z

executor/src/witgen/data_structures/identity.rs

+        selector: bus_interaction.latch.clone(),
+        expressions,
+    };
+    match is_receive {


Doesn't clippy tell you to use if is_receive { ... } else { ... } instead?

chriseth · 2025-01-24T09:56:53Z

executor/src/witgen/global_constraints.rs

@@ -249,14 +254,11 @@ fn propagate_constraints<T: FieldElement>(
                false
            }
        }
-        // Bus receives are handled when they are matched with a send.
+        // Cannot derive a range constraint from a receive.
        Identity::BusReceive(..) => false,
        Identity::BusSend(send) => {
            let receive = send.try_match_static(bus_receives).unwrap();


Why unwrap if it cannot match? Shouldn't we just ignore it in that case?

Sure, but I don't really want to think about the dynamic case in this PR. There are many places were we unwrap now and have to handle it later. But I could change that we don't have try_match_static in the first place, only match_static, which panics. And then I can undo that in the next PR.

chriseth · 2025-01-24T09:57:56Z

executor/src/witgen/global_constraints.rs

-            // In that case, we can remove the lookup, because its only function is to enforce
-            // the range constraint.
-            if receive.selected_tuple.expressions.len() == 1 {
+            // In that case, we can remove the bus interaction pair,


Do we actually remove the full pair? We only remove the send, right? There could be other sends on the same bus.

That is a good point, actually. They are never removed and that is also correct, because the same receive might also handle a conditional range constraint (e.g. if you have [b1] in [BYTES]; cond $ [b2] in [BYTES]). Which means I can also remove the handling of the multiplicity columns of removed receives :)

executor/src/witgen/global_constraints.rs

qwang98 · 2025-01-24T10:08:42Z

test_data/asm/block_to_block_with_bus.asm

-    bus_receive(ARITH_INTERACTION_ID, [0, x, y, z], latch * used, latch);
+    col witness bus_selector;
+    std::utils::force_bool(bus_selector);
+    bus_receive(ARITH_INTERACTION_ID, [0, x, y, z], latch * bus_selector, latch * bus_selector);


Should multiplicity of bus receive be negative here?

No, because bus_receive adds the negation. Basically, if you only use bus_send and bus_receive in PIL, and only deal with Identity::BusSend and Identity::BusReceive, you don't need to know how each is implemented. Probably it would make sense to have a different Constr variant in PIL as well, so this goes away entirely, but that should be the topic of another PR.

chriseth · 2025-01-24T11:04:48Z

executor/src/witgen/identity_processor.rs

-                self.process_lookup_or_permutation(*id, left, rows)
-            }
+            Identity::BusSend(bus_interaction) => self.process_lookup_or_permutation(
+                bus_interaction.id,


I now see that this changes from an identity id to a bus/interaction id. Could you change the names of the parameters?

Also shouldn't it be a T instead of a u64?

oh wait, it's bus_interaction.id instead of bus_interaction.interaction_id.

now interaction_id instead of bus_id ;)

But yeah, in the future, we'll have to to change the machine call interface to receive a run-time bus ID instead of a static identity ID (which currently determines the bus ID uniquely and statically).

georgwiese changed the base branch from make-latch-semantic-clearer to bus-base January 19, 2025 18:57

georgwiese force-pushed the native-bus2 branch 2 times, most recently from 0087d14 to 2b6fe08 Compare January 20, 2025 12:56

georgwiese changed the base branch from bus-base to main January 20, 2025 13:27

georgwiese commented Jan 21, 2025

View reviewed changes

executor/src/lib.rs Show resolved Hide resolved

georgwiese force-pushed the native-bus2 branch 2 times, most recently from e5bbf2b to b2b1f6d Compare January 22, 2025 00:42

georgwiese changed the base branch from main to fixed-lookup-with-constants January 22, 2025 00:42

georgwiese commented Jan 22, 2025

View reviewed changes

georgwiese force-pushed the native-bus2 branch 2 times, most recently from 607673d to adaee1f Compare January 22, 2025 12:27

github-actions bot reviewed Jan 22, 2025

View reviewed changes

georgwiese force-pushed the native-bus2 branch from adaee1f to a1401d1 Compare January 22, 2025 12:57

This was referenced Jan 22, 2025

Fix fixed lookup that contains constants #2371

Merged

Witgen: Use bus natively #2351

Closed

georgwiese changed the title ~~Witgen: Use bus natively (2)~~ Witgen: Use bus natively Jan 22, 2025

georgwiese marked this pull request as ready for review January 22, 2025 13:55

Base automatically changed from fixed-lookup-with-constants to main January 22, 2025 20:23

georgwiese added 8 commits January 22, 2025 20:43

Witgen: Use bus natively

dd418ad

Fix block-to-block with bus

fe46f78

Don't track multiplicities for permutations

00745bc

Fix block_to_block_with_bus again

c7935bf

Fix block_to_block_with_bus_different_size.asm

0c95f15

Fix PC lookup detection

866190d

Fix 2nd stage witgen for composite backend and bn254

bea099c

Clippy

606ca3b

georgwiese and others added 8 commits January 23, 2025 15:16

Apply suggestions from code review

906006e

Co-authored-by: chriseth <[email protected]>

Machine Global constraints feedback

3ccbb66

Clippy

0b7edf1

Relax conditions for range constraint transfer

32f9f07

Avoid converting polynomial identities

903ab49

Review feedback

001c652

Clippy

88dad6a

Review feedback

f0c426b

qwang98 reviewed Jan 24, 2025

View reviewed changes

chriseth reviewed Jan 24, 2025

View reviewed changes

executor/src/witgen/global_constraints.rs Outdated Show resolved Hide resolved

qwang98 reviewed Jan 24, 2025

View reviewed changes

chriseth reviewed Jan 24, 2025

View reviewed changes

georgwiese added 6 commits January 24, 2025 09:24

More review feedback

4b5461f

Store range constraint multiplicities, avoid having to convert again

bb2ce73

Make sure bus IDs won't collide

c05463f

Remove multiplicity column tracking again, receives are never removed

a3ec36d

Rename is_unconstrained -> has_arbitrary_multiplicity

b55d0b2

Remove warning

9e8dbef

		// TODO: We should instead analyze the range constraints of the
		// multiplicity expression.


		// Add an annotation for witness generation
		to_phantom_lookup(lookup_constraint, multiplicities);

Witgen: Use bus natively #2361

Are you sure you want to change the base?

Witgen: Use bus natively #2361

Conversation

georgwiese commented Jan 19, 2025 • edited Loading

Benchmark results

georgwiese commented Jan 19, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

github-actions bot left a comment

Choose a reason for hiding this comment

⚠️ Performance Alert ⚠️

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

qwang98 Jan 24, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chriseth Jan 24, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

qwang98 Jan 24, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chriseth commented Jan 24, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

georgwiese commented Jan 19, 2025 •

edited

Loading

qwang98 Jan 24, 2025 •

edited

Loading

chriseth Jan 24, 2025 •

edited

Loading

qwang98 Jan 24, 2025 •

edited

Loading