tokitai-operator 0.1.0

//! Theory-aware support matrix.
//!
//! `generated_theory_support_matrix` builds the public surface
//! index: one row per `(domain, operator, backend)` triple with
//! status, theory constraints, theorem packages, fallback mode,
//! public API path, and the test file(s) that exercise it. The
//! matrix is the source-of-truth for `docs/theory_support_matrix.md`
//! and is walked fail-closed by `tests/support_matrix_coverage.rs`.
//!
//! After P369 the matrix de-duplicates redundant `Supported` rows
//! that are shadowed by a more-specific pilot / unavailable row.
//! After P382 the remaining 8 irreducible duplicates are classified
//! as `MultiState` (4) or `MultiRule` (4) — see
//! `support_matrix_dedup_classify.rs`.
//!
use crate::backend::BackendCapabilities;
use crate::backend::gpu::GpuScaffoldBackend;
use crate::op::{LoweringRule, OperatorRegistry};
use crate::theory::TheoryId;
use crate::verify::TheoremBindingRegistry;
use crate::{Error, Result};

pub const THEORY_SUPPORT_MATRIX_ARTIFACT: &str = "tokitai-theory-support-matrix";
pub const THEORY_SUPPORT_MATRIX_VERSION: u32 = 1;

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum SupportStatus {
    Supported,
    FallbackOnly,
    Unsupported,
    FeatureGatedPilot,
    LocalHardwareEvidence,
    Unavailable,
}

