#!/usr/bin/env python3
"""Summarize the remaining global-reset proof gap for secondaryBranchState."""
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"
SOURCE = "map1_01a"
TARGET = "map2_02d"


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


def selector_for_root(root: dict) -> str | None:
    group = root.get("group")
    slot = root.get("slot")
    if group is None or slot is None:
        return None
    return f"{group}:{slot}"


def find_root_by_selector(fill_roots: dict, selector: str) -> dict:
    for row in fill_roots.get("routeOverlapRoots") or []:
        if selector_for_root(row) == selector:
            return row
    for row in fill_roots.get("roots") or []:
        if selector_for_root(row) == selector:
            return row
    return {}


def compact_fill_rows(rows: list[dict]) -> list[dict]:
    return [
        {
            "vaHex": row.get("vaHex"),
            "valueHex": row.get("valueHex"),
            "helperArgumentHex": row.get("helperArgumentHex"),
            "beforeCurrentFrontierReader": row.get("beforeCurrentFrontierReader"),
            "afterCurrentFrontierReader": row.get("afterCurrentFrontierReader"),
            "routeRelevance": row.get("routeRelevance"),
        }
        for row in rows
    ]


def proof_row(area: str, status: str, evidence: str, consequence: str) -> dict:
    return {
        "area": area,
        "status": status,
        "evidence": evidence,
        "consequence": consequence,
    }


