feat: Add overflow and underflow checks for unsigned integers in bril…

…lig (#4445)

# Description

## Problem\*

When overflow checks were added they were only added for ACIR. This adds
add, sub and multiply overflow checks for unsigned operations in
brillig.

## Summary\*



## Additional Context



## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[Exceptional Case]** Documentation to be submitted in a separate
PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.

compiler/noirc_evaluator/src/brillig/brillig_gen/brillig_block.rs

@@ -1,9 +1,7 @@
 use crate::brillig::brillig_ir::brillig_variable::{
     type_to_heap_value_type, BrilligArray, BrilligVariable, BrilligVector, SingleAddrVariable,
 };
-use crate::brillig::brillig_ir::{
-    BrilligBinaryOp, BrilligContext, BRILLIG_INTEGER_ARITHMETIC_BIT_SIZE,
-};
+use crate::brillig::brillig_ir::{BrilligBinaryOp, BrilligContext};
 use crate::ssa::ir::dfg::CallStack;
 use crate::ssa::ir::instruction::ConstrainError;
 use crate::ssa::ir::{
@@ -1197,7 +1195,7 @@ impl<'block> BrilligBlock<'block> {
         let left = self.convert_ssa_single_addr_value(binary.lhs, dfg);
         let right = self.convert_ssa_single_addr_value(binary.rhs, dfg);
 
-        let brillig_binary_op =
+        let (brillig_binary_op, is_signed) =
             convert_ssa_binary_op_to_brillig_binary_op(binary.operator, &binary_type);
 
         self.brillig_context.binary_instruction(
@@ -1206,6 +1204,93 @@ impl<'block> BrilligBlock<'block> {
             result_variable.address,
             brillig_binary_op,
         );
+
+        self.add_overflow_check(brillig_binary_op, left, right, result_variable, is_signed);
+    }
+
+    fn add_overflow_check(
+        &mut self,
+        binary_operation: BrilligBinaryOp,
+        left: SingleAddrVariable,
+        right: SingleAddrVariable,
+        result: SingleAddrVariable,
+        is_signed: bool,
+    ) {
+        let (op, bit_size) = if let BrilligBinaryOp::Integer { op, bit_size } = binary_operation {
+            (op, bit_size)
+        } else {
+            return;
+        };
+
+        match (op, is_signed) {
+            (BinaryIntOp::Add, false) => {
+                let condition = self.brillig_context.allocate_register();
+                // Check that lhs <= result
+                self.brillig_context.binary_instruction(
+                    left.address,
+                    result.address,
+                    condition,
+                    BrilligBinaryOp::Integer { op: BinaryIntOp::LessThanEquals, bit_size },
+                );
+                self.brillig_context.constrain_instruction(
+                    condition,
+                    Some("attempt to add with overflow".to_string()),
+                );
+                self.brillig_context.deallocate_register(condition);
+            }
+            (BinaryIntOp::Sub, false) => {
+                let condition = self.brillig_context.allocate_register();
+                // Check that rhs <= lhs
+                self.brillig_context.binary_instruction(
+                    right.address,
+                    left.address,
+                    condition,
+                    BrilligBinaryOp::Integer { op: BinaryIntOp::LessThanEquals, bit_size },
+                );
+                self.brillig_context.constrain_instruction(
+                    condition,
+                    Some("attempt to subtract with overflow".to_string()),
+                );
+                self.brillig_context.deallocate_register(condition);
+            }
+            (BinaryIntOp::Mul, false) => {
+                // Multiplication overflow is only possible for bit sizes > 1
+                if bit_size > 1 {
+                    let is_right_zero = self.brillig_context.allocate_register();
+                    let zero = self.brillig_context.make_constant(0_usize.into(), bit_size);
+                    self.brillig_context.binary_instruction(
+                        zero,
+                        right.address,
+                        is_right_zero,
+                        BrilligBinaryOp::Integer { op: BinaryIntOp::Equals, bit_size },
+                    );
+                    self.brillig_context.if_not_instruction(is_right_zero, |ctx| {
+                        let condition = ctx.allocate_register();
+                        // Check that result / rhs == lhs
+                        ctx.binary_instruction(
+                            result.address,
+                            right.address,
+                            condition,
+                            BrilligBinaryOp::Integer { op: BinaryIntOp::UnsignedDiv, bit_size },
+                        );
+                        ctx.binary_instruction(
+                            condition,
+                            left.address,
+                            condition,
+                            BrilligBinaryOp::Integer { op: BinaryIntOp::Equals, bit_size },
+                        );
+                        ctx.constrain_instruction(
+                            condition,
+                            Some("attempt to multiply with overflow".to_string()),
+                        );
+                        ctx.deallocate_register(condition);
+                    });
+                    self.brillig_context.deallocate_register(is_right_zero);
+                    self.brillig_context.deallocate_register(zero);
+                }
+            }
+            _ => {}
+        }
     }
 
     /// Converts an SSA `ValueId` into a `RegisterOrMemory`. Initializes if necessary.
@@ -1403,8 +1488,6 @@ impl<'block> BrilligBlock<'block> {
 }
 
 /// Returns the type of the operation considering the types of the operands
-/// TODO: SSA issues binary operations between fields and integers.
-/// This probably should be explicitly casted in SSA to avoid having to coerce at this level.
 pub(crate) fn type_of_binary_operation(lhs_type: &Type, rhs_type: &Type) -> Type {
     match (lhs_type, rhs_type) {
         (_, Type::Function) | (Type::Function, _) => {
@@ -1419,10 +1502,6 @@ pub(crate) fn type_of_binary_operation(lhs_type: &Type, rhs_type: &Type) -> Type
         (_, Type::Slice(..)) | (Type::Slice(..), _) => {
             unreachable!("Arrays are invalid in binary operations")
         }
-        // If either side is a Field constant then, we coerce into the type
-        // of the other operand
-        (Type::Numeric(NumericType::NativeField), typ)
-        | (typ, Type::Numeric(NumericType::NativeField)) => typ.clone(),
         // If both sides are numeric type, then we expect their types to be
         // the same.
         (Type::Numeric(lhs_type), Type::Numeric(rhs_type)) => {
@@ -1441,7 +1520,7 @@ pub(crate) fn type_of_binary_operation(lhs_type: &Type, rhs_type: &Type) -> Type
 pub(crate) fn convert_ssa_binary_op_to_brillig_binary_op(
     ssa_op: BinaryOp,
     typ: &Type,
-) -> BrilligBinaryOp {
+) -> (BrilligBinaryOp, bool) {
     // First get the bit size and whether its a signed integer, if it is a numeric type
     // if it is not,then we return None, indicating that
     // it is a Field.
@@ -1461,10 +1540,6 @@ pub(crate) fn convert_ssa_binary_op_to_brillig_binary_op(
             BinaryOp::Mul => BrilligBinaryOp::Field { op: BinaryFieldOp::Mul },
             BinaryOp::Div => BrilligBinaryOp::Field { op: BinaryFieldOp::Div },
             BinaryOp::Eq => BrilligBinaryOp::Field { op: BinaryFieldOp::Equals },
-            BinaryOp::Lt => BrilligBinaryOp::Integer {
-                op: BinaryIntOp::LessThan,
-                bit_size: BRILLIG_INTEGER_ARITHMETIC_BIT_SIZE,
-            },
             _ => unreachable!(
                 "Field type cannot be used with {op}. This should have been caught by the frontend"
             ),
@@ -1500,7 +1575,9 @@ pub(crate) fn convert_ssa_binary_op_to_brillig_binary_op(
 
     // If bit size is available then it is a binary integer operation
     match bit_size_signedness {
-        Some((bit_size, is_signed)) => binary_op_to_int_op(ssa_op, *bit_size, is_signed),
-        None => binary_op_to_field_op(ssa_op),
+        Some((bit_size, is_signed)) => {
+            (binary_op_to_int_op(ssa_op, *bit_size, is_signed), is_signed)
+        }
+        None => (binary_op_to_field_op(ssa_op), false),
     }
 }

compiler/noirc_evaluator/src/brillig/brillig_ir.rs

@@ -29,17 +29,6 @@ use acvm::{
 use debug_show::DebugShow;
 use num_bigint::BigUint;
 
-/// Integer arithmetic in Brillig is limited to 127 bit
-/// integers.
-///
-/// We could lift this in the future and have Brillig
-/// do big integer arithmetic when it exceeds the field size
-/// or we could have users re-implement big integer arithmetic
-/// in Brillig.
-/// Since constrained functions do not have this property, it
-/// would mean that unconstrained functions will differ from
-/// constrained functions in terms of syntax compatibility.
-pub(crate) const BRILLIG_INTEGER_ARITHMETIC_BIT_SIZE: u32 = 127;
 /// The Brillig VM does not apply a limit to the memory address space,
 /// As a convention, we take use 64 bits. This means that we assume that
 /// memory has 2^64 memory slots.
@@ -356,6 +345,21 @@ impl BrilligContext {
         self.enter_section(end_section);
     }
 
+    /// This instruction issues a branch that jumps over the code generated by the given function if the condition is truthy
+    pub(crate) fn if_not_instruction(
+        &mut self,
+        condition: MemoryAddress,
+        f: impl FnOnce(&mut BrilligContext),
+    ) {
+        let (end_section, end_label) = self.reserve_next_section_label();
+
+        self.jump_if_instruction(condition, end_label.clone());
+
+        f(self);
+
+        self.enter_section(end_section);
+    }
+
     /// Adds a label to the next opcode
     pub(crate) fn enter_context<T: ToString>(&mut self, label: T) {
         self.debug_show.enter_context(label.to_string());
@@ -533,7 +537,7 @@ impl BrilligContext {
         result: MemoryAddress,
         operation: BrilligBinaryOp,
     ) {
-        self.debug_show.binary_instruction(lhs, rhs, result, operation.clone());
+        self.debug_show.binary_instruction(lhs, rhs, result, operation);
         match operation {
             BrilligBinaryOp::Field { op } => {
                 let opcode = BrilligOpcode::BinaryFieldOp { op, destination: result, lhs, rhs };
@@ -1082,7 +1086,7 @@ impl BrilligContext {
 }
 
 /// Type to encapsulate the binary operation types in Brillig
-#[derive(Clone)]
+#[derive(Clone, Copy)]
 pub(crate) enum BrilligBinaryOp {
     Field { op: BinaryFieldOp },
     Integer { op: BinaryIntOp, bit_size: u32 },

test_programs/execution_success/brillig_fns_as_values/Prover.toml

@@ -1 +1 @@
-x = "0"
+x = "1"

test_programs/execution_success/brillig_fns_as_values/src/main.nr

@@ -7,9 +7,9 @@ struct MyStruct {
 fn main(x: u32) {
     assert(wrapper(increment, x) == x + 1);
     assert(wrapper(increment_acir, x) == x + 1);
-    assert(wrapper(decrement, x) == std::wrapping_sub(x, 1));
+    assert(wrapper(decrement, x) == x - 1);
     assert(wrapper_with_struct(MyStruct { operation: increment }, x) == x + 1);
-    assert(wrapper_with_struct(MyStruct { operation: decrement }, x) == std::wrapping_sub(x, 1));
+    assert(wrapper_with_struct(MyStruct { operation: decrement }, x) == x - 1);
     // https://github.com/noir-lang/noir/issues/1975
     assert(increment(x) == x + 1);
 }

test_programs/execution_success/brillig_wrapping/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "brillig_wrapping"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_success/brillig_wrapping/Prover.toml

@@ -0,0 +1,2 @@
+x = 0
+y = 255

test_programs/execution_success/brillig_wrapping/src/main.nr

@@ -0,0 +1,8 @@
+use dep::std;
+
+unconstrained fn main(x: u8, y: u8) {
+    assert(std::wrapping_sub(x, 1) == y);
+    assert(std::wrapping_add(y, 1) == x);
+    assert(std::wrapping_mul(y, y) == 1);
+}
+

test_programs/noir_test_success/brillig_overflow_checks/Nargo.toml

@@ -0,0 +1,5 @@
+[package]
+name = "brillig_overflow_checks"
+type = "bin"
+authors = [""]
+[dependencies]

test_programs/noir_test_success/brillig_overflow_checks/src/main.nr

@@ -0,0 +1,23 @@
+use dep::std::field::bn254::{TWO_POW_128, assert_gt};
+
+#[test(should_fail_with = "attempt to add with overflow")]
+unconstrained fn test_overflow_add() {
+    let a: u8 = 255;
+    let b: u8 = 1;
+    assert_eq(a + b, 0);
+}
+
+#[test(should_fail_with = "attempt to subtract with overflow")]
+unconstrained fn test_overflow_sub() {
+    let a: u8 = 0;
+    let b: u8 = 1;
+    assert_eq(a - b, 255);
+}
+
+#[test(should_fail_with = "attempt to multiply with overflow")]
+unconstrained fn test_overflow_mul() {
+    let a: u8 = 128;
+    let b: u8 = 2;
+    assert_eq(a * b, 0);
+}
+