feat(avm security): add static check for isolated/unused columns

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"

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<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)) // 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<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))
+        }) // 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::<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(_) => {}
+    }
+}
+
+pub(crate) fn format_source(source: &SourceRef) -> String {
+    let file = source.file_name.as_ref().map(|s| s.as_ref()).unwrap_or("<unknown>");
+    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::<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:?}");
+    }
+}

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<T: FieldElement>(analyzed: &Analyzed<T>) -> Result<(), String> {
+    let isolated = isolated_committed_columns(analyzed);
+    if isolated.len() > 0 {
+        return Err(format!("Isolated committed columns detected: {:?}", isolated));
+    }
+    Ok(())
+}

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;

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<Bn254Field> = 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);