chore(ssa refactor): simplify acir_variable using to_expression (#1658)

chore(ssa refactor): simplify acir_variable using to_expression; return an error for unprovable programs

crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs

@@ -107,46 +107,36 @@ impl AcirContext {
     /// Note: `Variables` are immutable.
     pub(crate) fn neg_var(&mut self, var: AcirVar) -> AcirVar {
         let var_data = &self.vars[var];
-        match var_data {
-            AcirVarData::Witness(witness) => {
-                let mut expr = Expression::default();
-                expr.push_addition_term(-FieldElement::one(), *witness);
-
-                self.add_data(AcirVarData::Expr(expr))
-            }
-            AcirVarData::Expr(expr) => self.add_data(AcirVarData::Expr(-expr)),
-            AcirVarData::Const(constant) => self.add_data(AcirVarData::Const(-*constant)),
-        }
+        let result_data = if let AcirVarData::Const(constant) = var_data {
+            AcirVarData::Const(-*constant)
+        } else {
+            AcirVarData::Expr(-var_data.to_expression().as_ref())
+        };
+        self.add_data(result_data)
     }
 
     /// Adds a new Variable to context whose value will
     /// be constrained to be the inverse of `var`.
     pub(crate) fn inv_var(&mut self, var: AcirVar) -> Result<AcirVar, AcirGenError> {
         let var_data = &self.vars[var];
-        let inverted_witness = match var_data {
-            AcirVarData::Witness(witness) => {
-                let expr = Expression::from(*witness);
-                self.acir_ir.directive_inverse(&expr)
-            }
-            AcirVarData::Expr(expr) => self.acir_ir.directive_inverse(expr),
-            AcirVarData::Const(constant) => {
-                // Note that this will return a 0 if the inverse is not available
-                let result_var = self.add_data(AcirVarData::Const(constant.inverse()));
-                return Ok(result_var);
-            }
-        };
+        if let AcirVarData::Const(constant) = var_data {
+            // Note that this will return a 0 if the inverse is not available
+            let result_var = self.add_data(AcirVarData::Const(constant.inverse()));
+            return Ok(result_var);
+        }
+        let inverted_witness = self.acir_ir.directive_inverse(&var_data.to_expression());
         let inverted_var = self.add_data(AcirVarData::Witness(inverted_witness));
 
         let should_be_one = self.mul_var(inverted_var, var)?;
-        self.assert_eq_one(should_be_one);
+        self.assert_eq_one(should_be_one)?;
 
         Ok(inverted_var)
     }
 
     /// Constrains the lhs to be equal to the constant value `1`
-    pub(crate) fn assert_eq_one(&mut self, var: AcirVar) {
+    pub(crate) fn assert_eq_one(&mut self, var: AcirVar) -> Result<(), AcirGenError> {
         let one_var = self.add_constant(FieldElement::one());
-        self.assert_eq_var(var, one_var);
+        self.assert_eq_var(var, one_var)
     }
 
     /// Returns an `AcirVar` that is `1` if `lhs` equals `rhs` and
@@ -216,39 +206,25 @@ impl AcirContext {
     }
 
     /// Constrains the `lhs` and `rhs` to be equal.
-    pub(crate) fn assert_eq_var(&mut self, lhs: AcirVar, rhs: AcirVar) {
+    pub(crate) fn assert_eq_var(&mut self, lhs: AcirVar, rhs: AcirVar) -> Result<(), AcirGenError> {
         // TODO: could use sub_var and then assert_eq_zero
         let lhs_data = &self.vars[lhs];
         let rhs_data = &self.vars[rhs];
-
-        match (lhs_data, rhs_data) {
-            (AcirVarData::Witness(witness), AcirVarData::Expr(expr))
-            | (AcirVarData::Expr(expr), AcirVarData::Witness(witness)) => {
-                self.acir_ir.assert_is_zero(expr - *witness);
-            }
-            (AcirVarData::Witness(witness), AcirVarData::Const(constant))
-            | (AcirVarData::Const(constant), AcirVarData::Witness(witness)) => self
-                .acir_ir
-                .assert_is_zero(&Expression::from(*witness) - &Expression::from(*constant)),
-            (AcirVarData::Expr(expr), AcirVarData::Const(constant))
-            | (AcirVarData::Const(constant), AcirVarData::Expr(expr)) => {
-                self.acir_ir.assert_is_zero(expr.clone() - *constant);
-            }
-            (AcirVarData::Expr(lhs_expr), AcirVarData::Expr(rhs_expr)) => {
-                self.acir_ir.assert_is_zero(lhs_expr - rhs_expr);
-            }
-            (AcirVarData::Witness(lhs_witness), AcirVarData::Witness(rhs_witness)) => self
-                .acir_ir
-                .assert_is_zero(&Expression::from(*lhs_witness) - &Expression::from(*rhs_witness)),
-            (AcirVarData::Const(lhs_constant), AcirVarData::Const(rhs_constant)) => {
-                // TODO: for constants, we add it as a gate.
-                // TODO: Assuming users will never want to create unsatisfiable programs
-                // TODO: We could return an error here instead
-                self.acir_ir.assert_is_zero(Expression::from(FieldElement::from(
-                    lhs_constant == rhs_constant,
-                )));
+        if let (AcirVarData::Const(lhs_const), AcirVarData::Const(rhs_const)) = (lhs_data, rhs_data)
+        {
+            if lhs_const == rhs_const {
+                // Constraint is always true and need not be added
+                Ok(())
+            } else {
+                // Constraint is always false - this program is unprovable
+                Err(AcirGenError::BadConstantEquality { lhs: *lhs_const, rhs: *rhs_const })
             }
-        };
+        } else {
+            self.acir_ir.assert_is_zero(
+                lhs_data.to_expression().as_ref() - rhs_data.to_expression().as_ref(),
+            );
+            Ok(())
+        }
     }
 
     /// Adds a new Variable to context whose value will
@@ -322,47 +298,23 @@ impl AcirContext {
     pub(crate) fn add_var(&mut self, lhs: AcirVar, rhs: AcirVar) -> Result<AcirVar, AcirGenError> {
         let lhs_data = &self.vars[lhs];
         let rhs_data = &self.vars[rhs];
-        let result = match (lhs_data, rhs_data) {
-            (AcirVarData::Witness(witness), AcirVarData::Expr(expr))
-            | (AcirVarData::Expr(expr), AcirVarData::Witness(witness)) => {
-                self.add_data(AcirVarData::Expr(expr + &Expression::from(*witness)))
-            }
-            (AcirVarData::Witness(witness), AcirVarData::Const(constant))
-            | (AcirVarData::Const(constant), AcirVarData::Witness(witness)) => self.add_data(
-                AcirVarData::Expr(&Expression::from(*witness) + &Expression::from(*constant)),
-            ),
-            (AcirVarData::Expr(expr), AcirVarData::Const(constant))
-            | (AcirVarData::Const(constant), AcirVarData::Expr(expr)) => {
-                self.add_data(AcirVarData::Expr(expr + &Expression::from(*constant)))
-            }
-            (AcirVarData::Expr(lhs_expr), AcirVarData::Expr(rhs_expr)) => {
-                self.add_data(AcirVarData::Expr(lhs_expr + rhs_expr))
-            }
-            (AcirVarData::Witness(lhs), AcirVarData::Witness(rhs)) => {
-                // TODO: impl Add for Witness which returns an Expression instead of the below
-                self.add_data(AcirVarData::Expr(&Expression::from(*lhs) + &Expression::from(*rhs)))
-            }
-            (AcirVarData::Const(lhs_const), AcirVarData::Const(rhs_const)) => {
-                self.add_data(AcirVarData::Const(*lhs_const + *rhs_const))
-            }
+        let result_data = if let (AcirVarData::Const(lhs_const), AcirVarData::Const(rhs_const)) =
+            (lhs_data, rhs_data)
+        {
+            AcirVarData::Const(*lhs_const + *rhs_const)
+        } else {
+            let sum = lhs_data.to_expression().as_ref() + rhs_data.to_expression().as_ref();
+            AcirVarData::Expr(sum)
         };
-        Ok(result)
+        Ok(self.add_data(result_data))
     }
 
     /// Adds a new variable that is constrained to be the logical NOT of `x`.
     ///
     /// `x` must be a 1-bit integer (i.e. a boolean)
     pub(crate) fn not_var(&mut self, x: AcirVar) -> AcirVar {
         // Since `x` can only be 0 or 1, we can derive NOT as 1 - x
-        match &self.vars[x] {
-            AcirVarData::Const(constant) => {
-                self.add_data(AcirVarData::Expr(&Expression::one() - &Expression::from(*constant)))
-            }
-            AcirVarData::Expr(expr) => self.add_data(AcirVarData::Expr(&Expression::one() - expr)),
-            AcirVarData::Witness(witness) => {
-                self.add_data(AcirVarData::Expr(&Expression::one() - *witness))
-            }
-        }
+        self.add_data(AcirVarData::Expr(&Expression::one() - self.vars[x].to_expression().as_ref()))
     }
 
     /// Returns an `AcirVar` that is constrained to be `lhs << rhs`.

crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/errors.rs

@@ -1,8 +1,11 @@
+use acvm::FieldElement;
+
 #[derive(Debug, PartialEq, Eq, Clone)]
 pub(crate) enum AcirGenError {
     InvalidRangeConstraint { num_bits: u32 },
     IndexOutOfBounds { index: usize, array_size: usize },
     UnsupportedIntegerSize { num_bits: u32, max_num_bits: u32 },
+    BadConstantEquality { lhs: FieldElement, rhs: FieldElement },
 }
 
 impl AcirGenError {
@@ -19,6 +22,9 @@ impl AcirGenError {
             AcirGenError::UnsupportedIntegerSize { num_bits, max_num_bits } => {
                 format!("Integer sized {num_bits} is over the max supported size of {max_num_bits}")
             }
+            AcirGenError::BadConstantEquality { lhs, rhs } => {
+                format!("{lhs} and {rhs} constrained to be equal though they never can be")
+            }
         }
     }
 }

crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs

@@ -159,7 +159,9 @@ impl Context {
             }
             Instruction::Constrain(value_id) => {
                 let constrain_condition = self.convert_numeric_value(*value_id, dfg);
-                self.acir_context.assert_eq_one(constrain_condition);
+                self.acir_context
+                    .assert_eq_one(constrain_condition)
+                    .expect("add Result types to all methods so errors bubble up");
             }
             Instruction::Cast(value_id, typ) => {
                 let result_acir_var = self.convert_ssa_cast(value_id, typ, dfg);