fix(ssa): Use post order when mapping instructions in loop invariant …

…pass (#7140)

Co-authored-by: Tom French <[email protected]>

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

@@ -16,6 +16,7 @@ use crate::ssa::{
         function::Function,
         function_inserter::FunctionInserter,
         instruction::{binary::eval_constant_binary_op, BinaryOp, Instruction, InstructionId},
+        post_order::PostOrder,
         types::Type,
         value::ValueId,
     },
@@ -272,8 +273,10 @@ impl<'f> LoopInvariantContext<'f> {
     /// correct new value IDs based upon the `FunctionInserter` internal map.
     /// Leaving out this mapping could lead to instructions with values that do not exist.
     fn map_dependent_instructions(&mut self) {
-        let blocks = self.inserter.function.reachable_blocks();
-        for block in blocks {
+        let mut block_order = PostOrder::with_function(self.inserter.function).into_vec();
+        block_order.reverse();
+
+        for block in block_order {
             for instruction_id in self.inserter.function.dfg[block].take_instructions() {
                 self.inserter.push_instruction(instruction_id, block);
             }

test_programs/execution_failure/regression_7128/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "regression_7128"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_failure/regression_7128/Prover.toml

@@ -0,0 +1 @@
+in0 = "1"

test_programs/execution_failure/regression_7128/src/main.nr

@@ -0,0 +1,26 @@
+fn main(in0: Field) -> pub Field {
+    let mut out0: Field = 0;
+    let tmp1: Field = in0;
+
+    if (out0 == out0) // <== changing out0 to in0 or removing
+    {
+        //     the comparison changes the result
+        let in0_as_bytes: [u8; 32] = in0.to_be_bytes();
+        let mut result: [u8; 32] = [0; 32];
+        for i in 0..32 {
+            result[i] = in0_as_bytes[i];
+        }
+    }
+
+    let mut tmp2: Field = 0; // <== moving this to the top of main,
+    if (0.lt(in0)) //     changes the result
+    {
+        tmp2 = 1;
+    }
+
+    out0 = (tmp2 - tmp1);
+
+    assert(out0 != 0, "soundness violation");
+
+    out0
+}

test_programs/execution_success/regression_7128/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "regression_7128"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_success/regression_7128/Prover.toml

@@ -0,0 +1 @@
+in0 = "1"

test_programs/execution_success/regression_7128/src/main.nr

@@ -0,0 +1,26 @@
+fn main(in0: Field) -> pub Field {
+    let mut out0: Field = 0;
+    let tmp1: Field = in0;
+
+    if (out0 == out0) // <== changing out0 to in0 or removing
+    {
+        //     the comparison changes the result
+        let in0_as_bytes: [u8; 32] = in0.to_be_bytes();
+        let mut result: [u8; 32] = [0; 32];
+        for i in 0..32 {
+            result[i] = in0_as_bytes[i];
+        }
+    }
+
+    let mut tmp2: Field = 0; // <== moving this to the top of main,
+    if (0.lt(in0)) //     changes the result
+    {
+        tmp2 = 1;
+    }
+
+    out0 = (tmp2 - tmp1);
+
+    assert(out0 == 0, "completeness violation");
+
+    out0
+}