Skip to content

Commit

Permalink
Bus multi interaction optional helper (#2458)
Browse files Browse the repository at this point in the history
Depends on #2457. Bus logic, bus interaction type, display, and witgen
changes to support helper column being an Option::None in case of odd
number of bus interactions or Option::Some in case of even number of bus
interactions.
  • Loading branch information
qwang98 authored Feb 10, 2025
1 parent 166808b commit feb7516
Show file tree
Hide file tree
Showing 7 changed files with 110 additions and 62 deletions.
13 changes: 8 additions & 5 deletions ast/src/analyzed/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -431,7 +431,7 @@ impl<T: Display> Display for PhantomBusInteractionIdentity<T> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
write!(
f,
"Constr::PhantomBusInteraction({}, {}, [{}], {}, [{}], [{}], [{}]);",
"Constr::PhantomBusInteraction({}, {}, [{}], {}, [{}], [{}], {});",
self.multiplicity,
self.bus_id,
self.payload.0.iter().map(ToString::to_string).format(", "),
Expand All @@ -445,10 +445,13 @@ impl<T: Display> Display for PhantomBusInteractionIdentity<T> {
.iter()
.map(ToString::to_string)
.format(", "),
self.helper_columns
.iter()
.map(ToString::to_string)
.format(", ")
match &self.helper_columns {
Some(helper_columns) => format!(
"Option::Some([{}])",
helper_columns.iter().map(ToString::to_string).format(", ")
),
None => "Option::None".to_string(),
},
)
}
}
Expand Down
2 changes: 1 addition & 1 deletion ast/src/analyzed/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1045,7 +1045,7 @@ pub struct PhantomBusInteractionIdentity<T> {
// to this struct, whereas `folded_expressions`
// can be linear and thus optimized away by pilopt.
pub accumulator_columns: Vec<AlgebraicReference>,
pub helper_columns: Vec<AlgebraicReference>,
pub helper_columns: Option<Vec<AlgebraicReference>>,
}

