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-owned-zero-rebirth-bound/LOCAL-PINS.json b/research/p104-owned-zero-rebirth-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..9c83fe1c7f --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/LOCAL-PINS.json @@ -0,0 +1,23 @@ +{ + "PROVENANCE.json": "57082f6a8287a6442cdb23a7c81137e06d6aad10402b7b395ec1250699b4e6ba", + "engines/compare_suffix.py": "990ef7b63b57d5fb058e2c1836cf9bc4d0dbfe8d1dd9cc0efb1fa2b9e24e0ab7", + "engines/first_use.py": "9c6130f3810fb6fb2ae3faf09954acc2760a7b1b78634fcb1fa3b12fc0d98016", + "engines/guarded_suffix.py": "bb215850fd11ed5a772173ed0e1c1033df8e63746f7bfad963741ee921a60872", + "engines/lead_suffix.py": "f07dec8ba879247e4e6a09b8af8f47a4b7bbdb192dabc86a1a41e91ed3c99a0a", + "engines/pair_audit.py": "6c22da952b76d2290169a81a64a3ccb246e246bcb30c4707effee31c027b66b0", + "engines/pair_screen.py": "b2648c9811273676a4b0556bdf1452c70d22e30a29ff21c75bce7ca4fe3469be", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/PR7362-SHA256.json": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "inputs/R139-PLAN.md": "b15120eb0538381a6ca30e36cab51e46ff6733fe5a3b5a8cd2c5a25043ce49e5", + "inputs/R140-PLAN.md": "4ffc55e3f4dd8bdb3a78f8b7dce3ce64f4d8ebad005eda463630eaf782b27257", + "inputs/R80-OWNED.json": "db293c67c896f54788681b7a8a9fec5f13da0e31fe5b3dd65fbe30e370ff1d2e", + "inputs/R92-PRICE.json.gz": "2274f514fb12f9ced0c24abe0c02a76c16cfee4c61f909e37a5ad89b07852371", + "inputs/aggregate.py": "8bf1b91d7fc0937305466686522f5fb3920c66c71830acfc94adde84ba4f49e1", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "receipts/PAIR-WITNESSES.json": "20534b54e165646dedb9e4f1e594f6bd8e1aeadd8a7f6fd9788ac7e1ffdf3d05", + "receipts/SHA256.json": "dacc2b20309276d24373a5ccd3bf2c1e734afc28cb949b66776f2bcff282612a", + "receipts/SUFFIX-AGREEMENT.json": "3abd6c0065ea97ef1b0e47cbb1d65ef021004b80f90c9faec38ffcaeb46a40fa", + "replay.py": "8a8eeee313194892c3ada9a0146961ae460b0ee017c125cbd723d10f653f69dd" +} diff --git a/research/p104-owned-zero-rebirth-bound/NOTICE b/research/p104-owned-zero-rebirth-bound/NOTICE new file mode 100644 index 0000000000..2f603bda33 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/NOTICE @@ -0,0 +1,9 @@ +Apache-2.0. + +#7334 and #7113 supply the exact native word and signed caller. #7338 +retains the independent comparator admission. #7362 and #7298 supply +the signed stock and directed tariff. #7355 and #7384 supply the row +and span engines for the earlier R137 proof receipt. #7307, #7308, +#5557 and #7378 supply prior owned-delete, exact replacement, guard, +and write-aggregation evidence. OpenAI Codex and subagents materially +assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-owned-zero-rebirth-bound/PROOF.md b/research/p104-owned-zero-rebirth-bound/PROOF.md new file mode 100644 index 0000000000..470affb57c --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/PROOF.md @@ -0,0 +1,77 @@ +# Fixed-clock owned zero-rebirth observability + +At each exact owned MOVE let Pᵢ be the moved row as a linear form on +the original public inputs. Let Sᵢ be the response to a unit defect +in that owned slot just after the original MOVE. Its observations +are the final public rows and the pre-write destinations of every +later COPY. Earlier guard coordinates in Sᵢ are zero by convention. +The exact normalized MOVE is the identity on its role value. +INIT and CLEAR reset a slot to zero. ADD, COPY and SCALE act with +the original signed rational coefficients. Evaluate COPY as a +linear assignment after recording its pre-write guard. This +relaxation is defined even when a candidate violates the guard. +A legal candidate must preserve both the observations and the +guard preconditions. + +Replacing one MOVE by a CLEAR and zero INIT at the original clock +injects defect −Pᵢ in that slot. The full observation difference is +−SᵢPᵢ. Exact reverse covectors verify a nonzero coordinate of every +Pᵢ. A grouped forward sweep and separate per-site exact sweeps find +a nonzero final public coefficient of every Sᵢ. The independent +engine also pulls each first coefficient back from the final +public output. They agree on the first coefficient and number of +nonzero observations at each site. The sole original COPY is at +clock 33805. All 11 unit defects injected before that clock are +zero at its destination just before the write. No unvisited site +or single-site survivor remains. + +## Two fixed-clock replacements + +Let i < j and let g be the scalar response of the first unit +defect in the second owned slot just after the original MOVE j. +At that point the second slot would hold Pⱼ − gPᵢ after applying +the first edit alone. The second zeroing adds −Pⱼ + gPᵢ in its +slot. The resulting observation difference is + +```text +−Sᵢ Pᵢ − Sⱼ Pⱼ + g Sⱼ Pᵢ. +``` + +If Pᵢ and Pⱼ are linearly independent, choose an input on which +Pᵢ vanishes and Pⱼ does not. The difference is nonzero because +Sⱼ is nonzero. If Sᵢ and Sⱼ are linearly independent, a linear +functional that vanishes on Sⱼ and is nonzero on Sᵢ leaves a +nonzero multiple of Pᵢ. Thus cancellation requires both pairs to +be proportional for any g. + +Exact 2×2 prefix minors exclude 1,073 of 1,081 pairs. Each of the +other eight has a public observation that is zero in exactly +one full suffix column, proving suffix independence. The lead +screen's suffix support counts or first coordinates differ on +these same eight. The independent checks list exact differing +coordinates and coefficients. All pairs close before any +cross-transport or candidate computation. + +This proof grants the normalized replacement even if the two +same-clock lifecycle changes would carry additional costs. A +successful normalized test would still require signed arbitrary-input +and adjoint equality, ownership, restoration, all-width physical and +compiler validity, and charged precision and tape checks. + +## Directed price + +A rank-r deletion saves 17 paid rank-r positions across the +signed caller. A single edit changes the paid count from 110,519 +to 110,502. A pair changes it to 110,485. Productive count stays +22,461 and the rank surplus increases by 17 times the sum of +deleted ranks. No additional paid call is granted in the quote. + +The strongest pair in the literal rank stock has ranks 6 and 5. +Its directed gross upper at the old crossing is 185.838303398540 +raw and its complete margin upper at the fixed moonshot target is +45.956805594899 raw, both rounded upward. The predecode +all-site relaxation bounds gross credit by 1,896.702946936210 raw +at the old crossing and grants all 47 anchors independently. +The exclusions above certify zero realized saving in the tested +single and pair families. The all-site quote is a relaxation; +the pair theorem gives no conclusion for larger simultaneous sets. diff --git a/research/p104-owned-zero-rebirth-bound/PROVENANCE.json b/research/p104-owned-zero-rebirth-bound/PROVENANCE.json new file mode 100644 index 0000000000..4a8caa2aa4 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/PROVENANCE.json @@ -0,0 +1,73 @@ +{ + "caller": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "scope": "Exact retained signed caller. No caller replay is required for this scoped exclusion.", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7113" + }, + "derived_inputs": { + "inputs/R139-PLAN.md": { + "relationship": "Frozen mechanism, exact case cap and next gates.", + "sha256": "b15120eb0538381a6ca30e36cab51e46ff6733fe5a3b5a8cd2c5a25043ce49e5" + }, + "inputs/R140-PLAN.md": { + "relationship": "Frozen mechanism, exact case cap and next gates.", + "sha256": "4ffc55e3f4dd8bdb3a78f8b7dce3ce64f4d8ebad005eda463630eaf782b27257" + }, + "inputs/R80-OWNED.json": { + "relationship": "Sealed earlier #7334 owned MOVE census. The replay independently reproduces all 47 paid ranks." + }, + "inputs/R92-PRICE.json.gz": { + "compression": "gzip", + "key": "R92-PRICE.json", + "receipt": "inputs/PR7362-SHA256.json" + } + }, + "files": { + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "inputs/PR7362-SHA256.json": { + "commit": "5eec7ed633dcf9b9bbc95552aa653da296f863fb", + "git_blob": "b1486e0b5cfe4535f381ed26f7bce4aee21d8a43", + "path": "research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json", + "sha256": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/5eec7ed633dcf9b9bbc95552aa653da296f863fb/research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json" + }, + "inputs/aggregate.py": { + "commit": "4dd0d15c1e94ea3e1ca3c5bd504f6bc142bf7a5e", + "git_blob": "c04096209237b27c7d255f740ea30630895d3c52", + "path": "research/p104-three-move-public-aggregate-bound/engines/aggregate.py", + "sha256": "8bf1b91d7fc0937305466686522f5fb3920c66c71830acfc94adde84ba4f49e1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/4dd0d15c1e94ea3e1ca3c5bd504f6bc142bf7a5e/research/p104-three-move-public-aggregate-bound/engines/aggregate.py" + }, + "inputs/donor_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "46e4621b69bba513f327de53153298e7f4ca0645", + "path": "research/p104-owned-add-source-span-bound/engines/forward.py", + "sha256": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/forward.py" + }, + "inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-owned-zero-rebirth-bound/README.md b/research/p104-owned-zero-rebirth-bound/README.md new file mode 100644 index 0000000000..3f10231ab9 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/README.md @@ -0,0 +1,72 @@ +# Owned zero-rebirth suffix bounds + +**NO VERIFIED GAIN.** Conditional κ remains `0.00364665195644` +on the independently reproduced complete comparator +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +`aaeec8c0acf01e99a5f331ef363a698d9c084ace` with exact signed +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +`07a76c5e2738882c0cb322278e56f6cae3c9885d`. Exact Δκ is zero. + +At each paid owned MOVE, grant a same-clock CLEAR at the old chart +and fresh zero INIT at the destination chart. Keep every other +event, sign and coefficient fixed. All 47 single-site edits change +a final public row. Of 1,081 unordered pairs, 1,073 have independent +original moved rows. The other eight have independently checked +distinct final-public response supports. Every pair is excluded +even when granting arbitrary cross-transport between both sites. +[Proof](PROOF.md) · [Pair witnesses](receipts/PAIR-WITNESSES.json). + +## Replay + +From a clean checkout, use POSIX CPython 3.12 with assertions. + +```sh +python3.12 -I -B research/p104-owned-zero-rebirth-bound/replay.py +``` + +The standard-library command authenticates the exact word, signed +invoice and predecessor source, regenerates nine deterministic +receipts, and rejects two altered dependencies. Use +`--out fresh-directory` to retain the receipts. No Git metadata, +network, external source root or prior temporary state is required. +[Provenance](PROVENANCE.json) · [Pins](LOCAL-PINS.json) · +[Verification](VERIFICATION.md). + +## Open next questions + +Could one ordinary correction at a specified legal coframe restore +every affected public row and clean-write guard within the +incumbent ordinary-work envelope? Start with a receiver whose full +guarded suffix response is known. Larger zeroing subsets, changed +times or coefficients, replacement donor writes, and changes to +the caller remain open. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +and [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +supply the exact native word and signed caller. +[#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) +retains the independent comparator admission. +[#7362](https://github.com/CrocSwap/integer-mult-bounds/pull/7362) +supplies the exact signed stock and +[#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +supplies the directed tariff. +[#7355](https://github.com/CrocSwap/integer-mult-bounds/pull/7355) +and [#7384](https://github.com/CrocSwap/integer-mult-bounds/pull/7384) +supply the exact row and span engines used to rebuild the R137 +predecessor rows. + +[#7307](https://github.com/CrocSwap/integer-mult-bounds/pull/7307) +checks direct dead owned MOVEs on #7277. +[#7308](https://github.com/CrocSwap/integer-mult-bounds/pull/7308) +checks immediate owned-row replacement on that older word. +[#5557](https://github.com/CrocSwap/integer-mult-bounds/pull/5557) +establishes earlier residual-preserving checks that motivate +the clean-write observables. +[#7378](https://github.com/CrocSwap/integer-mult-bounds/pull/7378) +checks a two-write aggregate while retaining the original dirty owner. +The present replay tests complete suffix observability for fresh zero +replacement on exact #7334. +OpenAI Codex and subagents materially assisted proof, implementation, +independent verification and packaging. diff --git a/research/p104-owned-zero-rebirth-bound/SOURCES.json b/research/p104-owned-zero-rebirth-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-owned-zero-rebirth-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-owned-zero-rebirth-bound/TASK.json b/research/p104-owned-zero-rebirth-bound/TASK.json new file mode 100644 index 0000000000..0c10b5a09b --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact single-site and two-site deletions of paid owned MOVEs replaced at the original clocks by CLEAR and fresh destination INIT. All other word operations and the signed caller are fixed.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 owned zero-rebirth research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A zero-rebirth edit could remove one or two charged owned MOVEs while retaining the complete productive stock.", + "budget_minutes": 8, + "evidence": "All 47 moved rows and complete guarded suffix columns are nonzero. Exact prefix minors exclude 1,073 pairs. Exact differing suffix coordinates exclude the other eight.", + "open_questions": [ + { + "blocked_by": "Each single or paired edit changes at least one required observation in the unchanged suffix.", + "first_step": "Preprice one exact compensating correction event using a receiver with known nonzero suffix response.", + "question": "Can one exact permitted correction restore the changed public response and every clean-write guard?", + "why_it_matters": "A correction that remains within the incumbent ordinary-work envelope can preserve the paid debit." + } + ], + "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": "Test complete guarded suffix observability of a new zero row instead of reconstructing the original row at a local contact.", + "scope_status": "changed", + "stop_rule": "47 sites of the 76,466-event native word under 25 runner seconds per suffix engine. Then all 1,081 pairs under 10 seconds using frozen prefix and suffix receipts. No further native test after all pair projective gates fail.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-owned-zero-rebirth-bound/VERIFICATION.md b/research/p104-owned-zero-rebirth-bound/VERIFICATION.md new file mode 100644 index 0000000000..f5c7277f3a --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/VERIFICATION.md @@ -0,0 +1,26 @@ +# Verification + +Direct CPython 3.12.14 replay exited 0 in 6.50 seconds. A relocated +Git-free copy in a cleared environment exited 0 in 6.13 seconds +and reproduced all nine receipts byte for byte. Mutating either +the single-site price or the independent suffix receipt rejects. +The price mutation is rejected even when the native word is absent. + +The package regenerates the exact R137 moved rows, both directed +prices, both guarded suffix results, their agreement and both +pair screens. The independent single-site engine computes an +exact reverse prefix coefficient and a separate exact suffix +column for every site. A second reverse pullback checks the first +nonzero output coefficient. Both engines agree on all 47 keys, +first signed coefficients and observable counts. The independent +pair engine recomputes a nonzero 2×2 minor for each of 1,073 +pairs and checks exact distinguishing output coordinates for +the other eight. Synthetic controls cover exact cancellation, +a surviving public defect, a dirty COPY guard and a reverse +prefix coefficient. + +This is a replay of the scoped obstructions under the inherited +word and caller. No new literal operator, signed caller or +complete conditional bound was constructed. + +[Replay](README.md) · [Exact receipts](receipts/SHA256.json). diff --git a/research/p104-owned-zero-rebirth-bound/VERIFY.json b/research/p104-owned-zero-rebirth-bound/VERIFY.json new file mode 100644 index 0000000000..9041b67a0f --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Rebuild signed quotes and exact single-site and pair guarded-response exclusions. Compare independent receipts and reject altered inputs.", + "timeout_seconds": 180 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-owned-zero-rebirth-bound/engines/compare_suffix.py b/research/p104-owned-zero-rebirth-bound/engines/compare_suffix.py new file mode 100644 index 0000000000..5a8ce4d530 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/engines/compare_suffix.py @@ -0,0 +1,32 @@ +"""Check the exact full-suffix and independent receipts key by key.""" +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +LEAD = "c81636f5fe4a5db1cb31220b451e400f2eb86af6dc3480235b7cfd34d09a8f40" +lead_bytes = (ROOT/"inputs/R139-LEAD-RESULT.json").read_bytes() +assert sha256(lead_bytes).hexdigest() == LEAD +a = loads(lead_bytes) +b_bytes = (ROOT/"RESULT.json").read_bytes() +b = loads(b_bytes) +assert (a["head"],a["caller"]) == (b["head"],b["caller"]) +assert not a["survivors"] and not a["unresolved"] and not b["unvisited"] +assert b["counts"] == {"excluded":47} and a["COPY_clocks"] == b["copy_clocks"] == [33805] +firsts = {r["move_clock"]:r for r in a["rows"]} +assert len(firsts) == len(a["rows"]) == len(b["cases"]) == 47 +checks = [] +for row in b["cases"]: + clock = row["move_clock"] + lead = firsts.pop(clock) + assert lead["key"] == [row[k] for k in ("role","before","after","rank")] + assert lead["observable_count"] == len(row["final_public"]) + len(row["copy_guards"]) + assert lead["first"] == ["public"] + row["final_public"][0] + assert row["reverse_first_public"] == row["final_public"][0] + assert not row["copy_guards"] + checks.append([clock,*lead["first"][1:],lead["observable_count"]]) +assert not firsts +print(dumps({"agrees":True,"checked":checks,"head":a["head"],"lead_sha256":LEAD, + "independent_sha256":sha256(b_bytes).hexdigest(), + "copy_guard_checks":sum(c[0]<33805 for c in checks),"copy_guard_nonzero":0, + "unresolved":0},indent=2,sort_keys=True)) diff --git a/research/p104-owned-zero-rebirth-bound/engines/first_use.py b/research/p104-owned-zero-rebirth-bound/engines/first_use.py new file mode 100644 index 0000000000..53f44eff7c --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/engines/first_use.py @@ -0,0 +1,151 @@ +"""Authenticate, price and check the first-use owned reconstruction stock.""" +from collections import Counter,defaultdict +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/R80-OWNED.json":"db293c67c896f54788681b7a8a9fec5f13da0e31fe5b3dd65fbe30e370ff1d2e", + "inputs/R92-PRICE.json":"05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/aggregate.py":"8bf1b91d7fc0937305466686522f5fb3920c66c71830acfc94adde84ba4f49e1", + "inputs/donor_span.py":"4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "inputs/pricing.py":"f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", +} + + +def unique(pairs): + obj=dict(pairs) + if len(obj)!=len(pairs): + raise ValueError("duplicate JSON key") + return obj + + +def read(path): + data=(ROOT/path).read_bytes() + if sha256(data).hexdigest()!=PINS[path]: + raise ValueError(f"changed dependency {path}") + return data + + +def quote(): + old, owned=(loads(read(p),object_pairs_hook=unique) + for p in ("inputs/R92-PRICE.json","inputs/R80-OWNED.json")) + assert old["head"]==owned["head"]=="aaeec8c0acf01e99a5f331ef363a698d9c084ace" + assert old["caller_head"]=="07a76c5e2738882c0cb322278e56f6cae3c9885d" + assert old["word_sha256"]==owned["word_sha256"]==PINS["inputs/7334-WORD.json.gz"] + stock=Counter({int(r):v for r,v in owned["paid_owned_rank"].items()}) + assert sum(stock.values())==47 + paid,target=(Counter({int(k):v for k,v in old[field].items()}) for field in ("old_paid","old_targets")) + assert (sum(paid.values()),sum(target.values()))==(110519,22461) + target.subtract(paid) + assert sum(r*n for r,n in target.items())==1424 + read("inputs/pricing.py") + cost=run_path(str(ROOT/"inputs/pricing.py"))["cost"] + at,probe,moon=(Q(old[k]) for k in ("old_crossing_upper","probe","moonshot")) + one={} + for r in stock: + delta={r:17} + profile=target.copy() + profile.update(delta) + margin=cost(profile,probe) + assert margin[0]>0 + one[r]=dict(paid_delta={r:-17},productive_delta={},gross=list(map(str,cost(delta,at))), + complete_probe=list(map(str,margin)),paid=110502,productive=22461,surplus=1424+17*r) + all_delta={r:17*n for r,n in stock.items()} + all_profile=target.copy() + all_profile.update(all_delta) + return dict(head=old["head"],caller=old["caller_head"],pins=PINS,one=one,stock=stock, + whole_gross_upper=str(cost(all_delta,at)[1]),fixed_target_upper=str(cost(all_profile,moon)[1]), + case_cap=47,event_cap=76466,runner_seconds=35) + + +def first_contacts(word,p): + tape=word["program"] + n=word["public"] + seen={} + records=[] + ranks=Counter() + for t,(op,r,*a) in enumerate(tape): + touch=[r] + if op in {"ADD","COPY"}: + touch.append(a[0]) + for j in touch: + if j in seen: + old=seen.pop(j) + records.append(dict(**old,first_clock=t,first_event=tape[t])) + if op=="MOVE" and a[2]: + assert r>=n + rank=abs(len(word["frames"][a[0]])-len(word["frames"][a[1]])) + assert rank>0 + ranks[rank]+=1 + seen[r]=dict(role=r,move_clock=t,chart_from=a[0],chart_to=a[1],rank=rank) + assert not seen and ranks==p["stock"] and len(records)==47 + return sorted(records,key=lambda x:(-x["rank"],x["move_clock"])) + + +def main(): + assert __debug__ + p=quote() + if sys.argv[1:]==["--price-only"]: + print(dumps(p,indent=2,sort_keys=True)) + return + assert not sys.argv[1:] + deadline=monotonic()+32 + raw=decompress(read("inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest()=="9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + word=loads(raw,object_pairs_hook=unique) + assert len(word["program"])==p["event_cap"] + records=first_contacts(word,p) + ask,refs=defaultdict(set),defaultdict(set) + for record in records: + op=record["first_event"][0] + t,r,c=record["first_clock"],record["role"],record["chart_to"] + if op in {"ADD","SCALE"}: + assert record["first_event"][-1]==c + ask[t].add((c,r)) + refs[t].add(r) + read("inputs/donor_span.py") + read("inputs/aggregate.py") + helper=run_path(str(ROOT/"inputs/donor_span.py")) + solve=run_path(str(ROOT/"inputs/aggregate.py")) + tests=solve["controls"](helper) + banks,values=helper["snapshot"](word,ask,refs,deadline) + for row in records: + t,r,c=row["first_clock"],row["role"],row["chart_to"] + key=t,c,r + row["delay_events"]=t-row["move_clock"]-1 + if row["first_event"][0] not in {"ADD","SCALE"}: + row["disposition"]="first contact outside scope" + continue + if key not in banks or (t,r) not in values or monotonic()>=deadline: + row["disposition"]="capped" + continue + target=values[t,r] + bank=banks[key] + answer=solve["exact_span"](target,bank,deadline,helper) + if answer is None: + row["disposition"]="capped" + continue + if "rank" in answer: + answer["span_rank"] = answer.pop("rank") + row.update(answer) + row["disposition"]=row.pop("decision") + row["bank_roles"]=sorted(bank) + row["row"]={i:str(q) for i,q in target.items()} + counts=Counter(r["disposition"] for r in records) + print(dumps(dict(head=p["head"],caller=p["caller"],pins=PINS,controls=tests,counts=counts, + records=records,unvisited=[r["move_clock"] for r in records if r["disposition"]=="capped"]), + indent=2,sort_keys=True)) + if counts["capped"]: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-owned-zero-rebirth-bound/engines/guarded_suffix.py b/research/p104-owned-zero-rebirth-bound/engines/guarded_suffix.py new file mode 100644 index 0000000000..e65895303f --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/engines/guarded_suffix.py @@ -0,0 +1,228 @@ +"""Independently test each owned zero-rebirth in a separate exact suffix walk.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parent +PINS = { + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/R137-RESULT.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "inputs/R137-PRICE.json": "1e8270d9a48728327f7eab9610a272fbb8ef09518dc4ddc5ceb573be00ae2beb", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +CASES, EVENTS, SECONDS = 47, 76466, 25 +ZERO, ONE = Q(0), Q(1) + + +def unique(pairs): + answer = dict(pairs) + if len(answer) != len(pairs): + raise ValueError("duplicate JSON key") + return answer + + +def authenticate(root, path, digest): + data = (root / path).read_bytes() + if sha256(data).hexdigest() != digest: + raise ValueError("changed dependency " + path) + return data + + +def add(vector, role, value): + if value: + total = vector.get(role, ZERO) + value + if total: + vector[role] = total + else: + vector.pop(role, None) + + +@lru_cache(maxsize=None) +def scalar(token): + return Q(token) + + +def pullback(tape, cut, role, coordinate, lower=0): + """One coefficient of a prefix or suffix, computed as a reverse covector.""" + covector = {role: ONE} + for clock in range(cut - 1, lower - 1, -1): + op, dst, *args = tape[clock] + if dst not in covector: + continue + value = covector[dst] + if op in ("INIT", "CLEAR"): + del covector[dst] + elif op == "SCALE": + covector[dst] = value * scalar(args[0]) + elif op in ("ADD", "COPY"): + if op == "COPY": + del covector[dst] + add(covector, args[0], value * scalar(args[1])) + else: + assert op == "MOVE" + return covector.get(coordinate, ZERO) + + +def suffix(tape, cut, role, public): + """One exact response column. Guard values are observed before writes.""" + effect = {role: ONE} + guards = [] + for clock in range(cut, len(tape)): + if not effect: + break + op, dst, *args = tape[clock] + if op == "ADD": + incoming = effect.get(args[0], ZERO) + if incoming: + add(effect, dst, incoming * scalar(args[1])) + elif op == "COPY": + dirty = effect.pop(dst, ZERO) + if dirty: + guards.append([clock, dst, str(dirty)]) + incoming = effect.get(args[0], ZERO) + if incoming: + effect[dst] = incoming * scalar(args[1]) + elif op in ("INIT", "CLEAR"): + effect.pop(dst, None) + elif op == "SCALE" and dst in effect: + effect[dst] *= scalar(args[0]) + else: + assert op in ("MOVE", "SCALE") + assert all(r < public for r in effect) + return guards, [[r, str(value)] for r, value in sorted(effect.items())] + + +def controls(): + # Public response can cancel even though there are literal outward reads. + assert suffix([["ADD",0,2,"1",4], ["ADD",0,2,"-1",4], + ["CLEAR",2,4]], 0, 2, 2) == ([], []) + # COPY consumes the original clean destination before overwriting it. + assert suffix([["COPY",2,1,"1/2",4], ["CLEAR",2,4]], 0, 2, 2) == ( + [[0,2,"1"]], []) + assert suffix([["ADD",1,2,"-3/2",4], ["CLEAR",2,4]], 0, 2, 2) == ( + [], [[1,"-3/2"]]) + assert pullback([["INIT",2,4], ["COPY",2,0,"-1/2",4], + ["ADD",2,1,"3/4",4]], 3, 2, 0) == Q(-1,2) + return ["cancellation", "pre-COPY guard", "signed public response", "reverse prefix coefficient"] + + +def census(word): + tape = word["program"] + public = word["public"] + owned = word["owned_fields"] + assert (public, owned, len(tape)) == (1501, 68, EVENTS) + frames = word["frames"] + active = word["initial"] + [None] * owned + anchors = {} + for clock, (op, dst, *args) in enumerate(tape): + if op == "MOVE": + before, after, is_owned = args + assert active[dst] == before and is_owned == (dst >= public) + rank = abs(len(frames[before]) - len(frames[after])) + assert rank + active[dst] = after + if is_owned: + anchors[clock] = (dst, before, after, rank) + elif op == "INIT": + assert dst >= public and active[dst] is None + active[dst] = args[0] + elif op == "CLEAR": + assert dst >= public and active[dst] == args[0] + active[dst] = None + else: + assert op in ("ADD", "COPY", "SCALE") + assert active[dst] == args[-1] + if op != "SCALE": + assert active[args[0]] == args[-1] and dst != args[0] + if op == "COPY": + assert dst >= public + assert active == word["final"] + [None] * owned + assert len(anchors) == CASES + return anchors + + +def main(): + assert __debug__ + cli = ArgumentParser(description=__doc__) + cli.add_argument("--root", type=Path, default=ROOT) + cli.add_argument("--price-sha") + cli.add_argument("--controls-only", action="store_true") + args = cli.parse_args() + tests = controls() + if args.controls_only: + print(dumps(tests)) + return + if not args.price_sha: + cli.error("requires the frozen R139 price SHA-256") + paths = {"inputs/R139-PRICE.json": args.price_sha} | PINS + payloads = {p: authenticate(args.root, p, digest) for p, digest in paths.items()} + predecessor = loads(payloads["inputs/R137-RESULT.json"], object_pairs_hook=unique) + old_price = loads(payloads["inputs/R137-PRICE.json"], object_pairs_hook=unique) + price = loads(payloads["inputs/R139-PRICE.json"], object_pairs_hook=unique) + assert all(p["head"] == HEAD and p["caller"] == CALLER + for p in (predecessor, old_price, price)) + assert price["case_cap"] == CASES and price["event_cap"] == EVENTS + by_clock = {r["move_clock"]:r for r in predecessor["records"]} + assert len(by_clock) == CASES and not predecessor["unvisited"] + result = dict(head=HEAD, caller=CALLER, caps=dict(events=EVENTS,cases=CASES,seconds=SECONDS), + pins=paths, controls=tests, cases=[], unvisited=sorted(by_clock)) + + def stop(*_): + raise TimeoutError("25-second hard limit") + + signal(SIGALRM, stop) + alarm(SECONDS) + deadline = monotonic() + SECONDS - 1 + try: + raw = decompress(payloads["inputs/7334-WORD.json.gz"]) + assert sha256(raw).hexdigest() == PAYLOAD + word = loads(raw, object_pairs_hook=unique) + anchors = census(word) + result["copy_clocks"] = [clock for clock,event in enumerate(word["program"]) if event[0] == "COPY"] + assert anchors.keys() == by_clock.keys() + assert {str(clock):list(key) for clock,key in anchors.items()} == price["keys"] + assert price["seconds_cap"] == SECONDS + assert Counter(a[3] for a in anchors.values()) == { + int(k):v for k,v in old_price["stock"].items()} + for clock, (role, before, after, rank) in sorted(anchors.items()): + if monotonic() >= deadline: + raise TimeoutError("before next case") + old = by_clock[clock] + assert (role,before,after,rank) == ( + old["role"],old["chart_from"],old["chart_to"],old["rank"]) + assert old["row"] + coordinate = min(map(int,old["row"])) + value = pullback(word["program"], clock, role, coordinate) + assert value and value == Q(old["row"][str(coordinate)]) + guards, outputs = suffix(word["program"], clock + 1, role, word["public"]) + first = None + if outputs: + target, response = outputs[0] + assert pullback(word["program"], EVENTS, target, role, clock + 1) == Q(response) + first = [target,response] + result["cases"].append(dict(move_clock=clock,role=role,before=before,after=after,rank=rank, + moved_witness=[coordinate,str(value)], copy_guards=guards, final_public=outputs, + reverse_first_public=first, + decision=("excluded" if guards or outputs else "support survivor"))) + result["unvisited"].remove(clock) + except TimeoutError as error: + result["stopped"] = str(error) + finally: + alarm(0) + result["counts"] = dict(Counter(r["decision"] for r in result["cases"])) + print(dumps(result, indent=2, sort_keys=True)) + if result["unvisited"]: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-zero-rebirth-bound/engines/lead_suffix.py b/research/p104-owned-zero-rebirth-bound/engines/lead_suffix.py new file mode 100644 index 0000000000..597c1ba4b6 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/engines/lead_suffix.py @@ -0,0 +1,138 @@ +"""Propagate independent owned-MOVE defect tags through the full word.""" +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 +import sys +from time import monotonic + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/PRICE.json":"1e8270d9a48728327f7eab9610a272fbb8ef09518dc4ddc5ceb573be00ae2beb", + "inputs/RESULT.json":"a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", +} + + +def unique(items): + x=dict(items) + if len(x)!=len(items): + raise ValueError("duplicate JSON key") + return x + + +def read(path): + raw=(ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def quote(): + p,r=(loads(read(path),object_pairs_hook=unique) for path in ("inputs/PRICE.json","inputs/RESULT.json")) + assert p["head"]==r["head"] and p["caller"]==r["caller"] + assert r["counts"]=={"outside donor span":47} + assert all(row["row"] and Q(row["separator_value"]) for row in r["records"]) + keys={row["move_clock"]:[row["role"],row["chart_from"],row["chart_to"],row["rank"]] for row in r["records"]} + assert len(keys)==47 and all(Q(p["one"][str(a[3])]["complete_probe"][0])>0 for a in keys.values()) + return dict(head=p["head"],caller=p["caller"],pins=PINS,keys=keys,quotes=p["one"], + whole_gross_upper=p["whole_gross_upper"],fixed_target_upper=p["fixed_target_upper"], + event_cap=76466,case_cap=47,seconds_cap=25) + + +@cache +def scalar(value): + return Q(value) + + +def axpy(dst,src,q): + for j,c in src.items(): + value=dst.get(j,0)+q*c + if value: + dst[j]=value + else: + dst.pop(j,None) + + +def sweep(w,p): + n=w["public"] + state=w["initial"]+[None]*w["owned_fields"] + values=[{} for _ in state] + guards={} + visited=set() + deadline=monotonic()+22 + assert len(w["program"])==p["event_cap"] + for t,(op,r,*a) in enumerate(w["program"]): + if t%128==0 and monotonic()>=deadline: + return dict(first_unvisited_event=t,unresolved=sorted(p["keys"])) + c=state[r] + if op=="MOVE": + assert a[0]==c and a[2]==(r>=n) + state[r]=a[1] + if a[2]: + q=abs(len(w["frames"][a[0]])-len(w["frames"][a[1]])) + assert p["keys"][t]==[r,a[0],a[1],q] + assert t not in values[r] + values[r][t]=Q(1) + visited.add(t) + elif op=="INIT": + assert r>=n and c is None and not values[r] + state[r]=a[0] + elif op=="CLEAR": + assert r>=n and c==a[0] + state[r]=None + values[r]={} + elif op=="SCALE": + assert c==a[-1] and scalar(a[0]) + values[r]={j:q*scalar(a[0]) for j,q in values[r].items()} + else: + s,scale,chart=a + assert s!=r and state[s]==c==chart and op in {"COPY","ADD"} + if op=="COPY": + assert r>=n + guards[t]=values[r].copy() + values[r]={} + axpy(values[r],values[s],scalar(scale)) + assert state==w["final"]+[None]*w["owned_fields"] and visited==set(p["keys"]) + assert not any(values[n:]) + columns={t:[] for t in visited} + for label,source in (("public",enumerate(values[:n])),("COPY guard",guards.items())): + for coordinate,vec in source: + for t,value in vec.items(): + columns[t].append([label,coordinate,str(value)]) + return dict(first_unvisited_event=None,unresolved=[],COPY_clocks=sorted(guards), + rows=[dict(move_clock=t,key=p["keys"][t],observable_count=len(v),first=v[0] if v else None) + for t,v in sorted(columns.items())], + survivors=[t for t,v in sorted(columns.items()) if not v]) + + +def controls(): + out={} + axpy(out,{4:Q(3)},Q(2)) + axpy(out,{4:Q(1)},Q(-6)) + assert not out + axpy(out,{4:Q(1)},Q(1)) + assert out=={4:Q(1)} + return ["exact cancellation","wrong coefficient exposes a tag"] + + +def main(): + assert __debug__ + p=quote() + if sys.argv[1:]==["--price-only"]: + print(dumps(p,indent=2,sort_keys=True)) + return + assert not sys.argv[1:] + raw=decompress(read("inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest()=="9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + out=sweep(loads(raw,object_pairs_hook=unique),p) + print(dumps(dict(head=p["head"],caller=p["caller"],pins=PINS,controls=controls(),**out), + indent=2,sort_keys=True)) + if out["unresolved"]: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-owned-zero-rebirth-bound/engines/pair_audit.py b/research/p104-owned-zero-rebirth-bound/engines/pair_audit.py new file mode 100644 index 0000000000..5ab1f95e68 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/engines/pair_audit.py @@ -0,0 +1,81 @@ +"""Cross-check the frozen pairs using exact prefix minors and full suffix supports.""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations +from json import dumps, loads +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +PINS = { + "R140-PRICE.json": "47a1e9f2a704bfe98f16cf4e36f1f592789595db211f6bb149dc77c026b6fb20", + "R137-RESULT.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "R139-INDEPENDENT-RESULT.json": "ad45f533e423dbd1edffa84c3848ed1beaf2cd9b7e32feb5ce2f4a3deb84eddc", + "R140-LEAD-RESULT.json": "2d07bdb7d32b1a50eb23e8af75eed40585f181fe924641298c1089518e6763b2", +} + + +def load(name): + raw = (ROOT/"inputs"/name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError("changed dependency "+name) + return loads(raw) + + +def minor(left, right): + """Return coordinates with a nonzero 2x2 minor, if one exists.""" + assert left and right + x = min(left) + a, b = left[x], right.get(x, 0) + for y in sorted(left.keys() | right.keys()): + value = a * right.get(y,0) - b * left.get(y,0) + if value: + return [x,y,str(value)] + return None + + +def column(row): + return {("public",r):Fraction(v) for r,v in row["final_public"]} | { + ("COPY guard",t):Fraction(v) for t,_,v in row["copy_guards"]} + + +def main(): + assert __debug__ + assert minor({1:2,2:3},{1:-2,2:-3}) is None + assert minor({1:2,2:3},{1:-2,2:-4}) == [1,2,"-2"] + price, prefix, suffix, lead = map(load, PINS) + assert all((x["head"],x["caller"])==(price["head"],price["caller"]) + for x in (prefix,suffix,lead)) + assert not prefix["unvisited"] and not suffix["unvisited"] and not lead["unresolved"] + pre = {r["move_clock"]:{int(i):Fraction(v) for i,v in r["row"].items()} + for r in prefix["records"]} + post = {r["move_clock"]:column(r) for r in suffix["cases"]} + expected = {tuple(r["clocks"]):r["disposition"] for r in lead["cases"]} + assert pre.keys() == post.keys() and len(pre) == 47 + assert all(pre.values()) and all(post.values()) + assert len(expected) == price["case_cap"] == 1081 + counts = Counter() + rank_witnesses = [] + for i,j in combinations(sorted(pre),2): + m = minor(pre[i],pre[j]) + decision = expected.pop((i,j)) + if m: + assert decision == "independent prefix rows" + else: + assert decision == "different guarded suffix support" + symmetric_difference = sorted(post[i].keys() ^ post[j].keys()) + assert symmetric_difference + k = symmetric_difference[0] + assert bool(post[i].get(k)) != bool(post[j].get(k)) + rank_witnesses.append({"clocks":[i,j], "observable":list(k), + "coefficients":[str(c.get(k,0)) for c in (post[i],post[j])], + "support_sizes":[len(c) for c in (post[i],post[j])]}) + counts[decision] += 1 + assert not expected + print(dumps({"head":price["head"],"caller":price["caller"],"pins":PINS, + "cases":sum(counts.values()),"counts":counts,"exact_suffix_witnesses":rank_witnesses, + "unresolved":[]},indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-zero-rebirth-bound/engines/pair_screen.py b/research/p104-owned-zero-rebirth-bound/engines/pair_screen.py new file mode 100644 index 0000000000..dc827e862e --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/engines/pair_screen.py @@ -0,0 +1,93 @@ +"""Exact projective screening of the 1081 two-site owned zeroings.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import combinations +from json import dumps,loads +from pathlib import Path +from runpy import run_path +import sys + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "inputs/R137-PRICE.json":"1e8270d9a48728327f7eab9610a272fbb8ef09518dc4ddc5ceb573be00ae2beb", + "inputs/R137-RESULT.json":"a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "inputs/R139-RESULT.json":"c81636f5fe4a5db1cb31220b451e400f2eb86af6dc3480235b7cfd34d09a8f40", + "inputs/R92-PRICE.json":"05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/pricing.py":"f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", +} + + +def unique(items): + out=dict(items) + if len(out)!=len(items): + raise ValueError("duplicate JSON key") + return out + + +def read(path): + raw=(ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def load(path): + return loads(read(path),object_pairs_hook=unique) + + +def quote(): + a,b=load("inputs/R137-PRICE.json"),load("inputs/R92-PRICE.json") + assert a["head"]==b["head"] and a["caller"]==b["caller_head"] + stock=Counter({int(r):v for r,v in a["stock"].items()}) + ranks=sorted(stock.elements(),reverse=True) + assert len(ranks)==47 and ranks[:2]==[6,5] + read("inputs/pricing.py") + cost=run_path(str(ROOT/"inputs/pricing.py"))["cost"] + delta={r:17 for r in ranks[:2]} + profile=Counter({int(r):n for r,n in b["old_targets"].items()}) + profile.subtract({int(r):n for r,n in b["old_paid"].items()}) + profile.update(delta) + at,moon=Q(b["old_crossing_upper"]),Q(b["moonshot"]) + return dict(head=a["head"],caller=a["caller"],pins=PINS,case_cap=1081,max_edits=2, + best_ranks=ranks[:2],paid=110485,productive=22461, + max_gross_upper=str(cost(delta,at)[1]),fixed_target_complete_upper=str(cost(profile,moon)[1])) + + +def line(row): + first=min(row,key=int) + d=Q(row[first]) + return tuple((i,str(Q(x)/d)) for i,x in sorted(row.items(),key=lambda p:int(p[0]))) + + +def screen(price): + pre,post=load("inputs/R137-RESULT.json"),load("inputs/R139-RESULT.json") + assert pre["head"]==post["head"]==price["head"] and not post["survivors"] and not post["unresolved"] + row={r["move_clock"]:r for r in pre["records"]} + col={r["move_clock"]:r for r in post["rows"]} + assert len(row)==len(col)==47 and set(row)==set(col) + assert all(col[t]["key"]==[a["role"],a["chart_from"],a["chart_to"],a["rank"]] for t,a in row.items()) + prefix={t:line(a["row"]) for t,a in row.items()} + suffix={t:(a["observable_count"],tuple(a["first"][:2])) for t,a in col.items()} + assert line({"2":"3","6":"-1"})==line({"2":"-6","6":"2"}) + assert line({"2":"3","6":"-1"})!=line({"2":"-6","6":"3"}) + cases=[] + for i,j in combinations(sorted(row),2): + if prefix[i]!=prefix[j]: + decision="independent prefix rows" + elif suffix[i]!=suffix[j]: + decision="different guarded suffix support" + else: + decision="unresolved exact cross transport" + cases.append(dict(clocks=[i,j],disposition=decision)) + assert len(cases)==price["case_cap"] + return dict(head=price["head"],caller=price["caller"],pins=PINS, + cases=cases,counts=Counter(r["disposition"] for r in cases), + unresolved=[r["clocks"] for r in cases if r["disposition"]=="unresolved exact cross transport"]) + + +if __name__=="__main__": + assert __debug__ + p=quote() + assert not sys.argv[1:] or sys.argv[1:]==["--price-only"] + print(dumps(p if sys.argv[1:] else screen(p),indent=2,sort_keys=True)) diff --git a/research/p104-owned-zero-rebirth-bound/inputs/7334-WORD.json.gz b/research/p104-owned-zero-rebirth-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-owned-zero-rebirth-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-owned-zero-rebirth-bound/inputs/ADMITTED.json b/research/p104-owned-zero-rebirth-bound/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-owned-zero-rebirth-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-owned-zero-rebirth-bound/inputs/PR7362-SHA256.json b/research/p104-owned-zero-rebirth-bound/inputs/PR7362-SHA256.json new file mode 100644 index 0000000000..b1486e0b5c --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/inputs/PR7362-SHA256.json @@ -0,0 +1,11 @@ +{ + "R92-COMPARE.json": "92bd567e3203a2cbc2e0c508bf921966c59ead267c1f373f7534a4a50cb208ac", + "R92-GEOMETRY.json": "e9f93f3271855012b2de705c70f186f78c31a369d28110e92c5f2ffadae209b3", + "R92-GUARDS.json": "c23e9c74b3479e4af6c452eeb73e000878148ec385560a0642433a1c5bac4a07", + "R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "R92-REVERSE.json": "f8e56b109352e07dfb8203bdbe42a10cb94374246b4cd419421e4f52e2730c4a", + "R93-COMPARE.json": "8a1f52179e5d457aa729714b0b79577894c1e22ab74a8b2f700838f471ffceb1", + "R93-MODULAR.json": "01ad2a656e69699b80b56d63cdf82448e424cd1c6e67636d53c079a6f03f55a5", + "R93-PRICE.json": "c108a061c6c03306a99a6fbafe919208954a7479ae28fb8a8fbf45d9832e6144", + "R93-RATIONAL.json": "2800af56efe23f7420a12f0713a659cd4fa4a3fb7c58449749ef697097ccccbf" +} diff --git a/research/p104-owned-zero-rebirth-bound/inputs/R139-PLAN.md b/research/p104-owned-zero-rebirth-bound/inputs/R139-PLAN.md new file mode 100644 index 0000000000..fde23ccaa7 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/inputs/R139-PLAN.md @@ -0,0 +1,14 @@ +# Round 139 · zero one owned MOVE under the entire original suffix + +Exact #7334 and signed #7113. Replace one paid owned MOVE with CLEAR in its old chart and INIT of zero in its destination. Leave every subsequent event, chart, and output contract fixed. All 47 exact old owner rows are nonzero by the R137 receipt. Thus the normalized difference is a nonzero old row times the unit suffix response on the moved owned coordinate. Test final public rows, all original COPY pre-write guards, and final-owned coordinates. + +Freeze complete signed R137 price before decode. One edit P_r−17, T unchanged, 110,502 paid, 22,461 productive and surplus 1424+17r. Whole optimistic bound grants all 47 rank-specific prices before ancillary cost. Cap 47 guarded columns, 76,466 events, and 25 seconds. An exact nonzero observable excludes the edit. Advance at most one zero response through legal CLEAR/INIT, lifetime, arbitrary-input physical phase and adjoint and complete paid, precision, tape and caller verification. No extra edit credit or new premise. + +CPython 3.12 with assertions, from this root: + +```sh +python3.12 -I -B lead/guarded_suffix.py --price-only > fresh-price.json +cmp lead/PRICE.json fresh-price.json +python3.12 -I -B lead/guarded_suffix.py > fresh-result.json +cmp lead/RESULT.json fresh-result.json +``` diff --git a/research/p104-owned-zero-rebirth-bound/inputs/R140-PLAN.md b/research/p104-owned-zero-rebirth-bound/inputs/R140-PLAN.md new file mode 100644 index 0000000000..0edd8f0cbb --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/inputs/R140-PLAN.md @@ -0,0 +1,16 @@ +# Round 140 · screen two simultaneous owned zeroings + +Exact #7334 aaeec8c0acf01e99a5f331ef363a698d9c084ace and signed #7113 07a76c5e2738882c0cb322278e56f6cae3c9885d. Select two distinct old paid owned MOVE clocks. At each replace the MOVE by CLEAR and fresh zero INIT, preserving every other original event and signed coefficient. At clock i denote the original owned row by P_i, and the later full guarded response to a unit defect by S_i. For i fresh-price.json +cmp lead/PRICE.json fresh-price.json +python3.12 -I -B lead/pair_screen.py > fresh-result.json +cmp lead/RESULT.json fresh-result.json +``` diff --git a/research/p104-owned-zero-rebirth-bound/inputs/R80-OWNED.json b/research/p104-owned-zero-rebirth-bound/inputs/R80-OWNED.json new file mode 100644 index 0000000000..93842d42c9 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/inputs/R80-OWNED.json @@ -0,0 +1,291 @@ +{ + "blocked_by": { + "ADD": 9 + }, + "case_cap": 4, + "consecutive_same_lifetime_pairs": [ + { + "blocker": [ + 33141, + [ + "ADD", + 1489, + 1502, + "4", + 534 + ] + ], + "directions": [ + "down", + "down" + ], + "frames": [ + 541, + 534, + 117 + ], + "key": [ + 1502, + 33136, + 33140, + 33142 + ], + "scales": [], + "turn": false + }, + { + "blocker": [ + 33143, + [ + "ADD", + 629, + 1502, + "2", + 117 + ] + ], + "directions": [ + "down", + "down" + ], + "frames": [ + 534, + 117, + 594 + ], + "key": [ + 1502, + 33136, + 33142, + 33149 + ], + "scales": [], + "turn": false + }, + { + "blocker": [ + 39806, + [ + "ADD", + 497, + 1503, + "-4", + 520 + ] + ], + "directions": [ + "down", + "down" + ], + "frames": [ + 529, + 520, + 595 + ], + "key": [ + 1503, + 39802, + 39805, + 39811 + ], + "scales": [], + "turn": false + }, + { + "blocker": [ + 39867, + [ + "ADD", + 1532, + 497, + "4", + 520 + ] + ], + "directions": [ + "up", + "up" + ], + "frames": [ + 595, + 520, + 529 + ], + "key": [ + 1532, + 38119, + 39866, + 39875 + ], + "scales": [], + "turn": false + }, + { + "blocker": [ + 40555, + [ + "ADD", + 1501, + 1525, + "1/4", + 115 + ] + ], + "directions": [ + "down", + "down" + ], + "frames": [ + 549, + 115, + 593 + ], + "key": [ + 1501, + 39975, + 40554, + 40558 + ], + "scales": [], + "turn": false + }, + { + "blocker": [ + 42469, + [ + "ADD", + 1562, + 1504, + "1", + 1031 + ] + ], + "directions": [ + "down", + "down" + ], + "frames": [ + 591, + 1031, + 597 + ], + "key": [ + 1504, + 39828, + 42468, + 42473 + ], + "scales": [], + "turn": false + }, + { + "blocker": [ + 42479, + [ + "ADD", + 1562, + 1533, + "1", + 1031 + ] + ], + "directions": [ + "up", + "up" + ], + "frames": [ + 597, + 1031, + 591 + ], + "key": [ + 1533, + 38130, + 42478, + 42491 + ], + "scales": [], + "turn": false + }, + { + "blocker": [ + 41997, + [ + "ADD", + 1531, + 1291, + "-2", + 117 + ] + ], + "directions": [ + "up", + "up" + ], + "frames": [ + 594, + 117, + 534 + ], + "key": [ + 1531, + 32607, + 41996, + 44242 + ], + "scales": [], + "turn": false + }, + { + "blocker": [ + 44243, + [ + "ADD", + 1531, + 995, + "-4", + 534 + ] + ], + "directions": [ + "up", + "up" + ], + "frames": [ + 117, + 534, + 541 + ], + "key": [ + 1531, + 32607, + 44242, + 44244 + ], + "scales": [], + "turn": false + } + ], + "controls": [ + "unary signed round trip", + "binary source read blocks pair" + ], + "eligible_turns": [], + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "paid_owned_rank": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "price_sha256": "76926ec9ff997159d281e0363326edb2e1aff8c530b041f361565030588e02cf", + "remaining": [], + "seconds_cap": 18, + "status": "EXHAUSTED", + "tested": [], + "total_events": 76466, + "visited_events": 76466, + "word_sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +} diff --git a/research/p104-owned-zero-rebirth-bound/inputs/R92-PRICE.json.gz b/research/p104-owned-zero-rebirth-bound/inputs/R92-PRICE.json.gz new file mode 100644 index 0000000000..0307eb95e2 Binary files /dev/null and b/research/p104-owned-zero-rebirth-bound/inputs/R92-PRICE.json.gz differ diff --git a/research/p104-owned-zero-rebirth-bound/inputs/aggregate.py b/research/p104-owned-zero-rebirth-bound/inputs/aggregate.py new file mode 100644 index 0000000000..c040962092 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/inputs/aggregate.py @@ -0,0 +1,164 @@ +"""Test the two fixed public endpoint banks for the literal role-532 aggregate.""" +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/R130-PRICE.json": "d9074aad58d3ffdad995ba68b2ffa541ae2b7df833b757d8e1a9767118140f39", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", +} +ROLE = 532 +BANKS = ((44611, 3, ROLE), (44612, 207, ROLE)) +SOURCES = ((41177, 363, Q(1), 744), (41179, 452, Q(-2), 746)) + + +def unique(pairs): + obj = dict(pairs) + if len(obj) != len(pairs): + raise ValueError("duplicate JSON key") + return obj + + +def read(path): + data = (ROOT / path).read_bytes() + if sha256(data).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency {path}") + return data + + +def invoice(): + old = loads(read("inputs/R130-PRICE.json"), object_pairs_hook=unique) + assert old["head"] == HEAD and old["caller"] == CALLER + assert old["word_sha256"] == PINS["inputs/7334-WORD.json.gz"] + by_role = {p["role"]: p for p in old["candidates"] if all(e[1] == p["role"] for _, e in p["contacts"])} + assert set(by_role) == {198, ROLE} + lead = by_role[ROLE] + assert lead["clocks"] == [41176, 41178, 44611] and lead["charts"] == [3, 744, 746, 207] + assert lead["contacts"] == [[t, ["ADD", ROLE, s, str(q), c]] for t, s, q, c in SOURCES] + assert lead["paid_delta"] == {"2": -17, "3": -34, "8": 17} + assert 0 < Q(lead["probe_lower"]) <= Q(lead["raw_upper"]) < 1 + return dict(head=HEAD, caller=CALLER, pins=PINS, candidate=lead, + compatible_cap=2, gross_upper=str(sum(Q(p["raw_upper"]) for p in by_role.values())), + paid=old["after_paid_one"], productive=old["productive"], surplus=old["surplus"], + selected_banks=[list(k) for k in BANKS], unresolved_role198=[42533,42599,44596]) + + +def exact_span(target, bank, deadline, helpers): + absent = set(target).difference(*(row.keys() for row in bank.values())) + if absent: + i = min(absent) + return dict(decision="outside donor span", separator={i: "1"}, separator_value=str(target[i]), + absent_coordinates=sorted(absent)) + # Row elimination, then transpose the reduction onto one nonzero residual coordinate. + axpy = helpers["axpy"] + basis = {} + for role, vector in sorted(bank.items()): + if monotonic() >= deadline: + return None + row, weights = vector.copy(), {role: Q(1)} + helpers["reduce_row"](row, basis, weights, -1) + if row: + i = min(row) + factor = row[i] + basis[i] = ({j: a / factor for j, a in row.items()}, {j: a / factor for j, a in weights.items()}) + row, weights = target.copy(), {} + helpers["reduce_row"](row, basis, weights, 1) + if not row: + check = {} + for role, q in weights.items(): + axpy(check, bank[role], q) + assert check == target + return dict(decision="exact span survivor", rank=len(basis), + coefficients={i: str(q) for i, q in weights.items()}) + i = min(row) + dual = {i: Q(1)} + for pivot, (vector, _) in sorted(basis.items(), reverse=True): + value = sum(q * dual.get(j, 0) for j, q in vector.items()) + if value: + dual[pivot] = dual.get(pivot, 0) - value + if not dual[pivot]: + del dual[pivot] + def dot(vector): + return sum(q * vector.get(j, 0) for j, q in dual.items()) + assert all(dot(v) == 0 for v in bank.values()) and dot(target) == row[i] + return dict(decision="outside donor span", rank=len(basis), + separator={j: str(q) for j, q in dual.items()}, separator_value=str(dot(target))) + + +def controls(helpers): + d = monotonic() + 1 + bank = {7: {0: Q(1), 1: Q(1)}, 8: {1: Q(2)}} + assert exact_span({0: Q(3)}, bank, d, helpers)["coefficients"] == {7: "3", 8: "-3/2"} + assert exact_span({0: Q(3), 2: Q(1)}, bank, d, helpers)["separator"] == {2: "1"} + covector = exact_span({0: Q(1)}, {7: bank[7]}, d, helpers) + assert covector["separator"] == {0: "-1", 1: "1"} and covector["separator_value"] == "-1" + return ["two donor exact aggregate", "exterior-coordinate perturbation", "same-support covector separation"] + + +def main(): + assert __debug__ + price = invoice() + if sys.argv[1:] == ["--price-only"]: + print(dumps(price, sort_keys=True, indent=2)) + return + assert not sys.argv[1:] + deadline = monotonic() + 18 + read("inputs/donor_span.py") + helpers = run_path(str(ROOT / "inputs/donor_span.py")) + control = controls(helpers) + raw = decompress(read("inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest() == PAYLOAD + word = loads(raw, object_pairs_hook=unique) + program = word["program"] + assert len(program) == 76466 + paid = price["candidate"] + a, b, c = paid["clocks"] + charts = paid["charts"] + assert [program[t] for t in (a, b, c)] == [ + ["MOVE", ROLE, x, y, False] for x, y in zip(charts[:-1], charts[1:], strict=True) + ] + selected = set() + for t in range(a + 1, c): + if t == b: + continue + e = program[t] + if ROLE in (e[1:3] if e[0] in {"ADD", "COPY"} else e[1:2]): + selected.add(t) + assert selected == {t for t, *_ in SOURCES} + assert all(program[t] == ["ADD", ROLE, s, str(q), chart] for t, s, q, chart in SOURCES) + req = {cut: {(chart, role)} for cut, chart, role in BANKS} + refs = {t: {s} for t, s, *_ in SOURCES} + banks, values = helpers["snapshot"](word, req, refs, deadline) + rows, aggregate = [], {} + if all((t, s) in values for t, s, *_ in SOURCES): + for t, s, q, _ in SOURCES: + helpers["axpy"](aggregate, values[t, s], q) + for key in BANKS: + if key not in banks or monotonic() >= deadline: + break + bank = {i: row for i, row in banks[key].items() if i < word["public"]} + result = exact_span(aggregate, bank, deadline, helpers) + if result is None: + break + rows.append(dict(key=list(key), bank_roles=sorted(bank), **result)) + unvisited = [list(k) for k in BANKS[len(rows):]] + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, price=price, + aggregate={i: str(a) for i, a in aggregate.items()}, + controls=control, rows=rows, unvisited=unvisited, + role198_status="outside this two-bank scope"), sort_keys=True, indent=2)) + if unvisited: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-zero-rebirth-bound/inputs/donor_span.py b/research/p104-owned-zero-rebirth-bound/inputs/donor_span.py new file mode 100644 index 0000000000..46e4621b69 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/inputs/donor_span.py @@ -0,0 +1,169 @@ +"""Match the literal ADD source using other live rows in the retimed chart.""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +import sys +from time import monotonic + +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE="c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d" + + +def checked(path,want,compressed=False): + raw=path.read_bytes() + if sha256(raw).hexdigest()!=want: + raise ValueError(f"changed dependency: {path.name}") + return json.loads(decompress(raw) if compressed else raw) + + +@cache +def scalar(x): + return Q(x) + + +def axpy(dst,src,c): + for k,a in src.items(): + value=dst.get(k,0)+c*a + if value: + dst[k]=value + else: + dst.pop(k,None) + + +def reduce_row(row,basis,weights,multiplier): + for k,(v,w) in sorted(basis.items()): + a=row.get(k,0) + if a: + axpy(row,v,-a) + axpy(weights,w,multiplier*a) + + +def solve(target,bank,deadline): + basis={} + for role,vector in sorted(bank.items()): + if monotonic()>=deadline: + return None + r=vector.copy() + w={role:Q(1)} + reduce_row(r,basis,w,-1) + if r: + k=min(r) + d=r[k] + basis[k]=({i:a/d for i,a in r.items()},{i:a/d for i,a in w.items()}) + residual=target.copy() + weights={} + reduce_row(residual,basis,weights,1) + rebuilt={} + for role,a in weights.items(): + axpy(rebuilt,bank[role],a) + axpy(rebuilt,residual,Q(1)) + assert rebuilt==target + return dict(rank=len(basis), residual={i:str(v) for i,v in residual.items()}, + matching_coefficients={i:str(v) for i,v in weights.items()} if not residual else None) + + +def snapshot(word,requested,targets,deadline): + public=word["public"] + active=word["initial"]+[None]*word["owned_fields"] + rows=[{i:Q(1)} for i in range(public)]+[None]*word["owned_fields"] + banks,values={},{} + stop=max(requested.keys()|targets.keys()) + for t,e in enumerate(word["program"]): + if t%64==0 and monotonic()>=deadline: + break + for chart,r in requested.get(t,()): + banks[t,chart,r]={i:rows[i].copy() for i in range(len(active)) if i!=r and active[i]==chart and rows[i]} + for s in targets.get(t,()): + assert active[s] is not None + values[t,s]=rows[s].copy() + if t==stop: + break + op,r,*args=e + if op=="MOVE": + assert active[r]==args[0] and args[2]==(r>=public) + active[r]=args[1] + elif op=="INIT": + assert active[r] is None and rows[r] is None and r>=public + active[r]=args[0] + rows[r]={} + elif op=="CLEAR": + assert active[r]==args[0] and rows[r] is not None and r>=public + active[r]=rows[r]=None + elif op=="SCALE": + assert active[r]==args[1] and scalar(args[0]) + rows[r]={i:v*scalar(args[0]) for i,v in rows[r].items()} + else: + s,k,chart=args + assert active[r]==active[s]==chart and r!=s and op in ("ADD","COPY") + if op=="COPY": + assert r>=public and not rows[r] + axpy(rows[r],rows[s],scalar(k)) + return banks,values + + +def controls(): + d=monotonic()+1 + a,b={0:Q(1),1:Q(1)},{1:Q(2)} + assert solve({0:Q(3)}, {7:a,8:b},d)["matching_coefficients"]=={7:"3",8:"-3/2"} + assert solve({2:Q(1)}, {7:a,8:b},d)["residual"]=={2:"1"} + assert solve({0:Q(3)}, {7:{0:Q(1),2:Q(1)},8:b},d)["residual"]=={2:"-3"} + assert solve({}, {7:a},d)["matching_coefficients"]=={} + return ["two-donor span","separating coordinate","changed donor row","zero source"] + + +def main(): + root=Path(sys.argv[1]) + price=checked(root/"price/PRICE.json",PRICE) + word=checked(root/"inputs/7334-WORD.json.gz",WORD,True) + assert price["head"]==HEAD and price["word_sha256"]==WORD + moves=word["program"] + req,targets=defaultdict(set),defaultdict(set) + bykey={} + for p in price["candidates"]: + r,s=p["owner"],p["peer"] + f,g=p["move_clocks"] + a,b,c=p["chart_path"] + t,add=p["literal_ADD"] + assert add[:2]==[r,s] and moves[t]==["ADD",*add] and f=deadline or (t,s) not in values or (cut,chart,r) not in banks: + pending.append(key) + continue + bank=banks[cut,chart,r] + source=values[t,s] + result=solve(source,bank,deadline) + if result is None: + pending.append(key) + continue + output.append(dict(key=key,source=[t,s],target_chart=chart,bank_roles=sorted(bank), + source_nnz=len(source),**result, + decision="exact span survivor" if result["matching_coefficients"] is not None else "outside donor span")) + print(json.dumps(dict(head=HEAD,price_sha256=PRICE,word_sha256=WORD,status="CAPPED" if pending else "EXHAUSTED", + case_cap=33,seconds_cap=18,controls=checks,counts=Counter(x["decision"] for x in output), + decisions=output,unvisited=pending,survivors=[x["key"] for x in output if x["matching_coefficients"] is not None]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-owned-zero-rebirth-bound/inputs/pricing.py b/research/p104-owned-zero-rebirth-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-owned-zero-rebirth-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-owned-zero-rebirth-bound/receipts/PAIR-WITNESSES.json b/research/p104-owned-zero-rebirth-bound/receipts/PAIR-WITNESSES.json new file mode 100644 index 0000000000..d65503fc78 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/receipts/PAIR-WITNESSES.json @@ -0,0 +1,162 @@ +{ + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "cases": 1081, + "counts": { + "different guarded suffix support": 8, + "independent prefix rows": 1073 + }, + "exact_suffix_witnesses": [ + { + "clocks": [ + 30537, + 30551 + ], + "coefficients": [ + "-1", + "0" + ], + "observable": [ + "public", + 38 + ], + "support_sizes": [ + 440, + 375 + ] + }, + { + "clocks": [ + 33133, + 39844 + ], + "coefficients": [ + "1/2", + "0" + ], + "observable": [ + "public", + 124 + ], + "support_sizes": [ + 413, + 404 + ] + }, + { + "clocks": [ + 33140, + 33142 + ], + "coefficients": [ + "4", + "0" + ], + "observable": [ + "public", + 19 + ], + "support_sizes": [ + 450, + 385 + ] + }, + { + "clocks": [ + 33140, + 33149 + ], + "coefficients": [ + "4", + "0" + ], + "observable": [ + "public", + 19 + ], + "support_sizes": [ + 450, + 377 + ] + }, + { + "clocks": [ + 33142, + 33149 + ], + "coefficients": [ + "-2", + "0" + ], + "observable": [ + "public", + 130 + ], + "support_sizes": [ + 385, + 377 + ] + }, + { + "clocks": [ + 34519, + 35434 + ], + "coefficients": [ + "1/2", + "0" + ], + "observable": [ + "public", + 113 + ], + "support_sizes": [ + 471, + 463 + ] + }, + { + "clocks": [ + 36319, + 36327 + ], + "coefficients": [ + "0", + "4" + ], + "observable": [ + "public", + 93 + ], + "support_sizes": [ + 446, + 439 + ] + }, + { + "clocks": [ + 39805, + 39811 + ], + "coefficients": [ + "2", + "0" + ], + "observable": [ + "public", + 145 + ], + "support_sizes": [ + 375, + 369 + ] + } + ], + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "pins": { + "R137-RESULT.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "R139-INDEPENDENT-RESULT.json": "ad45f533e423dbd1edffa84c3848ed1beaf2cd9b7e32feb5ce2f4a3deb84eddc", + "R140-LEAD-RESULT.json": "2d07bdb7d32b1a50eb23e8af75eed40585f181fe924641298c1089518e6763b2", + "R140-PRICE.json": "47a1e9f2a704bfe98f16cf4e36f1f592789595db211f6bb149dc77c026b6fb20" + }, + "unresolved": [] +} diff --git a/research/p104-owned-zero-rebirth-bound/receipts/SHA256.json b/research/p104-owned-zero-rebirth-bound/receipts/SHA256.json new file mode 100644 index 0000000000..b6055403f8 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/receipts/SHA256.json @@ -0,0 +1,11 @@ +{ + "R137-LEAD.json": "a109deda97d3b4f5ceb52814a50186035ea44ac1bdaf47281f564dcc2da239db", + "R137-PRICE.json": "1e8270d9a48728327f7eab9610a272fbb8ef09518dc4ddc5ceb573be00ae2beb", + "R139-AGREEMENT.json": "3abd6c0065ea97ef1b0e47cbb1d65ef021004b80f90c9faec38ffcaeb46a40fa", + "R139-INDEPENDENT.json": "ad45f533e423dbd1edffa84c3848ed1beaf2cd9b7e32feb5ce2f4a3deb84eddc", + "R139-LEAD.json": "c81636f5fe4a5db1cb31220b451e400f2eb86af6dc3480235b7cfd34d09a8f40", + "R139-PRICE.json": "b9d6d60d467af0269e5dd4d355607c8be5d35581da487f72a593ff775967fb57", + "R140-INDEPENDENT.json": "20534b54e165646dedb9e4f1e594f6bd8e1aeadd8a7f6fd9788ac7e1ffdf3d05", + "R140-LEAD.json": "2d07bdb7d32b1a50eb23e8af75eed40585f181fe924641298c1089518e6763b2", + "R140-PRICE.json": "47a1e9f2a704bfe98f16cf4e36f1f592789595db211f6bb149dc77c026b6fb20" +} diff --git a/research/p104-owned-zero-rebirth-bound/receipts/SUFFIX-AGREEMENT.json b/research/p104-owned-zero-rebirth-bound/receipts/SUFFIX-AGREEMENT.json new file mode 100644 index 0000000000..c98bc2aca8 --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/receipts/SUFFIX-AGREEMENT.json @@ -0,0 +1,293 @@ +{ + "agrees": true, + "checked": [ + [ + 30529, + 3, + "6305943/8192", + 489 + ], + [ + 30537, + 3, + "6307479/8192", + 440 + ], + [ + 30551, + 3, + "-28421/16", + 375 + ], + [ + 30581, + 3, + "-1/4", + 94 + ], + [ + 30593, + 3, + "1", + 94 + ], + [ + 32939, + 3, + "-82983/2048", + 408 + ], + [ + 33125, + 3, + "-1411731/2048", + 434 + ], + [ + 33133, + 3, + "-82983/2048", + 413 + ], + [ + 33140, + 3, + "-925149/1024", + 450 + ], + [ + 33142, + 3, + "-114163/128", + 385 + ], + [ + 33149, + 3, + "-114163/128", + 377 + ], + [ + 34515, + 3, + "235571/1024", + 418 + ], + [ + 34519, + 3, + "-19919/2048", + 471 + ], + [ + 35143, + 17, + "-1", + 54 + ], + [ + 35434, + 3, + "-316087/512", + 463 + ], + [ + 35439, + 3, + "-163687/512", + 362 + ], + [ + 35443, + 3, + "-163687/128", + 362 + ], + [ + 36315, + 3, + "764863/8192", + 493 + ], + [ + 36319, + 3, + "764863/8192", + 446 + ], + [ + 36327, + 3, + "764863/2048", + 439 + ], + [ + 36337, + 19, + "-1", + 63 + ], + [ + 36349, + 19, + "-4", + 63 + ], + [ + 39544, + 3, + "-163687/128", + 353 + ], + [ + 39572, + 19, + "-4", + 54 + ], + [ + 39718, + 3, + "2385/128", + 349 + ], + [ + 39776, + 3, + "239715/128", + 380 + ], + [ + 39805, + 3, + "30585/128", + 375 + ], + [ + 39811, + 3, + "30585/128", + 369 + ], + [ + 39844, + 3, + "213833/512", + 404 + ], + [ + 39866, + 17, + "-1", + 60 + ], + [ + 39875, + 17, + "-1", + 60 + ], + [ + 40529, + 3, + "1/2", + 45 + ], + [ + 40547, + 3, + "74831/128", + 372 + ], + [ + 40554, + 3, + "74831/64", + 371 + ], + [ + 40558, + 3, + "74831/64", + 371 + ], + [ + 41482, + 3, + "1", + 80 + ], + [ + 41637, + 3, + "163431/1024", + 361 + ], + [ + 41996, + 3, + "1/8", + 91 + ], + [ + 42468, + 3, + "-465465/256", + 412 + ], + [ + 42473, + 3, + "-465465/256", + 409 + ], + [ + 42478, + 3, + "-1/8", + 85 + ], + [ + 42491, + 3, + "-1/8", + 85 + ], + [ + 44235, + 52, + "-2", + 53 + ], + [ + 44242, + 3, + "1/8", + 91 + ], + [ + 44244, + 3, + "1/8", + 91 + ], + [ + 45629, + 17, + "-4", + 53 + ], + [ + 45647, + 17, + "-4", + 53 + ] + ], + "copy_guard_checks": 11, + "copy_guard_nonzero": 0, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "independent_sha256": "ad45f533e423dbd1edffa84c3848ed1beaf2cd9b7e32feb5ce2f4a3deb84eddc", + "lead_sha256": "c81636f5fe4a5db1cb31220b451e400f2eb86af6dc3480235b7cfd34d09a8f40", + "unresolved": 0 +} diff --git a/research/p104-owned-zero-rebirth-bound/replay.py b/research/p104-owned-zero-rebirth-bound/replay.py new file mode 100644 index 0000000000..52c125453e --- /dev/null +++ b/research/p104-owned-zero-rebirth-bound/replay.py @@ -0,0 +1,162 @@ +"""Replay the exact single-site and paired P104 owned zero-rebirth exclusions.""" +from argparse import ArgumentParser +from gzip import decompress +from hashlib import sha1,sha256 +from json import dumps,loads +from pathlib import Path +from subprocess import run +from tempfile import TemporaryDirectory +import sys + +ROOT=Path(__file__).resolve().parent + + +def unique(items): + out=dict(items) + if len(out)!=len(items): + raise ValueError('duplicate JSON key') + return out + + +def decode(raw): + return loads(raw,object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def source(name): + path=Path(name) + if path.is_absolute() or '..' in path.parts or path.as_posix()!=name: + raise ValueError('invalid package-relative path '+name) + return (ROOT/path).read_bytes() + + +def load_inputs(): + pins=decode(source('LOCAL-PINS.json')) + for name,expected in pins.items(): + if digest(source(name))!=expected: + raise ValueError('changed package dependency '+name) + p=decode(source('PROVENANCE.json')) + for name,entry in p['files'].items(): + raw=source(name) + assert digest(raw)==entry['sha256']==pins[name] + assert sha1(f'blob {len(raw)}\0'.encode()+raw).hexdigest()==entry['git_blob'] + old=decompress(source('inputs/R92-PRICE.json.gz')) + assert digest(old)==decode(source('inputs/PR7362-SHA256.json'))['R92-PRICE.json'] + a=decode(source('inputs/ADMITTED.json')) + assert a['head']=='aaeec8c0acf01e99a5f331ef363a698d9c084ace' + assert a['kappa']=='0.00364665195644' + return old + + +def call(script,*args,expect_success=True): + p=run([sys.executable,'-I','-B',str(script),*args],capture_output=True,timeout=40) + if expect_success and p.returncode: + sys.stderr.write(p.stderr.decode(errors='replace')) + p.check_returncode() + return p + + +def write(path,raw): + path.parent.mkdir(parents=True,exist_ok=True) + path.write_bytes(raw) + + +def replay(root,out): + old_price = load_inputs() + expected = decode(source("receipts/SHA256.json")) + outputs = {} + + def engine(directory, program, script=None): + target = directory / (script or program) + write(target,source("engines/"+program)) + return target + + def record(name,script,*args): + proc = call(script,*args) + raw = proc.stdout + assert digest(raw) == expected[name], ("changed deterministic receipt",name) + outputs[name] = raw + return decode(raw) + + prefix, lead, independent, pairs, pair_check = ( + root/key for key in ("prefix","lead","independent","pairs","pair-check")) + for d in (prefix,lead,independent): + write(d/"inputs/7334-WORD.json.gz",source("inputs/7334-WORD.json.gz")) + for name in ("R80-OWNED.json","aggregate.py","donor_span.py","pricing.py"): + write(prefix/"inputs"/name,source("inputs/"+name)) + write(prefix/"inputs/R92-PRICE.json",old_price) + prefix_engine = engine(prefix,"first_use.py","lead/first_use.py") + record("R137-PRICE.json",prefix_engine,"--price-only") + p = record("R137-LEAD.json",prefix_engine) + assert p["counts"] == {"outside donor span":47} and not p["unvisited"] + assert all(r["row"] for r in p["records"]) + + for d, names in ((lead,("PRICE.json","RESULT.json")), + (independent,("R137-PRICE.json","R137-RESULT.json")), + (pairs,("R137-PRICE.json","R137-RESULT.json"))): + for name, label in zip(names,("R137-PRICE.json","R137-LEAD.json"),strict=True): + write(d/"inputs"/name,outputs[label]) + lead_engine = engine(lead,"lead_suffix.py","lead/guarded_suffix.py") + record("R139-PRICE.json",lead_engine,"--price-only") + single = record("R139-LEAD.json",lead_engine) + assert not single["survivors"] and not single["unresolved"] + write(independent/"inputs/R139-PRICE.json",outputs["R139-PRICE.json"]) + write(independent/"inputs/R139-LEAD-RESULT.json",outputs["R139-LEAD.json"]) + independent_engine = engine(independent,"guarded_suffix.py") + independent_args = ("--price-sha",expected["R139-PRICE.json"]) + record("R139-INDEPENDENT.json",independent_engine,*independent_args) + write(independent/"RESULT.json",outputs["R139-INDEPENDENT.json"]) + agreement = record("R139-AGREEMENT.json",engine(independent,"compare_suffix.py","compare.py")) + assert agreement["copy_guard_checks"] == 11 and agreement["copy_guard_nonzero"] == 0 + assert outputs["R139-AGREEMENT.json"] == source("receipts/SUFFIX-AGREEMENT.json") + + write(pairs/"inputs/R139-RESULT.json",outputs["R139-LEAD.json"]) + write(pairs/"inputs/R92-PRICE.json",old_price) + write(pairs/"inputs/pricing.py",source("inputs/pricing.py")) + pair_engine = engine(pairs,"pair_screen.py","lead/pair_screen.py") + record("R140-PRICE.json",pair_engine,"--price-only") + paired = record("R140-LEAD.json",pair_engine) + assert not paired["unresolved"] + for name,label in ( + ("R137-RESULT.json","R137-LEAD.json"), + ("R139-INDEPENDENT-RESULT.json","R139-INDEPENDENT.json"), + ("R140-PRICE.json","R140-PRICE.json"), + ("R140-LEAD-RESULT.json","R140-LEAD.json")): + write(pair_check/"inputs"/name,outputs[label]) + audit_engine = engine(pair_check,"pair_audit.py") + audit = record("R140-INDEPENDENT.json",audit_engine) + assert outputs["R140-INDEPENDENT.json"] == source("receipts/PAIR-WITNESSES.json") + assert audit["counts"] == paired["counts"] == { + "different guarded suffix support":8, "independent prefix rows":1073} + assert len(audit["exact_suffix_witnesses"]) == 8 and not audit["unresolved"] + assert set(outputs) == set(expected) + + (independent/"inputs/7334-WORD.json.gz").unlink() + for path,script,args in ( + (independent/"inputs/R139-PRICE.json",independent_engine,independent_args), + (pair_check/"inputs/R139-INDEPENDENT-RESULT.json",audit_engine,())): + path.write_bytes(path.read_bytes()+b" ") + proc = call(script,*args,expect_success=False) + assert proc.returncode == 1 and b"changed dependency" in proc.stderr + + if out is not None: + out.mkdir(parents=True) + for name,raw in outputs.items(): + write(out/name,raw) + print("PASS_P104_OWNED_ZERO_REBIRTH_BOUND single=47 paired=1081 guards=11 unresolved=0") + + +def main(): + assert __debug__ and sys.version_info[:2] == (3,12) + cli = ArgumentParser(description=__doc__) + cli.add_argument("--out",type=Path) + args = cli.parse_args() + with TemporaryDirectory() as tmp: + replay(Path(tmp),args.out) + + +if __name__ == "__main__": + main()