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

Improve logging in Block Machine witgen

Browse Source
This commit is contained in:
Georg Wiese
2023-09-30 12:57:03 +00:00
parent eb593dee15
commit f76aab9cee
6 changed files with 93 additions and 23 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
compiler/tests/pil.rs
View File

@@ -119,7 +119,8 @@ fn test_witness_lookup() {
}),
);
// halo2 fails with "gates must contain at least one constraint"
gen_estark_proof(f, vec![3.into(), 5.into(), 2.into()]);
let inputs = vec![3, 5, 2, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7];
gen_estark_proof(f, inputs.into_iter().map(GoldilocksField::from).collect());
}
#[test]

39
executor/src/witgen/generator.rs
View File

@@ -3,8 +3,8 @@ use itertools::Itertools;
use number::{DegreeType, FieldElement};
use parser_util::lines::indent;
use std::cmp::max;
use std::collections::HashMap;
use std::collections::HashSet;
use std::collections::{BTreeSet, HashMap};
use std::time::Instant;
use crate::witgen::identity_processor::{self, IdentityProcessor};
@@ -50,7 +50,7 @@ impl<'a, T: FieldElement> CompletableIdentities<'a, T> {
pub struct Generator<'a, T: FieldElement> {
/// The witness columns belonging to this machine
witnesses: BTreeSet<PolyID>,
witnesses: HashSet<PolyID>,
row_factory: RowFactory<'a, T>,
fixed_data: &'a FixedData<'a, T>,
/// The subset of identities that contains a reference to the next row
@@ -106,7 +106,7 @@ impl<'a, T: FieldElement> Generator<'a, T> {
Generator {
row_factory,
witnesses: witnesses.clone().into_iter().collect(),
witnesses: witnesses.clone(),
fixed_data,
identities_with_next_ref: identities_with_next,
identities_without_next_ref: identities_without_next,
@@ -244,8 +244,11 @@ impl<'a, T: FieldElement> Generator<'a, T> {
log::trace!(
"{}",
self.current
.render(&format!("===== Row {}", self.current_row_index), true)
self.current.render(
&format!("===== Row {}", self.current_row_index),
true,
&self.witnesses
)
);
self.shift_rows();
@@ -314,6 +317,18 @@ impl<'a, T: FieldElement> Generator<'a, T> {
continue;
}
let is_machine_call = matches!(
identity.kind,
IdentityKind::Plookup | IdentityKind::Permutation
);
if is_machine_call && unknown_strategy == UnknownStrategy::Zero {
// The fact that we got to the point where we assume 0 for unknown cells, but this identity
// is still not complete, means that either the inputs or the machine is under-constrained.
errors.push(format!("{identity}:\n{}",
indent("This machine call could not be completed. Either some inputs are missing or the machine is under-constrained.", " ")).into());
continue;
}
let row_pair = RowPair::new(
&self.current,
&self.next,
@@ -369,8 +384,11 @@ impl<'a, T: FieldElement> Generator<'a, T> {
self.current_row_index
);
log::debug!("Some identities where not satisfiable after the following values were uniquely determined (known nonzero first, then zero, unknown omitted):");
log::debug!("{}", self.current.render("Current Row", false));
log::debug!("{}", self.next.render("Next Row", false));
log::debug!(
"{}",
self.current.render("Current Row", false, &self.witnesses)
);
log::debug!("{}", self.next.render("Next Row", false, &self.witnesses));
log::debug!("Set RUST_LOG=trace to understand why these values were chosen.");
log::debug!(
"Assuming these values are correct, the following identities fail:\n{}\n",
@@ -389,8 +407,11 @@ impl<'a, T: FieldElement> Generator<'a, T> {
);
log::debug!("Some columns could not be determined, but setting them to zero does not satisfy the constraints. This typically means that the system is underconstrained!");
log::debug!("{}", self.current.render("Current Row", true));
log::debug!("{}", self.next.render("Next Row", true));
log::debug!(
"{}",
self.current.render("Current Row", true, &self.witnesses)
);
log::debug!("{}", self.next.render("Next Row", true, &self.witnesses));
log::debug!("\nSet RUST_LOG=trace to understand why these values were (not) chosen.");
log::debug!(
"Assuming zero for unknown values, the following identities fail:\n{}\n",

35
executor/src/witgen/machines/block_machine.rs
View File

@@ -240,6 +240,21 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
self.data.len() as DegreeType
}
fn name(&self) -> &str {
let first_witness = self.witness_cols.iter().next().unwrap();
let first_witness_name = self.fixed_data.column_name(first_witness);
let namespace = first_witness_name
.rfind('.')
.map(|idx| &first_witness_name[..idx]);
if let Some(namespace) = namespace {
namespace
} else {
// For machines compiled using Powdr ASM we'll always have a namespace, but as a last
// resort we'll use the first witness name.
first_witness_name
}
}
fn process_plookup_internal<'b>(
&mut self,
fixed_lookup: &'b mut FixedLookup<T>,
@@ -247,7 +262,7 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
right: &'a SelectedExpressions<T>,
machines: Machines<'a, 'b, T>,
) -> EvalResult<'a, T> {
log::trace!("Start processing block machine");
log::trace!("Start processing block machine '{}'", self.name());
log::trace!("Left values of lookup:");
for l in left {
log::trace!(" {}", l);
@@ -279,6 +294,10 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
let result = identity_processor.process_link(left, right, &row_pair)?;
if result.is_complete() {
log::trace!(
"End processing block machine '{}' (already solved)",
self.name()
);
return Ok(result);
}
}
@@ -288,6 +307,10 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
if !sequence_iterator.has_steps() {
// Shortcut, no need to do anything.
log::trace!(
"Abort processing block machine '{}' (inputs incomplete according to cache)",
self.name()
);
return Ok(EvalValue::incomplete(
IncompleteCause::BlockMachineLookupIncomplete,
));
@@ -316,7 +339,10 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
let success = left_new.iter().all(|v| v.is_constant());
if success {
log::trace!("End processing block machine (successfully)");
log::trace!(
"End processing block machine '{}' (successfully)",
self.name()
);
self.append_block(new_block)?;
// We solved the query, so report it to the cache.
@@ -324,7 +350,10 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
.report_processing_sequence(left, sequence_iterator);
Ok(EvalValue::complete(outer_assignments))
} else {
log::trace!("End processing block machine (incomplete)");
log::trace!(
"End processing block machine '{}' (incomplete)",
self.name()
);
self.processing_sequence_cache.report_incomplete(left);
Ok(EvalValue::incomplete(
IncompleteCause::BlockMachineLookupIncomplete,

14
executor/src/witgen/mod.rs
View File

@@ -104,12 +104,16 @@ where
// Are we in an infinite loop and can just re-use the old values?
let mut looping_period = None;
let mut loop_log_level = log::Level::Info;
for row in 0..degree as DegreeType {
// Check if we are in a loop.
if looping_period.is_none() && row % 100 == 0 && row > 0 {
looping_period = rows_are_repeating(&rows, &relevant_witnesses_mask);
if let Some(p) = looping_period {
log::info!("Found loop with period {p} starting at row {row}");
log::log!(
loop_log_level,
"Found loop with period {p} starting at row {row}"
);
}
}
let mut row_values = None;
@@ -118,8 +122,14 @@ where
if generator.propose_next_row(row, values, &mut mutable_state) {
row_values = Some(values.clone());
} else {
log::info!("Using loop failed. Trying to generate regularly again.");
log::log!(
loop_log_level,
"Looping failed. Trying to generate regularly again. (Use RUST_LOG=debug to see whether this happens more often.)"
);
looping_period = None;
// For some programs, loop detection will often find loops and then fail.
// In this case, we don't want to spam the user with debug messages.
loop_log_level = log::Level::Debug;
}
}
if row_values.is_none() {

9
executor/src/witgen/processor.rs
View File

@@ -184,14 +184,14 @@ impl<'a, 'b, T: FieldElement, CalldataAvailable> Processor<'a, 'b, T, CalldataAv
log::warn!("Error in identity: {identity}");
log::warn!(
"Known values in current row (local: {row_index}, global {global_row_index}):\n{}",
self.data[row_index].render_values(false),
self.data[row_index].render_values(false, Some(self.witness_cols)),
);
if identity.contains_next_ref() {
log::warn!(
"Known values in next row (local: {}, global {}):\n{}",
row_index + 1,
global_row_index + 1,
self.data[row_index + 1].render_values(false),
self.data[row_index + 1].render_values(false, Some(self.witness_cols)),
);
}
e
@@ -363,7 +363,10 @@ mod tests {
// In case of any error, this will be useful
for (i, row) in data.iter().enumerate() {
println!("{}", row.render(&format!("Row {i}"), true));
println!(
"{}",
row.render(&format!("Row {i}"), true, &processor.witness_cols)
);
}
for &(i, name, expected) in asserted_values.iter() {

16
executor/src/witgen/rows.rs
View File

@@ -4,7 +4,8 @@ use ast::analyzed::{Expression, PolynomialReference};
use itertools::Itertools;
use number::{DegreeType, FieldElement};
use crate::witgen::Constraint;
use crate::witgen::{Constraint, PolyID};
use std::collections::HashSet;
use super::{
affine_expression::{AffineExpression, AffineResult},
@@ -105,22 +106,27 @@ pub type Row<'a, T> = WitnessColumnMap<Cell<'a, T>>;
impl<T: FieldElement> Debug for Row<'_, T> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
f.write_str(&self.render("Row", true))
write!(f, "Row:\n{}", self.render_values(true, None))
}
}
impl<T: FieldElement> Row<'_, T> {
/// Builds a string representing the current row
pub fn render(&self, title: &str, include_unknown: bool) -> String {
format!("{}:\n{}", title, self.render_values(include_unknown))
pub fn render(&self, title: &str, include_unknown: bool, cols: &HashSet<PolyID>) -> String {
format!(
"{}:\n{}",
title,
self.render_values(include_unknown, Some(cols))
)
}
/// Builds a string listing all values, one by row. Nonzero entries are
/// first, then zero, then unknown (if `include_unknown == true`).
pub fn render_values(&self, include_unknown: bool) -> String {
pub fn render_values(&self, include_unknown: bool, cols: Option<&HashSet<PolyID>>) -> String {
let mut cells = self
.iter()
.filter(|(_, cell)| cell.value.is_known() || include_unknown)
.filter(|(col, _)| cols.map(|cols| cols.contains(col)).unwrap_or(true))
.collect::<Vec<_>>();
// Nonzero first, then zero, then unknown