Add folded payload columns to PhantomBusInteraction
#2426
Conversation
georgwiese
force-pushed
the
bus-interaction-add-folded
branch
from
6886e5d to
f66f41a
Compare
| @@ -813,7 +817,7 @@ fn to_constraint<T: FieldElement>( | |||
| _ => panic!("Expected reference, got {f:?}"), | |||
| }) | |||
| .collect(), | |||
| _ => panic!("Expected array, got {:?}", fields[2]), | |||
| _ => panic!("Expected array, got {:?}", fields[5]), | |||
There was a problem hiding this comment.
The 2 was wrong before.
georgwiese
force-pushed
the
bus-interaction-add-folded
branch
from
f66f41a to
40ee74e
Compare
| @@ -91,7 +91,7 @@ let bus_interaction: expr, expr[], expr, expr -> () = constr |id, payload, multi | |||
| constrain_eq_ext(update_expr, from_base(0)); | |||
|
|
|||
| // Add phantom bus interaction | |||
| Constr::PhantomBusInteraction(multiplicity, id, payload, latch, acc); | |||
| Constr::PhantomBusInteraction(multiplicity, id, payload, latch, unpack_ext_array(folded), acc); | |||
There was a problem hiding this comment.
Isn't acc also an extension field that needs unpacking as well? Some how all tests passed in #2412 so this might not be required?
There was a problem hiding this comment.
acc is an array, and acc_ext is the extension field version of it. In both cases, it's just a list of expressions. If there was an error here, the PIL type checker would scream, and I think that's what happened before I did this commit haha 40ee74e
ast/src/analyzed/mod.rs
Outdated
| pub folded_expressions: ExpressionList<T>, | ||
| pub accumulator_columns: Vec<AlgebraicReference>, |
There was a problem hiding this comment.
This is very likely intended but why do we have reference for accumulator columns but expression (or list thereof) for everything else?
There was a problem hiding this comment.
Ok I might be answering myself here, but is it because folded_expressions can be either an expression (if materialized in case of BN254) or an Ext (in case of other fields), BUT accumulator_columns are always Ext?
Does is mean that Ext is converted to AlgebraicReference instead of expression in PIL analysis stage?
There was a problem hiding this comment.
Yeah, I added a comment to explain this a bit. For accumulator columns we expect direct column references, not any generic expression.
| /// Note that this could refer to witness columns, intermediate columns, or | ||
| /// in-lined expressions. |
There was a problem hiding this comment.
Wdym here? Are you referring to this chunk: https://github.com/powdr-labs/powdr/blob/main/std/protocols/bus.asm#L42-L71
So basically folded will be in-lined expression for BN254 but materialized witness/intermediate columns otherwise? What determines whether it'll be a witness or intermediate column?
There was a problem hiding this comment.
Exactly! In practice, it would currently be in-lined or a direct reference to a witness column. But Thibaut is working on an optimizer step that turns witness columns into intermediates (#2425) in some cases (to save commitment cost), then we would have the intermediate column case.
For context, intermediate columns and in-lined expressions are very similar: intermediates are just in-lined later, and with some caching, because in some cases inlining them at compile time would yield exponentially large expressions!
There was a problem hiding this comment.
Where are the inline and intermediate types defined (for example there's an intermediate_columns type in the Analyzed object but am not sure if it's the first time it appears in a Rust object)? Sounds like inlined expressions are expanded at compile time?
In our PIL std lib, we have an `Ext` that abstracts over `Fp2` and `Fp4`. But in cases where we don't need any extension field (e.g. BN254), we wrapped base field elements as `Fp2` anyway. This is a bit weird and can lead to issues when the optimizer removes the unused dimension (e.g., it might still be referenced by a prover function or witgen annotation). I had this problem in #2426. Now, there is an `Ext<T>::Fp` variant that simply wraps `T`.
georgwiese
force-pushed
the
bus-interaction-add-folded
branch
from
cb0ebfb to
5e0443f
Compare
|
Need another approval pls, I rebased against main after #2427 was merged :) |
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](https://github.com/powdr-labs/powdr/blob/e77d3801c1decff039fd0ec6bbeb55ed734357fb/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.