impl<T> Children<AlgebraicExpression<T>> for PhantomBusInteractionIdentity<T> {
Expand Down
27 changes: 19 additions & 8 deletions executor/src/witgen/bus_accumulator/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -215,11 +215,16 @@ impl<'a, T: FieldElement, Ext: ExtensionField<T> + Sync> BusAccumulatorGenerator
.collect::<Vec<_>>();
let folded = self.beta - self.fingerprint(&tuple);

let helper = folded.inverse() * multiplicity;
let to_add = folded.inverse() * multiplicity;

let helper = match bus_interaction.helper_columns {
Some(_) => to_add,
None => Ext::zero(),
};

let new_acc = match multiplicity.is_zero() {
true => current_acc,
false => current_acc + helper,
false => current_acc + to_add,
};

folded_list[i] = folded;
Expand Down Expand Up @@ -299,10 +304,16 @@ fn collect_acc_columns<T>(
fn collect_helper_columns<T>(
bus_interaction: &PhantomBusInteractionIdentity<T>,
helper: Vec<Vec<T>>,
) -> impl Iterator<Item = (PolyID, Vec<T>)> + '_ {
bus_interaction
.helper_columns
.iter()
.zip_eq(helper)
.map(|(column_reference, column)| (column_reference.poly_id, column))
) -> impl Iterator<Item = (PolyID, Vec<T>)> {
match &bus_interaction.helper_columns {
Some(helper_columns) => {
let pairs: Vec<_> = helper_columns
.iter()
.zip_eq(helper)
.map(|(column_reference, column)| (column_reference.poly_id, column))
.collect();
pairs.into_iter()
}
None => Vec::new().into_iter(),
}
}
8 changes: 4 additions & 4 deletions executor/src/witgen/data_structures/identity.rs
Original file line number Diff line number Diff line change
Expand Up @@ -421,8 +421,8 @@ namespace main(4);
// std::protocols::lookup_via_bus::lookup_receive.
let (send, receive) = get_generated_bus_interaction_pair(
// The folded expressions, accumulator, and helper columns are ignored in both the bus send and receive, so we just use the same.
r"Constr::PhantomBusInteraction(main::left_latch, 42, [main::a], main::left_latch, [main::folded], [main::acc], [main::helper]);
Constr::PhantomBusInteraction(-main::multiplicities, 42, [main::b], main::right_latch, [main::folded], [main::acc], [main::helper]);",
r"Constr::PhantomBusInteraction(main::left_latch, 42, [main::a], main::left_latch, [main::folded], [main::acc], Option::None);
Constr::PhantomBusInteraction(-main::multiplicities, 42, [main::b], main::right_latch, [main::folded], [main::acc], Option::None);",
);
assert_eq!(
send.selected_payload.to_string(),
Expand Down Expand Up @@ -479,8 +479,8 @@ namespace main(4);
// std::protocols::permutation_via_bus::permutation_receive.
let (send, receive) = get_generated_bus_interaction_pair(
// The folded expressions, accumulator, and helper columns are ignored in both the bus send and receive, so we just use the same.
r"Constr::PhantomBusInteraction(main::left_latch, 42, [main::a], main::left_latch, [main::folded], [main::acc], [main::helper]);
Constr::PhantomBusInteraction(-(main::right_latch * main::right_selector), 42, [main::b], main::right_latch * main::right_selector, [main::folded], [main::acc], [main::helper]);",
r"Constr::PhantomBusInteraction(main::left_latch, 42, [main::a], main::left_latch, [main::folded], [main::acc], Option::None);
Constr::PhantomBusInteraction(-(main::right_latch * main::right_selector), 42, [main::b], main::right_latch * main::right_selector, [main::folded], [main::acc], Option::None);",
);
assert_eq!(
send.selected_payload.to_string(),
Expand Down
35 changes: 25 additions & 10 deletions pil-analyzer/src/condenser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -820,17 +820,32 @@ fn to_constraint<T: FieldElement>(
_ => panic!("Expected array, got {:?}", fields[5]),
},
helper_columns: match fields[6].as_ref() {
Value::Array(fields) => fields
.iter()
.map(|f| match to_expr(f) {
AlgebraicExpression::Reference(reference) => {
assert!(!reference.next);
reference
Value::Enum(enum_value) => {
assert_eq!(enum_value.enum_decl.name, "std::prelude::Option");
match enum_value.variant {
"None" => None,
"Some" => {
let fields = enum_value.data.as_ref().unwrap();
assert_eq!(fields.len(), 1);
match fields[0].as_ref() {
Value::Array(fields) => fields
.iter()
.map(|f| match to_expr(f) {
AlgebraicExpression::Reference(reference) => {
assert!(!reference.next);
reference
}
_ => panic!("Expected reference, got {f:?}"),
})
.collect::<Vec<_>>()
.into(),
_ => panic!("Expected array, got {:?}", fields[0]),
}
}
_ => panic!("Expected reference, got {f:?}"),
})
.collect(),
_ => panic!("Expected array, got {:?}", fields[6]),
_ => panic!("Expected Some or None, got {0}", enum_value.variant),
}
}
_ => panic!("Expected Enum, got {:?}", fields[6]),
},
}
.into(),
Expand Down
2 changes: 1 addition & 1 deletion std/prelude.asm
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ enum Constr {
/// 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[], expr[])
PhantomBusInteraction(expr, expr, expr[], expr, expr[], expr[], Option<expr[]>)
}

/// This is the result of the "$" operator. It can be used as the left and
Expand Down
85 changes: 52 additions & 33 deletions std/protocols/bus.asm
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ let bus_multi_interaction: expr[], expr[][], expr[], expr[] -> () = constr |ids,
// Or equivalently when expanded:
// folded_{2*i} * folded_{2*i+1}' * helper_i - folded_{2*i+1} * multiplicity_{2*i} - folded_{2*i} * multiplicity_{2*i+1} = 0
let helper_arr: expr[][] = array::new(
(input_len + 1) / 2,
input_len / 2,
|helper|
array::new(
extension_field_size,
Expand All @@ -115,31 +115,17 @@ let bus_multi_interaction: expr[], expr[][], expr[], expr[] -> () = constr |ids,
);
// The expression to constrain.
let helper_expr_arr = array::new( // Ext<expr>[]
(input_len + 1) / 2,
|i| if i == input_len / 2 && input_len % 2 == 1 {
// The last helper column built from odd number of bus interactions
// is simply multiplicity / folded.
// Or equivalently:
// helper_i * folded_{2*i} - multiplicity_{2*i} = 0.
input_len / 2,
|i| sub_ext(
sub_ext(
mul_ext(
helper_ext_arr[i],
folded_arr[2 * i],
mul_ext(folded_arr[2 * i], folded_arr[2 * i + 1]),
helper_ext_arr[i]
),
m_ext_arr[2 * i]
)
} else {
sub_ext(
sub_ext(
mul_ext(
mul_ext(folded_arr[2 * i], folded_arr[2 * i + 1]),
helper_ext_arr[i]
),
mul_ext(folded_arr[2 * i + 1], m_ext_arr[2 * i])
),
mul_ext(folded_arr[2 * i], m_ext_arr[2 * i + 1])
)
}
mul_ext(folded_arr[2 * i + 1], m_ext_arr[2 * i])
),
mul_ext(folded_arr[2 * i], m_ext_arr[2 * i + 1])
)
);
// Return a flattened array of constraints. (Must use `array::fold` or the compiler won't allow nested Constr[][].)
array::fold(helper_expr_arr, [], |init, helper_expr| constrain_eq_ext(helper_expr, from_base(0)));
Expand All @@ -161,19 +147,52 @@ let bus_multi_interaction: expr[], expr[][], expr[], expr[] -> () = constr |ids,
),
next_acc
);
constrain_eq_ext(update_expr, from_base(0));

// In cases where there are odd number of bus interactions, the last bus interaction doesn't need helper column.
// Instead, we have `update_expr` + multiplicity_last' / folded_last' = 0
// Or equivalently:
// `update_expr` * folded_last' + multiplicity_last' = 0
let update_expr_final = if input_len % 2 == 1 {
// Odd number of bus interactions
add_ext(
mul_ext(
update_expr,
folded_next_arr[input_len - 1]
),
m_ext_next_arr[input_len - 1]
)
} else {
// Even number of bus interactions
update_expr
};

// Constrain the accumulator update identity
constrain_eq_ext(update_expr_final, from_base(0));

// Add array of phantom bus interactions
array::new(
input_len,
|i| Constr::PhantomBusInteraction(
multiplicities[i],
ids[i],
payloads[i],
latches[i],
unpack_ext_array(folded_arr[i]),
acc,
helper_arr[i / 2])
|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])
)
}
);
};

Expand Down Expand Up @@ -334,7 +353,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, unpack_ext_array(folded), acc, []);
Constr::PhantomBusInteraction(multiplicity, id, payload, latch, unpack_ext_array(folded), acc, Option::None);
};

/// Convenience function for single bus interaction to send columns
Expand Down

0 comments on commit feb7516

Please sign in to comment.