#!/usr/bin/env python3
"""Check whether the inherited-state predecessor is proven on the confirmed route."""
from __future__ import annotations

import argparse
import html
import json
from pathlib import Path


ROOT = Path(__file__).resolve().parents[1]
OUT = ROOT / "out"
SOURCE_MAP = "map1_01a"
TARGET_MAP = "map2_02d"
PREDECESSOR_ROUTE_ORDER_FAILED_GATE_IDS = [
    "source-current-selector-merge-order",
    "predecessor-branch-state-persistence",
    "strict-source-hotspot",
]
PREDECESSOR_ROUTE_ORDER_EVIDENCE_REFS = [
    {
        "path": "out/save_scene_selectors.json",
        "fields": ["selector", "selectedPointerHex", "fieldMaps"],
    },
    {
        "path": "out/save_selector_inherited_state_candidates.json",
        "fields": ["bestPrevious", "currentSelector", "sharedMaps", "introducedMaps"],
    },
    {
        "path": "out/playable_progress.json",
        "fields": ["reachableFromStart", "confirmedEdges"],
    },
    {
        "path": "out/save_selector_predecessor_route_order.json",
        "fields": ["orderEvidence", "remainingProofs", "routeOrderProven"],
    },
]


def selector_key(row: dict) -> str:
    return f"{row.get('group')}:{row.get('slot')}"


def find_selector(selectors: list[dict], key: str) -> dict:
    for row in selectors:
        if selector_key(row) == key:
            return row
    raise ValueError(f"selector {key} not found")


def selector_record(row: dict, confirmed_route_maps: set[str]) -> dict:
    field_maps = row.get("fieldMaps") or []
    field_set = set(field_maps)
    return {
        "selector": selector_key(row),
        "rootHex": row.get("selectedPointerHex"),
        "fieldMaps": field_maps,
        "containsSource": SOURCE_MAP in field_set,
        "containsTarget": TARGET_MAP in field_set,
        "confirmedOverlap": sorted(confirmed_route_maps & field_set),
    }


