#!/usr/bin/env python3
"""Verify O-0176's formal theorem and source-specific membership pin."""

from __future__ import annotations

import json
from pathlib import Path
import subprocess


HERE = Path(__file__).resolve().parent
ROOT = HERE.parents[2]
LEAN_ROOT = ROOT / "lean"
SHARED_LEAN = LEAN_ROOT / "RHResearch" / "HeatBoundary.lean"
PINNED_LEAN = HERE / "HeatBoundary.lean"
ROUTE = ROOT / "scratch" / "proof-system--o0176-field-redirecting-manuscript"

FORMAL_SCOPE = "Set.insert target (Set.range counterexample)"
REQUIRED_CONDITIONS = {"M1", "M2", "M3", "M4"}
COMPLETION_VERDICT = "ruled_out_if_admission_clauses_hold"
ALLOWED_ACTUAL_VERDICTS = {
    "actual_paper_nonmember",
    "theorem_input_not_member",
    "fails_at_target",
}
EXPECTED_PROGRAM_SOURCES = {
    "heat-flow": {"debruijn-1950", "rodgers-tao-2020"},
    "jensen": {
        "osullivan-2021",
        "griffin-ono-rolen-zagier-2019",
        "farmer-2022",
    },
    "laguerre": {
        "csordas-norfolk-varga-1986",
        "csordas-vishnyakova-2013",
    },
    "weil": {"bombieri-weil-2000", "suzuki-weil-2026"},
    "de-branges": {"conrey-li-2000"},
    "canonical-systems": {"suzuki-canonical-2018"},
    "total-positivity": {"grochenig-2023"},
}
EXPECTED_CONTROL_SOURCES = {
    "li": {"bombieri-lagarias-1999"},
    "nyman-beurling": {"baez-duarte-2002"},
}


def load_json(path: Path) -> dict:
    with path.open(encoding="utf-8") as handle:
        return json.load(handle)


def verify_lean() -> None:
    if SHARED_LEAN.read_bytes() != PINNED_LEAN.read_bytes():
        raise AssertionError("shared and pinned HeatBoundary.lean differ")

    lean_text = PINNED_LEAN.read_text(encoding="utf-8")
    if lean_text.count(FORMAL_SCOPE) < 2:
        raise AssertionError("Lean M4 scope is not restricted in both theorems")
    for theorem in (
        "no_accumulating_counterexample_interior_certificate",
        "no_open_certificate_at_accumulation",
        "no_certificate_interior_at_accumulation",
        "no_uniform_coercive_form",
        "no_finite_strict_continuous_hierarchy",
    ):
        if theorem not in lean_text:
            raise AssertionError(f"missing formal theorem: {theorem}")

    subprocess.run(
        ["lake", "env", "lean", str(PINNED_LEAN)],
        cwd=LEAN_ROOT,
        check=True,
    )


def verify_programs(
    canonical: dict,
    route_dossiers: dict,
    source_keys: set[str],
) -> None:
    programs = canonical.get("published_programs")
    if not isinstance(programs, list) or len(programs) != 7:
        raise AssertionError("canonical witness must contain seven programs")
    route_programs = {
        program["id"]: program for program in route_dossiers["claimed_programs"]
    }
    if set(route_programs) != set(EXPECTED_PROGRAM_SOURCES):
        raise AssertionError("route dossier program coverage changed")

    seen: set[str] = set()
    for program in programs:
        program_id = program.get("id")
        if program_id in seen:
            raise AssertionError(f"duplicate program id: {program_id!r}")
        seen.add(program_id)
        if program_id not in EXPECTED_PROGRAM_SOURCES:
            raise AssertionError(f"unexpected program id: {program_id!r}")

        sources = set(program.get("primary_sources", []))
        if sources != EXPECTED_PROGRAM_SOURCES[program_id]:
            raise AssertionError(f"{program_id}: primary-source set changed")
        if not sources <= source_keys:
            raise AssertionError(f"{program_id}: unpinned source key")

        conditions = program.get("source_conditions")
        if not isinstance(conditions, dict) or set(conditions) != REQUIRED_CONDITIONS:
            raise AssertionError(f"{program_id}: M1-M4 source audit incomplete")
        if not all(isinstance(value, str) and value for value in conditions.values()):
            raise AssertionError(f"{program_id}: empty source-condition verdict")

        actual = program.get("actual_paper_verdict")
        if actual not in ALLOWED_ACTUAL_VERDICTS:
            raise AssertionError(
                f"{program_id}: actual paper was admitted or verdict changed"
            )
        if program.get("completion_verdict") != COMPLETION_VERDICT:
            raise AssertionError(f"{program_id}: conditional verdict weakened")
        clauses = program.get("admission_clauses")
        if not isinstance(clauses, list) or len(clauses) < 4:
            raise AssertionError(f"{program_id}: admission checklist incomplete")
        if not all(isinstance(clause, str) and clause for clause in clauses):
            raise AssertionError(f"{program_id}: empty admission clause")

        route = route_programs[program_id]
        exact_pairs = {
            "primary_sources": "source_keys",
            "source_conditions": "source_premises",
            "actual_paper_verdict": "actual_paper_verdict",
            "admission_clauses": "admission_clauses",
            "completion_verdict": "completion_verdict",
            "survives": "surviving_mechanisms",
        }
        for canonical_key, route_key in exact_pairs.items():
            if program[canonical_key] != route[route_key]:
                raise AssertionError(
                    f"{program_id}: canon and manuscript dossier disagree on "
                    f"{canonical_key}"
                )

    if seen != set(EXPECTED_PROGRAM_SOURCES):
        raise AssertionError(f"program coverage changed: {seen!r}")


