diff --git a/research/p104-5718-causal-coverage-gap/README.md b/research/p104-5718-causal-coverage-gap/README.md new file mode 100644 index 0000000000..600079cafb --- /dev/null +++ b/research/p104-5718-causal-coverage-gap/README.md @@ -0,0 +1,135 @@ +# The fixed #5719 causal certificate does not cover merged #5718 + +**Audit, not a new κ.** The selected conditional exponent stays +**0.00310045** (`#5599`). This package does not admit or reject the `#5718` +construction. It shows that one published coverage certificate does not apply +to that word. + +## Result + +Let `W0` be the authenticated PR5684 word used by +[PR #5719](https://github.com/CrocSwap/integer-mult-bounds/pull/5719), and let +`W1` be the authenticated word of merged +[PR #5718](https://github.com/CrocSwap/integer-mult-bounds/pull/5718). + +The published `#5719` checker accepts `W0` and returns +`PASS_FIXED_CAUSAL_LEDGER_AND_TYPED_CONTACTS_ONLY`. On the bytes of `W1`, +renamed to the filename it requires, the same checker returns exit 3 and +`BINDING_UNRESOLVED`, with `scientific_falsifier` false and +`coverage_complete` false. The refusal is the pinned 106,613-byte cap. It is +not a scientific verdict on `#5718`. + +An independent census of the same authenticated bytes then separates what +transfers from what does not. + +| Premise named by the `#5719` certificate | On `W1` | +|---|---| +| Schema `p104-r22-reframe/1`, public count 743 | Schema `p104-terminal-main-split-short-cleanup/1`, public count 744, program length 25,546 | +| Strict frame chain, dimensions 0, 1, 3 at frames 3, 598, 396 | Same chain | +| Nine anchor events, each unique at its index | Four anchors occur nowhere. The other five occur once, at displacements 91, 91, 89, 90, and 92 | +| Sole field-712 write in `[823, 14983)` is `ADD 712,747,1` at frame 598 | The sole write there is `ADD 712,748,1` at frame 598, index 13,663 | +| Field-715 moves `3 → 598 → 396` | Those two moves are absent. The only move off frame 3 is `MOVE 715,3,396` at index 15,072 | +| No field-715 observer in `[823, 14983)` | Index 911 is `ADD 206,715,2` at frame 3 | +| One field-340 write in `[11202, 14983)`, the credited provenance `ADD` | Two writes: `ADD 340,344,1` at frame 70, index 11,260, and the credited `ADD` at index 11,293 | +| No field-340 write in the numeric interval `[14654, 14983)` | Still true, and not a transferred proof: index 14,654 and index 14,983 are different operations, the old read now lies inside the interval at 14,744, and the old cut lies at 15,075 | + +The owned `INIT`/`CLEAR` frame sequences of roles 743 through 751 on `W0` +match roles 744 through 752 on `W1` exactly. Role 743 is unused on `W1`. +Role 747 on `W1` therefore reproduces role 746 on `W0`, not role 747. A +uniform label shift describes the lifetimes. It does not make the +certificate's field-747 claim true, and it does not restore the missing +715 chart path. + +The frozen candidate of +[PR #5717](https://github.com/CrocSwap/integer-mult-bounds/pull/5717) is a +third word, SHA256 +`9fd67dd89ed24a644257cd9aef06934ed4c6fbe0441804684a968868f2ef66a8`. Its +published binding names that hash. This package does not rerun the adapter, +so it does not confirm or refute the `#5718` author's report that the adapter +passed. + +## Task and overlap + +Base `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. Card +`supplier-boundary-audit`, scope **refined** to the `#5718` delta named in +that card's first experiment. + +This is item 4 of the eligible list below. The nearest packages are the +inputs: `research/p104-temporal-fixed-independent-audit` states in prose that +its certificate does not transfer, and `research/p104-two-boundary-helper-split` +is the successor. Neither package evaluates the old anchors on the new word. +`research/p104-caller-owned-interface` authenticates a different candidate. + +Ordered eligible list for session r56, rebuilt on 2026-10-27 against +`de5ec2e7a6074068452f45b1a191b5c72832df4a`. Open handoffs from the 19 October +index (discussion comments 19030045, 19030047, 19030049, and 19030053) come +first and are dropped: the `(w, q, v_N)` consumer, the fresh T385 wrapper, +the L546 six-tape bill, and the single-ADD retiming class are already +delivered by this account or closed on main. No newer finite handoff index +replaced that list. The priority table is the revision-8 "Next bounded +decisions" table in `docs/research/current-priorities.md`. A row stays while +its stated next decision is still open. Catalogue cards not named by that +table were not reached. Dropped before the cut: work this account already +delivered, results closed on current main, and topics already on a fork +`cursor/*` branch. + +1. Complex helpers (`p104-side-correction`, `coverage-law-change`): one + uncovered helper group and causal cut with a complete caller bill. +2. BIT (`bit-helper-contract`): review the `#5679`/`#5708` chain before + another G20 search. +3. New decoders and interfaces: one complete changed producer/consumer + contract with an optimistic full signed bill. +4. **This package.** Supplier audit of merged `#5718` against the `#5719` + certificate and the `#5717` candidate hash. +5. All-size audit (`uniform-transfer-audit`): one selected assumption at its + actual caller. +6. Verification tooling (`replay-runtime`). + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 scripts/research_package.py --package research/p104-5718-causal-coverage-gap --check-only +python3 -B research/p104-5718-causal-coverage-gap/verify.py +python3.12 scripts/research_package.py --package research/p104-5718-causal-coverage-gap +``` + +`verify.py` prints + +```text +PASS_P104_5718_CAUSAL_COVERAGE_GAP absent_anchors=4 displacements=91,91,89,90,92 observer_read=911 owned_shift=1 direct_715_move=15072 checker_binding_refusal=true no_new_kappa=true +``` + +The checker hashes the five live inputs before reading them. It reruns the +published `#5719` program on `W0` and on a temporary copy of `W1`. The +injection control replaces one event of `W0` in memory: a destination-only +field-715 `ADD` stays allowed, and `ADD 206,715,2` at index 900 is the only +reported observer. A one-frame change to the shifted role-748 birth is +rejected by the lifetime comparison. + +Not run: the `#5718` scientific replay, the `#5717` adapter, the `#5599` +caller replay, Lean, and Docker. + +## Open next questions + +1. Does a rebased ledger, using the direct field-715 move from frame 3 to + frame 396 and classifying the extra field-340 write at index 11260, hold + on `W1`? The old certificate cannot be that ledger. First write a new + subject from the anchors recorded here and scan `W1` alone. Nothing here + prices that scan or the `#5718` caller. +2. Does the published `#5717` adapter accept `W1` under an explicit `+1` + label map? The frame sequences match that shift, and the packaged + candidate hash does not. First point the adapter at `W1` and record the + map it uses. Its entry point currently authenticates a different word. + +## Credit + +The fixed subject and checker are from Chris R / Clear1nsight, +`research/p104-temporal-fixed-independent-audit`, following Ali Romman's +PR5713 and Joel Pulikkan / GamingPuzzled's PR5684 word. The successor word is +from flyingviper, `research/p104-two-boundary-helper-split`. The third +candidate hash is from `research/p104-caller-owned-interface`. No file from +those packages is modified. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/p104-5718-causal-coverage-gap/SOURCES.json b/research/p104-5718-causal-coverage-gap/SOURCES.json new file mode 100644 index 0000000000..4e6f93cadc --- /dev/null +++ b/research/p104-5718-causal-coverage-gap/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-caller-owned-interface/source/BINDING.json", + "usage": "input", + "git_blob": "d7152c152617961ef24d4b3301e85a620b21994f", + "sha256": "aff998b6d3069cea1a0a10b2a2fcd3b8100d3c84e521ef54b679a5c996839a99" + }, + { + "path": "research/p104-caller-owned-interface/source/WORD.json.gz", + "usage": "input", + "git_blob": "45f6c10bf8a0ad6eb5f6714377a464e274db7dbd", + "sha256": "9fd67dd89ed24a644257cd9aef06934ed4c6fbe0441804684a968868f2ef66a8" + }, + { + "path": "research/p104-temporal-fixed-independent-audit/inputs/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/p104-temporal-fixed-independent-audit/inputs/NOTICE", + "usage": "input", + "git_blob": "fa0bd1401f5775f4351cfa23b08f3998dba6129e", + "sha256": "e8e0cabef6cf40d63f3cea3b6403dfd1af8727e40df03f09b2932718bcddc1b0" + }, + { + "path": "research/p104-temporal-fixed-independent-audit/inputs/WORD.json.gz", + "usage": "input", + "git_blob": "f3fb0e2144ec8a5c3407e4eaa6528bb3436ba573", + "sha256": "d6db1d0d97b13ea483a462c65437664d15d34dec56c3682cf6e1de31266ec6c2" + }, + { + "path": "research/p104-temporal-fixed-independent-audit/verify.py", + "usage": "input", + "git_blob": "a2111649f30f57f7acda419c678e950755e85258", + "sha256": "bce6cdf82cb1492d209c241670df894548a485b89622a39851f26352f61e999b" + }, + { + "path": "research/p104-two-boundary-helper-split/WORD.json.gz", + "usage": "input", + "git_blob": "4db015aca34ea957dd8b3b4d7ae4fa12b89934f8", + "sha256": "cff7196f8b168c4ebf8227185eed98387b66ec5db0179108adfea4045775cc31" + } + ] +} diff --git a/research/p104-5718-causal-coverage-gap/TASK.json b/research/p104-5718-causal-coverage-gap/TASK.json new file mode 100644 index 0000000000..ab173a97b5 --- /dev/null +++ b/research/p104-5718-causal-coverage-gap/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Does the fixed #5719 causal/typed-contact certificate, or the #5717 owned-label names, cover merged #5718?", + "scope_change_reason": "The card's first experiment asks for one latest uncovered candidate and one resolved coverage gap. This package answers that for merged #5718 against the #5719 certificate and the #5717 frozen candidate hash. It does not audit BIT #5679/#5708, rerun #5599 admission, or transfer those checks onto a later kappa proposal.", + "bottleneck_link": "A higher conditional P104 exponent can be selected only after the successor's own caller, causal, and owned-lifetime premises are covered. Showing that the #5719 certificate does not apply to #5718 blocks that particular reuse; it does not itself raise kappa.", + "budget_minutes": 60, + "stop_rule": "Stop when one source-bound gap is machine-checked: the published #5719 checker gives no scientific verdict on the #5718 bytes, and the fixed anchors, 715 chart path, provenance window, and role-747 lifetime do not hold on that word. Do not launch the #5718 or #5599 scientific replays.", + "outcome": "completed", + "evidence": "verify.py prints PASS_P104_5718_CAUSAL_COVERAGE_GAP. The predecessor checker accepts the pinned #5684 word and returns BINDING_UNRESOLVED, scientific_falsifier false, on the #5718 bytes. Independent census records four absent anchors, displacements 91,91,89,90,92, one forbidden 715 source read at index 911, and a uniform +1 owned-lifetime frame shift that makes role 747 a different lifetime.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does a rebased ledger, using the direct 715 move from frame 3 to frame 396 and classifying the extra field-340 write at index 11260, hold on the #5718 word?", + "why_it_matters": "The missing 3-to-598-to-396 path and the extra provenance write are the premises a transferred certificate would have to replace. A rebased pass would be new coverage; this package only shows the old certificate does not apply.", + "first_step": "Write a new fixed subject for the #5718 anchors observed here and scan that word alone, without reusing the #5719 index literals.", + "blocked_by": "No published subject pins those replacement events. The #5718 author replay is a different checker and was not rerun." + }, + { + "question": "Does the published #5717 owned-lifetime adapter accept the #5718 word under an explicit +1 label map?", + "why_it_matters": "The #5718 pull request says that adapter passed. Its published entry point is bound to a third word hash, so the claim is not the certificate executed here.", + "first_step": "Point the #5717 adapter at research/p104-two-boundary-helper-split/WORD.json.gz and record the label map it uses.", + "blocked_by": "The adapter authenticates source/WORD.json.gz inside its own package. Rebinding it is a separate source change, not a corollary of the frame-sequence shift." + } + ] +} diff --git a/research/p104-5718-causal-coverage-gap/VERIFY.json b/research/p104-5718-causal-coverage-gap/VERIFY.json new file mode 100644 index 0000000000..80bb558e7e --- /dev/null +++ b/research/p104-5718-causal-coverage-gap/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-caller-owned-interface/source/BINDING.json", + "research/p104-caller-owned-interface/source/WORD.json.gz", + "research/p104-temporal-fixed-independent-audit/inputs/LICENSE", + "research/p104-temporal-fixed-independent-audit/inputs/NOTICE", + "research/p104-temporal-fixed-independent-audit/inputs/WORD.json.gz", + "research/p104-temporal-fixed-independent-audit/verify.py", + "research/p104-two-boundary-helper-split/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Hash-pins both words and the published checkers, requires the #5719 checker to accept only its own word, and checks the anchor, provenance, chart-path, and owned-label delta plus injection controls." + } + ] +} diff --git a/research/p104-5718-causal-coverage-gap/verify.py b/research/p104-5718-causal-coverage-gap/verify.py new file mode 100644 index 0000000000..de08690a3c --- /dev/null +++ b/research/p104-5718-causal-coverage-gap/verify.py @@ -0,0 +1,315 @@ +#!/usr/bin/env python3 +"""Show that the fixed #5719 causal certificate does not cover merged #5718. + +The published checker is executed only as a custody control. The census below +is a separate reading of the two authenticated words. No new kappa is claimed. +""" + +import gzip +import hashlib +import json +import subprocess +import sys +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +OLD_WORD = ROOT / "research/p104-temporal-fixed-independent-audit/inputs/WORD.json.gz" +OLD_CHECKER = ROOT / "research/p104-temporal-fixed-independent-audit/verify.py" +NEW_WORD = ROOT / "research/p104-two-boundary-helper-split/WORD.json.gz" +OWNED_WORD = ROOT / "research/p104-caller-owned-interface/source/WORD.json.gz" +OWNED_BINDING = ROOT / "research/p104-caller-owned-interface/source/BINDING.json" + +PINS = { + OLD_WORD: "d6db1d0d97b13ea483a462c65437664d15d34dec56c3682cf6e1de31266ec6c2", + OLD_CHECKER: "bce6cdf82cb1492d209c241670df894548a485b89622a39851f26352f61e999b", + NEW_WORD: "cff7196f8b168c4ebf8227185eed98387b66ec5db0179108adfea4045775cc31", + OWNED_WORD: "9fd67dd89ed24a644257cd9aef06934ed4c6fbe0441804684a968868f2ef66a8", + OWNED_BINDING: "aff998b6d3069cea1a0a10b2a2fcd3b8100d3c84e521ef54b679a5c996839a99", +} + +# Index literals of the #5719 subject. These are the certificate's coordinates, +# not a claim that the same numbers name the same events on a later word. +INTERVAL = (823, 14983) +PROVENANCE = (11202, 14983) +STABILITY = (14654, 14983) +ANCHORS = { + 823: ["ADD", 207, 720, "-2", 3], + 11202: ["ADD", 340, 337, "1", 396], + 13572: ["ADD", 712, 747, "1", 598], + 13577: ["MOVE", 715, 3, 598, False], + 13578: ["ADD", 715, 747, "1", 598], + 13737: ["ADD", 525, 712, "-4", 598], + 14654: ["ADD", 525, 340, "1", 396], + 14982: ["MOVE", 715, 598, 396, False], + 14983: ["ADD", 340, 715, "-4", 396], +} +ABSENT_ON_SUCCESSOR = (13572, 13577, 13578, 14982) +SCALAR = {"ADD", "COPY", "SCALE", "INIT", "CLEAR"} + + +def fail(message): + raise SystemExit("FAIL_P104_5718_CAUSAL_COVERAGE_GAP " + message) + + +def sha256(raw): + return hashlib.sha256(raw).hexdigest() + + +def pinned(path): + raw = path.read_bytes() + digest = sha256(raw) + if digest != PINS[path]: + fail(path.name + " sha256 " + digest) + return raw + + +def load_word(path): + word = json.loads(gzip.decompress(pinned(path))) + if not isinstance(word, dict) or not isinstance(word.get("program"), list): + fail(path.name + " has no program") + if not isinstance(word.get("frames"), list) or len(word["frames"]) <= 598: + fail(path.name + " frame inventory does not contain 598") + return word + + +def span_mask(basis): + values = [0] + for vector in basis: + if not isinstance(vector, int) or vector <= 0: + fail("frame basis vector is not a positive integer") + # Materialize before extending. A live generator would walk the new items. + values.extend([item ^ vector for item in values]) + mask = 0 + for item in values: + mask |= 1 << item + return mask + + +def strict_subspace(frames, left, right): + return (len(frames[left]) < len(frames[right]) + and span_mask(frames[left]) & span_mask(frames[right]) == span_mask(frames[left])) + + +def locations(program, event): + return [index for index, item in enumerate(program) if item == event] + + +def scalar_writes(program, role, lo, hi): + return [index for index, event in enumerate(program) + if lo <= index < hi and event[0] in SCALAR and event[1] == role] + + +def forbidden_715(program, lo, hi): + """Field-715 touches in [lo, hi) other than MOVE or a destination-only ADD.""" + found = [] + for index, event in enumerate(program): + if not (lo <= index < hi): + continue + op = event[0] + if op == "MOVE": + continue + if op == "ADD" and event[1] == 715 and event[2] != 715: + continue + if op in ("ADD", "COPY") and (event[1] == 715 or event[2] == 715): + found.append((index, event)) + elif op in ("SCALE", "INIT", "CLEAR") and event[1] == 715: + found.append((index, event)) + return found + + +def lifetime(program, role): + return [(event[0], event[2]) for event in program + if event[0] in ("INIT", "CLEAR") and event[1] == role] + + +def moves_of(program, role): + return [(index, event) for index, event in enumerate(program) + if event[0] == "MOVE" and event[1] == role] + + +def run_predecessor(word_path): + completed = subprocess.run( + [sys.executable, "-B", str(OLD_CHECKER), str(word_path)], + cwd=ROOT, capture_output=True, text=True, timeout=60, check=False) + try: + payload = json.loads(completed.stdout) + except json.JSONDecodeError: + fail("predecessor checker did not return JSON; exit " + str(completed.returncode)) + receipt = payload.get("receipt") + if not isinstance(receipt, dict): + fail("predecessor checker returned no receipt") + return completed.returncode, receipt + + +def require_old_certificate(old): + program = old["program"] + if old["schema"] != "p104-r22-reframe/1" or old["public"] != 743: + fail("pinned #5684 word lost its schema or public count") + if [len(old["frames"][frame]) for frame in (3, 598, 396)] != [0, 1, 3]: + fail("pinned #5684 frame dimensions changed") + if not (strict_subspace(old["frames"], 3, 598) and strict_subspace(old["frames"], 598, 396)): + fail("pinned #5684 frame chain is not strict") + for index, event in ANCHORS.items(): + if locations(program, event) != [index]: + fail("pinned #5684 anchor " + str(index) + " is not unique at that index") + if scalar_writes(program, 712, *INTERVAL) != [13572]: + fail("pinned #5684 field-712 interval census changed") + if scalar_writes(program, 525, *INTERVAL) != [13737, 14654]: + fail("pinned #5684 field-525 interval census changed") + if scalar_writes(program, 340, *PROVENANCE) != [11202]: + fail("pinned #5684 field-340 provenance census changed") + if scalar_writes(program, 340, *STABILITY) != []: + fail("pinned #5684 field-340 stability interval is not empty") + if forbidden_715(program, *INTERVAL) != []: + fail("pinned #5684 interval already has a forbidden field-715 touch") + if moves_of(program, 715) != [ + (13577, ANCHORS[13577]), (14982, ANCHORS[14982]), (14988, ["MOVE", 715, 396, 127, False]) + ]: + fail("pinned #5684 field-715 moves changed") + + +def injection_controls(program): + allowed = [list(event) for event in program] + allowed[900] = ["ADD", 715, 525, "1/4", 3] + if forbidden_715(program, *INTERVAL) != [] or forbidden_715(allowed, *INTERVAL) != []: + fail("destination-only field-715 ADD was treated as an observer") + observed = [list(event) for event in program] + observed[900] = ["ADD", 206, 715, "2", 3] + if forbidden_715(observed, *INTERVAL) != [(900, ["ADD", 206, 715, "2", 3])]: + fail("injected field-715 source read was not detected") + + +def require_successor_gap(old, new): + program = new["program"] + if new["schema"] != "p104-terminal-main-split-short-cleanup/1" or new["public"] != 744: + fail("successor schema/public count is not the merged #5718 word") + if len(new["initial"]) != 744 or len(new["final"]) != 744 or len(program) != 25546: + fail("successor endpoint or program length changed") + if [len(new["frames"][frame]) for frame in (3, 598, 396)] != [0, 1, 3]: + fail("successor lost the 0/1/3 frame dimensions") + if not (strict_subspace(new["frames"], 3, 598) and strict_subspace(new["frames"], 598, 396)): + fail("successor lost the strict frame chain; that part of the certificate does transfer") + + displacements = [] + for index in sorted(ANCHORS): + found = locations(program, ANCHORS[index]) + if index in ABSENT_ON_SUCCESSOR: + if found: + fail("anchor " + str(index) + " is present on the successor") + continue + if len(found) != 1: + fail("surviving anchor " + str(index) + " is not unique") + displacements.append(found[0] - index) + if displacements != [91, 91, 89, 90, 92]: + fail("surviving-anchor displacements changed: " + str(displacements)) + if len(set(displacements)) == 1: + fail("a single index translation would cover the surviving anchors") + + if scalar_writes(program, 712, *INTERVAL) != [13663]: + fail("successor field-712 interval write is not the shifted role") + if program[13663] != ["ADD", 712, 748, "1", 598]: + fail("successor field-712 write is not source 748") + if scalar_writes(program, 340, *PROVENANCE) != [11260, 11293]: + fail("successor provenance window is not the two observed writes") + if program[11260] != ["ADD", 340, 344, "1", 70]: + fail("extra field-340 write at 11260 changed") + if program[11293] != ANCHORS[11202]: + fail("credited field-340 provenance ADD is not at 11293") + # The numeric stability interval is empty on both words. On the successor + # its endpoints are different operations, and the old read now sits inside it. + if scalar_writes(program, 340, *STABILITY) != []: + fail("numeric stability interval unexpectedly contains a field-340 write") + if program[14654] == old["program"][14654] or program[14983] == old["program"][14983]: + fail("numeric stability endpoints still denote the old events") + if not (STABILITY[0] < 14744 < STABILITY[1]) or not (15075 >= STABILITY[1]): + fail("the old read/cut no longer witnesses that the numeric interval moved") + + observed = forbidden_715(program, *INTERVAL) + if observed != [(911, ["ADD", 206, 715, "2", 3])]: + fail("field-715 observer failure is not the single read at 911") + successor_moves = moves_of(program, 715) + if successor_moves != [ + (15072, ["MOVE", 715, 3, 396, False]), + (15080, ["MOVE", 715, 396, 127, False]), + ]: + fail("field-715 chart path is not the direct 3-to-396 move") + if any(event[2] == 598 for _, event in successor_moves): + fail("a field-715 move through frame 598 is present") + + if lifetime(program, 743) != []: + fail("successor role 743 is an owned lifetime") + for role in range(743, 752): + if lifetime(old["program"], role) != lifetime(program, role + 1): + fail("owned frame sequence does not shift by one at role " + str(role)) + if lifetime(old["program"], 747) == lifetime(program, 747): + fail("role 747 names the same lifetime on both words") + mutated = [list(event) for event in program] + for event in mutated: + if event[0] == "INIT" and event[1] == 748: + event[2] += 1 + break + else: + fail("successor has no role-748 birth to mutate") + if all(lifetime(old["program"], role) == lifetime(mutated, role + 1) + for role in range(743, 752)): + fail("owned-sequence comparison ignores the birth frame") + + +def require_distinct_owned_candidate(): + binding = json.loads(pinned(OWNED_BINDING)) + if binding.get("word_bytes_sha256") != PINS[OWNED_WORD]: + fail("published #5717 binding does not name its packaged word") + if PINS[OWNED_WORD] in (PINS[OLD_WORD], PINS[NEW_WORD]): + fail("the #5717 candidate word is not a third artifact") + + +def require_checker_custody(old_receipt, successor_code, successor_receipt): + if old_receipt.get("status") != "PASS_FIXED_CAUSAL_LEDGER_AND_TYPED_CONTACTS_ONLY": + fail("predecessor checker did not accept its pinned word") + if old_receipt.get("new_kappa") is not None: + fail("predecessor checker reported a new kappa") + census = old_receipt.get("write_census") + if census != {"712": [13572], "525": [13737, 14654], "340": [11202]}: + fail("predecessor write census disagrees with the independent reading") + if successor_code == 0 or successor_receipt.get("status") == old_receipt["status"]: + fail("predecessor checker accepted the successor bytes") + if successor_receipt.get("status") != "BINDING_UNRESOLVED": + fail("successor refusal was not a binding failure: " + str(successor_receipt.get("status"))) + if successor_receipt.get("scientific_falsifier") is not False: + fail("binding refusal was labeled as a scientific falsifier") + if successor_receipt.get("coverage_complete") is not False: + fail("binding refusal claimed complete coverage") + + +def main(): + pinned(OLD_CHECKER) + old = load_word(OLD_WORD) + new = load_word(NEW_WORD) + require_old_certificate(old) + injection_controls(old["program"]) + require_successor_gap(old, new) + require_distinct_owned_candidate() + old_code, old_receipt = run_predecessor(OLD_WORD) + if old_code != 0: + fail("predecessor checker exit " + str(old_code) + " on its pinned word") + with tempfile.TemporaryDirectory() as directory: + successor_copy = Path(directory) / "WORD.json.gz" + successor_copy.write_bytes(NEW_WORD.read_bytes()) + successor_code, successor_receipt = run_predecessor(successor_copy) + require_checker_custody(old_receipt, successor_code, successor_receipt) + print( + "PASS_P104_5718_CAUSAL_COVERAGE_GAP" + " absent_anchors=4" + " displacements=91,91,89,90,92" + " observer_read=911" + " owned_shift=1" + " direct_715_move=15072" + " checker_binding_refusal=true" + " no_new_kappa=true" + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main())