From 9295a8bdb2b5710806dbb04ed162437168307e6c Mon Sep 17 00:00:00 2001 From: defkit Date: Mon, 12 Jan 2026 15:44:21 +0700 Subject: [PATCH 1/2] isolated values --- pil-analyzer/src/isolated_column_checker.rs | 93 +++++++++++++++++++++ pil-analyzer/src/lib.rs | 2 + pil-analyzer/src/pil_analyzer.rs | 14 +++- pil-analyzer/tests/isolated_columns.rs | 77 +++++++++++++++++ 4 files changed, 184 insertions(+), 2 deletions(-) create mode 100644 pil-analyzer/src/isolated_column_checker.rs create mode 100644 pil-analyzer/tests/isolated_columns.rs diff --git a/pil-analyzer/src/isolated_column_checker.rs b/pil-analyzer/src/isolated_column_checker.rs new file mode 100644 index 0000000000..298c525cc2 --- /dev/null +++ b/pil-analyzer/src/isolated_column_checker.rs @@ -0,0 +1,93 @@ +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 struct IsolatedCommittedColumn { + pub name: String, + pub source: SourceRef, +} + +/// Returns committed/witness columns that never appear together with any other column +/// in any identity (polynomial constraints, lookups, permutations, connect). +pub 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)) + .map(|(_poly_id, name, source)| IsolatedCommittedColumn { name, 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)) + }) + .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(_) => {} + } +} diff --git a/pil-analyzer/src/lib.rs b/pil-analyzer/src/lib.rs index 325a27721f..4d8761571e 100644 --- a/pil-analyzer/src/lib.rs +++ b/pil-analyzer/src/lib.rs @@ -2,6 +2,7 @@ mod call_graph; mod condenser; +mod isolated_column_checker; pub mod evaluator; pub mod expression_processor; mod pil_analyzer; @@ -24,6 +25,7 @@ use powdr_ast::{ }; pub use pil_analyzer::{analyze_ast, analyze_file, analyze_string}; +pub use isolated_column_checker::{isolated_committed_columns, IsolatedCommittedColumn}; pub trait AnalysisDriver: Clone + Copy { /// Turns a declaration into an absolute name. diff --git a/pil-analyzer/src/pil_analyzer.rs b/pil-analyzer/src/pil_analyzer.rs index 04e0eeafaa..12ec62e708 100644 --- a/pil-analyzer/src/pil_analyzer.rs +++ b/pil-analyzer/src/pil_analyzer.rs @@ -21,7 +21,7 @@ use powdr_ast::analyzed::{ use powdr_parser::parse_type; use crate::type_inference::{infer_types, ExpectedType}; -use crate::{side_effect_checker, AnalysisDriver}; +use crate::{AnalysisDriver, isolated_committed_columns, side_effect_checker}; use crate::statement_processor::{Counters, PILItem, StatementProcessor}; use crate::{condenser, evaluator, expression_processor::ExpressionProcessor}; @@ -49,7 +49,17 @@ fn analyze(files: Vec) -> Analyzed { analyzer.process(files); analyzer.side_effect_check(); analyzer.type_check(); - analyzer.condense() + let analyzed = analyzer.condense(); + let isolated = isolated_committed_columns(&analyzed); + if !isolated.is_empty() { + eprintln!("Isolated committed columns detected (declared but never referenced by any constraint/lookup/permutation/public declaration):\n"); + for d in isolated { + let file = d.source.file_name.as_ref().unwrap(); + eprintln!("- {} ({}): {} .. {}", d.name, file, d.source.start, d.source.end); + } + panic!("Isolated committed columns detected"); + } + analyzed } #[derive(Default)] diff --git a/pil-analyzer/tests/isolated_columns.rs b/pil-analyzer/tests/isolated_columns.rs new file mode 100644 index 0000000000..09b4469a08 --- /dev/null +++ b/pil-analyzer/tests/isolated_columns.rs @@ -0,0 +1,77 @@ +use powdr_number::GoldilocksField; +use powdr_pil_analyzer::{analyze_string, 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 not_isolated_when_constrained_with_fixed() { + let input = r#" + namespace N(16); + pol constant c; + pol commit a; + a - c = 0; + "#; + let analyzed = analyze_string::(input); + let isolated = isolated_committed_columns(&analyzed); + + assert!(isolated.len() == 0, "expected no isolated columns, 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:?}"); +} + + From 4fdfb0a4ddf4db0a7f294c1ae2851696995e3aa4 Mon Sep 17 00:00:00 2001 From: defkit Date: Mon, 12 Jan 2026 15:49:28 +0700 Subject: [PATCH 2/2] isolated values --- pil-analyzer/src/pil_analyzer.rs | 1 - pil-analyzer/tests/isolated_columns.rs | 10 ++++------ 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/pil-analyzer/src/pil_analyzer.rs b/pil-analyzer/src/pil_analyzer.rs index 12ec62e708..8708067ec9 100644 --- a/pil-analyzer/src/pil_analyzer.rs +++ b/pil-analyzer/src/pil_analyzer.rs @@ -57,7 +57,6 @@ fn analyze(files: Vec) -> Analyzed { let file = d.source.file_name.as_ref().unwrap(); eprintln!("- {} ({}): {} .. {}", d.name, file, d.source.start, d.source.end); } - panic!("Isolated committed columns detected"); } analyzed } diff --git a/pil-analyzer/tests/isolated_columns.rs b/pil-analyzer/tests/isolated_columns.rs index 09b4469a08..4b70ed6939 100644 --- a/pil-analyzer/tests/isolated_columns.rs +++ b/pil-analyzer/tests/isolated_columns.rs @@ -30,19 +30,17 @@ fn not_isolated_when_constrained_with_other_committed() { } #[test] -fn not_isolated_when_constrained_with_fixed() { +fn test_dead_columns() { let input = r#" - namespace N(16); - pol constant c; pol commit a; - a - c = 0; "#; let analyzed = analyze_string::(input); let isolated = isolated_committed_columns(&analyzed); - - assert!(isolated.len() == 0, "expected no isolated columns, got: {isolated:?}"); + 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#"