impl SupportStatus {
    pub fn as_str(&self) -> &'static str {
        match self {
            Self::Supported => "supported",
            Self::FallbackOnly => "fallback_only",
            Self::Unsupported => "unsupported",
            Self::FeatureGatedPilot => "feature_gated_pilot",
            Self::LocalHardwareEvidence => "local_hardware_evidence",
            Self::Unavailable => "unavailable",
        }
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheorySupportMatrixRow {
    pub domain: String,
    pub operator: String,
    pub theory_constraints: Vec<String>,
    pub theorem_packages: Vec<String>,
    pub backend: String,
    pub backend_capability: String,
    pub lowering_rule_id: Option<String>,
    pub support_status: SupportStatus,
    pub fallback_mode: String,
    pub public_api: String,
    pub tests: Vec<String>,
    pub non_claims: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheorySupportMatrix {
    pub artifact: String,
    pub version: u32,
    pub rows: Vec<TheorySupportMatrixRow>,
}

impl TheorySupportMatrix {
    pub fn to_markdown(&self) -> String {
        let mut lines = vec![
            "# Theory-Aware Support Matrix".to_string(),
            String::new(),
            "| Domain | Operator | Backend | Status | Theory constraints | Theorem packages | Fallback | Public API | Tests | Non-claims |".to_string(),
            "| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |".to_string(),
        ];
        for row in &self.rows {
            lines.push(format!(
                "| {} | {} | {} | {} | {} | {} | {} | {} | {} | {} |",
                md(&row.domain),
                md(&row.operator),
                md(&row.backend),
                row.support_status.as_str(),
                md(&row.theory_constraints.join("<br>")),
                md(&row.theorem_packages.join("<br>")),
                md(&row.fallback_mode),
                md(&row.public_api),
                md(&row.tests.join("<br>")),
                md(&row.non_claims.join("<br>"))
            ));
        }
        lines.join("\n")
    }

    pub fn to_json(&self) -> String {
        let rows = self
            .rows
            .iter()
            .map(TheorySupportMatrixRow::to_json)
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"artifact\":{},\"version\":{},\"rows\":[{}]}}",
            json_string(&self.artifact),
            self.version,
            rows
        )
    }
}

impl TheorySupportMatrixRow {
    fn to_json(&self) -> String {
        format!(
            "{{\"domain\":{},\"operator\":{},\"theory_constraints\":{},\"theorem_packages\":{},\"backend\":{},\"backend_capability\":{},\"lowering_rule_id\":{},\"support_status\":{},\"fallback_mode\":{},\"public_api\":{},\"tests\":{},\"non_claims\":{}}}",
            json_string(&self.domain),
            json_string(&self.operator),
            json_array(&self.theory_constraints),
            json_array(&self.theorem_packages),
            json_string(&self.backend),
            json_string(&self.backend_capability),
            json_option_string(&self.lowering_rule_id),
            json_string(self.support_status.as_str()),
            json_string(&self.fallback_mode),
            json_string(&self.public_api),
            json_array(&self.tests),
            json_array(&self.non_claims)
        )
    }
}

pub fn generated_theory_support_matrix() -> Result<TheorySupportMatrix> {
    let registry = OperatorRegistry::cpu_scalar_builtins()?;
    let theorem_registry = TheoremBindingRegistry::tokitai_default()?;
    theory_support_matrix_from_sources(
        &registry,
        &theorem_registry,
        &BackendCapabilities::cpu_scalar(),
        &GpuScaffoldBackend::capabilities(),
    )
}

/// # Example
///
/// ```
/// use tokitai_operator::verify::generated_theory_support_matrix;
/// let matrix = generated_theory_support_matrix().expect("support matrix");
/// assert!(!matrix.rows.is_empty(), "matrix must have at least one row");
/// let md = matrix.to_markdown();
/// assert!(md.starts_with("# Theory-Aware Support Matrix"));
/// assert!(md.contains("| Domain | Operator | Backend | Status |"));
/// ```

pub fn theory_support_matrix_from_sources(
    registry: &OperatorRegistry,
    theorem_registry: &TheoremBindingRegistry,
    cpu_capabilities: &BackendCapabilities,
    gpu_scaffold_capabilities: &BackendCapabilities,
) -> Result<TheorySupportMatrix> {
    let mut rows = Vec::new();
    for rule in registry.lowering_registry().rules() {
        rows.push(cpu_lowering_row(rule, theorem_registry, cpu_capabilities)?);
        rows.push(gpu_scaffold_row(
            rule,
            theorem_registry,
            gpu_scaffold_capabilities,
        )?);
    }
    rows.push(accelerated_pilot_row());
    rows.push(rocm_hip_hardware_contract_row());
    rows.push(rocm_hip_dense_i32_pilot_row());
    rows.push(rocm_hip_dense_i32_unavailable_row());
    rows.push(rocm_hip_padic_valuation_pilot_row());
    rows.push(rocm_hip_padic_valuation_unavailable_row());
    rows.push(rocm_hip_padic_stratified_matmul_pilot_row());
    rows.push(rocm_hip_padic_stratified_benchmark_suite_row());
    rows.push(rocm_hip_padic_stratified_matmul_unavailable_row());
    rows.push(rocm_hip_sheaf_locality_pilot_row());
    rows.push(rocm_hip_sheaf_locality_fallback_row());
    // P346-P348: P335-P348 surface evidence
    rows.push(p346_finite_field_domain_row());
    rows.push(p347_valuation_witnesses_row());
    rows.push(p348_cover_glue_inference_row());
    rows.sort_by(|lhs, rhs| {
        (
            lhs.domain.as_str(),
            lhs.operator.as_str(),
            lhs.backend.as_str(),
            lhs.lowering_rule_id.as_deref().unwrap_or(""),
        )
            .cmp(&(
                rhs.domain.as_str(),
                rhs.operator.as_str(),
                rhs.backend.as_str(),
                rhs.lowering_rule_id.as_deref().unwrap_or(""),
            ))
    });
    // P369: de-duplicate rows that are *redundant* with another row
    // on the same (domain, operator, backend, lowering_rule_id)
    // quadruple. A row is "redundant" iff its support_status is the
    // generic `Supported` AND another row exists for the same
    // quadruple. The more-specific pilot and unavailable rows
    // (which carry status=FeatureGatedPilot or Unavailable) are
    // always kept. This preserves the test contract: the explicit
    // `rocm_hip_dense_i32_pilot` pilot row and the
    // `rocm_hip_dense_i32_unavailable` row both coexist for the
    // same (domain, operator, backend, lowering_rule_id).
    let mut seen_with_specific_status: std::collections::BTreeSet<(
        String,
        String,
        String,
        String,
    )> = std::collections::BTreeSet::new();
    for r in &rows {
        if !matches!(r.support_status, SupportStatus::Supported) {
            let key = (
                r.domain.clone(),
                r.operator.clone(),
                r.backend.clone(),
                r.lowering_rule_id.clone().unwrap_or_default(),
            );
            seen_with_specific_status.insert(key);
        }
    }
    rows.retain(|r| {
        if matches!(r.support_status, SupportStatus::Supported) {
            let key = (
                r.domain.clone(),
                r.operator.clone(),
                r.backend.clone(),
                r.lowering_rule_id.clone().unwrap_or_default(),
            );
            !seen_with_specific_status.contains(&key)
        } else {
            true
        }
    });
    Ok(TheorySupportMatrix {
        artifact: THEORY_SUPPORT_MATRIX_ARTIFACT.to_string(),
        version: THEORY_SUPPORT_MATRIX_VERSION,
        rows,
    })
}

fn rocm_hip_dense_i32_pilot_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "integer".to_string(),
        operator: "add".to_string(),
        theory_constraints: vec![
            "cpu_oracle_elementwise_equality_required".to_string(),
            "rocm_hip_hardware_contract_required".to_string(),
        ],
        theorem_packages: vec!["none".to_string()],
        backend: "rocm_hip_dense_i32_pilot".to_string(),
        backend_capability:
            "feature-gated rocm-hip; real HIP dense_i32_add kernel; source and compiler fingerprints; CPU oracle comparison"
                .to_string(),
        lowering_rule_id: Some("hip.add.dense_i32".to_string()),
        support_status: SupportStatus::FeatureGatedPilot,
        fallback_mode:
            "feature must be enabled and ROCm/HIP must be available; default builds keep CPU execution"
                .to_string(),
        public_api: "cargo run --quiet --offline --features rocm-hip --example rocm_dense_pilot"
            .to_string(),
        tests: vec![
            "tests/rocm_hip_dense.rs --features rocm-hip".to_string(),
            "tests/rocm_audit_traces.rs --features rocm-hip".to_string(),
        ],
        non_claims: vec![
            "not broad GPU support".to_string(),
            "not p-adic or finite-site sheaf acceleration".to_string(),
            "not production performance evidence".to_string(),
            "not machine-code verification".to_string(),
        ],
    }
}

