#!/usr/bin/env python3
"""Combine active-flag evidence with the current selector equation."""
from __future__ import annotations

import argparse
import html
import json
from pathlib import Path
from typing import Any


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


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


def simulate_opcode12_selected_slot(table: list[int], start: int) -> int:
    slot = start & 0xFF
    for _ in range(12):
        slot = slot - 1 if slot else 0x0B
        if table[slot]:
            break
    for _ in range(12):
        slot = 0 if slot + 1 >= 0x0C else slot + 1
        if table[slot]:
            break
    return slot


def predecessor_table_outcomes(table: list[int]) -> list[dict]:
    rows = []
    for start in range(12):
        selected = simulate_opcode12_selected_slot(table, start)
        rows.append({
            "activeFlag": 1,
            "startSource": "prior selectionBuffer[0x20]",
            "startSlot": start,
            "selectedSlot": selected,
            "selectedValue": table[selected],
            "readerFallsThrough": table[selected] == 1,
        })
    selected = simulate_opcode12_selected_slot(table, 0)
    rows.append({
        "activeFlag": 0,
        "startSource": "forced zero",
        "startSlot": 0,
        "selectedSlot": selected,
        "selectedValue": table[selected],
        "readerFallsThrough": table[selected] == 1,
    })
    return rows


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

    table = predecessor_state_effect.get("secondaryBranchStateAfterFill") or [1, 1] + [0] * 10
    outcomes = predecessor_table_outcomes(table)
    arbitrary_state_counterexamples = [
        {
            "stateTable": [2] + [0] * 11,
            "startSlot": 0,
            "selectedSlot": simulate_opcode12_selected_slot([2] + [0] * 11, 0),
            "selectedValue": 2,
            "readerFallsThrough": False,
            "meaning": "opcode 0x12 can select a nonzero state value that is not the reader's required value 1",
        },
        {
            "stateTable": [0, 2] + [0] * 10,
            "startSlot": 1,
            "selectedSlot": simulate_opcode12_selected_slot([0, 2] + [0] * 10, 1),
            "selectedValue": 2,
            "readerFallsThrough": False,
            "meaning": "the active flag can change the search start, but it cannot convert state value 2 into pass value 1",
        },
    ]

    all_predecessor_starts_pass = all(row["readerFallsThrough"] for row in outcomes)
    conclusion = (
        "The active-selection flag evidence removes one static unknown from the 0x005428bc writer: the EXE/startup "
        "default for 0x00457744 is 1, so opcode 0x12 normally starts from the prior selectionBuffer[0x20] value. "
        "However, 0x00457744 is also save offset 0x006c and can be overwritten by a loaded save. More importantly, "
        "the prior start slot is not the decisive blocker under the strongest predecessor-fill hypothesis: if "
        "1:0 leaves secondaryBranchState as [1,1,0..], both activeFlag=1 for every possible prior slot and "
        "activeFlag=0 from zero select a passing slot. Without that predecessor/runtime table proof, opcode 0x12 "
        "still only selects a nonzero state, and state value 2 would fail the 0x00542b0c reader. Promotion therefore "
        "remains blocked on predecessor execution/state persistence, the gated control path, and a strict map1_01a hotspot."
    )
    return {
        "source": "map1_01a",
        "target": "map2_02d",
        "writerVaHex": branch_selector_equation.get("writerVaHex", "0x005428bc"),
        "readerVaHex": branch_selector_equation.get("readerVaHex", "0x00542b0c"),
        "activeFlagVaHex": active_flag_sources.get("activeFlagVaHex", "0x00457744"),
        "activeFlagStaticInitialByteHex": active_flag_sources.get("activeFlagStaticInitialByteHex"),
        "activeFlagSaveOffsetHex": (active_flag_sources.get("activeFlagSaveSource") or {}).get("saveOffsetHex"),
        "activeFlagResolvedStaticDefault": active_flag_sources.get("resolvedStaticDefault"),
        "activeFlagStartupInitVaHex": active_flag_sources.get("startupInitVaHex"),
        "activeFlagStartupInitCallCount": active_flag_sources.get("startupInitCallCount"),
        "predecessorSelector": predecessor_state_effect.get("predecessorSelector", "1:0"),
        "predecessorRootHex": predecessor_state_effect.get("predecessorRootHex", "0x00478364"),
        "predecessorFillValueHex": predecessor_state_effect.get("fillValueHex", "0x00000210"),
        "secondaryBranchStateAfterPredecessorFill": table,
        "outcomes": outcomes,
        "allPredecessorStartsPass": all_predecessor_starts_pass,
        "arbitraryStateCounterexamples": arbitrary_state_counterexamples,
        "priorSelectionBufferStillPrimaryBlockerUnderPredecessorHypothesis": False,
        "promotionStatus": "blocked",
        "remainingBlockers": [
            "prove predecessor 1:0 executes before current selector 2:0 in the normal route",
            "prove secondaryBranchState persists to 0x005428bc/0x00542b0c",
            "prove the gated control path reaches the 0x00542b0c frontier reader",
            "find strict map1_01a source coordinate or hotspot",
        ],
        "conclusion": conclusion,
    }