def build_summary(selectors: list[dict], inherited: dict, playable: dict) -> dict:
    predecessor = inherited.get("bestPrevious") or {}
    predecessor_key = predecessor.get("selector") or "1:0"
    current_key = inherited.get("currentSelector") or "2:0"
    predecessor_row = find_selector(selectors, predecessor_key)
    current_row = find_selector(selectors, current_key)
    confirmed_reachable = playable.get("reachableFromStart") or []
    confirmed_edges = playable.get("confirmedEdges") or []
    confirmed_route_maps = set(confirmed_reachable)
    predecessor_maps = set(predecessor_row.get("fieldMaps") or [])
    current_maps = set(current_row.get("fieldMaps") or [])
    current_only_confirmed = sorted(confirmed_route_maps & current_maps)
    predecessor_confirmed_overlap = sorted(confirmed_route_maps & predecessor_maps)
    previous_rows = [
        row
        for row in selectors
        if row.get("fieldMaps")
        and (row.get("group"), row.get("slot")) < (current_row.get("group"), current_row.get("slot"))
    ]
    source_side_previous = [
        selector_record(row, confirmed_route_maps)
        for row in previous_rows
        if SOURCE_MAP in set(row.get("fieldMaps") or [])
    ]
    target_side_previous = [
        selector_record(row, confirmed_route_maps)
        for row in previous_rows
        if TARGET_MAP in set(row.get("fieldMaps") or []) and SOURCE_MAP not in set(row.get("fieldMaps") or [])
    ]
    route_pair_previous = [
        selector_record(row, confirmed_route_maps)
        for row in previous_rows
        if {SOURCE_MAP, TARGET_MAP}.issubset(set(row.get("fieldMaps") or []))
    ]
    source_side_previous.sort(key=lambda item: (-len(item["confirmedOverlap"]), item["selector"]))
    target_side_previous.sort(key=lambda item: (item["selector"] != predecessor_key, item["selector"]))
    source_route_previous = source_side_previous[0] if source_side_previous else None
    predecessor_is_target_side_only = TARGET_MAP in predecessor_maps and SOURCE_MAP not in predecessor_maps
    selector_merge_gap_open = (
        SOURCE_MAP in current_maps
        and TARGET_MAP in current_maps
        and bool(source_side_previous)
        and bool(target_side_previous)
        and not route_pair_previous
    )
    order_evidence = [
        {
            "kind": "selector-index",
            "status": "supports-order",
            "detail": f"{predecessor_key} has a lower selector group/slot than {current_key}.",
        },
        {
            "kind": "selector-progress",
            "status": "supports-candidate",
            "detail": (
                f"{predecessor_key} shares {len(predecessor.get('sharedMaps') or [])} maps with {current_key} "
                f"and {current_key} introduces {', '.join(predecessor.get('introducedMaps') or []) or 'no maps'}."
            ),
        },
        {
            "kind": "source-side-selector",
            "status": "confirmed-route-overlap" if source_route_previous else "missing",
            "detail": (
                f"{SOURCE_MAP} is carried by previous selector "
                f"{(source_route_previous or {}).get('selector', 'none')}; "
                f"confirmed overlap={', '.join((source_route_previous or {}).get('confirmedOverlap') or []) or 'none'}."
            ),
        },
        {
            "kind": "target-side-predecessor",
            "status": "target-state-only" if predecessor_is_target_side_only else "also-source-side",
            "detail": (
                f"{predecessor_key} contains {TARGET_MAP}={TARGET_MAP in predecessor_maps} and "
                f"{SOURCE_MAP}={SOURCE_MAP in predecessor_maps}; it is therefore "
                f"{'not ' if not predecessor_is_target_side_only else ''}separate from the confirmed source-side selector."
            ),
        },
        {
            "kind": "selector-merge-shape",
            "status": "merge-gap-open" if selector_merge_gap_open else "not-merge-shaped",
            "detail": (
                f"{current_key} contains both {SOURCE_MAP} and {TARGET_MAP}; "
                f"previous selectors containing both route maps={len(route_pair_previous)}."
            ),
        },
        {
            "kind": "confirmed-route",
            "status": "does-not-prove-order",
            "detail": (
                f"confirmed route reaches {', '.join(confirmed_reachable)}; it overlaps {predecessor_key} in "
                f"{', '.join(predecessor_confirmed_overlap) or 'no maps'}."
            ),
        },
        {
            "kind": "confirmed-edge",
            "status": "does-not-prove-order",
            "detail": (
                "confirmed edges are "
                + (
                    ", ".join(f"{edge.get('source')}->{edge.get('target')}" for edge in confirmed_edges)
                    if confirmed_edges
                    else "empty"
                )
                + f"; none executes {predecessor_key} before {current_key}."
            ),
        },
    ]
    route_order_proven = bool(predecessor_confirmed_overlap) and any(
        edge.get("source") in predecessor_maps or edge.get("target") in predecessor_maps for edge in confirmed_edges
    )
    missing_evidence = [
        (
            f"prove the source-side selector {(source_route_previous or {}).get('selector', 'unknown')} "
            f"can progress into {current_key} after {predecessor_key} state is established"
        ),
        "prove secondaryBranchState persists from predecessor fill to current reader",
        "find strict map1_01a source coordinate or hotspot",
    ]
    failed_gate_ids = [] if route_order_proven else PREDECESSOR_ROUTE_ORDER_FAILED_GATE_IDS
    conclusion = (
        f"{predecessor_key} remains the strongest inherited secondaryBranchState producer candidate, but it is "
        f"target-side only for this route: it contains {TARGET_MAP} and does not contain {SOURCE_MAP}. The confirmed "
        f"source-side route overlaps {(source_route_previous or {}).get('selector', 'no previous selector')}, while "
        f"{current_key} looks like a merge of source-side {SOURCE_MAP} and target-side {TARGET_MAP} lists. The fill "
        "effect must stay blocked until save progression, a strict hotspot, or a VM/runtime trace proves that this "
        "merge path executes the predecessor state before the current reader."
    )
    return {
        "source": SOURCE_MAP,
        "target": TARGET_MAP,
        "currentSelector": current_key,
        "currentRootHex": current_row.get("selectedPointerHex"),
        "predecessorSelector": predecessor_key,
        "predecessorRootHex": predecessor_row.get("selectedPointerHex"),
        "predecessorMaps": predecessor_row.get("fieldMaps") or [],
        "currentMaps": current_row.get("fieldMaps") or [],
        "confirmedReachableFromStart": confirmed_reachable,
        "confirmedEdges": confirmed_edges,
        "predecessorConfirmedOverlap": predecessor_confirmed_overlap,
        "currentConfirmedOverlap": current_only_confirmed,
        "sourceSidePreviousSelectors": source_side_previous,
        "targetSidePreviousSelectors": target_side_previous,
        "routePairPreviousSelectors": route_pair_previous,
        "sourceRoutePreviousSelector": (source_route_previous or {}).get("selector"),
        "sourceRoutePreviousRootHex": (source_route_previous or {}).get("rootHex"),
        "sourceRoutePreviousConfirmedOverlap": (source_route_previous or {}).get("confirmedOverlap") or [],
        "predecessorIsTargetSideOnly": predecessor_is_target_side_only,
        "samePreviousContainsRoutePair": bool(route_pair_previous),
        "selectorMergeGapOpen": selector_merge_gap_open,
        "selectorIndexOrderSupportsPredecessor": True,
        "selectorProgressSupportsPredecessor": predecessor_key == "1:0",
        "routeOrderProven": route_order_proven,
        "proofFound": route_order_proven,
        "predecessorRouteOrderProofFound": route_order_proven,
        "failedPredecessorRouteOrderGateIds": failed_gate_ids,
        "missingEvidence": missing_evidence if failed_gate_ids else [],
        "remainingProofs": missing_evidence if failed_gate_ids else [],
        "evidenceRefs": PREDECESSOR_ROUTE_ORDER_EVIDENCE_REFS,
        "evidenceRefCount": len(PREDECESSOR_ROUTE_ORDER_EVIDENCE_REFS),
        "promotionStatus": "blocked",
        "orderEvidence": order_evidence,
        "conclusion": conclusion,
    }


