diff --git a/compiler/tests/pil.rs b/compiler/tests/pil.rs index 934c422d4..b7cf8e2b4 100644 --- a/compiler/tests/pil.rs +++ b/compiler/tests/pil.rs @@ -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] diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs index fa763cc0c..a6f084840 100644 --- a/executor/src/witgen/generator.rs +++ b/executor/src/witgen/generator.rs @@ -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, + witnesses: HashSet, 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", diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs index 656ba44e9..2f3d45a62 100644 --- a/executor/src/witgen/machines/block_machine.rs +++ b/executor/src/witgen/machines/block_machine.rs @@ -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, @@ -247,7 +262,7 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> { right: &'a SelectedExpressions, 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, diff --git a/executor/src/witgen/mod.rs b/executor/src/witgen/mod.rs index a9a2053cb..8d47cf216 100644 --- a/executor/src/witgen/mod.rs +++ b/executor/src/witgen/mod.rs @@ -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() { diff --git a/executor/src/witgen/processor.rs b/executor/src/witgen/processor.rs index 663776051..e71f2d444 100644 --- a/executor/src/witgen/processor.rs +++ b/executor/src/witgen/processor.rs @@ -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() { diff --git a/executor/src/witgen/rows.rs b/executor/src/witgen/rows.rs index e24c79803..599375cca 100644 --- a/executor/src/witgen/rows.rs +++ b/executor/src/witgen/rows.rs @@ -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>; impl 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 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) -> 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>) -> 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::>(); // Nonzero first, then zero, then unknown