sc_neurocore_engine/ir/
verify.rs

1// SPDX-License-Identifier: AGPL-3.0-or-later | Commercial license available
2// © Concepts 1996–2026 Miroslav Šotek. All rights reserved.
3// © Code 2020–2026 Miroslav Šotek. All rights reserved.
4// ORCID: 0009-0009-3560-0851
5// Contact: www.anulum.li | protoscience@anulum.li
6// SC-NeuroCore — Graph verification passes
7
8//! Graph verification passes.
9
10use std::collections::{HashMap, HashSet};
11
12use crate::ir::graph::*;
13
14/// Verification error with location info.
15#[derive(Debug, Clone)]
16pub struct VerifyError {
17    pub op_index: usize,
18    pub message: String,
19}
20
21impl std::fmt::Display for VerifyError {
22    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
23        write!(f, "op[{}]: {}", self.op_index, self.message)
24    }
25}
26
27/// Run all verification passes on a graph. Returns `Ok(())` if valid,
28/// or a list of all errors found.
29pub fn verify(graph: &ScGraph) -> Result<(), Vec<VerifyError>> {
30    let mut errors = Vec::new();
31    verify_ssa(graph, &mut errors);
32    verify_operand_defs(graph, &mut errors);
33    verify_no_cycles(graph, &mut errors);
34    if errors.is_empty() {
35        Ok(())
36    } else {
37        Err(errors)
38    }
39}
40
41/// Check that every ValueId is defined exactly once.
42fn verify_ssa(graph: &ScGraph, errors: &mut Vec<VerifyError>) {
43    let mut defined: HashMap<ValueId, usize> = HashMap::new();
44    for (idx, op) in graph.ops.iter().enumerate() {
45        let id = op.result_id();
46        if let Some(prev_idx) = defined.insert(id, idx) {
47            errors.push(VerifyError {
48                op_index: idx,
49                message: format!("{} is already defined by op[{}]", id, prev_idx),
50            });
51        }
52    }
53}
54
55/// Check that every operand references a value defined by an earlier op.
56fn verify_operand_defs(graph: &ScGraph, errors: &mut Vec<VerifyError>) {
57    let mut defined: HashSet<ValueId> = HashSet::new();
58    for (idx, op) in graph.ops.iter().enumerate() {
59        for operand in op.operands() {
60            if !defined.contains(&operand) {
61                errors.push(VerifyError {
62                    op_index: idx,
63                    message: format!(
64                        "operand {} not defined before use in {}",
65                        operand,
66                        op.op_name()
67                    ),
68                });
69            }
70        }
71        defined.insert(op.result_id());
72    }
73}
74
75/// Check that the operation list is acyclic (topological order).
76/// Since we enforce operand-before-use in `verify_operand_defs`,
77/// this is automatically satisfied if that check passes.
78/// This function is a belt-and-suspenders DFS cycle check.
79fn verify_no_cycles(graph: &ScGraph, errors: &mut Vec<VerifyError>) {
80    // Build adjacency from result_id → operand ids
81    let mut adj: HashMap<ValueId, Vec<ValueId>> = HashMap::new();
82    for op in &graph.ops {
83        adj.insert(op.result_id(), op.operands());
84    }
85
86    let mut visited: HashSet<ValueId> = HashSet::new();
87    let mut in_stack: HashSet<ValueId> = HashSet::new();
88
89    fn dfs(
90        node: ValueId,
91        adj: &HashMap<ValueId, Vec<ValueId>>,
92        visited: &mut HashSet<ValueId>,
93        in_stack: &mut HashSet<ValueId>,
94    ) -> bool {
95        if in_stack.contains(&node) {
96            return true; // cycle
97        }
98        if visited.contains(&node) {
99            return false;
100        }
101        visited.insert(node);
102        in_stack.insert(node);
103        if let Some(deps) = adj.get(&node) {
104            for dep in deps {
105                if dfs(*dep, adj, visited, in_stack) {
106                    return true;
107                }
108            }
109        }
110        in_stack.remove(&node);
111        false
112    }
113
114    for op in &graph.ops {
115        let id = op.result_id();
116        if dfs(id, &adj, &mut visited, &mut in_stack) {
117            errors.push(VerifyError {
118                op_index: 0,
119                message: format!("cycle detected involving {}", id),
120            });
121            break;
122        }
123    }
124}
sc_neurocore_engine/ir/verify.rs

sc_neurocore_engine/ir/
verify.rs
