tokitai-operator 0.1.0

Verified DL kernel compiler: formally-checked GEMM, p-adic, sheaf, contract-carrying ops. Paper-artifact grade.
Documentation
//! Fail-closed coverage walk for the support matrix (P359).
//!
//! Every row in `generated_theory_support_matrix()` lists a set of
//! test files in `tests/` and a public-API path in `src/`. This test
//! walks the matrix, loads each referenced file, and reports the
//! orphans: rows whose test file is missing, or whose API path is
//! missing, or whose tests vector is empty.
//!
//! The test is intentionally fail-closed: a regression in the
//! evidence chain (e.g. a typo in a path, a deleted test) is
//! caught here, not in the release-gate check.

use std::path::Path;
use tokitai_operator::verify::generated_theory_support_matrix;

fn split_path_and_features(raw: &str) -> (&str, Option<&str>) {
    if let Some(idx) = raw.find(" --features ") {
        (&raw[..idx], Some(&raw[idx + " --features ".len()..]))
    } else {
        (raw, None)
    }
}

#[test]
fn support_matrix_loads() {
    let matrix = generated_theory_support_matrix().expect("load support matrix");
    assert!(
        !matrix.rows.is_empty(),
        "support matrix must contain at least one row"
    );
    println!("matrix has {} rows", matrix.rows.len());
}

#[test]
fn every_row_has_at_least_one_test() {
    let matrix = generated_theory_support_matrix().expect("load support matrix");
    let orphans: Vec<String> = matrix
        .rows
        .iter()
        .filter(|r| r.tests.is_empty())
        .map(|r| {
            format!(
                "domain={} operator={} backend={}",
                r.domain, r.operator, r.backend
            )
        })
        .collect();
    assert!(
        orphans.is_empty(),
        "{} row(s) have an empty tests vector: {orphans:#?}",
        orphans.len()
    );
}

#[test]
fn every_referenced_test_file_exists() {
    let matrix = generated_theory_support_matrix().expect("load support matrix");
    let mut missing: Vec<String> = Vec::new();
    let mut seen: std::collections::BTreeSet<String> = std::collections::BTreeSet::new();
    for row in &matrix.rows {
        for raw in &row.tests {
            let (path, _features) = split_path_and_features(raw);
            if !seen.insert(path.to_string()) {
                continue;
            }
            if !Path::new(path).exists() {
                missing.push(format!(
                    "row[domain={} operator={} backend={}] references missing test file: {path}",
                    row.domain, row.operator, row.backend
                ));
            }
        }
    }
    assert!(
        missing.is_empty(),
        "{} test file(s) referenced by the support matrix are missing:\n{}",
        missing.len(),
        missing.join("\n")
    );
}

#[test]
fn every_referenced_public_api_path_exists() {
    let matrix = generated_theory_support_matrix().expect("load support matrix");
    let mut missing: Vec<String> = Vec::new();
    for row in &matrix.rows {
        let api_path = row.public_api.trim();
        if api_path.is_empty() {
            missing.push(format!(
                "row[domain={} operator={} backend={}] has empty public_api",
                row.domain, row.operator, row.backend
            ));
            continue;
        }
        let first = api_path.split_whitespace().next().unwrap_or("");
        if first.starts_with("src/") && first.ends_with(".rs") && !Path::new(first).exists() {
            missing.push(format!(
                "row[domain={} operator={} backend={}] references missing public API path: {first}",
                row.domain, row.operator, row.backend
            ));
        }
    }
    assert!(
        missing.is_empty(),
        "{} public_api path(s) referenced by the support matrix are missing:\n{}",
        missing.len(),
        missing.join("\n")
    );
}

#[test]
fn matrix_references_post_p353_surface_files() {
    let matrix = generated_theory_support_matrix().expect("load support matrix");
    let expected: &[&str] = &[
        "tests/arithmetic_ops.rs",
        "tests/shape_ops.rs",
        "tests/nn_ops.rs",
        "tests/index_ops.rs",
        "tests/reductions.rs",
        "tests/finite_field.rs",
        "tests/padic_witnesses.rs",
        "tests/cover_glue_inference.rs",
    ];
    let all_tests: std::collections::BTreeSet<String> = matrix
        .rows
        .iter()
        .flat_map(|r| r.tests.iter().cloned())
        .map(|s| split_path_and_features(&s).0.to_string())
        .collect();
    let mut missing: Vec<&str> = Vec::new();
    for path in expected {
        if !all_tests.contains(*path) {
            missing.push(path);
        }
    }
    assert!(
        missing.is_empty(),
        "support matrix is missing evidence for: {missing:#?}"
    );
}

