#!/usr/bin/env python3
"""Summarize why selector merge evidence is closed as shape-only."""
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"

SELECTOR_MERGE_MISSING_EVIDENCE_BY_GATE = {
    "selector-merge-execution-proof": (
        "source/predecessor forward bridge or execution-like selector merge bridge into selector 2:0"
    ),
    "selected-root-runtime-execution": "real selected-root runtime execution for 0x00540714",
    "predecessor-fill-route-order-proof": (
        "observed predecessor opcode 0x10 fill context and route-order proof"
    ),
    "strict-source-hotspot": "strict map1_01a source coordinate or tile hotspot evidence",
}
SELECTOR_MERGE_CLOSURE_EVIDENCE_REFS = [
    {
        "path": "out/save_selector_merge_execution_gap.json",
        "fields": [
            "selectorMergeExecutionProofFound",
            "proofFound",
            "failedSelectorMergeExecutionGateIds",
            "missingEvidence",
            "evidenceRefCount",
        ],
    },
    {
        "path": "out/save_selector_merge_runtime_context.json",
        "fields": [
            "selectorMergeRuntimeProofFound",
            "proofFound",
            "failedSelectorMergeRuntimeGateIds",
            "missingEvidence",
            "evidenceRefCount",
        ],
    },
    {
        "path": "out/save_selector_set_decomposition.json",
        "fields": [
            "currentEqualsPredecessorPlusSource",
            "sourcePredecessorUnionCoversCurrent",
            "sourcePredecessorUnionExtraMaps",
            "proofFound",
        ],
    },
    {
        "path": "out/save_selector_recomposition_lattice.json",
        "fields": [
            "current",
            "routePairOnlyCurrentSelector",
            "exactPairUnionCount",
        ],
    },
    {
        "path": "out/save_selector_target_alias_bridges.json",
        "fields": [
            "targetAliasSelectors",
            "publicCoveredForwardHitSelectors",
            "addressAdjacentForwardHitSelectors",
            "forwardHitsAddressAdjacentOnly",
            "targetAliasExecutionExclusionStatus",
        ],
    },
    {
        "path": "out/save_selector_route_root_ref_context.json",
        "fields": [
            "allRouteSelectorRootsTableOnly",
            "predecessorToCurrentRootRefFound",
            "sourceTargetSplitAcrossPreviousSelectors",
        ],
    },
    {
        "path": "out/save_selector_predecessor_bridge_refs.json",
        "fields": [
            "forwardExecutionBridgeFound",
            "forwardBridgeRows",
            "promotionStatus",
        ],
    },
    {
        "path": "out/save_selector_selected_root_execution_gap.json",
        "fields": [
            "selectedRootExecutionRefFound",
            "runtimeProbeGate",
            "diagnosticExclusionGate",
            "proofFound",
        ],
    },
    {
        "path": "out/save_selector_predecessor_fill_opcode10_context.json",
        "fields": [
            "proofFound",
            "failedPredecessorFillOpcode10GateIds",
            "missingEvidence",
            "evidenceRefCount",
            "runtimeObservedAllZero",
            "branchStatePollFillMatchCount",
        ],
    },
    {
        "path": "out/save_selector_predecessor_persistence_gap.json",
        "fields": [
            "routeOrderProven",
            "persistenceProven",
            "selectorMergeGapOpen",
            "promotionStatus",
        ],
    },
]


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


def csv(values: list[Any] | None) -> str:
    return ",".join(str(value) for value in values or []) or "-"


