#!/usr/bin/env python3
"""Summarize root-relative leaf-table indices for the current selector frontier."""
from __future__ import annotations

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

sys.path.insert(0, str(Path(__file__).resolve().parent))

from probe_exe_scene_tables import read_sections, va_to_offset


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

SOURCE = "map1_01a"
TARGET = "map2_02d"
CURRENT_SELECTOR = "2:0"
CURRENT_ROOT = 0x00540714
ROOT_TABLE_POINTER = 0x005429DC
TABLE_WINDOW_START = 0x005429A8
TABLE_WINDOW_END_EXCLUSIVE = 0x00542A04
FRONTIER_LEAF = 0x00542AE8
FRONTIER_READER = 0x00542B0C
DESCRIPTOR_MARKER = 0x0000003F

EVIDENCE_REFS = [
    {
        "path": "out/save_selector_leaf_streams.json",
        "fields": [
            "leafPointerHex",
            "fieldRecords",
            "nestedFieldRecords",
        ],
    },
    {
        "path": "out/save_selector_stream_traces.json",
        "fields": [
            "streamVaHex",
            "trace",
        ],
    },
    {
        "path": "out/save_selector_opcode2c_route_pair_context.json",
        "fields": [
            "rows",
            "descriptorHex",
            "correctedTrace",
            "reachesFrontierReader",
        ],
    },
]

LEAF_INDEX_MISSING_EVIDENCE_BY_GATE = {
    "normal-runtime-selector-root-execution": (
        "normal runtime selector/root execution reaches the corrected route-pair descriptors"
    ),
    "reader-branch-target-linkage": (
        "0x00542b0c reader branch outcome and map target linkage on a real route path"
    ),
    "strict-hotspot": "strict map1_01a source coordinate or hotspot",
}


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


def hex32(value: int | None) -> str | None:
    return f"0x{value:08x}" if isinstance(value, int) else None


def parse_hex(value: str | None) -> int | None:
    return int(value, 16) if value else None


def dword_at(exe: bytes, sections: list[dict], va: int) -> int | None:
    offset = va_to_offset(sections, va)
    if offset is None or offset + 4 > len(exe):
        return None
    return struct.unpack_from("<I", exe, offset)[0]


def field_maps_for_leaf(leaf_streams: list[dict], leaf_hex: str | None) -> list[str]:
    if not leaf_hex:
        return []
    row = next((item for item in leaf_streams if item.get("leafPointerHex") == leaf_hex), None)
    if not row:
        return []
    return [record.get("map") for record in row.get("fieldRecords") or [] if record.get("map")]


def nested_maps_for_leaf(leaf_streams: list[dict], leaf_hex: str | None) -> list[str]:
    if not leaf_hex:
        return []
    row = next((item for item in leaf_streams if item.get("leafPointerHex") == leaf_hex), None)
    if not row:
        return []
    return [record.get("map") for record in row.get("nestedFieldRecords") or [] if record.get("map")]


def trace_contains(stream_traces: list[dict], stream_hex: str | None, va_hex: str) -> bool:
    if not stream_hex:
        return False
    row = next((item for item in stream_traces if item.get("streamVaHex") == stream_hex), None)
    if not row:
        return False
    return any(item.get("vaHex") == va_hex for item in row.get("trace") or [])


def route_pair(maps: list[str]) -> bool:
    return SOURCE in maps and TARGET in maps


def corrected_traces_by_descriptor(opcode2c_route_pair_context: dict | None) -> dict[str, dict]:
    if not opcode2c_route_pair_context:
        return {}
    return {
        row.get("descriptorHex"): row.get("correctedTrace") or {}
        for row in opcode2c_route_pair_context.get("rows") or []
        if row.get("descriptorHex")
    }


