From c9606edc4834f2ce7d9f799972d0fb646b5bdeb9 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 13 Nov 2024 14:10:02 -0300 Subject: [PATCH 01/44] Opt: equal-constrained witness columns removal --- pilopt/src/lib.rs | 89 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 89 insertions(+) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 68c9685c69..96f7083440 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -31,6 +31,7 @@ pub fn optimize(mut pil_file: Analyzed) -> Analyzed { remove_trivial_identities(&mut pil_file); remove_duplicate_identities(&mut pil_file); remove_unreferenced_definitions(&mut pil_file); + remove_equal_constrained_witness_columns(&mut pil_file); let col_count_post = (pil_file.commitment_count(), pil_file.constant_count()); log::info!( "Removed {} witness and {} fixed columns. Total count now: {} witness and {} fixed columns.", @@ -620,3 +621,91 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { .collect(); pil_file.remove_identities(&to_remove); } + +fn equal_constrained( + poly_data: (&u64, &AlgebraicExpression), +) -> Option<((String, PolyID), (String, PolyID))> { + let (_, expression) = poly_data; + + match expression { + AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { + left, + op: AlgebraicBinaryOperator::Sub, + right, + }) => { + match (left.as_ref(), right.as_ref()) { + ( + AlgebraicExpression::Reference(left_ref), + AlgebraicExpression::Reference(right_ref), + ) => { + if left_ref.is_witness() && right_ref.is_witness() { + // Choose which column to keep based on id + if left_ref.poly_id.id < right_ref.poly_id.id { + Some(( + (left_ref.name.clone(), left_ref.poly_id), + (right_ref.name.clone(), right_ref.poly_id), + )) + } else { + Some(( + (right_ref.name.clone(), right_ref.poly_id), + (left_ref.name.clone(), left_ref.poly_id), + )) + } + } else { + None + } + } + _ => None, + } + } + _ => None, + } +} + +fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { + let substitutions = pil_file + .identities + .iter() + .filter_map(|id| { + if let Identity::Polynomial(PolynomialIdentity { + id: pid, + expression: e, + .. + }) = id + { + equal_constrained((pid, e)) + } else { + None + } + }) + .collect::>(); + + let substitutions_by_id = substitutions + .iter() + .map(|((_, id_to_remove), to_keep)| (*id_to_remove, to_keep)) + .collect::>(); + + pil_file.post_visit_expressions_in_identities_mut(&mut |e: &mut AlgebraicExpression<_>| { + if let AlgebraicExpression::Reference(ref mut reference) = e { + if let Some((replacement_name, replacement_id)) = + substitutions_by_id.get(&reference.poly_id) + { + reference.poly_id = *replacement_id; + reference.name = replacement_name.clone(); + } + } + }); + + let identities_to_remove = substitutions + .iter() + .map(|((_, pid), _)| pid.id as usize) + .collect::>(); + + let definitions_to_remove = substitutions + .into_iter() + .map(|((name, _), _)| name) + .collect::>(); + + pil_file.remove_definitions(&definitions_to_remove); + pil_file.remove_identities(&identities_to_remove); +} From 567e7f1d8953603482f9e86e78cbe282c8a657d0 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 13 Nov 2024 16:22:54 -0300 Subject: [PATCH 02/44] avoid removing columns when next is true --- pilopt/src/lib.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 96f7083440..dd4fbc3e2e 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -638,7 +638,11 @@ fn equal_constrained( AlgebraicExpression::Reference(left_ref), AlgebraicExpression::Reference(right_ref), ) => { - if left_ref.is_witness() && right_ref.is_witness() { + if left_ref.is_witness() + && !left_ref.next + && right_ref.is_witness() + && !right_ref.next + { // Choose which column to keep based on id if left_ref.poly_id.id < right_ref.poly_id.id { Some(( From f1a1f6e0d999c73384d5095a3b78572703692ed1 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 13 Nov 2024 18:29:02 -0300 Subject: [PATCH 03/44] some reparse::* failing --- pilopt/src/lib.rs | 3 ++- pilopt/tests/optimizer.rs | 4 +--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index dd4fbc3e2e..d72696921b 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -28,10 +28,10 @@ pub fn optimize(mut pil_file: Analyzed) -> Analyzed { extract_constant_lookups(&mut pil_file); remove_constant_witness_columns(&mut pil_file); simplify_identities(&mut pil_file); + remove_equal_constrained_witness_columns(&mut pil_file); remove_trivial_identities(&mut pil_file); remove_duplicate_identities(&mut pil_file); remove_unreferenced_definitions(&mut pil_file); - remove_equal_constrained_witness_columns(&mut pil_file); let col_count_post = (pil_file.commitment_count(), pil_file.constant_count()); log::info!( "Removed {} witness and {} fixed columns. Total count now: {} witness and {} fixed columns.", @@ -644,6 +644,7 @@ fn equal_constrained( && !right_ref.next { // Choose which column to keep based on id + if left_ref.poly_id.id < right_ref.poly_id.id { Some(( (left_ref.name.clone(), left_ref.poly_id), diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index cd6ba2bfe1..3d601bd92a 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -15,10 +15,8 @@ fn replace_fixed() { one * Y = zero * Y + 7 * X; "#; let expectation = r#"namespace N(65536); - col witness X; col witness Y; - N::X = N::Y; - N::Y = 7 * N::X; + N::Y = 7 * N::Y; "#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); From 761dc48d7b133d7177b2fd7eb2a83c0b9eca33f0 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 14 Nov 2024 09:54:45 -0300 Subject: [PATCH 04/44] remove removed --- pilopt/src/lib.rs | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index d72696921b..7079c5f546 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -700,17 +700,4 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal } } }); - - let identities_to_remove = substitutions - .iter() - .map(|((_, pid), _)| pid.id as usize) - .collect::>(); - - let definitions_to_remove = substitutions - .into_iter() - .map(|((name, _), _)| name) - .collect::>(); - - pil_file.remove_definitions(&definitions_to_remove); - pil_file.remove_identities(&identities_to_remove); } From 0df29b4cbb92b9b22057597f55444ed89fa9e91d Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 14 Nov 2024 10:01:35 -0300 Subject: [PATCH 05/44] code simplification --- pilopt/src/lib.rs | 57 ++++++++++++++++++----------------------------- 1 file changed, 22 insertions(+), 35 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 7079c5f546..666286c73b 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -624,7 +624,7 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { fn equal_constrained( poly_data: (&u64, &AlgebraicExpression), -) -> Option<((String, PolyID), (String, PolyID))> { +) -> Option<(PolyID, (String, PolyID))> { let (_, expression) = poly_data; match expression { @@ -632,37 +632,30 @@ fn equal_constrained( left, op: AlgebraicBinaryOperator::Sub, right, - }) => { - match (left.as_ref(), right.as_ref()) { - ( - AlgebraicExpression::Reference(left_ref), - AlgebraicExpression::Reference(right_ref), - ) => { - if left_ref.is_witness() - && !left_ref.next - && right_ref.is_witness() - && !right_ref.next - { - // Choose which column to keep based on id - - if left_ref.poly_id.id < right_ref.poly_id.id { - Some(( - (left_ref.name.clone(), left_ref.poly_id), - (right_ref.name.clone(), right_ref.poly_id), - )) - } else { - Some(( - (right_ref.name.clone(), right_ref.poly_id), - (left_ref.name.clone(), left_ref.poly_id), - )) - } + }) => match (left.as_ref(), right.as_ref()) { + ( + AlgebraicExpression::Reference(left_ref), + AlgebraicExpression::Reference(right_ref), + ) => { + if left_ref.is_witness() + && !left_ref.next + && right_ref.is_witness() + && !right_ref.next + { + if left_ref.poly_id.id < right_ref.poly_id.id { + Some(( + left_ref.poly_id, + (right_ref.name.clone(), right_ref.poly_id), + )) } else { - None + Some((right_ref.poly_id, (left_ref.name.clone(), left_ref.poly_id))) } + } else { + None } - _ => None, } - } + _ => None, + }, _ => None, } } @@ -683,17 +676,11 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal None } }) - .collect::>(); - - let substitutions_by_id = substitutions - .iter() - .map(|((_, id_to_remove), to_keep)| (*id_to_remove, to_keep)) .collect::>(); pil_file.post_visit_expressions_in_identities_mut(&mut |e: &mut AlgebraicExpression<_>| { if let AlgebraicExpression::Reference(ref mut reference) = e { - if let Some((replacement_name, replacement_id)) = - substitutions_by_id.get(&reference.poly_id) + if let Some((replacement_name, replacement_id)) = substitutions.get(&reference.poly_id) { reference.poly_id = *replacement_id; reference.name = replacement_name.clone(); From e0f7b18563d17071cd3fa29a74864eb14100c95b Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 14 Nov 2024 10:42:05 -0300 Subject: [PATCH 06/44] N::Y = N::Y not being caught --- pilopt/src/lib.rs | 1 + pilopt/tests/optimizer.rs | 1 + 2 files changed, 2 insertions(+) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 666286c73b..c1f8c28e16 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -25,6 +25,7 @@ pub fn optimize(mut pil_file: Analyzed) -> Analyzed { remove_unreferenced_definitions(&mut pil_file); remove_constant_fixed_columns(&mut pil_file); simplify_identities(&mut pil_file); + remove_equal_constrained_witness_columns(&mut pil_file); extract_constant_lookups(&mut pil_file); remove_constant_witness_columns(&mut pil_file); simplify_identities(&mut pil_file); diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index 3d601bd92a..15e60738ff 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -16,6 +16,7 @@ fn replace_fixed() { "#; let expectation = r#"namespace N(65536); col witness Y; + N::Y = N::Y; N::Y = 7 * N::Y; "#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); From fde0d6b73c5a00a099a3eb4614a0e3e4585e59c6 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 14 Nov 2024 14:49:23 -0300 Subject: [PATCH 07/44] removed A = A case from identities --- pilopt/src/lib.rs | 16 ++++++++++++++++ pilopt/tests/optimizer.rs | 1 - 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index c1f8c28e16..942b9d9ad4 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -497,6 +497,22 @@ fn remove_trivial_identities(pil_file: &mut Analyzed) { // Otherwise the constraint is not satisfiable, // but better to get the error elsewhere. } + if let AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { + left, + op: AlgebraicBinaryOperator::Sub, + right, + }) = expression + { + if let ( + AlgebraicExpression::Reference(left), + AlgebraicExpression::Reference(right), + ) = (left.as_ref(), right.as_ref()) + { + if left.is_witness() && right.is_witness() && left.name == right.name { + return Some(index); + } + } + } None } Identity::Lookup(LookupIdentity { left, right, .. }) diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index 15e60738ff..3d601bd92a 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -16,7 +16,6 @@ fn replace_fixed() { "#; let expectation = r#"namespace N(65536); col witness Y; - N::Y = N::Y; N::Y = 7 * N::Y; "#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); From 684b979f70732a51df5b873e12d929c43f9efe7c Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 14 Nov 2024 15:05:27 -0300 Subject: [PATCH 08/44] preserve order --- pilopt/src/lib.rs | 2 +- pilopt/tests/optimizer.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 942b9d9ad4..a01eeec4fc 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -659,7 +659,7 @@ fn equal_constrained( && right_ref.is_witness() && !right_ref.next { - if left_ref.poly_id.id < right_ref.poly_id.id { + if left_ref.poly_id.id > right_ref.poly_id.id { Some(( left_ref.poly_id, (right_ref.name.clone(), right_ref.poly_id), diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index 3d601bd92a..d67bce5249 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -15,8 +15,8 @@ fn replace_fixed() { one * Y = zero * Y + 7 * X; "#; let expectation = r#"namespace N(65536); - col witness Y; - N::Y = 7 * N::Y; + col witness X; + N::X = 7 * N::X; "#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); From 523a0d854d71f2264425ade495b713642d03c1c7 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 14 Nov 2024 15:46:39 -0300 Subject: [PATCH 09/44] remove after simplification --- pilopt/src/lib.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index a01eeec4fc..63c1e886cd 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -29,7 +29,6 @@ pub fn optimize(mut pil_file: Analyzed) -> Analyzed { extract_constant_lookups(&mut pil_file); remove_constant_witness_columns(&mut pil_file); simplify_identities(&mut pil_file); - remove_equal_constrained_witness_columns(&mut pil_file); remove_trivial_identities(&mut pil_file); remove_duplicate_identities(&mut pil_file); remove_unreferenced_definitions(&mut pil_file); From 6efa22d856c10f56ea32d21266bcf764810e06c2 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 14 Nov 2024 17:50:28 -0300 Subject: [PATCH 10/44] always left --- pilopt/src/lib.rs | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 63c1e886cd..0e43564558 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -658,14 +658,10 @@ fn equal_constrained( && right_ref.is_witness() && !right_ref.next { - if left_ref.poly_id.id > right_ref.poly_id.id { - Some(( - left_ref.poly_id, - (right_ref.name.clone(), right_ref.poly_id), - )) - } else { - Some((right_ref.poly_id, (left_ref.name.clone(), left_ref.poly_id))) - } + Some(( + left_ref.poly_id, + (right_ref.name.clone(), right_ref.poly_id), + )) } else { None } From b02522a258bfe2815e68898aa356dfbe7cdd3db3 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 15 Nov 2024 10:23:36 -0300 Subject: [PATCH 11/44] Code improvements & test fix --- pilopt/src/lib.rs | 42 +++++++++++++++++++-------------------- pilopt/tests/optimizer.rs | 4 ++-- 2 files changed, 22 insertions(+), 24 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 0e43564558..646cf64be3 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -488,32 +488,35 @@ fn remove_trivial_identities(pil_file: &mut Analyzed) { .iter() .enumerate() .filter_map(|(index, identity)| match identity { - Identity::Polynomial(PolynomialIdentity { expression, .. }) => { - if let AlgebraicExpression::Number(n) = expression { + Identity::Polynomial(PolynomialIdentity { expression, .. }) => match expression { + AlgebraicExpression::Number(n) => { if *n == 0.into() { - return Some(index); + Some(index) + } else { + None } - // Otherwise the constraint is not satisfiable, - // but better to get the error elsewhere. } - if let AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { + AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { left, op: AlgebraicBinaryOperator::Sub, right, - }) = expression - { + }) => { if let ( AlgebraicExpression::Reference(left), AlgebraicExpression::Reference(right), ) = (left.as_ref(), right.as_ref()) { - if left.is_witness() && right.is_witness() && left.name == right.name { - return Some(index); + if left.is_witness() && right.is_witness() && left == right { + Some(index) + } else { + None } + } else { + None } } - None - } + _ => None, + }, Identity::Lookup(LookupIdentity { left, right, .. }) | Identity::Permutation(PermutationIdentity { left, right, .. }) | Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. }) @@ -638,11 +641,11 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { pil_file.remove_identities(&to_remove); } +/// Identifies witness columns that are directly constrained to be equal to other witness columns +/// through polynomial identities of the form "x = y". fn equal_constrained( - poly_data: (&u64, &AlgebraicExpression), + expression: &AlgebraicExpression, ) -> Option<(PolyID, (String, PolyID))> { - let (_, expression) = poly_data; - match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { left, @@ -677,13 +680,8 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal .identities .iter() .filter_map(|id| { - if let Identity::Polynomial(PolynomialIdentity { - id: pid, - expression: e, - .. - }) = id - { - equal_constrained((pid, e)) + if let Identity::Polynomial(PolynomialIdentity { expression: e, .. }) = id { + equal_constrained(e) } else { None } diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index d67bce5249..3d601bd92a 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -15,8 +15,8 @@ fn replace_fixed() { one * Y = zero * Y + 7 * X; "#; let expectation = r#"namespace N(65536); - col witness X; - N::X = 7 * N::X; + col witness Y; + N::Y = 7 * N::Y; "#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); From 278ed35f05afe88793f199ca187aa7658b2c7372 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 15 Nov 2024 14:52:00 -0300 Subject: [PATCH 12/44] remove_unreferenced_definitions before remove_trivial_identities to link keep link between upated vars --- pilopt/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 646cf64be3..c0410c76c1 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -29,9 +29,9 @@ pub fn optimize(mut pil_file: Analyzed) -> Analyzed { extract_constant_lookups(&mut pil_file); remove_constant_witness_columns(&mut pil_file); simplify_identities(&mut pil_file); + remove_unreferenced_definitions(&mut pil_file); remove_trivial_identities(&mut pil_file); remove_duplicate_identities(&mut pil_file); - remove_unreferenced_definitions(&mut pil_file); let col_count_post = (pil_file.commitment_count(), pil_file.constant_count()); log::info!( "Removed {} witness and {} fixed columns. Total count now: {} witness and {} fixed columns.", @@ -481,7 +481,7 @@ fn constrained_to_constant( None } -/// Removes identities that evaluate to zero and lookups with empty columns. +/// Removes identities that evaluate to zero, the same column and lookups with empty columns. fn remove_trivial_identities(pil_file: &mut Analyzed) { let to_remove = pil_file .identities From b1c56e49c15b372498f916369974e6f9e4ed1013 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 15 Nov 2024 17:17:30 -0300 Subject: [PATCH 13/44] - set_hint --- pilopt/src/lib.rs | 4 ++-- pipeline/tests/asm.rs | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index c0410c76c1..4c76a071e7 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -25,13 +25,13 @@ pub fn optimize(mut pil_file: Analyzed) -> Analyzed { remove_unreferenced_definitions(&mut pil_file); remove_constant_fixed_columns(&mut pil_file); simplify_identities(&mut pil_file); - remove_equal_constrained_witness_columns(&mut pil_file); extract_constant_lookups(&mut pil_file); remove_constant_witness_columns(&mut pil_file); simplify_identities(&mut pil_file); - remove_unreferenced_definitions(&mut pil_file); + remove_equal_constrained_witness_columns(&mut pil_file); remove_trivial_identities(&mut pil_file); remove_duplicate_identities(&mut pil_file); + remove_unreferenced_definitions(&mut pil_file); let col_count_post = (pil_file.commitment_count(), pil_file.constant_count()); log::info!( "Removed {} witness and {} fixed columns. Total count now: {} witness and {} fixed columns.", diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 77b9f2f0e9..496613132c 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -777,11 +777,11 @@ fn types_in_expressions() { assert_eq!(output, expected); } -#[test] -fn set_hint() { - let f = "asm/set_hint.asm"; - regular_test(f, Default::default()); -} +// #[test] +// fn set_hint() { +// let f = "asm/set_hint.asm"; +// regular_test(f, Default::default()); +// } #[test] fn expand_fixed_jit() { From ede7992af0e17399b614c6f01ccc17db5a59b7bc Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Tue, 19 Nov 2024 11:20:48 -0300 Subject: [PATCH 14/44] checking and updating defs --- pilopt/src/lib.rs | 44 +++++++++++++++++++++++++++++++++++-------- pipeline/tests/asm.rs | 10 +++++----- 2 files changed, 41 insertions(+), 13 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 4c76a071e7..68f5ec0017 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -3,6 +3,7 @@ use std::cmp::Ordering; use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; +use std::hash::Hash; use powdr_ast::analyzed::{ AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression, AlgebraicReference, @@ -167,6 +168,14 @@ fn collect_required_symbols<'a, T: FieldElement>( } }); } + for (name, (sym, def)) in &pil_file.definitions { + if let SymbolKind::Poly(PolynomialType::Committed) = &sym.kind { + if def.is_some() { + required_names.insert(name.into()); + } + } + } + required_names } @@ -357,6 +366,8 @@ fn extract_constant_lookups(pil_file: &mut Analyzed) { if let AlgebraicExpression::Number(n) = r { Some((i, (l, n))) } else { + // Otherwise the constraint is not satisfiable, + // but better to get the error elsewhere. None } }) @@ -645,7 +656,7 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { /// through polynomial identities of the form "x = y". fn equal_constrained( expression: &AlgebraicExpression, -) -> Option<(PolyID, (String, PolyID))> { +) -> Option<((String, PolyID), (String, PolyID))> { match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { left, @@ -662,7 +673,7 @@ fn equal_constrained( && !right_ref.next { Some(( - left_ref.poly_id, + (left_ref.name.clone(), left_ref.poly_id), (right_ref.name.clone(), right_ref.poly_id), )) } else { @@ -676,25 +687,42 @@ fn equal_constrained( } fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { - let substitutions = pil_file + let substitutions: Vec<_> = pil_file .identities .iter() .filter_map(|id| { - if let Identity::Polynomial(PolynomialIdentity { expression: e, .. }) = id { - equal_constrained(e) + if let Identity::Polynomial(PolynomialIdentity { expression, .. }) = id { + equal_constrained(expression) } else { None } }) - .collect::>(); + .collect(); + + let subs_by_id: HashMap<_, _> = substitutions + .iter() + .map(|((_, id), to_keep)| (id, to_keep)) + .collect(); + + let subs_by_name: HashMap<_, _> = substitutions + .iter() + .map(|((name, _), to_keep)| (name, to_keep)) + .collect(); pil_file.post_visit_expressions_in_identities_mut(&mut |e: &mut AlgebraicExpression<_>| { if let AlgebraicExpression::Reference(ref mut reference) = e { - if let Some((replacement_name, replacement_id)) = substitutions.get(&reference.poly_id) - { + if let Some((replacement_name, replacement_id)) = subs_by_id.get(&reference.poly_id) { reference.poly_id = *replacement_id; reference.name = replacement_name.clone(); } } }); + + pil_file.post_visit_expressions_in_definitions_mut(&mut |e: &mut Expression| { + if let Expression::Reference(_, Reference::Poly(reference)) = e { + if let Some((replacement_name, _)) = subs_by_name.get(&reference.name) { + reference.name = replacement_name.clone(); + } + } + }); } diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 496613132c..77b9f2f0e9 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -777,11 +777,11 @@ fn types_in_expressions() { assert_eq!(output, expected); } -// #[test] -// fn set_hint() { -// let f = "asm/set_hint.asm"; -// regular_test(f, Default::default()); -// } +#[test] +fn set_hint() { + let f = "asm/set_hint.asm"; + regular_test(f, Default::default()); +} #[test] fn expand_fixed_jit() { From 3c378a32e84f2880be2a05172c5d7079992d6e93 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Tue, 19 Nov 2024 11:34:46 -0300 Subject: [PATCH 15/44] Docs, msgs, unused imports, etc --- pilopt/src/lib.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 68f5ec0017..7dbc06930d 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -3,7 +3,6 @@ use std::cmp::Ordering; use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; -use std::hash::Hash; use powdr_ast::analyzed::{ AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression, AlgebraicReference, @@ -492,7 +491,7 @@ fn constrained_to_constant( None } -/// Removes identities that evaluate to zero, the same column and lookups with empty columns. +/// Removes identities that evaluate to zero (including constraints of the form "X = X") and lookups with empty columns. fn remove_trivial_identities(pil_file: &mut Analyzed) { let to_remove = pil_file .identities @@ -653,7 +652,8 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { } /// Identifies witness columns that are directly constrained to be equal to other witness columns -/// through polynomial identities of the form "x = y". +/// through polynomial identities of the form "x = y" and returns a tuple ((name, id), (name, id)) +/// for each pair of identified columns fn equal_constrained( expression: &AlgebraicExpression, ) -> Option<((String, PolyID), (String, PolyID))> { From d8cbf75567b22055804f9d635ce7621c5bf16a6c Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Tue, 19 Nov 2024 13:18:17 -0300 Subject: [PATCH 16/44] set_hint? --- pipeline/tests/asm.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index d05fafddfc..21ec97e953 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -785,11 +785,11 @@ fn types_in_expressions() { assert_eq!(output, expected); } -#[test] -fn set_hint() { - let f = "asm/set_hint.asm"; - regular_test(f, Default::default()); -} +// #[test] +// fn set_hint() { +// let f = "asm/set_hint.asm"; +// regular_test(f, Default::default()); +// } #[test] fn expand_fixed_jit() { From 19aca283213f81415abf4637e5c18196530cdc85 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 20 Nov 2024 12:02:42 -0300 Subject: [PATCH 17/44] avoid get values from *_const in RISCV when pilopt removed them --- pilopt/src/lib.rs | 22 +++++++++++----------- riscv-executor/src/lib.rs | 24 ++++++++++++++++++++---- 2 files changed, 31 insertions(+), 15 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 7dbc06930d..c7d0f4d5ca 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -167,13 +167,6 @@ fn collect_required_symbols<'a, T: FieldElement>( } }); } - for (name, (sym, def)) in &pil_file.definitions { - if let SymbolKind::Poly(PolynomialType::Committed) = &sym.kind { - if def.is_some() { - required_names.insert(name.into()); - } - } - } required_names } @@ -672,10 +665,17 @@ fn equal_constrained( && right_ref.is_witness() && !right_ref.next { - Some(( - (left_ref.name.clone(), left_ref.poly_id), - (right_ref.name.clone(), right_ref.poly_id), - )) + if left_ref.poly_id > right_ref.poly_id { + Some(( + (left_ref.name.clone(), left_ref.poly_id), + (right_ref.name.clone(), right_ref.poly_id), + )) + } else { + Some(( + (right_ref.name.clone(), right_ref.poly_id), + (left_ref.name.clone(), left_ref.poly_id), + )) + } } else { None } diff --git a/riscv-executor/src/lib.rs b/riscv-executor/src/lib.rs index 0d0b00b3aa..49aad42625 100644 --- a/riscv-executor/src/lib.rs +++ b/riscv-executor/src/lib.rs @@ -626,6 +626,10 @@ mod builder { } } + pub fn col_is_defined(&self, name: &str) -> bool { + self.trace.cols.get(name).is_some() + } + pub fn push_row(&mut self) { if let ExecMode::Trace = self.mode { self.trace @@ -1039,10 +1043,22 @@ impl<'a, 'b, F: FieldElement> Executor<'a, 'b, F> { self.proc.backup_reg_mem(); - set_col!(X, get_col!(X_const)); - set_col!(Y, get_col!(Y_const)); - set_col!(Z, get_col!(Z_const)); - set_col!(W, get_col!(W_const)); + if self.proc.col_is_defined("X_const") { + set_col!(X, get_col!(X_const)); + } + + if self.proc.col_is_defined("Y_const") { + set_col!(Y, get_col!(Y_const)); + } + + if self.proc.col_is_defined("Z_const") { + set_col!(Z, get_col!(Z_const)); + } + + if self.proc.col_is_defined("W_const") { + set_col!(W, get_col!(W_const)); + } + self.proc .set_col(&format!("main::instr_{name}"), Elem::from_u32_as_fe(1)); From a4f6a4ec855f79bbe93acd0f6ce0abf2d73c4fb8 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 20 Nov 2024 12:19:19 -0300 Subject: [PATCH 18/44] contains_key --- riscv-executor/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/riscv-executor/src/lib.rs b/riscv-executor/src/lib.rs index 49aad42625..5498ef1a68 100644 --- a/riscv-executor/src/lib.rs +++ b/riscv-executor/src/lib.rs @@ -627,7 +627,7 @@ mod builder { } pub fn col_is_defined(&self, name: &str) -> bool { - self.trace.cols.get(name).is_some() + self.trace.cols.contains_key(name) } pub fn push_row(&mut self) { From 906a75bec96641f9e21a2f10a909e91df707dff1 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 20 Nov 2024 12:54:55 -0300 Subject: [PATCH 19/44] fix output --- pilopt/tests/optimizer.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index 3d601bd92a..d67bce5249 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -15,8 +15,8 @@ fn replace_fixed() { one * Y = zero * Y + 7 * X; "#; let expectation = r#"namespace N(65536); - col witness Y; - N::Y = 7 * N::Y; + col witness X; + N::X = 7 * N::X; "#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); From af1f67980c3c3711c4fb0b8739bb2626a2756c6b Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 20 Nov 2024 13:01:46 -0300 Subject: [PATCH 20/44] change set_hint() test to avoid opt --- pipeline/tests/asm.rs | 10 +++++----- test_data/asm/set_hint.asm | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 21ec97e953..d05fafddfc 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -785,11 +785,11 @@ fn types_in_expressions() { assert_eq!(output, expected); } -// #[test] -// fn set_hint() { -// let f = "asm/set_hint.asm"; -// regular_test(f, Default::default()); -// } +#[test] +fn set_hint() { + let f = "asm/set_hint.asm"; + regular_test(f, Default::default()); +} #[test] fn expand_fixed_jit() { diff --git a/test_data/asm/set_hint.asm b/test_data/asm/set_hint.asm index cd25283d73..f52ee78412 100644 --- a/test_data/asm/set_hint.asm +++ b/test_data/asm/set_hint.asm @@ -7,5 +7,5 @@ let new_col_with_hint: -> expr = constr || { machine Main with degree: 4 { let x; let w = new_col_with_hint(); - x = w; + x = w + 1; } \ No newline at end of file From be6f87bacb8b98a46568e6a7367c5cbc248b698a Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 20 Nov 2024 14:01:23 -0300 Subject: [PATCH 21/44] minor fix --- pilopt/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index c7d0f4d5ca..1d6db59cb8 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -358,8 +358,6 @@ fn extract_constant_lookups(pil_file: &mut Analyzed) { if let AlgebraicExpression::Number(n) = r { Some((i, (l, n))) } else { - // Otherwise the constraint is not satisfiable, - // but better to get the error elsewhere. None } }) @@ -496,6 +494,8 @@ fn remove_trivial_identities(pil_file: &mut Analyzed) { if *n == 0.into() { Some(index) } else { + // Otherwise the constraint is not satisfiable, + // but better to get the error elsewhere. None } } From a8f08649e65094e63d11c4c0abe99e64d96a324a Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 20 Nov 2024 14:02:41 -0300 Subject: [PATCH 22/44] empty spaces & minor details --- pilopt/src/lib.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 1d6db59cb8..4159d0b360 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -167,7 +167,6 @@ fn collect_required_symbols<'a, T: FieldElement>( } }); } - required_names } From 83a8b887cbfca2a350764082c02ca766382efd34 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 20 Nov 2024 15:26:41 -0300 Subject: [PATCH 23/44] namespace & try_get_col --- riscv-executor/src/lib.rs | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/riscv-executor/src/lib.rs b/riscv-executor/src/lib.rs index 5498ef1a68..959291fb63 100644 --- a/riscv-executor/src/lib.rs +++ b/riscv-executor/src/lib.rs @@ -626,8 +626,16 @@ mod builder { } } - pub fn col_is_defined(&self, name: &str) -> bool { - self.trace.cols.contains_key(name) + pub fn try_get_col(&self, name: &str) -> Option> { + if let ExecMode::Trace = self.mode { + self.trace + .cols + .get(name) + .and_then(|col| col.last()) + .map(|v| *v) + } else { + None + } } pub fn push_row(&mut self) { @@ -1043,19 +1051,19 @@ impl<'a, 'b, F: FieldElement> Executor<'a, 'b, F> { self.proc.backup_reg_mem(); - if self.proc.col_is_defined("X_const") { + if self.proc.try_get_col("main::X_const").is_some() { set_col!(X, get_col!(X_const)); } - if self.proc.col_is_defined("Y_const") { + if self.proc.try_get_col("main::Y_const").is_some() { set_col!(Y, get_col!(Y_const)); } - if self.proc.col_is_defined("Z_const") { + if self.proc.try_get_col("main::Z_const").is_some() { set_col!(Z, get_col!(Z_const)); } - if self.proc.col_is_defined("W_const") { + if self.proc.try_get_col("main::W_const").is_some() { set_col!(W, get_col!(W_const)); } From 2622366c5402c73beb18995b050d96a63f38f8b4 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 20 Nov 2024 15:45:48 -0300 Subject: [PATCH 24/44] avoid double call --- riscv-executor/src/lib.rs | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/riscv-executor/src/lib.rs b/riscv-executor/src/lib.rs index 959291fb63..833e798998 100644 --- a/riscv-executor/src/lib.rs +++ b/riscv-executor/src/lib.rs @@ -632,7 +632,7 @@ mod builder { .cols .get(name) .and_then(|col| col.last()) - .map(|v| *v) + .copied() } else { None } @@ -1051,22 +1051,21 @@ impl<'a, 'b, F: FieldElement> Executor<'a, 'b, F> { self.proc.backup_reg_mem(); - if self.proc.try_get_col("main::X_const").is_some() { - set_col!(X, get_col!(X_const)); + if let Some(x_const) = self.proc.try_get_col("main::X_const") { + set_col!(X, x_const); } - if self.proc.try_get_col("main::Y_const").is_some() { - set_col!(Y, get_col!(Y_const)); + if let Some(y_const) = self.proc.try_get_col("main::Y_const") { + set_col!(Y, y_const); } - if self.proc.try_get_col("main::Z_const").is_some() { - set_col!(Z, get_col!(Z_const)); + if let Some(z_const) = self.proc.try_get_col("main::Z_const") { + set_col!(Z, z_const); } - if self.proc.try_get_col("main::W_const").is_some() { - set_col!(W, get_col!(W_const)); + if let Some(w_const) = self.proc.try_get_col("main::W_const") { + set_col!(W, w_const); } - self.proc .set_col(&format!("main::instr_{name}"), Elem::from_u32_as_fe(1)); From 239d57363915172d07f6af374fa16d4bac687703 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 21 Nov 2024 10:39:20 -0300 Subject: [PATCH 25/44] more tests --- pilopt/tests/optimizer.rs | 52 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index d67bce5249..ba8b513169 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -335,3 +335,55 @@ fn handle_array_references_in_prover_functions() { let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); } + +#[test] +fn equal_constrained_array_elements_empty() { + let input = r#"namespace N(65536); + col witness w[20]; + w[4] = w[7]; + "#; + let expectation = r#""#; + let optimized = optimize(analyze_string::(input).unwrap()).to_string(); + assert_eq!(optimized, expectation); +} + +#[test] +fn equal_constrained_array_elements_query() { + let input = r#"namespace N(65536); + col witness w[20]; + w[4] = w[7]; + query |i| { + let _ = w[4] + w[7] - w[5]; + }; + "#; + let expectation = r#"namespace N(65536); + col witness w[20]; + query |i| { + let _: expr = N::w[4_int] + N::w[7_int] - N::w[5_int]; + }; +"#; + let optimized = optimize(analyze_string::(input).unwrap()).to_string(); + assert_eq!(optimized, expectation); +} + +#[test] +fn equal_constrained_array_elements() { + let input = r#"namespace N(65536); + col witness w[20]; + w[4] = w[7]; + w[3] = w[5]; + w[7] + w[1] = 5; + query |i| { + let value = w[4] + w[7] - w[5]; + }; + "#; + let expectation = r#"namespace N(65536); + col witness w[20]; + N::w[4] + N::w[1] = 5; + query |i| { + let value: expr = N::w[4_int] + N::w[7_int] - N::w[5_int]; + }; +"#; + let optimized = optimize(analyze_string::(input).unwrap()).to_string(); + assert_eq!(optimized, expectation); +} \ No newline at end of file From dfc942416d5dce3d39936f962f307575fc6083d0 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 21 Nov 2024 10:54:44 -0300 Subject: [PATCH 26/44] avoid array elem --- pilopt/src/lib.rs | 6 +++++- pilopt/tests/optimizer.rs | 20 ++++++++++---------- 2 files changed, 15 insertions(+), 11 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 4159d0b360..f1866ac610 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -648,6 +648,7 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { /// for each pair of identified columns fn equal_constrained( expression: &AlgebraicExpression, + poly_id_to_definition_name: &BTreeMap, ) -> Option<((String, PolyID), (String, PolyID))> { match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -663,6 +664,8 @@ fn equal_constrained( && !left_ref.next && right_ref.is_witness() && !right_ref.next + && !poly_id_to_definition_name.contains_key(&left_ref.poly_id) + && !poly_id_to_definition_name.contains_key(&right_ref.poly_id) { if left_ref.poly_id > right_ref.poly_id { Some(( @@ -686,12 +689,13 @@ fn equal_constrained( } fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { + let poly_id_to_definition_name = build_poly_id_to_definition_name_lookup(pil_file); let substitutions: Vec<_> = pil_file .identities .iter() .filter_map(|id| { if let Identity::Polynomial(PolynomialIdentity { expression, .. }) = id { - equal_constrained(expression) + equal_constrained(expression, &poly_id_to_definition_name) } else { None } diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index ba8b513169..8e0b9f2674 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -342,7 +342,10 @@ fn equal_constrained_array_elements_empty() { col witness w[20]; w[4] = w[7]; "#; - let expectation = r#""#; + let expectation = r#"namespace N(65536); + col witness w[20]; + N::w[4] = N::w[7]; +"#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); } @@ -358,6 +361,7 @@ fn equal_constrained_array_elements_query() { "#; let expectation = r#"namespace N(65536); col witness w[20]; + N::w[4] = N::w[7]; query |i| { let _: expr = N::w[4_int] + N::w[7_int] - N::w[5_int]; }; @@ -372,18 +376,14 @@ fn equal_constrained_array_elements() { col witness w[20]; w[4] = w[7]; w[3] = w[5]; - w[7] + w[1] = 5; - query |i| { - let value = w[4] + w[7] - w[5]; - }; + w[7] + w[5] = 5; "#; let expectation = r#"namespace N(65536); col witness w[20]; - N::w[4] + N::w[1] = 5; - query |i| { - let value: expr = N::w[4_int] + N::w[7_int] - N::w[5_int]; - }; + N::w[4] = N::w[7]; + N::w[3] = N::w[5]; + N::w[7] + N::w[5] = 5; "#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); -} \ No newline at end of file +} From dde999a30404bebb675bdd5d46cebc95c3b8fefd Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 21 Nov 2024 12:14:11 -0300 Subject: [PATCH 27/44] names --- ast/src/analyzed/mod.rs | 18 ++++++++++++++++++ pilopt/src/lib.rs | 34 +++++++++++++++++++++++++++------- pilopt/tests/optimizer.rs | 4 ++-- 3 files changed, 47 insertions(+), 9 deletions(-) diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index c2dd00da3c..aaf1b7828b 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -759,6 +759,24 @@ impl Symbol { }) } + /// Returns an iterator producing either an empty iterator (if it is not an array), + /// or all the elements of the array with their names in the form `array[index]`. + pub fn array_elements_only(&self) -> impl Iterator + '_ { + let SymbolKind::Poly(ptype) = self.kind else { + panic!("Expected polynomial."); + }; + let length = self.length.unwrap_or(0); + (0..length).map(move |i| { + ( + self.array_element_name(i), + PolyID { + id: self.id + i, + ptype, + }, + ) + }) + } + /// Returns "name[index]" if this is an array or just "name" otherwise. /// In the second case, requires index to be zero and otherwise /// requires index to be less than length. diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index f1866ac610..50a1747159 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -120,8 +120,8 @@ fn remove_unreferenced_definitions(pil_file: &mut Analyzed) pil_file.remove_trait_impls(&impls_to_remove); } -/// Builds a lookup-table that can be used to turn array elements -/// (in form of their poly ids) into the names of the arrays. +/// Builds a lookup-table that can be used to turn all symbols +/// (including array elements) in the form of their poly ids, into the names of the symbols. fn build_poly_id_to_definition_name_lookup( pil_file: &Analyzed, ) -> BTreeMap { @@ -141,6 +141,26 @@ fn build_poly_id_to_definition_name_lookup( poly_id_to_definition_name } +/// Builds a lookup-table that can be used to turn array elements +/// (in form of their poly ids) into the names of the arrays. +fn build_poly_id_to_array_elem_lookup( + pil_file: &Analyzed, +) -> BTreeMap { + let mut poly_id_to_definition_name = BTreeMap::new(); + for (name, (symbol, _)) in &pil_file.definitions { + if matches!(symbol.kind, SymbolKind::Poly(_)) { + symbol.array_elements_only().for_each(|(_, id)| { + poly_id_to_definition_name.insert(id, name); + }); + } + } + for (name, (symbol, _)) in &pil_file.intermediate_columns { + symbol.array_elements_only().for_each(|(_, id)| { + poly_id_to_definition_name.insert(id, name); + }); + } + poly_id_to_definition_name +} /// Collect all names that are referenced in identities and public declarations. fn collect_required_symbols<'a, T: FieldElement>( pil_file: &'a Analyzed, @@ -648,7 +668,7 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { /// for each pair of identified columns fn equal_constrained( expression: &AlgebraicExpression, - poly_id_to_definition_name: &BTreeMap, + poly_id_to_array_elem: &BTreeMap, ) -> Option<((String, PolyID), (String, PolyID))> { match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -664,8 +684,8 @@ fn equal_constrained( && !left_ref.next && right_ref.is_witness() && !right_ref.next - && !poly_id_to_definition_name.contains_key(&left_ref.poly_id) - && !poly_id_to_definition_name.contains_key(&right_ref.poly_id) + && !poly_id_to_array_elem.contains_key(&left_ref.poly_id) + && !poly_id_to_array_elem.contains_key(&right_ref.poly_id) { if left_ref.poly_id > right_ref.poly_id { Some(( @@ -689,13 +709,13 @@ fn equal_constrained( } fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { - let poly_id_to_definition_name = build_poly_id_to_definition_name_lookup(pil_file); + let poly_id_to_array_elem = build_poly_id_to_array_elem_lookup(pil_file); let substitutions: Vec<_> = pil_file .identities .iter() .filter_map(|id| { if let Identity::Polynomial(PolynomialIdentity { expression, .. }) = id { - equal_constrained(expression, &poly_id_to_definition_name) + equal_constrained(expression, &poly_id_to_array_elem) } else { None } diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index 8e0b9f2674..4d0ec65189 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -376,13 +376,13 @@ fn equal_constrained_array_elements() { col witness w[20]; w[4] = w[7]; w[3] = w[5]; - w[7] + w[5] = 5; + w[7] + w[1] = 5; "#; let expectation = r#"namespace N(65536); col witness w[20]; N::w[4] = N::w[7]; N::w[3] = N::w[5]; - N::w[7] + N::w[5] = 5; + N::w[7] + N::w[1] = 5; "#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); From b4f485e74054e35a0e30b0f3446730ffe8f4a541 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 25 Nov 2024 11:06:09 -0300 Subject: [PATCH 28/44] Function simplification, new doc, etc --- ast/src/analyzed/mod.rs | 18 ----------- pilopt/src/lib.rs | 68 ++++++++++++++++++++--------------------- 2 files changed, 33 insertions(+), 53 deletions(-) diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index aaf1b7828b..c2dd00da3c 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -759,24 +759,6 @@ impl Symbol { }) } - /// Returns an iterator producing either an empty iterator (if it is not an array), - /// or all the elements of the array with their names in the form `array[index]`. - pub fn array_elements_only(&self) -> impl Iterator + '_ { - let SymbolKind::Poly(ptype) = self.kind else { - panic!("Expected polynomial."); - }; - let length = self.length.unwrap_or(0); - (0..length).map(move |i| { - ( - self.array_element_name(i), - PolyID { - id: self.id + i, - ptype, - }, - ) - }) - } - /// Returns "name[index]" if this is an array or just "name" otherwise. /// In the second case, requires index to be zero and otherwise /// requires index to be less than length. diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 50a1747159..6a97fb9f36 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -85,7 +85,7 @@ fn remove_unreferenced_definitions(pil_file: &mut Analyzed) Box::new(value.iter().flat_map(|v| { v.all_children().flat_map(|e| { if let AlgebraicExpression::Reference(AlgebraicReference { poly_id, .. }) = e { - Some(poly_id_to_definition_name[poly_id].into()) + Some(poly_id_to_definition_name[poly_id].0.into()) } else { None } @@ -122,49 +122,45 @@ fn remove_unreferenced_definitions(pil_file: &mut Analyzed) /// Builds a lookup-table that can be used to turn all symbols /// (including array elements) in the form of their poly ids, into the names of the symbols. +/// The boolean flag indicates whether the symbol belongs to an array or not fn build_poly_id_to_definition_name_lookup( pil_file: &Analyzed, -) -> BTreeMap { - let mut poly_id_to_definition_name = BTreeMap::new(); +) -> BTreeMap { + let mut poly_id_to_info = BTreeMap::new(); + for (name, (symbol, _)) in &pil_file.definitions { if matches!(symbol.kind, SymbolKind::Poly(_)) { - symbol.array_elements().for_each(|(_, id)| { - poly_id_to_definition_name.insert(id, name); - }); + if symbol.is_array() { + symbol.array_elements().for_each(|(_, id)| { + poly_id_to_info.insert(id, (name, true)); + }); + } else { + symbol.array_elements().for_each(|(_, id)| { + poly_id_to_info.insert(id, (name, false)); + }); + } } } - for (name, (symbol, _)) in &pil_file.intermediate_columns { - symbol.array_elements().for_each(|(_, id)| { - poly_id_to_definition_name.insert(id, name); - }); - } - poly_id_to_definition_name -} -/// Builds a lookup-table that can be used to turn array elements -/// (in form of their poly ids) into the names of the arrays. -fn build_poly_id_to_array_elem_lookup( - pil_file: &Analyzed, -) -> BTreeMap { - let mut poly_id_to_definition_name = BTreeMap::new(); - for (name, (symbol, _)) in &pil_file.definitions { - if matches!(symbol.kind, SymbolKind::Poly(_)) { - symbol.array_elements_only().for_each(|(_, id)| { - poly_id_to_definition_name.insert(id, name); + for (name, (symbol, _)) in &pil_file.intermediate_columns { + if symbol.is_array() { + symbol.array_elements().for_each(|(_, id)| { + poly_id_to_info.insert(id, (name, true)); + }); + } else { + symbol.array_elements().for_each(|(_, id)| { + poly_id_to_info.insert(id, (name, false)); }); } } - for (name, (symbol, _)) in &pil_file.intermediate_columns { - symbol.array_elements_only().for_each(|(_, id)| { - poly_id_to_definition_name.insert(id, name); - }); - } - poly_id_to_definition_name + + poly_id_to_info } + /// Collect all names that are referenced in identities and public declarations. fn collect_required_symbols<'a, T: FieldElement>( pil_file: &'a Analyzed, - poly_id_to_definition_name: &BTreeMap, + poly_id_to_definition_name: &BTreeMap, ) -> HashSet> { let mut required_names: HashSet> = Default::default(); required_names.extend( @@ -183,7 +179,7 @@ fn collect_required_symbols<'a, T: FieldElement>( for id in &pil_file.identities { id.pre_visit_expressions(&mut |e: &AlgebraicExpression| { if let AlgebraicExpression::Reference(AlgebraicReference { poly_id, .. }) = e { - required_names.insert(poly_id_to_definition_name[poly_id].into()); + required_names.insert(poly_id_to_definition_name[poly_id].0.into()); } }); } @@ -668,7 +664,7 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { /// for each pair of identified columns fn equal_constrained( expression: &AlgebraicExpression, - poly_id_to_array_elem: &BTreeMap, + poly_id_to_array_elem: &BTreeMap, ) -> Option<((String, PolyID), (String, PolyID))> { match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -684,8 +680,10 @@ fn equal_constrained( && !left_ref.next && right_ref.is_witness() && !right_ref.next - && !poly_id_to_array_elem.contains_key(&left_ref.poly_id) - && !poly_id_to_array_elem.contains_key(&right_ref.poly_id) + && poly_id_to_array_elem.contains_key(&left_ref.poly_id) + && poly_id_to_array_elem.contains_key(&right_ref.poly_id) + && !poly_id_to_array_elem.get(&right_ref.poly_id).unwrap().1 + && !poly_id_to_array_elem.get(&left_ref.poly_id).unwrap().1 { if left_ref.poly_id > right_ref.poly_id { Some(( @@ -709,7 +707,7 @@ fn equal_constrained( } fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { - let poly_id_to_array_elem = build_poly_id_to_array_elem_lookup(pil_file); + let poly_id_to_array_elem = build_poly_id_to_definition_name_lookup(pil_file); let substitutions: Vec<_> = pil_file .identities .iter() From b9cbcbe83ee3ae39462c4f0491ad3c98721edaee Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 29 Nov 2024 12:20:48 -0300 Subject: [PATCH 29/44] only update definitions --- ast/src/analyzed/mod.rs | 10 ++++++++++ pilopt/src/lib.rs | 2 +- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index a0e9bc6e48..413e854bc7 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -374,6 +374,16 @@ impl Analyzed { .for_each(|e| e.post_visit_expressions_mut(f)); } + pub fn post_visit_expressions_in_definitions_mut(&mut self, f: &mut F) + where + F: FnMut(&mut Expression), + { + self.definitions + .values_mut() + .filter_map(|(_poly, definition)| definition.as_mut()) + .for_each(|definition| definition.post_visit_expressions_mut(f)); + } + /// Retrieves (name, col_name, poly_id, offset, stage) of each public witness in the trace. pub fn get_publics(&self) -> Vec<(String, String, PolyID, usize, u8)> { let mut publics = self diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index d86a5c7eb4..930f37eab2 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -790,7 +790,7 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal } }); - pil_file.post_visit_expressions_mut(&mut |e: &mut Expression| { + pil_file.post_visit_expressions_in_definitions_mut(&mut |e: &mut Expression| { if let Expression::Reference(_, Reference::Poly(reference)) = e { if let Some((replacement_name, _)) = subs_by_name.get(&reference.name) { reference.name = replacement_name.clone(); From 32e74efc41328210232fb5eab2dffd1503e828fb Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 29 Nov 2024 16:11:29 -0300 Subject: [PATCH 30/44] back --- ast/src/analyzed/mod.rs | 10 ---------- pilopt/src/lib.rs | 25 +++++++++++++++++++++++-- 2 files changed, 23 insertions(+), 12 deletions(-) diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index 413e854bc7..a0e9bc6e48 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -374,16 +374,6 @@ impl Analyzed { .for_each(|e| e.post_visit_expressions_mut(f)); } - pub fn post_visit_expressions_in_definitions_mut(&mut self, f: &mut F) - where - F: FnMut(&mut Expression), - { - self.definitions - .values_mut() - .filter_map(|(_poly, definition)| definition.as_mut()) - .for_each(|definition| definition.post_visit_expressions_mut(f)); - } - /// Retrieves (name, col_name, poly_id, offset, stage) of each public witness in the trace. pub fn get_publics(&self) -> Vec<(String, String, PolyID, usize, u8)> { let mut publics = self diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 930f37eab2..48a18edcc7 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -764,7 +764,12 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal .iter() .filter_map(|id| { if let Identity::Polynomial(PolynomialIdentity { expression, .. }) = id { - equal_constrained(expression, &poly_id_to_array_elem) + let r = equal_constrained(expression, &poly_id_to_array_elem); + if r.is_some() { + println!("Expr {expression:?} para {:?}", r.clone().unwrap()); + } + + r } else { None } @@ -781,18 +786,34 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal .map(|((name, _), to_keep)| (name, to_keep)) .collect(); + println!("Substitutions {substitutions:?}"); + pil_file.post_visit_expressions_in_identities_mut(&mut |e: &mut AlgebraicExpression<_>| { if let AlgebraicExpression::Reference(ref mut reference) = e { if let Some((replacement_name, replacement_id)) = subs_by_id.get(&reference.poly_id) { + println!( + "Iden ID: Sale {:?}, entra {:?}", + reference.poly_id, replacement_id + ); + println!( + "Iden Name: Sale {:?}, entra {:?}", + reference.name, + replacement_name.clone() + ); reference.poly_id = *replacement_id; reference.name = replacement_name.clone(); } } }); - pil_file.post_visit_expressions_in_definitions_mut(&mut |e: &mut Expression| { + pil_file.post_visit_expressions_mut(&mut |e: &mut Expression| { if let Expression::Reference(_, Reference::Poly(reference)) = e { if let Some((replacement_name, _)) = subs_by_name.get(&reference.name) { + println!( + "Def Name: Sale {:?}, entra {:?}", + reference.name, + replacement_name.clone() + ); reference.name = replacement_name.clone(); } } From ba335e8e0068600509c129d415c60cadacd6c759 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 29 Nov 2024 16:17:14 -0300 Subject: [PATCH 31/44] missed println --- pilopt/src/lib.rs | 23 +---------------------- 1 file changed, 1 insertion(+), 22 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 48a18edcc7..d86a5c7eb4 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -764,12 +764,7 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal .iter() .filter_map(|id| { if let Identity::Polynomial(PolynomialIdentity { expression, .. }) = id { - let r = equal_constrained(expression, &poly_id_to_array_elem); - if r.is_some() { - println!("Expr {expression:?} para {:?}", r.clone().unwrap()); - } - - r + equal_constrained(expression, &poly_id_to_array_elem) } else { None } @@ -786,20 +781,9 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal .map(|((name, _), to_keep)| (name, to_keep)) .collect(); - println!("Substitutions {substitutions:?}"); - pil_file.post_visit_expressions_in_identities_mut(&mut |e: &mut AlgebraicExpression<_>| { if let AlgebraicExpression::Reference(ref mut reference) = e { if let Some((replacement_name, replacement_id)) = subs_by_id.get(&reference.poly_id) { - println!( - "Iden ID: Sale {:?}, entra {:?}", - reference.poly_id, replacement_id - ); - println!( - "Iden Name: Sale {:?}, entra {:?}", - reference.name, - replacement_name.clone() - ); reference.poly_id = *replacement_id; reference.name = replacement_name.clone(); } @@ -809,11 +793,6 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal pil_file.post_visit_expressions_mut(&mut |e: &mut Expression| { if let Expression::Reference(_, Reference::Poly(reference)) = e { if let Some((replacement_name, _)) = subs_by_name.get(&reference.name) { - println!( - "Def Name: Sale {:?}, entra {:?}", - reference.name, - replacement_name.clone() - ); reference.name = replacement_name.clone(); } } From a86bd851b7c98e4e82a6ec42adbd08ca39c90810 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 2 Dec 2024 13:27:31 -0300 Subject: [PATCH 32/44] test estark --- pilopt/src/lib.rs | 47 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 45 insertions(+), 2 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index d86a5c7eb4..a83e0d69cd 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -9,7 +9,7 @@ use powdr_ast::analyzed::{ AlgebraicUnaryOperation, AlgebraicUnaryOperator, Analyzed, ConnectIdentity, Expression, FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PhantomLookupIdentity, PhantomPermutationIdentity, PolyID, PolynomialIdentity, PolynomialReference, PolynomialType, - Reference, Symbol, SymbolKind, + Reference, SelectedExpressions, Symbol, SymbolKind, }; use powdr_ast::parsed::types::Type; use powdr_ast::parsed::visitor::{AllChildren, Children, ExpressionVisitable}; @@ -716,6 +716,7 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { fn equal_constrained( expression: &AlgebraicExpression, poly_id_to_array_elem: &BTreeMap, + imported_columns: &HashSet, ) -> Option<((String, PolyID), (String, PolyID))> { match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -735,6 +736,8 @@ fn equal_constrained( && poly_id_to_array_elem.contains_key(&right_ref.poly_id) && !poly_id_to_array_elem.get(&right_ref.poly_id).unwrap().1 && !poly_id_to_array_elem.get(&left_ref.poly_id).unwrap().1 + && !imported_columns.contains(&left_ref.name) + && !imported_columns.contains(&right_ref.name) { if left_ref.poly_id > right_ref.poly_id { Some(( @@ -759,12 +762,13 @@ fn equal_constrained( fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { let poly_id_to_array_elem = build_poly_id_to_definition_name_lookup(pil_file); + let imported_columns = vars_in_identities(pil_file); let substitutions: Vec<_> = pil_file .identities .iter() .filter_map(|id| { if let Identity::Polynomial(PolynomialIdentity { expression, .. }) = id { - equal_constrained(expression, &poly_id_to_array_elem) + equal_constrained(expression, &poly_id_to_array_elem, &imported_columns) } else { None } @@ -798,3 +802,42 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal } }); } +fn vars_in_identities(pil_file: &Analyzed) -> HashSet { + pil_file + .identities + .iter() + .filter_map(|id| match id { + Identity::Lookup(LookupIdentity { + id, + source, + left, + right, + }) => Some( + vars_in_selected_expressions(left) + .chain(vars_in_selected_expressions(right)) + .collect::>(), + ), + _ => None, + }) + .flatten() + .collect() +} + +fn vars_in_selected_expressions( + selected_expr: &SelectedExpressions, +) -> impl Iterator + '_ { + let SelectedExpressions { + selector, + expressions, + } = selected_expr; + + expressions.iter().flat_map(|expr| { + expr.all_children() + .filter_map(|child| match child { + AlgebraicExpression::Reference(reference) => Some(reference.name.clone()), + AlgebraicExpression::PublicReference(preference) => Some(preference.clone()), + _ => None, + }) + .collect::>() + }) +} From 5d070be7b72f035cfbb8c2dbddb4d2f92c165946 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 2 Dec 2024 13:34:33 -0300 Subject: [PATCH 33/44] lint --- pilopt/src/lib.rs | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index a83e0d69cd..31ed31b413 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -807,12 +807,7 @@ fn vars_in_identities(pil_file: &Analyzed) -> HashSet Some( + Identity::Lookup(LookupIdentity { left, right, .. }) => Some( vars_in_selected_expressions(left) .chain(vars_in_selected_expressions(right)) .collect::>(), @@ -826,10 +821,7 @@ fn vars_in_identities(pil_file: &Analyzed) -> HashSet( selected_expr: &SelectedExpressions, ) -> impl Iterator + '_ { - let SelectedExpressions { - selector, - expressions, - } = selected_expr; + let SelectedExpressions { expressions, .. } = selected_expr; expressions.iter().flat_map(|expr| { expr.all_children() From ecde3319701a6457afa5582c08f3674facb198b0 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 2 Dec 2024 13:51:25 -0300 Subject: [PATCH 34/44] removed from lookups --- pilopt/src/lib.rs | 42 +++++++++++++++++++----------------------- 1 file changed, 19 insertions(+), 23 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 31ed31b413..2081aa85e9 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -762,7 +762,7 @@ fn equal_constrained( fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { let poly_id_to_array_elem = build_poly_id_to_definition_name_lookup(pil_file); - let imported_columns = vars_in_identities(pil_file); + let imported_columns = cols_in_identity_lookup(pil_file); let substitutions: Vec<_> = pil_file .identities .iter() @@ -802,34 +802,30 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal } }); } -fn vars_in_identities(pil_file: &Analyzed) -> HashSet { +fn cols_in_identity_lookup(pil_file: &Analyzed) -> HashSet { pil_file .identities .iter() .filter_map(|id| match id { - Identity::Lookup(LookupIdentity { left, right, .. }) => Some( - vars_in_selected_expressions(left) - .chain(vars_in_selected_expressions(right)) - .collect::>(), - ), + Identity::Lookup(LookupIdentity { left, .. }) => { + let SelectedExpressions { expressions, .. } = left; + Some(expressions.iter().flat_map(|expr| { + expr.all_children() + .filter_map(|child| match child { + AlgebraicExpression::Reference(reference) => { + Some(reference.name.clone()) + } + AlgebraicExpression::PublicReference(preference) => { + Some(preference.clone()) + } + _ => None, + }) + .collect::>() + })) + } + // Identity::Permutation(PermutationIdentity { left, .. }) => { } _ => None, }) .flatten() .collect() } - -fn vars_in_selected_expressions( - selected_expr: &SelectedExpressions, -) -> impl Iterator + '_ { - let SelectedExpressions { expressions, .. } = selected_expr; - - expressions.iter().flat_map(|expr| { - expr.all_children() - .filter_map(|child| match child { - AlgebraicExpression::Reference(reference) => Some(reference.name.clone()), - AlgebraicExpression::PublicReference(preference) => Some(preference.clone()), - _ => None, - }) - .collect::>() - }) -} From 8019fc46bfe4e57f2e49a5762c959df019b04daf Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 2 Dec 2024 15:13:19 -0300 Subject: [PATCH 35/44] cols in lookup & better code --- pilopt/src/lib.rs | 79 +++++++++++++++++---------------------- pilopt/tests/optimizer.rs | 18 +++++++++ 2 files changed, 53 insertions(+), 44 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 2081aa85e9..a05b92f7e3 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -716,7 +716,7 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { fn equal_constrained( expression: &AlgebraicExpression, poly_id_to_array_elem: &BTreeMap, - imported_columns: &HashSet, + cols_in_lookups: &HashSet, ) -> Option<((String, PolyID), (String, PolyID))> { match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -724,32 +724,26 @@ fn equal_constrained( op: AlgebraicBinaryOperator::Sub, right, }) => match (left.as_ref(), right.as_ref()) { - ( - AlgebraicExpression::Reference(left_ref), - AlgebraicExpression::Reference(right_ref), - ) => { - if left_ref.is_witness() - && !left_ref.next - && right_ref.is_witness() - && !right_ref.next - && poly_id_to_array_elem.contains_key(&left_ref.poly_id) - && poly_id_to_array_elem.contains_key(&right_ref.poly_id) - && !poly_id_to_array_elem.get(&right_ref.poly_id).unwrap().1 - && !poly_id_to_array_elem.get(&left_ref.poly_id).unwrap().1 - && !imported_columns.contains(&left_ref.name) - && !imported_columns.contains(&right_ref.name) - { - if left_ref.poly_id > right_ref.poly_id { - Some(( - (left_ref.name.clone(), left_ref.poly_id), - (right_ref.name.clone(), right_ref.poly_id), - )) + (AlgebraicExpression::Reference(l), AlgebraicExpression::Reference(r)) => { + let l_valid = l.is_witness() + && !l.next + && poly_id_to_array_elem + .get(&l.poly_id) + .map_or(false, |&(_, b)| !b); + let r_valid = r.is_witness() + && !r.next + && poly_id_to_array_elem + .get(&r.poly_id) + .map_or(false, |&(_, b)| !b); + let not_in_lookups = + !cols_in_lookups.contains(&l.name) && !cols_in_lookups.contains(&r.name); + + if l_valid && r_valid && not_in_lookups { + Some(if l.poly_id > r.poly_id { + ((l.name.clone(), l.poly_id), (r.name.clone(), r.poly_id)) } else { - Some(( - (right_ref.name.clone(), right_ref.poly_id), - (left_ref.name.clone(), left_ref.poly_id), - )) - } + ((r.name.clone(), r.poly_id), (l.name.clone(), l.poly_id)) + }) } else { None } @@ -762,13 +756,13 @@ fn equal_constrained( fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { let poly_id_to_array_elem = build_poly_id_to_definition_name_lookup(pil_file); - let imported_columns = cols_in_identity_lookup(pil_file); + let cols_in_lookups = cols_in_identity_lookup(pil_file); let substitutions: Vec<_> = pil_file .identities .iter() .filter_map(|id| { if let Identity::Polynomial(PolynomialIdentity { expression, .. }) = id { - equal_constrained(expression, &poly_id_to_array_elem, &imported_columns) + equal_constrained(expression, &poly_id_to_array_elem, &cols_in_lookups) } else { None } @@ -807,25 +801,22 @@ fn cols_in_identity_lookup(pil_file: &Analyzed) -> HashSet { - let SelectedExpressions { expressions, .. } = left; - Some(expressions.iter().flat_map(|expr| { - expr.all_children() - .filter_map(|child| match child { - AlgebraicExpression::Reference(reference) => { - Some(reference.name.clone()) - } - AlgebraicExpression::PublicReference(preference) => { - Some(preference.clone()) - } - _ => None, - }) - .collect::>() - })) + Identity::Lookup(LookupIdentity { left, right, .. }) => { + Some(extract_references(left).chain(extract_references(right))) } - // Identity::Permutation(PermutationIdentity { left, .. }) => { } _ => None, }) .flatten() .collect() } +fn extract_references( + selected_expr: &SelectedExpressions, +) -> impl Iterator + '_ { + selected_expr.expressions.iter().flat_map(|expr| { + expr.all_children().filter_map(|child| match child { + AlgebraicExpression::Reference(reference) => Some(reference.name.clone()), + AlgebraicExpression::PublicReference(preference) => Some(preference.clone()), + _ => None, + }) + }) +} diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index 18a83a1fb2..bc9c4e37ef 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -425,3 +425,21 @@ fn equal_constrained_array_elements() { let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); } + +#[test] +fn equal_constrained_identity() { + let input = r#"namespace N(65536); + col witness w; + col witness v; + w = v; + [w] in [v]; + "#; + let expectation = r#"namespace N(65536); + col witness w; + col witness v; + N::w = N::v; + [N::w] in [N::v]; +"#; + let optimized = optimize(analyze_string::(input).unwrap()).to_string(); + assert_eq!(optimized, expectation); +} From 0b3e774397b32e351d7b0f895166aea4eb6a5074 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 2 Dec 2024 16:18:53 -0300 Subject: [PATCH 36/44] toopt, removed --- pilopt/src/lib.rs | 56 ++++++++++++++++++--------------------- pilopt/tests/optimizer.rs | 18 ------------- 2 files changed, 26 insertions(+), 48 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index a05b92f7e3..0832fea844 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -716,7 +716,6 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { fn equal_constrained( expression: &AlgebraicExpression, poly_id_to_array_elem: &BTreeMap, - cols_in_lookups: &HashSet, ) -> Option<((String, PolyID), (String, PolyID))> { match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -735,10 +734,8 @@ fn equal_constrained( && poly_id_to_array_elem .get(&r.poly_id) .map_or(false, |&(_, b)| !b); - let not_in_lookups = - !cols_in_lookups.contains(&l.name) && !cols_in_lookups.contains(&r.name); - if l_valid && r_valid && not_in_lookups { + if l_valid && r_valid { Some(if l.poly_id > r.poly_id { ((l.name.clone(), l.poly_id), (r.name.clone(), r.poly_id)) } else { @@ -756,13 +753,12 @@ fn equal_constrained( fn remove_equal_constrained_witness_columns(pil_file: &mut Analyzed) { let poly_id_to_array_elem = build_poly_id_to_definition_name_lookup(pil_file); - let cols_in_lookups = cols_in_identity_lookup(pil_file); let substitutions: Vec<_> = pil_file .identities .iter() .filter_map(|id| { if let Identity::Polynomial(PolynomialIdentity { expression, .. }) = id { - equal_constrained(expression, &poly_id_to_array_elem, &cols_in_lookups) + equal_constrained(expression, &poly_id_to_array_elem) } else { None } @@ -796,27 +792,27 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal } }); } -fn cols_in_identity_lookup(pil_file: &Analyzed) -> HashSet { - pil_file - .identities - .iter() - .filter_map(|id| match id { - Identity::Lookup(LookupIdentity { left, right, .. }) => { - Some(extract_references(left).chain(extract_references(right))) - } - _ => None, - }) - .flatten() - .collect() -} -fn extract_references( - selected_expr: &SelectedExpressions, -) -> impl Iterator + '_ { - selected_expr.expressions.iter().flat_map(|expr| { - expr.all_children().filter_map(|child| match child { - AlgebraicExpression::Reference(reference) => Some(reference.name.clone()), - AlgebraicExpression::PublicReference(preference) => Some(preference.clone()), - _ => None, - }) - }) -} +// fn cols_in_identity_lookup(pil_file: &Analyzed) -> HashSet { +// pil_file +// .identities +// .iter() +// .filter_map(|id| match id { +// Identity::Lookup(LookupIdentity { left, right, .. }) => { +// Some(extract_references(left).chain(extract_references(right))) +// } +// _ => None, +// }) +// .flatten() +// .collect() +// } +// fn extract_references( +// selected_expr: &SelectedExpressions, +// ) -> impl Iterator + '_ { +// selected_expr.expressions.iter().flat_map(|expr| { +// expr.all_children().filter_map(|child| match child { +// AlgebraicExpression::Reference(reference) => Some(reference.name.clone()), +// AlgebraicExpression::PublicReference(preference) => Some(preference.clone()), +// _ => None, +// }) +// }) +// } diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index bc9c4e37ef..18a83a1fb2 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -425,21 +425,3 @@ fn equal_constrained_array_elements() { let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); } - -#[test] -fn equal_constrained_identity() { - let input = r#"namespace N(65536); - col witness w; - col witness v; - w = v; - [w] in [v]; - "#; - let expectation = r#"namespace N(65536); - col witness w; - col witness v; - N::w = N::v; - [N::w] in [N::v]; -"#; - let optimized = optimize(analyze_string::(input).unwrap()).to_string(); - assert_eq!(optimized, expectation); -} From 79d3d80c5fbdc580bfc29ce9e605eb3ce098b263 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 2 Dec 2024 16:35:16 -0300 Subject: [PATCH 37/44] build --- pilopt/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 0832fea844..ffef994ee0 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -9,7 +9,7 @@ use powdr_ast::analyzed::{ AlgebraicUnaryOperation, AlgebraicUnaryOperator, Analyzed, ConnectIdentity, Expression, FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PhantomLookupIdentity, PhantomPermutationIdentity, PolyID, PolynomialIdentity, PolynomialReference, PolynomialType, - Reference, SelectedExpressions, Symbol, SymbolKind, + Reference, Symbol, SymbolKind, }; use powdr_ast::parsed::types::Type; use powdr_ast::parsed::visitor::{AllChildren, Children, ExpressionVisitable}; From deeca6bead614f99660ed3c15d7ff2058f39970c Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 4 Dec 2024 12:37:29 -0300 Subject: [PATCH 38/44] Code improvements. test still failing --- pilopt/src/lib.rs | 57 ++++++++++------------------------------------- 1 file changed, 12 insertions(+), 45 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index ffef994ee0..eb6243a5ee 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -263,7 +263,6 @@ fn deduplicate_fixed_columns(pil_file: &mut Analyzed) { .unzip(); // substitute all occurences in expressions. - pil_file.post_visit_expressions_in_identities_mut(&mut |e| { if let AlgebraicExpression::Reference(r) = e { if let Some((new_name, new_id)) = replacement_by_id.get(&r.poly_id) { @@ -724,18 +723,15 @@ fn equal_constrained( right, }) => match (left.as_ref(), right.as_ref()) { (AlgebraicExpression::Reference(l), AlgebraicExpression::Reference(r)) => { - let l_valid = l.is_witness() - && !l.next - && poly_id_to_array_elem - .get(&l.poly_id) - .map_or(false, |&(_, b)| !b); - let r_valid = r.is_witness() - && !r.next - && poly_id_to_array_elem - .get(&r.poly_id) - .map_or(false, |&(_, b)| !b); - - if l_valid && r_valid { + let is_valid = |x: &AlgebraicReference| { + x.is_witness() + && !x.next + && poly_id_to_array_elem + .get(&x.poly_id) + .map_or(false, |&(_, b)| !b) + }; + + if is_valid(l) && is_valid(r) { Some(if l.poly_id > r.poly_id { ((l.name.clone(), l.poly_id), (r.name.clone(), r.poly_id)) } else { @@ -765,15 +761,10 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal }) .collect(); - let subs_by_id: HashMap<_, _> = substitutions + let (subs_by_id, subs_by_name): (HashMap<_, _>, HashMap<_, _>) = substitutions .iter() - .map(|((_, id), to_keep)| (id, to_keep)) - .collect(); - - let subs_by_name: HashMap<_, _> = substitutions - .iter() - .map(|((name, _), to_keep)| (name, to_keep)) - .collect(); + .map(|((name, id), to_keep)| ((id, to_keep), (name, to_keep))) + .unzip(); pil_file.post_visit_expressions_in_identities_mut(&mut |e: &mut AlgebraicExpression<_>| { if let AlgebraicExpression::Reference(ref mut reference) = e { @@ -792,27 +783,3 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal } }); } -// fn cols_in_identity_lookup(pil_file: &Analyzed) -> HashSet { -// pil_file -// .identities -// .iter() -// .filter_map(|id| match id { -// Identity::Lookup(LookupIdentity { left, right, .. }) => { -// Some(extract_references(left).chain(extract_references(right))) -// } -// _ => None, -// }) -// .flatten() -// .collect() -// } -// fn extract_references( -// selected_expr: &SelectedExpressions, -// ) -> impl Iterator + '_ { -// selected_expr.expressions.iter().flat_map(|expr| { -// expr.all_children().filter_map(|child| match child { -// AlgebraicExpression::Reference(reference) => Some(reference.name.clone()), -// AlgebraicExpression::PublicReference(preference) => Some(preference.clone()), -// _ => None, -// }) -// }) -// } From df5b7be14e2da4526c98679bbf730cace56540de Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 5 Dec 2024 12:23:05 -0300 Subject: [PATCH 39/44] fix program columns to witness columns --- riscv-executor/src/lib.rs | 51 ++++++++++++++++++++++++--------------- 1 file changed, 32 insertions(+), 19 deletions(-) diff --git a/riscv-executor/src/lib.rs b/riscv-executor/src/lib.rs index 133a97a32a..59080343eb 100644 --- a/riscv-executor/src/lib.rs +++ b/riscv-executor/src/lib.rs @@ -20,7 +20,7 @@ use builder::TraceBuilder; use itertools::Itertools; use powdr_ast::{ - analyzed::Analyzed, + analyzed::{AlgebraicExpression, Analyzed, Identity, LookupIdentity}, asm_analysis::{AnalysisASMFile, CallableSymbol, FunctionStatement, LabelStatement, Machine}, parsed::{ asm::{parse_absolute_path, AssignmentRegister, DebugDirective}, @@ -2422,24 +2422,37 @@ fn execute_inner( }) .unwrap_or_default(); - // program columns to witness columns - let program_cols: HashMap<_, _> = if let Some(fixed) = &fixed { - fixed - .iter() - .filter_map(|(name, _col)| { - if !name.starts_with("main__rom::p_") { - return None; - } - let wit_name = format!("main::{}", name.strip_prefix("main__rom::p_").unwrap()); - if !witness_cols.contains(&wit_name) { - return None; - } - Some((name.clone(), wit_name)) - }) - .collect() - } else { - Default::default() - }; + //program columns to witness columns + let program_cols: HashMap<_, _> = opt_pil + .map(|pil| { + pil.identities + .iter() + .flat_map(|id| match id { + Identity::Lookup(LookupIdentity { left, right, .. }) => left + .expressions + .iter() + .zip(right.expressions.iter()) + .filter_map(|(l, r)| match (l, r) { + ( + AlgebraicExpression::Reference(l), + AlgebraicExpression::Reference(r), + ) => { + if r.name.starts_with("main__rom::p_") + && witness_cols.contains(&l.name) + { + Some((r.name.clone(), l.name.clone())) + } else { + None + } + } + _ => None, + }) + .collect::>(), + _ => vec![], + }) + .collect() + }) + .unwrap_or_default(); let proc = match TraceBuilder::<'_, F>::new( main_machine, From c859b60b725a2da38389a572f8df2fb11f605db8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gast=C3=B3n=20Zanitti?= Date: Tue, 10 Dec 2024 09:58:55 -0300 Subject: [PATCH 40/44] Update pilopt/src/lib.rs Co-authored-by: chriseth --- pilopt/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index eb6243a5ee..76e5534991 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -121,8 +121,8 @@ fn remove_unreferenced_definitions(pil_file: &mut Analyzed) pil_file.remove_trait_impls(&impls_to_remove); } -/// Builds a lookup-table that can be used to turn all symbols -/// (including array elements) in the form of their poly ids, into the names of the symbols. +/// Builds a lookup-table that can be used to turn all poly ids into the names of the symbols that define them. +/// For array elements, this is the name of the array. /// The boolean flag indicates whether the symbol belongs to an array or not fn build_poly_id_to_definition_name_lookup( pil_file: &Analyzed, From 42c08b239ed61edd149e20d55025397f53c10a65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gast=C3=B3n=20Zanitti?= Date: Tue, 10 Dec 2024 09:59:30 -0300 Subject: [PATCH 41/44] Update pilopt/src/lib.rs Co-authored-by: chriseth --- pilopt/src/lib.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 76e5534991..41ae0c2099 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -131,15 +131,9 @@ fn build_poly_id_to_definition_name_lookup( for (name, (symbol, _)) in &pil_file.definitions { if matches!(symbol.kind, SymbolKind::Poly(_)) { - if symbol.is_array() { symbol.array_elements().for_each(|(_, id)| { - poly_id_to_info.insert(id, (name, true)); + poly_id_to_info.insert(id, (name, symbol.is_array())); }); - } else { - symbol.array_elements().for_each(|(_, id)| { - poly_id_to_info.insert(id, (name, false)); - }); - } } } From 934f668158b012885f5cc11cce4b781b1350460a Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Tue, 10 Dec 2024 10:16:31 -0300 Subject: [PATCH 42/44] minor changes --- pilopt/src/lib.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 41ae0c2099..ecc44b1b0b 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -131,9 +131,9 @@ fn build_poly_id_to_definition_name_lookup( for (name, (symbol, _)) in &pil_file.definitions { if matches!(symbol.kind, SymbolKind::Poly(_)) { - symbol.array_elements().for_each(|(_, id)| { - poly_id_to_info.insert(id, (name, symbol.is_array())); - }); + symbol.array_elements().for_each(|(_, id)| { + poly_id_to_info.insert(id, (name, symbol.is_array())); + }); } } From 7dd3a120edaf7b0850e2596c965ab62fa244d41c Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Tue, 10 Dec 2024 11:04:42 -0300 Subject: [PATCH 43/44] transitive substitutions --- pilopt/src/lib.rs | 60 ++++++++++++++++++++++++++++++--------- pilopt/tests/optimizer.rs | 18 ++++++++++++ 2 files changed, 64 insertions(+), 14 deletions(-) diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 14f28559fc..3775dfc073 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -122,26 +122,33 @@ fn remove_unreferenced_definitions(pil_file: &mut Analyzed) } /// Builds a lookup-table that can be used to turn all poly ids into the names of the symbols that define them. -/// For array elements, this is the name of the array. -/// The boolean flag indicates whether the symbol belongs to an array or not +/// For array elements, this contains the array name and the index of the element in the array. fn build_poly_id_to_definition_name_lookup( pil_file: &Analyzed, -) -> BTreeMap { +) -> BTreeMap)> { let mut poly_id_to_definition_name = BTreeMap::new(); #[allow(clippy::iter_over_hash_type)] for (name, (symbol, _)) in &pil_file.definitions { if matches!(symbol.kind, SymbolKind::Poly(_)) { - symbol.array_elements().for_each(|(_, id)| { - poly_id_to_definition_name.insert(id, (name, symbol.is_array())); - }); + symbol + .array_elements() + .enumerate() + .for_each(|(idx, (_, id))| { + let array_pos = if symbol.is_array() { Some(idx) } else { None }; + poly_id_to_definition_name.insert(id, (name, array_pos)); + }); } } #[allow(clippy::iter_over_hash_type)] for (name, (symbol, _)) in &pil_file.intermediate_columns { - symbol.array_elements().for_each(|(_, id)| { - poly_id_to_definition_name.insert(id, (name, symbol.is_array())); - }); + symbol + .array_elements() + .enumerate() + .for_each(|(idx, (_, id))| { + let array_pos = if symbol.is_array() { Some(idx) } else { None }; + poly_id_to_definition_name.insert(id, (name, array_pos)); + }); } poly_id_to_definition_name @@ -150,7 +157,7 @@ fn build_poly_id_to_definition_name_lookup( /// Collect all names that are referenced in identities and public declarations. fn collect_required_symbols<'a, T: FieldElement>( pil_file: &'a Analyzed, - poly_id_to_definition_name: &BTreeMap, + poly_id_to_definition_name: &BTreeMap)>, ) -> HashSet> { let mut required_names: HashSet> = Default::default(); required_names.extend( @@ -718,7 +725,7 @@ fn remove_duplicate_identities(pil_file: &mut Analyzed) { /// for each pair of identified columns fn equal_constrained( expression: &AlgebraicExpression, - poly_id_to_array_elem: &BTreeMap, + poly_id_to_array_elem: &BTreeMap)>, ) -> Option<((String, PolyID), (String, PolyID))> { match expression { AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -730,9 +737,7 @@ fn equal_constrained( let is_valid = |x: &AlgebraicReference| { x.is_witness() && !x.next - && poly_id_to_array_elem - .get(&x.poly_id) - .map_or(false, |&(_, b)| !b) + && poly_id_to_array_elem.get(&x.poly_id).unwrap().1.is_none() }; if is_valid(l) && is_valid(r) { @@ -765,6 +770,8 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal }) .collect(); + let substitutions = resolve_transitive_substitutions(substitutions); + let (subs_by_id, subs_by_name): (HashMap<_, _>, HashMap<_, _>) = substitutions .iter() .map(|((name, id), to_keep)| ((id, to_keep), (name, to_keep))) @@ -787,3 +794,28 @@ fn remove_equal_constrained_witness_columns(pil_file: &mut Anal } }); } + +fn resolve_transitive_substitutions( + subs: Vec<((String, PolyID), (String, PolyID))>, +) -> Vec<((String, PolyID), (String, PolyID))> { + let mut result = subs.clone(); + let mut changed = true; + + while changed { + changed = false; + for i in 0..result.len() { + let (_, target1) = &result[i].1; + if let Some(j) = result + .iter() + .position(|((_, source2), _)| source2 == target1) + { + let ((name1, source1), _) = &result[i]; + let (_, (name3, target2)) = &result[j]; + result[i] = ((name1.clone(), *source1), (name3.clone(), *target2)); + changed = true; + } + } + } + + result +} diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index 18a83a1fb2..67d7ab7d8d 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -425,3 +425,21 @@ fn equal_constrained_array_elements() { let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); } + +#[test] +fn equal_constrained_transitive() { + let input = r#"namespace N(65536); + col witness a; + col witness b; + col witness c; + a = b; + b = c; + a + b + c = 5; + "#; + let expectation = r#"namespace N(65536); + col witness a; + N::a + N::a + N::a = 5; +"#; + let optimized = optimize(analyze_string::(input).unwrap()).to_string(); + assert_eq!(optimized, expectation); +} From c01dca9bd9d592257a9e7c641d362a9633e39b86 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Tue, 10 Dec 2024 15:55:47 -0300 Subject: [PATCH 44/44] equal_constrained_transitive --- pilopt/tests/optimizer.rs | 6 +----- pipeline/tests/asm.rs | 6 ------ test_data/asm/intermediate.asm | 11 ----------- 3 files changed, 1 insertion(+), 22 deletions(-) delete mode 100644 test_data/asm/intermediate.asm diff --git a/pilopt/tests/optimizer.rs b/pilopt/tests/optimizer.rs index 67d7ab7d8d..731aeb5746 100644 --- a/pilopt/tests/optimizer.rs +++ b/pilopt/tests/optimizer.rs @@ -100,11 +100,7 @@ fn intermediate() { col intermediate = x; intermediate = intermediate; "#; - let expectation = r#"namespace N(65536); - col witness x; - col intermediate = N::x; - N::intermediate = N::intermediate; -"#; + let expectation = r#""#; let optimized = optimize(analyze_string::(input).unwrap()).to_string(); assert_eq!(optimized, expectation); } diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 99ecf47326..c9db9b3d3d 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -366,12 +366,6 @@ fn full_pil_constant() { regular_test_all_fields(f, Default::default()); } -#[test] -fn intermediate() { - let f = "asm/intermediate.asm"; - regular_test_all_fields(f, Default::default()); -} - #[test] fn intermediate_nested() { let f = "asm/intermediate_nested.asm"; diff --git a/test_data/asm/intermediate.asm b/test_data/asm/intermediate.asm deleted file mode 100644 index 4584503218..0000000000 --- a/test_data/asm/intermediate.asm +++ /dev/null @@ -1,11 +0,0 @@ -machine Intermediate with - latch: latch, - operation_id: operation_id, - degree: 8 -{ - col fixed latch = [1]*; - col fixed operation_id = [0]*; - col witness x; - col intermediate = x; - intermediate = intermediate; -}