fix: avoid overflows in integer division

crates/nargo_cli/tests/test_data/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/test_data/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/test_data/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/brillig/brillig_gen/brillig_directive.rs

@@ -87,3 +87,53 @@ pub(crate) fn directive_quotient(bit_size: u32) -> Vec<BrilligOpcode> {
         BrilligOpcode::Stop,
     ]
 }
+
+/// Generates brillig bytecode which computes `(a - pow) / b + 1` if a >= pow,
+/// It returns `0` if a < pow
+///
+///
+pub(crate) fn directive_truncate_helper(bit_size: u32) -> Vec<BrilligOpcode> {
+    // `a` is (0) (i.e register index 0)
+    // `b` is (1)
+    // `pow` is (2)
+    vec![
+        // If the predicate is zero, we jump to the exit segment
+        BrilligOpcode::BinaryIntOp {
+            op: BinaryIntOp::LessThan,
+            lhs: RegisterIndex::from(0),
+            rhs: RegisterIndex::from(2),
+            destination: RegisterIndex::from(3),
+            bit_size,
+        },
+        BrilligOpcode::JumpIf { condition: RegisterIndex::from(3), location: 7 },
+        //(0) = a-pow
+        BrilligOpcode::BinaryIntOp {
+            op: BinaryIntOp::Sub,
+            lhs: RegisterIndex::from(0),
+            rhs: RegisterIndex::from(2),
+            destination: RegisterIndex::from(0),
+            bit_size,
+        },
+        //(0) = (0)/(1) = (a-pow)/b
+        BrilligOpcode::BinaryIntOp {
+            op: BinaryIntOp::UnsignedDiv,
+            lhs: RegisterIndex::from(0),
+            rhs: RegisterIndex::from(1),
+            destination: RegisterIndex::from(0),
+            bit_size,
+        },
+        BrilligOpcode::Const { destination: RegisterIndex::from(1), value: Value::from(1_usize) },
+        //(0)= (0)+1
+        BrilligOpcode::BinaryIntOp {
+            op: BinaryIntOp::Add,
+            lhs: RegisterIndex::from(0),
+            rhs: RegisterIndex::from(1),
+            destination: RegisterIndex::from(0),
+            bit_size,
+        },
+        BrilligOpcode::Stop,
+        // Exit segment: we return 0
+        BrilligOpcode::Const { destination: RegisterIndex::from(0), value: Value::from(0_usize) },
+        BrilligOpcode::Stop,
+    ]
+}

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

@@ -20,6 +20,7 @@ use acvm::{
 };
 use iter_extended::{try_vecmap, vecmap};
 use noirc_errors::Location;
+use num_bigint::BigUint;
 use std::collections::HashMap;
 use std::{borrow::Cow, hash::Hash};
 
@@ -608,20 +609,80 @@ 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,
+        mut lhs: AcirVar,
         rhs: u32,
-        max_bit_size: u32,
+        mut max_bit_size: u32,
     ) -> Result<AcirVar, RuntimeError> {
-        let lhs_data = &self.vars[&lhs];
-        let lhs_expr = lhs_data.to_expression();
-
         // 2^{rhs}
         let divisor = FieldElement::from(2_i128).pow(&FieldElement::from(rhs as i128));
-        // Computes lhs = 2^{rhs} * q + r
+        // Target bit size is the bit size of the field modulus with some margin.
+        // This margin is required for the euclidian division which does not work with field elements
+        let target_bit_size = FieldElement::max_num_bits() - 3;
+
+        if max_bit_size > target_bit_size {
+            max_bit_size = target_bit_size;
+            // lhs is higher than the desired bit size, so we will remove multiples of the divisor from lhs
+            // until we get under the bit size. This will not change the end result.
+            let big_divisor = BigUint::from(2_u32).pow(rhs);
+            let one = self.add_constant(FieldElement::one());
+            let divisor_var = self.add_constant(divisor);
+            // Create a variable quotient_high such that lhs-quotient_high*divisor is target_bit_size-bits
+            let quotient_high = self.add_variable();
+            // Computes quotient_high non-deterministically
+            let target_bit_pow =
+                FieldElement::from(2_i128).pow(&FieldElement::from(target_bit_size as i128));
+            let target_bit_pow_var = self.add_constant(target_bit_pow);
+            let truncate_code =
+                brillig_directive::directive_truncate_helper(FieldElement::max_num_bits());
+            let field_type = AcirType::NumericType(NumericType::NativeField);
+            let inputs = vec![
+                AcirValue::Var(lhs, field_type.clone()),
+                AcirValue::Var(divisor_var, field_type.clone()),
+                AcirValue::Var(target_bit_pow_var, field_type.clone()),
+            ];
+            let quotient_high_value = self.brillig(one, truncate_code, inputs, vec![field_type])?
+                [0]
+            .clone()
+            .into_var()?;
+            self.assert_eq_var(quotient_high, quotient_high_value)?;
+            // Bounds quotient_high to q_max_big
+            // this bound is the smallest integer s.t p-1-bound*divisor < 2^target_bit_size
+            // since lhs is p-1 at max, we do not need an higher value
+            let q_max_big = (FieldElement::modulus()
+                - BigUint::from(1_u32)
+                - BigUint::from(2_u32).pow(target_bit_size))
+                / big_divisor
+                + BigUint::from(1_u32);
+            let q_max_bits = q_max_big.bits() as u32;
+            let toto = FieldElement::modulus()
+                - BigUint::from(1_u32)
+                - BigUint::from(2_u32).pow(target_bit_size);
+            dbg!(toto.bits());
+            let q_max_var =
+                self.add_constant(FieldElement::from_be_bytes_reduce(&q_max_big.to_bytes_be()));
+            self.range_constrain_var(
+                quotient_high,
+                &NumericType::Unsigned { bit_size: q_max_bits },
+            )?;
+            dbg!(&q_max_big);
+            dbg!(&q_max_bits);
+            self.less_than_constrain(quotient_high, q_max_var, q_max_bits, one)?;
+            // Reduce lhs with quotient_high
+            let reduce = self.mul_var(quotient_high, divisor_var)?;
+            let lhs_reduce = self.sub_var(lhs, reduce)?;
+            let lhs_reduce_witness = self.var_to_witness(lhs_reduce)?;
+            // Constrain lhs_reduce to be reduced to the target_bit_size
+            self.acir_ir.range_constraint(lhs_reduce_witness, target_bit_size)?;
+            lhs = lhs_reduce;
+        }
+
+        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

@@ -432,6 +432,8 @@ impl GeneratedAcir {
             }
         }
 
+        // Avoids overflow: 'q*b+r < 2^max_q_bits*2^max_rhs_bits'
+        assert!(max_q_bits + max_rhs_bits < FieldElement::max_num_bits() - 1);
         let (q_witness, r_witness) =
             self.brillig_quotient(lhs.clone(), rhs.clone(), predicate.clone(), max_bit_size + 1);
 

crates/noirc_evaluator/src/ssa/acir_gen/mod.rs

@@ -1121,7 +1121,7 @@ impl Context {
 
 #[cfg(test)]
 mod tests {
-    use std::{rc::Rc, collections::HashMap};
+    use std::{collections::HashMap, rc::Rc};
 
     use acvm::{
         acir::{