feat: add signed division

crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Nargo.toml

@@ -0,0 +1,5 @@
+[package]
+authors = [""]
+compiler_version = "0.1"
+
+[dependencies]

crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Prover.toml

@@ -0,0 +1,3 @@
+x = "7"
+y = "3"
+z = "2"

crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/src/main.nr

@@ -0,0 +1,28 @@
+use dep::std;
+
+// Testing signed integer division: 
+//  7/3  = 2
+// -7/3  = -2
+// -7/-3 = 2
+//  7/-3 = -2
+fn main(mut x: i32, mut y: i32, mut z: i32) {
+    // 7/3 = 2
+    assert(x / y == z);
+
+    // -7/3 = -2
+    x = 0-x;
+    z = 0-z;
+    assert(x+7==0);
+    assert(z+2==0);
+    assert(x / y == z);
+
+    // -7/-3 = 2
+    y = 0 - y;
+    z = 0-z;
+    assert(x / y == z);
+
+    // 7/-3 = -2
+    x = 0 - x;
+    z = 0-z;
+    assert(x / y == z);
+}

crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs

@@ -298,8 +298,10 @@ impl AcirContext {
                     self.euclidean_division_var(lhs, rhs, bit_size)?;
                 Ok(quotient_var)
             }
-            NumericType::Signed { .. } => {
-                todo!("Signed division");
+            NumericType::Signed { bit_size } => {
+                let (quotient_var, _remainder_var) =
+                    self.signed_division_var(lhs, rhs, bit_size)?;
+                Ok(quotient_var)
             }
         }
     }
@@ -431,6 +433,37 @@ impl AcirContext {
         Ok((quotient_var, remainder_var))
     }
 
