#!/usr/bin/env python3
"""Consolidate selector-merge runtime proof context."""
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_RUNTIME_MISSING_EVIDENCE_BY_GATE = {
"selector-merge-execution-proof": (
"source/predecessor selector-merge execution proof into selector 2:0"
),
"selected-root-runtime-execution": (
"non-diagnostic selected-root runtime execution for 0x00540714"
),
"predecessor-fill-runtime-proof": (
"observed predecessor fill-state on the route path before the current reader"
),
"route-pair-entry-execution": (
"route-pair entry execution that reaches the current reader on a normal path"
),
"strict-source-hotspot": "strict map1_01a source coordinate or tile hotspot evidence",
}
SELECTOR_MERGE_RUNTIME_EVIDENCE_REFS = [
{
"path": "out/save_selector_merge_execution_gap.json",
"fields": [
"selectorMergeExecutionProofFound",
"proofFound",
"failedSelectorMergeExecutionGateIds",
"missingEvidence",
"evidenceRefCount",
],
},
{
"path": "out/save_selector_predecessor_fill_site_execution_context.json",
"fields": [
"fillSiteExecutionContextProven",
"branchStatePollSampleCount",
"branchStatePollFillMatchCount",
"proofFound",
"failedPredecessorFillGateIds",
],
},
{
"path": "out/save_selector_selected_root_execution_gap.json",
"fields": [
"selectedRootExecutionRefFound",
"runtimeProbeGate",
"diagnosticExclusionGate",
"proofFound",
],
},
{
"path": "out/save_selector_route_pair_entry_execution_gap.json",
"fields": [
"routePairEntryExecutionProven",
"routePairCorrectedTraceReachesReaderCount",
"sourceOrPredecessorCurrentProducerCount",
"proofFound",
],
},
{
"path": "out/map1_01a_strict_hotspot_review_matrix.json",
"fields": [
"strictSourceCoordinateFound",
"tileHotspotConfirmed",
"transitionReviewRowCount",
"eventTransitionCount",
"candidateCount",
],
},
]
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 bool_text(value: Any) -> str:
return str(bool(value))
def build_summary(
merge_execution_gap: dict,
predecessor_fill_site_execution_context: dict,
selected_root_execution_gap: dict,
route_pair_entry_execution_gap: dict,
strict_hotspot_review_matrix: dict | None = None,
) -> dict:
strict_hotspot_review_matrix = strict_hotspot_review_matrix or {}
runtime_gate = selected_root_execution_gap.get("runtimeProbeGate") or {}
diagnostic_gate = selected_root_execution_gap.get("diagnosticExclusionGate") or {}
merge_shape_only = (
merge_execution_gap.get("currentEqualsPredecessorPlusSource") is True
and merge_execution_gap.get("sourcePredecessorUnionCoversCurrent") is True
and merge_execution_gap.get("routePairOnlyCurrentSelector") is True
and merge_execution_gap.get("selectorMergeExecutionProofFound") is not 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
)
diagnostic_route_excluded = (
runtime_gate.get("constructedDiagnosticPollReachedRouteSelector") is True
and diagnostic_gate.get("excludedFromSelectedRootExecutionProof") is True
)
public_predecessor_no_fill = (
int(predecessor_fill_site_execution_context.get("branchStatePollPublicPredecessorHitCount") or 0) > 0
and predecessor_fill_site_execution_context.get("branchStatePollFillMatchCount") == 0
)
strict_hotspot_missing = (
strict_hotspot_review_matrix.get("strictSourceCoordinateFound") is False
and strict_hotspot_review_matrix.get("tileHotspotConfirmed") is False
)
route_pair_entry_unexecuted = (
route_pair_entry_execution_gap.get("routePairEntryExecutionProven") is False
and route_pair_entry_execution_gap.get("routePairCorrectedTraceReachesReaderCount") == 2
)
selector_merge_runtime_proof_found = (
merge_execution_gap.get("selectorMergeExecutionProofFound") is True
and selected_root_execution_gap.get("selectedRootExecutionRefFound") is True
and predecessor_fill_site_execution_context.get("fillSiteExecutionContextProven") is True
)
failed_selector_merge_runtime_gate_ids = []
if merge_execution_gap.get("selectorMergeExecutionProofFound") is not True:
failed_selector_merge_runtime_gate_ids.append("selector-merge-execution-proof")
if (
selected_root_execution_gap.get("selectedRootExecutionRefFound") is not True
or runtime_gate.get("anyRuntimePollReachedRouteSelector") is not True
or diagnostic_gate.get("excludedFromSelectedRootExecutionProof") is True
):
failed_selector_merge_runtime_gate_ids.append("selected-root-runtime-execution")
if predecessor_fill_site_execution_context.get("fillSiteExecutionContextProven") is not True:
failed_selector_merge_runtime_gate_ids.append("predecessor-fill-runtime-proof")
if route_pair_entry_execution_gap.get("routePairEntryExecutionProven") is not True:
failed_selector_merge_runtime_gate_ids.append("route-pair-entry-execution")
if strict_hotspot_missing:
failed_selector_merge_runtime_gate_ids.append("strict-source-hotspot")
missing_evidence = [
SELECTOR_MERGE_RUNTIME_MISSING_EVIDENCE_BY_GATE.get(gate_id, gate_id)
for gate_id in failed_selector_merge_runtime_gate_ids
]
promotion_status = "ready-for-review" if selector_merge_runtime_proof_found else "blocked"
evidence = [
{
"kind": "merge-shape",
"status": "shape-only" if merge_shape_only else "not-merge-shaped",
"detail": (
f"currentEqualsPredecessorPlusSource="
f"{merge_execution_gap.get('currentEqualsPredecessorPlusSource')}; "
f"unionCoversCurrent={merge_execution_gap.get('sourcePredecessorUnionCoversCurrent')}; "
f"extra={csv(merge_execution_gap.get('sourcePredecessorUnionExtraMaps') or [])}; "
f"routePairOnlyCurrent={merge_execution_gap.get('routePairOnlyCurrentSelector')}"
),
},
{
"kind": "forward-bridge",
"status": "absent" if forward_bridge_absent else "present",
"detail": (
f"sourceToCurrent={merge_execution_gap.get('sourceToCurrentBridgeHitCount')}; "
f"predecessorToCurrent={merge_execution_gap.get('predecessorToCurrentHitCount')}; "
f"forwardMergeBridge={merge_execution_gap.get('forwardMergeBridgeHitCount')}; "
"encodedRaw="
f"{merge_execution_gap.get('forwardEncodedAnchorRawScalarCandidateCount')}; "
"encodedPromoting="
f"{merge_execution_gap.get('forwardEncodedAnchorPromotingCandidateCount')}; "
"encodedMerge="
f"{merge_execution_gap.get('encodedMergeExecutionBridgeFound')}; "
"aliasPublicForward="
f"{csv(merge_execution_gap.get('targetAliasPublicCoveredForwardHitSelectors'))}; "
"aliasAddressAdjacentForward="
f"{csv(merge_execution_gap.get('targetAliasAddressAdjacentForwardHitSelectors'))}; "
"aliasCoverage="
f"{merge_execution_gap.get('targetAliasPublicForwardHitCoverageStatus')}; "
"aliasExclusion="
f"{merge_execution_gap.get('targetAliasExecutionExclusionStatus')}"
),
},
{
"kind": "reverse-reuse",
"status": "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": "selected-root-runtime",
"status": "diagnostic-excluded" if diagnostic_route_excluded else "not-observed",
"detail": (
f"selectedRootRef={selected_root_execution_gap.get('selectedRootExecutionRefFound')}; "
f"anyPollRoute={runtime_gate.get('anyRuntimePollReachedRouteSelector')}; "
f"patchedRoute={runtime_gate.get('patchedPublicSelector20InputPathCaseAliasPollReachedRouteSelector')}; "
f"diagnosticExcluded={diagnostic_gate.get('excludedFromSelectedRootExecutionProof')}; "
f"followup={diagnostic_gate.get('followupSelector')}"
),
},
{
"kind": "predecessor-fill-runtime",
"status": "public-predecessor-fill-not-observed"
if public_predecessor_no_fill
else "not-classified",
"detail": (
f"branchPolls={predecessor_fill_site_execution_context.get('branchStatePollCount')}; "
f"samples={predecessor_fill_site_execution_context.get('branchStatePollSampleCount')}; "
f"publicHits={predecessor_fill_site_execution_context.get('branchStatePollPublicPredecessorHitCount')}; "
f"fillMatches={predecessor_fill_site_execution_context.get('branchStatePollFillMatchCount')}; "
f"contextProof={predecessor_fill_site_execution_context.get('fillSiteExecutionContextProven')}"
),
},
{
"kind": "route-pair-entry-execution",
"status": "reader-shaped-not-executed" if route_pair_entry_unexecuted else "executed",
"detail": (
f"entryIdx={route_pair_entry_execution_gap.get('routePairEntryIndices')}; "
f"correctedReader={route_pair_entry_execution_gap.get('routePairCorrectedTraceReachesReaderCount')}; "
f"sourcePredCurrentProducers="
f"{route_pair_entry_execution_gap.get('sourceOrPredecessorCurrentProducerCount')}; "
f"entryExec={route_pair_entry_execution_gap.get('routePairEntryExecutionProven')}"
),
},
{
"kind": "strict-hotspot",
"status": "missing" if strict_hotspot_missing else "present",
"detail": (
f"strictSource={strict_hotspot_review_matrix.get('strictSourceCoordinateFound')}; "
f"tileHotspot={strict_hotspot_review_matrix.get('tileHotspotConfirmed')}; "
f"routeReviews={strict_hotspot_review_matrix.get('transitionReviewRowCount')}; "
f"strictEvents={strict_hotspot_review_matrix.get('eventTransitionCount')}; "
f"candidates={strict_hotspot_review_matrix.get('candidateCount')}"
),
},
]
conclusion = (
"Selector 2:0 remains a merge-shaped runtime gap. It combines the predecessor 1:0 map set with "
"map1_01a and is the only selector carrying the route pair, but no source/predecessor forward bridge, "
"selected-root execution ref, predecessor fill observation, or strict hotspot proves that the merged "
"selector executes on the normal route."
)
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": merge_execution_gap.get(
"currentEqualsPredecessorPlusSource"
),
"sourcePredecessorUnionCoversCurrent": merge_execution_gap.get(
"sourcePredecessorUnionCoversCurrent"
),
"sourcePredecessorUnionExtraMaps": merge_execution_gap.get(
"sourcePredecessorUnionExtraMaps"
)
or [],
"routePairOnlyCurrentSelector": merge_execution_gap.get("routePairOnlyCurrentSelector"),
"currentExactPairUnionCount": merge_execution_gap.get("currentExactPairUnionCount"),
"sourceToCurrentBridgeHitCount": merge_execution_gap.get("sourceToCurrentBridgeHitCount"),
"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"
),
"targetAliasPublicCoveredForwardHitSelectors": merge_execution_gap.get(
"targetAliasPublicCoveredForwardHitSelectors"
)
or [],
"targetAliasForwardHitPublicSampleCount": merge_execution_gap.get(
"targetAliasForwardHitPublicSampleCount"
),
"targetAliasAddressAdjacentForwardHitSelectors": merge_execution_gap.get(
"targetAliasAddressAdjacentForwardHitSelectors"
)
or [],
"targetAliasForwardHitsAddressAdjacentOnly": merge_execution_gap.get(
"targetAliasForwardHitsAddressAdjacentOnly"
),
"targetAliasPublicForwardHitCoverageStatus": merge_execution_gap.get(
"targetAliasPublicForwardHitCoverageStatus"
),
"targetAliasExecutionExclusionStatus": merge_execution_gap.get(
"targetAliasExecutionExclusionStatus"
),
"currentToPredecessorHitCount": merge_execution_gap.get("currentToPredecessorHitCount"),
"currentToPredecessorBeforeFillHitCount": merge_execution_gap.get(
"currentToPredecessorBeforeFillHitCount"
),
"currentToPredecessorFillSiteHitCount": merge_execution_gap.get(
"currentToPredecessorFillSiteHitCount"
),
"mergeShapeOnly": merge_shape_only,
"forwardBridgeAbsent": forward_bridge_absent,
"reverseReuseBeforeFillOnly": reverse_reuse_before_fill_only,
"selectedRootExecutionRefFound": selected_root_execution_gap.get("selectedRootExecutionRefFound"),
"anyRuntimePollReachedRouteSelector": runtime_gate.get("anyRuntimePollReachedRouteSelector"),
"constructedDiagnosticPollReachedRouteSelector": runtime_gate.get(
"constructedDiagnosticPollReachedRouteSelector"
),
"constructedDiagnosticExcludedFromProof": diagnostic_gate.get(
"excludedFromSelectedRootExecutionProof"
),
"predecessorFillSiteExecutionContextProven": predecessor_fill_site_execution_context.get(
"fillSiteExecutionContextProven"
),
"predecessorBranchStatePollSampleCount": predecessor_fill_site_execution_context.get(
"branchStatePollSampleCount"
),
"predecessorBranchStatePollFillMatchCount": predecessor_fill_site_execution_context.get(
"branchStatePollFillMatchCount"
),
"routePairEntryExecutionProven": route_pair_entry_execution_gap.get(
"routePairEntryExecutionProven"
),
"routePairCorrectedTraceReachesReaderCount": route_pair_entry_execution_gap.get(
"routePairCorrectedTraceReachesReaderCount"
),
"strictSourceCoordinateFound": strict_hotspot_review_matrix.get("strictSourceCoordinateFound"),
"tileHotspotConfirmed": strict_hotspot_review_matrix.get("tileHotspotConfirmed"),
"selectorMergeExecutionProofFound": merge_execution_gap.get(
"selectorMergeExecutionProofFound"
),
"selectorMergeRuntimeProofFound": selector_merge_runtime_proof_found,
"proofFound": selector_merge_runtime_proof_found,
"failedSelectorMergeRuntimeGateIds": failed_selector_merge_runtime_gate_ids,
"missingEvidence": missing_evidence,
"evidenceRefs": SELECTOR_MERGE_RUNTIME_EVIDENCE_REFS,
"evidenceRefCount": len(SELECTOR_MERGE_RUNTIME_EVIDENCE_REFS),
"selectorMergeGapOpen": merge_execution_gap.get("selectorMergeGapOpen") is True
or not selector_merge_runtime_proof_found,
"promotionStatus": promotion_status,
"evidence": evidence,
"remainingProofs": [
"prove a source/predecessor forward bridge into selector 2:0",
"capture selected-root execution for 0x00540714 on a non-diagnostic path",
"observe predecessor fill-state on the route path before the current reader",
"find strict map1_01a source coordinate or tile hotspot evidence",
],
"conclusion": conclusion,
}
def markdown(summary: dict) -> str:
lines = [
"# Save Selector Merge Runtime 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"- current equals predecessor plus source: {summary['currentEqualsPredecessorPlusSource']}",
f"- source+predecessor union covers current: {summary['sourcePredecessorUnionCoversCurrent']}",
f"- source+predecessor extra maps: `{csv(summary.get('sourcePredecessorUnionExtraMaps'))}`",
f"- route pair only current selector: {summary['routePairOnlyCurrentSelector']}",
f"- forward bridge absent: {summary['forwardBridgeAbsent']}",
f"- target alias public/address-adjacent forward selectors: `{csv(summary.get('targetAliasPublicCoveredForwardHitSelectors'))}` / `{csv(summary.get('targetAliasAddressAdjacentForwardHitSelectors'))}`",
f"- target alias public coverage/exclusion: `{summary.get('targetAliasPublicForwardHitCoverageStatus')}` / `{summary.get('targetAliasExecutionExclusionStatus')}`",
f"- reverse reuse before fill only: {summary['reverseReuseBeforeFillOnly']}",
f"- selected-root execution ref found: {summary['selectedRootExecutionRefFound']}",
f"- constructed diagnostic excluded from proof: {summary['constructedDiagnosticExcludedFromProof']}",
f"- predecessor fill-site execution context proven: {summary['predecessorFillSiteExecutionContextProven']}",
f"- route-pair entry execution proven: {summary['routePairEntryExecutionProven']}",
f"- strict source coordinate / tile hotspot: {summary['strictSourceCoordinateFound']} / {summary['tileHotspotConfirmed']}",
f"- selector merge runtime proof found: {summary['selectorMergeRuntimeProofFound']}",
f"- proof found: {summary['proofFound']}",
f"- failed selector-merge runtime gates: `{csv(summary.get('failedSelectorMergeRuntimeGateIds'))}`",
f"- missing evidence count: {len(summary.get('missingEvidence') or [])}",
f"- evidence refs: {summary.get('evidenceRefCount')}",
f"- promotion status: `{summary['promotionStatus']}`",
"",
"## Missing Evidence",
"",
*[f"- {item}" for item in summary.get("missingEvidence") or []],
"",
"## Evidence",
"",
"| kind | status | detail |",
"| --- | --- | --- |",
]
for row in summary.get("evidence") or []:
lines.append(f"| {row['kind']} | {row['status']} | {row['detail']} |")
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:
evidence_rows = "\n".join(
""
f"| {html.escape(row['kind'])} | "
f"{html.escape(row['status'])} | "
f"{html.escape(row['detail'])} | "
"
"
for row in summary.get("evidence") or []
)
proof_items = "\n".join(
f"{html.escape(item)}" for item in summary.get("remainingProofs") or []
)
missing_items = "\n".join(
f"{html.escape(item)}" for item in summary.get("missingEvidence") or []
)
return "\n".join([
"",
'',
"",
' ',
" Save Selector Merge Runtime Context",
" ",
"",
"",
" Save Selector Merge Runtime Context
",
f" {html.escape(summary['conclusion'])}
",
(
" Route: "
f"{html.escape(str(summary['source']))} -> "
f"{html.escape(str(summary['target']))}.
"
),
(
" Selectors: "
f"source {html.escape(str(summary['sourceSelector']))}; "
f"predecessor {html.escape(str(summary['predecessorSelector']))}; "
f"current {html.escape(str(summary['currentSelector']))} "
f"root {html.escape(str(summary['currentRootHex']))}.
"
),
(
" Proof: "
f"forward bridge absent {bool_text(summary['forwardBridgeAbsent'])}; "
"target alias public/address-adjacent forward selectors "
f"{html.escape(csv(summary.get('targetAliasPublicCoveredForwardHitSelectors')))}/"
f"{html.escape(csv(summary.get('targetAliasAddressAdjacentForwardHitSelectors')))}; "
f"target alias public coverage/exclusion {html.escape(str(summary.get('targetAliasPublicForwardHitCoverageStatus')))}/"
f"{html.escape(str(summary.get('targetAliasExecutionExclusionStatus')))}; "
f"alias exclusion {html.escape(str(summary.get('targetAliasExecutionExclusionStatus')))}; "
f"selected-root ref {bool_text(summary['selectedRootExecutionRefFound'])}; "
f"diagnostic excluded {bool_text(summary['constructedDiagnosticExcludedFromProof'])}; "
f"predecessor fill context {bool_text(summary['predecessorFillSiteExecutionContextProven'])}; "
f"strict hotspot {bool_text(summary['strictSourceCoordinateFound'] or summary['tileHotspotConfirmed'])}; "
f"runtime proof {bool_text(summary['selectorMergeRuntimeProofFound'])}; "
f"proofFound={summary['proofFound']}; "
"failedSelectorMergeRuntimeGates="
f"{html.escape(csv(summary.get('failedSelectorMergeRuntimeGateIds')))}; "
f"missingEvidenceCount={len(summary.get('missingEvidence') or [])}; "
f"evidenceRefs={summary.get('evidenceRefCount')}; "
f"promotion status {html.escape(summary['promotionStatus'])}.
"
),
" Missing Evidence
",
f" ",
" Evidence
",
f" | kind | status | detail |
|---|
{evidence_rows}
",
" Remaining Proofs
",
f" ",
"",
"",
"",
])
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_runtime_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_predecessor_fill_site_execution_context.json"),
load_json(args.out_dir / "save_selector_selected_root_execution_gap.json"),
load_json(args.out_dir / "save_selector_route_pair_entry_execution_gap.json"),
load_json(args.out_dir / "map1_01a_strict_hotspot_review_matrix.json"),
)
json_out = write_outputs(summary, args.out_dir, args.html_out)
print(f"wrote save selector merge runtime context -> {json_out}")
if __name__ == "__main__":
main()