fix: avoid overflows in integer division

crates/nargo_cli/tests/compile_failure/brillig_assert_fail/src/main.nr

@@ -2,7 +2,7 @@
 // 
 // The features being tested is using assert on brillig
 fn main(x: Field)  {
-    assert(1 == conditional(x as bool));
+    assert(1 == conditional(x == 1));
 }
 
 unconstrained fn conditional(x : bool) -> Field {

crates/nargo_cli/tests/execution_success/arithmetic_binary_operations/src/main.nr

@@ -1,9 +1,13 @@
 // Tests a very simple program.
 // 
 // The features being tested are:
-// Binary addition, multiplication, division
+// Binary addition, multiplication, division, constant modulo
 // x = 3, y = 4, z = 5
 fn main(x : Field, y : Field, z : Field) -> pub Field {
+    //constant modulo
+    assert(x % 2 == 1);
+    assert(y as u1 == 0);
+
     let a = x + x; // 3 + 3 = 6
     let b = a - y; // 6 - 4 = 2
     let c = b * z; // 2 * 5 = 10

crates/nargo_cli/tests/execution_success/brillig_assert/src/main.nr

@@ -2,7 +2,7 @@
 // 
 // The features being tested is using assert on brillig
 fn main(x: Field)  {
-    assert(1 == conditional(x as bool));
+    assert(1 == conditional(x == 1));
 }
 
 unconstrained fn conditional(x : bool) -> Field {

crates/nargo_cli/tests/execution_success/brillig_conditional/src/main.nr

@@ -2,7 +2,7 @@
 // 
 // The features being tested is basic conditonal on brillig
 fn main(x: Field)  {
-    assert(4 == conditional(x as bool));
+    assert(4 == conditional(x == 1));
 }
 
 unconstrained fn conditional(x : bool) -> Field {

crates/nargo_cli/tests/execution_success/brillig_not/src/main.nr

@@ -2,8 +2,8 @@
 // 
 // The features being tested is not instruction on brillig
 fn main(x: Field, y : Field)  {
-    assert(false == not_operator(x as bool));
-    assert(true == not_operator(y as bool));
+    assert(false == not_operator(x == 1));
+    assert(true == not_operator(y == 1));
 }
 
 unconstrained fn not_operator(x : bool) -> bool {

crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs

@@ -686,19 +686,20 @@ impl AcirContext {
     }
 
     /// Returns an `AcirVar` which will be constrained to be lhs mod 2^{rhs}
-    /// In order to do this, we simply perform euclidian division of lhs by 2^{rhs}
+    /// In order to do this, we 'simply' perform euclidian division of lhs by 2^{rhs}
     /// The remainder of the division is then lhs mod 2^{rhs}
     pub(crate) fn truncate_var(
         &mut self,
         lhs: AcirVar,
         rhs: u32,
         max_bit_size: u32,
     ) -> Result<AcirVar, RuntimeError> {
-        let lhs_expr = self.var_to_expression(lhs)?;
-
         // 2^{rhs}
         let divisor = FieldElement::from(2_i128).pow(&FieldElement::from(rhs as i128));
-        // Computes lhs = 2^{rhs} * q + r
+
+        let lhs_data = &self.vars[&lhs];
+        let lhs_expr = lhs_data.to_expression();
+        //  Computes lhs = 2^{rhs} * q + r
         let (_, remainder) = self.acir_ir.euclidean_division(
             &lhs_expr,
             &Expression::from_field(divisor),

crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs

@@ -456,6 +456,18 @@ impl GeneratedAcir {
             }
         }
 
+        // Avoids overflow: 'q*b+r < 2^max_q_bits*2^max_rhs_bits'
+        let mut avoid_overflow = false;
+        if max_q_bits + max_rhs_bits >= FieldElement::max_num_bits() - 1 {
+            // q*b+r can overflow; we avoid this when b is constant
+            if rhs.is_const() {
+                avoid_overflow = true;
+            } else {
+                // we do not support unbounded division
+                unreachable!("overflow in unbounded division");
+            }
+        }
+
         let (q_witness, r_witness) =
             self.brillig_quotient(lhs.clone(), rhs.clone(), predicate.clone(), max_bit_size + 1);
 
@@ -482,6 +494,32 @@ impl GeneratedAcir {
         let div_euclidean = &self.mul_with_witness(lhs, predicate)
             - &self.mul_with_witness(&rhs_constraint, predicate);
 
+        if let Some(rhs_const) = rhs.to_const() {
+            if avoid_overflow {
+                // we compute q0 = p/rhs
+                let rhs_big = BigUint::from_bytes_be(&rhs_const.to_be_bytes());
+                let q0_big = FieldElement::modulus() / &rhs_big;
+                let q0 = FieldElement::from_be_bytes_reduce(&q0_big.to_bytes_be());
+                // when q == q0, b*q+r can overflow so we need to bound r to avoid the overflow.
+                let size_predicate =
+                    self.is_equal(&Expression::from_field(q0), &Expression::from(q_witness));
+                let predicate = self.mul_with_witness(&size_predicate.into(), predicate);
+                // Ensure that there is no overflow, under q == q0 predicate
+                let max_r_big = FieldElement::modulus() - q0_big * rhs_big;
+                let max_r = FieldElement::from_be_bytes_reduce(&max_r_big.to_bytes_be());
+                let max_r_predicate =
+                    self.mul_with_witness(&predicate, &Expression::from_field(max_r));
+                let r_predicate = self.mul_with_witness(&Expression::from(r_witness), &predicate);
+                // Bound the remainder to be <p-q0*b, if the predicate is true.
+                self.bound_constraint_with_offset(
+                    &r_predicate,
+                    &max_r_predicate,
+                    &predicate,
+                    rhs_const.num_bits(),
+                )?;
+            }
+        }
+
         self.push_opcode(AcirOpcode::Arithmetic(div_euclidean));
 
         Ok((q_witness, r_witness))