tokitai-operator 0.1.0

//! Semantic conformance report.
//!
//! `semantic_conformance_report` joins the previously separate CPU
//! oracle, property-check, theorem-binding, fallback, and
//! math-bound audit-trace evidence into a single deterministic
//! report. Per-theory rows (p-adic valuation, finite-site sheaf,
//! category law-witness) separate theorem-checked, runtime-tested,
//! and fallback evidence.
//!
//! The report is the public artifact that the
//! `examples/audit_traces.rs` example prints as the
//! "== math-bound audit ==" block. It is *not* a proof of the Rust
//! runtime, a full formal verification result, or a general p-adic
//! or sheaf theorem; it is an engineering harness.
//!
use crate::backend::conformance::{
    BackendComparisonStatus, BackendConformanceRunReport, CpuOracleConformanceReport,
    CpuOracleConformanceSuite, CpuOracleFixtureKind,
};
use crate::planner::ExecutionPlan;
use crate::theory::{LawWitnessStatus, TheoryEvidence, TheoryId};
use crate::verify::{
    AuditDocument, MathBoundAuditTrace, PropertyCheckReport, TheoremBindingRegistry,
};
use crate::{Error, Result};

pub const SEMANTIC_CONFORMANCE_REPORT_ARTIFACT: &str = "tokitai-semantic-conformance-report";
pub const SEMANTIC_CONFORMANCE_REPORT_VERSION: u32 = 1;

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum SemanticConformanceStatus {
    Passed,
    FallbackCaptured,
    MissingTheoryEvidence,
    Failed,
}

