#!/usr/bin/env python3 """Apply the current-reader branch-state equation to target-side selector aliases.""" 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" CURRENT_SELECTOR = "2:0" CURRENT_WRITER = "0x005428bc" CURRENT_READER = "0x00542b0c" PASS_FILL_VALUE = "0x00000210" PASS_TABLE = [1, 1] + [0] * 10 ZERO_TABLE = [0] * 12 def load_json(path: Path, fallback: Any) -> Any: if not path.exists(): return fallback return json.loads(path.read_text(encoding="utf-8")) def simulate_opcode12_selected_slot(table: list[int], start: int) -> int: slot = start & 0xFF for _ in range(12): slot = slot - 1 if slot else 0x0B if table[slot]: break for _ in range(12): slot = 0 if slot + 1 >= 0x0C else slot + 1 if table[slot]: break return slot def outcome_rows(table: list[int]) -> list[dict]: rows = [] for start in range(12): selected = simulate_opcode12_selected_slot(table, start) rows.append({ "startSlot": start, "selectedSlot": selected, "selectedValue": table[selected], "frontierReaderFallsThrough": table[selected] == 1, }) return rows def root_fills_by_hex(secondary_fill_roots: dict) -> dict[str, list[dict]]: return { row.get("rootHex"): row.get("fills") or [] for row in secondary_fill_roots.get("roots") or [] if row.get("rootHex") } def state_table_for_fills(fills: list[dict]) -> tuple[list[int] | None, str]: if not fills: return None, "no-fill-proof" values = {row.get("valueHex") for row in fills} if values == {PASS_FILL_VALUE}: return list(PASS_TABLE), "all-fills-produce-pass-prefix" return None, "unmodeled-fill-values" def build_summary(mapset_aliases: dict, secondary_fill_roots: dict) -> dict: fills_by_root = root_fills_by_hex(secondary_fill_roots) alias_rows = [] for alias in (mapset_aliases.get("targetAliasGroup") or {}).get("aliases") or []: root_hex = alias.get("rootHex") fills = fills_by_root.get(root_hex, []) table, effect_status = state_table_for_fills(fills) outcomes = outcome_rows(table) if table is not None else [] alias_rows.append({ "selector": alias.get("selector"), "role": alias.get("role"), "rootHex": root_hex, "rootAddressOrderIndex": alias.get("rootAddressOrderIndex"), "publicSampleIds": alias.get("publicSampleIds") or [], "fillCount": len(fills), "firstFillHex": (fills[0] or {}).get("vaHex") if fills else None, "lastFillHex": (fills[-1] or {}).get("vaHex") if fills else None, "uniqueFillValuesHex": sorted({row.get("valueHex") for row in fills if row.get("valueHex")}), "stateEffectStatus": effect_status, "secondaryBranchStateAfterLastModeledFill": table, "allStartSlotsPassCurrentReader": all(row["frontierReaderFallsThrough"] for row in outcomes) if outcomes else False, "passingStartSlotCount": sum(1 for row in outcomes if row["frontierReaderFallsThrough"]), "outcomes": outcomes, }) pass_aliases = [ row["selector"] for row in alias_rows if row.get("allStartSlotsPassCurrentReader") ] no_fill_aliases = [ row["selector"] for row in alias_rows if row.get("stateEffectStatus") == "no-fill-proof" ] conclusion = ( "Target-side aliases 1:0 and 10:0 both contain only modeled 0x00000210 secondaryBranchState fills, so if either " "alias actually executes and its state persists into current selector 2:0, the current 0x005428bc writer would select " "a passing slot for every possible start value before reader 0x00542b0c. Alias 17:0 has no modeled fill rows. " "This narrows the value side of the branch-state equation across target aliases, but it still does not prove which " "alias executes, that the state persists across roots, that the gated path reaches the reader, or that " "map1_01a has a strict source hotspot." ) return { "source": SOURCE, "target": TARGET, "currentSelector": CURRENT_SELECTOR, "currentWriterVaHex": CURRENT_WRITER, "currentReaderVaHex": CURRENT_READER, "targetAliasSelectors": [row.get("selector") for row in alias_rows], "targetAliasCount": len(alias_rows), "modeledPassFillValueHex": PASS_FILL_VALUE, "modeledPassTable": PASS_TABLE, "zeroTableControlOutcomes": outcome_rows(ZERO_TABLE), "aliasRows": alias_rows, "aliasesThatWouldPassIfExecutedAndPersisted": pass_aliases, "aliasPassCount": len(pass_aliases), "aliasesWithoutFillProof": no_fill_aliases, "aliasNoFillProofCount": len(no_fill_aliases), "allTargetAliasesHaveFillProof": len(no_fill_aliases) == 0 and len(pass_aliases) == len(alias_rows), "promotionStatus": "blocked", "remainingProofs": [ "prove which target-side alias actually executes before current selector 2:0", "prove secondaryBranchState persists into the 0x00542b0c reader", "prove the gated control path reaches 0x00542b0c", "find a strict map1_01a source hotspot or equivalent original transition trigger", ], "conclusion": conclusion, } def markdown(summary: dict) -> str: lines = [ "# Save Selector Target Alias State Effects", "", f"- route: `{summary['source']}` -> `{summary['target']}`", f"- current writer/reader: `{summary['currentWriterVaHex']}` / `{summary['currentReaderVaHex']}`", f"- target aliases: `{', '.join(summary['targetAliasSelectors'])}`", f"- modeled pass fill: `{summary['modeledPassFillValueHex']}`", f"- aliases that would pass if executed and persisted: `{', '.join(summary['aliasesThatWouldPassIfExecutedAndPersisted']) or '-'}`", f"- aliases without fill proof: `{', '.join(summary['aliasesWithoutFillProof']) or '-'}`", f"- all target aliases have fill proof: {summary['allTargetAliasesHaveFillProof']}", f"- promotion status: `{summary['promotionStatus']}`", "", summary["conclusion"], "", "## Alias Effects", "", "| selector | role | root | fills | fill values | pass starts | public samples | status |", "| --- | --- | --- | ---: | --- | ---: | --- | --- |", ] for row in summary["aliasRows"]: lines.append( f"| `{row['selector']}` | {row['role']} | `{row['rootHex']}` | {row['fillCount']} | " f"`{', '.join(row['uniqueFillValuesHex']) or '-'}` | {row['passingStartSlotCount']}/12 | " f"`{', '.join(row['publicSampleIds']) or '-'}` | `{row['stateEffectStatus']}` |" ) 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: rows = "\n".join( "" f"{html.escape(str(row['selector']))}" f"{html.escape(str(row['role']))}" f"{html.escape(str(row['rootHex']))}" f"{html.escape(str(row['fillCount']))}" f"{html.escape(', '.join(row['uniqueFillValuesHex']) or '-')}" f"{html.escape(str(row['passingStartSlotCount']))}/12" f"{html.escape(', '.join(row['publicSampleIds']) or '-')}" f"{html.escape(str(row['stateEffectStatus']))}" "" for row in summary["aliasRows"] ) proofs = "".join(f"
  • {html.escape(item)}
    • " for item in summary["remainingProofs"]) return "\n".join([ "Save Selector Target Alias State Effects", "", "

    Save Selector Target Alias State Effects

    ", "", f"

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

    ", "

    Alias Effects

    ", "", rows, "
    selectorrolerootfillsfill valuespass startspublic samplesstatus
    ", "

    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_target_alias_state_effects.json").write_text( json.dumps(summary, ensure_ascii=False, indent=2) + "\n", encoding="utf-8", ) (out_dir / "save_selector_target_alias_state_effects.html").write_text(html_page(summary), encoding="utf-8") def main() -> None: parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("--mapset-aliases", type=Path, default=OUT / "save_selector_mapset_aliases.json") parser.add_argument("--secondary-fill-roots", type=Path, default=OUT / "save_selector_secondary_fill_roots.json") parser.add_argument("--out-dir", type=Path, default=OUT) args = parser.parse_args() summary = build_summary( load_json(args.mapset_aliases, {}), load_json(args.secondary_fill_roots, {}), ) write_outputs(summary, args.out_dir) print(f"wrote target alias state effects -> {args.out_dir / 'save_selector_target_alias_state_effects.html'}") if __name__ == "__main__": main()