mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-01-11 02:07:59 -05:00
Inline only at end (#3173)
Fixes https://github.com/powdr-labs/powdr/issues/3113 --------- Co-authored-by: Georg Wiese <georgwiese@gmail.com> Co-authored-by: schaeff <thibaut@powdrlabs.com>
This commit is contained in:
chriseth
@@ -10,8 +10,6 @@ use num_traits::Zero;
|
||||
use powdr_constraint_solver::{
|
||||
constraint_system::{BusInteractionHandler, ConstraintRef, ConstraintSystem},
|
||||
grouped_expression::GroupedExpression,
|
||||
indexed_constraint_system::IndexedConstraintSystem,
|
||||
inliner,
|
||||
journaling_constraint_system::JournalingConstraintSystem,
|
||||
solver::Solver,
|
||||
};
|
||||
@@ -44,7 +42,6 @@ pub fn optimize_constraints<P: FieldElement, V: Ord + Clone + Eq + Hash + Displa
|
||||
constraint_system: JournalingConstraintSystem<P, V>,
|
||||
solver: &mut impl Solver<P, V>,
|
||||
bus_interaction_handler: impl BusInteractionHandler<P> + IsBusStateful<P> + Clone,
|
||||
should_inline: impl Fn(&V, &GroupedExpression<P, V>, &IndexedConstraintSystem<P, V>) -> bool,
|
||||
stats_logger: &mut StatsLogger,
|
||||
) -> Result<JournalingConstraintSystem<P, V>, Error> {
|
||||
let constraint_system = solver_based_optimization(constraint_system, solver)?;
|
||||
@@ -61,13 +58,19 @@ pub fn optimize_constraints<P: FieldElement, V: Ord + Clone + Eq + Hash + Displa
|
||||
remove_disconnected_columns(constraint_system, solver, bus_interaction_handler.clone());
|
||||
stats_logger.log("removing disconnected columns", &constraint_system);
|
||||
|
||||
// TODO should we remove inlined columns in the solver?
|
||||
// TODO should we inline here at all during solving (instead if only inside the solver)?
|
||||
let constraint_system =
|
||||
inliner::replace_constrained_witness_columns(constraint_system, should_inline);
|
||||
solver.add_algebraic_constraints(constraint_system.algebraic_constraints().cloned());
|
||||
stats_logger.log("in-lining witness columns", &constraint_system);
|
||||
Ok(trivial_simplifications(
|
||||
constraint_system,
|
||||
bus_interaction_handler,
|
||||
stats_logger,
|
||||
))
|
||||
}
|
||||
|
||||
/// Performs some very easy simplifications that only remove constraints.
|
||||
pub fn trivial_simplifications<P: FieldElement, V: Ord + Clone + Eq + Hash + Display>(
|
||||
constraint_system: JournalingConstraintSystem<P, V>,
|
||||
bus_interaction_handler: impl IsBusStateful<P>,
|
||||
stats_logger: &mut StatsLogger,
|
||||
) -> JournalingConstraintSystem<P, V> {
|
||||
let constraint_system = remove_trivial_constraints(constraint_system);
|
||||
stats_logger.log("removing trivial constraints", &constraint_system);
|
||||
|
||||
@@ -75,12 +78,13 @@ pub fn optimize_constraints<P: FieldElement, V: Ord + Clone + Eq + Hash + Displa
|
||||
remove_equal_bus_interactions(constraint_system, bus_interaction_handler);
|
||||
stats_logger.log("removing equal bus interactions", &constraint_system);
|
||||
|
||||
// TODO maybe we should keep learnt range constraints stored somewhere because
|
||||
// we might not be able to re-derive them if some constraints are missing.
|
||||
let constraint_system = remove_duplicate_factors(constraint_system);
|
||||
stats_logger.log("removing duplicate factors", &constraint_system);
|
||||
|
||||
let constraint_system = remove_redundant_constraints(constraint_system);
|
||||
stats_logger.log("removing redundant constraints", &constraint_system);
|
||||
|
||||
Ok(constraint_system)
|
||||
constraint_system
|
||||
}
|
||||
|
||||
fn solver_based_optimization<T: FieldElement, V: Clone + Ord + Hash + Display>(
|
||||
|
||||
@@ -4,8 +4,7 @@ use std::{collections::BTreeMap, fmt::Display};
|
||||
|
||||
use itertools::Itertools;
|
||||
use powdr_constraint_solver::constraint_system::BusInteractionHandler;
|
||||
use powdr_constraint_solver::indexed_constraint_system::IndexedConstraintSystem;
|
||||
use powdr_constraint_solver::inliner::inline_everything_below_degree_bound;
|
||||
use powdr_constraint_solver::inliner::{self, inline_everything_below_degree_bound};
|
||||
use powdr_constraint_solver::solver::{new_solver, Solver};
|
||||
use powdr_constraint_solver::{
|
||||
constraint_system::{BusInteraction, ConstraintSystem},
|
||||
@@ -14,7 +13,7 @@ use powdr_constraint_solver::{
|
||||
};
|
||||
use powdr_number::FieldElement;
|
||||
|
||||
use crate::constraint_optimizer::IsBusStateful;
|
||||
use crate::constraint_optimizer::{trivial_simplifications, IsBusStateful};
|
||||
use crate::low_degree_bus_interaction_optimizer::LowDegreeBusInteractionOptimizer;
|
||||
use crate::memory_optimizer::MemoryBusInteraction;
|
||||
use crate::range_constraint_optimizer::{optimize_range_constraints, RangeConstraintHandler};
|
||||
@@ -50,7 +49,6 @@ pub fn optimize<A: Adapter>(
|
||||
constraint_system,
|
||||
&mut solver,
|
||||
bus_interaction_handler.clone(),
|
||||
inline_everything_below_degree_bound(degree_bound),
|
||||
&mut stats_logger,
|
||||
bus_map,
|
||||
degree_bound,
|
||||
@@ -60,6 +58,14 @@ pub fn optimize<A: Adapter>(
|
||||
}
|
||||
}
|
||||
|
||||
let constraint_system = inliner::replace_constrained_witness_columns(
|
||||
constraint_system.into(),
|
||||
inline_everything_below_degree_bound(degree_bound),
|
||||
)
|
||||
.system()
|
||||
.clone();
|
||||
stats_logger.log("inlining", &constraint_system);
|
||||
|
||||
// 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(
|
||||
@@ -69,6 +75,14 @@ pub fn optimize<A: Adapter>(
|
||||
);
|
||||
stats_logger.log("optimizing range constraints", &constraint_system);
|
||||
|
||||
let constraint_system = trivial_simplifications(
|
||||
constraint_system.into(),
|
||||
bus_interaction_handler,
|
||||
&mut stats_logger,
|
||||
)
|
||||
.system()
|
||||
.clone();
|
||||
|
||||
// Sanity check: Degree bound should be respected:
|
||||
for algebraic_constraint in &constraint_system.algebraic_constraints {
|
||||
assert!(
|
||||
@@ -114,7 +128,6 @@ fn optimization_loop_iteration<
|
||||
+ IsBusStateful<P>
|
||||
+ RangeConstraintHandler<P>
|
||||
+ Clone,
|
||||
should_inline: impl Fn(&V, &GroupedExpression<P, V>, &IndexedConstraintSystem<P, V>) -> bool,
|
||||
stats_logger: &mut StatsLogger,
|
||||
bus_map: &BusMap<C>,
|
||||
degree_bound: DegreeBound,
|
||||
@@ -124,7 +137,6 @@ fn optimization_loop_iteration<
|
||||
constraint_system,
|
||||
solver,
|
||||
bus_interaction_handler.clone(),
|
||||
should_inline,
|
||||
stats_logger,
|
||||
)?;
|
||||
let constraint_system = constraint_system.system().clone();
|
||||
|
||||
@@ -32,21 +32,28 @@ pub fn replace_constrained_witness_columns<
|
||||
.indexed_system()
|
||||
.algebraic_constraints()
|
||||
.len();
|
||||
for curr_idx in (0..constraint_count).rev() {
|
||||
let constraint = &constraint_system.indexed_system().algebraic_constraints()[curr_idx];
|
||||
loop {
|
||||
let inlined_vars_count = inlined_vars.len();
|
||||
for curr_idx in (0..constraint_count).rev() {
|
||||
let constraint = &constraint_system.indexed_system().algebraic_constraints()[curr_idx];
|
||||
|
||||
for (var, expr) in find_inlinable_variables(constraint) {
|
||||
if should_inline(&var, &expr, constraint_system.indexed_system()) {
|
||||
log::trace!("Substituting {var} = {expr}");
|
||||
log::trace!(" (from identity {constraint})");
|
||||
for (var, expr) in find_inlinable_variables(constraint) {
|
||||
if should_inline(&var, &expr, constraint_system.indexed_system()) {
|
||||
log::trace!("Substituting {var} = {expr}");
|
||||
log::trace!(" (from identity {constraint})");
|
||||
|
||||
constraint_system.substitute_by_unknown(&var, &expr);
|
||||
to_remove_idx.insert(curr_idx);
|
||||
inlined_vars.insert(var);
|
||||
constraint_system.substitute_by_unknown(&var, &expr);
|
||||
to_remove_idx.insert(curr_idx);
|
||||
inlined_vars.insert(var);
|
||||
|
||||
break;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
if inlined_vars.len() == inlined_vars_count {
|
||||
// No more variables to inline
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
// remove inlined constraints from system
|
||||
|
||||
@@ -363,6 +363,10 @@ where
|
||||
while let Some(item) = self.constraint_system.pop_front() {
|
||||
let effects = match item {
|
||||
ConstraintRef::AlgebraicConstraint(c) => {
|
||||
if let Some((v1, expr)) = is_simple_equivalence(c) {
|
||||
self.apply_assignment(&v1, &expr);
|
||||
continue;
|
||||
}
|
||||
c.solve(&self.range_constraints)
|
||||
.map_err(Error::QseSolvingError)?
|
||||
.effects
|
||||
@@ -556,6 +560,24 @@ where
|
||||
}
|
||||
}
|
||||
|
||||
fn is_simple_equivalence<T: RuntimeConstant, V: Clone + Ord + Eq>(
|
||||
expr: &GroupedExpression<T, V>,
|
||||
) -> Option<(V, GroupedExpression<T, V>)> {
|
||||
if !expr.is_affine() {
|
||||
return None;
|
||||
}
|
||||
let (_, linear, offset) = expr.components();
|
||||
let [(v1, c1), (v2, c2)] = linear.collect_vec().try_into().ok()?;
|
||||
if offset.is_zero() && (c1.is_one() || c2.is_one()) && (c1.clone() + c2.clone()).is_zero() {
|
||||
Some((
|
||||
v2.clone(),
|
||||
GroupedExpression::from_unknown_variable(v1.clone()),
|
||||
))
|
||||
} else {
|
||||
None
|
||||
}
|
||||
}
|
||||
|
||||
/// The currently known range constraints for the variables.
|
||||
pub struct RangeConstraints<T: FieldElement, V> {
|
||||
pub range_constraints: HashMap<V, RangeConstraint<T>>,
|
||||
|
||||
@@ -1647,11 +1647,11 @@ mod tests {
|
||||
AirMetrics {
|
||||
widths: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 14702,
|
||||
log_up: 23300,
|
||||
main: 14698,
|
||||
log_up: 23296,
|
||||
},
|
||||
constraints: 4393,
|
||||
bus_interactions: 11419,
|
||||
constraints: 4389,
|
||||
bus_interactions: 11416,
|
||||
}
|
||||
"#]],
|
||||
powdr_expected_machine_count: expect![[r#"
|
||||
@@ -1675,11 +1675,11 @@ mod tests {
|
||||
AirMetrics {
|
||||
widths: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 14674,
|
||||
log_up: 23268,
|
||||
main: 14670,
|
||||
log_up: 23264,
|
||||
},
|
||||
constraints: 4369,
|
||||
bus_interactions: 11409,
|
||||
constraints: 4365,
|
||||
bus_interactions: 11406,
|
||||
}
|
||||
"#]],
|
||||
powdr_expected_machine_count: expect![[r#"
|
||||
@@ -1697,8 +1697,8 @@ mod tests {
|
||||
},
|
||||
after: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 14674,
|
||||
log_up: 23268,
|
||||
main: 14670,
|
||||
log_up: 23264,
|
||||
},
|
||||
}
|
||||
"#]]),
|
||||
@@ -1756,11 +1756,11 @@ mod tests {
|
||||
AirMetrics {
|
||||
widths: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 16416,
|
||||
log_up: 26292,
|
||||
main: 15999,
|
||||
log_up: 25852,
|
||||
},
|
||||
constraints: 9132,
|
||||
bus_interactions: 11135,
|
||||
constraints: 8721,
|
||||
bus_interactions: 10914,
|
||||
}
|
||||
"#]],
|
||||
powdr_expected_machine_count: expect![[r#"
|
||||
@@ -1778,8 +1778,8 @@ mod tests {
|
||||
},
|
||||
after: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 16416,
|
||||
log_up: 26292,
|
||||
main: 15999,
|
||||
log_up: 25852,
|
||||
},
|
||||
}
|
||||
"#]]),
|
||||
@@ -1805,11 +1805,11 @@ mod tests {
|
||||
AirMetrics {
|
||||
widths: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 19754,
|
||||
log_up: 30204,
|
||||
main: 19161,
|
||||
log_up: 29572,
|
||||
},
|
||||
constraints: 11826,
|
||||
bus_interactions: 13073,
|
||||
constraints: 11242,
|
||||
bus_interactions: 12759,
|
||||
}
|
||||
"#]],
|
||||
powdr_expected_machine_count: expect![[r#"
|
||||
@@ -1827,8 +1827,8 @@ mod tests {
|
||||
},
|
||||
after: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 19754,
|
||||
log_up: 30204,
|
||||
main: 19161,
|
||||
log_up: 29572,
|
||||
},
|
||||
}
|
||||
"#]]),
|
||||
@@ -1960,11 +1960,11 @@ mod tests {
|
||||
AirMetrics {
|
||||
widths: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 3313,
|
||||
log_up: 5192,
|
||||
main: 3314,
|
||||
log_up: 5204,
|
||||
},
|
||||
constraints: 849,
|
||||
bus_interactions: 2513,
|
||||
constraints: 837,
|
||||
bus_interactions: 2512,
|
||||
}
|
||||
"#]],
|
||||
powdr_expected_machine_count: expect![[r#"
|
||||
@@ -1977,13 +1977,13 @@ mod tests {
|
||||
AirWidthsDiff {
|
||||
before: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 32714,
|
||||
log_up: 42092,
|
||||
main: 32788,
|
||||
log_up: 42196,
|
||||
},
|
||||
after: AirWidths {
|
||||
preprocessed: 0,
|
||||
main: 3313,
|
||||
log_up: 5192,
|
||||
main: 3314,
|
||||
log_up: 5204,
|
||||
},
|
||||
}
|
||||
"#]]),
|
||||
|
||||
@@ -13,14 +13,14 @@ Symbolic machine using 26 unique main columns:
|
||||
from_state__timestamp_0
|
||||
reads_aux__0__base__prev_timestamp_0
|
||||
reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0
|
||||
writes_aux__prev_data__0_0
|
||||
writes_aux__prev_data__1_0
|
||||
writes_aux__prev_data__2_0
|
||||
writes_aux__prev_data__3_0
|
||||
a__0_0
|
||||
a__1_0
|
||||
a__2_0
|
||||
a__3_0
|
||||
b__0_0
|
||||
b__1_0
|
||||
b__2_0
|
||||
b__3_0
|
||||
read_data_aux__base__prev_timestamp_1
|
||||
read_data_aux__base__timestamp_lt_aux__lower_decomp__0_1
|
||||
mem_ptr_limbs__0_1
|
||||
@@ -42,7 +42,7 @@ mult=is_valid * -1, args=[0, from_state__timestamp_0]
|
||||
mult=is_valid * 1, args=[1788, from_state__timestamp_0 + 9]
|
||||
|
||||
// Bus 1 (MEMORY):
|
||||
mult=is_valid * -1, args=[1, 8, b__0_0, b__1_0, b__2_0, b__3_0, reads_aux__0__base__prev_timestamp_0]
|
||||
mult=is_valid * -1, args=[1, 8, writes_aux__prev_data__0_0, writes_aux__prev_data__1_0, writes_aux__prev_data__2_0, writes_aux__prev_data__3_0, reads_aux__0__base__prev_timestamp_0]
|
||||
mult=is_valid * 1, args=[1, 8, a__0_0, a__1_0, a__2_0, a__3_0, from_state__timestamp_0 + 3]
|
||||
mult=is_valid * -1, args=[1, 4, read_data__0_1, read_data__1_1, read_data__2_1, read_data__3_1, read_data_aux__base__prev_timestamp_1]
|
||||
mult=is_valid * -1, args=[2, mem_ptr_limbs__0_1 + 65536 * mem_ptr_limbs__1_1, prev_data__0_1, prev_data__1_1, prev_data__2_1, prev_data__3_1, write_base_aux__prev_timestamp_1]
|
||||
@@ -64,10 +64,10 @@ 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]
|
||||
|
||||
// Algebraic constraints:
|
||||
(7864320 * a__0_0 + 125829121 * is_valid - 7864320 * b__0_0) * (7864320 * a__0_0 + 125829120 - 7864320 * b__0_0) = 0
|
||||
(30720 * a__0_0 + 7864320 * a__1_0 + 491521 * is_valid - (30720 * b__0_0 + 7864320 * b__1_0)) * (30720 * a__0_0 + 7864320 * a__1_0 + 491520 - (30720 * b__0_0 + 7864320 * b__1_0)) = 0
|
||||
(120 * a__0_0 + 30720 * a__1_0 + 7864320 * a__2_0 + 1921 * is_valid - (120 * b__0_0 + 30720 * b__1_0 + 7864320 * b__2_0)) * (120 * a__0_0 + 30720 * a__1_0 + 7864320 * a__2_0 + 1920 - (120 * b__0_0 + 30720 * b__1_0 + 7864320 * b__2_0)) = 0
|
||||
(120 * a__1_0 + 30720 * a__2_0 + 7864320 * a__3_0 + 943718400 * b__0_0 - (943718400 * a__0_0 + 120 * b__1_0 + 30720 * b__2_0 + 7864320 * b__3_0 + 1006632952 * is_valid)) * (120 * a__1_0 + 30720 * a__2_0 + 7864320 * a__3_0 + 943718400 * b__0_0 - (943718400 * a__0_0 + 120 * b__1_0 + 30720 * b__2_0 + 7864320 * b__3_0 + 1006632953)) = 0
|
||||
(7864320 * a__0_0 + 125829121 * is_valid - 7864320 * writes_aux__prev_data__0_0) * (7864320 * a__0_0 + 125829120 - 7864320 * writes_aux__prev_data__0_0) = 0
|
||||
(30720 * a__0_0 + 7864320 * a__1_0 + 491521 * is_valid - (30720 * writes_aux__prev_data__0_0 + 7864320 * writes_aux__prev_data__1_0)) * (30720 * a__0_0 + 7864320 * a__1_0 + 491520 - (30720 * writes_aux__prev_data__0_0 + 7864320 * writes_aux__prev_data__1_0)) = 0
|
||||
(120 * a__0_0 + 30720 * a__1_0 + 7864320 * a__2_0 + 1921 * is_valid - (120 * writes_aux__prev_data__0_0 + 30720 * writes_aux__prev_data__1_0 + 7864320 * writes_aux__prev_data__2_0)) * (120 * a__0_0 + 30720 * a__1_0 + 7864320 * a__2_0 + 1920 - (120 * writes_aux__prev_data__0_0 + 30720 * writes_aux__prev_data__1_0 + 7864320 * writes_aux__prev_data__2_0)) = 0
|
||||
(943718400 * writes_aux__prev_data__0_0 + 120 * a__1_0 + 30720 * a__2_0 + 7864320 * a__3_0 - (120 * writes_aux__prev_data__1_0 + 30720 * writes_aux__prev_data__2_0 + 7864320 * writes_aux__prev_data__3_0 + 943718400 * a__0_0 + 1006632952 * is_valid)) * (943718400 * writes_aux__prev_data__0_0 + 120 * a__1_0 + 30720 * a__2_0 + 7864320 * a__3_0 - (120 * writes_aux__prev_data__1_0 + 30720 * writes_aux__prev_data__2_0 + 7864320 * writes_aux__prev_data__3_0 + 943718400 * a__0_0 + 1006632953)) = 0
|
||||
(30720 * mem_ptr_limbs__0_1 - (30720 * a__0_0 + 7864320 * a__1_0 + 368640 * is_valid)) * (30720 * mem_ptr_limbs__0_1 - (30720 * a__0_0 + 7864320 * a__1_0 + 368641)) = 0
|
||||
(943718400 * a__0_0 + 30720 * mem_ptr_limbs__1_1 - (120 * a__1_0 + 30720 * a__2_0 + 7864320 * a__3_0 + 943718400 * mem_ptr_limbs__0_1 + 754974726 * is_valid)) * (943718400 * a__0_0 + 30720 * mem_ptr_limbs__1_1 - (120 * a__1_0 + 30720 * a__2_0 + 7864320 * a__3_0 + 943718400 * mem_ptr_limbs__0_1 + 754974727)) = 0
|
||||
is_valid * (is_valid - 1) = 0
|
||||
@@ -6,11 +6,11 @@ Instructions:
|
||||
BNE 52 0 248 1 1
|
||||
|
||||
APC advantage:
|
||||
- Main columns: 172 -> 38 (4.53x reduction)
|
||||
- Bus interactions: 87 -> 22 (3.95x reduction)
|
||||
- Constraints: 111 -> 34 (3.26x reduction)
|
||||
- Main columns: 172 -> 37 (4.65x reduction)
|
||||
- Bus interactions: 87 -> 21 (4.14x reduction)
|
||||
- Constraints: 111 -> 33 (3.36x reduction)
|
||||
|
||||
Symbolic machine using 38 unique main columns:
|
||||
Symbolic machine using 37 unique main columns:
|
||||
from_state__timestamp_0
|
||||
reads_aux__0__base__prev_timestamp_0
|
||||
reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0
|
||||
@@ -33,12 +33,11 @@ Symbolic machine using 38 unique main columns:
|
||||
diff_val_1
|
||||
reads_aux__0__base__prev_timestamp_2
|
||||
reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_2
|
||||
b__0_2
|
||||
b__1_2
|
||||
b__2_2
|
||||
b__3_2
|
||||
writes_aux__prev_data__0_2
|
||||
writes_aux__prev_data__1_2
|
||||
writes_aux__prev_data__2_2
|
||||
writes_aux__prev_data__3_2
|
||||
cmp_result_2
|
||||
b_msb_f_2
|
||||
diff_marker__0_2
|
||||
diff_marker__1_2
|
||||
diff_marker__2_2
|
||||
@@ -58,7 +57,7 @@ mult=is_valid * 1, args=[244 * cmp_result_4 + 20, from_state__timestamp_0 + 14]
|
||||
mult=is_valid * -1, args=[1, 44, b__0_0, b__1_0, b__2_0, b__3_0, reads_aux__0__base__prev_timestamp_0]
|
||||
mult=is_valid * 1, args=[1, 44, b__0_0, b__1_0, b__2_0, b__3_0, from_state__timestamp_0]
|
||||
mult=is_valid * -1, args=[1, 52, writes_aux__prev_data__0_0, writes_aux__prev_data__1_0, writes_aux__prev_data__2_0, writes_aux__prev_data__3_0, writes_aux__base__prev_timestamp_0]
|
||||
mult=is_valid * -1, args=[1, 56, b__0_2, b__1_2, b__2_2, b__3_2, reads_aux__0__base__prev_timestamp_2]
|
||||
mult=is_valid * -1, args=[1, 56, writes_aux__prev_data__0_2, writes_aux__prev_data__1_2, writes_aux__prev_data__2_2, writes_aux__prev_data__3_2, reads_aux__0__base__prev_timestamp_2]
|
||||
mult=is_valid * 1, args=[1, 56, cmp_result_2, 0, 0, 0, from_state__timestamp_0 + 10]
|
||||
mult=is_valid * 1, args=[1, 52, cmp_result_1 + cmp_result_2 - cmp_result_1 * cmp_result_2, 0, 0, 0, from_state__timestamp_0 + 12]
|
||||
mult=is_valid * -1, args=[1, 0, 0, 0, 0, 0, reads_aux__1__base__prev_timestamp_4]
|
||||
@@ -78,7 +77,6 @@ mult=is_valid * 1, args=[15360 * reads_aux__1__base__prev_timestamp_4 + 15360 *
|
||||
mult=is_valid * 1, args=[b__0_0, 3, b__0_0 + 3 - 2 * a__0_0, 1]
|
||||
mult=diff_marker__0_1 + diff_marker__1_1 + diff_marker__2_1 + diff_marker__3_1, args=[diff_val_1 - 1, 0, 0, 0]
|
||||
mult=diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2, args=[diff_val_2 - 1, 0, 0, 0]
|
||||
mult=is_valid * 1, args=[b_msb_f_2, 0, 0, 0]
|
||||
|
||||
// Algebraic constraints:
|
||||
cmp_result_1 * (cmp_result_1 - 1) = 0
|
||||
@@ -94,19 +92,18 @@ diff_marker__0_1 * ((a__0_0 - 1) * (2 * cmp_result_1 - 1) + diff_val_1) = 0
|
||||
(diff_marker__0_1 + diff_marker__1_1 + diff_marker__2_1 + diff_marker__3_1) * (diff_marker__0_1 + diff_marker__1_1 + diff_marker__2_1 + diff_marker__3_1 - 1) = 0
|
||||
(1 - (diff_marker__0_1 + diff_marker__1_1 + diff_marker__2_1 + diff_marker__3_1)) * cmp_result_1 = 0
|
||||
cmp_result_2 * (cmp_result_2 - 1) = 0
|
||||
(b__3_2 - b_msb_f_2) * (b_msb_f_2 + 256 - b__3_2) = 0
|
||||
diff_marker__3_2 * (diff_marker__3_2 - 1) = 0
|
||||
(1 - diff_marker__3_2) * (b_msb_f_2 * (2 * cmp_result_2 - 1)) = 0
|
||||
diff_marker__3_2 * (b_msb_f_2 * (2 * cmp_result_2 - 1) + diff_val_2) = 0
|
||||
(1 - diff_marker__3_2) * (writes_aux__prev_data__3_2 * (2 * cmp_result_2 - 1)) = 0
|
||||
diff_marker__3_2 * (writes_aux__prev_data__3_2 * (2 * cmp_result_2 - 1) + diff_val_2) = 0
|
||||
diff_marker__2_2 * (diff_marker__2_2 - 1) = 0
|
||||
(1 - (diff_marker__2_2 + diff_marker__3_2)) * (b__2_2 * (2 * cmp_result_2 - 1)) = 0
|
||||
diff_marker__2_2 * (b__2_2 * (2 * cmp_result_2 - 1) + diff_val_2) = 0
|
||||
(1 - (diff_marker__2_2 + diff_marker__3_2)) * (writes_aux__prev_data__2_2 * (2 * cmp_result_2 - 1)) = 0
|
||||
diff_marker__2_2 * (writes_aux__prev_data__2_2 * (2 * cmp_result_2 - 1) + diff_val_2) = 0
|
||||
diff_marker__1_2 * (diff_marker__1_2 - 1) = 0
|
||||
(1 - (diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2)) * (b__1_2 * (2 * cmp_result_2 - 1)) = 0
|
||||
diff_marker__1_2 * (b__1_2 * (2 * cmp_result_2 - 1) + diff_val_2) = 0
|
||||
(1 - (diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2)) * (writes_aux__prev_data__1_2 * (2 * cmp_result_2 - 1)) = 0
|
||||
diff_marker__1_2 * (writes_aux__prev_data__1_2 * (2 * cmp_result_2 - 1) + diff_val_2) = 0
|
||||
diff_marker__0_2 * (diff_marker__0_2 - 1) = 0
|
||||
(1 * is_valid - (diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2)) * ((1 - b__0_2) * (2 * cmp_result_2 - 1)) = 0
|
||||
diff_marker__0_2 * ((b__0_2 - 1) * (2 * cmp_result_2 - 1) + diff_val_2) = 0
|
||||
(1 * is_valid - (diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2)) * ((1 - writes_aux__prev_data__0_2) * (2 * cmp_result_2 - 1)) = 0
|
||||
diff_marker__0_2 * ((writes_aux__prev_data__0_2 - 1) * (2 * cmp_result_2 - 1) + diff_val_2) = 0
|
||||
(diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2) * (diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2 - 1) = 0
|
||||
(1 - (diff_marker__0_2 + diff_marker__1_2 + diff_marker__2_2 + diff_marker__3_2)) * cmp_result_2 = 0
|
||||
cmp_result_4 * (cmp_result_4 - 1) = 0
|
||||
|
||||
@@ -2,11 +2,11 @@ Instructions:
|
||||
SLTU rd_ptr = 8, rs1_ptr = 5, rs2 = 1, rs2_as = 0
|
||||
|
||||
APC advantage:
|
||||
- Main columns: 37 -> 21 (1.76x reduction)
|
||||
- Bus interactions: 18 -> 12 (1.50x reduction)
|
||||
- Constraints: 28 -> 18 (1.56x reduction)
|
||||
- Main columns: 37 -> 20 (1.85x reduction)
|
||||
- Bus interactions: 18 -> 11 (1.64x reduction)
|
||||
- Constraints: 28 -> 17 (1.65x reduction)
|
||||
|
||||
Symbolic machine using 21 unique main columns:
|
||||
Symbolic machine using 20 unique main columns:
|
||||
from_state__timestamp_0
|
||||
reads_aux__0__base__prev_timestamp_0
|
||||
reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0
|
||||
@@ -21,7 +21,6 @@ Symbolic machine using 21 unique main columns:
|
||||
b__2_0
|
||||
b__3_0
|
||||
cmp_result_0
|
||||
b_msb_f_0
|
||||
diff_marker__0_0
|
||||
diff_marker__1_0
|
||||
diff_marker__2_0
|
||||
@@ -47,14 +46,12 @@ mult=is_valid * 1, args=[15360 * writes_aux__base__prev_timestamp_0 + 15360 * wr
|
||||
|
||||
// Bus 6 (BITWISE_LOOKUP):
|
||||
mult=diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0, args=[diff_val_0 - 1, 0, 0, 0]
|
||||
mult=is_valid * 1, args=[b_msb_f_0, 0, 0, 0]
|
||||
|
||||
// Algebraic constraints:
|
||||
cmp_result_0 * (cmp_result_0 - 1) = 0
|
||||
(b__3_0 - b_msb_f_0) * (b_msb_f_0 + 256 - b__3_0) = 0
|
||||
diff_marker__3_0 * (diff_marker__3_0 - 1) = 0
|
||||
(1 - diff_marker__3_0) * (b_msb_f_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__3_0 * (b_msb_f_0 * (2 * cmp_result_0 - 1) + diff_val_0) = 0
|
||||
(1 - diff_marker__3_0) * (b__3_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__3_0 * (b__3_0 * (2 * cmp_result_0 - 1) + diff_val_0) = 0
|
||||
diff_marker__2_0 * (diff_marker__2_0 - 1) = 0
|
||||
(1 - (diff_marker__2_0 + diff_marker__3_0)) * (b__2_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__2_0 * (b__2_0 * (2 * cmp_result_0 - 1) + diff_val_0) = 0
|
||||
|
||||
@@ -2,11 +2,11 @@ Instructions:
|
||||
BGEU 8 5 2 1 1
|
||||
|
||||
APC advantage:
|
||||
- Main columns: 32 -> 22 (1.45x reduction)
|
||||
- Bus interactions: 13 -> 12 (1.08x reduction)
|
||||
- Constraints: 25 -> 19 (1.32x reduction)
|
||||
- Main columns: 32 -> 20 (1.60x reduction)
|
||||
- Bus interactions: 13 -> 11 (1.18x reduction)
|
||||
- Constraints: 25 -> 17 (1.47x reduction)
|
||||
|
||||
Symbolic machine using 22 unique main columns:
|
||||
Symbolic machine using 20 unique main columns:
|
||||
from_state__timestamp_0
|
||||
reads_aux__0__base__prev_timestamp_0
|
||||
reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0
|
||||
@@ -21,8 +21,6 @@ Symbolic machine using 22 unique main columns:
|
||||
b__2_0
|
||||
b__3_0
|
||||
cmp_result_0
|
||||
a_msb_f_0
|
||||
b_msb_f_0
|
||||
diff_marker__0_0
|
||||
diff_marker__1_0
|
||||
diff_marker__2_0
|
||||
@@ -48,15 +46,12 @@ mult=is_valid * 1, args=[15360 * reads_aux__1__base__prev_timestamp_0 + 15360 *
|
||||
|
||||
// Bus 6 (BITWISE_LOOKUP):
|
||||
mult=diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0, args=[diff_val_0 - 1, 0, 0, 0]
|
||||
mult=is_valid * 1, args=[a_msb_f_0, b_msb_f_0, 0, 0]
|
||||
|
||||
// Algebraic constraints:
|
||||
cmp_result_0 * (cmp_result_0 - 1) = 0
|
||||
(a__3_0 - a_msb_f_0) * (a_msb_f_0 + 256 - a__3_0) = 0
|
||||
(b__3_0 - b_msb_f_0) * (b_msb_f_0 + 256 - b__3_0) = 0
|
||||
diff_marker__3_0 * (diff_marker__3_0 - 1) = 0
|
||||
(1 - diff_marker__3_0) * ((b_msb_f_0 - a_msb_f_0) * (1 - 2 * cmp_result_0)) = 0
|
||||
diff_marker__3_0 * ((a_msb_f_0 - b_msb_f_0) * (1 - 2 * cmp_result_0) + diff_val_0) = 0
|
||||
(1 - diff_marker__3_0) * ((b__3_0 - a__3_0) * (1 - 2 * cmp_result_0)) = 0
|
||||
diff_marker__3_0 * ((a__3_0 - b__3_0) * (1 - 2 * cmp_result_0) + diff_val_0) = 0
|
||||
diff_marker__2_0 * (diff_marker__2_0 - 1) = 0
|
||||
(1 - (diff_marker__2_0 + diff_marker__3_0)) * ((b__2_0 - a__2_0) * (1 - 2 * cmp_result_0)) = 0
|
||||
diff_marker__2_0 * ((a__2_0 - b__2_0) * (1 - 2 * cmp_result_0) + diff_val_0) = 0
|
||||
|
||||
@@ -2,11 +2,11 @@ Instructions:
|
||||
BLTU 8 5 2 1 1
|
||||
|
||||
APC advantage:
|
||||
- Main columns: 32 -> 22 (1.45x reduction)
|
||||
- Bus interactions: 13 -> 12 (1.08x reduction)
|
||||
- Constraints: 25 -> 19 (1.32x reduction)
|
||||
- Main columns: 32 -> 20 (1.60x reduction)
|
||||
- Bus interactions: 13 -> 11 (1.18x reduction)
|
||||
- Constraints: 25 -> 17 (1.47x reduction)
|
||||
|
||||
Symbolic machine using 22 unique main columns:
|
||||
Symbolic machine using 20 unique main columns:
|
||||
from_state__timestamp_0
|
||||
reads_aux__0__base__prev_timestamp_0
|
||||
reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0
|
||||
@@ -21,8 +21,6 @@ Symbolic machine using 22 unique main columns:
|
||||
b__2_0
|
||||
b__3_0
|
||||
cmp_result_0
|
||||
a_msb_f_0
|
||||
b_msb_f_0
|
||||
diff_marker__0_0
|
||||
diff_marker__1_0
|
||||
diff_marker__2_0
|
||||
@@ -48,15 +46,12 @@ mult=is_valid * 1, args=[15360 * reads_aux__1__base__prev_timestamp_0 + 15360 *
|
||||
|
||||
// Bus 6 (BITWISE_LOOKUP):
|
||||
mult=diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0, args=[diff_val_0 - 1, 0, 0, 0]
|
||||
mult=is_valid * 1, args=[a_msb_f_0, b_msb_f_0, 0, 0]
|
||||
|
||||
// Algebraic constraints:
|
||||
cmp_result_0 * (cmp_result_0 - 1) = 0
|
||||
(a__3_0 - a_msb_f_0) * (a_msb_f_0 + 256 - a__3_0) = 0
|
||||
(b__3_0 - b_msb_f_0) * (b_msb_f_0 + 256 - b__3_0) = 0
|
||||
diff_marker__3_0 * (diff_marker__3_0 - 1) = 0
|
||||
(1 - diff_marker__3_0) * ((b_msb_f_0 - a_msb_f_0) * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__3_0 * ((a_msb_f_0 - b_msb_f_0) * (2 * cmp_result_0 - 1) + diff_val_0) = 0
|
||||
(1 - diff_marker__3_0) * ((b__3_0 - a__3_0) * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__3_0 * ((a__3_0 - b__3_0) * (2 * cmp_result_0 - 1) + diff_val_0) = 0
|
||||
diff_marker__2_0 * (diff_marker__2_0 - 1) = 0
|
||||
(1 - (diff_marker__2_0 + diff_marker__3_0)) * ((b__2_0 - a__2_0) * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__2_0 * ((a__2_0 - b__2_0) * (2 * cmp_result_0 - 1) + diff_val_0) = 0
|
||||
|
||||
@@ -2,11 +2,11 @@ Instructions:
|
||||
SLTU rd_ptr = 8, rs1_ptr = 0, rs2 = 5, rs2_as = 1
|
||||
|
||||
APC advantage:
|
||||
- Main columns: 37 -> 23 (1.61x reduction)
|
||||
- Bus interactions: 18 -> 16 (1.12x reduction)
|
||||
- Constraints: 28 -> 18 (1.56x reduction)
|
||||
- Main columns: 37 -> 22 (1.68x reduction)
|
||||
- Bus interactions: 18 -> 15 (1.20x reduction)
|
||||
- Constraints: 28 -> 17 (1.65x reduction)
|
||||
|
||||
Symbolic machine using 23 unique main columns:
|
||||
Symbolic machine using 22 unique main columns:
|
||||
from_state__timestamp_0
|
||||
reads_aux__0__base__prev_timestamp_0
|
||||
reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0
|
||||
@@ -23,7 +23,6 @@ Symbolic machine using 23 unique main columns:
|
||||
c__2_0
|
||||
c__3_0
|
||||
cmp_result_0
|
||||
c_msb_f_0
|
||||
diff_marker__0_0
|
||||
diff_marker__1_0
|
||||
diff_marker__2_0
|
||||
@@ -53,14 +52,12 @@ mult=is_valid * 1, args=[15360 * writes_aux__base__prev_timestamp_0 + 15360 * wr
|
||||
|
||||
// Bus 6 (BITWISE_LOOKUP):
|
||||
mult=diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0, args=[diff_val_0 - 1, 0, 0, 0]
|
||||
mult=is_valid * 1, args=[c_msb_f_0, 0, 0, 0]
|
||||
|
||||
// Algebraic constraints:
|
||||
cmp_result_0 * (cmp_result_0 - 1) = 0
|
||||
(c__3_0 - c_msb_f_0) * (c_msb_f_0 + 256 - c__3_0) = 0
|
||||
diff_marker__3_0 * (diff_marker__3_0 - 1) = 0
|
||||
(1 - diff_marker__3_0) * (c_msb_f_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__3_0 * (diff_val_0 - c_msb_f_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
(1 - diff_marker__3_0) * (c__3_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__3_0 * (diff_val_0 - c__3_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__2_0 * (diff_marker__2_0 - 1) = 0
|
||||
(1 - (diff_marker__2_0 + diff_marker__3_0)) * (c__2_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
diff_marker__2_0 * (diff_val_0 - c__2_0 * (2 * cmp_result_0 - 1)) = 0
|
||||
|
||||
@@ -17,6 +17,9 @@ log = "0.4.27"
|
||||
pretty_assertions = "1.4.0"
|
||||
itertools = "0.13.0"
|
||||
|
||||
[dev-dependencies]
|
||||
expect-test = "1.5.1"
|
||||
|
||||
[lints]
|
||||
workspace = true
|
||||
|
||||
|
||||
@@ -1,3 +1,4 @@
|
||||
use expect_test::expect;
|
||||
use powdr_number::GoldilocksField;
|
||||
use powdr_pil_analyzer::analyze_string;
|
||||
|
||||
@@ -17,15 +18,16 @@ fn replace_fixed() {
|
||||
X * one = X * zero - zero + Y;
|
||||
one * Y = zero * Y + 7 * X * X;
|
||||
"#;
|
||||
let expectation = r#"namespace N(65536);
|
||||
col witness Y;
|
||||
query |i| {
|
||||
let _: expr = 1_expr;
|
||||
};
|
||||
N::Y = 7 * N::Y * N::Y;
|
||||
"#;
|
||||
let expectation = expect![[r#"
|
||||
namespace N(65536);
|
||||
col witness X;
|
||||
query |i| {
|
||||
let _: expr = 1_expr;
|
||||
};
|
||||
N::X = 7 * N::X * N::X;
|
||||
"#]];
|
||||
let optimized = optimize(analyze_string::<GoldilocksField>(input).unwrap()).to_string();
|
||||
assert_eq!(optimized, expectation);
|
||||
expectation.assert_eq(&optimized);
|
||||
}
|
||||
|
||||
#[test]
|
||||
@@ -138,16 +140,17 @@ fn zero_sized_array() {
|
||||
let t: col = |i| std::array::len(y);
|
||||
x[0] = t;
|
||||
"#;
|
||||
let expectation = r#"namespace std::array(65536);
|
||||
let<T> len: T[] -> int = [];
|
||||
namespace N(65536);
|
||||
col witness x[1];
|
||||
col witness y[0];
|
||||
col fixed t(i) { std::array::len::<expr>(N::y) };
|
||||
N::x[0] = N::t;
|
||||
"#;
|
||||
let expectation = expect![[r#"
|
||||
namespace std::array(65536);
|
||||
let<T> len: T[] -> int = [];
|
||||
namespace N(65536);
|
||||
col witness x[1];
|
||||
col witness y[0];
|
||||
col fixed t(i) { std::array::len::<expr>(N::y) };
|
||||
N::t = N::x[0];
|
||||
"#]];
|
||||
let optimized = optimize(analyze_string::<GoldilocksField>(input).unwrap()).to_string();
|
||||
assert_eq!(optimized, expectation);
|
||||
expectation.assert_eq(&optimized);
|
||||
}
|
||||
|
||||
#[test]
|
||||
@@ -212,14 +215,16 @@ fn remove_unreferenced_parts_of_arrays() {
|
||||
let inte: inter[5] = x;
|
||||
x[2] = inte[4];
|
||||
"#;
|
||||
let expectation = r#"namespace N(65536);
|
||||
col witness x[5];
|
||||
col inte[5] = [N::x[0], N::x[1], N::x[2], N::x[3], N::x[4]];
|
||||
N::x[2] = N::inte[4];
|
||||
"#;
|
||||
let expectation = expect![[r#"
|
||||
namespace N(65536);
|
||||
col witness x[5];
|
||||
col inte[5] = [N::x[0], N::x[1], N::x[2], N::x[3], N::x[4]];
|
||||
N::inte[4] = N::x[2];
|
||||
"#]];
|
||||
let optimized = optimize(analyze_string::<GoldilocksField>(input).unwrap());
|
||||
assert_eq!(optimized.intermediate_count(), 5);
|
||||
assert_eq!(optimized.to_string(), expectation);
|
||||
let optimized = optimize(analyze_string::<GoldilocksField>(input).unwrap()).to_string();
|
||||
expectation.assert_eq(&optimized);
|
||||
}
|
||||
|
||||
#[test]
|
||||
@@ -398,12 +403,13 @@ fn equal_constrained_array_elements_empty() {
|
||||
col witness w[20];
|
||||
w[4] = w[7];
|
||||
"#;
|
||||
let expectation = r#"namespace N(65536);
|
||||
col witness w[20];
|
||||
N::w[4] = N::w[7];
|
||||
"#;
|
||||
let expectation = expect![[r#"
|
||||
namespace N(65536);
|
||||
col witness w[20];
|
||||
N::w[7] = N::w[4];
|
||||
"#]];
|
||||
let optimized = optimize(analyze_string::<GoldilocksField>(input).unwrap()).to_string();
|
||||
assert_eq!(optimized, expectation);
|
||||
expectation.assert_eq(&optimized);
|
||||
}
|
||||
|
||||
#[test]
|
||||
@@ -415,15 +421,16 @@ fn equal_constrained_array_elements_query() {
|
||||
let _ = w[4] + w[7] - w[5];
|
||||
};
|
||||
"#;
|
||||
let expectation = r#"namespace N(65536);
|
||||
col witness w[20];
|
||||
N::w[4] = N::w[7];
|
||||
query |i| {
|
||||
let _: expr = N::w[4_int] + N::w[7_int] - N::w[5_int];
|
||||
};
|
||||
"#;
|
||||
let expectation = expect![[r#"
|
||||
namespace N(65536);
|
||||
col witness w[20];
|
||||
query |i| {
|
||||
let _: expr = N::w[4_int] + N::w[7_int] - N::w[5_int];
|
||||
};
|
||||
N::w[7] = N::w[4];
|
||||
"#]];
|
||||
let optimized = optimize(analyze_string::<GoldilocksField>(input).unwrap()).to_string();
|
||||
assert_eq!(optimized, expectation);
|
||||
expectation.assert_eq(&optimized);
|
||||
}
|
||||
|
||||
#[test]
|
||||
@@ -436,14 +443,16 @@ fn equal_constrained_array_elements() {
|
||||
x = w[3];
|
||||
w[7] + w[1] + x = 5;
|
||||
"#;
|
||||
let expectation = r#"namespace N(65536);
|
||||
let expectation = expect![
|
||||
r#"namespace N(65536);
|
||||
col witness w[20];
|
||||
N::w[4] = N::w[7];
|
||||
N::w[3] = N::w[5];
|
||||
N::w[1] + N::w[3] + N::w[7] = 5;
|
||||
"#;
|
||||
N::w[1] + N::w[3] + N::w[4] = 5;
|
||||
N::w[7] = N::w[4];
|
||||
N::w[5] = N::w[3];
|
||||
"#
|
||||
];
|
||||
let optimized = optimize(analyze_string::<GoldilocksField>(input).unwrap()).to_string();
|
||||
assert_eq!(optimized, expectation);
|
||||
expectation.assert_eq(&optimized);
|
||||
}
|
||||
|
||||
#[test]
|
||||
|
||||
@@ -1,34 +0,0 @@
|
||||
use powdr_number::{FieldElement, GoldilocksField};
|
||||
use powdr_pipeline::pipeline::Columns;
|
||||
use powdr_pipeline::Pipeline;
|
||||
use test_log::test;
|
||||
|
||||
fn run_witgen_pil<T: FieldElement>(pil: &str) -> Columns<T> {
|
||||
Pipeline::default()
|
||||
.from_pil_string(pil.to_string())
|
||||
.compute_witness()
|
||||
.unwrap()
|
||||
.0
|
||||
.clone()
|
||||
}
|
||||
|
||||
#[test]
|
||||
#[should_panic = "Publics are referenced by more than one machine: Machine1::pub"]
|
||||
fn two_machines_conflicting_public() {
|
||||
// This test *should* fail, because two machines access the same
|
||||
// public, but assign different values to it.
|
||||
let src = r#"
|
||||
namespace Machine1(4);
|
||||
col witness y;
|
||||
[ 42, y ] in [ Machine2.x, Machine2.y ];
|
||||
// y will be 43 on all rows
|
||||
public pub = y(3);
|
||||
y - pub = 0;
|
||||
namespace Machine2(8);
|
||||
col witness x, y;
|
||||
y = x + 1;
|
||||
// x will be 42 on all rows
|
||||
x - Machine1::pub = 0;
|
||||
"#;
|
||||
run_witgen_pil::<GoldilocksField>(src);
|
||||
}
|
||||
Reference in New Issue
Block a user