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-original-source-retime-late-donor-bound/LOCAL-PINS.json b/research/p104-original-source-retime-late-donor-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..0ffba3f57b --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/LOCAL-PINS.json @@ -0,0 +1,24 @@ +{ + "NOTICE": "644c59956808c910d1f17ca4a737d987dcaea2a366c2898625fceb7e3d2cfe36", + "PROOF.md": "e4eb1017a6bc516e99488d353d8684673afb379b64aafc5c4313e06fcebd1109", + "PROVENANCE.json": "d64fd437764cb8f55fd2a8e548f7e6712627f7836a1c39cf89165af737832e82", + "README.md": "7b3a204626b7751ac7971033f904f7d51e89a78f887a7deefe9791a9e8a6678f", + "SOURCES.json": "5ae4cfc96aa890b1b06aa0de688e03d9713b2772fb0f9c6ae7e23ad7d49c479d", + "TASK.json": "58c5adb9c0cc386edf31223390818212062ffdcdcacf74bc79b43a7c6ad6ce64", + "VERIFICATION.md": "0488feb8d67221b21084737537b4fd86e53dff730f94b2332568c4f866d075f8", + "VERIFY.json": "e595fe4d9320aa1671a9c03008a53ec8b625086bd09c0035f550a0738d523715", + "engines/r103/quote.py": "29e2991277da26de6704bcd77363daf31772b027e8522368616f5526312597bc", + "engines/r103/retime.py": "75d01989e97de54060d390cf7f7819dd9c28364ed9c336a06926b9a373200081", + "engines/r103/reverse_retime.py": "94417d906dac5890e1e47f3cb097bd9bcd7a0622f6b5bbb0ade69874b13e9fb2", + "engines/r104/reverse_late.py": "696046c7d5a55f643233a9b02fa4c995697a0b5c220c8269ccf3425cef6099e6", + "engines/r104/reverse_span.py": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", + "engines/r104/support.py": "716c69c926e1911b59541476d7bc7fa06f869afa59c09bc52955d561f7c16fd1", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/PR7365-SHA256.json": "f8418b2b07e4ecb6d49d8839015e9ceab2224816d7863edd59cb03f29de34566", + "inputs/R101-PRICE.json": "ac5ecb17f0e9f3c068423998b350a78c1a4769b6f61b50838be5f3e0d0b1a00c", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "receipts/SEPARATORS.json": "ad6f48ea8488d6efb8546a5074fdffaad920728f70d80ab95a9953b81fed4fbd", + "receipts/SHA256.json": "0a7c53857f40dc27e5e89579a1bdcc7c78fb5e8c8f276f805e639a198b1f18e4", + "replay.py": "d36168354681164d942a0d81f435b38d79d574099496c6591a72cd728d3fab30" +} diff --git a/research/p104-original-source-retime-late-donor-bound/NOTICE b/research/p104-original-source-retime-late-donor-bound/NOTICE new file mode 100644 index 0000000000..f54b426107 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. + +#7334 and #7113 supply the word and signed caller. #7365 supplies the frozen +predecessor windows and price. #7003 and #7336 supply earlier public retiming +and fusion evidence. #7355 supplies the donor-span engines. OpenAI Codex and +subagents materially assisted proof, implementation, replay and packaging. diff --git a/research/p104-original-source-retime-late-donor-bound/PROOF.md b/research/p104-original-source-retime-late-donor-bound/PROOF.md new file mode 100644 index 0000000000..54e4ea395c --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/PROOF.md @@ -0,0 +1,13 @@ +# Exact scope and price + +Each original destination d has a paid ascending chart sequence A→B→C. Its sole contact between the two MOVE clocks is a nonzero ADD with d as destination and public source s. The five pairs come from #7365. A sixth predecessor pair has owned source 1555 and is outside this scope. Both source and destination operands of every ADD and COPY count in the sole-contact test. + +The proposed direct MOVE A→C can occupy the old exit clock if the ADD uses A or the old entrance clock if it uses C. For original-source retiming, a pre-event cut is the state after exactly that many original events. Each typed cut specifies which of A or C is required. The range begins just after the first MOVE and ends immediately before the second MOVE. The old ADD clock is excluded for both types. The independent reverse chronology checks source charts and writes, then compares each source-chart interval, guard and disposition with the primary receipt. Of 9,432 cuts in each orientation, none has the original source on the required endpoint chart. Every one of the 18,864 fails the chart condition before its unchanged-source row condition matters. + +For alternate donors, only the old second MOVE pre-event cut is tested on A and C. The donor rows use all arbitrary initial public coordinates, and ownership or other paths stay fixed. No other operation reads d in the window, so deleting the old ADD and moving d's chart before this cut cannot affect any replacement donor row. If u denotes the original source row just before the old ADD and α≠0 is its coefficient, exact replacement by public donor rows dⱼ requires the sum of βⱼdⱼ to equal αu. + +Every listed test vector evaluates to zero on each donor and nonzero on αu. The only two-coordinate vector belongs to key [40102,44609,205,"exit"] at chart 207. Set public coordinates 58 and 1493 to 1 and −1/2, with all others zero. The original source row has coefficients (1,0) at these coordinates. Donor 198 has (1/2,1), and the other seven public donors have (0,0). The original ADD scalar is −1/2. The test is zero on every donor and −1/2 on the original response. Owned role 1567 is recorded outside the bank. The other nine cases use one coordinate each. The compact witness and all exact rows are checked against the independent replay. + +The existing complete signed bill across 17 copies has 110,519 paid positions and 22,461 productive positions, with rank surplus 1,424. A hypothetical rank-sum contraction removes 17 paid positions, keeping all productive positions and rank mass. The 0.277267940905222 one-edit and 0.774080773065573 compatible whole optimistic upper bounds grant auxiliary work free. Two windows on role 532 share a MOVE and cannot both receive credit. A new paid rank-one defeats any single edit. A construction would still need exact signed transport, ownership and restoration, compiler, ordinary work, precision and tape. + +The independently admitted #7334 all-size comparison retains native all-columns correctness, owned erasure, compiler, precision/tape and analytic recovery premises. The package checks the scoped necessary conditions and reuses the unchanged comparator evidence. diff --git a/research/p104-original-source-retime-late-donor-bound/PROVENANCE.json b/research/p104-original-source-retime-late-donor-bound/PROVENANCE.json new file mode 100644 index 0000000000..60404f5189 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/PROVENANCE.json @@ -0,0 +1,48 @@ +{ + "derived_inputs": { + "inputs/R101-PRICE.json": { + "key": "r101/lead/PRICE.json", + "receipt": "inputs/PR7365-SHA256.json" + } + }, + "files": { + "engines/r104/reverse_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "5efbeac87e3963085149244304614844307c8034", + "path": "research/p104-owned-add-source-span-bound/engines/reverse.py", + "sha256": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/reverse.py" + }, + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "inputs/PR7365-SHA256.json": { + "commit": "98be9db1f28cdc5fa8962c7da065bc0174db9744", + "git_blob": "2c2e083626e3e3227dcc8cb2864e61222b273d3f", + "path": "research/p104-changed-public-move-contraction-bound/receipts/SHA256.json", + "sha256": "f8418b2b07e4ecb6d49d8839015e9ceab2224816d7863edd59cb03f29de34566", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/98be9db1f28cdc5fa8962c7da065bc0174db9744/research/p104-changed-public-move-contraction-bound/receipts/SHA256.json" + }, + "inputs/donor_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "46e4621b69bba513f327de53153298e7f4ca0645", + "path": "research/p104-owned-add-source-span-bound/engines/forward.py", + "sha256": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/forward.py" + } + }, + "schema_version": 1 +} diff --git a/research/p104-original-source-retime-late-donor-bound/README.md b/research/p104-original-source-retime-late-donor-bound/README.md new file mode 100644 index 0000000000..a495b52560 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/README.md @@ -0,0 +1,27 @@ +# Original-source retiming and late public donor bound + +**NO VERIFIED GAIN.** Δκ = 0, exactly 0% relative to conditional κ = 0.00364665195644 on exact [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) `aaeec8c0acf01e99a5f331ef363a698d9c084ace` and signed [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) `07a76c5e2738882c0cb322278e56f6cae3c9885d`. + +The five frozen consecutive paid MOVE windows each have one ADD into the moving public role with a public original source. Two independent chronology walks exclude **18,864** typed pre-event cuts for retiming the ADD while keeping its original source and coefficient. At every alternative cut the original source occupies a different chart from the required endpoint chart. + +The second screen allows arbitrary rational replacement donors from either endpoint chart immediately before the old second MOVE. The target remains the original source functional immediately before its old ADD. Both exact engines exclude all **ten** late donor banks. Nine have a missing coordinate and one has a two-coordinate separating covector. The [exact separators](receipts/SEPARATORS.json) include the respective bank and source cut. The existing owned occupant in the latter bank stays outside the public donor span. + +The prospective contraction would remove 17 paid positions and preserve all productive positions. The directed one-edit upper is about 0.277267940905222 raw, and the four-role compatible whole upper is about 0.774080773065573 raw before ancillary costs. Exact support leaves zero verified savings. [Proof and price](PROOF.md) + +## Reproduce + +Use CPython 3.12 with assertions and the standard library. From this package in a clean checkout or Git-free export: + +```sh +python3.12 -I -B replay.py +``` + +Use `--output replayed` to retain six [pinned regenerated receipts](receipts/SHA256.json), including exact interval lists, sparse rows, covectors and per-case agreement. [Pinned provenance](PROVENANCE.json) · [Verification](VERIFICATION.md) + +## Open next questions + +Freeze a bounded set of earlier alternate-donor cuts other than the original ADD clock, which #7365 already covers. Keep the five frozen windows, determine the compatible full cost first, and test each selected bank against the original source functional. A rational span survivor still needs signed cochart transport, ownership and restoration, complete compiler, precision and tape checks and independent outer replay. Other windows, owned donors, changed donor paths and multiple binary contacts lie outside the two tested scopes. + +## 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 word and signed caller. [#7365](https://github.com/CrocSwap/integer-mult-bounds/pull/7365) at `98be9db1f28cdc5fa8962c7da065bc0174db9744` supplies the frozen predecessor windows, full directed price and original-clock public donor exclusions. [#7003](https://github.com/CrocSwap/integer-mult-bounds/pull/7003) supplies a changed-clock coframe retiming precedent. [#7336](https://github.com/CrocSwap/integer-mult-bounds/pull/7336) treats a different public fusion route. [#7355](https://github.com/CrocSwap/integer-mult-bounds/pull/7355) supplies the independent donor-span engines developed for owned destinations. OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-original-source-retime-late-donor-bound/SOURCES.json b/research/p104-original-source-retime-late-donor-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-original-source-retime-late-donor-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-original-source-retime-late-donor-bound/TASK.json b/research/p104-original-source-retime-late-donor-bound/TASK.json new file mode 100644 index 0000000000..03982b0e91 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334 original-public-source sole-ADD retiming across 18,864 typed cuts and 10 late endpoint public donor banks on five frozen paid MOVE windows.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 public ADD retiming research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "One direct rank-sum paid MOVE has positive directed price if the original sole-ADD response can be preserved at a legal endpoint cut.", + "budget_minutes": 20, + "evidence": "Two exact chronology engines exclude all 18,864 typed cuts. Two independent rational engines exclude all ten late alternate-donor banks, with nine unit-coordinate separators and one two-coordinate separator.", + "open_questions": [ + { + "blocked_by": "Original-source chart barriers and the late donor separators do not decide earlier alternate donor rows. Owned donors and changed itineraries require a separate cost and interface proof.", + "first_step": "Freeze a capped set of earlier alternate public-donor cuts from the exact five windows and reprice the whole compatible stock before checking exact spans.", + "question": "Does an earlier alternate-donor cut admit the exact original source row?", + "why_it_matters": "One full charged paid MOVE contraction may improve the complex bound." + } + ], + "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": "Extends #7365 original-clock public donor exclusions to original-source retiming throughout the frozen windows and alternate public donors at the final cut.", + "scope_status": "changed", + "stop_rule": "Check 76,466 events, five windows and 18,864 original-source typed cuts within 20 seconds; check ten late public donor banks within 20 seconds. A native prototype requires exact support.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-original-source-retime-late-donor-bound/VERIFICATION.md b/research/p104-original-source-retime-late-donor-bound/VERIFICATION.md new file mode 100644 index 0000000000..65a9d093b9 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/VERIFICATION.md @@ -0,0 +1,7 @@ +# Verification + +The package rebuilds six SHA-256-pinned receipts on CPython 3.12. The original and independent chronology engines check the same 76,466 literal events, five windows and 18,864 typed cuts. The original late rational test and independent reverse covector test check all ten banks under 20-second caps, agree on exact donor rank and membership, and authenticate 132 independent sparse rows. The wrapper directly re-evaluates every separating covector on the source and all its donors, including the original ADD coefficient. + +The independent chronology original and relocated runs took 0.07 and 0.11 seconds. The independent late-bank direct and relocated runs each took 0.18 seconds. Corrupted price and word inputs are rejected. Toy controls exercise pre-event boundaries, source writes, signed donor combinations, COPY and a nontrivial separator. The primary late-bank replay retains full elimination for each case as an exact control. + +The exact admitted comparator and [hosted replay](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43114736518) are unchanged predecessor evidence. No changed supplier or complete candidate replay was needed because both scoped gates exhausted without a candidate. diff --git a/research/p104-original-source-retime-late-donor-bound/VERIFY.json b/research/p104-original-source-retime-late-donor-bound/VERIFY.json new file mode 100644 index 0000000000..c227076ea7 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Regenerate six pinned receipts, both exact chronology and late donor checks, all ten separating covectors and mutated input rejection.", + "timeout_seconds": 120 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-original-source-retime-late-donor-bound/engines/r103/quote.py b/research/p104-original-source-retime-late-donor-bound/engines/r103/quote.py new file mode 100644 index 0000000000..bd6bf85845 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/engines/r103/quote.py @@ -0,0 +1,42 @@ +"""Freeze original-public-source retiming stock before word decode.""" +from collections import defaultdict +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +PIN = "ac5ecb17f0e9f3c068423998b350a78c1a4769b6f61b50838be5f3e0d0b1a00c" + + +def main(): + raw = (ROOT/"inputs/R101-PRICE.json").read_bytes() + assert sha256(raw).hexdigest()==PIN + parent = json.loads(raw) + rows = [r for r in parent["candidates"] if r["add"][1][2]<1501] + assert len(rows)==5 and len(parent["candidates"])==6 + stock = defaultdict(list) + for row in rows: + stock[row["key"][2]].append(row) + assert len(stock)==4 + for group in stock.values(): + if len(group)>1: + assert len(group)==2 and set(group[0]["key"][:2])&set(group[1]["key"][:2]) + cuts = sum(2*(r["key"][1]-r["key"][0]-1) for r in rows) + assert cuts==18864 + one = max(Q(r["quote"]["net"][1]) for r in rows) + total = sum(max(Q(r["quote"]["net"][1]) for r in group) for group in stock.values()) + assert all(Q(r["quote"]["extra_rank_one_upper"])<0 for r in rows) + out={"head":parent["head"],"caller_head":parent["caller_head"],"kappa":parent["kappa"], + "word_sha256":parent["word_sha256"],"payload_sha256":parent["payload_sha256"], + "parent_price_sha256":PIN,"candidates":rows,"whole_net_upper":str(total), + "one_net_upper":str(one),"complete_target_upper":parent["whole_target_margin_upper"], + "full_paid_after_one":parent["one_new_paid"],"productive":parent["targets"], + "limits":{"events":76466,"pair_windows":5,"typed_cuts":cuts,"runner_seconds":20, + "prototype_cases":1,"prototype_seconds":120}} + print(json.dumps(out,indent=2,sort_keys=True)) + + +if __name__=="__main__": + assert __debug__ + main() diff --git a/research/p104-original-source-retime-late-donor-bound/engines/r103/retime.py b/research/p104-original-source-retime-late-donor-bound/engines/r103/retime.py new file mode 100644 index 0000000000..7ca40b2a6e --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/engines/r103/retime.py @@ -0,0 +1,123 @@ +"""Classify original-source retimings on five pinned public MOVE pairs.""" +from bisect import bisect_left +from collections import Counter, defaultdict +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "lead/PRICE.json":"8fbd560cf7708b99609614a0b96d02b55efc55304225ddffa5dd223ed49d4073", + "inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} + + +def read(path): + raw=(ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def chart_at(clocks,frames,initial,cut): + i=bisect_left(clocks,cut) + return frames[i-1] if i else initial + + +def stable_window(writes,old,size): + i=bisect_left(writes,old) + assert i==len(writes) or writes[i]!=old + return (writes[i-1]+1 if i else 0,writes[i] if i=deadline: + raise TimeoutError("incident index cap") + op,d,*args=event + if d in sources: + (moves if op=="MOVE" else writes)[d].append((t,event)) + used=(d,args[0]) if op in ("ADD","COPY") else (d,) + for r in used: + if r in movers: + contacts[r].append((t,event)) + next_event=None + for row in price["candidates"]: + f,g,d=row["key"] + a,b,c=row["charts"] + old,add=row["add"] + s=add[2] + assert 0<=s=lim["typed_cuts"] or monotonic()>=deadline: + raise TimeoutError("typed cut cap") + actual=chart_at(clocks,frames,initial,cut) + status=("different chart" if actual!=chart else "source write" if not lo<=cut<=hi else "exact unchanged source") + item["counts"][status]+=1 + counts[status]+=1 + if intervals and intervals[-1][1]+1==cut and intervals[-1][2:]==[status,actual]: + intervals[-1][1]=cut + else: + intervals.append([cut,cut,status,actual]) + assert len(rows)==lim["pair_windows"] and sum(counts.values())==lim["typed_cuts"] + next_cut=None + except TimeoutError as exc: + reason=str(exc) + finally: + alarm(0) + result={"head":price["head"],"pins":PINS,"limits":lim,"rows":rows,"counts":counts, + "controls":["pre-event source chart","post-MOVE source chart","source-write boundaries"], + "first_unvisited_event":next_event,"first_unvisited_cut":next_cut,"timeout":reason} + print(json.dumps(result,indent=2,sort_keys=True)) + if reason: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-original-source-retime-late-donor-bound/engines/r103/reverse_retime.py b/research/p104-original-source-retime-late-donor-bound/engines/r103/reverse_retime.py new file mode 100644 index 0000000000..c62871ac7c --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/engines/r103/reverse_retime.py @@ -0,0 +1,250 @@ +"""Reconstruct the five frozen source windows by reverse literal occupancy.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +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 +import sys + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "8fbd560cf7708b99609614a0b96d02b55efc55304225ddffa5dd223ed49d4073", + "inputs/R101-PRICE.json": "ac5ecb17f0e9f3c068423998b350a78c1a4769b6f61b50838be5f3e0d0b1a00c", + "inputs/7334-WORD.json.gz": WORD, + "inputs/RETIMING.json": "331d26d99d45d24796253cd0bf86fdbd8b755ba164ca7765edc8304cc3365f6f", +} +EVENTS, WINDOWS, CUTS, SECONDS = 76466, 5, 18864, 20 + + +def unique(items): + data = dict(items) + if len(data) != len(items): + raise ValueError("duplicate JSON key") + return data + + +def read(root, name): + raw = (root / name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError(f"changed dependency: {name}") + return raw + + +def backwards(word, sources, destinations, deadline, progress): + tape = word["program"] + n, owned = word["public"], word["owned_fields"] + assert (n, owned) == (1501, 68) and len(tape) == EVENTS + active = word["final"] + [None] * owned + source_chart_intervals = defaultdict(list) + source_moves, source_writes, dest_incidents = (defaultdict(list) for _ in range(3)) + upper = dict.fromkeys(sources, len(tape)) + for t in range(len(tape) - 1, -1, -1): + progress["first_unvisited_event"] = t + if t % 128 == 0 and monotonic() >= deadline: + raise TimeoutError("reverse incidence time cap") + op, d, *args = e = tape[t] + current = active[d] + operands = [d] + if op == "MOVE": + old, new, flag = args + assert current == new and flag == (d >= n) + if d in sources: + source_chart_intervals[d].append((t + 1, upper[d], new)) + source_moves[d].append((t, e)) + upper[d] = t + active[d] = old + elif op == "CLEAR": + assert d >= n and current is None + active[d] = args[0] + elif op == "INIT": + assert d >= n and current == args[0] + active[d] = None + else: + assert op in ("ADD", "COPY", "SCALE") and current == args[-1] + if op in ("ADD", "COPY"): + assert args[0] != d and active[args[0]] == current + assert op != "COPY" or d >= n + operands.append(args[0]) + if d in sources: + source_writes[d].append((t, e)) + for r in operands: + if r in destinations: + dest_incidents[r].append((t, e)) + progress["events_replayed"] += 1 + assert active == word["initial"] + [None] * owned + progress["first_unvisited_event"] = None + for r in sources: + source_chart_intervals[r].append((0, upper[r], active[r])) + source_chart_intervals[r].reverse() + assert all(x[1] + 1 == y[0] for x, y in zip(source_chart_intervals[r], source_chart_intervals[r][1:])) + source_moves[r].reverse() + source_writes[r].reverse() + for r in destinations: + dest_incidents[r].reverse() + return source_chart_intervals, source_moves, source_writes, dest_incidents + + +def split(lo, hi, old): + return [(a, b) for a, b in ((lo, min(hi, old - 1)), (max(lo, old + 1), hi)) if a <= b] + + +def row_stability(writes, old, end): + earlier = next((r for r in reversed(writes) if r[0] < old), None) + later = next((r for r in writes if r[0] > old), None) + assert not any(t == old for t, _ in writes) + return (0 if earlier is None else earlier[0] + 1, end if later is None else later[0]), earlier, later + + +def typed_intervals(chart_spans, left, right, old, expected, stable): + result = [] + for a, b, chart in chart_spans: + for lo, hi in split(max(a, left), min(b, right), old): + ranges = [(lo, hi, "different chart", chart)] + if chart == expected: + s, t = stable + ranges = [(lo, min(hi, s - 1), "source write", chart), + (max(lo, s), min(hi, t), "exact unchanged source", chart), + (max(lo, t + 1), hi, "source write", chart)] + for first, last, status, actual in ranges: + if first > last: + continue + if result and result[-1][1] + 1 == first and result[-1][2:] == [status, actual]: + result[-1][1] = last + else: + result.append([first, last, status, actual]) + return result + + +def controls(): + assert split(1, 6, 4) == [(1, 3), (5, 6)] and split(4, 4, 4) == [] + stable, before, after = row_stability([(2, "WRITE1"), (6, "WRITE2")], 4, 8) + assert (stable, before, after) == ((3, 6), (2, "WRITE1"), (6, "WRITE2")) + actual = typed_intervals([(0, 3, 5), (4, 8, 7)], 1, 7, 4, 7, stable) + assert actual == [[1, 3, "different chart", 5], [5, 6, "exact unchanged source", 7], [7, 7, "source write", 7]] + return ["remove only old pre-event cut", "source write exact endpoints", + "signed chart and source-write distinction", "chart applies after its MOVE event"] + + +def candidate_results(word, price, candidates, histories, deadline, progress, result): + spans, moves, writes, incidents = histories + for row in candidates: + f, g, dst = row["key"] + a, b, c = row["charts"] + old, add = row["add"] + src = add[2] + assert f < old < g and dst == add[1] and 0 <= src < word["public"] and src != dst + contacts = incidents[dst] + expected = [(f, ["MOVE",dst,a,b,False]), (old,add), (g,["MOVE",dst,b,c,False])] + assert [r for r in contacts if f <= r[0] <= g] == expected + dst_before = next((r for r in reversed(contacts) if r[0] < f), None) + dst_after = next((r for r in contacts if r[0] > g), None) + assert len([1 for l,u,h in spans[src] if l <= old <= u and h == b]) == 1 + stable, prev_write, next_write = row_stability(writes[src], old, EVENTS) + item = dict(move_pair=row["key"], original_add=row["add"], source=src, + original_charts=row["charts"], unchanged_row_window=stable, + source_moves=[r for r in moves[src] if f <= r[0] <= g], + source_writes=[r for r in writes[src] if f <= r[0] <= g], + previous_source_write=prev_write, next_source_write=next_write, + destination_contacts=expected, previous_destination_contact=dst_before, + next_destination_contact=dst_after, cuts=[], counts=Counter()) + result.append(item) + for side, target in (("entrance", a), ("exit", c)): + progress["first_unvisited_typed_window"] = [f, g, dst, side] + if monotonic() >= deadline: + raise TimeoutError("typed window time cap") + ranges = typed_intervals(spans[src], f + 1, g, old, target, stable) + tested = sum(hi - lo + 1 for lo, hi, _, _ in ranges) + assert tested == g - f - 1 + if progress["typed_cuts_replayed"] + tested > price["limits"]["typed_cuts"]: + raise TimeoutError("typed cut count cap") + progress["typed_cuts_replayed"] += tested + for lo, hi, status, _ in ranges: + item["counts"][status] += hi - lo + 1 + item["cuts"].append(dict(side=side, chart=target, intervals=ranges)) + progress["first_unvisited_typed_window"] = None + + +def compare(result, primary): + assert primary["head"] == HEAD and primary["timeout"] is None + assert primary["first_unvisited_cut"] is None and primary["first_unvisited_event"] is None + assert len(result) == len(primary["rows"]) == WINDOWS + for a, b in zip(result, primary["rows"], strict=True): + for k in ("move_pair", "original_add", "source", "unchanged_row_window", "source_moves", "source_writes", "cuts", "counts"): + assert dumps(a[k], sort_keys=True) == dumps(b[k], sort_keys=True), (a["move_pair"], k) + counts = Counter() + for row in result: + counts.update(row["counts"]) + assert counts == primary["counts"] and sum(counts.values()) == CUTS + return counts + + +def main(): + p = ArgumentParser(description=__doc__) + p.add_argument("--root", type=Path, default=ROOT) + p.add_argument("--controls-only", action="store_true") + args = p.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 20-second cap") + + alarm(0) + signal(SIGALRM, stop) + alarm(SECONDS) + deadline = monotonic() + 18 + progress = dict(events_replayed=0, typed_cuts_replayed=0, first_unvisited_event=EVENTS-1, + first_unvisited_typed_window=None) + result, timeout, counts = [], None, None + try: + raw = {name: read(args.root, name) for name in PINS} + price, parent, primary = [loads(raw[f"inputs/{name}.json"], object_pairs_hook=unique) + for name in ("PRICE","R101-PRICE","RETIMING")] + assert price["head"] == parent["head"] == primary["head"] == HEAD + assert price["caller_head"] == parent["caller_head"] == CALLER + assert price["parent_price_sha256"] == PINS["inputs/R101-PRICE.json"] + assert price["word_sha256"] == parent["word_sha256"] == WORD + assert price["payload_sha256"] == parent["payload_sha256"] == PAYLOAD + assert primary["pins"]["lead/PRICE.json"] == PINS["inputs/PRICE.json"] + limits = price["limits"] + assert (limits["events"], limits["pair_windows"], limits["typed_cuts"], limits["runner_seconds"]) == ( + EVENTS, WINDOWS, CUTS, SECONDS) + payload = decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(payload).hexdigest() == PAYLOAD + word = loads(payload, object_pairs_hook=unique) + candidates = price["candidates"] + n = word["public"] + assert len(parent["candidates"]) == WINDOWS + 1 + assert [r for r in parent["candidates"] if r["add"][1][2] < n] == candidates + assert [r["add"][1][2] for r in parent["candidates"] if r["add"][1][2] >= n] == [1555] + sources = {r["add"][1][2] for r in candidates} + destinations = {r["key"][2] for r in candidates} + assert len(candidates) == len({tuple(r["key"]) for r in candidates}) == WINDOWS + histories = backwards(word, sources, destinations, deadline, progress) + candidate_results(word, price, candidates, histories, deadline, progress, result) + counts = compare(result, primary) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + + complete = timeout is None and counts is not None + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, controls=checks, complete=complete, + agreement=complete, limits=dict(events=EVENTS, windows=WINDOWS, typed_cuts=CUTS, seconds=SECONDS), + counts=counts, rows=result, progress=progress, timeout=timeout), indent=2, sort_keys=True)) + if not complete: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-original-source-retime-late-donor-bound/engines/r104/reverse_late.py b/research/p104-original-source-retime-late-donor-bound/engines/r104/reverse_late.py new file mode 100644 index 0000000000..c54767d51a --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/engines/r104/reverse_late.py @@ -0,0 +1,270 @@ +"""Verify ten late R104 donor banks by exact reverse covectors.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "8fbd560cf7708b99609614a0b96d02b55efc55304225ddffa5dd223ed49d4073", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "reused/reverse_span.py": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", +} +PRIMARY = "a8f16182496ea2f1b386cdbc2bd3c5551722a7539b6fae508502e00892fd98b6" +CASE_CAP = 10 +SECONDS = 20 +EVENTS = 76466 + + +def unique(pairs): + obj = dict(pairs) + if len(obj) != len(pairs): + raise ValueError("Duplicate JSON key") + return obj + + +def checked(path, pin): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"Changed input {path.name}") + return raw + + +def touches(role, event): + return role == event[1] or event[0] in ("ADD", "COPY") and role == event[2] + + +def ring_ok(q): + d = q.denominator + for p in (2, 3, 5): + while d % p == 0: + d //= p + return d == 1 and abs(q)+1 < 2**16 + + +def requests_for(word, price): + n = word["public"] + tape = word["program"] + frames = word["frames"] + + @cache + def span(label): + values = {0} + for v in frames[label]: + assert type(v) is int and 0 < v < 512 and v not in values + values |= {v ^ u for u in values} + return values + + specs = [] + for row in price["candidates"]: + l, r, mover = row["key"] + a, b, c = row["charts"] + clock, event = row["add"] + source = event[2] + assert b != 207 and 0 <= mover < n and l < clock < r + assert tape[l] == ["MOVE", mover, a, b, False] + assert tape[r] == ["MOVE", mover, b, c, False] + assert tape[clock] == event and event == ["ADD", mover, source, event[3], b] + assert 0 <= source < n and source != mover and Fraction(event[3]) + assert [t for t in range(l+1,r) if touches(mover, tape[t])] == [clock] + assert span(a) < span(b) < span(c) + for side, chart in (("entrance", a), ("exit", c)): + specs.append(dict(key=row["key"]+[side], clock=clock, cut=r, mover=mover, original_chart=b, + chart=chart, source=source, source_multiplier=event[3])) + assert len(specs) == len({tuple(row["key"]) for row in specs}) == CASE_CAP + return specs + + +def collect(word, specs, engine, deadline, progress): + tape = word["program"] + n, owned = word["public"], word["owned_fields"] + assert (len(tape), n, owned) == (EVENTS,1501,68) + requests, source_requests = defaultdict(list), defaultdict(list) + for row in specs: + requests[row["cut"]].append(row) + source_requests[row["clock"]].append(row) + active = word["final"] + [None] * owned + fresh_copy_dest = set() + bank_at = {} + for clock in range(EVENTS - 1, -1, -1): + progress["last_unvisited_event"] = clock + if clock % 128 == 0 and monotonic() >= deadline: + raise TimeoutError("reverse chart walk") + op, d, *args = tape[clock] + assert 0 <= d < len(active) and (d not in fresh_copy_dest or op == "INIT") + if op == "MOVE": + a,b,is_owned = args + assert active[d] == b and is_owned == (d >= n) + active[d] = a + elif op == "INIT": + assert d >= n and active[d] == args[0] + active[d] = None + fresh_copy_dest.discard(d) + elif op == "CLEAR": + assert d >= n and active[d] is None + active[d] = args[0] + else: + assert op in ("ADD", "COPY", "SCALE") and active[d] == args[-1] + engine["coefficient"](args[-2]) + if op in ("ADD", "COPY"): + src = args[0] + assert src != d and active[src] == args[-1] + if op == "COPY": + assert d >= n + fresh_copy_dest.add(d) + for row in source_requests.get(clock, ()): + assert active[row["mover"]] == active[row["source"]] == row["original_chart"] + for row in requests.get(clock, ()): + assert active[row["mover"]] == row["original_chart"] + bank = [role for role, label in enumerate(active) if label == row["chart"] and role != row["mover"]] + bank_at[tuple(row["key"])] = ([r for r in bank if r < n], [r for r in bank if r >= n]) + progress["events_checked"] += 1 + assert active == word["initial"] + [None] * owned and not fresh_copy_dest + progress["last_unvisited_event"] = None + assert len(bank_at) == CASE_CAP + return bank_at + + +def evaluate(word, specs, banks, engine, deadline, rows_out, results): + requests = defaultdict(list) + ids = {} + + def demand(clock, role): + key = clock, role + if key not in ids: + ids[key] = len(ids) + requests[clock].append((role,ids[key])) + return ids[key] + + setups = [] + for row in specs: + clock = row["clock"] + public, owned = banks[tuple(row["key"])] + target_id = demand(clock, row["source"]) + donors = [(r,demand(row["cut"],r)) for r in public] + setups.append((target_id, donors, owned)) + rows = engine["transpose_prefix"](word, requests, len(ids), deadline) + rows_out.extend(rows) + for row,(target_id,donors,owned) in zip(specs,setups,strict=True): + if monotonic() >= deadline: + raise TimeoutError("exact span gate") + target = rows[target_id] + bank = [(r,rows[i]) for r,i in donors] + proof = engine["exact_span"](bank,target) + status, replacement = "outside donor span", None + if proof["status"] == "exact_span": + replacement = {r: Fraction(row["source_multiplier"])*Fraction(v) for r,v in proof["coefficients"].items()} + status = "exact legal coefficients" if all(map(ring_ok,replacement.values())) else "coefficient gate unresolved" + replacement = {r:str(v) for r,v in replacement.items()} + elif proof["status"] == "absent_exterior_coordinate": + j = proof["coordinate"] + assert all(j not in vector for _, (vector,_) in bank) + proof["separating_covector"] = {j:"1"} + proof["separated_target"] = proof["target_coefficient"] + if status == "outside donor span": + dual = {j: Fraction(v) for j, v in proof["separating_covector"].items()} + assert all(engine["dot"](vector, dual) == 0 for _, vector in bank) + separated = engine["dot"](target, dual) + assert separated == Fraction(proof["separated_target"]) != 0 + proof["separated_original_add"] = str(Fraction(row["source_multiplier"]) * separated) + results.append(dict(key=row["key"],cut=row["cut"],chart=row["chart"],source=[row["clock"],row["source"]], + source_nnz=len(target[0]),bank_roles=[r for r,_ in bank],owned_donors_excluded=owned, + target_row_id=target_id,donor_role_row_ids=donors,status=status,replacement_coefficients=replacement, + proof=proof)) + + +def audit(root,engine): + price = loads(checked(root / "inputs/PRICE.json",PINS["inputs/PRICE.json"]),object_pairs_hook=unique) + assert price["head"] == HEAD and price["caller_head"] == CALLER + assert price["word_sha256"] == PINS["inputs/7334-WORD.json.gz"] and price["payload_sha256"] == PAYLOAD + assert 2*price["limits"]["pair_windows"] == CASE_CAP and price["limits"]["runner_seconds"] == SECONDS + tests = engine["controls"]() + assert ring_ok(Fraction(-3,5)) and not ring_ok(Fraction(1,7)) + tests += ["bounded signed coefficient ring"] + keys = [p["key"]+[side] for p in price["candidates"] for side in ("entrance","exit")] + assert len(keys) == len({tuple(k) for k in keys}) == CASE_CAP + results, rows = [], [] + progress = dict(events_checked=0,last_unvisited_event=EVENTS-1) + reason = None + + def stop(*_): + raise TimeoutError("Hard 20-second cap") + + signal(SIGALRM,stop) + alarm(SECONDS) + deadline = monotonic()+SECONDS-2 + try: + raw = decompress(checked(root / "inputs/7334-WORD.json.gz",PINS["inputs/7334-WORD.json.gz"])) + assert sha256(raw).hexdigest() == PAYLOAD + word = loads(raw,object_pairs_hook=unique) + specs = requests_for(word,price) + assert [r["key"] for r in specs] == keys + banks = collect(word,specs,engine,deadline,progress) + evaluate(word,specs,banks,engine,deadline,rows,results) + except TimeoutError as error: + reason = str(error) + finally: + alarm(0) + return dict(head=HEAD,caller_head=CALLER,pins=PINS,cases_cap=CASE_CAP,runner_seconds_cap=SECONDS, + controls=tests,timeout=reason,progress=progress,unvisited=keys[len(results):], + results=results,exact_integer_rows=rows, + counts=dict(Counter(r["status"] for r in results))) + + +def compare(path, result): + primary = loads(checked(path,PRIMARY),object_pairs_hook=unique) + assert primary["head"] == result["head"] + assert primary["pins"]["lead/PRICE.json"] == PINS["inputs/PRICE.json"] + assert primary["pins"]["inputs/7334-WORD.json.gz"] == PINS["inputs/7334-WORD.json.gz"] + assert primary["timeout"] is result["timeout"] is None and not primary["unvisited"] and not result["unvisited"] + assert primary["counts"] == result["counts"] == {"outside donor span": CASE_CAP} + cases = [] + for a,b in zip(primary["results"],result["results"],strict=True): + fields = ("key","cut","chart","source","source_nnz","bank_roles","owned_donors_excluded","status", + "replacement_coefficients") + assert all(a[k] == b[k] for k in fields) + assert a["rank"] == b["proof"]["donor_rank"] + if a["coordinate_separator"] is not None: + assert [b["proof"]["coordinate"],b["proof"]["target_coefficient"]] == a["coordinate_separator"] + else: + assert b["proof"]["status"] == "exact_rank_exclusion" + cases.append(dict(key=b["key"],donor_count=len(b["bank_roles"]),donor_rank=a["rank"], + exact_rank_obstruction=b["proof"]["status"],source=b["source"],cut=b["cut"],chart=b["chart"], + separating_covector=b["proof"]["separating_covector"], + separated_original_add=b["proof"]["separated_original_add"], + owned_donors_excluded=b["owned_donors_excluded"])) + return dict(head=HEAD,primary_sha256=PRIMARY,bank_status_agreement=CASE_CAP, + rank_agreement=CASE_CAP,cases=cases,counts=result["counts"]) + + +def main(): + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root",type=Path,default=ROOT) + parser.add_argument("--primary",type=Path) + parser.add_argument("--controls-only",action="store_true") + args=parser.parse_args() + source="reused/reverse_span.py" + checked(ROOT/source,PINS[source]) + engine=run_path(str(ROOT/source)) + if args.controls_only: + print(dumps(engine["controls"]())) + return + result=audit(args.root,engine) + print(dumps(compare(args.primary,result) if args.primary else result,indent=2,sort_keys=True)) + if result["timeout"]: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-original-source-retime-late-donor-bound/engines/r104/reverse_span.py b/research/p104-original-source-retime-late-donor-bound/engines/r104/reverse_span.py new file mode 100644 index 0000000000..5efbeac87e --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/engines/r104/reverse_span.py @@ -0,0 +1,393 @@ +"""Independent normalized reverse-contact and fraction-free donor-span gate.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import gcd, isqrt, lcm +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE = "c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d" +PRIME = 65521 + + +def unique(pairs): + values = dict(pairs) + assert len(values) == len(pairs), "duplicate JSON key" + return values + + +def checked(path, pin, compressed=False): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"changed input {path.name}") + return loads(decompress(raw) if compressed else raw, object_pairs_hook=unique) + + +@cache +def coefficient(raw): + q = Fraction(raw) + assert q and q.denominator % PRIME, "nonunit native denominator" + return q.numerator, q.denominator + + +def normalized(values, denominator): + if not values: + return {}, 1 + divisor = gcd(denominator, *values.values()) + if divisor != 1: + return {j: a // divisor for j, a in values.items()}, denominator // divisor + return values, denominator + + +def sum_scaled(first, second, factor): + a, da = first + b, db = second + numerator, denom = factor + if not b: + return first + common = lcm(da, db * denom) + out = {j: v * (common // da) for j, v in a.items()} + weight = numerator * (common // (db * denom)) + for j, v in b.items(): + val = out.get(j, 0) + weight * v + if val: + out[j] = val + else: + out.pop(j, None) + return normalized(out, common) + + +def incidence(e): + return e[1:3] if e[0] in ("ADD", "COPY") else e[1:2] + + +def candidates(word, quote): + n = word["public"] + tape = word["program"] + stock = {} + for case in quote["candidates"]: + owner = case["owner"] + left, right = case["move_clocks"] + a, middle, c = case["chart_path"] + original, entry = case["literal_ADD"] + assert case["owner_access"] == "destination" and entry[0] == owner + assert entry[1] == case["peer"] and entry[-1] == middle + assert tape[left] == ["MOVE", owner, a, middle, True] + assert tape[right] == ["MOVE", owner, middle, c, True] + assert tape[original] == ["ADD", *entry] + assert n <= owner and left < original < right + assert [i for i in range(left + 1, right) if owner in incidence(tape[i])] == [original] + assert case["cut_windows_pre_event"] == {"entrance": [left, right], "exit": [left + 1, right]} + stock[owner, left, right] = case + assert len(stock) == 3 and len({tuple(k) for k in quote["keys"]}) == quote["case_cap"] == 33 + return stock + + +def collect(word, cuts, observations, cap): + """Forward structural pass only. Assign one ID to each requested live value.""" + n = word["public"] + chart = list(word["initial"]) + [None] * word["owned_fields"] + revisions = [0] * len(chart) + fresh = set() + starts = {} + lifetimes = {} + requests = defaultdict(list) + observation_ids = {} + bank_ids = {} + value_id = {} + paid = Counter() + + @cache + def span(f): + vectors = {0} + for v in word["frames"][f]: + assert v not in vectors + vectors.update(v ^ t for t in tuple(vectors)) + return vectors + + def request(t, role): + assert chart[role] is not None + key = role, revisions[role] + if key not in value_id: + value_id[key] = len(value_id) + requests[t].append((role, value_id[key])) + return value_id[key] + + tape = word["program"] + for t in range(len(tape) + 1): + if t % 128 == 0 and monotonic() >= cap: + raise TimeoutError("literal structural scan") + for role in observations.get(t, ()): + observation_ids[t, role] = request(t, role) + for key, chart_id, exclude in cuts.get(t, ()): + bank_ids[key] = [(r, request(t, r)) for r, c in enumerate(chart) if c == chart_id and r != exclude] + if t == len(tape): + break + op, d, *args = tape[t] + assert 0 <= d < len(chart) + if op == "INIT": + assert d >= n and chart[d] is None + chart[d], starts[d] = args[0], t + fresh.add(d) + elif op == "CLEAR": + assert d >= n and chart[d] == args[0] and d in starts + lifetimes[d, starts.pop(d)] = t + chart[d] = None + fresh.discard(d) + elif op == "MOVE": + a, b, owned = args + assert chart[d] == a and owned == (d >= n) + assert span(a) < span(b) or owned and span(b) < span(a) + paid[abs(len(word["frames"][b]) - len(word["frames"][a]))] += 1 + chart[d] = b + fresh.discard(d) + continue + elif op == "SCALE": + assert chart[d] == args[-1] + coefficient(args[-2]) + fresh.discard(d) + else: + assert op in ("ADD", "COPY") + src, coeff, f = args + assert d != src and chart[d] == chart[src] == f + coefficient(coeff) + if op == "COPY": + assert d >= n and d in fresh + fresh.discard(d) + revisions[d] += 1 + assert not starts and chart == word["final"] + [None] * word["owned_fields"] + return requests, observation_ids, bank_ids, lifetimes, dict(paid), len(value_id) + + +def transpose_prefix(word, requests, count, cap): + """Propagate all requested output covectors backward, then transpose to input rows.""" + n = word["public"] + empty = ({}, 1) + adjoint = [empty] * (n + word["owned_fields"]) + tape = word["program"] + for t in range(max(requests), -1, -1): + if t % 128 == 0 and monotonic() >= cap: + raise TimeoutError("reverse normalized prefix") + op, d, *args = tape[t] + if op in ("INIT", "CLEAR"): + adjoint[d] = empty + elif op == "SCALE": + adjoint[d] = sum_scaled(empty, adjoint[d], coefficient(args[-2])) + elif op in ("ADD", "COPY"): + src = args[0] + adjoint[src] = sum_scaled(adjoint[src], adjoint[d], coefficient(args[-2])) + if op == "COPY": + adjoint[d] = empty + else: + assert op == "MOVE" + for r, output in requests.get(t, ()): + adjoint[r] = sum_scaled(adjoint[r], ({output: 1}, 1), (1, 1)) + assert not any(d for d, _ in adjoint[n:]) + by_output = [[] for _ in range(count)] + for coord, (coeffs, d) in enumerate(adjoint[:n]): + assert d % PRIME + for i, v in coeffs.items(): + by_output[i].append((coord, v, d)) + rows = [] + for entries in by_output: + common = lcm(*(d for _, _, d in entries)) + rows.append(normalized({i: v * (common // d) for i, v, d in entries}, common)) + return rows + + +def eliminate(v, basis, record=False): + """Reverse-pivot integer elimination. All leading pivots are exact.""" + v = v.copy() + reductions = [] + multiplier = 1 + while v: + k = max(v) + if k not in basis: + break + w = basis[k] + a, b = w[k], v[k] + d = gcd(a, b) + a, b = a // d, b // d + next_v = {j: a * x for j, x in v.items()} + for j, x in w.items(): + z = next_v.get(j, 0) - b * x + if z: + next_v[j] = z + else: + next_v.pop(j, None) + assert k not in next_v + g = gcd(*next_v.values()) or 1 + v = {j: x // g for j, x in next_v.items()} + if record: + reductions.append((k, Fraction(b, a) * multiplier)) + multiplier *= Fraction(g, a) + return v, reductions, multiplier + + +def dot(row, covector): + numerator, denominator = row + return sum((numerator.get(j, 0) * v for j, v in covector.items()), Fraction(0)) / denominator + + +def exact_span(bank, target): + t, dt = target + if not t: + return dict(status="exact_span", coefficients={}) + exterior = next((j for j in sorted(t) if all(j not in row for _, (row, _) in bank)), None) + basis = {} + histories = {} + for role, (v, d) in bank: + reduced, steps, scale = eliminate(v, basis, record=True) + if reduced: + pivot = max(reduced) + basis[pivot] = reduced + histories[pivot] = (role, d, steps, scale) + if exterior is not None: + residue = t[exterior] * pow(dt, -1, PRIME) % PRIME + return dict(status="absent_exterior_coordinate", donor_rank=len(basis), augmented_rank=len(basis)+1, + coordinate=exterior, target_coefficient=str(Fraction(t[exterior], dt)), + target_residue_mod_prime=residue) + residual, steps, scale = eliminate(t, basis, record=True) + if residual: + k = max(residual) + dual = {k: Fraction(1)} + for p, v in sorted(basis.items()): + coefficient = -sum((v.get(j, 0) * c for j, c in dual.items()), Fraction(0)) / v[p] + if coefficient: + dual[p] = coefficient + target_value = dot(target, dual) + assert target_value and all(dot(v, dual) == 0 for _, v in bank) + return dict(status="exact_rank_exclusion", donor_rank=len(basis), augmented_rank=len(basis) + 1, + missing_reverse_pivot=k, residual_integer_row=residual, + separating_covector={j: str(v) for j, v in dual.items()}, separated_target=str(target_value)) + pending = dict(steps) + solution = defaultdict(Fraction) + for pivot in sorted(basis): + if pivot not in pending: + continue + weight = pending.pop(pivot) + if not weight: + continue + role, denom, reductions, factor = histories[pivot] + weight /= factor + solution[role] += weight * denom / dt + for j, scalar in reductions: + pending[j] = pending.get(j, Fraction(0)) - weight * scalar + assert not pending + check = ({}, 1) + rows = dict(bank) + for r, x in solution.items(): + check = sum_scaled(check, rows[r], (x.numerator, x.denominator)) + assert check == target, (check, target) + return dict(status="exact_span", donor_rank=len(basis), + coefficients={r: str(x) for r, x in sorted(solution.items()) if x}) + + +def controls(): + toy = {"public": 4, "owned_fields": 1, "frames": [[]], "initial": [0] * 4, "final": [0] * 4, + "program": [["INIT", 4, 0], ["COPY", 4, 0, "1/2", 0], ["ADD", 4, 1, "-3", 0], + ["ADD", 0, 2, "2", 0], ["CLEAR", 4, 0]]} + req, ids, banks, _, _, count = collect(toy, {3:[((3,), 0, 4)], 4:[((4,), 0, 4)]}, {3:[4]}, float("inf")) + rows = transpose_prefix(toy, req, count, float("inf")) + target = rows[ids[3, 4]] + before = [(r, rows[i]) for r, i in banks[3,] if r in (0, 1)] + after = [(r, rows[i]) for r, i in banks[4,] if r in (0, 1)] + assert exact_span(before, target)["coefficients"] == {0:"1/2", 1:"-3"} + assert exact_span(after, target)["status"] == "exact_rank_exclusion" + assert exact_span(before[1:], target)["status"] == "absent_exterior_coordinate" + # Nontrivial exact dependency and reconstruction after a shared pivot. + multi = [(5, ({0: 3, 1: -1}, 2)), (6, ({0: 1, 1: 4}, 3)), (7, ({0: 11, 1: 2}, 1))] + hit = exact_span(multi, ({0: 11, 1: 2}, 1)) + assert hit["status"] == "exact_span" and len(hit["coefficients"]) == 2 + return ["signed_multi_source_and_owned_COPY", "intervening_write_blocks_span", "absent_exterior_coordinate", + "dependent_donor_bank_exact_reconstruction"] + + +def audit(word, quote, cap, decisions): + assert (word["public"], word["owned_fields"], len(word["program"])) == (1501, 68, 76466) + stock = candidates(word, quote) + observed = defaultdict(set) + cuts = defaultdict(list) + for row in quote["keys"]: + key = tuple(row) + owner, left, right, side, t = key + item = stock[owner, left, right] + chart = item["chart_path"][0 if side == "entrance" else 2] + assert item["cut_windows_pre_event"][side][0] <= t <= item["cut_windows_pre_event"][side][1] + cuts[t].append((key, chart, owner)) + observed[item["literal_ADD"][0]].add(item["peer"]) + requests, refs, banks, lifetimes, paid, count = collect(word, cuts, observed, cap) + assert paid == {1:4000, 2:853, 3:829, 4:223, 5:345, 6:14, 7:10, 8:5} + for item in stock.values(): + left, right = item["owner_lifetime"] + assert lifetimes[item["owner"], left] == right + rows = transpose_prefix(word, requests, count, cap) + for entry in quote["keys"]: + if monotonic() >= cap: + raise TimeoutError("exact donor bank gate") + owner, left, right, side, t = entry + item = stock[owner, left, right] + source = item["peer"] + target_id = refs[item["literal_ADD"][0], source] + target = rows[target_id] + bank = [(r, rows[i]) for r, i in banks[tuple(entry)]] + chart = item["chart_path"][0 if side == "entrance" else 2] + decision = exact_span(bank, target) + decisions.append(dict(key=entry, proposed_chart=chart, literal_read_peer=source, + literal_read_clock=item["literal_ADD"][0], donors=len(bank), owned_donors=sum(r>=word["public"] for r,_ in bank), + target_row_id=target_id, donor_role_row_ids=banks[tuple(entry)], + donor_rowset_sha256=sha256(dumps(bank, sort_keys=True).encode()).hexdigest(), **decision)) + return rows + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--word", type=Path) + parser.add_argument("--price", type=Path) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + if args.controls_only: + print(dumps(controls())) + return + assert args.word is not None and args.price is not None and __debug__ + start = monotonic() + def stop(*_): + raise TimeoutError("hard 20-second runner cap") + signal(SIGALRM, stop) + alarm(20) + decisions = [] + keys = [] + rows = None + tests = [] + timed_out = None + try: + tests = controls() + assert all(PRIME % d for d in range(2, isqrt(PRIME)+1)) + quote = checked(args.price, PRICE) + assert quote["head"] == HEAD and quote["word_sha256"] == WORD + keys = quote["keys"] + rows = audit(checked(args.word, WORD, compressed=True), quote, start+18, decisions) + except TimeoutError as error: + timed_out = str(error) + finally: + alarm(0) + result = dict(head=HEAD, word_sha256=WORD, price_sha256=PRICE, prime=PRIME, + case_cap=33, runner_cap_seconds=20, controls=tests, distinct_requested_rows=len(rows) if rows is not None else None, + requested_integer_rows=rows, + cases=decisions, disposition_counts=dict(Counter(r["status"] for r in decisions)), + unresolved=keys[len(decisions):], timeout=timed_out, + survivors=[r for r in decisions if r["status"] == "exact_span"]) + print(dumps(result, sort_keys=True, indent=2)) + if timed_out: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-original-source-retime-late-donor-bound/engines/r104/support.py b/research/p104-original-source-retime-late-donor-bound/engines/r104/support.py new file mode 100644 index 0000000000..0b9dfa27a9 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/engines/r104/support.py @@ -0,0 +1,139 @@ +"""Exact rational membership of each sole ADD source in its late endpoint banks.""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic, perf_counter + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "lead/PRICE.json": "8fbd560cf7708b99609614a0b96d02b55efc55304225ddffa5dd223ed49d4073", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/R103-RETIMING.json": "331d26d99d45d24796253cd0bf86fdbd8b755ba164ca7765edc8304cc3365f6f", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", +} + + +def unique(pairs): + result = dict(pairs) + if len(result)!=len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def checked(path): + raw = (ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def ring_ok(value): + d = value.denominator + for p in (2,3,5): + while d%p==0: + d//=p + return d==1 and abs(value)+1<2**16 + + +def stop(*_): + raise TimeoutError("hard runner timeout") + + +def main(): + assert __debug__ + price = json.loads(checked("lead/PRICE.json"),object_pairs_hook=unique) + old=json.loads(checked("inputs/R103-RETIMING.json"),object_pairs_hook=unique) + assert old["head"]==price["head"] and old["counts"]=={"different chart":18864} + checked("inputs/donor_span.py") + engine = run_path(str(ROOT/"inputs/donor_span.py")) + checks = engine["controls"]() + assert ring_ok(Q(-3,5)) and not ring_ok(Q(1,7)) + deadline = monotonic()+18 + signal(SIGALRM,stop) + alarm(price["limits"]["runner_seconds"]) + results = [] + pending = [] + reason = None + timings = {"coordinate_seconds":0.0,"same_snapshot_full_solve_seconds":0.0,"coordinate_decisions":0,"fallback_full_solve_seconds":0.0} + keys = [p["key"]+[side] for p in price["candidates"] for side in ("entrance","exit")] + assert len(keys)==len({tuple(k) for k in keys})==10 + try: + raw = decompress(checked("inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest()==price["payload_sha256"] + word = json.loads(raw,object_pairs_hook=unique) + tape = word["program"] + public = word["public"] + req, targets = defaultdict(set),defaultdict(set) + for p in price["candidates"]: + f,g,d = p["key"] + a,b,c = p["charts"] + t,e = p["add"] + s = e[2] + assert f=deadline or (g,chart,d) not in banks or (t,s) not in values: + pending.append(key) + continue + all_live = banks[g,chart,d] + public_bank = {r:row for r,row in all_live.items() if r=deadline: + return None + r=vector.copy() + w={role:Q(1)} + reduce_row(r,basis,w,-1) + if r: + k=min(r) + d=r[k] + basis[k]=({i:a/d for i,a in r.items()},{i:a/d for i,a in w.items()}) + residual=target.copy() + weights={} + reduce_row(residual,basis,weights,1) + rebuilt={} + for role,a in weights.items(): + axpy(rebuilt,bank[role],a) + axpy(rebuilt,residual,Q(1)) + assert rebuilt==target + return dict(rank=len(basis), residual={i:str(v) for i,v in residual.items()}, + matching_coefficients={i:str(v) for i,v in weights.items()} if not residual else None) + + +def snapshot(word,requested,targets,deadline): + public=word["public"] + active=word["initial"]+[None]*word["owned_fields"] + rows=[{i:Q(1)} for i in range(public)]+[None]*word["owned_fields"] + banks,values={},{} + stop=max(requested.keys()|targets.keys()) + for t,e in enumerate(word["program"]): + if t%64==0 and monotonic()>=deadline: + break + for chart,r in requested.get(t,()): + banks[t,chart,r]={i:rows[i].copy() for i in range(len(active)) if i!=r and active[i]==chart and rows[i]} + for s in targets.get(t,()): + assert active[s] is not None + values[t,s]=rows[s].copy() + if t==stop: + break + op,r,*args=e + if op=="MOVE": + assert active[r]==args[0] and args[2]==(r>=public) + active[r]=args[1] + elif op=="INIT": + assert active[r] is None and rows[r] is None and r>=public + active[r]=args[0] + rows[r]={} + elif op=="CLEAR": + assert active[r]==args[0] and rows[r] is not None and r>=public + active[r]=rows[r]=None + elif op=="SCALE": + assert active[r]==args[1] and scalar(args[0]) + rows[r]={i:v*scalar(args[0]) for i,v in rows[r].items()} + else: + s,k,chart=args + assert active[r]==active[s]==chart and r!=s and op in ("ADD","COPY") + if op=="COPY": + assert r>=public and not rows[r] + axpy(rows[r],rows[s],scalar(k)) + return banks,values + + +def controls(): + d=monotonic()+1 + a,b={0:Q(1),1:Q(1)},{1:Q(2)} + assert solve({0:Q(3)}, {7:a,8:b},d)["matching_coefficients"]=={7:"3",8:"-3/2"} + assert solve({2:Q(1)}, {7:a,8:b},d)["residual"]=={2:"1"} + assert solve({0:Q(3)}, {7:{0:Q(1),2:Q(1)},8:b},d)["residual"]=={2:"-3"} + assert solve({}, {7:a},d)["matching_coefficients"]=={} + return ["two-donor span","separating coordinate","changed donor row","zero source"] + + +def main(): + root=Path(sys.argv[1]) + price=checked(root/"price/PRICE.json",PRICE) + word=checked(root/"inputs/7334-WORD.json.gz",WORD,True) + assert price["head"]==HEAD and price["word_sha256"]==WORD + moves=word["program"] + req,targets=defaultdict(set),defaultdict(set) + bykey={} + for p in price["candidates"]: + r,s=p["owner"],p["peer"] + f,g=p["move_clocks"] + a,b,c=p["chart_path"] + t,add=p["literal_ADD"] + assert add[:2]==[r,s] and moves[t]==["ADD",*add] and f=deadline or (t,s) not in values or (cut,chart,r) not in banks: + pending.append(key) + continue + bank=banks[cut,chart,r] + source=values[t,s] + result=solve(source,bank,deadline) + if result is None: + pending.append(key) + continue + output.append(dict(key=key,source=[t,s],target_chart=chart,bank_roles=sorted(bank), + source_nnz=len(source),**result, + decision="exact span survivor" if result["matching_coefficients"] is not None else "outside donor span")) + print(json.dumps(dict(head=HEAD,price_sha256=PRICE,word_sha256=WORD,status="CAPPED" if pending else "EXHAUSTED", + case_cap=33,seconds_cap=18,controls=checks,counts=Counter(x["decision"] for x in output), + decisions=output,unvisited=pending,survivors=[x["key"] for x in output if x["matching_coefficients"] is not None]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-original-source-retime-late-donor-bound/receipts/SEPARATORS.json b/research/p104-original-source-retime-late-donor-bound/receipts/SEPARATORS.json new file mode 100644 index 0000000000..0871c597c0 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/receipts/SEPARATORS.json @@ -0,0 +1,356 @@ +[ + { + "chart": 3, + "covector": { + "28": "1" + }, + "cut": 44609, + "donors": [ + 455, + 556, + 647, + 718, + 722, + 731, + 756, + 1301 + ], + "key": [ + 40102, + 44609, + 205, + "entrance" + ], + "owned_donors_excluded": [], + "signed_add_value": "-1/2", + "source": [ + 40103, + 347 + ], + "source_value": "1" + }, + { + "chart": 207, + "covector": { + "1493": "-1/2", + "58": "1" + }, + "cut": 44609, + "donors": [ + 198, + 962, + 969, + 1081, + 1250, + 1305, + 1453, + 1467 + ], + "key": [ + 40102, + 44609, + 205, + "exit" + ], + "owned_donors_excluded": [ + 1567 + ], + "signed_add_value": "-1/2", + "source": [ + 40103, + 347 + ], + "source_value": "1" + }, + { + "chart": 3, + "covector": { + "29": "1" + }, + "cut": 41178, + "donors": [ + 113, + 115, + 122, + 132, + 140, + 141, + 165, + 198, + 217, + 455, + 473, + 475, + 482, + 495, + 498, + 499, + 523, + 527, + 528, + 530, + 531, + 537, + 538, + 540, + 541, + 543, + 544, + 545, + 550, + 551, + 553, + 554, + 556, + 568, + 569, + 570, + 577, + 580, + 583, + 584, + 585, + 586, + 588, + 589, + 647, + 709, + 715, + 718, + 722, + 731, + 733, + 755, + 756, + 757, + 765, + 900, + 908, + 909, + 930, + 1236, + 1262, + 1301, + 1456, + 1462, + 1473 + ], + "key": [ + 41176, + 41178, + 532, + "entrance" + ], + "owned_donors_excluded": [], + "signed_add_value": "1", + "source": [ + 41177, + 363 + ], + "source_value": "1" + }, + { + "chart": 746, + "covector": { + "29": "1" + }, + "cut": 41178, + "donors": [ + 452, + 1250 + ], + "key": [ + 41176, + 41178, + 532, + "exit" + ], + "owned_donors_excluded": [], + "signed_add_value": "1", + "source": [ + 41177, + 363 + ], + "source_value": "1" + }, + { + "chart": 744, + "covector": { + "27": "1" + }, + "cut": 44611, + "donors": [ + 361 + ], + "key": [ + 41178, + 44611, + 532, + "entrance" + ], + "owned_donors_excluded": [], + "signed_add_value": "1", + "source": [ + 41179, + 452 + ], + "source_value": "-1/2" + }, + { + "chart": 207, + "covector": { + "27": "1" + }, + "cut": 44611, + "donors": [ + 198, + 205, + 962, + 969, + 1081, + 1250, + 1305, + 1453, + 1467 + ], + "key": [ + 41178, + 44611, + 532, + "exit" + ], + "owned_donors_excluded": [ + 1567 + ], + "signed_add_value": "1", + "source": [ + 41179, + 452 + ], + "source_value": "-1/2" + }, + { + "chart": 3, + "covector": { + "2": "1" + }, + "cut": 42599, + "donors": [ + 115, + 132, + 165, + 455, + 531, + 556, + 586, + 647, + 718, + 722, + 731, + 755, + 756, + 765, + 900, + 930, + 1262, + 1301, + 1462, + 1473 + ], + "key": [ + 42533, + 42599, + 198, + "entrance" + ], + "owned_donors_excluded": [], + "signed_add_value": "1/2", + "source": [ + 42534, + 709 + ], + "source_value": "1/4" + }, + { + "chart": 120, + "covector": { + "2": "1" + }, + "cut": 42599, + "donors": [ + 648, + 649, + 653, + 654, + 962, + 1447, + 1493 + ], + "key": [ + 42533, + 42599, + 198, + "exit" + ], + "owned_donors_excluded": [ + 1555 + ], + "signed_add_value": "1/2", + "source": [ + 42534, + 709 + ], + "source_value": "1/4" + }, + { + "chart": 120, + "covector": { + "13": "1" + }, + "cut": 44564, + "donors": [ + 198, + 648, + 649, + 962, + 1447 + ], + "key": [ + 43135, + 44564, + 654, + "entrance" + ], + "owned_donors_excluded": [], + "signed_add_value": "-1/2", + "source": [ + 43136, + 302 + ], + "source_value": "-1/2" + }, + { + "chart": 983, + "covector": { + "40": "1" + }, + "cut": 44564, + "donors": [ + 1305, + 1449 + ], + "key": [ + 43135, + 44564, + 654, + "exit" + ], + "owned_donors_excluded": [], + "signed_add_value": "1/4", + "source": [ + 43136, + 302 + ], + "source_value": "1/4" + } +] diff --git a/research/p104-original-source-retime-late-donor-bound/receipts/SHA256.json b/research/p104-original-source-retime-late-donor-bound/receipts/SHA256.json new file mode 100644 index 0000000000..74964ede3d --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/receipts/SHA256.json @@ -0,0 +1,8 @@ +{ + "r103/independent/RESULT.json": "0ae21450bd1168f73c10c4a055744fad56bfbc3d6a7c93f5638b158401a6466d", + "r103/lead/PRICE.json": "8fbd560cf7708b99609614a0b96d02b55efc55304225ddffa5dd223ed49d4073", + "r103/lead/RETIMING.json": "331d26d99d45d24796253cd0bf86fdbd8b755ba164ca7765edc8304cc3365f6f", + "r104/independent/AGREEMENT.json": "44d389fcc1e5f74838a02a79024fba52c8a6239edbbb8b2e2e38d08b596add61", + "r104/independent/RESULT.json": "d681f827367d8a2150ba3eaaa07b04a1c6e196900471f57795a773f29f15c665", + "r104/lead/SUPPORT.json": "a8f16182496ea2f1b386cdbc2bd3c5551722a7539b6fae508502e00892fd98b6" +} diff --git a/research/p104-original-source-retime-late-donor-bound/replay.py b/research/p104-original-source-retime-late-donor-bound/replay.py new file mode 100644 index 0000000000..38aa31a807 --- /dev/null +++ b/research/p104-original-source-retime-late-donor-bound/replay.py @@ -0,0 +1,183 @@ +"""Replay original-source chronology and late public donor exclusions.""" +from argparse import ArgumentParser +from fractions import Fraction +from hashlib import sha1, sha256 +from json import loads +from pathlib import Path, PurePosixPath +from shutil import copyfile +from subprocess import run +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +WORD = "7334-WORD.json.gz" + + +def unique(pairs): + data = dict(pairs) + if len(data) != len(pairs): + raise ValueError("duplicate JSON key") + return data + + +def decode(raw): + return loads(raw,object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def safe(name): + path = PurePosixPath(name) + if not path.parts or path.is_absolute() or path.as_posix() != name or ".." in path.parts: + raise ValueError("invalid local path " + name) + return path + + +def install(source, destination): + destination.parent.mkdir(parents=True,exist_ok=True) + copyfile(source,destination) + + +def command(script,*args,check=True,timeout=20): + return run([sys.executable,"-I","-B",str(script),*map(str,args)], + capture_output=True,check=check,timeout=timeout) + + +def verify_inputs(): + pins = decode((HERE/"LOCAL-PINS.json").read_bytes()) + for name,expected in pins.items(): + if digest((HERE/safe(name)).read_bytes()) != expected: + raise ValueError("changed dependency " + name) + provenance = decode((HERE/"PROVENANCE.json").read_bytes()) + for name,row in provenance["files"].items(): + raw = (HERE/safe(name)).read_bytes() + assert digest(raw) == row["sha256"] + assert sha1(f"blob {len(raw)}\0".encode()+raw).hexdigest() == row["git_blob"] + for name,row in provenance["derived_inputs"].items(): + receipt = decode((HERE/safe(row["receipt"])).read_bytes()) + assert digest((HERE/safe(name)).read_bytes()) == receipt[row["key"]] + admission = decode((HERE/"inputs/ADMITTED.json").read_bytes()) + parent = decode((HERE/"inputs/R101-PRICE.json").read_bytes()) + assert admission["exit"] == 0 and admission["head"] == parent["head"] + assert admission["caller"] == parent["caller_head"] + assert admission["inputs"]["WORD.json.gz"] == parent["word_sha256"] + + +def verify_separators(price, exact): + rows = exact["exact_integer_rows"] + summaries = decode((HERE/"receipts/SEPARATORS.json").read_bytes()) + adds = {tuple(r["key"]):Fraction(r["add"][1][3]) for r in price["candidates"]} + sizes = [] + for summary,case in zip(summaries,exact["results"],strict=True): + for field in ("key","cut","chart","source","owned_donors_excluded"): + assert summary[field] == case[field] + assert summary["donors"] == case["bank_roles"] + probe = {axis:Fraction(weight) for axis,weight in summary["covector"].items()} + assert summary["covector"] == case["proof"]["separating_covector"] + + def apply(index): + numerator,denominator = rows[index] + return sum((Fraction(numerator.get(axis,0),denominator)*v for axis,v in probe.items()),Fraction()) + + target = apply(case["target_row_id"]) + assert target == Fraction(summary["source_value"]) != 0 + assert target*adds[tuple(case["key"][:3])] == Fraction(summary["signed_add_value"]) + assert all(apply(i)==0 for _,i in case["donor_role_row_ids"]) + sizes.append(len(probe)) + if len(probe) == 2: + assert case["key"] == [40102,44609,205,"exit"] and case["chart"] == 207 + assert probe == {"58":Fraction(1),"1493":Fraction(-1,2)} + assert target == 1 and Fraction(summary["signed_add_value"]) == Fraction(-1,2) + assert sorted(sizes) == [1]*9+[2] + + +def replay(root,output): + verify_inputs() + wanted = decode((HERE/"receipts/SHA256.json").read_bytes()) + regenerated = set() + + def stage(label,script,*args): + raw = command(script,*args).stdout + if digest(raw) != wanted[label]: + raise ValueError(f"changed receipt {label}: {digest(raw)}") + assert label not in regenerated + regenerated.add(label) + dest = root/safe(label) + dest.parent.mkdir(parents=True,exist_ok=True) + dest.write_bytes(raw) + return decode(raw) + + prior,late = root/"r103",root/"r104" + for folder,name,leading,independent in ( + (prior,"r103",("quote.py","retime.py"),"reverse_retime.py"), + (late,"r104",("support.py",),"reverse_late.py"), + ): + for name_py in leading: + install(HERE/"engines"/name/name_py,folder/"lead"/name_py) + install(HERE/"engines"/name/independent,folder/"independent"/independent) + for destination in (folder/"inputs",folder/"independent/inputs"): + install(HERE/"inputs"/WORD,destination/WORD) + + install(HERE/"inputs/R101-PRICE.json",prior/"inputs/R101-PRICE.json") + install(HERE/"inputs/R101-PRICE.json",prior/"independent/inputs/R101-PRICE.json") + price = stage("r103/lead/PRICE.json",prior/"lead/quote.py") + assert len(price["candidates"]) == 5 and price["limits"]["typed_cuts"] == 18864 + assert price["full_paid_after_one"] == 110502 and price["productive"] == 22461 + assert 0 < Fraction(price["one_net_upper"]) < Fraction(price["whole_net_upper"]) < 1 + retime = stage("r103/lead/RETIMING.json",prior/"lead/retime.py") + assert retime["counts"] == {"different chart":18864} and not retime["timeout"] + assert retime["first_unvisited_event"] is retime["first_unvisited_cut"] is None + for label in ("PRICE","RETIMING"): + install(prior/f"lead/{label}.json",prior/f"independent/inputs/{label}.json") + reverse = prior/"independent/reverse_retime.py" + chronology = stage("r103/independent/RESULT.json",reverse) + assert chronology["complete"] and chronology["agreement"] and not chronology["timeout"] + assert chronology["progress"]["events_replayed"] == 76466 + assert chronology["progress"]["typed_cuts_replayed"] == 18864 + + install(prior/"lead/PRICE.json",late/"lead/PRICE.json") + install(prior/"lead/RETIMING.json",late/"inputs/R103-RETIMING.json") + install(HERE/"inputs/donor_span.py",late/"inputs/donor_span.py") + support = stage("r104/lead/SUPPORT.json",late/"lead/support.py") + assert support["counts"] == {"outside donor span":10} and not support["unvisited"] + install(prior/"lead/PRICE.json",late/"independent/inputs/PRICE.json") + install(HERE/"engines/r104/reverse_span.py",late/"independent/reused/reverse_span.py") + donors = late/"independent/reverse_late.py" + exact = stage("r104/independent/RESULT.json",donors) + assert exact["counts"] == support["counts"] and not exact["unvisited"] + assert len(exact["exact_integer_rows"]) == 132 + agreement = stage("r104/independent/AGREEMENT.json",donors,"--primary",late/"lead/SUPPORT.json") + assert agreement["bank_status_agreement"] == agreement["rank_agreement"] == 10 + verify_separators(price,exact) + + for source,directory,name in ((reverse,prior/"independent","PRICE.json"), + (donors,late/"independent",WORD)): + target = directory/"inputs"/name + original = target.read_bytes() + target.write_bytes(original+b"\n") + try: + bad = command(source,check=False,timeout=10) + assert bad.returncode == 1 and not bad.stdout and name.encode() in bad.stderr + finally: + target.write_bytes(original) + + assert regenerated == set(wanted) + if output: + for name in sorted(regenerated): + install(root/safe(name),output/safe(name)) + print("PASS_P104_RETIME_LATE_DONORS typed_cuts=18864 wrong_chart=18864 late_banks=10 separators=10 unresolved=0 receipts=6") + + +def main(): + assert __debug__ and sys.version_info[:2] == (3,12) + parser = ArgumentParser(description=__doc__) + parser.add_argument("--output",type=Path,help="Optional directory for regenerated receipts") + args = parser.parse_args() + with TemporaryDirectory(prefix="p104-retime-late-") as temporary: + replay(Path(temporary),args.output) + + +if __name__ == "__main__": + main()