From 20fabd38e43db0929d37cdbdb32e9bce2c6ee9dd Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 30 Mar 2023 17:31:25 +0200 Subject: [PATCH] Explicitly handle the case for unsatisfiable constraints. --- src/witness_generator/affine_expression.rs | 61 ++++++++++--------- src/witness_generator/eval_error.rs | 5 ++ src/witness_generator/generator.rs | 8 ++- .../machines/fixed_lookup_machine.rs | 26 ++++---- .../machines/sorted_witness_machine.rs | 42 ++++++------- 5 files changed, 75 insertions(+), 67 deletions(-) diff --git a/src/witness_generator/affine_expression.rs b/src/witness_generator/affine_expression.rs index 1da08441c..569297689 100644 --- a/src/witness_generator/affine_expression.rs +++ b/src/witness_generator/affine_expression.rs @@ -5,6 +5,7 @@ use crate::number::{format_number, is_zero, AbstractNumberType, GOLDILOCKS_MOD}; use super::bit_constraints::BitConstraintSet; use super::eval_error::EvalError::ConflictingBitConstraints; +use super::eval_error::EvalError::ConstraintUnsatisfiable; use super::util::WitnessColumnNamer; use super::Constraint; use super::EvalResult; @@ -80,28 +81,36 @@ impl AffineExpression { /// affine expression to zero. pub fn solve(&self) -> EvalResult { let mut nonzero = self.nonzero_coefficients(); - nonzero - .next() - .and_then(|(i, c)| { - if nonzero.next().is_none() { - // c * a + o = 0 <=> a = -o/c - Some(vec![( - i, - Constraint::Assignment(if *c == 1.into() { - clamp(-self.offset.clone()) - } else if *c == (-1).into() || *c == (GOLDILOCKS_MOD - 1).into() { - self.offset.clone() - } else { - clamp(-clamp( - self.offset.clone() * inv(c.clone(), GOLDILOCKS_MOD.into()), - )) - }), - )]) + let first = nonzero.next(); + let second = nonzero.next(); + match (first, second) { + (Some((i, c)), None) => { + // c * a + o = 0 <=> a = -o/c + Ok(vec![( + i, + Constraint::Assignment(if *c == 1.into() { + clamp(-self.offset.clone()) + } else if *c == (-1).into() || *c == (GOLDILOCKS_MOD - 1).into() { + self.offset.clone() + } else { + clamp(-clamp( + self.offset.clone() * inv(c.clone(), GOLDILOCKS_MOD.into()), + )) + }), + )]) + } + (Some(_), Some(_)) => Err("Too many variables in linear constraint." + .to_string() + .into()), + (None, None) => { + if self.offset == 0.into() { + Ok(vec![]) } else { - None + Err(ConstraintUnsatisfiable(String::new())) } - }) - .ok_or_else(|| "Cannot solve affine expression.".to_string().into()) + } + (None, Some(_)) => panic!(), + } } /// Tries to solve "self = 0", or at least propagate a bit constraint: @@ -114,8 +123,10 @@ impl AffineExpression { known_constraints: &impl BitConstraintSet, ) -> EvalResult { // Try to solve directly. - if let Ok(result) = self.solve() { - return Ok(result); + match self.solve() { + Ok(result) => return Ok(result), + Err(ConstraintUnsatisfiable(e)) => return Err(ConstraintUnsatisfiable(e)), + Err(_) => {} } let new_constraints: Option<_> = if self .nonzero_coefficients() @@ -244,12 +255,6 @@ impl AffineExpression { } } - /// Returns true if it can be determined that this expression can never be zero. - pub fn is_invalid(&self) -> bool { - // TODO add constraint validity. - self.constant_value().map(|v| v != 0.into()) == Some(true) - } - pub fn format(&self, namer: &impl WitnessColumnNamer) -> String { self.nonzero_coefficients() .map(|(i, c)| { diff --git a/src/witness_generator/eval_error.rs b/src/witness_generator/eval_error.rs index 864f2d7a3..99e54efbc 100644 --- a/src/witness_generator/eval_error.rs +++ b/src/witness_generator/eval_error.rs @@ -6,6 +6,8 @@ pub enum EvalError { PreviousValueUnknown(String), /// Conflicting bit-constraints in an equation, i.e. for X = 0x100, where X is known to be at most 0xff. ConflictingBitConstraints, + /// A constraint that cannot be satisfied (i.e. 2 = 1). + ConstraintUnsatisfiable(String), Generic(String), Multiple(Vec), } @@ -36,6 +38,9 @@ impl Display for EvalError { f, "Previous value of the following column(s) is not (yet) known: {names}.", ), + EvalError::ConstraintUnsatisfiable(e) => { + write!(f, "Linear constraint is not satisfiable: {e}",) + } EvalError::ConflictingBitConstraints => { write!(f, "Bit constraints in the expression are conflicting or do not match the constant / offset.",) } diff --git a/src/witness_generator/generator.rs b/src/witness_generator/generator.rs index 77c2dba44..3d804e637 100644 --- a/src/witness_generator/generator.rs +++ b/src/witness_generator/generator.rs @@ -263,10 +263,12 @@ where } else { evaluated .solve_with_bit_constraints(&self.bit_constraint_set()) - .map_err(|_| { + .map_err(|e| { let formatted = evaluated.format(self.fixed_data); - if evaluated.is_invalid() { - format!("Constraint is invalid ({formatted} != 0).").into() + if let EvalError::ConstraintUnsatisfiable(_) = e { + EvalError::ConstraintUnsatisfiable(format!( + "Constraint is invalid ({formatted} != 0)." + )) } else { format!("Could not solve expression {formatted} = 0.").into() } diff --git a/src/witness_generator/machines/fixed_lookup_machine.rs b/src/witness_generator/machines/fixed_lookup_machine.rs index e35cdb948..084d785a1 100644 --- a/src/witness_generator/machines/fixed_lookup_machine.rs +++ b/src/witness_generator/machines/fixed_lookup_machine.rs @@ -129,20 +129,20 @@ impl FixedLookup { // TODO we could use bit constraints here match evaluated.solve() { Ok(constraints) => result.extend(constraints), - Err(_) => { - let formatted = l.format(fixed_data); - if evaluated.is_invalid() { - // Fail the whole lookup - return Err( - format!("Constraint is invalid ({formatted} != {r}).",).into(), - ); - } else { - reasons.push( - format!("Could not solve expression {formatted} = {r}.",) - .into(), - ) - } + Err(EvalError::ConstraintUnsatisfiable(_)) => { + // Fail the whole lookup + return Err(EvalError::ConstraintUnsatisfiable(format!( + "Constraint is invalid ({} != {r}).", + l.format(fixed_data) + ))); } + Err(err) => reasons.push( + format!( + "Could not solve expression {} = {r}: {err}", + l.format(fixed_data) + ) + .into(), + ), } } Err(err) => { diff --git a/src/witness_generator/machines/sorted_witness_machine.rs b/src/witness_generator/machines/sorted_witness_machine.rs index be1aabc6d..783582c7d 100644 --- a/src/witness_generator/machines/sorted_witness_machine.rs +++ b/src/witness_generator/machines/sorted_witness_machine.rs @@ -225,31 +225,27 @@ impl SortedWitnesses { match stored_value { // There is a stored value Some(v) => { - let constraint = l.clone() - (*v).clone().into(); - if constraint.is_invalid() { - // The LHS value is known and it is differetn from the stored one. - return Err(format!( - "Lookup mismatch: There is already a unique row with {} = \ + match (l.clone() - (*v).clone().into()).solve() { + Err(EvalError::ConstraintUnsatisfiable(_)) => { + // The LHS value is known and it is differetn from the stored one. + return Err(format!( + "Lookup mismatch: There is already a unique row with {} = \ {key_value} and {r} = {v}, but wanted to store {r} = {}", - self.key_col, - l.format(fixed_data), - ) - .into()); - } else if constraint.constant_value() == Some(0.into()) { - // Just a repeated lookup. - } else { - match constraint.solve() { - Ok(ass) => { - if fixed_data.verbose { - println!("Read {} = {key_value} -> {r} = {v}", self.key_col); - } - assignments.extend(ass); - } - Err(_) => { - return Err( - format!("Cannot solve {} = {v}", l.format(fixed_data)).into() - ) + self.key_col, + l.format(fixed_data), + ) + .into()); + } + Err(_) => { + return Err( + format!("Cannot solve {} = {v}", l.format(fixed_data)).into() + ) + } + Ok(ass) => { + if !ass.is_empty() && fixed_data.verbose { + println!("Read {} = {key_value} -> {r} = {v}", self.key_col); } + assignments.extend(ass); } } }