fix!: Integer division is not the inverse of integer multiplication

compiler/noirc_frontend/src/hir_def/types.rs

@@ -1761,7 +1761,7 @@
                         Err(UnificationError)
                     }
                 } else if let InfixExpr(lhs, op, rhs) = other {
-                    if let Some(inverse) = op.inverse() {
+                    if let Some(inverse) = op.approx_inverse() {
                         // Handle cases like `4 = a + b` by trying to solve to `a = 4 - b`
                         let new_type = InfixExpr(
                             Box::new(Constant(*value, kind.clone())),
@@ -2122,7 +2122,7 @@
         }
 
         let recur_on_binding = |id, replacement: &Type| {
             // Prevent recuring forever if there's a `T := T` binding
             if replacement.type_variable_id() == Some(id) {
                 replacement.clone()
             } else {
@@ -2202,7 +2202,7 @@
                 Type::Tuple(fields)
             }
             Type::Forall(typevars, typ) => {
                 // Trying to substitute_helper a variable de, substitute_bound_typevarsfined within a nested Forall
                 // is usually impossible and indicative of an error in the type checker somewhere.
                 for var in typevars {
                     assert!(!type_bindings.contains_key(&var.id()));
@@ -2368,7 +2368,7 @@
 
     /// Replace any `Type::NamedGeneric` in this type with a `Type::TypeVariable`
     /// using to the same inner `TypeVariable`. This is used during monomorphization
     /// to bind to named generics since they are unbindable during type checking.
     pub fn replace_named_generics_with_type_variables(&mut self) {
         match self {
             Type::FieldElement
@@ -2569,6 +2569,17 @@
 
     /// Return the operator that will "undo" this operation if applied to the rhs
     fn inverse(self) -> Option<BinaryTypeOperator> {
+        match self {
+            BinaryTypeOperator::Addition => Some(BinaryTypeOperator::Subtraction),
+            BinaryTypeOperator::Subtraction => Some(BinaryTypeOperator::Addition),
+            BinaryTypeOperator::Multiplication => None,
+            BinaryTypeOperator::Division => None,
+            BinaryTypeOperator::Modulo => None,
+        }
+    }
+
+    /// Return the operator that will "undo" this operation if applied to the rhs
+    fn approx_inverse(self) -> Option<BinaryTypeOperator> {
         match self {
             BinaryTypeOperator::Addition => Some(BinaryTypeOperator::Subtraction),
             BinaryTypeOperator::Subtraction => Some(BinaryTypeOperator::Addition),
@@ -2796,7 +2807,7 @@
                 len.hash(state);
                 env.hash(state);
             }
             Type::Tuple(elems) => elems.hash(state),
             Type::Struct(def, args) => {
                 def.hash(state);
                 args.hash(state);
@@ -2897,7 +2908,7 @@
             // Special case: we consider unbound named generics and type variables to be equal to each
             // other if their type variable ids match. This is important for some corner cases in
             // monomorphization where we call `replace_named_generics_with_type_variables` but
             // still want them to be equal for canonicalization checks in arithmetic generics.
             // Without this we'd fail the `serialize` test.
             (
                 NamedGeneric(lhs_var, _) | TypeVariable(lhs_var),

compiler/noirc_frontend/src/hir_def/types/arithmetic.rs

@@ -120,7 +120,7 @@ impl Type {
     /// Precondition: `lhs & rhs are in canonical form`
     ///
     /// - Simplifies `(N +/- M) -/+ M` to `N`
-    /// - Simplifies `(N */÷ M) ÷/* M` to `N`
+    /// - Simplifies `(N * M) ÷ M` to `N`
     fn try_simplify_non_constants_in_lhs(
         lhs: &Type,
         op: BinaryTypeOperator,
@@ -132,7 +132,10 @@ impl Type {
 
         // Note that this is exact, syntactic equality, not unification.
         // `rhs` is expected to already be in canonical form.
-        if l_op.inverse() != Some(op) || l_rhs.canonicalize() != *rhs {
+        if l_op.approx_inverse() != Some(op)
+            || l_op == BinaryTypeOperator::Division
+            || l_rhs.canonicalize() != *rhs
+        {
             return None;
         }
 
@@ -199,7 +202,8 @@ impl Type {
     /// Precondition: `lhs & rhs are in canonical form`
     ///
     /// - Simplifies `(N +/- C1) +/- C2` to `N +/- (C1 +/- C2)` if C1 and C2 are constants.
-    /// - Simplifies `(N */÷ C1) */÷ C2` to `N */÷ (C1 */÷ C2)` if C1 and C2 are constants.
+    /// - Simplifies `(N * C1) ÷ C2` to `N * (C1 ÷ C2)` if C1 and C2 are constants which divide
+    ///   without a remainder.
     fn try_simplify_partial_constants(
         lhs: &Type,
         mut op: BinaryTypeOperator,
@@ -218,12 +222,8 @@ impl Type {
                 let constant = Type::Constant(result, lhs.infix_kind(rhs));
                 Some(Type::InfixExpr(l_type, l_op, Box::new(constant)))
             }
-            (Multiplication | Division, Multiplication | Division) => {
-                // If l_op is a division we want to inverse the rhs operator.
-                if l_op == Division {
-                    op = op.inverse()?;
-                }
-
+            (Multiplication, Division) => {
+                // We need to ensure the result divides evenly to preserve integer division semantics
                 let divides_evenly = !lhs.infix_kind(rhs).is_type_level_field_element()
                     && l_const.to_i128().checked_rem(r_const.to_i128()) == Some(0);
 
@@ -248,7 +248,7 @@ impl Type {
         bindings: &mut TypeBindings,
     ) -> Result<(), UnificationError> {
         if let Type::InfixExpr(lhs_a, op_a, rhs_a) = self {
-            if let Some(inverse) = op_a.inverse() {
+            if let Some(inverse) = op_a.approx_inverse() {
                 let kind = lhs_a.infix_kind(rhs_a);
                 if let Some(rhs_a_value) = rhs_a.evaluate_to_field_element(&kind) {
                     let rhs_a = Box::new(Type::Constant(rhs_a_value, kind));
@@ -264,7 +264,7 @@ impl Type {
         }
 
         if let Type::InfixExpr(lhs_b, op_b, rhs_b) = other {
-            if let Some(inverse) = op_b.inverse() {
+            if let Some(inverse) = op_b.approx_inverse() {
                 let kind = lhs_b.infix_kind(rhs_b);
                 if let Some(rhs_b_value) = rhs_b.evaluate_to_field_element(&kind) {
                     let rhs_b = Box::new(Type::Constant(rhs_b_value, kind));

compiler/noirc_frontend/src/tests.rs

@@ -3357,3 +3357,34 @@ fn error_if_attribute_not_in_scope() {
         CompilationError::ResolverError(ResolverError::AttributeFunctionNotInScope { .. })
     ));
 }
+
+#[test]
+fn arithmetic_generics_rounding_pass() {
+    let src = r#"
+        fn main() {
+            // 3/2*2 = 2
+            round::<3, 2>([1, 2]);
+        }
+
+        fn round<let N: u32, let M: u32>(_x: [Field; N / M * M]) {}
+    "#;
+
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 0);
+}
+
+#[test]
+fn arithmetic_generics_rounding_fail() {
+    let src = r#"
+        fn main() {
+            // Do not simplify N/M*M to just N
+            // This should be 3/2*2 = 2, not 3
+            round::<3, 2>([1, 2, 3]);
+        }
+
+        fn round<let N: u32, let M: u32>(_x: [Field; N / M * M]) {}
+    "#;
+
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 1);
+}

test_programs/compile_success_empty/arithmetic_generics/src/main.nr

@@ -117,9 +117,12 @@ fn test_constant_folding<let N: u32>() {
 
     // N * C1 / C2 = N * (C1 / C2)
     let _: W<N * 10 / 2> = W::<N * 5> {};
-
+    // This case is invalid due to integer division
+    // If N does not divide evenly with 10 then we cannot simplify it.
+    // e.g. 15 / 10 * 2 = 2 versus 15 / 5 = 3
+    //
     // N / C1 * C2 = N / (C1 / C2)
-    let _: W<N / 10 * 2> = W::<N / 5> {};
+    // let _: W<N / 10 * 2> = W::<N / 5> {};
 }
 
 fn test_non_constant_folding<let N: u32, let M: u32>() {
@@ -131,7 +134,9 @@ fn test_non_constant_folding<let N: u32, let M: u32>() {
 
     // N * M / M = N
     let _: W<N * M / M> = W::<N> {};
-
+    // This case is not true due to integer division rounding!
+    // Consider 5 / 2 * 2 which should equal 4, not 5
+    //
     // N / M * M = N
-    let _: W<N / M * M> = W::<N> {};
+    // let _: W<N / M * M> = W::<N> {};
 }