#!/usr/bin/env python3 """Consolidate selector-merge shape evidence versus execution proof.""" 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_EXECUTION_MISSING_EVIDENCE_BY_GATE = { "source-current-bridge": "VM control-flow edge from source selector 0:0 into current selector 2:0", "predecessor-current-forward-bridge": ( "predecessor/target-side forward bridge into current selector 2:0" ), "execution-like-bridge-or-root-ref": ( "execution-like target-alias bridge, encoded merge bridge, or predecessor-to-current root ref" ), "branch-state-execution-proof": "branch-state execution proof reaching the current reader", "strict-source-hotspot": "strict map1_01a source coordinate or hotspot", } SELECTOR_MERGE_EXECUTION_EVIDENCE_REFS = [ { "path": "out/save_selector_set_decomposition.json", "fields": [ "currentEqualsPredecessorPlusSource", "sourcePredecessorUnionCoversCurrent", "sourcePredecessorUnionExtraMaps", "proofFound", ], }, { "path": "out/save_selector_recomposition_lattice.json", "fields": [ "current", "routePairOnlyCurrentSelector", "exactPairUnionCount", "oneMapAugmentationCount", ], }, { "path": "out/save_selector_merge_gap.json", "fields": [ "sourceToCurrentBridgeHitCount", "currentToSourceBridgeHitCount", "targetToCurrentBridgeHitCount", "selectorMergeGapOpen", ], }, { "path": "out/save_selector_merge_bridge_matrix.json", "fields": [ "sourceToCurrentHitCount", "predecessorToCurrentHitCount", "currentToPredecessorHitCount", "currentToPredecessorBeforeFillHitCount", "currentToPredecessorFillSiteHitCount", "forwardMergeBridgeHitCount", "encodedMergeExecutionBridgeFound", ], }, { "path": "out/save_selector_target_alias_bridges.json", "fields": [ "targetAliasSelectors", "aliasToCurrentExecutionLikeBridgeFound", "forwardHitsAddressAdjacentOnly", "targetAliasExecutionExclusionStatus", "aliasBridgeSummaryRows", ], }, { "path": "out/save_selector_route_root_ref_context.json", "fields": [ "allRouteSelectorRootsTableOnly", "predecessorToCurrentRootRefFound", "sourceTargetSplitAcrossPreviousSelectors", ], }, { "path": "out/save_selector_predecessor_branch_state_execution_gap.json", "fields": [ "branchStateExecutionProofFound", "runtimeBranchStateSplit", "strictHotspotFound", "proofFound", ], }, ] def csv(values: list[Any] | None) -> str: return ",".join(str(value) for value in values or []) or "-" def class_counts_text(counts: dict | None) -> str: counts = counts or {} return ",".join(f"{key}:{counts[key]}" for key in sorted(counts)) or "-" def build_summary( set_decomposition: dict, recomposition_lattice: dict, merge_gap: dict, merge_bridge_matrix: dict, target_alias_bridges: dict, route_root_ref_context: dict, predecessor_branch_state_execution_gap: dict, ) -> dict: current = recomposition_lattice.get("current") or {} current_selector = current.get("currentSelector") or {} source_selector = current.get("sourceSelector") or {} predecessor_selector = current.get("predecessorSelector") or {} current_equals_predecessor_plus_source = bool( set_decomposition.get("currentEqualsPredecessorPlusSource") and current.get("currentEqualsPredecessorPlusSource") ) current_source_predecessor_extra_maps = ( current.get("sourcePredecessorUnionExtraMaps") or set_decomposition.get("sourcePredecessorUnionExtraMaps") or [] ) route_pair_only_current = recomposition_lattice.get("routePairOnlyCurrentSelector") is True exact_pair_union_count = len(current.get("currentExactPairUnions") or []) covering_pair_count = len(current.get("currentCoveringPairUnions") or []) forward_merge_bridge_count = merge_bridge_matrix.get("forwardMergeBridgeHitCount") direct_merge_execution_bridge_found = ( merge_bridge_matrix.get("directMergeExecutionBridgeFound") is True or target_alias_bridges.get("aliasToCurrentExecutionLikeBridgeFound") is True or target_alias_bridges.get("aliasToCurrentAfterLastFillExecutionLikeBridgeFound") is True ) source_current_bridge_absent = ( merge_gap.get("sourceToCurrentBridgeHitCount") == 0 and merge_gap.get("currentToSourceBridgeHitCount") == 0 and merge_bridge_matrix.get("sourceToCurrentHitCount") == 0 ) predecessor_current_forward_absent = ( merge_bridge_matrix.get("predecessorToCurrentHitCount") == 0 and merge_gap.get("targetToCurrentBridgeHitCount") == 0 ) reverse_reuse_only = ( merge_bridge_matrix.get("currentToPredecessorHitCount") == 51 and merge_bridge_matrix.get("currentToPredecessorBeforeFillHitCount") == 51 and merge_bridge_matrix.get("currentToPredecessorFillSiteHitCount") == 0 ) route_roots_table_only = route_root_ref_context.get("allRouteSelectorRootsTableOnly") is True route_root_execution_ref_found = route_root_ref_context.get("predecessorToCurrentRootRefFound") is True target_alias_execution_bridge_found = target_alias_bridges.get("aliasToCurrentExecutionLikeBridgeFound") is True target_alias_forward_hit_selectors = target_alias_bridges.get("aliasesWithForwardHits") or [] target_alias_forward_data_selectors = target_alias_bridges.get("aliasesWithForwardDataHits") or [] target_alias_after_fill_data_selectors = target_alias_bridges.get("aliasesWithAfterLastFillDataHits") or [] target_alias_dominant_data_selectors = target_alias_bridges.get("dominantForwardDataAliases") or [] target_alias_bridge_summary_rows = target_alias_bridges.get("aliasBridgeSummaryRows") or [] target_alias_public_covered_selectors = target_alias_bridges.get("publicCoveredAliasSelectors") or [] target_alias_public_forward_selectors = target_alias_bridges.get("publicCoveredForwardHitSelectors") or [] target_alias_address_adjacent_forward_selectors = ( target_alias_bridges.get("addressAdjacentForwardHitSelectors") or [] ) target_alias_forward_hit_coverage_status = target_alias_bridges.get("publicForwardHitCoverageStatus") target_alias_execution_exclusion_status = target_alias_bridges.get("targetAliasExecutionExclusionStatus") target_alias_execution_exclusion_detail = target_alias_bridges.get("targetAliasExecutionExclusionDetail") forward_encoded_anchor_raw_count = merge_bridge_matrix.get("forwardEncodedAnchorRawScalarCandidateCount") forward_encoded_anchor_promoting_count = merge_bridge_matrix.get( "forwardEncodedAnchorPromotingCandidateCount" ) encoded_merge_execution_bridge_found = ( merge_bridge_matrix.get("encodedMergeExecutionBridgeFound") is True ) branch_state_execution_proof_found = ( predecessor_branch_state_execution_gap.get("branchStateExecutionProofFound") is True ) selector_merge_execution_proof_found = ( direct_merge_execution_bridge_found or encoded_merge_execution_bridge_found or route_root_execution_ref_found or target_alias_execution_bridge_found ) runtime_or_control_flow_proof_found = ( selector_merge_execution_proof_found and branch_state_execution_proof_found ) strict_hotspot_found = predecessor_branch_state_execution_gap.get("strictHotspotFound") is True proof_found = runtime_or_control_flow_proof_found failed_selector_merge_execution_gate_ids = [] if source_current_bridge_absent: failed_selector_merge_execution_gate_ids.append("source-current-bridge") if predecessor_current_forward_absent: failed_selector_merge_execution_gate_ids.append("predecessor-current-forward-bridge") if not selector_merge_execution_proof_found: failed_selector_merge_execution_gate_ids.append("execution-like-bridge-or-root-ref") if not branch_state_execution_proof_found: failed_selector_merge_execution_gate_ids.append("branch-state-execution-proof") if not strict_hotspot_found: failed_selector_merge_execution_gate_ids.append("strict-source-hotspot") missing_evidence = [ SELECTOR_MERGE_EXECUTION_MISSING_EVIDENCE_BY_GATE.get(gate_id, gate_id) for gate_id in failed_selector_merge_execution_gate_ids ] selector_merge_gap_open = ( merge_gap.get("selectorMergeGapOpen") is True or merge_bridge_matrix.get("selectorMergeProofStatus") == "blocked" or not selector_merge_execution_proof_found ) promotion_status = "blocked" if selector_merge_gap_open else "ready-for-review" evidence = [ { "kind": "set-recomposition-shape", "status": "merge-shaped" if current_equals_predecessor_plus_source else "not-merge-shaped", "detail": ( f"currentEqualsPredecessorPlusSource={current_equals_predecessor_plus_source}; " f"sourcePredecessorUnionExtra={csv(current_source_predecessor_extra_maps)}; " f"routePairOnlyCurrent={route_pair_only_current}" ), }, { "kind": "exact-previous-union", "status": "absent" if exact_pair_union_count == 0 else "present", "detail": ( f"currentExactPairUnions={exact_pair_union_count}; " f"coveringPairUnions={covering_pair_count}; " f"globalExactPairUnions={recomposition_lattice.get('exactPairUnionCount')}" ), }, { "kind": "source-current-bridge", "status": "absent" if source_current_bridge_absent else "present", "detail": ( f"sourceToCurrent={merge_gap.get('sourceToCurrentBridgeHitCount')}; " f"currentToSource={merge_gap.get('currentToSourceBridgeHitCount')}; " f"matrixSourceToCurrent={merge_bridge_matrix.get('sourceToCurrentHitCount')}" ), }, { "kind": "predecessor-current-forward-bridge", "status": "absent" if predecessor_current_forward_absent else "present", "detail": ( f"predecessorToCurrent={merge_bridge_matrix.get('predecessorToCurrentHitCount')}; " f"targetToCurrent={merge_gap.get('targetToCurrentBridgeHitCount')}; " f"forwardMergeBridge={forward_merge_bridge_count}; " f"encodedRaw={forward_encoded_anchor_raw_count}; " f"encodedPromoting={forward_encoded_anchor_promoting_count}; " f"encodedMerge={encoded_merge_execution_bridge_found}" ), }, { "kind": "current-predecessor-reverse-reuse", "status": "reuse-before-fill" if reverse_reuse_only else "open", "detail": ( f"currentToPredecessor={merge_bridge_matrix.get('currentToPredecessorHitCount')}; " f"beforeFill={merge_bridge_matrix.get('currentToPredecessorBeforeFillHitCount')}; " f"fillSite={merge_bridge_matrix.get('currentToPredecessorFillSiteHitCount')}" ), }, { "kind": "target-alias-bridge", "status": "non-execution-like" if not target_alias_execution_bridge_found else "execution-like", "detail": ( f"aliases={csv(target_alias_bridges.get('targetAliasSelectors'))}; " f"hits={target_alias_bridges.get('aliasToCurrentHitCount')}; " f"metadata/data={target_alias_bridges.get('aliasToCurrentMetadataHitCount')}/" f"{target_alias_bridges.get('aliasToCurrentDataHitCount')}; " "promotingMeta/Data=" f"{target_alias_bridges.get('aliasToCurrentPromotingMetadataHitCount')}/" f"{target_alias_bridges.get('aliasToCurrentPromotingDataHitCount')}; " f"metadataOnlyExact={target_alias_bridges.get('aliasToCurrentPromotingExactMetadataOnly')}; " f"afterFill={target_alias_bridges.get('aliasToCurrentAfterLastFillHitCount')}; " f"forwardHitAliases={csv(target_alias_forward_hit_selectors)}; " f"dataAliases={csv(target_alias_forward_data_selectors)}; " f"afterFillDataAliases={csv(target_alias_after_fill_data_selectors)}; " f"dominantDataAliases={csv(target_alias_dominant_data_selectors)}; " f"publicCovered={csv(target_alias_public_covered_selectors)}; " f"publicForward={csv(target_alias_public_forward_selectors)}; " f"addressAdjacentForward={csv(target_alias_address_adjacent_forward_selectors)}; " f"publicCoverage={target_alias_forward_hit_coverage_status}; " f"exclusion={target_alias_execution_exclusion_status}; " f"readerScene={target_alias_bridges.get('aliasToCurrentReaderOrSceneRecordHitCount')}; " f"executionLike={target_alias_execution_bridge_found}" ), }, { "kind": "route-root-ref-context", "status": "table-only" if route_roots_table_only and not route_root_execution_ref_found else "execution-ref", "detail": ( f"allTableOnly={route_roots_table_only}; " f"textRefs={route_root_ref_context.get('anyRouteSelectorRootTextRefs')}; " f"splitPrevious={route_root_ref_context.get('sourceTargetSplitAcrossPreviousSelectors')}; " f"predToCurrentRootRef={route_root_execution_ref_found}" ), }, { "kind": "branch-state-execution-proof", "status": "blocked" if not branch_state_execution_proof_found else "proven", "detail": ( f"fillWouldPass=" f"{predecessor_branch_state_execution_gap.get('predecessorFillWouldPassCurrentReader')}; " f"branchStateExecutionProofFound={branch_state_execution_proof_found}; " f"runtimeOrderGapOpen=" f"{predecessor_branch_state_execution_gap.get('openRuntimeOrderOrBytecodeGap')}; " f"strictHotspotFound={predecessor_branch_state_execution_gap.get('strictHotspotFound')}" ), }, ] conclusion = ( "Selector 2:0 still looks like a recomposed selector list, not a proven execution step. " "It is the only selector containing the route pair and can be described as target-side 1:0 plus map1_01a, " "but exact previous unions, source/current bridges, predecessor/current forward bridges, route-root execution refs, " "and execution-like target-alias bridges are absent. The merge gap therefore stays open until selected-root " "runtime evidence, VM control-flow proof, or a strict source hotspot appears." ) return { "source": set_decomposition.get("source") or "map1_01a", "target": set_decomposition.get("target") or "map2_02d", "sourceSelector": source_selector.get("selector") or set_decomposition.get("sourceSelector"), "sourceRootHex": source_selector.get("rootHex") or set_decomposition.get("sourceRootHex"), "predecessorSelector": predecessor_selector.get("selector") or set_decomposition.get("predecessorSelector"), "predecessorRootHex": predecessor_selector.get("rootHex") or set_decomposition.get("predecessorRootHex"), "currentSelector": current_selector.get("selector") or set_decomposition.get("currentSelector"), "currentRootHex": current_selector.get("rootHex") or set_decomposition.get("currentRootHex"), "currentEqualsPredecessorPlusSource": current_equals_predecessor_plus_source, "currentEqualsSourcePredecessorUnion": current.get("currentEqualsSourcePredecessorUnion"), "sourcePredecessorUnionCoversCurrent": current.get("sourcePredecessorUnionCoversCurrent"), "sourcePredecessorUnionExtraMaps": current_source_predecessor_extra_maps, "routePairOnlyCurrentSelector": route_pair_only_current, "routePairSelectorCount": recomposition_lattice.get("routePairSelectorCount"), "currentExactPairUnionCount": exact_pair_union_count, "currentCoveringPairUnionCount": covering_pair_count, "globalExactPairUnionCount": recomposition_lattice.get("exactPairUnionCount"), "oneMapAugmentationCount": recomposition_lattice.get("oneMapAugmentationCount"), "sourceToCurrentBridgeHitCount": merge_gap.get("sourceToCurrentBridgeHitCount"), "currentToSourceBridgeHitCount": merge_gap.get("currentToSourceBridgeHitCount"), "predecessorToCurrentHitCount": merge_bridge_matrix.get("predecessorToCurrentHitCount"), "currentToPredecessorHitCount": merge_bridge_matrix.get("currentToPredecessorHitCount"), "currentToPredecessorBeforeFillHitCount": merge_bridge_matrix.get("currentToPredecessorBeforeFillHitCount"), "currentToPredecessorFillSiteHitCount": merge_bridge_matrix.get("currentToPredecessorFillSiteHitCount"), "forwardMergeBridgeHitCount": forward_merge_bridge_count, "directMergeExecutionBridgeFound": direct_merge_execution_bridge_found, "forwardEncodedAnchorRawScalarCandidateCount": forward_encoded_anchor_raw_count, "forwardEncodedAnchorPromotingCandidateCount": forward_encoded_anchor_promoting_count, "encodedMergeExecutionBridgeFound": encoded_merge_execution_bridge_found, "targetAliasSelectors": target_alias_bridges.get("targetAliasSelectors") or [], "targetAliasToCurrentHitCount": target_alias_bridges.get("aliasToCurrentHitCount"), "targetAliasToCurrentMetadataHitCount": target_alias_bridges.get("aliasToCurrentMetadataHitCount"), "targetAliasToCurrentDataHitCount": target_alias_bridges.get("aliasToCurrentDataHitCount"), "targetAliasToCurrentPromotingMetadataHitCount": target_alias_bridges.get( "aliasToCurrentPromotingMetadataHitCount" ), "targetAliasToCurrentPromotingDataHitCount": target_alias_bridges.get( "aliasToCurrentPromotingDataHitCount" ), "targetAliasToCurrentPromotingExactMetadataOnly": target_alias_bridges.get( "aliasToCurrentPromotingExactMetadataOnly" ), "targetAliasToCurrentAfterLastFillHitCount": target_alias_bridges.get( "aliasToCurrentAfterLastFillHitCount" ), "targetAliasForwardHitSelectors": target_alias_forward_hit_selectors, "targetAliasForwardDataSelectors": target_alias_forward_data_selectors, "targetAliasAfterLastFillDataSelectors": target_alias_after_fill_data_selectors, "targetAliasDominantDataSelectors": target_alias_dominant_data_selectors, "targetAliasPublicCoveredSelectors": target_alias_public_covered_selectors, "targetAliasPublicCoveredForwardHitSelectors": target_alias_public_forward_selectors, "targetAliasPublicCoveredForwardHitAliasCount": target_alias_bridges.get( "publicCoveredForwardHitAliasCount" ), "targetAliasForwardHitPublicSampleCount": target_alias_bridges.get( "forwardHitPublicSampleCount" ), "targetAliasAddressAdjacentForwardHitSelectors": target_alias_address_adjacent_forward_selectors, "targetAliasForwardHitsAddressAdjacentOnly": target_alias_bridges.get( "forwardHitsAddressAdjacentOnly" ), "targetAliasPublicForwardHitCoverageStatus": target_alias_forward_hit_coverage_status, "targetAliasExecutionExclusionStatus": target_alias_execution_exclusion_status, "targetAliasExecutionExclusionDetail": target_alias_execution_exclusion_detail, "targetAliasBridgeSummaryRows": target_alias_bridge_summary_rows, "targetAliasToCurrentExecutionLikeBridgeFound": target_alias_execution_bridge_found, "routeRootsTableOnly": route_roots_table_only, "routeRootExecutionRefFound": route_root_execution_ref_found, "sourceTargetSplitAcrossPreviousSelectors": route_root_ref_context.get( "sourceTargetSplitAcrossPreviousSelectors" ), "branchStateExecutionProofFound": branch_state_execution_proof_found, "selectorMergeExecutionProofFound": selector_merge_execution_proof_found, "runtimeOrControlFlowProofFound": runtime_or_control_flow_proof_found, "proofFound": proof_found, "strictHotspotFound": strict_hotspot_found, "failedSelectorMergeExecutionGateIds": failed_selector_merge_execution_gate_ids, "missingEvidence": missing_evidence, "evidenceRefs": SELECTOR_MERGE_EXECUTION_EVIDENCE_REFS, "evidenceRefCount": len(SELECTOR_MERGE_EXECUTION_EVIDENCE_REFS), "selectorMergeGapOpen": selector_merge_gap_open, "promotionStatus": promotion_status, "evidence": evidence, "remainingProofs": [ "prove source-side selector 0:0 enters current selector 2:0 in VM control flow", "prove target-side predecessor/alias state reaches current 2:0 reader execution", "capture selected-pointer runtime evidence or a real selector 2:0 savedata sample", "find a strict map1_01a source coordinate or hotspot", ], "conclusion": conclusion, } def markdown(summary: dict) -> str: lines = [ "# Save Selector Merge Execution Gap", "", summary["conclusion"], "", f"- route: `{summary['source']} -> {summary['target']}`", f"- source selector: `{summary['sourceSelector']}` root `{summary['sourceRootHex']}`", f"- predecessor selector: `{summary['predecessorSelector']}` root `{summary['predecessorRootHex']}`", f"- current selector: `{summary['currentSelector']}` root `{summary['currentRootHex']}`", f"- current equals predecessor plus source: {summary['currentEqualsPredecessorPlusSource']}", f"- source+predecessor extra maps: {csv(summary['sourcePredecessorUnionExtraMaps'])}", f"- route pair only current selector: {summary['routePairOnlyCurrentSelector']}", f"- current exact pair unions: {summary['currentExactPairUnionCount']}", f"- source/current bridge hits: {summary['sourceToCurrentBridgeHitCount']} / {summary['currentToSourceBridgeHitCount']}", f"- predecessor/current bridge hits: {summary['predecessorToCurrentHitCount']} / {summary['currentToPredecessorHitCount']}", f"- current->predecessor before-fill/fill-site hits: {summary['currentToPredecessorBeforeFillHitCount']} / {summary['currentToPredecessorFillSiteHitCount']}", f"- forward encoded-anchor raw/promoting candidates: {summary['forwardEncodedAnchorRawScalarCandidateCount']} / {summary['forwardEncodedAnchorPromotingCandidateCount']}", f"- encoded merge execution bridge found: {summary['encodedMergeExecutionBridgeFound']}", f"- target alias -> current hits: {summary['targetAliasToCurrentHitCount']}", f"- target alias promoting metadata/data hits: {summary['targetAliasToCurrentPromotingMetadataHitCount']} / {summary['targetAliasToCurrentPromotingDataHitCount']}", f"- target alias exact promoting hits metadata-only: {summary['targetAliasToCurrentPromotingExactMetadataOnly']}", f"- target alias forward/data/after-fill-data selectors: {csv(summary['targetAliasForwardHitSelectors'])} / {csv(summary['targetAliasForwardDataSelectors'])} / {csv(summary['targetAliasAfterLastFillDataSelectors'])}", f"- target alias public-covered forward selectors: {csv(summary['targetAliasPublicCoveredForwardHitSelectors'])}", f"- target alias address-adjacent forward selectors: {csv(summary['targetAliasAddressAdjacentForwardHitSelectors'])}", f"- target alias public coverage/exclusion: `{summary['targetAliasPublicForwardHitCoverageStatus']}` / `{summary['targetAliasExecutionExclusionStatus']}`", f"- target alias execution-like bridge found: {summary['targetAliasToCurrentExecutionLikeBridgeFound']}", f"- route root execution ref found: {summary['routeRootExecutionRefFound']}", f"- branch-state execution proof found: {summary['branchStateExecutionProofFound']}", f"- selector merge execution proof found: {summary['selectorMergeExecutionProofFound']}", f"- proof found: {summary['proofFound']}", f"- failed selector-merge execution gates: {csv(summary.get('failedSelectorMergeExecutionGateIds'))}", f"- missing evidence count: {len(summary.get('missingEvidence') or [])}", f"- evidence refs: {summary.get('evidenceRefCount')}", f"- selector merge gap open: {summary['selectorMergeGapOpen']}", 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([ "", "## Target Alias Bridge Summary", "", "| selector | role | hits | data | after-fill data | classes | after-fill classes | trace W/R/S | current->alias |", "| --- | --- | ---: | ---: | ---: | --- | --- | --- | ---: |", ]) for row in summary["targetAliasBridgeSummaryRows"]: classes = class_counts_text(row.get("aliasToCurrentTargetClassCounts")) after_classes = class_counts_text(row.get("aliasToCurrentAfterLastFillTargetClassCounts")) lines.append( f"| `{row.get('selector')}` | {row.get('role')} | {row.get('aliasToCurrentHitCount')} | " f"{row.get('aliasToCurrentDataHitCount')} | {row.get('aliasToCurrentAfterLastFillDataHitCount')} | " f"{classes} | {after_classes} | " f"{row.get('aliasToCurrentPreWriterTraceCurrentWriterHitCount')}/" f"{row.get('aliasToCurrentPreWriterTraceCurrentReaderHitCount')}/" f"{row.get('aliasToCurrentPreWriterTraceRouteSceneRecordHitCount')} | " f"{row.get('currentToAliasHitCount')} |" ) 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( "" f"{html.escape(row['kind'])}" f"{html.escape(row['status'])}" f"{html.escape(row['detail'])}" "" for row in summary["evidence"] ) proof_items = "\n".join(f"
  • {html.escape(item)}
    • " for item in summary["remainingProofs"]) missing_items = "\n".join( f"
  • {html.escape(item)}
    • " for item in summary.get("missingEvidence") or [] ) return "\n".join( [ "", '', "", ' ', " Save Selector Merge Execution Gap", " ", "", "", "

    Save Selector Merge Execution Gap

    ", f"

    {html.escape(summary['conclusion'])}

    ", ( "

    Route: " f"{html.escape(summary['source'])} -> {html.escape(summary['target'])}; " f"source {html.escape(str(summary['sourceSelector']))} " f"root {html.escape(str(summary['sourceRootHex']))}; " f"predecessor {html.escape(str(summary['predecessorSelector']))} " f"root {html.escape(str(summary['predecessorRootHex']))}; " f"current {html.escape(str(summary['currentSelector']))} " f"root {html.escape(str(summary['currentRootHex']))}.

    " ), ( "

    Proof: " f"mergeShape={summary['currentEqualsPredecessorPlusSource']}; " f"exactPairUnions={summary['currentExactPairUnionCount']}; " f"directMergeExecution={summary['directMergeExecutionBridgeFound']}; " f"encodedMergeExecution={summary['encodedMergeExecutionBridgeFound']}; " f"routeRootExecution={summary['routeRootExecutionRefFound']}; " f"branchStateExecution={summary['branchStateExecutionProofFound']}; " f"proofFound={summary['proofFound']}; " "failedSelectorMergeExecutionGates=" f"{html.escape(csv(summary.get('failedSelectorMergeExecutionGateIds')))}; " f"missingEvidenceCount={len(summary.get('missingEvidence') or [])}; " f"evidenceRefs={summary.get('evidenceRefCount')}; " f"status {html.escape(summary['promotionStatus'])}.

    " ), ( "

    selector merge execution proof found: " f"{summary['selectorMergeExecutionProofFound']}; " "selector merge gap open: " f"{summary['selectorMergeGapOpen']}; " "promotion status: " f"{html.escape(summary['promotionStatus'])}.

    " ), ( "

    target alias forward/data/after-fill-data selectors: " f"forwardHitAliases={html.escape(csv(summary['targetAliasForwardHitSelectors']))}; " f"dataAliases={html.escape(csv(summary['targetAliasForwardDataSelectors']))}; " f"afterFillDataAliases={html.escape(csv(summary['targetAliasAfterLastFillDataSelectors']))}.

    " ), ( "

    target alias public-covered forward selectors; target alias address-adjacent forward selectors; target alias public coverage/exclusion: " f"publicForward={html.escape(csv(summary['targetAliasPublicCoveredForwardHitSelectors']))}; " f"addressAdjacentForward={html.escape(csv(summary['targetAliasAddressAdjacentForwardHitSelectors']))}; " f"coverage {html.escape(str(summary['targetAliasPublicForwardHitCoverageStatus']))}; " f"exclusion {html.escape(str(summary['targetAliasExecutionExclusionStatus']))}.

    " ), ( "

    target alias promoting metadata/data hits: " f"{summary['targetAliasToCurrentPromotingMetadataHitCount']} / " f"{summary['targetAliasToCurrentPromotingDataHitCount']}.

    " ), ( "

    target alias exact promoting hits metadata-only: " f"{summary['targetAliasToCurrentPromotingExactMetadataOnly']}.

    " ), "

    Missing Evidence

    ", f" ", "

    Evidence

    ", f" {evidence_rows}
    kindstatusdetail
    ", "

    Target Alias Bridge Summary

    ", " ", "\n".join( "" f"" f"" f"" f"" f"" f"" f"" f"" f"" "" for row in summary["targetAliasBridgeSummaryRows"] ), "
    selectorrolehitsdataafter-fill dataclassesafter-fill classestrace W/R/Scurrent->alias
    {html.escape(str(row.get('selector')))}{html.escape(str(row.get('role')))}{row.get('aliasToCurrentHitCount')}{row.get('aliasToCurrentDataHitCount')}{row.get('aliasToCurrentAfterLastFillDataHitCount')}{html.escape(class_counts_text(row.get('aliasToCurrentTargetClassCounts')))}{html.escape(class_counts_text(row.get('aliasToCurrentAfterLastFillTargetClassCounts')))}{row.get('aliasToCurrentPreWriterTraceCurrentWriterHitCount')}/" f"{row.get('aliasToCurrentPreWriterTraceCurrentReaderHitCount')}/" f"{row.get('aliasToCurrentPreWriterTraceRouteSceneRecordHitCount')}{row.get('currentToAliasHitCount')}
    ", "

    Remaining Proofs

    ", f" ", "", "", "", ] ) def write_outputs(summary: dict, out_dir: Path = OUT) -> None: out_dir.mkdir(parents=True, exist_ok=True) (out_dir / "save_selector_merge_execution_gap.json").write_text( json.dumps(summary, ensure_ascii=False, indent=2) + "\n", encoding="utf-8", ) (out_dir / "save_selector_merge_execution_gap.html").write_text(html_page(summary), encoding="utf-8") def load_json(path: Path) -> dict: return json.loads(path.read_text(encoding="utf-8")) def main() -> None: parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("--set-decomposition", type=Path, default=OUT / "save_selector_set_decomposition.json") parser.add_argument("--recomposition-lattice", type=Path, default=OUT / "save_selector_recomposition_lattice.json") parser.add_argument("--merge-gap", type=Path, default=OUT / "save_selector_merge_gap.json") parser.add_argument("--merge-bridge-matrix", type=Path, default=OUT / "save_selector_merge_bridge_matrix.json") parser.add_argument("--target-alias-bridges", type=Path, default=OUT / "save_selector_target_alias_bridges.json") parser.add_argument("--route-root-ref-context", type=Path, default=OUT / "save_selector_route_root_ref_context.json") parser.add_argument( "--predecessor-branch-state-execution-gap", type=Path, default=OUT / "save_selector_predecessor_branch_state_execution_gap.json", ) parser.add_argument("--out-dir", type=Path, default=OUT) args = parser.parse_args() summary = build_summary( load_json(args.set_decomposition), load_json(args.recomposition_lattice), load_json(args.merge_gap), load_json(args.merge_bridge_matrix), load_json(args.target_alias_bridges), load_json(args.route_root_ref_context), load_json(args.predecessor_branch_state_execution_gap), ) write_outputs(summary, args.out_dir) print(f"wrote selector merge execution gap -> {args.out_dir / 'save_selector_merge_execution_gap.html'}") if __name__ == "__main__": main()