tokitai-operator 0.1.0

//! First-of-kind novelty dossier.
//!
//! `first_of_kind_evidence_dossier` returns the 4 FOK hypotheses
//! (FOK1-FOK4) and their evidence-backed status. The dossier is
//! consumed by `tests/novelty_dossier.rs` and by the
//! `examples/audit_traces.rs` example. The dossier is *not* a
//! claim that Tokitai is the first to do X; it is a record of
//! which first-of-kind hypotheses have evidence in the repo.
//!
//! Source-of-truth: `docs/first_of_kind_novelty_evidence.md`.
//!
use crate::{Error, Result};

pub const NOVELTY_DOSSIER_DOC: &str = "docs/first_of_kind_novelty_evidence.md";

#[derive(Clone, Debug, PartialEq, Eq)]
pub struct NoveltyEvidenceEntry {
    pub fok_id: &'static str,
    pub status: &'static str,
    pub scoped_hypothesis: &'static str,
    pub prior_art_family: &'static str,
    pub prior_art_boundary: &'static str,
    pub pain_points: &'static [&'static str],
    pub tokitai_response: &'static [&'static str],
    pub repository_artifacts: &'static [&'static str],
    pub tests: &'static [&'static str],
    pub theorem_packages: &'static [&'static str],
    pub patent_claim_candidates: &'static [&'static str],
    pub paper_claim: &'static str,
    pub must_not_claim: &'static [&'static str],
    pub residual_risks: &'static [&'static str],
}

pub fn first_of_kind_evidence_dossier() -> &'static [NoveltyEvidenceEntry] {
    &FIRST_OF_KIND_EVIDENCE_DOSSIER
}

pub fn validate_first_of_kind_evidence_dossier(entries: &[NoveltyEvidenceEntry]) -> Result<()> {
    if entries.len() != 4 {
        return Err(Error::verification(format!(
            "expected four FOK evidence entries, found {}",
            entries.len()
        )));
    }

    for entry in entries {
        if entry.status != "evidence-backed hypothesis" && entry.status != "downgraded" {
            return Err(Error::verification(format!(
                "{} status must stay hypothesis-scoped or downgraded, found {}",
                entry.fok_id, entry.status
            )));
        }
        if entry.prior_art_family.is_empty() || entry.prior_art_boundary.is_empty() {
            return Err(Error::verification(format!(
                "{} must name prior-art family and boundary",
                entry.fok_id
            )));
        }
        if entry.pain_points.is_empty()
            || entry.tokitai_response.is_empty()
            || entry.repository_artifacts.is_empty()
            || entry.tests.is_empty()
            || entry.must_not_claim.is_empty()
            || entry.residual_risks.is_empty()
        {
            return Err(Error::verification(format!(
                "{} lacks required pain-point, artifact, test, non-claim, or risk evidence",
                entry.fok_id
            )));
        }
        if entry.scoped_hypothesis.contains("first p-adic")
            || entry.scoped_hypothesis.contains("first sheaf neural")
            || entry.paper_claim.contains("first p-adic")
            || entry.paper_claim.contains("first sheaf neural")
        {
            return Err(Error::verification(format!(
                "{} contains an overbroad usable firstness claim",
                entry.fok_id
            )));
        }
    }

    Ok(())
}

