diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9") diff --git a/research/p104-public-move-fusion-contact-bound/LOCAL-PINS.json b/research/p104-public-move-fusion-contact-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..eb1e22b010 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/LOCAL-PINS.json @@ -0,0 +1,16 @@ +{ + "dependencies/7298/RESULT.json": "aaf594b981f37e7dbddb12fd052d9286cf5c8c95c8d5265ab6426408f6e58cc5", + "dependencies/7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "dependencies/7298/verify.py": "4a4291c9019ef23c664ae9646b076dc57054b49f5c5ffd21908aa9f0edf19902", + "dependencies/r47/lead/screen.py": "04c6f986b45945dcb4df22bcbfc74780e5840ff9c97b6c4dad064fc2c5576f75", + "dependencies/round30/complex/source/inputs/CALLER.json.gz": "58beaf24e01c0589ecd5d1676d6d27e75b779f089d0674eda11725465ffc04e1", + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": "9851ebaa4b4404be1f5670b8a8dfc6ee96a8e19e85731edd4a71d52bbfa9c793", + "dependencies/round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "dependencies/round41/independent/replay_core.py": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "engines/common_lift.py": "9a5afb37eff2f960aa1190594500dc98f393615c3d1400b45ed6a883001665b9", + "engines/common_lift_audit.py": "7bef3292c3389fd35c380bd21b683dcc75414c0ac1f42288cff6be3f373d01ac", + "engines/silence.py": "c026ccad84094bc5a204aaad462c04dc0b63d92ed4a857fa5445a03b2cc0dbe1", + "engines/silence_audit.py": "9b331ebc2472b057d153d1849e9b2d1d71552b0290ce89100b4c4d55506ee188", + "receipts/SHA256.json": "8254394c3c0bae0a0334502fdce12b330a568968b0b01987dcc581575a0f69a4", + "receipts/SUMMARY.json": "20cf3b5e5d7e0b0974659c504e9df00aaf3347e4cf54657526ec8b4b3ae628e9" +} diff --git a/research/p104-public-move-fusion-contact-bound/NOTICE b/research/p104-public-move-fusion-contact-bound/NOTICE new file mode 100644 index 0000000000..2befe4cadf --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/NOTICE @@ -0,0 +1,5 @@ +Apache-2.0. +#7277 supplies the native word and comparable price. #7113 supplies the +signed caller. #7298, #7311 and #7308 supply the retained tariff and +replay methods. #7259, #7171, #6765 and #6529 supply related scoped +precedents. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-public-move-fusion-contact-bound/PROVENANCE.json b/research/p104-public-move-fusion-contact-bound/PROVENANCE.json new file mode 100644 index 0000000000..77c3cee3e1 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/PROVENANCE.json @@ -0,0 +1,69 @@ +{ + "files": { + "dependencies/7298/RESULT.json": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "c66ad2ed50e6f70c2c60cbb5b8b222dcd1b64a6f", + "path": "research/adjacent-owned-add-exchange-bound/RESULT.json", + "sha256": "aaf594b981f37e7dbddb12fd052d9286cf5c8c95c8d5265ab6426408f6e58cc5", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/RESULT.json", + "uncompress": false + }, + "dependencies/7298/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 + }, + "dependencies/7298/verify.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "a45510da2548ec701c7719e6205f079318bbd930", + "path": "research/adjacent-owned-add-exchange-bound/verify.py", + "sha256": "4a4291c9019ef23c664ae9646b076dc57054b49f5c5ffd21908aa9f0edf19902", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/verify.py", + "uncompress": false + }, + "dependencies/r47/lead/screen.py": { + "commit": "3c4f2decb66af92d234979dd3a843d4224890c58", + "git_blob": "2b4c6b13ebeb745b00958a1dd96c20a671a1ecc9", + "path": "research/p104-adjacent-add-scale-exchange/engines/primary.py", + "sha256": "04c6f986b45945dcb4df22bcbfc74780e5840ff9c97b6c4dad064fc2c5576f75", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/3c4f2decb66af92d234979dd3a843d4224890c58/research/p104-adjacent-add-scale-exchange/engines/primary.py", + "uncompress": false + }, + "dependencies/round30/complex/source/inputs/CALLER.json.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "9451ceaf6e8e037894680b549f3ef41c21b260d7", + "path": "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "uncompress": true + }, + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "ef86c8ec8ed0a2042017a6f42515e70dd15cfffd", + "path": "research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "sha256": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "uncompress": true + }, + "dependencies/round30/complex/source/inputs/WORD.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "077bf48c35db0ddafae81f1bfa0ffacc30894b2b", + "path": "research/p104-terminal-cut-rechart/WORD.json.gz", + "sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz", + "uncompress": false + }, + "dependencies/round41/independent/replay_core.py": { + "commit": "2c777389ec0476e97ab141c645af01ff28a46aa6", + "git_blob": "0a450da01e68662b134bf45b7943a382ea62b656", + "path": "research/p104-owned-move-destination-span/dependencies/round41/independent/replay_core.py", + "sha256": "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/2c777389ec0476e97ab141c645af01ff28a46aa6/research/p104-owned-move-destination-span/dependencies/round41/independent/replay_core.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-public-move-fusion-contact-bound/README.md b/research/p104-public-move-fusion-contact-bound/README.md new file mode 100644 index 0000000000..20cb2c48df --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/README.md @@ -0,0 +1,128 @@ +# Public MOVE fusion contact bound on the retained P104 word + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** On the exact +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) word, +consider fusing consecutive ascending paid MOVEs of the same public +role. Two fixed-word contact rules both leave zero surviving stock. + +- **Delete individually silent scalar contacts.** All 4,732 consecutive + public MOVE windows contain a nonsilent intervening contact. The exact + row replay covers 7,721 distinct scalar contacts and 11,548 window + incidences. Every case has a nonzero change witness. First witnesses + are 4,553 ADDs and 179 SCALEs. +- **Retime one unchanged ADD after an existing common lift.** All 1,922 + windows with exactly one intervening ADD fail because the other + operand's first later contact is different from the required direct + lift. The two lift orders are allowed in this scope. The complete + first-blocker counts are in [SUMMARY.json](receipts/SUMMARY.json). + +Zero cases remain unresolved in each declared scope. The compatible +saving upper bound after support is zero. The comparable conditional +witness remains #7277 at κ = 0.003645669928698. + +## Price and fixed-word predicates + +The old public itinerary A→B→C must be strictly nested and retains +its original public endpoints and productive targets. The direct A→C +MOVE runs at the second old MOVE clock. For old ranks x and y, the +direct replacement pays rank x+y. The signed price before new work +credits the exact complete 17-copy change +`17(Hₓ + Hᵧ − Hₓ₊ᵧ)` on the #7113 caller, where Hᵣ is the retained +recursive tariff at the pinned old crossing upper. Both price +receipts are written before support tests. The per-role maximum +matching counts each original MOVE at most once. Its directed upper +ignores cross-role interference and grants added ordinary and physical work free. + +The complete pre-support upper is approximately 363.3275462698572 +raw units for the scalar-silence stock and 199.18473699786647 for +the one-ADD stock. The latter is a subset of the former inventory +under a different contact rule. The two optimistic bounds are separate. + +In the first scope, deleting an ADD requires an identically zero source +row and preservation of the fresh-zero token. Deleting a SCALE requires +a zero field row for a nonunit scale. COPY and lifetime changes are +barriers. An independent denominator-safe mod-65521 interpreter +certifies nonzero changes by exhibiting a nonzero coefficient of +the exact rational row change. This provides an obstruction even +before physical phase, ownership, restoration or precision checks. + +In the second scope, the ADD keeps its operands and coefficient. It +moves from B to C after both original operands reach C. At the original +ADD clock the other operand's next contact must be its existing +B→C MOVE, which stays paid exactly once. After either individual lift +and before the common ADD, a contact of either operand would block +the edit. The independent reverse scan includes source reads as well +as destination contacts and reproduces the first blocker for every +case. + +| First blocker in the one-ADD scope | Cases | +| --- | ---: | +| MOVE to a different destination | 809 | +| ADD source read | 472 | +| ADD destination contact | 459 | +| No later contact | 149 | +| SCALE | 27 | +| CLEAR | 6 | + +Controls cover signed cancellation, an altered sign, COPY and fresh +token barriers, a shared old MOVE in the matching, both lift orders, +an intervening source read and a wrong destination. The fixed-word +result leaves changed peer itineraries, compensated scalar edits, +alternate transports and coupled edits open. + +## Replay + +From a clean checkout with CPython 3.12 and assertions enabled: + +~~~sh +python3.12 -B scripts/research_package.py --package research/p104-public-move-fusion-contact-bound +python3.12 -B scripts/check_research_commit.py --package research/p104-public-move-fusion-contact-bound --check-modes --check-source-history +~~~ + +From a Git-free export, this command also emits all six full receipts +into a fresh output directory: + +~~~sh +python3.12 -I -B research/p104-public-move-fusion-contact-bound/replay.py --out fresh-receipts +~~~ + +[PROVENANCE.json](PROVENANCE.json) pins all eight public inputs by +commit, path, Git blob and SHA-256. [LOCAL-PINS.json](LOCAL-PINS.json) +pins the bundled files by relative path. The wrapper regenerates +the complete deterministic plaintext receipts and verifies their +full SHA-256 values against [SHA256.json](receipts/SHA256.json). +This preserves every proof-relevant field without storing another +copy of the large JSON arrays. The independent engines also check +the literal keys and mathematical evidence. All inputs are bundled, +and the replay needs only the standard library. + +## Credit + +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) at +`ed090b57ed88f8859e5ff4643645099e6ba856ea` supplies the native word +and comparable price. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +supplies the exact signed 17-copy caller. +[#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +supplies the retained tariff and known-good paid-stock replay. +[#7311](https://github.com/CrocSwap/integer-mult-bounds/pull/7311) +supplies the word and contact-authentication engine and identifies +silent-contact fusion as its next test. +[#7308](https://github.com/CrocSwap/integer-mult-bounds/pull/7308) +supplies the signed normalized row interpreter. +[#7259](https://github.com/CrocSwap/integer-mult-bounds/pull/7259) +covers fixed-output verification on older words. +[#7171](https://github.com/CrocSwap/integer-mult-bounds/pull/7171), +[#6765](https://github.com/CrocSwap/integer-mult-bounds/pull/6765), +and [#6529](https://github.com/CrocSwap/integer-mult-bounds/pull/6529) +supply related timed-support, resident-carrier and compensated-fusion +precedents. OpenAI Codex and subagents materially assisted. + +## Open next questions + +Can a compensated public MOVE fusion change one peer's lift and +preserve the signed action at a favorable complete price? Start by +pinning one changed peer itinerary and bounding compatible savings +over the full word with all additional transports and contacts +charged. Any surviving proposal still needs arbitrary-input signed +forward and adjoint action, ownership, restoration, precision and +complete tape verification. diff --git a/research/p104-public-move-fusion-contact-bound/SOURCES.json b/research/p104-public-move-fusion-contact-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/SOURCES.json @@ -0,0 +1,18 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/p104-public-move-fusion-contact-bound/TASK.json b/research/p104-public-move-fusion-contact-bound/TASK.json new file mode 100644 index 0000000000..f10ccb6b74 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "One direct fusion of consecutive ascending public MOVEs on a fixed #7277 role, testing either locally silent intervening scalar contacts or a single unchanged ADD retimed after the operands' existing common lift.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Public MOVE contact research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Exhaust the fixed-word paid MOVE saving before changing a carrier or building a provider.", + "budget_minutes": 3, + "evidence": "Complete exact signed price, disjoint MOVE matching, exact normalized row checks, modular nonzero witnesses, exact primary common-lift records, and independent reverse next-contact census.", + "open_questions": [ + { + "blocked_by": "A survivor still needs arbitrary-input signed action, ownership and restoration, and fully charged precision and tape.", + "first_step": "Pin one changed peer itinerary and bound compatible savings over the full word, charging every added transport and contact.", + "question": "Can a compensated paid public MOVE fusion change a peer's lift without losing signed action?", + "why_it_matters": "The original peer chronology leaves every one-ADD common-lift case blocked." + } + ], + "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": "This tests literal public-role fusion after a changed contact rule, beyond adjacent scalar exchange and previous-word fixed-contact searches.", + "scope_status": "changed", + "stop_rule": "Price both exact stocks first. Stop at the declared census or the per-engine caps, retaining unresolved cases. Close either route if every scoped contact test fails.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-public-move-fusion-contact-bound/VERIFY.json b/research/p104-public-move-fusion-contact-bound/VERIFY.json new file mode 100644 index 0000000000..59bd24b74e --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Rebuild both full paid receipts, all 4,732 literal scalar-contact exclusions and all 1,922 common-lift exclusions, with separate exact controls.", + "timeout_seconds": 150 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-public-move-fusion-contact-bound/dependencies/7298/RESULT.json b/research/p104-public-move-fusion-contact-bound/dependencies/7298/RESULT.json new file mode 100644 index 0000000000..c66ad2ed50 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/dependencies/7298/RESULT.json @@ -0,0 +1,97 @@ +{ + "bit": { + "add_pairs": 30551, + "checked_edges": 62474, + "copies": 36, + "eligible": 0, + "normalized_neighbors": 31265, + "saving_upper": "0", + "shared_owned": 246, + "target": "10018846261809/2500000000000000", + "target_margin_upper": "-150259748047868384659982093203238820648182213480307/2500000000000000000000000000000000000000000000000", + "unresolved": 0 + }, + "complex": { + "cases": [ + { + "complete_upper": "-270628787660064862669178534471473339574581160716573/2000000000000000000000000000000000000000000000000", + "events": [ + [ + 34511, + 34513 + ], + [ + 36306, + 36308 + ], + [ + 41987, + 41989 + ] + ], + "new_ranks": [ + 4, + 4 + ], + "old_ranks": [ + 0, + 0 + ] + }, + { + "complete_upper": "-5299092335389733735192584095979599221603492103289/156250000000000000000000000000000000000000000000", + "events": [ + [ + 33139, + 33141 + ], + [ + 44255, + 44257 + ] + ], + "new_ranks": [ + 1, + 2 + ], + "old_ranks": [ + 0, + 1 + ] + }, + { + "complete_upper": "-844193076311159197372651950923578810446691810127887/5000000000000000000000000000000000000000000000000", + "events": [ + [ + 39852, + 39854 + ] + ], + "new_ranks": [ + 5, + 6 + ], + "old_ranks": [ + 0, + 1 + ] + } + ], + "copies": 17, + "counts": { + "all": 65118, + "different_charts": 4625, + "excluded": 14, + "shared_owned": 20 + }, + "probe": "91141748217473298207420876011401/25000000000000000000000000000000000", + "unresolved": 0 + }, + "controls": { + "cross_operands_rejected": true, + "nonnested_rank_not_dimension_gap": true, + "same_source_and_destination_commute": true, + "self_add_rejected": true + }, + "status": "PASS_ADJACENT_OWNED_ADD_EXCHANGE_BOUND" +} diff --git a/research/p104-public-move-fusion-contact-bound/dependencies/7298/pricing.py b/research/p104-public-move-fusion-contact-bound/dependencies/7298/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/dependencies/7298/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/p104-public-move-fusion-contact-bound/dependencies/7298/verify.py b/research/p104-public-move-fusion-contact-bound/dependencies/7298/verify.py new file mode 100644 index 0000000000..a45510da25 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/dependencies/7298/verify.py @@ -0,0 +1,253 @@ +"""Replay the exact adjacent shared-owned ADD census on both native words.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from hashlib import sha1, sha256 +from itertools import pairwise +from pathlib import Path +import gzip +import json +import runpy + +HERE=Path(__file__).resolve().parent +BIT='research/paired-query-only-bit/' +PRICING=runpy.run_path(str(HERE/'pricing.py')) + + +def read(path,pin): + raw=path.read_bytes() + if raw.startswith(b'\x1f\x8b') and pin.get('uncompress',False): + raw=gzip.decompress(raw) + blob=sha1(f'blob {len(raw)}\0'.encode()+raw).hexdigest() + if sha256(raw).hexdigest()!=pin['sha256'] or blob!=pin['git_blob']: + raise ValueError('Changed input: '+path.name) + return raw + + +def rank(rows): + pivots={} + for x in rows: + while x and x.bit_length() in pivots: + x^=pivots[x.bit_length()] + if x: + pivots[x.bit_length()]=x + return len(pivots) + + +def commutes(a,b,c,d): + return a!=b and c!=d and a!=d and c!=b + + +def complex_scan(word,caller,early): + frames=word['frames'] + n=word['public'] + dims=list(map(len,frames)) + program=word['program'] + assert all(rank(f)==r for f,r in zip(frames,dims,strict=True)) + + @cache + def distance(a,b): + return 2*rank(frames[a]+frames[b])-dims[a]-dims[b] + + chains={} + at={} + scalar=[] + native=Counter() + for t,(tag,d,*args) in enumerate(program): + if tag=='MOVE': + a,b,owned=args + r=distance(a,b) + assert owned==(d>=n) and r==abs(dims[a]-dims[b])>0 + native[r]+=1 + continue + scalar.append(t) + if tag=='INIT': + assert d not in chains + chains[d]=[] + for role in {d,args[0]} if tag in ('ADD','COPY') else {d}: + if role>=n: + seq=chains[role] + at[t,role]=seq,len(seq) + seq.append(t) + if tag=='CLEAR': + del chains[d] + assert not chains and sum(native.values())==6280 + stages=[e[1] for e in caller['events'] if e[0]=='J'] + assert stages==list(range(1,18)) + copies=len(stages) + paid=Counter({r:copies*v for r,v in native.items()}) + main=set(word['live'])|{x+112 for x in word['live']}|set(word['hosted']['X2']+word['hosted']['Y2']) + helper=Counter(dims[b]-dims[a] for r,(a,b) in enumerate(zip(word['initial'],word['final'],strict=True)) if r not in main) + targets=Counter({r:copies*v for r,v in helper.items()}) + for info in caller['types'].values(): + for sign,offset,*bits in info['diagonal']: + assert (sign,offset,len(bits))==(-1,0,copies) + targets[1+8*sum(bits)]+=len(info['ports']) + for e in caller['events']: + if e[0]=='J': + continue + kind,tag,_,*args=e + if tag=='QUERY': + paid[1]+=len(caller['types'][kind]['ports']) + if tag in ('IDLE_ONE','IDLE_ODD'): + paid[8*len(args[0])+int(tag=='IDLE_ODD')]+=len(caller['types'][kind]['ports']) + assert dict(paid)=={int(r):v for r,v in early['invoice']['P'].items()} + assert dict(targets)=={int(r):v for r,v in early['invoice']['T'].items()} + assert sum(paid.values())==110536 and sum(targets.values())==22461 + net=targets.copy() + net.subtract(paid) + assert sum(r*v for r,v in net.items())==1424 + k=Q(early['price']['independent_raw_bracket'][1]) + base=PRICING['cost'](net,k) + assert base[1]<0 + counts=Counter() + rows=defaultdict(list) + for t,u in pairwise(scalar): + p,q=program[t],program[u] + if p[0]!=q[0] or p[0]!='ADD': + continue + counts['all']+=1 + a,b,f=p[1],p[2],p[-1] + c,d,g=q[1],q[2],q[-1] + if f==g: + continue + counts['different_charts']+=1 + shared={a,b}&{c,d} + if not any(role>=n for role in shared): + continue + counts['shared_owned']+=1 + if min(shared)0 and j+1=n for r in set(a[1:3])&set(b[1:3]))] + eligible=[(a,b) for a,b in owned if a[-1]!=b[-1]] + assert len(scalar)-1==31265 and len(all_pairs)==30551 and len(owned)==246 and not eligible + margin=PRICING['cost'](signed,Q(PRICING['TARGET']))[1] + assert margin<0 + return {'normalized_neighbors':len(scalar)-1,'add_pairs':len(all_pairs),'shared_owned':len(owned), + 'checked_edges':edges,'eligible':len(eligible),'unresolved':0,'copies':copies, + 'target':PRICING['TARGET'],'target_margin_upper':str(margin),'saving_upper':'0'} + + +def controls(): + assert commutes(0,2,1,2) and commutes(0,1,0,2) + assert not commutes(0,1,1,2) and not commutes(0,1,1,0) + assert not commutes(0,0,1,2) + assert 2*rank([1,2,1,4])-4==2 + return {'same_source_and_destination_commute':True,'cross_operands_rejected':True, + 'self_add_rejected':True,'nonnested_rank_not_dimension_gap':True} + + +def unique_keys(entries): + out={} + for k,v in entries: + if k in out: + raise ValueError('Duplicate manifest key: '+k) + out[k]=v + return out + + +def run(root): + p=json.loads((HERE/'PROVENANCE.json').read_bytes(),object_pairs_hook=unique_keys) + c={} + for k,pin in p['bundled'].items(): + raw=read(HERE/k,pin) + c[k]=json.loads(gzip.decompress(raw) if raw.startswith(b'\x1f\x8b') else raw) + rows=json.loads((HERE/'SOURCES.json').read_bytes(),object_pairs_hook=unique_keys)['files'] + pins=unique_keys((row['path'],row) for row in rows) + bitword=BIT+'retained/inputs/BIT-NATIVE-WORD.json.gz' + invoice=BIT+'EFREE-RESULT.json' + return {'status':'PASS_ADJACENT_OWNED_ADD_EXCHANGE_BOUND','controls':controls(), + 'complex':complex_scan(c['inputs/WORD.json.gz'],c['inputs/CALLER.json.gz'],c['inputs/EARLY-RESULT.json.gz']), + 'bit':bit_scan(json.loads(gzip.decompress(read(root/bitword,pins[bitword]))), + json.loads(read(root/invoice,pins[invoice])))} + + +if __name__=='__main__': + assert __debug__ + parser=ArgumentParser(description=__doc__) + parser.add_argument('--root',type=Path,default=Path.cwd()) + args=parser.parse_args() + result=json.dumps(run(args.root),sort_keys=True,indent=2)+'\n' + frozen=HERE/'RESULT.json' + if frozen.is_file(): + assert result==frozen.read_text() + print(result,end='') diff --git a/research/p104-public-move-fusion-contact-bound/dependencies/r47/lead/screen.py b/research/p104-public-move-fusion-contact-bound/dependencies/r47/lead/screen.py new file mode 100644 index 0000000000..2b4c6b13eb --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/dependencies/r47/lead/screen.py @@ -0,0 +1,296 @@ +"""Preprice one signed adjacent ADD/SCALE exchange on the pinned #7277 word.""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import runpy +from time import monotonic + +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +PINS = { + "round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "round30/complex/source/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "round30/complex/source/inputs/EARLY-RESULT.json": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "7298/verify.py": "4a4291c9019ef23c664ae9646b076dc57054b49f5c5ffd21908aa9f0edf19902", + "7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "7298/RESULT.json": "aaf594b981f37e7dbddb12fd052d9286cf5c8c95c8d5265ab6426408f6e58cc5", +} + + +def unique(items): + result = dict(items) + assert len(result) == len(items), "Duplicate JSON key" + return result + + +def authenticate(roots): + files = {} + for key, digest in PINS.items(): + label, relative = key.split("/", 1) + path = roots[label] / relative + data = path.read_bytes() + if sha256(data).hexdigest() != digest: + raise ValueError(f"Changed input {key}") + if relative.endswith(".gz"): + data = gzip.decompress(data) + if relative.endswith((".json", ".json.gz")): + files[key] = json.loads(data, object_pairs_hook=unique) + return files + + +def write(root, filename, payload): + target = root / filename + temp = target.with_suffix(".tmp") + temp.write_text(json.dumps(payload, indent=2, sort_keys=True) + "\n") + temp.replace(target) + + +def interval(bounds): + return [str(x) for x in bounds] + + +def exchange(first, second): + add, scale = (first, second) if first[0] == "ADD" else (second, first) + role, lam = scale[1], Q(scale[2]) + exponent = int(role == add[1]) - int(role == add[2]) + assert exponent and lam + if first[0] == "SCALE": + exponent = -exponent + updated = [*add] + updated[3] = str(Q(add[3])*lam**exponent) + return (scale, updated) if first[0] == "ADD" else (updated, scale) + + +def scalar_product(events, roles): + rows = {r: [Q(int(r == j)) for j in roles] for r in roles} + for event in events: + op, d, *args = event + if op == "SCALE": + rows[d] = [Q(args[0])*v for v in rows[d]] + else: + s, coefficient, _ = args + rows[d] = [x+Q(coefficient)*y for x,y in zip(rows[d],rows[s],strict=True)] + return rows + + +def coefficient_legal(coefficient): + q = Q(coefficient) + denominator = q.denominator + for p in (2,3,5): + while denominator % p == 0: + denominator //= p + return q != 0 and denominator == 1 and abs(q)+1 < 2**16 + + +def controls(): + add = ["ADD",1,0,"-2",1] + for role, expected in ((1,"-3"), (0,"-4/3")): + scale = ["SCALE",role,"3/2",2] + old = (add,scale) + result = exchange(*old) + assert result[1][3] == expected + assert scalar_product(old,[0,1]) == scalar_product(result,[0,1]) + assert exchange(*result) == old + sign = [*result[1]] + sign[3] = str(-Q(sign[3])) + assert scalar_product(old,[0,1]) != scalar_product((result[0],sign),[0,1]) + assert coefficient_legal("-4/3") and not coefficient_legal("1/7") + assert not coefficient_legal(65535) + return ["exact_destination_and_source_conjugation", "both_orders", + "wrong_sign_rejected", "coefficient_alphabet_checked"] + + +def chronology(word, edge): + public, program = word["public"], word["program"] + current = word["initial"] + [None]*word["owned_fields"] + pending = defaultdict(list) + active, locations, incoming = {}, {}, {} + normalized, paid, owned_paid = [], Counter(), Counter() + for clock, event in enumerate(program): + op, role, *args = event + owned = role >= public + if op == "MOVE": + source,target,private = args + assert current[role] == source and private == owned + r = edge(source,target) + assert r and (owned or len(word["frames"][target]) > len(word["frames"][source])) + paid[r] += 1 + if owned: + assert role in active + owned_paid[r] += 1 + pending[role].append([clock,source,target,r]) + current[role] = target + continue + normalized.append(clock) + chart = args[-1] + if op == "INIT": + assert owned and current[role] is None and role not in active + assert not pending[role] + active[role] = [clock] + locations[role,clock] = active[role],0 + current[role] = chart + continue + for r in (role,args[0]) if op in ("ADD","COPY") else (role,): + assert current[r] == chart + if r < public: + continue + chain = active[r] + prior = chain[-1] + a = program[prior][-1] + rank = edge(a,chart) + path = pending.pop(r,[]) + assert (not path and rank == 0) or ( + len(path) == 1 and path[0][1:] == [a,chart,rank]) + incoming[r,clock] = path + locations[r,clock] = chain,len(chain) + chain.append(clock) + if op == "CLEAR": + assert owned + del active[role] + current[role] = None + assert not active and not any(pending.values()) + assert current == word["final"] + [None]*word["owned_fields"] + assert len(program) == 76443 and len(normalized) == 70163 and sum(paid.values()) == 6280 + assert owned_paid == {1:20,2:9,3:2,4:13,5:2,6:1} + return normalized, locations, incoming, paid, owned_paid + + +def gate(roots, out, start, seconds): + files = authenticate(roots) + input_prefix = "round30/complex/source/inputs/" + word,caller,early = (files[input_prefix+name] for name in ("WORD.json.gz","CALLER.json","EARLY-RESULT.json")) + predecessor = runpy.run_path(str(roots["7298"]/"verify.py")) + prior = predecessor["complex_scan"](word,caller,early) + assert json.loads(json.dumps(prior)) == files["7298/RESULT.json"]["complex"] + gf2_rank = predecessor["rank"] + cost = predecessor["PRICING"]["cost"] + frames = word["frames"] + + @cache + def edge(a,b): + if a == b: + return 0 + gap = abs(len(frames[a])-len(frames[b])) + distance = 2*gf2_rank(frames[a]+frames[b])-len(frames[a])-len(frames[b]) + return gap if gap and gap == distance else None + + normalized,loc,incoming,native,owned = chronology(word,edge) + p = Counter({int(k):v for k,v in early["invoice"]["P"].items()}) + targets = Counter({int(k):v for k,v in early["invoice"]["T"].items()}) + copies = prior["copies"] + net = targets.copy() + net.subtract(p) + kappa = Q(prior["probe"]) + baseline = cost(net,kappa) + assert sum(p.values()) == 110536 and sum(targets.values()) == 22461 and copies == 17 + assert baseline[1] < 0 and sum(k*v for k,v in net.items()) == 1424 + prog, public = word["program"],word["public"] + anchors = [i for i,t in enumerate(normalized) if prog[t][0] == "SCALE" and prog[t][1] >= public] + assert len(anchors) == 22 + stock_rank = copies*sum(k*v for k,v in owned.items()) + two_rank = copies*sum(sorted(owned.elements(),reverse=True)[:2]) + assert (stock_rank,two_rank) == (1904,187) + preprice = { + "head":HEAD, "inputs":PINS, "crossing_upper":str(kappa), + "complete_old_paid":p, "complete_targets":targets, "complete_old_margin":interval(baseline), + "complete_native_paid":native, "owned_paid":owned, "old_surplus":1424, "copies":copies, + "owned_scales":len(anchors), "neighbor_slot_cap":44, "hard_runner_cap_seconds":25, + "whole_compatible_stock_rank_upper_before_charges":stock_rank, + "single_swap_rank_upper_before_charges":two_rank, + "one_swap_only":True, "predecessor_add_add_receipt_reproduced":True, + "controls":controls(), + } + write(out,"PRICE.json",preprice) + + slots = sorted({j for i in anchors for j in (i-1,i) if 0 <= j < len(normalized)-1}) + assert len(slots) <= 44 + clocks = [(normalized[i],normalized[i+1]) for i in slots] + records = [] + for t,u in clocks: + if monotonic()-start >= seconds: + break + first,second = prog[t],prog[u] + row = {"clocks":[t,u],"literal":[first,second]} + records.append(row) + if {first[0],second[0]} != {"ADD","SCALE"}: + row["status"] = "other_neighbor" + continue + add,scale = (first,second) if first[0] == "ADD" else (second,first) + role = scale[1] + assert role >= public + if role not in add[1:3]: + row["status"] = "disjoint_roles" + continue + if first[-1] == second[-1] or Q(scale[2]) == 1: + row["status"] = "same_chart_or_unit_scale" + continue + rewritten = exchange(first,second) + replacement = next(event for event in rewritten if event[0] == "ADD") + if not coefficient_legal(replacement[3]): + row["status"] = "scalar_alphabet" + continue + domain = sorted(set(add[1:3])) + assert scalar_product([first,second],domain) == scalar_product(rewritten,domain) + chain,i = loc[role,t] + chain2,j = loc[role,u] + assert chain is chain2 and j == i+1 and i > 0 and j+1 < len(chain) + prev,nxt = chain[i-1],chain[j+1] + l,a,b,r = prog[prev][-1],first[-1],second[-1],prog[nxt][-1] + old = (edge(l,a),edge(b,r)) + new = (edge(l,b),edge(a,r)) + middle = edge(a,b) + assert None not in old and middle and middle == edge(b,a) + row.update(role=role, life_bounds=[chain[0],chain[-1]], contact_clocks=[prev,t,u,nxt], + chart_chain=[l,a,b,r], exterior_old=old, exterior_new=new, + literal_old_exterior_moves=incoming[role,t]+incoming[role,nxt], + old_middle_move=incoming[role,u], candidate_scalars=rewritten) + if None in new: + row["status"] = "nonnested" + continue + delta = Counter(x for x in old if x) + delta.subtract(x for x in new if x) + delta = {k:copies*v for k,v in delta.items() if v} + next_paid = p.copy() + next_paid.subtract(delta) + assert all(n >= 0 for n in next_paid.values()) + next_paid = +next_paid + next_net = targets.copy() + next_net.subtract(next_paid) + margin = cost(next_net,kappa) + row.update(full_paid=next_paid, paid_old_minus_new=delta, + incremental_moment=interval(cost(delta,kappa)), + complete_margin=interval(margin), + status="positive" if margin[0] > 0 else + ("possible_positive" if margin[1] > 0 else "no_positive_price")) + survivors = [r for r in records if r["status"] in ("positive","possible_positive")] + pending = clocks[len(records):] + result = { + "head":HEAD, "pair_slots":len(clocks), "visited":len(records), "unvisited":pending, + "unvisited_single_swap_rank_upper_before_charges":two_rank if pending else 0, + "counts":dict(Counter(r["status"] for r in records)), "survivors":survivors, "records":records, + } + write(out,"SUPPORT.json",result) + + +def main(): + start = monotonic() + if not __debug__: + raise RuntimeError("Run with assertions enabled") + parser = ArgumentParser(description=__doc__) + parser.add_argument("--round30",type=Path,required=True) + parser.add_argument("--predecessor",type=Path,required=True) + parser.add_argument("--out",type=Path,required=True) + parser.add_argument("--seconds",type=float,default=22) + args = parser.parse_args() + assert 0 < args.seconds <= 22 + args.out.mkdir(parents=True,exist_ok=True) + gate({"round30":args.round30.resolve(),"7298":args.predecessor.resolve()},args.out,start,args.seconds) + + +if __name__ == "__main__": + main() diff --git a/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz b/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz new file mode 100644 index 0000000000..290ef7c9c5 Binary files /dev/null and b/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz differ diff --git a/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz b/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz new file mode 100644 index 0000000000..8f4096badd Binary files /dev/null and b/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz differ diff --git a/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/WORD.json.gz b/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/WORD.json.gz new file mode 100644 index 0000000000..077bf48c35 Binary files /dev/null and b/research/p104-public-move-fusion-contact-bound/dependencies/round30/complex/source/inputs/WORD.json.gz differ diff --git a/research/p104-public-move-fusion-contact-bound/dependencies/round41/independent/replay_core.py b/research/p104-public-move-fusion-contact-bound/dependencies/round41/independent/replay_core.py new file mode 100644 index 0000000000..0a450da01e --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/dependencies/round41/independent/replay_core.py @@ -0,0 +1,182 @@ +"""Audit normalized owned-MOVE inputs using exact signed rational rows.""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +from hashlib import sha256 +import json +from math import gcd +from pathlib import Path +import time + +SHA = "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +OWNED_PAID = {1: 20, 2: 9, 3: 2, 4: 13, 5: 2, 6: 1} + + +def reduced(denominator, numerators): + if not numerators: + return 1, {} + factor = denominator + for n in numerators.values(): + factor = gcd(factor, n) + if factor == 1: + return denominator, numerators + return denominator // factor, {k: n // factor for k, n in numerators.items()} + + +def scaled(row, q): + denominator, numerators = row + return reduced(denominator * q.denominator, {k: q.numerator * n for k, n in numerators.items()}) + + +def plus(destination, source, q): + denominator, numerators = destination + s_den, s_num = source + right_denominator = s_den * q.denominator + common_factor = gcd(denominator, right_denominator) + left_scale = right_denominator // common_factor + right_scale = denominator // common_factor * q.numerator + sums = {k: left_scale * n for k, n in numerators.items()} if left_scale != 1 else numerators + for k, n in s_num.items(): + value = sums.get(k, 0) + right_scale * n + if value: + sums[k] = value + else: + sums.pop(k, None) + return reduced(denominator * left_scale, sums) + + +def frame_space(rows): + space = {0} + for row in rows: + space |= {v ^ row for v in space} + assert len(space) == 1 << len(rows) + return space + + +def audit(word, start, seconds, visit_owned_move=None): + public = word["public"] + roles = public + word["owned_fields"] + events = word["program"] + frames = [frame_space(f) for f in word["frames"]] + charts = word["initial"] + [None] * (roles - public) + rows = [(1, {r: 1}) for r in range(public)] + [None] * (roles - public) + fresh = set() + live = set() + owned_paid = Counter() + nonzero_clears = owned_copies = lifetimes = peak = visited = 0 + found, token_hits = [], [] + cap = start + seconds + for index, event in enumerate(events): + if index % 64 == 0 and time.monotonic() >= cap: + break + visited = index + 1 + op, d, *args = event + if op == "INIT": + frame, = args + assert d >= public and charts[d] is None and rows[d] is None and d not in live + rows[d], charts[d] = (1, {}), frame + fresh.add(d) + live.add(d) + lifetimes += 1 + peak = max(peak, len(live)) + elif op == "CLEAR": + frame, = args + assert d in live and charts[d] == frame + nonzero_clears += bool(rows[d][1]) + fresh.discard(d) + live.remove(d) + rows[d], charts[d] = None, None + elif op == "MOVE": + source, target, owned = args + assert charts[d] == source and owned == (d in live) == (d >= public) + assert frames[source] < frames[target] or (owned and frames[target] < frames[source]) + if owned: + rank = abs(len(word["frames"][target]) - len(word["frames"][source])) + if visit_owned_move is not None: + visit_owned_move(index, d, source, target, rank, charts, rows, live) + owned_paid[rank] += 1 + if not rows[d][1]: + found.append({"literal_index": index, "role": d, "from": source, "to": target, "rank": rank}) + if d in fresh: + assert not rows[d][1] + token_hits.append(index) + fresh.discard(d) + charts[d] = target + elif op == "SCALE": + coefficient, frame = args + q = Fraction(coefficient) + assert charts[d] == frame and q + rows[d] = scaled(rows[d], q) + else: + s, coefficient, frame = args + q = Fraction(coefficient) + assert op in ("ADD", "COPY") and d != s and charts[d] == frame == charts[s] and q + if op == "COPY": + assert d in live and d in fresh and not rows[d][1] + rows[d] = scaled(rows[s], q) + owned_copies += 1 + else: + rows[d] = plus(rows[d], rows[s], q) + fresh.discard(d) + first_unvisited = None if visited == len(events) else visited + remaining_move = next((i for i in range(visited, len(events)) if events[i][0] == "MOVE" and events[i][-1]), None) + if first_unvisited is None: + assert not live and not fresh and charts == word["final"] + [None] * (roles - public) + return { + "scope_exhausted": first_unvisited is None, + "literal_events": len(events), "literal_events_visited": visited, + "first_unvisited_literal_index": first_unvisited, + "first_unvisited_owned_move_index": remaining_move, + "paid_owned_histogram": owned_paid, "paid_owned_moves": sum(owned_paid.values()), + "exact_zero_moves": found, "fresh_zero_moves": len(token_hits), + "owned_lifetimes": lifetimes, "peak_owned": peak, "checked_copies": owned_copies, + "nonzero_owned_clears": nonzero_clears, + } + + +def control(): + # Same public input reaches an owned role with two different signed rational paths. + word = { + "public": 1, "owned_fields": 1, "initial": [0], "final": [0], "frames": [[], [1]], + "program": [ + ["INIT", 1, 0], ["COPY", 1, 0, "2/3", 0], + ["ADD", 1, 0, "-1/2", 0], ["ADD", 1, 0, "-1/6", 0], + ["MOVE", 1, 0, 1, True], ["CLEAR", 1, 1], + ], + } + observed = audit(word, time.monotonic(), 1) + assert observed["scope_exhausted"] + assert observed["exact_zero_moves"] == [{"literal_index": 4, "role": 1, "from": 0, "to": 1, "rank": 1}] + assert observed["fresh_zero_moves"] == 0 + word["program"][3][3] = "1/6" + changed = audit(word, time.monotonic(), 1) + assert changed["scope_exhausted"] and not changed["exact_zero_moves"] + return {"cancellation_detected": True, "changed_sign_rejected": True, "test_owned_move_index": 4} + + + +def main(): + if not __debug__: + raise RuntimeError("Run with assertions enabled") + start = time.monotonic() + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--word", required=True, type=Path) + parser.add_argument("--cap", default=22.0, type=float) + args = parser.parse_args() + assert 0 < args.cap <= 22.0 + raw = args.word.read_bytes() + if sha256(raw).hexdigest() != SHA: + raise ValueError("Unexpected compressed word SHA-256") + result = audit(json.loads(gzip.decompress(raw)), start, args.cap) + if result["scope_exhausted"]: + assert result["paid_owned_histogram"] == OWNED_PAID + assert tuple(result[k] for k in ("owned_lifetimes", "peak_owned", "checked_copies")) == (70, 49, 1) + print(json.dumps({"scientific_head": HEAD, "compressed_word_sha256": SHA, + **result, "control": control()}, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-public-move-fusion-contact-bound/engines/common_lift.py b/research/p104-public-move-fusion-contact-bound/engines/common_lift.py new file mode 100644 index 0000000000..030726d4dc --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/engines/common_lift.py @@ -0,0 +1,235 @@ +"""Exact price and local contact gate for one public MOVE fusion with one ADD.""" +from argparse import ArgumentParser +from bisect import bisect_right +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import runpy +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +WORD = 'dependencies/round30/complex/source/inputs/WORD.json.gz' +EARLY = 'dependencies/round30/complex/source/inputs/EARLY-RESULT.json' +CALLER = 'dependencies/round30/complex/source/inputs/CALLER.json' +PINS = { + WORD: '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + EARLY: '691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7', + CALLER: '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'lead/screen.py': 'c026ccad84094bc5a204aaad462c04dc0b63d92ed4a857fa5445a03b2cc0dbe1', + 'run/PRICE.json': 'b98a469e5250a7644b6e81ade01eb896b5f91bca18465a3166217e03fa35a306', + 'run/SUPPORT.json': '32d05c4efa4c3f6e3cf08fc9dd21478e0fb5218a38556e290966e64193fe2d80', + 'dependencies/7298/pricing.py': 'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', +} + + +def decode(raw): + def unique(pairs): + result = dict(pairs) + assert len(result) == len(pairs), 'duplicate JSON key' + return result + return json.loads(raw, object_pairs_hook=unique) + + +def save(out, name, data): + tmp = out / (name + '.tmp') + tmp.write_text(json.dumps(data, indent=2, sort_keys=True) + '\n') + tmp.replace(out / name) + + +def index_contacts(program): + chains = defaultdict(list) + for t, event in enumerate(program): + roles = event[1:3] if event[0] in ('ADD','COPY') else event[1:2] + assert len(set(roles)) == len(roles) + for r in roles: + chains[r].append(t) + return chains + + +def next_contact(chain, t): + i = bisect_right(chain, t) + return chain[i] if i < len(chain) else None + + +def contact_gate(program, contacts, row, public): + t, u = row['moves'] + v, = row['contacts'] + r = row['role'] + a,b,c = row['charts'] + assert t < v < u and r < public + assert list(program[t]) == ['MOVE',r,a,b,False] and list(program[u]) == ['MOVE',r,b,c,False] + op,d,s,q,frame = program[v] + assert op == 'ADD' and frame == b and r in (d,s) and d != s and Q(q) + peer = s if r == d else d + own = peer >= public + assert next_contact(contacts[r],t) == v and next_contact(contacts[r],v) == u + peer_move = next_contact(contacts[peer],v) + result = dict(role=r,moves=[t,u],charts=[a,b,c],add_clock=v,add=list(program[v]), + other_role=peer,first_other_contact=peer_move) + if peer_move is None or list(program[peer_move]) != ['MOVE',peer,b,c,own]: + result.update(status='other_first_contact_not_required_lift', + blocking_event=None if peer_move is None else list(program[peer_move])) + return result + later = max(u,peer_move) + assert peer_move != u + next_r = next_contact(contacts[r],u) + next_s = next_contact(contacts[peer],peer_move) + result.update(other_lift_clock=peer_move,later_lift_clock=later, + next_moved_role_contact=next_r,next_other_role_contact=next_s) + if any(clock is not None and clock <= later for clock in (next_r,next_s)): + result['status'] = 'post_lift_contact_before_join' + return result + result.update(status='support_only',remove=[t,v],replace_clock=u, + replacement=['MOVE',r,a,c,False],insert_after_clock=later, + retimed_add=['ADD',d,s,q,c],unchanged_other_move=list(program[peer_move])) + return result + + +def controls(): + positive = [ + ['MOVE',0,0,1,False], ['ADD',0,1,'-3/2',1], ['MOVE',1,1,2,False], + ['SCALE',2,'2',1], ['MOVE',0,1,2,False], ['ADD',1,0,'1',2], + ] + row = dict(moves=[0,4],contacts=[1],role=0,charts=[0,1,2]) + yes = contact_gate(positive,index_contacts(positive),row,3) + assert yes['status']=='support_only' and yes['retimed_add']==['ADD',0,1,'-3/2',2] + blocked = positive.copy() + blocked[3] = ['ADD',2,1,'2',2] + assert contact_gate(blocked,index_contacts(blocked),row,3)['status']=='post_lift_contact_before_join' + wrong = positive.copy() + wrong[2] = ['SCALE',1,'1',1] + assert contact_gate(wrong,index_contacts(wrong),row,3)['status']=='other_first_contact_not_required_lift' + reverse = positive[:2]+[positive[4],positive[3],positive[2],positive[5]] + rev = contact_gate(reverse,index_contacts(reverse),row | {'moves':[0,2]},3) + assert rev['status']=='support_only' and rev['insert_after_clock']==4 + return ['other_lift_first', 'moved_role_lift_first', 'intervening_read_blocks', 'wrong_first_lift_rejected'] + + +def run(root, out, cap, seconds, start): + raw = {} + for name, pin in PINS.items(): + raw[name] = (root/name).read_bytes() + assert sha256(raw[name]).hexdigest() == pin, ('changed dependency',name) + word = decode(gzip.decompress(raw[WORD])) + early,caller = (decode(raw[x]) for x in (EARLY,CALLER)) + old, support = (decode(raw[x]) for x in ('run/PRICE.json','run/SUPPORT.json')) + assert old['head'] == support['head'] == HEAD and support['scope_exhausted'] + assert not old['unresolved_price'] and not support['unresolved'] + full = old['records'] + prior = support['records'] + assert len(full) == len(prior) == old['pair_scope'] == 4732 + copies,k = old['copies'],Q(old['crossing_upper']) + assert [e[1] for e in caller['events'] if e[0]=='J'] == list(range(1,18)) + assert copies == 17 and k == Q(early['price']['independent_raw_bracket'][1]) + paid,productive = (Counter({int(r):n for r,n in early['invoice'][key].items()}) for key in ('P','T')) + assert dict(paid)=={int(r):n for r,n in old['old_full_paid'].items()} + assert dict(productive)=={int(r):n for r,n in old['old_full_targets'].items()} + assert sum(paid.values())==110536 and sum(productive.values())==22461 + cost = runpy.run_path(str(root/'dependencies/7298/pricing.py'))['cost'] + matching = runpy.run_path(str(root/'lead/screen.py'))['stock'] + net = productive.copy() + net.subtract(paid) + interval = lambda pair: list(map(str,pair)) + baseline = interval(cost(net,k)) + assert baseline == old['old_margin'] and Q(baseline[1]) < 0 + program = word['program'] + + @cache + def quote(x,y): + delta = Counter({x:copies}) + delta[y] += copies + delta[x+y] -= copies + edited = net.copy() + edited.update(delta) + return interval(cost(delta,k)),interval(cost(edited,k)),{str(r):n for r,n in delta.items()} + + def key(row): + return tuple(row['moves']) + + stock, credits = [], {} + for original,evidence in zip(full,prior,strict=True): + assert key(original)==key(evidence) and original['role']==evidence['role'] + if len(original['contacts']) != 1: + continue + clock = original['contacts'][0] + if program[clock][0] != 'ADD': + continue + assert evidence['status']=='scalar_exclusion' and evidence['scalar_evidence']==[[clock,'nonzero_add_source']] + assert original['fused_rank']==sum(original['ranks']) + saving,margin,delta = quote(*original['ranks']) + assert (saving,margin,delta)==(original['saving'],original['complete_margin'],original['full_paid_old_minus_new']) + assert key(original) not in credits + credits[key(original)] = max(Q(0),Q(saving[1])) + stock.append(original) + assert len(stock)==len(credits)==1922 + + def upper(retained): + return str(matching(full,[credits.get(key(row),Q(0)) if key(row) in retained else Q(0) for row in full])) + + whole = upper(credits.keys()) + save(out,'PRICE.json',dict(head=HEAD,pins=PINS,crossing_upper=str(k),copies=copies, + baseline_interval=baseline,original_paid=dict(paid),original_productive=dict(productive), + eligible_stock=len(stock),whole_compatible_upper=whole, + cap=cap,seconds_cap=seconds,records=stock, + grant='One alternative at a time. Whole upper uses each old moved-role MOVE at most once and grants cross-role conflicts and added costs free.')) + if Q(whole) <= 0: + return + chains = index_contacts(program) + records = [] + for row in stock: + if len(records)==cap or monotonic()>=start+seconds-1: + break + decision = contact_gate(program,chains,row,word['public']) + decision['complete_margin'] = row['complete_margin'] + decision['directed_paid_lower_positive'] = Q(row['complete_margin'][0])>0 + if decision['status']=='support_only': + b,c=row['charts'][1:] + decision['retimed_add_chart_dimensions']=[len(word['frames'][b]),len(word['frames'][c])] + records.append(decision) + remaining=stock[len(records):] + survives=[r for r in records if r['status']=='support_only'] + retained={key(r) for r in remaining+survives} + save(out,'SUPPORT.json',dict(head=HEAD,pins=PINS,controls=controls(), + price_sha256=sha256((out/'PRICE.json').read_bytes()).hexdigest(), + checked=len(records),counts=dict(Counter(r['status'] for r in records)),remaining=[r['moves'] for r in remaining], + post_support_compatible_upper=upper(retained),survivors=survives,records=records, + gate='Support and paid price only. Signed native phase, fully charged ordinary work, precision, tape and complete verification pending.')) + + +def main(): + p=ArgumentParser() + p.add_argument('round48',type=Path,nargs='?') + p.add_argument('out',type=Path,nargs='?') + p.add_argument('--cap',type=int,default=1922,choices=range(1,1923),metavar='1..1922') + p.add_argument('--seconds',type=int,default=25,choices=range(2,26),metavar='2..25') + p.add_argument('--controls-only',action='store_true') + a=p.parse_args() + if a.controls_only: + print(json.dumps(controls())) + return + if a.round48 is None or a.out is None: + p.error('explicit Round 48 dependency root and fresh output required') + a.out.mkdir() + + def timeout(*_): + raise TimeoutError('hard runner deadline') + + signal(SIGALRM,timeout) + alarm(a.seconds) + try: + run(a.round48,a.out,a.cap,a.seconds,monotonic()) + except TimeoutError: + save(a.out,'TIMEOUT.json',dict(head=HEAD,status='hard_timeout',unverified=1922, + price_saved=(a.out/'PRICE.json').exists())) + raise SystemExit(2) + finally: + alarm(0) + + +if __name__=='__main__': + main() diff --git a/research/p104-public-move-fusion-contact-bound/engines/common_lift_audit.py b/research/p104-public-move-fusion-contact-bound/engines/common_lift_audit.py new file mode 100644 index 0000000000..7f41006775 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/engines/common_lift_audit.py @@ -0,0 +1,171 @@ +"""Independently enumerate the literal one-ADD windows and reverse-scan blockers.""" +import argparse +from collections import Counter, defaultdict +from fractions import Fraction +import gzip +from hashlib import sha256 +from itertools import pairwise +import json +from pathlib import Path +import signal + +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +PINS = { + "WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "PRICE.json": "8904cdfebbf5f4c9612ece9c106d2d8f98c81ebb76a54fce6a3608f47da4b85e", + "SUPPORT.json": "5004e8ec6096597f4ed54d27afd069799410363c891d8e1be36fbc0ba7527bf8", +} + + +def unique(pairs): + obj = dict(pairs) + assert len(obj) == len(pairs) + return obj + + +def read(path, key): + data = path.read_bytes() + if sha256(data).hexdigest() != PINS[key]: + raise ValueError("changed dependency " + key) + if key.endswith(".gz"): + data = gzip.decompress(data) + return json.loads(data, object_pairs_hook=unique) + + +def touch(event): + return event[1:3] if event[0] in ("ADD","COPY") else event[1:2] + + +def literal_windows(word): + tape = word["program"] + n = word["public"] + paths = defaultdict(list) + physical = word["initial"] + [None]*word["owned_fields"] + spans = [] + for axes in word["frames"]: + row = {0} + for axis in axes: + assert axis not in row + row |= {axis ^ x for x in row} + spans.append(row) + for i,e in enumerate(tape): + op,r,*args = e + if op == "MOVE": + a,b,owned = args + assert owned == (r>=n) and physical[r] == a + assert spans[a]=n + physical[r] = args[0] + elif op == "CLEAR": + assert physical[r] == args[0] and r>=n + physical[r] = None + else: + assert op in ("ADD","COPY","SCALE") + assert all(physical[j]==e[-1] for j in touch(e)) + for role in touch(e): + if role < n: + paths[role].append(i) + assert physical == word["final"] + [None]*word["owned_fields"] + stock = [] + windows = 0 + for role, chain in paths.items(): + moves = [i for i,t in enumerate(chain) if tape[t][0]=="MOVE"] + for left,right in pairwise(moves): + windows += 1 + if right-left != 2: + continue + t, add, u = chain[left:right+1] + if tape[add][0] != "ADD": + continue + _,_,a,b,_ = tape[t] + _,_,bb,c,_ = tape[u] + _,d,s,q,frame = tape[add] + assert bb == b == frame and spans[a]=public]: + later = max(u,peer) + if any(v is not None and v<=later for v in (next_at[u,r],next_at[peer,other])): + status = "post_lift_contact_before_join" + else: + status = "support_only" + if event is None: + detail = "no_later_contact" + elif event[0]=="MOVE": + assert event[1]==other and event[2]==b + detail = "move_wrong_destination" if event[3]!=c else "move_to_required_destination" + elif event[0] in ("ADD","COPY"): + detail = event[0].lower()+("_source_read" if event[2]==other else "_destination") + else: + detail = event[0].lower() + records.append(dict(role=r,moves=[t,u],add_clock=add,add=tape[add],other_role=other, + charts=[a,b,c],first_other_contact=peer,blocking_event=event, + status=status,first_other_contact_class=detail)) + return records + + +def controls(): + p = [["MOVE",0,0,1,False],["ADD",0,1,"-3/2",1],["MOVE",1,1,2,False], + ["SCALE",2,"2",1],["MOVE",0,1,2,False],["ADD",1,0,"1",2]] + row = (0,4,0,1,1,0,1,2) + assert classify(p,[row],3)[0]["status"] == "support_only" + reversed_lifts = p[:2]+[p[4],p[3],p[2],p[5]] + assert classify(reversed_lifts,[(0,2,0,1,1,0,1,2)],3)[0]["status"] == "support_only" + p[3] = ["ADD",2,1,"2",2] + assert classify(p,[row],3)[0]["status"] == "post_lift_contact_before_join" + p[2] = ["MOVE",1,1,3,False] + r = classify(p,[row],3)[0] + assert r["status"] == "other_first_contact_not_required_lift" + assert r["first_other_contact_class"] == "move_wrong_destination" + return ["both_lift_orders","post_lift_source_read","wrong_lift_destination"] + + +def run(word, price, support): + assert price["head"] == support["head"] == HEAD + assert support["price_sha256"] == PINS["PRICE.json"] + assert not support["survivors"] and not support["remaining"] + windows = literal_windows(word) + records = classify(word["program"],windows,word["public"]) + assert len(records) == len(price["records"]) == len(support["records"]) == 1922 + for r,p,s in zip(records,price["records"],support["records"],strict=True): + assert (r["role"],r["moves"],r["charts"],[r["add_clock"]]) == ( + p["role"],p["moves"],p["charts"],p["contacts"]) + assert all(r[k]==s[k] for k in r if k!="first_other_contact_class") + statuses = Counter(r["status"] for r in records) + assert statuses == support["counts"] == {"other_first_contact_not_required_lift":1922} + counts = Counter(r["first_other_contact_class"] for r in records) + by_opcode = Counter(r["blocking_event"][0] if r["blocking_event"] else "NONE" for r in records) + return dict(head=HEAD, pins=PINS, total_windows=4732, exact_one_add=1922, + statuses=statuses, first_blockers=counts, by_opcode=by_opcode, + controls=controls(), all_cases_match_lead=True, unresolved=0, survivors=0) + + +if __name__ == "__main__": + assert __debug__ + p=argparse.ArgumentParser(description=__doc__) + p.add_argument("word", type=Path) + p.add_argument("receipt_root", type=Path) + a=p.parse_args() + signal.alarm(24) + print(json.dumps(run(read(a.word,"WORD.json.gz"),read(a.receipt_root/"PRICE.json","PRICE.json"), + read(a.receipt_root/"SUPPORT.json","SUPPORT.json")),indent=2,sort_keys=True)) diff --git a/research/p104-public-move-fusion-contact-bound/engines/silence.py b/research/p104-public-move-fusion-contact-bound/engines/silence.py new file mode 100644 index 0000000000..05ee53b8dd --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/engines/silence.py @@ -0,0 +1,251 @@ +"""Inventory and exact scalar-silence gate for one #7277 public MOVE fusion.""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from hashlib import sha256 +import json +from pathlib import Path +import runpy +from time import monotonic + +R47 = "04c6f986b45945dcb4df22bcbfc74780e5840ff9c97b6c4dad064fc2c5576f75" +CORE = "fd7a1a7f9cb8f71caa5e0d89ed16ea056503fa283bc05f655eb0da7e8d5fc6e0" +LIMIT = 6279 + + +def checked(path, pin): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"Unexpected source hash for {path.name}") + return raw + + +def contacts(event): + return event[1:3] if event[0] in ("ADD","COPY") else event[1:2] + + +def enumerate_pairs(word, edge): + prior, middle = {}, defaultdict(list) + pairs = [] + for clock,event in enumerate(word["program"]): + op, role, *args = event + if op == "MOVE": + source,dest,owned = args + if owned: + continue + rank = edge(source,dest) + assert role < word["public"] and rank + if role in prior: + first,a,b,x = prior[role] + assert b == source + pairs.append({"moves":[first,clock], "role":role, "charts":[a,b,dest], + "ranks":[x,rank], "contacts":middle.pop(role,[])}) + prior[role] = (clock,source,dest,rank) + else: + assert op in ("ADD","SCALE","COPY","INIT","CLEAR") + for r in contacts(event): + if r in prior: + middle[r].append(clock) + assert len(pairs) <= LIMIT + return pairs + + +def stock(pairs, uppers): + """Maximum bound with no old MOVE credited twice. Cross-role clashes are granted away.""" + windows = defaultdict(list) + for pair,upper in zip(pairs,uppers,strict=True): + windows[pair["role"]].append((pair["moves"],upper)) + total = Q(0) + for edges in windows.values(): + before, last = Q(0), Q(0) + previous = None + for (first,second), credit in edges: + assert previous is None or first == previous + before,last = last,max(last,before+credit) + previous = second + total += last + return total + + +def silent(event, rows, fresh): + op,d,*args = event + if op == "ADD": + s = args[0] + if rows[s][1]: + return "nonzero_add_source" + return "fresh_token_change" if d in fresh else "silent_zero_source_add" + if op == "SCALE": + return "nonzero_scale_row" if rows[d][1] else "silent_zero_row_scale" + return "hard_contact" + + +def scalar_audit(path, raw): + source = raw.decode() + old = "def audit(word, start, seconds, visit_owned_move=None):" + new = "def audit(word, start, seconds, visit_owned_move=None, visit_scalar=None):" + key = " op, d, *args = event\n" + assert source.count(old) == source.count(key) == 1 + adapter = (" if visit_scalar is not None and op in ('ADD','SCALE','COPY'):\n" + " visit_scalar(index, event, rows, fresh)\n") + source = source.replace(old,new).replace(key,key+adapter) + scope = {"__name__":"r48_signed_replay", "__file__":str(path)} + exec(compile(source,str(path),"exec"),scope) + return scope["audit"] + + +def controls(audit): + zero = (1,{}) + one = (1,{0:1}) + add = ["ADD",0,1,"-3/2",1] + assert silent(add,[one,zero],set()) == "silent_zero_source_add" + assert silent(add,[one,zero],{0}) == "fresh_token_change" + assert silent(add,[one,one],set()) == "nonzero_add_source" + assert silent(["COPY",0,1,"1",1],[one,zero],set()) == "hard_contact" + word = {"public":1,"owned_fields":1,"frames":[[],[1],[1,2]],"initial":[0],"final":[2], + "program":[["INIT",1,0],["COPY",1,0,"1",0],["ADD",0,1,"-1",0], + ["CLEAR",1,0],["MOVE",0,0,1,False],["SCALE",0,"3/2",1], + ["MOVE",0,1,2,False]]} + observed = {} + report = audit(word,monotonic(),1,visit_scalar=lambda i,e,rows,fresh: + observed.update({i:silent(e,rows,fresh)})) + assert report["scope_exhausted"] and observed[5] == "silent_zero_row_scale" + word["program"][2][3] = "1" + report = audit(word,monotonic(),1,visit_scalar=lambda i,e,rows,fresh: + observed.update({i:silent(e,rows,fresh)})) + assert report["scope_exhausted"] and observed[5] == "nonzero_scale_row" + assert stock([{"role":0,"moves":[1,2]},{"role":0,"moves":[2,3]}, + {"role":0,"moves":[3,4]}],[Q(2),Q(3),Q(2)]) == 4 + return ["zero_source_add","fresh_token_barrier","copy_barrier","exact_signed_zero_row_scale", + "changed_sign_breaks_silence","stock_cannot_double_spend_middle_move"] + + +def main(args, start): + source = checked(args.r47,R47) + assert source + old = runpy.run_path(str(args.r47)) + roots = {"round30":args.round30,"7298":args.predecessor} + files = old["authenticate"](roots) + core = checked(args.core,CORE) + prefix = "round30/complex/source/inputs/" + word,caller,early = (files[prefix+x] for x in ("WORD.json.gz","CALLER.json","EARLY-RESULT.json")) + previous = runpy.run_path(str(args.predecessor/"verify.py")) + receipt = previous["complex_scan"](word,caller,early) + assert json.loads(json.dumps(receipt)) == files["7298/RESULT.json"]["complex"] + rank, cost = previous["rank"],previous["PRICING"]["cost"] + frames = word["frames"] + + @cache + def edge(a,b): + if a == b: + return 0 + gap = abs(len(frames[a])-len(frames[b])) + distance = 2*rank(frames[a]+frames[b])-len(frames[a])-len(frames[b]) + return gap if gap and gap == distance else None + + _,_,_,native,owned = old["chronology"](word,edge) + paid = Counter({int(k):v for k,v in early["invoice"]["P"].items()}) + targets = Counter({int(k):v for k,v in early["invoice"]["T"].items()}) + kappa,copies = Q(receipt["probe"]),receipt["copies"] + net = targets.copy() + net.subtract(paid) + base = cost(net,kappa) + assert sum(paid.values()) == 110536 and sum(targets.values()) == 22461 and copies == 17 + assert base[1] < 0 and sum(k*v for k,v in net.items()) == 1424 + pairs = enumerate_pairs(word,edge) + program = word["program"] + + @cache + def quote(x,y): + delta = Counter({x:copies}) + delta[y] += copies + delta[x+y] -= copies + new_net = net.copy() + new_net.update(delta) + return old["interval"](cost(delta,kappa)),old["interval"](cost(new_net,kappa)),dict(delta) + + eligible, rows, uppers = [],[],[] + for pair in pairs: + if monotonic()-start >= args.seconds: + break + a,b,c = pair["charts"] + x,y = pair["ranks"] + fused = edge(a,c) + barriers = [i for i in pair["contacts"] if program[i][0] not in ("ADD","SCALE")] + row = {**pair,"fused_rank":fused,"hard_contacts":barriers} + rows.append(row) + if fused != x+y or barriers: + row["status"] = "structural_exclusion" + uppers.append(Q(0)) + continue + saving,margin,delta = quote(x,y) + row.update(saving=saving,complete_margin=margin,full_paid_old_minus_new=delta, + status="price_candidate" if Q(margin[1]) > 0 else "price_exclusion") + uppers.append(max(Q(0),Q(saving[1]))) + if row["status"] == "price_candidate": + eligible.append(row) + + unresolved_price = pairs[len(rows):] + upper = stock(pairs,uppers+[Q(copies*sum(pair["ranks"])) for pair in unresolved_price]) + price = { + "head":old["HEAD"],"input_pins":{**old["PINS"],"r47/lead/screen.py":R47, + "round41/independent/replay_core.py":CORE}, + "crossing_upper":str(kappa),"copies":copies,"old_margin":old["interval"](base), + "old_full_paid":paid,"old_full_targets":targets,"old_native_paid":native,"old_owned_paid":owned, + "pair_scope":len(pairs),"priced":len(rows),"whole_compatible_upper":str(upper), + "unresolved_price":unresolved_price,"price_candidates":len(eligible),"records":rows, + "budget":{"pair_limit":LIMIT,"hard_seconds":45,"cooperative_seconds":args.seconds}, + } + old["write"](args.out,"PRICE.json",price) + if args.inventory_only or unresolved_price or upper <= 0: + return + + audit = scalar_audit(args.core,core) + verified_controls = controls(audit) + requested = {i for pair in eligible for i in pair["contacts"]} + observed = {} + def observe(i,event,rows,fresh): + if i in requested: + observed[i] = silent(event,rows,fresh) + + decoded = None + if requested and monotonic()-start < args.seconds: + decoded = audit(word,start,args.seconds,visit_scalar=observe) + decisions = [] + for row in eligible: + states = [[i,observed.get(i,"unvisited")] for i in row["contacts"]] + failing = [s for _,s in states if s not in ("unvisited","silent_zero_source_add","silent_zero_row_scale")] + if failing: + status = "scalar_exclusion" + elif any(s == "unvisited" for _,s in states): + status = "unresolved" + elif Q(row["complete_margin"][0]) > 0: + status = "positive_contact_free" if not states else "positive_silent_contacts" + else: + status = "unresolved_price_interval" + decisions.append({**row,"status":status,"scalar_evidence":states}) + old["write"](args.out,"SUPPORT.json",{ + "head":old["HEAD"],"counts":dict(Counter(r["status"] for r in decisions)), + "scope_exhausted":all(not r["status"].startswith("unresolved") for r in decisions), + "unresolved":[r["moves"] for r in decisions if r["status"].startswith("unresolved")], + "survivors":[r for r in decisions if r["status"].startswith("positive")], + "controls":verified_controls,"literal_signed_replay":decoded,"records":decisions, + }) + + +if __name__ == "__main__": + start = monotonic() + if not __debug__: + raise RuntimeError("Run with assertions enabled") + parser = ArgumentParser(description=__doc__) + for flag in ("r47","round30","predecessor","core","out"): + parser.add_argument("--"+flag,type=Path,required=True) + parser.add_argument("--seconds",type=float,default=42) + parser.add_argument("--inventory-only",action="store_true") + args = parser.parse_args() + assert 0 < args.seconds <= 42 + for name in ("r47","round30","predecessor","core","out"): + setattr(args,name,getattr(args,name).resolve()) + args.out.mkdir(parents=True,exist_ok=True) + main(args,start) diff --git a/research/p104-public-move-fusion-contact-bound/engines/silence_audit.py b/research/p104-public-move-fusion-contact-bound/engines/silence_audit.py new file mode 100644 index 0000000000..a304af2f3d --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/engines/silence_audit.py @@ -0,0 +1,204 @@ +"""Independently certify non-silence for the literal #7277 public MOVE pairs.""" + +import argparse +from bisect import bisect_left, bisect_right +from collections import Counter, defaultdict +from fractions import Fraction +import gzip +from hashlib import sha256 +from itertools import pairwise +import json +from math import isqrt +from pathlib import Path +from time import monotonic + +WORD = "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +PRICE = "b98a469e5250a7644b6e81ade01eb896b5f91bca18465a3166217e03fa35a306" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +MOD = 65521 + + +def read(path,pin): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"Bad SHA-256 for {path.name}") + return json.loads(gzip.decompress(raw) if raw[:2] == b"\x1f\x8b" else raw) + + +def space(basis): + result = {0} + for v in basis: + assert v not in result + result.update(v^x for x in list(result)) + return result + + +def inventory(word, frames): + program, n = word["program"],word["public"] + moves, contacts = defaultdict(list),defaultdict(list) + for index,event in enumerate(program): + tag, r, *args = event + if tag == "MOVE": + assert args[-1] == (r >= n) + if r < n: + moves[r].append(index) + else: + assert tag in ("ADD","COPY","SCALE","INIT","CLEAR") + for v in (event[1:3] if tag in ("ADD","COPY") else event[1:2]): + if v < n: + contacts[v].append(index) + cases = {} + for role, chain in moves.items(): + between = contacts[role] + for left,right in pairwise(chain): + a,b = program[left][2:4] + mid,c = program[right][2:4] + assert b == mid and frames[a] < frames[b] < frames[c] + gap = between[bisect_right(between,left):bisect_left(between,right)] + assert gap and all(program[t][0] in ("ADD","SCALE") for t in gap) + cases[left,right] = {"role":role,"charts":[a,b,c],"contacts":gap} + return moves,cases + + +def tariff_matching(moves, quotes): + result = Fraction(0) + for chain in moves.values(): + prefix = [Fraction(0)]*(len(chain)+1) + for j in range(2,len(prefix)): + weight = quotes[chain[j-2],chain[j-1]] + prefix[j] = max(prefix[j-1],prefix[j-2]+weight) + result += prefix[-1] + return result + + +def coeff(raw): + q = Fraction(raw) + assert q and q.denominator % MOD + return q.numerator*pow(q.denominator,-1,MOD)%MOD + + +def replay(word, frames, requested, deadline): + n = word["public"] + charts = list(word["initial"])+[None]*word["owned_fields"] + values = [{r:1} for r in range(n)]+[None]*word["owned_fields"] + fresh, owned = set(),set() + proofs = {} + hist = Counter() + first_unvisited = None + for i, event in enumerate(word["program"]): + if i%64 == 0 and monotonic() >= deadline: + first_unvisited = i + break + op,d,*args = event + if op == "INIT": + assert d >= n and charts[d] is None + charts[d], values[d] = args[0],{} + owned.add(d) + fresh.add(d) + elif op == "CLEAR": + assert d in owned and charts[d] == args[0] + charts[d], values[d] = None,None + owned.remove(d) + fresh.discard(d) + elif op == "MOVE": + a,b,flag = args + assert charts[d] == a and flag == (d in owned) == (d >= n) + assert frames[a] < frames[b] or (flag and frames[b] < frames[a]) + hist[abs(len(word["frames"][a])-len(word["frames"][b]))] += 1 + charts[d] = b + fresh.discard(d) + elif op == "SCALE": + q,f = args + assert charts[d] == f + a = coeff(q) + assert a + if i in requested and values[d]: + j = min(values[d]) + if (w := (a-1)*values[d][j]%MOD): + proofs[i] = [i,"scale_row",d,j,values[d][j],w] + values[d] = {j:a*v%MOD for j,v in values[d].items()} + else: + assert op in ("ADD","COPY") + s,q,f = args + assert d != s and charts[d] == f == charts[s] + a = coeff(q) + if op == "COPY": + assert d in owned and d in fresh and not values[d] + values[d] = {} + if i in requested and op == "ADD" and values[s]: + j = min(values[s]) + if (w := a*values[s][j]%MOD): + proofs[i] = [i,"add_source",s,j,values[s][j],w] + for j,v in values[s].items(): + x = (values[d].get(j,0)+a*v)%MOD + if x: + values[d][j] = x + else: + values[d].pop(j,None) + fresh.discard(d) + if first_unvisited is None: + assert not owned and charts == word["final"]+[None]*word["owned_fields"] + return proofs,first_unvisited,hist + + +def controls(): + word = {"public":1,"owned_fields":1,"frames":[[],[1],[1,2]],"initial":[0],"final":[2], + "program":[["MOVE",0,0,1,False],["INIT",1,1],["ADD",0,1,"1/2",1], + ["SCALE",0,"3/2",1],["CLEAR",1,1],["MOVE",0,1,2,False]]} + frames = list(map(space,word["frames"])) + proofs,stop,hist = replay(word,frames,{2,3},monotonic()+1) + assert stop is None and set(proofs) == {3} + word["program"][2:2] = [["COPY",1,0,"1",1]] + proofs,stop,hist = replay(word,frames,{3,4},monotonic()+1) + assert stop is None and set(proofs) == {3,4} + assert proofs[3][-1] == pow(2,-1,MOD) + assert tariff_matching({0:[0,1,2,3]},{(0,1):2,(1,2):3,(2,3):2}) == 4 + return ["zero_source_does_not_certify_nonzero","scale_row_nonzero","add_witness_uses_denominator", + "overlapping_middle_move_not_credited_twice"] + + +def main(): + start = monotonic() + if not __debug__: + raise RuntimeError("Assertions required") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--word",type=Path,required=True) + parser.add_argument("--price",type=Path,required=True) + parser.add_argument("--cap",type=float,default=42) + args = parser.parse_args() + assert 0 < args.cap <= 42 and all(MOD%d for d in range(2,isqrt(MOD)+1)) + word,price = read(args.word,WORD),read(args.price,PRICE) + frames = list(map(space,word["frames"])) + moves,cases = inventory(word,frames) + literal_keys = {tuple(row["moves"]):row for row in price["records"]} + assert len(cases) == len(literal_keys) == len(price["records"]) == 4732 + assert cases.keys() == literal_keys.keys() + for key,item in cases.items(): + assert all(literal_keys[key][field] == value for field,value in item.items()) + matching = tariff_matching(moves,{k:Fraction(row["saving"][1]) for k,row in literal_keys.items()}) + assert matching == Fraction(price["whole_compatible_upper"]) + requested = {i for pair in cases.values() for i in pair["contacts"]} + proofs,stop,hist = replay(word,frames,requested,start+args.cap) + if stop is None: + assert hist == {int(r):n for r,n in price["old_native_paid"].items()} + pair_proofs = [] + unresolved = [] + for key,item in sorted(cases.items()): + certificate = next((proofs[i] for i in item["contacts"] if i in proofs),None) + if certificate is None: + unresolved.append(key) + else: + pair_proofs.append([*key,certificate]) + receipt = { + "head":HEAD,"word_sha256":WORD,"price_sha256":PRICE,"prime":MOD, + "public_pairs":len(cases),"unique_contacts":len(requested),"nonzero_contact_count":len(proofs), + "certified_pair_exclusions":len(pair_proofs),"unresolved_pairs":unresolved, + "first_unvisited_literal_index":stop,"whole_compatible_upper_from_pinned_weights":str(matching), + "proved_pair_witness_kinds":dict(Counter(p[2][1] for p in pair_proofs)), + "pair_proofs":pair_proofs,"controls":controls(), + } + print(json.dumps(receipt,indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-public-move-fusion-contact-bound/receipts/SHA256.json b/research/p104-public-move-fusion-contact-bound/receipts/SHA256.json new file mode 100644 index 0000000000..8160697053 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/receipts/SHA256.json @@ -0,0 +1,8 @@ +{ + "common-lift/INDEPENDENT.json": "56ff15c2ed3cac9f9b550c03972e8b6e783c39197f148d96c05ecbf0129068a3", + "common-lift/PRICE.json": "8904cdfebbf5f4c9612ece9c106d2d8f98c81ebb76a54fce6a3608f47da4b85e", + "common-lift/SUPPORT.json": "5004e8ec6096597f4ed54d27afd069799410363c891d8e1be36fbc0ba7527bf8", + "scalar-silence/INDEPENDENT.json": "b149d69142f541b41901437187b5d5cdf28f669738f65eca43f76d5ffe8ba28a", + "scalar-silence/PRICE.json": "b98a469e5250a7644b6e81ade01eb896b5f91bca18465a3166217e03fa35a306", + "scalar-silence/SUPPORT.json": "32d05c4efa4c3f6e3cf08fc9dd21478e0fb5218a38556e290966e64193fe2d80" +} diff --git a/research/p104-public-move-fusion-contact-bound/receipts/SUMMARY.json b/research/p104-public-move-fusion-contact-bound/receipts/SUMMARY.json new file mode 100644 index 0000000000..fa4235e341 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/receipts/SUMMARY.json @@ -0,0 +1,37 @@ +{ + "common-lift": { + "checked": 1922, + "first_blockers": { + "add_destination": 459, + "add_source_read": 472, + "clear": 6, + "move_wrong_destination": 809, + "no_later_contact": 149, + "scale": 27 + }, + "pre_support_compatible_upper": "995923684989332345782183516098045872439490660145727/5000000000000000000000000000000000000000000000000", + "primary_status_counts": { + "other_first_contact_not_required_lift": 1922 + } + }, + "compatible_saving_after_support": "0", + "copies": 17, + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "kappa": "0.003645669928698", + "kappa_change": "0", + "scalar-silence": { + "certified_nonzero": 7721, + "checked": 4732, + "first_witness_counts": { + "add_source": 4553, + "scale_row": 179 + }, + "pre_support_compatible_upper": "3633275462698571757779133557747431543190346878676463/10000000000000000000000000000000000000000000000000", + "primary_status_counts": { + "scalar_exclusion": 4732 + }, + "prime": 65521, + "unique_contacts": 7721 + }, + "unresolved": 0 +} diff --git a/research/p104-public-move-fusion-contact-bound/replay.py b/research/p104-public-move-fusion-contact-bound/replay.py new file mode 100644 index 0000000000..1304441fb9 --- /dev/null +++ b/research/p104-public-move-fusion-contact-bound/replay.py @@ -0,0 +1,152 @@ +"""Rebuild both exact public MOVE fusion scopes and their independent receipts.""" +from argparse import ArgumentParser +import gzip +from hashlib import sha1, sha256 +import json +from pathlib import Path, PurePosixPath +import shutil +import subprocess +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +WORD = "round30/complex/source/inputs/WORD.json.gz" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def decode(data): + return json.loads(data, object_pairs_hook=unique) + + +def read(path): + return decode(path.read_bytes()) + + +def authenticate(scratch): + pins = read(HERE / "LOCAL-PINS.json") + for key, expected in pins.items(): + rel = PurePosixPath(key) + if rel.is_absolute() or ".." in rel.parts or rel.as_posix() != key: + raise ValueError(f"invalid dependency path {key}") + if sha256((HERE / key).read_bytes()).hexdigest() != expected: + raise ValueError(f"changed dependency {key}") + deps = scratch / "dependencies" + shutil.copytree(HERE / "dependencies", deps) + provenance = read(HERE / "PROVENANCE.json")["files"] + assert len(provenance) == 8 and sum(p["uncompress"] for p in provenance.values()) == 2 + for key, pin in provenance.items(): + assert key in pins + raw = (HERE / key).read_bytes() + if pin["uncompress"]: + raw = gzip.decompress(raw) + (scratch / key).with_suffix("").write_bytes(raw) + assert sha256(raw).hexdigest() == pin["sha256"], key + assert sha1(f"blob {len(raw)}\0".encode()+raw).hexdigest() == pin["git_blob"], key + return deps + + +def run(script, *args, timeout): + result = subprocess.run([sys.executable, "-I", "-B", str(script), *map(str,args)], + capture_output=True, check=True, timeout=timeout) + return result.stdout + + +def check_receipts(artifacts): + pins = read(HERE / "receipts/SHA256.json") + assert pins.keys() == artifacts.keys() + for key, path in artifacts.items(): + if sha256(path.read_bytes()).hexdigest() != pins[key]: + raise ValueError(f"replay receipt changed: {key}") + + +def crosscheck(artifacts): + price, support, independent = (read(artifacts[f"scalar-silence/{name}.json"]) + for name in ("PRICE","SUPPORT","INDEPENDENT")) + lift_price, lift, reverse = (read(artifacts[f"common-lift/{name}.json"]) + for name in ("PRICE","SUPPORT","INDEPENDENT")) + assert {r["head"] for r in (price,support,independent,lift_price,lift,reverse)} == {HEAD} + assert price["old_full_paid"] == lift_price["original_paid"] + assert price["old_full_targets"] == lift_price["original_productive"] + assert price["copies"] == lift_price["copies"] == 17 + assert price["crossing_upper"] == lift_price["crossing_upper"] + assert price["old_margin"] == lift_price["baseline_interval"] + assert len(price["records"]) == len(support["records"]) == independent["public_pairs"] == 4732 + assert not price["unresolved_price"] and not support["unresolved"] and not support["survivors"] + assert not independent["unresolved_pairs"] and independent["first_unvisited_literal_index"] is None + assert independent["whole_compatible_upper_from_pinned_weights"] == price["whole_compatible_upper"] + assert independent["unique_contacts"] == independent["nonzero_contact_count"] == 7721 + rows = {tuple(r["moves"]):r for r in support["records"]} + proofs = {(l,r):proof for l,r,proof in independent["pair_proofs"]} + assert len(rows) == len(proofs) == 4732 and rows.keys() == proofs.keys() + for key, proof in proofs.items(): + row = rows[key] + kind = {"add_source": "nonzero_add_source", "scale_row": "nonzero_scale_row"}[proof[1]] + assert row["status"] == "scalar_exclusion" and row["scalar_evidence"][0] == [proof[0],kind] + assert proof[-1] != 0 + assert len(lift_price["records"]) == len(lift["records"]) == reverse["exact_one_add"] == 1922 + assert reverse["total_windows"] == 4732 and reverse["all_cases_match_lead"] + assert not lift["survivors"] and not lift["remaining"] and reverse["unresolved"] == 0 + assert lift["post_support_compatible_upper"] == "0" + expected = read(HERE / "receipts/SUMMARY.json") + assert expected["scalar-silence"] == { + "checked": len(rows), "primary_status_counts": support["counts"], + "pre_support_compatible_upper": price["whole_compatible_upper"], + "unique_contacts": independent["unique_contacts"], "certified_nonzero": independent["nonzero_contact_count"], + "first_witness_counts": independent["proved_pair_witness_kinds"], "prime": independent["prime"], + } + assert expected["common-lift"] == { + "checked": len(lift["records"]), "primary_status_counts": lift["counts"], + "pre_support_compatible_upper": lift_price["whole_compatible_upper"], + "first_blockers": reverse["first_blockers"], + } + assert expected["head"] == HEAD and expected["copies"] == price["copies"] + assert expected["unresolved"] == 0 and expected["compatible_saving_after_support"] == "0" + assert expected["kappa_change"] == "0" + + +def replay(output): + with TemporaryDirectory(prefix="p104-move-fusion-") as temp: + scratch = Path(temp) + deps = authenticate(scratch) + engines = HERE / "engines" + lead = scratch / "lead" + lead.mkdir() + shutil.copyfile(engines / "silence.py", lead / "screen.py") + silence, lift = scratch / "run", scratch / "common-lift" + word = deps / WORD + run(lead / "screen.py", "--r47", deps / "r47/lead/screen.py", + "--round30", deps / "round30", "--predecessor", deps / "7298", + "--core", deps / "round41/independent/replay_core.py", "--out", silence, timeout=45) + (silence / "INDEPENDENT.json").write_bytes(run(engines / "silence_audit.py", + "--word", word, "--price", silence / "PRICE.json", timeout=45)) + run(engines / "common_lift.py", scratch, lift, "--cap", 1922, "--seconds", 25, timeout=25) + (lift / "INDEPENDENT.json").write_bytes(run(engines / "common_lift_audit.py", + word, lift, timeout=25)) + artifacts = {f"{scope}/{name}.json": folder / f"{name}.json" + for scope,folder in (("scalar-silence",silence),("common-lift",lift)) + for name in ("PRICE","SUPPORT","INDEPENDENT")} + check_receipts(artifacts) + crosscheck(artifacts) + if output is not None: + output.mkdir(parents=True, exist_ok=False) + for key, path in artifacts.items(): + target = output / key + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(path, target) + print("PASS_PUBLIC_MOVE_CONTACT_BOUND silence=4732 nonzero_contacts=7721 common_lift=1922 unresolved=0 saving_upper=0 kappa_change=0") + + +if __name__ == "__main__": + assert __debug__, "run with assertions enabled" + assert sys.version_info[:2] == (3,12), "Python 3.12 required" + parser = ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="fresh destination for the full deterministic receipts") + args = parser.parse_args() + replay(args.out)