diff --git a/reviews/c6_witness_collision_reconciliation_20260929/SOURCE_FILES.json b/reviews/c6_witness_collision_reconciliation_20260929/SOURCE_FILES.json index 84485a8af..2a50517c2 100644 --- a/reviews/c6_witness_collision_reconciliation_20260929/SOURCE_FILES.json +++ b/reviews/c6_witness_collision_reconciliation_20260929/SOURCE_FILES.json @@ -28,9 +28,9 @@ }, { "path": "reconciliation_check.py", - "bytes": 37185, - "sha256": "216926d61676ef9e6ff274aa39be34df78d2a2a19eadbd9928ddfcf011c9b87b", - "git_blob": "8bdd4b6f843cc330dace59f0a8708c87e9b7b72e" + "bytes": 37996, + "sha256": "f13c63fd09beb549339034de82f79902802f0a6e8934db4dc00dacdd43d23fbf", + "git_blob": "3e95763fa20253491de48420230e51ba554693af" }, { "path": "RESULTS_INSTALLED.json", diff --git a/reviews/c6_witness_collision_reconciliation_20260929/reconciliation_check.py b/reviews/c6_witness_collision_reconciliation_20260929/reconciliation_check.py index 8bdd4b6f8..3e95763fa 100644 --- a/reviews/c6_witness_collision_reconciliation_20260929/reconciliation_check.py +++ b/reviews/c6_witness_collision_reconciliation_20260929/reconciliation_check.py @@ -19,6 +19,8 @@ MONOTONE exact enumeration: (n_A)_q <= (n)_q for every sub-count and q <= 4; 2*1{n>=2} <= n(n-1) <= n*Psi for Psi >= n; the Theta(r^3) bracket needs both the upper and the lower row. OPEN_RESIDUAL the open items of section 5 are recorded and the residual node is proposed open. +Every JSON input is parsed strictly: a duplicate key or a NaN/Infinity constant stops the run with passed false and an +input_error, as hard_gate.load_json_strict does (R-2). Mutants (each must fail): allow-symlink, no-hash, drop-edge, stale-fingerprint, executed-flag, close-residual, drop-lower-bound, regional-strict. """ @@ -164,6 +166,26 @@ def no_symlink_on_path(root, path): return not any((root / pathlib.PurePosixPath(*parts[:i])).is_symlink() for i in range(1, len(parts) + 1)) +class InputError(ValueError): + """A JSON input that a strict parse refuses (R-2).""" + + +def load_json(path): + """json.loads that rejects duplicate keys and NaN/Infinity, the rule of hard_gate.load_json_strict (R-2).""" + def pairs(items): + out = {} + for key, value in items: + if key in out: + raise InputError("%s: duplicate JSON key %r" % (path.name, key)) + out[key] = value + return out + + def constant(name): + raise InputError("%s: non-finite JSON constant %s" % (path.name, name)) + + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=pairs, parse_constant=constant) + + def check_identities(root): for path, (sha, blob) in INVENTORY.items(): p = root / path @@ -188,7 +210,7 @@ def check_verdicts(root): def check_obligation(root): - graph = json.loads((root / GRAPH).read_text(encoding="utf-8")) + graph = load_json(root / GRAPH) node = graph["nodes"].get(WITNESS) if not isinstance(node, dict) or node.get("kind") != "region" or node.get("controlling") is not False: return False @@ -199,7 +221,7 @@ def check_obligation(root): ok &= all(graph["nodes"].get(x, {}).get("classification") == "PROVED_REVIEWED" for x in node.get("reading_rule", [])) else: ok = node.get("classification") == "PROVED_REVIEWED" - sel = json.loads((root / SELECTOR).read_text(encoding="utf-8")) + sel = load_json(root / SELECTOR) ok &= "witness-collision" in sel.get("regions", []) index = (root / "PROOF_INDEX.md").read_text(encoding="utf-8") ok &= ("NO COMPLETE PROOF YET: shrinking-separation factorial-moment/collision estimate." in index # through bb429d3 @@ -324,15 +346,15 @@ def installed_state(graph, proposed_nodes, proposed_edges): 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")) + spec = load_json(root / HERE / "PROPOSED_TRANSITIONS.json") + graph = load_json(root / GRAPH) 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")) - graph = json.loads((root / GRAPH).read_text(encoding="utf-8")) + spec = load_json(root / HERE / "PROPOSED_TRANSITIONS.json") + d5 = load_json(root / D5_TRANSITIONS) + graph = load_json(root / GRAPH) 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"]} @@ -495,8 +517,8 @@ def check_selector(root): 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")) + spec = load_json(root / HERE / "PROPOSED_TRANSITIONS.json") + live = load_json(root / SELECTOR) prop = spec["selector_region_proposal"] cells = dict(prop["cells"]) if MUT == "open-cell-left": @@ -562,7 +584,7 @@ def check_open_residual(root): ok = "**Numerical constants**" in text and "leading-mass-localization" in text ok &= "localization of the leading-order mass at scale `r`" in text and "M(R, s_0)" in text ok &= "not supplied by the landed reviewed chain" in text and "candidates only" in text - spec = json.loads((root / HERE / "PROPOSED_TRANSITIONS.json").read_text(encoding="utf-8")) + spec = load_json(root / HERE / "PROPOSED_TRANSITIONS.json") res = next(e for e in spec["graph"] if e["node"] == RESIDUAL) ok &= res["proposed"] == "OPEN_ACTIVE" and MUT != "close-residual" return ok @@ -574,14 +596,20 @@ def main(): ap.add_argument("--mutant", choices=MUTANTS) MUT = ap.parse_args().mutant root = pathlib.Path(".").resolve() - ident = check_identities(root) - checks = {"IDENTITIES": ident, "VERDICTS": ident and check_verdicts(root), "OBLIGATION": check_obligation(root), - "NEGATIVES": check_negatives(root), "TRANSITIONS": check_transitions(root), - "MONOTONE": check_monotone(), "OPEN_RESIDUAL": check_open_residual(root), - "SELECTOR": check_selector(root)} + try: + ident = check_identities(root) + checks = {"IDENTITIES": ident, "VERDICTS": ident and check_verdicts(root), "OBLIGATION": check_obligation(root), + "NEGATIVES": check_negatives(root), "TRANSITIONS": check_transitions(root), + "MONOTONE": check_monotone(), "OPEN_RESIDUAL": check_open_residual(root), + "SELECTOR": check_selector(root)} + state = register_state(root) + except InputError as exc: + print(json.dumps({"object": "C6-WITNESS-COLLISION-RECONCILIATION-20260929-v1", "passed": False, + "input_error": str(exc)}, indent=2, sort_keys=True)) + return 1 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), "register_state": register_state(root), + "inventory_files": len(INVENTORY), "register_state": state, "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)) diff --git a/reviews/register_execution_readiness_20260930/README.md b/reviews/register_execution_readiness_20260930/README.md index 4cc096e6b..4bce440f7 100644 --- a/reviews/register_execution_readiness_20260930/README.md +++ b/reviews/register_execution_readiness_20260930/README.md @@ -17,6 +17,16 @@ proposals carry no compared Boolean below a node's top level (their only compare flags, which the hard gate types exactly); a guard test fails if that ever changes. Pinned outputs, proposals and the workflow mutant list are unchanged. Nothing is executed. +**R-2 successor (6 October 2026).** The same checker parsed GRAPH, SELECTOR_REGION and the proposals with plain +`json.loads`, which keeps the last of a duplicate key and accepts `NaN` and `Infinity`; a GRAPH or SELECTOR_REGION text +with a duplicate witness `classification`, a duplicate `regions` key or a non-finite constant reached the pinned +installed output with exit 0 (disposition [382/6018648978](https://github.com/d6g8k5htny-coder/Math-/pull/382#issuecomment-6018648978)). +Every JSON input now goes through one strict loader with the rule of `hard_gate.load_json_strict`; a refused input prints +`passed: false` with an `input_error` and exits 1. `test_witness_states.py` covers both duplicate kinds and `NaN`, +`Infinity` and `-Infinity` through the full checker and guards the single parse site. Pinned outputs, proposals and the +workflow mutant list are unchanged. `hard_gate.load_selector_region` still parses SELECTOR_REGION loosely; it belongs to +the downstream-gate package and is left to that package's owner. Nothing is executed. + **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). diff --git a/reviews/register_execution_readiness_20260930/test_witness_states.py b/reviews/register_execution_readiness_20260930/test_witness_states.py index fafb51a80..ddb0267ed 100644 --- a/reviews/register_execution_readiness_20260930/test_witness_states.py +++ b/reviews/register_execution_readiness_20260930/test_witness_states.py @@ -54,6 +54,18 @@ def graph_fixture(stage): return graph +def selector_fixture(installed): + selector = json.loads(baseline_bytes("SELECTOR_REGION.json")) + if installed: + proposal = PROPOSAL["selector_region_proposal"] + for name, value in proposal["cells"].items(): + for region in proposal["regions"]: + selector["selectors"][name][region] = value + selector["covered_region_ids"] = proposal["resulting_covered_region_ids"] + selector["open_region_ids"] = proposal["resulting_open_region_ids"] + return selector + + def nested_booleans(value, path=()): """Paths of every Boolean strictly below a node's top level (R-1 class).""" if isinstance(value, dict): @@ -182,16 +194,11 @@ def setUp(self): target.write_bytes(baseline_bytes(name)) def run_graph(self, graph, installed_selector=True): - (self.root / witness.GRAPH).write_text(json.dumps(graph)) - selector = json.loads(baseline_bytes("SELECTOR_REGION.json")) - if installed_selector: - proposal = PROPOSAL["selector_region_proposal"] - for name, value in proposal["cells"].items(): - for region in proposal["regions"]: - selector["selectors"][name][region] = value - selector["covered_region_ids"] = proposal["resulting_covered_region_ids"] - selector["open_region_ids"] = proposal["resulting_open_region_ids"] - (self.root / witness.SELECTOR).write_text(json.dumps(selector)) + return self.run_text(json.dumps(graph), json.dumps(selector_fixture(installed_selector))) + + def run_text(self, graph_text, selector_text): + (self.root / witness.GRAPH).write_text(graph_text) + (self.root / witness.SELECTOR).write_text(selector_text) flags = ["-O"] if sys.flags.optimize else [] run = subprocess.run([sys.executable, "-B", *flags, "-S", str(ENTRY)], cwd=self.root, capture_output=True, timeout=60) @@ -245,6 +252,40 @@ def test_nested_integer_boolean_is_rejected_by_full_checker(self): self.assertNotEqual(run.stdout, (PACKET / "RESULTS_INSTALLED.json").read_bytes()) + def test_duplicate_keys_and_non_finite_constants_are_rejected_by_full_checker(self): + # R-2: a loose parse keeps the last duplicate and accepts NaN/Infinity, so each text below would reach the + # pinned installed output. The checker must refuse the input instead. + graph = json.dumps(graph_fixture("open")) + selector = json.dumps(selector_fixture(True)) + node = '"%s": {' % witness.WITNESS + self.assertEqual(graph.count(node), 1) + self.assertTrue(selector.startswith("{")) + cases = { + "duplicate GRAPH key": (graph.replace(node, node + '"classification": "REFUTED", ', 1), selector, + "duplicate JSON key"), + "duplicate SELECTOR key": (graph, selector.replace("{", '{"regions": [], ', 1), "duplicate JSON key"), + "NaN in GRAPH": (graph.replace(node, node + '"note": NaN, ', 1), selector, "non-finite"), + "-Infinity in GRAPH": (graph.replace(node, node + '"note": -Infinity, ', 1), selector, "non-finite"), + "Infinity in SELECTOR": (graph, selector.replace("{", '{"note": Infinity, ', 1), "non-finite"), + } + for name, (graph_text, selector_text, reason) in cases.items(): + with self.subTest(case=name): + run, result = self.run_text(graph_text, selector_text) + self.assertEqual(run.returncode, 1) + self.assertFalse(result["passed"]) + self.assertIn(reason, result["input_error"]) + self.assertNotEqual(run.stdout, (PACKET / "RESULTS_INSTALLED.json").read_bytes()) + run, result = self.run_text(graph, selector) + self.assertEqual((run.returncode, run.stdout), (0, (PACKET / "RESULTS_INSTALLED.json").read_bytes())) + + def test_every_json_input_goes_through_the_strict_loader(self): + # GRAPH is read in several checks; one strict read is enough to refuse the run, so the full-CLI cases above + # cannot see a single loose call site. This guard keeps json.loads inside load_json only. + source = ENTRY.read_text(encoding="utf-8") + self.assertEqual(source.count("json.loads("), 1) + self.assertIn("object_pairs_hook=pairs, parse_constant=constant)", source) + + class SiblingProposals(unittest.TestCase): """Math-#167 and Math-#173 compare proposed fields with plain equality. That is exact today only because every Boolean they compare on a live node is a top-level controlling flag, which the hard gate types exactly. Fail if a