Function check_distinct_dag 

pub fn check_distinct_dag(
    root: usize,
    nodes: &[Node],
    expected: &CanonClauses,
) -> bool

Zero-trust local checker for the strict DAG: leaves carry ⊥; every internal node’s two children are exactly its recomputed cofactors. A pass certifies the root UNSAT by structural induction, in time linear in the DAG.