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

feat: avoid generating a new witness when checking if linear expression is zero #7031

Merged
merged 4 commits into from
Jan 13, 2025
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 15 additions & 19 deletions compiler/noirc_evaluator/src/acir/generated_acir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -479,7 +479,7 @@ impl<F: AcirField> GeneratedAcir<F> {
pub(crate) fn is_equal(&mut self, lhs: &Expression<F>, rhs: &Expression<F>) -> Witness {
let t = lhs - rhs;

self.is_zero(&t)
self.is_zero(t)
}

/// Returns a `Witness` that is constrained to be:
Expand Down Expand Up @@ -534,36 +534,32 @@ impl<F: AcirField> GeneratedAcir<F> {
/// 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<F>) -> 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.
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
let t_witness = if let Some(witness) = t_expr.to_witness() {
witness
fn is_zero(&mut self, t_expr: Expression<F>) -> 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::<F>::from(self.get_or_create_witness(&t_expr))
};
aakoshh marked this conversation as resolved.
Show resolved Hide resolved

// 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::<F>::from(z);

let y = self.next_witness_index();
let y_expr = Expression::<F>::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();
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
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
Expand Down
Loading