def build_summary(
    reset_scope: dict,
    secondary_sources: dict,
    predecessor_tail_reset: dict,
    persistence_gap: dict,
    secondary_fill_roots: dict,
    secondary_route_overlap_candidates: dict | None = None,
    secondary_block_writes: dict | None = None,
) -> dict:
    secondary = reset_scope.get("secondaryBranchState") or {}
    helper = reset_scope.get("helper") or {}
    route_scope = reset_scope.get("routeScope") or {}
    predecessor_selector = persistence_gap.get("predecessorSelector") or "1:0"
    current_selector = persistence_gap.get("currentSelector") or "2:0"
    predecessor_root = find_root_by_selector(secondary_fill_roots, predecessor_selector)
    current_root = find_root_by_selector(secondary_fill_roots, current_selector)
    predecessor_fills = compact_fill_rows(predecessor_root.get("fills") or [])
    current_fills = compact_fill_rows(current_root.get("fills") or [])
    after_frontier_rows = compact_fill_rows(secondary_sources.get("validAfterFrontier") or [])

    direct_writer_count = secondary.get("directIndexedWriterCount", 0)
    unresolved_ref_count = secondary.get("unresolvedRefCount", 0)
    helper_only_opcode10 = helper.get("onlyDirectCallInsideOpcode10Handler") is True
    current_before_count = route_scope.get(
        "currentRootValidBeforeFrontierFillCount",
        secondary_sources.get("validBeforeFrontierCount", 0),
    )
    current_after_count = route_scope.get(
        "currentRootValidAfterFrontierFillCount",
        secondary_sources.get("validAfterFrontierCount", 0),
    )
    tail_valid_count = route_scope.get(
        "predecessorTailValidSecondaryFillCount",
        predecessor_tail_reset.get("tailValidSecondaryFillCount", 0),
    )
    local_tail_reset_found = route_scope.get(
        "predecessorLocalTailResetFound",
        predecessor_tail_reset.get("localTailResetFound"),
    )
    no_direct_global_writer = reset_scope.get("noDirectGlobalSecondaryWriter") is True
    no_known_pre_frontier_reset = reset_scope.get("noKnownPreFrontierResetInScopedEvidence") is True
    closed_static_scope = (
        no_direct_global_writer
        and unresolved_ref_count == 0
        and helper_only_opcode10
        and current_before_count == 0
        and tail_valid_count == 0
        and local_tail_reset_found is False
    )
    block_write_touch_count = (secondary_block_writes or {}).get("touchBlockWriteCandidateCount", 0)
    block_write_full_cover_count = (secondary_block_writes or {}).get("fullCoverBlockWriteCandidateCount", 0)
    block_write_direct_overlap_count = (secondary_block_writes or {}).get("directOverlapWriteCount", 0)
    block_write_shape_closed = (
        bool(secondary_block_writes)
        and block_write_touch_count == 0
        and block_write_full_cover_count == 0
        and block_write_direct_overlap_count == 0
    )
    route_order_proven = persistence_gap.get("routeOrderProven") is True
    persistence_proven = persistence_gap.get("persistenceProven") is True
    strict_hotspot_found = persistence_gap.get("strictHotspotFound") is True
    selector_adjacent = persistence_gap.get("selectorAdjacent") is True
    intermediate_selector_count = persistence_gap.get("intermediateSelectorCount")
    current_no_known_overwrite = (
        persistence_gap.get("currentRootHasNoKnownBeforeFrontierOverwrite") is True
    )
    selector_order_reset_gap_closed = (
        closed_static_scope
        and selector_adjacent
        and intermediate_selector_count == 0
        and current_no_known_overwrite
    )
    open_runtime_gap = not (route_order_proven and persistence_proven and strict_hotspot_found)
    static_reset_shape_ruled_out = (
        closed_static_scope
        and block_write_shape_closed
        and selector_order_reset_gap_closed
    )
    runtime_reset_risk_class = (
        "runtime-order-or-untraced-bytecode-path"
        if open_runtime_gap or not static_reset_shape_ruled_out
        else "closed"
    )
    candidate_class = (
        "static-scope-closed-runtime-order-open"
        if closed_static_scope
        else "static-reset-scope-open"
    )
    proof_rows = [
        proof_row(
            "direct secondary table writes",
            "closed" if direct_writer_count == 0 and unresolved_ref_count == 0 else "open",
            f"directIndexedWriterCount={direct_writer_count}; unresolvedRefCount={unresolved_ref_count}",
            "No direct table writer remains in the scanned .text references.",
        ),
        proof_row(
            "helper entry scope",
            "closed" if helper_only_opcode10 else "open",
            (
                f"helper={helper.get('helperVaHex')}; directCallCount={helper.get('directCallCount')}; "
                f"onlyOpcode10={helper_only_opcode10}"
            ),
            "Secondary changes are still modeled as opcode 0x10 helper rows.",
        ),
        proof_row(
            "broad block write shape",
            "closed" if block_write_shape_closed else "open",
            (
                f"scanRange={(secondary_block_writes or {}).get('scanRangeHex')}; "
                f"addressLike={(secondary_block_writes or {}).get('addressLikeTouchingBaseCount')}; "
                f"directOverlap={block_write_direct_overlap_count}; "
                f"touchBlock={block_write_touch_count}; fullCoverBlock={block_write_full_cover_count}"
            ),
            "No obvious memset/memcpy-style secondaryBranchState reset remains in the current static scan.",
        ),
        proof_row(
            "current root before frontier",
            "closed" if current_before_count == 0 else "open",
            f"root={secondary_sources.get('rootRangeHex')}; beforeFrontierValidFills={current_before_count}",
            "The current selector has no valid secondary fill before the 0x00542b0c reader.",
        ),
        proof_row(
            "current root after frontier",
            "post-frontier-only" if current_after_count else "none",
            (
                f"afterFrontierValidFills={current_after_count}; "
                f"fillVas={','.join(row.get('vaHex') or '-' for row in after_frontier_rows or current_fills) or '-'}"
            ),
            "Post-frontier fills cannot initialize the earlier blocker branch.",
        ),
        proof_row(
            "predecessor local tail",
            "closed" if tail_valid_count == 0 and local_tail_reset_found is False else "open",
            (
                f"tailRange={predecessor_tail_reset.get('tailRangeHex')}; "
                f"tailValidSecondaryFills={tail_valid_count}; localTailResetFound={local_tail_reset_found}"
            ),
            "The known predecessor 1:0 tail does not locally clear the secondary fill.",
        ),
        proof_row(
            "selector-order reset window",
            "closed" if selector_order_reset_gap_closed else "open",
            (
                f"selectorAdjacent={selector_adjacent}; intermediateSelectors={intermediate_selector_count}; "
                f"currentNoKnownOverwrite={current_no_known_overwrite}; closedStaticResetScope={closed_static_scope}"
            ),
            "Within the selector-table adjacency model, no reset-capable selector/root remains between 1:0 and the current reader.",
        ),
        proof_row(
            "static reset shape",
            "closed" if static_reset_shape_ruled_out else "open",
            (
                f"closedStaticResetScope={closed_static_scope}; "
                f"blockWriteShapeClosed={block_write_shape_closed}; "
                f"selectorOrderResetGapClosed={selector_order_reset_gap_closed}"
            ),
            "The remaining secondary reset uncertainty is not an obvious static writer or block reset shape.",
        ),
        proof_row(
            "runtime order and global reset",
            "open" if open_runtime_gap or reset_scope.get("globalResetRuledOut") is not True else "closed",
            (
                f"routeOrderProven={persistence_gap.get('routeOrderProven')}; "
                f"persistenceProven={persistence_gap.get('persistenceProven')}; "
                f"globalResetRuledOut={reset_scope.get('globalResetRuledOut')}; "
                f"runtimeResetRiskClass={runtime_reset_risk_class}"
            ),
            "The remaining reset risk is dynamic execution order or an untraced VM bytecode path.",
        ),
        proof_row(
            "strict source hotspot",
            "open" if not strict_hotspot_found else "closed",
            f"strictHotspotFound={persistence_gap.get('strictHotspotFound')}",
            "A strict map1_01a source trigger is still required before route promotion.",
        ),
    ]
    remaining = [
        "prove selector 1:0 executes before selector 2:0 in the normal runtime path",
        "prove the selector-order model corresponds to the real VM execution path before the current reader, not an untraced opcode 0x10/helper path",
        "find strict map1_01a source coordinate or hotspot",
    ]
    conclusion = (
        "Static secondaryBranchState reset evidence is narrowed: no direct global writer was found, helper "
        "0x00410c90 is only reached through opcode 0x10, the broad block-write scan found no overlapping "
        "memset/memcpy-style reset candidate, the current root has no valid before-frontier fill, and the "
        "predecessor tail has no local reset. The selector-order reset window between adjacent selectors "
        "1:0 and 2:0 is also closed by the current static evidence. The proof still remains blocked because "
        "selector-table adjacency is not runtime execution order, the VM path before the reader is not captured, "
        "and the strict map1_01a source hotspot is not proven."
    )
    return {
        "source": SOURCE,
        "target": TARGET,
        "secondaryRangeHex": secondary.get("rangeHex"),
        "globalResetCandidateClass": candidate_class,
        "directGlobalSecondaryWriterCount": direct_writer_count,
        "unresolvedGlobalSecondaryRefCount": unresolved_ref_count,
        "helperVaHex": helper.get("helperVaHex"),
        "helperDirectCallCount": helper.get("directCallCount"),
        "helperOnlyCalledInsideOpcode10Handler": helper_only_opcode10,
        "secondaryBlockWriteScanRangeHex": (secondary_block_writes or {}).get("scanRangeHex"),
        "secondaryBlockAddressLikeTouchingBaseCount": (secondary_block_writes or {}).get("addressLikeTouchingBaseCount"),
        "secondaryBlockDirectOverlapWriteCount": block_write_direct_overlap_count,
        "secondaryTouchBlockWriteCandidateCount": block_write_touch_count,
        "secondaryFullCoverBlockWriteCandidateCount": block_write_full_cover_count,
        "secondaryBlockWriteShapeClosed": block_write_shape_closed,
        "currentSelector": current_selector,
        "currentRootHex": persistence_gap.get("currentRootHex") or route_scope.get("currentRootHex"),
        "currentRootRangeHex": secondary_sources.get("rootRangeHex"),
        "frontierReaderHex": secondary_sources.get("frontierReaderHex") or route_scope.get("frontierReaderHex"),
        "currentRootValidBeforeFrontierFillCount": current_before_count,
        "currentRootValidAfterFrontierFillCount": current_after_count,
        "currentRootAfterFrontierFillVas": [
            row.get("vaHex") for row in after_frontier_rows or current_fills if row.get("vaHex")
        ],
        "predecessorSelector": predecessor_selector,
        "predecessorRootHex": persistence_gap.get("predecessorRootHex") or predecessor_tail_reset.get("predecessorRootHex"),
        "predecessorRootRangeHex": predecessor_root.get("rootRangeHex") or predecessor_tail_reset.get("predecessorRootRangeHex"),
        "predecessorFillCount": predecessor_root.get("fillCount"),
        "predecessorFillVas": [row.get("vaHex") for row in predecessor_fills if row.get("vaHex")],
        "predecessorTailRangeHex": predecessor_tail_reset.get("tailRangeHex"),
        "predecessorTailValidSecondaryFillCount": tail_valid_count,
        "predecessorLocalTailResetFound": local_tail_reset_found,
        "predecessorFillWouldPassCurrentReader": persistence_gap.get("predecessorFillWouldPassCurrentReader"),
        "currentRootHasNoKnownBeforeFrontierOverwrite": persistence_gap.get("currentRootHasNoKnownBeforeFrontierOverwrite"),
        "selectorAdjacent": persistence_gap.get("selectorAdjacent"),
        "intermediateSelectorCount": intermediate_selector_count,
        "selectorOrderResetGapClosed": selector_order_reset_gap_closed,
        "routeOrderProven": persistence_gap.get("routeOrderProven"),
        "persistenceProven": persistence_gap.get("persistenceProven"),
        "strictHotspotFound": persistence_gap.get("strictHotspotFound"),
        "selectorMergeGapOpen": persistence_gap.get("selectorMergeGapOpen"),
        "secondaryRouteOverlapPromotionStatus": (secondary_route_overlap_candidates or {}).get("promotionStatus"),
        "noDirectGlobalSecondaryWriter": no_direct_global_writer,
        "noKnownPreFrontierResetInScopedEvidence": no_known_pre_frontier_reset,
        "closedStaticResetScope": closed_static_scope,
        "staticResetShapeRuledOut": static_reset_shape_ruled_out,
        "openRuntimeOrderOrBytecodeGap": open_runtime_gap,
        "runtimeResetRiskClass": runtime_reset_risk_class,
        "globalResetRuledOut": reset_scope.get("globalResetRuledOut"),
        "promotionStatus": "blocked",
        "proofRows": proof_rows,
        "remainingProofs": remaining,
        "conclusion": conclusion,
    }


