fix: mark field division and modulo as requiring predicate for all necessary types

compiler/noirc_evaluator/src/acir/acir_variable.rs

@@ -549,12 +549,12 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
         &mut self,
         lhs: AcirVar,
         rhs: AcirVar,
+        predicate: 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)?;
+        let _ = self.inv_var(diff_var, predicate)?;
         if let Some(payload) = assert_message {
             self.acir_ir
                 .assertion_payloads
@@ -613,7 +613,7 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
             }
             NumericType::Signed { bit_size } => {
                 let (quotient_var, _remainder_var) =
-                    self.signed_division_var(lhs, rhs, bit_size)?;
+                    self.signed_division_var(lhs, rhs, bit_size, predicate)?;
                 Ok(quotient_var)
             }
         }
@@ -1050,6 +1050,7 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
         lhs: AcirVar,
         rhs: AcirVar,
         bit_size: u32,
+        predicate: AcirVar,
     ) -> Result<(AcirVar, AcirVar), RuntimeError> {
         // We derive the signed division from the unsigned euclidean division.
         // note that this is not euclidean division!
@@ -1079,7 +1080,7 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
 
         // Performs the division using the unsigned values of lhs and rhs
         let (q1, r1) =
-            self.euclidean_division_var(unsigned_lhs, unsigned_rhs, bit_size - 1, one)?;
+            self.euclidean_division_var(unsigned_lhs, unsigned_rhs, bit_size - 1, predicate)?;
 
         // Unsigned to signed: derive q and r from q1,r1 and the signs of lhs and rhs
         // Quotient sign is lhs sign * rhs sign, whose resulting sign bit is the XOR of the sign bits
@@ -1117,7 +1118,9 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
         };
 
         let (_, remainder_var) = match numeric_type {
-            NumericType::Signed { bit_size } => self.signed_division_var(lhs, rhs, bit_size)?,
+            NumericType::Signed { bit_size } => {
+                self.signed_division_var(lhs, rhs, bit_size, predicate)?
+            }
             _ => self.euclidean_division_var(lhs, rhs, bit_size, predicate)?,
         };
         Ok(remainder_var)

compiler/noirc_evaluator/src/acir/mod.rs

@@ -762,7 +762,12 @@ impl<'a> Context<'a> {
                     None
                 };
 
-                self.acir_context.assert_neq_var(lhs, rhs, assert_payload)?;
+                self.acir_context.assert_neq_var(
+                    lhs,
+                    rhs,
+                    self.current_side_effects_enabled_var,
+                    assert_payload,
+                )?;
             }
             Instruction::Cast(value_id, _) => {
                 let acir_var = self.convert_numeric_value(*value_id, dfg)?;

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

@@ -423,7 +423,7 @@
             // These can fail.
             Constrain(..) | ConstrainNotEqual(..) | RangeCheck { .. } => true,
 
             // This should never be side-effectful
             MakeArray { .. } | Noop => false,
 
             // Some binary math can overflow or underflow
@@ -595,13 +595,17 @@
                 match binary.operator {
                     BinaryOp::Add { unchecked: false }
                     | BinaryOp::Sub { unchecked: false }
-                    | BinaryOp::Mul { unchecked: false }
-                    | BinaryOp::Div
-                    | BinaryOp::Mod => {
+                    | BinaryOp::Mul { unchecked: false } => {
                         // Some binary math can overflow or underflow, but this is only the case
                         // for unsigned types (here we assume the type of binary.lhs is the same)
                         dfg.type_of_value(binary.rhs).is_unsigned()
                     }
+                    BinaryOp::Div | BinaryOp::Mod => {
+                        // Div and Mod require a predicate if the RHS may be zero.
+                        dfg.get_numeric_constant(binary.rhs)
+                            .map(|rhs| !rhs.is_zero())
+                            .unwrap_or(true)
+                    }
                     BinaryOp::Add { unchecked: true }
                     | BinaryOp::Sub { unchecked: true }
                     | BinaryOp::Mul { unchecked: true }

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

@@ -1724,4 +1724,65 @@ mod test {
         let ssa = ssa.purity_analysis().fold_constants_using_constraints();
         assert_normalized_ssa_equals(ssa, expected);
     }
+
+    #[test]
+    fn does_not_deduplicate_field_divisions_under_different_predicates() {
+        // Regression test for https://github.com/noir-lang/noir/issues/7283
+        let src = "
+        acir(inline) fn main f0 {
+          b0(v0: Field, v1: Field, v2: u1):
+            enable_side_effects v2
+            v3 = div v1, v0
+            v4 = mul v3, v0
+            v5 = not v2
+            enable_side_effects v5
+            v6 = div v1, v0
+            return
+        }
+        ";
+
+        let ssa = Ssa::from_str(src).unwrap();
+        let ssa = ssa.fold_constants();
+        assert_normalized_ssa_equals(ssa, src);
+    }
+
+    #[test]
+    fn does_not_deduplicate_unsigned_divisions_under_different_predicates() {
+        // Regression test for https://github.com/noir-lang/noir/issues/7283
+        let src = "
+        acir(inline) fn main f0 {
+          b0(v0: u32, v1: u32, v2: u1):
+            enable_side_effects v2
+            v3 = div v1, v0
+            v4 = not v2
+            enable_side_effects v4
+            v5 = div v1, v0
+            return
+        }
+        ";
+
+        let ssa = Ssa::from_str(src).unwrap();
+        let ssa = ssa.fold_constants();
+        assert_normalized_ssa_equals(ssa, src);
+    }
+
+    #[test]
+    fn does_not_deduplicate_signed_divisions_under_different_predicates() {
+        // Regression test for https://github.com/noir-lang/noir/issues/7283
+        let src = "
+        acir(inline) fn main f0 {
+          b0(v0: i32, v1: i32, v2: u1):
+            enable_side_effects v2
+            v3 = div v1, v0
+            v4 = not v2
+            enable_side_effects v4
+            v5 = div v1, v0
+            return
+        }
+        ";
+
+        let ssa = Ssa::from_str(src).unwrap();
+        let ssa = ssa.fold_constants();
+        assert_normalized_ssa_equals(ssa, src);
+    }
 }

test_programs/execution_success/signed_inactive_division_by_zero/Nargo.toml

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

test_programs/execution_success/signed_inactive_division_by_zero/Prover.toml

@@ -0,0 +1,3 @@
+a = "1"
+b = "0"
+condition = false

test_programs/execution_success/signed_inactive_division_by_zero/src/main.nr

@@ -0,0 +1,8 @@
+fn main(a: i32, b: i32, condition: bool) -> pub i32 {
+    if condition {
+        // If `condition` is not set then we should not trigger an assertion failure here.
+        a / b
+    } else {
+        0
+    }
+}