Skip to content

Commit fd973e9

Browse files
authored
Bus multi interaction (arbitrary number of columns) (#2457)
CI fails from my attempt to break this up to several PR, I think it's probably because materializing the helper column isn't compatible with our permutation/lookup -> bus witgen infrastructure. #2458, which is #2457 plus not materializing the helper column in some cases, is passing all CI. Is it possible to merge this with CI failures which will be immediately fixed by #2458? Ready for a final review. Broken up from #2449 so that this works end to end for arbitrary number of columns (both even and odd). Instead of using and Option for helper columns, which currently bugs out, this version uses an array and forces the case of odd number of bus interactions to materialize a helper_last = multiplicity_last / payloads_last. This has the advantage of passing tests end to end, so we can debug in another PR. One curious case is that CI test for block_to_block_with_bus_composite() failed at the prover stage on the helper column witness constraint before if I use the bus multi version for it. Maybe some updates on witness generation for helper is needed (not on the bus accumulator but on the conversion from non-native permutation/lookup to bus)? @georgwiese
1 parent c5202a9 commit fd973e9

File tree

8 files changed

+396
-135
lines changed

8 files changed

+396
-135
lines changed

ast/src/analyzed/display.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -431,7 +431,7 @@ impl<T: Display> Display for PhantomBusInteractionIdentity<T> {
431431
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
432432
write!(
433433
f,
434-
"Constr::PhantomBusInteraction({}, {}, [{}], {}, [{}], [{}]);",
434+
"Constr::PhantomBusInteraction({}, {}, [{}], {}, [{}], [{}], {});",
435435
self.multiplicity,
436436
self.bus_id,
437437
self.payload.0.iter().map(ToString::to_string).format(", "),
@@ -445,6 +445,13 @@ impl<T: Display> Display for PhantomBusInteractionIdentity<T> {
445445
.iter()
446446
.map(ToString::to_string)
447447
.format(", "),
448+
match &self.helper_columns {
449+
Some(helper_columns) => format!(
450+
"Option::Some([{}])",
451+
helper_columns.iter().map(ToString::to_string).format(", ")
452+
),
453+
None => "Option::None".to_string(),
454+
},
448455
)
449456
}
450457
}

ast/src/analyzed/mod.rs

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1037,10 +1037,15 @@ pub struct PhantomBusInteractionIdentity<T> {
10371037
pub payload: ExpressionList<T>,
10381038
pub latch: AlgebraicExpression<T>,
10391039
pub folded_expressions: ExpressionList<T>,
1040-
// Note that in PIL, this is a list of expressions, but we'd
1041-
// always expect direct column references, so this is unpacked
1042-
// when converting from PIL to this struct.
1040+
// Note that in PIL, `accumulator_columns` and
1041+
// `helper_columns` are lists of expressions, but we'd
1042+
// always expect direct column references, because
1043+
// they always materialize as witness columns,
1044+
// so they are unpacked when converting from PIL
1045+
// to this struct, whereas `folded_expressions`
1046+
// can be linear and thus optimized away by pilopt.
10431047
pub accumulator_columns: Vec<AlgebraicReference>,
1048+
pub helper_columns: Option<Vec<AlgebraicReference>>,
10441049
}
10451050

10461051
impl<T> Children<AlgebraicExpression<T>> for PhantomBusInteractionIdentity<T> {

executor/src/witgen/bus_accumulator/mod.rs

Lines changed: 42 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ mod extension_field;
2121
mod fp2;
2222
mod fp4;
2323

24+
pub type InteractionColumns<T> = (Vec<Vec<T>>, Vec<Vec<T>>, Vec<Vec<T>>);
25+
2426
/// Generates the second-stage columns for the bus accumulator.
2527
pub fn generate_bus_accumulator_columns<'a, T>(
2628
pil: &'a Analyzed<T>,
@@ -127,8 +129,9 @@ impl<'a, T: FieldElement, Ext: ExtensionField<T> + Sync> BusAccumulatorGenerator
127129
.bus_interactions
128130
.par_iter()
129131
.flat_map(|bus_interaction| {
130-
let (folded, acc) = self.interaction_columns(bus_interaction);
132+
let (folded, helper, acc) = self.interaction_columns(bus_interaction);
131133
collect_folded_columns(bus_interaction, folded)
134+
.chain(collect_helper_columns(bus_interaction, helper))
132135
.chain(collect_acc_columns(bus_interaction, acc))
133136
.collect::<Vec<_>>()
134137
})
@@ -179,14 +182,20 @@ impl<'a, T: FieldElement, Ext: ExtensionField<T> + Sync> BusAccumulatorGenerator
179182
result
180183
}
181184

185+
/// Given a bus interaction and existing witness values,
186+
/// calculates and returns a triple tuple of:
187+
/// - the folded columns (one per bus interaction)
188+
/// - one helper column per pair of bus interactions
189+
/// - the accumulator column (shared by all interactions)
182190
fn interaction_columns(
183191
&self,
184192
bus_interaction: &PhantomBusInteractionIdentity<T>,
185-
) -> (Vec<Vec<T>>, Vec<Vec<T>>) {
193+
) -> InteractionColumns<T> {
186194
let intermediate_definitions = self.pil.intermediate_definitions();
187195

188196
let size = self.values.height();
189197
let mut folded_list = vec![Ext::zero(); size];
198+
let mut helper_list = vec![Ext::zero(); size];
190199
let mut acc_list = vec![Ext::zero(); size];
191200

192201
for i in 0..size {
@@ -206,28 +215,40 @@ impl<'a, T: FieldElement, Ext: ExtensionField<T> + Sync> BusAccumulatorGenerator
206215
.collect::<Vec<_>>();
207216
let folded = self.beta - self.fingerprint(&tuple);
208217

218+
let to_add = folded.inverse() * multiplicity;
219+
220+
let helper = match bus_interaction.helper_columns {
221+
Some(_) => to_add,
222+
None => Ext::zero(),
223+
};
224+
209225
let new_acc = match multiplicity.is_zero() {
210226
true => current_acc,
211-
false => current_acc + folded.inverse() * multiplicity,
227+
false => current_acc + to_add,
212228
};
213229

214230
folded_list[i] = folded;
231+
helper_list[i] = helper;
215232
acc_list[i] = new_acc;
216233
}
217234

218235
// Transpose from row-major to column-major & flatten.
219236
let mut folded = vec![Vec::with_capacity(size); Ext::size()];
237+
let mut helper = vec![Vec::with_capacity(size); Ext::size()];
220238
let mut acc = vec![Vec::with_capacity(size); Ext::size()];
221239
for row_index in 0..size {
222240
for (col_index, x) in folded_list[row_index].to_vec().into_iter().enumerate() {
223241
folded[col_index].push(x);
224242
}
243+
for (col_index, x) in helper_list[row_index].to_vec().into_iter().enumerate() {
244+
helper[col_index].push(x);
245+
}
225246
for (col_index, x) in acc_list[row_index].to_vec().into_iter().enumerate() {
226247
acc[col_index].push(x);
227248
}
228249
}
229250

230-
(folded, acc)
251+
(folded, helper, acc)
231252
}
232253

233254
/// Fingerprints a tuples of field elements, using the pre-computed powers of alpha.
@@ -279,3 +300,20 @@ fn collect_acc_columns<T>(
279300
.zip_eq(acc)
280301
.map(|(column_reference, column)| (column_reference.poly_id, column))
281302
}
303+
304+
fn collect_helper_columns<T>(
305+
bus_interaction: &PhantomBusInteractionIdentity<T>,
306+
helper: Vec<Vec<T>>,
307+
) -> impl Iterator<Item = (PolyID, Vec<T>)> {
308+
match &bus_interaction.helper_columns {
309+
Some(helper_columns) => {
310+
let pairs: Vec<_> = helper_columns
311+
.iter()
312+
.zip_eq(helper)
313+
.map(|(column_reference, column)| (column_reference.poly_id, column))
314+
.collect();
315+
pairs.into_iter()
316+
}
317+
None => Vec::new().into_iter(),
318+
}
319+
}

executor/src/witgen/data_structures/identity.rs

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -356,7 +356,7 @@ mod test {
356356
r"
357357
namespace main(4);
358358
col fixed right_latch = [0, 1]*;
359-
col witness right_selector, left_latch, a, b, multiplicities, folded, acc;
359+
col witness right_selector, left_latch, a, b, multiplicities, folded, acc, helper;
360360
{constraint}
361361
362362
// Selectors should be binary
@@ -420,9 +420,9 @@ namespace main(4);
420420
// std::protocols::lookup_via_bus::lookup_send and
421421
// std::protocols::lookup_via_bus::lookup_receive.
422422
let (send, receive) = get_generated_bus_interaction_pair(
423-
// The folded expressions and accumulator is ignored in both the bus send and receive, so we just use the same.
424-
r"Constr::PhantomBusInteraction(main::left_latch, 42, [main::a], main::left_latch, [main::folded], [main::acc]);
425-
Constr::PhantomBusInteraction(-main::multiplicities, 42, [main::b], main::right_latch, [main::folded], [main::acc]);",
423+
// The folded expressions, accumulator, and helper columns are ignored in both the bus send and receive, so we just use the same.
424+
r"Constr::PhantomBusInteraction(main::left_latch, 42, [main::a], main::left_latch, [main::folded], [main::acc], Option::None);
425+
Constr::PhantomBusInteraction(-main::multiplicities, 42, [main::b], main::right_latch, [main::folded], [main::acc], Option::None);",
426426
);
427427
assert_eq!(
428428
send.selected_payload.to_string(),
@@ -478,9 +478,9 @@ namespace main(4);
478478
// std::protocols::permutation_via_bus::permutation_send and
479479
// std::protocols::permutation_via_bus::permutation_receive.
480480
let (send, receive) = get_generated_bus_interaction_pair(
481-
// The folded expressions and accumulator is ignored in both the bus send and receive, so we just use the same.
482-
r"Constr::PhantomBusInteraction(main::left_latch, 42, [main::a], main::left_latch, [main::folded], [main::acc]);
483-
Constr::PhantomBusInteraction(-(main::right_latch * main::right_selector), 42, [main::b], main::right_latch * main::right_selector, [main::folded], [main::acc]);",
481+
// The folded expressions, accumulator, and helper columns are ignored in both the bus send and receive, so we just use the same.
482+
r"Constr::PhantomBusInteraction(main::left_latch, 42, [main::a], main::left_latch, [main::folded], [main::acc], Option::None);
483+
Constr::PhantomBusInteraction(-(main::right_latch * main::right_selector), 42, [main::b], main::right_latch * main::right_selector, [main::folded], [main::acc], Option::None);",
484484
);
485485
assert_eq!(
486486
send.selected_payload.to_string(),

pil-analyzer/src/condenser.rs

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -819,6 +819,34 @@ fn to_constraint<T: FieldElement>(
819819
.collect(),
820820
_ => panic!("Expected array, got {:?}", fields[5]),
821821
},
822+
helper_columns: match fields[6].as_ref() {
823+
Value::Enum(enum_value) => {
824+
assert_eq!(enum_value.enum_decl.name, "std::prelude::Option");
825+
match enum_value.variant {
826+
"None" => None,
827+
"Some" => {
828+
let fields = enum_value.data.as_ref().unwrap();
829+
assert_eq!(fields.len(), 1);
830+
match fields[0].as_ref() {
831+
Value::Array(fields) => fields
832+
.iter()
833+
.map(|f| match to_expr(f) {
834+
AlgebraicExpression::Reference(reference) => {
835+
assert!(!reference.next);
836+
reference
837+
}
838+
_ => panic!("Expected reference, got {f:?}"),
839+
})
840+
.collect::<Vec<_>>()
841+
.into(),
842+
_ => panic!("Expected array, got {:?}", fields[0]),
843+
}
844+
}
845+
_ => panic!("Expected Some or None, got {0}", enum_value.variant),
846+
}
847+
}
848+
_ => panic!("Expected Enum, got {:?}", fields[6]),
849+
},
822850
}
823851
.into(),
824852
_ => panic!("Expected constraint but got {constraint}"),

std/prelude.asm

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,12 @@ enum Constr {
5959
/// Note that this could refer to witness columns, intermediate columns, or
6060
/// in-lined expressions.
6161
/// - The list of accumulator columns.
62-
PhantomBusInteraction(expr, expr, expr[], expr, expr[], expr[])
62+
/// - The list of helper columns that are intermediate values
63+
/// (but materialized witnesses) to help calculate
64+
/// the accumulator columns, so that constraints are always bounded to
65+
/// degree 3. Each set of helper columns is always shared by two bus
66+
/// interactions.
67+
PhantomBusInteraction(expr, expr, expr[], expr, expr[], expr[], Option<expr[]>)
6368
}
6469

6570
/// This is the result of the "$" operator. It can be used as the left and

0 commit comments

Comments
 (0)