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

chore: pull out change to expression splitting from sync PR #7215

Merged
merged 1 commit into from
Jun 27, 2024
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
38 changes: 36 additions & 2 deletions noir/noir-repo/acvm-repo/acvm/src/compiler/transformers/csat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -432,7 +432,7 @@ fn fits_in_one_identity<F: AcirField>(expr: &Expression<F>, width: usize) -> boo
return true;
}

// We now know that we have a single mul term. We also know that the mul term must match up with two other terms
// We now know that we have a single mul term. We also know that the mul term must match up with at least one of the other terms
// A polynomial whose mul terms are non zero which do not match up with two terms in the fan-in cannot fit into one opcode
// An example of this is: Axy + Bx + Cy + ...
// Notice how the bivariate monomial xy has two univariate monomials with their respective coefficients
Expand Down Expand Up @@ -461,7 +461,25 @@ fn fits_in_one_identity<F: AcirField>(expr: &Expression<F>, width: usize) -> boo
}
}

found_x & found_y
// If the multiplication is a squaring then we must assign the two witnesses to separate wires and so we
// can never get a zero contribution to the width.
let multiplication_is_squaring = mul_term.1 == mul_term.2;

let mul_term_width_contribution = if !multiplication_is_squaring && (found_x & found_y) {
// Both witnesses involved in the multiplication exist elsewhere in the expression.
// They both do not contribute to the width of the expression as this would be double-counting
// due to their appearance in the linear terms.
0
} else if found_x || found_y {
// One of the witnesses involved in the multiplication exists elsewhere in the expression.
// The multiplication then only contributes 1 new witness to the width.
1
} else {
// Worst case scenario, the multiplication is using completely unique witnesses so has a contribution of 2.
2
};

mul_term_width_contribution + expr.linear_combinations.len() <= width
}

#[cfg(test)]
Expand Down Expand Up @@ -573,4 +591,20 @@ mod tests {
let contains_b = got_optimized_opcode_a.linear_combinations.iter().any(|(_, w)| *w == b);
assert!(contains_b);
}

#[test]
fn recognize_expr_with_single_shared_witness_which_fits_in_single_identity() {
// Regression test for an expression which Zac found which should have been preserved but
// was being split into two expressions.
let expr = Expression {
mul_terms: vec![(-FieldElement::from(555u128), Witness(8), Witness(10))],
linear_combinations: vec![
(FieldElement::one(), Witness(10)),
(FieldElement::one(), Witness(11)),
(-FieldElement::one(), Witness(13)),
],
q_c: FieldElement::zero(),
};
assert!(fits_in_one_identity(&expr, 4));
}
}
Loading