Merge pull request #390 from powdr-labs/avoid_format

Use less formatting.

executor/src/witgen/eval_result.rs

@@ -29,6 +29,8 @@ pub enum IncompleteCause<K = usize> {
     NoQueryAnswer(String, String),
     /// Query match scrutinee is not constant, so the query fails. Example: evaluate `match x { 1 => 1, _ => 0}` but `x` is not constant.
     NonConstantQueryMatchScrutinee,
+    /// Query element is not constant.
+    NonConstantQueryElement,
     /// The left selector in a lookup is not constant. Example: `x * {1} in [{1}]` where `x` is not constant.
     NonConstantLeftSelector,
     /// A value to be written is not constant. TODO: should this be covered by another case? it's used for memory
@@ -37,6 +39,10 @@ pub enum IncompleteCause<K = usize> {
     ExpressionEvaluationUnimplemented(String),
     /// A value is not found on the left side of a match. Example: `match x {1 => 2, 3 => 4}` where `x == 0`
     NoMatchArmFound,
+    /// A lookup into a block machine was not able to assign all variables in the query. It could be that we just need to re-run it.
+    BlockMachineLookupIncomplete,
+    /// We could not (yet) read some data
+    DataNotYetAvailable,
     /// Last resort error when all possible solving approaches have failed. TODO: make this more precise or use another variant
     SolvingFailed,
     /// Some knowledge was learnt, but not a concrete value. Example: `Y = X` if we know that `Y` is boolean. We learn that `X` is boolean, but not its exact value.

executor/src/witgen/generator.rs

@@ -12,7 +12,9 @@ use super::range_constraints::RangeConstraint;
 use super::expression_evaluator::ExpressionEvaluator;
 use super::machines::{FixedLookup, Machine};
 use super::symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator};
-use super::{Constraint, EvalResult, EvalValue, FixedData, IncompleteCause, WitnessColumn};
+use super::{
+    Constraint, EvalError, EvalResult, EvalValue, FixedData, IncompleteCause, WitnessColumn,
+};
 
 pub struct Generator<'a, T: FieldElement, QueryCallback: Send + Sync> {
     fixed_data: &'a FixedData<'a, T>,
@@ -29,7 +31,7 @@ pub struct Generator<'a, T: FieldElement, QueryCallback: Send + Sync> {
     /// Range constraints on the witness polynomials in the next row.
     next_range_constraints: Vec<Option<RangeConstraint<T>>>,
     next_row: DegreeType,
-    failure_reasons: Vec<String>,
+    failure_reasons: Vec<EvalError<T>>,
     last_report: DegreeType,
     last_report_time: Instant,
 }
@@ -103,6 +105,9 @@ where
             SolvingStrategy::SingleVariableAffine,
             SolvingStrategy::AssumeZero,
         ] {
+            if identity_failed {
+                break;
+            }
             log::trace!("  Strategy: {:?}", strategy);
             loop {
                 identity_failed = false;
@@ -117,7 +122,7 @@ where
                 {
                     let result = self.process_identity(identity, strategy).map_err(|err| {
                         let msg = match strategy {
-                            SolvingStrategy::SingleVariableAffine => "No progress on",
+                            SolvingStrategy::SingleVariableAffine => "Solving failed on",
                             SolvingStrategy::AssumeZero => {
                                 "Assuming zero for unknown columns failed in"
                             }
@@ -152,7 +157,7 @@ where
                     }
                 }
 
-                if !progress {
+                if !progress || identity_failed {
                     break;
                 }
             }
@@ -183,7 +188,13 @@ where
                 "\nThe following columns are still undetermined in the current row:\n{}",
                 list_undetermined(&self.next)
             );
-            log::debug!("\nReasons:\n{}\n", self.failure_reasons.join("\n\n"));
+            log::debug!(
+                "\nReasons:\n{}\n",
+                self.failure_reasons
+                    .iter()
+                    .map(|r| r.to_string())
+                    .join("\n\n")
+            );
             log::debug!(
                 "Determined range constraints for this row:\n{}",
                 self.next_range_constraints
@@ -257,7 +268,7 @@ where
                 "{next_row} of {} rows ({} %, {} rows per second)",
                 self.fixed_data.degree,
                 next_row * 100 / self.fixed_data.degree,
-                1000000 / duration.as_millis()
+                1_000_000_000 / duration.as_micros()
             );
             self.last_report = next_row;
         }
@@ -328,11 +339,6 @@ where
         &self,
         query: &'b Expression<T>,
     ) -> Result<String, IncompleteCause<&'b PolynomialReference>> {
-        if let Ok(v) = self.evaluate(query, EvaluationRow::Next, EvaluateUnknown::Symbolic) {
-            if v.is_constant() {
-                return Ok(v.to_string());
-            }
-        }
         // TODO combine that with the constant evaluator and the commit evaluator...
         match query {
             Expression::Tuple(items) => Ok(items
@@ -351,7 +357,11 @@ where
             Expression::MatchExpression(scrutinee, arms) => {
                 self.interpolate_match_expression_for_query(scrutinee.as_ref(), arms)
             }
-            query => unimplemented!("Cannot handle / evaluate {query}"),
+            _ => self
+                .evaluate(query, EvaluationRow::Next, EvaluateUnknown::Symbolic)?
+                .constant_value()
+                .map(|c| c.to_string())
+                .ok_or(IncompleteCause::NonConstantQueryElement),
         }
     }
 
@@ -528,7 +538,7 @@ where
                 progress
             }
             Err(reason) => {
-                self.failure_reasons.push(format!("{reason}"));
+                self.failure_reasons.push(reason);
                 false
             }
         }

