From dace07849aa28795abb30b3f9d979ffc6b6487e6 Mon Sep 17 00:00:00 2001
From: guipublic <47281315+guipublic@users.noreply.github.com>
Date: Thu, 28 Nov 2024 18:05:06 +0100
Subject: [PATCH] fix: used signed division for signed modulo (#6635)

---
 .../noirc_evaluator/src/acir/acir_variable.rs   | 17 ++++++++++++++---
 compiler/noirc_evaluator/src/acir/mod.rs        |  1 +
 docs/docs/noir/concepts/data_types/integers.md  | 11 +++++++++++
 .../execution_success/regression/Prover.toml    |  2 ++
 .../execution_success/regression/src/main.nr    | 10 +++++++++-
 5 files changed, 37 insertions(+), 4 deletions(-)

diff --git a/compiler/noirc_evaluator/src/acir/acir_variable.rs b/compiler/noirc_evaluator/src/acir/acir_variable.rs
index 6ba072f01a4..a42426e6c04 100644
--- a/compiler/noirc_evaluator/src/acir/acir_variable.rs
+++ b/compiler/noirc_evaluator/src/acir/acir_variable.rs
@@ -578,7 +578,7 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
         let numeric_type = match typ {
             AcirType::NumericType(numeric_type) => numeric_type,
             AcirType::Array(_, _) => {
-                todo!("cannot divide arrays. This should have been caught by the frontend")
+                unreachable!("cannot divide arrays. This should have been caught by the frontend")
             }
         };
         match numeric_type {
@@ -1084,11 +1084,22 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
         &mut self,
         lhs: AcirVar,
         rhs: AcirVar,
+        typ: AcirType,
         bit_size: u32,
         predicate: AcirVar,
     ) -> Result<AcirVar, RuntimeError> {
-        let (_, remainder) = self.euclidean_division_var(lhs, rhs, bit_size, predicate)?;
-        Ok(remainder)
+        let numeric_type = match typ {
+            AcirType::NumericType(numeric_type) => numeric_type,
+            AcirType::Array(_, _) => {
+                unreachable!("cannot modulo arrays. This should have been caught by the frontend")
+            }
+        };
+
+        let (_, remainder_var) = match numeric_type {
+            NumericType::Signed { bit_size } => self.signed_division_var(lhs, rhs, bit_size)?,
+            _ => self.euclidean_division_var(lhs, rhs, bit_size, predicate)?,
+        };
+        Ok(remainder_var)
     }
 
     /// Constrains the `AcirVar` variable to be of type `NumericType`.
diff --git a/compiler/noirc_evaluator/src/acir/mod.rs b/compiler/noirc_evaluator/src/acir/mod.rs
index 7274fe908d1..69679495b92 100644
--- a/compiler/noirc_evaluator/src/acir/mod.rs
+++ b/compiler/noirc_evaluator/src/acir/mod.rs
@@ -1968,6 +1968,7 @@ impl<'a> Context<'a> {
             BinaryOp::Mod => self.acir_context.modulo_var(
                 lhs,
                 rhs,
+                binary_type.clone(),
                 bit_count,
                 self.current_side_effects_enabled_var,
             ),
diff --git a/docs/docs/noir/concepts/data_types/integers.md b/docs/docs/noir/concepts/data_types/integers.md
index a1d59bf3166..f3badde62be 100644
--- a/docs/docs/noir/concepts/data_types/integers.md
+++ b/docs/docs/noir/concepts/data_types/integers.md
@@ -47,6 +47,17 @@ fn main() {
 
 The bit size determines the maximum and minimum range of value the integer type can store. For example, an `i8` variable can store a value in the range of -128 to 127 (i.e. $\\-2^{7}\\$ to $\\2^{7}-1\\$).
 
+
+```rust
+fn main(x: i16, y: i16) {
+    // modulo
+    let c = x % y;
+    let c = x % -13;
+}
+```
+
+Modulo operation is defined for negative integers thanks to integer division, so that the equality `x = (x/y)*y + (x%y)` holds.
+
 ## 128 bits Unsigned Integers
 
 The built-in structure `U128` allows you to use 128-bit unsigned integers almost like a native integer type. However, there are some differences to keep in mind:
diff --git a/test_programs/execution_success/regression/Prover.toml b/test_programs/execution_success/regression/Prover.toml
index 2875190982f..c81cbf10fbb 100644
--- a/test_programs/execution_success/regression/Prover.toml
+++ b/test_programs/execution_success/regression/Prover.toml
@@ -1,2 +1,4 @@
 x = [0x3f, 0x1c, 0xb8, 0x99, 0xab]
 z = 3
+u = "169"
+v = "-13"
\ No newline at end of file
diff --git a/test_programs/execution_success/regression/src/main.nr b/test_programs/execution_success/regression/src/main.nr
index 1c2f557d2cd..809fdbe4b28 100644
--- a/test_programs/execution_success/regression/src/main.nr
+++ b/test_programs/execution_success/regression/src/main.nr
@@ -94,7 +94,7 @@ fn bitshift_variable(idx: u8) -> u64 {
     bits
 }
 
-fn main(x: [u8; 5], z: Field) {
+fn main(x: [u8; 5], z: Field, u: i16, v: i16) {
     //Issue 1144
     let (nib, len) = compact_decode(x, z);
     assert(len == 5);
@@ -130,4 +130,12 @@ fn main(x: [u8; 5], z: Field) {
     assert(result_0 == 1);
     let result_4 = bitshift_variable(4);
     assert(result_4 == 16);
+
+    // Issue 6609
+    assert(u % -13 == 0);
+    assert(u % v == 0);
+    assert(u % -11 == 4);
+    assert(-u % -11 == -4);
+    assert(u % -11 == u % (v + 2));
+    assert(-u % -11 == -u % (v + 2));
 }