diff --git a/crates/nargo_cli/tests/compile_failure/brillig_assert_fail/src/main.nr b/crates/nargo_cli/tests/compile_failure/brillig_assert_fail/src/main.nr index 801a818c816..53619859dfa 100644 --- a/crates/nargo_cli/tests/compile_failure/brillig_assert_fail/src/main.nr +++ b/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 { diff --git a/crates/nargo_cli/tests/execution_success/arithmetic_binary_operations/src/main.nr b/crates/nargo_cli/tests/execution_success/arithmetic_binary_operations/src/main.nr index 391aa27049d..201353393a6 100644 --- a/crates/nargo_cli/tests/execution_success/arithmetic_binary_operations/src/main.nr +++ b/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 diff --git a/crates/nargo_cli/tests/execution_success/brillig_assert/src/main.nr b/crates/nargo_cli/tests/execution_success/brillig_assert/src/main.nr index 632c72f2393..ca2d8850c04 100644 --- a/crates/nargo_cli/tests/execution_success/brillig_assert/src/main.nr +++ b/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 { diff --git a/crates/nargo_cli/tests/execution_success/brillig_conditional/src/main.nr b/crates/nargo_cli/tests/execution_success/brillig_conditional/src/main.nr index 3755dd93c01..96e5217ca65 100644 --- a/crates/nargo_cli/tests/execution_success/brillig_conditional/src/main.nr +++ b/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 { diff --git a/crates/nargo_cli/tests/execution_success/brillig_not/src/main.nr b/crates/nargo_cli/tests/execution_success/brillig_not/src/main.nr index 0466649f67c..1ce39363bd3 100644 --- a/crates/nargo_cli/tests/execution_success/brillig_not/src/main.nr +++ b/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 { diff --git a/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs b/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs index 0fc10ee33c9..3005d3db2c8 100644 --- a/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs +++ b/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs @@ -686,7 +686,7 @@ 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, @@ -694,11 +694,12 @@ impl AcirContext { rhs: u32, max_bit_size: u32, ) -> Result { - 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), diff --git a/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs b/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs index 673323d671b..33f55e76de4 100644 --- a/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs +++ b/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