chore(ACIR): expand signed lt, div and mod in SSA

compiler/noirc_evaluator/src/acir/acir_context/mod.rs

@@ -597,10 +597,8 @@ impl<F: AcirField> AcirContext<F> {
                     self.euclidean_division_var(lhs, rhs, bit_size, predicate)?;
                 Ok(quotient_var)
             }
-            NumericType::Signed { bit_size } => {
-                let (quotient_var, _remainder_var) =
-                    self.signed_division_var(lhs, rhs, bit_size, predicate)?;
-                Ok(quotient_var)
+            NumericType::Signed { .. } => {
+                unreachable!("Signed division should have been removed before ACIRgen")
             }
         }
     }
@@ -1083,96 +1081,6 @@ impl<F: AcirField> AcirContext<F> {
         Ok(())
     }
 
-    // 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: AcirVar,
-        leading: AcirVar,
-        max_bit_size: u32,
-    ) -> Result<AcirVar, RuntimeError> {
-        let max_power_of_two = self.add_constant(power_of_two::<F>(max_bit_size - 1));
-
-        let intermediate = self.sub_var(max_power_of_two, lhs)?;
-        let intermediate = self.mul_var(intermediate, leading)?;
-
-        self.add_mul_var(lhs, F::from(2_u128), intermediate)
-    }
-
-    /// 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 euclidean division, where we have instead remainder < |rhs|
-    fn signed_division_var(
-        &mut self,
-        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!
-        // 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.
-
-        assert_ne!(bit_size, 0, "signed integer should have at least one bit");
-
-        // 2^{max_bit size-1}
-        let max_power_of_two = self.add_constant(power_of_two::<F>(bit_size - 1));
-        let zero = self.add_constant(F::zero());
-        let one = self.add_constant(F::one());
-
-        // Get the sign bit of rhs by computing rhs / max_power_of_two
-        let (rhs_leading, _) = self.euclidean_division_var(rhs, max_power_of_two, bit_size, one)?;
-
-        // Get the sign bit of lhs by computing lhs / max_power_of_two
-        let (lhs_leading, _) = self.euclidean_division_var(lhs, max_power_of_two, bit_size, one)?;
-
-        // Signed to unsigned:
-        let unsigned_lhs = self.two_complement(lhs, lhs_leading, bit_size)?;
-        let unsigned_rhs = self.two_complement(rhs, rhs_leading, bit_size)?;
-
-        // Performs the division using the unsigned values of lhs and rhs
-        let (q1, r1) =
-            self.euclidean_division_var(unsigned_lhs, unsigned_rhs, bit_size, 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
-        let q_sign = self.xor_var(lhs_leading, rhs_leading, AcirType::unsigned(1))?;
-        let quotient = self.two_complement(q1, q_sign, bit_size)?;
-        let remainder = self.two_complement(r1, lhs_leading, bit_size)?;
-
-        // Issue #5129 - When q1 is zero and quotient sign is -1, we compute -0=2^{bit_size},
-        // which is not valid because we do not wrap integer operations
-        // Similar case can happen with the remainder.
-        let q_is_0 = self.eq_var(q1, zero)?;
-        let q_is_not_0 = self.not_var(q_is_0, AcirType::unsigned(1))?;
-        let quotient = self.mul_var(quotient, q_is_not_0)?;
-        let r_is_0 = self.eq_var(r1, zero)?;
-        let r_is_not_0 = self.not_var(r_is_0, AcirType::unsigned(1))?;
-        let remainder = self.mul_var(remainder, r_is_not_0)?;
-
-        // The quotient must be a valid signed integer.
-        // For instance -128/-1 = 128, but 128 is not a valid i8
-        // Because it is the only possible overflow that can happen due to signed representation,
-        // we simply check for this case: quotient is negative, or distinct from 2^{bit_size-1}
-        // Indeed, negative quotient cannot 'overflow' because the division will not increase its absolute value
-        let assert_message =
-            self.generate_assertion_message_payload("Attempt to divide with overflow".to_string());
-        let unsigned = self.not_var(q_sign, AcirType::unsigned(1))?;
-
-        // This overflow check must also be under the predicate
-        let unsigned = self.mul_var(unsigned, predicate)?;
-
-        self.assert_neq_var(quotient, max_power_of_two, unsigned, Some(assert_message))?;
-
-        Ok((quotient, remainder))
-    }
-
     /// Returns a variable which is constrained to be `lhs mod rhs`
     pub(crate) fn modulo_var(
         &mut self,
@@ -1190,8 +1098,8 @@ impl<F: AcirField> AcirContext<F> {
         };
 
         let (_, remainder_var) = match numeric_type {
-            NumericType::Signed { bit_size } => {
-                self.signed_division_var(lhs, rhs, bit_size, predicate)?
+            NumericType::Signed { .. } => {
+                unreachable!("Signed modulo should have been removed before ACIRgen")
             }
             _ => self.euclidean_division_var(lhs, rhs, bit_size, predicate)?,
         };
@@ -1257,58 +1165,6 @@ impl<F: AcirField> AcirContext<F> {
         Ok(remainder)
     }
 
-    /// Returns an 'AcirVar' containing the boolean value lhs<rhs, assuming lhs and rhs are signed integers of size bit_count.
-    /// Like in the unsigned case, we compute the difference diff = lhs-rhs+2^n (and we avoid underflow)
-    /// The result depends on the diff and the signs of the inputs:
-    /// If same sign, lhs<rhs <=> diff<2^n, because the 2-complement representation keeps the ordering (e.g in 8 bits -1 is 255 > -2 = 254)
-    /// If not, lhs positive => diff > 2^n
-    /// and lhs negative => diff <= 2^n => diff < 2^n (because signs are not the same, so lhs != rhs and so diff != 2^n)
-    pub(crate) fn less_than_signed(
-        &mut self,
-        lhs: AcirVar,
-        rhs: AcirVar,
-        bit_count: u32,
-    ) -> Result<AcirVar, RuntimeError> {
-        let pow_last = self.add_constant(F::from(1_u128 << (bit_count - 1)));
-        let pow = self.add_constant(F::from(1_u128 << (bit_count)));
-
-        // We check whether the inputs have same sign or not by computing the XOR of their bit sign
-
-        // Predicate is always active as `pow_last` is known to be non-zero.
-        let one = self.add_constant(1_u128);
-        let lhs_sign = self.div_var(
-            lhs,
-            pow_last,
-            AcirType::NumericType(NumericType::Unsigned { bit_size: bit_count }),
-            one,
-        )?;
-        let rhs_sign = self.div_var(
-            rhs,
-            pow_last,
-            AcirType::NumericType(NumericType::Unsigned { bit_size: bit_count }),
-            one,
-        )?;
-        let same_sign = self.xor_var(
-            lhs_sign,
-            rhs_sign,
-            AcirType::NumericType(NumericType::Unsigned { bit_size: 1 }),
-        )?;
-
-        // We compute the input difference
-        let no_underflow = self.add_var(lhs, pow)?;
-        let diff = self.sub_var(no_underflow, rhs)?;
-
-        // We check the 'bit sign' of the difference
-        let diff_sign = self.less_than_var(diff, pow, bit_count + 1)?;
-
-        // Then the result is simply diff_sign XOR same_sign (can be checked with a truth table)
-        self.xor_var(
-            diff_sign,
-            same_sign,
-            AcirType::NumericType(NumericType::Unsigned { bit_size: 1 }),
-        )
-    }
-
     /// Returns an `AcirVar` which will be `1` if lhs >= rhs
     /// and `0` otherwise.
     pub(crate) fn more_than_eq_var(

compiler/noirc_evaluator/src/acir/mod.rs

@@ -763,7 +763,7 @@ impl<'a> Context<'a> {
             BinaryOp::Eq => self.acir_context.eq_var(lhs, rhs),
             BinaryOp::Lt => match binary_type {
                 AcirType::NumericType(NumericType::Signed { .. }) => {
-                    self.acir_context.less_than_signed(lhs, rhs, bit_count)
+                    panic!("ICE - signed less than should have been removed before ACIRgen")
                 }
                 _ => self.acir_context.less_than_var(lhs, rhs, bit_count),
             },

compiler/noirc_evaluator/src/acir/tests/mod.rs

@@ -243,33 +243,6 @@ fn derive_pedersen_generators_requires_constant_input() {
         .expect_err("Should fail with assert constant");
 }
 
-#[test]
-// Regression for https://github.com/noir-lang/noir/issues/9847
-fn signed_div_overflow() {
-    // Test that check -128 / -1 overflow for i8
-    let src = r#"
-        acir(inline) predicate_pure fn main f0 {
-          b0(v1: i8, v2: i8):
-            v3 = div v1, v2
-            return
-        }
-        "#;
-
-    let ssa = Ssa::from_str(src).unwrap();
-    let inputs = vec![FieldElement::from(128_u128), FieldElement::from(255_u128)];
-    let inputs = inputs
-        .into_iter()
-        .enumerate()
-        .map(|(i, f)| (Witness(i as u32), f))
-        .collect::<BTreeMap<_, _>>();
-    let initial_witness = WitnessMap::from(inputs);
-    let output = None;
-
-    // acir execution should fail to divide -128 / -1
-    let acir_execution_result = execute_ssa(ssa, initial_witness.clone(), output.as_ref());
-    assert!(matches!(acir_execution_result, (ACVMStatus::Failure(_), _)));
-}
-
 /// Convert the SSA input into ACIR and use ACVM to execute it
 /// Returns the ACVM execution status and the value of the 'output' witness value,
 /// unless the provided output is None or the ACVM fails during execution.

compiler/noirc_evaluator/src/ssa/mod.rs

@@ -174,6 +174,9 @@ pub fn primary_passes(options: &SsaEvaluatorOptions) -> Vec<SsaPass<'_>> {
         SsaPass::new(Ssa::simplify_cfg, "Simplifying"),
         SsaPass::new(Ssa::mem2reg, "Mem2Reg"),
         SsaPass::new(Ssa::remove_bit_shifts, "Removing Bit Shifts"),
+        // Expand signed lt/div/mod after "Removing Bit Shifts" because that pass might
+        // introduce signed divisions.
+        SsaPass::new(Ssa::expand_signed_math, "Expand signed math"),
         SsaPass::new(Ssa::simplify_cfg, "Simplifying"),
         SsaPass::new(Ssa::flatten_cfg, "Flattening"),
         // Run mem2reg once more with the flattened CFG to catch any remaining loads/stores

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

@@ -1,3 +1,9 @@
+/// An SSA pass that transforms the checked signed arithmetic operations add, sub and mul
+/// into unchecked operations followed by explicit overflow checks.
+///
+/// The purpose of this pass is to avoid ACIR and Brillig having to handle checked signed arithmetic
+/// operations, while also allowing further optimizations to be done during subsequent
+/// SSA passes on the expanded instructions.
 use acvm::{FieldElement, acir::AcirField};
 
 use crate::ssa::{
@@ -29,7 +35,7 @@ impl Function {
     /// The structure of this pass is simple:
     /// Go through each block and re-insert all instructions, decomposing any checked signed arithmetic to have explicit
     /// overflow checks.
-    pub(crate) fn expand_signed_checks(&mut self) {
+    fn expand_signed_checks(&mut self) {
         // TODO: consider whether we can implement this more efficiently in brillig.
 
         self.simple_optimization(|context| {