From bb36fc65ee0b161229169505f4840c436c5ca2b9 Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 14:22:27 +1100 Subject: [PATCH 1/3] Reuse #7147 selected replay navigation for onboarding This is the exact documentation prerequisite retained by #7156. It points the onboarding check to the selected #7000/#7001 review. Credit to Rohan Arun and the source authors. --- docs/ci-verification.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). From d2e54af81f9dda6487636b79d4964a2385d89b2b Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 21:53:51 +1100 Subject: [PATCH 2/3] Replay the historical selected check at its inspected commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The PR #6292 rejection census and package plan are statements about 2485805. Load its exact sources and planner in a private sparse checkout, keeping all source hashes, 19 expected rejections, nine package selections and the empty-plan control. Subsequent edits to the live Makefile and CI guide no longer invalidate this historical check. The original audit is by unpaidmoon, building on Dennis’s historical replay gate. The pinned repository view follows the precedent of Matarener’s PR #5434. Repair prepared with substantial OpenAI Codex assistance. --- .../historical-selected-replay-gap/README.md | 6 +- .../SOURCES.json | 60 +++++++++--------- .../VERIFY.json | 31 +-------- .../historical-selected-replay-gap/verify.py | 63 ++++++++++++++----- 4 files changed, 82 insertions(+), 78 deletions(-) diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9") From 1aecc7cb3151826ce8fb5d3708579a8a92f08c16 Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Thu, 12 Nov 2026 16:55:29 +1100 Subject: [PATCH 3/3] Price restoration of the fixed connector port Give the two-row clean-form lower bound and verify 67 unit operations with one owned zero row. Reprice the pinned width-16 fixture at 35060 versus 40754 and retain the distinction from retargeting. Builds on #7324, #2063, #1954 and #5372. Prepared with substantial OpenAI Codex and ChatGPT Pro assistance. --- research/fixed-port-connector-reset/README.md | 164 +++++++++++ .../fixed-port-connector-reset/RESULT.json | 201 +++++++++++++ .../fixed-port-connector-reset/SOURCES.json | 36 +++ research/fixed-port-connector-reset/TASK.json | 62 ++++ .../fixed-port-connector-reset/VERIFY.json | 23 ++ research/fixed-port-connector-reset/verify.py | 274 ++++++++++++++++++ 6 files changed, 760 insertions(+) create mode 100644 research/fixed-port-connector-reset/README.md create mode 100644 research/fixed-port-connector-reset/RESULT.json create mode 100644 research/fixed-port-connector-reset/SOURCES.json create mode 100644 research/fixed-port-connector-reset/TASK.json create mode 100644 research/fixed-port-connector-reset/VERIFY.json create mode 100644 research/fixed-port-connector-reset/verify.py diff --git a/research/fixed-port-connector-reset/README.md b/research/fixed-port-connector-reset/README.md new file mode 100644 index 0000000000..a7d5ecf7a9 --- /dev/null +++ b/research/fixed-port-connector-reset/README.md @@ -0,0 +1,164 @@ +# Return the original port in a five-source connector reset + +**Exact local result; no new κ.** At unit operation prices the restored +fixed-port connector costs **67 operations** with one owned zero row +before charging for that row. The unchanged restored connector costs +**74**. With a fixed additional provision price ρ ≥ 0 the exact +five-source comparison is **min(74, 67 + ρ)**: provision must cost +strictly less than seven units for a saving. On the retained width-16 +fixture, the complete declared fixed-port bill is **35,060** versus +**40,754** for the original restored connector, a saving of **5,694 +tariff units**. The existing retargeted solution costs 34,944 where +moving the child ports is legal. + +## Contract + +Over F₂ let z be the original arbitrary dirty connector and w one owned +width-L row supplied zero and returned zero. All n sources xⱼ are +immutable; every nonempty mask m has a distinct arbitrary dirty target +yₘ. Return z unchanged and add Aₘ(∑ⱼ∈ₘ Bⱼ xⱼ) to yₘ. The complete +child calls Bⱼ: z += Bⱼ xⱼ and Aₘ: yₘ += Aₘ z always use physical z, +restore their private scratch and heads, and leave other public rows +untouched. The targets are never read or observed during the word. The +maps are arbitrary linear maps, including singular and noncommuting +maps; the word must work for all of them. + +The only extra data operations are F: w += z, G: z += w, and at most +one Z: z := 0. Their positive complete prices are f, g and r. The +uniform prices for a source call and readout are b and a. Row provision +is separate. Without the auxiliary there is no legal reset that preserves +an arbitrary z, so the original #2063 comparator applies. The model +does not bundle operations, use outputs as storage or retarget a child. + +## Exact price of saving and restoring the port + +Let N = 2ⁿ − 1. Save the old z in w, clear z, and traverse the reflected +Gray path from 0 through all N nonzero masks. Toggle the entering source +and read the corresponding output once at each vertex. To leave z at +zero, either close the path with its single final source toggle or +reset z. Then use G and F to return z to its old value and w to zero. + +| Word | Save and clear | End of walk | B | A | F | G | Z | +| --- | --- | --- | ---: | ---: | ---: | ---: | ---: | +| Closed | F, G | One source toggle | N+1 | N | 2 | 2 | 0 | +| Entry reset | F, Z | One source toggle | N+1 | N | 2 | 1 | 1 | +| Exit reset | F, G | Z | N | N | 2 | 2 | 1 | + +All three include the final G, F. Each readout uses z at its intended +mask and never has to cancel a contribution from old z. No map is +commuted, inverted or moved to w. + +**Lower bound, including interleaved moves and repeated readouts.** +Specialize to scalar identity maps with independent source bits and an +independent original connector bit. Let α = (α_z, α_w) be the +coefficients of that original bit in the two rows. The pair cannot +become 00: the source bits are independent and no output can be read +back. The clean combination s = α_w z + α_z w starts and ends at 0. +Both F and G preserve s while changing coordinates. A B call can +toggle one source bit in s or do nothing. A legal Z can only send s to +0: it requires α_w = 1 and then puts α_z = 0 and z = 0. + +If k ≥ 1 targets each receive exactly one readout, those readouts need +α = 01 and k distinct nonzero masks in s. At least k B calls are needed +to create them, and the other targets need at least two readouts each, +so A ≥ 2N − k. If there are exactly k B calls, each must produce one +of those distinct nonzero masks for the first time; the single reset +must occur after the last one to return s to zero. With no B left, +all k once-read targets must already have been read before that reset. + +The coefficient path must go from 10 through 01 and back to 10. Entering +01 takes F and then either G or Z; returning takes G and F. Thus a word +without a reset needs at least k+1 B and two F, two G. A word with a +reset and at least k+1 B needs at least two F and one G. A word with a +reset and exactly k B still needs two F and two G because its reset is +used for closure, after the path has already entered 01. This yields + +```text +price >= b k + a (2N - k) + 2f + g + min(b+g, b+r, g+r). +``` + +For a ≥ b this bound is minimized at k=N, and the three Gray words +attain its minimum. This proves the exact price among all legal words +using at least one once-read target, without assuming a single clean +excursion. A word without any once-read target needs at least 2N A and +n B because every source must influence its own one-source mask. For +five sources at unit prices this lower bound is also 67, so the +wrapped optimum is global in that tariff. Paying ρ for any word using +w then gives the exact optional-provision comparison above. At general +prices the no-singleton bound need not settle the global optimum. + +## Pinned width-16 comparison + +The retained #1954 fixture uses five source permutations and 31 +permuted 13-tap readout maps. All 36 maps fix the all-ones vector. +Restricting every row to that one-dimensional subspace gives exactly +the identity test above, even for a word chosen specifically for these +maps. The lower bound does not transfer to every fixed map instance. +For example, two complementary projections used as the two source +maps and as the first two readouts (with identity for the combined +mask) let three outputs share one clean value. A ten-operation +fixed-port word there beats the generic eleven-operation once-read +bound at two sources. The replay checks all 4,096 inputs to this example. + +Keep #5372's charge of 26,704 for the shared tables and original rows, +403 for mask descriptors, and 58 for allocation, 16 storage cells and +16 initial zero writes. The complete source and readout prices are 29 +and 221. Charge each extra full-row XOR or reset 16 operations or +writes plus the same 13-unit action descriptor. The entry-reset word +costs 7,895 in actions (32×29 + 31×221 + 4×29). No word without a +once-read target can beat the action bill, since 62×221 + 5×29 is +13,847. Adding all retained fixed charges gives 35,060. This exact +total comparison stipulates those charges as fixed for the auxiliary +route. It does not optimize other layout or compilation tariffs. + +The original restored comparator is 40,754 by repricing all 16 of +#2063's exact profiles and retaining the original common charges. +Retargeting the children instead would avoid the four port actions +and cost 34,944, as in #5372. The wrapper costs 116 more and is useful +only when those ports must stay fixed. + +## Verification + +Run with CPython 3.12 from a clean checkout or the official Git-free +export (which includes the three declared inputs): + +```sh +python3.12 -I -B research/fixed-port-connector-reset/verify.py +``` + +[RESULT.json](RESULT.json) records 24 symbolic Gray words, 12 exact +shortest-word checks for one or two sources, the fixed-map counterexample, +and each of the three literal words on all 608 width-16 input basis +columns. The latter use the pinned fixture maps and a separate +dense-matrix target oracle. Seven controls reject lost dirty values, +incorrect closure or return, unpaid zero initialization, or a second +reset. The three comparison inputs are checked against the hashes in +[SOURCES.json](SOURCES.json). + +## Open next questions + +A multiplication caller still has to supply the fixed ports, an owned +zero row outside the child scratch, complete prices for its moves, +reset or closing call, and the full layout, tape, stock and recursive +bill. The width-16 tariff is a checked local instance. No physical +supplier, selected caller or changed κ follows. A useful next step is +to pin one actual caller and account for that row for the entire +interval before attempting a larger construction. + +## Credit + +Nick Petalas's [#7324](https://github.com/CrocSwap/integer-mult-bounds/pull/7324) +at `fd573cfe4e9714706b01f0534584e6f5032dc858` supplies the disposable +reset and open Gray schedule. Ross Richardson's +[#934](https://github.com/CrocSwap/integer-mult-bounds/pull/934) lineage +supplies the generic dirty connector, Adam Gall's +[#2063](https://github.com/CrocSwap/integer-mult-bounds/pull/2063) its exact +restored tariff, Cinna Davis's +[#1954](https://github.com/CrocSwap/integer-mult-bounds/pull/1954) the +fixture, and Ali Romman's +[#5372](https://github.com/CrocSwap/integer-mult-bounds/pull/5372) the +paid clean-row Gray cycle and retained invoice. +[#2182](https://github.com/CrocSwap/integer-mult-bounds/pull/2182) is a +separate fixed-port precedent with a second arbitrary dirty row and +paired readouts. OpenAI Codex and ChatGPT Pro materially assisted the +proof, adversarial review and exact replay. Apache-2.0. diff --git a/research/fixed-port-connector-reset/RESULT.json b/research/fixed-port-connector-reset/RESULT.json new file mode 100644 index 0000000000..3f0b72f6f6 --- /dev/null +++ b/research/fixed-port-connector-reset/RESULT.json @@ -0,0 +1,201 @@ +{ + "fixed_singular_counterexample_inputs": 4096, + "fixture": { + "all_witness_counts": { + "closed": { + "A": 31, + "B": 32, + "F": 2, + "G": 2, + "Z": 0 + }, + "entry_reset": { + "A": 31, + "B": 32, + "F": 2, + "G": 1, + "Z": 1 + }, + "exit_reset": { + "A": 31, + "B": 31, + "F": 2, + "G": 2, + "Z": 1 + } + }, + "basis_columns_per_word": 608, + "call_bill": 7895, + "charged_entry_reset_invoice": { + "action_descriptors": 871, + "allocation_release_descriptors": 26, + "fresh_row_cells": 16, + "mask_control_descriptors": 403, + "output_updates": 6448, + "shared_map_table_bits": 26112, + "shared_row_cells": 592, + "source_updates": 512, + "wrapper_reset_writes": 16, + "wrapper_row_xors": 48, + "zero_writes": 16 + }, + "dirty_comparator": 40754, + "fixed_map_identity_line_count": 36, + "mutations_rejected": 7, + "premium_vs_retargeting": 116, + "retargeted_comparator": 34944, + "saving_vs_dirty": 5694, + "total": 35060 + }, + "scope": "exact declared fixed-port connector model; no new kappa", + "small_exact_costs": [ + { + "minimum": 29, + "n": 1, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 20 + ], + "required_singleton": 1 + }, + { + "minimum": 23, + "n": 1, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 27, + "n": 1, + "prices_B_A_F_G_Z": [ + 7, + 9, + 2, + 3, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 7, + "n": 1, + "prices_B_A_F_G_Z": [ + 1, + 1, + 1, + 1, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 43, + "n": 2, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 20 + ], + "required_singleton": 1 + }, + { + "minimum": 37, + "n": 2, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 59, + "n": 2, + "prices_B_A_F_G_Z": [ + 7, + 9, + 2, + 3, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 11, + "n": 2, + "prices_B_A_F_G_Z": [ + 1, + 1, + 1, + 1, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 43, + "n": 2, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 20 + ], + "required_singleton": 3 + }, + { + "minimum": 37, + "n": 2, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 1 + ], + "required_singleton": 3 + }, + { + "minimum": 59, + "n": 2, + "prices_B_A_F_G_Z": [ + 7, + 9, + 2, + 3, + 1 + ], + "required_singleton": 3 + }, + { + "minimum": 11, + "n": 2, + "prices_B_A_F_G_Z": [ + 1, + 1, + 1, + 1, + 1 + ], + "required_singleton": 3 + } + ], + "symbolic_witnesses": 24, + "unit_original": 74, + "unit_provision_break_even": 7, + "unit_with_owned_zero": 67 +} diff --git a/research/fixed-port-connector-reset/SOURCES.json b/research/fixed-port-connector-reset/SOURCES.json new file mode 100644 index 0000000000..555e893ad1 --- /dev/null +++ b/research/fixed-port-connector-reset/SOURCES.json @@ -0,0 +1,36 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + }, + { + "git_blob": "bc1a3a0982948426f7611a63630e9fcfd03e0906", + "path": "research/clean-connector-per-mask-seede54e/verify.py", + "sha256": "8685db5771326f22fd4136879a2852b7505a9d483a474a8d62ea33869bd80617", + "usage": "input" + }, + { + "git_blob": "ed0379b63721d9ea790a79af9677005111614765", + "path": "research/connector-all-tariff-optimum/RESULT.json", + "sha256": "15b015913dda14b7516bb4aeee798ab9a4593d5bbd59d4813ec8911e89b6c83a", + "usage": "input" + }, + { + "git_blob": "d06dacdedf95ac55f6317344e5ecdfb2048816d8", + "path": "research/clean-connector-gray-optimum/RESULT.json", + "sha256": "7f21f666bdeb56a8cb90c69f6feceac35cfdf8579714ba0bd76d464c5cc655d9", + "usage": "input" + } + ], + "schema_version": 1 +} diff --git a/research/fixed-port-connector-reset/TASK.json b/research/fixed-port-connector-reset/TASK.json new file mode 100644 index 0000000000..35d4ed6b61 --- /dev/null +++ b/research/fixed-port-connector-reset/TASK.json @@ -0,0 +1,62 @@ +{ + "actual_scope": "All nonzero masks for a fixed-port restored F2 connector, an owned zero row returned zero, two directed row XORs, at most one reset, and positive uniform child prices. Exact five-source unit result and a pinned width-16 tariff fixture. No physical caller or kappa claim.", + "ai_assistance": "OpenAI Codex and ChatGPT Pro materially assisted formulation, adversarial proof review, and exact replay.", + "author": "Clear1nsight", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Charge preservation of the original dirty connector before importing a reset-based map schedule into any supplier.", + "budget_minutes": 60, + "evidence": "A two-row clean-form invariant gives an arbitrary-word lower bound; three exact Gray words attain it for uniform readout price at least source price. The exact unit five-source wrapped bill is 67 before provision. Full pinned fixture costs 35060, down 5694 in its declared tariff.", + "open_questions": [ + { + "blocked_by": "No selected supplier binding, full stock/routing cost, or native compiler integration is supplied here.", + "first_step": "Pin one caller and bind the row lifetime, port layout, both XORs, reset or closing toggle, and child-call prices to its compiler and tape.", + "question": "Which actual multiplication caller can supply and return the matching clean row at its existing fixed ports?", + "why_it_matters": "The local price margin cannot change kappa without a compatible physical caller and complete recursive invoice." + } + ], + "original_card": { + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "id": "connector-alphabet-change", + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ], + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ] + }, + "outcome": "completed", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Restore the original fixed physical connector using one paid clean row, two directed XOR operations and at most one reset. #7324 consumes the connector; #5372 retargets the child calls.", + "scope_status": "changed", + "stop_rule": "One restore contract; small finite shortest-word tests at n<=2; all basis columns of the retained length-16 fixture. Do not start recursive integration without a named caller and complete physical bill.", + "task_id": "connector-alphabet-change" +} diff --git a/research/fixed-port-connector-reset/VERIFY.json b/research/fixed-port-connector-reset/VERIFY.json new file mode 100644 index 0000000000..1755ac4f45 --- /dev/null +++ b/research/fixed-port-connector-reset/VERIFY.json @@ -0,0 +1,23 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Exact witnesses and small shortest words, fixed-map limit control, pinned 16-bit fixture basis and complete tariff.", + "timeout_seconds": 45 + } + ], + "inputs": [ + "research/clean-connector-per-mask-seede54e/verify.py", + "research/connector-all-tariff-optimum/RESULT.json", + "research/clean-connector-gray-optimum/RESULT.json" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/fixed-port-connector-reset/verify.py b/research/fixed-port-connector-reset/verify.py new file mode 100644 index 0000000000..48d31663b5 --- /dev/null +++ b/research/fixed-port-connector-reset/verify.py @@ -0,0 +1,274 @@ +"""Exact fixed-port restoration witnesses and source-bound controls. Apache-2.0.""" + +from argparse import ArgumentParser +from collections import Counter +from hashlib import sha256 +from heapq import heappop, heappush +from itertools import product +import json +from pathlib import Path +from runpy import run_path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FIXTURE = "research/clean-connector-per-mask-seede54e/verify.py" +BASELINE = "research/connector-all-tariff-optimum/RESULT.json" +RETARGET = "research/clean-connector-gray-optimum/RESULT.json" +KINDS = "BAFGZ" +MODES = ("closed", "entry_reset", "exit_reset") + + +def require(ok, detail): + if not ok: + raise ValueError(detail) + + +def json_at(path): + return json.loads(path.read_text(encoding="utf-8")) + + +def input_paths(): + pins = {row["path"]: row["sha256"] for row in json_at(HERE / "SOURCES.json")["files"] + if row["usage"] == "input"} + require(set(pins) == {FIXTURE, BASELINE, RETARGET}, "unexpected source closure") + for name, digest in pins.items(): + require(sha256((ROOT / name).read_bytes()).hexdigest() == digest, f"changed input: {name}") + + +def gray_word(n, mode): + require(n >= 1 and mode in MODES, "invalid wrapper") + vertices = [0] + for i in range(n): + vertices += [x | (1 << i) for x in reversed(vertices)] + word = [("F", 0), ("Z" if mode == "entry_reset" else "G", 0)] + for u, v in zip(vertices, vertices[1:]): + bit = u ^ v + require(bit.bit_count() == 1, "nonedge in Gray path") + word.extend((("B", bit.bit_length() - 1), ("A", v))) + terminal = vertices[-1] + require(terminal.bit_count() == 1, "closed Gray path needs one closing toggle") + word.append(("Z", 0) if mode == "exit_reset" else ("B", terminal.bit_length() - 1)) + return word + [("G", 0), ("F", 0)] + + +def execute(word, sources, old_z, outputs, backing_w, b_map, a_map, *, zero_owned=True): + """All child calls use z, never w. Allocation clears arbitrary backing contents.""" + z, w = old_z, (0 if zero_owned else backing_w) + y = list(outputs) + resets = 0 + for op, arg in word: + if op == "B" and 0 <= arg < len(sources): + z ^= b_map(arg, sources[arg]) + elif op == "A" and 1 <= arg <= len(y): + y[arg - 1] ^= a_map(arg, z) + elif op == "F": + w ^= z + elif op == "G": + z ^= w + elif op == "Z": + resets += 1 + require(resets <= 1, "second reset") + z = 0 + else: + raise ValueError(f"unknown fixed-port operation: {(op, arg)}") + return z, w, tuple(y) + + +def counts(word): + c = Counter(op for op, _ in word) + return dict(zip(KINDS, (c[op] for op in KINDS))) + + +def best_singleton(n, prices): + b, a, f, g, r = prices + return ((1 << n) - 1) * (a + b) + 2 * f + g + min(b + g, b + r, g + r) + + +def symbolic_replay(): + total = 0 + for n in range(1, 9): + targets = tuple(range(1, 1 << n)) + source = tuple(1 << j for j in range(n)) + old = 1 << n + for mode in MODES: + word = gray_word(n, mode) + result = execute(word, source, old, (0,) * len(targets), 0, lambda j, x: x, lambda m, z: z) + expected = dict(zip(KINDS, (len(targets) + (mode != "exit_reset"), len(targets), + 2, 1 + (mode != "entry_reset"), int(mode != "closed")))) + require(result == (old, 0, targets) and counts(word) == expected, "symbolic wrapper") + require(Counter(i for op, i in word if op == "A") == Counter(targets), "literal singleton calls") + total += 1 + return total + + +def exact_small(n, singleton, prices): + """Dijkstra over exact coefficients with one distinguished once-read target. + + Other targets may be read any number of times. In the chosen target's row, + zero means unread: its only legal read produces the required nonzero mask. + """ + b, a, f, g, r = prices + masks = tuple(range(1, 1 << n)) + old = 1 << n + start = (old, 0, (0,) * len(masks), False) + dist, heap = {start: 0}, [(0, start)] + while heap: + cost, state = heappop(heap) + if cost != dist[state]: + continue + z, w, ys, reset = state + if (z, w, ys) == (old, 0, masks): + return cost + edges = [(b, (z ^ (1 << j), w, ys, reset)) for j in range(n)] + edges.extend(((f, (z, w ^ z, ys, reset)), (g, (z ^ w, w, ys, reset)))) + if not reset and w & old: + edges.append((r, (0, w, ys, True))) + for i, m in enumerate(masks): + if m != singleton or (ys[i] == 0 and z == m): + dest = ys[:i] + (ys[i] ^ z,) + ys[i + 1:] + edges.append((a, (z, w, dest, reset))) + for weight, dest in edges: + new = cost + weight + if dest not in dist or new < dist[dest]: + dist[dest] = new + heappush(heap, (new, dest)) + raise ValueError("no endpoint in finite state graph") + + +def exact_controls(): + reports = [] + # The three strict minimizers and a unit tie. Uniform source/readout + # prices make masks 1 and 3 representatives of both weights at n=2. + price_vectors = ((2, 5, 3, 7, 20), (2, 5, 3, 7, 1), (7, 9, 2, 3, 1), (1, 1, 1, 1, 1)) + for n, m in ((1, 1), (2, 1), (2, 3)): + for p in price_vectors: + found = exact_small(n, m, p) + require(found == best_singleton(n, p), "small exact optimum mismatch") + reports.append({"n": n, "required_singleton": m, "prices_B_A_F_G_Z": p, "minimum": found}) + return reports + + +def fixed_map_control(): + # On these particular singular maps the three A calls can share one + # connector value. This rebuts an unrestricted fixed-instance lower bound. + word = [("F", 0), ("G", 0), ("B", 0), ("B", 1), ("A", 1), ("A", 2), + ("A", 3), ("Z", 0), ("G", 0), ("F", 0)] + for x, y, old, a, b, c in product(range(4), repeat=6): + p, q = x & 1, y & 2 + got = execute(word, (x, y), old, (a, b, c), 0, + lambda j, v: v & (1 << j), lambda m, v: v & m) + require(got == (old, 0, (a ^ p, b ^ q, c ^ p ^ q)), "fixed singular-map control") + require(len(word) == 10 < best_singleton(2, (1,) * 5), "control must be cheaper") + return 4**6 + + +def dense(rows, value): + return sum(((r & value).bit_count() & 1) << i for i, r in enumerate(rows)) + + +def fixture_replay(): + source = run_path(str(ROOT / FIXTURE)) + length, masks = source["L"], source["MASKS"] + require(length == 16 and masks == tuple(range(1, 32)), "fixture identity") + b_map = lambda j, x: source["permute"](x, source["B_MAPS"][j]) + a_map = lambda m, z: source["apply_output_map"](z, m - 1) + ones = (1 << length) - 1 + require(all(b_map(j, ones) == ones for j in range(5)) and + all(a_map(m, ones) == ones for m in masks), "the fixture lost the common identity line") + + b_rows = [tuple(1 << col for col in p) for p in source["B_MAPS"]] + kernel = source["a_rows"]() + a_rows = {m: tuple(sum(1 << p[i] for i in range(length) if r & (1 << i)) for r in kernel) + for m, p in zip(masks, source["Q_MAPS"], strict=True)} + + def expected(xs, old, out): + images = [dense(r, x) for r, x in zip(b_rows, xs, strict=True)] + result = list(out) + for m in masks: + total = 0 + for j, v in enumerate(images): + if m & (1 << j): + total ^= v + result[m - 1] ^= dense(a_rows[m], total) + return old, 0, tuple(result) + + words = {mode: gray_word(5, mode) for mode in MODES} + rows = 5 + 1 + len(masks) + 1 + for column in range(rows * length): + inputs = [0] * rows + inputs[column // length] = 1 << (column % length) + xs, old, out, backing = inputs[:5], inputs[5], inputs[6:-1], inputs[-1] + want = expected(xs, old, out) + for word in words.values(): + got = execute(word, xs, old, out, backing, b_map, a_map) + require(got == want, f"literal fixture basis column {column}") + + old, out, backing = ones, (0,) * len(masks), ones + xs = (1, 2, 4, 8, 16) + want = expected(xs, old, out) + entry, closed = words["entry_reset"], words["closed"] + mutants = (("missing save", entry[1:], True), + ("missing entry reset", entry[:1] + entry[2:], True), + ("missing close", closed[:-3] + closed[-2:], True), + ("missing restore", entry[:-2] + entry[-1:], True), + ("dirty release", entry[:-1], True), + ("missing allocation zeroing", entry, False)) + for label, word, zero in mutants: + require(execute(word, xs, old, out, backing, b_map, a_map, zero_owned=zero) != want, label) + try: + execute([("Z", 0)] + entry, xs, old, out, backing, b_map, a_map) + except ValueError as exc: + require(str(exc) == "second reset", "wrong reset rejection") + else: + raise ValueError("second reset accepted") + + ref = json_at(ROOT / RETARGET) + retained = ref["invoice"] + n = counts(entry) + actions = sum(n.values()) + invoice = {k: retained[k] for k in ("shared_map_table_bits", "shared_row_cells", + "mask_control_descriptors", "allocation_release_descriptors", + "fresh_row_cells", "zero_writes")} + invoice.update(source_updates=n["B"] * length, output_updates=n["A"] * length * 13, + wrapper_row_xors=(n["F"] + n["G"]) * length, + wrapper_reset_writes=n["Z"] * length, action_descriptors=actions * 13) + a, b = length * 13 + 13, length + 13 + call_bill = sum(n[op] * (a if op == "A" else b) for op in KINDS) + profiles = json_at(ROOT / BASELINE)["pareto_profiles"] + require(len(profiles) == 16 and all(len(v) == 36 for v in profiles), "retained tariff frontier") + dirty = invoice["shared_map_table_bits"] + invoice["shared_row_cells"] + dirty += min(sum(v[i] * (b if i < 5 else a) for i in range(36)) for v in profiles) + price = sum(invoice.values()) + require((call_bill, price, dirty, ref["new_clean_cost"]) == (7895, 35060, 40754, 34944), + "complete fixed-port tariff comparison") + require(call_bill == best_singleton(5, (b, a, b, b, b)) < 62 * a + 5 * b, + "fixture requires a global call-price comparison") + return {"basis_columns_per_word": rows * length, "fixed_map_identity_line_count": 36, + "mutations_rejected": len(mutants) + 1, "all_witness_counts": {k: counts(v) for k, v in words.items()}, + "charged_entry_reset_invoice": invoice, "call_bill": call_bill, "total": price, + "dirty_comparator": dirty, "retargeted_comparator": ref["new_clean_cost"], + "saving_vs_dirty": dirty - price, "premium_vs_retargeting": price - ref["new_clean_cost"]} + + +def replay(): + input_paths() + unit = best_singleton(5, (1,) * 5) + require(unit == 62 + 5 == 67, "global unit cost with an owned zero row") + return {"scope": "exact declared fixed-port connector model; no new kappa", + "symbolic_witnesses": symbolic_replay(), "small_exact_costs": exact_controls(), + "fixed_singular_counterexample_inputs": fixed_map_control(), + "unit_with_owned_zero": unit, "unit_original": 74, + "unit_provision_break_even": 74 - unit, "fixture": fixture_replay()} + + +if __name__ == "__main__": + parser = ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path, help="write a new exact receipt") + args = parser.parse_args() + result = json.dumps(replay(), indent=2, sort_keys=True) + "\n" + if args.write_result: + with args.write_result.open("x", encoding="utf-8") as f: + f.write(result) + else: + require((HERE / "RESULT.json").read_text(encoding="utf-8") == result, "changed exact receipt") + print("PASS_FIXED_PORT_CONNECTOR_RESET unit=67 baseline=74 break_even=7 fixture=35060 saving=5694 no_new_kappa")