fn rocm_hip_dense_i32_unavailable_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "integer".to_string(),
        operator: "add".to_string(),
        theory_constraints: vec!["cpu_oracle_remains_default".to_string()],
        theorem_packages: vec!["none".to_string()],
        backend: "rocm_hip_dense_i32_pilot".to_string(),
        backend_capability:
            "ROCm/HIP unavailable, wrong gfx target, missing kernel source, stale compiler fingerprint, or missing transfer obligations"
                .to_string(),
        lowering_rule_id: Some("hip.add.dense_i32".to_string()),
        support_status: SupportStatus::Unavailable,
        fallback_mode:
            "HIP lowering admission fails closed; dense integer add remains executable on cpu_scalar"
                .to_string(),
        public_api: "default cargo test --offline does not require ROCm/HIP".to_string(),
        tests: vec![
            "tests/rocm_hip_lowering.rs --features rocm-hip".to_string(),
            "tests/rocm_audit_traces.rs --features rocm-hip".to_string(),
        ],
        non_claims: vec![
            "not portable AMD GPU support".to_string(),
            "not silent GPU fallback".to_string(),
            "not production performance evidence".to_string(),
        ],
    }
}

fn rocm_hip_padic_valuation_pilot_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "padic:fixed_precision".to_string(),
        operator: "valuation".to_string(),
        theory_constraints: vec![
            "padic:valuation:valuation_skip_sound_mod_pk".to_string(),
            "cpu_oracle_padic_valuation_required".to_string(),
        ],
        theorem_packages: vec![
            "tokitai_padic_valuation_skip_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
        ],
        backend: "rocm_hip_padic_valuation_pilot".to_string(),
        backend_capability:
            "feature-gated rocm-hip; fixed-precision p-adic residue valuation helper; zero maps to precision cutoff; CPU oracle comparison"
                .to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::FeatureGatedPilot,
        fallback_mode:
            "feature must be enabled and ROCm/HIP must be available; CPU p-adic semantics remain authoritative"
                .to_string(),
        public_api:
            "cargo run --quiet --offline --features rocm-hip --example rocm_padic_valuation"
                .to_string(),
        tests: vec![
            "tests/rocm_padic_valuation.rs --features rocm-hip".to_string(),
            "tests/rocm_audit_traces.rs --features rocm-hip".to_string(),
            "scripts/check_padic_valuation_skip_theorem.sh".to_string(),
        ],
        non_claims: vec![
            "not full p-adic algebra".to_string(),
            "not arbitrary precision p-adic fields".to_string(),
            "not broad p-adic GPU acceleration".to_string(),
            "not production performance evidence".to_string(),
        ],
    }
}

/// P347: valuation witness evidence row. The witness types
/// (ValuationAdditivityWitness, UltrametricWitness,
/// PrecisionPreservationWitness) live in src/verify/witnesses.rs and are
/// exercised by tests/padic_witnesses.rs. The row documents the
/// CPU-reference evidence; no lowering rule, no GPU path.
fn p347_valuation_witnesses_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "padic:fixed_precision".to_string(),
        operator: "valuation_witnesses".to_string(),
        theory_constraints: vec![
            "padic:valuation:additivity_observed".to_string(),
            "padic:valuation:ultrametric_observed".to_string(),
            "padic:valuation:precision_preservation_observed".to_string(),
        ],
        theorem_packages: vec![
            "tokitai_padic_valuation_skip_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
        ],
        backend: "cpu_scalar".to_string(),
        backend_capability:
            "CPU-reference evidence only; no lowering rule, no GPU execution; 3 witness types exercised by tests/padic_witnesses.rs"
                .to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::Supported,
        fallback_mode: "witnesses are CPU-reference; no fallback path".to_string(),
        public_api: "src/verify/witnesses.rs (pub use re-export from src/verify/mod.rs)"
            .to_string(),
        tests: vec!["tests/padic_witnesses.rs".to_string()],
        non_claims: vec![
            "not a formal proof of the ultrametric inequality".to_string(),
            "not a witness of full p-adic algebra".to_string(),
            "not a production speedup claim".to_string(),
        ],
    }
}