def markdown(summary: dict) -> str:
    lines = [
        "# Save Selector Predecessor Route Order",
        "",
        f"- predecessor: `{summary['predecessorSelector']}` root `{summary['predecessorRootHex']}`",
        f"- current: `{summary['currentSelector']}` root `{summary['currentRootHex']}`",
        f"- confirmed route: {', '.join(summary['confirmedReachableFromStart'])}",
        f"- source-side previous selector: `{summary.get('sourceRoutePreviousSelector')}` overlap {', '.join(summary.get('sourceRoutePreviousConfirmedOverlap') or []) or 'none'}",
        f"- predecessor target-side only: {summary.get('predecessorIsTargetSideOnly')}",
        f"- selector merge gap open: {summary.get('selectorMergeGapOpen')}",
        f"- predecessor confirmed overlap: {', '.join(summary['predecessorConfirmedOverlap']) or 'none'}",
        f"- route order proven: {summary['routeOrderProven']}",
        f"- proof found: {summary.get('proofFound')}",
        f"- predecessor route order proof found: {summary.get('predecessorRouteOrderProofFound')}",
        f"- failed predecessor route-order gates: `{','.join(summary.get('failedPredecessorRouteOrderGateIds') or []) or '-'}`",
        f"- missing evidence count: {len(summary.get('missingEvidence') or [])}",
        f"- evidence refs: {summary.get('evidenceRefCount')}",
        f"- promotion status: {summary['promotionStatus']}",
        "",
        summary["conclusion"],
        "",
        "## Evidence",
        "",
        "| kind | status | detail |",
        "| --- | --- | --- |",
    ]
    for row in summary["orderEvidence"]:
        lines.append(f"| {row['kind']} | {row['status']} | {row['detail']} |")
    lines.extend(["", "## Missing Evidence", ""])
    lines.extend(f"- {item}" for item in summary["missingEvidence"])
    lines.extend(["", "## Evidence Refs", "", "| path | fields |", "| --- | --- |"])
    for row in summary.get("evidenceRefs") or []:
        lines.append(f"| `{row.get('path')}` | {', '.join(row.get('fields') or []) or '-'} |")
    lines.extend(["", "## Remaining Proofs", ""])
    lines.extend(f"- {item}" for item in summary["remainingProofs"])
    lines.append("")
    return "\n".join(lines)


