#!/usr/bin/env python3
"""Document the unresolved selector equation for map1_01a -> map2_02d."""
from __future__ import annotations

import argparse
import html
import json
from pathlib import Path


ROOT = Path(__file__).resolve().parents[1]
OUT = ROOT / "out"


SUMMARY = {
    "route": "map1_01a -> map2_02d",
    "writerVaHex": "0x005428bc",
    "writerValueHex": "0x00208212",
    "readerVaHex": "0x00542b0c",
    "readerValueHex": "0x00209011",
    "selectionOffsetHex": "0x20",
    "writerHandlerVaHex": "0x0040b55f",
    "readerHandlerVaHex": "0x0040b4e6",
    "activeFlagVaHex": "0x00457744",
    "primaryBranchStateVaHex": "0x0059e370",
    "secondaryBranchStateVaHex": "0x0059e360",
    "selectionBufferContextOffsetHex": "0xa8",
    "writerTable": "secondaryBranchState",
    "readerTable": "secondaryBranchState",
    "writerAlgorithm": [
        "stream+1 is 0x82, so opcode 0x12 uses secondaryBranchState at 0x0059e360.",
        "If byte(0x00457744) is set, the search starts from the existing selectionBuffer[0x20]; otherwise it starts from 0.",
        "The handler first walks backward through 12 slots with wraparound until it finds a nonzero secondaryBranchState slot.",
        "It then walks forward through 12 slots with wraparound until it finds a nonzero secondaryBranchState slot.",
        "The final slot index is written to selectionBuffer[0x20].",
    ],
    "readerAlgorithm": [
        "stream+1 is 0x90, so opcode 0x11 also reads secondaryBranchState at 0x0059e360.",
        "It reads slot = selectionBuffer[0x20].",
        "If secondaryBranchState[slot] == 1, execution falls through to 0x00542b14.",
        "Otherwise execution jumps to the stream operand target 0x0053f46f.",
    ],
    "resolved": False,
    "remainingUnknowns": [
        "runtime contents of secondaryBranchState[0..11] at the 0x005428bc writer",
        "runtime value of byte(0x00457744)",
        "prior value of selectionBuffer[0x20] when byte(0x00457744) is set",
        "control-flow proof that 0x005428bc reaches the 0x00542b0c frontier reader",
        "strict source tile coordinate or hotspot for map1_01a",
    ],
    "promotionStatus": "blocked",
    "conclusion": (
        "The inherited selector is now reduced to a 12-slot secondaryBranchState equation, not a constant transition. "
        "The writer can only guarantee a nonzero selected slot; the frontier reader requires that selected slot's value to be exactly 1. "
        "Without the runtime secondaryBranchState contents and a strict map1_01a source hotspot, this edge remains blocked."
    ),
}


def load_json(path: Path, fallback: dict) -> dict:
    if not path.exists():
        return fallback
    return json.loads(path.read_text(encoding="utf-8"))


def build_summary(
    predecessor_state_effect: dict | None = None,
    active_flag_effect: dict | None = None,
) -> dict:
    predecessor_state_effect = (
        predecessor_state_effect
        if predecessor_state_effect is not None
        else load_json(OUT / "save_selector_predecessor_state_effect.json", {})
    )
    active_flag_effect = (
        active_flag_effect
        if active_flag_effect is not None
        else load_json(OUT / "save_selector_active_flag_effect.json", {})
    )

    summary = dict(SUMMARY)
    predecessor_table = predecessor_state_effect.get("secondaryBranchStateAfterFill") or []
    predecessor_narrows_equation = (
        predecessor_state_effect.get("predecessorSelector") == "1:0"
        and predecessor_state_effect.get("currentSelector") == "2:0"
        and predecessor_state_effect.get("allStartsPassReader") is True
        and active_flag_effect.get("allPredecessorStartsPass") is True
        and active_flag_effect.get("priorSelectionBufferStillPrimaryBlockerUnderPredecessorHypothesis") is False
    )
    if predecessor_narrows_equation:
        summary["equationNarrowedByPredecessorHypothesis"] = True
        summary["predecessorFillHypothesis"] = {
            "predecessorSelector": predecessor_state_effect.get("predecessorSelector"),
            "predecessorRootHex": predecessor_state_effect.get("predecessorRootHex"),
            "fillValueHex": predecessor_state_effect.get("fillValueHex"),
            "secondaryBranchStateAfterFill": predecessor_table,
            "allStartsPassReader": predecessor_state_effect.get("allStartsPassReader"),
        }
        summary["activeFlagEffect"] = {
            "activeFlagResolvedStaticDefault": active_flag_effect.get("activeFlagResolvedStaticDefault"),
            "allPredecessorStartsPass": active_flag_effect.get("allPredecessorStartsPass"),
            "priorSelectionBufferStillPrimaryBlockerUnderPredecessorHypothesis": active_flag_effect.get(
                "priorSelectionBufferStillPrimaryBlockerUnderPredecessorHypothesis"
            ),
        }
        summary["remainingUnknowns"] = [
            "prove predecessor 1:0 executes before current selector 2:0 in the normal route",
            "prove secondaryBranchState persists to 0x005428bc/0x00542b0c",
            "control-flow proof that 0x005428bc reaches the 0x00542b0c frontier reader",
            "strict source tile coordinate or hotspot for map1_01a",
            "real selector 2:0 savedata or equivalent runtime trace",
        ]
        summary["conclusion"] = (
            "The 12-slot secondaryBranchState equation is still unresolved as confirmed route proof, but the strongest "
            "predecessor-fill hypothesis narrows the value side: if selector 1:0 leaves secondaryBranchState as "
            "[1,1,0..], every active-flag/start-slot case selects a slot whose value is 1. Under that hypothesis, the "
            "prior selectionBuffer[0x20] value is no longer the primary blocker. Promotion remains blocked on proving "
            "1:0 executes before 2:0, proving the state persists through the gated path to 0x00542b0c, and finding a "
            "strict map1_01a source hotspot."
        )
    else:
        summary["equationNarrowedByPredecessorHypothesis"] = False
    return summary