/// P348: cover-glue inference evidence row. The inference report
/// (CoverGlueInferenceReport, InferenceAttempt enum) lives in
/// src/verify/cover_glue_inference.rs and is exercised by
/// tests/cover_glue_inference.rs. The row documents the
/// CPU-reference glue-side enhancement; no lowering rule, no GPU path.
fn p348_cover_glue_inference_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "sheaf:finite_site".to_string(),
        operator: "cover_glue_inference".to_string(),
        theory_constraints: vec![
            "sheaf:finite_site:restriction_compatibility".to_string(),
            "sheaf:finite_site:obstruction_recovery_attempted".to_string(),
        ],
        theorem_packages: vec![
            "tokitai_finite_sheaf_gluing_sound (docs/theorems/finite_sheaf_gluing.lean)"
                .to_string(),
        ],
        backend: "cpu_scalar".to_string(),
        backend_capability:
            "CPU-reference glue-side recovery; 3 inference variants (InferredMissingSection, ResolvedOverlap, FailedRecovery); fail-closed on FailedRecovery"
                .to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::Supported,
        fallback_mode: "no fallback; failures stay FailedRecovery and the verifier stays fail-closed".to_string(),
        public_api: "src/verify/cover_glue_inference.rs (pub use re-export from src/verify/mod.rs)"
            .to_string(),
        tests: vec![
            "tests/cover_glue_inference.rs".to_string(),
            "tests/sheaf.rs".to_string(),
        ],
        non_claims: vec![
            "not H^0 / H^1 computation".to_string(),
            "not Cech cohomology".to_string(),
            "not general sheaf cohomology".to_string(),
        ],
    }
}

/// P346: finite-field domain evidence row. The domain type
/// (FiniteFieldDomain, FiniteFieldElement) lives in
/// src/domain/finite_field.rs and is exercised by
/// tests/finite_field.rs. The row documents the
/// domain-completeness extension; no lowering rule, no GPU path.
fn p346_finite_field_domain_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "finite_field:F_p^k".to_string(),
        operator: "finite_field_arithmetic".to_string(),
        theory_constraints: vec![
            "finite_field:associative".to_string(),
            "finite_field:commutative".to_string(),
            "finite_field:has_identity".to_string(),
            "finite_field:has_inverse".to_string(),
            "finite_field:exact".to_string(),
        ],
        theorem_packages: vec![
            "finite_field_spec_contract (src/domain/contract.rs::Claim::FiniteFieldSpec)"
                .to_string(),
        ],
        backend: "cpu_scalar".to_string(),
        backend_capability:
            "CPU-reference domain; supports prime fields F_p and extension fields F_{p^k} via polynomial-mod-irreducible multiplication; 12 tests + 2 doctests"
                .to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::Supported,
        fallback_mode: "no fallback; domain is exact by construction".to_string(),
        public_api: "src/domain/finite_field.rs (pub use re-export from src/domain/mod.rs)"
            .to_string(),
        tests: vec!["tests/finite_field.rs".to_string()],
        non_claims: vec![
            "not a p-adic finite field extension".to_string(),
            "not Galois group computation".to_string(),
            "not a polynomial ring over a finite field".to_string(),
            "not GPU lowering".to_string(),
        ],
    }
}

fn rocm_hip_padic_valuation_unavailable_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "padic:fixed_precision".to_string(),
        operator: "valuation".to_string(),
        theory_constraints: vec!["cpu_padic_oracle_remains_default".to_string()],
        theorem_packages: vec![
            "tokitai_padic_valuation_skip_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
        ],
        backend: "rocm_hip_padic_valuation_pilot".to_string(),
        backend_capability: "ROCm/HIP unavailable or p-adic valuation helper not built".to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::Unavailable,
        fallback_mode:
            "HIP p-adic helper is skipped; fixed-precision p-adic CPU oracle remains the supported path"
                .to_string(),
        public_api: "default cargo test --offline does not require ROCm/HIP".to_string(),
        tests: vec![
            "tests/rocm_padic_valuation.rs --features rocm-hip".to_string(),
            "tests/rocm_audit_traces.rs --features rocm-hip".to_string(),
        ],
        non_claims: vec![
            "not full p-adic algebra".to_string(),
            "not portable p-adic GPU support".to_string(),
            "not production performance evidence".to_string(),
        ],
    }
}

fn rocm_hip_padic_stratified_matmul_pilot_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "padic:fixed_precision".to_string(),
        operator: "matmul".to_string(),
        theory_constraints: vec![
            "padic:valuation:valuation_skip_sound_mod_pk".to_string(),
            "padic:valuation:valuation_skip_dot_product_sound_mod_pk".to_string(),
            "dense_cpu_oracle_required".to_string(),
            "certified_sparse_cpu_oracle_required".to_string(),
            "per_output_certificate_required".to_string(),
        ],
        theorem_packages: vec![
            "tokitai_padic_valuation_skip_dot_product_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
            "tokitai_padic_valuation_skip_matrix_output_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
        ],
        backend: "rocm_hip_padic_stratified_matmul_pilot".to_string(),
        backend_capability:
            "feature-gated rocm-hip; Q_5[3] 2x3x2 valuation-stratified p-adic matmul kernel; dense/sparse CPU oracle and certificate comparison"
                .to_string(),
        lowering_rule_id: Some("cpu.matmul.padic_valuation_stratified".to_string()),
        support_status: SupportStatus::FeatureGatedPilot,
        fallback_mode:
            "feature must be enabled and ROCm/HIP must be available; CPU dense and certified sparse oracles remain authoritative"
                .to_string(),
        public_api:
            "cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_matmul"
                .to_string(),
        tests: vec![
            "tests/rocm_padic_stratified_matmul.rs --features rocm-hip".to_string(),
            "tests/rocm_padic_stratified_benchmarks.rs --features rocm-hip".to_string(),
            "tests/padic.rs".to_string(),
            "tests/padic_valuation_skip_theorem.rs".to_string(),
        ],
        non_claims: vec![
            "not full p-adic algebra".to_string(),
            "not arbitrary precision p-adic fields".to_string(),
            "not broad p-adic GPU acceleration".to_string(),
            "not portable AMD GPU support".to_string(),
            "not production performance evidence".to_string(),
        ],
    }
}