impl SemanticConformanceStatus {
    pub fn as_str(&self) -> &'static str {
        match self {
            Self::Passed => "passed",
            Self::FallbackCaptured => "fallback_captured",
            Self::MissingTheoryEvidence => "missing_theory_evidence",
            Self::Failed => "failed",
        }
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheoryConformanceStatus {
    pub theory: TheoryId,
    pub status: SemanticConformanceStatus,
    pub constraints: Vec<String>,
    pub cpu_oracle_fixtures: Vec<String>,
    pub property_checks: Vec<String>,
    pub theorem_checked_evidence: Vec<String>,
    pub runtime_tested_evidence: Vec<String>,
    pub fallback_evidence: Vec<String>,
    pub missing_evidence: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct SemanticConformanceReport {
    pub artifact: String,
    pub version: u32,
    pub cpu_oracle: CpuOracleConformanceReport,
    pub backend_conformance: Option<BackendConformanceRunReport>,
    pub theory_statuses: Vec<TheoryConformanceStatus>,
    pub audit_traces: Vec<MathBoundAuditTrace>,
}

impl SemanticConformanceReport {
    pub fn passed(&self) -> bool {
        self.cpu_oracle.passed()
            && self.theory_statuses.iter().all(|status| {
                matches!(
                    status.status,
                    SemanticConformanceStatus::Passed | SemanticConformanceStatus::FallbackCaptured
                )
            })
            && self
                .backend_conformance
                .as_ref()
                .is_none_or(BackendConformanceRunReport::passed)
    }

    pub fn to_text(&self) -> String {
        let mut lines = vec![
            format!("artifact: {}", self.artifact),
            format!("version: {}", self.version),
            format!("passed: {}", self.passed()),
            format!("cpu_oracle_backend: {}", self.cpu_oracle.backend),
            format!(
                "cpu_oracle_capability_fingerprint: {}",
                self.cpu_oracle.capability_fingerprint
            ),
            format!("cpu_oracle_fixtures: {}", self.cpu_oracle.fixtures.len()),
        ];
        if let Some(conformance) = &self.backend_conformance {
            lines.push(format!(
                "backend_conformance: oracle={}, candidate={}, passed={}, cases={}, fallback_cases={}",
                conformance.oracle_backend,
                conformance.candidate_backend,
                conformance.passed(),
                conformance.cases.len(),
                conformance.fallback_cases().len()
            ));
        } else {
            lines.push("backend_conformance: none".to_string());
        }
        lines.push(format!("audit_traces: {}", self.audit_traces.len()));
        for trace in &self.audit_traces {
            lines.push(format!(
                "audit_trace: backend={}, plan_fingerprint={}, p_adic={}, sheaf={}, fallback={}",
                trace.backend_id,
                trace.plan_fingerprint,
                trace.p_adic_constraint_fingerprint,
                trace.sheaf_constraint_fingerprint,
                trace.fallback_reason.as_deref().unwrap_or("none")
            ));
        }
        for theory in &self.theory_statuses {
            lines.push(format!(
                "theory: id={}, status={}, constraints={}, cpu_fixtures={}, properties={}, theorem_checked={}, runtime_tested={}, fallback={}, missing={}",
                theory.theory.as_str(),
                theory.status.as_str(),
                theory.constraints.join("|"),
                theory.cpu_oracle_fixtures.join("|"),
                theory.property_checks.join("|"),
                theory.theorem_checked_evidence.join("|"),
                theory.runtime_tested_evidence.join("|"),
                theory.fallback_evidence.join("|"),
                theory.missing_evidence.join("|")
            ));
        }
        lines.join("\n")
    }

    pub fn to_json(&self) -> String {
        let traces = self
            .audit_traces
            .iter()
            .map(math_trace_json)
            .collect::<Vec<_>>()
            .join(",");
        let theory_statuses = self
            .theory_statuses
            .iter()
            .map(TheoryConformanceStatus::to_json)
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"artifact\":{},\"version\":{},\"passed\":{},\"cpu_oracle\":{},\"backend_conformance\":{},\"audit_traces\":[{}],\"theory_statuses\":[{}]}}",
            json_string(&self.artifact),
            self.version,
            self.passed(),
            cpu_oracle_json(&self.cpu_oracle),
            self.backend_conformance
                .as_ref()
                .map_or_else(|| "null".to_string(), backend_conformance_json),
            traces,
            theory_statuses
        )
    }
}

impl TheoryConformanceStatus {
    fn to_json(&self) -> String {
        format!(
            "{{\"theory\":{},\"status\":{},\"constraints\":{},\"cpu_oracle_fixtures\":{},\"property_checks\":{},\"theorem_checked_evidence\":{},\"runtime_tested_evidence\":{},\"fallback_evidence\":{},\"missing_evidence\":{}}}",
            json_string(self.theory.as_str()),
            json_string(self.status.as_str()),
            json_array(&self.constraints),
            json_array(&self.cpu_oracle_fixtures),
            json_array(&self.property_checks),
            json_array(&self.theorem_checked_evidence),
            json_array(&self.runtime_tested_evidence),
            json_array(&self.fallback_evidence),
            json_array(&self.missing_evidence)
        )
    }
}

pub fn semantic_conformance_report(
    plans: &[&ExecutionPlan],
    theory_evidence: &[TheoryEvidence],
    property_reports: &[PropertyCheckReport],
    backend_conformance: Option<&BackendConformanceRunReport>,
) -> Result<SemanticConformanceReport> {
    let cpu_oracle = CpuOracleConformanceSuite::new().run_all()?;
    let theorem_registry = TheoremBindingRegistry::tokitai_default()?;
    semantic_conformance_report_from_parts(
        plans,
        theory_evidence,
        property_reports,
        &cpu_oracle,
        &theorem_registry,
        backend_conformance,
    )
}

pub fn semantic_conformance_report_from_parts(
    plans: &[&ExecutionPlan],
    theory_evidence: &[TheoryEvidence],
    property_reports: &[PropertyCheckReport],
    cpu_oracle: &CpuOracleConformanceReport,
    theorem_registry: &TheoremBindingRegistry,
    backend_conformance: Option<&BackendConformanceRunReport>,
) -> Result<SemanticConformanceReport> {
    if !cpu_oracle.passed() {
        return Err(Error::verification(
            "semantic conformance report requires a passing CPU oracle baseline",
        ));
    }
    theorem_registry.validate()?;
    let audit_traces = plans
        .iter()
        .map(|plan| AuditDocument::from_plan(plan).math_bound)
        .collect::<Vec<_>>();
    let theory_statuses = [
        TheoryId::PadicValuation,
        TheoryId::FiniteSheaf,
        TheoryId::CategoricalLaw,
    ]
    .into_iter()
    .map(|theory| {
        theory_status(
            theory,
            theory_evidence,
            property_reports,
            cpu_oracle,
            theorem_registry,
            backend_conformance,
        )
    })
    .collect::<Result<Vec<_>>>()?;
    Ok(SemanticConformanceReport {
        artifact: SEMANTIC_CONFORMANCE_REPORT_ARTIFACT.to_string(),
        version: SEMANTIC_CONFORMANCE_REPORT_VERSION,
        cpu_oracle: cpu_oracle.clone(),
        backend_conformance: backend_conformance.cloned(),
        theory_statuses,
        audit_traces,
    })
}

fn theory_status(
    theory: TheoryId,
    theory_evidence: &[TheoryEvidence],
    property_reports: &[PropertyCheckReport],
    cpu_oracle: &CpuOracleConformanceReport,
    theorem_registry: &TheoremBindingRegistry,
    backend_conformance: Option<&BackendConformanceRunReport>,
) -> Result<TheoryConformanceStatus> {
    let evidences = theory_evidence
        .iter()
        .filter(|evidence| evidence.theory == theory)
        .collect::<Vec<_>>();
    let mut missing_evidence = Vec::new();
    let required_laws = required_laws(&theory);
    if evidences.is_empty() {
        missing_evidence.push(format!("missing {} TheoryEvidence", theory.as_str()));
    }
    for law in &required_laws {
        if !evidences
            .iter()
            .any(|evidence| evidence.has_law(law) && law_passed(evidence, law))
        {
            missing_evidence.push(format!("missing law {}:{}", theory.as_str(), law));
        }
    }

    let mut theorem_checked_evidence = Vec::new();
    let mut runtime_tested_evidence = Vec::new();
    let mut constraints = Vec::new();
    for evidence in &evidences {
        constraints.extend(
            evidence
                .constraints
                .iter()
                .map(|constraint| constraint.id.clone()),
        );
        for law in &evidence.law_witnesses {
            let item = format!("{}:{}", evidence.theory.as_str(), law.law_id);
            match law.status {
                LawWitnessStatus::TheoremBound => theorem_checked_evidence.push(item),
                LawWitnessStatus::RuntimeChecked => runtime_tested_evidence.push(item),
                LawWitnessStatus::AssumedForScope => {
                    runtime_tested_evidence.push(format!("{item}:assumed_for_scope"))
                }
                LawWitnessStatus::Failed => {
                    missing_evidence.push(format!("failed law witness {item}"));
                }
            }
        }
        for binding in &evidence.assumption_bindings {
            if theorem_registry.lookup(&binding.theorem_id).is_ok() {
                theorem_checked_evidence.push(format!(
                    "theorem={} assumption={} runtime_source={}",
                    binding.theorem_id, binding.assumption, binding.runtime_source
                ));
            } else {
                missing_evidence.push(format!("missing theorem binding {}", binding.theorem_id));
            }
        }
        runtime_tested_evidence.extend(evidence.audit_lines());
    }
    constraints.sort();
    constraints.dedup();
    theorem_checked_evidence.sort();
    theorem_checked_evidence.dedup();
    runtime_tested_evidence.sort();
    runtime_tested_evidence.dedup();

    let cpu_oracle_fixtures = cpu_oracle
        .fixtures
        .iter()
        .filter(|fixture| fixture_theory(&fixture.kind).as_ref() == Some(&theory))
        .map(|fixture| fixture.name.clone())
        .collect::<Vec<_>>();
    if cpu_oracle_fixtures.is_empty() {
        missing_evidence.push(format!(
            "missing CPU oracle fixture for {}",
            theory.as_str()
        ));
    }
    runtime_tested_evidence.extend(
        cpu_oracle
            .fixtures
            .iter()
            .filter(|fixture| fixture_theory(&fixture.kind).as_ref() == Some(&theory))
            .flat_map(|fixture| fixture.evidence.iter().cloned()),
    );

    let property_checks = property_reports_for_theory(&theory, property_reports);
    if property_checks
        .iter()
        .any(|property| property.contains("failed"))
    {
        missing_evidence.push(format!("failed property check for {}", theory.as_str()));
    }
    runtime_tested_evidence.extend(property_checks.iter().cloned());

    let fallback_evidence = backend_conformance
        .map(|conformance| {
            conformance
                .cases
                .iter()
                .filter(|case| {
                    fixture_theory(&case.family).as_ref() == Some(&theory)
                        && case.status == BackendComparisonStatus::FallbackCaptured
                })
                .map(|case| {
                    format!(
                        "{} fallback: {}",
                        case.fixture_name,
                        case.fallback_reason.as_deref().unwrap_or("captured")
                    )
                })
                .collect::<Vec<_>>()
        })
        .unwrap_or_default();

    let has_failed_cpu = cpu_oracle
        .fixtures
        .iter()
        .any(|fixture| fixture_theory(&fixture.kind).as_ref() == Some(&theory) && !fixture.passed);
    let status = if !missing_evidence.is_empty() {
        SemanticConformanceStatus::MissingTheoryEvidence
    } else if has_failed_cpu
        || property_checks
            .iter()
            .any(|property| property.contains("failed"))
    {
        SemanticConformanceStatus::Failed
    } else if !fallback_evidence.is_empty() {
        SemanticConformanceStatus::FallbackCaptured
    } else {
        SemanticConformanceStatus::Passed
    };

    Ok(TheoryConformanceStatus {
        theory,
        status,
        constraints,
        cpu_oracle_fixtures,
        property_checks,
        theorem_checked_evidence,
        runtime_tested_evidence,
        fallback_evidence,
        missing_evidence,
    })
}

fn required_laws(theory: &TheoryId) -> Vec<&'static str> {
    match theory {
        TheoryId::PadicValuation => vec!["valuation_skip_sound_mod_pk"],
        TheoryId::FiniteSheaf => vec!["finite_sheaf_gluing_sound"],
        TheoryId::CategoricalLaw => vec!["identity", "associativity"],
    }
}

