diff --git a/.github/workflows/c6-residual-closure.yml b/.github/workflows/c6-residual-closure.yml index be39b64ba..1bde9c3b3 100644 --- a/.github/workflows/c6-residual-closure.yml +++ b/.github/workflows/c6-residual-closure.yml @@ -34,7 +34,7 @@ jobs: - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 with: python-version: '3.11.16' - - name: Verify sources, replay both modes, reject mutants + - name: Verify sources, replay both modes (baseline or installed register), reject mutants env: PYTHONDONTWRITEBYTECODE: '1' run: | @@ -55,13 +55,16 @@ jobs: if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: raise ValueError('source identity mismatch: ' + entry['path']) script = str(root / 'residual_check.py') - expected = (root / 'RESULTS.json').read_bytes() - mutants = ['allow-symlink', 'no-hash', 'stale-fingerprint', 'drop-required-edge', 'executed-flag', 'controlling-true', 'tail-reversed', 'pair-identity-broken', 'route-c-broken', 'drop-review-needle', 'installed-drift', 'snapshot-omitted', 'record-unreviewed', 'reviewed-text-drift'] + mutants = ['partial-install', 'allow-symlink', 'no-hash', 'stale-fingerprint', 'drop-required-edge', 'executed-flag', 'controlling-true', 'tail-reversed', 'pair-identity-broken', 'route-c-broken', 'drop-review-needle', 'installed-drift', 'snapshot-omitted', 'record-unreviewed', 'reviewed-text-drift'] for flags in (['-B', '-S'], ['-B', '-O', '-S']): out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=300).stdout - if out != expected: - raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + state = json.loads(out).get('register_state') + if state not in ('baseline', 'installed'): + raise RuntimeError('checker reports register_state ' + repr(state)) + pinned = 'RESULTS.json' if state == 'baseline' else 'RESULTS_INSTALLED.json' + if out != (root / pinned).read_bytes(): + raise RuntimeError('output differs from ' + pinned + ' under ' + ' '.join(flags)) for m in mutants: rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=300).returncode diff --git a/.github/workflows/c6-witness-collision-reconciliation.yml b/.github/workflows/c6-witness-collision-reconciliation.yml index adc6c7d16..1f74fb0ca 100644 --- a/.github/workflows/c6-witness-collision-reconciliation.yml +++ b/.github/workflows/c6-witness-collision-reconciliation.yml @@ -36,7 +36,7 @@ jobs: - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 with: python-version: '3.11.16' - - name: Verify sources, replay both modes, reject mutants + - name: Verify sources, replay both modes (baseline or installed register), reject mutants env: PYTHONDONTWRITEBYTECODE: '1' run: | @@ -57,13 +57,16 @@ jobs: if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: raise ValueError('source identity mismatch: ' + entry['path']) script = str(root / 'reconciliation_check.py') - expected = (root / 'RESULTS.json').read_bytes() - mutants = ['allow-symlink', 'no-hash', 'drop-edge', 'stale-fingerprint', 'executed-flag', 'close-residual', 'drop-lower-bound', 'regional-strict', 'clone-live-node', 'open-cell-left'] + mutants = ['allow-symlink', 'no-hash', 'drop-edge', 'stale-fingerprint', 'executed-flag', 'close-residual', 'drop-lower-bound', 'regional-strict', 'clone-live-node', 'open-cell-left', 'installed-drift', 'partial-install', 'selector-ahead', 'witness-edges-partial'] for flags in (['-B', '-S'], ['-B', '-O', '-S']): out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=300).stdout - if out != expected: - raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + state = json.loads(out).get('register_state') + if state not in ('baseline', 'installed'): + raise RuntimeError('checker reports register_state ' + repr(state)) + pinned = 'RESULTS.json' if state == 'baseline' else 'RESULTS_INSTALLED.json' + if out != (root / pinned).read_bytes(): + raise RuntimeError('output differs from ' + pinned + ' under ' + ' '.join(flags)) for m in mutants: rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=300).returncode diff --git a/.github/workflows/register-alignment.yml b/.github/workflows/register-alignment.yml index e8d30be7f..ac806471c 100644 --- a/.github/workflows/register-alignment.yml +++ b/.github/workflows/register-alignment.yml @@ -37,7 +37,7 @@ jobs: - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 with: python-version: '3.11.16' - - name: Verify sources, replay both modes, reject mutants + - name: Verify sources, replay both modes (baseline or installed register), reject mutants env: PYTHONDONTWRITEBYTECODE: '1' run: | @@ -58,13 +58,16 @@ jobs: if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: raise ValueError('source identity mismatch: ' + entry['path']) script = str(root / 'alignment_check.py') - expected = (root / 'RESULTS.json').read_bytes() - mutants = ['allow-symlink', 'no-hash', 'stale-fingerprint', 'drop-review-source', 'controlling-true', 'executed-flag', 'skip-interface-premise', 'holder-reversed', 'baseline-drift', 'duplicate-drift', 'region-unlinked', 'review-metadata-only'] + mutants = ['allow-symlink', 'no-hash', 'stale-fingerprint', 'drop-review-source', 'controlling-true', 'executed-flag', 'skip-interface-premise', 'holder-reversed', 'baseline-drift', 'duplicate-drift', 'region-unlinked', 'review-metadata-only', 'installed-drift', 'partial-install', 'text-preinstalled'] for flags in (['-B', '-S'], ['-B', '-O', '-S']): out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=300).stdout - if out != expected: - raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + state = json.loads(out).get('register_state') + if state not in ('baseline', 'installed'): + raise RuntimeError('checker reports register_state ' + repr(state)) + pinned = 'RESULTS.json' if state == 'baseline' else 'RESULTS_INSTALLED.json' + if out != (root / pinned).read_bytes(): + raise RuntimeError('output differs from ' + pinned + ' under ' + ' '.join(flags)) for m in mutants: rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=300).returncode diff --git a/.github/workflows/register-execution-readiness.yml b/.github/workflows/register-execution-readiness.yml new file mode 100644 index 000000000..95ff83606 --- /dev/null +++ b/.github/workflows/register-execution-readiness.yml @@ -0,0 +1,38 @@ +name: Register execution readiness + +'on': + pull_request: + paths: + - 'reviews/register_execution_readiness_20260930/**' + - '.github/workflows/register-execution-readiness.yml' + - 'reviews/register_alignment_20260930/**' + - 'reviews/c6_witness_collision_reconciliation_20260929/**' + - 'reviews/c6_residual_closure_20260930/**' + - 'frontiers/downstream_gate_20260925/GRAPH.json' + - 'frontiers/downstream_gate_20260925/SELECTOR_REGION.json' + - 'frontiers/downstream_gate_20260925/hard_gate.py' + workflow_dispatch: + +permissions: + contents: read + +jobs: + compose-and-check: + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Compose the three proposals on a scratch copy; run the three checkers and their mutants in the installed state + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S reviews/register_execution_readiness_20260930/execution_dryrun.py --mutants + python -B -S reviews/register_execution_readiness_20260930/execution_dryrun.py --skip-old-node-move + python -B -S reviews/register_execution_readiness_20260930/execution_dryrun.py --selector-node-only + git diff --exit-code diff --git a/reviews/c6_residual_closure_20260930/PROPOSED_TRANSITIONS.json b/reviews/c6_residual_closure_20260930/PROPOSED_TRANSITIONS.json index 3706e8ac4..02f7a3708 100644 --- a/reviews/c6_residual_closure_20260930/PROPOSED_TRANSITIONS.json +++ b/reviews/c6_residual_closure_20260930/PROPOSED_TRANSITIONS.json @@ -278,7 +278,7 @@ "component_of": "math.rn-region.witness-collision.leading-mass-localization", "component_role": "reading_rule_record", "author_provider": "Anthropic Claude (this session; source-exposed, see section 0)", - "fingerprint": "b647a186d0cfd1662fc69e9d31dfd447dbb1b2f6ef4364bbd59c4956f18aed25", + "fingerprint": "60ed9ca2df666bc31cf50dc1fc7f3f8e8527d5efe4b16c265c205e1e9d1e6b34", "source": "reviews/c6_residual_closure_20260930/RECONCILIATION.md", "scope": "section 3: the corollary (D1) + steps 1-3 (Route A) and Route B, read by 5360645884 at b3fac79 and preserved verbatim in REVIEWED_SECTION_3_b3fac79.md; Route C (OpenAI-authored, checked 5902616692)", "review_basis": [ diff --git a/reviews/c6_residual_closure_20260930/RECONCILIATION.md b/reviews/c6_residual_closure_20260930/RECONCILIATION.md index 3cfd17c5e..9668d06a4 100644 --- a/reviews/c6_residual_closure_20260930/RECONCILIATION.md +++ b/reviews/c6_residual_closure_20260930/RECONCILIATION.md @@ -19,7 +19,15 @@ review 5360227991; v1.3 at `fe2c3ff` answers Math-#173's reviews: this record's path (OpenAI / GPT-5.6 Sol 5360645884, a non-Claude bounded read of §3 at head `b3fac79`, whose paragraphs are preserved verbatim in `REVIEWED_SECTION_3_b3fac79.md` and checked unchanged), the two evidence paths are modelled separately, and the checker accepts the installed state and replays the hard gate with source snapshots (Codex 5360636576); v1.4 at -`8d48d02` re-verifies after Math-#160 merged (no content change); v1.5 at `02772ec` applies the direct-statement amendment +`8d48d02` re-verifies after Math-#160 merged (no content change); v1.6 at `dda8991` (register execution readiness, +`reviews/register_execution_readiness_20260930`) keeps the installed-state simulation and its `installed-drift` mutant active on the installed +register too (before, the mutant was a no-op once the residual was live `PROVED_REVIEWED`, so the workflow's mutant rule +would have failed after execution), prints `register_state`, and the workflow compares the checker's output with +`RESULTS.json` in the baseline state and with `RESULTS_INSTALLED.json` in the installed state (the per-stage gate report +differs between the two by construction); after Codex review 5365065925 on Math-#183 (thread 4143661501) `LIVE` accepts +exactly two register states, baseline (residual absent or `OPEN_ACTIVE`, none of this record's edges, no component but +the cross-record palm node) and installed, so partial installs fail and the interim shape is a replay, not an accepted +live state (mutant `partial-install`); no other content changes; v1.5 at `02772ec` applies the direct-statement amendment of review 5360751376 (the diagonal argument; no fixed-`R` substitution into (L1)) and records that review's ACCEPT of Route C. Pickup: Math-#160 comment 5902470285; delivery 5902585446. @@ -260,7 +268,10 @@ therefore reaches the residual through the graph, not through the fingerprint st classification, controlling); anything else on such a source, or anything else under a proposed id, is a mismatch. If the residual is live `PROVED_REVIEWED`, every component, every edge and the reading rule must be present as proposed. The same test runs on the executed graph built from the proposal (installed state, simulated) in every run, so that - execution cannot turn this check red (Codex 4140125558). + execution cannot turn this check red (Codex 4140125558); on the installed register that simulation is the live graph + itself (v1.6). The live register must be baseline (residual absent or `OPEN_ACTIVE`, none of this record's edges, no + component except the cross-record palm node) or installed; anything else, the interim shape included, fails; the + installed graph without one component is asserted partial in every run (v1.6). - **REVIEWED.** The record node's first review basis is Math-#173 review 5360645884 (provider OpenAI, ACCEPT, head `b3fac79`); `REVIEWED_SECTION_3_b3fac79.md`, after its one-line provenance comment, has the SHA256 the proposal states, begins at the §3 heading, contains Route A and Route B and not Route C, and is a verbatim substring of the current @@ -288,11 +299,16 @@ therefore reaches the residual through the graph, not through the fingerprint st component; the deferred old-node transition is not applied (its presupposition is absent live) and is reported. - **NEGATIVES.** Delete, one-byte change, symlink and symlinked parent on a temporary copy of the inventory are rejected. -Fourteen mutants must fail: `allow-symlink`, `no-hash`, `stale-fingerprint`, `drop-required-edge`, `executed-flag`, +Fifteen mutants must fail: `partial-install` (partial installs labelled baseline), `allow-symlink`, `no-hash`, +`stale-fingerprint`, `drop-required-edge`, `executed-flag`, `controlling-true`, `tail-reversed`, `pair-identity-broken`, `route-c-broken`, `drop-review-needle`, and since v1.3 `installed-drift` (an installed component with another fingerprint must fail `LIVE`), `snapshot-omitted` (the reverse-impact replay without snapshots must fail `GATE`), `record-unreviewed` (the record node `PROVED_REVIEWED` with no review basis must fail `TRANSITIONS` and `REVIEWED`), `reviewed-text-drift` (a changed reviewed text must fail `REVIEWED`). +The workflow runs the checker in the state the repository is in: it compares the output with `RESULTS.json` when the +checker reports `register_state: baseline` and with `RESULTS_INSTALLED.json` when it reports `installed`; the mutants +must be rejected in either state (the composition of Math-#167, #160 and #173 on a scratch copy, with every mutant, is +replayed by `reviews/register_execution_readiness_20260930`). ## 7. Relation to other lanes diff --git a/reviews/c6_residual_closure_20260930/RESULTS.json b/reviews/c6_residual_closure_20260930/RESULTS.json index 986a13200..33f5f3e4e 100644 --- a/reviews/c6_residual_closure_20260930/RESULTS.json +++ b/reviews/c6_residual_closure_20260930/RESULTS.json @@ -224,9 +224,11 @@ "edges_present": false, "mismatched": [], "present": [], - "residual": null + "residual": null, + "state": "baseline" }, "object": "C6-RESIDUAL-CLOSURE-20260930-v1", "passed": true, + "register_state": "baseline", "scope": "identity, verdict-row, live-register (including the installed state), reviewed-text, exact finite bookkeeping of section 3, transition-shape, hard-gate replay with source snapshots in every execution shape, and filesystem-negative checks; the Gaussian limits are the sources' reviewed statements and are not re-proved; nothing is written" } diff --git a/reviews/c6_residual_closure_20260930/RESULTS_INSTALLED.json b/reviews/c6_residual_closure_20260930/RESULTS_INSTALLED.json new file mode 100644 index 000000000..dba346ea7 --- /dev/null +++ b/reviews/c6_residual_closure_20260930/RESULTS_INSTALLED.json @@ -0,0 +1,47 @@ +{ + "checks": { + "DEDUCTION": true, + "GATE": true, + "IDENTITIES": true, + "LIVE": true, + "NEGATIVES": true, + "REVIEWED": true, + "TRANSITIONS": true, + "VERDICTS": true + }, + "component_nodes": 10, + "gate": { + "installed": { + "changed_nodes": [], + "impacted": [], + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)", + "residual_classification": "PROVED_REVIEWED", + "residual_held": false, + "source_drift_reaches_residual": 10, + "source_snapshots_supplied": true + } + }, + "inventory_files": 13, + "live_state": { + "edges_present": true, + "mismatched": [], + "present": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record" + ], + "residual": "PROVED_REVIEWED", + "state": "installed" + }, + "object": "C6-RESIDUAL-CLOSURE-20260930-v1", + "passed": true, + "register_state": "installed", + "scope": "identity, verdict-row, live-register (including the installed state), reviewed-text, exact finite bookkeeping of section 3, transition-shape, hard-gate replay with source snapshots in every execution shape, and filesystem-negative checks; the Gaussian limits are the sources' reviewed statements and are not re-proved; nothing is written" +} diff --git a/reviews/c6_residual_closure_20260930/SOURCE_FILES.json b/reviews/c6_residual_closure_20260930/SOURCE_FILES.json index 692bb2b78..23ea8cbc8 100644 --- a/reviews/c6_residual_closure_20260930/SOURCE_FILES.json +++ b/reviews/c6_residual_closure_20260930/SOURCE_FILES.json @@ -16,32 +16,38 @@ { "path": "PROPOSED_TRANSITIONS.json", "bytes": 31461, - "sha256": "78a50b82fd9cbf04899aa5ddc62875850ce68b8b5a5babfb637b7db7e2a49c5c", - "git_blob": "3706e8ac4e906aa1b53cdf5634abfb324c35a9e3" + "sha256": "7c4348b36f2024a5035cb85c8bed45f4977665f3786463ac519cb434e9869956", + "git_blob": "02f7a370849bace78ad29fac7ed8a449e28e08d8" }, { "path": "RECONCILIATION.md", - "bytes": 34758, - "sha256": "b647a186d0cfd1662fc69e9d31dfd447dbb1b2f6ef4364bbd59c4956f18aed25", - "git_blob": "3cfd17c5ef0356dbd3e8f98a2d08cb404ddd982c" + "bytes": 36574, + "sha256": "60ed9ca2df666bc31cf50dc1fc7f3f8e8527d5efe4b16c265c205e1e9d1e6b34", + "git_blob": "9668d06a41e14057fe6e03ac1bf469aa1ed18580" }, { "path": "RESULTS.json", - "bytes": 10376, - "sha256": "3c61cc49155cae7bba0fec30c0bf0a9fb085340f3a161d5898c527b87f9b5805", - "git_blob": "986a1320098b37238f117280b7925c683ca7c3c2" + "bytes": 10433, + "sha256": "705722ac0464ab8fdaa7882806702515ccdcb400f43647c72803e757290e9011", + "git_blob": "33f5f3e4ed20792ff00572caa76b75c7cf5fc225" }, { "path": "residual_check.py", - "bytes": 33664, - "sha256": "76ebda22aef26a70ab8ef5916e64bc7c5b3b34833fa702664fa00a7b4c1c4406", - "git_blob": "2667d4b35baa674c74c051244febb7f08118c572" + "bytes": 35124, + "sha256": "fbe11e898e939603bd5be118e57fe6b2d361d480aaaab4dd3e88f46c436f41b2", + "git_blob": "e7dabcb174d5c86aadf3ae727f60623ca28f3bf4" }, { "path": "REVIEWED_SECTION_3_b3fac79.md", "bytes": 3157, "sha256": "50daacbe7e244bc149dbf4568970d79f38a356daa1e88a850f2fc2d074db5b6c", "git_blob": "2fff7c277b43fa8e967ce9a8d70cf01a69e5eee4" + }, + { + "path": "RESULTS_INSTALLED.json", + "bytes": 1708, + "sha256": "8c085f1772a8bd92f4bb1df2aadefc3f3809e5da2b5552e9f1209719451304e6", + "git_blob": "dba346ea742c50305f321fac9ac2063593e2f083" } ] } diff --git a/reviews/c6_residual_closure_20260930/residual_check.py b/reviews/c6_residual_closure_20260930/residual_check.py index 2667d4b35..e7dabcb17 100644 --- a/reviews/c6_residual_closure_20260930/residual_check.py +++ b/reviews/c6_residual_closure_20260930/residual_check.py @@ -19,7 +19,7 @@ import tempfile from fractions import Fraction as F -MUTANTS = ("allow-symlink", "no-hash", "stale-fingerprint", "drop-required-edge", "executed-flag", "controlling-true", +MUTANTS = ("partial-install", "allow-symlink", "no-hash", "stale-fingerprint", "drop-required-edge", "executed-flag", "controlling-true", "tail-reversed", "pair-identity-broken", "route-c-broken", "drop-review-needle", "installed-drift", "snapshot-omitted", "record-unreviewed", "reviewed-text-drift") MUT = None @@ -72,8 +72,8 @@ "70d05080ed81c66b43261438cae3b9ec2840e637" ], "reviews/c6_residual_closure_20260930/RECONCILIATION.md": [ - "b647a186d0cfd1662fc69e9d31dfd447dbb1b2f6ef4364bbd59c4956f18aed25", - "3cfd17c5ef0356dbd3e8f98a2d08cb404ddd982c" + "60ed9ca2df666bc31cf50dc1fc7f3f8e8527d5efe4b16c265c205e1e9d1e6b34", + "9668d06a41e14057fe6e03ac1bf469aa1ed18580" ], "reviews/c6_residual_closure_20260930/REVIEWED_SECTION_3_b3fac79.md": [ "50daacbe7e244bc149dbf4568970d79f38a356daa1e88a850f2fc2d074db5b6c", @@ -239,9 +239,21 @@ def installed_state(graph, spec): live_edges = {(e["from"], e["to"], e["required"], e["relation"]) for e in graph["edges"]} wanted = {(e["from"], e["to"], e["required"], e["relation"]) for e in spec["proposed_graph_edges"] if not e.get("deferred_with")} - return {"present": sorted(present), "mismatched": sorted(mismatched), - "residual": res.get("classification") if isinstance(res, dict) else None, - "edges_present": wanted <= live_edges} + res_cls = res.get("classification") if isinstance(res, dict) else None + all_ids = sorted(c["id"] for c in spec["proposed_graph_nodes"]) + # exactly two accepted states (Codex 4143661501): 'installed' (residual PROVED_REVIEWED, every component and edge + # live) and 'baseline' (residual absent or OPEN_ACTIVE, no edge of this record, no component except the + # cross-record palm node that Math-#160 creates); anything else, the interim shape included, is 'partial' + if not mismatched and sorted(present) == all_ids and wanted <= live_edges and res_cls == "PROVED_REVIEWED": + state = "installed" + elif not mismatched and set(present) <= {PALM_NODE} and not (wanted & live_edges) and res_cls in (None, "OPEN_ACTIVE"): + state = "baseline" + else: + state = "partial" + if MUT == "partial-install" and state == "partial": + state = "baseline" + return {"present": sorted(present), "mismatched": sorted(mismatched), "residual": res_cls, + "edges_present": wanted <= live_edges, "state": state} def live_ok(graph, sel, spec): @@ -255,7 +267,7 @@ def live_ok(graph, sel, spec): ok &= res.get("classification") in ("OPEN_ACTIVE", "PROVED_REVIEWED") ok &= "witness-collision" in sel.get("regions", []) st = installed_state(graph, spec) - ok &= not st["mismatched"] + ok &= not st["mismatched"] and st["state"] in ("baseline", "installed") if st["residual"] == "PROVED_REVIEWED": # a promoted residual must carry the whole proposal: every component by id and bytes, every edge, the reading rule ok &= set(c["id"] for c in spec["proposed_graph_nodes"]) <= set(st["present"]) and st["edges_present"] @@ -473,16 +485,22 @@ def check_transitions(root, spec): ok &= all(nodes[d]["classification"] == "PROVED_REVIEWED" for d in req_after) ok &= len(req_after) == expected_required.get(stage, len(cids)) builds[stage] = (old, new) + # the installed state, simulated (Codex 4140125558): the executed graph passes LIVE and re-building it is a no-op; + # on the installed register the simulation is the live graph itself, so the drift mutant is rejected in either state + sim = build(spec, graph, "final")[1] + if MUT == "installed-drift": + sim["nodes"]["math.c6r-component.spectral-closure-proof"]["fingerprint"] = "0" * 64 + sim_ok, sim_st = live_ok(sim, sel, spec) + ok &= sim_ok and sim_st["residual"] == "PROVED_REVIEWED" and sim_st["present"] == sorted(cids) + ok &= sim_st["edges_present"] and not sim_st["mismatched"] + o2, n2 = build(spec, sim, "final") + ok &= o2 == n2 + # the installed graph without one component (and its edges) is a partial install, never baseline (Codex 4143661501) + part = copy.deepcopy(sim) + part["nodes"].pop("math.c6r-component.spectral-closure-proof", None) + part["edges"] = [e for e in part["edges"] if "math.c6r-component.spectral-closure-proof" not in (e["from"], e["to"])] + ok &= installed_state(part, spec)["state"] == "partial" if not installed: - # the installed state, simulated (Codex 4140125558): the executed graph passes LIVE and re-building it is a no-op - sim = build(spec, graph, "final")[1] - if MUT == "installed-drift": - sim["nodes"]["math.c6r-component.spectral-closure-proof"]["fingerprint"] = "0" * 64 - sim_ok, sim_st = live_ok(sim, sel, spec) - ok &= sim_ok and sim_st["residual"] == "PROVED_REVIEWED" and sim_st["present"] == sorted(cids) - ok &= sim_st["edges_present"] and not sim_st["mismatched"] - o2, n2 = build(spec, sim, "final") - ok &= o2 == n2 builds["installed-simulated"] = (o2, n2) return bool(ok), builds @@ -628,6 +646,7 @@ def main(): passed = all(checks.values()) and len(checks) == 8 print(json.dumps({"object": "C6-RESIDUAL-CLOSURE-20260930-v1", "checks": checks, "passed": passed, "inventory_files": len(INVENTORY), "component_nodes": len(spec["proposed_graph_nodes"]), + "register_state": live_state.get("state"), "live_state": live_state, "gate": gate, "scope": "identity, verdict-row, live-register (including the installed state), reviewed-text, exact " "finite bookkeeping of section 3, transition-shape, hard-gate replay with source snapshots in " diff --git a/reviews/c6_witness_collision_reconciliation_20260929/RECONCILIATION.md b/reviews/c6_witness_collision_reconciliation_20260929/RECONCILIATION.md index e488c0afe..63599b625 100644 --- a/reviews/c6_witness_collision_reconciliation_20260929/RECONCILIATION.md +++ b/reviews/c6_witness_collision_reconciliation_20260929/RECONCILIATION.md @@ -17,7 +17,20 @@ v1.4 merges main `aa28838`, records xAI 5901345590 (ACCEPT as inventory; HOLD on makes the execution order explicit in §7. v1.5 merges main `bb429d3` and records Math-#166 as the third candidate for the §5 residual, the one whose statement matches the residual's definition. v1.6 records xAI 5901915195. v1.7 re-verifies at `ec6db8c`, quotes the register as Math-#151 rewrote it (§1a), rebinds the `OBLIGATION` check to the current text, lists the D5 nodes -now live, and records that Math-#151 took the keep-open alternative without defining the regional mechanism. +now live, and records that Math-#151 took the keep-open alternative without defining the regional mechanism. v1.8 +(register execution readiness, `reviews/register_execution_readiness_20260930`; re-verified at `dda8991`, Math-#173 merged): the checker +accepts the live register in exactly two states, **baseline** (nothing of §7 live) or **installed** on the main path of §7 +(every proposed node live exactly on every proposed key; the residual node either as proposed here, `OPEN_ACTIVE` with its +notes, or `PROVED_REVIEWED` as Math-#173 proposes, with layer, kind, fingerprint and `controlling` unchanged; every +proposed edge not leaving the witness node live; the witness node `OPEN_ACTIVE` with none of its proposed edges live +while step 4 is pending, or `PROVED_REVIEWED` with all of them live and their required targets `PROVED_REVIEWED`), rejects partial +or drifted installs and any other live fingerprinted node on a proposed source, and accepts the selector table either +untouched or carrying every proposed cell with the three region ids covered; the workflow compares the checker's output +with `RESULTS.json` in the baseline state and with `RESULTS_INSTALLED.json` in the installed state; two mutants added +(`installed-drift`, `partial-install`); after Codex review 5365065925 on Math-#183 (threads 4143661492, 4143661519) the +installed selector table is accepted only when the graph carries the proposal, and the open witness node may carry none +of its proposed edges (mutants `selector-ahead`, `witness-edges-partial`; four added in all). Nothing in §§1–7 changes. The §1a register-equivalent alternative (no separate +residual node) is not an accepted installed state, since Math-#173 presupposes the separate node. **Effect:** register reconciliation, **declarative only**. This record introduces **no new mathematical claim**. It binds the merged C6 chain to exact bytes, quotes the open obligation as the register recorded it, states which reviewed theorem discharges that obligation and at what scope, states precisely what is *not* discharged, and proposes the @@ -369,10 +382,18 @@ them invalidates the fold through the existing reader; `coverage_source` metadat cross-record node is one the D5 proposal defines and, since `ec6db8c`, live with that proposal's fingerprint; a source already carried by a live fingerprinted node ([LP], `math.uniform-matrix-cap-lifetime`) is referenced through that node, with equal SHA256 and its four required reading-rule edges present, and no proposed node duplicates a live source; every proposed node passes the hard - gate's shape rules; `declarative` is true and `executed` is false. + gate's shape rules; `declarative` is true and `executed` is false. The live register is in exactly one of two + accepted states, baseline (nothing of §7 live) or installed (as the v1.8 revision note defines it: every node exactly, + the residual as proposed or as Math-#173 promotes it, the witness node open with none of its proposed edges live, or + `PROVED_REVIEWED` with all of them live; one witness edge toggled is asserted partial in every run); once installed this record's nodes are the live carriers of their sources and nothing else may be. The + installed state is also simulated (steps 1–3 applied to the live graph, the witness node left as it is) and must be + accepted exactly. - **SELECTOR.** The selector proposal names every selector of the live table for its three regions, assigns each a value the hard gate classifies as covered or bypassed, and, applied to the live table, moves exactly those three - region ids from `open_region_ids` to `covered_region_ids`. + region ids from `open_region_ids` to `covered_region_ids`. A live table already carrying every proposed cell is + accepted as installed when the three region ids are covered and not open and the graph carries the proposal (a table + ahead of the graph is rejected, and the rule itself is asserted in every run); a table carrying part of the proposal + is rejected; the node-only alternative of §7 step 2 (table untouched) is the baseline case. - **MONOTONE.** Exact enumeration: `(n_A)_q ≤ (n)_q` for every sub-count and `q ≤ 4`; `2·1{n≥2} ≤ n(n−1) ≤ nΨ`; the `Θ(r³)` bracket needs both the upper and the lower row. - **OPEN_RESIDUAL.** §5's open items are recorded (numerical constants; the residual node with its scale-`r` @@ -380,8 +401,15 @@ them invalidates the fold through the existing reader; `coverage_source` metadat "not supplied by the landed reviewed chain", with the candidates named as candidates only) and the residual node is proposed open. -Ten mutants must fail: `allow-symlink`, `no-hash`, `drop-edge`, `stale-fingerprint`, `executed-flag`, -`close-residual`, `drop-lower-bound`, `regional-strict`, `clone-live-node`, `open-cell-left`. +Fourteen mutants must fail: `allow-symlink`, `no-hash`, `drop-edge`, `stale-fingerprint`, `executed-flag`, +`close-residual`, `drop-lower-bound`, `regional-strict`, `clone-live-node`, `open-cell-left`, `installed-drift` (the +simulated installed register with the [PALM] node's fingerprint changed), `partial-install` (the simulated installed +register without the supersession node's edges), `selector-ahead` (the selector-to-graph tie disabled) and +`witness-edges-partial` (the witness-edge count ignored: one edge toggled would pass). The workflow runs the checker in +the state the repository is in: it +compares the output with `RESULTS.json` when the checker reports `register_state: baseline` and with +`RESULTS_INSTALLED.json` when it reports `installed`; the mutants must be rejected in either state (the composition of +Math-#167, #160 and #173 on a scratch copy, with every mutant, is replayed by `reviews/register_execution_readiness_20260930`). ## 9. Relation to other lanes diff --git a/reviews/c6_witness_collision_reconciliation_20260929/RESULTS.json b/reviews/c6_witness_collision_reconciliation_20260929/RESULTS.json index f68f83614..b61e4f426 100644 --- a/reviews/c6_witness_collision_reconciliation_20260929/RESULTS.json +++ b/reviews/c6_witness_collision_reconciliation_20260929/RESULTS.json @@ -12,5 +12,6 @@ "inventory_files": 22, "object": "C6-WITNESS-COLLISION-RECONCILIATION-20260929-v1", "passed": true, - "scope": "identity, verdict-row, obligation, filesystem-negative, transition-chain, monotonicity, open-item and selector-cell checks; no mathematics is re-proved" + "register_state": "baseline", + "scope": "identity, verdict-row, obligation, filesystem-negative, transition-chain (live register baseline or exactly installed), monotonicity, open-item and selector-cell checks; no mathematics is re-proved" } diff --git a/reviews/c6_witness_collision_reconciliation_20260929/RESULTS_INSTALLED.json b/reviews/c6_witness_collision_reconciliation_20260929/RESULTS_INSTALLED.json new file mode 100644 index 000000000..e86d49ec6 --- /dev/null +++ b/reviews/c6_witness_collision_reconciliation_20260929/RESULTS_INSTALLED.json @@ -0,0 +1,17 @@ +{ + "checks": { + "IDENTITIES": true, + "MONOTONE": true, + "NEGATIVES": true, + "OBLIGATION": true, + "OPEN_RESIDUAL": true, + "SELECTOR": true, + "TRANSITIONS": true, + "VERDICTS": true + }, + "inventory_files": 22, + "object": "C6-WITNESS-COLLISION-RECONCILIATION-20260929-v1", + "passed": true, + "register_state": "installed", + "scope": "identity, verdict-row, obligation, filesystem-negative, transition-chain (live register baseline or exactly installed), monotonicity, open-item and selector-cell checks; no mathematics is re-proved" +} diff --git a/reviews/c6_witness_collision_reconciliation_20260929/SOURCE_FILES.json b/reviews/c6_witness_collision_reconciliation_20260929/SOURCE_FILES.json index e94572a01..ad59fa5c5 100644 --- a/reviews/c6_witness_collision_reconciliation_20260929/SOURCE_FILES.json +++ b/reviews/c6_witness_collision_reconciliation_20260929/SOURCE_FILES.json @@ -16,21 +16,27 @@ }, { "path": "RECONCILIATION.md", - "bytes": 41289, - "sha256": "96a0f0bf2700b64b933d08d3c81efbfa8388aa2094e5528a1a6bd627e69f902a", - "git_blob": "e488c0afed5c41c2872de0902f0e3d1c08e1b2ce" + "bytes": 44686, + "sha256": "81db346cb7594d8b284b548d1de052bac31041034d30f739fa87bb51d3225851", + "git_blob": "63599b6258045793979986e5c89e466b9fc4e5e5" }, { "path": "RESULTS.json", - "bytes": 482, - "sha256": "8fee5c3e02f2d10de095217d98e7b8a7a7bd7725821a2a9ec9680018cf728a33", - "git_blob": "f68f83614484a6e9f9ae3f96502c88a954dce6ee" + "bytes": 560, + "sha256": "297b489071f8f459f2adb405bf0df90c850fb21ef63f7924870c8d6829836bf4", + "git_blob": "b61e4f426e88fd9d845b7a31e225ab595ee1f4b8" }, { "path": "reconciliation_check.py", - "bytes": 28037, - "sha256": "a19a01fec6957463229b2297195860105ac7be735f2dd297ffb2907ba2d5d2fa", - "git_blob": "a7de1d22c9177cb15133c425283ad990d928efb8" + "bytes": 35466, + "sha256": "9560763b3c8499f77b033ca9b77d24f1a5374e1283b0ce2e385b17eafb372860", + "git_blob": "6e8a0f6e663ebdbd8052dc5d435927234776046a" + }, + { + "path": "RESULTS_INSTALLED.json", + "bytes": 561, + "sha256": "f5e4aec2fe13bcfb8e87abf8795ed38931a33ea49a938916c0dd94b14cc9070f", + "git_blob": "e86d49ec670979990860059c4835c1a4f4224c6e" } ] } diff --git a/reviews/c6_witness_collision_reconciliation_20260929/reconciliation_check.py b/reviews/c6_witness_collision_reconciliation_20260929/reconciliation_check.py index a7de1d22c..6e8a0f6e6 100644 --- a/reviews/c6_witness_collision_reconciliation_20260929/reconciliation_check.py +++ b/reviews/c6_witness_collision_reconciliation_20260929/reconciliation_check.py @@ -23,6 +23,7 @@ drop-lower-bound, regional-strict. """ import argparse +import copy import hashlib import itertools import json @@ -33,7 +34,8 @@ import tempfile MUTANTS = ("allow-symlink", "no-hash", "drop-edge", "stale-fingerprint", "executed-flag", "close-residual", - "drop-lower-bound", "regional-strict", "clone-live-node", "open-cell-left") + "drop-lower-bound", "regional-strict", "clone-live-node", "open-cell-left", + "installed-drift", "partial-install", "selector-ahead", "witness-edges-partial") MUT = None HERE = "reviews/c6_witness_collision_reconciliation_20260929" PALM = "frontiers/c6_palm_route_20260929/PROOF.md" @@ -243,10 +245,71 @@ def check_negatives(src): return all(rejected) and len(rejected) == 4 +def matches(live, fields): + return isinstance(live, dict) and all(live.get(k) == v for k, v in fields.items()) + + +def installed_state(graph, proposed_nodes, proposed_edges): + """How much of section 7's proposal the live graph carries, on the main path (the residual node created separately; + Math-#173 may since have promoted it). Fail-closed: a proposed id carrying anything but the proposal on every + proposed key is a mismatch (the residual: this record's node OPEN_ACTIVE with its notes, or PROVED_REVIEWED as + Math-#173 proposes, with layer, kind, fingerprint and controlling unchanged); so is any other live fingerprinted + node on a proposed source. 'installed': every node present, every edge not leaving the witness node live, and the + witness node OPEN_ACTIVE with none of its proposed edges live (step 4 pending) or PROVED_REVIEWED with all of them + live and their required targets PROVED_REVIEWED (Codex 4143661519). 'baseline': nothing of the proposal live. + Anything else is 'partial' and rejected.""" + nodes = graph["nodes"] + proposed = {n["id"]: n for n in proposed_nodes} + present, mismatched = set(), set() + for nid, comp in proposed.items(): + n = nodes.get(nid) + if n is None: + continue + fields = {k: v for k, v in comp.items() if k != "id"} + if nid == RESIDUAL: + fields = {k: fields[k] for k in ("layer", "kind", "fingerprint", "controlling")} + fields_ok = (n.get("classification") == "PROVED_REVIEWED" + or (n.get("classification") == "OPEN_ACTIVE" and n.get("notes") == comp["notes"])) + else: + fields_ok = True + (present if matches(n, fields) and fields_ok else mismatched).add(nid) + by_source = {n["source"]: nid for nid, n in proposed.items() if n.get("source")} + for nid, n in nodes.items(): + if isinstance(n, dict) and n.get("fingerprint") and n.get("source") in by_source and nid != by_source[n["source"]]: + mismatched.add(nid) + live_edges = {(e["from"], e["to"], e["required"], e["relation"]) for e in graph["edges"]} + wanted = {(e["from"], e["to"], e["required"], e["relation"]) for e in proposed_edges} + wit_edges = {e for e in wanted if e[0] == WITNESS} + other = wanted - wit_edges + n_other, n_wit = len(other & live_edges), len(wit_edges & live_edges) + wit = nodes.get(WITNESS) if isinstance(nodes.get(WITNESS), dict) else {} + cls = wit.get("classification") + targets_ok = all(nodes.get(e[1], {}).get("classification") == "PROVED_REVIEWED" for e in wit_edges if e[2] is True) + if MUT == "witness-edges-partial": + wit_ok = cls == "OPEN_ACTIVE" or (cls == "PROVED_REVIEWED" and targets_ok) + else: + wit_ok = (cls == "OPEN_ACTIVE" and n_wit == 0) or (cls == "PROVED_REVIEWED" and n_wit == len(wit_edges) and targets_ok) + if not mismatched and set(present) == set(proposed) and n_other == len(other) and wit_ok: + state = "installed" + elif not mismatched and not present and n_other == 0 and n_wit == 0: + state = "baseline" + else: + state = "partial" + return {"state": state, "present": sorted(present), "mismatched": sorted(mismatched), + "edges_present": n_other + n_wit, "edges_proposed": len(wanted), "witness": cls} + + +def register_state(root): + spec = json.loads((root / HERE / "PROPOSED_TRANSITIONS.json").read_text(encoding="utf-8")) + graph = json.loads((root / GRAPH).read_text(encoding="utf-8")) + return installed_state(graph, spec["proposed_graph_nodes"], spec["proposed_graph_edges"])["state"] + + def check_transitions(root): spec = json.loads((root / HERE / "PROPOSED_TRANSITIONS.json").read_text(encoding="utf-8")) d5 = json.loads((root / D5_TRANSITIONS).read_text(encoding="utf-8")) - live = json.loads((root / GRAPH).read_text(encoding="utf-8"))["nodes"] + graph = json.loads((root / GRAPH).read_text(encoding="utf-8")) + live = graph["nodes"] d5_nodes = {n["id"] for n in d5["proposed_graph_nodes"]} nodes = {n["id"]: n for n in spec["proposed_graph_nodes"]} edges = list(spec["proposed_graph_edges"]) @@ -273,6 +336,9 @@ def check_transitions(root): if n.get("source") == PALM: n["fingerprint"] = "0" * 64 ok = spec.get("declarative") is True and spec.get("executed") is False + # the live register carries nothing of the proposal, or all of it exactly (v1.8; Math-#173 may have promoted the residual) + st = installed_state(graph, list(nodes.values()), edges) + ok &= st["state"] in ("baseline", "installed") # shape rules of the hard gate, applied to the proposed nodes and edges for n in nodes.values(): ok &= n.get("classification") in CLASSES and type(n.get("controlling")) is bool and n["controlling"] is False @@ -306,9 +372,10 @@ def check_transitions(root): ok &= len({n.get("source") for n in nodes.values() if "fingerprint" in n and n.get("source")} & {n.get("source") for n in d5["proposed_graph_nodes"] if "fingerprint" in n and n.get("source")}) == 0 ok &= all(evidence[nid]["fingerprint"] == INVENTORY[src][0] for src, nid in by_source.items()) - # no proposed node duplicates a source the live graph already carries with a fingerprint (Codex 4139312869) + # no proposed node duplicates a source the live graph already carries with a fingerprint (Codex 4139312869); once + # installed, this record's own nodes are the live carriers of their sources and nothing else is (installed_state) ok &= not ({n.get("source") for n in nodes.values() if "fingerprint" in n and n.get("source")} - & {n["source"] for n in live_fp.values()}) + & {n["source"] for nid, n in live_fp.items() if nid not in nodes}) # the reused live node is PROVED_REVIEWED with its four required reading-rule components, all PROVED_REVIEWED lp = live.get(LIVE_LP, {}) ok &= lp.get("classification") == "PROVED_REVIEWED" and lp.get("source") == LP and lp.get("fingerprint") == INVENTORY[LP][0] @@ -357,12 +424,53 @@ def check_transitions(root): if isinstance(dup, dict): ok &= dup.get("fingerprint") == live.get("math.rn-fixed-remote-window", {}).get("fingerprint") \ == INVENTORY["frontiers/remote_window_20260924/PROOF.md"][0] + # the installed state, simulated on the baseline register (the live one once installed): steps 1-3 applied, the + # witness node left as it is; accepted exactly, and a drifted or partial install is rejected + sim = copy.deepcopy(graph) + for nid, n in nodes.items(): + if nid not in sim["nodes"]: + sim["nodes"][nid] = {k: v for k, v in n.items() if k != "id"} + have = {(e["from"], e["to"], e["required"], e["relation"]) for e in sim["edges"]} + for e in edges: + key = (e["from"], e["to"], e["required"], e["relation"]) + if key not in have and e["from"] != WITNESS: + sim["edges"].append({"from": e["from"], "to": e["to"], "required": e["required"], "relation": e["relation"]}) + have.add(key) + if MUT == "installed-drift": + sim["nodes"]["math.c6-component.palm-proof"]["fingerprint"] = "0" * 64 + if MUT == "partial-install": + sim["edges"] = [e for e in sim["edges"] if e["from"] != SUPERSESSION] + sim_st = installed_state(sim, list(nodes.values()), edges) + ok &= sim_st["state"] == "installed" and sim_st["mismatched"] == [] and sim_st["present"] == sorted(nodes) + # one witness edge toggled (added while the witness node is open, removed once it is PROVED_REVIEWED) is a partial + # step 4, never an accepted state (Codex 4143661519) + wit_edges = [e for e in edges if e["from"] == WITNESS] + if wit_edges: + tog = copy.deepcopy(sim) + first = wit_edges[0] + key = (first["from"], first["to"], first["required"], first["relation"]) + if tog["nodes"].get(WITNESS, {}).get("classification") == "PROVED_REVIEWED": + tog["edges"] = [e for e in tog["edges"] if (e["from"], e["to"], e["required"], e["relation"]) != key] + else: + tog["edges"].append({"from": key[0], "to": key[1], "required": key[2], "relation": key[3]}) + ok &= installed_state(tog, list(nodes.values()), edges)["state"] == "partial" + else: + ok = False return bool(ok) +def selector_state_ok(applied_all, graph_state): + """A table carrying every proposed cell is accepted only when the graph carries the proposal (Codex 4143661492).""" + if MUT == "selector-ahead": + return True + return (not applied_all) or graph_state == "installed" + + def check_selector(root): """Applied to the live selector table, the proposal leaves no open cell in its regions and moves exactly those - region ids from open to covered (Codex 4139312863).""" + region ids from open to covered (Codex 4139312863). Once the table carries every proposed cell, the three region + ids must be covered and not open, and the graph must carry the proposal (installed); a table carrying part of the + proposal, or the proposal ahead of the graph, is rejected (v1.8).""" spec = json.loads((root / HERE / "PROPOSED_TRANSITIONS.json").read_text(encoding="utf-8")) live = json.loads((root / SELECTOR).read_text(encoding="utf-8")) prop = spec["selector_region_proposal"] @@ -373,19 +481,26 @@ def check_selector(root): ok = set(regions) <= set(live["regions"]) and len(regions) == 3 ok &= set(cells) == set(live["selectors"]) ok &= all(v not in OPEN_CELLS for v in cells.values()) + ids = ["math.rn-region." + reg for reg in regions] + applied = sum(1 for s, v in cells.items() for reg in regions if live["selectors"].get(s, {}).get(reg) == v) table = {s: dict(row) for s, row in live["selectors"].items()} - for s, v in cells.items(): - for reg in regions: - table[s][reg] = v + ok &= selector_state_ok(applied == len(cells) * len(regions), register_state(root)) + ok &= not selector_state_ok(True, "baseline") and selector_state_ok(False, "baseline") # the rule itself + if applied == len(cells) * len(regions): # installed: cells and region lists as proposed + ok &= set(ids) <= set(live["covered_region_ids"]) and not (set(ids) & set(live["open_region_ids"])) + else: # baseline: the proposal applied to the live table + ok &= applied == 0 + for s, v in cells.items(): + for reg in regions: + table[s][reg] = v + covered = list(live["covered_region_ids"]) + [i for i in ids if i not in live["covered_region_ids"]] + opened = [i for i in live["open_region_ids"] if i not in ids] + ok &= sorted(prop["resulting_covered_region_ids"]) == sorted(covered) + ok &= sorted(prop["resulting_open_region_ids"]) == sorted(opened) + ok &= all(i in live["open_region_ids"] for i in ids) def is_open(reg): return any(table[s].get(reg) in OPEN_CELLS for s in live["selectors"]) ok &= not any(is_open(reg) for reg in regions) - ids = ["math.rn-region." + reg for reg in regions] - covered = list(live["covered_region_ids"]) + [i for i in ids if i not in live["covered_region_ids"]] - opened = [i for i in live["open_region_ids"] if i not in ids] - ok &= sorted(prop["resulting_covered_region_ids"]) == sorted(covered) - ok &= sorted(prop["resulting_open_region_ids"]) == sorted(opened) - ok &= all(("math.rn-region." + reg) in live["open_region_ids"] for reg in regions) ok &= prop.get("under_node") == SUPERSESSION return bool(ok) @@ -442,9 +557,10 @@ def main(): "SELECTOR": check_selector(root)} passed = all(checks.values()) and len(checks) == 8 print(json.dumps({"object": "C6-WITNESS-COLLISION-RECONCILIATION-20260929-v1", "checks": checks, "passed": passed, - "inventory_files": len(INVENTORY), - "scope": "identity, verdict-row, obligation, filesystem-negative, transition-chain, monotonicity, " - "open-item and selector-cell checks; no mathematics is re-proved"}, indent=2, sort_keys=True)) + "inventory_files": len(INVENTORY), "register_state": register_state(root), + "scope": "identity, verdict-row, obligation, filesystem-negative, transition-chain (live register baseline " + "or exactly installed), monotonicity, open-item and selector-cell checks; no mathematics is " + "re-proved"}, indent=2, sort_keys=True)) return 0 if passed else 1 diff --git a/reviews/register_alignment_20260930/RECONCILIATION.md b/reviews/register_alignment_20260930/RECONCILIATION.md index ece9655fd..979c1158b 100644 --- a/reviews/register_alignment_20260930/RECONCILIATION.md +++ b/reviews/register_alignment_20260930/RECONCILIATION.md @@ -16,7 +16,16 @@ gain `covered_by` edges, `apply()` carries scope exclusions and replacement note two-commit source mutations through the production reverse-impact rule, the interface's promoted scope is narrowed to self-contained inequalities plus conditional implications with its consumed premises as edges, the interface evidence labels separate exact from floating-point checks, and the external issue comments are preserved in `EXTERNAL_REVIEWS.md` -and labelled as mutable evidence; the eight classifications are unchanged. +and labelled as mutable evidence; the eight classifications are unchanged. v1.4 (register execution readiness, +`reviews/register_execution_readiness_20260930`; re-verified at `dda8991`, Math-#173 merged): the checker accepts the live register in +exactly two states, **baseline** (nothing of the proposal live) or **installed** (every proposed field of the eight nodes, +every component node and every proposed edge live exactly), rejects partial or drifted installs, replays the proposal +from the register without it (`strip`) and, once installed, asserts that `apply` is the identity and that this record's +objects are unheld; the workflow compares the checker's output with `RESULTS.json` in the baseline state and with +`RESULTS_INSTALLED.json` in the installed state; two mutants added (`installed-drift`, `partial-install`); after Codex +review 5365065925 on Math-#183 (thread 4143661511) the baseline state also pins the proposal-written fields of the eight +nodes to their digests at `dda8991`, so the proposal's metadata installed under the current classification is a partial +install (mutant `text-preinstalled`; three added in all). Transitions, sources and verdicts are unchanged. **Effect:** register reconciliation, **declarative only**. This record introduces **no new mathematical claim**. It binds five objects that the register already lists as accepted to their exact bytes, quotes the nonauthor verdicts that accepted them, records that their live graph nodes still carry the pre-review classification, and proposes the node @@ -214,8 +223,16 @@ rather than inferred from old-versus-new GRAPH metadata. object headers of the sources, the D4 sentence that consumes the interface, the interface note's (N1)/(N4)/(N5) displays, the five PROOF_INDEX rows, the interface review's overall verdict and evidence labels, and the seven comment ids with their verdict lines and the mutability label in `EXTERNAL_REVIEWS.md` are present as substrings. -- **BASELINE.** Each transition's live node exists with exactly the recorded current classification, fingerprint, - kind and source; the D1 node is `PROVED_REVIEWED` with its four reading-rule components `PROVED_REVIEWED`. +- **BASELINE.** The live register is in exactly one of two accepted states. *Baseline:* each transition's live node + exists with exactly the recorded current classification, fingerprint, kind and source, its proposal-written fields + (scope, explicit limits, notes, review disposition, review sources, review basis, coverage source, source) carry the + digest recorded at `dda8991` (`BASELINE_TEXT`), no component node and no proposed edge is live. *Installed:* each transition's live node carries every proposed field exactly (classification, + `controlling`, fingerprint, source, scope, explicit limits, notes, review disposition, review sources and the derived + `review_basis`), every component node is live as proposed on every proposed key, every proposed edge is live, and no + other live fingerprinted node carries a component source. Any node in between (one flipped, one not; a proposed key + drifted; a component present under another id) is a mismatch and the check fails. In both states the D1 node is + `PROVED_REVIEWED` with its four reading-rule components `PROVED_REVIEWED`, and every transition is a change (its + current and proposed classifications differ). - **TRANSITIONS.** `declarative` true, `executed` false, `edges_unchanged` false; every proposed classification is `PROVED_REVIEWED` with `controlling: false`, a non-empty scope, explicit limits, replacement notes and at least one review source; every candidate node's fingerprint equals the SHA256 of its inventoried source; every component node @@ -225,9 +242,20 @@ rather than inferred from old-versus-new GRAPH metadata. graph, no live node other than the eight changes, no live edge is removed, every flipped node's required premises (the live D1 node and cap component, the interface, the component nodes) are `PROVED_REVIEWED`, every region requires its covering node, and every applied node carries its `explicit_limits`, its replacement `notes` and a `review_basis`. -- **GATE.** The proposed graph passes the hard gate's `validate_graph_fail_closed`; `closure_report` gives `gate_ok` - with no illegal controlling node; `reverse_impact_between(live, proposed)` runs and its impacted set (the eight nodes, - the eight component nodes and their dependents) is recorded. + `apply` is idempotent (a node already carrying the proposal is left as it is, a live component or edge is not + re-created) and `strip` is its pre-image (the eight nodes at their current classification and fingerprint, the + component nodes and the edges touching them removed): on the baseline register `strip` is the identity, on the + installed register `apply` is, and `apply(strip(·))` reproduces every object on every proposed key in both. The + installed state is also simulated (on the baseline register: `apply` of the live graph; once installed: the live graph + itself) and must be accepted exactly, with re-application a no-op. +- **GATE.** The proposal replayed from the register without it: the replay passes the hard gate's + `validate_graph_fail_closed`; `closure_report` gives `gate_ok` with no illegal controlling node on the pre-image, the + replay and the live graph; `reverse_impact_between(pre-image, replay)` changes and impacts every one of the sixteen + objects (loss-only rule), and none of them is held once applied (every required premise `PROVED_REVIEWED`). In the + baseline state the pre-image is the live graph and the impacted set (the eight nodes, the eight component nodes and + their dependents) is recorded in `RESULTS.json`; in the installed state `reverse_impact_between(live, apply(live))` + must be empty (nothing left to apply) and the impacted set is not pinned, since after execution it depends on the + other landed records. - **PROPAGATION.** Nine two-commit cases on the proposed graph with source snapshots in the shape of `git_transition_audit.read_snapshot`: a D4 proof edit reaches the fixed-remote region and the mesoscopic consumer; an annulus proof edit reaches its region; deleting the interface review record reaches the interface, D4, the annulus and @@ -246,11 +274,18 @@ rather than inferred from old-versus-new GRAPH metadata. citing main#76 with verdict ACCEPT, `component_of` `math.d5-pin-neighborhood-first-moment`; and the older live node `math.rn-fixed-remote-window` still carries that fingerprint at `AUTHOR_SIDE_CANDIDATE`, the lag this record aligns. -Twelve mutants must fail: `allow-symlink`, `no-hash`, `stale-fingerprint`, `drop-review-source`, `controlling-true`, +Fifteen mutants must fail: `allow-symlink`, `no-hash`, `stale-fingerprint`, `drop-review-source`, `controlling-true`, `executed-flag`, `skip-interface-premise`, `holder-reversed`, `baseline-drift`, `duplicate-drift`, `region-unlinked` -(the `covered_by` edges removed before the propagation replay: proof edits no longer reach the regions) and +(the `covered_by` edges removed before the propagation replay: proof edits no longer reach the regions), `review-metadata-only` (the review-record nodes and their edges removed before the replay, leaving the citations as -metadata only: a deleted or edited review record no longer reaches its accepted object). +metadata only: a deleted or edited review record no longer reaches its accepted object), `installed-drift` (the +simulated installed register with one component fingerprint changed), `partial-install` (the simulated installed +register with the D4 node back at its current classification) and `text-preinstalled` (the baseline text-field rule +disabled: the pre-image of the applied graph, which carries the proposed metadata under the current classifications, +would pass as baseline; every run asserts that it is partial). The workflow runs the checker in the state the +repository is in: it compares the output with `RESULTS.json` when the checker reports `register_state: baseline` and +with `RESULTS_INSTALLED.json` when it reports `installed`; the mutants must be rejected in either state (the +composition of Math-#167, #160 and #173 on a scratch copy, with every mutant, is replayed by `reviews/register_execution_readiness_20260930`). ## 7. Relation to other lanes diff --git a/reviews/register_alignment_20260930/RESULTS.json b/reviews/register_alignment_20260930/RESULTS.json index 6702db536..dd785ae21 100644 --- a/reviews/register_alignment_20260930/RESULTS.json +++ b/reviews/register_alignment_20260930/RESULTS.json @@ -51,6 +51,7 @@ "math.rn-selector-region-crosswalk", "math.side24-coefficient" ], + "register_state": "baseline", "reverse_impact_keys": [ "changed_nodes", "context_changed", @@ -94,6 +95,7 @@ "two-scale-addendum-edit-reaches-annulus-and-region": true, "unrelated-edit-leaves-the-eight-untouched": true }, - "scope": "identity, verdict-row, live-baseline, transition-shape, hard-gate replay, two-commit propagation, interface arithmetic (exact and numerical parts labelled), filesystem-negative and live D4-duplicate checks; no mathematics is re-proved; nothing is written", + "register_state": "baseline", + "scope": "identity, verdict-row, live-register (baseline or exactly installed), transition-shape, hard-gate replay from the pre-image, two-commit propagation, interface arithmetic (exact and numerical parts labelled), filesystem-negative and live D4-duplicate checks; no mathematics is re-proved; nothing is written", "transitions": 8 } diff --git a/reviews/register_alignment_20260930/RESULTS_INSTALLED.json b/reviews/register_alignment_20260930/RESULTS_INSTALLED.json new file mode 100644 index 000000000..b56db6ae5 --- /dev/null +++ b/reviews/register_alignment_20260930/RESULTS_INSTALLED.json @@ -0,0 +1,54 @@ +{ + "checks": { + "BASELINE": true, + "D4_DUPLICATE": true, + "GATE": true, + "IDENTITIES": true, + "INTERFACE": true, + "NEGATIVES": true, + "PROPAGATION": true, + "TRANSITIONS": true, + "VERDICTS": true + }, + "component_nodes": 8, + "edges_added": 16, + "gate": { + "register_state": "installed", + "replay": "the proposal replayed from the pre-image (strip) on the installed register: loss-only rule and unheld objects asserted; the impacted set is not pinned post-execution" + }, + "interface_evidence": { + "exact_rational": [ + "(N1) Holder p=2,3 on finite rational spaces", + "(N2) exponent identity", + "(N3) conditional-mean identity", + "sharp-p example at r=2^-pm", + "(N4) integer monotonicity of ceil(t)" + ], + "numerical_corroboration_floating_point": [ + "(N4) grid maximum of (t+1)^p e^-3t", + "(N5) Simpson quadrature at three parameter points", + "(N4) example uniform tail on a grid" + ], + "results": { + "exact": true, + "numerical_corroboration": true + } + }, + "inventory_files": 15, + "object": "REGISTER-ALIGNMENT-20260930-v1", + "passed": true, + "propagation": { + "annulus-proof-edit-reaches-region": true, + "d4-fingerprint-edit-reaches-region": true, + "d4-proof-edit-reaches-region-and-consumer": true, + "external-review-record-edit-reaches-d2-d3-d4-d6": true, + "interface-review-deleted-reaches-interface-consumers-regions": true, + "no-op-impacts-nothing": true, + "realized-covers-edit-reaches-d6": true, + "two-scale-addendum-edit-reaches-annulus-and-region": true, + "unrelated-edit-leaves-the-eight-untouched": true + }, + "register_state": "installed", + "scope": "identity, verdict-row, live-register (baseline or exactly installed), transition-shape, hard-gate replay from the pre-image, two-commit propagation, interface arithmetic (exact and numerical parts labelled), filesystem-negative and live D4-duplicate checks; no mathematics is re-proved; nothing is written", + "transitions": 8 +} diff --git a/reviews/register_alignment_20260930/SOURCE_FILES.json b/reviews/register_alignment_20260930/SOURCE_FILES.json index e49e54aee..5f155d1c6 100644 --- a/reviews/register_alignment_20260930/SOURCE_FILES.json +++ b/reviews/register_alignment_20260930/SOURCE_FILES.json @@ -15,9 +15,9 @@ }, { "path": "RECONCILIATION.md", - "bytes": 32725, - "sha256": "0baf1c4e3c48ca3e2bb4eaeb419ee8ba368f082447f38f638fd10ce023c5249f", - "git_blob": "ece9655fd80ea51c18d7b1b2410d4c073854db89" + "bytes": 36811, + "sha256": "e726c7414cbdde57a665ae6b2daf2bf0524f0283a21f5efaa488c0ca69243531", + "git_blob": "979c1158b4148400e00ff09d02d78cb7534ea966" }, { "path": "RN_COUNT_INTERFACE_REVIEW.md", @@ -27,21 +27,27 @@ }, { "path": "RESULTS.json", - "bytes": 3452, - "sha256": "cbbff25994c22c55fd49c59bc2748af1c6ef128793a34880613cf7cb1d9162df", - "git_blob": "6702db536f00ec5689ab398c003f46a91b645d7b" + "bytes": 3569, + "sha256": "14c370b9a54e4b88e74d4192387e710892024e690099383ad1173f9545fc07d7", + "git_blob": "dd785ae218bc723f4130b23e6b6b39ba2c299c3d" }, { "path": "alignment_check.py", - "bytes": 31556, - "sha256": "eb1888ea57416f87fbfa4692b6c07b20261c97bd08ce926aee7ec6fca5486502", - "git_blob": "cd110b0cfb2cfaf6f11e7405d99e0070c816a224" + "bytes": 42786, + "sha256": "c87191deca98cb1b6ae4b0bf7a78a6fb12a4e0534227085d126a4cb07a050a21", + "git_blob": "fdd590208cd1cd2c61c4ac11e9fa1a10671c362d" }, { "path": "EXTERNAL_REVIEWS.md", "bytes": 29877, "sha256": "fa6677f16f688352f3fc9b1703d39324fe57a3b2bf61960591f524f858e99c9d", "git_blob": "2be80e35bce1ffc90d1f7a0675ad5e8830ddbd28" + }, + { + "path": "RESULTS_INSTALLED.json", + "bytes": 2029, + "sha256": "d0af4624139b9babdeced2ac0c6d2979dd0a72c154898c0c1bcf14eaeaca6bfe", + "git_blob": "b56db6ae529688f8be5f358e651fd425fe229135" } ] } diff --git a/reviews/register_alignment_20260930/alignment_check.py b/reviews/register_alignment_20260930/alignment_check.py index cd110b0cf..fdd590208 100644 --- a/reviews/register_alignment_20260930/alignment_check.py +++ b/reviews/register_alignment_20260930/alignment_check.py @@ -4,6 +4,14 @@ Checks: IDENTITIES, VERDICTS, BASELINE, TRANSITIONS, GATE, PROPAGATION, INTERFACE, NEGATIVES, D4_DUPLICATE. No mathematics is re-proved; the proposed graph is replayed through the downstream hard gate's own validators, and two-commit source mutations through its reverse-impact rule. Nothing is written to the repository. + +Register states (v1.4). The live register is accepted in exactly two states: 'baseline' (none of the proposal is live: the +eight nodes carry their recorded current classification and fingerprint, no component node, no proposed edge) and +'installed' (all of it is live exactly: every transition node carries every proposed field, every component node is +present as proposed, every proposed edge is live). Anything in between, or any drift on a proposed key, is rejected. In +either state the proposal is replayed from the register without it (strip) through the hard gate; in the installed state +apply() is additionally the identity and this record's objects are unheld. The printed report names the state; the +replay's impacted set is printed only in the baseline state (post-execution it depends on the other landed records). """ import argparse import copy @@ -20,7 +28,7 @@ MUTANTS = ("allow-symlink", "no-hash", "stale-fingerprint", "drop-review-source", "controlling-true", "executed-flag", "skip-interface-premise", "holder-reversed", "baseline-drift", "duplicate-drift", "region-unlinked", - "review-metadata-only") + "review-metadata-only", "installed-drift", "partial-install", "text-preinstalled") MUT = None HERE = "reviews/register_alignment_20260930" GRAPH = "frontiers/downstream_gate_20260925/GRAPH.json" @@ -30,6 +38,21 @@ D4_NODE = "math.rn-fixed-remote-window" IFACE = "math.rn-count-interface" D4 = "frontiers/remote_window_20260924/PROOF.md" +# the proposal-written fields of a transition node, and their digest per node as live at dda8991 (json, sorted keys, +# absent = null): the baseline state requires them unchanged, so the proposal's metadata installed under the current +# classification is a partial install, not baseline (Codex 4143661511 on Math-#183) +TEXT_FIELDS = ("scope", "explicit_limits", "notes", "review_disposition", "review_sources", "review_basis", + "coverage_source", "source") +BASELINE_TEXT = { + "math.rn-count-interface": "16b8a05feaea45acaaa4c1340d2dbed4ffea5501431d5bd11c4ce6298cd3eb16", + "math.lifetime-remainder": "e5164f8eb6b27b67214c4b30b52ccdcf7d154dc1cd3f2382aab15c042a59c6dc", + "math.side24-coefficient": "f5a17c6ff5b8e5503aa2ef30c91327503f66b2e82f61b102a12ae47e20bfb60b", + "math.rn-fixed-remote-window": "658289f63342a17dee388640eee1648a7f524e3ab4e2351aa42ba1e1a8619be9", + "math.rn-region.fixed-remote": "4813392472753d7af976656e900de10216a1930e89a7a5bff625a33efc0cd4c8", + "math.rn-fixed-annulus-window": "44aedcb20147d78b3134cdf312a5e1e115901c496b986605a2faaf1443851491", + "math.rn-region.fixed-annulus-window": "59b4e5cf61440f7c13a7b157aa609e8d6bd2f66a85fc4cfc5643fc0ac263a03d", + "math.p15-full-price": "11271b1ceb95af1fc9d11f22b19abfc5ac139005c543086f2181d1e8f2d1d5ca" +} INVENTORY = { "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md": [ "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", @@ -202,18 +225,97 @@ def load_spec(root): return spec +def proposed_fields(p): + """The live fields the proposal writes on a transition node (apply's normative form).""" + f = {"classification": p["classification"], "controlling": p["controlling"], "fingerprint": p["fingerprint"], + "scope": p["scope"], "explicit_limits": p["explicit_limits"], "notes": p["notes"], + "review_disposition": p["review_disposition"], "review_sources": [r["ref"] for r in p["review_sources"]], + "review_basis": [{"review": r["ref"], "provider": r.get("provider", "unstated"), "verdict": r.get("verdict", "")} + for r in p["review_sources"]]} + if p.get("source"): + f["source"] = p["source"] + if p.get("coverage_source"): + f["coverage_source"] = p["coverage_source"] + return f + + +def component_fields(comp): + return {k: v for k, v in comp.items() if k != "id"} + + +def matches(live, fields): + return isinstance(live, dict) and all(live.get(k) == v for k, v in fields.items()) + + +def text_digest(node): + return hashlib.sha256(json.dumps({k: node.get(k) for k in TEXT_FIELDS}, sort_keys=True, + ensure_ascii=False).encode("utf-8")).hexdigest() + + +def at_baseline(node, t): + """The recorded current classification and fingerprint, and the proposal-written fields as they were at dda8991.""" + ok = matches(node, {"classification": t["current"]["classification"], "fingerprint": t["current"]["fingerprint"]}) + if MUT != "text-preinstalled": + ok = ok and text_digest(node) == BASELINE_TEXT[t["node"]] + return ok + + +def installed_state(graph, spec): + """How much of the proposal the live graph carries. Fail-closed: a transition node is 'flipped' only if it carries + every proposed field exactly and 'baseline' only if it carries the recorded current classification and fingerprint + with the proposal-written fields unchanged since dda8991 (BASELINE_TEXT); a live node on a component source that is not the proposed node on every proposed key is a mismatch, as is a + proposed id carrying anything else. The state is 'installed' (everything, exactly), 'baseline' (nothing) or + 'partial' (rejected by BASELINE and TRANSITIONS).""" + nodes = graph["nodes"] + flipped, baseline, mismatched, present = set(), set(), set(), set() + for t in spec["transitions"]: + n = nodes.get(t["node"]) + if matches(n, proposed_fields(t["proposed"])): + flipped.add(t["node"]) + elif isinstance(n, dict) and at_baseline(n, t): + baseline.add(t["node"]) + else: + mismatched.add(t["node"]) + by_source = {c["source"]: c for c in spec["proposed_graph_nodes"]} + for nid, n in nodes.items(): + if not isinstance(n, dict) or n.get("source") not in by_source: + continue + comp = by_source[n["source"]] + (present if nid == comp["id"] and matches(n, component_fields(comp)) else mismatched).add(nid) + for c in spec["proposed_graph_nodes"]: + if c["id"] in nodes and c["id"] not in present: + mismatched.add(c["id"]) + live_edges = {(e["from"], e["to"], e["required"], e["relation"]) for e in graph["edges"]} + wanted = {(e["from"], e["to"], e["required"], e["relation"]) for e in spec["proposed_graph_edges"]} + n_edges = len(wanted & live_edges) + ids = sorted(t["node"] for t in spec["transitions"]) + cids = sorted(c["id"] for c in spec["proposed_graph_nodes"]) + if not mismatched and sorted(flipped) == ids and sorted(present) == cids and n_edges == len(wanted): + state = "installed" + elif not mismatched and not flipped and not present and n_edges == 0: + state = "baseline" + else: + state = "partial" + return {"state": state, "flipped": sorted(flipped), "baseline": sorted(baseline), "mismatched": sorted(mismatched), + "present": sorted(present), "edges_present": n_edges, "edges_proposed": len(wanted)} + + def check_baseline(root, spec): - live = json.loads((root / GRAPH).read_text(encoding="utf-8"))["nodes"] - ok = True + graph = json.loads((root / GRAPH).read_text(encoding="utf-8")) + live = graph["nodes"] + st = installed_state(graph, spec) + ok = st["state"] in ("baseline", "installed") for t in spec["transitions"]: n = live.get(t["node"]) if not isinstance(n, dict): return False - ok &= n.get("classification") == t["current"]["classification"] - ok &= n.get("fingerprint") == t["current"]["fingerprint"] + expect = t["proposed"] if st["state"] == "installed" else t["current"] + ok &= n.get("classification") == expect["classification"] + ok &= n.get("fingerprint") == expect["fingerprint"] ok &= n.get("kind") == t["kind"] and n.get("controlling") is False if t["kind"] == "candidate": ok &= n.get("source") == t["proposed"]["source"] + ok &= t["current"]["classification"] != t["proposed"]["classification"] # a transition is a change d1 = live.get(D1, {}) ok &= d1.get("classification") == "PROVED_REVIEWED" and d1.get("fingerprint") == INVENTORY[ "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md"][0] @@ -223,34 +325,50 @@ def check_baseline(root, spec): def apply(spec, graph): - """The proposal applied to a copy of the live graph: the eight flips with their scope exclusions and replacement - notes, plus the review-record / consumed-source component nodes and the required edges that carry the evidence.""" + """The proposal applied to a copy of the live graph, idempotently: the eight flips with their scope exclusions and + replacement notes (a no-op on a node that already carries them), the review-record / consumed-source component + nodes (not re-created when present as proposed) and the required edges that carry the evidence (not re-added when + live). On the installed register apply is the identity.""" new = copy.deepcopy(graph) for t in spec["transitions"]: - n = new["nodes"][t["node"]] - p = t["proposed"] - n["classification"] = p["classification"] - n["controlling"] = p["controlling"] - n["fingerprint"] = p["fingerprint"] - if p.get("source"): - n["source"] = p["source"] - n["scope"] = p["scope"] - n["explicit_limits"] = p["explicit_limits"] - n["notes"] = p["notes"] - n["review_disposition"] = p["review_disposition"] - n["review_sources"] = [r["ref"] for r in p["review_sources"]] - n["review_basis"] = [{"review": r["ref"], "provider": r.get("provider", "unstated"), "verdict": r.get("verdict", "")} - for r in p["review_sources"]] - if p.get("coverage_source"): - n["coverage_source"] = p["coverage_source"] + new["nodes"][t["node"]].update(proposed_fields(t["proposed"])) + present = set(installed_state(graph, spec)["present"]) for c in spec["proposed_graph_nodes"]: - new["nodes"][c["id"]] = {k: v for k, v in c.items() if k != "id"} - new["edges"] = list(new["edges"]) + [dict(e) for e in spec["proposed_graph_edges"]] + if c["id"] not in present: + new["nodes"][c["id"]] = component_fields(c) + have = {(e["from"], e["to"], e["required"], e["relation"]) for e in new["edges"]} + new["edges"] = list(new["edges"]) + for e in spec["proposed_graph_edges"]: + key = (e["from"], e["to"], e["required"], e["relation"]) + if key not in have: + new["edges"].append(dict(e)) + have.add(key) return new + +def strip(spec, graph): + """The register without the proposal, the pre-image the hard-gate replay starts from: the eight nodes at their + recorded current classification and fingerprint, the component nodes and every edge touching them removed, the + proposed edges removed. On the baseline register strip is the identity; apply(strip(installed)) reproduces every + installed object on every proposed key.""" + old = copy.deepcopy(graph) + for t in spec["transitions"]: + old["nodes"][t["node"]]["classification"] = t["current"]["classification"] + old["nodes"][t["node"]]["fingerprint"] = t["current"]["fingerprint"] + cids = {c["id"] for c in spec["proposed_graph_nodes"]} + for cid in cids: + old["nodes"].pop(cid, None) + wanted = {(e["from"], e["to"], e["required"], e["relation"]) for e in spec["proposed_graph_edges"]} + old["edges"] = [e for e in old["edges"] if (e["from"], e["to"], e["required"], e["relation"]) not in wanted + and e["from"] not in cids and e["to"] not in cids] + return old + def check_transitions(root, spec): graph = json.loads((root / GRAPH).read_text(encoding="utf-8")) + st = installed_state(graph, spec) + installed = st["state"] == "installed" ok = spec.get("declarative") is True and spec.get("executed") is False and spec.get("edges_unchanged") is False + ok &= st["state"] in ("baseline", "installed") ids = [t["node"] for t in spec["transitions"]] ok &= len(ids) == len(set(ids)) and len(ids) >= 1 for t in spec["transitions"]: @@ -264,12 +382,14 @@ def check_transitions(root, spec): ok &= t["kind"] == "region" and p.get("coverage_source") in ids ok &= not t["node"].startswith(("hist.", "eng.", "regional.")) # component nodes: one per byte identity, fingerprinted to the inventory, PROVED_REVIEWED evidence records, - # none for bytes the live graph already carries with a fingerprint (Codex 4139312869 on Math-#160) + # none for bytes the live graph already carries with a fingerprint (Codex 4139312869 on Math-#160); once installed, + # the only live node on a component source is the component itself comps = spec["proposed_graph_nodes"] cids = [c["id"] for c in comps] - live_fp_sources = {n.get("source") for n in graph["nodes"].values() - if isinstance(n, dict) and n.get("fingerprint") and n.get("source")} - ok &= len(cids) == len(set(cids)) and not (set(cids) & set(graph["nodes"])) and len(comps) == spec["nodes_added"] + live_fp_sources = {n.get("source") for nid, n in graph["nodes"].items() + if isinstance(n, dict) and n.get("fingerprint") and n.get("source") and nid not in cids} + ok &= len(cids) == len(set(cids)) and len(comps) == spec["nodes_added"] + ok &= (set(cids) <= set(graph["nodes"])) if installed else not (set(cids) & set(graph["nodes"])) ok &= len({c["source"] for c in comps}) == len(comps) for c in comps: ok &= c["kind"] == "reading_rule_component" and c["classification"] == "PROVED_REVIEWED" and c["controlling"] is False @@ -280,7 +400,8 @@ def check_transitions(root, spec): ok &= all(x in ids + cids for x in consumers) and len(consumers) >= 1 edges_new = spec["proposed_graph_edges"] known = set(graph["nodes"]) | set(cids) - live_keys = {(e["from"], e["to"], e["relation"]) for e in graph["edges"]} + base = strip(spec, graph) # the register without the proposal + live_keys = {(e["from"], e["to"], e["relation"]) for e in base["edges"]} seen = set() for e in edges_new: ok &= {"from", "to", "required", "relation"} <= set(e) and type(e["required"]) is bool @@ -293,10 +414,20 @@ def check_transitions(root, spec): if not ok: return False, None new = apply(spec, graph) + replay = apply(spec, base) nodes = new["nodes"] edges = new["edges"] - ok &= edges[:len(graph["edges"])] == graph["edges"] and len(edges) == len(graph["edges"]) + len(edges_new) + if installed: + ok &= new == graph # the live graph carries the proposal exactly: apply is a no-op + else: + ok &= base == graph and replay == new # strip is a no-op on the baseline register + ok &= edges[:len(graph["edges"])] == graph["edges"] and len(edges) == len(graph["edges"]) + (0 if installed else len(edges_new)) ok &= all(graph["nodes"][k] == nodes[k] for k in graph["nodes"] if k not in ids) # only the eight live nodes change + for t in spec["transitions"]: # the replay from the pre-image reproduces every object + ok &= matches(replay["nodes"][t["node"]], proposed_fields(t["proposed"])) + ok &= matches(nodes[t["node"]], proposed_fields(t["proposed"])) + for c in comps: + ok &= matches(replay["nodes"][c["id"]], component_fields(c)) and matches(nodes[c["id"]], component_fields(c)) for t in spec["transitions"]: nid = t["node"] req = [e["to"] for e in edges if e["from"] == nid and e["required"] is True] @@ -312,7 +443,20 @@ def check_transitions(root, spec): for c in comps: # component nodes' own required premises req = [e["to"] for e in edges if e["from"] == c["id"] and e["required"] is True] ok &= all(nodes[d]["classification"] == "PROVED_REVIEWED" for d in req) - return bool(ok), new + # the installed state, simulated on the baseline register (the live one once installed): the executed graph is + # accepted exactly, and re-applying the proposal to it is a no-op; a drifted or partial install is rejected + sim = copy.deepcopy(new) + if MUT == "installed-drift": + sim["nodes"][cids[0]]["fingerprint"] = "0" * 64 + if MUT == "partial-install": + t4 = next(t for t in spec["transitions"] if t["node"] == D4_NODE) + sim["nodes"][D4_NODE]["classification"] = t4["current"]["classification"] + sim_st = installed_state(sim, spec) + ok &= sim_st["state"] == "installed" and apply(spec, sim) == sim and sim_st["mismatched"] == [] + # the pre-image of the applied graph carries the proposed metadata under the current classifications: a partial + # install, never baseline (Codex 4143661511) + ok &= installed_state(strip(spec, new), spec)["state"] == "partial" + return bool(ok), {"new": new, "base": base, "replay": replay, "state": st["state"]} def load_hard_gate(root): hg_spec = importlib.util.spec_from_file_location("hard_gate", root / HARD_GATE) @@ -321,20 +465,27 @@ def load_hard_gate(root): return hg -def check_gate(root, spec, new): - if new is None: +def check_gate(root, spec, builds): + """The proposal replayed from the register without it (strip) through the hard gate: in the baseline state that is + the live graph against the proposed one; in the installed state the pre-image against its re-application, plus + the installed-state facts (nothing left to apply, this record's objects unheld).""" + if builds is None: return False, {} + new, old, replay, state = builds["new"], builds["base"], builds["replay"], builds["state"] hg = load_hard_gate(root) - old = json.loads((root / GRAPH).read_text(encoding="utf-8")) + live = json.loads((root / GRAPH).read_text(encoding="utf-8")) try: hg.validate_graph_fail_closed(new) - rep_new = hg.closure_report(new) + hg.validate_graph_fail_closed(replay) + rep_new = hg.closure_report(replay) rep_old = hg.closure_report(old) - ri = hg.reverse_impact_between(old, new) + rep_live = hg.closure_report(new) + ri = hg.reverse_impact_between(old, replay) + ri_live = hg.reverse_impact_between(live, new) except Exception: return False, {} ok = rep_new.get("gate_ok") is True and not rep_new.get("illegal_controlling") - ok &= rep_old.get("gate_ok") is True + ok &= rep_old.get("gate_ok") is True and rep_live.get("gate_ok") is True ok &= not any(n.get("controlling") for n in new["nodes"].values()) changed = sorted([t["node"] for t in spec["transitions"]] + [c["id"] for c in spec["proposed_graph_nodes"]]) imp = ri.get("impacted") if isinstance(ri, dict) else None @@ -342,9 +493,19 @@ def check_gate(root, spec, new): if isinstance(imp, list): for x in imp: names.append(x if isinstance(x, str) else str(x.get("node") or x.get("id") or x)) - # loss-only rule: every changed node is itself in the impacted set - ok &= isinstance(ri, dict) and set(changed) <= set(names) - return bool(ok), {"changed_nodes": changed, "impacted": sorted(set(names)), "reverse_impact_keys": sorted(ri.keys()) if isinstance(ri, dict) else []} + # loss-only rule: every changed node is itself in the impacted set, and the replay changes every one of them + ok &= isinstance(ri, dict) and set(changed) <= set(names) and set(changed) <= set(ri.get("changed_nodes", [])) + # this record's objects are unheld once applied: every required premise PROVED_REVIEWED + held = {h.get("node") for h in rep_live.get("hold_proposals", [])} + ok &= not (set(changed) & held) + if state == "installed": + ok &= ri_live.get("changed_nodes") == [] and ri_live.get("impacted") == [] # nothing left to apply + return bool(ok), {"register_state": "installed", + "replay": "the proposal replayed from the pre-image (strip) on the installed register: loss-only rule " + "and unheld objects asserted; the impacted set is not pinned post-execution"} + ok &= ri_live.get("changed_nodes") == ri.get("changed_nodes") and ri_live.get("impacted") == ri.get("impacted") + return bool(ok), {"register_state": "baseline", "changed_nodes": changed, "impacted": sorted(set(names)), + "reverse_impact_keys": sorted(ri.keys())} def check_interface(): @@ -455,7 +616,9 @@ def check_d4_duplicate(root, spec): ok &= dup.get("source") == t["proposed"]["source"] == want["source"] ok &= dup.get("component_of") == want["component_of"] ok &= any("main#76" in str(b.get("review")) and b.get("verdict") == "ACCEPT" for b in dup.get("review_basis", [])) - ok &= old.get("fingerprint") == dup.get("fingerprint") and old.get("classification") == t["current"]["classification"] + graph = json.loads((root / GRAPH).read_text(encoding="utf-8")) + expect = t["proposed" if installed_state(graph, spec)["state"] == "installed" else "current"]["classification"] + ok &= old.get("fingerprint") == dup.get("fingerprint") and old.get("classification") == expect return bool(ok) @@ -484,14 +647,14 @@ def snapshot(root, graph): return out -def check_propagation(root, spec, new): +def check_propagation(root, spec, builds): """Two-commit mutations on the proposed graph through the production loss-only rule (reverse_impact_between with source snapshots): evidence and consumed-source changes must reach the objects they support (OpenAI 5360320845, 5360327058; Codex 4139807558, 4139807567). Nothing scientific is decided here.""" - if new is None: + if builds is None: return False, {} hg = load_hard_gate(root) - g = copy.deepcopy(new) + g = copy.deepcopy(builds["new"]) if MUT == "region-unlinked": g["edges"] = [e for e in g["edges"] if e.get("relation") != "covered_by"] if MUT == "review-metadata-only": @@ -555,9 +718,10 @@ def main(): root = pathlib.Path(".").resolve() spec = load_spec(root) ident = identities_ok(root) - trans_ok, new = check_transitions(root, spec) - gate_ok, gate = check_gate(root, spec, new) - prop_ok, prop = check_propagation(root, spec, new) + trans_ok, builds = check_transitions(root, spec) + gate_ok, gate = check_gate(root, spec, builds) + prop_ok, prop = check_propagation(root, spec, builds) + state = installed_state(json.loads((root / GRAPH).read_text(encoding="utf-8")), spec)["state"] iface = check_interface() checks = {"IDENTITIES": ident, "VERDICTS": ident and check_verdicts(root), "BASELINE": check_baseline(root, spec), "TRANSITIONS": trans_ok, "GATE": gate_ok, "PROPAGATION": prop_ok, @@ -565,6 +729,7 @@ def main(): "D4_DUPLICATE": check_d4_duplicate(root, spec)} passed = all(checks.values()) and len(checks) == 9 print(json.dumps({"object": "REGISTER-ALIGNMENT-20260930-v1", "checks": checks, "passed": passed, + "register_state": state, "inventory_files": len(INVENTORY), "transitions": len(spec["transitions"]), "component_nodes": len(spec["proposed_graph_nodes"]), "edges_added": len(spec["proposed_graph_edges"]), "gate": gate, "propagation": prop, @@ -575,9 +740,10 @@ def main(): "(N5) Simpson quadrature at three parameter points", "(N4) example uniform tail on a grid"], "results": iface}, - "scope": "identity, verdict-row, live-baseline, transition-shape, hard-gate replay, two-commit propagation, " - "interface arithmetic (exact and numerical parts labelled), filesystem-negative and live D4-duplicate " - "checks; no mathematics is re-proved; nothing is written"}, indent=2, sort_keys=True)) + "scope": "identity, verdict-row, live-register (baseline or exactly installed), transition-shape, hard-gate " + "replay from the pre-image, two-commit propagation, interface arithmetic (exact and numerical parts " + "labelled), filesystem-negative and live D4-duplicate checks; no mathematics is re-proved; nothing is " + "written"}, indent=2, sort_keys=True)) return 0 if passed else 1 diff --git a/reviews/register_execution_readiness_20260930/README.md b/reviews/register_execution_readiness_20260930/README.md new file mode 100644 index 000000000..299adcab6 --- /dev/null +++ b/reviews/register_execution_readiness_20260930/README.md @@ -0,0 +1,138 @@ +# Register execution readiness — Math-#167, #160 and #173 against their own checkers after execution + +**Object:** REGISTER-EXECUTION-READINESS-20260930-v1. +**Author:** Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3` — the same session that authored the +three records (author-side; exposure stated in §5). **Read at:** Math- `main` `dda8991` (30 September 2026; Math-#177 merged). +**Effect:** engineering readiness only. Nothing is executed here: `GRAPH.json`, `SELECTOR_REGION.json`, `STATUS.md`, +`PROOF_INDEX.md` and the catalog are untouched, no proposal changes, no classification changes, `lemma_closed`, prizes +and premises are untouched. Scientific effect: NONE. + +## 1. The finding + +The three merged declarative records propose register transitions for a **non-Claude lane** to execute: + +| record | merged at | proposes | +| --- | --- | --- | +| Math-#167 `reviews/register_alignment_20260930` | `fa1cf7b` | eight node flips (D2, D3, D4, D5-annulus, D6, the RN count interface, two regions) to `PROVED_REVIEWED`, eight evidence component nodes, sixteen edges | +| Math-#160 `reviews/c6_witness_collision_reconciliation_20260929` | `8d48d02` | the C6 discharge: 22 nodes (aggregate, residual node `OPEN_ACTIVE`, supersession node, components), 49 edges, six selector cells in three regions, the witness node to `PROVED_REVIEWED` (step 4) | +| Math-#173 `reviews/c6_residual_closure_20260930` | `30106e1` | the residual node to `PROVED_REVIEWED` on two evidence paths, ten components, the deferred old-node edges | + +Composed in that order on a scratch copy of `main` `dda8991` (`execution_dryrun.py`, §3), the executed register is +sound for the hard gate: + +| | live `dda8991` | executed | +| --- | --- | --- | +| nodes / edges | 49 / 55 | 88 / 131 | +| `validate_graph_fail_closed` | OK | OK | +| `closure_report.gate_ok`, illegal controlling | true, none | true, none | +| hold proposals | `eng.main-pr87-crosswalk`, `hist.ALLCELL-FDZ-Q4`, `hist.ENV-RESCOV`, `math.rn-fixed-annulus-window`, `math.rn-fixed-remote-window`, `math.rn-mesoscopic-reduction` | the first three only: **no new hold**, three cleared | +| `reverse_impact_between` (source snapshots supplied) | — | 49 changed, 51 impacted | +| `d4_region_complement.open_complement` | — | empty; the two D4/D5 regions `PROVED_REVIEWED` with their coverage sources | + +After execution: the eight Math-#167 nodes, `math.rn-region.witness-collision`, its residual node and the aggregate +`math.c6-witness-collision-factorial-moment` are `PROVED_REVIEWED` and unheld; `regional.shrinking-regions.analytic-route` +is `SUPERSEDED_NONBLOCKING`; `math.rn-mesoscopic-reduction` stays `AUTHOR_SIDE_REDUCTION` (its hold clears because its +required premises are now `PROVED_REVIEWED`; nothing promotes it). + +**But the three records' own workflows would have gone red on the executing lane's pull request.** All three trigger on +`frontiers/downstream_gate_20260925/GRAPH.json` (and Math-#160's and #173's on `SELECTOR_REGION.json`), and against the +executed copy, before this packet: + +- Math-#167 `alignment_check.py`: `BASELINE`, `TRANSITIONS`, `GATE`, `PROPAGATION`, `D4_DUPLICATE` false. The checker + asserted the pre-execution classifications of the eight nodes, required its component ids to be absent, and its + `apply()` re-added the sixteen live edges, so the hard gate rejected the applied graph (`duplicate or contradictory + edge record`). +- Math-#160 `reconciliation_check.py`: `TRANSITIONS` false (its own installed nodes counted as live duplicates of their + sources); `SELECTOR` would have failed as soon as the six cells were applied (it asserted the three region ids still open). +- Math-#173 `residual_check.py`: every check true, but its printed report is not `RESULTS.json` (the per-stage gate + report differs between the two states by construction), so the workflow's byte comparison failed; and its + `installed-drift` mutant was a no-op on the installed register, so the workflow's mutant rule failed as well. + +## 2. What this packet changes (no proposal changes) + +- **Two accepted register states, fail-closed.** Each checker now accepts the live register in exactly two states: + *baseline* (nothing of its proposal live) and *installed* (all of it, exactly: every proposed field of every proposed + or flipped node, every component node on every proposed key, every proposed edge). Anything in between, any drift on a + proposed key, any other live fingerprinted node on a proposed source, is rejected. Math-#160 additionally accepts the + residual node promoted as Math-#173 proposes it, the witness node open (step 4 pending) or `PROVED_REVIEWED` with all + its evidence edges live, and the selector table untouched or carrying every proposed cell with the three region ids + covered. Math-#167's `apply()` is idempotent and its pre-image `strip()` lets the hard-gate replay run from the register + without the proposal in either state; once installed, `apply` is the identity and the record's objects are unheld. + After Codex review 5365065925 on Math-#183: Math-#167's baseline also pins the eight nodes' proposal-written fields + to their digests at `dda8991` (metadata installed under the old classification is partial); Math-#160 accepts the + installed selector table only when the graph carries the proposal, and the open witness node with none of its + proposed edges; Math-#173 accepts exactly baseline or installed (its interim shape is replayed, not accepted live). +- **Pinned outputs for both states.** Each checker prints `register_state`; each packet carries `RESULTS.json` (baseline) + and `RESULTS_INSTALLED.json` (installed), and the workflows compare the output with the file the reported state names. + The installed outputs contain no live-dependent lists (the post-execution impacted sets depend on the other landed + records), and they are identical across the three execution shapes of §3, so **the executing lane does not regenerate + anything in the three packets**. +- **Mutants in either state.** `installed-drift`, `partial-install` and `text-preinstalled` added to Math-#167; + `installed-drift`, `partial-install`, `selector-ahead` and `witness-edges-partial` to Math-#160; `partial-install` to + Math-#173, whose simulation of the installed state (and its `installed-drift` mutant) now runs on the installed + register too. Each new rule is asserted by a permanent self-test in every run, and its mutant disables the rule, so + it is rejected in either register state. Every mutant of every checker (44) is rejected on the baseline register and + on the executed copy (`--mutants`). +- **Records:** Math-#167 `RECONCILIATION.md` v1.4 (§0 revision note, §6), Math-#160 v1.8 (§0, §8), Math-#173 v1.6 (§0, §6; + its own bytes are re-pinned in `INVENTORY` and in the record node's fingerprint, as the record requires of itself). +- **This packet:** `execution_dryrun.py` and the workflow `register-execution-readiness.yml`, which composes the three + proposals on a scratch copy on every change to the three packets, the register surfaces or the hard gate, and requires + the three checkers green in the installed state, byte-identical to their pinned installed outputs, with every mutant + rejected, in three shapes: the full composition, `--skip-old-node-move` (Math-#160 steps 1–3 only) and + `--selector-node-only`. After a real execution the composition is the identity and the workflow stays green. + +## 3. The dry run + +From the repository root (standard library only; a temporary copy is used unless `--out DIR`: a path outside the +repository, neither inside it nor one of its parents, that does not exist or is an empty directory; the script never +deletes anything). `--write-installed-results` (maintenance of this packet) writes the pinned installed outputs only +after every checker, both interpreter modes and, if requested, every mutant have passed. + +``` +python -B -S reviews/register_execution_readiness_20260930/execution_dryrun.py --mutants +python -B -S reviews/register_execution_readiness_20260930/execution_dryrun.py --skip-old-node-move +python -B -S reviews/register_execution_readiness_20260930/execution_dryrun.py --selector-node-only +``` + +Composition, as the records state it: (1) Math-#167 `alignment_check.apply`; (2) Math-#160 `execution_order` steps 1–3 +on the main path (the residual node created separately, `OPEN_ACTIVE`; the supersession node and its three +`regional_bypass_only` edges; the component nodes; every proposed edge not leaving the witness node; the selector cells +and the three region ids moved from open to covered), then step 4 (the witness node `PROVED_REVIEWED`, given the fields +of Math-#173's deferred transition, its evidence edges added); (3) Math-#173 `residual_check.build(·, "final")`, then the +deferred old-node edges (one new: `witness → residual`; `witness → aggregate` is already Math-#160's). The witness node's +text fields are not constrained by any of the three checkers; the lane may word them as it decides. + +## 4. For the executing lane (non-Claude) + +- **Order.** Math-#167 at any time, in one commit. Math-#160 steps 1–3 **before** Math-#173 (the palm-proof node's fields + are Math-#160's; Math-#173 reuses it); the witness node's own evidence edges belong to step 4 (none of them while it is + open, all of them once it is `PROVED_REVIEWED`). Math-#173 in one commit (steps 1–2 together: the interim shape with the + residual still `OPEN_ACTIVE` is not an accepted live state). Math-#160 step 4 and Math-#173's deferred edges together, + or step 4 later: both shapes are accepted (§3). Executing Math-#173 first would create the palm node with Math-#173's fields, which + Math-#160's checker rejects as a mismatch until the node carries Math-#160's fields. +- **Not accepted (the checkers stay red):** a partial install of any record; a proposed key drifted on any installed + node; Math-#160's §1a register-equivalent alternative (no separate residual node; Math-#173 presupposes the node); + a selector table with some of the six cells; the three region ids moved without the cells or the cells without the ids. +- **Surfaces outside the graph.** Math-#160's `OBLIGATION` check requires `PROOF_INDEX.md` and + `reviews/candidates_pending_20260928/CANDIDATES.md` to keep either their quoted C6 sentences or a reference to + `reviews/c6_witness_collision_reconciliation_20260929`; a rewrite of the C6 rows should cite that path. `STATUS.md`, + `PROOF_INDEX.md` and catalog rows are the records' proposals, not touched here. +- **Nothing to regenerate** in the three packets (§2). The three workflows and the readiness workflow run on the + execution pull request and should be green; if one is red, the cause is a difference between the executed register and + the proposals as written, and the checker's `register_state` and check names locate it. + +## 5. Review of this packet + +Codex review 5365065925 on Math-#183 (six findings, all taken): selector table accepted ahead of the graph (4143661492); +baseline nodes not checked on the proposal-written fields (4143661511); Math-#173 labelling partial component installs +baseline (4143661501); the open witness node accepting a subset of its edges (4143661519); `--out` deleting an existing +path (4143661496); installed results written before validation (4143661525). Each checker rule now has a self-test in +every run and a mutant that disables it; the helper never deletes and writes only after a fully valid run. + +## 6. Exposure and independence + +The author of this packet is the author of the three records; the packet was written after this session's own dry run +found the failures of §1. A read of this packet by the same account, or by any Claude session, carries no organizational +independence; the executing lane is non-Claude and decides whether to take the checker changes before or with the +execution. `execution_dryrun.py` decides nothing scientific and writes nothing to the repository unless invoked with +`--write-installed-results`, which only maintains this packet's pinned installed outputs and is never run by a workflow. diff --git a/reviews/register_execution_readiness_20260930/execution_dryrun.py b/reviews/register_execution_readiness_20260930/execution_dryrun.py new file mode 100644 index 000000000..a083afa58 --- /dev/null +++ b/reviews/register_execution_readiness_20260930/execution_dryrun.py @@ -0,0 +1,271 @@ +"""Register execution dry run (standard library only; nothing is written to the repository unless asked). + +Composes the three merged declarative proposals, in their stated order, on a scratch copy of the repository: + 1. Math-#167 reviews/register_alignment_20260930/PROPOSED_TRANSITIONS.json (alignment_check.apply) + 2. Math-#160 reviews/c6_witness_collision_reconciliation_20260929/PROPOSED_TRANSITIONS.json (execution_order steps 1-4, + main path: residual node created separately; selector cells per selector_region_proposal; the old node's fields as + Math-#173's deferred transition proposes them) + 3. Math-#173 reviews/c6_residual_closure_20260930/PROPOSED_TRANSITIONS.json (residual_check.build 'final', then the + deferred old-node edges once Math-#160 step 4 is applied) +then validates the executed graph with the downstream hard gate and runs the three records' checkers against the +executed copy: each must pass, report its register as 'installed' and print its packet's RESULTS_INSTALLED.json byte +for byte under both interpreter modes. With --mutants every mutant of every checker must be rejected on the executed +copy as well. + +Usage, from the repository root: + python -B -S reviews/register_execution_readiness_20260930/execution_dryrun.py [--out DIR] [--skip-old-node-move] + [--selector-node-only] [--mutants] [--write-installed-results] + --out DIR keep the executed copy in DIR: a path outside the repository (not inside it, not one of its + parents) that does not exist or is an empty directory; nothing is ever deleted; default: a + temporary directory + --skip-old-node-move stop after Math-#160 steps 1-3: witness node left OPEN_ACTIVE, Math-#173's deferred edges not applied + --selector-node-only Math-#160's node-only alternative for the selector table (table unchanged) + --mutants also run every checker mutant on the executed copy + --write-installed-results maintenance of this packet only: write each checker's installed-state output into its packet + as RESULTS_INSTALLED.json, and only after every checker (and every mutant, if requested) + has passed (then the normal run compares against it) +Exit status 0 iff the executed graph validates and every checker (and mutant, if requested) behaves as required. +Scientific effect: NONE. This is not an execution: the repository's GRAPH.json and SELECTOR_REGION.json are not touched. +""" +import argparse +import copy +import hashlib +import importlib.util +import json +import pathlib +import re +import shutil +import subprocess +import sys +import tempfile + +GRAPH = "frontiers/downstream_gate_20260925/GRAPH.json" +SELECTOR = "frontiers/downstream_gate_20260925/SELECTOR_REGION.json" +HARD_GATE = "frontiers/downstream_gate_20260925/hard_gate.py" +PACKETS = { + "Math-#167": ("reviews/register_alignment_20260930", "alignment_check.py"), + "Math-#160": ("reviews/c6_witness_collision_reconciliation_20260929", "reconciliation_check.py"), + "Math-#173": ("reviews/c6_residual_closure_20260930", "residual_check.py"), +} +WIT = "math.rn-region.witness-collision" +RES = "math.rn-region.witness-collision.leading-mass-localization" +AGG = "math.c6-witness-collision-factorial-moment" +SUPERSESSION = "regional.shrinking-regions.analytic-route" +EIGHT_EXTRA = ("math.rn-mesoscopic-reduction",) + + +def load_module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + argv, sys.argv = sys.argv, [str(path)] + try: + spec.loader.exec_module(mod) + finally: + sys.argv = argv + return mod + + +def edge_key(e): + return (e["from"], e["to"], e["required"], e["relation"]) + + +def add_edges(graph, edges): + have = {(e["from"], e["to"], e["relation"]) for e in graph["edges"]} + added = 0 + for e in edges: + key = (e["from"], e["to"], e["relation"]) + if key in have: + continue + graph["edges"].append({"from": e["from"], "to": e["to"], "required": e["required"], "relation": e["relation"]}) + have.add(key) + added += 1 + return added + + +def compose(out, skip_old_node_move, selector_node_only): + hg = load_module("hard_gate", out / HARD_GATE) + al = load_module("alignment_check", out / PACKETS["Math-#167"][0] / PACKETS["Math-#167"][1]) + rc = load_module("residual_check", out / PACKETS["Math-#173"][0] / PACKETS["Math-#173"][1]) + g0 = json.loads((out / GRAPH).read_text(encoding="utf-8")) + sel0 = json.loads((out / SELECTOR).read_text(encoding="utf-8")) + report = {"live": {"nodes": len(g0["nodes"]), "edges": len(g0["edges"])}} + rep0 = hg.closure_report(g0) + holds0 = {h["node"] for h in rep0["hold_proposals"]} + report["live"]["gate_ok"] = rep0["gate_ok"] + report["live"]["holds"] = sorted(holds0) + # 1. Math-#167 + spec167 = al.load_spec(out) + g1 = al.apply(spec167, g0) + report["step_167"] = {"nodes": len(g1["nodes"]), "edges": len(g1["edges"]), + "flipped": sorted(t["node"] for t in spec167["transitions"])} + # 2. Math-#160, steps 1-3 (and 4 unless skipped) + spec160 = json.loads((out / PACKETS["Math-#160"][0] / "PROPOSED_TRANSITIONS.json").read_text(encoding="utf-8")) + spec173 = rc.load_spec(out) + g2 = copy.deepcopy(g1) + kept = [] + for n in spec160["proposed_graph_nodes"]: + if n["id"] in g2["nodes"]: + kept.append(n["id"]) + continue + g2["nodes"][n["id"]] = {k: v for k, v in n.items() if k != "id"} + added = add_edges(g2, [e for e in spec160["proposed_graph_edges"] if e["from"] != WIT]) + sel = copy.deepcopy(sel0) + srp = spec160["selector_region_proposal"] + if not selector_node_only: + for s, v in srp["cells"].items(): + for reg in srp["regions"]: + sel["selectors"][s][reg] = v + ids = ["math.rn-region." + reg for reg in srp["regions"]] + sel["covered_region_ids"] = list(sel["covered_region_ids"]) + [i for i in ids if i not in sel["covered_region_ids"]] + sel["open_region_ids"] = [i for i in sel["open_region_ids"] if i not in ids] + report["step_160"] = {"nodes": len(g2["nodes"]), "edges_after_steps_1_3": len(g2["edges"]) , "nodes_already_live": kept, + "selector": "node-only alternative (table unchanged)" if selector_node_only else "cells and region ids per selector_region_proposal"} + if not skip_old_node_move: + t1 = spec173["transitions"][1] + p = t1["proposed"] + w = g2["nodes"][WIT] + w.update({"classification": p["classification"], "controlling": p["controlling"], "fingerprint": p["fingerprint"], + "scope": p["scope"], "explicit_limits": p["explicit_limits"], "review_disposition": p["review_disposition"], + "review_sources": [r["ref"] for r in p["review_sources"]], + "review_basis": [{"review": r["ref"], "provider": r.get("provider", "unstated"), "verdict": r.get("verdict", "")} + for r in p["review_sources"]]}) + if p.get("notes"): + w["notes"] = p["notes"] + added += add_edges(g2, [e for e in spec160["proposed_graph_edges"] if e["from"] == WIT]) + report["step_160"]["step_4"] = "witness node PROVED_REVIEWED with Math-#173's deferred-transition fields; its evidence edges added" + else: + report["step_160"]["step_4"] = "not applied (--skip-old-node-move): witness node left as it is" + report["step_160"]["edges_added"] = added + # 3. Math-#173 + _, g3 = rc.build(spec173, g2, "final") + deferred = [e for e in spec173["proposed_graph_edges"] if e.get("deferred_with")] + d_added = 0 if skip_old_node_move else add_edges(g3, deferred) + report["step_173"] = {"nodes": len(g3["nodes"]), "edges": len(g3["edges"]), "deferred_edges_applied": d_added, + "residual": g3["nodes"][RES]["classification"]} + # validate + hg.validate_graph_fail_closed(g3) + rep3 = hg.closure_report(g3) + holds3 = {h["node"]: h.get("unsatisfied_required") for h in rep3["hold_proposals"]} + snap_old, snap_new = rc.snapshot(out, g0), rc.snapshot(out, g3) + ri = hg.reverse_impact_between(g0, g3, old_sources=snap_old, new_sources=snap_new) + watch = [WIT, RES, AGG, SUPERSESSION, *EIGHT_EXTRA, *(t["node"] for t in spec167["transitions"])] + report["executed"] = { + "nodes": len(g3["nodes"]), "edges": len(g3["edges"]), "validate_graph_fail_closed": "OK", + "gate_ok": rep3["gate_ok"], "illegal_controlling": rep3.get("illegal_controlling"), + "holds_new": {k: v for k, v in holds3.items() if k not in holds0}, "holds_cleared": sorted(holds0 - set(holds3)), + "classifications": {nid: g3["nodes"].get(nid, {}).get("classification") for nid in watch}, + "held": sorted(nid for nid in watch if nid in holds3), + "reverse_impact": {"changed_nodes": len(ri["changed_nodes"]), "impacted": len(ri["impacted"]), + "source_snapshots_supplied": ri["source_snapshots_supplied"]}, + "d4_region_complement": hg.d4_region_complement(g3) if hasattr(hg, "d4_region_complement") else None, + } + (out / GRAPH).write_text(json.dumps(g3, indent=2, ensure_ascii=False) + "\n", encoding="utf-8") + (out / SELECTOR).write_text(json.dumps(sel, indent=2, ensure_ascii=False) + "\n", encoding="utf-8") + return report + + +def run_checkers(root, out, mutants, write_installed): + """Run every checker (both interpreter modes, and every mutant if asked) on the executed copy; then, only if all of + that passed, write the pinned installed outputs if asked; then compare with the pinned files.""" + results, outputs = {}, {} + valid = True + for name, (pdir, script) in PACKETS.items(): + entry = {} + outs = {} + for flags in (("-B", "-S"), ("-B", "-O", "-S")): + r = subprocess.run([sys.executable, *flags, str(out / pdir / script)], cwd=out, capture_output=True, timeout=900) + outs[flags] = r.stdout + try: + payload = json.loads(r.stdout) + except Exception: + payload = {} + entry[" ".join(flags)] = {"rc": r.returncode, "checks": payload.get("checks"), "passed": payload.get("passed"), + "register_state": payload.get("register_state")} + valid &= r.returncode == 0 and payload.get("passed") is True and payload.get("register_state") == "installed" + entry["modes_identical"] = outs[("-B", "-S")] == outs[("-B", "-O", "-S")] + valid &= entry["modes_identical"] + if mutants: + src = (out / pdir / script).read_text(encoding="utf-8") + names = re.findall(r'"([a-z0-9-]+)"', re.search(r"MUTANTS = \((.*?)\)\n", src, re.S).group(1)) + rejected, not_rejected = [], [] + for m in names: + r = subprocess.run([sys.executable, "-B", "-S", str(out / pdir / script), "--mutant", m], cwd=out, + capture_output=True, timeout=900) + (rejected if r.returncode == 1 else not_rejected).append(m) + entry["mutants_rejected"] = len(rejected) + entry["mutants_not_rejected"] = not_rejected + valid &= not not_rejected and len(rejected) == len(names) + results[name] = entry + outputs[name] = outs[("-B", "-S")] + ok = valid + for name, (pdir, script) in PACKETS.items(): + entry = results[name] + pinned = root / pdir / "RESULTS_INSTALLED.json" + if write_installed and valid: # never on a failed run (Codex 4143661525) + pinned.write_bytes(outputs[name]) + entry["written"] = str(pinned.relative_to(root)) + elif write_installed: + entry["written"] = None + if pinned.exists(): + entry["matches_RESULTS_INSTALLED"] = pinned.read_bytes() == outputs[name] + entry["RESULTS_INSTALLED_sha256"] = hashlib.sha256(pinned.read_bytes()).hexdigest() + ok &= entry["matches_RESULTS_INSTALLED"] + else: + entry["matches_RESULTS_INSTALLED"] = None + ok = False + return ok, results + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--out") + ap.add_argument("--skip-old-node-move", action="store_true") + ap.add_argument("--selector-node-only", action="store_true") + ap.add_argument("--mutants", action="store_true") + ap.add_argument("--write-installed-results", action="store_true") + args = ap.parse_args() + root = pathlib.Path(".").resolve() + for rel in (GRAPH, SELECTOR, HARD_GATE, *(p + "/" + s for p, s in PACKETS.values())): + if not (root / rel).is_file(): + print(json.dumps({"error": "run from the repository root; missing " + rel})) + return 2 + tmp = None + if args.out: + out = pathlib.Path(args.out).resolve() + if root == out or root in out.parents or out in root.parents: + print(json.dumps({"error": "--out must lie outside the repository (neither inside it nor one of its parents)"})) + return 2 + if out.exists() and (not out.is_dir() or any(out.iterdir())): # nothing is ever deleted (Codex 4143661496) + print(json.dumps({"error": "--out must not exist or must be an empty directory; nothing is deleted"})) + return 2 + else: + tmp = tempfile.mkdtemp(prefix="register-dryrun-") + out = pathlib.Path(tmp) + shutil.copytree(root, out, symlinks=False, dirs_exist_ok=True, + ignore=shutil.ignore_patterns(".git", "__pycache__", "*.pyc")) + for p in out.rglob("__pycache__"): + shutil.rmtree(p, ignore_errors=True) + scenario = {"old_node_move": not args.skip_old_node_move, "selector": "node-only" if args.selector_node_only else "cells"} + try: + try: + report = compose(out, args.skip_old_node_move, args.selector_node_only) + composed = True + except Exception as ex: + report, composed = {"composition_error": repr(ex)[:500]}, False + ok, checkers = (run_checkers(root, out, args.mutants, args.write_installed_results) if composed else (False, {})) + for p in out.rglob("__pycache__"): + shutil.rmtree(p, ignore_errors=True) + finally: + if tmp is not None: + shutil.rmtree(tmp, ignore_errors=True) + payload = {"object": "REGISTER-EXECUTION-DRYRUN-20260930-v1", "scenario": scenario, "composition": report, + "checkers": checkers, "mutants_run": args.mutants, "passed": bool(composed and ok), + "scientific_effect": "NONE", "repository_written": bool(args.write_installed_results), + "meaning": "composition of three declarative proposals on a scratch copy; validation by the hard gate; the " + "records' own checkers in their installed state; not an execution, not acceptance"} + print(json.dumps(payload, indent=2, sort_keys=True)) + return 0 if payload["passed"] else 1 + + +if __name__ == "__main__": + sys.exit(main())