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-two-paid-subdivision-bank-bound/LOCAL-PINS.json b/research/p104-two-paid-subdivision-bank-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..d9b6b19bb5 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/LOCAL-PINS.json @@ -0,0 +1,24 @@ +{ + "PROVENANCE.json": "bb83bf52f9cbb33823341e120f8364197e037fb2dd4a77d6e649ce8b36cd209b", + "engines/r120/check.py": "22f26e7b3268fb927b99ebac9f04dd02cd73e2b8ac300b2156f9bb79304b4759", + "engines/r120/compare.py": "d1424905c06d39bedc741893a2ba4749226164a6402ae1d234daf74bffa35fc0", + "engines/r120/freeze.py": "4cb413c43904775c20998d5c3a08bc54abbf8b55f970b24d8b3e1bb13de04b86", + "engines/r120/prefix.py": "11445aaa594e34c360a869051af63bb85a7cc433b777e0ac1c0c525de73fa8bf", + "engines/r99/geometry.py": "cd8d0d042ec0fab012cb5c8c167913878301def765c8a924b157d7c542cf7397", + "engines/r99/modular.py": "9cb67eb5f600953a76660eed198346b7124fc10e82a996a33314acae057de572", + "engines/r99/quote.py": "3f1faf8acbb680dc7878678b12f995193751b149f8cf89c6f683d4250be5abed", + "engines/r99/select.py": "2472f9acd4fe8f80000ab853aa78300bdb3ed333227e1b8722c70f9ca722153e", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/BENCHMARK.json": "004331cff6ca8644489d7b7084e5c67439d74a2d283e4d64a9fdb9f88679253d", + "inputs/PR7362-SHA256.json": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "inputs/R92-GEOMETRY.json.gz": "37f15e69eff20041c2e40683d53fd19f75c3c2a951432e4ab4510f3afda80633", + "inputs/R92-PRICE.json.gz": "857b2776d4fb18844a08c82bb9387ddb3332d025bc7ecef2e606e6666705acf2", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "inputs/paired_support.py": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "receipts/AGREEMENT.json": "a85277d8bb97dbe1d4880032f3058604532de5fa5bb96b33977095b54b02d8c6", + "receipts/SHA256.json": "73b857d2ef0b6555e9df0179d3d3dda9f033076d8d701f83ee3bf45a1720748e", + "replay.py": "0b136fe9b8e30e3b86702c3a87e8a25cf8a4a720f995ea7ba9afb56ac9e1833c" +} diff --git a/research/p104-two-paid-subdivision-bank-bound/NOTICE b/research/p104-two-paid-subdivision-bank-bound/NOTICE new file mode 100644 index 0000000000..d4f16de5c7 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/NOTICE @@ -0,0 +1,8 @@ +Apache-2.0. + +#7334 and #7113 supply the exact word and signed caller. #7338 +and #7298 supply the signed invoice readback and directed tariff. +#7362 and #7364 supply the exact singleton stock and retimed +occupancy method. #7148, #7117 and #5751 supply constructive paid +subdivision precedents. #7355 and #7339 supply reused rational +support engines. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-two-paid-subdivision-bank-bound/PROOF.md b/research/p104-two-paid-subdivision-bank-bound/PROOF.md new file mode 100644 index 0000000000..5808839d5a --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/PROOF.md @@ -0,0 +1,81 @@ +# Exact exterior prefix obstruction + +Fix the exact #7334 word, original public and owned role bindings and the +615-role productive cohort with endpoints 3→127. At each typed cut, +two existing public MOVEs may each be split into two paid rank-one +MOVEs through the same strict binary subspace. Their incident-free +windows must overlap. The original chronology and all other roles +are fixed. A rank-four or rank-five chart with the same span may already +have a literal label. A span without a label is virtual. A permitted +bank has no owned occupant. The 102 surviving geometric representatives +all contain precisely their two moved public roles. + +In the normalized chart coordinates of the exact word, a paid MOVE +changes the physical chart and acts as identity on its public row. +The original rows of each mover are constant throughout its incident-free +window, including across its paid MOVE. The substitution preserves +those normalized rows. Group the representatives by their two +anchor clocks and mover roles. Within a group the incident-free +windows agree, the row roles are the same, and their exterior prefix +matrix is constant. This gives 17 support forms. The alias argument +concerns normalized prefix support. Distinct binary spans and signed +physical chart descriptors remain distinct. + +For the two normalized rows `r_1,r_2`, let `π_ext` retain precisely +the initial-coordinate axes outside the productive cohort. A split +requires a nonzero prefix combination supported on the cohort, so +some `(a,b) ≠ (0,0)` must satisfy +`a π_ext(r_1) + b π_ext(r_2) = 0`. A nonzero 2×2 minor of these two +exterior rows makes that equation impossible. For the first 16 +forms, the replay checks denominators are units at 65537 and computes +a nonzero minor at each form. Nonzero reduction of a minor over this +prime field implies a nonzero rational minor. + +The final form is representative `[42958,22]`, with anchors +`[42958,1255]` and `[43050,572]`. Both paid MOVEs ascend from chart +762 to 869. The three strict intermediate rank-five spans indexed +22, 33 and 44 have no existing chart label. The nearest literal +contacts of both operands delimit the common pre-event cuts +42958, 42959 and 42960, inclusive. The original event at 42960 +itself is outside the prefix. At 42958 role 1255 executes its paid +MOVE, which leaves its normalized row unchanged. At 42959 role +1074 moves and neither tested row is touched. The exact rational +row walk therefore checks the same exterior minor on axes [0, 890] +at all three cuts. + +```text +[ 1/2 0 ] +[ 0 -1 ] determinant = -1/2 +``` + +The independent row walk certifies the same minor modulo 65537 with +determinant 32768 and also finds nonzero determinant 16384 on axes +[172, 971]. This excludes the nine raw residual keys, including all +six geometric representatives. No suffix, exact unit-pairing or signed +physical prototype is required to reach this prefix exclusion. Those +checks were skipped. The result does not decide a different bank with +additional roles, an unequal-span meeting, or a changed chronology. + +## Directed complete price + +Let `H_r = r^(1−κ)`. Across 17 native invocations the paid histogram +changes by P1 +68 and P2 −34, while the productive histogram changes +by T4 +17, T5 +17 and T9 −17. No old rank-two debit is reused or +credited twice. Paid positions would rise from 110,519 to 110,553 and +productive positions from 22,461 to 22,478. The signed rank surplus +remains 1,424 and empty-root credits remain zero. + +The new minus old complete margin is +`17(H4 + H5 − H9 − 4H1 + 2H2)`. The exact directed net upper is +0.209047826097918 raw to the shown precision at the incumbent +crossing upper `0.00364665195644044790699554028334162`. The +complete probe at crossing upper plus 10⁻⁹ has a certified +lower margin of about 0.208660307681836, before any ancillary +changes. The fixed target `0.0040075385047236` still has +complete margin upper about −139.5374450214273. One additional +paid rank-one position also makes the complete incumbent margin +negative. The charge is an optimistic price for a proposed +literal change. The prefix obstruction leaves no admissible +edit in scope, so no new signed frame, setup or recovery work +can enter an improved construction here. The five framework +premises and retained BIT supplier are inherited. diff --git a/research/p104-two-paid-subdivision-bank-bound/PROVENANCE.json b/research/p104-two-paid-subdivision-bank-bound/PROVENANCE.json new file mode 100644 index 0000000000..6ff4128dd0 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/PROVENANCE.json @@ -0,0 +1,65 @@ +{ + "caller": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "scope": "Retained signed caller and pricing premises; no caller replay in this package.", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7113" + }, + "chronology": { + "scope": "Recorded 16 completed support forms and one capped form; replay reconstructs all outputs.", + "source": "https://github.com/CrocSwap/integer-mult-bounds/discussions/7111#discussioncomment-19555656" + }, + "files": { + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/PR7362-SHA256.json": { + "commit": "5eec7ed633dcf9b9bbc95552aa653da296f863fb", + "git_blob": "b1486e0b5cfe4535f381ed26f7bce4aee21d8a43", + "path": "research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json", + "sha256": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/5eec7ed633dcf9b9bbc95552aa653da296f863fb/research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json", + "uncompress": false + }, + "inputs/READBACK.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "625b508eead24b4428253bd257620b7e775800c1", + "path": "research/p104-compensated-fusion-readout-bound/price/READBACK.json", + "sha256": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/price/READBACK.json", + "uncompress": false + }, + "inputs/donor_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "46e4621b69bba513f327de53153298e7f4ca0645", + "path": "research/p104-owned-add-source-span-bound/engines/forward.py", + "sha256": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/forward.py" + }, + "inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "generated": { + "inputs/R92-GEOMETRY.json.gz": { + "manifest": "inputs/PR7362-SHA256.json", + "payload_key": "R92-GEOMETRY.json", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7362" + }, + "inputs/R92-PRICE.json.gz": { + "manifest": "inputs/PR7362-SHA256.json", + "payload_key": "R92-PRICE.json", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7362" + } + }, + "schema_version": 1 +} diff --git a/research/p104-two-paid-subdivision-bank-bound/README.md b/research/p104-two-paid-subdivision-bank-bound/README.md new file mode 100644 index 0000000000..2846b5b5e3 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/README.md @@ -0,0 +1,86 @@ +# Shared P104 banks funded by two paid subdivisions + +**NO VERIFIED GAIN.** Exact Δκ = 0 relative to independently reproduced +conditional κ = `0.00364665195644` on +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +`aaeec8c0acf01e99a5f331ef363a698d9c084ace`, with the signed +[#7113 caller](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +`07a76c5e2738882c0cb322278e56f6cae3c9885d`. + +Subdivide two existing paid rank-two public MOVEs to form a common +rank-four or rank-five bank at a shared incident-free cut. Charge both +subdivisions to one productive rank-nine 4+5 split. The bounded stock has +285 quotient lines, 108 pair comparisons and 38,967 typed cuts. Its 102 +geometric representatives reduce to 17 distinct normalized support forms. +The original modular screen excludes 16. The residual form uses roles 572 +and 1255 on the 762→869 ascent. Its three fresh binary spans and three +pre-event cuts give nine raw keys and six geometric representatives. An +exact rational 2×2 exterior prefix minor is nonzero at every cut, and an +independent modular walk checks both its own minor and the original axes. +All 17 forms are excluded, with zero unresolved within this scope. +[Agreement on the residual](receipts/AGREEMENT.json). + +The directed one-edit upper is 0.209047826097918 raw at the incumbent +crossing after charging all four new paid rank-one calls and removing the +two rank-two calls. [Proof and complete price](PROOF.md). + +## Replay + +From a clean checkout, run on POSIX with CPython 3.12 and assertions. + +```sh +python3.12 -I -B research/p104-two-paid-subdivision-bank-bound/replay.py +``` + +The standard-library replay authenticates the word, signed price readback, +directed tariff, and [#7362](https://github.com/CrocSwap/integer-mult-bounds/pull/7362) +predecessor manifest. It regenerates the original price, geometry, +selection and all 16 modular minors. It then regenerates the residual +price, exact and independent rank checks and agreement. A changed +cohort input and a changed residual price both reject. Use +`--out fresh-directory` to retain all eight output files. The replay +needs no Git metadata, network, external dependency root or prior +temporary state. [Provenance](PROVENANCE.json) · +[Path-keyed pins](LOCAL-PINS.json) · [Receipt hashes](receipts/SHA256.json). + +## Open next questions + +Unequal midpoints, shared cuts with additional public occupants, and +changed scalar chronology are outside this closure. To test a distinct +source of savings, start from the two signed chart-32 exchange windows +on role pairs (319, 35) and (1081, 807), with mover anchors +(31303, 38665) and (31360, 37214). Preprice both role itineraries +together, then inspect the peer's nearest source and destination contacts +and exact frame nesting at charts 3 and 355. A positive, legal +joint reframe could remove a paid child while preserving the external +role bindings and productive fields. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +and [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +supply the exact native word and signed caller. +[#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) +supplies the signed invoice readback and +[#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +the directed rational tariff. +[#7362](https://github.com/CrocSwap/integer-mult-bounds/pull/7362) +at `5eec7ed633dcf9b9bbc95552aa653da296f863fb` supplies the exact +95 anchors and 285 quotient lines. +[#7364](https://github.com/CrocSwap/integer-mult-bounds/pull/7364) +supplies the retimed singleton occupancy method and +[#7148](https://github.com/CrocSwap/integer-mult-bounds/pull/7148) +a constructive single-subdivision precedent. +[#7117](https://github.com/CrocSwap/integer-mult-bounds/pull/7117) +supplies a prior two-subdivision construction with different movers +and an additional neutral retime. +[#5751](https://github.com/CrocSwap/integer-mult-bounds/pull/5751) +supplies an earlier charged common meeting. +[#7355](https://github.com/CrocSwap/integer-mult-bounds/pull/7355) +supplies the reused rational row walk and +[#7339](https://github.com/CrocSwap/integer-mult-bounds/pull/7339) +the paired-support helper retained for the conditional suffix branch. +The [original capped result](https://github.com/CrocSwap/integer-mult-bounds/discussions/7111#discussioncomment-19555656) +records the first 16 forms and the residual. OpenAI Codex and +subagents materially assisted proof, implementation, independent +verification and packaging. diff --git a/research/p104-two-paid-subdivision-bank-bound/SOURCES.json b/research/p104-two-paid-subdivision-bank-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/SOURCES.json @@ -0,0 +1,18 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/p104-two-paid-subdivision-bank-bound/TASK.json b/research/p104-two-paid-subdivision-bank-bound/TASK.json new file mode 100644 index 0000000000..5a012181b1 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "On exact #7334, the common rank-four or rank-five banks formed by subdividing two pre-existing paid rank-two public MOVEs in their fixed incident-free chronology, charging both subdivisions and one productive rank-nine 4+5 split.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 two-paid-subdivision bank research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A productive split may improve the binding complex bill only if an intermediate public bank supplies a pure cohort prefix and suffix with exact unit pairing.", + "budget_minutes": 10, + "evidence": "Replays 108 comparisons and 38,967 typed cuts into 17 normalized support forms. The 16 earlier modular forms and one residual exact and independently checked form all fail exterior prefix rank.", + "open_questions": [ + { + "blocked_by": "The simultaneous equal-span two-subdivision bank has no pure prefix in the frozen stock.", + "first_step": "Reprice one exact paid chronology exchange that changes both public itineraries, then freeze the two role-pair windows and compute the incident chart compatibility before any build.", + "question": "Can a two-role change to paid chronology remove a child while preserving both original public output bindings?", + "why_it_matters": "A paid debit can improve the binding complex invoice without requiring a new productive split bank." + } + ], + "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": "Creates a bank with two simultaneous paid subdivisions. Earlier #7362 and #7364 tests use a single moved role against original bank stock.", + "scope_status": "changed", + "stop_rule": "Replay the frozen 285 quotient lines and 16 original support forms within their historical limits. Test only the residual nine typed cuts (one form) at exact rational and 65537, at most 76,466 events and 25 seconds per check; skip suffix and construction on full prefix rank.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-two-paid-subdivision-bank-bound/VERIFICATION.md b/research/p104-two-paid-subdivision-bank-bound/VERIFICATION.md new file mode 100644 index 0000000000..bdc7a0f0b9 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/VERIFICATION.md @@ -0,0 +1,23 @@ +# Verification + +Direct CPython 3.12.14 replay exited 0 in 6.07 seconds. A +relocated Git-free copy with an empty inherited environment +exited 0 in 5.89 seconds and matched all eight regenerated +receipts byte for byte. Both deliberately altered inputs +returned exit 1 before generating output. The residual price +control runs without the native word present. + +The original stock replay checks 285 quotient lines, 108 pair +comparisons and 38,967 typed cuts. Its modular screen excludes +all 16 selected forms and preserves the capped key. The exact +and independent residual checks exhaust three cuts and nine +raw keys. They agree on the original axes [0, 890] and the +nonzero determinant, with zero unresolved forms in the +17-form scope. Each run verifies the applicable arithmetic +and ownership controls. Suffix, signed construction, whole +caller replay and a fresh frontier claim are outside this +prefix certificate. + +The [receipt hashes](receipts/SHA256.json) bind the exact +outputs. See [README.md](README.md) for the checkout-relative +command and [PROVENANCE.json](PROVENANCE.json) for source pins. diff --git a/research/p104-two-paid-subdivision-bank-bound/VERIFY.json b/research/p104-two-paid-subdivision-bank-bound/VERIFY.json new file mode 100644 index 0000000000..a3822114df --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Authenticate the exact signed quote and #7362 geometry. Reproduce all 17 support-form exclusions, compare exact residual minor at 65537, and reject mutated dependencies.", + "timeout_seconds": 125 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-two-paid-subdivision-bank-bound/engines/r120/check.py b/research/p104-two-paid-subdivision-bank-bound/engines/r120/check.py new file mode 100644 index 0000000000..d0ede1b1c1 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/engines/r120/check.py @@ -0,0 +1,146 @@ +"""Check exact support of the frozen virtual two-paid-subdivision bank.""" +from collections import defaultdict +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "plan/PRICE.json": "b29ff21d96485317003db5d06d3332f71e7158de4fafbbc6b300a45fc5d5e3c6", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "inputs/paired_support.py": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + + +def checked(rel): + data = (ROOT / rel).read_bytes() + if sha256(data).hexdigest() != PINS[rel]: + raise ValueError(f"changed dependency {rel}") + return data + + +def unique(items): + doc = dict(items) + if len(doc) != len(items): + raise ValueError("duplicate JSON key") + return doc + + +def span(basis): + out = {0} + for row in basis: + assert row not in out + out |= {row ^ item for item in out} + return out + + +def contacts(event, role): + return role in event[1:3] if event[0] in ("ADD", "COPY") else event[1] == role + + +def geometry(word, price): + program = word["program"] + assert (len(program), word["public"], word["owned_fields"]) == (76466, 1501, 68) + moves, claims = {}, {} + for record in price["intervals"]: + assert record["chart"] is None and [record["first"], record["last"]] == [42958, 42960] + midway = span(record["basis"]) + assert len(midway) == 32 and all(midway != span(frame) for frame in word["frames"]) + claims[record["pair"]] = sorted(midway) + for clock, role, first, last, low, high in (record["left"], record["right"]): + assert program[clock] == ["MOVE", role, low, high, False] + a, c = (span(word["frames"][index]) for index in (low, high)) + assert (len(a), len(c)) == (16, 64) and a < midway < c + assert not any(contacts(event, role) for event in program[first:clock]) + assert not any(contacts(event, role) for event in program[clock + 1:last]) + assert contacts(program[first - 1], role) and contacts(program[last], role) + assert [word["initial"][role], word["final"][role]] == [3, 127] + moves[role] = [clock, program[clock], first, last] + assert sorted(claims) == [22, 33, 44] and len({tuple(v) for v in claims.values()}) == 3 + return moves, claims + + +def witness(rows, cohort): + a, b = ({i: v for i, v in row.items() if i not in cohort} for row in rows) + axes = sorted(a.keys() | b.keys()) + if not axes: + return None + i = axes[0] + for j in axes[1:]: + sub = [[a.get(i, 0), a.get(j, 0)], [b.get(i, 0), b.get(j, 0)]] + det = sub[0][0] * sub[1][1] - sub[0][1] * sub[1][0] + if det: + return {"axes": [i, j], "matrix": [list(map(str, row)) for row in sub], + "determinant": str(det)} + return None + + +def stop(*_): + raise TimeoutError("hard 25-second gate") + + +def main(): + assert __debug__ + assert witness([{1: Fraction(1, 2)}, {2: Fraction(-3)}], set())["determinant"] == "-3/2" + assert witness([{1: Fraction(1, 2)}, {1: Fraction(-3)}], set()) is None + signal(SIGALRM, stop) + alarm(25) + deadline = monotonic() + 23 + price = loads(checked("plan/PRICE.json"), object_pairs_hook=unique) + raw = decompress(checked("inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest() == PAYLOAD + word = loads(raw, object_pairs_hook=unique) + prior = loads(checked("inputs/R92-PRICE.json"), object_pairs_hook=unique) + cohort = set(prior["endpoint_cohort"]) + assert len(cohort) == 615 + checked("inputs/donor_span.py") + checked("inputs/paired_support.py") + snapshot = run_path(str(ROOT / "inputs/donor_span.py"))["snapshot"] + roles = price["row"]["bank"]["public"] + cuts = sorted({key[0] for key in price["raw_keys"]}) + assert roles == [572, 1255] and cuts == [42958, 42959, 42960] + moves, spans = geometry(word, price) + bank_requests = defaultdict(set) + _, rows = snapshot(word, bank_requests, {t: set(roles) for t in cuts}, deadline) + by_cut = {t: [rows[t, r] for r in roles] for t in cuts if all((t, r) in rows for r in roles)} + assert not by_cut or all(v == next(iter(by_cut.values())) for v in by_cut.values()) + first = by_cut.get(cuts[0]) + proof = witness(first, cohort) if first is not None else None + unresolved = [key for key in price["raw_keys"] if proof is None or key[0] not in by_cut] + status = "prefix exclusion" if proof and not unresolved else "prefix rank drop" if first and not proof else "capped" + if status == "prefix rank drop": + pair = run_path(str(ROOT / "inputs/paired_support.py")) + # Only literal prefix rows are transported into the virtual bank. The + # two paid subpaths act as identities in normalized row coordinates. + prefix_bank = dict(zip(roles, first, strict=True)) + _, in_basis = pair["pure_kernel"](prefix_bank, cohort, deadline) + suffixes, _ = pair["suffix_rows"](word, {cuts[0]: prefix_bank}, deadline) + if cuts[0] in suffixes: + _, out_basis = pair["pure_kernel"](suffixes[cuts[0]], cohort, deadline) + exact = pair["paired"](in_basis, out_basis, deadline) + if exact is None and len(by_cut) == len(cuts): + status, unresolved = "no rational unit pairing", [] + elif exact: + status = "exact support survivor" + proof = {name: {i: str(v) for i, v in row.items()} for name, row in exact.items()} + alarm(0) + print(dumps({ + "head": price["head"], "caller": price["caller"], "pins": PINS, + "status": status, "moves": moves, "fresh_spans": spans, + "cut_count": len(by_cut), "prefix_events": max(by_cut, default=0), + "raw_keys": price["raw_keys"], "representative_keys": price["representative_keys"], + "support_forms": 1, "rows_nnz": list(map(len, first)) if first else None, + "proof": proof, "unresolved": unresolved, + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/engines/r120/compare.py b/research/p104-two-paid-subdivision-bank-bound/engines/r120/compare.py new file mode 100644 index 0000000000..921ce51960 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/engines/r120/compare.py @@ -0,0 +1,63 @@ +"""Check the exact primary minor on all three independent modular prefixes.""" +from fractions import Fraction +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "lead/RESULT.json": "3fd4f688b25bcd213ff3bccdedbfeb4d254d125be90456f8bef686ef06fae664", + "independent/RESULT.json": "94c051452dd777b23913f5dda60f170ae82ae8b3d989bef9ba9687acfccad1fb", + "plan/PRICE.json": "b29ff21d96485317003db5d06d3332f71e7158de4fafbbc6b300a45fc5d5e3c6", +} +PRIME = 65537 + + +def checked(name): + raw = (ROOT / name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError("changed dependency " + name) + return loads(raw) + + +def residue(value): + q = Fraction(value) + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME + + +def main(): + assert __debug__ + lead, independent, price = map(checked, PINS) + assert lead["head"] == independent["head"] == price["head"] + assert independent["prime"] == PRIME + assert lead["raw_keys"] == independent["raw_excluded"] == price["raw_keys"] + assert not lead["unresolved"] and not independent["unresolved"] + assert independent["alias"]["shared_normalized_prefix"] + for role, (previous, at, following) in independent["alias"]["nearest_contacts"].items(): + assert lead["moves"][role][0] == at + assert lead["moves"][role][2:] == [previous + 1, following] + for interval in price["intervals"]: + span = {0} + for v in interval["basis"]: + assert v not in span + span |= {v ^ u for u in span} + assert sorted(span) == lead["fresh_spans"][str(interval["pair"])] + axes = lead["proof"]["axes"] + expected_matrix = [[residue(v) for v in row] for row in lead["proof"]["matrix"]] + expected_determinant = residue(lead["proof"]["determinant"]) + cuts = [] + for row in independent["rows"]: + assert row["rank"] == 2 and len(axes) == len(set(axes)) == 2 + actual = [[vector.get(str(j), 0) for j in axes] for vector in row["exterior"]] + determinant = (actual[0][0] * actual[1][1] - actual[0][1] * actual[1][0]) % PRIME + assert actual == expected_matrix and determinant == expected_determinant != 0 + cuts.append(row["cut"]) + assert len(cuts) == 3 + print(dumps(dict(pins=PINS, cut_agreement=cuts, raw_keys_agreement=len(price["raw_keys"]), + primary_exact_axis=axes, primary_axes_matrix_mod_65537=expected_matrix, + primary_axes_det_mod_65537=expected_determinant, unresolved=0), + indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/engines/r120/freeze.py b/research/p104-two-paid-subdivision-bank-bound/engines/r120/freeze.py new file mode 100644 index 0000000000..2ba37e1c43 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/engines/r120/freeze.py @@ -0,0 +1,97 @@ +"""Authenticate and price the one unvisited two-paid subdivision support bank.""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/BENCHMARK.json": "004331cff6ca8644489d7b7084e5c67439d74a2d283e4d64a9fdb9f88679253d", + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/R99-PRICE.json": "0eba831b917331f7a84f4d8a5da726577ed516f04c5f1b94671e031dd2c0b3b4", + "inputs/R99-GEOMETRY.json": "c89976cd5f808c29ab13770e262b2d216f56b4e1703ef836c3438d60f40eb11b", + "inputs/R99-SELECTION.json": "3a6f588eb597e56abfbfe568319fc81294d16d37f03f8b6159ba5b133dc2f416", + "inputs/R99-MODULAR.json": "4d24d44be888a52ac93e589bf7a15978317395b0d3ddc6d96dd2e6d14bde5b44", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", +} + + +def unique(items): + doc = dict(items) + if len(doc) != len(items): + raise ValueError("duplicate JSON key") + return doc + + +def hist(data): + return Counter({int(rank): count for rank, count in data.items()}) + + +def main(): + docs = [] + for path, expected in PINS.items(): + raw = (ROOT / path).read_bytes() + if sha256(raw).hexdigest() != expected: + raise ValueError(f"changed dependency {path}") + if path.endswith(".json"): + docs.append(loads(raw, object_pairs_hook=unique)) + bench, prior, old_price, geo, select, modular = docs + assert len({d["head"] for d in docs}) == 1 + assert select["geometry_sha256"] == PINS["inputs/R99-GEOMETRY.json"] + assert geo["stage"] == "complete" and geo["timeout"] is None and geo["visited_cuts"] == 38967 + assert modular["counts"] == {"prefix exclusion": 16} + assert len(select["unselected"]) == 1 and select["unselected"] == modular["unvisited"] + row, = select["unselected"] + assert row["anchors"] == [[42958, 1255], [43050, 572]] + assert row["bank"]["key"] == [42958, 22] and row["chart"] is None + intervals = [geo["pair_intervals"][i] for i in (22, 33, 44)] + assert all(w["chart"] is None and w["first"] == 42958 and w["last"] == 42960 for w in intervals) + representatives = [row["bank"]["key"], *row["aliases"]] + raw_keys = [[t, w["pair"]] for t in range(42958, 42961) for w in intervals] + assert representatives == raw_keys[:6] + assert row["bank"]["public"] == row["bank"]["pivots"] == [572, 1255] + assert row["bank"]["owned"] == [] + assert all(r in prior["endpoint_cohort"] for r in (572, 1255)) + assert len(prior["endpoint_cohort"]) == 615 + + paid, target = hist(prior["old_paid"]), hist(prior["old_targets"]) + old = target.copy() + old.subtract(paid) + paid.update({1: 68, 2: -34}) + target.update({4: 17, 5: 17, 9: -17}) + assert paid == hist(old_price["new_paid"]) and target == hist(old_price["new_targets"]) + new = target.copy() + new.subtract(paid) + assert sum(r * n for r, n in old.items()) == sum(r * n for r, n in new.items()) == 1424 + change = new.copy() + change.subtract(old) + cost = run_path(str(ROOT / "inputs/pricing.py"))["cost"] + at, probe, fixed = map(Fraction, (old_price["old_crossing_upper"], old_price["probe"], old_price["moonshot"])) + assert at == Fraction(bench["crossing"][1]) + assert at < probe < Fraction(old_price["retained_bit_premise"]) + net = cost(change, at) + candidate = cost(new, probe) + assert list(map(str, net)) == old_price["one_net_at_crossing"] + assert list(map(str, candidate)) == old_price["complete_probe"] and candidate[0] > 0 + extra = cost(new, at)[1] - 1 + assert extra < 0 + print(dumps({ + "pins": PINS, "head": bench["head"], "caller": old_price["caller_head"], + "word_sha256": old_price["word_sha256"], "row": row, "intervals": intervals, + "representative_keys": representatives, "raw_keys": raw_keys, + "paid_delta": old_price["paid_delta"], "productive_delta": old_price["target_delta"], + "paid": sum(paid.values()), "productive": sum(target.values()), "rank_surplus": 1424, + "old_crossing_upper": str(at), "probe": str(probe), "probe_complete_margin": list(map(str, candidate)), + "one_compatible_edit_net": list(map(str, net)), "extra_rank_one_upper": str(extra), + "fixed_target": str(fixed), "fixed_target_complete_upper": str(cost(new, fixed)[1]), + "caps": {"raw_keys": 9, "support_forms": 1, "events_per_direction": 76466, + "runner_seconds": 25, "exact_pairs": 1, "exact_seconds": 35, "prototype_seconds": 120}, + "scope": "One shared fresh rank-five bank, two fully charged rank-two subdivisions, one productive 4+5 split.", + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + assert __debug__ + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/engines/r120/prefix.py b/research/p104-two-paid-subdivision-bank-bound/engines/r120/prefix.py new file mode 100644 index 0000000000..014c5b32de --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/engines/r120/prefix.py @@ -0,0 +1,184 @@ +"""Independent second-prime exterior prefix and alias check for the last R99 bank.""" +from argparse import ArgumentParser +from bisect import bisect_left +from collections import Counter +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "plan/PRICE.json": "b29ff21d96485317003db5d06d3332f71e7158de4fafbbc6b300a45fc5d5e3c6", + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "inputs/7334-WORD.json.gz": WORD, +} +MOVERS = [572, 1255] +ANCHORS = {572: 43050, 1255: 42958} +LOW, HIGH = 762, 869 +CUTS, PAIRS = (42958, 42959, 42960), (22, 33, 44) +EVENTS, SECONDS, PRIME = 76466, 25, 65537 + + +def checked(root, rel): + data = (root / rel).read_bytes() + if sha256(data).hexdigest() != PINS[rel]: + raise ValueError("changed dependency " + rel) + return data + + +def freeze(root, engine): + load = lambda name: loads(checked(root, name), object_pairs_hook=engine["unique"]) + price = load("plan/PRICE.json") + cohort_data = load("inputs/R92-PRICE.json") + cohort = set(cohort_data["endpoint_cohort"]) + assert price["head"] == cohort_data["head"] == HEAD and price["caller"] == CALLER + assert price["pins"]["inputs/R92-PRICE.json"] == PINS["inputs/R92-PRICE.json"] + assert price["word_sha256"] == WORD and len(cohort) == 615 and set(MOVERS) <= cohort + caps = price["caps"] + assert (caps["events_per_direction"], caps["raw_keys"], caps["support_forms"], caps["runner_seconds"]) == (EVENTS, 9, 1, SECONDS) + assert price["raw_keys"] == [[t, i] for t in CUTS for i in PAIRS] + assert price["row"]["bank"]["public"] == price["row"]["bank"]["pivots"] == MOVERS + assert not price["row"]["bank"]["owned"] and price["row"]["chart"] is None + assert sorted(price["row"]["anchors"]) == sorted([t, r] for r, t in ANCHORS.items()) + return price, cohort + + +def geometry(word, price, engine, span): + frames = word["frames"] + low, high = span(LOW), span(HIGH) + assert len(low) == 16 and len(high) == 64 and low < high + spans = set() + for interval in price["intervals"]: + key, basis = interval["pair"], interval["basis"] + assert key in PAIRS and interval["chart"] is None + assert [interval["first"], interval["last"]] == [CUTS[0], CUTS[-1]] + assert len(basis) == 5 + mid = frozenset(engine["span"](basis)) + assert len(mid) == 32 and low < mid < high + spans.add(mid) + assert len(spans) == 3 + # A fresh chart has no pre-existing physical occupant or matching old label. + catalogue = {span(chart) for chart, frame in enumerate(frames) if len(frame) == 5} + assert spans.isdisjoint(catalogue) + for r, at in ANCHORS.items(): + assert word["program"][at] == ["MOVE", r, LOW, HIGH, False] + assert (word["initial"][r], word["final"][r]) == (3, 127) + return len(catalogue) + + +def sweep(word, price, cohort, engine, deadline, progress, rows, denoms): + n, owned, tape = word["public"], word["owned_fields"], word["program"] + assert (n, owned, len(tape)) == (1501, 68, EVENTS) + + @cache + def span(chart): + return frozenset(engine["span"](word["frames"][chart])) + + catalogue = geometry(word, price, engine, span) + state = word["initial"] + [None] * owned + vectors = [{j: 1} for j in range(n)] + [None] * owned + fresh, incidents = set(), {r: [] for r in MOVERS} + for t in range(EVENTS + 1): + progress["first_unvisited_cut"] = t + if (t % 128 == 0 or t in CUTS) and monotonic() >= deadline: + raise TimeoutError("literal prefix cap") + if t in CUTS: + assert [state[r] for r in MOVERS] == [LOW, LOW if t == CUTS[0] else HIGH] + proof = engine["classify"](MOVERS, vectors, cohort) + exterior = [{j: a for j, a in sorted(vectors[r].items()) if j not in cohort} for r in MOVERS] + minor = None + if proof["rank"] == 2: + axes = proof["minor_axes"] + matrix = [[v.get(j, 0) for j in axes] for v in exterior] + det = (matrix[0][0] * matrix[1][1] - matrix[0][1] * matrix[1][0]) % PRIME + assert det == proof["determinant"] != 0 and set(axes).isdisjoint(cohort) + minor = {"axes": axes, "matrix": matrix, "determinant": det} + rows[t] = dict(cut=t, old_charts=[state[r] for r in MOVERS], + full_rows=[dict(vectors[r]) for r in MOVERS], exterior=exterior, + rank=proof["rank"], minor=minor) + if t == EVENTS: + assert state == word["final"] + [None] * owned and not fresh + progress["first_unvisited_cut"] = None + break + event = tape[t] + op, d, *args = event + touched = (d, args[0]) if op in ("ADD", "COPY") else (d,) + for r in touched: + if r in incidents: + incidents[r].append(t) + if op == "MOVE": + a, b, is_owned = args + assert span(a) < span(b) or is_owned and span(b) < span(a) + engine["apply"](event, state, vectors, fresh, n, denoms, False) + progress["events"] += 1 + + neighbors = {} + for r, times in incidents.items(): + i = bisect_left(times, ANCHORS[r]) + assert 0 < i < len(times) - 1 and times[i] == ANCHORS[r] + neighbors[r] = [times[i - 1], times[i], times[i + 1]] + assert neighbors == {572: [42955, 43050, 43051], 1255: [42957, 42958, 42960]} + assert [max(row[0] + 1 for row in neighbors.values()), min(row[2] for row in neighbors.values())] == [CUTS[0], CUTS[-1]] + assert [t for t in range(CUTS[0], CUTS[-1]) if any(t in xs for xs in incidents.values())] == [42958] + # The only incident event inside the half-open alias corridor is a normalized MOVE. + assert tape[42958] == ["MOVE", 1255, LOW, HIGH, False] + assert all(rows[t]["full_rows"] == rows[CUTS[0]]["full_rows"] for t in CUTS) + return dict(nearest_contacts=neighbors, transition_events=[[t, tape[t]] for t in range(CUTS[0], CUTS[-1])], + distinct_fresh_rank_five_spaces=3, existing_distinct_rank_five_spaces=catalogue, + shared_normalized_prefix=True) + + +def main(): + parser = ArgumentParser() + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + assert __debug__ + name = "inputs/second_prime.py" + checked(args.root, name) + engine = run_path(str(args.root / name)) + controls = engine["controls"]() + assert engine["PRIME"] == PRIME + price, cohort = freeze(args.root, engine) + if args.controls_only: + print(dumps(dict(controls=controls, raw_keys=price["raw_keys"]), indent=2)) + return 0 + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + signal(SIGALRM, stop) + alarm(SECONDS) + progress = {"events": 0, "first_unvisited_cut": 0} + rows, denoms, alias, timeout = {}, set(), None, None + try: + payload = decompress(checked(args.root, "inputs/7334-WORD.json.gz")) + assert sha256(payload).hexdigest() == PAYLOAD + word = loads(payload, object_pairs_hook=engine["unique"]) + alias = sweep(word, price, cohort, engine, monotonic() + 23, progress, rows, denoms) + except TimeoutError as exc: + timeout = str(exc) + finally: + alarm(0) + proven = [key for key in price["raw_keys"] if alias is not None and rows[key[0]]["rank"] == 2] + unresolved = [key for key in price["raw_keys"] if key not in proven] + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, price_caps=price["caps"], controls=controls, + prime=PRIME, public=MOVERS, projection_cohort_size=len(cohort), rows=list(rows.values()), + progress=progress, denominator_units=sorted(denoms), alias=alias, timeout=timeout, + counts=Counter("full prefix rank" if r["rank"] == 2 else "prefix drop" for r in rows.values()), + raw_excluded=proven, unresolved=unresolved), indent=2, sort_keys=True)) + return 2 if timeout else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/p104-two-paid-subdivision-bank-bound/engines/r99/geometry.py b/research/p104-two-paid-subdivision-bank-bound/engines/r99/geometry.py new file mode 100644 index 0000000000..4b304b1d39 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/engines/r99/geometry.py @@ -0,0 +1,229 @@ +"""Find simultaneous mover-disjoint paid subdivisions with one common span.""" +from bisect import bisect_left +from collections import defaultdict +from gzip import decompress +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "lead/PRICE.json": "0eba831b917331f7a84f4d8a5da726577ed516f04c5f1b94671e031dd2c0b3b4", + "inputs/R92-GEOMETRY.json": "e9f93f3271855012b2de705c70f186f78c31a369d28110e92c5f2ffadae209b3", + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def checked(name): + value = (ROOT/name).read_bytes() + if sha256(value).hexdigest() != PINS[name]: + raise ValueError(f"changed dependency {name}") + if name.endswith(".gz"): + value = decompress(value) + assert sha256(value).hexdigest() == PAYLOAD + return json.loads(value,object_pairs_hook=unique) + + +def space(basis): + values = {0} + for v in basis: + assert v not in values + values.update(v^w for w in tuple(values)) + return frozenset(values) + + +def basis_of(span): + values = {0} + basis = [] + for v in span: + if v not in values: + values.update(v^w for w in tuple(values)) + basis.append(v) + assert values == set(span) + return basis + + +def incident(event): + op,d,*args = event + return (d,args[0]) if op in ("ADD","COPY") else (d,) + + +def window(clocks,at,end): + i = bisect_left(clocks,at) + assert clocks[i] == at + return (clocks[i-1]+1 if i else 0, clocks[i+1] if i+1 < len(clocks) else end) + + +def controls(): + assert incident(["COPY",5,2,"-3/2",3]) == (5,2) + assert window([0,3,5],3,7) == (1,5) + assert basis_of((0,1,4,5)) == [1,4] + assert space([1,4]) == frozenset((0,1,4,5)) + assert space([4,5]) == space([1,4]) + return ["source contact", "inclusive pre-event windows", "canonical span", "basis-invariant equality"] + + +def stopped(*_): + raise TimeoutError("hard runner limit") + + +def cap(condition,label): + if condition: + raise TimeoutError(label) + + +def main(): + assert __debug__ + price = checked("lead/PRICE.json") + limits = price["limits"] + signal(SIGALRM,stopped) + alarm(limits["geometry_seconds"]) + deadline = monotonic()+18 + out = {"stage":"authenticate","visited_placements":0,"pair_comparisons":0,"scheduled_cuts":0, + "visited_cuts":0,"owned_rejections":0,"representatives":[],"pair_intervals":[], + "outside_window":[],"first_unvisited_event":None,"current_pair":None} + reason = None + try: + previous = checked("inputs/R92-GEOMETRY.json") + prior_price = checked("inputs/R92-PRICE.json") + word = checked("inputs/7334-WORD.json.gz") + cohort = set(prior_price["endpoint_cohort"]) + program = word["program"] + n = word["public"] + size = len(program) + assert (n,word["owned_fields"],size) == (1501,68,limits["events_each"]) + out["stage"] = "mover contacts" + clocks = defaultdict(list) + for t,event in enumerate(program): + if t % 128 == 0: + out["first_unvisited_event"] = t + cap(monotonic()>=deadline,"mover contacts deadline") + for role in incident(event): + clocks[role].append(t) + frames = word["frames"] + spaces = [space(f) for f in frames] + labels = defaultdict(list) + for chart,span in enumerate(spaces): + if len(frames[chart]) in (4,5): + labels[tuple(sorted(span))].append(chart) + groups = defaultdict(list) + out["stage"] = "group frozen quotient lines" + for p in previous["raw_placements"]: + at,role,rank,v = (p["move_clock"],p["mover"],p["rank"],p["quotient_representative"]) + op,d,a,c,owned = program[at] + assert op == "MOVE" and d == role and d in cohort and not owned + lo,hi = spaces[a],spaces[c] + mid = lo | {x^v for x in lo} + assert lo < mid < hi and len(mid) == 2**rank + span = tuple(sorted(mid)) + assert [r["chart"] for r in p["labels"]] == labels[span] + first,last = window(clocks[role],at,size) + groups[span].append((at,role,first,last,a,c)) + out["visited_placements"] += 1 + assert out["visited_placements"] == limits["placement_count"] + out["distinct_spans"] = len(groups) + out["pair_stock"] = sum(len(entries)*(len(entries)-1)//2 for entries in groups.values()) + out["stage"] = "pair windows" + tasks = defaultdict(list) + for span,rows in sorted(groups.items()): + for left,right in combinations(sorted(rows),2): + out["current_pair"] = [left[0],right[0],list(span)] + cap(out["pair_comparisons"]>=limits["pair_comparisons"] or monotonic()>=deadline,"pair cap") + out["pair_comparisons"] += 1 + assert left[0] != right[0] and left[1] != right[1] + first,last = max(left[2],right[2]),min(left[3],right[3]) + if first > last: + out["outside_window"].append(out["current_pair"]) + continue + for chart in labels[span] or [None]: + pair_id = len(out["pair_intervals"]) + out["pair_intervals"].append({"pair":pair_id,"chart":chart,"basis":basis_of(span), + "left":left,"right":right,"first":first,"last":last}) + for t in range(first,last+1): + cap(out["scheduled_cuts"]>=limits["raw_pair_cuts"],"scheduled pair cut cap") + tasks[t].append(pair_id) + out["scheduled_cuts"] += 1 + assert out["pair_stock"] == out["pair_comparisons"] + out["current_pair"] = None + + out["stage"] = "public bank snapshots" + chart_of = word["initial"][:] + [None] * word["owned_fields"] + banks = defaultdict(set) + last_contact = {} + previous_class = {} + for t in range(size+1): + if t % 128 == 0: + out["first_unvisited_event"] = t + cap(monotonic()>=deadline,"bank replay deadline") + if t == 0: + for r,c in enumerate(word["initial"]): + banks[c].add(r) + for pair_id in tasks.get(t,()): + out["visited_cuts"] += 1 + row = out["pair_intervals"][pair_id] + chart = row["chart"] + a,d,*_ = row["left"] + b,e,*_ = row["right"] + current = banks[chart] if chart is not None else set() + assert not {d,e} & current + if any(r >= n for r in current): + out["owned_rejections"] += 1 + continue + token = (last_contact.get(chart),t>a,t>b) + if previous_class.get(pair_id) == token: + continue + previous_class[pair_id] = token + public = sorted(current|{d,e}) + out["representatives"].append({"key":[t,pair_id],"public":public,"owned":[], + "pivots":sorted(set(public)&cohort),"previous_chart_contact":token[0]}) + if t == size: + break + op,d,*args = program[t] + src = chart_of[d] + if src is not None: + last_contact[src] = t + if op in ("MOVE","INIT"): + dest = args[1] if op == "MOVE" else args[0] + if op == "MOVE": + assert src == args[0] and args[2] == (d>=n) + banks[src].remove(d) + else: + assert src is None and d>=n + banks[dest].add(d) + chart_of[d] = dest + last_contact[dest] = t + elif op == "CLEAR": + assert src == args[0] and d>=n + banks[src].remove(d) + chart_of[d] = None + else: + assert op in ("ADD","COPY","SCALE") and src == args[-1] + if op in ("ADD","COPY"): + assert chart_of[args[0]] == src + assert chart_of == word["final"] + [None] * word["owned_fields"] + assert out["scheduled_cuts"] == out["visited_cuts"] + out.update(stage="complete",first_unvisited_event=None) + except TimeoutError as exc: + reason = str(exc) + finally: + alarm(0) + print(json.dumps(dict(head=price["head"],pins=PINS,limits=limits,controls=controls(),timeout=reason,**out), + indent=2,sort_keys=True)) + if reason: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/engines/r99/modular.py b/research/p104-two-paid-subdivision-bank-bound/engines/r99/modular.py new file mode 100644 index 0000000000..f5e1212a95 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/engines/r99/modular.py @@ -0,0 +1,81 @@ +"""Two-sided exterior minors on frozen virtual two-mover banks.""" +from collections import Counter +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "lead/SELECTION.json": "3a6f588eb597e56abfbfe568319fc81294d16d37f03f8b6159ba5b133dc2f416", + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", +} + + +def side(word,banks,cohort,deadline,engine,back): + n = word["public"] + owned = word["owned_fields"] + tape = word["program"] + start = "final" if back else "initial" + active = word[start][:]+[None]*owned + vectors = [{i:1} for i in range(n)]+[None]*owned + cuts = range(len(tape),-1,-1) if back else range(len(tape)+1) + out = {} + fresh,denom = set(),set() + for t in cuts: + if (t%128==0 or t in banks) and monotonic()>=deadline: + break + if t in banks: + out[t] = engine["classify"](banks[t],vectors,cohort) + if t == (0 if back else len(tape)): + assert active == word["initial" if back else "final"]+[None]*owned + break + engine["apply"](tape[t-1 if back else t],active,vectors,fresh,n,denom,back) + return out,sorted(denom) + + +def main(): + assert __debug__ + documents = {} + for path,digest in PINS.items(): + raw = (ROOT/path).read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError(f"changed dependency {path}") + documents[path] = raw + engine = run_path(str(ROOT/"inputs/second_prime.py")) + unique = engine["unique"] + word = json.loads(decompress(documents["inputs/7334-WORD.json.gz"]),object_pairs_hook=unique) + selection = json.loads(documents["lead/SELECTION.json"],object_pairs_hook=unique) + cohort = set(json.loads(documents["inputs/R92-PRICE.json"],object_pairs_hook=unique)["endpoint_cohort"]) + assert len(word["program"])==76466 and len(cohort)==615 + controls = engine["controls"]() + rows = selection["selected"] + banks = {r["bank"]["key"][0]:r["bank"]["public"] for r in rows} + assert len(banks)==len(rows)==selection["case_cap"]==16 + deadline = monotonic()+22 + f,df = side(word,banks,cohort,deadline,engine,False) + open_banks = {t:v for t,v in banks.items() if t in f and f[t]["rank"]<2} + s,ds = side(word,open_banks,cohort,deadline,engine,True) if open_banks else ({},[]) + results = [] + for row in rows: + t = row["bank"]["key"][0] + p,q = f.get(t),s.get(t) + if p and p["rank"] == 2: + status = "prefix exclusion" + elif q: + status = "suffix exclusion" if q["rank"]==2 else "dual drop" + else: + status = "capped" + results.append(row|dict(status=status,prefix=p,suffix=q)) + print(json.dumps(dict(head=selection["head"],pins=PINS,cap=16,runner_seconds=25, + prime=engine["PRIME"],controls=controls,denominator_units={"prefix":df,"suffix":ds}, + results=results,counts=Counter(r["status"] for r in results),unvisited=selection["unselected"]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/engines/r99/quote.py b/research/p104-two-paid-subdivision-bank-bound/engines/r99/quote.py new file mode 100644 index 0000000000..fef95bf2e9 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/engines/r99/quote.py @@ -0,0 +1,95 @@ +"""Directed price for two paid rank-two subdivisions funding one 4+5 split.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/BENCHMARK.json": "004331cff6ca8644489d7b7084e5c67439d74a2d283e4d64a9fdb9f88679253d", + "inputs/R92-GEOMETRY.json": "e9f93f3271855012b2de705c70f186f78c31a369d28110e92c5f2ffadae209b3", + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", +} + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def hist(document): + return Counter({int(key): value for key, value in document.items()}) + + +def main(): + docs = [] + for path,pin in PINS.items(): + raw = (ROOT/path).read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"changed dependency {path}") + if path.endswith(".json"): + docs.append(json.loads(raw,object_pairs_hook=unique)) + bench,geo,prior = docs + assert bench["head"] == geo["head"] == prior["head"] == "aaeec8c0acf01e99a5f331ef363a698d9c084ace" + assert geo["word_sha256"] == prior["word_sha256"] + assert geo["price_sha256"] == PINS["inputs/R92-PRICE.json"] + placement = geo["raw_placements"] + anchors = {r["move_clock"] for r in placement} + roles = {r["mover"] for r in placement} + assert len(anchors) == 95 and len(placement) == 285 + stock = min(len(anchors),len(roles))//2 + paid = hist(prior["old_paid"]) + target = hist(prior["old_targets"]) + assert sum(paid.values()) == 110519 and sum(target.values()) == 22461 + old = target.copy() + old.subtract(paid) + assert sum(r*n for r,n in old.items()) == 1424 + new_paid = paid.copy() + paid_delta = {1:68, 2:-34} + new_paid.update(paid_delta) + new_target = target.copy() + target_delta = {4:17,5:17,9:-17} + new_target.update(target_delta) + new = new_target.copy() + new.subtract(new_paid) + assert sum(r*n for r,n in new.items()) == 1424 + assert sum(new_paid.values()) == 110553 and sum(new_target.values()) == 22478 + change = new.copy() + change.subtract(old) + cost = run_path(str(ROOT/"inputs/pricing.py"))["cost"] + at = Q(prior["old_crossing_upper"]) + probe = Q(prior["probe"]) + bit = Q(prior["retained_bit_premise"]) + moon = Q(prior["moonshot"]) + assert at == Q(bench["crossing"][1]) and at < probe < bit < moon + net = cost(change,at) + complete_probe = cost(new,probe) + extra_child = cost(new,at)[1]-1 + moon_net = cost(change,moon) + moon_complete = cost(old,moon)[1] + stock * max(Q(0),moon_net[1]) + assert complete_probe[0] > 0 and extra_child < 0 and moon_complete < 0 + data = { + "head": bench["head"],"caller_head":prior["caller_head"],"word_sha256":prior["word_sha256"], + "pins":PINS,"kappa":bench["kappa"],"old_crossing_upper":str(at),"probe":str(probe), + "moonshot":str(moon),"retained_bit_premise":str(bit),"anchors":len(anchors),"roles":len(roles), + "compatibility_cap_before_geometry":stock,"paid_delta":paid_delta,"target_delta":target_delta, + "new_paid":new_paid,"new_targets":new_target,"one_net_at_crossing":list(map(str,net)), + "whole_net_upper":str(stock*net[1]),"complete_probe":list(map(str,complete_probe)), + "complete_upper_with_one_added_rank_one":str(extra_child), + "one_moonshot_net_upper":str(moon_net[1]),"whole_moonshot_complete_upper":str(moon_complete), + "limits":{"event_passes":2,"events_each":76466,"placement_count":285,"pair_comparisons":2000, + "raw_pair_cuts":40000,"geometry_seconds":20,"modular_cases":16,"modular_seconds":25, + "exact_cases":4,"exact_seconds":35,"candidate_builds":1}, + "scope":"Two distinct unprotected cohort roles and two distinct paid rank-two anchors. Each MOVE is replaced by two rank-one MOVEs; one 4+5 target split. Distinct anchors and roles consumed once. Zero ancillary and zero chart-synthesis overhead gives an optimistic upper; no ordinary, routing, ownership or precision/tape credit.", + } + print(json.dumps(data,indent=2,sort_keys=True)) + + +if __name__ == "__main__": + assert __debug__ + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/engines/r99/select.py b/research/p104-two-paid-subdivision-bank-bound/engines/r99/select.py new file mode 100644 index 0000000000..fa3fbc3ee2 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/engines/r99/select.py @@ -0,0 +1,46 @@ +"""Freeze at most 16 distinct two-mover normalized support forms.""" +from collections import defaultdict +from hashlib import sha256 +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +PIN = "c89976cd5f808c29ab13770e262b2d216f56b4e1703ef836c3438d60f40eb11b" + + +def main(): + raw = (ROOT/"lead/GEOMETRY.json").read_bytes() + assert sha256(raw).hexdigest() == PIN + geometry = json.loads(raw) + assert geometry["stage"] == "complete" and not geometry["timeout"] + groups = defaultdict(list) + for row in geometry["representatives"]: + t,i = row["key"] + window = geometry["pair_intervals"][i] + a,d,*_ = window["left"] + b,e,*_ = window["right"] + group = tuple(sorted(((a,d),(b,e)))) + assert not row["owned"] and row["public"] == row["pivots"] == sorted((d,e)) + assert window["first"] <= t <= window["last"] + groups[group].append((row,window)) + entries = [] + for key,rows in groups.items(): + # Original rank/phase normalized rows and columns stay fixed on both + # movers. Their only incident events inside any window are their own + # MOVEs, which are identity in normalized coordinates. + windows = {(w["first"],w["last"]) for _,w in rows} + assert len(windows) == 1 + rows.sort(key=lambda rw:(rw[1]["chart"] is None,rw[0]["key"])) + chosen,w = rows[0] + entries.append({"bank":chosen,"anchors":key,"chart":w["chart"], + "aliases":sorted(row["key"] for row,_ in rows[1:])}) + entries.sort(key=lambda r:(r["chart"] is None,r["bank"]["key"])) + count = geometry["limits"]["modular_cases"] + assert len(entries) == 17 and len({r["bank"]["key"][0] for r in entries}) == len(entries) + print(json.dumps({"head":geometry["head"],"geometry_sha256":PIN, + "case_cap":count,"selected":entries[:count],"unselected":entries[count:]}, + indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/7334-WORD.json.gz b/research/p104-two-paid-subdivision-bank-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-two-paid-subdivision-bank-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/BENCHMARK.json b/research/p104-two-paid-subdivision-bank-bound/inputs/BENCHMARK.json new file mode 100644 index 0000000000..3cadb16667 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/inputs/BENCHMARK.json @@ -0,0 +1,67 @@ +{ + "admission_sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "checks": { + "caller": "PASS_HELPER_319_FUSED_CALLER 91166298911/25000000000000", + "early": "PASS_HELPER_319_EXACT_NATIVE_AND_SIGNED_PRICE 0.00364665195644", + "frontier": "PASS_HELPER_319_FUSED_FRONTIER_PROPOSAL 91166298911/25000000000000", + "native": "PASS_HELPER_319_FUSED_NATIVE 3646017316711/1000000000000000" + }, + "crossing": [ + "0.00364665195644044790699554028334161", + "0.00364665195644044790699554028334162" + ], + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "kappa": "0.00364665195644", + "main": "e54523517d0f03e58352e647c403a5af3e525a57", + "package_sha256": { + "research/p104-helper-319-fused-return/EARLY-RESULT.json": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649", + "research/p104-helper-319-fused-return/ENVIRONMENT.json": "1a4a755aa63e3c25c09a493550a0d13a58e23f8b50083d3f81ce3716581d8ad3", + "research/p104-helper-319-fused-return/INPUTS.json": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d", + "research/p104-helper-319-fused-return/NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "research/p104-helper-319-fused-return/NOTICE": "fd84c06a1c3343a1802808741c0863ffcec031f5c98eb78ddc350a747d3e2ddc", + "research/p104-helper-319-fused-return/PROOF.md": "560de573bfd4563c16ca3c7308fa729b4188fabe802d8830f343c3873f75b59d", + "research/p104-helper-319-fused-return/PROPOSED-CLAIM.json": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03", + "research/p104-helper-319-fused-return/README.md": "b4db0eb83ab6a2f7151bed2da955a487f4816ec9d1976eccc21e54c2725490b0", + "research/p104-helper-319-fused-return/REFERENCE.json": "3e66e054b803551f18b8670da0b2990a7d0eeb689dfc45b56dbcba295551da70", + "research/p104-helper-319-fused-return/REPLAY.txt": "230984f4b8206ae4d0c0f18fbba86ff43a1a9623f8ed337cf1285360f9a67c0c", + "research/p104-helper-319-fused-return/RESULT.json": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194", + "research/p104-helper-319-fused-return/SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "research/p104-helper-319-fused-return/TASK.json": "cceea066802e1175b1a78f65e8bff4677ce09e87fd7686265d63ee7236b32b1a", + "research/p104-helper-319-fused-return/VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "research/p104-helper-319-fused-return/WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "research/p104-helper-319-fused-return/adapt.py": "a9237d6dff55ce13c1e1d10159f592f35a0a79eb0a3c054063ba39665ba96296", + "research/p104-helper-319-fused-return/construct.py": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda", + "research/p104-helper-319-fused-return/derive_grid.py": "ceb7a44ef19d72a16db7b43c65c85910d965499d1715436011de32af5d39dbb0", + "research/p104-helper-319-fused-return/frontier.py": "c5f5e4e1f1f2d189f4816291764f1966c8165a7090d8624f72828199400333c2", + "research/p104-helper-319-fused-return/inputs/pr7314.tar.gz": "0589953b3886d96eacf3bda3d38d8d574bb739fba1056af7f32f56047b6061e2", + "research/p104-helper-319-fused-return/packing_reference.py": "c977cf46a9498d013145f74186081ec67674d11473295df399bca61f8a4e7382", + "research/p104-helper-319-fused-return/price.py": "6ec0f568b3491f3713ffabb2a8cc7b467339da175c8dcaa76369fbc3a9881029", + "research/p104-helper-319-fused-return/source.py": "a2be5bb28c7a9c9d528b8bae0d9ef99636bb8fabf80d66b7f8d3084de68358aa", + "research/p104-helper-319-fused-return/verify_caller.py": "6ef60923041d97f77f8291f568f2e81492af09021f4e1065054cf5376cbff861", + "research/p104-helper-319-fused-return/verify_early.py": "94e0e8bac205eed91f9f1f0ada110479a067ee7a3cd73d38d231947a0d46c0f9", + "research/p104-helper-319-fused-return/verify_native.py": "592729b40642957a4d2766c386d73925a1044d2b4eedce5176d988b8cef3b134" + }, + "receipt_sha256": { + "peer-prep/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "peer-prep/STATIC.json": "500cc563b7dac8b1de1faf1dee9b820e73152dfddc15a650cd1191edd39e8c79", + "peer-price/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "peer-price/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "peer/COMMAND.txt": "714bfab024155d8216f3ef99f3ee7627ddc35ab341c486ac6bd53c476b757130", + "peer/COMMIT.stdout": "597470d8132a3812deb3624a859546c0c13d52b094fd6fc61e7416941130bd70", + "peer/END-UTC.txt": "9c46923c616c14da5b8ed503e1652021d7bd409a10ec91a78a03263013fba08a", + "peer/METADATA.stdout": "5873404cb4424dca918a00d503569f3c29a3190fd029a007e1afb2006399f647", + "peer/RUN.exit": "9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa", + "peer/RUN.stderr": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "peer/RUN.stdout": "d589626c7581fbb9928bc615364cfee49deb62dfc0a39a903417ca62be89cf8c", + "peer/START-UTC.txt": "5b78fd6d42a2b42206891318c08e6014de57d7ca46b0201cd11a166f452210f7" + }, + "source_tree": "fa98712a459b20c10240450097c87de433f8a750", + "status": "exact-complete-receipt-reused" +} diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/PR7362-SHA256.json b/research/p104-two-paid-subdivision-bank-bound/inputs/PR7362-SHA256.json new file mode 100644 index 0000000000..b1486e0b5c --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/inputs/PR7362-SHA256.json @@ -0,0 +1,11 @@ +{ + "R92-COMPARE.json": "92bd567e3203a2cbc2e0c508bf921966c59ead267c1f373f7534a4a50cb208ac", + "R92-GEOMETRY.json": "e9f93f3271855012b2de705c70f186f78c31a369d28110e92c5f2ffadae209b3", + "R92-GUARDS.json": "c23e9c74b3479e4af6c452eeb73e000878148ec385560a0642433a1c5bac4a07", + "R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "R92-REVERSE.json": "f8e56b109352e07dfb8203bdbe42a10cb94374246b4cd419421e4f52e2730c4a", + "R93-COMPARE.json": "8a1f52179e5d457aa729714b0b79577894c1e22ab74a8b2f700838f471ffceb1", + "R93-MODULAR.json": "01ad2a656e69699b80b56d63cdf82448e424cd1c6e67636d53c079a6f03f55a5", + "R93-PRICE.json": "c108a061c6c03306a99a6fbafe919208954a7479ae28fb8a8fbf45d9832e6144", + "R93-RATIONAL.json": "2800af56efe23f7420a12f0713a659cd4fa4a3fb7c58449749ef697097ccccbf" +} diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/R92-GEOMETRY.json.gz b/research/p104-two-paid-subdivision-bank-bound/inputs/R92-GEOMETRY.json.gz new file mode 100644 index 0000000000..bae032baa6 Binary files /dev/null and b/research/p104-two-paid-subdivision-bank-bound/inputs/R92-GEOMETRY.json.gz differ diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/R92-PRICE.json.gz b/research/p104-two-paid-subdivision-bank-bound/inputs/R92-PRICE.json.gz new file mode 100644 index 0000000000..5aabb0ff2e Binary files /dev/null and b/research/p104-two-paid-subdivision-bank-bound/inputs/R92-PRICE.json.gz differ diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/READBACK.json b/research/p104-two-paid-subdivision-bank-bound/inputs/READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/inputs/READBACK.json @@ -0,0 +1,188 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "bit_admitted": "12039/3125000", + "bit_claim_headroom": "3000951089/25000000000000", + "bit_premise": "376669/100000000", + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "claim": "91166298911/25000000000000", + "context_c": 2430, + "context_headroom": 1666, + "copies": 17, + "directed_bounds": { + "new_at_claim": [ + "347195197206460540909548691538238227127/2000000000000000000000000000000000000000000000000", + "1735975986032302704547743457691191192207/10000000000000000000000000000000000000000000000000" + ], + "new_at_old_crossing_upper": [ + "333717954993733063339209580360321337006028706669/2000000000000000000000000000000000000000000000000", + "1668589774968665316696047901801606685030143589709/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_lower": [ + "8890529086421014119/10000000000000000000000000000000000000000000000000", + "8890529086421080299/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_upper": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "new_at_tested": [ + "1464673416007288863003441470091977383033/10000000000000000000000000000000000000000000000000", + "1464673416007288863003441470091977438357/10000000000000000000000000000000000000000000000000" + ], + "old_at_claim": [ + "-1668785950738799647054310634446839861363893886031/10000000000000000000000000000000000000000000000000", + "-66751438029551985882172425377873594454555753177/400000000000000000000000000000000000000000000000" + ], + "old_at_old_crossing_upper": [ + "-357270001119021587349/10000000000000000000000000000000000000000000000000", + "-357270001119021530951/10000000000000000000000000000000000000000000000000" + ] + }, + "empty_root_credits": 0, + "exact_gain": "215259997/500000000000000", + "exact_relative_percent": "21525999700/1823110718223", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "incumbent": "1823110718223/500000000000000", + "main_boundaries": 104, + "native_grid": [ + 1125, + 25 + ], + "native_ingredient_claim": "3646017316711/1000000000000000", + "new_raw_interval": [ + "364665195644044790699554028334161/100000000000000000000000000000000000", + "182332597822022395349777014167081/50000000000000000000000000000000000" + ], + "old_raw_upper": "36462214364462343366888845568981/10000000000000000000000000000000000", + "ordinary": 782715464, + "ordinary_delta": 52088, + "ordinary_headroom": 217284536, + "outer_functional": 4, + "outer_strict": 54, + "outer_strict_slack": "299635334804355997/10000000000000000000000000000000000", + "owned_lifetimes": 73, + "owned_peak": 50, + "paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110519, + "parent": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "path_pins": { + "dependencies/7298/pricing.py": { + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "dependencies/7314/NATIVE-RESULT.json": { + "sha256": "336f463da5afe5b60bfd3b9f0ce8aeea5a5feb1f854613bf4218ba0b28b3371b" + }, + "dependencies/7314/PROPOSED-CLAIM.json": { + "sha256": "41a08c4b7d0b2de4af22bc778948a143027eb3065fff47b0400b6ded1cc52778" + }, + "dependencies/7314/RESULT.json": { + "sha256": "432191ca572c9221935787ebe392699e3a1ef4512b0bf4fbc704657321cc87ca" + }, + "dependencies/round65/price.json": { + "sha256": "25205ad2cf4230bd2b2b704eec9f96ec4a5486fd575b5599861b28ffdd15b00b" + }, + "receipts/EARLY-RESULT.json": { + "git_blob": "675d6cf2374f3384019dfd53b2bdffd845005f13", + "sha256": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649" + }, + "receipts/INPUTS.json": { + "git_blob": "95c53f4594287a72d9b586f10ee136d0a1686984", + "sha256": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d" + }, + "receipts/NATIVE-RESULT.json": { + "git_blob": "eb101307d4d0399efed96d88cf6d4c01ec9c7369", + "sha256": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812" + }, + "receipts/PROOF.md": { + "git_blob": "7644e5571d583183ee93b686612b5ec4555f6911", + "sha256": "560de573bfd4563c16ca3c7308fa729b4188fabe802d8830f343c3873f75b59d" + }, + "receipts/PROPOSED-CLAIM.json": { + "git_blob": "6b491894580741e3e2c11a453722a0302db7b5d6", + "sha256": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03" + }, + "receipts/README.md": { + "git_blob": "b3a055f4e0d334ce2e7df3310caaa0849eb3eba1", + "sha256": "b4db0eb83ab6a2f7151bed2da955a487f4816ec9d1976eccc21e54c2725490b0" + }, + "receipts/REFERENCE.json": { + "git_blob": "8859e243cc39546bcb1e257d95c19a658c455dc7", + "sha256": "3e66e054b803551f18b8670da0b2990a7d0eeb689dfc45b56dbcba295551da70" + }, + "receipts/REPLAY.txt": { + "git_blob": "0b8d8048c18740060f4b7f6d380a5f3a0f30ee53", + "sha256": "230984f4b8206ae4d0c0f18fbba86ff43a1a9623f8ed337cf1285360f9a67c0c" + }, + "receipts/RESULT.json": { + "git_blob": "3034a490f5b0656ae71495c99493c4ab1ac1f5c6", + "sha256": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194" + }, + "receipts/SOURCES.json": { + "git_blob": "6b97e903a6df8de437068a0e2907823885928053", + "sha256": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593" + }, + "receipts/VERIFY.json": { + "git_blob": "cc98ee2a5c5a79e670094a6f55c7cacda8fd330c", + "sha256": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513" + }, + "receipts/construct.py": { + "git_blob": "89e923bd738dfc404ca76b7ae36f13844ac4bfbb", + "sha256": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + } + }, + "physical_maps": 3037, + "productive_fields": 22461, + "rank_surplus": 1424, + "raw_strict_separation": "43051999421357030665572644351/100000000000000000000000000000000000", + "scope": "Exact receipt and directed-price readback. No native or caller execution in this audit.", + "source_archive_sha256": "0589953b3886d96eacf3bda3d38d8d574bb739fba1056af7f32f56047b6061e2", + "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 + }, + "tested": "364665195644007/100000000000000000" +} diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/donor_span.py b/research/p104-two-paid-subdivision-bank-bound/inputs/donor_span.py new file mode 100644 index 0000000000..46e4621b69 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/inputs/donor_span.py @@ -0,0 +1,169 @@ +"""Match the literal ADD source using other live rows in the retimed chart.""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +import sys +from time import monotonic + +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE="c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d" + + +def checked(path,want,compressed=False): + raw=path.read_bytes() + if sha256(raw).hexdigest()!=want: + raise ValueError(f"changed dependency: {path.name}") + return json.loads(decompress(raw) if compressed else raw) + + +@cache +def scalar(x): + return Q(x) + + +def axpy(dst,src,c): + for k,a in src.items(): + value=dst.get(k,0)+c*a + if value: + dst[k]=value + else: + dst.pop(k,None) + + +def reduce_row(row,basis,weights,multiplier): + for k,(v,w) in sorted(basis.items()): + a=row.get(k,0) + if a: + axpy(row,v,-a) + axpy(weights,w,multiplier*a) + + +def solve(target,bank,deadline): + basis={} + for role,vector in sorted(bank.items()): + if monotonic()>=deadline: + return None + r=vector.copy() + w={role:Q(1)} + reduce_row(r,basis,w,-1) + if r: + k=min(r) + d=r[k] + basis[k]=({i:a/d for i,a in r.items()},{i:a/d for i,a in w.items()}) + residual=target.copy() + weights={} + reduce_row(residual,basis,weights,1) + rebuilt={} + for role,a in weights.items(): + axpy(rebuilt,bank[role],a) + axpy(rebuilt,residual,Q(1)) + assert rebuilt==target + return dict(rank=len(basis), residual={i:str(v) for i,v in residual.items()}, + matching_coefficients={i:str(v) for i,v in weights.items()} if not residual else None) + + +def snapshot(word,requested,targets,deadline): + public=word["public"] + active=word["initial"]+[None]*word["owned_fields"] + rows=[{i:Q(1)} for i in range(public)]+[None]*word["owned_fields"] + banks,values={},{} + stop=max(requested.keys()|targets.keys()) + for t,e in enumerate(word["program"]): + if t%64==0 and monotonic()>=deadline: + break + for chart,r in requested.get(t,()): + banks[t,chart,r]={i:rows[i].copy() for i in range(len(active)) if i!=r and active[i]==chart and rows[i]} + for s in targets.get(t,()): + assert active[s] is not None + values[t,s]=rows[s].copy() + if t==stop: + break + op,r,*args=e + if op=="MOVE": + assert active[r]==args[0] and args[2]==(r>=public) + active[r]=args[1] + elif op=="INIT": + assert active[r] is None and rows[r] is None and r>=public + active[r]=args[0] + rows[r]={} + elif op=="CLEAR": + assert active[r]==args[0] and rows[r] is not None and r>=public + active[r]=rows[r]=None + elif op=="SCALE": + assert active[r]==args[1] and scalar(args[0]) + rows[r]={i:v*scalar(args[0]) for i,v in rows[r].items()} + else: + s,k,chart=args + assert active[r]==active[s]==chart and r!=s and op in ("ADD","COPY") + if op=="COPY": + assert r>=public and not rows[r] + axpy(rows[r],rows[s],scalar(k)) + return banks,values + + +def controls(): + d=monotonic()+1 + a,b={0:Q(1),1:Q(1)},{1:Q(2)} + assert solve({0:Q(3)}, {7:a,8:b},d)["matching_coefficients"]=={7:"3",8:"-3/2"} + assert solve({2:Q(1)}, {7:a,8:b},d)["residual"]=={2:"1"} + assert solve({0:Q(3)}, {7:{0:Q(1),2:Q(1)},8:b},d)["residual"]=={2:"-3"} + assert solve({}, {7:a},d)["matching_coefficients"]=={} + return ["two-donor span","separating coordinate","changed donor row","zero source"] + + +def main(): + root=Path(sys.argv[1]) + price=checked(root/"price/PRICE.json",PRICE) + word=checked(root/"inputs/7334-WORD.json.gz",WORD,True) + assert price["head"]==HEAD and price["word_sha256"]==WORD + moves=word["program"] + req,targets=defaultdict(set),defaultdict(set) + bykey={} + for p in price["candidates"]: + r,s=p["owner"],p["peer"] + f,g=p["move_clocks"] + a,b,c=p["chart_path"] + t,add=p["literal_ADD"] + assert add[:2]==[r,s] and moves[t]==["ADD",*add] and f=deadline or (t,s) not in values or (cut,chart,r) not in banks: + pending.append(key) + continue + bank=banks[cut,chart,r] + source=values[t,s] + result=solve(source,bank,deadline) + if result is None: + pending.append(key) + continue + output.append(dict(key=key,source=[t,s],target_chart=chart,bank_roles=sorted(bank), + source_nnz=len(source),**result, + decision="exact span survivor" if result["matching_coefficients"] is not None else "outside donor span")) + print(json.dumps(dict(head=HEAD,price_sha256=PRICE,word_sha256=WORD,status="CAPPED" if pending else "EXHAUSTED", + case_cap=33,seconds_cap=18,controls=checks,counts=Counter(x["decision"] for x in output), + decisions=output,unvisited=pending,survivors=[x["key"] for x in output if x["matching_coefficients"] is not None]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/paired_support.py b/research/p104-two-paid-subdivision-bank-bound/inputs/paired_support.py new file mode 100644 index 0000000000..46180f7b49 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/inputs/paired_support.py @@ -0,0 +1,356 @@ +"""Exact pure prefix/suffix and unit pairing for the #7334 chart-207 split.""" +from argparse import ArgumentParser +from collections import defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +WORD = '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a' +ADMISSION = 'c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13' +PROTECTED = {319,863,1355,1568} +CAP = 128 + + +class Capped(Exception): + pass + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def check_time(deadline): + if monotonic() >= deadline: + raise Capped + + +def pinned(path, digest): + raw = path.read_bytes() + need(sha256(raw).hexdigest() == digest, f'Changed input {path.name}') + return raw + + +def unique(pairs): + doc = dict(pairs) + need(len(doc) == len(pairs), 'Duplicate receipt key') + return doc + + +def read(raw): + return loads(raw,object_pairs_hook=unique) + + +@cache +def rational(value): + return Q(value) + + +def axpy(dst, src, factor): + for j,v in src.items(): + value = dst.get(j,0) + factor*v + if value: + dst[j] = value + else: + dst.pop(j,None) + + +def dot(a,b): + return sum(v*b.get(j,0) for j,v in a.items()) + + +def compose(weights, rows): + vector = {} + for role, coefficient in weights.items(): + axpy(vector,rows[role],coefficient) + return vector + + +def pure_kernel(rows, allowed, deadline): + pivots, pure = {}, [] + for role,row in rows.items(): + check_time(deadline) + exterior = {j:v for j,v in row.items() if j not in allowed} + coeff = {role:Q(1)} + while exterior: + j = min(exterior) + if j not in pivots: + lead = exterior[j] + pivots[j] = ({k:v/lead for k,v in exterior.items()}, + {k:v/lead for k,v in coeff.items()}) + break + other, op = pivots[j] + factor = -exterior[j] + axpy(exterior,other,factor) + axpy(coeff,op,factor) + else: + projection = compose(coeff,rows) + assert projection.keys() <= allowed + pure.append((coeff,projection)) + assert len(pivots)+len(pure) == len(rows) + return sorted(pivots), pure + + +def solve_bilinear(B,D,deadline): + """Find x,y with xBy=1 and xDy=0, or prove no such rational pair.""" + n = len(B) + def trial(x): + bx,dx = compose(x,B),compose(x,D) + if not bx: + return None + if not dx: + j = min(bx) + return x,{j:1/bx[j]} + pivot = min(dx) + for j in sorted(bx.keys() | dx.keys()): + value = bx.get(j,0)*dx[pivot]-bx.get(pivot,0)*dx.get(j,0) + if value: + y = {j:dx[pivot]/value} + if dx.get(j,0): + y[pivot] = -dx[j]/value + assert dot(bx,y) == 1 and dot(dx,y) == 0 + return x,y + return None + for i in range(n): + check_time(deadline) + hit = trial({i:Q(1)}) + if hit: + return hit + # Each wedge coordinate is a homogeneous quadratic in x. Basis vectors + # and pair sums determine all coefficients over Q. + for i in range(n): + check_time(deadline) + for j in range(i+1,n): + hit = trial({i:Q(1),j:Q(1)}) + if hit: + return hit + # All wedges vanish. Only xD=0 but xB!=0 can give a pair. + _, kernel = pure_kernel(dict(enumerate(D)),set(),deadline) + for x,_ in kernel: + hit = trial(x) + if hit: + return hit + return None + + +def paired(prefix,suffix,deadline): + B,D = [],[] + for a,c in prefix: + check_time(deadline) + dot_boundary = {j:v for j,(_,d) in enumerate(suffix) if (v:=dot(c,d))} + dot_difference = {j:v for j,(b,_) in enumerate(suffix) if (v:=dot(a,b)-dot_boundary.get(j,0))} + B.append(dot_boundary); D.append(dot_difference) + hit = solve_bilinear(B,D,deadline) + if hit is None: + return None + x,y = hit + a,c = (compose(x,[pair[i] for pair in prefix]) for i in (0,1)) + b,d = (compose(y,[pair[i] for pair in suffix]) for i in (0,1)) + assert dot(a,b)==dot(c,d)==1 + return dict(a=a,b=b,c=c,d=d) + + +def initial_groups(word): + n = word['public'] + main = set(word['live']) | {r+112 for r in word['live']} + main.update(word['hosted']['X2']); main.update(word['hosted']['Y2']) + cohort = {r for r in range(n) if r not in main and (word['initial'][r],word['final'][r])==(3,127)} + return cohort-PROTECTED,cohort-PROTECTED + + +def prefix_rows(word, cuts, deadline): + n = word['public']; rows = [{r:Q(1)} for r in range(n)]+[None]*word['owned_fields'] + charts = word['initial']+[None]*word['owned_fields'] + banks, seen = {}, 0 + try: + for clock,event in enumerate(word['program']): + if clock%64 == 0 or clock in cuts: + check_time(deadline) + if clock in cuts: + banks[clock] = {r:rows[r].copy() for r in range(n) if charts[r]==207} + if clock >= max(cuts): + break + op,dst,*args = event + if op == 'MOVE': + old,new,owned = args + assert charts[dst] == old and owned==(dst>=n) + charts[dst]=new + elif op == 'INIT': + assert dst>=n and rows[dst] is None + rows[dst],charts[dst]={},args[0] + elif op == 'CLEAR': + assert dst>=n and charts[dst]==args[0] + rows[dst]=charts[dst]=None + elif op == 'SCALE': + assert charts[dst]==args[1] + rows[dst]={j:rational(args[0])*v for j,v in rows[dst].items()} + else: + src,q,chart=args + assert charts[dst]==charts[src]==chart and src!=dst and op in {'ADD','COPY'} + if op=='COPY': + assert dst>=n and not rows[dst], 'Dirty COPY' + axpy(rows[dst],rows[src],rational(q)) + seen=clock+1 + except Capped: + pass + return banks,seen + + +def suffix_rows(word,banks,deadline): + n=word['public']; cols=[{r:Q(1)} for r in range(n)]+[{} for _ in range(word['owned_fields'])] + snapshots,seen={},0 + try: + for clock in range(len(word['program']),min(banks)-1,-1): + if clock%64==0 or clock in banks: + check_time(deadline) + if clock in banks: + snapshots[clock]={r:cols[r].copy() for r in banks[clock]} + if clock==min(banks): + break + op,dst,*args=word['program'][clock-1] + if op in {'ADD','COPY'}: + src,q,_=args + axpy(cols[src],cols[dst],rational(q)) + if op=='COPY': + cols[dst]={} + elif op=='SCALE': + cols[dst]={j:rational(args[0])*v for j,v in cols[dst].items()} + elif op in {'INIT','CLEAR'}: + cols[dst]={} + else: + assert op=='MOVE' + seen+=1 + except Capped: + pass + return snapshots,seen + + +def geometry_keys(geometry): + if 'representative_keys' in geometry: + raw=geometry['representative_keys'] + elif 'keys' in geometry: + raw=geometry['keys'] + else: + raw=[(row['cut'],row['chart'],pivot) for row in geometry['segments'] for pivot in row['pivots']] + result=[tuple(row) if not isinstance(row,dict) else (row['cut'],row['chart'],row['pivot']) for row in raw] + need(len(result)==len(set(result)) and all(len(row)==3 and row[1]==207 and 44588<=row[0]<=44628 for row in result),'Wrong geometry key inventory') + return result + + +def audit(word,geometry,deadline): + all_keys=geometry_keys(geometry) + if not all_keys: + return dict(status='empty_geometry',selected=0,decisions=[],unresolved=[]) + keys=all_keys[:CAP] + cohort,pivots=initial_groups(word) + if 'endpoint_cohort' in geometry: + assert sorted(cohort)==geometry['endpoint_cohort'] + overflow=[tuple(key) for key in geometry.get('unvisited_keys',())] + assert len(overflow)==len(set(overflow)) and not set(overflow).intersection(all_keys) + bank_plan=defaultdict(list) + for cut,chart,pivot in keys: + need(pivot in pivots,'Protected or non-helper pivot') + bank_plan[cut].append(pivot) + banks,forward=prefix_rows(word,bank_plan,deadline) + decisions,opens={}, {} + try: + for cut,bank in banks.items(): + need(set(bank_plan[cut])<=bank.keys(),'Pivot absent from literal chart bank') + exterior,pure=pure_kernel(bank,cohort,deadline) + if any(c for _,c in pure): + opens[cut]=(exterior,pure) + else: + decisions[cut]=dict(status='no_nonzero_pure_prefix',public_bank=list(bank), + prefix_exterior_pivots=exterior,prefix_nullity=len(pure)) + except Capped: + pass + backward=0 + if opens: + snapshots,backward=suffix_rows(word,{c:banks[c] for c in opens},deadline) + try: + for cut,bank in snapshots.items(): + exterior,pure=pure_kernel(bank,cohort,deadline) + pre_rank,pre=opens[cut] + row=dict(public_bank=list(bank),prefix_exterior_pivots=pre_rank, + suffix_exterior_pivots=exterior,prefix_nullity=len(pre),suffix_nullity=len(pure)) + if not any(d for _,d in pure): + decisions[cut]=row|dict(status='no_nonzero_pure_suffix') + continue + witness=paired(pre,pure,deadline) + if witness is None: + decisions[cut]=row|dict(status='no_unit_pairing') + continue + assert compose(witness['a'],banks[cut])==witness['c'] + assert compose(witness['b'],bank)==witness['d'] + decisions[cut]=row|dict(status='exact_support_only',witness={k:{j:str(v) for j,v in value.items()} for k,value in witness.items()}) + except Capped: + pass + rows=[dict(key=key,**decisions[key[0]]) for key in keys if key[0] in decisions] + unresolved=[key for key in all_keys if key[0] not in decisions or key not in keys] + overflow + return dict(status='CAPPED' if unresolved else 'EXHAUSTED',selected=len(keys), + eligible_cohort=sorted(cohort),prefix_events=forward,suffix_events=backward, + decisions=rows,unresolved=unresolved,support_only=[row['key'] for row in rows if row['status']=='exact_support_only']) + + +def controls(): + inf=float('inf') + _,a=pure_kernel({4:{0:Q(1),2:Q(1)},5:{2:Q(1)}},{0},inf) + _,b=pure_kernel({4:{0:Q(1)},5:{3:Q(1)}},{0},inf) + hit=paired(a,b,inf) + assert hit and hit['a'][4] == -hit['a'][5] != 0 + assert dot(hit['a'],hit['b']) == dot(hit['c'],hit['d']) == 1 + _,wrong=pure_kernel({4:{0:Q(1),3:Q(1)},5:{3:Q(1)}},{0},inf) + assert paired(a,wrong,inf) is None + assert solve_bilinear([{0:Q(1)},{1:Q(1)}],[{0:Q(1)},{1:Q(2)}],inf)[0]=={0:Q(1),1:Q(1)} + assert solve_bilinear([{0:Q(1)},{0:Q(2)}],[{0:Q(1)},{0:Q(1)}],inf) is not None + return ['signed_unit_pair','unequal_pairing_rejected','quadratic_cross_term','left_kernel_D'] + + +def main(): + p=ArgumentParser(description=__doc__) + p.add_argument('--controls-only',action='store_true') + for key in ('word','price','geometry','admission'): + p.add_argument('--'+key,type=Path) + p.add_argument('--price-sha'); p.add_argument('--geometry-sha') + a=p.parse_args() + assert __debug__ + checks=controls() + if a.controls_only: + print(dumps(dict(controls=checks),indent=2,sort_keys=True)); return + need(all((a.word,a.price,a.geometry,a.admission,a.price_sha,a.geometry_sha)),'Sealed geometry and price are required') + price=read(pinned(a.price,a.price_sha)); geom=read(pinned(a.geometry,a.geometry_sha)) + admission=read(pinned(a.admission,ADMISSION)) + assert price['head']==admission['head']==HEAD and admission['exit']==0 + assert price['productive_delta']=={'1':17,'8':17,'9':-17} and not price['paid_delta'] + assert admission['inputs']['WORD.json.gz']==WORD + if 'price_sha256' in geom: + assert geom['price_sha256']==a.price_sha + if 'word_sha256' in geom: + assert geom['word_sha256']==WORD + keys=geometry_keys(geom) + if keys: + def watchdog(*_): + raise TimeoutError('hard support watchdog') + signal(SIGALRM,watchdog) + alarm(35) + try: + deadline=monotonic()+32 + result=audit(read(decompress(pinned(a.word,WORD))),geom,deadline) + finally: + alarm(0) + else: + result=dict(status='empty_geometry',selected=0,decisions=[],unresolved=[]) + result.update(head=HEAD,word_sha256=WORD,admission_sha256=ADMISSION,price_sha256=a.price_sha, + geometry_sha256=a.geometry_sha,cap=CAP,seconds_cap=35,controls=checks, + unvisited_credit_upper=price['one_edit_optimistic_credit'][1]) + print(dumps(result,indent=2,sort_keys=True)) + + +if __name__=='__main__': + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/pricing.py b/research/p104-two-paid-subdivision-bank-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/inputs/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/p104-two-paid-subdivision-bank-bound/inputs/second_prime.py b/research/p104-two-paid-subdivision-bank-bound/inputs/second_prime.py new file mode 100644 index 0000000000..0be5407fe6 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/inputs/second_prime.py @@ -0,0 +1,339 @@ +"""Independently verify R97's 310 frozen R96 bank keys modulo 65537.""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import isqrt +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic +import sys + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "inputs/GEOMETRY.json": "c6f9f018df8b58fcdf4f44356bd59bcac6d411b7845104ff4ad372ed4a95cfbd", + "inputs/REMAINING.json": "3597499663a57702856945e91214a65e1d0f94db8643b93c0234c2bbf9291b1a", + "inputs/7334-WORD.json.gz": WORD, +} +PRIME = 65537 +CASES = 310 +SECONDS = 25 +EVENTS = 76466 + + +def unique(items): + data = dict(items) + if len(items) != len(data): + raise ValueError("duplicate JSON key") + return data + + +def authenticate(root): + raw = {} + for rel, expected in PINS.items(): + data = (root / rel).read_bytes() + if sha256(data).hexdigest() != expected: + raise ValueError(f"changed dependency: {rel}") + raw[rel] = data + return raw + + +@cache +def coefficient(value): + q = Fraction(value) + if not q or q.denominator % PRIME == 0: + raise ValueError("zero scalar or denominator divisible by modulus") + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME, q.denominator + + +def axpy(target, source, scale): + if scale: + for role, old in source.items(): + current = (target.get(role, 0) + scale * old) % PRIME + if current: + target[role] = current + else: + target.pop(role, None) + + +def scaled(vector, scale): + return {i: y for i, x in vector.items() if (y := x * scale % PRIME)} + + +def verify_minor(vectors, columns): + """Independently recompute a minor on the original projected rows.""" + matrix = [[row.get(c, 0) for c in columns] for row in vectors] + determinant = 1 + for c in range(len(matrix)): + pivot = next((r for r in range(c, len(matrix)) if matrix[r][c]), None) + if pivot is None: + return 0 + if pivot != c: + matrix[c], matrix[pivot] = matrix[pivot], matrix[c] + determinant = -determinant + diag = matrix[c][c] + determinant = determinant * diag % PRIME + inverse = pow(diag, -1, PRIME) + for r in range(c + 1, len(matrix)): + factor = matrix[r][c] * inverse % PRIME + if factor: + for k in range(c + 1, len(matrix)): + matrix[r][k] = (matrix[r][k] - factor * matrix[c][k]) % PRIME + matrix[r][c] = 0 + return determinant % PRIME + + +def classify(bank, vectors, cohort): + full_rows = [vectors[r] for r in bank] + exterior = [{i: x for i, x in row.items() if i not in cohort} for row in full_rows] + basis, kernel = [], [] + determinant = 1 + for index, vector in enumerate(exterior): + work = vector.copy() + combination = {index: 1} + for col, known, combo in basis: + factor = -work.get(col, 0) + axpy(work, known, factor) + axpy(combination, combo, factor) + if not work: + image = {} + for i, factor in combination.items(): + axpy(image, full_rows[i], factor) + assert image.keys() <= cohort + kernel.append(dict(cut={bank[i]: x for i, x in combination.items()}, endpoint=image)) + continue + col = max(work) + pivot = work[col] + determinant = determinant * pivot % PRIME + inverse = pow(pivot, -1, PRIME) + basis.append((col, scaled(work, inverse), scaled(combination, inverse))) + rank = len(basis) + assert rank + len(kernel) == len(bank) + columns = [col for col, _, _ in basis] + if kernel: + return dict(rank=rank, kernel=kernel, minor_axes=None, determinant=None) + assert columns and verify_minor(exterior, columns) == determinant != 0 + return dict(rank=rank, kernel=[], minor_axes=columns, determinant=determinant) + + +def apply(event, state, vectors, fresh, n, denominators, backward): + op, r, *args = event + current = state[r] + if op == "MOVE": + old, new, owned = args + assert owned == (r >= n) + assert current == (new if backward else old) + state[r] = old if backward else new + fresh.discard(r) + return + if op in ("INIT", "CLEAR"): + assert r >= n + c, = args + entering = (op == "CLEAR") if backward else (op == "INIT") + if entering: + assert current is None and vectors[r] is None + state[r], vectors[r] = c, {} + if not backward: + fresh.add(r) + else: + assert current == c and vectors[r] is not None + state[r] = vectors[r] = None + fresh.discard(r) + return + assert op in ("SCALE", "ADD", "COPY") and current == args[-1] and vectors[r] is not None + factor, denominator = coefficient(args[-2]) + denominators.add(denominator) + if op == "SCALE": + vectors[r] = scaled(vectors[r], factor) + else: + src = args[0] + assert src != r and state[src] == current and vectors[src] is not None + if backward: + axpy(vectors[src], vectors[r], factor) + if op == "COPY": + assert r >= n + vectors[r] = {} + elif op == "COPY": + assert r >= n and r in fresh and not vectors[r] + vectors[r] = scaled(vectors[src], factor) + else: + axpy(vectors[r], vectors[src], factor) + fresh.discard(r) + + +def controls(): + assert all(PRIME % i for i in range(2, isqrt(PRIME) + 1)) + witness = classify([0, 1], [{3: 2, 8: 1}, {3: 3, 8: 4}], set()) + assert witness["minor_axes"] == [8, 3] and witness["determinant"] == PRIME - 5 + dropped = classify([0, 1], [{0: 1, 8: 1}, {1: 1, 8: 1}], {0, 1}) + assert dropped["kernel"] == [dict(cut={0: PRIME - 1, 1: 1}, endpoint={0: PRIME - 1, 1: 1})] + tape = [("ADD", 1, 0, "-3/2", 4), ("SCALE", 0, "2", 4), ("INIT", 2, 4), + ("COPY", 2, 1, "1", 4), ("ADD", 0, 2, "5", 4), ("CLEAR", 2, 4)] + result = [] + for backward in (False, True): + state, vectors, fresh, denoms = [4, 4, None], [{0: 1}, {1: 1}, None], set(), set() + for event in reversed(tape) if backward else tape: + apply(event, state, vectors, fresh, 2, denoms, backward) + assert state == [4, 4, None] and not fresh and denoms == {1, 2} + result.append(vectors) + assert result[0] == [{0: coefficient("-11/2")[0], 1: 5}, {0: coefficient("-3/2")[0], 1: 1}, None] + assert result[1] == [{0: coefficient("-11/2")[0], 1: coefficient("-3/2")[0]}, {0: 5, 1: 1}, None] + try: + coefficient("1/65537") + except ValueError: + pass + else: + raise AssertionError("nonunit denominator admitted") + return ["prime and signed nonzero minor", "planted pure kernel", "owned COPY forward and adjoint", + "nonunit denominator rejection"] + + +def span(frame): + vectors = {0} + for v in frame: + assert v not in vectors + vectors |= {v ^ w for w in vectors} + return vectors + + +def sweep(word, keys, cohort, deadline, result, progress, backward, previous=None): + tape, n, owned = (word[k] for k in ("program", "public", "owned_fields")) + assert (len(tape), n, owned) == (EVENTS, 1501, 68) + origin, target = ("final", "initial") if backward else ("initial", "final") + state = word[origin] + [None] * owned + vectors = [{r: 1} for r in range(n)] + [None] * owned + fresh, denoms = set(), set() + request = defaultdict(list) + frames = word["frames"] + low, high = span(frames[3]), span(frames[245]) + for cut, chart in keys: + assert 0 <= cut <= EVENTS and len(frames[chart]) == 4 and low < span(frames[chart]) < high + request[cut].append(chart) + boundaries = range(EVENTS, -1, -1) if backward else range(EVENTS + 1) + progress.update(events=0, first_unvisited_cut=boundaries.start, denominator_units=[]) + for cut in boundaries: + progress["first_unvisited_cut"] = cut + if (cut % 128 == 0 or cut in request) and monotonic() >= deadline: + break + for chart in request.get(cut, []): + key = (cut, chart) + public_bank = [r for r in range(n) if state[r] == chart] + owned_bank = [r for r in range(n, n + owned) if state[r] == chart] + pivots = sorted(set(public_bank) & cohort) + assert public_bank and pivots + if cut: + event = tape[cut - 1] + assert chart in (event[2:4] if event[0] == "MOVE" else event[-1:]) + bank = dict(public=public_bank, owned=owned_bank, pivots=pivots) + if previous is not None: + assert bank == previous[key]["bank"] + result[key] = dict(bank=bank, **classify(public_bank, vectors, cohort)) + if cut == (0 if backward else EVENTS): + assert state == word[target] + [None] * owned and not fresh + assert set(result) == set(keys) + progress["first_unvisited_cut"] = None + break + apply(tape[cut - 1 if backward else cut], state, vectors, fresh, n, denoms, backward) + progress["events"] += 1 + progress["denominator_units"] = sorted(denoms) + + +def pairing(prefix, suffix): + def dot(left, right): + return sum(v * right.get(i, 0) for i, v in left.items()) % PRIME + + return [[dict(cut=dot(a["cut"], b["cut"]), endpoint=dot(a["endpoint"], b["endpoint"])) + for b in suffix["kernel"]] for a in prefix["kernel"]] + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + assert __debug__ and sys.version_info[:2] == (3, 12) + checks = controls() + if args.controls_only: + print(dumps(checks)) + return + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + start = monotonic() + signal(SIGALRM, stop) + alarm(SECONDS) + timeout = None + keys, prior, prefix, suffix = [], [], {}, {} + prefix_progress, suffix_progress = {}, {} + try: + raw = authenticate(args.root) + price, geom, remaining = [loads(raw[f"inputs/{name}.json"], object_pairs_hook=unique) + for name in ("PRICE", "GEOMETRY", "REMAINING")] + assert price["head"] == geom["head"] == remaining["head"] == HEAD and price["caller"] == CALLER + assert price["word_sha256"] == geom["word_sha256"] == WORD + assert geom["price_sha256"] == PINS["inputs/PRICE.json"] + assert remaining["input_sha256"]["lead/GEOMETRY.json"] == PINS["inputs/GEOMETRY.json"] + assert geom["status"] == "EXHAUSTED" and geom["visited_events"] == EVENTS + keys = list(map(tuple, remaining["unvisited_prefix"])) + prior = remaining["dual_drops_requiring_rational"] + assert len(keys) == len(set(keys)) == remaining["next_modular_cases"] == CASES + assert remaining["next_modular_runner_seconds"] == SECONDS + assert keys == list(map(tuple, geom["unvisited_keys"])) + selected = {tuple(row["key"]) for row in geom["selected"]} + assert len(selected) == 16 and not set(keys) & selected and set(map(tuple, prior)) <= selected + assert set(keys) | selected == set(map(tuple, geom["all_representative_keys"])) + assert prior == [[41740, 242], [45266, 242]] + payload = decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(payload).hexdigest() == PAYLOAD + word = loads(payload, object_pairs_hook=unique) + cohort = set(price["cohort"]) + assert len(cohort) == 15 and all((word["initial"][r], word["final"][r]) == (3, 245) for r in cohort) + deadline = start + SECONDS - 2 + sweep(word, keys, cohort, deadline, prefix, prefix_progress, False) + candidates = [key for key in keys if key in prefix and prefix[key]["kernel"]] + if candidates: + sweep(word, candidates, cohort, deadline, suffix, suffix_progress, True, prefix) + else: + suffix_progress.update(events=0, first_unvisited_cut=None, denominator_units=[]) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + + results = [] + for key in keys: + left, right = prefix.get(key), suffix.get(key) + pair = None + if left and not left["kernel"]: + status = "prefix_exclusion" + elif right and not right["kernel"]: + status = "suffix_exclusion" + elif right: + status = "dual_drop" + pair = pairing(left, right) + else: + status = "unvisited" + results.append(dict(key=key, status=status, prefix=left, suffix=right, modular_pairings=pair)) + complete = (timeout is None and prefix_progress.get("first_unvisited_cut", 0) is None + and suffix_progress.get("first_unvisited_cut", 0) is None) + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, modulus=PRIME, controls=checks, + cap_cases=CASES, cap_seconds=SECONDS, prefix_progress=prefix_progress, suffix_progress=suffix_progress, + timeout=timeout, complete=complete, results=results, + counts=Counter(row["status"] for row in results), previously_frozen_exact_keys=prior), + indent=2, sort_keys=True)) + if not complete: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-two-paid-subdivision-bank-bound/receipts/AGREEMENT.json b/research/p104-two-paid-subdivision-bank-bound/receipts/AGREEMENT.json new file mode 100644 index 0000000000..5e1f0091d6 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/receipts/AGREEMENT.json @@ -0,0 +1,29 @@ +{ + "cut_agreement": [ + 42958, + 42959, + 42960 + ], + "pins": { + "independent/RESULT.json": "94c051452dd777b23913f5dda60f170ae82ae8b3d989bef9ba9687acfccad1fb", + "lead/RESULT.json": "3fd4f688b25bcd213ff3bccdedbfeb4d254d125be90456f8bef686ef06fae664", + "plan/PRICE.json": "b29ff21d96485317003db5d06d3332f71e7158de4fafbbc6b300a45fc5d5e3c6" + }, + "primary_axes_det_mod_65537": 32768, + "primary_axes_matrix_mod_65537": [ + [ + 32769, + 0 + ], + [ + 0, + 65536 + ] + ], + "primary_exact_axis": [ + 0, + 890 + ], + "raw_keys_agreement": 9, + "unresolved": 0 +} diff --git a/research/p104-two-paid-subdivision-bank-bound/receipts/SHA256.json b/research/p104-two-paid-subdivision-bank-bound/receipts/SHA256.json new file mode 100644 index 0000000000..7d430555ee --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/receipts/SHA256.json @@ -0,0 +1,10 @@ +{ + "r120/AGREEMENT.json": "a85277d8bb97dbe1d4880032f3058604532de5fa5bb96b33977095b54b02d8c6", + "r120/EXACT.json": "3fd4f688b25bcd213ff3bccdedbfeb4d254d125be90456f8bef686ef06fae664", + "r120/PRICE.json": "b29ff21d96485317003db5d06d3332f71e7158de4fafbbc6b300a45fc5d5e3c6", + "r120/SECOND.json": "94c051452dd777b23913f5dda60f170ae82ae8b3d989bef9ba9687acfccad1fb", + "r99/GEOMETRY.json": "c89976cd5f808c29ab13770e262b2d216f56b4e1703ef836c3438d60f40eb11b", + "r99/MODULAR.json": "4d24d44be888a52ac93e589bf7a15978317395b0d3ddc6d96dd2e6d14bde5b44", + "r99/PRICE.json": "0eba831b917331f7a84f4d8a5da726577ed516f04c5f1b94671e031dd2c0b3b4", + "r99/SELECTION.json": "3a6f588eb597e56abfbfe568319fc81294d16d37f03f8b6159ba5b133dc2f416" +} diff --git a/research/p104-two-paid-subdivision-bank-bound/replay.py b/research/p104-two-paid-subdivision-bank-bound/replay.py new file mode 100644 index 0000000000..2b4b810e54 --- /dev/null +++ b/research/p104-two-paid-subdivision-bank-bound/replay.py @@ -0,0 +1,178 @@ +"""Reproduce the 17 frozen same-span banks for two paid rank-two subdivisions.""" +from argparse import ArgumentParser +from fractions import Fraction +from gzip import decompress +from hashlib import sha1, sha256 +from json import loads +from pathlib import Path, PurePosixPath +from shutil import copyfile +from subprocess import run +import sys +from tempfile import TemporaryDirectory + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +SHARED = ("7334-WORD.json.gz", "BENCHMARK.json", "pricing.py", "second_prime.py") + + +def unique(items): + result = dict(items) + if len(result) != len(items): + raise ValueError("duplicate JSON key") + return result + + +def decode(raw): + return loads(raw, object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def relative(name): + path = PurePosixPath(name) + if path.is_absolute() or path.as_posix() != name or ".." in path.parts: + raise ValueError(f"invalid relative path: {name}") + return path + + +def authenticate(): + pins = decode((ROOT / "LOCAL-PINS.json").read_bytes()) + for name, expected in pins.items(): + if digest((ROOT / relative(name)).read_bytes()) != expected: + raise ValueError(f"changed package dependency: {name}") + provenance = decode((ROOT / "PROVENANCE.json").read_bytes()) + for name, record in provenance["files"].items(): + raw = (ROOT / relative(name)).read_bytes() + assert digest(raw) == record["sha256"] == pins[name] + assert sha1(f"blob {len(raw)}\0".encode() + raw).hexdigest() == record["git_blob"] + published = decode((ROOT / "inputs/PR7362-SHA256.json").read_bytes()) + inputs = {} + for name in ("R92-GEOMETRY.json", "R92-PRICE.json"): + raw = decompress((ROOT / "inputs" / (name + ".gz")).read_bytes()) + assert digest(raw) == published[name] + inputs[name] = raw + readback = decode((ROOT / "inputs/READBACK.json").read_bytes()) + price = decode(inputs["R92-PRICE.json"]) + bench = decode((ROOT / "inputs/BENCHMARK.json").read_bytes()) + assert readback["head"] == price["head"] == bench["head"] == HEAD + assert readback["caller_head"] == price["caller_head"] == CALLER + assert readback["copies"] == 17 and readback["empty_root_credits"] == 0 + assert (readback["paid_positions"], readback["productive_fields"], readback["rank_surplus"]) == (110519, 22461, 1424) + assert readback["paid"] == price["old_paid"] and readback["targets"] == price["old_targets"] + assert bench["receipt_sha256"]["peer-price/READBACK.json"] == pins["inputs/READBACK.json"] + return inputs + + +def command(root, script, *, timeout=25, check=True): + result = run([sys.executable, "-I", "-B", str(root / script)], + capture_output=True, timeout=timeout) + if check and result.returncode: + sys.stderr.write(result.stderr.decode(errors="replace")) + result.check_returncode() + return result + + +def seed(root, stage, scripts, shared, extra, inputs): + for folder in ("inputs", *sorted({Path(name).parent.as_posix() for name in scripts})): + (root / folder).mkdir(parents=True, exist_ok=True) + for name in (*shared, *extra): + copyfile(ROOT / "inputs" / name, root / "inputs" / name) + for path in scripts: + copyfile(ROOT / "engines" / stage / Path(path).name, root / path) + for name, raw in inputs.items(): + (root / "inputs" / name).write_bytes(raw) + + +def reject(root, path, script): + victim = root / path + raw = victim.read_bytes() + victim.write_bytes(raw + b"\n") + result = command(root, script, check=False) + assert result.returncode == 1 and not result.stdout + assert b"changed dependency" in result.stderr and victim.name.encode() in result.stderr + victim.write_bytes(raw) + + +def replay(root, out): + prior_inputs = authenticate() + expected = decode((ROOT / "receipts/SHA256.json").read_bytes()) + receipts = {} + + def record(stage, name, run_root, script, target=None): + key = f"{stage}/{name}.json" + raw = command(run_root, script).stdout + assert digest(raw) == expected[key], ("changed receipt", key) + receipts[key] = raw + if target is not None: + (run_root / target).write_bytes(raw) + return decode(raw) + + first = root / "r99" + seed(first, "r99", ("lead/quote.py", "lead/geometry.py", "lead/select.py", "lead/modular.py"), + SHARED, (), prior_inputs) + record("r99", "PRICE", first, "lead/quote.py", "lead/PRICE.json") + geometry = record("r99", "GEOMETRY", first, "lead/geometry.py", "lead/GEOMETRY.json") + selection = record("r99", "SELECTION", first, "lead/select.py", "lead/SELECTION.json") + original = record("r99", "MODULAR", first, "lead/modular.py", "lead/MODULAR.json") + assert geometry["stage"] == "complete" and geometry["timeout"] is None + assert (geometry["visited_placements"], geometry["pair_comparisons"], geometry["visited_cuts"]) == (285, 108, 38967) + assert len(geometry["representatives"]) == 102 and not geometry["owned_rejections"] + assert len(selection["selected"]) == 16 and len(selection["unselected"]) == 1 + assert original["counts"] == {"prefix exclusion": 16} and original["prime"] == 65537 + assert all(row["prefix"]["rank"] == 2 and row["suffix"] is None for row in original["results"]) + assert original["unvisited"] == selection["unselected"] + reject(first, "inputs/R92-PRICE.json", "lead/modular.py") + + second = root / "r120" + inputs = {"R92-PRICE.json": prior_inputs["R92-PRICE.json"]} + inputs.update({f"R99-{name}.json": receipts[f"r99/{name}.json"] + for name in ("PRICE", "GEOMETRY", "SELECTION", "MODULAR")}) + seed(second, "r120", ("plan/freeze.py", "lead/check.py", "independent/prefix.py", "independent/compare.py"), + SHARED, ("donor_span.py", "paired_support.py"), inputs) + price = record("r120", "PRICE", second, "plan/freeze.py", "plan/PRICE.json") + exact = record("r120", "EXACT", second, "lead/check.py", "lead/RESULT.json") + other = record("r120", "SECOND", second, "independent/prefix.py", "independent/RESULT.json") + agreement = record("r120", "AGREEMENT", second, "independent/compare.py") + assert receipts["r120/AGREEMENT.json"] == (ROOT / "receipts/AGREEMENT.json").read_bytes() + assert price["head"] == exact["head"] == other["head"] == HEAD + assert price["caller"] == exact["caller"] == other["caller"] == CALLER + assert price["row"] == selection["unselected"][0] + assert price["paid_delta"] == {"1": 68, "2": -34} and price["productive_delta"] == {"4": 17, "5": 17, "9": -17} + assert (price["paid"], price["productive"], price["rank_surplus"]) == (110553, 22478, 1424) + assert Fraction(price["probe_complete_margin"][0]) > 0 > Fraction(price["extra_rank_one_upper"]) + assert Fraction(price["fixed_target_complete_upper"]) < 0 + assert exact["status"] == "prefix exclusion" and exact["proof"]["axes"] == [0, 890] + assert exact["proof"]["determinant"] == "-1/2" + assert len(exact["raw_keys"]) == len(other["raw_excluded"]) == agreement["raw_keys_agreement"] == 9 + assert len(exact["representative_keys"]) == 6 + assert not exact["unresolved"] and not other["unresolved"] and agreement["unresolved"] == 0 + assert other["progress"] == {"events": 76466, "first_unvisited_cut": None} + assert all(row["rank"] == 2 for row in other["rows"]) + assert agreement["primary_axes_det_mod_65537"] == 32768 + (second / "inputs/7334-WORD.json.gz").unlink() + reject(second, "plan/PRICE.json", "independent/prefix.py") + + assert set(receipts) == set(expected) + if out is not None: + out.mkdir(parents=True) + for name, raw in receipts.items(): + path = out / relative(name) + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(raw) + print("PASS_TWO_PAID_SUBDIVISION_BANK_BOUND forms=17 previous=16 residual=1 raw_residual=9 unresolved=0") + + +def main(): + assert __debug__ and sys.version_info[:2] == (3, 12) + parser = ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="new directory for all eight regenerated receipts") + args = parser.parse_args() + with TemporaryDirectory() as tmp: + replay(Path(tmp), args.out) + + +if __name__ == "__main__": + main()