tokitai-operator 0.1.0

//! The `ExecutionPlan` data structure.
//!
//! `ExecutionPlan` is the planner's output: a sequence of
//! `PlanStep`s plus the plan-level cost, resource profile, and
//! the obligations list. The `PlanStepKind` enum distinguishes
//! `Single`, `Fused`, `PadicValuationSkip`, etc.
//!
//! The plan is the input to `CpuScalarBackend::execute_i64_plan`
//! and the source of the `audit_report`.
//!
use super::{Obligation, PlanCacheKey};
use crate::ir::RewriteJustification;

#[derive(Debug, Clone, PartialEq)]
pub struct ExecutionPlan {
    pub cache_key: Option<PlanCacheKey>,
    pub backend: String,
    pub steps: Vec<PlanStep>,
    pub cost: PlanCost,
    pub resources: PlanResourceProfile,
    pub fallback: Option<Fallback>,
    pub precision_schedule: PrecisionSchedule,
    pub obligations: Vec<Obligation>,
    pub rewrites: Vec<RewriteJustification>,
    pub proof_objects: Vec<ProofObject>,
    pub evidence_log: EvidenceLog,
}

impl ExecutionPlan {
    pub fn new(backend: String) -> Self {
        Self {
            cache_key: None,
            backend,
            steps: Vec::new(),
            cost: PlanCost::default(),
            resources: PlanResourceProfile::default(),
            fallback: None,
            precision_schedule: PrecisionSchedule::default(),
            obligations: Vec::new(),
            rewrites: Vec::new(),
            proof_objects: Vec::new(),
            evidence_log: EvidenceLog::default(),
        }
    }

    pub fn has_blocking_obligations(&self) -> bool {
        self.obligations.iter().any(Obligation::is_blocking)
    }
}

#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct PlanResourceProfile {
    pub padic: Option<PadicPlanningResource>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PadicPlanningResource {
    pub prime: u64,
    pub precision: u32,
    pub valuation_cutoff: u32,
    pub equality_digits: u32,
    pub backend_capability: String,
    pub fallback_reason: Option<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PlanStep {
    pub node_id: usize,
    pub op_name: String,
    pub backend: String,
    pub domain: String,
    pub representation: String,
    pub lowering_rule_id: Option<String>,
    pub kind: PlanStepKind,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum PlanStepKind {
    Single,
    Fused {
        node_ids: Vec<usize>,
        rule: String,
    },
    PadicValuationSkip {
        lhs_id: usize,
        rhs_id: usize,
        output_id: usize,
        prime: u64,
        precision: u32,
    },
    PadicMatmulValuationSkip {
        lhs_id: usize,
        rhs_id: usize,
        output_id: usize,
        prime: u64,
        precision: u32,
        certificate_policy: String,
        valuation_bucket_fingerprint: String,
    },
    CoverGlueCheck {
        target: String,
        opens: Vec<String>,
    },
}

#[derive(Debug, Clone, Default, PartialEq)]
pub struct PlanCost {
    pub estimated_runtime_ns: Option<u64>,
    pub estimated_memory_bytes: Option<u64>,
    pub precision_loss: Option<u32>,
    pub unresolved_obligations: usize,
    pub semantic: SemanticCost,
}

#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct SemanticCost {
    pub precision: Option<PrecisionCost>,
    pub valuation: Option<ValuationCost>,
    pub verification: Option<VerificationCost>,
    pub fallback: Option<FallbackCost>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PrecisionCost {
    pub input_digits: u32,
    pub output_digits: u32,
    pub precision_loss: u32,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ValuationCost {
    pub cutoff: u32,
    pub estimated_terms: usize,
    pub estimated_skipped_terms: usize,
    pub estimated_evaluated_terms: usize,
    pub certificate_policy: Option<String>,
    pub valuation_bucket_fingerprint_policy: Option<String>,
    pub precision_margin_floor: Option<u32>,
    pub rationale: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct VerificationCost {
    pub required_checks: usize,
    pub estimated_overhead_ns: Option<u64>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct FallbackCost {
    pub penalty_ns: Option<u64>,
    pub reason: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Fallback {
    pub backend: String,
    pub reason: String,
}

#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct PrecisionSchedule {
    pub steps: Vec<String>,
}

#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct EvidenceLog {
    pub entries: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ProofKind {
    ShapeEquality,
    ValuationCutoff,
    LoweringSemanticPreservation,
    RewriteSoundness,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ProofStatus {
    Proven,
    RuntimeChecked,
    Assumed,
    Pending,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofObject {
    pub id: String,
    pub kind: ProofKind,
    pub claim: String,
    pub status: ProofStatus,
    pub obligations: Vec<String>,
    pub evidence: Vec<String>,
}

impl ProofObject {
    pub fn new(
        id: impl Into<String>,
        kind: ProofKind,
        claim: impl Into<String>,
        status: ProofStatus,
    ) -> Self {
        Self {
            id: id.into(),
            kind,
            claim: claim.into(),
            status,
            obligations: Vec::new(),
            evidence: Vec::new(),
        }
    }

    pub fn with_obligation(mut self, obligation: impl Into<String>) -> Self {
        self.obligations.push(obligation.into());
        self
    }

    pub fn with_evidence(mut self, evidence: impl Into<String>) -> Self {
        self.evidence.push(evidence.into());
        self
    }
}