fix: do not simplify constraints with induction variable

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

@@ -2761,7 +2761,7 @@ mod control_dependence {
 
     #[test]
     fn simplify_constraint() {
-        // This test shows the simplification of the constraint constrain v17 == u1 1 which is converted into constrain u1 0 == u1 1 in b5
+        // This test shows the constraint constrain v17 == u1 1 is not simplified into constrain u1 0 == u1 1
         let src = "
         brillig(inline) fn main f0 {
           entry(v0: u32, v1: u32, v2: u32):
@@ -2793,11 +2793,10 @@ mod control_dependence {
         ";
 
         let ssa = Ssa::from_str(src).unwrap();
-
         let ssa = ssa.loop_invariant_code_motion();
-        // The loop is guaranteed to fully execute, so we expect the constrain to be simplified into constrain u1 0 == u1 1
-        // However, even though the constrain is not a loop invariant we expect it to remain in place
-        // as it is control dependent upon its predecessor blocks which are not pure.
+
+        // Despite the loop is guaranteed to fully execute, which implies that the constrain will fail at some iteration,
+        // the constraint is not simplified in case some side-effect instruction would run in the previous iterations.
         assert_ssa_snapshot!(ssa, @r"
         brillig(inline) fn main f0 {
           b0(v0: u32, v1: u32, v2: u32):
@@ -2821,9 +2820,9 @@ mod control_dependence {
             jmp b5()
           b5():
             v15 = lt v3, u32 4
-            constrain u1 0 == u1 1
-            v17 = unchecked_add v3, u32 1
-            jmp b1(v17)
+            constrain v15 == u1 1
+            v16 = unchecked_add v3, u32 1
+            jmp b1(v16)
         }
         ");
     }

compiler/noirc_evaluator/src/ssa/opt/loop_invariant/simplify.rs

@@ -6,11 +6,10 @@ use crate::ssa::{
             binary::{BinaryEvaluationResult, eval_constant_binary_op},
         },
         integer::IntegerConstant,
-        value::{Value, ValueId},
+        value::ValueId,
     },
     opt::loop_invariant::BlockContext,
 };
-use acvm::{FieldElement, acir::AcirField};
 use noirc_errors::call_stack::CallStackId;
 
 use super::{LoopContext, LoopInvariantContext};
@@ -98,49 +97,6 @@ impl LoopInvariantContext<'_> {
         }
     }
 
-    /// Simplify 'assert(lhs < rhs)' into 'assert(max(lhs) < rhs)' if lhs is an induction variable and rhs a loop invariant
-    /// For this simplification to be valid, we need to ensure that the induction variable takes all the values from min(induction) up to max(induction)
-    /// This means that the assert must be executed at each loop iteration, and that the loop processes all the iteration space
-    /// This is ensured via control dependence and the check for break patterns, before calling this function.
-    fn simplify_induction_in_constrain(
-        &mut self,
-        loop_context: &LoopContext,
-        lhs: ValueId,
-        rhs: ValueId,
-        err: &Option<ConstrainError>,
-        call_stack: CallStackId,
-    ) -> SimplifyResult {
-        let mut extract_variables = |rhs, lhs| {
-            let rhs_true =
-                self.inserter.function.dfg.get_numeric_constant(rhs)? == FieldElement::one();
-            let (is_left, min, max, binary) =
-                self.extract_induction_and_invariant(loop_context, lhs)?;
-            match (is_left, rhs_true) {
-                (true, true) => Some((max, binary.rhs)),
-                (false, true) => Some((binary.lhs, min)),
-                _ => None,
-            }
-        };
-        let Some((new_lhs, new_rhs)) = extract_variables(rhs, lhs) else {
-            return SimplifyResult::None;
-        };
-        let new_binary =
-            Instruction::Binary(Binary { lhs: new_lhs, rhs: new_rhs, operator: BinaryOp::Lt });
-        // The new comparison can be safely hoisted to the pre-header because it is loop invariant and control independent
-        let comparison_results = self
-            .inserter
-            .function
-            .dfg
-            .insert_instruction_and_results(new_binary, loop_context.pre_header(), None, call_stack)
-            .results();
-        assert!(comparison_results.len() == 1);
-        SimplifyResult::SimplifiedToInstruction(Instruction::Constrain(
-            comparison_results[0],
-            rhs,
-            err.clone(),
-        ))
-    }
-
     /// Replace 'assert(invariant != induction)' with assert((invariant < min(induction) || (invariant > max(induction)))
     /// For this simplification to be valid, we need to ensure that the induction variable takes all the values from min(induction) up to max(induction)
     /// This means that the assert must be executed at each loop iteration, and that the loop processes all the iteration space.
@@ -183,27 +139,6 @@ impl LoopInvariantContext<'_> {
         ))
     }
 
-    /// Returns the binary instruction only if the input value refers to a binary instruction
-    /// with invariant and induction variables as operands.
-    /// The return values are:
-    /// - a boolean indicating if the induction variable is on the lhs
-    /// - the minimum and maximum values of the induction variable, coming from the loop bounds
-    /// - the binary instruction itself
-    fn extract_induction_and_invariant(
-        &mut self,
-        loop_context: &LoopContext,
-        value: ValueId,
-    ) -> Option<(bool, ValueId, ValueId, Binary)> {
-        let Value::Instruction { instruction, .. } = &self.inserter.function.dfg[value] else {
-            return None;
-        };
-        let Instruction::Binary(binary) = self.inserter.function.dfg[*instruction].clone() else {
-            return None;
-        };
-        self.match_induction_and_invariant(loop_context, &binary.lhs, &binary.rhs)
-            .map(|(is_left, min, max)| (is_left, min, max, binary))
-    }
-
     /// If the inputs are an induction and loop invariant variables, it returns
     /// the maximum and minimum values of the induction variable, based on the loop bounds,
     /// and a boolean indicating if the induction variable is on the lhs or rhs (true for lhs)
@@ -249,18 +184,6 @@ impl LoopInvariantContext<'_> {
                 binary,
                 block_context.is_header,
             ),
-            Instruction::Constrain(x, y, err) => {
-                // Ensure the loop is fully executed, so we know that if the constraint would fail for *some* value,
-                // then it *will* definitely take up that value, and not break out early.
-                if loop_context.no_break
-                    && block_context.can_simplify_control_dependent_instruction()
-                {
-                    assert!(block_context.does_execute, "executing a non executable loop");
-                    self.simplify_induction_in_constrain(loop_context, *x, *y, err, call_stack)
-                } else {
-                    SimplifyResult::None
-                }
-            }
             Instruction::ConstrainNotEqual(x, y, err) => {
                 // Ensure the loop is fully executed
                 if loop_context.no_break