fn law_passed(evidence: &TheoryEvidence, law_id: &str) -> bool {
    evidence.law_witnesses.iter().any(|law| {
        law.law_id == law_id
            && matches!(
                law.status,
                LawWitnessStatus::TheoremBound
                    | LawWitnessStatus::RuntimeChecked
                    | LawWitnessStatus::AssumedForScope
            )
    })
}

fn fixture_theory(kind: &CpuOracleFixtureKind) -> Option<TheoryId> {
    match kind {
        CpuOracleFixtureKind::PadicPointwise
        | CpuOracleFixtureKind::PadicMatmul
        | CpuOracleFixtureKind::PadicValuationSkip => Some(TheoryId::PadicValuation),
        CpuOracleFixtureKind::SheafGlue => Some(TheoryId::FiniteSheaf),
        CpuOracleFixtureKind::CategoricalLaw => Some(TheoryId::CategoricalLaw),
        CpuOracleFixtureKind::DenseI64 => None,
    }
}

fn property_reports_for_theory(
    theory: &TheoryId,
    property_reports: &[PropertyCheckReport],
) -> Vec<String> {
    let needle = match theory {
        TheoryId::PadicValuation => "p-adic",
        TheoryId::FiniteSheaf => "sheaf",
        TheoryId::CategoricalLaw => "categorical",
    };
    property_reports
        .iter()
        .filter(|report| report.property.contains(needle))
        .map(|report| {
            format!(
                "{}:{}:samples={}",
                report.property,
                if report.passed { "passed" } else { "failed" },
                report.samples_checked
            )
        })
        .collect()
}