def markdown(summary: dict) -> str:
    lines = [
        "# Save Selector Branch Selector Equation",
        "",
        f"- route: {summary['route']}",
        f"- writer: `{summary['writerVaHex']}` `{summary['writerValueHex']}` via `{summary['writerHandlerVaHex']}`",
        f"- reader: `{summary['readerVaHex']}` `{summary['readerValueHex']}` via `{summary['readerHandlerVaHex']}`",
        f"- selection offset: `{summary['selectionOffsetHex']}`",
        f"- writer table: `{summary['writerTable']}` `{summary['secondaryBranchStateVaHex']}`",
        f"- reader table: `{summary['readerTable']}` `{summary['secondaryBranchStateVaHex']}`",
        f"- promotion status: {summary['promotionStatus']}",
        f"- conclusion: {summary['conclusion']}",
        "",
        "## Writer Algorithm",
        "",
    ]
    lines.extend(f"- {item}" for item in summary["writerAlgorithm"])
    lines.extend(["", "## Reader Algorithm", ""])
    lines.extend(f"- {item}" for item in summary["readerAlgorithm"])
    if summary.get("equationNarrowedByPredecessorHypothesis"):
        predecessor = summary.get("predecessorFillHypothesis") or {}
        active_flag = summary.get("activeFlagEffect") or {}
        lines.extend([
            "",
            "## Predecessor-Fill Narrowing",
            "",
            f"- predecessor: `{predecessor.get('predecessorSelector')}` root `{predecessor.get('predecessorRootHex')}`",
            f"- fill: `{predecessor.get('fillValueHex')}` -> `{predecessor.get('secondaryBranchStateAfterFill')}`",
            f"- all starts pass reader: {predecessor.get('allStartsPassReader')}",
            f"- active flag default resolved: {active_flag.get('activeFlagResolvedStaticDefault')}",
            f"- prior selectionBuffer still primary blocker: {active_flag.get('priorSelectionBufferStillPrimaryBlockerUnderPredecessorHypothesis')}",
        ])
    lines.extend(["", "## Remaining Unknowns", ""])
    lines.extend(f"- {item}" for item in summary["remainingUnknowns"])
    lines.append("")
    return "\n".join(lines)


def html_page(summary: dict) -> str:
    def ul(items: list[str]) -> str:
        return "<ul>" + "".join(f"<li>{html.escape(item)}</li>" for item in items) + "</ul>"

    return "\n".join([
        "<!doctype html><meta charset=\"utf-8\"><title>Save Selector Branch Selector Equation</title>",
        "<style>body{font-family:system-ui,sans-serif;background:#111;color:#eee;max-width:1100px;margin:24px auto;line-height:1.45}code{color:#9bd4ff}</style>",
        "<h1>Save Selector Branch Selector Equation</h1>",
        f"<p><strong>Route:</strong> {html.escape(summary['route'])}</p>",
        f"<p><strong>Writer:</strong> <code>{summary['writerVaHex']}</code> <code>{summary['writerValueHex']}</code> via <code>{summary['writerHandlerVaHex']}</code></p>",
        f"<p><strong>Reader:</strong> <code>{summary['readerVaHex']}</code> <code>{summary['readerValueHex']}</code> via <code>{summary['readerHandlerVaHex']}</code></p>",
        f"<p><strong>Conclusion:</strong> {html.escape(summary['conclusion'])}</p>",
        "<h2>Writer Algorithm</h2>",
        ul(summary["writerAlgorithm"]),
        "<h2>Reader Algorithm</h2>",
        ul(summary["readerAlgorithm"]),
        *(
            [
                "<h2>Predecessor-Fill Narrowing</h2>",
                ul([
                    f"predecessor {summary.get('predecessorFillHypothesis', {}).get('predecessorSelector')} root {summary.get('predecessorFillHypothesis', {}).get('predecessorRootHex')}",
                    f"fill {summary.get('predecessorFillHypothesis', {}).get('fillValueHex')} -> {summary.get('predecessorFillHypothesis', {}).get('secondaryBranchStateAfterFill')}",
                    f"all starts pass reader: {summary.get('predecessorFillHypothesis', {}).get('allStartsPassReader')}",
                    f"active flag default resolved: {summary.get('activeFlagEffect', {}).get('activeFlagResolvedStaticDefault')}",
                    f"prior selectionBuffer still primary blocker: {summary.get('activeFlagEffect', {}).get('priorSelectionBufferStillPrimaryBlockerUnderPredecessorHypothesis')}",
                ]),
            ]
            if summary.get("equationNarrowedByPredecessorHypothesis")
            else []
        ),
        "<h2>Remaining Unknowns</h2>",
        ul(summary["remainingUnknowns"]),
    ])


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


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument("--out-dir", type=Path, default=OUT)
    parser.add_argument("--predecessor-state-effect", type=Path, default=OUT / "save_selector_predecessor_state_effect.json")
    parser.add_argument("--active-flag-effect", type=Path, default=OUT / "save_selector_active_flag_effect.json")
    args = parser.parse_args()
    summary = build_summary(
        load_json(args.predecessor_state_effect, {}),
        load_json(args.active_flag_effect, {}),
    )
    write_outputs(summary, args.out_dir)
    print(f"wrote branch selector equation -> {args.out_dir / 'save_selector_branch_selector_equation.html'}")


if __name__ == "__main__":
    main()