def build_summary(
    merge_execution_gap: dict,
    merge_runtime_context: dict,
    set_decomposition: dict,
    recomposition_lattice: dict,
    target_alias_bridges: dict,
    route_root_ref_context: dict,
    predecessor_bridge_refs: dict,
    selected_root_execution_gap: dict,
    predecessor_fill_opcode10_context: dict,
    predecessor_persistence_gap: dict,
) -> dict:
    current = recomposition_lattice.get("current") or {}
    runtime_gate = selected_root_execution_gap.get("runtimeProbeGate") or {}
    diagnostic_gate = selected_root_execution_gap.get("diagnosticExclusionGate") or {}
    extra_maps = (
        merge_execution_gap.get("sourcePredecessorUnionExtraMaps")
        or current.get("sourcePredecessorUnionExtraMaps")
        or set_decomposition.get("sourcePredecessorUnionExtraMaps")
        or []
    )
    current_equals_predecessor_plus_source = (
        merge_execution_gap.get("currentEqualsPredecessorPlusSource") is True
        and set_decomposition.get("currentEqualsPredecessorPlusSource") is True
    )
    source_predecessor_union_covers_current = (
        merge_execution_gap.get("sourcePredecessorUnionCoversCurrent") is True
        or current.get("sourcePredecessorUnionCoversCurrent") is True
    )
    shape_over_includes_extra_maps = len(extra_maps) > 0
    shape_only = (
        current_equals_predecessor_plus_source
        and source_predecessor_union_covers_current
        and merge_runtime_context.get("mergeShapeOnly") is True
    )
    forward_bridge_absent = (
        merge_execution_gap.get("sourceToCurrentBridgeHitCount") == 0
        and merge_execution_gap.get("predecessorToCurrentHitCount") == 0
        and merge_execution_gap.get("forwardMergeBridgeHitCount") == 0
    )
    reverse_reuse_before_fill_only = (
        merge_execution_gap.get("currentToPredecessorHitCount") == 51
        and merge_execution_gap.get("currentToPredecessorBeforeFillHitCount") == 51
        and merge_execution_gap.get("currentToPredecessorFillSiteHitCount") == 0
    )
    alias_forward_address_adjacent_only = (
        target_alias_bridges.get("forwardHitsAddressAdjacentOnly") is True
        and target_alias_bridges.get("publicCoveredForwardHitAliasCount") == 0
        and target_alias_bridges.get("forwardHitPublicSampleCount") == 0
    )
    alias_execution_excluded = (
        target_alias_bridges.get("targetAliasExecutionExclusionStatus")
        == "address-adjacent-alias-data-only"
        and target_alias_bridges.get("aliasToCurrentExecutionLikeBridgeFound") is False
    )
    route_roots_table_only = (
        route_root_ref_context.get("allRouteSelectorRootsTableOnly") is True
        and route_root_ref_context.get("predecessorToCurrentRootRefFound") is False
    )
    selected_root_runtime_absent = (
        selected_root_execution_gap.get("selectedRootExecutionRefFound") is False
        and runtime_gate.get("anyRuntimePollReachedRouteSelector") is False
        and diagnostic_gate.get("excludedFromSelectedRootExecutionProof") is True
    )
    predecessor_fill_non_promoting = (
        predecessor_fill_opcode10_context.get("proofFound") is False
        and predecessor_fill_opcode10_context.get("runtimeObservedAllZero") is True
        and predecessor_fill_opcode10_context.get("branchStatePollFillMatchCount") == 0
    )
    route_order_proven = predecessor_persistence_gap.get("routeOrderProven")
    selector_merge_execution_proof_found = (
        merge_execution_gap.get("selectorMergeExecutionProofFound") is True
        or target_alias_bridges.get("aliasToCurrentExecutionLikeBridgeFound") is True
        or route_root_ref_context.get("predecessorToCurrentRootRefFound") is True
        or predecessor_bridge_refs.get("forwardExecutionBridgeFound") is True
    )
    selector_merge_runtime_proof_found = (
        merge_runtime_context.get("selectorMergeRuntimeProofFound") is True
        and selected_root_execution_gap.get("selectedRootExecutionRefFound") is True
    )
    predecessor_persistence_usable_for_current = (
        selector_merge_execution_proof_found
        and selector_merge_runtime_proof_found
        and predecessor_fill_opcode10_context.get("proofFound") is True
        and route_order_proven is True
    )
    strict_hotspot_missing = (
        merge_runtime_context.get("strictSourceCoordinateFound") is False
        and merge_runtime_context.get("tileHotspotConfirmed") is False
    )
    selector_merge_closure_proof_found = (
        selector_merge_execution_proof_found
        and selector_merge_runtime_proof_found
        and not strict_hotspot_missing
    )
    failed_selector_merge_gate_ids = []
    if not selector_merge_execution_proof_found:
        failed_selector_merge_gate_ids.append("selector-merge-execution-proof")
    if not selector_merge_runtime_proof_found:
        failed_selector_merge_gate_ids.append("selected-root-runtime-execution")
    if not (
        predecessor_fill_opcode10_context.get("proofFound") is True
        and route_order_proven is True
    ):
        failed_selector_merge_gate_ids.append("predecessor-fill-route-order-proof")
    if strict_hotspot_missing:
        failed_selector_merge_gate_ids.append("strict-source-hotspot")
    missing_evidence = [
        SELECTOR_MERGE_MISSING_EVIDENCE_BY_GATE.get(gate_id, gate_id)
        for gate_id in failed_selector_merge_gate_ids
    ]
    promotion_status = "ready-for-review" if selector_merge_closure_proof_found else "blocked"
    evidence = [
        {
            "kind": "shape-closure",
            "status": "shape-only-overinclusive" if shape_only and shape_over_includes_extra_maps else "open",
            "detail": (
                f"currentEqualsPredecessorPlusSource={current_equals_predecessor_plus_source}; "
                f"unionCoversCurrent={source_predecessor_union_covers_current}; "
                f"extra={csv(extra_maps)}; routePairOnlyCurrent="
                f"{merge_execution_gap.get('routePairOnlyCurrentSelector')}; "
                f"exactCurrentPairUnions={merge_execution_gap.get('currentExactPairUnionCount')}; "
                f"coveringCurrentPairUnions={merge_execution_gap.get('currentCoveringPairUnionCount')}; "
                f"globalExactPairUnions={merge_execution_gap.get('globalExactPairUnionCount')}"
            ),
        },
        {
            "kind": "forward-closure",
            "status": "no-forward-bridge" if forward_bridge_absent else "open",
            "detail": (
                f"sourceToCurrent={merge_execution_gap.get('sourceToCurrentBridgeHitCount')}; "
                f"predecessorToCurrent={merge_execution_gap.get('predecessorToCurrentHitCount')}; "
                f"forwardMergeBridge={merge_execution_gap.get('forwardMergeBridgeHitCount')}; "
                f"encodedRaw={merge_execution_gap.get('forwardEncodedAnchorRawScalarCandidateCount')}; "
                f"encodedPromoting={merge_execution_gap.get('forwardEncodedAnchorPromotingCandidateCount')}; "
                f"encodedMerge={merge_execution_gap.get('encodedMergeExecutionBridgeFound')}"
            ),
        },
        {
            "kind": "reverse-closure",
            "status": "reverse-reuse-before-fill-only" if reverse_reuse_before_fill_only else "open",
            "detail": (
                f"currentToPredecessor={merge_execution_gap.get('currentToPredecessorHitCount')}; "
                f"beforeFill={merge_execution_gap.get('currentToPredecessorBeforeFillHitCount')}; "
                f"fillSite={merge_execution_gap.get('currentToPredecessorFillSiteHitCount')}"
            ),
        },
        {
            "kind": "alias-closure",
            "status": "address-adjacent-data-only" if alias_forward_address_adjacent_only and alias_execution_excluded else "open",
            "detail": (
                f"targetAliases={csv(target_alias_bridges.get('targetAliasSelectors'))}; "
                f"publicForward={csv(target_alias_bridges.get('publicCoveredForwardHitSelectors'))}; "
                f"addressAdjacentForward={csv(target_alias_bridges.get('addressAdjacentForwardHitSelectors'))}; "
                f"publicSamples={target_alias_bridges.get('forwardHitPublicSampleCount')}; "
                f"executionLike={target_alias_bridges.get('aliasToCurrentExecutionLikeBridgeFound')}; "
                f"exclusion={target_alias_bridges.get('targetAliasExecutionExclusionStatus')}"
            ),
        },
        {
            "kind": "route-root-closure",
            "status": "table-only" if route_roots_table_only else "open",
            "detail": (
                f"allTableOnly={route_root_ref_context.get('allRouteSelectorRootsTableOnly')}; "
                f"textRefs={route_root_ref_context.get('anyRouteSelectorRootTextRefs')}; "
                f"predecessorToCurrentRootRef="
                f"{route_root_ref_context.get('predecessorToCurrentRootRefFound')}; "
                f"sourceTargetSplitAcrossPrevious="
                f"{route_root_ref_context.get('sourceTargetSplitAcrossPreviousSelectors')}"
            ),
        },
        {
            "kind": "selected-root-runtime",
            "status": "real-route-not-observed" if selected_root_runtime_absent else "open",
            "detail": (
                f"selectedRootExecutionRefFound="
                f"{selected_root_execution_gap.get('selectedRootExecutionRefFound')}; "
                f"anyRuntimePollRoute={runtime_gate.get('anyRuntimePollReachedRouteSelector')}; "
                f"constructedDiagnosticRoute="
                f"{runtime_gate.get('constructedDiagnosticPollReachedRouteSelector')}; "
                f"diagnosticExcluded={diagnostic_gate.get('excludedFromSelectedRootExecutionProof')}"
            ),
        },
        {
            "kind": "predecessor-fill-closure",
            "status": "opcode10-context-nonpromoting" if predecessor_fill_non_promoting else "open",
            "detail": (
                f"opcodeHandler={predecessor_fill_opcode10_context.get('opcodeHandlerHex')}; "
                f"helperOpcode10Only="
                f"{predecessor_fill_opcode10_context.get('helperOnlyDirectCallInsideOpcode10Handler')}; "
                f"directFillRefs={predecessor_fill_opcode10_context.get('directFillSiteTextRefCount')}; "
                f"runtimeAllZero={predecessor_fill_opcode10_context.get('runtimeObservedAllZero')}; "
                f"fillMatches={predecessor_fill_opcode10_context.get('branchStatePollFillMatchCount')}; "
                f"proof={predecessor_fill_opcode10_context.get('proofFound')}"
            ),
        },
        {
            "kind": "route-order-closure",
            "status": "route-order-unproven" if route_order_proven is False else "open",
            "detail": (
                f"routeOrderProven={route_order_proven}; "
                f"persistenceProven={predecessor_persistence_gap.get('persistenceProven')}; "
                f"selectorMergeGapOpen={predecessor_persistence_gap.get('selectorMergeGapOpen')}"
            ),
        },
        {
            "kind": "strict-hotspot",
            "status": "missing" if strict_hotspot_missing else "present",
            "detail": (
                f"strictSource={merge_runtime_context.get('strictSourceCoordinateFound')}; "
                f"tileHotspot={merge_runtime_context.get('tileHotspotConfirmed')}"
            ),
        },
    ]
    conclusion = (
        "Selector 2:0 can be explained as a source/predecessor set recomposition, but the closure remains "
        "shape-only: the union over-includes map1_02b, there is no source/predecessor forward bridge into "
        "2:0, reverse hits are before-fill reuse, target-alias hits are address-adjacent data only, route-root "
        "refs are table-only, and runtime evidence still lacks a real selected-root route observation."
    )
    return {
        "source": merge_execution_gap.get("source") or "map1_01a",
        "target": merge_execution_gap.get("target") or "map2_02d",
        "sourceSelector": merge_execution_gap.get("sourceSelector"),
        "predecessorSelector": merge_execution_gap.get("predecessorSelector"),
        "currentSelector": merge_execution_gap.get("currentSelector"),
        "currentRootHex": merge_execution_gap.get("currentRootHex"),
        "currentEqualsPredecessorPlusSource": current_equals_predecessor_plus_source,
        "sourcePredecessorUnionCoversCurrent": source_predecessor_union_covers_current,
        "sourcePredecessorUnionExtraMaps": extra_maps,
        "shapeOverIncludesExtraMaps": shape_over_includes_extra_maps,
        "routePairOnlyCurrentSelector": merge_execution_gap.get("routePairOnlyCurrentSelector"),
        "currentExactPairUnionCount": merge_execution_gap.get("currentExactPairUnionCount"),
        "currentCoveringPairUnionCount": merge_execution_gap.get("currentCoveringPairUnionCount"),
        "globalExactPairUnionCount": merge_execution_gap.get("globalExactPairUnionCount"),
        "mergeShapeOnly": shape_only,
        "sourceToCurrentBridgeHitCount": merge_execution_gap.get("sourceToCurrentBridgeHitCount"),
        "currentToSourceBridgeHitCount": merge_execution_gap.get("currentToSourceBridgeHitCount"),
        "predecessorToCurrentHitCount": merge_execution_gap.get("predecessorToCurrentHitCount"),
        "forwardMergeBridgeHitCount": merge_execution_gap.get("forwardMergeBridgeHitCount"),
        "forwardEncodedAnchorRawScalarCandidateCount": merge_execution_gap.get(
            "forwardEncodedAnchorRawScalarCandidateCount"
        ),
        "forwardEncodedAnchorPromotingCandidateCount": merge_execution_gap.get(
            "forwardEncodedAnchorPromotingCandidateCount"
        ),
        "encodedMergeExecutionBridgeFound": merge_execution_gap.get(
            "encodedMergeExecutionBridgeFound"
        ),
        "forwardBridgeAbsent": forward_bridge_absent,
        "currentToPredecessorHitCount": merge_execution_gap.get("currentToPredecessorHitCount"),
        "currentToPredecessorBeforeFillHitCount": merge_execution_gap.get(
            "currentToPredecessorBeforeFillHitCount"
        ),
        "currentToPredecessorFillSiteHitCount": merge_execution_gap.get(
            "currentToPredecessorFillSiteHitCount"
        ),
        "reverseReuseBeforeFillOnly": reverse_reuse_before_fill_only,
        "targetAliasSelectors": target_alias_bridges.get("targetAliasSelectors") or [],
        "targetAliasPublicCoveredForwardHitSelectors": target_alias_bridges.get(
            "publicCoveredForwardHitSelectors"
        )
        or [],
        "targetAliasAddressAdjacentForwardHitSelectors": target_alias_bridges.get(
            "addressAdjacentForwardHitSelectors"
        )
        or [],
        "targetAliasForwardHitPublicSampleCount": target_alias_bridges.get(
            "forwardHitPublicSampleCount"
        ),
        "targetAliasForwardHitsAddressAdjacentOnly": target_alias_bridges.get(
            "forwardHitsAddressAdjacentOnly"
        ),
        "targetAliasExecutionExclusionStatus": target_alias_bridges.get(
            "targetAliasExecutionExclusionStatus"
        ),
        "targetAliasToCurrentExecutionLikeBridgeFound": target_alias_bridges.get(
            "aliasToCurrentExecutionLikeBridgeFound"
        ),
        "routeRootsTableOnly": route_roots_table_only,
        "routeRootTextRefs": route_root_ref_context.get("anyRouteSelectorRootTextRefs"),
        "routeRootRefsPredecessorToCurrentRootRefFound": route_root_ref_context.get(
            "predecessorToCurrentRootRefFound"
        ),
        "routeRootRefsSourceTargetSplitAcrossPreviousSelectors": route_root_ref_context.get(
            "sourceTargetSplitAcrossPreviousSelectors"
        ),
        "predecessorBridgeForwardExecutionBridgeFound": predecessor_bridge_refs.get(
            "forwardExecutionBridgeFound"
        ),
        "selectedRootExecutionRefFound": selected_root_execution_gap.get(
            "selectedRootExecutionRefFound"
        ),
        "anyRuntimePollReachedRouteSelector": runtime_gate.get("anyRuntimePollReachedRouteSelector"),
        "constructedDiagnosticPollReachedRouteSelector": runtime_gate.get(
            "constructedDiagnosticPollReachedRouteSelector"
        ),
        "constructedDiagnosticExcludedFromProof": diagnostic_gate.get(
            "excludedFromSelectedRootExecutionProof"
        ),
        "predecessorFillOpcode10ProofFound": predecessor_fill_opcode10_context.get("proofFound"),
        "predecessorFillOpcode10HelperOnlyDirectCallInsideOpcode10Handler": (
            predecessor_fill_opcode10_context.get("helperOnlyDirectCallInsideOpcode10Handler")
        ),
        "predecessorFillOpcode10DirectFillSiteTextRefCount": predecessor_fill_opcode10_context.get(
            "directFillSiteTextRefCount"
        ),
        "predecessorFillOpcode10RuntimeObservedAllZero": predecessor_fill_opcode10_context.get(
            "runtimeObservedAllZero"
        ),
        "predecessorFillOpcode10BranchStatePollSampleCount": predecessor_fill_opcode10_context.get(
            "branchStatePollSampleCount"
        ),
        "predecessorFillOpcode10BranchStatePollFillMatchCount": predecessor_fill_opcode10_context.get(
            "branchStatePollFillMatchCount"
        ),
        "routeOrderProven": route_order_proven,
        "predecessorPersistenceProven": predecessor_persistence_gap.get("persistenceProven"),
        "predecessorPersistenceGapSelectorMergeGapOpen": predecessor_persistence_gap.get(
            "selectorMergeGapOpen"
        ),
        "strictSourceCoordinateFound": merge_runtime_context.get("strictSourceCoordinateFound"),
        "tileHotspotConfirmed": merge_runtime_context.get("tileHotspotConfirmed"),
        "selectorMergeExecutionProofFound": selector_merge_execution_proof_found,
        "selectorMergeRuntimeProofFound": selector_merge_runtime_proof_found,
        "selectorMergeClosureProofFound": selector_merge_closure_proof_found,
        "proofFound": selector_merge_closure_proof_found,
        "failedSelectorMergeGateIds": failed_selector_merge_gate_ids,
        "missingEvidence": missing_evidence,
        "evidenceRefs": SELECTOR_MERGE_CLOSURE_EVIDENCE_REFS,
        "evidenceRefCount": len(SELECTOR_MERGE_CLOSURE_EVIDENCE_REFS),
        "predecessorPersistenceUsableForCurrent": predecessor_persistence_usable_for_current,
        "selectorMergeGapOpen": not selector_merge_closure_proof_found,
        "promotionStatus": promotion_status,
        "evidence": evidence,
        "remainingProofs": [
            "prove a source/predecessor forward bridge into selector 2:0",
            "capture real selected-root runtime execution for 0x00540714",
            "turn predecessor opcode 0x10 fill context into an observed route-order proof",
            "find strict map1_01a source coordinate or tile hotspot evidence",
        ],
        "conclusion": conclusion,
    }


