sc_neurocore_engine/ir/
verify.rs

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

sc_neurocore_engine/ir/
verify.rs
