From 50be1258249768302dd16d74ee9ae2d4d75aec27 Mon Sep 17 00:00:00 2001 From: guipublic Date: Wed, 10 Sep 2025 14:31:33 +0200 Subject: [PATCH 1/2] do not simplify constraints with induction variable --- .../src/ssa/opt/loop_invariant/simplify.rs | 79 +------------------ 1 file changed, 1 insertion(+), 78 deletions(-) diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant/simplify.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant/simplify.rs index e9dc095ae4c..80f9ad0a3c1 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant/simplify.rs +++ b/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, - 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 From 678988ce5b3c771c40e34518896e9c3b8e6b4367 Mon Sep 17 00:00:00 2001 From: guipublic Date: Wed, 10 Sep 2025 15:47:45 +0200 Subject: [PATCH 2/2] fix unit test --- .../noirc_evaluator/src/ssa/opt/loop_invariant.rs | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs index f39dffbd432..539513b7093 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs +++ b/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) } "); }