car-verify 0.55.0

//! Shared DAG helpers for the verify family.
//!
//! `transitive_ancestors` + `ordered` were copied near-verbatim in
//! [`crate::transaction`] and [`crate::infoflow`]; both derive ordering from the
//! *same* [`car_ir::dependency_edges`] the executor sequences on, so the notion
//! of "ordered" stays identical to the runtime by construction. Keeping one copy
//! here removes the drift risk of two.

use car_ir::{dependency_edges, Action};
use std::collections::HashSet;

/// Transitive ancestors of each action in the executor's dependency graph.
/// `ancestors[i]` is every action that must complete before `i` runs.
/// Built from [`car_ir::dependency_edges`] — the *same* edges
/// [`car_ir::build_dag`] sequences on — so the checker's notion of "ordered" is
/// identical to the runtime's by construction (neo review C1: a re-derivation
/// drifts from the DAG and suppresses real races / invents false ones).
pub fn transitive_ancestors(actions: &[Action]) -> Vec<HashSet<usize>> {
    let direct = dependency_edges(actions);
    let n = actions.len();
    let mut ancestors: Vec<HashSet<usize>> = vec![HashSet::new(); n];
    // Edges only point to lower indices (`writer_idx < i`), so a single
    // ascending pass computes the full closure: i's ancestors are its
    // direct deps plus each direct dep's already-computed ancestors.
    for i in 0..n {
        for &d in &direct[i] {
            ancestors[i].insert(d);
            let d_anc: Vec<usize> = ancestors[d].iter().copied().collect();
            ancestors[i].extend(d_anc);
        }
    }
    ancestors
}

/// Are actions `i` and `j` sequenced by a (transitive) dependency — i.e. is one
/// a DAG ancestor of the other? If so a shared access is an ordered step, not a
/// race.
pub fn ordered(i: usize, j: usize, ancestors: &[HashSet<usize>]) -> bool {
    ancestors[i].contains(&j) || ancestors[j].contains(&i)
}