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-paid-carrier-loan-bound/LOCAL-PINS.json b/research/p104-paid-carrier-loan-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..cd70114d12 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/LOCAL-PINS.json @@ -0,0 +1,28 @@ +{ + "PROVENANCE.json": "2ee3f38aa19774651ed9b22fdbf48bbb32849a0075c566fab8f7b1368a733868", + "engines/immediate.py": "aa7b985c61d209718496edf30f7f47258a276b15d9bc391c8938a6e3169a5354", + "engines/immediate_reverse.py": "a3c137cc53f5973d512b318398a337906912d5ec86511a2349930365401f7c52", + "engines/loan.py": "8679883ebe230c47a6bf4dacd618dd739f6f1d7b6017bc2fb68a4acae489f2da", + "engines/nested.py": "cee12907f43044cb1a08ea355d45fe4d838da6d07b4545445e65f5e4b9ab0045", + "engines/quote.py": "37076d9d1a1c80438073e896b671e782c38c1e82d4c84b02b02d8460045f8cab", + "engines/reverse_audit.py": "e4e093ad96540fc034efd953581af224d8550b09713a12bf936f870817b47cd9", + "engines/reverse_geometry.py": "8340cd379961ed1b36e1e1591aa174e0fb03b86d4bc3695ec9a54c072776f22a", + "engines/support.py": "251301e145ad92b97c45028832aed93dcd826e41d3fdb93f6dd0535737948487", + "engines/verify_span.py": "b398327e066ec30935bac400666be00d0d661331cad15a6247d695de24a4045f", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/PR7362-SHA256.json": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "inputs/R137-PRICE.json": "1e8270d9a48728327f7eab9610a272fbb8ef09518dc4ddc5ceb573be00ae2beb", + "inputs/R137-RESULT.json.gz": "9d9ce10750598d51544452fdeea9b0f3b6869bd7bb22e15cb3e1c0e4f5b84966", + "inputs/R139-PRICE.json": "b9d6d60d467af0269e5dd4d355607c8be5d35581da487f72a593ff775967fb57", + "inputs/R141-PLAN.md": "98cc1cde3b11b291675a0ac657b777f3aa49a9b5dc125543f370f236cac80783", + "inputs/R142-PLAN.md": "53d2ea30224e63e841c43f93183cdc2f25b2720ca4626dfaa2d77edbe65cfe0a", + "inputs/R145-PLAN.md": "12a040d21c719ac7573a423b27876a720b55a65dee074ebfab3539c1b29ea7f5", + "inputs/R92-PRICE.json.gz": "2274f514fb12f9ced0c24abe0c02a76c16cfee4c61f909e37a5ad89b07852371", + "inputs/aggregate.py": "8bf1b91d7fc0937305466686522f5fb3920c66c71830acfc94adde84ba4f49e1", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "receipts/AGREEMENT.json": "603c20584a4fe0cfa92e3314fc50b4de2e7746ded66114d268d2c2446fab2871", + "receipts/SHA256.json": "7abb3441da03d6d0ae7a5e7fff0b613c3f7e997ea59ad687ca8ee790c36accba", + "replay.py": "21802687ecb54f6f452663b17f22f2d20e3d14b006e46dbde5c69a1acf156d4e" +} diff --git a/research/p104-paid-carrier-loan-bound/NOTICE b/research/p104-paid-carrier-loan-bound/NOTICE new file mode 100644 index 0000000000..b32417c22c --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/NOTICE @@ -0,0 +1,10 @@ +Apache-2.0. + +#7334 and #7113 supply the exact word and signed caller. #7338 +supplies comparator admission and a compensated fusion precedent. +#7387 and #7389 supply the exact owned census and signed deletion +prices. #7362 and #7298 supply the base invoice and directed tariff. +#7355 and #7384 supply the exact row and span engines. #7165 and +#7308 supply earlier unchanged-donor recovery evidence. #7244 +supplies earlier role-988/991 work on a distinct funded cut. +OpenAI Codex and subagents materially assisted. diff --git a/research/p104-paid-carrier-loan-bound/PROOF.md b/research/p104-paid-carrier-loan-bound/PROOF.md new file mode 100644 index 0000000000..3959e5c7a7 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/PROOF.md @@ -0,0 +1,116 @@ +# Geometry and restoration for a paid carrier loan + +For an owned role h let m be its old paid MOVE A→B. +The candidate injects h into a distinct existing carrier f while +both are at A. It clears h at A and reconstructs it at B. +Let v be the original normalized row of f at its earlier MOVE +clock u. Immediately after f reaches B, its normalized row is +v+h. In the tested restoration, the unchanged donor bank must +supply v so that a fresh owned h can receive f−v and then +f can be restored by subtracting h. Donor banks exclude h +and f. The two tests retain every other original role path, +scalar event, coefficient and ownership lifetime. + +## Same endpoints with deferred restoration + +The same-endpoint test keeps the original paid carrier A→B. +It holds the temporary carrier value until just before the +owner's first original use, at m+1. Both owner and carrier +must therefore have no intervening original contact while +the loan is live. Reads through ADD or COPY count as contacts. + +All 47 owner anchors have an exact first use at m+1. There +is one earlier same-endpoint MOVE after the owner's last old +contact. It is public f988 at clock 36647, chart 260→1091, +for owner h1540 at clock 45647. Clock 36648 reads f988 into +role 862 with coefficient +1 at chart 1091. It precedes the +specified restoration and excludes the route. The opposite +chronology walks agree on all anchors and zero eligible +carriers. The next test removes the deferred timing condition. + +## Same endpoints with immediate restoration + +Keep f988's original paid MOVE at 36647. Inject h1540 in chart +260, then CLEAR h1540. Freshly INIT it in chart 1091 and restore +both rows before the original ADD at 36648. The owner has no +original contact after clock 35146 and before its old paid MOVE +at 45647. Its first later use is ADD 756←1540 at 45648. +The immediate test preserves every other scalar and paid route. + +At pre-event 36647 both moving roles are in chart 260. The exact +chart-1091 bank has 14 public and three owned live donors. All +17 are granted as read-only sources. Both engines agree on the +137 nonzero coordinates of the original carrier row. The +forward donor matrix has rank 15. Independent reverse covectors +and exact elimination derive the same separator. + +```text +x397 − x382 − 3(x2+x230)/2 +``` + +It evaluates to zero on every allowed donor and −2 on f988. +This excludes the sole immediate exact-route case even with +arbitrary signed rational donor combinations. No donor with a +changed trajectory is granted. + +## Strict nested carrier with immediate restoration + +For an ascending owner MOVE A→B, the earlier carrier originally +moves A→C with strict GF(2) spans A ⊊ B ⊊ C. The proposed +carrier split A→B→C restores both rows at B before the +second leg and the next old event at u. The owner must have +no literal contact from u to its old MOVE. The carrier needs +no later contact restriction after it is restored. + +Both chronology walks agree on each of the 47 previous-owner +contact clocks and the exact nested key. The forward walk +counts six same-source incidences at ascending owner anchors. +The reverse walk counts those six and four incidences at +descending owner anchors, three at 35434 and one at 39811. +The latter four fail A ⊊ B by dimension. Five of the six +ascending-source incidences fail the second strict inclusion. + +The remaining route is h1550 at m=44235 and public f1161 at +u=40226, with chart chain 541→543→127 and ranks 1+1. +The last previous h1550 contact is clock 39172. The next +original h1550 contact after its MOVE is the outward ADD at +44236. The pre-event chart-543 bank at 40226 contains exactly +public roles 628 and 630 and no owned role. + +The exact forward row and independent reverse covectors agree +on the required row v. Its input-4 coefficient is −1/2. +Input coordinate 4 annihilates both donor rows. No rational +combination restores the carrier under the tested contract. +No geometry or support key remains unvisited or unresolved. + +## Complete directed quote + +Write H_r = r^(1−κ). An exact same-route loan would delete 17 +paid rank-r positions across the signed caller while keeping +22,461 productive fields. Its highest one-edit gross upper +at the old crossing is 101.33571240164612 raw. The sole +immediate exact-route candidate would retain f988's paid MOVE +and delete only the owner's rank-one MOVE, for ideal gross 17 +raw and 110,502 paid positions. Its realized saving is zero. + +In the nested test the old pair has ranks r and r+s and the +new pair has ranks r and s. Its exact signed paid delta is +P_{r+s} −17 and P_s +17. The paid count stays 110,519 and +the productive count stays 22,461. Signed surplus becomes +1424+17r. Its directed raw gain is 17(H_{r+s}−H_s). +Concavity bounds it strictly by the corresponding owner +deletion gain 17H_r. The predecode all-47 relaxation gives a +gross upper of 1,896.702946936210 raw at the old crossing, +before compatibility or restoration. That relaxation grants +each owner debit only once. + +The best quoted nested one-edit upper is 101.15855820113319 +raw at the old crossing and its complete fixed-target upper +is −38.69131601905544, both rounded upward. The sole exact +geometry has gross upper 16.91416786145965 and complete +fixed-target upper −122.86124079250860. An additional paid +rank-one position alone would exceed its gross credit. The +literal obstruction leaves zero feasible saving. Any changed +construction would still need physical signed maps and their +adjoints, exact phase, ownership and restoration, and charged +source access, compiler, precision and tape obligations. diff --git a/research/p104-paid-carrier-loan-bound/PROVENANCE.json b/research/p104-paid-carrier-loan-bound/PROVENANCE.json new file mode 100644 index 0000000000..662c979fb5 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/PROVENANCE.json @@ -0,0 +1,93 @@ +{ + "caller": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "scope": "Exact retained signed caller. No caller replay is required for this scoped exclusion.", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7113" + }, + "derived_inputs": { + "inputs/R137-PRICE.json": { + "commit": "8f4b87165e158c4329999ad857b775b4361b4063", + "relationship": "Exact generated R137-PRICE.json used for the immediate exact-route rank-one quote.", + "sha256": "1e8270d9a48728327f7eab9610a272fbb8ef09518dc4ddc5ceb573be00ae2beb", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7387" + }, + "inputs/R137-RESULT.json.gz": { + "commit": "8f4b87165e158c4329999ad857b775b4361b4063", + "compression": "gzip", + "decompressed_sha256": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "relationship": "Exact generated R137-LEAD.json receipt. It supplies the current owned MOVE keys and first contacts. The geometric traversals check the exact literal keys.", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7387" + }, + "inputs/R139-PRICE.json": { + "commit": "50ad6777539c9ad3794989259f2bd081f1eb66be", + "relationship": "Exact generated R139-PRICE.json, signed rank-deletion stock. Used unchanged for the identical-route hypothesis.", + "sha256": "b9d6d60d467af0269e5dd4d355607c8be5d35581da487f72a593ff775967fb57", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7389" + }, + "inputs/R141-PLAN.md": { + "relationship": "Exact predecode scope and cap.", + "sha256": "98cc1cde3b11b291675a0ac657b777f3aa49a9b5dc125543f370f236cac80783" + }, + "inputs/R142-PLAN.md": { + "relationship": "Exact predecode scope and cap.", + "sha256": "53d2ea30224e63e841c43f93183cdc2f25b2720ca4626dfaa2d77edbe65cfe0a" + }, + "inputs/R145-PLAN.md": { + "relationship": "Frozen single immediate-restoration case and cap.", + "sha256": "12a040d21c719ac7573a423b27876a720b55a65dee074ebfab3539c1b29ea7f5" + }, + "inputs/R92-PRICE.json.gz": { + "compression": "gzip", + "key": "R92-PRICE.json", + "receipt": "inputs/PR7362-SHA256.json" + } + }, + "files": { + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "inputs/PR7362-SHA256.json": { + "commit": "5eec7ed633dcf9b9bbc95552aa653da296f863fb", + "git_blob": "b1486e0b5cfe4535f381ed26f7bce4aee21d8a43", + "path": "research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json", + "sha256": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/5eec7ed633dcf9b9bbc95552aa653da296f863fb/research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json" + }, + "inputs/aggregate.py": { + "commit": "4dd0d15c1e94ea3e1ca3c5bd504f6bc142bf7a5e", + "git_blob": "c04096209237b27c7d255f740ea30630895d3c52", + "path": "research/p104-three-move-public-aggregate-bound/engines/aggregate.py", + "sha256": "8bf1b91d7fc0937305466686522f5fb3920c66c71830acfc94adde84ba4f49e1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/4dd0d15c1e94ea3e1ca3c5bd504f6bc142bf7a5e/research/p104-three-move-public-aggregate-bound/engines/aggregate.py" + }, + "inputs/donor_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "46e4621b69bba513f327de53153298e7f4ca0645", + "path": "research/p104-owned-add-source-span-bound/engines/forward.py", + "sha256": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/forward.py" + }, + "inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-paid-carrier-loan-bound/README.md b/research/p104-paid-carrier-loan-bound/README.md new file mode 100644 index 0000000000..9b9697b203 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/README.md @@ -0,0 +1,74 @@ +# Paid carrier loans for owned lifts + +**NO VERIFIED GAIN.** Conditional κ remains `0.00364665195644` +against independently reproduced +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +`aaeec8c0acf01e99a5f331ef363a698d9c084ace` and exact signed +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +`07a76c5e2738882c0cb322278e56f6cae3c9885d`. + +Two tests exhaust all 47 paid owned MOVE anchors. The sole +same-endpoint carrier with restoration deferred to the owner's +old MOVE has an intervening read. The strict nested-carrier test +allows immediate restoration and has one geometric survivor. +Its required carrier row has coefficient −1/2 on input 4. +The only two live cocharted donor rows both have coefficient zero. +Arbitrary rational combinations of those donors fail. + +The same-endpoint route also fails with immediate restoration. +Its chart-1091 bank has 17 live donor rows, including three owned +rows. The exact covector x397 − x382 − 3(x2+x230)/2 annihilates all +17 and evaluates to −2 on the required f988 row. +[Proof and price](PROOF.md) · [Exact agreement](receipts/AGREEMENT.json). + +## Replay + +From a clean checkout use POSIX CPython 3.12 with assertions. + +```sh +python3.12 -I -B research/p104-paid-carrier-loan-bound/replay.py +``` + +The command authenticates the pinned word, earlier census, +signed price and tariff sources. It regenerates eleven original +receipts and checks an exact agreement receipt. Three altered +dependencies are rejected. Use `--out fresh-directory` to retain +all twelve receipts. The standard-library replay works without +Git metadata, network, an external source root or prior temporary +state. [Source provenance](PROVENANCE.json) · [Verification](VERIFICATION.md). + +## Open next questions + +Can one compensated donor trajectory supply the missing input +response in the chart-1091 bank before clock 36648? Start with a +separately priced donor edit and check the four-coordinate dual +while preserving every original read and restoration. This +changes the frozen unchanged-donor contract. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +and [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +supply the word and signed caller. +[#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) +supplies independent comparator admission and a distinct +compensated fusion precedent. +[#7387](https://github.com/CrocSwap/integer-mult-bounds/pull/7387) +supplies the exact owned MOVE census and first-contact inventory. +[#7389](https://github.com/CrocSwap/integer-mult-bounds/pull/7389) +supplies the signed deletion-price stock. +[#7362](https://github.com/CrocSwap/integer-mult-bounds/pull/7362) +supplies the exact base invoice and a distinct paid-midpoint +productive split. [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +supplies the directed tariff. +[#7355](https://github.com/CrocSwap/integer-mult-bounds/pull/7355) +and [#7384](https://github.com/CrocSwap/integer-mult-bounds/pull/7384) +supply forward exact row and donor-span engines. +[#7165](https://github.com/CrocSwap/integer-mult-bounds/pull/7165) +and [#7308](https://github.com/CrocSwap/integer-mult-bounds/pull/7308) +supply earlier unchanged-donor recovery precedents. +[#7244](https://github.com/CrocSwap/integer-mult-bounds/pull/7244) +uses roles 988 and 991 on an earlier word and funded cut. +The current tests use exact #7334 banks and clocks. +OpenAI Codex and subagents materially assisted proof, implementation, +independent replay and packaging. diff --git a/research/p104-paid-carrier-loan-bound/SOURCES.json b/research/p104-paid-carrier-loan-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-paid-carrier-loan-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-paid-carrier-loan-bound/TASK.json b/research/p104-paid-carrier-loan-bound/TASK.json new file mode 100644 index 0000000000..9ffe868a7d --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Every one of the 47 exact #7334 paid owned MOVE anchors. Fixed endpoint carrier loan with no owner/carrier contact during the loan, or an earlier carrier A\u2192C split via a strict nested owner destination B and restored before the next old event. Also restore the sole same-endpoint carrier immediately at its original MOVE, using unchanged cocharted public or owned donors.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 paid carrier research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A carrier loan can trade two paid lifts for one identical lift or for two strictly lower charged ranks only when the original carrier can be restored.", + "budget_minutes": 12, + "evidence": "Exact-route geometry rejects the sole nominal carrier by an intervening contact. One strict nested route survives among six ascending-source incidences. Both exact row engines certify input coordinate 4 separates its required carrier row from both live donors. The immediate same-endpoint alternative has a rank-15 donor span over all 17 eligible rows and an exact four-coordinate separating dual.", + "open_questions": [ + { + "blocked_by": "The sole exact and sole nested routes both lack their original carrier row in the unchanged destination bank.", + "first_step": "Preprice one modified donor trajectory at the chart-1091 bank that can carry the missing covector response and retain all original reads.", + "question": "Can a compensated donor trajectory restore f988 immediately without another paid position?", + "why_it_matters": "The exact same-endpoint route could retain 17 rank-one paid credits if all extra work fits the signed comparator contract." + } + ], + "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": "Keep the owner\u2019s first use and all original scalar clocks fixed. Try borrowing a distinct already paid carrier and exactly restoring its original value at the destination.", + "scope_status": "changed", + "stop_rule": "Both geometry gates exhaust all 47 anchors of the 76,466-event word within 128 priority keys and 25 runner seconds per engine. Test the only nested support key under 30 seconds. The sole immediate same-endpoint support case is capped at 20 seconds.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-paid-carrier-loan-bound/VERIFICATION.md b/research/p104-paid-carrier-loan-bound/VERIFICATION.md new file mode 100644 index 0000000000..7e265b2159 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/VERIFICATION.md @@ -0,0 +1,30 @@ +# Verification + +Direct CPython 3.12.14 replay exited 0 in 6.58 seconds. +A relocated Git-free copy with a cleared environment exited 0 +in 6.55 seconds. All twelve receipts matched byte for byte. +Mutating the nested price, reverse geometry receipt or +immediate-restoration price causes rejection before decoding +the native word. Each control also rejects with the word absent. + +The deferred exact-route engines agree on the absence of a +feasible carrier. The nested geometry engines agree on all 47 +anchors, previous contacts and the sole eligible carrier and +bank. The six versus ten source-incidence counts differ by +the four descending-anchor incidences in the exact agreement. +The two nested support engines agree on the entire required +carrier row and separating coordinate 4. + +The immediate exact-route engines agree on all 17 live donors, +all 137 nonzero carrier coefficients and the four-coordinate +separator. The reverse engine independently reconstructs the +donor rows and derives the separator by exact elimination. +Synthetic controls check the intervening carrier contact, +strict binary nesting, false dimension-only containment, +signed donor recovery and exact separating duals. + +The same signed comparator and caller are retained. No new +physical construction, signed caller or complete conditional +bound was produced. + +[Replay](README.md) · [Exact receipt hashes](receipts/SHA256.json). diff --git a/research/p104-paid-carrier-loan-bound/VERIFY.json b/research/p104-paid-carrier-loan-bound/VERIFY.json new file mode 100644 index 0000000000..d5aaf4ff1e --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Rebuild all three directed quotes, both exact route timing cases, strict nested geometry, both support checks and rejecting mutations.", + "timeout_seconds": 180 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-paid-carrier-loan-bound/engines/immediate.py b/research/p104-paid-carrier-loan-bound/engines/immediate.py new file mode 100644 index 0000000000..01fd4db02f --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/immediate.py @@ -0,0 +1,93 @@ +"""Test same-clock recovery on the sole earlier exact-endpoint carrier.""" +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from sys import argv +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/R137-PRICE.json": "1e8270d9a48728327f7eab9610a272fbb8ef09518dc4ddc5ceb573be00ae2beb", + "inputs/R137-RESULT.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "inputs/R141-REVERSE.json": "508b66c75a45f43b7d231071787d5737feda0505f9d8e633306b19c3423ebad9", + "inputs/aggregate.py": "8bf1b91d7fc0937305466686522f5fb3920c66c71830acfc94adde84ba4f49e1", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", +} +WORD = "inputs/7334-WORD.json.gz" +u, m, f, h, A, B = 36647, 45647, 988, 1540, 260, 1091 + + +def checked(path): + raw = (ROOT / path).read_bytes() + if sha256(raw).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def timeout(*_): + raise TimeoutError("20-second exact cap") + + +def touches(event, role): + return event[1] == role or (event[0] in ("ADD", "COPY") and event[2] == role) + + +def main(): + assert __debug__ and argv[1:] in ([], ["--price-only"]) + data = {path: checked(path) for path in PINS if path != WORD} + quote = loads(data["inputs/R137-PRICE.json"]) + prior = loads(data["inputs/R141-REVERSE.json"]) + assert prior["counts"][-1] == [m, 1, 1] and not prior["eligible"] + one = quote["one"]["1"] + assert one["paid_delta"] == {"1": -17} and one["productive_delta"] == {} + assert one["gross"] == ["17", "17"] and Fraction(one["complete_probe"][0]) > 0 + price = dict(key=[m, h, u, f, A, B], head=quote["head"], caller=quote["caller"], + one=one, case_cap=1, event_cap=76466, runner_seconds=20, pins=PINS) + if argv[1:]: + print(dumps(price, indent=2, sort_keys=True)) + return + + signal(SIGALRM, timeout) + alarm(20) + deadline = monotonic() + 20 + payload = decompress(checked(WORD)) + assert sha256(payload).hexdigest() == "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + word = loads(payload) + tape = word["program"] + assert len(tape) == 76466 and f < word["public"] <= h + assert tape[u] == ["MOVE", f, A, B, False] and tape[m] == ["MOVE", h, A, B, True] + assert tape[u + 1][0:3] == ["ADD", 862, f] + assert tape[m + 1][0:3] == ["ADD", 756, h] + assert not any(touches(event, h) for event in tape[u:m]) + state = word["initial"][:] + [None] * word["owned_fields"] + for op, dest, *args in tape[:u]: + if op in ("INIT", "MOVE"): + state[dest] = args[-1] if op == "INIT" else args[1] + elif op == "CLEAR": + state[dest] = None + assert state[f] == state[h] == A + bank_roles = [role for role, chart in enumerate(state) if chart == B] + helper = run_path(str(ROOT / "inputs/donor_span.py")) + algebra = run_path(str(ROOT / "inputs/aggregate.py")) + tests = algebra["controls"](helper) + banks, targets = helper["snapshot"](word, {u: {(B, h)}}, {u: {f}}, deadline) + assert set(banks) == {(u, B, h)} and (u, f) in targets + bank = banks[u, B, h] + assert set(bank) <= set(bank_roles) + source = targets[u, f] + result = algebra["exact_span"](source, bank, deadline, helper) + if result is None: + timeout() + alarm(0) + receipt = dict(price=price, bank_roles=bank_roles, nonzero_roles=sorted(bank), + source={i: str(v) for i, v in source.items()}, controls=tests, result=result) + print(dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-paid-carrier-loan-bound/engines/immediate_reverse.py b/research/p104-paid-carrier-loan-bound/engines/immediate_reverse.py new file mode 100644 index 0000000000..1825963675 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/immediate_reverse.py @@ -0,0 +1,203 @@ +"""Exact reverse chronology and signed covectors for the one immediate loan.""" +from argparse import ArgumentParser +from fractions import Fraction as Q +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 +PINS={ + "inputs/R145-PLAN.md":"12a040d21c719ac7573a423b27876a720b55a65dee074ebfab3539c1b29ea7f5", + "inputs/R137-PRICE.json":"1e8270d9a48728327f7eab9610a272fbb8ef09518dc4ddc5ceb573be00ae2beb", + "inputs/R137-RESULT.json":"a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "inputs/R141-REVERSE.json":"508b66c75a45f43b7d231071787d5737feda0505f9d8e633306b19c3423ebad9", + "inputs/reverse_covectors.py":"b398327e066ec30935bac400666be00d0d661331cad15a6247d695de24a4045f", + "inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER="07a76c5e2738882c0cb322278e56f6cae3c9885d" +RAW="9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +KEY={"owner":1540,"anchor":45647,"carrier":988,"carrier_move":36647,"charts":[260,1091]} +EVENTS,SECONDS=76466,20 +ZERO,ONE=Q(0),Q(1) + + +def unique(pairs): + x=dict(pairs) + if len(x)!=len(pairs): + raise ValueError("duplicate JSON key") + return x + + +def check(root,name,digest): + data=(root/name).read_bytes() + if sha256(data).hexdigest()!=digest: + raise ValueError("changed dependency "+name) + return data + + +def axpy(dst,src,multiplier): + for key,v in src.items(): + x=dst.get(key,ZERO)+multiplier*v + if x: + dst[key]=x + else: + dst.pop(key,None) + + +def evaluate(vector,covector): + return sum((v*vector.get(k,ZERO) for k,v in covector.items()),ZERO) + + +def solve(target,donors): + for x,v in sorted(target.items()): + if not any(x in row for row in donors.values()): + return dict(decision="outside donor span",dual={x:"1"},value=str(v)) + pivots=[] + for role,row in donors.items(): + r=row.copy() + coeff={role:ONE} + for pivot,old,expansion in pivots: + c=r.get(pivot,ZERO) + if c: + axpy(r,old,-c) + axpy(coeff,expansion,-c) + if not r: + continue + p=min(r) + v=r[p] + pivots.append((p,{k:x/v for k,x in r.items()},{k:x/v for k,x in coeff.items()})) + remaining=target.copy() + coeff={} + for pivot,row,expansion in pivots: + c=remaining.get(pivot,ZERO) + if c: + axpy(remaining,row,-c) + axpy(coeff,expansion,c) + if not remaining: + actual={} + for role,v in coeff.items(): + axpy(actual,donors[role],v) + assert actual==target + return dict(decision="supported",coefficients={r:str(v) for r,v in coeff.items()}) + q=min(remaining) + dual={q:ONE} + for pivot,row,_ in reversed(pivots): + axpy(dual,{pivot:ONE},-evaluate(row,dual)) + assert all(evaluate(r,dual)==0 for r in donors.values()) + assert evaluate(target,dual)==remaining[q] + return dict(decision="outside donor span",dual={i:str(v) for i,v in dual.items()},value=str(remaining[q])) + + +def occurrences(event): + return event[1:3] if event[0] in ("ADD","COPY") else event[1:2] + + +def reverse_bank(word,deadline): + tape=word["program"] + h,m,f,u=(KEY[k] for k in ("owner","anchor","carrier","carrier_move")) + a,b=KEY["charts"] + n=word["public"] + assert tape[u]==["MOVE",f,a,b,False] and tape[m]==["MOVE",h,a,b,True] + assert f=deadline: + raise TimeoutError("reverse chart cap") + op,role,*args=tape[t] + if op=="MOVE": + before,after,owned=args + assert state[role]==after and owned==(role>=n) + state[role]=before + elif op=="INIT": + assert state[role]==args[0] and role>=n + state[role]=None + elif op=="CLEAR": + assert state[role] is None and role>=n + state[role]=args[0] + else: + assert op in ("ADD","COPY","SCALE") and all(state[r]==args[-1] for r in occurrences(tape[t])) + assert state[h]==state[f]==a + donors=[r for r,chart in enumerate(state) if chart==b and r not in (h,f)] + return donors,[[t,tape[t]] for t in (last,u+1,m+1)] + + +def controls(): + assert solve({0:Q(3),1:Q(-2)},{5:{0:ONE},7:{1:ONE}})=={ + "decision":"supported","coefficients":{5:"3",7:"-2"}} + assert solve({0:ONE,1:ONE,2:Q(3)},{5:{0:ONE,2:ONE},7:{1:ONE,2:ONE}})=={ + "decision":"outside donor span","dual":{2:"1",1:"-1",0:"-1"},"value":"1"} + return ["exact signed recovery","exact separating dual with no absent coordinate"] + + +def main(): + assert __debug__ + cli=ArgumentParser(description=__doc__) + cli.add_argument("--root",type=Path,default=ROOT) + cli.add_argument("--price-sha") + cli.add_argument("--controls-only",action="store_true") + args=cli.parse_args() + tests=controls() + if args.controls_only: + print(dumps(tests)) + return + if not args.price_sha: + cli.error("requires frozen R145 price SHA-256") + pins={"inputs/R145-PRICE.json":args.price_sha}|PINS + raw={name:check(args.root,name,digest) for name,digest in pins.items()} + old=loads(raw["inputs/R137-PRICE.json"],object_pairs_hook=unique) + price=loads(raw["inputs/R145-PRICE.json"],object_pairs_hook=unique) + frozen=loads(raw["inputs/R141-REVERSE.json"],object_pairs_hook=unique) + prior=loads(raw["inputs/R137-RESULT.json"],object_pairs_hook=unique) + assert all((p["head"],p["caller"])==(HEAD,CALLER) for p in (old,price,prior)) + assert not frozen["eligible"] and [45647,1,1] in frozen["counts"] + assert old["one"]["1"]["paid_delta"]=={"1":-17} and old["one"]["1"]["gross"]==["17","17"] + assert Q(old["one"]["1"]["complete_probe"][0])>0 + engine=run_path(str(args.root/"inputs/reverse_covectors.py")) + + def stop(*_): + raise TimeoutError("20-second hard cap") + signal(SIGALRM,stop) + alarm(SECONDS) + deadline=monotonic()+SECONDS-1 + try: + blob=decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(blob).hexdigest()==RAW + word=loads(blob,object_pairs_hook=unique) + tape=word["program"] + assert len(tape)==EVENTS and word["public"]==1501 and word["owned_fields"]==68 + donors,contacts=reverse_bank(word,deadline) + carrier=KEY["carrier"] + rows=engine["prefix_rows"](tape,KEY["carrier_move"],[carrier,*donors],deadline) + assert all(k=word["public"]], + rows={r:{k:str(v) for k,v in row.items()} for r,row in rows.items()},unresolved=[]) + finally: + alarm(0) + print(dumps(ans,indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-paid-carrier-loan-bound/engines/loan.py b/research/p104-paid-carrier-loan-bound/engines/loan.py new file mode 100644 index 0000000000..caea48ff6f --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/loan.py @@ -0,0 +1,100 @@ +"""Bound one carrier loan while preserving both literal ownership itineraries.""" +from collections import defaultdict +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +from pathlib import Path +from time import monotonic +import json +import sys + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/R137-RESULT.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "inputs/R139-PRICE.json": "b9d6d60d467af0269e5dd4d355607c8be5d35581da487f72a593ff775967fb57", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} + + +def unique(items): + out = dict(items) + if len(out) != len(items): + raise ValueError("duplicate key") + return out + + +def raw(path): + data = (ROOT / path).read_bytes() + if sha256(data).hexdigest() != PINS[path]: + raise ValueError(f"changed {path}") + return data + + +def quote(): + anchors = json.loads(raw("inputs/R137-RESULT.json"), object_pairs_hook=unique) + price = json.loads(raw("inputs/R139-PRICE.json"), object_pairs_hook=unique) + assert (price["head"], price["caller"]) == (anchors["head"], anchors["caller"]) + assert len(anchors["records"]) == 47 and all(a["first_clock"] == a["move_clock"]+1 for a in anchors["records"]) + assert all(a["first_event"][0] in {"ADD", "SCALE"} for a in anchors["records"]) + raw("inputs/7334-WORD.json.gz") + return dict(head=price["head"], caller=price["caller"], quotes=price["quotes"], pins=PINS, + whole_gross_upper=price["whole_gross_upper"], fixed_target_upper=price["fixed_target_upper"], + max_anchors=47, max_events=76466, max_cases=128, max_seconds=25, max_support_cases=8, + max_support_seconds=30, max_builds=1) + + +def roles(event): + return event[1:3] if event[0] in {"ADD", "COPY"} else event[1:2] + + +def candidates(program, records): + contacts, endpoint_moves = defaultdict(list), defaultdict(list) + preceding, following = {}, {} + for t, e in enumerate(program): + op = e[0] + for r in set(roles(e)): + past = contacts[r] + if past: + preceding[t,r] = past[-1] + following[past[-1],r] = t + past.append(t) + if op == "MOVE": + endpoint_moves[tuple(e[2:4])].append((t,e[1])) + result = [] + for a in records: + m, h, k = (a[field] for field in ("move_clock", "role", "first_clock")) + ab = (a["chart_from"], a["chart_to"]) + assert program[m] == ["MOVE",h,*ab,True] + assert program[k] == a["first_event"] and following[m,h] == k + for t,f in endpoint_moves[ab]: + if preceding.get((m,h),-1) < t < m and f != h and following.get((t,f),len(program)) >= k: + result.append(dict(owner=h, anchor=m, carrier=f, carrier_move=t, first_use=k, charts=list(ab), rank=a["rank"])) + return sorted(result,key=lambda r:(-r["rank"], r["anchor"]-r["carrier_move"],r["anchor"],r["carrier"])) + + +def screen(price): + begin = monotonic() + expected = json.dumps(price, indent=2, sort_keys=True)+"\n" + assert (ROOT / "lead/PRICE.json").read_text() == expected + program = json.loads(decompress(raw("inputs/7334-WORD.json.gz")), object_pairs_hook=unique)["program"] + records = json.loads(raw("inputs/R137-RESULT.json"), object_pairs_hook=unique)["records"] + assert len(program) == price["max_events"] + control = [["INIT",3,1],["MOVE",2,1,2,False],["MOVE",3,1,2,True],["ADD",2,3,"1",2]] + synthetic = [dict(move_clock=2,role=3,first_clock=3,first_event=control[3],chart_from=1,chart_to=2,rank=1)] + assert len(candidates(control,synthetic)) == 1 + bad = control[:2]+[["SCALE",2,"-1",2]]+control[2:] + assert not candidates(bad,[dict(synthetic[0],move_clock=3,first_clock=4)]) + found = candidates(program, records) + assert monotonic()-begin < price["max_seconds"], "event cap expired before complete inventory" + ranks = {k["anchor"]:k["rank"] for k in found} + upper = sum(Fraction(price["quotes"][str(r)]["gross"][1]) for r in ranks.values()) + return dict(head=price["head"], events=len(program), anchors=len(records), topology_keys=len(found), + distinct_supported_anchors=len(ranks), visited=found[:price["max_cases"]], unvisited=found[price["max_cases"]:], + conditional_upper=str(upper), support_unresolved=found) + + +if __name__ == "__main__": + assert __debug__ + p = quote() + assert sys.argv[1:] in ([], ["--price-only"]) + print(json.dumps(p if sys.argv[1:] else screen(p), indent=2, sort_keys=True)) diff --git a/research/p104-paid-carrier-loan-bound/engines/nested.py b/research/p104-paid-carrier-loan-bound/engines/nested.py new file mode 100644 index 0000000000..2eabda586d --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/nested.py @@ -0,0 +1,134 @@ +"""Census all strictly nested carriers in the frozen owner contact intervals.""" +from collections import 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 time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/R137-RESULT.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "next/PRICE.json": "7f99902aaa6b47029f51fa0e10a59c677a78eca0e91b43c213d4f7e34cfececa", +} + + +def unique(items): + obj = dict(items) + if len(obj) != len(items): + raise ValueError("duplicate JSON key") + return obj + + +def checked(path): + data = (ROOT / path).read_bytes() + if sha256(data).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency {path}") + return data + + +@cache +def span(rows): + out = {0} + for row in rows: + assert row not in out + out.update(row ^ other for other in tuple(out)) + return frozenset(out) + + +def census(word, anchors, cells, deadline): + frames = [tuple(frame) for frame in word["frames"]] + public = word["public"] + state = word["initial"] + [None] * word["owned_fields"] + program = word["program"] + by_clock = {a["move_clock"]: a for a in anchors} + by_source = defaultdict(list) + for a in anchors: + m, h, lo, mid = (a[k] for k in ("move_clock", "role", "chart_from", "chart_to")) + assert program[m] == ["MOVE", h, lo, mid, True] + assert a["first_clock"] == m+1 and program[m+1] == a["first_event"] + assert abs(len(frames[mid])-len(frames[lo])) == a["rank"] + if span(frames[lo]) < span(frames[mid]): + by_source[lo].append((m, h, mid)) + else: + assert span(frames[mid]) < span(frames[lo]) + latest, inside, receipt, keys = {}, defaultdict(list), [], [] + for u, event in enumerate(program): + if u%128 == 0 and monotonic() >= deadline: + return receipt, keys, u + op, role, *args = event + before = state[role] + if u in by_clock: + a = by_clock[u] + last = latest[role] + matches = [x for x in inside[u] if x["carrier_move"]>last] + keys.extend(x for x in matches if x["nested"]) + receipt.append(dict(anchor=u,owner=role,last_contact=last, + charts=[a["chart_from"],a["chart_to"]], + source_moves=len(matches),nested_keys=sum(x["nested"] for x in matches))) + if op == "MOVE": + lo, hi, owned = args + assert before==lo and owned==(role>=public) + for m,h,mid in by_source[lo]: + if not (u=public],price_upper=cells[r,s]["gross"][1]) + inside[m].append(info) + state[role]=hi + elif op == "INIT": + assert before is None and role>=public + state[role]=args[0] + elif op == "CLEAR": + assert before==args[0] and role>=public + state[role]=None + else: + assert op in {"SCALE","ADD","COPY"} and before==args[-1] + if op in {"ADD","COPY"}: + assert args[0]!=role and state[args[0]]==before + for i in (event[1:3] if op in {"ADD","COPY"} else [role]): + latest[i]=u + assert state==word["final"]+[None]*word["owned_fields"] + assert len(receipt)==len(anchors)==47 + return receipt, keys, None + + +def main(): + assert __debug__ + begin=monotonic() + prices=loads(checked("next/PRICE.json"),object_pairs_hook=unique) + old=loads(checked("inputs/R137-RESULT.json"),object_pairs_hook=unique) + assert prices["head"]==old["head"] and prices["caller"]==old["caller"] + assert prices["paid"]==110519 and prices["productive"]==22461 and len(prices["cells"])==33 + assert span(())128: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-paid-carrier-loan-bound/engines/quote.py b/research/p104-paid-carrier-loan-bound/engines/quote.py new file mode 100644 index 0000000000..538b35bc5d --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/quote.py @@ -0,0 +1,51 @@ +"""Price a nested carrier split before reading the literal word.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +PINS = { + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "../lead/PRICE.json": "88ff264d2744dee9bc0bc9ecfe25fc4e53f30958c8c947d16e4df87c908e5c65", +} + +def read(name): + raw = (ROOT / name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError(f"changed {name}") + return raw + +def main(): + assert __debug__ + p = json.loads(read("inputs/R92-PRICE.json")) + prior = json.loads(read("../lead/PRICE.json")) + read("inputs/pricing.py") + cost = run_path(str(ROOT / "inputs/pricing.py"))["cost"] + assert p["head"] == prior["head"] and p["caller_head"] == prior["caller"] + incumbent, probe, target = (Q(p[k]) for k in ("old_crossing_upper", "probe", "moonshot")) + net = Counter({int(r): n for r, n in p["old_targets"].items()}) + net.subtract({int(r): n for r, n in p["old_paid"].items()}) + cells = [] + for r in range(1, 7): + for s in range(1, 10-r): + gain = {r+s: 17, s: -17} + edited = net.copy() + edited.update(gain) + gross = cost(gain, incumbent) + at_probe = cost(edited, probe) + assert gross[0] > 0 and at_probe[0] > 0 + cells.append(dict(r=r,s=s,paid_delta={r+s:-17,s:17},rank_surplus=1424+17*r, + gross=list(map(str,gross)),complete_probe=list(map(str,at_probe)), + fixed_target_complete_upper=str(cost(edited,target)[1]))) + print(json.dumps(dict(pins=PINS, head=p["head"], caller=p["caller_head"], paid=110519, + productive=22461, whole_gross_upper=prior["whole_gross_upper"], + fixed_target_upper=prior["fixed_target_upper"], + maximum_one_edit=max(cells,key=lambda c:Q(c["gross"][1])), cells=cells), + sort_keys=True, indent=2)) + +if __name__ == "__main__": + main() diff --git a/research/p104-paid-carrier-loan-bound/engines/reverse_audit.py b/research/p104-paid-carrier-loan-bound/engines/reverse_audit.py new file mode 100644 index 0000000000..96f8af98b7 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/reverse_audit.py @@ -0,0 +1,41 @@ +"""Independently count earlier carriers with a reverse first-contact walk.""" +import gzip +import hashlib +import json +from pathlib import Path + +base = Path(__file__).resolve().parents[1] +pins = { + "lead/PRICE.json": "88ff264d2744dee9bc0bc9ecfe25fc4e53f30958c8c947d16e4df87c908e5c65", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/R137-RESULT.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", +} + +def load(name): + raw = (base / name).read_bytes() + assert hashlib.sha256(raw).hexdigest() == pins[name] + return json.loads(gzip.decompress(raw) if name.endswith(".gz") else raw) + +price = load("lead/PRICE.json") +rows = load("inputs/R137-RESULT.json")["records"] +word = load("inputs/7334-WORD.json.gz")["program"] +def touch(e, h): + return h in e[1:3] if e[0] in ("COPY", "ADD") else h == e[1] + +eligible, counts = [], [] +for row in rows: + anchor, h = row["move_clock"], row["role"] + next_use = row["first_clock"] + assert touch(word[next_use], h) and next_use == anchor + 1 + moves = [] + for t in range(anchor-1, -1, -1): + e = word[t] + if touch(e, h): + break + if e[0] == "MOVE" and e[2:4] == [row["chart_from"], row["chart_to"]]: + moves.append((t,e[1])) + blocked = [(t,f) for t,f in moves if any(touch(e,f) for e in word[t+1:next_use])] + eligible.extend([anchor,t,f] for t,f in moves if (t,f) not in blocked) + counts.append([anchor,len(moves),len(blocked)]) +assert len(word) == price["max_events"] and len(rows) == price["max_anchors"] and not eligible +print(json.dumps({"counts": sorted(counts), "eligible": eligible, "pins": pins}, sort_keys=True, indent=2)) diff --git a/research/p104-paid-carrier-loan-bound/engines/reverse_geometry.py b/research/p104-paid-carrier-loan-bound/engines/reverse_geometry.py new file mode 100644 index 0000000000..040111c0af --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/reverse_geometry.py @@ -0,0 +1,238 @@ +"""Reverse literal interval census for a split earlier paid carrier.""" +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 signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PINS = { + "inputs/R142-PLAN.md": "53d2ea30224e63e841c43f93183cdc2f25b2720ca4626dfaa2d77edbe65cfe0a", + "inputs/R142-PRICE.json": "7f99902aaa6b47029f51fa0e10a59c677a78eca0e91b43c213d4f7e34cfececa", + "inputs/R139-PRICE.json": "b9d6d60d467af0269e5dd4d355607c8be5d35581da487f72a593ff775967fb57", + "inputs/R137-RESULT.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +RAW = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +EVENTS, ANCHORS, KEYS, SECONDS = 76466, 47, 128, 25 + + +def unique(pairs): + obj = dict(pairs) + if len(obj) != len(pairs): + raise ValueError("duplicate JSON key") + return obj + + +def authenticate(root): + payloads = {} + for name, digest in PINS.items(): + raw = (root/name).read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError("changed dependency "+name) + payloads[name] = raw + return payloads + + +def reduce(vector, basis): + while vector: + pivot = vector.bit_length()-1 + if pivot not in basis: + break + vector ^= basis[pivot] + return vector + + +def span(vectors): + basis = {} + for vector in vectors: + residual = reduce(vector,basis) + assert residual + basis[residual.bit_length()-1] = residual + return basis + + +def incidences(event): + return event[1:3] if event[0] in ("COPY","ADD") else event[1:2] + + +def reverse_census(word, rows, prices, deadline, progress): + n, owned, tape = (word[k] for k in ("public","owned_fields","program")) + state = word["final"] + [None]*owned + frames = word["frames"] + bank = defaultdict(set) + for role,chart in enumerate(state): + if chart is not None: + bank[chart].add(role) + open_by_role = {} + open_by_source = defaultdict(set) + next_contact = {} + records = {} + geometry = [] + paid_owned = set() + + @cache + def is_strict_subset(a,b): + return len(frames[a]) < len(frames[b]) and all( + reduce(vector,basis(b)) == 0 for vector in frames[a]) + + @cache + def basis(chart): + return span(frames[chart]) + + def change(role, old, new): + assert state[role] == old + if old is not None: + bank[old].remove(role) + if new is not None: + bank[new].add(role) + state[role] = new + + for t in range(len(tape)-1,-1,-1): + progress["first_unvisited_event"] = t + if t%128 == 0 and monotonic() >= deadline: + raise TimeoutError("reverse traversal time cap") + event = tape[t] + op,role,*args = event + touched = incidences(event) + for h in touched: + if h in open_by_role: + anchor = open_by_role.pop(h) + source = rows[anchor]["chart_from"] + open_by_source[source].remove(anchor) + records[anchor]["previous"] = [t,event] + + if op == "MOVE": + a,c,is_owned = args + assert is_owned == (role >= n) + change(role,c,a) + if is_owned: + paid_owned.add(t) + for anchor in sorted(open_by_source[a]): + r = rows[anchor] + h,b = r["role"],r["chart_to"] + assert role != h and state[h] == a and t < anchor + count = records[anchor] + count["source_moves"] += 1 + if not is_strict_subset(a,b) or not is_strict_subset(b,c): + count["not_strict_chain"] += 1 + continue + dr,ds = len(frames[b])-len(frames[a]),len(frames[c])-len(frames[b]) + assert dr == r["rank"] and (dr,ds) in prices + if len(geometry) == KEYS: + raise OverflowError("128 exact geometry keys reached before all source incidences") + donors = sorted(bank[b]-{h,role}) + geometry.append(dict( + anchor=anchor, carrier=t, h=h, f=role, + charts=[a,b,c], ranks=[dr,ds], carrier_owned=is_owned, + donor_public=[x for x in donors if x < n], + donor_owned=[x for x in donors if x >= n], + gross_upper=prices[dr,ds], + )) + count["strict_chain"] += 1 + if is_owned: + r = rows[t] + assert (role,a,c) == (r["role"],r["chart_from"],r["chart_to"]) + assert abs(len(frames[a])-len(frames[c])) == r["rank"] + nxt = next_contact[role] + assert nxt == r["first_clock"] == t+1 and tape[nxt] == r["first_event"] + assert tape[nxt][0] in ("ADD","SCALE") + open_by_role[role] = t + open_by_source[a].add(t) + records[t] = dict(anchor=t,h=role,first_use=[nxt,tape[nxt]],source_moves=0, + not_strict_chain=0,strict_chain=0) + elif op == "INIT": + assert role >= n + change(role,args[0],None) + elif op == "CLEAR": + assert role >= n + change(role,None,args[0]) + else: + assert op in ("ADD","COPY","SCALE") + assert all(state[h] == args[-1] for h in touched) + if op == "COPY": + assert role >= n + for h in touched: + next_contact[h] = t + progress["events"] += 1 + assert state == word["initial"]+[None]*owned + assert paid_owned == rows.keys() and not open_by_role + progress["first_unvisited_event"] = None + return records,geometry + + +def controls(): + toy = { + "public":3, "owned_fields":1, "frames":[[],[1],[1,2]], + "initial":[0,1,0], "final":[2,1,0], + "program":[["INIT",3,0],["ADD",3,2,"1",0],["MOVE",0,0,2,False], + ["MOVE",3,0,1,True],["ADD",1,3,"1",1],["CLEAR",3,1]], + } + rows = {3:dict(role=3,chart_from=0,chart_to=1,rank=1,first_clock=4,first_event=toy["program"][4])} + records, geom = reverse_census(toy,rows,{(1,1):"17"},monotonic()+1,{"events":0}) + assert records[3]["previous"] == [1,toy["program"][1]] + assert len(geom)==1 and geom[0]["donor_public"]==[1] + assert geom[0]["carrier"] == 2 and geom[0]["charts"] == [0,1,2] + toy["frames"][2] = [2,4] + records, geom = reverse_census(toy,rows,{(1,1):"17"},monotonic()+1,{"events":0}) + assert not geom and records[3]["not_strict_chain"] == 1 + return ["nested carrier with untouched live B donor","larger dimension without B containment"] + + +def main(): + cli = ArgumentParser(description=__doc__) + cli.add_argument("--root",type=Path,default=ROOT) + cli.add_argument("--controls-only",action="store_true") + args = cli.parse_args() + assert __debug__ + tests = controls() + if args.controls_only: + print(dumps(tests)) + return + data = authenticate(args.root) + quote, old, previous = [loads(data["inputs/"+name],object_pairs_hook=unique) for name in + ("R142-PRICE.json","R139-PRICE.json","R137-RESULT.json")] + assert all((p["head"],p["caller"]) == (HEAD,CALLER) for p in (quote,old,previous)) + prices = {(r["r"],r["s"]):r["gross"][1] for r in quote["cells"]} + assert len(prices)==33 and all(Fraction(x)>0 for x in prices.values()) + rows = {r["move_clock"]:r for r in previous["records"]} + assert len(rows) == ANCHORS and not previous["unvisited"] + assert {str(t):[r["role"],r["chart_from"],r["chart_to"],r["rank"]] for t,r in rows.items()} == old["keys"] + + def stop(*_): + raise TimeoutError("25-second hard cap") + + signal(SIGALRM,stop) + alarm(SECONDS) + progress = {"events":0,"first_unvisited_event":EVENTS-1} + deadline = monotonic()+SECONDS-1 + result = dict(head=HEAD,caller=CALLER,pins=PINS,controls=tests,progress=progress, + caps=dict(events=EVENTS,anchors=ANCHORS,keys=KEYS,seconds=SECONDS)) + try: + raw=decompress(data["inputs/7334-WORD.json.gz"]) + assert sha256(raw).hexdigest()==RAW + word=loads(raw,object_pairs_hook=unique) + assert (len(word["program"]),word["public"],word["owned_fields"]) == (EVENTS,1501,68) + records,geometry=reverse_census(word,rows,prices,deadline,progress) + ordered=sorted(geometry,key=lambda g:(-Fraction(g["gross_upper"]),g["anchor"],g["carrier"])) + result |= dict(complete=True, anchors=[records[t] for t in sorted(records)], geometry=ordered, + counts=dict(Counter({name:sum(r[name] for r in records.values()) for name in + ("source_moves","not_strict_chain","strict_chain")})),unresolved=[]) + except (TimeoutError,OverflowError) as e: + result |= dict(complete=False, reason=str(e),unresolved=sorted(rows)) + finally: + alarm(0) + print(dumps(result,indent=2,sort_keys=True)) + if not result["complete"]: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-paid-carrier-loan-bound/engines/support.py b/research/p104-paid-carrier-loan-bound/engines/support.py new file mode 100644 index 0000000000..7d72e3a613 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/support.py @@ -0,0 +1,55 @@ +"""Check the exact carrier row at the frozen R142 nested move.""" +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path +from runpy import run_path +from time import monotonic + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/donor_span.py":"4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "inputs/aggregate.py":"8bf1b91d7fc0937305466686522f5fb3920c66c71830acfc94adde84ba4f49e1", + "next/PRICE.json":"7f99902aaa6b47029f51fa0e10a59c677a78eca0e91b43c213d4f7e34cfececa", +} + + +def checked(path): + raw=(ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def main(): + assert __debug__ + checked("inputs/donor_span.py") + checked("inputs/aggregate.py") + price=loads(checked("next/PRICE.json")) + assert Fraction(price["cells"][0]["complete_probe"][0])>0 + data=decompress(checked("inputs/7334-WORD.json.gz")) + assert sha256(data).hexdigest()=="9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + word=loads(data) + u,m,f,h,B=40226,44235,1161,1550,543 + program=word["program"] + assert program[u]==["MOVE",f,541,127,False] and program[m]==["MOVE",h,541,B,True] + helper=run_path(str(ROOT/"inputs/donor_span.py")) + algebra=run_path(str(ROOT/"inputs/aggregate.py")) + tests=algebra["controls"](helper) + limit=monotonic()+28 + req={(u,B,h)} + banks,targets=helper["snapshot"](word,{u:{(B,h)}},{u:{f}},limit) + assert set(banks)==req and (u,f) in targets + bank=banks[u,B,h] + assert sorted(bank)==[628,630] + result=algebra["exact_span"](targets[u,f],bank,limit,helper) + if result is None: + raise TimeoutError("exact support cap reached") + print(dumps(dict(key=[m,h,u,f,B],head=price["head"],caller=price["caller"],pins=PINS,controls=tests, + source={i:str(v) for i,v in targets[u,f].items()},bank_roles=sorted(bank),result=result),indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-paid-carrier-loan-bound/engines/verify_span.py b/research/p104-paid-carrier-loan-bound/engines/verify_span.py new file mode 100644 index 0000000000..c40717bb91 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/engines/verify_span.py @@ -0,0 +1,149 @@ +"""Independent reverse pullback and exact two-donor span decision for R142.""" +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM,alarm,signal +from time import monotonic + +ROOT = Path(__file__).resolve().parent +PINS = { + "GEOMETRY.json": "92f5533fb14a10f6594cca514e508478dc5e1e493701cb2ac63af7a0f5f0df02", + "reverse_geometry.py": "8340cd379961ed1b36e1e1591aa174e0fb03b86d4bc3695ec9a54c072776f22a", +} +ZERO, ONE = Q(0), Q(1) + + +def check(name,digest): + raw=(ROOT/name).read_bytes() + if sha256(raw).hexdigest()!=digest: + raise ValueError("changed dependency "+name) + return raw + + +@cache +def rational(x): + return Q(x) + + +def prefix_rows(tape,cut,roles,deadline): + dual = {r:{r:ONE} for r in roles} + for t in range(cut-1,-1,-1): + if t%128==0 and monotonic()>=deadline: + raise TimeoutError("reverse covector cap") + op,dst,*args=tape[t] + for row in dual.values(): + if dst not in row: + continue + value=row[dst] + if op in ("INIT","CLEAR","COPY"): + del row[dst] + if op in ("ADD","COPY"): + src, coeff, _ = args + new=row.get(src,ZERO)+value*rational(coeff) + if new: + row[src]=new + else: + row.pop(src,None) + elif op=="SCALE": + row[dst]=value*rational(args[0]) + else: + assert op in ("MOVE","INIT","CLEAR") + return dual + + +def value(row,coord): + return row.get(coord,ZERO) + + +def certify(target,first,second): + columns=sorted(target.keys() | first.keys() | second.keys()) + for x in columns: + if value(target,x) and not (value(first,x) or value(second,x)): + return {"decision":"outside span","dual":{x:"1"},"value":str(target[x])} + donors=[first,second] + if not first: + donors.reverse() + a,b=donors + if not a: + assert not target + return {"decision":"supported","coefficients":["0","0"]} + x=min(a) + other=next((y for y in columns if a[x]*value(b,y)-value(b,x)*value(a,y)),None) + tx,bx=value(target,x),value(b,x) + if other is None: + alpha,beta=tx/a[x],ZERO + else: + y=other + det=a[x]*value(b,y)-bx*value(a,y) + alpha=(tx*value(b,y)-bx*value(target,y))/det + beta=(a[x]*value(target,y)-tx*value(a,y))/det + for z in columns: + residual=value(target,z)-alpha*value(a,z)-beta*value(b,z) + if not residual: + continue + if other is None: + weights={x:-value(a,z)/a[x],z:ONE} + else: + y=other + ax,ay,az=a[x],value(a,y),value(a,z) + bx,by,bz=value(b,x),value(b,y),value(b,z) + weights={x:(-az*by+ay*bz)/det,y:(-ax*bz+az*bx)/det,z:ONE} + assert all(sum(w*value(v,k) for k,w in weights.items())==0 for v in (a,b)) + assert sum(w*value(target,k) for k,w in weights.items())==residual + return {"decision":"outside span","dual":{k:str(w) for k,w in weights.items() if w}, + "value":str(residual)} + coeff=[str(alpha),str(beta)] + return {"decision":"supported","coefficients":coeff if a is first else coeff[::-1]} + + +def main(): + assert __debug__ + geom=loads(check("GEOMETRY.json",PINS["GEOMETRY.json"])) + check("reverse_geometry.py",PINS["reverse_geometry.py"]) + g=run_path(str(ROOT/"reverse_geometry.py")) + assert geom["complete"] and not geom["unresolved"] and len(geom["geometry"])==1 + key=geom["geometry"][0] + assert (key["anchor"],key["carrier"],key["h"],key["f"],key["donor_public"],key["donor_owned"]) == ( + 44235,40226,1550,1161,[628,630],[]) + assert certify({0:Q(2),1:Q(-3)},{0:ONE},{1:ONE})=={ + "decision":"supported","coefficients":["2","-3"]} + assert certify({0:ONE,1:ONE,2:Q(3)},{0:ONE,2:ONE},{1:ONE,2:ONE})=={ + "decision":"outside span","dual":{0:"-1",1:"-1",2:"1"},"value":"1"} + + def timeout(*_): + raise TimeoutError("30-second hard cap") + + signal(SIGALRM,timeout) + alarm(30) + deadline=monotonic()+29 + try: + raw=decompress(g["authenticate"](ROOT)["inputs/7334-WORD.json.gz"]) + assert sha256(raw).hexdigest()==g["RAW"] + word=loads(raw,object_pairs_hook=g["unique"]) + tape=word["program"] + clock=key["carrier"] + h=key["h"] + anchor=key["anchor"] + roles=[key["f"],*key["donor_public"]] + cut=next(r for r in geom["anchors"] if r["anchor"]==anchor) + assert cut["previous"][0] < clock < anchor < cut["first_use"][0] == anchor+1 + assert all(h not in g["incidences"](e) for e in tape[clock:anchor]) + assert tape[clock]==["MOVE",roles[0],541,127,False] + assert tape[anchor]==["MOVE",h,541,543,True] + rows=prefix_rows(tape,clock,roles,deadline) + assert all(k fresh-price.json +cmp lead/PRICE.json fresh-price.json +python3.12 -I -B lead/loan.py > fresh-geometry.json +``` diff --git a/research/p104-paid-carrier-loan-bound/inputs/R142-PLAN.md b/research/p104-paid-carrier-loan-bound/inputs/R142-PLAN.md new file mode 100644 index 0000000000..a0e365c905 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/inputs/R142-PLAN.md @@ -0,0 +1,26 @@ +# R142 · shorten one retained paid carrier through an owned destination + +This is a preflight only. Exact #7334 aaeec8c0acf01e99a5f331ef363a698d9c084ace, κ 0.00364665195644, and signed #7113 07a76c5e2738882c0cb322278e56f6cae3c9885d. R141 exhausted the exact same-endpoint carrier test across all 47 owned MOVE anchors. The new route uses a larger already-paid carrier exit, with no native decode or geometry run in reserve. + +## Literal proposed edit + +Owner h has paid A→B at old clock m. Find another already live public or owned role f with old paid A→C at clock u r142-fresh-price.json +cmp next/PRICE.json r142-fresh-price.json +``` + +Price SHA256 7f99902aaa6b47029f51fa0e10a59c677a78eca0e91b43c213d4f7e34cfececa. Inputs pin the admitted exact comparator price, tariff and R141 cap by relative paths. The unchanged literal input and R137 anchors are pinned in R141 SHA256. The exact #7386 chart-207 terminal report surfaced in the last refresh and remains distinct. + +## First implementation step and caps + +After a new overlap refresh, copy the R141 geometry contact walker into an isolated R142 root. Replace exact endpoint indexing with source-chart indexing, precompute GF(2) nested span checks on the declared catalogue, and test A⊊B⊊C inside each exact h interval. Record all endpoints, ranks, clock keys and live untouched B bank labels. At most 76,466 events, 47 owned anchors, 128 priority keys or 25 runner seconds. If positive, test exact v membership from up to eight highest fully priced keys or 30 seconds using the R137 rational engine, with a signed planted loan/restoration and missing-axis negative control. Preserve keys beyond caps as unresolved. One candidate may get a 120-second signed literal prototype only after exact span, legal coefficients with at most 16 actual ADDs, directed price and compiler/ownership feasibility. Scale only if exact verified net saving and a compatible count can clear the target. Zero geometry or all-scope exact span exclusions trigger a pivot. No R142 word decode occurred in reserve. diff --git a/research/p104-paid-carrier-loan-bound/inputs/R145-PLAN.md b/research/p104-paid-carrier-loan-bound/inputs/R145-PLAN.md new file mode 100644 index 0000000000..43eae8d062 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/inputs/R145-PLAN.md @@ -0,0 +1,16 @@ +# Round 145 · immediate restoration of the exact-route carrier + +Exact #7334 aaeec8c0acf01e99a5f331ef363a698d9c084ace and signed #7113 07a76c5e2738882c0cb322278e56f6cae3c9885d. R141 found one earlier exact route, owner1540 old MOVE45647 and public carrier988 MOVE36647 on 260→1091, blocked only by an intervening carrier use under the deferred-restoration contract. R142 restores at the carrier's old MOVE clock but requires a strict larger exit. Apply that same-clock restoration to this sole equal-endpoint key. At pre-event36647 add h into f, clear h early in chart260, execute f's unchanged paid MOVE, freshly INIT h at 1091, recover h=f−v from the existing unchanged bank and restore f−=h before ADD36648. Delete h's old paid MOVE. Require no original h contact until its actual next use45648. All other paid/scalar paths remain fixed. + +Price one compatible old rank-one deletion before decode. Exact R137 quote P1−17, T fixed, 110,502 paid, 22,461 productive, surplus 1441. Gross upper 17 raw, positive complete probe and insufficient alone for fixed moonshot. No new paid child credited. New ordinary ADDs, early owner occupancy, absolute signed physical action and adjoint, compiler, peak memory/precision/tape and source charging require actual replay on any survivor. + +Cap one exact key, 76,466 events, and 20 runner seconds. Confirm chronology and proper nesting; test original f row against all existing cocharted public and owned donors at the carrier clock. Exact nonmembership closes this scope. A rational solution must use legal coefficients with at most 16 ADDs and fit the full paid invoice. Only then emit one literal candidate and run 120-second signed prototype followed by complete independent verification. Preserve any missing or unverified gate. + +CPython 3.12 and assertions: + +```sh +python3.12 -I -B lead/immediate.py --price-only > fresh-price.json +cmp lead/PRICE.json fresh-price.json +python3.12 -I -B lead/immediate.py > fresh-result.json +cmp lead/RESULT.json fresh-result.json +``` diff --git a/research/p104-paid-carrier-loan-bound/inputs/R92-PRICE.json.gz b/research/p104-paid-carrier-loan-bound/inputs/R92-PRICE.json.gz new file mode 100644 index 0000000000..0307eb95e2 Binary files /dev/null and b/research/p104-paid-carrier-loan-bound/inputs/R92-PRICE.json.gz differ diff --git a/research/p104-paid-carrier-loan-bound/inputs/aggregate.py b/research/p104-paid-carrier-loan-bound/inputs/aggregate.py new file mode 100644 index 0000000000..c040962092 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/inputs/aggregate.py @@ -0,0 +1,164 @@ +"""Test the two fixed public endpoint banks for the literal role-532 aggregate.""" +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/R130-PRICE.json": "d9074aad58d3ffdad995ba68b2ffa541ae2b7df833b757d8e1a9767118140f39", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", +} +ROLE = 532 +BANKS = ((44611, 3, ROLE), (44612, 207, ROLE)) +SOURCES = ((41177, 363, Q(1), 744), (41179, 452, Q(-2), 746)) + + +def unique(pairs): + obj = dict(pairs) + if len(obj) != len(pairs): + raise ValueError("duplicate JSON key") + return obj + + +def read(path): + data = (ROOT / path).read_bytes() + if sha256(data).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency {path}") + return data + + +def invoice(): + old = loads(read("inputs/R130-PRICE.json"), object_pairs_hook=unique) + assert old["head"] == HEAD and old["caller"] == CALLER + assert old["word_sha256"] == PINS["inputs/7334-WORD.json.gz"] + by_role = {p["role"]: p for p in old["candidates"] if all(e[1] == p["role"] for _, e in p["contacts"])} + assert set(by_role) == {198, ROLE} + lead = by_role[ROLE] + assert lead["clocks"] == [41176, 41178, 44611] and lead["charts"] == [3, 744, 746, 207] + assert lead["contacts"] == [[t, ["ADD", ROLE, s, str(q), c]] for t, s, q, c in SOURCES] + assert lead["paid_delta"] == {"2": -17, "3": -34, "8": 17} + assert 0 < Q(lead["probe_lower"]) <= Q(lead["raw_upper"]) < 1 + return dict(head=HEAD, caller=CALLER, pins=PINS, candidate=lead, + compatible_cap=2, gross_upper=str(sum(Q(p["raw_upper"]) for p in by_role.values())), + paid=old["after_paid_one"], productive=old["productive"], surplus=old["surplus"], + selected_banks=[list(k) for k in BANKS], unresolved_role198=[42533,42599,44596]) + + +def exact_span(target, bank, deadline, helpers): + absent = set(target).difference(*(row.keys() for row in bank.values())) + if absent: + i = min(absent) + return dict(decision="outside donor span", separator={i: "1"}, separator_value=str(target[i]), + absent_coordinates=sorted(absent)) + # Row elimination, then transpose the reduction onto one nonzero residual coordinate. + axpy = helpers["axpy"] + basis = {} + for role, vector in sorted(bank.items()): + if monotonic() >= deadline: + return None + row, weights = vector.copy(), {role: Q(1)} + helpers["reduce_row"](row, basis, weights, -1) + if row: + i = min(row) + factor = row[i] + basis[i] = ({j: a / factor for j, a in row.items()}, {j: a / factor for j, a in weights.items()}) + row, weights = target.copy(), {} + helpers["reduce_row"](row, basis, weights, 1) + if not row: + check = {} + for role, q in weights.items(): + axpy(check, bank[role], q) + assert check == target + return dict(decision="exact span survivor", rank=len(basis), + coefficients={i: str(q) for i, q in weights.items()}) + i = min(row) + dual = {i: Q(1)} + for pivot, (vector, _) in sorted(basis.items(), reverse=True): + value = sum(q * dual.get(j, 0) for j, q in vector.items()) + if value: + dual[pivot] = dual.get(pivot, 0) - value + if not dual[pivot]: + del dual[pivot] + def dot(vector): + return sum(q * vector.get(j, 0) for j, q in dual.items()) + assert all(dot(v) == 0 for v in bank.values()) and dot(target) == row[i] + return dict(decision="outside donor span", rank=len(basis), + separator={j: str(q) for j, q in dual.items()}, separator_value=str(dot(target))) + + +def controls(helpers): + d = monotonic() + 1 + bank = {7: {0: Q(1), 1: Q(1)}, 8: {1: Q(2)}} + assert exact_span({0: Q(3)}, bank, d, helpers)["coefficients"] == {7: "3", 8: "-3/2"} + assert exact_span({0: Q(3), 2: Q(1)}, bank, d, helpers)["separator"] == {2: "1"} + covector = exact_span({0: Q(1)}, {7: bank[7]}, d, helpers) + assert covector["separator"] == {0: "-1", 1: "1"} and covector["separator_value"] == "-1" + return ["two donor exact aggregate", "exterior-coordinate perturbation", "same-support covector separation"] + + +def main(): + assert __debug__ + price = invoice() + if sys.argv[1:] == ["--price-only"]: + print(dumps(price, sort_keys=True, indent=2)) + return + assert not sys.argv[1:] + deadline = monotonic() + 18 + read("inputs/donor_span.py") + helpers = run_path(str(ROOT / "inputs/donor_span.py")) + control = controls(helpers) + raw = decompress(read("inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest() == PAYLOAD + word = loads(raw, object_pairs_hook=unique) + program = word["program"] + assert len(program) == 76466 + paid = price["candidate"] + a, b, c = paid["clocks"] + charts = paid["charts"] + assert [program[t] for t in (a, b, c)] == [ + ["MOVE", ROLE, x, y, False] for x, y in zip(charts[:-1], charts[1:], strict=True) + ] + selected = set() + for t in range(a + 1, c): + if t == b: + continue + e = program[t] + if ROLE in (e[1:3] if e[0] in {"ADD", "COPY"} else e[1:2]): + selected.add(t) + assert selected == {t for t, *_ in SOURCES} + assert all(program[t] == ["ADD", ROLE, s, str(q), chart] for t, s, q, chart in SOURCES) + req = {cut: {(chart, role)} for cut, chart, role in BANKS} + refs = {t: {s} for t, s, *_ in SOURCES} + banks, values = helpers["snapshot"](word, req, refs, deadline) + rows, aggregate = [], {} + if all((t, s) in values for t, s, *_ in SOURCES): + for t, s, q, _ in SOURCES: + helpers["axpy"](aggregate, values[t, s], q) + for key in BANKS: + if key not in banks or monotonic() >= deadline: + break + bank = {i: row for i, row in banks[key].items() if i < word["public"]} + result = exact_span(aggregate, bank, deadline, helpers) + if result is None: + break + rows.append(dict(key=list(key), bank_roles=sorted(bank), **result)) + unvisited = [list(k) for k in BANKS[len(rows):]] + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, price=price, + aggregate={i: str(a) for i, a in aggregate.items()}, + controls=control, rows=rows, unvisited=unvisited, + role198_status="outside this two-bank scope"), sort_keys=True, indent=2)) + if unvisited: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-paid-carrier-loan-bound/inputs/donor_span.py b/research/p104-paid-carrier-loan-bound/inputs/donor_span.py new file mode 100644 index 0000000000..46e4621b69 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/inputs/donor_span.py @@ -0,0 +1,169 @@ +"""Match the literal ADD source using other live rows in the retimed chart.""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +import sys +from time import monotonic + +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE="c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d" + + +def checked(path,want,compressed=False): + raw=path.read_bytes() + if sha256(raw).hexdigest()!=want: + raise ValueError(f"changed dependency: {path.name}") + return json.loads(decompress(raw) if compressed else raw) + + +@cache +def scalar(x): + return Q(x) + + +def axpy(dst,src,c): + for k,a in src.items(): + value=dst.get(k,0)+c*a + if value: + dst[k]=value + else: + dst.pop(k,None) + + +def reduce_row(row,basis,weights,multiplier): + for k,(v,w) in sorted(basis.items()): + a=row.get(k,0) + if a: + axpy(row,v,-a) + axpy(weights,w,multiplier*a) + + +def solve(target,bank,deadline): + basis={} + for role,vector in sorted(bank.items()): + if monotonic()>=deadline: + return None + r=vector.copy() + w={role:Q(1)} + reduce_row(r,basis,w,-1) + if r: + k=min(r) + d=r[k] + basis[k]=({i:a/d for i,a in r.items()},{i:a/d for i,a in w.items()}) + residual=target.copy() + weights={} + reduce_row(residual,basis,weights,1) + rebuilt={} + for role,a in weights.items(): + axpy(rebuilt,bank[role],a) + axpy(rebuilt,residual,Q(1)) + assert rebuilt==target + return dict(rank=len(basis), residual={i:str(v) for i,v in residual.items()}, + matching_coefficients={i:str(v) for i,v in weights.items()} if not residual else None) + + +def snapshot(word,requested,targets,deadline): + public=word["public"] + active=word["initial"]+[None]*word["owned_fields"] + rows=[{i:Q(1)} for i in range(public)]+[None]*word["owned_fields"] + banks,values={},{} + stop=max(requested.keys()|targets.keys()) + for t,e in enumerate(word["program"]): + if t%64==0 and monotonic()>=deadline: + break + for chart,r in requested.get(t,()): + banks[t,chart,r]={i:rows[i].copy() for i in range(len(active)) if i!=r and active[i]==chart and rows[i]} + for s in targets.get(t,()): + assert active[s] is not None + values[t,s]=rows[s].copy() + if t==stop: + break + op,r,*args=e + if op=="MOVE": + assert active[r]==args[0] and args[2]==(r>=public) + active[r]=args[1] + elif op=="INIT": + assert active[r] is None and rows[r] is None and r>=public + active[r]=args[0] + rows[r]={} + elif op=="CLEAR": + assert active[r]==args[0] and rows[r] is not None and r>=public + active[r]=rows[r]=None + elif op=="SCALE": + assert active[r]==args[1] and scalar(args[0]) + rows[r]={i:v*scalar(args[0]) for i,v in rows[r].items()} + else: + s,k,chart=args + assert active[r]==active[s]==chart and r!=s and op in ("ADD","COPY") + if op=="COPY": + assert r>=public and not rows[r] + axpy(rows[r],rows[s],scalar(k)) + return banks,values + + +def controls(): + d=monotonic()+1 + a,b={0:Q(1),1:Q(1)},{1:Q(2)} + assert solve({0:Q(3)}, {7:a,8:b},d)["matching_coefficients"]=={7:"3",8:"-3/2"} + assert solve({2:Q(1)}, {7:a,8:b},d)["residual"]=={2:"1"} + assert solve({0:Q(3)}, {7:{0:Q(1),2:Q(1)},8:b},d)["residual"]=={2:"-3"} + assert solve({}, {7:a},d)["matching_coefficients"]=={} + return ["two-donor span","separating coordinate","changed donor row","zero source"] + + +def main(): + root=Path(sys.argv[1]) + price=checked(root/"price/PRICE.json",PRICE) + word=checked(root/"inputs/7334-WORD.json.gz",WORD,True) + assert price["head"]==HEAD and price["word_sha256"]==WORD + moves=word["program"] + req,targets=defaultdict(set),defaultdict(set) + bykey={} + for p in price["candidates"]: + r,s=p["owner"],p["peer"] + f,g=p["move_clocks"] + a,b,c=p["chart_path"] + t,add=p["literal_ADD"] + assert add[:2]==[r,s] and moves[t]==["ADD",*add] and f=deadline or (t,s) not in values or (cut,chart,r) not in banks: + pending.append(key) + continue + bank=banks[cut,chart,r] + source=values[t,s] + result=solve(source,bank,deadline) + if result is None: + pending.append(key) + continue + output.append(dict(key=key,source=[t,s],target_chart=chart,bank_roles=sorted(bank), + source_nnz=len(source),**result, + decision="exact span survivor" if result["matching_coefficients"] is not None else "outside donor span")) + print(json.dumps(dict(head=HEAD,price_sha256=PRICE,word_sha256=WORD,status="CAPPED" if pending else "EXHAUSTED", + case_cap=33,seconds_cap=18,controls=checks,counts=Counter(x["decision"] for x in output), + decisions=output,unvisited=pending,survivors=[x["key"] for x in output if x["matching_coefficients"] is not None]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-paid-carrier-loan-bound/inputs/pricing.py b/research/p104-paid-carrier-loan-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/inputs/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/p104-paid-carrier-loan-bound/receipts/AGREEMENT.json b/research/p104-paid-carrier-loan-bound/receipts/AGREEMENT.json new file mode 100644 index 0000000000..93e05a742a --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/receipts/AGREEMENT.json @@ -0,0 +1,76 @@ +{ + "anchored_cases": 47, + "exact_route_blocker": [ + 36648, + [ + "ADD", + 862, + 988, + "1", + 1091 + ] + ], + "exact_route_nominal": [ + 45647, + 36647, + 988 + ], + "forward_ascending": 6, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "nested_geometry": { + "anchor": 44235, + "carrier": 40226, + "carrier_owned": false, + "charts": [ + 541, + 543, + 127 + ], + "donor_owned": [], + "donor_public": [ + 628, + 630 + ], + "f": 1161, + "gross_upper": "42285419653649119703395556732799431826679854310187/2500000000000000000000000000000000000000000000000", + "h": 1550, + "ranks": [ + 1, + 1 + ] + }, + "reverse_all": 10, + "reverse_descending": 4, + "separator": { + "4": "1" + }, + "separator_value": "-1/2", + "source_incidences": { + "30581": [ + "ascending", + 1, + 1 + ], + "35434": [ + "descending", + 0, + 3 + ], + "39811": [ + "descending", + 0, + 1 + ], + "44235": [ + "ascending", + 1, + 1 + ], + "45647": [ + "ascending", + 4, + 4 + ] + }, + "unresolved": [] +} diff --git a/research/p104-paid-carrier-loan-bound/receipts/SHA256.json b/research/p104-paid-carrier-loan-bound/receipts/SHA256.json new file mode 100644 index 0000000000..544f6ce5c6 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/receipts/SHA256.json @@ -0,0 +1,13 @@ +{ + "R141-GEOMETRY.json": "dc9fa3853050dd0fe128b40c756965053d103737561d76f13f879ed36bdb9140", + "R141-INDEPENDENT.json": "508b66c75a45f43b7d231071787d5737feda0505f9d8e633306b19c3423ebad9", + "R141-PRICE.json": "88ff264d2744dee9bc0bc9ecfe25fc4e53f30958c8c947d16e4df87c908e5c65", + "R142-GEOMETRY.json": "8f43843881d3fa3d34181ea99aa3707097f3a9c2fd74a45feb8759afae22a030", + "R142-INDEPENDENT-GEOMETRY.json": "92f5533fb14a10f6594cca514e508478dc5e1e493701cb2ac63af7a0f5f0df02", + "R142-INDEPENDENT-SPAN.json": "987621c5f23852a95298df2a428856b56291baef0cb65075fd27dc48f149bd2e", + "R142-PRICE.json": "7f99902aaa6b47029f51fa0e10a59c677a78eca0e91b43c213d4f7e34cfececa", + "R142-SUPPORT.json": "8cd71c0a605663d918d6f06217a742b3b53ecf32b0fdceaeee3eaee6a86a59be", + "R145-INDEPENDENT.json": "ed1ee6fb37876ba3628937466fe5273b773240dd9f32f4d56aa611a5210bb912", + "R145-LEAD.json": "690a6d5ec054df64230c352ea2afe7e2b46329ed590eb6101cd6428e30c49de6", + "R145-PRICE.json": "9fe8145daaed58f7276177b3543f480fd0e5e7f74489206688bdbc036a8da201" +} diff --git a/research/p104-paid-carrier-loan-bound/replay.py b/research/p104-paid-carrier-loan-bound/replay.py new file mode 100644 index 0000000000..6093208006 --- /dev/null +++ b/research/p104-paid-carrier-loan-bound/replay.py @@ -0,0 +1,225 @@ +"""Replay the fixed-route and nested P104 paid carrier exclusions.""" +from argparse import ArgumentParser +from gzip import decompress +from hashlib import sha1,sha256 +from json import dumps,loads +from pathlib import Path +from subprocess import run +from tempfile import TemporaryDirectory +import sys + +ROOT=Path(__file__).resolve().parent + + +def unique(items): + out=dict(items) + if len(out)!=len(items): + raise ValueError('duplicate JSON key') + return out + + +def decode(raw): + return loads(raw,object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def source(name): + path=Path(name) + if path.is_absolute() or '..' in path.parts or path.as_posix()!=name: + raise ValueError('invalid package-relative path '+name) + return (ROOT/path).read_bytes() + + +def load_inputs(): + pins=decode(source('LOCAL-PINS.json')) + for name,expected in pins.items(): + if digest(source(name))!=expected: + raise ValueError('changed package dependency '+name) + p=decode(source('PROVENANCE.json')) + for name,entry in p['files'].items(): + raw=source(name) + assert digest(raw)==entry['sha256']==pins[name] + assert sha1(f'blob {len(raw)}\0'.encode()+raw).hexdigest()==entry['git_blob'] + old=decompress(source('inputs/R92-PRICE.json.gz')) + assert digest(old)==decode(source('inputs/PR7362-SHA256.json'))['R92-PRICE.json'] + a=decode(source('inputs/ADMITTED.json')) + assert a['head']=='aaeec8c0acf01e99a5f331ef363a698d9c084ace' + assert a['kappa']=='0.00364665195644' + return old + + +def call(script,*args,expect_success=True): + p=run([sys.executable,'-I','-B',str(script),*args],capture_output=True,timeout=40) + if expect_success and p.returncode: + sys.stderr.write(p.stderr.decode(errors='replace')) + p.check_returncode() + return p + + +def write(path,raw): + path.parent.mkdir(parents=True,exist_ok=True) + path.write_bytes(raw) + + +def reconcile(raw_word,predecessor,exact,exact_reverse,nested,nested_reverse,lead,reverse): + word=decode(decompress(raw_word)) + anchors={r["move_clock"]:r for r in predecessor["records"]} + tape=word["program"] + frames=word["frames"] + assert len(anchors)==exact["anchors"]==47 and len(tape)==exact["events"]==76466 + assert not (exact["topology_keys"] or exact["unvisited"] or exact["support_unresolved"] + or exact_reverse["eligible"]) + counts={r[0]:r[1:] for r in exact_reverse["counts"]} + assert counts.keys()==anchors.keys() + assert {k:v for k,v in counts.items() if v!=[0,0]}=={45647:[1,1]} + erow=anchors[45647] + incidences=lambda e: e[1:3] if e[0] in ("ADD","COPY") else e[1:2] + previous=next(t for t in range(45646,-1,-1) if erow["role"] in incidences(tape[t])) + routes=[(t,e[1]) for t in range(previous+1,45647) + if (e:=tape[t])[0]=="MOVE" and e[2:4]==[erow["chart_from"],erow["chart_to"]]] + assert len(routes)==1 + clock,carrier=routes[0] + blocked=next(t for t in range(clock+1,45648) if carrier in incidences(tape[t])) + + forward={r["anchor"]:r for r in nested["anchors"]} + backward={r["anchor"]:r for r in nested_reverse["anchors"]} + assert forward.keys()==backward.keys()==anchors.keys() + split={} + for clock_h,h in anchors.items(): + f,b=forward[clock_h],backward[clock_h] + a,c=h["chart_from"],h["chart_to"] + assert (f["owner"],f["charts"],f["last_contact"])==(b["h"],[a,c],b["previous"][0]) + assert b["strict_chain"]==f["nested_keys"] + if len(frames[a])