+    /// Returns the quotient and remainder such that lhs = rhs * quotient + remainder
+    /// and |remainder| < |rhs|
+    /// and remainder has the same sign than lhs
+    /// Note that this is not the euclidian division, where we have instead remainder < |rhs|
+    ///
+    ///
+    ///
+    ///
+
+    fn signed_division_var(
+        &mut self,
+        lhs: AcirVar,
+        rhs: AcirVar,
+        bit_size: u32,
+    ) -> Result<(AcirVar, AcirVar), AcirGenError> {
+        let lhs_data = &self.vars[&lhs].clone();
+        let rhs_data = &self.vars[&rhs].clone();
+
+        let lhs_expr = lhs_data.to_expression();
+        let rhs_expr = rhs_data.to_expression();
+        let l_witness = self.acir_ir.get_or_create_witness(&lhs_expr);
+        let r_witness = self.acir_ir.get_or_create_witness(&rhs_expr);
+        assert_ne!(bit_size, 0);
+        let (q, r) =
+            self.acir_ir.signed_division(&l_witness.into(), &r_witness.into(), bit_size)?;
+
+        let q_vd = AcirVarData::Expr(q);
+        let r_vd = AcirVarData::Expr(r);
+        Ok((self.add_data(q_vd), self.add_data(r_vd)))
+    }
+
     /// Returns a variable which is constrained to be `lhs mod rhs`
     pub(crate) fn modulo_var(
         &mut self,
@@ -493,8 +526,7 @@ impl AcirContext {
     ) -> Result<AcirVar, AcirGenError> {
         let data = &self.vars[&variable];
         match numeric_type {
-            NumericType::Signed { .. } => todo!("signed integer constraining is unimplemented"),
-            NumericType::Unsigned { bit_size } => {
+            NumericType::Signed { bit_size } | NumericType::Unsigned { bit_size } => {
                 let data_expr = data.to_expression();
                 let witness = self.acir_ir.get_or_create_witness(&data_expr);
                 self.acir_ir.range_constraint(witness, *bit_size)?;
@@ -823,7 +855,7 @@ impl AcirContext {
         });
         // Enforce the outputs to be sorted
         for i in 0..(outputs_var.len() - 1) {
-            self.less_than_constrain(outputs_var[i], outputs_var[i + 1], bit_size)?;
+            self.less_than_constrain(outputs_var[i], outputs_var[i + 1], bit_size, None)?;
         }
         // Enforce the outputs to be a permutation of the inputs
         self.acir_ir.permutation(&inputs_expr, &output_expr);
@@ -837,8 +869,9 @@ impl AcirContext {
         lhs: AcirVar,
         rhs: AcirVar,
         bit_size: u32,
+        predicate: Option<AcirVar>,
     ) -> Result<(), AcirGenError> {
-        let lhs_less_than_rhs = self.more_than_eq_var(rhs, lhs, bit_size, None)?;
+        let lhs_less_than_rhs = self.more_than_eq_var(rhs, lhs, bit_size, predicate)?;
         self.assert_eq_one(lhs_less_than_rhs)
     }
 }

crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs

@@ -307,6 +307,81 @@ impl GeneratedAcir {
         Ok(limb_witnesses)
     }
 
+    // Returns the 2-complement of lhs, using the provided sign bit in 'leading'
+    // if leading is zero, it returns lhs
+    // if leading is one, it returns 2^bit_size-lhs
+    fn two_complement(
+        &mut self,
+        lhs: &Expression,
+        leading: Witness,
+        max_bit_size: u32,
+    ) -> Expression {
+        let max_power_of_two =
+            FieldElement::from(2_i128).pow(&FieldElement::from(max_bit_size as i128 - 1));
+        let inter = &(&Expression::from_field(max_power_of_two) - lhs) * &leading.into();
+        lhs.add_mul(FieldElement::from(2_i128), &inter)
+    }
+
+    /// Signed division lhs /  rhs
+    /// We derive the signed division from the unsigned euclidian division.
+    /// note that this is not euclidian division!
+    // if x is a signed integer, then sign(x)x >= 0
+    // so if a and b are signed integers, we can do the unsigned division:
+    // sign(a)a = q1*sign(b)b + r1
+    // => a = sign(a)sign(b)q1*b + sign(a)r1
+    // => a = qb+r, with |r|<|b| and a and r have the same sign.
+    pub(crate) fn signed_division(
+        &mut self,
+        lhs: &Expression,
+        rhs: &Expression,
+        max_bit_size: u32,
+    ) -> Result<(Expression, Expression), AcirGenError> {
+        // 2^{max_bit size-1}
+        let max_power_of_two =
+            FieldElement::from(2_i128).pow(&FieldElement::from(max_bit_size as i128 - 1));
+
+        // Get the sign bit of rhs by computing rhs / max_power_of_two
+        let (rhs_leading, _) = self.euclidean_division(
+            rhs,
+            &max_power_of_two.into(),
+            max_bit_size,
+            &Expression::one(),
+        )?;
+
+        // Get the sign bit of lhs by computing lhs / max_power_of_two
+        let (lhs_leading, _) = self.euclidean_division(
+            lhs,
+            &max_power_of_two.into(),
+            max_bit_size,
+            &Expression::one(),
+        )?;
+
+        // Signed to unsigned:
+        let unsigned_lhs = self.two_complement(lhs, lhs_leading, max_bit_size);
+        let unsigned_rhs = self.two_complement(rhs, rhs_leading, max_bit_size);
+        let unsigned_l_witness = self.get_or_create_witness(&unsigned_lhs);
+        let unsigned_r_witness = self.get_or_create_witness(&unsigned_rhs);
+
+        // Performs the division using the unsigned values of lhs and rhs
+        let (q1, r1) = self.euclidean_division(
+            &unsigned_l_witness.into(),
+            &unsigned_r_witness.into(),
+            max_bit_size - 1,
+            &Expression::one(),
+        )?;
+
+        // 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
+        let q_sign = (&Expression::from(lhs_leading) + &Expression::from(rhs_leading)).add_mul(
+            -FieldElement::from(2_i128),
+            &(&Expression::from(lhs_leading) * &Expression::from(rhs_leading)),
+        );
+        let q_sign_witness = self.get_or_create_witness(&q_sign);
+        let quotient = self.two_complement(&q1.into(), q_sign_witness, max_bit_size);
+        let remainder = self.two_complement(&r1.into(), lhs_leading, max_bit_size);
+        Ok((quotient, remainder))
+    }
+
     /// Computes lhs/rhs by using euclidean division.
     ///
     /// Returns `q` for quotient and `r` for remainder such