-
Notifications
You must be signed in to change notification settings - Fork 100
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Batch arbitrary number of bus interactions #2449
base: main
Are you sure you want to change the base?
Conversation
// Assumed to be direct column references. | ||
pub helper_columns: Option<Vec<AlgebraicReference>>, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is an Option
because in the case of odd number of bus interactions, there will be no helper columns.
This is Vec<AlgebraicReference>
instead of ExpressionList
, because I assume that all helper_columns will be direct references, similar to accumulator_columns. I'm not entirely sure about your early explanation why folded_expressions are not Vec<AlgebraicReference>
. Is it because they might be materialized and thus indirect reference?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is because they might not be materializes! Then it would be an expression like beta * x1 + x
(or similar). Then it is ignored (because witgen does not need to do anything). I guess we could also turn it into an Option<Vec<AlgebraicReference>>
, because we don't really need the expression in the non-materialized case...
let (folded, helper, acc) = self.interaction_columns(bus_interaction); | ||
collect_folded_columns(bus_interaction, folded) | ||
.chain(collect_helper_columns(bus_interaction, helper)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
WItgen for helper columns follow a similar idea of map reduce. Mapping by the same PolyID and reducing by aggregating the value calculated for a specific bus interaction. Because helper column are always shared by two bus interactions, this is basically calculating multiplicity / payload
for each bus interaction and then summing up the two parts.
let helper = folded.inverse() * multiplicity; | ||
|
||
let new_acc = match multiplicity.is_zero() { | ||
true => current_acc, | ||
false => current_acc + folded.inverse() * multiplicity, | ||
false => current_acc + helper, | ||
}; | ||
|
||
folded_list[i] = folded; | ||
helper_list[i] = helper; | ||
acc_list[i] = new_acc; | ||
} | ||
|
||
// Transpose from row-major to column-major & flatten. | ||
let mut folded = vec![Vec::with_capacity(size); Ext::size()]; | ||
let mut helper = vec![Vec::with_capacity(size); Ext::size()]; | ||
let mut acc = vec![Vec::with_capacity(size); Ext::size()]; | ||
for row_index in 0..size { | ||
for (col_index, x) in folded_list[row_index].to_vec().into_iter().enumerate() { | ||
folded[col_index].push(x); | ||
} | ||
for (col_index, x) in helper_list[row_index].to_vec().into_iter().enumerate() { | ||
helper[col_index].push(x); | ||
} | ||
for (col_index, x) in acc_list[row_index].to_vec().into_iter().enumerate() { | ||
acc[col_index].push(x); | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This part will need to updated to account for the odd/even cases but I haven't gotten here yet.
/// the accumulator columns, so that constraints are always bounded to | ||
/// degree 3. Each set of helper columns is always shared by two bus | ||
/// interactions. | ||
PhantomBusInteraction(expr, expr, expr[], expr, expr[], expr[], Option<expr[]>) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The biggest road block so far is that I get a type error from this line. I think it's this line because it's the only place I reference Option<expr[]>
. Not really sure how to debug:
thread 'main' panicked at /Users/steve/Documents/repo/powdr-8_7_24/powdr/backend-utils/src/lib.rs:323:52:
called `Result::unwrap()` on an `Err` value: [Error { source_ref: :6461-6491, message: "Expected type: std::prelude::Option<expr[]>\nInferred type: expr[]\nCannot unify types expr[] and std::prelude::Option<expr[]>" }]
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How do I reproduce the error? When I run the tests, witgen fails in a lot of them but not due to a type error?
On how to debug, the source_ref: :6461-6491
should be helpful. These refer to character positions in some source file I think. It sounds like you're passing expr[]
somewhere, though it's not obvious to me where.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This :)
cargo run pil test_data/asm/static_bus_multi_2.asm --force --linker-mode bus --prove-with mock --field gl
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, I think my setup was broken before, that's why many tests were failing.
This looks like it is related to the print function! If you look at ./static_bus_multi_2_opt.pil
, you find lines like this:
Constr::PhantomBusInteraction(-main::add_sel, 123, [main::add_a, main::add_b, main::add_c], main::add_sel, [main::folded, main::folded_1], [main::acc, main::acc_1], [main::helper, main::helper_1]);
What's curious is that this is after witgen runs through, so it looks like a bug in how the PIL is persisted to the file system. This file seems to be read again and parsed, which then gives you the error.
@@ -49,7 +63,12 @@ let materialize_folded: -> bool = || match known_field() { | |||
/// - payload: An array of expressions to be sent to the bus | |||
/// - multiplicity: The multiplicity which shows how many times a column will be sent | |||
/// - latch: a binary expression which indicates where the multiplicity can be non-zero. | |||
let bus_interaction: expr, expr[], expr, expr -> () = constr |id, payload, multiplicity, latch| { | |||
let bus_multi_interaction_2: expr[], expr[][], expr[], expr[] -> () = constr |ids, payloads, multiplicities, latches| { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a pretty ugly interface and will be transposed to (expr, expr[], expr, expr)[]
later or simply add another function that takes (expr, expr[], expr, expr)[]
and wraps this function.
|
||
let m_ext = from_base(multiplicity); | ||
let m_ext_next = next_ext(m_ext); | ||
let m_ext_arr = array::map(multiplicities, |multiplicity| from_base(multiplicity)); // Ext<expr>[] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Another major road block:
If the main function takes an bus_inputs: (expr, expr[], expr, expr)[]
, this will look like:
array::map(bus_inputs, |bus_input| from_base(bus_input.2));
But apparently we don't have tuple indexing, so would have to transpose all the arguments from bus_inputs: (expr, expr[], expr, expr)[]
to multiplicities
here, for which I still don't have a good solution:
let multiplicities: expr[] = array::map(bus_inputs, |bus_input| {
let (_, _, multiplicity, _) = bus_input;
multiplicity
});
I'm afraid that this will materialize all the multiplicity columns twice (once as input arguments and once in the destructuring).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And we need to do this for some/all of id, payload, and latch as well.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure I understand the problem. What do you mean by "materialize all the multiplicity columns twice"? I think your solution to transpose would work fine.
I'd expect the bus_inputs
to be mapped once to get the folded payload, multiplicities and latches, and then the result can be transposed to do some batching.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I meant multiplicity is already a part of the input argument and then another let
clause defines it within this example I commented above, but I think according to Chris and as you also just commented, I think this transposition should be fine, though not the best looking for sure ;)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We could add a general transpose(matrix: T[][]) -> T[][]
function to the PIL std lib. Though I think converting the tuples to list would still look similarly ugly. AFAIK that can't be done generically, but you could add a matrix_from_4_tuple_list(tuple_list: (T, T, T, T)[]) -> T[][]
(or whatever number of elements you need). Beyond that, I'm out of ideas :D
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One more complication is that the 4 tuple list are (expr, expr[], expr, expr), so technically need two generic arguments, and therefore probably won't be good for the stdlib as much. I think the matrix transposition function could be useful though, and I can do it in another PR.
array::new( | ||
input_len, | ||
|i| if input_len % 2 == 1 && i == input_len - 1 { | ||
Constr::PhantomBusInteraction( | ||
multiplicities[i], | ||
ids[i], | ||
payloads[i], | ||
latches[i], | ||
unpack_ext_array(folded_arr[i]), | ||
acc, | ||
Option::None | ||
) | ||
} else { | ||
Constr::PhantomBusInteraction( | ||
multiplicities[i], | ||
ids[i], | ||
payloads[i], | ||
latches[i], | ||
unpack_ext_array(folded_arr[i]), | ||
acc, | ||
Option::Some(helper_arr[i / 2]) | ||
) | ||
} | ||
); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this is where the unable to unify type error happens, the Option::None / Option::Some returned here is somehow parsed as expr[]
while an Option<expr[]>
is expected. Not sure how to debug.
bus_multi_receive_2( | ||
[ADD_BUS_ID, MUL_BUS_ID, SUB_BUS_ID, DOUBLE_BUS_ID], | ||
[[add_a, add_b, add_c], [mul_a, mul_b, mul_c], [sub_a, sub_b, sub_c], [double_a, double_b, double_c]], | ||
[add_sel, mul_sel, sub_sel, double_sel], | ||
[add_sel, mul_sel, sub_sel, double_sel] | ||
); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For this entire test file, a follow up PR is to create more complicated test cases, maybe reusing the same columns for different payloads and send/receives.
I think you're on the right track! It would be good to break this up a bit. For example, adding the helper columns to the annotation could be a standalone PR (just setting them to |
Sounds good :) Thanks for the review. |
@@ -431,7 +431,7 @@ impl<T: Display> Display for PhantomBusInteractionIdentity<T> { | |||
fn fmt(&self, f: &mut Formatter<'_>) -> Result { | |||
write!( | |||
f, | |||
"Constr::PhantomBusInteraction({}, {}, [{}], {}, [{}], [{}]);", | |||
"Constr::PhantomBusInteraction({}, {}, [{}], {}, [{}], [{}], [{}]);", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, this is wrong I think, this would just print the list (without Option::Some(...)
or [None]
).
WIP. Not ready for a final review, but would still like some preliminary comments on whether I'm on the right track. Currently passes test in
bus_static_multi_2.asm
with four bus interactions, up to commit hash 96747e0 (the second to last commit). The lastest commit adds partial support for odd number of bus interactions, but gets a unable to unify type error (explained below) I'm not sure why.This PR will probably be broken into two:
Currently it's just one PR for the sake of easy review.