feat: add ConstrainNotEqual instruction (#7032)

compiler/noirc_evaluator/src/acir/acir_variable.rs

@@ -541,6 +541,29 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
         Ok(())
     }
 
+    /// Constrains the `lhs` and `rhs` to be non-equal.
+    ///
+    /// This is done by asserting the existence of an inverse for the value `lhs - rhs`.
+    /// The constraint `(lhs - rhs) * inverse == 1` will only be satisfiable if `lhs` and `rhs` are non-equal.
+    pub(crate) fn assert_neq_var(
+        &mut self,
+        lhs: AcirVar,
+        rhs: AcirVar,
+        assert_message: Option<AssertionPayload<F>>,
+    ) -> Result<(), RuntimeError> {
+        let diff_var = self.sub_var(lhs, rhs)?;
+
+        let one = self.add_constant(F::one());
+        let _ = self.inv_var(diff_var, one)?;
+        if let Some(payload) = assert_message {
+            self.acir_ir
+                .assertion_payloads
+                .insert(self.acir_ir.last_acir_opcode_location(), payload);
+        }
+
+        Ok(())
+    }
+
     pub(crate) fn vars_to_expressions_or_memory(
         &self,
         values: &[AcirValue],

compiler/noirc_evaluator/src/acir/mod.rs

@@ -723,6 +723,47 @@ impl<'a> Context<'a> {
 
                 self.acir_context.assert_eq_var(lhs, rhs, assert_payload)?;
             }
+            Instruction::ConstrainNotEqual(lhs, rhs, assert_message) => {
+                let lhs = self.convert_numeric_value(*lhs, dfg)?;
+                let rhs = self.convert_numeric_value(*rhs, dfg)?;
+
+                let assert_payload = if let Some(error) = assert_message {
+                    match error {
+                        ConstrainError::StaticString(string) => Some(
+                            self.acir_context.generate_assertion_message_payload(string.clone()),
+                        ),
+                        ConstrainError::Dynamic(error_selector, is_string_type, values) => {
+                            if let Some(constant_string) = try_to_extract_string_from_error_payload(
+                                *is_string_type,
+                                values,
+                                dfg,
+                            ) {
+                                Some(
+                                    self.acir_context
+                                        .generate_assertion_message_payload(constant_string),
+                                )
+                            } else {
+                                let acir_vars: Vec<_> = values
+                                    .iter()
+                                    .map(|value| self.convert_value(*value, dfg))
+                                    .collect();
+
+                                let expressions_or_memory =
+                                    self.acir_context.vars_to_expressions_or_memory(&acir_vars)?;
+
+                                Some(AssertionPayload {
+                                    error_selector: error_selector.as_u64(),
+                                    payload: expressions_or_memory,
+                                })
+                            }
+                        }
+                    }
+                } else {
+                    None
+                };
+
+                self.acir_context.assert_neq_var(lhs, rhs, assert_payload)?;
+            }
             Instruction::Cast(value_id, _) => {
                 let acir_var = self.convert_numeric_value(*value_id, dfg)?;
                 self.define_result_var(dfg, instruction_id, acir_var);

compiler/noirc_evaluator/src/brillig/brillig_gen/brillig_block.rs

@@ -279,6 +279,10 @@ impl<'block> BrilligBlock<'block> {
                     self.brillig_context.deallocate_single_addr(condition);
                 }
             }
+            Instruction::ConstrainNotEqual(..) => {
+                unreachable!("only implemented in ACIR")
+            }
+
             Instruction::Allocate => {
                 let result_value = dfg.instruction_results(instruction_id)[0];
                 let pointer = self.variables.define_single_addr_variable(

compiler/noirc_evaluator/src/ssa.rs

@@ -186,6 +186,7 @@ fn optimize_all(builder: SsaBuilder, options: &SsaEvaluatorOptions) -> Result<Ss
         .run_pass(Ssa::fold_constants, "Constant Folding")
         .run_pass(Ssa::remove_enable_side_effects, "EnableSideEffectsIf removal")
         .run_pass(Ssa::fold_constants_using_constraints, "Constraint Folding")
+        .run_pass(Ssa::make_constrain_not_equal_instructions, "Adding constrain not equal")
         .run_pass(Ssa::dead_instruction_elimination, "Dead Instruction Elimination (1st)")
         .run_pass(Ssa::simplify_cfg, "Simplifying:")
         .run_pass(Ssa::array_set_optimization, "Array Set Optimizations")

compiler/noirc_evaluator/src/ssa/checks/check_for_underconstrained_values.rs

@@ -267,7 +267,8 @@ impl DependencyContext {
                 }
                 // Check the constrain instruction arguments against those
                 // involved in Brillig calls, remove covered calls
-                Instruction::Constrain(value_id1, value_id2, _) => {
+                Instruction::Constrain(value_id1, value_id2, _)
+                | Instruction::ConstrainNotEqual(value_id1, value_id2, _) => {
                     self.clear_constrained(
                         &[function.dfg.resolve(*value_id1), function.dfg.resolve(*value_id2)],
                         function,
@@ -555,6 +556,7 @@ impl Context {
                 | Instruction::Binary(..)
                 | Instruction::Cast(..)
                 | Instruction::Constrain(..)
+                | Instruction::ConstrainNotEqual(..)
                 | Instruction::IfElse { .. }
                 | Instruction::Load { .. }
                 | Instruction::Not(..)

compiler/noirc_evaluator/src/ssa/ir/instruction.rs

@@ -256,6 +256,9 @@ pub(crate) enum Instruction {
     /// Constrains two values to be equal to one another.
     Constrain(ValueId, ValueId, Option<ConstrainError>),
 
+    /// Constrains two values to not be equal to one another.
+    ConstrainNotEqual(ValueId, ValueId, Option<ConstrainError>),
+
     /// Range constrain `value` to `max_bit_size`
     RangeCheck { value: ValueId, max_bit_size: u32, assert_message: Option<String> },
 
@@ -364,6 +367,7 @@ impl Instruction {
                 InstructionResultType::Operand(*value)
             }
             Instruction::Constrain(..)
+            | Instruction::ConstrainNotEqual(..)
             | Instruction::Store { .. }
             | Instruction::IncrementRc { .. }
             | Instruction::DecrementRc { .. }
@@ -405,7 +409,7 @@ impl Instruction {
             },
 
             // These can fail.
-            Constrain(..) | RangeCheck { .. } => true,
+            Constrain(..) | ConstrainNotEqual(..) | RangeCheck { .. } => true,
 
             // This should never be side-effectful
             MakeArray { .. } | Noop => false,
@@ -472,7 +476,7 @@ impl Instruction {
             },
 
             // We can deduplicate these instructions if we know the predicate is also the same.
-            Constrain(..) | RangeCheck { .. } => deduplicate_with_predicate,
+            Constrain(..) | ConstrainNotEqual(..) | RangeCheck { .. } => deduplicate_with_predicate,
 
             // Noop instructions can always be deduplicated, although they're more likely to be
             // removed entirely.
@@ -540,6 +544,7 @@ impl Instruction {
             }
 
             Constrain(..)
+            | ConstrainNotEqual(..)
             | EnableSideEffectsIf { .. }
             | IncrementRc { .. }
             | DecrementRc { .. }
@@ -610,6 +615,7 @@ impl Instruction {
             Instruction::Cast(_, _)
             | Instruction::Not(_)
             | Instruction::Truncate { .. }
+            | Instruction::ConstrainNotEqual(..)
             | Instruction::Constrain(_, _, _)
             | Instruction::RangeCheck { .. }
             | Instruction::Allocate
@@ -656,6 +662,22 @@ impl Instruction {
                 });
                 Instruction::Constrain(lhs, rhs, assert_message)
             }
+            Instruction::ConstrainNotEqual(lhs, rhs, assert_message) => {
+                // Must map the `lhs` and `rhs` first as the value `f` is moved with the closure
+                let lhs = f(*lhs);
+                let rhs = f(*rhs);
+                let assert_message = assert_message.as_ref().map(|error| match error {
+                    ConstrainError::Dynamic(selector, is_string, payload_values) => {
+                        ConstrainError::Dynamic(
+                            *selector,
+                            *is_string,
+                            payload_values.iter().map(|&value| f(value)).collect(),
+                        )
+                    }
+                    _ => error.clone(),
+                });
+                Instruction::ConstrainNotEqual(lhs, rhs, assert_message)
+            }
             Instruction::Call { func, arguments } => Instruction::Call {
                 func: f(*func),
                 arguments: vecmap(arguments.iter().copied(), f),
@@ -714,7 +736,8 @@ impl Instruction {
             Instruction::Truncate { value, bit_size: _, max_bit_size: _ } => {
                 *value = f(*value);
             }
-            Instruction::Constrain(lhs, rhs, assert_message) => {
+            Instruction::Constrain(lhs, rhs, assert_message)
+            | Instruction::ConstrainNotEqual(lhs, rhs, assert_message) => {
                 *lhs = f(*lhs);
                 *rhs = f(*rhs);
                 if let Some(ConstrainError::Dynamic(_, _, payload_values)) = assert_message {
@@ -786,7 +809,8 @@ impl Instruction {
             | Instruction::Load { address: value } => {
                 f(*value);
             }
-            Instruction::Constrain(lhs, rhs, assert_error) => {
+            Instruction::Constrain(lhs, rhs, assert_error)
+            | Instruction::ConstrainNotEqual(lhs, rhs, assert_error) => {
                 f(*lhs);
                 f(*rhs);
                 if let Some(ConstrainError::Dynamic(_, _, values)) = assert_error.as_ref() {
@@ -878,6 +902,7 @@ impl Instruction {
                     SimplifiedToInstructionMultiple(constraints)
                 }
             }
+            Instruction::ConstrainNotEqual(..) => None,
             Instruction::ArrayGet { array, index } => {
                 if let Some(index) = dfg.get_numeric_constant(*index) {
                     try_optimize_array_get_from_previous_set(dfg, *array, index)

compiler/noirc_evaluator/src/ssa/ir/printer.rs

@@ -198,6 +198,14 @@ fn display_instruction_inner(
                 writeln!(f)
             }
         }
+        Instruction::ConstrainNotEqual(lhs, rhs, error) => {
+            write!(f, "constrain {} != {}", show(*lhs), show(*rhs))?;
+            if let Some(error) = error {
+                display_constrain_error(dfg, error, f)
+            } else {
+                writeln!(f)
+            }
+        }
         Instruction::Call { func, arguments } => {
             let arguments = value_list(dfg, arguments);
             writeln!(f, "call {}({}){}", show(*func), arguments, result_types(dfg, results))

compiler/noirc_evaluator/src/ssa/opt/make_constrain_not_equal.rs

@@ -0,0 +1,72 @@
+use acvm::AcirField;
+
+use crate::ssa::{
+    ir::{
+        function::Function,
+        instruction::{Binary, BinaryOp, Instruction},
+        value::Value,
+    },
+    ssa_gen::Ssa,
+};
+
+impl Ssa {
+    /// A simple SSA pass to go through each [`Instruction::Constrain`], determine whether it's asserting
+    /// two values are not equal, and if so replace it with a [`Instruction::ConstrainNotEqual`].
+    ///
+    /// Note that this pass must be placed after CFG flattening as the flattening pass cannot
+    /// handle this instruction.
+    #[tracing::instrument(level = "trace", skip(self))]
+    pub(crate) fn make_constrain_not_equal_instructions(mut self) -> Ssa {
+        for function in self.functions.values_mut() {
+            function.make_constrain_not_equal();
+        }
+        self
+    }
+}
+
+impl Function {
+    pub(crate) fn make_constrain_not_equal(&mut self) {
+        if !self.runtime().is_acir() {
+            return;
+        }
+
+        for block in self.reachable_blocks() {
+            let instructions = self.dfg[block].instructions().to_vec();
+
+            for instruction in instructions {
+                let constrain_ne: Instruction = match &self.dfg[instruction] {
+                    Instruction::Constrain(lhs, rhs, msg) => {
+                        if self
+                            .dfg
+                            .get_numeric_constant(*rhs)
+                            .map_or(false, |constant| constant.is_zero())
+                        {
+                            if let Value::Instruction { instruction, .. } =
+                                &self.dfg[self.dfg.resolve(*lhs)]
+                            {
+                                if let Instruction::Binary(Binary {
+                                    lhs,
+                                    rhs,
+                                    operator: BinaryOp::Eq,
+                                    ..
+                                }) = self.dfg[*instruction]
+                                {
+                                    Instruction::ConstrainNotEqual(lhs, rhs, msg.clone())
+                                } else {
+                                    continue;
+                                }
+                            } else {
+                                continue;
+                            }
+                        } else {
+                            continue;
+                        }
+                    }
+                    _ => continue,
+                };
+
+                self.dfg[instruction] = constrain_ne;
+            }
+        }
+    }
+}

compiler/noirc_evaluator/src/ssa/opt/mod.rs

@@ -14,6 +14,7 @@ pub(crate) mod flatten_cfg;
 mod hint;
 mod inlining;
 mod loop_invariant;
+mod make_constrain_not_equal;
 mod mem2reg;
 mod normalize_value_ids;
 mod rc;

compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs

@@ -143,6 +143,7 @@ impl Context {
             | Not(_)
             | Truncate { .. }
             | Constrain(..)
+            | ConstrainNotEqual(..)
             | RangeCheck { .. }
             | IfElse { .. }
             | IncrementRc { .. }