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). 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") diff --git a/research/p104-changed-public-move-contraction-bound/LOCAL-PINS.json b/research/p104-changed-public-move-contraction-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..dad253e41f --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/LOCAL-PINS.json @@ -0,0 +1,28 @@ +{ + "NOTICE": "a84f4da6ce5218b08ba25ac8da9cf82575a197fc760f7f2f0f973769d608a6a8", + "PROOF.md": "3d0ed14b5a0a26ecdb17cea1cbb1eb8116d356616daf83a50cd4dce347119f04", + "PROVENANCE.json": "e49345e2387cd61e4041b388624a7a0300b1097dffb3e7ed75d62a3cabc50a05", + "README.md": "e49a6b27565b0d56c448b7a2975608449c69f2182294e7ab0bda783bc7d6ddf9", + "SOURCES.json": "5ae4cfc96aa890b1b06aa0de688e03d9713b2772fb0f9c6ae7e23ad7d49c479d", + "TASK.json": "2fe77d7cb096614a2cda9c6901e233559780b9a40737d74c6667f48045740e99", + "VERIFICATION.md": "c92e71e2dd186c692bdd1cfed39f361666e9d07af9322e68ef91887cfcda92ef", + "VERIFY.json": "bc07f69895abb5a6b727f294adcf6f0db1874216017d421b91dcd42985cd3630", + "engines/r100/geometry.py": "29af034fab238533905d6c5fc57b5e8af29234495edf2afaaacdfe2c5400b5b0", + "engines/r100/quote.py": "184481178657cf4a78479f3f75bcded934494fa7428b8ad58629b7561d6336b4", + "engines/r100/reverse_contacts.py": "0819e0811ffec51a398f768e7655462ec28c7892b8f6f57c21f95b5f938e9da0", + "engines/r101/quote.py": "fbdb7c51bceefcd09aef3c466b02b291bc77f4c36c16766350a561b961d2baac", + "engines/r101/reverse_donors.py": "3bbcc821a4d4b2725354a9c4681f934d9f6fc0cd294366d208697e5a7070a313", + "engines/r101/reverse_span.py": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", + "engines/r101/support.py": "ce109dcfbfdb9c2e169563e4fba98997bb9a3bce87c780cba276aa8ece917c32", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/BENCHMARK.json": "004331cff6ca8644489d7b7084e5c67439d74a2d283e4d64a9fdb9f88679253d", + "inputs/PR7362-SHA256.json": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "inputs/R92-PRICE.json.gz": "2274f514fb12f9ced0c24abe0c02a76c16cfee4c61f909e37a5ad89b07852371", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "receipts/SEPARATORS.json": "a089841b83b6bd6cfa51da7ccb6968955ffe9e4e44ff0871b3e987ced1a6fe1b", + "receipts/SHA256.json": "f8418b2b07e4ecb6d49d8839015e9ceab2224816d7863edd59cb03f29de34566", + "replay.py": "11b85da8dff797281f4a63caab99e9ee84ba6d625f77c46ba24b43f7905bc4f0" +} diff --git a/research/p104-changed-public-move-contraction-bound/NOTICE b/research/p104-changed-public-move-contraction-bound/NOTICE new file mode 100644 index 0000000000..02bfe663f9 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. + +#7334 and #7113 supply the word and signed caller. #7339 supplies changed-block +roles. #7312, #7336 and #7338 are contact and compensated fusion precedents. +#7355 supplies the donor-span method, and #7298 and #7362 supply directed price +and rank-stock provenance. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-changed-public-move-contraction-bound/PROOF.md b/research/p104-changed-public-move-contraction-bound/PROOF.md new file mode 100644 index 0000000000..41916cac3f --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/PROOF.md @@ -0,0 +1,19 @@ +# Exact scope and price + +For a public role with strictly ascending consecutive paid MOVEs A→B→C, an empty contact interval allows a prospective A→C contraction. A nonzero unary SCALE in the interval may retain its clock on A. In normalized coordinates scalar multiplication commutes with the chart transports. The signed physical construction would also have to prove the chart identity and its adjoint, preserve chart and ownership restoration, and meet the full compiler, precision and tape contracts. A binary source or destination contact prevents this literal contraction under the fixed-contact rule. + +A reverse chart walk verifies every event and independently builds chronological incidence lists. The 14 public role IDs are authenticated by the #7334 changed-block receipt. Their 51 paid MOVEs give 37 consecutive pairs. All pairs contain an ADD, with 33 source incidences, 32 destination incidences and two SCALE incidences. The predecessor #7312 recorded 38 such windows with an ADD on these IDs on #7277. The current word has one fewer window on role 319. The conclusion for #7334 uses the fresh literal replay. + +## Donor relaxation + +Freeze only the six windows with one contact, a nonzero ADD into the mover at chart B different from 207. The prospective direct MOVE executes at the old entrance or exit, so at the original ADD clock the mover is on C or A respectively. It has no other contact within the window. Keeping the other original paths fixes every donor's row at that cut. This statement uses arbitrary initial public input, including the coordinates unrelated to the moving role. + +If the original source has normalized row s and scalar α≠0, a replacement from the same-clock public donor rows dⱼ requires that the sum of βⱼdⱼ equals αs. Every tested pair has a coordinate i with sᵢ≠0 and zero i-th coefficient for every donor. The i-th coordinate is therefore an exact separating covector. The six shared coordinates for both endpoint banks are 648, 28, 29, 27, 2 and 13 with original-source coefficients −1, 1, 1, −1/2, 1/4 and −1/2 respectively, before multiplying by α. The reverse covector engine computes signed rational prefix rows and the forward engine independently checks each full rational bank. + +## Complete invoice + +On the exact signed 17-copy invoice, replacing paid ranks p and q by p+q removes 17 paid positions and preserves every productive position and signed rank mass. The literal comparator has 110,519 paid positions, 22,461 productive positions and rank surplus 1,424. The prospective bill has 110,502 paid positions. It uses the existing endpoint charts and allows no auxiliary paid call. + +The predecode optimistic single-edit upper is 0.380712103178622 raw on the 20 rank profiles. At most four disjoint pairs per role across the 14 roles gives the relaxed whole upper 21.31987777800283 raw at the comparator and a fixed-target complete margin upper of approximately −116.35274417830618. For the six frozen donor windows, at most one pair per each of four roles may be credited because the two windows for role 198 share one MOVE and the two for role 532 share one MOVE. The respective one-edit and whole upper bounds are 0.294636248924991 and 0.914203210927566 raw. The complete fixed-target margin upper is approximately −138.76276984112278. All ceilings grant ancillary work free. One additional paid rank-one position would erase any one-edit credit. Exact support leaves zero verified savings. + +The binding complex crossing and inherited assumptions stay those of #7334. The comparator retains `native_all_columns`, `owned_erasure`, `compiler`, `precision_tape` and `analytic_recovery`. This contribution changes neither the selected record nor the strongest independently reproduced comparator. diff --git a/research/p104-changed-public-move-contraction-bound/PROVENANCE.json b/research/p104-changed-public-move-contraction-bound/PROVENANCE.json new file mode 100644 index 0000000000..3640aca6c5 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/PROVENANCE.json @@ -0,0 +1,69 @@ +{ + "derived_inputs": { + "inputs/BENCHMARK.json": { + "receipt": "inputs/ADMITTED.json", + "relationship": "Exact admission SHA, head, and crossing checked at replay" + }, + "inputs/R92-PRICE.json.gz": { + "compression": "gzip", + "key": "R92-PRICE.json", + "receipt": "inputs/PR7362-SHA256.json" + } + }, + "files": { + "engines/r101/reverse_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "5efbeac87e3963085149244304614844307c8034", + "path": "research/p104-owned-add-source-span-bound/engines/reverse.py", + "sha256": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/reverse.py" + }, + "inputs/7334-CHANGED.json": { + "commit": "4b958b057e133e92a5c3a07f1fb489c626dc2525", + "git_blob": "b1644106d97cdadfabb729dd4625adb4a77c20a0", + "path": "research/p104-retimed-chart207-split-bound/inputs/IDENTITIES.json", + "sha256": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/4b958b057e133e92a5c3a07f1fb489c626dc2525/research/p104-retimed-chart207-split-bound/inputs/IDENTITIES.json", + "uncompress": false + }, + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "inputs/PR7362-SHA256.json": { + "commit": "5eec7ed633dcf9b9bbc95552aa653da296f863fb", + "git_blob": "b1486e0b5cfe4535f381ed26f7bce4aee21d8a43", + "path": "research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json", + "sha256": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/5eec7ed633dcf9b9bbc95552aa653da296f863fb/research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json" + }, + "inputs/donor_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "46e4621b69bba513f327de53153298e7f4ca0645", + "path": "research/p104-owned-add-source-span-bound/engines/forward.py", + "sha256": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/forward.py" + }, + "inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-changed-public-move-contraction-bound/README.md b/research/p104-changed-public-move-contraction-bound/README.md new file mode 100644 index 0000000000..fceed4b8cc --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/README.md @@ -0,0 +1,25 @@ +# Changed-public MOVE contraction bound + +**NO VERIFIED GAIN.** The verified gain is Δκ = 0, exactly 0% relative to conditional κ = 0.00364665195644 on exact #7334 `aaeec8c0acf01e99a5f331ef363a698d9c084ace` and signed #7113 `07a76c5e2738882c0cb322278e56f6cae3c9885d`. Two exact screens rule out a paid MOVE contraction on the declared public roles under their tested contact contracts. + +The literal full-word census covers all 37 consecutive paid ascending MOVE windows on the 14 changed-block public roles. Every interval has an ADD contact, including reads of the mover. The two engines agree on all 67 signed contacts. The contact-free and SCALE-only scopes each have zero candidates and zero unresolved windows. + +The narrower donor relaxation keeps the old ADD clock in six windows where it is the mover's only intervening contact, the mover is its destination, and the middle chart differs from 207. At each of the two endpoint charts, the source row has a nonzero public input coordinate absent from every eligible donor row. The exact [12 separators](receipts/SEPARATORS.json) rule out arbitrary rational public-donor combinations at those fixed clocks. Both engines agree on all bank membership, source support sizes, donor ranks and dispositions. Three endpoint banks at chart 207 are empty. The one owned occupant at a chart-120 bank remains outside the donor basis. + +## Reproduce + +Use CPython 3.12 with assertions and the standard library. From this package in a clean checkout or Git-free export: + +```sh +python3.12 -I -B replay.py +``` + +Use `--output replayed` to retain the [eight regenerated receipts](receipts/SHA256.json), including literal contact bytes and exact sparse source and donor rows. [Proof and price](PROOF.md) · [Verification](VERIFICATION.md) · [Pinned provenance](PROVENANCE.json) + +## Open next questions + +Start from a [separating coordinate](receipts/SEPARATORS.json) and specify what new source mechanism could supply it. Price all compatible edits before changing the bank or clock. The donor relaxation covers six of the 37 current windows. The other 31, middles on chart 207, roles outside the frozen 14, owned replacement donors, multiple binary contacts, source-side edits and different ADD clocks remain outside its scope. A signed native and complete caller replay would still be required for any candidate. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) and [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) supply the exact comparator and signed caller. [#7339](https://github.com/CrocSwap/integer-mult-bounds/pull/7339) supplies the changed-block role record. [#7312](https://github.com/CrocSwap/integer-mult-bounds/pull/7312) supplies the #7277 contact census and predecessor fusion gates. [#7336](https://github.com/CrocSwap/integer-mult-bounds/pull/7336) and [#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) supply related compensated fusion evidence. [#7355](https://github.com/CrocSwap/integer-mult-bounds/pull/7355) supplies the exact two-engine donor method for owned movers. [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) and [#7362](https://github.com/CrocSwap/integer-mult-bounds/pull/7362) supply directed price and the pinned rank-stock receipt. OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-changed-public-move-contraction-bound/SOURCES.json b/research/p104-changed-public-move-contraction-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ], + "schema_version": 1 +} diff --git a/research/p104-changed-public-move-contraction-bound/TASK.json b/research/p104-changed-public-move-contraction-bound/TASK.json new file mode 100644 index 0000000000..2e1073eb78 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334 one-pair public MOVE contraction over the 14 changed-block roles, with a fixed-clock public donor span relaxation for six frozen sole ADD destination cases.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 public MOVE contraction research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Replacing two paid ascending children by one would improve the complete complex bill if all binary contacts are absent or exactly supplied at their old clock.", + "budget_minutes": 20, + "evidence": "The two literal scans agree on all 37 consecutive MOVE windows. Each has an ADD barrier. Twelve endpoint donor banks for six frozen sole ADD destination windows have exact one-coordinate separators, independently verified.", + "open_questions": [ + { + "blocked_by": "The listed public donor banks lack an essential independent input coordinate. Owned donor changes, moved ADD clocks and additional paid routes require separate proofs and charges.", + "first_step": "Start from receipts/SEPARATORS.json. Choose one different source mechanism for a listed missing coordinate and bound the whole compatible invoice before extending the scope.", + "question": "Can a changed binary-contact contract support a legal paid contraction?", + "why_it_matters": "The complete invoice allows a small saving if all original binary responses are retained with no extra paid child." + } + ], + "original_card": { + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4133: literal-slot defect", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4136: uniform commutation gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4140: uniform encoding gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "status": "author-checked" + }, + { + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "status": "author-checked" + }, + { + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4154: fiber-tag seam mismatch", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "status": "author-checked" + }, + { + "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": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "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": "p104-side-correction", + "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": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "New literal current-word contact scope on 14 certified public changed-block roles and exact same-clock donor banks. Earlier #7312 uses #7277; #7355 treats owned movers.", + "scope_status": "changed", + "stop_rule": "Exhaust 76,466 native events and at most 112 consecutive windows in 20 seconds. Test at most 12 fixed donor banks in 20 seconds. A native build requires an exact support survivor.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-changed-public-move-contraction-bound/VERIFICATION.md b/research/p104-changed-public-move-contraction-bound/VERIFICATION.md new file mode 100644 index 0000000000..b212b40c25 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/VERIFICATION.md @@ -0,0 +1,5 @@ +# Verification + +The clean CPython 3.12 replay regenerates eight SHA-256-pinned receipts, checks exact agreement at every window and bank, verifies each separating coordinate against the full independent sparse rows, and rejects corrupted price and word inputs. The 76,466-event and 112-pair contact cap completed with 37 cases in the independent 0.10-second run. The 12-case rational cap completed in 0.20 seconds. Both run under 20-second limits. + +The original and relocated independent outputs are byte-identical. Toy controls exercise signed unary SCALE, empty intervals, ADD and COPY source barriers, GF(2) nesting, a signed rational donor solution and a separating coordinate. No changed supplier or complete outer replay was required because both support gates exhausted with no candidate. The full comparable #7334 admission and its [hosted replay](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43114736518) are predecessor evidence. diff --git a/research/p104-changed-public-move-contraction-bound/VERIFY.json b/research/p104-changed-public-move-contraction-bound/VERIFY.json new file mode 100644 index 0000000000..9ec8d000dd --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Rebuild both exact prices, both paired independent native screens, eight pinned receipts, twelve separating coordinates and mutated input rejection.", + "timeout_seconds": 120 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-changed-public-move-contraction-bound/engines/r100/geometry.py b/research/p104-changed-public-move-contraction-bound/engines/r100/geometry.py new file mode 100644 index 0000000000..fab9a9cad2 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/engines/r100/geometry.py @@ -0,0 +1,147 @@ +"""Census consecutive paid MOVE pairs on the exact changed public roles.""" +from collections import Counter +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "lead/PRICE.json": "7109125bbf60e3015c8c0ac7b10b24b7de61f358c1508d06604ebccd89ef6343", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} + + +def unique(pairs): + result = dict(pairs) + if len(result)!=len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def checked(path): + raw = (ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def space(frame): + vals = {0} + for v in frame: + assert v not in vals + vals.update(v^a for a in tuple(vals)) + return frozenset(vals) + + +def touches(event): + op,r,*args = event + return (r,args[0]) if op in ("ADD","COPY") else (r,) + + +def disposition(contacts): + if any(e[0]!="SCALE" for _,e in contacts): + return "binary barrier" + return "scales only" if contacts else "contact free" + + +def controls(): + assert touches(["ADD",1,2,"-5",4]) == (1,2) + assert touches(["COPY",5,2,"3/2",4]) == (5,2) + assert disposition([(2,["SCALE",1,"-5",4])]) == "scales only" + assert disposition([(2,["ADD",2,1,"-5",4])]) == "binary barrier" + assert disposition([]) == "contact free" + return ["source-only ADD barrier","source-only COPY barrier","nonzero unary SCALE","contact-free"] + + +def stopped(*_): + raise TimeoutError("hard runner cap") + + +def main(): + assert __debug__ + price = json.loads(checked("lead/PRICE.json"),object_pairs_hook=unique) + caps = price["limits"] + signal(SIGALRM,stopped) + alarm(caps["runner_seconds"]) + deadline = monotonic()+18 + pairs = [] + moves = Counter() + tail = None + reason = None + try: + raw = decompress(checked("inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest()==price["word_payload_sha256"] + word = json.loads(raw,object_pairs_hook=unique) + n = word["public"] + program = word["program"] + assert len(program)==caps["event_cap"] and n==1501 + roles = set(price["roles"]) + assert len(roles)==14 and max(roles)=deadline: + raise TimeoutError("cooperative runner cap") + op,d,*a = event + current = state[d] + if op=="MOVE": + before,after,owned = a + assert before==current and owned==(d>=n) + assert spans[before]=caps["paid_pairs"]: + raise TimeoutError("paid pair cap") + earlier,old,contacts = pending[d] + assert old[3]==before + start = old[2] + p,q = ranks[before]-ranks[start],ranks[after]-ranks[before] + assert p>0 and q>0 and spans[start]=n + state[d]=a[0] + elif op=="CLEAR": + assert current==a[0] and d>=n + state[d]=None + else: + assert current==a[-1] and op in ("ADD","COPY","SCALE") and Fraction(a[-2]) + if op in ("ADD","COPY"): + assert state[a[0]]==current and a[0]!=d + for r in touches(event): + if r in pending: + pending[r][2].append([t,event]) + assert state==word["final"]+[None]*word["owned_fields"] + assert all(c<=9 for c in moves.values()) + assert len(pairs)==sum(c-1 for c in moves.values()) + tail = None + except TimeoutError as exc: + reason = str(exc) + finally: + alarm(0) + eligible=sorted((r for r in pairs if r["status"]!="binary barrier"), + key=lambda r:(-Fraction(r["net"][0]),r["key"])) + out = {"head":price["head"],"pins":PINS,"controls":controls(),"caps":caps,"moves":moves,"pairs":pairs, + "counts":Counter(r["status"] for r in pairs),"candidate_keys":[r["key"] for r in eligible], + "first_unvisited_event":tail,"timeout":reason} + print(json.dumps(out,indent=2,sort_keys=True)) + if reason: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-changed-public-move-contraction-bound/engines/r100/quote.py b/research/p104-changed-public-move-contraction-bound/engines/r100/quote.py new file mode 100644 index 0000000000..7230cf7cb2 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/engines/r100/quote.py @@ -0,0 +1,90 @@ +"""Exact complete price of a public monotone paid MOVE contraction.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/BENCHMARK.json": "004331cff6ca8644489d7b7084e5c67439d74a2d283e4d64a9fdb9f88679253d", + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", +} + + +def unique(pairs): + result = dict(pairs) + if len(result)!=len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def hist(x): + return Counter({int(k):v for k,v in x.items()}) + + +def interval(x): + return list(map(str,x)) + + +def main(): + docs = {} + for path,pin in PINS.items(): + data = (ROOT/path).read_bytes() + if sha256(data).hexdigest()!=pin: + raise ValueError(f"changed dependency {path}") + if path.endswith(".json"): + docs[path] = json.loads(data,object_pairs_hook=unique) + bench,prior,changed = docs.values() + assert bench["head"] == prior["head"] and len(changed["roles"])==14 + assert changed["word_sha256"][-1]=="9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + assert bench["status"]=="exact-complete-receipt-reused" + targets,paid = hist(prior["old_targets"]),hist(prior["old_paid"]) + assert sum(targets.values())==22461 and sum(paid.values())==110519 + old = targets.copy() + old.subtract(paid) + assert sum(r*n for r,n in old.items())==1424 + cost = run_path(str(ROOT/"inputs/pricing.py"))["cost"] + at = Q(prior["old_crossing_upper"]) + probe = Q(prior["probe"]) + bit = Q(prior["retained_bit_premise"]) + target = Q(prior["moonshot"]) + assert at == Q(bench["crossing"][1]) and at < probe < bit < target + profiles=[] + for p in range(1,9): + for q in range(p,10-p): + change=Counter((p,q)) + change.subtract((p+q,)) + change=Counter({r:17*n for r,n in change.items()}) + new=old.copy() + new.update(change) + assert sum(r*n for r,n in new.items())==1424 + full_probe=cost(new,probe) + assert full_probe[0]>0 + profiles.append({"ranks":[p,q,p+q],"paid_delta":{r:-n for r,n in change.items()}, + "net":interval(cost(change,at)),"full_probe":interval(full_probe), + "net_target":interval(cost(change,target)), + "extra_rank_one_upper":str(cost(new,at)[1]-1)}) + assert len(profiles)==20 + # Every public MOVE is strict ascending within rank 0..9. Each of the 14 + # roles can have at most 9 MOVEs and thus at most four disjoint pairs. + stock=len(changed["roles"])*(9//2) + max_net=max(Q(x["net"][1]) for x in profiles) + max_target=max(Q(x["net_target"][1]) for x in profiles) + out={"head":bench["head"],"kappa":bench["kappa"],"caller_head":prior["caller_head"], + "pins":PINS,"word_sha256":prior["word_sha256"],"word_payload_sha256":changed["word_sha256"][-1], + "roles":changed["roles"],"old_crossing_upper":str(at),"probe":str(probe), + "fixed_target":str(target),"bit_premise":str(bit),"full_paid_before":110519,"full_paid_after":110502, + "productive_positions":22461,"rank_surplus":1424,"profiles":profiles, + "distinct_compatible_cap":stock,"one_net_upper":str(max_net), + "whole_net_upper":str(stock*max_net),"whole_target_margin_upper":str(cost(old,target)[1]+stock*max_target), + "limits":{"event_cap":76466,"runner_seconds":20,"paid_pairs":112,"builds":1,"prototype_seconds":120}} + print(json.dumps(out,indent=2,sort_keys=True)) + + +if __name__=="__main__": + assert __debug__ + main() diff --git a/research/p104-changed-public-move-contraction-bound/engines/r100/reverse_contacts.py b/research/p104-changed-public-move-contraction-bound/engines/r100/reverse_contacts.py new file mode 100644 index 0000000000..2392c8fe69 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/engines/r100/reverse_contacts.py @@ -0,0 +1,259 @@ +"""Verify the frozen R100 public MOVE windows by reverse indexed incidence.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from itertools import pairwise +from json import dumps, loads +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "7109125bbf60e3015c8c0ac7b10b24b7de61f358c1508d06604ebccd89ef6343", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +PRIMARY = "075301daf545c8021800c36af19d05517e3c4136dac4e2114cb85204d0b31c64" +EVENT_CAP = 76466 +PAIR_CAP = 112 +SECONDS = 20 + + +def unique(pairs): + data = dict(pairs) + if len(data) != len(pairs): + raise ValueError("Duplicate JSON key") + return data + + +def authenticate(path, pin): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"Changed input {path.name}") + return raw + + +def read_input(root, rel): + data = authenticate(root / rel, PINS[rel]) + if rel.endswith(".gz"): + data = decompress(data) + assert sha256(data).hexdigest() == PAYLOAD + return loads(data, object_pairs_hook=unique) + + +def participants(event): + op, dst, *args = event + if op in ("COPY", "ADD"): + return ((dst, "destination"), (args[0], "source")) + return ((dst, "unary"),) + + +def disposition(rows): + if not rows: + return "contact free" + if all(row["event"][0] == "SCALE" for row in rows): + return "scales only" + assert any(row["event"][0] in ("ADD", "COPY") for row in rows) + return "binary barrier" + + +def span_index(frames): + @cache + def span(label): + values = [0] + seen = 1 + for v in frames[label]: + assert type(v) is int and 0 < v < 512 and not (seen >> v & 1) + layer = [u ^ v for u in values] + values.extend(layer) + seen |= sum(1 << u for u in layer) + return seen + return span + + +def strict_subset(a, b): + return a != b and a & b == a + + +@cache +def signed_scalar(literal): + value = Fraction(literal) + assert value + return value + + +def controls(): + add = ["ADD", 1, 0, "-5", 4] + copy = ["COPY", 5, 0, "3/2", 4] + scale = ["SCALE", 0, "-5/2", 4] + assert participants(add)[1] == participants(copy)[1] == (0, "source") + assert disposition([{"event": e} for e in (scale, add)]) == "binary barrier" + assert disposition([{"event": copy}]) == "binary barrier" + assert signed_scalar(scale[-2]) == Fraction(-5, 2) + assert disposition([{"event": scale}]) == "scales only" + assert disposition([]) == "contact free" + span = span_index([[1], [1, 2], [1, 2, 4], [1, 4]]) + assert strict_subset(span(0), span(1)) and strict_subset(span(1), span(2)) + assert not strict_subset(span(1), span(3)) + return ["source ADD", "source COPY", "signed SCALE", "empty interval", "strict GF2 nesting"] + + +def reverse_index(word, roles, span, deadline, result): + n = word["public"] + owned = word["owned_fields"] + program = word["program"] + assert (n, owned, len(program)) == (1501, 68, EVENT_CAP) + charts = word["final"] + [None] * owned + incidence = {role: [] for role in sorted(roles)} + must_be_fresh = set() + for t in range(EVENT_CAP - 1, -1, -1): + result["last_unvisited_clock"] = t + if t % 128 == 0 and monotonic() >= deadline: + raise TimeoutError("reverse literal cap") + event = program[t] + op, d, *args = event + assert 0 <= d < len(charts) and (d not in must_be_fresh or op == "INIT") + if op == "MOVE": + low, high, is_owned = args + assert charts[d] == high and type(is_owned) is bool and is_owned == (d >= n) + assert strict_subset(span(low), span(high)) or is_owned and strict_subset(span(high), span(low)) + charts[d] = low + elif op == "INIT": + assert d >= n and charts[d] == args[0] + must_be_fresh.discard(d) + charts[d] = None + elif op == "CLEAR": + assert d >= n and charts[d] is None + charts[d] = args[0] + else: + assert op in ("ADD", "COPY", "SCALE") and charts[d] == args[-1] + signed_scalar(args[-2]) + if op != "SCALE": + src = args[0] + assert 0 <= src < len(charts) and src != d and charts[src] == args[-1] + if op == "COPY": + assert d >= n + must_be_fresh.add(d) + for role, access in participants(event): + if role in incidence: + incidence[role].append((t, access)) + result["events_checked"] += 1 + assert charts == word["initial"] + [None] * owned and not must_be_fresh + result["last_unvisited_clock"] = None + return {role: list(reversed(rows)) for role, rows in incidence.items()} + + +def windows(word, price, span, incidence, deadline, result): + tape = word["program"] + profiles = {tuple(row["ranks"]): row for row in price["profiles"]} + assert len(profiles) == 20 + frames = word["frames"] + pending = [] + for role, events in incidence.items(): + moves = [i for i, (t, _) in enumerate(events) if tape[t][0] == "MOVE"] + assert len(moves) <= 9 + result["moves"][role] = len(moves) + for left, right in pairwise(moves): + pending.append((role, events[left][0], events[right][0], events[left+1:right])) + pending.sort(key=lambda case: (case[2], case[0], case[1])) + result["unvisited_pair_keys"] = [[first, second, role] for role, first, second, _ in pending] + for i, (role, first, second, inside) in enumerate(pending): + if i == PAIR_CAP or monotonic() >= deadline: + raise TimeoutError("pair or cooperative cap") + op, old_role, a, b, old_flag = tape[first] + op2, new_role, mid, c, new_flag = tape[second] + assert op == op2 == "MOVE" and old_role == new_role == role and not old_flag and not new_flag + assert b == mid and strict_subset(span(a), span(b)) and strict_subset(span(b), span(c)) + p, q = len(frames[b]) - len(frames[a]), len(frames[c]) - len(frames[b]) + assert p > 0 and q > 0 and p + q == len(frames[c]) - len(frames[a]) + contacts = [dict(clock=t, event=tape[t], access=access) for t, access in inside] + assert all(row["event"][-1] == b for row in contacts) + quote = profiles[(*sorted((p, q)), p+q)] + assert Fraction(quote["full_probe"][0]) > 0 + result["pairs"].append(dict(key=[first, second, role], charts=[a,b,c], + ranks=[p,q,p+q], contacts=contacts, status=disposition(contacts), + full_probe=quote["full_probe"], net=quote["net"])) + del result["unvisited_pair_keys"][0] + + +def audit(root): + result = dict(events_checked=0, last_unvisited_clock=EVENT_CAP-1, + unvisited_pair_keys=None, moves={}, pairs=[]) + reason = None + + def stop(*_): + raise TimeoutError("Hard 20-second cap") + + signal(SIGALRM, stop) + alarm(SECONDS) + deadline = monotonic() + SECONDS - 2 + try: + price = read_input(root, "inputs/PRICE.json") + changed = read_input(root, "inputs/7334-CHANGED.json") + assert price["head"] == HEAD and price["caller_head"] == CALLER + assert price["word_sha256"] == PINS["inputs/7334-WORD.json.gz"] + assert price["word_payload_sha256"] == changed["word_sha256"][1] == PAYLOAD + assert price["limits"]["event_cap"] == EVENT_CAP and price["limits"]["paid_pairs"] == PAIR_CAP + assert price["limits"]["runner_seconds"] == SECONDS + roles = set(changed["roles"]) + assert price["roles"] == changed["roles"] and len(roles) == 14 and max(roles) < 1501 + word = read_input(root, "inputs/7334-WORD.json.gz") + span = span_index(word["frames"]) + incidence = reverse_index(word, roles, span, deadline, result) + windows(word, price, span, incidence, deadline, result) + except TimeoutError as exc: + reason = str(exc) + finally: + alarm(0) + cases = result["pairs"] + return dict(head=HEAD, caller_head=CALLER, pins=PINS, event_cap=EVENT_CAP, pair_cap=PAIR_CAP, + seconds_cap=SECONDS, controls=controls(), timeout=reason, **result, + counts=dict(Counter(row["status"] for row in cases)), + access_counts=dict(Counter(f'{r["event"][0]}:{r["access"]}' for row in cases for r in row["contacts"])), + candidate_keys=[row["key"] for row in cases if row["status"] != "binary barrier"]) + + +def compare(path, result): + lead = loads(authenticate(path, PRIMARY), object_pairs_hook=unique) + assert lead["head"] == result["head"] and lead["pins"]["lead/PRICE.json"] == PINS["inputs/PRICE.json"] + assert lead["pins"]["inputs/7334-WORD.json.gz"] == PINS["inputs/7334-WORD.json.gz"] + assert lead["first_unvisited_event"] is result["last_unvisited_clock"] is None + assert lead["timeout"] is result["timeout"] is None and not result["unvisited_pair_keys"] + assert lead["counts"] == result["counts"] and lead["candidate_keys"] == result["candidate_keys"] + assert lead["moves"] == {str(k): v for k, v in result["moves"].items()} + ncontacts = 0 + for a, b in zip(lead["pairs"], result["pairs"], strict=True): + fields = ("key", "charts", "ranks", "status", "full_probe", "net") + assert all(a[k] == b[k] for k in fields) + assert a["contacts"] == [[r["clock"], r["event"]] for r in b["contacts"]] + ncontacts += len(b["contacts"]) + return dict(primary_sha256=PRIMARY, head=HEAD, exact_windows=len(lead["pairs"]), + exact_signed_contact_incidences=ncontacts, access_counts=result["access_counts"], + dispositions=result["counts"], agrees=True) + + +def main(): + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--primary", type=Path) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + if args.controls_only: + print(dumps(controls())) + return + result = audit(args.root) + print(dumps(compare(args.primary, result) if args.primary else result, indent=2, sort_keys=True)) + if result["timeout"]: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-changed-public-move-contraction-bound/engines/r101/quote.py b/research/p104-changed-public-move-contraction-bound/engines/r101/quote.py new file mode 100644 index 0000000000..ea41a30a03 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/engines/r101/quote.py @@ -0,0 +1,70 @@ +"""Preprice a same-clock public donor-bank contraction.""" +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/R100-PRICE.json": "7109125bbf60e3015c8c0ac7b10b24b7de61f358c1508d06604ebccd89ef6343", + "inputs/R100-GEOMETRY.json": "075301daf545c8021800c36af19d05517e3c4136dac4e2114cb85204d0b31c64", +} + + +def unique(pairs): + result = dict(pairs) + if len(result)!=len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def main(): + docs = {} + for path,pin in PINS.items(): + data = (ROOT/path).read_bytes() + if sha256(data).hexdigest()!=pin: + raise ValueError(f"changed dependency {path}") + docs[path] = json.loads(data,object_pairs_hook=unique) + price,geo = docs.values() + assert price["head"]==geo["head"] and len(geo["pairs"])==37 and not geo["timeout"] + assert geo["pins"]["lead/PRICE.json"]==PINS["inputs/R100-PRICE.json"] + profiles = {tuple(q["ranks"]):q for q in price["profiles"]} + candidates, by_role = [],{} + for row in geo["pairs"]: + if len(row["contacts"])!=1 or row["charts"][1]==207: + continue + t,event = row["contacts"][0] + f,g,role = row["key"] + if event[0]!="ADD" or event[1]!=role: + continue + p,q,s = row["ranks"] + quote = profiles[(*sorted((p,q)),s)] + assert row["net"]==quote["net"] and Q(quote["full_probe"][0])>0 + candidates.append({"key":row["key"],"charts":row["charts"],"add":[t,event], + "ranks":row["ranks"],"quote":quote}) + if role not in by_role or Q(quote["net"][1])>Q(by_role[role]["net"][1]): + by_role[role]=quote + assert len(candidates)==6 and len(by_role)==4 + assert all(Q(q["extra_rank_one_upper"])<0 for q in by_role.values()) + target_full_upper = Q(price["whole_target_margin_upper"]) + largest_unrestricted = max(Q(r["net_target"][1]) for r in profiles.values()) + base_target_upper = target_full_upper-price["distinct_compatible_cap"]*largest_unrestricted + whole_target_upper = base_target_upper + sum(max(Q(r["quote"]["net_target"][1]) for r in candidates if r["key"][2]==role) + for role in by_role) + candidates.sort(key=lambda r:(-Q(r["quote"]["net"][0]),r["key"])) + print(json.dumps({ + "head":price["head"],"pins":PINS,"kappa":price["kappa"],"caller_head":price["caller_head"], + "word_sha256":price["word_sha256"],"payload_sha256":price["word_payload_sha256"], + "probe":price["probe"],"candidates":candidates,"old_paid":110519,"one_new_paid":110502, + "targets":22461,"rank_surplus":1424,"distinct_roles":len(by_role), + "one_net_upper":str(max(Q(q["net"][1]) for q in by_role.values())), + "whole_net_upper":str(sum(Q(q["net"][1]) for q in by_role.values())), + "whole_target_margin_upper":str(whole_target_upper), + "limits":{"cases":12,"runner_seconds":20,"prototype_cases":1,"prototype_seconds":120}, + "scope":"Only moved destination has a sole ADD at its original clock. Use arbitrary rational same-clock public donor rows at A or C, excluding mover. No extra paid call. Complete price treats auxiliary ordinary cost as free, checks actual scalar/grid/compiler/ownership costs for any candidate.", + },indent=2,sort_keys=True)) + + +if __name__=="__main__": + assert __debug__ + main() diff --git a/research/p104-changed-public-move-contraction-bound/engines/r101/reverse_donors.py b/research/p104-changed-public-move-contraction-bound/engines/r101/reverse_donors.py new file mode 100644 index 0000000000..8c938806a1 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/engines/r101/reverse_donors.py @@ -0,0 +1,255 @@ +"""Verify the twelve R101 endpoint donor banks using exact reverse covectors.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "ac5ecb17f0e9f3c068423998b350a78c1a4769b6f61b50838be5f3e0d0b1a00c", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "reused/reverse_span.py": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", +} +PRIMARY = "b7700e618ce3c69cbe7544842f265e980f87903dea30121df118861d104b2c51" +CASE_CAP = 12 +SECONDS = 20 +EVENTS = 76466 + + +def unique(pairs): + obj = dict(pairs) + if len(obj) != len(pairs): + raise ValueError("Duplicate JSON key") + return obj + + +def checked(path, pin): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"Changed input {path.name}") + return raw + + +def touches(role, event): + return role == event[1] or event[0] in ("ADD", "COPY") and role == event[2] + + +def ring_ok(q): + d = q.denominator + for p in (2, 3, 5): + while d % p == 0: + d //= p + return d == 1 and abs(q)+1 < 2**16 + + +def requests_for(word, price): + n = word["public"] + tape = word["program"] + frames = word["frames"] + + @cache + def span(label): + values = {0} + for v in frames[label]: + assert type(v) is int and 0 < v < 512 and v not in values + values |= {v ^ u for u in values} + return values + + specs = [] + for row in price["candidates"]: + l, r, mover = row["key"] + a, b, c = row["charts"] + clock, event = row["add"] + source = event[2] + assert b != 207 and 0 <= mover < n and l < clock < r + assert tape[l] == ["MOVE", mover, a, b, False] + assert tape[r] == ["MOVE", mover, b, c, False] + assert tape[clock] == event and event == ["ADD", mover, source, event[3], b] + assert source != mover and Fraction(event[3]) + assert [t for t in range(l+1,r) if touches(mover, tape[t])] == [clock] + assert span(a) < span(b) < span(c) + for side, chart in (("entrance", a), ("exit", c)): + specs.append(dict(key=row["key"]+[side], clock=clock, mover=mover, original_chart=b, + chart=chart, source=source, source_multiplier=event[3])) + assert len(specs) == len({tuple(row["key"]) for row in specs}) == CASE_CAP + return specs + + +def collect(word, specs, engine, deadline, progress): + tape = word["program"] + n, owned = word["public"], word["owned_fields"] + assert (len(tape), n, owned) == (EVENTS,1501,68) + requests = defaultdict(list) + for row in specs: + requests[row["clock"]].append(row) + active = word["final"] + [None] * owned + fresh_copy_dest = set() + bank_at = {} + for clock in range(EVENTS - 1, -1, -1): + progress["last_unvisited_event"] = clock + if clock % 128 == 0 and monotonic() >= deadline: + raise TimeoutError("reverse chart walk") + op, d, *args = tape[clock] + assert 0 <= d < len(active) and (d not in fresh_copy_dest or op == "INIT") + if op == "MOVE": + a,b,is_owned = args + assert active[d] == b and is_owned == (d >= n) + active[d] = a + elif op == "INIT": + assert d >= n and active[d] == args[0] + active[d] = None + fresh_copy_dest.discard(d) + elif op == "CLEAR": + assert d >= n and active[d] is None + active[d] = args[0] + else: + assert op in ("ADD", "COPY", "SCALE") and active[d] == args[-1] + engine["coefficient"](args[-2]) + if op in ("ADD", "COPY"): + src = args[0] + assert src != d and active[src] == args[-1] + if op == "COPY": + assert d >= n + fresh_copy_dest.add(d) + for row in requests.get(clock, ()): + assert active[row["mover"]] == active[row["source"]] == row["original_chart"] + bank = [role for role, label in enumerate(active) if label == row["chart"] and role != row["mover"]] + bank_at[tuple(row["key"])] = ([r for r in bank if r < n], [r for r in bank if r >= n]) + progress["events_checked"] += 1 + assert active == word["initial"] + [None] * owned and not fresh_copy_dest + progress["last_unvisited_event"] = None + assert len(bank_at) == CASE_CAP + return bank_at + + +def evaluate(word, specs, banks, engine, deadline, rows_out, results): + requests = defaultdict(list) + ids = {} + + def demand(clock, role): + key = clock, role + if key not in ids: + ids[key] = len(ids) + requests[clock].append((role,ids[key])) + return ids[key] + + setups = [] + for row in specs: + clock = row["clock"] + public, owned = banks[tuple(row["key"])] + target_id = demand(clock, row["source"]) + donors = [(r,demand(clock,r)) for r in public] + setups.append((target_id, donors, owned)) + rows = engine["transpose_prefix"](word, requests, len(ids), deadline) + rows_out.extend(rows) + for row,(target_id,donors,owned) in zip(specs,setups,strict=True): + if monotonic() >= deadline: + raise TimeoutError("exact span gate") + target = rows[target_id] + bank = [(r,rows[i]) for r,i in donors] + proof = engine["exact_span"](bank,target) + status, replacement = "outside donor span", None + if proof["status"] == "exact_span": + replacement = {r: Fraction(row["source_multiplier"])*Fraction(v) for r,v in proof["coefficients"].items()} + status = "exact legal coefficients" if all(map(ring_ok,replacement.values())) else "coefficient gate unresolved" + replacement = {r:str(v) for r,v in replacement.items()} + elif proof["status"] == "absent_exterior_coordinate": + j = proof["coordinate"] + assert all(j not in vector for _, (vector,_) in bank) + proof["separating_covector"] = {j:"1"} + proof["separated_target"] = proof["target_coefficient"] + results.append(dict(key=row["key"],chart=row["chart"],source=[row["clock"],row["source"]], + source_nnz=len(target[0]),bank_roles=[r for r,_ in bank],owned_donors_excluded=owned, + target_row_id=target_id,donor_role_row_ids=donors,status=status,replacement_coefficients=replacement, + proof=proof)) + + +def audit(root,engine): + price = loads(checked(root / "inputs/PRICE.json",PINS["inputs/PRICE.json"]),object_pairs_hook=unique) + assert price["head"] == HEAD and price["caller_head"] == CALLER + assert price["word_sha256"] == PINS["inputs/7334-WORD.json.gz"] and price["payload_sha256"] == PAYLOAD + assert price["limits"]["cases"] == CASE_CAP and price["limits"]["runner_seconds"] == SECONDS + tests = engine["controls"]() + assert ring_ok(Fraction(-3,5)) and not ring_ok(Fraction(1,7)) + tests += ["bounded signed coefficient ring"] + keys = [p["key"]+[side] for p in price["candidates"] for side in ("entrance","exit")] + assert len(keys) == len({tuple(k) for k in keys}) == CASE_CAP + results, rows = [], [] + progress = dict(events_checked=0,last_unvisited_event=EVENTS-1) + reason = None + + def stop(*_): + raise TimeoutError("Hard 20-second cap") + + signal(SIGALRM,stop) + alarm(SECONDS) + deadline = monotonic()+SECONDS-2 + try: + raw = decompress(checked(root / "inputs/7334-WORD.json.gz",PINS["inputs/7334-WORD.json.gz"])) + assert sha256(raw).hexdigest() == PAYLOAD + word = loads(raw,object_pairs_hook=unique) + specs = requests_for(word,price) + assert [r["key"] for r in specs] == keys + banks = collect(word,specs,engine,deadline,progress) + evaluate(word,specs,banks,engine,deadline,rows,results) + except TimeoutError as error: + reason = str(error) + finally: + alarm(0) + return dict(head=HEAD,caller_head=CALLER,pins=PINS,cases_cap=CASE_CAP,runner_seconds_cap=SECONDS, + controls=tests,timeout=reason,progress=progress,unvisited=keys[len(results):], + results=results,exact_integer_rows=rows, + counts=dict(Counter(r["status"] for r in results))) + + +def compare(path, result): + primary = loads(checked(path,PRIMARY),object_pairs_hook=unique) + assert primary["head"] == result["head"] + assert primary["pins"]["lead/PRICE.json"] == PINS["inputs/PRICE.json"] + assert primary["pins"]["inputs/7334-WORD.json.gz"] == PINS["inputs/7334-WORD.json.gz"] + assert primary["timeout"] is result["timeout"] is None and not primary["unvisited"] and not result["unvisited"] + assert primary["counts"] == result["counts"] == {"outside donor span": CASE_CAP} + cases = [] + for a,b in zip(primary["results"],result["results"],strict=True): + fields = ("key","chart","source","source_nnz","bank_roles","owned_donors_excluded","status", + "replacement_coefficients") + assert all(a[k] == b[k] for k in fields) + assert a["rank"] == b["proof"]["donor_rank"] + cases.append(dict(key=b["key"],donor_count=len(b["bank_roles"]),donor_rank=a["rank"], + exact_rank_obstruction=b["proof"]["status"],source=b["source"],chart=b["chart"], + owned_donors_excluded=b["owned_donors_excluded"])) + return dict(head=HEAD,primary_sha256=PRIMARY,bank_status_agreement=CASE_CAP, + rank_agreement=CASE_CAP,cases=cases,counts=result["counts"]) + + +def main(): + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root",type=Path,default=ROOT) + parser.add_argument("--primary",type=Path) + parser.add_argument("--controls-only",action="store_true") + args=parser.parse_args() + source="reused/reverse_span.py" + checked(ROOT/source,PINS[source]) + engine=run_path(str(ROOT/source)) + if args.controls_only: + print(dumps(engine["controls"]())) + return + result=audit(args.root,engine) + print(dumps(compare(args.primary,result) if args.primary else result,indent=2,sort_keys=True)) + if result["timeout"]: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-changed-public-move-contraction-bound/engines/r101/reverse_span.py b/research/p104-changed-public-move-contraction-bound/engines/r101/reverse_span.py new file mode 100644 index 0000000000..5efbeac87e --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/engines/r101/reverse_span.py @@ -0,0 +1,393 @@ +"""Independent normalized reverse-contact and fraction-free donor-span gate.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import gcd, isqrt, lcm +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE = "c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d" +PRIME = 65521 + + +def unique(pairs): + values = dict(pairs) + assert len(values) == len(pairs), "duplicate JSON key" + return values + + +def checked(path, pin, compressed=False): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"changed input {path.name}") + return loads(decompress(raw) if compressed else raw, object_pairs_hook=unique) + + +@cache +def coefficient(raw): + q = Fraction(raw) + assert q and q.denominator % PRIME, "nonunit native denominator" + return q.numerator, q.denominator + + +def normalized(values, denominator): + if not values: + return {}, 1 + divisor = gcd(denominator, *values.values()) + if divisor != 1: + return {j: a // divisor for j, a in values.items()}, denominator // divisor + return values, denominator + + +def sum_scaled(first, second, factor): + a, da = first + b, db = second + numerator, denom = factor + if not b: + return first + common = lcm(da, db * denom) + out = {j: v * (common // da) for j, v in a.items()} + weight = numerator * (common // (db * denom)) + for j, v in b.items(): + val = out.get(j, 0) + weight * v + if val: + out[j] = val + else: + out.pop(j, None) + return normalized(out, common) + + +def incidence(e): + return e[1:3] if e[0] in ("ADD", "COPY") else e[1:2] + + +def candidates(word, quote): + n = word["public"] + tape = word["program"] + stock = {} + for case in quote["candidates"]: + owner = case["owner"] + left, right = case["move_clocks"] + a, middle, c = case["chart_path"] + original, entry = case["literal_ADD"] + assert case["owner_access"] == "destination" and entry[0] == owner + assert entry[1] == case["peer"] and entry[-1] == middle + assert tape[left] == ["MOVE", owner, a, middle, True] + assert tape[right] == ["MOVE", owner, middle, c, True] + assert tape[original] == ["ADD", *entry] + assert n <= owner and left < original < right + assert [i for i in range(left + 1, right) if owner in incidence(tape[i])] == [original] + assert case["cut_windows_pre_event"] == {"entrance": [left, right], "exit": [left + 1, right]} + stock[owner, left, right] = case + assert len(stock) == 3 and len({tuple(k) for k in quote["keys"]}) == quote["case_cap"] == 33 + return stock + + +def collect(word, cuts, observations, cap): + """Forward structural pass only. Assign one ID to each requested live value.""" + n = word["public"] + chart = list(word["initial"]) + [None] * word["owned_fields"] + revisions = [0] * len(chart) + fresh = set() + starts = {} + lifetimes = {} + requests = defaultdict(list) + observation_ids = {} + bank_ids = {} + value_id = {} + paid = Counter() + + @cache + def span(f): + vectors = {0} + for v in word["frames"][f]: + assert v not in vectors + vectors.update(v ^ t for t in tuple(vectors)) + return vectors + + def request(t, role): + assert chart[role] is not None + key = role, revisions[role] + if key not in value_id: + value_id[key] = len(value_id) + requests[t].append((role, value_id[key])) + return value_id[key] + + tape = word["program"] + for t in range(len(tape) + 1): + if t % 128 == 0 and monotonic() >= cap: + raise TimeoutError("literal structural scan") + for role in observations.get(t, ()): + observation_ids[t, role] = request(t, role) + for key, chart_id, exclude in cuts.get(t, ()): + bank_ids[key] = [(r, request(t, r)) for r, c in enumerate(chart) if c == chart_id and r != exclude] + if t == len(tape): + break + op, d, *args = tape[t] + assert 0 <= d < len(chart) + if op == "INIT": + assert d >= n and chart[d] is None + chart[d], starts[d] = args[0], t + fresh.add(d) + elif op == "CLEAR": + assert d >= n and chart[d] == args[0] and d in starts + lifetimes[d, starts.pop(d)] = t + chart[d] = None + fresh.discard(d) + elif op == "MOVE": + a, b, owned = args + assert chart[d] == a and owned == (d >= n) + assert span(a) < span(b) or owned and span(b) < span(a) + paid[abs(len(word["frames"][b]) - len(word["frames"][a]))] += 1 + chart[d] = b + fresh.discard(d) + continue + elif op == "SCALE": + assert chart[d] == args[-1] + coefficient(args[-2]) + fresh.discard(d) + else: + assert op in ("ADD", "COPY") + src, coeff, f = args + assert d != src and chart[d] == chart[src] == f + coefficient(coeff) + if op == "COPY": + assert d >= n and d in fresh + fresh.discard(d) + revisions[d] += 1 + assert not starts and chart == word["final"] + [None] * word["owned_fields"] + return requests, observation_ids, bank_ids, lifetimes, dict(paid), len(value_id) + + +def transpose_prefix(word, requests, count, cap): + """Propagate all requested output covectors backward, then transpose to input rows.""" + n = word["public"] + empty = ({}, 1) + adjoint = [empty] * (n + word["owned_fields"]) + tape = word["program"] + for t in range(max(requests), -1, -1): + if t % 128 == 0 and monotonic() >= cap: + raise TimeoutError("reverse normalized prefix") + op, d, *args = tape[t] + if op in ("INIT", "CLEAR"): + adjoint[d] = empty + elif op == "SCALE": + adjoint[d] = sum_scaled(empty, adjoint[d], coefficient(args[-2])) + elif op in ("ADD", "COPY"): + src = args[0] + adjoint[src] = sum_scaled(adjoint[src], adjoint[d], coefficient(args[-2])) + if op == "COPY": + adjoint[d] = empty + else: + assert op == "MOVE" + for r, output in requests.get(t, ()): + adjoint[r] = sum_scaled(adjoint[r], ({output: 1}, 1), (1, 1)) + assert not any(d for d, _ in adjoint[n:]) + by_output = [[] for _ in range(count)] + for coord, (coeffs, d) in enumerate(adjoint[:n]): + assert d % PRIME + for i, v in coeffs.items(): + by_output[i].append((coord, v, d)) + rows = [] + for entries in by_output: + common = lcm(*(d for _, _, d in entries)) + rows.append(normalized({i: v * (common // d) for i, v, d in entries}, common)) + return rows + + +def eliminate(v, basis, record=False): + """Reverse-pivot integer elimination. All leading pivots are exact.""" + v = v.copy() + reductions = [] + multiplier = 1 + while v: + k = max(v) + if k not in basis: + break + w = basis[k] + a, b = w[k], v[k] + d = gcd(a, b) + a, b = a // d, b // d + next_v = {j: a * x for j, x in v.items()} + for j, x in w.items(): + z = next_v.get(j, 0) - b * x + if z: + next_v[j] = z + else: + next_v.pop(j, None) + assert k not in next_v + g = gcd(*next_v.values()) or 1 + v = {j: x // g for j, x in next_v.items()} + if record: + reductions.append((k, Fraction(b, a) * multiplier)) + multiplier *= Fraction(g, a) + return v, reductions, multiplier + + +def dot(row, covector): + numerator, denominator = row + return sum((numerator.get(j, 0) * v for j, v in covector.items()), Fraction(0)) / denominator + + +def exact_span(bank, target): + t, dt = target + if not t: + return dict(status="exact_span", coefficients={}) + exterior = next((j for j in sorted(t) if all(j not in row for _, (row, _) in bank)), None) + basis = {} + histories = {} + for role, (v, d) in bank: + reduced, steps, scale = eliminate(v, basis, record=True) + if reduced: + pivot = max(reduced) + basis[pivot] = reduced + histories[pivot] = (role, d, steps, scale) + if exterior is not None: + residue = t[exterior] * pow(dt, -1, PRIME) % PRIME + return dict(status="absent_exterior_coordinate", donor_rank=len(basis), augmented_rank=len(basis)+1, + coordinate=exterior, target_coefficient=str(Fraction(t[exterior], dt)), + target_residue_mod_prime=residue) + residual, steps, scale = eliminate(t, basis, record=True) + if residual: + k = max(residual) + dual = {k: Fraction(1)} + for p, v in sorted(basis.items()): + coefficient = -sum((v.get(j, 0) * c for j, c in dual.items()), Fraction(0)) / v[p] + if coefficient: + dual[p] = coefficient + target_value = dot(target, dual) + assert target_value and all(dot(v, dual) == 0 for _, v in bank) + return dict(status="exact_rank_exclusion", donor_rank=len(basis), augmented_rank=len(basis) + 1, + missing_reverse_pivot=k, residual_integer_row=residual, + separating_covector={j: str(v) for j, v in dual.items()}, separated_target=str(target_value)) + pending = dict(steps) + solution = defaultdict(Fraction) + for pivot in sorted(basis): + if pivot not in pending: + continue + weight = pending.pop(pivot) + if not weight: + continue + role, denom, reductions, factor = histories[pivot] + weight /= factor + solution[role] += weight * denom / dt + for j, scalar in reductions: + pending[j] = pending.get(j, Fraction(0)) - weight * scalar + assert not pending + check = ({}, 1) + rows = dict(bank) + for r, x in solution.items(): + check = sum_scaled(check, rows[r], (x.numerator, x.denominator)) + assert check == target, (check, target) + return dict(status="exact_span", donor_rank=len(basis), + coefficients={r: str(x) for r, x in sorted(solution.items()) if x}) + + +def controls(): + toy = {"public": 4, "owned_fields": 1, "frames": [[]], "initial": [0] * 4, "final": [0] * 4, + "program": [["INIT", 4, 0], ["COPY", 4, 0, "1/2", 0], ["ADD", 4, 1, "-3", 0], + ["ADD", 0, 2, "2", 0], ["CLEAR", 4, 0]]} + req, ids, banks, _, _, count = collect(toy, {3:[((3,), 0, 4)], 4:[((4,), 0, 4)]}, {3:[4]}, float("inf")) + rows = transpose_prefix(toy, req, count, float("inf")) + target = rows[ids[3, 4]] + before = [(r, rows[i]) for r, i in banks[3,] if r in (0, 1)] + after = [(r, rows[i]) for r, i in banks[4,] if r in (0, 1)] + assert exact_span(before, target)["coefficients"] == {0:"1/2", 1:"-3"} + assert exact_span(after, target)["status"] == "exact_rank_exclusion" + assert exact_span(before[1:], target)["status"] == "absent_exterior_coordinate" + # Nontrivial exact dependency and reconstruction after a shared pivot. + multi = [(5, ({0: 3, 1: -1}, 2)), (6, ({0: 1, 1: 4}, 3)), (7, ({0: 11, 1: 2}, 1))] + hit = exact_span(multi, ({0: 11, 1: 2}, 1)) + assert hit["status"] == "exact_span" and len(hit["coefficients"]) == 2 + return ["signed_multi_source_and_owned_COPY", "intervening_write_blocks_span", "absent_exterior_coordinate", + "dependent_donor_bank_exact_reconstruction"] + + +def audit(word, quote, cap, decisions): + assert (word["public"], word["owned_fields"], len(word["program"])) == (1501, 68, 76466) + stock = candidates(word, quote) + observed = defaultdict(set) + cuts = defaultdict(list) + for row in quote["keys"]: + key = tuple(row) + owner, left, right, side, t = key + item = stock[owner, left, right] + chart = item["chart_path"][0 if side == "entrance" else 2] + assert item["cut_windows_pre_event"][side][0] <= t <= item["cut_windows_pre_event"][side][1] + cuts[t].append((key, chart, owner)) + observed[item["literal_ADD"][0]].add(item["peer"]) + requests, refs, banks, lifetimes, paid, count = collect(word, cuts, observed, cap) + assert paid == {1:4000, 2:853, 3:829, 4:223, 5:345, 6:14, 7:10, 8:5} + for item in stock.values(): + left, right = item["owner_lifetime"] + assert lifetimes[item["owner"], left] == right + rows = transpose_prefix(word, requests, count, cap) + for entry in quote["keys"]: + if monotonic() >= cap: + raise TimeoutError("exact donor bank gate") + owner, left, right, side, t = entry + item = stock[owner, left, right] + source = item["peer"] + target_id = refs[item["literal_ADD"][0], source] + target = rows[target_id] + bank = [(r, rows[i]) for r, i in banks[tuple(entry)]] + chart = item["chart_path"][0 if side == "entrance" else 2] + decision = exact_span(bank, target) + decisions.append(dict(key=entry, proposed_chart=chart, literal_read_peer=source, + literal_read_clock=item["literal_ADD"][0], donors=len(bank), owned_donors=sum(r>=word["public"] for r,_ in bank), + target_row_id=target_id, donor_role_row_ids=banks[tuple(entry)], + donor_rowset_sha256=sha256(dumps(bank, sort_keys=True).encode()).hexdigest(), **decision)) + return rows + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--word", type=Path) + parser.add_argument("--price", type=Path) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + if args.controls_only: + print(dumps(controls())) + return + assert args.word is not None and args.price is not None and __debug__ + start = monotonic() + def stop(*_): + raise TimeoutError("hard 20-second runner cap") + signal(SIGALRM, stop) + alarm(20) + decisions = [] + keys = [] + rows = None + tests = [] + timed_out = None + try: + tests = controls() + assert all(PRIME % d for d in range(2, isqrt(PRIME)+1)) + quote = checked(args.price, PRICE) + assert quote["head"] == HEAD and quote["word_sha256"] == WORD + keys = quote["keys"] + rows = audit(checked(args.word, WORD, compressed=True), quote, start+18, decisions) + except TimeoutError as error: + timed_out = str(error) + finally: + alarm(0) + result = dict(head=HEAD, word_sha256=WORD, price_sha256=PRICE, prime=PRIME, + case_cap=33, runner_cap_seconds=20, controls=tests, distinct_requested_rows=len(rows) if rows is not None else None, + requested_integer_rows=rows, + cases=decisions, disposition_counts=dict(Counter(r["status"] for r in decisions)), + unresolved=keys[len(decisions):], timeout=timed_out, + survivors=[r for r in decisions if r["status"] == "exact_span"]) + print(dumps(result, sort_keys=True, indent=2)) + if timed_out: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-changed-public-move-contraction-bound/engines/r101/support.py b/research/p104-changed-public-move-contraction-bound/engines/r101/support.py new file mode 100644 index 0000000000..383d612032 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/engines/r101/support.py @@ -0,0 +1,120 @@ +"""Exact rational membership of each sole ADD source in its endpoint banks.""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "lead/PRICE.json": "ac5ecb17f0e9f3c068423998b350a78c1a4769b6f61b50838be5f3e0d0b1a00c", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", +} + + +def unique(pairs): + result = dict(pairs) + if len(result)!=len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def checked(path): + raw = (ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def ring_ok(value): + d = value.denominator + for p in (2,3,5): + while d%p==0: + d//=p + return d==1 and abs(value)+1<2**16 + + +def stop(*_): + raise TimeoutError("hard runner timeout") + + +def main(): + assert __debug__ + price = json.loads(checked("lead/PRICE.json"),object_pairs_hook=unique) + checked("inputs/donor_span.py") + engine = run_path(str(ROOT/"inputs/donor_span.py")) + checks = engine["controls"]() + assert ring_ok(Q(-3,5)) and not ring_ok(Q(1,7)) + deadline = monotonic()+18 + signal(SIGALRM,stop) + alarm(price["limits"]["runner_seconds"]) + results = [] + pending = [] + reason = None + keys = [p["key"]+[side] for p in price["candidates"] for side in ("entrance","exit")] + assert len(keys)==len({tuple(k) for k in keys})==price["limits"]["cases"] + try: + raw = decompress(checked("inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest()==price["payload_sha256"] + word = json.loads(raw,object_pairs_hook=unique) + tape = word["program"] + public = word["public"] + req, targets = defaultdict(set),defaultdict(set) + for p in price["candidates"]: + f,g,d = p["key"] + a,b,c = p["charts"] + t,e = p["add"] + s = e[2] + assert f=deadline or (t,chart,d) not in banks or (t,s) not in values: + pending.append(key) + continue + all_live = banks[t,chart,d] + public_bank = {r:row for r,row in all_live.items() if r=deadline: + return None + r=vector.copy() + w={role:Q(1)} + reduce_row(r,basis,w,-1) + if r: + k=min(r) + d=r[k] + basis[k]=({i:a/d for i,a in r.items()},{i:a/d for i,a in w.items()}) + residual=target.copy() + weights={} + reduce_row(residual,basis,weights,1) + rebuilt={} + for role,a in weights.items(): + axpy(rebuilt,bank[role],a) + axpy(rebuilt,residual,Q(1)) + assert rebuilt==target + return dict(rank=len(basis), residual={i:str(v) for i,v in residual.items()}, + matching_coefficients={i:str(v) for i,v in weights.items()} if not residual else None) + + +def snapshot(word,requested,targets,deadline): + public=word["public"] + active=word["initial"]+[None]*word["owned_fields"] + rows=[{i:Q(1)} for i in range(public)]+[None]*word["owned_fields"] + banks,values={},{} + stop=max(requested.keys()|targets.keys()) + for t,e in enumerate(word["program"]): + if t%64==0 and monotonic()>=deadline: + break + for chart,r in requested.get(t,()): + banks[t,chart,r]={i:rows[i].copy() for i in range(len(active)) if i!=r and active[i]==chart and rows[i]} + for s in targets.get(t,()): + assert active[s] is not None + values[t,s]=rows[s].copy() + if t==stop: + break + op,r,*args=e + if op=="MOVE": + assert active[r]==args[0] and args[2]==(r>=public) + active[r]=args[1] + elif op=="INIT": + assert active[r] is None and rows[r] is None and r>=public + active[r]=args[0] + rows[r]={} + elif op=="CLEAR": + assert active[r]==args[0] and rows[r] is not None and r>=public + active[r]=rows[r]=None + elif op=="SCALE": + assert active[r]==args[1] and scalar(args[0]) + rows[r]={i:v*scalar(args[0]) for i,v in rows[r].items()} + else: + s,k,chart=args + assert active[r]==active[s]==chart and r!=s and op in ("ADD","COPY") + if op=="COPY": + assert r>=public and not rows[r] + axpy(rows[r],rows[s],scalar(k)) + return banks,values + + +def controls(): + d=monotonic()+1 + a,b={0:Q(1),1:Q(1)},{1:Q(2)} + assert solve({0:Q(3)}, {7:a,8:b},d)["matching_coefficients"]=={7:"3",8:"-3/2"} + assert solve({2:Q(1)}, {7:a,8:b},d)["residual"]=={2:"1"} + assert solve({0:Q(3)}, {7:{0:Q(1),2:Q(1)},8:b},d)["residual"]=={2:"-3"} + assert solve({}, {7:a},d)["matching_coefficients"]=={} + return ["two-donor span","separating coordinate","changed donor row","zero source"] + + +def main(): + root=Path(sys.argv[1]) + price=checked(root/"price/PRICE.json",PRICE) + word=checked(root/"inputs/7334-WORD.json.gz",WORD,True) + assert price["head"]==HEAD and price["word_sha256"]==WORD + moves=word["program"] + req,targets=defaultdict(set),defaultdict(set) + bykey={} + for p in price["candidates"]: + r,s=p["owner"],p["peer"] + f,g=p["move_clocks"] + a,b,c=p["chart_path"] + t,add=p["literal_ADD"] + assert add[:2]==[r,s] and moves[t]==["ADD",*add] and f=deadline or (t,s) not in values or (cut,chart,r) not in banks: + pending.append(key) + continue + bank=banks[cut,chart,r] + source=values[t,s] + result=solve(source,bank,deadline) + if result is None: + pending.append(key) + continue + output.append(dict(key=key,source=[t,s],target_chart=chart,bank_roles=sorted(bank), + source_nnz=len(source),**result, + decision="exact span survivor" if result["matching_coefficients"] is not None else "outside donor span")) + print(json.dumps(dict(head=HEAD,price_sha256=PRICE,word_sha256=WORD,status="CAPPED" if pending else "EXHAUSTED", + case_cap=33,seconds_cap=18,controls=checks,counts=Counter(x["decision"] for x in output), + decisions=output,unvisited=pending,survivors=[x["key"] for x in output if x["matching_coefficients"] is not None]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-changed-public-move-contraction-bound/inputs/pricing.py b/research/p104-changed-public-move-contraction-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/inputs/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +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 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 diff --git a/research/p104-changed-public-move-contraction-bound/receipts/SEPARATORS.json b/research/p104-changed-public-move-contraction-bound/receipts/SEPARATORS.json new file mode 100644 index 0000000000..82e4685da3 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/receipts/SEPARATORS.json @@ -0,0 +1,472 @@ +[ + { + "chart": 597, + "coefficient": "-1", + "coordinate": 648, + "donors": [ + 122, + 217, + 498, + 499, + 733 + ], + "key": [ + 42599, + 44596, + 198, + "entrance" + ], + "owned_donors_excluded": [], + "source": [ + 42600, + 1555 + ] + }, + { + "chart": 207, + "coefficient": "-1", + "coordinate": 648, + "donors": [], + "key": [ + 42599, + 44596, + 198, + "exit" + ], + "owned_donors_excluded": [], + "source": [ + 42600, + 1555 + ] + }, + { + "chart": 3, + "coefficient": "1", + "coordinate": 28, + "donors": [ + 112, + 113, + 114, + 115, + 117, + 118, + 120, + 122, + 124, + 126, + 132, + 140, + 141, + 142, + 147, + 149, + 150, + 152, + 153, + 155, + 156, + 157, + 161, + 164, + 165, + 167, + 168, + 170, + 171, + 174, + 176, + 180, + 182, + 183, + 184, + 185, + 188, + 190, + 193, + 195, + 197, + 198, + 199, + 201, + 202, + 207, + 208, + 217, + 219, + 220, + 221, + 452, + 453, + 454, + 455, + 457, + 461, + 471, + 473, + 474, + 475, + 482, + 484, + 492, + 495, + 498, + 499, + 507, + 508, + 518, + 520, + 521, + 523, + 526, + 527, + 528, + 530, + 531, + 532, + 537, + 538, + 540, + 541, + 543, + 544, + 545, + 550, + 551, + 553, + 554, + 556, + 568, + 569, + 570, + 577, + 580, + 583, + 584, + 585, + 586, + 588, + 589, + 647, + 649, + 703, + 704, + 707, + 709, + 715, + 718, + 722, + 731, + 733, + 755, + 756, + 757, + 765, + 793, + 885, + 900, + 908, + 909, + 930, + 932, + 935, + 962, + 1229, + 1236, + 1250, + 1251, + 1253, + 1262, + 1301, + 1302, + 1449, + 1453, + 1456, + 1462, + 1464, + 1473 + ], + "key": [ + 40102, + 44609, + 205, + "entrance" + ], + "owned_donors_excluded": [], + "source": [ + 40103, + 347 + ] + }, + { + "chart": 207, + "coefficient": "1", + "coordinate": 28, + "donors": [], + "key": [ + 40102, + 44609, + 205, + "exit" + ], + "owned_donors_excluded": [], + "source": [ + 40103, + 347 + ] + }, + { + "chart": 3, + "coefficient": "1", + "coordinate": 29, + "donors": [ + 113, + 115, + 122, + 132, + 140, + 141, + 165, + 198, + 217, + 455, + 473, + 475, + 482, + 495, + 498, + 499, + 523, + 527, + 528, + 530, + 531, + 537, + 538, + 540, + 541, + 543, + 544, + 545, + 550, + 551, + 553, + 554, + 556, + 568, + 569, + 570, + 577, + 580, + 583, + 584, + 585, + 586, + 588, + 589, + 647, + 709, + 715, + 718, + 722, + 731, + 733, + 755, + 756, + 757, + 765, + 900, + 908, + 909, + 930, + 1236, + 1262, + 1301, + 1456, + 1462, + 1473 + ], + "key": [ + 41176, + 41178, + 532, + "entrance" + ], + "owned_donors_excluded": [], + "source": [ + 41177, + 363 + ] + }, + { + "chart": 746, + "coefficient": "1", + "coordinate": 29, + "donors": [ + 452, + 1250 + ], + "key": [ + 41176, + 41178, + 532, + "exit" + ], + "owned_donors_excluded": [], + "source": [ + 41177, + 363 + ] + }, + { + "chart": 744, + "coefficient": "-1/2", + "coordinate": 27, + "donors": [ + 361, + 363, + 1125 + ], + "key": [ + 41178, + 44611, + 532, + "entrance" + ], + "owned_donors_excluded": [], + "source": [ + 41179, + 452 + ] + }, + { + "chart": 207, + "coefficient": "-1/2", + "coordinate": 27, + "donors": [], + "key": [ + 41178, + 44611, + 532, + "exit" + ], + "owned_donors_excluded": [], + "source": [ + 41179, + 452 + ] + }, + { + "chart": 3, + "coefficient": "1/4", + "coordinate": 2, + "donors": [ + 115, + 132, + 165, + 217, + 455, + 498, + 499, + 531, + 556, + 586, + 647, + 718, + 722, + 731, + 755, + 756, + 757, + 765, + 900, + 930, + 1262, + 1301, + 1462, + 1473 + ], + "key": [ + 42533, + 42599, + 198, + "entrance" + ], + "owned_donors_excluded": [], + "source": [ + 42534, + 709 + ] + }, + { + "chart": 120, + "coefficient": "1/4", + "coordinate": 2, + "donors": [ + 648, + 649, + 653, + 654, + 962, + 1447, + 1493 + ], + "key": [ + 42533, + 42599, + 198, + "exit" + ], + "owned_donors_excluded": [ + 1555 + ], + "source": [ + 42534, + 709 + ] + }, + { + "chart": 120, + "coefficient": "-1/2", + "coordinate": 13, + "donors": [ + 198, + 648, + 649, + 653, + 962, + 1447, + 1493 + ], + "key": [ + 43135, + 44564, + 654, + "entrance" + ], + "owned_donors_excluded": [], + "source": [ + 43136, + 302 + ] + }, + { + "chart": 983, + "coefficient": "-1/2", + "coordinate": 13, + "donors": [ + 1305, + 1488 + ], + "key": [ + 43135, + 44564, + 654, + "exit" + ], + "owned_donors_excluded": [], + "source": [ + 43136, + 302 + ] + } +] diff --git a/research/p104-changed-public-move-contraction-bound/receipts/SHA256.json b/research/p104-changed-public-move-contraction-bound/receipts/SHA256.json new file mode 100644 index 0000000000..2c2e083626 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/receipts/SHA256.json @@ -0,0 +1,10 @@ +{ + "r100/independent/AGREEMENT.json": "ef797676d7550c65ca1780e5c7f8cc568f53f9c80ce764a659754c0cbcdc13e3", + "r100/independent/RESULT.json": "5462d132a6610dc8953332cadcad0c9b2096fa7db2bc131af3dbd80614b52d25", + "r100/lead/GEOMETRY.json": "075301daf545c8021800c36af19d05517e3c4136dac4e2114cb85204d0b31c64", + "r100/lead/PRICE.json": "7109125bbf60e3015c8c0ac7b10b24b7de61f358c1508d06604ebccd89ef6343", + "r101/independent/AGREEMENT.json": "9618ff9dc2282bee0068866879d900f881dc440234c5d12cb0dcf983c21eb6f3", + "r101/independent/RESULT.json": "526deef9465a563146100282ccb84bcc3d7613333354c48ec9452d97ff7d3d20", + "r101/lead/PRICE.json": "ac5ecb17f0e9f3c068423998b350a78c1a4769b6f61b50838be5f3e0d0b1a00c", + "r101/lead/SUPPORT.json": "b7700e618ce3c69cbe7544842f265e980f87903dea30121df118861d104b2c51" +} diff --git a/research/p104-changed-public-move-contraction-bound/replay.py b/research/p104-changed-public-move-contraction-bound/replay.py new file mode 100644 index 0000000000..bcdfd32565 --- /dev/null +++ b/research/p104-changed-public-move-contraction-bound/replay.py @@ -0,0 +1,171 @@ +"""Regenerate the exact current-word public MOVE and donor-span receipts.""" +from argparse import ArgumentParser +from fractions import Fraction +from gzip import decompress +from hashlib import sha1, sha256 +from json import loads +from pathlib import Path, PurePosixPath +from shutil import copyfile +from subprocess import run +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent + + +def unique(pairs): + data = dict(pairs) + if len(data) != len(pairs): + raise ValueError("duplicate JSON key") + return data + + +def decode(raw): + return loads(raw, object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def safe(name): + path = PurePosixPath(name) + if not path.parts or path.is_absolute() or path.as_posix() != name or ".." in path.parts: + raise ValueError("invalid local path " + name) + return path + + +def verify_inputs(): + pins = decode((HERE / "LOCAL-PINS.json").read_bytes()) + for name, expected in pins.items(): + if digest((HERE / safe(name)).read_bytes()) != expected: + raise ValueError("changed dependency " + name) + provenance = decode((HERE / "PROVENANCE.json").read_bytes()) + for name, row in provenance["files"].items(): + raw = (HERE / safe(name)).read_bytes() + assert digest(raw) == row["sha256"] + assert sha1(f"blob {len(raw)}\0".encode()+raw).hexdigest() == row["git_blob"] + admission = decode((HERE / "inputs/ADMITTED.json").read_bytes()) + bench = decode((HERE / "inputs/BENCHMARK.json").read_bytes()) + assert digest((HERE / "inputs/ADMITTED.json").read_bytes()) == bench["admission_sha256"] + assert admission["head"] == bench["head"] and admission["crossing"] == bench["crossing"] + r92 = decode((HERE / "inputs/PR7362-SHA256.json").read_bytes()) + assert digest(decompress((HERE / "inputs/R92-PRICE.json.gz").read_bytes())) == r92["R92-PRICE.json"] + + +def install(source, destination): + destination.parent.mkdir(parents=True, exist_ok=True) + copyfile(source, destination) + + +def command(script, *args, timeout=20, check=True): + return run([sys.executable,"-I","-B",str(script),*map(str,args)], + capture_output=True,check=check,timeout=timeout) + + +def replay(root, output): + verify_inputs() + wanted = decode((HERE / "receipts/SHA256.json").read_bytes()) + regenerated = set() + + def stage(label, script, *args, timeout=20): + raw = command(script,*args,timeout=timeout).stdout + if digest(raw) != wanted[label]: + raise ValueError(f"changed receipt {label}: {digest(raw)}") + assert label not in regenerated + regenerated.add(label) + result = root / safe(label) + result.parent.mkdir(parents=True, exist_ok=True) + result.write_bytes(raw) + return decode(raw) + + old, new = root/"r100", root/"r101" + for target, name, primary, reverse in ( + (old, "r100", "geometry.py", "reverse_contacts.py"), + (new, "r101", "support.py", "reverse_donors.py"), + ): + for path in ("quote.py", primary): + install(HERE/"engines"/name/path, target/"lead"/path) + install(HERE/"engines"/name/reverse,target/"independent"/reverse) + for destination in (target/"inputs", target/"independent/inputs"): + install(HERE/"inputs/7334-WORD.json.gz",destination/"7334-WORD.json.gz") + for name in ("BENCHMARK.json", "7334-CHANGED.json", "pricing.py"): + install(HERE/"inputs"/name,old/"inputs"/name) + install(HERE/"inputs/7334-CHANGED.json",old/"independent/inputs/7334-CHANGED.json") + (old/"inputs/R92-PRICE.json").write_bytes(decompress((HERE/"inputs/R92-PRICE.json.gz").read_bytes())) + price = stage("r100/lead/PRICE.json", old/"lead/quote.py") + assert price["full_paid_before"] == 110519 and price["full_paid_after"] == 110502 + assert price["productive_positions"] == 22461 and price["rank_surplus"] == 1424 + assert len(price["roles"]) == 14 and price["distinct_compatible_cap"] == 56 + assert Fraction(price["whole_target_margin_upper"]) < Fraction("-116") + geom = stage("r100/lead/GEOMETRY.json",old/"lead/geometry.py") + assert geom["counts"] == {"binary barrier":37} and not geom["candidate_keys"] + assert geom["first_unvisited_event"] is None and geom["timeout"] is None + assert sum(geom["moves"].values()) == 51 + install(old/"lead/PRICE.json",old/"independent/inputs/PRICE.json") + contacts = old/"independent/reverse_contacts.py" + reverse = stage("r100/independent/RESULT.json",contacts) + assert reverse["events_checked"] == 76466 and not reverse["unvisited_pair_keys"] + agreement = stage("r100/independent/AGREEMENT.json",contacts,"--primary",old/"lead/GEOMETRY.json") + assert agreement["agrees"] and agreement["exact_windows"] == 37 and agreement["exact_signed_contact_incidences"] == 67 + assert agreement["access_counts"] == {"ADD:destination":32,"ADD:source":33,"SCALE:unary":2} + + for name in ("PRICE", "GEOMETRY"): + install(old/f"lead/{name}.json",new/f"inputs/R100-{name}.json") + install(HERE/"inputs/donor_span.py",new/"inputs/donor_span.py") + install(HERE/"engines/r101/reverse_span.py",new/"independent/reused/reverse_span.py") + quote = stage("r101/lead/PRICE.json",new/"lead/quote.py") + assert len(quote["candidates"]) == 6 and quote["distinct_roles"] == 4 + assert quote["one_new_paid"] == 110502 and quote["targets"] == 22461 + assert Fraction(quote["whole_target_margin_upper"]) < Fraction("-138") + support = stage("r101/lead/SUPPORT.json",new/"lead/support.py") + assert support["counts"] == {"outside donor span":12} and not support["unvisited"] + install(new/"lead/PRICE.json",new/"independent/inputs/PRICE.json") + donors = new/"independent/reverse_donors.py" + reverse = stage("r101/independent/RESULT.json",donors) + assert len(reverse["exact_integer_rows"]) == 261 and not reverse["unvisited"] + agree = stage("r101/independent/AGREEMENT.json",donors,"--primary",new/"lead/SUPPORT.json") + assert agree["bank_status_agreement"] == agree["rank_agreement"] == 12 + + witness = decode((HERE/"receipts/SEPARATORS.json").read_bytes()) + rows = reverse["exact_integer_rows"] + for summary, tested in zip(witness,reverse["results"],strict=True): + for k in ("key","chart","source","owned_donors_excluded"): + assert summary[k] == tested[k] + assert summary["donors"] == tested["bank_roles"] + coordinate = str(summary["coordinate"]) + numerator, denominator = rows[tested["target_row_id"]] + assert Fraction(numerator[coordinate],denominator) == Fraction(summary["coefficient"]) != 0 + assert all(coordinate not in rows[i][0] for _,i in tested["donor_role_row_ids"]) + assert tested["proof"]["separating_covector"] == {coordinate:"1"} + + for source, directory, mutation in ( + (contacts,old/"independent","PRICE.json"), + (donors,new/"independent","7334-WORD.json.gz"), + ): + target = directory/"inputs"/mutation + original = target.read_bytes() + target.write_bytes(original+b"\n") + try: + bad = command(source,check=False,timeout=10) + assert bad.returncode == 1 and not bad.stdout and b"Changed input " in bad.stderr + finally: + target.write_bytes(original) + assert regenerated == set(wanted) + if output: + for name in sorted(regenerated): + install(root/safe(name),output/safe(name)) + print("PASS_P104_PUBLIC_MOVE_CONTRACTION windows=37 binary=37 donor_banks=12 separators=12 unresolved=0 receipts=8") + + +def main(): + assert __debug__ and sys.version_info[:2] == (3,12) + parser = ArgumentParser(description=__doc__) + parser.add_argument("--output",type=Path,help="Optional directory for regenerated evidence") + args = parser.parse_args() + with TemporaryDirectory(prefix="public-move-contact-") as temporary: + replay(Path(temporary),args.output) + + +if __name__ == "__main__": + main()