const FIRST_OF_KIND_EVIDENCE_DOSSIER: [NoveltyEvidenceEntry; 4] = [
    NoveltyEvidenceEntry {
        fok_id: "FOK1",
        status: "evidence-backed hypothesis",
        scoped_hypothesis: "A Rust operator runtime contract where p-adic valuation and precision affect planning, lowering admission, backend fallback, conformance equality, and theorem-bound proof replay.",
        prior_art_family: "p-adic machine learning, p-adic cellular neural networks, p-adic PDE/image-processing, and exact p-adic computer algebra",
        prior_art_boundary: "Prior work covers p-adic mathematics and application models more deeply; Tokitai only claims the runtime-contract integration for selected fixed-precision operators.",
        pain_points: &[
            "p-adic valuation is often embedded in one model or algebra system rather than exposed as a reusable planner resource",
            "hardware fallback and proof/audit replay are usually outside the core p-adic interface",
        ],
        tokitai_response: &[
            "PadicPlanningResource carries prime, precision, valuation cutoff, estimated skip/evaluate counts, and backend support evidence",
            "lowering checks reject p-adic plans when fixed-precision capability or valuation obligations are missing",
            "CPU oracle conformance and Lean theorem binding cover the minimized valuation-skip boundary",
        ],
        repository_artifacts: &[
            "src/planner/plan.rs",
            "src/planner/mod.rs",
            "src/op/registry.rs",
            "src/verify/equality.rs",
            "src/verify/theorems.rs",
            "docs/padic_planner_resource.md",
            "docs/padic_valuation_skip_theorem.md",
        ],
        tests: &[
            "tests/padic.rs",
            "tests/lowering_capabilities.rs",
            "tests/cross_backend_conformance.rs",
            "tests/padic_valuation_skip_theorem.rs",
        ],
        theorem_packages: &[
            "docs/theorems/padic_valuation_skip.lean",
            "docs/theorems/padic_valuation_skip.transcript.txt",
        ],
        patent_claim_candidates: &["PC2", "PC3", "PC4"],
        paper_claim: "p-adic valuation and precision are executable runtime resources for selected fixed-precision operators, not just numeric metadata.",
        must_not_claim: &[
            "Tokitai is the first p-adic computation system",
            "Tokitai formalizes p-adic fields or all p-adic algebra",
            "Tokitai accelerates p-adic operators on GPU today",
        ],
        residual_risks: &[
            "scope is limited to fixed-precision p-adic sum-product/matmul-style planning",
            "Lean theorem covers a minimized modular lemma, not the whole Rust runtime",
        ],
    },
    NoveltyEvidenceEntry {
        fok_id: "FOK2",
        status: "evidence-backed hypothesis",
        scoped_hypothesis: "A finite-site sheaf operator family where restriction, compatibility, gluing, obstruction, backend capability checks, conformance, and theorem mapping are first-class runtime evidence.",
        prior_art_family: "sheaf neural networks, neural sheaf diffusion, cellular sheaf graph learning, and distributed consistency systems",
        prior_art_boundary: "Prior work covers sheaf-based models and graph learning; Tokitai only claims a general finite-site operator-runtime boundary with explicit obstruction evidence.",
        pain_points: &[
            "many sheaf systems are model architectures rather than reusable local-to-global operator runtimes",
            "obstruction reporting and backend lowering contracts are often secondary to predictive performance",
        ],
        tokitai_response: &[
            "SectionTable emits restriction witnesses, compatibility reports, glue reports, and structured obstructions",
            "lowering contracts can require finite-site sheaf locality before backend admission",
            "Lean theorem binding maps compatible and obstructed reports to minimized finite-site assumptions",
        ],
        repository_artifacts: &[
            "src/object/sheaf.rs",
            "src/planner/mod.rs",
            "src/op/registry.rs",
            "src/verify/theorems.rs",
            "docs/sheaf_operator_family.md",
            "docs/finite_sheaf_gluing_theorem.md",
        ],
        tests: &[
            "tests/sheaf.rs",
            "tests/lowering_capabilities.rs",
            "tests/cross_backend_conformance.rs",
            "tests/finite_sheaf_gluing_theorem.rs",
        ],
        theorem_packages: &[
            "docs/theorems/finite_sheaf_gluing.lean",
            "docs/theorems/finite_sheaf_gluing.transcript.txt",
        ],
        patent_claim_candidates: &["PC2", "PC5"],
        paper_claim: "finite-site sheaf local-to-global semantics are executable operator contracts with obstruction evidence.",
        must_not_claim: &[
            "Tokitai is the first sheaf computation framework",
            "Tokitai is a sheaf neural network architecture",
            "Tokitai formalizes general sheaf theory or cohomology",
        ],
        residual_risks: &[
            "current support is finite-site and SectionTable-oriented",
            "categorical scope remains contract-witness level",
        ],
    },
    NoveltyEvidenceEntry {
        fok_id: "FOK3",
        status: "evidence-backed hypothesis",
        scoped_hypothesis: "A heterogeneous backend boundary where nonstandard mathematical contracts can block lowering even when ordinary dtype, layout, or device metadata would otherwise fit.",
        prior_art_family: "MLIR, IREE, TVM, XLA, Triton, ONNX Runtime, oneDNN, and GPU kernel libraries",
        prior_art_boundary: "These systems are much broader heterogeneous compiler stacks; Tokitai only claims math-contract-gated admission above backend implementation.",
        pain_points: &[
            "ordinary backend selection usually centers dtype, shape, layout, memory, and kernel availability",
            "domain-specific equivalence such as p-adic precision or sheaf compatibility is not generally the lowering gate",
        ],
        tokitai_response: &[
            "ComputeHardware exposes capability fingerprints without owning mathematical semantics",
            "LoweringCapability carries p-adic and finite-site sheaf requirements",
            "GPU scaffold emits explicit fallback evidence for unsupported nonstandard domains",
            "math-bound audit traces record backend, device, capability, math constraint, lowering, fallback, and conformance fields",
        ],
        repository_artifacts: &[
            "src/backend/hardware.rs",
            "src/backend/gpu.rs",
            "src/op/registry.rs",
            "src/backend/conformance.rs",
            "src/verify/mod.rs",
            "docs/hardware_abstraction_boundary.md",
            "docs/gpu_scaffold.md",
            "docs/math_bound_audit_traces.md",
        ],
        tests: &[
            "tests/hardware_abstraction.rs",
            "tests/gpu_scaffold.rs",
            "tests/lowering_capabilities.rs",
            "tests/math_bound_audit_traces.rs",
        ],
        theorem_packages: &[],
        patent_claim_candidates: &["PC1", "PC2", "PC3"],
        paper_claim: "heterogeneous execution is subordinate to mathematical capability contracts and auditable fallback evidence.",
        must_not_claim: &[
            "Tokitai replaces MLIR, TVM, IREE, XLA, or Triton",
            "Tokitai has production GPU kernels for nonstandard domains",
            "Tokitai proves backend correctness from capability fingerprints alone",
        ],
        residual_risks: &[
            "GPU support is scaffold or narrow dense-i64 pilot only",
            "no device allocation, streams, or nonstandard GPU kernels exist yet",
        ],
    },
    NoveltyEvidenceEntry {
        fok_id: "FOK4",
        status: "evidence-backed hypothesis",
        scoped_hypothesis: "An integrated evidence chain from nonstandard-domain plan to proof object, replay/checker evidence, backend capability fingerprint, conformance status, and reproducible benchmark/evidence rows.",
        prior_art_family: "proof-carrying code, proof assistants, audit logs, reproducibility artifacts, and benchmark harnesses",
        prior_art_boundary: "Tokitai does not replace proof assistants or general audit systems; it binds selected nonstandard operator execution evidence into one reproducible trace.",
        pain_points: &[
            "proof artifacts, backend conformance, and benchmark rows are often separate evidence streams",
            "paper artifacts can hide fallback behavior or mix correctness evidence with speed claims",
        ],
        tokitai_response: &[
            "MathBoundAuditTrace binds plan fingerprints to backend/device/math/lowering/fallback/conformance evidence",
            "application-evidence-matrix rows separate correctness, speed proxy, fallback rate, precision/locality scope, and proof evidence",
            "theorem transcripts record native Lean checks when available while preserving offline structural validation",
        ],
        repository_artifacts: &[
            "src/verify/mod.rs",
            "examples/audit_traces.rs",
            "examples/paper_benchmarks.rs",
            "docs/math_bound_audit_traces.md",
            "docs/benchmark_application_evidence_matrix.md",
            "docs/theorems/padic_valuation_skip.transcript.txt",
            "docs/theorems/finite_sheaf_gluing.transcript.txt",
        ],
        tests: &[
            "tests/math_bound_audit_traces.rs",
            "tests/paper_benchmarks_example.rs",
            "tests/padic_valuation_skip_theorem.rs",
            "tests/finite_sheaf_gluing_theorem.rs",
        ],
        theorem_packages: &[
            "docs/theorems/padic_valuation_skip.lean",
            "docs/theorems/finite_sheaf_gluing.lean",
        ],
        patent_claim_candidates: &["PC1", "PC3", "PC4"],
        paper_claim: "Tokitai reports correctness, fallback, proof, and benchmark evidence as one scoped nonstandard-operator evidence chain.",
        must_not_claim: &[
            "Tokitai provides full formal verification of the runtime",
            "Tokitai's deterministic benchmark rows prove production speedup",
            "Tokitai's audit trace alone proves mathematical correctness",
        ],
        residual_risks: &[
            "benchmark evidence remains deterministic and CI-oriented rather than broad performance evaluation",
            "proof assistant coverage is limited to minimized theorem packages",
        ],
    },
];