tokitai-operator 0.1.0

//! Theory-aware p-adic and sheaf glue-check policies.
//!
//! The planner uses a `TheoryId` to decide which low-level rules
//! apply. `src/theory.rs` is the public entry point for the
//! user-supplied p-adic domain and sheaf-cover objects, and
//! exposes the property->theorem bindings that the verifier reads.
//!
//! Public types:
//! - `TheoryId` — the abstract identifier (e.g. `Q_5`, `Z_2`).
//! - `PadicDomain` — the p-adic precision-bounded domain used by
//!   the p-adic valuation-skip planner.
//! - `SheafCompatibilityReport` — the per-cover glue-check result.
//!
//! See `docs/theory_contract_core.md` and `docs/theorems/` for the
//! per-theory release-gate evidence.
//!
use crate::domain::{Padic, PadicDomain};
use crate::object::sheaf::{CechObstructionSummary, SheafCompatibilityReport};
use crate::planner::{
    DischargeStatus, ExecutionPlan, Obligation, ObligationSeverity, ObligationSource, PlanStepKind,
    ProofKind,
};
use crate::verify::{
    FINITE_SHEAF_GLUING_LEAN_FILE, FINITE_SHEAF_GLUING_THEOREM_ID,
    FINITE_SHEAF_OBSTRUCTION_THEOREM_ID, PADIC_VALUATION_SKIP_LEAN_FILE,
    PADIC_VALUATION_SKIP_THEOREM_ID, PropertyCheckReport, TheoremBindingRegistry,
};
use crate::{Error, Result};

#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum TheoryId {
    PadicValuation,
    FiniteSheaf,
    CategoricalLaw,
}

impl TheoryId {
    pub fn as_str(&self) -> &'static str {
        match self {
            TheoryId::PadicValuation => "padic:valuation",
            TheoryId::FiniteSheaf => "sheaf:finite_site",
            TheoryId::CategoricalLaw => "category:law_witness",
        }
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheoryConstraint {
    pub theory: TheoryId,
    pub id: String,
    pub description: String,
    pub parameters: Vec<(String, String)>,
    pub required_evidence: Vec<String>,
}

impl TheoryConstraint {
    pub fn new(theory: TheoryId, id: impl Into<String>, description: impl Into<String>) -> Self {
        Self {
            theory,
            id: id.into(),
            description: description.into(),
            parameters: Vec::new(),
            required_evidence: Vec::new(),
        }
    }

