From 14c9237c92d4f7d2d30a25a20307d58c586e9fc0 Mon Sep 17 00:00:00 2001 From: Tom French <15848336+TomAFrench@users.noreply.github.com> Date: Mon, 13 Jan 2025 11:18:15 +0000 Subject: [PATCH] feat: avoid generating a new witness when checking if linear expression is zero (#7031) --- .../src/acir/generated_acir.rs | 34 ++++++++----------- 1 file changed, 15 insertions(+), 19 deletions(-) diff --git a/compiler/noirc_evaluator/src/acir/generated_acir.rs b/compiler/noirc_evaluator/src/acir/generated_acir.rs index a2b161688c0..14ceac62461 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 { - // 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 + fn is_zero(&mut self, t_expr: Expression) -> Witness { + // 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 { - 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