def markdown(summary: dict) -> str:
    lines = [
        "# Save Selector Merge Closure Context",
        "",
        summary["conclusion"],
        "",
        f"- route: `{summary['source']} -> {summary['target']}`",
        f"- selectors: source `{summary['sourceSelector']}`, predecessor `{summary['predecessorSelector']}`, current `{summary['currentSelector']}`",
        f"- current root: `{summary['currentRootHex']}`",
        f"- merge shape only: {summary['mergeShapeOnly']}",
        f"- source+predecessor extra maps: `{csv(summary['sourcePredecessorUnionExtraMaps'])}`",
        f"- forward bridge absent: {summary['forwardBridgeAbsent']}",
        f"- reverse reuse before fill only: {summary['reverseReuseBeforeFillOnly']}",
        f"- alias public/address-adjacent forward selectors: `{csv(summary['targetAliasPublicCoveredForwardHitSelectors'])}` / `{csv(summary['targetAliasAddressAdjacentForwardHitSelectors'])}`",
        f"- route roots table only: {summary['routeRootsTableOnly']}",
        f"- selected-root execution ref found: {summary['selectedRootExecutionRefFound']}",
        f"- predecessor opcode10 proof found: {summary['predecessorFillOpcode10ProofFound']}",
        f"- route order proven: {summary['routeOrderProven']}",
        f"- selector merge execution/runtime/closure proof found: {summary['selectorMergeExecutionProofFound']} / {summary['selectorMergeRuntimeProofFound']} / {summary['selectorMergeClosureProofFound']}",
        f"- proof found: {summary['proofFound']}",
        f"- failed selector-merge gates: `{csv(summary.get('failedSelectorMergeGateIds'))}`",
        f"- missing evidence count: {len(summary.get('missingEvidence') or [])}",
        f"- evidence refs: {summary.get('evidenceRefCount')}",
        f"- predecessor persistence usable for current: {summary['predecessorPersistenceUsableForCurrent']}",
        f"- promotion status: `{summary['promotionStatus']}`",
        "",
        "## Missing Evidence",
        "",
        *[f"- {item}" for item in summary.get("missingEvidence") or []],
        "",
        "## Evidence",
        "",
        "| kind | status | detail |",
        "| --- | --- | --- |",
    ]
    for row in summary["evidence"]:
        lines.append(f"| {row['kind']} | {row['status']} | {row['detail']} |")
    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["evidence"]
    )
    proof_items = "\n".join(f"<li>{html.escape(item)}</li>" for item in summary["remainingProofs"])
    missing_items = "\n".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">',
            "  <title>Save Selector Merge Closure Context</title>",
            "  <style>body{font-family:system-ui,sans-serif;margin:24px;line-height:1.45;max-width:1200px}table{border-collapse:collapse;width:100%;margin:16px 0}td,th{border:1px solid #ddd;padding:6px 8px;text-align:left;vertical-align:top}th{background:#f5f5f5}code{white-space:nowrap}</style>",
            "</head>",
            "<body>",
            "  <h1>Save Selector Merge Closure Context</h1>",
            f"  <p>{html.escape(summary['conclusion'])}</p>",
            (
                "  <p><b>Route:</b> "
                f"<code>{html.escape(str(summary['source']))}</code> -&gt; "
                f"<code>{html.escape(str(summary['target']))}</code>; "
                f"source <code>{html.escape(str(summary['sourceSelector']))}</code>; "
                f"predecessor <code>{html.escape(str(summary['predecessorSelector']))}</code>; "
                f"current <code>{html.escape(str(summary['currentSelector']))}</code> "
                f"root <code>{html.escape(str(summary['currentRootHex']))}</code>.</p>"
            ),
            (
                "  <p><b>Closure:</b> "
                f"shapeOnly={summary['mergeShapeOnly']}; "
                f"extraMaps=<code>{html.escape(csv(summary['sourcePredecessorUnionExtraMaps']))}</code>; "
                f"forwardBridgeAbsent={summary['forwardBridgeAbsent']}; "
                f"reverseBeforeFillOnly={summary['reverseReuseBeforeFillOnly']}; "
                f"routeRootsTableOnly={summary['routeRootsTableOnly']}; "
                f"selectedRootExecution={summary['selectedRootExecutionRefFound']}; "
                f"opcode10Proof={summary['predecessorFillOpcode10ProofFound']}; "
                f"routeOrder={summary['routeOrderProven']}; "
                f"closureProof={summary['selectorMergeClosureProofFound']}; "
                f"proofFound={summary['proofFound']}; "
                "failedSelectorMergeGates="
                f"<code>{html.escape(csv(summary.get('failedSelectorMergeGateIds')))}</code>; "
                f"missingEvidenceCount={len(summary.get('missingEvidence') or [])}; "
                f"evidenceRefs={summary.get('evidenceRefCount')}; "
                f"status <code>{html.escape(summary['promotionStatus'])}</code>.</p>"
            ),
            (
                "  <p><b>Alias closure:</b> "
                f"publicForward=<code>{html.escape(csv(summary['targetAliasPublicCoveredForwardHitSelectors']))}</code>; "
                f"addressAdjacentForward=<code>{html.escape(csv(summary['targetAliasAddressAdjacentForwardHitSelectors']))}</code>; "
                f"publicSamples={summary['targetAliasForwardHitPublicSampleCount']}; "
                f"exclusion <code>{html.escape(str(summary['targetAliasExecutionExclusionStatus']))}</code>.</p>"
            ),
            "  <h2>Missing Evidence</h2>",
            f"  <ul>{missing_items}</ul>",
            "  <h2>Evidence</h2>",
            f"  <table><thead><tr><th>kind</th><th>status</th><th>detail</th></tr></thead><tbody>{evidence_rows}</tbody></table>",
            "  <h2>Remaining Proofs</h2>",
            f"  <ul>{proof_items}</ul>",
            "</body>",
            "</html>",
            "",
        ]
    )


