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-owned-move-destination-span/LOCAL-PINS.json b/research/p104-owned-move-destination-span/LOCAL-PINS.json new file mode 100644 index 0000000000..cf3117f703 --- /dev/null +++ b/research/p104-owned-move-destination-span/LOCAL-PINS.json @@ -0,0 +1,22 @@ +{ + "dependencies/round30/complex/audit.py": "67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb", + "dependencies/round30/complex/source/inputs/CALLER.json.gz": "58beaf24e01c0589ecd5d1676d6d27e75b779f089d0674eda11725465ffc04e1", + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": "9851ebaa4b4404be1f5670b8a8dfc6ee96a8e19e85731edd4a71d52bbfa9c793", + "dependencies/round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "dependencies/round30/complex/source/powers.py": "c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee", + "dependencies/round41/independent/RESULT.json": "1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7", + "dependencies/round41/independent/donor_replay.py": "2407116eba5b9c8231f0469b14963f1d5ef9a7dc315079b6e12011831ffcb0d6", + "dependencies/round41/independent/replay_bank.py": "a2a12b33fd7ef7bdc469d97902edaddc592bf40228a7f58c0c3499c177222d28", + "dependencies/round41/independent/replay_core.py": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "dependencies/round41/independent/replay_pairs.py": "75a69025bb1b70578e848f336c4ce85b3f8c62a51eed72c7d9070b1e671c7241", + "dependencies/round41/lead/r41-price-support/PRICE.json": "1efe8b52e02a8db0ac6a04cdf6b943e515badee5fc0b7bea6ea3fe4a30fd1d01", + "dependencies/round41/lead/r41-price-support/SUPPORT.json": "c31c8425e2a99fe15a9ffa48662dacca4eda2b778d55ceceae2978a9bdb12f3c", + "engines/fullbank.py": "d7930a4e6a2585a52c7a9d43b9b802f6d0ceb1c3928c2b0cdf16d6dbe655029b", + "engines/pairs.py": "b2fc8fd0dd01471a9c2eb425eb123f4cd41aee922d3b09b3ff46b6cf9d88de26", + "receipts/fullbank/PRICE.json": "959b9e4ceb947577ab42d759e91bed48ce855ccce32e72a51a0bf49de524bc4d", + "receipts/fullbank/SUPPORT.json": "1cd0f34e721c4559def3a3f88a80737a480294cbc5b72c16221c9f3e89c4c7da", + "receipts/independent/BANK.json": "9600d23495eca54fc13fae0b88e316de5928d44423cfb4f8fe2f7a6e0b3b1422", + "receipts/independent/PAIRS.json": "f5dbfb93b650787774539746670e7fc71168209d966f0de4df273544fac0b715", + "receipts/pairs/PRICE.json": "34468ff846c336db7d712ec8bccdf2c659e167baf935bf63bb6eb463898d8e45", + "receipts/pairs/SUPPORT.json": "f4997460d73a4ccd35ee3e0facced89bc33184c26cdd74b247479abe7386cc32" +} diff --git a/research/p104-owned-move-destination-span/NOTICE b/research/p104-owned-move-destination-span/NOTICE new file mode 100644 index 0000000000..464bb0c4f4 --- /dev/null +++ b/research/p104-owned-move-destination-span/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. +The literal native word and crossing come from #7277, the signed caller +from #7113, and the earlier destination-bank or owned-MOVE precedents +from #6069, #7293, #7165 and #7307. The bundled census and signed price +use the same campaign's earlier exact-word replay. OpenAI Codex and +subagents materially assisted. diff --git a/research/p104-owned-move-destination-span/PROVENANCE.json b/research/p104-owned-move-destination-span/PROVENANCE.json new file mode 100644 index 0000000000..2f7eb22afd --- /dev/null +++ b/research/p104-owned-move-destination-span/PROVENANCE.json @@ -0,0 +1,29 @@ +{ + "files": { + "dependencies/round30/complex/source/inputs/CALLER.json.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "9451ceaf6e8e037894680b549f3ef41c21b260d7", + "path": "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "uncompress": true + }, + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "ef86c8ec8ed0a2042017a6f42515e70dd15cfffd", + "path": "research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "sha256": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "uncompress": true + }, + "dependencies/round30/complex/source/inputs/WORD.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "077bf48c35db0ddafae81f1bfa0ffacc30894b2b", + "path": "research/p104-terminal-cut-rechart/WORD.json.gz", + "sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-owned-move-destination-span/README.md b/research/p104-owned-move-destination-span/README.md new file mode 100644 index 0000000000..68adcf8973 --- /dev/null +++ b/research/p104-owned-move-destination-span/README.md @@ -0,0 +1,85 @@ +# Live destination span bound for paid P104 owned MOVEs + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** On the exact +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) P104 +word, at each paid owned MOVE's literal clock, form the bank of other +nonzero rows already live at that MOVE's original destination chart. +The moving row is outside the bank's exact rational span for all 47 +MOVEs. The exhaustive census contains 424 donor incidences and has zero +unresolved cases. The compatible paid saving upper bound is exactly zero. + +## Price and evidence + +The full signed invoice is rebuilt on the exact native word and +17-copy #7113 caller. The replay saves the directed price before +checking donor support. Granting each eligible MOVE deletion once +and all replacement work free gives an initial upper of about +1,778.20218 raw units for 44 sites with two or more donors. All 2,767 +exact pairs fail. The 39 remaining sites with three or more donors +give a second optimistic upper of about 1,676.28799 raw units before +the complete-bank test. Exact rational price intervals and the pinned +raw crossing upper are in the [pair price](receipts/pairs/PRICE.json) +and [bank price](receipts/fullbank/PRICE.json). + +The [full-bank receipt](receipts/fullbank/SUPPORT.json) gives one +sparse rational separating dual per literal MOVE. Its dot product +vanishes on every available donor row and is nonzero on the target. +The replay verifies those products on the original rows. A separate +denominator-cleared rank implementation independently gives a rank +increase after adjoining the target for every one of the 39 larger +banks. The other eight cuts are independently covered by exact +pair checks and the one-donor or zero-input controls. The +[pair](receipts/independent/PAIRS.json) and +[rank](receipts/independent/BANK.json) receipts record that coverage. +Controls include a combination requiring three donors, dependent +rows, an empty bank, a sign mutation and an outside coordinate. +Both support engines use the pinned exact normalized word interpreter. + +The result fixes the literal clock, original destination-chart ID, +original word and live bank. Changed clocks, other charts, cached retired +rows, new paid deliveries, altered ownership and simultaneous word +changes are outside this bound. No physical candidate was built. The +strongest independently reproduced comparable witness remains #7277 +at conditional κ = 0.003645669928698. + +## Replay + +From a clean checkout, use CPython 3.12 with assertions enabled and +the standard library. + +~~~sh +python3.12 -B scripts/research_package.py --package research/p104-owned-move-destination-span +python3.12 -B scripts/check_research_commit.py --package research/p104-owned-move-destination-span --check-modes --check-source-history +~~~ + +For a Git-free export run +`python3.12 -I -B research/p104-owned-move-destination-span/replay.py`. +[PROVENANCE.json](PROVENANCE.json) records exact public commits, paths, +Git blobs and SHA-256 for the word, crossing receipt and caller. +[LOCAL-PINS.json](LOCAL-PINS.json) authenticates the bundled scripts, +dependencies and exact receipts by package-relative paths. No external +checkout, prior temporary state or network fetch is required. + +## Predecessors + +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) at +`ed090b57ed88f8859e5ff4643645099e6ba856ea` supplies the literal word +and comparator. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +at `07a76c5e2738882c0cb322278e56f6cae3c9885d` supplies the signed caller. +[#6069](https://github.com/CrocSwap/integer-mult-bounds/pull/6069) +supplies the older complex endpoint span precedent. +[#7293](https://github.com/CrocSwap/integer-mult-bounds/pull/7293) +supplies the same-clock destination-bank method on BIT. +[#7165](https://github.com/CrocSwap/integer-mult-bounds/pull/7165) +supplies the earlier complex owned-MOVE donor-route comparison. +[#7307](https://github.com/CrocSwap/integer-mult-bounds/pull/7307) +supplies the direct-deletion baseline on the same 47 moves. +OpenAI Codex and subagents materially assisted. + +## Open next questions + +Can a changed schedule or a newly paid donor provide a row before the +required read? Pin that changed bank and bound its total compatible +saving across the full signed invoice. A surviving proposal needs +exact physical signed action, ownership and restoration, and all +routing, precision and tape costs charged. diff --git a/research/p104-owned-move-destination-span/SOURCES.json b/research/p104-owned-move-destination-span/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-owned-move-destination-span/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-owned-move-destination-span/TASK.json b/research/p104-owned-move-destination-span/TASK.json new file mode 100644 index 0000000000..d2ae20896d --- /dev/null +++ b/research/p104-owned-move-destination-span/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Recover each paid owned MOVE on the exact #7277 word from other already-live original destination-chart rows at its literal clock.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Round 43 research campaign", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Bound paid MOVE savings from the full same-clock destination bank before testing a physical replacement.", + "budget_minutes": 3, + "evidence": "Exact paid 17-copy invoice and outward price, independent one/two-donor checks, 47 sparse separating duals, independent denominator-cleared ranks for the 39 larger banks.", + "open_questions": [ + { + "blocked_by": "Any survivor still needs physical arbitrary-input equivalence, ownership and restoration, and fully charged routing, precision and tape costs.", + "first_step": "Pin a changed clock or newly paid donor and bound compatible savings over the full word on one signed invoice.", + "question": "Can one changed coframed schedule provide a donor before the same read?", + "why_it_matters": "The complete original live bank misses every target row." + } + ], + "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": "This tests alternate nonzero donor reconstruction at a fixed clock, beyond direct deletion and earlier-word source or carrier routes.", + "scope_status": "changed", + "stop_rule": "Price each compatible old MOVE once before decoding. Exhaust all 2,767 pairs and, if none fit, all 47 complete banks or explicitly report unresolved cases.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-owned-move-destination-span/VERIFY.json b/research/p104-owned-move-destination-span/VERIFY.json new file mode 100644 index 0000000000..dee7777d5e --- /dev/null +++ b/research/p104-owned-move-destination-span/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Reprice the complete signed word, replay all 2,767 donor pairs and 47 rational bank duals, and independently verify the exact augmented ranks.", + "timeout_seconds": 150 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-owned-move-destination-span/dependencies/round30/complex/audit.py b/research/p104-owned-move-destination-span/dependencies/round30/complex/audit.py new file mode 100644 index 0000000000..89e4a6b3dd --- /dev/null +++ b/research/p104-owned-move-destination-span/dependencies/round30/complex/audit.py @@ -0,0 +1,423 @@ +"""Independent exact binary-scope audit of signed invoice and flow/cut equality.""" +import argparse +from collections import Counter, defaultdict, deque +from fractions import Fraction as F +from hashlib import sha256 +from itertools import pairwise +from pathlib import Path +from time import monotonic +import gzip +import json +import runpy +import sys + +ROOT = Path(__file__).resolve().parent +SOURCE = ROOT / 'source' +GRID = 10**48 +TARGET = F(10018846261809, 2500000000000000) +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +INPUTS = { + 'inputs/WORD.json.gz': '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + 'inputs/EARLY-RESULT.json': '691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7', + 'inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'powers.py': 'c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee', +} + + +def source(path): + data = (SOURCE / path).read_bytes() + assert sha256(data).hexdigest() == INPUTS[path] + return data + + +def basis(vectors): + pivot = {} + for v in vectors: + while v.bit_length() in pivot: + v ^= pivot[v.bit_length()] + assert v + pivot[v.bit_length()] = v + return pivot + + +def inside(vectors, pivot): + for v in vectors: + while v: + if v.bit_length() not in pivot: + return False + v ^= pivot[v.bit_length()] + return True + + +def log_scaled(value): + z = (value - 1) / (value + 1) + term = z + q = F(0) + for j in range(0, 160, 2): + q += term / (j+1) + term *= z*z + return 2*q, 2*(q+term/(161*(1-z*z))) + + +def exp_minus(value, steps): + term = F(1) + total = F(1) + for j in range(1, steps+1): + term *= -value / j + total += term + return total + + +def verify_power(rank, value): + if not rank: + assert value == (0, 0) + return + exponent = rank.bit_length()-1 + unit_lo, unit_hi = log_scaled(F(rank, 1 << exponent)) + two_lo, two_hi = log_scaled(F(2)) + xlo = TARGET*(unit_lo+exponent*two_lo) + xhi = TARGET*(unit_hi+exponent*two_hi) + assert 0 <= xlo <= xhi < 1 + # Round the exponents outward before Taylor, keeping intermediate + # numerators small without losing the finer-than-grid audit. + fine = 10**64 + xlo = F((xlo*fine).__floor__(), fine) + xhi = F((xhi*fine).__ceil__(), fine) + low = GRID*rank*exp_minus(xhi, 49) + high = GRID*rank*exp_minus(xlo, 50) + assert value[0] <= low <= high <= value[1], rank + + +def read_model(): + word = json.loads(gzip.decompress(source('inputs/WORD.json.gz'))) + early = json.loads(source('inputs/EARLY-RESULT.json')) + caller = json.loads(source('inputs/CALLER.json')) + source('powers.py') + primary = runpy.run_path(str(SOURCE/'powers.py')) + assert primary['GRID'] == GRID and primary['TARGET'] == TARGET + initial, final = word['initial'], word['final'] + n = word['public'] + program = word['program'] + frame = word['frames'] + ranks = [len(v) for v in frame] + bases = [basis(v) for v in frame] + subset = {} + main = set(word['live']) | {r+112 for r in word['live']} | set(word['hosted']['X2'] + word['hosted']['Y2']) + assert len(main) == 400 + + def nested(a, b): + key = a,b + if key not in subset: + subset[key] = ranks[a] < ranks[b] and inside(frame[a], bases[b]) + return subset[key] + + def rank(a, b, owned): + if a == b: + return 0 + if nested(a, b) or owned and nested(b, a): + return abs(ranks[a]-ranks[b]) + return None + + chart = {(-1, r): f for r, f in enumerate(initial)} + current = initial + [None]*word['owned_fields'] + contacts = [[(-1, r)] for r in range(n)] + [[] for _ in range(word['owned_fields'])] + chains = [] + paid = Counter() + for t, row in enumerate(program): + op, r = row[:2] + if op == 'MOVE': + a, b, owned = row[2:] + assert current[r] == a and owned == (r >= n) + rr = rank(a, b, owned) + assert rr + paid[rr] += 1 + current[r] = b + continue + f = row[-1] + key = (t, 0) + chart[key] = f + if op == 'INIT': + assert r >= n and not contacts[r] and current[r] is None + current[r] = f + roles = {r, row[2]} if op in ('ADD', 'COPY') else {r} + for role in roles: + assert current[role] == f + contacts[role].append(key) + if op == 'CLEAR': + assert r >= n and contacts[r] + chains.append((r, contacts[r])) + contacts[r] = [] + current[r] = None + assert current == final + [None]*word['owned_fields'] and not any(contacts[n:]) + assert len(chains) == 70 + movable = {k for k in chart if k[0] != -1} + terminal = {} + for r, f in enumerate(final): + key = (len(program), r) + chart[key] = f + contacts[r].append(key) + chains.append((r, contacts[r])) + if r not in main: + terminal[key] = initial[r] + movable.add(key) + edges = [(a,b,r >= n) for r, seq in chains for a,b in pairwise(seq)] + native_paid = Counter(rr for a,b,owned in edges if (rr := rank(chart[a],chart[b],owned))) + assert native_paid == paid and sum(paid.values()) == 6280 and len(edges) == 137891 + assert len(chart) == 73165 and len(terminal) == 1101 + copies = sum(e[0] == 'J' for e in caller['events']) + assert copies == 17 + target = Counter(rank(initial, chart[v], False) for v, initial in terminal.items()) + assert min(target) > 0 + P, T = [Counter({r: copies*q for r, q in hist.items()}) for hist in (paid, target)] + for kind, info in caller['types'].items(): + count = len(info['ports']) + for sign, offset, *bits in info['diagonal']: + assert (sign, offset, len(bits)) == (-1, 0, copies) + T[1+8*sum(bits)] += count + for event in caller['events']: + if event[0] == 'J': + continue + kind, op, _, *args = event + count = len(caller['types'][kind]['ports']) + if op == 'QUERY': + P[1] += count + elif op in ('IDLE_ONE', 'IDLE_ODD'): + P[8*len(args[0])+int(op == 'IDLE_ODD')] += count + assert P == Counter({int(k):n for k,n in early['invoice']['P'].items()}) + assert T == Counter({int(k):n for k,n in early['invoice']['T'].items()}) + assert sum(P.values()) == 110536 and sum(T.values()) == 22461 + prices = {r: tuple(int(v*GRID) for v in primary['power'](r,TARGET)) for r in P.keys()|T.keys()|set(range(1,10))} + prices[0] = (0,0) + for r,v in prices.items(): + verify_power(r,v) + incident = defaultdict(list) + charts = defaultdict(list) + for i,(a,b,_) in enumerate(edges): + incident[a].append(i) + incident[b].append(i) + for v in sorted(movable): + charts[chart[v]].append(v) + return chart, rank, terminal, edges, incident, charts, copies, P, T, prices + + +def dinic(n, s, t, caps, clock): + """Return feasible flow and prove equal capacity of the residual cut.""" + adj = [[] for _ in range(n)] + graph = [] + for (u,v),cap in sorted(caps.items()): + if cap: + assert cap > 0 and u != v + i = len(graph) + graph.extend(([u,v,cap,cap],[v,u,0,0])) + adj[u].append(i) + adj[v].append(i+1) + sys.setrecursionlimit(max(sys.getrecursionlimit(), n+50)) + total = 0 + while True: + clock() + levels = [-1]*n + levels[s] = 0 + q = deque([s]) + while q: + u = q.popleft() + for i in adj[u]: + _,v,r,_ = graph[i] + if r and levels[v] == -1: + levels[v] = levels[u]+1 + q.append(v) + if levels[t] == -1: + break + cursor = [0]*n + def augment(u, capacity): + if u == t: + return capacity + while cursor[u] < len(adj[u]): + i = adj[u][cursor[u]] + _,v,r,_ = graph[i] + if r and levels[v] == levels[u]+1: + d = augment(v, min(capacity,r)) + if d: + graph[i][2] -= d + graph[i^1][2] += d + return d + cursor[u] += 1 + return 0 + limit = sum(caps[s,v] for v in range(n)) + while (delta := augment(s,limit)): + clock() + total += delta + lhs = [0]*n + certificate = [] + for u,v,r,c in graph[::2]: + f = c-r + assert 0 <= f <= c + lhs[u] += f + lhs[v] -= f + if f: + certificate.append([u,v,f]) + assert lhs[s] == total == -lhs[t] and all(not lhs[i] for i in range(n) if i not in (s,t)) + cut = [i for i,l in enumerate(levels) if l >= 0] + assert s in cut and t not in cut + inside = set(cut) + assert total == sum(c for (u,v),c in caps.items() if u in inside and v not in inside) + return total, certificate, cut + + +def compile_case(model, pair): + chart, rank, terminal, edges, incident, charts, copies, P, T, prices = model + lo,hi = pair + labels = (lo,hi) + vertices = sorted(charts[lo] + charts[hi]) + var = {v:i for i,v in enumerate(vertices)} + E = sorted(set(i for v in vertices for i in incident[v])) + n = len(vertices) + s,t = n,n+1 + max_finite = max(max(v) for v in prices.values()) + hard = (len(E)+len(vertices)+1)*(2*max_finite+1) + unary = [[0,0] for _ in vertices] + cap = Counter() + old = 0 + + def edge(a,b,owned): + d = rank(a,b,owned) + return hard if d is None else prices[d][0] + + def terminal_cost(v, z): + d = rank(terminal[v],z,False) + return hard if d is None or d == 0 else -prices[d][1] + + for i in E: + a,b,owned = edges[i] + old += edge(chart[a],chart[b],owned) + if a in var and b in var: + cap[var[a],var[b]] += edge(lo,hi,owned) + cap[var[b],var[a]] += edge(hi,lo,owned) + elif a in var: + for bit,f in enumerate(labels): + unary[var[a]][bit] += edge(f,chart[b],owned) + else: + for bit,g in enumerate(labels): + unary[var[b]][bit] += edge(chart[a],g,owned) + for v in vertices: + if v in terminal: + old += terminal_cost(v,chart[v]) + for bit,z in enumerate(labels): + unary[var[v]][bit] += terminal_cost(v,z) + offset = 0 + for i,(a,b) in enumerate(unary): + m = min(a,b) + offset += m + cap[s,i] += b-m + cap[i,t] += a-m + assert all(c>=0 for c in cap.values()) + return vertices,E,old,offset,cap + + +def quote_case(model, scope, pair, changed): + chart, rank, terminal, edges, incident, charts, copies, P, T, prices = model + vertices,E,old,offset,cap=scope + labels=tuple(pair) + assert set(changed) <= set(vertices) + assert all(f in labels and f != chart[v] for v,f in changed.items()) + paid = P.copy() + productive = T.copy() + objective = 0 + for i in E: + a,b,owned = edges[i] + old_r = rank(chart[a],chart[b],owned) + new_r = rank(changed.get(a,chart[a]),changed.get(b,chart[b]),owned) + assert new_r is not None + if old_r: + paid[old_r] -= copies + if new_r: + paid[new_r] += copies + objective += prices[new_r][0] + for v in vertices: + if v in terminal: + old_r = rank(terminal[v],chart[v],False) + new_r = rank(terminal[v],changed.get(v,chart[v]),False) + assert new_r + productive[old_r] -= copies + productive[new_r] += copies + objective -= prices[new_r][1] + final_clock = max(k[0] for k in chart) + upper = sum(q*prices[r][1] for r,q in productive.items())-sum(q*prices[r][0] for r,q in paid.items()) + baseline = sum(q*prices[r][1] for r,q in T.items())-sum(q*prices[r][0] for r,q in P.items()) + assert upper == baseline+copies*(old-objective) + return {'status':'PASS_EXACT_DIRECTED_BINARY_CUT','head':HEAD,'pair':pair, + 'movable_vertices':len(vertices),'changed_vertices':len(changed), + 'directed_whole_upper':str(F(upper,GRID)), + 'signed_paid':dict(+paid),'signed_targets':dict(+productive), + 'rank_surplus':sum(r*(productive[r]-paid[r]) for r in productive.keys()|paid.keys()), + 'event_relabels':sorted((k,f) for (k,r),f in changed.items() if k=end: + raise TimeoutError('independent audit cap') + r=json.loads(args.receipt.read_bytes()) + assert r['head']==HEAD + model=read_model() + checked=[] + unresolved=[] + for row in r['cuts']: + if row['status']!='PASS_EXACT_DIRECTED_BINARY_CUT': + unresolved.append(row['pair']) + continue + clock() + checked.append(verify_case(model,row,clock)) + print(json.dumps({'status':'PASS_INDEPENDENT_FLOW_CUT_AND_DIRECTED_INVOICE','head':HEAD, + 'receipt_sha256':sha256(args.receipt.read_bytes()).hexdigest(),'checks':checked, + 'unresolved':unresolved+r['unvisited']},sort_keys=True,separators=(',',':'))) + + +if __name__=='__main__': + main() diff --git a/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/CALLER.json.gz b/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/CALLER.json.gz new file mode 100644 index 0000000000..290ef7c9c5 Binary files /dev/null and b/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/CALLER.json.gz differ diff --git a/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz b/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz new file mode 100644 index 0000000000..8f4096badd Binary files /dev/null and b/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz differ diff --git a/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/WORD.json.gz b/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/WORD.json.gz new file mode 100644 index 0000000000..077bf48c35 Binary files /dev/null and b/research/p104-owned-move-destination-span/dependencies/round30/complex/source/inputs/WORD.json.gz differ diff --git a/research/p104-owned-move-destination-span/dependencies/round30/complex/source/powers.py b/research/p104-owned-move-destination-span/dependencies/round30/complex/source/powers.py new file mode 100644 index 0000000000..1ac680b880 --- /dev/null +++ b/research/p104-owned-move-destination-span/dependencies/round30/complex/source/powers.py @@ -0,0 +1,177 @@ +"""Directed signed invoice and paired rank-reduction ceilings.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as F +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path +from time import monotonic + +TARGET = F(10018846261809, 2500000000000000) +CLAIMS = F('0.003645372367832'), F('0.003645473221716') +GRID = 10**48 +PINS = { + 'old/inputs/native/WORD.json.gz': '75061d1e4b354e4cf36b690f30ddb2b257ed2f4e86509f87e17bb0f63eca126f', + 'old/inputs/native/RESULT.json': '75f34132b5b12b1a92f13b7a7c47ea3857f1955403090ae06b38dd9cf18aeb49', + 'old/inputs/caller/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'peer/WORD.json.gz': '66bc395b599bc0b805c5061bbbd124e2027ad86645c07abe40d0b472fa1a7a2b', + 'peer/RESULT.json': 'acd6ef312fc1d1b8a94919b345667fb17a8a38939db17976ba6a21c7d4de9eb9', +} + + +def load(old, peer): + roots = {'old':old, 'peer':peer} + out = {} + for name, digest in PINS.items(): + label, path = name.split('/', 1) + raw = (roots[label] / path).read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError(f'Pinned SHA-256 mismatch: {name}') + out[name] = json.loads(gzip.decompress(raw) if name.endswith('.gz') else raw) + return list(out.values()) + + +def invoice(word, caller): + ranks = list(map(len, word['frames'])) + main = set(word['live']) | {i+112 for i in word['live']} | set(word['hosted']['X2'] + word['hosted']['Y2']) + assert len(main) == 400 and word['public'] == 1501 and len(word['program']) == 76444 + paid, target = Counter(), Counter() + for op, role, *args in word['program']: + if op == 'MOVE': + src, dst, owned = args + assert owned == (role >= word['public']) and ranks[src] != ranks[dst] + paid[abs(ranks[src]-ranks[dst])] += 1 + for role, (src, dst) in enumerate(zip(word['initial'], word['final'], strict=True)): + if role not in main: + assert ranks[dst] > ranks[src] + target[ranks[dst]-ranks[src]] += 1 + stages = [event[1] for event in caller['events'] if event[0] == 'J'] + assert stages == list(range(1, 18)) + copies = len(stages) + P = Counter({rank:n*copies for rank,n in paid.items()}) + T = Counter({rank:n*copies for rank,n in target.items()}) + for spec in caller['types'].values(): + for sign, offset, *bits in spec['diagonal']: + assert sign == -1 and offset == 0 and len(bits) == copies and set(bits) <= {0, 1} + T[1+8*sum(bits)] += len(spec['ports']) + for kind, op, *args in (event for event in caller['events'] if event[0] != 'J'): + n = len(caller['types'][kind]['ports']) + if op == 'QUERY': + P[1] += n + elif op in ('IDLE_ONE','IDLE_ODD'): + P[8*len(args[1])+int(op=='IDLE_ODD')] += n + assert sum(P.values()) == 110553 and sum(T.values()) == 22461 + assert sum(r*(T[r]-P[r]) for r in T.keys()|P.keys()) == 1424 + return paid, target, P, T, copies + + +def round_interval(a, b): + a, b = a*GRID, b*GRID + return F(a.numerator//a.denominator, GRID), F(-((-b.numerator)//b.denominator), GRID) + + +@cache +def log_unit(x): + y = (x-1)/(x+1) + p = sum((2*y**j/j for j in range(1, 111, 2)), F(0)) + return round_interval(p, p+2*y**111/(111*(1-y*y))) + + +@cache +def power(rank, k): + e = rank.bit_length()-1 + lo,hi = [q+e*d for q,d in zip(log_unit(F(rank, 2**e)),log_unit(F(2)),strict=True)] + + def exp_negative(x, n): + term = total = F(1) + assert 0 <= x < 1 + for i in range(1,n+1): + term *= -x/i + total += term + return total + + return round_interval(rank*exp_negative(k*hi, 39), rank*exp_negative(k*lo, 40)) + + +def moment(P, T, k): + lower = upper = F(0) + for r in P.keys()|T.keys(): + n = T[r]-P[r] + lo,hi = power(r,k) + if n < 0: + lo,hi = hi,lo + lower += n*lo + upper += n*hi + return lower,upper + + +def slope(rank): + a,b = power(rank,TARGET) + c,d = power(rank-1,TARGET) + return a-d,b-c + + +def stock(paid, target, copies, baseline, paid_ranks, target_ranks): + eligible_paid = sorted(((slope(r)[1],r) for r in paid_ranks for _ in range(paid[r])),reverse=True) + eligible_target = sorted((slope(r)[0],r) for r in target_ranks for _ in range(target[r])) + price = F(0) + use_paid, use_target = Counter(), Counter() + for (upper,p),(lower,t) in zip(eligible_paid,eligible_target): + if upper <= lower: + break + price += upper-lower + use_paid[p] += 1 + use_target[t] += 1 + saving = copies*price + return {'eligible_paid':len(eligible_paid), 'eligible_targets':len(eligible_target), + 'selected_paid':dict(use_paid),'selected_targets':dict(use_target), + 'optimistic_pairs':sum(use_paid.values()), 'signed_saving_upper':str(saving), + 'signed_target_net_upper':str(baseline+saving)} + + +def run(old, peer, seconds): + deadline = monotonic()+seconds + before, before_receipt, caller, after, after_receipt = load(old,peer) + previous, next_ = invoice(before,caller), invoice(after,caller) + assert next_[4] == previous[4] == 17 + delta = lambda a,b:{r:a[r]-b[r] for r in a.keys()|b.keys() if a[r]!=b[r]} + assert delta(next_[0],previous[0]) == {4:1,5:-1} + assert delta(next_[1],previous[1]) == {8:1,9:-1} + result = {} + for name, (p,t,P,T,n), receipt, claim in zip(('7244','7274'),(previous,next_), + (before_receipt,after_receipt),CLAIMS,strict=True): + frozen = receipt['price']['after'] + assert P == {int(r):v for r,v in frozen['P'].items()} + assert T == {int(r):v for r,v in frozen['T'].items()} + # Known-good signed prices and a missing-call mutation. + removed_call = P.copy() + removed_call[1] -= 1 + assert removed_call != {int(r):v for r,v in frozen['P'].items()} + a,b = map(F,receipt['price']['price']['independent_raw_bracket']) + low, high = moment(P,T,a), moment(P,T,b) + assert low[0]>0 and high[1]<0 and a>claim + deficit = moment(P,T,TARGET) + scopes = {label:stock(p,t,n,deficit[1],pr,tr) for label,pr,tr in ( + ('same_delta',{5},{9}),('rank9_target',set(p)-{1},{9}), + ('any_one_step',set(p)-{1},set(t)-{1}))} + result[name]={'native_paid':dict(p),'native_target':dict(t),'paid':dict(P),'target':dict(T), + 'crossing_interval':[str(a),str(b)],'crossing_sign_controls':[str(low[0]),str(high[1])], + 'claim':str(claim),'target_raw_interval':list(map(str,deficit)),'scopes':scopes} + assert F(result['7244']['crossing_interval'][1]) < F(result['7274']['crossing_interval'][0]) + assert moment(previous[2],previous[3],CLAIMS[1])[1]<0 + assert monotonic() 1: + return {k: v // common for k, v in row.items()} + return row + + +def add_row(basis, raw): + # Copy before elimination because the literal row is still in use. + row = raw.copy() + while row: + pivot = max(row) + known = basis.get(pivot) + if known is None: + basis[pivot] = primitive(row) + return True + p, q = row[pivot], known[pivot] + common = gcd(p, q) + row = { + key: value for key in row.keys() | known.keys() + if (value := (q//common)*row.get(key, 0) - (p//common)*known.get(key, 0)) + } + row = primitive(row) + return False + + +def ranks(rows, target): + basis = {} + # Each stored denominator multiplies its entire row by a nonzero unit of Q. + for _, numerators in rows: + add_row(basis, numerators) + old = len(basis) + add_row(basis, target[1]) + return old, len(basis) + + +def observer(records): + def visit(index, role, source, destination, paid_rank, charts, rows, owned): + donors = [ + rows[r] for r in range(len(rows)) if r != role and charts[r] == destination and rows[r][1] + ] + if len(donors) < 3: + return + old, augmented = ranks(donors, rows[role]) + records.append({ + "literal_index": index, "role": role, "from": source, "to": destination, + "paid_rank": paid_rank, "donors": len(donors), + "donor_rank": old, "augmented_rank": augmented, "in_span": old == augmented, + }) + return visit + + +def controls(): + bank = [(3, {0:1, 1:1}), (5, {0:1, 1:-1}), (7, {2:2})] + target = (2, {0:1, 2:-1}) + assert ranks(bank, target) == (3,3) + assert all(ranks([bank[j] for j in range(3) if j != i], target) == (2,3) for i in range(3)) + dependent = (11, {0:-6, 1:-6}) + assert ranks([*bank, dependent], target) == (3,3) + assert ranks(bank, (2, {0:1, 2:-1, 3:1})) == (3,4) + return {"three_donor_required": True, "dependent_extra_donor": True, "outside_coordinate_rejected": True} + + +def main(): + start = time.monotonic() + if not __debug__: + raise RuntimeError("Run with assertions enabled") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--word", required=True, type=Path) + parser.add_argument("--cap", default=22, type=float) + args = parser.parse_args() + assert 0 < args.cap <= 22 + core = Path(__file__).resolve().with_name("replay_core.py") + checked(core, CORE) + audit = runpy.run_path(str(core))["audit"] + word = json.loads(gzip.decompress(checked(args.word, WORD))) + records = [] + report = audit(word, start, args.cap, observer(records)) + payload = { + **report, "scientific_head": HEAD, "word_sha256": WORD, "replay_core_sha256": CORE, + "banks_tested": len(records), "donors": sum(r["donors"] for r in records), + "matches": sum(r["in_span"] for r in records), "records": records, "controls": controls(), + } + if report["scope_exhausted"]: + assert (report["paid_owned_moves"], payload["banks_tested"], payload["donors"]) == (47,39,411) + print(json.dumps(payload, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-move-destination-span/dependencies/round41/independent/replay_core.py b/research/p104-owned-move-destination-span/dependencies/round41/independent/replay_core.py new file mode 100644 index 0000000000..0a450da01e --- /dev/null +++ b/research/p104-owned-move-destination-span/dependencies/round41/independent/replay_core.py @@ -0,0 +1,182 @@ +"""Audit normalized owned-MOVE inputs using exact signed rational rows.""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +from hashlib import sha256 +import json +from math import gcd +from pathlib import Path +import time + +SHA = "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +OWNED_PAID = {1: 20, 2: 9, 3: 2, 4: 13, 5: 2, 6: 1} + + +def reduced(denominator, numerators): + if not numerators: + return 1, {} + factor = denominator + for n in numerators.values(): + factor = gcd(factor, n) + if factor == 1: + return denominator, numerators + return denominator // factor, {k: n // factor for k, n in numerators.items()} + + +def scaled(row, q): + denominator, numerators = row + return reduced(denominator * q.denominator, {k: q.numerator * n for k, n in numerators.items()}) + + +def plus(destination, source, q): + denominator, numerators = destination + s_den, s_num = source + right_denominator = s_den * q.denominator + common_factor = gcd(denominator, right_denominator) + left_scale = right_denominator // common_factor + right_scale = denominator // common_factor * q.numerator + sums = {k: left_scale * n for k, n in numerators.items()} if left_scale != 1 else numerators + for k, n in s_num.items(): + value = sums.get(k, 0) + right_scale * n + if value: + sums[k] = value + else: + sums.pop(k, None) + return reduced(denominator * left_scale, sums) + + +def frame_space(rows): + space = {0} + for row in rows: + space |= {v ^ row for v in space} + assert len(space) == 1 << len(rows) + return space + + +def audit(word, start, seconds, visit_owned_move=None): + public = word["public"] + roles = public + word["owned_fields"] + events = word["program"] + frames = [frame_space(f) for f in word["frames"]] + charts = word["initial"] + [None] * (roles - public) + rows = [(1, {r: 1}) for r in range(public)] + [None] * (roles - public) + fresh = set() + live = set() + owned_paid = Counter() + nonzero_clears = owned_copies = lifetimes = peak = visited = 0 + found, token_hits = [], [] + cap = start + seconds + for index, event in enumerate(events): + if index % 64 == 0 and time.monotonic() >= cap: + break + visited = index + 1 + op, d, *args = event + if op == "INIT": + frame, = args + assert d >= public and charts[d] is None and rows[d] is None and d not in live + rows[d], charts[d] = (1, {}), frame + fresh.add(d) + live.add(d) + lifetimes += 1 + peak = max(peak, len(live)) + elif op == "CLEAR": + frame, = args + assert d in live and charts[d] == frame + nonzero_clears += bool(rows[d][1]) + fresh.discard(d) + live.remove(d) + rows[d], charts[d] = None, None + elif op == "MOVE": + source, target, owned = args + assert charts[d] == source and owned == (d in live) == (d >= public) + assert frames[source] < frames[target] or (owned and frames[target] < frames[source]) + if owned: + rank = abs(len(word["frames"][target]) - len(word["frames"][source])) + if visit_owned_move is not None: + visit_owned_move(index, d, source, target, rank, charts, rows, live) + owned_paid[rank] += 1 + if not rows[d][1]: + found.append({"literal_index": index, "role": d, "from": source, "to": target, "rank": rank}) + if d in fresh: + assert not rows[d][1] + token_hits.append(index) + fresh.discard(d) + charts[d] = target + elif op == "SCALE": + coefficient, frame = args + q = Fraction(coefficient) + assert charts[d] == frame and q + rows[d] = scaled(rows[d], q) + else: + s, coefficient, frame = args + q = Fraction(coefficient) + assert op in ("ADD", "COPY") and d != s and charts[d] == frame == charts[s] and q + if op == "COPY": + assert d in live and d in fresh and not rows[d][1] + rows[d] = scaled(rows[s], q) + owned_copies += 1 + else: + rows[d] = plus(rows[d], rows[s], q) + fresh.discard(d) + first_unvisited = None if visited == len(events) else visited + remaining_move = next((i for i in range(visited, len(events)) if events[i][0] == "MOVE" and events[i][-1]), None) + if first_unvisited is None: + assert not live and not fresh and charts == word["final"] + [None] * (roles - public) + return { + "scope_exhausted": first_unvisited is None, + "literal_events": len(events), "literal_events_visited": visited, + "first_unvisited_literal_index": first_unvisited, + "first_unvisited_owned_move_index": remaining_move, + "paid_owned_histogram": owned_paid, "paid_owned_moves": sum(owned_paid.values()), + "exact_zero_moves": found, "fresh_zero_moves": len(token_hits), + "owned_lifetimes": lifetimes, "peak_owned": peak, "checked_copies": owned_copies, + "nonzero_owned_clears": nonzero_clears, + } + + +def control(): + # Same public input reaches an owned role with two different signed rational paths. + word = { + "public": 1, "owned_fields": 1, "initial": [0], "final": [0], "frames": [[], [1]], + "program": [ + ["INIT", 1, 0], ["COPY", 1, 0, "2/3", 0], + ["ADD", 1, 0, "-1/2", 0], ["ADD", 1, 0, "-1/6", 0], + ["MOVE", 1, 0, 1, True], ["CLEAR", 1, 1], + ], + } + observed = audit(word, time.monotonic(), 1) + assert observed["scope_exhausted"] + assert observed["exact_zero_moves"] == [{"literal_index": 4, "role": 1, "from": 0, "to": 1, "rank": 1}] + assert observed["fresh_zero_moves"] == 0 + word["program"][3][3] = "1/6" + changed = audit(word, time.monotonic(), 1) + assert changed["scope_exhausted"] and not changed["exact_zero_moves"] + return {"cancellation_detected": True, "changed_sign_rejected": True, "test_owned_move_index": 4} + + + +def main(): + if not __debug__: + raise RuntimeError("Run with assertions enabled") + start = time.monotonic() + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--word", required=True, type=Path) + parser.add_argument("--cap", default=22.0, type=float) + args = parser.parse_args() + assert 0 < args.cap <= 22.0 + raw = args.word.read_bytes() + if sha256(raw).hexdigest() != SHA: + raise ValueError("Unexpected compressed word SHA-256") + result = audit(json.loads(gzip.decompress(raw)), start, args.cap) + if result["scope_exhausted"]: + assert result["paid_owned_histogram"] == OWNED_PAID + assert tuple(result[k] for k in ("owned_lifetimes", "peak_owned", "checked_copies")) == (70, 49, 1) + print(json.dumps({"scientific_head": HEAD, "compressed_word_sha256": SHA, + **result, "control": control()}, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-move-destination-span/dependencies/round41/independent/replay_pairs.py b/research/p104-owned-move-destination-span/dependencies/round41/independent/replay_pairs.py new file mode 100644 index 0000000000..537ebb93bc --- /dev/null +++ b/research/p104-owned-move-destination-span/dependencies/round41/independent/replay_pairs.py @@ -0,0 +1,123 @@ +"""Independent exact determinant audit of #7277 two-donor opportunities.""" + +import argparse +from fractions import Fraction +import gzip +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +import runpy +import time + +WORD = "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +CORE = "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" + + +def checked(path, digest): + raw = path.read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError(f"Unexpected SHA-256 for {path.name}") + return raw + + +def span(target, first, second): + dt, z = target + dx, x = first + dy, y = second + assert x and y + i = min(x) + xi, yi, zi = x[i], y.get(i, 0), z.get(i, 0) + donor_support = x.keys() | y.keys() + pivot = next(((j, d) for j in sorted(donor_support) + if (d := xi*y.get(j, 0) - x.get(j, 0)*yi)), None) + if pivot is None: + # Since xi is nonzero, all minors involving i vanish iff y is proportional to x. + if any(xi*z.get(k, 0) != zi*x.get(k, 0) for k in x.keys() | z.keys()): + return 1, None + y_over_x = Fraction(yi*dx, xi*dy) + z_over_x = Fraction(zi*dx, xi*dt) + b = Fraction(1) + if z_over_x == y_over_x: + b = Fraction(2) + return 1, (z_over_x-b*y_over_x, b) + j, d = pivot + zj, yj, xj = z.get(j, 0), y.get(j, 0), x.get(j, 0) + a_num, b_num = zi*yj-zj*yi, xi*zj-xj*zi + if any(d*z.get(k, 0) != a_num*x.get(k, 0)+b_num*y.get(k, 0) + for k in donor_support | z.keys()): + return 2, None + return 2, (Fraction(a_num*dx, d*dt), Fraction(b_num*dy, d*dt)) + + +def observer(records): + def visit(index, role, source, dest, paid_rank, charts, rows, live): + available = [r for r, chart in enumerate(charts) if r != role and chart == dest] + donors = [r for r in available if rows[r][1]] + pairs = dependent = 0 + hits = [] + for a, b in combinations(donors, 2): + pairs += 1 + rank, coeff = span(rows[role], rows[a], rows[b]) + dependent += rank == 1 + if coeff is not None: + hits.append({"donors": [a,b], "donor_rank": rank, "coefficients": list(map(str, coeff))}) + records.append({ + "literal_index": index, "role": role, "from": source, "to": dest, "paid_rank": paid_rank, + "destination_live_roles": len(available), "nonzero_donors": len(donors), + "zero_donors": len(available)-len(donors), "pairs": pairs, + "dependent_pairs": dependent, "matches": hits, + }) + return visit + + +def controls(): + first = (3, {0:2, 1:-1, 2:1}) + second = (5, {0:1, 1:2, 2:-2}) + target = (15, {0:7, 1:-11, 2:11}) + assert span(target, first, second) == (2, (Fraction(1), Fraction(-1))) + wrong = (15, {0:7, 1:-11, 2:-11}) + assert span(wrong, first, second) == (2, None) + dependent = (3, {0:-4, 1:2, 2:-2}) + assert span(target, first, dependent) == (1, None) + assert span(first, first, dependent) == (1, (Fraction(3), Fraction(1))) + return {"positive_signed_coefficients": ["1", "-1"], + "same_support_sign_mutation_rejected": True, "dependent_positive_and_negative": True} + + +def main(): + start = time.monotonic() + if not __debug__: + raise RuntimeError("Run with assertions enabled") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--word", required=True, type=Path) + parser.add_argument("--cap", default=26, type=float) + args = parser.parse_args() + assert 0 < args.cap <= 26 + core = Path(__file__).resolve().with_name("replay_core.py") + checked(core, CORE) + replay = runpy.run_path(str(core))["audit"] + word = json.loads(gzip.decompress(checked(args.word, WORD))) + records = [] + result = replay(word, start, args.cap, observer(records)) + assert len(records) == result["paid_owned_moves"] + payload = { + **result, "scientific_head": HEAD, "word_sha256": WORD, "replay_core_sha256": CORE, + "sites_with_pairs": sum(r["pairs"] > 0 for r in records), + "two_donor_pairs": sum(r["pairs"] for r in records), + "rank_one_pairs": sum(r["dependent_pairs"] for r in records), + "matches": sum(len(r["matches"]) for r in records), + "fallback_sites_with_three_or_more_donors": sum(r["nonzero_donors"] >= 3 for r in records), + "fallback_whole_rank_upper_before_new_work": 17*sum( + r["paid_rank"] for r in records if r["nonzero_donors"] >= 3), + "fallback_bound_complete": result["scope_exhausted"], + "controls": controls(), "records": records, + } + if result["scope_exhausted"]: + assert (len(records), payload["sites_with_pairs"], payload["two_donor_pairs"]) == (47, 44, 2767) + print(json.dumps(payload, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-move-destination-span/dependencies/round41/lead/r41-price-support/PRICE.json b/research/p104-owned-move-destination-span/dependencies/round41/lead/r41-price-support/PRICE.json new file mode 100644 index 0000000000..7798e08ba8 --- /dev/null +++ b/research/p104-owned-move-destination-span/dependencies/round41/lead/r41-price-support/PRICE.json @@ -0,0 +1,502 @@ +{ + "baseline_interval": [ + "-1002247197758299781/500000000000000000000000000000000000000000000000", + "-2004494395516543389/1000000000000000000000000000000000000000000000000" + ], + "cap": 47, + "copies": 17, + "crossing_upper": "91141748217473298207420876011401/25000000000000000000000000000000000", + "exact_optimistic_single_site_by_rank": { + "1": { + "complete_margin_interval": [ + "8499999999999999999999999999998997752802241700219/500000000000000000000000000000000000000000000000", + "16999999999999999999999999999997995505604483456611/1000000000000000000000000000000000000000000000000" + ], + "removed_rank_histogram_per_copy": { + "1": 1 + }, + "saving_interval": [ + "17", + "17" + ] + }, + "2": { + "complete_margin_interval": [ + "6782838189298859181046507642853085205894263256029/200000000000000000000000000000000000000000000000", + "33914190946494295905232538214265426029471316336301/1000000000000000000000000000000000000000000000000" + ], + "removed_rank_histogram_per_copy": { + "2": 1 + }, + "saving_interval": [ + "3391419094649429590523253821426743052386683287969/100000000000000000000000000000000000000000000000", + "33914190946494295905232538214267430523866832879707/1000000000000000000000000000000000000000000000000" + ] + }, + "3": { + "complete_margin_interval": [ + "10159228888878758214179089584042859164260518392599/200000000000000000000000000000000000000000000000", + "50796144444393791070895447920214295821302592019151/1000000000000000000000000000000000000000000000000" + ], + "removed_rank_histogram_per_copy": { + "3": 1 + }, + "saving_interval": [ + "2539807222219689553544772396010815015784905428127/50000000000000000000000000000000000000000000000", + "50796144444393791070895447920216300315698108562557/1000000000000000000000000000000000000000000000000" + ] + }, + "4": { + "complete_margin_interval": [ + "8457149614377026958411829202233166019006501911113/125000000000000000000000000000000000000000000000", + "33828598457508107833647316808932664076026007672547/500000000000000000000000000000000000000000000000" + ], + "removed_rank_histogram_per_copy": { + "4": 1 + }, + "saving_interval": [ + "33828598457508107833647316808933666323223765944233/500000000000000000000000000000000000000000000000", + "67657196915016215667294633617867332646447531888483/1000000000000000000000000000000000000000000000000" + ] + }, + "5": { + "complete_margin_interval": [ + "2112568113860389463634373813701686237622706547569/25000000000000000000000000000000000000000000000", + "21125681138603894636343738137016862376227065489729/250000000000000000000000000000000000000000000000" + ], + "removed_rank_histogram_per_copy": { + "5": 1 + }, + "saving_interval": [ + "16900544910883115709074990509613890799860755700461/200000000000000000000000000000000000000000000000", + "42251362277207789272687476274034726999651889251161/500000000000000000000000000000000000000000000000" + ] + }, + "6": { + "complete_margin_interval": [ + "101335890707816260929155437636642299101243550342361/1000000000000000000000000000000000000000000000000", + "101335890707816260929155437636642299101243550398551/1000000000000000000000000000000000000000000000000" + ], + "removed_rank_histogram_per_copy": { + "6": 1 + }, + "saving_interval": [ + "101335890707816260929155437636644303595639066941923/1000000000000000000000000000000000000000000000000", + "5066794535390813046457771881832215179781953347097/50000000000000000000000000000000000000000000000" + ] + } + }, + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "original_paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5882, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "original_productive": { + "1": 306, + "2": 357, + "3": 799, + "4": 3808, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10905, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "per_site_local_costs": { + "add_CLEAR": 1, + "add_COPY": 1, + "add_INIT": 1, + "net_literal_events": 2, + "new_owner_slots": 0, + "remove_MOVE": 1 + }, + "pins": { + "complex/audit.py": "67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb", + "complex/source/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "complex/source/inputs/EARLY-RESULT.json": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "complex/source/powers.py": "c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee" + }, + "price_assumption": "Grant all extra costs free only for the deletion upper.", + "scope_size": 47, + "seconds_cap": 90, + "sites": [ + { + "clock": 30527, + "destination": 1090, + "rank": 4, + "role": 1510, + "source": 477 + }, + { + "clock": 30535, + "destination": 470, + "rank": 1, + "role": 1520, + "source": 1090 + }, + { + "clock": 30549, + "destination": 601, + "rank": 2, + "role": 1521, + "source": 470 + }, + { + "clock": 30579, + "destination": 470, + "rank": 2, + "role": 1547, + "source": 601 + }, + { + "clock": 30591, + "destination": 1090, + "rank": 1, + "role": 1546, + "source": 470 + }, + { + "clock": 32937, + "destination": 1091, + "rank": 4, + "role": 1529, + "source": 267 + }, + { + "clock": 33123, + "destination": 541, + "rank": 1, + "role": 1528, + "source": 543 + }, + { + "clock": 33131, + "destination": 260, + "rank": 1, + "role": 1514, + "source": 1091 + }, + { + "clock": 33138, + "destination": 534, + "rank": 1, + "role": 1502, + "source": 541 + }, + { + "clock": 33140, + "destination": 117, + "rank": 1, + "role": 1502, + "source": 534 + }, + { + "clock": 33147, + "destination": 594, + "rank": 4, + "role": 1502, + "source": 117 + }, + { + "clock": 34512, + "destination": 243, + "rank": 4, + "role": 1513, + "source": 517 + }, + { + "clock": 34516, + "destination": 431, + "rank": 1, + "role": 1518, + "source": 243 + }, + { + "clock": 35138, + "destination": 260, + "rank": 2, + "role": 1541, + "source": 599 + }, + { + "clock": 35429, + "destination": 600, + "rank": 2, + "role": 1519, + "source": 431 + }, + { + "clock": 35434, + "destination": 431, + "rank": 2, + "role": 1545, + "source": 600 + }, + { + "clock": 35438, + "destination": 243, + "rank": 1, + "role": 1544, + "source": 431 + }, + { + "clock": 36307, + "destination": 240, + "rank": 4, + "role": 1512, + "source": 518 + }, + { + "clock": 36311, + "destination": 394, + "rank": 1, + "role": 1516, + "source": 240 + }, + { + "clock": 36319, + "destination": 598, + "rank": 2, + "role": 1517, + "source": 394 + }, + { + "clock": 36329, + "destination": 394, + "rank": 2, + "role": 1543, + "source": 598 + }, + { + "clock": 36341, + "destination": 240, + "rank": 1, + "role": 1542, + "source": 394 + }, + { + "clock": 39532, + "destination": 517, + "rank": 4, + "role": 1539, + "source": 243 + }, + { + "clock": 39559, + "destination": 518, + "rank": 4, + "role": 1538, + "source": 240 + }, + { + "clock": 39705, + "destination": 529, + "rank": 1, + "role": 1526, + "source": 531 + }, + { + "clock": 39763, + "destination": 531, + "rank": 1, + "role": 1548, + "source": 529 + }, + { + "clock": 39792, + "destination": 520, + "rank": 1, + "role": 1503, + "source": 529 + }, + { + "clock": 39798, + "destination": 595, + "rank": 5, + "role": 1503, + "source": 520 + }, + { + "clock": 39831, + "destination": 599, + "rank": 2, + "role": 1515, + "source": 260 + }, + { + "clock": 39853, + "destination": 520, + "rank": 5, + "role": 1532, + "source": 595 + }, + { + "clock": 39862, + "destination": 529, + "rank": 1, + "role": 1532, + "source": 520 + }, + { + "clock": 40518, + "destination": 559, + "rank": 1, + "role": 1549, + "source": 549 + }, + { + "clock": 40536, + "destination": 549, + "rank": 1, + "role": 1527, + "source": 559 + }, + { + "clock": 40543, + "destination": 115, + "rank": 2, + "role": 1501, + "source": 549 + }, + { + "clock": 40547, + "destination": 593, + "rank": 4, + "role": 1501, + "source": 115 + }, + { + "clock": 41474, + "destination": 477, + "rank": 4, + "role": 1537, + "source": 1090 + }, + { + "clock": 41629, + "destination": 549, + "rank": 6, + "role": 1530, + "source": 593 + }, + { + "clock": 41988, + "destination": 117, + "rank": 4, + "role": 1531, + "source": 594 + }, + { + "clock": 42460, + "destination": 1031, + "rank": 3, + "role": 1504, + "source": 591 + }, + { + "clock": 42465, + "destination": 597, + "rank": 4, + "role": 1504, + "source": 1031 + }, + { + "clock": 42470, + "destination": 1031, + "rank": 4, + "role": 1533, + "source": 597 + }, + { + "clock": 42483, + "destination": 591, + "rank": 3, + "role": 1533, + "source": 1031 + }, + { + "clock": 44249, + "destination": 543, + "rank": 1, + "role": 1550, + "source": 541 + }, + { + "clock": 44256, + "destination": 534, + "rank": 1, + "role": 1531, + "source": 117 + }, + { + "clock": 44258, + "destination": 541, + "rank": 1, + "role": 1531, + "source": 534 + }, + { + "clock": 45607, + "destination": 267, + "rank": 4, + "role": 1551, + "source": 1091 + }, + { + "clock": 45625, + "destination": 1091, + "rank": 1, + "role": 1540, + "source": 260 + } + ], + "unresolved_costs": [ + "ordinary chart volume and coefficient tariff", + "dirty complement and restoration", + "signed phase", + "lifetime, peak tape and recovery", + "full caller and outer bounds" + ], + "whole_stock_optimistic_upper": { + "complete_margin_interval": [ + "94835245355954723349180965976694800342493336746977/50000000000000000000000000000000000000000000000", + "189670490711909446698361931953389600684986673499573/100000000000000000000000000000000000000000000000" + ], + "removed_rank_histogram_per_copy": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "saving_interval": [ + "1896704907119094466983619319533898011344262251538881/1000000000000000000000000000000000000000000000000", + "94835245355954723349180965976694900567213112576967/50000000000000000000000000000000000000000000000" + ] + } +} diff --git a/research/p104-owned-move-destination-span/dependencies/round41/lead/r41-price-support/SUPPORT.json b/research/p104-owned-move-destination-span/dependencies/round41/lead/r41-price-support/SUPPORT.json new file mode 100644 index 0000000000..a9e2181a76 --- /dev/null +++ b/research/p104-owned-move-destination-span/dependencies/round41/lead/r41-price-support/SUPPORT.json @@ -0,0 +1,649 @@ +{ + "controls": [ + "negative_signed_proportional_donor", + "partial_coefficient_match_rejected", + "disjoint_or_zero_support_rejected", + "donor_must_be_live_in_destination_chart" + ], + "first_unvisited_clock": null, + "full_tape_exhausted": true, + "gate": "Any donor remains provisional until fully charged, literal signed, restored and independently replayed.", + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "original_COPY_guards_checked": 1, + "pins": { + "complex/audit.py": "67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb", + "complex/source/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "complex/source/inputs/EARLY-RESULT.json": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "complex/source/powers.py": "c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee" + }, + "price_sha256": "1efe8b52e02a8db0ac6a04cdf6b943e515badee5fc0b7bea6ea3fe4a30fd1d01", + "rows": [ + { + "clock": 30527, + "destination": 1090, + "live_other_roles": 25, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "10ce85c1d2044e7749783212165582fff5df1bfd512fd431a9f7c2afc3a262fc", + "nonzero_peer_rows": 25, + "role": 1510, + "row_support_size": 139, + "source": 477 + }, + { + "clock": 30535, + "destination": 470, + "live_other_roles": 3, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "4374ab05f4960e4298bdf553cc2e0ca3186c293080a5d6aad88d65525874ee83", + "nonzero_peer_rows": 2, + "role": 1520, + "row_support_size": 179, + "source": 1090 + }, + { + "clock": 30549, + "destination": 601, + "live_other_roles": 3, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "f9b3e33785f25af3d32a83fa4db96119abcf2a43004de425673c6917ea5c06f7", + "nonzero_peer_rows": 3, + "role": 1521, + "row_support_size": 179, + "source": 470 + }, + { + "clock": 30579, + "destination": 470, + "live_other_roles": 7, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "4c4b1d61cec402189bd496ef5e52db778f07797e6df5854a380f60d208635a5f", + "nonzero_peer_rows": 5, + "role": 1547, + "row_support_size": 257, + "source": 601 + }, + { + "clock": 30591, + "destination": 1090, + "live_other_roles": 27, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "2a9279d69ba75aaca6b4bd9bd93a7b5ec2268304c90db5ad06d1958d7dde7307", + "nonzero_peer_rows": 26, + "role": 1546, + "row_support_size": 289, + "source": 470 + }, + { + "clock": 32937, + "destination": 1091, + "live_other_roles": 12, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "e944a0197f2814c268dce71a41af984bd2e34e1481a760695dd132309dbe245f", + "nonzero_peer_rows": 12, + "role": 1529, + "row_support_size": 110, + "source": 267 + }, + { + "clock": 33123, + "destination": 541, + "live_other_roles": 7, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "89efb6aa64652707a26ec78f00365cb863bc683026a5cdcbb82c9cf041a48cef", + "nonzero_peer_rows": 7, + "role": 1528, + "row_support_size": 118, + "source": 543 + }, + { + "clock": 33131, + "destination": 260, + "live_other_roles": 9, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "ee9c967004b4b4b30e579d3e582300f9a3610437f6c824d170ba2ef2f90e55f9", + "nonzero_peer_rows": 8, + "role": 1514, + "row_support_size": 124, + "source": 1091 + }, + { + "clock": 33138, + "destination": 534, + "live_other_roles": 2, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "22f2a8fc0a0761be19e83157dab8c12c602220305f039fb617edb90ce1f43c19", + "nonzero_peer_rows": 2, + "role": 1502, + "row_support_size": 184, + "source": 541 + }, + { + "clock": 33140, + "destination": 117, + "live_other_roles": 14, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "22f2a8fc0a0761be19e83157dab8c12c602220305f039fb617edb90ce1f43c19", + "nonzero_peer_rows": 14, + "role": 1502, + "row_support_size": 184, + "source": 534 + }, + { + "clock": 33147, + "destination": 594, + "live_other_roles": 4, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "22f2a8fc0a0761be19e83157dab8c12c602220305f039fb617edb90ce1f43c19", + "nonzero_peer_rows": 4, + "role": 1502, + "row_support_size": 184, + "source": 117 + }, + { + "clock": 34512, + "destination": 243, + "live_other_roles": 12, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "e348fd232ae9fd226f06671685f62433a1ed4c9f2c36d0604c0b8cab0e22e9f3", + "nonzero_peer_rows": 12, + "role": 1513, + "row_support_size": 179, + "source": 517 + }, + { + "clock": 34516, + "destination": 431, + "live_other_roles": 5, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "f269cab88b84440518e16f8af39014ae0674ca25beb30fc16a7cfa70e0375422", + "nonzero_peer_rows": 4, + "role": 1518, + "row_support_size": 165, + "source": 243 + }, + { + "clock": 35138, + "destination": 260, + "live_other_roles": 9, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "75b0ec19a64d48d417b6c52b7f15cc33d9478c02750e20dd631c441dbf226d9b", + "nonzero_peer_rows": 9, + "role": 1541, + "row_support_size": 126, + "source": 599 + }, + { + "clock": 35429, + "destination": 600, + "live_other_roles": 4, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "c73463d29efb12334e4f73c0106cde7cf0a21d98f116aa9beb3fbdafc4c06da6", + "nonzero_peer_rows": 4, + "role": 1519, + "row_support_size": 165, + "source": 431 + }, + { + "clock": 35434, + "destination": 431, + "live_other_roles": 6, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "f371831d5863b5d0504e33819d9f0a9b5046a36c56a278d41c2cd0da4437e930", + "nonzero_peer_rows": 5, + "role": 1545, + "row_support_size": 239, + "source": 600 + }, + { + "clock": 35438, + "destination": 243, + "live_other_roles": 22, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "c4ad2dbe967aa2a6249f67fe8c62218464a0740e3d247e8295d99fa8d9b531dd", + "nonzero_peer_rows": 21, + "role": 1544, + "row_support_size": 247, + "source": 431 + }, + { + "clock": 36307, + "destination": 240, + "live_other_roles": 19, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "5f0446c9cf8163ae41879fa3663c14fa31296f3bde84a2a5cc57fdb41d042c33", + "nonzero_peer_rows": 18, + "role": 1512, + "row_support_size": 127, + "source": 518 + }, + { + "clock": 36311, + "destination": 394, + "live_other_roles": 5, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "0f8e7d1df812662ec813e1e9992e78205fb8d9bae1f763932ac92193db4c85f0", + "nonzero_peer_rows": 2, + "role": 1516, + "row_support_size": 137, + "source": 240 + }, + { + "clock": 36319, + "destination": 598, + "live_other_roles": 3, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "a708f70066bc3315b88e37112711d30188aba32e42323652f5918fe0baf0dc09", + "nonzero_peer_rows": 3, + "role": 1517, + "row_support_size": 137, + "source": 394 + }, + { + "clock": 36329, + "destination": 394, + "live_other_roles": 7, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "dd260d964a96d25a5080c9633699b1f7eca4dc8287268ff769542d842dab675e", + "nonzero_peer_rows": 5, + "role": 1543, + "row_support_size": 260, + "source": 598 + }, + { + "clock": 36341, + "destination": 240, + "live_other_roles": 20, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "1aa2f38b66a1f6dd29a1d3893dcd8facf4d5a9b129e6b1820dd7f8b61e30d56e", + "nonzero_peer_rows": 19, + "role": 1542, + "row_support_size": 280, + "source": 394 + }, + { + "clock": 39532, + "destination": 517, + "live_other_roles": 13, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "3ebe7bf053aca8495d17f9a5b6c4b5223ab1e54b0116c63d040f7a3d59cce9ec", + "nonzero_peer_rows": 13, + "role": 1539, + "row_support_size": 247, + "source": 243 + }, + { + "clock": 39559, + "destination": 518, + "live_other_roles": 12, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "1aa2f38b66a1f6dd29a1d3893dcd8facf4d5a9b129e6b1820dd7f8b61e30d56e", + "nonzero_peer_rows": 12, + "role": 1538, + "row_support_size": 280, + "source": 240 + }, + { + "clock": 39705, + "destination": 529, + "live_other_roles": 7, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "d7ef421ccb656d704f573f3f726e4a9ca47361d1f37e6b3767a9c6c72e19cba3", + "nonzero_peer_rows": 6, + "role": 1526, + "row_support_size": 125, + "source": 531 + }, + { + "clock": 39763, + "destination": 531, + "live_other_roles": 4, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "ce9bc6895b310f72297158609238e292391d8f109899e70a19da53414b606a25", + "nonzero_peer_rows": 4, + "role": 1548, + "row_support_size": 79, + "source": 529 + }, + { + "clock": 39792, + "destination": 520, + "live_other_roles": 1, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "f71001537daf99cd0533428ea747e0ae8d3fd73f3fa19752954aa175eb7bfab6", + "nonzero_peer_rows": 1, + "role": 1503, + "row_support_size": 236, + "source": 529 + }, + { + "clock": 39798, + "destination": 595, + "live_other_roles": 11, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "f71001537daf99cd0533428ea747e0ae8d3fd73f3fa19752954aa175eb7bfab6", + "nonzero_peer_rows": 11, + "role": 1503, + "row_support_size": 236, + "source": 520 + }, + { + "clock": 39831, + "destination": 599, + "live_other_roles": 2, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "9cf57594854f2f12f2bd274e84562be2b4d42cc9ac6191cff2ec7b70ca875f18", + "nonzero_peer_rows": 2, + "role": 1515, + "row_support_size": 124, + "source": 260 + }, + { + "clock": 39853, + "destination": 520, + "live_other_roles": 1, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "aaf750f37929bbcf572f4e0e2243b53a86925ffe5c7787d5b98c6655767fb4dc", + "nonzero_peer_rows": 1, + "role": 1532, + "row_support_size": 288, + "source": 595 + }, + { + "clock": 39862, + "destination": 529, + "live_other_roles": 13, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "7858234e7d1d182859e2730014af31f08909daca80c7c911c5d8702f2d42b366", + "nonzero_peer_rows": 13, + "role": 1532, + "row_support_size": 294, + "source": 520 + }, + { + "clock": 40518, + "destination": 559, + "live_other_roles": 2, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "7fb1e13c4bbb36e67f52102a2dae4967ca3a512346a612174b54a13656ce35b6", + "nonzero_peer_rows": 2, + "role": 1549, + "row_support_size": 96, + "source": 549 + }, + { + "clock": 40536, + "destination": 549, + "live_other_roles": 11, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "caf49ede415a8127434bbd9881b59496b9f6057ae321b7e42d7055d2bab028b3", + "nonzero_peer_rows": 9, + "role": 1527, + "row_support_size": 207, + "source": 559 + }, + { + "clock": 40543, + "destination": 115, + "live_other_roles": 11, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "bef3f5100df715b3eccf037f994fc5492cfba4aca6dda3c02a1644f50e40f44c", + "nonzero_peer_rows": 11, + "role": 1501, + "row_support_size": 247, + "source": 549 + }, + { + "clock": 40547, + "destination": 593, + "live_other_roles": 6, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "68b319b01bde3dd2d4b55f8e38590edaa9fe1dd7a4621f01494c703b231fa482", + "nonzero_peer_rows": 6, + "role": 1501, + "row_support_size": 247, + "source": 115 + }, + { + "clock": 41474, + "destination": 477, + "live_other_roles": 13, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "a97546ddda213d4a5cd5ae180f90beab4508a8abe265de005bac8b55e9bdb87d", + "nonzero_peer_rows": 13, + "role": 1537, + "row_support_size": 289, + "source": 1090 + }, + { + "clock": 41629, + "destination": 549, + "live_other_roles": 9, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "55b456819c32f890c568a248b7837bdb699d8a604ce4e643b4d63c5a249023f1", + "nonzero_peer_rows": 9, + "role": 1530, + "row_support_size": 284, + "source": 593 + }, + { + "clock": 41988, + "destination": 117, + "live_other_roles": 15, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "68caff8adce898d3995e5c193fdeff380b9f11852abca5cf236b26e535a8b5c1", + "nonzero_peer_rows": 15, + "role": 1531, + "row_support_size": 297, + "source": 594 + }, + { + "clock": 42460, + "destination": 1031, + "live_other_roles": 17, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "5546930ac9e2930cb4daaa25e1344d88f41c4ae0b391dedf210c6ef595225cc2", + "nonzero_peer_rows": 17, + "role": 1504, + "row_support_size": 121, + "source": 591 + }, + { + "clock": 42465, + "destination": 597, + "live_other_roles": 3, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "a1601874efa1958e098b9716cdbdc024704965669bbf33025298cf05d63a9c6b", + "nonzero_peer_rows": 3, + "role": 1504, + "row_support_size": 226, + "source": 1031 + }, + { + "clock": 42470, + "destination": 1031, + "live_other_roles": 17, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "d683a3af8b9a2463f81aabb9aa514a73102020f2e2b47c9d18b77a057232f968", + "nonzero_peer_rows": 17, + "role": 1533, + "row_support_size": 207, + "source": 597 + }, + { + "clock": 42483, + "destination": 591, + "live_other_roles": 6, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "df0e18b4542908b13db321eaac260d599c92e2f1a2ca507247c8c2fc96a053e9", + "nonzero_peer_rows": 6, + "role": 1533, + "row_support_size": 243, + "source": 1031 + }, + { + "clock": 44249, + "destination": 543, + "live_other_roles": 3, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "bfd30c52423b23ec9b52001f1f07d9023c3a5f2cdbd0cb99684d5668699b152e", + "nonzero_peer_rows": 3, + "role": 1550, + "row_support_size": 183, + "source": 541 + }, + { + "clock": 44256, + "destination": 534, + "live_other_roles": 1, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "6ae5506183a397296f4854a83cf096895fb5de5cd8acca3722cd22680c12ca04", + "nonzero_peer_rows": 1, + "role": 1531, + "row_support_size": 312, + "source": 117 + }, + { + "clock": 44258, + "destination": 541, + "live_other_roles": 8, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "1619ca5f36c0c97d3dae9eb3c100fda9256bf31ed592df0fca620972bbf3356c", + "nonzero_peer_rows": 8, + "role": 1531, + "row_support_size": 312, + "source": 534 + }, + { + "clock": 45607, + "destination": 267, + "live_other_roles": 7, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "892f12b1c2d0943d28a3f3e45874f9505d65ff57c8c6a72983e6df26ced73322", + "nonzero_peer_rows": 7, + "role": 1551, + "row_support_size": 148, + "source": 1091 + }, + { + "clock": 45625, + "destination": 1091, + "live_other_roles": 24, + "matches": [], + "moved_row": null, + "moved_row_nonzero": true, + "moved_row_sha256": "2e2e035b70cf81a6e52cbca4a6a6e3c3b932e6d8b7f1ea1abf734afebef42f98", + "nonzero_peer_rows": 24, + "role": 1540, + "row_support_size": 137, + "source": 260 + } + ], + "status": "scoped_exclusion", + "support_survivor_sites": 0, + "unresolved": [], + "visited": 47, + "whole_post_support_optimistic_upper": { + "complete_margin_interval": [ + "-1002247197758299781/500000000000000000000000000000000000000000000000", + "-2004494395516543389/1000000000000000000000000000000000000000000000000" + ], + "removed_rank_histogram_per_copy": {}, + "saving_interval": [ + "0", + "0" + ] + } +} diff --git a/research/p104-owned-move-destination-span/engines/fullbank.py b/research/p104-owned-move-destination-span/engines/fullbank.py new file mode 100644 index 0000000000..8cafcc4110 --- /dev/null +++ b/research/p104-owned-move-destination-span/engines/fullbank.py @@ -0,0 +1,195 @@ +"""Exact same-clock destination span with constructive or separating witnesses.""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import runpy +import signal +from time import monotonic + +PINS = { + "round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "round41/independent/RESULT.json": "1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7", + "round41/independent/replay_core.py": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "round41/lead/r41-price-support/PRICE.json": "1efe8b52e02a8db0ac6a04cdf6b943e515badee5fc0b7bea6ea3fe4a30fd1d01", +} + + +def unique(items): + out = dict(items) + if len(items) != len(out): + raise ValueError("duplicate JSON key") + return out + + +def record(out, name, content): + tmp = out / (name + ".partial") + tmp.write_text(json.dumps(content, indent=2, sort_keys=True) + "\n") + tmp.replace(out / name) + + +def axpy(dst, src, scale): + for key, value in src.items(): + updated = dst.get(key, 0) + scale * value + if updated: + dst[key] = updated + else: + dst.pop(key, None) + + +def dot(left, right): + return sum(v * right.get(k, 0) for k, v in left.items()) + + +def solve(target, donors): + basis = {} + for role, donor in donors.items(): + row, combination = dict(donor), {role: Fraction(1)} + for pivot, (old, coefficients) in sorted(basis.items()): + if pivot in row: + scale = -row[pivot] + axpy(row, old, scale) + axpy(combination, coefficients, scale) + if row: + pivot = min(row) + factor = row[pivot] + basis[pivot] = ({k: v / factor for k, v in row.items()}, + {k: v / factor for k, v in combination.items()}) + + residual, combination = dict(target), {} + for pivot, (row, coefficients) in sorted(basis.items()): + if pivot in residual: + scale = residual[pivot] + axpy(residual, row, -scale) + axpy(combination, coefficients, scale) + if not residual: + recovered = {} + for role, scale in combination.items(): + axpy(recovered, donors[role], scale) + assert recovered == target + return len(basis), "combination", combination + + free = min(residual) + dual = {free: Fraction(1)} + assert free not in basis + for pivot, (row, _) in sorted(basis.items(), reverse=True): + value = -dot(row, dual) + if value: + dual[pivot] = value + assert all(dot(donor, dual) == 0 for donor in donors.values()) + assert dot(target, dual) == residual[free] != 0 + return len(basis), "separating_dual", dual + + +def controls(): + f = Fraction + donors = {5: {1: f(1), 4: f(2)}, 6: {2: f(1)}, 7: {3: f(1)}, 8: {1: f(2), 4: f(4)}} + target = {1: f(-1, 3), 2: f(2, 5), 3: f(1), 4: f(-2, 3)} + assert solve(target, donors) == (3, "combination", {5: f(-1, 3), 6: f(2, 5), 7: f(1)}) + target[4] = f(2, 3) + rank, kind, witness = solve(target, donors) + assert (rank, kind, witness) == (3, "separating_dual", {4: f(1), 1: f(-2)}) + assert solve({0: f(1)}, {}) == (0, "separating_dual", {0: f(1)}) + try: + unique([("same", 1), ("same", 2)]) + except ValueError: + pass + else: + raise AssertionError("duplicate pin control") + return ["signed_three_donor_combination", "dependent_row_retained", + "changed_sign_separating_dual", "empty_bank", "duplicate_key_rejected"] + + +def as_vector(row): + denominator, terms = row + return {key: Fraction(value, denominator) for key, value in terms.items()} + + +def run(deps, out, seconds): + start = monotonic() + out.mkdir(parents=True, exist_ok=False) + raw = {} + for path, digest in PINS.items(): + data = (deps / path).read_bytes() + if sha256(data).hexdigest() != digest: + raise ValueError(f"changed dependency {path}") + raw[path] = data + census = json.loads(raw["round41/independent/RESULT.json"], object_pairs_hook=unique) + invoice = json.loads(raw["round41/lead/r41-price-support/PRICE.json"], object_pairs_hook=unique) + assert census["scope_exhausted"] and not census["match_count"] and invoice["copies"] == 17 + hist = Counter(row["rank"] for row in census["records"] if row["nonzero_destination_roles"] >= 3) + quote = invoice["exact_optimistic_single_site_by_rank"] + stock = [sum((n * Fraction(quote[str(r)]["saving_interval"][i]) for r, n in hist.items()), Fraction()) + for i in range(2)] + price = { + "eligible_sites_after_pair_exclusion": sum(hist.values()), + "eligible_nonzero_donors": sum(r["nonzero_destination_roles"] for r in census["records"] + if r["nonzero_destination_roles"] >= 3), + "optimistic_saving_interval": list(map(str, stock)), + "whole_margin_interval_before_new_charges": [ + str(Fraction(v) + s) for v, s in zip(invoice["baseline_interval"], stock, strict=True) + ], + "copies": 17, + "baseline_interval": invoice["baseline_interval"], + "crossing_upper": invoice["crossing_upper"], + "rank_histogram": dict(hist), + "pins": PINS, + } + assert price["eligible_sites_after_pair_exclusion"] == 39 and price["eligible_nonzero_donors"] == 411 + record(out, "PRICE.json", price) + + rows = [] + known = {row["literal_index"]: row for row in census["records"]} + core = runpy.run_path(str(deps / "round41/independent/replay_core.py")) + word = json.loads(gzip.decompress(raw["round30/complex/source/inputs/WORD.json.gz"]), + object_pairs_hook=unique) + + def visit(index, role, old, chart, rank, charts, values, live): + donor_ids = [r for r, f in enumerate(charts) if r != role and f == chart and values[r][1]] + old_count = known[index] + assert (role, old, chart, rank, len(donor_ids)) == ( + old_count["role"], old_count["from"], old_count["to"], old_count["rank"], + old_count["nonzero_destination_roles"], + ) + vector = as_vector(values[role]) + assert vector + basis_rank, kind, witness = solve(vector, {r: as_vector(values[r]) for r in donor_ids}) + rows.append({"literal_index": index, "role": role, "source_chart": old, "destination_chart": chart, + "paid_rank": rank, "donors": donor_ids, "bank_rank": basis_rank, "kind": kind, + "witness": {str(k): str(v) for k, v in witness.items()}}) + + summary = core["audit"](word, start, seconds - 2, visit) + visited = {row["literal_index"] for row in rows} + unvisited = sorted(known.keys() - visited) + matches = [r["literal_index"] for r in rows if r["kind"] == "combination"] + remaining = set(unvisited) | set(matches) + upper = sum((Fraction(quote[str(known[clock]["rank"])]["saving_interval"][1]) + for clock in remaining), Fraction()) + if summary["scope_exhausted"]: + assert len(rows) == 47 and sum(len(row["donors"]) for row in rows) == 424 + record(out, "SUPPORT.json", { + "head": core["HEAD"], "scope": "all nonzero live destination-chart donor rows at each literal MOVE", + "census": summary, "controls": controls(), "matches": matches, + "optimistic_saving_upper_after_support": str(upper), "rows": rows, "unvisited_moves": unvisited, + "price_sha256": sha256((out / "PRICE.json").read_bytes()).hexdigest(), + }) + + +if __name__ == "__main__": + assert __debug__ + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("dependencies", type=Path) + parser.add_argument("out", type=Path) + parser.add_argument("--seconds", type=int, default=45, choices=range(4, 46)) + args = parser.parse_args() + + def deadline(_signum, _frame): + raise TimeoutError("full bank runner watchdog") + + signal.signal(signal.SIGALRM, deadline) + signal.alarm(args.seconds) + run(args.dependencies.resolve(), args.out.resolve(), args.seconds) diff --git a/research/p104-owned-move-destination-span/engines/pairs.py b/research/p104-owned-move-destination-span/engines/pairs.py new file mode 100644 index 0000000000..a665b2d2bd --- /dev/null +++ b/research/p104-owned-move-destination-span/engines/pairs.py @@ -0,0 +1,275 @@ +"""Exact two-donor normalized support inventory on the pinned #7277 word.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +from functools import cache +import gzip +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +import runpy +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +WORD = 'round30/complex/source/inputs/WORD.json.gz' +EARLY = 'round30/complex/source/inputs/EARLY-RESULT.json' +CORE = 'round41/independent/replay_core.py' +LEAD_PRICE = 'round41/lead/r41-price-support/PRICE.json' +LEAD_SUPPORT = 'round41/lead/r41-price-support/SUPPORT.json' +INDEPENDENT = 'round41/independent/RESULT.json' +PINS = { + 'round30/complex/audit.py': '67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb', + 'round30/complex/source/inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + EARLY: '691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7', + WORD: '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + 'round30/complex/source/powers.py': 'c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee', + CORE: 'fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0', + INDEPENDENT: '1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7', + LEAD_PRICE: '1efe8b52e02a8db0ac6a04cdf6b943e515badee5fc0b7bea6ea3fe4a30fd1d01', + LEAD_SUPPORT: 'c31c8425e2a99fe15a9ffa48662dacca4eda2b778d55ceceae2978a9bdb12f3c', +} +R42_UPPER = [ + '55568818205146215263695136468307142417029952282393/31250000000000000000000000000000000000000000000', + '889101091282339444219122183492914278672479236518509/500000000000000000000000000000000000000000000000', +] + + +def load(roots): + result = {} + for key, digest in PINS.items(): + root, path = key.split('/', 1) + file = roots[root] / path + raw = file.read_bytes() + assert sha256(raw).hexdigest() == digest, ('changed dependency', key) + result[key] = file, raw + return result + + +def decode(raw): + def unique(pairs): + result = dict(pairs) + assert len(result) == len(pairs), 'duplicate JSON key' + return result + return json.loads(raw, object_pairs_hook=unique) + + +def write(out, name, value): + tmp = out / (name + '.tmp') + tmp.write_text(json.dumps(value, indent=2, sort_keys=True) + '\n') + tmp.replace(out / name) + + +def solve(target, left, right): + """Use two independent coordinate equations and check every coordinate.""" + xd, x = target + ud, u = left + vd, v = right + assert x and u and v and xd > 0 and ud > 0 and vd > 0 + indices = u.keys() | v.keys() + i = min(indices) + ui, vi = u.get(i, 0), v.get(i, 0) + for j in sorted(indices - {i}): + determinant = ui * v.get(j, 0) - vi * u.get(j, 0) + if determinant: + break + else: + return 'dependent', None + xi, xj = x.get(i, 0), x.get(j, 0) + a = xi * v.get(j, 0) - xj * vi + b = ui * xj - u.get(j, 0) * xi + if any(x.get(k, 0) * determinant != a * u.get(k, 0) + b * v.get(k, 0) + for k in x.keys() | indices): + return 'nonzero_residual', None + if not a or not b: + return 'single_donor', None + return 'supported', ([i, j], Q(a * ud, determinant * xd), Q(b * vd, determinant * xd)) + + +def controls(): + x = (6, {0: -1, 2: 5, 3: 4}) + u = (2, {0: 1, 2: 1}) + v = (3, {0: 1, 2: -2, 3: -2}) + assert solve(x, u, v) == ('supported', ([0, 2], Q(1, 3), Q(-1))) + assert solve((6, {0: -1, 2: 5, 3: -4}), u, v)[0] == 'nonzero_residual' + assert solve((6, {0: -1, 2: 5, 3: 4, 4: 1}), u, v)[0] == 'nonzero_residual' + assert solve(x, u, (7, {0: -4, 2: -4}))[0] == 'dependent' + assert solve(u, u, v)[0] == 'single_donor' + return ['signed_rational_coefficients', 'off_pivot_sign_rejected', 'outside_union_rejected', + 'dependent_pair_and_zero_coefficient_distinguished'] + + +def receipt_stock(data, word): + prior_price, lead, other = [decode(data[name][1]) for name in (LEAD_PRICE, LEAD_SUPPORT, INDEPENDENT)] + assert lead['head'] == prior_price['head'] == other['scientific_head'] == HEAD + assert lead['price_sha256'] == PINS[LEAD_PRICE] and other['core_sha256'] == PINS[CORE] + assert lead['full_tape_exhausted'] and other['scope_exhausted'] + assert not lead['unresolved'] and not other['exact_zero_moves'] + assert lead['support_survivor_sites'] == other['match_count'] == 0 + census = {} + for site, a, b in zip(prior_price['sites'], lead['rows'], other['records'], strict=True): + t = site['clock'] + op, owner, source, destination, owned = word['program'][t] + assert op == 'MOVE' and owned and t not in census + assert (owner, source, destination) == (site['role'], site['source'], site['destination']) + assert (t, owner, source, destination, site['rank']) == ( + b['literal_index'], b['role'], b['from'], b['to'], b['rank']) + assert (t, owner, source, destination) == (a['clock'], a['role'], a['source'], a['destination']) + assert a['moved_row_nonzero'] and not a['matches'] and not b['matches'] + assert a['live_other_roles'] == b['live_destination_roles'] + n = b['nonzero_destination_roles'] + assert n == a['nonzero_peer_rows'] + census[t] = site | {'nonzero_donors': n, 'pairs': n * (n - 1) // 2} + assert len(census) == 47 and sum(bool(r['pairs']) for r in census.values()) == 44 + assert sum(r['pairs'] for r in census.values()) == 2767 + return prior_price, census + + +class SoftCap(Exception): + """Stop between exact tests, preserving completed coverage.""" + + +def run(roots, out, seconds, pair_cap, started): + checks = controls() + data = load(roots) + word = decode(gzip.decompress(data[WORD][1])) + prior_price, census = receipt_stock(data, word) + audit = runpy.run_path(str(data['round30/complex/audit.py'][0])) + power = runpy.run_path(str(data['round30/complex/source/powers.py'][0]))['power'] + _, rank, _, edges, _, _, copies, paid, productive, _ = audit['read_model']() + assert audit['HEAD'] == HEAD and copies == prior_price['copies'] == 17 and len(edges) == 137891 + assert dict(paid) == {int(k): v for k, v in prior_price['original_paid'].items()} + assert dict(productive) == {int(k): v for k, v in prior_price['original_productive'].items()} + k = Q(decode(data[EARLY][1])['price']['independent_raw_bracket'][1]) + assert k == Q(prior_price['crossing_upper']) + for r in census.values(): + assert r['rank'] == rank(r['source'], r['destination'], True) + tariff = cache(lambda r: power(r, k)) + + def price(hist): + lo = hi = Q(0) + for r, count in hist.items(): + a, b = tariff(r) + lo += count * (a if count >= 0 else b) + hi += count * (b if count >= 0 else a) + return list(map(str, (lo, hi))) + + net = productive.copy() + net.subtract(paid) + baseline = price(net) + assert baseline == prior_price['baseline_interval'] and Q(baseline[1]) < 0 + + def quote(clocks): + assert len(clocks) == len(set(clocks)) + ranks = Counter(census[t]['rank'] for t in clocks) + debits = {r: n * copies for r, n in ranks.items()} + assert all(n <= paid[r] for r, n in debits.items()) + new = net.copy() + new.update(debits) + return dict(removed_ranks_per_copy=dict(ranks), saving_interval=price(debits), + complete_margin_interval=price(new)) + + eligible = [t for t, site in census.items() if site['pairs']] + whole = quote(eligible) + assert list(map(Q, whole['saving_interval'])) == list(map(Q, R42_UPPER)) + write(out, 'PRICE.json', dict(head=HEAD, pins=PINS, crossing_upper=str(k), copies=copies, + baseline_interval=baseline, original_paid=dict(paid), original_productive=dict(productive), + eligible_sites=len(eligible), pairs=2767, cap=pair_cap, seconds_cap=seconds, + sites=list(census.values()), whole_optimistic_upper=whole, + local_change_per_copy=dict(add_CLEAR=1, add_INIT=1, add_COPY=1, add_ADD=1, remove_MOVE=1, + net_literal_events=3, new_owner_slots=0), + grant='Remove each eligible owned MOVE once across all copies, granting all other costs free.')) + if Q(whole['complete_margin_interval'][1]) <= 0: + return + + progress, witnesses, visited_sites = {}, [], set() + solved = 0 + deadline = started + seconds - 2 + + def visit(t, role, source, destination, size, charts, rows, live): + nonlocal solved + site = census[t] + assert (role, source, destination, size) == tuple(site[k] for k in ('role', 'source', 'destination', 'rank')) + assert role in live and rows[role][1] + donors = [r for r, chart in enumerate(charts) if r != role and chart == destination and rows[r][1]] + assert len(donors) == site['nonzero_donors'] + visited_sites.add(t) + counts = progress[t] = Counter() + for a, b in combinations(donors, 2): + if solved >= pair_cap or monotonic() >= deadline: + raise SoftCap + status, result = solve(rows[role], rows[a], rows[b]) + counts[status] += 1 + solved += 1 + if result is not None: + pivots, alpha, beta = result + snapshot = [(rows[r][0], rows[r][1].copy()) for r in (role, a, b)] + witnesses.append(dict(clock=t, role=role, donor_roles=[a, b], coefficients=[str(alpha), str(beta)], + pivots=pivots, normalized_rows=snapshot, + proposed_events=[['CLEAR', role, source], ['INIT', role, destination], + ['COPY', role, a, str(alpha), destination], + ['ADD', role, b, str(beta), destination]])) + + core = runpy.run_path(str(data[CORE][0])) + assert core['HEAD'] == HEAD and core['SHA'] == PINS[WORD] + core_report = None + try: + core_report = core['audit'](word, started, seconds - 2, visit) + except SoftCap: + pass + remaining = {t: site['pairs'] - sum(progress.get(t, {}).values()) for t, site in census.items() + if site['pairs'] > sum(progress.get(t, {}).values())} + assert sum(remaining.values()) + solved == 2767 + status_counts = Counter() + for row in progress.values(): + status_counts.update(row) + assert sum(status_counts.values()) == solved and status_counts['single_donor'] == 0 + if core_report and core_report['scope_exhausted']: + assert len(visited_sites) == 47 and not remaining and not core_report['exact_zero_moves'] + assert core_report['paid_owned_histogram'] == core['OWNED_PAID'] + possible = sorted(set(remaining) | {w['clock'] for w in witnesses}) + write(out, 'SUPPORT.json', dict(head=HEAD, pins=PINS, controls=checks, + price_sha256=sha256((out / 'PRICE.json').read_bytes()).hexdigest(), + visited_pairs=solved, unvisited_pairs=sum(remaining.values()), unvisited_by_clock=remaining, + status_counts=dict(status_counts), site_status_counts={t: dict(c) for t, c in progress.items()}, + support_witnesses=witnesses, surviving_sites=len({w['clock'] for w in witnesses}), + whole_post_support_optimistic_upper=quote(possible), core_receipt=core_report, + scope_exhausted=not remaining, status='support_only' if witnesses else 'capped' if remaining else 'excluded', + pending_costs=['lawful signed coefficients and physical phase', 'ordinary COPY/ADD and setup', + 'ownership, dirty restoration, recovery, precision and tape', 'complete independent replay'])) + + +def main(): + p = ArgumentParser() + p.add_argument('round30', type=Path, nargs='?') + p.add_argument('round41', type=Path, nargs='?') + p.add_argument('out', type=Path, nargs='?') + p.add_argument('--seconds', type=int, default=120, choices=range(3, 121), metavar='3..120') + p.add_argument('--pairs', type=int, default=2767, choices=range(1, 2768), metavar='1..2767') + p.add_argument('--controls-only', action='store_true') + a = p.parse_args() + if a.controls_only: + print(json.dumps(controls())) + return + if None in (a.round30, a.round41, a.out): + p.error('explicit Round 30 and Round 41 roots and a fresh output are required') + a.out.mkdir() + + def timeout(*_): + raise TimeoutError('hard runner deadline') + + signal(SIGALRM, timeout) + alarm(a.seconds) + try: + run({'round30': a.round30, 'round41': a.round41}, a.out, a.seconds, a.pairs, monotonic()) + except TimeoutError: + write(a.out, 'TIMEOUT.json', dict(head=HEAD, status='hard_timeout', pairs_unverified=2767, + price_saved=(a.out / 'PRICE.json').is_file(), seconds_cap=a.seconds)) + raise SystemExit(2) + finally: + alarm(0) + + +if __name__ == '__main__': + main() diff --git a/research/p104-owned-move-destination-span/receipts/fullbank/PRICE.json b/research/p104-owned-move-destination-span/receipts/fullbank/PRICE.json new file mode 100644 index 0000000000..5db176e5a5 --- /dev/null +++ b/research/p104-owned-move-destination-span/receipts/fullbank/PRICE.json @@ -0,0 +1,32 @@ +{ + "baseline_interval": [ + "-1002247197758299781/500000000000000000000000000000000000000000000000", + "-2004494395516543389/1000000000000000000000000000000000000000000000000" + ], + "copies": 17, + "crossing_upper": "91141748217473298207420876011401/25000000000000000000000000000000000", + "eligible_nonzero_donors": 411, + "eligible_sites_after_pair_exclusion": 39, + "optimistic_saving_interval": [ + "838143995809092296266505914385780563410545820078443/500000000000000000000000000000000000000000000000", + "1676287991618184592533011828771561126821091640157311/1000000000000000000000000000000000000000000000000" + ], + "pins": { + "round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "round41/independent/RESULT.json": "1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7", + "round41/independent/replay_core.py": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "round41/lead/r41-price-support/PRICE.json": "1efe8b52e02a8db0ac6a04cdf6b943e515badee5fc0b7bea6ea3fe4a30fd1d01" + }, + "rank_histogram": { + "1": 14, + "2": 8, + "3": 2, + "4": 13, + "5": 1, + "6": 1 + }, + "whole_margin_interval_before_new_charges": [ + "419071997904546148133252957192889780581674030889331/250000000000000000000000000000000000000000000000", + "838143995809092296266505914385779561163348061806961/500000000000000000000000000000000000000000000000" + ] +} diff --git a/research/p104-owned-move-destination-span/receipts/fullbank/SUPPORT.json b/research/p104-owned-move-destination-span/receipts/fullbank/SUPPORT.json new file mode 100644 index 0000000000..17a38fbf5b --- /dev/null +++ b/research/p104-owned-move-destination-span/receipts/fullbank/SUPPORT.json @@ -0,0 +1,1157 @@ +{ + "census": { + "checked_copies": 1, + "exact_zero_moves": [], + "first_unvisited_literal_index": null, + "first_unvisited_owned_move_index": null, + "fresh_zero_moves": 0, + "literal_events": 76443, + "literal_events_visited": 76443, + "nonzero_owned_clears": 69, + "owned_lifetimes": 70, + "paid_owned_histogram": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "paid_owned_moves": 47, + "peak_owned": 49, + "scope_exhausted": true + }, + "controls": [ + "signed_three_donor_combination", + "dependent_row_retained", + "changed_sign_separating_dual", + "empty_bank", + "duplicate_key_rejected" + ], + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "matches": [], + "optimistic_saving_upper_after_support": "0", + "price_sha256": "959b9e4ceb947577ab42d759e91bed48ce855ccce32e72a51a0bf49de524bc4d", + "rows": [ + { + "bank_rank": 25, + "destination_chart": 1090, + "donors": [ + 41, + 42, + 106, + 400, + 401, + 403, + 405, + 410, + 741, + 813, + 814, + 876, + 1162, + 1163, + 1165, + 1167, + 1171, + 1357, + 1365, + 1373, + 1380, + 1385, + 1392, + 1397, + 1448 + ], + "kind": "separating_dual", + "literal_index": 30527, + "paid_rank": 4, + "role": 1510, + "source_chart": 477, + "witness": { + "4": "1" + } + }, + { + "bank_rank": 2, + "destination_chart": 470, + "donors": [ + 402, + 1164 + ], + "kind": "separating_dual", + "literal_index": 30535, + "paid_rank": 1, + "role": 1520, + "source_chart": 1090, + "witness": { + "4": "1" + } + }, + { + "bank_rank": 2, + "destination_chart": 601, + "donors": [ + 728, + 1349, + 1547 + ], + "kind": "separating_dual", + "literal_index": 30549, + "paid_rank": 2, + "role": 1521, + "source_chart": 470, + "witness": { + "4": "1" + } + }, + { + "bank_rank": 4, + "destination_chart": 470, + "donors": [ + 402, + 727, + 1164, + 1508, + 1520 + ], + "kind": "separating_dual", + "literal_index": 30579, + "paid_rank": 2, + "role": 1547, + "source_chart": 601, + "witness": { + "142": "1", + "4": "-1/2" + } + }, + { + "bank_rank": 26, + "destination_chart": 1090, + "donors": [ + 41, + 42, + 106, + 400, + 401, + 403, + 405, + 410, + 741, + 813, + 814, + 876, + 1162, + 1163, + 1165, + 1167, + 1171, + 1357, + 1365, + 1373, + 1380, + 1385, + 1392, + 1397, + 1448, + 1510 + ], + "kind": "separating_dual", + "literal_index": 30591, + "paid_rank": 1, + "role": 1546, + "source_chart": 470, + "witness": { + "105": "2", + "1163": "1", + "15": "-2", + "41": "2", + "52": "4" + } + }, + { + "bank_rank": 11, + "destination_chart": 1091, + "donors": [ + 57, + 81, + 92, + 224, + 225, + 227, + 229, + 234, + 742, + 754, + 1499, + 1564 + ], + "kind": "separating_dual", + "literal_index": 32937, + "paid_rank": 4, + "role": 1529, + "source_chart": 267, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 7, + "destination_chart": 541, + "donors": [ + 130, + 151, + 399, + 472, + 745, + 899, + 1359 + ], + "kind": "separating_dual", + "literal_index": 33123, + "paid_rank": 1, + "role": 1528, + "source_chart": 543, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 7, + "destination_chart": 260, + "donors": [ + 226, + 749, + 988, + 990, + 1345, + 1393, + 1477, + 1540 + ], + "kind": "separating_dual", + "literal_index": 33131, + "paid_rank": 1, + "role": 1514, + "source_chart": 1091, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 2, + "destination_chart": 534, + "donors": [ + 995, + 1489 + ], + "kind": "separating_dual", + "literal_index": 33138, + "paid_rank": 1, + "role": 1502, + "source_chart": 541, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 14, + "destination_chart": 117, + "donors": [ + 623, + 624, + 626, + 627, + 629, + 710, + 732, + 753, + 1288, + 1290, + 1291, + 1292, + 1482, + 1524 + ], + "kind": "separating_dual", + "literal_index": 33140, + "paid_rank": 1, + "role": 1502, + "source_chart": 534, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 4, + "destination_chart": 594, + "donors": [ + 213, + 1206, + 1427, + 1531 + ], + "kind": "separating_dual", + "literal_index": 33147, + "paid_rank": 4, + "role": 1502, + "source_chart": 117, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 12, + "destination_chart": 243, + "donors": [ + 8, + 26, + 95, + 368, + 369, + 371, + 373, + 378, + 743, + 771, + 1389, + 1390 + ], + "kind": "separating_dual", + "literal_index": 34512, + "paid_rank": 4, + "role": 1513, + "source_chart": 517, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 3, + "destination_chart": 431, + "donors": [ + 375, + 1135, + 1137, + 1535 + ], + "kind": "separating_dual", + "literal_index": 34516, + "paid_rank": 1, + "role": 1518, + "source_chart": 243, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 8, + "destination_chart": 260, + "donors": [ + 226, + 749, + 988, + 990, + 1345, + 1393, + 1506, + 1514, + 1540 + ], + "kind": "separating_dual", + "literal_index": 35138, + "paid_rank": 2, + "role": 1541, + "source_chart": 599, + "witness": { + "270": "-1/4", + "317": "1/3", + "749": "1" + } + }, + { + "bank_rank": 3, + "destination_chart": 600, + "donors": [ + 723, + 724, + 725, + 1545 + ], + "kind": "separating_dual", + "literal_index": 35429, + "paid_rank": 2, + "role": 1519, + "source_chart": 431, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 4, + "destination_chart": 431, + "donors": [ + 546, + 1348, + 1507, + 1518, + 1535 + ], + "kind": "separating_dual", + "literal_index": 35434, + "paid_rank": 2, + "role": 1545, + "source_chart": 600, + "witness": { + "34": "1" + } + }, + { + "bank_rank": 21, + "destination_chart": 243, + "donors": [ + 8, + 26, + 95, + 368, + 369, + 371, + 373, + 378, + 743, + 771, + 780, + 798, + 865, + 1130, + 1131, + 1133, + 1135, + 1140, + 1389, + 1390, + 1513 + ], + "kind": "separating_dual", + "literal_index": 35438, + "paid_rank": 1, + "role": 1544, + "source_chart": 431, + "witness": { + "26": "-1/2", + "368": "1", + "67": "-1", + "8": "1/2", + "80": "1/2", + "88": "1/2" + } + }, + { + "bank_rank": 18, + "destination_chart": 240, + "donors": [ + 58, + 86, + 93, + 336, + 337, + 339, + 341, + 346, + 828, + 856, + 863, + 1098, + 1099, + 1101, + 1103, + 1108, + 1369, + 1437 + ], + "kind": "separating_dual", + "literal_index": 36307, + "paid_rank": 4, + "role": 1512, + "source_chart": 518, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 2, + "destination_chart": 394, + "donors": [ + 338, + 1100 + ], + "kind": "separating_dual", + "literal_index": 36311, + "paid_rank": 1, + "role": 1516, + "source_chart": 240, + "witness": { + "1": "1" + } + }, + { + "bank_rank": 2, + "destination_chart": 598, + "donors": [ + 711, + 1341, + 1543 + ], + "kind": "separating_dual", + "literal_index": 36319, + "paid_rank": 2, + "role": 1517, + "source_chart": 394, + "witness": { + "1": "1" + } + }, + { + "bank_rank": 4, + "destination_chart": 394, + "donors": [ + 338, + 713, + 1100, + 1505, + 1516 + ], + "kind": "separating_dual", + "literal_index": 36329, + "paid_rank": 2, + "role": 1543, + "source_chart": 598, + "witness": { + "1": "1", + "34": "1" + } + }, + { + "bank_rank": 19, + "destination_chart": 240, + "donors": [ + 58, + 86, + 93, + 336, + 337, + 339, + 341, + 346, + 828, + 856, + 863, + 1098, + 1099, + 1101, + 1103, + 1108, + 1369, + 1437, + 1512 + ], + "kind": "separating_dual", + "literal_index": 36341, + "paid_rank": 1, + "role": 1542, + "source_chart": 394, + "witness": { + "28": "1/2", + "58": "1/2", + "82": "1/2", + "86": "-1/2", + "93": "1" + } + }, + { + "bank_rank": 13, + "destination_chart": 517, + "donors": [ + 9, + 104, + 110, + 272, + 320, + 352, + 748, + 781, + 874, + 880, + 1035, + 1114, + 1496 + ], + "kind": "separating_dual", + "literal_index": 39532, + "paid_rank": 4, + "role": 1539, + "source_chart": 243, + "witness": { + "8": "1" + } + }, + { + "bank_rank": 12, + "destination_chart": 518, + "donors": [ + 256, + 288, + 304, + 384, + 416, + 735, + 1020, + 1051, + 1066, + 1146, + 1176, + 1351 + ], + "kind": "separating_dual", + "literal_index": 39559, + "paid_rank": 4, + "role": 1538, + "source_chart": 240, + "witness": { + "1": "1" + } + }, + { + "bank_rank": 6, + "destination_chart": 529, + "donors": [ + 146, + 162, + 744, + 1358, + 1444, + 1494 + ], + "kind": "separating_dual", + "literal_index": 39705, + "paid_rank": 1, + "role": 1526, + "source_chart": 531, + "witness": { + "3": "1" + } + }, + { + "bank_rank": 4, + "destination_chart": 531, + "donors": [ + 640, + 641, + 1298, + 1429 + ], + "kind": "separating_dual", + "literal_index": 39763, + "paid_rank": 1, + "role": 1548, + "source_chart": 529, + "witness": { + "10": "-2", + "164": "1", + "3": "2", + "5": "5/2", + "8": "-2" + } + }, + { + "bank_rank": 1, + "destination_chart": 520, + "donors": [ + 497 + ], + "kind": "separating_dual", + "literal_index": 39792, + "paid_rank": 1, + "role": 1503, + "source_chart": 529, + "witness": { + "3": "1" + } + }, + { + "bank_rank": 10, + "destination_chart": 595, + "donors": [ + 450, + 451, + 581, + 582, + 746, + 1207, + 1255, + 1479, + 1495, + 1532, + 1557 + ], + "kind": "separating_dual", + "literal_index": 39798, + "paid_rank": 5, + "role": 1503, + "source_chart": 520, + "witness": { + "0": "1" + } + }, + { + "bank_rank": 2, + "destination_chart": 599, + "donors": [ + 716, + 1344 + ], + "kind": "separating_dual", + "literal_index": 39831, + "paid_rank": 2, + "role": 1515, + "source_chart": 260, + "witness": { + "0": "1" + } + }, + { + "bank_rank": 1, + "destination_chart": 520, + "donors": [ + 497 + ], + "kind": "separating_dual", + "literal_index": 39853, + "paid_rank": 5, + "role": 1532, + "source_chart": 595, + "witness": { + "0": "1" + } + }, + { + "bank_rank": 13, + "destination_chart": 529, + "donors": [ + 146, + 162, + 228, + 440, + 744, + 913, + 927, + 992, + 1197, + 1358, + 1444, + 1451, + 1494 + ], + "kind": "separating_dual", + "literal_index": 39862, + "paid_rank": 1, + "role": 1532, + "source_chart": 520, + "witness": { + "0": "-1", + "146": "1" + } + }, + { + "bank_rank": 1, + "destination_chart": 559, + "donors": [ + 613, + 1527 + ], + "kind": "separating_dual", + "literal_index": 40518, + "paid_rank": 1, + "role": 1549, + "source_chart": 549, + "witness": { + "1": "1", + "142": "1" + } + }, + { + "bank_rank": 9, + "destination_chart": 549, + "donors": [ + 111, + 121, + 173, + 235, + 752, + 881, + 891, + 937, + 999 + ], + "kind": "separating_dual", + "literal_index": 40536, + "paid_rank": 1, + "role": 1527, + "source_chart": 559, + "witness": { + "1": "1" + } + }, + { + "bank_rank": 11, + "destination_chart": 115, + "donors": [ + 607, + 609, + 612, + 614, + 736, + 751, + 1276, + 1278, + 1368, + 1374, + 1525 + ], + "kind": "separating_dual", + "literal_index": 40543, + "paid_rank": 2, + "role": 1501, + "source_chart": 549, + "witness": { + "1": "1" + } + }, + { + "bank_rank": 6, + "destination_chart": 593, + "donors": [ + 174, + 469, + 549, + 561, + 1254, + 1530 + ], + "kind": "separating_dual", + "literal_index": 40547, + "paid_rank": 4, + "role": 1501, + "source_chart": 115, + "witness": { + "1": "1" + } + }, + { + "bank_rank": 13, + "destination_chart": 477, + "donors": [ + 20, + 23, + 29, + 39, + 65, + 240, + 750, + 792, + 795, + 801, + 811, + 835, + 1004 + ], + "kind": "separating_dual", + "literal_index": 41474, + "paid_rank": 4, + "role": 1537, + "source_chart": 1090, + "witness": { + "15": "1" + } + }, + { + "bank_rank": 8, + "destination_chart": 549, + "donors": [ + 111, + 121, + 173, + 235, + 752, + 881, + 937, + 999, + 1522 + ], + "kind": "separating_dual", + "literal_index": 41629, + "paid_rank": 6, + "role": 1530, + "source_chart": 593, + "witness": { + "10": "-4", + "126": "1" + } + }, + { + "bank_rank": 15, + "destination_chart": 117, + "donors": [ + 623, + 624, + 626, + 627, + 629, + 732, + 753, + 1285, + 1286, + 1288, + 1290, + 1291, + 1292, + 1482, + 1524 + ], + "kind": "separating_dual", + "literal_index": 41988, + "paid_rank": 4, + "role": 1531, + "source_chart": 594, + "witness": { + "129": "-1", + "131": "1" + } + }, + { + "bank_rank": 17, + "destination_chart": 1031, + "donors": [ + 695, + 696, + 698, + 699, + 702, + 706, + 747, + 1332, + 1333, + 1335, + 1336, + 1337, + 1362, + 1386, + 1498, + 1523, + 1562 + ], + "kind": "separating_dual", + "literal_index": 42460, + "paid_rank": 3, + "role": 1504, + "source_chart": 591, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 3, + "destination_chart": 597, + "donors": [ + 709, + 1340, + 1533 + ], + "kind": "separating_dual", + "literal_index": 42465, + "paid_rank": 4, + "role": 1504, + "source_chart": 1031, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 17, + "destination_chart": 1031, + "donors": [ + 695, + 696, + 698, + 699, + 702, + 706, + 747, + 1332, + 1333, + 1335, + 1336, + 1337, + 1362, + 1386, + 1498, + 1523, + 1562 + ], + "kind": "separating_dual", + "literal_index": 42470, + "paid_rank": 4, + "role": 1533, + "source_chart": 597, + "witness": { + "129": "1", + "1336": "1", + "34": "1" + } + }, + { + "bank_rank": 6, + "destination_chart": 591, + "donors": [ + 133, + 697, + 767, + 901, + 1334, + 1377 + ], + "kind": "separating_dual", + "literal_index": 42483, + "paid_rank": 3, + "role": 1533, + "source_chart": 1031, + "witness": { + "21": "-1", + "23": "-1", + "24": "1", + "5": "1", + "8": "-1" + } + }, + { + "bank_rank": 3, + "destination_chart": 543, + "donors": [ + 628, + 630, + 1290 + ], + "kind": "separating_dual", + "literal_index": 44249, + "paid_rank": 1, + "role": 1550, + "source_chart": 541, + "witness": { + "129": "1", + "4": "-7/2" + } + }, + { + "bank_rank": 1, + "destination_chart": 534, + "donors": [ + 995 + ], + "kind": "separating_dual", + "literal_index": 44256, + "paid_rank": 1, + "role": 1531, + "source_chart": 117, + "witness": { + "2": "1" + } + }, + { + "bank_rank": 8, + "destination_chart": 541, + "donors": [ + 130, + 151, + 399, + 472, + 745, + 899, + 917, + 1359 + ], + "kind": "separating_dual", + "literal_index": 44258, + "paid_rank": 1, + "role": 1531, + "source_chart": 534, + "witness": { + "19": "-2", + "2": "1", + "244": "1" + } + }, + { + "bank_rank": 7, + "destination_chart": 267, + "donors": [ + 18, + 45, + 61, + 63, + 103, + 108, + 817 + ], + "kind": "separating_dual", + "literal_index": 45607, + "paid_rank": 4, + "role": 1551, + "source_chart": 1091, + "witness": { + "0": "1" + } + }, + { + "bank_rank": 23, + "destination_chart": 1091, + "donors": [ + 57, + 81, + 92, + 224, + 225, + 227, + 229, + 234, + 717, + 719, + 720, + 742, + 754, + 756, + 827, + 851, + 862, + 988, + 989, + 991, + 993, + 998, + 1499, + 1564 + ], + "kind": "separating_dual", + "literal_index": 45625, + "paid_rank": 1, + "role": 1540, + "source_chart": 260, + "witness": { + "2": "-9", + "230": "-1", + "756": "1" + } + } + ], + "scope": "all nonzero live destination-chart donor rows at each literal MOVE", + "unvisited_moves": [] +} diff --git a/research/p104-owned-move-destination-span/receipts/independent/BANK.json b/research/p104-owned-move-destination-span/receipts/independent/BANK.json new file mode 100644 index 0000000000..a261e6dad9 --- /dev/null +++ b/research/p104-owned-move-destination-span/receipts/independent/BANK.json @@ -0,0 +1,464 @@ +{ + "banks_tested": 39, + "checked_copies": 1, + "controls": { + "dependent_extra_donor": true, + "outside_coordinate_rejected": true, + "three_donor_required": true + }, + "donors": 411, + "exact_zero_moves": [], + "first_unvisited_literal_index": null, + "first_unvisited_owned_move_index": null, + "fresh_zero_moves": 0, + "literal_events": 76443, + "literal_events_visited": 76443, + "matches": 0, + "nonzero_owned_clears": 69, + "owned_lifetimes": 70, + "paid_owned_histogram": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "paid_owned_moves": 47, + "peak_owned": 49, + "records": [ + { + "augmented_rank": 26, + "donor_rank": 25, + "donors": 25, + "from": 477, + "in_span": false, + "literal_index": 30527, + "paid_rank": 4, + "role": 1510, + "to": 1090 + }, + { + "augmented_rank": 3, + "donor_rank": 2, + "donors": 3, + "from": 470, + "in_span": false, + "literal_index": 30549, + "paid_rank": 2, + "role": 1521, + "to": 601 + }, + { + "augmented_rank": 5, + "donor_rank": 4, + "donors": 5, + "from": 601, + "in_span": false, + "literal_index": 30579, + "paid_rank": 2, + "role": 1547, + "to": 470 + }, + { + "augmented_rank": 27, + "donor_rank": 26, + "donors": 26, + "from": 470, + "in_span": false, + "literal_index": 30591, + "paid_rank": 1, + "role": 1546, + "to": 1090 + }, + { + "augmented_rank": 12, + "donor_rank": 11, + "donors": 12, + "from": 267, + "in_span": false, + "literal_index": 32937, + "paid_rank": 4, + "role": 1529, + "to": 1091 + }, + { + "augmented_rank": 8, + "donor_rank": 7, + "donors": 7, + "from": 543, + "in_span": false, + "literal_index": 33123, + "paid_rank": 1, + "role": 1528, + "to": 541 + }, + { + "augmented_rank": 8, + "donor_rank": 7, + "donors": 8, + "from": 1091, + "in_span": false, + "literal_index": 33131, + "paid_rank": 1, + "role": 1514, + "to": 260 + }, + { + "augmented_rank": 15, + "donor_rank": 14, + "donors": 14, + "from": 534, + "in_span": false, + "literal_index": 33140, + "paid_rank": 1, + "role": 1502, + "to": 117 + }, + { + "augmented_rank": 5, + "donor_rank": 4, + "donors": 4, + "from": 117, + "in_span": false, + "literal_index": 33147, + "paid_rank": 4, + "role": 1502, + "to": 594 + }, + { + "augmented_rank": 13, + "donor_rank": 12, + "donors": 12, + "from": 517, + "in_span": false, + "literal_index": 34512, + "paid_rank": 4, + "role": 1513, + "to": 243 + }, + { + "augmented_rank": 4, + "donor_rank": 3, + "donors": 4, + "from": 243, + "in_span": false, + "literal_index": 34516, + "paid_rank": 1, + "role": 1518, + "to": 431 + }, + { + "augmented_rank": 9, + "donor_rank": 8, + "donors": 9, + "from": 599, + "in_span": false, + "literal_index": 35138, + "paid_rank": 2, + "role": 1541, + "to": 260 + }, + { + "augmented_rank": 4, + "donor_rank": 3, + "donors": 4, + "from": 431, + "in_span": false, + "literal_index": 35429, + "paid_rank": 2, + "role": 1519, + "to": 600 + }, + { + "augmented_rank": 5, + "donor_rank": 4, + "donors": 5, + "from": 600, + "in_span": false, + "literal_index": 35434, + "paid_rank": 2, + "role": 1545, + "to": 431 + }, + { + "augmented_rank": 22, + "donor_rank": 21, + "donors": 21, + "from": 431, + "in_span": false, + "literal_index": 35438, + "paid_rank": 1, + "role": 1544, + "to": 243 + }, + { + "augmented_rank": 19, + "donor_rank": 18, + "donors": 18, + "from": 518, + "in_span": false, + "literal_index": 36307, + "paid_rank": 4, + "role": 1512, + "to": 240 + }, + { + "augmented_rank": 3, + "donor_rank": 2, + "donors": 3, + "from": 394, + "in_span": false, + "literal_index": 36319, + "paid_rank": 2, + "role": 1517, + "to": 598 + }, + { + "augmented_rank": 5, + "donor_rank": 4, + "donors": 5, + "from": 598, + "in_span": false, + "literal_index": 36329, + "paid_rank": 2, + "role": 1543, + "to": 394 + }, + { + "augmented_rank": 20, + "donor_rank": 19, + "donors": 19, + "from": 394, + "in_span": false, + "literal_index": 36341, + "paid_rank": 1, + "role": 1542, + "to": 240 + }, + { + "augmented_rank": 14, + "donor_rank": 13, + "donors": 13, + "from": 243, + "in_span": false, + "literal_index": 39532, + "paid_rank": 4, + "role": 1539, + "to": 517 + }, + { + "augmented_rank": 13, + "donor_rank": 12, + "donors": 12, + "from": 240, + "in_span": false, + "literal_index": 39559, + "paid_rank": 4, + "role": 1538, + "to": 518 + }, + { + "augmented_rank": 7, + "donor_rank": 6, + "donors": 6, + "from": 531, + "in_span": false, + "literal_index": 39705, + "paid_rank": 1, + "role": 1526, + "to": 529 + }, + { + "augmented_rank": 5, + "donor_rank": 4, + "donors": 4, + "from": 529, + "in_span": false, + "literal_index": 39763, + "paid_rank": 1, + "role": 1548, + "to": 531 + }, + { + "augmented_rank": 11, + "donor_rank": 10, + "donors": 11, + "from": 520, + "in_span": false, + "literal_index": 39798, + "paid_rank": 5, + "role": 1503, + "to": 595 + }, + { + "augmented_rank": 14, + "donor_rank": 13, + "donors": 13, + "from": 520, + "in_span": false, + "literal_index": 39862, + "paid_rank": 1, + "role": 1532, + "to": 529 + }, + { + "augmented_rank": 10, + "donor_rank": 9, + "donors": 9, + "from": 559, + "in_span": false, + "literal_index": 40536, + "paid_rank": 1, + "role": 1527, + "to": 549 + }, + { + "augmented_rank": 12, + "donor_rank": 11, + "donors": 11, + "from": 549, + "in_span": false, + "literal_index": 40543, + "paid_rank": 2, + "role": 1501, + "to": 115 + }, + { + "augmented_rank": 7, + "donor_rank": 6, + "donors": 6, + "from": 115, + "in_span": false, + "literal_index": 40547, + "paid_rank": 4, + "role": 1501, + "to": 593 + }, + { + "augmented_rank": 14, + "donor_rank": 13, + "donors": 13, + "from": 1090, + "in_span": false, + "literal_index": 41474, + "paid_rank": 4, + "role": 1537, + "to": 477 + }, + { + "augmented_rank": 9, + "donor_rank": 8, + "donors": 9, + "from": 593, + "in_span": false, + "literal_index": 41629, + "paid_rank": 6, + "role": 1530, + "to": 549 + }, + { + "augmented_rank": 16, + "donor_rank": 15, + "donors": 15, + "from": 594, + "in_span": false, + "literal_index": 41988, + "paid_rank": 4, + "role": 1531, + "to": 117 + }, + { + "augmented_rank": 18, + "donor_rank": 17, + "donors": 17, + "from": 591, + "in_span": false, + "literal_index": 42460, + "paid_rank": 3, + "role": 1504, + "to": 1031 + }, + { + "augmented_rank": 4, + "donor_rank": 3, + "donors": 3, + "from": 1031, + "in_span": false, + "literal_index": 42465, + "paid_rank": 4, + "role": 1504, + "to": 597 + }, + { + "augmented_rank": 18, + "donor_rank": 17, + "donors": 17, + "from": 597, + "in_span": false, + "literal_index": 42470, + "paid_rank": 4, + "role": 1533, + "to": 1031 + }, + { + "augmented_rank": 7, + "donor_rank": 6, + "donors": 6, + "from": 1031, + "in_span": false, + "literal_index": 42483, + "paid_rank": 3, + "role": 1533, + "to": 591 + }, + { + "augmented_rank": 4, + "donor_rank": 3, + "donors": 3, + "from": 541, + "in_span": false, + "literal_index": 44249, + "paid_rank": 1, + "role": 1550, + "to": 543 + }, + { + "augmented_rank": 9, + "donor_rank": 8, + "donors": 8, + "from": 534, + "in_span": false, + "literal_index": 44258, + "paid_rank": 1, + "role": 1531, + "to": 541 + }, + { + "augmented_rank": 8, + "donor_rank": 7, + "donors": 7, + "from": 1091, + "in_span": false, + "literal_index": 45607, + "paid_rank": 4, + "role": 1551, + "to": 267 + }, + { + "augmented_rank": 24, + "donor_rank": 23, + "donors": 24, + "from": 260, + "in_span": false, + "literal_index": 45625, + "paid_rank": 1, + "role": 1540, + "to": 1091 + } + ], + "replay_core_sha256": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "scientific_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "scope_exhausted": true, + "word_sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +} diff --git a/research/p104-owned-move-destination-span/receipts/independent/PAIRS.json b/research/p104-owned-move-destination-span/receipts/independent/PAIRS.json new file mode 100644 index 0000000000..2d0387cd70 --- /dev/null +++ b/research/p104-owned-move-destination-span/receipts/independent/PAIRS.json @@ -0,0 +1,653 @@ +{ + "checked_copies": 1, + "controls": { + "dependent_positive_and_negative": true, + "positive_signed_coefficients": [ + "1", + "-1" + ], + "same_support_sign_mutation_rejected": true + }, + "exact_zero_moves": [], + "fallback_bound_complete": true, + "fallback_sites_with_three_or_more_donors": 39, + "fallback_whole_rank_upper_before_new_work": 1683, + "first_unvisited_literal_index": null, + "first_unvisited_owned_move_index": null, + "fresh_zero_moves": 0, + "literal_events": 76443, + "literal_events_visited": 76443, + "matches": 0, + "nonzero_owned_clears": 69, + "owned_lifetimes": 70, + "paid_owned_histogram": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "paid_owned_moves": 47, + "peak_owned": 49, + "rank_one_pairs": 10, + "records": [ + { + "dependent_pairs": 0, + "destination_live_roles": 25, + "from": 477, + "literal_index": 30527, + "matches": [], + "nonzero_donors": 25, + "paid_rank": 4, + "pairs": 300, + "role": 1510, + "to": 1090, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 3, + "from": 1090, + "literal_index": 30535, + "matches": [], + "nonzero_donors": 2, + "paid_rank": 1, + "pairs": 1, + "role": 1520, + "to": 470, + "zero_donors": 1 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 3, + "from": 470, + "literal_index": 30549, + "matches": [], + "nonzero_donors": 3, + "paid_rank": 2, + "pairs": 3, + "role": 1521, + "to": 601, + "zero_donors": 0 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 7, + "from": 601, + "literal_index": 30579, + "matches": [], + "nonzero_donors": 5, + "paid_rank": 2, + "pairs": 10, + "role": 1547, + "to": 470, + "zero_donors": 2 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 27, + "from": 470, + "literal_index": 30591, + "matches": [], + "nonzero_donors": 26, + "paid_rank": 1, + "pairs": 325, + "role": 1546, + "to": 1090, + "zero_donors": 1 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 12, + "from": 267, + "literal_index": 32937, + "matches": [], + "nonzero_donors": 12, + "paid_rank": 4, + "pairs": 66, + "role": 1529, + "to": 1091, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 7, + "from": 543, + "literal_index": 33123, + "matches": [], + "nonzero_donors": 7, + "paid_rank": 1, + "pairs": 21, + "role": 1528, + "to": 541, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 9, + "from": 1091, + "literal_index": 33131, + "matches": [], + "nonzero_donors": 8, + "paid_rank": 1, + "pairs": 28, + "role": 1514, + "to": 260, + "zero_donors": 1 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 2, + "from": 541, + "literal_index": 33138, + "matches": [], + "nonzero_donors": 2, + "paid_rank": 1, + "pairs": 1, + "role": 1502, + "to": 534, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 14, + "from": 534, + "literal_index": 33140, + "matches": [], + "nonzero_donors": 14, + "paid_rank": 1, + "pairs": 91, + "role": 1502, + "to": 117, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 4, + "from": 117, + "literal_index": 33147, + "matches": [], + "nonzero_donors": 4, + "paid_rank": 4, + "pairs": 6, + "role": 1502, + "to": 594, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 12, + "from": 517, + "literal_index": 34512, + "matches": [], + "nonzero_donors": 12, + "paid_rank": 4, + "pairs": 66, + "role": 1513, + "to": 243, + "zero_donors": 0 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 5, + "from": 243, + "literal_index": 34516, + "matches": [], + "nonzero_donors": 4, + "paid_rank": 1, + "pairs": 6, + "role": 1518, + "to": 431, + "zero_donors": 1 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 9, + "from": 599, + "literal_index": 35138, + "matches": [], + "nonzero_donors": 9, + "paid_rank": 2, + "pairs": 36, + "role": 1541, + "to": 260, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 4, + "from": 431, + "literal_index": 35429, + "matches": [], + "nonzero_donors": 4, + "paid_rank": 2, + "pairs": 6, + "role": 1519, + "to": 600, + "zero_donors": 0 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 6, + "from": 600, + "literal_index": 35434, + "matches": [], + "nonzero_donors": 5, + "paid_rank": 2, + "pairs": 10, + "role": 1545, + "to": 431, + "zero_donors": 1 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 22, + "from": 431, + "literal_index": 35438, + "matches": [], + "nonzero_donors": 21, + "paid_rank": 1, + "pairs": 210, + "role": 1544, + "to": 243, + "zero_donors": 1 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 19, + "from": 518, + "literal_index": 36307, + "matches": [], + "nonzero_donors": 18, + "paid_rank": 4, + "pairs": 153, + "role": 1512, + "to": 240, + "zero_donors": 1 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 5, + "from": 240, + "literal_index": 36311, + "matches": [], + "nonzero_donors": 2, + "paid_rank": 1, + "pairs": 1, + "role": 1516, + "to": 394, + "zero_donors": 3 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 3, + "from": 394, + "literal_index": 36319, + "matches": [], + "nonzero_donors": 3, + "paid_rank": 2, + "pairs": 3, + "role": 1517, + "to": 598, + "zero_donors": 0 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 7, + "from": 598, + "literal_index": 36329, + "matches": [], + "nonzero_donors": 5, + "paid_rank": 2, + "pairs": 10, + "role": 1543, + "to": 394, + "zero_donors": 2 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 20, + "from": 394, + "literal_index": 36341, + "matches": [], + "nonzero_donors": 19, + "paid_rank": 1, + "pairs": 171, + "role": 1542, + "to": 240, + "zero_donors": 1 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 13, + "from": 243, + "literal_index": 39532, + "matches": [], + "nonzero_donors": 13, + "paid_rank": 4, + "pairs": 78, + "role": 1539, + "to": 517, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 12, + "from": 240, + "literal_index": 39559, + "matches": [], + "nonzero_donors": 12, + "paid_rank": 4, + "pairs": 66, + "role": 1538, + "to": 518, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 7, + "from": 531, + "literal_index": 39705, + "matches": [], + "nonzero_donors": 6, + "paid_rank": 1, + "pairs": 15, + "role": 1526, + "to": 529, + "zero_donors": 1 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 4, + "from": 529, + "literal_index": 39763, + "matches": [], + "nonzero_donors": 4, + "paid_rank": 1, + "pairs": 6, + "role": 1548, + "to": 531, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 1, + "from": 529, + "literal_index": 39792, + "matches": [], + "nonzero_donors": 1, + "paid_rank": 1, + "pairs": 0, + "role": 1503, + "to": 520, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 11, + "from": 520, + "literal_index": 39798, + "matches": [], + "nonzero_donors": 11, + "paid_rank": 5, + "pairs": 55, + "role": 1503, + "to": 595, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 2, + "from": 260, + "literal_index": 39831, + "matches": [], + "nonzero_donors": 2, + "paid_rank": 2, + "pairs": 1, + "role": 1515, + "to": 599, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 1, + "from": 595, + "literal_index": 39853, + "matches": [], + "nonzero_donors": 1, + "paid_rank": 5, + "pairs": 0, + "role": 1532, + "to": 520, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 13, + "from": 520, + "literal_index": 39862, + "matches": [], + "nonzero_donors": 13, + "paid_rank": 1, + "pairs": 78, + "role": 1532, + "to": 529, + "zero_donors": 0 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 2, + "from": 549, + "literal_index": 40518, + "matches": [], + "nonzero_donors": 2, + "paid_rank": 1, + "pairs": 1, + "role": 1549, + "to": 559, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 11, + "from": 559, + "literal_index": 40536, + "matches": [], + "nonzero_donors": 9, + "paid_rank": 1, + "pairs": 36, + "role": 1527, + "to": 549, + "zero_donors": 2 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 11, + "from": 549, + "literal_index": 40543, + "matches": [], + "nonzero_donors": 11, + "paid_rank": 2, + "pairs": 55, + "role": 1501, + "to": 115, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 6, + "from": 115, + "literal_index": 40547, + "matches": [], + "nonzero_donors": 6, + "paid_rank": 4, + "pairs": 15, + "role": 1501, + "to": 593, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 13, + "from": 1090, + "literal_index": 41474, + "matches": [], + "nonzero_donors": 13, + "paid_rank": 4, + "pairs": 78, + "role": 1537, + "to": 477, + "zero_donors": 0 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 9, + "from": 593, + "literal_index": 41629, + "matches": [], + "nonzero_donors": 9, + "paid_rank": 6, + "pairs": 36, + "role": 1530, + "to": 549, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 15, + "from": 594, + "literal_index": 41988, + "matches": [], + "nonzero_donors": 15, + "paid_rank": 4, + "pairs": 105, + "role": 1531, + "to": 117, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 17, + "from": 591, + "literal_index": 42460, + "matches": [], + "nonzero_donors": 17, + "paid_rank": 3, + "pairs": 136, + "role": 1504, + "to": 1031, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 3, + "from": 1031, + "literal_index": 42465, + "matches": [], + "nonzero_donors": 3, + "paid_rank": 4, + "pairs": 3, + "role": 1504, + "to": 597, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 17, + "from": 597, + "literal_index": 42470, + "matches": [], + "nonzero_donors": 17, + "paid_rank": 4, + "pairs": 136, + "role": 1533, + "to": 1031, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 6, + "from": 1031, + "literal_index": 42483, + "matches": [], + "nonzero_donors": 6, + "paid_rank": 3, + "pairs": 15, + "role": 1533, + "to": 591, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 3, + "from": 541, + "literal_index": 44249, + "matches": [], + "nonzero_donors": 3, + "paid_rank": 1, + "pairs": 3, + "role": 1550, + "to": 543, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 1, + "from": 117, + "literal_index": 44256, + "matches": [], + "nonzero_donors": 1, + "paid_rank": 1, + "pairs": 0, + "role": 1531, + "to": 534, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 8, + "from": 534, + "literal_index": 44258, + "matches": [], + "nonzero_donors": 8, + "paid_rank": 1, + "pairs": 28, + "role": 1531, + "to": 541, + "zero_donors": 0 + }, + { + "dependent_pairs": 0, + "destination_live_roles": 7, + "from": 1091, + "literal_index": 45607, + "matches": [], + "nonzero_donors": 7, + "paid_rank": 4, + "pairs": 21, + "role": 1551, + "to": 267, + "zero_donors": 0 + }, + { + "dependent_pairs": 1, + "destination_live_roles": 24, + "from": 260, + "literal_index": 45625, + "matches": [], + "nonzero_donors": 24, + "paid_rank": 1, + "pairs": 276, + "role": 1540, + "to": 1091, + "zero_donors": 0 + } + ], + "replay_core_sha256": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "scientific_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "scope_exhausted": true, + "sites_with_pairs": 44, + "two_donor_pairs": 2767, + "word_sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +} diff --git a/research/p104-owned-move-destination-span/receipts/pairs/PRICE.json b/research/p104-owned-move-destination-span/receipts/pairs/PRICE.json new file mode 100644 index 0000000000..0a46f5e3b3 --- /dev/null +++ b/research/p104-owned-move-destination-span/receipts/pairs/PRICE.json @@ -0,0 +1,515 @@ +{ + "baseline_interval": [ + "-1002247197758299781/500000000000000000000000000000000000000000000000", + "-2004494395516543389/1000000000000000000000000000000000000000000000000" + ], + "cap": 2767, + "copies": 17, + "crossing_upper": "91141748217473298207420876011401/25000000000000000000000000000000000", + "eligible_sites": 44, + "grant": "Remove each eligible owned MOVE once across all copies, granting all other costs free.", + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "local_change_per_copy": { + "add_ADD": 1, + "add_CLEAR": 1, + "add_COPY": 1, + "add_INIT": 1, + "net_literal_events": 3, + "new_owner_slots": 0, + "remove_MOVE": 1 + }, + "original_paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5882, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "original_productive": { + "1": 306, + "2": 357, + "3": 799, + "4": 3808, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10905, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "pairs": 2767, + "pins": { + "round30/complex/audit.py": "67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb", + "round30/complex/source/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "round30/complex/source/inputs/EARLY-RESULT.json": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "round30/complex/source/powers.py": "c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee", + "round41/independent/RESULT.json": "1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7", + "round41/independent/replay_core.py": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "round41/lead/r41-price-support/PRICE.json": "1efe8b52e02a8db0ac6a04cdf6b943e515badee5fc0b7bea6ea3fe4a30fd1d01", + "round41/lead/r41-price-support/SUPPORT.json": "c31c8425e2a99fe15a9ffa48662dacca4eda2b778d55ceceae2978a9bdb12f3c" + }, + "seconds_cap": 120, + "sites": [ + { + "clock": 30527, + "destination": 1090, + "nonzero_donors": 25, + "pairs": 300, + "rank": 4, + "role": 1510, + "source": 477 + }, + { + "clock": 30535, + "destination": 470, + "nonzero_donors": 2, + "pairs": 1, + "rank": 1, + "role": 1520, + "source": 1090 + }, + { + "clock": 30549, + "destination": 601, + "nonzero_donors": 3, + "pairs": 3, + "rank": 2, + "role": 1521, + "source": 470 + }, + { + "clock": 30579, + "destination": 470, + "nonzero_donors": 5, + "pairs": 10, + "rank": 2, + "role": 1547, + "source": 601 + }, + { + "clock": 30591, + "destination": 1090, + "nonzero_donors": 26, + "pairs": 325, + "rank": 1, + "role": 1546, + "source": 470 + }, + { + "clock": 32937, + "destination": 1091, + "nonzero_donors": 12, + "pairs": 66, + "rank": 4, + "role": 1529, + "source": 267 + }, + { + "clock": 33123, + "destination": 541, + "nonzero_donors": 7, + "pairs": 21, + "rank": 1, + "role": 1528, + "source": 543 + }, + { + "clock": 33131, + "destination": 260, + "nonzero_donors": 8, + "pairs": 28, + "rank": 1, + "role": 1514, + "source": 1091 + }, + { + "clock": 33138, + "destination": 534, + "nonzero_donors": 2, + "pairs": 1, + "rank": 1, + "role": 1502, + "source": 541 + }, + { + "clock": 33140, + "destination": 117, + "nonzero_donors": 14, + "pairs": 91, + "rank": 1, + "role": 1502, + "source": 534 + }, + { + "clock": 33147, + "destination": 594, + "nonzero_donors": 4, + "pairs": 6, + "rank": 4, + "role": 1502, + "source": 117 + }, + { + "clock": 34512, + "destination": 243, + "nonzero_donors": 12, + "pairs": 66, + "rank": 4, + "role": 1513, + "source": 517 + }, + { + "clock": 34516, + "destination": 431, + "nonzero_donors": 4, + "pairs": 6, + "rank": 1, + "role": 1518, + "source": 243 + }, + { + "clock": 35138, + "destination": 260, + "nonzero_donors": 9, + "pairs": 36, + "rank": 2, + "role": 1541, + "source": 599 + }, + { + "clock": 35429, + "destination": 600, + "nonzero_donors": 4, + "pairs": 6, + "rank": 2, + "role": 1519, + "source": 431 + }, + { + "clock": 35434, + "destination": 431, + "nonzero_donors": 5, + "pairs": 10, + "rank": 2, + "role": 1545, + "source": 600 + }, + { + "clock": 35438, + "destination": 243, + "nonzero_donors": 21, + "pairs": 210, + "rank": 1, + "role": 1544, + "source": 431 + }, + { + "clock": 36307, + "destination": 240, + "nonzero_donors": 18, + "pairs": 153, + "rank": 4, + "role": 1512, + "source": 518 + }, + { + "clock": 36311, + "destination": 394, + "nonzero_donors": 2, + "pairs": 1, + "rank": 1, + "role": 1516, + "source": 240 + }, + { + "clock": 36319, + "destination": 598, + "nonzero_donors": 3, + "pairs": 3, + "rank": 2, + "role": 1517, + "source": 394 + }, + { + "clock": 36329, + "destination": 394, + "nonzero_donors": 5, + "pairs": 10, + "rank": 2, + "role": 1543, + "source": 598 + }, + { + "clock": 36341, + "destination": 240, + "nonzero_donors": 19, + "pairs": 171, + "rank": 1, + "role": 1542, + "source": 394 + }, + { + "clock": 39532, + "destination": 517, + "nonzero_donors": 13, + "pairs": 78, + "rank": 4, + "role": 1539, + "source": 243 + }, + { + "clock": 39559, + "destination": 518, + "nonzero_donors": 12, + "pairs": 66, + "rank": 4, + "role": 1538, + "source": 240 + }, + { + "clock": 39705, + "destination": 529, + "nonzero_donors": 6, + "pairs": 15, + "rank": 1, + "role": 1526, + "source": 531 + }, + { + "clock": 39763, + "destination": 531, + "nonzero_donors": 4, + "pairs": 6, + "rank": 1, + "role": 1548, + "source": 529 + }, + { + "clock": 39792, + "destination": 520, + "nonzero_donors": 1, + "pairs": 0, + "rank": 1, + "role": 1503, + "source": 529 + }, + { + "clock": 39798, + "destination": 595, + "nonzero_donors": 11, + "pairs": 55, + "rank": 5, + "role": 1503, + "source": 520 + }, + { + "clock": 39831, + "destination": 599, + "nonzero_donors": 2, + "pairs": 1, + "rank": 2, + "role": 1515, + "source": 260 + }, + { + "clock": 39853, + "destination": 520, + "nonzero_donors": 1, + "pairs": 0, + "rank": 5, + "role": 1532, + "source": 595 + }, + { + "clock": 39862, + "destination": 529, + "nonzero_donors": 13, + "pairs": 78, + "rank": 1, + "role": 1532, + "source": 520 + }, + { + "clock": 40518, + "destination": 559, + "nonzero_donors": 2, + "pairs": 1, + "rank": 1, + "role": 1549, + "source": 549 + }, + { + "clock": 40536, + "destination": 549, + "nonzero_donors": 9, + "pairs": 36, + "rank": 1, + "role": 1527, + "source": 559 + }, + { + "clock": 40543, + "destination": 115, + "nonzero_donors": 11, + "pairs": 55, + "rank": 2, + "role": 1501, + "source": 549 + }, + { + "clock": 40547, + "destination": 593, + "nonzero_donors": 6, + "pairs": 15, + "rank": 4, + "role": 1501, + "source": 115 + }, + { + "clock": 41474, + "destination": 477, + "nonzero_donors": 13, + "pairs": 78, + "rank": 4, + "role": 1537, + "source": 1090 + }, + { + "clock": 41629, + "destination": 549, + "nonzero_donors": 9, + "pairs": 36, + "rank": 6, + "role": 1530, + "source": 593 + }, + { + "clock": 41988, + "destination": 117, + "nonzero_donors": 15, + "pairs": 105, + "rank": 4, + "role": 1531, + "source": 594 + }, + { + "clock": 42460, + "destination": 1031, + "nonzero_donors": 17, + "pairs": 136, + "rank": 3, + "role": 1504, + "source": 591 + }, + { + "clock": 42465, + "destination": 597, + "nonzero_donors": 3, + "pairs": 3, + "rank": 4, + "role": 1504, + "source": 1031 + }, + { + "clock": 42470, + "destination": 1031, + "nonzero_donors": 17, + "pairs": 136, + "rank": 4, + "role": 1533, + "source": 597 + }, + { + "clock": 42483, + "destination": 591, + "nonzero_donors": 6, + "pairs": 15, + "rank": 3, + "role": 1533, + "source": 1031 + }, + { + "clock": 44249, + "destination": 543, + "nonzero_donors": 3, + "pairs": 3, + "rank": 1, + "role": 1550, + "source": 541 + }, + { + "clock": 44256, + "destination": 534, + "nonzero_donors": 1, + "pairs": 0, + "rank": 1, + "role": 1531, + "source": 117 + }, + { + "clock": 44258, + "destination": 541, + "nonzero_donors": 8, + "pairs": 28, + "rank": 1, + "role": 1531, + "source": 534 + }, + { + "clock": 45607, + "destination": 267, + "nonzero_donors": 7, + "pairs": 21, + "rank": 4, + "role": 1551, + "source": 1091 + }, + { + "clock": 45625, + "destination": 1091, + "nonzero_donors": 24, + "pairs": 276, + "rank": 1, + "role": 1540, + "source": 260 + } + ], + "whole_optimistic_upper": { + "complete_margin_interval": [ + "889101091282339444219122183492913276425281478218609/500000000000000000000000000000000000000000000000", + "71128087302587155537529774679433062114022518259737/40000000000000000000000000000000000000000000000" + ], + "removed_ranks_per_copy": { + "1": 18, + "2": 9, + "3": 2, + "4": 13, + "5": 1, + "6": 1 + }, + "saving_interval": [ + "55568818205146215263695136468307142417029952282393/31250000000000000000000000000000000000000000000", + "889101091282339444219122183492914278672479236518509/500000000000000000000000000000000000000000000000" + ] + } +} diff --git a/research/p104-owned-move-destination-span/receipts/pairs/SUPPORT.json b/research/p104-owned-move-destination-span/receipts/pairs/SUPPORT.json new file mode 100644 index 0000000000..39302c4a58 --- /dev/null +++ b/research/p104-owned-move-destination-span/receipts/pairs/SUPPORT.json @@ -0,0 +1,217 @@ +{ + "controls": [ + "signed_rational_coefficients", + "off_pivot_sign_rejected", + "outside_union_rejected", + "dependent_pair_and_zero_coefficient_distinguished" + ], + "core_receipt": { + "checked_copies": 1, + "exact_zero_moves": [], + "first_unvisited_literal_index": null, + "first_unvisited_owned_move_index": null, + "fresh_zero_moves": 0, + "literal_events": 76443, + "literal_events_visited": 76443, + "nonzero_owned_clears": 69, + "owned_lifetimes": 70, + "paid_owned_histogram": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "paid_owned_moves": 47, + "peak_owned": 49, + "scope_exhausted": true + }, + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "pending_costs": [ + "lawful signed coefficients and physical phase", + "ordinary COPY/ADD and setup", + "ownership, dirty restoration, recovery, precision and tape", + "complete independent replay" + ], + "pins": { + "round30/complex/audit.py": "67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb", + "round30/complex/source/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "round30/complex/source/inputs/EARLY-RESULT.json": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "round30/complex/source/powers.py": "c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee", + "round41/independent/RESULT.json": "1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7", + "round41/independent/replay_core.py": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "round41/lead/r41-price-support/PRICE.json": "1efe8b52e02a8db0ac6a04cdf6b943e515badee5fc0b7bea6ea3fe4a30fd1d01", + "round41/lead/r41-price-support/SUPPORT.json": "c31c8425e2a99fe15a9ffa48662dacca4eda2b778d55ceceae2978a9bdb12f3c" + }, + "price_sha256": "34468ff846c336db7d712ec8bccdf2c659e167baf935bf63bb6eb463898d8e45", + "scope_exhausted": true, + "site_status_counts": { + "30527": { + "nonzero_residual": 300 + }, + "30535": { + "nonzero_residual": 1 + }, + "30549": { + "dependent": 1, + "nonzero_residual": 2 + }, + "30579": { + "dependent": 1, + "nonzero_residual": 9 + }, + "30591": { + "nonzero_residual": 325 + }, + "32937": { + "nonzero_residual": 66 + }, + "33123": { + "nonzero_residual": 21 + }, + "33131": { + "nonzero_residual": 28 + }, + "33138": { + "nonzero_residual": 1 + }, + "33140": { + "nonzero_residual": 91 + }, + "33147": { + "nonzero_residual": 6 + }, + "34512": { + "nonzero_residual": 66 + }, + "34516": { + "dependent": 1, + "nonzero_residual": 5 + }, + "35138": { + "dependent": 1, + "nonzero_residual": 35 + }, + "35429": { + "nonzero_residual": 6 + }, + "35434": { + "dependent": 1, + "nonzero_residual": 9 + }, + "35438": { + "nonzero_residual": 210 + }, + "36307": { + "nonzero_residual": 153 + }, + "36311": { + "nonzero_residual": 1 + }, + "36319": { + "dependent": 1, + "nonzero_residual": 2 + }, + "36329": { + "dependent": 1, + "nonzero_residual": 9 + }, + "36341": { + "nonzero_residual": 171 + }, + "39532": { + "nonzero_residual": 78 + }, + "39559": { + "nonzero_residual": 66 + }, + "39705": { + "nonzero_residual": 15 + }, + "39763": { + "nonzero_residual": 6 + }, + "39792": {}, + "39798": { + "nonzero_residual": 55 + }, + "39831": { + "nonzero_residual": 1 + }, + "39853": {}, + "39862": { + "nonzero_residual": 78 + }, + "40518": { + "dependent": 1 + }, + "40536": { + "nonzero_residual": 36 + }, + "40543": { + "nonzero_residual": 55 + }, + "40547": { + "nonzero_residual": 15 + }, + "41474": { + "nonzero_residual": 78 + }, + "41629": { + "dependent": 1, + "nonzero_residual": 35 + }, + "41988": { + "nonzero_residual": 105 + }, + "42460": { + "nonzero_residual": 136 + }, + "42465": { + "nonzero_residual": 3 + }, + "42470": { + "nonzero_residual": 136 + }, + "42483": { + "nonzero_residual": 15 + }, + "44249": { + "nonzero_residual": 3 + }, + "44256": {}, + "44258": { + "nonzero_residual": 28 + }, + "45607": { + "nonzero_residual": 21 + }, + "45625": { + "dependent": 1, + "nonzero_residual": 275 + } + }, + "status": "excluded", + "status_counts": { + "dependent": 10, + "nonzero_residual": 2757 + }, + "support_witnesses": [], + "surviving_sites": 0, + "unvisited_by_clock": {}, + "unvisited_pairs": 0, + "visited_pairs": 2767, + "whole_post_support_optimistic_upper": { + "complete_margin_interval": [ + "-1002247197758299781/500000000000000000000000000000000000000000000000", + "-2004494395516543389/1000000000000000000000000000000000000000000000000" + ], + "removed_ranks_per_copy": {}, + "saving_interval": [ + "0", + "0" + ] + } +} diff --git a/research/p104-owned-move-destination-span/replay.py b/research/p104-owned-move-destination-span/replay.py new file mode 100644 index 0000000000..d6bf4b2035 --- /dev/null +++ b/research/p104-owned-move-destination-span/replay.py @@ -0,0 +1,98 @@ +"""Replay exact donor exclusion, complete invoice and controls on a sealed word.""" +from argparse import ArgumentParser +import gzip +from hashlib import sha1, sha256 +import json +from pathlib import Path, PurePosixPath +import shutil +import subprocess +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +WORD = "round30/complex/source/inputs/WORD.json.gz" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" + + +def unique(items): + value = dict(items) + if len(value) != len(items): + raise ValueError("duplicate JSON key") + return value + + +def decode(raw): + return json.loads(raw, object_pairs_hook=unique) + + +def matches(actual, expected): + assert decode(actual) == decode(expected.read_bytes()), expected.name + + +def subprocess_replay(script, *args): + result = subprocess.run([sys.executable, "-I", "-B", str(script), *map(str, args)], + check=True, capture_output=True) + return result.stdout + + +def authenticate(scratch): + pins = decode((HERE / "LOCAL-PINS.json").read_bytes()) + for key, digest in pins.items(): + path = PurePosixPath(key) + if path.is_absolute() or ".." in path.parts or path.as_posix() != key: + raise ValueError(f"invalid dependency path {key}") + if sha256((HERE / key).read_bytes()).hexdigest() != digest: + raise ValueError(f"changed dependency {key}") + provenance = decode((HERE / "PROVENANCE.json").read_bytes())["files"] + assert set(provenance) == { + "dependencies/" + WORD, + "dependencies/round30/complex/source/inputs/CALLER.json.gz", + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz", + } + for key, pin in provenance.items(): + assert key in pins + raw = (HERE / key).read_bytes() + if pin["uncompress"]: + raw = gzip.decompress(raw) + (scratch / key).with_suffix("").write_bytes(raw) + assert sha256(raw).hexdigest() == pin["sha256"], key + assert sha1(f"blob {len(raw)}\0".encode() + raw).hexdigest() == pin["git_blob"], key + assert provenance["dependencies/" + WORD]["commit"] == HEAD + + +def run(): + with TemporaryDirectory(prefix="p104-destination-span-") as temp: + scratch = Path(temp) + deps = scratch / "dependencies" + shutil.copytree(HERE / "dependencies", deps) + authenticate(scratch) + indep = deps / "round41/independent" + word = deps / WORD + matches(subprocess_replay(indep / "donor_replay.py", "--word", word), indep / "RESULT.json") + pair = scratch / "pair" + subprocess_replay(HERE / "engines/pairs.py", deps / "round30", deps / "round41", pair) + matches(subprocess_replay(indep / "replay_pairs.py", "--word", word), + HERE / "receipts/independent/PAIRS.json") + full = scratch / "full" + subprocess_replay(HERE / "engines/fullbank.py", deps, full) + matches(subprocess_replay(indep / "replay_bank.py", "--word", word), + HERE / "receipts/independent/BANK.json") + for path, scope in ((pair, "pairs"), (full, "fullbank")): + for name in ("PRICE.json", "SUPPORT.json"): + matches((path / name).read_bytes(), HERE / "receipts" / scope / name) + pair_result = decode((pair / "SUPPORT.json").read_bytes()) + report = decode((full / "SUPPORT.json").read_bytes()) + rows = report["rows"] + assert len(rows) == 47 and sum(len(r["donors"]) for r in rows) == 424 + assert all(r["kind"] == "separating_dual" for r in rows) + assert not report["matches"] and not report["unvisited_moves"] + assert pair_result["visited_pairs"] == 2767 and pair_result["unvisited_pairs"] == 0 + assert report["optimistic_saving_upper_after_support"] == "0" + print("PASS_OWNED_MOVE_DESTINATION_SPAN moves=47 donors=424 pairs=2767 duals=47 independent_large_ranks=39 unresolved=0 saving_upper=0 kappa_change=0") + + +if __name__ == "__main__": + assert __debug__, "run with assertions enabled" + parser = ArgumentParser(description=__doc__) + parser.parse_args() + run()