fn rocm_hip_padic_stratified_benchmark_suite_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "padic:fixed_precision".to_string(),
        operator: "matmul_benchmark_matrix".to_string(),
        theory_constraints: vec![
            "padic:valuation:valuation_skip_dot_product_sound_mod_pk".to_string(),
            "padic:valuation:valuation_skip_matrix_output_sound_mod_pk".to_string(),
            "dense_cpu_oracle_required".to_string(),
            "certified_sparse_cpu_oracle_required".to_string(),
            "hip_or_fallback_row_required".to_string(),
            "benchmark_distribution_coverage_required".to_string(),
            "speed_claim_guard_required".to_string(),
        ],
        theorem_packages: vec![
            "tokitai_padic_valuation_skip_dot_product_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
            "tokitai_padic_valuation_skip_matrix_output_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
        ],
        backend: "rocm_hip_padic_stratified_benchmark_suite".to_string(),
        backend_capability:
            "feature-gated rocm-hip; deterministic valuation distributions; dense CPU, certified sparse CPU, HIP stratified, and fallback benchmark rows"
                .to_string(),
        lowering_rule_id: Some("cpu.matmul.padic_valuation_stratified".to_string()),
        support_status: SupportStatus::FeatureGatedPilot,
        fallback_mode:
            "unsupported prime, precision, or shape rows must be explicit fallback evidence with CPU oracles"
                .to_string(),
        public_api:
            "cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks"
                .to_string(),
        tests: vec![
            "tests/rocm_padic_stratified_benchmarks.rs --features rocm-hip".to_string(),
            "tests/rocm_paper_gate.rs --features rocm-hip".to_string(),
            "tests/theory_release_gate.rs".to_string(),
        ],
        non_claims: vec![
            "not full p-adic algebra".to_string(),
            "not arbitrary precision p-adic fields".to_string(),
            "not portable AMD GPU support".to_string(),
            "not verified HIP machine code".to_string(),
            "not production speedup evidence".to_string(),
        ],
    }
}

fn rocm_hip_padic_stratified_matmul_unavailable_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "padic:fixed_precision".to_string(),
        operator: "matmul".to_string(),
        theory_constraints: vec!["cpu_padic_oracles_remain_default".to_string()],
        theorem_packages: vec![
            "tokitai_padic_valuation_skip_dot_product_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
            "tokitai_padic_valuation_skip_matrix_output_sound_mod_pk (docs/theorems/padic_valuation_skip.lean)"
                .to_string(),
        ],
        backend: "rocm_hip_padic_stratified_matmul_pilot".to_string(),
        backend_capability:
            "ROCm/HIP unavailable or p-adic stratified matmul helper not built".to_string(),
        lowering_rule_id: Some("cpu.matmul.padic_valuation_stratified".to_string()),
        support_status: SupportStatus::Unavailable,
        fallback_mode:
            "HIP p-adic matmul helper is skipped; dense CPU and certified sparse CPU oracles remain the supported path"
                .to_string(),
        public_api: "default cargo test --offline does not require ROCm/HIP".to_string(),
        tests: vec![
            "tests/rocm_padic_stratified_matmul.rs --features rocm-hip".to_string(),
            "tests/padic.rs".to_string(),
        ],
        non_claims: vec![
            "not full p-adic algebra".to_string(),
            "not portable p-adic GPU support".to_string(),
            "not production performance evidence".to_string(),
        ],
    }
}

fn rocm_hip_sheaf_locality_pilot_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "sheaf:finite_site".to_string(),
        operator: "overlap_compatibility".to_string(),
        theory_constraints: vec![
            "sheaf:finite_site:finite_sheaf_gluing_sound".to_string(),
            "SectionTable_obstruction_oracle_required".to_string(),
        ],
        theorem_packages: vec![
            "tokitai_finite_sheaf_gluing_sound (docs/theorems/finite_sheaf_gluing.lean)"
                .to_string(),
        ],
        backend: "rocm_hip_sheaf_locality_pilot".to_string(),
        backend_capability:
            "feature-gated rocm-hip; finite-site overlap equality helper; CPU SectionTable compatibility and obstruction oracle"
                .to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::FeatureGatedPilot,
        fallback_mode:
            "feature must be enabled and ROCm/HIP must be available; CPU SectionTable report remains authoritative"
                .to_string(),
        public_api:
            "cargo run --quiet --offline --features rocm-hip --example rocm_sheaf_locality"
                .to_string(),
        tests: vec![
            "tests/rocm_sheaf_locality.rs --features rocm-hip".to_string(),
            "tests/rocm_audit_traces.rs --features rocm-hip".to_string(),
            "scripts/check_finite_sheaf_gluing_theorem.sh".to_string(),
        ],
        non_claims: vec![
            "not general sheaf theory".to_string(),
            "not sheaf cohomology".to_string(),
            "not global repair synthesis".to_string(),
            "not production performance evidence".to_string(),
        ],
    }
}