def markdown(summary: dict) -> str:
    lines = [
        "# Save Selector Active Flag Effect",
        "",
        f"- route: {summary['source']} -> {summary['target']}",
        f"- writer/reader: `{summary['writerVaHex']}` / `{summary['readerVaHex']}`",
        f"- active flag: `{summary['activeFlagVaHex']}` static `{summary['activeFlagStaticInitialByteHex']}` save offset `{summary['activeFlagSaveOffsetHex']}`",
        f"- startup init: `{summary['activeFlagStartupInitVaHex']}` calls {summary['activeFlagStartupInitCallCount']}",
        f"- predecessor: `{summary['predecessorSelector']}` root `{summary['predecessorRootHex']}` fill `{summary['predecessorFillValueHex']}`",
        f"- all predecessor starts pass: {summary['allPredecessorStartsPass']}",
        f"- prior selectionBuffer still primary blocker under predecessor hypothesis: {summary['priorSelectionBufferStillPrimaryBlockerUnderPredecessorHypothesis']}",
        f"- promotion status: `{summary['promotionStatus']}`",
        "",
        summary["conclusion"],
        "",
        "## Predecessor-Fill Outcomes",
        "",
        "| active flag | start source | start slot | selected slot | selected value | reader falls through |",
        "| ---: | --- | ---: | ---: | ---: | --- |",
    ]
    for row in summary["outcomes"]:
        lines.append(
            f"| {row['activeFlag']} | {row['startSource']} | {row['startSlot']} | "
            f"{row['selectedSlot']} | {row['selectedValue']} | {'yes' if row['readerFallsThrough'] else 'no'} |"
        )
    lines.extend([
        "",
        "## Counterexamples Without Predecessor Table Proof",
        "",
        "| start slot | selected slot | selected value | reader falls through | meaning |",
        "| ---: | ---: | ---: | --- | --- |",
    ])
    for row in summary["arbitraryStateCounterexamples"]:
        lines.append(
            f"| {row['startSlot']} | {row['selectedSlot']} | {row['selectedValue']} | "
            f"{'yes' if row['readerFallsThrough'] else 'no'} | {row['meaning']} |"
        )
    lines.extend(["", "## Remaining Blockers", ""])
    lines.extend(f"- {item}" for item in summary["remainingBlockers"])
    lines.append("")
    return "\n".join(lines)


def html_page(summary: dict) -> str:
    outcome_rows = "\n".join(
        "<tr>"
        f"<td>{row['activeFlag']}</td>"
        f"<td>{html.escape(row['startSource'])}</td>"
        f"<td>{row['startSlot']}</td>"
        f"<td>{row['selectedSlot']}</td>"
        f"<td>{row['selectedValue']}</td>"
        f"<td>{'yes' if row['readerFallsThrough'] else 'no'}</td>"
        "</tr>"
        for row in summary["outcomes"]
    )
    counter_rows = "\n".join(
        "<tr>"
        f"<td>{row['startSlot']}</td>"
        f"<td>{row['selectedSlot']}</td>"
        f"<td>{row['selectedValue']}</td>"
        f"<td>{'yes' if row['readerFallsThrough'] else 'no'}</td>"
        f"<td>{html.escape(row['meaning'])}</td>"
        "</tr>"
        for row in summary["arbitraryStateCounterexamples"]
    )
    blockers = "".join(f"<li>{html.escape(item)}</li>" for item in summary["remainingBlockers"])
    return "\n".join([
        "<!doctype html><meta charset=\"utf-8\"><title>Save Selector Active Flag Effect</title>",
        "<style>body{font-family:system-ui,sans-serif;background:#111;color:#eee;max-width:1120px;margin:24px auto;line-height:1.45}table{border-collapse:collapse;width:100%;margin:16px 0 28px}td,th{border:1px solid #444;padding:6px 8px;vertical-align:top}th{background:#202020}code{color:#9bd4ff}</style>",
        "<h1>Save Selector Active Flag Effect</h1>",
        f"<p>route: {html.escape(summary['source'])} -&gt; {html.escape(summary['target'])}; writer <code>{summary['writerVaHex']}</code>; reader <code>{summary['readerVaHex']}</code>.</p>",
        f"<p>active flag <code>{summary['activeFlagVaHex']}</code>; static <code>{summary['activeFlagStaticInitialByteHex']}</code>; save offset <code>{summary['activeFlagSaveOffsetHex']}</code>; startup init <code>{summary['activeFlagStartupInitVaHex']}</code>.</p>",
        f"<p>all predecessor starts pass: {summary['allPredecessorStartsPass']}; prior selectionBuffer still primary blocker under predecessor hypothesis: {summary['priorSelectionBufferStillPrimaryBlockerUnderPredecessorHypothesis']}; promotion status <code>{summary['promotionStatus']}</code>.</p>",
        f"<p>{html.escape(summary['conclusion'])}</p>",
        "<h2>Predecessor-Fill Outcomes</h2>",
        "<table><thead><tr><th>active flag</th><th>start source</th><th>start slot</th><th>selected slot</th><th>selected value</th><th>reader falls through</th></tr></thead><tbody>",
        outcome_rows,
        "</tbody></table>",
        "<h2>Counterexamples Without Predecessor Table Proof</h2>",
        "<table><thead><tr><th>start slot</th><th>selected slot</th><th>selected value</th><th>reader falls through</th><th>meaning</th></tr></thead><tbody>",
        counter_rows,
        "</tbody></table>",
        "<h2>Remaining Blockers</h2>",
        f"<ul>{blockers}</ul>",
    ])


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


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument("--out-dir", type=Path, default=OUT)
    args = parser.parse_args()
    summary = build_summary()
    write_outputs(summary, args.out_dir)
    print(f"wrote save selector active flag effect -> {args.out_dir / 'save_selector_active_flag_effect.html'}")


if __name__ == "__main__":
    main()