diff --git a/executor/src/witgen/eval_result.rs b/executor/src/witgen/eval_result.rs index 2cc1c8f42..c893762eb 100644 --- a/executor/src/witgen/eval_result.rs +++ b/executor/src/witgen/eval_result.rs @@ -29,6 +29,8 @@ pub enum IncompleteCause { 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 { 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. diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs index bc05ecdb5..94bdd9403 100644 --- a/executor/src/witgen/generator.rs +++ b/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>>, next_row: DegreeType, - failure_reasons: Vec, + failure_reasons: Vec>, 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, ) -> Result> { - 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 } } diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs index 144274701..0583cccb0 100644 --- a/executor/src/witgen/machines/block_machine.rs +++ b/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 Machine for BlockMachine { 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 BlockMachine { .reduce(|x: EvalError, 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, + )) } } diff --git a/executor/src/witgen/machines/sorted_witness_machine.rs b/executor/src/witgen/machines/sorted_witness_machine.rs index e71ea2859..a02e5102e 100644 --- a/executor/src/witgen/machines/sorted_witness_machine.rs +++ b/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 SortedWitnesses { right: &SelectedExpressions, 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 SortedWitnesses { *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)); } }, }