fn rocm_hip_sheaf_locality_fallback_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "sheaf:finite_site".to_string(),
        operator: "overlap_compatibility".to_string(),
        theory_constraints: vec!["SectionTable_obstruction_oracle_required".to_string()],
        theorem_packages: vec![
            "tokitai_finite_sheaf_gluing_sound (docs/theorems/finite_sheaf_gluing.lean)"
                .to_string(),
        ],
        backend: "rocm_hip_sheaf_locality_pilot".to_string(),
        backend_capability:
            "missing overlap, missing section, invalid cover, or unavailable ROCm/HIP triggers fail-closed CPU provenance"
                .to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::FallbackOnly,
        fallback_mode:
            "HIP helper does not execute when finite-site obstruction provenance cannot be represented on device"
                .to_string(),
        public_api: "default cargo test --offline does not require ROCm/HIP".to_string(),
        tests: vec![
            "tests/rocm_sheaf_locality.rs --features rocm-hip".to_string(),
            "tests/rocm_audit_traces.rs --features rocm-hip".to_string(),
        ],
        non_claims: vec![
            "not general sheaf theory".to_string(),
            "not sheaf cohomology".to_string(),
            "not silent obstruction repair".to_string(),
        ],
    }
}

fn rocm_hip_hardware_contract_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "hardware:rocm_hip".to_string(),
        operator: "hardware_contract".to_string(),
        theory_constraints: vec![
            "device_capability_fingerprint_required".to_string(),
            "cpu_oracle_required_before_kernel_admission".to_string(),
        ],
        theorem_packages: vec!["none".to_string()],
        backend: "rocm_hip_hardware_contract".to_string(),
        backend_capability:
            "local ROCm/HIP detector; records device, gfx target, VRAM, compute units, hipcc, and driver evidence; no kernel execution"
                .to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::LocalHardwareEvidence,
        fallback_mode:
            "ROCm unavailable or incomplete evidence keeps HIP lowerings inadmissible and leaves CPU oracle as default"
                .to_string(),
        public_api: "cargo run --quiet --offline --example rocm_capabilities".to_string(),
        tests: vec![
            "tests/rocm_capabilities.rs".to_string(),
            "tests/theory_support_matrix.rs".to_string(),
        ],
        non_claims: vec![
            "not a HIP kernel execution claim".to_string(),
            "not portable AMD GPU support".to_string(),
            "not p-adic or finite-site sheaf acceleration".to_string(),
            "not production performance evidence".to_string(),
        ],
    }
}

fn cpu_lowering_row(
    rule: &LoweringRule,
    theorem_registry: &TheoremBindingRegistry,
    capabilities: &BackendCapabilities,
) -> Result<TheorySupportMatrixRow> {
    let theorem_packages = theorem_packages(rule, theorem_registry)?;
    Ok(TheorySupportMatrixRow {
        domain: domain_scope(rule),
        operator: rule.op_name.clone(),
        theory_constraints: theory_constraints(rule),
        theorem_packages,
        backend: rule.backend.clone(),
        backend_capability: backend_capability_summary(capabilities),
        lowering_rule_id: Some(rule.id.0.clone()),
        support_status: SupportStatus::Supported,
        fallback_mode: "none; CPU oracle/backend is the support boundary".to_string(),
        public_api: public_api_for(rule),
        tests: tests_for(rule),
        non_claims: non_claims_for(rule),
    })
}

fn gpu_scaffold_row(
    rule: &LoweringRule,
    theorem_registry: &TheoremBindingRegistry,
    capabilities: &BackendCapabilities,
) -> Result<TheorySupportMatrixRow> {
    let domain = domain_scope(rule);
    let fallback_mode = if is_padic_domain_scope(&domain) {
        "gpu_scaffold rejects fixed-precision p-adic execution; prefer-gpu facade falls back to cpu_scalar"
    } else if is_sheaf_domain_scope(&domain) {
        "gpu_scaffold rejects finite-site sheaf locality; prefer-gpu facade falls back to cpu_scalar"
    } else {
        "gpu_scaffold has no executable kernel; prefer-gpu facade falls back to cpu_scalar"
    };
    let mut non_claims = non_claims_for(rule);
    non_claims.push(
        "GPU scaffold rows are fallback evidence, not nonstandard-domain acceleration".to_string(),
    );
    Ok(TheorySupportMatrixRow {
        domain,
        operator: rule.op_name.clone(),
        theory_constraints: theory_constraints(rule),
        theorem_packages: theorem_packages(rule, theorem_registry)?,
        backend: capabilities.name.clone(),
        backend_capability: backend_capability_summary(capabilities),
        // P369: include the rule's lowering_rule_id so the row is
        // uniquely identified within (domain, operator, backend)
        // for the dedup pass. Without this, multiple rules with the
        // same op_name in the same domain (e.g. 3 Q_* matmul rules)
        // produce identical rows and are reported as duplicates.
        lowering_rule_id: Some(rule.id.0.clone()),
        support_status: SupportStatus::FallbackOnly,
        fallback_mode: fallback_mode.to_string(),
        public_api: public_api_for(rule),
        tests: gpu_tests_for(rule),
        non_claims,
    })
}