def entry_row(
    exe: bytes,
    sections: list[dict],
    leaf_streams: list[dict],
    stream_traces: list[dict],
    corrected_by_descriptor: dict[str, dict],
    entry_va: int,
) -> dict:
    value = dword_at(exe, sections, entry_va)
    value_hex = hex32(value)
    marker = dword_at(exe, sections, value) if isinstance(value, int) else None
    child = dword_at(exe, sections, value + 4) if marker == DESCRIPTOR_MARKER and isinstance(value, int) else None
    child_hex = hex32(child)
    descriptor_maps = field_maps_for_leaf(leaf_streams, value_hex)
    nested_maps = nested_maps_for_leaf(leaf_streams, value_hex)
    child_maps = field_maps_for_leaf(leaf_streams, child_hex)
    descriptor_reader = trace_contains(stream_traces, value_hex, hex32(FRONTIER_READER) or "")
    child_reader = trace_contains(stream_traces, child_hex, hex32(FRONTIER_READER) or "")
    corrected_descriptor_trace = corrected_by_descriptor.get(value_hex) or {}
    corrected_descriptor_reader = corrected_descriptor_trace.get("reachesFrontierReader") is True
    return {
        "entryVa": entry_va,
        "entryVaHex": hex32(entry_va),
        "rootRelativeIndex": (entry_va - ROOT_TABLE_POINTER) // 4,
        "insideCurrentRootEntryRun": entry_va >= ROOT_TABLE_POINTER,
        "descriptorHex": value_hex,
        "descriptorMarkerHex": hex32(marker),
        "descriptorIsMarkerShape": marker == DESCRIPTOR_MARKER,
        "childPointerHex": child_hex,
        "descriptorFieldMaps": descriptor_maps,
        "descriptorNestedFieldMaps": nested_maps,
        "childFieldMaps": child_maps,
        "descriptorHasRoutePair": route_pair(descriptor_maps),
        "childHasRoutePair": route_pair(child_maps),
        "descriptorTraceContainsFrontierReader": descriptor_reader,
        "childTraceContainsFrontierReader": child_reader,
        "correctedDescriptorTraceContainsFrontierReader": corrected_descriptor_reader,
        "correctedDescriptorFrontierReaderStep": corrected_descriptor_trace.get("frontierReaderStep"),
        "effectiveDescriptorTraceContainsFrontierReader": descriptor_reader or corrected_descriptor_reader,
        "isFrontierLeafChild": child == FRONTIER_LEAF,
        "isFrontierLeafDescriptor": value == FRONTIER_LEAF,
        "routeRelevant": (
            route_pair(descriptor_maps)
            or route_pair(child_maps)
            or descriptor_reader
            or child_reader
            or corrected_descriptor_reader
        ),
    }


