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-charged-rank-six-support-bound/LOCAL-PINS.json b/research/p104-charged-rank-six-support-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..8edc678025 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/LOCAL-PINS.json @@ -0,0 +1,22 @@ +{ + "dependencies/round30/complex/audit.py": "67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb", + "dependencies/round30/complex/source/inputs/CALLER.json.gz": "58beaf24e01c0589ecd5d1676d6d27e75b779f089d0674eda11725465ffc04e1", + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": "9851ebaa4b4404be1f5670b8a8dfc6ee96a8e19e85731edd4a71d52bbfa9c793", + "dependencies/round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "dependencies/round30/complex/source/powers.py": "c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee", + "dependencies/round35/verify.py": "c906fffec26f043e159f8e314b0f245cde432cf72d2bc6a6ade6235a4c798c5a", + "dependencies/round36/cochart-audit/verify.py": "58cab0bb2f24fe29d0e190cbe3cc0dc85f889ec4af66b5a02328d1e1d0e37e8a", + "dependencies/round36/incremental/predecessor_split.py": "999b9eeabe5cd1a7e3ec014d1a449f850b4ac9bfb19749cddef41ae12cd0b405", + "dependencies/round36/incremental/support.py": "f3e6eeb879480715c5c32c1a390a63c57d26ea1c9a9cbdb89b83ca34260e47f6", + "dependencies/round36/predecessor_search.py": "668022953f53929fd4d95ed1b5c01ac2ba3b4bdf6be7babae511757eb21b7e6a", + "dependencies/round37/preflight/PRICE.json.gz": "47594a4d194330b5d5beab4c76e46d2cbd89968458aa3b0042c2de6918b52c95", + "dependencies/round37/preflight/price.py": "8b1b345bd4a2732c74251c1b95d47f98cd37184894d8979a6ef1953d38686be8", + "dependencies/round38/incremental/screen.py": "43a74344555088b016a3fb857b7c86de3f2880ef85b77846c4362037779b8405", + "dependencies/round49/NEXT.md": "f304c5b62077e43d35696d939a0f96f420a30cc8173fc97978c4e54d867ff86f", + "dependencies/round50/lead/screen.py": "47251bd902c4fd3fda3597463cf4609bf380194558461320dc432b86f6c989d1", + "engines/independent_2_5.py": "7bae36fb1530b08f84ac21e66a44ae27a282e4a3aba3997a1acd4324be2d6ee1", + "engines/independent_3_4.py": "7565c5984841022d70e4103ebaf2969967618c386929ecbf9ecf27385fe5b336", + "engines/primary_2_5.py": "5850a8275d2dce67736b8515f19c57dc57720212d41df59c559c8acba2c9ee87", + "receipts/SHA256.json": "4756831bd3e43d7af429dfa203a480df4aef32cb1417ae38881225bed269d37b", + "receipts/SUMMARY.json": "da07165d52f580cee19abc123e733d2b28679322114c64e8ea07a22e16d90ac5" +} diff --git a/research/p104-charged-rank-six-support-bound/NOTICE b/research/p104-charged-rank-six-support-bound/NOTICE new file mode 100644 index 0000000000..593ed609c6 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/NOTICE @@ -0,0 +1,8 @@ +Apache-2.0. +#7277 supplies the literal word and comparable invoice. #7113 supplies +the signed caller. #7142 supplies the charged endpoint precedent, and +#5599/#7130 supply the common-chart split and basis constructor lineage. +#7299, #7303 and #7308 supply related price, fixed-mass and replay +comparisons. Earlier campaign sources and original attributions are +retained in the bundled replay dependencies. OpenAI Codex and subagents +materially assisted. diff --git a/research/p104-charged-rank-six-support-bound/PROVENANCE.json b/research/p104-charged-rank-six-support-bound/PROVENANCE.json new file mode 100644 index 0000000000..58d29af597 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/PROVENANCE.json @@ -0,0 +1,45 @@ +{ + "files": { + "dependencies/round30/complex/audit.py": { + "commit": "2c777389ec0476e97ab141c645af01ff28a46aa6", + "git_blob": "89e4a6b3dd93f91fd56c18ec37e15ee668b486d3", + "path": "research/p104-owned-move-destination-span/dependencies/round30/complex/audit.py", + "sha256": "67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/2c777389ec0476e97ab141c645af01ff28a46aa6/research/p104-owned-move-destination-span/dependencies/round30/complex/audit.py", + "uncompress": false + }, + "dependencies/round30/complex/source/inputs/CALLER.json.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "9451ceaf6e8e037894680b549f3ef41c21b260d7", + "path": "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "uncompress": true + }, + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "ef86c8ec8ed0a2042017a6f42515e70dd15cfffd", + "path": "research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "sha256": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "uncompress": true + }, + "dependencies/round30/complex/source/inputs/WORD.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "077bf48c35db0ddafae81f1bfa0ffacc30894b2b", + "path": "research/p104-terminal-cut-rechart/WORD.json.gz", + "sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz", + "uncompress": false + }, + "dependencies/round30/complex/source/powers.py": { + "commit": "2c777389ec0476e97ab141c645af01ff28a46aa6", + "git_blob": "1ac680b880d282ff3ec98593c87340413ae958b0", + "path": "research/p104-owned-move-destination-span/dependencies/round30/complex/source/powers.py", + "sha256": "c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/2c777389ec0476e97ab141c645af01ff28a46aa6/research/p104-owned-move-destination-span/dependencies/round30/complex/source/powers.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-charged-rank-six-support-bound/README.md b/research/p104-charged-rank-six-support-bound/README.md new file mode 100644 index 0000000000..fd9df16900 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/README.md @@ -0,0 +1,121 @@ +# Charged rank-six productive split support on the retained P104 word + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** On the exact +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) +word, all 83 charged rank-six endpoint extensions of type 3+4 and +all 83 of type 2+5 fail the necessary common-chart support test. +Each family includes 50 input extensions, 33 output extensions +and 73 endpoint-and-partition groups. Zero signatures or cut +incidences remain unresolved. The compatible saving upper after +support is zero. The complete comparable witness remains #7277 +at κ = 0.003645669928698. + +| Productive partition | Typed signatures | Representative cut incidences | Nonzero pure prefix | Nonzero pure suffix in independent replay | Price-only lower margin | +| --- | ---: | ---: | ---: | ---: | ---: | +| 3+4 | 83 | 714 | 0 | 24 | 0.1174506515937458 | +| 2+5 | 83 | 346 | 0 | 0 | 0.08102479309361352 | + +## Complete price and scoped support + +Each alternative adds one paid rank-one endpoint MOVE and replaces +one productive rank-six job by productive jobs of ranks 3 and 4, +or 2 and 5, in each of the 17 exact #7113 native copies. The replay +reconstructs the complete signed invoice and regenerates the frozen +endpoint price table before evaluating support. The positive +margins in the table are directed lower bounds at the pinned old +crossing upper, rounded for display. Other added ordinary and +physical costs are free in this price-only probe. Prices are +computed per alternative, and the exact rational endpoints are +in [SUMMARY.json](receipts/SUMMARY.json) and the emitted PRICE +receipts. + +For a selected partition, fix the proposed endpoints and a strictly +intermediate chart at one of its two rank offsets. The enlarged +cohort is the existing helper cohort at the proposed endpoints +together with all allowed single extenders. Each individual +extension lies inside this enlarged domain. The #5599 split +requires a nonzero rational prefix image and an adjoint suffix +image supported on the same helper coordinates with nonzero +pairing. A zero pure prefix on the enlarged cohort excludes +the requirement for every individual extender. + +Representative cuts are reconstructed from the literal contacts +of each chart. Between consecutive contacts, the bank and its +normalized prefix rows remain fixed. Operations on other charts +act trivially on a suffix perturbation supported on the bank. +The initial-bank guard is checked. The new rank-one endpoint +transport lies outside the eligible intermediate chart ranks, so +the fixed-chart, fixed-order representative census still applies. +Scalar operands, MOVE endpoints and owned lifetimes are checked +in the literal trace. + +The primary gate checks the necessary pure prefix at all 1,060 +representative incidences across the two disjoint typed partitions. +The independent replay separately reconstructs geometry, price and +cut coverage, runs the rational suffix sweep first, and then checks +the pure prefix. The 24 nonzero suffix incidences in 3+4 have no +pure prefix partner. The omitted-paid-MOVE and wrong-pairing +controls reject their mutations. A lawful cocharted basis fixture +and exterior-cancellation fixture provide positive controls. + +This result concerns one charged endpoint extension at a time +under the original word's chart and ownership chronology. Changed +chronology, new chart labels, new endpoint mechanisms and smaller +ranks remain open. No physical candidate advanced to signed native, +ownership, precision, tape, caller or outer verification. + +## Replay + +From a clean checkout with CPython 3.12 and assertions enabled: + +~~~sh +python3.12 -B scripts/research_package.py --package research/p104-charged-rank-six-support-bound +python3.12 -B scripts/check_research_commit.py --package research/p104-charged-rank-six-support-bound --check-modes --check-source-history +~~~ + +From a Git-free export, this command also emits all ten complete +receipts into a fresh output directory: + +~~~sh +python3.12 -I -B research/p104-charged-rank-six-support-bound/replay.py --out fresh-receipts +~~~ + +[PROVENANCE.json](PROVENANCE.json) pins the public inputs by exact +commit, path, Git blob and SHA-256. [LOCAL-PINS.json](LOCAL-PINS.json) +pins the bundled replay sources and earlier campaign dependencies +by package-relative path. The replay authenticates the uncompressed +payloads of the bundled caller, crossing and price snapshots. It +verifies all ten deterministic plaintext receipts against the exact +hashes in [SHA256.json](receipts/SHA256.json) and can emit their full +proof-relevant fields. It uses only the standard library. + +## Credit + +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) at +`ed090b57ed88f8859e5ff4643645099e6ba856ea` supplies the word +and complete comparator. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +at `07a76c5e2738882c0cb322278e56f6cae3c9885d` supplies the +signed caller. [#7142](https://github.com/CrocSwap/integer-mult-bounds/pull/7142) +supplies the charged endpoint precedent. +[#5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) +and [#7130](https://github.com/CrocSwap/integer-mult-bounds/pull/7130) +supply the common-chart split identity and basis constructor lineage. +[#7299](https://github.com/CrocSwap/integer-mult-bounds/pull/7299) +supplies related split pricing. [#7308](https://github.com/CrocSwap/integer-mult-bounds/pull/7308) +supplies the bundled complete signed-invoice audit and directed +price helper. The earlier campaign priced all 777 typed signatures +in Round 37 and replayed the higher-rank eight and seven subsets +in Rounds 37 and 38. Those support certificates have different +rank scopes. [#7303](https://github.com/CrocSwap/integer-mult-bounds/pull/7303) +covers fixed-mass singleton splits under the retained word, whereas +this test charges a rank-one endpoint extension. OpenAI Codex and +subagents materially assisted. + +## Open next questions + +Can a changed chart chronology or endpoint basis supply a common +chart with pure prefix support at a favorable complete price? +Pin one distinct interface or partition and bound the full +compatible stock before building. A surviving proposal needs +arbitrary-input signed forward and adjoint action, ownership, +restoration and fully charged precision and tape. diff --git a/research/p104-charged-rank-six-support-bound/SOURCES.json b/research/p104-charged-rank-six-support-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-charged-rank-six-support-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-charged-rank-six-support-bound/TASK.json b/research/p104-charged-rank-six-support-bound/TASK.json new file mode 100644 index 0000000000..b415c409f5 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "One paid rank-one endpoint extension of a rank-six productive helper in exact #7277, followed by a 3+4 or 2+5 cocharted split with the retained chart and ownership chronology.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Charged productive split research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Decide whether either independently price-positive typed partition has a necessary common-chart support witness before building.", + "budget_minutes": 8, + "evidence": "Exact 17-copy directed price, literal cut and ownership trace, primary and reverse-first rational support, lawful pairing positive control and missing paid MOVE rejection.", + "open_questions": [ + { + "blocked_by": "A survivor still needs exact arbitrary-input signed forward and adjoint action, ownership and restoration, complete price, precision and tape.", + "first_step": "Pin the new interface or partition and upper-bound the entire compatible charged stock before testing a native site.", + "question": "Can a changed chronology or endpoint basis create paid support for a different productive extension?", + "why_it_matters": "Both tested rank-six partitions have empty pure prefix support across the original chart cuts." + } + ], + "original_card": { + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4133: literal-slot defect", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4136: uniform commutation gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4140: uniform encoding gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "status": "author-checked" + }, + { + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "status": "author-checked" + }, + { + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4154: fiber-tag seam mismatch", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "p104-side-correction", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "This tests rank-six productive credit under an explicit added paid child, outside the fixed-mass singleton and earlier higher-rank screens.", + "scope_status": "changed", + "stop_rule": "Price each alternative separately and exhaust each 83-signature stock within its original capped replay. Stop without a build if the pure prefix and adjoint support gate excludes all cuts.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-charged-rank-six-support-bound/UNPACK.json b/research/p104-charged-rank-six-support-bound/UNPACK.json new file mode 100644 index 0000000000..c6122352da --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/UNPACK.json @@ -0,0 +1,14 @@ +{ + "dependencies/round30/complex/source/inputs/CALLER.json.gz": { + "destination": "dependencies/round30/complex/source/inputs/CALLER.json", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" + }, + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": { + "destination": "dependencies/round30/complex/source/inputs/EARLY-RESULT.json", + "sha256": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7" + }, + "dependencies/round37/preflight/PRICE.json.gz": { + "destination": "dependencies/round37/preflight/PRICE.json", + "sha256": "bc6134776a077b4ae3ef595c6000563062b2a42a3684a3852ba4f2f77b8dc726" + } +} diff --git a/research/p104-charged-rank-six-support-bound/VERIFY.json b/research/p104-charged-rank-six-support-bound/VERIFY.json new file mode 100644 index 0000000000..4d8b872d8b --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Reprice and exhaust both rank-six charged endpoint partitions, independently reconstruct the signed invoices and reverse-first support, and verify the exact full receipts.", + "timeout_seconds": 340 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/audit.py b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/audit.py new file mode 100644 index 0000000000..89e4a6b3dd --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/audit.py @@ -0,0 +1,423 @@ +"""Independent exact binary-scope audit of signed invoice and flow/cut equality.""" +import argparse +from collections import Counter, defaultdict, deque +from fractions import Fraction as F +from hashlib import sha256 +from itertools import pairwise +from pathlib import Path +from time import monotonic +import gzip +import json +import runpy +import sys + +ROOT = Path(__file__).resolve().parent +SOURCE = ROOT / 'source' +GRID = 10**48 +TARGET = F(10018846261809, 2500000000000000) +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +INPUTS = { + 'inputs/WORD.json.gz': '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + 'inputs/EARLY-RESULT.json': '691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7', + 'inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'powers.py': 'c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee', +} + + +def source(path): + data = (SOURCE / path).read_bytes() + assert sha256(data).hexdigest() == INPUTS[path] + return data + + +def basis(vectors): + pivot = {} + for v in vectors: + while v.bit_length() in pivot: + v ^= pivot[v.bit_length()] + assert v + pivot[v.bit_length()] = v + return pivot + + +def inside(vectors, pivot): + for v in vectors: + while v: + if v.bit_length() not in pivot: + return False + v ^= pivot[v.bit_length()] + return True + + +def log_scaled(value): + z = (value - 1) / (value + 1) + term = z + q = F(0) + for j in range(0, 160, 2): + q += term / (j+1) + term *= z*z + return 2*q, 2*(q+term/(161*(1-z*z))) + + +def exp_minus(value, steps): + term = F(1) + total = F(1) + for j in range(1, steps+1): + term *= -value / j + total += term + return total + + +def verify_power(rank, value): + if not rank: + assert value == (0, 0) + return + exponent = rank.bit_length()-1 + unit_lo, unit_hi = log_scaled(F(rank, 1 << exponent)) + two_lo, two_hi = log_scaled(F(2)) + xlo = TARGET*(unit_lo+exponent*two_lo) + xhi = TARGET*(unit_hi+exponent*two_hi) + assert 0 <= xlo <= xhi < 1 + # Round the exponents outward before Taylor, keeping intermediate + # numerators small without losing the finer-than-grid audit. + fine = 10**64 + xlo = F((xlo*fine).__floor__(), fine) + xhi = F((xhi*fine).__ceil__(), fine) + low = GRID*rank*exp_minus(xhi, 49) + high = GRID*rank*exp_minus(xlo, 50) + assert value[0] <= low <= high <= value[1], rank + + +def read_model(): + word = json.loads(gzip.decompress(source('inputs/WORD.json.gz'))) + early = json.loads(source('inputs/EARLY-RESULT.json')) + caller = json.loads(source('inputs/CALLER.json')) + source('powers.py') + primary = runpy.run_path(str(SOURCE/'powers.py')) + assert primary['GRID'] == GRID and primary['TARGET'] == TARGET + initial, final = word['initial'], word['final'] + n = word['public'] + program = word['program'] + frame = word['frames'] + ranks = [len(v) for v in frame] + bases = [basis(v) for v in frame] + subset = {} + main = set(word['live']) | {r+112 for r in word['live']} | set(word['hosted']['X2'] + word['hosted']['Y2']) + assert len(main) == 400 + + def nested(a, b): + key = a,b + if key not in subset: + subset[key] = ranks[a] < ranks[b] and inside(frame[a], bases[b]) + return subset[key] + + def rank(a, b, owned): + if a == b: + return 0 + if nested(a, b) or owned and nested(b, a): + return abs(ranks[a]-ranks[b]) + return None + + chart = {(-1, r): f for r, f in enumerate(initial)} + current = initial + [None]*word['owned_fields'] + contacts = [[(-1, r)] for r in range(n)] + [[] for _ in range(word['owned_fields'])] + chains = [] + paid = Counter() + for t, row in enumerate(program): + op, r = row[:2] + if op == 'MOVE': + a, b, owned = row[2:] + assert current[r] == a and owned == (r >= n) + rr = rank(a, b, owned) + assert rr + paid[rr] += 1 + current[r] = b + continue + f = row[-1] + key = (t, 0) + chart[key] = f + if op == 'INIT': + assert r >= n and not contacts[r] and current[r] is None + current[r] = f + roles = {r, row[2]} if op in ('ADD', 'COPY') else {r} + for role in roles: + assert current[role] == f + contacts[role].append(key) + if op == 'CLEAR': + assert r >= n and contacts[r] + chains.append((r, contacts[r])) + contacts[r] = [] + current[r] = None + assert current == final + [None]*word['owned_fields'] and not any(contacts[n:]) + assert len(chains) == 70 + movable = {k for k in chart if k[0] != -1} + terminal = {} + for r, f in enumerate(final): + key = (len(program), r) + chart[key] = f + contacts[r].append(key) + chains.append((r, contacts[r])) + if r not in main: + terminal[key] = initial[r] + movable.add(key) + edges = [(a,b,r >= n) for r, seq in chains for a,b in pairwise(seq)] + native_paid = Counter(rr for a,b,owned in edges if (rr := rank(chart[a],chart[b],owned))) + assert native_paid == paid and sum(paid.values()) == 6280 and len(edges) == 137891 + assert len(chart) == 73165 and len(terminal) == 1101 + copies = sum(e[0] == 'J' for e in caller['events']) + assert copies == 17 + target = Counter(rank(initial, chart[v], False) for v, initial in terminal.items()) + assert min(target) > 0 + P, T = [Counter({r: copies*q for r, q in hist.items()}) for hist in (paid, target)] + for kind, info in caller['types'].items(): + count = len(info['ports']) + for sign, offset, *bits in info['diagonal']: + assert (sign, offset, len(bits)) == (-1, 0, copies) + T[1+8*sum(bits)] += count + for event in caller['events']: + if event[0] == 'J': + continue + kind, op, _, *args = event + count = len(caller['types'][kind]['ports']) + if op == 'QUERY': + P[1] += count + elif op in ('IDLE_ONE', 'IDLE_ODD'): + P[8*len(args[0])+int(op == 'IDLE_ODD')] += count + assert P == Counter({int(k):n for k,n in early['invoice']['P'].items()}) + assert T == Counter({int(k):n for k,n in early['invoice']['T'].items()}) + assert sum(P.values()) == 110536 and sum(T.values()) == 22461 + prices = {r: tuple(int(v*GRID) for v in primary['power'](r,TARGET)) for r in P.keys()|T.keys()|set(range(1,10))} + prices[0] = (0,0) + for r,v in prices.items(): + verify_power(r,v) + incident = defaultdict(list) + charts = defaultdict(list) + for i,(a,b,_) in enumerate(edges): + incident[a].append(i) + incident[b].append(i) + for v in sorted(movable): + charts[chart[v]].append(v) + return chart, rank, terminal, edges, incident, charts, copies, P, T, prices + + +def dinic(n, s, t, caps, clock): + """Return feasible flow and prove equal capacity of the residual cut.""" + adj = [[] for _ in range(n)] + graph = [] + for (u,v),cap in sorted(caps.items()): + if cap: + assert cap > 0 and u != v + i = len(graph) + graph.extend(([u,v,cap,cap],[v,u,0,0])) + adj[u].append(i) + adj[v].append(i+1) + sys.setrecursionlimit(max(sys.getrecursionlimit(), n+50)) + total = 0 + while True: + clock() + levels = [-1]*n + levels[s] = 0 + q = deque([s]) + while q: + u = q.popleft() + for i in adj[u]: + _,v,r,_ = graph[i] + if r and levels[v] == -1: + levels[v] = levels[u]+1 + q.append(v) + if levels[t] == -1: + break + cursor = [0]*n + def augment(u, capacity): + if u == t: + return capacity + while cursor[u] < len(adj[u]): + i = adj[u][cursor[u]] + _,v,r,_ = graph[i] + if r and levels[v] == levels[u]+1: + d = augment(v, min(capacity,r)) + if d: + graph[i][2] -= d + graph[i^1][2] += d + return d + cursor[u] += 1 + return 0 + limit = sum(caps[s,v] for v in range(n)) + while (delta := augment(s,limit)): + clock() + total += delta + lhs = [0]*n + certificate = [] + for u,v,r,c in graph[::2]: + f = c-r + assert 0 <= f <= c + lhs[u] += f + lhs[v] -= f + if f: + certificate.append([u,v,f]) + assert lhs[s] == total == -lhs[t] and all(not lhs[i] for i in range(n) if i not in (s,t)) + cut = [i for i,l in enumerate(levels) if l >= 0] + assert s in cut and t not in cut + inside = set(cut) + assert total == sum(c for (u,v),c in caps.items() if u in inside and v not in inside) + return total, certificate, cut + + +def compile_case(model, pair): + chart, rank, terminal, edges, incident, charts, copies, P, T, prices = model + lo,hi = pair + labels = (lo,hi) + vertices = sorted(charts[lo] + charts[hi]) + var = {v:i for i,v in enumerate(vertices)} + E = sorted(set(i for v in vertices for i in incident[v])) + n = len(vertices) + s,t = n,n+1 + max_finite = max(max(v) for v in prices.values()) + hard = (len(E)+len(vertices)+1)*(2*max_finite+1) + unary = [[0,0] for _ in vertices] + cap = Counter() + old = 0 + + def edge(a,b,owned): + d = rank(a,b,owned) + return hard if d is None else prices[d][0] + + def terminal_cost(v, z): + d = rank(terminal[v],z,False) + return hard if d is None or d == 0 else -prices[d][1] + + for i in E: + a,b,owned = edges[i] + old += edge(chart[a],chart[b],owned) + if a in var and b in var: + cap[var[a],var[b]] += edge(lo,hi,owned) + cap[var[b],var[a]] += edge(hi,lo,owned) + elif a in var: + for bit,f in enumerate(labels): + unary[var[a]][bit] += edge(f,chart[b],owned) + else: + for bit,g in enumerate(labels): + unary[var[b]][bit] += edge(chart[a],g,owned) + for v in vertices: + if v in terminal: + old += terminal_cost(v,chart[v]) + for bit,z in enumerate(labels): + unary[var[v]][bit] += terminal_cost(v,z) + offset = 0 + for i,(a,b) in enumerate(unary): + m = min(a,b) + offset += m + cap[s,i] += b-m + cap[i,t] += a-m + assert all(c>=0 for c in cap.values()) + return vertices,E,old,offset,cap + + +def quote_case(model, scope, pair, changed): + chart, rank, terminal, edges, incident, charts, copies, P, T, prices = model + vertices,E,old,offset,cap=scope + labels=tuple(pair) + assert set(changed) <= set(vertices) + assert all(f in labels and f != chart[v] for v,f in changed.items()) + paid = P.copy() + productive = T.copy() + objective = 0 + for i in E: + a,b,owned = edges[i] + old_r = rank(chart[a],chart[b],owned) + new_r = rank(changed.get(a,chart[a]),changed.get(b,chart[b]),owned) + assert new_r is not None + if old_r: + paid[old_r] -= copies + if new_r: + paid[new_r] += copies + objective += prices[new_r][0] + for v in vertices: + if v in terminal: + old_r = rank(terminal[v],chart[v],False) + new_r = rank(terminal[v],changed.get(v,chart[v]),False) + assert new_r + productive[old_r] -= copies + productive[new_r] += copies + objective -= prices[new_r][1] + final_clock = max(k[0] for k in chart) + upper = sum(q*prices[r][1] for r,q in productive.items())-sum(q*prices[r][0] for r,q in paid.items()) + baseline = sum(q*prices[r][1] for r,q in T.items())-sum(q*prices[r][0] for r,q in P.items()) + assert upper == baseline+copies*(old-objective) + return {'status':'PASS_EXACT_DIRECTED_BINARY_CUT','head':HEAD,'pair':pair, + 'movable_vertices':len(vertices),'changed_vertices':len(changed), + 'directed_whole_upper':str(F(upper,GRID)), + 'signed_paid':dict(+paid),'signed_targets':dict(+productive), + 'rank_surplus':sum(r*(productive[r]-paid[r]) for r in productive.keys()|paid.keys()), + 'event_relabels':sorted((k,f) for (k,r),f in changed.items() if k=end: + raise TimeoutError('independent audit cap') + r=json.loads(args.receipt.read_bytes()) + assert r['head']==HEAD + model=read_model() + checked=[] + unresolved=[] + for row in r['cuts']: + if row['status']!='PASS_EXACT_DIRECTED_BINARY_CUT': + unresolved.append(row['pair']) + continue + clock() + checked.append(verify_case(model,row,clock)) + print(json.dumps({'status':'PASS_INDEPENDENT_FLOW_CUT_AND_DIRECTED_INVOICE','head':HEAD, + 'receipt_sha256':sha256(args.receipt.read_bytes()).hexdigest(),'checks':checked, + 'unresolved':unresolved+r['unvisited']},sort_keys=True,separators=(',',':'))) + + +if __name__=='__main__': + main() diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz new file mode 100644 index 0000000000..290ef7c9c5 Binary files /dev/null and b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz differ diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz new file mode 100644 index 0000000000..8f4096badd Binary files /dev/null and b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz differ diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/WORD.json.gz b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/WORD.json.gz new file mode 100644 index 0000000000..077bf48c35 Binary files /dev/null and b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/inputs/WORD.json.gz differ diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/powers.py b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/powers.py new file mode 100644 index 0000000000..1ac680b880 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round30/complex/source/powers.py @@ -0,0 +1,177 @@ +"""Directed signed invoice and paired rank-reduction ceilings.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as F +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path +from time import monotonic + +TARGET = F(10018846261809, 2500000000000000) +CLAIMS = F('0.003645372367832'), F('0.003645473221716') +GRID = 10**48 +PINS = { + 'old/inputs/native/WORD.json.gz': '75061d1e4b354e4cf36b690f30ddb2b257ed2f4e86509f87e17bb0f63eca126f', + 'old/inputs/native/RESULT.json': '75f34132b5b12b1a92f13b7a7c47ea3857f1955403090ae06b38dd9cf18aeb49', + 'old/inputs/caller/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'peer/WORD.json.gz': '66bc395b599bc0b805c5061bbbd124e2027ad86645c07abe40d0b472fa1a7a2b', + 'peer/RESULT.json': 'acd6ef312fc1d1b8a94919b345667fb17a8a38939db17976ba6a21c7d4de9eb9', +} + + +def load(old, peer): + roots = {'old':old, 'peer':peer} + out = {} + for name, digest in PINS.items(): + label, path = name.split('/', 1) + raw = (roots[label] / path).read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError(f'Pinned SHA-256 mismatch: {name}') + out[name] = json.loads(gzip.decompress(raw) if name.endswith('.gz') else raw) + return list(out.values()) + + +def invoice(word, caller): + ranks = list(map(len, word['frames'])) + main = set(word['live']) | {i+112 for i in word['live']} | set(word['hosted']['X2'] + word['hosted']['Y2']) + assert len(main) == 400 and word['public'] == 1501 and len(word['program']) == 76444 + paid, target = Counter(), Counter() + for op, role, *args in word['program']: + if op == 'MOVE': + src, dst, owned = args + assert owned == (role >= word['public']) and ranks[src] != ranks[dst] + paid[abs(ranks[src]-ranks[dst])] += 1 + for role, (src, dst) in enumerate(zip(word['initial'], word['final'], strict=True)): + if role not in main: + assert ranks[dst] > ranks[src] + target[ranks[dst]-ranks[src]] += 1 + stages = [event[1] for event in caller['events'] if event[0] == 'J'] + assert stages == list(range(1, 18)) + copies = len(stages) + P = Counter({rank:n*copies for rank,n in paid.items()}) + T = Counter({rank:n*copies for rank,n in target.items()}) + for spec in caller['types'].values(): + for sign, offset, *bits in spec['diagonal']: + assert sign == -1 and offset == 0 and len(bits) == copies and set(bits) <= {0, 1} + T[1+8*sum(bits)] += len(spec['ports']) + for kind, op, *args in (event for event in caller['events'] if event[0] != 'J'): + n = len(caller['types'][kind]['ports']) + if op == 'QUERY': + P[1] += n + elif op in ('IDLE_ONE','IDLE_ODD'): + P[8*len(args[1])+int(op=='IDLE_ODD')] += n + assert sum(P.values()) == 110553 and sum(T.values()) == 22461 + assert sum(r*(T[r]-P[r]) for r in T.keys()|P.keys()) == 1424 + return paid, target, P, T, copies + + +def round_interval(a, b): + a, b = a*GRID, b*GRID + return F(a.numerator//a.denominator, GRID), F(-((-b.numerator)//b.denominator), GRID) + + +@cache +def log_unit(x): + y = (x-1)/(x+1) + p = sum((2*y**j/j for j in range(1, 111, 2)), F(0)) + return round_interval(p, p+2*y**111/(111*(1-y*y))) + + +@cache +def power(rank, k): + e = rank.bit_length()-1 + lo,hi = [q+e*d for q,d in zip(log_unit(F(rank, 2**e)),log_unit(F(2)),strict=True)] + + def exp_negative(x, n): + term = total = F(1) + assert 0 <= x < 1 + for i in range(1,n+1): + term *= -x/i + total += term + return total + + return round_interval(rank*exp_negative(k*hi, 39), rank*exp_negative(k*lo, 40)) + + +def moment(P, T, k): + lower = upper = F(0) + for r in P.keys()|T.keys(): + n = T[r]-P[r] + lo,hi = power(r,k) + if n < 0: + lo,hi = hi,lo + lower += n*lo + upper += n*hi + return lower,upper + + +def slope(rank): + a,b = power(rank,TARGET) + c,d = power(rank-1,TARGET) + return a-d,b-c + + +def stock(paid, target, copies, baseline, paid_ranks, target_ranks): + eligible_paid = sorted(((slope(r)[1],r) for r in paid_ranks for _ in range(paid[r])),reverse=True) + eligible_target = sorted((slope(r)[0],r) for r in target_ranks for _ in range(target[r])) + price = F(0) + use_paid, use_target = Counter(), Counter() + for (upper,p),(lower,t) in zip(eligible_paid,eligible_target): + if upper <= lower: + break + price += upper-lower + use_paid[p] += 1 + use_target[t] += 1 + saving = copies*price + return {'eligible_paid':len(eligible_paid), 'eligible_targets':len(eligible_target), + 'selected_paid':dict(use_paid),'selected_targets':dict(use_target), + 'optimistic_pairs':sum(use_paid.values()), 'signed_saving_upper':str(saving), + 'signed_target_net_upper':str(baseline+saving)} + + +def run(old, peer, seconds): + deadline = monotonic()+seconds + before, before_receipt, caller, after, after_receipt = load(old,peer) + previous, next_ = invoice(before,caller), invoice(after,caller) + assert next_[4] == previous[4] == 17 + delta = lambda a,b:{r:a[r]-b[r] for r in a.keys()|b.keys() if a[r]!=b[r]} + assert delta(next_[0],previous[0]) == {4:1,5:-1} + assert delta(next_[1],previous[1]) == {8:1,9:-1} + result = {} + for name, (p,t,P,T,n), receipt, claim in zip(('7244','7274'),(previous,next_), + (before_receipt,after_receipt),CLAIMS,strict=True): + frozen = receipt['price']['after'] + assert P == {int(r):v for r,v in frozen['P'].items()} + assert T == {int(r):v for r,v in frozen['T'].items()} + # Known-good signed prices and a missing-call mutation. + removed_call = P.copy() + removed_call[1] -= 1 + assert removed_call != {int(r):v for r,v in frozen['P'].items()} + a,b = map(F,receipt['price']['price']['independent_raw_bracket']) + low, high = moment(P,T,a), moment(P,T,b) + assert low[0]>0 and high[1]<0 and a>claim + deficit = moment(P,T,TARGET) + scopes = {label:stock(p,t,n,deficit[1],pr,tr) for label,pr,tr in ( + ('same_delta',{5},{9}),('rank9_target',set(p)-{1},{9}), + ('any_one_step',set(p)-{1},set(t)-{1}))} + result[name]={'native_paid':dict(p),'native_target':dict(t),'paid':dict(P),'target':dict(T), + 'crossing_interval':[str(a),str(b)],'crossing_sign_controls':[str(low[0]),str(high[1])], + 'claim':str(claim),'target_raw_interval':list(map(str,deficit)),'scopes':scopes} + assert F(result['7244']['crossing_interval'][1]) < F(result['7274']['crossing_interval'][0]) + assert moment(previous[2],previous[3],CLAIMS[1])[1]<0 + assert monotonic()= public) + rank = relative(start, end) + gap = len(word["frames"][end]) - len(word["frames"][start]) + assert rank == abs(gap) > 0 and (owned or gap > 0) + bill[rank] += 1 + chart[r] = end + elif op == "INIT": + assert chart[r] is None and r >= public + chart[r] = args[0] + else: + assert all(chart[v] == args[-1] for v in roles(row)) + if op == "CLEAR": + assert r >= public + chart[r] = None + assert chart == word["final"] + [None] * word["owned_fields"] + return bill + + +def whole_contact_recount(events, word, relative, focus=frozenset(), shared=frozenset()): + public = word["public"] + dims = list(map(len, word["frames"])) + prior = {r: (-1, chart) for r, chart in enumerate(word["initial"])} + paid = Counter() + exterior = [] + edges = 0 + + def contact(role, clock, chart): + nonlocal edges + a, f = prior[role] + rank = relative(f, chart) + edges += 1 + if role < public: + assert rank == dims[chart] - dims[f] + if rank: + paid[rank] += 1 + if role in shared and ((a in focus) != (clock in focus)): + exterior.append(rank) + prior[role] = clock, chart + + for clock, row in events: + if row[0] == "INIT": + assert row[1] not in prior + prior[row[1]] = clock, row[-1] + else: + for role in roles(row): + contact(role, clock, row[-1]) + if row[0] == "CLEAR": + del prior[row[1]] + assert set(prior) == set(range(public)) + for role, chart in enumerate(word["final"]): + contact(role, len(word["program"]), chart) + assert edges == 137891 + return paid, tuple(sorted(exterior)) + + +def full_bill(word, caller, native, relative): + stages = [row[1] for row in caller["events"] if row[0] == "J"] + assert stages == list(range(1, 18)) + copies = len(stages) + main = set(word["live"]) | {r + 112 for r in word["live"]} | set( + word["hosted"]["X2"] + word["hosted"]["Y2"] + ) + assert len(main) == 400 + helpful = Counter(relative(a, b) for r, (a, b) in enumerate( + zip(word["initial"], word["final"], strict=True)) if r not in main) + assert sum(helpful.values()) == 1101 and 0 not in helpful + paid, productive = (Counter({r: n * copies for r, n in h.items()}) + for h in (native, helpful)) + for ty in caller["types"].values(): + for sign, offset, *bits in ty["diagonal"]: + assert (sign, offset, len(bits)) == (-1, 0, copies) + productive[1 + 8 * sum(bits)] += len(ty["ports"]) + for row in caller["events"]: + if row[0] == "J": + continue + ty, op, _, *args = row + ports = len(caller["types"][ty]["ports"]) + if op == "QUERY": + paid[1] += ports + elif op in ("IDLE_ONE", "IDLE_ODD"): + paid[8 * len(args[0]) + (op == "IDLE_ODD")] += ports + return paid, productive, copies + + +@cache +def log_interval(x): + z = (x - 1) / (x + 1) + partial = 2 * sum(z**i / i for i in range(1, 117, 2)) + return partial, partial + 2 * z**117 / (117 * (1 - z*z)) + + +def positive_exp_interval(x): + assert 0 <= x < 1 + term = total = F(1) + for n in range(1, 39): + term *= x / n + total += term + return total, total + term*x / (39 * (1-x/40)) + + +@cache +def tariff(rank, k): + if rank == 0: + return F(0), F(0) + e = rank.bit_length() - 1 + a, b = log_interval(F(rank, 1 << e)) + c, d = log_interval(F(2)) + grid = 10**50 + lo = rank / positive_exp_interval(k * (b + e*d))[1] + hi = rank / positive_exp_interval(k * (a + e*c))[0] + return F((grid*lo).__floor__(), grid), F((grid*hi).__ceil__(), grid) + + +def price(hist, k): + lower = upper = F(0) + for r, n in hist.items(): + lo, hi = tariff(r, k) + lower += n * (lo if n >= 0 else hi) + upper += n * (hi if n >= 0 else lo) + return lower, upper + + +def run(root, declared_file): + word, caller, early = read_inputs(root) + declared_raw = declared_file.read_bytes() + lead = json.loads(declared_raw) + assert lead["head"] == HEAD + assert {f"complex/source/{p}": h for p, h in PINS.items()}.items() <= lead["pins"].items() + assert not lead["unresolved"] and not lead["positives"] + k = F(early["price"]["independent_raw_bracket"][1]) + assert k == F(lead["crossing_upper"]) + frames = spaces(word["frames"]) + ranks = [len(frame).bit_length() - 1 for frame in frames] + + @cache + def relative(a, b): + if a == b: + return 0 + intersection = len(frames[a] & frames[b]) + assert intersection > 0 and intersection & (intersection - 1) == 0 + intersection_rank = intersection.bit_length() - 1 + return ranks[a] + ranks[b] - 2 * intersection_rank + + def rank(a, b): + return relative(min(a, b), max(a, b)) + + full = word["program"] + normalized = [(i, row) for i, row in enumerate(full) if row[0] != "MOVE"] + literal = literal_move_bill(full, word, rank) + reconstructed, _ = whole_contact_recount(normalized, word, rank) + assert literal == reconstructed and sum(literal.values()) == 6280 + omission = next(i for i, row in enumerate(full) if row[0] == "MOVE") + try: + literal_move_bill(full[:omission] + full[omission+1:], word, rank) + except AssertionError: + pass + else: + raise AssertionError("omitted paid MOVE accepted") + + paid, targets, copies = full_bill(word, caller, literal, rank) + frozen = early["invoice"] + assert {str(r): n for r, n in paid.items()} == frozen["P"] + assert {str(r): n for r, n in targets.items()} == frozen["T"] + assert sum(r * (targets[r] - paid[r]) for r in paid.keys() | targets.keys()) == frozen["S"] == 1424 + assert copies == lead["copies"] == 17 + baseline = targets.copy() + baseline.subtract(paid) + base_l, base_u = price(baseline, k) + assert F(lead["baseline_moment_interval"][0]) <= base_l <= base_u <= F(lead["baseline_moment_interval"][1]) < 0 + + rows = {tuple(event): row for row in lead["rows"] for event in row["events"]} + assert len(rows) == sum(len(r["events"]) for r in lead["rows"]) == 6 + census = Counter() + verified = [] + signatures = set() + for slot, ((ta, a), (tb, b)) in enumerate(pairwise(normalized)): + if a[0] != "ADD" or b[0] != "ADD": + continue + census["adjacent_add_add"] += 1 + if a[-1] == b[-1]: + continue + census["different_chart"] += 1 + shared = roles(a) & roles(b) + if not any(r >= word["public"] for r in shared): + continue + census["shared_owned"] += 1 + matrix_equal = commute(a, b) + if min(shared) < word["public"] or not matrix_equal: + census["excluded_commutation_or_public"] += 1 + continue + focus = {ta, tb} + prior, ext_old = whole_contact_recount(normalized, word, rank, focus, shared) + changed = normalized.copy() + changed[slot], changed[slot+1] = changed[slot+1], changed[slot] + successor, ext_new = whole_contact_recount(changed, word, rank, focus, shared) + assert prior == literal + delta = prior.copy() + delta.subtract(successor) + exterior_delta = Counter(ext_old) + exterior_delta.subtract(ext_new) + assert all(delta[r] == exterior_delta[r] for r in delta.keys() | exterior_delta.keys() if r) + quote = rows.pop((ta, tb)) + assert tuple(quote["old_exterior_ranks"]) == ext_old and tuple(quote["new_exterior_ranks"]) == ext_new + signatures.add((ext_old, ext_new)) + saving = {r: copies*n for r, n in delta.items() if n} + dl, du = price(saving, k) + assert F(quote["delta_price"][0]) <= dl <= du <= F(quote["delta_price"][1]) + next_paid, next_targets, _ = full_bill(word, caller, successor, rank) + assert next_targets == targets + next_signed = next_targets.copy() + next_signed.subtract(next_paid) + _, margin = price(next_signed, k) + assert margin <= F(quote["complete_margin_upper"]) < 0 + verified.append({"events":[ta,tb],"shared_roles":sorted(shared), + "old_exterior_ranks":ext_old,"new_exterior_ranks":ext_new, + "per_copy_old_minus_new":{r:n for r,n in delta.items() if n}, + "independent_complete_margin_upper":str(margin)}) + assert not rows and census == lead["counts"] and len(signatures) == lead["signature_count"] == 3 + assert len(verified) == 6 + return {"status":"PASS_INDEPENDENT_ROUND35_ADD_EXCHANGE", + "head":HEAD,"source_sha256":PINS,"lead_receipt_sha256":sha256(declared_raw).hexdigest(), + "crossing_upper":str(k),"counts":dict(census),"signature_count":len(signatures), + "original_native_paid":sum(literal.values()),"complete_paid":sum(paid.values()), + "complete_productive":sum(targets.values()),"original_margin_interval":[str(base_l),str(base_u)], + "verified":verified,"unresolved":0,"physical_site_tests":0, + "controls":["REJECT_OMITTED_LITERAL_PAID_MOVE"]} + + +if __name__ == "__main__": + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("source_root", type=Path) + parser.add_argument("lead_receipt", type=Path) + args = parser.parse_args() + alarm(90) + print(json.dumps(run(args.source_root, args.lead_receipt),indent=2,sort_keys=True)) + alarm(0) diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round36/cochart-audit/verify.py b/research/p104-charged-rank-six-support-bound/dependencies/round36/cochart-audit/verify.py new file mode 100644 index 0000000000..3ff0f20f7a --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round36/cochart-audit/verify.py @@ -0,0 +1,300 @@ +"""Independent rational audit of the 128 cocharted #7277 nominations.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +import gzip +from hashlib import sha256 +from itertools import groupby +import json +from pathlib import Path + +PINS = { + 'complex/source/inputs/WORD.json.gz': '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + 'complex/source/inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'complex/source/inputs/EARLY-RESULT.json': '691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7', +} + + +def load(path): + def unique(items): + result = dict(items) + assert len(result) == len(items) + return result + raw = path.read_bytes() + if path.suffix == '.gz': + raw = gzip.decompress(raw) + return json.loads(raw, object_pairs_hook=unique) + + +def put(row, k, x): + x += row.get(k,0) + if x: + row[k] = x + else: + row.pop(k,None) + + +def add(dst, src, a): + for k,x in src.items(): + put(dst,k,a*x) + + +def linear(rows, op, d, s, q, reverse=False): + if op in ('INIT','CLEAR'): + rows[d] = {} + elif op == 'SCALE': + rows[d] = {k:q*x for k,x in rows[d].items()} + elif op in ('ADD','COPY'): + if reverse: + add(rows[s], dict(rows[d]) if s==d else rows[d], q) + if op=='COPY': + assert s != d + rows[d] = {} + elif op == 'COPY': + rows[d] = {k:q*x for k,x in rows[s].items()} + else: + add(rows[d], dict(rows[s]) if s==d else rows[s], q) + + +def pure_images(rows, current, group): + # Coefficient-elimination order is independent of the lead checker. + # Carry the complete image vector and eliminate greatest exterior + # coordinate first, leaving an image basis spanning the pure image. + exterior, interior = {}, {} + for role in sorted(current, reverse=True): + residual = rows[role].copy() + while (lead := max((k for k in residual if k not in group), default=-1)) >= 0: + if lead not in exterior: + exterior[lead] = residual + break + old = exterior[lead] + add(residual, old, -residual[lead]/old[lead]) + else: + while residual: + lead = max(residual) + if lead not in interior: + interior[lead] = residual + break + old = interior[lead] + add(residual, old, -residual[lead]/old[lead]) + return tuple(interior.values()) + + +def binary_span(rows): + space = {0} + for row in rows: + assert row not in space + space |= {row^x for x in space} + return space + + +def geometry(word): + public = word['public'] + main = set(word['live']) | {r+112 for r in word['live']} + for hosted in ('X2','Y2'): + main.update(word['hosted'][hosted]) + assert len(main)==400 and public==1501 + starts, ends = word['initial'], word['final'] + spaces = list(map(binary_span,word['frames'])) + ranks = list(map(len,word['frames'])) + groups = defaultdict(set) + helpers = {} + for role,(a,b) in enumerate(zip(starts,ends,strict=True)): + if role not in main: + assert spaces[a] < spaces[b] + groups[a,b].add(role) + helpers[role] = (a,b) + chart = starts + [None]*word['owned_fields'] + at = defaultdict(set) + for role,frame in enumerate(starts): + at[frame].add(role) + tape, cuts, contexts = [], defaultdict(list), {} + paid = Counter() + for t,(op,d,*args) in enumerate(word['program']): + s,q = d,None + if op == 'MOVE': + a,b,owned = args + assert chart[d]==a and owned==(d>=public) + assert spaces[a]b[1] for a,b in zip(by_price,by_price[1:])) + assert all(lo+gain[0]>0 for _,_,gain in ranked[:128]) + return [key for key,_,_ in ranked[:128]],sum(p.values()),sum(t.values()) + + +def test_cut(): + assert pure_images([{0:Q(1),2:Q(1)},{1:Q(1),2:Q(1)}],(0,1),{0,1}) == ({0:Q(1),1:Q(-1)},) + assert pure_images([{2:Q(1)},{2:Q(1)}],(0,1),{0,1}) == () + assert pure_images([{0:Q(1)},{1:Q(1)}],(0,1),{0,1}) + + +def run(root, receipts): + paths = {str(root/p):h for p,h in PINS.items()} + assert all(sha256(Path(p).read_bytes()).hexdigest()==h for p,h in paths.items()) + word,caller,early = (load(root/p) for p in PINS) + inventory,search = (load(receipts/name) for name in ('INVENTORY.json','SEARCH.json')) + assert search['candidate'] is None and search['phase']=='exhausted_nominations' + ranks,helpers,groups,tape,cuts,contexts,native = geometry(word) + keys,paid,productive = price(ranks,helpers,native,caller,early,cuts,inventory) + selected = {tuple(row['key']):row for row in search['selected']} + assert list(selected)==keys + test_cut() + schedule = defaultdict(list) + counts = defaultdict(Counter) + for key in keys: + for t in cuts[key]: + schedule[t].append(key) + n = word['public'] + def basis(): + return [{i:Q(1)} for i in range(n)]+[{} for _ in range(word['owned_fields'])] + forward = basis() + surviving = defaultdict(list) + for t,(op,d,s,q) in enumerate(tape): + linear(forward,op,d,s,q) + for a,b,f in schedule.get(t,()): + k = (a,b,f) + image = pure_images(forward,contexts[t,f],groups[a,b]) + counts[k]['prefix_checked'] += 1 + if image: + counts[k]['prefix_nonzero'] += 1 + surviving[t].append((k,image)) + assert all(forward[r]=={r:Q(1)} for r in helpers) + backward = basis() + for t in reversed(range(len(tape))): + for (a,b,f),prefix in surviving.get(t,()): + k = (a,b,f) + suffix = pure_images(backward,contexts[t,f],groups[a,b]) + counts[k]['suffix_checked'] += 1 + for c in prefix: + for d in suffix: + assert not sum(v*d.get(i,0) for i,v in c.items()), (t,k,c,d) + linear(backward,*tape[t],reverse=True) + for key,count in counts.items(): + assert all(value==selected[key].get(name,0) for name,value in count.items()) + assert selected[key]['cuts']==count['prefix_checked'] + assert len(counts)==128 and len(cuts)-128==search['outside_signature_cap'] + totals = sum(counts.values(),Counter()) + return {'status':'PASS_INDEPENDENT_RATIONAL_COCHART_AUDIT', + 'head':inventory['head'],'pins':PINS | {f'incremental/run/{name}':sha256((receipts/name).read_bytes()).hexdigest() for name in ('INVENTORY.json','SEARCH.json')}, + 'paid':paid,'productive':productive,'scope':len(cuts),'selected':len(counts), + 'outside_cap':len(cuts)-len(counts),'totals':dict(totals),'nonzero_pairs':0, + 'controls':['MIXED_OUTSIDE_CANCELLATION','ZERO_IMAGE_NOT_CREDITED','PURE_BASIS_POSITIVE']} + + +if __name__=='__main__': + assert __debug__ + parser = ArgumentParser() + parser.add_argument('dependency_root',type=Path) + parser.add_argument('receipt_directory',type=Path) + a = parser.parse_args() + print(json.dumps(run(a.dependency_root,a.receipt_directory),sort_keys=True,indent=2)) diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round36/incremental/predecessor_split.py b/research/p104-charged-rank-six-support-bound/dependencies/round36/incremental/predecessor_split.py new file mode 100644 index 0000000000..f1c7609653 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round36/incremental/predecessor_split.py @@ -0,0 +1,155 @@ +"""Split independent helper jobs with three scalar basis changes. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Adapted for arbitrary counted owned-field inventory by @CubeJerry with OpenAI assistance. +Successor: OpenAI Codex for dillona excludes both hosted main planes from helper groups. +The source word and caller retain the credits in README.md. +Successors: dillona/OpenAI Codex choose a small smooth swap entry when pivot is zero; +then also when a nonzero pivot has a nonunit reciprocal, preserving the native alphabet. +""" +from copy import deepcopy +from fractions import Fraction as Q +from support import L + + +def inverse(program): + return [[e[0], *e[1:-2], + str(1/Q(e[-2]) if e[0] == 'SCALE' else -Q(e[-2])), e[-1]] + for e in reversed(program)] + + +def basis(a, b, pivot, frame): + """Return B with row pivot equal to a and B b equal to e_pivot.""" + L.need(sum(v*b.get(k, 0) for k, v in a.items()) == 1, 'Unit basis pairing') + roles = sorted(set(a) | set(b) | {pivot}) + values, program = dict(b), [] + + def emit(event): + program.append(event) + r, q = event[1], Q(event[-2]) + if event[0] == 'SCALE': + values[r] = values.get(r, 0)*q + else: + values[r] = values.get(r, 0)+q*values.get(event[2], 0) + + def swap_score(r): + q=b[r] + def smooth(x): + for prime in (2,3,5): + while x%prime==0:x//=prime + return x==1 + return (not(smooth(abs(q.numerator)) and smooth(q.denominator)), + abs(q.numerator).bit_length()+q.denominator.bit_length(),r) + j = pivot if b.get(pivot) and not swap_score(pivot)[0] else min((r for r in roles if b.get(r)),key=swap_score) + if j != pivot: + for event in [['ADD', pivot, j, '1', frame], + ['ADD', j, pivot, '-1', frame], + ['ADD', pivot, j, '1', frame], + ['SCALE', j, '-1', frame]]: + emit(event) + if values[pivot] != 1: + emit(['SCALE', pivot, str(1/values[pivot]), frame]) + for r in roles: + if r != pivot and values.get(r): + emit(['ADD', r, pivot, str(-values[r]), frame]) + L.need(all(values.get(r, 0) == int(r == pivot) for r in roles), 'Basis column') + inverse_rows = {r: {r: Q(1)} for r in roles} + for e in inverse(program): + if e[0] == 'SCALE': + inverse_rows[e[1]] = {k: Q(e[-2])*v for k, v in inverse_rows[e[1]].items()} + else: + L.add(inverse_rows[e[1]], inverse_rows[e[2]], Q(e[-2])) + row = {} + for r, q in a.items(): + L.add(row, inverse_rows[r], q) + L.need(row[pivot] == 1, 'Basis row coefficient') + for r in roles: + if r != pivot and row.get(r): + program.append(['ADD', pivot, r, str(row[r]), frame]) + return program + + +def check_cut(word, h): + """Check the whole prefix row and suffix column over the rationals.""" + n, cut, f, p = word['public'], h['cut_after'], h['frame'], h['pivot'] + a, b, c, d = ({int(k): Q(v) for k, v in h[s].items()} for s in ('a', 'b', 'c', 'd')) + main = set(word['live']) | {r+112 for r in word['live']} | set(word['hosted']['X2']) | set(word['hosted']['Y2']) + L.need(p < n and p not in main, 'A helper supplies the retained output role') + u, v = word['initial'][p], word['final'][p] + group = {r for r in range(n) if r not in main and + (word['initial'][r], word['final'][r]) == (u, v)} + L.need(set(c) | set(d) <= group, 'Both boundary vectors use one helper group') + L.need(L.span(word['frames'][u]) < L.span(word['frames'][f]) < L.span(word['frames'][v]), + 'Two strictly productive nested targets') + L.need(h['ranks'] == [len(word['frames'][f])-len(word['frames'][u]), + len(word['frames'][v])-len(word['frames'][f])], 'Declared split ranks') + rows = [{r: Q(1)} if r < n else {} for r in range(n+word['owned_fields'])] + current = word['initial']+[None]*word['owned_fields'] + for e in word['program'][:cut+1]: + op, r = e[:2] + if op == 'MOVE': + current[r] = e[3] + elif op in ('INIT', 'CLEAR'): + rows[r] = {} + current[r] = e[2] if op == 'INIT' else None + elif op == 'SCALE': + rows[r] = {k: Q(e[-2])*x for k, x in rows[r].items()} + elif op == 'COPY': + rows[r] = {k: Q(e[-2])*x for k, x in rows[e[2]].items()} + else: + L.add(rows[r], rows[e[2]], Q(e[-2])) + L.need(all(current[r] == f for r in set(a) | set(b) | {p}), 'One intermediate chart') + total = {} + for r, q in a.items(): + L.add(total, rows[r], q) + L.need(total == c, 'Exact prefix functional; no other input') + column = [b.get(r, Q(0)) for r in range(n+word['owned_fields'])] + for e in word['program'][cut+1:]: + op, r = e[:2] + if op in ('INIT', 'CLEAR'): + column[r] = Q(0) + elif op == 'SCALE': + column[r] *= Q(e[-2]) + elif op == 'COPY': + column[r] = Q(e[-2])*column[e[2]] + elif op == 'ADD': + column[r] += Q(e[-2])*column[e[2]] + L.need(column == [d.get(r, Q(0)) for r in range(n+word['owned_fields'])], 'Exact suffix direction; no other output') + L.need(sum(x*b.get(r, 0) for r, x in a.items()) == + sum(x*d.get(r, 0) for r, x in c.items()) == 1, 'Both independent pairings') + return a, b, c, d + + +def split(word, h): + a, b, c, d = check_cut(word, h) + n, p, f, cut = word['public'], h['pivot'], h['frame'], h['cut_after'] + u, v = word['initial'][p], word['final'][p] + + def shift_owned(event): + e = event.copy() + e[1] += int(e[1] >= n) + if e[0] in ('ADD', 'COPY'): + e[2] += int(e[2] >= n) + return e + + def use_successor(event): + e = event.copy() + if e[1] == p: + e[1] = n + if e[0] in ('ADD', 'COPY') and e[2] == p: + e[2] = n + return e + + boundary, middle = basis(c, d, p, u), basis(a, b, p, f) + out = deepcopy(word) + out['public'] = n+1 + out['initial'].append(f) + out['final'].append(v) + out['final'][p] = f + out['program'] = inverse(boundary) + out['program'] += [shift_owned(e) for e in word['program'][:cut+1]] + out['program'] += [shift_owned(e) for e in middle] + out['program'] += [use_successor(shift_owned(e)) for e in inverse(middle)] + out['program'] += [use_successor(shift_owned(e)) for e in word['program'][cut+1:]] + out['program'] += [use_successor([*e[:-1], v]) for e in boundary] + return out diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round36/incremental/support.py b/research/p104-charged-rank-six-support-bound/dependencies/round36/incremental/support.py new file mode 100644 index 0000000000..192cd38d27 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round36/incremental/support.py @@ -0,0 +1,18 @@ +"""Small exact sparse operations, retained from Ali Romman/CubeJerry. Apache-2.0.""" +class L: + @staticmethod + def need(ok, why): + if not ok: raise ValueError(why) + @staticmethod + def add(dst, src, q): + for k,v in tuple(src.items()): + value=dst.get(k,0)+q*v + if value: dst[k]=value + else: dst.pop(k,None) + @staticmethod + def span(basis): + out={0} + for v in basis: + L.need(type(v) is int and 0 1: + hits.extend(candidates(word, roles, entry, exit_frame)) + tested += 1 + print(json.dumps(encode({'tested_boundary_groups':tested, 'candidates':hits}), sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round37/preflight/PRICE.json.gz b/research/p104-charged-rank-six-support-bound/dependencies/round37/preflight/PRICE.json.gz new file mode 100644 index 0000000000..59922aea1f Binary files /dev/null and b/research/p104-charged-rank-six-support-bound/dependencies/round37/preflight/PRICE.json.gz differ diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round37/preflight/price.py b/research/p104-charged-rank-six-support-bound/dependencies/round37/preflight/price.py new file mode 100644 index 0000000000..3e25394050 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round37/preflight/price.py @@ -0,0 +1,97 @@ +"""Price existing-chart rank-one endpoint extensions before scalar support.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import runpy + +PINS = { + 'complex/audit.py':'67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb', + 'complex/source/inputs/WORD.json.gz':'2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + 'complex/source/inputs/EARLY-RESULT.json':'691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7', + 'complex/source/inputs/CALLER.json':'255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'complex/source/powers.py':'c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee', +} + + +def space(rows): + span = {0} + for row in rows: + assert row not in span + span |= {v^row for v in span} + return span + + +def screen(root): + for name, digest in PINS.items(): + assert sha256((root/name).read_bytes()).hexdigest()==digest, name + source=root/'complex/source' + w=json.loads(gzip.decompress((source/'inputs/WORD.json.gz').read_bytes())) + audit=runpy.run_path(str(root/'complex/audit.py')) + _,_,_,_,_,_,copies,paid,targets,_=audit['read_model']() + assert copies==17 + k=Q(json.loads((source/'inputs/EARLY-RESULT.json').read_bytes())['price']['independent_raw_bracket'][1]) + power=cache(runpy.run_path(str(source/'powers.py'))['power']) + def moment(net): + terms=[sorted(n*x for x in power(r,k)) for r,n in net.items() if n] + return tuple(sum(t[i] for t in terms) for i in (0,1)) + signed=targets.copy() + signed.subtract(paid) + baseline=moment(signed) + assert baseline[1]<0 + dims=list(map(len,w['frames'])) + spaces=[space(v) for v in w['frames']] + main=set(w['live'])|{r+112 for r in w['live']}|set(w['hosted']['X2']+w['hosted']['Y2']) + roles=defaultdict(list) + for h,(u,v) in enumerate(zip(w['initial'],w['final'],strict=True)): + if h not in main: + assert spaces[u]=2 and b>=2 + delta=Counter((a,b)) + delta[r]-=1 + delta[1]-=1 + assert sum(n*j for j,n in delta.items())==0 + return moment({j:copies*n for j,n in delta.items()}) + for (u,v),helpers in sorted(roles.items()): + r=dims[v]-dims[u] + if not 3<=r<=8: + continue + start=[('input',f,v) for f in frames[dims[u]-1] if spaces[f]0 + stock.append({'side':side,'prior':[u,v],'new':[a0,b0], + 'old_rank':r,'parts':[a,b],'extender_roles':helpers, + 'new_cohort_before_extension':roles.get((a0,b0),[]), + 'complete_margin_interval':[str(baseline[0]+lo),str(baseline[1]+hi)], + 'margin_lower':lo}) + stock.sort(key=lambda r:(-r['margin_lower'],r['side'],r['prior'],r['new'],r['parts'])) + for row in stock: + row.pop('margin_lower') + return {'head':audit['HEAD'],'source_pins':PINS,'copies':copies,'crossing_upper':str(k), + 'baseline_moment_interval':list(map(str,baseline)),'typed_signatures':len(stock), + 'rank_hist':dict(Counter(r['old_rank'] for r in stock)), + 'side_hist':dict(Counter(r['side'] for r in stock)), + 'all_source_helpers':sum(map(len,roles.values())),'rows':stock, + 'physical_sites':0,'support_tested':0} + + +if __name__=='__main__': + parser=ArgumentParser() + parser.add_argument('root',type=Path) + args=parser.parse_args() + print(json.dumps(screen(args.root),indent=2,sort_keys=True)) diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round38/incremental/screen.py b/research/p104-charged-rank-six-support-bound/dependencies/round38/incremental/screen.py new file mode 100644 index 0000000000..0e0938e7e6 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round38/incremental/screen.py @@ -0,0 +1,299 @@ +"""Rational support of charged endpoint splits on the literal #7277 word.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import runpy +import sys +from time import monotonic + +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +WORD = 'complex/source/inputs/WORD.json.gz' +PINS = { + 'round30/'+WORD: '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + 'round37/preflight/PRICE.json': 'bc6134776a077b4ae3ef595c6000563062b2a42a3684a3852ba4f2f77b8dc726', + 'round36/cochart-audit/verify.py': '58cab0bb2f24fe29d0e190cbe3cc0dc85f889ec4af66b5a02328d1e1d0e37e8a', + 'round36/incremental/predecessor_split.py': '999b9eeabe5cd1a7e3ec014d1a449f850b4ac9bfb19749cddef41ae12cd0b405', + 'round36/incremental/support.py': 'f3e6eeb879480715c5c32c1a390a63c57d26ea1c9a9cbdb89b83ca34260e47f6', +} + + +def read_json(raw): + def unique(items): + result = dict(items) + assert len(result)==len(items),'Duplicate keys' + return result + return json.loads(raw,object_pairs_hook=unique) + + +def save(out,name,receipt): + path = out/(name+'.tmp') + path.write_text(json.dumps(receipt,indent=2,sort_keys=True)+'\n') + path.replace(out/name) + + +def dot(a,b): + return sum(x*b.get(i,0) for i,x in a.items()) + + +def pure_coefficients(rows, roles, group, add): + exterior, output = {}, [] + for role in reversed(roles): + residual = rows[role].copy() + coefficients = {role:Q(1)} + while (lead:=max((k for k in residual if k not in group),default=-1))>=0: + if lead not in exterior: + exterior[lead] = residual,coefficients + break + old,co = exterior[lead] + scale = -residual[lead]/old[lead] + add(residual,old,scale) + add(coefficients,co,scale) + else: + output.append((residual,coefficients)) + return output + + +def admissible(program): + def smooth(n): + for p in (2,3,5): + while n%p==0: + n//=p + return n==1 + for op,*e in program: + q = Q(e[-2]) + if not q or not smooth(q.denominator) or op=='SCALE' and not smooth(abs(q.numerator)): + return False + return True + + +def nominate(word, side, extender, new, t, frame, pivot, ranks, a,b,c,d, check): + u,v = new + changed = dict(word,initial=word['initial'].copy(),final=word['final'].copy()) + if side=='input': + prior = changed['initial'][extender] + changed['initial'][extender] = u + changed['program'] = [['MOVE',extender,u,prior,False]]+word['program'] + else: + prior = changed['final'][extender] + changed['final'][extender] = v + changed['program'] = word['program']+[['MOVE',extender,prior,v,False]] + h = dict(cut_after=t+(side=='input'),frame=frame,pivot=pivot,ranks=ranks) + h.update({name:{str(i):str(q) for i,q in vector.items()} for name,vector in zip('abcd',(a,b,c,d),strict=True)}) + check(changed,h) + return dict(extender=extender,side=side,new=new,original_cut=t,split=h,added_move=changed['program'][0 if side=='input' else -1]) + + +def run(roots,out,seconds): + start = monotonic() + files = {} + for name,digest in PINS.items(): + prefix,p = name.split('/',1) + path = roots[prefix]/p + assert sha256(path.read_bytes()).hexdigest()==digest,name + files[name] = path + word = read_json(gzip.decompress(files['round30/'+WORD].read_bytes())) + receipt = read_json(files['round37/preflight/PRICE.json'].read_bytes()) + predecessor = runpy.run_path(str(files['round36/cochart-audit/verify.py'])) + sys.path.insert(0,str(roots['round36']/'incremental')) + from predecessor_split import basis, check_cut + space,linear,add = (predecessor[name] for name in ('binary_span','linear','add')) + pure_images = predecessor['pure_images'] + assert receipt['head']==HEAD and receipt['copies']==17 and receipt['typed_signatures']==777 + rows = [r for r in receipt['rows'] if r['old_rank']==7] + assert len(rows)==90 + assert all(Q(r['complete_margin_interval'][0])>0 for r in rows) + n,tape = word['public'],word['program'] + spaces = list(map(space,word['frames'])) + dims = list(map(len,word['frames'])) + main = set(word['live']) | {i+112 for i in word['live']} + main.update(word['hosted']['X2']) + main.update(word['hosted']['Y2']) + groups = defaultdict(set) + for i,(a,b) in enumerate(zip(word['initial'],word['final'],strict=True)): + if i not in main: + groups[a,b].add(i) + options = defaultdict(dict) + typed = defaultdict(list) + for row in rows: + side = row['side'] + a,b = row['prior'] + u,v = row['new'] + g = groups[u,v] + assert set(row['new_cohort_before_extension'])==g + assert groups[a,b]==set(row['extender_roles']) and not g&groups[a,b] + assert (b==v and spaces[u]=n) + assert spaces[a]=seconds: + return checkpoint('prefix_cap',t) + linear(forward,*e) + for key,f,roles in schedule.get(t,()): + pp = pure_images(forward,roles,universe[key]) + bump(key,'prefix_checked') + if pp: + snaps[t].append((key,f,roles,pp)) + bump(key,'prefix_nonzero') + if t%4096==0: + checkpoint('prefix',t) + assert all(forward[i]=={i:Q(1)} for i in set().union(*universe.values())) + backward = identity() + for t in reversed(range(len(decoded))): + if monotonic()-start>=seconds: + return checkpoint('suffix_cap',t) + for key,f,roles,pp in snaps.get(t,()): + ss = pure_images(backward,roles,universe[key]) + bump(key,'suffix_checked') + if not any(dot(c,d) for c in pp for d in ss): + continue + bump(key,'union_nonzero') + # Recover the exact prefix only at cuts surviving the union test. + local = identity() + for e in decoded[:t+1]: + linear(local,*e) + pivot_stock = set(roles) + u,v = key[:2] + g = groups[u,v] + for extender,row in options[key].items(): + if monotonic()-start>=seconds: + unresolved.append(dict(clock=t,frame=f,endpoints=key[:2],parts=key[2:],reason='extender_cap')) + return checkpoint('extender_cap',t) + group = g|{extender} + pivots = sorted(pivot_stock&group) + if not pivots: + continue + cc = pure_coefficients(local,roles,group,add) + dd = pure_coefficients(backward,roles,group,add) + bump(key,'exact_extender_checked') + nonzero = False + for c,a in cc: + for d,b in dd: + paired = dot(c,d) + if not paired: + continue + nonzero = True + if dot(a,b)!=paired: + continue + for scale in (Q(1),paired,Q(-1)): + aa = {i:q/scale for i,q in a.items()} + co = {i:q/scale for i,q in c.items()} + bb = {i:q*scale/paired for i,q in b.items()} + do = {i:q*scale/paired for i,q in d.items()} + for pivot in pivots: + try: + ops = basis(aa,bb,pivot,f)+basis(co,do,pivot,u) + except ValueError: + continue + if admissible(ops): + candidate = nominate(word,row['side'],extender,(u,v),t,f,pivot, + [dims[f]-dims[u],dims[v]-dims[f]],aa,bb,co,do,check_cut) + candidate['price_margin'] = row['complete_margin_interval'] + return checkpoint('witness',t) + if nonzero: + unresolved.append(dict(clock=t,frame=f,endpoints=key[:2],parts=key[2:],extender=extender,reason='no_admissible_basis_pair')) + linear(backward,*decoded[t],reverse=True) + if t%4096==0: + checkpoint('suffix',t) + checkpoint('exhausted' if not unresolved else 'unresolved_basis_pairs',0) + + +if __name__=='__main__': + assert __debug__ + p = ArgumentParser() + p.add_argument('round30',type=Path) + p.add_argument('round36',type=Path) + p.add_argument('round37',type=Path) + p.add_argument('out',type=Path) + p.add_argument('--seconds',type=int,default=175) + a = p.parse_args() + a.out.mkdir() + run({k:getattr(a,k) for k in ('round30','round36','round37')},a.out,a.seconds) diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round49/NEXT.md b/research/p104-charged-rank-six-support-bound/dependencies/round49/NEXT.md new file mode 100644 index 0000000000..1b9a4cda7b --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round49/NEXT.md @@ -0,0 +1,35 @@ +# Next incremental gate after Round 49 + +Pivot from paid public MOVE contacts to productive helper credit. +Recheck exact #7277 and #7113 and compare pending #7303 (fixed-word +singleton splits), #7142 (funded endpoint proof), plus the latest +open, merged, archive and Discussion coverage. Rounds 37–38 closed +the rank-eight and rank-seven typed scopes. Test only rank-six to +rank-seven charged endpoint extensions with productive partition 3+4. +Keep the literal chart/ownership chronology outside the extension. + +The authenticated Round 37 price receipt `preflight/PRICE.json` +(SHA-256 `bc6134776a077b4ae3ef595c6000563062b2a42a3684a3852ba4f2f77b8dc726`) +has 83 such signatures. It grants a productive replacement of rank 6 +by 3 and 4 and charges one new paid rank-one child in each of the +17 signed native copies. The recorded complete directed lower margin +at the old crossing upper is exactly +`1835166431152278266166310959958201126735264211/15625000000000000000000000000000000000000000000` +(about 0.1174506515937458 raw), before any other ordinary or physical +changes. Treat alternatives separately unless compatibility is proved. + +First implementation step: copy the sealed Round 38 +`incremental/screen.py` into the new isolated artifact and select only +`old_rank == 6` with `parts == [3,4]`. Update the verified stock +assertions to 83 and target rank seven, derive cohort counts from the +literal inputs, and retain the Round 36 cochart and exact support pins. +Rebuild the complete invoice and save a priced inventory before signed +prefix/suffix decoding. Use the existing exact necessary union test +and refine any nonzero union result to one literal extender and an +exact pair of legal basis vectors. Cap at 83 signatures or 120 runner +seconds, including a 115-second checkpoint. Allow at most one survivor +full physical validation within the current discovery reserve. Advance +only after a positive fully charged invoice, exact arbitrary-input +forward and adjoint, ownership and restoration, fresh grid, precision, +tape and complete independent caller/outer replay. If exhausted or +capped without a support witness, save exact unvisited keys and pivot. diff --git a/research/p104-charged-rank-six-support-bound/dependencies/round50/lead/screen.py b/research/p104-charged-rank-six-support-bound/dependencies/round50/lead/screen.py new file mode 100644 index 0000000000..3ccb707821 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/dependencies/round50/lead/screen.py @@ -0,0 +1,376 @@ +"""Exact rank-six to rank-seven, 3+4 charged endpoint support gate.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import runpy +from signal import SIGALRM, alarm, signal +import sys +from time import monotonic + +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +WORD = 'complex/source/inputs/WORD.json.gz' +PINS = { + 'round30/'+WORD: '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + 'round30/complex/audit.py': '67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb', + 'round30/complex/source/powers.py': 'c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee', + 'round30/complex/source/inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'round30/complex/source/inputs/EARLY-RESULT.json': '691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7', + 'round37/preflight/price.py': '8b1b345bd4a2732c74251c1b95d47f98cd37184894d8979a6ef1953d38686be8', + 'round38/incremental/screen.py': '43a74344555088b016a3fb857b7c86de3f2880ef85b77846c4362037779b8405', + 'round49/NEXT.md': 'f304c5b62077e43d35696d939a0f96f420a30cc8173fc97978c4e54d867ff86f', + 'round37/preflight/PRICE.json': 'bc6134776a077b4ae3ef595c6000563062b2a42a3684a3852ba4f2f77b8dc726', + 'round36/cochart-audit/verify.py': '58cab0bb2f24fe29d0e190cbe3cc0dc85f889ec4af66b5a02328d1e1d0e37e8a', + 'round36/incremental/predecessor_split.py': '999b9eeabe5cd1a7e3ec014d1a449f850b4ac9bfb19749cddef41ae12cd0b405', + 'round36/incremental/support.py': 'f3e6eeb879480715c5c32c1a390a63c57d26ea1c9a9cbdb89b83ca34260e47f6', +} + + +def read_json(raw): + def unique(items): + result = dict(items) + assert len(result)==len(items),'Duplicate keys' + return result + return json.loads(raw,object_pairs_hook=unique) + + +def save(out,name,receipt): + path = out/(name+'.tmp') + path.write_text(json.dumps(receipt,indent=2,sort_keys=True)+'\n') + path.replace(out/name) + + +def dot(a,b): + return sum(x*b.get(i,0) for i,x in a.items()) + + +def pure_coefficients(rows, roles, group, add): + exterior, output = {}, [] + for role in reversed(roles): + residual = rows[role].copy() + coefficients = {role:Q(1)} + while (lead:=max((k for k in residual if k not in group),default=-1))>=0: + if lead not in exterior: + exterior[lead] = residual,coefficients + break + old,co = exterior[lead] + scale = -residual[lead]/old[lead] + add(residual,old,scale) + add(coefficients,co,scale) + else: + output.append((residual,coefficients)) + return output + + +def admissible(program): + def smooth(n): + for p in (2,3,5): + while n%p==0: + n//=p + return n==1 + for op,*e in program: + q = Q(e[-2]) + if not q or not smooth(q.denominator) or op=='SCALE' and not smooth(abs(q.numerator)): + return False + return True + + +def nominate(word, side, extender, new, t, frame, pivot, ranks, a,b,c,d, check): + u,v = new + changed = dict(word,initial=word['initial'].copy(),final=word['final'].copy()) + if side=='input': + prior = changed['initial'][extender] + changed['initial'][extender] = u + changed['program'] = [['MOVE',extender,u,prior,False]]+word['program'] + else: + prior = changed['final'][extender] + changed['final'][extender] = v + changed['program'] = word['program']+[['MOVE',extender,prior,v,False]] + h = dict(cut_after=t+(side=='input'),frame=frame,pivot=pivot,ranks=ranks) + h.update({name:{str(i):str(q) for i,q in vector.items()} for name,vector in zip('abcd',(a,b,c,d),strict=True)}) + check(changed,h) + return dict(extender=extender,side=side,new=new,original_cut=t,split=h,added_move=changed['program'][0 if side=='input' else -1]) + + +def controls(predecessor): + add, images = predecessor['add'], predecessor['pure_images'] + rows = [{0:Q(1),3:Q(1)}, {3:Q(1)}, {1:Q(-2)}] + assert images(rows,[0,1],{0}) and not images(rows,[0,1],{1}) + (image,coefficients), = pure_coefficients(rows,[0,1],{0},add) + assert set(image)=={0} and abs(image[0])==1 + assert set(coefficients)=={0,1} + assert dot(image,{0:Q(2)}) and not dot(image,rows[2]) + assert admissible([['ADD',0,1,'-7/15',0],['SCALE',1,'-3/10',0]]) + assert not admissible([['ADD',0,1,'1/7',0]]) + assert not admissible([['SCALE',1,'7/10',0]]) + return ['exterior_cancellation_recovers_pure_image','outside_only_bank_excluded', + 'signed_pairing_positive_and_zero','native_basis_coefficient_controls'] + + +def authenticate(roots): + files = {} + for name,digest in PINS.items(): + prefix,p = name.split('/',1) + path = roots[prefix]/p + assert sha256(path.read_bytes()).hexdigest()==digest,name + files[name] = path + return files + + +def run(roots,out,seconds,price_only=False): + start = monotonic() + deadline = start + min(115,seconds-1) + files = authenticate(roots) + word = read_json(gzip.decompress(files['round30/'+WORD].read_bytes())) + receipt = read_json(files['round37/preflight/PRICE.json'].read_bytes()) + predecessor = runpy.run_path(str(files['round36/cochart-audit/verify.py'])) + sys.path.insert(0,str(roots['round36']/'incremental')) + from predecessor_split import basis, check_cut + space,linear,add = (predecessor[name] for name in ('binary_span','linear','add')) + pure_images = predecessor['pure_images'] + assert receipt['head']==HEAD and receipt['copies']==17 and receipt['typed_signatures']==777 + price_model = runpy.run_path(str(files['round37/preflight/price.py'])) + rebuilt = price_model['screen'](roots['round30']) + assert json.loads(json.dumps(rebuilt)) == receipt + rows = [r for r in receipt['rows'] if r['old_rank']==6 and r['parts']==[3,4]] + assert len(rows)==83 and Counter(r['side'] for r in rows)=={'input':50,'output':33} + assert all(Q(r['complete_margin_interval'][0])== + Q('1835166431152278266166310959958201126735264211/15625000000000000000000000000000000000000000000') + for r in rows) + save(out,'PRICE.json',dict(head=HEAD,pins=PINS,crossing_upper=receipt['crossing_upper'], + baseline_interval=receipt['baseline_moment_interval'],copies=17,selected_signatures=len(rows), + paid_rank_delta={1:17},productive_rank_delta={3:17,4:17,6:-17}, + complete_margin_interval_per_alternative=rows[0]['complete_margin_interval'], + alternatives=rows,grant='One alternative at a time. Additional ordinary and physical costs free only in this upper.')) + checks = controls(predecessor) + if price_only: + return + n,tape = word['public'],word['program'] + spaces = list(map(space,word['frames'])) + dims = list(map(len,word['frames'])) + main = set(word['live']) | {i+112 for i in word['live']} + main.update(word['hosted']['X2']) + main.update(word['hosted']['Y2']) + groups = defaultdict(set) + for i,(a,b) in enumerate(zip(word['initial'],word['final'],strict=True)): + if i not in main: + groups[a,b].add(i) + options = defaultdict(dict) + typed = defaultdict(list) + for row in rows: + side = row['side'] + a,b = row['prior'] + u,v = row['new'] + g = groups[u,v] + assert set(row['new_cohort_before_extension'])==g + assert groups[a,b]==set(row['extender_roles']) and not g&groups[a,b] + assert (b==v and spaces[u]=deadline: + return save(out,'SUPPORT.json',dict(head=HEAD,phase='inventory_cap',clock=t, + candidate=None,unresolved_signatures=rows,controls=checks)) + src,q = dst,None + if op=='MOVE': + a,b,owned = args + assert chart[dst]==a and owned==(dst>=n) + assert spaces[a]=deadline: + return checkpoint('prefix_cap',t) + linear(forward,*e) + for key,f,roles in schedule.get(t,()): + pp = pure_images(forward,roles,universe[key]) + bump(key,'prefix_checked') + if pp: + snaps[t].append((key,f,roles,pp)) + bump(key,'prefix_nonzero') + else: + pending.discard((t,key,f)) + if t%4096==0: + checkpoint('prefix',t) + assert all(forward[i]=={i:Q(1)} for i in set().union(*universe.values())) + backward = identity() + for t in reversed(range(len(decoded))): + if monotonic()>=deadline: + return checkpoint('suffix_cap',t) + for key,f,roles,pp in snaps.get(t,()): + ss = pure_images(backward,roles,universe[key]) + bump(key,'suffix_checked') + if not any(dot(c,d) for c in pp for d in ss): + pending.discard((t,key,f)) + continue + bump(key,'union_nonzero') + # Recover the exact prefix only at cuts surviving the union test. + local = identity() + for e in decoded[:t+1]: + linear(local,*e) + pivot_stock = set(roles) + u,v = key[:2] + g = groups[u,v] + unresolved_before = len(unresolved) + for extender,row in options[key].items(): + if monotonic()>=deadline: + unresolved.append(dict(clock=t,frame=f,endpoints=key[:2],parts=key[2:],reason='extender_cap')) + return checkpoint('extender_cap',t) + group = g|{extender} + pivots = sorted(pivot_stock&group) + if not pivots: + continue + cc = pure_coefficients(local,roles,group,add) + dd = pure_coefficients(backward,roles,group,add) + bump(key,'exact_extender_checked') + nonzero = False + for c,a in cc: + for d,b in dd: + paired = dot(c,d) + if not paired: + continue + nonzero = True + if dot(a,b)!=paired: + continue + for scale in (Q(1),paired,Q(-1)): + aa = {i:q/scale for i,q in a.items()} + co = {i:q/scale for i,q in c.items()} + bb = {i:q*scale/paired for i,q in b.items()} + do = {i:q*scale/paired for i,q in d.items()} + for pivot in pivots: + try: + ops = basis(aa,bb,pivot,f)+basis(co,do,pivot,u) + except ValueError: + continue + if admissible(ops): + candidate = nominate(word,row['side'],extender,(u,v),t,f,pivot, + [dims[f]-dims[u],dims[v]-dims[f]],aa,bb,co,do,check_cut) + candidate['price_margin'] = row['complete_margin_interval'] + candidate['build_command'] = 'python3.12 -I -B build.py dependencies SUPPORT.json CANDIDATE.json' + return checkpoint('witness',t) + if nonzero: + unresolved.append(dict(clock=t,frame=f,endpoints=key[:2],parts=key[2:],extender=extender,reason='no_admissible_basis_pair')) + if len(unresolved)==unresolved_before: + pending.discard((t,key,f)) + linear(backward,*decoded[t],reverse=True) + if t%4096==0: + checkpoint('suffix',t) + assert bool(pending)==bool(unresolved) + checkpoint('exhausted' if not unresolved else 'unresolved_basis_pairs',0) + + +if __name__=='__main__': + assert __debug__ + p = ArgumentParser() + p.add_argument('dependencies',type=Path,nargs='?',default=Path(__file__).resolve().parent/'dependencies') + p.add_argument('out',type=Path,nargs='?') + p.add_argument('--seconds',type=int,default=120,choices=range(2,121),metavar='2..120') + p.add_argument('--controls-only',action='store_true') + p.add_argument('--price-only',action='store_true') + a = p.parse_args() + roots = {key:a.dependencies/key for key in ('round30','round36','round37','round38','round49')} + if a.controls_only: + files = authenticate(roots) + print(json.dumps(controls(runpy.run_path(str(files['round36/cochart-audit/verify.py']))))) + else: + if a.out is None: + p.error('fresh output directory required') + a.out.mkdir() + def cap(*_): + raise TimeoutError('hard runner deadline') + signal(SIGALRM,cap) + alarm(a.seconds) + try: + run(roots,a.out,a.seconds,a.price_only) + except TimeoutError: + save(a.out,'TIMEOUT.json',dict(head=HEAD,status='hard_timeout',unverified_signatures=83)) + raise SystemExit(2) + finally: + alarm(0) diff --git a/research/p104-charged-rank-six-support-bound/engines/independent_2_5.py b/research/p104-charged-rank-six-support-bound/engines/independent_2_5.py new file mode 100644 index 0000000000..1283f9a3fe --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/engines/independent_2_5.py @@ -0,0 +1,286 @@ +"""Independent reverse-first census for charged rank-six 2+5 helper extensions.""" +from argparse import ArgumentParser +from ast import FunctionDef, Module, parse +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from hashlib import sha256 +import json +from pathlib import Path +import runpy +from signal import alarm, signal, SIGALRM + +PINS = { + 'round35/verify.py': 'c906fffec26f043e159f8e314b0f245cde432cf72d2bc6a6ade6235a4c798c5a', + 'round36/predecessor_search.py': '668022953f53929fd4d95ed1b5c01ac2ba3b4bdf6be7babae511757eb21b7e6a', + 'round37/preflight/PRICE.json': 'bc6134776a077b4ae3ef595c6000563062b2a42a3684a3852ba4f2f77b8dc726', +} +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +PARTS = ((2, 5),) + + +def add(row, other, factor): + for k,x in other.items(): + y = row.get(k,0) + factor*x + if y: + row[k] = y + else: + row.pop(k,None) + + +def read_json(data): + def unique(pairs): + result = dict(pairs) + assert len(result) == len(pairs), 'duplicate JSON key' + return result + return json.loads(data, object_pairs_hook=unique) + + +def source(roots, inventory_hash, support_hash): + PINS["round51/INVENTORY.json"] = inventory_hash + PINS["round51/SUPPORT.json"] = support_hash + loaded = {} + for name,digest in PINS.items(): + label,path = name.split('/',1) + file = roots[label]/path + assert sha256(file.read_bytes()).hexdigest() == digest, name + loaded[name] = file + audit = runpy.run_path(str(loaded['round35/verify.py'])) + tree = parse(loaded['round36/predecessor_search.py'].read_text()) + function, = [x for x in tree.body if isinstance(x,FunctionDef) and x.name == 'pure_combinations'] + env = {'add':add,'Q':Q} + exec(compile(Module(body=[function],type_ignores=[]), 'pinned-pure-combinations', 'exec'), env) + receipts = [read_json(path.read_bytes()) for key,path in loaded.items() if key.endswith('.json')] + return audit,env['pure_combinations'],receipts + + +def write(out,name,obj): + temp = out/(name+'.tmp') + temp.write_text(json.dumps(obj,sort_keys=True,indent=2)+'\n') + temp.replace(out/name) + + +def geometry(word,caller,early,audit,receipt): + frames = audit['spaces'](word['frames']) + dims = [len(s).bit_length()-1 for s in frames] + main = set(word['live']) | {i+112 for i in word['live']} | set(word['hosted']['X2']+word['hosted']['Y2']) + helpers = defaultdict(set) + for i,(a,b) in enumerate(zip(word['initial'],word['final'],strict=True)): + if i not in main: + helpers[a,b].add(i) + extensions = {} + for (a,b),roles in helpers.items(): + if dims[b]-dims[a] != 6: + continue + assert frames[a] < frames[b] + for f,span in enumerate(frames): + if dims[f] == dims[a]-1 and span < frames[a]: + extensions['input',(a,b),(f,b)] = roles + if dims[f] == dims[b]+1 and frames[b] < span: + extensions['output',(a,b),(a,f)] = roles + typed = {(*key,part):roles for key,roles in extensions.items() for part in PARTS} + source_rows = [r for r in receipt['rows'] if r['old_rank'] == 6 and tuple(r['parts']) in PARTS] + keys = [(r['side'],tuple(r['prior']),tuple(r['new']),tuple(r['parts'])) for r in source_rows] + assert len(keys) == len(set(keys)) == len(typed) == 83 + declared = dict(zip(keys,source_rows,strict=True)) + assert typed.keys() == declared.keys() + for key,roles in typed.items(): + r = declared[key] + assert roles == set(r['extender_roles']) + assert helpers.get(key[2],set()) == set(r['new_cohort_before_extension']) + assert not roles & helpers.get(key[2],set()) + assert Counter(r['old_rank'] for r in receipt['rows']) == {8:24,7:90,6:166,5:432,4:15,3:50} + + @cache + def relative(a,b): + return dims[a]+dims[b]-2*(len(frames[a]&frames[b]).bit_length()-1) + + tape = word['program'] + remove = next(i for i,e in enumerate(tape) if e[0] == 'MOVE') + paid = audit['literal_move_bill'](tape,word,relative) + contacts,_ = audit['whole_contact_recount']([(i,e) for i,e in enumerate(tape) if e[0]!='MOVE'],word,relative) + assert sum(paid.values()) == 6280 and contacts == paid + try: + audit['literal_move_bill'](tape[:remove]+tape[remove+1:],word,relative) + except AssertionError: + pass + else: + raise AssertionError('omitted paid MOVE accepted') + P,T,copies = audit['full_bill'](word,caller,paid,relative) + assert copies == receipt['copies'] == 17 + assert {str(r):v for r,v in P.items()} == early['invoice']['P'] + assert {str(r):v for r,v in T.items()} == early['invoice']['T'] + net = T.copy() + net.subtract(P) + k = Q(early['price']['independent_raw_bracket'][1]) + assert k == Q(receipt['crossing_upper']) + baseline = audit['price'](net,k) + assert baseline[1] < 0 + bounds = {} + for parts in PARTS: + change = Counter(parts) + change[6] -= 1 + change[1] -= 1 + assert sum(rank*n for rank,n in change.items()) == 0 + delta = audit['price']({r:v*copies for r,v in change.items()},k) + bounds[parts] = tuple(a+b for a,b in zip(delta,baseline,strict=True)) + assert 0 < bounds[parts][0] <= bounds[parts][1] + for key,row in declared.items(): + lo,hi = map(Q,row['complete_margin_interval']) + lower,upper = bounds[key[3]] + assert lo <= lower <= upper <= hi + interval_rank = sorted(PARTS,key=lambda part:bounds[part][0],reverse=True) + assert all(bounds[a][0] > bounds[b][1] for a,b in zip(interval_rank,interval_rank[1:])) + assert [r['parts'] for r in source_rows] == [ + list(part) for part in interval_rank for _ in range(len(extensions))] + assert [tuple(x) for x in interval_rank] == [(2,5)] + return frames,dims,helpers,typed,bounds,interval_rank + + +def groups_for(helpers,typed): + grouping = defaultdict(dict) + for key,roles in typed.items(): + grouping[key[2],key[3]][key] = roles + universe = {g:helpers.get(g[0],set()) | set().union(*rows.values()) + for g,rows in grouping.items()} + assert len(grouping) == 73 + return grouping,universe + + +def reverse_cuts(word,frames,dims,helpers,grouping,universe): + n = word['public'] + tape = word['program'] + charts = word['final'] + [None]*word['owned_fields'] + banks = defaultdict(set) + for r,f in enumerate(charts[:n]): + banks[f].add(r) + groups_by_frame = defaultdict(list) + for g in grouping: + (a,b),parts = g + assert not any(word['initial'][r] == f + for f in range(len(frames)) if dims[f]-dims[a] in parts and frames[a]=n) + assert frames[a]=n + charts[r] = f + banks[f].add(r) + elif op == 'INIT': + f = args[0] + assert charts[r] == f and r>=n + charts[r] = None + banks[f].remove(r) + else: + assert charts[r] == args[-1] + if op in ('ADD','COPY'): + assert charts[args[0]] == charts[r] + assert charts == word['initial']+[None]*word['owned_fields'] + return schedule,counts,typed_counts + + +def step(rows,e,reverse): + op,d,*args = e + if op in ('CLEAR','INIT'): + rows[d] = {} + elif op == 'SCALE': + q = Q(args[-2]) + rows[d] = {k:q*v for k,v in rows[d].items()} + elif op in ('ADD','COPY'): + s,q = args[0],Q(args[-2]) + assert s != d + if reverse: + add(rows[s],rows[d],q) + if op == 'COPY': + rows[d] = {} + elif op == 'ADD': + add(rows[d],rows[s],q) + else: + rows[d] = {k:q*v for k,v in rows[s].items()} + + +def run(roots,out,inventory_hash,support_hash): + audit,pure,(pricing,inventory,lead) = source(roots,inventory_hash,support_hash) + word,caller,early = audit['read_inputs'](roots['round30']/'complex/source') + assert pricing['head'] == inventory['head'] == lead['head'] == HEAD + frames,dims,helpers,typed,bounds,ranking = geometry(word,caller,early,audit,pricing) + grouping,universe = groups_for(helpers,typed) + schedule,cuts,typed_counts = reverse_cuts(word,frames,dims,helpers,grouping,universe) + assert cuts == Counter({(tuple(r['endpoints']),tuple(r['parts'])):r['cuts'] for r in inventory['counts']}) + assert typed_counts == Counter({(r['side'],tuple(r['prior']),tuple(r['new']),tuple(r['parts'])):r['cuts'] for r in inventory['typed']}) + assert sum(cuts.values()) == inventory['cuts'] + result = {'head':HEAD,'typed_signatures':len(typed),'union_groups':len(grouping), + 'rank_six_3_plus_4_predecessor':83,'smaller_outside_scope':497,'cut_incidences':sum(cuts.values()), + 'part_price_order':[list(p) for p in ranking], + 'whole_margins':{'+'.join(map(str,p)):list(map(str,v)) for p,v in bounds.items()}, + 'literal_paid_move_omission_rejected':True,'pins':PINS} + write(out,'CUTS.json',result) + n,tape = word['public'],word['program'] + def identity(): + return [{i:Q(1)} for i in range(n)]+[{} for _ in range(word['owned_fields'])] + suffix, stored, seen = identity(),{},0 + for t in reversed(range(len(tape))): + for group,f,roles in schedule.get(t,()): + right = pure(suffix,roles,universe[group]) + seen += 1 + if right: + stored[t,group,f] = tuple(d for d,_ in right) + step(suffix,tape[t],True) + prefix,positive,checked,comparisons = identity(),Counter(),0,0 + for t,e in enumerate(tape): + step(prefix,e,False) + for group,f,roles in schedule.get(t,()): + left = pure(prefix,roles,universe[group]) + checked += 1 + if left: + positive[group] += 1 + for c,_ in left: + for d in stored.get((t,group,f),()): + comparisons += 1 + assert not sum(x*d.get(i,0) for i,x in c.items()),(t,f,group) + assert all(prefix[i] == {i:Q(1)} for u in universe.values() for i in u) + assert seen == checked == inventory['cuts'] + assert positive == Counter({(tuple(r['endpoints']),tuple(r['parts'])):r.get('prefix_nonzero',0) for r in lead['by_parts']}) + assert lead['phase']=='exhausted' + assert not lead['candidate'] and not lead['unresolved'] + result.update(status='PASS_INDEPENDENT_REVERSE_FIRST_RANK6_2_PLUS_5',positive_prefix_images=sum(positive.values()), + suffix_nonzero_cuts=len(stored),basis_pairings_tested=comparisons,positive_pairings=0) + write(out,'RESULT.json',result) + + +if __name__ == '__main__': + p = ArgumentParser(description=__doc__) + for name in ('round30','round35','round36','round37','round51','out'): + p.add_argument(name,type=Path) + p.add_argument("--inventory-sha",required=True) + p.add_argument("--support-sha",required=True) + a = p.parse_args() + a.out.mkdir() + def timeout(*_): + raise TimeoutError('independent replay watchdog') + signal(SIGALRM,timeout) + alarm(43) + run({k:getattr(a,k) for k in ('round30','round35','round36','round37','round51')},a.out,a.inventory_sha,a.support_sha) + alarm(0) diff --git a/research/p104-charged-rank-six-support-bound/engines/independent_3_4.py b/research/p104-charged-rank-six-support-bound/engines/independent_3_4.py new file mode 100644 index 0000000000..cb40c5b29a --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/engines/independent_3_4.py @@ -0,0 +1,286 @@ +"""Independent reverse-first census for charged rank-six 3+4 helper extensions.""" +from argparse import ArgumentParser +from ast import FunctionDef, Module, parse +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from hashlib import sha256 +import json +from pathlib import Path +import runpy +from signal import alarm, signal, SIGALRM + +PINS = { + 'round35/verify.py': 'c906fffec26f043e159f8e314b0f245cde432cf72d2bc6a6ade6235a4c798c5a', + 'round36/predecessor_search.py': '668022953f53929fd4d95ed1b5c01ac2ba3b4bdf6be7babae511757eb21b7e6a', + 'round37/preflight/PRICE.json': 'bc6134776a077b4ae3ef595c6000563062b2a42a3684a3852ba4f2f77b8dc726', +} +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +PARTS = ((3, 4),) + + +def add(row, other, factor): + for k,x in other.items(): + y = row.get(k,0) + factor*x + if y: + row[k] = y + else: + row.pop(k,None) + + +def read_json(data): + def unique(pairs): + result = dict(pairs) + assert len(result) == len(pairs), 'duplicate JSON key' + return result + return json.loads(data, object_pairs_hook=unique) + + +def source(roots, inventory_hash, support_hash): + PINS["round50/INVENTORY.json"] = inventory_hash + PINS["round50/SUPPORT.json"] = support_hash + loaded = {} + for name,digest in PINS.items(): + label,path = name.split('/',1) + file = roots[label]/path + assert sha256(file.read_bytes()).hexdigest() == digest, name + loaded[name] = file + audit = runpy.run_path(str(loaded['round35/verify.py'])) + tree = parse(loaded['round36/predecessor_search.py'].read_text()) + function, = [x for x in tree.body if isinstance(x,FunctionDef) and x.name == 'pure_combinations'] + env = {'add':add,'Q':Q} + exec(compile(Module(body=[function],type_ignores=[]), 'pinned-pure-combinations', 'exec'), env) + receipts = [read_json(path.read_bytes()) for key,path in loaded.items() if key.endswith('.json')] + return audit,env['pure_combinations'],receipts + + +def write(out,name,obj): + temp = out/(name+'.tmp') + temp.write_text(json.dumps(obj,sort_keys=True,indent=2)+'\n') + temp.replace(out/name) + + +def geometry(word,caller,early,audit,receipt): + frames = audit['spaces'](word['frames']) + dims = [len(s).bit_length()-1 for s in frames] + main = set(word['live']) | {i+112 for i in word['live']} | set(word['hosted']['X2']+word['hosted']['Y2']) + helpers = defaultdict(set) + for i,(a,b) in enumerate(zip(word['initial'],word['final'],strict=True)): + if i not in main: + helpers[a,b].add(i) + extensions = {} + for (a,b),roles in helpers.items(): + if dims[b]-dims[a] != 6: + continue + assert frames[a] < frames[b] + for f,span in enumerate(frames): + if dims[f] == dims[a]-1 and span < frames[a]: + extensions['input',(a,b),(f,b)] = roles + if dims[f] == dims[b]+1 and frames[b] < span: + extensions['output',(a,b),(a,f)] = roles + typed = {(*key,part):roles for key,roles in extensions.items() for part in PARTS} + source_rows = [r for r in receipt['rows'] if r['old_rank'] == 6 and tuple(r['parts']) in PARTS] + keys = [(r['side'],tuple(r['prior']),tuple(r['new']),tuple(r['parts'])) for r in source_rows] + assert len(keys) == len(set(keys)) == len(typed) == 83 + declared = dict(zip(keys,source_rows,strict=True)) + assert typed.keys() == declared.keys() + for key,roles in typed.items(): + r = declared[key] + assert roles == set(r['extender_roles']) + assert helpers.get(key[2],set()) == set(r['new_cohort_before_extension']) + assert not roles & helpers.get(key[2],set()) + assert Counter(r['old_rank'] for r in receipt['rows']) == {8:24,7:90,6:166,5:432,4:15,3:50} + + @cache + def relative(a,b): + return dims[a]+dims[b]-2*(len(frames[a]&frames[b]).bit_length()-1) + + tape = word['program'] + remove = next(i for i,e in enumerate(tape) if e[0] == 'MOVE') + paid = audit['literal_move_bill'](tape,word,relative) + contacts,_ = audit['whole_contact_recount']([(i,e) for i,e in enumerate(tape) if e[0]!='MOVE'],word,relative) + assert sum(paid.values()) == 6280 and contacts == paid + try: + audit['literal_move_bill'](tape[:remove]+tape[remove+1:],word,relative) + except AssertionError: + pass + else: + raise AssertionError('omitted paid MOVE accepted') + P,T,copies = audit['full_bill'](word,caller,paid,relative) + assert copies == receipt['copies'] == 17 + assert {str(r):v for r,v in P.items()} == early['invoice']['P'] + assert {str(r):v for r,v in T.items()} == early['invoice']['T'] + net = T.copy() + net.subtract(P) + k = Q(early['price']['independent_raw_bracket'][1]) + assert k == Q(receipt['crossing_upper']) + baseline = audit['price'](net,k) + assert baseline[1] < 0 + bounds = {} + for parts in PARTS: + change = Counter(parts) + change[6] -= 1 + change[1] -= 1 + assert sum(rank*n for rank,n in change.items()) == 0 + delta = audit['price']({r:v*copies for r,v in change.items()},k) + bounds[parts] = tuple(a+b for a,b in zip(delta,baseline,strict=True)) + assert 0 < bounds[parts][0] <= bounds[parts][1] + for key,row in declared.items(): + lo,hi = map(Q,row['complete_margin_interval']) + lower,upper = bounds[key[3]] + assert lo <= lower <= upper <= hi + interval_rank = sorted(PARTS,key=lambda part:bounds[part][0],reverse=True) + assert all(bounds[a][0] > bounds[b][1] for a,b in zip(interval_rank,interval_rank[1:])) + assert [r['parts'] for r in source_rows] == [ + list(part) for part in interval_rank for _ in range(len(extensions))] + assert [tuple(x) for x in interval_rank] == [(3,4)] + return frames,dims,helpers,typed,bounds,interval_rank + + +def groups_for(helpers,typed): + grouping = defaultdict(dict) + for key,roles in typed.items(): + grouping[key[2],key[3]][key] = roles + universe = {g:helpers.get(g[0],set()) | set().union(*rows.values()) + for g,rows in grouping.items()} + assert len(grouping) == 73 + return grouping,universe + + +def reverse_cuts(word,frames,dims,helpers,grouping,universe): + n = word['public'] + tape = word['program'] + charts = word['final'] + [None]*word['owned_fields'] + banks = defaultdict(set) + for r,f in enumerate(charts[:n]): + banks[f].add(r) + groups_by_frame = defaultdict(list) + for g in grouping: + (a,b),parts = g + assert not any(word['initial'][r] == f + for f in range(len(frames)) if dims[f]-dims[a] in parts and frames[a]=n) + assert frames[a]=n + charts[r] = f + banks[f].add(r) + elif op == 'INIT': + f = args[0] + assert charts[r] == f and r>=n + charts[r] = None + banks[f].remove(r) + else: + assert charts[r] == args[-1] + if op in ('ADD','COPY'): + assert charts[args[0]] == charts[r] + assert charts == word['initial']+[None]*word['owned_fields'] + return schedule,counts,typed_counts + + +def step(rows,e,reverse): + op,d,*args = e + if op in ('CLEAR','INIT'): + rows[d] = {} + elif op == 'SCALE': + q = Q(args[-2]) + rows[d] = {k:q*v for k,v in rows[d].items()} + elif op in ('ADD','COPY'): + s,q = args[0],Q(args[-2]) + assert s != d + if reverse: + add(rows[s],rows[d],q) + if op == 'COPY': + rows[d] = {} + elif op == 'ADD': + add(rows[d],rows[s],q) + else: + rows[d] = {k:q*v for k,v in rows[s].items()} + + +def run(roots,out,inventory_hash,support_hash): + audit,pure,(pricing,inventory,lead) = source(roots,inventory_hash,support_hash) + word,caller,early = audit['read_inputs'](roots['round30']/'complex/source') + assert pricing['head'] == inventory['head'] == lead['head'] == HEAD + frames,dims,helpers,typed,bounds,ranking = geometry(word,caller,early,audit,pricing) + grouping,universe = groups_for(helpers,typed) + schedule,cuts,typed_counts = reverse_cuts(word,frames,dims,helpers,grouping,universe) + assert cuts == Counter({(tuple(r['endpoints']),tuple(r['parts'])):r['cuts'] for r in inventory['counts']}) + assert typed_counts == Counter({(r['side'],tuple(r['prior']),tuple(r['new']),tuple(r['parts'])):r['cuts'] for r in inventory['typed']}) + assert sum(cuts.values()) == inventory['cuts'] + result = {'head':HEAD,'typed_signatures':len(typed),'union_groups':len(grouping), + 'rank_six_2_plus_5_outside_scope':83,'smaller_outside_scope':497,'cut_incidences':sum(cuts.values()), + 'part_price_order':[list(p) for p in ranking], + 'whole_margins':{'+'.join(map(str,p)):list(map(str,v)) for p,v in bounds.items()}, + 'literal_paid_move_omission_rejected':True,'pins':PINS} + write(out,'CUTS.json',result) + n,tape = word['public'],word['program'] + def identity(): + return [{i:Q(1)} for i in range(n)]+[{} for _ in range(word['owned_fields'])] + suffix, stored, seen = identity(),{},0 + for t in reversed(range(len(tape))): + for group,f,roles in schedule.get(t,()): + right = pure(suffix,roles,universe[group]) + seen += 1 + if right: + stored[t,group,f] = tuple(d for d,_ in right) + step(suffix,tape[t],True) + prefix,positive,checked,comparisons = identity(),Counter(),0,0 + for t,e in enumerate(tape): + step(prefix,e,False) + for group,f,roles in schedule.get(t,()): + left = pure(prefix,roles,universe[group]) + checked += 1 + if left: + positive[group] += 1 + for c,_ in left: + for d in stored.get((t,group,f),()): + comparisons += 1 + assert not sum(x*d.get(i,0) for i,x in c.items()),(t,f,group) + assert all(prefix[i] == {i:Q(1)} for u in universe.values() for i in u) + assert seen == checked == inventory['cuts'] + assert positive == Counter({(tuple(r['endpoints']),tuple(r['parts'])):r.get('prefix_nonzero',0) for r in lead['by_parts']}) + assert lead['phase']=='exhausted' + assert not lead['candidate'] and not lead['unresolved'] + result.update(status='PASS_INDEPENDENT_REVERSE_FIRST_RANK6_3_PLUS_4',positive_prefix_images=sum(positive.values()), + suffix_nonzero_cuts=len(stored),basis_pairings_tested=comparisons,positive_pairings=0) + write(out,'RESULT.json',result) + + +if __name__ == '__main__': + p = ArgumentParser(description=__doc__) + for name in ('round30','round35','round36','round37','round50','out'): + p.add_argument(name,type=Path) + p.add_argument("--inventory-sha",required=True) + p.add_argument("--support-sha",required=True) + a = p.parse_args() + a.out.mkdir() + def timeout(*_): + raise TimeoutError('independent replay watchdog') + signal(SIGALRM,timeout) + alarm(43) + run({k:getattr(a,k) for k in ('round30','round35','round36','round37','round50')},a.out,a.inventory_sha,a.support_sha) + alarm(0) diff --git a/research/p104-charged-rank-six-support-bound/engines/primary_2_5.py b/research/p104-charged-rank-six-support-bound/engines/primary_2_5.py new file mode 100644 index 0000000000..20779bf5b3 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/engines/primary_2_5.py @@ -0,0 +1,376 @@ +"""Exact rank-six to rank-seven, 2+5 charged endpoint support gate.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import runpy +from signal import SIGALRM, alarm, signal +import sys +from time import monotonic + +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' +WORD = 'complex/source/inputs/WORD.json.gz' +PINS = { + 'round30/'+WORD: '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756', + 'round30/complex/audit.py': '67b006627fd4e07c349f48f31e6d541c62804416bdc85f664a3607dd1b386efb', + 'round30/complex/source/powers.py': 'c0c460b464d7c836fb887010b57119be322aae686736b86820aae3544d380bee', + 'round30/complex/source/inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'round30/complex/source/inputs/EARLY-RESULT.json': '691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7', + 'round37/preflight/price.py': '8b1b345bd4a2732c74251c1b95d47f98cd37184894d8979a6ef1953d38686be8', + 'round38/incremental/screen.py': '43a74344555088b016a3fb857b7c86de3f2880ef85b77846c4362037779b8405', + 'round50/lead/screen.py': '47251bd902c4fd3fda3597463cf4609bf380194558461320dc432b86f6c989d1', + 'round37/preflight/PRICE.json': 'bc6134776a077b4ae3ef595c6000563062b2a42a3684a3852ba4f2f77b8dc726', + 'round36/cochart-audit/verify.py': '58cab0bb2f24fe29d0e190cbe3cc0dc85f889ec4af66b5a02328d1e1d0e37e8a', + 'round36/incremental/predecessor_split.py': '999b9eeabe5cd1a7e3ec014d1a449f850b4ac9bfb19749cddef41ae12cd0b405', + 'round36/incremental/support.py': 'f3e6eeb879480715c5c32c1a390a63c57d26ea1c9a9cbdb89b83ca34260e47f6', +} + + +def read_json(raw): + def unique(items): + result = dict(items) + assert len(result)==len(items),'Duplicate keys' + return result + return json.loads(raw,object_pairs_hook=unique) + + +def save(out,name,receipt): + path = out/(name+'.tmp') + path.write_text(json.dumps(receipt,indent=2,sort_keys=True)+'\n') + path.replace(out/name) + + +def dot(a,b): + return sum(x*b.get(i,0) for i,x in a.items()) + + +def pure_coefficients(rows, roles, group, add): + exterior, output = {}, [] + for role in reversed(roles): + residual = rows[role].copy() + coefficients = {role:Q(1)} + while (lead:=max((k for k in residual if k not in group),default=-1))>=0: + if lead not in exterior: + exterior[lead] = residual,coefficients + break + old,co = exterior[lead] + scale = -residual[lead]/old[lead] + add(residual,old,scale) + add(coefficients,co,scale) + else: + output.append((residual,coefficients)) + return output + + +def admissible(program): + def smooth(n): + for p in (2,3,5): + while n%p==0: + n//=p + return n==1 + for op,*e in program: + q = Q(e[-2]) + if not q or not smooth(q.denominator) or op=='SCALE' and not smooth(abs(q.numerator)): + return False + return True + + +def nominate(word, side, extender, new, t, frame, pivot, ranks, a,b,c,d, check): + u,v = new + changed = dict(word,initial=word['initial'].copy(),final=word['final'].copy()) + if side=='input': + prior = changed['initial'][extender] + changed['initial'][extender] = u + changed['program'] = [['MOVE',extender,u,prior,False]]+word['program'] + else: + prior = changed['final'][extender] + changed['final'][extender] = v + changed['program'] = word['program']+[['MOVE',extender,prior,v,False]] + h = dict(cut_after=t+(side=='input'),frame=frame,pivot=pivot,ranks=ranks) + h.update({name:{str(i):str(q) for i,q in vector.items()} for name,vector in zip('abcd',(a,b,c,d),strict=True)}) + check(changed,h) + return dict(extender=extender,side=side,new=new,original_cut=t,split=h,added_move=changed['program'][0 if side=='input' else -1]) + + +def controls(predecessor): + add, images = predecessor['add'], predecessor['pure_images'] + rows = [{0:Q(1),3:Q(1)}, {3:Q(1)}, {1:Q(-2)}] + assert images(rows,[0,1],{0}) and not images(rows,[0,1],{1}) + (image,coefficients), = pure_coefficients(rows,[0,1],{0},add) + assert set(image)=={0} and abs(image[0])==1 + assert set(coefficients)=={0,1} + assert dot(image,{0:Q(2)}) and not dot(image,rows[2]) + assert admissible([['ADD',0,1,'-7/15',0],['SCALE',1,'-3/10',0]]) + assert not admissible([['ADD',0,1,'1/7',0]]) + assert not admissible([['SCALE',1,'7/10',0]]) + return ['exterior_cancellation_recovers_pure_image','outside_only_bank_excluded', + 'signed_pairing_positive_and_zero','native_basis_coefficient_controls'] + + +def authenticate(roots): + files = {} + for name,digest in PINS.items(): + prefix,p = name.split('/',1) + path = roots[prefix]/p + assert sha256(path.read_bytes()).hexdigest()==digest,name + files[name] = path + return files + + +def run(roots,out,seconds,price_only=False): + start = monotonic() + deadline = start + min(115,seconds-1) + files = authenticate(roots) + word = read_json(gzip.decompress(files['round30/'+WORD].read_bytes())) + receipt = read_json(files['round37/preflight/PRICE.json'].read_bytes()) + predecessor = runpy.run_path(str(files['round36/cochart-audit/verify.py'])) + sys.path.insert(0,str(roots['round36']/'incremental')) + from predecessor_split import basis, check_cut + space,linear,add = (predecessor[name] for name in ('binary_span','linear','add')) + pure_images = predecessor['pure_images'] + assert receipt['head']==HEAD and receipt['copies']==17 and receipt['typed_signatures']==777 + price_model = runpy.run_path(str(files['round37/preflight/price.py'])) + rebuilt = price_model['screen'](roots['round30']) + assert json.loads(json.dumps(rebuilt)) == receipt + rows = [r for r in receipt['rows'] if r['old_rank']==6 and r['parts']==[2,5]] + assert len(rows)==83 and Counter(r['side'] for r in rows)=={'input':50,'output':33} + assert all(Q(r['complete_margin_interval'][0])== + Q('81024793093613521452053125690576433136027840493/1000000000000000000000000000000000000000000000000') + for r in rows) + save(out,'PRICE.json',dict(head=HEAD,pins=PINS,crossing_upper=receipt['crossing_upper'], + baseline_interval=receipt['baseline_moment_interval'],copies=17,selected_signatures=len(rows), + paid_rank_delta={1:17},productive_rank_delta={2:17,5:17,6:-17}, + complete_margin_interval_per_alternative=rows[0]['complete_margin_interval'], + alternatives=rows,grant='One alternative at a time. Additional ordinary and physical costs free only in this upper.')) + checks = controls(predecessor) + if price_only: + return + n,tape = word['public'],word['program'] + spaces = list(map(space,word['frames'])) + dims = list(map(len,word['frames'])) + main = set(word['live']) | {i+112 for i in word['live']} + main.update(word['hosted']['X2']) + main.update(word['hosted']['Y2']) + groups = defaultdict(set) + for i,(a,b) in enumerate(zip(word['initial'],word['final'],strict=True)): + if i not in main: + groups[a,b].add(i) + options = defaultdict(dict) + typed = defaultdict(list) + for row in rows: + side = row['side'] + a,b = row['prior'] + u,v = row['new'] + g = groups[u,v] + assert set(row['new_cohort_before_extension'])==g + assert groups[a,b]==set(row['extender_roles']) and not g&groups[a,b] + assert (b==v and spaces[u]=deadline: + return save(out,'SUPPORT.json',dict(head=HEAD,phase='inventory_cap',clock=t, + candidate=None,unresolved_signatures=rows,controls=checks)) + src,q = dst,None + if op=='MOVE': + a,b,owned = args + assert chart[dst]==a and owned==(dst>=n) + assert spaces[a]=deadline: + return checkpoint('prefix_cap',t) + linear(forward,*e) + for key,f,roles in schedule.get(t,()): + pp = pure_images(forward,roles,universe[key]) + bump(key,'prefix_checked') + if pp: + snaps[t].append((key,f,roles,pp)) + bump(key,'prefix_nonzero') + else: + pending.discard((t,key,f)) + if t%4096==0: + checkpoint('prefix',t) + assert all(forward[i]=={i:Q(1)} for i in set().union(*universe.values())) + backward = identity() + for t in reversed(range(len(decoded))): + if monotonic()>=deadline: + return checkpoint('suffix_cap',t) + for key,f,roles,pp in snaps.get(t,()): + ss = pure_images(backward,roles,universe[key]) + bump(key,'suffix_checked') + if not any(dot(c,d) for c in pp for d in ss): + pending.discard((t,key,f)) + continue + bump(key,'union_nonzero') + # Recover the exact prefix only at cuts surviving the union test. + local = identity() + for e in decoded[:t+1]: + linear(local,*e) + pivot_stock = set(roles) + u,v = key[:2] + g = groups[u,v] + unresolved_before = len(unresolved) + for extender,row in options[key].items(): + if monotonic()>=deadline: + unresolved.append(dict(clock=t,frame=f,endpoints=key[:2],parts=key[2:],reason='extender_cap')) + return checkpoint('extender_cap',t) + group = g|{extender} + pivots = sorted(pivot_stock&group) + if not pivots: + continue + cc = pure_coefficients(local,roles,group,add) + dd = pure_coefficients(backward,roles,group,add) + bump(key,'exact_extender_checked') + nonzero = False + for c,a in cc: + for d,b in dd: + paired = dot(c,d) + if not paired: + continue + nonzero = True + if dot(a,b)!=paired: + continue + for scale in (Q(1),paired,Q(-1)): + aa = {i:q/scale for i,q in a.items()} + co = {i:q/scale for i,q in c.items()} + bb = {i:q*scale/paired for i,q in b.items()} + do = {i:q*scale/paired for i,q in d.items()} + for pivot in pivots: + try: + ops = basis(aa,bb,pivot,f)+basis(co,do,pivot,u) + except ValueError: + continue + if admissible(ops): + candidate = nominate(word,row['side'],extender,(u,v),t,f,pivot, + [dims[f]-dims[u],dims[v]-dims[f]],aa,bb,co,do,check_cut) + candidate['price_margin'] = row['complete_margin_interval'] + candidate['build_command'] = 'python3.12 -I -B build.py dependencies SUPPORT.json CANDIDATE.json' + return checkpoint('witness',t) + if nonzero: + unresolved.append(dict(clock=t,frame=f,endpoints=key[:2],parts=key[2:],extender=extender,reason='no_admissible_basis_pair')) + if len(unresolved)==unresolved_before: + pending.discard((t,key,f)) + linear(backward,*decoded[t],reverse=True) + if t%4096==0: + checkpoint('suffix',t) + assert bool(pending)==bool(unresolved) + checkpoint('exhausted' if not unresolved else 'unresolved_basis_pairs',0) + + +if __name__=='__main__': + assert __debug__ + p = ArgumentParser() + p.add_argument('dependencies',type=Path,nargs='?',default=Path(__file__).resolve().parent/'dependencies') + p.add_argument('out',type=Path,nargs='?') + p.add_argument('--seconds',type=int,default=120,choices=range(2,121),metavar='2..120') + p.add_argument('--controls-only',action='store_true') + p.add_argument('--price-only',action='store_true') + a = p.parse_args() + roots = {key:a.dependencies/key for key in ('round30','round36','round37','round38','round50')} + if a.controls_only: + files = authenticate(roots) + print(json.dumps(controls(runpy.run_path(str(files['round36/cochart-audit/verify.py']))))) + else: + if a.out is None: + p.error('fresh output directory required') + a.out.mkdir() + def cap(*_): + raise TimeoutError('hard runner deadline') + signal(SIGALRM,cap) + alarm(a.seconds) + try: + run(roots,a.out,a.seconds,a.price_only) + except TimeoutError: + save(a.out,'TIMEOUT.json',dict(head=HEAD,status='hard_timeout',unverified_signatures=83)) + raise SystemExit(2) + finally: + alarm(0) diff --git a/research/p104-charged-rank-six-support-bound/receipts/SHA256.json b/research/p104-charged-rank-six-support-bound/receipts/SHA256.json new file mode 100644 index 0000000000..bb3cf2d39f --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/receipts/SHA256.json @@ -0,0 +1,12 @@ +{ + "2-plus-5/CUTS.json": "208a3f52596aea0c458dbe14023d3689e8ac53d4a7f38e2c7529184e6077f88e", + "2-plus-5/INVENTORY.json": "fcbf8540005f9b8775e842d2df3f74307935d4ad528e542098ce5a9f28250d84", + "2-plus-5/PRICE.json": "8f9eaab7f0869ec201df34dddb0fcad841af64b2b017bae80dd6cd087db1648d", + "2-plus-5/RESULT.json": "2c0b4ad55abf019e4e61f142c59d5f7cddd05706c494f2dcb83ca73d8523bced", + "2-plus-5/SUPPORT.json": "37950056295bb820d21390081ba9791eacde54e8782618e1570c49d56cf182cd", + "3-plus-4/CUTS.json": "3044cbe5dccf547b6cfe63437473e7dc2e05c57456afb27da6e32a64ad9f8c42", + "3-plus-4/INVENTORY.json": "b6cb030f3d747ef00d24abfd4b9adfcd990533b9621cd0cfc4c2a47d061e6a0c", + "3-plus-4/PRICE.json": "4b035e8bcc2e7f9d08078f41a2e16ea3e6ba0d5ca688b48ebb6243948e878078", + "3-plus-4/RESULT.json": "8f513bcbd4f5479cfcfdbc81ef1c349e4670e9a69a4399a7df21572651d586dc", + "3-plus-4/SUPPORT.json": "c8c2772ebb65eb218d24d66e1763e84258ccdcb16b131d83d9ede0311337d7e1" +} diff --git a/research/p104-charged-rank-six-support-bound/receipts/SUMMARY.json b/research/p104-charged-rank-six-support-bound/receipts/SUMMARY.json new file mode 100644 index 0000000000..b7dcb473e2 --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/receipts/SUMMARY.json @@ -0,0 +1,34 @@ +{ + "2-plus-5": { + "candidate": null, + "prefix_nonzero": 0, + "price_only_complete_margin": [ + "81024793093613521452053125690576433136027840493/1000000000000000000000000000000000000000000000000", + "81024793093613521452053125690576433136027896717/1000000000000000000000000000000000000000000000000" + ], + "representative_cut_incidences": 346, + "suffix_nonzero_independent": 0, + "typed_signatures": 83, + "union_groups": 73, + "unresolved": 0 + }, + "3-plus-4": { + "candidate": null, + "prefix_nonzero": 0, + "price_only_complete_margin": [ + "1835166431152278266166310959958201126735264211/15625000000000000000000000000000000000000000000", + "3670332862304556532332621919916402253470530179/31250000000000000000000000000000000000000000000" + ], + "representative_cut_incidences": 714, + "suffix_nonzero_independent": 24, + "typed_signatures": 83, + "union_groups": 73, + "unresolved": 0 + }, + "compatible_saving_after_support": "0", + "copies": 17, + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "kappa": "0.003645669928698", + "kappa_change": "0", + "unresolved": 0 +} diff --git a/research/p104-charged-rank-six-support-bound/replay.py b/research/p104-charged-rank-six-support-bound/replay.py new file mode 100644 index 0000000000..9e0c2140ad --- /dev/null +++ b/research/p104-charged-rank-six-support-bound/replay.py @@ -0,0 +1,178 @@ +"""Reprice and replay both charged rank-six support exclusions.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +import gzip +from hashlib import sha1, sha256 +import json +from pathlib import Path, PurePosixPath +import runpy +import shutil +import subprocess +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def read(path): + return json.loads(path.read_bytes(), object_pairs_hook=unique) + + +def authenticate(scratch): + pins = read(HERE / "LOCAL-PINS.json") + for key, expected in pins.items(): + rel = PurePosixPath(key) + if rel.is_absolute() or ".." in rel.parts or rel.as_posix() != key: + raise ValueError(f"invalid dependency path {key}") + if sha256((HERE / key).read_bytes()).hexdigest() != expected: + raise ValueError(f"changed dependency {key}") + deps = scratch / "dependencies" + shutil.copytree(HERE / "dependencies", deps) + unpack = read(HERE / "UNPACK.json") + assert len(unpack) == 3 + for key, entry in unpack.items(): + assert key in pins and key.endswith(".gz") and entry["destination"] == key.removesuffix(".gz") + raw = gzip.decompress((HERE / key).read_bytes()) + assert sha256(raw).hexdigest() == entry["sha256"], key + (scratch / entry["destination"]).write_bytes(raw) + provenance = read(HERE / "PROVENANCE.json")["files"] + assert len(provenance) == 5 and sum(p["uncompress"] for p in provenance.values()) == 2 + for key, pin in provenance.items(): + assert key in pins + literal = unpack[key]["destination"] if pin["uncompress"] else key + raw = (scratch / literal).read_bytes() + assert sha256(raw).hexdigest() == pin["sha256"], key + assert sha1(f"blob {len(raw)}\0".encode()+raw).hexdigest() == pin["git_blob"], key + return deps + + +def basis_control(deps): + folder = deps / "round36/incremental" + sys.path.insert(0, str(folder)) + try: + mod = runpy.run_path(str(folder / "predecessor_split.py")) + finally: + sys.path.pop(0) + a, b = {0: Q(1), 1: Q(1)}, {1: Q(1)} + program = mod["basis"](a,b,0,0) + def apply(events, values): + state = list(values) + for event in events: + if event[0] == "ADD": + _,d,s,q,_ = event + state[d] += Q(q)*state[s] + else: + assert event[0] == "SCALE" + _,d,q,_ = event + state[d] *= Q(q) + return state + assert program and apply(program, [0,1]) == [1,0] + for j in (0,1): + v = [Q(j==0),Q(j==1)] + transformed = apply(program, v) + assert transformed[0] == a[j] + assert apply(mod["inverse"](program), transformed) == v + try: + mod["basis"](a,{1:Q(-1)},0,0) + except ValueError as exc: + assert "Unit basis pairing" in str(exc) + else: + raise AssertionError("invalid paired basis accepted") + + +def run(script, *args, timeout): + subprocess.run([sys.executable,"-I","-B",str(script),*map(str,args)], check=True, timeout=timeout) + + +def check_receipts(files, pins): + for key, path in files.items(): + if sha256(path.read_bytes()).hexdigest() != pins[key]: + raise ValueError(f"replay receipt changed: {key}") + + +def crosscheck(files): + summary = read(HERE / "receipts/SUMMARY.json") + assert summary["head"] == HEAD and summary["copies"] == 17 + assert summary["unresolved"] == 0 and summary["compatible_saving_after_support"] == "0" + assert summary["kappa_change"] == "0" + signatures = {} + for label,parts,cut_count,suffix in (("3-plus-4",[3,4],714,24),("2-plus-5",[2,5],346,0)): + p,n,s,c,i = (read(files[f"{label}/{name}.json"]) + for name in ("PRICE","INVENTORY","SUPPORT","CUTS","RESULT")) + assert {r["head"] for r in (p,n,s,c,i)} == {HEAD} + assert p["copies"] == 17 and p["paid_rank_delta"] == {"1":17} + assert p["productive_rank_delta"] == {"6":-17, **{str(x):17 for x in parts}} + assert len(p["alternatives"]) == n["selected_signatures"] == i["typed_signatures"] == 83 + assert Counter(r["side"] for r in p["alternatives"]) == {"input":50,"output":33} + assert len(n["counts"]) == n["union_groups"] == i["union_groups"] == 73 + assert n["cuts"] == c["cut_incidences"] == i["cut_incidences"] == cut_count + assert s["counts"] == {"prefix_checked":cut_count} + assert s["phase"] == "exhausted" and s["pending_cut_count"] == 0 + assert not s["unresolved"] and s["candidate"] is None + assert i["positive_prefix_images"] == i["positive_pairings"] == 0 + assert i["suffix_nonzero_cuts"] == suffix and i["literal_paid_move_omission_rejected"] + margin = p["complete_margin_interval_per_alternative"] + assert Q(0) < Q(margin[0]) <= Q(margin[1]) + assert all(r["parts"] == parts and r["complete_margin_interval"] == margin for r in p["alternatives"]) + lo, hi = map(Q, i["whole_margins"]["+".join(map(str,parts))]) + assert 0 < lo <= hi and Q(margin[0]) <= hi and lo <= Q(margin[1]) + assert summary[label] == { + "typed_signatures":83, "union_groups":73, "representative_cut_incidences":cut_count, + "prefix_nonzero":0, "suffix_nonzero_independent":suffix, "price_only_complete_margin":margin, + "unresolved":0, "candidate":None, + } + signatures[label] = {(r["side"],tuple(r["prior"]),tuple(r["new"]),tuple(r["parts"])) + for r in p["alternatives"]} + assert all(len(x) == 83 for x in signatures.values()) + assert signatures["3-plus-4"].isdisjoint(signatures["2-plus-5"]) + + +def replay(output): + with TemporaryDirectory(prefix="p104-charged-rank-six-") as temp: + scratch = Path(temp) + deps = authenticate(scratch) + basis_control(deps) + pins = read(HERE / "receipts/SHA256.json") + files = {} + for label,primary,independent in ( + ("3-plus-4",deps / "round50/lead/screen.py",HERE / "engines/independent_3_4.py"), + ("2-plus-5",HERE / "engines/primary_2_5.py",HERE / "engines/independent_2_5.py"), + ): + result = scratch / label + audit = scratch / (label+"-independent") + run(primary,deps,result,"--seconds",120,timeout=122) + for name in ("PRICE","INVENTORY","SUPPORT"): + files[f"{label}/{name}.json"] = result / f"{name}.json" + check_receipts({k:v for k,v in files.items() if k.startswith(label)},pins) + run(independent,*(deps / d for d in ("round30","round35","round36","round37")), + result,audit,"--inventory-sha",pins[f"{label}/INVENTORY.json"], + "--support-sha",pins[f"{label}/SUPPORT.json"],timeout=45) + for name in ("CUTS","RESULT"): + files[f"{label}/{name}.json"] = audit / f"{name}.json" + assert files.keys() == pins.keys() + check_receipts(files,pins) + crosscheck(files) + if output is not None: + output.mkdir(parents=True,exist_ok=False) + for key, path in files.items(): + dest = output / key + dest.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(path,dest) + print("PASS_CHARGED_RANK_SIX_SUPPORT signatures=166 cuts=1060 pure_prefix=0 suffix_3_4=24 suffix_2_5=0 unresolved=0 saving_upper=0 kappa_change=0") + + +if __name__ == "__main__": + assert __debug__, "run with assertions enabled" + assert sys.version_info[:2] == (3,12), "Python 3.12 required" + p = ArgumentParser(description=__doc__) + p.add_argument("--out",type=Path,help="fresh destination for all ten full receipts") + replay(p.parse_args().out)