#[test]
fn matrix_rows_carry_a_lowering_rule_id_or_are_pilot_rows() {
    let matrix = generated_theory_support_matrix().expect("load support matrix");
    let orphans: Vec<String> = matrix
        .rows
        .iter()
        .filter(|r| r.lowering_rule_id.is_none() && !is_pilot_row(r))
        .map(|r| {
            format!(
                "row[domain={} operator={} backend={}] has no lowering_rule_id and is not a known pilot row",
                r.domain, r.operator, r.backend
            )
        })
        .collect();
    assert!(
        orphans.is_empty(),
        "{} row(s) are missing a lowering_rule_id: {orphans:#?}",
        orphans.len()
    );
}

fn is_pilot_row(row: &tokitai_operator::verify::TheorySupportMatrixRow) -> bool {
    let s = format!(
        "{} {} {} {} {}",
        row.public_api, row.fallback_mode, row.backend_capability, row.domain, row.operator
    );
    s.contains("pilot")
        || s.contains("unavailable")
        || s.contains("Hardware contract")
        || s.contains("p-adic")
        || s.contains("valuation")
        || s.contains("sheaf")
        || s.contains("stratified")
        || s.contains("sheaf-locality")
        || s.contains("finite_field")
        || s.contains("cover_glue")
        || row.operator == "valuation_witnesses"
        || row.operator == "cover_glue_inference"
        || row.operator == "finite_field_arithmetic"
}

#[test]
fn matrix_unique_domain_operator_pairs_sanity() {
    let matrix = generated_theory_support_matrix().expect("load support matrix");
    let mut seen: std::collections::BTreeSet<(String, String)> = std::collections::BTreeSet::new();
    let mut triple_seen: std::collections::BTreeSet<(String, String, String)> =
        std::collections::BTreeSet::new();
    let mut dups = 0usize;
    for row in &matrix.rows {
        seen.insert((row.domain.clone(), row.operator.clone()));
        if !triple_seen.insert((
            row.domain.clone(),
            row.operator.clone(),
            row.backend.clone(),
        )) {
            dups += 1;
        }
    }
    println!(
        "support matrix: {} unique (domain, operator) pairs, {} duplicate (domain, operator, backend) triples",
        seen.len(),
        dups
    );
    if dups > 0 {
        // Diagnostic: per-triple detail.
        let matrix = generated_theory_support_matrix().expect("load");
        let mut dup_count: std::collections::BTreeMap<
            (String, String, String),
            Vec<&tokitai_operator::verify::TheorySupportMatrixRow>,
        > = std::collections::BTreeMap::new();
        for r in &matrix.rows {
            dup_count
                .entry((r.domain.clone(), r.operator.clone(), r.backend.clone()))
                .or_default()
                .push(r);
        }
        for (triple, rows) in &dup_count {
            if rows.len() > 1 {
                println!(
                    "  duplicate (n={}): {} | {} | {}",
                    rows.len(),
                    triple.0,
                    triple.1,
                    triple.2
                );
                for (i, r) in rows.iter().enumerate() {
                    println!(
                        "    [{}] lr_id={:?} status={:?}",
                        i, r.lowering_rule_id, r.support_status
                    );
                }
            }
        }
    }
    assert!(
        seen.len() >= 30,
        "expected at least 30 unique (domain, operator) pairs, got {}",
        seen.len()
    );
    // P369: this is now <= the original 8 because the
    // pilot+lowering-rule overlap has been resolved. Some dups
    // remain (e.g. two distinct Q_* matmul rules), but the
    // pseudo-dups (pilot row + lowering-rule row on the same
    // quadruple) are gone.
    assert!(
        dups <= 8,
        "expected at most 8 duplicate triples after P369, got {dups}"
    );
}