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

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

@@ -1257,58 +1257,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/ssa/opt/expand_signed_checks.rs

@@ -43,7 +43,8 @@
                 operator:
                     operator @ (BinaryOp::Add { unchecked: false }
                     | BinaryOp::Sub { unchecked: false }
-                    | BinaryOp::Mul { unchecked: false }),
+                    | BinaryOp::Mul { unchecked: false }
+                    | BinaryOp::Lt),
             }) = instruction
             else {
                 return;
@@ -68,6 +69,7 @@
                 BinaryOp::Add { .. } => expansion_context.insert_add(lhs, rhs),
                 BinaryOp::Sub { .. } => expansion_context.insert_sub(lhs, rhs),
                 BinaryOp::Mul { .. } => expansion_context.insert_mul(lhs, rhs),
+                BinaryOp::Lt => expansion_context.insert_lt(lhs, rhs),
                 _ => unreachable!("ICE: expand_signed_checks called on non-add/sub/mul"),
             };
 
@@ -136,6 +138,40 @@
         self.insert_cast(truncated, self.context.dfg.type_of_value(lhs).unwrap_numeric())
     }
 
+    fn insert_lt(&mut self, lhs: ValueId, rhs: ValueId) -> ValueId {
+        // First cast lhs and rhs to their unsigned equivalents
+        let bit_size = self.context.dfg.type_of_value(lhs).bit_size();
+        let unsigned_typ = NumericType::unsigned(bit_size);
+        let lhs_unsigned = self.insert_cast(lhs, unsigned_typ);
+        let rhs_unsigned = self.insert_cast(rhs, unsigned_typ);
+
+        // Check if lhs and rhs are positive or negative, respectively
+        let pow_last = self.numeric_constant(1_u128 << (bit_size - 1), unsigned_typ);
+        let lhs_is_positive = self.insert_binary(lhs_unsigned, BinaryOp::Div, pow_last);
+        let lhs_is_positive = self.insert_cast(lhs_is_positive, NumericType::bool());
+        let rhs_is_positive = self.insert_binary(rhs_unsigned, BinaryOp::Div, pow_last);
+        let rhs_is_positive = self.insert_cast(rhs_is_positive, NumericType::bool());
+
+        // Do rhs and lhs have a different sign?
+        let different_sign = self.insert_binary(lhs_is_positive, BinaryOp::Xor, rhs_is_positive);
+
+        // Check lhs < rhs using their unsigned equivalents
+        let unsigned_lt = self.insert_binary(lhs_unsigned, BinaryOp::Lt, rhs_unsigned);
+
+        // It can be shown that the result is given by xor'ing the two results above:
+        // - if lhs and rhs have the same sign (different_sign is 0):
+        //   - if both are positive then the unsigned comparison is correct, xoring it with 0 gives
+        //     same result
+        //   - if both are negative then the unsigned comparison is also correct, as, for example,
+        //     for i8, -128 i8 is Field 128 and -1 i8 is Field 255 and `-128 < -1` and `128 < 255`
+        // - if lhs and rhs have different signs (different_sign is 1):
+        //   - if lhs is positive and rhs is negative then, as fields, rhs will be greater, but
+        //     the result is the opposite (so xor'ing with 1 gives the correct result)
+        //   - if lhs is negative and rhs is positive then, as fields, lhs will be greater, but
+        //     the result is the opposite (so xor'ing with 1 gives the correct result)
+        self.insert_binary(different_sign, BinaryOp::Xor, unsigned_lt)
+    }
+
     /// Insert constraints ensuring that the operation does not overflow the bit size of the result
     /// We assume that:
     /// lhs and rhs are signed integers of bit size bit_size
@@ -626,4 +662,32 @@
         ";
         assert_ssa_does_not_change(src, Ssa::expand_signed_checks);
     }
