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-public-four-move-rechart-bound/LOCAL-PINS.json b/research/p104-public-four-move-rechart-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..c2a84f13fe --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/LOCAL-PINS.json @@ -0,0 +1,18 @@ +{ + "engines/compare.py": "988b121bdc6a081af783c14f89e05a0383e62536cceda911311d0ebbf40fc3a4", + "engines/quote.py": "be3f9cc196485413b1e667e21e3d61cc236b2f822835bf9df8ae4872d9aa0890", + "engines/rechart_gate.py": "ab89a72dc849b10e0837dd42f4be2d8717f75e32bb14630943dd8570bcfa3053", + "engines/reverse_geometry.py": "689d19969beb151d264455f8ea659cc0ea63d5a5a4bb3dca9f3b312520df61f3", + "inputs/7277-SUPPORT.json.gz": "a63d766dce9ccc5b7a97057fb298350617cbf78833f0ebc5bb488dec00e71159", + "inputs/7277-WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "inputs/7314-HELPERS.json.gz": "535c1461f1f2cbc3010c2111f3c6244e19e127630f1e4f208bd24c559bc83b4d", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "receipts/COMPARE.json": "e77bace53d794ee9d68eee8ad20dd12ff1b48a99c5100e356bd02c6ba1787ac4", + "receipts/FORWARD.json": "7ef82a94baec5e5ede8af38bc9172739f0cff24be94f8d4c3c5bc4e877768805", + "receipts/PRICE.json": "005efb8329d38638800d82e5273580b1bb529ac490d9923ba1a92e112d31c8b1", + "receipts/REVERSE.json": "97e6272c27714065c382360eb2a7a26209a13bf13a568ca4a643d46ec4b7889d" +} diff --git a/research/p104-public-four-move-rechart-bound/NOTICE b/research/p104-public-four-move-rechart-bound/NOTICE new file mode 100644 index 0000000000..9d3977d114 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. + +Exact words and caller from #7277, #7334 and #7113. Contact and role +receipts from #7312, #7319 and #7339. Directed tariff from #7298. +Related methods from #7337, #7297, #7122 and #7325. +OpenAI Codex and subagents materially assisted. diff --git a/research/p104-public-four-move-rechart-bound/PROOF.md b/research/p104-public-four-move-rechart-bound/PROOF.md new file mode 100644 index 0000000000..c36012ef33 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/PROOF.md @@ -0,0 +1,24 @@ +# Fixed-route common chart obstruction + +## Literal scope + +For each eligible public ADD, the incoming and outgoing contacts of each operand are its own paid ascending MOVEs. Write their chart paths as A₁→B→C₁ and A₂→B→C₂. The ADD at B is their only intervening incident event. Both original role assignments, its rational coefficient, all four MOVE clocks, the ADD clock, and the two routes' outer charts stay fixed. + +The predecessor is exact #7277 `ed090b57ed88f8859e5ff4643645099e6ba856ea`. The checks reproduce the literal ADD, including its sign, operand order, coefficient and chart. On exact #7334 they match the same ADD occurrence and every incoming and outgoing contact and confirm the same relative order of the five events. Source and destination accesses of ADD and COPY count as contacts. The role filter excludes the main/hosted roles, the known changed block and other protected roles. The scope is the nine prepriced inherited keys. + +If a replacement chart E existed, the MOVE quotient from A to E followed by E to C would compose to the same exact chart quotient A→C. The cocharted ADD has the same normalized action on arbitrary dirty arrays when both operands share E. No scalar value is assumed zero. A changed signed chart descriptor would still require its phase, all-width compiler and complete tape binding. The necessary span gate closes before that obligation. + +## Exact span test + +A legal positive-rank pair requires `A_i ⊊ E ⊊ C_i` for both operands. Therefore +`L = A₁ + A₂ ⊆ E ⊆ U = C₁ ∩ C₂`. Conversely, if the desired rank lies between dim L and dim U and all four rank gaps are positive, an abstract subspace E of that rank exists by extending a basis of L inside U. This equivalence is solely a geometry condition. + +All nine cases have `dim L = dim B = dim U = 4`. Since the original B already lies between L and U, both equal B as a subspace. Thus even a new abstract rank-five chart is unavailable. The primary records all basis certificates, including a direct high intersection and the equality `dim U = dim C₁ + dim C₂ − dim(C₁+C₂)`. The independent method walks the contacts in reverse and reconstructs the intersection and union from complete finite GF(2) sets. Both agree on all nine keys and no cap is hit. + +For example, ancestor ADD clock 38408 maps to current clock 38420, where the literal event is `ADD 1059,1427,−1,725`. Its four current MOVEs are 38418 and 41815 on role 1059, and 38419 and 41219 on role 1427. The high charts 861 and 883 each have rank six and their sum has rank eight. Their intersection has basis `[25,102,136,290]`, the exact old chart 725 span. The priced +1 rank is impossible. + +## Paid moment + +Let p_i and q_i be the old incoming and outgoing ranks on each operand. A shift by δ replaces them by `p_i+δ,q_i−δ`, both positive. The full 17-copy gross credit is +`17 Σ_i(H_(p_i)+H_(q_i)−H_(p_i+δ)−H_(q_i−δ))`, +where `H_r=r^(1−κ)`. Paid count and rank mass are fixed, and all target terms are fixed. The exact directed preprice checks every legal rank offset in the inherited scope. The compatible upper grants all ancillary costs free and credits each old MOVE at most once. All nine positive keys happen to use disjoint old paid MOVE clocks. With no feasible midpoint, the compatible saving is zero. No changed supplier or complete candidate was built. diff --git a/research/p104-public-four-move-rechart-bound/PROVENANCE.json b/research/p104-public-four-move-rechart-bound/PROVENANCE.json new file mode 100644 index 0000000000..4c78677935 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/PROVENANCE.json @@ -0,0 +1,53 @@ +{ + "files": { + "inputs/7277-WORD.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "077bf48c35db0ddafae81f1bfa0ffacc30894b2b", + "path": "research/p104-terminal-cut-rechart/WORD.json.gz", + "sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz", + "uncompress": false + }, + "inputs/7334-CHANGED.json": { + "commit": "4b958b057e133e92a5c3a07f1fb489c626dc2525", + "git_blob": "b1644106d97cdadfabb729dd4625adb4a77c20a0", + "path": "research/p104-retimed-chart207-split-bound/inputs/IDENTITIES.json", + "sha256": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/4b958b057e133e92a5c3a07f1fb489c626dc2525/research/p104-retimed-chart207-split-bound/inputs/IDENTITIES.json", + "uncompress": false + }, + "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/CrocSwap/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "generated": { + "inputs/7277-SUPPORT.json.gz": { + "commit": "09af2cd99a17cc9cfac49af21868c2082d77efde", + "manifest_path": "research/p104-public-move-fusion-contact-bound/receipts/SHA256.json", + "receipt_key": "scalar-silence/SUPPORT.json", + "receipt_sha256": "32d05c4efa4c3f6e3cf08fc9dd21478e0fb5218a38556e290966e64193fe2d80", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/09af2cd99a17cc9cfac49af21868c2082d77efde/research/p104-public-move-fusion-contact-bound/receipts/SHA256.json" + }, + "inputs/7314-HELPERS.json.gz": { + "commit": "b2d3bc4dd584f8d3aacd244505b12286db4d4875", + "manifest_path": "research/p104-helper-entrance-first-contact-bound/receipts/SHA256.json", + "receipt_key": "REVERSE.json", + "receipt_sha256": "bf353b3e05d0bf5fe3e49c15673c4cb9203251329bd594009303541cf7fecc09", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/b2d3bc4dd584f8d3aacd244505b12286db4d4875/research/p104-helper-entrance-first-contact-bound/receipts/SHA256.json" + } + }, + "schema_version": 1 +} diff --git a/research/p104-public-four-move-rechart-bound/README.md b/research/p104-public-four-move-rechart-bound/README.md new file mode 100644 index 0000000000..8a2a0340ec --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/README.md @@ -0,0 +1,35 @@ +# Public ADD recharts with four fixed MOVE clocks + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** All nine profitable inherited public-helper rechart keys match the signed ADD and the four immediate paid MOVE contacts on exact [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334). Each fixed cochart interval contains only its original rank-four subspace. The priced rank-five alternatives are impossible. Both independent walks exhaust their scope with zero survivors, zero unresolved ancestry and zero unvisited keys. + +The independently reproduced comparison is #7334 at `aaeec8c0acf01e99a5f331ef363a698d9c084ace`, κ 0.00364665195644, with exact [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) signed caller `07a76c5e2738882c0cb322278e56f6cae3c9885d`. The scope retains both public productive helpers, the original nonzero ADD coefficient and operand order, all five original clocks, the four outer charts and both productive boundaries. It starts from inherited #7277 keys. Newly created current-word shapes are outside the enumeration. [Proof](PROOF.md) + +## Complete price before support + +The inherited #7312 receipt gives 4,732 public consecutive MOVE windows. Exactly 184 ADD clocks are the sole intervening contact in both public operands' windows. Restricting both roles to unprotected productive helpers gives 48 pairs. The predecode directed price retains nine profitable rank-offset choices. Paid positions remain 110,519, productive positions 22,461, signed rank surplus 1,424 and empty credit zero. + +The one-edit gross upper is about 0.05315269560459226 raw at the incumbent crossing. The no-double-counting bound for all nine keys is about 0.39474780129390424 before ancillary charges. At fixed κ 0.0040075385047236 the complete upper margin is below −139.3333857837905. The exact price receipt preserves the directed rational bounds. Geometry reduces the compatible saving to zero. + +## Replay + +Use CPython 3.12 with assertions and the standard library. From a clean repository checkout: + +~~~sh +python3.12 -B scripts/research_package.py --package research/p104-public-four-move-rechart-bound +~~~ + +From the package directory or a Git-free export: + +~~~sh +python3.12 -I -B replay.py --out fresh-receipts +~~~ + +The standalone replay authenticates both exact word inputs and predecessor receipts, recomputes the complete price before either word is decoded, runs both contact and rank checks, and reconciles all nine signed literal correspondences. It matches four plaintext receipts byte for byte and rejects mutations of the price and both word inputs. [Verification and source pins](VERIFICATION.md) + +## Open next questions + +A different outer route could enlarge one interval, and later source edits may have introduced new public contact shapes. Start by pinning one exact changed route and pricing all its paid and ordinary work before checking span and signed phase. The current whole-stock upper is below the cost of one additional raw paid rank-one position. + +## Attribution + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) and [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) supply the comparator and caller. [#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277), [#7312](https://github.com/CrocSwap/integer-mult-bounds/pull/7312) and [#7319](https://github.com/CrocSwap/integer-mult-bounds/pull/7319) supply the predecessor word, ordered contact evidence and helper cohort. [#7339](https://github.com/CrocSwap/integer-mult-bounds/pull/7339) supplies the changed-role protection record, [#7337](https://github.com/CrocSwap/integer-mult-bounds/pull/7337) the mixed-role incidence method, and [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) the directed tariff. [#7297](https://github.com/CrocSwap/integer-mult-bounds/pull/7297), [#7122](https://github.com/CrocSwap/integer-mult-bounds/pull/7122) and [#7325](https://github.com/CrocSwap/integer-mult-bounds/pull/7325) supply related owned-contact, global-rechart and concave-price precedents. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-public-four-move-rechart-bound/SOURCES.json b/research/p104-public-four-move-rechart-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-public-four-move-rechart-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-public-four-move-rechart-bound/TASK.json b/research/p104-public-four-move-rechart-bound/TASK.json new file mode 100644 index 0000000000..25c24d229d --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "On exact #7334, rechart one existing ADD between public productive helpers, retaining all four incident paid MOVE clocks, both strict monotone itineraries' outer charts, coefficient, roles and outputs. Price only the nine profitable inherited #7277 keys.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 public cochart rechart research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A more polarized four-rank paid profile at fixed count, paid rank mass and targets could improve the binding signed complex invoice.", + "budget_minutes": 8, + "evidence": "Two exact walks match the original signed ADD and four immediate MOVE contacts for all nine keys. The low union and high intersection equal the original rank-four midpoint for each. All demanded rank-five alternatives fail.", + "open_questions": [ + { + "blocked_by": "All nine inherited fixed-route intervals collapse to the existing rank-four chart and added rank-one work exceeds the entire priced stock.", + "first_step": "Pin one four-MOVE signature and price every additional route or rank change before an exact span test.", + "question": "Can a different outer route create one larger cochart at positive complete price?", + "why_it_matters": "The exact interval is frozen only by the two retained endpoint routes." + } + ], + "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": "Changes the four paid rank labels without changing productive targets or paid count, in the public-public complement of the mixed #7337 gate.", + "scope_status": "changed", + "stop_rule": "Exhaust nine prepriced inherited keys or 20 runner seconds. Build only if a midpoint passes exact geometry and subsequent signed binding.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-public-four-move-rechart-bound/VERIFICATION.md b/research/p104-public-four-move-rechart-bound/VERIFICATION.md new file mode 100644 index 0000000000..9106f8a787 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/VERIFICATION.md @@ -0,0 +1,29 @@ +# Verification and exact sources + +The exact compressed #7334 word has SHA-256 +`4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a`. +The exact compressed #7277 predecessor has SHA-256 +`2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756`. +The exact historical support and helper cohort payloads are matched to +the public #7312 and #7319 replay hash manifests. [PROVENANCE.json](PROVENANCE.json) +records the exact commit and path for each and the Git blobs for the +vendored word, tariff and changed-role sources. [LOCAL-PINS.json](LOCAL-PINS.json) +pins every scientific input, engine and receipt by package-relative path. +The prior #7334 admission and full signed price readback are included as +immutable comparison receipts. The present replay checks the new +preprice and finite geometry, using that prior admitted comparator. + +The original source-bound price took 0.30 s. The forward and reverse +literal runs took 0.10 s and 0.11 s under a nine-case and 20-second cap. +The relocated replays took 0.12 s and 0.09 s and matched byte for byte. +Both replays use CPython 3.12.14, isolated mode and assertions. The +standalone runner regenerates the price, forward, reverse and +comparison receipts from clean relative inputs. It rejects a changed +byte in the price, current word and ancestor word separately. +Synthetic controls cover an expanded intersection, a saturated +intersection, a low-union obstruction, an abstract new descriptor, +and an intervening source read. + +A changed native word, signed chart supplier, precision/tape and +outer recurrence replay were not needed because every case was +excluded at geometry. Hosted checks are separate. diff --git a/research/p104-public-four-move-rechart-bound/VERIFY.json b/research/p104-public-four-move-rechart-bound/VERIFY.json new file mode 100644 index 0000000000..e4d82c71a6 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/VERIFY.json @@ -0,0 +1,14 @@ +{ + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/replay.py"], + "checks": "Rebuild the complete preprice, match exact inherited ADD and MOVE order in two independent walks, reproduce all nine GF(2) certificates and reject changed source bytes.", + "timeout_seconds": 90 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-public-four-move-rechart-bound/engines/compare.py b/research/p104-public-four-move-rechart-bound/engines/compare.py new file mode 100644 index 0000000000..2907b3c86a --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/engines/compare.py @@ -0,0 +1,50 @@ +"""Reconcile the exact frozen R88 contact and rank decisions.""" +from argparse import ArgumentParser +from fractions import Fraction +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +PINS={ + "lead":"7ef82a94baec5e5ede8af38bc9172739f0cff24be94f8d4c3c5bc4e877768805", + "independent":"97e6272c27714065c382360eb2a7a26209a13bf13a568ca4a643d46ec4b7889d", +} + + +def main(): + p=ArgumentParser(description=__doc__) + for name in PINS: + p.add_argument(name,type=Path) + args=p.parse_args() + docs=[] + for name,pin in PINS.items(): + raw=getattr(args,name).read_bytes() + assert sha256(raw).hexdigest()==pin, f"Changed receipt {name}" + docs.append(loads(raw)) + lead,ind=docs + assert lead["head"]==ind["head"] and lead["ancestor_head"]==ind["predecessor_head"] + assert not any((lead["unresolved"],ind["unresolved"],lead["unvisited"],ind["unvisited"], + lead["survivors"],ind["survivors"])) + ranks=[] + for a,b in zip(lead["outcomes"],ind["decisions"],strict=True): + assert a["key"]==b["key"] and a["ancestor_ADD_clock"]==b["legacy_add_clock"] + assert a["current_ADD_clock"]==b["current_add_clock"] + assert a["ancestor_relative_order"]==a["current_relative_order"]==b["legacy_order"] + assert [a["ancestor_MOVE_clocks"][str(r)] for r in b["roles"]]==b["legacy_move_clocks"] + assert [a["current_MOVE_clocks"][str(r)] for r in b["roles"]]==b["current_move_clocks"] + assert a["literal_ADD"]==["ADD",*b["literal_add"]] + cert=a["geometry_certificate"] + assert cert["wanted_rank"]==b["required_rank"]==5 + assert cert["low_union_rank"]==b["low_union_rank"]==4 + assert cert["high_intersection_rank"]==b["high_intersection_rank"]==4 + assert a["status"]==b["status"]=="high_intersection_too_small" + assert Fraction(a["gross_at_incumbent"][1])==Fraction(b["directed_gross_upper"]) + ranks.append([a["key"],b["current_add_clock"],4,5]) + assert len(ranks)==9 + print(dumps(dict(head=lead["head"],pins=PINS,exact_key_agreements=9, + exact_rank_intervals_collapsed_to_old_span=9,geometry_survivors=0,unresolved=0,rows=ranks), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-public-four-move-rechart-bound/engines/quote.py b/research/p104-public-four-move-rechart-bound/engines/quote.py new file mode 100644 index 0000000000..ea6824f05a --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/engines/quote.py @@ -0,0 +1,172 @@ +"""Preprice one shared public ADD chart on the sealed #7277 ancestry stock.""" + +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +PINS = { + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/7314-HELPERS.json": "bf353b3e05d0bf5fe3e49c15673c4cb9203251329bd594009303541cf7fecc09", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "inputs/7277-SUPPORT.json.gz": "a63d766dce9ccc5b7a97057fb298350617cbf78833f0ebc5bb488dec00e71159", +} +SUPPORT_PAYLOAD = "32d05c4efa4c3f6e3cf08fc9dd21478e0fb5218a38556e290966e64193fe2d80" +COMPARATOR = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PREDECESSOR = "ed090b57ed88f8859e5ff4643645099e6ba856ea" + + +def unique(rows): + data = dict(rows) + if len(rows) != len(data): + raise ValueError("duplicate input key") + return data + + +def interval(x): + return list(map(str, x)) + + +def matching(rows, point): + # Price variants of one contact share all four old paid clocks. + moves = [set(k for row in r["operands"] for k in row["moves"]) for r in rows] + forbidden = [sum(1 << j for j, right in enumerate(moves) if left & right) for left in moves] + weights = [Q(r[point][1]) for r in rows] + + @cache + def best(remaining): + if not remaining: + return Q(0), () + low = remaining & -remaining + index = low.bit_length() - 1 + value, chosen = best(remaining & ~forbidden[index]) + return max(best(remaining ^ low), (value + weights[index], (index, *chosen))) + + upper, indexes = best((1 << len(rows)) - 1) + return {"directed_upper": str(upper), "maximizing_keys": [rows[i]["key"] for i in indexes]} + + +def main(): + assert __debug__ + raw = {} + for name, pin in PINS.items(): + raw[name] = (ROOT / name).read_bytes() + if sha256(raw[name]).hexdigest() != pin: + raise ValueError(f"changed dependency {name}") + + def read(name): + return loads(raw[f"inputs/{name}.json"], object_pairs_hook=unique) + + base, admission = read("READBACK"), read("ADMITTED") + helper, changed = read("7314-HELPERS"), read("7334-CHANGED") + assert base["head"] == admission["head"] == COMPARATOR + assert admission["exit"] == 0 and admission["status"] == "independently_reproduced_comparable" + assert base["caller_head"] == admission["caller"] + assert helper["complete"] and len(helper["rows"]) == 1101 and len(changed["roles"]) == 14 + helpers = {r["role"] for r in helper["rows"]} + protected = set(changed["roles"]) | {863,1355,1531,1567,1568} + assert 319 in protected and len(helpers) == 1101 + support = decompress(raw["inputs/7277-SUPPORT.json.gz"]) + assert sha256(support).hexdigest() == SUPPORT_PAYLOAD + inherited = loads(support, object_pairs_hook=unique) + assert inherited["head"] == PREDECESSOR and inherited["scope_exhausted"] + assert len(inherited["records"]) == 4732 + + paired = defaultdict(list) + for row in inherited["records"]: + if len(row["contacts"]) == 1 and row["scalar_evidence"] == [[row["contacts"][0], "nonzero_add_source"]]: + paired[row["contacts"][0]].append(row) + assert max(map(len, paired.values())) == 2 + paired = {clock:rows for clock,rows in paired.items() if len(rows) == 2} + assert len(paired) == 184 + + def histogram(x): + return Counter({int(rank): n for rank,n in x.items()}) + + paid, targets = histogram(base["paid"]), histogram(base["targets"]) + old = targets.copy() + old.subtract(paid) + assert base["copies"] == 17 + assert (sum(paid.values()),sum(targets.values()),sum(r*n for r,n in old.items())) == (110519,22461,1424) + assert base["empty_root_credits"] == 0 + cost = run_path(str(ROOT / "inputs/pricing.py"))["cost"] + at = Q(base["new_raw_interval"][1]) + probe = at + Q(1,10**9) + target = Q("0.0040075385047236") + assert cost(old, at)[1] < 0 + + eligible = positive_legacy = 0 + out, unresolved = [], [] + for clock, operands in sorted(paired.items()): + operands = sorted(operands, key=lambda x:x["role"]) + roles = {x["role"] for x in operands} + assert len(roles) == 2 and operands[0]["charts"][1] == operands[1]["charts"][1] + assert len({t for x in operands for t in x["moves"]}) == 4 + allowed = roles <= helpers and not roles & protected + eligible += allowed + old_left = [x["ranks"][0] for x in operands] + old_right = [x["ranks"][1] for x in operands] + for offset in range(1-min(old_left), min(old_right)): + if not offset: + continue + rank_shift = Counter() + for p,q in zip(old_left, old_right, strict=True): + rank_shift[p+offset] += 17 + rank_shift[q-offset] += 17 + rank_shift[p] -= 17 + rank_shift[q] -= 17 + assert sum(rank_shift.values()) == sum(r*n for r,n in rank_shift.items()) == 0 + paid_delta = {r:n for r,n in sorted(rank_shift.items()) if n} + if not paid_delta: + continue + credit = {r:-n for r,n in paid_delta.items()} + saving = cost(credit, at) + if saving[1] <= 0: + continue + if saving[0] <= 0: + unresolved.append([clock,offset]) + continue + positive_legacy += 1 + if not allowed: + continue + new = old.copy() + new.subtract(paid_delta) + assert cost(new,probe)[0] > 0 + out.append({ + "key":[clock,offset], + "operands":[{k:x[k] for k in ("role","moves","charts","ranks")} for x in operands], + "paid_delta":paid_delta, "target_delta":{}, "delta_midpoint_rank":offset, + "gross_at_incumbent":interval(saving), "gross_at_moonshot":interval(cost(credit,target)), + "complete_margin_at_incumbent":interval(cost(new,at)), + "complete_margin_at_probe":interval(cost(new,probe)), + }) + assert positive_legacy == 20 and 0 < len(out) <= positive_legacy and not unresolved + out.sort(key=lambda r:(-Q(r["gross_at_incumbent"][0]),r["key"])) + current_whole = matching(out,"gross_at_incumbent") + target_whole = matching(out,"gross_at_moonshot") + margin_at_target = cost(old,target)[1] + Q(target_whole["directed_upper"]) + assert margin_at_target < 0 + print(dumps({ + "head":COMPARATOR, "caller_head":admission["caller"], + "word_sha256":admission["inputs"]["WORD.json.gz"], "predecessor_head":PREDECESSOR, + "input_sha256":PINS, "legacy_payload_sha256":SUPPORT_PAYLOAD, + "old_crossing_upper":str(at), "price_probe":str(probe), "fixed_moonshot":str(target), + "old_complete_margin":interval(cost(old,at)), "old_moonshot_margin":interval(cost(old,target)), + "moonshot_complete_margin_upper":str(margin_at_target), + "legacy_two_public_move_neighbors":len(paired), "allowed_helper_pairs":eligible, + "positive_legacy_before_protection":positive_legacy, "protected_roles":sorted(protected), + "first_case_cap":20, "first_runner_seconds":20, "build_cap":1, "price_unresolved":unresolved, + "whole_compatible_at_incumbent":current_whole, "whole_compatible_at_moonshot":target_whole, + "alternatives":out, "scope":"Exact inherited #7277 one-ADD/four-MOVE signatures, restricted to unprotected productive helpers. No current word or span decoded." + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-public-four-move-rechart-bound/engines/rechart_gate.py b/research/p104-public-four-move-rechart-bound/engines/rechart_gate.py new file mode 100644 index 0000000000..8af8107373 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/engines/rechart_gate.py @@ -0,0 +1,337 @@ +"""Exact inherited public ADD contact and GF(2) chart-rank gate.""" + +from argparse import ArgumentParser +from bisect import bisect_left +from collections import Counter +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 alarm +from time import monotonic + +PRICE = "preflight/PRICE.json" +WORD = "preflight/inputs/7334-WORD.json.gz" +ANCESTOR = "lead/inputs/7277-WORD.json.gz" +PINS = { + PRICE: "005efb8329d38638800d82e5273580b1bb529ac490d9923ba1a92e112d31c8b1", + WORD: "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + ANCESTOR: "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", +} +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +ANCESTOR_HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +CASE_CAP, HARD_SECONDS, SOFT_SECONDS = 9, 20, 18 + + +class DeadlineReached(Exception): + """The cooperative gate stopped before resolving a frozen key.""" + + +def check_time(deadline): + if monotonic() >= deadline: + raise DeadlineReached + + +def unique(pairs): + obj = dict(pairs) + if len(obj) != len(pairs): + raise ValueError("duplicate JSON key") + return obj + + +def authenticate(root): + raw = {} + for relative, pin in PINS.items(): + raw[relative] = (root / relative).read_bytes() + if sha256(raw[relative]).hexdigest() != pin: + raise ValueError(f"changed dependency {relative}") + return raw + + +def contacts(word, tracked, deadline): + tape = word["program"] + public = word["public"] + initial, final = word["initial"], word["final"] + active = {role: initial[role] for role in tracked} + index = {role: [] for role in tracked} + for clock, event in enumerate(tape): + if clock % 256 == 0: + check_time(deadline) + opcode, dst = event[:2] + if opcode == "MOVE": + if dst in index: + a, b, owned = event[2:] + assert dst < public and owned is False and active[dst] == a + active[dst] = b + index[dst].append(clock) + elif opcode in ("ADD", "COPY", "SCALE"): + roles = event[1:3] if opcode in ("ADD", "COPY") else event[1:2] + for role in roles: + if role in index: + assert active[role] == event[-1] + index[role].append(clock) + else: + assert opcode in ("INIT", "CLEAR") and dst not in index + assert all(active[role] == final[role] for role in tracked) + return index + + +def expected_moves(operand): + r = operand["role"] + a, b, c = operand["charts"] + return ["MOVE", r, a, b, False], ["MOVE", r, b, c, False] + + +def incident_neighbors(tape, index, role, clock): + row = index[role] + k = bisect_left(row, clock) + assert k < len(row) and row[k] == clock + return [ + [row[k - 1], tape[row[k - 1]]] if k else None, + [row[k + 1], tape[row[k + 1]]] if k + 1 < len(row) else None, + ] + + +def clock_order(add, pairs): + named = [(add, "ADD")] + for role, (a, b) in pairs.items(): + named.extend(((a, f"{role}:in"), (b, f"{role}:out"))) + assert len({clock for clock, _ in named}) == 5 + return [name for _, name in sorted(named)] + + +def identify(old, now, old_index, now_index, row): + old_tape, now_tape = old["program"], now["program"] + old_add, _ = row["key"] + operands = row["operands"] + roles = [x["role"] for x in operands] + add = old_tape[old_add] + assert add[0] == "ADD" and set(add[1:3]) == set(roles) and Fraction(add[3]) + assert add[-1] == operands[0]["charts"][1] == operands[1]["charts"][1] + old_moves = {x["role"]: x["moves"] for x in operands} + for operand in operands: + r = operand["role"] + expected = expected_moves(operand) + a, b = old_moves[r] + assert a < old_add < b + assert incident_neighbors(old_tape, old_index, r, old_add) == [[a, expected[0]], [b, expected[1]]] + + # The protected-role filter excludes the sources of changed public-public + # contacts in #7314 and #7334. Equal literal contacts retain their order. + same_old = [k for k in old_index[roles[0]] if old_tape[k] == add] + same_now = [k for k in now_index[roles[0]] if now_tape[k] == add] + old_ordinal = same_old.index(old_add) + evidence = { + "literal_ADD": add, "ancestor_ADD_clock": old_add, "ancestor_MOVE_clocks": old_moves, + "ancestor_exact_ADD_clocks": same_old, "current_exact_ADD_clocks": same_now, + "ancestor_exact_ADD_ordinal": old_ordinal, + } + if not same_now: + return "missing_inherited_literal_ADD", evidence + if len(same_old) != len(same_now): + return "unresolved_ancestry_ordinal", evidence + + current_add = same_now[old_ordinal] + neighbors = {r: incident_neighbors(now_tape, now_index, r, current_add) for r in roles} + evidence |= {"current_ADD_clock": current_add, "current_incident_neighbors": neighbors} + current_moves = {} + for operand in operands: + r = operand["role"] + incoming, outgoing = neighbors[r] + expected = expected_moves(operand) + if not incoming or not outgoing or incoming[1] != expected[0] or outgoing[1] != expected[1]: + return "missing_inherited_immediate_MOVE_pair", evidence + current_moves[r] = [incoming[0], outgoing[0]] + + old_order = clock_order(old_add, old_moves) + now_order = clock_order(current_add, current_moves) + evidence |= {"current_MOVE_clocks": current_moves, "ancestor_relative_order": old_order, + "current_relative_order": now_order} + if old_order != now_order: + return "changed_inherited_clock_order", evidence + charts = {c for operand in operands for c in operand["charts"]} + if any(old["frames"][c] != now["frames"][c] for c in charts): + return "unresolved_chart_payload", evidence + return "contact_match", evidence + + +def space(vectors): + elements = {0} + for v in vectors: + assert type(v) is int and 0 <= v < 512 + if v not in elements: + elements |= {v ^ x for x in elements} + return elements + + +def basis(elements): + vectors = [] + span = {0} + for x in sorted(elements): + if x not in span: + vectors.append(x) + span |= {x ^ y for y in span} + assert span == elements + return vectors + + +def dimensions(elements): + size = len(elements) + rank = size.bit_length() - 1 + assert size == 1 << rank + return rank + + +def geometry(frames, chart_paths, old_ranks, offset, deadline): + check_time(deadline) + (a, b, c), (d, middle, e) = chart_paths + assert b == middle and offset + frame = {i: frames[i] for i in {a,b,c,d,e}} + spans = {i: space(vectors) for i, vectors in frame.items()} + rank = {i: dimensions(value) for i, value in spans.items()} + assert all(rank[i] == len(frame[i]) for i in frame) + assert spans[a] < spans[b] < spans[c] and spans[d] < spans[b] < spans[e] + assert old_ranks == [[rank[b] - rank[a], rank[c] - rank[b]], [rank[b] - rank[d], rank[e] - rank[b]]] + low = space(frame[a] + frame[d]) + high = spans[c] & spans[e] + high_sum = space(frame[c] + frame[e]) + assert low <= spans[b] <= high + low_dim, high_dim, high_sum_dim = map(dimensions, (low, high, high_sum)) + assert high_dim == rank[c] + rank[e] - high_sum_dim + wanted = rank[b] + offset + new_ranks = [[wanted-rank[a], rank[c]-wanted], [wanted-rank[d], rank[e]-wanted]] + assert new_ranks == [[p+offset,q-offset] for p,q in old_ranks] and min(sum(new_ranks, [])) > 0 + certificate = { + "chart_bases": frame, "chart_ranks": rank, "wanted_rank": wanted, + "low_union_basis": basis(low), "low_union_rank": low_dim, + "high_intersection_basis": basis(high), "high_intersection_rank": high_dim, + "high_sum_basis": basis(high_sum), "high_sum_rank": high_sum_dim, + "new_paid_ranks": new_ranks, + } + if wanted < low_dim: + return "low_union_too_large", certificate + if wanted > high_dim: + return "high_intersection_too_small", certificate + + for i, f in enumerate(frames): + if i % 32 == 0: + check_time(deadline) + if len(f) == wanted and all(x in high for x in f): + s = space(f) + if len(s) == 1 << wanted and low <= s: + certificate["midpoint"] = {"kind": "existing_chart", "chart": i, "basis": f} + break + else: + constructed = basis(low) + current = low.copy() + for x in sorted(high): + if len(constructed) == wanted: + break + if x not in current: + constructed.append(x) + current |= {x ^ y for y in current} + assert len(constructed) == wanted and low <= current <= high + certificate["midpoint"] = {"kind": "new_descriptor_pending_compiler", "basis": constructed} + return "exact_geometry_survivor", certificate + + +def controls(): + paths, old = [[0,1,2],[0,1,3]], [[1,2],[1,2]] + start = monotonic() + expand = [[], [1], [1,2,4], [1,2,8], [1,2]] + status, r = geometry(expand,paths,old,1,start+2) + assert status == "exact_geometry_survivor" and r["midpoint"]["chart"] == 4 + saturated = [[], [1], [1,2,4], [1,8,16]] + status, r = geometry(saturated,paths,old,1,start+2) + assert status == "high_intersection_too_small" and r["high_intersection_basis"] == [1] + new = expand[:-1] + status, r = geometry(new,paths,old,1,start+2) + assert status == "exact_geometry_survivor" and r["midpoint"]["basis"] == [1,2] + w = {"public":3,"initial":[0,0,1],"final":[2,3,1],"frames":expand, + "program":[["MOVE",0,0,1,False],["MOVE",1,0,1,False],["ADD",0,1,"-2",1], + ["MOVE",0,1,2,False],["MOVE",1,1,3,False]]} + row = {"key":[2,1],"operands":[{"role":0,"moves":[0,3],"charts":paths[0]}, + {"role":1,"moves":[1,4],"charts":paths[1]}]} + n = w | {"program":w["program"][:2]+[["ADD",2,1,"1",1]]+w["program"][2:]} + old_index, now_index = [contacts(x,{0,1},start+2) for x in (w,n)] + status, evidence = identify(w,n,old_index,now_index,row) + assert status == "missing_inherited_immediate_MOVE_pair" + assert evidence["current_incident_neighbors"][1][0] == [2,["ADD",2,1,"1",1]] + return ["expanded_high_intersection", "saturated_high_intersection", + "deterministic_new_descriptor", "intervening_source_read_blocks_contact"] + + +def helpers(word): + mains = set(word["live"]) | {r+112 for r in word["live"]} + mains.update(word["hosted"]["X2"], word["hosted"]["Y2"]) + assert len(mains) == 400 and word["public"] == 1501 + return set(range(word["public"])) - mains + + +def audit(raw, deadline): + price = loads(raw[PRICE], object_pairs_hook=unique) + assert price["head"] == HEAD and price["predecessor_head"] == ANCESTOR_HEAD and price["word_sha256"] == PINS[WORD] + assert not price["price_unresolved"] and price["first_runner_seconds"] == HARD_SECONDS + cases = price["alternatives"] + assert len(cases) == CASE_CAP and len({tuple(row["key"]) for row in cases}) == CASE_CAP + outcomes, visited = [], 0 + stage = "decode" + try: + old, now = [loads(decompress(raw[rel]), object_pairs_hook=unique) for rel in (ANCESTOR, WORD)] + stage = "contact_index" + tracked = {operand["role"] for row in cases for operand in row["operands"]} + assert tracked <= helpers(old) & helpers(now) and not tracked & set(price["protected_roles"]) + old_index, now_index = [contacts(w,tracked,deadline) for w in (old,now)] + stage = "nine_frozen_keys" + for row in cases: + check_time(deadline) + status, evidence = identify(old,now,old_index,now_index,row) + if status == "contact_match": + status, certificate = geometry(now["frames"],[x["charts"] for x in row["operands"]], + [x["ranks"] for x in row["operands"]], + row["delta_midpoint_rank"], deadline) + evidence["geometry_certificate"] = certificate + outcomes.append({"key": row["key"], "status": status, + "gross_at_incumbent": row["gross_at_incumbent"], **evidence}) + visited += 1 + except DeadlineReached: + pass + unvisited = [{"key": row["key"],"gross_at_incumbent":row["gross_at_incumbent"]} for row in cases[visited:]] + unresolved = [r["key"] for r in outcomes if r["status"].startswith("unresolved")] + survivors = [r["key"] for r in outcomes if r["status"] == "exact_geometry_survivor"] + return { + "head":HEAD, "ancestor_head":ANCESTOR_HEAD, "input_sha256":PINS, + "price_sha256":PINS[PRICE], "word_sha256":PINS[WORD], + "status":"CAPPED" if unvisited else "EXHAUSTED", "last_stage":stage, + "case_cap":CASE_CAP, "hard_seconds":HARD_SECONDS, "cooperative_seconds":SOFT_SECONDS, + "visited":visited, "unvisited":unvisited, "unresolved":unresolved, + "counts":dict(Counter(r["status"] for r in outcomes)), "survivors":survivors, "outcomes":outcomes, + "scope":"Nine frozen public-helper fixed-clock ADD recharts, exact ancestor ordinal and current contact topology, then exact GF(2) rank.", + } + + +def main(): + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("root", type=Path, nargs="?") + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + if args.controls_only: + print(dumps({"controls": controls()}, sort_keys=True)) + return + if args.root is None: + parser.error("the R88 evidence root is required") + alarm(HARD_SECONDS) + deadline = monotonic() + SOFT_SECONDS + raw = authenticate(args.root) + checked = controls() + result = audit(raw, deadline) + result["controls"] = checked + print(dumps(result, sort_keys=True, indent=2)) + alarm(0) + + +if __name__ == "__main__": + main() diff --git a/research/p104-public-four-move-rechart-bound/engines/reverse_geometry.py b/research/p104-public-four-move-rechart-bound/engines/reverse_geometry.py new file mode 100644 index 0000000000..26a2d39c2e --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/engines/reverse_geometry.py @@ -0,0 +1,293 @@ +"""Reverse contact reconciliation and exhaustive GF(2) rank geometry for R88.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from itertools import pairwise +from json import dumps, loads +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +OLD_HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +PINS = { + "price": "005efb8329d38638800d82e5273580b1bb529ac490d9923ba1a92e112d31c8b1", + "word": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "legacy": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", +} +CURRENT_PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("Duplicate JSON key") + return result + + +def checked(path, key): + raw = path.read_bytes() + if sha256(raw).hexdigest() != PINS[key]: + raise ValueError(f"Changed input {key}") + if key != "price": + raw = decompress(raw) + if key == "word": + assert sha256(raw).hexdigest() == CURRENT_PAYLOAD + return loads(raw, object_pairs_hook=unique) + + +def span(basis): + result = {0} + for v in basis: + assert isinstance(v,int) and 0 < v < 512 and v not in result + result.update(v^x for x in tuple(result)) + return result + + +def basis_for(space): + result = [] + obtained = {0} + for v in sorted(space): + if v not in obtained: + result.append(v) + obtained.update(v^x for x in tuple(obtained)) + assert obtained == space + return result + + +def dimension(space): + size = len(space) + assert size > 0 and size & (size-1) == 0 + return size.bit_length()-1 + + +def reach_interval(lo1, lo2, hi1, hi2, old_mid, target): + low = {a^b for a in lo1 for b in lo2} + high = hi1 & hi2 + assert low <= old_mid <= high + dim_lo,dim_hi = dimension(low),dimension(high) + return low,high,{ + "required_rank":target, "low_union_rank":dim_lo, "high_intersection_rank":dim_hi, + "low_union_basis":basis_for(low), "high_intersection_basis":basis_for(high), + "low_vector_count":len(low), "high_vector_count":len(high), + "status":"geometry_survivor" if dim_lo<=target<=dim_hi else + ("high_intersection_too_small" if target>dim_hi else "low_union_too_large"), + } + + +def incidence(event): + tag = event[0] + if tag in ("ADD","COPY"): + assert event[1] != event[2] + return event[1:3] + assert tag in ("MOVE","SCALE","INIT","CLEAR") + return event[1:2] + + +def contact_index(tape, roles, deadline): + result = {r:[] for r in roles} + for clock in range(len(tape)-1,-1,-1): + if clock%256 == 0 and monotonic()>=deadline: + raise TimeoutError("backwards literal contact index") + for role in incidence(tape[clock]): + if role in result: + result[role].append(clock) + return result + + +def route_contacts(tape, backwards, role, path): + found = {} + a,b,c = path + for after,clock,before in zip(backwards,backwards[1:],backwards[2:]): + assert before < clock < after + if tape[before] != ["MOVE",role,a,b,False] or tape[after] != ["MOVE",role,b,c,False]: + continue + event = tape[clock] + if event[0] == "ADD" and event[-1] == b: + found[clock]=(before,after) + return found + + +def signed_add(event): + op,dst,src,k,chart = event + assert op=="ADD" and dst!=src + coef = Fraction(k) + assert coef + return dst,src,coef,chart + + +def order_signature(clock, roles, legs): + positions = [(clock,"ADD")] + positions += [(t,f"{r}:{s}") for r,(i,j) in zip(roles,legs,strict=True) for t,s in ((i,"in"),(j,"out"))] + assert len({x[0] for x in positions})==5 + return [k for _,k in sorted(positions)] + + +def check_case(case, old, new, old_ix, new_ix): + old_tape,new_tape = old["program"],new["program"] + old_clock,delta = case["key"] + operands = case["operands"] + assert delta == case["delta_midpoint_rank"] and delta + roles = [x["role"] for x in operands] + paths = [x["charts"] for x in operands] + old_moves = [x["moves"] for x in operands] + midpoint = paths[0][1] + assert paths[1][1]==midpoint and len(roles)==len(set(roles))==2 + old_add = signed_add(old_tape[old_clock]) + assert set(old_add[:2])==set(roles) and old_add[3]==midpoint + for role,path,quoted in zip(roles,paths,old_moves,strict=True): + exact = route_contacts(old_tape,old_ix[role],role,path) + assert list(exact[old_clock]) == quoted + inherited_order = order_signature(old_clock,roles,old_moves) + + route_a,route_b = [route_contacts(new_tape,new_ix[role],role,path) for role,path in zip(roles,paths,strict=True)] + common = sorted(route_a.keys() & route_b.keys()) + signed_matches = [t for t in common if signed_add(new_tape[t])==old_add] + accepted = [] + for t in signed_matches: + legs = [route_a[t],route_b[t]] + if order_signature(t,roles,legs)==inherited_order: + accepted.append((t,legs)) + record = {"key":case["key"], "roles":roles, "legacy_add_clock":old_clock, + "legacy_move_clocks":old_moves,"legacy_order":inherited_order, + "literal_add":[old_add[0],old_add[1],str(old_add[2]),old_add[3]], + "common_chart_shape_clocks":common,"signed_matches":signed_matches, + "current_match_count":len(accepted),"paid_delta":case["paid_delta"], + "directed_gross_upper":case["gross_at_incumbent"][1]} + if not accepted: + return record | {"status":"inherited_topology_missing"} + if len(accepted)!=1: + return record | {"status":"ambiguous_inherited_topology", + "current_matching_tuples":[[t,*legs] for t,legs in accepted]} + clock,legs=accepted[0] + frames=new["frames"] + get=cache(lambda j:span(frames[j])) + low1,mid1,high1=paths[0] + low2,mid2,high2=paths[1] + assert get(mid1)==get(mid2) + fixed=[(get(a),get(b),get(c)) for a,b,c in paths] + old_ranks=[] + paid=Counter() + for (a,b,c), alt in zip(fixed,operands,strict=True): + assert a0 and q-delta>0 + old_ranks.append([p,q]) + paid[p] -= 17 + paid[q] -= 17 + paid[p+delta] += 17 + paid[q-delta] += 17 + paid={str(r):v for r,v in sorted(paid.items()) if v} + assert paid==case["paid_delta"] and not case["target_delta"] + assert Fraction(case["complete_margin_at_probe"][0]) > 0 + rank=dimension(get(midpoint))+delta + low,high,proof=reach_interval(get(low1),get(low2),get(high1),get(high2),get(midpoint),rank) + if proof["status"]=="geometry_survivor": + current_chart=next((i for i,v in enumerate(frames) if len(v)==rank and low<=get(i)<=high),None) + if current_chart is not None: + chosen=list(frames[current_chart]) + else: + chosen=basis_for(low) + seen=span(chosen) + for v in sorted(high): + if len(chosen)==rank: + break + if v not in seen: + chosen.append(v) + seen.update(v^w for w in tuple(seen)) + assert len(chosen)==rank and low<=span(chosen)<=high + proof["existing_chart"]=current_chart + proof["constructive_basis"]=chosen + return record|{"current_add_clock":clock,"current_move_clocks":legs, + "old_midpoint_rank":dimension(get(midpoint)),"old_paid_ranks":old_ranks, + "new_paid_ranks":[[p+delta,q-delta] for p,q in old_ranks], + "old_chart_paths":paths,**proof} + + +def controls(): + low1,low2=span([1]),span([2]) + mid=span([1,2]) + hi=span([1,2,4,8]) + success=reach_interval(low1,low2,hi,span([1,2,4,16]),mid,3)[2] + assert success["status"]=="geometry_survivor" and success["high_intersection_rank"]==3 + bad=reach_interval(low1,low2,hi,span([1,2,16,32]),mid,3)[2] + assert bad["status"]=="high_intersection_too_small" and bad["high_intersection_rank"]==2 + assert reach_interval(low1,low2,hi,hi,mid,1)[2]["status"]=="low_union_too_large" + + tape=[["MOVE",0,1,2,False],["ADD",0,1,"-3/2",2],["MOVE",0,2,3,False]] + ix=contact_index(tape,{0},float("inf")) + assert route_contacts(tape,ix[0],0,[1,2,3])=={1:(0,2)} + tape.insert(2,["ADD",2,0,"1",2]) + ix=contact_index(tape,{0},float("inf")) + assert not route_contacts(tape,ix[0],0,[1,2,3]) + return ["strict_rank_extension","saturated_high_intersection","low_union_bound","source_read_blocks_adjacency"] + + +def main(): + parser=ArgumentParser(description=__doc__) + for name in PINS: + parser.add_argument("--"+name,type=Path) + parser.add_argument("--controls-only",action="store_true") + args=parser.parse_args() + if not __debug__: + raise RuntimeError("Run with assertions") + if args.controls_only: + print(dumps(controls())) + return + if not all(getattr(args,name) for name in PINS): + parser.error("Require all three pinned input paths") + + def stop(*_): + raise TimeoutError("hard 20-second runner cap") + + tests,keys,decisions=[],[],[] + timed_out=None + signal(SIGALRM,stop) + alarm(20) + deadline=monotonic()+18 + try: + tests=controls() + price=checked(args.price,"price") + assert price["head"]==HEAD and price["predecessor_head"]==OLD_HEAD and price["word_sha256"]==PINS["word"] + cases=price["alternatives"] + keys=[r["key"] for r in cases] + assert len(keys)==len(set(map(tuple,keys)))==9 and not price["price_unresolved"] + old=checked(args.legacy,"legacy") + word=checked(args.word,"word") + assert (word["public"],word["owned_fields"],len(word["program"]))==(1501,68,76466) + used_charts={j for row in cases for operand in row["operands"] for j in operand["charts"]} + assert all(old["frames"][j]==word["frames"][j] for j in used_charts) + roles={x["role"] for row in cases for x in row["operands"]} + assert not roles&set(price["protected_roles"]) + for exact in (old,word): + main=set(exact["live"])|{r+112 for r in exact["live"]}|set(exact["hosted"]["X2"])|set(exact["hosted"]["Y2"]) + assert len(main)==400 and not roles&main and all(0<=r=deadline: + raise TimeoutError("nine-key geometry") + decisions.append(check_case(case,old,word,old_ix,new_ix)) + except TimeoutError as exc: + timed_out=str(exc) + finally: + alarm(0) + pending=keys[len(decisions):] + unresolved=pending+[r["key"] for r in decisions if r["status"]=="ambiguous_inherited_topology"] + print(dumps(dict(head=HEAD,predecessor_head=OLD_HEAD,input_sha256=PINS,case_cap=9,runner_cap_seconds=20, + controls=tests,decisions=decisions,unvisited=pending,unresolved=unresolved, + status_counts=dict(Counter(r["status"] for r in decisions)), + survivors=[r["key"] for r in decisions if r["status"]=="geometry_survivor"], + scope="Only nine inherited profitable shapes. No search for new current-word contacts.",timeout=timed_out), + indent=2,sort_keys=True)) + if timed_out: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-public-four-move-rechart-bound/inputs/7277-SUPPORT.json.gz b/research/p104-public-four-move-rechart-bound/inputs/7277-SUPPORT.json.gz new file mode 100644 index 0000000000..277f5ddb95 Binary files /dev/null and b/research/p104-public-four-move-rechart-bound/inputs/7277-SUPPORT.json.gz differ diff --git a/research/p104-public-four-move-rechart-bound/inputs/7277-WORD.json.gz b/research/p104-public-four-move-rechart-bound/inputs/7277-WORD.json.gz new file mode 100644 index 0000000000..077bf48c35 Binary files /dev/null and b/research/p104-public-four-move-rechart-bound/inputs/7277-WORD.json.gz differ diff --git a/research/p104-public-four-move-rechart-bound/inputs/7314-HELPERS.json.gz b/research/p104-public-four-move-rechart-bound/inputs/7314-HELPERS.json.gz new file mode 100644 index 0000000000..716a7ffc9a Binary files /dev/null and b/research/p104-public-four-move-rechart-bound/inputs/7314-HELPERS.json.gz differ diff --git a/research/p104-public-four-move-rechart-bound/inputs/7334-CHANGED.json b/research/p104-public-four-move-rechart-bound/inputs/7334-CHANGED.json new file mode 100644 index 0000000000..b1644106d9 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/inputs/7334-CHANGED.json @@ -0,0 +1,72 @@ +{ + "body_clocks": [ + 40222, + 40840, + 42609, + 43022, + 43023, + 43024, + 43025, + 43026, + 43028, + 43030, + 43403, + 43491, + 43535, + 43696, + 43698, + 43887, + 45365, + 45396 + ], + "copy_and_chart_local_ownership_checked": true, + "dirty_readout": { + "319": 1 + }, + "exact_basis_columns": 14, + "forward_direction": { + "1081": -1, + "1467": 1 + }, + "literal_candidate_clocks": [ + 44588, + 44627 + ], + "paid_delta_per_word": { + "1": -1, + "5": -1, + "6": 1 + }, + "ranks": [ + 3, + 8, + 9 + ], + "roles": [ + 198, + 205, + 319, + 532, + 652, + 654, + 962, + 969, + 1081, + 1250, + 1303, + 1305, + 1453, + 1467 + ], + "scope": "Local normalized rational block, literal chart availability and nesting. Absolute Gaussian phase and whole caller separate.", + "status": "PASS_INDEPENDENT_319_BLOCK", + "window": [ + 44616, + 45718 + ], + "word_sha256": [ + "0358b9f6e0340fb3e5aa46c747c558b32a5280cbf9cd92c3b9de627dd18a9a4f", + "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + ], + "wrong_sign_and_omitted_readout_rejected": true +} diff --git a/research/p104-public-four-move-rechart-bound/inputs/7334-WORD.json.gz b/research/p104-public-four-move-rechart-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-public-four-move-rechart-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-public-four-move-rechart-bound/inputs/ADMITTED.json b/research/p104-public-four-move-rechart-bound/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/inputs/ADMITTED.json @@ -0,0 +1,58 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "caller_sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "crossing": [ + "0.00364665195644044790699554028334161", + "0.00364665195644044790699554028334162" + ], + "end": "2026-11-11T23:04:43Z", + "exit": 0, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "hosted_at_admission": "plan and historical success; candidate replay in progress", + "inputs": { + "EARLY-RESULT.json": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649", + "INPUTS.json": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d", + "NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "PROPOSED-CLAIM.json": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03", + "RESULT.json": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194", + "SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + }, + "kappa": "0.00364665195644", + "ours": "0", + "peer_gain": "0.000000430519994", + "prior_kappa": "0.003646221436446", + "receipt": { + "peer-prep/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "peer-prep/STATIC.json": "500cc563b7dac8b1de1faf1dee9b820e73152dfddc15a650cd1191edd39e8c79", + "peer-price/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "peer-price/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "peer/COMMAND.txt": "714bfab024155d8216f3ef99f3ee7627ddc35ab341c486ac6bd53c476b757130", + "peer/COMMIT.stdout": "597470d8132a3812deb3624a859546c0c13d52b094fd6fc61e7416941130bd70", + "peer/END-UTC.txt": "9c46923c616c14da5b8ed503e1652021d7bd409a10ec91a78a03263013fba08a", + "peer/METADATA.stdout": "5873404cb4424dca918a00d503569f3c29a3190fd029a007e1afb2006399f647", + "peer/RUN.exit": "9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa", + "peer/RUN.stderr": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "peer/RUN.stdout": "d589626c7581fbb9928bc615364cfee49deb62dfc0a39a903417ca62be89cf8c", + "peer/START-UTC.txt": "5b78fd6d42a2b42206891318c08e6014de57d7ca46b0201cd11a166f452210f7" + }, + "source_history": "exact anchored base and recursive package provenance, sparse shallow stock wrapper not executed", + "stages": { + "caller": "PASS_HELPER_319_FUSED_CALLER 91166298911/25000000000000", + "early": "PASS_HELPER_319_EXACT_NATIVE_AND_SIGNED_PRICE 0.00364665195644", + "frontier": "PASS_HELPER_319_FUSED_FRONTIER_PROPOSAL 91166298911/25000000000000", + "native": "PASS_HELPER_319_FUSED_NATIVE 3646017316711/1000000000000000" + }, + "start": "2026-11-11T22:54:48Z", + "status": "independently_reproduced_comparable", + "tree": "fa98712a459b20c10240450097c87de433f8a750" +} diff --git a/research/p104-public-four-move-rechart-bound/inputs/READBACK.json b/research/p104-public-four-move-rechart-bound/inputs/READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/inputs/READBACK.json @@ -0,0 +1,188 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "bit_admitted": "12039/3125000", + "bit_claim_headroom": "3000951089/25000000000000", + "bit_premise": "376669/100000000", + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "claim": "91166298911/25000000000000", + "context_c": 2430, + "context_headroom": 1666, + "copies": 17, + "directed_bounds": { + "new_at_claim": [ + "347195197206460540909548691538238227127/2000000000000000000000000000000000000000000000000", + "1735975986032302704547743457691191192207/10000000000000000000000000000000000000000000000000" + ], + "new_at_old_crossing_upper": [ + "333717954993733063339209580360321337006028706669/2000000000000000000000000000000000000000000000000", + "1668589774968665316696047901801606685030143589709/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_lower": [ + "8890529086421014119/10000000000000000000000000000000000000000000000000", + "8890529086421080299/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_upper": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "new_at_tested": [ + "1464673416007288863003441470091977383033/10000000000000000000000000000000000000000000000000", + "1464673416007288863003441470091977438357/10000000000000000000000000000000000000000000000000" + ], + "old_at_claim": [ + "-1668785950738799647054310634446839861363893886031/10000000000000000000000000000000000000000000000000", + "-66751438029551985882172425377873594454555753177/400000000000000000000000000000000000000000000000" + ], + "old_at_old_crossing_upper": [ + "-357270001119021587349/10000000000000000000000000000000000000000000000000", + "-357270001119021530951/10000000000000000000000000000000000000000000000000" + ] + }, + "empty_root_credits": 0, + "exact_gain": "215259997/500000000000000", + "exact_relative_percent": "21525999700/1823110718223", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "incumbent": "1823110718223/500000000000000", + "main_boundaries": 104, + "native_grid": [ + 1125, + 25 + ], + "native_ingredient_claim": "3646017316711/1000000000000000", + "new_raw_interval": [ + "364665195644044790699554028334161/100000000000000000000000000000000000", + "182332597822022395349777014167081/50000000000000000000000000000000000" + ], + "old_raw_upper": "36462214364462343366888845568981/10000000000000000000000000000000000", + "ordinary": 782715464, + "ordinary_delta": 52088, + "ordinary_headroom": 217284536, + "outer_functional": 4, + "outer_strict": 54, + "outer_strict_slack": "299635334804355997/10000000000000000000000000000000000", + "owned_lifetimes": 73, + "owned_peak": 50, + "paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110519, + "parent": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "path_pins": { + "dependencies/7298/pricing.py": { + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "dependencies/7314/NATIVE-RESULT.json": { + "sha256": "336f463da5afe5b60bfd3b9f0ce8aeea5a5feb1f854613bf4218ba0b28b3371b" + }, + "dependencies/7314/PROPOSED-CLAIM.json": { + "sha256": "41a08c4b7d0b2de4af22bc778948a143027eb3065fff47b0400b6ded1cc52778" + }, + "dependencies/7314/RESULT.json": { + "sha256": "432191ca572c9221935787ebe392699e3a1ef4512b0bf4fbc704657321cc87ca" + }, + "dependencies/round65/price.json": { + "sha256": "25205ad2cf4230bd2b2b704eec9f96ec4a5486fd575b5599861b28ffdd15b00b" + }, + "receipts/EARLY-RESULT.json": { + "git_blob": "675d6cf2374f3384019dfd53b2bdffd845005f13", + "sha256": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649" + }, + "receipts/INPUTS.json": { + "git_blob": "95c53f4594287a72d9b586f10ee136d0a1686984", + "sha256": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d" + }, + "receipts/NATIVE-RESULT.json": { + "git_blob": "eb101307d4d0399efed96d88cf6d4c01ec9c7369", + "sha256": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812" + }, + "receipts/PROOF.md": { + "git_blob": "7644e5571d583183ee93b686612b5ec4555f6911", + "sha256": "560de573bfd4563c16ca3c7308fa729b4188fabe802d8830f343c3873f75b59d" + }, + "receipts/PROPOSED-CLAIM.json": { + "git_blob": "6b491894580741e3e2c11a453722a0302db7b5d6", + "sha256": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03" + }, + "receipts/README.md": { + "git_blob": "b3a055f4e0d334ce2e7df3310caaa0849eb3eba1", + "sha256": "b4db0eb83ab6a2f7151bed2da955a487f4816ec9d1976eccc21e54c2725490b0" + }, + "receipts/REFERENCE.json": { + "git_blob": "8859e243cc39546bcb1e257d95c19a658c455dc7", + "sha256": "3e66e054b803551f18b8670da0b2990a7d0eeb689dfc45b56dbcba295551da70" + }, + "receipts/REPLAY.txt": { + "git_blob": "0b8d8048c18740060f4b7f6d380a5f3a0f30ee53", + "sha256": "230984f4b8206ae4d0c0f18fbba86ff43a1a9623f8ed337cf1285360f9a67c0c" + }, + "receipts/RESULT.json": { + "git_blob": "3034a490f5b0656ae71495c99493c4ab1ac1f5c6", + "sha256": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194" + }, + "receipts/SOURCES.json": { + "git_blob": "6b97e903a6df8de437068a0e2907823885928053", + "sha256": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593" + }, + "receipts/VERIFY.json": { + "git_blob": "cc98ee2a5c5a79e670094a6f55c7cacda8fd330c", + "sha256": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513" + }, + "receipts/construct.py": { + "git_blob": "89e923bd738dfc404ca76b7ae36f13844ac4bfbb", + "sha256": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + } + }, + "physical_maps": 3037, + "productive_fields": 22461, + "rank_surplus": 1424, + "raw_strict_separation": "43051999421357030665572644351/100000000000000000000000000000000000", + "scope": "Exact receipt and directed-price readback. No native or caller execution in this audit.", + "source_archive_sha256": "0589953b3886d96eacf3bda3d38d8d574bb739fba1056af7f32f56047b6061e2", + "targets": { + "1": 306, + "2": 357, + "3": 799, + "4": 3825, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "tested": "364665195644007/100000000000000000" +} diff --git a/research/p104-public-four-move-rechart-bound/inputs/pricing.py b/research/p104-public-four-move-rechart-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-public-four-move-rechart-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-public-four-move-rechart-bound/receipts/COMPARE.json b/research/p104-public-four-move-rechart-bound/receipts/COMPARE.json new file mode 100644 index 0000000000..f481f42360 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/receipts/COMPARE.json @@ -0,0 +1,94 @@ +{ + "exact_key_agreements": 9, + "exact_rank_intervals_collapsed_to_old_span": 9, + "geometry_survivors": 0, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "pins": { + "independent": "97e6272c27714065c382360eb2a7a26209a13bf13a568ca4a643d46ec4b7889d", + "lead": "7ef82a94baec5e5ede8af38bc9172739f0cff24be94f8d4c3c5bc4e877768805" + }, + "rows": [ + [ + [ + 38408, + 1 + ], + 38420, + 4, + 5 + ], + [ + [ + 38411, + 1 + ], + 38423, + 4, + 5 + ], + [ + [ + 38476, + 1 + ], + 38488, + 4, + 5 + ], + [ + [ + 40895, + 1 + ], + 40903, + 4, + 5 + ], + [ + [ + 41575, + 1 + ], + 41583, + 4, + 5 + ], + [ + [ + 39129, + 1 + ], + 39141, + 4, + 5 + ], + [ + [ + 41941, + 1 + ], + 41949, + 4, + 5 + ], + [ + [ + 42623, + 1 + ], + 42629, + 4, + 5 + ], + [ + [ + 42946, + 1 + ], + 42952, + 4, + 5 + ] + ], + "unresolved": 0 +} diff --git a/research/p104-public-four-move-rechart-bound/receipts/FORWARD.json b/research/p104-public-four-move-rechart-bound/receipts/FORWARD.json new file mode 100644 index 0000000000..d7fe675855 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/receipts/FORWARD.json @@ -0,0 +1,1692 @@ +{ + "ancestor_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "case_cap": 9, + "controls": [ + "expanded_high_intersection", + "saturated_high_intersection", + "deterministic_new_descriptor", + "intervening_source_read_blocks_contact" + ], + "cooperative_seconds": 18, + "counts": { + "high_intersection_too_small": 9 + }, + "hard_seconds": 20, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "lead/inputs/7277-WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "preflight/PRICE.json": "005efb8329d38638800d82e5273580b1bb529ac490d9923ba1a92e112d31c8b1", + "preflight/inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + }, + "last_stage": "nine_frozen_keys", + "outcomes": [ + { + "ancestor_ADD_clock": 38408, + "ancestor_MOVE_clocks": { + "1059": [ + 38406, + 41807 + ], + "1427": [ + 38407, + 41211 + ] + }, + "ancestor_exact_ADD_clocks": [ + 38408 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "1059:in", + "1427:in", + "ADD", + "1427:out", + "1059:out" + ], + "current_ADD_clock": 38420, + "current_MOVE_clocks": { + "1059": [ + 38418, + 41815 + ], + "1427": [ + 38419, + 41219 + ] + }, + "current_exact_ADD_clocks": [ + 38420 + ], + "current_incident_neighbors": { + "1059": [ + [ + 38418, + [ + "MOVE", + 1059, + 341, + 725, + false + ] + ], + [ + 41815, + [ + "MOVE", + 1059, + 725, + 861, + false + ] + ] + ], + "1427": [ + [ + 38419, + [ + "MOVE", + 1427, + 594, + 725, + false + ] + ], + [ + 41219, + [ + "MOVE", + 1427, + 725, + 883, + false + ] + ] + ] + }, + "current_relative_order": [ + "1059:in", + "1427:in", + "ADD", + "1427:out", + "1059:out" + ], + "geometry_certificate": { + "chart_bases": { + "341": [ + 102, + 145, + 290 + ], + "594": [ + 25 + ], + "725": [ + 25, + 102, + 136, + 290 + ], + "861": [ + 1, + 6, + 24, + 96, + 136, + 290 + ], + "883": [ + 9, + 16, + 36, + 66, + 129, + 262 + ] + }, + "chart_ranks": { + "341": 3, + "594": 1, + "725": 4, + "861": 6, + "883": 6 + }, + "high_intersection_basis": [ + 25, + 102, + 136, + 290 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 1, + 6, + 8, + 16, + 34, + 66, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 25, + 102, + 136, + 290 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "key": [ + 38408, + 1 + ], + "literal_ADD": [ + "ADD", + 1059, + 1427, + "-1", + 725 + ], + "status": "high_intersection_too_small" + }, + { + "ancestor_ADD_clock": 38411, + "ancestor_MOVE_clocks": { + "791": [ + 38409, + 41201 + ], + "1232": [ + 38410, + 39146 + ] + }, + "ancestor_exact_ADD_clocks": [ + 38411 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "791:in", + "1232:in", + "ADD", + "1232:out", + "791:out" + ], + "current_ADD_clock": 38423, + "current_MOVE_clocks": { + "791": [ + 38421, + 41209 + ], + "1232": [ + 38422, + 39158 + ] + }, + "current_exact_ADD_clocks": [ + 38423 + ], + "current_incident_neighbors": { + "791": [ + [ + 38421, + [ + "MOVE", + 791, + 342, + 726, + false + ] + ], + [ + 41209, + [ + "MOVE", + 791, + 726, + 862, + false + ] + ] + ], + "1232": [ + [ + 38422, + [ + "MOVE", + 1232, + 594, + 726, + false + ] + ], + [ + 39158, + [ + "MOVE", + 1232, + 726, + 884, + false + ] + ] + ] + }, + "current_relative_order": [ + "791:in", + "1232:in", + "ADD", + "1232:out", + "791:out" + ], + "geometry_certificate": { + "chart_bases": { + "342": [ + 102, + 162, + 273 + ], + "594": [ + 25 + ], + "726": [ + 25, + 102, + 162, + 264 + ], + "862": [ + 1, + 6, + 24, + 96, + 162, + 264 + ], + "884": [ + 9, + 16, + 36, + 66, + 134, + 257 + ] + }, + "chart_ranks": { + "342": 3, + "594": 1, + "726": 4, + "862": 6, + "884": 6 + }, + "high_intersection_basis": [ + 25, + 102, + 162, + 264 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 1, + 6, + 8, + 16, + 34, + 66, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 25, + 102, + 162, + 264 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "key": [ + 38411, + 1 + ], + "literal_ADD": [ + "ADD", + 791, + 1232, + "-1", + 726 + ], + "status": "high_intersection_too_small" + }, + { + "ancestor_ADD_clock": 38476, + "ancestor_MOVE_clocks": { + "1150": [ + 38474, + 39523 + ], + "1426": [ + 38475, + 39133 + ] + }, + "ancestor_exact_ADD_clocks": [ + 38476 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "1150:in", + "1426:in", + "ADD", + "1426:out", + "1150:out" + ], + "current_ADD_clock": 38488, + "current_MOVE_clocks": { + "1150": [ + 38486, + 39535 + ], + "1426": [ + 38487, + 39145 + ] + }, + "current_exact_ADD_clocks": [ + 38488 + ], + "current_incident_neighbors": { + "1150": [ + [ + 38486, + [ + "MOVE", + 1150, + 454, + 759, + false + ] + ], + [ + 39535, + [ + "MOVE", + 1150, + 759, + 825, + false + ] + ] + ], + "1426": [ + [ + 38487, + [ + "MOVE", + 1426, + 593, + 759, + false + ] + ], + [ + 39145, + [ + "MOVE", + 1426, + 759, + 852, + false + ] + ] + ] + }, + "current_relative_order": [ + "1150:in", + "1426:in", + "ADD", + "1426:out", + "1150:out" + ], + "geometry_certificate": { + "chart_bases": { + "454": [ + 75, + 176, + 304 + ], + "593": [ + 7 + ], + "759": [ + 7, + 75, + 176, + 304 + ], + "825": [ + 7, + 10, + 32, + 65, + 144, + 272 + ], + "852": [ + 7, + 9, + 16, + 66, + 160, + 288 + ] + }, + "chart_ranks": { + "454": 3, + "593": 1, + "759": 4, + "825": 6, + "852": 6 + }, + "high_intersection_basis": [ + 7, + 75, + 176, + 304 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 3, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 7, + 75, + 176, + 304 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "key": [ + 38476, + 1 + ], + "literal_ADD": [ + "ADD", + 1150, + 1426, + "-1", + 759 + ], + "status": "high_intersection_too_small" + }, + { + "ancestor_ADD_clock": 40895, + "ancestor_MOVE_clocks": { + "296": [ + 40894, + 42356 + ], + "490": [ + 40893, + 42229 + ] + }, + "ancestor_exact_ADD_clocks": [ + 40895 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "490:in", + "296:in", + "ADD", + "490:out", + "296:out" + ], + "current_ADD_clock": 40903, + "current_MOVE_clocks": { + "296": [ + 40902, + 42364 + ], + "490": [ + 40901, + 42237 + ] + }, + "current_exact_ADD_clocks": [ + 40903 + ], + "current_incident_neighbors": { + "296": [ + [ + 40902, + [ + "MOVE", + 296, + 341, + 725, + false + ] + ], + [ + 42364, + [ + "MOVE", + 296, + 725, + 861, + false + ] + ] + ], + "490": [ + [ + 40901, + [ + "MOVE", + 490, + 594, + 725, + false + ] + ], + [ + 42237, + [ + "MOVE", + 490, + 725, + 883, + false + ] + ] + ] + }, + "current_relative_order": [ + "490:in", + "296:in", + "ADD", + "490:out", + "296:out" + ], + "geometry_certificate": { + "chart_bases": { + "341": [ + 102, + 145, + 290 + ], + "594": [ + 25 + ], + "725": [ + 25, + 102, + 136, + 290 + ], + "861": [ + 1, + 6, + 24, + 96, + 136, + 290 + ], + "883": [ + 9, + 16, + 36, + 66, + 129, + 262 + ] + }, + "chart_ranks": { + "341": 3, + "594": 1, + "725": 4, + "861": 6, + "883": 6 + }, + "high_intersection_basis": [ + 25, + 102, + 136, + 290 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 1, + 6, + 8, + 16, + 34, + 66, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 25, + 102, + 136, + 290 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "key": [ + 40895, + 1 + ], + "literal_ADD": [ + "ADD", + 490, + 296, + "1", + 725 + ], + "status": "high_intersection_too_small" + }, + { + "ancestor_ADD_clock": 41575, + "ancestor_MOVE_clocks": { + "388": [ + 41574, + 42082 + ], + "561": [ + 41573, + 42251 + ] + }, + "ancestor_exact_ADD_clocks": [ + 41575 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "561:in", + "388:in", + "ADD", + "388:out", + "561:out" + ], + "current_ADD_clock": 41583, + "current_MOVE_clocks": { + "388": [ + 41582, + 42090 + ], + "561": [ + 41581, + 42259 + ] + }, + "current_exact_ADD_clocks": [ + 41583 + ], + "current_incident_neighbors": { + "388": [ + [ + 41582, + [ + "MOVE", + 388, + 454, + 759, + false + ] + ], + [ + 42090, + [ + "MOVE", + 388, + 759, + 825, + false + ] + ] + ], + "561": [ + [ + 41581, + [ + "MOVE", + 561, + 593, + 759, + false + ] + ], + [ + 42259, + [ + "MOVE", + 561, + 759, + 852, + false + ] + ] + ] + }, + "current_relative_order": [ + "561:in", + "388:in", + "ADD", + "388:out", + "561:out" + ], + "geometry_certificate": { + "chart_bases": { + "454": [ + 75, + 176, + 304 + ], + "593": [ + 7 + ], + "759": [ + 7, + 75, + 176, + 304 + ], + "825": [ + 7, + 10, + 32, + 65, + 144, + 272 + ], + "852": [ + 7, + 9, + 16, + 66, + 160, + 288 + ] + }, + "chart_ranks": { + "454": 3, + "593": 1, + "759": 4, + "825": 6, + "852": 6 + }, + "high_intersection_basis": [ + 7, + 75, + 176, + 304 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 3, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 7, + 75, + 176, + 304 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "key": [ + 41575, + 1 + ], + "literal_ADD": [ + "ADD", + 561, + 388, + "1", + 759 + ], + "status": "high_intersection_too_small" + }, + { + "ancestor_ADD_clock": 39129, + "ancestor_MOVE_clocks": { + "1033": [ + 39127, + 39134 + ], + "1224": [ + 39128, + 39529 + ] + }, + "ancestor_exact_ADD_clocks": [ + 39129 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "1033:in", + "1224:in", + "ADD", + "1033:out", + "1224:out" + ], + "current_ADD_clock": 39141, + "current_MOVE_clocks": { + "1033": [ + 39139, + 39146 + ], + "1224": [ + 39140, + 39541 + ] + }, + "current_exact_ADD_clocks": [ + 39141 + ], + "current_incident_neighbors": { + "1033": [ + [ + 39139, + [ + "MOVE", + 1033, + 305, + 715, + false + ] + ], + [ + 39146, + [ + "MOVE", + 1033, + 715, + 852, + false + ] + ] + ], + "1224": [ + [ + 39140, + [ + "MOVE", + 1224, + 676, + 715, + false + ] + ], + [ + 39541, + [ + "MOVE", + 1224, + 715, + 876, + false + ] + ] + ] + }, + "current_relative_order": [ + "1033:in", + "1224:in", + "ADD", + "1033:out", + "1224:out" + ], + "geometry_certificate": { + "chart_bases": { + "305": [ + 14, + 69, + 400 + ], + "676": [ + 7, + 66 + ], + "715": [ + 7, + 9, + 66, + 400 + ], + "852": [ + 7, + 9, + 16, + 66, + 160, + 288 + ], + "876": [ + 3, + 4, + 9, + 48, + 65, + 400 + ] + }, + "chart_ranks": { + "305": 3, + "676": 2, + "715": 4, + "852": 6, + "876": 6 + }, + "high_intersection_basis": [ + 7, + 9, + 66, + 400 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 3, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 7, + 9, + 66, + 400 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "161230404088678643731066192226389795710423889911/5000000000000000000000000000000000000000000000000", + "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000" + ], + "key": [ + 39129, + 1 + ], + "literal_ADD": [ + "ADD", + 1033, + 1224, + "-1", + 715 + ], + "status": "high_intersection_too_small" + }, + { + "ancestor_ADD_clock": 41941, + "ancestor_MOVE_clocks": { + "270": [ + 41940, + 42250 + ], + "471": [ + 41939, + 43960 + ] + }, + "ancestor_exact_ADD_clocks": [ + 41941 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "471:in", + "270:in", + "ADD", + "270:out", + "471:out" + ], + "current_ADD_clock": 41949, + "current_MOVE_clocks": { + "270": [ + 41948, + 42258 + ], + "471": [ + 41947, + 43946 + ] + }, + "current_exact_ADD_clocks": [ + 41949 + ], + "current_incident_neighbors": { + "270": [ + [ + 41948, + [ + "MOVE", + 270, + 305, + 715, + false + ] + ], + [ + 42258, + [ + "MOVE", + 270, + 715, + 852, + false + ] + ] + ], + "471": [ + [ + 41947, + [ + "MOVE", + 471, + 676, + 715, + false + ] + ], + [ + 43946, + [ + "MOVE", + 471, + 715, + 876, + false + ] + ] + ] + }, + "current_relative_order": [ + "471:in", + "270:in", + "ADD", + "270:out", + "471:out" + ], + "geometry_certificate": { + "chart_bases": { + "305": [ + 14, + 69, + 400 + ], + "676": [ + 7, + 66 + ], + "715": [ + 7, + 9, + 66, + 400 + ], + "852": [ + 7, + 9, + 16, + 66, + 160, + 288 + ], + "876": [ + 3, + 4, + 9, + 48, + 65, + 400 + ] + }, + "chart_ranks": { + "305": 3, + "676": 2, + "715": 4, + "852": 6, + "876": 6 + }, + "high_intersection_basis": [ + 7, + 9, + 66, + 400 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 3, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 7, + 9, + 66, + 400 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "161230404088678643731066192226389795710423889911/5000000000000000000000000000000000000000000000000", + "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000" + ], + "key": [ + 41941, + 1 + ], + "literal_ADD": [ + "ADD", + 471, + 270, + "1", + 715 + ], + "status": "high_intersection_too_small" + }, + { + "ancestor_ADD_clock": 42623, + "ancestor_MOVE_clocks": { + "1193": [ + 42621, + 42855 + ], + "1262": [ + 42622, + 42892 + ] + }, + "ancestor_exact_ADD_clocks": [ + 42623 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "1193:in", + "1262:in", + "ADD", + "1193:out", + "1262:out" + ], + "current_ADD_clock": 42629, + "current_MOVE_clocks": { + "1193": [ + 42627, + 42861 + ], + "1262": [ + 42628, + 42898 + ] + }, + "current_exact_ADD_clocks": [ + 42629 + ], + "current_incident_neighbors": { + "1193": [ + [ + 42627, + [ + "MOVE", + 1193, + 511, + 773, + false + ] + ], + [ + 42861, + [ + "MOVE", + 1193, + 773, + 775, + false + ] + ] + ], + "1262": [ + [ + 42628, + [ + "MOVE", + 1262, + 652, + 773, + false + ] + ], + [ + 42898, + [ + "MOVE", + 1262, + 773, + 774, + false + ] + ] + ] + }, + "current_relative_order": [ + "1193:in", + "1262:in", + "ADD", + "1193:out", + "1262:out" + ], + "geometry_certificate": { + "chart_bases": { + "511": [ + 30, + 140, + 268 + ], + "652": [ + 82, + 268 + ], + "773": [ + 30, + 76, + 140, + 268 + ], + "774": [ + 13, + 19, + 39, + 65, + 129, + 257 + ], + "775": [ + 7, + 25, + 43, + 75, + 139, + 267 + ] + }, + "chart_ranks": { + "511": 3, + "652": 2, + "773": 4, + "774": 6, + "775": 6 + }, + "high_intersection_basis": [ + 30, + 76, + 140, + 268 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 1, + 6, + 10, + 18, + 32, + 64, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 30, + 76, + 140, + 268 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "161230404088678643731066192226389795710423889911/5000000000000000000000000000000000000000000000000", + "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000" + ], + "key": [ + 42623, + 1 + ], + "literal_ADD": [ + "ADD", + 1193, + 1262, + "-1", + 773 + ], + "status": "high_intersection_too_small" + }, + { + "ancestor_ADD_clock": 42946, + "ancestor_MOVE_clocks": { + "436": [ + 42945, + 43004 + ], + "586": [ + 42944, + 42969 + ] + }, + "ancestor_exact_ADD_clocks": [ + 42946 + ], + "ancestor_exact_ADD_ordinal": 0, + "ancestor_relative_order": [ + "586:in", + "436:in", + "ADD", + "586:out", + "436:out" + ], + "current_ADD_clock": 42952, + "current_MOVE_clocks": { + "436": [ + 42951, + 43010 + ], + "586": [ + 42950, + 42975 + ] + }, + "current_exact_ADD_clocks": [ + 42952 + ], + "current_incident_neighbors": { + "436": [ + [ + 42951, + [ + "MOVE", + 436, + 511, + 773, + false + ] + ], + [ + 43010, + [ + "MOVE", + 436, + 773, + 775, + false + ] + ] + ], + "586": [ + [ + 42950, + [ + "MOVE", + 586, + 652, + 773, + false + ] + ], + [ + 42975, + [ + "MOVE", + 586, + 773, + 774, + false + ] + ] + ] + }, + "current_relative_order": [ + "586:in", + "436:in", + "ADD", + "586:out", + "436:out" + ], + "geometry_certificate": { + "chart_bases": { + "511": [ + 30, + 140, + 268 + ], + "652": [ + 82, + 268 + ], + "773": [ + 30, + 76, + 140, + 268 + ], + "774": [ + 13, + 19, + 39, + 65, + 129, + 257 + ], + "775": [ + 7, + 25, + 43, + 75, + 139, + 267 + ] + }, + "chart_ranks": { + "511": 3, + "652": 2, + "773": 4, + "774": 6, + "775": 6 + }, + "high_intersection_basis": [ + 30, + 76, + 140, + 268 + ], + "high_intersection_rank": 4, + "high_sum_basis": [ + 1, + 6, + 10, + 18, + 32, + 64, + 128, + 256 + ], + "high_sum_rank": 8, + "low_union_basis": [ + 30, + 76, + 140, + 268 + ], + "low_union_rank": 4, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "wanted_rank": 5 + }, + "gross_at_incumbent": [ + "161230404088678643731066192226389795710423889911/5000000000000000000000000000000000000000000000000", + "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000" + ], + "key": [ + 42946, + 1 + ], + "literal_ADD": [ + "ADD", + 586, + 436, + "1", + 773 + ], + "status": "high_intersection_too_small" + } + ], + "price_sha256": "005efb8329d38638800d82e5273580b1bb529ac490d9923ba1a92e112d31c8b1", + "scope": "Nine frozen public-helper fixed-clock ADD recharts, exact ancestor ordinal and current contact topology, then exact GF(2) rank.", + "status": "EXHAUSTED", + "survivors": [], + "unresolved": [], + "unvisited": [], + "visited": 9, + "word_sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +} diff --git a/research/p104-public-four-move-rechart-bound/receipts/PRICE.json b/research/p104-public-four-move-rechart-bound/receipts/PRICE.json new file mode 100644 index 0000000000..fe794c3699 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/receipts/PRICE.json @@ -0,0 +1,712 @@ +{ + "allowed_helper_pairs": 48, + "alternatives": [ + { + "complete_margin_at_incumbent": [ + "531526956045922605118177615578754702453953365257/10000000000000000000000000000000000000000000000000", + "265763478022961302559088807789377351226976710577/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "527651349852979855561346786909788523363571292127/10000000000000000000000000000000000000000000000000", + "65956418731622481945168348363723565420446418503/1250000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "583748999986160510201494705219280187227313772829/10000000000000000000000000000000000000000000000000", + "7296862499827006377518683815241002340341422161/125000000000000000000000000000000000000000000000" + ], + "key": [ + 38408, + 1 + ], + "operands": [ + { + "charts": [ + 341, + 725, + 861 + ], + "moves": [ + 38406, + 41807 + ], + "ranks": [ + 1, + 2 + ], + "role": 1059 + }, + { + "charts": [ + 594, + 725, + 883 + ], + "moves": [ + 38407, + 41211 + ], + "ranks": [ + 3, + 2 + ], + "role": 1427 + } + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "target_delta": {} + }, + { + "complete_margin_at_incumbent": [ + "531526956045922605118177615578754702453953365257/10000000000000000000000000000000000000000000000000", + "265763478022961302559088807789377351226976710577/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "527651349852979855561346786909788523363571292127/10000000000000000000000000000000000000000000000000", + "65956418731622481945168348363723565420446418503/1250000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "583748999986160510201494705219280187227313772829/10000000000000000000000000000000000000000000000000", + "7296862499827006377518683815241002340341422161/125000000000000000000000000000000000000000000000" + ], + "key": [ + 38411, + 1 + ], + "operands": [ + { + "charts": [ + 342, + 726, + 862 + ], + "moves": [ + 38409, + 41201 + ], + "ranks": [ + 1, + 2 + ], + "role": 791 + }, + { + "charts": [ + 594, + 726, + 884 + ], + "moves": [ + 38410, + 39146 + ], + "ranks": [ + 3, + 2 + ], + "role": 1232 + } + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "target_delta": {} + }, + { + "complete_margin_at_incumbent": [ + "531526956045922605118177615578754702453953365257/10000000000000000000000000000000000000000000000000", + "265763478022961302559088807789377351226976710577/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "527651349852979855561346786909788523363571292127/10000000000000000000000000000000000000000000000000", + "65956418731622481945168348363723565420446418503/1250000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "583748999986160510201494705219280187227313772829/10000000000000000000000000000000000000000000000000", + "7296862499827006377518683815241002340341422161/125000000000000000000000000000000000000000000000" + ], + "key": [ + 38476, + 1 + ], + "operands": [ + { + "charts": [ + 454, + 759, + 825 + ], + "moves": [ + 38474, + 39523 + ], + "ranks": [ + 1, + 2 + ], + "role": 1150 + }, + { + "charts": [ + 593, + 759, + 852 + ], + "moves": [ + 38475, + 39133 + ], + "ranks": [ + 3, + 2 + ], + "role": 1426 + } + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "target_delta": {} + }, + { + "complete_margin_at_incumbent": [ + "531526956045922605118177615578754702453953365257/10000000000000000000000000000000000000000000000000", + "265763478022961302559088807789377351226976710577/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "527651349852979855561346786909788523363571292127/10000000000000000000000000000000000000000000000000", + "65956418731622481945168348363723565420446418503/1250000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "583748999986160510201494705219280187227313772829/10000000000000000000000000000000000000000000000000", + "7296862499827006377518683815241002340341422161/125000000000000000000000000000000000000000000000" + ], + "key": [ + 40895, + 1 + ], + "operands": [ + { + "charts": [ + 341, + 725, + 861 + ], + "moves": [ + 40894, + 42356 + ], + "ranks": [ + 1, + 2 + ], + "role": 296 + }, + { + "charts": [ + 594, + 725, + 883 + ], + "moves": [ + 40893, + 42229 + ], + "ranks": [ + 3, + 2 + ], + "role": 490 + } + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "target_delta": {} + }, + { + "complete_margin_at_incumbent": [ + "531526956045922605118177615578754702453953365257/10000000000000000000000000000000000000000000000000", + "265763478022961302559088807789377351226976710577/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "527651349852979855561346786909788523363571292127/10000000000000000000000000000000000000000000000000", + "65956418731622481945168348363723565420446418503/1250000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "106305391209184521023635523121724336674221137451/2000000000000000000000000000000000000000000000000", + "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "583748999986160510201494705219280187227313772829/10000000000000000000000000000000000000000000000000", + "7296862499827006377518683815241002340341422161/125000000000000000000000000000000000000000000000" + ], + "key": [ + 41575, + 1 + ], + "operands": [ + { + "charts": [ + 454, + 759, + 825 + ], + "moves": [ + 41574, + 42082 + ], + "ranks": [ + 1, + 2 + ], + "role": 388 + }, + { + "charts": [ + 593, + 759, + 852 + ], + "moves": [ + 41573, + 42251 + ], + "ranks": [ + 3, + 2 + ], + "role": 561 + } + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "target_delta": {} + }, + { + "complete_margin_at_incumbent": [ + "322460808177357287462132384422912610503695457807/10000000000000000000000000000000000000000000000000", + "161230404088678643731066192211456305251847756869/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "63717029017370681331189585581984139809517368453/2000000000000000000000000000000000000000000000000", + "79646286271713351663986981977480174761896724549/2500000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "161230404088678643731066192226389795710423889911/5000000000000000000000000000000000000000000000000", + "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "354164717704983294072118927317509090956702321189/10000000000000000000000000000000000000000000000000", + "8854117942624582351802973182937727273917558031/250000000000000000000000000000000000000000000000" + ], + "key": [ + 39129, + 1 + ], + "operands": [ + { + "charts": [ + 305, + 715, + 852 + ], + "moves": [ + 39127, + 39134 + ], + "ranks": [ + 1, + 2 + ], + "role": 1033 + }, + { + "charts": [ + 676, + 715, + 876 + ], + "moves": [ + 39128, + 39529 + ], + "ranks": [ + 2, + 2 + ], + "role": 1224 + } + ], + "paid_delta": { + "1": 17, + "2": -34, + "3": 17 + }, + "target_delta": {} + }, + { + "complete_margin_at_incumbent": [ + "322460808177357287462132384422912610503695457807/10000000000000000000000000000000000000000000000000", + "161230404088678643731066192211456305251847756869/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "63717029017370681331189585581984139809517368453/2000000000000000000000000000000000000000000000000", + "79646286271713351663986981977480174761896724549/2500000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "161230404088678643731066192226389795710423889911/5000000000000000000000000000000000000000000000000", + "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "354164717704983294072118927317509090956702321189/10000000000000000000000000000000000000000000000000", + "8854117942624582351802973182937727273917558031/250000000000000000000000000000000000000000000000" + ], + "key": [ + 41941, + 1 + ], + "operands": [ + { + "charts": [ + 305, + 715, + 852 + ], + "moves": [ + 41940, + 42250 + ], + "ranks": [ + 1, + 2 + ], + "role": 270 + }, + { + "charts": [ + 676, + 715, + 876 + ], + "moves": [ + 41939, + 43960 + ], + "ranks": [ + 2, + 2 + ], + "role": 471 + } + ], + "paid_delta": { + "1": 17, + "2": -34, + "3": 17 + }, + "target_delta": {} + }, + { + "complete_margin_at_incumbent": [ + "322460808177357287462132384422912610503695457807/10000000000000000000000000000000000000000000000000", + "161230404088678643731066192211456305251847756869/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "63717029017370681331189585581984139809517368453/2000000000000000000000000000000000000000000000000", + "79646286271713351663986981977480174761896724549/2500000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "161230404088678643731066192226389795710423889911/5000000000000000000000000000000000000000000000000", + "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "354164717704983294072118927317509090956702321189/10000000000000000000000000000000000000000000000000", + "8854117942624582351802973182937727273917558031/250000000000000000000000000000000000000000000000" + ], + "key": [ + 42623, + 1 + ], + "operands": [ + { + "charts": [ + 511, + 773, + 775 + ], + "moves": [ + 42621, + 42855 + ], + "ranks": [ + 1, + 2 + ], + "role": 1193 + }, + { + "charts": [ + 652, + 773, + 774 + ], + "moves": [ + 42622, + 42892 + ], + "ranks": [ + 2, + 2 + ], + "role": 1262 + } + ], + "paid_delta": { + "1": 17, + "2": -34, + "3": 17 + }, + "target_delta": {} + }, + { + "complete_margin_at_incumbent": [ + "322460808177357287462132384422912610503695457807/10000000000000000000000000000000000000000000000000", + "161230404088678643731066192211456305251847756869/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "63717029017370681331189585581984139809517368453/2000000000000000000000000000000000000000000000000", + "79646286271713351663986981977480174761896724549/2500000000000000000000000000000000000000000000000" + ], + "delta_midpoint_rank": 1, + "gross_at_incumbent": [ + "161230404088678643731066192226389795710423889911/5000000000000000000000000000000000000000000000000", + "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "354164717704983294072118927317509090956702321189/10000000000000000000000000000000000000000000000000", + "8854117942624582351802973182937727273917558031/250000000000000000000000000000000000000000000000" + ], + "key": [ + 42946, + 1 + ], + "operands": [ + { + "charts": [ + 511, + 773, + 775 + ], + "moves": [ + 42945, + 43004 + ], + "ranks": [ + 1, + 2 + ], + "role": 436 + }, + { + "charts": [ + 652, + 773, + 774 + ], + "moves": [ + 42944, + 42969 + ], + "ranks": [ + 2, + 2 + ], + "role": 586 + } + ], + "paid_delta": { + "1": 17, + "2": -34, + "3": 17 + }, + "target_delta": {} + } + ], + "build_cap": 1, + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "first_case_cap": 20, + "first_runner_seconds": 20, + "fixed_moonshot": "10018846261809/2500000000000000", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "inputs/7277-SUPPORT.json.gz": "a63d766dce9ccc5b7a97057fb298350617cbf78833f0ebc5bb488dec00e71159", + "inputs/7314-HELPERS.json": "bf353b3e05d0bf5fe3e49c15673c4cb9203251329bd594009303541cf7fecc09", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "legacy_payload_sha256": "32d05c4efa4c3f6e3cf08fc9dd21478e0fb5218a38556e290966e64193fe2d80", + "legacy_two_public_move_neighbors": 184, + "moonshot_complete_margin_upper": "-696666928918952751686697170771240598446248488276171/5000000000000000000000000000000000000000000000000", + "old_complete_margin": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "old_crossing_upper": "182332597822022395349777014167081/50000000000000000000000000000000000", + "old_moonshot_margin": [ + "-1397669261708656239100690290777847634192460354758679/10000000000000000000000000000000000000000000000000", + "-698834630854328119550345145388923817096230177350851/5000000000000000000000000000000000000000000000000" + ], + "positive_legacy_before_protection": 20, + "predecessor_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "price_probe": "182332647822022395349777014167081/50000000000000000000000000000000000", + "price_unresolved": [], + "protected_roles": [ + 198, + 205, + 319, + 532, + 652, + 654, + 863, + 962, + 969, + 1081, + 1250, + 1303, + 1305, + 1355, + 1453, + 1467, + 1531, + 1567, + 1568 + ], + "scope": "Exact inherited #7277 one-ADD/four-MOVE signatures, restricted to unprotected productive helpers. No current word or span decoded.", + "whole_compatible_at_incumbent": { + "directed_upper": "1973739006469521087719708807927113391269459778011/5000000000000000000000000000000000000000000000000", + "maximizing_keys": [ + [ + 38408, + 1 + ], + [ + 38411, + 1 + ], + [ + 38476, + 1 + ], + [ + 40895, + 1 + ], + [ + 41575, + 1 + ], + [ + 39129, + 1 + ], + [ + 41941, + 1 + ], + [ + 42623, + 1 + ], + [ + 42946, + 1 + ] + ] + }, + "whole_compatible_at_moonshot": { + "directed_upper": "54192548384384196591199365442080466249542226867/125000000000000000000000000000000000000000000000", + "maximizing_keys": [ + [ + 38408, + 1 + ], + [ + 38411, + 1 + ], + [ + 38476, + 1 + ], + [ + 40895, + 1 + ], + [ + 41575, + 1 + ], + [ + 39129, + 1 + ], + [ + 41941, + 1 + ], + [ + 42623, + 1 + ], + [ + 42946, + 1 + ] + ] + }, + "word_sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +} diff --git a/research/p104-public-four-move-rechart-bound/receipts/REVERSE.json b/research/p104-public-four-move-rechart-bound/receipts/REVERSE.json new file mode 100644 index 0000000000..8517ebcc04 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/receipts/REVERSE.json @@ -0,0 +1,1013 @@ +{ + "case_cap": 9, + "controls": [ + "strict_rank_extension", + "saturated_high_intersection", + "low_union_bound", + "source_read_blocks_adjacency" + ], + "decisions": [ + { + "common_chart_shape_clocks": [ + 38420 + ], + "current_add_clock": 38420, + "current_match_count": 1, + "current_move_clocks": [ + [ + 38418, + 41815 + ], + [ + 38419, + 41219 + ] + ], + "directed_gross_upper": "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 25, + 102, + 136, + 290 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 38408, + 1 + ], + "legacy_add_clock": 38408, + "legacy_move_clocks": [ + [ + 38406, + 41807 + ], + [ + 38407, + 41211 + ] + ], + "legacy_order": [ + "1059:in", + "1427:in", + "ADD", + "1427:out", + "1059:out" + ], + "literal_add": [ + 1059, + 1427, + "-1", + 725 + ], + "low_union_basis": [ + 25, + 102, + 136, + 290 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "old_chart_paths": [ + [ + 341, + 725, + 861 + ], + [ + 594, + 725, + 883 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 3, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "required_rank": 5, + "roles": [ + 1059, + 1427 + ], + "signed_matches": [ + 38420 + ], + "status": "high_intersection_too_small" + }, + { + "common_chart_shape_clocks": [ + 38423 + ], + "current_add_clock": 38423, + "current_match_count": 1, + "current_move_clocks": [ + [ + 38421, + 41209 + ], + [ + 38422, + 39158 + ] + ], + "directed_gross_upper": "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 25, + 102, + 162, + 264 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 38411, + 1 + ], + "legacy_add_clock": 38411, + "legacy_move_clocks": [ + [ + 38409, + 41201 + ], + [ + 38410, + 39146 + ] + ], + "legacy_order": [ + "791:in", + "1232:in", + "ADD", + "1232:out", + "791:out" + ], + "literal_add": [ + 791, + 1232, + "-1", + 726 + ], + "low_union_basis": [ + 25, + 102, + 162, + 264 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "old_chart_paths": [ + [ + 342, + 726, + 862 + ], + [ + 594, + 726, + 884 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 3, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "required_rank": 5, + "roles": [ + 791, + 1232 + ], + "signed_matches": [ + 38423 + ], + "status": "high_intersection_too_small" + }, + { + "common_chart_shape_clocks": [ + 38488 + ], + "current_add_clock": 38488, + "current_match_count": 1, + "current_move_clocks": [ + [ + 38486, + 39535 + ], + [ + 38487, + 39145 + ] + ], + "directed_gross_upper": "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 7, + 75, + 176, + 304 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 38476, + 1 + ], + "legacy_add_clock": 38476, + "legacy_move_clocks": [ + [ + 38474, + 39523 + ], + [ + 38475, + 39133 + ] + ], + "legacy_order": [ + "1150:in", + "1426:in", + "ADD", + "1426:out", + "1150:out" + ], + "literal_add": [ + 1150, + 1426, + "-1", + 759 + ], + "low_union_basis": [ + 7, + 75, + 176, + 304 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "old_chart_paths": [ + [ + 454, + 759, + 825 + ], + [ + 593, + 759, + 852 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 3, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "required_rank": 5, + "roles": [ + 1150, + 1426 + ], + "signed_matches": [ + 38488 + ], + "status": "high_intersection_too_small" + }, + { + "common_chart_shape_clocks": [ + 40903 + ], + "current_add_clock": 40903, + "current_match_count": 1, + "current_move_clocks": [ + [ + 40902, + 42364 + ], + [ + 40901, + 42237 + ] + ], + "directed_gross_upper": "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 25, + 102, + 136, + 290 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 40895, + 1 + ], + "legacy_add_clock": 40895, + "legacy_move_clocks": [ + [ + 40894, + 42356 + ], + [ + 40893, + 42229 + ] + ], + "legacy_order": [ + "490:in", + "296:in", + "ADD", + "490:out", + "296:out" + ], + "literal_add": [ + 490, + 296, + "1", + 725 + ], + "low_union_basis": [ + 25, + 102, + 136, + 290 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "old_chart_paths": [ + [ + 341, + 725, + 861 + ], + [ + 594, + 725, + 883 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 3, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "required_rank": 5, + "roles": [ + 296, + 490 + ], + "signed_matches": [ + 40903 + ], + "status": "high_intersection_too_small" + }, + { + "common_chart_shape_clocks": [ + 41583 + ], + "current_add_clock": 41583, + "current_match_count": 1, + "current_move_clocks": [ + [ + 41582, + 42090 + ], + [ + 41581, + 42259 + ] + ], + "directed_gross_upper": "265763478022961302559088807804310841685552843653/5000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 7, + 75, + 176, + 304 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 41575, + 1 + ], + "legacy_add_clock": 41575, + "legacy_move_clocks": [ + [ + 41574, + 42082 + ], + [ + 41573, + 42251 + ] + ], + "legacy_order": [ + "561:in", + "388:in", + "ADD", + "388:out", + "561:out" + ], + "literal_add": [ + 561, + 388, + "1", + 759 + ], + "low_union_basis": [ + 7, + 75, + 176, + 304 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "old_chart_paths": [ + [ + 454, + 759, + 825 + ], + [ + 593, + 759, + 852 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 3, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -17, + "3": -17, + "4": 17 + }, + "required_rank": 5, + "roles": [ + 388, + 561 + ], + "signed_matches": [ + 41583 + ], + "status": "high_intersection_too_small" + }, + { + "common_chart_shape_clocks": [ + 39141 + ], + "current_add_clock": 39141, + "current_match_count": 1, + "current_move_clocks": [ + [ + 39139, + 39146 + ], + [ + 39140, + 39541 + ] + ], + "directed_gross_upper": "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 7, + 9, + 66, + 400 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 39129, + 1 + ], + "legacy_add_clock": 39129, + "legacy_move_clocks": [ + [ + 39127, + 39134 + ], + [ + 39128, + 39529 + ] + ], + "legacy_order": [ + "1033:in", + "1224:in", + "ADD", + "1033:out", + "1224:out" + ], + "literal_add": [ + 1033, + 1224, + "-1", + 715 + ], + "low_union_basis": [ + 7, + 9, + 66, + 400 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "old_chart_paths": [ + [ + 305, + 715, + 852 + ], + [ + 676, + 715, + 876 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 2, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -34, + "3": 17 + }, + "required_rank": 5, + "roles": [ + 1033, + 1224 + ], + "signed_matches": [ + 39141 + ], + "status": "high_intersection_too_small" + }, + { + "common_chart_shape_clocks": [ + 41949 + ], + "current_add_clock": 41949, + "current_match_count": 1, + "current_move_clocks": [ + [ + 41948, + 42258 + ], + [ + 41947, + 43946 + ] + ], + "directed_gross_upper": "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 7, + 9, + 66, + 400 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 41941, + 1 + ], + "legacy_add_clock": 41941, + "legacy_move_clocks": [ + [ + 41940, + 42250 + ], + [ + 41939, + 43960 + ] + ], + "legacy_order": [ + "471:in", + "270:in", + "ADD", + "270:out", + "471:out" + ], + "literal_add": [ + 471, + 270, + "1", + 715 + ], + "low_union_basis": [ + 7, + 9, + 66, + 400 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "old_chart_paths": [ + [ + 305, + 715, + 852 + ], + [ + 676, + 715, + 876 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 2, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -34, + "3": 17 + }, + "required_rank": 5, + "roles": [ + 270, + 471 + ], + "signed_matches": [ + 41949 + ], + "status": "high_intersection_too_small" + }, + { + "common_chart_shape_clocks": [ + 42629 + ], + "current_add_clock": 42629, + "current_match_count": 1, + "current_move_clocks": [ + [ + 42627, + 42861 + ], + [ + 42628, + 42898 + ] + ], + "directed_gross_upper": "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 30, + 76, + 140, + 268 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 42623, + 1 + ], + "legacy_add_clock": 42623, + "legacy_move_clocks": [ + [ + 42621, + 42855 + ], + [ + 42622, + 42892 + ] + ], + "legacy_order": [ + "1193:in", + "1262:in", + "ADD", + "1193:out", + "1262:out" + ], + "literal_add": [ + 1193, + 1262, + "-1", + 773 + ], + "low_union_basis": [ + 30, + 76, + 140, + 268 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "old_chart_paths": [ + [ + 511, + 773, + 775 + ], + [ + 652, + 773, + 774 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 2, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -34, + "3": 17 + }, + "required_rank": 5, + "roles": [ + 1193, + 1262 + ], + "signed_matches": [ + 42629 + ], + "status": "high_intersection_too_small" + }, + { + "common_chart_shape_clocks": [ + 42952 + ], + "current_add_clock": 42952, + "current_match_count": 1, + "current_move_clocks": [ + [ + 42951, + 43010 + ], + [ + 42950, + 42975 + ] + ], + "directed_gross_upper": "322460808177357287462132384452779591420847779873/10000000000000000000000000000000000000000000000000", + "high_intersection_basis": [ + 30, + 76, + 140, + 268 + ], + "high_intersection_rank": 4, + "high_vector_count": 16, + "key": [ + 42946, + 1 + ], + "legacy_add_clock": 42946, + "legacy_move_clocks": [ + [ + 42945, + 43004 + ], + [ + 42944, + 42969 + ] + ], + "legacy_order": [ + "586:in", + "436:in", + "ADD", + "586:out", + "436:out" + ], + "literal_add": [ + 586, + 436, + "1", + 773 + ], + "low_union_basis": [ + 30, + 76, + 140, + 268 + ], + "low_union_rank": 4, + "low_vector_count": 16, + "new_paid_ranks": [ + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "old_chart_paths": [ + [ + 511, + 773, + 775 + ], + [ + 652, + 773, + 774 + ] + ], + "old_midpoint_rank": 4, + "old_paid_ranks": [ + [ + 1, + 2 + ], + [ + 2, + 2 + ] + ], + "paid_delta": { + "1": 17, + "2": -34, + "3": 17 + }, + "required_rank": 5, + "roles": [ + 436, + 586 + ], + "signed_matches": [ + 42952 + ], + "status": "high_intersection_too_small" + } + ], + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "legacy": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "price": "005efb8329d38638800d82e5273580b1bb529ac490d9923ba1a92e112d31c8b1", + "word": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + }, + "predecessor_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "runner_cap_seconds": 20, + "scope": "Only nine inherited profitable shapes. No search for new current-word contacts.", + "status_counts": { + "high_intersection_too_small": 9 + }, + "survivors": [], + "timeout": null, + "unresolved": [], + "unvisited": [] +} diff --git a/research/p104-public-four-move-rechart-bound/replay.py b/research/p104-public-four-move-rechart-bound/replay.py new file mode 100644 index 0000000000..87664030b1 --- /dev/null +++ b/research/p104-public-four-move-rechart-bound/replay.py @@ -0,0 +1,123 @@ +"""Replay the signed predecessor matching and exact public chart intervals.""" + +from argparse import ArgumentParser +from gzip import decompress +from hashlib import sha1, sha256 +from json import loads +from pathlib import Path +from shutil import copyfile +from subprocess import run +from sys import executable +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def unique(pairs): + value = dict(pairs) + require(len(value) == len(pairs), "duplicate JSON key") + return value + + +def read(raw): + return loads(raw, object_pairs_hook=unique) + + +def authenticate(): + pins = read((HERE / "LOCAL-PINS.json").read_bytes()) + for relative, pin in pins.items(): + path = (HERE / relative).resolve() + require(path.is_relative_to(HERE) and sha256(path.read_bytes()).hexdigest() == pin, + f"changed local dependency {relative}") + provenance = read((HERE / "PROVENANCE.json").read_bytes()) + for relative, entry in provenance["files"].items(): + require(relative in pins, f"unpinned public source {relative}") + raw = (HERE / relative).read_bytes() + if entry["uncompress"]: + raw = decompress(raw) + blob = sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(sha256(raw).hexdigest() == entry["sha256"] and blob == entry["git_blob"], + f"changed public source {relative}") + for relative, entry in provenance["generated"].items(): + require(relative in pins, f"unpinned generated source {relative}") + raw = decompress((HERE / relative).read_bytes()) + require(sha256(raw).hexdigest() == entry["receipt_sha256"], + f"changed predecessor receipt {relative}") + + +def replay(output): + require(__debug__, "assertions must be enabled") + authenticate() + output.mkdir(parents=True, exist_ok=False) + with TemporaryDirectory(prefix="public-four-move-rechart-") as directory: + root = Path(directory) + price_root = root / "preflight" + inputs = price_root / "inputs" + ancestor_root = root / "lead/inputs" + inputs.mkdir(parents=True) + ancestor_root.mkdir(parents=True) + for name in ("ADMITTED.json","READBACK.json","pricing.py","7334-CHANGED.json", + "7277-SUPPORT.json.gz","7334-WORD.json.gz"): + copyfile(HERE / "inputs" / name, inputs / name) + old_word = ancestor_root / "7277-WORD.json.gz" + copyfile(HERE / "inputs/7277-WORD.json.gz", old_word) + cohort = decompress((HERE / "inputs/7314-HELPERS.json.gz").read_bytes()) + (inputs / "7314-HELPERS.json").write_bytes(cohort) + quote = price_root / "quote.py" + copyfile(HERE / "engines/quote.py", quote) + + def stage(name, script, *args): + result = run([executable, "-I", "-B", str(script), *map(str, args)], cwd=root, + check=True, capture_output=True, timeout=22) + require(result.stdout == (HERE / "receipts" / name).read_bytes(), f"changed receipt {name}") + (output / name).write_bytes(result.stdout) + return result.stdout + + raw_price = stage("PRICE.json", quote) + price_path = price_root / "PRICE.json" + price_path.write_bytes(raw_price) + forward_script = HERE / "engines/rechart_gate.py" + raw_forward = stage("FORWARD.json", forward_script, root) + reverse_script = HERE / "engines/reverse_geometry.py" + raw_reverse = stage("REVERSE.json", reverse_script, "--price", price_path, + "--word", inputs / "7334-WORD.json.gz", "--legacy", old_word) + raw_compare = stage("COMPARE.json", HERE / "engines/compare.py", + output / "FORWARD.json", output / "REVERSE.json") + price, forward, reverse, compare = map(read, (raw_price, raw_forward, raw_reverse, raw_compare)) + require(price["head"] == forward["head"] == reverse["head"] == compare["head"] == HEAD + and price["legacy_two_public_move_neighbors"] == 184 and price["allowed_helper_pairs"] == 48 + and len(price["alternatives"]) == 9, "changed source stock") + require(forward["status"] == "EXHAUSTED" and reverse["timeout"] is None and not reverse["unvisited"] + and compare["exact_key_agreements"] == compare["exact_rank_intervals_collapsed_to_old_span"] == 9 + and compare["geometry_survivors"] == compare["unresolved"] == 0, "incomplete exact geometry") + for mutated in (price_path, old_word, inputs / "7334-WORD.json.gz"): + original = mutated.read_bytes() + mutated.write_bytes(original + b"\n") + reject = run([executable, "-I", "-B", str(forward_script), str(root)], cwd=root, + capture_output=True, timeout=8) + require(reject.returncode == 1 and not reject.stdout + and f"changed dependency {mutated.relative_to(root)}".encode() in reject.stderr, + f"changed dependency passed {mutated.relative_to(root)}") + mutated.write_bytes(original) + print("PASS_PUBLIC_FOUR_MOVE_RECHART keys=9 old_rank=4 required_rank=5 excluded=9 unresolved=0 kappa_change=0") + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path) + args = parser.parse_args() + if args.out: + replay(args.out.resolve()) + else: + with TemporaryDirectory(prefix="public-four-move-receipts-") as directory: + replay(Path(directory) / "out") + + +if __name__ == "__main__": + main()