Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: Divide by zero should fail to satisfy constraints for Field and ints #2475

Merged
merged 10 commits into from
Aug 29, 2023
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "divide_by_zero"
type = "bin"
authors = [""]
compiler_version = "0.10.3"

[dependencies]
Empty file.
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
use dep::std;

fn main() {
let a: Field = 3 / 0;
std::println(a);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "div_by_zero_numerator_witness"
type = "bin"
authors = [""]
compiler_version = "0.10.3"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
x = "3"
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
use dep::std;

fn main(x: Field) {
let a: Field = x / 0;
std::println(a);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "div_by_zero_witness"
type = "bin"
authors = [""]
compiler_version = "0.10.3"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
x = "3"
y = "0"
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
use dep::std;

// It is expected that `y` must be equal to 0.
fn main(x : Field, y : pub Field) {
let a: Field = x / y;
std::println(a);
}
12 changes: 10 additions & 2 deletions crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -284,8 +284,14 @@ impl AcirContext {
let var_data = &self.vars[&var];
if let AcirVarData::Const(constant) = var_data {
// Note that this will return a 0 if the inverse is not available
let result_var = self.add_data(AcirVarData::Const(constant.inverse()));
return Ok(result_var);
let inverted_var = self.add_data(AcirVarData::Const(constant.inverse()));

// Check that the inverted var is valid.
// This check prevents invalid divisons by zero.
let should_be_one = self.mul_var(inverted_var, var)?;
self.maybe_eq_predicate(should_be_one, predicate)?;

return Ok(inverted_var);
}

// Compute the inverse with brillig code
Expand All @@ -300,6 +306,8 @@ impl AcirContext {
)?;
let inverted_var = Self::expect_one_var(results);

// Check that the inverted var is valid.
// This check prevents invalid divisons by zero.
let should_be_one = self.mul_var(inverted_var, var)?;
self.maybe_eq_predicate(should_be_one, predicate)?;

Expand Down
10 changes: 10 additions & 0 deletions crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -467,6 +467,16 @@ impl GeneratedAcir {
//
// If predicate is zero, `q_witness` and `r_witness` will be 0

// Check that we the rhs is not zero.
// Otherwise, when executing the brillig quotient we may attempt to divide by zero, causing a VM panic.
//
// When the predicate is 0, the equation always passes.
// When the predicate is 1, the rhs must not be 0.
let rhs_is_zero = self.is_equal(&Expression::zero(), rhs);
let rhs_is_not_zero = &self.mul_with_witness(&rhs_is_zero.into(), predicate)
- &self.mul_with_witness(&Expression::zero(), predicate);
self.push_opcode(AcirOpcode::Arithmetic(rhs_is_not_zero));

// maximum bit size for q and for [r and rhs]
let mut max_q_bits = max_bit_size;
let mut max_rhs_bits = max_bit_size;
Expand Down
6 changes: 6 additions & 0 deletions crates/noirc_evaluator/src/ssa/ir/instruction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -584,6 +584,12 @@ impl Binary {
let operand_type = dfg.type_of_value(self.lhs);

if let (Some(lhs), Some(rhs)) = (lhs, rhs) {
// If the rhs of a division is zero, attempting to evaluate the divison will cause a compiler panic.
// Thus, we do not evaluate this divison as we want to avoid triggering a panic and a division by zero
// should fail to satisfy constraints laid down during ACIR generation.
if matches!(self.operator, BinaryOp::Div) && rhs == FieldElement::zero() {
return SimplifyResult::None;
}
return match self.eval_constants(dfg, lhs, rhs, operand_type) {
Some(value) => SimplifyResult::SimplifiedTo(value),
None => SimplifyResult::None,
Expand Down