diff --git a/autoprecompiles/src/adapter.rs b/autoprecompiles/src/adapter.rs index f6bd82514..f2913e8e9 100644 --- a/autoprecompiles/src/adapter.rs +++ b/autoprecompiles/src/adapter.rs @@ -9,6 +9,7 @@ use crate::{ blocks::{BasicBlock, Candidate, Instruction, Program}, constraint_optimizer::IsBusStateful, memory_optimizer::MemoryBusInteraction, + range_constraint_optimizer::RangeConstraintHandler, Apc, InstructionHandler, VmConfig, }; @@ -19,6 +20,7 @@ pub trait Adapter: Sized { type BusInteractionHandler: BusInteractionHandler + Clone + IsBusStateful + + RangeConstraintHandler + Sync; type Candidate: Candidate + Send; type Program: Program + Send; diff --git a/autoprecompiles/src/lib.rs b/autoprecompiles/src/lib.rs index 17a25e669..1d656f558 100644 --- a/autoprecompiles/src/lib.rs +++ b/autoprecompiles/src/lib.rs @@ -32,6 +32,7 @@ pub mod expression_conversion; pub mod memory_optimizer; pub mod optimizer; pub mod powdr; +pub mod range_constraint_optimizer; mod stats_logger; pub mod symbolic_machine_generator; pub use powdr_constraint_solver::inliner::DegreeBound; diff --git a/autoprecompiles/src/optimizer.rs b/autoprecompiles/src/optimizer.rs index 74dba002a..8fbde3923 100644 --- a/autoprecompiles/src/optimizer.rs +++ b/autoprecompiles/src/optimizer.rs @@ -21,6 +21,7 @@ use powdr_number::FieldElement; use crate::constraint_optimizer::IsBusStateful; use crate::memory_optimizer::MemoryBusInteraction; +use crate::range_constraint_optimizer::optimize_range_constraints; use crate::{ adapter::Adapter, bitwise_lookup_optimizer::optimize_bitwise_lookup, @@ -71,6 +72,15 @@ pub fn optimize( bus_map, )?; + // 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, + bus_interaction_handler.clone(), + degree_bound, + ); + stats_logger.log("optimizing range constraints", &constraint_system); + // Sanity check: All PC lookups should be removed, because we'd only have constants on the LHS. let pc_lookup_bus_id = bus_map.get_bus_id(&BusType::PcLookup).unwrap(); assert!( diff --git a/autoprecompiles/src/range_constraint_optimizer.rs b/autoprecompiles/src/range_constraint_optimizer.rs new file mode 100644 index 000000000..c16767712 --- /dev/null +++ b/autoprecompiles/src/range_constraint_optimizer.rs @@ -0,0 +1,167 @@ +use std::collections::BTreeMap; +use std::fmt::Display; +use std::hash::Hash; + +use itertools::Itertools; +use num_traits::One; +use powdr_constraint_solver::constraint_system::{ + BusInteraction, BusInteractionHandler, ConstraintSystem, +}; +use powdr_constraint_solver::grouped_expression::GroupedExpression; +use powdr_constraint_solver::inliner::DegreeBound; +use powdr_constraint_solver::range_constraint::RangeConstraint; +use powdr_constraint_solver::solver::{new_solver, Solver}; +use powdr_number::FieldElement; + +pub type RangeConstraints = Vec<(GroupedExpression, RangeConstraint)>; + +pub trait RangeConstraintHandler { + /// If the bus interaction *only* enforces range constraints, returns them + /// as a map of expressions to range constraints. + /// + /// For example: + /// - If a bus interaction takes two arguments `a` and `b` and enforces the + /// range constraints `0 <= a < 2^b`, it is *not* a pure range constraint if + /// both values are unknown (because the allowed values of `a` depend on `b`) + /// - On the other hand, if `b` is known, it is a pure range constraint. + /// + /// Any stateful bus interaction is not a pure range constraint. + /// This function will only be called with bus interactions with multiplicity 1. + fn pure_range_constraints( + &self, + bus_interaction: &BusInteraction>, + ) -> Option>; + + /// Given a set of range constraints, returns a list of bus interactions + /// that implements them. The implementation is free to implement multiple + /// range constraints using a single bus interaction. + /// As all input range constraints are unconditional, the multiplicity of + /// the returned bus interactions should be 1. + /// Note that only range constraints returned from `pure_range_constraints` + /// are passed here, so the implementation should always be able to construct + /// a valid bus interaction from them. + fn batch_make_range_constraints( + &self, + range_constraints: RangeConstraints, + ) -> Vec>>; +} + +/// Optimizes range constraints, minimizing the number of bus interactions. +/// +/// This step: +/// - removes range constraints that are already implied by existing constraints +/// - batches several range constraints into one bus interaction, if possible +/// - implements bit constraints via polynomial constraints, if the degree bound allows +pub fn optimize_range_constraints( + mut system: ConstraintSystem, + bus_interaction_handler: impl BusInteractionHandler + RangeConstraintHandler + Clone, + degree_bound: DegreeBound, +) -> ConstraintSystem { + // Remove all pure range constraints, but collect what was removed. + // We store the expressions to constrain in a vector, so that we can keep the order of + // the range constraints as much as possible. + let mut to_constrain = Vec::new(); + let mut range_constraints = BTreeMap::new(); + system.bus_interactions.retain(|bus_int| { + if bus_int.multiplicity != GroupedExpression::from_number(T::one()) { + // Most range constraints are unconditional in practice, it's probably not + // worth dealing with the conditional ones. + return true; + } + + match bus_interaction_handler.pure_range_constraints(bus_int) { + Some(new_range_constraints) => { + to_constrain.extend(new_range_constraints.iter().map(|(expr, _)| expr.clone())); + for (expr, rc) in new_range_constraints { + let existing_rc = range_constraints + .entry(expr) + .or_insert_with(RangeConstraint::default); + *existing_rc = existing_rc.conjunction(&rc); + } + false + } + None => true, + } + }); + + // Filter range constraints that are already implied by existing constraints. + // TODO: They could also be implied by each other. + let mut solver = new_solver(system.clone(), bus_interaction_handler.clone()); + solver.solve().unwrap(); + let to_constrain = to_constrain + .into_iter() + .unique() + .map(|expr| { + let rc = range_constraints.remove(&expr).unwrap(); + (expr, rc) + }) + .filter(|(expr, rc)| { + let current_rc = solver.range_constraint_for_expression(expr); + current_rc != current_rc.conjunction(rc) + }) + .collect::>(); + + // Implement bit constraints via polynomial constraints, if the degree bound allows. + let mut bit_constraints = Vec::new(); + let to_constrain = to_constrain + .into_iter() + .filter(|(expr, rc)| { + if rc == &RangeConstraint::from_mask(1) && expr.degree() < degree_bound.identities { + bit_constraints.push(expr.clone() * (expr.clone() - GroupedExpression::one())); + false + } else { + true + } + }) + .collect(); + + // Create all range constraints in batch and add them to the system. + let range_constraints = bus_interaction_handler.batch_make_range_constraints(to_constrain); + for bus_interaction in &range_constraints { + assert_eq!(bus_interaction.multiplicity.try_to_number(), Some(T::one())); + } + system.bus_interactions.extend(range_constraints); + system.algebraic_constraints.extend(bit_constraints); + + system +} + +/// Utility functions useful for implementing `batch_make_range_constraints`. +pub mod utils { + use itertools::Itertools; + use powdr_constraint_solver::{ + grouped_expression::GroupedExpression, range_constraint::RangeConstraint, + }; + use powdr_number::FieldElement; + use std::fmt::Display; + use std::hash::Hash; + + use crate::range_constraint_optimizer::RangeConstraints; + + /// If the range constraints is the range 0..(2^bits - 1), returns Some(bits). + pub fn range_constraint_to_num_bits( + range_constraint: &RangeConstraint, + ) -> Option { + (0..30).find(|num_bits| { + let mask = (1u64 << num_bits) - 1; + range_constraint == &RangeConstraint::from_mask(mask) + }) + } + + /// Given a a set of range constraints, filters out those which can be checked via a + /// byte constraint. + pub fn filter_byte_constraints( + range_constraints: &mut RangeConstraints, + ) -> Vec> { + let mut byte_constraints = Vec::new(); + range_constraints.retain(|(expr, rc)| match range_constraint_to_num_bits(rc) { + Some(bits) if bits <= 8 => { + let factor = GroupedExpression::from_number(T::from(1u64 << (8 - bits))); + byte_constraints.push(expr.clone() * factor.clone()); + false + } + _ => true, + }); + byte_constraints.into_iter().unique().collect() + } +} diff --git a/constraint-solver/src/grouped_expression.rs b/constraint-solver/src/grouped_expression.rs index e50430b24..28575a971 100644 --- a/constraint-solver/src/grouped_expression.rs +++ b/constraint-solver/src/grouped_expression.rs @@ -65,7 +65,7 @@ pub enum Error { /// (some kinds of) equations. /// /// The name is derived from the fact that it groups linear terms by variable. -#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] pub struct GroupedExpression { /// Quadratic terms of the form `a * X * Y`, where `a` is a (symbolically) /// known value and `X` and `Y` are grouped expressions that diff --git a/openvm/src/bus_interaction_handler/bitwise_lookup.rs b/openvm/src/bus_interaction_handler/bitwise_lookup.rs index cea5e480e..8e6d5a515 100644 --- a/openvm/src/bus_interaction_handler/bitwise_lookup.rs +++ b/openvm/src/bus_interaction_handler/bitwise_lookup.rs @@ -1,4 +1,7 @@ -use powdr_constraint_solver::range_constraint::RangeConstraint; +use powdr_autoprecompiles::range_constraint_optimizer::RangeConstraints; +use powdr_constraint_solver::{ + grouped_expression::GroupedExpression, range_constraint::RangeConstraint, +}; use powdr_number::{FieldElement, LargeInt}; use super::byte_constraint; @@ -62,6 +65,45 @@ pub fn handle_bitwise_lookup( } } +pub fn bitwise_lookup_pure_range_constraints( + payload: &[GroupedExpression], +) -> Option> { + // See: https://github.com/openvm-org/openvm/blob/v1.0.0/crates/circuits/primitives/src/bitwise_op_lookup/bus.rs + // Expects (x, y, z, op), where: + // - if op == 0, x & y are bytes, z = 0 + // - if op == 1, x & y are bytes, z = x ^ y + let [x, y, z, op] = payload else { + panic!("Expected arguments (x, y, z, op)"); + }; + let byte_rc = RangeConstraint::from_mask(0xffu64); + let zero_rc = RangeConstraint::from_value(T::zero()); + if op.try_to_number() == Some(T::from(0u64)) { + Some( + [ + (x.clone(), byte_rc.clone()), + (y.clone(), byte_rc.clone()), + (z.clone(), zero_rc.clone()), + ] + .into(), + ) + } else if x == y { + // This is a common pattern, because the `BaseAluCoreChip` range-constraints + // the output of an addition by sending each limb as both operands to the XOR table: + // https://github.com/openvm-org/openvm/blob/v1.0.0/extensions/rv32im/circuit/src/base_alu/core.rs#L131-L138 + // Note that this block also gets executed if `op` is unknown (but we know that `op` can only be 0 or 1). + Some( + [ + (x.clone(), byte_rc.clone()), + (z.clone(), zero_rc.clone()), + (op.clone(), RangeConstraint::from_mask(1)), + ] + .into(), + ) + } else { + None + } +} + #[cfg(test)] mod tests { use crate::{ diff --git a/openvm/src/bus_interaction_handler/mod.rs b/openvm/src/bus_interaction_handler/mod.rs index e856ffd6f..98d7addde 100644 --- a/openvm/src/bus_interaction_handler/mod.rs +++ b/openvm/src/bus_interaction_handler/mod.rs @@ -1,15 +1,36 @@ +use std::fmt::Display; + use bitwise_lookup::handle_bitwise_lookup; +use itertools::Itertools; use memory::handle_memory; -use powdr_autoprecompiles::{bus_map::BusType, constraint_optimizer::IsBusStateful}; +use powdr_autoprecompiles::{ + bus_map::BusType, + constraint_optimizer::IsBusStateful, + range_constraint_optimizer::{ + utils::{filter_byte_constraints, range_constraint_to_num_bits}, + RangeConstraintHandler, RangeConstraints, + }, +}; use powdr_constraint_solver::{ constraint_system::{BusInteraction, BusInteractionHandler}, + grouped_expression::GroupedExpression, range_constraint::RangeConstraint, }; use powdr_number::{FieldElement, LargeInt}; +use std::hash::Hash; use tuple_range_checker::handle_tuple_range_checker; use variable_range_checker::handle_variable_range_checker; -use crate::bus_map::{BusMap, OpenVmBusType}; +use crate::{ + bus_interaction_handler::{ + bitwise_lookup::bitwise_lookup_pure_range_constraints, + tuple_range_checker::{ + tuple_range_checker_pure_range_constraints, tuple_range_checker_ranges, + }, + variable_range_checker::variable_range_checker_pure_range_constraints, + }, + bus_map::{BusMap, OpenVmBusType}, +}; mod bitwise_lookup; mod memory; @@ -91,6 +112,132 @@ impl IsBusStateful for OpenVmBusInteractionHandler { } } +impl RangeConstraintHandler for OpenVmBusInteractionHandler { + fn pure_range_constraints( + &self, + bus_interaction: &BusInteraction>, + ) -> Option> { + let bus_id = bus_interaction + .bus_id + .try_to_number() + .unwrap() + .to_integer() + .try_into_u64() + .unwrap(); + match self.bus_map.bus_type(bus_id) { + BusType::ExecutionBridge | BusType::Memory | BusType::PcLookup => None, + BusType::OpenVmBitwiseLookup => { + bitwise_lookup_pure_range_constraints(&bus_interaction.payload) + } + BusType::Other(OpenVmBusType::VariableRangeChecker) => { + variable_range_checker_pure_range_constraints(&bus_interaction.payload) + } + BusType::Other(OpenVmBusType::TupleRangeChecker) => { + tuple_range_checker_pure_range_constraints(&bus_interaction.payload) + } + } + } + + fn batch_make_range_constraints( + &self, + mut range_constraints: RangeConstraints, + ) -> Vec>> { + let mut byte_constraints = filter_byte_constraints(&mut range_constraints); + let tuple_range_checker_ranges = tuple_range_checker_ranges::(); + assert_eq!( + tuple_range_checker_ranges.0, + RangeConstraint::from_mask(0xffu64), + ); + + // The tuple range checker bus can range-check two expressions at the same time. + // We assume the first range is a byte range (see assertion above). From the remaining + // range constraints, we find all that happen to require the second range and zip them + // with the byte constraints. + let (mut tuple_range_checker_second_args, mut range_constraints): (Vec<_>, Vec<_>) = + range_constraints + .into_iter() + .partition(|(_expr, rc)| rc == &tuple_range_checker_ranges.1); + if tuple_range_checker_second_args.len() > byte_constraints.len() { + range_constraints + .extend(tuple_range_checker_second_args.drain(byte_constraints.len()..)); + } + let num_variable_range_checker_interactions = tuple_range_checker_second_args.len(); + + let tuple_range_checker_constraints = byte_constraints + .drain(..num_variable_range_checker_interactions) + .zip_eq(tuple_range_checker_second_args) + .map(|(byte_expr, (expr2, _rc))| { + // See: https://github.com/openvm-org/openvm/blob/v1.0.0/crates/circuits/primitives/src/range_tuple/bus.rs + // Expects (x, y), where `x` is in the range [0, MAX_0] and `y` is in the range [0, MAX_1] + let bus_id = self + .bus_map + .get_bus_id(&BusType::Other(OpenVmBusType::TupleRangeChecker)) + .unwrap(); + BusInteraction { + bus_id: GroupedExpression::from_number(T::from(bus_id)), + multiplicity: GroupedExpression::from_number(T::one()), + payload: vec![byte_expr.clone(), expr2.clone()], + } + }) + .collect::>(); + + let byte_constraints = byte_constraints + .into_iter() + .chunks(2) + .into_iter() + .map(|mut bytes| { + // Use the bitwise lookup to range-check two bytes at the same time: + // See: https://github.com/openvm-org/openvm/blob/v1.0.0/crates/circuits/primitives/src/bitwise_op_lookup/bus.rs + // Expects (x, y, z, op), where: + // - if op == 0, x & y are bytes, z = 0 + // - if op == 1, x & y are bytes, z = x ^ y + let byte1 = bytes.next().unwrap(); + let byte2 = bytes + .next() + .unwrap_or(GroupedExpression::from_number(T::zero())); + + let bus_id = self + .bus_map + .get_bus_id(&BusType::OpenVmBitwiseLookup) + .unwrap(); + BusInteraction { + bus_id: GroupedExpression::from_number(T::from(bus_id)), + multiplicity: GroupedExpression::from_number(T::one()), + payload: vec![ + byte1.clone(), + byte2.clone(), + GroupedExpression::from_number(T::zero()), + GroupedExpression::from_number(T::zero()), + ], + } + }) + .collect::>(); + let other_constraints = range_constraints.into_iter().map(|(expr, rc)| { + // Use the variable range checker to range-check expressions: + // 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 num_bits = range_constraint_to_num_bits(&rc).unwrap(); + let bus_id = self + .bus_map + .get_bus_id(&BusType::Other(OpenVmBusType::VariableRangeChecker)) + .unwrap(); + BusInteraction { + bus_id: GroupedExpression::from_number(T::from(bus_id)), + multiplicity: GroupedExpression::from_number(T::one()), + payload: vec![ + expr, + GroupedExpression::from_number(T::from(num_bits as u64)), + ], + } + }); + tuple_range_checker_constraints + .into_iter() + .chain(byte_constraints) + .chain(other_constraints) + .collect::>() + } +} + #[cfg(test)] mod test_utils { diff --git a/openvm/src/bus_interaction_handler/tuple_range_checker.rs b/openvm/src/bus_interaction_handler/tuple_range_checker.rs index 75a0c7eb4..62e36258f 100644 --- a/openvm/src/bus_interaction_handler/tuple_range_checker.rs +++ b/openvm/src/bus_interaction_handler/tuple_range_checker.rs @@ -1,15 +1,18 @@ -use powdr_constraint_solver::range_constraint::RangeConstraint; +use powdr_autoprecompiles::range_constraint_optimizer::RangeConstraints; +use powdr_constraint_solver::{ + grouped_expression::GroupedExpression, range_constraint::RangeConstraint, +}; use powdr_number::FieldElement; -/// Maximum value of the first element, -/// see https://github.com/openvm-org/openvm/blob/main/extensions/rv32im/circuit/src/extension.rs#L124 +/// The ranges for the two elements in the tuple range checker. +/// see https://github.com/openvm-org/openvm/blob/v1.0.0/extensions/rv32im/circuit/src/extension.rs#L125 // TODO: This should be configurable -const MAX_0: u64 = (1u64 << 8) - 1; - -/// Maximum value of the second element, -/// see https://github.com/openvm-org/openvm/blob/main/extensions/rv32im/circuit/src/extension.rs#L124 -// TODO: This should be configurable -const MAX_1: u64 = (8 * (1 << 8)) - 1; +pub fn tuple_range_checker_ranges() -> (RangeConstraint, RangeConstraint) { + ( + RangeConstraint::from_range(T::from(0u64), T::from((1u64 << 8) - 1)), + RangeConstraint::from_range(T::from(0u64), T::from((8 * (1 << 8)) - 1)), + ) +} pub fn handle_tuple_range_checker( payload: &[RangeConstraint], @@ -20,10 +23,20 @@ pub fn handle_tuple_range_checker( panic!("Expected arguments (x, y)"); }; - vec![ - RangeConstraint::from_range(T::from(0u64), T::from(MAX_0)), - RangeConstraint::from_range(T::from(0u64), T::from(MAX_1)), - ] + let (x_rc, y_rc) = tuple_range_checker_ranges(); + vec![x_rc, y_rc] +} + +pub fn tuple_range_checker_pure_range_constraints( + payload: &[GroupedExpression], +) -> Option> { + // See: https://github.com/openvm-org/openvm/blob/v1.0.0/crates/circuits/primitives/src/range_tuple/bus.rs + // Expects (x, y), where `x` is in the range [0, MAX_0] and `y` is in the range [0, MAX_1] + let [x, y] = payload else { + panic!("Expected arguments (x, y)"); + }; + let (x_rc, y_rc) = tuple_range_checker_ranges(); + Some([(x.clone(), x_rc), (y.clone(), y_rc)].into()) } #[cfg(test)] @@ -56,7 +69,8 @@ mod tests { let y = default(); let result = run(x, y); assert_eq!(result.len(), 2); - assert_eq!(result[0], range(0, MAX_0)); - assert_eq!(result[1], range(0, MAX_1),); + let (x_rc, y_rc) = tuple_range_checker_ranges(); + assert_eq!(result[0], x_rc); + assert_eq!(result[1], y_rc); } } diff --git a/openvm/src/bus_interaction_handler/variable_range_checker.rs b/openvm/src/bus_interaction_handler/variable_range_checker.rs index 3d027b6de..54b4ab6fe 100644 --- a/openvm/src/bus_interaction_handler/variable_range_checker.rs +++ b/openvm/src/bus_interaction_handler/variable_range_checker.rs @@ -1,4 +1,7 @@ -use powdr_constraint_solver::range_constraint::RangeConstraint; +use powdr_autoprecompiles::range_constraint_optimizer::RangeConstraints; +use powdr_constraint_solver::{ + grouped_expression::GroupedExpression, range_constraint::RangeConstraint, +}; use powdr_number::{FieldElement, LargeInt}; /// The maximum number of bits that can be checked by the variable range checker. @@ -29,6 +32,23 @@ pub fn handle_variable_range_checker( } } +pub fn variable_range_checker_pure_range_constraints( + payload: &[GroupedExpression], +) -> Option> { + // 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)"); + }; + bits.try_to_number().map(|bits| { + [( + x.clone(), + RangeConstraint::from_mask((1u64 << bits.to_degree()) - 1), + )] + .into() + }) +} + #[cfg(test)] mod tests { use crate::{ diff --git a/openvm/src/lib.rs b/openvm/src/lib.rs index 6e31c6954..6db220004 100644 --- a/openvm/src/lib.rs +++ b/openvm/src/lib.rs @@ -1486,10 +1486,10 @@ mod tests { widths: AirWidths { preprocessed: 0, main: 14664, - log_up: 11960, + log_up: 10248, }, - constraints: 4143, - bus_interactions: 11630, + constraints: 4351, + bus_interactions: 9916, } "#]], powdr_expected_machine_count: expect![[r#" @@ -1514,10 +1514,10 @@ mod tests { widths: AirWidths { preprocessed: 0, main: 14644, - log_up: 11940, + log_up: 10228, }, - constraints: 4127, - bus_interactions: 11620, + constraints: 4335, + bus_interactions: 9906, } "#]], powdr_expected_machine_count: expect![[r#" @@ -1536,7 +1536,7 @@ mod tests { after: AirWidths { preprocessed: 0, main: 14644, - log_up: 11940, + log_up: 10228, }, } "#]]), @@ -1593,10 +1593,10 @@ mod tests { widths: AirWidths { preprocessed: 0, main: 2008, - log_up: 1788, + log_up: 1616, }, - constraints: 166, - bus_interactions: 1780, + constraints: 234, + bus_interactions: 1611, } "#]], powdr_expected_machine_count: expect![[r#" @@ -1621,10 +1621,10 @@ mod tests { widths: AirWidths { preprocessed: 0, main: 2008, - log_up: 1788, + log_up: 1616, }, - constraints: 166, - bus_interactions: 1780, + constraints: 234, + bus_interactions: 1611, } "#]], powdr_expected_machine_count: expect![[r#" @@ -1649,10 +1649,10 @@ mod tests { widths: AirWidths { preprocessed: 0, main: 2008, - log_up: 1788, + log_up: 1616, }, - constraints: 166, - bus_interactions: 1780, + constraints: 234, + bus_interactions: 1611, } "#]], powdr_expected_machine_count: expect![[r#" @@ -1671,7 +1671,7 @@ mod tests { after: AirWidths { preprocessed: 0, main: 2008, - log_up: 1788, + log_up: 1616, }, } "#]]), @@ -1699,15 +1699,15 @@ mod tests { AirMetrics { widths: AirWidths { preprocessed: 0, - main: 4850, - log_up: 3948, + main: 4949, + log_up: 3856, }, - constraints: 950, - bus_interactions: 3819, + constraints: 1075, + bus_interactions: 3714, } "#]], powdr_expected_machine_count: expect![[r#" - 19 + 21 "#]], non_powdr_expected_sum: NON_POWDR_EXPECTED_SUM, non_powdr_expected_machine_count: NON_POWDR_EXPECTED_MACHINE_COUNT, @@ -1716,13 +1716,13 @@ mod tests { AirWidthsDiff { before: AirWidths { preprocessed: 0, - main: 39120, - log_up: 27036, + main: 39446, + log_up: 27272, }, after: AirWidths { preprocessed: 0, - main: 4850, - log_up: 3948, + main: 4949, + log_up: 3856, }, } "#]]), diff --git a/openvm/tests/apc_builder_outputs/single_loadb.txt b/openvm/tests/apc_builder_outputs/single_loadb.txt index 11c5d2a8b..0415d8012 100644 --- a/openvm/tests/apc_builder_outputs/single_loadb.txt +++ b/openvm/tests/apc_builder_outputs/single_loadb.txt @@ -38,7 +38,6 @@ mult=is_valid * -1, args=[2, mem_ptr_limbs__0_0 + 65536 * mem_ptr_limbs__1_0 + o mult=is_valid * 1, args=[2, mem_ptr_limbs__0_0 + 65536 * mem_ptr_limbs__1_0 + opcode_loadb_flag0_0 - (2 * shift_most_sig_bit_0 + 1), shift_most_sig_bit_0 * shifted_read_data__2_0 + (1 - shift_most_sig_bit_0) * shifted_read_data__0_0, shift_most_sig_bit_0 * shifted_read_data__3_0 + (1 - shift_most_sig_bit_0) * shifted_read_data__1_0, shift_most_sig_bit_0 * shifted_read_data__0_0 + (1 - shift_most_sig_bit_0) * shifted_read_data__2_0, shift_most_sig_bit_0 * shifted_read_data__1_0 + (1 - shift_most_sig_bit_0) * shifted_read_data__3_0, from_state__timestamp_0 + 1] // Bus 3 (VARIABLE_RANGE_CHECKER): -mult=is_valid * 1, args=[shifted_read_data__0_0 * opcode_loadb_flag0_0 + shifted_read_data__1_0 * (1 - opcode_loadb_flag0_0) - 128 * data_most_sig_bit_0, 7] mult=is_valid * 1, args=[rs1_aux_cols__base__timestamp_lt_aux__lower_decomp__0_0, 17] mult=is_valid * 1, args=[15360 * rs1_aux_cols__base__prev_timestamp_0 + 15360 * rs1_aux_cols__base__timestamp_lt_aux__lower_decomp__0_0 + 15360 - 15360 * from_state__timestamp_0, 12] mult=is_valid * 1, args=[1006632960 * shift_most_sig_bit_0 + 503316480 - (503316480 * mem_ptr_limbs__0_0 + 503316480 * opcode_loadb_flag0_0), 14] @@ -46,6 +45,9 @@ mult=is_valid * 1, args=[mem_ptr_limbs__1_0, 13] mult=is_valid * 1, args=[read_data_aux__base__timestamp_lt_aux__lower_decomp__0_0, 17] mult=is_valid * 1, args=[15360 * read_data_aux__base__prev_timestamp_0 + 15360 * read_data_aux__base__timestamp_lt_aux__lower_decomp__0_0 - 15360 * from_state__timestamp_0, 12] +// Bus 6 (OPENVM_BITWISE_LOOKUP): +mult=is_valid * 1, args=[2 * shifted_read_data__0_0 * opcode_loadb_flag0_0 + 2 * shifted_read_data__1_0 * (1 - opcode_loadb_flag0_0) - 256 * data_most_sig_bit_0, 0, 0, 0] + // Algebraic constraints: opcode_loadb_flag0_0 * (opcode_loadb_flag0_0 - 1) = 0 data_most_sig_bit_0 * (data_most_sig_bit_0 - 1) = 0 diff --git a/openvm/tests/apc_builder_outputs/single_loadh.txt b/openvm/tests/apc_builder_outputs/single_loadh.txt index b390356f4..966ed0dfb 100644 --- a/openvm/tests/apc_builder_outputs/single_loadh.txt +++ b/openvm/tests/apc_builder_outputs/single_loadh.txt @@ -45,7 +45,6 @@ mult=is_valid * -1, args=[1, 8, prev_data__0_0, prev_data__1_0, prev_data__2_0, mult=is_valid * 1, args=[1, 8, shifted_read_data__0_0, shifted_read_data__1_0, 255 * data_most_sig_bit_0, 255 * data_most_sig_bit_0, from_state__timestamp_0 + 2] // Bus 3 (VARIABLE_RANGE_CHECKER): -mult=is_valid * 1, args=[shifted_read_data__1_0 - 128 * data_most_sig_bit_0, 7] mult=is_valid * 1, args=[rs1_aux_cols__base__timestamp_lt_aux__lower_decomp__0_0, 17] mult=is_valid * 1, args=[15360 * rs1_aux_cols__base__prev_timestamp_0 + 15360 * rs1_aux_cols__base__timestamp_lt_aux__lower_decomp__0_0 + 15360 - 15360 * from_state__timestamp_0, 12] mult=is_valid * 1, args=[1006632960 * shift_most_sig_bit_0 - 503316480 * mem_ptr_limbs__0_0, 14] @@ -55,6 +54,9 @@ mult=is_valid * 1, args=[15360 * read_data_aux__base__prev_timestamp_0 + 15360 * mult=is_valid * 1, args=[write_base_aux__timestamp_lt_aux__lower_decomp__0_0, 17] mult=is_valid * 1, args=[15360 * write_base_aux__prev_timestamp_0 + 15360 * write_base_aux__timestamp_lt_aux__lower_decomp__0_0 - (15360 * from_state__timestamp_0 + 15360), 12] +// Bus 6 (OPENVM_BITWISE_LOOKUP): +mult=is_valid * 1, args=[2 * shifted_read_data__1_0 - 256 * data_most_sig_bit_0, 0, 0, 0] + // Algebraic constraints: data_most_sig_bit_0 * (data_most_sig_bit_0 - 1) = 0 shift_most_sig_bit_0 * (shift_most_sig_bit_0 - 1) = 0 diff --git a/openvm/tests/apc_builder_outputs/single_sll.txt b/openvm/tests/apc_builder_outputs/single_sll.txt index 7c51e1f0d..7456b840b 100644 --- a/openvm/tests/apc_builder_outputs/single_sll.txt +++ b/openvm/tests/apc_builder_outputs/single_sll.txt @@ -3,7 +3,7 @@ Instructions: APC advantage: - Main columns: 53 -> 18 (2.94x reduction) - - Bus interactions: 24 -> 16 (1.50x reduction) + - Bus interactions: 24 -> 14 (1.71x reduction) - Constraints: 76 -> 1 (76.00x reduction) Symbolic machine using 18 unique main columns: @@ -37,16 +37,14 @@ mult=is_valid * -1, args=[1, 68, writes_aux__prev_data__0_0, writes_aux__prev_da mult=is_valid * 1, args=[1, 68, a__0_0, a__1_0, a__2_0, a__3_0, from_state__timestamp_0 + 2] // Bus 3 (VARIABLE_RANGE_CHECKER): -mult=is_valid * 1, args=[7864320 * a__0_0 - 62914560 * b__0_0, 3] -mult=is_valid * 1, args=[30720 * a__0_0 + 7864320 * a__1_0 - (245760 * b__0_0 + 62914560 * b__1_0), 3] -mult=is_valid * 1, args=[120 * a__0_0 + 30720 * a__1_0 + 7864320 * a__2_0 - (960 * b__0_0 + 245760 * b__1_0 + 62914560 * b__2_0), 3] -mult=is_valid * 1, args=[120 * a__1_0 + 30720 * a__2_0 + 7864320 * a__3_0 - (943718400 * a__0_0 + 503316484 * b__0_0 + 960 * b__1_0 + 245760 * b__2_0 + 62914560 * b__3_0), 3] mult=is_valid * 1, args=[reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0, 17] mult=is_valid * 1, args=[15360 * reads_aux__0__base__prev_timestamp_0 + 15360 * reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 + 15360 - 15360 * from_state__timestamp_0, 12] mult=is_valid * 1, args=[writes_aux__base__timestamp_lt_aux__lower_decomp__0_0, 17] mult=is_valid * 1, args=[15360 * writes_aux__base__prev_timestamp_0 + 15360 * writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 - (15360 * from_state__timestamp_0 + 15360), 12] // Bus 6 (OPENVM_BITWISE_LOOKUP): +mult=is_valid * 1, args=[251658240 * a__0_0 + b__0_0, 983040 * a__0_0 + 251658240 * a__1_0 + b__1_0 - 7864320 * b__0_0, 0, 0] +mult=is_valid * 1, args=[3840 * a__0_0 + 983040 * a__1_0 + 251658240 * a__2_0 + b__2_0 - (30720 * b__0_0 + 7864320 * b__1_0), 15 * a__0_0 + 3840 * a__1_0 + 983040 * a__2_0 + 251658240 * a__3_0 + b__3_0 - (120 * b__0_0 + 30720 * b__1_0 + 7864320 * b__2_0), 0, 0] mult=is_valid * 1, args=[a__0_0, a__1_0, 0, 0] mult=is_valid * 1, args=[a__2_0, a__3_0, 0, 0] diff --git a/openvm/tests/apc_builder_outputs/single_sra.txt b/openvm/tests/apc_builder_outputs/single_sra.txt index fa1d7ad4b..a2e0da57a 100644 --- a/openvm/tests/apc_builder_outputs/single_sra.txt +++ b/openvm/tests/apc_builder_outputs/single_sra.txt @@ -61,7 +61,6 @@ mult=is_valid * -1, args=[1, 68, writes_aux__prev_data__0_0, writes_aux__prev_da mult=is_valid * 1, args=[1, 68, a__0_0, a__1_0, a__2_0, a__3_0, from_state__timestamp_0 + 2] // Bus 3 (VARIABLE_RANGE_CHECKER): -mult=is_valid * 1, args=[503316481 * limb_shift_marker__0_0 - (62914560 * c__0_0 + 440401920 * bit_shift_marker__0_0 + 377487360 * bit_shift_marker__1_0 + 314572800 * bit_shift_marker__2_0 + 251658240 * bit_shift_marker__3_0 + 188743680 * bit_shift_marker__4_0 + 125829120 * bit_shift_marker__5_0 + 62914560 * bit_shift_marker__6_0 + 1006632960 * limb_shift_marker__1_0 + 503316480 * limb_shift_marker__2_0 + 62914561), 3] mult=is_valid * 1, args=[bit_shift_carry__0_0, 7 - (7 * bit_shift_marker__0_0 + 6 * bit_shift_marker__1_0 + 5 * bit_shift_marker__2_0 + 4 * bit_shift_marker__3_0 + 3 * bit_shift_marker__4_0 + 2 * bit_shift_marker__5_0 + bit_shift_marker__6_0)] mult=is_valid * 1, args=[bit_shift_carry__1_0, 7 - (7 * bit_shift_marker__0_0 + 6 * bit_shift_marker__1_0 + 5 * bit_shift_marker__2_0 + 4 * bit_shift_marker__3_0 + 3 * bit_shift_marker__4_0 + 2 * bit_shift_marker__5_0 + bit_shift_marker__6_0)] mult=is_valid * 1, args=[bit_shift_carry__2_0, 7 - (7 * bit_shift_marker__0_0 + 6 * bit_shift_marker__1_0 + 5 * bit_shift_marker__2_0 + 4 * bit_shift_marker__3_0 + 3 * bit_shift_marker__4_0 + 2 * bit_shift_marker__5_0 + bit_shift_marker__6_0)] @@ -75,8 +74,9 @@ mult=is_valid * 1, args=[15360 * writes_aux__base__prev_timestamp_0 + 15360 * wr // Bus 6 (OPENVM_BITWISE_LOOKUP): mult=is_valid * 1, args=[b__3_0, 128, b__3_0 + 128 - 256 * b_sign_0, 1] -mult=is_valid * 1, args=[a__0_0, a__1_0, 0, 0] -mult=is_valid * 1, args=[a__2_0, a__3_0, 0, 0] +mult=is_valid * 1, args=[c__0_0 + 7 * bit_shift_marker__0_0 + 6 * bit_shift_marker__1_0 + 5 * bit_shift_marker__2_0 + 4 * bit_shift_marker__3_0 + 3 * bit_shift_marker__4_0 + 2 * bit_shift_marker__5_0 + bit_shift_marker__6_0 + 24 * limb_shift_marker__0_0 + 16 * limb_shift_marker__1_0 + 8 * limb_shift_marker__2_0 - 31, a__0_0, 0, 0] +mult=is_valid * 1, args=[a__1_0, a__2_0, 0, 0] +mult=is_valid * 1, args=[a__3_0, 0, 0, 0] // Algebraic constraints: bit_shift_marker__0_0 * (bit_shift_marker__0_0 - 1) = 0 diff --git a/openvm/tests/apc_builder_outputs/single_srl.txt b/openvm/tests/apc_builder_outputs/single_srl.txt index 6d60be8e5..99cc81426 100644 --- a/openvm/tests/apc_builder_outputs/single_srl.txt +++ b/openvm/tests/apc_builder_outputs/single_srl.txt @@ -3,8 +3,8 @@ Instructions: APC advantage: - Main columns: 53 -> 15 (3.53x reduction) - - Bus interactions: 24 -> 12 (2.00x reduction) - - Constraints: 76 -> 1 (76.00x reduction) + - Bus interactions: 24 -> 11 (2.18x reduction) + - Constraints: 76 -> 2 (38.00x reduction) Symbolic machine using 15 unique main columns: from_state__timestamp_0 @@ -34,7 +34,6 @@ mult=is_valid * -1, args=[1, 68, writes_aux__prev_data__0_0, writes_aux__prev_da mult=is_valid * 1, args=[1, 68, a__0_0, 0, 0, 0, from_state__timestamp_0 + 2] // Bus 3 (VARIABLE_RANGE_CHECKER): -mult=is_valid * 1, args=[b__3_0 - 2 * a__0_0, 1] mult=is_valid * 1, args=[reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0, 17] mult=is_valid * 1, args=[15360 * reads_aux__0__base__prev_timestamp_0 + 15360 * reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 + 15360 - 15360 * from_state__timestamp_0, 12] mult=is_valid * 1, args=[writes_aux__base__timestamp_lt_aux__lower_decomp__0_0, 17] @@ -44,4 +43,5 @@ mult=is_valid * 1, args=[15360 * writes_aux__base__prev_timestamp_0 + 15360 * wr mult=is_valid * 1, args=[a__0_0, 0, 0, 0] // Algebraic constraints: +(b__3_0 - 2 * a__0_0) * (b__3_0 - (2 * a__0_0 + 1)) = 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 beb4edb1a..8c3ca1599 100644 --- a/openvm/tests/optimizer.rs +++ b/openvm/tests/optimizer.rs @@ -59,6 +59,6 @@ fn test_optimize() { machine.bus_interactions.len(), machine.constraints.len() ], - [2007, 1780, 165] + [2007, 1611, 233] ); }