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

Refactor QuadraticSymbolicExpression (#2923)

Browse Source 
This PR refactors `QuadraticSymbolicExpression`: I removed the reference
to
[`SymbolicExpression`](f60e9d9f69/constraint-solver/src/quadratic_symbolic_expression.rs (L70)).
It can represent values that are known at runtime, represented as an
expression. We don't need this in the context of APC: Variables are
either unknown or known at compile time, and therefore can be
represented as a `FieldElement` instead.

The idea is to introduce [this
trait](4989be08f3/constraint-solver/src/runtime_constant.rs (L11)),
which is implemented by `SymbolicExpression` and any `T: FieldElement`.
This way, we can continue to use the solver with
`QuadraticSymbolicExpression<SymbolicExpression<T, V>, V>` (equivalent
to the current `QuadraticSymbolicExpression<T, V>`) in the old JIT
pipeline and use the simpler `QuadraticSymbolicExpression<T, V>` in the
APC pipeline.

---------

Co-authored-by: chriseth <chriseth.github@gmail.com>
This commit is contained in:
Georg Wiese
2025-06-30 17:47:12 +02:00
committed by GitHub
parent 33979e5583
commit a22065ee2d
34 changed files with 734 additions and 458 deletions
Download Patch File Download Diff File Expand all files Collapse all files

31
ast/src/analyzed/algebraic_expression_conversion.rs
View File

@@ -1,3 +1,4 @@
use num_traits::One;
use powdr_number::{FieldElement, LargeInt};
use super::{
@@ -5,7 +6,8 @@ use super::{
AlgebraicUnaryOperation, AlgebraicUnaryOperator, Challenge,
};
pub trait TerminalConverter<Target> {
pub trait TerminalConverter<T, Target> {
fn convert_number(&mut self, number: &T) -> Target;
fn convert_reference(&mut self, reference: &AlgebraicReference) -> Target;
fn convert_public_reference(&mut self, reference: &str) -> Target;
fn convert_challenge(&mut self, challenge: &Challenge) -> Target;
@@ -15,11 +17,11 @@ pub trait TerminalConverter<Target> {
/// The `terminal_converter` is used to convert the terminal nodes of the expression.
pub fn convert<T: FieldElement, Target>(
expr: &AlgebraicExpression<T>,
terminal_converter: &mut impl TerminalConverter<Target>,
terminal_converter: &mut impl TerminalConverter<T, Target>,
) -> Target
where
Target: From<T>
+ Clone
Target: Clone
+ One
+ std::ops::Add<Output = Target>
+ std::ops::Sub<Output = Target>
+ std::ops::Mul<Output = Target>
@@ -29,7 +31,7 @@ where
AlgebraicExpression::Reference(r) => terminal_converter.convert_reference(r),
AlgebraicExpression::PublicReference(r) => terminal_converter.convert_public_reference(r),
AlgebraicExpression::Challenge(c) => terminal_converter.convert_challenge(c),
AlgebraicExpression::Number(n) => (*n).into(),
AlgebraicExpression::Number(n) => terminal_converter.convert_number(n),
AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { left, op, right }) => {
if *op == AlgebraicBinaryOperator::Pow {
let AlgebraicExpression::Number(exponent) = right.as_ref() else {
@@ -62,13 +64,12 @@ where
}
}
fn apply_pow<T, Target>(v: &Target, exponent: u32) -> Target
fn apply_pow<Target>(v: &Target, exponent: u32) -> Target
where
T: From<u64>,
Target: From<T> + Clone + std::ops::Mul<Output = Target>,
Target: Clone + One + std::ops::Mul<Output = Target>,
{
if exponent == 0 {
Target::from(T::from(1))
Target::one()
} else if exponent & 1 == 1 {
let r: Target = apply_pow(v, exponent >> 1);
(r.clone() * r) * v.clone()
@@ -85,11 +86,11 @@ mod test {
#[test]
fn test_apply_pow() {
let v = 9u64;
assert_eq!(apply_pow::<u64, _>(&v, 0), 1);
assert_eq!(apply_pow::<u64, _>(&v, 1), 9);
assert_eq!(apply_pow::<u64, _>(&v, 2), 9 * 9);
assert_eq!(apply_pow::<u64, _>(&v, 3), 9 * 9 * 9);
assert_eq!(apply_pow::<u64, _>(&v, 4), 9 * 9 * 9 * 9);
assert_eq!(apply_pow::<u64, _>(&v, 5), 9 * 9 * 9 * 9 * 9);
assert_eq!(apply_pow::<u64>(&v, 0), 1);
assert_eq!(apply_pow::<u64>(&v, 1), 9);
assert_eq!(apply_pow::<u64>(&v, 2), 9 * 9);
assert_eq!(apply_pow::<u64>(&v, 3), 9 * 9 * 9);
assert_eq!(apply_pow::<u64>(&v, 4), 9 * 9 * 9 * 9);
assert_eq!(apply_pow::<u64>(&v, 5), 9 * 9 * 9 * 9 * 9);
}
}

1
autoprecompiles/Cargo.toml
View File

@@ -13,6 +13,7 @@ powdr-constraint-solver.workspace = true
itertools = "0.13"
log = "0.4.18"
num-traits = "0.2.15"
serde = "1.0.218"
[package.metadata.cargo-udeps.ignore]

19
autoprecompiles/src/bitwise_lookup_optimizer.rs
View File

@@ -3,6 +3,7 @@ use std::hash::Hash;
use std::{fmt::Debug, fmt::Display};
use itertools::Itertools;
use num_traits::{One, Zero};
use powdr_constraint_solver::constraint_system::{BusInteraction, ConstraintSystem};
use powdr_constraint_solver::quadratic_symbolic_expression::QuadraticSymbolicExpression;
use powdr_number::FieldElement;
@@ -40,14 +41,14 @@ pub fn optimize_bitwise_lookup<T: FieldElement, V: Hash + Eq + Clone + Ord + Deb
// The bus interaction is equivalent to "x and y are bytes and z = 0".
to_byte_constrain.extend([x.clone(), y.clone()]);
// If it is not zero, we could also add it as a new constraint.
assert!(z == &T::from(0).into());
assert!(z.is_zero());
false
} else if op == 1.into() {
// The bus interaction is equivalent to "x, y and z are bytes and z = x ^ y".
// If any argument is zero, the other two have to be equal.
let mut args = vec![x, y, z];
if let Some(zero_pos) = args.iter().position(|e| *e == &T::from(0).into()) {
if let Some(zero_pos) = args.iter().position(|e| e.is_zero()) {
args.remove(zero_pos);
// The two remaning expressions in args are equal and bytes.
let [a, b] = args.try_into().unwrap();
@@ -82,25 +83,25 @@ pub fn optimize_bitwise_lookup<T: FieldElement, V: Hash + Eq + Clone + Ord + Deb
.unique()
.collect_vec();
if to_byte_constrain.len() % 2 != 0 {
to_byte_constrain.push(T::from(0).into());
to_byte_constrain.push(Zero::zero());
}
for (x, y) in to_byte_constrain.into_iter().tuples() {
system.bus_interactions.push(BusInteraction {
bus_id: T::from(bitwise_lookup_bus_id).into(),
payload: vec![x.clone(), y.clone(), T::from(0).into(), T::from(0).into()],
multiplicity: T::from(1).into(),
bus_id: QuadraticSymbolicExpression::from_number(T::from(bitwise_lookup_bus_id)),
payload: vec![x.clone(), y.clone(), Zero::zero(), Zero::zero()],
multiplicity: One::one(),
});
}
system.algebraic_constraints.extend(new_constraints);
system
}
fn is_simple_multiplicity_bitwise_bus_interaction<T: FieldElement, V: Ord>(
fn is_simple_multiplicity_bitwise_bus_interaction<T: FieldElement, V: Clone + Hash + Eq + Ord>(
bus_int: &BusInteraction<QuadraticSymbolicExpression<T, V>>,
bitwise_lookup_bus_id: u64,
) -> bool {
bus_int.bus_id == T::from(bitwise_lookup_bus_id).into()
&& bus_int.multiplicity == T::from(1).into()
bus_int.bus_id == QuadraticSymbolicExpression::from_number(T::from(bitwise_lookup_bus_id))
&& bus_int.multiplicity.is_one()
}
/// Returns all expressions that are byte-constrained in the machine.

5
autoprecompiles/src/constraint_optimizer.rs
View File

@@ -1,6 +1,7 @@
use std::{collections::HashSet, fmt::Display, hash::Hash};
use inliner::DegreeBound;
use num_traits::Zero;
use powdr_constraint_solver::{
constraint_system::BusInteractionHandler, inliner,
journaling_constraint_system::JournalingConstraintSystem,
@@ -135,10 +136,10 @@ fn remove_disconnected_columns<T: FieldElement, V: Clone + Ord + Hash + Display>
constraint_system
}
fn remove_trivial_constraints<P: FieldElement, V: PartialEq>(
fn remove_trivial_constraints<P: FieldElement, V: PartialEq + Clone + Hash + Ord>(
mut constraint_system: JournalingConstraintSystem<P, V>,
) -> JournalingConstraintSystem<P, V> {
let zero = QuadraticSymbolicExpression::from(P::zero());
let zero = QuadraticSymbolicExpression::zero();
constraint_system.retain_algebraic_constraints(|constraint| constraint != &zero);
constraint_system
.retain_bus_interactions(|bus_interaction| bus_interaction.multiplicity != zero);

47
autoprecompiles/src/expression_conversion.rs
View File

@@ -1,12 +1,9 @@
use powdr_constraint_solver::{
quadratic_symbolic_expression::QuadraticSymbolicExpression,
symbolic_expression::{BinaryOperator, SymbolicExpression, UnaryOperator},
quadratic_symbolic_expression::QuadraticSymbolicExpression, runtime_constant::RuntimeConstant,
symbolic_expression::SymbolicExpression,
};
use powdr_expression::{
AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicUnaryOperation,
AlgebraicUnaryOperator,
};
use powdr_number::FieldElement;
use powdr_expression::{AlgebraicUnaryOperation, AlgebraicUnaryOperator};
use powdr_number::{ExpressionConvertible, FieldElement};
use crate::expression::{AlgebraicExpression, AlgebraicReference};
@@ -15,9 +12,10 @@ use crate::expression::{AlgebraicExpression, AlgebraicReference};
pub fn algebraic_to_quadratic_symbolic_expression<T: FieldElement>(
expr: &AlgebraicExpression<T>,
) -> QuadraticSymbolicExpression<T, AlgebraicReference> {
powdr_expression::conversion::convert(expr, &mut |reference| {
QuadraticSymbolicExpression::from_unknown_variable(reference.clone())
})
expr.to_expression(
&|n| QuadraticSymbolicExpression::from_number(*n),
&|reference| QuadraticSymbolicExpression::from_unknown_variable(reference.clone()),
)
}
/// Turns a quadratic symbolic expression back into an algebraic expression.
@@ -83,37 +81,16 @@ pub fn quadratic_symbolic_expression_to_algebraic<T: FieldElement>(
fn symbolic_expression_to_algebraic<T: FieldElement>(
e: &SymbolicExpression<T, AlgebraicReference>,
) -> AlgebraicExpression<T> {
match e {
SymbolicExpression::Concrete(v) => {
e.to_expression(
&|v| {
if v.is_in_lower_half() {
AlgebraicExpression::from(*v)
} else {
-AlgebraicExpression::from(-*v)
}
}
SymbolicExpression::Symbol(r, _) => AlgebraicExpression::Reference(r.clone()),
SymbolicExpression::BinaryOperation(left, op, right, _) => {
let left = Box::new(symbolic_expression_to_algebraic(left));
let right = Box::new(symbolic_expression_to_algebraic(right));
let op = symbolic_op_to_algebraic(*op);
AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { left, op, right })
}
SymbolicExpression::UnaryOperation(op, inner, _) => match op {
UnaryOperator::Neg => AlgebraicExpression::UnaryOperation(AlgebraicUnaryOperation {
expr: Box::new(symbolic_expression_to_algebraic(inner)),
op: AlgebraicUnaryOperator::Minus,
}),
},
}
}
fn symbolic_op_to_algebraic(op: BinaryOperator) -> AlgebraicBinaryOperator {
match op {
BinaryOperator::Add => AlgebraicBinaryOperator::Add,
BinaryOperator::Sub => AlgebraicBinaryOperator::Sub,
BinaryOperator::Mul => AlgebraicBinaryOperator::Mul,
BinaryOperator::Div => unreachable!(),
}
&|r| AlgebraicExpression::Reference(r.clone()),
)
}
/// If `e` is negated, returns the expression without negation and `true`,

4
autoprecompiles/src/memory_optimizer.rs
View File

@@ -39,7 +39,7 @@ pub fn optimize_memory<T: FieldElement, V: Hash + Eq + Clone + Ord + Display>(
// Check that the number of register memory bus interactions for each concrete address in the precompile is even.
// Assumption: all register memory bus interactions feature a concrete address.
pub fn check_register_operation_consistency<T: FieldElement, V: Clone + Ord + Display>(
pub fn check_register_operation_consistency<T: FieldElement, V: Clone + Ord + Display + Hash>(
system: &ConstraintSystem<T, V>,
memory_bus_id: u64,
) -> bool {
@@ -89,7 +89,7 @@ struct MemoryBusInteraction<T: FieldElement, V> {
timestamp: QuadraticSymbolicExpression<T, V>,
}
impl<T: FieldElement, V: Ord + Clone + Eq + Display> MemoryBusInteraction<T, V> {
impl<T: FieldElement, V: Ord + Clone + Eq + Display + Hash> MemoryBusInteraction<T, V> {
/// Tries to convert a `BusInteraction` to a `MemoryBusInteraction`.
///
/// Returns `Ok(None)` if we know that the bus interaction is not a memory bus interaction.

3
autoprecompiles/src/optimizer.rs
View File

@@ -4,7 +4,6 @@ use powdr_constraint_solver::{
constraint_system::{BusInteraction, BusInteractionHandler, ConstraintSystem},
journaling_constraint_system::JournalingConstraintSystem,
quadratic_symbolic_expression::{NoRangeConstraints, QuadraticSymbolicExpression},
symbolic_expression::SymbolicExpression,
};
use powdr_number::FieldElement;
@@ -249,7 +248,7 @@ fn symbolic_bus_interaction_to_bus_interaction<P: FieldElement>(
bus_interaction: &SymbolicBusInteraction<P>,
) -> BusInteraction<QuadraticSymbolicExpression<P, AlgebraicReference>> {
BusInteraction {
bus_id: SymbolicExpression::Concrete(P::from(bus_interaction.id)).into(),
bus_id: QuadraticSymbolicExpression::from_number(P::from(bus_interaction.id)),
payload: bus_interaction
.args
.iter()

3
constraint-solver/src/constraint_system.rs
View File

@@ -2,6 +2,7 @@ use crate::{
effect::Effect,
quadratic_symbolic_expression::{QuadraticSymbolicExpression, RangeConstraintProvider},
range_constraint::RangeConstraint,
runtime_constant::RuntimeConstant,
};
use itertools::Itertools;
use powdr_number::FieldElement;
@@ -17,7 +18,7 @@ pub struct ConstraintSystem<T: FieldElement, V> {
pub bus_interactions: Vec<BusInteraction<QuadraticSymbolicExpression<T, V>>>,
}
impl<T: FieldElement, V: Clone + Ord + Display> Display for ConstraintSystem<T, V> {
impl<T: FieldElement, V: Clone + Ord + Display + Hash> Display for ConstraintSystem<T, V> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(
f,

64
constraint-solver/src/effect.rs
View File

@@ -3,28 +3,35 @@ use std::fmt::{self, Display, Formatter};
use itertools::Itertools;
use powdr_number::FieldElement;
use crate::{range_constraint::RangeConstraint, symbolic_expression::SymbolicExpression};
use crate::{
range_constraint::RangeConstraint, runtime_constant::RuntimeConstant,
symbolic_expression::SymbolicExpression,
};
/// The effect of solving a symbolic equation.
#[derive(Clone, PartialEq, Eq)]
pub enum Effect<T: FieldElement, V> {
pub enum EffectImpl<T: RuntimeConstant, V> {
/// Variable can be assigned a value.
Assignment(V, SymbolicExpression<T, V>),
Assignment(V, T),
/// Perform a bit decomposition of a known value, and assign multiple variables.
BitDecomposition(BitDecomposition<T, V>),
/// We learnt a new range constraint on variable.
RangeConstraint(V, RangeConstraint<T>),
RangeConstraint(V, RangeConstraint<T::FieldType>),
/// A run-time assertion. If this fails, we have conflicting constraints.
Assertion(Assertion<T, V>),
Assertion(Assertion<T>),
/// A variable is assigned one of two alternative expressions, depending on a condition.
ConditionalAssignment {
variable: V,
condition: Condition<T, V>,
in_range_value: SymbolicExpression<T, V>,
out_of_range_value: SymbolicExpression<T, V>,
condition: Condition<T>,
in_range_value: T,
out_of_range_value: T,
},
}
// TODO: This type is equivalent to a pre-refactoring version of `EffectImpl`.
// It should be removed in a follow-up PR & we should rename `EffectImpl` to `Effect`.
pub type Effect<T, V> = EffectImpl<SymbolicExpression<T, V>, V>;
/// A bit decomposition of a value.
/// Executing this effect solves the following equation:
/// value = sum_{i=0}^{components.len() - 1} (-1)**components[i].negative * 2**components[i].exponent * components[i].variable
@@ -32,14 +39,14 @@ pub enum Effect<T: FieldElement, V> {
/// This effect can only be created if the equation has a unique solution.
/// It might be that it leads to a contradiction, which should result in an assertion failure.
#[derive(Clone, PartialEq, Eq)]
pub struct BitDecomposition<T: FieldElement, V> {
pub struct BitDecomposition<T: RuntimeConstant, V> {
/// The value that is decomposed.
pub value: SymbolicExpression<T, V>,
pub value: T,
/// The components of the decomposition.
pub components: Vec<BitDecompositionComponent<T, V>>,
pub components: Vec<BitDecompositionComponent<T::FieldType, V>>,
}
impl<T: FieldElement, V: Display> Display for BitDecomposition<T, V> {
impl<T: RuntimeConstant + Display, V: Display> Display for BitDecomposition<T, V> {
fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
let BitDecomposition { value, components } = self;
write!(f, "{} := {value};", components.iter().format(" + "))
@@ -81,33 +88,30 @@ impl<T: FieldElement, V: Display> Display for BitDecompositionComponent<T, V> {
/// A run-time assertion. If this fails, we have conflicting constraints.
#[derive(Clone, PartialEq, Eq)]
pub struct Assertion<T: FieldElement, V> {
pub lhs: SymbolicExpression<T, V>,
pub rhs: SymbolicExpression<T, V>,
pub struct Assertion<T: RuntimeConstant> {
pub lhs: T,
pub rhs: T,
/// If this is true, we assert that both sides are equal.
/// Otherwise, we assert that they are different.
pub expected_equal: bool,
}
impl<T: FieldElement, V> Assertion<T, V> {
pub fn assert_is_zero(condition: SymbolicExpression<T, V>) -> Effect<T, V> {
Self::assert_eq(condition, SymbolicExpression::from(T::from(0)))
impl<T: RuntimeConstant> Assertion<T> {
pub fn assert_is_zero<V>(condition: T) -> EffectImpl<T, V> {
Self::assert_eq(condition, T::from_u64(0))
}
pub fn assert_is_nonzero(condition: SymbolicExpression<T, V>) -> Effect<T, V> {
Self::assert_neq(condition, SymbolicExpression::from(T::from(0)))
pub fn assert_is_nonzero<V>(condition: T) -> EffectImpl<T, V> {
Self::assert_neq(condition, T::from_u64(0))
}
pub fn assert_eq(lhs: SymbolicExpression<T, V>, rhs: SymbolicExpression<T, V>) -> Effect<T, V> {
Effect::Assertion(Assertion {
pub fn assert_eq<V>(lhs: T, rhs: T) -> EffectImpl<T, V> {
EffectImpl::Assertion(Assertion {
lhs,
rhs,
expected_equal: true,
})
}
pub fn assert_neq(
lhs: SymbolicExpression<T, V>,
rhs: SymbolicExpression<T, V>,
) -> Effect<T, V> {
Effect::Assertion(Assertion {
pub fn assert_neq<V>(lhs: T, rhs: T) -> EffectImpl<T, V> {
EffectImpl::Assertion(Assertion {
lhs,
rhs,
expected_equal: false,
@@ -116,7 +120,7 @@ impl<T: FieldElement, V> Assertion<T, V> {
}
#[derive(Clone, PartialEq, Eq)]
pub struct Condition<T: FieldElement, V> {
pub value: SymbolicExpression<T, V>,
pub condition: RangeConstraint<T>,
pub struct Condition<T: RuntimeConstant> {
pub value: T,
pub condition: RangeConstraint<T::FieldType>,
}

7
constraint-solver/src/indexed_constraint_system.rs
View File

@@ -241,7 +241,7 @@ impl<T: FieldElement, V: Clone + Hash + Ord + Eq> IndexedConstraintSystem<T, V>
) {
let bus_interaction = &mut self.constraint_system.bus_interactions[interaction_index];
let field = bus_interaction.fields_mut().nth(field_index).unwrap();
*field = value.into();
*field = QuadraticSymbolicExpression::from_number(value);
}
/// Substitute an unknown variable by a QuadraticSymbolicExpression in the whole system.
@@ -417,7 +417,7 @@ fn substitute_by_unknown_in_item<T: FieldElement, V: Ord + Clone + Hash + Eq>(
}
}
impl<T: FieldElement, V: Clone + Ord + Display> Display for IndexedConstraintSystem<T, V> {
impl<T: FieldElement, V: Clone + Ord + Display + Hash> Display for IndexedConstraintSystem<T, V> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "{}", self.constraint_system)
}
@@ -475,8 +475,7 @@ mod tests {
s.substitute_by_unknown(
&"z",
&(Qse::from_unknown_variable("x")
+ Qse::from(SymbolicExpression::from(GoldilocksField::from(7)))),
&(Qse::from_unknown_variable("x") + Qse::from_number(GoldilocksField::from(7))),
);
assert_eq!(

4
constraint-solver/src/journaling_constraint_system.rs
View File

@@ -103,7 +103,9 @@ impl<T: FieldElement, V> JournalingConstraintSystem<T, V> {
}
}
impl<T: FieldElement, V: Clone + Ord + Display> Display for JournalingConstraintSystem<T, V> {
impl<T: FieldElement, V: Clone + Ord + Display + Hash> Display
for JournalingConstraintSystem<T, V>
{
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "{}", self.system)
}

1
constraint-solver/src/lib.rs
View File

@@ -8,6 +8,7 @@ pub mod inliner;
pub mod journaling_constraint_system;
pub mod quadratic_symbolic_expression;
pub mod range_constraint;
pub mod runtime_constant;
pub mod solver;
pub mod symbolic_expression;
pub mod symbolic_to_quadratic;

412
constraint-solver/src/quadratic_symbolic_expression.rs
View File

@@ -5,32 +5,33 @@ use std::{
ops::{Add, AddAssign, Mul, MulAssign, Neg, Sub},
};
use itertools::Itertools;
use num_traits::Zero;
use powdr_number::{log2_exact, FieldElement, LargeInt};
use crate::{
effect::Condition, symbolic_to_quadratic::symbolic_expression_to_quadratic_symbolic_expression,
effect::Condition,
runtime_constant::{ReferencedSymbols, RuntimeConstant, Substitutable},
};
use itertools::Itertools;
use num_traits::One;
use num_traits::Zero;
use powdr_number::{log2_exact, ExpressionConvertible, FieldElement, LargeInt};
use super::effect::{Assertion, BitDecomposition, BitDecompositionComponent, Effect};
use super::effect::{Assertion, BitDecomposition, BitDecompositionComponent, EffectImpl};
use super::range_constraint::RangeConstraint;
use super::symbolic_expression::SymbolicExpression;
#[derive(Default)]
pub struct ProcessResult<T: FieldElement, V> {
pub effects: Vec<Effect<T, V>>,
pub struct ProcessResult<T: RuntimeConstant, V> {
pub effects: Vec<EffectImpl<T, V>>,
pub complete: bool,
}
impl<T: FieldElement, V> ProcessResult<T, V> {
impl<T: RuntimeConstant, V> ProcessResult<T, V> {
pub fn empty() -> Self {
Self {
effects: vec![],
complete: false,
}
}
pub fn complete(effects: Vec<Effect<T, V>>) -> Self {
pub fn complete(effects: Vec<EffectImpl<T, V>>) -> Self {
Self {
effects,
complete: true,
@@ -58,49 +59,90 @@ pub enum Error {
/// an unknown variable gets known and provides functions to solve
/// (some kinds of) equations.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct QuadraticSymbolicExpression<T: FieldElement, V> {
pub struct QuadraticSymbolicExpressionImpl<T, V> {
/// Quadratic terms of the form `a * X * Y`, where `a` is a (symbolically)
/// known value and `X` and `Y` are quadratic symbolic expressions that
/// have at least one unknown.
quadratic: Vec<(Self, Self)>,
/// Linear terms of the form `a * X`, where `a` is a (symbolically) known
/// value and `X` is an unknown variable.
linear: BTreeMap<V, SymbolicExpression<T, V>>,
linear: BTreeMap<V, T>,
/// Constant term, a (symbolically) known value.
constant: SymbolicExpression<T, V>,
constant: T,
}
impl<T: FieldElement, V> From<SymbolicExpression<T, V>> for QuadraticSymbolicExpression<T, V> {
fn from(k: SymbolicExpression<T, V>) -> Self {
// TODO: This type is equivalent to a pre-refactoring version of `QuadraticSymbolicExpressionImpl`.
// It should be removed in a follow-up PR & we should rename `QuadraticSymbolicExpressionImpl` to `QuadraticSymbolicExpression`.
pub type QuadraticSymbolicExpression<T, V> =
QuadraticSymbolicExpressionImpl<SymbolicExpression<T, V>, V>;
impl<F: FieldElement, T: RuntimeConstant<FieldType = F>, V> QuadraticSymbolicExpressionImpl<T, V> {
pub fn from_number(k: F) -> Self {
Self {
quadratic: Default::default(),
linear: Default::default(),
constant: k,
constant: T::from(k),
}
}
}
impl<T: FieldElement, V> From<T> for QuadraticSymbolicExpression<T, V> {
fn from(k: T) -> Self {
SymbolicExpression::from(k).into()
impl<T: RuntimeConstant, V: Clone + Ord + Eq + Hash> Zero
for QuadraticSymbolicExpressionImpl<T, V>
{
fn zero() -> Self {
Self {
quadratic: Default::default(),
linear: Default::default(),
constant: T::zero(),
}
}
fn is_zero(&self) -> bool {
self.try_to_known().is_some_and(|k| k.is_known_zero())
}
}
impl<T: FieldElement, V: Ord + Clone + Eq> QuadraticSymbolicExpression<T, V> {
pub fn from_known_symbol(symbol: V, rc: RangeConstraint<T>) -> Self {
SymbolicExpression::from_symbol(symbol, rc).into()
impl<T: RuntimeConstant, V: Clone + Ord + Eq + Hash> One for QuadraticSymbolicExpressionImpl<T, V> {
fn one() -> Self {
Self {
quadratic: Default::default(),
linear: Default::default(),
constant: T::one(),
}
}
fn is_one(&self) -> bool {
self.try_to_known().is_some_and(|k| k.is_known_one())
}
}
impl<F: FieldElement, V: Ord + Clone + Eq + Hash>
QuadraticSymbolicExpressionImpl<SymbolicExpression<F, V>, V>
{
pub fn from_known_symbol(symbol: V, rc: RangeConstraint<F>) -> Self {
Self::from_runtime_constant(SymbolicExpression::from_symbol(symbol, rc))
}
}
impl<T: RuntimeConstant, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpressionImpl<T, V> {
pub fn from_runtime_constant(constant: T) -> Self {
Self {
quadratic: Default::default(),
linear: Default::default(),
constant,
}
}
pub fn from_unknown_variable(var: V) -> Self {
Self {
quadratic: Default::default(),
linear: [(var.clone(), T::from(1).into())].into_iter().collect(),
constant: T::from(0).into(),
linear: [(var.clone(), T::one())].into_iter().collect(),
constant: T::zero(),
}
}
/// If this expression does not contain unknown variables, returns the symbolic expression.
pub fn try_to_known(&self) -> Option<&SymbolicExpression<T, V>> {
pub fn try_to_known(&self) -> Option<&T> {
if self.quadratic.is_empty() && self.linear.is_empty() {
Some(&self.constant)
} else {
@@ -114,7 +156,7 @@ impl<T: FieldElement, V: Ord + Clone + Eq> QuadraticSymbolicExpression<T, V> {
}
/// If the expression is a known number, returns it.
pub fn try_to_number(&self) -> Option<T> {
pub fn try_to_number(&self) -> Option<T::FieldType> {
self.try_to_known()?.try_to_number()
}
@@ -150,20 +192,13 @@ impl<T: FieldElement, V: Ord + Clone + Eq> QuadraticSymbolicExpression<T, V> {
}
/// Returns the quadratic, linear and constant components of this expression.
#[allow(clippy::type_complexity)]
pub fn components(
&self,
) -> (
&[(Self, Self)],
impl Iterator<Item = (&V, &SymbolicExpression<T, V>)>,
&SymbolicExpression<T, V>,
) {
pub fn components(&self) -> (&[(Self, Self)], impl Iterator<Item = (&V, &T)>, &T) {
(&self.quadratic, self.linear.iter(), &self.constant)
}
/// Returns the coefficient of the variable `variable` if this is an affine expression.
/// Panics if the expression is quadratic.
pub fn coefficient_of_variable(&self, var: &V) -> Option<&SymbolicExpression<T, V>> {
pub fn coefficient_of_variable(&self, var: &V) -> Option<&T> {
assert!(!self.is_quadratic());
self.linear.get(var)
}
@@ -171,8 +206,8 @@ impl<T: FieldElement, V: Ord + Clone + Eq> QuadraticSymbolicExpression<T, V> {
/// Returns the range constraint of the full expression.
pub fn range_constraint(
&self,
range_constraints: &impl RangeConstraintProvider<T, V>,
) -> RangeConstraint<T> {
range_constraints: &impl RangeConstraintProvider<T::FieldType, V>,
) -> RangeConstraint<T::FieldType> {
self.quadratic
.iter()
.map(|(l, r)| {
@@ -190,10 +225,12 @@ impl<T: FieldElement, V: Ord + Clone + Eq> QuadraticSymbolicExpression<T, V> {
}
}
impl<T: FieldElement, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpression<T, V> {
impl<T: RuntimeConstant + Substitutable<V>, V: Ord + Clone + Eq + Hash>
QuadraticSymbolicExpressionImpl<T, V>
{
/// 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.
pub fn substitute_by_known(&mut self, variable: &V, substitution: &SymbolicExpression<T, V>) {
pub fn substitute_by_known(&mut self, variable: &V, substitution: &T) {
self.constant.substitute(variable, substitution);
if self.linear.contains_key(variable) {
@@ -202,7 +239,7 @@ impl<T: FieldElement, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpression<T,
// any symbolic expression.
// We replace the variable by a symbolic expression, so it goes into the constant part.
let coeff = self.linear.remove(variable).unwrap();
self.constant += &coeff * substitution;
self.constant += coeff * substitution.clone();
} else {
for coeff in self.linear.values_mut() {
coeff.substitute(variable, substitution);
@@ -213,13 +250,15 @@ impl<T: FieldElement, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpression<T,
// TODO can we do that without moving everything?
// In the end, the order does not matter much.
let mut to_add = QuadraticSymbolicExpression::from(T::zero());
let mut to_add = QuadraticSymbolicExpressionImpl::zero();
self.quadratic.retain_mut(|(l, r)| {
l.substitute_by_known(variable, substitution);
r.substitute_by_known(variable, substitution);
match (l.try_to_known(), r.try_to_known()) {
(Some(l), Some(r)) => {
to_add += (l * r).into();
to_add += QuadraticSymbolicExpressionImpl::from_runtime_constant(
l.clone() * r.clone(),
);
false
}
(Some(l), None) => {
@@ -245,13 +284,13 @@ impl<T: FieldElement, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpression<T,
pub fn substitute_by_unknown(
&mut self,
variable: &V,
substitution: &QuadraticSymbolicExpression<T, V>,
substitution: &QuadraticSymbolicExpressionImpl<T, V>,
) {
if !self.referenced_unknown_variables().any(|v| v == variable) {
return;
}
let mut to_add = QuadraticSymbolicExpression::from(T::zero());
let mut to_add = QuadraticSymbolicExpressionImpl::zero();
for (var, coeff) in std::mem::take(&mut self.linear) {
if var == *variable {
to_add += substitution.clone() * coeff;
@@ -267,7 +306,7 @@ impl<T: FieldElement, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpression<T,
r.substitute_by_unknown(variable, substitution);
match (l.try_to_known(), r.try_to_known()) {
(Some(lval), Some(rval)) => {
to_add += (lval * rval).into();
to_add += Self::from_runtime_constant(lval.clone() * rval.clone());
None
}
(Some(lval), None) => {
@@ -285,7 +324,11 @@ impl<T: FieldElement, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpression<T,
*self += to_add;
}
}
impl<T: RuntimeConstant + ReferencedSymbols<V>, V: Ord + Clone + Eq + Hash>
QuadraticSymbolicExpressionImpl<T, V>
{
/// Returns the set of referenced variables, both know and unknown. Might contain repetitions.
pub fn referenced_variables(&self) -> Box<dyn Iterator<Item = &V> + '_> {
let quadr = self
@@ -300,7 +343,9 @@ impl<T: FieldElement, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpression<T,
let constant = self.constant.referenced_symbols();
Box::new(quadr.chain(linear).chain(constant))
}
}
impl<T, V> QuadraticSymbolicExpressionImpl<T, V> {
/// Returns the referenced unknown variables. Might contain repetitions.
pub fn referenced_unknown_variables(&self) -> Box<dyn Iterator<Item = &V> + '_> {
let quadratic = self.quadratic.iter().flat_map(|(a, b)| {
@@ -311,12 +356,14 @@ impl<T: FieldElement, V: Ord + Clone + Eq + Hash> QuadraticSymbolicExpression<T,
}
}
impl<T: FieldElement, V1: Ord + Clone> QuadraticSymbolicExpression<T, V1> {
impl<T: FieldElement, V1: Ord + Clone>
QuadraticSymbolicExpressionImpl<SymbolicExpression<T, V1>, V1>
{
pub fn transform_var_type<V2: Ord + Clone>(
&self,
var_transform: &mut impl FnMut(&V1) -> V2,
) -> QuadraticSymbolicExpression<T, V2> {
QuadraticSymbolicExpression {
) -> QuadraticSymbolicExpressionImpl<SymbolicExpression<T, V2>, V2> {
QuadraticSymbolicExpressionImpl {
quadratic: self
.quadratic
.iter()
@@ -352,7 +399,11 @@ impl<T: FieldElement, V> RangeConstraintProvider<T, V> for NoRangeConstraints {
}
}
impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExpression<T, V> {
impl<
T: RuntimeConstant + Display + ExpressionConvertible<<T as RuntimeConstant>::FieldType, V>,
V: Ord + Clone + Hash + Eq + Display,
> QuadraticSymbolicExpressionImpl<T, V>
{
/// Solves the equation `self = 0` and returns how to compute the solution.
/// The solution can contain assignments to multiple variables.
/// If no way to solve the equation (and no way to derive new range
@@ -361,7 +412,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
/// If the equation is known to be unsolvable, returns an error.
pub fn solve(
&self,
range_constraints: &impl RangeConstraintProvider<T, V>,
range_constraints: &impl RangeConstraintProvider<T::FieldType, V>,
) -> Result<ProcessResult<T, V>, Error> {
Ok(if self.is_quadratic() {
self.solve_quadratic(range_constraints)?
@@ -383,7 +434,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
/// has a coefficient which is known to be not zero.
///
/// Returns the resulting solved quadratic symbolic expression.
pub fn try_solve_for(&self, variable: &V) -> Option<QuadraticSymbolicExpression<T, V>> {
pub fn try_solve_for(&self, variable: &V) -> Option<QuadraticSymbolicExpressionImpl<T, V>> {
if self
.quadratic
.iter()
@@ -399,7 +450,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
}
let mut result = self.clone();
let coefficient = result.linear.remove(variable)?;
Some(result * (SymbolicExpression::from(-T::from(1)).field_div(&coefficient)))
Some(result * (-T::one().field_div(&coefficient)))
}
/// Algebraically transforms the constraint such that `self = 0` is equivalent
@@ -409,8 +460,8 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
/// Panics if `expr` is quadratic.
pub fn try_solve_for_expr(
&self,
expr: &QuadraticSymbolicExpression<T, V>,
) -> Option<QuadraticSymbolicExpression<T, V>> {
expr: &QuadraticSymbolicExpressionImpl<T, V>,
) -> Option<QuadraticSymbolicExpressionImpl<T, V>> {
assert!(
expr.is_affine(),
"Tried to solve for quadratic expression {expr}"
@@ -431,7 +482,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
None
}
})
.unwrap_or(T::from(1).into());
.unwrap_or(T::one());
let result = expr - &(self.clone() * normalization_factor);
// Check that the operations removed all variables in `expr` from `self`.
@@ -452,7 +503,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
fn solve_affine(
&self,
range_constraints: &impl RangeConstraintProvider<T, V>,
range_constraints: &impl RangeConstraintProvider<T::FieldType, V>,
) -> Result<ProcessResult<T, V>, Error> {
Ok(if self.linear.len() == 1 {
let (var, coeff) = self.linear.iter().next().unwrap();
@@ -463,7 +514,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
);
if coeff.is_known_nonzero() {
// In this case, we can always compute a solution.
let value = self.constant.field_div(&-coeff);
let value = self.constant.field_div(&-coeff.clone());
ProcessResult::complete(vec![assignment_if_satisfies_range_constraints(
var.clone(),
value,
@@ -472,7 +523,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
} else if self.constant.is_known_nonzero() {
// If the offset is not zero, then the coefficient must be non-zero,
// otherwise the constraint is violated.
let value = self.constant.field_div(&-coeff);
let value = self.constant.field_div(&-coeff.clone());
ProcessResult::complete(vec![
Assertion::assert_is_nonzero(coeff.clone()),
assignment_if_satisfies_range_constraints(
@@ -504,7 +555,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
/// Tries to solve a bit-decomposition equation.
fn solve_bit_decomposition(
&self,
range_constraints: &impl RangeConstraintProvider<T, V>,
range_constraints: &impl RangeConstraintProvider<T::FieldType, V>,
) -> Result<ProcessResult<T, V>, Error> {
assert!(!self.is_quadratic());
// All the coefficients need to be known numbers and the
@@ -537,8 +588,8 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
let mut concrete_assignments = vec![];
// Check if they are mutually exclusive and compute assignments.
let mut covered_bits: <T as FieldElement>::Integer = 0.into();
let mut components = vec![];
let mut covered_bits: <T::FieldType as FieldElement>::Integer = 0.into();
let mut components: Vec<BitDecompositionComponent<T::FieldType, V>> = vec![];
for (variable, constraint, is_negative, coeff_abs, exponent) in constrained_coefficients
.into_iter()
.sorted_by_key(|(_, _, _, _, exponent)| *exponent)
@@ -555,15 +606,17 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
// if it is not known, we return a BitDecomposition effect.
if let Some(offset) = &mut offset {
let mut component = if is_negative { -*offset } else { *offset }.to_integer();
if component > (T::modulus() - 1.into()) >> 1 {
if component > (T::FieldType::modulus() - 1.into()) >> 1 {
// Convert a signed finite field element into two's complement.
// a regular subtraction would underflow, so we do this.
// We add the difference between negative numbers in the field
// and negative numbers in two's complement.
component += T::Integer::MAX - T::modulus() + 1.into();
component += <T::FieldType as FieldElement>::Integer::MAX
- T::FieldType::modulus()
+ 1.into();
};
component &= bit_mask;
if component >= T::modulus() {
if component >= T::FieldType::modulus() {
// If the component does not fit the field, the bit mask is not
// tight good enough.
return Ok(ProcessResult::empty());
@@ -571,12 +624,15 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
concrete_assignments.push(
// We're not using assignment_if_satisfies_range_constraints here, because we
// might still exit early. The error case is handled below.
Effect::Assignment(variable.clone(), T::from(component >> exponent).into()),
EffectImpl::Assignment(
variable.clone(),
T::FieldType::from(component >> exponent).into(),
),
);
if is_negative {
*offset += T::from(component);
*offset += T::FieldType::from(component);
} else {
*offset -= T::from(component);
*offset -= T::FieldType::from(component);
}
} else {
components.push(BitDecompositionComponent {
@@ -588,7 +644,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
}
}
if covered_bits >= T::modulus() {
if covered_bits >= T::FieldType::modulus() {
return Ok(ProcessResult::empty());
}
@@ -599,7 +655,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
assert_eq!(concrete_assignments.len(), self.linear.len());
Ok(ProcessResult::complete(concrete_assignments))
} else {
Ok(ProcessResult::complete(vec![Effect::BitDecomposition(
Ok(ProcessResult::complete(vec![EffectImpl::BitDecomposition(
BitDecomposition {
value: self.constant.clone(),
components,
@@ -610,8 +666,8 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
fn transfer_constraints(
&self,
range_constraints: &impl RangeConstraintProvider<T, V>,
) -> Vec<Effect<T, V>> {
range_constraints: &impl RangeConstraintProvider<T::FieldType, V>,
) -> Vec<EffectImpl<T, V>> {
// Solve for each of the variables in the linear component and
// compute the range constraints.
assert!(!self.is_quadratic());
@@ -622,13 +678,13 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
Some((var, rc))
})
.filter(|(_, constraint)| !constraint.is_unconstrained())
.map(|(var, constraint)| Effect::RangeConstraint(var.clone(), constraint))
.map(|(var, constraint)| EffectImpl::RangeConstraint(var.clone(), constraint))
.collect()
}
fn solve_quadratic(
&self,
range_constraints: &impl RangeConstraintProvider<T, V>,
range_constraints: &impl RangeConstraintProvider<T::FieldType, V>,
) -> Result<ProcessResult<T, V>, Error> {
let Some((left, right)) = self.try_as_single_product() else {
return Ok(ProcessResult::empty());
@@ -663,15 +719,18 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> QuadraticSymbolicExp
/// Tries to combine two process results from alternative branches into a
/// conditional assignment.
fn combine_to_conditional_assignment<T: FieldElement, V: Ord + Clone + Hash + Eq + Display>(
fn combine_to_conditional_assignment<
T: RuntimeConstant + ExpressionConvertible<<T as RuntimeConstant>::FieldType, V>,
V: Ord + Clone + Hash + Eq + Display,
>(
left: &ProcessResult<T, V>,
right: &ProcessResult<T, V>,
range_constraints: &impl RangeConstraintProvider<T, V>,
range_constraints: &impl RangeConstraintProvider<T::FieldType, V>,
) -> Option<ProcessResult<T, V>> {
let [Effect::Assignment(first_var, first_assignment)] = left.effects.as_slice() else {
let [EffectImpl::Assignment(first_var, first_assignment)] = left.effects.as_slice() else {
return None;
};
let [Effect::Assignment(second_var, second_assignment)] = right.effects.as_slice() else {
let [EffectImpl::Assignment(second_var, second_assignment)] = right.effects.as_slice() else {
return None;
};
@@ -684,9 +743,13 @@ fn combine_to_conditional_assignment<T: FieldElement, V: Ord + Clone + Hash + Eq
// the same time (i.e. the "or" is exclusive), we can turn this into a
// conditional assignment.
let diff = symbolic_expression_to_quadratic_symbolic_expression(
&(first_assignment.clone() + -second_assignment.clone()),
let diff = first_assignment.clone() + -second_assignment.clone();
let diff: QuadraticSymbolicExpression<T::FieldType, V> = diff.try_to_expression(
&|n| QuadraticSymbolicExpression::from_number(*n),
&|v| QuadraticSymbolicExpressionImpl::from_unknown_variable(v.clone()),
&|e| e.try_to_number(),
)?;
let diff = diff.try_to_known()?.try_to_number()?;
// `diff = A - B` is a compile-time known number, i.e. `A = B + diff`.
// Now if `rc + diff` is disjoint from `rc`, it means
@@ -702,7 +765,7 @@ fn combine_to_conditional_assignment<T: FieldElement, V: Ord + Clone + Hash + Eq
}
Some(ProcessResult {
effects: vec![Effect::ConditionalAssignment {
effects: vec![EffectImpl::ConditionalAssignment {
variable: first_var.clone(),
condition: Condition {
value: first_assignment.clone(),
@@ -718,7 +781,7 @@ fn combine_to_conditional_assignment<T: FieldElement, V: Ord + Clone + Hash + Eq
/// Tries to combine range constraint results from two alternative branches.
/// In some cases, if both branches produce a complete range constraint for the same variable,
/// and those range constraints can be combined without loss, the result is complete as well.
fn combine_range_constraints<T: FieldElement, V: Ord + Clone + Hash + Eq + Display>(
fn combine_range_constraints<T: RuntimeConstant, V: Ord + Clone + Hash + Eq + Display>(
left: &ProcessResult<T, V>,
right: &ProcessResult<T, V>,
) -> ProcessResult<T, V> {
@@ -760,37 +823,37 @@ fn combine_range_constraints<T: FieldElement, V: Ord + Clone + Hash + Eq + Displ
ProcessResult {
effects: effects
.into_iter()
.map(|(v, rc, _)| Effect::RangeConstraint(v.clone(), rc))
.map(|(v, rc, _)| EffectImpl::RangeConstraint(v.clone(), rc))
.collect(),
complete,
}
}
fn assignment_if_satisfies_range_constraints<T: FieldElement, V: Ord + Clone + Hash + Eq>(
fn assignment_if_satisfies_range_constraints<T: RuntimeConstant, V: Ord + Clone + Hash + Eq>(
var: V,
value: SymbolicExpression<T, V>,
range_constraints: &impl RangeConstraintProvider<T, V>,
) -> Result<Effect<T, V>, Error> {
value: T,
range_constraints: &impl RangeConstraintProvider<T::FieldType, V>,
) -> Result<EffectImpl<T, V>, Error> {
let rc = range_constraints.get(&var);
if rc.is_disjoint(&value.range_constraint()) {
return Err(Error::ConflictingRangeConstraints);
}
Ok(Effect::Assignment(var, value))
Ok(EffectImpl::Assignment(var, value))
}
/// Turns an effect into a range constraint on a variable.
fn effect_to_range_constraint<T: FieldElement, V: Ord + Clone + Hash + Eq>(
effect: &Effect<T, V>,
) -> Option<(V, RangeConstraint<T>)> {
fn effect_to_range_constraint<T: RuntimeConstant, V: Ord + Clone + Hash + Eq>(
effect: &EffectImpl<T, V>,
) -> Option<(V, RangeConstraint<T::FieldType>)> {
match effect {
Effect::RangeConstraint(var, rc) => Some((var.clone(), rc.clone())),
Effect::Assignment(var, value) => Some((var.clone(), value.range_constraint())),
EffectImpl::RangeConstraint(var, rc) => Some((var.clone(), rc.clone())),
EffectImpl::Assignment(var, value) => Some((var.clone(), value.range_constraint())),
_ => None,
}
}
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Add for QuadraticSymbolicExpression<T, V> {
type Output = QuadraticSymbolicExpression<T, V>;
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq> Add for QuadraticSymbolicExpressionImpl<T, V> {
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn add(mut self, rhs: Self) -> Self {
self += rhs;
@@ -798,16 +861,18 @@ impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Add for QuadraticSymbolicExpre
}
}
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Add for &QuadraticSymbolicExpression<T, V> {
type Output = QuadraticSymbolicExpression<T, V>;
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq> Add
for &QuadraticSymbolicExpressionImpl<T, V>
{
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn add(self, rhs: Self) -> Self::Output {
self.clone() + rhs.clone()
}
}
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> AddAssign<QuadraticSymbolicExpression<T, V>>
for QuadraticSymbolicExpression<T, V>
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq>
AddAssign<QuadraticSymbolicExpressionImpl<T, V>> for QuadraticSymbolicExpressionImpl<T, V>
{
fn add_assign(&mut self, rhs: Self) {
self.quadratic.extend(rhs.quadratic);
@@ -822,23 +887,25 @@ impl<T: FieldElement, V: Clone + Ord + Hash + Eq> AddAssign<QuadraticSymbolicExp
}
}
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Sub for &QuadraticSymbolicExpression<T, V> {
type Output = QuadraticSymbolicExpression<T, V>;
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq> Sub
for &QuadraticSymbolicExpressionImpl<T, V>
{
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn sub(self, rhs: Self) -> Self::Output {
self + &-rhs
}
}
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Sub for QuadraticSymbolicExpression<T, V> {
type Output = QuadraticSymbolicExpression<T, V>;
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq> Sub for QuadraticSymbolicExpressionImpl<T, V> {
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn sub(self, rhs: Self) -> Self::Output {
&self - &rhs
}
}
impl<T: FieldElement, V: Clone + Ord> QuadraticSymbolicExpression<T, V> {
impl<T: RuntimeConstant, V: Clone + Ord> QuadraticSymbolicExpressionImpl<T, V> {
fn negate(&mut self) {
for (first, _) in &mut self.quadratic {
first.negate()
@@ -850,8 +917,8 @@ impl<T: FieldElement, V: Clone + Ord> QuadraticSymbolicExpression<T, V> {
}
}
impl<T: FieldElement, V: Clone + Ord> Neg for QuadraticSymbolicExpression<T, V> {
type Output = QuadraticSymbolicExpression<T, V>;
impl<T: RuntimeConstant, V: Clone + Ord> Neg for QuadraticSymbolicExpressionImpl<T, V> {
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn neg(mut self) -> Self {
self.negate();
@@ -859,8 +926,8 @@ impl<T: FieldElement, V: Clone + Ord> Neg for QuadraticSymbolicExpression<T, V>
}
}
impl<T: FieldElement, V: Clone + Ord> Neg for &QuadraticSymbolicExpression<T, V> {
type Output = QuadraticSymbolicExpression<T, V>;
impl<T: RuntimeConstant, V: Clone + Ord> Neg for &QuadraticSymbolicExpressionImpl<T, V> {
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn neg(self) -> Self::Output {
-((*self).clone())
@@ -868,33 +935,33 @@ impl<T: FieldElement, V: Clone + Ord> Neg for &QuadraticSymbolicExpression<T, V>
}
/// Multiply by known symbolic expression.
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Mul<&SymbolicExpression<T, V>>
for QuadraticSymbolicExpression<T, V>
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq> Mul<&T>
for QuadraticSymbolicExpressionImpl<T, V>
{
type Output = QuadraticSymbolicExpression<T, V>;
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn mul(mut self, rhs: &SymbolicExpression<T, V>) -> Self {
fn mul(mut self, rhs: &T) -> Self {
self *= rhs;
self
}
}
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Mul<SymbolicExpression<T, V>>
for QuadraticSymbolicExpression<T, V>
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq> Mul<T>
for QuadraticSymbolicExpressionImpl<T, V>
{
type Output = QuadraticSymbolicExpression<T, V>;
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn mul(self, rhs: SymbolicExpression<T, V>) -> Self {
fn mul(self, rhs: T) -> Self {
self * &rhs
}
}
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> MulAssign<&SymbolicExpression<T, V>>
for QuadraticSymbolicExpression<T, V>
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq> MulAssign<&T>
for QuadraticSymbolicExpressionImpl<T, V>
{
fn mul_assign(&mut self, rhs: &SymbolicExpression<T, V>) {
fn mul_assign(&mut self, rhs: &T) {
if rhs.is_known_zero() {
*self = T::zero().into();
*self = Self::zero();
} else {
for (first, _) in &mut self.quadratic {
*first *= rhs;
@@ -907,10 +974,10 @@ impl<T: FieldElement, V: Clone + Ord + Hash + Eq> MulAssign<&SymbolicExpression<
}
}
impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Mul for QuadraticSymbolicExpression<T, V> {
type Output = QuadraticSymbolicExpression<T, V>;
impl<T: RuntimeConstant, V: Clone + Ord + Hash + Eq> Mul for QuadraticSymbolicExpressionImpl<T, V> {
type Output = QuadraticSymbolicExpressionImpl<T, V>;
fn mul(self, rhs: QuadraticSymbolicExpression<T, V>) -> Self {
fn mul(self, rhs: QuadraticSymbolicExpressionImpl<T, V>) -> Self {
if let Some(k) = rhs.try_to_known() {
self * k
} else if let Some(k) = self.try_to_known() {
@@ -919,13 +986,15 @@ impl<T: FieldElement, V: Clone + Ord + Hash + Eq> Mul for QuadraticSymbolicExpre
Self {
quadratic: vec![(self, rhs)],
linear: Default::default(),
constant: T::from(0).into(),
constant: T::zero(),
}
}
}
}
impl<T: FieldElement, V: Clone + Ord + Display> Display for QuadraticSymbolicExpression<T, V> {
impl<T: RuntimeConstant + Display, V: Clone + Ord + Display> Display
for QuadraticSymbolicExpressionImpl<T, V>
{
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let (sign, s) = self.to_signed_string();
if sign {
@@ -936,7 +1005,7 @@ impl<T: FieldElement, V: Clone + Ord + Display> Display for QuadraticSymbolicExp
}
}
impl<T: FieldElement, V: Clone + Ord + Display> QuadraticSymbolicExpression<T, V> {
impl<T: RuntimeConstant + Display, V: Clone + Ord + Display> QuadraticSymbolicExpressionImpl<T, V> {
fn to_signed_string(&self) -> (bool, String) {
self.quadratic
.iter()
@@ -949,8 +1018,8 @@ impl<T: FieldElement, V: Clone + Ord + Display> QuadraticSymbolicExpression<T, V
self.linear
.iter()
.map(|(var, coeff)| match coeff.try_to_number() {
Some(k) if k == 1.into() => (false, format!("{var}")),
Some(k) if k == (-1).into() => (true, format!("{var}")),
Some(k) if k == T::FieldType::one() => (false, format!("{var}")),
Some(k) if k == -T::FieldType::one() => (true, format!("{var}")),
_ => {
let (sign, coeff) = Self::symbolic_expression_to_signed_string(coeff);
(sign, format!("{coeff} * {var}"))
@@ -958,7 +1027,7 @@ impl<T: FieldElement, V: Clone + Ord + Display> QuadraticSymbolicExpression<T, V
}),
)
.chain(match self.constant.try_to_number() {
Some(k) if k == T::zero() => None,
Some(k) if k == T::FieldType::zero() => None,
_ => Some(Self::symbolic_expression_to_signed_string(&self.constant)),
})
.reduce(|(n1, p1), (n2, p2)| {
@@ -974,7 +1043,7 @@ impl<T: FieldElement, V: Clone + Ord + Display> QuadraticSymbolicExpression<T, V
.unwrap_or((false, "0".to_string()))
}
fn symbolic_expression_to_signed_string(value: &SymbolicExpression<T, V>) -> (bool, String) {
fn symbolic_expression_to_signed_string(value: &T) -> (bool, String) {
match value.try_to_number() {
Some(k) => {
if k.is_in_lower_half() {
@@ -999,7 +1068,10 @@ mod tests {
use pretty_assertions::assert_eq;
type Qse = QuadraticSymbolicExpression<GoldilocksField, &'static str>;
type Qse = QuadraticSymbolicExpressionImpl<
SymbolicExpression<GoldilocksField, &'static str>,
&'static str,
>;
#[test]
fn test_mul() {
@@ -1039,7 +1111,7 @@ mod tests {
let x = Qse::from_unknown_variable("X");
let y = Qse::from_unknown_variable("Y");
let a = Qse::from_known_symbol("A", RangeConstraint::default());
let zero = Qse::from(GoldilocksField::from(0));
let zero = Qse::zero();
let t: Qse = x * y + a;
assert_eq!(t.to_string(), "(X) * (Y) + A");
assert_eq!((t.clone() * zero).to_string(), "0");
@@ -1125,7 +1197,7 @@ mod tests {
#[test]
fn unsolvable() {
let r = Qse::from(GoldilocksField::from(10)).solve(&NoRangeConstraints);
let r = Qse::from_number(GoldilocksField::from(10)).solve(&NoRangeConstraints);
assert!(r.is_err());
}
@@ -1133,14 +1205,12 @@ mod tests {
fn unsolvable_with_vars() {
let x = &Qse::from_known_symbol("X", Default::default());
let y = &Qse::from_known_symbol("Y", Default::default());
let mut constr = x + y - GoldilocksField::from(10).into();
let mut constr = x + y - constant(10);
// We cannot solve it, but we can also not learn anything new from it.
let result = constr.solve(&NoRangeConstraints).unwrap();
assert!(result.complete && result.effects.is_empty());
// But if we know the values, we can be sure there is a conflict.
assert!(Qse::from(GoldilocksField::from(10))
.solve(&NoRangeConstraints)
.is_err());
assert!(constant(10).solve(&NoRangeConstraints).is_err());
// The same with range constraints that disallow zero.
constr.substitute_by_known(
@@ -1154,14 +1224,12 @@ mod tests {
RangeConstraint::from_range(100.into(), 102.into()),
),
);
assert!(Qse::from(GoldilocksField::from(10))
.solve(&NoRangeConstraints)
.is_err());
assert!(constant(10).solve(&NoRangeConstraints).is_err());
}
#[test]
fn solvable_without_vars() {
let constr = Qse::from(GoldilocksField::from(0));
let constr = constant(0);
let result = constr.solve(&NoRangeConstraints).unwrap();
assert!(result.complete && result.effects.is_empty());
}
@@ -1171,14 +1239,14 @@ mod tests {
let y = Qse::from_known_symbol("y", Default::default());
let x = Qse::from_unknown_variable("X");
// 2 * X + 7 * y - 10 = 0
let two = Qse::from(GoldilocksField::from(2));
let seven = Qse::from(GoldilocksField::from(7));
let ten = Qse::from(GoldilocksField::from(10));
let two = constant(2);
let seven = constant(7);
let ten = constant(10);
let constr = two * x + seven * y - ten;
let result = constr.solve(&NoRangeConstraints).unwrap();
assert!(result.complete);
assert_eq!(result.effects.len(), 1);
let Effect::Assignment(var, expr) = &result.effects[0] else {
let EffectImpl::Assignment(var, expr) = &result.effects[0] else {
panic!("Expected assignment");
};
assert_eq!(var.to_string(), "X");
@@ -1191,8 +1259,8 @@ mod tests {
let z = Qse::from_known_symbol("z", Default::default());
let x = Qse::from_unknown_variable("X");
// z * X + 7 * y - 10 = 0
let seven = Qse::from(GoldilocksField::from(7));
let ten = Qse::from(GoldilocksField::from(10));
let seven = constant(7);
let ten = constant(10);
let mut constr = z * x + seven * y - ten.clone();
// If we do not range-constrain z, we cannot solve since we don't know if it might be zero.
let result = constr.solve(&NoRangeConstraints).unwrap();
@@ -1211,7 +1279,7 @@ mod tests {
let result = constr.solve(&range_constraints).unwrap();
assert!(result.complete);
let effects = result.effects;
let Effect::Assignment(var, expr) = &effects[0] else {
let EffectImpl::Assignment(var, expr) = &effects[0] else {
panic!("Expected assignment");
};
assert_eq!(var.to_string(), "X");
@@ -1227,10 +1295,9 @@ mod tests {
let c = Qse::from_unknown_variable("c");
let z = Qse::from_known_symbol("Z", Default::default());
// a * 0x100 - b * 0x10000 + c * 0x1000000 + 10 + Z = 0
let ten = Qse::from(GoldilocksField::from(10));
let constr: Qse = a * Qse::from(GoldilocksField::from(0x100))
- b * Qse::from(GoldilocksField::from(0x10000))
+ c * Qse::from(GoldilocksField::from(0x1000000))
let ten = constant(10);
let constr: Qse = a * constant(0x100) - b * constant(0x10000)
+ c * constant(0x1000000)
+ ten.clone()
+ z.clone();
// Without range constraints on a, this is not solvable.
@@ -1245,7 +1312,7 @@ mod tests {
let [effect] = &result.effects[..] else {
panic!();
};
let Effect::BitDecomposition(BitDecomposition { value, components }) = effect else {
let EffectImpl::BitDecomposition(BitDecomposition { value, components }) = effect else {
panic!();
};
assert_eq!(format!("{value}"), "(10 + Z)");
@@ -1282,19 +1349,17 @@ c = (((10 + Z) & 0xff000000) >> 24) [negative];
let range_constraints =
HashMap::from([("a", rc.clone()), ("b", rc.clone()), ("c", rc.clone())]);
// a * 0x100 + b * 0x10000 + c * 0x1000000 + 10 - Z = 0
let ten = Qse::from(GoldilocksField::from(10));
let constr = a * Qse::from(GoldilocksField::from(0x100))
+ b * Qse::from(GoldilocksField::from(0x10000))
+ c * Qse::from(GoldilocksField::from(0x1000000))
+ ten.clone()
- z.clone();
let ten = constant(10);
let constr =
a * constant(0x100) + b * constant(0x10000) + c * constant(0x1000000) + ten.clone()
- z.clone();
let result = constr.solve(&range_constraints).unwrap();
assert!(!result.complete);
let effects = result
.effects
.into_iter()
.map(|effect| match effect {
Effect::RangeConstraint(v, rc) => format!("{v}: {rc};\n"),
EffectImpl::RangeConstraint(v, rc) => format!("{v}: {rc};\n"),
_ => panic!(),
})
.format("")
@@ -1314,8 +1379,8 @@ c = (((10 + Z) & 0xff000000) >> 24) [negative];
let a = Qse::from_unknown_variable("a");
let b = Qse::from_known_symbol("b", rc.clone());
let range_constraints = HashMap::from([("a", rc.clone()), ("b", rc.clone())]);
let ten = Qse::from(GoldilocksField::from(10));
let two_pow8 = Qse::from(GoldilocksField::from(0x100));
let ten = constant(10);
let two_pow8 = constant(0x100);
let constr = (a.clone() - b.clone() + two_pow8 - ten.clone()) * (a - b - ten);
let result = constr.solve(&range_constraints).unwrap();
assert!(result.complete);
@@ -1323,7 +1388,7 @@ c = (((10 + Z) & 0xff000000) >> 24) [negative];
.effects
.into_iter()
.map(|effect| match effect {
Effect::ConditionalAssignment {
EffectImpl::ConditionalAssignment {
variable,
condition: Condition { value, condition },
in_range_value,
@@ -1347,7 +1412,7 @@ c = (((10 + Z) & 0xff000000) >> 24) [negative];
constr.substitute_by_known(&"b", &GoldilocksField::from(2).into());
let result = constr.solve(&range_constraints).unwrap();
assert!(result.complete);
let [Effect::Assignment(var, expr)] = result.effects.as_slice() else {
let [EffectImpl::Assignment(var, expr)] = result.effects.as_slice() else {
panic!("Expected 1 assignment");
};
assert_eq!(var, &"a");
@@ -1355,12 +1420,15 @@ c = (((10 + Z) & 0xff000000) >> 24) [negative];
}
fn unpack_range_constraint(
process_result: &ProcessResult<GoldilocksField, &'static str>,
process_result: &ProcessResult<
SymbolicExpression<GoldilocksField, &'static str>,
&'static str,
>,
) -> (&'static str, RangeConstraint<GoldilocksField>) {
let [effect] = &process_result.effects[..] else {
panic!();
};
let Effect::RangeConstraint(var, rc) = effect else {
let EffectImpl::RangeConstraint(var, rc) = effect else {
panic!();
};
(var, rc.clone())
@@ -1369,9 +1437,9 @@ c = (((10 + Z) & 0xff000000) >> 24) [negative];
#[test]
fn detect_bit_constraint() {
let a = Qse::from_unknown_variable("a");
let one = Qse::from(GoldilocksField::from(1));
let three = Qse::from(GoldilocksField::from(3));
let five = Qse::from(GoldilocksField::from(5));
let one = constant(1);
let three = constant(3);
let five = constant(5);
// All these constraints should be equivalent to a bit constraint.
let constraints = [
@@ -1392,8 +1460,8 @@ c = (((10 + Z) & 0xff000000) >> 24) [negative];
#[test]
fn detect_complete_range_constraint() {
let a = Qse::from_unknown_variable("a");
let three = Qse::from(GoldilocksField::from(3));
let four = Qse::from(GoldilocksField::from(4));
let three = constant(3);
let four = constant(4);
// `a` can be 3 or 4, which is can be completely represented by
// RangeConstraint::from_range(3, 4), so the identity should be
@@ -1413,8 +1481,8 @@ c = (((10 + Z) & 0xff000000) >> 24) [negative];
#[test]
fn detect_incomplete_range_constraint() {
let a = Qse::from_unknown_variable("a");
let three = Qse::from(GoldilocksField::from(3));
let five = Qse::from(GoldilocksField::from(5));
let three = constant(3);
let five = constant(5);
// `a` can be 3 or 5, so there is a range constraint
// RangeConstraint::from_range(3, 5) on `a`.

113
constraint-solver/src/runtime_constant.rs Normal file
View File

@@ -0,0 +1,113 @@
use std::ops::{Add, AddAssign, Mul, MulAssign, Neg, Sub};
use num_traits::{One, Zero};
use powdr_number::FieldElement;
use crate::range_constraint::RangeConstraint;
/// Represents a run-time constant in the constraint solver, built over
/// a base field type.
/// The base field type itself (i.e. any T: FieldElement) represents a run-time constant
/// (which is also a compile-time constant), but the trait lets us represent run-time
/// constants symbolically as well.
pub trait RuntimeConstant:
Sized
+ Neg<Output = Self>
+ Clone
+ From<Self::FieldType>
+ Add<Output = Self>
+ AddAssign<Self>
+ Sub<Output = Self>
+ Mul<Output = Self>
+ MulAssign<Self>
+ PartialEq
+ Eq
+ Zero
+ One
{
type FieldType: FieldElement;
/// Tries to convert the constant to a single number. This always works for compile-time constants.
fn try_to_number(&self) -> Option<Self::FieldType>;
/// Returns the range constraint for this constant. For compile-time constants,
/// this will be a single value range constraint.
fn range_constraint(&self) -> RangeConstraint<Self::FieldType>;
/// Divides this constant by another constant, returning a new constant.
fn field_div(&self, other: &Self) -> Self;
/// Converts a u64 to a run-time constant.
fn from_u64(k: u64) -> Self {
Self::from(Self::FieldType::from(k))
}
/// Returns whether this constant is known to be zero at compile time.
fn is_known_zero(&self) -> bool {
self.try_to_number().is_some_and(|n| n.is_zero())
}
/// Returns whether this constant is known to be one at compile time.
fn is_known_one(&self) -> bool {
self.try_to_number().is_some_and(|n| n.is_one())
}
/// Returns whether this constant is known to be -1 at compile time.
fn is_known_minus_one(&self) -> bool {
self.try_to_number()
.is_some_and(|n| n == -Self::FieldType::from(1))
}
/// Returns whether this constant is known to be non-zero at compile time.
/// Note that this could return true even if the constant is not known fully
/// at compile time, but it is guaranteed that the constant is not zero.
fn is_known_nonzero(&self) -> bool {
// Only checking range constraint is enough since if this is a known
// fixed value, we will get a range constraint with just a single value.
!self.range_constraint().allows_value(0.into())
}
}
pub trait ReferencedSymbols<V> {
/// Returns an iterator over all referenced symbols in this constant.
fn referenced_symbols<'a>(&'a self) -> impl Iterator<Item = &'a V> + 'a
where
V: 'a;
}
pub trait Substitutable<V> {
/// Substitutes a variable with another constant.
fn substitute(&mut self, variable: &V, substitution: &Self);
}
impl<T: FieldElement> RuntimeConstant for T {
type FieldType = T;
fn try_to_number(&self) -> Option<Self> {
Some(*self)
}
fn range_constraint(&self) -> RangeConstraint<Self::FieldType> {
RangeConstraint::from_value(*self)
}
fn field_div(&self, other: &Self) -> Self {
*self / *other
}
}
impl<T: FieldElement, V> ReferencedSymbols<V> for T {
fn referenced_symbols<'a>(&'a self) -> impl Iterator<Item = &'a V> + 'a
where
V: 'a,
{
// No symbols in numbers.
std::iter::empty()
}
}
impl<T: FieldElement, V> Substitutable<V> for T {
fn substitute(&mut self, _variable: &V, _substitution: &Self) {
// No-op for numbers.
}
}

7
constraint-solver/src/solver.rs
View File

@@ -203,7 +203,10 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display, BusInter: BusInterac
fn apply_effect(&mut self, effect: Effect<T, Variable<V>>) -> bool {
match effect {
Effect::Assignment(v, expr) => self.apply_assignment(&v, &expr.into()),
Effect::Assignment(v, expr) => self.apply_assignment(
&v,
&QuadraticSymbolicExpression::from_runtime_constant(expr),
),
Effect::RangeConstraint(v, range_constraint) => {
self.apply_range_constraint_update(&v, range_constraint)
}
@@ -223,7 +226,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display, BusInter: BusInterac
if self.range_constraints.update(variable, &range_constraint) {
let new_rc = self.range_constraints.get(variable);
if let Some(value) = new_rc.try_to_single_value() {
self.apply_assignment(variable, &value.into());
self.apply_assignment(variable, &QuadraticSymbolicExpression::from_number(value));
} else {
// The range constraint was updated.
log::trace!("({variable}: {range_constraint})");

6
constraint-solver/src/solver/bus_interaction_variable_wrapper.rs
View File

@@ -82,8 +82,10 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display> BusInteractionVariab
// Apply any assignments to the bus interaction field definitions.
if let Variable::BusInteractionField(..) = variable {
if let Some(value) = expr.try_to_number() {
self.bus_interaction_vars
.insert(variable.clone(), value.into());
self.bus_interaction_vars.insert(
variable.clone(),
QuadraticSymbolicExpression::from_number(value),
);
} else {
// Non-concrete assignments are only generated by the `quadratic_equivalences` module,
// and bus interaction fields should only appear in bus interactions and constraints

1
constraint-solver/src/solver/quadratic_equivalences.rs
View File

@@ -8,6 +8,7 @@ use powdr_number::FieldElement;
use crate::{
quadratic_symbolic_expression::{QuadraticSymbolicExpression, RangeConstraintProvider},
range_constraint::RangeConstraint,
runtime_constant::RuntimeConstant,
symbolic_expression::SymbolicExpression,
};

217
constraint-solver/src/symbolic_expression.rs
View File

@@ -1,5 +1,6 @@
use auto_enums::auto_enum;
use itertools::Itertools;
use num_traits::{One, Zero};
use std::hash::Hash;
use std::ops::Sub;
use std::ops::{AddAssign, MulAssign};
@@ -10,7 +11,9 @@ use std::{
sync::Arc,
};
use powdr_number::FieldElement;
use powdr_number::{ExpressionConvertible, FieldElement};
use crate::runtime_constant::{ReferencedSymbols, RuntimeConstant, Substitutable};
use super::range_constraint::RangeConstraint;
@@ -72,42 +75,6 @@ impl<T: FieldElement, S> SymbolicExpression<T, S> {
SymbolicExpression::Symbol(symbol, rc)
}
}
pub fn is_known_zero(&self) -> bool {
self.try_to_number().is_some_and(|n| n.is_zero())
}
pub fn is_known_one(&self) -> bool {
self.try_to_number().is_some_and(|n| n.is_one())
}
pub fn is_known_minus_one(&self) -> bool {
self.try_to_number().is_some_and(|n| n == -T::from(1))
}
pub fn is_known_nonzero(&self) -> bool {
// Only checking range constraint is enough since if this is a known
// fixed value, we will get a range constraint with just a single value.
!self.range_constraint().allows_value(0.into())
}
pub fn range_constraint(&self) -> RangeConstraint<T> {
match self {
SymbolicExpression::Concrete(v) => RangeConstraint::from_value(*v),
SymbolicExpression::Symbol(.., rc)
| SymbolicExpression::BinaryOperation(.., rc)
| SymbolicExpression::UnaryOperation(.., rc) => rc.clone(),
}
}
pub fn try_to_number(&self) -> Option<T> {
match self {
SymbolicExpression::Concrete(n) => Some(*n),
SymbolicExpression::Symbol(..)
| SymbolicExpression::BinaryOperation(..)
| SymbolicExpression::UnaryOperation(..) => None,
}
}
}
impl<T: FieldElement, S: Clone + Eq> SymbolicExpression<T, S> {
@@ -150,6 +117,51 @@ impl<T: FieldElement, S: Clone + Eq> SymbolicExpression<T, S> {
}
}
impl<T: FieldElement, V> ExpressionConvertible<T, V> for SymbolicExpression<T, V> {
/// Turns a SymbolicExpression into an expression over its variables, essentially
/// making all variables unknown variables.
///
/// Fails in case a division operation is used.
fn try_to_expression<
E: Add<E, Output = E> + Sub<E, Output = E> + Mul<E, Output = E> + Neg<Output = E>,
>(
&self,
number_converter: &impl Fn(&T) -> E,
var_converter: &impl Fn(&V) -> E,
try_to_number: &impl Fn(&E) -> Option<T>,
) -> Option<E> {
Some(match self {
SymbolicExpression::Concrete(value) => number_converter(value),
SymbolicExpression::Symbol(var, _) => var_converter(var),
SymbolicExpression::BinaryOperation(left, op, right, _) => {
let left =
left.try_to_expression(number_converter, var_converter, try_to_number)?;
let right =
right.try_to_expression(number_converter, var_converter, try_to_number)?;
match op {
BinaryOperator::Add => left + right,
BinaryOperator::Sub => left - right,
BinaryOperator::Mul => left * right,
BinaryOperator::Div => {
if let Some(right) = try_to_number(&right) {
left * number_converter(&(T::from(1) / right))
} else {
return None;
}
}
}
}
SymbolicExpression::UnaryOperation(op, inner, _) => {
let inner =
inner.try_to_expression(number_converter, var_converter, try_to_number)?;
match op {
UnaryOperator::Neg => -inner,
}
}
})
}
}
impl<T: FieldElement, S1: Ord + Clone> SymbolicExpression<T, S1> {
pub fn transform_var_type<S2: Ord + Clone>(
&self,
@@ -235,7 +247,7 @@ impl<T: FieldElement, V> From<T> for SymbolicExpression<T, V> {
}
}
impl<T: FieldElement, V: Clone + PartialEq> Add for &SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> Add for &SymbolicExpression<T, V> {
type Output = SymbolicExpression<T, V>;
fn add(self, rhs: Self) -> Self::Output {
@@ -265,20 +277,20 @@ impl<T: FieldElement, V: Clone + PartialEq> Add for &SymbolicExpression<T, V> {
}
}
impl<T: FieldElement, V: Clone + PartialEq> Add for SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> Add for SymbolicExpression<T, V> {
type Output = SymbolicExpression<T, V>;
fn add(self, rhs: Self) -> Self::Output {
&self + &rhs
}
}
impl<T: FieldElement, V: Clone + PartialEq> AddAssign for SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> AddAssign for SymbolicExpression<T, V> {
fn add_assign(&mut self, rhs: Self) {
*self = self.clone() + rhs;
}
}
impl<T: FieldElement, V: Clone + PartialEq> Sub for &SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> Sub for &SymbolicExpression<T, V> {
type Output = SymbolicExpression<T, V>;
fn sub(self, rhs: Self) -> Self::Output {
@@ -304,14 +316,14 @@ impl<T: FieldElement, V: Clone + PartialEq> Sub for &SymbolicExpression<T, V> {
}
}
impl<T: FieldElement, V: Clone + PartialEq> Sub for SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> Sub for SymbolicExpression<T, V> {
type Output = SymbolicExpression<T, V>;
fn sub(self, rhs: Self) -> Self::Output {
&self - &rhs
}
}
impl<T: FieldElement, V: Clone + PartialEq> Neg for &SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> Neg for &SymbolicExpression<T, V> {
type Output = SymbolicExpression<T, V>;
fn neg(self) -> Self::Output {
@@ -360,14 +372,14 @@ impl<T: FieldElement, V: Clone + PartialEq> Neg for &SymbolicExpression<T, V> {
}
}
impl<T: FieldElement, V: Clone + PartialEq> Neg for SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> Neg for SymbolicExpression<T, V> {
type Output = SymbolicExpression<T, V>;
fn neg(self) -> Self::Output {
-&self
}
}
impl<T: FieldElement, V: Clone + PartialEq> Mul for &SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> Mul for &SymbolicExpression<T, V> {
type Output = SymbolicExpression<T, V>;
fn mul(self, rhs: Self) -> Self::Output {
@@ -395,43 +407,20 @@ impl<T: FieldElement, V: Clone + PartialEq> Mul for &SymbolicExpression<T, V> {
}
}
impl<T: FieldElement, V: Clone + PartialEq> Mul for SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> Mul for SymbolicExpression<T, V> {
type Output = SymbolicExpression<T, V>;
fn mul(self, rhs: Self) -> Self {
&self * &rhs
}
}
impl<T: FieldElement, V: Clone + PartialEq> MulAssign for SymbolicExpression<T, V> {
impl<T: FieldElement, V: Clone + Eq> MulAssign for SymbolicExpression<T, V> {
fn mul_assign(&mut self, rhs: Self) {
*self = self.clone() * rhs;
}
}
impl<T: FieldElement, V: Clone + PartialEq> SymbolicExpression<T, V> {
/// Field element division.
/// If you use this, you must ensure that the divisor is not zero.
pub fn field_div(&self, rhs: &Self) -> Self {
if let (SymbolicExpression::Concrete(a), SymbolicExpression::Concrete(b)) = (self, rhs) {
assert!(b != &T::from(0));
SymbolicExpression::Concrete(*a / *b)
} else if self.is_known_zero() {
SymbolicExpression::Concrete(T::from(0))
} else if rhs.is_known_one() {
self.clone()
} else if rhs.is_known_minus_one() {
-self
} else {
// TODO other simplifications like `-x / -y => x / y`, `-x / concrete => x / -concrete`, etc.
SymbolicExpression::BinaryOperation(
Arc::new(self.clone()),
BinaryOperator::Div,
Arc::new(rhs.clone()),
Default::default(),
)
}
}
impl<T: FieldElement, V: Clone + Eq> SymbolicExpression<T, V> {
/// Returns the multiplicative inverse in the field.
pub fn field_inverse(&self) -> Self {
if let SymbolicExpression::Concrete(x) = self {
@@ -454,3 +443,89 @@ impl<T: FieldElement, V: Clone + PartialEq> SymbolicExpression<T, V> {
}
}
}
impl<T: FieldElement, V: Clone + Eq> Zero for SymbolicExpression<T, V> {
fn zero() -> Self {
SymbolicExpression::Concrete(T::from(0))
}
fn is_zero(&self) -> bool {
self.is_known_zero()
}
}
impl<T: FieldElement, V: Clone + Eq> One for SymbolicExpression<T, V> {
fn one() -> Self {
SymbolicExpression::Concrete(T::from(1))
}
fn is_one(&self) -> bool {
self.is_known_one()
}
}
impl<T: FieldElement, V: Clone + Eq> RuntimeConstant for SymbolicExpression<T, V> {
type FieldType = T;
fn try_to_number(&self) -> Option<Self::FieldType> {
match self {
SymbolicExpression::Concrete(n) => Some(*n),
SymbolicExpression::Symbol(..)
| SymbolicExpression::BinaryOperation(..)
| SymbolicExpression::UnaryOperation(..) => None,
}
}
fn range_constraint(&self) -> RangeConstraint<Self::FieldType> {
match self {
SymbolicExpression::Concrete(v) => RangeConstraint::from_value(*v),
SymbolicExpression::Symbol(.., rc)
| SymbolicExpression::BinaryOperation(.., rc)
| SymbolicExpression::UnaryOperation(.., rc) => rc.clone(),
}
}
/// Field element division.
/// If you use this, you must ensure that the divisor is not zero.
fn field_div(&self, rhs: &Self) -> Self {
if let (SymbolicExpression::Concrete(a), SymbolicExpression::Concrete(b)) = (self, rhs) {
assert!(b != &T::from(0));
SymbolicExpression::Concrete(*a / *b)
} else if self.is_known_zero() {
SymbolicExpression::Concrete(T::from(0))
} else if rhs.is_known_one() {
self.clone()
} else if rhs.is_known_minus_one() {
-self
} else {
// TODO other simplifications like `-x / -y => x / y`, `-x / concrete => x / -concrete`, etc.
SymbolicExpression::BinaryOperation(
Arc::new(self.clone()),
BinaryOperator::Div,
Arc::new(rhs.clone()),
Default::default(),
)
}
}
fn from_u64(k: u64) -> Self {
SymbolicExpression::Concrete(T::from(k))
}
}
impl<T: FieldElement, V: Clone + Hash + Eq + Ord> ReferencedSymbols<V>
for SymbolicExpression<T, V>
{
fn referenced_symbols<'a>(&'a self) -> impl Iterator<Item = &'a V> + 'a
where
V: 'a,
{
SymbolicExpression::referenced_symbols(self)
}
}
impl<T: FieldElement, V: Clone + Hash + Eq + Ord> Substitutable<V> for SymbolicExpression<T, V> {
fn substitute(&mut self, variable: &V, substitution: &Self) {
SymbolicExpression::substitute(self, variable, substitution);
}
}

47
constraint-solver/src/symbolic_to_quadratic.rs
View File

@@ -1,48 +1 @@
use std::hash::Hash;
use powdr_number::FieldElement;
use crate::{
quadratic_symbolic_expression::QuadraticSymbolicExpression,
symbolic_expression::{BinaryOperator, SymbolicExpression, UnaryOperator},
};
/// Turns a SymbolicExpression to a QuadraticSymbolicExpression essentially
/// making all variables unknown variables.
///
/// Fails in case a division operation is used.
pub fn symbolic_expression_to_quadratic_symbolic_expression<
T: FieldElement,
V: Clone + Ord + Hash,
>(
e: &SymbolicExpression<T, V>,
) -> Option<QuadraticSymbolicExpression<T, V>> {
Some(match e {
SymbolicExpression::Concrete(value) => (*value).into(),
SymbolicExpression::Symbol(var, _) => {
QuadraticSymbolicExpression::from_unknown_variable(var.clone())
}
SymbolicExpression::BinaryOperation(left, op, right, _) => {
let left = symbolic_expression_to_quadratic_symbolic_expression(left)?;
let right = symbolic_expression_to_quadratic_symbolic_expression(right)?;
match op {
BinaryOperator::Add => left + right,
BinaryOperator::Sub => left - right,
BinaryOperator::Mul => left * right,
BinaryOperator::Div => {
if let Some(right) = right.try_to_known() {
left * right.field_inverse()
} else {
return None;
}
}
}
}
SymbolicExpression::UnaryOperation(op, inner, _) => {
let inner = symbolic_expression_to_quadratic_symbolic_expression(inner)?;
match op {
UnaryOperator::Neg => -inner,
}
}
})
}

2
constraint-solver/src/test_utils.rs
View File

@@ -10,5 +10,5 @@ pub fn var(name: Var) -> Qse {
}
pub fn constant(value: u64) -> Qse {
GoldilocksField::from(value).into()
Qse::from_number(GoldilocksField::from(value))
}

4
constraint-solver/tests/solver.rs
View File

@@ -371,8 +371,8 @@ fn binary_flags() {
fn ternary_flags() {
// Implementing this logic in the OpenVM load/store chip:
// https://github.com/openvm-org/openvm/blob/v1.2.0/extensions/rv32im/circuit/src/loadstore/core.rs#L110-L139
let two_inv = Qse::from(GoldilocksField::one() / GoldilocksField::from(2));
let neg_one = Qse::from(-GoldilocksField::one());
let two_inv = Qse::from_number(GoldilocksField::one() / GoldilocksField::from(2));
let neg_one = Qse::from_number(-GoldilocksField::one());
let sum = var("flag0") + var("flag1") + var("flag2") + var("flag3");
// The flags must be 0, 1, or 2, and their sum must be 1 or 2.
// Given these constraints, there are 14 possible assignments. The following

7
executor/src/witgen/jit/block_machine_processor.rs
View File

@@ -2,6 +2,7 @@ use std::collections::{BTreeMap, BTreeSet, HashSet};
use bit_vec::BitVec;
use itertools::Itertools;
use num_traits::{One, Zero};
use powdr_ast::analyzed::{ContainsNextRef, PolyID, PolynomialType};
use powdr_constraint_solver::quadratic_symbolic_expression::QuadraticSymbolicExpression;
use powdr_number::FieldElement;
@@ -85,7 +86,7 @@ impl<'a, T: FieldElement> BlockMachineProcessor<'a, T> {
let selector = &bus_receive.selected_payload.selector;
queue_items.extend(algebraic_expression_to_queue_items(
selector,
T::one(),
QuadraticSymbolicExpression::one(),
self.latch_row as i32,
&witgen,
));
@@ -94,7 +95,7 @@ impl<'a, T: FieldElement> BlockMachineProcessor<'a, T> {
// Set the known argument to the concrete value.
queue_items.extend(algebraic_expression_to_queue_items(
&bus_receive.selected_payload.expressions[index],
value,
QuadraticSymbolicExpression::from_number(value),
self.latch_row as i32,
&witgen,
));
@@ -106,7 +107,7 @@ impl<'a, T: FieldElement> BlockMachineProcessor<'a, T> {
if other_selector != selector {
queue_items.extend(algebraic_expression_to_queue_items(
other_selector,
T::zero(),
QuadraticSymbolicExpression::zero(),
self.latch_row as i32,
&witgen,
));

6
executor/src/witgen/jit/compiler.rs
View File

@@ -377,6 +377,7 @@ fn format_effect<T: FieldElement>(effect: &Effect<T, Variable>, is_top_level: bo
lhs,
rhs,
expected_equal,
..
}) => format!(
"assert!({} {} {});",
format_expression(lhs),
@@ -534,7 +535,7 @@ fn format_bit_decomposition<T: FieldElement>(
}
fn format_condition<T: FieldElement>(
Condition { value, condition }: &Condition<T, Variable>,
Condition { value, condition }: &Condition<SymbolicExpression<T, Variable>>,
) -> String {
let value = format!("IntType::from({})", format_expression(value));
let (min, max) = condition.range();
@@ -676,6 +677,7 @@ mod tests {
use powdr_ast::analyzed::AlgebraicReference;
use powdr_ast::analyzed::FunctionValueDefinition;
use powdr_constraint_solver::range_constraint::RangeConstraint;
use powdr_constraint_solver::runtime_constant::RuntimeConstant;
use pretty_assertions::assert_eq;
use test_log::test;
@@ -770,7 +772,7 @@ mod tests {
assignment(&x0, number(7) * symbol(&a0)),
assignment(&cv1, symbol(&x0)),
Effect::MachineCall(
7.into(),
GoldilocksField::from(7),
[false, true].into_iter().collect(),
vec![r1.clone(), cv1.clone()],
),

4
executor/src/witgen/jit/debug_formatter.rs
View File

@@ -3,7 +3,9 @@ use powdr_ast::analyzed::{
AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression as Expression,
AlgebraicUnaryOperation, PolynomialIdentity, SelectedExpressions,
};
use powdr_constraint_solver::range_constraint::RangeConstraint;
use powdr_constraint_solver::{
range_constraint::RangeConstraint, runtime_constant::RuntimeConstant,
};
use powdr_number::FieldElement;
use crate::witgen::data_structures::identity::{BusSend, Identity};

28
executor/src/witgen/jit/effect.rs
View File

@@ -8,6 +8,7 @@ use powdr_ast::indent;
use powdr_constraint_solver::effect::{
Assertion, BitDecomposition, BitDecompositionComponent, Condition,
};
use powdr_constraint_solver::runtime_constant::RuntimeConstant;
use powdr_constraint_solver::symbolic_expression::SymbolicExpression;
use powdr_number::FieldElement;
@@ -18,24 +19,33 @@ use super::variable::Variable;
/// The effect of solving a symbolic equation.
#[derive(Clone, PartialEq, Eq)]
pub enum Effect<T: FieldElement, V> {
pub enum Effect<T: FieldElement, V>
where
SymbolicExpression<T, V>: RuntimeConstant,
{
/// Variable can be assigned a value.
Assignment(V, SymbolicExpression<T, V>),
/// Perform a bit decomposition of a known value, and assign multiple variables.
BitDecomposition(BitDecomposition<T, V>),
BitDecomposition(BitDecomposition<SymbolicExpression<T, V>, V>),
/// We learnt a new range constraint on variable.
RangeConstraint(V, RangeConstraint<T>),
/// A run-time assertion. If this fails, we have conflicting constraints.
Assertion(Assertion<T, V>),
Assertion(Assertion<SymbolicExpression<T, V>>),
/// A call to a different machine, with bus ID, known inputs and argument variables.
MachineCall(T, BitVec, Vec<V>),
/// Compute one variable by executing a prover function (given by index) on the value of other variables.
ProverFunctionCall(ProverFunctionCall<V>),
/// A branch on a variable.
Branch(Condition<T, V>, Vec<Effect<T, V>>, Vec<Effect<T, V>>),
Branch(
Condition<SymbolicExpression<T, V>>,
Vec<Effect<T, V>>,
Vec<Effect<T, V>>,
),
}
impl<T: FieldElement, V: Clone> From<ConstraintSolverEffect<T, V>> for Effect<T, V> {
impl<T: FieldElement, V: Clone + Hash + Eq + Ord> From<ConstraintSolverEffect<T, V>>
for Effect<T, V>
{
fn from(effect: ConstraintSolverEffect<T, V>) -> Self {
match effect {
ConstraintSolverEffect::Assignment(v, expr) => Effect::Assignment(v, expr),
@@ -87,7 +97,10 @@ impl<T: FieldElement> Effect<T, Variable> {
}
}
impl<T: FieldElement, V: Hash + Eq> Effect<T, V> {
impl<T: FieldElement, V: Hash + Eq> Effect<T, V>
where
SymbolicExpression<T, V>: RuntimeConstant,
{
/// Returns an iterator over all referenced variables, both read and written.
pub fn referenced_variables(&self) -> impl Iterator<Item = &V> {
let iter: Box<dyn Iterator<Item = &V>> = match self {
@@ -143,6 +156,7 @@ pub fn format_code<T: FieldElement>(effects: &[Effect<T, Variable>]) -> String {
lhs,
rhs,
expected_equal,
..
}) => {
format!(
"assert {lhs} {} {rhs};",
@@ -206,7 +220,7 @@ pub fn format_code<T: FieldElement>(effects: &[Effect<T, Variable>]) -> String {
}
fn format_condition<T: FieldElement>(
Condition { value, condition }: &Condition<T, Variable>,
Condition { value, condition }: &Condition<SymbolicExpression<T, Variable>>,
) -> String {
let (min, max) = condition.range();
match min.cmp(&max) {

1
executor/src/witgen/jit/identity_queue.rs
View File

@@ -12,6 +12,7 @@ use powdr_ast::{
};
use powdr_constraint_solver::{
quadratic_symbolic_expression::QuadraticSymbolicExpression,
runtime_constant::RuntimeConstant,
symbolic_expression::SymbolicExpression,
variable_update::{UpdateKind, VariableUpdate},
};

2
executor/src/witgen/jit/interpreter.rs
View File

@@ -80,7 +80,7 @@ enum BranchTest<T: FieldElement> {
impl<T: FieldElement> BranchTest<T> {
fn new(
var_mapper: &mut VariableMapper,
Condition { value, condition }: &Condition<T, Variable>,
Condition { value, condition }: &Condition<SymbolicExpression<T, Variable>>,
) -> Self {
let (min, max) = condition.range();
let value = var_mapper.map_expr_to_rpn(value);

5
executor/src/witgen/jit/processor.rs
View File

@@ -1,6 +1,7 @@
use std::fmt::{self, Display, Formatter, Write};
use itertools::Itertools;
use num_traits::Zero;
use powdr_ast::analyzed::{AlgebraicExpression, PolynomialIdentity};
use powdr_constraint_solver::range_constraint::RangeConstraint;
use powdr_constraint_solver::symbolic_expression::SymbolicExpression;
@@ -48,7 +49,7 @@ pub struct Processor<'a, T: FieldElement> {
pub struct ProcessorResult<T: FieldElement> {
/// Generated code.
pub code: Vec<Effect<T, Variable>>,
/// Range constrainst of the variables they were requested on.
/// Range constraints of the variables they were requested on.
pub range_constraints: Vec<RangeConstraint<T>>,
}
@@ -111,7 +112,7 @@ impl<'a, T: FieldElement> Processor<'a, T> {
}
Identity::Polynomial(identity) => algebraic_expression_to_queue_items(
&identity.expression,
T::zero(),
QuadraticSymbolicExpression::zero(),
*row_offset,
&witgen,
)

8
executor/src/witgen/jit/witgen_inference.rs
View File

@@ -15,6 +15,7 @@ use powdr_constraint_solver::{
Error, ProcessResult, QuadraticSymbolicExpression, RangeConstraintProvider,
},
range_constraint::RangeConstraint,
runtime_constant::RuntimeConstant,
symbolic_expression::SymbolicExpression,
};
use powdr_number::FieldElement;
@@ -75,7 +76,7 @@ pub struct BranchResult<'a, T: FieldElement, FixedEval> {
/// The code common to both branches.
pub common_code: Vec<Effect<T, Variable>>,
/// The condition of the branch.
pub condition: Condition<T, Variable>,
pub condition: Condition<SymbolicExpression<T, Variable>>,
/// The two branches.
pub branches: [WitgenInference<'a, T, FixedEval>; 2],
}
@@ -232,7 +233,8 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
/// Set a variable to a fixed value.
pub fn set_variable(&mut self, variable: Variable, value: T) -> Result<Vec<Variable>, Error> {
self.process_equation(
&(QuadraticSymbolicExpression::from_unknown_variable(variable) - value.into()),
&(QuadraticSymbolicExpression::from_unknown_variable(variable)
- QuadraticSymbolicExpression::from_number(value)),
)
}
@@ -466,7 +468,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
self,
),
Expression::PublicReference(_) | Expression::Challenge(_) => todo!(),
Expression::Number(n) => (*n).into(),
Expression::Number(n) => QuadraticSymbolicExpression::from_number(*n),
Expression::BinaryOperation(AlgebraicBinaryOperation { left, op, right }) => {
let left = self.evaluate(left, row_offset, require_concretely_known);
let right = self.evaluate(right, row_offset, require_concretely_known);

38
expression/src/conversion.rs
View File

@@ -1,38 +0,0 @@
use powdr_number::FieldElement;
use super::{
AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression,
AlgebraicUnaryOperation, AlgebraicUnaryOperator,
};
/// Converts an AlgebraicExpression into a different structure that supports algebraic operations.
/// The `reference_converter` is used to convert the reference that appear in the expression.
pub fn convert<T: FieldElement, R, Target>(
expr: &AlgebraicExpression<T, R>,
reference_converter: &mut impl FnMut(&R) -> Target,
) -> Target
where
Target: From<T>
+ Clone
+ std::ops::Add<Output = Target>
+ std::ops::Sub<Output = Target>
+ std::ops::Mul<Output = Target>
+ std::ops::Neg<Output = Target>,
{
match expr {
AlgebraicExpression::Reference(r) => reference_converter(r),
AlgebraicExpression::Number(n) => (*n).into(),
AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { left, op, right }) => {
let left = convert(left, reference_converter);
let right = convert(right, reference_converter);
match op {
AlgebraicBinaryOperator::Add => left + right,
AlgebraicBinaryOperator::Sub => left - right,
AlgebraicBinaryOperator::Mul => left * right,
}
}
AlgebraicExpression::UnaryOperation(AlgebraicUnaryOperation { op, expr }) => match op {
AlgebraicUnaryOperator::Minus => -convert(expr, reference_converter),
},
}
}

37
expression/src/lib.rs
View File

@@ -1,9 +1,12 @@
use std::{iter, ops};
use std::{
iter,
ops::{self, Add, Mul, Neg, Sub},
};
use powdr_number::ExpressionConvertible;
use schemars::JsonSchema;
use serde::{Deserialize, Serialize};
pub mod conversion;
pub mod display;
pub mod visitors;
@@ -164,3 +167,33 @@ impl<T, R> From<T> for AlgebraicExpression<T, R> {
AlgebraicExpression::Number(value)
}
}
impl<T, R> ExpressionConvertible<T, R> for AlgebraicExpression<T, R> {
fn to_expression<
E: Add<E, Output = E> + Sub<E, Output = E> + Mul<E, Output = E> + Neg<Output = E>,
>(
&self,
number_converter: &impl Fn(&T) -> E,
var_converter: &impl Fn(&R) -> E,
) -> E {
match self {
AlgebraicExpression::Reference(r) => var_converter(r),
AlgebraicExpression::Number(n) => number_converter(n),
AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { left, op, right }) => {
let left = left.to_expression(number_converter, var_converter);
let right = right.to_expression(number_converter, var_converter);
match op {
AlgebraicBinaryOperator::Add => left + right,
AlgebraicBinaryOperator::Sub => left - right,
AlgebraicBinaryOperator::Mul => left * right,
}
}
AlgebraicExpression::UnaryOperation(AlgebraicUnaryOperation { op, expr }) => match op {
AlgebraicUnaryOperator::Minus => {
-expr.to_expression(number_converter, var_converter)
}
},
}
}
}

49
number/src/expression_convertible.rs Normal file
View File

@@ -0,0 +1,49 @@
use std::ops::{Add, Mul, Neg, Sub};
use crate::FieldElement;
pub trait ExpressionConvertible<T, V> {
/// Converts `self` into a structure that supports algebraic operations.
///
/// Fails in case a non-algebraic operation is used.
///
/// The `try_to_number` function is used to check if some conversions can be simplified.
///
/// This or `to_expression` must be implemented.
fn try_to_expression<
E: Add<E, Output = E> + Sub<E, Output = E> + Mul<E, Output = E> + Neg<Output = E>,
>(
&self,
number_converter: &impl Fn(&T) -> E,
var_converter: &impl Fn(&V) -> E,
_try_to_number: &impl Fn(&E) -> Option<T>,
) -> Option<E> {
Some(self.to_expression(number_converter, var_converter))
}
/// Converts `self` into a structure that supports algebraic operations.
///
/// This or `try_to_expression` must be implemented.
fn to_expression<
E: Add<E, Output = E> + Sub<E, Output = E> + Mul<E, Output = E> + Neg<Output = E>,
>(
&self,
number_converter: &impl Fn(&T) -> E,
var_converter: &impl Fn(&V) -> E,
) -> E {
self.try_to_expression(number_converter, var_converter, &|_| unreachable!())
.unwrap()
}
}
impl<V, T: FieldElement> ExpressionConvertible<T, V> for T {
fn to_expression<
E: Add<E, Output = E> + Sub<E, Output = E> + Mul<E, Output = E> + Neg<Output = E>,
>(
&self,
number_converter: &impl Fn(&T) -> E,
_var_converter: &impl Fn(&V) -> E,
) -> E {
number_converter(self)
}
}

3
number/src/lib.rs
View File

@@ -9,14 +9,17 @@ mod koala_bear;
mod mersenne31;
#[macro_use]
mod plonky3_macros;
mod expression_convertible;
mod serialize;
mod traits;
pub use serialize::{
buffered_write_file, read_polys_csv_file, write_polys_csv_file, CsvRenderMode, ReadWrite,
};
pub use baby_bear::BabyBearField;
pub use bn254::Bn254Field;
pub use expression_convertible::ExpressionConvertible;
pub use goldilocks::GoldilocksField;
pub use koala_bear::KoalaBearField;
pub use mersenne31::Mersenne31Field;

6
pilopt/src/qse_opt.rs
View File

@@ -9,6 +9,7 @@ use powdr_ast::analyzed::{
};
use powdr_constraint_solver::constraint_system::ConstraintSystem;
use powdr_constraint_solver::indexed_constraint_system::apply_substitutions;
use powdr_constraint_solver::runtime_constant::RuntimeConstant;
use powdr_constraint_solver::{
quadratic_symbolic_expression::QuadraticSymbolicExpression,
solver::{self, SolveResult},
@@ -114,7 +115,7 @@ pub fn algebraic_to_quadratic_symbolic_expression<T: FieldElement>(
struct TerminalConverter;
impl<T: FieldElement> algebraic_expression_conversion::TerminalConverter<Qse<T>>
impl<T: FieldElement> algebraic_expression_conversion::TerminalConverter<T, Qse<T>>
for TerminalConverter
{
fn convert_reference(&mut self, reference: &AlgebraicReference) -> Qse<T> {
@@ -126,6 +127,9 @@ pub fn algebraic_to_quadratic_symbolic_expression<T: FieldElement>(
fn convert_challenge(&mut self, challenge: &Challenge) -> Qse<T> {
Qse::from_unknown_variable(Variable::Challenge(*challenge))
}
fn convert_number(&mut self, number: &T) -> Qse<T> {
Qse::from_number(*number)
}
}
algebraic_expression_conversion::convert(expr, &mut TerminalConverter)