diff --git a/bb-pilcom/Cargo.lock b/bb-pilcom/Cargo.lock index 518f781cad5f..58c5f26b8004 100644 --- a/bb-pilcom/Cargo.lock +++ b/bb-pilcom/Cargo.lock @@ -1,6 +1,6 @@ # This file is automatically @generated by Cargo. # It is not intended for manual editing. -version = 3 +version = 4 [[package]] name = "ahash" @@ -250,6 +250,8 @@ dependencies = [ "num-traits", "powdr-ast", "powdr-number", + "powdr-parser-util", + "powdr-pil-analyzer", "rand", "serde_json", ] diff --git a/bb-pilcom/bb-pil-backend/Cargo.toml b/bb-pilcom/bb-pil-backend/Cargo.toml index 57fb58415e0d..e1c78484bd4f 100644 --- a/bb-pilcom/bb-pil-backend/Cargo.toml +++ b/bb-pilcom/bb-pil-backend/Cargo.toml @@ -12,6 +12,8 @@ use_optimized = [] num-bigint = "0.4.3" powdr-number = { path = "../powdr/number" } +powdr-parser-util = { path = "../powdr/parser-util" } +powdr-pil-analyzer = { path = "../powdr/pil-analyzer" } num-traits = "0.2.15" num-integer = "0.1.45" itertools = "^0.10" diff --git a/bb-pilcom/bb-pil-backend/src/checks/isolated_columns_check.rs b/bb-pilcom/bb-pil-backend/src/checks/isolated_columns_check.rs new file mode 100644 index 000000000000..d3f736230ef8 --- /dev/null +++ b/bb-pilcom/bb-pil-backend/src/checks/isolated_columns_check.rs @@ -0,0 +1,175 @@ +use std::collections::HashSet; + +use powdr_ast::analyzed::{AlgebraicExpression, Analyzed, PolyID, PolynomialType, SymbolKind}; +use powdr_number::FieldElement; +use powdr_parser_util::SourceRef; + +/// A committed/witness column (including array elements) that appears in at least one identity, +/// but never co-occurs with any other column in the same identity. +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) struct IsolatedCommittedColumn { + pub name: String, + pub source: String, +} + +/// Returns committed/witness columns that never appear together with any other column +/// in any identity (polynomial constraints, lookups, permutations, connect). +pub(crate) fn isolated_committed_columns(analyzed: &Analyzed) -> Vec { + let declared_committed = declared_committed_poly_ids(analyzed); + let connected = committed_poly_ids_with_any_cooccurrence(analyzed); + + declared_committed + .into_iter() + .filter(|(_poly_id, _name, _src)| !connected.contains(_poly_id)) // filter all committed polynomials that are not connected + .map(|(_poly_id, name, source)| IsolatedCommittedColumn { name, source: format_source(&source) }) + .collect() +} + +fn declared_committed_poly_ids( + analyzed: &Analyzed, +) -> Vec<(PolyID, String, SourceRef)> { + analyzed + .definitions + .iter() + .filter(|(name, (sym, _))| { + !analyzed.auto_added_symbols.contains(*name) + && matches!(sym.kind, SymbolKind::Poly(PolynomialType::Committed)) + }) // filter all committed polynomials + .flat_map(|(_name, (sym, _def))| { + sym.array_elements() + .map(|(elem_name, poly_id)| (poly_id, elem_name, sym.source.clone())) + .collect::>() + }) + .collect() +} + +fn committed_poly_ids_with_any_cooccurrence( + analyzed: &Analyzed, +) -> HashSet { + let mut connected: HashSet = HashSet::new(); + for identity in analyzed.identities_with_inlined_intermediate_polynomials() { + let mut refs: HashSet = HashSet::new(); + for expr in identity + .left + .selector + .iter() + .chain(identity.left.expressions.iter()) + .chain(identity.right.selector.iter()) + .chain(identity.right.expressions.iter()) + { + collect_poly_ids(expr, &mut refs); + } + + if refs.len() <= 1 { + continue; + } + + for poly_id in refs.iter() { + if poly_id.ptype == PolynomialType::Committed { + connected.insert(*poly_id); + } + } + } + + connected +} + +fn collect_poly_ids(expr: &AlgebraicExpression, out: &mut HashSet) { + match expr { + AlgebraicExpression::Reference(r) => { + out.insert(r.poly_id); + } + AlgebraicExpression::BinaryOperation(op) => { + collect_poly_ids(&op.left, out); + collect_poly_ids(&op.right, out); + } + AlgebraicExpression::UnaryOperation(op) => { + collect_poly_ids(&op.expr, out); + } + AlgebraicExpression::PublicReference(_) + | AlgebraicExpression::Challenge(_) + | AlgebraicExpression::Number(_) => {} + } +} + +pub(crate) fn format_source(source: &SourceRef) -> String { + let file = source.file_name.as_ref().map(|s| s.as_ref()).unwrap_or(""); + format!("{file}:{}..{}", source.start, source.end) +} + +#[cfg(test)] +mod tests { + use powdr_number::GoldilocksField; + use powdr_pil_analyzer::analyze_string; + use super::isolated_committed_columns; + + #[test] + fn isolated_if_only_self_constrained() { + let input = r#" + namespace N(16); + pol commit a; + (a - 1) * a = 0; + "#; + let analyzed = analyze_string::(input); + let isolated = isolated_committed_columns(&analyzed); + + assert!(isolated.len() == 1, "expected 1 isolated column, got: {isolated:?}"); + assert!(isolated[0].name == "N.a", "expected N.a to be isolated, got: {isolated:?}"); + } + + #[test] + fn not_isolated_when_constrained_with_other_committed() { + let input = r#" + namespace N(16); + pol commit a; + pol commit b; + a - b = 0; + "#; + let analyzed = analyze_string::(input); + let isolated = isolated_committed_columns(&analyzed); + + assert!(isolated.len() == 0, "expected no isolated columns, got: {isolated:?}"); + } + + #[test] + fn test_dead_columns() { + let input = r#" + pol commit a; + "#; + let analyzed = analyze_string::(input); + let isolated = isolated_committed_columns(&analyzed); + assert!(isolated.len() == 1, "expected 1 isolated column, got: {isolated:?}"); + assert!(isolated[0].name == "a", "expected a to be isolated, got: {isolated:?}"); + } + + + #[test] + fn isolated_if_only_used_in_unused_intermediate() { + let input = r#" + namespace N(16); + pol commit a; + pol X = a + 1; + "#; + let analyzed = analyze_string::(input); + let isolated = isolated_committed_columns(&analyzed); + + assert!(isolated.len() == 1, "expected 1 isolated column, got: {isolated:?}"); + assert!(isolated[0].name == "N.a", "expected N.a to be isolated, got: {isolated:?}"); + } + + #[test] + fn not_isolated_when_used_in_lookup_identity() { + let input = r#" + namespace N(16); + pol commit sel; + pol commit a; + pol commit table; + // Use `a` only through a lookup identity; this should count as co-occurrence. + sel { a } in table { table }; + "#; + let analyzed = analyze_string::(input); + let isolated = isolated_committed_columns(&analyzed); + + assert!(isolated.len() == 0, "expected no isolated columns, got: {isolated:?}"); + } +} diff --git a/bb-pilcom/bb-pil-backend/src/checks/mod.rs b/bb-pilcom/bb-pil-backend/src/checks/mod.rs new file mode 100644 index 000000000000..77f12a2b8456 --- /dev/null +++ b/bb-pilcom/bb-pil-backend/src/checks/mod.rs @@ -0,0 +1,13 @@ +mod isolated_columns_check; + +use isolated_columns_check::isolated_committed_columns; +use powdr_ast::analyzed::Analyzed; +use powdr_number::FieldElement; + +pub fn check(analyzed: &Analyzed) -> Result<(), String> { + let isolated = isolated_committed_columns(analyzed); + if isolated.len() > 0 { + return Err(format!("Isolated committed columns detected: {:?}", isolated)); + } + Ok(()) +} diff --git a/bb-pilcom/bb-pil-backend/src/lib.rs b/bb-pilcom/bb-pil-backend/src/lib.rs index 0bef4b83456e..86ba796d092c 100644 --- a/bb-pilcom/bb-pil-backend/src/lib.rs +++ b/bb-pilcom/bb-pil-backend/src/lib.rs @@ -6,3 +6,4 @@ pub mod permutation_builder; mod relation_builder; mod utils; pub mod vm_builder; +pub mod checks; diff --git a/bb-pilcom/cli/src/main.rs b/bb-pilcom/cli/src/main.rs index c69fed461a31..92cc25f7b7d4 100644 --- a/bb-pilcom/cli/src/main.rs +++ b/bb-pilcom/cli/src/main.rs @@ -1,6 +1,6 @@ use std::{io, path::Path}; -use bb_pil_backend::vm_builder::analyzed_to_cpp; +use bb_pil_backend::{checks::check, vm_builder::analyzed_to_cpp}; use clap::Parser; use powdr_ast::analyzed::Analyzed; use powdr_number::Bn254Field; @@ -33,6 +33,10 @@ fn main() -> Result<(), io::Error> { let name = args.name.unwrap(); println!("Analyzing PIL file: {}", file_name); let analyzed: Analyzed = analyze_file(Path::new(&file_name)); + if let Err(e) = check(&analyzed) { + eprintln!("Error: {}", e); + panic!("Error: {}", e); + } analyzed_to_cpp(&analyzed, args.output_directory.as_deref(), &name, args.yes);