From bb36fc65ee0b161229169505f4840c436c5ca2b9 Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 14:22:27 +1100 Subject: [PATCH 1/3] Reuse #7147 selected replay navigation for onboarding This is the exact documentation prerequisite retained by #7156. It points the onboarding check to the selected #7000/#7001 review. Credit to Rohan Arun and the source authors. --- docs/ci-verification.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). From d2e54af81f9dda6487636b79d4964a2385d89b2b Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 21:53:51 +1100 Subject: [PATCH 2/3] Replay the historical selected check at its inspected commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The PR #6292 rejection census and package plan are statements about 2485805. Load its exact sources and planner in a private sparse checkout, keeping all source hashes, 19 expected rejections, nine package selections and the empty-plan control. Subsequent edits to the live Makefile and CI guide no longer invalidate this historical check. The original audit is by unpaidmoon, building on Dennis’s historical replay gate. The pinned repository view follows the precedent of Matarener’s PR #5434. Repair prepared with substantial OpenAI Codex assistance. --- .../historical-selected-replay-gap/README.md | 6 +- .../SOURCES.json | 60 +++++++++--------- .../VERIFY.json | 31 +-------- .../historical-selected-replay-gap/verify.py | 63 ++++++++++++++----- 4 files changed, 82 insertions(+), 78 deletions(-) diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9") From e19556382c7162edbee3fe37d06dd1e6a8a2f8c1 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 13:47:37 -0800 Subject: [PATCH 3/3] Exclude two simultaneous Type B phase transfers --- .../LOCAL-PINS.json | 22 + .../p104-two-type-b-phase-transfers/NOTICE | 8 + .../p104-two-type-b-phase-transfers/PROOF.md | 17 + .../PROVENANCE.json | 45 + .../p104-two-type-b-phase-transfers/README.md | 31 + .../SOURCES.json | 18 + .../p104-two-type-b-phase-transfers/TASK.json | 84 ++ .../VERIFY.json | 19 + .../admission/ADMITTED.json | 48 + .../admission/ANCHORED.json | 34 + .../admission/ARCHIVE.stdout | 47 + .../admission/COMMIT.stdout | 1 + .../admission/DECLARED-SOURCE-PINS.json | 35 + .../admission/HISTORY.stderr | 1 + .../admission/METADATA.stdout | 1 + .../admission/STAGE-caller.json | 62 + .../admission/STAGE-early.json | 15 + .../admission/STAGE-frontier.json | 16 + .../admission/STAGE-native.json | 37 + .../admission/TREE.txt | 34 + .../engines/compare.py | 47 + .../engines/four_edits.py | 242 ++++ .../engines/two_phase.py | 259 ++++ .../inputs/7113/CALLER.json.gz | Bin 0 -> 11215 bytes .../inputs/7298/pricing.py | 82 ++ .../inputs/7314/EARLY-RESULT.json | 206 +++ .../inputs/r52/screen.py | 360 +++++ .../inputs/r56/PRICE.json | 1159 +++++++++++++++++ .../receipts/INDEPENDENT-SUMMARY.json | 10 + .../receipts/SHA256.json | 6 + .../p104-two-type-b-phase-transfers/replay.py | 127 ++ 31 files changed, 3073 insertions(+) create mode 100644 research/p104-two-type-b-phase-transfers/LOCAL-PINS.json create mode 100644 research/p104-two-type-b-phase-transfers/NOTICE create mode 100644 research/p104-two-type-b-phase-transfers/PROOF.md create mode 100644 research/p104-two-type-b-phase-transfers/PROVENANCE.json create mode 100644 research/p104-two-type-b-phase-transfers/README.md create mode 100644 research/p104-two-type-b-phase-transfers/SOURCES.json create mode 100644 research/p104-two-type-b-phase-transfers/TASK.json create mode 100644 research/p104-two-type-b-phase-transfers/VERIFY.json create mode 100644 research/p104-two-type-b-phase-transfers/admission/ADMITTED.json create mode 100644 research/p104-two-type-b-phase-transfers/admission/ANCHORED.json create mode 100644 research/p104-two-type-b-phase-transfers/admission/ARCHIVE.stdout create mode 100644 research/p104-two-type-b-phase-transfers/admission/COMMIT.stdout create mode 100644 research/p104-two-type-b-phase-transfers/admission/DECLARED-SOURCE-PINS.json create mode 100644 research/p104-two-type-b-phase-transfers/admission/HISTORY.stderr create mode 100644 research/p104-two-type-b-phase-transfers/admission/METADATA.stdout create mode 100644 research/p104-two-type-b-phase-transfers/admission/STAGE-caller.json create mode 100644 research/p104-two-type-b-phase-transfers/admission/STAGE-early.json create mode 100644 research/p104-two-type-b-phase-transfers/admission/STAGE-frontier.json create mode 100644 research/p104-two-type-b-phase-transfers/admission/STAGE-native.json create mode 100644 research/p104-two-type-b-phase-transfers/admission/TREE.txt create mode 100644 research/p104-two-type-b-phase-transfers/engines/compare.py create mode 100644 research/p104-two-type-b-phase-transfers/engines/four_edits.py create mode 100644 research/p104-two-type-b-phase-transfers/engines/two_phase.py create mode 100644 research/p104-two-type-b-phase-transfers/inputs/7113/CALLER.json.gz create mode 100644 research/p104-two-type-b-phase-transfers/inputs/7298/pricing.py create mode 100644 research/p104-two-type-b-phase-transfers/inputs/7314/EARLY-RESULT.json create mode 100644 research/p104-two-type-b-phase-transfers/inputs/r52/screen.py create mode 100644 research/p104-two-type-b-phase-transfers/inputs/r56/PRICE.json create mode 100644 research/p104-two-type-b-phase-transfers/receipts/INDEPENDENT-SUMMARY.json create mode 100644 research/p104-two-type-b-phase-transfers/receipts/SHA256.json create mode 100644 research/p104-two-type-b-phase-transfers/replay.py diff --git a/research/p104-two-type-b-phase-transfers/LOCAL-PINS.json b/research/p104-two-type-b-phase-transfers/LOCAL-PINS.json new file mode 100644 index 0000000000..27c4564a2f --- /dev/null +++ b/research/p104-two-type-b-phase-transfers/LOCAL-PINS.json @@ -0,0 +1,22 @@ +{ + "admission/ADMITTED.json": "41b8a189dffeb768e5843446cdc469f9cc2f0aa038d0a593cf2be43aa009a9a3", + "admission/ANCHORED.json": "6378aff76d6d38b3863d039b2d1814db48c3105ffe933e96d9c449e799f624aa", + "admission/ARCHIVE.stdout": "fbfe4d32b4b7614ec0adbcf31d788706c305fa85c88db34822daa3e057b85599", + "admission/COMMIT.stdout": "fd1d72b0397b2e089e9e6ae467c9322a96a08628d7d511c68b417203b5b4cee8", + "admission/DECLARED-SOURCE-PINS.json": "aad96b05ba3fb91051f310120c1d32729d4fd6cf20395943c4aea4fcf1d2d4d4", + "admission/HISTORY.stderr": "c95523eb2c5d47834d66c8568f1d755cf2201e8a23b18ec0e1a5c3fab0eb9b74", + "admission/METADATA.stdout": "5873404cb4424dca918a00d503569f3c29a3190fd029a007e1afb2006399f647", + "admission/STAGE-caller.json": "a653be3423a20a9aa0b6c532fabf7bf96ea7e5feab6bd3924d171d2b9c5c5f76", + "admission/STAGE-early.json": "cee13f7126ecdd375ad62b4a6773f3ac4182df52bc484dc2944a92ee31cd15f7", + "admission/STAGE-frontier.json": "75b8ceb5547f9828b03d60b7646fc2fdb47a0d02b5715d8f7fb35d7de946694f", + "admission/STAGE-native.json": "36ec25be5eb332a45f36d935fc1d0397e02e0b243ea38cc77d340592a33c478b", + "admission/TREE.txt": "6b7c113f9b02b45024c96eafb88256b76a8d3b3d91a1c1730090ded0d3be7246", + "engines/compare.py": "d4e18444edfbaa278da140f961ac64f90497fca796bf7203fc6cfc24d3d0231d", + "engines/four_edits.py": "140c10fb4365bb5e254df5f9b0a7d89ad54b901ceaf36d528e2ff4baa4bd3c80", + "engines/two_phase.py": "ad3b5efd85a56c6c60c747cf45cbd1b7174ab9a714142ab069648261bcbf6631", + "inputs/7113/CALLER.json.gz": "58beaf24e01c0589ecd5d1676d6d27e75b779f089d0674eda11725465ffc04e1", + "inputs/7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/7314/EARLY-RESULT.json": "b5043855411432b24336ecc443cba9ebfae6392e2045ddd01c87cfe2c51f5f08", + "inputs/r52/screen.py": "cdf54b266ac31fd0efe544badbb9840598d4c63c4d3cd363f60ae9a74cc4b256", + "inputs/r56/PRICE.json": "6f3510db09e18278c0f18d8e0cbe1242fc48e999dafc87cb04cc87e240b93819" +} diff --git a/research/p104-two-type-b-phase-transfers/NOTICE b/research/p104-two-type-b-phase-transfers/NOTICE new file mode 100644 index 0000000000..83a17ba4c7 --- /dev/null +++ b/research/p104-two-type-b-phase-transfers/NOTICE @@ -0,0 +1,8 @@ +Apache-2.0. + +#7113 supplies the literal signed caller, #7314 the complete comparable +invoice, and #7298 the directed tariff. #7317 supplies single-transfer stock, +price and proof lineage; #7315 supplies the reused signed decoder. #7309 and +#7296 supply related pure-demotion and child-volume results. #3204 and #1324 +supply older four-site rigidity and simultaneous-axis precedents. +OpenAI Codex and subagents materially assisted. diff --git a/research/p104-two-type-b-phase-transfers/PROOF.md b/research/p104-two-type-b-phase-transfers/PROOF.md new file mode 100644 index 0000000000..d5e67c6467 --- /dev/null +++ b/research/p104-two-type-b-phase-transfers/PROOF.md @@ -0,0 +1,17 @@ +# Exact four-site endpoint obstruction + +## Necessary specialization and primary engine + +The original Type B word is a linear operator at each legal phase/body specialization. A uniform signed caller identity would hold at `q = −1` with all 17 body values equal to one. The edit at any chosen clock i multiplies its old role by the additional reflection `D_i = I − 2e_r e_r^T`. At this specialization the reflection commutes with the original idle gate, both for demotion and promotion. + +Let `F_i = G_i … G_1` be the chronological old prefix with `F_0 = I`. Define `R_i = F_(i−1)^−1 D_i F_(i−1)`. For the four ascending clocks the edited endpoint equals the old endpoint times `R_4 R_3 R_2 R_1`. Each `R_i` is an involution, so agreement requires `R_4 R_3 = R_1 R_2`. For `R_i = I − 2u_i v_i^T` the ordered product defect is `−2u_i v_i^T − 2u_j v_j^T + 4(v_j^T u_i)u_j v_i^T` for `R_j R_i`. The primary engine checks the old endpoint and inverse relation, denominator and inverse-pivot units, and every pair-product comparison modulo the verified prime 65,521. A nonzero residue excludes exact equality. + +## Independent exact endpoint engine + +The second engine uses no inverse or modular arithmetic. It replays each of the 36 original input columns and verifies the complete old endpoint. At each eligible clock i it records the old output on that role, immediately after the old idle. Separately it propagates one unit impulse from that output through the literal old suffix, recording its arrivals at all later sites and at the endpoint. + +The edited role output is the negative of its old-gate output on the actual incoming state. For each input column, let `b_j` be the old output at edited site j, `k_ij` the previously recorded arrival of impulse i at site j, and `δ_i` its injected difference. In ascending clock order, `δ_j = −2(b_j + Σ_(i 1: + new[clock] = (event[2] - offset, event[3]) + assert len(old) == 4 and len(new) == 26 + stock = old | new + assert all(0 <= role < n and len(set(mask)) == len(mask) and all(1 <= s <= 17 for s in mask) + for role, mask in stock.values()) + cases = sorted(tuple(sorted(odd + even)) for odd in combinations(old, 2) for even in combinations(new, 2)) + assert len(cases) == len(set(cases)) == CASE_LIMIT + priced = [] + for item in price['keys']: + assert len(item['odd']) == len(item['even']) == 2 + assert all(clock in old for clock in item['odd']) and all(clock in new for clock in item['even']) + shape = sorted(len(new[clock][1]) for clock in item['even']) + assert item['price'] == ','.join(map(str, shape)) and item['price'] in price['prices'] + priced.append(tuple(sorted(item['odd'] + item['even']))) + assert sorted(priced) == cases, 'price scope differs from literal caller' + gates = [decode(event, offset) for event in caller['events']] + data = old_trajectories(gates, {c: x[0] for c, x in stock.items()}, n, + [signed(x[0]) for x in block['diagonal']]) + records = [] + for key in cases: + if monotonic() - started >= SECONDS: + break + mismatch = first_difference(data, key, n) + if mismatch is None: + records.append({'key': key, 'first_difference': None}) + else: + col, row, value = mismatch + records.append({'key': key, 'first_difference': [col + offset, row + offset, str(value)]}) + unvisited = cases[len(records):] + return {'status': 'HIT_TIME_CAP' if unvisited else 'EXHAUSTED', 'cases': CASE_LIMIT, + 'comparator_head': COMPARATOR, 'caller_head': CALLER_HEAD, 'caller_sha256': CALLER_SHA, + 'admission_sha256': ADMISSION_SHA, 'price_sha256': price_sha, 'controls': control_result, + 'odd_clocks': sorted(old), 'even_clocks': sorted(new), 'old_endpoint_columns': n, + 'common_denominator': data[0], 'records': records, 'tested': len(records), + 'survivors': [r['key'] for r in records if r['first_difference'] is None], 'unvisited': unvisited} + + +def main(): + started = monotonic() + parser = ArgumentParser(description=__doc__) + parser.add_argument('--inputs', type=Path, default=Path('inputs')) + parser.add_argument('--price', type=Path) + parser.add_argument('--price-sha') + parser.add_argument('--controls-only', action='store_true') + args = parser.parse_args() + assert __debug__ + control_result = controls() + if args.controls_only: + print(json.dumps(control_result, sort_keys=True)) + return + if args.price is None or args.price_sha is None: + parser.error('authenticate the price-before-decoding receipt first') + price = authenticated_json(args.price, args.price_sha) + assert price['head'] == COMPARATOR and price['caller_head'] == CALLER_HEAD and price['copies'] == 17 + assert price['input_sha256']['inputs/7113/CALLER.json'] == CALLER_SHA + admission = authenticated_json(args.inputs / 'ADMITTED.json', ADMISSION_SHA) + assert admission['status'] == 'independently_reproduced_comparable' + assert admission['head'] == COMPARATOR and admission['caller_sha256'] == CALLER_SHA + caller = authenticated_json(args.inputs / 'CALLER.json', CALLER_SHA) + print(json.dumps(run(caller, control_result, price, args.price_sha, started), indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-two-type-b-phase-transfers/engines/two_phase.py b/research/p104-two-type-b-phase-transfers/engines/two_phase.py new file mode 100644 index 0000000000..b7ec038c45 --- /dev/null +++ b/research/p104-two-type-b-phase-transfers/engines/two_phase.py @@ -0,0 +1,259 @@ +"""Directed price and bounded two-transfer endpoint test on Type B.""" + +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction +from functools import cache +from hashlib import sha256 +from itertools import combinations +from json import dumps, loads +from math import isqrt +from pathlib import Path +from runpy import run_path +from time import monotonic + +HEAD = '9d0119eb12fbd9fa534b48cd37b68e7099757b91' +CALLER_HEAD = '07a76c5e2738882c0cb322278e56f6cae3c9885d' +ADMISSION = '41b8a189dffeb768e5843446cdc469f9cc2f0aa038d0a593cf2be43aa009a9a3' +PINS = { + 'admission/ADMITTED.json': ADMISSION, + 'inputs/7113/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'inputs/7298/pricing.py': 'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', + 'inputs/7314/EARLY-RESULT.json': 'b5043855411432b24336ecc443cba9ebfae6392e2045ddd01c87cfe2c51f5f08', + 'inputs/r52/screen.py': 'cdf54b266ac31fd0efe544badbb9840598d4c63c4d3cd363f60ae9a74cc4b256', + 'inputs/r56/PRICE.json': '6f3510db09e18278c0f18d8e0cbe1242fc48e999dafc87cb04cc87e240b93819', +} + + +def unique(items): + out = dict(items) + if len(out) != len(items): + raise ValueError('Duplicate JSON key') + return out + + +def decode(data): + return loads(data, object_pairs_hook=unique) + + +def authenticated(root): + files = {} + for path,digest in PINS.items(): + raw = (root/path).read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError(f'Changed input {path}') + files[path] = raw + a = decode(files['admission/ADMITTED.json']) + assert a['head'] == HEAD and a['caller_sha256'] == PINS['inputs/7113/CALLER.json'] + assert a['status'] == 'independently_reproduced_comparable' + assert set(a['stages']) == {'early','native','caller','frontier'} + for row in [*a['stages'].values(), a['source_history']['evidence']]: + assert sha256((root/'admission'/row['path']).read_bytes()).hexdigest() == row['sha256'] + return files + + +def inventory(r56): + odd = {int(k):v for k,v in r56['odd_jobs'].items()} + even = {int(k):v for k,v in r56['even_jobs'].items()} + assert len(odd) == 4 and len(even) == 26 and not set(odd) & set(even) + assert [k for k,v in even.items() if len(v[1]) == 8] == [2324,2337] + return odd, even + + +def price(root, files): + r56 = decode(files['inputs/r56/PRICE.json']) + inv = decode(files['inputs/7314/EARLY-RESULT.json'])['invoice'] + assert r56['comparator_admission']['head'] == HEAD and r56['caller_head'] == CALLER_HEAD + assert r56['complete_paid'] == inv['P'] and r56['complete_targets'] == inv['T'] + assert (sum(inv['P'].values()),sum(inv['T'].values()),inv['S'],inv['empty_root_credits']) == (110536,22461,1424,0) + net = Counter({int(k):v for k,v in inv['T'].items()}) + net.subtract({int(k):v for k,v in inv['P'].items()}) + directed = run_path(str(root/'inputs/7298/pricing.py'))['cost'] + crossing = Fraction(r56['crossing_upper']) + assert crossing == Fraction('0.0036462214364462343366888845568981') + old = directed(net,crossing) + assert old[1] < 0 + assert r56['type_b_ports'] == 8 and r56['copies'] == 17 + odd, even = inventory(r56) + rank_prices = {} + keys = [] + for o in combinations(sorted(odd),2): + for e in combinations(sorted(even),2): + m,n = sorted(len(even[i][1]) for i in e) + key = f'{m},{n}' + if key not in rank_prices: + delta = Counter() + for length in (m,n): + delta.update({9:8,8*length:8,8:-8,8*length+1:-8}) + assert sum(delta.values()) == sum(k*v for k,v in delta.items()) == 0 + changed = net.copy() + changed.update(delta) + credit = directed(delta,crossing) + margin = directed(changed,crossing) + changed[1] -= 1 + extra = directed(changed,crossing) + assert credit[0] > 0 and margin[0] > 0 > extra[1] + rank_prices[key] = {'net_delta':dict(delta),'credit':list(map(str,credit)), + 'margin':list(map(str,margin)), + 'extra_paid_rank_one_margin':list(map(str,extra))} + keys.append({'odd':list(o),'even':list(e),'price':key}) + upper = max(Fraction(row['credit'][1]) for row in rank_prices.values()) + assert upper == Fraction(rank_prices['8,8']['credit'][1]) + assert upper == Fraction('72803865248455278947107190998539661213280058633/625000000000000000000000000000000000000000000000') + assert len(keys) == 1950 + return {'head':HEAD,'caller_head':CALLER_HEAD,'input_sha256':PINS,'crossing_upper':str(crossing), + 'old_margin':list(map(str,old)),'complete_paid':inv['P'],'complete_targets':inv['T'], + 'copies':17,'odd_jobs':odd,'even_jobs':even,'prices':rank_prices,'keys':keys, + 'whole_optimistic_upper':str(upper),'scope':'exactly two simultaneous transfers', + 'limits':{'cases':1950,'primary_seconds':25,'independent_seconds':30, + 'nonunit_seconds':25,'formal_cases':3,'formal_seconds':45,'binding_seconds':90}} + + +def check_stock(caller, frozen): + b = caller['types']['B'] + assert (caller['stages'],b['offset'],b['roles'],len(b['ports'])) == (17,36,36,8) + odd,even = inventory(frozen) + got_odd,got_even = {},{} + for i,e in enumerate(caller['events']): + if e[:2] == ['B','IDLE_ODD']: + assert e[4:] == [-1] and len(e[3]) == 1 + got_odd[i] = [e[2]-36,e[3]] + if e[:2] == ['B','IDLE_ONE'] and len(e[3]) > 1: + got_even[i] = [e[2]-36,e[3]] + assert got_odd == odd and got_even == even + return {clock:v[0] for clock,v in (odd|even).items()} + + +def dot(a,b,p): + return sum(x*y for x,y in zip(a,b,strict=True)) % p + + +def linear(a,b,s,t,p): + return [(s*x+t*y)%p for x,y in zip(a,b,strict=True)] + + +def prefixes(caller, site, decoder, body): + p = decoder['MOD'] + n = 36 + assert p == 65521 and all(p%i for i in range(2,isqrt(p)+1)) + assert len(body) == 17 and all(v%p for v in body) + clocks, gates = decoder['compile_gates'](caller,p-1,body) + gate = dict(zip(clocks,gates,strict=True)) + rows = [[int(i==j) for i in range(n)] for j in range(n)] + cols = [row.copy() for row in rows] + out = {} + for clock in sorted(set(gate)|set(site)): + if clock in site: + role = site[clock] + u,v = tuple(cols[role]),tuple(rows[role]) + assert dot(v,u,p) == 1 + out[clock] = (u,v) + if clock not in gate: + continue + _,op,i,j,c = gate[clock] + if op == 'SWAP': + rows[i],rows[j] = rows[j],rows[i] + cols[i],cols[j] = cols[j],cols[i] + elif op == 'ADD': + rows[i] = linear(rows[i],rows[j],1,c,p) + cols[j] = linear(cols[j],cols[i],1,-c,p) + elif op == 'SCALE': + inv = pow(c,-1,p) + rows[i] = [c*x%p for x in rows[i]] + cols[i] = [inv*x%p for x in cols[i]] + else: + assert op == 'J' + a,b,c,d = c + inv = pow((a*d-b*c)%p,-1,p) + x,y = rows[i],rows[j] + rows[i],rows[j] = linear(x,y,a,b,p),linear(x,y,c,d,p) + x,y = cols[i],cols[j] + cols[i],cols[j] = linear(x,y,inv*d,-inv*c,p),linear(x,y,-inv*b,inv*a,p) + wanted = caller['types']['B']['diagonal'] + for j,diag in enumerate(wanted): + coefficient = pow(p-1,diag[0]%4,p) + for power,value in zip(diag[2:],body,strict=True): + coefficient = coefficient*pow(value,power,p)%p + assert rows[j] == [int(i==j)*coefficient for i in range(n)] + assert all(dot(row,col,p) == int(i==j) for i,row in enumerate(rows) for j,col in enumerate(cols)) + assert len(out) == 30 + return out + + +def defect(left,right,p): + u,v = left + x,y = right + t = 4*dot(v,x,p) + return tuple((-2*a*b-2*c*d+t*a*d)%p for a,c in zip(u,x,strict=True) + for b,d in zip(v,y,strict=True)) + + +def project(line,p): + divisor = pow(dot(line,line,p),-1,p) + return line,tuple(x*divisor%p for x in line) + + +def controls(p): + a,b,c,d = [project(v,p) for v in [(1,0),(0,1),(3,4),(-4,3)]] + assert a != b and c != d + assert defect(d,c,p) == defect(a,b,p) + assert defect(a,c,p) != defect(a,b,p) + return ['different_orthogonal_bases_cancel_jointly','one_replaced_reflection_fails'] + + +def support(root, files, frozen, stage, previous=None): + caller = decode(files['inputs/7113/CALLER.json']) + site = check_stock(caller,frozen) + decoder = run_path(str(root/'inputs/r52/screen.py')) + p = decoder['MOD'] + check = controls(p) + start = monotonic() + bodies = [(1,)*17] if stage == 'body-one' else list(decoder['BODIES']) + matrices = [prefixes(caller,site,decoder,body) for body in bodies] + + @cache + def pair(i,a,b): + table = matrices[i] + return defect(table[a],table[b],p) + + keys = frozen['keys'] if previous is None else previous['survivors'] + rows = [] + for key in keys: + if monotonic() >= start+22: + break + a,b,c,d = sorted(key['odd']+key['even']) + verdict = None + for i in range(len(bodies)): + first, second = pair(i,d,c),pair(i,a,b) + if first != second: + k = next(k for k,(x,y) in enumerate(zip(first,second,strict=True)) if x!=y) + verdict = {'body_index':i,'row':k//36,'column':k%36,'left':first[k],'right':second[k]} + break + rows.append({'key':key,'chronological':[a,b,c,d],'mismatch':verdict}) + return {'head':HEAD,'caller_head':CALLER_HEAD,'mode':stage,'prime':p,'controls':check, + 'body_values':bodies,'visited':len(rows),'results':rows,'site_count':len(site), + 'cached_ordered_pairs':pair.cache_info().currsize, + 'unvisited':([] if previous is None else previous['unvisited'])+keys[len(rows):], + 'survivors':[row['key'] for row in rows if row['mismatch'] is None]} + + +if __name__ == '__main__': + parser = ArgumentParser(description=__doc__) + parser.add_argument('root',type=Path) + parser.add_argument('stage',choices=['price','body-one','nonunit']) + parser.add_argument('--price-sha') + args = parser.parse_args() + files = authenticated(args.root) + frozen = price(args.root,files) + if args.stage == 'price': + result = frozen + else: + raw = (args.root/'PRICE.json').read_bytes() + assert sha256(raw).hexdigest() == args.price_sha + assert decode(raw) == decode(dumps(frozen)) + previous = None if args.stage == 'body-one' else decode((args.root/'BODY1.json').read_bytes()) + if previous is not None: + assert previous['price_sha256'] == args.price_sha and previous['mode'] == 'body-one' + result = support(args.root,files,frozen,args.stage,previous) + result['price_sha256'] = args.price_sha + print(dumps(result,sort_keys=True,indent=2)) diff --git a/research/p104-two-type-b-phase-transfers/inputs/7113/CALLER.json.gz b/research/p104-two-type-b-phase-transfers/inputs/7113/CALLER.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..290ef7c9c52553e421350ea76ac73eb98d1f187b GIT binary patch literal 11215 zcmZv=V{j!-{N+8-#L2{VCdtG$Cbn(cww)W>nb_8iZQHo9Z9c#MK3iM+V!OINb-MaZ z*XizWcO4=C%#Z(R;AodQws8le2|GRG|Ma(TiZWlb+n{?^8%stSh+oOTvHVb-wzxJRp-*Yi^g+l*tS3mY37I~z;yw-09wKPKxeI6IX)wmBBx>h8<#d%ty`>hFvU9}lNdxX3cf z*2y}^o_LN>6j2;dBvZJ_vdT8ey2w7rUhL4YGqEvo)U%dbCtALNC|AgLie`(xnw68B zlBAM4D6%LvC^{(KDZ(j6D4q+)W$9&4GmSEhvi36fvQRTovl27sk-e~81uklc+*go0 zoz*`dzF!uQS6cEG-Ch`XwtR5E=N|pPw>HiNI{n>0jRgXCT1s#zZb$Pf!-y`BzHNvu zmIYR;{p+;94O+kY>^_6H-k>`kk^2kZ1RKBpAHB^%U;X7A&Yy(lLP z?~LvK-(O9CB>x?11++{()eSw+>+mD)G<)}o3FwSJWpL|xUD#$ke6^sx0HPa$QbyBHh5U91P~I=b7!_xP-~>!|0|`PwKhubBfp6Hx2_bq|>H zzjXD%_2ccx9I4c9NO|lW%$XAZG^@jaaHpOQEck#zC4OrPKGA^qVHP;2E%?=s|=_KdbA1$Mt-_uI$J3 z!2n<0Qk&Lp-@V@N1uOLM^=Kg4S^Zt!-y7UrC&o6J*LA67tsiRrxjs%d=HLhoXyeh< z*^*L$>4)n0BMYG3dr%`hdI?T`8w9wwzUvbgJA_7kn^c#}LVl+PX~GieI<3Wk(jd&A zhB|D|m9+_CcD-Lh>n`scKCOor$k*wol#O`r%y;o>bjop(yMAxRuFd|%@Y+dNJIAE( zvIey$r|e{xm=ST{q&2Ei-bx1cavn(9>N9p6zGVY=t(hg6+gqftMhO~@l)BvYG6nH7 zC?j+JPAYdL1w@`5GBhOn9}67U0_u}M^ovOAzNn#Jjf~vfKF`q*Lz<4Am`@b9e`!S? zhYIWHDp%MsKRY{M^NXjUqTCwK@XKR zrL8z!<^;}N|4?T5DG)%&GW_nfr8{?jlk2ysPpA*QW3~zu(| zUMN+KYSn|=YFh7P{1c^hXh>&N-)2)?N8;@2JHWjxcF;8YSzH%wQ!Z0zEX_A*F=e(1 z7ra>0d>R4;tjG4WZ0;T?rdsyox6CltJN%%~!=Cr6UaO9N2=Qaminr?+-;{*UPVF^Y z^QfO*rw^?kM zJ!F6#R1{J!NWgfWZ4rfon>hGT?W*8&(K`f7ksd4?Tv5gaJ>5aq{5*i=8 z8lz@2k`DFIcb&V^k=4)V`!7H&9)2Z55S95U`JY@4%Nm4uql-B$uR?kjaam4D>$YPtK{U4cw1 zJM{tEwb0iqLC@C5+qFcf#2nkTy8EAAcYe0Usrrt0eth0NZbQV!EdBiTpFVl3<*Tc3 z0&9(V7uUGL@Yurl=)!n(P;TW@uzhVF*L_?)w41TUwsA+P-l4&bjb9OM!4 z4DetXyZ>e8Y*Lr~$yntgU?!vxd_WO2ZHWh4zdec!z1cvRKsgQV89x|THfW>3(fK!h z8o4hjLKTW#mJfP`AY7V|!(0^B`f?jGrEyPHX9D)aoa^_ypxF*BEm&zK0^{KXA$kcv*{$?=&+79krN^2{Y#RM;g50IXmoxRb6Daeb`-TS z)o3&c19O<(eIg+%!kWq z`SBMlSY0Otz{#>V#djo&VmY?A_&2he~~>(bs537;7Tv5Jc+QYr?>_(O#QQ z>s$jt1vcYcVr7F(NlN13u|!3MD?dYKJTr?G=p#rU zN6=rkpSO^F@*gT@loP2Hrf3~Z1-d3lU$x}Mn)~ivUVNESKgb29ONv0Vl{47$6m|xsuRwCU-T^)J-kOs% z5<~n!_&J-U84YbrCWMSOpKO#NU0m*2j!h{imst&EhBm;_gR2ZE)(aF10*VCy#nMOE zlsSesrt=XETAnjx)*EkhpaSr*ie2cZXa`vpp>3dG3S; zA2ZUPnuHldI*A>l)#L&xy^VHH!S)o}Vi^w_0pi8SC`H_z_^KDwMiW;D()XEod>lb2Cx~8$ZLm0u?Gce*!7q6mCiQM-0kcu^viu7;f&>e@%DNMp> zMk_s9C*cX1KFtkD408>_-YkM+@~W?W<#x5 ziG6hOPQV`_ySMNmyj9>NOa0&(3Ur}T27dQ5`rrFQWl%^xj^S_(!k?@8UKa{HZe{p9 zi!lTh!=IH|C=WYb_z~n*@^-_RVUMDKIBu`S{lY-Pm=}xw$_yBEuf>FzLj-=SQ^oK& zFRx@}Q?u&d{-5$aFH=3y@Gw=uugzmfyDLR&&YW|x-H`(`$0yP}dg!5M0+lo2`nW41 zfOBYdEkGse3IlI@E5%@HU6BOsDW!DOOaY=0+(rT4Y(4H->d@Sk6p5mV0y+-5=ugoE z!T&A8)zS2(Jep@!!;PIe+5Zn({3JoSK^T$m$!@Gs!s~LtTLnzq#L%Cu5&2st4*NLk zg+E&x^KaK|f4?Mqwq3P&FxZ=TnK4M}lLT)|31;ppTV!W*Llb_>mYJ z=V-`&afb6$*`uY?g?hKX6nY-7UZvXw@6hA$d8e-GqF-^+*EC(}*Jl6OFz@9|sS#?{ z)jXD3UT3rbyX?r>cjiW^ac}dwzlsn`N0WScs<@ex3h8ShL6mtI7O#;?BrOE`0}Gil z0^qC<69D&P3=U@Iqz)cnzL?(aodk^%O7QM6(N(d8zae+@CCafC`68ZL3ghOe2&}=d z;^QJB{%q!7Bk7k5Q6vu8V%tfj(F#j7gO*Is75T2D(P~MhAS_=+O!*2|ZpJ=W$P)OM7`JN&4deJBcEJq zB&b)V9xus`S+e=m0k&T4q)My_LK9O?MeDAKvFC$9&iGqyVoA(iV_Zm4JeB2ZL!!r= z*;m;VC$V%qBlRA~Y_dH@Agm697GiT8;)UqqiZ*B+Ve_QVymgvDYM#+Ru zS>#}F#9f1j$yio7O_LtwrbL<9u*RfB%I$v6|#nRrTS~(`l z#2334p6#Fzg3`DBX3FLuh!}`YHJ;Gr*P;KN5(d2QCAFq8(^s^aaov^adfh!K8DgMW zCc+UORTDiB5K-uVo3uWhT>c&q)9TjnaA`T`y`Jqq1G@6xu3^=fP@NG>49kujptd-i z0gX40$egA`@WlkK_Fl;2do;Li#gBYnvl#sEytN%Vx8rD^$+V|xwvr|~o+EZO=nT~a zfLiSt-sZNsSAF-@mWe8oN#<%`kmqL63b9pL^~A5)6^w?WpV7{hy!AXBRwnsj4_c*$ zsyRQ&Po}GDzz9I@@Q+|k0$d-o&Xw#%gcxnt;@B-Sd0FuJu29d4<745jX|z4QB_PAf|^HXaWHVs^t(%1|BxyD{LxAF zXNy1Bh(8tZ%4n9hgqa()5;8hueX)jBYpJ}8%LJ|O-Xnrg6LqXfaU@+$ouQ&Qwqg{g zFz{=uv*|z{E;KJWH?}|R104SMThXIe^3|F3XFo%}9|@|AzLKt>Q^!J(J;P*b$dMSj z-{(Zd>~Vd^Yl|5neLX|D)3$Z~r81oD3ZeBYszJQ?pNyDa5}LzWvlrBG=40UIo^%$z z_~U=T$H(BtJ?UgVtyZ^;4Xs2-#^HNQ2peXb4uuv_pN018VJ2zdC(os+p>@fuOu-Z< zq$Ad?1CNy_7lR+M-Bgp2?SbV3O^pR;t$}XGsS6oFS)~bA+N2b*Bi0`ti^H)acI_oP zD3PgLPL>C1(PdkB^FF8+GAzFbW5yQ_^Fx2REd>#D_8rNguo===li40E_Inbyrcv-` zEjBqRaj>2}J>cc4Emlu)mb}IvH7dyW*YxoqK8;deJ|~RCt!H5_<=9qLy{#Lb)w8}2 z&86_Q69V6e{W)!Xg5JCsvIuy$0e9rBBbi-HCqd{5`sXj7Cyy6G+%6ieBmFI&H81#d zK5^PSO>cA61h}7nc$_~Np^yMF#x5zcYdu3A3`=5G-)DGzYFRCx9wXYOe&eQ@{}fr5 zd}z&DAJaw5LP#;`SW9Fx}b=@tS_u@b99YX+^RqOC#`tQbIk&6w9F32?_n8=pq6_ z_g3m4OYzwp3au$C5F0JlL;*(4uvaxg+Cl+7KXnKiJP2mPgXWR!90qTtB6(ne4PMFn z9)s8C28gi{+r!~&*Hioy8sW8@NS;;|ky6^Ep5pYYJ+O>YkdGy$p-3XNSpr3i9Nsil zH};tLL3;wO=CN!y!o!Tz zRFQ!GyuZJlv5;F%sC4BRs#yx_?R&agPO)1qwSwsn6i~IPR_f_1nRb&ZNctjV1#^n! ze*MA=Djnmq|G}8Dv)?ZfGr4W~VBlIJX+-WNIMgZ|LJ_m!)!iO0$B+x`%p2$LR$onbO5>U7fvxg z*I}q^KJ6rfp#tpvc>>>;Jy3r5fr*YTxvP+x3QF_lAMN;TDsFuS)pWKc+7lul03R2=4#VkodVU=nPsCwz6DF^ zvn8{4a2xiPl>qskPI9Jaa0PP1<7S%^u-iGk%E&lUqzIsBqrzH9tgR5>XSrb|yPE|> zp<*TNF3WIN$&$vt-U3_+ludGE3mZp|iE`sO#ZK|LY4TW2`_<6BqKKEaPKJgovkAW!8>vn1r{U*x zP3+Mts)q&YZYJ`?YnHp{c*AN132d*im2ZfoR53qktp51J7F&I*e!V~DsOl1Os=1?} z?9Ib%$gsi@^(K|mZn%i}*zU;DY%LY7F8Y3CorvXNt+@)dO&CUCwCyRu!*Uta1pTL% zG}r=}l%no0>3Z-E^56jfEn5&{?`^y!KQ3mE%ARv_d|+`025REtPeme86N6@x&icaEQ;_tKqpv{nFHAT#>QzeD%NDwCQV%UFF6p^{)G@uY` zL@I=C9d7nd%{HH&K};Z$rHnUM&GxIN0)vcivan zE;L7g=j&az96M!d6;S~V#3(R*h>~tnA!H=Y*t9{y3YXe$XQ5==Y~lYn%a-YQh6YNS zFn$PYlOgj|Bl}W^@f5e$L%^Q%*qxiHy7xnZ($3_P7ZZz8DXrKv24#LaL}nlaptD3` zW{6N`yiDa}&YRt^*>gPral8&K>9{ipW9j#?+YQb@ugKFB5nFNJiY19alxIZtkuwPzRFKF!;b3!$j>9P>bz4}6)MVZ&N)6drL#^5ghK?2I~_dySSE`GqTkc)znme+ZcnNLyb4e@(?EMcI_J$Gx#P{Z~$t0%eU&OwfSj zNB`Y^(l#64$IJ=(|2?s{C#pjpVIj834BH=$Yz@xV@iZ!W$n4b1!i93n+7^*s>OMZg zfd3>ysCh>fH1ZRI3jc$gun;A3Y-)>Ih$4 z$PxV$=(sAZM<t7(QnBF8GTH!2t^}_}yd*JQ3R8tq z1BWS7cp^@ZMn>$3QH61*Z`&0yhPwS8Ko`}domPPm7|?ylpm zg7dG0(*VbdUcu{Lk~?D3GqC+@um$hZp$HLLls>Pmef9|hcDW48cW=vXC`;(DYDe{* z^(eO0i`ZF!WOh93+9)xqAYPy7UHz{(N!COYnWz!+kjU_~#q1(8jAq*=F!TxbT7b)3 z+0T_%M(Bu_=ekcN)edn^ zZm`iN!CyCW|F*a`4G#PUkxy=ExzPK-oMG5|`RCUDL3@n+LDCZ=ikDMKK>VP;JY&4t z+V9Bni1jR~-;A!`JjQCi>=7bRnEKT+bzf)uU1>jZ%`qr{pV@2s?IInG`7%k`TCzWD z>*tuifrV1YM}l9O=qRyA3uVH!RV*tM(lF>MB-R+g9_1(gF!J_SXreArGRUttItRrJ z)hqFoM|4N&xTKxvtY|-m5$^1~RuBXY1BdKFiaUyLxXTSz4QCKx{H=4HG=bMd{ew*I z)A^99W_-5dMbQ3R;PRb20Pn6uh8@J0yNAHW9*Kr?1&(2SFnzdT^nDI_? zPs|-6p5-29e{XAdCmT(u^1jdYqd*=E*jko!^EuNLSi(gF)V!(}^fB{y+h8sDUURhq z8L{*jRdaKK))QA!vS39d*Z55h#q5DdJ=sawj1}9Mr0Tbf0 zgu$UJgQF9A!33+KCs3rmO+IYv|I7Qw_{}ki~gZmzcHO5?BN6X|RJ4 z%Bb?4&LzXTp4x}eIF^&uK6Gd_ZVvMSr}5|?5=`_KYnS=>{cI9(Mfn5JVr0fv>3te| zKH~X)v16cg<{`p!iE>coX#r3%?$Ct(Auq+^ya z|ET0PApT);+LrWRY^{Zbig__2$I>9Q3wv9AM>rhZaOlL!gi<4LD;mx^h6;{g{3KAv zc1glPP{BuoUbO?_19`0cD^YJ2_Je>!9FZ^E59=B&vxaLz;im8eX>=|HHu(b$p-2;$ z-1OQfR6z~4Qc=<^`gOa>c6NP8>2gK$N2?cq)|IkyBJk#B9Sba53pM^kO^|CU)a~XM zOL~!{5x03v4M}-vTLd25Enf*6e&J^G{^rC<4T>R+Yk#!f(m$ky_WhWzb=^ow(toIz z>A|#9*bP}2VN>rTuN53j3XZ6T{2{7P$Hzpip`tR&je&tsDhdUNf@2OR<)jt)A4MAO zh!eh05EKaZG=lJe1NV?)C{wE-bKP0!{qMA?y2&MrtD{VS~9UIlF?=LhORH;2zZ- zRo9HeR)T`UQk)QQSjn}JH(bc_mKV-5~7V*I!A%mUC{ByF#aRqCzT$nKwwJq zPKV)gx{ypKSMd%(>(sBYwaq?V7r?O|QCP=62R!b%3wk4eR4eU0$OBIH;ejK{AP;LG z5x`=bwEfs|MSpycz)Zm<2gSUSSG|&T^T+QR+cf98J}kAJ7RfkJ3Dplou%fnABq$nY zWDfj)S|MrlkAi&#^D_8-tCBigibQKK3{{VjXEZJD<_s(3M3p{u;M-_h@)ajTm^*;d zUGIW#SX74S7Rvy6m%o7cq^?53CjfHUA8(qA3x=D z4K@dtD5u@xS+j4^s|oa-IFjtYUeEorkB}odO-aKZ#fls1g;jVH_Y&gR1yH!e+%{oh3fUm-i0_aT?Ih#MU>VVAnC&>QwzX>kzFThy!D;5OIoW`Q&KEv+ycME_+r zb)Rc{_u}y{hm9V@U#%~%>qbFEAruilu1tMp918z2M0JmuP*I+2M0MZUxTSn_Rvloi z9rgu@^_wGrA_}2x5>1kRXE{|^!{r=5(}!#$S-+zCKZfTd)dFr)uSaU(I-NZwwOrm6|OIF5dhhnLrt+1%9)UlsN^NBGbUnb)> zl7Dkglz&H6=7d~x4L>uN!unHOxI^}Lvcw+4jCiw-P7|9vpX_EsI86WGG=J)C0}ZBT z^>Q`BWjjMoXZ+8;WjiBGXE=i&PyYzjj%(e*5Tc3j7xbZWWRwKA27~n`zeukO+R&PK z$q1O4l%9lUE2|5Sn*{N@y7<}>&q-7DRv|d$LfR8N3V+@=>Ep(;+)z)4krFe?%XAM_srOv8Bs_J+3{0hLgUV5zw_Qot2A# z?L127bBJA&9{-NA2B$vGEjeUWyT4#AL;95pJ>z#5lF1AC*9e8!^DosP1iBFzT)nqK z1kvIoWaz4@LIfq%AUnLzkwSzy)gV7C`dwN2NKQi}tC3@D`Cp#0K&W(~(is|M^FO@= z`XbyhA;@|Qx>xB}1t0$!XM_{hNI_A#t>&3?`NpZ^^1gGYn5Ugih+qw*QtUr*2R>!B@5L_;-6rw_vceO)L(360tx){MRQJA<1g{uRpHx z1b_JKcKD8AN)=J2#gPQPt{lq2LvN$9C;$ez{!IpYyAyhl_tVVVB|5W|QAv@}dIaN9 z>Z>m*9%x_nd$NMEwNIaU`tc{Q;GB+#=#Jr>fQ9Af{jk6N`(X^E86)R(hHU4i~~h%ZJNQ}O7Lg&~+(NdbK2w;Qt&v@xUe z|37T@*w-$dGW=;tL&DP-W1tPqng%MTzB1BJBcF_EoESp*BJ%BH@Y*{xJ;Y<;3q6SB zcCU;I02%a{z!RQ!i<5$4KrFpiyM%QALIiKj=>LFfHUj+rjrj=D7^?ppdz=N8M|+?0 zME>trpQTxVT6(|FDF(ks{qG}&sVsr7OLcp{`%C?r?T^y$k0br>XQC{Q>z%F6*VDJl z>un#P-}A_F=c~YV&v|W3n!x4<=yF7!gJ}C>sw2za`~Iu6$9qB9`~GPwOI`qhLqNC3 z*ZsbOV@2TWVc^l7Bk$|U-2eG#|NZ+N^q%#V@TKnG{WTZ<(3lsB{ub{4cKi1J1-kzF zoO1oXN9N$Tto=U4>UmA$;PCJET=8@NyuBRZ=;`_TT6jmc|K52lZN1(>?A(sF_q|>D PMn*AXLoONv`| 1: + na,a = heappop(heap) + nb,b = heappop(heap) + selected.append(sorted((groups[a].pop(),groups[b].pop()))) + if na < -1: + heappush(heap,(na+1,a)) + if nb < -1: + heappush(heap,(nb+1,b)) + counts = Counter(j[2] for j in jobs) + upper = min(len(jobs)//2,len(jobs)-max(counts.values(),default=0)) + assert len(selected) == upper and len({x for pair in selected for x in pair}) == 2*upper + return selected,counts + + +def price(roots): + files = authenticate(roots) + base = "round30/complex/source/inputs/" + word,caller,early = (unpack(files[base+name]) for name in ("WORD.json.gz","CALLER.json","EARLY-RESULT.json")) + old = runpy.run_path(str(roots["7298"]/"verify.py")) + audit = old["complex_scan"](word,caller,early) + assert json.loads(json.dumps(audit)) == unpack(files["7298/RESULT.json"])["complex"] + binding = next(raw for key,raw in files.items() if key.startswith("7113/")) + assert b"rank = 8*len(selected)" in binding + assert (caller["stages"],caller["types"]["B"]["offset"],caller["types"]["B"]["roles"]) == (17,36,36) + ports = len(caller["types"]["B"]["ports"]) + assert ports == 8 + jobs = [(i,e[2]-36,e[3][0]) for i,e in enumerate(caller["events"]) + if e[:2] == ["B","IDLE_ONE"] and len(e[3]) == 1] + assert len(jobs) == 34 and all(0 <= r < N and 1 <= stage <= 17 for _,r,stage in jobs) + cases = [(s[0],t[0]) for s,t in combinations(jobs,2) if s[2] != t[2]] + assert len(cases) == 544 + matching,counts = maximum_matching(jobs) + assert set(map(tuple,matching)) <= set(cases) + kappa = Q(audit["probe"]) + paid = Counter({int(k):v for k,v in early["invoice"]["P"].items()}) + targets = Counter({int(k):v for k,v in early["invoice"]["T"].items()}) + assert (sum(paid.values()),sum(targets.values()),audit["copies"]) == (110536,22461,17) + net = targets.copy() + net.subtract(paid) + delta = {8:2*ports,16:-ports} + changed = net.copy() + changed.update(delta) + cost = old["PRICING"]["cost"] + old_margin,new_margin,credit = cost(net,kappa),cost(changed,kappa),cost(delta,kappa) + assert old_margin[1] < 0 < new_margin[0] and credit[0] > 0 + h8 = old["PRICING"]["power_bounds"](8,kappa) + h16 = old["PRICING"]["power_bounds"](16,kappa) + report = { + "head":HEAD, "caller_head":CALLER_HEAD, "inputs":PINS, "crossing_upper":str(kappa), + "native_copies":audit["copies"], "type_b_ports":ports, "old_complete_paid":paid, + "old_complete_targets":targets, "old_complete_margin":list(map(str,old_margin)), + "one_pair_paid_old_minus_new":delta, "one_pair_complete_margin":list(map(str,new_margin)), + "one_pair_moment_credit":list(map(str,credit)), + "break_even_volume_factor":list(map(str,(2*h8[0]/h16[1],2*h8[1]/h16[0]))), + "whole_compatible_optimistic_upper":str(len(matching)*credit[1]), + "maximum_disjoint_pairs":len(matching), "illustrative_matching":matching, + "stage_counts":counts,"jobs":jobs,"pair_keys":cases, + "new_work_assumed_free_in_price":True, + "predeclared_followup":{"nonunit_body_vectors":BODIES,"nonunit_hard_seconds":25, + "structural_hard_seconds":45,"structural_max_cases":3}, + } + return report,caller + + +def field_scalar(raw): + q = Q(raw) + if q.denominator % MOD == 0: + raise ValueError("Nonunit modular denominator") + return q.numerator*pow(q.denominator,-1,MOD)%MOD + + +def compile_gates(caller,q,body): + gates = [] + for i,event in enumerate(caller["events"]): + kind,op,*args = event + if kind == "J": + s,t,a,b = args[1] + a,b = field_scalar(a),field_scalar(b) + m = body[op-1] + h = (m,m*a*q%MOD,m*b*q%MOD,m*(1+a*b)%MOD) + assert (h[0]*h[3]-h[1]*h[2])%MOD + gates.append((i,"J",s-36,t-36,h)) + elif kind == "B": + d = args[0]-36 + assert 0 <= d < N + if op == "ADD": + gates.append((i,op,d,args[1]-36,field_scalar(args[2]))) + elif op == "QUERY": + gates.append((i,"ADD",d,args[1]-36,pow(q,args[2]%4,MOD))) + elif op == "SWAP": + gates.append((i,op,d,args[1]-36,0)) + elif op == "SCALE": + value = field_scalar(args[1]) + assert value + gates.append((i,op,d,d,value)) + elif op in ("IDLE_ONE","IDLE_ODD"): + value = pow(q,args[2]%4,MOD) if op == "IDLE_ODD" else 1 + for stage in args[1]: + value = value*body[stage-1]%MOD + assert value + if value != 1: + gates.append((i,"SCALE",d,d,value)) + elif op != "LAMBDA": + raise ValueError(op) + return [g[0] for g in gates],gates + + +def transport(gates,initial,row,mod=None,dimension=N): + vec = [0]*dimension + vec[initial] = 1 + mixed = False + for _,op,d,s,c in reversed(gates) if row else gates: + if op == "ADD": + to,frm = (s,d) if row else (d,s) + vec[to] += c*vec[frm] + if mod: + vec[to] %= mod + elif op == "SCALE": + vec[d] *= c + if mod: + vec[d] %= mod + elif op == "SWAP": + vec[d],vec[s] = vec[s],vec[d] + elif op == "J": + a,b,x,y = c + if row: + b,x = x,b + u,v = vec[d],vec[s] + vec[d],vec[s] = (a*u+b*v)%mod,(x*u+y*v)%mod + else: + raise ValueError(op) + if mod is None and sum(bool(x) for x in vec) > 1: + mixed = True + assert any(vec) + return vec,mixed + + +def outside(vec,axis): + return next(([i,v] for i,v in enumerate(vec) if i != axis and v),None) + + +def controls(): + gates = [(0,"ADD",1,0,1),(1,"SCALE",0,0,2),(2,"ADD",1,0,-1)] + assert outside(transport(gates,0,False,MOD,2)[0],0) == [1,MOD-1] + gates[1] = (1,"SCALE",0,0,1) + assert outside(transport(gates,0,False,MOD,2)[0],0) is None + assert outside(transport(gates,0,True,MOD,2)[0],0) is None + assert transport(gates,0,False,None,2)[1] + read = [(0,"ADD",0,1,1)] + assert outside(transport(read,0,True,MOD,2)[0],0) == [1,1] + assert outside(transport(read,0,False,MOD,2)[0],0) is None + match,_ = maximum_matching([(i,0,s) for i,s in enumerate([1,1,1,1,2,3])]) + assert len(match) == 2 + caller = {"events":[["B","IDLE_ONE",36,[1]],["B","ADD",37,36,"1"], + ["B","ADD",37,36,"-1"],["B","IDLE_ONE",36,[2]]]} + assert structural(caller,0,3,0,0) == ("formal_projector_transport",True,None) + caller["events"][2] = ["B","ADD",37,36,"1"] + assert structural(caller,0,3,0,0) == ("unresolved_endpoint",True,3) + return ["body_one_false_positive","genuine_nondiagonal_transient","outside_read_only", + "distinct_mask_matching_does_not_double_spend"] + + +def modular_stage(caller,jobs,cases,bodies,deadline): + compiled = [(v,q,*compile_gates(caller,q,body)) + for v,body in enumerate(bodies) for q in (1,MOD-1)] + records = [] + for left,right in cases: + if monotonic() >= deadline: + break + source,target = jobs[left],jobs[right] + witness = None + for v,q,clocks,gates in compiled: + interval = gates[bisect_right(clocks,left):bisect_left(clocks,right)] + write,_ = transport(interval,source,False,MOD) + read,_ = transport(interval,target,True,MOD) + bad_col,bad_row = outside(write,target),outside(read,source) + if bad_col or bad_row: + witness = {"vector_index":v,"q":1 if q == 1 else -1, + "outside_write":bad_col,"outside_read":bad_row} + break + records.append({"key":[left,right],"witness":witness}) + return records + + +def structural(caller,left,right,source,target): + r = source + block = [] + mixed = False + + def flush(axis): + vec,m1 = transport(block,axis,False) + nz = [i for i,v in enumerate(vec) if v] + if len(nz) != 1: + return None,True + end = nz[0] + dual,m2 = transport(block,end,True) + return (None if outside(dual,axis) else end),m1 or m2 + + for clock,event in enumerate(caller["events"][left+1:right],left+1): + kind,op,*args = event + if kind == "B" and op in ("ADD","SCALE","SWAP"): + d = args[0]-36 + if op == "ADD": + block.append((clock,op,d,args[1]-36,Q(args[2]))) + elif op == "SCALE": + block.append((clock,op,d,d,Q(args[1]))) + else: + block.append((clock,op,d,args[1]-36,0)) + continue + if kind not in ("B","J"): + continue + r,inner = flush(r) + mixed |= inner + block.clear() + if r is None: + return "unresolved_constant_block",mixed,clock + if kind == "J" and r in {args[1][0]-36,args[1][1]-36}: + return "unresolved_active_j",True,clock + if kind == "B" and op == "QUERY" and r in {args[0]-36,args[1]-36}: + return "unresolved_query",True,clock + r,inner = flush(r) + mixed |= inner + if r != target: + return "unresolved_endpoint",mixed,right + return ("formal_projector_transport" if mixed else "diagonal_path_overlap_pending"),mixed,None + + +def previous(out,name,price_sha): + value = json.loads((out/name).read_text()) + assert value["price_sha256"] == price_sha + return value + + +def main(args,start): + roots = {"round30":args.round30,"7298":args.predecessor,"7113":args.caller_root} + pre,caller = price(roots) + out = args.out + if args.stage in ("price","body1"): + price_sha = save(out,"PRICE.json",pre) + else: + frozen = (out/"PRICE.json").read_bytes() + assert unpack(frozen) == json.loads(json.dumps(pre)) + price_sha = sha256(frozen).hexdigest() + if args.stage == "price": + return + jobs = {j[0]:j[1] for j in pre["jobs"]} + cases = pre["pair_keys"] + checks = controls() + assert all(MOD%d for d in range(2,isqrt(MOD)+1)) + prior_unvisited = [] + if args.stage != "body1": + first = previous(out,"BODY1.json",price_sha) + cases = first["survivors"] + prior_unvisited = first["unvisited"] + if args.stage == "structural": + second = previous(out,"NONUNIT.json",price_sha) + cases = second["survivors"] + prior_unvisited = second["unvisited"] + deadline = start+CAP[args.stage] + if args.stage in ("body1","nonunit"): + bodies = ((1,)*17,) if args.stage == "body1" else BODIES + rows = modular_stage(caller,jobs,cases,bodies,deadline) + survivors = [r["key"] for r in rows if r["witness"] is None] + save(out,("BODY1.json" if args.stage == "body1" else "NONUNIT.json"),{ + "stage":args.stage,"price_sha256":price_sha,"prime":MOD,"body_vectors":bodies, + "scope":len(cases),"visited":len(rows),"exclusions":len(rows)-len(survivors), + "survivors":survivors,"unvisited":[*prior_unvisited,*cases[len(rows):]], + "records":rows,"controls":checks, + }) + return + rows = [] + for a,b in cases[:3]: + if monotonic() >= deadline: + break + status,mixed,at = structural(caller,a,b,jobs[a],jobs[b]) + rows.append({"key":[a,b],"status":status,"nondiagonal_transient":mixed,"stop_clock":at}) + save(out,"STRUCTURAL.json",{ + "price_sha256":price_sha,"scope":len(cases),"visited":len(rows),"hard_seconds":45, + "unvisited":[*prior_unvisited,*cases[len(rows):]], + "support_survivors":[r["key"] for r in rows if r["status"] == "formal_projector_transport"], + "unresolved":[r["key"] for r in rows if r["status"] != "formal_projector_transport"], + "records":rows,"controls":checks, + }) + + +if __name__ == "__main__": + start = monotonic() + if not __debug__: + raise RuntimeError("Assertions required") + parser = ArgumentParser(description=__doc__) + for flag in ("round30","predecessor","caller-root","out"): + parser.add_argument("--"+flag,type=lambda x:Path(x).resolve(),required=True) + parser.add_argument("--stage",choices=("price","body1","nonunit","structural"),default="body1") + args = parser.parse_args() + args.out.mkdir(parents=True,exist_ok=True) + main(args,start) diff --git a/research/p104-two-type-b-phase-transfers/inputs/r56/PRICE.json b/research/p104-two-type-b-phase-transfers/inputs/r56/PRICE.json new file mode 100644 index 0000000000..f19a11a096 --- /dev/null +++ b/research/p104-two-type-b-phase-transfers/inputs/r56/PRICE.json @@ -0,0 +1,1159 @@ +{ + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "comparator": "7314", + "comparator_admission": { + "head": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "hosted": { + "head": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "run": "https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43097104414", + "status": "queued" + }, + "sha256": "41b8a189dffeb768e5843446cdc469f9cc2f0aa038d0a593cf2be43aa009a9a3", + "source_history": { + "evidence": { + "path": "ANCHORED.json", + "sha256": "6378aff76d6d38b3863d039b2d1814db48c3105ffe933e96d9c449e799f624aa" + }, + "stock_wrapper": "refused_shallow", + "validation": "exact_anchored_pins" + }, + "stages": { + "caller": { + "exit": 0, + "path": "STAGE-caller.json", + "sha256": "a653be3423a20a9aa0b6c532fabf7bf96ea7e5feab6bd3924d171d2b9c5c5f76" + }, + "early": { + "exit": 0, + "path": "STAGE-early.json", + "sha256": "cee13f7126ecdd375ad62b4a6773f3ac4182df52bc484dc2944a92ee31cd15f7" + }, + "frontier": { + "exit": 0, + "path": "STAGE-frontier.json", + "sha256": "75b8ceb5547f9828b03d60b7646fc2fdb47a0d02b5715d8f7fb35d7de946694f" + }, + "native": { + "exit": 0, + "path": "STAGE-native.json", + "sha256": "36ec25be5eb332a45f36d935fc1d0397e02e0b243ea38cc77d340592a33c478b" + } + } + }, + "complete_paid": { + "1": 68401, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5882, + "6": 221, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "complete_targets": { + "1": 306, + "2": 357, + "3": 799, + "4": 3825, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "copies": 17, + "crossing_upper": "36462214364462343366888845568981/10000000000000000000000000000000000", + "even_jobs": { + "1855": [ + 0, + [ + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ] + ], + "1869": [ + 2, + [ + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ] + ], + "1887": [ + 0, + [ + 3, + 4, + 5, + 6, + 7, + 8 + ] + ], + "1940": [ + 0, + [ + 3, + 4, + 5, + 6, + 7, + 8 + ] + ], + "1997": [ + 0, + [ + 4, + 5, + 6, + 7, + 8 + ] + ], + "2027": [ + 2, + [ + 4, + 5, + 6, + 7, + 8 + ] + ], + "2061": [ + 0, + [ + 5, + 6, + 7, + 8 + ] + ], + "2099": [ + 2, + [ + 5, + 6, + 7, + 8 + ] + ], + "2141": [ + 0, + [ + 6, + 7, + 8 + ] + ], + "2187": [ + 2, + [ + 6, + 7, + 8 + ] + ], + "2237": [ + 0, + [ + 7, + 8 + ] + ], + "2291": [ + 2, + [ + 7, + 8 + ] + ], + "2324": [ + 0, + [ + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9 + ] + ], + "2337": [ + 1, + [ + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9 + ] + ], + "2355": [ + 0, + [ + 15, + 14, + 13, + 12, + 11, + 10, + 9 + ] + ], + "2377": [ + 16, + [ + 15, + 14, + 13, + 12, + 11, + 10, + 9 + ] + ], + "2403": [ + 0, + [ + 14, + 13, + 12, + 11, + 10, + 9 + ] + ], + "2433": [ + 16, + [ + 14, + 13, + 12, + 11, + 10, + 9 + ] + ], + "2467": [ + 0, + [ + 13, + 12, + 11, + 10, + 9 + ] + ], + "2505": [ + 16, + [ + 13, + 12, + 11, + 10, + 9 + ] + ], + "2547": [ + 0, + [ + 12, + 11, + 10, + 9 + ] + ], + "2593": [ + 16, + [ + 12, + 11, + 10, + 9 + ] + ], + "2643": [ + 0, + [ + 11, + 10, + 9 + ] + ], + "2697": [ + 16, + [ + 11, + 10, + 9 + ] + ], + "2750": [ + 0, + [ + 10, + 9 + ] + ], + "2804": [ + 0, + [ + 10, + 9 + ] + ] + }, + "extra_costs_granted_free_only_for_upper": true, + "followup": { + "body_one_hard_seconds": 25, + "nonunit_body_vectors": [ + [ + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18 + ], + [ + 19, + 23, + 29, + 31, + 37, + 41, + 43, + 47, + 53, + 59, + 61, + 67, + 71, + 73, + 79, + 83, + 89 + ] + ], + "nonunit_hard_seconds": 25, + "one_candidate_uniform_binding_seconds": 90, + "structural_hard_seconds": 45, + "structural_max_cases": 3 + }, + "odd_jobs": { + "1339": [ + 32, + [ + 8 + ] + ], + "1340": [ + 33, + [ + 8 + ] + ], + "2970": [ + 34, + [ + 9 + ] + ], + "2971": [ + 35, + [ + 9 + ] + ] + }, + "old_complete_margin_interval": [ + "-357270001119021587349/10000000000000000000000000000000000000000000000000", + "-357270001119021530951/10000000000000000000000000000000000000000000000000" + ], + "paid_multistage_odd_binding": "unproved", + "pair_keys": [ + [ + 1339, + 1855, + 7 + ], + [ + 1339, + 1869, + 7 + ], + [ + 1339, + 1887, + 6 + ], + [ + 1339, + 1940, + 6 + ], + [ + 1339, + 1997, + 5 + ], + [ + 1339, + 2027, + 5 + ], + [ + 1339, + 2061, + 4 + ], + [ + 1339, + 2099, + 4 + ], + [ + 1339, + 2141, + 3 + ], + [ + 1339, + 2187, + 3 + ], + [ + 1339, + 2237, + 2 + ], + [ + 1339, + 2291, + 2 + ], + [ + 1339, + 2324, + 8 + ], + [ + 1339, + 2337, + 8 + ], + [ + 1339, + 2355, + 7 + ], + [ + 1339, + 2377, + 7 + ], + [ + 1339, + 2403, + 6 + ], + [ + 1339, + 2433, + 6 + ], + [ + 1339, + 2467, + 5 + ], + [ + 1339, + 2505, + 5 + ], + [ + 1339, + 2547, + 4 + ], + [ + 1339, + 2593, + 4 + ], + [ + 1339, + 2643, + 3 + ], + [ + 1339, + 2697, + 3 + ], + [ + 1339, + 2750, + 2 + ], + [ + 1339, + 2804, + 2 + ], + [ + 1340, + 1855, + 7 + ], + [ + 1340, + 1869, + 7 + ], + [ + 1340, + 1887, + 6 + ], + [ + 1340, + 1940, + 6 + ], + [ + 1340, + 1997, + 5 + ], + [ + 1340, + 2027, + 5 + ], + [ + 1340, + 2061, + 4 + ], + [ + 1340, + 2099, + 4 + ], + [ + 1340, + 2141, + 3 + ], + [ + 1340, + 2187, + 3 + ], + [ + 1340, + 2237, + 2 + ], + [ + 1340, + 2291, + 2 + ], + [ + 1340, + 2324, + 8 + ], + [ + 1340, + 2337, + 8 + ], + [ + 1340, + 2355, + 7 + ], + [ + 1340, + 2377, + 7 + ], + [ + 1340, + 2403, + 6 + ], + [ + 1340, + 2433, + 6 + ], + [ + 1340, + 2467, + 5 + ], + [ + 1340, + 2505, + 5 + ], + [ + 1340, + 2547, + 4 + ], + [ + 1340, + 2593, + 4 + ], + [ + 1340, + 2643, + 3 + ], + [ + 1340, + 2697, + 3 + ], + [ + 1340, + 2750, + 2 + ], + [ + 1340, + 2804, + 2 + ], + [ + 2970, + 1855, + 7 + ], + [ + 2970, + 1869, + 7 + ], + [ + 2970, + 1887, + 6 + ], + [ + 2970, + 1940, + 6 + ], + [ + 2970, + 1997, + 5 + ], + [ + 2970, + 2027, + 5 + ], + [ + 2970, + 2061, + 4 + ], + [ + 2970, + 2099, + 4 + ], + [ + 2970, + 2141, + 3 + ], + [ + 2970, + 2187, + 3 + ], + [ + 2970, + 2237, + 2 + ], + [ + 2970, + 2291, + 2 + ], + [ + 2970, + 2324, + 8 + ], + [ + 2970, + 2337, + 8 + ], + [ + 2970, + 2355, + 7 + ], + [ + 2970, + 2377, + 7 + ], + [ + 2970, + 2403, + 6 + ], + [ + 2970, + 2433, + 6 + ], + [ + 2970, + 2467, + 5 + ], + [ + 2970, + 2505, + 5 + ], + [ + 2970, + 2547, + 4 + ], + [ + 2970, + 2593, + 4 + ], + [ + 2970, + 2643, + 3 + ], + [ + 2970, + 2697, + 3 + ], + [ + 2970, + 2750, + 2 + ], + [ + 2970, + 2804, + 2 + ], + [ + 2971, + 1855, + 7 + ], + [ + 2971, + 1869, + 7 + ], + [ + 2971, + 1887, + 6 + ], + [ + 2971, + 1940, + 6 + ], + [ + 2971, + 1997, + 5 + ], + [ + 2971, + 2027, + 5 + ], + [ + 2971, + 2061, + 4 + ], + [ + 2971, + 2099, + 4 + ], + [ + 2971, + 2141, + 3 + ], + [ + 2971, + 2187, + 3 + ], + [ + 2971, + 2237, + 2 + ], + [ + 2971, + 2291, + 2 + ], + [ + 2971, + 2324, + 8 + ], + [ + 2971, + 2337, + 8 + ], + [ + 2971, + 2355, + 7 + ], + [ + 2971, + 2377, + 7 + ], + [ + 2971, + 2403, + 6 + ], + [ + 2971, + 2433, + 6 + ], + [ + 2971, + 2467, + 5 + ], + [ + 2971, + 2505, + 5 + ], + [ + 2971, + 2547, + 4 + ], + [ + 2971, + 2593, + 4 + ], + [ + 2971, + 2643, + 3 + ], + [ + 2971, + 2697, + 3 + ], + [ + 2971, + 2750, + 2 + ], + [ + 2971, + 2804, + 2 + ] + ], + "price_by_mask_length": { + "2": { + "complete_margin_interval": [ + "191169293130670396906442713584462319201385900283/10000000000000000000000000000000000000000000000000", + "191169293130670396906442713584462319201385956681/10000000000000000000000000000000000000000000000000" + ], + "new_ranks": [ + 8, + 17 + ], + "old_ranks": [ + 9, + 16 + ], + "paid_old_minus_new": { + "8": -8, + "9": 8, + "16": 8, + "17": -8 + }, + "promoted_volume_break_even_before_other_costs": [ + "42069186807975017907109010321330640696813535870313/42063212767564684457205683986519961561803523136325", + "168276747231900071628436041285322562787254143481255/168252851070258737828822735946079846247214092545299" + ], + "saving_interval": [ + "1493510102583362475831583702669783752503183497/78125000000000000000000000000000000000000000000", + "5974040410333449903326334810679135010012733989/312500000000000000000000000000000000000000000000" + ] + }, + "3": { + "complete_margin_interval": [ + "304834526570162319802117508624556783427386582171/10000000000000000000000000000000000000000000000000", + "304834526570162319802117508624556783427386638569/10000000000000000000000000000000000000000000000000" + ], + "new_ranks": [ + 8, + 25 + ], + "old_ranks": [ + 9, + 24 + ], + "paid_old_minus_new": { + "8": -8, + "9": 8, + "24": 8, + "25": -8 + }, + "promoted_volume_break_even_before_other_costs": [ + "247121072505851519762213535230811855616901830581283/247082968190030249472238270542189127268833529560095", + "123560536252925759881106767615405927808450915290643/123541484095015124736119135271094563634416764780047" + ], + "saving_interval": [ + "9526078955317572493816172155682087017075255297/312500000000000000000000000000000000000000000000", + "4763039477658786246908086077841043508537627649/156250000000000000000000000000000000000000000000" + ] + }, + "4": { + "complete_margin_interval": [ + "385972732715420141257903319097780691904627585083/10000000000000000000000000000000000000000000000000", + "385972732715420141257903319097780691904627641473/10000000000000000000000000000000000000000000000000" + ], + "new_ranks": [ + 8, + 33 + ], + "old_ranks": [ + 9, + 32 + ], + "paid_old_minus_new": { + "8": -8, + "9": 8, + "32": 8, + "33": -8 + }, + "promoted_volume_break_even_before_other_costs": [ + "325867768287915683355990825659200482656180940450684/325819521696326255838333587744268601319552984304133", + "325867768287915683355990825659200482656180940450687/325819521696326255838333587744268601319552984304131" + ], + "saving_interval": [ + "48246591589427517657237914931881336627956146551/1250000000000000000000000000000000000000000000000", + "12061647897356879414309478732970334156989036639/312500000000000000000000000000000000000000000000" + ] + }, + "5": { + "complete_margin_interval": [ + "449102241918047104064758566753739463187384886539/10000000000000000000000000000000000000000000000000", + "449102241918047104064758566753739463187384942921/10000000000000000000000000000000000000000000000000" + ], + "new_ranks": [ + 8, + 41 + ], + "old_ranks": [ + 9, + 40 + ], + "paid_old_minus_new": { + "8": -8, + "9": 8, + "40": 8, + "41": -8 + }, + "promoted_volume_break_even_before_other_costs": [ + "404541947005988370073124095848629720000699023866745/404485809225748614185116001027740843817660723057513", + "404541947005988370073124095848629720000699023866749/404485809225748614185116001027740843817660723057511" + ], + "saving_interval": [ + "3508611264984743000505926305554761439893800577/78125000000000000000000000000000000000000000000", + "28068890119877944004047410444438091519150404619/625000000000000000000000000000000000000000000000" + ] + }, + "6": { + "complete_margin_interval": [ + "500775415264468804181834483297103919284318429483/10000000000000000000000000000000000000000000000000", + "500775415264468804181834483297103919284318485849/10000000000000000000000000000000000000000000000000" + ], + "new_ranks": [ + 8, + 49 + ], + "old_ranks": [ + 9, + 48 + ], + "paid_old_minus_new": { + "8": -8, + "9": 8, + "48": 8, + "49": -8 + }, + "promoted_volume_break_even_before_other_costs": [ + "80526397461757731404200814895241375946346870258272/80515964640606388304113693343498576489671800674589", + "483158384770546388425204889371448255678081221549637/483095787843638329824682160060991458938030804047531" + ], + "saving_interval": [ + "31298463454029300261364655228398370025208751049/625000000000000000000000000000000000000000000000", + "31298463454029300261364655228398370025208751053/625000000000000000000000000000000000000000000000" + ] + }, + "7": { + "complete_margin_interval": [ + "108902818158350885014893265416077064635187346103/2000000000000000000000000000000000000000000000000", + "544514090791754425074466327080385323175936786889/10000000000000000000000000000000000000000000000000" + ], + "new_ranks": [ + 8, + 57 + ], + "old_ranks": [ + 9, + 56 + ], + "paid_old_minus_new": { + "8": -8, + "9": 8, + "56": 8, + "57": -8 + }, + "promoted_volume_break_even_before_other_costs": [ + "62414093067325626954787914255708050951204203441747/62406530371620185921106324445604750182811217909555", + "561726837605930642593091228301372458560837830975728/561658773344581673289956920010442751645300961185993" + ], + "saving_interval": [ + "2127008167155290722947134091553341110527180929/39062500000000000000000000000000000000000000000", + "13612852269793860626861658185941383107373957947/250000000000000000000000000000000000000000000000" + ] + }, + "8": { + "complete_margin_interval": [ + "582430921987642231576857527631047288587218881699/10000000000000000000000000000000000000000000000000", + "116486184397528446315371505526209457717443787613/2000000000000000000000000000000000000000000000000" + ], + "new_ranks": [ + 8, + 65 + ], + "old_ranks": [ + 9, + 64 + ], + "paid_old_minus_new": { + "8": -8, + "9": 8, + "64": 8, + "65": -8 + }, + "promoted_volume_break_even_before_other_costs": [ + "640254235137638904550954215195766130787808570459277/640181431272390449272007108004767591126595290400652", + "640254235137638904550954215195766130787808570459282/640181431272390449272007108004767591126595290400649" + ], + "saving_interval": [ + "582430921987642231576857527988317289706240469/10000000000000000000000000000000000000000000000", + "72803865248455278947107190998539661213280058633/1250000000000000000000000000000000000000000000000" + ] + } + }, + "source_pins": { + "7113/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "7113/check_odd_physical_binding.py": "5c80c3b0415a7f91d216395248dd6f13297eed637732098e1ca8fb0548951b98", + "7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "7314/EARLY-RESULT.json": "b5043855411432b24336ecc443cba9ebfae6392e2045ddd01c87cfe2c51f5f08", + "7314/PRICE-ONLY.json": "b757665a3a50324b2ae6649cc89f5b8d9a752c7af996f1ee894a0de47ade94e1", + "7314/SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "7314/VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "7314/WORD.json.gz": "c404b9b61220e6cf740d85276df2828bbb4a9d68a4d44b5e283f8d96f78c0fd9", + "r44/RESULT.json": "8d17c43c46d0a3a98f2c3c5849f13ac49a86244ffb87ef1b62e7bf4688cd525b", + "r52/screen.py": "cdf54b266ac31fd0efe544badbb9840598d4c63c4d3cd363f60ae9a74cc4b256", + "r53/PRICE.json": "86f779c3eeb43563793e6ccb2227257ef732b2ca12fbbde2f9099988f903a484" + }, + "type_b_ports": 8, + "upper_broad_job_choices": [ + 2324, + 2337, + 1855, + 1869 + ], + "whole_compatible_optimistic_upper": "8804257912339036380088467620515411046884365523/39062500000000000000000000000000000000000000000" +} diff --git a/research/p104-two-type-b-phase-transfers/receipts/INDEPENDENT-SUMMARY.json b/research/p104-two-type-b-phase-transfers/receipts/INDEPENDENT-SUMMARY.json new file mode 100644 index 0000000000..bec4938e81 --- /dev/null +++ b/research/p104-two-type-b-phase-transfers/receipts/INDEPENDENT-SUMMARY.json @@ -0,0 +1,10 @@ +{ + "cases": 1950, + "common_denominator": 40, + "old_endpoint_columns": 36, + "receipt_sha256": "b83b1001825ea4490c0dafe78bd86755030e73bde2b0d30ddfdb060f75f9b23b", + "status": "EXHAUSTED", + "survivors": [], + "tested": 1950, + "unvisited": [] +} diff --git a/research/p104-two-type-b-phase-transfers/receipts/SHA256.json b/research/p104-two-type-b-phase-transfers/receipts/SHA256.json new file mode 100644 index 0000000000..86e9fd4a6d --- /dev/null +++ b/research/p104-two-type-b-phase-transfers/receipts/SHA256.json @@ -0,0 +1,6 @@ +{ + "BODY1.json": "7407f6ccd01dd0f153554c250d6f953356d5692ecf39237f2418b3149df13131", + "COMPARE.json": "64c8b5c806abe2cef3c046a7a8f871eca377c80beeb2f48c9c01eb925b71ed3e", + "EXACT.json": "b83b1001825ea4490c0dafe78bd86755030e73bde2b0d30ddfdb060f75f9b23b", + "PRICE.json": "b73057381860987c6de1666205e91a0e3d116a8299d8aa425682f5960609c21f" +} diff --git a/research/p104-two-type-b-phase-transfers/replay.py b/research/p104-two-type-b-phase-transfers/replay.py new file mode 100644 index 0000000000..b287299833 --- /dev/null +++ b/research/p104-two-type-b-phase-transfers/replay.py @@ -0,0 +1,127 @@ +"""Authenticate and reproduce the exact two-transfer Type B exclusion.""" +from argparse import ArgumentParser +from fractions import Fraction +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 +UPPER = Fraction('72803865248455278947107190998539661213280058633/' + '625000000000000000000000000000000000000000000000') + + +def unique(pairs): + value = dict(pairs) + if len(value) != len(pairs): + raise ValueError('duplicate JSON key') + return value + + +def decode(raw): + return json.loads(raw, object_pairs_hook=unique) + + +def authenticate(scratch): + pins = decode((HERE / 'LOCAL-PINS.json').read_bytes()) + for name, expected in pins.items(): + rel = PurePosixPath(name) + if rel.is_absolute() or '..' in rel.parts or rel.as_posix() != name: + raise ValueError('invalid pinned path: ' + name) + if sha256((HERE / name).read_bytes()).hexdigest() != expected: + raise ValueError('changed pinned dependency: ' + name) + for folder in ('inputs', 'admission'): + shutil.copytree(HERE / folder, scratch / folder) + sources = decode((HERE / 'PROVENANCE.json').read_bytes())['files'] + assert len(sources) == 5 + for name, source in sources.items(): + assert name in pins + raw = (HERE / name).read_bytes() + if source['uncompress']: + raw = gzip.decompress(raw) + (scratch / name).with_suffix('').write_bytes(raw) + assert sha256(raw).hexdigest() == source['sha256'] + assert sha1(f'blob {len(raw)}\0'.encode() + raw).hexdigest() == source['git_blob'] + anchor = decode((scratch / 'admission/ANCHORED.json').read_bytes()) + for entry in anchor['evidence']: + rel = PurePosixPath(entry['path']) + assert len(rel.parts) == 1 and not rel.is_absolute() and '..' not in rel.parts + assert pins['admission/' + rel.as_posix()] == entry['sha256'] + + +def run(engine, *args, seconds=10, check=True): + argv = [sys.executable, '-I', '-B', str(HERE / 'engines' / engine), *map(str, args)] + return subprocess.run(argv, check=check, capture_output=True, timeout=seconds) + + +def replay(scratch, emit): + authenticate(scratch) + expected = decode((HERE / 'receipts/SHA256.json').read_bytes()) + generated = {} + + def record(name, raw, path=None): + assert sha256(raw).hexdigest() == expected[name], ('different replay receipt', name) + generated[name] = raw + if path is not None: + path.write_bytes(raw) + return decode(raw) + + price = scratch / 'PRICE.json' + price_sha = expected['PRICE.json'] + quoted = record('PRICE.json', run('two_phase.py', scratch, 'price').stdout, price) + assert len(quoted['keys']) == 1950 and Fraction(quoted['whole_optimistic_upper']) == UPPER + assert (sum(quoted['complete_paid'].values()), sum(quoted['complete_targets'].values()), quoted['copies']) == (110536, 22461, 17) + for row in quoted['prices'].values(): + delta = {int(rank): units for rank, units in row['net_delta'].items()} + assert sum(delta.values()) == sum(rank * units for rank, units in delta.items()) == 0 + assert Fraction(row['margin'][0]) > 0 > Fraction(row['extra_paid_rank_one_margin'][1]) + + mod = record('BODY1.json', run('two_phase.py', scratch, 'body-one', '--price-sha', price_sha, + seconds=25).stdout, scratch / 'BODY1.json') + assert mod['visited'] == 1950 and not mod['survivors'] and not mod['unvisited'] + assert mod['controls'] == ['different_orthogonal_bases_cancel_jointly','one_replaced_reflection_fails'] + + inputs = scratch / 'independent-inputs' + inputs.mkdir() + shutil.copyfile(scratch / 'inputs/7113/CALLER.json', inputs / 'CALLER.json') + shutil.copyfile(scratch / 'admission/ADMITTED.json', inputs / 'ADMITTED.json') + exact_out = scratch / 'independent' / 'RESULT.json' + exact_out.parent.mkdir() + argv = ('--inputs', inputs, '--price', price, '--price-sha') + exact = record('EXACT.json', run('four_edits.py', *argv, price_sha, seconds=30).stdout, exact_out) + assert exact['status'] == 'EXHAUSTED' and exact['tested'] == 1950 + assert exact['controls'] == {'fractional_noncommuting_direct_columns':9, 'two_individually_failing_pairs_cancel':True} + comparison = record('COMPARE.json', run('compare.py', scratch).stdout) + assert (comparison['all_keys_matched'], comparison['body_one_survivors'], comparison['unresolved'], + comparison['compatible_saving_in_scope']) == (1950, 0, 0, 0) + assert Fraction(comparison['whole_optimistic_upper']) == UPPER + + # Controls mutate disposable paths only. Neither invalid input reaches the endpoint test. + stale = run('four_edits.py', *argv, '0' * 64, check=False) + assert stale.returncode == 1 and b'changed input: PRICE.json' in stale.stderr and not stale.stdout + caller = scratch / 'inputs/7113/CALLER.json' + caller.write_bytes(caller.read_bytes() + b'\n') + changed = run('two_phase.py', scratch, 'price', check=False) + assert changed.returncode == 1 and b'Changed input inputs/7113/CALLER.json' in changed.stderr and not changed.stdout + + assert generated.keys() == expected.keys() + if emit is not None: + emit.mkdir() + for name, raw in generated.items(): + (emit / name).write_bytes(raw) + print('PASS_P104_TWO_TYPE_B_PHASE_TRANSFERS cases=1950 survivors=0 unresolved=0 ' + 'compatible_saving=0 kappa_change=0') + + +if __name__ == '__main__': + assert __debug__, 'assertions are required' + assert sys.version_info[:2] == (3, 12), 'CPython 3.12 required' + parser = ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path) + options = parser.parse_args() + with TemporaryDirectory(prefix='p104-two-type-b-phase-') as root: + replay(Path(root), options.out)