diff --git a/autoprecompiles/Cargo.toml b/autoprecompiles/Cargo.toml index 89820f9b1e..b1539ddc38 100644 --- a/autoprecompiles/Cargo.toml +++ b/autoprecompiles/Cargo.toml @@ -23,6 +23,11 @@ rayon = "1.10.0" strum = { version = "0.27.0", features = ["derive"] } metrics = "0.23.0" +crepe = { git = "https://github.com/chriseth/crepe", branch = "profiling", version = "0.1.8" } +derive_more = "0.99.17" + +[dev-dependencies] +expect-test = "1.5.1" [package.metadata.cargo-udeps.ignore] development = ["env_logger"] diff --git a/autoprecompiles/src/constraint_optimizer.rs b/autoprecompiles/src/constraint_optimizer.rs index 225329ac5b..a1217aa088 100644 --- a/autoprecompiles/src/constraint_optimizer.rs +++ b/autoprecompiles/src/constraint_optimizer.rs @@ -23,6 +23,7 @@ use crate::{ low_degree_bus_interaction_optimizer::LowDegreeBusInteractionOptimizer, memory_optimizer::{optimize_memory, MemoryBusInteraction}, range_constraint_optimizer::RangeConstraintHandler, + rule_based_optimizer::rule_based_optimization, stats_logger::StatsLogger, }; @@ -57,10 +58,24 @@ pub fn optimize_constraints< stats_logger: &mut StatsLogger, memory_bus_id: Option, degree_bound: DegreeBound, + new_var: &mut impl FnMut(&str) -> V, ) -> Result, Error> { // Index the constraint system for the first time let constraint_system = IndexedConstraintSystem::from(constraint_system); + stats_logger.log("indexing", &constraint_system); + let (constraint_system, derived_constraints) = rule_based_optimization( + constraint_system, + &*solver, + bus_interaction_handler.clone(), + new_var, + // No degree bound given, i.e. only perform replacements that + // do not increase the degree. + None, + ); + stats_logger.log("rule-based optimization", &constraint_system); + println!("XXXX algebraic constraints:\n{constraint_system}",); + let constraint_system = solver_based_optimization(constraint_system, solver)?; stats_logger.log("solver-based optimization", &constraint_system); @@ -81,6 +96,18 @@ pub fn optimize_constraints< stats_logger, ); + let (constraint_system, derived_constraints) = rule_based_optimization( + constraint_system, + &*solver, + bus_interaction_handler.clone(), + new_var, + // No degree bound given, i.e. only perform replacements that + // do not increase the degree. + None, + ); + solver.add_algebraic_constraints(derived_constraints); + stats_logger.log("rule-based optimization", &constraint_system); + // At this point, we throw away the index and only keep the constraint system, since the rest of the optimisations are defined on the system alone let constraint_system: ConstraintSystem = constraint_system.into(); diff --git a/autoprecompiles/src/lib.rs b/autoprecompiles/src/lib.rs index 7d6ccee94c..f954654e9d 100644 --- a/autoprecompiles/src/lib.rs +++ b/autoprecompiles/src/lib.rs @@ -40,6 +40,7 @@ mod stats_logger; pub mod symbolic_machine_generator; pub use pgo::{PgoConfig, PgoType}; pub use powdr_constraint_solver::inliner::DegreeBound; +pub mod rule_based_optimizer; pub mod trace_handler; #[derive(Clone)] diff --git a/autoprecompiles/src/optimizer.rs b/autoprecompiles/src/optimizer.rs index a9af07b5f4..7358d60a43 100644 --- a/autoprecompiles/src/optimizer.rs +++ b/autoprecompiles/src/optimizer.rs @@ -4,8 +4,9 @@ use std::{collections::BTreeMap, fmt::Display}; use itertools::Itertools; use powdr_constraint_solver::constraint_system::{ - AlgebraicConstraint, ComputationMethod, DerivedVariable, + self, AlgebraicConstraint, ComputationMethod, DerivedVariable, }; +use powdr_constraint_solver::grouped_expression::NoRangeConstraints; use powdr_constraint_solver::inliner::{self, inline_everything_below_degree_bound}; use powdr_constraint_solver::solver::new_solver; use powdr_constraint_solver::{ @@ -16,6 +17,7 @@ use powdr_number::FieldElement; use crate::constraint_optimizer::trivial_simplifications; use crate::range_constraint_optimizer::optimize_range_constraints; +use crate::rule_based_optimizer::rule_based_optimization; use crate::ColumnAllocator; use crate::{ adapter::Adapter, @@ -35,7 +37,7 @@ pub fn optimize( bus_interaction_handler: A::BusInteractionHandler, degree_bound: DegreeBound, bus_map: &BusMap, - column_allocator: ColumnAllocator, + mut column_allocator: ColumnAllocator, ) -> Result<(SymbolicMachine, ColumnAllocator), crate::constraint_optimizer::Error> { let mut stats_logger = StatsLogger::start(&machine); @@ -44,7 +46,30 @@ pub fn optimize( stats_logger.log("exec bus optimization", &machine); } - let mut constraint_system = symbolic_machine_to_constraint_system(machine); + let mut new_var = |name: &str| { + let id = column_allocator.issue_next_poly_id(); + AlgebraicReference { + // TODO is it a problem that we do not check the name to be unique? + name: format!("{name}_{id}").into(), + id, + } + }; + + let constraint_system = symbolic_machine_to_constraint_system(machine); + stats_logger.log("system construction", &constraint_system); + + let (constraint_system, derived_constraints) = rule_based_optimization( + constraint_system.into(), + NoRangeConstraints, + bus_interaction_handler.clone(), + &mut new_var, + // No degree bound given, i.e. only perform replacements that + // do not increase the degree. + None, + ); + stats_logger.log("rule-based optimization", &constraint_system); + let mut constraint_system = constraint_system.system().clone(); + let mut solver = new_solver(constraint_system.clone(), bus_interaction_handler.clone()); loop { let stats = stats_logger::Stats::from(&constraint_system); @@ -55,6 +80,7 @@ pub fn optimize( &mut stats_logger, bus_map.get_bus_id(&BusType::Memory), degree_bound, + &mut new_var, )? .clone(); if stats == stats_logger::Stats::from(&constraint_system) { @@ -65,15 +91,20 @@ pub fn optimize( let constraint_system = inliner::replace_constrained_witness_columns( constraint_system.into(), inline_everything_below_degree_bound(degree_bound), - ) - .system() - .clone(); + ); stats_logger.log("inlining", &constraint_system); + let (constraint_system, _) = rule_based_optimization( + constraint_system, + &solver, + bus_interaction_handler.clone(), + &mut new_var, + Some(degree_bound), + ); // Note that the rest of the optimization does not benefit from optimizing range constraints, // so we only do it once at the end. let constraint_system = optimize_range_constraints( - constraint_system, + constraint_system.into(), bus_interaction_handler.clone(), degree_bound, ); diff --git a/autoprecompiles/src/rule_based_optimizer.rs b/autoprecompiles/src/rule_based_optimizer.rs new file mode 100644 index 0000000000..63c9e4d24f --- /dev/null +++ b/autoprecompiles/src/rule_based_optimizer.rs @@ -0,0 +1,1177 @@ +#![allow(clippy::iter_over_hash_type)] +// This is about a warning about interior mutability for the key +// `Env`. We need it and it is probably fine. +#![allow(clippy::mutable_key_type)] +use std::{ + cell::RefCell, + collections::{BTreeSet, HashMap, HashSet}, + fmt::Display, + hash::Hash, + ops::Index, +}; + +use itertools::{EitherOrBoth, Itertools}; +use powdr_constraint_solver::{ + algebraic_constraint, + constraint_system::{ + BusInteraction, BusInteractionHandler, ComputationMethod, ConstraintSystem, DerivedVariable, + }, + grouped_expression::{GroupedExpression, GroupedExpressionComponent, RangeConstraintProvider}, + indexed_constraint_system::IndexedConstraintSystem, + inliner::DegreeBound, + range_constraint::RangeConstraint, + runtime_constant::VarTransformable, +}; +use powdr_number::FieldElement; + +use derive_more::{From, Into}; +#[allow(unused_imports)] +use num_traits::Zero; + +use crepe::crepe; + +const SIZE_LIMIT: usize = 100600; + +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, From, Into)] +struct Var(usize); + +impl Display for Var { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "v_{}", self.0) + } +} + +/// A database of items that are assigned consecutive identifiers +/// and which can translate back and forth between identifiers +/// and items. +struct ItemDB { + items: Vec, + reverse: HashMap, + _phantom: std::marker::PhantomData, +} + +impl Default for ItemDB { + fn default() -> Self { + Self { + items: Vec::new(), + reverse: HashMap::new(), + _phantom: std::marker::PhantomData, + } + } +} + +impl FromIterator for ItemDB +where + Item: Clone + Hash + Eq, +{ + fn from_iter>(iter: T) -> Self { + let items = iter.into_iter().collect::>(); + let reverse = items + .iter() + .enumerate() + .map(|(i, v)| (v.clone(), i)) + .collect(); + Self { + items, + reverse, + _phantom: std::marker::PhantomData, + } + } +} + +impl Index for ItemDB +where + Ident: Into, +{ + type Output = Item; + fn index(&self, index: Ident) -> &Self::Output { + &self.items[index.into()] + } +} + +impl ItemDB +where + Item: Clone + Hash + Eq, + Ident: From + Copy, +{ + fn insert_owned_new(&mut self, item: Item) -> Ident { + let id = self.items.len(); + self.items.push(item.clone()); + self.reverse.insert(item, id); + Ident::from(id) + } + + pub fn insert(&mut self, item: &Item) -> Ident { + if let Some(&id) = self.reverse.get(item) { + Ident::from(id) + } else { + self.insert_owned_new(item.clone()) + } + } + + pub fn insert_owned(&mut self, item: Item) -> Ident { + if let Some(&id) = self.reverse.get(&item) { + Ident::from(id) + } else { + self.insert_owned_new(item) + } + } + + pub fn id(&self, item: &Item) -> Ident { + self.reverse.get(item).map(|&id| Ident::from(id)).unwrap() + } + + pub fn iter(&self) -> impl Iterator { + self.items + .iter() + .enumerate() + .map(|(i, item)| (Ident::from(i), item)) + } + + // TODO avoid using this (as pub) + pub fn next_free_id(&self) -> usize { + self.items.len() + } +} + +struct Environment { + expressions: RefCell, Expr>>, + var_to_string: HashMap, + + /// Variables that only occurr once in the system + /// (also only once in the constraint they occur in). + single_occurrence_variables: HashSet, + range_constraints_on_vars: HashMap>, + new_var_generator: RefCell>, +} + +impl Environment { + fn new( + expressions: ItemDB, Expr>, + var_to_string: HashMap, + single_occurrence_variables: HashSet, + range_constraints_on_vars: HashMap>, + new_var_generator: NewVarGenerator, + ) -> Self { + Self { + expressions: RefCell::new(expressions), + var_to_string, + single_occurrence_variables, + range_constraints_on_vars, + new_var_generator: RefCell::new(new_var_generator), + } + } + + fn terminate(self) -> (ItemDB, Expr>, NewVarGenerator) { + ( + self.expressions.into_inner(), + self.new_var_generator.into_inner(), + ) + } +} + +impl PartialEq for Environment { + fn eq(&self, _other: &Self) -> bool { + true + } +} + +impl Eq for Environment {} + +impl PartialOrd for Environment { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} + +impl Ord for Environment { + fn cmp(&self, _other: &Self) -> std::cmp::Ordering { + std::cmp::Ordering::Equal + } +} + +impl Hash for Environment { + fn hash(&self, state: &mut H) { + 0.hash(state); + } +} + +impl Environment { + pub fn insert(&self, expr: &GroupedExpression) -> Expr { + self.expressions.borrow_mut().insert(expr) + } + + pub fn insert_owned(&self, expr: GroupedExpression) -> Expr { + self.expressions.borrow_mut().insert_owned(expr) + } + + /// Extract an Expr into a free GroupedExpression. + /// This is expensive since it clones the expression. + pub fn extract(&self, expr: Expr) -> GroupedExpression { + self.expressions.borrow()[expr].clone() + } + + pub fn new_var( + &self, + prefix: &str, + method: ComputationMethod>, + ) -> Var { + self.new_var_generator.borrow_mut().generate(prefix, method) + } + + pub fn referenced_variables(&self, expr: Expr) -> BTreeSet { + let db = self.expressions.borrow(); + db[expr].referenced_unknown_variables().cloned().collect() + } + + pub fn single_occurrence_variables(&self) -> impl Iterator { + self.single_occurrence_variables.iter() + } + + pub fn affine_var_count(&self, expr: Expr) -> Option { + let db = self.expressions.borrow(); + let expr = &db[expr]; + expr.is_affine().then(|| expr.linear_components().len()) + } + + pub fn try_to_affine(&self, expr: Expr) -> Option<(T, Var, T)> { + let db = self.expressions.borrow(); + let expr = &db[expr]; + if !expr.is_affine() { + return None; + } + let (var, coeff) = expr.linear_components().exactly_one().ok()?; + Some((*coeff, *var, *expr.constant_offset())) + } + + pub fn on_expr( + &self, + expr: Expr, + args: Args, + f: impl Fn(&GroupedExpression, Args) -> Ret, + ) -> Ret { + let db = self.expressions.borrow(); + let expr = &db[expr]; + f(expr, args) + } + + pub fn range_constraint_on_expr(&self, expr: Expr) -> RangeConstraint { + let db = self.expressions.borrow(); + db[expr].range_constraint(self) + } + + // TODO potentially make this a more generic "matches structure" function + pub fn try_as_single_product(&self, expr: Expr) -> Option<(Expr, Expr)> { + let (l, r) = { + let db = self.expressions.borrow(); + let (l, r) = db[expr].try_as_single_product()?; + (l.clone(), r.clone()) + }; + // TODO eventually, l and r are cloned. + // if we change GroupedExpression to use `Expr` for the recursion, we do not + // have to insert everything multiple times. + Some((self.insert(&l), self.insert(&r))) + } + + /// Returns Some(C) if `a - b = C' and both are affine. + pub fn constant_difference(&self, a: Expr, b: Expr) -> Option { + let db = self.expressions.borrow(); + let a = &db[a]; + let b = &db[b]; + (a.is_affine() + && b.is_affine() + && a.linear_components() + .zip(b.linear_components()) + .all(|(x, y)| x == y)) + .then(|| *a.constant_offset() - *b.constant_offset()) + } + + /// If this returns `Some((v1, v2, coeff))`, then `a` and `b` are affine expressions + /// such that `b` is obtained from `a` when replacing `v1` by `v2` and + /// `coeff` is the coefficient of `v1` in `a` (and also of `v2` in `b`) + /// also `a` and `b` have at least two variables each. + pub fn differ_in_exactly_one_variable(&self, a_id: Expr, b_id: Expr) -> Option<(Var, Var, T)> { + let db = self.expressions.borrow(); + let a = &db[a_id]; + let b = &db[b_id]; + if !a.is_affine() + || !b.is_affine() + || a.constant_offset() != b.constant_offset() + || a.linear_components().len() != b.linear_components().len() + || a.linear_components().len() < 2 + { + return None; + } + let mut joined = a + .linear_components() + // Join the sorted iterators into another sorted list, + // noting where the items came from. + .merge_join_by(b.linear_components(), Ord::cmp) + // Remove those that are equal in both iterators. + .filter(|either| !matches!(either, EitherOrBoth::Both(_, _))); + let first_diff = joined.next()?; + let second_diff = joined.next()?; + if joined.next().is_some() { + return None; + } + let (left_var, right_var, coeff) = match (first_diff, second_diff) { + (EitherOrBoth::Left((lv, lc)), EitherOrBoth::Right((rv, rc))) + | (EitherOrBoth::Right((rv, rc)), EitherOrBoth::Left((lv, lc))) => { + if lc != rc { + return None; + } + (*lv, *rv, *lc) + } + _ => return None, + }; + Some((left_var, right_var, coeff)) + } + + #[allow(dead_code)] + pub fn substitute_by_known(&self, e: Expr, var: Var, value: T) -> Expr { + let expr = { + let db = self.expressions.borrow(); + let mut expr = db[e].clone(); + // expr.substitute_by_known(&var, &value); + expr.substitute_simple(&var, value); + expr + }; + self.insert_owned(expr) + } + + #[allow(dead_code)] + pub fn substitute_by_var(&self, e: Expr, var: Var, replacement: Var) -> Expr { + let expr = { + let db = self.expressions.borrow(); + let mut expr = db[e].clone(); + expr.substitute_by_unknown( + &var, + &GroupedExpression::from_unknown_variable(replacement), + ); + expr + }; + self.insert_owned(expr) + } + + #[allow(dead_code)] + pub fn format_expr(&self, expr: Expr) -> String { + let db = self.expressions.borrow(); + db[expr] + .transform_var_type(&mut |v| &self.var_to_string[v]) + .to_string() + } + + #[allow(dead_code)] + pub fn format_var(&self, var: Var) -> String { + self.var_to_string + .get(&var) + .cloned() + .unwrap_or_else(|| var.to_string()) + } +} + +struct NewVarGenerator { + counter: usize, + requests: Vec<(Var, String)>, + computation_methods: HashMap>>, +} + +impl NewVarGenerator { + fn new(initial_counter: usize) -> Self { + Self { + counter: initial_counter, + requests: Default::default(), + computation_methods: Default::default(), + } + } + + fn generate( + &mut self, + prefix: &str, + computation_method: ComputationMethod>, + ) -> Var { + let var = Var::from(self.counter); + self.requests.push((var, prefix.to_string())); + self.computation_methods.insert(var, computation_method); + self.counter += 1; + var + } +} + +impl RangeConstraintProvider for Environment { + fn get(&self, var: &Var) -> RangeConstraint { + self.range_constraints_on_vars + .get(var) + .cloned() + .unwrap_or(RangeConstraint::unconstrained()) + } +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, From, Into)] +struct Expr(usize); + +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +enum Action { + SubstituteVariableByConstant(Var, T), + SubstituteVariableByVariable(Var, Var), + ReplaceAlgebraicConstraintBy(Expr, Expr), + ReplacePairOfAlgebraicConstraintsBy(Expr, Expr, Expr), +} + +crepe! { + @input + struct Env<'a, T: FieldElement>(&'a Environment); + + @input + struct InitialAlgebraicConstraint(Expr); + + @input + struct InitialRangeConstraintOnExpression(Expr, RangeConstraint); + + struct AlgebraicConstraint(Expr); + AlgebraicConstraint(e) <- InitialAlgebraicConstraint(e); + + // @input + // struct BusInteractionConstraint<'a>(&'a BusInteraction); + + struct RangeConstraintOnExpression(Expr, RangeConstraint); + + struct Expression(Expr); + Expression(e) <- AlgebraicConstraint(e); + Expression(e) <- RangeConstraintOnExpression(e, _); + + RangeConstraintOnExpression(e, rc) <- + InitialRangeConstraintOnExpression(e, rc); + + RangeConstraintOnExpression(e, rc) <- + Env(env), + Expression(e), + let rc = env.range_constraint_on_expr(e); + + struct ContainsVariable(Expr, Var); + ContainsVariable(e, v) <- + Expression(e), + Env(env), + for v in env.referenced_variables(e); + + struct AffineExpression(Expr, T, Var, T); + AffineExpression(e, coeff, var, offset) <- + Expression(e), + Env(env), + let Some((coeff, var, offset)) = env.try_to_affine(e); + + struct RangeConstraintOnVar(Var, RangeConstraint); + RangeConstraintOnVar(v, rc) <- Env(env), ContainsVariable(_, v), let rc = env.get(&v); + // RC(coeff * var + offset) = rc <=> + // coeff * RC(var) + offset = rc <=> + // RC(var) = (rc - offset) / coeff + RangeConstraintOnVar(v, rc.combine_sum(&RangeConstraint::from_value(-offset)).multiple(T::one() / coeff)) <- + RangeConstraintOnExpression(e, rc), + AffineExpression(e, coeff, v, offset), + (coeff != T::zero()); + + RangeConstraintOnVar(v, v_rc1.conjunction(&v_rc2)) <- + RangeConstraintOnVar(v, v_rc1), + RangeConstraintOnVar(v, v_rc2); + + struct Product(Expr, Expr, Expr); + Product(e, l, r) <- + Expression(e), + Env(env), + let Some((l, r)) = env.try_as_single_product(e); + Product(e, r, l) <- Product(e, l, r); + + // (E, expr, offset) <-> E = (expr) * (expr + offset) is a constraint + struct QuadraticEquivalenceCandidate(Expr, Expr, T); + QuadraticEquivalenceCandidate(e, r, offset) <- + AlgebraicConstraint(e), + Env(env), + Product(e, l, r), + ({env.affine_var_count(l).unwrap_or(0) > 1 && env.affine_var_count(r).unwrap_or(0) > 1}), + let Some(offset) = env.constant_difference(l, r); + + struct QuadraticEquivalenceCandidatePair(Expr, Expr, T, Var, Var); + QuadraticEquivalenceCandidatePair(expr1, expr2, offset / coeff, v1, v2) <- + Env(env), + QuadraticEquivalenceCandidate(_, expr1, offset), + QuadraticEquivalenceCandidate(_, expr2, offset), + (expr1 < expr2), + let Some((v1, v2, coeff)) = env.differ_in_exactly_one_variable(expr1, expr2); + // what exactly is re-executed for an update? + + struct QuadraticEquivalence(Var, Var); + QuadraticEquivalence(v1, v2) <- + QuadraticEquivalenceCandidatePair(_, _, offset, v1, v2), + RangeConstraintOnVar(v1, rc), + RangeConstraintOnVar(v2, rc), + (rc.is_disjoint(&rc.combine_sum(&RangeConstraint::from_value(offset)))); + + struct ReplaceAlgebraicConstraintBy(Expr, Expr); + + // Combine multiple variables that only occur in the same algebraic constraint. + // + // Assume we have an algebraic constraint of the form `X * V1 + Y * V2 = R`, + // where `V1` and `V2` only occur in this constraint and only once. + // The only combination of values for `X`, `Y` and `R` where this is _not_ satisfiable + // is `X = 0`, `Y = 0`, `R != 0`. So the constraint is equivalent to the statement + // `(X = 0 and Y = 0) -> R = 0`. + // + // Considering the simpler case where both `X` and `Y` are non-negative such that + // `X + Y` does not wrap. + // Then `X = 0 and Y = 0` is equivalent to `X + Y = 0`. So we can replace the constraint + // by `(X + Y) * V3 = C`, where `V3` is a new variable that only occurs here. + // + // For the general case, where e.g. `X` can be negative, we replace it by `X * X`, + // if that value is still small enough. + struct SOV(Var); + SOV(v) <- + Env(env), + for v in env.single_occurrence_variables().cloned(); + struct SingleOccurrenceVariable(Expr, Var); + SingleOccurrenceVariable(e, v) <- + Env(env), + SOV(v), + // We somehow cannot use "v" directly here. + ContainsVariable(e, v), + AlgebraicConstraint(e); + + struct LargestSingleOccurrenceVariablePairInExpr(Expr, Var, Var); + LargestSingleOccurrenceVariablePairInExpr(e, v1, v2) <- + Env(env), + SingleOccurrenceVariable(e, v1), + SingleOccurrenceVariable(e, v2), + (v1 < v2), + (env + .single_occurrence_variables() + .filter(|v3| env.referenced_variables(e).contains(v3)) + .all(|&v3| v3 == v1 || v3 == v2 || v3 < v1)); + + struct HasProductSummand(Expr, Expr, Expr); + HasProductSummand(e, l, r) <- + Env(env), + Expression(e), + (!env.on_expr(e, (), |e, _| e.is_affine())), + for (l, r) in env.extract(e).into_summands().filter_map(|s| { + if let GroupedExpressionComponent::Quadratic(l, r) = s { + Some((env.insert_owned(l), env.insert_owned(r))) + } else { + None + } + }); + HasProductSummand(e, r, l) <- HasProductSummand(e, l, r); + Expression(l) <- HasProductSummand(_, l, _); + Expression(r) <- HasProductSummand(_, _, r); + + // FreeVariableCombinationCandidate(e, coeff1, v1, coeff2, v2, x1, x2) + // if e is the expression of an algebraic constraint and + // e = coeff1 * v1 * x1 + coeff2 * v2 * x2 + ... + // where v1 and v2 are different variables that only occur here and only once. + struct FreeVariableCombinationCandidate(Expr, T, Var, Expr, T, Var, Expr); + FreeVariableCombinationCandidate(e, coeff1, v1, x1, coeff2, v2, x2) <- + // SingleOccurrenceVariable(e, v1), + // SingleOccurrenceVariable(e, v2), + // TODO this way, we could miss optimization opportunities + // if this is not working out because of range constraints, + // but at least the replacement becomes deterministic. + LargestSingleOccurrenceVariablePairInExpr(e, v1, v2), + AlgebraicConstraint(e), + HasProductSummand(e, x1, v1_), + AffineExpression(v1_, coeff1, v1, offset1), + (offset1.is_zero()), + HasProductSummand(e, x2, v2_), + (x2 != v1_), + (x1 != v2_), + AffineExpression(v2_, coeff2, v2, offset2), + (offset2.is_zero()); + + struct PotentiallyReplaceAlgebraicConstraintBy(Expr, Expr); + + PotentiallyReplaceAlgebraicConstraintBy(e, replacement) <- + Env(env), + FreeVariableCombinationCandidate(e, coeff1, v1, x1, coeff2, v2, x2), + // Here, we have e = coeff1 * v1 * x1 + coeff2 * v2 * x2 + ... + RangeConstraintOnExpression(x1, rc1), + RangeConstraintOnExpression(x2, rc2), + let Some(replacement) = (|| { + // If the expression is not known to be non-negative, we square it. + let square_if_needed = |expr: Expr, rc: RangeConstraint| { + let expr = env.extract(expr); + if rc.range().0 == T::zero() { + (expr, rc) + } else { + (expr.clone() * expr, rc.square()) + } + }; + let (x1, rc1) = square_if_needed(x1, rc1); + let (x2, rc2) = square_if_needed(x2, rc2); + if !rc1.range().0.is_zero() || !rc2.range().0.is_zero() { + return None; + } + let sum_rc = rc1.multiple(coeff1).combine_sum(&rc2.multiple(coeff2)); + if !(sum_rc.range().0.is_zero() && sum_rc.range().1 < T::from(-1)) { + return None; + } + // Remove the summands with v1 and v2 from the expression. + let r = env.extract(e).into_summands().filter(|s|{ + if let GroupedExpressionComponent::Quadratic(l, r) = s { + let mut vars = l.referenced_unknown_variables().chain(r.referenced_unknown_variables()); + if vars.any(|v| v == &v1 || v == &v2) { + return false; + } + }; + true + }).map(GroupedExpression::from).sum::>(); + let factor = x1 * coeff1 + x2 * coeff2; + let combined_var = env.new_var("free_var", ComputationMethod::QuotientOrZero(-r.clone(), factor.clone())); + let replacement = r + GroupedExpression::from_unknown_variable(combined_var) * factor; + Some(env.insert_owned(replacement)) + })(); + + struct ProductConstraint(Expr, Expr, Expr); + ProductConstraint(e, l, r) <- + AlgebraicConstraint(e), + Product(e, l, r); + + // If we have x * a = 0 and x * b = 0 and (a = 0 and b = 0) is equivalent to (a + b = 0), + // replace those two by x * (a + b) = 0. + struct PotentiallyReplacePairOfAlgebraicConstraintsBy(Expr, Expr, Expr); + PotentiallyReplacePairOfAlgebraicConstraintsBy(e1, e2, replacement) <- + Env(env), + ProductConstraint(e1, x, a), + ProductConstraint(e2, x, b), + (e1 < e2), + RangeConstraintOnExpression(a, rc_a), + RangeConstraintOnExpression(b, rc_b), + (rc_a.range().0 == T::zero() + && rc_b.range().0 == T::zero() && rc_a.combine_sum(&rc_b).range().1 < T::from(-1)), + let replacement = env.insert_owned(env.extract(x) * (env.extract(a) + env.extract(b))); + + + // TODO wait a second. We can craete range constraints on expressions for all + // algebraic constraints. Then we just work on range constraints on expressions + // instead of algebraic constraints. Might be more difficult with the scaling, though. + + struct Solvable(Expr, Var, T); + Solvable(e, var, -offset / coeff) <- + AffineExpression(e, coeff, var, offset); + + // Boolean range constraint + RangeConstraintOnVar(v, RangeConstraint::from_range(x1, x1 + T::from(1))) <- + ProductConstraint(_, l, r), + (l < r), + Solvable(l, v, x1), + Solvable(r, v, x1 + T::from(1)); + + struct Assignment(Var, T); + Assignment(var, v) <- + AlgebraicConstraint(e), + Solvable(e, var, v); + + struct Equivalence(Var, Var); + Equivalence(v1, v2) <- QuadraticEquivalence(v1, v2); + + Equivalence(v1, v2) <- + Env(env), + AlgebraicConstraint(e), + let Some((v1, v2)) = env.on_expr(e, (), |e, _| { + if !e.is_affine() || e.constant_offset() != &T::zero() { + return None; + } + let ((v1, c1), (v2, c2)) = e.linear_components().collect_tuple()?; + let (v1, c1, v2, c2) = if v1 < v2 { + (v1, c1, v2, c2) + } else { + (v2, c2, v1, c1) + }; + // We have `c1 * v1 + c2 * v2 = 0`, which is equivalent to + // `v1 = -c2 / c1 * v2` + (-*c2 / *c1).is_one().then_some((*v1, *v2)) + }); + + + ReplaceAlgebraicConstraintBy(e, env.substitute_by_known(e, v, val)) <- + Env(env), + AlgebraicConstraint(e), + ContainsVariable(e, v), + Assignment(v, val); + ReplaceAlgebraicConstraintBy(e, env.substitute_by_var(e, v, v2)) <- + Env(env), + AlgebraicConstraint(e), + ContainsVariable(e, v), + Equivalence(v, v2); + + // TODO this way, one constraint could be replaced by multiple + // alternative constraints. + AlgebraicConstraint(e) <- + ReplaceAlgebraicConstraintBy(_, e); + + + @output + struct ActionRule(Action); + ActionRule(Action::SubstituteVariableByConstant(v, val)) <- + Assignment(v, val); + ActionRule(Action::SubstituteVariableByVariable(v, v2)) <- + Equivalence(v, v2); + ActionRule(Action::ReplaceAlgebraicConstraintBy(old, new)) <- + PotentiallyReplaceAlgebraicConstraintBy(old, new); + ActionRule(Action::ReplacePairOfAlgebraicConstraintsBy(e1, e2, replacement)) <- + PotentiallyReplacePairOfAlgebraicConstraintsBy(e1, e2, replacement); +} + +pub fn rule_based_optimization( + mut system: IndexedConstraintSystem, + range_constraints: impl RangeConstraintProvider, + bus_interaction_handler: impl BusInteractionHandler + Clone, + new_var_outer: &mut impl FnMut(&str) -> V, + degree_bound: Option, +) -> ( + IndexedConstraintSystem, + Vec>>, +) { + if system.system().algebraic_constraints.len() > SIZE_LIMIT { + log::debug!( + "Skipping rule-based optimization because the system is too large ({} > {}).", + system.system().algebraic_constraints.len(), + SIZE_LIMIT + ); + return (system, vec![]); + } + + let mut additional_algebraic_constraints = vec![]; + let mut var_mapper = system + .referenced_unknown_variables() + .cloned() + .collect::>(); + + let mut expr_db = Some(ItemDB::, Expr>::default()); + + loop { + let (algebraic_constraints, bus_interactions) = + transform_constraint_system(&system, &var_mapper, expr_db.as_mut().unwrap()); + // TODO it would be better to handle that inside the rule system, + // but it is difficult because of the vector and the combinatorial + // explosion of the range constraints. + let rcs = system + .bus_interactions() + .iter() + .zip(bus_interactions) + .flat_map(|(bus_inter, bus_inter_transformed)| { + let bi_rc = bus_inter + .fields() + .map(|e| e.range_constraint(&range_constraints)) + .collect(); + let updated_rcs = bus_interaction_handler + .handle_bus_interaction(bi_rc) + .fields() + .cloned() + .collect_vec(); + bus_inter_transformed + .fields() + .cloned() + .zip(updated_rcs) + .collect_vec() + }) + .map(|(e, rc)| InitialRangeConstraintOnExpression(e, rc)) + .collect_vec(); + let mut rt = Crepe::new(); + rt.extend(rcs.into_iter()); + + let env = Environment::::new( + expr_db.take().unwrap(), + var_mapper + .iter() + .map(|(id, var)| (id, var.to_string())) + .collect(), + system + .single_occurrence_variables() + .map(|v| var_mapper.id(v)) + .collect(), + system + .referenced_unknown_variables() + .map(|v| (var_mapper.id(v), range_constraints.get(v))) + .collect(), + // TODO or we just clone the var mapper? + NewVarGenerator::new(var_mapper.next_free_id()), + ); + + rt.extend( + algebraic_constraints + .iter() + .copied() + .map(InitialAlgebraicConstraint), + ); + rt.extend(std::iter::once(Env(&env))); + + let ((actions,), profile) = rt.run_with_profiling(); + profile.report(); + let (db, new_var_generator) = env.terminate(); + expr_db = Some(db); + + // TODO we do not need all of those variables. + for (var, prefix) in new_var_generator.requests { + let v = new_var_outer(&prefix); + assert_eq!(var_mapper.insert(&v), var); + let computation_method = untransform_computation_method( + new_var_generator.computation_methods.get(&var).unwrap(), + &var_mapper, + ); + system.extend(ConstraintSystem { + derived_variables: vec![DerivedVariable { + variable: v.clone(), + computation_method, + }], + ..Default::default() + }); + } + + // TODO update RC on vars? + + let mut progress = false; + for action in actions.into_iter().map(|a| a.0).sorted() { + match action { + Action::SubstituteVariableByConstant(var, val) => { + system.substitute_by_known(&var_mapper[var], &val); + progress = true; + } + Action::SubstituteVariableByVariable(v1, v2) => { + let (v1, v2) = if var_mapper[v1] < var_mapper[v2] { + (v1, v2) + } else { + (v2, v1) + }; + // We need to notify the solver of the equivalence. + additional_algebraic_constraints.push( + algebraic_constraint::AlgebraicConstraint::assert_zero( + GroupedExpression::from_unknown_variable(var_mapper[v1].clone()) + - GroupedExpression::from_unknown_variable(var_mapper[v2].clone()), + ), + ); + system.substitute_by_unknown( + &var_mapper[v1], + &GroupedExpression::from_unknown_variable(var_mapper[v2].clone()), + ); + progress = true; + } + Action::ReplaceAlgebraicConstraintBy(e1, e2) => { + let expr1 = + untransform_grouped_expression(&expr_db.as_ref().unwrap()[e1], &var_mapper); + let expr2 = + untransform_grouped_expression(&expr_db.as_ref().unwrap()[e2], &var_mapper); + // If the degree does not increase, we do it in any case. If the degree increases, we + // only do it if a degree bound is given and it stays within the bound. + if expr2.degree() > expr1.degree() + && (degree_bound.is_none() + || expr2.degree() > degree_bound.unwrap().identities) + { + log::debug!( + "Skipping replacement of {expr1} by {expr2} due to degree constraints." + ); + continue; + } + // TODO more efficient? + let mut found = false; + system.retain_algebraic_constraints(|c| { + if c.expression == expr1 { + found = true; + false + } else { + true + } + }); + if found { + system.add_algebraic_constraints([ + algebraic_constraint::AlgebraicConstraint::assert_zero(expr2), + ]); + progress = true; + } else { + log::warn!( + "Was about to replace {expr1} but did not find it in the system." + ); + } + } + Action::ReplacePairOfAlgebraicConstraintsBy(e1, e2, replacement) => { + let expr1 = + untransform_grouped_expression(&expr_db.as_ref().unwrap()[e1], &var_mapper); + let expr2 = + untransform_grouped_expression(&expr_db.as_ref().unwrap()[e2], &var_mapper); + let mut found1 = false; + let mut found2 = false; + for c in system.algebraic_constraints() { + if c.expression == expr1 { + found1 = true; + } else if c.expression == expr2 { + found2 = true; + } + } + if found1 && found2 { + system.retain_algebraic_constraints(|c| { + c.expression != expr1 && c.expression != expr2 + }); + let replacement = untransform_grouped_expression( + &expr_db.as_ref().unwrap()[replacement], + &var_mapper, + ); + assert!(replacement.degree() <= expr1.degree().max(expr2.degree())); + system.add_algebraic_constraints([ + algebraic_constraint::AlgebraicConstraint::assert_zero(replacement), + ]); + progress = true; + } else { + log::warn!( + "Was about to replace {expr1} and {expr2} but did not find them in the system." + ); + } + } + } + } + if !progress { + break; + } + } + system.retain_algebraic_constraints(|c| !c.is_redundant()); + (system, additional_algebraic_constraints) +} + +fn transform_constraint_system( + system: &IndexedConstraintSystem, + var_mapper: &ItemDB, + expression_db: &mut ItemDB, Expr>, +) -> (Vec, Vec>) { + let algebraic_constraints = system + .system() + .algebraic_constraints + .iter() + .map(|c| transform_grouped_expression(&c.expression, var_mapper)) + .map(|e| expression_db.insert_owned(e)) + .collect_vec(); + let bus_interactions: Vec> = system + .system() + .bus_interactions + .iter() + .map(|bus_inter| { + bus_inter + .fields() + .map(|f| transform_grouped_expression(f, var_mapper)) + .map(|e| expression_db.insert_owned(e)) + .collect() + }) + .collect_vec(); + (algebraic_constraints, bus_interactions) +} + +fn transform_grouped_expression( + expr: &GroupedExpression, + var_mapper: &ItemDB, +) -> GroupedExpression { + expr.transform_var_type(&mut |v| var_mapper.id(v)) +} + +fn untransform_grouped_expression( + expr: &GroupedExpression, + var_mapper: &ItemDB, +) -> GroupedExpression { + expr.transform_var_type(&mut |v| var_mapper[*v].clone()) +} + +fn untransform_computation_method( + method: &ComputationMethod>, + var_mapper: &ItemDB, +) -> ComputationMethod> { + match method { + ComputationMethod::Constant(c) => ComputationMethod::Constant(*c), + ComputationMethod::QuotientOrZero(numerator, denominator) => { + ComputationMethod::QuotientOrZero( + untransform_grouped_expression(numerator, var_mapper), + untransform_grouped_expression(denominator, var_mapper), + ) + } + } +} + +#[cfg(test)] +mod tests { + use expect_test::expect; + use powdr_constraint_solver::{ + algebraic_constraint, constraint_system::DefaultBusInteractionHandler, + grouped_expression::NoRangeConstraints, + }; + use powdr_number::{BabyBearField, LargeInt}; + + use super::*; + + fn assert_zero( + expr: GroupedExpression, + ) -> algebraic_constraint::AlgebraicConstraint> { + algebraic_constraint::AlgebraicConstraint::assert_zero(expr) + } + + fn v(name: &str) -> GroupedExpression { + GroupedExpression::from_unknown_variable(name.to_string()) + } + + fn c(value: i64) -> GroupedExpression { + GroupedExpression::from_number(BabyBearField::from(value)) + } + + fn new_var() -> impl FnMut(&str) -> String { + let mut counter = 0; + move |prefix: &str| { + let name = format!("{prefix}_{counter}"); + counter += 1; + name + } + } + + fn handle_variable_range_checker( + payload: &[RangeConstraint], + ) -> Vec> { + const MAX_BITS: u64 = 25; + // See: https://github.com/openvm-org/openvm/blob/v1.0.0/crates/circuits/primitives/src/var_range/bus.rs + // Expects (x, bits), where `x` is in the range [0, 2^bits - 1] + let [_x, bits] = payload else { + panic!("Expected arguments (x, bits)"); + }; + match bits.try_to_single_value() { + Some(bits_value) if bits_value.to_degree() <= MAX_BITS => { + let bits_value = bits_value.to_integer().try_into_u64().unwrap(); + let mask = (1u64 << bits_value) - 1; + vec![RangeConstraint::from_mask(mask), *bits] + } + _ => { + vec![ + RangeConstraint::from_mask((1u64 << MAX_BITS) - 1), + RangeConstraint::from_range(T::from(0), T::from(MAX_BITS)), + ] + } + } + } + + fn try_handle_bus_interaction( + bus_interaction: &BusInteraction>, + ) -> Option>> { + let mult = bus_interaction.multiplicity.try_to_single_value()?; + if mult == Zero::zero() { + return None; + } + let bus_id = bus_interaction + .bus_id + .try_to_single_value()? + .to_integer() + .try_into_u64()?; + let payload_constraints = match bus_id { + 3 => handle_variable_range_checker(&bus_interaction.payload), + _ => return None, + }; + Some(BusInteraction { + payload: payload_constraints, + ..bus_interaction.clone() + }) + } + + #[derive(Clone)] + struct TestBusInteractionHandler; + + impl BusInteractionHandler for TestBusInteractionHandler { + fn handle_bus_interaction( + &self, + bus_interaction: BusInteraction>, + ) -> BusInteraction> { + try_handle_bus_interaction(&bus_interaction).unwrap_or(bus_interaction) + } + } + + fn bit_constraint( + variable: &str, + bits: u32, + ) -> BusInteraction> { + BusInteraction { + bus_id: c(3), + payload: vec![v(variable), c(bits as i64)], + multiplicity: c(1), + } + } + + #[test] + fn test_rule_based_optimization_empty() { + let system: IndexedConstraintSystem = + IndexedConstraintSystem::default(); + let optimized_system = rule_based_optimization( + system, + NoRangeConstraints, + DefaultBusInteractionHandler::default(), + &mut new_var(), + None, + ); + assert_eq!(optimized_system.0.system().algebraic_constraints.len(), 0); + } + + #[test] + fn test_rule_based_optimization_simple_assignment() { + let mut system = IndexedConstraintSystem::default(); + let x = v("x"); + system.add_algebraic_constraints([ + assert_zero(x * BabyBearField::from(7) - c(21)), + assert_zero(v("y") * (v("y") - c(1)) - v("x")), + ]); + let optimized_system = rule_based_optimization( + system, + NoRangeConstraints, + DefaultBusInteractionHandler::default(), + &mut new_var(), + None, + ); + expect!["(y) * (y - 1) - 3 = 0"].assert_eq(&optimized_system.0.to_string()); + } + + #[test] + fn test_rule_based_optimization_quadratic_equality() { + let mut system = IndexedConstraintSystem::default(); + system.add_algebraic_constraints([ + assert_zero( + (c(30720) * v("rs1_data__0_1") + c(7864320) * v("rs1_data__1_1") + - c(30720) * v("mem_ptr_limbs__0_1") + + c(737280)) + * (c(30720) * v("rs1_data__0_1") + c(7864320) * v("rs1_data__1_1") + - c(30720) * v("mem_ptr_limbs__0_1") + + c(737281)), + ), + assert_zero( + (c(30720) * v("rs1_data__0_1") + c(7864320) * v("rs1_data__1_1") + - c(30720) * v("mem_ptr_limbs__0_2") + + c(737280)) + * (c(30720) * v("rs1_data__0_1") + c(7864320) * v("rs1_data__1_1") + - c(30720) * v("mem_ptr_limbs__0_2") + + c(737281)), + ), + ]); + system.add_bus_interactions([ + bit_constraint("rs1_data__0_1", 8), + bit_constraint("rs1_data__1_1", 8), + BusInteraction { + bus_id: c(3), + multiplicity: c(1), + payload: vec![c(-503316480) * v("mem_ptr_limbs__0_1"), c(14)], + }, + BusInteraction { + bus_id: c(3), + multiplicity: c(1), + payload: vec![c(-503316480) * v("mem_ptr_limbs__0_2"), c(14)], + }, + ]); + let optimized_system = rule_based_optimization( + system, + NoRangeConstraints, + TestBusInteractionHandler, + &mut new_var(), + None, + ); + // Note that in the system below, mem_ptr_limbs__0_2 has been eliminated + expect![[r#" + (30720 * mem_ptr_limbs__0_1 - 30720 * rs1_data__0_1 - 7864320 * rs1_data__1_1 - 737280) * (30720 * mem_ptr_limbs__0_1 - 30720 * rs1_data__0_1 - 7864320 * rs1_data__1_1 - 737281) = 0 + (30720 * mem_ptr_limbs__0_2 - 30720 * rs1_data__0_1 - 7864320 * rs1_data__1_1 - 737280) * (30720 * mem_ptr_limbs__0_2 - 30720 * rs1_data__0_1 - 7864320 * rs1_data__1_1 - 737281) = 0 + BusInteraction { bus_id: 3, multiplicity: 1, payload: rs1_data__0_1, 8 } + BusInteraction { bus_id: 3, multiplicity: 1, payload: rs1_data__1_1, 8 } + BusInteraction { bus_id: 3, multiplicity: 1, payload: -(503316480 * mem_ptr_limbs__0_1), 14 } + BusInteraction { bus_id: 3, multiplicity: 1, payload: -(503316480 * mem_ptr_limbs__0_2), 14 }"#]].assert_eq(&optimized_system.0.to_string()); + } +} diff --git a/constraint-solver/src/algebraic_constraint/solve.rs b/constraint-solver/src/algebraic_constraint/solve.rs index 4b03d73b23..dd48c4d16a 100644 --- a/constraint-solver/src/algebraic_constraint/solve.rs +++ b/constraint-solver/src/algebraic_constraint/solve.rs @@ -393,7 +393,7 @@ mod tests { use crate::grouped_expression::NoRangeConstraints; use super::*; - use powdr_number::{FieldElement, GoldilocksField}; + use powdr_number::GoldilocksField; use pretty_assertions::assert_eq; @@ -407,14 +407,6 @@ mod tests { Qse::from_number(GoldilocksField::from(value)) } - impl RangeConstraintProvider - for HashMap<&'static str, RangeConstraint> - { - fn get(&self, var: &&'static str) -> RangeConstraint { - self.get(var).cloned().unwrap_or_default() - } - } - #[test] fn unsolvable() { let r = AlgebraicConstraint::assert_zero(&Qse::from_number(GoldilocksField::from(10))) diff --git a/constraint-solver/src/constraint_system.rs b/constraint-solver/src/constraint_system.rs index dc4580836e..5dcda0ef22 100644 --- a/constraint-solver/src/constraint_system.rs +++ b/constraint-solver/src/constraint_system.rs @@ -316,7 +316,7 @@ pub trait BusInteractionHandler { /// A default bus interaction handler that does nothing. Using it is /// equivalent to ignoring bus interactions. -#[derive(Default)] +#[derive(Default, Clone)] pub struct DefaultBusInteractionHandler { _marker: std::marker::PhantomData, } diff --git a/constraint-solver/src/grouped_expression.rs b/constraint-solver/src/grouped_expression.rs index cdf27b8b72..474e87aa6a 100644 --- a/constraint-solver/src/grouped_expression.rs +++ b/constraint-solver/src/grouped_expression.rs @@ -1,5 +1,5 @@ use std::{ - collections::{BTreeMap, HashSet}, + collections::{BTreeMap, HashMap, HashSet}, fmt::Display, hash::Hash, iter::{once, Sum}, @@ -55,6 +55,33 @@ pub enum GroupedExpressionComponent { Constant(T), } +impl From> for GroupedExpression +where + F: FieldElement, + T: RuntimeConstant, + V: Clone + Ord + Eq, +{ + fn from(s: GroupedExpressionComponent) -> Self { + match s { + GroupedExpressionComponent::Quadratic(l, r) => Self { + quadratic: vec![(l, r)], + linear: Default::default(), + constant: T::zero(), + }, + GroupedExpressionComponent::Linear(v, c) => Self { + quadratic: Default::default(), + linear: [(v, c)].into_iter().collect(), + constant: T::zero(), + }, + GroupedExpressionComponent::Constant(c) => Self { + quadratic: Default::default(), + linear: Default::default(), + constant: c, + }, + } + } +} + impl, V> GroupedExpression { pub fn from_number(k: F) -> Self { Self { @@ -210,7 +237,10 @@ impl GroupedExpression { /// Otherwise, the variables returned here might also appear inside the higher order terms /// and this the dependency on these variables might be more complicated than just a /// runtime constant factor. - pub fn linear_components(&self) -> impl DoubleEndedIterator + Clone { + pub fn linear_components( + &self, + ) -> impl DoubleEndedIterator + ExactSizeIterator + Clone + { self.linear.iter() } @@ -272,6 +302,26 @@ impl GroupedExpression { self.linear.get(var) } + /// If `self` contains `var` exactly once in an affine way, + /// returns `Some((coeff, rest))` where `self = coeff * var + rest`. + /// + /// This is relatively expensive because it needs to construct a new + /// GroupedExpression. + pub fn try_extract_affine_var(&self, var: V) -> Option<(T, Self)> { + if self + .referenced_unknown_variables() + .filter(|v| *v == &var) + .count() + != 1 + { + return None; + } + let coeff = self.linear.get(&var)?.clone(); + let mut rest = self.clone(); + rest.linear.remove(&var); + Some((coeff, rest)) + } + /// Returns the range constraint of the full expression. pub fn range_constraint( &self, @@ -280,8 +330,12 @@ impl GroupedExpression { self.quadratic .iter() .map(|(l, r)| { - l.range_constraint(range_constraints) - .combine_product(&r.range_constraint(range_constraints)) + if l == r { + l.range_constraint(range_constraints).square() + } else { + l.range_constraint(range_constraints) + .combine_product(&r.range_constraint(range_constraints)) + } }) .chain(self.linear.iter().map(|(var, coeff)| { range_constraints @@ -294,6 +348,44 @@ impl GroupedExpression { } } +impl GroupedExpression { + pub fn substitute_simple(&mut self, variable: &V, substitution: T) { + if self.linear.contains_key(variable) { + let coeff = self.linear.remove(variable).unwrap(); + self.constant += coeff * substitution; + } + + let mut to_add = GroupedExpression::zero(); + self.quadratic.retain_mut(|(l, r)| { + l.substitute_simple(variable, substitution); + r.substitute_simple(variable, substitution); + match (l.try_to_known(), r.try_to_known()) { + (Some(l), Some(r)) => { + self.constant += *l * *r; + false + } + (Some(l), None) => { + if !l.is_zero() { + to_add += r.clone() * l; + } + false + } + (None, Some(r)) => { + if !r.is_zero() { + to_add += l.clone() * r; + } + false + } + _ => true, + } + }); + // remove_quadratic_terms_adding_to_zero(&mut self.quadratic); + + if !to_add.is_zero() { + *self += to_add; + } + } +} impl, V: Ord + Clone + Eq> GroupedExpression { /// Substitute a variable by a symbolically known expression. The variable can be known or unknown. /// If it was already known, it will be substituted in the known expressions. @@ -444,6 +536,14 @@ impl, T: FieldElement, V> RangeConstraintProvid } } +impl RangeConstraintProvider + for HashMap> +{ + fn get(&self, var: &V) -> RangeConstraint { + HashMap::get(self, var).cloned().unwrap_or_default() + } +} + #[derive(Clone, Copy)] pub struct NoRangeConstraints; impl RangeConstraintProvider for NoRangeConstraints { diff --git a/constraint-solver/src/indexed_constraint_system.rs b/constraint-solver/src/indexed_constraint_system.rs index abb3808987..c02d2b36b3 100644 --- a/constraint-solver/src/indexed_constraint_system.rs +++ b/constraint-solver/src/indexed_constraint_system.rs @@ -198,6 +198,24 @@ impl IndexedConstraintSystem { self.constraint_system.referenced_unknown_variables() } + /// Returns a list of variables that occur exactly once in the system. + pub fn single_occurrence_variables<'a>(&'a self) -> impl Iterator + 'a { + self.variable_occurrences.iter().filter_map(|(v, items)| { + let item = items + .iter() + .filter(|item| !item.is_derived_variable()) + .exactly_one() + .ok()?; + item.try_to_constraint_ref(&self.constraint_system) + .unwrap() + .referenced_unknown_variables() + .filter(|var| *var == v) + .exactly_one() + .is_ok() + .then_some(v) + }) + } + /// Removes all constraints that do not fulfill the predicate. pub fn retain_algebraic_constraints( &mut self, diff --git a/constraint-solver/src/range_constraint.rs b/constraint-solver/src/range_constraint.rs index 2966f91b69..bcc014eb66 100644 --- a/constraint-solver/src/range_constraint.rs +++ b/constraint-solver/src/range_constraint.rs @@ -187,6 +187,26 @@ impl RangeConstraint { } } + /// If `Self` is a valid range constraint on an expression `e`, returns + /// a valid range constraint for `e * e`. + pub fn square(&self) -> Self { + let square_rc = if self.min > self.max { + { + let max_abs = std::cmp::max(-self.min, self.max); + if max_abs.to_arbitrary_integer() * max_abs.to_arbitrary_integer() + < T::modulus().to_arbitrary_integer() + { + Self::from_range(T::zero(), max_abs * max_abs) + } else { + Default::default() + } + } + } else { + Default::default() + }; + self.combine_product(self).conjunction(&square_rc) + } + /// Returns the conjunction of this constraint and the other. /// This operation is not lossless, but if `r1` and `r2` allow /// a value `x`, then `r1.conjunction(r2)` also allows `x`. diff --git a/constraint-solver/src/solver/base.rs b/constraint-solver/src/solver/base.rs index b81de11f77..5593a4ec31 100644 --- a/constraint-solver/src/solver/base.rs +++ b/constraint-solver/src/solver/base.rs @@ -374,14 +374,15 @@ where /// Tries to find equivalent variables using quadratic constraints. fn try_solve_quadratic_equivalences(&mut self) -> bool { - let equivalences = quadratic_equivalences::find_quadratic_equalities( - self.constraint_system.system().algebraic_constraints(), - &*self, - ); - for (x, y) in &equivalences { - self.apply_assignment(y, &GroupedExpression::from_unknown_variable(x.clone())); - } - !equivalences.is_empty() + false + // let equivalences = quadratic_equivalences::find_quadratic_equalities( + // self.constraint_system.system().algebraic_constraints(), + // &*self, + // ); + // for (x, y) in &equivalences { + // self.apply_assignment(y, &GroupedExpression::from_unknown_variable(x.clone())); + // } + // !equivalences.is_empty() } /// Find groups of variables with a small set of possible assignments. diff --git a/constraint-solver/src/solver/quadratic_equivalences.rs b/constraint-solver/src/solver/quadratic_equivalences.rs index 3e54470166..d8f032f2a3 100644 --- a/constraint-solver/src/solver/quadratic_equivalences.rs +++ b/constraint-solver/src/solver/quadratic_equivalences.rs @@ -12,6 +12,7 @@ use crate::{ }; /// Given a list of constraints, tries to determine pairs of equivalent variables. +#[allow(dead_code)] pub fn find_quadratic_equalities( constraints: &[AlgebraicConstraint>], range_constraints: impl RangeConstraintProvider, @@ -21,11 +22,16 @@ pub fn find_quadratic_equalities= 2) .collect::>(); - candidates + let equiv = candidates .iter() .tuple_combinations() .flat_map(|(c1, c2)| process_quadratic_equality_candidate_pair(c1, c2, &range_constraints)) - .collect() + .collect_vec(); + for (e1, e2) in &equiv { + let (e1, e2) = if e1 < e2 { (e1, e2) } else { (e2, e1) }; + println!("{e1} == {e2} (EQS)"); + } + vec![] } /// If we have two constraints of the form @@ -73,12 +79,14 @@ fn process_quadratic_equality_candidate_pair< // Now the only remaining check is to see if the affine expressions are the same. // This could have been the first step, but it is rather expensive, so we do it last. - if c1.expr - GroupedExpression::from_unknown_variable(c1_var.clone()) - != c2.expr - GroupedExpression::from_unknown_variable(c2_var.clone()) + if c1.expr.clone() - GroupedExpression::from_unknown_variable(c1_var.clone()) + != c2.expr.clone() - GroupedExpression::from_unknown_variable(c2_var.clone()) { return None; } + // println!("XXX {c1_var}, {c2_var},\n{}\n{}", c1.expr, c2.expr); + // Now we have `(X + A) * (X + A + offset) = 0` and `(Y + A) * (Y + A + offset) = 0` // Furthermore, the range constraints of `X` and `Y` are such that for both identities, // the two alternatives can never be satisfied at the same time. Since both variables @@ -87,6 +95,7 @@ fn process_quadratic_equality_candidate_pair< // - X = -A - offset and Y = -A - offset // Since `A` has to have some value, we can conclude `X = Y`. + // None Some((c1_var.clone(), c2_var.clone())) } diff --git a/openvm/src/lib.rs b/openvm/src/lib.rs index 011817dd17..e9eea46505 100644 --- a/openvm/src/lib.rs +++ b/openvm/src/lib.rs @@ -1737,10 +1737,10 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 41, + main: 38, log_up: 56, }, - constraints: 15, + constraints: 12, bus_interactions: 26, } "#]], @@ -1765,10 +1765,10 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 41, + main: 38, log_up: 56, }, - constraints: 15, + constraints: 12, bus_interactions: 26, } "#]], @@ -1787,7 +1787,7 @@ mod tests { }, after: AirWidths { preprocessed: 0, - main: 41, + main: 38, log_up: 56, }, } @@ -1813,11 +1813,11 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 14263, - log_up: 22752, + main: 16961, + log_up: 26908, }, - constraints: 4285, - bus_interactions: 11143, + constraints: 5009, + bus_interactions: 13221, } "#]], powdr_expected_machine_count: expect![[r#" @@ -1841,11 +1841,11 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 14235, - log_up: 22720, + main: 16933, + log_up: 26876, }, - constraints: 4261, - bus_interactions: 11133, + constraints: 4985, + bus_interactions: 13211, } "#]], powdr_expected_machine_count: expect![[r#" @@ -1863,8 +1863,8 @@ mod tests { }, after: AirWidths { preprocessed: 0, - main: 14235, - log_up: 22720, + main: 16933, + log_up: 26876, }, } "#]]), @@ -1890,10 +1890,10 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 17300, + main: 17297, log_up: 27896, }, - constraints: 8834, + constraints: 8830, bus_interactions: 11925, } "#]], @@ -1912,7 +1912,7 @@ mod tests { }, after: AirWidths { preprocessed: 0, - main: 17300, + main: 17297, log_up: 27896, }, } @@ -1942,7 +1942,7 @@ mod tests { main: 19928, log_up: 30924, }, - constraints: 11103, + constraints: 11099, bus_interactions: 13442, } "#]], @@ -1987,7 +1987,7 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 2025, + main: 2022, log_up: 3472, }, constraints: 187, @@ -2015,7 +2015,7 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 2025, + main: 2022, log_up: 3472, }, constraints: 187, @@ -2043,7 +2043,7 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 2025, + main: 2022, log_up: 3472, }, constraints: 187, @@ -2065,7 +2065,7 @@ mod tests { }, after: AirWidths { preprocessed: 0, - main: 2025, + main: 2022, log_up: 3472, }, } @@ -2094,15 +2094,15 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 3246, - log_up: 5264, + main: 3291, + log_up: 5204, }, - constraints: 598, - bus_interactions: 2562, + constraints: 381, + bus_interactions: 2571, } "#]], powdr_expected_machine_count: expect![[r#" - 22 + 8 "#]], non_powdr_expected_sum: NON_POWDR_EXPECTED_SUM, non_powdr_expected_machine_count: NON_POWDR_EXPECTED_MACHINE_COUNT, @@ -2111,13 +2111,13 @@ mod tests { AirWidthsDiff { before: AirWidths { preprocessed: 0, - main: 32370, - log_up: 41644, + main: 29106, + log_up: 37212, }, after: AirWidths { preprocessed: 0, - main: 3246, - log_up: 5264, + main: 3291, + log_up: 5204, }, } "#]]), diff --git a/openvm/src/powdr_extension/trace_generator/cuda/mod.rs b/openvm/src/powdr_extension/trace_generator/cuda/mod.rs index e5adb49399..4fe2c99a78 100644 --- a/openvm/src/powdr_extension/trace_generator/cuda/mod.rs +++ b/openvm/src/powdr_extension/trace_generator/cuda/mod.rs @@ -121,7 +121,7 @@ fn compile_derived_to_gpu( bytecode.push(c.as_canonical_u32()); } ComputationMethod::QuotientOrZero(e1, e2) => { - // Encode inner expression, then apply InvOrZero + // Invert denominator (or use zero), then multiply with numerator. emit_expr(&mut bytecode, e2, apc_poly_id_to_index, apc_height); bytecode.push(OpCode::InvOrZero as u32); emit_expr(&mut bytecode, e1, apc_poly_id_to_index, apc_height); diff --git a/openvm/tests/apc_snapshots/complex/load_two_bytes_compare.txt b/openvm/tests/apc_snapshots/complex/load_two_bytes_compare.txt index b7b2a94581..ff7469e3c1 100644 --- a/openvm/tests/apc_snapshots/complex/load_two_bytes_compare.txt +++ b/openvm/tests/apc_snapshots/complex/load_two_bytes_compare.txt @@ -4,11 +4,11 @@ Instructions: BNE 52 56 28 1 1 APC advantage: - - Main columns: 98 -> 53 (1.85x reduction) + - Main columns: 98 -> 51 (1.92x reduction) - Bus interactions: 47 -> 32 (1.47x reduction) - Constraints: 47 -> 15 (3.13x reduction) -Symbolic machine using 53 unique main columns: +Symbolic machine using 51 unique main columns: from_state__timestamp_0 rs1_data__0_0 rs1_data__1_0 @@ -58,9 +58,7 @@ Symbolic machine using 53 unique main columns: prev_data__3_1 cmp_result_2 diff_inv_marker__0_2 - diff_inv_marker__1_2 - diff_inv_marker__2_2 - diff_inv_marker__3_2 + free_var_105 is_valid // Bus 0 (EXECUTION_BRIDGE): @@ -115,5 +113,5 @@ shift_most_sig_bit_1 * (shift_most_sig_bit_1 - 1) = 0 cmp_result_2 * (cmp_result_2 - 1) = 0 (1 - cmp_result_2) * ((opcode_loadb_flag0_1 - 1) * shifted_read_data__1_1 + opcode_loadb_flag0_0 * shifted_read_data__0_0 + (1 - opcode_loadb_flag0_0) * shifted_read_data__1_0 - opcode_loadb_flag0_1 * shifted_read_data__0_1) = 0 (1 - cmp_result_2) * (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) = 0 -((opcode_loadb_flag0_1 - 1) * shifted_read_data__1_1 + opcode_loadb_flag0_0 * shifted_read_data__0_0 + (1 - opcode_loadb_flag0_0) * shifted_read_data__1_0 - opcode_loadb_flag0_1 * shifted_read_data__0_1) * diff_inv_marker__0_2 + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * diff_inv_marker__1_2 + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * diff_inv_marker__2_2 + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * diff_inv_marker__3_2 - cmp_result_2 = 0 +((opcode_loadb_flag0_1 - 1) * shifted_read_data__1_1 + opcode_loadb_flag0_0 * shifted_read_data__0_0 + (1 - opcode_loadb_flag0_0) * shifted_read_data__1_0 - opcode_loadb_flag0_1 * shifted_read_data__0_1) * diff_inv_marker__0_2 + free_var_105 * ((255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1)) - cmp_result_2 = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/apc_snapshots/complex/memcpy_block.txt b/openvm/tests/apc_snapshots/complex/memcpy_block.txt index cf1f110484..ce061f467d 100644 --- a/openvm/tests/apc_snapshots/complex/memcpy_block.txt +++ b/openvm/tests/apc_snapshots/complex/memcpy_block.txt @@ -8,7 +8,7 @@ Instructions: APC advantage: - Main columns: 172 -> 37 (4.65x reduction) - Bus interactions: 87 -> 21 (4.14x reduction) - - Constraints: 111 -> 33 (3.36x reduction) + - Constraints: 111 -> 31 (3.58x reduction) Symbolic machine using 37 unique main columns: from_state__timestamp_0 @@ -46,7 +46,7 @@ Symbolic machine using 37 unique main columns: reads_aux__1__base__prev_timestamp_4 reads_aux__1__base__timestamp_lt_aux__lower_decomp__0_4 cmp_result_4 - diff_inv_marker__0_4 + free_var_177 is_valid // Bus 0 (EXECUTION_BRIDGE): @@ -81,11 +81,8 @@ mult=diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2, // Algebraic constraints: cmp_result_1 * (cmp_result_1 - 1) = 0 diff_marker__3_1 * (diff_marker__3_1 - 1) = 0 -diff_marker__3_1 * diff_val_1 = 0 diff_marker__2_1 * (diff_marker__2_1 - 1) = 0 -diff_marker__2_1 * diff_val_1 = 0 diff_marker__1_1 * (diff_marker__1_1 - 1) = 0 -diff_marker__1_1 * diff_val_1 = 0 diff_marker__0_1 * (diff_marker__0_1 - 1) = 0 (1 * is_valid - (diff_marker__0_1 + diff_marker__1_1 + diff_marker__2_1 + diff_marker__3_1)) * ((1 - a__0_0) * (2 * cmp_result_1 - 1)) = 0 diff_marker__0_1 * ((a__0_0 - 1) * (2 * cmp_result_1 - 1) + diff_val_1) = 0 @@ -108,7 +105,8 @@ diff_marker__0_2 * ((writes_aux__prev_data__0_2 - 1) * (2 * cmp_result_2 - 1) + (1 - (diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2)) * cmp_result_2 = 0 cmp_result_4 * (cmp_result_4 - 1) = 0 (1 - cmp_result_4) * (cmp_result_1 + cmp_result_2 - cmp_result_1 * cmp_result_2) = 0 -(cmp_result_1 + cmp_result_2 - cmp_result_1 * cmp_result_2) * diff_inv_marker__0_4 - cmp_result_4 = 0 +free_var_177 * (cmp_result_1 + cmp_result_2 - cmp_result_1 * cmp_result_2) - cmp_result_4 = 0 +diff_val_1 * (diff_marker__1_1 + diff_marker__2_1 + diff_marker__3_1) = 0 (1 - is_valid) * (diff_marker__0_1 + diff_marker__1_1 + diff_marker__2_1 + diff_marker__3_1) = 0 (1 - is_valid) * (diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2) = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/apc_snapshots/complex/unaligned_memcpy.txt b/openvm/tests/apc_snapshots/complex/unaligned_memcpy.txt index c0295a0265..88d02fc553 100644 --- a/openvm/tests/apc_snapshots/complex/unaligned_memcpy.txt +++ b/openvm/tests/apc_snapshots/complex/unaligned_memcpy.txt @@ -16,7 +16,7 @@ Instructions: APC advantage: - Main columns: 465 -> 105 (4.43x reduction) - Bus interactions: 242 -> 58 (4.17x reduction) - - Constraints: 286 -> 69 (4.14x reduction) + - Constraints: 286 -> 67 (4.27x reduction) Symbolic machine using 105 unique main columns: from_state__timestamp_0 @@ -122,7 +122,7 @@ Symbolic machine using 105 unique main columns: a__2_9 a__3_9 cmp_result_12 - diff_inv_marker__0_12 + free_var_470 is_valid // Bus 0 (EXECUTION_BRIDGE): @@ -224,11 +224,8 @@ flags__1_3 * (flags__1_3 - 1) + flags__2_3 * (flags__2_3 - 1) + 4 * flags__0_3 * (943718400 * writes_aux__prev_data__0_4 + 120 * a__1_4 + 30720 * a__2_4 + 7864320 * a__3_4 - (120 * writes_aux__prev_data__1_4 + 30720 * writes_aux__prev_data__2_4 + 7864320 * writes_aux__prev_data__3_4 + 943718400 * a__0_4 + 943718399 * is_valid)) * (943718400 * writes_aux__prev_data__0_4 + 120 * a__1_4 + 30720 * a__2_4 + 7864320 * a__3_4 - (120 * writes_aux__prev_data__1_4 + 30720 * writes_aux__prev_data__2_4 + 7864320 * writes_aux__prev_data__3_4 + 943718400 * a__0_4 + 943718400)) = 0 cmp_result_6 * (cmp_result_6 - 1) = 0 diff_marker__3_6 * (diff_marker__3_6 - 1) = 0 -diff_marker__3_6 * diff_val_6 = 0 diff_marker__2_6 * (diff_marker__2_6 - 1) = 0 -diff_marker__2_6 * diff_val_6 = 0 diff_marker__1_6 * (diff_marker__1_6 - 1) = 0 -diff_marker__1_6 * diff_val_6 = 0 diff_marker__0_6 * (diff_marker__0_6 - 1) = 0 (1 - (diff_marker__0_6 + diff_marker__1_6 + diff_marker__2_6 + diff_marker__3_6)) * (a__0_5 * (2 * cmp_result_6 - 1)) = 0 diff_marker__0_6 * (diff_val_6 - a__0_5 * (2 * cmp_result_6 - 1)) = 0 @@ -254,10 +251,11 @@ diff_marker__0_7 * (diff_val_7 - a__0_4 * (2 * cmp_result_7 - 1)) = 0 (120 * a__0_9 + 30720 * a__1_9 + 7864320 * a__2_9 - (120 * b__0_5 + 30720 * b__1_5 + 7864320 * b__2_5 + 120 * is_valid)) * (120 * a__0_9 + 30720 * a__1_9 + 7864320 * a__2_9 - (120 * b__0_5 + 30720 * b__1_5 + 7864320 * b__2_5 + 121)) = 0 (943718400 * b__0_5 + 120 * a__1_9 + 30720 * a__2_9 + 7864320 * a__3_9 + 943718400 * is_valid - (120 * b__1_5 + 30720 * b__2_5 + 7864320 * b__3_5 + 943718400 * a__0_9)) * (943718400 * b__0_5 + 120 * a__1_9 + 30720 * a__2_9 + 7864320 * a__3_9 + 943718399 - (120 * b__1_5 + 30720 * b__2_5 + 7864320 * b__3_5 + 943718400 * a__0_9)) = 0 cmp_result_12 * (cmp_result_12 - 1) = 0 -(1 - cmp_result_12) * (cmp_result_6 * cmp_result_7) = 0 -cmp_result_6 * cmp_result_7 * diff_inv_marker__0_12 - cmp_result_12 = 0 flags__2_3 * (flags__2_3 - 1) - (flags__0_3 * (flags__0_3 + flags__1_3 + flags__2_3 + flags__3_3 - 2) + 2 * flags__1_3 * (flags__0_3 + flags__1_3 + flags__2_3 + flags__3_3 - 2) + 3 * flags__2_3 * (flags__0_3 + flags__1_3 + flags__2_3 + flags__3_3 - 2)) = 0 +(1 - cmp_result_12) * (cmp_result_6 * cmp_result_7) = 0 +free_var_470 * (cmp_result_6 * cmp_result_7) - cmp_result_12 = 0 opcode_loadb_flag0_0 * shifted_read_data__0_0 + (1 - opcode_loadb_flag0_0) * shifted_read_data__1_0 - read_data__0_3 = 0 +diff_val_6 * (diff_marker__1_6 + diff_marker__2_6 + diff_marker__3_6) = 0 (1 - is_valid) * (diff_marker__0_6 + diff_marker__1_6 + diff_marker__2_6 + diff_marker__3_6) = 0 (1 - is_valid) * (diff_marker__0_7 + diff_marker__1_7 + diff_marker__2_7 + diff_marker__3_7) = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/apc_snapshots/pseudo_instructions/beqz.txt b/openvm/tests/apc_snapshots/pseudo_instructions/beqz.txt index cca96adc7e..4a4695ac59 100644 --- a/openvm/tests/apc_snapshots/pseudo_instructions/beqz.txt +++ b/openvm/tests/apc_snapshots/pseudo_instructions/beqz.txt @@ -2,11 +2,11 @@ Instructions: BEQ 5 0 8 1 1 APC advantage: - - Main columns: 26 -> 15 (1.73x reduction) + - Main columns: 26 -> 12 (2.17x reduction) - Bus interactions: 11 -> 10 (1.10x reduction) - - Constraints: 11 -> 7 (1.57x reduction) + - Constraints: 11 -> 4 (2.75x reduction) -Symbolic machine using 15 unique main columns: +Symbolic machine using 12 unique main columns: from_state__timestamp_0 reads_aux__0__base__prev_timestamp_0 reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 @@ -17,10 +17,7 @@ Symbolic machine using 15 unique main columns: a__2_0 a__3_0 cmp_result_0 - diff_inv_marker__0_0 - diff_inv_marker__1_0 - diff_inv_marker__2_0 - diff_inv_marker__3_0 + free_var_31 is_valid // Bus 0 (EXECUTION_BRIDGE): @@ -41,9 +38,6 @@ mult=is_valid * 1, args=[15360 * reads_aux__1__base__prev_timestamp_0 + 15360 * // Algebraic constraints: cmp_result_0 * (cmp_result_0 - 1) = 0 -cmp_result_0 * a__0_0 = 0 -cmp_result_0 * a__1_0 = 0 -cmp_result_0 * a__2_0 = 0 -cmp_result_0 * a__3_0 = 0 -a__0_0 * diff_inv_marker__0_0 + a__1_0 * diff_inv_marker__1_0 + a__2_0 * diff_inv_marker__2_0 + a__3_0 * diff_inv_marker__3_0 + cmp_result_0 - 1 * is_valid = 0 +cmp_result_0 * (a__0_0 + a__1_0 + a__2_0 + a__3_0) = 0 +free_var_31 * (a__0_0 + a__1_0 + a__2_0 + a__3_0) + cmp_result_0 - 1 * is_valid = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/apc_snapshots/pseudo_instructions/bnez.txt b/openvm/tests/apc_snapshots/pseudo_instructions/bnez.txt index 786e3455a7..d67b478a08 100644 --- a/openvm/tests/apc_snapshots/pseudo_instructions/bnez.txt +++ b/openvm/tests/apc_snapshots/pseudo_instructions/bnez.txt @@ -2,11 +2,11 @@ Instructions: BNE 5 0 8 1 1 APC advantage: - - Main columns: 26 -> 15 (1.73x reduction) + - Main columns: 26 -> 12 (2.17x reduction) - Bus interactions: 11 -> 10 (1.10x reduction) - - Constraints: 11 -> 7 (1.57x reduction) + - Constraints: 11 -> 4 (2.75x reduction) -Symbolic machine using 15 unique main columns: +Symbolic machine using 12 unique main columns: from_state__timestamp_0 reads_aux__0__base__prev_timestamp_0 reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 @@ -17,10 +17,7 @@ Symbolic machine using 15 unique main columns: a__2_0 a__3_0 cmp_result_0 - diff_inv_marker__0_0 - diff_inv_marker__1_0 - diff_inv_marker__2_0 - diff_inv_marker__3_0 + free_var_31 is_valid // Bus 0 (EXECUTION_BRIDGE): @@ -41,9 +38,6 @@ mult=is_valid * 1, args=[15360 * reads_aux__1__base__prev_timestamp_0 + 15360 * // Algebraic constraints: cmp_result_0 * (cmp_result_0 - 1) = 0 -(1 - cmp_result_0) * a__0_0 = 0 -(1 - cmp_result_0) * a__1_0 = 0 -(1 - cmp_result_0) * a__2_0 = 0 -(1 - cmp_result_0) * a__3_0 = 0 -a__0_0 * diff_inv_marker__0_0 + a__1_0 * diff_inv_marker__1_0 + a__2_0 * diff_inv_marker__2_0 + a__3_0 * diff_inv_marker__3_0 - cmp_result_0 = 0 +(1 - cmp_result_0) * (a__0_0 + a__1_0 + a__2_0 + a__3_0) = 0 +free_var_31 * (a__0_0 + a__1_0 + a__2_0 + a__3_0) - cmp_result_0 = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/apc_snapshots/single_instructions/single_beq.txt b/openvm/tests/apc_snapshots/single_instructions/single_beq.txt index 277aca5da9..716f3dc16c 100644 --- a/openvm/tests/apc_snapshots/single_instructions/single_beq.txt +++ b/openvm/tests/apc_snapshots/single_instructions/single_beq.txt @@ -2,11 +2,11 @@ Instructions: BEQ 8 5 2 1 1 APC advantage: - - Main columns: 26 -> 19 (1.37x reduction) + - Main columns: 26 -> 16 (1.62x reduction) - Bus interactions: 11 -> 10 (1.10x reduction) - Constraints: 11 -> 7 (1.57x reduction) -Symbolic machine using 19 unique main columns: +Symbolic machine using 16 unique main columns: from_state__timestamp_0 reads_aux__0__base__prev_timestamp_0 reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 @@ -21,10 +21,7 @@ Symbolic machine using 19 unique main columns: b__2_0 b__3_0 cmp_result_0 - diff_inv_marker__0_0 - diff_inv_marker__1_0 - diff_inv_marker__2_0 - diff_inv_marker__3_0 + free_var_33 is_valid // Bus 0 (EXECUTION_BRIDGE): @@ -49,5 +46,5 @@ cmp_result_0 * (a__0_0 - b__0_0) = 0 cmp_result_0 * (a__1_0 - b__1_0) = 0 cmp_result_0 * (a__2_0 - b__2_0) = 0 cmp_result_0 * (a__3_0 - b__3_0) = 0 -(a__0_0 - b__0_0) * diff_inv_marker__0_0 + (a__1_0 - b__1_0) * diff_inv_marker__1_0 + (a__2_0 - b__2_0) * diff_inv_marker__2_0 + (a__3_0 - b__3_0) * diff_inv_marker__3_0 + cmp_result_0 - 1 * is_valid = 0 +free_var_33 * ((a__0_0 - b__0_0) * (a__0_0 - b__0_0) + (a__1_0 - b__1_0) * (a__1_0 - b__1_0) + (a__2_0 - b__2_0) * (a__2_0 - b__2_0) + (a__3_0 - b__3_0) * (a__3_0 - b__3_0)) + cmp_result_0 - 1 * is_valid = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/apc_snapshots/single_instructions/single_bne.txt b/openvm/tests/apc_snapshots/single_instructions/single_bne.txt index 9b9a117315..a65969adb3 100644 --- a/openvm/tests/apc_snapshots/single_instructions/single_bne.txt +++ b/openvm/tests/apc_snapshots/single_instructions/single_bne.txt @@ -2,11 +2,11 @@ Instructions: BNE 8 5 2 1 1 APC advantage: - - Main columns: 26 -> 19 (1.37x reduction) + - Main columns: 26 -> 16 (1.62x reduction) - Bus interactions: 11 -> 10 (1.10x reduction) - Constraints: 11 -> 7 (1.57x reduction) -Symbolic machine using 19 unique main columns: +Symbolic machine using 16 unique main columns: from_state__timestamp_0 reads_aux__0__base__prev_timestamp_0 reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 @@ -21,10 +21,7 @@ Symbolic machine using 19 unique main columns: b__2_0 b__3_0 cmp_result_0 - diff_inv_marker__0_0 - diff_inv_marker__1_0 - diff_inv_marker__2_0 - diff_inv_marker__3_0 + free_var_33 is_valid // Bus 0 (EXECUTION_BRIDGE): @@ -49,5 +46,5 @@ cmp_result_0 * (cmp_result_0 - 1) = 0 (1 - cmp_result_0) * (a__1_0 - b__1_0) = 0 (1 - cmp_result_0) * (a__2_0 - b__2_0) = 0 (1 - cmp_result_0) * (a__3_0 - b__3_0) = 0 -(a__0_0 - b__0_0) * diff_inv_marker__0_0 + (a__1_0 - b__1_0) * diff_inv_marker__1_0 + (a__2_0 - b__2_0) * diff_inv_marker__2_0 + (a__3_0 - b__3_0) * diff_inv_marker__3_0 - cmp_result_0 = 0 +free_var_33 * ((a__0_0 - b__0_0) * (a__0_0 - b__0_0) + (a__1_0 - b__1_0) * (a__1_0 - b__1_0) + (a__2_0 - b__2_0) * (a__2_0 - b__2_0) + (a__3_0 - b__3_0) * (a__3_0 - b__3_0)) - cmp_result_0 = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/apc_snapshots/single_instructions/single_sra.txt b/openvm/tests/apc_snapshots/single_instructions/single_sra.txt index 0ed2ebb4c2..acff293b1e 100644 --- a/openvm/tests/apc_snapshots/single_instructions/single_sra.txt +++ b/openvm/tests/apc_snapshots/single_instructions/single_sra.txt @@ -4,7 +4,7 @@ Instructions: APC advantage: - Main columns: 53 -> 40 (1.32x reduction) - Bus interactions: 24 -> 22 (1.09x reduction) - - Constraints: 76 -> 38 (2.00x reduction) + - Constraints: 76 -> 35 (2.17x reduction) Symbolic machine using 40 unique main columns: from_state__timestamp_0 @@ -104,16 +104,13 @@ limb_shift_marker__1_0 * (limb_shift_marker__1_0 - 1) = 0 limb_shift_marker__1_0 * (a__0_0 * bit_multiplier_right_0 + bit_shift_carry__1_0 - (b__1_0 + 256 * bit_shift_carry__2_0)) = 0 limb_shift_marker__1_0 * (a__1_0 * bit_multiplier_right_0 + bit_shift_carry__2_0 - (b__2_0 + 256 * bit_shift_carry__3_0)) = 0 limb_shift_marker__1_0 * (a__2_0 * bit_multiplier_right_0 + bit_shift_carry__3_0 - (256 * b_sign_0 * (bit_multiplier_right_0 - 1) + b__3_0)) = 0 -limb_shift_marker__1_0 * (a__3_0 - 255 * b_sign_0) = 0 limb_shift_marker__2_0 * (limb_shift_marker__2_0 - 1) = 0 limb_shift_marker__2_0 * (a__0_0 * bit_multiplier_right_0 + bit_shift_carry__2_0 - (b__2_0 + 256 * bit_shift_carry__3_0)) = 0 limb_shift_marker__2_0 * (a__1_0 * bit_multiplier_right_0 + bit_shift_carry__3_0 - (256 * b_sign_0 * (bit_multiplier_right_0 - 1) + b__3_0)) = 0 -limb_shift_marker__2_0 * (a__2_0 - 255 * b_sign_0) = 0 -limb_shift_marker__2_0 * (a__3_0 - 255 * b_sign_0) = 0 (1 - (limb_shift_marker__0_0 + limb_shift_marker__1_0 + limb_shift_marker__2_0)) * (limb_shift_marker__0_0 + limb_shift_marker__1_0 + limb_shift_marker__2_0) = 0 (1 - (limb_shift_marker__0_0 + limb_shift_marker__1_0 + limb_shift_marker__2_0)) * (a__0_0 * bit_multiplier_right_0 + bit_shift_carry__3_0 - (256 * b_sign_0 * (bit_multiplier_right_0 - 1) + b__3_0)) = 0 (1 - (limb_shift_marker__0_0 + limb_shift_marker__1_0 + limb_shift_marker__2_0)) * (a__1_0 - 255 * b_sign_0) = 0 -(1 - (limb_shift_marker__0_0 + limb_shift_marker__1_0 + limb_shift_marker__2_0)) * (a__2_0 - 255 * b_sign_0) = 0 -(1 - (limb_shift_marker__0_0 + limb_shift_marker__1_0 + limb_shift_marker__2_0)) * (a__3_0 - 255 * b_sign_0) = 0 b_sign_0 * (b_sign_0 - 1) = 0 +(a__2_0 - 255 * b_sign_0) * (1 - (limb_shift_marker__0_0 + limb_shift_marker__1_0)) = 0 +(a__3_0 - 255 * b_sign_0) * (1 - limb_shift_marker__0_0) = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/optimizer.rs b/openvm/tests/optimizer.rs index 3a0cf4948b..a089d9391d 100644 --- a/openvm/tests/optimizer.rs +++ b/openvm/tests/optimizer.rs @@ -53,7 +53,7 @@ fn test_optimize() { // This cbor file above has the `is_valid` column removed, this is why the number below // might be one less than in other tests. expect![[r#" - 1756 + 1753 "#]] .assert_debug_eq(&machine.main_columns().count()); expect![[r#" @@ -87,15 +87,15 @@ fn test_sha256() { // This cbor file above has the `is_valid` column removed, this is why the number below // might be one less than in other tests. expect![[r#" - 12394 + 13288 "#]] .assert_debug_eq(&machine.main_columns().count()); expect![[r#" - 9753 + 10483 "#]] .assert_debug_eq(&machine.bus_interactions.len()); expect![[r#" - 3746 + 4148 "#]] .assert_debug_eq(&machine.constraints.len()); }