executor/src/witgen/machines/block_machine.rs

@@ -14,7 +14,7 @@ use crate::witgen::{
     symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator},
     Constraint, EvalError,
 };
-use crate::witgen::{Constraints, EvalValue};
+use crate::witgen::{Constraints, EvalValue, IncompleteCause};
 use ast::analyzed::{Expression, Identity, IdentityKind, PolynomialReference, SelectedExpressions};
 use number::{DegreeType, FieldElement};
 
@@ -144,13 +144,15 @@ impl<T: FieldElement> Machine<T> for BlockMachine<T> {
         Some({
             let result = self.process_plookup_internal(fixed_data, fixed_lookup, left, right);
             self.range_constraints.clear();
-            result.map_err(|e| {
-                // rollback the changes.
-                for col in self.data.values_mut() {
-                    col.truncate(previous_len)
+            if let Ok(assignments) = &result {
+                if !assignments.is_complete() {
+                    // rollback the changes.
+                    for col in self.data.values_mut() {
+                        col.truncate(previous_len)
+                    }
                 }
-                e
-            })
+            }
+            result
         })
     }
 
@@ -373,7 +375,9 @@ impl<T: FieldElement> BlockMachine<T> {
                 .reduce(|x: EvalError<T>, y| x.combine(y))
                 .unwrap())
         } else {
-            Err("Could not assign all variables in the query - maybe the machine does not have enough constraints?".to_string().into())
+            Ok(EvalValue::incomplete(
+                IncompleteCause::BlockMachineLookupIncomplete,
+            ))
         }
     }
 

executor/src/witgen/machines/sorted_witness_machine.rs

@@ -7,11 +7,11 @@ use super::fixed_lookup_machine::FixedLookup;
 use super::Machine;
 use super::{EvalResult, FixedData};
 use crate::witgen::affine_expression::AffineResult;
-use crate::witgen::EvalValue;
 use crate::witgen::{
     expression_evaluator::ExpressionEvaluator, fixed_evaluator::FixedEvaluator,
     symbolic_evaluator::SymbolicEvaluator,
 };
+use crate::witgen::{EvalValue, IncompleteCause};
 use ast::analyzed::{Expression, Identity, IdentityKind, PolynomialReference, SelectedExpressions};
 use number::FieldElement;
 
@@ -183,7 +183,7 @@ impl<T: FieldElement> SortedWitnesses<T> {
         right: &SelectedExpressions<T>,
         rhs: Vec<&PolynomialReference>,
     ) -> EvalResult<'a, T> {
-        // Fail if the LHS has an error.
+        // Return "incomplete" if the LHS has an error (we still need more information).
         let (left, errors): (Vec<_>, Vec<_>) = left.iter().partition_map(|x| match x {
             Ok(x) => Either::Left(x),
             Err(x) => Either::Right(x),
@@ -242,11 +242,7 @@ impl<T: FieldElement> SortedWitnesses<T> {
                         *stored_value = Some(v);
                     }
                     None => {
-                        return Err(format!(
-                            "Value {r} for key {} = {key_value} not known",
-                            self.key_col,
-                        )
-                        .into())
+                        return Ok(EvalValue::incomplete(IncompleteCause::DataNotYetAvailable));
                     }
                 },
             }