From cce4375497acee48edaf95a1958ebafd49f77497 Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 20 Dec 2024 11:32:35 +0000 Subject: [PATCH 01/31] Single step processor. --- executor/src/witgen/jit/mod.rs | 1 + .../src/witgen/jit/single_step_processor.rs | 154 ++++++++++++++++++ 2 files changed, 155 insertions(+) create mode 100644 executor/src/witgen/jit/single_step_processor.rs diff --git a/executor/src/witgen/jit/mod.rs b/executor/src/witgen/jit/mod.rs index 91df4a9c6f..c2b33e43f2 100644 --- a/executor/src/witgen/jit/mod.rs +++ b/executor/src/witgen/jit/mod.rs @@ -3,6 +3,7 @@ mod block_machine_processor; mod compiler; mod effect; pub(crate) mod function_cache; +mod single_step_processor; mod symbolic_expression; mod variable; pub(crate) mod witgen_inference; diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs new file mode 100644 index 0000000000..8b949921e4 --- /dev/null +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -0,0 +1,154 @@ +#![allow(dead_code)] +use std::collections::HashSet; + +use itertools::Itertools; +use powdr_ast::analyzed::AlgebraicReference; +use powdr_number::FieldElement; + +use crate::witgen::{machines::MachineParts, FixedData}; + +use super::{ + effect::Effect, + variable::{Cell, Variable}, + witgen_inference::{FixedEvaluator, WitgenInference}, +}; + +/// A processor for generating JIT code that computes the next row from the previous row. +pub struct SingleStepProcessor<'a, T: FieldElement> { + fixed_data: &'a FixedData<'a, T>, + machine_parts: MachineParts<'a, T>, +} + +impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { + pub fn new(fixed_data: &'a FixedData<'a, T>, machine_parts: MachineParts<'a, T>) -> Self { + SingleStepProcessor { + fixed_data, + machine_parts, + } + } + + pub fn generate_code(&self) -> Result>, String> { + // All witness columns in row 0 are known. + let known_variables = self.machine_parts.witnesses.iter().map(|id| { + Variable::Cell(Cell { + column_name: self.fixed_data.column_name(id).to_string(), + id: id.id, + row_offset: 0, + }) + }); + let mut witgen = WitgenInference::new(self.fixed_data, self, known_variables); + + let mut complete = HashSet::new(); + for iteration in 0.. { + let mut progress = false; + + for id in &self.machine_parts.identities { + let row_offset = if id.contains_next_ref() { 0 } else { 1 }; + if !complete.contains(&(id.id(), row_offset)) { + let result = witgen.process_identity(id, row_offset); + if result.complete { + complete.insert((id.id(), row_offset)); + } + progress |= result.progress; + } + } + if !progress { + log::debug!("Finishing after {iteration} iterations"); + break; + } + } + + // Check that we could derive all witness values in the next row. + let unknown_witnesses = self + .machine_parts + .witnesses + .iter() + .filter(|wit| { + !witgen.is_known(&Variable::Cell(Cell { + column_name: self.fixed_data.column_name(wit).to_string(), + id: wit.id, + row_offset: 1, + })) + }) + .sorted() + .collect_vec(); + + // TODO also check that we completed all machine calls? + if unknown_witnesses.is_empty() { + Ok(witgen.code()) + } else { + Err(format!( + "Unable to derive algorithm to compute values for witness columns in the next row for the following columns: {}", + unknown_witnesses.iter().map(|wit| self.fixed_data.column_name(wit)).format(", ") + )) + } + } +} + +impl FixedEvaluator for &SingleStepProcessor<'_, T> { + fn evaluate(&self, _var: &AlgebraicReference, _row_offset: i32) -> Option { + // We can only return something here if the fixed column is constant + // in the region wer are considering. + // This might be the case if we know we are not evaluating the first or the last + // row, but this is not yet implemented. + None + } +} + +#[cfg(test)] +mod test { + + use powdr_ast::analyzed::Analyzed; + use powdr_number::GoldilocksField; + + use crate::{ + constant_evaluator, + witgen::{ + global_constraints, + jit::{effect::Effect, test_util::format_code}, + machines::MachineParts, + FixedData, + }, + }; + + use super::{SingleStepProcessor, Variable}; + + fn generate_single_step( + input_pil: &str, + ) -> Result>, String> { + let analyzed: Analyzed = + powdr_pil_analyzer::analyze_string(input_pil).unwrap(); + let fixed_col_vals = constant_evaluator::generate(&analyzed); + let fixed_data = FixedData::new(&analyzed, &fixed_col_vals, &[], Default::default(), 0); + let (fixed_data, retained_identities) = + global_constraints::set_global_constraints(fixed_data, &analyzed.identities); + + let witness_columns = analyzed + .committed_polys_in_source_order() + .flat_map(|(symbol, _)| symbol.array_elements().map(|(_, id)| id)) + .collect(); + + let machine_parts = MachineParts::new( + &fixed_data, + // no connections + Default::default(), + retained_identities, + witness_columns, + // No prover functions + Vec::new(), + ); + + SingleStepProcessor { + fixed_data: &fixed_data, + machine_parts, + } + .generate_code() + } + + #[test] + fn fib() { + let input = "let X; let Y; X' = Y; Y' = X + Y;"; + let code = generate_single_step(input).unwrap(); + assert_eq!(format_code(&code), "X[1] = Y[0];\nY[1] = (X[0] + Y[0]);"); + } +} From c54c0dd1c25358b93ef4786927c344d01dc3e076 Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 20 Dec 2024 11:38:59 +0000 Subject: [PATCH 02/31] Negative test. --- executor/src/witgen/jit/single_step_processor.rs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index 8b949921e4..c32db27a96 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -151,4 +151,14 @@ mod test { let code = generate_single_step(input).unwrap(); assert_eq!(format_code(&code), "X[1] = Y[0];\nY[1] = (X[0] + Y[0]);"); } + + #[test] + fn no_progress() { + let input = "let X; let Y; X' = X;"; + let err = generate_single_step(input).err().unwrap(); + assert_eq!( + err.to_string(), + "Unable to derive algorithm to compute values for witness columns in the next row for the following columns: Y" + ); + } } From eb245acf9760006375a6df94239b238b8bc63ef7 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 2 Jan 2025 13:14:24 +0100 Subject: [PATCH 03/31] Apply suggestions from code review Co-authored-by: Georg Wiese --- executor/src/witgen/jit/single_step_processor.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index c32db27a96..6f93e05ec3 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -73,8 +73,8 @@ impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { .sorted() .collect_vec(); - // TODO also check that we completed all machine calls? if unknown_witnesses.is_empty() { + assert_eq!(complete, self.machine_parts.identities.len()); Ok(witgen.code()) } else { Err(format!( @@ -88,7 +88,7 @@ impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { impl FixedEvaluator for &SingleStepProcessor<'_, T> { fn evaluate(&self, _var: &AlgebraicReference, _row_offset: i32) -> Option { // We can only return something here if the fixed column is constant - // in the region wer are considering. + // in the region we are considering. // This might be the case if we know we are not evaluating the first or the last // row, but this is not yet implemented. None From 1588eb2077f045cf563e99c8e031c968c6084b7a Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 2 Jan 2025 13:25:52 +0000 Subject: [PATCH 04/31] adjust tests. --- .../src/witgen/jit/single_step_processor.rs | 48 +++++++++++-------- 1 file changed, 29 insertions(+), 19 deletions(-) diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index 6f93e05ec3..af67901487 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -27,7 +27,10 @@ impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { } } - pub fn generate_code(&self) -> Result>, String> { + pub fn generate_code + Clone>( + &self, + can_process: CanProcess, + ) -> Result>, String> { // All witness columns in row 0 are known. let known_variables = self.machine_parts.witnesses.iter().map(|id| { Variable::Cell(Cell { @@ -43,11 +46,11 @@ impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { let mut progress = false; for id in &self.machine_parts.identities { - let row_offset = if id.contains_next_ref() { 0 } else { 1 }; - if !complete.contains(&(id.id(), row_offset)) { - let result = witgen.process_identity(id, row_offset); + if !complete.contains(&id.id()) { + let row_offset = if id.contains_next_ref() { 0 } else { 1 }; + let result = witgen.process_identity(can_process.clone(), id, row_offset); if result.complete { - complete.insert((id.id(), row_offset)); + complete.insert(id.id()); } progress |= result.progress; } @@ -73,13 +76,14 @@ impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { .sorted() .collect_vec(); - if unknown_witnesses.is_empty() { - assert_eq!(complete, self.machine_parts.identities.len()); + let missing_identities = self.machine_parts.len() - complete.len(); + if unknown_witnesses.is_empty() && missing_identities == 0{ Ok(witgen.code()) } else { Err(format!( - "Unable to derive algorithm to compute values for witness columns in the next row for the following columns: {}", - unknown_witnesses.iter().map(|wit| self.fixed_data.column_name(wit)).format(", ") + "Unable to derive algorithm to compute values for witness columns in the next row for the following columns:\n{}\nand {missing_identities} identities are missing.", + unknown_witnesses.iter().map(|wit| self.fixed_data.column_name(wit)).format(", "), + )) } } @@ -104,10 +108,7 @@ mod test { use crate::{ constant_evaluator, witgen::{ - global_constraints, - jit::{effect::Effect, test_util::format_code}, - machines::MachineParts, - FixedData, + data_structures::mutable_state::MutableState, global_constraints, jit::{effect::Effect, test_util::read_pil}, machines::{machine_extractor::MachineExtractor, KnownMachine, MachineParts}, FixedData }, }; @@ -116,12 +117,18 @@ mod test { fn generate_single_step( input_pil: &str, ) -> Result>, String> { - let analyzed: Analyzed = - powdr_pil_analyzer::analyze_string(input_pil).unwrap(); - let fixed_col_vals = constant_evaluator::generate(&analyzed); + let (analyzed, fixed_col_vals) = read_pil(input_pil); + let fixed_data = FixedData::new(&analyzed, &fixed_col_vals, &[], Default::default(), 0); let (fixed_data, retained_identities) = global_constraints::set_global_constraints(fixed_data, &analyzed.identities); + let machines = MachineExtractor::new(&fixed_data).split_out_machines(retained_identities); + let mutable_state = MutableState::new(machines.into_iter(), &|_| { + Err("Query not implemented".to_string()) + }); + + let KnownMachine::DynamicMachine(machine)= mutable_state.get_machine("Main") else { panic!(); } + assert_eq!(machines.len(), 1); let witness_columns = analyzed .committed_polys_in_source_order() @@ -137,24 +144,27 @@ mod test { // No prover functions Vec::new(), ); + let mutable_state = MutableState::new(machines.into_iter(), &|_| { + Err("Query not implemented".to_string()) + }); SingleStepProcessor { fixed_data: &fixed_data, machine_parts, } - .generate_code() + .generate_code(&mutable_state) } #[test] fn fib() { - let input = "let X; let Y; X' = Y; Y' = X + Y;"; + let input = "namespace Main(256); let X; let Y; X' = Y; Y' = X + Y;"; let code = generate_single_step(input).unwrap(); assert_eq!(format_code(&code), "X[1] = Y[0];\nY[1] = (X[0] + Y[0]);"); } #[test] fn no_progress() { - let input = "let X; let Y; X' = X;"; + let input = "namespace Main(256); let X; let Y; X' = X;"; let err = generate_single_step(input).err().unwrap(); assert_eq!( err.to_string(), From cc70c191b9aaa51da7cd9a3da42895d1a3df361f Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 2 Jan 2025 13:33:41 +0000 Subject: [PATCH 05/31] Remove test function. --- .../witgen/data_structures/mutable_state.rs | 14 ---------- .../src/witgen/jit/block_machine_processor.rs | 28 +++++++++++-------- 2 files changed, 16 insertions(+), 26 deletions(-) diff --git a/executor/src/witgen/data_structures/mutable_state.rs b/executor/src/witgen/data_structures/mutable_state.rs index c8777af7eb..37564084bb 100644 --- a/executor/src/witgen/data_structures/mutable_state.rs +++ b/executor/src/witgen/data_structures/mutable_state.rs @@ -42,20 +42,6 @@ impl<'a, T: FieldElement, Q: QueryCallback> MutableState<'a, T, Q> { } } - #[cfg(test)] - pub fn get_machine(&self, substring: &str) -> &RefCell> { - use itertools::Itertools; - - self.machines - .iter() - .filter(|m| m.borrow().name().contains(substring)) - .exactly_one() - .map_err(|e| { - format!("Expected exactly one machine with substring '{substring}', but found {e}.") - }) - .unwrap() - } - /// Runs the first machine (unless there are no machines) end returns the generated columns. /// The first machine might call other machines, which is handled automatically. pub fn run(self) -> HashMap> { diff --git a/executor/src/witgen/jit/block_machine_processor.rs b/executor/src/witgen/jit/block_machine_processor.rs index fa8ad9effc..c0b1067625 100644 --- a/executor/src/witgen/jit/block_machine_processor.rs +++ b/executor/src/witgen/jit/block_machine_processor.rs @@ -195,31 +195,35 @@ mod test { let (fixed_data, retained_identities) = global_constraints::set_global_constraints(fixed_data, &analyzed.identities); let machines = MachineExtractor::new(&fixed_data).split_out_machines(retained_identities); - let mutable_state = MutableState::new(machines.into_iter(), &|_| { - Err("Query not implemented".to_string()) - }); - - let machine = mutable_state.get_machine(machine_name); - let ((machine_parts, block_size, latch_row), connection_ids) = match *machine.borrow() { - KnownMachine::BlockMachine(ref m) => (m.machine_info(), m.identity_ids()), - _ => panic!("Expected a block machine"), + let [KnownMachine::BlockMachine(machine)] = machines + .iter() + .filter(|m| m.name().contains(machine_name)) + .collect_vec() + .as_slice() + else { + panic!("Expected exactly one matching block machine") }; - assert_eq!(connection_ids.len(), 1); - + let (machine_parts, block_size, latch_row) = machine.machine_info(); + assert_eq!(machine_parts.connections.len(), 1); + let connection_id = *machine_parts.connections.keys().next().unwrap(); let processor = BlockMachineProcessor { fixed_data: &fixed_data, - machine_parts, + machine_parts: machine_parts.clone(), block_size, latch_row, }; + let mutable_state = MutableState::new(machines.into_iter(), &|_| { + Err("Query not implemented".to_string()) + }); + let known_values = BitVec::from_iter( (0..num_inputs) .map(|_| true) .chain((0..num_outputs).map(|_| false)), ); - processor.generate_code(&mutable_state, connection_ids[0], &known_values) + processor.generate_code(&mutable_state, connection_id, &known_values) } #[test] From 96d5506994eac037dccc6ec0da00663d85e3dae4 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 2 Jan 2025 14:04:46 +0000 Subject: [PATCH 06/31] Fix testing functions. --- .../src/witgen/jit/single_step_processor.rs | 72 +++++++++---------- .../src/witgen/machines/dynamic_machine.rs | 5 ++ 2 files changed, 40 insertions(+), 37 deletions(-) diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index af67901487..c2780c5241 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -10,7 +10,7 @@ use crate::witgen::{machines::MachineParts, FixedData}; use super::{ effect::Effect, variable::{Cell, Variable}, - witgen_inference::{FixedEvaluator, WitgenInference}, + witgen_inference::{CanProcessCall, FixedEvaluator, WitgenInference}, }; /// A processor for generating JIT code that computes the next row from the previous row. @@ -76,14 +76,13 @@ impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { .sorted() .collect_vec(); - let missing_identities = self.machine_parts.len() - complete.len(); - if unknown_witnesses.is_empty() && missing_identities == 0{ + let missing_identities = self.machine_parts.identities.len() - complete.len(); + if unknown_witnesses.is_empty() && missing_identities == 0 { Ok(witgen.code()) } else { Err(format!( "Unable to derive algorithm to compute values for witness columns in the next row for the following columns:\n{}\nand {missing_identities} identities are missing.", - unknown_witnesses.iter().map(|wit| self.fixed_data.column_name(wit)).format(", "), - + unknown_witnesses.iter().map(|wit| self.fixed_data.column_name(wit)).format(", ") )) } } @@ -102,20 +101,26 @@ impl FixedEvaluator for &SingleStepProcessor<'_, T> { #[cfg(test)] mod test { - use powdr_ast::analyzed::Analyzed; + use itertools::Itertools; + use powdr_number::GoldilocksField; - use crate::{ - constant_evaluator, - witgen::{ - data_structures::mutable_state::MutableState, global_constraints, jit::{effect::Effect, test_util::read_pil}, machines::{machine_extractor::MachineExtractor, KnownMachine, MachineParts}, FixedData + use crate::witgen::{ + data_structures::mutable_state::MutableState, + global_constraints, + jit::{ + effect::{format_code, Effect}, + test_util::read_pil, }, + machines::{machine_extractor::MachineExtractor, KnownMachine, Machine}, + FixedData, }; use super::{SingleStepProcessor, Variable}; fn generate_single_step( input_pil: &str, + machine_name: &str, ) -> Result>, String> { let (analyzed, fixed_col_vals) = read_pil(input_pil); @@ -123,27 +128,15 @@ mod test { let (fixed_data, retained_identities) = global_constraints::set_global_constraints(fixed_data, &analyzed.identities); let machines = MachineExtractor::new(&fixed_data).split_out_machines(retained_identities); - let mutable_state = MutableState::new(machines.into_iter(), &|_| { - Err("Query not implemented".to_string()) - }); - - let KnownMachine::DynamicMachine(machine)= mutable_state.get_machine("Main") else { panic!(); } - assert_eq!(machines.len(), 1); - - let witness_columns = analyzed - .committed_polys_in_source_order() - .flat_map(|(symbol, _)| symbol.array_elements().map(|(_, id)| id)) - .collect(); - - let machine_parts = MachineParts::new( - &fixed_data, - // no connections - Default::default(), - retained_identities, - witness_columns, - // No prover functions - Vec::new(), - ); + let [KnownMachine::DynamicMachine(machine)] = machines + .iter() + .filter(|m| m.name().contains(machine_name)) + .collect_vec() + .as_slice() + else { + panic!("Expected exactly one matching dynamic machine") + }; + let machine_parts = machine.machine_parts().clone(); let mutable_state = MutableState::new(machines.into_iter(), &|_| { Err("Query not implemented".to_string()) }); @@ -157,18 +150,23 @@ mod test { #[test] fn fib() { - let input = "namespace Main(256); let X; let Y; X' = Y; Y' = X + Y;"; - let code = generate_single_step(input).unwrap(); - assert_eq!(format_code(&code), "X[1] = Y[0];\nY[1] = (X[0] + Y[0]);"); + let input = "namespace M(256); let X; let Y; X' = Y; Y' = X + Y;"; + let code = generate_single_step(input, "M").unwrap(); + assert_eq!( + format_code(&code), + "M::X[1] = M::Y[0];\nM::Y[1] = (M::X[0] + M::Y[0]);" + ); } #[test] fn no_progress() { - let input = "namespace Main(256); let X; let Y; X' = X;"; - let err = generate_single_step(input).err().unwrap(); + let input = "namespace M(256); let X; let Y; X' = X;"; + let err = generate_single_step(input, "M").err().unwrap(); assert_eq!( err.to_string(), - "Unable to derive algorithm to compute values for witness columns in the next row for the following columns: Y" + "Unable to derive algorithm to compute values for witness columns in the next row for the following columns:\n\ + M::Y\n\ + and 0 identities are missing." ); } } diff --git a/executor/src/witgen/machines/dynamic_machine.rs b/executor/src/witgen/machines/dynamic_machine.rs index 26f25f1bd8..762d662cd1 100644 --- a/executor/src/witgen/machines/dynamic_machine.rs +++ b/executor/src/witgen/machines/dynamic_machine.rs @@ -278,4 +278,9 @@ impl<'a, T: FieldElement> DynamicMachine<'a, T> { ); } } + + #[cfg(test)] + pub fn machine_parts(&self) -> &MachineParts<'a, T> { + &self.parts + } } From 64de47cdfe68d86eed963b516a6da21e58bd9170 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 13 Jan 2025 17:59:51 +0000 Subject: [PATCH 07/31] Provide completed identities and store `completed` inside witgen_inference. --- .../src/witgen/jit/block_machine_processor.rs | 2 +- executor/src/witgen/jit/processor.rs | 43 +++++-------- .../src/witgen/jit/single_step_processor.rs | 29 +++++++-- executor/src/witgen/jit/witgen_inference.rs | 64 +++++++++++++++---- 4 files changed, 93 insertions(+), 45 deletions(-) diff --git a/executor/src/witgen/jit/block_machine_processor.rs b/executor/src/witgen/jit/block_machine_processor.rs index c691b0d51a..6d152b7caa 100644 --- a/executor/src/witgen/jit/block_machine_processor.rs +++ b/executor/src/witgen/jit/block_machine_processor.rs @@ -56,7 +56,7 @@ impl<'a, T: FieldElement> BlockMachineProcessor<'a, T> { .enumerate() .filter_map(|(i, is_input)| is_input.then_some(Variable::Param(i))) .collect::>(); - let mut witgen = WitgenInference::new(self.fixed_data, self, known_variables); + let mut witgen = WitgenInference::new(self.fixed_data, self, known_variables, []); // In the latch row, set the RHS selector to 1. let selector = &connection.right.selector; diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 576322ad5a..4d6add4aa3 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -1,6 +1,6 @@ #![allow(dead_code)] use std::{ - collections::{BTreeSet, HashSet}, + collections::BTreeSet, fmt::{self, Display, Formatter, Write}, }; @@ -60,19 +60,17 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv can_process: CanProcess, witgen: WitgenInference<'a, T, FixedEval>, ) -> Result>, Error<'a, T>> { - let complete = Default::default(); let branch_depth = 0; - self.generate_code_for_branch(can_process, witgen, complete, branch_depth) + self.generate_code_for_branch(can_process, witgen, branch_depth) } fn generate_code_for_branch + Clone>( &self, can_process: CanProcess, mut witgen: WitgenInference<'a, T, FixedEval>, - mut complete: HashSet<(u64, i32)>, branch_depth: usize, ) -> Result>, Error<'a, T>> { - self.process_until_no_progress(can_process.clone(), &mut witgen, &mut complete); + self.process_until_no_progress(can_process.clone(), &mut witgen); if self.check_block_shape { // Check that the "spill" into the previous block is compatible @@ -94,7 +92,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv .cloned() .collect_vec(); - let incomplete_machine_calls = self.incomplete_machine_calls(&complete); + let incomplete_machine_calls = self.incomplete_machine_calls(&witgen); if missing_variables.is_empty() && incomplete_machine_calls.is_empty() { return Ok(witgen.code()); } @@ -117,7 +115,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv let incomplete_identities = self .identities .iter() - .filter(|(id, row_offset)| !complete.contains(&(id.id(), *row_offset))) + .filter(|(id, row_offset)| !witgen.is_complete(id, *row_offset)) .map(|(id, row_offset)| (*id, *row_offset)) .collect_vec(); return Err(Error { @@ -142,14 +140,10 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv // TODO Tuning: If this fails (or also if it does not generate progress right away), // we could also choose a different variable to branch on. - let left_branch_code = self.generate_code_for_branch( - can_process.clone(), - first_branch, - complete.clone(), - branch_depth + 1, - )?; + let left_branch_code = + self.generate_code_for_branch(can_process.clone(), first_branch, branch_depth + 1)?; let right_branch_code = - self.generate_code_for_branch(can_process, second_branch, complete, branch_depth + 1)?; + self.generate_code_for_branch(can_process, second_branch, branch_depth + 1)?; let code = if left_branch_code == right_branch_code { common_code.into_iter().chain(left_branch_code).collect() } else { @@ -170,7 +164,6 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv &self, can_process: CanProcess, witgen: &mut WitgenInference<'a, T, FixedEval>, - complete: &mut HashSet<(u64, i32)>, ) { let mut progress = true; while progress { @@ -181,14 +174,9 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv // to other known (but not concrete) variables. for (id, row_offset) in &self.identities { - if complete.contains(&(id.id(), *row_offset)) { - continue; - } - let result = witgen.process_identity(can_process.clone(), id, *row_offset); - progress |= result.progress; - if result.complete { - complete.insert((id.id(), *row_offset)); - } + progress |= witgen + .process_identity(can_process.clone(), id, *row_offset) + .progress; } } } @@ -197,7 +185,10 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv /// So, the underlying lookup / permutation / bus argument likely does not hold. /// This function checks that all machine calls are complete, at least for a window of rows. /// It returns the list of incomplete calls, if any. - fn incomplete_machine_calls(&self, complete: &HashSet<(u64, i32)>) -> Vec<(&Identity, i32)> { + fn incomplete_machine_calls( + &self, + witgen: &WitgenInference<'a, T, FixedEval>, + ) -> Vec<(&Identity, i32)> { self.identities .iter() .map(|(id, _)| id) @@ -207,7 +198,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv let rows = self.rows_for_identity(call); let complete_rows = rows .iter() - .filter(|&&row| complete.contains(&(call.id(), row))) + .filter(|&&row| witgen.is_complete(call, row)) .collect::>(); // We might process more rows than `self.block_size`, so we check // that the complete calls are on consecutive rows. @@ -223,7 +214,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv } } rows.iter() - .filter(|&row| !complete.contains(&(call.id(), *row))) + .filter(|&row| !witgen.is_complete(call, *row)) .map(|row| (call, *row)) .collect::>() }) diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index 8acbe0680c..7a0d0f7859 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -45,12 +45,31 @@ impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { let known_variables = all_witnesses.iter().map(|&id| self.cell(id, 0)); // and we want to know the ones in the next row. let requested_known = all_witnesses.iter().map(|&id| self.cell(id, 1)); - let identities = self.machine_parts.identities.iter().map(|&id| { - let row_offset = if id.contains_next_ref() { 0 } else { 1 }; - (id, row_offset) - }); + // Identities that span two rows are only processed on row 0, + // the others are processed on both rows. + let mut complete_identities = vec![]; + let identities = self + .machine_parts + .identities + .iter() + .flat_map(|&id| { + if id.contains_next_ref() { + vec![(id, 0)] + } else { + // Process it on both rows, but do not call it on row 0 if it is + // a submachine call. + complete_identities.push((id.id(), 0)); + vec![(id, 0), (id, 1)] + } + }) + .collect_vec(); let block_size = 1; - let witgen = WitgenInference::new(self.fixed_data, NoEval, known_variables); + let witgen = WitgenInference::new( + self.fixed_data, + NoEval, + known_variables, + complete_identities, + ); Processor::new( self.fixed_data, diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 00dd92b7cb..38dfc0ac0e 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -40,6 +40,9 @@ pub struct WitgenInference<'a, T: FieldElement, FixedEval> { fixed_evaluator: FixedEval, derived_range_constraints: HashMap>, known_variables: HashSet, + /// Identities where we do not want to generate a submachine call + /// to avoid two calls to the same submachine on the same row. + complete_identities: HashSet<(u64, i32)>, /// Internal equalities we were not able to solve yet. assignments: Vec>, code: Vec>, @@ -77,12 +80,14 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F fixed_data: &'a FixedData<'a, T>, fixed_evaluator: FixedEval, known_variables: impl IntoIterator, + complete_identities: impl IntoIterator, ) -> Self { Self { fixed_data, fixed_evaluator, derived_range_constraints: Default::default(), known_variables: known_variables.into_iter().collect(), + complete_identities: complete_identities.into_iter().collect(), assignments: Default::default(), code: Default::default(), } @@ -100,6 +105,11 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F self.known_variables.contains(variable) } + pub fn is_complete(&self, identity: &Identity, row_offset: i32) -> bool { + self.complete_identities + .contains(&(identity.id(), row_offset)) + } + pub fn value(&self, variable: &Variable) -> Value { let rc = self.range_constraint(variable); if let Some(val) = rc.try_to_single_value() { @@ -148,6 +158,13 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F id: &'a Identity, row_offset: i32, ) -> ProcessSummary { + // TODO remove this once we propagate range constraints. + if self.is_complete(id, row_offset) { + return ProcessSummary { + complete: true, + progress: false, + }; + } let result = match id { Identity::Polynomial(PolynomialIdentity { expression, .. }) => { self.process_equality_on_row(expression, row_offset, T::from(0).into()) @@ -166,7 +183,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F Identity::PhantomBusInteraction(_) => ProcessResult::empty(), Identity::Connect(_) => ProcessResult::empty(), }; - self.ingest_effects(result) + self.ingest_effects(result, Some((id.id(), row_offset))) } /// Process the constraint that the expression evaluated at the given offset equals the given value. @@ -294,7 +311,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F }; let r = self.process_equality_on_row(assignment.lhs, assignment.row_offset, rhs); - let summary = self.ingest_effects(r); + let summary = self.ingest_effects(r, None); progress |= summary.progress; // If it is not complete, queue it again. (!summary.complete).then_some(assignment) @@ -307,33 +324,54 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } } - fn ingest_effects(&mut self, process_result: ProcessResult) -> ProcessSummary { + /// Analyze the effects and update the internal state. + /// If the effect is the result of a machine call, `identity_id` must be given + /// to avoid two calls to the same sub-machine on the same row. + fn ingest_effects( + &mut self, + process_result: ProcessResult, + identity_id: Option<(u64, i32)>, + ) -> ProcessSummary { let mut progress = false; for e in process_result.effects { match &e { Effect::Assignment(variable, assignment) => { - assert!(self.known_variables.insert(variable.clone())); // If the variable was determined to be a constant, we add this // as a range constraint, so we can use it in future evaluations. - self.add_range_constraint(variable.clone(), assignment.range_constraint()); - progress = true; - self.code.push(e); + progress |= + self.add_range_constraint(variable.clone(), assignment.range_constraint()); + if !self.is_known(variable) { + self.known_variables.insert(variable.clone()); + progress = true; + self.code.push(e); + } } Effect::RangeConstraint(variable, rc) => { progress |= self.add_range_constraint(variable.clone(), rc.clone()); } Effect::MachineCall(_, _, vars) => { - for v in vars { - // Inputs are already known, but it does not hurt to add all of them. - self.known_variables.insert(v.clone()); + // If the machine call is already complete, it means that we have + // processed itand created code for it in the past. We might still process it + // multiple times to get better range constraints. + if self.complete_identities.contains(&identity_id.unwrap()) { + for v in vars { + // Inputs are already known, but it does not hurt to add all of them. + self.known_variables.insert(v.clone()); + } + progress = true; + + self.code.push(e); } - progress = true; - self.code.push(e); } Effect::Assertion(_) => self.code.push(e), Effect::Branch(..) => unreachable!(), } } + if process_result.complete { + if let Some(identity_id) = identity_id { + self.complete_identities.insert(identity_id); + } + } if progress { self.process_assignments(); } @@ -605,7 +643,7 @@ mod test { }); let ref_eval = FixedEvaluatorForFixedData(&fixed_data); - let mut witgen = WitgenInference::new(&fixed_data, ref_eval, known_cells); + let mut witgen = WitgenInference::new(&fixed_data, ref_eval, known_cells, []); let mut complete = HashSet::new(); let mut counter = 0; let expected_complete = expected_complete.unwrap_or(retained_identities.len() * rows.len()); From f44e52b5c93a3972baa5c7d9953835ae6d762bbf Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 13 Jan 2025 19:23:07 +0000 Subject: [PATCH 08/31] fix --- .../src/witgen/jit/block_machine_processor.rs | 2 +- executor/src/witgen/jit/processor.rs | 25 ++++++++++--------- executor/src/witgen/jit/witgen_inference.rs | 5 ++-- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/executor/src/witgen/jit/block_machine_processor.rs b/executor/src/witgen/jit/block_machine_processor.rs index 6d152b7caa..e9067bbea2 100644 --- a/executor/src/witgen/jit/block_machine_processor.rs +++ b/executor/src/witgen/jit/block_machine_processor.rs @@ -14,7 +14,7 @@ use super::{ }; /// This is a tuning value. It is the maximum nesting depth of branches in the JIT code. -const BLOCK_MACHINE_MAX_BRANCH_DEPTH: usize = 6; +const BLOCK_MACHINE_MAX_BRANCH_DEPTH: usize = 0; /// A processor for generating JIT code for a block machine. pub struct BlockMachineProcessor<'a, T: FieldElement> { diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 4d6add4aa3..fa37aa26c7 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -165,18 +165,19 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv can_process: CanProcess, witgen: &mut WitgenInference<'a, T, FixedEval>, ) { - let mut progress = true; - while progress { - progress = false; - - // TODO At this point, we should call a function on `witgen` - // to propagate known concrete values across the identities - // to other known (but not concrete) variables. - - for (id, row_offset) in &self.identities { - progress |= witgen - .process_identity(can_process.clone(), id, *row_offset) - .progress; + loop { + let progress = self + .identities + .iter() + .map(|(id, row_offset)| { + witgen + .process_identity(can_process.clone(), id, *row_offset) + .progress + }) + .reduce(std::ops::BitOr::bitor) + .unwrap_or(false); + if !progress { + break; } } } diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 38dfc0ac0e..28b6b8f9b0 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -340,8 +340,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F // as a range constraint, so we can use it in future evaluations. progress |= self.add_range_constraint(variable.clone(), assignment.range_constraint()); - if !self.is_known(variable) { - self.known_variables.insert(variable.clone()); + if self.known_variables.insert(variable.clone()) { progress = true; self.code.push(e); } @@ -353,7 +352,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F // If the machine call is already complete, it means that we have // processed itand created code for it in the past. We might still process it // multiple times to get better range constraints. - if self.complete_identities.contains(&identity_id.unwrap()) { + if self.complete_identities.insert(identity_id.unwrap()) { for v in vars { // Inputs are already known, but it does not hurt to add all of them. self.known_variables.insert(v.clone()); From f5c1f74a8216cc5fb9790806cf334e26a6d24e9d Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 10:17:36 +0000 Subject: [PATCH 09/31] Simplify process summary. --- executor/src/witgen/jit/processor.rs | 4 +- executor/src/witgen/jit/witgen_inference.rs | 54 +++++++-------------- 2 files changed, 18 insertions(+), 40 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index fa37aa26c7..d8e516aacd 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -170,9 +170,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv .identities .iter() .map(|(id, row_offset)| { - witgen - .process_identity(can_process.clone(), id, *row_offset) - .progress + witgen.process_identity(can_process.clone(), id, *row_offset) }) .reduce(std::ops::BitOr::bitor) .unwrap_or(false); diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 760653f570..8d5f18f9f8 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -24,14 +24,6 @@ use super::{ variable::{MachineCallVariable, Variable}, }; -/// Summary of the effect of processing an action. -pub struct ProcessSummary { - /// The action has been fully completed, processing it again will not have any effect. - pub complete: bool, - /// Processing the action changed the state of the inference. - pub progress: bool, -} - /// This component can generate code that solves identities. /// It needs a driver that tells it which identities to process on which rows. #[derive(Clone)] @@ -152,18 +144,16 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } /// Process an identity on a certain row. + /// Returns true if there was progress. pub fn process_identity>( &mut self, can_process: CanProcess, id: &'a Identity, row_offset: i32, - ) -> ProcessSummary { + ) -> bool { // TODO remove this once we propagate range constraints. if self.is_complete(id, row_offset) { - return ProcessSummary { - complete: true, - progress: false, - }; + return false; } let result = match id { Identity::Polynomial(PolynomialIdentity { expression, .. }) => { @@ -310,7 +300,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F VariableOrValue::Value(v) => (*v).into(), }; let r = self.process_equality_on_row(assignment.lhs, assignment.row_offset, rhs); - progress |= self.ingest_effects(r, None).progress; + progress |= self.ingest_effects(r, None); } assert!(self.assignments.is_empty()); self.assignments = assignments; @@ -323,11 +313,12 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F /// Analyze the effects and update the internal state. /// If the effect is the result of a machine call, `identity_id` must be given /// to avoid two calls to the same sub-machine on the same row. + /// Returns true if there was progress. fn ingest_effects( &mut self, process_result: ProcessResult, identity_id: Option<(u64, i32)>, - ) -> ProcessSummary { + ) -> bool { let mut progress = false; for e in process_result.effects { match &e { @@ -370,10 +361,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F if progress { self.process_assignments(); } - ProcessSummary { - complete: process_result.complete, - progress, - } + progress } /// Adds a range constraint to the set of derived range constraints. Returns true if progress was made. @@ -603,12 +591,7 @@ mod test { } } - fn solve_on_rows( - input: &str, - rows: &[i32], - known_cells: Vec<(&str, i32)>, - expected_complete: Option, - ) -> String { + fn solve_on_rows(input: &str, rows: &[i32], known_cells: Vec<(&str, i32)>) -> String { let (analyzed, fixed_col_vals) = read_pil::(input); let fixed_data = FixedData::new(&analyzed, &fixed_col_vals, &[], Default::default(), 0); let (fixed_data, retained_identities) = @@ -639,20 +622,18 @@ mod test { let ref_eval = FixedEvaluatorForFixedData(&fixed_data); let mut witgen = WitgenInference::new(&fixed_data, ref_eval, known_cells, []); - let mut complete = HashSet::new(); let mut counter = 0; - let expected_complete = expected_complete.unwrap_or(retained_identities.len() * rows.len()); - while complete.len() != expected_complete { + loop { + let mut progress = false; counter += 1; for row in rows { for id in retained_identities.iter() { - if !complete.contains(&(id.id(), *row)) - && witgen.process_identity(&mutable_state, id, *row).complete - { - complete.insert((id.id(), *row)); - } + progress |= witgen.process_identity(&mutable_state, id, *row); } } + if !progress { + break; + } assert!(counter < 10000, "Solving took more than 10000 rounds."); } format_code(&witgen.code()) @@ -661,14 +642,14 @@ mod test { #[test] fn simple_polynomial_solving() { let input = "let X; let Y; let Z; X = 1; Y = X + 1; Z * Y = X + 10;"; - let code = solve_on_rows(input, &[0], vec![], None); + let code = solve_on_rows(input, &[0], vec![]); assert_eq!(code, "X[0] = 1;\nY[0] = 2;\nZ[0] = -9223372034707292155;"); } #[test] fn fib() { let input = "let X; let Y; X' = Y; Y' = X + Y;"; - let code = solve_on_rows(input, &[0, 1], vec![("X", 0), ("Y", 0)], None); + let code = solve_on_rows(input, &[0, 1], vec![("X", 0), ("Y", 0)]); assert_eq!( code, "X[1] = Y[0];\nY[1] = (X[0] + Y[0]);\nX[2] = Y[1];\nY[2] = (X[1] + Y[1]);" @@ -688,7 +669,7 @@ mod test { x' - y = 0; y' - (x + y) = 0; "; - let code = solve_on_rows(input, &[0, 1, 2, 3], vec![], None); + let code = solve_on_rows(input, &[0, 1, 2, 3], vec![]); assert_eq!( code, "Fib::y[0] = 1; @@ -739,7 +720,6 @@ namespace Xor(256 * 256); ("Xor::A", 7), ("Xor::C", 7), // We solve it in reverse, just for fun. ], - Some(16), ); assert_eq!( code, From 2945d10edaedcb7ca5cf37a15ae385af57984f12 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 10:32:16 +0000 Subject: [PATCH 10/31] Cleanup --- executor/src/witgen/jit/block_machine_processor.rs | 2 +- executor/src/witgen/jit/single_step_processor.rs | 4 ++-- executor/src/witgen/jit/witgen_inference.rs | 10 +++++++--- 3 files changed, 10 insertions(+), 6 deletions(-) diff --git a/executor/src/witgen/jit/block_machine_processor.rs b/executor/src/witgen/jit/block_machine_processor.rs index e9067bbea2..6d152b7caa 100644 --- a/executor/src/witgen/jit/block_machine_processor.rs +++ b/executor/src/witgen/jit/block_machine_processor.rs @@ -14,7 +14,7 @@ use super::{ }; /// This is a tuning value. It is the maximum nesting depth of branches in the JIT code. -const BLOCK_MACHINE_MAX_BRANCH_DEPTH: usize = 0; +const BLOCK_MACHINE_MAX_BRANCH_DEPTH: usize = 6; /// A processor for generating JIT code for a block machine. pub struct BlockMachineProcessor<'a, T: FieldElement> { diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index 7a0d0f7859..55006b5f3d 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -56,8 +56,8 @@ impl<'a, T: FieldElement> SingleStepProcessor<'a, T> { if id.contains_next_ref() { vec![(id, 0)] } else { - // Process it on both rows, but do not call it on row 0 if it is - // a submachine call. + // Process it on both rows, but mark it as complete on row 0, + // so that we do not produce two submachine calls. complete_identities.push((id.id(), 0)); vec![(id, 0), (id, 1)] } diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 8d5f18f9f8..eb6491df66 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -32,8 +32,9 @@ pub struct WitgenInference<'a, T: FieldElement, FixedEval> { fixed_evaluator: FixedEval, derived_range_constraints: HashMap>, known_variables: HashSet, - /// Identities where we do not want to generate a submachine call - /// to avoid two calls to the same submachine on the same row. + /// Identities that have already been completed. + /// This mainly avoids generating multiple submachine calls for the same + /// connection on the same row. complete_identities: HashSet<(u64, i32)>, /// Internal equality constraints that are not identities from the constraint set. assignments: Vec>, @@ -337,9 +338,10 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } Effect::MachineCall(_, _, vars) => { // If the machine call is already complete, it means that we have - // processed itand created code for it in the past. We might still process it + // should not create another submachine call. We might still process it // multiple times to get better range constraints. if self.complete_identities.insert(identity_id.unwrap()) { + assert!(process_result.complete); for v in vars { // Inputs are already known, but it does not hurt to add all of them. self.known_variables.insert(v.clone()); @@ -355,6 +357,8 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } if process_result.complete { if let Some(identity_id) = identity_id { + // We actually only need to store completeness for submachine calls, + // but we do it for all identities. self.complete_identities.insert(identity_id); } } From 5423bb0f8c8af97c5c62a7a98d3aa80838587bc0 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 15 Jan 2025 11:03:36 +0100 Subject: [PATCH 11/31] Apply suggestions from code review Co-authored-by: Georg Wiese --- executor/src/witgen/jit/processor.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index d8e516aacd..9dd96f0548 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -169,11 +169,9 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv let progress = self .identities .iter() - .map(|(id, row_offset)| { + .any(|(id, row_offset)| { witgen.process_identity(can_process.clone(), id, *row_offset) - }) - .reduce(std::ops::BitOr::bitor) - .unwrap_or(false); + }); if !progress { break; } From 64b622ac61083b0959ae310f3e3e650839fd6637 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 15 Jan 2025 10:25:09 +0000 Subject: [PATCH 12/31] fix expectations --- .../src/witgen/jit/block_machine_processor.rs | 56 +++++++++---------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/executor/src/witgen/jit/block_machine_processor.rs b/executor/src/witgen/jit/block_machine_processor.rs index 6d152b7caa..9adba5b0c1 100644 --- a/executor/src/witgen/jit/block_machine_processor.rs +++ b/executor/src/witgen/jit/block_machine_processor.rs @@ -274,55 +274,55 @@ main_binary::operation_id[3] = params[0]; main_binary::A[3] = params[1]; main_binary::B[3] = params[2]; main_binary::operation_id[2] = main_binary::operation_id[3]; +main_binary::operation_id[1] = main_binary::operation_id[2]; +main_binary::operation_id[0] = main_binary::operation_id[1]; +main_binary::operation_id_next[-1] = main_binary::operation_id[0]; +main_binary::operation_id_next[0] = main_binary::operation_id[1]; +main_binary::operation_id_next[1] = main_binary::operation_id[2]; main_binary::A_byte[2] = ((main_binary::A[3] & 4278190080) // 16777216); main_binary::A[2] = (main_binary::A[3] & 16777215); assert (main_binary::A[3] & 18446744069414584320) == 0; -main_binary::B_byte[2] = ((main_binary::B[3] & 4278190080) // 16777216); -main_binary::B[2] = (main_binary::B[3] & 16777215); -assert (main_binary::B[3] & 18446744069414584320) == 0; -main_binary::operation_id_next[2] = main_binary::operation_id[3]; -call_var(9, 2, 0) = main_binary::operation_id_next[2]; -call_var(9, 2, 1) = main_binary::A_byte[2]; -call_var(9, 2, 2) = main_binary::B_byte[2]; -machine_call(9, [Known(call_var(9, 2, 0)), Known(call_var(9, 2, 1)), Known(call_var(9, 2, 2)), Unknown(call_var(9, 2, 3))]); -main_binary::C_byte[2] = call_var(9, 2, 3); -main_binary::operation_id[1] = main_binary::operation_id[2]; main_binary::A_byte[1] = ((main_binary::A[2] & 16711680) // 65536); main_binary::A[1] = (main_binary::A[2] & 65535); assert (main_binary::A[2] & 18446744073692774400) == 0; -main_binary::B_byte[1] = ((main_binary::B[2] & 16711680) // 65536); -main_binary::B[1] = (main_binary::B[2] & 65535); -assert (main_binary::B[2] & 18446744073692774400) == 0; -main_binary::operation_id_next[1] = main_binary::operation_id[2]; -call_var(9, 1, 0) = main_binary::operation_id_next[1]; -call_var(9, 1, 1) = main_binary::A_byte[1]; -call_var(9, 1, 2) = main_binary::B_byte[1]; -machine_call(9, [Known(call_var(9, 1, 0)), Known(call_var(9, 1, 1)), Known(call_var(9, 1, 2)), Unknown(call_var(9, 1, 3))]); -main_binary::C_byte[1] = call_var(9, 1, 3); -main_binary::operation_id[0] = main_binary::operation_id[1]; main_binary::A_byte[0] = ((main_binary::A[1] & 65280) // 256); main_binary::A[0] = (main_binary::A[1] & 255); assert (main_binary::A[1] & 18446744073709486080) == 0; +main_binary::A_byte[-1] = main_binary::A[0]; +main_binary::B_byte[2] = ((main_binary::B[3] & 4278190080) // 16777216); +main_binary::B[2] = (main_binary::B[3] & 16777215); +assert (main_binary::B[3] & 18446744069414584320) == 0; +main_binary::B_byte[1] = ((main_binary::B[2] & 16711680) // 65536); +main_binary::B[1] = (main_binary::B[2] & 65535); +assert (main_binary::B[2] & 18446744073692774400) == 0; main_binary::B_byte[0] = ((main_binary::B[1] & 65280) // 256); main_binary::B[0] = (main_binary::B[1] & 255); assert (main_binary::B[1] & 18446744073709486080) == 0; -main_binary::operation_id_next[0] = main_binary::operation_id[1]; -call_var(9, 0, 0) = main_binary::operation_id_next[0]; -call_var(9, 0, 1) = main_binary::A_byte[0]; -call_var(9, 0, 2) = main_binary::B_byte[0]; -machine_call(9, [Known(call_var(9, 0, 0)), Known(call_var(9, 0, 1)), Known(call_var(9, 0, 2)), Unknown(call_var(9, 0, 3))]); -main_binary::C_byte[0] = call_var(9, 0, 3); -main_binary::A_byte[-1] = main_binary::A[0]; main_binary::B_byte[-1] = main_binary::B[0]; -main_binary::operation_id_next[-1] = main_binary::operation_id[0]; call_var(9, -1, 0) = main_binary::operation_id_next[-1]; call_var(9, -1, 1) = main_binary::A_byte[-1]; call_var(9, -1, 2) = main_binary::B_byte[-1]; machine_call(9, [Known(call_var(9, -1, 0)), Known(call_var(9, -1, 1)), Known(call_var(9, -1, 2)), Unknown(call_var(9, -1, 3))]); main_binary::C_byte[-1] = call_var(9, -1, 3); main_binary::C[0] = main_binary::C_byte[-1]; +call_var(9, 0, 0) = main_binary::operation_id_next[0]; +call_var(9, 0, 1) = main_binary::A_byte[0]; +call_var(9, 0, 2) = main_binary::B_byte[0]; +machine_call(9, [Known(call_var(9, 0, 0)), Known(call_var(9, 0, 1)), Known(call_var(9, 0, 2)), Unknown(call_var(9, 0, 3))]); +main_binary::C_byte[0] = call_var(9, 0, 3); main_binary::C[1] = (main_binary::C[0] + (main_binary::C_byte[0] * 256)); +call_var(9, 1, 0) = main_binary::operation_id_next[1]; +call_var(9, 1, 1) = main_binary::A_byte[1]; +call_var(9, 1, 2) = main_binary::B_byte[1]; +machine_call(9, [Known(call_var(9, 1, 0)), Known(call_var(9, 1, 1)), Known(call_var(9, 1, 2)), Unknown(call_var(9, 1, 3))]); +main_binary::C_byte[1] = call_var(9, 1, 3); main_binary::C[2] = (main_binary::C[1] + (main_binary::C_byte[1] * 65536)); +main_binary::operation_id_next[2] = main_binary::operation_id[3]; +call_var(9, 2, 0) = main_binary::operation_id_next[2]; +call_var(9, 2, 1) = main_binary::A_byte[2]; +call_var(9, 2, 2) = main_binary::B_byte[2]; +machine_call(9, [Known(call_var(9, 2, 0)), Known(call_var(9, 2, 1)), Known(call_var(9, 2, 2)), Unknown(call_var(9, 2, 3))]); +main_binary::C_byte[2] = call_var(9, 2, 3); main_binary::C[3] = (main_binary::C[2] + (main_binary::C_byte[2] * 16777216)); params[3] = main_binary::C[3];" ) From aedb50d7bb3722eaab70510692b77832a12ca122 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 15 Jan 2025 10:28:33 +0000 Subject: [PATCH 13/31] fix comment. --- executor/src/witgen/jit/witgen_inference.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index eb6491df66..876118f989 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -337,8 +337,8 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F progress |= self.add_range_constraint(variable.clone(), rc.clone()); } Effect::MachineCall(_, _, vars) => { - // If the machine call is already complete, it means that we have - // should not create another submachine call. We might still process it + // If the machine call is already complete, it means that we should + // not create another submachine call. We might still process it // multiple times to get better range constraints. if self.complete_identities.insert(identity_id.unwrap()) { assert!(process_result.complete); From 1b1129b44730c8446bd5376bf5f7b98b931ec635 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 10:47:08 +0000 Subject: [PATCH 14/31] Propagate known --- executor/src/witgen/jit/processor.rs | 1 + .../src/witgen/jit/single_step_processor.rs | 18 ++--- executor/src/witgen/jit/witgen_inference.rs | 73 +++++++++++++------ 3 files changed, 59 insertions(+), 33 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 530fb57cda..42730e4ead 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -166,6 +166,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv witgen: &mut WitgenInference<'a, T, FixedEval>, ) { loop { + // TODO call witgen.process_assignments? let progress = self .identities .iter() diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index 55006b5f3d..110a376d06 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -199,28 +199,26 @@ mod test { instr_add * (A' - (A + B)) + instr_mul * (A' - A * B) + (1 - instr_add - instr_mul) * (A' - A) = 0; B' = B; "; + + // TODO see if we can avoid the "unused" call_var assignments. + // (they are for the completed call) let code = generate_single_step(input, "Main").unwrap(); assert_eq!( format_code(&code), "\ VM::pc[1] = (VM::pc[0] + 1); +call_var(1, 0, 0) = VM::pc[0]; +call_var(1, 0, 1) = VM::instr_add[0]; +call_var(1, 0, 2) = VM::instr_mul[0]; call_var(1, 1, 0) = VM::pc[1]; machine_call(1, [Known(call_var(1, 1, 0)), Unknown(call_var(1, 1, 1)), Unknown(call_var(1, 1, 2))]); VM::instr_add[1] = call_var(1, 1, 1); VM::instr_mul[1] = call_var(1, 1, 2); VM::B[1] = VM::B[0]; if (VM::instr_add[0] == 1) { - if (VM::instr_mul[0] == 1) { - VM::A[1] = -((-(VM::A[0] + VM::B[0]) + -(VM::A[0] * VM::B[0])) + VM::A[0]); - } else { - VM::A[1] = (VM::A[0] + VM::B[0]); - } + VM::A[1] = (VM::A[0] + VM::B[0]); } else { - if (VM::instr_mul[0] == 1) { - VM::A[1] = (VM::A[0] * VM::B[0]); - } else { - VM::A[1] = VM::A[0]; - } + VM::A[1] = (VM::A[0] * VM::B[0]); }" ); } diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 876118f989..a080f1ab5e 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -152,14 +152,13 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F id: &'a Identity, row_offset: i32, ) -> bool { - // TODO remove this once we propagate range constraints. - if self.is_complete(id, row_offset) { - return false; - } let result = match id { - Identity::Polynomial(PolynomialIdentity { expression, .. }) => { - self.process_equality_on_row(expression, row_offset, T::from(0).into()) - } + Identity::Polynomial(PolynomialIdentity { expression, .. }) => self + .process_equality_on_row( + expression, + row_offset, + &VariableOrValue::Value(T::from(0)), + ), Identity::Lookup(LookupIdentity { id, left, .. }) | Identity::Permutation(PermutationIdentity { id, left, .. }) | Identity::PhantomPermutation(PhantomPermutationIdentity { id, left, .. }) @@ -210,17 +209,47 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F &self, lhs: &Expression, offset: i32, - rhs: AffineSymbolicExpression, + rhs: &VariableOrValue, ) -> ProcessResult { - if let Some(r) = self.evaluate(lhs, offset) { - // TODO propagate or report error properly. - // If solve returns an error, it means that the constraint is conflicting. - // In the future, we might run this in a runtime-conditional, so an error - // could just mean that this case cannot happen in practice. - (r - rhs).solve().unwrap() - } else { - ProcessResult::empty() + // First we try to find a new assignment to a variable in the equality. + + let evaluator = Evaluator::new(self); + let Some(lhs_evaluated) = evaluator.evaluate(lhs, offset) else { + return ProcessResult::empty(); + }; + + let rhs_evaluated = match rhs { + VariableOrValue::Variable(v) => evaluator.evaluate_variable(v.clone()), + VariableOrValue::Value(v) => (*v).into(), + }; + + // TODO propagate or report error properly. + // If solve returns an error, it means that the constraint is conflicting. + // In the future, we might run this in a runtime-conditional, so an error + // could just mean that this case cannot happen in practice. + let result = (lhs_evaluated - rhs_evaluated).solve().unwrap(); + if result.complete && result.effects.is_empty() { + // TODO refactor this part into its own function and call this function + // directly for complete identities (if it is a performance problem) + + // A complete result without effects means that there were no unknowns + // in the constraint. + // We try again, but this time we treat all non-concrete variables + // as unknown and in that way try to find new concrete values for + // already known variables. + let evaluator = Evaluator::new(self).only_concrete_known(); + if let Some(lhs_evaluated) = evaluator.evaluate(lhs, offset) { + let rhs_evaluated = match rhs { + VariableOrValue::Variable(v) => evaluator.evaluate_variable(v.clone()), + VariableOrValue::Value(v) => (*v).into(), + }; + let result = (lhs_evaluated - rhs_evaluated).solve().unwrap(); + if !result.effects.is_empty() { + return result; + } + } } + result } fn process_call>( @@ -294,13 +323,11 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F // We need to take them out because ingest_effects needs a &mut self. let assignments = std::mem::take(&mut self.assignments); for assignment in &assignments { - let rhs = match &assignment.rhs { - VariableOrValue::Variable(v) => { - Evaluator::new(self).evaluate_variable(v.clone()) - } - VariableOrValue::Value(v) => (*v).into(), - }; - let r = self.process_equality_on_row(assignment.lhs, assignment.row_offset, rhs); + let r = self.process_equality_on_row( + assignment.lhs, + assignment.row_offset, + &assignment.rhs, + ); progress |= self.ingest_effects(r, None); } assert!(self.assignments.is_empty()); From 917f677bd7ef508056567769d768af40a60dd107 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 14:10:35 +0000 Subject: [PATCH 15/31] Fix test. --- executor/src/witgen/jit/single_step_processor.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index 110a376d06..e546906e38 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -235,7 +235,7 @@ if (VM::instr_add[0] == 1) { col fixed INSTR_ADD = [0, 1] + [0]*; col fixed INSTR_MUL = [1, 0] + [1]*; - pc' = pc + 1; + pc' = pc; instr_add = 0; [ pc, instr_add, instr_mul ] in [ LINE, INSTR_ADD, INSTR_MUL ]; @@ -249,8 +249,11 @@ if (VM::instr_add[0] == 1) { assert_eq!( format_code(&code), "\ -VM::pc[1] = (VM::pc[0] + 1); +VM::pc[1] = VM::pc[0]; VM::instr_add[1] = 0; +call_var(2, 0, 0) = VM::pc[0]; +call_var(2, 0, 1) = 0; +call_var(2, 0, 2) = VM::instr_mul[0]; call_var(2, 1, 0) = VM::pc[1]; call_var(2, 1, 1) = 0; call_var(2, 1, 2) = 1; From 1405bc070b57a6c9c350b43335e05b79fda668b2 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 14:20:22 +0000 Subject: [PATCH 16/31] cleanup --- executor/src/witgen/jit/processor.rs | 1 - executor/src/witgen/jit/single_step_processor.rs | 2 -- 2 files changed, 3 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 42730e4ead..530fb57cda 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -166,7 +166,6 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv witgen: &mut WitgenInference<'a, T, FixedEval>, ) { loop { - // TODO call witgen.process_assignments? let progress = self .identities .iter() diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index e546906e38..8fa9246a88 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -200,8 +200,6 @@ mod test { B' = B; "; - // TODO see if we can avoid the "unused" call_var assignments. - // (they are for the completed call) let code = generate_single_step(input, "Main").unwrap(); assert_eq!( format_code(&code), From f9372520f888fbeb5ed9d718b59f3e62ea93bd0f Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 14:24:23 +0000 Subject: [PATCH 17/31] Refactor. --- executor/src/witgen/jit/witgen_inference.rs | 35 +++++++++++++-------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index a080f1ab5e..a3ab538068 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -229,29 +229,38 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F // could just mean that this case cannot happen in practice. let result = (lhs_evaluated - rhs_evaluated).solve().unwrap(); if result.complete && result.effects.is_empty() { - // TODO refactor this part into its own function and call this function - // directly for complete identities (if it is a performance problem) - // A complete result without effects means that there were no unknowns // in the constraint. // We try again, but this time we treat all non-concrete variables // as unknown and in that way try to find new concrete values for // already known variables. - let evaluator = Evaluator::new(self).only_concrete_known(); - if let Some(lhs_evaluated) = evaluator.evaluate(lhs, offset) { - let rhs_evaluated = match rhs { - VariableOrValue::Variable(v) => evaluator.evaluate_variable(v.clone()), - VariableOrValue::Value(v) => (*v).into(), - }; - let result = (lhs_evaluated - rhs_evaluated).solve().unwrap(); - if !result.effects.is_empty() { - return result; - } + let result = self.process_equality_on_row_concrete(lhs, offset, rhs); + if !result.effects.is_empty() { + return result; } } result } + /// Process an equality but only consider concrete variables as known + /// and thus propagate range constraints across the equality. + fn process_equality_on_row_concrete( + &self, + lhs: &Expression, + offset: i32, + rhs: &VariableOrValue, + ) -> ProcessResult { + let evaluator = Evaluator::new(self).only_concrete_known(); + let Some(lhs_evaluated) = evaluator.evaluate(lhs, offset) else { + return ProcessResult::empty(); + }; + let rhs_evaluated = match rhs { + VariableOrValue::Variable(v) => evaluator.evaluate_variable(v.clone()), + VariableOrValue::Value(v) => (*v).into(), + }; + (lhs_evaluated - rhs_evaluated).solve().unwrap() + } + fn process_call>( &mut self, can_process_call: CanProcess, From 73c9d8150eac4db0e2979f73598bcb4d7b72ccd6 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 17:41:33 +0000 Subject: [PATCH 18/31] Better errors. --- executor/src/witgen/jit/witgen_inference.rs | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index a3ab538068..7ca68fb694 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -227,7 +227,12 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F // If solve returns an error, it means that the constraint is conflicting. // In the future, we might run this in a runtime-conditional, so an error // could just mean that this case cannot happen in practice. - let result = (lhs_evaluated - rhs_evaluated).solve().unwrap(); + let result = (lhs_evaluated - rhs_evaluated) + .solve() + .map_err(|e| { + panic!("Error solving equality constraint: {lhs} = {rhs} on row {offset}: {e}"); + }) + .unwrap(); if result.complete && result.effects.is_empty() { // A complete result without effects means that there were no unknowns // in the constraint. @@ -258,7 +263,12 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F VariableOrValue::Variable(v) => evaluator.evaluate_variable(v.clone()), VariableOrValue::Value(v) => (*v).into(), }; - (lhs_evaluated - rhs_evaluated).solve().unwrap() + (lhs_evaluated - rhs_evaluated) + .solve() + .map_err(|e| { + panic!("Error solving equality constraint: {lhs} = {rhs} on row {offset}: {e}"); + }) + .unwrap() } fn process_call>( @@ -568,7 +578,7 @@ struct Assignment<'a, T: FieldElement> { rhs: VariableOrValue, } -#[derive(Clone)] +#[derive(Clone, derive_more::Display)] enum VariableOrValue { Variable(V), Value(T), From 6ce7f65bdf457999cdb058d16359fc3f25da8655 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 18:01:38 +0000 Subject: [PATCH 19/31] Also print code generated so far. --- executor/src/witgen/jit/witgen_inference.rs | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 7ca68fb694..aecd0518aa 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -15,7 +15,7 @@ use powdr_number::FieldElement; use crate::witgen::{ data_structures::mutable_state::MutableState, global_constraints::RangeConstraintSet, - range_constraints::RangeConstraint, FixedData, QueryCallback, + jit::effect::format_code, range_constraints::RangeConstraint, FixedData, QueryCallback, }; use super::{ @@ -230,7 +230,11 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F let result = (lhs_evaluated - rhs_evaluated) .solve() .map_err(|e| { - panic!("Error solving equality constraint: {lhs} = {rhs} on row {offset}: {e}"); + panic!( + "Error solving equality constraint: {lhs} = {rhs} on row {offset}: {e}\n\ + Code generated since the previous branching point:\n{}", + format_code(&self.code) + ); }) .unwrap(); if result.complete && result.effects.is_empty() { @@ -266,7 +270,11 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F (lhs_evaluated - rhs_evaluated) .solve() .map_err(|e| { - panic!("Error solving equality constraint: {lhs} = {rhs} on row {offset}: {e}"); + panic!( + "Error solving equality constraint: {lhs} = {rhs} on row {offset}: {e}\n\ + Code generated since the previous branching point:\n{}", + format_code(&self.code) + ); }) .unwrap() } From cafd532db847be7dc456634e08e3ad6634b8f8ee Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 18:14:13 +0000 Subject: [PATCH 20/31] Compile-time check for covered offset. --- .../witgen/jit/affine_symbolic_expression.rs | 28 +++++++++++-------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/executor/src/witgen/jit/affine_symbolic_expression.rs b/executor/src/witgen/jit/affine_symbolic_expression.rs index 402e4c4745..cb18e1e14d 100644 --- a/executor/src/witgen/jit/affine_symbolic_expression.rs +++ b/executor/src/witgen/jit/affine_symbolic_expression.rs @@ -196,12 +196,12 @@ impl AffineSymbolicExpression { } } _ => { - let r = self.solve_bit_decomposition(); + let r = self.solve_bit_decomposition()?; if r.complete { r } else { let negated = -self; - let r = negated.solve_bit_decomposition(); + let r = negated.solve_bit_decomposition()?; if r.complete { r } else { @@ -221,7 +221,7 @@ impl AffineSymbolicExpression { } /// Tries to solve a bit-decomposition equation. - fn solve_bit_decomposition(&self) -> ProcessResult { + fn solve_bit_decomposition(&self) -> Result, EvalError> { // All the coefficients need to be known numbers and the // variables need to be range-constrained. let constrained_coefficients = self @@ -234,7 +234,7 @@ impl AffineSymbolicExpression { }) .collect::>>(); let Some(constrained_coefficients) = constrained_coefficients else { - return ProcessResult::empty(); + return Ok(ProcessResult::empty()); }; // Check if they are mutually exclusive and compute assignments. @@ -244,7 +244,7 @@ impl AffineSymbolicExpression { let mask = *constraint.multiple(coeff).mask(); if !(mask & covered_bits).is_zero() { // Overlapping range constraints. - return ProcessResult::empty(); + return Ok(ProcessResult::empty()); } else { covered_bits |= mask; } @@ -256,18 +256,24 @@ impl AffineSymbolicExpression { } if covered_bits >= T::modulus() { - return ProcessResult::empty(); + return Ok(ProcessResult::empty()); } // We need to assert that the masks cover "-offset", // otherwise the equation is not solvable. // We assert -offset & !masks == 0 - effects.push(Assertion::assert_eq( - -&self.offset & !covered_bits, - T::from(0).into(), - )); + if let Some(offset) = self.offset.try_to_number() { + if (-offset).to_integer() & !covered_bits != 0.into() { + return Err(EvalError::ConflictingRangeConstraints); + } + } else { + effects.push(Assertion::assert_eq( + -&self.offset & !covered_bits, + T::from(0).into(), + )); + } - ProcessResult::complete(effects) + Ok(ProcessResult::complete(effects)) } fn transfer_constraints(&self) -> Option> { From 5c9f1a5590c2e6cf1cc5ab5fe34a8924c75ebdc8 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 18:36:21 +0000 Subject: [PATCH 21/31] Consider conflicting branches. --- executor/src/witgen/jit/processor.rs | 81 +++++++++++++++------ executor/src/witgen/jit/witgen_inference.rs | 61 +++++++--------- 2 files changed, 85 insertions(+), 57 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 530fb57cda..729b8cb79b 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -8,7 +8,7 @@ use itertools::Itertools; use powdr_ast::analyzed::{Identity, PolyID, PolynomialType}; use powdr_number::FieldElement; -use crate::witgen::FixedData; +use crate::witgen::{EvalError, FixedData}; use super::{ effect::{format_code, Effect}, @@ -70,7 +70,8 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv mut witgen: WitgenInference<'a, T, FixedEval>, branch_depth: usize, ) -> Result>, Error<'a, T>> { - self.process_until_no_progress(can_process.clone(), &mut witgen); + self.process_until_no_progress(can_process.clone(), &mut witgen) + .map_err(|_| Error::conflicting_constraints())?; if self.check_block_shape { // Check that the "spill" into the previous block is compatible @@ -140,42 +141,58 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv // TODO Tuning: If this fails (or also if it does not generate progress right away), // we could also choose a different variable to branch on. - let left_branch_code = - self.generate_code_for_branch(can_process.clone(), first_branch, branch_depth + 1)?; - let right_branch_code = - self.generate_code_for_branch(can_process, second_branch, branch_depth + 1)?; - let code = if left_branch_code == right_branch_code { - common_code.into_iter().chain(left_branch_code).collect() - } else { - common_code + + let first_branch_result = + self.generate_code_for_branch(can_process.clone(), first_branch, branch_depth + 1); + let second_branch_result = + self.generate_code_for_branch(can_process, second_branch, branch_depth + 1); + // There is a recoverable error: It might be that a branch has conflicting + // constraints, which means we can just take the other branch without actually + // branching. + match (first_branch_result, second_branch_result) { + (Err(el), Err(er)) + if el.reason == ErrorReason::ConflictingConstraints + && er.reason == ErrorReason::ConflictingConstraints => + { + // Both are conflicting, so we push it up. + Err(Error::conflicting_constraints()) + } + (Err(e), Ok(code)) | (Ok(code), Err(e)) + if e.reason == ErrorReason::ConflictingConstraints => + { + log::trace!("Branching on {most_constrained_var} resulted in a conflict, we can reduce to a sigle branch."); + Ok(common_code.into_iter().chain(code).collect()) + } + (Err(e), _) | (_, Err(e)) => Err(e), + (Ok(first_code), Ok(second_code)) if first_code == second_code => { + log::trace!("Branching on {most_constrained_var} resulted in the same code, we can reduce to a sigle branch."); + Ok(common_code.into_iter().chain(first_code).collect()) + } + (Ok(first_code), Ok(second_code)) => Ok(common_code .into_iter() .chain(std::iter::once(Effect::Branch( condition, - left_branch_code, - right_branch_code, + first_code, + second_code, ))) - .collect() - }; - - Ok(code) + .collect()), + } } fn process_until_no_progress + Clone>( &self, can_process: CanProcess, witgen: &mut WitgenInference<'a, T, FixedEval>, - ) { + ) -> Result<(), EvalError> { loop { - let progress = self - .identities - .iter() - .any(|(id, row_offset)| { - witgen.process_identity(can_process.clone(), id, *row_offset) - }); + let progress = self.identities.iter().any(|(id, row_offset)| { + witgen.process_identity(can_process.clone(), id, *row_offset) + }); if !progress { break; } } + Ok(()) } /// If any machine call could not be completed, that's bad because machine calls typically have side effects. @@ -323,8 +340,16 @@ pub struct Error<'a, T: FieldElement> { pub incomplete_identities: Vec<(&'a Identity, i32)>, } +#[derive(PartialEq, Eq)] pub enum ErrorReason { + /// This error means that the current branch (if it is a branch) + /// is actually not reachable. + ConflictingConstraints, + /// We were not able to solve all required constraints and + /// there is no variable left to branch on. NoBranchVariable, + /// We were not able to solve all required constraints and + /// the maximum branch depth was reached. MaxBranchDepthReached(usize), } @@ -339,12 +364,22 @@ impl Display for Error<'_, T> { } impl Error<'_, T> { + pub fn conflicting_constraints() -> Self { + Self { + code: vec![], + reason: ErrorReason::ConflictingConstraints, + missing_variables: vec![], + incomplete_identities: vec![], + } + } + pub fn to_string_with_variable_formatter( &self, var_formatter: impl Fn(&Variable) -> String, ) -> String { let mut s = String::new(); let reason_str = match &self.reason { + ErrorReason::ConflictingConstraints => "Conflicting constraints".to_string(), ErrorReason::NoBranchVariable => "No variable available to branch on".to_string(), ErrorReason::MaxBranchDepthReached(depth) => { format!("Maximum branch depth of {depth} reached") diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index aecd0518aa..bced5a8137 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -15,7 +15,8 @@ use powdr_number::FieldElement; use crate::witgen::{ data_structures::mutable_state::MutableState, global_constraints::RangeConstraintSet, - jit::effect::format_code, range_constraints::RangeConstraint, FixedData, QueryCallback, + jit::effect::format_code, range_constraints::RangeConstraint, EvalError, FixedData, + QueryCallback, }; use super::{ @@ -145,20 +146,21 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } /// Process an identity on a certain row. - /// Returns true if there was progress. + /// Returns Ok(true) if there was progress and Ok(false) if there was no progress. + /// If this returns an error, it means we have conflicting constraints. pub fn process_identity>( &mut self, can_process: CanProcess, id: &'a Identity, row_offset: i32, - ) -> bool { + ) -> Result> { let result = match id { Identity::Polynomial(PolynomialIdentity { expression, .. }) => self .process_equality_on_row( expression, row_offset, &VariableOrValue::Value(T::from(0)), - ), + )?, Identity::Lookup(LookupIdentity { id, left, .. }) | Identity::Permutation(PermutationIdentity { id, left, .. }) | Identity::PhantomPermutation(PhantomPermutationIdentity { id, left, .. }) @@ -173,7 +175,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F Identity::PhantomBusInteraction(_) => ProcessResult::empty(), Identity::Connect(_) => ProcessResult::empty(), }; - self.ingest_effects(result, Some((id.id(), row_offset))) + Ok(self.ingest_effects(result, Some((id.id(), row_offset)))) } /// Process the constraint that the expression evaluated at the given offset equals the given value. @@ -205,17 +207,19 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F self.process_assignments(); } + /// Processes an equality constraint. + /// If this returns an error, it means we have conflicting constraints. fn process_equality_on_row( &self, lhs: &Expression, offset: i32, rhs: &VariableOrValue, - ) -> ProcessResult { + ) -> Result, EvalError> { // First we try to find a new assignment to a variable in the equality. let evaluator = Evaluator::new(self); let Some(lhs_evaluated) = evaluator.evaluate(lhs, offset) else { - return ProcessResult::empty(); + return Ok(ProcessResult::empty()); }; let rhs_evaluated = match rhs { @@ -223,32 +227,24 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F VariableOrValue::Value(v) => (*v).into(), }; - // TODO propagate or report error properly. - // If solve returns an error, it means that the constraint is conflicting. - // In the future, we might run this in a runtime-conditional, so an error - // could just mean that this case cannot happen in practice. let result = (lhs_evaluated - rhs_evaluated) .solve() - .map_err(|e| { - panic!( - "Error solving equality constraint: {lhs} = {rhs} on row {offset}: {e}\n\ - Code generated since the previous branching point:\n{}", - format_code(&self.code) - ); - }) - .unwrap(); + .map_err(|e| match e { + EvalError::ConflictingRangeConstraints | EvalError::ConstraintUnsatisfiable(_) => e, + _ => panic!("Unexpected error: {e}"), + })?; if result.complete && result.effects.is_empty() { // A complete result without effects means that there were no unknowns // in the constraint. // We try again, but this time we treat all non-concrete variables // as unknown and in that way try to find new concrete values for // already known variables. - let result = self.process_equality_on_row_concrete(lhs, offset, rhs); + let result = self.process_equality_on_row_concrete(lhs, offset, rhs)?; if !result.effects.is_empty() { - return result; + return Ok(result); } } - result + Ok(result) } /// Process an equality but only consider concrete variables as known @@ -258,10 +254,10 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F lhs: &Expression, offset: i32, rhs: &VariableOrValue, - ) -> ProcessResult { + ) -> Result, EvalError> { let evaluator = Evaluator::new(self).only_concrete_known(); let Some(lhs_evaluated) = evaluator.evaluate(lhs, offset) else { - return ProcessResult::empty(); + return Ok(ProcessResult::empty()); }; let rhs_evaluated = match rhs { VariableOrValue::Variable(v) => evaluator.evaluate_variable(v.clone()), @@ -269,14 +265,10 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F }; (lhs_evaluated - rhs_evaluated) .solve() - .map_err(|e| { - panic!( - "Error solving equality constraint: {lhs} = {rhs} on row {offset}: {e}\n\ - Code generated since the previous branching point:\n{}", - format_code(&self.code) - ); + .map_err(|e| match e { + EvalError::ConflictingRangeConstraints | EvalError::ConstraintUnsatisfiable(_) => e, + _ => panic!("Unexpected error: {e}"), }) - .unwrap() } fn process_call>( @@ -344,7 +336,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } } - fn process_assignments(&mut self) { + fn process_assignments(&mut self) -> Result<(), EvalError> { loop { let mut progress = false; // We need to take them out because ingest_effects needs a &mut self. @@ -354,7 +346,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F assignment.lhs, assignment.row_offset, &assignment.rhs, - ); + )?; progress |= self.ingest_effects(r, None); } assert!(self.assignments.is_empty()); @@ -363,6 +355,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F break; } } + Ok(()) } /// Analyze the effects and update the internal state. @@ -686,7 +679,7 @@ mod test { counter += 1; for row in rows { for id in retained_identities.iter() { - progress |= witgen.process_identity(&mutable_state, id, *row); + progress |= witgen.process_identity(&mutable_state, id, *row).unwrap(); } } if !progress { From 926c0edbc15c163a6802f6dd47366f757224c597 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 22:19:18 +0000 Subject: [PATCH 22/31] Check assignments. --- executor/src/witgen/jit/witgen_inference.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index bced5a8137..ac573b5bd9 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -187,7 +187,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F row_offset, rhs: VariableOrValue::Value(value), }); - self.process_assignments(); + self.process_assignments().unwrap(); } /// Process the constraint that the expression evaluated at the given offset equals the given formal variable. @@ -204,7 +204,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F row_offset, rhs: VariableOrValue::Variable(variable), }); - self.process_assignments(); + self.process_assignments().unwrap(); } /// Processes an equality constraint. @@ -410,7 +410,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } } if progress { - self.process_assignments(); + self.process_assignments().unwrap(); } progress } From 80c376f9954134eff165de7193664e828e9e7ec8 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 22:19:32 +0000 Subject: [PATCH 23/31] Better logging. --- executor/src/witgen/jit/witgen_inference.rs | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index ac573b5bd9..1c12f1f249 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -15,8 +15,7 @@ use powdr_number::FieldElement; use crate::witgen::{ data_structures::mutable_state::MutableState, global_constraints::RangeConstraintSet, - jit::effect::format_code, range_constraints::RangeConstraint, EvalError, FixedData, - QueryCallback, + range_constraints::RangeConstraint, EvalError, FixedData, QueryCallback, }; use super::{ @@ -303,11 +302,6 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F let Some(new_range_constraints) = can_process_call.can_process_call_fully(lookup_id, &known, &range_constraints) else { - log::trace!( - "Sub-machine cannot process call fully (will retry later): {lookup_id}, arguments: {}", - arguments.iter().zip(known).map(|(arg, known)| { - format!("{arg} [{}]", if known { "known" } else { "unknown" }) - }).format(", ")); return ProcessResult::empty(); }; let mut effects = vec![]; @@ -376,6 +370,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F progress |= self.add_range_constraint(variable.clone(), assignment.range_constraint()); if self.known_variables.insert(variable.clone()) { + log::trace!("{variable} := {assignment}"); progress = true; self.code.push(e); } @@ -388,6 +383,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F // not create another submachine call. We might still process it // multiple times to get better range constraints. if self.complete_identities.insert(identity_id.unwrap()) { + log::trace!("Machine call: {:?}", identity_id.unwrap()); assert!(process_result.complete); for v in vars { // Inputs are already known, but it does not hurt to add all of them. From c90b8195066fd70b93adbe9e9ed5541c34a3c658 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 14 Jan 2025 22:33:04 +0000 Subject: [PATCH 24/31] Use BTreeSet for assignments. --- executor/src/witgen/jit/witgen_inference.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 1c12f1f249..1cc9936cb5 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -1,5 +1,5 @@ use std::{ - collections::{HashMap, HashSet}, + collections::{BTreeSet, HashMap, HashSet}, fmt::{Display, Formatter}, }; @@ -37,7 +37,7 @@ pub struct WitgenInference<'a, T: FieldElement, FixedEval> { /// connection on the same row. complete_identities: HashSet<(u64, i32)>, /// Internal equality constraints that are not identities from the constraint set. - assignments: Vec>, + assignments: BTreeSet>, code: Vec>, } @@ -181,7 +181,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F /// This does not have to be solvable right away, but is always processed as soon as we have progress. /// Note that all variables in the expression can be unknown and their status can also change over time. pub fn assign_constant(&mut self, expression: &'a Expression, row_offset: i32, value: T) { - self.assignments.push(Assignment { + self.assignments.insert(Assignment { lhs: expression, row_offset, rhs: VariableOrValue::Value(value), @@ -198,7 +198,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F row_offset: i32, variable: Variable, ) { - self.assignments.push(Assignment { + self.assignments.insert(Assignment { lhs: expression, row_offset, rhs: VariableOrValue::Variable(variable), @@ -568,14 +568,14 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Evaluator<'a, T, FixedEv /// An equality constraint between an algebraic expression evaluated /// on a certain row offset and a variable or fixed constant value. -#[derive(Clone)] +#[derive(Clone, Ord, PartialOrd, Eq, PartialEq, Debug)] struct Assignment<'a, T: FieldElement> { lhs: &'a Expression, row_offset: i32, rhs: VariableOrValue, } -#[derive(Clone, derive_more::Display)] +#[derive(Clone, derive_more::Display, Ord, PartialOrd, Eq, PartialEq, Debug)] enum VariableOrValue { Variable(V), Value(T), From 0972be02a6e49d9a276342430a6bbf898adb1bcb Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 15 Jan 2025 16:05:25 +0000 Subject: [PATCH 25/31] fmt --- executor/src/witgen/jit/processor.rs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 530fb57cda..4d09c5d460 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -166,12 +166,9 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv witgen: &mut WitgenInference<'a, T, FixedEval>, ) { loop { - let progress = self - .identities - .iter() - .any(|(id, row_offset)| { - witgen.process_identity(can_process.clone(), id, *row_offset) - }); + let progress = self.identities.iter().any(|(id, row_offset)| { + witgen.process_identity(can_process.clone(), id, *row_offset) + }); if !progress { break; } From a3dc8137e85d512c3ebdb04d44a3ee0a49a1d852 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 16 Jan 2025 08:29:08 +0000 Subject: [PATCH 26/31] fix --- executor/src/witgen/jit/processor.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 729b8cb79b..c22c0a9fa0 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -185,9 +185,13 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv witgen: &mut WitgenInference<'a, T, FixedEval>, ) -> Result<(), EvalError> { loop { - let progress = self.identities.iter().any(|(id, row_offset)| { - witgen.process_identity(can_process.clone(), id, *row_offset) - }); + let mut progress = false; + for (id, row_offset) in &self.identities { + if witgen.process_identity(can_process.clone(), id, *row_offset)? { + progress = true; + break; + } + } if !progress { break; } From 71032b5da83e6218c85406734a37b061994643d0 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 16 Jan 2025 21:00:21 +0000 Subject: [PATCH 27/31] Typos. --- executor/src/witgen/jit/processor.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index c22c0a9fa0..60f04e2c22 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -160,12 +160,12 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv (Err(e), Ok(code)) | (Ok(code), Err(e)) if e.reason == ErrorReason::ConflictingConstraints => { - log::trace!("Branching on {most_constrained_var} resulted in a conflict, we can reduce to a sigle branch."); + log::trace!("Branching on {most_constrained_var} resulted in a conflict, we can reduce to a single branch."); Ok(common_code.into_iter().chain(code).collect()) } (Err(e), _) | (_, Err(e)) => Err(e), (Ok(first_code), Ok(second_code)) if first_code == second_code => { - log::trace!("Branching on {most_constrained_var} resulted in the same code, we can reduce to a sigle branch."); + log::trace!("Branching on {most_constrained_var} resulted in the same code, we can reduce to a single branch."); Ok(common_code.into_iter().chain(first_code).collect()) } (Ok(first_code), Ok(second_code)) => Ok(common_code From 8840d7f1e754e49b40a7e4e0966169671abfe2c1 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 16 Jan 2025 21:01:34 +0000 Subject: [PATCH 28/31] Extend docstring. --- executor/src/witgen/jit/witgen_inference.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 1cc9936cb5..762b6f2da9 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -33,6 +33,8 @@ pub struct WitgenInference<'a, T: FieldElement, FixedEval> { derived_range_constraints: HashMap>, known_variables: HashSet, /// Identities that have already been completed. + /// Completed identities are still processed to propagate range constraints + /// and concrete values. /// This mainly avoids generating multiple submachine calls for the same /// connection on the same row. complete_identities: HashSet<(u64, i32)>, From 737c767dd5eb2bc11ae56268227d4db717064393 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 16 Jan 2025 22:02:20 +0000 Subject: [PATCH 29/31] Simplify errors. --- .../witgen/jit/affine_symbolic_expression.rs | 18 ++- executor/src/witgen/jit/processor.rs | 108 ++++++++++-------- .../src/witgen/jit/single_step_processor.rs | 7 +- executor/src/witgen/jit/witgen_inference.rs | 51 +++++---- 4 files changed, 106 insertions(+), 78 deletions(-) diff --git a/executor/src/witgen/jit/affine_symbolic_expression.rs b/executor/src/witgen/jit/affine_symbolic_expression.rs index cb18e1e14d..374fa49b8a 100644 --- a/executor/src/witgen/jit/affine_symbolic_expression.rs +++ b/executor/src/witgen/jit/affine_symbolic_expression.rs @@ -8,7 +8,7 @@ use itertools::Itertools; use num_traits::Zero; use powdr_number::FieldElement; -use crate::witgen::{jit::effect::Assertion, EvalError}; +use crate::witgen::jit::effect::Assertion; use super::{ super::range_constraints::RangeConstraint, effect::Effect, @@ -36,6 +36,14 @@ impl ProcessResult { } } +#[derive(Debug)] +pub enum Error { + /// The range constraints of the parts do not cover the full constant sum. + ConflictingRangeConstraints, + /// An equality constraint evaluates to a known-nonzero value. + ConstraintUnsatisfiable, +} + /// Represents an expression `a_1 * x_1 + ... + a_k * x_k + offset`, /// where the `a_i` and `offset` are symbolic expressions, i.e. values known at run-time /// (which can still include variables or symbols, which are only known at run-time), @@ -161,11 +169,11 @@ impl AffineSymbolicExpression { /// constraints) has been found, but it still contains /// unknown variables, returns an empty, incomplete result. /// If the equation is known to be unsolvable, returns an error. - pub fn solve(&self) -> Result, EvalError> { + pub fn solve(&self) -> Result, Error> { Ok(match self.coefficients.len() { 0 => { if self.offset.is_known_nonzero() { - return Err(EvalError::ConstraintUnsatisfiable(self.to_string())); + return Err(Error::ConstraintUnsatisfiable); } else { ProcessResult::complete(vec![]) } @@ -221,7 +229,7 @@ impl AffineSymbolicExpression { } /// Tries to solve a bit-decomposition equation. - fn solve_bit_decomposition(&self) -> Result, EvalError> { + fn solve_bit_decomposition(&self) -> Result, Error> { // All the coefficients need to be known numbers and the // variables need to be range-constrained. let constrained_coefficients = self @@ -264,7 +272,7 @@ impl AffineSymbolicExpression { // We assert -offset & !masks == 0 if let Some(offset) = self.offset.try_to_number() { if (-offset).to_integer() & !covered_bits != 0.into() { - return Err(EvalError::ConflictingRangeConstraints); + return Err(Error::ConflictingRangeConstraints); } } else { effects.push(Assertion::assert_eq( diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 60f04e2c22..39eb22d15b 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -8,9 +8,10 @@ use itertools::Itertools; use powdr_ast::analyzed::{Identity, PolyID, PolynomialType}; use powdr_number::FieldElement; -use crate::witgen::{EvalError, FixedData}; +use crate::witgen::FixedData; use super::{ + affine_symbolic_expression, effect::{format_code, Effect}, variable::{Cell, Variable}, witgen_inference::{BranchResult, CanProcessCall, FixedEvaluator, Value, WitgenInference}, @@ -59,7 +60,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv &self, can_process: CanProcess, witgen: WitgenInference<'a, T, FixedEval>, - ) -> Result>, Error<'a, T>> { + ) -> Result>, Error<'a, T, FixedEval>> { let branch_depth = 0; self.generate_code_for_branch(can_process, witgen, branch_depth) } @@ -69,9 +70,13 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv can_process: CanProcess, mut witgen: WitgenInference<'a, T, FixedEval>, branch_depth: usize, - ) -> Result>, Error<'a, T>> { - self.process_until_no_progress(can_process.clone(), &mut witgen) - .map_err(|_| Error::conflicting_constraints())?; + ) -> Result>, Error<'a, T, FixedEval>> { + if self + .process_until_no_progress(can_process.clone(), &mut witgen) + .is_err() + { + return Err(Error::conflicting_constraints(witgen)); + } if self.check_block_shape { // Check that the "spill" into the previous block is compatible @@ -95,7 +100,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv let incomplete_machine_calls = self.incomplete_machine_calls(&witgen); if missing_variables.is_empty() && incomplete_machine_calls.is_empty() { - return Ok(witgen.code()); + return Ok(witgen.finish()); } // We need to do some work, try to branch. @@ -106,9 +111,15 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv .filter(|(_, rc)| rc.try_to_single_value().is_none()) .sorted() .min_by_key(|(_, rc)| rc.range_width()) - .map(|(var, _)| var.clone()); - if branch_depth >= self.max_branch_depth || most_constrained_var.is_none() { - let reason = if most_constrained_var.is_none() { + .map(|(var, rc)| (var.clone(), rc.clone())); + // Either there is no variable left to branch on or the most constrained + // still has more than (1 << max_branch_depth) possible values. + let no_viable_branch_variable = most_constrained_var + .as_ref() + .map(|(_, rc)| (rc.range_width() >> self.max_branch_depth) > 0.into()) + .unwrap_or(true); + if branch_depth >= self.max_branch_depth || no_viable_branch_variable { + let reason = if no_viable_branch_variable { ErrorReason::NoBranchVariable } else { ErrorReason::MaxBranchDepthReached(self.max_branch_depth) @@ -121,17 +132,14 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv .collect_vec(); return Err(Error { reason, - code: witgen.code(), + witgen, missing_variables, incomplete_identities, }); }; - let most_constrained_var = most_constrained_var.unwrap(); + let (most_constrained_var, range) = most_constrained_var.unwrap(); - log::debug!( - "Branching on variable {most_constrained_var} with range {} at depth {branch_depth}", - witgen.range_constraint(&most_constrained_var) - ); + log::debug!("Branching on variable {most_constrained_var} with range {range} at depth {branch_depth}"); let BranchResult { common_code, @@ -146,44 +154,36 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv self.generate_code_for_branch(can_process.clone(), first_branch, branch_depth + 1); let second_branch_result = self.generate_code_for_branch(can_process, second_branch, branch_depth + 1); - // There is a recoverable error: It might be that a branch has conflicting - // constraints, which means we can just take the other branch without actually - // branching. - match (first_branch_result, second_branch_result) { - (Err(el), Err(er)) - if el.reason == ErrorReason::ConflictingConstraints - && er.reason == ErrorReason::ConflictingConstraints => - { - // Both are conflicting, so we push it up. - Err(Error::conflicting_constraints()) - } - (Err(e), Ok(code)) | (Ok(code), Err(e)) + let result = match (first_branch_result, second_branch_result) { + (Err(e), other) | (other, Err(e)) if e.reason == ErrorReason::ConflictingConstraints => { + // Any branch with a conflicting constraint is not reachable and thus + // can be pruned. We do not branch but still add the range constraint. + // Note that the other branch might also have a conflicting constraint, + // but then it is correct to return it. log::trace!("Branching on {most_constrained_var} resulted in a conflict, we can reduce to a single branch."); - Ok(common_code.into_iter().chain(code).collect()) + other } + // Any other error should be propagated. (Err(e), _) | (_, Err(e)) => Err(e), (Ok(first_code), Ok(second_code)) if first_code == second_code => { log::trace!("Branching on {most_constrained_var} resulted in the same code, we can reduce to a single branch."); - Ok(common_code.into_iter().chain(first_code).collect()) + Ok(first_code) } - (Ok(first_code), Ok(second_code)) => Ok(common_code - .into_iter() - .chain(std::iter::once(Effect::Branch( - condition, - first_code, - second_code, - ))) - .collect()), - } + (Ok(first_code), Ok(second_code)) => { + Ok(vec![Effect::Branch(condition, first_code, second_code)]) + } + }; + // Prepend the common code in the success case. + result.map(|code| common_code.into_iter().chain(code).collect()) } fn process_until_no_progress + Clone>( &self, can_process: CanProcess, witgen: &mut WitgenInference<'a, T, FixedEval>, - ) -> Result<(), EvalError> { + ) -> Result<(), affine_symbolic_expression::Error> { loop { let mut progress = false; for (id, row_offset) in &self.identities { @@ -333,13 +333,12 @@ fn is_machine_call(identity: &Identity) -> bool { } } -pub struct Error<'a, T: FieldElement> { - /// Code generated so far - pub code: Vec>, +pub struct Error<'a, T: FieldElement, FixedEval: FixedEvaluator> { pub reason: ErrorReason, + pub witgen: WitgenInference<'a, T, FixedEval>, /// Required variables that could not be determined pub missing_variables: Vec, - /// Identities that could not be performed properly. + /// Identities that could not be processed completely. /// Note that we only force submachine calls to be complete. pub incomplete_identities: Vec<(&'a Identity, i32)>, } @@ -357,7 +356,7 @@ pub enum ErrorReason { MaxBranchDepthReached(usize), } -impl Display for Error<'_, T> { +impl> Display for Error<'_, T, FE> { fn fmt(&self, f: &mut Formatter) -> fmt::Result { write!( f, @@ -367,10 +366,10 @@ impl Display for Error<'_, T> { } } -impl Error<'_, T> { - pub fn conflicting_constraints() -> Self { +impl<'a, T: FieldElement, FE: FixedEvaluator> Error<'a, T, FE> { + pub fn conflicting_constraints(witgen: WitgenInference<'a, T, FE>) -> Self { Self { - code: vec![], + witgen, reason: ErrorReason::ConflictingConstraints, missing_variables: vec![], incomplete_identities: vec![], @@ -416,10 +415,21 @@ impl Error<'_, T> { ) .unwrap(); }; - if self.code.is_empty() { + write!( + s, + "\nThe following branch decisions were taken:\n{}", + self.witgen + .branches_taken() + .iter() + .map(|(var, rc)| format!(" {var} = {rc}")) + .join("\n") + ) + .unwrap(); + let code = self.witgen.code(); + if code.is_empty() { write!(s, "\nNo code generated so far.").unwrap(); } else { - write!(s, "\nGenerated code so far:\n{}", format_code(&self.code)).unwrap(); + write!(s, "\nGenerated code so far:\n{}", format_code(&code)).unwrap(); }; s } diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index 8fa9246a88..24069e0dc9 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -174,8 +174,11 @@ mod test { assert_eq!( err.to_string(), "Unable to derive algorithm to compute required values: \ - Maximum branch depth of 6 reached.\nThe following variables or values are still missing: M::Y[1]\n\ - No code generated so far." + No variable available to branch on.\nThe following variables or values are still missing: M::Y[1]\n\ + The following branch decisions were taken:\n\ + \n\ + Generated code so far:\n\ + M::X[1] = M::X[0];" ); } diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index 762b6f2da9..c30bdc5bf6 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -15,11 +15,11 @@ use powdr_number::FieldElement; use crate::witgen::{ data_structures::mutable_state::MutableState, global_constraints::RangeConstraintSet, - range_constraints::RangeConstraint, EvalError, FixedData, QueryCallback, + range_constraints::RangeConstraint, FixedData, QueryCallback, }; use super::{ - affine_symbolic_expression::{AffineSymbolicExpression, ProcessResult}, + affine_symbolic_expression::{AffineSymbolicExpression, Error, ProcessResult}, effect::{BranchCondition, Effect}, variable::{MachineCallVariable, Variable}, }; @@ -30,6 +30,8 @@ use super::{ pub struct WitgenInference<'a, T: FieldElement, FixedEval> { fixed_data: &'a FixedData<'a, T>, fixed_evaluator: FixedEval, + /// Sequences of branches taken in the past to get to the current state. + branches_taken: Vec<(Variable, RangeConstraint)>, derived_range_constraints: HashMap>, known_variables: HashSet, /// Identities that have already been completed. @@ -80,6 +82,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F Self { fixed_data, fixed_evaluator, + branches_taken: Default::default(), derived_range_constraints: Default::default(), known_variables: known_variables.into_iter().collect(), complete_identities: complete_identities.into_iter().collect(), @@ -88,10 +91,18 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } } - pub fn code(self) -> Vec> { + pub fn finish(self) -> Vec> { self.code } + pub fn code(&self) -> &Vec> { + &self.code + } + + pub fn branches_taken(&self) -> &[(Variable, RangeConstraint)] { + &self.branches_taken + } + pub fn known_variables(&self) -> &HashSet { &self.known_variables } @@ -132,8 +143,8 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F let common_code = std::mem::take(&mut self.code); let mut low_branch = self.clone(); - self.add_range_constraint(variable.clone(), high_condition.clone()); - low_branch.add_range_constraint(variable.clone(), low_condition.clone()); + self.branch_to(variable, high_condition.clone()); + low_branch.branch_to(variable, low_condition.clone()); BranchResult { common_code, @@ -146,6 +157,12 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } } + fn branch_to(&mut self, var: &Variable, range_constraint: RangeConstraint) { + self.branches_taken + .push((var.clone(), range_constraint.clone())); + self.add_range_constraint(var.clone(), range_constraint); + } + /// Process an identity on a certain row. /// Returns Ok(true) if there was progress and Ok(false) if there was no progress. /// If this returns an error, it means we have conflicting constraints. @@ -154,7 +171,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F can_process: CanProcess, id: &'a Identity, row_offset: i32, - ) -> Result> { + ) -> Result { let result = match id { Identity::Polynomial(PolynomialIdentity { expression, .. }) => self .process_equality_on_row( @@ -215,7 +232,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F lhs: &Expression, offset: i32, rhs: &VariableOrValue, - ) -> Result, EvalError> { + ) -> Result, Error> { // First we try to find a new assignment to a variable in the equality. let evaluator = Evaluator::new(self); @@ -228,12 +245,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F VariableOrValue::Value(v) => (*v).into(), }; - let result = (lhs_evaluated - rhs_evaluated) - .solve() - .map_err(|e| match e { - EvalError::ConflictingRangeConstraints | EvalError::ConstraintUnsatisfiable(_) => e, - _ => panic!("Unexpected error: {e}"), - })?; + let result = (lhs_evaluated - rhs_evaluated).solve()?; if result.complete && result.effects.is_empty() { // A complete result without effects means that there were no unknowns // in the constraint. @@ -255,7 +267,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F lhs: &Expression, offset: i32, rhs: &VariableOrValue, - ) -> Result, EvalError> { + ) -> Result, Error> { let evaluator = Evaluator::new(self).only_concrete_known(); let Some(lhs_evaluated) = evaluator.evaluate(lhs, offset) else { return Ok(ProcessResult::empty()); @@ -264,12 +276,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F VariableOrValue::Variable(v) => evaluator.evaluate_variable(v.clone()), VariableOrValue::Value(v) => (*v).into(), }; - (lhs_evaluated - rhs_evaluated) - .solve() - .map_err(|e| match e { - EvalError::ConflictingRangeConstraints | EvalError::ConstraintUnsatisfiable(_) => e, - _ => panic!("Unexpected error: {e}"), - }) + (lhs_evaluated - rhs_evaluated).solve() } fn process_call>( @@ -332,7 +339,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } } - fn process_assignments(&mut self) -> Result<(), EvalError> { + fn process_assignments(&mut self) -> Result<(), Error> { loop { let mut progress = false; // We need to take them out because ingest_effects needs a &mut self. @@ -685,7 +692,7 @@ mod test { } assert!(counter < 10000, "Solving took more than 10000 rounds."); } - format_code(&witgen.code()) + format_code(&witgen.finish()) } #[test] From 28f4e10c3a8e21ffc423f0b717a1b329fdcb9a90 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 16 Jan 2025 22:02:43 +0000 Subject: [PATCH 30/31] clippy --- executor/src/witgen/jit/processor.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index 39eb22d15b..a307e4bc6c 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -429,7 +429,7 @@ impl<'a, T: FieldElement, FE: FixedEvaluator> Error<'a, T, FE> { if code.is_empty() { write!(s, "\nNo code generated so far.").unwrap(); } else { - write!(s, "\nGenerated code so far:\n{}", format_code(&code)).unwrap(); + write!(s, "\nGenerated code so far:\n{}", format_code(code)).unwrap(); }; s } From f0e658224919a10f7e747a037a8882bb2ce671c3 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 20 Jan 2025 09:58:13 +0000 Subject: [PATCH 31/31] Cleanup and test expectation updates. --- executor/src/witgen/jit/processor.rs | 5 +---- executor/src/witgen/jit/single_step_processor.rs | 4 ++-- executor/src/witgen/jit/witgen_inference.rs | 1 + 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/executor/src/witgen/jit/processor.rs b/executor/src/witgen/jit/processor.rs index ce8c5ec321..5aaeb84728 100644 --- a/executor/src/witgen/jit/processor.rs +++ b/executor/src/witgen/jit/processor.rs @@ -206,10 +206,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> Processor<'a, T, FixedEv identities_to_process.extend( updated_vars .iter() - .flat_map(|v| { - log::trace!("Variable updated: {v}"); - self.occurrences.get(v) - }) + .flat_map(|v| self.occurrences.get(v)) .flatten() // Filter out the one we just processed. .filter(|(id, row)| (*id, *row) != (identity, row_offset)) diff --git a/executor/src/witgen/jit/single_step_processor.rs b/executor/src/witgen/jit/single_step_processor.rs index c49fe10a4d..2c18794721 100644 --- a/executor/src/witgen/jit/single_step_processor.rs +++ b/executor/src/witgen/jit/single_step_processor.rs @@ -219,10 +219,10 @@ namespace M(256); format_code(&code), "\ VM::pc[1] = (VM::pc[0] + 1); -VM::B[1] = VM::B[0]; call_var(1, 0, 0) = VM::pc[0]; call_var(1, 0, 1) = VM::instr_add[0]; call_var(1, 0, 2) = VM::instr_mul[0]; +VM::B[1] = VM::B[0]; call_var(1, 1, 0) = VM::pc[1]; machine_call(1, [Known(call_var(1, 1, 0)), Unknown(call_var(1, 1, 1)), Unknown(call_var(1, 1, 2))]); VM::instr_add[1] = call_var(1, 1, 1); @@ -262,10 +262,10 @@ if (VM::instr_add[0] == 1) { format_code(&code), "\ VM::pc[1] = VM::pc[0]; -VM::instr_add[1] = 0; call_var(2, 0, 0) = VM::pc[0]; call_var(2, 0, 1) = 0; call_var(2, 0, 2) = VM::instr_mul[0]; +VM::instr_add[1] = 0; call_var(2, 1, 0) = VM::pc[1]; call_var(2, 1, 1) = 0; call_var(2, 1, 2) = 1; diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index fc03cef9a4..f097eb9379 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -390,6 +390,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> WitgenInference<'a, T, F } Effect::RangeConstraint(variable, rc) => { if self.add_range_constraint(variable.clone(), rc.clone()) { + log::trace!("{variable}: {rc}"); updated_variables.push(variable.clone()); } }