github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-01-08 21:58:00 -05:00
Code Issues Packages Projects Releases Wiki Activity

fix apc register memory optimizer bug (#2717)

Browse Source 
The bug that happened was that the last send of a register memory bus
interaction was removed due to having multiplicity zero. In the end the
bus was left unbalanced. Therefore, we need to run the solver optimizer
before the reg mem opt, so that these multiplicities are removed in
pairs before the apc optimizer runs and keeps only the first receive and
last send, because those multiplicities need to match. This is the main
solution implemented here in `build`. I also added some checks that the
reg mem interactions need to be even per address and in total.

A side effect of this fix is that we can no longer easily remove the
timestamp columns of removed mem int receives, the constraint that
decomposes it into bytes, the decomposing columns, and the range checks
on them. The pattern matching becomes too brittle and would be even
hackier if we wanted to keep supporting it that way. That's what causes
the regression in the test, and all the code that is removed in this PR,
since we won't do this anymore. The ultimate fix is to rely on the
optimizer to remove these columns, since:
- The reg mem int receive is removed
- Then the timestamp column becomes a free variable in its constraint
- The constraint can be removed
- The limb decomposition columns become unused in polynomial constraints
and only appear in range checks
- Therefore the range checks and columns can also be removed

At this point the result should be the same as the pattern matching
alternative removed by this PR.
I anticipate that we'll also need a fixpoint loop because it may be the
case that we need a few iterations to propagate everything possible when
this is implemented.
This commit is contained in:
Leo
2025-05-16 12:11:43 +02:00
committed by GitHub
parent 550c12b091
commit 357894b539
2 changed files with 42 additions and 76 deletions
Download Patch File Download Diff File Expand all files Collapse all files

77
autoprecompiles/src/lib.rs
View File

@@ -322,10 +322,24 @@ impl<T: FieldElement> Autoprecompiles<T> {
let machine = optimize_pc_lookup(machine, opcode);
let machine = optimize_exec_bus(machine);
let machine = optimize_precompile(machine);
let machine = optimize(machine, bus_interaction_handler, degree_bound);
assert!(check_precompile(&machine));
// We need to remove memory bus interactions with inlined multiplicity zero before
// doing register memory optimizations.
let machine = optimize(machine, bus_interaction_handler.clone(), degree_bound);
assert!(check_precompile(&machine));
let machine = remove_zero_mult(machine);
let machine = optimize_precompile(machine);
assert!(check_precompile(&machine));
// Fixpoint style re-attempt.
// TODO we probably need proper fixpoint here at some point.
let machine = optimize(machine, bus_interaction_handler, degree_bound);
assert!(check_precompile(&machine));
let machine = remove_zero_constraint(machine);
assert!(check_precompile(&machine));
// add guards to constraints that are not satisfied by zeroes
let machine = add_guards(machine);
@@ -510,11 +524,34 @@ pub fn exec_receive<T: FieldElement>(machine: &SymbolicMachine<T>) -> SymbolicBu
r
}
// Check that the number of register memory bus interactions for each concrete address in the precompile is even.
// Assumption: all register memory bus interactions feature a concrete address.
pub fn check_precompile<T: FieldElement>(machine: &SymbolicMachine<T>) -> bool {
let count_per_addr = machine
.bus_interactions
.iter()
.filter_map(|bus_int| bus_int.clone().try_into().ok())
.filter(|mem_int: &MemoryBusInteraction<T>| matches!(mem_int.ty, MemoryType::Register))
.map(|mem_int| {
mem_int.try_addr_u32().unwrap_or_else(|| {
panic!(
"Register memory access must have constant address but found {}",
mem_int.addr
)
})
})
.fold(BTreeMap::new(), |mut map, addr| {
*map.entry(addr).or_insert(0) += 1;
map
});
count_per_addr.values().all(|&v| v % 2 == 0)
}
pub fn optimize_precompile<T: FieldElement>(mut machine: SymbolicMachine<T>) -> SymbolicMachine<T> {
let mut receive = true;
let mut local_reg_mem: BTreeMap<u32, Vec<AlgebraicExpression<T>>> = BTreeMap::new();
let mut new_constraints: Vec<SymbolicConstraint<T>> = Vec::new();
let mut prev_tss: Vec<AlgebraicExpression<T>> = Vec::new();
let mut to_remove: BTreeSet<usize> = Default::default();
let mut last_store: BTreeMap<u32, usize> = BTreeMap::new();
machine
@@ -560,11 +597,6 @@ pub fn optimize_precompile<T: FieldElement>(mut machine: SymbolicMachine<T>) ->
new_constraints.push(eq_expr.into());
});
// If this receive's ts is a prev_ts, we can remove the constraint that
// decomposes this prev_ts and range checks on the limbs.
let prev_ts = mem_int.bus_interaction.args[6].clone();
assert!(powdr::is_ref(&prev_ts));
prev_tss.push(prev_ts);
to_remove.insert(i);
}
None => {
@@ -625,35 +657,6 @@ pub fn optimize_precompile<T: FieldElement>(mut machine: SymbolicMachine<T>) ->
})
.collect();
let mut to_remove: BTreeSet<AlgebraicExpression<T>> = Default::default();
machine.constraints.retain(|c| {
for prev_ts in &prev_tss {
if powdr::has_ref(&c.expr, prev_ts) {
let (col1, col2) = powdr::find_byte_decomp(&c.expr);
to_remove.insert(col1);
to_remove.insert(col2);
return false;
}
}
true
});
machine.bus_interactions.retain(|bus_int| {
if bus_int.id != RANGE_CHECK_BUS_ID {
return true;
}
assert_eq!(bus_int.args.len(), 2);
let col = bus_int.args[0].clone();
if to_remove.contains(&col) {
return false;
}
true
});
machine.constraints.extend(new_constraints);
machine

