From 1b85816cb1f7539917ed9212c411613f29168add Mon Sep 17 00:00:00 2001 From: Maxim Vezenov Date: Tue, 29 Aug 2023 19:54:08 +0100 Subject: [PATCH] fix: Divide by zero should fail to satisfy constraints for `Field` and ints (#2475) --- .../compile_failure/div_by_zero_constants/Nargo.toml | 7 +++++++ .../div_by_zero_constants/Prover.toml | 0 .../div_by_zero_constants/src/main.nr | 6 ++++++ .../div_by_zero_numerator_witness/Nargo.toml | 7 +++++++ .../div_by_zero_numerator_witness/Prover.toml | 1 + .../div_by_zero_numerator_witness/src/main.nr | 6 ++++++ .../compile_failure/div_by_zero_witness/Nargo.toml | 7 +++++++ .../compile_failure/div_by_zero_witness/Prover.toml | 2 ++ .../compile_failure/div_by_zero_witness/src/main.nr | 7 +++++++ .../src/ssa/acir_gen/acir_ir/acir_variable.rs | 12 ++++++++++-- .../src/ssa/acir_gen/acir_ir/generated_acir.rs | 10 ++++++++++ crates/noirc_evaluator/src/ssa/ir/instruction.rs | 6 ++++++ 12 files changed, 69 insertions(+), 2 deletions(-) create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_constants/Nargo.toml create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_constants/Prover.toml create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_constants/src/main.nr create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/Nargo.toml create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/Prover.toml create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/src/main.nr create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_witness/Nargo.toml create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_witness/Prover.toml create mode 100644 crates/nargo_cli/tests/compile_failure/div_by_zero_witness/src/main.nr diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_constants/Nargo.toml b/crates/nargo_cli/tests/compile_failure/div_by_zero_constants/Nargo.toml new file mode 100644 index 00000000000..55e36368845 --- /dev/null +++ b/crates/nargo_cli/tests/compile_failure/div_by_zero_constants/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "divide_by_zero" +type = "bin" +authors = [""] +compiler_version = "0.10.3" + +[dependencies] \ No newline at end of file diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_constants/Prover.toml b/crates/nargo_cli/tests/compile_failure/div_by_zero_constants/Prover.toml new file mode 100644 index 00000000000..e69de29bb2d diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_constants/src/main.nr b/crates/nargo_cli/tests/compile_failure/div_by_zero_constants/src/main.nr new file mode 100644 index 00000000000..2259d51e6de --- /dev/null +++ b/crates/nargo_cli/tests/compile_failure/div_by_zero_constants/src/main.nr @@ -0,0 +1,6 @@ +use dep::std; + +fn main() { + let a: Field = 3 / 0; + std::println(a); +} \ No newline at end of file diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/Nargo.toml b/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/Nargo.toml new file mode 100644 index 00000000000..58a60a38a0c --- /dev/null +++ b/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "div_by_zero_numerator_witness" +type = "bin" +authors = [""] +compiler_version = "0.10.3" + +[dependencies] \ No newline at end of file diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/Prover.toml b/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/Prover.toml new file mode 100644 index 00000000000..07890234a19 --- /dev/null +++ b/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/Prover.toml @@ -0,0 +1 @@ +x = "3" diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/src/main.nr b/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/src/main.nr new file mode 100644 index 00000000000..f51b26d5ba1 --- /dev/null +++ b/crates/nargo_cli/tests/compile_failure/div_by_zero_numerator_witness/src/main.nr @@ -0,0 +1,6 @@ +use dep::std; + +fn main(x: Field) { + let a: Field = x / 0; + std::println(a); +} diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/Nargo.toml b/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/Nargo.toml new file mode 100644 index 00000000000..08dbe74f018 --- /dev/null +++ b/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "div_by_zero_witness" +type = "bin" +authors = [""] +compiler_version = "0.10.3" + +[dependencies] \ No newline at end of file diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/Prover.toml b/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/Prover.toml new file mode 100644 index 00000000000..a1f166bf325 --- /dev/null +++ b/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/Prover.toml @@ -0,0 +1,2 @@ +x = "3" +y = "0" diff --git a/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/src/main.nr b/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/src/main.nr new file mode 100644 index 00000000000..4ce567e49a6 --- /dev/null +++ b/crates/nargo_cli/tests/compile_failure/div_by_zero_witness/src/main.nr @@ -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); +} 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 08e4197326f..b2e5a0e56e1 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 @@ -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 @@ -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)?; 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 3f12bda8da2..d2edd596503 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 @@ -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; diff --git a/crates/noirc_evaluator/src/ssa/ir/instruction.rs b/crates/noirc_evaluator/src/ssa/ir/instruction.rs index c0d2a6251f2..be289909581 100644 --- a/crates/noirc_evaluator/src/ssa/ir/instruction.rs +++ b/crates/noirc_evaluator/src/ssa/ir/instruction.rs @@ -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,