+
+    #[test]
+    fn expands_signed_lt() {
+        let src = "
+        acir(inline) fn main f0 {
+          b0(v0: i8, v1: i8):
+            v2 = lt v0, v1
+            return v2
+        }
+        ";
+        let ssa = Ssa::from_str(src).unwrap();
+        let ssa = ssa.expand_signed_checks();
+        assert_ssa_snapshot!(ssa, @r"
+        acir(inline) fn main f0 {
+          b0(v0: i8, v1: i8):
+            v2 = cast v0 as u8
+            v3 = cast v1 as u8
+            v5 = div v2, u8 128
+            v6 = cast v5 as u1
+            v7 = div v3, u8 128
+            v8 = cast v7 as u1
+            v9 = xor v6, v8
+            v10 = lt v2, v3
+            v11 = xor v9, v10
+            return v11
+        }
+        ");
+    }
 }

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

@@ -252,10 +252,15 @@ impl Context<'_, '_, '_> {
             }
             NumericType::Signed { bit_size } => {
                 // Get the sign of the operand; positive signed operand will just do a division as well
-                let zero =
-                    self.numeric_constant(FieldElement::zero(), NumericType::signed(bit_size));
+                let unsigned_typ = NumericType::unsigned(bit_size);
+                let lhs_as_unsigned = self.insert_cast(lhs, unsigned_typ);
+
                 // The sign will be 0 for positive numbers and 1 for negatives, so it covers both cases.
-                let lhs_sign = self.insert_binary(lhs, BinaryOp::Lt, zero);
+                // To compute this we check if the value, as a Field, is greater or equal than the maximum
+                // value that is considered positive, that is, 2^(bit_size-1)-1: 2^(bit_size-1)-1 < lhs_as_field
+                let max_positive = (1_u128 << (bit_size - 1)) - 1;
+                let max_positive = self.numeric_constant(max_positive, unsigned_typ);
+                let lhs_sign = self.insert_binary(max_positive, BinaryOp::Lt, lhs_as_unsigned);
                 let lhs_sign_as_field = self.insert_cast(lhs_sign, NumericType::NativeField);
                 let lhs_as_field = self.insert_cast(lhs, NumericType::NativeField);
                 // For negative numbers, we prepare for the division using a wrapping addition of a + 1. Unchecked add as these are fields.
@@ -914,17 +919,18 @@ mod tests {
             assert_ssa_snapshot!(ssa, @r"
             acir(inline) fn main f0 {
               b0(v0: i32):
-                v2 = lt v0, i32 0
-                v3 = cast v2 as Field
-                v4 = cast v0 as Field
-                v5 = add v3, v4
-                v6 = truncate v5 to 32 bits, max_bit_size: 33
-                v7 = cast v6 as i32
-                v9 = div v7, i32 4
-                v10 = cast v2 as i32
-                v11 = unchecked_sub v9, v10
-                v12 = truncate v11 to 32 bits, max_bit_size: 33
-                return v12
+                v1 = cast v0 as u32
+                v3 = lt u32 2147483647, v1
+                v4 = cast v3 as Field
+                v5 = cast v0 as Field
+                v6 = add v4, v5
+                v7 = truncate v6 to 32 bits, max_bit_size: 33
+                v8 = cast v7 as i32
+                v10 = div v8, i32 4
+                v11 = cast v3 as i32
+                v12 = unchecked_sub v10, v11
+                v13 = truncate v12 to 32 bits, max_bit_size: 33
+                return v13
             }
             ");
         }
@@ -992,17 +998,18 @@ mod tests {
                 v55 = mul v54, v50
                 v56 = add v53, v55
                 v57 = cast v56 as i32
-                v59 = lt v0, i32 0
-                v60 = cast v59 as Field
-                v61 = cast v0 as Field
-                v62 = add v60, v61
-                v63 = truncate v62 to 32 bits, max_bit_size: 33
-                v64 = cast v63 as i32
-                v65 = div v64, v57
-                v66 = cast v59 as i32
-                v67 = unchecked_sub v65, v66
-                v68 = truncate v67 to 32 bits, max_bit_size: 33
-                return v68
+                v58 = cast v0 as u32
+                v60 = lt u32 2147483647, v58
+                v61 = cast v60 as Field
+                v62 = cast v0 as Field
+                v63 = add v61, v62
+                v64 = truncate v63 to 32 bits, max_bit_size: 33
+                v65 = cast v64 as i32
+                v66 = div v65, v57
+                v67 = cast v60 as i32
+                v68 = unchecked_sub v66, v67
+                v69 = truncate v68 to 32 bits, max_bit_size: 33
+                return v69
             }
             "#);
         }