From 6e22b386576afc443b59fedf1e5204d9c31132dc Mon Sep 17 00:00:00 2001 From: Tom French Date: Sat, 11 Jan 2025 19:18:42 +0000 Subject: [PATCH 1/3] feat: avoid generating a new witness when checking when linear expression is zero --- .../src/acir/generated_acir.rs | 30 ++++++++----------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/compiler/noirc_evaluator/src/acir/generated_acir.rs b/compiler/noirc_evaluator/src/acir/generated_acir.rs index a2b161688c0..09872031383 100644 --- a/compiler/noirc_evaluator/src/acir/generated_acir.rs +++ b/compiler/noirc_evaluator/src/acir/generated_acir.rs @@ -479,7 +479,7 @@ impl GeneratedAcir { pub(crate) fn is_equal(&mut self, lhs: &Expression, rhs: &Expression) -> Witness { let t = lhs - rhs; - self.is_zero(&t) + self.is_zero(t) } /// Returns a `Witness` that is constrained to be: @@ -534,36 +534,32 @@ impl GeneratedAcir { /// By setting `z` to be `0`, we can make `y` equal to `1`. /// This is easily observed: `y = 1 - t * 0` /// Now since `y` is one, this means that `t` needs to be zero, or else `y * t == 0` will fail. - fn is_zero(&mut self, t_expr: &Expression) -> Witness { + fn is_zero(&mut self, t_expr: Expression) -> Witness { // We're checking for equality with zero so we can negate the expression without changing the result. // This is useful as it will sometimes allow us to simplify an expression down to a witness. - let t_witness = if let Some(witness) = t_expr.to_witness() { - witness + let linear_t = if t_expr.is_degree_one_univariate() { + t_expr } else { - let negated_expr = t_expr * -F::one(); - self.get_or_create_witness(&negated_expr) + Expression::::from(self.get_or_create_witness(&t_expr)) }; // Call the inversion directive, since we do not apply a constraint // the prover can choose anything here. - let z = self.brillig_inverse(t_witness.into()); + let z = self.brillig_inverse(linear_t.clone()); + let z_expr = Expression::::from(z); let y = self.next_witness_index(); + let y_expr = Expression::::from(y); // Add constraint y == 1 - tz => y + tz - 1 == 0 - let y_is_boolean_constraint = Expression { - mul_terms: vec![(F::one(), t_witness, z)], - linear_combinations: vec![(F::one(), y)], - q_c: -F::one(), - }; + let mut y_is_boolean_constraint = + (&z_expr * &linear_t).expect("multiplying two linear expressions"); + y_is_boolean_constraint.push_addition_term(F::one(), y); + let y_is_boolean_constraint = y_is_boolean_constraint - F::one(); self.assert_is_zero(y_is_boolean_constraint); // Add constraint that y * t == 0; - let ty_zero_constraint = Expression { - mul_terms: vec![(F::one(), t_witness, y)], - linear_combinations: vec![], - q_c: F::zero(), - }; + let ty_zero_constraint = (&y_expr * &linear_t).expect("multiplying two linear expressions"); self.assert_is_zero(ty_zero_constraint); y From a501b6fcf1431e98abcbcad58b02a9c8736a8a22 Mon Sep 17 00:00:00 2001 From: Tom French <15848336+TomAFrench@users.noreply.github.com> Date: Sat, 11 Jan 2025 19:31:13 +0000 Subject: [PATCH 2/3] Update compiler/noirc_evaluator/src/acir/generated_acir.rs --- compiler/noirc_evaluator/src/acir/generated_acir.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/compiler/noirc_evaluator/src/acir/generated_acir.rs b/compiler/noirc_evaluator/src/acir/generated_acir.rs index 09872031383..58d51f5b9c1 100644 --- a/compiler/noirc_evaluator/src/acir/generated_acir.rs +++ b/compiler/noirc_evaluator/src/acir/generated_acir.rs @@ -535,8 +535,8 @@ impl GeneratedAcir { /// This is easily observed: `y = 1 - t * 0` /// Now since `y` is one, this means that `t` needs to be zero, or else `y * t == 0` will fail. fn is_zero(&mut self, t_expr: Expression) -> Witness { - // We're checking for equality with zero so we can negate the expression without changing the result. - // This is useful as it will sometimes allow us to simplify an expression down to a witness. + // We're going to be multiplying this expression by a two different witnesses in a second so we want to + // ensure that this expression only contains a single witness. We can tolerate a coefficients and constant terms however. let linear_t = if t_expr.is_degree_one_univariate() { t_expr } else { From 3a86ceab3d0fbc61d78426c0a745c32e51adf9e7 Mon Sep 17 00:00:00 2001 From: Tom French <15848336+TomAFrench@users.noreply.github.com> Date: Sun, 12 Jan 2025 00:08:45 +0000 Subject: [PATCH 3/3] Update generated_acir.rs --- compiler/noirc_evaluator/src/acir/generated_acir.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/compiler/noirc_evaluator/src/acir/generated_acir.rs b/compiler/noirc_evaluator/src/acir/generated_acir.rs index 58d51f5b9c1..14ceac62461 100644 --- a/compiler/noirc_evaluator/src/acir/generated_acir.rs +++ b/compiler/noirc_evaluator/src/acir/generated_acir.rs @@ -535,8 +535,8 @@ impl GeneratedAcir { /// This is easily observed: `y = 1 - t * 0` /// Now since `y` is one, this means that `t` needs to be zero, or else `y * t == 0` will fail. fn is_zero(&mut self, t_expr: Expression) -> Witness { - // We're going to be multiplying this expression by a two different witnesses in a second so we want to - // ensure that this expression only contains a single witness. We can tolerate a coefficients and constant terms however. + // We're going to be multiplying this expression by two different witnesses in a second so we want to + // ensure that this expression only contains a single witness. We can tolerate coefficients and constant terms however. let linear_t = if t_expr.is_degree_one_univariate() { t_expr } else {