Explicitly handle the case for unsatisfiable constraints.

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)| {

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<EvalError>),
 }
@@ -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.",)
             }

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()
                     }

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) => {

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);
                         }
                     }
                 }