github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-01-09 14:48:16 -05:00
Code Issues Packages Projects Releases Wiki Activity

Remove free variables (#3098)

Browse Source 
This PR adds a new optimizer step:

5568270f77/autoprecompiles/src/constraint_optimizer.rs (L96-L108)

This can be useful to remove "left-over" range constraints, e.g. from
removed memory bus interactions:
- Imagine a memory bus interaction receiving a previous time stamp and
then having a range constraint like `[current_timestamp - prev_timestamp
- 1] in [BIT16]` to enforce that it is smaller than the current
timestamp.
- Then, `prev_timestamp` would only be mentioned in this stateless bus
interaction after the memory bus interaction is removed by the memory
optimizer.
- The `remove_disconnected_columns` step would not remove it, because
`current_timestamp` is also mentioned and it is connected to a stateful
bus interaction.
- The constraint is still redundant: For any value of
`current_timestamp`, the prover could pick a satisfying value for
`current_timestamp - prev_timestamp - 1` (e.g. $0$) and solve for
`prev_timestamp`

---------

Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
This commit is contained in:
Georg Wiese
2025-07-30 17:03:39 +02:00
committed by GitHub
parent eff797efe7
commit 5c8ecd2a46
2 changed files with 114 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

99
autoprecompiles/src/constraint_optimizer.rs
View File

@@ -2,12 +2,13 @@ use std::{
collections::{HashMap, HashSet},
fmt::Display,
hash::Hash,
iter::once,
};
use itertools::Itertools;
use num_traits::Zero;
use powdr_constraint_solver::{
constraint_system::{BusInteractionHandler, ConstraintSystem},
constraint_system::{BusInteractionHandler, ConstraintRef, ConstraintSystem},
grouped_expression::GroupedExpression,
indexed_constraint_system::IndexedConstraintSystem,
inliner,
@@ -49,6 +50,10 @@ pub fn optimize_constraints<P: FieldElement, V: Ord + Clone + Eq + Hash + Displa
let constraint_system = solver_based_optimization(constraint_system, solver)?;
stats_logger.log("solver-based optimization", &constraint_system);
let constraint_system =
remove_free_variables(constraint_system, solver, bus_interaction_handler.clone());
stats_logger.log("removing free variables", &constraint_system);
let constraint_system =
remove_disconnected_columns(constraint_system, solver, bus_interaction_handler.clone());
stats_logger.log("removing disconnected columns", &constraint_system);
@@ -88,6 +93,98 @@ fn solver_based_optimization<T: FieldElement, V: Clone + Ord + Hash + Display>(
Ok(constraint_system)
}
/// Removes free variables from the constraint system, under some conditions.
///
/// Motivation: Suppose there is a constraint `2 * foo = bar` and `foo` only appears in this constraint.
/// Then, if we assume that all constraints are satisfiable, the prover would be able to satisfy it for
/// any value of `bar` by solving for `foo`. Therefore, the constraint can be removed.
/// The same would be true for a *stateless* bus interaction, e.g. `[foo * bar] in [BYTES]`.
///
/// This function removes *some* constraints like this (see TODOs below).
fn remove_free_variables<T: FieldElement, V: Clone + Ord + Eq + Hash + Display>(
mut constraint_system: JournalingConstraintSystem<T, V>,
solver: &mut impl Solver<T, V>,
bus_interaction_handler: impl IsBusStateful<T> + Clone,
) -> JournalingConstraintSystem<T, V> {
let all_variables = constraint_system
.system()
.expressions()
.flat_map(|expr| expr.referenced_unknown_variables())
.cloned()
.collect::<HashSet<_>>();
let variables_to_delete = all_variables
.iter()
// Find variables that are referenced in exactly one constraint
.filter_map(|variable| {
constraint_system
.indexed_system()
.constraints_referencing_variables(once(variable.clone()))
.exactly_one()
.ok()
.map(|constraint| (variable.clone(), constraint))
})
.filter(|(variable, constraint)| match constraint {
// TODO: These constraints could be removed also if they are linear in the free variable.
// The problem with this currently is that this removes constraints like
// `writes_aux__prev_data__3_0 - BusInteractionField(15, 7)` (`writes_aux__prev_data__3_0` is a free variable)
// which causes `remove_bus_interaction_variables` to fail, because it doesn't know the definition of the
// bus interaction variable.
ConstraintRef::AlgebraicConstraint(..) => false,
ConstraintRef::BusInteraction(bus_interaction) => {
let bus_id = bus_interaction.bus_id.try_to_number().unwrap();
// Only stateless bus interactions can be removed.
let is_stateless = !bus_interaction_handler.is_stateful(bus_id);
// TODO: This is overly strict.
// We assume that the bus interaction is satisfiable. Given that it is, there
// will be at least one assignment of the payload fields that satisfies it.
// If the prover has the freedom to choose each payload field, it can always find
// a satisfying assignment.
// This could be generalized to multiple unknown fields, but it would be more complicated,
// because *each* field would need a *different* free variable.
let has_one_unknown_field = bus_interaction
.payload
.iter()
.filter(|field| field.try_to_number().is_none())
.count()
== 1;
// If the expression is linear in the free variable, the prover would be able to solve for it
// to satisfy the constraint. Otherwise, this is not necessarily the case.
// Note that if the above check is true, there will only be one field of degree > 0.
let all_degrees_at_most_one = bus_interaction
.payload
.iter()
.all(|field| field.degree_of_variable(variable) <= 1);
is_stateless && has_one_unknown_field && all_degrees_at_most_one
}
})
.map(|(variable, _constraint)| variable.clone())
.collect::<HashSet<_>>();
let variables_to_keep = all_variables
.difference(&variables_to_delete)
.cloned()
.collect::<HashSet<_>>();
solver.retain_variables(&variables_to_keep);
constraint_system.retain_algebraic_constraints(|constraint| {
constraint
.referenced_variables()
.all(|var| variables_to_keep.contains(var))
});
constraint_system.retain_bus_interactions(|bus_interaction| {
let bus_id = bus_interaction.bus_id.try_to_number().unwrap();
bus_interaction_handler.is_stateful(bus_id)
|| bus_interaction
.referenced_variables()
.all(|var| variables_to_keep.contains(var))
});
constraint_system
}
/// Removes any columns that are not connected to *stateful* bus interactions (e.g. memory),
/// because those are the only way to interact with the rest of the zkVM (e.g. other
/// instructions).

17
constraint-solver/src/grouped_expression.rs
View File

@@ -2,6 +2,7 @@ use std::{
collections::{BTreeMap, HashSet},
fmt::Display,
hash::Hash,
iter::once,
ops::{Add, AddAssign, Mul, MulAssign, Neg, Sub},
};
@@ -231,7 +232,9 @@ impl<T: RuntimeConstant, V: Ord + Clone + Eq> GroupedExpression<T, V> {
(&self.quadratic, self.linear.iter(), &self.constant)
}
/// Computes the degree of a GroupedExpression (as it is contsructed) in the unknown variables.
/// Computes the degree of a GroupedExpression in the unknown variables.
/// Note that it might overestimate the degree if the expression contains
/// terms that cancel each other out, e.g. `a * (b + 1) - a * b - a`.
/// Variables inside runtime constants are ignored.
pub fn degree(&self) -> usize {
self.quadratic
@@ -242,6 +245,18 @@ impl<T: RuntimeConstant, V: Ord + Clone + Eq> GroupedExpression<T, V> {
.unwrap_or(0)
}
/// Computes the degree of a variable in this expression.
/// Variables inside runtime constants are ignored.
pub fn degree_of_variable(&self, var: &V) -> usize {
let linear_degree = if self.linear.contains_key(var) { 1 } else { 0 };
self.quadratic
.iter()
.map(|(l, r)| l.degree_of_variable(var) + r.degree_of_variable(var))
.chain(once(linear_degree))
.max()
.unwrap()
}
/// Returns the coefficient of the variable `variable` if this is an affine expression.
/// Panics if the expression is quadratic.
pub fn coefficient_of_variable(&self, var: &V) -> Option<&T> {