fn accelerated_pilot_row() -> TheorySupportMatrixRow {
    TheorySupportMatrixRow {
        domain: "integer".to_string(),
        operator: "add".to_string(),
        theory_constraints: vec!["none".to_string()],
        theorem_packages: vec!["none".to_string()],
        backend: "gpu_dense_i64_pilot".to_string(),
        backend_capability:
            "feature-gated accelerated-pilot; dense_i64_add_only; no device allocator or streams"
                .to_string(),
        lowering_rule_id: None,
        support_status: SupportStatus::FeatureGatedPilot,
        fallback_mode: "feature must be enabled; CPU oracle comparison remains the guardrail"
            .to_string(),
        public_api: "not exposed as nonstandard public API; internal feature-gated pilot only"
            .to_string(),
        tests: vec!["tests/accelerated_pilot.rs --features accelerated-pilot".to_string()],
        non_claims: vec![
            "not broad GPU support".to_string(),
            "not p-adic or finite-site sheaf acceleration".to_string(),
            "not production performance evidence".to_string(),
        ],
    }
}

fn theorem_packages(
    rule: &LoweringRule,
    theorem_registry: &TheoremBindingRegistry,
) -> Result<Vec<String>> {
    let mut packages = Vec::new();
    for requirement in &rule.theory_requirements {
        if let Some(theorem_id) = &requirement.theorem_id {
            let descriptor = theorem_registry.lookup(theorem_id).map_err(|_| {
                Error::verification(format!(
                    "support matrix lowering {} references unknown theorem {}",
                    rule.id.0, theorem_id
                ))
            })?;
            packages.push(format!(
                "{} ({})",
                descriptor.theorem_id, descriptor.lean_file
            ));
        }
    }
    if packages.is_empty() {
        packages.push("none".to_string());
    }
    packages.sort();
    packages.dedup();
    Ok(packages)
}

fn theory_constraints(rule: &LoweringRule) -> Vec<String> {
    let mut constraints = rule
        .theory_requirements
        .iter()
        .map(|requirement| format!("{}:{}", requirement.theory.as_str(), requirement.law_id))
        .collect::<Vec<_>>();
    if constraints.is_empty() {
        constraints.push("none".to_string());
    }
    constraints.sort();
    constraints.dedup();
    constraints
}

fn domain_scope(rule: &LoweringRule) -> String {
    if !rule.supported_domains.is_empty() {
        return rule.supported_domains.join("|");
    }
    let mut domains = rule
        .capabilities
        .iter()
        .map(|capability| format!("{:?}", capability.domain))
        .collect::<Vec<_>>();
    if domains.is_empty() {
        domains.push("any".to_string());
    }
    domains.sort();
    domains.dedup();
    domains.join("|")
}

fn backend_capability_summary(capabilities: &BackendCapabilities) -> String {
    format!(
        "exact={}, deterministic={}, domains={}, representations={}, degradations={}",
        capabilities.exact,
        capabilities.deterministic,
        capabilities.supported_domains.join("|"),
        capabilities.supported_representations.join("|"),
        if capabilities.semantic_degradations.is_empty() {
            "none".to_string()
        } else {
            capabilities.semantic_degradations.join("|")
        }
    )
}

fn public_api_for(rule: &LoweringRule) -> String {
    match rule.op_name.as_str() {
        "padic_sum_products_valuation_skip" => {
            "Tokitai::plan_padic_sum_products + Tokitai::execute_padic_sum_products".to_string()
        }
        "cover_glue_check" => {
            "Tokitai::plan_sheaf_glue_check + Tokitai::verify_sheaf_glue".to_string()
        }
        "add" | "mul" | "matmul" if is_padic_domain_scope(&domain_scope(rule)) => {
            "GraphBuilder/Tokitai::plan_public can plan; no typed p-adic graph execution facade"
                .to_string()
        }
        "add" | "mul" | "map" | "reduce" | "matmul" | "fused:add+map" => {
            "GraphBuilder/Tokitai::plan_public; Tokitai::execute_i64 for integer graph execution"
                .to_string()
        }
        _ => "no public facade exposure recorded".to_string(),
    }
}

