From ad0a65443f2ab0717e757936a0fa42afb73c1d52 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 19 Jun 2024 14:38:05 +0000 Subject: [PATCH 1/3] fix: avoid unnecessarily splitting expressions with multiplication terms with a shared term --- .../acvm/src/compiler/transformers/csat.rs | 40 ++++++++++++++++++- 1 file changed, 38 insertions(+), 2 deletions(-) diff --git a/acvm-repo/acvm/src/compiler/transformers/csat.rs b/acvm-repo/acvm/src/compiler/transformers/csat.rs index f2a3cc2c84e..9a6b454f54d 100644 --- a/acvm-repo/acvm/src/compiler/transformers/csat.rs +++ b/acvm-repo/acvm/src/compiler/transformers/csat.rs @@ -432,7 +432,7 @@ fn fits_in_one_identity(expr: &Expression, 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 @@ -461,9 +461,29 @@ fn fits_in_one_identity(expr: &Expression, 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_x) { + // 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)] mod tests { use super::*; @@ -573,4 +593,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)) + } } From e6327ded775db0d9b86e7b27a087c76b2d0af114 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 19 Jun 2024 14:59:44 +0000 Subject: [PATCH 2/3] chore: fmt --- acvm-repo/acvm/src/compiler/transformers/csat.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/acvm-repo/acvm/src/compiler/transformers/csat.rs b/acvm-repo/acvm/src/compiler/transformers/csat.rs index 9a6b454f54d..34d4cbd33ff 100644 --- a/acvm-repo/acvm/src/compiler/transformers/csat.rs +++ b/acvm-repo/acvm/src/compiler/transformers/csat.rs @@ -482,8 +482,6 @@ fn fits_in_one_identity(expr: &Expression, width: usize) -> boo mul_term_width_contribution + expr.linear_combinations.len() <= width } - - #[cfg(test)] mod tests { use super::*; From 89d8b26ed877fabeafafa7e22b9f288b4625dcd3 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 19 Jun 2024 15:01:46 +0000 Subject: [PATCH 3/3] chore: clippy --- acvm-repo/acvm/src/compiler/transformers/csat.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/acvm-repo/acvm/src/compiler/transformers/csat.rs b/acvm-repo/acvm/src/compiler/transformers/csat.rs index 34d4cbd33ff..19cc18ca7f3 100644 --- a/acvm-repo/acvm/src/compiler/transformers/csat.rs +++ b/acvm-repo/acvm/src/compiler/transformers/csat.rs @@ -465,7 +465,7 @@ fn fits_in_one_identity(expr: &Expression, width: usize) -> boo // 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_x) { + 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. @@ -605,6 +605,6 @@ mod tests { ], q_c: FieldElement::zero(), }; - assert!(fits_in_one_identity(&expr, 4)) + assert!(fits_in_one_identity(&expr, 4)); } }