mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-05-13 03:00:26 -04:00
Merge pull request #168 from chriseth/find_repeating_rows
Find repeating rows.
This commit is contained in:
@@ -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}")))
|
||||
|
||||
@@ -75,15 +75,7 @@ where
|
||||
}
|
||||
|
||||
pub fn compute_next_row(&mut self, next_row: DegreeType) -> Vec<FieldElement> {
|
||||
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<String, Vec<FieldElement>> {
|
||||
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<String> {
|
||||
let mut values = self.next.iter().enumerate().collect::<Vec<_>>();
|
||||
values.sort_by_key(|(i, v1)| {
|
||||
|
||||
@@ -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();
|
||||
|
||||
@@ -64,9 +64,33 @@ pub fn generate<'a>(
|
||||
|
||||
let mut values: Vec<(&str, Vec<FieldElement>)> =
|
||||
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::<Vec<_>>();
|
||||
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<FieldElement>)]) -> Option<usize> {
|
||||
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<Vec<(usize, Constraint)>, EvalError>;
|
||||
|
||||
@@ -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(),
|
||||
|
||||
@@ -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() {
|
||||
|
||||
6
tests/riscv_data/trivial.rs
Normal file
6
tests/riscv_data/trivial.rs
Normal file
@@ -0,0 +1,6 @@
|
||||
#![no_std]
|
||||
|
||||
#[no_mangle]
|
||||
pub extern "C" fn main() -> ! {
|
||||
loop {}
|
||||
}
|
||||
Reference in New Issue
Block a user