tokitai-operator 0.1.0

Verified DL kernel compiler: formally-checked GEMM, p-adic, sheaf, contract-carrying ops. Paper-artifact grade.
Documentation
//! Classification of the irreducible duplicate triples in
//! `generated_theory_support_matrix` (P382).
//!
//! After P369 the support matrix has 8 duplicate (domain, operator,
//! backend) triples. Detailed inspection shows they fall into 2
//! categories, both LEGITIMATE:
//!
//! - **multi_state**: a (n=2) duplicate where both rows have the same
//!   `lowering_rule_id` but different `support_status` (one is
//!   `FeatureGatedPilot`, the other is `Unavailable` or
//!   `FallbackOnly`). The p205 test requires both to coexist because
//!   they represent the same rule in two different states (e.g.,
//!   "HIP add kernel is available with the rocm-hip feature flag" vs
//!   "HIP add kernel is unavailable because the driver is missing").
//!
//! - **multi_rule**: a (n=2 or n=3) duplicate where the rows have
//!   DIFFERENT `lowering_rule_id`s (e.g., the 3 Q_* matmul rules
//!   `cpu.matmul.padic_dense`, `cpu.matmul.padic_valuation_skip`,
//!   `cpu.matmul.padic_valuation_stratified` all share the
//!   `Q_*` domain because `domain_scope` returns `Q_*` from their
//!   `supported_domains`). These are distinct rules that happen to
//!   share a (domain, operator, backend) triple.
//!
//! This module exposes a `classify_dup` function that returns a
//! `DupKind` enum, and a `matrix_dedup_summary` function that
//! summarizes the matrix's duplicate count and classification.

use std::collections::BTreeMap;

use super::support_matrix::{TheorySupportMatrix, TheorySupportMatrixRow};

/// Classification of a duplicate (domain, operator, backend) triple.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum DupKind {
    /// Two rows, same lowering_rule_id, different support_status
    /// (typically FeatureGatedPilot + Unavailable).
    MultiState,
    /// Two or more rows, different lowering_rule_ids (or one of them
    /// is None), representing distinct rules sharing the same triple.
    MultiRule,
    /// Anything else (unexpected).
    Other,
}

/// A single duplicate triple plus its classification.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ClassifiedDup {
    pub triple: (String, String, String),
    pub count: usize,
    pub kind: DupKind,
}

/// Classify a single (domain, operator, backend) triple's rows.
pub fn classify_dup(rows: &[&TheorySupportMatrixRow]) -> DupKind {
    if rows.len() < 2 {
        return DupKind::Other;
    }
    // Compute the set of distinct lowering_rule_ids (treating None
    // as the empty string for set membership).
    let mut ids = std::collections::BTreeSet::new();
    for r in rows {
        ids.insert(r.lowering_rule_id.clone().unwrap_or_default());
    }
    // Compute the set of distinct support_status values.
    let mut statuses = std::collections::BTreeSet::new();
    for r in rows {
        statuses.insert(format!("{:?}", r.support_status));
    }
    if ids.len() == 1 && statuses.len() > 1 {
        // Same lowering rule, different status values (e.g.,
        // pilot+unavailable or pilot+fallback) => MultiState.
        return DupKind::MultiState;
    }
    if ids.len() > 1 {
        // Different lowering rules sharing the same (domain,
        // operator, backend) triple => MultiRule.
        return DupKind::MultiRule;
    }
    // Same id, same status (true duplicates) => Other. Should
    // not happen after P369, but reported for completeness.
    DupKind::Other
}

/// Walk the support matrix, find all duplicate (domain, operator,
/// backend) triples, and classify each.
pub fn matrix_dedup_summary(matrix: &TheorySupportMatrix) -> Vec<ClassifiedDup> {
    let mut by_triple: BTreeMap<(String, String, String), Vec<&TheorySupportMatrixRow>> =
        BTreeMap::new();
    for row in &matrix.rows {
        by_triple
            .entry((
                row.domain.clone(),
                row.operator.clone(),
                row.backend.clone(),
            ))
            .or_default()
            .push(row);
    }
    let mut out: Vec<ClassifiedDup> = by_triple
        .into_iter()
        .filter(|(_, rows)| rows.len() > 1)
        .map(|(triple, rows)| ClassifiedDup {
            triple,
            count: rows.len(),
            kind: classify_dup(&rows),
        })
        .collect();
    out.sort_by(|a, b| a.triple.0.cmp(&b.triple.0));
    out
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::verify::support_matrix::{SupportStatus, TheorySupportMatrixRow};

    fn row(
        domain: &str,
        operator: &str,
        backend: &str,
        lr: Option<&str>,
        status: SupportStatus,
    ) -> TheorySupportMatrixRow {
        TheorySupportMatrixRow {
            domain: domain.to_string(),
            operator: operator.to_string(),
            theory_constraints: vec![],
            theorem_packages: vec![],
            backend: backend.to_string(),
            backend_capability: String::new(),
            lowering_rule_id: lr.map(String::from),
            support_status: status,
            fallback_mode: String::new(),
            public_api: String::new(),
            tests: vec![],
            non_claims: vec![],
        }
    }

    #[test]
    fn multi_state_classified() {
        let r1 = row(
            "d",
            "op",
            "b",
            Some("lr1"),
            SupportStatus::FeatureGatedPilot,
        );
        let r2 = row("d", "op", "b", Some("lr1"), SupportStatus::Unavailable);
        let rows = vec![&r1, &r2];
        assert_eq!(classify_dup(&rows), DupKind::MultiState);
    }

    #[test]
    fn multi_rule_classified() {
        let r1 = row("d", "op", "b", Some("lr1"), SupportStatus::Supported);
        let r2 = row("d", "op", "b", Some("lr2"), SupportStatus::Supported);
        let rows = vec![&r1, &r2];
        assert_eq!(classify_dup(&rows), DupKind::MultiRule);
    }

    #[test]
    fn single_row_is_other() {
        let r1 = row("d", "op", "b", Some("lr1"), SupportStatus::Supported);
        let rows = vec![&r1];
        assert_eq!(classify_dup(&rows), DupKind::Other);
    }

    #[test]
    fn matrix_dedup_summary_classifies_correctly() {
        // Build a tiny matrix with 1 multi_state pair + 1 multi_rule triple.
        let r1 = row(
            "d1",
            "op",
            "b1",
            Some("lr1"),
            SupportStatus::FeatureGatedPilot,
        );
        let r2 = row("d1", "op", "b1", Some("lr1"), SupportStatus::Unavailable);
        let r3 = row("d2", "op", "b1", Some("lr2"), SupportStatus::Supported);
        let r4 = row("d2", "op", "b1", Some("lr3"), SupportStatus::Supported);
        let r5 = row("d3", "op", "b2", Some("lr4"), SupportStatus::Supported);
        let m = TheorySupportMatrix {
            artifact: "test".to_string(),
            version: 1,
            rows: vec![r1, r2, r3, r4, r5],
        };
        let summary = matrix_dedup_summary(&m);
        assert_eq!(summary.len(), 2);
        assert_eq!(summary[0].kind, DupKind::MultiState);
        assert_eq!(summary[0].count, 2);
        assert_eq!(summary[1].kind, DupKind::MultiRule);
        assert_eq!(summary[1].count, 2);
    }
}