Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
93 changes: 93 additions & 0 deletions pil-analyzer/src/isolated_column_checker.rs
Original file line number Diff line number Diff line change
@@ -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<T: FieldElement>(analyzed: &Analyzed<T>) -> Vec<IsolatedCommittedColumn> {
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<T: FieldElement>(
analyzed: &Analyzed<T>,
) -> 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::<Vec<_>>()
})
.collect()
}

fn committed_poly_ids_with_any_cooccurrence<T: FieldElement>(
analyzed: &Analyzed<T>,
) -> HashSet<PolyID> {
let mut connected: HashSet<PolyID> = HashSet::new();
for identity in analyzed.identities_with_inlined_intermediate_polynomials() {
let mut refs: HashSet<PolyID> = 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<T>(expr: &AlgebraicExpression<T>, out: &mut HashSet<PolyID>) {
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(_) => {}
}
}
2 changes: 2 additions & 0 deletions pil-analyzer/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

mod call_graph;
mod condenser;
mod isolated_column_checker;
pub mod evaluator;
pub mod expression_processor;
mod pil_analyzer;
Expand All @@ -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.
Expand Down
13 changes: 11 additions & 2 deletions pil-analyzer/src/pil_analyzer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -49,7 +49,16 @@ fn analyze<T: FieldElement>(files: Vec<PILFile>) -> Analyzed<T> {
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);
}
}
analyzed
}

#[derive(Default)]
Expand Down
75 changes: 75 additions & 0 deletions pil-analyzer/tests/isolated_columns.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
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::<GoldilocksField>(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::<GoldilocksField>(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::<GoldilocksField>(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::<GoldilocksField>(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::<GoldilocksField>(input);
let isolated = isolated_committed_columns(&analyzed);

assert!(isolated.len() == 0, "expected no isolated columns, got: {isolated:?}");
}


Loading