Skip to content

Commit

Permalink
fix: Divide by zero should fail to satisfy constraints for Field an…
Browse files Browse the repository at this point in the history
…d ints (#2475)
  • Loading branch information
vezenovm authored Aug 29, 2023
1 parent 37bb781 commit 1b85816
Show file tree
Hide file tree
Showing 12 changed files with 69 additions and 2 deletions.
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 @@ -609,6 +609,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

0 comments on commit 1b85816

Please sign in to comment.