def build_summary(
    exe: bytes,
    leaf_streams: list[dict],
    stream_traces: list[dict],
    opcode2c_route_pair_context: dict | None = None,
) -> dict:
    sections = read_sections(exe)
    corrected_by_descriptor = corrected_traces_by_descriptor(opcode2c_route_pair_context)
    rows = [
        entry_row(exe, sections, leaf_streams, stream_traces, corrected_by_descriptor, va)
        for va in range(TABLE_WINDOW_START, TABLE_WINDOW_END_EXCLUSIVE, 4)
    ]
    current_rows = [row for row in rows if row["insideCurrentRootEntryRun"]]
    negative_rows = [row for row in rows if not row["insideCurrentRootEntryRun"]]
    route_descriptor_rows = [row for row in current_rows if row.get("descriptorHasRoutePair")]
    reader_child_rows = [row for row in rows if row.get("childTraceContainsFrontierReader") or row.get("descriptorTraceContainsFrontierReader")]
    current_reader_rows = [row for row in current_rows if row in reader_child_rows]
    negative_reader_rows = [row for row in negative_rows if row in reader_child_rows]
    corrected_current_reader_rows = [
        row
        for row in current_rows
        if row.get("correctedDescriptorTraceContainsFrontierReader")
    ]
    corrected_route_pair_reader_rows = [
        row
        for row in route_descriptor_rows
        if row.get("correctedDescriptorTraceContainsFrontierReader")
    ]
    frontier_child_rows = [row for row in rows if row.get("isFrontierLeafChild") or row.get("isFrontierLeafDescriptor")]
    runtime_selection_proven = False
    strict_hotspot_found = False
    failed_leaf_index_gate_ids = []
    if not runtime_selection_proven:
        failed_leaf_index_gate_ids.append("normal-runtime-selector-root-execution")
    if not current_reader_rows:
        failed_leaf_index_gate_ids.append("reader-branch-target-linkage")
    if not strict_hotspot_found:
        failed_leaf_index_gate_ids.append("strict-hotspot")
    missing_evidence = [
        LEAF_INDEX_MISSING_EVIDENCE_BY_GATE.get(gate_id, gate_id)
        for gate_id in failed_leaf_index_gate_ids
    ]
    conclusion = (
        f"The current selector {CURRENT_SELECTOR} table pointer is {hex32(ROOT_TABLE_POINTER)}. "
        "The raw generic stream trace still finds the direct frontier leaf reference only as the descriptor "
        "child at root-relative index -12, before that table pointer. However, the opcode 0x2c correction "
        "shows the non-negative current-root route-pair descriptors at indices 6 and 8 can also reach the "
        "frontier reader 0x00542b0c. That resolves the stale no-fixed-advance trace contradiction, but it is "
        "still descriptor/control-flow evidence only; normal runtime selector execution, reader branch "
        "outcome, and a strict map1_01a hotspot remain unproven."
    )
    return {
        "source": SOURCE,
        "target": TARGET,
        "selector": CURRENT_SELECTOR,
        "rootHex": hex32(CURRENT_ROOT),
        "rootTablePointerHex": hex32(ROOT_TABLE_POINTER),
        "tableWindowHex": f"{hex32(TABLE_WINDOW_START)}..{hex32(TABLE_WINDOW_END_EXCLUSIVE - 4)}",
        "frontierLeafHex": hex32(FRONTIER_LEAF),
        "frontierReaderHex": hex32(FRONTIER_READER),
        "evidenceRefs": EVIDENCE_REFS,
        "evidenceRefCount": len(EVIDENCE_REFS),
        "entryCount": len(rows),
        "negativeIndexCount": len(negative_rows),
        "currentRootEntryCount": len(current_rows),
        "routePairDescriptorCurrentEntryCount": len(route_descriptor_rows),
        "readerBearingCurrentEntryCount": len(current_reader_rows),
        "readerBearingNegativeEntryCount": len(negative_reader_rows),
        "opcode2cCorrectionApplied": bool(corrected_by_descriptor),
        "correctedReaderBearingCurrentEntryCount": len(corrected_current_reader_rows),
        "correctedRoutePairTraceReachesReaderCount": len(corrected_route_pair_reader_rows),
        "correctedTraceAllRoutePairDescriptorsReachReader": bool(route_descriptor_rows)
        and len(corrected_route_pair_reader_rows) == len(route_descriptor_rows),
        "frontierLeafChildEntryIndices": [row["rootRelativeIndex"] for row in frontier_child_rows],
        "frontierLeafChildOnlyNegativeIndex": bool(frontier_child_rows)
        and all(row["rootRelativeIndex"] < 0 for row in frontier_child_rows),
        "frontierReaderSelectableByNonNegativeIndex": bool(current_reader_rows),
        "frontierReaderReachableByCorrectedNonNegativeIndex": bool(corrected_current_reader_rows),
        "routePairCurrentDescriptorIndices": [row["rootRelativeIndex"] for row in route_descriptor_rows],
        "routePairCorrectedTraceDescriptorIndices": [
            row["rootRelativeIndex"] for row in corrected_route_pair_reader_rows
        ],
        "readerBearingNegativeIndices": [row["rootRelativeIndex"] for row in negative_reader_rows],
        "rows": rows,
        "routeRelevantRows": [row for row in rows if row.get("routeRelevant")],
        "runtimeSelectionProven": runtime_selection_proven,
        "proofFound": runtime_selection_proven,
        "failedLeafIndexGateIds": failed_leaf_index_gate_ids,
        "missingEvidence": missing_evidence,
        "strictHotspotFound": strict_hotspot_found,
        "promotionStatus": "blocked",
        "remainingProofs": [
            "prove normal runtime selector/root execution reaches the corrected route-pair descriptors",
            "resolve the 0x00542b0c reader branch outcome and map target linkage on a real route path",
            "or find a strict map1_01a source coordinate/hotspot",
        ],
        "conclusion": conclusion,
    }