def write_outputs(summary: dict, out_dir: Path = OUT, html_out: Path | None = None) -> Path:
    out_dir.mkdir(parents=True, exist_ok=True)
    json_out = out_dir / "save_selector_merge_closure_context.json"
    json_out.write_text(
        json.dumps(summary, ensure_ascii=False, indent=2) + "\n",
        encoding="utf-8",
    )
    if html_out is not None:
        html_out.parent.mkdir(parents=True, exist_ok=True)
        html_out.write_text(html_page(summary), encoding="utf-8")
    return json_out


def main() -> None:
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--out-dir", type=Path, default=OUT)
    parser.add_argument("--html-out", type=Path)
    args = parser.parse_args()
    summary = build_summary(
        load_json(args.out_dir / "save_selector_merge_execution_gap.json"),
        load_json(args.out_dir / "save_selector_merge_runtime_context.json"),
        load_json(args.out_dir / "save_selector_set_decomposition.json"),
        load_json(args.out_dir / "save_selector_recomposition_lattice.json"),
        load_json(args.out_dir / "save_selector_target_alias_bridges.json"),
        load_json(args.out_dir / "save_selector_route_root_ref_context.json"),
        load_json(args.out_dir / "save_selector_predecessor_bridge_refs.json"),
        load_json(args.out_dir / "save_selector_selected_root_execution_gap.json"),
        load_json(args.out_dir / "save_selector_predecessor_fill_opcode10_context.json"),
        load_json(args.out_dir / "save_selector_predecessor_persistence_gap.json"),
    )
    json_out = write_outputs(summary, args.out_dir, args.html_out)
    print(f"wrote save selector merge closure context -> {json_out}")


if __name__ == "__main__":
    main()