fn tests_for(rule: &LoweringRule) -> Vec<String> {
    match rule.op_name.as_str() {
        "padic_sum_products_valuation_skip" => vec![
            "tests/padic.rs".to_string(),
            "tests/certified_contracts.rs".to_string(),
            "tests/semantic_conformance_report.rs".to_string(),
        ],
        "cover_glue_check" => vec![
            "tests/sheaf.rs".to_string(),
            "tests/finite_sheaf_gluing_theorem.rs".to_string(),
            "tests/certified_contracts.rs".to_string(),
        ],
        "reduce" => vec![
            "tests/operator_registry.rs".to_string(),
            "tests/certified_contracts.rs".to_string(),
        ],
        "matmul" if is_padic_domain_scope(&domain_scope(rule)) => vec![
            "tests/padic.rs".to_string(),
            "tests/nonstandard_cost_model.rs".to_string(),
            "tests/backend_lowering_cache.rs".to_string(),
            "tests/theorem_binding_registry.rs".to_string(),
            "tests/padic_valuation_skip_theorem.rs".to_string(),
        ],
        "add" | "mul" if is_padic_domain_scope(&domain_scope(rule)) => {
            vec!["tests/padic.rs".to_string()]
        }
        // P335: arithmetic expansion
        "sub" | "div" | "scalar_add" | "scalar_mul" | "pow" | "sqrt" | "exp2" | "log2" => vec![
            "tests/operator_registry.rs".to_string(),
            "tests/arithmetic_ops.rs".to_string(),
        ],
        // P336: shape ops
        "reshape" | "transpose" | "permute" | "slice" | "concat" | "broadcast" | "flatten"
        | "squeeze" | "unsqueeze" => vec![
            "tests/operator_registry.rs".to_string(),
            "tests/shape_ops.rs".to_string(),
        ],
        // P337: NN / activation ops
        "relu" | "sigmoid" | "tanh" | "gelu" | "softmax" | "layer_norm" => vec![
            "tests/operator_registry.rs".to_string(),
            "tests/nn_ops.rs".to_string(),
        ],
        // P338: index ops
        "gather" | "scatter" | "index_select" | "index_add" | "nonzero" => vec![
            "tests/operator_registry.rs".to_string(),
            "tests/index_ops.rs".to_string(),
        ],
        // P339: reduction ops
        "sum" | "mean" | "max" | "min" | "argmax" | "argmin" | "prod" | "any" | "all" => vec![
            "tests/operator_registry.rs".to_string(),
            "tests/reductions.rs".to_string(),
        ],
        _ => vec![
            "tests/operator_registry.rs".to_string(),
            "tests/adaptive_planning.rs".to_string(),
        ],
    }
}

fn gpu_tests_for(rule: &LoweringRule) -> Vec<String> {
    let mut tests = vec![
        "tests/gpu_scaffold.rs".to_string(),
        "tests/cross_backend_conformance.rs".to_string(),
    ];
    if is_padic_domain_scope(&domain_scope(rule)) || is_sheaf_domain_scope(&domain_scope(rule)) {
        tests.push("tests/facade.rs".to_string());
    }
    tests.sort();
    tests.dedup();
    tests
}

fn non_claims_for(rule: &LoweringRule) -> Vec<String> {
    let domain = domain_scope(rule);
    let mut claims = if is_padic_domain_scope(&domain) {
        vec![
            "not full p-adic algebra".to_string(),
            "not arbitrary precision p-adic fields".to_string(),
        ]
    } else if is_sheaf_domain_scope(&domain) {
        vec![
            "not general sheaf theory".to_string(),
            "not sheaf cohomology".to_string(),
        ]
    } else if rule
        .theory_requirements
        .iter()
        .any(|requirement| requirement.theory == TheoryId::CategoricalLaw)
    {
        vec!["not a full category-theory framework".to_string()]
    } else {
        vec!["not a production tensor compiler claim".to_string()]
    };
    if rule.theory_requirements.iter().any(|requirement| {
        requirement
            .theorem_id
            .as_deref()
            .is_some_and(|theorem| theorem.starts_with("tokitai_"))
    }) {
        claims.push("theorem binding does not prove the Rust runtime".to_string());
    }
    claims.sort();
    claims.dedup();
    claims
}

fn is_padic_domain_scope(domain: &str) -> bool {
    domain.contains("Q_") || domain.contains("padic")
}

fn is_sheaf_domain_scope(domain: &str) -> bool {
    domain.contains("cover:") || domain.contains("sheaf")
}

fn md(value: &str) -> String {
    value.replace('|', "\\|")
}

fn json_array(values: &[String]) -> String {
    format!(
        "[{}]",
        values
            .iter()
            .map(|value| json_string(value))
            .collect::<Vec<_>>()
            .join(",")
    )
}

fn json_option_string(value: &Option<String>) -> String {
    value
        .as_ref()
        .map_or_else(|| "null".to_string(), |value| json_string(value))
}

fn json_string(value: &str) -> String {
    let mut escaped = String::from("\"");
    for ch in value.chars() {
        match ch {
            '"' => escaped.push_str("\\\""),
            '\\' => escaped.push_str("\\\\"),
            '\n' => escaped.push_str("\\n"),
            '\r' => escaped.push_str("\\r"),
            '\t' => escaped.push_str("\\t"),
            ch if ch.is_control() => escaped.push_str(&format!("\\u{:04x}", ch as u32)),
            ch => escaped.push(ch),
        }
    }
    escaped.push('"');
    escaped
}