def markdown(summary: dict) -> str:
    lines = [
        "# Save Selector Leaf Index Space",
        "",
        f"- route: `{summary['source']} -> {summary['target']}`",
        f"- selector: `{summary['selector']}` root `{summary['rootHex']}`",
        f"- root table pointer: `{summary['rootTablePointerHex']}`",
        f"- table window: `{summary['tableWindowHex']}`",
        f"- frontier leaf: `{summary['frontierLeafHex']}`",
        f"- frontier reader: `{summary['frontierReaderHex']}`",
        f"- entries: {summary['entryCount']}",
        f"- negative-index entries: {summary['negativeIndexCount']}",
        f"- current-root entries: {summary['currentRootEntryCount']}",
        f"- current route-pair descriptor entries: {summary['routePairDescriptorCurrentEntryCount']}",
        f"- current reader-bearing entries: {summary['readerBearingCurrentEntryCount']}",
        f"- negative reader-bearing entries: {summary['readerBearingNegativeEntryCount']}",
        f"- opcode 0x2c correction applied: {summary['opcode2cCorrectionApplied']}",
        f"- corrected current reader-bearing entries: {summary['correctedReaderBearingCurrentEntryCount']}",
        f"- corrected route-pair traces reaching reader: {summary['correctedRoutePairTraceReachesReaderCount']}",
        f"- frontier leaf child entry indices: {summary['frontierLeafChildEntryIndices']}",
        f"- frontier reader selectable by non-negative index: {summary['frontierReaderSelectableByNonNegativeIndex']}",
        f"- frontier reader reachable by corrected non-negative index: {summary['frontierReaderReachableByCorrectedNonNegativeIndex']}",
        f"- proof found: {summary['proofFound']}",
        f"- failed leaf-index gates: `{', '.join(summary.get('failedLeafIndexGateIds') or []) or '-'}`",
        f"- missing evidence count: {len(summary.get('missingEvidence') or [])}",
        f"- promotion status: `{summary['promotionStatus']}`",
        f"- evidence refs: `{summary['evidenceRefCount']}`",
        "",
        summary["conclusion"],
        "",
    ]
    lines.extend(["## Missing Evidence", ""])
    lines.extend(f"- {item}" for item in summary.get("missingEvidence") or [])
    lines.extend(["", "## Evidence Refs", ""])
    for ref in summary.get("evidenceRefs") or []:
        lines.append(
            f"- `{ref.get('path')}`: {', '.join(ref.get('fields') or [])}"
        )
    lines.extend([
        "",
        "## Route-Relevant Entries",
        "",
        "| index | entry | descriptor | child | current entry | desc maps | nested maps | child maps | raw desc reader | corrected desc reader | child reader |",
        "| ---: | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |",
    ])
    for row in summary["routeRelevantRows"]:
        lines.append(
            f"| {row['rootRelativeIndex']} | `{row['entryVaHex']}` | `{row.get('descriptorHex')}` | "
            f"`{row.get('childPointerHex') or '-'}` | {row['insideCurrentRootEntryRun']} | "
            f"{', '.join(row.get('descriptorFieldMaps') or []) or '-'} | "
            f"{', '.join(row.get('descriptorNestedFieldMaps') or []) or '-'} | "
            f"{', '.join(row.get('childFieldMaps') or []) or '-'} | "
            f"{row.get('descriptorTraceContainsFrontierReader')} | "
            f"{row.get('correctedDescriptorTraceContainsFrontierReader')} | "
            f"{row.get('childTraceContainsFrontierReader')} |"
        )
    lines.extend([
        "",
        "## All Entries",
        "",
        "| index | entry | descriptor | child | current entry | marker | route relevant |",
        "| ---: | --- | --- | --- | --- | --- | --- |",
    ])
    for row in summary["rows"]:
        lines.append(
            f"| {row['rootRelativeIndex']} | `{row['entryVaHex']}` | `{row.get('descriptorHex')}` | "
            f"`{row.get('childPointerHex') or '-'}` | {row['insideCurrentRootEntryRun']} | "
            f"`{row.get('descriptorMarkerHex') or '-'}` | {row.get('routeRelevant')} |"
        )
    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_refs = "".join(
        "<li>"
        f"<code>{html.escape(str(ref.get('path')))}</code>: "
        f"{html.escape(', '.join(ref.get('fields') or []))}"
        "</li>"
        for ref in summary.get("evidenceRefs") or []
    )

    def relevant_rows() -> str:
        return "\n".join(
            "<tr>"
            f"<td>{row['rootRelativeIndex']}</td>"
            f"<td><code>{html.escape(str(row['entryVaHex']))}</code></td>"
            f"<td><code>{html.escape(str(row.get('descriptorHex')))}</code></td>"
            f"<td><code>{html.escape(str(row.get('childPointerHex') or '-'))}</code></td>"
            f"<td>{row['insideCurrentRootEntryRun']}</td>"
            f"<td>{html.escape(', '.join(row.get('descriptorFieldMaps') or []) or '-')}</td>"
            f"<td>{html.escape(', '.join(row.get('descriptorNestedFieldMaps') or []) or '-')}</td>"
            f"<td>{html.escape(', '.join(row.get('childFieldMaps') or []) or '-')}</td>"
            f"<td>{row.get('descriptorTraceContainsFrontierReader')}</td>"
            f"<td>{row.get('correctedDescriptorTraceContainsFrontierReader')}</td>"
            f"<td>{row.get('childTraceContainsFrontierReader')}</td>"
            "</tr>"
            for row in summary["routeRelevantRows"]
        )

    def all_rows() -> str:
        return "\n".join(
            "<tr>"
            f"<td>{row['rootRelativeIndex']}</td>"
            f"<td><code>{html.escape(str(row['entryVaHex']))}</code></td>"
            f"<td><code>{html.escape(str(row.get('descriptorHex')))}</code></td>"
            f"<td><code>{html.escape(str(row.get('childPointerHex') or '-'))}</code></td>"
            f"<td>{row['insideCurrentRootEntryRun']}</td>"
            f"<td><code>{html.escape(str(row.get('descriptorMarkerHex') or '-'))}</code></td>"
            f"<td>{row.get('routeRelevant')}</td>"
            "</tr>"
            for row in summary["rows"]
        )

    proofs = "".join(f"<li>{html.escape(item)}</li>" for item in summary["remainingProofs"])
    missing_items = "".join(
        f"<li>{html.escape(item)}</li>" for item in summary.get("missingEvidence") or []
    )
    return "\n".join([
        "<!doctype html>",
        '<html lang="en">',
        "<head>",
        '  <meta charset="utf-8">',
        '  <meta name="viewport" content="width=device-width, initial-scale=1">',
        "  <title>Save Selector Leaf Index Space</title>",
        "  <style>body{font-family:system-ui,sans-serif;background:#111;color:#eee;margin:24px}table{border-collapse:collapse;width:100%;max-width:1280px}td,th{border:1px solid #333;padding:6px 8px;text-align:left;vertical-align:top}th{background:#1f1f1f}code{color:#9bd4ff}</style>",
        "</head>",
        "<body>",
        "  <h1>Save Selector Leaf Index Space</h1>",
        f"  <p>route <code>{summary['source']} -&gt; {summary['target']}</code>; selector <code>{summary['selector']}</code>; root table pointer <code>{summary['rootTablePointerHex']}</code>; current route-pair descriptor entries {summary['routePairDescriptorCurrentEntryCount']}; current reader-bearing entries {summary['readerBearingCurrentEntryCount']}; negative reader-bearing entries {summary['readerBearingNegativeEntryCount']}; opcode 0x2c correction applied {summary['opcode2cCorrectionApplied']}; corrected route-pair traces reaching reader {summary['correctedRoutePairTraceReachesReaderCount']}; frontier reader selectable by non-negative index {summary['frontierReaderSelectableByNonNegativeIndex']}; frontier reader reachable by corrected non-negative index {summary['frontierReaderReachableByCorrectedNonNegativeIndex']}; proofFound={summary['proofFound']}; failedLeafIndexGates=<code>{html.escape(','.join(summary.get('failedLeafIndexGateIds') or []) or '-')}</code>; missingEvidenceCount={len(summary.get('missingEvidence') or [])}; promotion <code>{summary['promotionStatus']}</code>.</p>",
        f"  <p>{html.escape(summary['conclusion'])}</p>",
        f"  <p><b>Evidence refs:</b> {summary['evidenceRefCount']}.</p>",
        f"  <h2>Missing Evidence</h2><ul>{missing_items}</ul>",
        f"  <h2>Evidence Refs</h2><ul>{evidence_refs}</ul>",
        "  <h2>Route-Relevant Entries</h2>",
        "  <table><thead><tr><th>index</th><th>entry</th><th>descriptor</th><th>child</th><th>current entry</th><th>desc maps</th><th>nested maps</th><th>child maps</th><th>raw desc reader</th><th>corrected desc reader</th><th>child reader</th></tr></thead><tbody>",
        relevant_rows(),
        "  </tbody></table>",
        "  <h2>All Entries</h2>",
        "  <table><thead><tr><th>index</th><th>entry</th><th>descriptor</th><th>child</th><th>current entry</th><th>marker</th><th>route relevant</th></tr></thead><tbody>",
        all_rows(),
        "  </tbody></table>",
        "  <h2>Remaining Proofs</h2>",
        f"  <ul>{proofs}</ul>",
        "</body>",
        "</html>",
        "",
    ])


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


def main() -> None:
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--exe", type=Path, default=ROOT / "Hwanse2.exe")
    parser.add_argument("--out-dir", type=Path, default=OUT)
    args = parser.parse_args()
    summary = build_summary(
        args.exe.read_bytes(),
        load_json(args.out_dir / "save_selector_leaf_streams.json", []),
        load_json(args.out_dir / "save_selector_stream_traces.json", []),
        load_json(args.out_dir / "save_selector_opcode2c_route_pair_context.json", {}),
    )
    write_outputs(summary, args.out_dir)
    print(f"wrote save selector leaf index space -> {args.out_dir / 'save_selector_leaf_index_space.html'}")


if __name__ == "__main__":
    main()