From c0d5fd6ef896af4ac26a7d763ec466fe9827e0c0 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 17 Apr 2023 12:52:23 +0200 Subject: [PATCH] Find repeating rows. --- src/witness_generator/affine_expression.rs | 2 +- src/witness_generator/generator.rs | 49 +++++++++++++++---- .../machines/block_machine.rs | 13 ++++- src/witness_generator/mod.rs | 44 ++++++++++++++++- tests/common/mod.rs | 1 + tests/riscv.rs | 7 +++ tests/riscv_data/trivial.rs | 6 +++ 7 files changed, 108 insertions(+), 14 deletions(-) create mode 100644 tests/riscv_data/trivial.rs diff --git a/src/witness_generator/affine_expression.rs b/src/witness_generator/affine_expression.rs index 81468f762..0d5c92b75 100644 --- a/src/witness_generator/affine_expression.rs +++ b/src/witness_generator/affine_expression.rs @@ -260,7 +260,7 @@ impl AffineExpression { } else if *c == (-1).into() { format!("-{name}") } else { - format!("{} * {name}", c) + format!("{c} * {name}") } }) .chain(self.constant_value().map(|v| format!("{v}"))) diff --git a/src/witness_generator/generator.rs b/src/witness_generator/generator.rs index 2f54f907c..086f7769d 100644 --- a/src/witness_generator/generator.rs +++ b/src/witness_generator/generator.rs @@ -75,15 +75,7 @@ where } pub fn compute_next_row(&mut self, next_row: DegreeType) -> Vec { - if next_row >= self.last_report + 1000 { - log::info!( - "{next_row} of {} rows ({} %)", - self.fixed_data.degree, - next_row * 100 / self.fixed_data.degree - ); - self.last_report = next_row; - } - self.next_row = next_row; + self.set_next_row_and_log(next_row); // TODO maybe better to generate a dependency graph than looping multiple times. // TODO at least we could cache the affine expressions between loops. @@ -184,6 +176,33 @@ where } } + /// Verifies the proposed values for the next row. + /// TODO this is bad for machines because we might introduce rows in the machine that are then + /// not used. + pub fn propose_next_row(&mut self, next_row: DegreeType, values: &[FieldElement]) -> bool { + self.set_next_row_and_log(next_row); + self.next = values.iter().cloned().map(Some).collect(); + + for identity in self.identities { + let result = match identity.kind { + IdentityKind::Polynomial => { + self.process_polynomial_identity(identity.left.selector.as_ref().unwrap()) + } + IdentityKind::Plookup | IdentityKind::Permutation => self.process_plookup(identity), + _ => Err("Unsupported lookup type".to_string().into()), + }; + if result.is_err() { + self.next = vec![None; self.current.len()]; + self.next_bit_constraints = vec![None; self.current.len()]; + return false; + } + } + std::mem::swap(&mut self.next, &mut self.current); + self.next = vec![None; self.current.len()]; + self.next_bit_constraints = vec![None; self.current.len()]; + true + } + pub fn machine_witness_col_values(&mut self) -> HashMap> { let mut result: HashMap<_, _> = Default::default(); for m in &mut self.machines { @@ -192,6 +211,18 @@ where result } + fn set_next_row_and_log(&mut self, next_row: DegreeType) { + if next_row >= self.last_report + 1000 { + log::info!( + "{next_row} of {} rows ({} %)", + self.fixed_data.degree, + next_row * 100 / self.fixed_data.degree + ); + self.last_report = next_row; + } + self.next_row = next_row; + } + fn format_next_values(&self) -> Vec { let mut values = self.next.iter().enumerate().collect::>(); values.sort_by_key(|(i, v1)| { diff --git a/src/witness_generator/machines/block_machine.rs b/src/witness_generator/machines/block_machine.rs index 03b402a4a..6f30aebef 100644 --- a/src/witness_generator/machines/block_machine.rs +++ b/src/witness_generator/machines/block_machine.rs @@ -192,9 +192,18 @@ impl BlockMachine { if left .iter() .all(|v| v.as_ref().ok().map(|v| v.is_constant()) == Some(true)) + && self.rows() > 0 { - return Ok(vec![]); - // TOOD check that they really exist (maybe just check the last row) + // All values on the left hand side are known, check if this is a query + // to the last row. + self.row = self.rows() - 1; + if self.process_outer_query(fixed_data, left, right).is_ok() { + return Ok(vec![]); + } else { + return Err("Lookup of constant values in block machine failed." + .to_string() + .into()); + } } let old_len = self.rows(); diff --git a/src/witness_generator/mod.rs b/src/witness_generator/mod.rs index d374b74eb..4e4610f03 100644 --- a/src/witness_generator/mod.rs +++ b/src/witness_generator/mod.rs @@ -64,9 +64,33 @@ pub fn generate<'a>( let mut values: Vec<(&str, Vec)> = witness_cols.iter().map(|p| (p.name, Vec::new())).collect(); + // Are we in an infinite loop and can just re-use the old values? + let mut looping_period = None; for row in 0..degree as DegreeType { - let row_values = generator.compute_next_row(row); - for (col, v) in row_values.into_iter().enumerate() { + // Check if we are in a loop. + if looping_period.is_none() && row % 100 == 0 && row > 0 { + looping_period = rows_are_repeating(&values); + if let Some(p) = looping_period { + log::info!("Found loop with period {p} starting at row {row}") + } + } + let mut row_values = None; + if let Some(period) = looping_period { + let values = values + .iter() + .map(|(_, v)| v[v.len() - period]) + .collect::>(); + if generator.propose_next_row(row, &values) { + row_values = Some(values); + } else { + log::info!("Using loop failed. Trying to generate regularly again."); + looping_period = None; + } + } + if row_values.is_none() { + row_values = Some(generator.compute_next_row(row)); + }; + for (col, v) in row_values.unwrap().into_iter().enumerate() { values[col].1.push(v); } } @@ -83,6 +107,22 @@ pub fn generate<'a>( values } +/// Checks if the last rows are repeating and returns the period. +/// Only checks for periods of 1, 2, 3 and 4. +fn rows_are_repeating(values: &[(&str, Vec)]) -> Option { + if values.is_empty() { + return Some(1); + } else if values[0].1.len() < 4 { + return None; + } + (1..=3).find(|&period| { + values.iter().all(|(_name, value)| { + let len = value.len(); + (1..=period).all(|i| value[len - i - period] == value[len - i]) + }) + }) +} + /// Result of evaluating an expression / lookup. /// New assignments or constraints for witness columns identified by an ID. type EvalResult = Result, EvalError>; diff --git a/tests/common/mod.rs b/tests/common/mod.rs index c9f1c5e01..d27e7b309 100644 --- a/tests/common/mod.rs +++ b/tests/common/mod.rs @@ -44,6 +44,7 @@ pub fn verify(file_name: &str, temp_dir: &Path) { let verifier_output = Command::new("node") .args([ + "--max-old-space-size=8000".to_string(), // 8GB of memory format!("{pilcom}/src/main_pilverifier.js"), commits_file, "-j".to_string(), diff --git a/tests/riscv.rs b/tests/riscv.rs index b1c646f5d..56b8dc0ba 100644 --- a/tests/riscv.rs +++ b/tests/riscv.rs @@ -3,6 +3,13 @@ use powdr::number::FieldElement; mod common; +#[test] +#[ignore = "Too slow"] +fn test_trivial() { + let case = "trivial.rs"; + verify_file(case, vec![]); +} + #[test] #[ignore = "Too slow"] fn test_sum() { diff --git a/tests/riscv_data/trivial.rs b/tests/riscv_data/trivial.rs new file mode 100644 index 000000000..6d7e99acb --- /dev/null +++ b/tests/riscv_data/trivial.rs @@ -0,0 +1,6 @@ +#![no_std] + +#[no_mangle] +pub extern "C" fn main() -> ! { + loop {} +}