def markdown(summary: dict) -> str:
    lines = [
        "# Save Selector Secondary Global Reset Gap",
        "",
        f"- route: `{summary['source']} -> {summary['target']}`",
        f"- secondaryBranchState: `{summary.get('secondaryRangeHex')}`",
        f"- candidate class: `{summary.get('globalResetCandidateClass')}`",
        f"- direct global secondary writers: {summary.get('directGlobalSecondaryWriterCount')}",
        f"- unresolved global secondary refs: {summary.get('unresolvedGlobalSecondaryRefCount')}",
        f"- helper only called inside opcode 0x10 handler: {summary.get('helperOnlyCalledInsideOpcode10Handler')}",
        f"- secondary block-write scan range: `{summary.get('secondaryBlockWriteScanRangeHex')}`",
        f"- secondary block address-like bases: {summary.get('secondaryBlockAddressLikeTouchingBaseCount')}",
        f"- secondary direct overlap writes: {summary.get('secondaryBlockDirectOverlapWriteCount')}",
        f"- secondary touch block candidates: {summary.get('secondaryTouchBlockWriteCandidateCount')}",
        f"- secondary full-cover block candidates: {summary.get('secondaryFullCoverBlockWriteCandidateCount')}",
        f"- secondary block-write shape closed: {summary.get('secondaryBlockWriteShapeClosed')}",
        f"- current before-frontier valid fills: {summary.get('currentRootValidBeforeFrontierFillCount')}",
        f"- current after-frontier valid fills: {summary.get('currentRootValidAfterFrontierFillCount')} ({', '.join(summary.get('currentRootAfterFrontierFillVas') or []) or '-'})",
        f"- predecessor fills: {summary.get('predecessorFillCount')} ({', '.join(summary.get('predecessorFillVas') or []) or '-'})",
        f"- predecessor tail valid secondary fills: {summary.get('predecessorTailValidSecondaryFillCount')}",
        f"- closed static reset scope: {summary.get('closedStaticResetScope')}",
        f"- static reset shape ruled out: {summary.get('staticResetShapeRuledOut')}",
        f"- selector-order reset gap closed: {summary.get('selectorOrderResetGapClosed')}",
        f"- runtime reset risk class: `{summary.get('runtimeResetRiskClass')}`",
        f"- global reset ruled out: {summary.get('globalResetRuledOut')}",
        f"- promotion status: {summary.get('promotionStatus')}",
        "",
        summary.get("conclusion") or "",
        "",
        "## Proof Rows",
        "",
        "| area | status | evidence | consequence |",
        "| --- | --- | --- | --- |",
    ]
    for row in summary.get("proofRows") or []:
        lines.append(
            f"| {row.get('area')} | {row.get('status')} | {row.get('evidence')} | {row.get('consequence')} |"
        )
    lines.extend(["", "## Remaining Proofs", ""])
    lines.extend(f"- {item}" for item in summary.get("remainingProofs") or [])
    lines.append("")
    return "\n".join(lines)


