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-type-b-simultaneous-idle-bound/LOCAL-PINS.json b/research/p104-type-b-simultaneous-idle-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..5824dde2ef --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/LOCAL-PINS.json @@ -0,0 +1,33 @@ +{ + "engines/stage_compare.py": "e8b53af84a49d0e7c79fb93d96061971b2f4e64f16b604a768ccaed4b35cf757", + "engines/stage_quote.py": "8c79975e8279f971ffa3bc60a9143ec489a26e16a37335ebba15a8720d4acfc3", + "engines/stage_support.py": "3b1496e1b688426ccbcce08566c0f841ca0e839297a3dac0bc4e1b023ffc58b4", + "engines/stage_tangent.py": "64704d99bda0739195c480385864182e4e6db0234c9d7c0200eebf0ff5c29c9e", + "r123/LOCAL-PINS.json": "4f5ce1e33442de204bbd9a5465ffe32af0cc49a2f21a2fe02d9dd259839a726e", + "r123/PROOF.md": "e6c749d92e8bdca5cd2bc6caf962c07140ae5e5c89a1c9974c3dd2c34be0bad4", + "r123/PROVENANCE.json": "048d70849ec7a6f93a060cfc5a4cb9aaa2609cf6ab57f6085c13d16978417cdc", + "r123/engines/compare.py": "91ce91a5e99bfc629ffc400487b6331c5be86459397a293bf2f90753859d3cef", + "r123/engines/pair_derivative.py": "ce9477aadf31c0b21fefea1ae55059793c2a28fd070c7dcc501ca9b3b7151734", + "r123/engines/quote.py": "3a676f5d102c3aa02522937b85275b0fb16cfce98797c667370e85c91774e05c", + "r123/engines/tangent.py": "8ad672bd808b6b8c30306fa2b125b19be5e8c19215425b79dc592e552a96b169", + "r123/inputs/7113-CALLER.json.gz": "7e8038559cd158f6e32ef6d1a3bf15ab6a8ecc2239af32ab1699511ac28e26d9", + "r123/inputs/PR7357-SHA256.json": "877af2f9d65e0457e74f843a6ede78571ffdf9d57e7565d383c3c4d6be91d54c", + "r123/inputs/direct_impulse.py": "d04426aed9528aedc6400d384d7fd13c6531e5e3e6592a7eea4faee46c61e004", + "r123/r85/independent/RESULT.json.gz": "62888bf58026aebb87019c1e76eeec885317f4da6e703c7fe8a2f90a7a019c49", + "r123/r85/independent/SHA256": "cfcac30934a139cf120885ee210c0923b60f387ecb880f18ea92ff0d33a159ba", + "r123/r85/lead/RESULT.json.gz": "30c782c2faab1387d9394f6e95874507a34a151596e45c758d979cec11e21f3d", + "r123/r85/price/PRICE.json.gz": "67ae145bb973e0e9dd759bd5b0433ca64c2483100a5c7d00a236916992567eac", + "r123/r85/price/SHA256": "37e11ffc1979e090deb4e046e7b770339a3d9e1898fff8b5a04f4a70da70e383", + "r123/r85/price/inputs/7334-ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "r123/r85/price/inputs/7334-READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "r123/r85/price/inputs/derivative_check.py": "348c8b2de72f1f112cb1337eca9d29ca96c85a7ad903beecafb1a2a1221f408e", + "r123/r85/price/inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "r123/receipts/AGREEMENT.json": "057201100051f25a72b22f0cbe49a8d20e08549043a4787faf25af6c5c8ee0a9", + "r123/receipts/SHA256.json": "06c464b960dc721b990cec4968edb35e5ba4a1ba73884a1c249422d2d9e1afed", + "r123/replay.py": "a038125efdc5fb0e2bf86bd9081b387755694e96e2757513f221a94e24348007", + "receipts/STAGE-AGREEMENT.json": "151d252274d03a1f0f0d0983921b108b8854d56486127f1deea18ffca857dc33", + "receipts/STAGE-INDEPENDENT.json": "5bf41ba41b70ee549526289d5e38a3987515dd387ef142a77d80a557a269e2a7", + "receipts/STAGE-LEAD.json": "01f4a0ff68b3a9428a82920a55751ccec7f5cf628cd2d9bd02bebbcaa6bbbde3", + "receipts/STAGE-PRICE.json": "8940a6b5e49e838fb6dba06b73500ee6c906f6dcc8422a04ac6d5eb7b7ecf397", + "replay.py": "eb2d1019b2bbfbcdde9771e777c41f90f184e5f068da3179de2830125a045c07" +} diff --git a/research/p104-type-b-simultaneous-idle-bound/NOTICE b/research/p104-type-b-simultaneous-idle-bound/NOTICE new file mode 100644 index 0000000000..66472c54e8 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/NOTICE @@ -0,0 +1,3 @@ +Apache-2.0. + +#7334 and #7113 supply the exact comparable application and caller. #7357 supplies the one-edit exact proof and predecessor replay bytes. #7315, #7323, #7356 and #7144 supply related derivative and signed cancellation methods, #7296 a related canonical-volume restriction and #7298 directed arithmetic. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-type-b-simultaneous-idle-bound/PROOF.md b/research/p104-type-b-simultaneous-idle-bound/PROOF.md new file mode 100644 index 0000000000..16ac67138d --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/PROOF.md @@ -0,0 +1,17 @@ +# Stagewise exclusion for simultaneous Type B unions + +The exact #7113 Type B caller has 36 normalized roles, eight ports and 17 body stages. A proposed union pairs one of four signed singleton odd idles with one of 60 even idles whose body mask is disjoint from the odd mask. The combined operation keeps the odd clock, role and phase sign and removes the even job. There are 180 permitted edges. A schedule chooses a nonempty matching of at most four edges and preserves all other operators. + +At q=+1 and all body variables one, the old and edited operators agree at every clock and all edited factors are identities. The old endpoint is identity on 36 columns. For clock c, let F be its prefix, S its suffix and E the projector on its role. A change in the derivative at c contributes SEF to the endpoint. At each stage j, the derivative difference for a schedule is the sum of these projectors at the odd clocks paired to even masks containing j, minus the sum at the corresponding even clocks. Other terms cancel. These two stage-local clock sets have the same cardinality. Every odd clock in such a set must have an original mask omitting j. Any exact schedule requires equality of the two sums at every stage. + +Both engines independently reconstruct the 64 projectors from all 4,783 caller events at the exact specialization. The lead uses prefix/inverse conjugation and three modular linear functionals on the exact rational projectors. All denominators are units at the chosen primes. The independent engine uses prefix covectors and suffix impulses, and an exact rational linear functional. Equality of matrices implies equality under each functional. Any equality of signatures is tested by an exact full rational matrix comparison. The independent implementation also counts stage-local subset pairs with at least one full mask-compatible matching. + +For each of 17 stages, the replay enumerates every equal-size odd/even subset pair of cardinality one through four under this necessary incidence restriction. The 26,075 relaxed cap admits 18,443 comparisons after removing odd sites whose original masks contain the stage, of which 4,527 admit a mask-compatible bijection. No modular collision or exact rational signature equality appears. There is no equal matrix sum. Every even site belongs to at least one stage, and each has an independently matching missing-stage certificate. Thus any nonempty schedule has a nonzero derivative at some stage and fails the arbitrary-input endpoint. No coupled search, formal nonunit gate or physical prototype is needed for this family. + +The nested two-edit proof additionally uses the exact #7357 one-edit derivatives to isolate an unmatched stage for all 11,728 unequal-mask placements. It explicitly computes the joint rational derivative at all 210 equal-mask placements. Both direct size-eight endpoint tangents give +16 at global coordinate (36,36) for the two possible matchings of odd clocks 1339/1340 and even clocks 2324/2337. The planted controls verify that two individually nonzero defects can cancel after swaps and that changing a sign can spoil that cancellation. [Exact two-edit proof](r123/PROOF.md) + +## Complete directed price + +The price uses 17 unchanged native words and all eight Type B ports. For each edge with even mask size m it replaces one rank-nine and one rank-8m position per port by one rank-(8m+9) position. Exact weighted matching over the 180 permitted edges counts each paid odd and even clock at most once. The favorable four-edit witness lowers paid positions from 110,519 to 110,487 and preserves 22,461 productive positions, rank surplus 1,424 and zero empty-root credit. Its total directed optimistic upper is 3.076075380146476 raw at the old crossing. At κ = 0.0040075385047236 the complete upper is −136.39071166273732. The relaxed price grants all ancillary work free. A candidate would have to account for changed setup, ownership, restoration, routing, precision and tape. + +The complete endpoint is required under the five inherited native, owned-erasure, compiler, precision/tape and analytic recovery premises. This scoped derivative obstruction rules out the specified fixed-clock unions under those premises. It leaves changed-clock, changed-role and changed-provider constructions open. diff --git a/research/p104-type-b-simultaneous-idle-bound/README.md b/research/p104-type-b-simultaneous-idle-bound/README.md new file mode 100644 index 0000000000..e98f8c7795 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/README.md @@ -0,0 +1,29 @@ +# Fixed-clock simultaneous Type B signed idle unions + +**NO VERIFIED GAIN.** Exact Δκ = 0 on independently reproduced conditional κ = `0.00364665195644`, #7334 at `aaeec8c0acf01e99a5f331ef363a698d9c084ace`, with signed #7113 at `07a76c5e2738882c0cb322278e56f6cae3c9885d`. [Comparator #7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) · [Signed caller #7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) + +Each proposed edit adds one disjoint even body mask to a signed odd idle at the original odd clock and role, and removes that even idle. We exclude every nonempty choice of at most four edits with distinct odd and even clocks and the rest of the caller fixed. Both engines exhaust 17 body stages and 18,443 stagewise subset comparisons. Of those, 4,527 admit a mask-compatible bijection. No exact projector sum agrees, and all 60 even sites have a missing-stage certificate. [Stagewise proof](PROOF.md) · [Agreement](receipts/STAGE-AGREEMENT.json) + +The nested two-edit test independently excludes all 11,728 unequal-mask and 210 equal-mask placements. The two largest size-eight cases also fail direct 36-column endpoint tangents, with witness +16 at global coordinate (36,36). [Two-edit proof](r123/PROOF.md) · [Two-edit agreement](r123/receipts/AGREEMENT.json) + +The optimistic four-edit matching would lower the paid position count from 110,519 to 110,487 and leave 22,461 productive positions fixed. The whole-stock upper is 3.076075380146476 raw at the incumbent. The complete fixed-target margin is at most −136.39071166273732. The tested family has no supported construction and zero verified savings. + +## Replay + +Use CPython 3.12 and assertions from a clean checkout. + +```sh +python3.12 -I -B research/p104-type-b-simultaneous-idle-bound/replay.py +``` + +The standard-library replay authenticates exact #7357 receipts and the signed #7113 caller, regenerates both complete prices and replays both engines at each scope. Add `--out fresh-directory` for all eight receipts. Altered predecessor, price and caller bytes reject. [Verification](VERIFICATION.md) · [Path-keyed pins](LOCAL-PINS.json) · [Source provenance](r123/PROVENANCE.json) + +## Open next questions + +Could a distinct paid mechanism preserve these body-stage responses with different clocks, roles or supplier action? Start from one concrete changed operator and price every changed child and ancillary operation on the complete invoice. The result exhausts the fixed original-odd-clock union family and does not address those different mechanisms. + +## Credit + +#7357 at `b4902a36a1506ab87cbdee03c51345b179fb00a6` supplies the 180 one-edit obstructions and exact input manifests. #7315 supplies the even-idle census and projector method. #7323 supplies the odd-idle census and earlier joint sign-cancellation method. #7356 extends that separate sign-transfer model, #7144 supplies a different fixed-skeleton diagonal-gauge obstruction, and #7296 treats the exact site (1339,2324) under a canonical erased-child volume bound. #7298 supplies the directed tariff. [#7357](https://github.com/CrocSwap/integer-mult-bounds/pull/7357) · [#7315](https://github.com/CrocSwap/integer-mult-bounds/pull/7315) · [#7323](https://github.com/CrocSwap/integer-mult-bounds/pull/7323) · [#7356](https://github.com/CrocSwap/integer-mult-bounds/pull/7356) · [#7144](https://github.com/CrocSwap/integer-mult-bounds/pull/7144) · [#7296](https://github.com/CrocSwap/integer-mult-bounds/pull/7296) · [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) + +OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-type-b-simultaneous-idle-bound/SOURCES.json b/research/p104-type-b-simultaneous-idle-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-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-type-b-simultaneous-idle-bound/TASK.json b/research/p104-type-b-simultaneous-idle-bound/TASK.json new file mode 100644 index 0000000000..34f9d0f50d --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/TASK.json @@ -0,0 +1,84 @@ +{ + "actual_scope": "Any nonempty matching of up to four fixed-original-odd-clock Type B signed unions on exact #7113 and #7334. Preserve all other caller operators.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Signed Type B simultaneous idle research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A valid union matching can reduce the complete complex paid moment only if all independent stage derivatives vanish.", + "budget_minutes": 5, + "evidence": "Both stagewise engines exhaust 17 stages and 18,443 comparisons, with no exact sum equality and 60 missing-stage certificates. The nested two-edit replay excludes all 11,938 placements, with two independent direct endpoint tangents.", + "open_questions": [ + { + "blocked_by": "Every fixed-clock even site lacks an exact supporting stage set.", + "first_step": "Pin a concrete different operator and charge all changed children, setup and routing before signed support.", + "question": "Can a different paid mechanism preserve the independent body-stage responses?", + "why_it_matters": "A lawful signed change could reduce the complete binding paid moment." + } + ], + "original_card": { + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": "joint-query-controller", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Extends the exact one-edit and two-edit obstructions to the full at-most-four fixed-clock family.", + "scope_status": "changed", + "stop_rule": "Test 17 stages under a 26,075 relaxed comparison and 25-second cap. Stop when every even site lacks stage support.", + "task_id": "joint-query-controller" +} diff --git a/research/p104-type-b-simultaneous-idle-bound/VERIFICATION.md b/research/p104-type-b-simultaneous-idle-bound/VERIFICATION.md new file mode 100644 index 0000000000..36a3d6ec56 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/VERIFICATION.md @@ -0,0 +1,7 @@ +# Verification + +The direct CPython 3.12 replay took 2.10 seconds and the relocated Git-free replay with an empty inherited environment took 2.35 seconds. Both exited zero and regenerated eight byte-identical receipts. Seven corruption controls across the two scopes reject altered predecessor evidence, price or caller bytes. + +The stagewise engines agree on all 68 stage-cardinality records and 60 missing-stage certificates. The nested two-edit engines agree on every exact witness and nonzero entry count and independently transport the two highest-price endpoint tangents. There are no unresolved cases in either tested scope. + +[Exact caller and predecessor provenance](r123/PROVENANCE.json) · [Checkout-relative command](README.md) · [Path-keyed pins](LOCAL-PINS.json) diff --git a/research/p104-type-b-simultaneous-idle-bound/VERIFY.json b/research/p104-type-b-simultaneous-idle-bound/VERIFY.json new file mode 100644 index 0000000000..6691bd0e09 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Authenticate predecessor and signed caller, replay both complete prices and all exact two-edit and stagewise certificates, compare both independent engines and reject altered inputs.", + "timeout_seconds": 90 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-type-b-simultaneous-idle-bound/engines/stage_compare.py b/research/p104-type-b-simultaneous-idle-bound/engines/stage_compare.py new file mode 100644 index 0000000000..1d80db0aa7 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/engines/stage_compare.py @@ -0,0 +1,45 @@ +"""Reconcile every R124 stage/cardinality and every missing-stage certificate.""" +from argparse import ArgumentParser +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +PINS = { + "lead/RESULT.json": "01f4a0ff68b3a9428a82920a55751ccec7f5cf628cd2d9bd02bebbcaa6bbbde3", + "independent/RESULT.json": "5bf41ba41b70ee549526289d5e38a3987515dd387ef142a77d80a557a269e2a7", +} + + +def read(root, rel): + raw = (root / rel).read_bytes() + if sha256(raw).hexdigest() != PINS[rel]: + raise ValueError(f"changed dependency {rel}") + return loads(raw) + + +def main(): + parser = ArgumentParser() + parser.add_argument("--root", type=Path, default=Path(__file__).resolve().parents[1]) + args = parser.parse_args() + lead, independent = (read(args.root, rel) for rel in PINS) + for key in ("head", "caller", "q", "body", "literal_events", "comparisons", "exact_match_count", + "eliminations", "remaining_even_sites", "unvisited_stages", "timeout"): + assert lead[key] == independent[key], key + assert lead["comparisons"] == 18443 and independent["compatible_comparisons"] == 4527 + assert lead["exact_match_count"] == 0 and lead["timeout"] is None + assert lead["unvisited_stages"] == lead["remaining_even_sites"] == [] + assert len(lead["eliminations"]) == 1 and len(lead["eliminations"][0]) == 60 + for left, right in zip(lead["stages"], independent["stages"], strict=True): + assert left["stage"] == right["stage"] and left["matches"] == right["matches"] == [] + for a, b in zip(left["cardinalities"], right["cardinalities"], strict=True): + for key in ("k", "odd_subsets", "even_subsets", "comparisons", "exact_sums"): + assert a[key] == b[key], (left["stage"], key) + assert a["modular_collisions"] == b["rational_scalar_equal"] == 0 + result = dict(pins=PINS, stages=len(lead["stages"]), stage_cardinality_rows=68, + comparisons=18443, fully_mask_compatible=4527, exact_matches=0, + missing_stage_certificates=60, unvisited_stages=[]) + print(dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-type-b-simultaneous-idle-bound/engines/stage_quote.py b/research/p104-type-b-simultaneous-idle-bound/engines/stage_quote.py new file mode 100644 index 0000000000..aaa697c383 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/engines/stage_quote.py @@ -0,0 +1,103 @@ +"""Price all simultaneous fixed-clock fusions and freeze a stagewise support gate.""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from json import dumps +from math import comb +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parents[1] +PREDECESSOR = "inputs/r123_quote.py" +PREDECESSOR_SHA = "3a676f5d102c3aa02522937b85275b0fb16cfce98797c667370e85c91774e05c" + + +def matching(keys, odd, even, weights): + states = {0: (Fraction(0), [])} + for e, mask in even.items(): + following = states.copy() + for seen, (score, edges) in states.items(): + for index, o in enumerate(odd): + bit = 1 << index + if seen & bit or (o, e) not in keys: + continue + new = (score + weights[len(mask)], edges + [[o, e]]) + if seen | bit not in following or new[0] > following[seen | bit][0]: + following[seen | bit] = new + states = following + return max(states.values(), key=lambda row: row[0]) + + +def hist(rows): + return Counter({int(k): v for k, v in rows.items()}) + + +def bill(edges, even): + result = Counter() + for _, e in edges: + size = len(even[e]) + result.update({9: 8, 8 * size: 8, 8 * size + 9: -8}) + return result + + +def main(): + assert __debug__ + script = ROOT / PREDECESSOR + if sha256(script.read_bytes()).hexdigest() != PREDECESSOR_SHA: + raise ValueError("changed predecessor price engine") + previous = run_path(str(script)) + source = ROOT / "r85" + docs = previous["authenticated"](source) + stock = docs["price/PRICE.json"] + previous["inventory"](stock, docs["lead/RESULT.json"], docs["independent/RESULT.json"]) + even = {int(e): sorted(mask) for e, (_, mask) in stock["even_jobs"].items()} + odd = {int(o): sorted(mask) for o, (_, mask) in stock["odd_jobs"].items()} + keys = {(x["odd"], x["even"]) for x in stock["keys"]} + tariff = run_path(str(source / "price/inputs/pricing.py"))["cost"] + at = Fraction(stock["crossing"][1]) + target = Fraction(stock["moonshot"]) + paid, productive = hist(stock["complete_paid"]), hist(stock["complete_targets"]) + old = productive.copy() + old.subtract(paid) + assert (sum(paid.values()), sum(productive.values()), sum(r * n for r, n in old.items())) == (110519, 22461, 1424) + by_size = stock["prices_by_even_mask_size"] + optimum, edges = matching(keys, odd, even, {int(m): Fraction(row["credit"][1]) for m, row in by_size.items()}) + moon_credit, moon_edges = matching(keys, odd, even, + {int(m): Fraction(row["target_credit"][1]) for m, row in by_size.items()}) + assert len(edges) == len(moon_edges) == len(odd) == 4 + assert optimum == Fraction(stock["whole_compatible_upper"]) + assert moon_credit == Fraction(stock["moonshot_whole_compatible_upper"]) + assert tariff(bill(edges, even), at)[1] <= optimum + signed_delta = bill(edges, even) + new = old.copy() + new.update(signed_delta) + assert sum(signed_delta.values()) == 32 and sum(r * n for r, n in new.items()) == 1424 + assert tariff(new, at + Fraction(1, 10**9))[0] > 0 + stages, relaxed = [], 0 + for j in range(1, 18): + o = [clock for clock, mask in odd.items() if j not in mask] + e = [clock for clock, mask in even.items() if j in mask] + comparisons = sum(comb(len(odd), k) * comb(len(e), k) for k in range(1, 5)) + stages.append({"stage": j, "odd": sorted(o), "even": sorted(e), "relaxed_comparisons": comparisons}) + relaxed += comparisons + assert relaxed == 26075 + print(dumps({ + "head": stock["head"], "caller": stock["caller_head"], "caller_sha256": stock["caller_sha256"], + "pins": {PREDECESSOR: PREDECESSOR_SHA}, "r85_pins": previous["PINS"], + "old_crossing_upper": str(at), "fixed_target": str(target), + "whole_compatible_credit_upper": str(optimum), + "complete_old_crossing_upper": str(tariff(old, at)[1] + optimum), + "paid_count_at_upper_witness": 110487, "productive": 22461, "rank_surplus": 1424, + "paid_delta_at_upper_witness": {r: -n for r, n in signed_delta.items() if n}, + "matching_witness": edges, "fixed_target_matching": moon_edges, + "fixed_target_complete_upper": str(tariff(old, target)[1] + moon_credit), + "relaxed_comparisons": relaxed, "stages": stages, "odd_masks": odd, "even_masks": even, + "limits": {"stages": 17, "relaxed_comparisons": 26075, "seconds": 25, + "coupled_cases": 4096, "coupled_seconds": 35, + "formal_cases": 4, "formal_seconds": 35, "prototype_seconds": 90}, + "scope": "Up to four disjoint fixed-odd-clock Type B unions. Necessary stagewise projector equality; complete signed price is optimistic before any ancillary cost.", + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-type-b-simultaneous-idle-bound/engines/stage_support.py b/research/p104-type-b-simultaneous-idle-bound/engines/stage_support.py new file mode 100644 index 0000000000..c93ed6e4e7 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/engines/stage_support.py @@ -0,0 +1,170 @@ +"""Stage-local necessary support and sound elimination for up to four fusions.""" +from collections import defaultdict +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +from itertools import combinations, permutations +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "plan/PRICE.json": "8940a6b5e49e838fb6dba06b73500ee6c906f6dcc8422a04ac6d5eb7b7ecf397", + "inputs/7113-CALLER.json.gz": "7e8038559cd158f6e32ef6d1a3bf15ab6a8ecc2239af32ab1699511ac28e26d9", + "inputs/direct_impulse.py": "d04426aed9528aedc6400d384d7fd13c6531e5e3e6592a7eea4faee46c61e004", + "inputs/r123_pair_derivative.py": "ce9477aadf31c0b21fefea1ae55059793c2a28fd070c7dcc501ca9b3b7151734", +} +FILTERS = [(65521, 11), (65537, 17), (65537, 29)] + + +def unique(items): + doc = dict(items) + if len(doc) != len(items): + raise ValueError("duplicate JSON key") + return doc + + +def checked(rel): + data = (ROOT / rel).read_bytes() + if sha256(data).hexdigest() != PINS[rel]: + raise ValueError(f"changed dependency {rel}") + return data + + +def signatures(projectors): + result = {} + for clock, matrix in projectors.items(): + result[clock] = tuple( + sum(q.numerator * pow(q.denominator, -1, p) * pow(36*i+j+1, exponent, p) + for (i, j), q in matrix.items()) % p + for p, exponent in FILTERS + ) + return result + + +def sum_signature(group, signature): + return tuple(sum(signature[c][i] for c in group) % p for i, (p, _) in enumerate(FILTERS)) + + +def exact_sum(group, values): + out = defaultdict(Fraction) + for clock in group: + for key, value in values[clock].items(): + out[key] += value + return {k: v for k, v in out.items() if v} + + +def perfect(left, right, allowed): + return any(all((o, e) in allowed for o, e in zip(left, perm, strict=True)) + for perm in permutations(right)) + + +def find_local(stage, sigs, projectors, allowed, deadline): + result = {"stage": stage["stage"], "cardinalities": [], "matches": []} + for size in range(1, 5): + odds = list(combinations(stage["odd"], size)) + odds_by_signature = defaultdict(list) + for group in odds: + odds_by_signature[sum_signature(group, sigs)].append(group) + even_count = 0 + collisions = 0 + exact = 0 + for evens in combinations(stage["even"], size): + if monotonic() >= deadline: + raise TimeoutError("stage subset cap") + even_count += 1 + for odd in odds_by_signature.get(sum_signature(evens, sigs), []): + collisions += 1 + if exact_sum(odd, projectors) != exact_sum(evens, projectors): + continue + exact += 1 + if perfect(odd, evens, allowed): + result["matches"].append({"odd": odd, "even": evens}) + result["cardinalities"].append({ + "k": size, "odd_subsets": len(odds), "even_subsets": even_count, + "comparisons": len(odds) * even_count, "modular_collisions": collisions, "exact_sums": exact, + }) + return result + + +def prune(stages, even_masks): + active = set(even_masks) + steps = [] + while active: + coverage = defaultdict(set) + for entry in stages: + for match in entry["matches"]: + if set(match["even"]) <= active: + for clock in match["even"]: + coverage[clock].add(entry["stage"]) + removed = {e: min(set(even_masks[e]) - coverage[e]) for e in sorted(active) + if set(even_masks[e]) - coverage[e]} + if not removed: + break + active -= removed.keys() + steps.append(removed) + return sorted(active), steps + + +def controls(): + values = {1: {(0, 0): Fraction(1, 2)}, 2: {(0, 0): Fraction(-1, 3)}, + 3: {(0, 0): Fraction(1, 6)}, 4: {}} + assert exact_sum([1, 2], values) == exact_sum([3, 4], values) + assert sum_signature([1, 2], signatures(values)) == sum_signature([3, 4], signatures(values)) + assert perfect([1, 2], [3, 4], {(1, 4), (2, 3)}) and not perfect([1, 2], [3, 4], {(1, 3), (2, 3)}) + stages = [{"stage": 1, "matches": [{"even": [3, 4]}]}, {"stage": 2, "matches": []}] + assert prune(stages, {3: [1, 2], 4: [1]}) == ([], [{3: 2}, {4: 1}]) + return ["signed equal rational sum", "distinct odd/even matching", "cascading missing-stage elimination"] + + +def stop(*_): + raise TimeoutError("hard 25-second cap") + + +def main(): + assert __debug__ + signal(SIGALRM, stop) + alarm(25) + deadline = monotonic() + 23 + price = loads(checked("plan/PRICE.json"), object_pairs_hook=unique) + results, events, reason = [], None, None + active, steps = sorted(map(int, price["even_masks"])), [] + try: + payload = decompress(checked("inputs/7113-CALLER.json.gz")) + assert sha256(payload).hexdigest() == price["caller_sha256"] + caller = loads(payload, object_pairs_hook=unique) + checked("inputs/direct_impulse.py") + engine = run_path(str(ROOT / "inputs/direct_impulse.py")) + checked("inputs/r123_pair_derivative.py") + walker = run_path(str(ROOT / "inputs/r123_pair_derivative.py")) + odd, even = engine["literal_stock"](caller["events"], 36) + assert {str(t): v[1] for t, v in odd.items()} == price["odd_masks"] + assert {str(t): v[1] for t, v in even.items()} == price["even_masks"] + allowed = {(o, e) for o, (_, a) in odd.items() for e, (_, b) in even.items() if set(a).isdisjoint(b)} + assert len(allowed) == 180 + values, events = walker["walk"](caller, engine, [], deadline) + sigs = signatures(values) + for stage in price["stages"]: + results.append(find_local(stage, sigs, values, allowed, deadline)) + assert len(results) == 17 + active, steps = prune(results, {t: v[1] for t, v in even.items()}) + except TimeoutError as error: + reason = str(error) + finally: + alarm(0) + print(dumps({ + "head": price["head"], "caller": price["caller"], "pins": PINS, "controls": controls(), + "q": 1, "body": "unit", "literal_events": events, "filters": FILTERS, + "stages": results, "comparisons": sum(c["comparisons"] for row in results for c in row["cardinalities"]), + "exact_match_count": sum(len(row["matches"]) for row in results), + "eliminations": steps, "remaining_even_sites": active, + "unvisited_stages": [r["stage"] for r in price["stages"][len(results):]], "timeout": reason, + }, sort_keys=True, indent=2)) + return 124 if reason else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/p104-type-b-simultaneous-idle-bound/engines/stage_tangent.py b/research/p104-type-b-simultaneous-idle-bound/engines/stage_tangent.py new file mode 100644 index 0000000000..b8aac5b002 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/engines/stage_tangent.py @@ -0,0 +1,215 @@ +"""Independent exact rational derivative screen for all one- to four-union stage sets.""" +from argparse import ArgumentParser +from collections import defaultdict +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +from itertools import combinations, permutations +from json import dumps, loads +from math import comb +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PRICE = "plan/PRICE.json" +ARCHIVE = "inputs/7113-CALLER.json.gz" +ENGINE = "independent/r123_tangent.py" +PINS = { + PRICE: "8940a6b5e49e838fb6dba06b73500ee6c906f6dcc8422a04ac6d5eb7b7ecf397", + ARCHIVE: "7e8038559cd158f6e32ef6d1a3bf15ab6a8ecc2239af32ab1699511ac28e26d9", + ENGINE: "8ad672bd808b6b8c30306fa2b125b19be5e8c19215425b79dc592e552a96b169", +} +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PAYLOAD = "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +LIMIT, SECONDS = 26075, 25 + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate metadata key") + return result + + +def pinned(root, relative): + raw = (root / relative).read_bytes() + if sha256(raw).hexdigest() != PINS[relative]: + raise ValueError(f"changed dependency {relative}") + return raw + + +def weight(i, j): + return (-1) ** (i + j) * (i + 1) ** 41 * (j + 2) ** 37 + + +def project(matrix): + return sum((value * weight(i, j) for (i, j), value in matrix.items()), Q(0)) + + +def signed_matrix(terms, odd, even): + result = defaultdict(Q) + for sign, clocks in [(1, odd), (-1, even)]: + for clock in clocks: + for index, value in terms[clock].items(): + result[index] += sign * value + return {index: value for index, value in result.items() if value} + + +def match(left, right, allowed): + return next((list(zip(left, permutation, strict=True)) + for permutation in permutations(right) + if all((o, e) in allowed for o, e in zip(left, permutation, strict=True))), None) + + +def controls(engine): + same = {(0, 0): Q(1, 2)} + unequal = {(0, 1): project(same) / weight(0, 1)} + assert project(same) == project(unequal) + terms = {1: same, 2: unequal, 3: same, 4: unequal} + assert signed_matrix(terms, (1,), (2,)) + assert not signed_matrix(terms, (1, 2), (3, 4)) + assert match((1, 2), (3, 4), {(1, 4), (2, 3)}) == [(1, 4), (2, 3)] + assert match((1, 2), (3, 4), {(1, 3), (2, 3)}) is None + return engine["controls"]() + [ + "equal rational fingerprint and unequal exact matrices", + "equal full matrix sum with nonzero summands", + "distinct compatible bijection and reused donor rejection", + ] + + +def check_stage(stage, odd, even, terms, signatures, allowed, state, deadline): + row = dict(stage=stage, odd=odd, even=even, cardinalities=[], matches=[]) + for size in range(1, 5): + left = [(group, sum(signatures[o] for o in group)) for group in combinations(odd, size)] + right = [(group, sum(signatures[e] for e in group)) for group in combinations(even, size)] + counts = dict(k=size, odd_subsets=len(left), even_subsets=len(right), comparisons=0, + compatible=0, rational_scalar_equal=0, exact_sums=0) + for odd_clocks, a in left: + for even_clocks, b in right: + if state["comparisons"] >= LIMIT or monotonic() >= deadline: + raise TimeoutError("stage comparison cap") + state["comparisons"] += 1 + counts["comparisons"] += 1 + pairing = match(odd_clocks, even_clocks, allowed) + counts["compatible"] += pairing is not None + if a != b: + continue + counts["rational_scalar_equal"] += 1 + if signed_matrix(terms, odd_clocks, even_clocks): + continue + counts["exact_sums"] += 1 + if pairing is not None: + row["matches"].append(dict(odd=odd_clocks, even=even_clocks)) + assert counts["comparisons"] == len(left) * len(right) + row["cardinalities"].append(counts) + return row + + +def eliminate(stages, masks): + active = set(masks) + receipts = [] + while active: + admitted = defaultdict(set) + for row in stages: + for item in row["matches"]: + if set(item["even"]).issubset(active): + for e in item["even"]: + admitted[e].add(row["stage"]) + gone = {e: min(set(masks[e]) - admitted[e]) for e in sorted(active) + if not set(masks[e]).issubset(admitted[e])} + if not gone: + break + receipts.append(gone) + active.difference_update(gone) + return receipts, sorted(active) + + +def literal(root, price, engine, state, deadline): + raw = decompress(pinned(root, ARCHIVE)) + if sha256(raw).hexdigest() != PAYLOAD: + raise ValueError("changed caller payload") + caller = loads(raw, object_pairs_hook=unique) + b = caller["types"]["B"] + n, offset = b["roles"], b["offset"] + assert (caller["stages"], n, offset, len(b["ports"])) == (17, 36, 36, 8) + steps, odd, even = engine["unit_ops"](caller["events"], n, offset) + state["literal_events"] = len(steps) + assert {str(t): list(m) for t, (_, m) in odd.items()} == price["odd_masks"] + assert {str(t): list(m) for t, (_, m) in even.items()} == price["even_masks"] + allowed = {(o, e) for o, (_, left) in odd.items() for e, (_, right) in even.items() + if set(left).isdisjoint(right)} + assert len(allowed) == 180 + roles = {t: row[0] for t, row in (odd | even).items()} + terms = engine["impulses"](steps, roles, n, deadline) + signatures = {t: project(matrix) for t, matrix in terms.items()} + state["projector_fingerprints"] = {t: str(v) for t, v in signatures.items()} + + # Compare the exact full direct derivative to the independent impulses at + # two largest matching-witness stages before relying on fingerprints. + samples = [] + for stage in (2, 9): + pairs = [(o, e) for o, e in price["matching_witness"] if stage in even[e][1]] + inject = {t: (roles[t], sign) for o, e in pairs for t, sign in [(o, 1), (e, -1)]} + assert len(pairs) == 2 and len(inject) == 4 + endpoint, full = engine["tangent"](steps, inject, n) + odd_sites, even_sites = zip(*pairs, strict=True) + delta = signed_matrix(terms, odd_sites, even_sites) + assert endpoint == engine["identity"](n) and full == delta + assert project(delta) == sum(signatures[o] - signatures[e] for o, e in pairs) + i, j = min(delta) + samples.append(dict(stage=stage, fusions=pairs, witness=[i + offset, j + offset, str(delta[i, j])])) + state["full_tangent_controls"] = samples + for stage in range(1, 18): + left = sorted(o for o, (_, mask) in odd.items() if stage not in mask) + right = sorted(e for e, (_, mask) in even.items() if stage in mask) + previous = price["stages"][stage - 1] + assert (stage, left, right) == (previous["stage"], previous["odd"], previous["even"]) + assert sum(comb(len(odd), k) * comb(len(right), k) for k in range(1, 5)) == previous["relaxed_comparisons"] + state["stages"].append(check_stage(stage, left, right, terms, signatures, allowed, state, deadline)) + state["eliminations"], state["remaining_even_sites"] = eliminate( + state["stages"], {t: mask for t, (_, mask) in even.items()}) + state["compatible_comparisons"] = sum(c["compatible"] for row in state["stages"] for c in row["cardinalities"]) + state["exact_match_count"] = sum(len(row["matches"]) for row in state["stages"]) + + +def main(): + parser = ArgumentParser() + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + assert __debug__ + price = loads(pinned(args.root, PRICE), object_pairs_hook=unique) + assert (price["head"], price["caller"], price["caller_sha256"]) == (HEAD, CALLER, PAYLOAD) + assert price["limits"]["relaxed_comparisons"] == LIMIT and price["limits"]["seconds"] == SECONDS + pinned(args.root, ENGINE) + engine = run_path(str(args.root / ENGINE)) + tests = controls(engine) + if args.controls_only: + print(dumps(dict(controls=tests), indent=2, sort_keys=True)) + return 0 + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + state = dict(head=HEAD, caller=CALLER, caller_sha256=PAYLOAD, q=1, body="unit", + cap_cases=LIMIT, cap_seconds=SECONDS, pins=PINS, comparisons=0, + stages=[], timeout=None, controls=tests) + signal(SIGALRM, stop) + alarm(SECONDS) + deadline = monotonic() + 23 + try: + literal(args.root, price, engine, state, deadline) + except TimeoutError as problem: + state["timeout"] = str(problem) + finally: + alarm(0) + state["unvisited_stages"] = list(range(len(state["stages"]) + 1, 18)) + print(dumps(state, indent=2, sort_keys=True)) + return 124 if state["timeout"] else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/LOCAL-PINS.json b/research/p104-type-b-simultaneous-idle-bound/r123/LOCAL-PINS.json new file mode 100644 index 0000000000..06f93585f7 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/LOCAL-PINS.json @@ -0,0 +1,22 @@ +{ + "PROVENANCE.json": "048d70849ec7a6f93a060cfc5a4cb9aaa2609cf6ab57f6085c13d16978417cdc", + "engines/compare.py": "91ce91a5e99bfc629ffc400487b6331c5be86459397a293bf2f90753859d3cef", + "engines/pair_derivative.py": "ce9477aadf31c0b21fefea1ae55059793c2a28fd070c7dcc501ca9b3b7151734", + "engines/quote.py": "3a676f5d102c3aa02522937b85275b0fb16cfce98797c667370e85c91774e05c", + "engines/tangent.py": "8ad672bd808b6b8c30306fa2b125b19be5e8c19215425b79dc592e552a96b169", + "inputs/7113-CALLER.json.gz": "7e8038559cd158f6e32ef6d1a3bf15ab6a8ecc2239af32ab1699511ac28e26d9", + "inputs/PR7357-SHA256.json": "877af2f9d65e0457e74f843a6ede78571ffdf9d57e7565d383c3c4d6be91d54c", + "inputs/direct_impulse.py": "d04426aed9528aedc6400d384d7fd13c6531e5e3e6592a7eea4faee46c61e004", + "r85/independent/RESULT.json.gz": "62888bf58026aebb87019c1e76eeec885317f4da6e703c7fe8a2f90a7a019c49", + "r85/independent/SHA256": "cfcac30934a139cf120885ee210c0923b60f387ecb880f18ea92ff0d33a159ba", + "r85/lead/RESULT.json.gz": "30c782c2faab1387d9394f6e95874507a34a151596e45c758d979cec11e21f3d", + "r85/price/PRICE.json.gz": "67ae145bb973e0e9dd759bd5b0433ca64c2483100a5c7d00a236916992567eac", + "r85/price/SHA256": "37e11ffc1979e090deb4e046e7b770339a3d9e1898fff8b5a04f4a70da70e383", + "r85/price/inputs/7334-ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "r85/price/inputs/7334-READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "r85/price/inputs/derivative_check.py": "348c8b2de72f1f112cb1337eca9d29ca96c85a7ad903beecafb1a2a1221f408e", + "r85/price/inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "receipts/AGREEMENT.json": "057201100051f25a72b22f0cbe49a8d20e08549043a4787faf25af6c5c8ee0a9", + "receipts/SHA256.json": "06c464b960dc721b990cec4968edb35e5ba4a1ba73884a1c249422d2d9e1afed", + "replay.py": "a038125efdc5fb0e2bf86bd9081b387755694e96e2757513f221a94e24348007" +} diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/PROOF.md b/research/p104-type-b-simultaneous-idle-bound/r123/PROOF.md new file mode 100644 index 0000000000..9657488da5 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/PROOF.md @@ -0,0 +1,22 @@ +# Exact first derivative of two signed Type B idle unions + +The signed #7113 Type B caller has 36 normalized roles at offset 36, eight ports and 17 independent body stages. In one edit a singleton signed odd idle at clock o gains the body mask M of a removed even idle at clock e. The phase sign and odd role and clock stay fixed. The old odd body mask and M are disjoint. A two-edit proposal uses two distinct odd clocks and two distinct even clocks, with all other operators fixed. + +At q=+1 and all body variables one, the changed idle operators are identities in both words. The original unit endpoint is the identity on all 36 columns. Let F_c be the prefix up to clock c, S_c the suffix after c and E_c the coordinate projector at that idle's role. An added derivative at c contributes S_c E_c F_c to the endpoint. Since the old endpoint and the unit idle are identities, S_c = F_c⁻¹. For one fusion, each stage j in M contributes D(o,e) = S_o E_o F_o − S_e E_e F_e. For j outside M the new and old terms cancel. All common derivatives also cancel because both words agree at specialization on every event. + +For masks M₁ and M₂, the derivative in stage j is the sum of the two defects whose masks contain j. A stage in their symmetric difference isolates one original defect. The exact #7357 rational receipts certify every one-edit defect nonzero and match the corresponding modular witnesses. The exact literal census contains 4 odd sites, 60 even sites, 180 admissible single edits and 11,938 distinct two-edit placements. This argument exhausts the 11,728 placements with unequal masks. + +For the 210 equal-mask placements, the lead engine transports projectors by exact prefix and inverse conjugation. The independent engine computes the exact prefix covector and suffix impulse without maintaining a prefix inverse. Both compare the two-edit sum. All 210 sums are nonzero, with agreement on the exact first witness and nonzero entry count. Direct tangent transport of all 36 columns independently checks both highest-priced keys before the whole-group impulse comparisons. + +| Odd-to-even assignments | Common stages | First global witness | Nonzero entries | +|---|---|---|---:| +| (1339,2324), (1340,2337) | 9 through 16 | (36,36), +16 | 18 | +| (1339,2337), (1340,2324) | 9 through 16 | (36,36), +16 | 18 | + +The controls include two nonzero defects that cancel exactly after swaps, and a signed mutation that spoils that cancellation. Exact nonzero derivatives at a single valid character specialization disprove arbitrary-input endpoint equality. No q=−1 or nonunit-body formal continuation, physical candidate or κ gain was needed. The result covers precisely the two fixed edits with disjoint clocks and unchanged remaining caller. + +## Complete price + +For two equal removed masks of size m, the net paid change across eight ports is `P9−16, P_(8m)−16, P_(8m+9)+16`. The price uses all 17 native copies. Paid positions would fall from 110,519 to 110,503. The 22,461 productive positions, rank surplus 1,424 and zero empty-root credit stay fixed. The largest directed complete margin at the old crossing upper is about 1.570089088072506 raw and remains 1.5697019379633825 at the higher probe. An additional eight-port rank-one charge would exceed it. At fixed target κ = 0.0040075385047236 the complete margin upper is about −138.04366119900828. No ancillary setup, route, restoration, ownership, precision or tape credit is granted to a construction. + +All five inherited framework premises remain. A different operator or supplier would require a new fully charged signed construction and complete independent replay. diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/PROVENANCE.json b/research/p104-type-b-simultaneous-idle-bound/r123/PROVENANCE.json new file mode 100644 index 0000000000..676277c6d1 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/PROVENANCE.json @@ -0,0 +1,64 @@ +{ + "derived_gzip": { + "r85/independent/RESULT.json.gz": "INDEPENDENT.json", + "r85/lead/RESULT.json.gz": "LEAD.json", + "r85/price/PRICE.json.gz": "PRICE.json" + }, + "derived_gzip_manifest": "inputs/PR7357-SHA256.json", + "files": { + "inputs/7113-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 + }, + "inputs/PR7357-SHA256.json": { + "commit": "b4902a36a1506ab87cbdee03c51345b179fb00a6", + "git_blob": "da232d65c09203969358334906af2700a881a170", + "path": "research/p104-type-b-odd-even-idle-bound/receipts/SHA256.json", + "sha256": "877af2f9d65e0457e74f843a6ede78571ffdf9d57e7565d383c3c4d6be91d54c", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/b4902a36a1506ab87cbdee03c51345b179fb00a6/research/p104-type-b-odd-even-idle-bound/receipts/SHA256.json" + }, + "inputs/direct_impulse.py": { + "commit": "b4902a36a1506ab87cbdee03c51345b179fb00a6", + "git_blob": "14b5e8bb185788a111aab6a47f4b0728ce0820c9", + "path": "research/p104-type-b-odd-even-idle-bound/independent/direct_impulse.py", + "sha256": "d04426aed9528aedc6400d384d7fd13c6531e5e3e6592a7eea4faee46c61e004", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/b4902a36a1506ab87cbdee03c51345b179fb00a6/research/p104-type-b-odd-even-idle-bound/independent/direct_impulse.py" + }, + "r85/price/inputs/7334-ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "r85/price/inputs/7334-READBACK.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "625b508eead24b4428253bd257620b7e775800c1", + "path": "research/p104-compensated-fusion-readout-bound/price/READBACK.json", + "sha256": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/price/READBACK.json", + "uncompress": false + }, + "r85/price/inputs/derivative_check.py": { + "commit": "b4902a36a1506ab87cbdee03c51345b179fb00a6", + "git_blob": "ce5cdf377926b14bf77245083e51701a34fd683f", + "path": "research/p104-type-b-odd-even-idle-bound/price/inputs/derivative_check.py", + "sha256": "348c8b2de72f1f112cb1337eca9d29ca96c85a7ad903beecafb1a2a1221f408e", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/b4902a36a1506ab87cbdee03c51345b179fb00a6/research/p104-type-b-odd-even-idle-bound/price/inputs/derivative_check.py" + }, + "r85/price/inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/engines/compare.py b/research/p104-type-b-simultaneous-idle-bound/r123/engines/compare.py new file mode 100644 index 0000000000..320c6ee294 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/engines/compare.py @@ -0,0 +1,40 @@ +"""Compare all exact R123 two-edit derivative witnesses.""" +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "lead/RESULT.json":"4803b929abd8e1d0e9600bb4713e1b5111c61425571492c9e0488f59c2678a6d", + "independent/RESULT.json":"a44744be08ffd75f02ffbd9c96799f8a995a111b04a136f71f4c4b171a17d5b8", +} + + +def checked(name): + raw=(ROOT/name).read_bytes() + if sha256(raw).hexdigest()!=PINS[name]: + raise ValueError("changed dependency "+name) + return loads(raw) + + +def main(): + assert __debug__ + lead,independent=map(checked,PINS) + fields=("head","caller","q","body","cap_cases","cap_seconds","counts","unvisited","timeout") + assert all(lead[k]==independent[k] for k in fields) + assert lead["events"]==independent["progress"]["caller_events"]==4783 + assert lead["pins"]["plan/PRICE.json"]==independent["pins"]["plan/PRICE.json"] + assert lead["pins"]["inputs/7113-CALLER.json.gz"]==independent["pins"]["inputs/7113-CALLER.json.gz"] + assert len(lead["results"])==len(independent["results"])==210 + fields=("fusions","even_mask","witness","nonzero_coordinates","status") + for a,b in zip(lead["results"],independent["results"],strict=True): + assert all(a[k]==b[k] for k in fields) + priority=independent["results"][:2] + assert all(r["direct_tangent"] and r["witness"]==[36,36,"16"] for r in priority) + print(dumps(dict(pins=PINS,exact_witness_agreement=210,exact_nonzero_count_agreement=210, + direct_endpoint_tangent_priority=priority,unequal_mask_excluded=11728,unresolved=0), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/engines/pair_derivative.py b/research/p104-type-b-simultaneous-idle-bound/r123/engines/pair_derivative.py new file mode 100644 index 0000000000..0cec075217 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/engines/pair_derivative.py @@ -0,0 +1,158 @@ +"""Exact first-derivative necessity for two fixed Type B idle fusions.""" +from collections import Counter +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from sys import argv +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "plan/PRICE.json": "3633b57cc096fe511daac7c23ead578f839096df8b6ef62651844c2e62a3f2a6", + "inputs/7113-CALLER.json.gz": "7e8038559cd158f6e32ef6d1a3bf15ab6a8ecc2239af32ab1699511ac28e26d9", + "inputs/direct_impulse.py": "d04426aed9528aedc6400d384d7fd13c6531e5e3e6592a7eea4faee46c61e004", +} + + +def unique(items): + result = dict(items) + if len(result) != len(items): + raise ValueError("duplicate JSON key") + return result + + +def checked(rel): + data = (ROOT / rel).read_bytes() + if sha256(data).hexdigest() != PINS[rel]: + raise ValueError(f"changed dependency {rel}") + return data + + +def identity(n): + return [[Fraction(i == j) for j in range(n)] for i in range(n)] + + +def update(gate, rows, inverse_columns): + op, d, s, value = gate + if op == "add": + rows[d] = [x + value * y for x, y in zip(rows[d], rows[s])] + inverse_columns[s] = [x - value * y for x, y in zip(inverse_columns[s], inverse_columns[d])] + elif op == "scale": + assert value + rows[d] = [value * x for x in rows[d]] + inverse_columns[d] = [x / value for x in inverse_columns[d]] + else: + assert op == "swap" + rows[d], rows[s] = rows[s], rows[d] + inverse_columns[d], inverse_columns[s] = inverse_columns[s], inverse_columns[d] + + +def projector(column, row): + return {(i, j): x * y for i, x in enumerate(column) if x for j, y in enumerate(row) if y} + + +def difference(projectors, pairs): + total = {} + for odd, even in pairs: + for site, sign in ((odd, 1), (even, -1)): + for key, value in projectors[site].items(): + total[key] = total.get(key, 0) + sign * value + return {k: v for k, v in total.items() if v} + + +def controls(): + ident = identity(3) + rows, columns = identity(3), identity(3) + for op in [("add", 0, 1, Fraction(-3, 2)), ("swap", 1, 2, Fraction(1)), + ("scale", 0, 0, Fraction(2, 3))]: + update(op, rows, columns) + assert [[sum(a * b for a, b in zip(row, col)) for col in columns] for row in rows] == ident + p, q = projector(ident[0], ident[0]), projector(ident[1], ident[1]) + values = {1: p, 2: q, 3: q, 4: p} + assert difference(values, [(1, 2)]) and not difference(values, [(1, 2), (3, 4)]) + assert set([1, 2]) ^ set([2, 3]) == {1, 3} + return ["exact inverse conjugation", "two nonzero differences that cancel", "unequal mask variable"] + + +def walk(caller, engine, requested, deadline): + data = caller["types"]["B"] + n, offset = data["roles"], data["offset"] + assert (caller["stages"], n, offset, len(data["ports"])) == (17, 36, 36, 8) + events = caller["events"] + odd, even = engine["literal_stock"](events, offset) + assert len(odd) == 4 and len(even) == 60 + roles = odd | even + for item in requested: + masks = [even[e][1] for _, e in item["fusions"]] + assert masks[0] == masks[1] == item["even_mask"] + assert len({c for pair in item["fusions"] for c in pair}) == 4 + assert all(set(odd[o][1]).isdisjoint(even[e][1]) for o, e in item["fusions"]) + rows, columns = identity(n), identity(n) + values = {} + q = Fraction(1) + for t, event in enumerate(events): + if t % 128 == 0 and monotonic() >= deadline: + raise TimeoutError("literal projector walk cap") + if t in roles: + role = roles[t][0] + values[t] = projector(columns[role], rows[role]) + for gate in engine["gates"](event, offset, q): + update(gate, rows, columns) + assert rows == columns == identity(n) and len(values) == 64 + return values, len(events) + + +def stop(*_): + raise TimeoutError("hard 25-second cap") + + +def main(): + assert __debug__ + price = loads(checked("plan/PRICE.json"), object_pairs_hook=unique) + keys = price["equal_mask_keys"] + assert len(keys) == 210 and len(keys[0]["even_mask"]) == len(keys[1]["even_mask"]) == 8 + tests = controls() + checked("inputs/direct_impulse.py") + if argv[1:] == ["--controls-only"]: + print(dumps({"controls": tests, "cases": len(keys), "priority": keys[:2]}, sort_keys=True)) + return 0 + assert not argv[1:] + signal(SIGALRM, stop) + alarm(25) + deadline = monotonic() + 23 + results, events, reason = [], None, None + try: + payload = decompress(checked("inputs/7113-CALLER.json.gz")) + assert sha256(payload).hexdigest() == price["caller_sha256"] + caller = loads(payload, object_pairs_hook=unique) + engine = run_path(str(ROOT / "inputs/direct_impulse.py")) + projections, events = walk(caller, engine, keys, deadline) + for item in keys: + if monotonic() >= deadline: + raise TimeoutError("paired matrix cap") + values = difference(projections, item["fusions"]) + witness = None + if values: + row, column = min(values) + witness = [row + 36, column + 36, str(values[row, column])] + results.append(item | {"status": "exact derivative exclusion" if witness else "first derivative zero", + "witness": witness, "nonzero_coordinates": len(values)}) + except TimeoutError as error: + reason = str(error) + finally: + alarm(0) + print(dumps({ + "pins": PINS, "head": price["head"], "caller": price["caller"], "q": 1, "body": "unit", + "controls": tests, "events": events, "cap_cases": 210, "cap_seconds": 25, + "counts": Counter(r["status"] for r in results), "results": results, + "unvisited": keys[len(results):], "timeout": reason, + }, sort_keys=True, indent=2)) + return 124 if reason else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/engines/quote.py b/research/p104-type-b-simultaneous-idle-bound/r123/engines/quote.py new file mode 100644 index 0000000000..3c18e8d37e --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/engines/quote.py @@ -0,0 +1,200 @@ +"""Freeze two-fusion keys and the complete directed price from sealed metadata.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations +from json import dumps, loads +from pathlib import Path +from runpy import run_path + +PINS = { + "price/SHA256": "37e11ffc1979e090deb4e046e7b770339a3d9e1898fff8b5a04f4a70da70e383", + "independent/SHA256": "cfcac30934a139cf120885ee210c0923b60f387ecb880f18ea92ff0d33a159ba", + "price/PRICE.json": "33aad506112912ddf0721a2b007d9194eaa02e5792aceda2f9774f8838511262", + "lead/RESULT.json": "bf0cbae853422e85788449b40ddc2fa807b042d8a357a56a7c7654dda51331e4", + "independent/RESULT.json": "afec20386a8fbdc70d1b96998adbe18edace42a3e14a015e0eab5c09fc311617", + "price/inputs/7334-ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "price/inputs/7334-READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "price/inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "price/inputs/derivative_check.py": "348c8b2de72f1f112cb1337eca9d29ca96c85a7ad903beecafb1a2a1221f408e", +} +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +CALLER_SHA = "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +TARGET = Fraction("0.0040075385047236") + + +def unique(pairs): + obj = dict(pairs) + if len(obj) != len(pairs): + raise ValueError("duplicate metadata key") + return obj + + +def authenticated(root): + docs = {} + for name, expected in PINS.items(): + raw = (root / name).read_bytes() + if sha256(raw).hexdigest() != expected: + raise ValueError(f"changed dependency {name}") + if name.endswith(".json"): + docs[name] = loads(raw, object_pairs_hook=unique) + for name, members in [ + ("price/SHA256", ("price/PRICE.json", "price/inputs/7334-ADMITTED.json", + "price/inputs/7334-READBACK.json", "price/inputs/pricing.py", + "price/inputs/derivative_check.py")), + ("independent/SHA256", ("independent/RESULT.json",)), + ]: + folder = str(Path(name).parent) + "/" + entries = {} + for line in (root / name).read_text().splitlines(): + digest, relative = line.split(maxsplit=1) + if relative in entries: + raise ValueError(f"duplicate manifest path {folder + relative}") + entries[relative] = digest + for member in members: + assert entries[member.removeprefix(folder)] == PINS[member], member + return docs + + +def bounds(approximation): + return [str(endpoint) for endpoint in approximation] + + +def inventory(stock, lead, independent): + odd = {int(clock): tuple(mask) for clock, (_, mask) in stock["odd_jobs"].items()} + even = {int(clock): tuple(sorted(mask)) for clock, (_, mask) in stock["even_jobs"].items()} + assert set(odd) == {1339, 1340, 2970, 2971} + keys = {(row["odd"], row["even"]) for row in stock["keys"]} + assert keys == {(o, e) for o in odd for e in even if set(odd[o]).isdisjoint(even[e])} + assert len(keys) == len(stock["keys"]) == 180 and len(even) == 60 + assert independent["q"] == lead["q"] == 1 + assert independent["body"] == "unit" and lead["body"] == "all one" + assert lead["price_sha256"] == independent["price_sha256"] == PINS["price/PRICE.json"] + assert lead["caller_sha256"] == independent["caller_sha256"] == CALLER_SHA + assert lead["head"] == independent["head"] == HEAD + assert len(independent["outcomes"]) == len(lead["decisions"]) == len(keys) + assert not independent["unvisited"] and not lead["unvisited"] + assert {tuple(row["key"]) for row in independent["outcomes"]} == keys + primary = {(row["key"]["odd"], row["key"]["even"]): row for row in lead["decisions"]} + assert set(primary) == keys + modulus = lead["modulus"] + for row in independent["outcomes"]: + field, coordinate, rational = row["exact_off_axis"] + residue = Fraction(rational) + counterpart = primary[tuple(row["key"])] + assert row["status"] == counterpart["decision"] == "excluded" + assert field == "column" and residue + assert counterpart["outside_column"] == [ + coordinate - 36, residue.numerator * pow(residue.denominator, -1, modulus) % modulus, + ] + eligible = [] + distinct = 0 + for left, right in combinations(sorted(keys), 2): + if left[0] == right[0] or left[1] == right[1]: + continue + distinct += 1 + if even[left[1]] == even[right[1]]: + eligible.append({"fusions": [left, right], "even_mask": even[left[1]]}) + eligible.sort(key=lambda row: (-len(row["even_mask"]), row["fusions"])) + by_size = Counter(len(row["even_mask"]) for row in eligible) + assert distinct == 11938 and len(eligible) == 210 + assert by_size == {1: 184, 2: 4, 3: 4, 4: 4, 5: 4, 6: 4, 7: 4, 8: 2} + return distinct, eligible, by_size + + +def signed(hist): + return Counter({int(rank): multiplicity for rank, multiplicity in hist.items()}) + + +def main(): + cli = ArgumentParser() + cli.add_argument("--r85", type=Path, required=True) + options = cli.parse_args() + root = options.r85.resolve() + doc = authenticated(root) + stock, lead, exact = (doc[name] for name in ("price/PRICE.json", "lead/RESULT.json", + "independent/RESULT.json")) + admit = doc["price/inputs/7334-ADMITTED.json"] + complete = doc["price/inputs/7334-READBACK.json"] + assert admit["head"] == stock["head"] == complete["head"] == HEAD and admit["exit"] == 0 + assert admit["caller"] == stock["caller_head"] == complete["caller_head"] == CALLER + assert admit["caller_sha256"] == stock["caller_sha256"] == CALLER_SHA + assert stock["copies"] == complete["copies"] == 17 and stock["ports"] == 8 + paid, targets = signed(complete["paid"]), signed(complete["targets"]) + assert paid == signed(stock["complete_paid"]) and targets == signed(stock["complete_targets"]) + assert sum(paid.values()) == 110519 and sum(targets.values()) == 22461 + net = targets.copy() + net.subtract(paid) + assert sum(rank * count for rank, count in net.items()) == 1424 + assert complete["empty_root_credits"] == 0 + lo, hi = map(Fraction, admit["crossing"]) + assert (lo, hi) == tuple(map(Fraction, stock["crossing"])) + assert (lo, hi) == tuple(map(Fraction, complete["new_raw_interval"])) + bit = Fraction(complete["bit_premise"]) + assert bit == Fraction(stock["retained_BIT"]) + probe = hi + Fraction(1, 10**9) + distinct, keys, by_size = inventory(stock, lead, exact) + tariff = run_path(str(root / "price/inputs/pricing.py")) + cost = tariff["cost"] + derivative = run_path(str(root / "price/inputs/derivative_check.py"))["derivative"] + prices = {} + for size, count in sorted(by_size.items()): + # Two call deletions per port: each old odd + even pair becomes one union. + credit_hist = Counter({9: 16, 8 * size: 16, 8 * size + 9: -16}) + assert sum(credit_hist.values()) == 16 + assert sum(r * n for r, n in credit_hist.items()) == 0 + changed = net.copy() + changed.update(credit_hist) + assert sum(paid.values()) - sum(credit_hist.values()) == 110503 + credit, target_credit = cost(credit_hist, hi), cost(credit_hist, TARGET) + old_quote, new_quote = cost(changed, hi), cost(changed, probe) + assert 0 < credit[0] <= credit[1] and 0 < new_quote[0] <= new_quote[1] + assert credit[1] == 2 * Fraction(stock["prices_by_even_mask_size"][str(size)]["credit"][1]) + assert target_credit[1] == 2 * Fraction(stock["prices_by_even_mask_size"][str(size)]["target_credit"][1]) + one, two = changed.copy(), changed.copy() + one[1] -= 1 + two[1] -= 2 + debit_bounds = cost(two, lo) + debit_slope = derivative(two, lo, bit, tariff) + assert debit_bounds[1] < 0 and debit_slope[1] < 0 + prices[size] = { + "keys": count, + "paid_delta": {r: -n for r, n in credit_hist.items()}, + "gross_credit_at_old_upper": bounds(credit), + "gross_credit_at_fixed_target": bounds(target_credit), + "complete_margin_at_old_upper": bounds(old_quote), + "complete_margin_at_probe": bounds(new_quote), + "complete_margin_with_one_raw_rank_one_debit_at_old_upper": bounds(cost(one, hi)), + "complete_margin_with_two_raw_rank_one_debits_at_old_lower": bounds(debit_bounds), + "complete_derivative_with_two_debits_through_retained_BIT": bounds(debit_slope), + "complete_margin_at_fixed_target": bounds(cost(changed, TARGET)), + } + assert all(Fraction(prices[m]["gross_credit_at_old_upper"][1]) < + Fraction(prices[m+1]["gross_credit_at_old_upper"][1]) for m in range(1, 8)) + assert all(Fraction(prices[m]["gross_credit_at_fixed_target"][1]) < + Fraction(prices[m+1]["gross_credit_at_fixed_target"][1]) for m in range(1, 8)) + largest = prices[8] + assert Fraction(largest["complete_margin_at_fixed_target"][1]) < 0 + assert Fraction(largest["complete_margin_with_one_raw_rank_one_debit_at_old_upper"][0]) > 0 + print(dumps({ + "head": HEAD, "caller": CALLER, "caller_sha256": CALLER_SHA, + "R85_path_pins": PINS, "scope": "Two disjoint fixed-odd-clock unions; no other edits", + "old_crossing": bounds((lo, hi)), "price_probe": str(probe), "fixed_target": str(TARGET), + "retained_BIT": str(bit), "complete_native_copies": 17, "Type_B_ports": 8, + "old_complete_paid": paid, "complete_productive": targets, "new_paid_positions": 110503, + "productive_fields": 22461, "rank_surplus": 1424, "empty_root_credit": 0, + "all_disjoint_pair_placements": distinct, "unequal_mask_exclusions": distinct - len(keys), + "equal_mask_keys": keys, "prices_by_even_mask_size": prices, + "max_gross_at_old_upper": largest["gross_credit_at_old_upper"][1], + "max_gross_at_fixed_target": largest["gross_credit_at_fixed_target"][1], + "max_complete_margin_at_fixed_target": largest["complete_margin_at_fixed_target"][1], + "first_gate": {"keys": 210, "runner_seconds": 25}, + "formal_gate": {"keys": 4, "runner_seconds": 35}, + "literal_word_or_caller_decoded": False, + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/engines/tangent.py b/research/p104-type-b-simultaneous-idle-bound/r123/engines/tangent.py new file mode 100644 index 0000000000..6c80a6c6d6 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/engines/tangent.py @@ -0,0 +1,263 @@ +"""Direct endpoint tangents and independent prefix/suffix impulses for R123.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +from itertools import combinations +from json import dumps,loads +from pathlib import Path +from signal import SIGALRM,alarm,signal +from time import monotonic + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "plan/PRICE.json":"3633b57cc096fe511daac7c23ead578f839096df8b6ef62651844c2e62a3f2a6", + "inputs/7113-CALLER.json.gz":"7e8038559cd158f6e32ef6d1a3bf15ab6a8ecc2239af32ab1699511ac28e26d9", +} +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER="07a76c5e2738882c0cb322278e56f6cae3c9885d" +CALLER_PAYLOAD="255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +CAP,SECONDS=210,25 + + +def unique(pairs): + result=dict(pairs) + if len(result)!=len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def checked(root,name): + raw=(root/name).read_bytes() + if sha256(raw).hexdigest()!=PINS[name]: + raise ValueError("changed dependency "+name) + return raw + + +def unit_ops(events,n,offset): + """Decode the signed caller only at q=+1 and body variables all one.""" + rows,odd,even=[],{},{} + hosts=0 + for t,event in enumerate(events): + ty,tag,*tail=event + if ty=="J": + assert type(tag) is int and tag==hosts+1 + hosts+=1 + u,v,left,right=tail[1] + u,v=u-offset,v-offset + assert 0<=u=deadline: + raise TimeoutError("prefix impulse cap") + if t in roles: + assert not ops + prefix[t]=rows[roles[t]] + for op in ops: + update(rows,op) + for t in range(len(steps)-1,-1,-1): + if t%128==0 and monotonic()>=deadline: + raise TimeoutError("suffix impulse cap") + if t in roles: + suffix[t]=columns[roles[t]] + for op in reversed(steps[t]): + update(columns,op,True) + assert rows==columns==identity(n) + return {t:{(i,j):u*v for i,u in suffix[t].items() for j,v in prefix[t].items()} for t in roles} + + +def exact_delta(terms,placements,roles): + inject={t:(roles[t],sign) for o,e in placements for t,sign in ((o,1),(e,-1))} + assert len(inject)==2*len(placements) + out={} + for t,(_,sign) in inject.items(): + out=axpy(out,terms[t],sign) + return out,inject + + +def controls(): + steps=[(),(),(("SWAP",0,1,Q(1)),),(),(),(("SWAP",0,1,Q(1)),)] + roles={0:0,1:1,3:0,4:1} + terms=impulses(steps,roles,2,float("inf")) + first,_=exact_delta(terms,[(0,1)],roles) + other,_=exact_delta(terms,[(3,4)],roles) + total,inject=exact_delta(terms,[(0,1),(3,4)],roles) + assert first and other and not total + assert tangent(steps,inject,2)==(identity(2),{}) + inject[4]=(1,1) + assert tangent(steps,inject,2)[1] + fraction=identity(2) + update(fraction,("ADD",0,1,Q(-3,2))) + assert fraction[0]=={0:1,1:Q(-3,2)} + return ["two nonzero transported derivatives cancel across swaps","wrong sign spoils cancellation","exact fractional transport"] + + +def launch(caller,price,deadline,rows,progress): + b=caller["types"]["B"] + n,offset=b["roles"],b["offset"] + assert (caller["stages"],n,offset,len(b["ports"]))==(17,36,36,8) + steps,odd,even=unit_ops(caller["events"],n,offset) + keys,total=stock(odd,even) + assert keys==price["equal_mask_keys"] and len(keys)==CAP + assert total==price["all_disjoint_pair_placements"]==11938 + assert total-len(keys)==price["unequal_mask_exclusions"]==11728 + roles={t:r for t,(r,_) in (odd|even).items()} + progress.update(caller_events=len(steps),literal_single_edits=180,odd_sites=len(odd),even_sites=len(even)) + direct=[] + for item in keys[:2]: + assert len(item["even_mask"])==8 + inject={t:(roles[t],sign) for o,e in item["fusions"] for t,sign in ((o,1),(e,-1))} + assert len(inject)==4 + old,delta=tangent(steps,inject,n) + assert old==identity(n) + direct.append(delta) + progress["old_endpoint_columns"]=n + progress["direct_tangent_keys"]=2 + terms=impulses(steps,roles,n,deadline) + for i,item in enumerate(keys): + if monotonic()>=deadline: + raise TimeoutError("paired derivative cap") + delta,_=exact_delta(terms,item["fusions"],roles) + if i<2: + assert delta==direct[i] + witness=None + if delta: + a,b=min(delta) + witness=[a+offset,b+offset,str(delta[a,b])] + rows.append(item|dict(status="exact derivative exclusion" if witness else "first derivative zero", + witness=witness,nonzero_coordinates=len(delta),direct_tangent=i<2)) + + +def main(): + parser=ArgumentParser() + parser.add_argument("--root",type=Path,default=ROOT) + parser.add_argument("--controls-only",action="store_true") + args=parser.parse_args() + assert __debug__ + price=loads(checked(args.root,"plan/PRICE.json"),object_pairs_hook=unique) + assert price["head"]==HEAD and price["caller"]==CALLER and price["caller_sha256"]==CALLER_PAYLOAD + assert price["first_gate"]=={"keys":CAP,"runner_seconds":SECONDS} + assert price["formal_gate"]=={"keys":4,"runner_seconds":35} + tests=controls() + keys=price["equal_mask_keys"] + assert len(keys)==CAP + if args.controls_only: + print(dumps(dict(controls=tests,highest_price=keys[:2]),indent=2,sort_keys=True)) + return 0 + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + signal(SIGALRM,stop) + alarm(SECONDS) + rows,progress,error=[],{},None + try: + raw=decompress(checked(args.root,"inputs/7113-CALLER.json.gz")) + assert sha256(raw).hexdigest()==CALLER_PAYLOAD + launch(loads(raw,object_pairs_hook=unique),price,monotonic()+22,rows,progress) + except TimeoutError as exc: + error=str(exc) + finally: + alarm(0) + print(dumps(dict(head=HEAD,caller=CALLER,pins=PINS,q=1,body="unit",controls=tests, + cap_cases=CAP,cap_seconds=SECONDS,counts=Counter(r["status"] for r in rows),progress=progress, + results=rows,unvisited=keys[len(rows):],timeout=error),indent=2,sort_keys=True)) + return 2 if error else 0 + + +if __name__=="__main__": + raise SystemExit(main()) diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/inputs/7113-CALLER.json.gz b/research/p104-type-b-simultaneous-idle-bound/r123/inputs/7113-CALLER.json.gz new file mode 100644 index 0000000000..2479c3a615 Binary files /dev/null and b/research/p104-type-b-simultaneous-idle-bound/r123/inputs/7113-CALLER.json.gz differ diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/inputs/PR7357-SHA256.json b/research/p104-type-b-simultaneous-idle-bound/r123/inputs/PR7357-SHA256.json new file mode 100644 index 0000000000..da232d65c0 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/inputs/PR7357-SHA256.json @@ -0,0 +1,5 @@ +{ + "INDEPENDENT.json": "afec20386a8fbdc70d1b96998adbe18edace42a3e14a015e0eab5c09fc311617", + "LEAD.json": "bf0cbae853422e85788449b40ddc2fa807b042d8a357a56a7c7654dda51331e4", + "PRICE.json": "33aad506112912ddf0721a2b007d9194eaa02e5792aceda2f9774f8838511262" +} diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/inputs/direct_impulse.py b/research/p104-type-b-simultaneous-idle-bound/r123/inputs/direct_impulse.py new file mode 100644 index 0000000000..14b5e8bb18 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/inputs/direct_impulse.py @@ -0,0 +1,170 @@ +"""Independent exact direct interval projector comparison for R85.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from time import monotonic + +PRICE = "33aad506112912ddf0721a2b007d9194eaa02e5792aceda2f9774f8838511262" +ADMISSION = "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13" +CALLER = "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CAP, SECONDS = 180, 20 + + +class Capped(Exception): + pass + + +def need(condition, text): + if not condition: + raise ValueError(text) + + +def read(path, expected): + raw = path.read_bytes() + need(sha256(raw).hexdigest() == expected, "changed input " + path.name) + return loads(raw) + + +def gates(event, offset, q): + family, op, *a = event + if family == "J": + u, v, l, r = a[1] + u, v = u - offset, v - offset + return [("add", u, v, q * Q(l)), ("add", v, u, Q(r) / q)] + if family != "B": + need(family == "A", "unknown event family") + return [] + dest, *tail = a + dest -= offset + if op == "ADD": + return [("add", dest, tail[0] - offset, Q(tail[1]))] + if op == "QUERY": + return [("add", dest, tail[0] - offset, q ** tail[1])] + if op == "SWAP": + return [("swap", dest, tail[0] - offset, Q(1))] + if op == "SCALE": + return [("scale", dest, dest, Q(tail[0]))] + if op == "IDLE_ODD": + return [("scale", dest, dest, q ** tail[1])] + need(op in ("IDLE_ONE", "LAMBDA"), "unknown Type B op") + return [] + + +def basis(n, i): + return [Q(k == i) for k in range(n)] + + +def apply(op, vector, transpose=False): + kind, d, s, c = op + if kind == "add": + if transpose: + d, s = s, d + if vector[s]: + vector[d] += c * vector[s] + elif kind == "scale": + vector[d] *= c + else: + need(kind == "swap", "bad gate") + vector[d], vector[s] = vector[s], vector[d] + + +def between(items, early_role, late_role, n): + column = basis(n, early_role) + for op in items: + apply(op, column) + for i, x in enumerate(column): + if i != late_role and x: + return "column", i, x + row = basis(n, late_role) + for op in reversed(items): + apply(op, row, True) + for i, x in enumerate(row): + if i != early_role and x: + return "row", i, x + need(column[late_role] == row[early_role] and column[late_role], "singular interval action") + return None + + +def controls(): + need(between([("swap", 0, 1, Q(1))], 0, 1, 2) is None, "valid swapped projector rejected") + need(between([("add", 1, 0, Q(-2))], 0, 0, 2) == ("column", 1, Q(-2)), + "mixed impulse column not rejected") + need(between([("add", 0, 1, Q(-3, 2))], 0, 0, 2) == ("row", 1, Q(-3, 2)), + "mixed covector row not rejected") + return ["swapped projector", "negative column shear", "fractional row shear"] + + +def literal_stock(events, offset): + odd, even = {}, {} + for i, e in enumerate(events): + if e[:2] == ["B", "IDLE_ODD"]: + need(len(e[3]) == 1 and e[4:] == [-1], "unexpected signed odd idle") + odd[i] = [e[2] - offset, sorted(e[3])] + if e[:2] == ["B", "IDLE_ONE"]: + even[i] = [e[2] - offset, sorted(e[3])] + return odd, even + + +def main(args): + tests = controls() + price, admission = read(args.price, PRICE), read(args.admission, ADMISSION) + need(price["head"] == admission["head"] == HEAD and admission["exit"] == 0 and + price["caller_sha256"] == CALLER and price["limits"]["first_cases"] == CAP and + price["limits"]["first_seconds"] == SECONDS, "price mismatch") + started = monotonic() + caller = read(args.caller, CALLER) + data = caller["types"]["B"] + n, off = data["roles"], data["offset"] + need((caller["stages"], n, off, len(data["ports"])) == (17, 36, 36, 8), "wrong Type B contract") + old, new = literal_stock(caller["events"], off) + need({str(k): v for k, v in old.items()} == price["odd_jobs"] and + {str(k): v for k, v in new.items()} == price["even_jobs"], "exact literal census differs") + keys = [{"odd": o, "even": e, "size": len(b)} for o, (_, a) in sorted(old.items()) + for e, (_, b) in sorted(new.items()) if set(a).isdisjoint(b)] + need(keys == price["keys"] and len(keys) == CAP, "exact key stock differs") + q = Q(1) + flattened = [] + offsets = [0] + for event in caller["events"]: + flattened.extend(gates(event, off, q)) + offsets.append(len(flattened)) + for i in range(n): + vector = basis(n, i) + for op in flattened: + apply(op, vector) + need(vector == basis(n, i), "old exact unit endpoint differs") + roles = {t: v[0] for t, v in (old | new).items()} + outcomes = [] + for key in keys: + if monotonic() - started >= SECONDS - 2: + break + a, b = sorted((key["odd"], key["even"])) + # Original old idles are identity at q=+1, unit body, so both boundaries can be omitted. + interval = flattened[offsets[a + 1]:offsets[b]] + witness = between(interval, roles[a], roles[b], n) + result = {"key": [key["odd"], key["even"]], "mask_size": key["size"], + "chronological_roles": [roles[a] + off, roles[b] + off]} + if witness is None: + result |= {"status": "provisional_projectors_equal"} + else: + side, role, value = witness + result |= {"status": "excluded", "exact_off_axis": [side, role + off, str(value)]} + outcomes.append(result) + unvisited = keys[len(outcomes):] + return {"status": "CAPPED" if unvisited else "EXHAUSTED", "head": HEAD, "price_sha256": PRICE, + "caller_sha256": CALLER, "admission_sha256": ADMISSION, "case_cap": CAP, + "runner_cap_seconds": SECONDS, "q": 1, "body": "unit", "old_endpoint_columns": n, + "controls": tests, "tested": len(outcomes), "outcomes": outcomes, + "counts": dict(Counter(row["status"] for row in outcomes)), "unvisited": unvisited, + "survivors": [row["key"] for row in outcomes if row["status"] != "excluded"]} + + +if __name__ == "__main__": + p = ArgumentParser() + for name in ("price", "admission", "caller"): + p.add_argument("--" + name, type=Path, required=True) + print(dumps(main(p.parse_args()), sort_keys=True, indent=2)) diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/r85/independent/RESULT.json.gz b/research/p104-type-b-simultaneous-idle-bound/r123/r85/independent/RESULT.json.gz new file mode 100644 index 0000000000..fbbd2392d2 Binary files /dev/null and b/research/p104-type-b-simultaneous-idle-bound/r123/r85/independent/RESULT.json.gz differ diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/r85/independent/SHA256 b/research/p104-type-b-simultaneous-idle-bound/r123/r85/independent/SHA256 new file mode 100644 index 0000000000..a5556c7439 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/r85/independent/SHA256 @@ -0,0 +1,16 @@ +d04426aed9528aedc6400d384d7fd13c6531e5e3e6592a7eea4faee46c61e004 direct_impulse.py +fa7c834d0ac27cc6959bc00b59df3fbfcba36678a02c34b268e609bc5bd1c69a REPLAY.md +afec20386a8fbdc70d1b96998adbe18edace42a3e14a015e0eab5c09fc311617 RESULT.json +9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa RUN.exit +b134aeb750734abe6c294210bd3d3862e946ec7ee073157ae43d6ada3e4bd0f7 RUN.stderr +f8696f7217783bc7353a40981543d3bf0f02ef94f8c1f91b388256dca3a309a8 PREP-START-UTC.txt +f8696f7217783bc7353a40981543d3bf0f02ef94f8c1f91b388256dca3a309a8 PREP-END-UTC.txt +f8696f7217783bc7353a40981543d3bf0f02ef94f8c1f91b388256dca3a309a8 RUN-START-UTC.txt +f8696f7217783bc7353a40981543d3bf0f02ef94f8c1f91b388256dca3a309a8 RUN-END-UTC.txt +afec20386a8fbdc70d1b96998adbe18edace42a3e14a015e0eab5c09fc311617 CLEAN.json +9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa CLEAN.exit +18bb574022c48434ed6c9ef094760544c28a61efa58c0aac313cf190b2c8dcb5 CLEAN.stderr +9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa CLEAN-COMPARE.exit +4355a46b19d348dc2f57c046f8ef63d4538ebb936000f3c9ee954a27460dd865 MUTATION.exit +ba6750091223b40a0d96e287945005491a7c68efa4932f5fcecba2634948c175 MUTATION.stderr +e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 MUTATION.stdout diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/r85/lead/RESULT.json.gz b/research/p104-type-b-simultaneous-idle-bound/r123/r85/lead/RESULT.json.gz new file mode 100644 index 0000000000..44bb683d37 Binary files /dev/null and b/research/p104-type-b-simultaneous-idle-bound/r123/r85/lead/RESULT.json.gz differ diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/PRICE.json.gz b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/PRICE.json.gz new file mode 100644 index 0000000000..58b48bbf43 Binary files /dev/null and b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/PRICE.json.gz differ diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/SHA256 b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/SHA256 new file mode 100644 index 0000000000..6292503a02 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/SHA256 @@ -0,0 +1,20 @@ +6757d1f60533e42c5f42c085dd9300338825b0b4642f4e977fd148ac9a143de0 quote.py +bb55822cfee7a53d9e191e278123bb7751ba61c0fda943f267eecde4ba399e5c REPLAY.md +33aad506112912ddf0721a2b007d9194eaa02e5792aceda2f9774f8838511262 PRICE.json +9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa PRICE.exit +93cb96a65652fced100efb93dcf6a27bd78876f938a0117cee3b00a9b3d33fc6 PRICE.stderr +33aad506112912ddf0721a2b007d9194eaa02e5792aceda2f9774f8838511262 CLEAN.json +9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa CLEAN.exit +f26bbae0822e7aef8005467b9931c3277a251620d2bf4527722e4da923952632 CLEAN.stderr +9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa CLEAN-COMPARE.exit +4355a46b19d348dc2f57c046f8ef63d4538ebb936000f3c9ee954a27460dd865 FIRST-PRICE.exit +310b6d3d374b605736519d1bfe01b8f0c1caee3a3d98420b17ac5ad37a47d37e FIRST-PRICE.stderr +ec6dfd31095dd02fd0ad51c497853ea90335e8d6b7b95e96e569c88384782077 PREP-START-UTC.txt +37dd353b5516e7dc29d16354acaf2a713c3a906e3fd41d29e63fdf99a3178bd0 PREP-END-UTC.txt +255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc inputs/7113-CALLER.json +c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13 inputs/7334-ADMITTED.json +337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82 inputs/7334-READBACK.json +86f779c3eeb43563793e6ccb2227257ef732b2ca12fbbde2f9099988f903a484 inputs/R53-PRICE.json +b73057381860987c6de1666205e91a0e3d116a8299d8aa425682f5960609c21f inputs/R59-PRICE.json +348c8b2de72f1f112cb1337eca9d29ca96c85a7ad903beecafb1a2a1221f408e inputs/derivative_check.py +f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182 inputs/pricing.py diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/7334-ADMITTED.json b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/7334-ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/7334-ADMITTED.json @@ -0,0 +1,58 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "caller_sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "crossing": [ + "0.00364665195644044790699554028334161", + "0.00364665195644044790699554028334162" + ], + "end": "2026-11-11T23:04:43Z", + "exit": 0, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "hosted_at_admission": "plan and historical success; candidate replay in progress", + "inputs": { + "EARLY-RESULT.json": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649", + "INPUTS.json": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d", + "NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "PROPOSED-CLAIM.json": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03", + "RESULT.json": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194", + "SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + }, + "kappa": "0.00364665195644", + "ours": "0", + "peer_gain": "0.000000430519994", + "prior_kappa": "0.003646221436446", + "receipt": { + "peer-prep/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "peer-prep/STATIC.json": "500cc563b7dac8b1de1faf1dee9b820e73152dfddc15a650cd1191edd39e8c79", + "peer-price/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "peer-price/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "peer/COMMAND.txt": "714bfab024155d8216f3ef99f3ee7627ddc35ab341c486ac6bd53c476b757130", + "peer/COMMIT.stdout": "597470d8132a3812deb3624a859546c0c13d52b094fd6fc61e7416941130bd70", + "peer/END-UTC.txt": "9c46923c616c14da5b8ed503e1652021d7bd409a10ec91a78a03263013fba08a", + "peer/METADATA.stdout": "5873404cb4424dca918a00d503569f3c29a3190fd029a007e1afb2006399f647", + "peer/RUN.exit": "9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa", + "peer/RUN.stderr": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "peer/RUN.stdout": "d589626c7581fbb9928bc615364cfee49deb62dfc0a39a903417ca62be89cf8c", + "peer/START-UTC.txt": "5b78fd6d42a2b42206891318c08e6014de57d7ca46b0201cd11a166f452210f7" + }, + "source_history": "exact anchored base and recursive package provenance, sparse shallow stock wrapper not executed", + "stages": { + "caller": "PASS_HELPER_319_FUSED_CALLER 91166298911/25000000000000", + "early": "PASS_HELPER_319_EXACT_NATIVE_AND_SIGNED_PRICE 0.00364665195644", + "frontier": "PASS_HELPER_319_FUSED_FRONTIER_PROPOSAL 91166298911/25000000000000", + "native": "PASS_HELPER_319_FUSED_NATIVE 3646017316711/1000000000000000" + }, + "start": "2026-11-11T22:54:48Z", + "status": "independently_reproduced_comparable", + "tree": "fa98712a459b20c10240450097c87de433f8a750" +} diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/7334-READBACK.json b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/7334-READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/7334-READBACK.json @@ -0,0 +1,188 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "bit_admitted": "12039/3125000", + "bit_claim_headroom": "3000951089/25000000000000", + "bit_premise": "376669/100000000", + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "claim": "91166298911/25000000000000", + "context_c": 2430, + "context_headroom": 1666, + "copies": 17, + "directed_bounds": { + "new_at_claim": [ + "347195197206460540909548691538238227127/2000000000000000000000000000000000000000000000000", + "1735975986032302704547743457691191192207/10000000000000000000000000000000000000000000000000" + ], + "new_at_old_crossing_upper": [ + "333717954993733063339209580360321337006028706669/2000000000000000000000000000000000000000000000000", + "1668589774968665316696047901801606685030143589709/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_lower": [ + "8890529086421014119/10000000000000000000000000000000000000000000000000", + "8890529086421080299/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_upper": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "new_at_tested": [ + "1464673416007288863003441470091977383033/10000000000000000000000000000000000000000000000000", + "1464673416007288863003441470091977438357/10000000000000000000000000000000000000000000000000" + ], + "old_at_claim": [ + "-1668785950738799647054310634446839861363893886031/10000000000000000000000000000000000000000000000000", + "-66751438029551985882172425377873594454555753177/400000000000000000000000000000000000000000000000" + ], + "old_at_old_crossing_upper": [ + "-357270001119021587349/10000000000000000000000000000000000000000000000000", + "-357270001119021530951/10000000000000000000000000000000000000000000000000" + ] + }, + "empty_root_credits": 0, + "exact_gain": "215259997/500000000000000", + "exact_relative_percent": "21525999700/1823110718223", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "incumbent": "1823110718223/500000000000000", + "main_boundaries": 104, + "native_grid": [ + 1125, + 25 + ], + "native_ingredient_claim": "3646017316711/1000000000000000", + "new_raw_interval": [ + "364665195644044790699554028334161/100000000000000000000000000000000000", + "182332597822022395349777014167081/50000000000000000000000000000000000" + ], + "old_raw_upper": "36462214364462343366888845568981/10000000000000000000000000000000000", + "ordinary": 782715464, + "ordinary_delta": 52088, + "ordinary_headroom": 217284536, + "outer_functional": 4, + "outer_strict": 54, + "outer_strict_slack": "299635334804355997/10000000000000000000000000000000000", + "owned_lifetimes": 73, + "owned_peak": 50, + "paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110519, + "parent": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "path_pins": { + "dependencies/7298/pricing.py": { + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "dependencies/7314/NATIVE-RESULT.json": { + "sha256": "336f463da5afe5b60bfd3b9f0ce8aeea5a5feb1f854613bf4218ba0b28b3371b" + }, + "dependencies/7314/PROPOSED-CLAIM.json": { + "sha256": "41a08c4b7d0b2de4af22bc778948a143027eb3065fff47b0400b6ded1cc52778" + }, + "dependencies/7314/RESULT.json": { + "sha256": "432191ca572c9221935787ebe392699e3a1ef4512b0bf4fbc704657321cc87ca" + }, + "dependencies/round65/price.json": { + "sha256": "25205ad2cf4230bd2b2b704eec9f96ec4a5486fd575b5599861b28ffdd15b00b" + }, + "receipts/EARLY-RESULT.json": { + "git_blob": "675d6cf2374f3384019dfd53b2bdffd845005f13", + "sha256": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649" + }, + "receipts/INPUTS.json": { + "git_blob": "95c53f4594287a72d9b586f10ee136d0a1686984", + "sha256": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d" + }, + "receipts/NATIVE-RESULT.json": { + "git_blob": "eb101307d4d0399efed96d88cf6d4c01ec9c7369", + "sha256": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812" + }, + "receipts/PROOF.md": { + "git_blob": "7644e5571d583183ee93b686612b5ec4555f6911", + "sha256": "560de573bfd4563c16ca3c7308fa729b4188fabe802d8830f343c3873f75b59d" + }, + "receipts/PROPOSED-CLAIM.json": { + "git_blob": "6b491894580741e3e2c11a453722a0302db7b5d6", + "sha256": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03" + }, + "receipts/README.md": { + "git_blob": "b3a055f4e0d334ce2e7df3310caaa0849eb3eba1", + "sha256": "b4db0eb83ab6a2f7151bed2da955a487f4816ec9d1976eccc21e54c2725490b0" + }, + "receipts/REFERENCE.json": { + "git_blob": "8859e243cc39546bcb1e257d95c19a658c455dc7", + "sha256": "3e66e054b803551f18b8670da0b2990a7d0eeb689dfc45b56dbcba295551da70" + }, + "receipts/REPLAY.txt": { + "git_blob": "0b8d8048c18740060f4b7f6d380a5f3a0f30ee53", + "sha256": "230984f4b8206ae4d0c0f18fbba86ff43a1a9623f8ed337cf1285360f9a67c0c" + }, + "receipts/RESULT.json": { + "git_blob": "3034a490f5b0656ae71495c99493c4ab1ac1f5c6", + "sha256": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194" + }, + "receipts/SOURCES.json": { + "git_blob": "6b97e903a6df8de437068a0e2907823885928053", + "sha256": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593" + }, + "receipts/VERIFY.json": { + "git_blob": "cc98ee2a5c5a79e670094a6f55c7cacda8fd330c", + "sha256": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513" + }, + "receipts/construct.py": { + "git_blob": "89e923bd738dfc404ca76b7ae36f13844ac4bfbb", + "sha256": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + } + }, + "physical_maps": 3037, + "productive_fields": 22461, + "rank_surplus": 1424, + "raw_strict_separation": "43051999421357030665572644351/100000000000000000000000000000000000", + "scope": "Exact receipt and directed-price readback. No native or caller execution in this audit.", + "source_archive_sha256": "0589953b3886d96eacf3bda3d38d8d574bb739fba1056af7f32f56047b6061e2", + "targets": { + "1": 306, + "2": 357, + "3": 799, + "4": 3825, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "tested": "364665195644007/100000000000000000" +} diff --git a/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/derivative_check.py b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/derivative_check.py new file mode 100644 index 0000000000..ce5cdf3779 --- /dev/null +++ b/research/p104-type-b-simultaneous-idle-bound/r123/r85/price/inputs/derivative_check.py @@ -0,0 +1,67 @@ +"""Check decrease of the complete priced moments through the retained BIT cap.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +PINS = { + 'PRICE.json':'52e05b80069ce01cad3b8e5f3cf9123e930de36987bd398dd43f103953a4674a', + 'inputs/pricing.py':'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', + 'inputs/7334-READBACK.json':'337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82', +} + + +def derivative(histogram,low,high,tariff): + log,power = tariff['log_bounds'],tariff['power_bounds'] + ln2_low,ln2_high = log(Q(2)) + lower = upper = Q(0) + for rank,count in histogram.items(): + shift = rank.bit_length()-1 + a,b = log(Q(rank,1<