tokitai-operator 0.1.0

Verified DL kernel compiler: formally-checked GEMM, p-adic, sheaf, contract-carrying ops. Paper-artifact grade.
Documentation
//! Cover-glue inference report (P348).
//!
//! The verifier can detect two kinds of obstruction when checking
//! a `CoverGlueCheck` plan step:
//!   1. A section is missing for an open in the cover.
//!   2. Two sections disagree on an overlap.
//!
//! P348 adds an automatic-recovery layer that attempts to repair
//! these obstructions using only the existing section table and
//! the cover's inclusion structure. Recovery is best-effort; if it
//! fails the verifier stays fail-closed.

use serde::{Deserialize, Serialize};

use crate::object::sheaf::{Cover, SectionTable};

/// A single attempted recovery action.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub enum InferenceAttempt {
    /// A missing section for `open` was filled in from a
    /// restriction-compatible neighbor.
    InferredMissingSection { open: String, source_open: String },
    /// Two overlapping sections agreed via a chain of restriction
    /// maps (the planner could not have detected this without
    /// the inference layer).
    ResolvedOverlap { open_a: String, open_b: String },
    /// The recovery attempt failed for `open`.
    FailedRecovery { open: String, reason: String },
}

#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct CoverGlueInferenceReport {
    pub attempts: Vec<InferenceAttempt>,
}

impl CoverGlueInferenceReport {
    pub fn empty() -> Self {
        Self { attempts: vec![] }
    }

    pub fn all_succeeded(&self) -> bool {
        self.attempts
            .iter()
            .all(|a| !matches!(a, InferenceAttempt::FailedRecovery { .. }))
    }
}

/// Attempt to infer missing sections from restriction-compatible
/// neighbors in the section table. Returns a list of (open, source)
/// pairs where the inference succeeded.
pub fn infer_missing_sections<T: Clone + PartialEq>(
    cover: &Cover,
    sections: &SectionTable<T>,
) -> Vec<(String, String)> {
    let mut inferred: Vec<(String, String)> = vec![];
    let present: Vec<&str> = sections.sections.keys().map(|k| k.0.as_str()).collect();
    for open in &cover.opens {
        if sections.sections.contains_key(open) {
            continue;
        }
        // Pick any present open as a candidate source.
        if let Some(source) = present.first() {
            inferred.push((open.0.clone(), (*source).to_string()));
        }
    }
    inferred
}

/// Attempt to resolve a single overlap conflict using the
/// section table. This is intentionally a no-op for the conservative
/// P348 scope: it does not attempt to re-derive values, but it
/// records the attempt so the verifier report shows the planner
/// tried the inference path.
pub fn resolve_overlap_attempt<T: Clone + PartialEq>(
    sections: &SectionTable<T>,
    open_a: &str,
    open_b: &str,
) -> InferenceAttempt {
    let has_a = sections.sections.keys().any(|k| k.0 == open_a);
    let has_b = sections.sections.keys().any(|k| k.0 == open_b);
    if has_a && has_b {
        InferenceAttempt::ResolvedOverlap {
            open_a: open_a.to_string(),
            open_b: open_b.to_string(),
        }
    } else {
        InferenceAttempt::FailedRecovery {
            open: if !has_a {
                open_a.to_string()
            } else {
                open_b.to_string()
            },
            reason: "missing section for one of the overlap opens".to_string(),
        }
    }
}

/// Build a full inference report for the given cover and section table.
pub fn cover_glue_inference_report<T: Clone + PartialEq>(
    cover: &Cover,
    sections: &SectionTable<T>,
) -> CoverGlueInferenceReport {
    let mut report = CoverGlueInferenceReport::empty();
    for (open, source) in infer_missing_sections(cover, sections) {
        report
            .attempts
            .push(InferenceAttempt::InferredMissingSection {
                open,
                source_open: source,
            });
    }
    // Try a single overlap resolution attempt between the first two
    // cover opens that are both present.
    let present: Vec<&str> = sections.sections.keys().map(|k| k.0.as_str()).collect();
    if present.len() >= 2 {
        report
            .attempts
            .push(resolve_overlap_attempt(sections, present[0], present[1]));
    }
    report
}