fn cpu_oracle_json(report: &CpuOracleConformanceReport) -> String {
    let fixtures = report
        .fixtures
        .iter()
        .map(|fixture| {
            format!(
                "{{\"name\":{},\"kind\":{},\"backend\":{},\"capability_gate\":{},\"passed\":{},\"checked_outputs\":{},\"evidence\":{}}}",
                json_string(&fixture.name),
                json_string(&format!("{:?}", fixture.kind)),
                json_string(&fixture.backend),
                json_string(&fixture.capability_gate),
                fixture.passed,
                json_usize_array(&fixture.checked_outputs),
                json_array(&fixture.evidence)
            )
        })
        .collect::<Vec<_>>()
        .join(",");
    format!(
        "{{\"backend\":{},\"capability_fingerprint\":{},\"fixtures\":[{}]}}",
        json_string(&report.backend),
        json_string(&report.capability_fingerprint),
        fixtures
    )
}

fn backend_conformance_json(report: &BackendConformanceRunReport) -> String {
    let cases = report
        .cases
        .iter()
        .map(|case| {
            format!(
                "{{\"fixture_name\":{},\"family\":{},\"oracle_backend\":{},\"candidate_backend\":{},\"candidate_capability_fingerprint\":{},\"mathematical_constraints\":{},\"status\":{},\"checked_outputs\":{},\"fallback_reason\":{},\"evidence\":{}}}",
                json_string(&case.fixture_name),
                json_string(&format!("{:?}", case.family)),
                json_string(&case.oracle_backend),
                json_string(&case.candidate_backend),
                json_string(&case.candidate_capability_fingerprint),
                json_array(&case.mathematical_constraints),
                json_string(&format!("{:?}", case.status)),
                json_usize_array(&case.checked_outputs),
                json_option_string(&case.fallback_reason),
                json_array(&case.evidence)
            )
        })
        .collect::<Vec<_>>()
        .join(",");
    format!(
        "{{\"oracle_backend\":{},\"oracle_capability_fingerprint\":{},\"candidate_backend\":{},\"candidate_capability_fingerprint\":{},\"passed\":{},\"cases\":[{}]}}",
        json_string(&report.oracle_backend),
        json_string(&report.oracle_capability_fingerprint),
        json_string(&report.candidate_backend),
        json_string(&report.candidate_capability_fingerprint),
        report.passed(),
        cases
    )
}

fn math_trace_json(trace: &MathBoundAuditTrace) -> String {
    format!(
        "{{\"plan_fingerprint\":{},\"backend_id\":{},\"device_kind\":{},\"capability_fingerprint\":{},\"p_adic_constraint_fingerprint\":{},\"sheaf_constraint_fingerprint\":{},\"lowering_rule_ids\":{},\"fallback_reason\":{},\"conformance_result\":{},\"benchmark_environment\":{}}}",
        json_string(&trace.plan_fingerprint),
        json_string(&trace.backend_id),
        json_string(&trace.device_kind),
        json_string(&trace.capability_fingerprint),
        json_string(&trace.p_adic_constraint_fingerprint),
        json_string(&trace.sheaf_constraint_fingerprint),
        json_array(&trace.lowering_rule_ids),
        json_option_string(&trace.fallback_reason),
        json_option_string(&trace.conformance_result),
        json_option_string(&trace.benchmark_environment)
    )
}

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

fn json_usize_array(values: &[usize]) -> String {
    format!(
        "[{}]",
        values
            .iter()
            .map(usize::to_string)
            .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
}