feat: add signed division

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,56 @@ impl GeneratedAcir {
         Ok(limb_witnesses)
     }
 
+    pub(crate) fn signed_division(
+        &mut self,
+        lhs: &Expression,
+        rhs: &Expression,
+        max_bit_size: u32,
+    ) -> Result<(Expression, Expression), AcirGenError> {
+        // maximum power of two for the bit size
+        let max_power_of_two =
+            FieldElement::from(2_i128).pow(&FieldElement::from(max_bit_size as i128 - 1));
+
+        //rhs / max_power_of_two
+        let (rhs_leading, rhs_mantissa) = self.euclidean_division(
+            rhs,
+            &max_power_of_two.into(),
+            max_bit_size,
+            &Expression::one(),
+        )?;
+
+        //lhs / max_power_of_two
+        let (lhs_leading, lhs_mantissa) = self.euclidean_division(
+            lhs,
+            &max_power_of_two.into(),
+            max_bit_size,
+            &Expression::one(),
+        )?;
+
+        // signed to unsigned
+        let l_inter = &Expression::from(lhs_leading) * &Expression::from(lhs_mantissa);
+        let r_inter = &Expression::from(rhs_leading) * &Expression::from(rhs_mantissa);
+        let unsigned_l = lhs.add_mul(FieldElement::from(2_i128), &l_inter);
+        let unsigned_r = rhs.add_mul(FieldElement::from(2_i128), &r_inter);
+        let unsigned_l_witness = self.get_or_create_witness(&unsigned_l);
+        let unsigned_r_witness = self.get_or_create_witness(&unsigned_r);
+
+        let (q1, r1) = self.euclidean_division(
+            &unsigned_l_witness.into(),
+            &unsigned_r_witness.into(),
+            max_bit_size - 1,
+            &Expression::one(),
+        )?;
+
+        // unsigned to signed
+        let q1_inter = &(&Expression::from_field(max_power_of_two) - &Expression::from(q1))
+            * &rhs_leading.into();
+        let quotient = Expression::from(q1).add_mul(FieldElement::from(2_i128), &q1_inter);
+        let r1_inter = &(&Expression::from_field(max_power_of_two) - &Expression::from(r1))
+            * &lhs_leading.into();
+        let remainder = Expression::from(r1).add_mul(FieldElement::from(2_i128), &r1_inter);
+        Ok((quotient, remainder))
+    }
     /// Computes lhs/rhs by using euclidean division.
     ///
     /// Returns `q` for quotient and `r` for remainder such