41
autoprecompiles/src/powdr.rs
View File

@@ -4,9 +4,8 @@ use std::ops::ControlFlow;
use itertools::Itertools;
use powdr_ast::analyzed::{
AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression, AlgebraicReference,
AlgebraicReferenceThin, AlgebraicUnaryOperation, BusInteractionIdentity, PolyID,
PolynomialType,
AlgebraicBinaryOperation, AlgebraicExpression, AlgebraicReference, AlgebraicReferenceThin,
AlgebraicUnaryOperation, BusInteractionIdentity, PolyID, PolynomialType,
};
use powdr_ast::parsed::asm::SymbolPath;
use powdr_ast::parsed::visitor::AllChildren;
@@ -59,42 +58,6 @@ pub fn is_zero<T: FieldElement>(expr: &AlgebraicExpression<T>) -> bool {
}
}
pub fn find_byte_decomp<T: FieldElement>(
expr: &AlgebraicExpression<T>,
) -> (AlgebraicExpression<T>, AlgebraicExpression<T>) {
let mut e1 = None;
let mut e2 = None;
expr.visit_expressions(
&mut |expr| {
if let AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation {
left,
op: AlgebraicBinaryOperator::Add,
right,
}) = expr
{
if let AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation {
left: inner_left,
op: AlgebraicBinaryOperator::Mul,
right: inner_right,
}) = &**right
{
let is_mul_by_2_17 = matches!(&**inner_right, AlgebraicExpression::Number(n) if *n == 131072u32.into());
if is_ref(&**left) && is_ref(&**inner_left) && is_mul_by_2_17 {
assert!(e1.is_none());
assert!(e2.is_none());
e1 = Some((**left).clone());
e2 = Some((**inner_left).clone());
return ControlFlow::Break(());
}
}
}
ControlFlow::Continue::<()>(())
},
VisitOrder::Pre,
);
(e1.unwrap(), e2.unwrap())
}
pub fn has_ref<T: Clone + std::cmp::PartialEq>(
expr: &AlgebraicExpression<T>,
r: &AlgebraicExpression<T>,