    pub fn with_parameter(mut self, key: impl Into<String>, value: impl ToString) -> Self {
        self.parameters.push((key.into(), value.to_string()));
        self
    }

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

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum LawWitnessStatus {
    RuntimeChecked,
    TheoremBound,
    AssumedForScope,
    Failed,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct LawWitness {
    pub theory: TheoryId,
    pub law_id: String,
    pub status: LawWitnessStatus,
    pub obligations: Vec<String>,
    pub evidence: Vec<String>,
}

impl LawWitness {
    pub fn new(theory: TheoryId, law_id: impl Into<String>, status: LawWitnessStatus) -> Self {
        Self {
            theory,
            law_id: law_id.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
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AssumptionBinding {
    pub theorem_id: String,
    pub theorem_file: String,
    pub runtime_source: String,
    pub assumption: String,
    pub evidence: String,
}

impl AssumptionBinding {
    pub fn new(
        theorem_id: impl Into<String>,
        theorem_file: impl Into<String>,
        runtime_source: impl Into<String>,
        assumption: impl Into<String>,
        evidence: impl Into<String>,
    ) -> Self {
        Self {
            theorem_id: theorem_id.into(),
            theorem_file: theorem_file.into(),
            runtime_source: runtime_source.into(),
            assumption: assumption.into(),
            evidence: evidence.into(),
        }
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheoryEvidence {
    pub theory: TheoryId,
    pub scope: String,
    pub constraints: Vec<TheoryConstraint>,
    pub law_witnesses: Vec<LawWitness>,
    pub assumption_bindings: Vec<AssumptionBinding>,
    pub audit_entries: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CertifiedTheoryRequirement {
    pub theory: TheoryId,
    pub law_id: String,
    pub theorem_id: Option<String>,
    pub required_evidence: Vec<String>,
    pub fallback_reason: String,
}

impl CertifiedTheoryRequirement {
    pub fn new(theory: TheoryId, law_id: impl Into<String>) -> Self {
        let law_id = law_id.into();
        Self {
            theory,
            fallback_reason: format!("missing theory law witness {law_id}"),
            law_id,
            theorem_id: None,
            required_evidence: Vec::new(),
        }
    }

    pub fn with_theorem(mut self, theorem_id: impl Into<String>) -> Self {
        self.theorem_id = Some(theorem_id.into());
        self
    }

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

    pub fn with_fallback_reason(mut self, reason: impl Into<String>) -> Self {
        self.fallback_reason = reason.into();
        self
    }

    pub fn padic_valuation_skip() -> Self {
        Self::new(TheoryId::PadicValuation, "valuation_skip_sound_mod_pk")
            .with_theorem(PADIC_VALUATION_SKIP_THEOREM_ID)
            .requiring("PadicPlanningResource")
            .requiring("valuation_cutoff proof object")
            .with_fallback_reason(
                "valuation-skip rewrite/lowering requires p-adic law and theorem evidence",
            )
    }

    pub fn finite_sheaf_gluing() -> Self {
        Self::new(TheoryId::FiniteSheaf, "finite_sheaf_gluing_sound")
            .with_theorem(FINITE_SHEAF_GLUING_THEOREM_ID)
            .requiring("SheafCompatibilityReport")
            .requiring("restriction witnesses")
            .with_fallback_reason(
                "cover-local glue rewrite/lowering requires finite-sheaf law and theorem evidence",
            )
    }

    pub fn categorical_identity() -> Self {
        Self::new(TheoryId::CategoricalLaw, "identity")
            .requiring("categorical identity witness")
            .with_fallback_reason("categorical lowering requires identity law evidence")
    }

    pub fn categorical_associativity() -> Self {
        Self::new(TheoryId::CategoricalLaw, "associativity")
            .requiring("categorical associative composition witness")
            .with_fallback_reason("categorical lowering requires associativity law evidence")
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CertifiedTheoryContractReport {
    pub satisfied: bool,
    pub missing_laws: Vec<String>,
    pub missing_theorems: Vec<String>,
    pub missing_evidence: Vec<String>,
    pub audit_entries: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PadicTheoryOperatorReport {
    pub result: Padic,
    pub lhs_valuation: Option<u32>,
    pub rhs_valuation: Option<u32>,
    pub result_valuation: Option<u32>,
    pub evidence: TheoryEvidence,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct SheafObstructionLocalization {
    pub compatible: bool,
    pub obstruction_count: usize,
    pub localized_opens: Vec<String>,
    pub suggested_repairs: Vec<String>,
    pub evidence: TheoryEvidence,
}

impl CertifiedTheoryContractReport {
    pub fn passed(audit_entries: Vec<String>) -> Self {
        Self {
            satisfied: true,
            missing_laws: Vec::new(),
            missing_theorems: Vec::new(),
            missing_evidence: Vec::new(),
            audit_entries,
        }
    }

    pub fn failed(
        missing_laws: Vec<String>,
        missing_theorems: Vec<String>,
        missing_evidence: Vec<String>,
        audit_entries: Vec<String>,
    ) -> Self {
        Self {
            satisfied: false,
            missing_laws,
            missing_theorems,
            missing_evidence,
            audit_entries,
        }
    }
}

impl TheoryEvidence {
    pub fn new(theory: TheoryId, scope: impl Into<String>) -> Self {
        Self {
            theory,
            scope: scope.into(),
            constraints: Vec::new(),
            law_witnesses: Vec::new(),
            assumption_bindings: Vec::new(),
            audit_entries: Vec::new(),
        }
    }

    pub fn has_law(&self, law_id: &str) -> bool {
        self.law_witnesses.iter().any(|law| law.law_id == law_id)
    }

    pub fn has_required_evidence(&self, evidence: &str) -> bool {
        self.constraints
            .iter()
            .flat_map(|constraint| constraint.required_evidence.iter())
            .chain(
                self.law_witnesses
                    .iter()
                    .flat_map(|law| law.evidence.iter()),
            )
            .chain(
                self.assumption_bindings
                    .iter()
                    .map(|binding| &binding.evidence),
            )
            .any(|candidate| candidate == evidence || candidate.contains(evidence))
    }

    pub fn audit_lines(&self) -> Vec<String> {
        let mut lines = vec![format!(
            "theory={} scope={} constraints={} laws={} assumptions={}",
            self.theory.as_str(),
            self.scope,
            self.constraints.len(),
            self.law_witnesses.len(),
            self.assumption_bindings.len()
        )];
        lines.extend(self.audit_entries.iter().cloned());
        lines
    }
}

pub fn padic_valuation_cutoff_theory_evidence(plan: &ExecutionPlan) -> Result<TheoryEvidence> {
    let resource = plan.resources.padic.as_ref().ok_or_else(|| {
        Error::verification("p-adic theory evidence requires PadicPlanningResource")
    })?;
    if !plan.steps.iter().any(|step| {
        matches!(
            step.kind,
            PlanStepKind::PadicValuationSkip { .. } | PlanStepKind::PadicMatmulValuationSkip { .. }
        )
    }) {
        return Err(Error::verification(
            "p-adic theory evidence requires a valuation-skip plan step",
        ));
    }
    let proof = plan
        .proof_objects
        .iter()
        .find(|proof| proof.kind == ProofKind::ValuationCutoff)
        .ok_or_else(|| {
            Error::verification("p-adic theory evidence requires valuation_cutoff proof object")
        })?;

    let mut evidence = TheoryEvidence::new(
        TheoryId::PadicValuation,
        "fixed-precision valuation-skip modulo p^k",
    );
    evidence.constraints.push(
        TheoryConstraint::new(
            TheoryId::PadicValuation,
            "padic.valuation_cutoff",
            "terms with valuation at least the active precision vanish modulo p^k",
        )
        .with_parameter("prime", resource.prime)
        .with_parameter("precision", resource.precision)
        .with_parameter("valuation_cutoff", resource.valuation_cutoff)
        .with_parameter("equality_digits", resource.equality_digits)
        .requiring("PadicPlanningResource")
        .requiring("valuation_cutoff proof object"),
    );
    evidence.law_witnesses.push(
        LawWitness::new(
            TheoryId::PadicValuation,
            "valuation_skip_sound_mod_pk",
            LawWitnessStatus::TheoremBound,
        )
        .with_obligation("all inputs share the same fixed-precision p-adic domain")
        .with_obligation("runtime valuation checks use the active precision cutoff")
        .with_evidence(proof.id.clone())
        .with_evidence(format!(
            "prime={}, precision={}, cutoff={}",
            resource.prime, resource.precision, resource.valuation_cutoff
        )),
    );
    evidence.assumption_bindings.push(AssumptionBinding::new(
        PADIC_VALUATION_SKIP_THEOREM_ID,
        PADIC_VALUATION_SKIP_LEAN_FILE,
        proof.id.clone(),
        "skippedTermVanishesModulo",
        "PadicPlanningResource(prime, precision, valuation_cutoff)",
    ));
    evidence.audit_entries.push(format!(
        "padic theory evidence: backend_capability={}, fallback={}",
        resource.backend_capability,
        resource.fallback_reason.as_deref().unwrap_or("none")
    ));
    Ok(evidence)
}

pub fn finite_sheaf_compatibility_theory_evidence<T>(
    plan: &ExecutionPlan,
    compatibility: &SheafCompatibilityReport<T>,
) -> Result<TheoryEvidence> {
    let (target, opens) = plan
        .steps
        .iter()
        .find_map(|step| {
            if let PlanStepKind::CoverGlueCheck { target, opens } = &step.kind {
                Some((target.clone(), opens.clone()))
            } else {
                None
            }
        })
        .ok_or_else(|| Error::verification("sheaf theory evidence requires cover_glue_check"))?;
    let proof = plan
        .proof_objects
        .iter()
        .find(|proof| proof.kind == ProofKind::RewriteSoundness)
        .ok_or_else(|| {
            Error::verification("sheaf theory evidence requires rewrite soundness proof")
        })?;

    let mut evidence = TheoryEvidence::new(
        TheoryId::FiniteSheaf,
        "finite-site cover compatibility and gluing",
    );
    evidence.constraints.push(
        TheoryConstraint::new(
            TheoryId::FiniteSheaf,
            "sheaf.compatible_overlaps",
            "local sections agree on checked overlaps before gluing",
        )
        .with_parameter("target", target)
        .with_parameter("cover_opens", opens.join("|"))
        .with_parameter("checked_overlaps", compatibility.checked_overlaps)
        .requiring("SheafCompatibilityReport")
        .requiring("restriction witnesses"),
    );
    evidence.law_witnesses.push(
        LawWitness::new(
            TheoryId::FiniteSheaf,
            if compatibility.compatible {
                "finite_sheaf_gluing_sound"
            } else {
                "finite_sheaf_obstruction_boundary"
            },
            if compatibility.compatible {
                LawWitnessStatus::TheoremBound
            } else {
                LawWitnessStatus::RuntimeChecked
            },
        )
        .with_obligation("cover validates on the finite site")
        .with_obligation("restriction composition witnesses are checked")
        .with_evidence(proof.id.clone())
        .with_evidence(format!(
            "compatible={}, obstructions={}, restriction_witnesses={}",
            compatibility.compatible,
            compatibility.obstructions.len(),
            compatibility.restriction_witnesses.len()
        )),
    );
    evidence.assumption_bindings.push(AssumptionBinding::new(
        if compatibility.compatible {
            FINITE_SHEAF_GLUING_THEOREM_ID
        } else {
            FINITE_SHEAF_OBSTRUCTION_THEOREM_ID
        },
        FINITE_SHEAF_GLUING_LEAN_FILE,
        proof.id.clone(),
        "compatibleOverlaps",
        "SheafCompatibilityReport.compatible plus restriction witnesses",
    ));
    evidence.audit_entries.push(format!(
        "sheaf theory evidence: compatible={}, checked_overlaps={}, obstructions={}",
        compatibility.compatible,
        compatibility.checked_overlaps,
        compatibility.obstructions.len()
    ));
    Ok(evidence)
}

pub fn categorical_law_theory_evidence(
    identity_checked: bool,
    associativity_checked: bool,
) -> Result<TheoryEvidence> {
    if !identity_checked || !associativity_checked {
        return Err(Error::verification(
            "categorical theory evidence requires identity and associativity witnesses",
        ));
    }
    let mut evidence = TheoryEvidence::new(
        TheoryId::CategoricalLaw,
        "contract-witness category laws for implemented fixtures",
    );
    evidence.constraints.push(
        TheoryConstraint::new(
            TheoryId::CategoricalLaw,
            "category.identity_associativity",
            "identity and associativity laws hold for the checked contract witness scope",
        )
        .requiring("categorical identity witness")
        .requiring("categorical associativity witness"),
    );
    evidence.law_witnesses.push(
        LawWitness::new(
            TheoryId::CategoricalLaw,
            "identity",
            LawWitnessStatus::RuntimeChecked,
        )
        .with_evidence("categorical identity witness"),
    );
    evidence.law_witnesses.push(
        LawWitness::new(
            TheoryId::CategoricalLaw,
            "associativity",
            LawWitnessStatus::RuntimeChecked,
        )
        .with_evidence("categorical associative composition witness"),
    );
    evidence
        .audit_entries
        .push("categorical theory evidence: contract-witness scope only".to_string());
    Ok(evidence)
}

pub fn finite_sheaf_cech_obstruction_theory_evidence(
    summary: &CechObstructionSummary,
) -> Result<TheoryEvidence> {
    if !summary
        .cpu_oracle_fingerprint
        .starts_with("cech-summary-fnv64:")
    {
        return Err(Error::verification(
            "Cech obstruction summary requires CPU oracle fingerprint",
        ));
    }
    let mut evidence = TheoryEvidence::new(
        TheoryId::FiniteSheaf,
        "finite-site Cech H0/H1 obstruction summary",
    );
    evidence.constraints.push(
        TheoryConstraint::new(
            TheoryId::FiniteSheaf,
            "sheaf.cech_obstruction_summary",
            "finite cover summary records compatible H0 local sections and H1-style obstruction support counts",
        )
        .with_parameter("target", &summary.target.0)
        .with_parameter("cover_opens", summary.cover_opens.len())
        .with_parameter("compatible_h0_sections", summary.compatible_h0_sections)
        .with_parameter("h1_obstruction_count", summary.h1_obstruction_count)
        .requiring("CechObstructionSummary")
        .requiring("cpu_oracle_fingerprint"),
    );
    evidence.law_witnesses.push(
        LawWitness::new(
            TheoryId::FiniteSheaf,
            "finite_sheaf_cech_h0_h1_summary",
            LawWitnessStatus::RuntimeChecked,
        )
        .with_obligation("summary is computed from SectionTable::compatibility_report")
        .with_obligation("obstruction supports are finite-site opens from the checked cover")
        .with_evidence("CechObstructionSummary")
        .with_evidence(summary.cpu_oracle_fingerprint.clone()),
    );
    evidence.assumption_bindings.push(AssumptionBinding::new(
        FINITE_SHEAF_OBSTRUCTION_THEOREM_ID,
        FINITE_SHEAF_GLUING_LEAN_FILE,
        summary.cpu_oracle_fingerprint.clone(),
        "localizedObstructionSupport",
        "CechObstructionSummary(target, cover, H0-compatible count, H1 obstruction supports)",
    ));
    evidence.audit_entries.push(format!(
        "finite sheaf Cech summary: target={}, h0={}, h1_obstructions={}, fingerprint={}",
        summary.target.0,
        summary.compatible_h0_sections,
        summary.h1_obstruction_count,
        summary.cpu_oracle_fingerprint
    ));
    Ok(evidence)
}

pub fn padic_mul_with_theory_evidence(
    domain: &PadicDomain,
    lhs: &Padic,
    rhs: &Padic,
) -> Result<PadicTheoryOperatorReport> {
    let result = domain.mul(lhs, rhs)?;
    let lhs_valuation = domain.valuation_of(lhs)?;
    let rhs_valuation = domain.valuation_of(rhs)?;
    let result_valuation = domain.valuation_of(&result)?;
    let mut evidence = TheoryEvidence::new(
        TheoryId::PadicValuation,
        "fixed-precision p-adic multiplication valuation identity",
    );
    evidence.constraints.push(
        TheoryConstraint::new(
            TheoryId::PadicValuation,
            "padic.mul_valuation_identity",
            "v_p(x * y) = v_p(x) + v_p(y) for checked nonzero fixed-precision operands before precision saturation",
        )
        .with_parameter("prime", domain.meta.prime)
        .with_parameter("precision", domain.meta.precision)
        .with_parameter(
            "lhs_valuation",
            lhs_valuation
                .map(|value| value.to_string())
                .unwrap_or_else(|| "zero".to_string()),
        )
        .with_parameter(
            "rhs_valuation",
            rhs_valuation
                .map(|value| value.to_string())
                .unwrap_or_else(|| "zero".to_string()),
        )
        .with_parameter(
            "result_valuation",
            result_valuation
                .map(|value| value.to_string())
                .unwrap_or_else(|| "zero".to_string()),
        )
        .requiring("PadicDomain::mul")
        .requiring("PadicDomain::valuation_of"),
    );
    let status = match (lhs_valuation, rhs_valuation, result_valuation) {
        (Some(lhs_v), Some(rhs_v), Some(result_v)) if lhs_v.saturating_add(rhs_v) == result_v => {
            LawWitnessStatus::RuntimeChecked
        }
        (None, _, None) | (_, None, None) => LawWitnessStatus::RuntimeChecked,
        _ => LawWitnessStatus::Failed,
    };
    evidence.law_witnesses.push(
        LawWitness::new(
            TheoryId::PadicValuation,
            "valuation_multiplication_identity",
            status,
        )
        .with_obligation("operands must share the same fixed-precision p-adic domain")
        .with_evidence("PadicDomain::mul")
        .with_evidence("PadicDomain::valuation_of"),
    );
    evidence.audit_entries.push(format!(
        "padic multiplication theory operator: lhs_v={:?}, rhs_v={:?}, result_v={:?}",
        lhs_valuation, rhs_valuation, result_valuation
    ));
    if matches!(
        evidence.law_witnesses.first().map(|law| &law.status),
        Some(LawWitnessStatus::Failed)
    ) {
        return Err(Error::verification(
            "p-adic multiplication valuation identity failed for theory operator report",
        ));
    }
    Ok(PadicTheoryOperatorReport {
        result,
        lhs_valuation,
        rhs_valuation,
        result_valuation,
        evidence,
    })
}

pub fn padic_algebra_law_theory_evidence(
    domain: &PadicDomain,
    properties: &[PropertyCheckReport],
) -> Result<TheoryEvidence> {
    let required = [
        (
            "padic.identity_laws",
            "p-adic additive and multiplicative identities",
        ),
        ("padic.unit_inverse", "p-adic unit inverse law"),
        (
            "padic.distributivity",
            "p-adic multiplication distributes over addition",
        ),
        (
            "padic.vector_oracle_laws",
            "p-adic vector operation oracle laws",
        ),
    ];
    let mut evidence = TheoryEvidence::new(
        TheoryId::PadicValuation,
        "fixed-precision p-adic algebra runtime law checks",
    );
    evidence.constraints.push(
        TheoryConstraint::new(
            TheoryId::PadicValuation,
            "padic.algebra_laws",
            "runtime-checked p-adic identities, unit inverse, distributivity, and vector operation oracle laws",
        )
        .with_parameter("prime", domain.meta.prime)
        .with_parameter("precision", domain.meta.precision)
        .requiring("check_padic_contract_properties"),
    );

    for (law_id, property_name) in required {
        let report = properties
            .iter()
            .find(|report| report.property == property_name)
            .ok_or_else(|| {
                Error::verification(format!(
                    "p-adic algebra law evidence requires property report {property_name}"
                ))
            })?;
        if !report.passed {
            return Err(Error::verification(format!(
                "p-adic algebra law property failed: {} ({})",
                report.property, report.message
            )));
        }
        evidence.law_witnesses.push(
            LawWitness::new(
                TheoryId::PadicValuation,
                law_id,
                LawWitnessStatus::RuntimeChecked,
            )
            .with_obligation("operands must share the same fixed-precision p-adic domain")
            .with_evidence(format!(
                "PropertyCheckReport:{}:samples={}",
                report.property, report.samples_checked
            )),
        );
    }
    evidence.audit_entries.push(format!(
        "padic algebra law evidence: prime={}, precision={}, law_reports={}",
        domain.meta.prime,
        domain.meta.precision,
        required.len()
    ));
    Ok(evidence)
}

pub fn localize_sheaf_obstructions_with_theory_evidence<T>(
    plan: &ExecutionPlan,
    compatibility: &SheafCompatibilityReport<T>,
) -> Result<SheafObstructionLocalization> {
    let evidence = finite_sheaf_compatibility_theory_evidence(plan, compatibility)?;
    let mut localized_opens = Vec::new();
    let mut suggested_repairs = Vec::new();
    for obstruction in &compatibility.obstructions {
        let opens = obstruction
            .opens
            .iter()
            .map(|open| open.0.clone())
            .collect::<Vec<_>>();
        localized_opens.extend(opens.iter().cloned());
        suggested_repairs.push(format!(
            "repair {:?} on opens {}: {}",
            obstruction.kind,
            opens.join("|"),
            obstruction.message
        ));
    }
    localized_opens.sort();
    localized_opens.dedup();
    Ok(SheafObstructionLocalization {
        compatible: compatibility.compatible,
        obstruction_count: compatibility.obstructions.len(),
        localized_opens,
        suggested_repairs,
        evidence,
    })
}

pub fn validate_theory_evidence(
    evidence: &TheoryEvidence,
    required_laws: &[&str],
    required_evidence: &[&str],
) -> Result<()> {
    for law in required_laws {
        if !evidence.has_law(law) {
            return Err(Error::verification(format!(
                "theory {} missing law witness {}",
                evidence.theory.as_str(),
                law
            )));
        }
    }
    for requirement in required_evidence {
        if !evidence.has_required_evidence(requirement) {
            return Err(Error::verification(format!(
                "theory {} missing required evidence {}",
                evidence.theory.as_str(),
                requirement
            )));
        }
    }
    Ok(())
}

pub fn certify_theory_requirements(
    evidences: &[TheoryEvidence],
    theorem_registry: Option<&TheoremBindingRegistry>,
    requirements: &[CertifiedTheoryRequirement],
) -> CertifiedTheoryContractReport {
    let mut missing_laws = Vec::new();
    let mut missing_theorems = Vec::new();
    let mut missing_evidence = Vec::new();
    let mut audit_entries = Vec::new();

    for requirement in requirements {
        let matching_evidence = evidences
            .iter()
            .find(|evidence| evidence.theory == requirement.theory);
        let Some(evidence) = matching_evidence else {
            missing_laws.push(format!(
                "{}:{}",
                requirement.theory.as_str(),
                requirement.law_id
            ));
            audit_entries.push(format!(
                "missing theory evidence for {} law {}: {}",
                requirement.theory.as_str(),
                requirement.law_id,
                requirement.fallback_reason
            ));
            continue;
        };
        if !evidence.has_law(&requirement.law_id) {
            missing_laws.push(format!(
                "{}:{}",
                requirement.theory.as_str(),
                requirement.law_id
            ));
        }
        for required in &requirement.required_evidence {
            if !evidence.has_required_evidence(required) {
                missing_evidence.push(format!(
                    "{}:{} requires {}",
                    requirement.theory.as_str(),
                    requirement.law_id,
                    required
                ));
            }
        }
        if let Some(theorem_id) = &requirement.theorem_id {
            match theorem_registry {
                Some(registry) if registry.lookup(theorem_id).is_ok() => {
                    audit_entries.push(format!(
                        "theory requirement {}:{} bound to theorem {}",
                        requirement.theory.as_str(),
                        requirement.law_id,
                        theorem_id
                    ));
                }
                _ => missing_theorems.push(theorem_id.clone()),
            }
        }
        audit_entries.push(format!(
            "checked theory requirement {}:{}",
            requirement.theory.as_str(),
            requirement.law_id
        ));
    }

    if missing_laws.is_empty() && missing_theorems.is_empty() && missing_evidence.is_empty() {
        CertifiedTheoryContractReport::passed(audit_entries)
    } else {
        CertifiedTheoryContractReport::failed(
            missing_laws,
            missing_theorems,
            missing_evidence,
            audit_entries,
        )
    }
}

pub fn attach_theory_evidence_to_plan(plan: &mut ExecutionPlan, evidence: &TheoryEvidence) {
    for line in evidence.audit_lines() {
        plan.evidence_log
            .entries
            .push(format!("theory_contract: {line}"));
    }
    for constraint in &evidence.constraints {
        plan.obligations.push(Obligation {
            source: ObligationSource::Planner(format!("theory:{}", evidence.theory.as_str())),
            condition: format!("{}: {}", constraint.id, constraint.description),
            severity: ObligationSeverity::AuditOnly,
            status: DischargeStatus::Discharged("theory evidence attached".to_string()),
        });
    }
}