def verify_controls(
    canonical: dict,
    route_dossiers: dict,
    source_keys: set[str],
) -> None:
    controls = canonical.get("boundary_controls")
    if not isinstance(controls, list) or len(controls) != 2:
        raise AssertionError("canonical witness must contain two controls")
    route_controls = {
        control["id"]: control for control in route_dossiers["boundary_controls"]
    }
    seen: set[str] = set()
    for control in controls:
        control_id = control.get("id")
        if control_id not in EXPECTED_CONTROL_SOURCES:
            raise AssertionError(f"unexpected control id: {control_id!r}")
        seen.add(control_id)
        sources = set(control.get("primary_sources", []))
        if sources != EXPECTED_CONTROL_SOURCES[control_id]:
            raise AssertionError(f"{control_id}: primary-source set changed")
        if not sources <= source_keys:
            raise AssertionError(f"{control_id}: unpinned source key")
        route = route_controls[control_id]
        if control["primary_sources"] != route["source_keys"]:
            raise AssertionError(f"{control_id}: canon and route sources differ")
        if control["actual_paper_verdict"] != route["actual_paper_verdict"]:
            raise AssertionError(f"{control_id}: canon and route verdict differ")
        if control["reason"] != route["reason_not_claimed_as_direct_program_member"]:
            raise AssertionError(f"{control_id}: canon and route rationale differ")
        if control["survives"] != route["survives"]:
            raise AssertionError(f"{control_id}: canon and route survivor differs")
    if seen != set(EXPECTED_CONTROL_SOURCES):
        raise AssertionError("boundary-control coverage changed")


def verify_membership_schema() -> None:
    canonical = load_json(HERE / "membership.json")
    route_dossiers = load_json(ROUTE / "dossiers.json")
    source_manifest = load_json(ROUTE / "source_manifest.json")

    if canonical.get("formal_scope") != FORMAL_SCOPE:
        raise AssertionError("canonical M4 scope changed")
    conditions = canonical.get("required_conditions")
    if not isinstance(conditions, dict) or set(conditions) != REQUIRED_CONDITIONS:
        raise AssertionError("canonical M1-M4 schema changed")

    source_audit = canonical.get("source_audit")
    expected_audit = (
        "literature/"
        "2026-07-19-uniform-interior-certificate-barrier-primary-sources.md"
    )
    if source_audit != expected_audit or not (ROOT / source_audit).is_file():
        raise AssertionError("source audit path changed or is missing")
    audit_text = (ROOT / source_audit).read_text(encoding="utf-8")
    if "No cited paper is classified as an actual AIC member." not in audit_text:
        raise AssertionError("source audit no longer disclaims paper membership")
    if "No published paper in the named families is an AIC member." not in audit_text:
        raise AssertionError("source audit conclusion is missing nonmembership")

    source_keys = set(source_manifest["sources"])
    verify_programs(canonical, route_dossiers, source_keys)
    verify_controls(canonical, route_dossiers, source_keys)


def main() -> None:
    verify_lean()
    verify_membership_schema()
    print(
        "verified O-0176: exact target-plus-sequence theorem; seven "
        "source-specific nonmember dossiers; two boundary controls"
    )


if __name__ == "__main__":
    main()