def html_page(summary: dict) -> str:
    rows = "\n".join(
        "<tr>"
        f"<td>{html.escape(row.get('area') or '')}</td>"
        f"<td>{html.escape(row.get('status') or '')}</td>"
        f"<td>{html.escape(row.get('evidence') or '')}</td>"
        f"<td>{html.escape(row.get('consequence') or '')}</td>"
        "</tr>"
        for row in summary.get("proofRows") or []
    )
    proofs = "".join(f"<li>{html.escape(item)}</li>" for item in summary.get("remainingProofs") or [])
    after = ", ".join(summary.get("currentRootAfterFrontierFillVas") or []) or "-"
    predecessor = ", ".join(summary.get("predecessorFillVas") or []) or "-"
    return "\n".join([
        "<!doctype html><meta charset=\"utf-8\"><title>Save Selector Secondary Global Reset Gap</title>",
        "<style>body{font-family:system-ui,sans-serif;background:#111;color:#eee;max-width:1120px;margin:24px auto}table{border-collapse:collapse;width:100%;margin:18px 0}td,th{border:1px solid #444;padding:6px 8px;vertical-align:top}code{color:#9bd4ff}</style>",
        "<h1>Save Selector Secondary Global Reset Gap</h1>",
        f"<p>Route <code>{html.escape(summary['source'])} -&gt; {html.escape(summary['target'])}</code>; secondaryBranchState <code>{html.escape(summary.get('secondaryRangeHex') or '')}</code>; class <code>{html.escape(summary.get('globalResetCandidateClass') or '')}</code>.</p>",
        f"<p>direct global secondary writers: {summary.get('directGlobalSecondaryWriterCount')}; unresolved global secondary refs: {summary.get('unresolvedGlobalSecondaryRefCount')}; helper only called inside opcode 0x10 handler: {summary.get('helperOnlyCalledInsideOpcode10Handler')}; current before-frontier valid fills: {summary.get('currentRootValidBeforeFrontierFillCount')}; current after-frontier valid fills: {summary.get('currentRootValidAfterFrontierFillCount')} ({html.escape(after)}); predecessor fills: {summary.get('predecessorFillCount')} ({html.escape(predecessor)}); predecessor tail valid secondary fills: {summary.get('predecessorTailValidSecondaryFillCount')}.</p>",
        f"<p>secondary block-write scan range: <code>{html.escape(str(summary.get('secondaryBlockWriteScanRangeHex')))}</code>; address-like bases: {summary.get('secondaryBlockAddressLikeTouchingBaseCount')}; direct overlap writes: {summary.get('secondaryBlockDirectOverlapWriteCount')}; touch block candidates: {summary.get('secondaryTouchBlockWriteCandidateCount')}; full-cover block candidates: {summary.get('secondaryFullCoverBlockWriteCandidateCount')}; secondary block-write shape closed: {summary.get('secondaryBlockWriteShapeClosed')}.</p>",
        f"<p>closed static reset scope: {summary.get('closedStaticResetScope')}; static reset shape ruled out: {summary.get('staticResetShapeRuledOut')}; selector-order reset gap closed: {summary.get('selectorOrderResetGapClosed')}; runtime reset risk class: <code>{html.escape(summary.get('runtimeResetRiskClass') or '')}</code>; global reset ruled out: {summary.get('globalResetRuledOut')}; promotion status: <code>{html.escape(summary.get('promotionStatus') or '')}</code>.</p>",
        f"<p>{html.escape(summary.get('conclusion') or '')}</p>",
        "<h2>Proof Rows</h2><table><thead><tr><th>area</th><th>status</th><th>evidence</th><th>consequence</th></tr></thead><tbody>",
        rows,
        "</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_secondary_global_reset_gap.json").write_text(
        json.dumps(summary, ensure_ascii=False, indent=2) + "\n",
        encoding="utf-8",
    )
    (out_dir / "save_selector_secondary_global_reset_gap.html").write_text(html_page(summary), encoding="utf-8")


def main() -> None:
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--out-dir", type=Path, default=OUT)
    args = parser.parse_args()
    summary = build_summary(
        load_json(args.out_dir / "save_selector_secondary_reset_scope.json", {}),
        load_json(args.out_dir / "save_selector_secondary_state_sources.json", {}),
        load_json(args.out_dir / "save_selector_predecessor_tail_reset.json", {}),
        load_json(args.out_dir / "save_selector_predecessor_persistence_gap.json", {}),
        load_json(args.out_dir / "save_selector_secondary_fill_roots.json", {}),
        load_json(args.out_dir / "save_selector_secondary_route_overlap_candidates.json", {}),
        load_json(args.out_dir / "save_selector_secondary_block_writes.json", {}),
    )
    write_outputs(summary, args.out_dir)
    print(f"wrote secondary global reset gap -> {args.out_dir / 'save_selector_secondary_global_reset_gap.html'}")


if __name__ == "__main__":
    main()