def html_page(summary: dict) -> str:
    evidence_rows = "\n".join(
        "<tr>"
        f"<td>{html.escape(row['kind'])}</td>"
        f"<td>{html.escape(row['status'])}</td>"
        f"<td>{html.escape(row['detail'])}</td>"
        "</tr>"
        for row in summary["orderEvidence"]
    )
    proofs = "".join(f"<li>{html.escape(item)}</li>" for item in summary["remainingProofs"])
    missing = "".join(f"<li>{html.escape(item)}</li>" for item in summary.get("missingEvidence") or [])
    evidence_refs = "\n".join(
        "<tr>"
        f"<td><code>{html.escape(str(row.get('path')))}</code></td>"
        f"<td>{html.escape(', '.join(row.get('fields') or []) or '-')}</td>"
        "</tr>"
        for row in summary.get("evidenceRefs") or []
    )
    return "\n".join([
        "<!doctype html><meta charset=\"utf-8\"><title>Save Selector Predecessor Route Order</title>",
        "<style>body{font-family:system-ui,sans-serif;background:#111;color:#eee;max-width:1100px;margin:24px auto}table{border-collapse:collapse}td,th{border:1px solid #444;padding:6px 8px;vertical-align:top}code{color:#9bd4ff}</style>",
        "<h1>Save Selector Predecessor Route Order</h1>",
        f"<p>Predecessor <code>{summary['predecessorSelector']}</code> root <code>{summary['predecessorRootHex']}</code>; current <code>{summary['currentSelector']}</code> root <code>{summary['currentRootHex']}</code>.</p>",
        f"<p>Confirmed route: {html.escape(', '.join(summary['confirmedReachableFromStart']))}</p>",
        f"<p>source-side previous selector: <code>{html.escape(str(summary.get('sourceRoutePreviousSelector')))}</code>; overlap: {html.escape(', '.join(summary.get('sourceRoutePreviousConfirmedOverlap') or []) or 'none')}; predecessor target-side only: {summary.get('predecessorIsTargetSideOnly')}; selector merge gap open: {summary.get('selectorMergeGapOpen')}</p>",
        f"<p>predecessor confirmed overlap: {html.escape(', '.join(summary['predecessorConfirmedOverlap']) or 'none')}</p>",
        (
            f"<p>route order proven: {summary['routeOrderProven']}; "
            f"proof found: {summary.get('proofFound')}; "
            f"failed route-order gates: {html.escape(', '.join(summary.get('failedPredecessorRouteOrderGateIds') or []) or '-')}; "
            f"missing evidence count: {len(summary.get('missingEvidence') or [])}; "
            f"evidence refs: {summary.get('evidenceRefCount')}; "
            f"promotion status: {html.escape(summary['promotionStatus'])}</p>"
        ),
        f"<p>{html.escape(summary['conclusion'])}</p>",
        "<table><thead><tr><th>kind</th><th>status</th><th>detail</th></tr></thead><tbody>",
        evidence_rows,
        "</tbody></table>",
        "<h2>Missing Evidence</h2>",
        f"<ul>{missing}</ul>",
        "<h2>Evidence Refs</h2>",
        "<table><thead><tr><th>path</th><th>fields</th></tr></thead><tbody>",
        evidence_refs,
        "</tbody></table>",
        "<h2>Remaining Proofs</h2>",
        f"<ul>{proofs}</ul>",
    ])


def write_outputs(summary: dict, out_dir: Path) -> None:
    out_dir.mkdir(parents=True, exist_ok=True)
    (out_dir / "save_selector_predecessor_route_order.json").write_text(
        json.dumps(summary, ensure_ascii=False, indent=2) + "\n",
        encoding="utf-8",
    )
    (out_dir / "save_selector_predecessor_route_order.html").write_text(html_page(summary), encoding="utf-8")


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument("--selectors", type=Path, default=OUT / "save_scene_selectors.json")
    parser.add_argument("--inherited", type=Path, default=OUT / "save_selector_inherited_state_candidates.json")
    parser.add_argument("--playable", type=Path, default=OUT / "playable_progress.json")
    parser.add_argument("--out-dir", type=Path, default=OUT)
    args = parser.parse_args()
    summary = build_summary(
        json.loads(args.selectors.read_text(encoding="utf-8")),
        json.loads(args.inherited.read_text(encoding="utf-8")),
        json.loads(args.playable.read_text(encoding="utf-8")),
    )
    write_outputs(summary, args.out_dir)
    print(f"wrote predecessor route order -> {args.out_dir / 'save_selector_predecessor_route_order.html'}")


if __name__ == "__main__":
    main()