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 18b7045ee3515fa866a3f30b67cbd37bd4c361d7 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 10:32:16 -0800 Subject: [PATCH 3/3] Exclude one-chart BIT retag donors Certify exact support exclusion and complete directed price for the retained one-chart donor family. Credit #7001, #7177 and #7200. Material OpenAI Codex assistance. --- .../bit-one-chart-donor-envelope/CERT.json | 542 ++++++++++++++++++ .../LOCAL-PINS.json | 8 + research/bit-one-chart-donor-envelope/NOTICE | 7 + .../bit-one-chart-donor-envelope/PRICE.json | 48 ++ .../bit-one-chart-donor-envelope/README.md | 84 +++ .../bit-one-chart-donor-envelope/SOURCES.json | 30 + .../bit-one-chart-donor-envelope/STOCK.json | 490 ++++++++++++++++ .../bit-one-chart-donor-envelope/TASK.json | 77 +++ .../bit-one-chart-donor-envelope/VERIFY.json | 24 + .../check_stock.py | 74 +++ .../pr7200_verify.py | 224 ++++++++ .../bit-one-chart-donor-envelope/price.py | 367 ++++++++++++ .../bit-one-chart-donor-envelope/replay.py | 106 ++++ .../bit-one-chart-donor-envelope/retag.py | 67 +++ .../bit-one-chart-donor-envelope/screen.py | 185 ++++++ 15 files changed, 2333 insertions(+) create mode 100644 research/bit-one-chart-donor-envelope/CERT.json create mode 100644 research/bit-one-chart-donor-envelope/LOCAL-PINS.json create mode 100644 research/bit-one-chart-donor-envelope/NOTICE create mode 100644 research/bit-one-chart-donor-envelope/PRICE.json create mode 100644 research/bit-one-chart-donor-envelope/README.md create mode 100644 research/bit-one-chart-donor-envelope/SOURCES.json create mode 100644 research/bit-one-chart-donor-envelope/STOCK.json create mode 100644 research/bit-one-chart-donor-envelope/TASK.json create mode 100644 research/bit-one-chart-donor-envelope/VERIFY.json create mode 100644 research/bit-one-chart-donor-envelope/check_stock.py create mode 100644 research/bit-one-chart-donor-envelope/pr7200_verify.py create mode 100644 research/bit-one-chart-donor-envelope/price.py create mode 100644 research/bit-one-chart-donor-envelope/replay.py create mode 100644 research/bit-one-chart-donor-envelope/retag.py create mode 100644 research/bit-one-chart-donor-envelope/screen.py diff --git a/research/bit-one-chart-donor-envelope/CERT.json b/research/bit-one-chart-donor-envelope/CERT.json new file mode 100644 index 0000000000..b5a715a31c --- /dev/null +++ b/research/bit-one-chart-donor-envelope/CERT.json @@ -0,0 +1,542 @@ +{ + "explicit": [ + [32929,344,[0]], + [32929,345,[0]], + [32929,346,[0]], + [32929,266,[0]], + [32929,269,[0]], + [32929,271,[0]], + [32929,273,[0]], + [32929,275,[0]], + [32929,276,[0]], + [32929,506,[0]], + [32929,113,[0]], + [32929,114,[0]], + [32929,115,[0]], + [32929,116,[0]], + [32929,117,[0]], + [32929,118,[0]], + [32929,119,[0]], + [32929,120,[0]], + [32929,121,[0]], + [32929,122,[0]], + [32929,123,[0]], + [32929,124,[0]], + [32929,127,[0]], + [32929,139,[0]], + [32929,145,[0]], + [32929,146,[0]], + [32929,157,[0]], + [32929,169,[0]], + [32929,175,[0]], + [32929,176,[0]], + [32929,190,[0]], + [32929,194,[0]], + [32929,205,[0]], + [32929,211,[0]], + [32929,212,[0]], + [32929,223,[0]], + [32929,229,[0]], + [32929,230,[0]], + [32929,241,[0]], + [32929,247,[0]], + [32929,248,[0]], + [32929,259,[0]], + [32929,265,[0]], + [32929,8,[0]], + [32929,11,[0]], + [32929,12,[0]], + [32929,13,[0]], + [32929,14,[0]], + [32929,15,[0]], + [32929,48,[0]], + [32929,49,[0]], + [32929,50,[0]], + [32929,51,[0]], + [32929,52,[0]], + [32929,53,[0]], + [32929,54,[0]], + [32929,55,[0]], + [32929,56,[0]], + [32929,57,[0]], + [32929,58,[0]], + [32929,59,[0]], + [32929,60,[0]], + [32929,75,[0]], + [32929,76,[0]], + [32929,77,[0]], + [32929,78,[0]], + [32929,79,[0]], + [32929,80,[0]], + [32929,81,[0]], + [32929,82,[0]], + [32929,83,[0]], + [32929,84,[0]], + [32929,85,[0]], + [32929,86,[0]], + [32929,87,[0]], + [32929,88,[0]], + [32929,89,[0]], + [32929,90,[0]], + [32929,91,[0]], + [32929,92,[0]], + [32929,93,[0]], + [32929,94,[0]], + [32929,95,[0]], + [32929,96,[0]], + [32929,97,[0]], + [32929,98,[0]], + [32929,99,[0]], + [32929,100,[0]], + [32929,101,[0]], + [32929,102,[0]], + [32929,103,[0]], + [32929,104,[0]], + [32981,326,[0]], + [32981,329,[1]], + [32981,330,[0]], + [32981,266,[0]], + [32981,267,[1]], + [32981,272,[1]], + [32981,273,[0]], + [32981,274,[1]], + [32981,275,[0]], + [32981,507,[1]], + [32981,114,[0]], + [32981,125,[1]], + [32981,126,[1]], + [32981,127,[0]], + [32981,128,[0]], + [32981,129,[0]], + [32981,130,[0]], + [32981,131,[0]], + [32981,132,[0]], + [32981,133,[0]], + [32981,139,[0]], + [32981,140,[0]], + [32981,151,[0]], + [32981,157,[0]], + [32981,158,[0]], + [32981,163,[0]], + [32981,169,[0]], + [32981,170,[0]], + [32981,181,[0]], + [32981,185,[0]], + [32981,193,[0]], + [32981,194,[0]], + [32981,200,[0]], + [32981,206,[0]], + [32981,212,[0]], + [32981,223,[0]], + [32981,229,[0]], + [32981,230,[0]], + [32981,241,[0]], + [32981,247,[0]], + [32981,248,[0]], + [32981,254,[0]], + [32981,260,[0]], + [32981,11,[0,5]], + [32981,12,[0]], + [32981,13,[0]], + [32981,14,[0]], + [32981,15,[0]], + [32981,32,[0]], + [32981,33,[0]], + [32981,34,[0]], + [32981,35,[0]], + [32981,36,[0]], + [32981,37,[0]], + [32981,38,[0]], + [32981,39,[0]], + [32981,40,[0]], + [32981,41,[0]], + [32981,42,[0]], + [32981,43,[0]], + [32981,44,[0]], + [32981,45,[0]], + [32981,46,[0]], + [32981,47,[0]], + [32981,61,[0]], + [32981,62,[0]], + [32981,63,[0]], + [32981,64,[0]], + [32981,65,[0]], + [32981,66,[0]], + [32981,67,[0]], + [32981,68,[0]], + [32981,69,[0]], + [32981,70,[0]], + [32981,71,[0]], + [32981,72,[0]], + [32981,73,[0]], + [32981,74,[0]], + [32981,90,[0]], + [32981,91,[0]], + [32981,92,[0]], + [32981,93,[0]], + [32981,94,[0]], + [32981,95,[0]], + [32981,96,[0]], + [32981,97,[0]], + [32981,98,[0]], + [32981,99,[0]], + [32981,100,[0]], + [32981,101,[0]], + [32981,102,[0]], + [32981,103,[0]], + [32981,104,[0]], + [33032,345,[9]], + [33032,347,[3]], + [33032,349,[3]], + [33032,267,[0,3]], + [33032,269,[5]], + [33032,270,[3]], + [33032,272,[3]], + [33032,275,[6]], + [33032,277,[0,3]], + [33032,506,[0,3]], + [33032,113,[3]], + [33032,114,[3]], + [33032,115,[3]], + [33032,116,[3]], + [33032,117,[3]], + [33032,118,[3]], + [33032,119,[3]], + [33032,120,[3]], + [33032,121,[3]], + [33032,122,[3]], + [33032,123,[3]], + [33032,124,[3]], + [33032,125,[5]], + [33032,134,[3]], + [33032,145,[3]], + [33032,151,[3]], + [33032,157,[3]], + [33032,158,[3]], + [33032,163,[3]], + [33032,164,[3]], + [33032,175,[3]], + [33032,181,[3]], + [33032,185,[3]], + [33032,193,[3]], + [33032,199,[3]], + [33032,200,[3]], + [33032,211,[3]], + [33032,217,[3]], + [33032,223,[3]], + [33032,224,[3]], + [33032,235,[3]], + [33032,236,[3]], + [33032,247,[3]], + [33032,253,[3]], + [33032,259,[3]], + [33032,260,[3]], + [33032,8,[3]], + [33032,11,[0,3]], + [33032,16,[3]], + [33032,17,[3]], + [33032,22,[3]], + [33032,23,[3]], + [33032,25,[3]], + [33032,27,[3]], + [33032,28,[3]], + [33032,30,[3]], + [33032,34,[3]], + [33032,35,[3]], + [33032,36,[3]], + [33032,37,[3]], + [33032,40,[3]], + [33032,42,[3]], + [33032,45,[3]], + [33032,47,[3]], + [33032,48,[3]], + [33032,49,[3]], + [33032,50,[3]], + [33032,54,[3]], + [33032,56,[3]], + [33032,58,[3]], + [33032,60,[3]], + [33032,61,[3]], + [33032,62,[3]], + [33032,66,[3]], + [33032,67,[3]], + [33032,68,[3]], + [33032,69,[3]], + [33032,72,[3]], + [33032,73,[3]], + [33032,77,[3]], + [33032,78,[3]], + [33032,81,[3]], + [33032,82,[3]], + [33032,83,[3]], + [33032,84,[3]], + [33032,86,[3]], + [33032,88,[3]], + [33032,90,[3]], + [33032,91,[3]], + [33032,94,[3]], + [33032,95,[3]], + [33032,99,[3]], + [33032,101,[3]], + [33032,103,[3]], + [33032,105,[0,3]], + [33032,106,[3]], + [33032,107,[3]], + [33032,108,[0,3]], + [33032,109,[0,3]], + [33032,110,[0,3]], + [33032,111,[0,3]], + [33032,112,[3]], + [33041,488,[12]], + [33041,491,[0]], + [33041,492,[0]], + [33041,277,[10]], + [33041,289,[0]], + [33041,301,[0]], + [33041,305,[0]], + [33041,310,[0]], + [33041,320,[0]], + [33041,521,[0]], + [33041,113,[0]], + [33041,119,[0]], + [33041,125,[5]], + [33041,130,[0]], + [33041,136,[0]], + [33041,143,[0]], + [33041,149,[0]], + [33041,155,[0]], + [33041,161,[0]], + [33041,166,[0]], + [33041,173,[0]], + [33041,179,[0]], + [33041,184,[0]], + [33041,187,[0]], + [33041,194,[0]], + [33041,195,[0]], + [33041,196,[0]], + [33041,197,[0]], + [33041,198,[0]], + [33041,199,[0]], + [33041,200,[0]], + [33041,201,[0]], + [33041,202,[0]], + [33041,203,[0]], + [33041,204,[0]], + [33041,205,[0]], + [33041,206,[0]], + [33041,207,[0]], + [33041,208,[0]], + [33041,209,[0]], + [33041,210,[0]], + [33041,211,[0]], + [33041,217,[0]], + [33041,218,[0]], + [33041,229,[0]], + [33041,235,[0]], + [33041,236,[0]], + [33041,247,[0]], + [33041,249,[0]], + [33041,250,[0]], + [33041,253,[0]], + [33041,8,[0]], + [33041,12,[0]], + [33041,15,[0]], + [33041,16,[0]], + [33041,17,[0]], + [33041,22,[0]], + [33041,23,[0]], + [33041,24,[0]], + [33041,26,[0]], + [33041,29,[0]], + [33041,31,[0]], + [33041,34,[0]], + [33041,35,[0]], + [33041,36,[0]], + [33041,37,[0]], + [33041,41,[0]], + [33041,43,[0]], + [33041,44,[0]], + [33041,46,[0]], + [33041,48,[0]], + [33041,49,[0]], + [33041,50,[0]], + [33041,55,[0]], + [33041,57,[0]], + [33041,59,[0]], + [33041,61,[0]], + [33041,62,[0]], + [33041,66,[0]], + [33041,67,[0]], + [33041,70,[0]], + [33041,71,[0]], + [33041,74,[0]], + [33041,77,[0]], + [33041,78,[0]], + [33041,81,[0]], + [33041,82,[0]], + [33041,85,[0]], + [33041,87,[0]], + [33041,89,[0]], + [33041,90,[0]], + [33041,91,[0]], + [33041,94,[0]], + [33041,95,[0]], + [33041,98,[0]], + [33041,100,[0]], + [33041,102,[0]], + [33041,104,[0]], + [33041,105,[0,1]], + [33041,106,[0]], + [33041,107,[0]], + [33041,108,[0,1]], + [33041,109,[0,8]], + [33041,110,[0,1]], + [33041,111,[0,1]], + [33041,112,[0]], + [33837,471,[2]], + [33837,473,[1]], + [33837,475,[2,4]], + [33837,266,[2,4]], + [33837,278,[1]], + [33837,300,[7]], + [33837,306,[1]], + [33837,309,[1]], + [33837,323,[2]], + [33837,522,[2]], + [33837,118,[1]], + [33837,119,[1]], + [33837,130,[1]], + [33837,131,[1]], + [33837,135,[1]], + [33837,144,[1]], + [33837,150,[1]], + [33837,153,[1]], + [33837,159,[1]], + [33837,165,[1]], + [33837,174,[1]], + [33837,180,[1]], + [33837,183,[1]], + [33837,186,[1]], + [33837,191,[1]], + [33837,194,[1]], + [33837,205,[1]], + [33837,211,[1]], + [33837,212,[2]], + [33837,213,[2]], + [33837,214,[2]], + [33837,215,[1]], + [33837,216,[1]], + [33837,217,[1]], + [33837,218,[1]], + [33837,219,[1]], + [33837,220,[1]], + [33837,221,[1]], + [33837,222,[1]], + [33837,223,[1]], + [33837,224,[1]], + [33837,225,[1]], + [33837,226,[1]], + [33837,227,[1]], + [33837,228,[1]], + [33837,229,[1]], + [33837,230,[1]], + [33837,232,[1]], + [33837,234,[1]], + [33837,248,[1]], + [33837,254,[1]], + [33837,260,[1]], + [33837,11,[0,1]], + [33837,12,[1]], + [33837,13,[1]], + [33837,14,[1]], + [33837,15,[1]], + [33837,17,[0,1]], + [33837,19,[1]], + [33837,21,[1]], + [33837,23,[1]], + [33837,26,[1]], + [33837,27,[1]], + [33837,30,[1]], + [33837,31,[1]], + [33837,33,[0,1]], + [33837,35,[0,1]], + [33837,37,[2]], + [33837,39,[0,1]], + [33837,42,[1]], + [33837,43,[1]], + [33837,46,[0,1]], + [33837,47,[2]], + [33837,49,[1]], + [33837,50,[0,1]], + [33837,52,[1,5]], + [33837,55,[1]], + [33837,56,[0,1]], + [33837,57,[1,5]], + [33837,58,[1]], + [33837,62,[1]], + [33837,63,[1]], + [33837,65,[1,5]], + [33837,67,[0,1]], + [33837,71,[1]], + [33837,72,[1]], + [33837,73,[1]], + [33837,74,[1]], + [33837,76,[1]], + [33837,78,[1]], + [33837,79,[2]], + [33837,81,[2]], + [33837,84,[1]], + [33837,85,[0,1]], + [33837,86,[1]], + [33837,87,[1]], + [33837,91,[2]], + [33837,93,[1]], + [33837,94,[2]], + [33837,96,[1]], + [33837,100,[1]], + [33837,101,[1]], + [33837,102,[1]], + [33837,103,[1]], + [33837,108,[0,1]], + [33837,110,[0,1]], + [33837,111,[0,1]], + [33860,453,[8]], + [33860,455,[4]], + [33860,457,[7]], + [33860,266,[1,7]], + [33860,278,[2]], + [33860,300,[4]], + [33860,303,[2]], + [33860,312,[2]], + [33860,322,[4]], + [33860,523,[7]], + [33860,118,[2]], + [33860,119,[2]] + ], + "aggregate": [ + [33860,[0,3,5,106,116,125,127,129,131,138,142,144,148,152,155,156,159,161,167,170,173,175,178,179,184,200,203,205]], + [33876,[17,24,30,108,113,125,127,132,138,150,162,164,176,180,186,189,191,192,196,197,199,200,201]], + [33883,[0,3,14,22,109,119,134,135,137,140,142,145,148,153,156,165,181,188,193,208,209,211]], + [19154,[0]], + [19155,[0]], + [19201,[3]], + [19202,[3]], + [19235,[5]], + [19236,[5]], + [19153,[0]], + [19167,[1]], + [19168,[1]], + [19180,[2]], + [19181,[2]], + [19200,[3]], + [19214,[4]], + [19215,[4]], + [19233,[5]], + [19234,[5]], + [19277,[7]], + [19278,[7]], + [19289,[8]], + [19290,[8]], + [19291,[8]] + ] +} diff --git a/research/bit-one-chart-donor-envelope/LOCAL-PINS.json b/research/bit-one-chart-donor-envelope/LOCAL-PINS.json new file mode 100644 index 0000000000..267fa6735a --- /dev/null +++ b/research/bit-one-chart-donor-envelope/LOCAL-PINS.json @@ -0,0 +1,8 @@ +{ + "CERT.json": "36e221ac20102e40f0e419444d85b588278d3bdcd0e4c212bb2d907844811186", + "check_stock.py": "60aa3eb29bfe8c70d3014d118411215ef0324262654cf55ed8a52215115ca9a0", + "pr7200_verify.py": "90f23e033bfced9673da33c07123eb749493164d5557f372a16b674e45461e1f", + "price.py": "6a33aac4c7032de9bb3881da248f5371b69c6b9af0893220825727f3d4878fae", + "retag.py": "cf9b4fbe12225f3c258648d3e49660111976523babfa788dd09a267d9e7b904b", + "screen.py": "066b4c8315bbae5cfe0a74aecd05071d94d93d8f76b1e5825651f71bb5f5f89d" +} diff --git a/research/bit-one-chart-donor-envelope/NOTICE b/research/bit-one-chart-donor-envelope/NOTICE new file mode 100644 index 0000000000..3c7836c64a --- /dev/null +++ b/research/bit-one-chart-donor-envelope/NOTICE @@ -0,0 +1,7 @@ +Apache-2.0. The retained native word and full paired BIT bill come from +#7001 and its #6726 lineage. #7200 supplies the retag, normalized trace and +strict-prefix certificate, preserved in pr7200_verify.py, retag.py and +CERT.json. #7177 supplies the formal QUERY 349 credit. The directed price +helper price.py comes from the Round 36 whole-word fusion audit. #7277 +supplies the complete comparable benchmark. See README.md for exact links. +OpenAI Codex and subagents materially assisted. diff --git a/research/bit-one-chart-donor-envelope/PRICE.json b/research/bit-one-chart-donor-envelope/PRICE.json new file mode 100644 index 0000000000..be2d6bd91a --- /dev/null +++ b/research/bit-one-chart-donor-envelope/PRICE.json @@ -0,0 +1,48 @@ +{ + "changed_calls": 18, + "formal_H1_credit": 111, + "inputs": { + "deps/inputs/INVOICE.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "deps/inputs/WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "deps/price.py": "6a33aac4c7032de9bb3881da248f5371b69c6b9af0893220825727f3d4878fae", + "screen/CERT.json": "36e221ac20102e40f0e419444d85b588278d3bdcd0e4c212bb2d907844811186", + "screen/pr7200_verify.py": "90f23e033bfced9673da33c07123eb749493164d5557f372a16b674e45461e1f", + "screen/retag.py": "cf9b4fbe12225f3c258648d3e49660111976523babfa788dd09a267d9e7b904b" + }, + "old_native": { + "1": 1386, + "2": 1253, + "3": 62, + "4": 47, + "5": 9, + "6": 104, + "7": 10 + }, + "raw_baseline_paid_minus_targets": [ + "1173904281623971755156110103150303286313923542813/19531250000000000000000000000000000000000000000", + "300519496095736769319964186406477641296364427009319/5000000000000000000000000000000000000000000000000" + ], + "retag_cost_per_call": [ + "77380279700453902369070102717743791315527406941439/10000000000000000000000000000000000000000000000000", + "4836267481278368898066881419858986957220462933843/625000000000000000000000000000000000000000000000" + ], + "retag_delta": { + "1": -48, + "2": 21, + "3": -6, + "4": 6, + "6": -8, + "7": 8 + }, + "saving_needed_per_changed_call": [ + "147314004466607296880531703622057254378703696477693/30000000000000000000000000000000000000000000000000", + "49104668155535765626843901207352418126234565498079/10000000000000000000000000000000000000000000000000" + ], + "saving_needed_whole": [ + "441942013399821890641595110866171763136111089433079/5000000000000000000000000000000000000000000000000", + "441942013399821890641595110866171763136111089482711/5000000000000000000000000000000000000000000000000" + ], + "scope": "one distinct positive retained canonical donor chart per delivery, fixed field volume", + "target": "10018846261809/2500000000000000", + "zero_price_for_all_35_adjusted_moves_stock_upper_per_call": "15164440167204342855521567240849951195651793865281/125000000000000000000000000000000000000000000000" +} diff --git a/research/bit-one-chart-donor-envelope/README.md b/research/bit-one-chart-donor-envelope/README.md new file mode 100644 index 0000000000..3d9d1b145a --- /dev/null +++ b/research/bit-one-chart-donor-envelope/README.md @@ -0,0 +1,84 @@ +# One-chart donor exclusion for the fixed-volume BIT retag + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** The eight-port +retag of the retained #7001 BIT word has 35 adjusted deliveries. For each +delivery, consider a donor from one distinct positive canonical chart. +Grant free access through the first next contact with the recipient to +every normalized row previously observed in the chosen chart. The target +row is outside that span in all 22,190 chart/delivery pairs. Formation, +routing, ownership and restoration may all be free in this relaxation, +and each delivery may choose a different chart without interference. +The resulting optimistic whole-word saving upper bound is exactly zero. + +The fixed stock has 635 positive canonical charts, of which 627 have +nonzero observed rows. Each delivery has 634 alternate charts. The +exhaustive test finished with zero unresolved pairs. It includes +nonnested and oblique alternate chart pairs within the retained cache +contract. It leaves donors combining multiple charts, new synthesized +rows, different recipient deadlines, altered field volume and the other +103 ports outside the tested scope. + +## Price and evidence + +At fixed target κ = 0.0040075385047236, the replay reconstructs the +36-copy paid and productive invoice, charges 18 retagged calls and +credits the 111 formal rank-one savings from QUERY 349. The retag's +per-call native rank histogram changes by +`{1: -48, 2: 21, 3: -6, 4: 6, 6: -8, 7: 8}`. The directed interval +requires more than 88.3884026799643 raw units of further compatible +whole-word savings, or more than 4.91046681555357 per changed call. +The replay saves [PRICE.json](PRICE.json) before decoding donor +supports. The exact endpoints are in that receipt. + +The first engine computes high-pivot binary spans for the 659-column +normalized trace. The second engine solves the transposed low-pivot +dual equations separately for each chart/delivery pair. A separator +must vanish on all available donor rows and evaluate to one on the +target. Appending the target row in a synthetic fixture makes those +equations inconsistent. Both engines reuse the pinned trace and +geometry of #7200. Its 79 empty, 512 explicit and 382 shared-certificate +strict-prefix cases form the predecessor control. Its trace checks +normalized endpoints and 237 owned lifetimes. [STOCK.json](STOCK.json) +records the full census and all case-level price bounds. + +## Replay + +From a clean checkout, use CPython 3.12 with assertions enabled and +the standard library. + +~~~sh +python3.12 -B scripts/research_package.py --package research/bit-one-chart-donor-envelope +python3.12 -B scripts/check_research_commit.py --package research/bit-one-chart-donor-envelope --check-modes --check-source-history +~~~ + +A Git-free export including the two declared inputs can run +`python3.12 -I -B research/bit-one-chart-donor-envelope/replay.py --root .`. +The replay authenticates workspace-relative inputs by SHA-256 and Git +blob ID and rejects duplicate JSON keys and source paths. It compares +all deterministic price and stock fields. + +## Predecessors + +[#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001) at +`d777f3a0aa2878bea0478918923dabcf86b9878b` supplies the retained +signed BIT caller and invoice, and #6726 supplies its native word. +[#7200](https://github.com/CrocSwap/integer-mult-bounds/pull/7200) at +`08f41734863055b42b3975c0d434ecf2ca4fcaf8` supplies the exact retag, +trace and strict-prefix controls. This package extends its tested cache +domain to every distinct retained positive chart. [#7177](https://github.com/CrocSwap/integer-mult-bounds/pull/7177) +at `f59cf773c6038d72bc3b5aeae204cbe1923b34bf` supplies the formal +QUERY 349 credit. [#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) +at `ed090b57ed88f8859e5ff4643645099e6ba856ea` supplies the complete +comparable κ = 0.003645669928698. The exact native input and invoice in +this replay come from canonical commit +`e54523517d0f03e58352e647c403a5af3e525a57`. OpenAI Codex and +subagents materially assisted. + +## Open next questions + +Can a changed provider supply a row through a richer chart interface? +The next test should pin that chart and ownership contract and bound +the fully charged stock across all relevant deliveries before building +one instance. An algebraic fit would still need signed forward and +adjoint action, ownership and restoration, and a complete paid and tape +invoice. diff --git a/research/bit-one-chart-donor-envelope/SOURCES.json b/research/bit-one-chart-donor-envelope/SOURCES.json new file mode 100644 index 0000000000..64f01435ff --- /dev/null +++ b/research/bit-one-chart-donor-envelope/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "usage": "input" + }, + { + "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8", + "path": "research/paired-query-only-bit/EFREE-RESULT.json", + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "usage": "input" + } + ], + "schema_version": 1 +} diff --git a/research/bit-one-chart-donor-envelope/STOCK.json b/research/bit-one-chart-donor-envelope/STOCK.json new file mode 100644 index 0000000000..caf4d0b5b8 --- /dev/null +++ b/research/bit-one-chart-donor-envelope/STOCK.json @@ -0,0 +1,490 @@ +{ + "all_chart_pairs": 22190, + "changed_calls": 18, + "decision": "PIVOT", + "formal_H1_credit": 111, + "formation_routing_ownership_restoration": "granted free in upper, nonnegative when charged", + "inputs": { + "deps/inputs/INVOICE.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "deps/inputs/WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "deps/price.py": "6a33aac4c7032de9bb3881da248f5371b69c6b9af0893220825727f3d4878fae", + "screen/CERT.json": "36e221ac20102e40f0e419444d85b588278d3bdcd0e4c212bb2d907844811186", + "screen/pr7200_verify.py": "90f23e033bfced9673da33c07123eb749493164d5557f372a16b674e45461e1f", + "screen/retag.py": "cf9b4fbe12225f3c258648d3e49660111976523babfa788dd09a267d9e7b904b" + }, + "lower_price_pairs": 0, + "nonnested_span_pairs": 0, + "old_native": { + "1": 1386, + "2": 1253, + "3": 62, + "4": 47, + "5": 9, + "6": 104, + "7": 10 + }, + "optimistic_saving_upper_per_call": "0", + "optimistic_saving_upper_whole": "0", + "positive_declared_charts": 635, + "positive_observed_charts": 627, + "predecessor_control": { + "aggregate_cases": 382, + "aggregate_recipients": 24, + "empty": 79, + "explicit": 512 + }, + "raw_baseline_paid_minus_targets": [ + "1173904281623971755156110103150303286313923542813/19531250000000000000000000000000000000000000000", + "300519496095736769319964186406477641296364427009319/5000000000000000000000000000000000000000000000000" + ], + "retag_cost_per_call": [ + "77380279700453902369070102717743791315527406941439/10000000000000000000000000000000000000000000000000", + "4836267481278368898066881419858986957220462933843/625000000000000000000000000000000000000000000000" + ], + "retag_delta": { + "1": -48, + "2": 21, + "3": -6, + "4": 6, + "6": -8, + "7": 8 + }, + "saving_needed_per_changed_call": [ + "147314004466607296880531703622057254378703696477693/30000000000000000000000000000000000000000000000000", + "49104668155535765626843901207352418126234565498079/10000000000000000000000000000000000000000000000000" + ], + "saving_needed_whole": [ + "441942013399821890641595110866171763136111089433079/5000000000000000000000000000000000000000000000000", + "441942013399821890641595110866171763136111089482711/5000000000000000000000000000000000000000000000000" + ], + "schedule": "grants independent donor availability through next target contact, no interference", + "scope": "one distinct positive retained canonical donor chart per delivery, fixed field volume", + "scope_exhausted": true, + "shortfall_remaining_lower": "441942013399821890641595110866171763136111089433079/5000000000000000000000000000000000000000000000000", + "sites": [ + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 20985, + "event": 19152, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 125 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 20996, + "event": 19153, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 126 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22592, + "event": 19154, + "nonnested_support": 0, + "old_rank": 4, + "saving_upper": "0", + "support_count": 0, + "target_chart": 270 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22656, + "event": 19155, + "nonnested_support": 0, + "old_rank": 4, + "saving_upper": "0", + "support_count": 0, + "target_chart": 272 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 21907, + "event": 19166, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 212 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 21917, + "event": 19167, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 213 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 21928, + "event": 19168, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 214 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22096, + "event": 19179, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 230 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22107, + "event": 19180, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 231 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22117, + "event": 19181, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 232 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 20986, + "event": 19199, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 125 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 21006, + "event": 19200, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 127 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22566, + "event": 19201, + "nonnested_support": 0, + "old_rank": 4, + "saving_upper": "0", + "support_count": 0, + "target_chart": 269 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22760, + "event": 19202, + "nonnested_support": 0, + "old_rank": 4, + "saving_upper": "0", + "support_count": 0, + "target_chart": 275 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22095, + "event": 19213, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 230 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22127, + "event": 19214, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 233 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22138, + "event": 19215, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 234 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 20849, + "event": 19233, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 113 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 20859, + "event": 19234, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 114 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22655, + "event": 19235, + "nonnested_support": 0, + "old_rank": 4, + "saving_upper": "0", + "support_count": 0, + "target_chart": 272 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22699, + "event": 19236, + "nonnested_support": 0, + "old_rank": 4, + "saving_upper": "0", + "support_count": 0, + "target_chart": 273 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 21908, + "event": 19276, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 212 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 21939, + "event": 19277, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 215 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 21949, + "event": 19278, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 216 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22286, + "event": 19289, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 248 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22296, + "event": 19290, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 249 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 22307, + "event": 19291, + "nonnested_support": 0, + "old_rank": 2, + "saving_upper": "0", + "support_count": 0, + "target_chart": 250 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 32910, + "event": 32929, + "nonnested_support": 0, + "old_rank": 7, + "saving_upper": "0", + "support_count": 0, + "target_chart": 525 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 32961, + "event": 32981, + "nonnested_support": 0, + "old_rank": 7, + "saving_upper": "0", + "support_count": 0, + "target_chart": 531 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 33011, + "event": 33032, + "nonnested_support": 0, + "old_rank": 7, + "saving_upper": "0", + "support_count": 0, + "target_chart": 536 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 33019, + "event": 33041, + "nonnested_support": 0, + "old_rank": 7, + "saving_upper": "0", + "support_count": 0, + "target_chart": 537 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 33814, + "event": 33837, + "nonnested_support": 0, + "old_rank": 7, + "saving_upper": "0", + "support_count": 0, + "target_chart": 628 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 33836, + "event": 33860, + "nonnested_support": 0, + "old_rank": 7, + "saving_upper": "0", + "support_count": 0, + "target_chart": 631 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 33851, + "event": 33876, + "nonnested_support": 0, + "old_rank": 7, + "saving_upper": "0", + "support_count": 0, + "target_chart": 633 + }, + { + "chart_count": 634, + "cheaper": [], + "cheaper_count": 0, + "due": 33857, + "event": 33883, + "nonnested_support": 0, + "old_rank": 7, + "saving_upper": "0", + "support_count": 0, + "target_chart": 634 + } + ], + "span_pairs": 0, + "target": "10018846261809/2500000000000000", + "unresolved_sites": 0, + "zero_price_for_all_35_adjusted_moves_stock_upper_per_call": "15164440167204342855521567240849951195651793865281/125000000000000000000000000000000000000000000000" +} diff --git a/research/bit-one-chart-donor-envelope/TASK.json b/research/bit-one-chart-donor-envelope/TASK.json new file mode 100644 index 0000000000..9ebacb48a3 --- /dev/null +++ b/research/bit-one-chart-donor-envelope/TASK.json @@ -0,0 +1,77 @@ +{ + "actual_scope": "One distinct positive retained canonical donor chart per adjusted delivery on the exact eight-port #7200 retag of the #7001 BIT word.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Round 39 research campaign", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Bound complete compatible BIT savings before building a physical donor.", + "budget_minutes": 2, + "evidence": "Exact normalized endpoint and ownership checks, directed price, exhaustive primal separation and separate dual-equation replay over all 22,190 chart/site pairs.", + "open_questions": [ + { + "blocked_by": "A successful algebraic fit must still preserve signed arbitrary-input action, ownership and restoration with all paid and tape costs charged.", + "first_step": "Pin the chart/ownership contract and bound compatible fully charged stock at all relevant deliveries before constructing a new donor.", + "question": "Can a changed provider synthesize a supported donor beyond the retained one-chart cache?", + "why_it_matters": "No retained single-chart span contains any of the 35 requested rows at its deadline." + } + ], + "original_card": { + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "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.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "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." + }, + "id": "bit-helper-contract", + "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." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "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." + ], + "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", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "This tests the fixed-volume nonnested and oblique retained-cache class left open by the strict-prefix envelope.", + "scope_status": "changed", + "stop_rule": "Save the directed signed whole-word price before decoding. Exhaust 35 deliveries times 634 alternate charts or stop with explicit unresolved cases. Pivot if the optimistic summed stock cannot meet the shortfall.", + "task_id": "bit-helper-contract" +} diff --git a/research/bit-one-chart-donor-envelope/VERIFY.json b/research/bit-one-chart-donor-envelope/VERIFY.json new file mode 100644 index 0000000000..6c49093beb --- /dev/null +++ b/research/bit-one-chart-donor-envelope/VERIFY.json @@ -0,0 +1,24 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py", + "--root", + "." + ], + "checks": "Reconstruct the retag and whole signed invoice, price before decoding, exhaust 22,190 single-chart pairs and independently solve all separating dual systems.", + "timeout_seconds": 30 + } + ], + "inputs": [ + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "research/paired-query-only-bit/EFREE-RESULT.json" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/bit-one-chart-donor-envelope/check_stock.py b/research/bit-one-chart-donor-envelope/check_stock.py new file mode 100644 index 0000000000..d8b8e9dd7e --- /dev/null +++ b/research/bit-one-chart-donor-envelope/check_stock.py @@ -0,0 +1,74 @@ +"""Verify the zero-stock receipt by solving the dual parity equations.""" +import argparse +import gzip +import json +from pathlib import Path +import runpy +import time + +from screen import authenticated + + +def consistent(equations): + """Equations have the coefficient bitset followed by the right side in bit 0.""" + pivots = {} + for equation in equations: + while equation > 1: + key = (equation & -2) & -(equation & -2) + if key in pivots: + equation ^= pivots[key] + else: + pivots[key] = equation + break + else: + if equation: + return False + return True + + +def verify(deps, receipt_path): + here = Path(__file__).resolve().parent + authenticated({"deps": deps, "screen": here}) + src = runpy.run_path(str(here / "pr7200_verify.py")) + rewrite = runpy.run_path(str(here / "retag.py")) + word = json.loads(gzip.decompress((deps / "inputs/WORD.json.gz").read_bytes())) + expected = json.loads(receipt_path.read_text()) + frames, ranks, canonical = src["geometry"](word) + changed, origin, adjusted, _ = rewrite["retag"](word, rewrite["modules"](word)) + _, sites, observed = src["trace"](changed, origin, adjusted, frames, ranks, canonical) + assert len(sites) == len(expected["sites"]) == 35 + charts = {chart for chart in canonical.values() if ranks[chart]} + chart_total = len(charts) + assert chart_total == 635 + assert sum(bool(observed.get(chart)) for chart in charts) == 627 + assert consistent([3]) and not consistent([2, 3]) + # An appended copy of the target makes a previously separating dual impossible. + assert consistent([2, 4, 9]) and not consistent([2, 4, 8, 9]) + count = 0 + for site, record in zip(sites, expected["sites"], strict=True): + assert all(site[k] == record[k] for k in ("event", "target_chart", "due")) + n = 0 + for chart in charts - {site["target_chart"]}: + rows = observed.get(chart, {}) + equations = [2 * row for row, cut in rows.items() if cut <= site["due"]] + equations.append(2 * site["target_row"] + 1) + assert consistent(equations), (site["event"], chart) + n += 1 + assert n == record["chart_count"] == 634 + count += n + assert count == expected["all_chart_pairs"] == 22190 + assert expected["optimistic_saving_upper_whole"] == "0" + print(json.dumps({"dual_systems_consistent": count, "sites": len(sites), + "positive_charts": chart_total, "controls": "PASS"})) + + +if __name__ == "__main__": + start = time.monotonic() + if not __debug__: + raise RuntimeError("Run with assertions enabled") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--deps", type=Path, required=True) + parser.add_argument("--receipt", type=Path, required=True) + args = parser.parse_args() + verify(args.deps.resolve(), args.receipt.resolve()) + print(f"seconds={time.monotonic()-start:.6f}") diff --git a/research/bit-one-chart-donor-envelope/pr7200_verify.py b/research/bit-one-chart-donor-envelope/pr7200_verify.py new file mode 100644 index 0000000000..3e67a33688 --- /dev/null +++ b/research/bit-one-chart-donor-envelope/pr7200_verify.py @@ -0,0 +1,224 @@ +"""Check retained strict-prefix separation on the literal eight-port BIT retag.""" +from collections import Counter, defaultdict +from fractions import Fraction +import gzip +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BIT = ROOT / "research/paired-query-only-bit" +PINS = { + "retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "independent/interval_gate.py": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec", +} +TRIAL = Fraction("0.004008162992724") + + +def checked(path, expected): + raw = path.read_bytes() + if sha256(raw).hexdigest() != expected: + raise ValueError(f"SHA-256 mismatch: {path}") + return raw + + +def load(path): + spec = spec_from_file_location(path.stem, path) + module = module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def eliminate(rows): + pivots = {} + for vector in rows: + row = list(map(Fraction, vector)) + for pivot, previous in sorted(pivots.items()): + factor = row[pivot] + row = [a - factor * b for a, b in zip(row, previous, strict=True)] + pivot = next((i for i, x in enumerate(row) if x), None) + if pivot is not None: + pivots[pivot] = tuple(x / row[pivot] for x in row) + for pivot, row in sorted(pivots.items(), reverse=True): + for earlier in (i for i in pivots if i < pivot): + previous = pivots[earlier] + pivots[earlier] = tuple(a - previous[pivot] * b for a, b in zip(previous, row, strict=True)) + return tuple(row for _, row in sorted(pivots.items())) + + +def geometry(word): + frames = {} + ranks = {} + canonical = {} + names = {} + for f, entry in sorted((int(k), v) for k, v in word["frames"].items()): + head = eliminate(entry["B"]) + tail = eliminate(entry["A"]) + rank = entry["dim"] + assert len(head) == rank and len(tail) == 8 - rank + assert all(len(x) == 8 for x in head + tail) + assert all(sum(a * b for a, b in zip(x, y, strict=True)) == 0 for x in head for y in tail) + ranks[f], frames[f] = rank, (head, tail) + canonical[f] = names.setdefault(head, f) + return frames, ranks, canonical + + +def trace(word, origin, adjusted, frames, ranks, canonical): + public, owned = word["public"], word["owned_fields"] + charts = [*word["start"], *([None] * owned)] + rows = [*(1 << i for i in range(public)), *([0] * owned)] + cache = defaultdict(dict) + sites, pending = [], {} + paid, nesting = Counter(), {} + active = peak = erasures = 0 + + def observe(role, cut): + chart, row = charts[role], rows[role] + if chart is not None and row: + cache[canonical[chart]].setdefault(row, cut) + + for role in range(len(rows)): + observe(role, 0) + for cut, (old_event, event) in enumerate(zip(origin, word["program"], strict=True)): + op, role, *args = event + touched = event[1:3] if op in ("ADD", "SWAP") else event[1:2] + for owner in touched: + if owner in pending: + pending.pop(owner)["due"] = cut + if op == "ADD": + donor, chart = args + assert charts[role] == charts[donor] == chart + rows[role] ^= rows[donor] + elif op == "SWAP": + other, = args + charts[role], charts[other] = charts[other], charts[role] + rows[role], rows[other] = rows[other], rows[role] + observe(other, cut + 1) + elif op == "INIT": + assert role >= public and charts[role] is None and not rows[role] + charts[role] = args[0] + active += 1 + peak = max(peak, active) + elif op == "CLEAR": + assert role >= public and charts[role] == args[0] + charts[role], rows[role] = None, 0 + active -= 1 + erasures += 1 + else: + source, target = args + assert op == "MOVE" and charts[role] == source + smaller, larger = sorted(args, key=ranks.__getitem__) + if (smaller, larger) not in nesting: + nesting[smaller, larger] = all( + sum(a * b for a, b in zip(x, y, strict=True)) == 0 + for x in frames[smaller][0] for y in frames[larger][1]) + delta = ranks[larger] - ranks[smaller] + assert delta > 0 and nesting[smaller, larger] + paid[delta] += 1 + if old_event in adjusted: + assert source == 0 and rows[role] + site = {"event": old_event, "target_chart": canonical[target], + "target_row": rows[role], "due": len(origin)} + sites.append(site) + pending[role] = site + charts[role] = target + observe(role, cut + 1) + assert charts == [*word["final"], *([None] * owned)] and active == 0 + assert rows[:public] == [(1 << i) ^ ((1 << (i - 111)) if 111 <= i < 222 else 0) for i in range(public)] + assert (peak, erasures) == (237, 237) + return paid, sites, cache + + +def decode_duals(entries): + result = {} + for *ids, coordinates in entries: + key = tuple(ids) + assert key not in result + assert coordinates == sorted(set(coordinates)) and all(0 <= j < 659 for j in coordinates) + result[key] = sum(1 << j for j in coordinates) + return result + + +def separates(dual, target, rows): + return (dual & target).bit_count() % 2 == 1 and all((dual & row).bit_count() % 2 == 0 for row in rows) + + +def support_check(sites, cache, frames, ranks, canonical, certificate): + explicit = decode_duals(certificate["explicit"]) + aggregate = decode_duals(certificate["aggregate"]) + checked = Counter() + for site in sites: + event, target, due, target_row = (site[k] for k in ("event", "target_chart", "due", "target_row")) + for chart, rep in canonical.items(): + if chart != rep or not 0 < ranks[chart] < ranks[target]: + continue + if not all(sum(a * b for a, b in zip(x, y, strict=True)) == 0 + for x in frames[chart][0] for y in frames[target][1]): + continue + rows = [row for row, cut in cache[chart].items() if cut <= due] + if not rows: + checked["empty"] += 1 + continue + key = (event, chart) + if key in explicit: + dual = explicit.pop(key) + checked["explicit"] += 1 + else: + dual = aggregate[event,] + checked["aggregate_cases"] += 1 + checked[event] += 1 + if not separates(dual, target_row, rows): + raise ValueError(f"Invalid separator for event {event}, chart {chart}") + assert not explicit and set(aggregate) == {(event,) for event in checked if isinstance(event, int)} + assert {k: checked[k] for k in ("empty", "explicit", "aggregate_cases")} == { + "empty": 79, "explicit": 512, "aggregate_cases": 382} + assert len(aggregate) == 24 + return {"empty": 79, "explicit": 512, "aggregate_cases": 382, "aggregate_recipients": 24} + + +def price(gate, invoice, old, new): + assert old == {int(r): n for r, n in invoice["native_paid"].items()} + delta = {r: new[r] - old[r] for r in new.keys() | old.keys() if new[r] != old[r]} + assert delta == {1: -48, 2: 21, 3: -6, 4: 6, 6: -8, 7: 8} + paid = {int(r): n for r, n in invoice["paid"].items()} + targets = {int(r): n for r, n in invoice["targets"].items()} + raw_allowance = gate.add(gate.exact(111), gate.sub(gate.moment(targets, TRIAL), gate.moment(paid, TRIAL))) + cost = gate.moment(delta, TRIAL) + allowance = gate.div(raw_allowance, gate.exact(18)) + excess = gate.sub(cost, allowance) + assert excess[0] > 0 + return {"trial": str(TRIAL), "delta": delta, "cost": gate.show(cost), + "conditional_allowance": gate.show(allowance), "excess": gate.show(excess)} + + +def main(): + if not __debug__: + raise RuntimeError("Run with assertions enabled") + assert separates(4, 5, [1, 2]) and not separates(4, 5, [1, 2, 4]) + assert not separates(1, 2, [4]) + data = {k: checked(BIT / k, digest) for k, digest in PINS.items()} + word = json.loads(gzip.decompress(data["retained/inputs/BIT-NATIVE-WORD.json.gz"])) + invoice = json.loads(data["EFREE-RESULT.json"]) + gate = load(BIT / "independent/interval_gate.py") + rewrite = load(HERE / "retag.py") + certificate = json.loads((HERE / "CERT.json").read_text(encoding="utf-8")) + frames, ranks, canonical = geometry(word) + changed, origin, adjusted, _ = rewrite.retag(word, rewrite.modules(word)) + old_paid, _, _ = trace(word, range(len(word["program"])), {}, frames, ranks, canonical) + new_paid, sites, cache = trace(changed, origin, adjusted, frames, ranks, canonical) + assert len(sites) == len(adjusted) == 35 + assert next(row for row in sites if row["event"] == 19234)["target_row"] == (1 << 5) | (1 << 235) + support = support_check(sites, cache, frames, ranks, canonical, certificate) + receipt = {"support": support, "sites": 35, "available_strict_donor_credit": [0, 0], + "price": price(gate, invoice, old_paid, new_paid)} + expected = HERE / "RESULT.json" + assert json.loads(expected.read_text(encoding="utf-8")) == json.loads(json.dumps(receipt)) + print(json.dumps(receipt, sort_keys=True, indent=2)) + print("PASS_BIT_STRICT_PREFIX_ENVELOPE sites=35 explicit=512 aggregate=382 no_new_kappa") + + +if __name__ == "__main__": + main() diff --git a/research/bit-one-chart-donor-envelope/price.py b/research/bit-one-chart-donor-envelope/price.py new file mode 100644 index 0000000000..799226172f --- /dev/null +++ b/research/bit-one-chart-donor-envelope/price.py @@ -0,0 +1,367 @@ +"""Independent exact read-lineage, geometry and disjoint-price audit.""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +WORD = "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" +INVOICE = "research/paired-query-only-bit/EFREE-RESULT.json" +TARGET = "10018846261809/2500000000000000" +TRIAL = "1002040748181/250000000000000" +SCALE = 10**49 + + +def read_inputs(root): + pins = {} + sources = HERE / "replay/bit/SOURCES.tsv" + for line in sources.read_text().splitlines(): + key, expected, _ = line.split("\t") + path = Path(key) + if path.is_absolute() or ".." in path.parts or key in pins: + raise ValueError(f"invalid source key {key}") + contents = (root / path).read_bytes() + if sha256(contents).hexdigest() != expected: + raise ValueError(f"changed source {key}") + pins[key] = expected + return ( + json.loads(gzip.decompress((root / WORD).read_bytes())), + json.loads((root / INVOICE).read_bytes()), + pins, + ) + + +def walk(word, observe_move=None): + """Track logical owner identities through transparent physical SWAPs.""" + public = word["public"] + slots = [(j, f, 1 << j) for j, f in enumerate(word["start"])] + slots.extend((None, None, 0) for _ in range(word["owned_fields"])) + history = defaultdict(list) + moves = {} + ownership = Counter() + for clock, (op, i, *args) in enumerate(word["program"]): + owner, frame, row = slots[i] + if op == "SWAP": + (j,) = args + slots[i], slots[j] = slots[j], slots[i] + continue + if op == "INIT": + (f,) = args + assert i >= public and slots[i] == (None, None, 0) + slots[i] = (public + clock, f, 0) + ownership["init"] += 1 + continue + assert owner is not None + history[owner].append((clock, op)) + if op == "MOVE": + src, dst = args + assert src == frame and src != dst + if observe_move is not None: + observe_move(clock, i, src, dst, row, slots) + moves[clock] = (src, dst, row) + slots[i] = (owner, dst, row) + elif op == "ADD": + j, f = args + other, other_frame, other_row = slots[j] + assert other is not None and frame == f == other_frame + if other != owner: + history[other].append((clock, op)) + slots[i] = (owner, frame, row ^ other_row) + else: + assert op == "CLEAR" and i >= public and args == [frame] + ownership["clear"] += 1 + slots[i] = (None, None, 0) + assert [x[1] for x in slots] == word["final"] + [None] * word["owned_fields"] + expected = [1 << j if j < public else 0 for j in range(len(slots))] + for j in range(111): + expected[j + 111] ^= 1 << j + assert [x[2] for x in slots] == expected + + runs = [] + for records in history.values(): + chain = [] + for clock, op in records: + if op == "MOVE": + chain.append(clock) + elif chain: + runs.append(tuple(chain)) + chain.clear() + if chain: + runs.append(tuple(chain)) + runs.sort() + covered = [t for run in runs for t in run] + assert len(covered) == len(set(covered)) == len(moves) and set(covered) == set(moves) + assert all(moves[i][1] == moves[j][0] for run in runs for i, j in zip(run, run[1:])) + return moves, runs, ownership + + +def annihilator(rows): + """Exact RREF, then a basis of the right nullspace of each chart.""" + matrix = [list(map(Fraction, row)) for row in rows] + pivots = [] + for col in range(8): + pivot = len(pivots) + hit = next((i for i in range(pivot, len(matrix)) if matrix[i][col]), None) + if hit is None: + continue + matrix[hit], matrix[pivot] = matrix[pivot], matrix[hit] + a = matrix[pivot] + p = a[col] + matrix[pivot] = [x / p for x in a] + for i, row in enumerate(matrix): + if i != pivot and row[col]: + b = row[col] + matrix[i] = [x - b*y for x, y in zip(row, matrix[pivot], strict=True)] + pivots.append(col) + assert len(pivots) == len(rows) + normals = [] + for f in set(range(8)) - set(pivots): + v = [Fraction(0)] * 8 + v[f] = Fraction(1) + for i, p in enumerate(pivots): + v[p] = -matrix[i][f] + normals.append(v) + return normals + + +def verify_incidence(word, moves, runs): + ranks = {int(f): v["dim"] for f, v in word["frames"].items()} + bases = {int(f): [[Fraction(x) for x in row] for row in v["B"]] + for f, v in word["frames"].items()} + assert all(len(bases[f]) == r for f, r in ranks.items()) + + @cache + def normals(frame): + return annihilator(bases[frame]) + + @cache + def endpoint_type(src, dst): + if src == dst: + return "identical" + if ranks[src] == ranks[dst]: + return "equal_rank_distinct" + low, high = sorted((src, dst), key=ranks.__getitem__) + if any(sum(a*b for a, b in zip(row, normal, strict=True)) + for row in bases[low] for normal in normals(high)): + return "nonnested" + return "nested" + + total = Counter() + domains = [] + for chain in runs: + starting = defaultdict(list) + for i, a in enumerate(chain): + for j in range(i + 1, len(chain)): + b = chain[j] + src, dst = moves[a][0], moves[b][1] + kind = endpoint_type(src, dst) + total[kind] += 1 + if kind in ("identical", "nested"): + delta = Counter(abs(ranks[moves[t][0]] - ranks[moves[t][1]]) + for t in chain[i:j+1]) + if src != dst: + delta[abs(ranks[src] - ranks[dst])] -= 1 + starting[i].append((j+1, (a, b, src, dst), delta)) + domains.append((len(chain), starting)) + old = Counter(abs(ranks[src] - ranks[dst]) for src, dst, _ in moves.values()) + return total, domains, old, ranks + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def optimize(domains, copies, k, declared): + valid = {} + totals = [Fraction(0), Fraction(0)] + for chain, (n, starts) in enumerate(domains): + def extreme(side): + suffix = [Fraction(0)] * (n+1) + for i in range(n-1, -1, -1): + suffix[i] = max( + [suffix[i+1]] + + [suffix[j] + cost(delta, k)[side] for j, _, delta in starts[i]] + ) + return suffix[0] + for side in (0, 1): + totals[side] += copies*extreme(side) + for i, intervals in starts.items(): + for j, key, delta in intervals: + assert key not in valid + valid[key] = (chain, i, j, delta) + seen = set() + chosen = Counter() + for item in declared: + key = tuple(item) + if key not in valid: + raise ValueError(f"invalid chosen interval {item}") + chain, i, j, delta = valid[key] + paid = {(chain, x) for x in range(i, j)} + if seen & paid: + raise ValueError(f"overlapping chosen interval {item}") + seen.update(paid) + chosen.update(delta) + return totals, cost({r: copies*n for r, n in chosen.items()}, k) + + +def intersect(a, b): + return max(a[0], b[0]) <= min(a[1], b[1]) + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies + + +def audit(root, receipt): + word, invoice, pins = read_inputs(root) + assert receipt["status"] == "PASS_WHOLE_WORD_FUSION_UPPER" + assert receipt["pins"] == pins + assert invoice["native_source_sha256"] == pins[WORD] + moves, runs, ownership = walk(word) + counts, domains, old, ranks = verify_incidence(word, moves, runs) + signed, copies = profile(invoice, old, word, ranks) + path_lengths = Counter(map(len, runs)) + assert {str(r): n for r, n in path_lengths.items()} == receipt["path_length_histogram"] + assert {str(r): n for r, n in old.items()} == receipt["charged_ranks"] + assert receipt["native_paid_moves"] == sum(old.values()) and receipt["native_instances"] == copies + assert receipt["physical_sites"] == 0 + audit_result = {} + for trial, declared in receipt["result"].items(): + k = Fraction(trial) + expected_case_count = sum(counts.values()) + expected_eligible_count = counts["nested"] + counts["identical"] + if declared["cases_visited"] != expected_case_count or declared["eligible_intervals"] != expected_eligible_count: + raise ValueError("incorrect exhaustive incidence counters") + savings, chosen = optimize(domains, copies, k, declared["optimistic_argmax"]) + baseline = cost(signed, k) + net = [a+b for a,b in zip(baseline, savings, strict=True)] + for field, v in (("saving_interval", savings), ("raw_comparator_net", baseline), + ("net_after_free_fusion", net)): + if not intersect(v, list(map(Fraction, declared[field]))): + raise ValueError(f"forged {field}") + if not intersect(chosen, list(map(Fraction, declared["saving_interval"]))): + raise ValueError("selected intervals fail to realize claimed upper at price precision") + audit_result[trial] = { + "baseline": list(map(str, baseline)), + "saving": list(map(str, savings)), + "net": list(map(str, net)), + "selected_interval_saving": list(map(str, chosen)), + } + assert TARGET in audit_result + if Fraction(audit_result[TARGET]["net"][1]) < 0: + assert set(audit_result) == {TARGET} + return { + "status": "PASS_INDEPENDENT_FUSION_AUDIT", + "paid_moves": len(moves), + "ownership": dict(ownership), + "paths": len(runs), + "incidence_by_endpoint": dict(counts), + "source_sha256": pins[WORD], + "invoice_sha256": pins[INVOICE], + "independent_result": audit_result, + } + + +def control(): + e1 = [1, 0, 0, 0, 0, 0, 0, 0] + e2 = [0, 1, 0, 0, 0, 0, 0, 0] + frames = {"0": {"dim": 0, "B": []}, "1": {"dim": 1, "B": [e1]}, + "2": {"dim": 2, "B": [e1, e2]}} + moves = {0: (0, 1, 0), 2: (1, 2, 0), 4: (2, 0, 0)} + counts, domains, _, _ = verify_incidence({"frames": frames}, moves, [(0, 2, 4)]) + assert counts == {"nested": 2, "identical": 1} + savings, selected = optimize(domains, 36, Fraction(TARGET), [(0, 4, 0, 0)]) + assert tuple(savings) == selected and savings[0] > 0 + try: + optimize(domains, 36, Fraction(TARGET), [(0, 2, 0, 2), (0, 4, 0, 0)]) + except ValueError as error: + assert "overlapping" in str(error) + else: + raise AssertionError("overlap control accepted a double-spent paid MOVE") + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("input_root", type=Path) + parser.add_argument("receipt", type=Path) + args = parser.parse_args() + assert __debug__ + control() + receipt = json.loads(args.receipt.read_bytes()) + print(json.dumps(audit(args.input_root, receipt), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/bit-one-chart-donor-envelope/replay.py b/research/bit-one-chart-donor-envelope/replay.py new file mode 100644 index 0000000000..563b7cbffa --- /dev/null +++ b/research/bit-one-chart-donor-envelope/replay.py @@ -0,0 +1,106 @@ +"""Check the signed BIT bill and replay both one-chart separation engines.""" +from argparse import ArgumentParser +from collections import Counter +import gzip +from hashlib import sha1, sha256 +import json +from pathlib import Path +import runpy +import shutil +import subprocess +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +BIT = "research/paired-query-only-bit/" +FILES = { + BIT + "retained/inputs/BIT-NATIVE-WORD.json.gz": "WORD.json.gz", + BIT + "EFREE-RESULT.json": "INVOICE.json", +} + + +def keyed(items): + result = dict(items) + assert len(result) == len(items), "duplicate JSON key" + return result + + +def read_json(raw): + return json.loads(raw, object_pairs_hook=keyed) + + +def source_index(rows): + pins = {row["path"]: row for row in rows} + assert len(pins) == len(rows), "duplicate source path" + return pins + + +def reject(fn, value): + try: + fn(value) + except AssertionError: + return + raise AssertionError("duplicate control accepted") + + +def run(root): + reject(read_json, b'{"a":1,"a":2}') + reject(source_index, [{"path": "same"}, {"path": "same"}]) + pins = source_index(read_json((HERE / "SOURCES.json").read_bytes())["files"]) + assert set(FILES) == {key for key, pin in pins.items() if pin["usage"] == "input"} + for key, digest in read_json((HERE / "LOCAL-PINS.json").read_bytes()).items(): + assert sha256((HERE / key).read_bytes()).hexdigest() == digest, key + with TemporaryDirectory(prefix="bit-donor-replay-") as scratch: + temp = Path(scratch) + deps = temp / "deps" + inputs = deps / "inputs" + inputs.mkdir(parents=True) + inputs_data = {} + for key, filename in FILES.items(): + raw = (root / key).read_bytes() + pin = pins[key] + assert sha256(raw).hexdigest() == pin["sha256"], ("changed input", key) + assert sha1(f"blob {len(raw)}\0".encode() + raw).hexdigest() == pin["git_blob"], key + inputs_data[filename] = read_json(gzip.decompress(raw) if filename.endswith(".gz") else raw) + (inputs / filename).write_bytes(raw) + shutil.copyfile(HERE / "price.py", deps / "price.py") + word = inputs_data["WORD.json.gz"] + invoice = inputs_data["INVOICE.json"] + price = runpy.run_path(str(HERE / "price.py")) + moves, _, _ = price["walk"](word) + ranks = {int(key): frame["dim"] for key, frame in word["frames"].items()} + native = Counter(abs(ranks[src] - ranks[dst]) for src, dst, _ in moves.values()) + _, copies = price["profile"](invoice, native, word, ranks) + assert copies == 36 + + screen = runpy.run_path(str(HERE / "screen.py")) + out = temp / "result" + out.mkdir() + screen["run"](deps, out, screen["time"].monotonic()) + expected_price = read_json((HERE / "PRICE.json").read_bytes()) + actual_price = read_json((out / "PRICE.json").read_bytes()) + assert actual_price == expected_price + stock = read_json((out / "STOCK.json").read_bytes()) + stock.pop("elapsed_seconds") + assert stock == read_json((HERE / "STOCK.json").read_bytes()) + dual = subprocess.run( + [sys.executable, "-E", "-B", str(HERE / "check_stock.py"), + "--deps", str(deps), "--receipt", str(out / "STOCK.json")], + check=True, capture_output=True, text=True, + ) + report = read_json(dual.stdout.splitlines()[0]) + assert report["dual_systems_consistent"] == stock["all_chart_pairs"] == 22190 + return { + **report, "scope_exhausted": stock["scope_exhausted"], + "unresolved_sites": stock["unresolved_sites"], + "savings_upper_whole": stock["optimistic_saving_upper_whole"], + "shortfall_remaining_lower": stock["shortfall_remaining_lower"], + "kappa_gain": "0", + } + + +if __name__ == "__main__": + assert __debug__, "run with assertions enabled" + p = ArgumentParser(description=__doc__) + p.add_argument("--root", type=Path, default=Path.cwd()) + print(json.dumps(run(p.parse_args().root), sort_keys=True)) diff --git a/research/bit-one-chart-donor-envelope/retag.py b/research/bit-one-chart-donor-envelope/retag.py new file mode 100644 index 0000000000..28ea7898d5 --- /dev/null +++ b/research/bit-one-chart-donor-envelope/retag.py @@ -0,0 +1,67 @@ +"""The eight frozen #7001 backup retags from the Round 13 experiment.""" + +import copy + +def touched(event): + return event[1:3] if event[0] in ('ADD', 'SWAP') else event[1:2] + + +def modules(word): + program = word['program'] + selected = [] + edited_indices = set() + for start, (event, next_) in enumerate(zip(program, program[1:])): + if not (event[0] == 'INIT' and next_[0] == 'ADD' and event[1] == next_[1] + and next_[2] < 111 and event[2] == word['start'][next_[2]]): + continue + _, backup, source = event + port = next_[2] + body = start + 2 + while program[body][0] == 'MOVE' and program[body][2:] == [0, source]: + body += 1 + ingress = list(range(start + 2, body)) + roles = {port} | {program[i][1] for i in ingress} + assert len(roles) == len(ingress) + 1 + end_add = body + while program[end_add][0] == 'ADD' and program[end_add][3] == source and set(touched(program[end_add])) <= roles: + end_add += 1 + end = end_add + len(roles) + exits = list(range(end_add, end)) + assert {program[i][1] for i in exits} == roles + assert all(program[i][0] == 'MOVE' and program[i][2] == source for i in exits) + init, copied, late, clear = (i for i in range(start, len(program)) if backup in touched(program[i])) + assert (init, copied) == (start, start + 1) + consumer = program[late][1] + assert program[late - 1:late + 1] == [['MOVE', consumer, 0, source], ['ADD', consumer, backup, source]] + assert program[late + 1][:3] == ['MOVE', consumer, source] + assert program[clear] == ['CLEAR', backup, source] + changes = set(range(start, end)) | {late - 1, late, late + 1, clear} + assert not edited_indices & changes + edited_indices.update(changes) + selected.append({'port': port, 'backup': backup, 'source': source, 'init': start, + 'first_add': body, 'exits': exits, 'ingress': ingress, 'late_add': late, + 'late_consumer': consumer, 'clear': clear}) + if len(selected) == 8: + break + assert [m['port'] for m in selected] == [0, 1, 2, 3, 4, 5, 7, 8] + return selected + + +def retag(word, selected): + changed = copy.deepcopy(word) + program = changed['program'] + drop, adjusted = set(), {} + for m in selected: + port, start, late, clear = (m[k] for k in ('port', 'init', 'late_add', 'clear')) + changed['start'][port] = 0 + program[start][-1] = program[start + 1][-1] = program[clear][-1] = 0 + for j in range(m['first_add'], m['exits'][0]): + program[j][-1] = 0 + for j in (*m['exits'], late + 1): + program[j][2] = 0 + adjusted[j] = port + program[late][-1] = 0 + drop.update([*m['ingress'], late - 1]) + origin = [i for i in range(len(program)) if i not in drop] + changed['program'] = [program[i] for i in origin] + return changed, origin, adjusted, sorted(drop) diff --git a/research/bit-one-chart-donor-envelope/screen.py b/research/bit-one-chart-donor-envelope/screen.py new file mode 100644 index 0000000000..9d4b6a035b --- /dev/null +++ b/research/bit-one-chart-donor-envelope/screen.py @@ -0,0 +1,185 @@ +"""Single retained chart lower-price screen for the fixed-volume BIT contract.""" + +import argparse +from fractions import Fraction +from functools import cache +import gzip +import hashlib +import json +from pathlib import Path +import runpy +import time + +PINS = { + "deps/inputs/WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "deps/inputs/INVOICE.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "deps/price.py": "6a33aac4c7032de9bb3881da248f5371b69c6b9af0893220825727f3d4878fae", + "screen/pr7200_verify.py": "90f23e033bfced9673da33c07123eb749493164d5557f372a16b674e45461e1f", + "screen/retag.py": "cf9b4fbe12225f3c258648d3e49660111976523babfa788dd09a267d9e7b904b", + "screen/CERT.json": "36e221ac20102e40f0e419444d85b588278d3bdcd0e4c212bb2d907844811186", +} + + +def authenticated(roots): + for key, digest in PINS.items(): + prefix, relative = key.split("/", 1) + path = roots[prefix] / relative + if hashlib.sha256(path.read_bytes()).hexdigest() != digest: + raise ValueError(f"changed input {key}") + + +def gf2_basis(rows): + basis = {} + for row in rows: + while row: + pivot = row.bit_length() + if pivot not in basis: + basis[pivot] = row + break + row ^= basis[pivot] + return basis + + +def contains(basis, row): + while row: + pivot = row.bit_length() + if pivot not in basis: + return False + row ^= basis[pivot] + return True + + +def interval_string(interval): + return [str(n) for n in interval] + + +def save(out, filename, payload): + path = out / filename + temporary = path.with_suffix(".tmp") + temporary.write_text(json.dumps(payload, indent=2, sort_keys=True) + "\n") + temporary.replace(path) + + +def run(deps, out, start): + screen = Path(__file__).resolve().parent + authenticated({"deps": deps, "screen": screen}) + src = runpy.run_path(str(screen / "pr7200_verify.py")) + rewrite = runpy.run_path(str(screen / "retag.py")) + price = runpy.run_path(str(deps / "price.py")) + word = json.loads(gzip.decompress((deps / "inputs" / "WORD.json.gz").read_bytes())) + invoice = json.loads((deps / "inputs" / "INVOICE.json").read_bytes()) + frames, ranks, canonical = src["geometry"](word) + changed, origin, adjusted, _ = rewrite["retag"](word, rewrite["modules"](word)) + old, _, _ = src["trace"](word, range(len(word["program"])), {}, frames, ranks, canonical) + new, sites, available = src["trace"](changed, origin, adjusted, frames, ranks, canonical) + assert old == {int(rank): n for rank, n in invoice["native_paid"].items()} + assert len(sites) == len(adjusted) == 35 + delta = {r: new[r] - old[r] for r in new.keys() | old.keys() if new[r] != old[r]} + assert delta == {1: -48, 2: 21, 3: -6, 4: 6, 6: -8, 7: 8} + target = Fraction(price["TARGET"]) + h = {0: (Fraction(0), Fraction(0))} + h.update({r: price["power_bounds"](r, target) for r in range(1, 9)}) + paid = {int(r): n for r, n in invoice["paid"].items()} + targets = {int(r): n for r, n in invoice["targets"].items()} + p_lo, p_hi = price["cost"](paid, target) + t_lo, t_hi = price["cost"](targets, target) + d_lo, d_hi = price["cost"](delta, target) + shortfall = (p_lo - t_hi + 18*d_lo - 111, p_hi - t_lo + 18*d_hi - 111) + assert shortfall[0] > 0 + initial = { + "inputs": PINS, "target": str(target), "old_native": dict(old), + "retag_delta": delta, "changed_calls": 18, "formal_H1_credit": 111, + "raw_baseline_paid_minus_targets": interval_string((p_lo-t_hi, p_hi-t_lo)), + "retag_cost_per_call": interval_string((d_lo, d_hi)), + "saving_needed_whole": interval_string(shortfall), + "saving_needed_per_changed_call": interval_string(tuple(x/18 for x in shortfall)), + "zero_price_for_all_35_adjusted_moves_stock_upper_per_call": + str(sum(h[ranks[site["target_chart"]]][1] for site in sites)), + "scope": "one distinct positive retained canonical donor chart per delivery, fixed field volume", + } + save(out, "PRICE.json", initial) + control = src["support_check"](sites, available, frames, ranks, canonical, + json.loads((screen / "CERT.json").read_text())) + assert control == {"empty": 79, "explicit": 512, "aggregate_cases": 382, "aggregate_recipients": 24} + assert contains(gf2_basis([3, 6]), 5) + assert not contains(gf2_basis([3, 6]), 4) + # A simple nonnested pair. The rank of P-Q is 2 although their ranks coincide. + x, y = (1, 0), (1, 1) + assert 2*len(src["eliminate"]((x, y))) - 2 == 2 + # A charge that mistakenly uses the absolute rank difference admits this pair for free. + assert abs(len((x,)) - len((y,))) == 0 + + @cache + def basis(chart, due): + return gf2_basis(row for row, first in available[chart].items() if first <= due) + + @cache + def distance(chart, other): + union = src["eliminate"](frames[chart][0] + frames[other][0]) + return 2*len(union) - ranks[chart] - ranks[other] + + donors = sorted({chart for chart in canonical.values() if ranks[chart]}) + # Candidate stock is rounded upward per site. Costs of forming, routing and + # cleaning donors are credited zero only in this optimistic upper bound. + records = [] + for site in sites: + if time.monotonic() - start >= 114: + break + target_chart, target_row, due = (site[k] for k in ("target_chart", "target_row", "due")) + baseline_rank = ranks[target_chart] + chart_count = support_count = nonnested_count = cheaper_count = 0 + cheaper = [] + for chart in donors: + if chart == target_chart: + continue + chart_count += 1 + if not contains(basis(chart, due), target_row): + continue + support_count += 1 + low_rank = distance(chart, target_chart) + nonnested_count += low_rank > abs(ranks[chart] - baseline_rank) + if low_rank < baseline_rank: + cheaper_count += 1 + cheaper.append((low_rank, chart)) + best = min(cheaper, default=None) + optimistic = Fraction(0) if best is None else h[baseline_rank][1] - h[best[0]][0] + records.append({ + "event": site["event"], "target_chart": target_chart, "due": due, "old_rank": baseline_rank, + "chart_count": chart_count, "support_count": support_count, "nonnested_support": nonnested_count, + "cheaper_count": cheaper_count, "cheaper": cheaper, + "saving_upper": str(optimistic), + }) + complete = len(records) == len(sites) + upper = sum(Fraction(row["saving_upper"]) for row in records) + sum( + h[ranks[site["target_chart"]]][1] for site in sites[len(records):] + ) + receipt = { + **initial, "predecessor_control": control, "positive_declared_charts": len(donors), + "positive_observed_charts": sum(bool(available[chart]) for chart in donors), + "scope_exhausted": complete, "unresolved_sites": len(sites) - len(records), + "all_chart_pairs": sum(r["chart_count"] for r in records), + "span_pairs": sum(r["support_count"] for r in records), + "nonnested_span_pairs": sum(r["nonnested_support"] for r in records), + "lower_price_pairs": sum(r["cheaper_count"] for r in records), + "optimistic_saving_upper_per_call": str(upper), + "optimistic_saving_upper_whole": str(18*upper), + "shortfall_remaining_lower": str(shortfall[0] - 18*upper), + "formation_routing_ownership_restoration": "granted free in upper, nonnegative when charged", + "schedule": "grants independent donor availability through next target contact, no interference", + "decision": "PIVOT" if 18*upper < shortfall[0] else "UNRESOLVED", + "sites": records, + "elapsed_seconds": time.monotonic() - start, + } + save(out, "STOCK.json", receipt) + print(json.dumps({k: v for k, v in receipt.items() if k != "sites"}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + if not __debug__: + raise RuntimeError("Run with assertions enabled") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--deps", type=Path, required=True) + parser.add_argument("--out", type=Path, required=True) + args = parser.parse_args() + args.out.mkdir(parents=True, exist_ok=True) + run(args.deps.resolve(), args.out.resolve(), time.monotonic())